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

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/MeasurableToStructured.ma
r2896 r2897 137 137 λS,s1,s2,tlr,stack_cost,currentfn,initial. 138 138 maximum (update_stacksize_info stack_cost (mk_stacksize_info initial 0) (extract_call_ud_from_tlr S s1 s2 tlr currentfn)). 139 140 (* A bit of mucking around because we're going to build a will_return in Type[0].141 In principle we could drop the alternative form of will_return entirely, but142 time pressures don't really allow for that. *)143 record cft (ge:genv) (n:nat) (s:state) (hd:state×trace) (rem:list (state × trace)) (s':state) (EX:?) : Type[0] ≝ {144 cft_tr : trace;145 cft_s : state;146 cft_EV : eval_statement ge s = Value ??? 〈cft_tr,cft_s〉;147 cft_EX : exec_steps n … RTLabs_fullexec ge cft_s = OK ? 〈rem,s'〉;148 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)149 }.150 151 lemma cons_flat_trace : ∀ge,n,s,hd,trace,s'.152 ∀EX:exec_steps (S n) … RTLabs_fullexec ge s = return 〈hd::trace,s'〉.153 cft ge n s hd trace s' EX.154 #ge #n #s #hd #trace #s' #EX155 lapply (refl ? (eval_statement ge s))156 cases (eval_statement ge s) in ⊢ (???% → ?);157 [ #o #k  3: #m ]158 [ 1,2: #EV @⊥ cases (exec_steps_S … EX) #NF * #tr * #s2 * #tl * * #E1 destruct159 change with (eval_statement ??) in ⊢ (??%? → ?); >EV #E destruct160 ] * #tr #s1 #EV161 @(mk_cft … tr s1 EV)162 [ cases (exec_steps_S … EX) #NF * #tr2 * #s2 * #tl * * #E1 destruct163 change with (eval_statement ??) in ⊢ (??%? → ?);164 >EV in ⊢ (% → ?); #E destruct #EX' @EX'165  whd in ⊢ (??%?); generalize in ⊢ (??(?%)?);166 >EV in ⊢ (???% → ??(match % with [_⇒?_⇒?_⇒?]?)?);167 #ST' whd in ⊢ (??%?); %168 ] qed.169 139 170 140 lemma will_return_equiv : ∀ge,trace,depth,n,s,s',EX. … … 251 221 generalize in match (cs_callee ??); 252 222 whd in match (cs_classify ??); cases (next_instruction f) // 253 qed.254 255 (* TODO move*)256 lemma All2_tail : ∀A,B,P,a,b.257 All2 A B P a b →258 All2 A B P (tail A a) (tail B b).259 #A #B #P * [2: #ah #at] * [2,4: #bh #bt]260 * //261 223 qed. 262 224 … … 745 707 746 708 747 (* TODO move *)748 lemma make_flat_trace_length : ∀ge,n,s1,trace,s2,EX.749 length_flat_trace io_out io_in ge s1 (make_flat_trace ge n s1 trace s2 EX) = n.750 #ge #n0 elim n0751 [ #s1 #trace #s2 #EX %752  #n #IH #s1 #trace #s2 #EX753 cases (exec_steps_S … EX) #_ * #tr * #s' * #tl * * #E1 #E2 #E3 destruct754 cases (cons_flat_trace ?????? EX)755 #tr'' #s'' #ST'' #EX'' #E >E whd in ⊢ (??%?); @eq_f @IH756 ] qed.757 709 758 710 … … 855 807 * // 856 808 ] 857 ] ]858 809 ] 810
Note: See TracChangeset
for help on using the changeset viewer.