Changeset 2118 for src/common


Ignore:
Timestamp:
Jun 27, 2012, 12:04:27 PM (7 years ago)
Author:
campbell
Message:

Labelling preserves behaviour.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/SmallstepExec.ma

    r1599 r2118  
    8080*)
    8181
     82lemma exec_inf_stops_at_final : ∀O,I,TS,ge,s,s',tr,r.
     83  exec_inf_aux O I TS ge (step … ge s) = e_stop … tr r s' →
     84  step … ge s = Value … 〈tr, s'〉 ∧
     85  is_final … s' = Some ? r.
     86#O #I #TS #ge #s #s' #tr #r
     87>exec_inf_aux_unfold
     88cases (step … ge s)
     89[ 1,3: normalize #H1 #H2 try #H3 destruct
     90| * #tr' #s''
     91  whd in ⊢ (??%? → ?);
     92  lapply (refl ? (is_final … s''))
     93  cases (is_final … s'') in ⊢ (???% → %);
     94  [ #_ whd in ⊢ (??%? → ?); #E destruct
     95  | #r' #E1 #E2 whd in E2:(??%?);  destruct % //
     96  ]
     97] qed.
     98
     99lemma extract_step : ∀O,I,TS,ge,s,s',tr,e.
     100  exec_inf_aux O I TS ge (step … ge s) = e_step … tr s' e →
     101  step … ge s = Value …  〈tr,s'〉 ∧ e = exec_inf_aux O I TS ge (step … ge s').
     102#O #I #TS #ge #s #s' #tr #e
     103>exec_inf_aux_unfold
     104cases (step … s)
     105[ 1,3: normalize #H1 #H2 try #H3 destruct
     106| * #tr' #s''
     107  whd in ⊢ (??%? → ?);
     108  cases (is_final … s'')
     109  [ #E normalize in E; destruct /2/
     110  | #r #E normalize in E; destruct
     111  ]
     112] qed.
     113
     114lemma exec_e_step_not_final : ∀O,I,TS,ge,s,s',tr,e.
     115  exec_inf_aux O I TS ge (step … ge s) = e_step … tr s' e →
     116  is_final … s' = None ?.
     117#O #I #TS #ge #s #s' #tr #e
     118>exec_inf_aux_unfold
     119cases (step … s)
     120[ 1,3: normalize #H1 #H2 try #H3 destruct
     121| * #tr' #s''
     122  whd in ⊢ (??%? → ?);
     123  lapply (refl ? (is_final … s''))
     124  cases (is_final … s'') in ⊢ (???% → %);
     125  [ #F whd in ⊢ (??%? → ?); #E destruct @F
     126  | #r' #_ #E whd in E:(??%?);  destruct
     127  ]
     128] qed.
     129
     130
     131
    82132record fullexec (outty:Type[0]) (inty:outty → Type[0]) : Type[2] ≝
    83133{ program : Type[0]
Note: See TracChangeset for help on using the changeset viewer.