Changeset 2570 for src/common


Ignore:
Timestamp:
Jan 5, 2013, 1:41:13 PM (7 years ago)
Author:
piccolo
Message:

ERTLtoERTLptr in place

Location:
src/common
Files:
1 added
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/extraGlobalenvs.ma

    r2478 r2570  
    193193>(find_funct_ptr_transf … EQfunct) #EQ'' destruct %
    194194qed.
     195
     196
     197include alias "common/PositiveMap.ma".
     198
     199lemma add_functs_functions_miss : ∀F. ∀ge : genv_t F.∀ l.∀ id.
     200id < (nextfunction ? ge) →
     201lookup_opt … id (functions ? ge) = None ? →
     202lookup_opt … id (functions … (add_functs F ge l)) = None ?.
     203#F #ge #l #id whd in match add_functs; normalize nodelta
     204elim 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
     212qed.
     213
     214lemma add_globals_functions_miss : ∀F,V,init. ∀gem : genv_t F × mem.∀ id,l.
     215lookup_opt … id (functions ? (\fst gem)) = None ? →
     216lookup_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;
     219normalize nodelta #IND #m #ge #H whd in match (foldl ?????); normalize nodelta
     220cases(alloc m ? ? x2) #m1 #bl1 normalize nodelta @IND whd in match add_symbol;
     221normalize nodelta inversion(lookup_opt ? ? ?) [ #_ %]
     222#f1 #H3 <(drop_fn_lfn … f1 H3) assumption
     223qed.
     224
     225 
     226lemma 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
     230whd in match find_funct_ptr; normalize nodelta
     231whd in match globalenv;
     232whd in match globalenv_allocmem; normalize nodelta
     233@add_globals_functions_miss @add_functs_functions_miss normalize //
     234qed.
     235
     236
     237
Note: See TracChangeset for help on using the changeset viewer.