Changeset 2892


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

Add cost hypotheses.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/MeasurableToStructured.ma

    r2839 r2892  
    218218  >STEPS'' %
    219219] qed.
    220  
     220
     221lemma label_to_return_state_labelled : ∀C,n,s,trace,s'.
     222  trace_is_label_to_return C trace →
     223  exec_steps n ?? C ? s = OK ? 〈trace,s'〉 →
     224  cs_labelled C s.
     225#C #n #s #trace #s'
     226* #tr * #s1 * #trace' * #tr' * #s2 * * #E #CS #_ destruct
     227#EX >(exec_steps_first … EX)
     228@CS
     229qed.
     230
     231lemma well_cost_labelled_exec_steps : ∀n,g,s,trace,s'.
     232  well_cost_labelled_ge g →
     233  exec_steps n ?? RTLabs_fullexec g s = OK ? 〈trace,s'〉 →
     234  well_cost_labelled_state s →
     235  well_cost_labelled_state s'.
     236#n #g elim n
     237[ #s #trace #s' #_ #E whd in E:(??%%); destruct //
     238| #m #IH #s #trace #s' #WCLge #EX
     239  cases (exec_steps_S … EX) #NF * #tr * #s1 * #tl * * #E #STEP #EX'
     240  #WCLs @(IH … WCLge … EX')
     241  @(well_cost_labelled_state_step … STEP WCLge WCLs)
     242] qed.
    221243 
    222244
     
    228250
    229251theorem measurable_subtraces_are_structured : ∀p,m,n,stack_cost,max,prefix,interesting.
     252  well_cost_labelled_program p →
    230253  measurable RTLabs_pcsys p m n stack_cost max →
    231254  observables RTLabs_pcsys p m n = return 〈prefix,interesting〉 →
     
    236259  pi1 … (observables_trace_label_return (RTLabs_status (make_global p)) sm sn tlr fn) = interesting.
    237260#p #m #n #stack_cost #max #prefix #interesting
     261#WCLP cases (well_cost_labelled_make_global p WCLP)
    238262change with (make_global … RTLabs_fullexec p) in match (make_global p);
     263#WCLge #SLge
    239264* #s0 * #prefix' * #s1 * #interesting' * #s2
    240265letin ge ≝ (make_global … RTLabs_fullexec p)
     
    249274lapply (make_label_return' ge 0 s1' (make_flat_trace ????? EXEC2) ????)
    250275[ @will_return_equiv assumption
    251 |
    252 |
    253 |
     276| @(label_to_return_state_labelled … LABEL_TO_RETURN EXEC2)
     277| @(well_cost_labelled_exec_steps … EXEC1)
     278  [ assumption
     279  | @(proj1 … (well_cost_labelled_initial … INIT WCLP))
     280  ]
     281| @WCLge
    254282| * #s2' #rem #_ #tlr #STACK #_
    255283%{s1'} %{s2'} % [2: %{tlr}
Note: See TracChangeset for help on using the changeset viewer.