equal
deleted
inserted
replaced
86 lemma only1_in_multiset: "(\<lambda>b. if b = a then 1 else 0) \<in> multiset" |
86 lemma only1_in_multiset: "(\<lambda>b. if b = a then 1 else 0) \<in> multiset" |
87 by (simp add: multiset_def) |
87 by (simp add: multiset_def) |
88 |
88 |
89 lemma union_preserves_multiset: |
89 lemma union_preserves_multiset: |
90 "M \<in> multiset ==> N \<in> multiset ==> (\<lambda>a. M a + N a) \<in> multiset" |
90 "M \<in> multiset ==> N \<in> multiset ==> (\<lambda>a. M a + N a) \<in> multiset" |
91 apply (simp add: multiset_def) |
91 by (simp add: multiset_def) |
92 apply (drule (1) finite_UnI) |
92 |
93 apply (simp del: finite_Un add: Un_def) |
|
94 done |
|
95 |
93 |
96 lemma diff_preserves_multiset: |
94 lemma diff_preserves_multiset: |
97 "M \<in> multiset ==> (\<lambda>a. M a - N a) \<in> multiset" |
95 "M \<in> multiset ==> (\<lambda>a. M a - N a) \<in> multiset" |
98 apply (simp add: multiset_def) |
96 apply (simp add: multiset_def) |
99 apply (rule finite_subset) |
97 apply (rule finite_subset) |