741 is also equivalent to $\FROM{this}~\HAVENAME$. |
741 is also equivalent to $\FROM{this}~\HAVENAME$. |
742 \item [$\THUSNAME$] abbreviates $\THEN~\SHOWNAME$. Note that $\THUSNAME$ is |
742 \item [$\THUSNAME$] abbreviates $\THEN~\SHOWNAME$. Note that $\THUSNAME$ is |
743 also equivalent to $\FROM{this}~\SHOWNAME$. |
743 also equivalent to $\FROM{this}~\SHOWNAME$. |
744 \end{descr} |
744 \end{descr} |
745 |
745 |
746 Note that any goal statement causes some term abbreviations (such as |
746 Any goal statement causes some term abbreviations (such as $\Var{thesis}$, |
747 $\Var{thesis}$, $\dots$) to be bound automatically, see also |
747 $\dots$) to be bound automatically, see also \S\ref{sec:term-abbrev}. |
748 \S\ref{sec:term-abbrev}. Furthermore, the local context of a (non-atomic) |
748 Furthermore, the local context of a (non-atomic) goal is provided via the case |
749 goal is provided via the case name $antecedent$\indexisarcase{antecedent}, see |
749 name $antecedent$\indexisarcase{antecedent}, see also \S\ref{sec:cases}. |
750 also \S\ref{sec:cases}. |
750 |
|
751 \medskip |
|
752 |
|
753 \begin{warn} |
|
754 Isabelle/Isar suffers theory-level goal statements to contain \emph{unbound |
|
755 schematic variables}, although this does not conform to the aim of |
|
756 human-readable proof documents! The main problem with schematic goals is |
|
757 that the actual outcome is usually hard to predict, depending on the |
|
758 behavior of the actual proof methods applied during the reasoning. Note |
|
759 that most semi-automated methods heavily depend on several kinds of implicit |
|
760 rule declarations within the current theory context. As this would also |
|
761 result in non-compositional checking of sub-proofs, \emph{local goals} are |
|
762 not allowed to be schematic at all. |
|
763 |
|
764 Nevertheless, schematic goals do have their use in Prolog-style interactive |
|
765 synthesis of proven results, usually by stepwise refinement via emulation of |
|
766 traditional Isabelle tactic scripts (see also \S\ref{sec:tactic-commands}). |
|
767 In any case, users should know what they are doing! |
|
768 \end{warn} |
751 |
769 |
752 |
770 |
753 \subsection{Initial and terminal proof steps}\label{sec:proof-steps} |
771 \subsection{Initial and terminal proof steps}\label{sec:proof-steps} |
754 |
772 |
755 \indexisarcmd{proof}\indexisarcmd{qed}\indexisarcmd{by} |
773 \indexisarcmd{proof}\indexisarcmd{qed}\indexisarcmd{by} |