Ignore:
Timestamp:
Dec 4, 2012, 6:16:25 PM (8 years ago)
Author:
tranquil
Message:

rewritten function handling in joint
swapped call_rel with ret_rel in the definition of status_rel, and parameterised status_simulation on status_rel
renamed SemanticUtils?

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semanticsUtils.ma

    r2470 r2529  
    7575  mk_sem_params
    7676    g_pars
    77     (mk_more_sem_params
    78       g_pars
    79       (spars ?)
    80       (word_of_identifier ?)
    81       (an_identifier ?)
    82       ? (refl …)
    83     ).
     77    (spars ?)
     78    (word_of_identifier ?)
     79    (an_identifier ?)
     80    ? (refl …).
    8481* #p % qed.
    8582
     
    8986@pos_elim [%]
    9087#p #IH >nat_possucc whd in ⊢ (??%?); >IH % qed.
    91 
    9288
    9389definition make_sem_lin_params :
     
    9995  mk_sem_params
    10096    lin_pars
    101     (mk_more_sem_params
    102       lin_pars
    103       (spars ?)
    104       succ_pos_of_nat
    105       (λp.pred (nat_of_pos p))
    106       ??
    107     ).
    108 [ @pos_cases [%] #p >nat_possucc @succ_pos_of_nat_of_pos
    109 | #n >nat_succ_pos %
     97    (spars ?)
     98    succ_pos_of_nat
     99    (λp.pred (nat_of_pos p))
     100    ??.
     101[ #n >nat_succ_pos %
     102| @pos_cases [%] #p >nat_possucc @succ_pos_of_nat_of_pos
    110103] qed.
     104
     105
     106
     107
     108lemma fetch_statement_eq : ∀p:sem_params.∀g.
     109  ∀ge : genv_t (joint_function p g).∀ptr : program_counter.
     110  ∀i,fn,s.
     111  fetch_internal_function … ge (pc_block ptr) = OK … 〈i, fn〉 →
     112  let pt ≝ point_of_pc … ptr in
     113  stmt_at … (joint_if_code … fn) pt = Some ? s →
     114  fetch_statement … ge ptr = OK … 〈i, fn, s〉.
     115#p #g #ge #ptr #i #f #s #EQ1 #EQ2
     116whd in match fetch_statement; normalize nodelta >EQ1 >m_return_bind
     117>EQ2 %
     118qed.
     119
     120lemma fetch_statement_inv : ∀p:sem_params.∀g.
     121  ∀ge : genv_t (joint_function p g).∀ptr : program_counter.
     122  ∀i,fn,s.
     123  fetch_statement … ge ptr = OK … 〈i, fn, s〉 →
     124  fetch_internal_function … ge (pc_block ptr) = OK … 〈i, fn〉 ∧
     125  let pt ≝ point_of_pc p ptr in
     126  stmt_at … (joint_if_code … fn) pt = Some ? s.
     127#p #g #ge #ptr #i #fn #s #H
     128elim (bind_inversion ????? H) * #i #f' * #EQ1 -H #H
     129elim (bind_inversion ????? H) #s' * #H
     130lapply (opt_eq_from_res ???? H) -H #EQ2
     131whd in ⊢ (??%%→?); #EQ destruct(EQ) %{EQ1 EQ2}
     132qed.
     133
Note: See TracChangeset for help on using the changeset viewer.