equal
deleted
inserted
replaced
146 text {* |
146 text {* |
147 We use the timing function @{ML timing_wrapper} from Recipe~\ref{rec:timing}. |
147 We use the timing function @{ML timing_wrapper} from Recipe~\ref{rec:timing}. |
148 To measure any difference between the simproc and conversion, we will create |
148 To measure any difference between the simproc and conversion, we will create |
149 mechanically terms involving additions and then set up a goal to be |
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 |
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 |
151 other parts of the simplifier do not interfere. For this we construct an |
152 unprovable goal which, after simplification, we are going to ``prove'' with |
152 unprovable goal which, after simplification, we are going to ``prove'' with |
153 the help of the lemma: |
153 the help of the lemma: |
154 *} |
154 *} |
155 |
155 |
156 lemma cheat: "A" sorry |
156 lemma cheat: "A" sorry |
173 in |
173 in |
174 term_tree_aux n |
174 term_tree_aux n |
175 end*} |
175 end*} |
176 |
176 |
177 text {* |
177 text {* |
178 This function generates for example |
178 This function generates for example: |
179 |
179 |
180 @{ML_response_fake [display,gray] |
180 @{ML_response_fake [display,gray] |
181 "warning (Syntax.string_of_term @{context} (term_tree 2))" |
181 "warning (Syntax.string_of_term @{context} (term_tree 2))" |
182 "(1 + 2) + (3 + 4)"} |
182 "(1 + 2) + (3 + 4)"} |
183 |
183 |
189 |
189 |
190 text {* |
190 text {* |
191 Note that the goal needs to be wrapped in a @{term "Trueprop"}. Next we define |
191 Note that the goal needs to be wrapped in a @{term "Trueprop"}. Next we define |
192 two tactics, @{text "c_tac"} and @{text "s_tac"}, for the conversion and simproc, |
192 two tactics, @{text "c_tac"} and @{text "s_tac"}, for the conversion and simproc, |
193 respectively. The idea is to first apply the conversion (respectively simproc) and |
193 respectively. The idea is to first apply the conversion (respectively simproc) and |
194 then prove the remaining goal using the lemma @{thm [source] cheat}. |
194 then prove the remaining goal using the @{thm [source] cheat}-lemma. |
195 *} |
195 *} |
196 |
196 |
197 ML{*local |
197 ML{*local |
198 fun mk_tac tac = timing_wrapper (EVERY1 [tac, rtac @{thm cheat}]) |
198 fun mk_tac tac = timing_wrapper (EVERY1 [tac, rtac @{thm cheat}]) |
199 in |
199 in |
208 ML{*val _ = Goal.prove @{context} [] [] (goal 8) (K c_tac) |
208 ML{*val _ = Goal.prove @{context} [] [] (goal 8) (K c_tac) |
209 val _ = Goal.prove @{context} [] [] (goal 8) (K s_tac)*} |
209 val _ = Goal.prove @{context} [] [] (goal 8) (K s_tac)*} |
210 |
210 |
211 text {* |
211 text {* |
212 If you do the exercise, you can see that both ways of simplifying additions |
212 If you do the exercise, you can see that both ways of simplifying additions |
213 perform relatively the same with perhaps some advantages for the |
213 perform relatively similar with perhaps some advantages for the |
214 simproc. That means the simplifier, even if much more complicated than |
214 simproc. That means the simplifier, even if much more complicated than |
215 conversions, is quite efficient for tasks it is designed for. It usually does not |
215 conversions, is quite efficient for tasks it is designed for. It usually does not |
216 make sense to implement general-purpose rewriting using |
216 make sense to implement general-purpose rewriting using |
217 conversions. Conversions only have clear advantages in special situations: |
217 conversions. Conversions only have clear advantages in special situations: |
218 for example if you need to have control over innermost or outermost |
218 for example if you need to have control over innermost or outermost |