src/HOL/Library/Multiset.thy
changeset 44339 eda6aef75939
parent 42871 1c0b99f950d9
child 44890 22f665a2e91c
equal deleted inserted replaced
44338:700008399ee5 44339:eda6aef75939
  1596 subsection {* Image *}
  1596 subsection {* Image *}
  1597 
  1597 
  1598 definition image_mset :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a multiset \<Rightarrow> 'b multiset" where
  1598 definition image_mset :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a multiset \<Rightarrow> 'b multiset" where
  1599   "image_mset f = fold_mset (op + o single o f) {#}"
  1599   "image_mset f = fold_mset (op + o single o f) {#}"
  1600 
  1600 
  1601 interpretation image_fun_commute: comp_fun_commute "op + o single o f"
  1601 interpretation image_fun_commute: comp_fun_commute "op + o single o f" for f
  1602 proof qed (simp add: add_ac fun_eq_iff)
  1602 proof qed (simp add: add_ac fun_eq_iff)
  1603 
  1603 
  1604 lemma image_mset_empty [simp]: "image_mset f {#} = {#}"
  1604 lemma image_mset_empty [simp]: "image_mset f {#} = {#}"
  1605 by (simp add: image_mset_def)
  1605 by (simp add: image_mset_def)
  1606 
  1606