Ignore:
Timestamp:
Mar 16, 2013, 9:08:21 PM (7 years ago)
Author:
campbell
Message:

Minor tidying.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLabs_partial_traces.ma

    r2895 r2897  
    8888] qed.
    8989
     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. *)
     94record 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
    90102lemma cons_flat_trace : ∀ge,n,s,hd,trace,s'.
    91103  ∀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.
    93105#ge #n #s #hd #trace #s' #EX
    94106lapply (refl ? (eval_statement ge s))
     
    98110  change with (eval_statement ??) in ⊢ (??%? → ?); >EV #E destruct
    99111] * #tr #s1 #EV
    100 %{s1}
    101 cases (exec_steps_S … EX) #NF * #tr2 * #s2 * #tl * * #E1 destruct
    102 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.
    108120
    109121let rec length_flat_trace O I ge s (t:flat_trace O I ge s) on t : nat ≝
     
    112124| ft_step _ _ _ _ t' ⇒ S (length_flat_trace … t')
    113125].
     126
     127lemma 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.
    114136
    115137
Note: See TracChangeset for help on using the changeset viewer.