28 definition permutes (infixr "permutes" 41) |
28 definition permutes (infixr "permutes" 41) |
29 where "(p permutes S) \<longleftrightarrow> (\<forall>x. x \<notin> S \<longrightarrow> p x = x) \<and> (\<forall>y. \<exists>!x. p x = y)" |
29 where "(p permutes S) \<longleftrightarrow> (\<forall>x. x \<notin> S \<longrightarrow> p x = x) \<and> (\<forall>y. \<exists>!x. p x = y)" |
30 |
30 |
31 lemma permutes_in_image: "p permutes S \<Longrightarrow> p x \<in> S \<longleftrightarrow> x \<in> S" |
31 lemma permutes_in_image: "p permutes S \<Longrightarrow> p x \<in> S \<longleftrightarrow> x \<in> S" |
32 unfolding permutes_def by metis |
32 unfolding permutes_def by metis |
|
33 |
|
34 lemma permutes_not_in: |
|
35 assumes "f permutes S" "x \<notin> S" shows "f x = x" |
|
36 using assms by (auto simp: permutes_def) |
33 |
37 |
34 lemma permutes_image: "p permutes S \<Longrightarrow> p ` S = S" |
38 lemma permutes_image: "p permutes S \<Longrightarrow> p ` S = S" |
35 unfolding permutes_def |
39 unfolding permutes_def |
36 apply (rule set_eqI) |
40 apply (rule set_eqI) |
37 apply (simp add: image_iff) |
41 apply (simp add: image_iff) |
38 apply metis |
42 apply metis |
39 done |
43 done |
40 |
44 |
41 lemma permutes_inj: "p permutes S \<Longrightarrow> inj p" |
45 lemma permutes_inj: "p permutes S \<Longrightarrow> inj p" |
42 unfolding permutes_def inj_on_def by blast |
46 unfolding permutes_def inj_on_def by blast |
|
47 |
|
48 lemma permutes_inj_on: "f permutes S \<Longrightarrow> inj_on f A" |
|
49 unfolding permutes_def inj_on_def by auto |
43 |
50 |
44 lemma permutes_surj: "p permutes s \<Longrightarrow> surj p" |
51 lemma permutes_surj: "p permutes s \<Longrightarrow> surj p" |
45 unfolding permutes_def surj_def by metis |
52 unfolding permutes_def surj_def by metis |
46 |
53 |
47 lemma permutes_bij: "p permutes s \<Longrightarrow> bij p" |
54 lemma permutes_bij: "p permutes s \<Longrightarrow> bij p" |
811 by (simp add: sign_def evenperm_swap) |
837 by (simp add: sign_def evenperm_swap) |
812 |
838 |
813 lemma sign_idempotent: "sign p * sign p = 1" |
839 lemma sign_idempotent: "sign p * sign p = 1" |
814 by (simp add: sign_def) |
840 by (simp add: sign_def) |
815 |
841 |
|
842 |
|
843 subsection \<open>Permuting a list\<close> |
|
844 |
|
845 text \<open>This function permutes a list by applying a permutation to the indices.\<close> |
|
846 |
|
847 definition permute_list :: "(nat \<Rightarrow> nat) \<Rightarrow> 'a list \<Rightarrow> 'a list" where |
|
848 "permute_list f xs = map (\<lambda>i. xs ! (f i)) [0..<length xs]" |
|
849 |
|
850 lemma permute_list_map: |
|
851 assumes "f permutes {..<length xs}" |
|
852 shows "permute_list f (map g xs) = map g (permute_list f xs)" |
|
853 using permutes_in_image[OF assms] by (auto simp: permute_list_def) |
|
854 |
|
855 lemma permute_list_nth: |
|
856 assumes "f permutes {..<length xs}" "i < length xs" |
|
857 shows "permute_list f xs ! i = xs ! f i" |
|
858 using permutes_in_image[OF assms(1)] assms(2) |
|
859 by (simp add: permute_list_def) |
|
860 |
|
861 lemma permute_list_Nil [simp]: "permute_list f [] = []" |
|
862 by (simp add: permute_list_def) |
|
863 |
|
864 lemma length_permute_list [simp]: "length (permute_list f xs) = length xs" |
|
865 by (simp add: permute_list_def) |
|
866 |
|
867 lemma permute_list_compose: |
|
868 assumes "g permutes {..<length xs}" |
|
869 shows "permute_list (f \<circ> g) xs = permute_list g (permute_list f xs)" |
|
870 using assms[THEN permutes_in_image] by (auto simp add: permute_list_def) |
|
871 |
|
872 lemma permute_list_ident [simp]: "permute_list (\<lambda>x. x) xs = xs" |
|
873 by (simp add: permute_list_def map_nth) |
|
874 |
|
875 lemma permute_list_id [simp]: "permute_list id xs = xs" |
|
876 by (simp add: id_def) |
|
877 |
|
878 lemma mset_permute_list [simp]: |
|
879 assumes "f permutes {..<length (xs :: 'a list)}" |
|
880 shows "mset (permute_list f xs) = mset xs" |
|
881 proof (rule multiset_eqI) |
|
882 fix y :: 'a |
|
883 from assms have [simp]: "f x < length xs \<longleftrightarrow> x < length xs" for x |
|
884 using permutes_in_image[OF assms] by auto |
|
885 have "count (mset (permute_list f xs)) y = |
|
886 card ((\<lambda>i. xs ! f i) -` {y} \<inter> {..<length xs})" |
|
887 by (simp add: permute_list_def mset_map count_image_mset atLeast0LessThan) |
|
888 also have "(\<lambda>i. xs ! f i) -` {y} \<inter> {..<length xs} = f -` {i. i < length xs \<and> y = xs ! i}" |
|
889 by auto |
|
890 also from assms have "card \<dots> = card {i. i < length xs \<and> y = xs ! i}" |
|
891 by (intro card_vimage_inj) (auto simp: permutes_inj permutes_surj) |
|
892 also have "\<dots> = count (mset xs) y" by (simp add: count_mset length_filter_conv_card) |
|
893 finally show "count (mset (permute_list f xs)) y = count (mset xs) y" by simp |
|
894 qed |
|
895 |
|
896 lemma set_permute_list [simp]: |
|
897 assumes "f permutes {..<length xs}" |
|
898 shows "set (permute_list f xs) = set xs" |
|
899 by (rule mset_eq_setD[OF mset_permute_list]) fact |
|
900 |
|
901 lemma distinct_permute_list [simp]: |
|
902 assumes "f permutes {..<length xs}" |
|
903 shows "distinct (permute_list f xs) = distinct xs" |
|
904 by (simp add: distinct_count_atmost_1 assms) |
|
905 |
|
906 lemma permute_list_zip: |
|
907 assumes "f permutes A" "A = {..<length xs}" |
|
908 assumes [simp]: "length xs = length ys" |
|
909 shows "permute_list f (zip xs ys) = zip (permute_list f xs) (permute_list f ys)" |
|
910 proof - |
|
911 from permutes_in_image[OF assms(1)] assms(2) |
|
912 have [simp]: "f i < length ys \<longleftrightarrow> i < length ys" for i by simp |
|
913 have "permute_list f (zip xs ys) = map (\<lambda>i. zip xs ys ! f i) [0..<length ys]" |
|
914 by (simp_all add: permute_list_def zip_map_map) |
|
915 also have "\<dots> = map (\<lambda>(x, y). (xs ! f x, ys ! f y)) (zip [0..<length ys] [0..<length ys])" |
|
916 by (intro nth_equalityI) simp_all |
|
917 also have "\<dots> = zip (permute_list f xs) (permute_list f ys)" |
|
918 by (simp_all add: permute_list_def zip_map_map) |
|
919 finally show ?thesis . |
|
920 qed |
|
921 |
|
922 lemma map_of_permute: |
|
923 assumes "\<sigma> permutes fst ` set xs" |
|
924 shows "map_of xs \<circ> \<sigma> = map_of (map (\<lambda>(x,y). (inv \<sigma> x, y)) xs)" (is "_ = map_of (map ?f _)") |
|
925 proof |
|
926 fix x |
|
927 from assms have "inj \<sigma>" "surj \<sigma>" by (simp_all add: permutes_inj permutes_surj) |
|
928 thus "(map_of xs \<circ> \<sigma>) x = map_of (map ?f xs) x" |
|
929 by (induction xs) (auto simp: inv_f_f surj_f_inv_f) |
|
930 qed |
|
931 |
816 |
932 |
817 subsection \<open>More lemmas about permutations\<close> |
933 subsection \<open>More lemmas about permutations\<close> |
|
934 |
|
935 text \<open> |
|
936 If two lists correspond to the same multiset, there exists a permutation |
|
937 on the list indices that maps one to the other. |
|
938 \<close> |
|
939 lemma mset_eq_permutation: |
|
940 assumes mset_eq: "mset (xs::'a list) = mset ys" |
|
941 defines [simp]: "n \<equiv> length xs" |
|
942 obtains f where "f permutes {..<length ys}" "permute_list f ys = xs" |
|
943 proof - |
|
944 from mset_eq have [simp]: "length xs = length ys" |
|
945 by (rule mset_eq_length) |
|
946 def indices_of \<equiv> "\<lambda>(x::'a) xs. {i. i < length xs \<and> x = xs ! i}" |
|
947 have indices_of_subset: "indices_of x xs \<subseteq> {..<length xs}" for x xs |
|
948 unfolding indices_of_def by blast |
|
949 have [simp]: "finite (indices_of x xs)" for x xs |
|
950 by (rule finite_subset[OF indices_of_subset]) simp_all |
|
951 |
|
952 have "\<forall>x\<in>set xs. \<exists>f. bij_betw f (indices_of x xs) (indices_of x ys)" |
|
953 proof |
|
954 fix x |
|
955 from mset_eq have "count (mset xs) x = count (mset ys) x" by simp |
|
956 hence "card (indices_of x xs) = card (indices_of x ys)" |
|
957 by (simp add: count_mset length_filter_conv_card indices_of_def) |
|
958 thus "\<exists>f. bij_betw f (indices_of x xs) (indices_of x ys)" |
|
959 by (intro finite_same_card_bij) simp_all |
|
960 qed |
|
961 hence "\<exists>f. \<forall>x\<in>set xs. bij_betw (f x) (indices_of x xs) (indices_of x ys)" |
|
962 by (rule bchoice) |
|
963 then guess f .. note f = this |
|
964 def g \<equiv> "\<lambda>i. if i < n then f (xs ! i) i else i" |
|
965 |
|
966 have bij_f: "bij_betw (\<lambda>i. f (xs ! i) i) (indices_of x xs) (indices_of x ys)" |
|
967 if x: "x \<in> set xs" for x |
|
968 proof (subst bij_betw_cong) |
|
969 from f x show "bij_betw (f x) (indices_of x xs) (indices_of x ys)" by blast |
|
970 fix i assume "i \<in> indices_of x xs" |
|
971 thus "f (xs ! i) i = f x i" by (simp add: indices_of_def) |
|
972 qed |
|
973 |
|
974 hence "bij_betw (\<lambda>i. f (xs ! i) i) (\<Union>x\<in>set xs. indices_of x xs) (\<Union>x\<in>set xs. indices_of x ys)" |
|
975 by (intro bij_betw_UNION_disjoint) (auto simp add: disjoint_family_on_def indices_of_def) |
|
976 also have "(\<Union>x\<in>set xs. indices_of x xs) = {..<n}" by (auto simp: indices_of_def) |
|
977 also from mset_eq have "set xs = set ys" by (rule mset_eq_setD) |
|
978 also have "(\<Union>x\<in>set ys. indices_of x ys) = {..<n}" |
|
979 by (auto simp: indices_of_def set_conv_nth) |
|
980 also have "bij_betw (\<lambda>i. f (xs ! i) i) {..<n} {..<n} \<longleftrightarrow> bij_betw g {..<n} {..<n}" |
|
981 by (intro bij_betw_cong) (simp_all add: g_def) |
|
982 finally have "g permutes {..<length ys}" |
|
983 by (intro bij_imp_permutes refl) (simp_all add: g_def) |
|
984 |
|
985 moreover have "permute_list g ys = xs" |
|
986 proof (rule sym, intro nth_equalityI allI impI) |
|
987 fix i assume i: "i < length xs" |
|
988 from i have "permute_list g ys ! i = ys ! f (xs ! i) i" |
|
989 by (simp add: permute_list_def g_def) |
|
990 also from i have "i \<in> indices_of (xs ! i) xs" by (simp add: indices_of_def) |
|
991 with bij_f[of "xs ! i"] i have "f (xs ! i) i \<in> indices_of (xs ! i) ys" |
|
992 by (auto simp: bij_betw_def) |
|
993 hence "ys ! f (xs ! i) i = xs ! i" by (simp add: indices_of_def) |
|
994 finally show "xs ! i = permute_list g ys ! i" .. |
|
995 qed simp_all |
|
996 |
|
997 ultimately show ?thesis by (rule that) |
|
998 qed |
818 |
999 |
819 lemma permutes_natset_le: |
1000 lemma permutes_natset_le: |
820 fixes S :: "'a::wellorder set" |
1001 fixes S :: "'a::wellorder set" |
821 assumes p: "p permutes S" |
1002 assumes p: "p permutes S" |
822 and le: "\<forall>i \<in> S. p i \<le> i" |
1003 and le: "\<forall>i \<in> S. p i \<le> i" |
1045 then show "inj_on ?f (insert a S \<times> ?P)" |
1226 then show "inj_on ?f (insert a S \<times> ?P)" |
1046 unfolding inj_on_def by clarify metis |
1227 unfolding inj_on_def by clarify metis |
1047 qed |
1228 qed |
1048 qed |
1229 qed |
1049 |
1230 |
|
1231 |
|
1232 subsection \<open>Constructing permutations from association lists\<close> |
|
1233 |
|
1234 definition list_permutes where |
|
1235 "list_permutes xs A \<longleftrightarrow> set (map fst xs) \<subseteq> A \<and> set (map snd xs) = set (map fst xs) \<and> |
|
1236 distinct (map fst xs) \<and> distinct (map snd xs)" |
|
1237 |
|
1238 lemma list_permutesI [simp]: |
|
1239 assumes "set (map fst xs) \<subseteq> A" "set (map snd xs) = set (map fst xs)" "distinct (map fst xs)" |
|
1240 shows "list_permutes xs A" |
|
1241 proof - |
|
1242 from assms(2,3) have "distinct (map snd xs)" |
|
1243 by (intro card_distinct) (simp_all add: distinct_card del: set_map) |
|
1244 with assms show ?thesis by (simp add: list_permutes_def) |
|
1245 qed |
|
1246 |
|
1247 definition permutation_of_list where |
|
1248 "permutation_of_list xs x = (case map_of xs x of None \<Rightarrow> x | Some y \<Rightarrow> y)" |
|
1249 |
|
1250 lemma permutation_of_list_Cons: |
|
1251 "permutation_of_list ((x,y) # xs) x' = (if x = x' then y else permutation_of_list xs x')" |
|
1252 by (simp add: permutation_of_list_def) |
|
1253 |
|
1254 fun inverse_permutation_of_list where |
|
1255 "inverse_permutation_of_list [] x = x" |
|
1256 | "inverse_permutation_of_list ((y,x')#xs) x = |
|
1257 (if x = x' then y else inverse_permutation_of_list xs x)" |
|
1258 |
|
1259 declare inverse_permutation_of_list.simps [simp del] |
|
1260 |
|
1261 lemma inj_on_map_of: |
|
1262 assumes "distinct (map snd xs)" |
|
1263 shows "inj_on (map_of xs) (set (map fst xs))" |
|
1264 proof (rule inj_onI) |
|
1265 fix x y assume xy: "x \<in> set (map fst xs)" "y \<in> set (map fst xs)" |
|
1266 assume eq: "map_of xs x = map_of xs y" |
|
1267 from xy obtain x' y' |
|
1268 where x'y': "map_of xs x = Some x'" "map_of xs y = Some y'" |
|
1269 by (cases "map_of xs x"; cases "map_of xs y") |
|
1270 (simp_all add: map_of_eq_None_iff) |
|
1271 moreover from this x'y' have "(x,x') \<in> set xs" "(y,y') \<in> set xs" |
|
1272 by (force dest: map_of_SomeD)+ |
|
1273 moreover from this eq x'y' have "x' = y'" by simp |
|
1274 ultimately show "x = y" using assms |
|
1275 by (force simp: distinct_map dest: inj_onD[of _ _ "(x,x')" "(y,y')"]) |
|
1276 qed |
|
1277 |
|
1278 lemma inj_on_the: "None \<notin> A \<Longrightarrow> inj_on the A" |
|
1279 by (auto simp: inj_on_def option.the_def split: option.splits) |
|
1280 |
|
1281 lemma inj_on_map_of': |
|
1282 assumes "distinct (map snd xs)" |
|
1283 shows "inj_on (the \<circ> map_of xs) (set (map fst xs))" |
|
1284 by (intro comp_inj_on inj_on_map_of assms inj_on_the) |
|
1285 (force simp: eq_commute[of None] map_of_eq_None_iff) |
|
1286 |
|
1287 lemma image_map_of: |
|
1288 assumes "distinct (map fst xs)" |
|
1289 shows "map_of xs ` set (map fst xs) = Some ` set (map snd xs)" |
|
1290 using assms by (auto simp: rev_image_eqI) |
|
1291 |
|
1292 lemma the_Some_image [simp]: "the ` Some ` A = A" |
|
1293 by (subst image_image) simp |
|
1294 |
|
1295 lemma image_map_of': |
|
1296 assumes "distinct (map fst xs)" |
|
1297 shows "(the \<circ> map_of xs) ` set (map fst xs) = set (map snd xs)" |
|
1298 by (simp only: image_comp [symmetric] image_map_of assms the_Some_image) |
|
1299 |
|
1300 lemma permutation_of_list_permutes [simp]: |
|
1301 assumes "list_permutes xs A" |
|
1302 shows "permutation_of_list xs permutes A" (is "?f permutes _") |
|
1303 proof (rule permutes_subset[OF bij_imp_permutes]) |
|
1304 from assms show "set (map fst xs) \<subseteq> A" |
|
1305 by (simp add: list_permutes_def) |
|
1306 from assms have "inj_on (the \<circ> map_of xs) (set (map fst xs))" (is ?P) |
|
1307 by (intro inj_on_map_of') (simp_all add: list_permutes_def) |
|
1308 also have "?P \<longleftrightarrow> inj_on ?f (set (map fst xs))" |
|
1309 by (intro inj_on_cong) |
|
1310 (auto simp: permutation_of_list_def map_of_eq_None_iff split: option.splits) |
|
1311 finally have "bij_betw ?f (set (map fst xs)) (?f ` set (map fst xs))" |
|
1312 by (rule inj_on_imp_bij_betw) |
|
1313 also from assms have "?f ` set (map fst xs) = (the \<circ> map_of xs) ` set (map fst xs)" |
|
1314 by (intro image_cong refl) |
|
1315 (auto simp: permutation_of_list_def map_of_eq_None_iff split: option.splits) |
|
1316 also from assms have "\<dots> = set (map fst xs)" |
|
1317 by (subst image_map_of') (simp_all add: list_permutes_def) |
|
1318 finally show "bij_betw ?f (set (map fst xs)) (set (map fst xs))" . |
|
1319 qed (force simp: permutation_of_list_def dest!: map_of_SomeD split: option.splits)+ |
|
1320 |
|
1321 lemma eval_permutation_of_list [simp]: |
|
1322 "permutation_of_list [] x = x" |
|
1323 "x = x' \<Longrightarrow> permutation_of_list ((x',y)#xs) x = y" |
|
1324 "x \<noteq> x' \<Longrightarrow> permutation_of_list ((x',y')#xs) x = permutation_of_list xs x" |
|
1325 by (simp_all add: permutation_of_list_def) |
|
1326 |
|
1327 lemma eval_inverse_permutation_of_list [simp]: |
|
1328 "inverse_permutation_of_list [] x = x" |
|
1329 "x = x' \<Longrightarrow> inverse_permutation_of_list ((y,x')#xs) x = y" |
|
1330 "x \<noteq> x' \<Longrightarrow> inverse_permutation_of_list ((y',x')#xs) x = inverse_permutation_of_list xs x" |
|
1331 by (simp_all add: inverse_permutation_of_list.simps) |
|
1332 |
|
1333 lemma permutation_of_list_id: |
|
1334 assumes "x \<notin> set (map fst xs)" |
|
1335 shows "permutation_of_list xs x = x" |
|
1336 using assms by (induction xs) (auto simp: permutation_of_list_Cons) |
|
1337 |
|
1338 lemma permutation_of_list_unique': |
|
1339 assumes "distinct (map fst xs)" "(x, y) \<in> set xs" |
|
1340 shows "permutation_of_list xs x = y" |
|
1341 using assms by (induction xs) (force simp: permutation_of_list_Cons)+ |
|
1342 |
|
1343 lemma permutation_of_list_unique: |
|
1344 assumes "list_permutes xs A" "(x,y) \<in> set xs" |
|
1345 shows "permutation_of_list xs x = y" |
|
1346 using assms by (intro permutation_of_list_unique') (simp_all add: list_permutes_def) |
|
1347 |
|
1348 lemma inverse_permutation_of_list_id: |
|
1349 assumes "x \<notin> set (map snd xs)" |
|
1350 shows "inverse_permutation_of_list xs x = x" |
|
1351 using assms by (induction xs) auto |
|
1352 |
|
1353 lemma inverse_permutation_of_list_unique': |
|
1354 assumes "distinct (map snd xs)" "(x, y) \<in> set xs" |
|
1355 shows "inverse_permutation_of_list xs y = x" |
|
1356 using assms by (induction xs) (force simp: inverse_permutation_of_list.simps)+ |
|
1357 |
|
1358 lemma inverse_permutation_of_list_unique: |
|
1359 assumes "list_permutes xs A" "(x,y) \<in> set xs" |
|
1360 shows "inverse_permutation_of_list xs y = x" |
|
1361 using assms by (intro inverse_permutation_of_list_unique') (simp_all add: list_permutes_def) |
|
1362 |
|
1363 lemma inverse_permutation_of_list_correct: |
|
1364 assumes "list_permutes xs (A :: 'a set)" |
|
1365 shows "inverse_permutation_of_list xs = inv (permutation_of_list xs)" |
|
1366 proof (rule ext, rule sym, subst permutes_inv_eq) |
|
1367 from assms show "permutation_of_list xs permutes A" by simp |
|
1368 next |
|
1369 fix x |
|
1370 show "permutation_of_list xs (inverse_permutation_of_list xs x) = x" |
|
1371 proof (cases "x \<in> set (map snd xs)") |
|
1372 case True |
|
1373 then obtain y where "(y, x) \<in> set xs" by force |
|
1374 with assms show ?thesis |
|
1375 by (simp add: inverse_permutation_of_list_unique permutation_of_list_unique) |
|
1376 qed (insert assms, auto simp: list_permutes_def |
|
1377 inverse_permutation_of_list_id permutation_of_list_id) |
|
1378 qed |
|
1379 |
1050 end |
1380 end |
1051 |
1381 |