
diff -r fe10da5354a3 -r 5dcad9348e4d CookBook/Tactical.thy
--- a/CookBook/Tactical.thy	Sat Feb 07 14:21:33 2009 +0000
+++ b/CookBook/Tactical.thy	Sun Feb 08 08:45:25 2009 +0000
@@ -100,8 +100,8 @@
 done
 
 text {*
-  By using @{text "tactic \<verbopen> \<dots> \<verbclose>"} in the apply-step,
-  you can call from the user level of Isabelle the tactic @{ML foo_tac} or 
+  By using @{text "tactic \<verbopen> \<dots> \<verbclose>"} you can call from the 
+  user level of Isabelle the tactic @{ML foo_tac} or 
   any other function that returns a tactic.
 
   The tactic @{ML foo_tac} is just a sequence of simple tactics stringed
@@ -196,10 +196,10 @@
   instead.
   \end{readmore}
 
-  For a beginner it might be surprising that tactics, which transform
+  It might be surprising that tactics, which transform
   one proof state to the next, are functions from theorems to theorem 
   (sequences). The surprise resolves by knowing that every 
-  proof state is indeed a theorem. To shed more light on this,
+  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
 *}
@@ -216,7 +216,7 @@
   in Section~\ref{sec:printing}) and then behaves like @{ML all_tac}. We
   now can inspect every proof state in the follwing proof. On the left-hand
   side we show the goal state as shown by the system; on the right-hand
-  side the print out from our @{ML my_print_tac}.
+  side the print out from @{ML my_print_tac}.
 *}
 
 lemma shows "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"
@@ -275,9 +275,12 @@
   @{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. Since the goal @{term C} can potentially be an implication, 
-  there is a protector (invisible in the print out above) wrapped around 
-  it. This prevents that premises are misinterpreted as open subgoals. 
+  subgoals. So in the first step the goal state is always of the form
+  @{text "C \<Longrightarrow> (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 are misinterpreted 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. 
@@ -297,23 +300,30 @@
 text {*
   Similarly, @{ML rtac}, @{ML dtac}, @{ML etac} and @{ML ftac} correspond
   to @{text rule}, @{text drule}, @{text erule} and @{text frule}, 
-  respectively. Below are three examples with the resulting goal state. How
-  they work should therefore be self-explanatory.  
+  respectively. Each of them takes a theorem as argument. Below are three 
+  examples with the resulting goal state. How
+  they work should be self-explanatory.  
 *}
 
 lemma shows "P \<and> Q"
 apply(tactic {* rtac @{thm conjI} 1 *})
-txt{*@{subgoals [display]}*}
+txt{*\begin{minipage}{\textwidth}
+     @{subgoals [display]}
+     \end{minipage}*}
 (*<*)oops(*>*)
 
 lemma shows "P \<and> Q \<Longrightarrow> False"
 apply(tactic {* etac @{thm conjE} 1 *})
-txt{*@{subgoals [display]}*}
+txt{*\begin{minipage}{\textwidth}
+     @{subgoals [display]}
+     \end{minipage}*}
 (*<*)oops(*>*)
 
 lemma shows "False \<and> True \<Longrightarrow> False"
 apply(tactic {* dtac @{thm conjunct2} 1 *})
-txt{*@{subgoals [display]}*}
+txt{*\begin{minipage}{\textwidth}
+     @{subgoals [display]}
+     \end{minipage}*}
 (*<*)oops(*>*)
 
 text {*
@@ -323,7 +333,9 @@
 
 lemma shows "Foo" and "P \<and> Q"
 apply(tactic {* rtac @{thm conjI} 2 *})
-txt {*@{subgoals [display]}*}
+txt {*\begin{minipage}{\textwidth}
+      @{subgoals [display]}
+      \end{minipage}*}
 (*<*)oops(*>*)
 
 text {* 
@@ -343,7 +355,9 @@
 lemma shows "C \<longrightarrow> (A \<and> B)" and "(A \<longrightarrow> B) \<and> C"
 apply(tactic {* resolve_tac_xmp 1 *})
 apply(tactic {* resolve_tac_xmp 2 *})
-txt{* @{subgoals [display]} *}
+txt{*\begin{minipage}{\textwidth}
+     @{subgoals [display]} 
+     \end{minipage}*}
 (*<*)oops(*>*)
 
 text {* 
@@ -359,15 +373,12 @@
 (*<*)oops(*>*)
 
 text {*
-  Also for useful for debugging purposes are the tactics @{ML all_tac} and
-  @{ML no_tac}. The former always succeeds (but does not change the goal state), and
-  the latter always fails.
-
+  
   (FIXME explain RS MRS)
 
-  Often proofs involve elaborate operations on assumptions and variables
-  @{text "\<And>"}-quantified in the goal state. To do such operations on the ML-level 
-  using the basic tactics, is very unwieldy and brittle. Some convenience and
+  Often proofs involve elaborate operations on assumptions and 
+  @{text "\<And>"}-quantified variables. To do such operations on the ML-level 
+  using the basic tactics 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. 
 *}
@@ -426,15 +437,15 @@
   Note in the actual output the brown colour of the variables @{term x} and 
   @{term y}. Although parameters in the original goal, they are fixed inside
   the subproof. Similarly the schematic variable @{term z}. The assumption 
-  is bound once as @{ML_type cterm} to the record-variable @{text asms} and 
-  another time as @{ML_type thm} to @{text prems}.
+  @{prop "A x y"} is bound once as @{ML_type cterm} to the record-variable 
+  @{text asms} and another time as @{ML_type thm} to @{text prems}.
 
   Notice also that we had to append @{text "?"} to \isacommand{apply}. The 
   reason is that @{ML SUBPROOF} normally expects that the subgoal is solved completely.
   Since in the function @{ML sp_tac} we returned the tactic @{ML no_tac}, the subproof
   obviously fails. The question-mark allows us to recover from this failure
   in a graceful manner so that the warning messages are not overwritten
-  by the error message.
+  by an error message.
 
   If we continue the proof script by applying the @{text impI}-rule
 *}
@@ -458,7 +469,7 @@
 (*<*)oops(*>*)
 
 text {*
-  where we now also have @{term "B y x"} as assumption.
+  where we now also have @{term "B y x"} as an assumption.
 
   One convenience of @{ML SUBPROOF} is that we can apply assumption
   using the usual tactics, because the parameter @{text prems} 
@@ -466,23 +477,42 @@
   implement a tactic that almost behaves like @{ML atac}:
 *}
 
+ML{*val atac' = SUBPROOF (fn {prems, ...} => resolve_tac prems 1)*}
 lemma shows "\<And>x y. \<lbrakk>B x y; A x y; C x y\<rbrakk> \<Longrightarrow> A x y"
-apply(tactic 
-       {* SUBPROOF (fn {prems, ...} => resolve_tac prems 1) @{context} 1 *})
+apply(tactic {* atac' @{context} 1 *})
 txt{* yields
       @{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
+  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 proof inside. It is therefore possible to also apply 
+  @{ML atac'} to the second goal:
+*}
+
+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 *})
+txt{* This gives:
+      @{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
-  an advantage in the situations for which @{ML SUBPROOF} was designed: 
-  the reason is that instantiation of schematic variables can potentially 
-  has affect several goals and can render them unprovable.  
-
-  A similar but less powerful function is @{ML SUBGOAL}. It allows you to 
-  inspect a subgoal specified by a number. 
+  A similar but less powerful function than @{ML SUBPROOF} is @{ML SUBGOAL}. 
+  It allows you to inspect a subgoal specified by a number. With this we can 
+  implement a little tactic that applies a rule corresponding to its 
+  topmost connective. The tactic should only apply ``safe'' rules (that is
+  which do not render the goal unprovable). For this we can write:
 *}
 
 ML %linenumbers{*fun select_tac (t,i) =
@@ -492,12 +522,13 @@
    | @{term "op \<longrightarrow>"} $ _ $ _ => rtac @{thm impI} i
    | @{term "Not"} $ _ => rtac @{thm notI} i
    | Const (@{const_name "All"}, _) $ _ => rtac @{thm allI} i
-   | _ => no_tac*}
+   | _ => all_tac*}
 
-lemma shows "A \<and> B" "A \<longrightarrow> B" "\<forall>x. C x"
+lemma shows "A \<and> B" "A \<longrightarrow> B" "\<forall>x. C x" "D \<Longrightarrow> E"
+apply(tactic {* SUBGOAL select_tac 4 *})
+apply(tactic {* SUBGOAL select_tac 3 *})
+apply(tactic {* SUBGOAL select_tac 2 *})
 apply(tactic {* SUBGOAL select_tac 1 *})
-apply(tactic {* SUBGOAL select_tac 3 *})
-apply(tactic {* SUBGOAL select_tac 4 *})
 txt{* @{subgoals [display]} *}
 (*<*)oops(*>*)
 
@@ -506,6 +537,8 @@
   to implement a proof procedure like the one above. They will be explained
   in the next section.
 
+  (Notice that we applied the goals in reverse order)
+
   A variant of @{ML SUBGOAL} is @{ML CSUBGOAL} which allows access to the goal
   as @{ML_type cterm} instead of a @{ML_type term}.
 *}




