From f72015819c90a23b150b1d70147eb51c51e2d5ed Mon Sep 17 00:00:00 2001 From: Jason Koenig Date: Mon, 11 Jul 2011 15:33:45 -0700 Subject: Partial implementation of multisets. --- Binaries/DafnyPrelude.bpl | 103 ++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 103 insertions(+) (limited to 'Binaries') 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(Set T, TickType): T; axiom (forall 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 o: T, ms: MultiSet T :: { ms[o] } 0 <= ms[o] ); + +function MultiSet#Empty(): MultiSet T; +axiom (forall o: T :: { MultiSet#Empty()[o] } MultiSet#Empty()[o] == 0); + +function MultiSet#Singleton(T): MultiSet T; +axiom (forall r: T :: { MultiSet#Singleton(r) } MultiSet#Singleton(r)[r] == 1); +axiom (forall 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(MultiSet T, T): MultiSet T; +// pure containment axiom (in the original multiset or is the added element) +axiom (forall 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 a: MultiSet T, x: T :: { MultiSet#UnionOne(a, x) } + MultiSet#UnionOne(a, x)[x] == a[x] + 1); +// non-decreasing +axiom (forall 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 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(MultiSet T, MultiSet T): MultiSet T; +// union-ing is the sum of the contents +axiom (forall 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 a, b: MultiSet T, y: T :: { MultiSet#Union(a, b), a[y] } + 0 < a[y] ==> 0 < MultiSet#Union(a, b)[y]); +axiom (forall 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 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(MultiSet T, MultiSet T): MultiSet T; +axiom (forall 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 a, b: MultiSet T :: { MultiSet#Intersection(MultiSet#Intersection(a, b), b) } + MultiSet#Intersection(MultiSet#Intersection(a, b), b) == MultiSet#Intersection(a, b)); +axiom (forall 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(MultiSet T, MultiSet T): MultiSet T; +axiom (forall 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 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(MultiSet T, MultiSet T): bool; +axiom(forall 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(MultiSet T, MultiSet T): bool; +axiom(forall 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 a: MultiSet T, b: MultiSet T :: { MultiSet#Equal(a,b) } + MultiSet#Equal(a,b) ==> a == b); + +function MultiSet#Disjoint(MultiSet T, MultiSet T): bool; +axiom (forall 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(Set T): MultiSet T; +axiom (forall 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(Set T, TickType): T; +//axiom (forall a: Set T, tick: TickType :: { Set#Choose(a, tick) } +// a != Set#Empty() ==> a[Set#Choose(a, tick)]); + + // --------------------------------------------------------------- // -- Axiomatization of sequences -------------------------------- // --------------------------------------------------------------- -- cgit v1.2.3