Ignore:
Timestamp:
Jul 24, 2012, 7:40:21 PM (7 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/Clight/toCminor.ma

    r2251 r2252  
    965965| MemDest e1' ⇒ OK ? «St_store ? e1' e2', ?»
    966966].
    967 % try (//)  try (elim e2' //) elim e1' //
     967% try (//) elim e2' /2/ elim e1' /2/
    968968qed.
    969969
     
    12671267    OK ? «〈fgens1, St_cost l s1'〉, ?»
    12681268].
    1269 try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj
     1269try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj
    12701270try (@I)
    12711271try (#l #H elim H)
     
    13381338                | 2,5: #H %1 %2 assumption
    13391339                | 3,6: #H %2 assumption ] ]
    1340 try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @I try assumption
     1340try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @I try assumption
    13411341[ 1,7,17: whd elim e1' #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal)
    13421342| (*2,8: @(stmt_P_mp … Hstmt_inv1) #s0 #Hstmt_vars @(stmt_vars_mp … Hstmt_vars) //
     
    15501550lemma stmt_P_conj : ∀ (P1:stmt → Prop). ∀ (P2:stmt → Prop). ∀ s. stmt_P P1 s → stmt_P P2 s → stmt_P (λs.P1 s ∧ P2 s) s.
    15511551#P1 #P2 #s elim s
    1552 normalize try @conj try @conj try /3/
    1553 [ #z0 #s #Hind1 #Hind2 * * #HA #HB #HC * * #HD #HE #HF try @conj try @conj try @conj try /2/
    1554 | #H5 #H6 #H7 #H8 #H9 #H10 #H11 * * #H15 #H16 #H17 * * #H20 #H21 #H22
    1555   try @conj try @conj try @conj try /2/
    1556 | *: #H36 #H37 #H38 * #H42 #H43 * #H46 #H47 try @conj try @conj try @conj try /2/ ]
     1552normalize /6 by proj1, proj2, conj/
    15571553qed.
    15581554
Note: See TracChangeset for help on using the changeset viewer.