237 val goal = Logic.mk_equals (t, sum) |
237 val goal = Logic.mk_equals (t, sum) |
238 in |
238 in |
239 Goal.prove ctxt [] [] goal (K (Arith_Data.arith_tac ctxt 1)) |
239 Goal.prove ctxt [] [] goal (K (Arith_Data.arith_tac ctxt 1)) |
240 end |
240 end |
241 |
241 |
242 fun add_sp_aux ss t = |
242 fun add_sp_aux ctxt t = |
243 let |
243 let |
244 val ctxt = Simplifier.the_context ss |
|
245 val t' = term_of t |
244 val t' = term_of t |
246 in |
245 in |
247 SOME (get_sum_thm ctxt t' (dest_sum t')) |
246 SOME (get_sum_thm ctxt t' (dest_sum t')) |
248 handle TERM _ => NONE |
247 handle TERM _ => NONE |
249 end*} |
248 end*} |
253 simproc_setup %gray add_sp ("t1 + t2") = {* K add_sp_aux *} |
252 simproc_setup %gray add_sp ("t1 + t2") = {* K add_sp_aux *} |
254 |
253 |
255 text {* and a test case is the lemma *} |
254 text {* and a test case is the lemma *} |
256 |
255 |
257 lemma "P (Suc (99 + 1)) ((0 + 0)::nat) (Suc (3 + 3 + 3)) ((4 + 1)::nat)" |
256 lemma "P (Suc (99 + 1)) ((0 + 0)::nat) (Suc (3 + 3 + 3)) ((4 + 1)::nat)" |
258 apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [@{simproc add_sp}]) 1 *}) |
257 apply(tactic {* simp_tac (put_simpset HOL_basic_ss @{context} addsimprocs [@{simproc add_sp}]) 1 *}) |
259 txt {* |
258 txt {* |
260 where the simproc produces the goal state |
259 where the simproc produces the goal state |
261 |
260 |
262 \begin{minipage}{\textwidth} |
261 \begin{minipage}{\textwidth} |
263 @{subgoals [display]} |
262 @{subgoals [display]} |
346 two tactics, @{text "c_tac"} and @{text "s_tac"}, for the conversion and simproc, |
345 two tactics, @{text "c_tac"} and @{text "s_tac"}, for the conversion and simproc, |
347 respectively. The idea is to first apply the conversion (respectively simproc) and |
346 respectively. The idea is to first apply the conversion (respectively simproc) and |
348 then prove the remaining goal using @{ML "cheat_tac" in Skip_Proof}. |
347 then prove the remaining goal using @{ML "cheat_tac" in Skip_Proof}. |
349 *} |
348 *} |
350 |
349 |
|
350 ML Skip_Proof.cheat_tac |
|
351 |
351 ML %grayML{*local |
352 ML %grayML{*local |
352 fun mk_tac tac = |
353 fun mk_tac tac = |
353 timing_wrapper (EVERY1 [tac, K (Skip_Proof.cheat_tac @{theory})]) |
354 timing_wrapper (EVERY1 [tac, Skip_Proof.cheat_tac]) |
354 in |
355 in |
355 val c_tac = mk_tac (add_tac @{context}) |
356 fun c_tac ctxt = mk_tac (add_tac ctxt) |
356 val s_tac = mk_tac (simp_tac |
357 fun s_tac ctxt = mk_tac (simp_tac |
357 (HOL_basic_ss addsimprocs [@{simproc add_sp}])) |
358 (put_simpset HOL_basic_ss ctxt addsimprocs [@{simproc add_sp}])) |
358 end*} |
359 end*} |
359 |
360 |
360 text {* |
361 text {* |
361 This is all we need to let the conversion run against the simproc: |
362 This is all we need to let the conversion run against the simproc: |
362 *} |
363 *} |
363 |
364 |
364 ML %grayML{*val _ = Goal.prove @{context} [] [] (goal 8) (K c_tac) |
365 ML %grayML{*val _ = Goal.prove @{context} [] [] (goal 8) (fn {context, ...} => c_tac context) |
365 val _ = Goal.prove @{context} [] [] (goal 8) (K s_tac)*} |
366 val _ = Goal.prove @{context} [] [] (goal 8) (fn {context, ...} => s_tac context)*} |
366 |
367 |
367 text {* |
368 text {* |
368 If you do the exercise, you can see that both ways of simplifying additions |
369 If you do the exercise, you can see that both ways of simplifying additions |
369 perform relatively similar with perhaps some advantages for the |
370 perform relatively similar with perhaps some advantages for the |
370 simproc. That means the simplifier, even if much more complicated than |
371 simproc. That means the simplifier, even if much more complicated than |