--- a/CookBook/Solutions.thy	Thu Mar 12 14:25:35 2009 +0000
+++ b/CookBook/Solutions.thy	Thu Mar 12 15:43:22 2009 +0000
@@ -1,5 +1,5 @@
 theory Solutions
-imports Base 
+imports Base "Recipes/Timing"
 begin
 
 chapter {* Solutions to Most Exercises\label{ch:solutions} *}
@@ -100,7 +100,6 @@
   exercise.
 *}
 
-
 ML{*fun add_simple_conv ctxt ctrm =
 let
   val trm =  Thm.term_of ctrm
@@ -142,63 +141,83 @@
   \end{minipage}\bigskip
 *}(*<*)oops(*>*)
 
-subsection {* Tests start here *}
-
-lemma cheat: "P" sorry
+text {* \solution{ex:addconversion} *}
 
-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))
+text {* 
+  To measure the difference, we will create mechanically some terms involving 
+  additions and then set up a goal to be simplified. To prove the remaining 
+  goal we use the ``lemma'':
 *}
 
-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)
+lemma cheat: "A" sorry
+
+text {*
+  The reason is that it allows us to set up an unprovable goal where we can
+  eliminate all interferences from other parts of the simplifier and
+  then prove the goal using @{thm [source] cheat}. We also assume
+  the timing function @{ML timing_wrapper} from Recipe~\ref{rec:timing}.
+
+  First we define a function that returns a complete binary tree whose 
+  leaves are numbers and the nodes are additions.
 *}
 
-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{*fun term_tree n =
+let
+  val count = ref 0; 
 
-ML {*
-warning (Syntax.string_of_term @{context} (create_term 4))
+  fun term_tree_aux n =
+    case n of
+      0 => (count := !count + 1; HOLogic.mk_number @{typ nat} (!count))
+    | _ => Const (@{const_name "plus"}, @{typ "nat\<Rightarrow>nat\<Rightarrow>nat"}) 
+             $ (term_tree_aux (n - 1)) $ (term_tree_aux (n - 1))
+in
+  term_tree_aux n
+end*}
+
+text {*
+  For example
+
+  @{ML_response_fake [display,gray] 
+  "warning (Syntax.string_of_term @{context} (term_tree 2))" 
+  "(1 + 2) + (3 + 4)"} 
+
+  The next function generates a goal of the form @{text "P \<dots>"} with a term 
+  filled in.
 *}
 
-ML {* 
-val _ = Goal.prove @{context} [] [] (create_term 100) 
-   (fn _ => timing_wrapper (EVERY1 [add_tac, rtac @{thm cheat}]))
+ML{*fun goal n = HOLogic.mk_Trueprop (@{term "P::nat\<Rightarrow> bool"} $ (term_tree n))*}
+
+text {*
+  Note that the goal needs to be wrapped in a @{term "Trueprop"}. Next we define
+  two tactics, @{text "c_tac"} and @{text "s_tac"}, for the conversion and simproc,
+  respectively. The tactics first apply the conversion (respectively simproc) and 
+  then prove the remaining goal using the lemma @{thm [source] 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{*local
+  fun mk_tac tac = timing_wrapper (EVERY1 [tac, rtac @{thm cheat}])
+in
+val c_tac = mk_tac add_tac
+val s_tac = mk_tac 
+             (simp_tac (HOL_basic_ss addsimprocs [@{simproc add_sp}]))
+end*}
+
+text {*
+  This is all we need to let them run against each other.
 *}
 
-ML {* 
-val _ = Goal.prove @{context} [] [] (create_term 400) 
-  (fn _ => timing_wrapper (EVERY1 [add_tac, rtac @{thm cheat}]))
-*}
+ML{*val _ = Goal.prove @{context} [] [] (goal 8) (K c_tac);
+val _ = Goal.prove @{context} [] [] (goal 8) (K s_tac)*}
 
-ML {* 
-val _ = Goal.prove @{context} [] [] (create_term 400) 
-   (fn _ => timing_wrapper (EVERY1 [simp_tac (HOL_basic_ss addsimprocs [@{simproc add_sp}]), rtac @{thm cheat}]))
+text {*
+  As you can see, both versions perform relatively the same with perhaps some
+  advantages for the simproc. That means the simplifier, while much more
+  complicated than conversions, is quite good for tasks it is designed for. It
+  usually does not make sense to implement general-purpose rewriting using
+  conversions. Conversions only have clear advantages in special situations:
+  for example if you need to have control over innermost or outermost
+  rewriting; another situation is when rewriting rules are prone to
+  non-termination.
 *}
 
 end
\ No newline at end of file

--- a/CookBook/Tactical.thy	Thu Mar 12 14:25:35 2009 +0000
+++ b/CookBook/Tactical.thy	Thu Mar 12 15:43:22 2009 +0000
@@ -2033,10 +2033,11 @@
   the same assumptions as in \ref{ex:addsimproc}. 
   \end{exercise}
 
-  \begin{exercise}
-  Compare which way (either Exercise ~\ref{addsimproc} or \ref{ex:addconversion}) of 
-  rewriting such terms is faster. For this you might have to construct quite 
-  large terms. Also see Recipe \ref{rec:timing} for information about timing.
+  \begin{exercise}\label{ex:compare}
+  Compare your solutions of Exercises~\ref{addsimproc} and \ref{ex:addconversion},
+  and try to determine which way of rewriting such terms is faster. For this you might 
+  have to construct quite large terms. Also see Recipe \ref{rec:timing} for information 
+  about timing.
   \end{exercise}
 
   \begin{readmore}

Binary file cookbook.pdf has changed