
diff -r 8db9195bb3e9 -r 2d9198bcb850 CookBook/Tactical.thy
--- a/CookBook/Tactical.thy	Mon Feb 23 00:27:27 2009 +0000
+++ b/CookBook/Tactical.thy	Mon Feb 23 17:08:15 2009 +0000
@@ -68,8 +68,6 @@
   Isabelle Reference Manual.
   \end{readmore}
 
-  (FIXME:  what is @{ML Goal.prove_global}?) 
-
   Note that in the code above we use 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 where there are no ML-binding obtain
@@ -210,11 +208,11 @@
 *}
 
 ML{*fun my_print_tac ctxt thm =
- let
-   val _ = warning (str_of_thm ctxt thm)
- in 
-   Seq.single thm
- end*}
+let
+  val _ = warning (str_of_thm ctxt thm)
+in 
+  Seq.single thm
+end*}
 
 text_raw {*
   \begin{figure}[p]
@@ -537,21 +535,21 @@
 \begin{isabelle}
 *}
 ML{*fun sp_tac {prems, params, asms, concl, context, schematics} = 
-  let 
-    val str_of_params = str_of_cterms context params
-    val str_of_asms = str_of_cterms context asms
-    val str_of_concl = str_of_cterm context concl
-    val str_of_prems = str_of_thms context prems   
-    val str_of_schms = str_of_cterms context (snd schematics)    
+let 
+  val str_of_params = str_of_cterms context params
+  val str_of_asms = str_of_cterms context asms
+  val str_of_concl = str_of_cterm context concl
+  val str_of_prems = str_of_thms context prems   
+  val str_of_schms = str_of_cterms context (snd schematics)    
  
-    val _ = (warning ("params: " ^ str_of_params);
-             warning ("schematics: " ^ str_of_schms);
-             warning ("assumptions: " ^ str_of_asms);
-             warning ("conclusion: " ^ str_of_concl);
-             warning ("premises: " ^ str_of_prems))
-  in
-    no_tac 
-  end*}
+  val _ = (warning ("params: " ^ str_of_params);
+           warning ("schematics: " ^ str_of_schms);
+           warning ("assumptions: " ^ str_of_asms);
+           warning ("conclusion: " ^ str_of_concl);
+           warning ("premises: " ^ str_of_prems))
+in
+  no_tac 
+end*}
 text_raw{*
 \end{isabelle}
 \caption{A function that prints out the various parameters provided by the tactic
@@ -1032,7 +1030,7 @@
   simplification is too unpredictable and potentially loops.
 
   To see how simprocs work, let us first write a simproc that just prints out
-  the pattern that triggers it and otherwise does nothing. For this
+  the pattern which triggers it and otherwise does nothing. For this
   you can use the function:
 *}
 
@@ -1046,7 +1044,7 @@
 
 text {*
   This function takes a simpset and a redex (a @{ML_type cterm}) as
-  argument. In Lines 3 and~4, we first extract the context from the given
+  arguments. In Lines 3 and~4, we first extract the context from the given
   simpset and then print out a message containing the redex.  The function
   returns @{ML NONE} (standing for an optional @{ML_type thm}) since at the
   moment we are \emph{not} interested in actually rewriting anything. We want
@@ -1075,8 +1073,8 @@
   0"}, and then the simproc ``fires'' also on that term. 
 
   We can add or delete the simproc from the current simpset by the usual 
-  \isacommand{declare}-statement. For example the simproc will be deleted 
-  if you type:
+  \isacommand{declare}-statement. For example the simproc will be deleted
+  with the declaration
 *}
 
 declare [[simproc del: fail_sp]]
@@ -1088,12 +1086,10 @@
 *}
 
 lemma shows "Suc 0 = 1"
-  apply(tactic {* simp_tac (HOL_ss addsimprocs [@{simproc fail_sp}]) 1*})
+  apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [@{simproc fail_sp}]) 1*})
 (*<*)oops(*>*)
 
 text {*
-  (FIXME: should one use HOL-basic-ss or HOL-ss?)
-
   Now the message shows up only once since the term @{term "1::nat"} is 
   left unchanged. 
 
@@ -1130,8 +1126,12 @@
 text {*
   Here the pattern is given as @{ML_type term} (instead of @{ML_type cterm}).
   The function also takes a list of patterns that can trigger the simproc.
-  It might be interesting to notice that simprocs are applied from inside 
-  to outside and from left to right. You can see this in the proof
+  Now the simproc is set up and can be explicitly added using
+  {ML addsimprocs} to a simpset whenerver
+  needed. 
+
+  Simprocs are applied from inside to outside and from left to right. You can
+  see this in the proof
 *}
 
 lemma shows "Suc (Suc 0) = (Suc 1)"
@@ -1139,7 +1139,7 @@
 (*<*)oops(*>*)
 
 text {*
-  since @{ML fail_sp'} prints out the sequence 
+  The simproc @{ML fail_sp'} prints out the sequence 
 
 @{text [display]
 "> Suc 0
@@ -1156,7 +1156,7 @@
 text {*
   Simprocs expect that the given equation is a meta-equation, however the
   equation can contain preconditions (the simproc then will only fire if the
-  preconditions can be solved). To see one has relatively precise control over
+  preconditions can be solved). To see that one has relatively precise control over
   the rewriting with simprocs, let us further assume we want that the simproc
   only rewrites terms ``greater'' than @{term "Suc 0"}. For this we can write 
 *}
@@ -1180,7 +1180,7 @@
   end*}
 
 text {*
-  Now the simproc is set up xso that it is triggered by terms
+  Now the simproc is set up so that it is triggered by terms
   of the form @{term "Suc n"}, but inside the simproc we only produce
   a theorem if the term is not @{term "Suc 0"}. The result you can see
   in the following proof
@@ -1196,14 +1196,15 @@
 (*<*)oops(*>*)
 
 text {*
-  As usual with simplification you have to be careful with looping: you already have
-  one @{ML plus_one_sp}, if you apply if with the default simpset (because
-  the default simpset contains a rule which just undoes the rewriting 
-  @{ML plus_one_sp}).
+  As usual with simplification you have to worry about looping: you already have
+  a loop with @{ML plus_one_sp}, if you apply it with the default simpset (because
+  the default simpset contains a rule which just does the opposite of @{ML plus_one_sp},
+  namely rewriting @{text [quotes] "+ 1"} to a successor). So you have to be careful 
+  in choosing the right simpset to which you add a simproc. 
 
-  Let us next implement a simproc that replaces terms of the form @{term "Suc n"}
+  Next let us implement a simproc that replaces terms of the form @{term "Suc n"}
   with the number @{text n} increase by one. First we implement a function that
-  takes a term and produces the corresponding integer value, if it can.
+  takes a term and produces the corresponding integer value.
 
 *}
 
@@ -1221,21 +1222,45 @@
 ML %linenosgray{*fun get_thm ctxt (t, n) =
 let
   val num = HOLogic.mk_number @{typ "nat"} n
-  val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (t,num))
+  val goal = Logic.mk_equals (t, num)
 in
-  mk_meta_eq (Goal.prove ctxt [] [] goal (K (simp_tac @{simpset} 1)))
+  Goal.prove ctxt [] [] goal (K (arith_tac ctxt 1))
 end*}
 
 text {*
-  (FIXME: is @{text "@{simpset}"} kosher here? Otherwise the following will loop.)
+  From the integer value it generates the corresponding number term, called 
+  @{text num} (Line 3), and then generates the meta-equation @{text "t \<equiv> num"} 
+  (Line 4), which it proves by the arithmetic tactic in Line 6. 
+
+  For our purpose at the moment, using in the code above @{ML arith_tac} is
+  fine, but there is also an alternative employing the simplifier with a very
+  restricted simpset. For the kind of lemmas we want to prove, the simpset
+  @{text "num_ss"} in the code will suffice.
+*}
 
-  From the integer value it generates the corresponding number term, called 
-  @{text num} (Line 3), and then generates the equation @{text "t = num"} (Line 4),
-  which it proves by simplification in Line 6. The function @{ML mk_meta_eq} 
-  at the outside of the proof just transforms the equality into a meta-equality.
+ML{*fun get_thm_alt ctxt (t, n) =
+let
+  val num = HOLogic.mk_number @{typ "nat"} n
+  val goal = Logic.mk_equals (t, num)
+  val num_ss = HOL_ss addsimps [@{thm One_nat_def}, @{thm Let_def}] @ 
+          @{thms nat_number} @ @{thms neg_simps} @ @{thms plus_nat.simps}
+in
+  Goal.prove ctxt [] [] goal (K (simp_tac num_ss 1))
+end*}
 
-  Both functions can be stringed together in the function that produces the 
-  actual theorem for the simproc.
+text {*
+  The advantage of @{ML get_thm_alt} is that it leaves very little room for 
+  something to go wrong; in contrast it is much more difficult to predict 
+  what happens with @{ML arith_tac}, especially in more complicated 
+  circumstances. The disatvantage of @{ML get_thm_alt} is to find a simpset
+  that is sufficiently powerful to solve every instance of the lemmas
+  we like to prove. This requires careful tuning, but is often necessary in 
+  ``production code''.\footnote{It would be of great help if there is another
+  way than tracing the simplifier to obtain the lemmas that are successfully 
+  applied during simplification. Alas, there is none.} 
+
+  Anyway, either version can be used in the function that produces the actual 
+  theorem for the simproc.
 *}
 
 ML{*fun nat_number_sp_aux ss t =
@@ -1254,12 +1279,12 @@
 *}
 
 ML{*val nat_number_sp =
-  let
-    val thy = @{theory}
-    val pat = [@{term "Suc n"}]
-  in 
-    Simplifier.simproc_i thy "nat_number" pat (K nat_number_sp_aux) 
-  end*}
+let
+  val thy = @{theory}
+  val pat = [@{term "Suc n"}]
+in 
+  Simplifier.simproc_i thy "nat_number" pat (K nat_number_sp_aux) 
+end*}
 
 text {* 
   Now in the lemma
@@ -1275,7 +1300,7 @@
 (*<*)oops(*>*)
 
 text {*
-  where the simproc rewrites all @{term "Suc"}s except in the last arguments. There it cannot 
+  where the simproc rewrites all @{term "Suc"}s except in the last argument. There it cannot 
   rewrite anything, because it does not know how to transform the term @{term "Suc (0 + 0)"}
   into a number. To solve this problem have a look at the next exercise. 
 
@@ -1289,6 +1314,9 @@
   one can say about them?)
 *}
 
+section {* Conversions *}
+
+
 section {* Structured Proofs *}
 
 text {* TBD *}




