Ignore:
Timestamp:
Mar 23, 2011, 2:28:55 PM (9 years ago)
Author:
campbell
Message:

Use a more normalize-friendly definition of clight_exec to make the destruct
tactic usable again, and recomplete the equivalence proof.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/CexecSound.ma

    r700 r708  
    536536  ]
    537537qed.
     538
     539lemma is_final_sound: ∀s,r. is_final s = Some ? r → final_state s r.
     540* [ 3: #v * [ #m #r cases v [ 2: #r' #E normalize in E; destruct %
     541                            | *: normalize #x1 try #x2 try #x3 try #x4 try #x5 destruct
     542                            ]
     543            | *: normalize #x1 try #x2 try #x3 try #x4 try #x5 try #x6 try #x7 destruct
     544            ]
     545  | *: normalize #x1 #x2 #x3 #x4 #x5 #x6 try #x7 destruct
     546  ] qed.
Note: See TracChangeset for help on using the changeset viewer.