1#[allow(unused_imports)]
2use super::multiset::Multiset;
3#[allow(unused_imports)]
4use super::prelude::*;
5
6verus! {
7
8broadcast use super::multiset::group_multiset_axioms;
9
10impl<A> Multiset<A> {
11 pub open spec fn is_empty(self) -> (b: bool) {
13 self.len() == 0
14 }
15
16 pub open spec fn is_singleton(self) -> bool {
18 &&& self.len() > 0
19 &&& (forall|x: A| self.contains(x) ==> self.count(x) == 1)
20 &&& (forall|x: A, y: A| self.contains(x) && self.contains(y) ==> x == y)
21 }
22
23 pub proof fn lemma_is_singleton_contains_elem_equal_singleton(self, x: A)
25 requires
26 self.is_singleton(),
27 self.contains(x),
28 ensures
29 self =~= Multiset::singleton(x),
30 {
31 assert forall|y: A| #[trigger] Multiset::singleton(x).count(y) == self.count(y) by {
32 if self.contains(y) {
33 } else {
34 }
35 };
36 }
37
38 pub proof fn lemma_singleton_size(self)
40 requires
41 self.is_singleton(),
42 ensures
43 self.len() == 1,
44 {
45 self.lemma_is_singleton_contains_elem_equal_singleton(self.choose());
46 }
47
48 pub proof fn lemma_is_singleton(s: Multiset<A>)
50 ensures
51 s.is_singleton() <==> (s.len() == 1),
52 {
53 if s.is_singleton() {
54 s.lemma_singleton_size();
55 }
56 if s.len() == 1 {
57 assert forall|x: A, y: A| s.contains(x) && s.contains(y) implies x == y by {
58 assert(s.remove(x).len() == 0);
59 if x != y {
60 assert(s.remove(x).count(y) == 0);
61 assert(s.remove(x).insert(x) =~= s);
62 }
63 }
64 }
65 }
66}
67
68}