565 \begin{isamarkuptext}% |
565 \begin{isamarkuptext}% |
566 The old TFL commands \mbox{\isa{\isacommand{recdef}}} and \mbox{\isa{\isacommand{recdef{\isacharunderscore}tc}}} for defining recursive are mostly obsolete; \mbox{\isa{\isacommand{function}}} or \mbox{\isa{\isacommand{fun}}} should be used instead. |
566 The old TFL commands \mbox{\isa{\isacommand{recdef}}} and \mbox{\isa{\isacommand{recdef{\isacharunderscore}tc}}} for defining recursive are mostly obsolete; \mbox{\isa{\isacommand{function}}} or \mbox{\isa{\isacommand{fun}}} should be used instead. |
567 |
567 |
568 \begin{matharray}{rcl} |
568 \begin{matharray}{rcl} |
569 \indexdef{HOL}{command}{recdef}\mbox{\isa{\isacommand{recdef}}} & : & \isartrans{theory}{theory} \\ |
569 \indexdef{HOL}{command}{recdef}\mbox{\isa{\isacommand{recdef}}} & : & \isartrans{theory}{theory} \\ |
570 \indexdef{HOL}{command}{recdef-tc}\mbox{\isa{\isacommand{recdef{\isacharunderscore}tc}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isartrans{theory}{proof(prove)} \\ |
570 \indexdef{HOL}{command}{recdef\_tc}\mbox{\isa{\isacommand{recdef{\isacharunderscore}tc}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isartrans{theory}{proof(prove)} \\ |
571 \end{matharray} |
571 \end{matharray} |
572 |
572 |
573 \begin{rail} |
573 \begin{rail} |
574 'recdef' ('(' 'permissive' ')')? \\ name term (prop +) hints? |
574 'recdef' ('(' 'permissive' ')')? \\ name term (prop +) hints? |
575 ; |
575 ; |
607 |
607 |
608 \medskip Hints for \mbox{\isa{\isacommand{recdef}}} may be also declared |
608 \medskip Hints for \mbox{\isa{\isacommand{recdef}}} may be also declared |
609 globally, using the following attributes. |
609 globally, using the following attributes. |
610 |
610 |
611 \begin{matharray}{rcl} |
611 \begin{matharray}{rcl} |
612 \indexdef{HOL}{attribute}{recdef-simp}\mbox{\isa{recdef{\isacharunderscore}simp}} & : & \isaratt \\ |
612 \indexdef{HOL}{attribute}{recdef\_simp}\mbox{\isa{recdef{\isacharunderscore}simp}} & : & \isaratt \\ |
613 \indexdef{HOL}{attribute}{recdef-cong}\mbox{\isa{recdef{\isacharunderscore}cong}} & : & \isaratt \\ |
613 \indexdef{HOL}{attribute}{recdef\_cong}\mbox{\isa{recdef{\isacharunderscore}cong}} & : & \isaratt \\ |
614 \indexdef{HOL}{attribute}{recdef-wf}\mbox{\isa{recdef{\isacharunderscore}wf}} & : & \isaratt \\ |
614 \indexdef{HOL}{attribute}{recdef\_wf}\mbox{\isa{recdef{\isacharunderscore}wf}} & : & \isaratt \\ |
615 \end{matharray} |
615 \end{matharray} |
616 |
616 |
617 \begin{rail} |
617 \begin{rail} |
618 ('recdef\_simp' | 'recdef\_cong' | 'recdef\_wf') (() | 'add' | 'del') |
618 ('recdef\_simp' | 'recdef\_cong' | 'recdef\_wf') (() | 'add' | 'del') |
619 ; |
619 ; |
626 \isamarkuptrue% |
626 \isamarkuptrue% |
627 % |
627 % |
628 \begin{isamarkuptext}% |
628 \begin{isamarkuptext}% |
629 \begin{matharray}{rcl} |
629 \begin{matharray}{rcl} |
630 \indexdef{HOL}{command}{specification}\mbox{\isa{\isacommand{specification}}} & : & \isartrans{theory}{proof(prove)} \\ |
630 \indexdef{HOL}{command}{specification}\mbox{\isa{\isacommand{specification}}} & : & \isartrans{theory}{proof(prove)} \\ |
631 \indexdef{HOL}{command}{ax-specification}\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}} & : & \isartrans{theory}{proof(prove)} \\ |
631 \indexdef{HOL}{command}{ax\_specification}\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}} & : & \isartrans{theory}{proof(prove)} \\ |
632 \end{matharray} |
632 \end{matharray} |
633 |
633 |
634 \begin{rail} |
634 \begin{rail} |
635 ('specification' | 'ax\_specification') '(' (decl +) ')' \\ (thmdecl? prop +) |
635 ('specification' | 'ax\_specification') '(' (decl +) ')' \\ (thmdecl? prop +) |
636 ; |
636 ; |
696 domain of the fixedpoint definition, and the package does not have |
696 domain of the fixedpoint definition, and the package does not have |
697 to use inference rules for type-checking. |
697 to use inference rules for type-checking. |
698 |
698 |
699 \begin{matharray}{rcl} |
699 \begin{matharray}{rcl} |
700 \indexdef{HOL}{command}{inductive}\mbox{\isa{\isacommand{inductive}}} & : & \isarkeep{local{\dsh}theory} \\ |
700 \indexdef{HOL}{command}{inductive}\mbox{\isa{\isacommand{inductive}}} & : & \isarkeep{local{\dsh}theory} \\ |
701 \indexdef{HOL}{command}{inductive-set}\mbox{\isa{\isacommand{inductive{\isacharunderscore}set}}} & : & \isarkeep{local{\dsh}theory} \\ |
701 \indexdef{HOL}{command}{inductive\_set}\mbox{\isa{\isacommand{inductive{\isacharunderscore}set}}} & : & \isarkeep{local{\dsh}theory} \\ |
702 \indexdef{HOL}{command}{coinductive}\mbox{\isa{\isacommand{coinductive}}} & : & \isarkeep{local{\dsh}theory} \\ |
702 \indexdef{HOL}{command}{coinductive}\mbox{\isa{\isacommand{coinductive}}} & : & \isarkeep{local{\dsh}theory} \\ |
703 \indexdef{HOL}{command}{coinductive-set}\mbox{\isa{\isacommand{coinductive{\isacharunderscore}set}}} & : & \isarkeep{local{\dsh}theory} \\ |
703 \indexdef{HOL}{command}{coinductive\_set}\mbox{\isa{\isacommand{coinductive{\isacharunderscore}set}}} & : & \isarkeep{local{\dsh}theory} \\ |
704 \indexdef{HOL}{attribute}{mono}\mbox{\isa{mono}} & : & \isaratt \\ |
704 \indexdef{HOL}{attribute}{mono}\mbox{\isa{mono}} & : & \isaratt \\ |
705 \end{matharray} |
705 \end{matharray} |
706 |
706 |
707 \begin{rail} |
707 \begin{rail} |
708 ('inductive' | 'inductive\_set' | 'coinductive' | 'coinductive\_set') target? fixes ('for' fixes)? \\ |
708 ('inductive' | 'inductive\_set' | 'coinductive' | 'coinductive\_set') target? fixes ('for' fixes)? \\ |
815 \isamarkuptrue% |
815 \isamarkuptrue% |
816 % |
816 % |
817 \begin{isamarkuptext}% |
817 \begin{isamarkuptext}% |
818 \begin{matharray}{rcl} |
818 \begin{matharray}{rcl} |
819 \indexdef{HOL}{method}{arith}\mbox{\isa{arith}} & : & \isarmeth \\ |
819 \indexdef{HOL}{method}{arith}\mbox{\isa{arith}} & : & \isarmeth \\ |
820 \indexdef{HOL}{method}{arith-split}\mbox{\isa{arith{\isacharunderscore}split}} & : & \isaratt \\ |
820 \indexdef{HOL}{method}{arith\_split}\mbox{\isa{arith{\isacharunderscore}split}} & : & \isaratt \\ |
821 \end{matharray} |
821 \end{matharray} |
822 |
822 |
823 The \mbox{\isa{arith}} method decides linear arithmetic problems |
823 The \mbox{\isa{arith}} method decides linear arithmetic problems |
824 (on types \isa{nat}, \isa{int}, \isa{real}). Any current |
824 (on types \isa{nat}, \isa{int}, \isa{real}). Any current |
825 facts are inserted into the goal before running the procedure. |
825 facts are inserted into the goal before running the procedure. |
839 \begin{isamarkuptext}% |
839 \begin{isamarkuptext}% |
840 The following important tactical tools of Isabelle/HOL have been |
840 The following important tactical tools of Isabelle/HOL have been |
841 ported to Isar. These should be never used in proper proof texts! |
841 ported to Isar. These should be never used in proper proof texts! |
842 |
842 |
843 \begin{matharray}{rcl} |
843 \begin{matharray}{rcl} |
844 \indexdef{HOL}{method}{case-tac}\mbox{\isa{case{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\ |
844 \indexdef{HOL}{method}{case\_tac}\mbox{\isa{case{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\ |
845 \indexdef{HOL}{method}{induct-tac}\mbox{\isa{induct{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\ |
845 \indexdef{HOL}{method}{induct\_tac}\mbox{\isa{induct{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\ |
846 \indexdef{HOL}{method}{ind-cases}\mbox{\isa{ind{\isacharunderscore}cases}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\ |
846 \indexdef{HOL}{method}{ind\_cases}\mbox{\isa{ind{\isacharunderscore}cases}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\ |
847 \indexdef{HOL}{command}{inductive-cases}\mbox{\isa{\isacommand{inductive{\isacharunderscore}cases}}} & : & \isartrans{theory}{theory} \\ |
847 \indexdef{HOL}{command}{inductive\_cases}\mbox{\isa{\isacommand{inductive{\isacharunderscore}cases}}} & : & \isartrans{theory}{theory} \\ |
848 \end{matharray} |
848 \end{matharray} |
849 |
849 |
850 \begin{rail} |
850 \begin{rail} |
851 'case\_tac' goalspec? term rule? |
851 'case\_tac' goalspec? term rule? |
852 ; |
852 ; |
898 programs to SML. See \cite{isabelle-HOL} for further information |
898 programs to SML. See \cite{isabelle-HOL} for further information |
899 (this actually covers the new-style theory format as well). |
899 (this actually covers the new-style theory format as well). |
900 |
900 |
901 \begin{matharray}{rcl} |
901 \begin{matharray}{rcl} |
902 \indexdef{HOL}{command}{value}\mbox{\isa{\isacommand{value}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ |
902 \indexdef{HOL}{command}{value}\mbox{\isa{\isacommand{value}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ |
903 \indexdef{HOL}{command}{code-module}\mbox{\isa{\isacommand{code{\isacharunderscore}module}}} & : & \isartrans{theory}{theory} \\ |
903 \indexdef{HOL}{command}{code\_module}\mbox{\isa{\isacommand{code{\isacharunderscore}module}}} & : & \isartrans{theory}{theory} \\ |
904 \indexdef{HOL}{command}{code-library}\mbox{\isa{\isacommand{code{\isacharunderscore}library}}} & : & \isartrans{theory}{theory} \\ |
904 \indexdef{HOL}{command}{code\_library}\mbox{\isa{\isacommand{code{\isacharunderscore}library}}} & : & \isartrans{theory}{theory} \\ |
905 \indexdef{HOL}{command}{consts-code}\mbox{\isa{\isacommand{consts{\isacharunderscore}code}}} & : & \isartrans{theory}{theory} \\ |
905 \indexdef{HOL}{command}{consts\_code}\mbox{\isa{\isacommand{consts{\isacharunderscore}code}}} & : & \isartrans{theory}{theory} \\ |
906 \indexdef{HOL}{command}{types-code}\mbox{\isa{\isacommand{types{\isacharunderscore}code}}} & : & \isartrans{theory}{theory} \\ |
906 \indexdef{HOL}{command}{types\_code}\mbox{\isa{\isacommand{types{\isacharunderscore}code}}} & : & \isartrans{theory}{theory} \\ |
907 \indexdef{HOL}{attribute}{code}\mbox{\isa{code}} & : & \isaratt \\ |
907 \indexdef{HOL}{attribute}{code}\mbox{\isa{code}} & : & \isaratt \\ |
908 \end{matharray} |
908 \end{matharray} |
909 |
909 |
910 \begin{rail} |
910 \begin{rail} |
911 'value' term |
911 'value' term |
959 abstract executable view and \emph{serialization} to a specific |
959 abstract executable view and \emph{serialization} to a specific |
960 \emph{target language}. See \cite{isabelle-codegen} for an |
960 \emph{target language}. See \cite{isabelle-codegen} for an |
961 introduction on how to use it. |
961 introduction on how to use it. |
962 |
962 |
963 \begin{matharray}{rcl} |
963 \begin{matharray}{rcl} |
964 \indexdef{HOL}{command}{export-code}\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ |
964 \indexdef{HOL}{command}{export\_code}\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ |
965 \indexdef{HOL}{command}{code-thms}\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ |
965 \indexdef{HOL}{command}{code\_thms}\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ |
966 \indexdef{HOL}{command}{code-deps}\mbox{\isa{\isacommand{code{\isacharunderscore}deps}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ |
966 \indexdef{HOL}{command}{code\_deps}\mbox{\isa{\isacommand{code{\isacharunderscore}deps}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ |
967 \indexdef{HOL}{command}{code-datatype}\mbox{\isa{\isacommand{code{\isacharunderscore}datatype}}} & : & \isartrans{theory}{theory} \\ |
967 \indexdef{HOL}{command}{code\_datatype}\mbox{\isa{\isacommand{code{\isacharunderscore}datatype}}} & : & \isartrans{theory}{theory} \\ |
968 \indexdef{HOL}{command}{code-const}\mbox{\isa{\isacommand{code{\isacharunderscore}const}}} & : & \isartrans{theory}{theory} \\ |
968 \indexdef{HOL}{command}{code\_const}\mbox{\isa{\isacommand{code{\isacharunderscore}const}}} & : & \isartrans{theory}{theory} \\ |
969 \indexdef{HOL}{command}{code-type}\mbox{\isa{\isacommand{code{\isacharunderscore}type}}} & : & \isartrans{theory}{theory} \\ |
969 \indexdef{HOL}{command}{code\_type}\mbox{\isa{\isacommand{code{\isacharunderscore}type}}} & : & \isartrans{theory}{theory} \\ |
970 \indexdef{HOL}{command}{code-class}\mbox{\isa{\isacommand{code{\isacharunderscore}class}}} & : & \isartrans{theory}{theory} \\ |
970 \indexdef{HOL}{command}{code\_class}\mbox{\isa{\isacommand{code{\isacharunderscore}class}}} & : & \isartrans{theory}{theory} \\ |
971 \indexdef{HOL}{command}{code-instance}\mbox{\isa{\isacommand{code{\isacharunderscore}instance}}} & : & \isartrans{theory}{theory} \\ |
971 \indexdef{HOL}{command}{code\_instance}\mbox{\isa{\isacommand{code{\isacharunderscore}instance}}} & : & \isartrans{theory}{theory} \\ |
972 \indexdef{HOL}{command}{code-monad}\mbox{\isa{\isacommand{code{\isacharunderscore}monad}}} & : & \isartrans{theory}{theory} \\ |
972 \indexdef{HOL}{command}{code\_monad}\mbox{\isa{\isacommand{code{\isacharunderscore}monad}}} & : & \isartrans{theory}{theory} \\ |
973 \indexdef{HOL}{command}{code-reserved}\mbox{\isa{\isacommand{code{\isacharunderscore}reserved}}} & : & \isartrans{theory}{theory} \\ |
973 \indexdef{HOL}{command}{code\_reserved}\mbox{\isa{\isacommand{code{\isacharunderscore}reserved}}} & : & \isartrans{theory}{theory} \\ |
974 \indexdef{HOL}{command}{code-include}\mbox{\isa{\isacommand{code{\isacharunderscore}include}}} & : & \isartrans{theory}{theory} \\ |
974 \indexdef{HOL}{command}{code\_include}\mbox{\isa{\isacommand{code{\isacharunderscore}include}}} & : & \isartrans{theory}{theory} \\ |
975 \indexdef{HOL}{command}{code-modulename}\mbox{\isa{\isacommand{code{\isacharunderscore}modulename}}} & : & \isartrans{theory}{theory} \\ |
975 \indexdef{HOL}{command}{code\_modulename}\mbox{\isa{\isacommand{code{\isacharunderscore}modulename}}} & : & \isartrans{theory}{theory} \\ |
976 \indexdef{HOL}{command}{code-exception}\mbox{\isa{\isacommand{code{\isacharunderscore}exception}}} & : & \isartrans{theory}{theory} \\ |
976 \indexdef{HOL}{command}{code\_exception}\mbox{\isa{\isacommand{code{\isacharunderscore}exception}}} & : & \isartrans{theory}{theory} \\ |
977 \indexdef{HOL}{command}{print-codesetup}\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ |
977 \indexdef{HOL}{command}{print\_codesetup}\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ |
978 \indexdef{HOL}{attribute}{code}\mbox{\isa{code}} & : & \isaratt \\ |
978 \indexdef{HOL}{attribute}{code}\mbox{\isa{code}} & : & \isaratt \\ |
979 \end{matharray} |
979 \end{matharray} |
980 |
980 |
981 \begin{rail} |
981 \begin{rail} |
982 'export\_code' ( constexpr + ) ? \\ |
982 'export\_code' ( constexpr + ) ? \\ |