Nuprl 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))
Proof
Definitions occuring in Statement :
mk-set: mk-set(Item;set;member;empty;isEmpty;singleton;add;union;remove),
set-sig: set-sig{i:l}(Item),
valueall-type: valueall-type(T),
assert: ↑b,
bool: 𝔹,
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
not: ¬A,
implies: P ⇒ Q,
or: P ∨ Q,
and: P ∧ Q,
member: t ∈ T,
set: {x:A| B[x]} ,
apply: f a,
function: x:A ⟶ B[x],
universe: Type,
equal: s = t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
mk-set: mk-set(Item;set;member;empty;isEmpty;singleton;add;union;remove),
set-sig: set-sig{i:l}(Item),
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,
so_lambda: λ2x.t[x],
so_apply: x[s],
or: P ∨ Q
Latex:
\mforall{}[Item:Type]. \mforall{}[set:\{s:Type| valueall-type(Item) {}\mRightarrow{} valueall-type(s)\} ]. \mforall{}[member:Item {}\mrightarrow{} set {}\mrightarrow{} \mBbbB{}].
\mforall{}[empty:\{s:set| \mforall{}x:Item. (\mneg{}\muparrow{}(member x s))\} ]. \mforall{}[isEmpty:\{f:set {}\mrightarrow{} \mBbbB{}|
\mforall{}s:set
(\muparrow{}(f s) \mLeftarrow{}{}\mRightarrow{} \mforall{}x:Item. (\mneg{}\muparrow{}(member x s)))\} ].
\mforall{}[singleton:\{f:Item {}\mrightarrow{} set| \mforall{}x,y:Item. (\muparrow{}(member x (f y)) \mLeftarrow{}{}\mRightarrow{} x = y)\} ].
\mforall{}[add:\{f:Item {}\mrightarrow{} set {}\mrightarrow{} set|
\mforall{}s:set. \mforall{}x,y:Item. (\muparrow{}(member x (f y s)) \mLeftarrow{}{}\mRightarrow{} (x = y) \mvee{} (\muparrow{}(member x s)))\} ].
\mforall{}[union:\{f:set {}\mrightarrow{} set {}\mrightarrow{} set|
\mforall{}s1,s2:set. \mforall{}x:Item. (\muparrow{}(member x (f s1 s2)) \mLeftarrow{}{}\mRightarrow{} (\muparrow{}(member x s1)) \mvee{} (\muparrow{}(member x s2)))\} ].
\mforall{}[remove:\{f:Item {}\mrightarrow{} set {}\mrightarrow{} set|
\mforall{}s:set. \mforall{}x,y:Item. (\muparrow{}(member x (f y s)) \mLeftarrow{}{}\mRightarrow{} (\mneg{}(x = y)) \mwedge{} (\muparrow{}(member x s)))\} ].
(mk-set(Item;set;member;empty;isEmpty;singleton;add;union;remove) \mmember{} set-sig\{i:l\}(Item))
Date html generated:
2016_05_17-PM-01_44_07
Last ObjectModification:
2015_12_28-PM-08_52_54
Theory : datatype-signatures
Home
Index