--- a/src/HOL/Library/Multiset.thy Mon Sep 19 12:53:30 2016 +0200
+++ b/src/HOL/Library/Multiset.thy Mon Sep 19 17:37:22 2016 +0200
@@ -1989,6 +1989,21 @@
finally show ?case by simp
qed simp_all
+(* Contributed by Lukas Bulwahn *)
+lemma image_mset_mset_set:
+ assumes "inj_on f A"
+ shows "image_mset f (mset_set A) = mset_set (f ` A)"
+proof cases
+ assume "finite A"
+ from this \<open>inj_on f A\<close> show ?thesis
+ by (induct A) auto
+next
+ assume "infinite A"
+ from this \<open>inj_on f A\<close> have "infinite (f ` A)"
+ using finite_imageD by blast
+ from \<open>infinite A\<close> \<open>infinite (f ` A)\<close> show ?thesis by simp
+qed
+
subsection \<open>More properties of the replicate and repeat operations\<close>
--- a/src/HOL/Library/Permutations.thy Mon Sep 19 12:53:30 2016 +0200
+++ b/src/HOL/Library/Permutations.thy Mon Sep 19 17:37:22 2016 +0200
@@ -105,6 +105,48 @@
lemma permutes_superset: "p permutes S \<Longrightarrow> (\<forall>x \<in> S - T. p x = x) \<Longrightarrow> p permutes T"
by (simp add: Ball_def permutes_def) metis
+(* Next three lemmas contributed by Lukas Bulwahn *)
+lemma permutes_bij_inv_into:
+ fixes A :: "'a set" and B :: "'b set"
+ assumes "p permutes A"
+ assumes "bij_betw f A B"
+ shows "(\<lambda>x. if x \<in> B then f (p (inv_into A f x)) else x) permutes B"
+proof (rule bij_imp_permutes)
+ have "bij_betw p A A" "bij_betw f A B" "bij_betw (inv_into A f) B A"
+ using assms by (auto simp add: permutes_imp_bij bij_betw_inv_into)
+ from this have "bij_betw (f o p o inv_into A f) B B" by (simp add: bij_betw_trans)
+ from this show "bij_betw (\<lambda>x. if x \<in> B then f (p (inv_into A f x)) else x) B B"
+ by (subst bij_betw_cong[where g="f o p o inv_into A f"]) auto
+next
+ fix x
+ assume "x \<notin> B"
+ from this show "(if x \<in> B then f (p (inv_into A f x)) else x) = x" by auto
+qed
+
+lemma permutes_image_mset:
+ assumes "p permutes A"
+ shows "image_mset p (mset_set A) = mset_set A"
+using assms by (metis image_mset_mset_set bij_betw_imp_inj_on permutes_imp_bij permutes_image)
+
+lemma permutes_implies_image_mset_eq:
+ assumes "p permutes A" "\<And>x. x \<in> A \<Longrightarrow> f x = f' (p x)"
+ shows "image_mset f' (mset_set A) = image_mset f (mset_set A)"
+proof -
+ have "f x = f' (p x)" if x: "x \<in># mset_set A" for x
+ using assms(2)[of x] x by (cases "finite A") auto
+ from this have "image_mset f (mset_set A) = image_mset (f' o p) (mset_set A)"
+ using assms by (auto intro!: image_mset_cong)
+ also have "\<dots> = image_mset f' (image_mset p (mset_set A))"
+ by (simp add: image_mset.compositionality)
+ also have "\<dots> = image_mset f' (mset_set A)"
+ proof -
+ from assms have "image_mset p (mset_set A) = mset_set A"
+ using permutes_image_mset by blast
+ from this show ?thesis by simp
+ qed
+ finally show ?thesis ..
+qed
+
subsection \<open>Group properties\<close>
@@ -893,7 +935,7 @@
finally show "count (mset (permute_list f xs)) y = count (mset xs) y" by simp
qed
-lemma set_permute_list [simp]:
+lemma set_permute_list [simp]:
assumes "f permutes {..<length xs}"
shows "set (permute_list f xs) = set xs"
by (rule mset_eq_setD[OF mset_permute_list]) fact
@@ -933,69 +975,111 @@
subsection \<open>More lemmas about permutations\<close>
text \<open>
- If two lists correspond to the same multiset, there exists a permutation
- on the list indices that maps one to the other.
+ The following few lemmas were contributed by Lukas Bulwahn.
\<close>
-lemma mset_eq_permutation:
- assumes mset_eq: "mset (xs::'a list) = mset ys"
- defines [simp]: "n \<equiv> length xs"
- obtains f where "f permutes {..<length ys}" "permute_list f ys = xs"
+
+lemma count_image_mset_eq_card_vimage:
+ assumes "finite A"
+ shows "count (image_mset f (mset_set A)) b = card {a \<in> A. f a = b}"
+ using assms
+proof (induct A)
+ case empty
+ show ?case by simp
+next
+ case (insert x F)
+ show ?case
+ proof cases
+ assume "f x = b"
+ from this have "count (image_mset f (mset_set (insert x F))) b = Suc (card {a \<in> F. f a = f x})"
+ using insert.hyps by auto
+ also have "\<dots> = card (insert x {a \<in> F. f a = f x})"
+ using insert.hyps(1,2) by simp
+ also have "card (insert x {a \<in> F. f a = f x}) = card {a \<in> insert x F. f a = b}"
+ using \<open>f x = b\<close> by (auto intro: arg_cong[where f="card"])
+ finally show ?thesis using insert by auto
+ next
+ assume A: "f x \<noteq> b"
+ hence "{a \<in> F. f a = b} = {a \<in> insert x F. f a = b}" by auto
+ with insert A show ?thesis by simp
+ qed
+qed
+
+(* Prove image_mset_eq_implies_permutes *)
+lemma image_mset_eq_implies_permutes:
+ fixes f :: "'a \<Rightarrow> 'b"
+ assumes "finite A"
+ assumes mset_eq: "image_mset f (mset_set A) = image_mset f' (mset_set A)"
+ obtains p where "p permutes A" and "\<forall>x\<in>A. f x = f' (p x)"
proof -
- from mset_eq have [simp]: "length xs = length ys"
- by (rule mset_eq_length)
- define indices_of :: "'a \<Rightarrow> 'a list \<Rightarrow> nat set"
- where "indices_of x xs = {i. i < length xs \<and> x = xs ! i}" for x xs
- have indices_of_subset: "indices_of x xs \<subseteq> {..<length xs}" for x xs
- unfolding indices_of_def by blast
- have [simp]: "finite (indices_of x xs)" for x xs
- by (rule finite_subset[OF indices_of_subset]) simp_all
-
- have "\<forall>x\<in>set xs. \<exists>f. bij_betw f (indices_of x xs) (indices_of x ys)"
+ from \<open>finite A\<close> have [simp]: "finite {a \<in> A. f a = (b::'b)}" for f b by auto
+ have "f ` A = f' ` A"
+ proof -
+ have "f ` A = f ` (set_mset (mset_set A))" using \<open>finite A\<close> by simp
+ also have "\<dots> = f' ` (set_mset (mset_set A))"
+ by (metis mset_eq multiset.set_map)
+ also have "\<dots> = f' ` A" using \<open>finite A\<close> by simp
+ finally show ?thesis .
+ qed
+ have "\<forall>b\<in>(f ` A). \<exists>p. bij_betw p {a \<in> A. f a = b} {a \<in> A. f' a = b}"
proof
- fix x
- from mset_eq have "count (mset xs) x = count (mset ys) x" by simp
- hence "card (indices_of x xs) = card (indices_of x ys)"
- by (simp add: count_mset length_filter_conv_card indices_of_def)
- thus "\<exists>f. bij_betw f (indices_of x xs) (indices_of x ys)"
+ fix b
+ from mset_eq have
+ "count (image_mset f (mset_set A)) b = count (image_mset f' (mset_set A)) b" by simp
+ from this have "card {a \<in> A. f a = b} = card {a \<in> A. f' a = b}"
+ using \<open>finite A\<close>
+ by (simp add: count_image_mset_eq_card_vimage)
+ from this show "\<exists>p. bij_betw p {a\<in>A. f a = b} {a \<in> A. f' a = b}"
by (intro finite_same_card_bij) simp_all
qed
- hence "\<exists>f. \<forall>x\<in>set xs. bij_betw (f x) (indices_of x xs) (indices_of x ys)"
+ hence "\<exists>p. \<forall>b\<in>f ` A. bij_betw (p b) {a \<in> A. f a = b} {a \<in> A. f' a = b}"
by (rule bchoice)
- then guess f .. note f = this
- define g where "g i = (if i < n then f (xs ! i) i else i)" for i
-
- have bij_f: "bij_betw (\<lambda>i. f (xs ! i) i) (indices_of x xs) (indices_of x ys)"
- if x: "x \<in> set xs" for x
- proof (subst bij_betw_cong)
- from f x show "bij_betw (f x) (indices_of x xs) (indices_of x ys)" by blast
- fix i assume "i \<in> indices_of x xs"
- thus "f (xs ! i) i = f x i" by (simp add: indices_of_def)
+ then guess p .. note p = this
+ define p' where "p' = (\<lambda>a. if a \<in> A then p (f a) a else a)"
+ have "p' permutes A"
+ proof (rule bij_imp_permutes)
+ have "disjoint_family_on (\<lambda>i. {a \<in> A. f' a = i}) (f ` A)"
+ unfolding disjoint_family_on_def by auto
+ moreover have "bij_betw (\<lambda>a. p (f a) a) {a \<in> A. f a = b} {a \<in> A. f' a = b}" if b: "b \<in> f ` A" for b
+ using p b by (subst bij_betw_cong[where g="p b"]) auto
+ ultimately have "bij_betw (\<lambda>a. p (f a) a) (\<Union>b\<in>f ` A. {a \<in> A. f a = b}) (\<Union>b\<in>f ` A. {a \<in> A. f' a = b})"
+ by (rule bij_betw_UNION_disjoint)
+ moreover have "(\<Union>b\<in>f ` A. {a \<in> A. f a = b}) = A" by auto
+ moreover have "(\<Union>b\<in>f ` A. {a \<in> A. f' a = b}) = A" using \<open>f ` A = f' ` A\<close> by auto
+ ultimately show "bij_betw p' A A"
+ unfolding p'_def by (subst bij_betw_cong[where g="(\<lambda>a. p (f a) a)"]) auto
+ next
+ fix x
+ assume "x \<notin> A"
+ from this show "p' x = x"
+ unfolding p'_def by simp
qed
+ moreover from p have "\<forall>x\<in>A. f x = f' (p' x)"
+ unfolding p'_def using bij_betwE by fastforce
+ ultimately show ?thesis by (rule that)
+qed
- 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)"
- by (intro bij_betw_UNION_disjoint) (auto simp add: disjoint_family_on_def indices_of_def)
- also have "(\<Union>x\<in>set xs. indices_of x xs) = {..<n}" by (auto simp: indices_of_def)
- also from mset_eq have "set xs = set ys" by (rule mset_eq_setD)
- also have "(\<Union>x\<in>set ys. indices_of x ys) = {..<n}"
- by (auto simp: indices_of_def set_conv_nth)
- also have "bij_betw (\<lambda>i. f (xs ! i) i) {..<n} {..<n} \<longleftrightarrow> bij_betw g {..<n} {..<n}"
- by (intro bij_betw_cong) (simp_all add: g_def)
- finally have "g permutes {..<length ys}"
- by (intro bij_imp_permutes refl) (simp_all add: g_def)
+lemma mset_set_upto_eq_mset_upto:
+ "mset_set {..<n} = mset [0..<n]"
+ by (induct n) (auto simp add: add.commute lessThan_Suc)
- moreover have "permute_list g ys = xs"
- proof (rule sym, intro nth_equalityI allI impI)
- fix i assume i: "i < length xs"
- from i have "permute_list g ys ! i = ys ! f (xs ! i) i"
- by (simp add: permute_list_def g_def)
- also from i have "i \<in> indices_of (xs ! i) xs" by (simp add: indices_of_def)
- with bij_f[of "xs ! i"] i have "f (xs ! i) i \<in> indices_of (xs ! i) ys"
- by (auto simp: bij_betw_def)
- hence "ys ! f (xs ! i) i = xs ! i" by (simp add: indices_of_def)
- finally show "xs ! i = permute_list g ys ! i" ..
- qed simp_all
-
- ultimately show ?thesis by (rule that)
+(* and derive the existing property: *)
+lemma mset_eq_permutation:
+ assumes mset_eq: "mset (xs::'a list) = mset ys"
+ obtains p where "p permutes {..<length ys}" "permute_list p ys = xs"
+proof -
+ from mset_eq have length_eq: "length xs = length ys"
+ using mset_eq_length by blast
+ have "mset_set {..<length ys} = mset [0..<length ys]"
+ using mset_set_upto_eq_mset_upto by blast
+ from mset_eq length_eq this have
+ "image_mset (\<lambda>i. xs ! i) (mset_set {..<length ys}) = image_mset (\<lambda>i. ys ! i) (mset_set {..<length ys})"
+ by (metis map_nth mset_map)
+ from image_mset_eq_implies_permutes[OF _ this]
+ obtain p where "p permutes {..<length ys}"
+ and "\<forall>i\<in>{..<length ys}. xs ! i = ys ! (p i)" by auto
+ moreover from this length_eq have "permute_list p ys = xs"
+ by (auto intro!: nth_equalityI simp add: permute_list_nth)
+ ultimately show thesis using that by blast
qed
lemma permutes_natset_le: