--- 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: