2 imports Base 

     2 imports Base "Recipes/Timing"

   145 subsection {* Tests start here *}

   144 text {* \solution{ex:addconversion} *}

   146 

   145 

   147 lemma cheat: "P" sorry

   146 text {* 

   148 

   147   To measure the difference, we will create mechanically some terms involving 

   149 ML{*fun timing_wrapper tac st =

   148   additions and then set up a goal to be simplified. To prove the remaining 

   150 let 

   149   goal we use the ``lemma'':

   151   val t_start = start_timing ();

   150 *}

   152   val res = tac st;

   151 

   153   val t_end = end_timing t_start;

   152 lemma cheat: "A" sorry

   154 in

   153 

   155   (warning (#message t_end); res)

   154 text {*

   155   The reason is that it allows us to set up an unprovable goal where we can

   156   eliminate all interferences from other parts of the simplifier and

   157   then prove the goal using @{thm [source] cheat}. We also assume

   158   the timing function @{ML timing_wrapper} from Recipe~\ref{rec:timing}.

   159 

   160   First we define a function that returns a complete binary tree whose 

   161   leaves are numbers and the nodes are additions.

   162 *}

   163 

   164 ML{*fun term_tree n =

   165 let

   166   val count = ref 0; 

   167 

   168   fun term_tree_aux n =

   169     case n of

   170       0 => (count := !count + 1; HOLogic.mk_number @{typ nat} (!count))

   171     | _ => Const (@{const_name "plus"}, @{typ "nat\<Rightarrow>nat\<Rightarrow>nat"}) 

   172              $ (term_tree_aux (n - 1)) $ (term_tree_aux (n - 1))

   173 in

   174   term_tree_aux n

   158 ML{* 

   177 text {*

   159 fun create_term1 0 = @{term "0::nat"}

   178   For example

   160   | create_term1 n = 

   179 

   161        Const (@{const_name "plus"}, @{typ "nat\<Rightarrow>nat\<Rightarrow>nat"}) 

   180   @{ML_response_fake [display,gray] 

   162          $ (HOLogic.mk_number @{typ "nat"} n) $ (create_term1 (n-1))

   181   "warning (Syntax.string_of_term @{context} (term_tree 2))" 

   163 *}

   182   "(1 + 2) + (3 + 4)"} 

   164 

   183 

   165 ML{* 

   184   The next function generates a goal of the form @{text "P \<dots>"} with a term 

   166 fun create_term2 0 = @{term "0::nat"}

   185   filled in.

   167   | create_term2 n = 

   186 *}

   168        Const (@{const_name "plus"}, @{typ "nat\<Rightarrow>nat\<Rightarrow>nat"}) 

   187 

   169          $ (create_term2 (n-1)) $ (HOLogic.mk_number @{typ nat} n)

   188 ML{*fun goal n = HOLogic.mk_Trueprop (@{term "P::nat\<Rightarrow> bool"} $ (term_tree n))*}

   170 *}

   189 

   171 

   190 text {*

   172 ML{*

   191   Note that the goal needs to be wrapped in a @{term "Trueprop"}. Next we define

   173 fun create_term n = 

   192   two tactics, @{text "c_tac"} and @{text "s_tac"}, for the conversion and simproc,

   174   HOLogic.mk_Trueprop

   193   respectively. The tactics first apply the conversion (respectively simproc) and 

   175   (@{term "P::nat\<Rightarrow> bool"} $ 

   194   then prove the remaining goal using the lemma @{thm [source] cheat}.

   176    (Const (@{const_name "plus"}, @{typ "nat\<Rightarrow>nat\<Rightarrow>nat"}) 

   195 *}

   177     $ (create_term1 n) $ (create_term2 n)))

   196 

   178 *}

   197 ML{*local

   179 

   198   fun mk_tac tac = timing_wrapper (EVERY1 [tac, rtac @{thm cheat}])

   180 ML {*

   199 in

   181 warning (Syntax.string_of_term @{context} (create_term 4))

   200 val c_tac = mk_tac add_tac

   182 *}

   201 val s_tac = mk_tac 

   183 

   202              (simp_tac (HOL_basic_ss addsimprocs [@{simproc add_sp}]))

   184 ML {* 

   203 end*}

   185 val _ = Goal.prove @{context} [] [] (create_term 100) 

   204 

   186    (fn _ => timing_wrapper (EVERY1 [add_tac, rtac @{thm cheat}]))

   205 text {*

   187 *}

   206   This is all we need to let them run against each other.

   188 

   207 *}

   189 ML {* 

   208 

   190 val _ = Goal.prove @{context} [] [] (create_term 100) 

   209 ML{*val _ = Goal.prove @{context} [] [] (goal 8) (K c_tac);

   191    (fn _ => timing_wrapper (EVERY1 [simp_tac (HOL_basic_ss addsimprocs [@{simproc add_sp}]), rtac @{thm cheat}]))

   210 val _ = Goal.prove @{context} [] [] (goal 8) (K s_tac)*}

   192 *}

   211 

   193 

   212 text {*

   194 ML {* 

   213   As you can see, both versions perform relatively the same with perhaps some

   195 val _ = Goal.prove @{context} [] [] (create_term 400) 

   214   advantages for the simproc. That means the simplifier, while much more

   196   (fn _ => timing_wrapper (EVERY1 [add_tac, rtac @{thm cheat}]))

   215   complicated than conversions, is quite good for tasks it is designed for. It

   197 *}

   216   usually does not make sense to implement general-purpose rewriting using

   198 

   217   conversions. Conversions only have clear advantages in special situations:

   199 ML {* 

   218   for example if you need to have control over innermost or outermost

   200 val _ = Goal.prove @{context} [] [] (create_term 400) 

   219   rewriting; another situation is when rewriting rules are prone to

   201    (fn _ => timing_wrapper (EVERY1 [simp_tac (HOL_basic_ss addsimprocs [@{simproc add_sp}]), rtac @{thm cheat}]))

   220   non-termination.

   202 *}

   221 *}

   203 

   222 

   204 end

   223 end