more connections between mset _ = mset _ and permutations

--- 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>