equal
deleted
inserted
replaced
443 |
443 |
444 val exi_zero = @{lemma "P (0::perm) ==> (? x. P x)" by auto} |
444 val exi_zero = @{lemma "P (0::perm) ==> (? x. P x)" by auto} |
445 |
445 |
446 fun cases_tac intros ctxt = |
446 fun cases_tac intros ctxt = |
447 let |
447 let |
448 val prod_simps = @{thms split_conv prod_alpha_def prod_rel.simps} |
448 val prod_simps = @{thms split_conv prod_alpha_def prod_rel_def} |
449 |
449 |
450 val unbound_tac = REPEAT o (etac @{thm conjE}) THEN' atac |
450 val unbound_tac = REPEAT o (etac @{thm conjE}) THEN' atac |
451 |
451 |
452 val bound_tac = |
452 val bound_tac = |
453 EVERY' [ rtac exi_zero, |
453 EVERY' [ rtac exi_zero, |
491 let |
491 let |
492 val prems' = map (transform_prem1 context pred_names) prems |
492 val prems' = map (transform_prem1 context pred_names) prems |
493 in |
493 in |
494 resolve_tac prems' 1 |
494 resolve_tac prems' 1 |
495 end) ctxt |
495 end) ctxt |
496 val prod_simps = @{thms split_conv permute_prod.simps prod_alpha_def prod_rel.simps alphas} |
496 val prod_simps = @{thms split_conv permute_prod.simps prod_alpha_def prod_rel_def alphas} |
497 in |
497 in |
498 EVERY' |
498 EVERY' |
499 [ etac exi_neg, |
499 [ etac exi_neg, |
500 resolve_tac @{thms alpha_sym_eqvt}, |
500 resolve_tac @{thms alpha_sym_eqvt}, |
501 asm_full_simp_tac (HOL_ss addsimps prod_simps), |
501 asm_full_simp_tac (HOL_ss addsimps prod_simps), |
541 HEADGOAL (rtac exi_inst) |
541 HEADGOAL (rtac exi_inst) |
542 end) |
542 end) |
543 |
543 |
544 fun non_trivial_cases_tac pred_names intros ctxt = |
544 fun non_trivial_cases_tac pred_names intros ctxt = |
545 let |
545 let |
546 val prod_simps = @{thms split_conv alphas permute_prod.simps prod_alpha_def prod_rel.simps} |
546 val prod_simps = @{thms split_conv alphas permute_prod.simps prod_alpha_def prod_rel_def} |
547 in |
547 in |
548 resolve_tac intros |
548 resolve_tac intros |
549 THEN_ALL_NEW (asm_simp_tac HOL_basic_ss THEN' |
549 THEN_ALL_NEW (asm_simp_tac HOL_basic_ss THEN' |
550 TRY o EVERY' (* if binders are present *) |
550 TRY o EVERY' (* if binders are present *) |
551 [ etac @{thm exE}, |
551 [ etac @{thm exE}, |
594 @{lemma "transp R == !x y. R x y --> (!z. R y z --> R x z)" |
594 @{lemma "transp R == !x y. R x y --> (!z. R y z --> R x z)" |
595 by (rule eq_reflection, auto simp add: transp_def)} |
595 by (rule eq_reflection, auto simp add: transp_def)} |
596 |
596 |
597 fun raw_prove_equivp alphas alpha_bns refl symm trans ctxt = |
597 fun raw_prove_equivp alphas alpha_bns refl symm trans ctxt = |
598 let |
598 let |
599 val refl' = map (fold_rule @{thms reflp_def} o atomize) refl |
599 val refl' = map (fold_rule @{thms reflp_def[THEN eq_reflection]} o atomize) refl |
600 val symm' = map (fold_rule @{thms symp_def} o atomize) symm |
600 val symm' = map (fold_rule @{thms symp_def[THEN eq_reflection]} o atomize) symm |
601 val trans' = map (fold_rule [transp_def'] o atomize) trans |
601 val trans' = map (fold_rule [transp_def'] o atomize) trans |
602 |
602 |
603 fun prep_goal t = |
603 fun prep_goal t = |
604 HOLogic.mk_Trueprop (Const (@{const_name "equivp"}, fastype_of t --> @{typ bool}) $ t) |
604 HOLogic.mk_Trueprop (Const (@{const_name "equivp"}, fastype_of t --> @{typ bool}) $ t) |
605 in |
605 in |
669 fun mk_prop ty (x, y) = HOLogic.mk_eq |
669 fun mk_prop ty (x, y) = HOLogic.mk_eq |
670 (HOLogic.size_const ty $ x, HOLogic.size_const ty $ y) |
670 (HOLogic.size_const ty $ x, HOLogic.size_const ty $ y) |
671 |
671 |
672 val props = map2 (fn trm => fn ty => (trm, mk_prop ty)) all_alpha_trms arg_tys |
672 val props = map2 (fn trm => fn ty => (trm, mk_prop ty)) all_alpha_trms arg_tys |
673 |
673 |
674 val ss = HOL_ss addsimps (simps @ @{thms alphas prod_alpha_def prod_rel.simps |
674 val ss = HOL_ss addsimps (simps @ @{thms alphas prod_alpha_def prod_rel_def |
675 permute_prod_def prod.cases prod.recs}) |
675 permute_prod_def prod.cases prod.recs}) |
676 |
676 |
677 val tac = (TRY o REPEAT o etac @{thm exE}) THEN' asm_full_simp_tac ss |
677 val tac = (TRY o REPEAT o etac @{thm exE}) THEN' asm_full_simp_tac ss |
678 in |
678 in |
679 alpha_prove all_alpha_trms props alpha_induct (K tac) ctxt |
679 alpha_prove all_alpha_trms props alpha_induct (K tac) ctxt |
683 (* respectfulness for constructors *) |
683 (* respectfulness for constructors *) |
684 |
684 |
685 fun raw_constr_rsp_tac alpha_intros simps = |
685 fun raw_constr_rsp_tac alpha_intros simps = |
686 let |
686 let |
687 val pre_ss = HOL_ss addsimps @{thms fun_rel_def} |
687 val pre_ss = HOL_ss addsimps @{thms fun_rel_def} |
688 val post_ss = HOL_ss addsimps @{thms alphas prod_alpha_def prod_rel.simps |
688 val post_ss = HOL_ss addsimps @{thms alphas prod_alpha_def prod_rel_def |
689 prod_fv.simps fresh_star_zero permute_zero prod.cases} @ simps |
689 prod_fv.simps fresh_star_zero permute_zero prod.cases} @ simps |
690 in |
690 in |
691 asm_full_simp_tac pre_ss |
691 asm_full_simp_tac pre_ss |
692 THEN' REPEAT o (resolve_tac @{thms allI impI}) |
692 THEN' REPEAT o (resolve_tac @{thms allI impI}) |
693 THEN' resolve_tac alpha_intros |
693 THEN' resolve_tac alpha_intros |
752 |
752 |
753 |
753 |
754 (* transformation of the natural rsp-lemmas into standard form *) |
754 (* transformation of the natural rsp-lemmas into standard form *) |
755 |
755 |
756 val fun_rsp = @{lemma |
756 val fun_rsp = @{lemma |
757 "(!x y. R x y --> f x = f y) ==> (R ===> (op =)) f f" by simp} |
757 "(!x y. R x y --> f x = f y) ==> (R ===> (op =)) f f" by (simp add: fun_rel_def)} |
758 |
758 |
759 fun mk_funs_rsp thm = |
759 fun mk_funs_rsp thm = |
760 thm |
760 thm |
761 |> atomize |
761 |> atomize |
762 |> single |
762 |> single |
763 |> curry (op OF) fun_rsp |
763 |> curry (op OF) fun_rsp |
764 |
764 |
765 |
765 |
766 val permute_rsp = @{lemma |
766 val permute_rsp = @{lemma |
767 "(!x y p. R x y --> R (permute p x) (permute p y)) |
767 "(!x y p. R x y --> R (permute p x) (permute p y)) |
768 ==> ((op =) ===> R ===> R) permute permute" by simp} |
768 ==> ((op =) ===> R ===> R) permute permute" by (simp add: fun_rel_def)} |
769 |
769 |
770 fun mk_alpha_permute_rsp thm = |
770 fun mk_alpha_permute_rsp thm = |
771 thm |
771 thm |
772 |> atomize |
772 |> atomize |
773 |> single |
773 |> single |