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

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

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

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

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

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

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

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

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

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

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

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

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

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

   157   additions.

   153   additions.

   158 *}

   154 *}

   159 

   155 

   185 

   181 

   186 text {*

   182 text {*

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

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

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

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

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

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

   191 *}

   187 *}

   192 

   188 

   193 ML{*local

   189 ML{*local

   195 in

   191 in

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

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

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

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

   198 end*}

   194 end*}

   199 

   195