diff -r 179ff9cb160b -r 5b25fee0362c doc-src/IsarRef/Thy/document/Proof.tex --- a/doc-src/IsarRef/Thy/document/Proof.tex Wed Mar 04 10:43:39 2009 +0100 +++ b/doc-src/IsarRef/Thy/document/Proof.tex Wed Mar 04 10:45:52 2009 +0100 @@ -3,8 +3,6 @@ \def\isabellecontext{Proof}% % \isadelimtheory -\isanewline -\isanewline % \endisadelimtheory % @@ -20,7 +18,7 @@ % \endisadelimtheory % -\isamarkupchapter{Proofs% +\isamarkupchapter{Proofs \label{ch:proofs}% } \isamarkuptrue% % @@ -28,8 +26,8 @@ Proof commands perform transitions of Isar/VM machine configurations, which are block-structured, consisting of a stack of nodes with three main components: logical proof context, current - facts, and open goals. Isar/VM transitions are \emph{typed} - according to the following three different modes of operation: + facts, and open goals. Isar/VM transitions are typed according to + the following three different modes of operation: \begin{description} @@ -49,13 +47,17 @@ \end{description} - The proof mode indicator may be read as a verb telling the writer - what kind of operation may be performed next. The corresponding - typings of proof commands restricts the shape of well-formed proof - texts to particular command sequences. So dynamic arrangements of - commands eventually turn out as static texts of a certain structure. - \Appref{ap:refcard} gives a simplified grammar of the overall - (extensible) language emerging that way.% + The proof mode indicator may be understood as an instruction to the + writer, telling what kind of operation may be performed next. The + corresponding typings of proof commands restricts the shape of + well-formed proof texts to particular command sequences. So dynamic + arrangements of commands eventually turn out as static texts of a + certain structure. + + \Appref{ap:refcard} gives a simplified grammar of the (extensible) + language emerging that way from the different types of proof + commands. The main ideas of the overall Isar framework are + explained in \chref{ch:isar-framework}.% \end{isamarkuptext}% \isamarkuptrue% % @@ -691,7 +693,6 @@ \indexdef{}{method}{assumption}\hypertarget{method.assumption}{\hyperlink{method.assumption}{\mbox{\isa{assumption}}}} & : & \isa{method} \\ \indexdef{}{method}{this}\hypertarget{method.this}{\hyperlink{method.this}{\mbox{\isa{this}}}} & : & \isa{method} \\ \indexdef{}{method}{rule}\hypertarget{method.rule}{\hyperlink{method.rule}{\mbox{\isa{rule}}}} & : & \isa{method} \\ - \indexdef{}{method}{iprover}\hypertarget{method.iprover}{\hyperlink{method.iprover}{\mbox{\isa{iprover}}}} & : & \isa{method} \\[0.5ex] \indexdef{Pure}{attribute}{intro}\hypertarget{attribute.Pure.intro}{\hyperlink{attribute.Pure.intro}{\mbox{\isa{intro}}}} & : & \isa{attribute} \\ \indexdef{Pure}{attribute}{elim}\hypertarget{attribute.Pure.elim}{\hyperlink{attribute.Pure.elim}{\mbox{\isa{elim}}}} & : & \isa{attribute} \\ \indexdef{Pure}{attribute}{dest}\hypertarget{attribute.Pure.dest}{\hyperlink{attribute.Pure.dest}{\mbox{\isa{dest}}}} & : & \isa{attribute} \\ @@ -706,8 +707,6 @@ ; 'rule' thmrefs? ; - 'iprover' ('!' ?) (rulemod *) - ; rulemod: ('intro' | 'elim' | 'dest') ((('!' | () | '?') nat?) | 'del') ':' thmrefs ; ('intro' | 'elim' | 'dest') ('!' | () | '?') nat? @@ -762,26 +761,11 @@ default behavior of \hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}} and ``\hyperlink{command.ddot}{\mbox{\isa{\isacommand{{\isachardot}{\isachardot}}}}}'' (double-dot) steps (see \secref{sec:proof-steps}). - \item \hyperlink{method.iprover}{\mbox{\isa{iprover}}} performs intuitionistic proof search, - depending on specifically declared rules from the context, or given - as explicit arguments. Chained facts are inserted into the goal - before commencing proof search; ``\hyperlink{method.iprover}{\mbox{\isa{iprover}}}\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}'' - means to include the current \hyperlink{fact.prems}{\mbox{\isa{prems}}} as well. - - Rules need to be classified as \hyperlink{attribute.Pure.intro}{\mbox{\isa{intro}}}, - \hyperlink{attribute.Pure.elim}{\mbox{\isa{elim}}}, or \hyperlink{attribute.Pure.dest}{\mbox{\isa{dest}}}; here the - ``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}'' indicator refers to ``safe'' rules, which may be - applied aggressively (without considering back-tracking later). - Rules declared with ``\isa{{\isachardoublequote}{\isacharquery}{\isachardoublequote}}'' are ignored in proof search (the - single-step \hyperlink{method.rule}{\mbox{\isa{rule}}} method still observes these). An - explicit weight annotation may be given as well; otherwise the - number of rule premises will be taken into account here. - \item \hyperlink{attribute.Pure.intro}{\mbox{\isa{intro}}}, \hyperlink{attribute.Pure.elim}{\mbox{\isa{elim}}}, and \hyperlink{attribute.Pure.dest}{\mbox{\isa{dest}}} declare introduction, elimination, and - destruct rules, to be used with the \hyperlink{method.rule}{\mbox{\isa{rule}}} and \hyperlink{method.iprover}{\mbox{\isa{iprover}}} methods. Note that the latter will ignore rules declared - with ``\isa{{\isachardoublequote}{\isacharquery}{\isachardoublequote}}'', while ``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}'' are used most - aggressively. + destruct rules, to be used with method \hyperlink{method.rule}{\mbox{\isa{rule}}}, and similar + tools. Note that the latter will ignore rules declared with + ``\isa{{\isachardoublequote}{\isacharquery}{\isachardoublequote}}'', while ``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}'' are used most aggressively. The classical reasoner (see \secref{sec:classical}) introduces its own variants of these attributes; use qualified names to access the @@ -966,7 +950,7 @@ \begin{matharray}{l} \isa{{\isachardoublequote}{\isasymlangle}using\ b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub k{\isasymrangle}{\isachardoublequote}}~~\hyperlink{command.obtain}{\mbox{\isa{\isacommand{obtain}}}}~\isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m\ {\isasymWHERE}\ a{\isacharcolon}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymphi}\isactrlsub n\ \ {\isasymlangle}proof{\isasymrangle}\ {\isasymequiv}{\isachardoublequote}} \\[1ex] \quad \hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}~\isa{{\isachardoublequote}{\isasymAnd}thesis{\isachardot}\ {\isacharparenleft}{\isasymAnd}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isachardot}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isasymphi}\isactrlsub n\ {\isasymLongrightarrow}\ thesis{\isacharparenright}\ {\isasymLongrightarrow}\ thesis{\isachardoublequote}} \\ - \quad \hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}~\isa{succeed} \\ + \quad \hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}~\hyperlink{method.succeed}{\mbox{\isa{succeed}}} \\ \qquad \hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}~\isa{thesis} \\ \qquad \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}~\isa{{\isachardoublequote}that\ {\isacharbrackleft}Pure{\isachardot}intro{\isacharquery}{\isacharbrackright}{\isacharcolon}\ {\isasymAnd}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isachardot}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isasymphi}\isactrlsub n\ {\isasymLongrightarrow}\ thesis{\isachardoublequote}} \\ \qquad \hyperlink{command.then}{\mbox{\isa{\isacommand{then}}}}~\hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}}~\isa{thesis} \\