
diff -r 549be64e890f -r 58d4dc6000fc doc-src/IsarRef/Thy/document/Proof.tex
--- 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%
 %




