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




