Nuprl Lemma : C_Struct_vs_DVALp

∀store:C_STOREp(). ∀ctyp:C_TYPE(). ∀env:C_TYPE_env(). ∀dval:C_DVALUEp().
  (C_STOREp-welltyped(env;store)
  ⇒ (↑C_Struct?(ctyp))
  ⇒ C_TYPE_vs_DVALp(env;ctyp) dval 
     = if DVp_Struct?(dval)
       then let r = map(λp.<fst(p), C_TYPE_vs_DVALp(env;snd(p))>;C_Struct-fields(ctyp)) in
             let lbls = DVp_Struct-lbls(dval) in
             let g = DVp_Struct-struct(dval) in
             (∀p∈r.let a,wt = p 
                   in a ∈b lbls) ∧b (wt (g a)))_b
       else ff
       fi )


Proof



Definitions occuring in Statement :  C_STOREp-welltyped: C_STOREp-welltyped(env;store),  C_STOREp: C_STOREp(),  C_TYPE_vs_DVALp: C_TYPE_vs_DVALp(env;ctyp),  DVp_Struct-struct: DVp_Struct-struct(v),  DVp_Struct-lbls: DVp_Struct-lbls(v),  DVp_Struct?: DVp_Struct?(v),  C_DVALUEp: C_DVALUEp(),  C_TYPE_env: C_TYPE_env(),  C_Struct-fields: C_Struct-fields(v),  C_Struct?: C_Struct?(v),  C_TYPE: C_TYPE(),  deq-member: x ∈b L),  atom-deq: AtomDeq,  bl-all: (∀x∈L.P[x])_b,  map: map(f;as),  band: p ∧b q,  assert: ↑b,  ifthenelse: if b then t else f fi ,  bfalse: ff,  bool: 𝔹,  let: let,  pi1: fst(t),  pi2: snd(t),  all: ∀x:A. B[x],  implies: P ⇒ Q,  apply: f a,  lambda: λx.A[x],  spread: spread def,  pair: <a, b>,  equal: s = t ∈ T
Lemmas :  iff_imp_equal_bool,  bdd-all_wf,  length_wf_nat,  C_TYPE_wf,  value-type-has-value,  atom-value-type,  select_wf,  sq_stable__le,  deq-member_wf,  atom-deq_wf,  DVp_Struct-lbls_wf,  bool_wf,  eqtt_to_assert,  assert-deq-member,  C_TYPE_vs_DVALp_wf,  DVp_Struct-struct_wf,  l_member_wf,  int_seg_wf,  length_wf,  bl-all_wf,  C_DVALUEp_wf,  map_wf,  C_DVALUEp-ext,  eq_atom_wf,  assert_of_eq_atom,  subtype_base_sq,  atom_subtype_base,  unit_wf2,  unit_subtype_base,  it_wf,  eqff_to_assert,  equal_wf,  bool_cases_sqequal,  bool_subtype_base,  assert-bnot,  neg_assert_of_eq_atom,  assert-bdd-all,  assert-bl-all,  assert_wf,  iff_wf,  all_wf,  l_all_wf2,  list_induction,  list_wf,  length_of_nil_lemma,  stuck-spread,  base_wf,  map_nil_lemma,  length_of_cons_lemma,  map_cons_lemma,  l_all_nil,  less_than_transitivity1,  less_than_irreflexivity,  nil_wf,  l_all_cons,  cons_wf,  length_cons,  non_neg_length,  false_wf,  lelt_wf,  decidable__le,  not-le-2,  condition-implies-le,  minus-add,  minus-one-mul,  zero-add,  add-associates,  add-swap,  add-commutes,  add_functionality_wrt_le,  add-zero,  le-add-cancel,  decidable__lt,  less-iff-le,  le-add-cancel2,  select_cons_tl_sq,  decidable__equal_int,  int_subtype_base,  product_subtype_base,  C_TYPE_subtype_base,  select-cons-tl,  not-equal-2,  minus-zero,  subtract_wf,  minus-minus
\mforall{}store:C\_STOREp().  \mforall{}ctyp:C\_TYPE().  \mforall{}env:C\_TYPE\_env().  \mforall{}dval:C\_DVALUEp().
    (C\_STOREp-welltyped(env;store)
    {}\mRightarrow{}  (\muparrow{}C\_Struct?(ctyp))
    {}\mRightarrow{}  C\_TYPE\_vs\_DVALp(env;ctyp)  dval 
          =  if  DVp\_Struct?(dval)
              then  let  r  =  map(\mlambda{}p.<fst(p),  C\_TYPE\_vs\_DVALp(env;snd(p))>C\_Struct-fields(ctyp))  in
                          let  lbls  =  DVp\_Struct-lbls(dval)  in
                          let  g  =  DVp\_Struct-struct(dval)  in
                          (\mforall{}p\mmember{}r.let  a,wt  =  p 
                                      in  a  \mmember{}\msubb{}  lbls)  \mwedge{}\msubb{}  (wt  (g  a)))\_b
              else  ff
              fi  )


Date html generated: 2015_07_17-AM-07_45_26
Last ObjectModification: 2015_01_29-PM-04_39_43

Home Index