Changeset 1336
 Timestamp:
 Oct 10, 2011, 3:54:59 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/CexecSound.ma
r1244 r1336 33 33 lemma bool_of: ∀v,ty,b. bool_of_val v ty (of_bool b) → 34 34 if b then is_true v ty else is_false v ty. 35 #v #ty #b cases b; #H inversion H; #v' #ty' #H' #ev #et #ev //; 36 @False_ind @(absurd ? ev ?) 37 [ 2: @sym_neq ] @bool_val_distinct 35 #v #ty #b cases b; #H inversion H; #v' #ty' #H' #ev #et #ev' //; 36 @⊥ cases (bool_val_distinct) #X @X [2: @sym_eq] @ev' 38 37 qed. 39 38 … … 51 50 qed. 52 51 53 definitionexec_cast_sound : ∀m:mem. ∀v:val. ∀ty:type. ∀ty':type. ∀v':val. exec_cast m v ty ty' = OK ? v' → cast m v ty ty' v'.54 #m #v #ty #ty' #v'52 axiom exec_cast_sound : ∀m:mem. ∀v:val. ∀ty:type. ∀ty':type. ∀v':val. exec_cast m v ty ty' = OK ? v' → cast m v ty ty' v'. 53 (*#m #v #ty #ty' #v' 55 54 cases v; 56 55 [ #H whd in H:(??%?); destruct; … … 123 122 ] 124 123 ] 125 ] qed. 124 ] qed.*) 126 125 127 126 let rec expr_lvalue_ind
Note: See TracChangeset
for help on using the changeset viewer.