equal
deleted
inserted
replaced
126 (Conv.prems_conv ~1 (add_conv ctxt) then_conv |
126 (Conv.prems_conv ~1 (add_conv ctxt) then_conv |
127 Conv.concl_conv ~1 (add_conv ctxt))) ctxt) i |
127 Conv.concl_conv ~1 (add_conv ctxt))) ctxt) i |
128 end)*} |
128 end)*} |
129 |
129 |
130 text {* |
130 text {* |
131 A test case is as follows |
131 A test case for this conversion is as follows |
132 *} |
132 *} |
133 |
133 |
134 lemma "P (Suc (99 + 1)) ((0 + 0)::nat) (Suc (3 + 3 + 3)) (4 + 1)" |
134 lemma "P (Suc (99 + 1)) ((0 + 0)::nat) (Suc (3 + 3 + 3)) (4 + 1)" |
135 apply(tactic {* add_tac 1 *})? |
135 apply(tactic {* add_tac 1 *})? |
136 txt {* |
136 txt {* |
137 where the conversion produces the goal state |
137 where it produces the goal state |
138 |
138 |
139 \begin{minipage}{\textwidth} |
139 \begin{minipage}{\textwidth} |
140 @{subgoals [display]} |
140 @{subgoals [display]} |
141 \end{minipage}\bigskip |
141 \end{minipage}\bigskip |
142 *}(*<*)oops(*>*) |
142 *}(*<*)oops(*>*) |
200 val c_tac = mk_tac add_tac |
200 val c_tac = mk_tac add_tac |
201 val s_tac = mk_tac (simp_tac (HOL_basic_ss addsimprocs [@{simproc add_sp}])) |
201 val s_tac = mk_tac (simp_tac (HOL_basic_ss addsimprocs [@{simproc add_sp}])) |
202 end*} |
202 end*} |
203 |
203 |
204 text {* |
204 text {* |
205 This is all we need to let the conversion run against the simproc. |
205 This is all we need to let the conversion run against the simproc: |
206 *} |
206 *} |
207 |
207 |
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 |