Changeset 732


Ignore:
Timestamp:
Apr 1, 2011, 2:52:30 PM (9 years ago)
Author:
campbell
Message:

Fixups for CexecEquiv? due to earlier changes in SmallstepExec?.ma

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/CexecEquiv.ma

    r708 r732  
    5252 (∀r. final_state s r → P (Some ? r)) →
    5353 ((¬∃r.final_state s r) → P (None ?)) →
    54 P (is_final clight_exec s).
    55 #s #P #F #NF lapply (refl ? (is_final clight_exec s))
    56 cases (is_final clight_exec s) in ⊢ (???% → %)
     54P (is_final ?? clight_exec s).
     55#s #P #F #NF lapply (refl ? (is_final ?? clight_exec s))
     56cases (is_final ?? clight_exec s) in ⊢ (???% → %)
    5757[ #E @NF % * #r #H > (is_final_complete … H) in E #H destruct
    5858| #r #E @F @is_final_sound @E
     
    6060
    6161lemma exec_e_step: ∀ge,x,tr,s,e.
    62   exec_inf_aux clight_exec ge x = e_step ??? tr s e →
    63   exec_inf_aux clight_exec ge (exec_step ge s) = e.
     62  exec_inf_aux ?? clight_exec ge x = e_step ??? tr s e →
     63  exec_inf_aux ?? clight_exec ge (exec_step ge s) = e.
    6464#ge #x #tr #s #e
    6565>(exec_inf_aux_unfold …) cases x;
     
    7373
    7474lemma exec_e_step_inv: ∀ge,x,tr,s,e.
    75   exec_inf_aux clight_exec ge x = e_step ??? tr s e →
     75  exec_inf_aux ?? clight_exec ge x = e_step ??? tr s e →
    7676  x = Value ??? 〈tr,s〉.
    7777#ge #x #tr #s #e
     
    8686
    8787lemma exec_e_step_inv2: ∀ge,x,tr,s,e.
    88   exec_inf_aux clight_exec ge x = e_step ??? tr s e →
     88  exec_inf_aux ?? clight_exec ge x = e_step ??? tr s e →
    8989  ¬∃r.final_state s r.
    9090#ge #x #tr #s #e
     
    9797
    9898definition exec_from : genv → state → s_execution → Prop ≝
    99 λge,s,se. single_exec_of (exec_inf_aux clight_exec ge (exec_step ge s)) se.
     99λge,s,se. single_exec_of (exec_inf_aux ?? clight_exec ge (exec_step ge s)) se.
    100100
    101101lemma se_step_eq : ∀tr,s,e,tr',s',e'.
     
    294294
    295295lemma e_stop_inv: ∀ge,x,tr,r,m.
    296   exec_inf_aux clight_exec ge x = e_stop ??? tr r m →
     296  exec_inf_aux ?? clight_exec ge x = e_stop ??? tr r m →
    297297  x = Value ??? 〈tr,Returnstate (Vint r) Kstop m〉.
    298298#ge #x #tr #r #m
     
    991991
    992992lemma initial_step: ∀ge,s,e.
    993   exec_inf_aux clight_exec ge (Value ??? 〈E0,s〉) = e →
     993  exec_inf_aux ?? clight_exec ge (Value ??? 〈E0,s〉) = e →
    994994  ¬(∃r.final_state s r) →
    995995  ∃e'.e = e_step ??? E0 s e'.
     
    10051005  ∀classic:(∀P:Prop.P ∨ ¬P).
    10061006  ∀constructive_indefinite_description:(∀A:Type[0]. ∀P:A→Prop. (∃x. P x) → Sig A P).
    1007   ∀p,e. single_exec_of (exec_inf p) e →
     1007  ∀p,e. single_exec_of (exec_inf ?? clight_fullexec p) e →
    10081008   ∃b.execution_matches_behavior e b ∧ exec_program p b.
    10091009#classic #constructive_indefinite_description #p #e
Note: See TracChangeset for help on using the changeset viewer.