From a90615dc6e2673b591e154e59cd7f04e1ff90563 Mon Sep 17 00:00:00 2001
From: Jason Koenig <unknown>
Date: Mon, 11 Jul 2011 19:43:42 -0700
Subject: Multiset forming operators added.

---
 Binaries/DafnyPrelude.bpl | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

(limited to 'Binaries')

diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index 1a8bb027..e11acf26 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -100,8 +100,10 @@ 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 $IsGoodMultiSet<T>(ms: MultiSet T): bool;
+// ints are non-negative, used after havocing.
+axiom (forall<T> ms: MultiSet T :: { $IsGoodMultiSet(ms) } 
+     $IsGoodMultiSet(ms) <==> (forall o: T :: { ms[o] } 0 <= ms[o]));
 
 function MultiSet#Empty<T>(): MultiSet T;
 axiom (forall<T> o: T :: { MultiSet#Empty()[o] } MultiSet#Empty()[o] == 0);
@@ -178,14 +180,12 @@ axiom (forall<T> a: MultiSet T, b: MultiSet T :: { MultiSet#Disjoint(a,b) }
 // 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)]);
+  (MultiSet#FromSet(s)[a] == 0 <==> !s[a]) &&
+  (MultiSet#FromSet(s)[a] == 1 <==> s[a]));
 
+// conversion to a multiset. each element in the original set has duplicity 1.
+function MultiSet#FromSeq<T>(Seq T): MultiSet T;
+// no axioms yet.
 
 // ---------------------------------------------------------------
 // -- Axiomatization of sequences --------------------------------
-- 
cgit v1.2.3