--- a/CookBook/Tactical.thy Sat Feb 07 14:21:33 2009 +0000
+++ b/CookBook/Tactical.thy Sun Feb 08 08:45:25 2009 +0000
@@ -100,8 +100,8 @@
done
text {*
- By using @{text "tactic \<verbopen> \<dots> \<verbclose>"} in the apply-step,
- you can call from the user level of Isabelle the tactic @{ML foo_tac} or
+ By using @{text "tactic \<verbopen> \<dots> \<verbclose>"} you can call from the
+ user level of Isabelle the tactic @{ML foo_tac} or
any other function that returns a tactic.
The tactic @{ML foo_tac} is just a sequence of simple tactics stringed
@@ -196,10 +196,10 @@
instead.
\end{readmore}
- For a beginner it might be surprising that tactics, which transform
+ It might be surprising that tactics, which transform
one proof state to the next, are functions from theorems to theorem
(sequences). The surprise resolves by knowing that every
- proof state is indeed a theorem. To shed more light on this,
+ goal state is indeed a theorem. To shed more light on this,
let us modify the code of @{ML all_tac} to obtain the following
tactic
*}
@@ -216,7 +216,7 @@
in Section~\ref{sec:printing}) and then behaves like @{ML all_tac}. We
now can inspect every proof state in the follwing proof. On the left-hand
side we show the goal state as shown by the system; on the right-hand
- side the print out from our @{ML my_print_tac}.
+ side the print out from @{ML my_print_tac}.
*}
lemma shows "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"
@@ -275,9 +275,12 @@
@{text[display] "A\<^isub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^isub>n \<Longrightarrow> (C)"}
where @{term C} is the goal to be proved and the @{term "A\<^isub>i"} are the
- subgoals. Since the goal @{term C} can potentially be an implication,
- there is a protector (invisible in the print out above) wrapped around
- it. This prevents that premises are misinterpreted as open subgoals.
+ subgoals. So in the first step the goal state is always of the form
+ @{text "C \<Longrightarrow> (C)"}. Since the goal @{term C} can potentially be an implication,
+ there is a ``protector'' wrapped around it (in from of an outermost constant
+ @{text "Const (\"prop\", bool \<Rightarrow> bool)"} applied to each goal;
+ however this constant is invisible in the print out above). This
+ prevents that premises 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 variables.
@@ -297,23 +300,30 @@
text {*
Similarly, @{ML rtac}, @{ML dtac}, @{ML etac} and @{ML ftac} correspond
to @{text rule}, @{text drule}, @{text erule} and @{text frule},
- respectively. Below are three examples with the resulting goal state. How
- they work should therefore be self-explanatory.
+ respectively. Each of them takes a theorem as argument. Below are three
+ examples with the resulting goal state. How
+ they work should be self-explanatory.
*}
lemma shows "P \<and> Q"
apply(tactic {* rtac @{thm conjI} 1 *})
-txt{*@{subgoals [display]}*}
+txt{*\begin{minipage}{\textwidth}
+ @{subgoals [display]}
+ \end{minipage}*}
(*<*)oops(*>*)
lemma shows "P \<and> Q \<Longrightarrow> False"
apply(tactic {* etac @{thm conjE} 1 *})
-txt{*@{subgoals [display]}*}
+txt{*\begin{minipage}{\textwidth}
+ @{subgoals [display]}
+ \end{minipage}*}
(*<*)oops(*>*)
lemma shows "False \<and> True \<Longrightarrow> False"
apply(tactic {* dtac @{thm conjunct2} 1 *})
-txt{*@{subgoals [display]}*}
+txt{*\begin{minipage}{\textwidth}
+ @{subgoals [display]}
+ \end{minipage}*}
(*<*)oops(*>*)
text {*
@@ -323,7 +333,9 @@
lemma shows "Foo" and "P \<and> Q"
apply(tactic {* rtac @{thm conjI} 2 *})
-txt {*@{subgoals [display]}*}
+txt {*\begin{minipage}{\textwidth}
+ @{subgoals [display]}
+ \end{minipage}*}
(*<*)oops(*>*)
text {*
@@ -343,7 +355,9 @@
lemma shows "C \<longrightarrow> (A \<and> B)" and "(A \<longrightarrow> B) \<and> C"
apply(tactic {* resolve_tac_xmp 1 *})
apply(tactic {* resolve_tac_xmp 2 *})
-txt{* @{subgoals [display]} *}
+txt{*\begin{minipage}{\textwidth}
+ @{subgoals [display]}
+ \end{minipage}*}
(*<*)oops(*>*)
text {*
@@ -359,15 +373,12 @@
(*<*)oops(*>*)
text {*
- Also for useful for debugging purposes are the tactics @{ML all_tac} and
- @{ML no_tac}. The former always succeeds (but does not change the goal state), and
- the latter always fails.
-
+
(FIXME explain RS MRS)
- Often proofs involve elaborate operations on assumptions and variables
- @{text "\<And>"}-quantified in the goal state. To do such operations on the ML-level
- using the basic tactics, is very unwieldy and brittle. Some convenience and
+ Often proofs involve elaborate operations on assumptions and
+ @{text "\<And>"}-quantified variables. To do such operations on the ML-level
+ using the basic tactics is very unwieldy and brittle. Some convenience and
safety is provided by the tactic @{ML SUBPROOF}. This tactic fixes the parameters
and binds the various components of a proof state into a record.
*}
@@ -426,15 +437,15 @@
Note in the actual output the brown colour of the variables @{term x} and
@{term y}. Although parameters in the original goal, they are fixed inside
the subproof. Similarly the schematic variable @{term z}. The assumption
- is bound once as @{ML_type cterm} to the record-variable @{text asms} and
- another time as @{ML_type thm} to @{text prems}.
+ @{prop "A x y"} is bound once as @{ML_type cterm} to the record-variable
+ @{text asms} and another time as @{ML_type thm} to @{text prems}.
Notice also that we had to append @{text "?"} to \isacommand{apply}. The
reason is that @{ML SUBPROOF} normally expects that the subgoal is solved completely.
Since in the function @{ML sp_tac} we returned the tactic @{ML no_tac}, the subproof
obviously fails. The question-mark allows us to recover from this failure
in a graceful manner so that the warning messages are not overwritten
- by the error message.
+ by an error message.
If we continue the proof script by applying the @{text impI}-rule
*}
@@ -458,7 +469,7 @@
(*<*)oops(*>*)
text {*
- where we now also have @{term "B y x"} as assumption.
+ where we now also have @{term "B y x"} as an assumption.
One convenience of @{ML SUBPROOF} is that we can apply assumption
using the usual tactics, because the parameter @{text prems}
@@ -466,23 +477,42 @@
implement a tactic that almost behaves like @{ML atac}:
*}
+ML{*val atac' = SUBPROOF (fn {prems, ...} => resolve_tac prems 1)*}
lemma shows "\<And>x y. \<lbrakk>B x y; A x y; C x y\<rbrakk> \<Longrightarrow> A x y"
-apply(tactic
- {* SUBPROOF (fn {prems, ...} => resolve_tac prems 1) @{context} 1 *})
+apply(tactic {* atac' @{context} 1 *})
txt{* yields
@{subgoals [display]} *}
(*<*)oops(*>*)
+text {*
+ The restriction in this tactic is that it cannot instantiate any
+ schematic variables. This might be seen as a defect, but is actually
+ an advantage in the situations for which @{ML SUBPROOF} was designed:
+ the reason is that instantiation of schematic variables can affect
+ several goals and can render them unprovable. @{ML SUBPROOF} is meant
+ to avoid this.
+
+ Notice that @{ML atac'} 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"}. Another advantage
+ of @{ML SUBGOAL} is that the addressing inside it is completely
+ local to the proof inside. It is therefore possible to also apply
+ @{ML atac'} to the second goal:
+*}
+
+lemma shows "True" and "\<And>x y. \<lbrakk>B x y; A x y; C x y\<rbrakk> \<Longrightarrow> A x y"
+apply(tactic {* atac' @{context} 2 *})
+txt{* This gives:
+ @{subgoals [display]} *}
+(*<*)oops(*>*)
+
text {*
- The restriction in this tactic is that it cannot instantiate any
- schematic variables. This might be seen as a defect, but is actually
- an advantage in the situations for which @{ML SUBPROOF} was designed:
- the reason is that instantiation of schematic variables can potentially
- has affect several goals and can render them unprovable.
-
- A similar but less powerful function is @{ML SUBGOAL}. It allows you to
- inspect a subgoal specified by a number.
+ A similar but less powerful function than @{ML SUBPROOF} is @{ML SUBGOAL}.
+ It allows you to inspect a subgoal specified by a number. With this we can
+ implement a little tactic that applies a rule corresponding to its
+ topmost connective. The tactic should only apply ``safe'' rules (that is
+ which do not render the goal unprovable). For this we can write:
*}
ML %linenumbers{*fun select_tac (t,i) =
@@ -492,12 +522,13 @@
| @{term "op \<longrightarrow>"} $ _ $ _ => rtac @{thm impI} i
| @{term "Not"} $ _ => rtac @{thm notI} i
| Const (@{const_name "All"}, _) $ _ => rtac @{thm allI} i
- | _ => no_tac*}
+ | _ => all_tac*}
-lemma shows "A \<and> B" "A \<longrightarrow> B" "\<forall>x. C x"
+lemma shows "A \<and> B" "A \<longrightarrow> B" "\<forall>x. C x" "D \<Longrightarrow> E"
+apply(tactic {* SUBGOAL select_tac 4 *})
+apply(tactic {* SUBGOAL select_tac 3 *})
+apply(tactic {* SUBGOAL select_tac 2 *})
apply(tactic {* SUBGOAL select_tac 1 *})
-apply(tactic {* SUBGOAL select_tac 3 *})
-apply(tactic {* SUBGOAL select_tac 4 *})
txt{* @{subgoals [display]} *}
(*<*)oops(*>*)
@@ -506,6 +537,8 @@
to implement a proof procedure like the one above. They will be explained
in the next section.
+ (Notice that we applied the goals in reverse order)
+
A variant of @{ML SUBGOAL} is @{ML CSUBGOAL} which allows access to the goal
as @{ML_type cterm} instead of a @{ML_type term}.
*}