isabelle-cookbook: comparison CookBook/Tactical.thy

equal deleted inserted replaced

-:bdd82350cf22
+:258ce361ba1b
 \end{readmore}
 Note that we used antiquotations for referencing the theorems. Many theorems
 also have ML-bindings with the same name. Therefore, we could also just have
 written @{ML "etac disjE 1"}, or in case there are no ML-binding obtained
-the theorem dynamically using the theorem @{ML thm}; for example @{ML "etac
+the theorem dynamically using the function @{ML thm}; for example
-(thm \"disjE\") 1"}. Both ways however are considered bad style. The reason
+@{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.
 The tactic @{ML foo_tac} is just a sequence of simple tactics stringed
 together by @{ML THEN}. As can be seen, each simple tactic in @{ML foo_tac}
 has a hard-coded number that stands for the subgoal analysed by the
 tactic (@{text "1"} stands for the first, or top-most, subgoal). This hard-coding
 of goals is sometimes wanted, but usually it is not. To avoid the explicit numbering,
-you can write
+you can write\label{tac:footacprime}
 *}
 ML{*val foo_tac' =
 (etac @{thm disjE}
 THEN' rtac @{thm disjI2}
 hence the type of a tactic is:
 @{text [display, gray] "type tactic = thm -> thm Seq.seq"}
 It is custom that if a tactic fails, it should return the empty sequence:
-therefore your own tactics should not raise exceptions willy-nilly.
+therefore your own tactics should not raise exceptions willy-nilly. Only
+in very grave failure situations should a tactic raise the exception
+@{text THM}.
 The simplest tactics are @{ML no_tac} and @{ML all_tac}. The first returns
 the empty sequence and is defined as
 *}
 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. It is defined as
+as a single member sequence; @{ML all_tac} is defined as
 *}
 ML{*fun all_tac thm = Seq.single thm*}
 text {*
-which means @{ML all_tac} always succeeds (but also does not make any progress
+which means it always succeeds (but also does not make any progress
 with the proof).
 The lazy list of possible successor states shows through at the user-level
 of Isabelle when using the command \isacommand{back}. For instance in the
 following proof, there are two possibilities for how to apply
-@{ML foo_tac'}.
+@{ML foo_tac'}: either using the first assumption or the second.
 *}
 lemma "\<lbrakk>P \<or> Q; P \<or> Q\<rbrakk> \<Longrightarrow> Q \<or> P"
 apply(tactic {* foo_tac' 1 *})
 back
 done
 text {*
 By using \isacommand{back}, we construct the proof that uses the
-second assumption. In more interesting situations, different possibilities
+second assumption. In more interesting situations, only by exploring
-can lead to different proofs and even often need to be explored when
+different possibilities one might be able to find a proof.
-a first proof attempt is unsuccessful.
 \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
 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
-now can inspect every proof state in a proof. Consider the proof below: on
+are now in the position to inspect every proof state in a proof. Consider
-the left-hand side we show the goal state as shown by Isabelle; on the
+the proof below: on the left-hand side we show the goal state as shown
-right-hand side the print out from @{ML my_print_tac}.
+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} *})
 @{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)"}. Since the goal @{term C} can potentially be an implication,
+@{text "C \<Longrightarrow> (C)"}, and when the proof is finished we are left with @{text "(C)"}.
+Since the goal @{term C} can potentially be an implication,
 there is a ``protector'' wrapped around it (in from of an outermost constant
 @{text "Const (\"prop\", bool \<Rightarrow> bool)"} applied to each goal;
 however this constant is invisible in the print out above). This
-prevents that premises of @{text C} are misinterpreted as open subgoals.
+prevents that premises of @{text C} are mis-interpreted as open subgoals.
 While tactics can operate on the subgoals (the @{text "A\<^isub>i"} above), they
 are expected to leave the conclusion @{term C} intact, with the
 exception of possibly instantiating schematic variables.
 *}
 section {* Simple Tactics *}
 text {*
-A simple tactic is @{ML print_tac}, which is useful for low-level debugging of tactics.
+A simple tactic is @{ML print_tac}, which is quite useful for low-level debugging of tactics.
 It just prints out a message and the current goal state.
 *}
 lemma shows "False \<Longrightarrow> True"
 apply(tactic {* print_tac "foo message" *})
+txt{*\begin{minipage}{\textwidth}\small
+@{text "foo message"}\\[3mm]
+@{prop "False \<Longrightarrow> True"}\\
+@{text " 1. False \<Longrightarrow> True"}\\
+\end{minipage}
+*}
 (*<*)oops(*>*)
 text {*
 Another simple tactic is the function @{ML atac}, which, as shown in the previous
 section, corresponds to the assumption command.
 (*<*)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 break up the second subgoal by focusing on this subgoal first.
+we first analyse the second subgoal by focusing on this subgoal first.
 *}
 lemma shows "Foo" and "P \<and> Q"
 apply(tactic {* rtac @{thm conjI} 2 *})
 txt {*\begin{minipage}{\textwidth}
 text {*
 Similarly versions exists for @{ML atac} (@{ML assume_tac}), @{ML etac}
 (@{ML eresolve_tac}) and so on.
-(FIXME: @{ML cut_facts_tac})
+Another simple tactic is @{ML cut_facts_tac}. It inserts a list of theorems
+into the assumptions of the current goal state. For example:
+*}
+lemma shows "True \<noteq> False"
+apply(tactic {* cut_facts_tac [@{thm True_def}, @{thm False_def}] 1 *})
+txt{*\begin{minipage}{\textwidth}
+@{subgoals [display]}
+\end{minipage}*}
+(*<*)oops(*>*)
+text {*
 Since rules are applied using higher-order unification, an automatic proof
 procedure might become too fragile, if it just applies inference rules shown
 in the fashion above.  More constraints can be introduced by
 pre-instantiating theorems with other theorems. You can do this using the
 function @{ML RS}. For example
 @{ML_response_fake [display,gray]
 "@{thm disjI1} RS @{thm conjI}" "\<lbrakk>?P1; ?Q\<rbrakk> \<Longrightarrow> (?P1 \<or> ?Q1) \<and> ?Q"}
 instantiates the first premise of the @{text conjI}-rule with the
-rule @{text disjI1}. The function @{ML RSN} is similar, but
+rule @{text disjI1}. If this is impossible, as in the case of
-takes a number and makes explicit which premise should be instantiated.
-To improve readability we are going use the following function
+@{ML_response_fake_both [display,gray]
+"@{thm conjI} RS @{thm mp}"
+"*** Exception- THM (\"RSN: no unifiers\", 1,
+[\"\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q\", \"\<lbrakk>?P \<longrightarrow> ?Q; ?P\<rbrakk> \<Longrightarrow> ?Q\"]) raised"}
+the function raises an exception. The function @{ML RSN} is similar, but
+takes a number as argument and thus you can make explicit which premise
+should be instantiated.
+To improve readability of the theorems we produce below, we shall use
+the following function
 *}
 ML{*fun no_vars ctxt thm =
 let
 val ((_, [thm']), _) = Variable.import_thms true [thm] ctxt
 in
 thm'
 end*}
 text {*
-to transform the schematic variables of a theorem into free variables.
+that transform the schematic variables of a theorem into free variables.
-This means for the @{ML RS}-expression above:
+This means for the first @{ML RS}-expression above:
 @{ML_response_fake [display,gray]
 "no_vars @{context} (@{thm disjI1} RS @{thm conjI})" "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> (P \<or> Qa) \<and> Q"}
-If you want to instantiate more than one premise, you can use the function
+If you want to instantiate more than one premise of a theorem, you can use
-@{ML MRS}:
+the function @{ML MRS}:
 @{ML_response_fake [display,gray]
 "no_vars @{context} ([@{thm disjI1}, @{thm disjI2}] MRS @{thm conjI})"
 "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> (P \<or> Qa) \<and> (Pa \<or> Q)"}
 If you need to instantiate lists of theorems, you can use the
-functions @{ML RL} and @{ML MRL}. For example below every
+functions @{ML RL} and @{ML MRL}. For example in the code below
-theorem in the first list is instantiated against every theorem
+every theorem in the first list is instantiated against every
-in the second.
+theorem in the second.
 @{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,
 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 yields the printout:
+which gives the printout:
 \begin{quote}\small
 \begin{tabular}{ll}
 params:      & @{term x}, @{term y}\\
 schematics:  & @{term z}\\
 apply(rule impI)
 apply(tactic {* SUBPROOF sp_tac @{context} 1 *})?
 txt {*
-then @{ML SUBPROOF} prints out
+then @{ML sp_tac} prints out
 \begin{quote}\small
 \begin{tabular}{ll}
 params:      & @{term x}, @{term y}\\
 schematics:  & @{term z}\\
 contains them as theorems. With this we can easily
 implement a tactic that almost behaves like @{ML atac}, namely:
 *}
 ML{*val atac' = SUBPROOF (fn {prems, ...} => resolve_tac prems 1)*}
+text {*
+If we apply it to the next lemma
+*}
 lemma shows "\<And>x y. \<lbrakk>B x y; A x y; C x y\<rbrakk> \<Longrightarrow> A x y"
 apply(tactic {* atac' @{context} 1 *})
-txt{* yields
+txt{* we get
 @{subgoals [display]} *}
 (*<*)oops(*>*)
 text {*
 The restriction in this tactic is that it cannot instantiate any
-schematic variables. This might be seen as a defect, but is actually
+schematic variable. This might be seen as a defect, but it is actually
 an advantage in the situations for which @{ML SUBPROOF} was designed:
 the reason is that instantiation of schematic variables can affect
 several goals and can render them unprovable. @{ML SUBPROOF} is meant
 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
-@{ML atac'} to the second goal:
+@{ML atac'} to the second goal by just writing:
 *}
 lemma shows "True" and "\<And>x y. \<lbrakk>B x y; A x y; C x y\<rbrakk> \<Longrightarrow> A x y"
 apply(tactic {* atac' @{context} 2 *})
 apply(rule TrueI)
 The function @{ML SUBPROOF} is defined in @{ML_file "Pure/subgoal.ML"} and
 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 specified subgoal. With this you can implement
+It allows you to inspect a given  subgoal. With this you can implement
-a tactic that applies a rule according to its topmost connective (we only
+a tactic that applies a rule according to the topmost connective in the
-analyse a few connectives). The tactic is as follows:
+subgoal (to illustrate this we only analyse a few connectives). The code
+of this tactic is as follows.\label{tac:selecttac}
 *}
 ML %linenumbers{*fun select_tac (t,i) =
 case t of
 @{term "Trueprop"} $ t' => select_tac (t',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
-to get to the connective you like to analyse. Otherwise goals @{prop "A \<and> B"}
+to get to the connective you like to analyse. Otherwise goals like @{prop "A \<and> B"}
-are not bropek up. In line 7, the pattern cannot be constructed using the
+are not properly analysed. While for the first four pattern we can use the
-@{text "@term"}-antiquotation, because that would fix the type of the
+@{text "@term"}-antiquotation, the pattern in Line 7 cannot be constructed
-quantified variable. In this case you really have to construct the pattern
+in this way. The reason is that an antiquotation would fix the type of the
-by using the term-constructors. The other cases work, because their type
+quantified variable. So you really have to construct the pattern
-is always bool. In case that the goal does not fall into any of the categorories,
+using the term-constructors. This is not necessary in  other cases, because
-then we chose to just return @{ML all_tac} (i.e., the tactic never fails).
+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.
-Let us now see how to apply this tactic.
+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:
 *}
 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 4 *})
 apply(tactic {* SUBGOAL select_tac 3 *})
 apply(tactic {* SUBGOAL select_tac 2 *})
 apply(tactic {* SUBGOAL select_tac 1 *})
-txt{* @{subgoals [display]} *}
+txt{* \begin{minipage}{\textwidth}
-(*<*)oops(*>*)
+@{subgoals [display]}
+\end{minipage} *}
-text {*
+(*<*)oops(*>*)
-Note that we applied it in ``reverse'' order. This is a trick in
-order to be independent from what subgoals the rule produced. If we had
+text {*
-it applied in the other order
+where in all but the last the tactic applied an introduction rule.
+Note that we applied the tactic to subgoals in ``reverse'' order.
+This is a trick in order to be independent from what subgoals are
+that are produced by the rule. If we had it applied in the other order
 *}
 lemma shows "A \<and> B" and "A \<longrightarrow> B \<longrightarrow>C" and "\<forall>x. D x" and "E \<Longrightarrow> F"
 apply(tactic {* SUBGOAL select_tac 1 *})
 apply(tactic {* SUBGOAL select_tac 3 *})
 apply(tactic {* SUBGOAL select_tac 5 *})
 (*<*)oops(*>*)
 text {*
 then we have to be careful to not apply the tactic to the two subgoals the
-first goal produced. This can be messy in an automated proof script. The
+first goal produced. To do this can result in quite messy code. In contrast,
-reverse application, on the other hand, is easy to implement.
+the ``reverse application'' is easy to implement.
-However, this example is contrived: there are much simpler ways to implement
+However, this example is very contrived: there are much simpler methods to implement
-such proof procedure that analyses a goal according to its topmost
+such a proof procedure analying a goal according to its topmost
-connective. They will be explained in the next section.
+connective. These simpler methods use tactic combinators which will be explained
+in the next section.
 *}
 section {* Tactic Combinators *}
 text {*
-To be able to implement powerful tactics out of smaller component tactics,
+The purpose of tactic combinators is to build powerful tactics out of
-Isabelle provides tactic combinators. In the previous section we already
+smaller components. In the previous section we already used @{ML THEN} which
-used @{ML THEN} which strings two tactics together in sequence. For example:
+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 *})
 txt {* \begin{minipage}{\textwidth}
 \end{minipage} *}
 (*<*)oops(*>*)
 text {*
 If you want to avoid the hard-coded subgoal addressing, then you can use
-@{ML THEN'}. For example:
+the ``primed'' version of @{ML THEN}, namely @{ML THEN'}. For example:
 *}
 lemma shows "(Foo \<and> Bar) \<and> False"
 apply(tactic {* (rtac @{thm conjI} THEN' rtac @{thm conjI}) 1 *})
 txt {* \begin{minipage}{\textwidth}
 @{subgoals [display]}
 \end{minipage} *}
 (*<*)oops(*>*)
 text {*
-For most tactic combinators such a ``primed'' version exists.
+For most tactic combinators such a ``primed'' version exists and
-In what follows we will, whenever appropriate, prefer the primed version of
+in what follows we will usually prefer it over the ``unprimed'' one.
-the tactic combinator and omit to mention the simple one.
+If there is a list of tactics that should all be tried out in
-With @{ML THEN} and @{ML THEN'} it must be guaranteed that both tactics
+sequence, you can use the combinator @{ML EVERY'}. For example
-sucessfully apply; otherwise the whole tactic will fail. If you want to
+the function @{ML foo_tac'} from page~\ref{tac:footacprime} can also
-try out either one tactic, then you can use @{ML ORELSE'}. For
+be written as
-example
+*}
+ML{*val foo_tac'' = EVERY' [etac @{thm disjE}, rtac @{thm disjI2},
+atac, rtac @{thm disjI1}, atac]*}
+text {*
+There is even another variant for @{ML foo_tac''}: in automatic proof
+procedures (in contrast to tactics that might be called by the user)
+there are often long lists of tactics that are applied to the first
+subgoal. Instead of writing the code above and then calling
+@{ML "foo_tac'' 1"}, you can also just write
+*}
+ML{*val foo_tac1 = EVERY1 [etac @{thm disjE}, rtac @{thm disjI2},
+atac, rtac @{thm disjI1}, atac]*}
+text {*
+With the combinators @{ML THEN'}, @{ML EVERY'} and @{ML EVERY1} it must be
+guaranteed that  all component tactics sucessfully apply; otherwise the
+whole tactic will fail. If you rather want to try out a number of tactics,
+then you can use the combinator @{ML ORELSE'} for two tactics and @{ML FIRST'}
+(or @{ML FIRST1}) for a list of tactics. For example, the tactic
 *}
 ML{*val orelse_xmp = (rtac @{thm disjI1} ORELSE' rtac @{thm conjI})*}
 text {*
-will first try out rule @{text disjI} and after that @{text conjI}.
+will first try out whether rule @{text disjI} applies and after that
+whether @{text conjI}. To see this consider the proof:
 *}
 lemma shows "True \<and> False" and "Foo \<or> Bar"
 apply(tactic {* orelse_xmp 1 *})
 apply(tactic {* orelse_xmp 3 *})
-txt {* @{subgoals [display]} *}
+txt {* which results in the goal state
-(*<*)oops(*>*)
+\begin{minipage}{\textwidth}
+@{subgoals [display]}
-text {*
+\end{minipage}
-applies
+*}
+(*<*)oops(*>*)
+text {*
+Using @{ML FIRST'} we can write our @{ML select_tac} from Page~\ref{tac:selecttac}
+simply as follows:
+*}
+ML{*val select_tac' = FIRST' [rtac @{thm conjI}, rtac @{thm impI},
+rtac @{thm notI}, rtac @{thm allI}, K all_tac]*}
+text {*
+Since we like to mimic the bahaviour of @{ML select_tac}, we must include
+@{ML all_tac} at the end (@{ML all_tac} must also be ``wrapped up'' using
+the @{ML K}-combinator as it does not take a subgoal number as argument).
+We can test the tactic on the same proof:
+*}
+lemma shows "A \<and> B" and "A \<longrightarrow> B \<longrightarrow>C" and "\<forall>x. D x" and "E \<Longrightarrow> F"
+apply(tactic {* select_tac' 4 *})
+apply(tactic {* select_tac' 3 *})
+apply(tactic {* select_tac' 2 *})
+apply(tactic {* select_tac' 1 *})
+txt{* \begin{minipage}{\textwidth}
+@{subgoals [display]}
+\end{minipage} *}
+(*<*)oops(*>*)
+text {*
+and obtain the same subgoals. Since this repeated application of a tactic
+to the reverse order of \emph{all} subgoals is quite common, there is
+the tactics combinator @{ML ALLGOALS} that simplifies this. Using this
+combinator we can simply write: *}
+lemma shows "A \<and> B" and "A \<longrightarrow> B \<longrightarrow>C" and "\<forall>x. D x" and "E \<Longrightarrow> F"
+apply(tactic {* ALLGOALS select_tac' *})
+txt{* \begin{minipage}{\textwidth}
+@{subgoals [display]}
+\end{minipage} *}
+(*<*)oops(*>*)
+text {*
+We chose to write @{ML select_tac'} in such a way that it always succeeds.
+This can be potetially very  confusing for the user in cases of goals
+of the form
+*}
+lemma shows "E \<Longrightarrow> F"
+apply(tactic {* select_tac' 1 *})
+txt{* \begin{minipage}{\textwidth}
+@{subgoals [display]}
+\end{minipage} *}
+(*<*)oops(*>*)
+text {*
+where no rule applies. The reason is that the user has little chance
+to see whether progress in the proof has been made or not. We could simply
+remove @{ML "K all_tac"} from the end of the list. Then the tactic would
+only apply in cases where it can make some progress. But for the sake of
+argument, let us assume that this is not an option. In such cases, you
+can use the combinator @{ML CHANGED} to make sure the subgoal has been
+changed by the tactic. Because now
+*}
+lemma shows "E \<Longrightarrow> F"
+apply(tactic {* CHANGED (select_tac' 1) *})(*<*)?(*>*)
+txt{* results in the usual error message for empty result sequences. *}
+(*<*)oops(*>*)
+text {*
 @{ML REPEAT} @{ML DETERM}
+@{ML CHANGED}
 *}
 section {* Rewriting and Simplifier Tactics *}

changeset 107	258ce361ba1b
parent 105	f49dc7e96235
child 108	8bea3f74889d