180 text {* |
180 text {* |
181 Now the tactic which applies a single rule can be implemented |
181 Now the tactic which applies a single rule can be implemented |
182 as follows. |
182 as follows. |
183 *} |
183 *} |
184 |
184 |
185 ML %linenosgray{*val apply_tac = |
185 ML %linenosgray{*fun apply_tac ctxt = |
186 let |
186 let |
187 val intros = @{thms conjI disjI1 disjI2 impI iffI} |
187 val intros = @{thms conjI disjI1 disjI2 impI iffI} |
188 val elims = @{thms FalseE conjE disjE iffE impE2} |
188 val elims = @{thms FalseE conjE disjE iffE impE2} |
189 in |
189 in |
190 atac |
190 assume_tac ctxt |
191 ORELSE' resolve_tac intros |
191 ORELSE' resolve_tac ctxt intros |
192 ORELSE' eresolve_tac elims |
192 ORELSE' eresolve_tac ctxt elims |
193 ORELSE' (etac @{thm impE1} THEN' atac) |
193 ORELSE' (eresolve_tac ctxt [@{thm impE1}] THEN' assume_tac ctxt) |
194 end*} |
194 end*} |
195 |
195 |
196 text {* |
196 text {* |
197 In Line 11 we apply the rule @{thm [source] impE1} in concjunction |
197 In Line 11 we apply the rule @{thm [source] impE1} in concjunction |
198 with @{ML atac} in order to reduce the number of possibilities that |
198 with @{ML assume_tac} in order to reduce the number of possibilities that |
199 need to be explored. You can use the tactic as follows. |
199 need to be explored. You can use the tactic as follows. |
200 *} |
200 *} |
201 |
201 |
202 lemma |
202 lemma |
203 shows "((((P \<longrightarrow> Q) \<longrightarrow> P) \<longrightarrow> P) \<longrightarrow> Q) \<longrightarrow> Q" |
203 shows "((((P \<longrightarrow> Q) \<longrightarrow> P) \<longrightarrow> P) \<longrightarrow> Q) \<longrightarrow> Q" |
204 apply(tactic {* (DEPTH_SOLVE o apply_tac) 1 *}) |
204 apply(tactic {* (DEPTH_SOLVE o apply_tac @{context}) 1 *}) |
205 done |
205 done |
206 |
206 |
207 text {* |
207 text {* |
208 We can use the tactic to prove or disprove automatically the |
208 We can use the tactic to prove or disprove automatically the |
209 de Bruijn formulae from Exercise \ref{ex:debruijn}. |
209 de Bruijn formulae from Exercise \ref{ex:debruijn}. |
212 ML %grayML{*fun de_bruijn_prove ctxt n = |
212 ML %grayML{*fun de_bruijn_prove ctxt n = |
213 let |
213 let |
214 val goal = HOLogic.mk_Trueprop (HOLogic.mk_imp (lhs n n, rhs n)) |
214 val goal = HOLogic.mk_Trueprop (HOLogic.mk_imp (lhs n n, rhs n)) |
215 in |
215 in |
216 Goal.prove ctxt ["P"] [] goal |
216 Goal.prove ctxt ["P"] [] goal |
217 (fn _ => (DEPTH_SOLVE o apply_tac) 1) |
217 (fn _ => (DEPTH_SOLVE o apply_tac ctxt) 1) |
218 end*} |
218 end*} |
219 |
219 |
220 text {* |
220 text {* |
221 You can use this function to prove de Bruijn formulae. |
221 You can use this function to prove de Bruijn formulae. |
222 *} |
222 *} |
225 |
225 |
226 text {* \solution{ex:addsimproc} *} |
226 text {* \solution{ex:addsimproc} *} |
227 |
227 |
228 ML %grayML{*fun dest_sum term = |
228 ML %grayML{*fun dest_sum term = |
229 case term of |
229 case term of |
230 (@{term "(op +):: nat \<Rightarrow> nat \<Rightarrow> nat"} $ t1 $ t2) => |
230 (@{term "(+):: nat \<Rightarrow> nat \<Rightarrow> nat"} $ t1 $ t2) => |
231 (snd (HOLogic.dest_number t1), snd (HOLogic.dest_number t2)) |
231 (snd (HOLogic.dest_number t1), snd (HOLogic.dest_number t2)) |
232 | _ => raise TERM ("dest_sum", [term]) |
232 | _ => raise TERM ("dest_sum", [term]) |
233 |
233 |
234 fun get_sum_thm ctxt t (n1, n2) = |
234 fun get_sum_thm ctxt t (n1, n2) = |
235 let |
235 let |
273 ML %grayML{*fun add_simple_conv ctxt ctrm = |
273 ML %grayML{*fun add_simple_conv ctxt ctrm = |
274 let |
274 let |
275 val trm = Thm.term_of ctrm |
275 val trm = Thm.term_of ctrm |
276 in |
276 in |
277 case trm of |
277 case trm of |
278 @{term "(op +)::nat \<Rightarrow> nat \<Rightarrow> nat"} $ _ $ _ => |
278 @{term "(+)::nat \<Rightarrow> nat \<Rightarrow> nat"} $ _ $ _ => |
279 get_sum_thm ctxt trm (dest_sum trm) |
279 get_sum_thm ctxt trm (dest_sum trm) |
280 | _ => Conv.all_conv ctrm |
280 | _ => Conv.all_conv ctrm |
281 end |
281 end |
282 |
282 |
283 val add_conv = Conv.bottom_conv add_simple_conv |
283 val add_conv = Conv.bottom_conv add_simple_conv |
348 *} |
348 *} |
349 |
349 |
350 ML Skip_Proof.cheat_tac |
350 ML Skip_Proof.cheat_tac |
351 |
351 |
352 ML %grayML{*local |
352 ML %grayML{*local |
353 fun mk_tac tac = |
353 fun mk_tac ctxt tac = |
354 timing_wrapper (EVERY1 [tac, Skip_Proof.cheat_tac]) |
354 timing_wrapper (EVERY1 [tac, Skip_Proof.cheat_tac ctxt]) |
355 in |
355 in |
356 fun c_tac ctxt = mk_tac (add_tac ctxt) |
356 fun c_tac ctxt = mk_tac ctxt (add_tac ctxt) |
357 fun s_tac ctxt = mk_tac (simp_tac |
357 fun s_tac ctxt = mk_tac ctxt (simp_tac |
358 (put_simpset HOL_basic_ss ctxt addsimprocs [@{simproc add_sp}])) |
358 (put_simpset HOL_basic_ss ctxt addsimprocs [@{simproc add_sp}])) |
359 end*} |
359 end*} |
360 |
360 |
361 text {* |
361 text {* |
362 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: |