--- a/CookBook/Solutions.thy	Thu Mar 12 18:39:10 2009 +0000
+++ b/CookBook/Solutions.thy	Fri Mar 13 01:15:55 2009 +0100
@@ -144,21 +144,21 @@
 text {* \solution{ex:addconversion} *}
 
 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'':
+  We use the timing function @{ML timing_wrapper} from Recipe~\ref{rec:timing}.
+  To measure any difference between the simproc and conversion, we will create 
+  mechanically terms involving additions and then set up a goal to be 
+  simplified. We have to be careful to set up the goal so that
+  other parts of the simplifier do not interfere. For this we set up an
+  unprovable goal which, after simplification, we are going to ``prove'' with
+  the help of the lemma:
 *}
 
 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.
+  For constructing test cases, we first define a function that returns a 
+  complete binary tree whose leaves are numbers and the nodes are 
+  additions.
 *}
 
 ML{*fun term_tree n =
@@ -175,14 +175,14 @@
 end*}
 
 text {*
-  For example
+  This function generates 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.
+  The next function constructs a goal of the form @{text "P \<dots>"} with a term 
+  produced by @{ML term_tree} filled in.
 *}
 
 ML{*fun goal n = HOLogic.mk_Trueprop (@{term "P::nat\<Rightarrow> bool"} $ (term_tree n))*}
@@ -190,7 +190,7 @@
 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 
+  respectively. The idea is to first apply the conversion (respectively simproc) and 
   then prove the remaining goal using the lemma @{thm [source] cheat}.
 *}
 
@@ -198,26 +198,25 @@
   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}]))
+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.
+  This is all we need to let the conversion run against the simproc.
 *}
 
-ML{*val _ = Goal.prove @{context} [] [] (goal 8) (K c_tac);
+ML{*val _ = Goal.prove @{context} [] [] (goal 8) (K c_tac)
 val _ = Goal.prove @{context} [] [] (goal 8) (K s_tac)*}
 
 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
+  If you do the exercise, you can see that both ways of simplifying additions
+  perform relatively the same with perhaps some advantages for the
+  simproc. That means the simplifier, even if much more complicated than
+  conversions, is quite efficient 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.
+  rewriting, or when rewriting rules are lead to non-termination.
 *}
 
 end
\ No newline at end of file

--- a/CookBook/Tactical.thy	Thu Mar 12 18:39:10 2009 +0000
+++ b/CookBook/Tactical.thy	Fri Mar 13 01:15:55 2009 +0100
@@ -1762,9 +1762,9 @@
 
   Note that the actual response in this example is @{term "2 + 10 \<equiv> 2 + (10::nat)"}, 
   since the pretty-printer for @{ML_type cterm}s already beta-normalises terms.
-  But by the way how we constructed the term (using the function 
-  @{ML Thm.capply}, which is the application @{ML $} for @{ML_type cterm}s),
-  we can be sure the left-hand side must contain beta-redexes. Indeed
+  But how we constructed the term (using the function 
+  @{ML Thm.capply}, which is the application @{ML $} for @{ML_type cterm}s)
+  ensures that the left-hand side must contain beta-redexes. Indeed
   if we obtain the ``raw'' representation of the produced theorem, we
   can see the difference:
 
@@ -1808,7 +1808,7 @@
 
 text {* 
   You can see how this function works in the example rewriting 
-  the @{ML_type cterm} @{term "True \<and> (Foo \<longrightarrow> Bar)"} to @{term "Foo \<longrightarrow> Bar"}.
+  @{term "True \<and> (Foo \<longrightarrow> Bar)"} to @{term "Foo \<longrightarrow> Bar"}.
 
   @{ML_response_fake [display,gray]
 "let 
@@ -1861,6 +1861,14 @@
   does not fail, however, because the combinator @{ML Conv.else_conv} will then 
   try out @{ML Conv.all_conv}, which always succeeds.
 
+  The conversion combinator @{ML Conv.try_conv} constructs a conversion 
+  which is tried out on a term, but in case of failure just does nothing.
+  For example
+  
+  @{ML_response_fake [display,gray]
+  "Conv.try_conv (Conv.rewr_conv @{thm true_conj1}) @{cterm \"True \<or> P\"}"
+  "True \<or> P \<equiv> True \<or> P"}
+
   Apart from the function @{ML beta_conversion in Thm}, which is able to fully
   beta-normalise a term, the conversions so far are restricted in that they
   only apply to the outer-most level of a @{ML_type cterm}. In what follows we
@@ -2028,8 +2036,6 @@
   and simprocs; the advantage of conversions, however, is that you never have
   to worry about non-termination.
 
-  (FIXME: explain @{ML Conv.try_conv})
-
   \begin{exercise}\label{ex:addconversion}
   Write a tactic that does the same as the simproc in exercise
   \ref{ex:addsimproc}, but is based in conversions. That means replace terms
@@ -2038,7 +2044,7 @@
   \end{exercise}
 
   \begin{exercise}\label{ex:compare}
-  Compare your solutions of Exercises~\ref{addsimproc} and \ref{ex:addconversion},
+  Compare your solutions of Exercises~\ref{ex: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.

Binary file cookbook.pdf has changed