Definition: set-sig
set-sig{i:l}(Item) ==
"set":{s:Type| valueall-type(Item) ⇒ valueall-type(s)}
"member":Item ⟶ self."set" ⟶ 𝔹
"empty":{s:self."set"| ∀x:Item. (¬↑(self."member" x s))}
"isEmpty":{f:self."set" ⟶ 𝔹| ∀s:self."set". (↑(f s) ⇐⇒ ∀x:Item. (¬↑(self."member" x s)))}
"singleton":{f:Item ⟶ self."set"| ∀x,y:Item. (↑(self."member" x (f y)) ⇐⇒ x = y ∈ Item)}
"add":{f:Item ⟶ self."set" ⟶ self."set"|
∀s:self."set". ∀x,y:Item. (↑(self."member" x (f y s)) ⇐⇒ (x = y ∈ Item) ∨ (↑(self."member" x s)))}
"union":{f:self."set" ⟶ self."set" ⟶ self."set"|
∀s1,s2:self."set". ∀x:Item.
(↑(self."member" x (f s1 s2)) ⇐⇒ (↑(self."member" x s1)) ∨ (↑(self."member" x s2)))}
"remove":{f:Item ⟶ self."set" ⟶ self."set"|
∀s:self."set". ∀x,y:Item. (↑(self."member" x (f y s)) ⇐⇒ (¬(x = y ∈ Item)) ∧ (↑(self."member" x s)))}
Lemma: set-sig_wf
∀[Item:Type]. (set-sig{i:l}(Item) ∈ 𝕌')
Definition: mk-set
mk-set(Item;set;member;empty;isEmpty;singleton;add;union;remove) ==
λx.x["set" := set]["member" := member]["empty" := empty]["isEmpty" := isEmpty]["singleton" := singleton]["add" := add]
["union" := union]["remove" := remove]
Lemma: mk-set_wf
∀[Item:Type]. ∀[set:{s:Type| valueall-type(Item) ⇒ valueall-type(s)} ]. ∀[member:Item ⟶ set ⟶ 𝔹].
∀[empty:{s:set| ∀x:Item. (¬↑(member x s))} ]. ∀[isEmpty:{f:set ⟶ 𝔹| ∀s:set. (↑(f s) ⇐⇒ ∀x:Item. (¬↑(member x s)))} ].
∀[singleton:{f:Item ⟶ set| ∀x,y:Item. (↑(member x (f y)) ⇐⇒ x = y ∈ Item)} ]. ∀[add:{f:Item ⟶ set ⟶ set|
∀s:set. ∀x,y:Item.
(↑(member x (f y s))
⇐⇒ (x = y ∈ Item)
∨ (↑(member x s)))} ].
∀[union:{f:set ⟶ set ⟶ set| ∀s1,s2:set. ∀x:Item. (↑(member x (f s1 s2)) ⇐⇒ (↑(member x s1)) ∨ (↑(member x s2)))} ].
∀[remove:{f:Item ⟶ set ⟶ set| ∀s:set. ∀x,y:Item. (↑(member x (f y s)) ⇐⇒ (¬(x = y ∈ Item)) ∧ (↑(member x s)))} ].
(mk-set(Item;set;member;empty;isEmpty;singleton;add;union;remove) ∈ set-sig{i:l}(Item))
Definition: set-sig-set
set-sig-set(s) == s."set"
Lemma: set-sig-set_wf
∀[Item:Type]. ∀[s:set-sig{i:l}(Item)]. (set-sig-set(s) ∈ Type)
Lemma: set-sig-set-squash
∀[Item:Type]. ∀[s:set-sig{i:l}(Item)]. (↓set-sig-set(s))
Lemma: set-sig-set-vatype
∀[Item:Type]. ∀[s:set-sig{i:l}(Item)]. valueall-type(set-sig-set(s)) supposing valueall-type(Item)
Definition: set-sig-member
set-sig-member(s) == s."member"
Lemma: set-sig-member_wf
∀[Item:Type]. ∀[s:set-sig{i:l}(Item)]. (set-sig-member(s) ∈ Item ⟶ set-sig-set(s) ⟶ 𝔹)
Definition: set-sig-empty
set-sig-empty(s) == s."empty"
Lemma: set-sig-empty_wf
∀[Item:Type]. ∀[s:set-sig{i:l}(Item)]. (set-sig-empty(s) ∈ set-sig-set(s))
Lemma: set-sig-empty-prop
∀[Item:Type]. ∀[s:set-sig{i:l}(Item)]. ∀[x:Item]. (¬↑(set-sig-member(s) x set-sig-empty(s)))
Lemma: set-sig-empty-prop2
∀[Item:Type]. ∀[s:set-sig{i:l}(Item)]. ∀[x:Item]. uiff(↑(set-sig-member(s) x set-sig-empty(s));False)
Definition: set-sig-isEmpty
set-sig-isEmpty(s) == s."isEmpty"
Lemma: set-sig-isEmpty_wf
∀[Item:Type]. ∀[s:set-sig{i:l}(Item)]. (set-sig-isEmpty(s) ∈ set-sig-set(s) ⟶ 𝔹)
Definition: set-sig-singleton
set-sig-singleton(s) == s."singleton"
Lemma: set-sig-singleton_wf
∀[Item:Type]. ∀[s:set-sig{i:l}(Item)]. (set-sig-singleton(s) ∈ Item ⟶ set-sig-set(s))
Definition: set-sig-add
set-sig-add(s) == s."add"
Lemma: set-sig-add_wf
∀[Item:Type]. ∀[s:set-sig{i:l}(Item)]. (set-sig-add(s) ∈ Item ⟶ set-sig-set(s) ⟶ set-sig-set(s))
Lemma: set-sig-add-prop
∀[Item:Type]
∀s:set-sig{i:l}(Item). ∀set:set-sig-set(s). ∀x,y:Item.
(↑(set-sig-member(s) x (set-sig-add(s) y set)) ⇐⇒ (x = y ∈ Item) ∨ (↑(set-sig-member(s) x set)))
Definition: set-sig-union
set-sig-union(s) == s."union"
Lemma: set-sig-union_wf
∀[Item:Type]. ∀[s:set-sig{i:l}(Item)]. (set-sig-union(s) ∈ set-sig-set(s) ⟶ set-sig-set(s) ⟶ set-sig-set(s))
Definition: set-sig-remove
set-sig-remove(s) == s."remove"
Lemma: set-sig-remove_wf
∀[Item:Type]. ∀[s:set-sig{i:l}(Item)]. (set-sig-remove(s) ∈ Item ⟶ set-sig-set(s) ⟶ set-sig-set(s))
Definition: in-missing
in-missing(i;missing) == reduce(λx,r. (x ≤z i ∧b ((x =z i) ∨br));ff;missing)
Lemma: in-missing_wf
∀[i:ℤ]. ∀[missing:ℤ List]. (in-missing(i;missing) ∈ 𝔹)
Lemma: assert-in-missing
∀i:ℤ. ∀missing:ℤ List. ((↑in-missing(i;missing)) ⇒ (i ∈ missing))
Lemma: assert-in-missing-iff
∀i:ℤ. ∀missing:{l:ℤ List| l-ordered(ℤ;x,y.x < y;l)} . (↑in-missing(i;missing) ⇐⇒ (i ∈ missing))
Lemma: assert-in-missing-nat
∀i:ℕ. ∀missing:ℕ List. ((↑in-missing(i;missing)) ⇒ (i ∈ missing))
Lemma: assert-in-missing-nat-iff
∀i:ℕ. ∀missing:{l:ℕ List| l-ordered(ℕ;x,y.x < y;l)} . (↑in-missing(i;missing) ⇐⇒ (i ∈ missing))
Definition: nat-missing-type
nat-missing-type() == m:{m:ℤ| (-1) ≤ m} × {L:ℕ List| l-ordered(ℕ;x,y.x < y;L) ∧ (∀x∈L.x < m)}
Lemma: nat-missing-type_wf
nat-missing-type() ∈ Type
Definition: member-nat-missing
member-nat-missing(i;s) == let max,missing = s in i ≤z max ∧b (¬bin-missing(i;missing))
Lemma: member-nat-missing_wf
∀[i:ℕ]. ∀[s:nat-missing-type()]. (member-nat-missing(i;s) ∈ 𝔹)
Lemma: assert-member-nat-missing
∀[i:ℕ]. ∀[s:nat-missing-type()]. (↑member-nat-missing(i;s) ⇐⇒ (i ≤ (fst(s))) ∧ (¬(i ∈ snd(s))))
Definition: empty-nat-missing
empty-nat-missing() == <-1, []>
Lemma: empty-nat-missing_wf
empty-nat-missing() ∈ nat-missing-type()
Lemma: empty-nat-missing-prop
∀x:ℕ. (¬↑member-nat-missing(x;empty-nat-missing()))
Definition: isEmpty-nat-missing
isEmpty-nat-missing(s) == let max,missing = s in max <z 0 ∧b null(missing)
Lemma: isEmpty-nat-missing_wf
∀[s:nat-missing-type()]. (isEmpty-nat-missing(s) ∈ 𝔹)
Lemma: isEmpty-nat-missing-prop
∀s:nat-missing-type(). (↑isEmpty-nat-missing(s) ⇐⇒ ∀x:ℕ. (¬↑member-nat-missing(x;s)))
Definition: singleton-nat-missing
singleton-nat-missing(i) == <i, [0, i)>
Lemma: singleton-nat-missing_wf
∀[i:ℕ]. (singleton-nat-missing(i) ∈ nat-missing-type())
Lemma: singleton-nat-missing-prop
∀x,y:ℕ. (↑member-nat-missing(x;singleton-nat-missing(y)) ⇐⇒ x = y ∈ ℕ)
Definition: add-nat-missing
add-nat-missing(i;s) ==
let max,missing = s
in if max <z i then <i, missing @ [max + 1, i)>
if (max =z i) then <max, missing>
else <max, remove-combine(λx.(x - i);missing)>
fi
Lemma: add-nat-missing_wf
∀[i:ℕ]. ∀[s:nat-missing-type()]. (add-nat-missing(i;s) ∈ nat-missing-type())
Lemma: add-nat-missing-prop
∀s:nat-missing-type(). ∀x,y:ℕ.
(↑member-nat-missing(x;add-nat-missing(y;s)) ⇐⇒ (x = y ∈ ℕ) ∨ (↑member-nat-missing(x;s)))
Definition: union-nat-missing-pos
union-nat-missing-pos(s1;max;missing) ==
primrec(max + 1;s1;λm,s. if in-missing(m;missing) then s else add-nat-missing(m;s) fi )
Lemma: union-nat-missing-pos_wf
∀[s1:nat-missing-type()]. ∀[max:ℕ]. ∀[missing:ℕ List]. (union-nat-missing-pos(s1;max;missing) ∈ nat-missing-type())
Lemma: union-nat-missing-pos-prop
∀s1:nat-missing-type(). ∀max:ℕ. ∀missing:{l:ℕ List| l-ordered(ℕ;x,y.x < y;l)} . ∀x:ℕ.
(↑member-nat-missing(x;union-nat-missing-pos(s1;max;missing))
⇐⇒ (↑member-nat-missing(x;s1)) ∨ ((x ≤ max) ∧ (¬(x ∈ missing))))
Definition: union-nat-missing
union-nat-missing(s1;s2) == let max,missing = s2 in if 0 ≤z max then union-nat-missing-pos(s1;max;missing) else s1 fi
Lemma: union-nat-missing_wf
∀[s1,s2:nat-missing-type()]. (union-nat-missing(s1;s2) ∈ nat-missing-type())
Lemma: union-nat-missing-prop
∀s1,s2:nat-missing-type(). ∀x:ℕ.
(↑member-nat-missing(x;union-nat-missing(s1;s2)) ⇐⇒ (↑member-nat-missing(x;s1)) ∨ (↑member-nat-missing(x;s2)))
Definition: select-last-in-nat-missing
select-last-in-nat-missing(max;missing) ==
primrec(max;if in-missing(0;missing) then -1 else 0 fi ;λm,r. if in-missing(m;missing) then r else m fi )
Lemma: select-last-in-nat-missing_wf
∀[max:ℕ]. ∀[missing:{l:ℕ List| l-ordered(ℕ;x,y.x < y;l)} ].
(select-last-in-nat-missing(max;missing) ∈ {x:ℤ|
((-1) ≤ x)
∧ (x ≤ max)
∧ ((0 ≤ x) ⇒ (¬(x ∈ missing)))
∧ (∀y:ℕ. ((¬(y ∈ missing)) ⇒ y < max ⇒ (y ≤ x)))
∧ (∀y:ℕ. (y < max ⇒ x < y ⇒ (y ∈ missing)))} )
Definition: remove-nat-missing
remove-nat-missing(i;s) ==
let max,missing = s
in if (i =z max)
then if null(missing)
then <max - 1, []>
else eval x = last(missing) in
if (x =z max - 1) then eval n = select-last-in-nat-missing(x;missing) in <n, filter(λx.x <z n;missing)>\000C else <max - 1, missing> fi
fi
if max <z i then <max, missing>
else <max, insert-combine(int-minus-comparison-inc(λx.x);λi,a. i;i;missing)>
fi
Lemma: remove-nat-missing_wf
∀[i:ℕ]. ∀[s:nat-missing-type()]. (remove-nat-missing(i;s) ∈ nat-missing-type())
Lemma: remove-nat-missing-prop
∀s:nat-missing-type(). ∀x,y:ℕ.
(↑member-nat-missing(x;remove-nat-missing(y;s)) ⇐⇒ (¬(x = y ∈ ℕ)) ∧ (↑member-nat-missing(x;s)))
Definition: mk-set-nat-missing
mk-set-nat-missing() ==
mk-set(ℕ;nat-missing-type();λi,s. member-nat-missing(i;s);empty-nat-missing();λs.isEmpty-nat-missing(s);
λi.singleton-nat-missing(i);λi,s. add-nat-missing(i;s);λs1,s2. union-nat-missing(s1;s2);λi,s. remove-nat-missin\000Cg(i;s))
Lemma: mk-set-nat-missing_wf
mk-set-nat-missing() ∈ set-sig{i:l}(ℕ)
Definition: map-sig
map-sig{i:l}(Key;Value) ==
"map":{m:Type| (valueall-type(m)) supposing (valueall-type(Value) and valueall-type(Key))}
"eqKey":EqDecider(Key)
"find":Key ⟶ self."map" ⟶ (Value?)
"inDom":{f:Key ⟶ self."map" ⟶ 𝔹| ∀k:Key. ∀m:self."map". (↑(f k m) ⇐⇒ ↑isl(self."find" k m))}
"empty":{m:self."map"| ∀k:Key. (¬↑(self."inDom" k m))}
"isEmpty":{f:self."map" ⟶ 𝔹| ∀m:self."map". (↑(f m) ⇐⇒ ∀k:Key. (¬↑(self."inDom" k m)))}
"update":{f:Key ⟶ Value ⟶ self."map" ⟶ self."map"|
∀m:self."map". ∀k1,k2:Key. ∀v:Value.
((self."find" k1 (f k2 v m)) = if self."eqKey" k1 k2 then inl v else self."find" k1 m fi ∈ (Value?))}
"add":{f:Key ⟶ Value ⟶ self."map" ⟶ self."map"|
∀m:self."map". ∀k1,k2:Key. ∀v:Value.
((self."find" k1 (f k2 v m))
= if (self."eqKey" k1 k2) ∧b (¬b(self."inDom" k2 m)) then inl v else self."find" k1 m fi
∈ (Value?))}
"remove":{f:Key ⟶ self."map" ⟶ self."map"|
∀m:self."map". ∀k1,k2:Key.
((self."find" k1 (f k2 m)) = if self."eqKey" k1 k2 then inr ⋅ else self."find" k1 m fi ∈ (Value?))}
Lemma: map-sig_wf
∀[Key,Value:Type]. (map-sig{i:l}(Key;Value) ∈ 𝕌')
Definition: mk-map
mk-map(Key;Value;map;eqKey;find;inDom;empty;isEmpty;update;add;remove) ==
λx.x["map" := map]["eqKey" := eqKey]["find" := find]["inDom" := inDom]["empty" := empty]["isEmpty" := isEmpty]
["update" := update]["add" := add]["remove" := remove]
Lemma: mk-map_wf
∀[Key,Value:Type]. ∀[map:{m:Type| (valueall-type(m)) supposing (valueall-type(Value) and valueall-type(Key))} ].
∀[eqKey:EqDecider(Key)]. ∀[find:Key ⟶ map ⟶ (Value?)]. ∀[inDom:{f:Key ⟶ map ⟶ 𝔹|
∀k:Key. ∀m:map. (↑(f k m) ⇐⇒ ↑isl(find k m))} ].
∀[empty:{m:map| ∀k:Key. (¬↑(inDom k m))} ]. ∀[isEmpty:{f:map ⟶ 𝔹| ∀m:map. (↑(f m) ⇐⇒ ∀k:Key. (¬↑(inDom k m)))} ].
∀[update:{f:Key ⟶ Value ⟶ map ⟶ map|
∀m:map. ∀k1,k2:Key. ∀v:Value.
((find k1 (f k2 v m)) = if eqKey k1 k2 then inl v else find k1 m fi ∈ (Value?))} ].
∀[add:{f:Key ⟶ Value ⟶ map ⟶ map|
∀m:map. ∀k1,k2:Key. ∀v:Value.
((find k1 (f k2 v m)) = if (eqKey k1 k2) ∧b (¬b(inDom k2 m)) then inl v else find k1 m fi ∈ (Value?))} ].
∀[remove:{f:Key ⟶ map ⟶ map|
∀m:map. ∀k1,k2:Key. ((find k1 (f k2 m)) = if eqKey k1 k2 then inr ⋅ else find k1 m fi ∈ (Value?))} ].
(mk-map(Key;Value;map;eqKey;find;inDom;empty;isEmpty;update;add;remove) ∈ map-sig{i:l}(Key;Value))
Definition: map-sig-map
map-sig-map(m) == m."map"
Lemma: map-sig-map_wf
∀[Key,Value:Type]. ∀[m:map-sig{i:l}(Key;Value)]. (map-sig-map(m) ∈ Type)
Lemma: map-sig-map-squash
∀[Key,Value:Type]. ∀[m:map-sig{i:l}(Key;Value)]. (↓map-sig-map(m))
Lemma: map-sig-map-vatype
∀[Key,Value:Type]. ∀[m:map-sig{i:l}(Key;Value)].
(valueall-type(map-sig-map(m))) supposing (valueall-type(Key) and valueall-type(Value))
Definition: map-sig-eqKey
map-sig-eqKey(m) == m."eqKey"
Lemma: map-sig-eqKey_wf
∀[Key,Value:Type]. ∀[m:map-sig{i:l}(Key;Value)]. (map-sig-eqKey(m) ∈ EqDecider(Key))
Definition: map-sig-find
map-sig-find(m) == m."find"
Lemma: map-sig-find_wf
∀[Key,Value:Type]. ∀[m:map-sig{i:l}(Key;Value)]. (map-sig-find(m) ∈ Key ⟶ map-sig-map(m) ⟶ (Value?))
Definition: map-sig-inDom
map-sig-inDom(m) == m."inDom"
Lemma: map-sig-inDom_wf
∀[Key,Value:Type]. ∀[m:map-sig{i:l}(Key;Value)]. (map-sig-inDom(m) ∈ Key ⟶ map-sig-map(m) ⟶ 𝔹)
Lemma: map-sig-inDom-prop
∀[Key,Value:Type]. ∀[ms:map-sig{i:l}(Key;Value)]. ∀[k:Key]. ∀[m:map-sig-map(ms)].
(↑(map-sig-inDom(ms) k m) ⇐⇒ ↑isl(map-sig-find(ms) k m))
Definition: map-sig-empty
map-sig-empty(m) == m."empty"
Lemma: map-sig-empty_wf
∀[Key,Value:Type]. ∀[m:map-sig{i:l}(Key;Value)]. (map-sig-empty(m) ∈ map-sig-map(m))
Definition: map-sig-isEmpty
map-sig-isEmpty(m) == m."isEmpty"
Lemma: map-sig-isEmpty_wf
∀[Key,Value:Type]. ∀[m:map-sig{i:l}(Key;Value)]. (map-sig-isEmpty(m) ∈ map-sig-map(m) ⟶ 𝔹)
Definition: map-sig-update
map-sig-update(m) == m."update"
Lemma: map-sig-update_wf
∀[Key,Value:Type]. ∀[m:map-sig{i:l}(Key;Value)]. (map-sig-update(m) ∈ Key ⟶ Value ⟶ map-sig-map(m) ⟶ map-sig-map(m))
Definition: map-sig-add
map-sig-add(m) == m."add"
Lemma: map-sig-add_wf
∀[Key,Value:Type]. ∀[m:map-sig{i:l}(Key;Value)]. (map-sig-add(m) ∈ Key ⟶ Value ⟶ map-sig-map(m) ⟶ map-sig-map(m))
Definition: map-sig-remove
map-sig-remove(m) == m."remove"
Lemma: map-sig-remove_wf
∀[Key,Value:Type]. ∀[m:map-sig{i:l}(Key;Value)]. (map-sig-remove(m) ∈ Key ⟶ map-sig-map(m) ⟶ map-sig-map(m))
Definition: int-decr-map-type
int-decr-map-type(Value) == {l:(ℤ × Value) List| l-ordered(ℤ × Value;x,y.(fst(x)) > (fst(y));l)}
Lemma: int-decr-map-type_wf
∀[Value:Type]. (int-decr-map-type(Value) ∈ Type)
Lemma: int-decr-map-fun
∀[Value:Type]. ∀[m:int-decr-map-type(Value)]. ∀[k:ℤ]. ∀[v1,v2:Value].
(v1 = v2 ∈ Value) supposing ((<k, v1> ∈ m) and (<k, v2> ∈ m))
Lemma: int-decr-map-type-member-sq-stable
∀[Value:Type]. ∀k:ℤ. ∀v:Value. ∀m:int-decr-map-type(Value). SqStable((<k, v> ∈ m))
Definition: int-decr-map-find
int-decr-map-find(k;m) == case find-combine(λp.(k - fst(p));m) of inl(x) => inl (snd(x)) | inr(x) => inr ⋅
Lemma: int-decr-map-find_wf
∀[Value:Type]. ∀[k:ℤ]. ∀[m:int-decr-map-type(Value)].
(int-decr-map-find(k;m) ∈ {v:Value| (¬↑null(m)) ∧ (<k, v> ∈ m)} + (↓(∀p∈m.¬(k = (fst(p)) ∈ ℤ))))
Lemma: int-decr-map-find-wf
∀[Value:Type]. ∀[k:ℤ]. ∀[m:int-decr-map-type(Value)]. (int-decr-map-find(k;m) ∈ Value?)
Lemma: int-decr-map-find-prop
∀[Value:Type]
∀k:ℤ. ∀m:int-decr-map-type(Value).
((↑isl(int-decr-map-find(k;m))) ⇒ ((¬↑null(m)) ∧ (<k, outl(int-decr-map-find(k;m))> ∈ m)))
Lemma: int-decr-map-find-prop2
∀[Value:Type]. ∀[k:ℤ]. ∀[m:int-decr-map-type(Value)].
(∀p∈m.¬(k = (fst(p)) ∈ ℤ)) supposing ¬↑isl(int-decr-map-find(k;m))
Lemma: int-decr-map-find-not-in
∀[Value:Type]. ∀[k:ℤ]. ∀[m:int-decr-map-type(Value)].
int-decr-map-find(k;m) = (inr ⋅ ) ∈ (Value?) supposing (∀p∈m.¬(k = (fst(p)) ∈ ℤ))
Definition: int-decr-map-inDom
int-decr-map-inDom(k;m) == isl(int-decr-map-find(k;m))
Lemma: int-decr-map-inDom_wf
∀[Value:Type]. ∀[k:ℤ]. ∀[m:int-decr-map-type(Value)]. (int-decr-map-inDom(k;m) ∈ 𝔹)
Lemma: int-decr-map-inDom-prop
∀[Value:Type]. ∀[k:ℤ]. ∀[m:int-decr-map-type(Value)]. (↑int-decr-map-inDom(k;m) ⇐⇒ ↑isl(int-decr-map-find(k;m)))
Lemma: int-decr-map-inDom-prop1
∀[Value:Type]
∀k:ℤ. ∀m:int-decr-map-type(Value).
(¬↑null(m)) ∧ (<k, outl(int-decr-map-find(k;m))> ∈ m) supposing ↑int-decr-map-inDom(k;m)
Lemma: int-decr-map-inDom-prop2
∀[Value:Type]. ∀[k:ℤ]. ∀[m:int-decr-map-type(Value)]. (∀p∈m.¬(k = (fst(p)) ∈ ℤ)) supposing ¬↑int-decr-map-inDom(k;m)
Lemma: int-decr-map-inDom-cons
∀[Value:Type]. ∀[k:ℤ]. ∀[u:ℤ × Value]. ∀[v:int-decr-map-type(Value)].
(k ≤ (fst(u))) supposing ((↑int-decr-map-inDom(k;[u / v])) and (∀y:ℤ × Value. ((y ∈ v) ⇒ ((fst(u)) > (fst(y))))))
Definition: int-decr-map-empty
int-decr-map-empty() == []
Lemma: int-decr-map-empty_wf
∀[Value:Type]. (int-decr-map-empty() ∈ int-decr-map-type(Value))
Lemma: int-decr-map-empty-prop
∀[Value:Type]. ∀[k:ℤ]. (¬↑int-decr-map-inDom(k;int-decr-map-empty()))
Definition: int-decr-map-isEmpty
int-decr-map-isEmpty(m) == null(m)
Lemma: int-decr-map-isEmpty_wf
∀[Value:Type]. ∀[m:int-decr-map-type(Value)]. (int-decr-map-isEmpty(m) ∈ 𝔹)
Lemma: int-decr-map-isEmpty-assert
∀[Value:Type]. ∀[m:int-decr-map-type(Value)].
uiff(↑int-decr-map-isEmpty(m);m = int-decr-map-empty() ∈ int-decr-map-type(Value))
Lemma: int-decr-map-isEmpty-prop
∀[Value:Type]. ∀[m:int-decr-map-type(Value)]. (↑int-decr-map-isEmpty(m) ⇐⇒ ∀k:ℤ. (¬↑int-decr-map-inDom(k;m)))
Definition: int-decr-map-update
int-decr-map-update(k;v;m) == insert-combine(int-minus-comparison(λp.(fst(p)));λx,a. x;<k, v>;m)
Lemma: int-decr-map-update_wf
∀[Value:Type]. ∀[k:ℤ]. ∀[v:Value]. ∀[m:int-decr-map-type(Value)].
(int-decr-map-update(k;v;m) ∈ int-decr-map-type(Value))
Lemma: int-decr-map-update-prop
∀[Value:Type]. ∀[m:int-decr-map-type(Value)]. ∀[k1,k2:ℤ]. ∀[v:Value].
(int-decr-map-find(k1;int-decr-map-update(k2;v;m))
= if (k1 =z k2) then inl v else int-decr-map-find(k1;m) fi
∈ (Value?))
Definition: int-decr-map-add
int-decr-map-add(k;v;m) == insert-combine(int-minus-comparison(λp.(fst(p)));λx,a. a;<k, v>;m)
Lemma: int-decr-map-add_wf
∀[Value:Type]. ∀[k:ℤ]. ∀[v:Value]. ∀[m:int-decr-map-type(Value)]. (int-decr-map-add(k;v;m) ∈ int-decr-map-type(Value))
Lemma: int-decr-map-add-prop
∀[Value:Type]. ∀[m:int-decr-map-type(Value)]. ∀[k1,k2:ℤ]. ∀[v:Value].
(int-decr-map-find(k1;int-decr-map-add(k2;v;m))
= if (k1 =z k2) ∧b (¬bint-decr-map-inDom(k2;m)) then inl v else int-decr-map-find(k1;m) fi
∈ (Value?))
Definition: int-decr-map-remove
int-decr-map-remove(k;m) == remove-combine(λp.(k - fst(p));m)
Lemma: int-decr-map-remove_wf
∀[Value:Type]. ∀[k:ℤ]. ∀[m:int-decr-map-type(Value)]. (int-decr-map-remove(k;m) ∈ int-decr-map-type(Value))
Lemma: int-decr-map-remove-prop
∀[Value:Type]. ∀[m:int-decr-map-type(Value)]. ∀[k1,k2:ℤ].
(int-decr-map-find(k1;int-decr-map-remove(k2;m))
= if (k1 =z k2) then inr ⋅ else int-decr-map-find(k1;m) fi
∈ (Value?))
Definition: mk-map-int-decr
mk-map-int-decr(Value) ==
mk-map(ℤ;Value;int-decr-map-type(Value);λx,y. (x =z y);λk,m. int-decr-map-find(k;m);λk,m. int-decr-map-inDom(k;m);
int-decr-map-empty();λm.int-decr-map-isEmpty(m);λk,v,m. int-decr-map-update(k;v;m);λk,v,m. int-decr-map-add(k;v\000C;m);
λk,m. int-decr-map-remove(k;m))
Lemma: mk-map-int-decr_wf
∀[Value:Type]. (mk-map-int-decr(Value) ∈ map-sig{i:l}(ℤ;Value))
Definition: lookup-list-map-type
lookup-list-map-type(Key;Value) == (Key × Value) List
Lemma: lookup-list-map-type_wf
∀[Key,Value:Type]. (lookup-list-map-type(Key;Value) ∈ Type)
Lemma: lookup-list-map-type-prop
∀[Key,Value:Type].
(valueall-type(lookup-list-map-type(Key;Value))) supposing (valueall-type(Value) and valueall-type(Key))
Definition: lookup-list-map-eqKey
lookup-list-map-eqKey(keyDeq) == keyDeq
Lemma: lookup-list-map-eqKey_wf
∀[Key:Type]. ∀[keyDeq:EqDecider(Key)]. (lookup-list-map-eqKey(keyDeq) ∈ EqDecider(Key))
Definition: lookup-list-map-find
lookup-list-map-find(deqKey;key;m) == apply-alist(deqKey;m;key)
Lemma: lookup-list-map-find_wf
∀[Key,Value:Type]. ∀[deqKey:EqDecider(Key)]. ∀[key:Key]. ∀[m:lookup-list-map-type(Key;Value)].
(lookup-list-map-find(deqKey;key;m) ∈ Value?)
Definition: lookup-list-map-inDom
lookup-list-map-inDom(deqKey;key;m) == rec-case(m) of [] => ff | h::t => r.let k,v = h in (deqKey key k) ∨br
Lemma: lookup-list-map-inDom_wf
∀[Key,Value:Type]. ∀[deqKey:EqDecider(Key)]. ∀[key:Key]. ∀[m:lookup-list-map-type(Key;Value)].
(lookup-list-map-inDom(deqKey;key;m) ∈ 𝔹)
Lemma: lookup-list-map-inDom-prop
∀[Key,Value:Type]. ∀[deqKey:EqDecider(Key)]. ∀[key:Key]. ∀[m:lookup-list-map-type(Key;Value)].
(↑lookup-list-map-inDom(deqKey;key;m) ⇐⇒ ↑isl(lookup-list-map-find(deqKey;key;m)))
Definition: lookup-list-map-empty
lookup-list-map-empty() == []
Lemma: lookup-list-map-empty_wf
∀[Key,Value:Type]. (lookup-list-map-empty() ∈ lookup-list-map-type(Key;Value))
Lemma: lookup-list-map-empty-prop
∀[Key:Type]. ∀[deqKey:EqDecider(Key)]. ∀[key:Key]. (¬↑lookup-list-map-inDom(deqKey;key;lookup-list-map-empty()))
Definition: lookup-list-map-isEmpty
lookup-list-map-isEmpty(m) == null(m)
Lemma: lookup-list-map-isEmpty_wf
∀[Key,Value:Type]. ∀[m:lookup-list-map-type(Key;Value)]. (lookup-list-map-isEmpty(m) ∈ 𝔹)
Lemma: lookup-list-map-isEmpty-prop
∀[Key,Value:Type]. ∀[deqKey:EqDecider(Key)]. ∀[m:lookup-list-map-type(Key;Value)].
(↑lookup-list-map-isEmpty(m) ⇐⇒ ∀k:Key. (¬↑lookup-list-map-inDom(deqKey;k;m)))
Definition: lookup-list-map-update
lookup-list-map-update(deqKey;key;val;m) == update-alist(deqKey;m;key;val;v.val)
Lemma: lookup-list-map-update_wf
∀[Key,Value:Type]. ∀[deqKey:EqDecider(Key)]. ∀[key:Key]. ∀[val:Value]. ∀[m:lookup-list-map-type(Key;Value)].
(lookup-list-map-update(deqKey;key;val;m) ∈ lookup-list-map-type(Key;Value))
Lemma: lookup-list-map-update-prop
∀[Key,Value:Type]. ∀[deqKey:EqDecider(Key)]. ∀[key2:Key]. ∀[val:Value]. ∀[m:lookup-list-map-type(Key;Value)].
∀[key1:Key].
(lookup-list-map-find(deqKey;key1;lookup-list-map-update(deqKey;key2;val;m))
= if deqKey key1 key2 then inl val else lookup-list-map-find(deqKey;key1;m) fi
∈ (Value?))
Definition: lookup-list-map-add
lookup-list-map-add(deqKey;key;val;m) == update-alist(deqKey;m;key;val;v.v)
Lemma: lookup-list-map-add_wf
∀[Key,Value:Type]. ∀[deqKey:EqDecider(Key)]. ∀[key:Key]. ∀[val:Value]. ∀[m:lookup-list-map-type(Key;Value)].
(lookup-list-map-add(deqKey;key;val;m) ∈ lookup-list-map-type(Key;Value))
Lemma: lookup-list-map-add-prop
∀[Key,Value:Type]. ∀[deqKey:EqDecider(Key)]. ∀[key2:Key]. ∀[val:Value]. ∀[m:lookup-list-map-type(Key;Value)].
∀[key1:Key].
(lookup-list-map-find(deqKey;key1;lookup-list-map-add(deqKey;key2;val;m))
= if (deqKey key1 key2) ∧b (¬blookup-list-map-inDom(deqKey;key2;m))
then inl val
else lookup-list-map-find(deqKey;key1;m)
fi
∈ (Value?))
Definition: lookup-list-map-remove
lookup-list-map-remove(deqKey;key;m) == remove-alist(deqKey;m;key)
Lemma: lookup-list-map-remove_wf
∀[Key,Value:Type]. ∀[deqKey:EqDecider(Key)]. ∀[key:Key]. ∀[m:lookup-list-map-type(Key;Value)].
(lookup-list-map-remove(deqKey;key;m) ∈ lookup-list-map-type(Key;Value))
Lemma: lookup-list-map-remove-prop
∀[Key,Value:Type]. ∀[deqKey:EqDecider(Key)]. ∀[key2:Key]. ∀[m:lookup-list-map-type(Key;Value)]. ∀[key1:Key].
(lookup-list-map-find(deqKey;key1;lookup-list-map-remove(deqKey;key2;m))
= if deqKey key1 key2 then inr ⋅ else lookup-list-map-find(deqKey;key1;m) fi
∈ (Value?))
Definition: mk-lookup-list-map
mk-lookup-list-map(Key;Value;deqKey) ==
mk-map(Key;Value;lookup-list-map-type(Key;Value);lookup-list-map-eqKey(deqKey);λk,m. lookup-list-map-find(deqKey;k;m);
λk,m. lookup-list-map-inDom(deqKey;k;m);lookup-list-map-empty();λm.lookup-list-map-isEmpty(m);
λk,v,m. lookup-list-map-update(deqKey;k;v;m);λk,v,m. lookup-list-map-add(deqKey;k;v;m);
λk,m. lookup-list-map-remove(deqKey;k;m))
Lemma: mk-lookup-list-map_wf
∀[Key,Value:Type]. ∀[deqKey:EqDecider(Key)]. (mk-lookup-list-map(Key;Value;deqKey) ∈ map-sig{i:l}(Key;Value))
Home
Index