Changeset 2570 for src/common
 Timestamp:
 Jan 5, 2013, 1:41:13 PM (8 years ago)
 Location:
 src/common
 Files:

 1 added
 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/extraGlobalenvs.ma
r2478 r2570 193 193 >(find_funct_ptr_transf … EQfunct) #EQ'' destruct % 194 194 qed. 195 196 197 include alias "common/PositiveMap.ma". 198 199 lemma add_functs_functions_miss : ∀F. ∀ge : genv_t F.∀ l.∀ id. 200 id < (nextfunction ? ge) → 201 lookup_opt … id (functions ? ge) = None ? → 202 lookup_opt … id (functions … (add_functs F ge l)) = None ?. 203 #F #ge #l #id whd in match add_functs; normalize nodelta 204 elim l l [ #_ normalize //] 205 * #id1 #f1 #tl #IND #H #H1 whd in match (foldr ?????); 206 >lookup_opt_insert_miss [ inversion(lookup_opt ? ? ?) [ #_ %] 207 #f1 #H3 <(drop_fn_lfn … f1 H3) @(IND H H1) 208  cut(nextfunction F ge ≤ nextfunction F (foldr … (add_funct F) ge tl)) 209 [elim tl [normalize //] 210 #x #tl2 whd in match (foldr ?????) in ⊢ (? → %); #H %2{H} ] 211 #H2 lapply(transitive_le … H H2) @lt_to_not_eq 212 qed. 213 214 lemma add_globals_functions_miss : ∀F,V,init. ∀gem : genv_t F × mem.∀ id,l. 215 lookup_opt … id (functions ? (\fst gem)) = None ? → 216 lookup_opt … id (functions … (\fst (add_globals F V init gem l))) = None ?. 217 #F #V #init * #ge #m #id #l lapply ge ge lapply m m elim l [ #ge #m #H @H] 218 ** #x1 #x2 #x3 #tl whd in match add_globals; 219 normalize nodelta #IND #m #ge #H whd in match (foldl ?????); normalize nodelta 220 cases(alloc m ? ? x2) #m1 #bl1 normalize nodelta @IND whd in match add_symbol; 221 normalize nodelta inversion(lookup_opt ? ? ?) [ #_ %] 222 #f1 #H3 <(drop_fn_lfn … f1 H3) assumption 223 qed. 224 225 226 lemma globalenv_no_minus_one : 227 ∀F,V,i,p. 228 find_funct_ptr … (globalenv F V i p) (mk_block Code (1)) = None ?. 229 #F #V #i #p 230 whd in match find_funct_ptr; normalize nodelta 231 whd in match globalenv; 232 whd in match globalenv_allocmem; normalize nodelta 233 @add_globals_functions_miss @add_functs_functions_miss normalize // 234 qed. 235 236 237
Note: See TracChangeset
for help on using the changeset viewer.