equal
deleted
inserted
replaced
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_left_comm: fun_left_comm "op + o single o f" |
1601 interpretation image_left_comm: fun_left_comm "op + o single o f" |
1602 proof qed (simp add: add_ac) |
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 |
1607 lemma image_mset_single [simp]: "image_mset f {#x#} = {#f x#}" |
1607 lemma image_mset_single [simp]: "image_mset f {#x#} = {#f x#}" |