# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1236778923 0
# Node ID 00d153e32a5391b415e92a6aebdd17455219c5ab
# Parent  890fbfef6d6b3e9d8f3d20813ea871b437e6b2df
improvments to the solutions suggested by Sacha B?hme

diff -r 890fbfef6d6b -r 00d153e32a53 CookBook/Solutions.thy
--- a/CookBook/Solutions.thy	Wed Mar 11 01:43:28 2009 +0000
+++ b/CookBook/Solutions.thy	Wed Mar 11 13:42:03 2009 +0000
@@ -95,21 +95,18 @@
 
 text {* \solution{ex:addconversion} *}
 
-text {*
-  (FIXME This solution works but is awkward.)
-*}
+ML{*fun add_simple_conv ctxt ctrm =
+let
+  val trm =  Thm.term_of ctrm
+in 
+  get_sum_thm ctxt trm (dest_sum trm)
+end
 
-ML{*fun add_conv ctxt ctrm =
+fun add_conv ctxt ctrm =
   (case Thm.term_of ctrm of
      @{term "(op +)::nat \<Rightarrow> nat \<Rightarrow> nat"} $ _ $ _ => 
-         (let
-            val eq1 = Conv.binop_conv (add_conv ctxt) ctrm;
-            val ctrm' = Thm.rhs_of eq1;
-            val trm' = Thm.term_of ctrm';
-            val eq2 = Conv.rewr_conv (get_sum_thm ctxt trm' (dest_sum trm')) ctrm'
-          in
-             Thm.transitive eq1 eq2
-          end)       
+         (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
diff -r 890fbfef6d6b -r 00d153e32a53 CookBook/Tactical.thy
--- a/CookBook/Tactical.thy	Wed Mar 11 01:43:28 2009 +0000
+++ b/CookBook/Tactical.thy	Wed Mar 11 13:42:03 2009 +0000
@@ -2024,12 +2024,13 @@
   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
   of the form @{term "t\<^isub>1 + t\<^isub>2"} by their result. You can make
-  the same assumptions as in \ref{ex:addsimproc}. FIXME: the current solution
-  requires some additional functions.
+  the same assumptions as in \ref{ex:addsimproc}. 
   \end{exercise}
 
   \begin{exercise}