Changeset 2252 for src/Cminor/syntax.ma


Ignore:
Timestamp:
Jul 24, 2012, 7:40:21 PM (8 years ago)
Author:
campbell
Message:

Use the return statement invariant. Restructure the invariants for Cminor
a bit to make them more understandable.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/syntax.ma

    r2251 r2252  
    5151| St_cost : costlabel → stmt → stmt.
    5252
     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
    5356let rec stmt_P (P:stmt → Prop) (s:stmt) on s : Prop ≝
    5457match s with
    55 [ St_seq s1 s2 ⇒ P s ∧ stmt_P P s1 ∧ stmt_P P s2
    56 | St_ifthenelse _ _ _ s1 s2 ⇒ P s ∧ stmt_P P s1 ∧ stmt_P P s2
     58[ 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)
    5760| St_label _ s' ⇒ P s ∧ stmt_P P s'
    5861| St_cost _ s' ⇒ P s ∧ stmt_P P s'
    59 | _ ⇒ P s
     62| _ ⇒ P s ∧ True
    6063].
    6164
    6265lemma 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/
     67qed.
    6868
    6969(* Assert a predicate on every variable or parameter identifier. *)
     
    9191
    9292lemma 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/
     94qed.
    9995
    10096lemma 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.