--- a/ProgTutorial/Tactical.thy Thu Aug 20 23:30:51 2009 +0200
+++ b/ProgTutorial/Tactical.thy Fri Aug 21 11:42:14 2009 +0200
@@ -49,41 +49,43 @@
THEN atac 1)
end" "?P \<or> ?Q \<Longrightarrow> ?Q \<or> ?P"}
- To start the proof, the function @{ML "Goal.prove"}~@{text "ctxt xs As C
- tac"} sets up a goal state for proving the goal @{text C}
- (that is @{prop "P \<or> Q \<Longrightarrow> Q \<or> P"} in the proof at hand) under the
- assumptions @{text As} (happens to be empty) with the variables
- @{text xs} that will be generalised once the goal is proved (in our case
- @{text P} and @{text Q}). The @{text "tac"} is the tactic that proves the goal;
- it can make use of the local assumptions (there are none in this example).
- The tactics @{ML_ind etac}, @{ML_ind rtac} and @{ML_ind atac}
- in the code above correspond
- roughly to @{text erule}, @{text rule} and @{text assumption}, respectively.
- The operator @{ML_ind THEN} strings the tactics together.
+ To start the proof, the function @{ML_ind "Goal.prove"}~@{text "ctxt xs As C
+ tac"} sets up a goal state for proving the goal @{text C} (that is @{prop "P
+ \<or> Q \<Longrightarrow> Q \<or> P"} in the proof at hand) under the assumptions @{text As}
+ (happens to be empty) with the variables @{text xs} that will be generalised
+ once the goal is proved (in our case @{text P} and @{text
+ Q}).\footnote{FIXME: explain prove earlier} The @{text "tac"} is the tactic
+ that proves the goal; it can make use of the local assumptions (there are
+ none in this example). The tactics @{ML_ind etac}, @{ML_ind rtac} and
+ @{ML_ind atac} in the code above correspond roughly to @{text erule}, @{text
+ rule} and @{text assumption}, respectively. The operator @{ML_ind THEN}
+ strings the tactics together.
\begin{readmore}
- To learn more about the function @{ML_ind prove in Goal} see \isccite{sec:results}
- and the file @{ML_file "Pure/goal.ML"}. See @{ML_file
+ To learn more about the function @{ML_ind prove in Goal} see
+ \isccite{sec:results} and the file @{ML_file "Pure/goal.ML"}. See @{ML_file
"Pure/tactic.ML"} and @{ML_file "Pure/tactical.ML"} for the code of basic
tactics and tactic combinators; see also Chapters 3 and 4 in the old
- Isabelle Reference Manual, and Chapter 3 in the Isabelle/Isar Implementation Manual.
+ Isabelle Reference Manual, and Chapter 3 in the Isabelle/Isar Implementation
+ Manual.
\end{readmore}
- Note that in the code above we use antiquotations for referencing the theorems. Many theorems
- also have ML-bindings with the same name. Therefore, we could also just have
- written @{ML "etac disjE 1"}, or in case where there is no ML-binding obtain
- the theorem dynamically using the function @{ML thm}; for example
- \mbox{@{ML "etac (thm \"disjE\") 1"}}. Both ways however are considered bad style!
- The reason
- is that the binding for @{ML disjE} can be re-assigned by the user and thus
- one does not have complete control over which theorem is actually
- applied. This problem is nicely prevented by using antiquotations, because
- then the theorems are fixed statically at compile-time.
+ Note that in the code above we use antiquotations for referencing the
+ theorems. Many theorems also have ML-bindings with the same name. Therefore,
+ we could also just have written @{ML "etac disjE 1"}, or in case where there
+ is no ML-binding obtain the theorem dynamically using the function @{ML
+ thm}; for example \mbox{@{ML "etac (thm \"disjE\") 1"}}. Both ways however
+ are considered bad style! The reason is that the binding for @{ML disjE} can
+ be re-assigned by the user and thus one does not have complete control over
+ which theorem is actually applied. This problem is nicely prevented by using
+ antiquotations, because then the theorems are fixed statically at
+ compile-time.
- During the development of automatic proof procedures, you will often find it
- necessary to test a tactic on examples. This can be conveniently
- done with the command \isacommand{apply}@{text "(tactic \<verbopen> \<dots> \<verbclose>)"}.
+ During the development of automatic proof procedures, you will often find it
+ necessary to test a tactic on examples. This can be conveniently done with
+ the command \isacommand{apply}@{text "(tactic \<verbopen> \<dots> \<verbclose>)"}.
Consider the following sequence of tactics
+
*}
ML{*val foo_tac =
@@ -302,7 +304,6 @@
\end{figure}
*}
-
text {*
which prints out the given theorem (using the string-function defined in
Section~\ref{sec:printing}) and then behaves like @{ML all_tac}. With this
@@ -315,9 +316,7 @@
where @{term C} is the goal to be proved and the @{term "A\<^isub>i"} are
the subgoals. So after setting up the lemma, the goal state is always of the
form @{text "C \<Longrightarrow> #C"}; when the proof is finished we are left with @{text
- "#C"}.\footnote{This only applies to single statements. If the lemma
- contains more than one statement, then one has more such implications.}
- Since the goal @{term C} can potentially be an implication, there is a
+ "#C"}. Since the goal @{term C} can potentially be an implication, there is a
``protector'' wrapped around it (the wrapper is the outermost constant
@{text "Const (\"prop\", bool \<Rightarrow> bool)"}; in the figure we make it visible
as an @{text #}). This wrapper prevents that premises of @{text C} are
@@ -1267,6 +1266,7 @@
simplification rules, congruence rules and simprocs.\label{fig:printss}}
\end{figure} *}
+
text {*
To see how they work, consider the function in Figure~\ref{fig:printss}, which
prints out some parts of a simpset. If you use it to print out the components of the