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 m) ⇐⇒ ↑isl(find m))} ].
[empty:{m:map| ∀k:Key. (¬↑(inDom m))} ]. ∀[isEmpty:{f:map ⟶ 𝔹| ∀m:map. (↑(f m) ⇐⇒ ∀k:Key. (¬↑(inDom m)))} ].
[update:{f:Key ⟶ Value ⟶ map ⟶ map| 
          ∀m:map. ∀k1,k2:Key. ∀v:Value.
            ((find k1 (f k2 m)) if eqKey k1 k2 then inl else find k1 fi  ∈ (Value?))} ].
[add:{f:Key ⟶ Value ⟶ map ⟶ map| 
       ∀m:map. ∀k1,k2:Key. ∀v:Value.
         ((find k1 (f k2 m)) if (eqKey k1 k2) ∧b b(inDom k2 m)) then inl else find k1 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 fi  ∈ (Value?))} ].
  (mk-map(Key;Value;map;eqKey;find;inDom;empty;isEmpty;update;add;remove) ∈ map-sig{i:l}(Key;Value))


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 then else fi  isl: isl(x) bool: 𝔹 it: uimplies: supposing a uall: [x:A]. B[x] all: x:A. B[x] iff: ⇐⇒ Q not: ¬A unit: Unit member: t ∈ T set: {x:A| B[x]}  apply: a function: x:A ⟶ B[x] inr: inr  inl: inl x union: left right universe: Type equal: 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:  Q bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) and: P ∧ Q uimplies: supposing a ifthenelse: if then else fi  sq_type: SQType(T) guard: {T} record-select: r.x eq_atom: =a y bfalse: ff iff: ⇐⇒ Q not: ¬A prop: rev_implies:  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

\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{}| 
                                                                                                                (\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