equal
deleted
inserted
replaced
24 |
24 |
25 val alpha_prove: term list -> (term * ((term * term) -> term)) list -> thm -> |
25 val alpha_prove: term list -> (term * ((term * term) -> term)) list -> thm -> |
26 (Proof.context -> int -> tactic) -> Proof.context -> thm list |
26 (Proof.context -> int -> tactic) -> Proof.context -> thm list |
27 |
27 |
28 val raw_prove_refl: term list -> term list -> thm list -> thm -> Proof.context -> thm list |
28 val raw_prove_refl: term list -> term list -> thm list -> thm -> Proof.context -> thm list |
29 val raw_prove_sym: term list -> thm list -> thm -> Proof.context -> thm list |
29 val raw_prove_sym: term list -> thm list -> thm -> thm list -> Proof.context -> thm list |
30 val raw_prove_trans: term list -> thm list -> thm list -> thm -> thm list -> Proof.context -> thm list |
30 val raw_prove_trans: term list -> thm list -> thm list -> thm -> thm list -> thm list -> |
|
31 Proof.context -> thm list |
31 val raw_prove_equivp: term list -> term list -> thm list -> thm list -> thm list -> |
32 val raw_prove_equivp: term list -> term list -> thm list -> thm list -> thm list -> |
32 Proof.context -> thm list * thm list |
33 Proof.context -> thm list * thm list |
33 |
34 |
34 val raw_prove_bn_imp: term list -> term list -> thm list -> thm -> Proof.context -> thm list |
35 val raw_prove_bn_imp: term list -> term list -> thm list -> thm -> Proof.context -> thm list |
35 val raw_fv_bn_rsp_aux: term list -> term list -> term list -> term list -> |
36 val raw_fv_bn_rsp_aux: term list -> term list -> term list -> term list -> |
490 |
491 |
491 val exi_neg = @{lemma "(EX (p::perm). P p) ==> (!!q. P q ==> Q (- q)) ==> EX p. Q p" |
492 val exi_neg = @{lemma "(EX (p::perm). P p) ==> (!!q. P q ==> Q (- q)) ==> EX p. Q p" |
492 by (erule exE, rule_tac x="-p" in exI, auto)} |
493 by (erule exE, rule_tac x="-p" in exI, auto)} |
493 |
494 |
494 (* for premises that contain binders *) |
495 (* for premises that contain binders *) |
495 fun prem_bound_tac pred_names ctxt = |
496 fun prem_bound_tac pred_names alpha_eqvt ctxt = |
496 let |
497 let |
497 fun trans_prem_tac pred_names ctxt = |
498 fun trans_prem_tac pred_names ctxt = |
498 SUBPROOF (fn {prems, context, ...} => |
499 SUBPROOF (fn {prems, context, ...} => |
499 let |
500 let |
500 val prems' = map (transform_prem1 context pred_names) prems |
501 val prems' = map (transform_prem1 context pred_names) prems |
505 in |
506 in |
506 EVERY' |
507 EVERY' |
507 [ etac exi_neg, |
508 [ etac exi_neg, |
508 resolve_tac @{thms alpha_sym_eqvt}, |
509 resolve_tac @{thms alpha_sym_eqvt}, |
509 asm_full_simp_tac (HOL_ss addsimps prod_simps), |
510 asm_full_simp_tac (HOL_ss addsimps prod_simps), |
510 eqvt_tac ctxt eqvt_relaxed_config THEN' rtac @{thm refl}, |
511 eqvt_tac ctxt (eqvt_relaxed_config addpres alpha_eqvt) THEN' rtac @{thm refl}, |
511 trans_prem_tac pred_names ctxt ] |
512 trans_prem_tac pred_names ctxt] |
512 end |
513 end |
513 |
514 |
514 fun raw_prove_sym alpha_trms alpha_intros alpha_induct ctxt = |
515 fun raw_prove_sym alpha_trms alpha_intros alpha_induct alpha_eqvt ctxt = |
515 let |
516 let |
516 val props = map (fn t => fn (x, y) => t $ y $ x) alpha_trms |
517 val props = map (fn t => fn (x, y) => t $ y $ x) alpha_trms |
517 |
518 |
518 fun tac ctxt = |
519 fun tac ctxt = |
519 let |
520 let |
520 val alpha_names = map (fst o dest_Const) alpha_trms |
521 val alpha_names = map (fst o dest_Const) alpha_trms |
521 in |
522 in |
522 resolve_tac alpha_intros THEN_ALL_NEW |
523 resolve_tac alpha_intros THEN_ALL_NEW |
523 FIRST' [atac, rtac @{thm sym} THEN' atac, prem_bound_tac alpha_names ctxt] |
524 FIRST' [atac, rtac @{thm sym} THEN' atac, prem_bound_tac alpha_names alpha_eqvt ctxt] |
524 end |
525 end |
525 in |
526 in |
526 alpha_prove alpha_trms (alpha_trms ~~ props) alpha_induct tac ctxt |
527 alpha_prove alpha_trms (alpha_trms ~~ props) alpha_induct tac ctxt |
527 end |
528 end |
528 |
529 |
547 val exi_inst = Drule.instantiate' [SOME (@{ctyp "perm"})] [NONE, SOME pq_inst] @{thm exI} |
548 val exi_inst = Drule.instantiate' [SOME (@{ctyp "perm"})] [NONE, SOME pq_inst] @{thm exI} |
548 in |
549 in |
549 HEADGOAL (rtac exi_inst) |
550 HEADGOAL (rtac exi_inst) |
550 end) |
551 end) |
551 |
552 |
552 fun non_trivial_cases_tac pred_names intros ctxt = |
553 fun non_trivial_cases_tac pred_names intros alpha_eqvt ctxt = |
553 let |
554 let |
554 val prod_simps = @{thms split_conv alphas permute_prod.simps prod_alpha_def prod_rel_def} |
555 val prod_simps = @{thms split_conv alphas permute_prod.simps prod_alpha_def prod_rel_def} |
555 in |
556 in |
556 resolve_tac intros |
557 resolve_tac intros |
557 THEN_ALL_NEW (asm_simp_tac HOL_basic_ss THEN' |
558 THEN_ALL_NEW (asm_simp_tac HOL_basic_ss THEN' |
560 etac @{thm exE}, |
561 etac @{thm exE}, |
561 perm_inst_tac ctxt, |
562 perm_inst_tac ctxt, |
562 resolve_tac @{thms alpha_trans_eqvt}, |
563 resolve_tac @{thms alpha_trans_eqvt}, |
563 atac, |
564 atac, |
564 aatac pred_names ctxt, |
565 aatac pred_names ctxt, |
565 eqvt_tac ctxt eqvt_relaxed_config THEN' rtac @{thm refl}, |
566 eqvt_tac ctxt (eqvt_relaxed_config addpres alpha_eqvt) THEN' rtac @{thm refl}, |
566 asm_full_simp_tac (HOL_ss addsimps prod_simps) ]) |
567 asm_full_simp_tac (HOL_ss addsimps prod_simps) ]) |
567 end |
568 end |
568 |
569 |
569 fun prove_trans_tac pred_names raw_dt_thms intros cases ctxt = |
570 fun prove_trans_tac pred_names raw_dt_thms intros cases alpha_eqvt ctxt = |
570 let |
571 let |
571 fun all_cases ctxt = |
572 fun all_cases ctxt = |
572 asm_full_simp_tac (HOL_basic_ss addsimps raw_dt_thms) |
573 asm_full_simp_tac (HOL_basic_ss addsimps raw_dt_thms) |
573 THEN' TRY o non_trivial_cases_tac pred_names intros ctxt |
574 THEN' TRY o non_trivial_cases_tac pred_names intros alpha_eqvt ctxt |
574 in |
575 in |
575 EVERY' [ rtac @{thm allI}, rtac @{thm impI}, |
576 EVERY' [ rtac @{thm allI}, rtac @{thm impI}, |
576 ecases_tac cases ctxt THEN_ALL_NEW all_cases ctxt ] |
577 ecases_tac cases ctxt THEN_ALL_NEW all_cases ctxt ] |
577 end |
578 end |
578 |
579 |
583 val rhs = alpha_trm $ arg1 $ (Bound 0) |
584 val rhs = alpha_trm $ arg1 $ (Bound 0) |
584 in |
585 in |
585 HOLogic.all_const arg_ty $ Abs ("z", arg_ty, HOLogic.mk_imp (mid, rhs)) |
586 HOLogic.all_const arg_ty $ Abs ("z", arg_ty, HOLogic.mk_imp (mid, rhs)) |
586 end |
587 end |
587 |
588 |
588 fun raw_prove_trans alpha_trms raw_dt_thms alpha_intros alpha_induct alpha_cases ctxt = |
589 fun raw_prove_trans alpha_trms raw_dt_thms alpha_intros alpha_induct alpha_cases alpha_eqvt ctxt = |
589 let |
590 let |
590 val alpha_names = map (fst o dest_Const) alpha_trms |
591 val alpha_names = map (fst o dest_Const) alpha_trms |
591 val props = map prep_trans_goal alpha_trms |
592 val props = map prep_trans_goal alpha_trms |
592 in |
593 in |
593 alpha_prove alpha_trms (alpha_trms ~~ props) alpha_induct |
594 alpha_prove alpha_trms (alpha_trms ~~ props) alpha_induct |
594 (prove_trans_tac alpha_names raw_dt_thms alpha_intros alpha_cases) ctxt |
595 (prove_trans_tac alpha_names raw_dt_thms alpha_intros alpha_cases alpha_eqvt) ctxt |
595 end |
596 end |
596 |
597 |
597 |
598 |
598 (** proves the equivp predicate for all alphas **) |
599 (** proves the equivp predicate for all alphas **) |
599 |
600 |