--- a/CookBook/Tactical.thy Mon Feb 09 04:18:14 2009 +0000
+++ b/CookBook/Tactical.thy Wed Feb 11 17:40:24 2009 +0000
@@ -21,7 +21,7 @@
text {*
To see how tactics work, let us first transcribe a simple \isacommand{apply}-style proof
- into ML. Consider the following proof.
+ into ML. Suppose the following proof.
*}
lemma disj_swap: "P \<or> Q \<Longrightarrow> Q \<or> P"
@@ -62,18 +62,17 @@
\begin{readmore}
To learn more about the function @{ML Goal.prove} see \isccite{sec:results}
- and the file @{ML_file "Pure/goal.ML"}. For more information about the
- internals of goals see \isccite{sec:tactical-goals}. See @{ML_file
+ and the file @{ML_file "Pure/goal.ML"}. See @{ML_file
"Pure/tactic.ML"} and @{ML_file "Pure/tctical.ML"} for the code of basic
tactics and tactic combinators; see also Chapters 3 and 4 in the old
Isabelle Reference Manual.
\end{readmore}
- Note that we used antiquotations for referencing the theorems. Many theorems
+ Note that in the code above we used 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 there are no ML-binding obtained
the theorem dynamically using the function @{ML thm}; for example
- @{ML "etac (thm \"disjE\") 1"}. Both ways however are considered bad style.
+ @{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
@@ -133,7 +132,7 @@
text {*
This kind of addressing is more difficult to achieve when the goal is
- hard-coded inside the tactic. For every operator that combines tactics
+ hard-coded inside the tactic. For most operators that combine tactics
(@{ML THEN} is only one such operator) a ``primed'' version exists.
The tactics @{ML foo_tac} and @{ML foo_tac'} are very specific for
@@ -175,7 +174,7 @@
The lazy list of possible successor states shows through at the user-level
of Isabelle when using the command \isacommand{back}. For instance in the
- following proof, there are two possibilities for how to apply
+ following proof there are two possibilities for how to apply
@{ML foo_tac'}: either using the first assumption or the second.
*}
@@ -215,7 +214,7 @@
text {*
which prints out the given theorem (using the string-function defined
in Section~\ref{sec:printing}) and then behaves like @{ML all_tac}. We
- are now in the position to inspect every proof state in a proof. Consider
+ are now in the position to inspect every goal state in a proof. Consider
the proof below: on the left-hand side we show the goal state as shown
by Isabelle, on the right-hand side the print out from @{ML my_print_tac}.
*}
@@ -224,48 +223,48 @@
apply(tactic {* my_print_tac @{context} *})
txt{* \small
- \begin{tabular}{@ {}l@ {}p{0.7\textwidth}@ {}}
+ \begin{tabularstar}{\textwidth}{@ {}l@ {\extracolsep{\fill}}l@ {}}
\begin{minipage}[t]{0.3\textwidth}
@{subgoals [display]}
\end{minipage} &
- \hfill@{text "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}
- \end{tabular}
+ @{text "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}
+ \end{tabularstar}
*}
apply(rule conjI)
apply(tactic {* my_print_tac @{context} *})
txt{* \small
- \begin{tabular}{@ {}l@ {}p{0.76\textwidth}@ {}}
+ \begin{tabularstar}{\textwidth}{@ {}l@ {\extracolsep{\fill}}l@ {}}
\begin{minipage}[t]{0.26\textwidth}
@{subgoals [display]}
\end{minipage} &
- \hfill@{text "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> B) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}
- \end{tabular}
+ @{text "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> B) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}
+ \end{tabularstar}
*}
apply(assumption)
apply(tactic {* my_print_tac @{context} *})
txt{* \small
- \begin{tabular}{@ {}l@ {}p{0.7\textwidth}@ {}}
+ \begin{tabularstar}{\textwidth}{@ {}l@ {\extracolsep{\fill}}l@ {}}
\begin{minipage}[t]{0.3\textwidth}
@{subgoals [display]}
\end{minipage} &
- \hfill@{text "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> B) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}
- \end{tabular}
+ @{text "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> B) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}
+ \end{tabularstar}
*}
apply(assumption)
apply(tactic {* my_print_tac @{context} *})
txt{* \small
- \begin{tabular}{@ {}l@ {}p{0.7\textwidth}@ {}}
+ \begin{tabularstar}{\textwidth}{@ {}l@ {\extracolsep{\fill}}l@ {}}
\begin{minipage}[t]{0.3\textwidth}
@{subgoals [display]}
\end{minipage} &
- \hfill@{text "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"}
- \end{tabular}
+ @{text "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"}
+ \end{tabularstar}
*}
done
@@ -277,7 +276,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)"}, and when the proof is finished we are left with @{text "(C)"}.
+ @{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 (in from of an outermost constant
@{text "Const (\"prop\", bool \<Rightarrow> bool)"} applied to each goal;
@@ -285,8 +284,13 @@
prevents that premises of @{text C} are mis-interpreted 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.
+ exception of possibly instantiating schematic variables. If you use
+ the predefined tactics, this will always be the case.
+ \begin{readmore}
+ For more information about the internals of goals see \isccite{sec:tactical-goals}.
+ \end{readmore}
+
*}
section {* Simple Tactics *}
@@ -396,16 +400,33 @@
text {*
Since rules are applied using higher-order unification, an automatic proof
- procedure might become too fragile, if it just applies inference rules shown
- in the fashion above. More constraints can be introduced by
- pre-instantiating theorems with other theorems. You can do this using the
- function @{ML RS}. For example
+ procedure might become too fragile, if it just applies inference rules as
+ shown above. The reason is that a number of rules introduce meta-variables
+ into the goal state. Consider for example the proof
+*}
+
+lemma shows "\<forall>x\<in>A. P x \<Longrightarrow> Q x"
+apply(drule bspec)
+txt{*\begin{minipage}{\textwidth}
+ @{subgoals [display]}
+ \end{minipage}*}
+(*<*)oops(*>*)
+
+text {*
+ where the application of @{text bspec} results into two subgoals involving the
+ meta-variable @{text "?x"}. The point is that if you are not careful, tactics
+ 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 enforced by
+ pre-instantiating theorems with other theorems, for example by using the
+ function @{ML RS}
@{ML_response_fake [display,gray]
"@{thm disjI1} RS @{thm conjI}" "\<lbrakk>?P1; ?Q\<rbrakk> \<Longrightarrow> (?P1 \<or> ?Q1) \<and> ?Q"}
- instantiates the first premise of the @{text conjI}-rule with the
- rule @{text disjI1}. If this is impossible, as in the case of
+ which, for instance, instantiates the first premise of the @{text conjI}-rule
+ with the rule @{text disjI1}. If this is impossible, as in the case of
@{ML_response_fake_both [display,gray]
"@{thm conjI} RS @{thm mp}"
@@ -613,7 +634,7 @@
| _ => all_tac*}
text {*
- In line 3 you need to decend under the outermost @{term "Trueprop"} in order
+ In line 3 you need to descend under the outermost @{term "Trueprop"} in order
to get to the connective you like to analyse. Otherwise goals like @{prop "A \<and> B"}
are not properly analysed. While for the first four pattern we can use the
@{text "@term"}-antiquotation, the pattern in Line 7 cannot be constructed
@@ -621,7 +642,7 @@
quantified variable. So you really have to construct the pattern
using the term-constructors. This is not necessary in other cases, because
their type is always something involving @{typ bool}. The final patter is
- for the case where the goal does not fall into any of the categorories before.
+ for the case where the goal does not fall into any of the categories before.
In this case we chose to just return @{ML all_tac} (i.e., @{ML select_tac}
never fails).
@@ -643,7 +664,7 @@
where in all but the last the tactic applied an introduction rule.
Note that we applied the tactic to subgoals in ``reverse'' order.
This is a trick in order to be independent from what subgoals are
- that are produced by the rule. If we had it applied in the other order
+ that are produced by the rule. If we had applied it in the other order
*}
lemma shows "A \<and> B" and "A \<longrightarrow> B \<longrightarrow>C" and "\<forall>x. D x" and "E \<Longrightarrow> F"
@@ -659,7 +680,7 @@
the ``reverse application'' is easy to implement.
However, this example is very contrived: there are much simpler methods to implement
- such a proof procedure analying a goal according to its topmost
+ such a proof procedure analysing a goal according to its topmost
connective. These simpler methods use tactic combinators which will be explained
in the next section.
*}
@@ -668,7 +689,7 @@
text {*
The purpose of tactic combinators is to build powerful tactics out of
- smaller components. In the previous section we already used @{ML THEN} which
+ smaller components. In the previous section we already used @{ML THEN}, which
strings two tactics together in sequence. For example:
*}
@@ -681,7 +702,7 @@
text {*
If you want to avoid the hard-coded subgoal addressing, then you can use
- the ``primed'' version of @{ML THEN}, namely @{ML THEN'}. For example:
+ the ``primed'' version of @{ML THEN}. For example:
*}
lemma shows "(Foo \<and> Bar) \<and> False"
@@ -698,28 +719,27 @@
If there is a list of tactics that should all be tried out in
sequence, you can use the combinator @{ML EVERY'}. For example
the function @{ML foo_tac'} from page~\ref{tac:footacprime} can also
- be written as
+ be written as:
*}
ML{*val foo_tac'' = EVERY' [etac @{thm disjE}, rtac @{thm disjI2},
atac, rtac @{thm disjI1}, atac]*}
text {*
- There is even another variant for @{ML foo_tac''}: in automatic proof
- procedures (in contrast to tactics that might be called by the user)
- there are often long lists of tactics that are applied to the first
- subgoal. Instead of writing the code above and then calling
- @{ML "foo_tac'' 1"}, you can also just write
+ There is even another way: in automatic proof procedures (in contrast to
+ tactics that might be called by the user) there are often long lists of
+ tactics that are applied to the first subgoal. Instead of writing the code
+ above and then calling @{ML "foo_tac'' 1"}, you can also just write
*}
ML{*val foo_tac1 = EVERY1 [etac @{thm disjE}, rtac @{thm disjI2},
- atac, rtac @{thm disjI1}, atac]*}
+ atac, rtac @{thm disjI1}, atac]*}
text {*
With the combinators @{ML THEN'}, @{ML EVERY'} and @{ML EVERY1} it must be
- guaranteed that all component tactics sucessfully apply; otherwise the
+ guaranteed that all component tactics successfully apply; otherwise the
whole tactic will fail. If you rather want to try out a number of tactics,
- then you can use the combinator @{ML ORELSE'} for two tactics and @{ML FIRST'}
+ then you can use the combinator @{ML ORELSE'} for two tactics, and @{ML FIRST'}
(or @{ML FIRST1}) for a list of tactics. For example, the tactic
*}
@@ -731,8 +751,8 @@
*}
lemma shows "True \<and> False" and "Foo \<or> Bar"
+apply(tactic {* orelse_xmp 2 *})
apply(tactic {* orelse_xmp 1 *})
-apply(tactic {* orelse_xmp 3 *})
txt {* which results in the goal state
\begin{minipage}{\textwidth}
@@ -751,10 +771,10 @@
rtac @{thm notI}, rtac @{thm allI}, K all_tac]*}
text {*
- Since we like to mimic the bahaviour of @{ML select_tac}, we must include
- @{ML all_tac} at the end (@{ML all_tac} must also be ``wrapped up'' using
- the @{ML K}-combinator as it does not take a subgoal number as argument).
- We can test the tactic on the same proof:
+ Since we like to mimic the behaviour of @{ML select_tac} as closely as possible,
+ we must include @{ML all_tac} at the end of the list (@{ML all_tac} must also
+ be ``wrapped up'' using the @{ML K}-combinator, as it does not take a subgoal
+ number as argument). We can test the tactic on the same proof:
*}
lemma shows "A \<and> B" and "A \<longrightarrow> B \<longrightarrow>C" and "\<forall>x. D x" and "E \<Longrightarrow> F"
@@ -768,10 +788,10 @@
(*<*)oops(*>*)
text {*
- and obtain the same subgoals. Since this repeated application of a tactic
- to the reverse order of \emph{all} subgoals is quite common, there is
- the tactics combinator @{ML ALLGOALS} that simplifies this. Using this
- combinator we can simply write: *}
+ Because such repeated applications of a tactic to the reverse order of
+ \emph{all} subgoals is quite common, there is the tactics combinator
+ @{ML ALLGOALS} that simplifies this. Using this combinator we can simply
+ write: *}
lemma shows "A \<and> B" and "A \<longrightarrow> B \<longrightarrow>C" and "\<forall>x. D x" and "E \<Longrightarrow> F"
apply(tactic {* ALLGOALS select_tac' *})
@@ -781,9 +801,9 @@
(*<*)oops(*>*)
text {*
- We chose to write @{ML select_tac'} in such a way that it always succeeds.
- This can be potetially very confusing for the user in cases of goals
- of the form
+ Remember that we chose to write @{ML select_tac'} in such a way that it always
+ succeeds. This can be potentially very confusing for the user, for example,
+ in cases the goals is the form
*}
lemma shows "E \<Longrightarrow> F"
@@ -796,24 +816,131 @@
text {*
where no rule applies. The reason is that the user has little chance
to see whether progress in the proof has been made or not. We could simply
- remove @{ML "K all_tac"} from the end of the list. Then the tactic would
- only apply in cases where it can make some progress. But for the sake of
- argument, let us assume that this is not an option. In such cases, you
+ delete th @{ML "K all_tac"} from the end of the list. Then @{ML select_tac'}
+ would only succeed on goals where it can make progress. But for the sake of
+ argument, let us suppose that this deletion is not an option. In such cases, you
can use the combinator @{ML CHANGED} to make sure the subgoal has been
changed by the tactic. Because now
*}
lemma shows "E \<Longrightarrow> F"
apply(tactic {* CHANGED (select_tac' 1) *})(*<*)?(*>*)
-txt{* results in the usual error message for empty result sequences. *}
-(*<*)oops(*>*)
+txt{* results in the error message:
+ \begin{isabelle}
+ @{text "*** empty result sequence -- proof command failed"}\\
+ @{text "*** At command \"apply\"."}
+ \end{isabelle}
+*}(*<*)oops(*>*)
text {*
+ Meaning the tactic failed.
- @{ML REPEAT} @{ML DETERM}
+ We can extend @{ML select_tac'} so that it not just applies to the top-most
+ connective, but also to the ones immediately ``underneath''. For this you can use the
+ tactic combinator @{ML REPEAT}. For example suppose the following tactic
+*}
+
+ML{*val repeat_xmp = REPEAT (CHANGED (select_tac' 1)) *}
+
+text {* and the proof *}
+
+lemma shows "((\<not>A) \<and> (\<forall>x. B x)) \<and> (C \<longrightarrow> D)"
+apply(tactic {* repeat_xmp *})
+txt{* \begin{minipage}{\textwidth}
+ @{subgoals [display]}
+ \end{minipage} *}
+(*<*)oops(*>*)
+
+text {*
+ Here it is crucial that @{ML select_tac'} is prefixed with @{ML CHANGED},
+ because otherwise @{ML REPEAT} runs into an infinite loop. The function
+ @{ML REPEAT1} is similar, but runs the tactic at least once (failing if
+ this is not possible).
+
+ If you are after the ``primed'' version of @{ML repeat_xmp} then it
+ needs to be coded as
+*}
+
+ML{*val repeat_xmp' = REPEAT o CHANGED o select_tac'*}
+
+text {*
+ since there are no ``primed'' versions of @{ML REPEAT} and @{ML CHANGED}.
+
+ If you look closely at the goal state above, the tactics @{ML repeat_xmp}
+ and @{ML repeat_xmp'} are not yet quite what we are after: the problem is
+ that goals 2 and 3 are not yet analysed. This is because both tactics
+ apply repeatedly only to the first subgoal. To analyse also all
+ resulting subgoals, you can use the function @{ML REPEAT_ALL_NEW}.
+ Suppose the tactic
+*}
+
+ML{*val repeat_all_new_xmp = REPEAT_ALL_NEW (CHANGED o select_tac')*}
+
+text {*
+ which analyses the topmost connectives also in all resulting
+ subgoals.
+*}
+
+lemma shows "((\<not>A) \<and> (\<forall>x. B x)) \<and> (C \<longrightarrow> D)"
+apply(tactic {* repeat_all_new_xmp 1 *})
+txt{* \begin{minipage}{\textwidth}
+ @{subgoals [display]}
+ \end{minipage} *}
+(*<*)oops(*>*)
- @{ML CHANGED}
+text {*
+ The last tactic combinator we describe here is @{ML DETERM}. Recall
+ that tactics produce a lazy sequence of successor goal states. These
+ states can be explored using the command \isacommand{back}. For example
+
+*}
+
+lemma "\<lbrakk>P1 \<or> Q1; P2 \<or> Q2\<rbrakk> \<Longrightarrow> R"
+apply(tactic {* etac @{thm disjE} 1 *})
+txt{* applies the rule to the first assumption
+
+ \begin{minipage}{\textwidth}
+ @{subgoals [display]}
+ \end{minipage} *}
+(*<*)
+oops
+lemma "\<lbrakk>P1 \<or> Q1; P2 \<or> Q2\<rbrakk> \<Longrightarrow> R"
+apply(tactic {* etac @{thm disjE} 1 *})
+(*>*)
+back
+txt{* whereas it is now applied to the second
+
+ \begin{minipage}{\textwidth}
+ @{subgoals [display]}
+ \end{minipage} *}
+(*<*)oops(*>*)
+
+text {*
+ Sometimes this leads to confusing behaviour of tactics and also has
+ the potential to explode the search space for tactics build on top.
+ This can be avoided by prefixing the tactic with @{ML DETERM}.
+*}
+
+lemma "\<lbrakk>P1 \<or> Q1; P2 \<or> Q2\<rbrakk> \<Longrightarrow> R"
+apply(tactic {* DETERM (etac @{thm disjE} 1) *})
+txt {*\begin{minipage}{\textwidth}
+ @{subgoals [display]}
+ \end{minipage} *}
+(*<*)oops(*>*)
+text {*
+ This will prune the search space to just the first possibility.
+ Attempting to apply \isacommand{back} in this goal states gives the
+ error message:
+
+ \begin{isabelle}
+ @{text "*** back: no alternatives"}\\
+ @{text "*** At command \"back\"."}
+ \end{isabelle}
+
+ \begin{readmore}
+ Most tactic combinators are defined in @{ML_file "Pure/tctical.ML"}.
+ \end{readmore}
*}