summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | haftmann |

Sun, 28 Feb 2021 20:13:07 +0000 | |

changeset 73327 | fd32f08f4fb5 |

parent 73326 | 7a88313895d5 |

child 73328 | ff24fe85ee57 |

more connections between mset _ = mset _ and permutations

src/HOL/Library/List_Permutation.thy | file | annotate | diff | comparison | revisions | |

src/HOL/Library/Multiset.thy | file | annotate | diff | comparison | revisions |

--- a/src/HOL/Library/List_Permutation.thy Sun Feb 28 20:13:07 2021 +0000 +++ b/src/HOL/Library/List_Permutation.thy Sun Feb 28 20:13:07 2021 +0000 @@ -5,7 +5,7 @@ section \<open>Permuted Lists\<close> theory List_Permutation -imports Multiset +imports Permutations begin subsection \<open>An inductive definition \ldots\<close> @@ -82,12 +82,17 @@ assumes "xs <~~> ys" shows "\<exists>f. bij_betw f {..<length xs} {..<length ys} \<and> (\<forall>i<length xs. xs ! i = ys ! (f i))" proof - - from assms have \<open>mset ys = mset xs\<close> - by (simp add: perm_iff_eq_mset) - then obtain f where \<open>bij_betw f {..<length ys} {..<length xs}\<close> - \<open>xs = map (\<lambda>n. ys ! f n) [0..<length ys]\<close> + from assms have \<open>mset xs = mset ys\<close> \<open>length xs = length ys\<close> + by (auto simp add: perm_iff_eq_mset dest: mset_eq_length) + from \<open>mset xs = mset ys\<close> obtain p where \<open>p permutes {..<length ys}\<close> \<open>permute_list p ys = xs\<close> by (rule mset_eq_permutation) - then show ?thesis by auto + then have \<open>bij_betw p {..<length xs} {..<length ys}\<close> + by (simp add: \<open>length xs = length ys\<close> permutes_imp_bij) + moreover have \<open>\<forall>i<length xs. xs ! i = ys ! (p i)\<close> + using \<open>permute_list p ys = xs\<close> \<open>length xs = length ys\<close> \<open>p permutes {..<length ys}\<close> permute_list_nth + by auto + ultimately show ?thesis + by blast qed proposition perm_finite: "finite {B. B <~~> A}"

--- a/src/HOL/Library/Multiset.thy Sun Feb 28 20:13:07 2021 +0000 +++ b/src/HOL/Library/Multiset.thy Sun Feb 28 20:13:07 2021 +0000 @@ -2720,109 +2720,7 @@ mset (ls[j := ls ! i, i := ls ! j]) = mset ls" by (cases "i = j") (simp_all add: mset_update nth_mem_mset) -lemma mset_eq_permutation: - assumes \<open>mset xs = mset ys\<close> - obtains f where - \<open>bij_betw f {..<length xs} {..<length ys}\<close> - \<open>ys = map (\<lambda>n. xs ! f n) [0..<length xs]\<close> -proof - - from assms have \<open>length ys = length xs\<close> - by (auto dest: mset_eq_length) - from assms have \<open>\<exists>f. f ` {..<length xs} = {..<length xs} \<and> ys = map (\<lambda>n. xs ! f n) [0..<length xs]\<close> - proof (induction xs arbitrary: ys rule: rev_induct) - case Nil - then show ?case by simp - next - case (snoc x xs) - from snoc.prems have \<open>x \<in> set ys\<close> - by (auto dest: union_single_eq_member) - then obtain zs ws where split: \<open>ys = zs @ x # ws\<close> and \<open>x \<notin> set zs\<close> - by (auto dest: split_list_first) - then have \<open>remove1 x ys = zs @ ws\<close> - by (simp add: remove1_append) - moreover from snoc.prems [symmetric] have \<open>mset xs = mset (remove1 x ys)\<close> - by simp - ultimately have \<open>mset xs = mset (zs @ ws)\<close> - by simp - then have \<open>\<exists>f. f ` {..<length xs} = {..<length xs} \<and> zs @ ws = map (\<lambda>n. xs ! f n) [0..<length xs]\<close> - by (rule snoc.IH) - then obtain f where - raw_surj: \<open>f ` {..<length xs} = {..<length xs}\<close> - and hyp: \<open>zs @ ws = map (\<lambda>n. xs ! f n) [0..<length xs]\<close> by blast - define l and k where \<open>l = length zs\<close> and \<open>k = length ws\<close> - then have [simp]: \<open>length zs = l\<close> \<open>length ws = k\<close> - by simp_all - from \<open>mset xs = mset (zs @ ws)\<close> have \<open>length xs = length (zs @ ws)\<close> - by (rule mset_eq_length) - then have [simp]: \<open>length xs = l + k\<close> - by simp - from raw_surj have f_surj: \<open>f ` {..<l + k} = {..<l + k}\<close> - by simp - have [simp]: \<open>[0..<l + k] = [0..<l] @ [l..<l + k]\<close> - by (rule nth_equalityI) (simp_all add: nth_append) - have [simp]: \<open>[l..<l + k] @ [l + k] = [l] @ [Suc l..<Suc (l + k)]\<close> - by (rule nth_equalityI) - (auto simp add: nth_append nth_Cons split: nat.split) - define g :: \<open>nat \<Rightarrow> nat\<close> - where \<open>g n = (if n < l then f n - else if n = l then l + k - else f (n - 1))\<close> for n - have \<open>{..<Suc (l + k)} = {..<l} \<union> {l} \<union> {Suc l..<Suc (l + k)}\<close> - by auto - then have \<open>g ` {..<Suc (l + k)} = g ` {..<l} \<union> {g l} \<union> g ` {Suc l..<Suc (l + k)}\<close> - by auto - also have \<open>g ` {Suc l..<Suc (l + k)} = f ` {l..<l + k}\<close> - apply (auto simp add: g_def Suc_le_lessD) - apply (auto simp add: image_def) - apply (metis Suc_le_mono atLeastLessThan_iff diff_Suc_Suc diff_zero lessI less_trans_Suc) - done - finally have \<open>g ` {..<Suc (l + k)} = f ` {..<l} \<union> {l + k} \<union> f ` {l..<l + k}\<close> - by (simp add: g_def) - also have \<open>\<dots> = {..<Suc (l + k)}\<close> - by simp (metis atLeastLessThan_add_Un f_surj image_Un le_add1 le_add_same_cancel1 lessThan_Suc lessThan_atLeast0) - finally have g_surj: \<open>g ` {..<Suc (l + k)} = {..<Suc (l + k)}\<close> . - from hyp have zs_f: \<open>zs = map (\<lambda>n. xs ! f n) [0..<l]\<close> - and ws_f: \<open>ws = map (\<lambda>n. xs ! f n) [l..<l + k]\<close> - by simp_all - have \<open>zs = map (\<lambda>n. (xs @ [x]) ! g n) [0..<l]\<close> - proof (rule sym, rule map_upt_eqI) - fix n - assume \<open>n < length zs\<close> - then have \<open>n < l\<close> - by simp - with f_surj have \<open>f n < l + k\<close> - by auto - with \<open>n < l\<close> show \<open>zs ! n = (xs @ [x]) ! g (0 + n)\<close> - by (simp add: zs_f g_def nth_append) - qed simp - moreover have \<open>x = (xs @ [x]) ! g l\<close> - by (simp add: g_def nth_append) - moreover have \<open>ws = map (\<lambda>n. (xs @ [x]) ! g n) [Suc l..<Suc (l + k)]\<close> - proof (rule sym, rule map_upt_eqI) - fix n - assume \<open>n < length ws\<close> - then have \<open>n < k\<close> - by simp - with f_surj have \<open>f (l + n) < l + k\<close> - by auto - with \<open>n < k\<close> show \<open>ws ! n = (xs @ [x]) ! g (Suc l + n)\<close> - by (simp add: ws_f g_def nth_append) - qed simp - ultimately have \<open>zs @ x # ws = map (\<lambda>n. (xs @ [x]) ! g n) [0..<length (xs @ [x])]\<close> - by simp - with g_surj show ?case - by (auto simp add: split) - qed - then obtain f where - surj: \<open>f ` {..<length xs} = {..<length xs}\<close> - and hyp: \<open>ys = map (\<lambda>n. xs ! f n) [0..<length xs]\<close> by blast - from surj have \<open>bij_betw f {..<length xs} {..<length ys}\<close> - by (simp add: bij_betw_def \<open>length ys = length xs\<close> eq_card_imp_inj_on) - then show thesis - using hyp .. -qed - -proposition mset_eq_finite: +lemma mset_eq_finite: \<open>finite {ys. mset ys = mset xs}\<close> proof - have \<open>{ys. mset ys = mset xs} \<subseteq> {ys. set ys \<subseteq> set xs \<and> length ys \<le> length xs}\<close>