666 val symp = HOLogic.mk_imp (alpha $ var $ var2, alpha $ var2 $ var); |
666 val symp = HOLogic.mk_imp (alpha $ var $ var2, alpha $ var2 $ var); |
667 val transp = HOLogic.mk_imp (alpha $ var $ var2, |
667 val transp = HOLogic.mk_imp (alpha $ var $ var2, |
668 HOLogic.mk_all (z, ty, |
668 HOLogic.mk_all (z, ty, |
669 HOLogic.mk_imp (alpha $ var2 $ var3, alpha $ var $ var3))) |
669 HOLogic.mk_imp (alpha $ var2 $ var3, alpha $ var $ var3))) |
670 in |
670 in |
671 ((alpha $ var $ var), (symp, transp)) |
671 (symp, transp) |
672 end; |
672 end; |
673 val (refl_eqs, eqs) = split_list (map build_alpha alphas) |
673 val eqs = map build_alpha alphas |
674 val (sym_eqs, trans_eqs) = split_list eqs |
674 val (sym_eqs, trans_eqs) = split_list eqs |
675 fun conj l = @{term Trueprop} $ foldr1 HOLogic.mk_conj l |
675 fun conj l = @{term Trueprop} $ foldr1 HOLogic.mk_conj l |
676 in |
676 in |
677 (conj refl_eqs, (conj sym_eqs, conj trans_eqs)) |
677 (conj sym_eqs, conj trans_eqs) |
678 end |
678 end |
679 *} |
679 *} |
680 |
680 |
681 ML {* |
681 ML {* |
682 fun reflp_tac induct inj ctxt = |
682 fun build_alpha_refl_gl fv_alphas_lst = |
|
683 let |
|
684 val (fvs_alphas, ls) = split_list fv_alphas_lst; |
|
685 val (_, alpha_ts) = split_list fvs_alphas; |
|
686 val tys = map (domain_type o fastype_of) alpha_ts; |
|
687 val names = Datatype_Prop.make_tnames tys; |
|
688 val args = map Free (names ~~ tys); |
|
689 fun mk_alpha_refl arg (_, alpha) = alpha $ arg $ arg; |
|
690 fun refl_eq_arg ((alpha, arg), l) = |
|
691 foldr1 HOLogic.mk_conj |
|
692 ((alpha $ arg $ arg) :: |
|
693 (map (mk_alpha_refl arg) l)) |
|
694 val eqs = map refl_eq_arg ((alpha_ts ~~ args) ~~ ls) |
|
695 in |
|
696 (names, HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj eqs)) |
|
697 end |
|
698 *} |
|
699 |
|
700 ML {* |
|
701 fun reflp_tac induct eq_iff ctxt = |
683 rtac induct THEN_ALL_NEW |
702 rtac induct THEN_ALL_NEW |
684 simp_tac ((mk_minimal_ss ctxt) addsimps inj) THEN_ALL_NEW |
703 simp_tac ((mk_minimal_ss ctxt) addsimps eq_iff) THEN_ALL_NEW |
685 split_conjs THEN_ALL_NEW REPEAT o rtac @{thm exI[of _ "0 :: perm"]} |
704 split_conjs THEN_ALL_NEW REPEAT o rtac @{thm exI[of _ "0 :: perm"]} |
686 THEN_ALL_NEW split_conjs THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps |
705 THEN_ALL_NEW split_conjs THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps |
687 @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv |
706 @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv |
688 add_0_left supp_zero_perm Int_empty_left split_conv}) |
707 add_0_left supp_zero_perm Int_empty_left split_conv}) |
689 *} |
708 *} |
690 |
709 |
|
710 ML {* |
|
711 fun build_alpha_refl fv_alphas_lst induct eq_iff ctxt = |
|
712 let |
|
713 val (names, gl) = build_alpha_refl_gl fv_alphas_lst; |
|
714 val refl_conj = Goal.prove ctxt names [] gl (fn _ => reflp_tac induct eq_iff ctxt 1); |
|
715 in |
|
716 HOLogic.conj_elims refl_conj |
|
717 end |
|
718 *} |
691 |
719 |
692 lemma exi_neg: "\<exists>(pi :: perm). P pi \<Longrightarrow> (\<And>(p :: perm). P p \<Longrightarrow> Q (- p)) \<Longrightarrow> \<exists>pi. Q pi" |
720 lemma exi_neg: "\<exists>(pi :: perm). P pi \<Longrightarrow> (\<And>(p :: perm). P p \<Longrightarrow> Q (- p)) \<Longrightarrow> \<exists>pi. Q pi" |
693 apply (erule exE) |
721 apply (erule exE) |
694 apply (rule_tac x="-pi" in exI) |
722 apply (rule_tac x="-pi" in exI) |
695 by auto |
723 by auto |
785 resolve_tac symps THEN' |
813 resolve_tac symps THEN' |
786 rtac @{thm transp_aux} THEN' resolve_tac transps |
814 rtac @{thm transp_aux} THEN' resolve_tac transps |
787 *} |
815 *} |
788 |
816 |
789 ML {* |
817 ML {* |
790 fun build_equivps alphas term_induct alpha_induct term_inj alpha_inj distinct cases eqvt ctxt = |
818 fun build_equivps alphas reflps alpha_induct term_inj alpha_inj distinct cases eqvt ctxt = |
791 let |
819 let |
792 val ([x, y, z], ctxt') = Variable.variant_fixes ["x","y","z"] ctxt; |
820 val ([x, y, z], ctxt') = Variable.variant_fixes ["x","y","z"] ctxt; |
793 val (reflg, (symg, transg)) = build_alpha_refl_gl alphas (x, y, z) |
821 val (symg, transg) = build_alpha_sym_trans_gl alphas (x, y, z) |
794 fun reflp_tac' _ = reflp_tac term_induct alpha_inj ctxt 1; |
|
795 fun symp_tac' _ = symp_tac alpha_induct alpha_inj eqvt ctxt 1; |
822 fun symp_tac' _ = symp_tac alpha_induct alpha_inj eqvt ctxt 1; |
796 fun transp_tac' _ = transp_tac ctxt alpha_induct alpha_inj term_inj distinct cases eqvt 1; |
823 fun transp_tac' _ = transp_tac ctxt alpha_induct alpha_inj term_inj distinct cases eqvt 1; |
797 val reflt = Goal.prove ctxt' [] [] reflg reflp_tac'; |
824 val symp_loc = Goal.prove ctxt' [] [] symg symp_tac'; |
798 val symt = Goal.prove ctxt' [] [] symg symp_tac'; |
825 val transp_loc = Goal.prove ctxt' [] [] transg transp_tac'; |
799 val transt = Goal.prove ctxt' [] [] transg transp_tac'; |
826 val [symp, transp] = Variable.export ctxt' ctxt [symp_loc, transp_loc] |
800 val [refltg, symtg, transtg] = Variable.export ctxt' ctxt [reflt, symt, transt] |
827 val symps = HOLogic.conj_elims symp |
801 val reflts = HOLogic.conj_elims refltg |
828 val transps = HOLogic.conj_elims transp |
802 val symts = HOLogic.conj_elims symtg |
|
803 val transts = HOLogic.conj_elims transtg |
|
804 fun equivp alpha = |
829 fun equivp alpha = |
805 let |
830 let |
806 val equivp = Const (@{const_name equivp}, fastype_of alpha --> @{typ bool}) |
831 val equivp = Const (@{const_name equivp}, fastype_of alpha --> @{typ bool}) |
807 val goal = @{term Trueprop} $ (equivp $ alpha) |
832 val goal = @{term Trueprop} $ (equivp $ alpha) |
808 fun tac _ = equivp_tac reflts symts transts 1 |
833 fun tac _ = equivp_tac reflps symps transps 1 |
809 in |
834 in |
810 Goal.prove ctxt [] [] goal tac |
835 Goal.prove ctxt [] [] goal tac |
811 end |
836 end |
812 in |
837 in |
813 map equivp alphas |
838 map equivp alphas |