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

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

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

   148   To measure any difference between the simproc and conversion, we will create 

   149   goal we use the ``lemma'':

   149   mechanically terms involving additions and then set up a goal to be 

   150   simplified. We have to be careful to set up the goal so that

   151   other parts of the simplifier do not interfere. For this we set up an

   152   unprovable goal which, after simplification, we are going to ``prove'' with

   153   the help of the lemma:

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

   159   For constructing test cases, we first define a function that returns a 

   156   eliminate all interferences from other parts of the simplifier and

   160   complete binary tree whose leaves are numbers and the nodes are 

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

   161   additions.

   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.

   178   For example

   178   This function generates for example

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

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

   185   filled in.

   185   produced by @{ML term_tree} filled in.

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

   193   respectively. The idea is to first apply the conversion (respectively simproc) and 

   201 val s_tac = mk_tac 

   201 val s_tac = mk_tac (simp_tac (HOL_basic_ss addsimprocs [@{simproc add_sp}]))

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

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

   205   This is all we need to let the conversion run against the simproc.

   207 *}

   206 *}

   208 

   207 

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

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

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

   212   If you do the exercise, you can see that both ways of simplifying additions

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

   213   perform relatively the same with perhaps some advantages for the

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

   214   simproc. That means the simplifier, even if much more complicated than

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

   215   conversions, is quite efficient for tasks it is designed for. It usually does not

   216   make sense to implement general-purpose rewriting using

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

   219   rewriting, or when rewriting rules are lead to non-termination.

   220   non-termination.

   220 *}

   221 *}

   221 

   222 

   222 end

   223 end