src/HOL/Library/Multiset.thy
changeset 42871 1c0b99f950d9
parent 42809 5b45125b15ba
child 44339 eda6aef75939
     1.1 --- a/src/HOL/Library/Multiset.thy	Fri May 20 08:16:56 2011 +0200
     1.2 +++ b/src/HOL/Library/Multiset.thy	Fri May 20 11:44:16 2011 +0200
     1.3 @@ -1457,7 +1457,7 @@
     1.4  lemma fold_mset_empty[simp]: "fold_mset f z {#} = z"
     1.5  unfolding fold_mset_def by blast
     1.6  
     1.7 -context fun_left_comm
     1.8 +context comp_fun_commute
     1.9  begin
    1.10  
    1.11  lemma fold_msetG_determ:
    1.12 @@ -1563,10 +1563,10 @@
    1.13  qed
    1.14  
    1.15  lemma fold_mset_fusion:
    1.16 -  assumes "fun_left_comm g"
    1.17 +  assumes "comp_fun_commute g"
    1.18    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")
    1.19  proof -
    1.20 -  interpret fun_left_comm g by (fact assms)
    1.21 +  interpret comp_fun_commute g by (fact assms)
    1.22    show "PROP ?P" by (induct A) auto
    1.23  qed
    1.24  
    1.25 @@ -1598,7 +1598,7 @@
    1.26  definition image_mset :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a multiset \<Rightarrow> 'b multiset" where
    1.27    "image_mset f = fold_mset (op + o single o f) {#}"
    1.28  
    1.29 -interpretation image_left_comm: fun_left_comm "op + o single o f"
    1.30 +interpretation image_fun_commute: comp_fun_commute "op + o single o f"
    1.31  proof qed (simp add: add_ac fun_eq_iff)
    1.32  
    1.33  lemma image_mset_empty [simp]: "image_mset f {#} = {#}"