# HG changeset patch # User Christian Urban # Date 1236872602 0 # Node ID ec47352e99c289db0b78a2a34b8e63b8d3304140 # Parent 18f90044c7774bdbb8c7290b920439cbf520127c improved the solution for the simproc/conversion exercise diff -r 18f90044c777 -r ec47352e99c2 CookBook/Solutions.thy --- 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\nat\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\nat\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\ bool"} $ - (Const (@{const_name "plus"}, @{typ "nat\nat\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\nat\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 \"} 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\ 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 diff -r 18f90044c777 -r ec47352e99c2 CookBook/Tactical.thy --- 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} diff -r 18f90044c777 -r ec47352e99c2 cookbook.pdf Binary file cookbook.pdf has changed