Ignore:
Timestamp:
Nov 23, 2012, 3:47:22 PM (8 years ago)
Author:
campbell
Message:

Set up "after_n_steps" to enforce an invariant on states.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Executions.ma

    r2338 r2487  
    4646
    4747lemma after_inv : ∀FE:fullexec io_out io_in.
    48  ∀n,g,P,s.
    49   after_n_steps (S n) … FE g s P →
     48 ∀n,g,inv,P,s.
     49  after_n_steps (S n) … FE g s inv P →
    5050  ∃tr,s'.
    5151    P tr s' ∧
     
    5858                 (exec_inf_aux … FE g (step … FE g s'))
    5959    ].
    60 #FE #n #g #P
     60#FE #n #g #inv #P
    6161(* Rather nasty generalisation *)
    6262#s whd in ⊢ (% → ?); cases (is_final … s) [2: #r * ] whd in ⊢ (% → ?); #AW
     
    6666[ #s #tr whd in ⊢ (% → %);
    6767  cases (step … s) [ #o #K * | 3: #m * ]
    68   * #tr' #s' #AW %{tr'} %{s'} %{AW}
     68  * #tr' #s'
     69  whd in ⊢ (% → ?); cases (inv s') [2: *]
     70  #AW %{tr'} %{s'} %{AW}
    6971  lapply (refl ? (is_final … s')) cases (is_final … s') in ⊢ (???% → %);
    7072  [ #NF whd >exec_inf_aux_unfold whd in ⊢ (???%?); >NF @steps_step
     
    7375| #n' #IH #s #tr whd in ⊢ (% → ?);
    7476  cases (step … s) [ #o #K * | 3: #m * ] * #tr1 #s1
     77  whd in ⊢ (% → ?); cases (inv s1) [2: *]
    7578  whd in ⊢ (% → ?); lapply (refl ? (is_final … s1)) cases (is_final … s1) in ⊢ (???% → %);
    7679  [ 2: #r #_ * ] #NF1 whd in ⊢ (% → ?); #AW1
Note: See TracChangeset for help on using the changeset viewer.