isabelle-cookbook: comparison CookBook/Tactical.thy

equal deleted inserted replaced

-:8bea3f74889d
+:b4234e8a0202
 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!
+\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
 applied. This problem is nicely prevented by using antiquotations, because
 then the theorems are fixed statically at compile-time.
 THEN' atac)*}
 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"
 and "P2 \<or> Q2 \<Longrightarrow> Q2 \<or> P2"
 apply(tactic {* foo_tac' 2 *})
 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
 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
+This means 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,
+are functions mapping a goal state to a (lazy) sequence of successor states.
-hence the type of a tactic is:
+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:
+text {*
-therefore your own tactics should not raise exceptions willy-nilly. Only
+By convention, if a tactic fails, then it should return the empty sequence.
-in very grave failure situations should a tactic raise the exception
+Therefore, if you write your own tactics, they  should not raise exceptions
-@{text THM}.
+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
 *}
 ML{*fun no_tac thm = Seq.empty*}
 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
+which means @{ML all_tac} always succeeds, but also does not make any progress
-with the proof).
+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.
 *}
 done
 text {*
 By using \isacommand{back}, we construct the proof that uses the
-second assumption. In more interesting situations, only by exploring
+second assumption. While in the proof above, it does not really matter which
-different possibilities one might be able to find a proof.
+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
+sequences. In day-to-day Isabelle programming, however, one rarely
-constructs sequences explicitly, but uses the predefined functions
+constructs sequences explicitly, but uses the predefined tactics and
-instead.
+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
 tactic
 *}
 val _ = warning (str_of_thm ctxt thm)
 in
 Seq.single thm
 end*}
-text {*
+text_raw {*
-which prints out the given theorem (using the string-function defined
+\begin{figure}[p]
-in Section~\ref{sec:printing}) and then behaves like @{ML all_tac}. We
+\begin{isabelle}
-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}.
-*}
 lemma shows "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"
 apply(tactic {* my_print_tac @{context} *})
-txt{* \small
+txt{* \begin{minipage}{\textwidth}
-\begin{tabularstar}{\textwidth}{@ {}l@ {\extracolsep{\fill}}l@ {}}
-\begin{minipage}[t]{0.3\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
+txt{* \begin{minipage}{\textwidth}
-\begin{tabularstar}{\textwidth}{@ {}l@ {\extracolsep{\fill}}l@ {}}
-\begin{minipage}[t]{0.26\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
+txt{* \begin{minipage}{\textwidth}
-\begin{tabularstar}{\textwidth}{@ {}l@ {\extracolsep{\fill}}l@ {}}
-\begin{minipage}[t]{0.3\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
+txt{* \begin{minipage}{\textwidth}
-\begin{tabularstar}{\textwidth}{@ {}l@ {\extracolsep{\fill}}l@ {}}
-\begin{minipage}[t]{0.3\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 {*
-text {*
+\end{isabelle}
-As can be seen, internally every goal state is an implication of the form
+\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}
+*}
+text {*
+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
+where @{term C} is the goal to be proved and the @{term "A\<^isub>i"} are
-subgoals. So after setting up the lemma, the goal state is always of the form
+the subgoals. So after setting up the lemma, the goal state is always of the
-@{text "C \<Longrightarrow> (C)"}; when the proof is finished we are left with @{text "(C)"}.
+form @{text "C \<Longrightarrow> (C)"}; when the proof is finished we are left with @{text
-Since the goal @{term C} can potentially be an implication,
+"(C)"}. Since the goal @{term C} can potentially be an implication, there is
-there is a ``protector'' wrapped around it (in from of an outermost constant
+a ``protector'' wrapped around it (in from of an outermost constant @{text
-@{text "Const (\"prop\", bool \<Rightarrow> bool)"} applied to each goal;
+"Const (\"prop\", bool \<Rightarrow> bool)"} applied to each goal; however this constant
-however this constant is invisible in the print out above). This
+is invisible in the figure). This prevents that premises of @{text C} are
-prevents that premises of @{text C} are mis-interpreted as open subgoals.
+mis-interpreted as open subgoals. While tactics can operate on the subgoals
-While tactics can operate on the subgoals (the @{text "A\<^isub>i"} above), they
+(the @{text "A\<^isub>i"} above), they are expected to leave the conclusion
-are expected to leave the conclusion @{term C} intact, with the
+@{term C} intact, with the exception of possibly instantiating schematic
-exception of possibly instantiating schematic variables. If you use
+variables. If you use the predefined tactics, which we describe in the next
-the predefined tactics, this will always be the case.
+section, 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 *}
 text {*
-A simple tactic is @{ML print_tac}, which is quite useful for low-level debugging of tactics.
+Let us start with the tactic @{ML print_tac}, which is quite useful for low-level
-It just prints out a message and the current goal state.
+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"}\\
 \end{minipage}
 *}
 section, corresponds to the assumption command.
 *}
 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
+respectively. Each of them takes a theorem as argument and attempts to
-examples with the resulting goal state. How
+apply it to a goal. Below are three self-explanatory examples.
-they work should be self-explanatory.
 *}
 lemma shows "P \<and> Q"
 apply(tactic {* rtac @{thm conjI} 1 *})
 txt{*\begin{minipage}{\textwidth}
 @{subgoals [display]}
 \end{minipage}*}
 (*<*)oops(*>*)
 text {*
-As mentioned in the previous section, most basic tactics take a number as
+Note the number in each tactic call. Also as mentioned in the previous section, most
-argument, which addresses the subgoal they are analysing. In the proof below,
+basic tactics take such an argument; it addresses the subgoal they are analysing.
-we first analyse the second subgoal by focusing on this subgoal first.
+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"
 apply(tactic {* rtac @{thm conjI} 2 *})
 txt {*\begin{minipage}{\textwidth}
 @{subgoals [display]}
 \end{minipage}*}
 (*<*)oops(*>*)
 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
 explored via the lazy sequences mechanism). Given the code
 *}
 @{subgoals [display]}
 \end{minipage}*}
 (*<*)oops(*>*)
 text {*
-Similarly versions exists for @{ML atac} (@{ML assume_tac}), @{ML etac}
+Similarly versions taking a list of theorems exist for the tactics
-(@{ML eresolve_tac}) and so on.
+@{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(*>*)
 text {*
 @{subgoals [display]}
 \end{minipage}*}
 (*<*)oops(*>*)
 text {*
-where the application of @{text bspec} results into two subgoals involving the
+where the application of Rule @{text bspec} generates two subgoals involving the
-meta-variable @{text "?x"}. The point is that if you are not careful, tactics
+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
+constraint version of the @{text bspec}-rule. Such constraints can be given by
-pre-instantiating theorems with other theorems, for example by using the
+pre-instantiating theorems with other theorems. One function to do this is
-function @{ML RS}
+@{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
+which in the example instantiates the first premise of the @{text conjI}-rule
-with the rule @{text disjI1}. If this is impossible, as in the case of
+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
+then the function raises an exception. The function @{ML RSN} is similar to @{ML RS}, but
-takes a number as argument and thus you can make explicit which premise
+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
 the following function
 *}
 in
 thm'
 end*}
 text {*
 that transform the schematic variables of a theorem into free variables.
-This means for the first @{ML RS}-expression above:
+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"}
 If you want to instantiate more than one premise of a theorem, you can use
 @{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 in the code below
+functions @{ML RL} and @{ML MRL}. For example in the code below,
-every theorem in the first list is instantiated against every
+every theorem in the second list is instantiated with every
-theorem in the second.
+theorem in the first.
 @{ML_response_fake [display,gray]
 "[@{thm impI}, @{thm disjI2}] RL [@{thm conjI}, @{thm disjI1}]"
 "[\<lbrakk>P \<Longrightarrow> Q; Qa\<rbrakk> \<Longrightarrow> (P \<longrightarrow> Q) \<and> Qa,
 \<lbrakk>Q; Qa\<rbrakk> \<Longrightarrow> (P \<or> Q) \<and> Qa,
 \begin{readmore}
 The combinators for instantiating theorems are defined in @{ML_file "Pure/drule.ML"}.
 \end{readmore}
-Often proofs involve elaborate operations on assumptions and
+Often proofs on the ML-level involve elaborate operations on assumptions and
-@{text "\<And>"}-quantified variables. To do such operations on the ML-level
+@{text "\<And>"}-quantified variables. To do such operations using the basic tactics
-using the basic tactics is very unwieldy and brittle. Some convenience and
+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
+takes a record and just prints out the content of this record (using the
-string transformation functions defined in Section~\ref{sec:printing}). Consider
+string transformation functions from in Section~\ref{sec:printing}). Consider
-now the proof
+now the proof:
 *}
 text_raw{*
 \begin{figure}
 \begin{isabelle}
 lemma shows "\<And>x y. A x y \<Longrightarrow> B y x \<longrightarrow> C (?z y) x"
 apply(tactic {* SUBPROOF sp_tac @{context} 1 *})?
 txt {*
-which gives the printout:
+The tactic produces the following printout:
 \begin{quote}\small
 \begin{tabular}{ll}
 params:      & @{term x}, @{term y}\\
 schematics:  & @{term z}\\
 \end{tabular}
 \end{quote}
 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
+Notice also that we had to append @{text [quotes] "?"} to the
-reason is that @{ML SUBPROOF} normally expects that the subgoal is solved completely.
+\isacommand{apply}-command. The reason is that @{ML SUBPROOF} normally
-Since in the function @{ML sp_tac} we returned the tactic @{ML no_tac}, the subproof
+expects that the subgoal is solved completely.  Since in the function @{ML
-obviously fails. The question-mark allows us to recover from this failure
+sp_tac} we returned the tactic @{ML no_tac}, the subproof obviously
-in a graceful manner so that the warning messages are not overwritten
+fails. The question-mark allows us to recover from this failure in a
-by an error message.
+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
 *}
 apply(rule impI)
 apply(tactic {* SUBPROOF sp_tac @{context} 1 *})?
 txt {*
-then @{ML sp_tac} prints out
+then tactic prints out
 \begin{quote}\small
 \begin{tabular}{ll}
 params:      & @{term x}, @{term y}\\
 schematics:  & @{term z}\\
 \end{quote}
 *}
 (*<*)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
+contains them as theorems. With this you can easily
-implement a tactic that almost behaves like @{ML atac}, namely:
+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
+Notice that @{ML atac'} inside @{ML SUBPROOF} calls @{ML resolve_tac} with
-number @{text "1"} and also the ``outer'' call to @{ML SUBPROOF} in
+the subgoal number @{text "1"} and also the outer call to @{ML SUBPROOF} in
-the \isacommand{apply}-step uses @{text "1"}. Another advantage
+the \isacommand{apply}-step uses @{text "1"}. This is another advantage
-of @{ML SUBGOAL} is that the addressing  inside it is completely
+of @{ML SUBPROOF}: the addressing  inside it is completely
-local to the subproof inside. It is therefore possible to also apply
+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
 also described in \isccite{sec:results}.
 \end{readmore}
 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
 | Const (@{const_name "All"}, _) $ _ => rtac @{thm allI} i
 | _ => all_tac*}
 text {*
-In line 3 you need to descend under the outermost @{term "Trueprop"} in order
+The input of the function is a term representing the subgoal and a number
-to get to the connective you like to analyse. Otherwise goals like @{prop "A \<and> B"}
+specifying the subgoal of interest. In line 3 you need to descend under the
-are not properly analysed. While for the first four pattern we can use the
+outermost @{term "Trueprop"} in order to get to the connective you like to
-@{text "@term"}-antiquotation, the pattern in Line 7 cannot be constructed
+analyse. Otherwise goals like @{prop "A \<and> B"} are not properly
-in this way. The reason is that an antiquotation would fix the type of the
+analysed. Similarly with meta-implications in the next line.  While for the
-quantified variable. So you really have to construct the pattern
+first five patterns we can use the @{text "@term"}-antiquotation to
-using the term-constructors. This is not necessary in  other cases, because
+construct the patterns, the pattern in Line 8 cannot be constructed in this
-their type is always something involving @{typ bool}. The final patter is
+way. The reason is that an antiquotation would fix the type of the
-for the case where the goal does not fall into any of the categories before.
+quantified variable. So you really have to construct the pattern using the
-In this case we chose to just return @{ML all_tac} (i.e., @{ML select_tac}
+basic term-constructors. This is not necessary in other cases, because their type
-never fails).
+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:
 *}
 \end{minipage} *}
 (*<*)oops(*>*)
 text {*
 where in all but the last the tactic applied an introduction rule.
-Note that we applied the tactic to subgoals in ``reverse'' order.
+Note that we applied the tactic to the goals in ``reverse'' order.
-This is a trick in order to be independent from what subgoals are
+This is a trick in order to be independent from the subgoals that are
-that are produced by the rule. If we had applied it in the other order
+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"
 apply(tactic {* SUBGOAL select_tac 1 *})
 apply(tactic {* SUBGOAL select_tac 3 *})
 apply(tactic {* SUBGOAL select_tac 4 *})
 apply(tactic {* SUBGOAL select_tac 5 *})
 (*<*)oops(*>*)
 text {*
-then we have to be careful to not apply the tactic to the two subgoals the
+then we have to be careful to not apply the tactic to the two subgoals produced by
-first goal produced. To do this can result in quite messy code. In contrast,
+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
+Of course, this example is contrived: there are much simpler methods available in
-such a proof procedure analysing a goal according to its topmost
+Isabelle for implementing a proof procedure analysing a goal according to its topmost
-connective. These simpler methods use tactic combinators which will be explained
+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
+The purpose of tactic combinators is to build compound tactics out of
-smaller components. In the previous section we already used @{ML THEN}, which
+smaller tactics. In the previous section we already used @{ML THEN}, which
-strings two tactics together in sequence. For example:
+just strings together two tactics in a sequence. For example:
 *}
 lemma shows "(Foo \<and> Bar) \<and> False"
 apply(tactic {* rtac @{thm conjI} 1 THEN rtac @{thm conjI} 1 *})
 txt {* \begin{minipage}{\textwidth}
 @{subgoals [display]}
 \end{minipage} *}
 (*<*)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:
 *}
 ML{*val foo_tac'' = EVERY' [etac @{thm disjE}, rtac @{thm disjI2},
 atac, rtac @{thm disjI1}, atac]*}
 text {*
-There is even another way: in automatic proof procedures (in contrast to
+There is even another way of implementing this tactic: in automatic proof
-tactics that might be called by the user) there are often long lists of
+procedures (in contrast to tactics that might be called by the user) there
-tactics that are applied to the first subgoal. Instead of writing the code
+are often long lists of tactics that are applied to the first
-above and then calling @{ML "foo_tac'' 1"}, you can also just write
+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
+and just call @{ML foo_tac1}.
-guaranteed that  all component tactics successfully apply; otherwise the
-whole tactic will fail. If you rather want to try out a number of tactics,
+With the combinators @{ML THEN'}, @{ML EVERY'} and @{ML EVERY1} it must be
-then you can use the combinator @{ML ORELSE'} for two tactics, and @{ML FIRST'}
+guaranteed that all component tactics successfully apply; otherwise the
-(or @{ML FIRST1}) for a list of tactics. For example, the tactic
+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"
 apply(tactic {* orelse_xmp 2 *})
 apply(tactic {* orelse_xmp 1 *})
 *}
 (*<*)oops(*>*)
 text {*
-Using @{ML FIRST'} we can write our @{ML select_tac} from Page~\ref{tac:selecttac}
+Using @{ML FIRST'} we can simplify our @{ML select_tac} from Page~\pageref{tac:selecttac}
-simply as follows:
+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 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
+we must include @{ML all_tac} at the end of the list, otherwise the tactic will
-be ``wrapped up'' using the @{ML K}-combinator, as it does not take a subgoal
+fail if no rule applies (we laso have to wrap @{ML all_tac} using the
-number as argument). We can test the tactic on the same proof:
+@{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"
 apply(tactic {* select_tac' 4 *})
 apply(tactic {* select_tac' 3 *})
 @{subgoals [display]}
 \end{minipage} *}
 (*<*)oops(*>*)
 text {*
-Because such repeated applications of a tactic to the reverse order of
+Since such repeated applications of a tactic to the reverse order of
-\emph{all} subgoals is quite common, there is the tactics combinator
+\emph{all} subgoals is quite common, there is the tactic combinator
-@{ML ALLGOALS} that simplifies this. Using this combinator we can simply
+@{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"
 apply(tactic {* ALLGOALS select_tac' *})
 txt{* \begin{minipage}{\textwidth}
 @{subgoals [display]}
 \end{minipage} *}
 (*<*)oops(*>*)
 text {*
-Remember that we chose to write @{ML select_tac'} in such a way that it always
+Remember that we chose to implement @{ML select_tac'} so that it
-succeeds. This can be potentially very confusing for the user, for example,
+always  succeeds. This can be potentially very confusing for the user,
-in cases the goals is the form
+for example,  in cases where the goal is 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
+In this case no rule applies. The problem for the user is that there is little
-to see whether progress in the proof has been made or not. We could simply
+chance to see whether or not progress in the proof has been made. By convention
-delete th @{ML "K all_tac"} from the end of the list. Then @{ML select_tac'}
+therefore, tactics visible to the user should either change something or fail.
-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
+To comply with this convention, we could simply delete the @{ML "K all_tac"}
-can use the combinator @{ML CHANGED} to make sure the subgoal has been
+from the end of the theorem list. As a result @{ML select_tac'} would only
-changed by the tactic. Because now
+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\"."}
 \end{isabelle}
 *}(*<*)oops(*>*)
 text {*
-Meaning the tactic failed.
+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
-We can extend @{ML select_tac'} so that it not just applies to the top-most
+completely. For this you can use the tactic combinator @{ML REPEAT}. As an example
-connective, but also to the ones immediately ``underneath''. For this you can use the
+suppose the following tactic
-tactic combinator @{ML REPEAT}. For 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
+If you are after the ``primed'' version of @{ML repeat_xmp} then you
-needs to be coded as
+need to implement it 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
+that goals 2 and 3 are not analysed. This is because the tactic
-apply repeatedly only to the first subgoal. To analyse also all
+is applied repeatedly only to the first subgoal. To analyse also all
-resulting subgoals, you can use the function @{ML REPEAT_ALL_NEW}.
+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
+you see that the following goal
-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(*>*)
 text {*
-The last tactic combinator we describe here is @{ML DETERM}. Recall
+is completely analysed according to the theorems we chose to
-that tactics produce a lazy sequence of successor goal states. These
+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]}
 \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.
+the potential to explode the search space for tactics.
-This can be avoided by prefixing the tactic with @{ML DETERM}.
+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"
 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.
+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:
 \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"}.
+Most tactic combinators described in this section are defined in @{ML_file "Pure/tctical.ML"}.
 \end{readmore}
 *}
 section {* Rewriting and Simplifier Tactics *}

changeset 109	b4234e8a0202
parent 108	8bea3f74889d
child 114	13fd0a83d3c3