605 in |
603 in |
606 (((all_fvs, ordered_fvs), alphas), lthy''') |
604 (((all_fvs, ordered_fvs), alphas), lthy''') |
607 end |
605 end |
608 *} |
606 *} |
609 |
607 |
610 |
608 end |
611 |
|
612 ML {* |
|
613 fun build_alpha_sym_trans_gl alphas (x, y, z) = |
|
614 let |
|
615 fun build_alpha alpha = |
|
616 let |
|
617 val ty = domain_type (fastype_of alpha); |
|
618 val var = Free(x, ty); |
|
619 val var2 = Free(y, ty); |
|
620 val var3 = Free(z, ty); |
|
621 val symp = HOLogic.mk_imp (alpha $ var $ var2, alpha $ var2 $ var); |
|
622 val transp = HOLogic.mk_imp (alpha $ var $ var2, |
|
623 HOLogic.mk_all (z, ty, |
|
624 HOLogic.mk_imp (alpha $ var2 $ var3, alpha $ var $ var3))) |
|
625 in |
|
626 (symp, transp) |
|
627 end; |
|
628 val eqs = map build_alpha alphas |
|
629 val (sym_eqs, trans_eqs) = split_list eqs |
|
630 fun conj l = @{term Trueprop} $ foldr1 HOLogic.mk_conj l |
|
631 in |
|
632 (conj sym_eqs, conj trans_eqs) |
|
633 end |
|
634 *} |
|
635 |
|
636 ML {* |
|
637 fun build_alpha_refl_gl fv_alphas_lst alphas = |
|
638 let |
|
639 val (fvs_alphas, _) = split_list fv_alphas_lst; |
|
640 val (_, alpha_ts) = split_list fvs_alphas; |
|
641 val tys = map (domain_type o fastype_of) alpha_ts; |
|
642 val names = Datatype_Prop.make_tnames tys; |
|
643 val args = map Free (names ~~ tys); |
|
644 fun find_alphas ty x = |
|
645 domain_type (fastype_of x) = ty; |
|
646 fun refl_eq_arg (ty, arg) = |
|
647 let |
|
648 val rel_alphas = filter (find_alphas ty) alphas; |
|
649 in |
|
650 map (fn x => x $ arg $ arg) rel_alphas |
|
651 end; |
|
652 (* Flattening loses the induction structure *) |
|
653 val eqs = map (foldr1 HOLogic.mk_conj) (map refl_eq_arg (tys ~~ args)) |
|
654 in |
|
655 (names, HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj eqs)) |
|
656 end |
|
657 *} |
|
658 |
|
659 ML {* |
|
660 fun reflp_tac induct eq_iff = |
|
661 rtac induct THEN_ALL_NEW |
|
662 simp_tac (HOL_basic_ss addsimps eq_iff) THEN_ALL_NEW |
|
663 split_conj_tac THEN_ALL_NEW REPEAT o rtac @{thm exI[of _ "0 :: perm"]} |
|
664 THEN_ALL_NEW split_conj_tac THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps |
|
665 @{thms alphas fresh_star_def fresh_zero_perm permute_zero ball_triv |
|
666 add_0_left supp_zero_perm Int_empty_left split_conv}) |
|
667 *} |
|
668 |
|
669 ML {* |
|
670 fun build_alpha_refl fv_alphas_lst alphas induct eq_iff ctxt = |
|
671 let |
|
672 val (names, gl) = build_alpha_refl_gl fv_alphas_lst alphas; |
|
673 val refl_conj = Goal.prove ctxt names [] gl (fn _ => reflp_tac induct eq_iff 1); |
|
674 in |
|
675 HOLogic.conj_elims refl_conj |
|
676 end |
|
677 *} |
|
678 |
|
679 lemma exi_neg: "\<exists>(pi :: perm). P pi \<Longrightarrow> (\<And>(p :: perm). P p \<Longrightarrow> Q (- p)) \<Longrightarrow> \<exists>pi. Q pi" |
|
680 apply (erule exE) |
|
681 apply (rule_tac x="-pi" in exI) |
|
682 by auto |
|
683 |
|
684 ML {* |
|
685 fun symp_tac induct inj eqvt ctxt = |
|
686 rel_indtac induct THEN_ALL_NEW |
|
687 simp_tac (HOL_basic_ss addsimps inj) THEN_ALL_NEW split_conj_tac |
|
688 THEN_ALL_NEW |
|
689 REPEAT o etac @{thm exi_neg} |
|
690 THEN_ALL_NEW |
|
691 split_conj_tac THEN_ALL_NEW |
|
692 asm_full_simp_tac (HOL_ss addsimps @{thms supp_minus_perm minus_add[symmetric]}) THEN_ALL_NEW |
|
693 TRY o (resolve_tac @{thms alphas_compose_sym2} ORELSE' resolve_tac @{thms alphas_compose_sym}) THEN_ALL_NEW |
|
694 (asm_full_simp_tac (HOL_ss addsimps (eqvt @ all_eqvts ctxt))) |
|
695 *} |
|
696 |
|
697 |
|
698 lemma exi_sum: "\<exists>(pi :: perm). P pi \<Longrightarrow> \<exists>(pi :: perm). Q pi \<Longrightarrow> (\<And>(p :: perm) (pi :: perm). P p \<Longrightarrow> Q pi \<Longrightarrow> R (pi + p)) \<Longrightarrow> \<exists>pi. R pi" |
|
699 apply (erule exE)+ |
|
700 apply (rule_tac x="pia + pi" in exI) |
|
701 by auto |
|
702 |
|
703 |
|
704 ML {* |
|
705 fun eetac rule = |
|
706 Subgoal.FOCUS_PARAMS (fn focus => |
|
707 let |
|
708 val concl = #concl focus |
|
709 val prems = Logic.strip_imp_prems (term_of concl) |
|
710 val exs = filter (fn x => is_ex (HOLogic.dest_Trueprop x)) prems |
|
711 val cexs = map (SOME o (cterm_of (ProofContext.theory_of (#context focus)))) exs |
|
712 val thins = map (fn cex => Drule.instantiate' [] [cex] Drule.thin_rl) cexs |
|
713 in |
|
714 (etac rule THEN' RANGE[atac, eresolve_tac thins]) 1 |
|
715 end |
|
716 ) |
|
717 *} |
|
718 |
|
719 ML {* |
|
720 fun transp_tac ctxt induct alpha_inj term_inj distinct cases eqvt = |
|
721 rel_indtac induct THEN_ALL_NEW |
|
722 (TRY o rtac allI THEN' imp_elim_tac cases ctxt) THEN_ALL_NEW |
|
723 asm_full_simp_tac (HOL_basic_ss addsimps alpha_inj) THEN_ALL_NEW |
|
724 split_conj_tac THEN_ALL_NEW REPEAT o (eetac @{thm exi_sum} ctxt) THEN_ALL_NEW split_conj_tac |
|
725 THEN_ALL_NEW (asm_full_simp_tac (HOL_ss addsimps (term_inj @ distinct))) |
|
726 THEN_ALL_NEW split_conj_tac THEN_ALL_NEW |
|
727 TRY o (eresolve_tac @{thms alphas_compose_trans2} ORELSE' eresolve_tac @{thms alphas_compose_trans}) THEN_ALL_NEW |
|
728 (asm_full_simp_tac (HOL_ss addsimps (all_eqvts ctxt @ eqvt @ term_inj @ distinct))) |
|
729 *} |
|
730 |
|
731 lemma transpI: |
|
732 "(\<And>xa ya. R xa ya \<longrightarrow> (\<forall>z. R ya z \<longrightarrow> R xa z)) \<Longrightarrow> transp R" |
|
733 unfolding transp_def |
|
734 by blast |
|
735 |
|
736 ML {* |
|
737 fun equivp_tac reflps symps transps = |
|
738 (*let val _ = tracing (PolyML.makestring (reflps, symps, transps)) in *) |
|
739 simp_tac (HOL_ss addsimps @{thms equivp_reflp_symp_transp reflp_def symp_def}) |
|
740 THEN' rtac conjI THEN' rtac allI THEN' |
|
741 resolve_tac reflps THEN' |
|
742 rtac conjI THEN' rtac allI THEN' rtac allI THEN' |
|
743 resolve_tac symps THEN' |
|
744 rtac @{thm transpI} THEN' resolve_tac transps |
|
745 *} |
|
746 |
|
747 ML {* |
|
748 fun build_equivps alphas reflps alpha_induct term_inj alpha_inj distinct cases eqvt ctxt = |
|
749 let |
|
750 val ([x, y, z], ctxt') = Variable.variant_fixes ["x","y","z"] ctxt; |
|
751 val (symg, transg) = build_alpha_sym_trans_gl alphas (x, y, z) |
|
752 fun symp_tac' _ = symp_tac alpha_induct alpha_inj eqvt ctxt 1; |
|
753 fun transp_tac' _ = transp_tac ctxt alpha_induct alpha_inj term_inj distinct cases eqvt 1; |
|
754 val symp_loc = Goal.prove ctxt' [] [] symg symp_tac'; |
|
755 val transp_loc = Goal.prove ctxt' [] [] transg transp_tac'; |
|
756 val [symp, transp] = Variable.export ctxt' ctxt [symp_loc, transp_loc] |
|
757 val symps = HOLogic.conj_elims symp |
|
758 val transps = HOLogic.conj_elims transp |
|
759 fun equivp alpha = |
|
760 let |
|
761 val equivp = Const (@{const_name equivp}, fastype_of alpha --> @{typ bool}) |
|
762 val goal = @{term Trueprop} $ (equivp $ alpha) |
|
763 fun tac _ = equivp_tac reflps symps transps 1 |
|
764 in |
|
765 Goal.prove ctxt [] [] goal tac |
|
766 end |
|
767 in |
|
768 map equivp alphas |
|
769 end |
|
770 *} |
|
771 |
|
772 lemma not_in_union: "c \<notin> a \<union> b \<equiv> (c \<notin> a \<and> c \<notin> b)" |
|
773 by auto |
|
774 |
|
775 ML {* |
|
776 fun supports_tac perm = |
|
777 simp_tac (HOL_ss addsimps @{thms supports_def not_in_union} @ perm) THEN_ALL_NEW ( |
|
778 REPEAT o rtac allI THEN' REPEAT o rtac impI THEN' split_conj_tac THEN' |
|
779 asm_full_simp_tac (HOL_ss addsimps @{thms fresh_def[symmetric] |
|
780 swap_fresh_fresh fresh_atom swap_at_base_simps(3) swap_atom_image_fresh |
|
781 supp_fset_to_set supp_fmap_atom})) |
|
782 *} |
|
783 |
|
784 ML {* |
|
785 fun mk_supp ty x = |
|
786 Const (@{const_name supp}, ty --> @{typ "atom set"}) $ x |
|
787 *} |
|
788 |
|
789 ML {* |
|
790 fun mk_supports_eq thy cnstr = |
|
791 let |
|
792 val (tys, ty) = (strip_type o fastype_of) cnstr |
|
793 val names = Datatype_Prop.make_tnames tys |
|
794 val frees = map Free (names ~~ tys) |
|
795 val rhs = list_comb (cnstr, frees) |
|
796 |
|
797 fun mk_supp_arg (x, ty) = |
|
798 if is_atom thy ty then mk_supp @{typ atom} (mk_atom ty $ x) else |
|
799 if is_atom_set thy ty then mk_supp @{typ "atom set"} (mk_atom_set x) else |
|
800 if is_atom_fset thy ty then mk_supp @{typ "atom set"} (mk_atom_fset x) |
|
801 else mk_supp ty x |
|
802 val lhss = map mk_supp_arg (frees ~~ tys) |
|
803 val supports = Const(@{const_name "supports"}, @{typ "atom set"} --> ty --> @{typ bool}) |
|
804 val eq = HOLogic.mk_Trueprop (supports $ mk_union lhss $ rhs) |
|
805 in |
|
806 (names, eq) |
|
807 end |
|
808 *} |
|
809 |
|
810 ML {* |
|
811 fun prove_supports ctxt perms cnst = |
|
812 let |
|
813 val (names, eq) = mk_supports_eq (ProofContext.theory_of ctxt) cnst |
|
814 in |
|
815 Goal.prove ctxt names [] eq (fn _ => supports_tac perms 1) |
|
816 end |
|
817 *} |
|
818 |
|
819 ML {* |
|
820 fun mk_fs tys = |
|
821 let |
|
822 val names = Datatype_Prop.make_tnames tys |
|
823 val frees = map Free (names ~~ tys) |
|
824 val supps = map2 mk_supp tys frees |
|
825 val fin_supps = map (fn x => @{term "finite :: atom set \<Rightarrow> bool"} $ x) supps |
|
826 in |
|
827 (names, HOLogic.mk_Trueprop (mk_conjl fin_supps)) |
|
828 end |
|
829 *} |
|
830 |
|
831 ML {* |
|
832 fun fs_tac induct supports = rel_indtac induct THEN_ALL_NEW ( |
|
833 rtac @{thm supports_finite} THEN' resolve_tac supports) THEN_ALL_NEW |
|
834 asm_full_simp_tac (HOL_ss addsimps @{thms supp_atom supp_atom_image supp_fset_to_set |
|
835 supp_fmap_atom finite_insert finite.emptyI finite_Un finite_supp}) |
|
836 *} |
|
837 |
|
838 ML {* |
|
839 fun prove_fs ctxt induct supports tys = |
|
840 let |
|
841 val (names, eq) = mk_fs tys |
|
842 in |
|
843 Goal.prove ctxt names [] eq (fn _ => fs_tac induct supports 1) |
|
844 end |
|
845 *} |
|
846 |
|
847 ML {* |
|
848 fun mk_supp x = Const (@{const_name supp}, fastype_of x --> @{typ "atom set"}) $ x; |
|
849 |
|
850 fun mk_supp_neq arg (fv, alpha) = |
|
851 let |
|
852 val collect = Const ("Collect", @{typ "(atom \<Rightarrow> bool) \<Rightarrow> atom \<Rightarrow> bool"}); |
|
853 val ty = fastype_of arg; |
|
854 val perm = Const ("Nominal2_Base.pt_class.permute", @{typ perm} --> ty --> ty); |
|
855 val finite = @{term "finite :: atom set \<Rightarrow> bool"} |
|
856 val rhs = collect $ Abs ("a", @{typ atom}, |
|
857 HOLogic.mk_not (finite $ |
|
858 (collect $ Abs ("b", @{typ atom}, |
|
859 HOLogic.mk_not (alpha $ (perm $ (@{term swap} $ Bound 1 $ Bound 0) $ arg) $ arg))))) |
|
860 in |
|
861 HOLogic.mk_eq (fv $ arg, rhs) |
|
862 end; |
|
863 |
|
864 fun supp_eq fv_alphas_lst = |
|
865 let |
|
866 val (fvs_alphas, ls) = split_list fv_alphas_lst; |
|
867 val (fv_ts, _) = split_list fvs_alphas; |
|
868 val tys = map (domain_type o fastype_of) fv_ts; |
|
869 val names = Datatype_Prop.make_tnames tys; |
|
870 val args = map Free (names ~~ tys); |
|
871 fun supp_eq_arg ((fv, arg), l) = |
|
872 mk_conjl |
|
873 ((HOLogic.mk_eq (fv $ arg, mk_supp arg)) :: |
|
874 (map (mk_supp_neq arg) l)) |
|
875 val eqs = mk_conjl (map supp_eq_arg ((fv_ts ~~ args) ~~ ls)) |
|
876 in |
|
877 (names, HOLogic.mk_Trueprop eqs) |
|
878 end |
|
879 *} |
|
880 |
|
881 ML {* |
|
882 fun combine_fv_alpha_bns (fv_ts_nobn, fv_ts_bn) (alpha_ts_nobn, alpha_ts_bn) bn_nos = |
|
883 if length fv_ts_bn < length alpha_ts_bn then |
|
884 (fv_ts_nobn ~~ alpha_ts_nobn) ~~ (replicate (length fv_ts_nobn) []) |
|
885 else let |
|
886 val fv_alpha_nos = 0 upto (length fv_ts_nobn - 1); |
|
887 fun filter_fn i (x, j) = if j = i then SOME x else NONE; |
|
888 val fv_alpha_bn_nos = (fv_ts_bn ~~ alpha_ts_bn) ~~ bn_nos; |
|
889 val fv_alpha_bn_all = map (fn i => map_filter (filter_fn i) fv_alpha_bn_nos) fv_alpha_nos; |
|
890 in |
|
891 (fv_ts_nobn ~~ alpha_ts_nobn) ~~ fv_alpha_bn_all |
|
892 end |
|
893 *} |
|
894 |
|
895 (* TODO: this is a hack, it assumes that only one type of Abs's is present |
|
896 in the type and chooses this supp_abs. Additionally single atoms are |
|
897 treated properly. *) |
|
898 ML {* |
|
899 fun choose_alpha_abs eqiff = |
|
900 let |
|
901 fun exists_subterms f ts = true mem (map (exists_subterm f) ts); |
|
902 val terms = map prop_of eqiff; |
|
903 fun check cname = exists_subterms (fn x => fst(dest_Const x) = cname handle _ => false) terms |
|
904 val no = |
|
905 if check @{const_name alpha_lst} then 2 else |
|
906 if check @{const_name alpha_res} then 1 else |
|
907 if check @{const_name alpha_gen} then 0 else |
|
908 error "Failure choosing supp_abs" |
|
909 in |
|
910 nth @{thms supp_abs[symmetric]} no |
|
911 end |
|
912 *} |
|
913 lemma supp_abs_atom: "supp (Abs {atom a} (x :: 'a :: fs)) = supp x - {atom a}" |
|
914 by (rule supp_abs(1)) |
|
915 |
|
916 lemma supp_abs_sum: |
|
917 "supp (Abs x (a :: 'a :: fs)) \<union> supp (Abs x (b :: 'b :: fs)) = supp (Abs x (a, b))" |
|
918 "supp (Abs_res x (a :: 'a :: fs)) \<union> supp (Abs_res x (b :: 'b :: fs)) = supp (Abs_res x (a, b))" |
|
919 "supp (Abs_lst y (a :: 'a :: fs)) \<union> supp (Abs_lst y (b :: 'b :: fs)) = supp (Abs_lst y (a, b))" |
|
920 apply (simp_all add: supp_abs supp_Pair) |
|
921 apply blast+ |
|
922 done |
|
923 |
|
924 |
|
925 ML {* |
|
926 fun supp_eq_tac ind fv perm eqiff ctxt = |
|
927 rel_indtac ind THEN_ALL_NEW |
|
928 asm_full_simp_tac (HOL_basic_ss addsimps fv) THEN_ALL_NEW |
|
929 asm_full_simp_tac (HOL_basic_ss addsimps @{thms supp_abs_atom[symmetric]}) THEN_ALL_NEW |
|
930 asm_full_simp_tac (HOL_basic_ss addsimps [choose_alpha_abs eqiff]) THEN_ALL_NEW |
|
931 simp_tac (HOL_basic_ss addsimps @{thms supp_abs_sum}) THEN_ALL_NEW |
|
932 simp_tac (HOL_basic_ss addsimps @{thms supp_def}) THEN_ALL_NEW |
|
933 simp_tac (HOL_basic_ss addsimps (@{thms permute_abs} @ perm)) THEN_ALL_NEW |
|
934 simp_tac (HOL_basic_ss addsimps (@{thms Abs_eq_iff} @ eqiff)) THEN_ALL_NEW |
|
935 simp_tac (HOL_basic_ss addsimps @{thms alphas3 alphas2}) THEN_ALL_NEW |
|
936 simp_tac (HOL_basic_ss addsimps @{thms alphas}) THEN_ALL_NEW |
|
937 asm_full_simp_tac (HOL_basic_ss addsimps (@{thm supp_Pair} :: sym_eqvts ctxt)) THEN_ALL_NEW |
|
938 asm_full_simp_tac (HOL_basic_ss addsimps (@{thm Pair_eq} :: all_eqvts ctxt)) THEN_ALL_NEW |
|
939 simp_tac (HOL_basic_ss addsimps @{thms supp_at_base[symmetric,simplified supp_def]}) THEN_ALL_NEW |
|
940 simp_tac (HOL_basic_ss addsimps @{thms Collect_disj_eq[symmetric]}) THEN_ALL_NEW |
|
941 simp_tac (HOL_basic_ss addsimps @{thms infinite_Un[symmetric]}) THEN_ALL_NEW |
|
942 simp_tac (HOL_basic_ss addsimps @{thms Collect_disj_eq[symmetric]}) THEN_ALL_NEW |
|
943 simp_tac (HOL_basic_ss addsimps @{thms de_Morgan_conj[symmetric]}) THEN_ALL_NEW |
|
944 simp_tac (HOL_basic_ss addsimps @{thms ex_simps(1,2)[symmetric]}) THEN_ALL_NEW |
|
945 simp_tac (HOL_ss addsimps @{thms Collect_const finite.emptyI}) |
|
946 *} |
|
947 |
|
948 |
|
949 |
|
950 ML {* |
|
951 fun build_eqvt_gl pi frees fnctn ctxt = |
|
952 let |
|
953 val typ = domain_type (fastype_of fnctn); |
|
954 val arg = the (AList.lookup (op=) frees typ); |
|
955 in |
|
956 ([HOLogic.mk_eq ((perm_arg (fnctn $ arg) $ pi $ (fnctn $ arg)), (fnctn $ (perm_arg arg $ pi $ arg)))], ctxt) |
|
957 end |
|
958 *} |
|
959 |
|
960 ML {* |
|
961 fun prove_eqvt tys ind simps funs ctxt = |
|
962 let |
|
963 val ([pi], ctxt') = Variable.variant_fixes ["p"] ctxt; |
|
964 val pi = Free (pi, @{typ perm}); |
|
965 val tac = asm_full_simp_tac (HOL_ss addsimps (@{thms atom_eqvt permute_list.simps} @ simps @ all_eqvts ctxt')) |
|
966 val ths_loc = prove_by_induct tys (build_eqvt_gl pi) ind tac funs ctxt' |
|
967 val ths = Variable.export ctxt' ctxt ths_loc |
|
968 val add_eqvt = Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add) |
|
969 in |
|
970 (ths, snd (Local_Theory.note ((Binding.empty, [add_eqvt]), ths) ctxt)) |
|
971 end |
|
972 *} |
|
973 |
|
974 end |
|