# HG changeset patch # User wenzelm # Date 1272058966 -7200 # Node ID 58d4dc6000fc77856e7b291091809c21fc3d9167 # Parent 549be64e890fe9d196e6a99fd83787f4063137d8 updated generated files; 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% % diff -r 549be64e890f -r 58d4dc6000fc etc/isar-keywords-ZF.el --- 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")) diff -r 549be64e890f -r 58d4dc6000fc etc/isar-keywords.el --- 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"