196 if a = noatoms then b else |
196 if a = noatoms then b else |
197 if b = noatoms then a else |
197 if b = noatoms then a else |
198 if a = b then a else |
198 if a = b then a else |
199 HOLogic.mk_binop @{const_name sup} (a, b)) (rev sets) noatoms; |
199 HOLogic.mk_binop @{const_name sup} (a, b)) (rev sets) noatoms; |
200 val mk_inter = foldr1 (HOLogic.mk_binop @{const_name inf}) |
200 val mk_inter = foldr1 (HOLogic.mk_binop @{const_name inf}) |
201 fun mk_conjl props = |
|
202 fold (fn a => fn b => |
|
203 if a = @{term True} then b else |
|
204 if b = @{term True} then a else |
|
205 HOLogic.mk_conj (a, b)) (rev props) @{term True}; |
|
206 fun mk_diff a b = |
201 fun mk_diff a b = |
207 if b = noatoms then a else |
202 if b = noatoms then a else |
208 if b = a then noatoms else |
203 if b = a then noatoms else |
209 HOLogic.mk_binop @{const_name minus} (a, b); |
204 HOLogic.mk_binop @{const_name minus} (a, b); |
210 fun mk_atom_set t = |
205 fun mk_atom_set t = |
595 in |
590 in |
596 (((all_fvs, ordered_fvs), alphas), lthy''') |
591 (((all_fvs, ordered_fvs), alphas), lthy''') |
597 end |
592 end |
598 *} |
593 *} |
599 |
594 |
600 (* |
595 |
601 atom_decl name |
|
602 datatype lam = |
|
603 VAR "name" |
|
604 | APP "lam" "lam" |
|
605 | LET "bp" "lam" |
|
606 and bp = |
|
607 BP "name" "lam" |
|
608 primrec |
|
609 bi::"bp \<Rightarrow> atom set" |
|
610 where |
|
611 "bi (BP x t) = {atom x}" |
|
612 setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Fv.lam") 2 *} |
|
613 local_setup {* |
|
614 snd o define_fv_alpha (Datatype.the_info @{theory} "Fv.lam") |
|
615 [[[], [], [(SOME (@{term bi}, true), 0, 1)]], [[]]] [(@{term bi}, 1, [[0]])] *} |
|
616 print_theorems |
|
617 *) |
|
618 |
|
619 (*atom_decl name |
|
620 datatype rtrm1 = |
|
621 rVr1 "name" |
|
622 | rAp1 "rtrm1" "rtrm1" |
|
623 | rLm1 "name" "rtrm1" --"name is bound in trm1" |
|
624 | rLt1 "bp" "rtrm1" "rtrm1" --"all variables in bp are bound in the 2nd trm1" |
|
625 and bp = |
|
626 BUnit |
|
627 | BVr "name" |
|
628 | BPr "bp" "bp" |
|
629 primrec |
|
630 bv1 |
|
631 where |
|
632 "bv1 (BUnit) = {}" |
|
633 | "bv1 (BVr x) = {atom x}" |
|
634 | "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp1)" |
|
635 setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Fv.rtrm1") 2 *} |
|
636 local_setup {* |
|
637 snd o define_fv_alpha (Datatype.the_info @{theory} "Fv.rtrm1") |
|
638 [[[], [], [(NONE, 0, 1)], [(SOME (@{term bv1}, false), 0, 2)]], |
|
639 [[], [], []]] [(@{term bv1}, 1, [[], [0], [0, 1]])] *} |
|
640 print_theorems |
|
641 *) |
|
642 |
|
643 (* |
|
644 atom_decl name |
|
645 datatype rtrm5 = |
|
646 rVr5 "name" |
|
647 | rLt5 "rlts" "rtrm5" --"bind (bv5 lts) in (rtrm5)" |
|
648 and rlts = |
|
649 rLnil |
|
650 | rLcons "name" "rtrm5" "rlts" |
|
651 primrec |
|
652 rbv5 |
|
653 where |
|
654 "rbv5 rLnil = {}" |
|
655 | "rbv5 (rLcons n t ltl) = {atom n} \<union> (rbv5 ltl)" |
|
656 setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Fv.rtrm5") 2 *} |
|
657 local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Fv.rtrm5") |
|
658 [[[], [(SOME (@{term rbv5}, false), 0, 1)]], [[], []]] [(@{term rbv5}, 1, [[], [0, 2]])] *} |
|
659 print_theorems |
|
660 *) |
|
661 |
|
662 ML {* |
|
663 fun alpha_inj_tac dist_inj intrs elims = |
|
664 SOLVED' (asm_full_simp_tac (HOL_ss addsimps intrs)) ORELSE' |
|
665 (rtac @{thm iffI} THEN' RANGE [ |
|
666 (eresolve_tac elims THEN_ALL_NEW |
|
667 asm_full_simp_tac (HOL_ss addsimps dist_inj) |
|
668 ), |
|
669 asm_full_simp_tac (HOL_ss addsimps intrs)]) |
|
670 *} |
|
671 |
|
672 ML {* |
|
673 fun build_alpha_inj_gl thm = |
|
674 let |
|
675 val prop = prop_of thm; |
|
676 val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop); |
|
677 val hyps = map HOLogic.dest_Trueprop (Logic.strip_imp_prems prop); |
|
678 fun list_conj l = foldr1 HOLogic.mk_conj l; |
|
679 in |
|
680 if hyps = [] then concl |
|
681 else HOLogic.mk_eq (concl, list_conj hyps) |
|
682 end; |
|
683 *} |
|
684 |
|
685 ML {* |
|
686 fun build_alpha_inj intrs dist_inj elims ctxt = |
|
687 let |
|
688 val ((_, thms_imp), ctxt') = Variable.import false intrs ctxt; |
|
689 val gls = map (HOLogic.mk_Trueprop o build_alpha_inj_gl) thms_imp; |
|
690 fun tac _ = alpha_inj_tac dist_inj intrs elims 1; |
|
691 val thms = map (fn gl => Goal.prove ctxt' [] [] gl tac) gls; |
|
692 in |
|
693 Variable.export ctxt' ctxt thms |
|
694 end |
|
695 *} |
|
696 |
596 |
697 ML {* |
597 ML {* |
698 fun build_alpha_sym_trans_gl alphas (x, y, z) = |
598 fun build_alpha_sym_trans_gl alphas (x, y, z) = |
699 let |
599 let |
700 fun build_alpha alpha = |
600 fun build_alpha alpha = |
744 |
644 |
745 ML {* |
645 ML {* |
746 fun reflp_tac induct eq_iff ctxt = |
646 fun reflp_tac induct eq_iff ctxt = |
747 rtac induct THEN_ALL_NEW |
647 rtac induct THEN_ALL_NEW |
748 simp_tac ((mk_minimal_ss ctxt) addsimps eq_iff) THEN_ALL_NEW |
648 simp_tac ((mk_minimal_ss ctxt) addsimps eq_iff) THEN_ALL_NEW |
749 split_conjs THEN_ALL_NEW REPEAT o rtac @{thm exI[of _ "0 :: perm"]} |
649 split_conj_tac THEN_ALL_NEW REPEAT o rtac @{thm exI[of _ "0 :: perm"]} |
750 THEN_ALL_NEW split_conjs THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps |
650 THEN_ALL_NEW split_conj_tac THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps |
751 @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv |
651 @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv |
752 add_0_left supp_zero_perm Int_empty_left split_conv}) |
652 add_0_left supp_zero_perm Int_empty_left split_conv}) |
753 *} |
653 *} |
754 |
654 |
755 ML {* |
655 ML {* |
797 apply (rule_tac x="-pi" in exI) |
697 apply (rule_tac x="-pi" in exI) |
798 by auto |
698 by auto |
799 |
699 |
800 ML {* |
700 ML {* |
801 fun symp_tac induct inj eqvt ctxt = |
701 fun symp_tac induct inj eqvt ctxt = |
802 ind_tac induct THEN_ALL_NEW |
702 rel_indtac induct THEN_ALL_NEW |
803 simp_tac ((mk_minimal_ss ctxt) addsimps inj) THEN_ALL_NEW split_conjs |
703 simp_tac ((mk_minimal_ss ctxt) addsimps inj) THEN_ALL_NEW split_conj_tac |
804 THEN_ALL_NEW |
704 THEN_ALL_NEW |
805 REPEAT o etac @{thm exi_neg} |
705 REPEAT o etac @{thm exi_neg} |
806 THEN_ALL_NEW |
706 THEN_ALL_NEW |
807 split_conjs THEN_ALL_NEW |
707 split_conj_tac THEN_ALL_NEW |
808 asm_full_simp_tac (HOL_ss addsimps @{thms supp_minus_perm minus_add[symmetric]}) THEN_ALL_NEW |
708 asm_full_simp_tac (HOL_ss addsimps @{thms supp_minus_perm minus_add[symmetric]}) THEN_ALL_NEW |
809 TRY o (rtac @{thm alpha_gen_compose_sym2} ORELSE' rtac @{thm alpha_gen_compose_sym}) THEN_ALL_NEW |
709 TRY o (rtac @{thm alpha_gen_compose_sym2} ORELSE' rtac @{thm alpha_gen_compose_sym}) THEN_ALL_NEW |
810 (asm_full_simp_tac (HOL_ss addsimps (eqvt @ all_eqvts ctxt))) |
710 (asm_full_simp_tac (HOL_ss addsimps (eqvt @ all_eqvts ctxt))) |
811 *} |
711 *} |
812 |
712 |
862 ) |
762 ) |
863 *} |
763 *} |
864 |
764 |
865 ML {* |
765 ML {* |
866 fun transp_tac ctxt induct alpha_inj term_inj distinct cases eqvt = |
766 fun transp_tac ctxt induct alpha_inj term_inj distinct cases eqvt = |
867 ind_tac induct THEN_ALL_NEW |
767 rel_indtac induct THEN_ALL_NEW |
868 (TRY o rtac allI THEN' imp_elim_tac cases ctxt) THEN_ALL_NEW |
768 (TRY o rtac allI THEN' imp_elim_tac cases ctxt) THEN_ALL_NEW |
869 asm_full_simp_tac ((mk_minimal_ss ctxt) addsimps alpha_inj) THEN_ALL_NEW |
769 asm_full_simp_tac ((mk_minimal_ss ctxt) addsimps alpha_inj) THEN_ALL_NEW |
870 split_conjs THEN_ALL_NEW REPEAT o (eetac @{thm exi_sum} ctxt) THEN_ALL_NEW split_conjs |
770 split_conj_tac THEN_ALL_NEW REPEAT o (eetac @{thm exi_sum} ctxt) THEN_ALL_NEW split_conj_tac |
871 THEN_ALL_NEW (asm_full_simp_tac (HOL_ss addsimps (term_inj @ distinct))) |
771 THEN_ALL_NEW (asm_full_simp_tac (HOL_ss addsimps (term_inj @ distinct))) |
872 THEN_ALL_NEW split_conjs THEN_ALL_NEW |
772 THEN_ALL_NEW split_conj_tac THEN_ALL_NEW |
873 TRY o (etac @{thm alpha_gen_compose_trans2} ORELSE' etac @{thm alpha_gen_compose_trans}) THEN_ALL_NEW |
773 TRY o (etac @{thm alpha_gen_compose_trans2} ORELSE' etac @{thm alpha_gen_compose_trans}) THEN_ALL_NEW |
874 (asm_full_simp_tac (HOL_ss addsimps (all_eqvts ctxt @ eqvt @ term_inj @ distinct))) |
774 (asm_full_simp_tac (HOL_ss addsimps (all_eqvts ctxt @ eqvt @ term_inj @ distinct))) |
875 *} |
775 *} |
876 |
776 |
877 lemma transpI: |
777 lemma transpI: |
953 by auto |
853 by auto |
954 |
854 |
955 ML {* |
855 ML {* |
956 fun supports_tac perm = |
856 fun supports_tac perm = |
957 simp_tac (HOL_ss addsimps @{thms supports_def not_in_union} @ perm) THEN_ALL_NEW ( |
857 simp_tac (HOL_ss addsimps @{thms supports_def not_in_union} @ perm) THEN_ALL_NEW ( |
958 REPEAT o rtac allI THEN' REPEAT o rtac impI THEN' split_conjs THEN' |
858 REPEAT o rtac allI THEN' REPEAT o rtac impI THEN' split_conj_tac THEN' |
959 asm_full_simp_tac (HOL_ss addsimps @{thms fresh_def[symmetric] |
859 asm_full_simp_tac (HOL_ss addsimps @{thms fresh_def[symmetric] |
960 swap_fresh_fresh fresh_atom swap_at_base_simps(3) swap_atom_image_fresh |
860 swap_fresh_fresh fresh_atom swap_at_base_simps(3) swap_atom_image_fresh |
961 supp_fset_to_set supp_fmap_atom})) |
861 supp_fset_to_set supp_fmap_atom})) |
962 *} |
862 *} |
963 |
863 |
1077 apply blast |
977 apply blast |
1078 done |
978 done |
1079 |
979 |
1080 ML {* |
980 ML {* |
1081 fun supp_eq_tac ind fv perm eqiff ctxt = |
981 fun supp_eq_tac ind fv perm eqiff ctxt = |
1082 ind_tac ind THEN_ALL_NEW |
982 rel_indtac ind THEN_ALL_NEW |
1083 asm_full_simp_tac (HOL_basic_ss addsimps fv) THEN_ALL_NEW |
983 asm_full_simp_tac (HOL_basic_ss addsimps fv) THEN_ALL_NEW |
1084 asm_full_simp_tac (HOL_basic_ss addsimps @{thms supp_Abs[symmetric]}) THEN_ALL_NEW |
984 asm_full_simp_tac (HOL_basic_ss addsimps @{thms supp_Abs[symmetric]}) THEN_ALL_NEW |
1085 simp_tac (HOL_basic_ss addsimps @{thms supp_abs_sum}) THEN_ALL_NEW |
985 simp_tac (HOL_basic_ss addsimps @{thms supp_abs_sum}) THEN_ALL_NEW |
1086 simp_tac (HOL_basic_ss addsimps @{thms supp_def}) THEN_ALL_NEW |
986 simp_tac (HOL_basic_ss addsimps @{thms supp_def}) THEN_ALL_NEW |
1087 simp_tac (HOL_basic_ss addsimps (@{thm permute_ABS} :: perm)) THEN_ALL_NEW |
987 simp_tac (HOL_basic_ss addsimps (@{thm permute_ABS} :: perm)) THEN_ALL_NEW |
1097 simp_tac (HOL_basic_ss addsimps @{thms de_Morgan_conj[symmetric]}) THEN_ALL_NEW |
997 simp_tac (HOL_basic_ss addsimps @{thms de_Morgan_conj[symmetric]}) THEN_ALL_NEW |
1098 simp_tac (HOL_basic_ss addsimps @{thms ex_simps(1,2)[symmetric]}) THEN_ALL_NEW |
998 simp_tac (HOL_basic_ss addsimps @{thms ex_simps(1,2)[symmetric]}) THEN_ALL_NEW |
1099 simp_tac (HOL_ss addsimps @{thms Collect_const finite.emptyI}) |
999 simp_tac (HOL_ss addsimps @{thms Collect_const finite.emptyI}) |
1100 *} |
1000 *} |
1101 |
1001 |
1102 (* Given function for buildng a goal for an input, prepares a |
1002 |
1103 one common goals for all the inputs and proves it by induction |
|
1104 together *) |
|
1105 ML {* |
|
1106 fun prove_by_induct tys build_goal ind utac inputs ctxt = |
|
1107 let |
|
1108 val names = Datatype_Prop.make_tnames tys; |
|
1109 val (names', ctxt') = Variable.variant_fixes names ctxt; |
|
1110 val frees = map Free (names' ~~ tys); |
|
1111 val (gls_lists, ctxt'') = fold_map (build_goal (tys ~~ frees)) inputs ctxt'; |
|
1112 val gls = flat gls_lists; |
|
1113 fun trm_gls_map t = filter (exists_subterm (fn s => s = t)) gls; |
|
1114 val trm_gl_lists = map trm_gls_map frees; |
|
1115 val trm_gl_insts = map2 (fn n => fn l => [NONE, if l = [] then NONE else SOME n]) names' trm_gl_lists |
|
1116 val trm_gls = map mk_conjl trm_gl_lists; |
|
1117 val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj trm_gls); |
|
1118 fun tac {context,...} = ((fn _ => print_tac (PolyML.makestring names')) THEN' |
|
1119 InductTacs.induct_rules_tac context [(flat trm_gl_insts)] [ind] |
|
1120 THEN_ALL_NEW split_conjs THEN_ALL_NEW utac) 1 |
|
1121 val th_loc = Goal.prove ctxt'' [] [] gl tac |
|
1122 val ths_loc = HOLogic.conj_elims th_loc |
|
1123 val ths = Variable.export ctxt'' ctxt ths_loc |
|
1124 in |
|
1125 filter (fn x => not (prop_of x = prop_of @{thm TrueI})) ths |
|
1126 end |
|
1127 *} |
|
1128 |
1003 |
1129 ML {* |
1004 ML {* |
1130 fun build_eqvt_gl pi frees fnctn ctxt = |
1005 fun build_eqvt_gl pi frees fnctn ctxt = |
1131 let |
1006 let |
1132 val typ = domain_type (fastype_of fnctn); |
1007 val typ = domain_type (fastype_of fnctn); |
1149 (ths, snd (Local_Theory.note ((Binding.empty, [add_eqvt]), ths) ctxt)) |
1024 (ths, snd (Local_Theory.note ((Binding.empty, [add_eqvt]), ths) ctxt)) |
1150 end |
1025 end |
1151 *} |
1026 *} |
1152 |
1027 |
1153 ML {* |
1028 ML {* |
1154 fun prove_by_alpha_induct alphas build_goal ind utac inputs ctxt = |
|
1155 let |
|
1156 val tys = map (domain_type o fastype_of) alphas; |
|
1157 val names = Datatype_Prop.make_tnames tys; |
|
1158 val (namesl, ctxt') = Variable.variant_fixes names ctxt; |
|
1159 val (namesr, ctxt'') = Variable.variant_fixes names ctxt'; |
|
1160 val freesl = map Free (namesl ~~ tys); |
|
1161 val freesr = map Free (namesr ~~ tys); |
|
1162 val (gls_lists, ctxt'') = fold_map (build_goal (tys ~~ (freesl ~~ freesr))) inputs ctxt''; |
|
1163 val gls = flat gls_lists; |
|
1164 fun trm_gls_map t = filter (exists_subterm (fn s => s = t)) gls; |
|
1165 val trm_gl_lists = map trm_gls_map freesl; |
|
1166 val trm_gls = map mk_conjl trm_gl_lists; |
|
1167 val pgls = map |
|
1168 (fn ((alpha, gl), (l, r)) => HOLogic.mk_imp (alpha $ l $ r, gl)) |
|
1169 ((alphas ~~ trm_gls) ~~ (freesl ~~ freesr)) |
|
1170 val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj pgls); |
|
1171 (* val _ = tracing (PolyML.makestring gl); *) |
|
1172 fun tac {context,...} = (ind_tac ind THEN_ALL_NEW split_conjs THEN_ALL_NEW utac) 1 |
|
1173 val th_loc = Goal.prove ctxt'' [] [] gl tac |
|
1174 val ths_loc = HOLogic.conj_elims th_loc |
|
1175 val ths = Variable.export ctxt'' ctxt ths_loc |
|
1176 in |
|
1177 filter (fn x => not (prop_of x = prop_of @{thm TrueI})) ths |
|
1178 end |
|
1179 *} |
|
1180 |
|
1181 ML {* |
|
1182 fun build_rsp_gl alphas fnctn ctxt = |
1029 fun build_rsp_gl alphas fnctn ctxt = |
1183 let |
1030 let |
1184 val typ = domain_type (fastype_of fnctn); |
1031 val typ = domain_type (fastype_of fnctn); |
1185 val (argl, argr) = the (AList.lookup (op=) alphas typ); |
1032 val (argl, argr) = the (AList.lookup (op=) alphas typ); |
1186 in |
1033 in |