src/HOL/Algebra/Divisibility.thy

   from bfs have birr: "\<forall>b \<in> set bs. irreducible G b" by (fast elim: wfactorsE)
 
   have "\<exists>c cs. c \<in> carrier G \<and> set cs \<subseteq> carrier G \<and> wfactors G cs c \<and> fmset G cs = fmset G bs - fmset G as"
   proof (intro mset_wfactorsEx, simp)
     fix X
-    assume "count (fmset G as) X < count (fmset G bs) X"
-    hence "0 < count (fmset G bs) X" by simp
-    hence "X \<in> set_mset (fmset G bs)" by simp
+    assume "X \<in># fmset G bs - fmset G as"
+    hence "X \<in># fmset G bs" by (rule in_diffD)
     hence "X \<in> set (map (assocs G) bs)" by (simp add: fmset_def)
     hence "\<exists>x. x \<in> set bs \<and> X = assocs G x" by (induct bs) auto
     from this obtain x
         where xbs: "x \<in> set bs"
         and X: "X = assocs G x"

 
   have "\<exists>c cs. c \<in> carrier G \<and> set cs \<subseteq> carrier G \<and> wfactors G cs c \<and> 
                fmset G cs = fmset G as #\<inter> fmset G bs"
   proof (intro mset_wfactorsEx)
     fix X
-    assume "X \<in> set_mset (fmset G as #\<inter> fmset G bs)"
-    hence "X \<in> set_mset (fmset G as)" by (simp add: multiset_inter_def)
+    assume "X \<in># fmset G as #\<inter> fmset G bs"
+    hence "X \<in># fmset G as" by simp
     hence "X \<in> set (map (assocs G) as)" by (simp add: fmset_def)
     hence "\<exists>x. X = assocs G x \<and> x \<in> set as" by (induct as) auto
     from this obtain x
         where X: "X = assocs G x"
         and xas: "x \<in> set as"

 
   have "\<exists>c cs. c \<in> carrier G \<and> set cs \<subseteq> carrier G \<and> wfactors G cs c \<and> 
                fmset G cs = (fmset G as - fmset G bs) + fmset G bs"
   proof (intro mset_wfactorsEx)
     fix X
-    assume "X \<in> set_mset ((fmset G as - fmset G bs) + fmset G bs)"
-    hence "X \<in> set_mset (fmset G as) \<or> X \<in> set_mset (fmset G bs)"
-       by (cases "X :# fmset G bs", simp, simp)
+    assume "X \<in># (fmset G as - fmset G bs) + fmset G bs"
+    hence "X \<in># fmset G as \<or> X \<in># fmset G bs"
+      by (auto dest: in_diffD)
     moreover
     {
       assume "X \<in> set_mset (fmset G as)"
       hence "X \<in> set (map (assocs G) as)" by (simp add: fmset_def)
       hence "\<exists>x. x \<in> set as \<and> X = assocs G x" by (induct as) auto