src/HOL/Algebra/Divisibility.thy

 
 
 subsubsection {* Interpreting multisets as factorizations *}
 
 lemma (in monoid) mset_fmsetEx:
-  assumes elems: "\<And>X. X \<in> set_of Cs \<Longrightarrow> \<exists>x. P x \<and> X = assocs G x"
+  assumes elems: "\<And>X. X \<in> set_mset Cs \<Longrightarrow> \<exists>x. P x \<and> X = assocs G x"
   shows "\<exists>cs. (\<forall>c \<in> set cs. P c) \<and> fmset G cs = Cs"
 proof -
   have "\<exists>Cs'. Cs = multiset_of Cs'"
       by (rule surjE[OF surj_multiset_of], fast)
   from this obtain Cs'

   qed
   thus ?thesis by (simp add: fmset_def)
 qed
 
 lemma (in monoid) mset_wfactorsEx:
-  assumes elems: "\<And>X. X \<in> set_of Cs 
+  assumes elems: "\<And>X. X \<in> set_mset Cs 
                       \<Longrightarrow> \<exists>x. (x \<in> carrier G \<and> irreducible G x) \<and> X = assocs G x"
   shows "\<exists>c cs. c \<in> carrier G \<and> set cs \<subseteq> carrier G \<and> wfactors G cs c \<and> fmset G cs = Cs"
 proof -
   have "\<exists>cs. (\<forall>c\<in>set cs. c \<in> carrier G \<and> irreducible G c) \<and> fmset G cs = Cs"
       by (intro mset_fmsetEx, rule elems)

   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_of (fmset G bs)" by simp
+    hence "X \<in> set_mset (fmset G bs)" by simp
     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_of (fmset G as #\<inter> fmset G bs)"
-    hence "X \<in> set_of (fmset G as)" by (simp add: multiset_inter_def)
+    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)
     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_of ((fmset G as - fmset G bs) + fmset G bs)"
-    hence "X \<in> set_of (fmset G as) \<or> X \<in> set_of (fmset G bs)"
+    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)
     moreover
     {
-      assume "X \<in> set_of (fmset G as)"
+      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
       from this obtain x
           where xas: "x \<in> set as"
           and X: "X = assocs G x" by auto

       from xcarr and xirr and X
           have "\<exists>x. (x \<in> carrier G \<and> irreducible G x) \<and> X = assocs G x" by fast
     }
     moreover
     {
-      assume "X \<in> set_of (fmset G bs)"
+      assume "X \<in> set_mset (fmset G bs)"
       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 as) auto
       from this obtain x
           where xbs: "x \<in> set bs"
           and X: "X = assocs G x" by auto