src/HOL/Library/Multiset.thy

 done
 
 lemma fold_mset_empty[simp]: "fold_mset f z {#} = z"
 unfolding fold_mset_def by blast
 
-context fun_left_comm
+context comp_fun_commute
 begin
 
 lemma fold_msetG_determ:
   "fold_msetG f z A x \<Longrightarrow> fold_msetG f z A y \<Longrightarrow> y = x"
 proof (induct arbitrary: x y z rule: full_multiset_induct)

     by (simp add: fold_mset_commute[of x,symmetric] add fold_mset_insert)
   finally show ?case .
 qed
 
 lemma fold_mset_fusion:
-  assumes "fun_left_comm g"
+  assumes "comp_fun_commute g"
   shows "(\<And>x y. h (g x y) = f x (h y)) \<Longrightarrow> h (fold_mset g w A) = fold_mset f (h w) A" (is "PROP ?P")
 proof -
-  interpret fun_left_comm g by (fact assms)
+  interpret comp_fun_commute g by (fact assms)
   show "PROP ?P" by (induct A) auto
 qed
 
 lemma fold_mset_rec:
   assumes "a \<in># A" 

 subsection {* Image *}
 
 definition image_mset :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a multiset \<Rightarrow> 'b multiset" where
   "image_mset f = fold_mset (op + o single o f) {#}"
 
-interpretation image_left_comm: fun_left_comm "op + o single o f"
+interpretation image_fun_commute: comp_fun_commute "op + o single o f"
 proof qed (simp add: add_ac fun_eq_iff)
 
 lemma image_mset_empty [simp]: "image_mset f {#} = {#}"
 by (simp add: image_mset_def)