115 | _ $ _ => Conv.combination_conv |
115 | _ $ _ => Conv.combination_conv |
116 (add_conv ctxt) (add_conv ctxt) ctrm |
116 (add_conv ctxt) (add_conv ctxt) ctrm |
117 | Abs _ => Conv.abs_conv (fn (_, ctxt) => add_conv ctxt) ctxt ctrm |
117 | Abs _ => Conv.abs_conv (fn (_, ctxt) => add_conv ctxt) ctxt ctrm |
118 | _ => Conv.all_conv ctrm) |
118 | _ => Conv.all_conv ctrm) |
119 |
119 |
120 val add_tac = CSUBGOAL (fn (goal, i) => |
120 fun add_tac ctxt = CSUBGOAL (fn (goal, i) => |
121 let |
121 CONVERSION |
122 val ctxt = ProofContext.init (Thm.theory_of_cterm goal) |
122 (Conv.params_conv ~1 (fn ctxt => |
123 in |
123 (Conv.prems_conv ~1 (add_conv ctxt) then_conv |
124 CONVERSION |
124 Conv.concl_conv ~1 (add_conv ctxt))) ctxt) i)*} |
125 (Conv.params_conv ~1 (fn ctxt => |
|
126 (Conv.prems_conv ~1 (add_conv ctxt) then_conv |
|
127 Conv.concl_conv ~1 (add_conv ctxt))) ctxt) i |
|
128 end)*} |
|
129 |
125 |
130 text {* |
126 text {* |
131 A test case for this conversion is as follows |
127 A test case for this conversion is as follows |
132 *} |
128 *} |
133 |
129 |
134 lemma "P (Suc (99 + 1)) ((0 + 0)::nat) (Suc (3 + 3 + 3)) (4 + 1)" |
130 lemma "P (Suc (99 + 1)) ((0 + 0)::nat) (Suc (3 + 3 + 3)) (4 + 1)" |
135 apply(tactic {* add_tac 1 *})? |
131 apply(tactic {* add_tac @{context} 1 *})? |
136 txt {* |
132 txt {* |
137 where it produces the goal state |
133 where it produces the goal state |
138 |
134 |
139 \begin{minipage}{\textwidth} |
135 \begin{minipage}{\textwidth} |
140 @{subgoals [display]} |
136 @{subgoals [display]} |
195 *} |
191 *} |
196 |
192 |
197 ML{*local |
193 ML{*local |
198 fun mk_tac tac = timing_wrapper (EVERY1 [tac, rtac @{thm cheat}]) |
194 fun mk_tac tac = timing_wrapper (EVERY1 [tac, rtac @{thm cheat}]) |
199 in |
195 in |
200 val c_tac = mk_tac add_tac |
196 val c_tac = mk_tac (add_tac @{context}) |
201 val s_tac = mk_tac (simp_tac (HOL_basic_ss addsimprocs [@{simproc add_sp}])) |
197 val s_tac = mk_tac (simp_tac (HOL_basic_ss addsimprocs [@{simproc add_sp}])) |
202 end*} |
198 end*} |
203 |
199 |
204 text {* |
200 text {* |
205 This is all we need to let the conversion run against the simproc: |
201 This is all we need to let the conversion run against the simproc: |