 Timestamp:
 Nov 9, 2012, 4:01:12 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/lineariseProof.ma
r2446 r2447 148 148 qed. 149 149 150 axiomsigma_pc_commute:150 lemma sigma_pc_commute: 151 151 ∀p,p',graph_prog,s1,prf. 152 152 sigma_pc_of_status p p' graph_prog (choose_sigma p p' graph_prog) s1 prf = … … 155 155 (pc (lin_prog_params p p' (linearise p graph_prog)) 156 156 (linearise_status_fun p p' graph_prog (choose_sigma p p' graph_prog) s1 prf)). 157 #p #p' #prog #s #prf whd in ⊢ (??%%); change with (? = nat_of_bitvector ??); 158 whd in match (pc … (linearise_status_fun …)); 159 >nat_of_bitvector_bitvector_of_nat_inverse // 160 cases daemon (* CSC: Paolo, you must prove this additional invariant! *) 161 qed. 157 162 158 163 definition linearise_status_rel: … … 170 175 qed. 171 176 172 axiom fetch_function_sigma_commute: 177 (* To be added to common/Globalenvs, it strenghtens 178 find_funct_ptr_transf *) 179 lemma 180 find_funct_ptr_transf_eq: 181 ∀A,B,V,iV. ∀p: program A V. ∀transf: (∀vs. A vs → B vs). 182 ∀b: block. 183 find_funct_ptr ? (globalenv … iV (transform_program … p transf)) b = 184 m_map ??? 185 (transf …) 186 (find_funct_ptr ? (globalenv … iV p) b). 187 #A #B #V #iV #p #transf #b inversion (find_funct_ptr ???) in ⊢ (???%); 188 [ cases daemon (* TODO in Globalenvs.ma *) 189  #f #H >(find_funct_ptr_transf A B … H) // ] 190 qed. 191 192 lemma fetch_function_sigma_commute: 173 193 ∀p,p',graph_prog,sigma,st1. 174 194 ∀prf:well_formed_status ??? sigma st1. … … 188 208 (ev_genv (graph_prog_params p p' graph_prog)) 189 209 (pc (graph_prog_params p p' graph_prog) st1)). 210 #p #p' #prog #sigma #st #prf whd in match fetch_function; normalize nodelta 211 whd in match function_of_block; normalize nodelta 212 >(find_funct_ptr_transf_eq … (λglobals.transf_fundef … (linearise_int_fun … globals)) …) 213 cases (find_funct_ptr ???) // * // 214 qed. 190 215 191 216 lemma stm_at_sigma_commute:
Note: See TracChangeset
for help on using the changeset viewer.