From 442dceca5acb9ab93978d0173e850125288db6d5 Mon Sep 17 00:00:00 2001 From: rustanleino Date: Fri, 9 Jul 2010 03:10:43 +0000 Subject: Dafny: Axiom about inverting a set union operation, similar to the recent ones added for sequence concatenation. The new SeparationLogicList example profits from this axiom. --- Binaries/DafnyPrelude.bpl | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'Binaries') diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index eeb4f103..8d89715f 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -39,6 +39,10 @@ axiom (forall a, b: Set T, y: T :: { Set#Union(a, b), a[y] } a[y] ==> Set#Union(a, b)[y]); axiom (forall a, b: Set T, y: T :: { Set#Union(a, b), b[y] } b[y] ==> Set#Union(a, b)[y]); +axiom (forall a, b: Set T :: { Set#Union(a, b) } + Set#Disjoint(a, b) ==> + Set#Difference(Set#Union(a, b), a) == b && + Set#Difference(Set#Union(a, b), b) == a); function Set#Intersection(Set T, Set T) returns (Set T); axiom (forall a: Set T, b: Set T, o: T :: { Set#Intersection(a,b)[o] } -- cgit v1.2.3