Changeset 2588 for src/Clight/switchRemoval.ma
 Timestamp:
 Jan 23, 2013, 2:38:06 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/switchRemoval.ma
r2510 r2588 2124 2124 (* Conservation of the semantics of binary operators under memory extensions. 2125 2125 Tried to factorise it a bit but the play with indexes just becomes too messy. *) 2126 lemma sim_sem_binary_operation : ∀op,v1,v2,e1,e2,m1,m2, writeable.2126 lemma sim_sem_binary_operation : ∀op,v1,v2,e1,e2,m1,m2,target_type,writeable. 2127 2127 ∀Hext:sr_memext m1 m2 writeable. ∀res. 2128 sem_binary_operation op v1 (typeof e1) v2 (typeof e2) m1 = Some ? res →2129 sem_binary_operation op v1 (typeof e1) v2 (typeof e2) m2 = Some ? res.2130 #op #v1 #v2 #e1 #e2 #m1 #m2 # writeable #Hmemext #res cases op2131 whd in match (sem_binary_operation ?????? );2128 sem_binary_operation op v1 (typeof e1) v2 (typeof e2) m1 target_type = Some ? res → 2129 sem_binary_operation op v1 (typeof e1) v2 (typeof e2) m2 target_type = Some ? res. 2130 #op #v1 #v2 #e1 #e2 #m1 #m2 #target_type #writeable #Hmemext #res cases op 2131 whd in match (sem_binary_operation ???????); 2132 2132 try // 2133 whd in match (sem_binary_operation ?????? );2133 whd in match (sem_binary_operation ???????); 2134 2134 lapply (me_valid_pointers … Hmemext) 2135 2135 lapply (me_not_writeable_ptr … Hmemext) … … 2282 2282 >(Hsim2 ? (refl ??)) 2283 2283 whd in match (m_bind ?????); 2284 lapply (sim_sem_binary_operation op v pval e1 e2 m1 m2 writeable Hext)2285 cases (sem_binary_operation op v (typeof e1) pval (typeof e2) m1 )2284 lapply (sim_sem_binary_operation op v pval e1 e2 m1 m2 ty writeable Hext) 2285 cases (sem_binary_operation op v (typeof e1) pval (typeof e2) m1 ty) 2286 2286 [ 1: #_ // ] #val #H >(H val (refl ??)) 2287 2287 normalize destruct @conj @refl … … 2319 2319 whd in match (m_bind ?????); 2320 2320 whd in match (m_bind ?????); 2321 [ 2,3: normalize@conj try @refl ]2321 [ 2,3: cases (cast_bool_to_target ty ?) normalize // #v @conj try @refl ] 2322 2322 cases (exec_expr ge en1 m1 e2) in Hsim2; 2323 2323 [ 2,4: #error #_ normalize @I ] … … 2326 2326 cases (exec_bool_of_val v2 (typeof e2)) 2327 2327 [ 2,4: #error normalize @I ] 2328 * normalize @conj @refl 2328 * 2329 whd in match (m_bind ?????); 2330 cases (cast_bool_to_target ty ?) normalize // #v @conj try @refl 2329 2331  12: #ty #ty' cases ty 2330 2332 [  #sz #sg  #ty  #ty #n  #tl #ty  #id #fl  #id #fl  #ty ]
Note: See TracChangeset
for help on using the changeset viewer.