--- a/CookBook/Tactical.thy Mon Feb 09 01:23:35 2009 +0000
+++ b/CookBook/Tactical.thy Mon Feb 09 04:18:14 2009 +0000
@@ -72,8 +72,9 @@
Note that 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 theorem @{ML thm}; for example @{ML "etac
- (thm \"disjE\") 1"}. Both ways however are considered bad style. The reason
+ the theorem dynamically using the function @{ML thm}; for example
+ @{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
@@ -108,7 +109,7 @@
has a hard-coded number that stands for the subgoal analysed by the
tactic (@{text "1"} stands for the first, or top-most, subgoal). This hard-coding
of goals is sometimes wanted, but usually it is not. To avoid the explicit numbering,
- you can write
+ you can write\label{tac:footacprime}
*}
ML{*val foo_tac' =
@@ -151,7 +152,9 @@
@{text [display, gray] "type tactic = thm -> thm Seq.seq"}
It is custom that if a tactic fails, it should return the empty sequence:
- therefore your own tactics should not raise exceptions willy-nilly.
+ therefore your own tactics should not raise exceptions willy-nilly. Only
+ in very grave failure situations should a tactic raise the exception
+ @{text THM}.
The simplest tactics are @{ML no_tac} and @{ML all_tac}. The first returns
the empty sequence and is defined as
@@ -161,19 +164,19 @@
text {*
which means @{ML no_tac} always fails. The second returns the given theorem wrapped
- as a single member sequence. It is defined as
+ as a single member sequence; @{ML all_tac} is defined as
*}
ML{*fun all_tac thm = Seq.single thm*}
text {*
- which means @{ML all_tac} always succeeds (but also does not make any progress
+ which means it always succeeds (but also does not make any progress
with the proof).
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
- @{ML foo_tac'}.
+ @{ML foo_tac'}: either using the first assumption or the second.
*}
lemma "\<lbrakk>P \<or> Q; P \<or> Q\<rbrakk> \<Longrightarrow> Q \<or> P"
@@ -184,9 +187,8 @@
text {*
By using \isacommand{back}, we construct the proof that uses the
- second assumption. In more interesting situations, different possibilities
- can lead to different proofs and even often need to be explored when
- a first proof attempt is unsuccessful.
+ second assumption. In more interesting situations, only by exploring
+ different possibilities one might be able to find a proof.
\begin{readmore}
See @{ML_file "Pure/General/seq.ML"} for the implementation of lazy
@@ -213,9 +215,9 @@
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
- now can inspect every proof 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}.
+ are now in the position to inspect every proof 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}.
*}
lemma shows "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"
@@ -275,11 +277,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)"}. Since the goal @{term C} can potentially be an implication,
+ @{text "C \<Longrightarrow> (C)"}, and 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;
however this constant is invisible in the print out above). This
- prevents that premises of @{text C} are misinterpreted as open subgoals.
+ 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.
@@ -289,12 +292,18 @@
section {* Simple Tactics *}
text {*
- A simple tactic is @{ML print_tac}, which is useful for low-level debugging of tactics.
+ A simple tactic is @{ML print_tac}, which is quite useful for low-level debugging of tactics.
It just prints out a message and the current goal state.
*}
lemma shows "False \<Longrightarrow> True"
apply(tactic {* print_tac "foo message" *})
+txt{*\begin{minipage}{\textwidth}\small
+ @{text "foo message"}\\[3mm]
+ @{prop "False \<Longrightarrow> True"}\\
+ @{text " 1. False \<Longrightarrow> True"}\\
+ \end{minipage}
+ *}
(*<*)oops(*>*)
text {*
@@ -338,7 +347,7 @@
text {*
As mentioned in the previous section, most basic tactics take a number as
argument, which addresses the subgoal they are analysing. In the proof below,
- we first break up the second subgoal by focusing on this subgoal first.
+ we first analyse the second subgoal by focusing on this subgoal first.
*}
lemma shows "Foo" and "P \<and> Q"
@@ -374,8 +383,18 @@
Similarly versions exists for @{ML atac} (@{ML assume_tac}), @{ML etac}
(@{ML eresolve_tac}) and so on.
- (FIXME: @{ML cut_facts_tac})
+ Another simple tactic is @{ML cut_facts_tac}. It inserts a list of theorems
+ into the assumptions of the current goal state. For example:
+*}
+lemma shows "True \<noteq> False"
+apply(tactic {* cut_facts_tac [@{thm True_def}, @{thm False_def}] 1 *})
+txt{*\begin{minipage}{\textwidth}
+ @{subgoals [display]}
+ \end{minipage}*}
+(*<*)oops(*>*)
+
+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
@@ -386,9 +405,19 @@
"@{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}. The function @{ML RSN} is similar, but
- takes a number and makes explicit which premise should be instantiated.
- To improve readability we are going use the following function
+ rule @{text disjI1}. If this is impossible, as in the case of
+
+ @{ML_response_fake_both [display,gray]
+ "@{thm conjI} RS @{thm mp}"
+"*** Exception- THM (\"RSN: no unifiers\", 1,
+[\"\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q\", \"\<lbrakk>?P \<longrightarrow> ?Q; ?P\<rbrakk> \<Longrightarrow> ?Q\"]) raised"}
+
+ the function raises an exception. The function @{ML RSN} is similar, but
+ takes a number as argument and thus you can make explicit which premise
+ should be instantiated.
+
+ To improve readability of the theorems we produce below, we shall use
+ the following function
*}
ML{*fun no_vars ctxt thm =
@@ -399,23 +428,23 @@
end*}
text {*
- to transform the schematic variables of a theorem into free variables.
- This means for the @{ML RS}-expression above:
+ that transform the schematic variables of a theorem into free variables.
+ This means for the first @{ML RS}-expression above:
@{ML_response_fake [display,gray]
"no_vars @{context} (@{thm disjI1} RS @{thm conjI})" "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> (P \<or> Qa) \<and> Q"}
- If you want to instantiate more than one premise, you can use the function
- @{ML MRS}:
+ If you want to instantiate more than one premise of a theorem, you can use
+ the function @{ML MRS}:
@{ML_response_fake [display,gray]
"no_vars @{context} ([@{thm disjI1}, @{thm disjI2}] MRS @{thm conjI})"
"\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> (P \<or> Qa) \<and> (Pa \<or> Q)"}
If you need to instantiate lists of theorems, you can use the
- functions @{ML RL} and @{ML MRL}. For example below every
- theorem in the first list is instantiated against every theorem
- in the second.
+ functions @{ML RL} and @{ML MRL}. For example in the code below
+ every theorem in the first list is instantiated against every
+ theorem in the second.
@{ML_response_fake [display,gray]
"[@{thm impI}, @{thm disjI2}] RL [@{thm conjI}, @{thm disjI1}]"
@@ -472,7 +501,7 @@
apply(tactic {* SUBPROOF sp_tac @{context} 1 *})?
txt {*
- which yields the printout:
+ which gives the printout:
\begin{quote}\small
\begin{tabular}{ll}
@@ -504,7 +533,7 @@
apply(tactic {* SUBPROOF sp_tac @{context} 1 *})?
txt {*
- then @{ML SUBPROOF} prints out
+ then @{ML sp_tac} prints out
\begin{quote}\small
\begin{tabular}{ll}
@@ -528,15 +557,20 @@
*}
ML{*val atac' = SUBPROOF (fn {prems, ...} => resolve_tac prems 1)*}
+
+text {*
+ If we apply it to the next lemma
+*}
+
lemma shows "\<And>x y. \<lbrakk>B x y; A x y; C x y\<rbrakk> \<Longrightarrow> A x y"
apply(tactic {* atac' @{context} 1 *})
-txt{* yields
+txt{* we get
@{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
+ 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 instantiation of schematic variables can affect
several goals and can render them unprovable. @{ML SUBPROOF} is meant
@@ -547,7 +581,7 @@
the \isacommand{apply}-step uses @{text "1"}. Another advantage
of @{ML SUBGOAL} is that the addressing inside it is completely
local to the subproof inside. It is therefore possible to also apply
- @{ML atac'} to the second goal:
+ @{ML atac'} to the second goal by just writing:
*}
lemma shows "True" and "\<And>x y. \<lbrakk>B x y; A x y; C x y\<rbrakk> \<Longrightarrow> A x y"
@@ -563,9 +597,10 @@
\end{readmore}
A similar but less powerful function than @{ML SUBPROOF} is @{ML SUBGOAL}.
- It allows you to inspect a specified subgoal. With this you can implement
- a tactic that applies a rule according to its topmost connective (we only
- analyse a few connectives). The tactic is as follows:
+ It allows you to inspect a given subgoal. With this you can implement
+ a tactic that applies a rule according to the topmost connective in the
+ subgoal (to illustrate this we only analyse a few connectives). The code
+ of this tactic is as follows.\label{tac:selecttac}
*}
ML %linenumbers{*fun select_tac (t,i) =
@@ -579,15 +614,18 @@
text {*
In line 3 you need to decend under the outermost @{term "Trueprop"} in order
- to get to the connective you like to analyse. Otherwise goals @{prop "A \<and> B"}
- are not bropek up. In line 7, the pattern cannot be constructed using the
- @{text "@term"}-antiquotation, because that would fix the type of the
- quantified variable. In this case you really have to construct the pattern
- by using the term-constructors. The other cases work, because their type
- is always bool. In case that the goal does not fall into any of the categorories,
- then we chose to just return @{ML all_tac} (i.e., the tactic never fails).
+ 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
+ in this way. The reason is that an antiquotation would fix the type of the
+ 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.
+ In this case we chose to just return @{ML all_tac} (i.e., @{ML select_tac}
+ never fails).
- Let us now see how to apply this tactic.
+ Let us now see how to apply this tactic. Consider the four goals:
*}
@@ -596,13 +634,16 @@
apply(tactic {* SUBGOAL select_tac 3 *})
apply(tactic {* SUBGOAL select_tac 2 *})
apply(tactic {* SUBGOAL select_tac 1 *})
-txt{* @{subgoals [display]} *}
+txt{* \begin{minipage}{\textwidth}
+ @{subgoals [display]}
+ \end{minipage} *}
(*<*)oops(*>*)
text {*
- Note that we applied it in ``reverse'' order. This is a trick in
- order to be independent from what subgoals the rule produced. If we had
- it applied in the other order
+ 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
*}
lemma shows "A \<and> B" and "A \<longrightarrow> B \<longrightarrow>C" and "\<forall>x. D x" and "E \<Longrightarrow> F"
@@ -614,20 +655,21 @@
text {*
then we have to be careful to not apply the tactic to the two subgoals the
- first goal produced. This can be messy in an automated proof script. The
- reverse application, on the other hand, is easy to implement.
+ first goal produced. To do this can result in quite messy code. In contrast,
+ the ``reverse application'' is easy to implement.
- However, this example is contrived: there are much simpler ways to implement
- such proof procedure that analyses a goal according to its topmost
- connective. They will be explained in the next section.
+ However, this example is very contrived: there are much simpler methods to implement
+ such a proof procedure analying a goal according to its topmost
+ connective. These simpler methods use tactic combinators which will be explained
+ in the next section.
*}
section {* Tactic Combinators *}
text {*
- To be able to implement powerful tactics out of smaller component tactics,
- Isabelle provides tactic combinators. In the previous section we already
- used @{ML THEN} which strings two tactics together in sequence. For example:
+ The purpose of tactic combinators is to build powerful tactics out of
+ smaller components. In the previous section we already used @{ML THEN} which
+ strings two tactics together in sequence. For example:
*}
lemma shows "(Foo \<and> Bar) \<and> False"
@@ -639,7 +681,7 @@
text {*
If you want to avoid the hard-coded subgoal addressing, then you can use
- @{ML THEN'}. For example:
+ the ``primed'' version of @{ML THEN}, namely @{ML THEN'}. For example:
*}
lemma shows "(Foo \<and> Bar) \<and> False"
@@ -650,35 +692,129 @@
(*<*)oops(*>*)
text {*
- For most tactic combinators such a ``primed'' version exists.
- In what follows we will, whenever appropriate, prefer the primed version of
- the tactic combinator and omit to mention the simple one.
+ For most tactic combinators such a ``primed'' version exists and
+ in what follows we will usually prefer it over the ``unprimed'' one.
+
+ 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
+*}
+
+ML{*val foo_tac'' = EVERY' [etac @{thm disjE}, rtac @{thm disjI2},
+ atac, rtac @{thm disjI1}, atac]*}
- With @{ML THEN} and @{ML THEN'} it must be guaranteed that both tactics
- sucessfully apply; otherwise the whole tactic will fail. If you want to
- try out either one tactic, then you can use @{ML ORELSE'}. For
- example
+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
+*}
+
+ML{*val foo_tac1 = EVERY1 [etac @{thm disjE}, rtac @{thm disjI2},
+ 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
+ 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'}
+ (or @{ML FIRST1}) for a list of tactics. For example, the tactic
*}
ML{*val orelse_xmp = (rtac @{thm disjI1} ORELSE' rtac @{thm conjI})*}
text {*
- will first try out rule @{text disjI} and after that @{text conjI}.
+ will first try out whether rule @{text disjI} applies and after that
+ whether @{text conjI}. To see this consider the proof:
*}
lemma shows "True \<and> False" and "Foo \<or> Bar"
apply(tactic {* orelse_xmp 1 *})
apply(tactic {* orelse_xmp 3 *})
-txt {* @{subgoals [display]} *}
+txt {* which results in the goal state
+
+ \begin{minipage}{\textwidth}
+ @{subgoals [display]}
+ \end{minipage}
+*}
(*<*)oops(*>*)
text {*
- applies
+ Using @{ML FIRST'} we can write our @{ML select_tac} from Page~\ref{tac:selecttac}
+ simply as follows:
+*}
+
+ML{*val select_tac' = FIRST' [rtac @{thm conjI}, rtac @{thm impI},
+ 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:
+*}
+
+lemma shows "A \<and> B" and "A \<longrightarrow> B \<longrightarrow>C" and "\<forall>x. D x" and "E \<Longrightarrow> F"
+apply(tactic {* select_tac' 4 *})
+apply(tactic {* select_tac' 3 *})
+apply(tactic {* select_tac' 2 *})
+apply(tactic {* select_tac' 1 *})
+txt{* \begin{minipage}{\textwidth}
+ @{subgoals [display]}
+ \end{minipage} *}
+(*<*)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: *}
+
+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' *})
+txt{* \begin{minipage}{\textwidth}
+ @{subgoals [display]}
+ \end{minipage} *}
+(*<*)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
+*}
+
+lemma shows "E \<Longrightarrow> F"
+apply(tactic {* select_tac' 1 *})
+txt{* \begin{minipage}{\textwidth}
+ @{subgoals [display]}
+ \end{minipage} *}
+(*<*)oops(*>*)
+
+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
+ 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(*>*)
+text {*
+
@{ML REPEAT} @{ML DETERM}
+ @{ML CHANGED}
+
*}
section {* Rewriting and Simplifier Tactics *}