From bcb9f9e189461258d9b50aee0565afe3b8c59e5c Mon Sep 17 00:00:00 2001 From: chrishaw Date: Thu, 26 Feb 2015 23:11:11 -0800 Subject: Add imap type, which is like map but may have have infinite size --- Binaries/DafnyPrelude.bpl | 49 ++++++++++++++++++++++++++++++++++++++++------- 1 file changed, 42 insertions(+), 7 deletions(-) (limited to 'Binaries') diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index 6ddff694..b88a0bdc 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -23,6 +23,7 @@ function TSet(Ty) : Ty; function TMultiSet(Ty) : Ty; function TSeq(Ty) : Ty; function TMap(Ty, Ty) : Ty; +function TIMap(Ty, Ty) : Ty; function Inv0_TSet(Ty) : Ty; axiom (forall t: Ty :: { TSet(t) } Inv0_TSet(TSet(t)) == t); @@ -878,13 +879,16 @@ axiom (forall u: U :: !Map#Domain(Map#Empty(): Map U V)[u]); axiom (forall m: Map U V :: { Map#Card(m) } Map#Card(m) == 0 <==> m == Map#Empty()); -function Map#Glue([U] bool, [U]V): Map U V; -axiom (forall a: [U] bool, b:[U]V :: - { Map#Domain(Map#Glue(a, b)) } - Map#Domain(Map#Glue(a, b)) == a); -axiom (forall a: [U] bool, b:[U]V :: - { Map#Elements(Map#Glue(a, b)) } - Map#Elements(Map#Glue(a, b)) == b); +function Map#Glue([U] bool, [U]V, Ty): Map U V; +axiom (forall a: [U] bool, b:[U]V, t:Ty :: + { Map#Domain(Map#Glue(a, b, t)) } + Map#Domain(Map#Glue(a, b, t)) == a); +axiom (forall a: [U] bool, b:[U]V, t:Ty :: + { Map#Elements(Map#Glue(a, b, t)) } + Map#Elements(Map#Glue(a, b, t)) == b); +axiom (forall a: [U] bool, b:[U]V, t:Ty :: + { $Is(Map#Glue(a, b, t), t) } + $Is(Map#Glue(a, b, t), t)); //Build is used in displays, and for map updates @@ -921,6 +925,37 @@ axiom (forall m: Map U V, m': Map U V :: { Map#Disjoint(m, m') } Map#Disjoint(m, m') <==> (forall o: U :: {Map#Domain(m)[o]} {Map#Domain(m')[o]} !Map#Domain(m)[o] || !Map#Domain(m')[o])); +// --------------------------------------------------------------- +// -- Axiomatization of IMaps ------------------------------------ +// --------------------------------------------------------------- + +type IMap U V; + +function IMap#Domain(IMap U V): [U] bool; +function IMap#Elements(IMap U V): [U]V; + +function IMap#Glue([U] bool, [U]V, Ty): IMap U V; +axiom (forall a: [U] bool, b:[U]V, t:Ty :: + { IMap#Domain(IMap#Glue(a, b, t)) } + IMap#Domain(IMap#Glue(a, b, t)) == a); +axiom (forall a: [U] bool, b:[U]V, t:Ty :: + { IMap#Elements(IMap#Glue(a, b, t)) } + IMap#Elements(IMap#Glue(a, b, t)) == b); +axiom (forall a: [U] bool, b:[U]V, t:Ty :: + { $Is(IMap#Glue(a, b, t), t) } + $Is(IMap#Glue(a, b, t), t)); + +//equality for imaps +function IMap#Equal(IMap U V, IMap U V): bool; +axiom (forall m: IMap U V, m': IMap U V:: + { IMap#Equal(m, m') } + IMap#Equal(m, m') <==> (forall u : U :: IMap#Domain(m)[u] == IMap#Domain(m')[u]) && + (forall u : U :: IMap#Domain(m)[u] ==> IMap#Elements(m)[u] == IMap#Elements(m')[u])); +// extensionality +axiom (forall m: IMap U V, m': IMap U V:: + { IMap#Equal(m, m') } + IMap#Equal(m, m') ==> m == m'); + // ------------------------------------------------------------------------- // -- Provide arithmetic wrappers to improve triggering and non-linear math // ------------------------------------------------------------------------- -- cgit v1.2.3