--- a/ProgTutorial/Tactical.thy Sat Apr 25 14:28:58 2009 +0200
+++ b/ProgTutorial/Tactical.thy Sat Apr 25 17:46:47 2009 +0200
@@ -56,8 +56,8 @@
@{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 functions @{ML etac}, @{ML rtac} and @{ML atac} in the code above correspond to
- @{text erule}, @{text rule} and @{text assumption}, respectively.
+ The tactics @{ML etac}, @{ML rtac} and @{ML atac} in the code above correspond
+ roughly to @{text erule}, @{text rule} and @{text assumption}, respectively.
The operator @{ML THEN} strings the tactics together.
\begin{readmore}
@@ -145,7 +145,9 @@
@{text "*** At command \"apply\"."}
\end{isabelle}
- This means they failed. The reason for this error message is that tactics
+ This means they failed.\footnote{To be precise tactics do not produce this error
+ message, the it originates from the \isacommand{apply} wrapper.} The reason for this
+ error message is that tactics
are functions mapping a goal state to a (lazy) sequence of successor states.
Hence the type of a tactic is:
*}
@@ -310,10 +312,12 @@
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)"}. 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)"}; however this constant
- is invisible in the figure). This wrapper prevents that premises of @{text C} are
+ "(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
+ ``protector'' wrapped around it (the wrapper is the outermost constant
+ @{text "Const (\"prop\", bool \<Rightarrow> bool)"}; however this constant is invisible
+ in the figure). This wrapper prevents that premises of @{text C} are
misinterpreted as open subgoals. While tactics can operate on the subgoals
(the @{text "A\<^isub>i"} above), they are expected to leave the conclusion
@{term C} intact, with the exception of possibly instantiating schematic
@@ -362,6 +366,9 @@
(*<*)oops(*>*)
text {*
+ This tactic works however only if the quick-and-dirty mode of Isabelle
+ is switched on.
+
Another simple tactic is the function @{ML atac}, which, as shown in the previous
section, corresponds to the assumption command.
*}
@@ -374,7 +381,7 @@
(*<*)oops(*>*)
text {*
- Similarly, @{ML rtac}, @{ML dtac}, @{ML etac} and @{ML ftac} correspond
+ Similarly, @{ML rtac}, @{ML dtac}, @{ML etac} and @{ML ftac} correspond (roughly)
to @{text rule}, @{text drule}, @{text erule} and @{text frule},
respectively. Each of them take a theorem as argument and attempt to
apply it to a goal. Below are three self-explanatory examples.
@@ -461,7 +468,7 @@
applied to the first subgoal might instantiate this meta-variable in such a
way that the second subgoal becomes unprovable. If it is clear what the @{text "?x"}
should be, then this situation can be avoided by introducing a more
- constraint version of the @{text bspec}-rule. Such constraints can be given by
+ constrained version of the @{text bspec}-rule. Such constraints can be given by
pre-instantiating theorems with other theorems. One function to do this is
@{ML RS}
@@ -516,7 +523,7 @@
Often proofs on the ML-level involve elaborate operations on assumptions and
@{text "\<And>"}-quantified variables. To do such operations using the basic tactics
shown so far is very unwieldy and brittle. Some convenience and
- safety is provided by the tactic @{ML SUBPROOF}. This tactic fixes the parameters
+ safety is provided by @{ML SUBPROOF}. This tactic fixes the parameters
and binds the various components of a goal state to a record.
To see what happens, assume the function defined in Figure~\ref{fig:sptac}, which
takes a record and just prints out the content of this record (using the
@@ -629,20 +636,19 @@
(*<*)oops(*>*)
text {*
- The restriction in this tactic which is not present in @{ML atac} is
- that it cannot instantiate any
- schematic variable. This might be seen as a defect, but it is actually
- an advantage in the situations for which @{ML SUBPROOF} was designed:
- the reason is that, as mentioned before, instantiation of schematic variables can affect
- several goals and can render them unprovable. @{ML SUBPROOF} is meant
- to avoid this.
+ The restriction in this tactic which is not present in @{ML atac} is that it
+ cannot instantiate any schematic variables. This might be seen as a defect,
+ but it is actually an advantage in the situations for which @{ML SUBPROOF}
+ was designed: the reason is that, as mentioned before, instantiation of
+ schematic variables can affect several goals and can render them
+ unprovable. @{ML SUBPROOF} is meant to avoid this.
- Notice that @{ML atac'} inside @{ML SUBPROOF} calls @{ML resolve_tac} with
- the subgoal number @{text "1"} and also the outer call to @{ML SUBPROOF} in
- the \isacommand{apply}-step uses @{text "1"}. This is another advantage
- of @{ML SUBPROOF}: the addressing inside it is completely
- local to the tactic inside the subproof. It is therefore possible to also apply
- @{ML atac'} to the second goal by just writing:
+ Notice that @{ML atac'} inside @{ML SUBPROOF} calls @{ML resolve_tac} with
+ the subgoal number @{text "1"} and also the outer call to @{ML SUBPROOF} in
+ the \isacommand{apply}-step uses @{text "1"}. This is another advantage of
+ @{ML SUBPROOF}: the addressing inside it is completely local to the tactic
+ inside the subproof. It is therefore possible to also apply @{ML atac'} to
+ the second goal by just writing:
*}
lemma shows "True" and "\<lbrakk>B x y; A x y; C x y\<rbrakk> \<Longrightarrow> A x y"