Definition: bm_wt
bm_wt(i) == i + i + i
Lemma: bm_wt_wf
∀[i:ℤ]. (bm_wt(i) ∈ ℤ)
Definition: binary_mapco
binary_mapco(T;Key) ==
corec(X.lbl:Atom × if lbl =a "E" then Unit
if lbl =a "T" then key:Key × value:T × cnt:ℤ × left:X × X
else Void
fi )
Lemma: binary_mapco_wf
∀[T,Key:Type]. (binary_mapco(T;Key) ∈ Type)
Lemma: binary_mapco-ext
∀[T,Key:Type].
binary_mapco(T;Key) ≡ lbl:Atom × if lbl =a "E" then Unit
if lbl =a "T"
then key:Key × value:T × cnt:ℤ × left:binary_mapco(T;Key) × binary_mapco(T;Key)
else Void
fi
Definition: binary_mapco_size
binary_mapco_size(p) ==
fix((λsize,p. let lbl,x = p
in if lbl =a "E" then 0
if lbl =a "T" then let key,value,cnt,left,z = x in (1 + (size left)) + (size z)
else 0
fi ))
p
Lemma: binary_mapco_size_wf
∀[T,Key:Type]. ∀[p:binary_mapco(T;Key)]. (binary_mapco_size(p) ∈ partial(ℕ))
Definition: binary_map
binary_map(T;Key) == {p:binary_mapco(T;Key)| (binary_mapco_size(p))↓}
Lemma: binary_map_wf
∀[T,Key:Type]. (binary_map(T;Key) ∈ Type)
Definition: binary_map_size
binary_map_size(p) ==
fix((λsize,p. let lbl,x = p
in if lbl =a "E" then 0
if lbl =a "T" then let key,value,cnt,left,z = x in (1 + (size left)) + (size z)
else 0
fi ))
p
Lemma: binary_map_size_wf
∀[T,Key:Type]. ∀[p:binary_map(T;Key)]. (binary_map_size(p) ∈ ℕ)
Lemma: binary_map-ext
∀[T,Key:Type].
binary_map(T;Key) ≡ lbl:Atom × if lbl =a "E" then Unit
if lbl =a "T"
then key:Key × value:T × cnt:ℤ × left:binary_map(T;Key) × binary_map(T;Key)
else Void
fi
Definition: bm_E
bm_E() == <"E", ⋅>
Lemma: bm_E_wf
∀[T,Key:Type]. (bm_E() ∈ binary_map(T;Key))
Definition: bm_T
bm_T(key;value;cnt;left;right) == <"T", key, value, cnt, left, right>
Lemma: bm_T_wf
∀[T,Key:Type]. ∀[key:Key]. ∀[value:T]. ∀[cnt:ℤ]. ∀[left,right:binary_map(T;Key)].
(bm_T(key;value;cnt;left;right) ∈ binary_map(T;Key))
Definition: bm_E?
bm_E?(v) == fst(v) =a "E"
Lemma: bm_E?_wf
∀[T,Key:Type]. ∀[v:binary_map(T;Key)]. (bm_E?(v) ∈ 𝔹)
Definition: bm_T?
bm_T?(v) == fst(v) =a "T"
Lemma: bm_T?_wf
∀[T,Key:Type]. ∀[v:binary_map(T;Key)]. (bm_T?(v) ∈ 𝔹)
Definition: bm_T-key
bm_T-key(v) == fst(snd(v))
Lemma: bm_T-key_wf
∀[T,Key:Type]. ∀[v:binary_map(T;Key)]. bm_T-key(v) ∈ Key supposing ↑bm_T?(v)
Definition: bm_T-value
bm_T-value(v) == fst(snd(snd(v)))
Lemma: bm_T-value_wf
∀[T,Key:Type]. ∀[v:binary_map(T;Key)]. bm_T-value(v) ∈ T supposing ↑bm_T?(v)
Definition: bm_T-cnt
bm_T-cnt(v) == fst(snd(snd(snd(v))))
Lemma: bm_T-cnt_wf
∀[T,Key:Type]. ∀[v:binary_map(T;Key)]. bm_T-cnt(v) ∈ ℤ supposing ↑bm_T?(v)
Definition: bm_T-left
bm_T-left(v) == fst(snd(snd(snd(snd(v)))))
Lemma: bm_T-left_wf
∀[T,Key:Type]. ∀[v:binary_map(T;Key)]. bm_T-left(v) ∈ binary_map(T;Key) supposing ↑bm_T?(v)
Definition: bm_T-right
bm_T-right(v) == snd(snd(snd(snd(snd(v)))))
Lemma: bm_T-right_wf
∀[T,Key:Type]. ∀[v:binary_map(T;Key)]. bm_T-right(v) ∈ binary_map(T;Key) supposing ↑bm_T?(v)
Lemma: binary_map-induction
∀[T,Key:Type]. ∀[P:binary_map(T;Key) ⟶ ℙ].
(P[bm_E()]
⇒ (∀key:Key. ∀value:T. ∀cnt:ℤ. ∀left,right:binary_map(T;Key).
(P[left] ⇒ P[right] ⇒ P[bm_T(key;value;cnt;left;right)]))
⇒ {∀v:binary_map(T;Key). P[v]})
Lemma: binary_map-definition
∀[T,Key,A:Type]. ∀[R:A ⟶ binary_map(T;Key) ⟶ ℙ].
({x:A| R[x;bm_E()]}
⇒ (∀key:Key. ∀value:T. ∀cnt:ℤ. ∀left,right:binary_map(T;Key).
({x:A| R[x;left]} ⇒ {x:A| R[x;right]} ⇒ {x:A| R[x;bm_T(key;value;cnt;left;right)]} ))
⇒ {∀v:binary_map(T;Key). {x:A| R[x;v]} })
Definition: binary_map_ind
binary_map_ind(v;E;key,value,cnt,left,right,rec1,rec2.T[key;value;cnt;left;right;rec1;rec2]) ==
fix((λbinary_map_ind,v. let lbl,v1 = v
in if lbl="E" then E
if lbl="T"
then let key,v2 = v1
in let value,v3 = v2
in let cnt,v4 = v3
in let left,v5 = v4
in T[key;value;cnt;left;v5;binary_map_ind left;binary_map_ind v5]
else Ax
fi ))
v
Lemma: binary_map_ind_wf
∀[T,Key,A:Type]. ∀[R:A ⟶ binary_map(T;Key) ⟶ ℙ]. ∀[v:binary_map(T;Key)]. ∀[E:{x:A| R[x;bm_E()]} ].
∀[T:key:Key
⟶ value:T
⟶ cnt:ℤ
⟶ left:binary_map(T;Key)
⟶ right:binary_map(T;Key)
⟶ {x:A| R[x;left]}
⟶ {x:A| R[x;right]}
⟶ {x:A| R[x;bm_T(key;value;cnt;left;right)]} ].
(binary_map_ind(v;E;key,value,cnt,left,right,rec1,rec2.T[key;value;cnt;left;right;rec1;rec2]) ∈ {x:A| R[x;v]} )
Lemma: binary_map_ind_wf_simple
∀[T,Key,A:Type]. ∀[v:binary_map(T;Key)]. ∀[E:A]. ∀[T:key:Key
⟶ value:T
⟶ cnt:ℤ
⟶ left:binary_map(T;Key)
⟶ right:binary_map(T;Key)
⟶ A
⟶ A
⟶ A].
(binary_map_ind(v;E;key,value,cnt,left,right,rec1,rec2.T[key;value;cnt;left;right;rec1;rec2]) ∈ A)
Definition: binary_map_case
binary_map_case(m;E;key,value,cnt,left,right.F[key; value; cnt; left; right]) ==
binary_map_ind(m;E;key,value,cnt,left,right,_,__.F[key; value; cnt; left; right])
Lemma: binary_map_case_wf
∀[X,T,Key:Type]. ∀[x:binary_map(T;Key)]. ∀[E:X]. ∀[F:key:Key
⟶ value:T
⟶ cnt:ℤ
⟶ left:binary_map(T;Key)
⟶ right:binary_map(T;Key)
⟶ X].
(binary_map_case(x;E;key,value,cnt,left,right.F[key;value;cnt;left;right]) ∈ X)
Lemma: binary_map_case_T_reduce_lemma
∀F,E,right,left,cnt,value,key:Top.
(binary_map_case(bm_T(key;value;cnt;left;right);E;key,value,cnt,left,right.F[key;value;cnt;left;right])
~ F[key;value;cnt;left;right])
Lemma: binary_map_case_T
∀[key,value,cnt,left,right,E,F:Top].
(binary_map_case(bm_T(key;value;cnt;left;right);E;key,value,cnt,left,right.F[key;value;cnt;left;right])
~ F[key;value;cnt;left;right])
Lemma: binary_map_case_E_reduce_lemma
∀F,E:Top. (binary_map_case(bm_E();E;key,value,cnt,left,right.F[key;value;cnt;left;right]) ~ E)
Lemma: binary_map_case_E
∀[E,F:Top]. (binary_map_case(bm_E();E;key,value,cnt,left,right.F[key;value;cnt;left;right]) ~ E)
Definition: bm_cnt_prop0
bm_cnt_prop0(m) ==
binary_map_ind(m;<0, tt>;key,value,cnt,left,right,recL,recR.<cnt, (cnt =z 1 + (fst(recL)) + (fst(recR))) ∧b (snd(recL)\000C) ∧b (snd(recR))>)
Lemma: bm_cnt_prop0_wf
∀[T,Key:Type]. ∀[m:binary_map(T;Key)]. (bm_cnt_prop0(m) ∈ ℤ × 𝔹)
Lemma: bm_cnt_prop0_E_reduce_lemma
bm_cnt_prop0(bm_E()) ~ <0, tt>
Lemma: bm_cnt_prop0_E
bm_cnt_prop0(bm_E()) ~ <0, tt>
Lemma: bm_cnt_prop0_T
∀[key,value,cnt,left,right:Top].
(bm_cnt_prop0(bm_T(key;value;cnt;left;right)) ~ <cnt
, (cnt =z 1 + (fst(bm_cnt_prop0(left))) + (fst(bm_cnt_prop0(right))))
∧b (snd(bm_cnt_prop0(left)))
∧b (snd(bm_cnt_prop0(right)))
>)
Definition: bm_cnt_prop
bm_cnt_prop(m) == snd(bm_cnt_prop0(m))
Lemma: bm_cnt_prop_wf
∀[T,Key:Type]. ∀[m:binary_map(T;Key)]. (bm_cnt_prop(m) ∈ 𝔹)
Lemma: bm_cnt_prop_E_reduce_lemma
bm_cnt_prop(bm_E()) ~ tt
Lemma: bm_cnt_prop_E
bm_cnt_prop(bm_E()) ~ tt
Definition: binary-map
binary-map(T;Key) == {m:binary_map(T;Key)| ↑bm_cnt_prop(m)}
Lemma: binary-map_wf
∀[T,Key:Type]. (binary-map(T;Key) ∈ Type)
Definition: bm_empty
bm_empty() == bm_E()
Lemma: bm_empty_wf
∀[T,Key:Type]. (bm_empty() ∈ binary-map(T;Key))
Definition: bm_isEmpty
bm_isEmpty(m) == bm_E?(m)
Lemma: bm_isEmpty_wf
∀[T,Key:Type]. ∀[m:binary_map(T;Key)]. (bm_isEmpty(m) ∈ 𝔹)
Definition: bm_numItems
bm_numItems(m) == binary_map_case(m;0;key,value,cnt,left,right.cnt)
Lemma: bm_numItems_wf
∀[T,Key:Type]. ∀[m:binary_map(T;Key)]. (bm_numItems(m) ∈ ℤ)
Lemma: bm_numItems_E_reduce_lemma
bm_numItems(bm_E()) ~ 0
Lemma: bm_numItems_E
bm_numItems(bm_E()) ~ 0
Lemma: bm_numItems_T_reduce_lemma
∀right,left,cnt,value,key:Top. (bm_numItems(bm_T(key;value;cnt;left;right)) ~ cnt)
Lemma: bm_numItems_T
∀[key,value,cnt,left,right:Top]. (bm_numItems(bm_T(key;value;cnt;left;right)) ~ cnt)
Lemma: bm_numItems_is_cnt_prop0
∀[T,Key:Type]. ∀[m:binary_map(T;Key)]. (bm_numItems(m) ~ fst(bm_cnt_prop0(m)))
Lemma: bm_cnt_prop_T
∀[T,Key:Type]. ∀[key:Key]. ∀[value:T]. ∀[cnt:ℤ]. ∀[left,right:binary_map(T;Key)].
uiff(↑bm_cnt_prop(bm_T(key;value;cnt;left;right));(cnt = (1 + bm_numItems(left) + bm_numItems(right)) ∈ ℤ)
∧ (↑bm_cnt_prop(left))
∧ (↑bm_cnt_prop(right)))
Lemma: bm_E-wf2
∀[T,Key:Type]. (bm_E() ∈ binary-map(T;Key))
Lemma: bm_T-wf2
∀[T,Key:Type]. ∀[key:Key]. ∀[value:T]. ∀[cnt:ℤ]. ∀[left,right:binary-map(T;Key)].
bm_T(key;value;cnt;left;right) ∈ binary-map(T;Key) supposing cnt = (1 + bm_numItems(left) + bm_numItems(right)) ∈ ℤ
Lemma: binary_map_case-wf2
∀[X,T,Key:Type]. ∀[x:binary-map(T;Key)]. ∀[E:X]. ∀[F:key:Key
⟶ value:T
⟶ cnt:ℤ
⟶ left:binary-map(T;Key)
⟶ right:binary-map(T;Key)
⟶ X].
(binary_map_case(x;E;key,value,cnt,left,right.F[key;value;cnt;left;right]) ∈ X)
Lemma: binary_map_ind-wf2
∀[X,T,Key:Type]. ∀[x:binary-map(T;Key)]. ∀[E:X]. ∀[F:key:Key
⟶ value:T
⟶ cnt:ℤ
⟶ left:binary-map(T;Key)
⟶ right:binary-map(T;Key)
⟶ X
⟶ X
⟶ X].
(binary_map_ind(x;E;key,value,cnt,left,right,recL,recR.F[key;value;cnt;left;right;recL;recR]) ∈ X)
Definition: bm_count
bm_count(m) == binary_map_ind(m;0;key,value,cnt,left,right,recL,recR.1 + recL + recR)
Lemma: bm_count_wf
∀[T,Key:Type]. ∀[m:binary_map(T;Key)]. (bm_count(m) ∈ ℤ)
Lemma: bm_count_E_reduce_lemma
bm_count(bm_E()) ~ 0
Lemma: bm_count_E
bm_count(bm_E()) ~ 0
Lemma: bm_count_T
∀[key,value,cnt,left,right:Top]. (bm_count(bm_T(key;value;cnt;left;right)) ~ 1 + bm_count(left) + bm_count(right))
Lemma: bm_count_prop
∀[T,Key:Type]. ∀[m:binary_map(T;Key)]. bm_numItems(m) = bm_count(m) ∈ ℤ supposing ↑bm_cnt_prop(m)
Lemma: bm_count_prop_pos
∀[T,Key:Type]. ∀[m:binary_map(T;Key)]. (0 ≤ bm_count(m))
Lemma: bm_cnt_prop_pos
∀[T,Key:Type]. ∀[m:binary_map(T;Key)]. 0 ≤ bm_numItems(m) supposing ↑bm_cnt_prop(m)
Definition: bm_first
bm_first(m) ==
binary_map_ind(m;inr ⋅ ;key,value,cnt,left,right,rec1,rec2.if bm_isEmpty(left) then inl value else rec1 fi )
Lemma: bm_first_wf
∀[T,Key:Type]. ∀[m:binary_map(T;Key)]. (bm_first(m) ∈ T?)
Definition: bm_firsti
bm_firsti(m) ==
binary_map_ind(m;inr ⋅ ;key,value,cnt,left,right,rec1,rec2.if bm_isEmpty(left) then inl <key, value> else rec1 fi )
Lemma: bm_firsti_wf
∀[T,Key:Type]. ∀[m:binary_map(T;Key)]. (bm_firsti(m) ∈ Key × T?)
Definition: bm_N
bm_N(k;v;m1;m2) ==
binary_map_case(m1;binary_map_case(m2;bm_T(k;v;1;bm_E();bm_E());key,value,cnt,left,right.bm_T(k;v;1 + cnt;bm_E();m2));
key,value,cnt,left,right.binary_map_case(m2;bm_T(k;v;1 + cnt;m1;bm_E());key',value',cnt',left',right'.
bm_T(k;v;1 + cnt + cnt';m1;m2)))
Lemma: bm_N_wf
∀[T,Key:Type]. ∀[k:Key]. ∀[v:T]. ∀[m1,m2:binary-map(T;Key)]. (bm_N(k;v;m1;m2) ∈ binary-map(T;Key))
Definition: bm_single_L
bm_single_L(a;av;x;m) == binary_map_case(m;"error";key,value,cnt,left,right.bm_N(key;value;bm_N(a;av;x;left);right))
Lemma: bm_single_L_wf
∀[T,Key:Type]. ∀[a:Key]. ∀[av:T]. ∀[x,m:binary-map(T;Key)].
bm_single_L(a;av;x;m) ∈ binary-map(T;Key) supposing ↑bm_T?(m)
Definition: bm_single_R
bm_single_R(b;bv;m;z) == binary_map_case(m;"error";key,value,cnt,left,right.bm_N(key;value;left;bm_N(b;bv;right;z)))
Lemma: bm_single_R_wf
∀[T,Key:Type]. ∀[b:Key]. ∀[bv:T]. ∀[m,z:binary-map(T;Key)].
bm_single_R(b;bv;m;z) ∈ binary-map(T;Key) supposing ↑bm_T?(m)
Definition: bm_double_L
bm_double_L(a;av;w;m) ==
binary_map_case(m;"error";key,value,cnt,left,right.
binary_map_case(left;"error";key',value',cnt',left',right'.
bm_N(key';value';bm_N(a;av;w;left');bm_N(key';value';right';right))))
Lemma: bm_double_L_wf
∀[T,Key:Type]. ∀[a:Key]. ∀[av:T]. ∀[w,m:binary-map(T;Key)].
(bm_double_L(a;av;w;m) ∈ binary-map(T;Key)) supposing ((↑bm_T?(bm_T-left(m))) and (↑bm_T?(m)))
Definition: bm_double_R
bm_double_R(c;cv;m;z) ==
binary_map_case(m;"error";key,value,cnt,left,right.
binary_map_case(right;"error";key',value',cnt',left',right'.
bm_N(key';value';bm_N(key;value;left;left);bm_N(c;cv;right;z))))
Lemma: bm_double_R_wf
∀[T,Key:Type]. ∀[c:Key]. ∀[cv:T]. ∀[m,z:binary-map(T;Key)].
(bm_double_R(c;cv;m;z) ∈ binary-map(T;Key)) supposing ((↑bm_T?(bm_T-right(m))) and (↑bm_T?(m)))
Definition: bm_T'
bm_T'(k;v;m1;m2) ==
binary_map_case(m1;binary_map_case(m2;bm_T(k;v;1;bm_E();bm_E());key2,value2,cnt2,left2,right2.
binary_map_case(left2;binary_map_case(right2;bm_T(k;v;2;bm_E();m2);
key2r,value2r,cnt2r,left2r,right2r.
bm_single_L(k;v;m1;m2));
key2l,value2l,cnt2l,left2l,right2l.
binary_map_case(right2;bm_double_L(k;v;m1;m2);
key2r,value2r,cnt2r,left2r,right2r.
if cnt2l <z cnt2r
then bm_single_L(k;v;m1;m2)
else bm_double_L(k;v;m1;m2)
fi )));key1,value1,cnt1,left1,right1.
binary_map_case(m2;binary_map_case(left1;binary_map_case(right1;bm_T(k;v;2;m1;bm_E());
key1r,value1r,cnt1r,left1r,right1r.
bm_double_R(k;v;m1;m2));
key1l,value1l,cnt1l,left1l,right1l.
binary_map_case(right1;bm_single_R(k;v;m1;m2);
key1r,value1r,cnt1r,left1r,right1r.
if cnt1r <z cnt1l
then bm_single_R(k;v;m1;m2)
else bm_double_R(k;v;m1;m2)
fi ));key2,value2,cnt2,left2,right2.
if bm_wt(cnt1) ≤z cnt2
then if bm_numItems(left2) <z bm_numItems(right2)
then bm_single_L(k;v;m1;m2)
else bm_double_L(k;v;m1;m2)
fi
if bm_wt(cnt2) ≤z cnt1
then if bm_numItems(right1) <z bm_numItems(left1)
then bm_single_R(k;v;m1;m2)
else bm_double_R(k;v;m1;m2)
fi
else bm_T(k;v;cnt1 + cnt2 + 1;m1;m2)
fi ))
Lemma: bm_T'_wf
∀[T,Key:Type]. ∀[k:Key]. ∀[v:T]. ∀[m1,m2:binary-map(T;Key)]. (bm_T'(k;v;m1;m2) ∈ binary-map(T;Key))
Definition: bm_min
bm_min(m) ==
binary_map_ind(m;"error";key,value,cnt,left,right,recL,recR.binary_map_case(left;<key, value>;
keyL,valueL,cntL,leftL,rightL.recL))
Lemma: bm_min_wf
∀[T,Key:Type]. ∀[m:binary_map(T;Key)]. bm_min(m) ∈ Key × T supposing ↑bm_T?(m)
Definition: bm_delmin
bm_delmin(m) ==
binary_map_ind(m;"error";key,value,cnt,left,right,recL,recR.binary_map_case(left;right;keyL,valueL,cntL,leftL,rightL.
bm_T'(key;value;recL;right)))
Lemma: bm_delmin_wf
∀[T,Key:Type]. ∀[m:binary-map(T;Key)]. bm_delmin(m) ∈ binary-map(T;Key) supposing ↑bm_T?(m)
Definition: bm_delete'
bm_delete'(m1;m2) ==
binary_map_case(m1;m2;key1,value1,cnt1,left1,right1.binary_map_case(m2;m1;key2,value2,cnt2,left2,right2.
let mink,minv = bm_min(m2)
in bm_T'(mink;minv;m1;bm_delmin(m2))))
Lemma: bm_delete'_wf
∀[T,Key:Type]. ∀[m1,m2:binary-map(T;Key)]. (bm_delete'(m1;m2) ∈ binary-map(T;Key))
Definition: bm_singleton
bm_singleton(x;v) == bm_T(x;v;1;bm_E();bm_E())
Lemma: bm_singleton_wf
∀[T,Key:Type]. ∀[x:Key]. ∀[v:T]. (bm_singleton(x;v) ∈ binary-map(T;Key))
Definition: bm_compare
bm_compare(K) ==
{compare:K ⟶ K ⟶ ℤ|
Trans(K;x,y.0 ≤ (compare x y))
∧ AntiSym(K;x,y.0 ≤ (compare x y))
∧ Connex(K;x,y.0 ≤ (compare x y))
∧ Refl(K;x,y.(compare x y) = 0 ∈ ℤ)
∧ Sym(K;x,y.(compare x y) = 0 ∈ ℤ)}
Lemma: bm_compare_wf
∀[K:Type]. (bm_compare(K) ∈ Type)
Lemma: bm_compare_trans_le
∀[K:Type]. ∀[compare:bm_compare(K)]. ∀[k1,k2,k3:K].
((0 ≤ (compare k1 k2)) ⇒ (0 ≤ (compare k2 k3)) ⇒ (0 ≤ (compare k1 k3)))
Lemma: bm_compare_antisym_le
∀[K:Type]. ∀[compare:bm_compare(K)]. ∀[k1,k2:K]. ((0 ≤ (compare k1 k2)) ⇒ (0 ≤ (compare k2 k1)) ⇒ (k1 = k2 ∈ K))
Lemma: bm_compare_connex_le
∀[K:Type]. ∀compare:bm_compare(K). ∀k1,k2:K. ((0 ≤ (compare k1 k2)) ∨ (0 ≤ (compare k2 k1)))
Lemma: bm_compare_refl_le
∀[K:Type]. ∀[compare:bm_compare(K)]. ∀[k:K]. (0 ≤ (compare k k))
Lemma: bm_compare_refl_eq
∀[K:Type]. ∀[compare:bm_compare(K)]. ∀[k:K]. ((compare k k) = 0 ∈ ℤ)
Lemma: bm_compare_sym_eq
∀[K:Type]. ∀[compare:bm_compare(K)]. ∀[k1,k2:K]. (((compare k1 k2) = 0 ∈ ℤ) ⇒ ((compare k2 k1) = 0 ∈ ℤ))
Lemma: bm_compare_greater_greater_false
∀[K:Type]. ∀[compare:bm_compare(K)]. ∀[k1,k2:K]. (0 < compare k1 k2 ⇒ 0 < compare k2 k1 ⇒ False)
Lemma: bm_compare_greater_to_less_eq
∀[K:Type]. ∀[compare:bm_compare(K)]. ∀[k1,k2:K]. (0 < compare k1 k2 ⇒ ((compare k2 k1) ≤ 0))
Lemma: bm_compare_less_to_greater_eq
∀[K:Type]. ∀[compare:bm_compare(K)]. ∀[k1,k2:K]. (compare k1 k2 < 0 ⇒ (0 ≤ (compare k2 k1)))
Lemma: bm_compare_less_less_false
∀[K:Type]. ∀[compare:bm_compare(K)]. ∀[k1,k2:K]. (compare k1 k2 < 0 ⇒ compare k2 k1 < 0 ⇒ False)
Definition: bm_compare_int
bm_compare_int() == λn1,n2. if n1 <z n2 then -1 if (n1 =z n2) then 0 else 1 fi
Lemma: bm_compare_int_wf
bm_compare_int() ∈ bm_compare(ℤ)
Definition: bm_insert
bm_insert(compare;m;x;v) ==
binary_map_ind(m;bm_T(x;v;1;bm_E();bm_E());key,value,cnt,left,right,recL,recR.let c ⟵ compare key x
in if 0 <z c
then bm_T'(key;value;recL;right)
if c <z 0
then bm_T'(key;value;left;recR)
else bm_T(x;v;cnt;left;right)
fi )
Lemma: bm_insert_wf
∀[T,Key:Type]. ∀[compare:bm_compare(Key)]. ∀[m:binary-map(T;Key)]. ∀[x:Key]. ∀[v:T].
(bm_insert(compare;m;x;v) ∈ binary-map(T;Key))
Definition: bm_insert'
bm_insert'(compare;p;m) == let x,v = p in bm_insert(compare;m;x;v)
Lemma: bm_insert'_wf
∀[T,Key:Type]. ∀[compare:bm_compare(Key)]. ∀[p:Key × T]. ∀[m:binary-map(T;Key)].
(bm_insert'(compare;p;m) ∈ binary-map(T;Key))
Definition: bm_insert_if_not_in
bm_insert_if_not_in(compare;m;x;v) ==
binary_map_ind(m;bm_T(x;v;1;bm_E();bm_E());key,value,cnt,left,right,recL,recR.let c ⟵ compare key x
in if 0 <z c
then bm_T'(key;value;recL;right)
if c <z 0
then bm_T'(key;value;left;recR)
else bm_T(key;value;cnt;left;right)
fi )
Lemma: bm_insert_if_not_in_wf
∀[T,Key:Type]. ∀[compare:bm_compare(Key)]. ∀[m:binary-map(T;Key)]. ∀[x:Key]. ∀[v:T].
(bm_insert_if_not_in(compare;m;x;v) ∈ binary-map(T;Key))
Definition: bm_inDomain
bm_inDomain(compare;m;x) ==
binary_map_ind(m;ff;key,value,cnt,left,right,recL,recR.let c ⟵ compare x key
in if 0 <z c then recR
if c <z 0 then recL
else tt
fi )
Lemma: bm_inDomain_wf
∀[T,Key:Type]. ∀[compare:bm_compare(Key)]. ∀[x:Key]. ∀[m:binary-map(T;Key)]. (bm_inDomain(compare;m;x) ∈ 𝔹)
Definition: bm_find
bm_find(compare;m;x) ==
binary_map_ind(m;inr ⋅ ;key,value,cnt,left,right,recL,recR.let c ⟵ compare x key
in if 0 <z c then recR
if c <z 0 then recL
else inl value
fi )
Lemma: bm_find_wf
∀[T,Key:Type]. ∀[compare:bm_compare(Key)]. ∀[x:Key]. ∀[m:binary-map(T;Key)]. (bm_find(compare;m;x) ∈ T?)
Definition: bm_lookup
bm_lookup(compare;m;x) ==
binary_map_ind(m;"error";key,value,cnt,left,right,recL,recR.let c ⟵ compare x key
in if 0 <z c then recR
if c <z 0 then recL
else value
fi )
Lemma: bm_lookup_wf
∀[T,Key:Type]. ∀[compare:bm_compare(Key)]. ∀[x:Key]. ∀[m:binary-map(T;Key)].
bm_lookup(compare;m;x) ∈ T supposing ↑bm_inDomain(compare;m;x)
Definition: bm_exists
bm_exists(m;p) == binary_map_ind(m;ff;key,value,cnt,left,right,recL,recR.p[value] ∨brecL ∨brecR)
Lemma: bm_exists_wf
∀[T,Key:Type]. ∀[m:binary-map(T;Key)]. ∀[p:T ⟶ 𝔹]. (bm_exists(m;p) ∈ 𝔹)
Definition: bm_exists_downeq
bm_exists_downeq(compare;m;k;p) ==
binary_map_ind(m;ff;key,value,cnt,left,right,recL,recR.if 0 ≤z compare key k
then p[value] ∨bbm_exists(left;p) ∨brecR
else recL
fi )
Lemma: bm_exists_downeq_wf
∀[T,Key:Type]. ∀[compare:bm_compare(Key)]. ∀[m:binary-map(T;Key)]. ∀[k:Key]. ∀[p:T ⟶ 𝔹].
(bm_exists_downeq(compare;m;k;p) ∈ 𝔹)
Definition: bm_try_remove
bm_try_remove(compare;m;x) ==
binary_map_ind(m;<bm_E(), inr ⋅ >;key,value,cnt,left,right,recL,recR.eval c = compare key x in
if 0 <z c
then let left',v = recL
in <bm_T'(key;value;left';right), v>
if c <z 0
then let right',v = recR
in <bm_T'(key;value;left;right'), v>
else <bm_delete'(left;right), inl value>
fi )
Lemma: bm_try_remove_wf
∀[T,Key:Type]. ∀[compare:bm_compare(Key)]. ∀[x:Key]. ∀[m:binary-map(T;Key)].
(bm_try_remove(compare;m;x) ∈ binary-map(T;Key) × (T?))
Definition: bm_remove
bm_remove(compare;m;x) ==
binary_map_ind(m;"error";key,value,cnt,left,right,recL,recR.let c ⟵ compare key x
in if 0 <z c
then let left',v = recL
in <bm_T'(key;value;left';right), v>
if c <z 0
then let right',v = recR
in <bm_T'(key;value;left;right'), v>
else <bm_delete'(left;right), value>
fi )
Lemma: bm_remove_wf
∀[T,Key:Type]. ∀[compare:bm_compare(Key)]. ∀[x:Key]. ∀[m:binary-map(T;Key)].
bm_remove(compare;m;x) ∈ binary-map(T;Key) × T supposing ↑bm_inDomain(compare;m;x)
Definition: bm_listItems_d2l
bm_listItems_d2l(m) == binary_map_ind(m;λl.l;key,value,cnt,left,right,recL,recR.λl.(recL [value / (recR l)]))
Lemma: bm_listItems_d2l_wf
∀[T,Key:Type]. ∀[m:binary-map(T;Key)]. (bm_listItems_d2l(m) ∈ (T List) ⟶ (T List))
Definition: bm_listItems
bm_listItems(m) == bm_listItems_d2l(m) []
Lemma: bm_listItems_wf
∀[T,Key:Type]. ∀[m:binary-map(T;Key)]. (bm_listItems(m) ∈ T List)
Definition: bm_listItemsi_d2l
bm_listItemsi_d2l(m) == binary_map_ind(m;λl.l;key,value,cnt,left,right,recL,recR.λl.(recL [<key, value> / (recR l)]))
Lemma: bm_listItemsi_d2l_wf
∀[T,Key:Type]. ∀[m:binary-map(T;Key)]. (bm_listItemsi_d2l(m) ∈ ((Key × T) List) ⟶ ((Key × T) List))
Definition: bm_listItemsi
bm_listItemsi(m) == bm_listItemsi_d2l(m) []
Lemma: bm_listItemsi_wf
∀[T,Key:Type]. ∀[m:binary-map(T;Key)]. (bm_listItemsi(m) ∈ (Key × T) List)
Definition: bm_listKeys_d2l
bm_listKeys_d2l(m) == binary_map_ind(m;λl.l;key,value,cnt,left,right,recL,recR.λl.(recL [key / (recR l)]))
Lemma: bm_listKeys_d2l_wf
∀[T,Key:Type]. ∀[m:binary-map(T;Key)]. (bm_listKeys_d2l(m) ∈ (Key List) ⟶ (Key List))
Definition: bm_listKeys
bm_listKeys(m) == bm_listKeys_d2l(m) []
Lemma: bm_listKeys_wf
∀[T,Key:Type]. ∀[m:binary-map(T;Key)]. (bm_listKeys(m) ∈ Key List)
Definition: bm_collate_left
bm_collate_left(m) ==
binary_map_ind(m;λrest.rest;key,value,cnt,left,right,recL,recR.λrest.(recL [bm_T(key;value;cnt;left;right) / rest]))
Lemma: bm_collate_left_wf
∀[T,Key:Type]. ∀[m:binary-map(T;Key)]. (bm_collate_left(m) ∈ (binary-map(T;Key) List) ⟶ (binary-map(T;Key) List))
Definition: bm_collate_next
bm_collate_next(l) ==
rec-case(l) of
[] => <bm_E(), []>
t::rest =>
z.binary_map_case(t;<bm_E(), []>;key,value,cnt,left,right.<t, bm_collate_left(right) rest>)
Lemma: bm_collate_next_wf
∀[T,Key:Type]. ∀[l:binary-map(T;Key) List]. (bm_collate_next(l) ∈ binary-map(T;Key) × (binary-map(T;Key) List))
Definition: bm_mapi
bm_mapi(f;m) == binary_map_ind(m;bm_E();key,value,cnt,left,right,recL,recR.bm_T(key;f key value;cnt;recL;recR))
Lemma: bm_mapi_wf
∀[T,Key:Type]. ∀[f:Key ⟶ T ⟶ T]. ∀[m:binary-map(T;Key)]. (bm_mapi(f;m) ∈ binary-map(T;Key))
Definition: bm_map
bm_map(f;m) == bm_mapi(λk.f;m)
Lemma: bm_map_wf
∀[T,Key:Type]. ∀[f:T ⟶ T]. ∀[m:binary-map(T;Key)]. (bm_map(f;m) ∈ binary-map(T;Key))
Definition: bm_foldli_aux
bm_foldli_aux(f;m) == binary_map_ind(m;λv.v;key,value,cnt,left,right,recL,recR.λv.(recR (f key value (recL v))))
Lemma: bm_foldli_aux_wf
∀[T,U,Key:Type]. ∀[f:Key ⟶ T ⟶ U ⟶ U]. ∀[m:binary-map(T;Key)]. (bm_foldli_aux(f;m) ∈ U ⟶ U)
Definition: bm_foldli
bm_foldli(f;init;m) == bm_foldli_aux(f;m) init
Lemma: bm_foldli_wf
∀[T,U,Key:Type]. ∀[f:Key ⟶ T ⟶ U ⟶ U]. ∀[m:binary-map(T;Key)]. ∀[init:U]. (bm_foldli(f;init;m) ∈ U)
Definition: bm_foldl
bm_foldl(f;init;m) == bm_foldli(λk,v,a. (f v a);init;m)
Lemma: bm_foldl_wf
∀[T,U,Key:Type]. ∀[f:T ⟶ U ⟶ U]. ∀[m:binary-map(T;Key)]. ∀[init:U]. (bm_foldl(f;init;m) ∈ U)
Definition: bm_unionWith_ins
bm_unionWith_ins(compare;f;key;x;m) ==
case bm_find(compare;m;key) of inl(x') => bm_insert(compare;m;key;f x x') | inr(y) => bm_insert(compare;m;key;x)
Lemma: bm_unionWith_ins_wf
∀[T,Key:Type]. ∀[compare:bm_compare(Key)]. ∀[key:Key]. ∀[x:T]. ∀[m:binary-map(T;Key)]. ∀[f:T ⟶ T ⟶ T].
(bm_unionWith_ins(compare;f;key;x;m) ∈ binary-map(T;Key))
Definition: bm_unionWith
bm_unionWith(compare;f;m1;m2) ==
if bm_numItems(m2) <z bm_numItems(m1)
then bm_foldli(λk,v,a. bm_unionWith_ins(compare;f;k;v;a);m1;m2)
else bm_foldli(λk,v,a. bm_unionWith_ins(compare;λx1,x2. (f x2 x1);k;v;a);m2;m1)
fi
Lemma: bm_unionWith_wf
∀[T,Key:Type]. ∀[compare:bm_compare(Key)]. ∀[m1,m2:binary-map(T;Key)]. ∀[f:T ⟶ T ⟶ T].
(bm_unionWith(compare;f;m1;m2) ∈ binary-map(T;Key))
Home
Index