223 |
223 |
224 simproc_setup %gray add_sp ("t1 + t2") = {* K add_sp_aux *} |
224 simproc_setup %gray add_sp ("t1 + t2") = {* K add_sp_aux *} |
225 |
225 |
226 text {* and a test case is the lemma *} |
226 text {* and a test case is the lemma *} |
227 |
227 |
228 lemma "P (Suc (99 + 1)) ((0 + 0)::nat) (Suc (3 + 3 + 3)) (4 + 1)" |
228 lemma "P (Suc (99 + 1)) ((0 + 0)::nat) (Suc (3 + 3 + 3)) ((4 + 1)::nat)" |
229 apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [@{simproc add_sp}]) 1 *}) |
229 apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [@{simproc add_sp}]) 1 *}) |
230 txt {* |
230 txt {* |
231 where the simproc produces the goal state |
231 where the simproc produces the goal state |
232 |
232 |
233 \begin{minipage}{\textwidth} |
233 \begin{minipage}{\textwidth} |
240 text {* |
240 text {* |
241 The following code assumes the function @{ML dest_sum} from the previous |
241 The following code assumes the function @{ML dest_sum} from the previous |
242 exercise. |
242 exercise. |
243 *} |
243 *} |
244 |
244 |
245 ML{*fun add_simple_conv ctxt ctrm = |
245 ML {*fun add_simple_conv ctxt ctrm = |
246 let |
246 let |
247 val trm = Thm.term_of ctrm |
247 val trm = Thm.term_of ctrm |
248 in |
248 in |
249 get_sum_thm ctxt trm (dest_sum trm) |
249 case trm of |
|
250 @{term "(op +)::nat \<Rightarrow> nat \<Rightarrow> nat"} $ _ $ _ => |
|
251 get_sum_thm ctxt trm (dest_sum trm) |
|
252 | _ => Conv.all_conv ctrm |
250 end |
253 end |
251 |
254 |
252 fun add_conv ctxt ctrm = |
255 val add_conv = More_Conv.bottom_conv add_simple_conv |
253 (case Thm.term_of ctrm of |
256 |
254 @{term "(op +)::nat \<Rightarrow> nat \<Rightarrow> nat"} $ _ $ _ => |
257 fun add_tac ctxt = CONVERSION |
255 (Conv.binop_conv (add_conv ctxt) |
|
256 then_conv (Conv.try_conv (add_simple_conv ctxt))) ctrm |
|
257 | _ $ _ => Conv.comb_conv (add_conv ctxt) ctrm |
|
258 | Abs _ => Conv.abs_conv (fn (_, ctxt) => add_conv ctxt) ctxt ctrm |
|
259 | _ => Conv.all_conv ctrm) |
|
260 |
|
261 fun add_tac ctxt = CSUBGOAL (fn (goal, i) => |
|
262 CONVERSION |
|
263 (Conv.params_conv ~1 (fn ctxt => |
258 (Conv.params_conv ~1 (fn ctxt => |
264 (Conv.prems_conv ~1 (add_conv ctxt) then_conv |
259 (Conv.prems_conv ~1 (add_conv ctxt) then_conv |
265 Conv.concl_conv ~1 (add_conv ctxt))) ctxt) i)*} |
260 Conv.concl_conv ~1 (add_conv ctxt))) ctxt)*} |
266 |
261 |
267 text {* |
262 text {* |
268 A test case for this conversion is as follows |
263 A test case for this conversion is as follows |
269 *} |
264 *} |
270 |
265 |
271 lemma "P (Suc (99 + 1)) ((0 + 0)::nat) (Suc (3 + 3 + 3)) (4 + 1)" |
266 lemma "P (Suc (99 + 1)) ((0 + 0)::nat) (Suc (3 + 3 + 3)) ((4 + 1)::nat)" |
272 apply(tactic {* add_tac @{context} 1 *})? |
267 apply(tactic {* add_tac @{context} 1 *})? |
273 txt {* |
268 txt {* |
274 where it produces the goal state |
269 where it produces the goal state |
275 |
270 |
276 \begin{minipage}{\textwidth} |
271 \begin{minipage}{\textwidth} |