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
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
mk-map: mk-map(Key;Value;map;eqKey;find;inDom;empty;isEmpty;update;add;remove),
map-sig: map-sig{i:l}(Key;Value),
record+: record+,
record-update: r[x := v],
record: record(x.T[x]),
top: Top,
all: ∀x:A. B[x],
implies: P ⇒ Q,
bool: 𝔹,
unit: Unit,
it: ⋅,
btrue: tt,
uiff: uiff(P;Q),
and: P ∧ Q,
uimplies: b supposing a,
ifthenelse: if b then t else f fi ,
sq_type: SQType(T),
guard: {T},
record-select: r.x,
eq_atom: x =a y,
bfalse: ff,
iff: P ⇐⇒ Q,
not: ¬A,
prop: ℙ,
rev_implies: P ⇐ Q,
exposed-bfalse: exposed-bfalse,
so_lambda: λ2x.t[x],
deq: EqDecider(T),
eqof: eqof(d),
exists: ∃x:A. B[x],
or: P ∨ Q,
bnot: ¬bb,
assert: ↑b,
false: False,
so_apply: x[s],
band: p ∧b q
Latex:
\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:
2016_05_17-PM-01_46_40
Last ObjectModification:
2015_12_28-PM-08_52_17
Theory : datatype-signatures
Home
Index