equal
deleted
inserted
replaced
34 (** bag_of **) |
34 (** bag_of **) |
35 |
35 |
36 lemma bag_of_append [simp]: "bag_of (l@l') = bag_of l + bag_of l'" |
36 lemma bag_of_append [simp]: "bag_of (l@l') = bag_of l + bag_of l'" |
37 by (fact mset_append) |
37 by (fact mset_append) |
38 |
38 |
39 lemma subseteq_le_multiset: "A #\<subseteq># A + B" |
39 lemma subseteq_le_multiset: "(A :: 'a::order multiset) \<le> A + B" |
40 unfolding le_multiset_def apply (cases B; simp) |
40 unfolding less_eq_multiset_def apply (cases B; simp) |
41 apply (rule union_less_mono2[of "{#}" "_ + {#_#}" A, simplified]) |
41 apply (rule union_le_mono2[of "{#}" "_ + {#_#}" A, simplified]) |
42 apply (simp add: less_multiset\<^sub>H\<^sub>O) |
42 apply (simp add: less_multiset\<^sub>H\<^sub>O) |
43 done |
43 done |
44 |
44 |
45 lemma mono_bag_of: "mono (bag_of :: 'a list => ('a::order) multiset)" |
45 lemma mono_bag_of: "mono (bag_of :: 'a list => ('a::order) multiset)" |
46 apply (rule monoI) |
46 apply (rule monoI) |
47 apply (unfold prefix_def) |
47 apply (unfold prefix_def) |
48 apply (erule genPrefix.induct, simp_all add: add_right_mono) |
48 apply (erule genPrefix.induct, simp_all add: add_right_mono) |
49 apply (erule order_trans) |
49 apply (erule order_trans) |
50 apply (simp add: less_eq_multiset_def subseteq_le_multiset) |
50 apply (simp add: subseteq_le_multiset) |
51 done |
51 done |
52 |
52 |
53 (** setsum **) |
53 (** setsum **) |
54 |
54 |
55 declare setsum.cong [cong] |
55 declare setsum.cong [cong] |