Nuprl Lemma : C_DVALUEp_ind_wf_simple
∀[A:Type]. ∀[v:C_DVALUEp()]. ∀[Null:x:Unit ⟶ A]. ∀[Int:int:ℤ ⟶ A]. ∀[Pointer:ptr:(C_LVALUE()?) ⟶ A].
∀[Array:lower:ℤ ⟶ upper:ℤ ⟶ arr:({lower..upper-} ⟶ C_DVALUEp()) ⟶ (u:{lower..upper-} ⟶ A) ⟶ A].
∀[Struct:lbls:(Atom List) ⟶ struct:({a:Atom| (a ∈ lbls)} ⟶ C_DVALUEp()) ⟶ (u:{a:Atom| (a ∈ lbls)} ⟶ A) ⟶ A].
(C_DVALUEp_ind(v;
DVp_Null(x)⇒ Null[x];
DVp_Int(int)⇒ Int[int];
DVp_Pointer(ptr)⇒ Pointer[ptr];
DVp_Array(lower,upper,arr)⇒ rec1.Array[lower;upper;arr;rec1];
DVp_Struct(lbls,struct)⇒ rec2.Struct[lbls;struct;rec2]) ∈ A)
Proof
Definitions occuring in Statement :
C_DVALUEp_ind: C_DVALUEp_ind,
C_DVALUEp: C_DVALUEp(),
C_LVALUE: C_LVALUE(),
l_member: (x ∈ l),
list: T List,
int_seg: {i..j-},
uall: ∀[x:A]. B[x],
so_apply: x[s1;s2;s3;s4],
so_apply: x[s1;s2;s3],
so_apply: x[s],
unit: Unit,
member: t ∈ T,
set: {x:A| B[x]} ,
function: x:A ⟶ B[x],
union: left + right,
int: ℤ,
atom: Atom,
universe: Type
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
so_lambda: λ2x y.t[x; y],
so_apply: x[s1;s2],
subtype_rel: A ⊆r B,
so_lambda: λ2x.t[x],
so_apply: x[s],
prop: ℙ,
uimplies: b supposing a,
all: ∀x:A. B[x],
true: True,
guard: {T}
Lemmas referenced :
C_DVALUEp_ind_wf,
true_wf,
C_DVALUEp_wf,
subtype_rel_dep_function,
unit_wf2,
C_LVALUE_wf,
int_seg_wf,
list_wf,
l_member_wf,
set_wf
Rules used in proof :
cut,
lemma_by_obid,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
hypothesis,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
sqequalRule,
lambdaEquality,
applyEquality,
because_Cache,
setEquality,
independent_isectElimination,
lambdaFormation,
dependent_set_memberEquality,
natural_numberEquality,
intEquality,
unionEquality,
functionEquality,
setElimination,
rename,
atomEquality,
equalityTransitivity,
equalitySymmetry,
universeEquality
Latex:
\mforall{}[A:Type]. \mforall{}[v:C\_DVALUEp()]. \mforall{}[Null:x:Unit {}\mrightarrow{} A]. \mforall{}[Int:int:\mBbbZ{} {}\mrightarrow{} A].
\mforall{}[Pointer:ptr:(C\_LVALUE()?) {}\mrightarrow{} A]. \mforall{}[Array:lower:\mBbbZ{}
{}\mrightarrow{} upper:\mBbbZ{}
{}\mrightarrow{} arr:(\{lower..upper\msupminus{}\} {}\mrightarrow{} C\_DVALUEp())
{}\mrightarrow{} (u:\{lower..upper\msupminus{}\} {}\mrightarrow{} A)
{}\mrightarrow{} A]. \mforall{}[Struct:lbls:(Atom List)
{}\mrightarrow{} struct:(\{a:Atom| (a \mmember{} lbls)\}
{}\mrightarrow{} C\_DVALUEp())
{}\mrightarrow{} (u:\{a:Atom| (a \mmember{} lbls)\} {}\mrightarrow{} A)
{}\mrightarrow{} A].
(C\_DVALUEp\_ind(v;
DVp\_Null(x){}\mRightarrow{} Null[x];
DVp\_Int(int){}\mRightarrow{} Int[int];
DVp\_Pointer(ptr){}\mRightarrow{} Pointer[ptr];
DVp\_Array(lower,upper,arr){}\mRightarrow{} rec1.Array[lower;upper;arr;rec1];
DVp\_Struct(lbls,struct){}\mRightarrow{} rec2.Struct[lbls;struct;rec2]) \mmember{} A)
Date html generated:
2016_05_16-AM-08_51_06
Last ObjectModification:
2015_12_28-PM-06_54_59
Theory : C-semantics
Home
Index