--- a/doc-src/IsarRef/Thy/document/Proof.tex Fri Apr 23 23:38:01 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/Proof.tex Fri Apr 23 23:42:46 2010 +0200
@@ -385,6 +385,9 @@
\indexdef{}{command}{lemma}\hypertarget{command.lemma}{\hyperlink{command.lemma}{\mbox{\isa{\isacommand{lemma}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\
\indexdef{}{command}{theorem}\hypertarget{command.theorem}{\hyperlink{command.theorem}{\mbox{\isa{\isacommand{theorem}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\
\indexdef{}{command}{corollary}\hypertarget{command.corollary}{\hyperlink{command.corollary}{\mbox{\isa{\isacommand{corollary}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\
+ \indexdef{}{command}{schematic\_lemma}\hypertarget{command.schematic-lemma}{\hyperlink{command.schematic-lemma}{\mbox{\isa{\isacommand{schematic{\isacharunderscore}lemma}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\
+ \indexdef{}{command}{schematic\_theorem}\hypertarget{command.schematic-theorem}{\hyperlink{command.schematic-theorem}{\mbox{\isa{\isacommand{schematic{\isacharunderscore}theorem}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\
+ \indexdef{}{command}{schematic\_corollary}\hypertarget{command.schematic-corollary}{\hyperlink{command.schematic-corollary}{\mbox{\isa{\isacommand{schematic{\isacharunderscore}corollary}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\
\indexdef{}{command}{have}\hypertarget{command.have}{\hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}} & : & \isa{{\isachardoublequote}proof{\isacharparenleft}state{\isacharparenright}\ {\isacharbar}\ proof{\isacharparenleft}chain{\isacharparenright}\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\
\indexdef{}{command}{show}\hypertarget{command.show}{\hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}}} & : & \isa{{\isachardoublequote}proof{\isacharparenleft}state{\isacharparenright}\ {\isacharbar}\ proof{\isacharparenleft}chain{\isacharparenright}\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\
\indexdef{}{command}{hence}\hypertarget{command.hence}{\hyperlink{command.hence}{\mbox{\isa{\isacommand{hence}}}}} & : & \isa{{\isachardoublequote}proof{\isacharparenleft}state{\isacharparenright}\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\
@@ -425,7 +428,8 @@
and assumptions, cf.\ \secref{sec:obtain}).
\begin{rail}
- ('lemma' | 'theorem' | 'corollary') target? (goal | longgoal)
+ ('lemma' | 'theorem' | 'corollary' |
+ 'schematic\_lemma' | 'schematic\_theorem' | 'schematic\_corollary') target? (goal | longgoal)
;
('have' | 'show' | 'hence' | 'thus') goal
;
@@ -454,6 +458,18 @@
\item \hyperlink{command.theorem}{\mbox{\isa{\isacommand{theorem}}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}} and \hyperlink{command.corollary}{\mbox{\isa{\isacommand{corollary}}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}} are essentially the same as \hyperlink{command.lemma}{\mbox{\isa{\isacommand{lemma}}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}}, but the facts are internally marked as
being of a different kind. This discrimination acts like a formal
comment.
+
+ \item \hyperlink{command.schematic-lemma}{\mbox{\isa{\isacommand{schematic{\isacharunderscore}lemma}}}}, \hyperlink{command.schematic-theorem}{\mbox{\isa{\isacommand{schematic{\isacharunderscore}theorem}}}},
+ \hyperlink{command.schematic-corollary}{\mbox{\isa{\isacommand{schematic{\isacharunderscore}corollary}}}} are similar to \hyperlink{command.lemma}{\mbox{\isa{\isacommand{lemma}}}},
+ \hyperlink{command.theorem}{\mbox{\isa{\isacommand{theorem}}}}, \hyperlink{command.corollary}{\mbox{\isa{\isacommand{corollary}}}}, respectively but allow
+ the statement to contain unbound schematic variables.
+
+ Under normal circumstances, an Isar proof text needs to specify
+ claims explicitly. Schematic goals are more like goals in Prolog,
+ where certain results are synthesized in the course of reasoning.
+ With schematic statements, the inherent compositionality of Isar
+ proofs is lost, which also impacts performance, because proof
+ checking is forced into sequential mode.
\item \hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}} claims a local goal,
eventually resulting in a fact within the current logical context.
@@ -499,27 +515,7 @@
meaning: (1) during the of this claim they refer to the the local
context introductions, (2) the resulting rule is annotated
accordingly to support symbolic case splits when used with the
- \indexref{}{method}{cases}\hyperlink{method.cases}{\mbox{\isa{cases}}} method (cf.\ \secref{sec:cases-induct}).
-
- \medskip
-
- \begin{warn}
- Isabelle/Isar suffers theory-level goal statements to contain
- \emph{unbound schematic variables}, although this does not conform
- to the aim of human-readable proof documents! The main problem
- with schematic goals is that the actual outcome is usually hard to
- predict, depending on the behavior of the proof methods applied
- during the course of reasoning. Note that most semi-automated
- methods heavily depend on several kinds of implicit rule
- declarations within the current theory context. As this would
- also result in non-compositional checking of sub-proofs,
- \emph{local goals} are not allowed to be schematic at all.
- Nevertheless, schematic goals do have their use in Prolog-style
- interactive synthesis of proven results, usually by stepwise
- refinement via emulation of traditional Isabelle tactic scripts
- (see also \secref{sec:tactic-commands}). In any case, users
- should know what they are doing.
- \end{warn}%
+ \indexref{}{method}{cases}\hyperlink{method.cases}{\mbox{\isa{cases}}} method (cf.\ \secref{sec:cases-induct}).%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/etc/isar-keywords-ZF.el Fri Apr 23 23:38:01 2010 +0200
+++ b/etc/isar-keywords-ZF.el Fri Apr 23 23:42:46 2010 +0200
@@ -162,6 +162,9 @@
"realizers"
"remove_thy"
"rep_datatype"
+ "schematic_corollary"
+ "schematic_lemma"
+ "schematic_theorem"
"sect"
"section"
"setup"
@@ -425,6 +428,9 @@
"instance"
"interpretation"
"lemma"
+ "schematic_corollary"
+ "schematic_lemma"
+ "schematic_theorem"
"subclass"
"sublocale"
"theorem"))
--- a/etc/isar-keywords.el Fri Apr 23 23:38:01 2010 +0200
+++ b/etc/isar-keywords.el Fri Apr 23 23:42:46 2010 +0200
@@ -220,6 +220,9 @@
"remove_thy"
"rep_datatype"
"repdef"
+ "schematic_corollary"
+ "schematic_lemma"
+ "schematic_theorem"
"sect"
"section"
"setup"
@@ -570,6 +573,9 @@
"quotient_type"
"recdef_tc"
"rep_datatype"
+ "schematic_corollary"
+ "schematic_lemma"
+ "schematic_theorem"
"specification"
"subclass"
"sublocale"