--- a/CookBook/Solutions.thy	Sun Feb 22 03:44:03 2009 +0000
+++ b/CookBook/Solutions.thy	Sun Feb 22 13:37:47 2009 +0000
@@ -8,20 +8,20 @@
 
 ML{*fun rev_sum t =
 let
- fun dest_sum (Const (@{const_name plus}, _) $ u $ u') = u' :: dest_sum u
-   | dest_sum u = [u]
- in
+  fun dest_sum (Const (@{const_name plus}, _) $ u $ u') = u' :: dest_sum u
+    | dest_sum u = [u]
+in
    foldl1 (HOLogic.mk_binop @{const_name plus}) (dest_sum t)
- end *}
+end *}
 
 text {* \solution{fun:makesum} *}
 
 ML{*fun make_sum t1 t2 =
-    HOLogic.mk_nat (HOLogic.dest_nat t1 + HOLogic.dest_nat t2) *}
+      HOLogic.mk_nat (HOLogic.dest_nat t1 + HOLogic.dest_nat t2) *}
 
 text {* \solution{ex:scancmts} *}
 
-ML{*val any = Scan.one (Symbol.not_eof);
+ML{*val any = Scan.one (Symbol.not_eof)
 
 val scan_cmt =
   let
@@ -32,9 +32,10 @@
     >> (enclose "(**" "**)" o implode)
   end
 
+val parser = Scan.repeat (scan_cmt || any)
+
 val scan_all =
-  Scan.finite Symbol.stopper (Scan.repeat (scan_cmt || any)) 
-    >> implode #> fst *}
+  Scan.finite Symbol.stopper parser >> implode #> fst *}
 
 text {*
   By using @{text "#> fst"} in the last line, the function 
@@ -43,12 +44,55 @@
 
   @{ML_response [display,gray]
 "let
-   val input1 = (explode \"foo bar\")
-   val input2 = (explode \"foo (*test*) bar (*test*)\")
- in
-   (scan_all input1, scan_all input2)
- end"
-"(\"foo bar\",\"foo (**test**) bar (**test**)\")"}
+  val input1 = (explode \"foo bar\")
+  val input2 = (explode \"foo (*test*) bar (*test*)\")
+in
+  (scan_all input1, scan_all input2)
+end"
+"(\"foo bar\", \"foo (**test**) bar (**test**)\")"}
 *}
 
+text {* \solution{ex:addsimproc} *}
+
+ML{*fun dest_sum term =
+  case term of 
+    (@{term "(op +):: nat \<Rightarrow> nat \<Rightarrow> nat"} $ t1 $ t2) =>
+        (snd (HOLogic.dest_number t1), snd (HOLogic.dest_number t2))
+  | _ => raise TERM ("dest_sum", [term])
+
+fun get_sum_thm ctxt t (n1, n2) =  
+let 
+  val sum = HOLogic.mk_number @{typ "nat"} (n1 + n2)
+  val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, sum))
+in
+  mk_meta_eq (Goal.prove ctxt [] [] goal (K (simp_tac @{simpset} 1)))
+end
+
+fun add_sp_aux ss t =
+let 
+  val ctxt = Simplifier.the_context ss
+  val t' = term_of t
+in
+  SOME (get_sum_thm ctxt t' (dest_sum t'))
+  handle TERM _ => NONE
+end*}
+
+text {* The setup for the simproc is *}
+
+simproc_setup add_sp ("t1 + t2") = {* K add_sp_aux *}
+ 
+text {* and a test case is the lemma *}
+
+lemma "P (Suc (99 + 1)) ((0 + 0)::nat) (Suc (3 + 3 + 3)) (4 + 1)"
+  apply(tactic {* simp_tac (HOL_ss addsimprocs [@{simproc add_sp}]) 1 *})
+txt {* 
+  where the simproc produces the goal state
+  
+  \begin{minipage}{\textwidth}
+  @{subgoals [display]}
+  \end{minipage}
+*}(*<*)oops(*>*)
+
+
+
 end
\ No newline at end of file