# HG changeset patch # User wenzelm # Date 1286963535 -3600 # Node ID 57c7498f11a82dfb907aed36ec3ecdaccbd1a1a0 # Parent 21d189bfdfd151696c1fada2f22068998d6c400e tuned; diff -r 21d189bfdfd1 -r 57c7498f11a8 doc-src/IsarImplementation/Thy/Isar.thy --- a/doc-src/IsarImplementation/Thy/Isar.thy Tue Oct 12 21:18:05 2010 +0100 +++ b/doc-src/IsarImplementation/Thy/Isar.thy Wed Oct 13 10:52:15 2010 +0100 @@ -4,38 +4,38 @@ chapter {* Isar language elements *} -text {* The Isar proof language (see also - \cite[\S2]{isabelle-isar-ref}) consists of three main categories of - language elements: +text {* + %FIXME proper formal markup of methods!? + + The Isar proof language (see also \cite[\S2]{isabelle-isar-ref}) + consists of three main categories of language elements: \begin{enumerate} \item Proof \emph{commands} define the primary language of transactions of the underlying Isar/VM interpreter. Typical examples are @{command "fix"}, @{command "assume"}, @{command - "show"}, and @{command "by"}. + "show"}, @{command "proof"}, and @{command "qed"}. - Composing proof commands according to the rules of the Isar/VM - essentially leads to expressions of structured proof text, such that - both the machine and the human reader can give it a meaning as - formal reasoning. + Composing proof commands according to the rules of the Isar/VM leads + to expressions of structured proof text, such that both the machine + and the human reader can give it a meaning as formal reasoning. \item Proof \emph{methods} define a secondary language of mixed forward-backward refinement steps involving facts and goals. - Typical example methods are @{method rule}, @{method unfold}, or - @{text simp}. %FIXME proper formal markup!? + Typical examples are @{method rule}, @{method unfold}, and @{text + simp}. Methods can occur in certain well-defined parts of the Isar proof language, say as arguments to @{command "proof"}, @{command "qed"}, or @{command "by"}. \item \emph{Attributes} define a tertiary language of small - annotations to facts: facts being defined or referenced may always - be decorated with attribute expressions. Attributes can modify both - the fact and the context. + annotations to facts being defined or referenced. Attributes can + modify both the fact and the context. - Typical example attributes are @{attribute intro} (which affects the - context), or @{attribute symmetric} (which affects the fact). + Typical examples are @{attribute symmetric} (which affects the + fact), and @{attribute intro} (which affects the context). \end{enumerate} *} @@ -48,11 +48,11 @@ place: part of the commands are primitive, the other part is defined as derived elements. Adding to the genuine structured proof language requires profound understanding of the Isar/VM machinery, - though, so this is far beyond the scope of this manual. + though, so this is beyond the scope of this manual. What can be done realistically is to define some diagnostic commands - that merely inspect the general state of the Isar/VM, and report - some feedback to the user. Typically this involves checking of the + that inspect the general state of the Isar/VM, and report some + feedback to the user. Typically this involves checking of the linguistic \emph{mode} of a proof state, or peeking at the pending goals (if available). *} @@ -74,13 +74,13 @@ \item @{ML_type Proof.state} represents Isar proof states. This is a block-structured configuration with proof context, linguistic - mode, and optional goal state. An Isar goal consists of goal - context, goal facts (``@{text "using"}''), and tactical goal state - (see \secref{sec:tactical-goals}). + mode, and optional goal. The latter consists of goal context, goal + facts (``@{text "using"}''), and tactical goal state (see + \secref{sec:tactical-goals}). The general idea is that the facts shall contribute to the - refinement of the goal state --- how exactly is defined by the proof - method that is applied in that situation. + refinement of some parts of the tactical goal --- how exactly is + defined by the proof method that is applied in that situation. \item @{ML Proof.assert_forward}, @{ML Proof.assert_chain}, @{ML Proof.assert_backward} are partial identity functions that fail @@ -96,7 +96,7 @@ Isar goal (if available) in the form seen by ``simple'' methods (like @{text simp} or @{text blast}). The Isar goal facts are already inserted as premises into the subgoals, which are presented - separately as in @{ML Proof.goal}. + individually as in @{ML Proof.goal}. \item @{ML Proof.goal}~@{text "state"} returns the structured Isar goal (if available) in the form seen by regular methods (like @@ -105,9 +105,9 @@ \item @{ML Proof.raw_goal}~@{text "state"} returns the structured Isar goal (if available) in the raw internal form seen by ``raw'' - methods (like @{text induct}). This form is very rarely appropriate - for dignostic tools; @{ML Proof.simple_goal} or @{ML Proof.goal} - should be used in most situations. + methods (like @{text induct}). This form is rarely appropriate for + dignostic tools; @{ML Proof.simple_goal} or @{ML Proof.goal} should + be used in most situations. \end{description} *} @@ -146,19 +146,18 @@ text {* Proof methods are syntactically embedded into the Isar proof language as arguments to certain commands, e.g.\ @{command "by"} or - @{command apply}. User-space additions are relatively easy by - plugging a suitable method-valued parser function into the - framework. + @{command apply}. User-space additions are reasonably easy by + plugging suitable method-valued parser functions into the framework. Operationally, a proof method is like a structurally enhanced tactic: it operates on the full Isar goal configuration with - context, goal facts, and primitive goal state. Like a tactic, it + context, goal facts, and tactical goal state. Like a tactic, it enumerates possible follow-up goal states, with the potential - addition of named extensions of the proof context (called - \emph{cases}). + addition of named extensions of the proof context (\emph{cases}). - To get a better idea about the range of possibilities, consider - first the following structured proof scheme: + To get a better idea about the range of possibilities, consider the + following Isar proof schemes. First some general form of structured + proof text: \medskip \begin{tabular}{l} @@ -171,21 +170,20 @@ \noindent The goal configuration consists of @{text "facts\<^sub>1"} and @{text "facts\<^sub>2"} appended in that order, and various @{text "props"} - that are claimed here. The @{text "initial_method"} is invoked with - that information and refines the problem to something that is - accommodated recursively in the proof @{text "body"}. The @{text + being claimed here. The @{text "initial_method"} is invoked with + facts and goals together and refines the problem to something that + is handled recursively in the proof @{text "body"}. The @{text "terminal_method"} has another chance to finish-off any remaining subgoals, but it does not see the facts of the initial step. - \medskip Here is another pattern for unstructured proof scripts: + \medskip The second pattern illustrates unstructured proof scripts: + \medskip \begin{tabular}{l} @{command have}~@{text "props"} \\ - \quad@{command using}~@{text "facts\<^sub>1"} \\ - \quad@{command apply}~@{text "method\<^sub>1"} \\ + \quad@{command using}~@{text "facts\<^sub>1"}~@{command apply}~@{text "method\<^sub>1"} \\ \quad@{command apply}~@{text "method\<^sub>2"} \\ - \quad@{command using}~@{text "facts\<^sub>3"} \\ - \quad@{command apply}~@{text "method\<^sub>3"} \\ + \quad@{command using}~@{text "facts\<^sub>3"}~@{command apply}~@{text "method\<^sub>3"} \\ \quad@{command done} \\ \end{tabular} \medskip @@ -194,8 +192,8 @@ together while using @{text "facts\<^bsub>1\<^esub>"}. Since the @{command apply} command structurally resets the facts, the @{text "method\<^sub>2"} will operate on the remaining goal state without facts. The @{text - "method\<^sub>3"} will see a collection of @{text "facts\<^sub>3"} that has been - inserted into the script explicitly. + "method\<^sub>3"} will see again a collection of @{text "facts\<^sub>3"} that has + been inserted into the script explicitly. \medskip Empirically, Isar proof methods can be categorized as follows: