# HG changeset patch
# User haftmann
# Date 1621242450 0
# Node ID 4b1386b2c23e7405a6ebcd748ae19804a3173241
# Parent  ac07f6be27eae7481ca87d23f3caf56bd69d2f82
mere abbreviation for logical alias

diff -r ac07f6be27ea -r 4b1386b2c23e src/HOL/Algebra/Divisibility.thy
--- a/src/HOL/Algebra/Divisibility.thy	Mon May 17 13:57:19 2021 +1000
+++ b/src/HOL/Algebra/Divisibility.thy	Mon May 17 09:07:30 2021 +0000
@@ -878,7 +878,7 @@
 lemma perm_map [intro]:
   assumes p: "a <~~> b"
   shows "map f a <~~> map f b"
-  using p by (simp add: perm_iff_eq_mset)
+  using p by simp
 
 lemma perm_map_switch:
   assumes m: "map f a = map f b" and p: "b <~~> c"
@@ -887,7 +887,7 @@
   from m have \<open>length a = length b\<close>
     by (rule map_eq_imp_length_eq)
   from p have \<open>mset c = mset b\<close>
-    by (simp add: perm_iff_eq_mset)
+    by simp
   then obtain p where \<open>p permutes {..<length b}\<close> \<open>permute_list p b = c\<close>
     by (rule mset_eq_permutation)
   with \<open>length a = length b\<close> have \<open>p permutes {..<length a}\<close>
@@ -897,48 +897,27 @@
     using m \<open>p permutes {..<length b}\<close> \<open>permute_list p b = c\<close>
     by (auto simp flip: permute_list_map)
   then show ?thesis
-    by (auto simp add: perm_iff_eq_mset)
+    by auto
 qed
 
 lemma (in monoid) perm_assoc_switch:
   assumes a:"as [\<sim>] bs" and p: "bs <~~> cs"
   shows "\<exists>bs'. as <~~> bs' \<and> bs' [\<sim>] cs"
-  using p a
-proof (induction bs cs arbitrary: as)
-  case (swap y x l)
-  then show ?case
-    by (metis (no_types, hide_lams) list_all2_Cons2 perm.swap)
-next
-case (Cons xs ys z)
-  then show ?case
-    by (metis list_all2_Cons2 perm.Cons)
-next
-  case (trans xs ys zs)
-  then show ?case
-    by (meson perm.trans)
-qed auto
+proof -
+  from p have \<open>mset cs = mset bs\<close>
+    by simp
+  then obtain p where \<open>p permutes {..<length bs}\<close> \<open>permute_list p bs = cs\<close>
+    by (rule mset_eq_permutation)
+  moreover define bs' where \<open>bs' = permute_list p as\<close>
+  ultimately have \<open>as <~~> bs'\<close> and \<open>bs' [\<sim>] cs\<close>
+    using a by (auto simp add: list_all2_permute_list_iff list_all2_lengthD)
+  then show ?thesis by blast
+qed
 
 lemma (in monoid) perm_assoc_switch_r:
   assumes p: "as <~~> bs" and a:"bs [\<sim>] cs"
   shows "\<exists>bs'. as [\<sim>] bs' \<and> bs' <~~> cs"
-  using p a
-proof (induction as bs arbitrary: cs)
-  case Nil
-  then show ?case
-    by auto
-next
-  case (swap y x l)
-  then show ?case
-    by (metis (no_types, hide_lams) list_all2_Cons1 perm.swap)
-next
-  case (Cons xs ys z)
-  then show ?case
-    by (metis list_all2_Cons1 perm.Cons)
-next
-  case (trans xs ys zs)
-  then show ?case
-    by (blast intro:  elim: )
-qed
+  using a p by (rule list_all2_reorder_left_invariance)
 
 declare perm_sym [sym]
 
@@ -946,14 +925,7 @@
   assumes perm: "as <~~> bs"
     and as: "P (set as)"
   shows "P (set bs)"
-proof -
-  from perm have "mset as = mset bs"
-    by (simp add: mset_eq_perm)
-  then have "set as = set bs"
-    by (rule mset_eq_setD)
-  with as show "P (set bs)"
-    by simp
-qed
+  using assms by (metis set_mset_mset)
 
 lemmas (in monoid) perm_closed = perm_setP[of _ _ "\<lambda>as. as \<subseteq> carrier G"]
 
@@ -1006,7 +978,7 @@
   from perm_assoc_switch [OF this] obtain bs' where p: "abs <~~> bs'" and a: "bs' [\<sim>] bcs"
     by blast
   assume "as <~~> abs"
-  with p have pp: "as <~~> bs'" by fast
+  with p have pp: "as <~~> bs'" by simp
   from pp ascarr have c1: "set bs' \<subseteq> carrier G" by (rule perm_closed)
   from pb bscarr have c2: "set bcs \<subseteq> carrier G" by (rule perm_closed)
   assume "bcs [\<sim>] cs"
@@ -1063,14 +1035,15 @@
   assumes prm: "as <~~> bs"
     and ascarr: "set as \<subseteq> carrier G"
   shows "foldr (\<otimes>) as \<one> = foldr (\<otimes>) bs \<one>"
-  using prm ascarr
-proof induction
-  case (swap y x l) then show ?case
-    by (simp add: m_lcomm)
-next
-  case (trans xs ys zs) then show ?case
-    using perm_closed by auto
-qed auto
+proof -
+  from prm have \<open>mset (rev as) = mset (rev bs)\<close>
+    by simp
+  moreover note one_closed
+  ultimately have \<open>fold (\<otimes>) (rev as) \<one> = fold (\<otimes>) (rev bs) \<one>\<close>
+    by (rule fold_permuted_eq) (use ascarr in \<open>auto intro: m_lcomm\<close>)
+  then show ?thesis
+    by (simp add: foldr_conv_fold)
+qed
 
 lemma (in comm_monoid_cancel) multlist_ee_cong:
   assumes "essentially_equal G fs fs'"
@@ -1197,12 +1170,13 @@
 proof (elim essentially_equalE)
   fix fs
   assume prm: "as <~~> fs"
-  with carr have fscarr: "set fs \<subseteq> carrier G" by (simp add: perm_closed)
+  with carr have fscarr: "set fs \<subseteq> carrier G"
+    using perm_closed by blast
 
   note bfs
   also assume [symmetric]: "fs [\<sim>] bs"
   also (wfactors_listassoc_cong_l)
-  note prm[symmetric]
+  have \<open>mset fs = mset as\<close> using prm by simp
   finally (wfactors_perm_cong_l)
   show "wfactors G as b" by (simp add: carr fscarr)
 qed
@@ -1621,7 +1595,7 @@
 lemma (in monoid) fmset_perm_cong:
   assumes prm: "as <~~> bs"
   shows "fmset G as = fmset G bs"
-  using perm_map[OF prm] unfolding mset_eq_perm fmset_def by blast
+  using perm_map[OF prm] unfolding fmset_def by blast
 
 lemma (in comm_monoid_cancel) eqc_listassoc_cong:
   assumes "as [\<sim>] bs" and "set as \<subseteq> carrier G" and "set bs \<subseteq> carrier G"
@@ -1683,7 +1657,7 @@
     by (simp_all add: permute_list_map) 
   moreover define as' where \<open>as' = permute_list p as\<close>
   ultimately have tp: "as <~~> as'" and tm: "map (assocs G) as' = map (assocs G) bs"
-    by (simp_all add: perm_iff_eq_mset)
+    by simp_all
   from tp show ?thesis
   proof (rule essentially_equalI)
     from tm tp ascarr have as'carr: "set as' \<subseteq> carrier G"
@@ -1941,7 +1915,7 @@
   then obtain ds where "p # cs <~~> ds" and dsassoc: "ds [\<sim>] (as @ bs)"
     by (fast elim: essentially_equalE)
   then have "p \<in> set ds"
-    by (simp add: perm_set_eq[symmetric])
+    by (metis \<open>mset (p # cs) = mset ds\<close> insert_iff list.set(2) perm_set_eq) 
   with dsassoc obtain p' where "p' \<in> set (as@bs)" and pp': "p \<sim> p'"
     unfolding list_all2_conv_all_nth set_conv_nth by force
   then consider "p' \<in> set as" | "p' \<in> set bs" by auto
@@ -2003,7 +1977,7 @@
         then obtain ds where "p # cs <~~> ds" and dsassoc: "ds [\<sim>] (as @ bs)"
           by (fast elim: essentially_equalE)
         then have "p \<in> set ds"
-          by (simp add: perm_set_eq[symmetric])
+          by (metis list.set_intros(1) set_mset_mset)
         with dsassoc obtain p' where "p' \<in> set (as@bs)" and pp': "p \<sim> p'"
           unfolding list_all2_conv_all_nth set_conv_nth by force
         then consider "p' \<in> set as" | "p' \<in> set bs" by auto
@@ -2641,7 +2615,7 @@
 proof (induct as arbitrary: a as')
   case Nil
   then have "a \<sim> \<one>"
-    by (meson Units_one_closed one_closed perm.Nil perm_wfactorsD unit_wfactors)
+    by (simp add: perm_wfactorsD) 
   then have "as' = []"
     using Nil.prems assoc_unit_l unit_wfactors_empty by blast
   then show ?case
@@ -2728,8 +2702,12 @@
       by (simp add: a'carr set_drop set_take)
     from a'fs this have "essentially_equal G as (take i as' @ drop (Suc i) as')"
       using Cons.hyps a'carr carr_ah(2) set_drop set_take by auto
-    with carr_ah have ee1: "essentially_equal G (ah # as) (ah # take i as' @ drop (Suc i) as')"
-      by (auto simp: essentially_equal_def)
+    then obtain bs where \<open>mset as = mset bs\<close> \<open>bs [\<sim>] take i as' @ drop (Suc i) as'\<close>
+      by (auto simp add: essentially_equal_def)
+    with carr_ah have \<open>mset (ah # as) = mset (ah # bs)\<close> \<open>ah # bs [\<sim>] ah # take i as' @ drop (Suc i) as'\<close>
+      by simp_all
+    then have ee1: "essentially_equal G (ah # as) (ah # take i as' @ drop (Suc i) as')"
+      unfolding essentially_equal_def by blast
     have ee2: "essentially_equal G (ah # take i as' @ drop (Suc i) as')
       (as' ! i # take i as' @ drop (Suc i) as')"
     proof (intro essentially_equalI)
diff -r ac07f6be27ea -r 4b1386b2c23e src/HOL/Combinatorics/List_Permutation.thy
--- a/src/HOL/Combinatorics/List_Permutation.thy	Mon May 17 13:57:19 2021 +1000
+++ b/src/HOL/Combinatorics/List_Permutation.thy	Mon May 17 09:07:30 2021 +0000
@@ -13,52 +13,10 @@
   \<^text>\<open>Permutations\<close>; it should be seldom needed.
 \<close>
 
-subsection \<open>An inductive definition \ldots\<close>
-
-inductive perm :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"  (infixr \<open><~~>\<close> 50)
-where
-  Nil [intro!]: "[] <~~> []"
-| swap [intro!]: "y # x # l <~~> x # y # l"
-| Cons [intro!]: "xs <~~> ys \<Longrightarrow> z # xs <~~> z # ys"
-| trans [intro]: "xs <~~> ys \<Longrightarrow> ys <~~> zs \<Longrightarrow> xs <~~> zs"
-
-proposition perm_refl [iff]: "l <~~> l"
-  by (induct l) auto
-
-text \<open>\ldots that is equivalent to an already existing notion:\<close>
+subsection \<open>An existing notion\<close>
 
-lemma perm_iff_eq_mset:
-  \<open>xs <~~> ys \<longleftrightarrow> mset xs = mset ys\<close>
-proof
-  assume \<open>mset xs = mset ys\<close>
-  then show \<open>xs <~~> ys\<close>
-  proof (induction xs arbitrary: ys)
-    case Nil
-    then show ?case
-      by simp
-  next
-    case (Cons x xs)
-    from Cons.prems [symmetric] have \<open>mset xs = mset (remove1 x ys)\<close>
-      by simp
-    then have \<open>xs <~~> remove1 x ys\<close>
-      by (rule Cons.IH)
-    then have \<open>x # xs <~~> x # remove1 x ys\<close>
-      by (rule perm.Cons)
-    moreover from Cons.prems have \<open>x \<in> set ys\<close>
-      by (auto dest: union_single_eq_member)
-    then have \<open>x # remove1 x ys <~~> ys\<close>
-      by (induction ys) auto
-    ultimately show \<open>x # xs <~~> ys\<close>
-      by (rule perm.trans)
-  qed
-next
-  assume \<open>xs <~~> ys\<close>
-  then show \<open>mset xs = mset ys\<close>
-    by induction simp_all
-qed
-
-theorem mset_eq_perm: \<open>mset xs = mset ys \<longleftrightarrow> xs <~~> ys\<close>
-  by (simp add: perm_iff_eq_mset)
+abbreviation (input) perm :: \<open>'a list \<Rightarrow> 'a list \<Rightarrow> bool\<close>  (infixr \<open><~~>\<close> 50)
+  where \<open>xs <~~> ys \<equiv> mset xs = mset ys\<close>
 
 
 subsection \<open>Nontrivial conclusions\<close>
@@ -66,29 +24,29 @@
 proposition perm_swap:
   \<open>xs[i := xs ! j, j := xs ! i] <~~> xs\<close>
   if \<open>i < length xs\<close> \<open>j < length xs\<close>
-  using that by (simp add: perm_iff_eq_mset mset_swap)
+  using that by (simp add: mset_swap)
 
 proposition mset_le_perm_append: "mset xs \<subseteq># mset ys \<longleftrightarrow> (\<exists>zs. xs @ zs <~~> ys)"
-  by (auto simp add: perm_iff_eq_mset mset_subset_eq_exists_conv ex_mset dest: sym)
+  by (auto simp add: mset_subset_eq_exists_conv ex_mset dest: sym)
 
 proposition perm_set_eq: "xs <~~> ys \<Longrightarrow> set xs = set ys"
-  by (rule mset_eq_setD) (simp add: perm_iff_eq_mset)
+  by (rule mset_eq_setD) simp
 
 proposition perm_distinct_iff: "xs <~~> ys \<Longrightarrow> distinct xs \<longleftrightarrow> distinct ys"
-  by (rule mset_eq_imp_distinct_iff) (simp add: perm_iff_eq_mset)
+  by (rule mset_eq_imp_distinct_iff) simp
 
 theorem eq_set_perm_remdups: "set xs = set ys \<Longrightarrow> remdups xs <~~> remdups ys"
-  by (simp add: perm_iff_eq_mset set_eq_iff_mset_remdups_eq)
+  by (simp add: set_eq_iff_mset_remdups_eq)
 
 proposition perm_remdups_iff_eq_set: "remdups x <~~> remdups y \<longleftrightarrow> set x = set y"
-  by (simp add: perm_iff_eq_mset set_eq_iff_mset_remdups_eq)
+  by (simp add: set_eq_iff_mset_remdups_eq)
 
 theorem permutation_Ex_bij:
   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 xs = mset ys\<close> \<open>length xs = length ys\<close>
-    by (auto simp add: perm_iff_eq_mset dest: mset_eq_length)
+    by (auto simp add: 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 have \<open>bij_betw p {..<length xs} {..<length ys}\<close>
@@ -101,84 +59,84 @@
 qed
 
 proposition perm_finite: "finite {B. B <~~> A}"
-  using mset_eq_finite by (auto simp add: perm_iff_eq_mset)
+  using mset_eq_finite by auto
 
 
 subsection \<open>Trivial conclusions:\<close>
 
 proposition perm_empty_imp: "[] <~~> ys \<Longrightarrow> ys = []"
-  by (simp add: perm_iff_eq_mset)
+  by simp
 
 
 text \<open>\medskip This more general theorem is easier to understand!\<close>
 
 proposition perm_length: "xs <~~> ys \<Longrightarrow> length xs = length ys"
-  by (rule mset_eq_length) (simp add: perm_iff_eq_mset)
+  by (rule mset_eq_length) simp
 
 proposition perm_sym: "xs <~~> ys \<Longrightarrow> ys <~~> xs"
-  by (simp add: perm_iff_eq_mset)
+  by simp
 
 
 text \<open>We can insert the head anywhere in the list.\<close>
 
 proposition perm_append_Cons: "a # xs @ ys <~~> xs @ a # ys"
-  by (simp add: perm_iff_eq_mset)
+  by simp
 
 proposition perm_append_swap: "xs @ ys <~~> ys @ xs"
-  by (simp add: perm_iff_eq_mset)
+  by simp
 
 proposition perm_append_single: "a # xs <~~> xs @ [a]"
-  by (simp add: perm_iff_eq_mset)
+  by simp
 
 proposition perm_rev: "rev xs <~~> xs"
-  by (simp add: perm_iff_eq_mset)
+  by simp
 
 proposition perm_append1: "xs <~~> ys \<Longrightarrow> l @ xs <~~> l @ ys"
-  by (simp add: perm_iff_eq_mset)
+  by simp
 
 proposition perm_append2: "xs <~~> ys \<Longrightarrow> xs @ l <~~> ys @ l"
-  by (simp add: perm_iff_eq_mset)
+  by simp
 
 proposition perm_empty [iff]: "[] <~~> xs \<longleftrightarrow> xs = []"
-  by (simp add: perm_iff_eq_mset)
+  by simp
 
 proposition perm_empty2 [iff]: "xs <~~> [] \<longleftrightarrow> xs = []"
-  by (simp add: perm_iff_eq_mset)
+  by simp
 
 proposition perm_sing_imp: "ys <~~> xs \<Longrightarrow> xs = [y] \<Longrightarrow> ys = [y]"
-  by (simp add: perm_iff_eq_mset)
+  by simp
 
 proposition perm_sing_eq [iff]: "ys <~~> [y] \<longleftrightarrow> ys = [y]"
-  by (simp add: perm_iff_eq_mset)
+  by simp
 
 proposition perm_sing_eq2 [iff]: "[y] <~~> ys \<longleftrightarrow> ys = [y]"
-  by (simp add: perm_iff_eq_mset)
+  by simp
 
 proposition perm_remove: "x \<in> set ys \<Longrightarrow> ys <~~> x # remove1 x ys"
-  by (simp add: perm_iff_eq_mset)
+  by simp
 
 
 text \<open>\medskip Congruence rule\<close>
 
 proposition perm_remove_perm: "xs <~~> ys \<Longrightarrow> remove1 z xs <~~> remove1 z ys"
-  by (simp add: perm_iff_eq_mset)
+  by simp
 
 proposition remove_hd [simp]: "remove1 z (z # xs) = xs"
-  by (simp add: perm_iff_eq_mset)
+  by simp
 
 proposition cons_perm_imp_perm: "z # xs <~~> z # ys \<Longrightarrow> xs <~~> ys"
-  by (simp add: perm_iff_eq_mset)
+  by simp
 
 proposition cons_perm_eq [simp]: "z#xs <~~> z#ys \<longleftrightarrow> xs <~~> ys"
-  by (simp add: perm_iff_eq_mset)
+  by simp
 
 proposition append_perm_imp_perm: "zs @ xs <~~> zs @ ys \<Longrightarrow> xs <~~> ys"
-  by (simp add: perm_iff_eq_mset)
+  by simp
 
 proposition perm_append1_eq [iff]: "zs @ xs <~~> zs @ ys \<longleftrightarrow> xs <~~> ys"
-  by (simp add: perm_iff_eq_mset)
+  by simp
 
 proposition perm_append2_eq [iff]: "xs @ zs <~~> ys @ zs \<longleftrightarrow> xs <~~> ys"
-  by (simp add: perm_iff_eq_mset)
+  by simp
 
 end
diff -r ac07f6be27ea -r 4b1386b2c23e src/HOL/Combinatorics/Permutations.thy
--- a/src/HOL/Combinatorics/Permutations.thy	Mon May 17 13:57:19 2021 +1000
+++ b/src/HOL/Combinatorics/Permutations.thy	Mon May 17 09:07:30 2021 +0000
@@ -1150,6 +1150,11 @@
     by (induct xs) (auto simp: inv_f_f surj_f_inv_f)
 qed
 
+lemma list_all2_permute_list_iff:
+  \<open>list_all2 P (permute_list p xs) (permute_list p ys) \<longleftrightarrow> list_all2 P xs ys\<close>
+  if \<open>p permutes {..<length xs}\<close>
+  using that by (auto simp add: list_all2_iff simp flip: permute_list_zip)
+
 
 subsection \<open>More lemmas about permutations\<close>
 
diff -r ac07f6be27ea -r 4b1386b2c23e src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Mon May 17 13:57:19 2021 +1000
+++ b/src/HOL/Library/Multiset.thy	Mon May 17 09:07:30 2021 +0000
@@ -1923,26 +1923,55 @@
   using assms by (metis count_mset)
 
 lemma fold_multiset_equiv:
-  assumes f: "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f x \<circ> f y = f y \<circ> f x"
-    and equiv: "mset xs = mset ys"
-  shows "List.fold f xs = List.fold f ys"
-  using f equiv [symmetric]
-proof (induct xs arbitrary: ys)
+  \<open>List.fold f xs = List.fold f ys\<close>
+    if f: \<open>\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f x \<circ> f y = f y \<circ> f x\<close>
+    and \<open>mset xs = mset ys\<close>
+using f \<open>mset xs = mset ys\<close> [symmetric] proof (induction xs arbitrary: ys)
   case Nil
   then show ?case by simp
 next
   case (Cons x xs)
-  then have *: "set ys = set (x # xs)"
+  then have *: \<open>set ys = set (x # xs)\<close>
     by (blast dest: mset_eq_setD)
-  have "\<And>x y. x \<in> set ys \<Longrightarrow> y \<in> set ys \<Longrightarrow> f x \<circ> f y = f y \<circ> f x"
+  have \<open>\<And>x y. x \<in> set ys \<Longrightarrow> y \<in> set ys \<Longrightarrow> f x \<circ> f y = f y \<circ> f x\<close>
     by (rule Cons.prems(1)) (simp_all add: *)
-  moreover from * have "x \<in> set ys"
+  moreover from * have \<open>x \<in> set ys\<close>
+    by simp
+  ultimately have \<open>List.fold f ys = List.fold f (remove1 x ys) \<circ> f x\<close>
+    by (fact fold_remove1_split)
+  moreover from Cons.prems have \<open>List.fold f xs = List.fold f (remove1 x ys)\<close>
+    by (auto intro: Cons.IH)
+  ultimately show ?case
     by simp
-  ultimately have "List.fold f ys = List.fold f (remove1 x ys) \<circ> f x"
-    by (fact fold_remove1_split)
-  moreover from Cons.prems have "List.fold f xs = List.fold f (remove1 x ys)"
-    by (auto intro: Cons.hyps)
-  ultimately show ?case by simp
+qed
+
+lemma fold_permuted_eq:
+  \<open>List.fold (\<odot>) xs z = List.fold (\<odot>) ys z\<close>
+    if \<open>mset xs = mset ys\<close>
+    and \<open>P z\<close> and P: \<open>\<And>x z. x \<in> set xs \<Longrightarrow> P z \<Longrightarrow> P (x \<odot> z)\<close>
+    and f: \<open>\<And>x y z. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> P z \<Longrightarrow> x \<odot> (y \<odot> z) = y \<odot> (x \<odot> z)\<close>
+  for f (infixl \<open>\<odot>\<close> 70)
+using \<open>P z\<close> P f \<open>mset xs = mset ys\<close> [symmetric] proof (induction xs arbitrary: ys z)
+  case Nil
+  then show ?case by simp
+next
+  case (Cons x xs)
+  then have *: \<open>set ys = set (x # xs)\<close>
+    by (blast dest: mset_eq_setD)
+  have \<open>P z\<close>
+    by (fact Cons.prems(1))
+  moreover have \<open>\<And>x z. x \<in> set ys \<Longrightarrow> P z \<Longrightarrow> P (x \<odot> z)\<close>
+    by (rule Cons.prems(2)) (simp_all add: *)
+  moreover have \<open>\<And>x y z. x \<in> set ys \<Longrightarrow> y \<in> set ys \<Longrightarrow> P z \<Longrightarrow> x \<odot> (y \<odot> z) = y \<odot> (x \<odot> z)\<close>
+    by (rule Cons.prems(3)) (simp_all add: *)
+  moreover from * have \<open>x \<in> set ys\<close>
+    by simp
+  ultimately have \<open>fold (\<odot>) ys z = fold (\<odot>) (remove1 x ys) (x \<odot> z)\<close>
+    by (induction ys arbitrary: z) auto
+  moreover from Cons.prems have \<open>fold (\<odot>) xs (x \<odot> z) = fold (\<odot>) (remove1 x ys) (x \<odot> z)\<close>
+    by (auto intro: Cons.IH)
+  ultimately show ?case
+    by simp
 qed
 
 lemma mset_shuffles: "zs \<in> shuffles xs ys \<Longrightarrow> mset zs = mset xs + mset ys"