equal
deleted
inserted
replaced
1052 by (induct xs) (simp_all add: ac_simps) |
1052 by (induct xs) (simp_all add: ac_simps) |
1053 |
1053 |
1054 lemma mset_map: "mset (map f xs) = image_mset f (mset xs)" |
1054 lemma mset_map: "mset (map f xs) = image_mset f (mset xs)" |
1055 by (induct xs) simp_all |
1055 by (induct xs) simp_all |
1056 |
1056 |
1057 permanent_interpretation mset_set: folding "\<lambda>x M. {#x#} + M" "{#}" |
1057 global_interpretation mset_set: folding "\<lambda>x M. {#x#} + M" "{#}" |
1058 defines mset_set = "folding.F (\<lambda>x M. {#x#} + M) {#}" |
1058 defines mset_set = "folding.F (\<lambda>x M. {#x#} + M) {#}" |
1059 by standard (simp add: fun_eq_iff ac_simps) |
1059 by standard (simp add: fun_eq_iff ac_simps) |
1060 |
1060 |
1061 lemma count_mset_set [simp]: |
1061 lemma count_mset_set [simp]: |
1062 "finite A \<Longrightarrow> x \<in> A \<Longrightarrow> count (mset_set A) x = 1" (is "PROP ?P") |
1062 "finite A \<Longrightarrow> x \<in> A \<Longrightarrow> count (mset_set A) x = 1" (is "PROP ?P") |