| changeset 3183 | 313e6f2cdd89 |
| parent 3180 | 7b5db6c23753 |
| child 3184 | ae1defecd8c0 |
| 3182:5335c0ea743a | 3183:313e6f2cdd89 |
|---|---|
797 |
797 |
798 method_setup perm_strict_simp = |
798 method_setup perm_strict_simp = |
799 {* Nominal_Permeq.args_parser >> Nominal_Permeq.perm_strict_simp_meth *} |
799 {* Nominal_Permeq.args_parser >> Nominal_Permeq.perm_strict_simp_meth *} |
800 {* pushes permutations inside, raises an error if it cannot solve all permutations. *} |
800 {* pushes permutations inside, raises an error if it cannot solve all permutations. *} |
801 |
801 |
802 simproc_setup perm_simproc ("p \<bullet> t") = {* fn _ => fn ss => fn ctrm => |
|
803 case term_of (Thm.dest_arg ctrm) of |
|
804 Free _ => NONE |
|
805 | Var _ => NONE |
|
806 | Const (@{const_name permute}, _) $ _ $ _ => NONE |
|
807 | _ => |
|
808 let |
|
809 val ctxt = Simplifier.the_context ss |
|
810 val thm = Nominal_Permeq.eqvt_conv ctxt Nominal_Permeq.eqvt_strict_config ctrm |
|
811 handle ERROR _ => Thm.reflexive ctrm |
|
812 in |
|
813 if Thm.is_reflexive thm then NONE else SOME(thm) |
|
814 end |
|
815 *} |
|
816 |
|
802 |
817 |
803 subsubsection {* Equivariance for permutations and swapping *} |
818 subsubsection {* Equivariance for permutations and swapping *} |
804 |
819 |
805 lemma permute_eqvt: |
820 lemma permute_eqvt: |
806 shows "p \<bullet> (q \<bullet> x) = (p \<bullet> q) \<bullet> (p \<bullet> x)" |
821 shows "p \<bullet> (q \<bullet> x) = (p \<bullet> q) \<bullet> (p \<bullet> x)" |
873 by (perm_simp) (rule refl) |
888 by (perm_simp) (rule refl) |
874 |
889 |
875 lemma if_eqvt [eqvt]: |
890 lemma if_eqvt [eqvt]: |
876 shows "p \<bullet> (if b then x else y) = (if p \<bullet> b then p \<bullet> x else p \<bullet> y)" |
891 shows "p \<bullet> (if b then x else y) = (if p \<bullet> b then p \<bullet> x else p \<bullet> y)" |
877 by (simp add: permute_fun_def permute_bool_def) |
892 by (simp add: permute_fun_def permute_bool_def) |
878 |
|
879 lemma Let_eqvt [eqvt]: |
|
880 shows "p \<bullet> Let x y = Let (p \<bullet> x) (p \<bullet> y)" |
|
881 unfolding Let_def permute_fun_app_eq .. |
|
882 |
893 |
883 lemma True_eqvt [eqvt]: |
894 lemma True_eqvt [eqvt]: |
884 shows "p \<bullet> True = True" |
895 shows "p \<bullet> True = True" |
885 unfolding permute_bool_def .. |
896 unfolding permute_bool_def .. |
886 |
897 |
918 |
929 |
919 lemma the_eqvt2: |
930 lemma the_eqvt2: |
920 assumes unique: "\<exists>!x. P x" |
931 assumes unique: "\<exists>!x. P x" |
921 shows "(p \<bullet> (THE x. P x)) = (THE x. p \<bullet> P (- p \<bullet> x))" |
932 shows "(p \<bullet> (THE x. P x)) = (THE x. p \<bullet> P (- p \<bullet> x))" |
922 apply(rule the1_equality [symmetric]) |
933 apply(rule the1_equality [symmetric]) |
923 apply(simp add: ex1_eqvt2[symmetric]) |
934 apply(simp only: ex1_eqvt2[symmetric]) |
924 apply(simp add: permute_bool_def unique) |
935 apply(simp add: permute_bool_def unique) |
925 apply(simp add: permute_bool_def) |
936 apply(simp add: permute_bool_def) |
926 apply(rule theI'[OF unique]) |
937 apply(rule theI'[OF unique]) |
927 done |
938 done |
928 |
939 |
938 unfolding permute_set_eq permute_fun_def |
949 unfolding permute_set_eq permute_fun_def |
939 by (auto simp add: permute_bool_def) |
950 by (auto simp add: permute_bool_def) |
940 |
951 |
941 lemma inter_eqvt [eqvt]: |
952 lemma inter_eqvt [eqvt]: |
942 shows "p \<bullet> (A \<inter> B) = (p \<bullet> A) \<inter> (p \<bullet> B)" |
953 shows "p \<bullet> (A \<inter> B) = (p \<bullet> A) \<inter> (p \<bullet> B)" |
943 unfolding Int_def |
954 unfolding Int_def by simp |
944 by (perm_simp) (rule refl) |
|
945 |
955 |
946 lemma Bex_eqvt [eqvt]: |
956 lemma Bex_eqvt [eqvt]: |
947 shows "p \<bullet> (\<exists>x \<in> S. P x) = (\<exists>x \<in> (p \<bullet> S). (p \<bullet> P) x)" |
957 shows "p \<bullet> (\<exists>x \<in> S. P x) = (\<exists>x \<in> (p \<bullet> S). (p \<bullet> P) x)" |
948 unfolding Bex_def |
958 unfolding Bex_def by simp |
949 by (perm_simp) (rule refl) |
|
950 |
959 |
951 lemma Ball_eqvt [eqvt]: |
960 lemma Ball_eqvt [eqvt]: |
952 shows "p \<bullet> (\<forall>x \<in> S. P x) = (\<forall>x \<in> (p \<bullet> S). (p \<bullet> P) x)" |
961 shows "p \<bullet> (\<forall>x \<in> S. P x) = (\<forall>x \<in> (p \<bullet> S). (p \<bullet> P) x)" |
953 unfolding Ball_def |
962 unfolding Ball_def by simp |
954 by (perm_simp) (rule refl) |
|
955 |
963 |
956 lemma image_eqvt [eqvt]: |
964 lemma image_eqvt [eqvt]: |
957 shows "p \<bullet> (f ` A) = (p \<bullet> f) ` (p \<bullet> A)" |
965 shows "p \<bullet> (f ` A) = (p \<bullet> f) ` (p \<bullet> A)" |
958 unfolding image_def |
966 unfolding image_def by simp |
959 by (perm_simp) (rule refl) |
|
960 |
967 |
961 lemma Image_eqvt [eqvt]: |
968 lemma Image_eqvt [eqvt]: |
962 shows "p \<bullet> (R `` A) = (p \<bullet> R) `` (p \<bullet> A)" |
969 shows "p \<bullet> (R `` A) = (p \<bullet> R) `` (p \<bullet> A)" |
963 unfolding Image_def |
970 unfolding Image_def by simp |
964 by (perm_simp) (rule refl) |
|
965 |
971 |
966 lemma UNIV_eqvt [eqvt]: |
972 lemma UNIV_eqvt [eqvt]: |
967 shows "p \<bullet> UNIV = UNIV" |
973 shows "p \<bullet> UNIV = UNIV" |
968 unfolding UNIV_def |
974 unfolding UNIV_def |
969 by (perm_simp) (rule refl) |
975 by (perm_simp) (rule refl) |
970 |
976 |
971 lemma union_eqvt [eqvt]: |
977 lemma union_eqvt [eqvt]: |
972 shows "p \<bullet> (A \<union> B) = (p \<bullet> A) \<union> (p \<bullet> B)" |
978 shows "p \<bullet> (A \<union> B) = (p \<bullet> A) \<union> (p \<bullet> B)" |
973 unfolding Un_def |
979 unfolding Un_def by simp |
974 by (perm_simp) (rule refl) |
|
975 |
980 |
976 lemma Diff_eqvt [eqvt]: |
981 lemma Diff_eqvt [eqvt]: |
977 fixes A B :: "'a::pt set" |
982 fixes A B :: "'a::pt set" |
978 shows "p \<bullet> (A - B) = (p \<bullet> A) - (p \<bullet> B)" |
983 shows "p \<bullet> (A - B) = (p \<bullet> A) - (p \<bullet> B)" |
979 unfolding set_diff_eq |
984 unfolding set_diff_eq by simp |
980 by (perm_simp) (rule refl) |
|
981 |
985 |
982 lemma Compl_eqvt [eqvt]: |
986 lemma Compl_eqvt [eqvt]: |
983 fixes A :: "'a::pt set" |
987 fixes A :: "'a::pt set" |
984 shows "p \<bullet> (- A) = - (p \<bullet> A)" |
988 shows "p \<bullet> (- A) = - (p \<bullet> A)" |
985 unfolding Compl_eq_Diff_UNIV |
989 unfolding Compl_eq_Diff_UNIV by simp |
986 by (perm_simp) (rule refl) |
|
987 |
990 |
988 lemma subset_eqvt [eqvt]: |
991 lemma subset_eqvt [eqvt]: |
989 shows "p \<bullet> (S \<subseteq> T) \<longleftrightarrow> (p \<bullet> S) \<subseteq> (p \<bullet> T)" |
992 shows "p \<bullet> (S \<subseteq> T) \<longleftrightarrow> (p \<bullet> S) \<subseteq> (p \<bullet> T)" |
990 unfolding subset_eq |
993 unfolding subset_eq by simp |
991 by (perm_simp) (rule refl) |
|
992 |
994 |
993 lemma psubset_eqvt [eqvt]: |
995 lemma psubset_eqvt [eqvt]: |
994 shows "p \<bullet> (S \<subset> T) \<longleftrightarrow> (p \<bullet> S) \<subset> (p \<bullet> T)" |
996 shows "p \<bullet> (S \<subset> T) \<longleftrightarrow> (p \<bullet> S) \<subset> (p \<bullet> T)" |
995 unfolding psubset_eq |
997 unfolding psubset_eq by simp |
996 by (perm_simp) (rule refl) |
|
997 |
998 |
998 lemma vimage_eqvt [eqvt]: |
999 lemma vimage_eqvt [eqvt]: |
999 shows "p \<bullet> (f -` A) = (p \<bullet> f) -` (p \<bullet> A)" |
1000 shows "p \<bullet> (f -` A) = (p \<bullet> f) -` (p \<bullet> A)" |
1000 unfolding vimage_def |
1001 unfolding vimage_def by simp |
1001 by (perm_simp) (rule refl) |
|
1002 |
1002 |
1003 lemma Union_eqvt [eqvt]: |
1003 lemma Union_eqvt [eqvt]: |
1004 shows "p \<bullet> (\<Union> S) = \<Union> (p \<bullet> S)" |
1004 shows "p \<bullet> (\<Union> S) = \<Union> (p \<bullet> S)" |
1005 unfolding Union_eq |
1005 unfolding Union_eq by simp |
1006 by (perm_simp) (rule refl) |
|
1007 |
1006 |
1008 lemma Inter_eqvt [eqvt]: |
1007 lemma Inter_eqvt [eqvt]: |
1009 shows "p \<bullet> (\<Inter> S) = \<Inter> (p \<bullet> S)" |
1008 shows "p \<bullet> (\<Inter> S) = \<Inter> (p \<bullet> S)" |
1010 unfolding Inter_eq |
1009 unfolding Inter_eq by simp |
1011 by (perm_simp) (rule refl) |
1010 |
1011 thm foldr.simps |
|
1012 |
1012 |
1013 lemma foldr_eqvt[eqvt]: |
1013 lemma foldr_eqvt[eqvt]: |
1014 "p \<bullet> foldr a b c = foldr (p \<bullet> a) (p \<bullet> b) (p \<bullet> c)" |
1014 "p \<bullet> foldr f xs = foldr (p \<bullet> f) (p \<bullet> xs)" |
1015 apply (induct b) |
1015 apply(induct xs) |
1016 apply simp_all |
1016 apply(simp_all) |
1017 apply (perm_simp) |
1017 apply(perm_simp exclude: foldr) |
1018 apply simp |
1018 apply(simp) |
1019 done |
1019 done |
1020 |
|
1021 thm eqvts_raw |
|
1022 |
|
1020 |
1023 |
1021 (* FIXME: eqvt attribute *) |
1024 (* FIXME: eqvt attribute *) |
1022 lemma Sigma_eqvt: |
1025 lemma Sigma_eqvt: |
1023 shows "(p \<bullet> (X \<times> Y)) = (p \<bullet> X) \<times> (p \<bullet> Y)" |
1026 shows "(p \<bullet> (X \<times> Y)) = (p \<bullet> X) \<times> (p \<bullet> Y)" |
1024 unfolding Sigma_def |
1027 unfolding Sigma_def |
1088 |
1091 |
1089 lemma lfp_eqvt [eqvt]: |
1092 lemma lfp_eqvt [eqvt]: |
1090 fixes F::"('a \<Rightarrow> 'b) \<Rightarrow> ('a::pt \<Rightarrow> 'b::{inf_eqvt, le_eqvt})" |
1093 fixes F::"('a \<Rightarrow> 'b) \<Rightarrow> ('a::pt \<Rightarrow> 'b::{inf_eqvt, le_eqvt})" |
1091 shows "p \<bullet> (lfp F) = lfp (p \<bullet> F)" |
1094 shows "p \<bullet> (lfp F) = lfp (p \<bullet> F)" |
1092 unfolding lfp_def |
1095 unfolding lfp_def |
1093 by (perm_simp) (rule refl) |
1096 by simp |
1094 |
1097 |
1095 lemma finite_eqvt [eqvt]: |
1098 lemma finite_eqvt [eqvt]: |
1096 shows "p \<bullet> finite A = finite (p \<bullet> A)" |
1099 shows "p \<bullet> finite A = finite (p \<bullet> A)" |
1097 unfolding finite_def |
1100 unfolding finite_def |
1098 by (perm_simp) (rule refl) |
1101 by simp |
1099 |
1102 |
1100 |
1103 |
1101 subsubsection {* Equivariance for product operations *} |
1104 subsubsection {* Equivariance for product operations *} |
1102 |
1105 |
1103 lemma fst_eqvt [eqvt]: |
1106 lemma fst_eqvt [eqvt]: |
1109 by (cases x) simp |
1112 by (cases x) simp |
1110 |
1113 |
1111 lemma split_eqvt [eqvt]: |
1114 lemma split_eqvt [eqvt]: |
1112 shows "p \<bullet> (split P x) = split (p \<bullet> P) (p \<bullet> x)" |
1115 shows "p \<bullet> (split P x) = split (p \<bullet> P) (p \<bullet> x)" |
1113 unfolding split_def |
1116 unfolding split_def |
1114 by (perm_simp) (rule refl) |
1117 by simp |
1115 |
1118 |
1116 |
1119 |
1117 subsubsection {* Equivariance for list operations *} |
1120 subsubsection {* Equivariance for list operations *} |
1118 |
1121 |
1119 lemma append_eqvt [eqvt]: |
1122 lemma append_eqvt [eqvt]: |
1124 shows "p \<bullet> (rev xs) = rev (p \<bullet> xs)" |
1127 shows "p \<bullet> (rev xs) = rev (p \<bullet> xs)" |
1125 by (induct xs) (simp_all add: append_eqvt) |
1128 by (induct xs) (simp_all add: append_eqvt) |
1126 |
1129 |
1127 lemma map_eqvt [eqvt]: |
1130 lemma map_eqvt [eqvt]: |
1128 shows "p \<bullet> (map f xs) = map (p \<bullet> f) (p \<bullet> xs)" |
1131 shows "p \<bullet> (map f xs) = map (p \<bullet> f) (p \<bullet> xs)" |
1129 by (induct xs) (simp_all, simp only: permute_fun_app_eq) |
1132 by (induct xs) (simp_all) |
1130 |
1133 |
1131 lemma removeAll_eqvt [eqvt]: |
1134 lemma removeAll_eqvt [eqvt]: |
1132 shows "p \<bullet> (removeAll x xs) = removeAll (p \<bullet> x) (p \<bullet> xs)" |
1135 shows "p \<bullet> (removeAll x xs) = removeAll (p \<bullet> x) (p \<bullet> xs)" |
1133 by (induct xs) (auto) |
1136 by (induct xs) (auto) |
1134 |
1137 |
1154 |
1157 |
1155 subsubsection {* Equivariance for @{typ "'a option"} *} |
1158 subsubsection {* Equivariance for @{typ "'a option"} *} |
1156 |
1159 |
1157 lemma option_map_eqvt[eqvt]: |
1160 lemma option_map_eqvt[eqvt]: |
1158 shows "p \<bullet> (Option.map f x) = Option.map (p \<bullet> f) (p \<bullet> x)" |
1161 shows "p \<bullet> (Option.map f x) = Option.map (p \<bullet> f) (p \<bullet> x)" |
1159 by (cases x) (simp_all, simp add: permute_fun_app_eq) |
1162 by (cases x) (simp_all) |
1160 |
1163 |
1161 |
1164 |
1162 subsubsection {* Equivariance for @{typ "'a fset"} *} |
1165 subsubsection {* Equivariance for @{typ "'a fset"} *} |
1163 |
1166 |
1164 lemma in_fset_eqvt [eqvt]: |
1167 lemma in_fset_eqvt [eqvt]: |
1165 shows "(p \<bullet> (x |\<in>| S)) = ((p \<bullet> x) |\<in>| (p \<bullet> S))" |
1168 shows "(p \<bullet> (x |\<in>| S)) = ((p \<bullet> x) |\<in>| (p \<bullet> S))" |
1166 unfolding in_fset |
1169 unfolding in_fset by simp |
1167 by (perm_simp) (simp) |
|
1168 |
1170 |
1169 lemma union_fset_eqvt [eqvt]: |
1171 lemma union_fset_eqvt [eqvt]: |
1170 shows "(p \<bullet> (S |\<union>| T)) = ((p \<bullet> S) |\<union>| (p \<bullet> T))" |
1172 shows "(p \<bullet> (S |\<union>| T)) = ((p \<bullet> S) |\<union>| (p \<bullet> T))" |
1171 by (induct S) (simp_all) |
1173 by (induct S) (simp_all) |
1172 |
1174 |
1173 lemma inter_fset_eqvt [eqvt]: |
1175 lemma inter_fset_eqvt [eqvt]: |
1174 shows "(p \<bullet> (S |\<inter>| T)) = ((p \<bullet> S) |\<inter>| (p \<bullet> T))" |
1176 shows "(p \<bullet> (S |\<inter>| T)) = ((p \<bullet> S) |\<inter>| (p \<bullet> T))" |
1175 apply(descending) |
1177 apply(descending) |
1176 unfolding list_eq_def inter_list_def |
1178 unfolding list_eq_def inter_list_def |
1177 apply(perm_simp) |
|
1178 apply(simp) |
1179 apply(simp) |
1179 done |
1180 done |
1180 |
1181 |
1181 lemma subset_fset_eqvt [eqvt]: |
1182 lemma subset_fset_eqvt [eqvt]: |
1182 shows "(p \<bullet> (S |\<subseteq>| T)) = ((p \<bullet> S) |\<subseteq>| (p \<bullet> T))" |
1183 shows "(p \<bullet> (S |\<subseteq>| T)) = ((p \<bullet> S) |\<subseteq>| (p \<bullet> T))" |
1183 apply(descending) |
1184 apply(descending) |
1184 unfolding sub_list_def |
1185 unfolding sub_list_def |
1185 apply(perm_simp) |
|
1186 apply(simp) |
1186 apply(simp) |
1187 done |
1187 done |
1188 |
1188 |
1189 lemma map_fset_eqvt [eqvt]: |
1189 lemma map_fset_eqvt [eqvt]: |
1190 shows "p \<bullet> (map_fset f S) = map_fset (p \<bullet> f) (p \<bullet> S)" |
1190 shows "p \<bullet> (map_fset f S) = map_fset (p \<bullet> f) (p \<bullet> S)" |
1252 subsection {* supp and fresh are equivariant *} |
1252 subsection {* supp and fresh are equivariant *} |
1253 |
1253 |
1254 |
1254 |
1255 lemma supp_eqvt [eqvt]: |
1255 lemma supp_eqvt [eqvt]: |
1256 shows "p \<bullet> (supp x) = supp (p \<bullet> x)" |
1256 shows "p \<bullet> (supp x) = supp (p \<bullet> x)" |
1257 unfolding supp_def |
1257 unfolding supp_def by simp |
1258 by (perm_simp) |
|
1259 (simp only: permute_eqvt[symmetric]) |
|
1260 |
1258 |
1261 lemma fresh_eqvt [eqvt]: |
1259 lemma fresh_eqvt [eqvt]: |
1262 shows "p \<bullet> (a \<sharp> x) = (p \<bullet> a) \<sharp> (p \<bullet> x)" |
1260 shows "p \<bullet> (a \<sharp> x) = (p \<bullet> a) \<sharp> (p \<bullet> x)" |
1263 unfolding fresh_def |
1261 unfolding fresh_def by simp |
1264 by (perm_simp) (rule refl) |
|
1265 |
1262 |
1266 lemma fresh_permute_iff: |
1263 lemma fresh_permute_iff: |
1267 shows "(p \<bullet> a) \<sharp> (p \<bullet> x) \<longleftrightarrow> a \<sharp> x" |
1264 shows "(p \<bullet> a) \<sharp> (p \<bullet> x) \<longleftrightarrow> a \<sharp> x" |
1268 by (simp only: fresh_eqvt[symmetric] permute_bool_def) |
1265 by (simp only: fresh_eqvt[symmetric] permute_bool_def) |
1269 |
1266 |
1749 { fix p::"perm" |
1746 { fix p::"perm" |
1750 have "p \<bullet> (f (q \<bullet> x)) = p \<bullet> q \<bullet> (f x)" |
1747 have "p \<bullet> (f (q \<bullet> x)) = p \<bullet> q \<bullet> (f x)" |
1751 using assms by (simp add: eqvt_at_def) |
1748 using assms by (simp add: eqvt_at_def) |
1752 also have "\<dots> = (p + q) \<bullet> (f x)" by simp |
1749 also have "\<dots> = (p + q) \<bullet> (f x)" by simp |
1753 also have "\<dots> = f ((p + q) \<bullet> x)" |
1750 also have "\<dots> = f ((p + q) \<bullet> x)" |
1754 using assms by (simp add: eqvt_at_def) |
1751 using assms by (simp only: eqvt_at_def) |
1755 finally have "p \<bullet> (f (q \<bullet> x)) = f (p \<bullet> q \<bullet> x)" by simp } |
1752 finally have "p \<bullet> (f (q \<bullet> x)) = f (p \<bullet> q \<bullet> x)" by simp } |
1756 then show "eqvt_at f (q \<bullet> x)" unfolding eqvt_at_def |
1753 then show "eqvt_at f (q \<bullet> x)" unfolding eqvt_at_def |
1757 by simp |
1754 by simp |
1758 qed |
1755 qed |
1759 |
1756 |
1976 fixes S::"('a::fs set)" |
1973 fixes S::"('a::fs set)" |
1977 assumes fin: "finite S" |
1974 assumes fin: "finite S" |
1978 shows "(\<Union>x\<in>S. supp x) \<subseteq> supp S" |
1975 shows "(\<Union>x\<in>S. supp x) \<subseteq> supp S" |
1979 proof - |
1976 proof - |
1980 have eqvt: "eqvt (\<lambda>S. \<Union> supp ` S)" |
1977 have eqvt: "eqvt (\<lambda>S. \<Union> supp ` S)" |
1981 unfolding eqvt_def |
1978 unfolding eqvt_def |
1982 by (perm_simp) (simp) |
1979 by (perm_simp) (simp) |
1983 have "(\<Union>x\<in>S. supp x) = supp (\<Union>x\<in>S. supp x)" |
1980 have "(\<Union>x\<in>S. supp x) = supp (\<Union>x\<in>S. supp x)" |
1984 by (rule supp_finite_atom_set[symmetric]) (rule Union_of_finite_supp_sets[OF fin]) |
1981 by (rule supp_finite_atom_set[symmetric]) (rule Union_of_finite_supp_sets[OF fin]) |
1985 also have "\<dots> = supp ((\<lambda>S. \<Union> supp ` S) S)" by simp |
1982 also have "\<dots> = supp ((\<lambda>S. \<Union> supp ` S) S)" by simp |
1986 also have "\<dots> \<subseteq> supp S" using eqvt |
1983 also have "\<dots> \<subseteq> supp S" using eqvt |
2332 unfolding fresh_star_def |
2329 unfolding fresh_star_def |
2333 by (metis mem_permute_iff permute_minus_cancel(1) fresh_permute_iff) |
2330 by (metis mem_permute_iff permute_minus_cancel(1) fresh_permute_iff) |
2334 |
2331 |
2335 lemma fresh_star_eqvt [eqvt]: |
2332 lemma fresh_star_eqvt [eqvt]: |
2336 shows "p \<bullet> (as \<sharp>* x) \<longleftrightarrow> (p \<bullet> as) \<sharp>* (p \<bullet> x)" |
2333 shows "p \<bullet> (as \<sharp>* x) \<longleftrightarrow> (p \<bullet> as) \<sharp>* (p \<bullet> x)" |
2337 unfolding fresh_star_def |
2334 unfolding fresh_star_def by simp |
2338 by (perm_simp) (rule refl) |
|
2339 |
|
2340 |
2335 |
2341 |
2336 |
2342 section {* Induction principle for permutations *} |
2337 section {* Induction principle for permutations *} |
2343 |
2338 |
2344 lemma smaller_supp: |
2339 lemma smaller_supp: |
2707 apply(auto)[1] |
2702 apply(auto)[1] |
2708 apply(subgoal_tac "q \<bullet> a \<in> {a. q \<bullet> a \<noteq> a}") |
2703 apply(subgoal_tac "q \<bullet> a \<in> {a. q \<bullet> a \<noteq> a}") |
2709 apply(blast) |
2704 apply(blast) |
2710 apply(simp) |
2705 apply(simp) |
2711 done |
2706 done |
2712 then have "supp (q \<bullet> a \<rightleftharpoons> p \<bullet> a) \<subseteq> insert a bs \<union> p \<bullet> insert a bs" by (simp add: supp_swap) |
2707 then have "supp (q \<bullet> a \<rightleftharpoons> p \<bullet> a) \<subseteq> insert a bs \<union> p \<bullet> insert a bs" |
2708 unfolding supp_swap by auto |
|
2713 moreover |
2709 moreover |
2714 have "supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs" |
2710 have "supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs" |
2715 using ** by (auto simp add: insert_eqvt) |
2711 using ** by (auto simp add: insert_eqvt) |
2716 ultimately |
2712 ultimately |
2717 have "supp q' \<subseteq> insert a bs \<union> p \<bullet> insert a bs" |
2713 have "supp q' \<subseteq> insert a bs \<union> p \<bullet> insert a bs" |
2775 apply(auto)[1] |
2771 apply(auto)[1] |
2776 apply(subgoal_tac "q \<bullet> a \<in> {a. q \<bullet> a \<noteq> a}") |
2772 apply(subgoal_tac "q \<bullet> a \<in> {a. q \<bullet> a \<noteq> a}") |
2777 apply(blast) |
2773 apply(blast) |
2778 apply(simp) |
2774 apply(simp) |
2779 done |
2775 done |
2780 then have "supp (q \<bullet> a \<rightleftharpoons> p \<bullet> a) \<subseteq> set (a # bs) \<union> p \<bullet> set (a # bs)" by (simp add: supp_swap) |
2776 then have "supp (q \<bullet> a \<rightleftharpoons> p \<bullet> a) \<subseteq> set (a # bs) \<union> p \<bullet> set (a # bs)" |
2777 unfolding supp_swap by auto |
|
2781 moreover |
2778 moreover |
2782 have "supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" |
2779 have "supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" |
2783 using ** by (auto simp add: insert_eqvt) |
2780 using ** by (auto simp add: insert_eqvt) |
2784 ultimately |
2781 ultimately |
2785 have "supp q' \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" |
2782 have "supp q' \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" |
2959 |
2956 |
2960 lemma fresh_at_base_permute_iff [simp]: |
2957 lemma fresh_at_base_permute_iff [simp]: |
2961 fixes a::"'a::at_base" |
2958 fixes a::"'a::at_base" |
2962 shows "atom (p \<bullet> a) \<sharp> p \<bullet> x \<longleftrightarrow> atom a \<sharp> x" |
2959 shows "atom (p \<bullet> a) \<sharp> p \<bullet> x \<longleftrightarrow> atom a \<sharp> x" |
2963 unfolding atom_eqvt[symmetric] |
2960 unfolding atom_eqvt[symmetric] |
2964 by (simp add: fresh_permute_iff) |
2961 by (simp only: fresh_permute_iff) |
2965 |
2962 |
2966 |
2963 |
2967 section {* Infrastructure for concrete atom types *} |
2964 section {* Infrastructure for concrete atom types *} |
2968 |
2965 |
2969 definition |
2966 definition |