Ignore:
Timestamp:
Jun 6, 2012, 6:24:43 PM (7 years ago)
Author:
campbell
Message:

Split out special induction principle for Clight from soundness file.
Put cast simplification into compiler.ma.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/SimplifyCasts.ma

    r2011 r2019  
    20462046// qed.
    20472047
    2048 include "CexecSound.ma".
    2049 
    2050 definition expr_lvalue_ind_combined ≝
    2051 λP,Q,ci,cf,lv,vr,dr,ao,uo,bo,ca,cd,ab,ob,sz,fl,co,xx.
    2052 conj ??
    2053  (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx)
    2054  (lvalue_expr_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx).
     2048include "Clight/CexecInd.ma".
    20552049 
    20562050lemma simulation_transitive : ∀A,r0,r1,r2. simulate A r0 r1 → simulate A r1 r2 → simulate A r0 r2.
Note: See TracChangeset for help on using the changeset viewer.