diff -r 00d153e32a53 -r 3e30ea95c7aa CookBook/Solutions.thy
--- a/CookBook/Solutions.thy	Wed Mar 11 13:42:03 2009 +0000
+++ b/CookBook/Solutions.thy	Wed Mar 11 17:38:17 2009 +0000
@@ -1,5 +1,5 @@
 theory Solutions
-imports Base
+imports Base 
 begin
 
 chapter {* Solutions to Most Exercises\label{ch:solutions} *}
@@ -84,7 +84,7 @@
 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
   
@@ -132,5 +132,63 @@
   \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