11 \medskip |
11 \medskip |
12 |
12 |
13 Isar commands may be either \emph{proper} document constructors, or |
13 Isar commands may be either \emph{proper} document constructors, or |
14 \emph{improper commands}. Some proof methods and attributes introduced later |
14 \emph{improper commands}. Some proof methods and attributes introduced later |
15 are classified as improper as well. Improper Isar language elements, which |
15 are classified as improper as well. Improper Isar language elements, which |
16 are subsequently marked by $^*$, are often helpful when developing proof |
16 are subsequently marked by ``$^*$'', are often helpful when developing proof |
17 documents, while their use is discouraged for the final outcome. Typical |
17 documents, while their use is discouraged for the final outcome. Typical |
18 examples are diagnostic commands that print terms or theorems according to the |
18 examples are diagnostic commands that print terms or theorems according to the |
19 current context; other commands even emulate old-style tactical theorem |
19 current context; other commands even emulate old-style tactical theorem |
20 proving. |
20 proving. |
21 |
21 |
22 |
22 |
23 \section{Theory commands} |
23 \section{Theory specification commands} |
24 |
24 |
25 \subsection{Defining theories}\label{sec:begin-thy} |
25 \subsection{Defining theories}\label{sec:begin-thy} |
26 |
26 |
27 \indexisarcmd{header}\indexisarcmd{theory}\indexisarcmd{end}\indexisarcmd{context} |
27 \indexisarcmd{header}\indexisarcmd{theory}\indexisarcmd{end}\indexisarcmd{context} |
28 \begin{matharray}{rcl} |
28 \begin{matharray}{rcl} |
117 \begin{descr} |
117 \begin{descr} |
118 \item [$\isarkeyword{chapter}$, $\isarkeyword{section}$, |
118 \item [$\isarkeyword{chapter}$, $\isarkeyword{section}$, |
119 $\isarkeyword{subsection}$, and $\isarkeyword{subsubsection}$] mark chapter |
119 $\isarkeyword{subsection}$, and $\isarkeyword{subsubsection}$] mark chapter |
120 and section headings. |
120 and section headings. |
121 \item [$\TEXT$] specifies paragraphs of plain text, including references to |
121 \item [$\TEXT$] specifies paragraphs of plain text, including references to |
122 formal entities.\footnote{The latter feature is not yet supported. |
122 formal entities (see also \S\ref{sec:antiq} on ``antiquotations''). |
123 Nevertheless, any source text of the form |
|
124 ``\texttt{\at\ttlbrace$\dots$\ttrbrace}'' should be considered as reserved |
|
125 for future use.} |
|
126 \item [$\isarkeyword{text_raw}$] inserts {\LaTeX} source into the output, |
123 \item [$\isarkeyword{text_raw}$] inserts {\LaTeX} source into the output, |
127 without additional markup. Thus the full range of document manipulations |
124 without additional markup. Thus the full range of document manipulations |
128 becomes available. A typical application would be to emit |
125 becomes available. |
129 \verb,\begin{comment}, and \verb,\end{comment}, commands to exclude certain |
|
130 parts from the final document.\footnote{This requires the \texttt{comment} |
|
131 package to be included in {\LaTeX}, of course.} |
|
132 \end{descr} |
126 \end{descr} |
133 |
127 |
134 Any of these markup elements corresponds to a {\LaTeX} command with the name |
128 Any of these markup elements corresponds to a {\LaTeX} command with the name |
135 prefixed by \verb,\isamarkup,. For the sectioning commands this is a plain |
129 prefixed by \verb,\isamarkup,. For the sectioning commands this is a plain |
136 macro with a single argument, e.g.\ \verb,\isamarkupchapter{,\dots\verb,}, for |
130 macro with a single argument, e.g.\ \verb,\isamarkupchapter{,\dots\verb,}, for |
713 since $nothing$\indexisarthm{nothing} is bound to the empty list of facts. |
702 since $nothing$\indexisarthm{nothing} is bound to the empty list of facts. |
714 |
703 |
715 |
704 |
716 \subsection{Goal statements} |
705 \subsection{Goal statements} |
717 |
706 |
718 \indexisarcmd{theorem}\indexisarcmd{lemma} |
707 \indexisarcmd{lemma}\indexisarcmd{theorem}\indexisarcmd{corollary} |
719 \indexisarcmd{have}\indexisarcmd{show}\indexisarcmd{hence}\indexisarcmd{thus} |
708 \indexisarcmd{have}\indexisarcmd{show}\indexisarcmd{hence}\indexisarcmd{thus} |
720 \begin{matharray}{rcl} |
709 \begin{matharray}{rcl} |
|
710 \isarcmd{lemma} & : & \isartrans{theory}{proof(prove)} \\ |
721 \isarcmd{theorem} & : & \isartrans{theory}{proof(prove)} \\ |
711 \isarcmd{theorem} & : & \isartrans{theory}{proof(prove)} \\ |
722 \isarcmd{lemma} & : & \isartrans{theory}{proof(prove)} \\ |
712 \isarcmd{corollary} & : & \isartrans{theory}{proof(prove)} \\ |
723 \isarcmd{have} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\ |
713 \isarcmd{have} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\ |
724 \isarcmd{show} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\ |
714 \isarcmd{show} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\ |
725 \isarcmd{hence} & : & \isartrans{proof(state)}{proof(prove)} \\ |
715 \isarcmd{hence} & : & \isartrans{proof(state)}{proof(prove)} \\ |
726 \isarcmd{thus} & : & \isartrans{proof(state)}{proof(prove)} \\ |
716 \isarcmd{thus} & : & \isartrans{proof(state)}{proof(prove)} \\ |
727 \end{matharray} |
717 \end{matharray} |
728 |
718 |
729 Proof mode is entered from theory mode by initial goal commands $\THEOREMNAME$ |
719 From a theory context, proof mode is entered from theory mode by initial goal |
730 and $\LEMMANAME$. New local goals may be claimed within proof mode as well. |
720 commands $\LEMMANAME$, $\THEOREMNAME$, and $\COROLLARYNAME$. Within a proof, |
731 Four variants are available, indicating whether the result is meant to solve |
721 new claims may be introduced locally as well; four variants are available, |
732 some pending goal or whether forward chaining is indicated. |
722 indicating whether the result is meant to solve some pending goal or whether |
733 |
723 forward chaining is indicated. |
734 \begin{rail} |
724 |
735 ('theorem' | 'lemma') goal |
725 Goals may consist of multiple statements, resulting in a list of facts |
|
726 eventually. A pending multi-goal is internally represented as a meta-level |
|
727 conjunction (printed as \verb,&&,), which is automatically split into the |
|
728 corresponding number of sub-goals prior to any initial method application, via |
|
729 $\PROOFNAME$ (\S\ref{sec:proof-steps}) or $\APPLYNAME$ |
|
730 (\S\ref{sec:tactic-commands}).\footnote{Deviating from the latter principle, |
|
731 the $induct$ method covered in \S\ref{sec:cases-induct-meth} acts on |
|
732 multiple claims simultaneously.} |
|
733 |
|
734 %FIXME define locale, context |
|
735 |
|
736 \begin{rail} |
|
737 ('lemma' | 'theorem' | 'corollary') locale context goal |
736 ; |
738 ; |
737 ('have' | 'show' | 'hence' | 'thus') goal |
739 ('have' | 'show' | 'hence' | 'thus') goal |
738 ; |
740 ; |
739 |
741 |
740 goal: thmdecl? prop proppat? comment? |
742 goal: (props comment? + 'and') |
741 ; |
743 ; |
742 \end{rail} |
744 \end{rail} |
743 |
745 |
744 \begin{descr} |
746 \begin{descr} |
745 \item [$\THEOREM{a}{\phi}$] enters proof mode with $\phi$ as main goal, |
747 \item [$\LEMMA{a}{\vec\phi}$] enters proof mode with $\vec\phi$ as main goal, |
746 eventually resulting in some theorem $\turn \phi$ to be put back into the |
748 eventually resulting in some fact $\turn \vec\phi$ to be put back into the |
747 theory. |
749 theory context, and optionally into the specified locale, cf.\ |
748 \item [$\LEMMA{a}{\phi}$] is similar to $\THEOREMNAME$, but tags the result as |
750 \S\ref{sec:locale}. An additional \railnonterm{context} specification may |
749 ``lemma''. |
751 build an initial proof context for the subsequent claim; this may include |
750 \item [$\HAVE{a}{\phi}$] claims a local goal, eventually resulting in a |
752 local definitions and syntax as well, see \S\ref{sec:locale} for more |
751 theorem with the current assumption context as hypotheses. |
753 information. |
752 \item [$\SHOW{a}{\phi}$] is similar to $\HAVE{a}{\phi}$, but solves some |
754 |
753 pending goal with the result \emph{exported} into the corresponding context |
755 \item [$\THEOREM{a}{\vec\phi}$ and $\COROLLARY{a}{\vec\phi}$] are essentially |
754 (cf.\ \S\ref{sec:proof-context}). |
756 the same as $\LEMMA{a}{\vec\phi}$, but the facts are internally marked as |
|
757 being of a different kind. This discrimination acts like a formal comment. |
|
758 |
|
759 \item [$\HAVE{a}{\vec\phi}$] claims a local goal, eventually resulting in a |
|
760 fact within the current logical context. This operation is completely |
|
761 independent of any pending sub-goals of an enclosing goal statements, so |
|
762 $\HAVENAME$ may be freely used for experimental exploration of potential |
|
763 results within a proof body. |
|
764 |
|
765 \item [$\SHOW{a}{\vec\phi}$] is like $\HAVE{a}{\vec\phi}$ plus a second stage |
|
766 to refine some pending sub-goal for each one of the finished result, after |
|
767 having been exported into the corresponding context (at the head of the |
|
768 sub-proof that the $\SHOWNAME$ command belongs to). |
|
769 |
|
770 To accommodate interactive debugging, resulting rules are printed before |
|
771 being applied internally. Even more, interactive execution of $\SHOWNAME$ |
|
772 predicts potential failure after finishing its proof, and displays the |
|
773 resulting error message as a warning beforehand, adding this header: |
|
774 |
|
775 \begin{ttbox} |
|
776 Problem! Local statement will fail to solve any pending goal |
|
777 \end{ttbox} |
|
778 |
755 \item [$\HENCENAME$] abbreviates $\THEN~\HAVENAME$, i.e.\ claims a local goal |
779 \item [$\HENCENAME$] abbreviates $\THEN~\HAVENAME$, i.e.\ claims a local goal |
756 to be proven by forward chaining the current facts. Note that $\HENCENAME$ |
780 to be proven by forward chaining the current facts. Note that $\HENCENAME$ |
757 is also equivalent to $\FROM{this}~\HAVENAME$. |
781 is also equivalent to $\FROM{this}~\HAVENAME$. |
758 \item [$\THUSNAME$] abbreviates $\THEN~\SHOWNAME$. Note that $\THUSNAME$ is |
782 \item [$\THUSNAME$] abbreviates $\THEN~\SHOWNAME$. Note that $\THUSNAME$ is |
759 also equivalent to $\FROM{this}~\SHOWNAME$. |
783 also equivalent to $\FROM{this}~\SHOWNAME$. |
760 \end{descr} |
784 \end{descr} |
761 |
785 |
762 Any goal statement causes some term abbreviations (such as $\Var{thesis}$, |
786 Any goal statement causes some term abbreviations (such as $\Var{thesis}$, |
763 $\dots$) to be bound automatically, see also \S\ref{sec:term-abbrev}. |
787 $\dots$) to be bound automatically, see also \S\ref{sec:term-abbrev}. |
764 Furthermore, the local context of a (non-atomic) goal is provided via the |
788 Furthermore, the local context of a (non-atomic) goal is provided via the |
765 $rule_context$\indexisarcase{rule-context} case, see also \S\ref{sec:cases}. |
789 $rule_context$\indexisarcase{rule-context} case, see also |
|
790 \S\ref{sec:rule-cases}. |
766 |
791 |
767 \medskip |
792 \medskip |
768 |
793 |
769 \begin{warn} |
794 \begin{warn} |
770 Isabelle/Isar suffers theory-level goal statements to contain \emph{unbound |
795 Isabelle/Isar suffers theory-level goal statements to contain \emph{unbound |
773 that the actual outcome is usually hard to predict, depending on the |
798 that the actual outcome is usually hard to predict, depending on the |
774 behavior of the actual proof methods applied during the reasoning. Note |
799 behavior of the actual proof methods applied during the reasoning. Note |
775 that most semi-automated methods heavily depend on several kinds of implicit |
800 that most semi-automated methods heavily depend on several kinds of implicit |
776 rule declarations within the current theory context. As this would also |
801 rule declarations within the current theory context. As this would also |
777 result in non-compositional checking of sub-proofs, \emph{local goals} are |
802 result in non-compositional checking of sub-proofs, \emph{local goals} are |
778 not allowed to be schematic at all. |
803 not allowed to be schematic at all. Nevertheless, schematic goals do have |
779 |
804 their use in Prolog-style interactive synthesis of proven results, usually |
780 Nevertheless, schematic goals do have their use in Prolog-style interactive |
805 by stepwise refinement via emulation of traditional Isabelle tactic scripts |
781 synthesis of proven results, usually by stepwise refinement via emulation of |
806 (see also \S\ref{sec:tactic-commands}). In any case, users should know what |
782 traditional Isabelle tactic scripts (see also \S\ref{sec:tactic-commands}). |
807 they are doing. |
783 In any case, users should know what they are doing! |
|
784 \end{warn} |
808 \end{warn} |
785 |
809 |
786 |
810 |
787 \subsection{Initial and terminal proof steps}\label{sec:proof-steps} |
811 \subsection{Initial and terminal proof steps}\label{sec:proof-steps} |
788 |
812 |
860 sufficient to see what is going wrong. |
884 sufficient to see what is going wrong. |
861 \item [``$\DDOT$''] is a \emph{default proof}\index{proof!default}; it |
885 \item [``$\DDOT$''] is a \emph{default proof}\index{proof!default}; it |
862 abbreviates $\BY{rule}$. |
886 abbreviates $\BY{rule}$. |
863 \item [``$\DOT$''] is a \emph{trivial proof}\index{proof!trivial}; it |
887 \item [``$\DOT$''] is a \emph{trivial proof}\index{proof!trivial}; it |
864 abbreviates $\BY{this}$. |
888 abbreviates $\BY{this}$. |
865 \item [$\SORRY$] is a \emph{fake proof}\index{proof!fake}; provided that the |
889 \item [$\SORRY$] is a \emph{fake proof}\index{proof!fake} pretending to solve |
866 \texttt{quick_and_dirty} flag is enabled, $\SORRY$ pretends to solve the |
890 the pending claim without further ado. This only works in interactive |
867 goal without further ado. Of course, the result would be a fake theorem |
891 development, or if the \texttt{quick_and_dirty} flag is enabled. Certainly, |
868 only, involving some oracle in its internal derivation object (this is |
892 any facts emerging from fake proofs are not the real thing. Internally, |
869 indicated as ``$[!]$'' in the printed result). The main application of |
893 each theorem container is tainted by an oracle invocation, which is |
870 $\SORRY$ is to support experimentation and top-down proof development. |
894 indicated as ``$[!]$'' in the printed result. |
|
895 |
|
896 The most important application of $\SORRY$ is to support experimentation and |
|
897 top-down proof development in a simple manner. |
871 \end{descr} |
898 \end{descr} |
872 |
899 |
873 |
900 |
874 \subsection{Fundamental methods and attributes}\label{sec:pure-meth-att} |
901 \subsection{Fundamental methods and attributes}\label{sec:pure-meth-att} |
875 |
902 |
1004 statement that is an application $f(t)$, then $t$ is bound to the special text |
1031 statement that is an application $f(t)$, then $t$ is bound to the special text |
1005 variable ``$\dots$''\indexisarvar{\dots} (three dots). The canonical |
1032 variable ``$\dots$''\indexisarvar{\dots} (three dots). The canonical |
1006 application of the latter are calculational proofs (see |
1033 application of the latter are calculational proofs (see |
1007 \S\ref{sec:calculation}). |
1034 \S\ref{sec:calculation}). |
1008 |
1035 |
1009 %FIXME !? |
|
1010 |
|
1011 % A few \emph{automatic} term abbreviations\index{term abbreviations} for goals |
|
1012 % and facts are available as well. For any open goal, |
|
1013 % $\Var{thesis_prop}$\indexisarvar{thesis-prop} refers to the full proposition |
|
1014 % (which may be a rule), $\Var{thesis_concl}$\indexisarvar{thesis-concl} to its |
|
1015 % (atomic) conclusion, and $\Var{thesis}$\indexisarvar{thesis} to its |
|
1016 % object-level statement. The latter two abstract over any meta-level |
|
1017 % parameters. |
|
1018 |
|
1019 % Fact statements resulting from assumptions or finished goals are bound as |
|
1020 % $\Var{this_prop}$\indexisarvar{this-prop}, |
|
1021 % $\Var{this_concl}$\indexisarvar{this-concl}, and |
|
1022 % $\Var{this}$\indexisarvar{this}, similar to $\Var{thesis}$ above. In case |
|
1023 % $\Var{this}$ refers to an object-logic statement that is an application |
|
1024 % $f(t)$, then $t$ is bound to the special text variable |
|
1025 % ``$\dots$''\indexisarvar{\dots} (three dots). The canonical application of |
|
1026 % the latter are calculational proofs (see \S\ref{sec:calculation}). |
|
1027 |
|
1028 |
1036 |
1029 \subsection{Block structure} |
1037 \subsection{Block structure} |
1030 |
1038 |
1031 \indexisarcmd{next}\indexisarcmd{\{}\indexisarcmd{\}} |
1039 \indexisarcmd{next}\indexisarcmd{\{}\indexisarcmd{\}} |
1032 \begin{matharray}{rcl} |
1040 \begin{matharray}{rcl} |