Partial implementation of multisets.

1 files changed, 103 insertions, 0 deletions

diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index dc152185..1a8bb027 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -84,6 +84,109 @@ function Set#Choose<T>(Set T, TickType): T;
 axiom (forall<T> a: Set T, tick: TickType :: { Set#Choose(a, tick) }

   a != Set#Empty() ==> a[Set#Choose(a, tick)]);

 

+

+// ---------------------------------------------------------------

+// -- Axiomatization of multisets --------------------------------

+// ---------------------------------------------------------------

+

+function Math#min(a: int, b: int): int;

+axiom (forall a: int, b: int :: { Math#min(a, b) } a <= b <==> Math#min(a, b) == a);

+axiom (forall a: int, b: int :: { Math#min(a, b) } b <= a <==> Math#min(a, b) == b);

+axiom (forall a: int, b: int :: { Math#min(a, b) } Math#min(a, b) == a || Math#min(a, b) == b);

+

+function Math#clip(a: int): int;

+axiom (forall a: int :: { Math#clip(a) } 0 <= a ==> Math#clip(a) == a);

+axiom (forall a: int :: { Math#clip(a) } a < 0  ==> Math#clip(a) == 0);

+

+type MultiSet T = [T]int;

+

+// ints are non-negative

+axiom (forall<T> o: T, ms: MultiSet T :: { ms[o] } 0 <= ms[o] );

+

+function MultiSet#Empty<T>(): MultiSet T;

+axiom (forall<T> o: T :: { MultiSet#Empty()[o] } MultiSet#Empty()[o] == 0);

+

+function MultiSet#Singleton<T>(T): MultiSet T;

+axiom (forall<T> r: T :: { MultiSet#Singleton(r) } MultiSet#Singleton(r)[r] == 1);

+axiom (forall<T> r: T, o: T :: { MultiSet#Singleton(r)[o] } (MultiSet#Singleton(r)[o] == 1 <==> r == o) &&

+                                                            (MultiSet#Singleton(r)[o] == 0 <==> r != o));

+

+function MultiSet#UnionOne<T>(MultiSet T, T): MultiSet T;

+// pure containment axiom (in the original multiset or is the added element)

+axiom (forall<T> a: MultiSet T, x: T, o: T :: { MultiSet#UnionOne(a,x)[o] }

+  0 < MultiSet#UnionOne(a,x)[o] <==> o == x || 0 < a[o]);

+// union-ing increases count by one

+axiom (forall<T> a: MultiSet T, x: T :: { MultiSet#UnionOne(a, x) }

+  MultiSet#UnionOne(a, x)[x] == a[x] + 1);

+// non-decreasing

+axiom (forall<T> a: MultiSet T, x: T, y: T :: { MultiSet#UnionOne(a, x), a[y] }

+  0 < a[y] ==> 0 < MultiSet#UnionOne(a, x)[y]);

+// other elements unchanged

+axiom (forall<T> a: MultiSet T, x: T, y: T :: { MultiSet#UnionOne(a, x), a[y] }

+  x != y ==> a[y] == MultiSet#UnionOne(a, x)[y]);

+

+function MultiSet#Union<T>(MultiSet T, MultiSet T): MultiSet T;

+// union-ing is the sum of the contents

+axiom (forall<T> a: MultiSet T, b: MultiSet T, o: T :: { MultiSet#Union(a,b)[o] }

+  MultiSet#Union(a,b)[o] == a[o] + b[o]);

+

+// two containment axioms

+axiom (forall<T> a, b: MultiSet T, y: T :: { MultiSet#Union(a, b), a[y] }

+  0 < a[y] ==> 0 < MultiSet#Union(a, b)[y]);

+axiom (forall<T> a, b: MultiSet T, y: T :: { MultiSet#Union(a, b), b[y] }

+  0 < b[y] ==> 0 < MultiSet#Union(a, b)[y]);

+

+// symmetry axiom

+axiom (forall<T> a, b: MultiSet T :: { MultiSet#Union(a, b) }

+  MultiSet#Disjoint(a, b) ==>

+    MultiSet#Difference(MultiSet#Union(a, b), a) == b &&

+    MultiSet#Difference(MultiSet#Union(a, b), b) == a);

+

+function MultiSet#Intersection<T>(MultiSet T, MultiSet T): MultiSet T;

+axiom (forall<T> a: MultiSet T, b: MultiSet T, o: T :: { MultiSet#Intersection(a,b)[o] }

+  MultiSet#Intersection(a,b)[o] == Math#min(a[o],  b[o]));

+

+// left and right pseudo-idempotence

+axiom (forall<T> a, b: MultiSet T :: { MultiSet#Intersection(MultiSet#Intersection(a, b), b) }

+  MultiSet#Intersection(MultiSet#Intersection(a, b), b) == MultiSet#Intersection(a, b));

+axiom (forall<T> a, b: MultiSet T :: { MultiSet#Intersection(a, MultiSet#Intersection(a, b)) }

+  MultiSet#Intersection(a, MultiSet#Intersection(a, b)) == MultiSet#Intersection(a, b));

+

+// multiset difference, a - b. clip() makes it positive.

+function MultiSet#Difference<T>(MultiSet T, MultiSet T): MultiSet T;

+axiom (forall<T> a: MultiSet T, b: MultiSet T, o: T :: { MultiSet#Difference(a,b)[o] }

+  MultiSet#Difference(a,b)[o] == Math#clip(a[o] - b[o]));

+axiom (forall<T> a, b: MultiSet T, y: T :: { MultiSet#Difference(a, b), b[y], a[y] }

+  a[y] <= b[y] ==> MultiSet#Difference(a, b)[y] == 0 );

+

+// multiset subset means a must have at most as many of each element as b

+function MultiSet#Subset<T>(MultiSet T, MultiSet T): bool;

+axiom(forall<T> a: MultiSet T, b: MultiSet T :: { MultiSet#Subset(a,b) }

+  MultiSet#Subset(a,b) <==> (forall o: T :: {a[o]} {b[o]} a[o] <= b[o]));

+

+function MultiSet#Equal<T>(MultiSet T, MultiSet T): bool;

+axiom(forall<T> a: MultiSet T, b: MultiSet T :: { MultiSet#Equal(a,b) }

+  MultiSet#Equal(a,b) <==> (forall o: T :: {a[o]} {b[o]} a[o] == b[o]));

+// extensionality axiom for multisets

+axiom(forall<T> a: MultiSet T, b: MultiSet T :: { MultiSet#Equal(a,b) }

+  MultiSet#Equal(a,b) ==> a == b);

+

+function MultiSet#Disjoint<T>(MultiSet T, MultiSet T): bool;

+axiom (forall<T> a: MultiSet T, b: MultiSet T :: { MultiSet#Disjoint(a,b) }

+  MultiSet#Disjoint(a,b) <==> (forall o: T :: {a[o]} {b[o]} a[o] == 0 || b[o] == 0));

+

+// conversion to a multiset. each element in the original set has duplicity 1.

+function MultiSet#FromSet<T>(Set T): MultiSet T;

+axiom (forall<T> s: Set T, a: T :: { MultiSet#FromSet(s)[a] }

+  MultiSet#FromSet(s)[a] == 0 <==> !s[a] &&

+  MultiSet#FromSet(s)[a] == 1 <==> s[a]);

+

+// avoiding this for now.

+//function Set#Choose<T>(Set T, TickType): T;

+//axiom (forall<T> a: Set T, tick: TickType :: { Set#Choose(a, tick) }

+//  a != Set#Empty() ==> a[Set#Choose(a, tick)]);

+

+

 // ---------------------------------------------------------------

 // -- Axiomatization of sequences --------------------------------

 // ---------------------------------------------------------------