Changeset 2252 for src/Cminor/syntax.ma
 Timestamp:
 Jul 24, 2012, 7:40:21 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Cminor/syntax.ma
r2251 r2252 51 51  St_cost : costlabel → stmt → stmt. 52 52 53 (* Apply a predicate to every statement. Be careful with grouping so that the 54 local application is the first conjunct, and substatements the second. *) 55 53 56 let rec stmt_P (P:stmt → Prop) (s:stmt) on s : Prop ≝ 54 57 match s with 55 [ St_seq s1 s2 ⇒ P s ∧ stmt_P P s1 ∧ stmt_P P s256  St_ifthenelse _ _ _ s1 s2 ⇒ P s ∧ stmt_P P s1 ∧ stmt_P P s258 [ St_seq s1 s2 ⇒ P s ∧ (stmt_P P s1 ∧ stmt_P P s2) 59  St_ifthenelse _ _ _ s1 s2 ⇒ P s ∧ (stmt_P P s1 ∧ stmt_P P s2) 57 60  St_label _ s' ⇒ P s ∧ stmt_P P s' 58 61  St_cost _ s' ⇒ P s ∧ stmt_P P s' 59  _ ⇒ P s 62  _ ⇒ P s ∧ True 60 63 ]. 61 64 62 65 lemma stmt_P_P : ∀P,s. stmt_P P s → P s. 63 #P * normalize /2/ 64 [ #s1 #s2 * * /2/ 65  #sz #sg #e #s1 #s2 * * /2/ 66  *: #i #s normalize * /2/ 67 ] qed. 66 #P * normalize * /3 by proj1/ 67 qed. 68 68 69 69 (* Assert a predicate on every variable or parameter identifier. *) … … 91 91 92 92 lemma stmt_P_mp : ∀P,Q. (∀s. P s → Q s) → ∀s. stmt_P P s → stmt_P Q s. 93 #P #Q #H #s elim s /2/ 94 [ #s1 #s2 #H1 #H2 normalize * * /4/ 95  #sz #sg #e #s1 #s2 #H1 #H2 * * /5/ 96  #l #s #H * /5/ 97  #l #s #H * /5/ 98 ] qed. 93 #P #Q #H #s elim s /6 by proj1, proj2, conj/ 94 qed. 99 95 100 96 lemma stmt_vars_mp : ∀P,Q. (∀i,t. P i t → Q i t) → ∀s. stmt_vars P s → stmt_vars Q s.
Note: See TracChangeset
for help on using the changeset viewer.