Changeset 2319 for src/common/Globalenvs.ma
 Timestamp:
 Sep 3, 2012, 1:16:29 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/Globalenvs.ma
r2226 r2319 770 770 // 771 771 qed. 772 773 lemma 774 init_mem_transf_gen: 775 ∀tag,A,B,V,iV,g. ∀transf: (∀vs. universe tag → A vs → B vs × (universe tag)). ∀p: program A V. 776 init_mem … iV (\fst (transform_program_gen … g p transf)) = init_mem … iV p. 777 #tag #A #B #C #iV #g #transf #p 778 @(init_mem_match … (transform_program_gen_match … transf ?)) 779 // 780 qed. 772 781 773 782 … … 791 800  @(find_funct_transf A B V iV tf p) 792 801  @(find_funct_ptr_transf A B V iV p tf) 802 ] qed. 803 804 record related_globals_gen (tag:String) (A,B:Type[0]) (t: universe tag → A → B × (universe tag)) (ge:genv_t A) (ge':genv_t B) : Prop ≝ { 805 rgg_find_symbol: ∀s. 806 find_symbol … ge s = find_symbol … ge' s; 807 rgg_find_funct_ptr: ∀b,f. 808 find_funct_ptr … ge b = Some ? f → 809 ∃g. find_funct_ptr … ge' b = Some ? (\fst (t g f)); 810 rgg_find_funct: ∀v,f. 811 find_funct … ge v = Some ? f → 812 ∃g. find_funct … ge' v = Some ? (\fst (t g f)) 813 }. 814 815 include "utilities/bool.ma". 816 817 theorem transform_program_gen_related : ∀tag,A,B,V,init,g,p. ∀tf:∀vs. universe tag → A vs → B vs × (universe tag). 818 related_globals_gen tag (A ?) (B ?) (tf ?) (globalenv A V init p) (globalenv B V init (\fst (transform_program_gen tag A B V g p tf))). 819 #tag #A #B #V #iV #g #p #tf % 820 [ #s @sym_eq @(find_symbol_match … (transform_program_gen_match … tf p)) 821 #v #w * // 822  #b #f #FFP 823 cases (find_funct_ptr_match … (transform_program_gen_match … tf p) … FFP) 824 [ 2: @iV 825  #fn' * #FFP' 826 generalize in match (matching_vars ????); 827 whd in match (prog_var_names ???); whd in match (prog_vars ???); 828 #E >(K ?? E) * #g1 * #g2 whd in ⊢ (??%% → ?); #E' >FFP' %{g1} >E' % 829  skip 830 ] 831  * [5: #ptr #fn whd in match (find_funct ???); 832 @if_elim #Eoff #FFP 833 [ cases (find_funct_ptr_match … (transform_program_gen_match … tf p) … FFP) 834 [ 2: @iV 835  #fn' * #FFP' 836 generalize in match (matching_vars ????); 837 whd in match (prog_var_names ???); whd in match (prog_vars ???); 838 #E >(K ?? E) * #g1 * #g2 whd in ⊢ (??%% → ?); #E' 839 %{g1} whd in ⊢ (??%?); >Eoff >FFP' >E' % 840 ] 841  destruct 842 ] 843  *: normalize #A #B try #C try #D destruct 844 ] 793 845 ] qed. 794 846
Note: See TracChangeset
for help on using the changeset viewer.