--- a/doc-src/IsarImplementation/Thy/Isar.thy Mon Oct 11 21:42:37 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/Isar.thy Tue Oct 12 20:03:31 2010 +0100
@@ -4,17 +4,38 @@
chapter {* Isar language elements *}
-text {*
- The primary Isar language consists of three main categories of
+text {* The Isar proof language (see also
+ \cite[\S2]{isabelle-isar-ref}) consists of three main categories of
language elements:
\begin{enumerate}
- \item Proof commands
+ \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"}.
+
+ 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.
- \item Proof methods
+ \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!?
- \item Attributes
+ 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.
+
+ Typical example attributes are @{attribute intro} (which affects the
+ context), or @{attribute symmetric} (which affects the fact).
\end{enumerate}
*}
@@ -22,7 +43,75 @@
section {* Proof commands *}
-text FIXME
+text {* In principle, Isar proof commands could be defined in
+ user-space as well. The system is built like that in the first
+ 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.
+
+ 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
+ linguistic \emph{mode} of a proof state, or peeking at the pending
+ goals (if available).
+*}
+
+text %mlref {*
+ \begin{mldecls}
+ @{index_ML_type Proof.state} \\
+ @{index_ML Proof.assert_forward: "Proof.state -> Proof.state"} \\
+ @{index_ML Proof.assert_chain: "Proof.state -> Proof.state"} \\
+ @{index_ML Proof.assert_backward: "Proof.state -> Proof.state"} \\
+ @{index_ML Proof.simple_goal: "Proof.state -> {context: Proof.context, goal: thm}"} \\
+ @{index_ML Proof.goal: "Proof.state ->
+ {context: Proof.context, facts: thm list, goal: thm}"} \\
+ @{index_ML Proof.raw_goal: "Proof.state ->
+ {context: Proof.context, facts: thm list, goal: thm}"} \\
+ \end{mldecls}
+
+ \begin{description}
+
+ \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}).
+
+ 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.
+
+ \item @{ML Proof.assert_forward}, @{ML Proof.assert_chain}, @{ML
+ Proof.assert_backward} are partial identity functions that fail
+ unless a certain linguistic mode is active, namely ``@{text
+ "proof(state)"}'', ``@{text "proof(chain)"}'', ``@{text
+ "proof(prove)"}'', respectively (using the terminology of
+ \cite{isabelle-isar-ref}).
+
+ It is advisable study the implementations of existing proof commands
+ for suitable modes to be asserted.
+
+ \item @{ML Proof.simple_goal}~@{text "state"} returns the structured
+ 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}.
+
+ \item @{ML Proof.goal}~@{text "state"} returns the structured Isar
+ goal (if available) in the form seen by regular methods (like
+ @{method rule}). The auxiliary internal encoding of Pure
+ conjunctions is split into individual subgoals as usual.
+
+ \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.
+
+ \end{description}
+*}
+
section {* Proof methods *}