Changeset 2897 for src/RTLabs/RTLabs_partial_traces.ma
 Timestamp:
 Mar 16, 2013, 9:08:21 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/RTLabs_partial_traces.ma
r2895 r2897 88 88 ] qed. 89 89 90 (* Use a record to keep things in Type[0] overall, because in 91 MeasurableToStructured we're going to build a will_return in Type[0]. 92 In principle we could drop the alternative form of will_return entirely, but 93 time pressures don't really allow for that. *) 94 record cft (ge:genv) (n:nat) (s:state) (hd:state×trace) (rem:list (state × trace)) (s':state) (EX:?) : Type[0] ≝ { 95 cft_tr : trace; 96 cft_s : state; 97 cft_EV : eval_statement ge s = Value ??? 〈cft_tr,cft_s〉; 98 cft_EX : exec_steps n … RTLabs_fullexec ge cft_s = OK ? 〈rem,s'〉; 99 cft_E : make_flat_trace ge (S n) s (hd::rem) s' EX = ft_step ??? s cft_tr cft_s cft_EV (make_flat_trace ge n cft_s rem s' cft_EX) 100 }. 101 90 102 lemma cons_flat_trace : ∀ge,n,s,hd,trace,s'. 91 103 ∀EX:exec_steps (S n) … RTLabs_fullexec ge s = return 〈hd::trace,s'〉. 92 Σs1. ∃ST,EX'. make_flat_trace ge (S n) s (hd::trace) s' EX = ft_step ??? s (\snd hd) s1 ST (make_flat_trace ge n s1 trace s' EX').104 cft ge n s hd trace s' EX. 93 105 #ge #n #s #hd #trace #s' #EX 94 106 lapply (refl ? (eval_statement ge s)) … … 98 110 change with (eval_statement ??) in ⊢ (??%? → ?); >EV #E destruct 99 111 ] * #tr #s1 #EV 100 %{s1} 101 cases (exec_steps_S … EX) #NF * #tr2 * #s2 * #tl * * #E1 destruct102 change with (eval_statement ??) in ⊢ (??%? → ?); >EV in ⊢ (% → ?); #E destruct #EX' 103 %{EV} %{EX'} 104 whd in ⊢ (??%?); generalize in ⊢ (??(?%)?);105 >EV in ⊢ (???% → ??(match % with [_⇒?_⇒?_⇒?]?)?);106 #ST' whd in ⊢ (??%?); %107 qed.112 @(mk_cft … tr s1 EV) 113 [ cases (exec_steps_S … EX) #NF * #tr2 * #s2 * #tl * * #E1 destruct 114 change with (eval_statement ??) in ⊢ (??%? → ?); 115 >EV in ⊢ (% → ?); #E destruct #EX' @EX' 116  whd in ⊢ (??%?); generalize in ⊢ (??(?%)?); 117 >EV in ⊢ (???% → ??(match % with [_⇒?_⇒?_⇒?]?)?); 118 #ST' whd in ⊢ (??%?); % 119 ] qed. 108 120 109 121 let rec length_flat_trace O I ge s (t:flat_trace O I ge s) on t : nat ≝ … … 112 124  ft_step _ _ _ _ t' ⇒ S (length_flat_trace … t') 113 125 ]. 126 127 lemma make_flat_trace_length : ∀ge,n,s1,trace,s2,EX. 128 length_flat_trace io_out io_in ge s1 (make_flat_trace ge n s1 trace s2 EX) = n. 129 #ge #n0 elim n0 130 [ #s1 #trace #s2 #EX % 131  #n #IH #s1 #trace #s2 #EX 132 cases (exec_steps_S … EX) #_ * #tr * #s' * #tl * * #E1 #E2 #E3 destruct 133 cases (cons_flat_trace ?????? EX) 134 #tr'' #s'' #ST'' #EX'' #E >E whd in ⊢ (??%?); @eq_f @IH 135 ] qed. 114 136 115 137
Note: See TracChangeset
for help on using the changeset viewer.