--- a/CookBook/Tactical.thy Wed Feb 11 17:40:24 2009 +0000
+++ b/CookBook/Tactical.thy Thu Feb 12 14:15:50 2009 +0000
@@ -72,7 +72,7 @@
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!
+ \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
@@ -121,7 +121,7 @@
text {*
and then give the number for the subgoal explicitly when the tactic is
called. So in the next proof you can first discharge the second subgoal, and
- after that the first.
+ subsequently the first.
*}
lemma "P1 \<or> Q1 \<Longrightarrow> Q1 \<or> P1"
@@ -137,23 +137,25 @@
The tactics @{ML foo_tac} and @{ML foo_tac'} are very specific for
analysing goals being only of the form @{prop "P \<or> Q \<Longrightarrow> Q \<or> P"}. If the goal is not
- of this form, then they throw the error message:
+ of this form, then they return the error message:
\begin{isabelle}
@{text "*** empty result sequence -- proof command failed"}\\
@{text "*** At command \"apply\"."}
\end{isabelle}
- Meaning the tactics failed. The reason for this error message is that tactics
- are functions that map a goal state to a (lazy) sequence of successor states,
- hence the type of a tactic is:
+ This means the tactics failed. 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:
+*}
- @{text [display, gray] "type tactic = thm -> thm Seq.seq"}
+ML{*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. Only
- in very grave failure situations should a tactic raise the exception
- @{text THM}.
+text {*
+ By convention, if a tactic fails, then it should return the empty sequence.
+ Therefore, if you write your own tactics, they 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
@@ -163,16 +165,16 @@
text {*
which means @{ML no_tac} always fails. The second returns the given theorem wrapped
- as a single member sequence; @{ML all_tac} is defined as
+ up in a single member sequence; it is defined as
*}
ML{*fun all_tac thm = Seq.single thm*}
text {*
- which means it always succeeds (but also does not make any progress
- with the proof).
+ which means @{ML all_tac} 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
+ The lazy list of possible successor goal 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'}: either using the first assumption or the second.
@@ -186,18 +188,19 @@
text {*
By using \isacommand{back}, we construct the proof that uses the
- second assumption. In more interesting situations, only by exploring
- different possibilities one might be able to find a proof.
+ second assumption. While in the proof above, it does not really matter which
+ assumption is used, in more interesting cases provability might depend
+ on exploring different possibilities.
\begin{readmore}
See @{ML_file "Pure/General/seq.ML"} for the implementation of lazy
- sequences. However in day-to-day Isabelle programming, one rarely
- constructs sequences explicitly, but uses the predefined functions
- instead.
+ sequences. In day-to-day Isabelle programming, however, one rarely
+ constructs sequences explicitly, but uses the predefined tactics and
+ tactic combinators instead.
\end{readmore}
It might be surprising that tactics, which transform
- one proof state to the next, are functions from theorems to theorem
+ one goal state to the next, are functions from theorems to theorem
(sequences). The surprise resolves by knowing that every
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
@@ -211,81 +214,104 @@
Seq.single thm
end*}
-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 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}.
+text_raw {*
+ \begin{figure}[p]
+ \begin{isabelle}
*}
-
lemma shows "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"
apply(tactic {* my_print_tac @{context} *})
-txt{* \small
- \begin{tabularstar}{\textwidth}{@ {}l@ {\extracolsep{\fill}}l@ {}}
- \begin{minipage}[t]{0.3\textwidth}
+txt{* \begin{minipage}{\textwidth}
@{subgoals [display]}
- \end{minipage} &
+ \end{minipage}\medskip
+
+ \begin{minipage}{\textwidth}
+ \small\colorbox{gray!20}{
+ \begin{tabular}{@ {}l@ {}}
+ internal goal state:\\
@{text "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}
- \end{tabularstar}
+ \end{tabular}}
+ \end{minipage}\medskip
*}
apply(rule conjI)
apply(tactic {* my_print_tac @{context} *})
-txt{* \small
- \begin{tabularstar}{\textwidth}{@ {}l@ {\extracolsep{\fill}}l@ {}}
- \begin{minipage}[t]{0.26\textwidth}
+txt{* \begin{minipage}{\textwidth}
@{subgoals [display]}
- \end{minipage} &
+ \end{minipage}\medskip
+
+ \begin{minipage}{\textwidth}
+ \small\colorbox{gray!20}{
+ \begin{tabular}{@ {}l@ {}}
+ internal goal state:\\
@{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}
+ \end{tabular}}
+ \end{minipage}\medskip
*}
apply(assumption)
apply(tactic {* my_print_tac @{context} *})
-txt{* \small
- \begin{tabularstar}{\textwidth}{@ {}l@ {\extracolsep{\fill}}l@ {}}
- \begin{minipage}[t]{0.3\textwidth}
+txt{* \begin{minipage}{\textwidth}
@{subgoals [display]}
- \end{minipage} &
+ \end{minipage}\medskip
+
+ \begin{minipage}{\textwidth}
+ \small\colorbox{gray!20}{
+ \begin{tabular}{@ {}l@ {}}
+ internal goal state:\\
@{text "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> B) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}
- \end{tabularstar}
+ \end{tabular}}
+ \end{minipage}\medskip
*}
apply(assumption)
apply(tactic {* my_print_tac @{context} *})
-txt{* \small
- \begin{tabularstar}{\textwidth}{@ {}l@ {\extracolsep{\fill}}l@ {}}
- \begin{minipage}[t]{0.3\textwidth}
+txt{* \begin{minipage}{\textwidth}
@{subgoals [display]}
- \end{minipage} &
+ \end{minipage}\medskip
+
+ \begin{minipage}{\textwidth}
+ \small\colorbox{gray!20}{
+ \begin{tabular}{@ {}l@ {}}
+ internal goal state:\\
@{text "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"}
- \end{tabularstar}
+ \end{tabular}}
+ \end{minipage}\medskip
+ *}
+done
+text_raw {*
+ \end{isabelle}
+ \caption{A proof where we show the goal state as printed
+ by the Isabelle system and as represented internally
+ (highlighted boxes).\label{fig:goalstates}}
+ \end{figure}
*}
-done
text {*
- As can be seen, internally every goal state is an implication of the form
+ 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
+ tactic we are in the position to inspect every goal state in a
+ proof. Consider now the proof in Figure~\ref{fig:goalstates}: as can be seen,
+ internally every goal state is an implication of the form
@{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. 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 (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 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. If you use
- the predefined tactics, this will always be the case.
+ 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 (in from of an outermost constant @{text
+ "Const (\"prop\", bool \<Rightarrow> bool)"} applied to each goal; however this constant
+ is invisible in the figure). This 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. If you use the predefined tactics, which we describe in the next
+ section, this will always be the case.
\begin{readmore}
For more information about the internals of goals see \isccite{sec:tactical-goals}.
@@ -296,13 +322,16 @@
section {* Simple Tactics *}
text {*
- 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.
+ Let us start with the tactic @{ML print_tac}, which is quite useful for low-level
+ debugging of tactics. It just prints out a message and the current goal state.
+ Processing the proof
*}
lemma shows "False \<Longrightarrow> True"
apply(tactic {* print_tac "foo message" *})
-txt{*\begin{minipage}{\textwidth}\small
+txt{*gives:\medskip
+
+ \begin{minipage}{\textwidth}\small
@{text "foo message"}\\[3mm]
@{prop "False \<Longrightarrow> True"}\\
@{text " 1. False \<Longrightarrow> True"}\\
@@ -317,14 +346,16 @@
lemma shows "P \<Longrightarrow> P"
apply(tactic {* atac 1 *})
-done
+txt{*\begin{minipage}{\textwidth}
+ @{subgoals [display]}
+ \end{minipage}*}
+(*<*)oops(*>*)
text {*
Similarly, @{ML rtac}, @{ML dtac}, @{ML etac} and @{ML ftac} correspond
to @{text rule}, @{text drule}, @{text erule} and @{text frule},
- 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.
+ respectively. Each of them takes a theorem as argument and attempts to
+ apply it to a goal. Below are three self-explanatory examples.
*}
lemma shows "P \<and> Q"
@@ -349,9 +380,10 @@
(*<*)oops(*>*)
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 analyse the second subgoal by focusing on this subgoal first.
+ Note the number in each tactic call. Also as mentioned in the previous section, most
+ basic tactics take such an argument; it addresses the subgoal they are analysing.
+ In the proof below, we first split up the conjunction in the second subgoal by
+ focusing on this subgoal first.
*}
lemma shows "Foo" and "P \<and> Q"
@@ -361,7 +393,9 @@
\end{minipage}*}
(*<*)oops(*>*)
-text {*
+text {*
+ (FIXME: is it important to get the number of subgoals?)
+
The function @{ML resolve_tac} is similar to @{ML rtac}, except that it
expects a list of theorems as arguments. From this list it will apply the
first applicable theorem (later theorems that are also applicable can be
@@ -384,16 +418,19 @@
(*<*)oops(*>*)
text {*
- Similarly versions exists for @{ML atac} (@{ML assume_tac}), @{ML etac}
- (@{ML eresolve_tac}) and so on.
+ Similarly versions taking a list of theorems exist for the tactics
+ @{ML dtac} (@{ML dresolve_tac}), @{ML etac} (@{ML eresolve_tac}) and so on.
+
Another simple tactic is @{ML cut_facts_tac}. It inserts a list of theorems
- into the assumptions of the current goal state. For example:
+ 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}
+txt{*produces the goal state\medskip
+
+ \begin{minipage}{\textwidth}
@{subgoals [display]}
\end{minipage}*}
(*<*)oops(*>*)
@@ -413,28 +450,29 @@
(*<*)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
+ where the application of Rule @{text bspec} generates two subgoals involving the
+ meta-variable @{text "?x"}. Now, 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}
+ constraint 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}
@{ML_response_fake [display,gray]
"@{thm disjI1} RS @{thm conjI}" "\<lbrakk>?P1; ?Q\<rbrakk> \<Longrightarrow> (?P1 \<or> ?Q1) \<and> ?Q"}
- 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
+ which in the example instantiates the first premise of the @{text conjI}-rule
+ with the rule @{text disjI1}. If the instantiation 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
+ then the function raises an exception. The function @{ML RSN} is similar to @{ML RS}, but
+ takes an additional number as argument that makes explicit which premise
should be instantiated.
To improve readability of the theorems we produce below, we shall use
@@ -449,8 +487,9 @@
end*}
text {*
- that transform the schematic variables of a theorem into free variables.
- This means for the first @{ML RS}-expression above:
+ that transform the schematic variables of a theorem into free variables.
+ Using this function for the first @{ML RS}-expression above would produce
+ the more readable result:
@{ML_response_fake [display,gray]
"no_vars @{context} (@{thm disjI1} RS @{thm conjI})" "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> (P \<or> Qa) \<and> Q"}
@@ -463,9 +502,9 @@
"\<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 in the code 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 second list is instantiated with every
+ theorem in the first.
@{ML_response_fake [display,gray]
"[@{thm impI}, @{thm disjI2}] RL [@{thm conjI}, @{thm disjI1}]"
@@ -478,15 +517,15 @@
The combinators for instantiating theorems are defined in @{ML_file "Pure/drule.ML"}.
\end{readmore}
- 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
+ Often proofs on the ML-level involve elaborate operations on assumptions and
+ @{text "\<And>"}-quantified variables. To do such operations 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.
+ 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 as argument and just prints out the content of this record (using the
- string transformation functions defined in Section~\ref{sec:printing}). Consider
- now the proof
+ takes a record and just prints out the content of this record (using the
+ string transformation functions from in Section~\ref{sec:printing}). Consider
+ now the proof:
*}
text_raw{*
@@ -522,7 +561,7 @@
apply(tactic {* SUBPROOF sp_tac @{context} 1 *})?
txt {*
- which gives the printout:
+ The tactic produces the following printout:
\begin{quote}\small
\begin{tabular}{ll}
@@ -536,16 +575,18 @@
Note in the actual output the brown colour of the variables @{term x} and
@{term y}. Although they are parameters in the original goal, they are fixed inside
- the subproof. Similarly the schematic variable @{term z}. The assumption
+ the subproof. By convention these fixed variables are printed in brown colour.
+ Similarly the schematic variable @{term z}. The assumption, or premise,
@{prop "A x y"} is bound as @{ML_type cterm} to the record-variable
- @{text asms} but also as @{ML_type thm} to @{text prems}.
+ @{text asms}, but also 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 an error message.
+ Notice also that we had to append @{text [quotes] "?"} to the
+ \isacommand{apply}-command. 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 an
+ ``empty sequence'' error message.
If we continue the proof script by applying the @{text impI}-rule
*}
@@ -554,7 +595,7 @@
apply(tactic {* SUBPROOF sp_tac @{context} 1 *})?
txt {*
- then @{ML sp_tac} prints out
+ then tactic prints out
\begin{quote}\small
\begin{tabular}{ll}
@@ -569,43 +610,44 @@
(*<*)oops(*>*)
text {*
- where we now also have @{term "B y x"} as an assumption.
+ Now also @{term "B y x"} is an assumption bound to @{text asms} and @{text prems}.
One convenience of @{ML SUBPROOF} is that we can apply the assumptions
using the usual tactics, because the parameter @{text prems}
- contains them as theorems. With this we can easily
- implement a tactic that almost behaves like @{ML atac}, namely:
+ contains them as theorems. With this you can easily
+ implement a tactic that behaves almost like @{ML atac}:
*}
ML{*val atac' = SUBPROOF (fn {prems, ...} => resolve_tac prems 1)*}
text {*
- If we apply it to the next lemma
+ If you apply @{ML atac'} to the next lemma
*}
-lemma shows "\<And>x y. \<lbrakk>B x y; A x y; C x y\<rbrakk> \<Longrightarrow> A x y"
+lemma shows "\<lbrakk>B x y; A x y; C x y\<rbrakk> \<Longrightarrow> A x y"
apply(tactic {* atac' @{context} 1 *})
-txt{* we get
+txt{* it will produce
@{subgoals [display]} *}
(*<*)oops(*>*)
text {*
- The restriction in this tactic is that it cannot instantiate any
+ 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 instantiation of schematic variables can affect
+ 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'} 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 subproof inside. It is therefore possible to also apply
+ 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 "\<And>x y. \<lbrakk>B x y; A x y; C x y\<rbrakk> \<Longrightarrow> A x y"
+lemma shows "True" and "\<lbrakk>B x y; A x y; C x y\<rbrakk> \<Longrightarrow> A x y"
apply(tactic {* atac' @{context} 2 *})
apply(rule TrueI)
done
@@ -619,14 +661,15 @@
A similar but less powerful function than @{ML SUBPROOF} is @{ML SUBGOAL}.
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
+ a tactic that applies a rule according to the topmost logic connective in the
subgoal (to illustrate this we only analyse a few connectives). The code
- of this tactic is as follows.\label{tac:selecttac}
+ of the tactic is as follows.\label{tac:selecttac}
*}
ML %linenumbers{*fun select_tac (t,i) =
case t of
@{term "Trueprop"} $ t' => select_tac (t',i)
+ | @{term "op \<Longrightarrow>"} $ _ $ t' => select_tac (t',i)
| @{term "op \<and>"} $ _ $ _ => rtac @{thm conjI} i
| @{term "op \<longrightarrow>"} $ _ $ _ => rtac @{thm impI} i
| @{term "Not"} $ _ => rtac @{thm notI} i
@@ -634,17 +677,19 @@
| _ => all_tac*}
text {*
- 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
- 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 categories before.
- In this case we chose to just return @{ML all_tac} (i.e., @{ML select_tac}
- never fails).
+ The input of the function is a term representing the subgoal and a number
+ specifying the subgoal of interest. 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. Similarly with meta-implications in the next line. While for the
+ first five patterns we can use the @{text "@term"}-antiquotation to
+ construct the patterns, the pattern in Line 8 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
+ basic term-constructors. This is not necessary in other cases, because their type
+ is always fixed to function types involving only the type @{typ bool}. The
+ final pattern, we chose to just return @{ML all_tac}. Consequently,
+ @{ML select_tac} never fails.
Let us now see how to apply this tactic. Consider the four goals:
*}
@@ -662,9 +707,9 @@
text {*
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 applied it in the other order
+ Note that we applied the tactic to the goals in ``reverse'' order.
+ This is a trick in order to be independent from the subgoals 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"
@@ -675,22 +720,22 @@
(*<*)oops(*>*)
text {*
- then we have to be careful to not apply the tactic to the two subgoals the
- first goal produced. To do this can result in quite messy code. In contrast,
+ then we have to be careful to not apply the tactic to the two subgoals produced by
+ the first goal. To do this can result in quite messy code. In contrast,
the ``reverse application'' is easy to implement.
- However, this example is very contrived: there are much simpler methods to implement
- such a proof procedure analysing a goal according to its topmost
- connective. These simpler methods use tactic combinators which will be explained
+ Of course, this example is contrived: there are much simpler methods available in
+ Isabelle for implementing a proof procedure analysing a goal according to its topmost
+ connective. These simpler methods use tactic combinators, which we will explain
in the next section.
*}
section {* Tactic Combinators *}
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
- strings two tactics together in sequence. For example:
+ The purpose of tactic combinators is to build compound tactics out of
+ smaller tactics. In the previous section we already used @{ML THEN}, which
+ just strings together two tactics in a sequence. For example:
*}
lemma shows "(Foo \<and> Bar) \<and> False"
@@ -713,12 +758,14 @@
(*<*)oops(*>*)
text {*
+ Here you only have to specify the subgoal of interest only once and
+ it is consistently applied to the component tactics.
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
+ the function @{ML foo_tac'} from page~\pageref{tac:footacprime} can also
be written as:
*}
@@ -726,28 +773,32 @@
atac, rtac @{thm disjI1}, atac]*}
text {*
- 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
+ There is even another way of implementing this tactic: 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 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'}
- (or @{ML FIRST1}) for a list of tactics. For example, the tactic
+ and just call @{ML foo_tac1}.
+
+ With the combinators @{ML THEN'}, @{ML EVERY'} and @{ML EVERY1} it must be
+ 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'} (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 whether rule @{text disjI} applies and after that
- whether @{text conjI}. To see this consider the proof:
+ @{text conjI}. To see this consider the proof
*}
lemma shows "True \<and> False" and "Foo \<or> Bar"
@@ -763,8 +814,8 @@
text {*
- Using @{ML FIRST'} we can write our @{ML select_tac} from Page~\ref{tac:selecttac}
- simply as follows:
+ Using @{ML FIRST'} we can simplify our @{ML select_tac} from Page~\pageref{tac:selecttac}
+ as follows:
*}
ML{*val select_tac' = FIRST' [rtac @{thm conjI}, rtac @{thm impI},
@@ -772,9 +823,10 @@
text {*
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:
+ we must include @{ML all_tac} at the end of the list, otherwise the tactic will
+ fail if no rule applies (we laso have to wrap @{ML all_tac} using the
+ @{ML K}-combinator, because it does not take a subgoal number as argument). You can
+ test the tactic on the same goals:
*}
lemma shows "A \<and> B" and "A \<longrightarrow> B \<longrightarrow>C" and "\<forall>x. D x" and "E \<Longrightarrow> F"
@@ -788,9 +840,9 @@
(*<*)oops(*>*)
text {*
- 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
+ Since such repeated applications of a tactic to the reverse order of
+ \emph{all} subgoals is quite common, there is the tactic combinator
+ @{ML ALLGOALS} that simplifies this. Using this combinator you can simply
write: *}
lemma shows "A \<and> B" and "A \<longrightarrow> B \<longrightarrow>C" and "\<forall>x. D x" and "E \<Longrightarrow> F"
@@ -801,9 +853,9 @@
(*<*)oops(*>*)
text {*
- 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
+ Remember that we chose to implement @{ML select_tac'} so that it
+ always succeeds. This can be potentially very confusing for the user,
+ for example, in cases where the goal is the form
*}
lemma shows "E \<Longrightarrow> F"
@@ -814,18 +866,22 @@
(*<*)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
- 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
+ In this case no rule applies. The problem for the user is that there is little
+ chance to see whether or not progress in the proof has been made. By convention
+ therefore, tactics visible to the user should either change something or fail.
+
+ To comply with this convention, we could simply delete the @{ML "K all_tac"}
+ from the end of the theorem list. As a result @{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 \emph{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 error message:
+txt{* gives the error message:
\begin{isabelle}
@{text "*** empty result sequence -- proof command failed"}\\
@{text "*** At command \"apply\"."}
@@ -834,32 +890,34 @@
text {*
- Meaning the tactic failed.
-
- 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
+ We can further extend @{ML select_tac'} so that it not just applies to the topmost
+ connective, but also to the ones immediately ``underneath'', i.e.~analyse the goal
+ completely. For this you can use the tactic combinator @{ML REPEAT}. As an example
+ suppose the following tactic
*}
ML{*val repeat_xmp = REPEAT (CHANGED (select_tac' 1)) *}
-text {* and the proof *}
+text {* which applied to the proof *}
lemma shows "((\<not>A) \<and> (\<forall>x. B x)) \<and> (C \<longrightarrow> D)"
apply(tactic {* repeat_xmp *})
-txt{* \begin{minipage}{\textwidth}
+txt{* produces
+
+ \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
+ because otherwise @{ML REPEAT} runs into an infinite loop (it applies the
+ tactic as long as it succeeds). 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
+ If you are after the ``primed'' version of @{ML repeat_xmp} then you
+ need to implement it as
*}
ML{*val repeat_xmp' = REPEAT o CHANGED o select_tac'*}
@@ -869,17 +927,16 @@
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}.
+ that goals 2 and 3 are not analysed. This is because the tactic
+ is applied repeatedly only to the first subgoal. To analyse also all
+ resulting subgoals, you can use the tactic combinator @{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.
+ you see that the following goal
*}
lemma shows "((\<not>A) \<and> (\<forall>x. B x)) \<and> (C \<longrightarrow> D)"
@@ -890,26 +947,31 @@
(*<*)oops(*>*)
text {*
- The last tactic combinator we describe here is @{ML DETERM}. Recall
- that tactics produce a lazy sequence of successor goal states. These
+ is completely analysed according to the theorems we chose to
+ include in @{ML select_tac}.
+
+ 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
+txt{* applies the rule to the first assumption yielding the goal state:\smallskip
\begin{minipage}{\textwidth}
@{subgoals [display]}
- \end{minipage} *}
+ \end{minipage}\smallskip
+
+ After typing
+ *}
(*<*)
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
+txt{* the rule now applies to the second assumption.\smallskip
\begin{minipage}{\textwidth}
@{subgoals [display]}
@@ -918,8 +980,9 @@
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}.
+ the potential to explode the search space for tactics.
+ These problems can be avoided by prefixing the tactic with the tactic
+ combinator @{ML DETERM}.
*}
lemma "\<lbrakk>P1 \<or> Q1; P2 \<or> Q2\<rbrakk> \<Longrightarrow> R"
@@ -929,7 +992,7 @@
\end{minipage} *}
(*<*)oops(*>*)
text {*
- This will prune the search space to just the first possibility.
+ This will combinator prune the search space to just the first successful application.
Attempting to apply \isacommand{back} in this goal states gives the
error message:
@@ -939,7 +1002,7 @@
\end{isabelle}
\begin{readmore}
- Most tactic combinators are defined in @{ML_file "Pure/tctical.ML"}.
+ Most tactic combinators described in this section are defined in @{ML_file "Pure/tctical.ML"}.
\end{readmore}
*}