268 "equivp r \<Longrightarrow> r a b \<Longrightarrow> r c a = r c b" |
268 "equivp r \<Longrightarrow> r a b \<Longrightarrow> r c a = r c b" |
269 unfolding equivp_reflp_symp_transp symp_def transp_def |
269 unfolding equivp_reflp_symp_transp symp_def transp_def |
270 by blast |
270 by blast |
271 |
271 |
272 ML {* |
272 ML {* |
273 fun prove_alpha_bn_rsp alphas inducts inj_dis equivps ctxt (alpha_bn, n) = |
273 fun prove_alpha_bn_rsp alphas inducts exhausts inj_dis equivps ctxt (alpha_bn, n) = |
274 let |
274 let |
275 val alpha = nth alphas n; |
275 val alpha = nth alphas n; |
276 val ty = domain_type (fastype_of alpha); |
276 val ty = domain_type (fastype_of alpha); |
277 val names = Datatype_Prop.make_tnames [ty, ty]; |
277 val ([x, y, a], ctxt') = Variable.variant_fixes ["x","y","a"] ctxt; |
278 val [l, r] = map (fn x => (Free (x, ty))) names; |
278 val [l, r] = map (fn x => (Free (x, ty))) [x, y] |
|
279 val lhs = HOLogic.mk_Trueprop (alpha $ l $ r) |
279 val g1 = |
280 val g1 = |
280 Logic.mk_implies (HOLogic.mk_Trueprop (alpha $ l $ r), |
281 Logic.mk_implies (lhs, |
281 HOLogic.mk_Trueprop (HOLogic.mk_all ("a", ty, |
282 HOLogic.mk_Trueprop (HOLogic.mk_all (a, ty, |
282 HOLogic.mk_eq (alpha_bn $ l $ Bound 0, alpha_bn $ r $ Bound 0)))) |
283 HOLogic.mk_eq (alpha_bn $ l $ Bound 0, alpha_bn $ r $ Bound 0)))); |
283 val g2 = |
284 val g2 = |
284 Logic.mk_implies (HOLogic.mk_Trueprop (alpha $ l $ r), |
285 Logic.mk_implies (lhs, |
285 HOLogic.mk_Trueprop (HOLogic.mk_all ("a", ty, |
286 HOLogic.mk_Trueprop (HOLogic.mk_all (a, ty, |
286 HOLogic.mk_eq (alpha_bn $ Bound 0 $ l, alpha_bn $ Bound 0 $ r)))) |
287 HOLogic.mk_eq (alpha_bn $ Bound 0 $ l, alpha_bn $ Bound 0 $ r)))); |
|
288 val resl = map (fn x => @{thm equivp_rspl} OF [x]) equivps; |
|
289 val resr = map (fn x => @{thm equivp_rspr} OF [x]) equivps; |
287 fun tac {context, ...} = ( |
290 fun tac {context, ...} = ( |
288 etac (nth inducts n) THEN_ALL_NEW |
291 etac (nth inducts n) THEN_ALL_NEW |
289 (TRY o rtac @{thm TrueI}) THEN_ALL_NEW rtac allI THEN_ALL_NEW |
292 (TRY o rtac @{thm TrueI}) THEN_ALL_NEW rtac allI THEN_ALL_NEW |
290 InductTacs.case_tac context "a" THEN_ALL_NEW split_conjs THEN_ALL_NEW |
293 split_conjs THEN_ALL_NEW |
|
294 InductTacs.case_rule_tac context a (nth exhausts n) THEN_ALL_NEW |
291 asm_full_simp_tac (HOL_ss addsimps inj_dis) THEN_ALL_NEW |
295 asm_full_simp_tac (HOL_ss addsimps inj_dis) THEN_ALL_NEW |
292 REPEAT_ALL_NEW (rtac @{thm arg_cong2[of _ _ _ _ "op \<and>"]}) THEN_ALL_NEW |
296 TRY o REPEAT_ALL_NEW (rtac @{thm arg_cong2[of _ _ _ _ "op \<and>"]}) THEN_ALL_NEW |
293 TRY o eresolve_tac (map (fn x => @{thm equivp_rspl} OF [x]) equivps) THEN_ALL_NEW |
297 TRY o eresolve_tac (resl @ resr) THEN_ALL_NEW |
294 TRY o eresolve_tac (map (fn x => @{thm equivp_rspr} OF [x]) equivps) THEN_ALL_NEW |
298 asm_full_simp_tac (HOL_ss addsimps inj_dis) |
295 TRY o rtac refl |
|
296 ) 1; |
299 ) 1; |
297 val t1 = Goal.prove ctxt names [] g1 tac; |
300 val t1 = Goal.prove ctxt [] [] g1 tac; |
298 val t2 = Goal.prove ctxt names [] g2 tac; |
301 val t2 = Goal.prove ctxt [] [] g2 tac; |
299 in |
302 in |
300 [t1, t2] |
303 Variable.export ctxt' ctxt [t1, t2] |
301 end |
304 end |
302 *} |
305 *} |
303 |
306 |
304 |
307 |
305 end |
308 end |