diff -r 693711a0c702 -r e0d368a45537 CookBook/Tactical.thy
--- a/CookBook/Tactical.thy	Sat Feb 21 11:38:14 2009 +0000
+++ b/CookBook/Tactical.thy	Sun Feb 22 03:44:03 2009 +0000
@@ -68,6 +68,8 @@
   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
@@ -1018,13 +1020,211 @@
   
   @{ML ObjectLogic.rulify_tac}
 
-  Something about simprocs.
+*}
+
+section {* Simprocs *}
+
+text {*
+  In Isabelle you can also implement custom simplification procedures, called
+  \emph{simprocs}. Simprocs can be triggered on a specified term-pattern and
+  rewrite a term according to a given theorem. They are useful in cases where
+  a rewriting rule must be produced on ``demand'' or when rewriting by
+  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
+  you can use the function:
+*}
+
+ML %linenosgray{*fun fail_sp_aux simpset redex = 
+let
+  val ctxt = Simplifier.the_context simpset
+  val _ = warning ("The redex: " ^ (str_of_cterm ctxt redex))
+in
+  NONE
+end*}
+
+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
+  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
+  that the simproc is triggered by the pattern @{term "Suc n"}. For this we
+  can add the simproc with this pattern to the current simpset as follows
+*}
+
+simproc_setup fail_sp ("Suc n") = {* K fail_sp_aux *}
+
+text {*
+  where the second argument specifies the pattern and the right-hand side
+  contains the code of the simproc (we have to use @{ML K} since we ignoring
+  an argument). After this setup, the simplifier is aware of
+  this simproc and you can test whether it fires with the lemma
+*}
 
+lemma shows "Suc 0 = 1"
+apply(simp)
+(*<*)oops(*>*)
+
+text {*
+  This will print out the message twice: once for the left-hand side and
+  once for the right-hand side. This is because during simplification the
+  simplifier will by default reduce the term @{term "1::nat"} to @{term "Suc
+  0"}, and then the simproc ``fires'' also on that term. 
+
+  We can add or delete the simproc by the usual methods. For example
+  the simproc will be deleted by the declaration:
+*}
+
+declare [[simproc del: fail_sp]]
+
+text {*
+  If you want to see what happens with just \emph{this} simproc, without any 
+  interference from other rewrite rules, you can call @{text fail_sp} 
+  as follows:
+*}
+
+lemma shows "Suc 0 = 1"
+apply(tactic {* simp_tac (HOL_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. 
+
+  Setting up a simproc using the command \isacommand{setup\_simproc} will
+  always add automatically the simproc to the current simpset. If you do not
+  want this, then you have to use a slightly different method for setting 
+  up the simproc. First the function @{ML fail_sp_aux} needs to be modified
+  to
+*}
+
+ML{*fun fail_sp_aux' simpset redex = 
+let
+  val ctxt = Simplifier.the_context simpset
+  val _ = warning ("The redex: " ^ (Syntax.string_of_term ctxt redex))
+in
+  NONE
+end*}
+
+text {*
+  Here the redex is given as a @{ML_type term}, instead of a @{ML_type cterm}.
+  We can turn this function into a simproc using
 *}
 
 
+ML{*val fail_sp' = 
+      Simplifier.simproc_i @{theory} "fail_sp'" [@{term "Suc n"}] 
+        (K fail_sp_aux')*}
+
+text {*
+  Here the pattern is given as @{ML_type term} (instead of @{ML_type cterm}).
+
+  Simprocs are applied from inside to outside, from left to right. You can see
+  this in the proof
+*}
+
+lemma shows "Suc (Suc 0) = (Suc 1)"
+apply(tactic {* simp_tac (HOL_ss addsimprocs [fail_sp']) 1*})
+(*<*)oops(*>*)
+
+text {*
+  since it prints out the sequence @{term "Suc 0"}, @{term "Suc (Suc 0)"} and 
+  @{term "Suc 1"}.
+
+  To see how a simproc applies a theorem  let us rewrite terms according to the 
+  equation:
+*}
+
+lemma plus_one: 
+  shows "Suc n \<equiv> n + 1" by simp
+
+text {*
+  The simproc expects the equation to be a meta-equation, however it can contain 
+  possible preconditions (the simproc then only fires if the preconditions can be 
+  solved). Let us further assume we want to only rewrite terms greater than 
+  @{term "Suc 0"}. For this we can write
+*}
+
+ML{*fun plus_one_sp_aux thy ss redex =
+  case redex of
+    @{term "Suc 0"} => NONE
+  | _ => SOME @{thm plus_one}*}
+
+text {*
+  and set up the simproc as follows.
+*}
+
+ML{*val plus_one_sproc = 
+       Simplifier.simproc_i @{theory} "sproc +1" [@{term "Suc n"}] 
+         plus_one_sp_aux*}
+
+text {*
+  Now the simproc fires one every term of the for @{term "Suc n"}, but
+  the lemma is only applied whenever the term is not @{term "Suc 0"}. So
+  in 
+*}
+
+lemma shows "P (Suc (Suc (Suc 0))) (Suc 0)"
+apply(tactic {* simp_tac (HOL_ss addsimprocs [plus_one_sproc]) 1*})
+txt{*
+  the simproc produces the goal state
+
+  @{subgoals[display]}
+*}  
+(*<*)oops(*>*)
+
+text {*
+  where the first argument is rewritten, but not the second. With @{ML
+  plus_one_sproc} you already have to be careful to not cause the simplifier
+  to loop. If we call this simproc together with the default simpset, we
+  already have a loop as it contains a rule which just undoes the rewriting of
+  the simproc.
+*}
+
+ML{*fun dest_suc_trm ((Const (@{const_name "Suc"}, _)) $ t) = 1 + dest_suc_trm t
+  | dest_suc_trm t = snd (HOLogic.dest_number t)*}
+
+text {* This function might raise @{ML TERM}. *}
+
+ML{*fun nat_number_sp_aux ss t =
+let 
+  val ctxt = Simplifier.the_context ss
+
+  fun get_thm (t, n) =
+  let
+    val num = HOLogic.mk_number @{typ "nat"} n
+    val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (t,num))
+  in
+    Goal.prove ctxt [] [] goal (K (simp_tac @{simpset} 1))
+  end
+in
+  SOME (mk_meta_eq (get_thm (t,dest_suc_trm t)))
+  handle TERM _ => NONE
+end*}
+
+text {*
+  (FIXME: is @{text "@{simpset}"} kosher here? Otherwise the following loops.)
+*}
+
+ML{*val nat_number_sp = 
+       Simplifier.simproc_i @{theory} "nat_number" [@{term "Suc n"}] 
+         (K nat_number_sp_aux) *}
+
+lemma "P (Suc (Suc 2)) (Suc 99) (0::nat) (Suc 4 + Suc 0) (Suc (0 + 0))"
+  apply(tactic {* simp_tac (HOL_ss addsimprocs [nat_number_sp]) 1*})
+txt {* 
+  @{subgoals [display]}
+  *}
+(*<*)oops(*>*)
+
+
 section {* Structured Proofs *}
 
+text {* TBD *}
+
 lemma True
 proof