Ignore:
Timestamp:
Apr 3, 2013, 5:54:34 PM (7 years ago)
Author:
campbell
Message:

Tidy up recent work a little.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/SmallstepExec.ma

    r2685 r3081  
    235235qed.
    236236
     237lemma after_aux_result : ∀avs,n,s,tr,P.
     238  after_aux avs n s tr P →
     239  ∃tr',s'. P tr' s' ∧ after_aux avs n s tr (λtr'',s''. 〈tr'',s''〉 = 〈tr',s'〉).
     240#avs #n elim n
     241[ #s #tr #P #A whd in A; %{tr} %{s} % [ @A | % ]
     242| #n' #IH #s #tr #P
     243  whd in ⊢ (% → ?);
     244  lapply (refl ? (is_final … s))
     245  cases (is_final … s) in ⊢ (???% → %);
     246  [ #F whd in ⊢ (% → ?);
     247    lapply (refl ? (step … s))
     248    cases (step … s) in ⊢ (???% → %);
     249    [ #o #k #_ *
     250    | * #tr1 #s1 #ST whd in ⊢ (% → ?);
     251      cases n' in IH ⊢ %;
     252      [ #_ whd in ⊢ (% → ?); #p % [2: % [2: %{p} whd >F whd >ST whd % | skip ] | skip ]
     253      | #n'' #IH lapply (refl ? (avs_inv avs s1)) cases (avs_inv avs s1) in ⊢ (???% → %);
     254        [ #INV #AF
     255          cases (IH … AF) #tr' * #s' * #p #AF'
     256         % [2: % [2: %{p} whd >F whd >ST whd >INV @AF' | skip ] | skip ]
     257        | #_ *
     258        ]
     259      ]
     260    | #m #_ *
     261    ]
     262  | #r #F *
     263  ]
     264] qed.
     265
     266lemma after_n_result : ∀n,O,I,exec,g,s,P,inv.
     267  after_n_steps n O I exec g s inv P →
     268  ∃tr',s'.
     269    P tr' s' ∧
     270    after_n_steps n O I exec g s inv (λtr'',s''. 〈tr'',s''〉 = 〈tr',s'〉).
     271#n #O #I #exec #g #s #P #inv #A
     272cases (after_aux_result … A) #tr * #s' * #p #A'
     273%{tr} %{s'} %{p} @A'
     274qed.
     275
     276lemma after_1_of_n_steps' : ∀n,O,I,exec,g,tr,s',s.
     277  after_n_steps (S n) O I exec g s (λ_.true) (λtrx,sx. 〈trx,sx〉 = 〈tr,s'〉) →
     278  ∃tr1,tr2,s1.
     279  is_final … exec g s = None ? ∧
     280  step … exec g s = Value … 〈tr1,s1〉 ∧
     281  tr = tr1⧺tr2 ∧
     282  after_n_steps n O I exec g s1 (λ_.true) (λtrx,sx. 〈trx,sx〉 = 〈tr2,s'〉).
     283#n #O #I #exec #g #tr #s' #s #A
     284cases (after_1_of_n_steps … A)
     285#tr1 * #s1 * * * #F #ST #_ #A'
     286cases (after_n_result … A')
     287#tr'' * #s'' * #E #A'' destruct
     288% [2: % [2: % [2: % [ % [% [ @F | @ST ] | % ] | @A'' ] | skip ] | skip ] | skip ]
     289qed.
     290
    237291(* A typical way to use the following:
    238292
Note: See TracChangeset for help on using the changeset viewer.