Ignore:
Timestamp:
Jun 6, 2012, 6:24:43 PM (8 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/labelSimulation.ma

    r2011 r2019  
    22include "Clight/label.ma".
    33include "Clight/Cexec.ma".
    4 
    5 (* for the induction principle *)
    6 include "Clight/CexecSound.ma".
     4include "Clight/CexecInd.ma".
    75
    86(* TODO: make something general that can live in common/Globalenvs.ma. *)
     
    8482#tr1 #tr2 #tr1' #tr2' #twel1 elim twel1 /3/
    8583qed. 
    86 
    87 definition expr_lvalue_ind_combined ≝
    88 λP,Q,ci,cf,lv,vr,dr,ao,uo,bo,ca,cd,ab,ob,sz,fl,co,xx.
    89 conj ??
    90  (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx)
    91  (lvalue_expr_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx).
    9284
    9385theorem label_expr_ok : ∀ge,ge',en,m.
Note: See TracChangeset for help on using the changeset viewer.