--- a/CookBook/Solutions.thy	Thu Feb 26 13:46:05 2009 +0100
+++ b/CookBook/Solutions.thy	Thu Mar 12 08:11:02 2009 +0100
@@ -1,8 +1,8 @@
 theory Solutions
-imports Base
+imports Base 
 begin
 
-chapter {* Solutions to Most Exercises *}
+chapter {* Solutions to Most Exercises\label{ch:solutions} *}
 
 text {* \solution{fun:revsum} *}
 
@@ -24,18 +24,18 @@
 ML{*val any = Scan.one (Symbol.not_eof)
 
 val scan_cmt =
-  let
-    val begin_cmt = Scan.this_string "(*" 
-    val end_cmt = Scan.this_string "*)"
-  in
-   begin_cmt |-- Scan.repeat (Scan.unless end_cmt any) --| end_cmt 
-    >> (enclose "(**" "**)" o implode)
-  end
+let
+  val begin_cmt = Scan.this_string "(*" 
+  val end_cmt = Scan.this_string "*)"
+in
+  begin_cmt |-- Scan.repeat (Scan.unless end_cmt any) --| end_cmt 
+  >> (enclose "(**" "**)" o implode)
+end
 
 val parser = Scan.repeat (scan_cmt || any)
 
 val scan_all =
-  Scan.finite Symbol.stopper parser >> implode #> fst *}
+      Scan.finite Symbol.stopper parser >> implode #> fst *}
 
 text {*
   By using @{text "#> fst"} in the last line, the function 
@@ -84,15 +84,121 @@
 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 *})
+  apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [@{simproc add_sp}]) 1 *})
 txt {* 
   where the simproc produces the goal state
   
   \begin{minipage}{\textwidth}
   @{subgoals [display]}
-  \end{minipage}
+  \end{minipage}\bigskip
+*}(*<*)oops(*>*)
+
+text {* \solution{ex:addconversion} *}
+
+text {*
+  The following code assumes the function @{ML dest_sum} from the previous
+  exercise.
+*}
+
+
+ML{*fun add_simple_conv ctxt ctrm =
+let
+  val trm =  Thm.term_of ctrm
+in 
+  get_sum_thm ctxt trm (dest_sum trm)
+end
+
+fun add_conv ctxt ctrm =
+  (case Thm.term_of ctrm of
+     @{term "(op +)::nat \<Rightarrow> nat \<Rightarrow> nat"} $ _ $ _ => 
+         (Conv.binop_conv (add_conv ctxt)
+          then_conv (Conv.try_conv (add_simple_conv ctxt))) ctrm         
+    | _ $ _ => Conv.combination_conv 
+                 (add_conv ctxt) (add_conv ctxt) ctrm
+    | Abs _ => Conv.abs_conv (fn (_, ctxt) => add_conv ctxt) ctxt ctrm
+    | _ => Conv.all_conv ctrm)
+
+val add_tac = CSUBGOAL (fn (goal, i) =>
+  let
+    val ctxt = ProofContext.init (Thm.theory_of_cterm goal)
+  in
+    CONVERSION
+      (Conv.params_conv ~1 (fn ctxt =>
+        (Conv.prems_conv ~1 (add_conv ctxt) then_conv
+          Conv.concl_conv ~1 (add_conv ctxt))) ctxt) i
+  end)*}
+
+text {*
+  A test case is as follows
+*}
+
+lemma "P (Suc (99 + 1)) ((0 + 0)::nat) (Suc (3 + 3 + 3)) (4 + 1)"
+  apply(tactic {* add_tac 1 *})?
+txt {* 
+  where the conversion produces the goal state
+  
+  \begin{minipage}{\textwidth}
+  @{subgoals [display]}
+  \end{minipage}\bigskip
 *}(*<*)oops(*>*)
 
+subsection {* Tests start here *}
 
+lemma cheat: "P" sorry
+
+ML{*fun timing_wrapper tac st =
+let 
+  val t_start = start_timing ();
+  val res = tac st;
+  val t_end = end_timing t_start;
+in
+  (warning (#message t_end); res)
+end*}
+
+ML{* 
+fun create_term1 0 = @{term "0::nat"}
+  | create_term1 n = 
+       Const (@{const_name "plus"}, @{typ "nat\<Rightarrow>nat\<Rightarrow>nat"}) 
+         $ (HOLogic.mk_number @{typ "nat"} n) $ (create_term1 (n-1))
+*}
+
+ML{* 
+fun create_term2 0 = @{term "0::nat"}
+  | create_term2 n = 
+       Const (@{const_name "plus"}, @{typ "nat\<Rightarrow>nat\<Rightarrow>nat"}) 
+         $ (create_term2 (n-1)) $ (HOLogic.mk_number @{typ nat} n)
+*}
+
+ML{*
+fun create_term n = 
+  HOLogic.mk_Trueprop
+  (@{term "P::nat\<Rightarrow> bool"} $ 
+   (Const (@{const_name "plus"}, @{typ "nat\<Rightarrow>nat\<Rightarrow>nat"}) 
+    $ (create_term1 n) $ (create_term2 n)))
+*}
+
+ML {*
+warning (Syntax.string_of_term @{context} (create_term 4))
+*}
+
+ML {* 
+val _ = Goal.prove @{context} [] [] (create_term 100) 
+   (fn _ => timing_wrapper (EVERY1 [add_tac, rtac @{thm cheat}]))
+*}
+
+ML {* 
+val _ = Goal.prove @{context} [] [] (create_term 100) 
+   (fn _ => timing_wrapper (EVERY1 [simp_tac (HOL_basic_ss addsimprocs [@{simproc add_sp}]), rtac @{thm cheat}]))
+*}
+
+ML {* 
+val _ = Goal.prove @{context} [] [] (create_term 400) 
+  (fn _ => timing_wrapper (EVERY1 [add_tac, rtac @{thm cheat}]))
+*}
+
+ML {* 
+val _ = Goal.prove @{context} [] [] (create_term 400) 
+   (fn _ => timing_wrapper (EVERY1 [simp_tac (HOL_basic_ss addsimprocs [@{simproc add_sp}]), rtac @{thm cheat}]))
+*}
 
 end
\ No newline at end of file