equal
deleted
inserted
replaced
37 by (fact mset_append) |
37 by (fact mset_append) |
38 |
38 |
39 lemma subseteq_le_multiset: "(A :: 'a::order multiset) \<le> A + B" |
39 lemma subseteq_le_multiset: "(A :: 'a::order multiset) \<le> A + B" |
40 unfolding less_eq_multiset_def apply (cases B; simp) |
40 unfolding less_eq_multiset_def apply (cases B; simp) |
41 apply (rule union_le_mono2[of "{#}" "_ + {#_#}" A, simplified]) |
41 apply (rule union_le_mono2[of "{#}" "_ + {#_#}" A, simplified]) |
42 apply (simp add: less_multiset\<^sub>H\<^sub>O) |
|
43 done |
42 done |
44 |
43 |
45 lemma mono_bag_of: "mono (bag_of :: 'a list => ('a::order) multiset)" |
44 lemma mono_bag_of: "mono (bag_of :: 'a list => ('a::order) multiset)" |
46 apply (rule monoI) |
45 apply (rule monoI) |
47 apply (unfold prefix_def) |
46 apply (unfold prefix_def) |