isabelle-cookbook: comparison CookBook/Tactical.thy

equal deleted inserted replaced

-:258ce361ba1b
+:8bea3f74889d
 section {* Basics of Reasoning with Tactics*}
 text {*
 To see how tactics work, let us first transcribe a simple \isacommand{apply}-style proof
-into ML. Consider the following proof.
+into ML. Suppose the following proof.
 *}
 lemma disj_swap: "P \<or> Q \<Longrightarrow> Q \<or> P"
 apply(erule disjE)
 apply(rule disjI2)
 @{text erule}, @{text rule} and @{text assumption}, respectively.
 The operator @{ML THEN} strings the tactics together.
 \begin{readmore}
 To learn more about the function @{ML Goal.prove} see \isccite{sec:results}
-and the file @{ML_file "Pure/goal.ML"}. For more information about the
+and the file @{ML_file "Pure/goal.ML"}.  See @{ML_file
-internals of goals see \isccite{sec:tactical-goals}.  See @{ML_file
 "Pure/tactic.ML"} and @{ML_file "Pure/tctical.ML"} for the code of basic
 tactics and tactic combinators; see also Chapters 3 and 4 in the old
 Isabelle Reference Manual.
 \end{readmore}
-Note that we used antiquotations for referencing the theorems. Many theorems
+Note that in the code above we used antiquotations for referencing the theorems. Many theorems
 also have ML-bindings with the same name. Therefore, we could also just have
 written @{ML "etac disjE 1"}, or in case there are no ML-binding obtained
 the theorem dynamically using the function @{ML thm}; for example
-@{ML "etac (thm \"disjE\") 1"}. Both ways however are considered bad style.
+@{ML "etac (thm \"disjE\") 1"}. Both ways however are considered bad style!
 The reason
 is that the binding for @{ML disjE} can be re-assigned by the user and thus
 one does not have complete control over which theorem is actually
 applied. This problem is nicely prevented by using antiquotations, because
 then the theorems are fixed statically at compile-time.
 apply(tactic {* foo_tac' 1 *})
 done
 text {*
 This kind of addressing is more difficult to achieve when the goal is
-hard-coded inside the tactic. For every operator that combines tactics
+hard-coded inside the tactic. For most operators that combine tactics
 (@{ML THEN} is only one such operator) a ``primed'' version exists.
 The tactics @{ML foo_tac} and @{ML foo_tac'} are very specific for
 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:
 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
+following proof there are two possibilities for how to apply
 @{ML foo_tac'}: either using the first assumption or the second.
 *}
 lemma "\<lbrakk>P \<or> Q; P \<or> Q\<rbrakk> \<Longrightarrow> Q \<or> P"
 apply(tactic {* foo_tac' 1 *})
 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 proof state in a proof. Consider
+are now in the position to inspect every goal state in a proof. Consider
 the proof below: on the left-hand side we show the goal state as shown
 by Isabelle, on the right-hand side the print out from @{ML my_print_tac}.
 *}
 lemma shows "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"
 apply(tactic {* my_print_tac @{context} *})
 txt{* \small
-\begin{tabular}{@ {}l@ {}p{0.7\textwidth}@ {}}
+\begin{tabularstar}{\textwidth}{@ {}l@ {\extracolsep{\fill}}l@ {}}
 \begin{minipage}[t]{0.3\textwidth}
 @{subgoals [display]}
 \end{minipage} &
-\hfill@{text "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}
+@{text "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}
-\end{tabular}
+\end{tabularstar}
 *}
 apply(rule conjI)
 apply(tactic {* my_print_tac @{context} *})
 txt{* \small
-\begin{tabular}{@ {}l@ {}p{0.76\textwidth}@ {}}
+\begin{tabularstar}{\textwidth}{@ {}l@ {\extracolsep{\fill}}l@ {}}
 \begin{minipage}[t]{0.26\textwidth}
 @{subgoals [display]}
 \end{minipage} &
-\hfill@{text "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> B) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}
+@{text "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> B) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}
-\end{tabular}
+\end{tabularstar}
 *}
 apply(assumption)
 apply(tactic {* my_print_tac @{context} *})
 txt{* \small
-\begin{tabular}{@ {}l@ {}p{0.7\textwidth}@ {}}
+\begin{tabularstar}{\textwidth}{@ {}l@ {\extracolsep{\fill}}l@ {}}
 \begin{minipage}[t]{0.3\textwidth}
 @{subgoals [display]}
 \end{minipage} &
-\hfill@{text "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> B) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}
+@{text "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> B) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}
-\end{tabular}
+\end{tabularstar}
 *}
 apply(assumption)
 apply(tactic {* my_print_tac @{context} *})
 txt{* \small
-\begin{tabular}{@ {}l@ {}p{0.7\textwidth}@ {}}
+\begin{tabularstar}{\textwidth}{@ {}l@ {\extracolsep{\fill}}l@ {}}
 \begin{minipage}[t]{0.3\textwidth}
 @{subgoals [display]}
 \end{minipage} &
-\hfill@{text "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"}
+@{text "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"}
-\end{tabular}
+\end{tabularstar}
 *}
 done
 text {*
 @{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)"}, and when the proof is finished we are left with @{text "(C)"}.
+@{text "C \<Longrightarrow> (C)"}; when the proof is finished we are left with @{text "(C)"}.
 Since the goal @{term C} can potentially be an implication,
 there is a ``protector'' wrapped around it (in from of an outermost constant
 @{text "Const (\"prop\", bool \<Rightarrow> bool)"} applied to each goal;
 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.
+exception of possibly instantiating schematic variables. If you use
+the predefined tactics, this will always be the case.
+\begin{readmore}
+For more information about the internals of goals see \isccite{sec:tactical-goals}.
+\end{readmore}
 *}
 section {* Simple Tactics *}
 text {*
 \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
+procedure might become too fragile, if it just applies inference rules as
-in the fashion above.  More constraints can be introduced by
+shown above. The reason is that a number of rules introduce meta-variables
-pre-instantiating theorems with other theorems. You can do this using the
+into the goal state. Consider for example the proof
-function @{ML RS}. For example
+*}
+lemma shows "\<forall>x\<in>A. P x \<Longrightarrow> Q x"
+apply(drule bspec)
+txt{*\begin{minipage}{\textwidth}
+@{subgoals [display]}
+\end{minipage}*}
+(*<*)oops(*>*)
+text {*
+where the application of @{text bspec} results into two subgoals involving the
+meta-variable @{text "?x"}. The point is that if you are not careful, tactics
+applied to the first subgoal might instantiate this meta-variable in such a
+way that the second subgoal becomes unprovable. If it is clear what the @{text "?x"}
+should be, then this situation can be avoided by introducing a more
+constraint version of the @{text bspec}-rule. Such constraints can be enforced by
+pre-instantiating theorems with other theorems, for example by using the
+function @{ML RS}
 @{ML_response_fake [display,gray]
 "@{thm disjI1} RS @{thm conjI}" "\<lbrakk>?P1; ?Q\<rbrakk> \<Longrightarrow> (?P1 \<or> ?Q1) \<and> ?Q"}
-instantiates the first premise of the @{text conjI}-rule with the
+which, for instance, instantiates the first premise of the @{text conjI}-rule
-rule @{text disjI1}. If this is impossible, as in the case of
+with the rule @{text disjI1}. If this is impossible, as in the case of
 @{ML_response_fake_both [display,gray]
 "@{thm conjI} RS @{thm mp}"
 "*** Exception- THM (\"RSN: no unifiers\", 1,
 [\"\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q\", \"\<lbrakk>?P \<longrightarrow> ?Q; ?P\<rbrakk> \<Longrightarrow> ?Q\"]) raised"}
 | @{term "Not"} $ _ => rtac @{thm notI} i
 | Const (@{const_name "All"}, _) $ _ => rtac @{thm allI} i
 | _ => all_tac*}
 text {*
-In line 3 you need to decend under the outermost @{term "Trueprop"} in order
+In line 3 you need to descend under the outermost @{term "Trueprop"} in order
 to get to the connective you like to analyse. Otherwise goals like @{prop "A \<and> B"}
 are not properly analysed. While for the first four pattern we can use the
 @{text "@term"}-antiquotation, the pattern in Line 7 cannot be constructed
 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.
+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).
 Let us now see how to apply this tactic. Consider the four goals:
 *}
 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 it applied in the other order
+that are produced by the rule. If we had applied it in the other order
 *}
 lemma shows "A \<and> B" and "A \<longrightarrow> B \<longrightarrow>C" and "\<forall>x. D x" and "E \<Longrightarrow> F"
 apply(tactic {* SUBGOAL select_tac 1 *})
 apply(tactic {* SUBGOAL select_tac 3 *})
 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,
 the ``reverse application'' is easy to implement.
 However, this example is very contrived: there are much simpler methods to implement
-such a proof procedure analying a goal according to its topmost
+such a proof procedure analysing a goal according to its topmost
 connective. These simpler methods use tactic combinators which will be explained
 in the next section.
 *}
 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
+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"
 apply(tactic {* rtac @{thm conjI} 1 THEN rtac @{thm conjI} 1 *})
 \end{minipage} *}
 (*<*)oops(*>*)
 text {*
 If you want to avoid the hard-coded subgoal addressing, then you can use
-the ``primed'' version of @{ML THEN}, namely @{ML THEN'}. For example:
+the ``primed'' version of @{ML THEN}. For example:
 *}
 lemma shows "(Foo \<and> Bar) \<and> False"
 apply(tactic {* (rtac @{thm conjI} THEN' rtac @{thm conjI}) 1 *})
 txt {* \begin{minipage}{\textwidth}
 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
+be written as:
 *}
 ML{*val foo_tac'' = EVERY' [etac @{thm disjE}, rtac @{thm disjI2},
 atac, rtac @{thm disjI1}, atac]*}
 text {*
-There is even another variant for @{ML foo_tac''}: in automatic proof
+There is even another way: in automatic proof procedures (in contrast to
-procedures (in contrast to tactics that might be called by the user)
+tactics that might be called by the user) there are often long lists of
-there are often long lists of tactics that are applied to the first
+tactics that are applied to the first subgoal. Instead of writing the code
-subgoal. Instead of writing the code above and then calling
+above and then calling @{ML "foo_tac'' 1"}, you can also just write
-@{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
+guaranteed that  all component tactics successfully apply; otherwise the
 whole tactic will fail. If you rather want to try out a number of tactics,
-then you can use the combinator @{ML ORELSE'} for two tactics and @{ML FIRST'}
+then you can use the combinator @{ML ORELSE'} for two tactics, and @{ML FIRST'}
 (or @{ML FIRST1}) for a list of tactics. For example, the tactic
 *}
 ML{*val orelse_xmp = (rtac @{thm disjI1} ORELSE' rtac @{thm 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 2 *})
 apply(tactic {* orelse_xmp 1 *})
-apply(tactic {* orelse_xmp 3 *})
 txt {* which results in the goal state
 \begin{minipage}{\textwidth}
 @{subgoals [display]}
 \end{minipage}
 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
+Since we like to mimic the behaviour of @{ML select_tac} as closely as possible,
-@{ML all_tac} at the end (@{ML all_tac} must also be ``wrapped up'' using
+we must include @{ML all_tac} at the end of the list (@{ML all_tac} must also
-the @{ML K}-combinator as it does not take a subgoal number as argument).
+be ``wrapped up'' using the @{ML K}-combinator, as it does not take a subgoal
-We can test the tactic on the same proof:
+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 *})
 @{subgoals [display]}
 \end{minipage} *}
 (*<*)oops(*>*)
 text {*
-and obtain the same subgoals. Since this repeated application of a tactic
+Because such repeated applications of a tactic to the reverse order of
-to the reverse order of \emph{all} subgoals is quite common, there is
+\emph{all} subgoals is quite common, there is the tactics combinator
-the tactics combinator @{ML ALLGOALS} that simplifies this. Using this
+@{ML ALLGOALS} that simplifies this. Using this combinator we can simply
-combinator we can simply write: *}
+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.
+Remember that we chose to write @{ML select_tac'} in such a way that it always
-This can be potetially very  confusing for the user in cases of goals
+succeeds. This can be potentially very confusing for the user, for example,
-of the form
+in cases the goals is the form
 *}
 lemma shows "E \<Longrightarrow> F"
 apply(tactic {* select_tac' 1 *})
 txt{* \begin{minipage}{\textwidth}
 (*<*)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
+delete th @{ML "K all_tac"} from the end of the list. Then @{ML select_tac'}
-only apply in cases where it can make some progress. But for the sake of
+would only succeed on goals where it can make progress. But for the sake of
-argument, let us assume that this is not an option. In such cases, you
+argument, let us suppose that this deletion is not an option. In such cases, you
 can use the combinator @{ML CHANGED} to make sure the subgoal has been
 changed by the tactic. Because now
 *}
 lemma shows "E \<Longrightarrow> F"
 apply(tactic {* CHANGED (select_tac' 1) *})(*<*)?(*>*)
-txt{* results in the usual error message for empty result sequences. *}
+txt{* results in the error message:
-(*<*)oops(*>*)
+\begin{isabelle}
+@{text "*** empty result sequence -- proof command failed"}\\
+@{text "*** At command \"apply\"."}
-text {*
+\end{isabelle}
+*}(*<*)oops(*>*)
-@{ML REPEAT} @{ML DETERM}
-@{ML CHANGED}
+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
+*}
+ML{*val repeat_xmp = REPEAT (CHANGED (select_tac' 1)) *}
+text {* and the proof *}
+lemma shows "((\<not>A) \<and> (\<forall>x. B x)) \<and> (C \<longrightarrow> D)"
+apply(tactic {* repeat_xmp *})
+txt{* \begin{minipage}{\textwidth}
+@{subgoals [display]}
+\end{minipage} *}
+(*<*)oops(*>*)
+text {*
+Here it is crucial that @{ML select_tac'} is prefixed with @{ML CHANGED},
+because otherwise @{ML REPEAT} runs into an infinite loop. The function
+@{ML REPEAT1} is similar, but runs the tactic at least once (failing if
+this is not possible).
+If you are after the ``primed'' version of @{ML repeat_xmp} then it
+needs to be coded as
+*}
+ML{*val repeat_xmp' = REPEAT o CHANGED o select_tac'*}
+text {*
+since there are no ``primed'' versions of @{ML REPEAT} and @{ML CHANGED}.
+If you look closely at the goal state above, the tactics @{ML repeat_xmp}
+and @{ML repeat_xmp'} are not yet quite what we are after: the problem is
+that goals 2 and 3 are not yet analysed. This is because both tactics
+apply repeatedly only to the first subgoal. To analyse also all
+resulting subgoals, you can use the function @{ML REPEAT_ALL_NEW}.
+Suppose the tactic
+*}
+ML{*val repeat_all_new_xmp = REPEAT_ALL_NEW (CHANGED o select_tac')*}
+text {*
+which analyses the topmost connectives also in all resulting
+subgoals.
+*}
+lemma shows "((\<not>A) \<and> (\<forall>x. B x)) \<and> (C \<longrightarrow> D)"
+apply(tactic {* repeat_all_new_xmp 1 *})
+txt{* \begin{minipage}{\textwidth}
+@{subgoals [display]}
+\end{minipage} *}
+(*<*)oops(*>*)
+text {*
+The last tactic combinator we describe here is @{ML DETERM}. Recall
+that tactics produce a lazy sequence of successor goal states. These
+states can be explored using the command \isacommand{back}. For example
+*}
+lemma "\<lbrakk>P1 \<or> Q1; P2 \<or> Q2\<rbrakk> \<Longrightarrow> R"
+apply(tactic {* etac @{thm disjE} 1 *})
+txt{* applies the rule to the first assumption
+\begin{minipage}{\textwidth}
+@{subgoals [display]}
+\end{minipage} *}
+(*<*)
+oops
+lemma "\<lbrakk>P1 \<or> Q1; P2 \<or> Q2\<rbrakk> \<Longrightarrow> R"
+apply(tactic {* etac @{thm disjE} 1 *})
+(*>*)
+back
+txt{* whereas it is now applied to the second
+\begin{minipage}{\textwidth}
+@{subgoals [display]}
+\end{minipage} *}
+(*<*)oops(*>*)
+text {*
+Sometimes this leads to confusing behaviour of tactics and also has
+the potential to explode the search space for tactics build on top.
+This can be avoided by prefixing the tactic with @{ML DETERM}.
+*}
+lemma "\<lbrakk>P1 \<or> Q1; P2 \<or> Q2\<rbrakk> \<Longrightarrow> R"
+apply(tactic {* DETERM (etac @{thm disjE} 1) *})
+txt {*\begin{minipage}{\textwidth}
+@{subgoals [display]}
+\end{minipage} *}
+(*<*)oops(*>*)
+text {*
+This will prune the search space to just the first possibility.
+Attempting to apply \isacommand{back} in this goal states gives the
+error message:
+\begin{isabelle}
+@{text "*** back: no alternatives"}\\
+@{text "*** At command \"back\"."}
+\end{isabelle}
+\begin{readmore}
+Most tactic combinators are defined in @{ML_file "Pure/tctical.ML"}.
+\end{readmore}
 *}
 section {* Rewriting and Simplifier Tactics *}

changeset 108	8bea3f74889d
parent 107	258ce361ba1b
child 109	b4234e8a0202