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

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

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

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

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

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

   273   other parts of the simplifier do not interfere. For this we construct an

   273   other parts of the simplifier do not interfere. For this we construct an

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

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

   276 

   276 

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

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

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

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

   279   additions.

   279   additions.

   280 *}

   280 *}

   307 

   307 

   308 text {*

   308 text {*

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

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

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

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

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

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

   313 *}

   313 *}

   314 

   314 

   315 ML{*local

   315 ML{*local

   316   fun mk_tac tac = 

   316   fun mk_tac tac = 

   318 in

   318 in

   319 val c_tac = mk_tac (add_tac @{context}) 

   319 val c_tac = mk_tac (add_tac @{context}) 

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

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

   321 end*}

   321 end*}

   322 

   322