
diff -r 258ce361ba1b -r 8bea3f74889d CookBook/Tactical.thy
--- a/CookBook/Tactical.thy	Mon Feb 09 04:18:14 2009 +0000
+++ b/CookBook/Tactical.thy	Wed Feb 11 17:40:24 2009 +0000
@@ -21,7 +21,7 @@
 
 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"
@@ -62,18 +62,17 @@
 
   \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
-  internals of goals see \isccite{sec:tactical-goals}.  See @{ML_file
+  and the file @{ML_file "Pure/goal.ML"}.  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
@@ -133,7 +132,7 @@
 
 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
@@ -175,7 +174,7 @@
 
   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.
 *}
 
@@ -215,7 +214,7 @@
 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}.
 *}
@@ -224,48 +223,48 @@
 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)"}
-      \end{tabular}
+      @{text "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}
+      \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)"}
-      \end{tabular}
+      @{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}
 *}
 
 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)"}
-      \end{tabular}
+      @{text "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> B) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}
+      \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"}
-      \end{tabular}
+      @{text "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"}
+      \end{tabularstar}
 *}
 
 done
@@ -277,7 +276,7 @@
 
   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;
@@ -285,8 +284,13 @@
   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 *}
@@ -396,16 +400,33 @@
 
 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
+  procedure might become too fragile, if it just applies inference rules as 
+  shown above. The reason is that a number of rules introduce meta-variables 
+  into the goal state. Consider for example the proof
+*}
+
+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
-  rule @{text disjI1}. If this is impossible, as in the case of
+  which, for instance, instantiates the first premise of the @{text conjI}-rule 
+  with the rule @{text disjI1}. If this is impossible, as in the case of
 
   @{ML_response_fake_both [display,gray]
   "@{thm conjI} RS @{thm mp}" 
@@ -613,7 +634,7 @@
    | _ => 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
@@ -621,7 +642,7 @@
   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). 
 
@@ -643,7 +664,7 @@
   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"
@@ -659,7 +680,7 @@
   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.
 *}
@@ -668,7 +689,7 @@
 
 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:
 *}
 
@@ -681,7 +702,7 @@
 
 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"
@@ -698,28 +719,27 @@
   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
-  procedures (in contrast to tactics that might be called by the user) 
-  there are often long lists of tactics that are applied to the first
-  subgoal. Instead of writing the code above and then calling 
-  @{ML "foo_tac'' 1"}, you can also just write
+  There is even another way: 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]*}
+                       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
 *}
 
@@ -731,8 +751,8 @@
 *}
 
 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}
@@ -751,10 +771,10 @@
                           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:
+  Since we like to mimic the behaviour of @{ML select_tac} as closely as possible, 
+  we must include @{ML all_tac} at the end of the list (@{ML all_tac} must also 
+  be ``wrapped up'' using the @{ML K}-combinator, as it does not take a subgoal 
+  number as argument). We can test the tactic on the same proof:
 *}
 
 lemma shows "A \<and> B" and "A \<longrightarrow> B \<longrightarrow>C" and "\<forall>x. D x" and "E \<Longrightarrow> F"
@@ -768,10 +788,10 @@
 (*<*)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: *}
+  Because such repeated applications of a tactic to the reverse order of 
+  \emph{all} subgoals is quite common, there is the tactics combinator 
+  @{ML ALLGOALS} that simplifies this. Using this combinator we can simply 
+  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' *})
@@ -781,9 +801,9 @@
 (*<*)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
+  Remember that we chose to write @{ML select_tac'} in such a way that it always 
+  succeeds. This can be potentially very confusing for the user, for example,  
+  in cases the goals is the form
 *}
 
 lemma shows "E \<Longrightarrow> F"
@@ -796,24 +816,131 @@
 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 
+  delete th @{ML "K all_tac"} from the end of the list. Then @{ML select_tac'} 
+  would only succeed on goals where it can make progress. But for the sake of
+  argument, let us suppose that this deletion is not an option. In such cases, you 
   can use the combinator @{ML CHANGED} to make sure the subgoal has been
   changed by the tactic. Because now
 *}
 
 lemma shows "E \<Longrightarrow> F"
 apply(tactic {* CHANGED (select_tac' 1) *})(*<*)?(*>*)
-txt{* results in the usual error message for empty result sequences. *}
-(*<*)oops(*>*)
+txt{* results in the error message:
+  \begin{isabelle}
+  @{text "*** empty result sequence -- proof command failed"}\\
+  @{text "*** At command \"apply\"."}
+  \end{isabelle} 
+*}(*<*)oops(*>*)
 
 
 text {*
+  Meaning the tactic failed. 
 
-  @{ML REPEAT} @{ML DETERM}
+  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(*>*)
 
-  @{ML CHANGED}
+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}
 
 *}
 




