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}) |
|
708 *} |
|
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 *} |
|
719 |
|
720 ML {* |
|
721 fun build_alpha_alphabn fv_alphas_lst inducts eq_iff ctxt = |
|
722 let |
|
723 val (fvs_alphas, ls) = split_list fv_alphas_lst; |
|
724 val (_, alpha_ts) = split_list fvs_alphas; |
|
725 val tys = map (domain_type o fastype_of) alpha_ts; |
|
726 val names = Datatype_Prop.make_tnames tys; |
|
727 val names2 = Name.variant_list names names; |
|
728 val args = map Free (names ~~ tys); |
|
729 val args2 = map Free (names2 ~~ tys); |
|
730 fun alpha_alphabn ((alpha, (arg, arg2)), (no, l)) = |
|
731 if l = [] then [] else |
|
732 let |
|
733 val alpha_bns = map snd l; |
|
734 val lhs = alpha $ arg $ arg2; |
|
735 val rhs = foldr1 HOLogic.mk_conj (map (fn x => x $ arg $ arg2) alpha_bns); |
|
736 val gl = Logic.mk_implies (HOLogic.mk_Trueprop lhs, HOLogic.mk_Trueprop rhs); |
|
737 fun tac _ = (etac (nth inducts no) THEN_ALL_NEW TRY o rtac @{thm TrueI} |
|
738 THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps eq_iff)) 1 |
|
739 val th = Goal.prove ctxt (names @ names2) [] gl tac; |
|
740 in |
|
741 Project_Rule.projects ctxt (1 upto length l) th |
|
742 end; |
|
743 val eqs = map alpha_alphabn ((alpha_ts ~~ (args ~~ args2)) ~~ ((0 upto (length ls - 1)) ~~ ls)); |
|
744 in |
|
745 flat eqs |
|
746 end |
689 *} |
747 *} |
690 |
748 |
691 |
749 |
692 lemma exi_neg: "\<exists>(pi :: perm). P pi \<Longrightarrow> (\<And>(p :: perm). P p \<Longrightarrow> Q (- p)) \<Longrightarrow> \<exists>pi. Q pi" |
750 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) |
751 apply (erule exE) |
785 resolve_tac symps THEN' |
843 resolve_tac symps THEN' |
786 rtac @{thm transp_aux} THEN' resolve_tac transps |
844 rtac @{thm transp_aux} THEN' resolve_tac transps |
787 *} |
845 *} |
788 |
846 |
789 ML {* |
847 ML {* |
790 fun build_equivps alphas term_induct alpha_induct term_inj alpha_inj distinct cases eqvt ctxt = |
848 fun build_equivps alphas reflps alpha_induct term_inj alpha_inj distinct cases eqvt ctxt = |
791 let |
849 let |
792 val ([x, y, z], ctxt') = Variable.variant_fixes ["x","y","z"] ctxt; |
850 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) |
851 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; |
852 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; |
853 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'; |
854 val symp_loc = Goal.prove ctxt' [] [] symg symp_tac'; |
798 val symt = Goal.prove ctxt' [] [] symg symp_tac'; |
855 val transp_loc = Goal.prove ctxt' [] [] transg transp_tac'; |
799 val transt = Goal.prove ctxt' [] [] transg transp_tac'; |
856 val [symp, transp] = Variable.export ctxt' ctxt [symp_loc, transp_loc] |
800 val [refltg, symtg, transtg] = Variable.export ctxt' ctxt [reflt, symt, transt] |
857 val symps = HOLogic.conj_elims symp |
801 val reflts = HOLogic.conj_elims refltg |
858 val transps = HOLogic.conj_elims transp |
802 val symts = HOLogic.conj_elims symtg |
|
803 val transts = HOLogic.conj_elims transtg |
|
804 fun equivp alpha = |
859 fun equivp alpha = |
805 let |
860 let |
806 val equivp = Const (@{const_name equivp}, fastype_of alpha --> @{typ bool}) |
861 val equivp = Const (@{const_name equivp}, fastype_of alpha --> @{typ bool}) |
807 val goal = @{term Trueprop} $ (equivp $ alpha) |
862 val goal = @{term Trueprop} $ (equivp $ alpha) |
808 fun tac _ = equivp_tac reflts symts transts 1 |
863 fun tac _ = equivp_tac reflps symps transps 1 |
809 in |
864 in |
810 Goal.prove ctxt [] [] goal tac |
865 Goal.prove ctxt [] [] goal tac |
811 end |
866 end |
812 in |
867 in |
813 map equivp alphas |
868 map equivp alphas |