equal
deleted
inserted
replaced
824 "image_mset f (M+N) = image_mset f M + image_mset f N" |
824 "image_mset f (M+N) = image_mset f M + image_mset f N" |
825 apply (induct N) |
825 apply (induct N) |
826 apply simp |
826 apply simp |
827 apply (simp add: add_assoc [symmetric] image_mset_insert) |
827 apply (simp add: add_assoc [symmetric] image_mset_insert) |
828 done |
828 done |
|
829 |
|
830 lemma set_of_image_mset [simp]: "set_of (image_mset f M) = image f (set_of M)" |
|
831 by (induct M) simp_all |
829 |
832 |
830 lemma size_image_mset [simp]: "size (image_mset f M) = size M" |
833 lemma size_image_mset [simp]: "size (image_mset f M) = size M" |
831 by (induct M) simp_all |
834 by (induct M) simp_all |
832 |
835 |
833 lemma image_mset_is_empty_iff [simp]: "image_mset f M = {#} \<longleftrightarrow> M = {#}" |
836 lemma image_mset_is_empty_iff [simp]: "image_mset f M = {#} \<longleftrightarrow> M = {#}" |