Changeset 3081 for src/Clight/SwitchAndLabel.ma
 Timestamp:
 Apr 3, 2013, 5:54:34 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/SwitchAndLabel.ma
r3047 r3081 2 2 include "Clight/labelSimulation.ma". 3 3 4 5 lemma after_aux_result : ∀avs,n,s,tr,P. 6 after_aux avs n s tr P → 7 ∃tr',s'. P tr' s' ∧ after_aux avs n s tr (λtr'',s''. 〈tr'',s''〉 = 〈tr',s'〉). 8 #avs #n elim n 9 [ #s #tr #P #A whd in A; %{tr} %{s} % [ @A  % ] 10  #n' #IH #s #tr #P 11 whd in ⊢ (% → ?); 12 lapply (refl ? (is_final … s)) 13 cases (is_final … s) in ⊢ (???% → %); 14 [ #F whd in ⊢ (% → ?); 15 lapply (refl ? (step … s)) 16 cases (step … s) in ⊢ (???% → %); 17 [ #o #k #_ * 18  * #tr1 #s1 #ST whd in ⊢ (% → ?); 19 cases n' in IH ⊢ %; 20 [ #_ whd in ⊢ (% → ?); #p % [2: % [2: %{p} whd >F whd >ST whd %  skip ]  skip ] 21  #n'' #IH lapply (refl ? (avs_inv avs s1)) cases (avs_inv avs s1) in ⊢ (???% → %); 22 [ #INV #AF 23 cases (IH … AF) #tr' * #s' * #p #AF' 24 % [2: % [2: %{p} whd >F whd >ST whd >INV @AF'  skip ]  skip ] 25  #_ * 26 ] 27 ] 28  #m #_ * 29 ] 30  #r #F * 31 ] 32 ] qed. 33 34 lemma after_n_result : ∀n,O,I,exec,g,s,P,inv. 35 after_n_steps n O I exec g s inv P → 36 ∃tr',s'. 37 P tr' s' ∧ 38 after_n_steps n O I exec g s inv (λtr'',s''. 〈tr'',s''〉 = 〈tr',s'〉). 39 #n #O #I #exec #g #s #P #inv #A 40 cases (after_aux_result … A) #tr * #s' * #p #A' 41 %{tr} %{s'} %{p} @A' 42 qed. 43 44 45 lemma after_1_of_n_steps' : ∀n,O,I,exec,g,tr,s',s. 46 after_n_steps (S n) O I exec g s (λ_.true) (λtrx,sx. 〈trx,sx〉 = 〈tr,s'〉) → 47 ∃tr1,tr2,s1. 48 is_final … exec g s = None ? ∧ 49 step … exec g s = Value … 〈tr1,s1〉 ∧ 50 tr = tr1⧺tr2 ∧ 51 after_n_steps n O I exec g s1 (λ_.true) (λtrx,sx. 〈trx,sx〉 = 〈tr2,s'〉). 52 #n #O #I #exec #g #tr #s' #s #A 53 cases (after_1_of_n_steps … A) 54 #tr1 * #s1 * * * #F #ST #_ #A' 55 cases (after_n_result … A') 56 #tr'' * #s'' * #E #A'' destruct 57 % [2: % [2: % [2: % [ % [% [ @F  @ST ]  % ]  @A'' ]  skip ]  skip ]  skip ] 58 qed. 59 60 theorem steps_with_labels : ∀ge,ge'. 4 (* Combine the results about switch removal and labelling to provide a single 5 result linking the input Clight program with the cost labelled Clight 6 program. *) 7 8 (* First lift the step result for labelling to a finite run of steps. *) 9 10 lemma steps_with_labels : ∀ge,ge'. 61 11 related_globals_gen … label_fundef ge ge' → 62 12 ∀n,s1,s1',tr,s2. … … 138 88 #tr #s #tr' #s' #E destruct % 139 89 qed. 90 91 (* Now build the coinduction simulation, taking one step to many after switch 92 removal, then use steps_with_labels to take those to the cost labelled 93 version. *) 140 94 141 95 let corec build_exec … … 210 164 ] qed. 211 165 166 (* And deal with the start of the program to tie up everything nicely. *) 167 212 168 theorem switch_and_labelling_sim : ∀p. 213 169 let e1 ≝ exec_inf … clight_fullexec p in
Note: See TracChangeset
for help on using the changeset viewer.