Nuprl 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))
Proof
Definitions occuring in Statement :
mk-map: mk-map(Key;Value;map;eqKey;find;inDom;empty;isEmpty;update;add;remove),
map-sig: map-sig{i:l}(Key;Value),
deq: EqDecider(T),
band: p ∧b q,
valueall-type: valueall-type(T),
bnot: ¬bb,
assert: ↑b,
ifthenelse: if b then t else f fi ,
isl: isl(x),
bool: 𝔹,
it: ⋅,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
not: ¬A,
unit: Unit,
member: t ∈ T,
set: {x:A| B[x]} ,
apply: f a,
function: x:A ─→ B[x],
inr: inr x ,
inl: inl x,
union: left + right,
universe: Type,
equal: s = t ∈ T
Lemmas :
eq_atom_wf,
uiff_transitivity,
equal-wf-base,
atom_subtype_base,
assert_wf,
eqtt_to_assert,
assert_of_eq_atom,
subtype_base_sq,
rec_select_update_lemma,
iff_transitivity,
bnot_wf,
not_wf,
iff_weakening_uiff,
eqff_to_assert,
assert_of_bnot,
bool_wf,
set_wf,
all_wf,
equal_wf,
unit_wf2,
safe-assert-deq,
it_wf,
bool_cases_sqequal,
bool_subtype_base,
assert-bnot,
eqof_wf,
assert_of_band,
iff_wf,
isl_wf,
deq_wf,
valueall-type_wf
\mforall{}[Key,Value:Type]. \mforall{}[map:\{m:Type|
(valueall-type(m)) supposing (valueall-type(Value) and valueall-type(Key))\000C\} ].
\mforall{}[eqKey:EqDecider(Key)]. \mforall{}[find:Key {}\mrightarrow{} map {}\mrightarrow{} (Value?)]. \mforall{}[inDom:\{f:Key {}\mrightarrow{} map {}\mrightarrow{} \mBbbB{}|
\mforall{}k:Key. \mforall{}m:map.
(\muparrow{}(f k m) \mLeftarrow{}{}\mRightarrow{} \muparrow{}isl(find k m))\} ]\000C.
\mforall{}[empty:\{m:map| \mforall{}k:Key. (\mneg{}\muparrow{}(inDom k m))\} ]. \mforall{}[isEmpty:\{f:map {}\mrightarrow{} \mBbbB{}|
\mforall{}m:map
(\muparrow{}(f m) \mLeftarrow{}{}\mRightarrow{} \mforall{}k:Key. (\mneg{}\muparrow{}(inDom k m)))\} ].
\mforall{}[update:\{f:Key {}\mrightarrow{} Value {}\mrightarrow{} map {}\mrightarrow{} map|
\mforall{}m:map. \mforall{}k1,k2:Key. \mforall{}v:Value.
((find k1 (f k2 v m)) = if eqKey k1 k2 then inl v else find k1 m fi )\} ].
\mforall{}[add:\{f:Key {}\mrightarrow{} Value {}\mrightarrow{} map {}\mrightarrow{} map|
\mforall{}m:map. \mforall{}k1,k2:Key. \mforall{}v:Value.
((find k1 (f k2 v m))
= if (eqKey k1 k2) \mwedge{}\msubb{} (\mneg{}\msubb{}(inDom k2 m)) then inl v else find k1 m fi )\} ].
\mforall{}[remove:\{f:Key {}\mrightarrow{} map {}\mrightarrow{} map|
\mforall{}m:map. \mforall{}k1,k2:Key.
((find k1 (f k2 m)) = if eqKey k1 k2 then inr \mcdot{} else find k1 m fi )\} ].
(mk-map(Key;Value;map;eqKey;find;inDom;empty;isEmpty;update;add;remove) \mmember{} map-sig\{i:l\}(Key;Value))
Date html generated:
2015_07_17-AM-08_22_02
Last ObjectModification:
2015_04_02-PM-05_43_32
Home
Index