Nuprl Lemma : C_DVALUEp_ind_wf
∀[A:Type]. ∀[R:A ⟶ C_DVALUEp() ⟶ ℙ]. ∀[v:C_DVALUEp()]. ∀[Null:x:Unit ⟶ {x1:A| R[x1;DVp_Null(x)]} ].
∀[Int:int:ℤ ⟶ {x:A| R[x;DVp_Int(int)]} ]. ∀[Pointer:ptr:(C_LVALUE()?) ⟶ {x:A| R[x;DVp_Pointer(ptr)]} ].
∀[Array:lower:ℤ
⟶ upper:ℤ
⟶ arr:({lower..upper-} ⟶ C_DVALUEp())
⟶ (u:{lower..upper-} ⟶ {x:A| R[x;arr u]} )
⟶ {x:A| R[x;DVp_Array(lower;upper;arr)]} ]. ∀[Struct:lbls:(Atom List)
⟶ struct:({a:Atom| (a ∈ lbls)} ⟶ C_DVALUEp())
⟶ (u:{a:Atom| (a ∈ lbls)} ⟶ {x:A| R[x;struct u]} )
⟶ {x:A| R[x;DVp_Struct(lbls;struct)]} ].
(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]) ∈ {x:A| R[x;v]} )
Proof
Definitions occuring in Statement :
C_DVALUEp_ind: C_DVALUEp_ind,
DVp_Struct: DVp_Struct(lbls;struct),
DVp_Array: DVp_Array(lower;upper;arr),
DVp_Pointer: DVp_Pointer(ptr),
DVp_Int: DVp_Int(int),
DVp_Null: DVp_Null(x),
C_DVALUEp: C_DVALUEp(),
C_LVALUE: C_LVALUE(),
l_member: (x ∈ l),
list: T List,
int_seg: {i..j-},
uall: ∀[x:A]. B[x],
prop: ℙ,
so_apply: x[s1;s2;s3;s4],
so_apply: x[s1;s2;s3],
so_apply: x[s1;s2],
so_apply: x[s],
unit: Unit,
member: t ∈ T,
set: {x:A| B[x]} ,
apply: f a,
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,
C_DVALUEp_ind: C_DVALUEp_ind,
so_apply: x[s1;s2;s3],
so_apply: x[s1;s2;s3;s4],
so_apply: x[s],
so_apply: x[s1;s2],
C_DVALUEp-definition,
C_DVALUEp-induction,
uniform-comp-nat-induction,
C_DVALUEp-ext,
eq_atom: x =a y,
it: ⋅,
bool_cases_sqequal,
eqff_to_assert,
any: any x,
btrue: tt,
bfalse: ff,
top: Top,
all: ∀x:A. B[x],
implies: P ⇒ Q,
has-value: (a)↓,
so_lambda: so_lambda(x,y,z,w.t[x; y; z; w]),
so_lambda: λ2x.t[x],
uimplies: b supposing a,
strict4: strict4(F),
and: P ∧ Q,
prop: ℙ,
guard: {T},
or: P ∨ Q,
squash: ↓T,
subtype_rel: A ⊆r B
Lemmas referenced :
C_DVALUEp-definition,
C_DVALUEp-induction,
uniform-comp-nat-induction,
C_DVALUEp-ext,
bool_cases_sqequal,
eqff_to_assert,
set_wf,
all_wf,
DVp_Struct_wf,
l_member_wf,
list_wf,
DVp_Array_wf,
int_seg_wf,
DVp_Pointer_wf,
C_LVALUE_wf,
DVp_Int_wf,
DVp_Null_wf,
unit_wf2,
C_DVALUEp_wf,
base_wf,
lifting-strict-atom_eq,
is-exception_wf,
has-value_wf_base,
top_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
introduction,
cut,
sqequalRule,
isect_memberEquality,
voidElimination,
voidEquality,
thin,
lemma_by_obid,
hypothesis,
lambdaFormation,
because_Cache,
sqequalSqle,
divergentSqle,
callbyvalueDecide,
sqequalHypSubstitution,
unionEquality,
unionElimination,
sqleReflexivity,
equalityEquality,
equalityTransitivity,
equalitySymmetry,
hypothesisEquality,
dependent_functionElimination,
independent_functionElimination,
decideExceptionCases,
axiomSqleEquality,
exceptionSqequal,
baseApply,
closedConclusion,
baseClosed,
isectElimination,
independent_isectElimination,
independent_pairFormation,
inrFormation,
imageMemberEquality,
imageElimination,
inlFormation,
instantiate,
extract_by_obid,
applyEquality,
lambdaEquality,
isectEquality,
functionEquality,
cumulativity,
universeEquality,
setEquality,
intEquality,
atomEquality,
setElimination,
rename,
dependent_set_memberEquality,
axiomEquality
Latex:
\mforall{}[A:Type]. \mforall{}[R:A {}\mrightarrow{} C\_DVALUEp() {}\mrightarrow{} \mBbbP{}]. \mforall{}[v:C\_DVALUEp()].
\mforall{}[Null:x:Unit {}\mrightarrow{} \{x1:A| R[x1;DVp\_Null(x)]\} ]. \mforall{}[Int:int:\mBbbZ{} {}\mrightarrow{} \{x:A| R[x;DVp\_Int(int)]\} ].
\mforall{}[Pointer:ptr:(C\_LVALUE()?) {}\mrightarrow{} \{x:A| R[x;DVp\_Pointer(ptr)]\} ].
\mforall{}[Array:lower:\mBbbZ{}
{}\mrightarrow{} upper:\mBbbZ{}
{}\mrightarrow{} arr:(\{lower..upper\msupminus{}\} {}\mrightarrow{} C\_DVALUEp())
{}\mrightarrow{} (u:\{lower..upper\msupminus{}\} {}\mrightarrow{} \{x:A| R[x;arr u]\} )
{}\mrightarrow{} \{x:A| R[x;DVp\_Array(lower;upper;arr)]\} ]. \mforall{}[Struct:lbls:(Atom List)
{}\mrightarrow{} struct:(\{a:Atom| (a \mmember{} lbls)\}
{}\mrightarrow{} C\_DVALUEp())
{}\mrightarrow{} (u:\{a:Atom| (a \mmember{} lbls)\} {}\mrightarrow{} \{x:A|
R[x;struct
u]\} )
{}\mrightarrow{} \{x:A|
R[x;DVp\_Struct(lbls;struct)]\} ].
(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{} \{x:A| R[x;v]\} )
Date html generated:
2016_05_16-AM-08_51_03
Last ObjectModification:
2016_01_17-AM-09_44_15
Theory : C-semantics
Home
Index