1.1 --- a/doc-src/IsarRef/Thy/document/Proof.tex Fri Apr 23 23:38:01 2010 +0200
1.2 +++ b/doc-src/IsarRef/Thy/document/Proof.tex Fri Apr 23 23:42:46 2010 +0200
1.3 @@ -385,6 +385,9 @@
1.4 \indexdef{}{command}{lemma}\hypertarget{command.lemma}{\hyperlink{command.lemma}{\mbox{\isa{\isacommand{lemma}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\
1.5 \indexdef{}{command}{theorem}\hypertarget{command.theorem}{\hyperlink{command.theorem}{\mbox{\isa{\isacommand{theorem}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\
1.6 \indexdef{}{command}{corollary}\hypertarget{command.corollary}{\hyperlink{command.corollary}{\mbox{\isa{\isacommand{corollary}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\
1.7 + \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}} \\
1.8 + \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}} \\
1.9 + \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}} \\
1.10 \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}} \\
1.11 \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}} \\
1.12 \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}} \\
1.13 @@ -425,7 +428,8 @@
1.14 and assumptions, cf.\ \secref{sec:obtain}).
1.15
1.16 \begin{rail}
1.17 - ('lemma' | 'theorem' | 'corollary') target? (goal | longgoal)
1.18 + ('lemma' | 'theorem' | 'corollary' |
1.19 + 'schematic\_lemma' | 'schematic\_theorem' | 'schematic\_corollary') target? (goal | longgoal)
1.20 ;
1.21 ('have' | 'show' | 'hence' | 'thus') goal
1.22 ;
1.23 @@ -454,6 +458,18 @@
1.24 \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
1.25 being of a different kind. This discrimination acts like a formal
1.26 comment.
1.27 +
1.28 + \item \hyperlink{command.schematic-lemma}{\mbox{\isa{\isacommand{schematic{\isacharunderscore}lemma}}}}, \hyperlink{command.schematic-theorem}{\mbox{\isa{\isacommand{schematic{\isacharunderscore}theorem}}}},
1.29 + \hyperlink{command.schematic-corollary}{\mbox{\isa{\isacommand{schematic{\isacharunderscore}corollary}}}} are similar to \hyperlink{command.lemma}{\mbox{\isa{\isacommand{lemma}}}},
1.30 + \hyperlink{command.theorem}{\mbox{\isa{\isacommand{theorem}}}}, \hyperlink{command.corollary}{\mbox{\isa{\isacommand{corollary}}}}, respectively but allow
1.31 + the statement to contain unbound schematic variables.
1.32 +
1.33 + Under normal circumstances, an Isar proof text needs to specify
1.34 + claims explicitly. Schematic goals are more like goals in Prolog,
1.35 + where certain results are synthesized in the course of reasoning.
1.36 + With schematic statements, the inherent compositionality of Isar
1.37 + proofs is lost, which also impacts performance, because proof
1.38 + checking is forced into sequential mode.
1.39
1.40 \item \hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}} claims a local goal,
1.41 eventually resulting in a fact within the current logical context.
1.42 @@ -499,27 +515,7 @@
1.43 meaning: (1) during the of this claim they refer to the the local
1.44 context introductions, (2) the resulting rule is annotated
1.45 accordingly to support symbolic case splits when used with the
1.46 - \indexref{}{method}{cases}\hyperlink{method.cases}{\mbox{\isa{cases}}} method (cf.\ \secref{sec:cases-induct}).
1.47 -
1.48 - \medskip
1.49 -
1.50 - \begin{warn}
1.51 - Isabelle/Isar suffers theory-level goal statements to contain
1.52 - \emph{unbound schematic variables}, although this does not conform
1.53 - to the aim of human-readable proof documents! The main problem
1.54 - with schematic goals is that the actual outcome is usually hard to
1.55 - predict, depending on the behavior of the proof methods applied
1.56 - during the course of reasoning. Note that most semi-automated
1.57 - methods heavily depend on several kinds of implicit rule
1.58 - declarations within the current theory context. As this would
1.59 - also result in non-compositional checking of sub-proofs,
1.60 - \emph{local goals} are not allowed to be schematic at all.
1.61 - Nevertheless, schematic goals do have their use in Prolog-style
1.62 - interactive synthesis of proven results, usually by stepwise
1.63 - refinement via emulation of traditional Isabelle tactic scripts
1.64 - (see also \secref{sec:tactic-commands}). In any case, users
1.65 - should know what they are doing.
1.66 - \end{warn}%
1.67 + \indexref{}{method}{cases}\hyperlink{method.cases}{\mbox{\isa{cases}}} method (cf.\ \secref{sec:cases-induct}).%
1.68 \end{isamarkuptext}%
1.69 \isamarkuptrue%
1.70 %
2.1 --- a/etc/isar-keywords-ZF.el Fri Apr 23 23:38:01 2010 +0200
2.2 +++ b/etc/isar-keywords-ZF.el Fri Apr 23 23:42:46 2010 +0200
2.3 @@ -162,6 +162,9 @@
2.4 "realizers"
2.5 "remove_thy"
2.6 "rep_datatype"
2.7 + "schematic_corollary"
2.8 + "schematic_lemma"
2.9 + "schematic_theorem"
2.10 "sect"
2.11 "section"
2.12 "setup"
2.13 @@ -425,6 +428,9 @@
2.14 "instance"
2.15 "interpretation"
2.16 "lemma"
2.17 + "schematic_corollary"
2.18 + "schematic_lemma"
2.19 + "schematic_theorem"
2.20 "subclass"
2.21 "sublocale"
2.22 "theorem"))
3.1 --- a/etc/isar-keywords.el Fri Apr 23 23:38:01 2010 +0200
3.2 +++ b/etc/isar-keywords.el Fri Apr 23 23:42:46 2010 +0200
3.3 @@ -220,6 +220,9 @@
3.4 "remove_thy"
3.5 "rep_datatype"
3.6 "repdef"
3.7 + "schematic_corollary"
3.8 + "schematic_lemma"
3.9 + "schematic_theorem"
3.10 "sect"
3.11 "section"
3.12 "setup"
3.13 @@ -570,6 +573,9 @@
3.14 "quotient_type"
3.15 "recdef_tc"
3.16 "rep_datatype"
3.17 + "schematic_corollary"
3.18 + "schematic_lemma"
3.19 + "schematic_theorem"
3.20 "specification"
3.21 "subclass"
3.22 "sublocale"