equal
deleted
inserted
replaced
52 |
52 |
53 (** bag_of **) |
53 (** bag_of **) |
54 |
54 |
55 lemma bag_of_append [simp]: "bag_of (l@l') = bag_of l + bag_of l'" |
55 lemma bag_of_append [simp]: "bag_of (l@l') = bag_of l + bag_of l'" |
56 apply (induct_tac "l", simp) |
56 apply (induct_tac "l", simp) |
57 apply (simp add: plus_ac0) |
57 apply (simp add: add_ac) |
58 done |
58 done |
59 |
59 |
60 lemma mono_bag_of: "mono (bag_of :: 'a list => ('a::order) multiset)" |
60 lemma mono_bag_of: "mono (bag_of :: 'a list => ('a::order) multiset)" |
61 apply (rule monoI) |
61 apply (rule monoI) |
62 apply (unfold prefix_def) |
62 apply (unfold prefix_def) |
78 lemma bag_of_sublist: |
78 lemma bag_of_sublist: |
79 "bag_of (sublist l A) = |
79 "bag_of (sublist l A) = |
80 (\<Sum>i: A Int lessThan (length l). {# l!i #})" |
80 (\<Sum>i: A Int lessThan (length l). {# l!i #})" |
81 apply (rule_tac xs = l in rev_induct, simp) |
81 apply (rule_tac xs = l in rev_induct, simp) |
82 apply (simp add: sublist_append Int_insert_right lessThan_Suc nth_append |
82 apply (simp add: sublist_append Int_insert_right lessThan_Suc nth_append |
83 bag_of_sublist_lemma plus_ac0) |
83 bag_of_sublist_lemma add_ac) |
84 done |
84 done |
85 |
85 |
86 |
86 |
87 lemma bag_of_sublist_Un_Int: |
87 lemma bag_of_sublist_Un_Int: |
88 "bag_of (sublist l (A Un B)) + bag_of (sublist l (A Int B)) = |
88 "bag_of (sublist l (A Un B)) + bag_of (sublist l (A Int B)) = |