Changeset 2251 for src/Cminor/initialisation.ma
 Timestamp:
 Jul 24, 2012, 7:40:21 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Cminor/initialisation.ma
r2249 r2251 19 19 ]. 20 20 21 (* None of the additional code introduces locals or labels. *)21 (* None of the additional code introduces locals, labels or returns. *) 22 22 definition stmt_inv : stmt → Prop ≝ 23 stmt_P (λs. stmt_vars (λ_.λ_.False) s ∧ stmt_labels (λ_.False) s ).23 stmt_P (λs. stmt_vars (λ_.λ_.False) s ∧ stmt_labels (λ_.False) s ∧ match s with [ St_return _ ⇒ False  _ ⇒ True ]). 24 24 25 25 discriminator option. … … 38 38 ] 39 39 ]. 40 % / /40 % /2/ 41 41 cases init in p; [ 7:  8: #a #b  *: #a ] #p normalize in p; 42 destruct;/ 2/42 destruct;/3/ 43 43 qed. 44 44 … … 50 50 〈off + (size_init_data datum), St_seq (init_datum id r datum off) s〉) 51 51 〈0, mk_Sig ? (λx.stmt_inv x) St_skip ?〉 init). 52 [ % / /52 [ % /2/ 53 53  elim init 54 [ % // 55  #h #t #IH whd in ⊢ (?(???%)); @breakup_pair whd in ⊢ (?%); % [ % [ % //  @(pi2 … (init_datum …)) ]  @IH ] 54 [ % /2/ 55  #h #t #IH whd in ⊢ (?(???%)); @breakup_pair whd in ⊢ (?%); 56 % [ % [ % /2/  @(pi2 … (init_datum …)) ]  @IH ] 56 57 ] qed. 57 58 58 59 definition init_vars : list (ident × region × (list init_data)) → Σs:stmt. stmt_inv s ≝ 59 60 λvars. foldr ? (Σs:stmt. stmt_inv s) 60 (λvar,s. mk_Sig ? (λx.stmt_inv x ) (St_seq s (init_var (\fst (\fst var)) (\snd (\fst var)) (\snd var))) ?) (mk_Sig ? (λx.stmt_inv x ) St_skip (conj ?? II)) vars.61 % [ % [ % / /  @(pi2 … s) ]  @(pi2 … (init_var …)) ]61 (λvar,s. mk_Sig ? (λx.stmt_inv x ) (St_seq s (init_var (\fst (\fst var)) (\snd (\fst var)) (\snd var))) ?) (mk_Sig ? (λx.stmt_inv x ) St_skip (conj ?? (conj ?? I I) I)) vars. 62 % [ % [ % /2/  @(pi2 … s) ]  @(pi2 … (init_var …)) ] 62 63 qed. 63 64 64 65 lemma no_labels : ∀s. stmt_inv s → labels_of s = [ ]. 65 66 #s elim s // 66 [ #s1 #s2 #IH1 #IH2 * * * #_ #_ #H1 #H2 whd in ⊢ (??%?);67 [ #s1 #s2 #IH1 #IH2 * * * * #_ #_ #_ #H1 #H2 whd in ⊢ (??%?); 67 68 >(IH1 H1) >(IH2 H2) @refl 68 69  #sz #sg #e #s1 #s2 #IH1 #IH2 * * * #_ #_ #H1 #H2 whd in ⊢ (??%?); 69 70 >(IH1 H1) >(IH2 H2) @refl 70  #l #s #IH * * #_ *71  #l #s #IH * * * #_ * 71 72  #l #s #IH * * #_ #_ #H @(IH H) 72 73 ] qed. … … 95 96 % 96 97 [ % [ % //  97 @(stmt_P_mp … H) #s * #V #L%98 @(stmt_P_mp … H) #s * * #V #L #R % 98 99 [ @(stmt_vars_mp … V) #i #t * 99 100  @(stmt_labels_mp … L) #l * 101  cases s in R ⊢ %; // #x * 100 102 ] 101 103 ]
Note: See TracChangeset
for help on using the changeset viewer.