diff -r ec3fc818b82e -r 866841668584 doc-src/IsarRef/Thy/Framework.thy --- a/doc-src/IsarRef/Thy/Framework.thy Sat Feb 14 21:34:12 2009 +0100 +++ b/doc-src/IsarRef/Thy/Framework.thy Sat Feb 14 21:37:04 2009 +0100 @@ -97,9 +97,9 @@ text_raw {*\end{minipage}*} text {* - \medskip\noindent Note that @{command "assume"} augments the proof - context, @{command "then"} indicates that the current fact shall be - used in the next step, and @{command "have"} states an intermediate + \medskip\noindent Note that @{command assume} augments the proof + context, @{command then} indicates that the current fact shall be + used in the next step, and @{command have} states an intermediate goal. The two dots ``@{command ".."}'' refer to a complete proof of this claim, using the indicated facts and a canonical rule from the context. We could have been more explicit here by spelling out the @@ -154,17 +154,17 @@ text {* \medskip\noindent This Isar reasoning pattern again refers to the primitive rule depicted above. The system determines it in the - ``@{command "proof"}'' step, which could have been spelt out more - explicitly as ``@{command "proof"}~@{text "(rule InterI)"}''. Note + ``@{command proof}'' step, which could have been spelt out more + explicitly as ``@{command proof}~@{text "(rule InterI)"}''. Note that the rule involves both a local parameter @{term "A"} and an assumption @{prop "A \ \"} in the nested reasoning. This kind of compound rule typically demands a genuine sub-proof in Isar, working backwards rather than forwards as seen before. In the proof body we - encounter the @{command "fix"}-@{command "assume"}-@{command "show"} - skeleton of nested sub-proofs that is typical for Isar. The final - @{command "show"} is like @{command "have"} followed by an - additional refinement of the enclosing claim, using the rule derived - from the proof body. + encounter the @{command fix}-@{command assume}-@{command show} + outline of nested sub-proofs that is typical for Isar. The final + @{command show} is like @{command have} followed by an additional + refinement of the enclosing claim, using the rule derived from the + proof body. \medskip The next example involves @{term "\\"}, which can be characterized as the set of all @{term "x"} such that @{prop "\A. x @@ -207,7 +207,7 @@ conclusion @{prop "C"}, which represents the final result, but is irrelevant for now. This issue arises for any elimination rule involving local parameters. Isar provides the derived language - element @{command "obtain"}, which is able to perform the same + element @{command obtain}, which is able to perform the same elimination proof more conveniently: *} @@ -437,14 +437,13 @@ \] \noindent Here the @{text "sub\proof"} rule stems from the - main @{command "fix"}-@{command "assume"}-@{command "show"} skeleton - of Isar (cf.\ \secref{sec:framework-subproof}): each assumption + main @{command fix}-@{command assume}-@{command show} outline of + Isar (cf.\ \secref{sec:framework-subproof}): each assumption indicated in the text results in a marked premise @{text "G"} above. The marking enforces resolution against one of the sub-goal's - premises. Consequently, @{command "fix"}-@{command - "assume"}-@{command "show"} enables to fit the result of a sub-proof - quite robustly into a pending sub-goal, while maintaining a good - measure of flexibility. + premises. Consequently, @{command fix}-@{command assume}-@{command + show} enables to fit the result of a sub-proof quite robustly into a + pending sub-goal, while maintaining a good measure of flexibility. *} @@ -479,7 +478,7 @@ & @{text "|"} & @{command "note"}~@{text "name = facts"} \\ & @{text "|"} & @{command "let"}~@{text "term = term"} \\ & @{text "|"} & @{command "fix"}~@{text "var\<^sup>+"} \\ - & @{text "|"} & @{text "\ \inference\ name: props"} \\ + & @{text "|"} & @{command assume}~@{text "\inference\ name: props"} \\ & @{text "|"} & @{command "then"}@{text "\<^sup>?"}~@{text goal} \\ @{text goal} & = & @{command "have"}~@{text "name: props proof"} \\ & @{text "|"} & @{command "show"}~@{text "name: props proof"} \\ @@ -494,7 +493,7 @@ matching. \medskip Facts may be referenced by name or proposition. For - example, the result of ``@{command "have"}~@{text "a: A \proof\"}'' + example, the result of ``@{command have}~@{text "a: A \proof\"}'' becomes available both as @{text "a"} and \isacharbackquoteopen@{text "A"}\isacharbackquoteclose. Moreover, fact expressions may involve attributes that modify either the @@ -505,22 +504,26 @@ declares a fact as introduction rule in the context. The special fact called ``@{fact this}'' always refers to the last - result, as produced by @{command note}, @{text "\"}, @{command - "have"}, or @{command "show"}. Since @{command "note"} occurs - frequently together with @{command "then"} we provide some - abbreviations: ``@{command "from"}~@{text a}'' for ``@{command - "note"}~@{text a}~@{command "then"}'', and ``@{command - "with"}~@{text a}'' for ``@{command "from"}~@{text a}~@{keyword - "and"}~@{fact this}''. + result, as produced by @{command note}, @{command assume}, @{command + have}, or @{command show}. Since @{command note} occurs + frequently together with @{command then} we provide some + abbreviations: - \medskip The @{text "method"} category is essentially a parameter - and may be populated later. Methods use the facts indicated by - @{command "then"} or @{command "using"}, and then operate on the - goal state. Some basic methods are predefined: ``@{method "-"}'' - leaves the goal unchanged, ``@{method this}'' applies the facts as - rules to the goal, ``@{method "rule"}'' applies the facts to another - rule and the result to the goal (both ``@{method this}'' and - ``@{method rule}'' refer to @{inference resolution} of + \medskip + \begin{tabular}{rcl} + @{command from}~@{text a} & @{text "\"} & @{command note}~@{text a}~@{command then} \\ + @{command with}~@{text a} & @{text "\"} & @{command from}~@{text "a \ this"} \\ + \end{tabular} + \medskip + + The @{text "method"} category is essentially a parameter and may be + populated later. Methods use the facts indicated by @{command + "then"} or @{command using}, and then operate on the goal state. + Some basic methods are predefined: ``@{method "-"}'' leaves the goal + unchanged, ``@{method this}'' applies the facts as rules to the + goal, ``@{method "rule"}'' applies the facts to another rule and the + result to the goal (both ``@{method this}'' and ``@{method rule}'' + refer to @{inference resolution} of \secref{sec:framework-resolution}). The secondary arguments to ``@{method rule}'' may be specified explicitly as in ``@{text "(rule a)"}'', or picked from the context. In the latter case, the system @@ -528,27 +531,26 @@ @{attribute (Pure) dest}, followed by those declared as @{attribute (Pure) intro}. - The default method for @{command "proof"} is ``@{method rule}'' - (arguments picked from the context), for @{command "qed"} it is + The default method for @{command proof} is ``@{method rule}'' + (arguments picked from the context), for @{command qed} it is ``@{method "-"}''. Further abbreviations for terminal proof steps are ``@{command "by"}~@{text "method\<^sub>1 method\<^sub>2"}'' for - ``@{command "proof"}~@{text "method\<^sub>1"}~@{command - "qed"}~@{text "method\<^sub>2"}'', and ``@{command ".."}'' for - ``@{command "by"}~@{method rule}, and ``@{command "."}'' for - ``@{command "by"}~@{method this}''. The @{command "unfolding"} - element operates directly on the current facts and goal by applying - equalities. + ``@{command proof}~@{text "method\<^sub>1"}~@{command qed}~@{text + "method\<^sub>2"}'', and ``@{command ".."}'' for ``@{command + "by"}~@{method rule}, and ``@{command "."}'' for ``@{command + "by"}~@{method this}''. The @{command unfolding} element operates + directly on the current facts and goal by applying equalities. - \medskip Block structure can be indicated explicitly by - ``@{command "{"}~@{text "\"}~@{command "}"}'', although the body of - a sub-proof already involves implicit nesting. In any case, - @{command "next"} jumps into the next section of a block, i.e.\ it - acts like closing an implicit block scope and opening another one; - there is no direct correspondence to subgoals here. + \medskip Block structure can be indicated explicitly by ``@{command + "{"}~@{text "\"}~@{command "}"}'', although the body of a sub-proof + already involves implicit nesting. In any case, @{command next} + jumps into the next section of a block, i.e.\ it acts like closing + an implicit block scope and opening another one; there is no direct + correspondence to subgoals here. - The remaining elements @{command "fix"} and @{text "\"} build - up a local context (see \secref{sec:framework-context}), while - @{command "show"} refines a pending sub-goal by the rule resulting + The remaining elements @{command fix} and @{command assume} build up + a local context (see \secref{sec:framework-context}), while + @{command show} refines a pending sub-goal by the rule resulting from a nested sub-proof (see \secref{sec:framework-subproof}). Further derived concepts will support calculational reasoning (see \secref{sec:framework-calc}). @@ -563,35 +565,51 @@ towards a higher-level notion, with additional information for type-inference, term abbreviations, local facts, hypotheses etc. - The element @{command "fix"}~@{text "x :: \"} declares a local + The element @{command fix}~@{text "x :: \"} declares a local parameter, i.e.\ an arbitrary-but-fixed entity of a given type; in results exported from the context, @{text "x"} may become anything. - The @{text "\"} element provides a general interface to - hypotheses: ``@{text "\ \inference\ A"}'' produces @{text "A \ - A"} locally, while the included inference tells how to discharge - @{text "A"} from results @{text "A \ B"} later on. There is no - user-syntax for @{text "\inference\"}, i.e.\ @{text "\"} may - only occur in derived elements that provide a suitable inference - internally. In particular, ``@{command "assume"}~@{text A}'' - abbreviates ``@{text "\ \discharge\ A"}'', and ``@{command - "def"}~@{text "x \ a"}'' abbreviates ``@{command "fix"}~@{text "x - \ \expansion\ x \ a"}'', involving the following inferences: + The @{command assume}~@{text "\inference\"} element provides a + general interface to hypotheses: ``@{command assume}~@{text + "\inference\ A"}'' produces @{text "A \ A"} locally, while the + included inference tells how to discharge @{text A} from results + @{text "A \ B"} later on. There is no user-syntax for @{text + "\inference\"}, i.e.\ it may only occur internally when derived + commands are defined in ML. + + At the user-level, the default inference for @{command assume} is + @{inference discharge} as given below. The additional variants + @{command presume} and @{command def} are defined as follows: + + \medskip + \begin{tabular}{rcl} + @{command presume}~@{text A} & @{text "\"} & @{command assume}~@{text "\weak\discharge\ A"} \\ + @{command def}~@{text "x \ a"} & @{text "\"} & @{command fix}~@{text x}~@{command assume}~@{text "\expansion\ x \ a"} \\ + \end{tabular} + \medskip \[ - \infer[(@{inference_def "discharge"})]{@{text "\\ - A \ #A \ B"}}{@{text "\\ \ B"}} - \qquad + \infer[(@{inference_def discharge})]{@{text "\\ - A \ #A \ B"}}{@{text "\\ \ B"}} + \] + \[ + \infer[(@{inference_def "weak\discharge"})]{@{text "\\ - A \ A \ B"}}{@{text "\\ \ B"}} + \] + \[ \infer[(@{inference_def expansion})]{@{text "\\ - (x \ a) \ B a"}}{@{text "\\ \ B x"}} \] - \medskip The most interesting derived element in Isar is @{command - "obtain"} \cite[\S5.3]{Wenzel-PhD}, which supports generalized - elimination steps in a purely forward manner. + \medskip Note that @{inference discharge} and @{inference + "weak\discharge"} differ in the marker for @{prop A}, which is + relevant when the result of a @{command fix}-@{command + assume}-@{command show} outline is composed with a pending goal, + cf.\ \secref{sec:framework-subproof}. - The @{command "obtain"} element takes a specification of parameters - @{text "\<^vec>x"} and assumptions @{text "\<^vec>A"} to be added to - the context, together with a proof of a case rule stating that this - extension is conservative (i.e.\ may be removed from closed results - later on): + The most interesting derived context element in Isar is @{command + obtain} \cite[\S5.3]{Wenzel-PhD}, which supports generalized + elimination steps in a purely forward manner. The @{command obtain} + element takes a specification of parameters @{text "\<^vec>x"} and + assumptions @{text "\<^vec>A"} to be added to the context, together + with a proof of a case rule stating that this extension is + conservative (i.e.\ may be removed from closed results later on): \medskip \begin{tabular}{l} @@ -602,7 +620,7 @@ \qquad @{command assume}~@{text "[intro]: \\<^vec>x. \<^vec>A \<^vec>x \ thesis"} \\ \qquad @{command show}~@{text thesis}~@{command using}~@{text "\facts\ \proof\"} \\ \quad @{command qed} \\ - \quad @{command fix}~@{text "\<^vec>x \ \elimination case\ \<^vec>A \<^vec>x"} \\ + \quad @{command fix}~@{text "\<^vec>x"}~@{command assume}~@{text "\elimination case\ \<^vec>A \<^vec>x"} \\ \end{tabular} \medskip @@ -619,18 +637,17 @@ \noindent Here the name ``@{text thesis}'' is a specific convention for an arbitrary-but-fixed proposition; in the primitive natural deduction rules shown before we have occasionally used @{text C}. - The whole statement of ``@{command "obtain"}~@{text x}~@{keyword + The whole statement of ``@{command obtain}~@{text x}~@{keyword "where"}~@{text "A x"}'' may be read as a claim that @{text "A x"} may be assumed for some arbitrary-but-fixed @{text "x"}. Also note - that ``@{command "obtain"}~@{text A}~@{keyword "and"}~@{text B}'' - without parameters is similar to ``@{command "have"}~@{text - A}~@{keyword "and"}~@{text B}'', but the latter involves multiple - sub-goals. + that ``@{command obtain}~@{text "A \ B"}'' without parameters + is similar to ``@{command have}~@{text "A \ B"}'', but the + latter involves multiple sub-goals. \medskip The subsequent Isar proof texts explain all context elements introduced above using the formal proof language itself. After finishing a local proof within a block, we indicate the - exported result via @{command "note"}. This illustrates the meaning + exported result via @{command note}. This illustrates the meaning of Isar context elements without goals getting in between. *}