Changeset 2481 for src/joint/lineariseProof.ma
 Timestamp:
 Nov 20, 2012, 6:40:08 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/lineariseProof.ma
r2476 r2481 18 18 include "joint/semanticsUtils.ma". 19 19 20 21 lemma ok_is_internal_function_of_program_noinit :22 ∀A.∀prog:program (λvars.fundef (A vars)) ℕ.∀i.23 is_internal_function_of_program … prog i →24 is_internal_function ? (globalenv_noinit ? prog) i ≝25 λA,prog.ok_is_internal_function_of_program … prog.26 27 lemma is_internal_function_of_program_ok_noinit :28 ∀A.∀prog:program (λvars.fundef (A vars)) ℕ.∀i.29 is_internal_function ? (globalenv_noinit ? prog) i →30 is_internal_function_of_program … prog i ≝31 λA,prog.is_internal_function_of_program_ok … prog.32 33 definition if_in_global_env_to_if_in_prog_noinit :34 ∀A.∀prog:program (λvars.fundef (A vars)) ℕ.35 (Σi.is_internal_function ? (globalenv_noinit ? prog) i) →36 Σi.is_internal_function_of_program ?? prog i ≝37 λA,prog,f.«f, is_internal_function_of_program_ok_noinit … (pi2 … f)».38 39 (*40 coercion if_in_prog_from_if_in_global_env nocomposites :41 ∀A.∀prog:program (λvars.fundef (A vars)) ℕ.42 ∀f:Σi.is_internal_function ? (globalenv_noinit ? prog) i.43 Σi.is_internal_function_of_program ?? prog i ≝44 if_in_global_env_to_if_in_prog_noinit45 on _f : Sig ident (λi.is_internal_function ?? i)46 to Sig ident (λi.is_internal_function_of_program ??? i).47 *)48 49 20 definition graph_prog_params ≝ 50 21 λp,p',prog,stack_sizes. … … 127 98 128 99 definition sigma_pc_opt: 129 ∀p,p' ,graph_prog,stack_sizes.100 ∀p,p'.∀graph_prog : joint_program (mk_graph_params p). 130 101 ((Σi.is_internal_function_of_program … graph_prog i) → 131 102 code_point (mk_graph_params p) → option ℕ) → 132 103 program_counter → option program_counter 133 104 ≝ 134 λp,p',prog,s tack_sizes,sigma,pc.135 let pars ≝ graph_prog_params p p' prog stack_sizesin136 let ge ≝ ev_genv parsin105 λp,p',prog,sigma,pc. 106 let pars ≝ make_sem_graph_params p p' in 107 let ge ≝ globalenv_noinit … prog in 137 108 ! f ← int_funct_of_block ? ge (pc_block pc) ; 138 ! lin_point ← sigma (pi1 … f)(point_of_pc ? pars pc) ;109 ! lin_point ← sigma f (point_of_pc ? pars pc) ; 139 110 return pc_of_point ? (make_sem_lin_params ? p') pc lin_point. 140 @(is_internal_function_of_program_ok … prog … (pi2 … f))141 qed.142 111 143 112 definition well_formed_pc: 144 ∀p,p',graph_prog ,stack_sizes.113 ∀p,p',graph_prog. 145 114 ((Σi.is_internal_function_of_program … graph_prog i) → 146 115 label → option ℕ) → 147 116 program_counter → Prop 148 117 ≝ 149 λp,p',prog,s tack_sizes,sigma,pc.150 sigma_pc_opt p p' prog s tack_sizes sigma pc118 λp,p',prog,sigma,pc. 119 sigma_pc_opt p p' prog sigma pc 151 120 ≠ None …. 152 121 153 122 definition well_formed_status: 154 ∀p,p',graph_prog ,stack_sizes.123 ∀p,p',graph_prog. 155 124 ((Σi.is_internal_function_of_program … graph_prog i) → 156 125 label → option ℕ) → 157 126 state_pc (make_sem_graph_params p p') → Prop ≝ 158 λp,p',prog,s tack_sizes,sigma,st.159 well_formed_pc p p' prog s tack_sizes sigma (pc … st) ∧ ?.127 λp,p',prog,sigma,st. 128 well_formed_pc p p' prog sigma (pc … st) ∧ ?. 160 129 cases daemon (* TODO *) 161 130 qed. … … 188 157 *) 189 158 definition sigma_pc : 190 ∀p,p',graph_prog ,stack_sizes.159 ∀p,p',graph_prog. 191 160 ∀sigma : ((Σi.is_internal_function_of_program … graph_prog i) → 192 161 label → option ℕ). 193 162 ∀pc. 194 ∀prf : well_formed_pc p p' graph_prog s tack_sizes sigma pc.163 ∀prf : well_formed_pc p p' graph_prog sigma pc. 195 164 program_counter ≝ 196 λp,p',graph_prog,s tack_sizes,sigma,st.opt_safe ….165 λp,p',graph_prog,sigma,st.opt_safe …. 197 166 198 167 lemma sigma_pc_of_status_ok: 199 ∀p,p',graph_prog ,stack_sizes.168 ∀p,p',graph_prog. 200 169 ∀sigma. 201 170 ∀pc. 202 ∀prf:well_formed_pc p p' graph_prog stack_sizes sigma pc. 203 sigma_pc_opt p p' graph_prog stack_sizes sigma pc = 204 Some … (sigma_pc p p' graph_prog stack_sizes sigma pc prf). 205 #p #p' #graph_prog #stack_sizes #sigma #st #prf @opt_to_opt_safe qed. 206 171 ∀prf:well_formed_pc p p' graph_prog sigma pc. 172 sigma_pc_opt p p' graph_prog sigma pc = 173 Some … (sigma_pc p p' graph_prog sigma pc prf). 174 #p #p' #graph_prog #sigma #st #prf @opt_to_opt_safe qed. 207 175 208 176 definition sigma_state : 209 177 ∀p. 210 178 ∀p':∀F.sem_unserialized_params p F. 211 ∀graph_prog ,stack_sizes.179 ∀graph_prog. 212 180 ∀sigma. 213 181 (* let lin_prog ≝ linearise ? graph_prog in *) 214 ∀s:state_pc ( p' ?). (* = graph_abstract_status p p' graph_prog stack_sizes *)215 well_formed_status p p' graph_prog s tack_sizes sigma s →182 ∀s:state_pc (make_sem_graph_params p p'). (* = graph_abstract_status p p' graph_prog stack_sizes *) 183 well_formed_status p p' graph_prog sigma s → 216 184 state_pc (make_sem_lin_params p p') (* = lin_abstract_status p p' lin_prog ? *) 217 185 ≝ 218 λp,p',graph_prog,s tack_sizes,sigma,s,prf.186 λp,p',graph_prog,sigma,s,prf. 219 187 let pc' ≝ sigma_pc … (proj1 … prf) in 220 188 mk_state_pc ? ? pc'. … … 222 190 223 191 lemma sigma_pc_commute: 224 ∀p,p',graph_prog,s tack_sizes,sigma,st.225 ∀prf : well_formed_status p p' graph_prog s tack_sizes sigma st.192 ∀p,p',graph_prog,sigma,st. 193 ∀prf : well_formed_status p p' graph_prog sigma st. 226 194 sigma_pc … (pc ? st) (proj1 … prf) = 227 195 pc ? (sigma_state … st prf). 228 #p #p' #prog #s tack_sizes #sigma #st #prf %196 #p #p' #prog #sigma #st #prf % 229 197 qed. 230 198 … … 234 202 235 203 definition sigma_function_name : 236 ∀p, p',graph_prog.204 ∀p,graph_prog. 237 205 let lin_prog ≝ linearise p graph_prog in 238 ∀lin_stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ. 239 let graph_stack_sizes ≝ 240 stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p') 241 ? graph_prog lin_stack_sizes in 242 (Σf.is_internal_function … (ev_genv (graph_prog_params p p' graph_prog graph_stack_sizes)) f) → 243 (Σf.is_internal_function … (ev_genv (lin_prog_params p p' lin_prog lin_stack_sizes)) f) ≝ 244 λp,p',graph_prog,lin_stack_sizes,f.pi1 … f. 245 @(ok_is_internal_function_of_program ??? (linearise … graph_prog) ??) 246 @if_propagate 247 @is_internal_function_of_program_ok [2: @(pi2 … f) ] 248 qed. 206 (Σf.is_internal_function_of_program … graph_prog f) → 207 (Σf.is_internal_function_of_program … lin_prog f) ≝ 208 λp,graph_prog,f.«f, if_propagate … (pi2 … f)». 249 209 250 210 lemma if_of_function_commute: 251 ∀p,p'.∀graph_prog : joint_program (mk_graph_params p).∀stack_sizes. 252 ∀graph_fun,prf. 253 let graph_fd ≝ if_of_function ? (globalenv_noinit … graph_prog) graph_fun in 254 let lin_fun ≝ sigma_function_name p p' graph_prog stack_sizes «graph_fun, prf» in 211 ∀p. 212 ∀graph_prog : joint_program (mk_graph_params p). 213 ∀graph_fun : Σi.is_internal_function_of_program … graph_prog i. 214 let graph_fd ≝ if_of_function … graph_fun in 215 let lin_fun ≝ sigma_function_name … graph_fun in 255 216 let lin_fd ≝ if_of_function … lin_fun in 256 217 lin_fd = \fst (linearise_int_fun ?? graph_fd). 257 #p #p' #graph_prog #stack_sizes #graph_fun #prf whd 258 (* Old comment? usare match_opt_prf_elim ? *) 259 cases daemon (* Job for Paolo *) qed. 218 #p #graph_prog #graph_fun whd 219 @prog_if_of_function_transform % qed. 260 220 261 221 lemma bind_opt_inversion: … … 271 231 ∀p,p',graph_prog. 272 232 let lin_prog ≝ linearise p graph_prog in 273 ∀lin_stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.274 let graph_stack_sizes ≝275 stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')276 ? graph_prog lin_stack_sizes in277 233 ∀sigma,pc. 278 ∀prf : well_formed_pc p p' graph_prog graph_stack_sizessigma pc.279 pc_block (sigma_pc ? p' graph_prog graph_stack_sizessigma pc prf) =234 ∀prf : well_formed_pc p p' graph_prog sigma pc. 235 pc_block (sigma_pc ? p' graph_prog sigma pc prf) = 280 236 pc_block pc. 281 #p #p' #graph_prog #s tack_sizes #sigma #pc #prf237 #p #p' #graph_prog #sigma #pc #prf 282 238 whd in match sigma_pc; normalize nodelta 283 239 @opt_safe_elim #x #x_spec … … 287 243 qed. 288 244 245 (* 289 246 lemma bind_opt_non_none : ∀A,B : Type[0] . ∀ m : option A . ∀g : A → option B. 290 247 (! x ← m ; g x) ≠ None ? → m ≠ None ?. … … 300 257 #A #B #C #m #x #b #f #g #H1 #H2 % #m_eq_none >m_eq_none in H1; normalize #H elim H H #H @H assumption 301 258 qed. 302 303 axiom int_funct_of_block_transf_commute: 259 *) 260 261 lemma funct_of_block_transf : 262 ∀A,B.∀progr : program (λvars .fundef (A vars)) ℕ. 263 ∀transf : ∀vars. A vars → B vars. ∀bl,f,prf. 264 let progr' ≝ transform_program … progr (λvars.transf_fundef … (transf vars)) in 265 funct_of_block … (globalenv_noinit … progr) bl = return f → 266 funct_of_block … (globalenv_noinit … progr') bl = return «pi1 … f,prf». 267 #A #B #progr #transf #bl #f #prf whd 268 whd in match funct_of_block in ⊢ (%→?); normalize nodelta 269 cut (∀A,B : Type[0].∀Q : option A → Prop.∀P : B → Prop. 270 ∀o.∀prf : Q o. 271 ∀f1,f2. 272 (∀x,prf.P (f1 x prf)) → (∀prf.P(f2 prf)) → 273 P (match o return λx.Q x → B with [ Some x ⇒ f1 x  None ⇒ f2 ] prf)) 274 [ #A #B #Q #P * /2/ ] #aux 275 @aux [2: #_ change with (?=Some ??→?) #ABS destruct(ABS) ] 276 #fd #EQfind whd in ⊢ (??%%→?); 277 generalize in ⊢ (??(??(????%))?→?); #e #EQ destruct(EQ) 278 whd in match funct_of_block; normalize nodelta 279 @aux [ # fd' ] 280 [2: >(find_funct_ptr_transf … EQfind) #ABS destruct(ABS) ] 281 #prf' cases daemon qed. 282 283 lemma description_of_function_transf : 284 ∀A,B.∀progr : program (λvars .fundef (A vars)) ℕ. 285 ∀transf : ∀vars. A vars → B vars. 286 let progr' ≝ transform_program … progr (λvars.transf_fundef … (transf vars)) in 287 ∀f_out,prf. 288 description_of_function … 289 (globalenv_noinit … progr') f_out = 290 transf_fundef … (transf ?) (description_of_function … (globalenv_noinit … progr) 291 «pi1 … f_out, prf»). 292 #A #B #progr #transf #f_out #prf 293 whd in match description_of_function in ⊢ (???%); 294 normalize nodelta 295 cut (∀A,B : Type[0].∀Q : option A → Prop.∀P : B → Prop. 296 ∀o.∀prf : Q o. 297 ∀f1,f2. 298 (∀x,prf.o = Some ? x → P (f1 x prf)) → (∀prf.o = None ? → P(f2 prf)) → 299 P (match o return λx.Q x → B with [ Some x ⇒ f1 x  None ⇒ f2 ] prf)) 300 [ #A #B #Q #P * /2/ ] #aux 301 @aux 302 [ #fd' ] * #fd #EQ destruct (EQ) 303 inversion (find_symbol ???) [ #_ whd in ⊢ (??%?→?); #ABS destruct(ABS) ] 304 #bl #EQfind >m_return_bind #EQfindf 305 whd in match description_of_function; normalize nodelta 306 @aux 307 [ #fdo' ] * #fdo #EQ destruct (EQ) 308 >find_symbol_transf >EQfind >m_return_bind 309 >(find_funct_ptr_transf … EQfindf) #EQ destruct(EQ) % 310 qed. 311 312 313 lemma match_int_fun : 314 ∀A,B : Type[0].∀P : B → Prop. 315 ∀Q : fundef A → Prop. 316 ∀m : fundef A. 317 ∀f1 : ∀fd.Q (Internal \ldots fd) → B. 318 ∀f2 : ∀fd.Q (External … fd) → B. 319 ∀prf : Q m. 320 (∀fd,prf.P (f1 fd prf)) → 321 (∀fd,prf.P (f2 fd prf)) → 322 P (match m 323 return λx.Q x → ? 324 with 325 [ Internal fd ⇒ f1 fd 326  External fd ⇒ f2 fd 327 ] prf). 328 #A #B #P #Q * // qed. 329 (*) 330 lemma match_int_fun : 331 ∀A,B : Type[0].∀P : B → Prop. 332 ∀m : fundef A. 333 ∀f1 : ∀fd.m = Internal … fd → B. 334 ∀f2 : ∀fd.m = External … fd → B. 335 (∀fd,prf.P (f1 fd prf)) → 336 (∀fd,prf.P (f2 fd prf)) → 337 P (match m 338 return λx.m = x → ? 339 with 340 [ Internal fd ⇒ f1 fd 341  External fd ⇒ f2 fd 342 ] (refl …)). 343 #A #B #P * // qed. 344 *) 345 (* 346 lemma prova : 347 ∀ A.∀progr : program (λvars. fundef (A vars)) ℕ. 348 ∀ M : fundef (A (prog_var_names (λvars:list ident.fundef (A vars)) ℕ progr)). 349 ∀ f,g,prf1. 350 match M return λx.M = x → option (Σi.is_internal_function_of_program ?? progr i) with 351 [Internal fn ⇒ λ prf.return «g,prf1 fn prf»  352 External fn ⇒ λprf.None ? ] (refl ? M) = return f → 353 ∃ fn. ∃ prf : M = Internal ? fn . f = «g, prf1 fn prf». 354 #H1 #H2 #H3 #H4 #H5 #H6 355 @match_int_fun 356 #fd #EQ #EQ' whd in EQ' : (??%%); destruct 357 %[%[ % ]] qed. 358 *) 359 360 lemma int_funct_of_block_transf_commute: 304 361 ∀A,B.∀progr: program (λvars. fundef (A vars)) ℕ. 305 362 ∀transf: ∀vars. A vars → B vars. ∀bl,f,prf. … … 307 364 int_funct_of_block ? (globalenv_noinit … progr) bl = return f → 308 365 int_funct_of_block ? (globalenv_noinit … progr') bl = return «pi1 … f,prf». 366 #A #B #progr #transf #bl #f #prf 367 whd whd in match int_funct_of_block in ⊢ (??%?→?); normalize nodelta 368 #H 369 elim (bind_opt_inversion ??? ?? H) H #x 370 * #x_spec 371 @match_int_fun [2: #fd #_ #ABS destruct(ABS) ] 372 #fd #EQdescr change with (Some ?? = ? → ?) #EQ destruct(EQ) 373 whd in match int_funct_of_block; normalize nodelta 374 >(funct_of_block_transf … (internal_function_is_function … prf) … x_spec) 375 >m_return_bind 376 @match_int_fun #fd' #prf' [ % ] 377 @⊥ cases x in prf EQdescr prf'; x #x #x_prf #prf #EQdescr 378 >(description_of_function_transf) [2: @x_prf ] 379 >EQdescr whd in ⊢ (??%%→?); #ABS destruct qed. 380 309 381 310 382 lemma fetch_function_sigma_commute : 311 383 ∀p,p',graph_prog. 312 384 let lin_prog ≝ linearise p graph_prog in 313 ∀lin_stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.314 let graph_stack_sizes ≝315 stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')316 ? graph_prog lin_stack_sizes in317 385 ∀sigma,pc_st,f. 318 ∀prf : well_formed_pc p p' graph_prog graph_stack_sizessigma pc_st.319 fetch_function … ( ev_genv (graph_prog_params p p' graph_prog graph_stack_sizes)) pc_st =386 ∀prf : well_formed_pc p p' graph_prog sigma pc_st. 387 fetch_function … (globalenv_noinit … graph_prog) pc_st = 320 388 return f 321 → fetch_function … (ev_genv (lin_prog_params p p' lin_prog lin_stack_sizes)) 322 (sigma_pc … pc_st prf) = 389 → fetch_function … (globalenv_noinit … lin_prog) (sigma_pc … pc_st prf) = 323 390 return sigma_function_name … f. 324 #p #p' #graph_prog #s tack_sizes #sigma #st #f #prf391 #p #p' #graph_prog #sigma #st #f #prf 325 392 whd in match fetch_function; normalize nodelta 326 393 >(sigma_pblock_eq_lemma … prf) #H … … 391 458 392 459 lemma stmt_at_sigma_commute: 393 ∀p, p',graph_prog,stack_sizes,graph_fun,prf2,lbl,pt.460 ∀p,graph_prog,graph_fun,lbl,pt. 394 461 let lin_prog ≝ linearise ? graph_prog in 395 let lin_fun ≝ sigma_function_name p p' graph_prog stack_sizesgraph_fun in462 let lin_fun ≝ sigma_function_name p graph_prog graph_fun in 396 463 ∀sigma.good_sigma p graph_prog sigma → 397 sigma «pi1 … graph_fun,prf2»lbl = return pt →464 sigma graph_fun lbl = return pt → 398 465 ∀stmt. 399 466 stmt_at … … … 403 470 (joint_if_code ?? (if_of_function ?? lin_fun)) 404 471 pt = return (graph_to_lin_statement … stmt). 405 #p #p' #graph_prog #stack_sizes #graph_fun #prf2 #lbl #pt #sigma #good #prf 406 #prf 472 #p #graph_prog #graph_fun #lbl #pt #sigma #good #prf 407 473 (* 408 474 whd in match (stmt_at ????); … … 424 490 425 491 lemma fetch_statement_sigma_commute: 426 ∀p,p',graph_prog, lin_stack_sizes,pc,fn,stmt.492 ∀p,p',graph_prog,pc,fn,stmt. 427 493 let lin_prog ≝ linearise ? graph_prog in 428 let graph_stack_sizes ≝429 stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')430 ? graph_prog lin_stack_sizes in431 494 ∀sigma.good_sigma p graph_prog sigma → 432 ∀prf : well_formed_pc p p' graph_prog graph_stack_sizessigma pc.433 fetch_statement ? (make_sem_graph_params p p') … (ev_genv (graph_prog_params p p' graph_prog graph_stack_sizes)) pc =434 return 〈fn,stmt〉 →435 fetch_statement ? (make_sem_lin_params p p') … (ev_genv (lin_prog_params p p' lin_prog lin_stack_sizes))436 (sigma_pc … pc prf) =495 ∀prf : well_formed_pc p p' graph_prog sigma pc. 496 fetch_statement ? (make_sem_graph_params p p') … 497 (globalenv_noinit … graph_prog) pc = return 〈fn,stmt〉 → 498 fetch_statement ? (make_sem_lin_params p p') … 499 (globalenv_noinit … lin_prog) (sigma_pc … pc prf) = 437 500 return 〈sigma_function_name … fn, graph_to_lin_statement … stmt〉. 438 #p #p' #graph_prog # stack_sizes #pc #fn #stmt #sigma #good #wfprf501 #p #p' #graph_prog #pc #fn #stmt #sigma #good #wfprf 439 502 whd in match fetch_statement; normalize nodelta #H 440 cases (bind_inversion ????? H) #id * H # H441 >(fetch_function_sigma_commute … wfprf … H) H>m_return_bind503 cases (bind_inversion ????? H) #id * H #fetchfn 504 >(fetch_function_sigma_commute … wfprf … fetchfn) >m_return_bind 442 505 #H cases (bind_inversion ????? H) #fstmt * H #H 443 506 lapply (opt_eq_from_res ???? H) H #H #EQ whd in EQ:(??%%); destruct 444 >(stmt_at_sigma_commute … good … H) 445 [3: @is_internal_function_of_program_ok [2: @(pi2 … fn)] 446 2: cases daemon (* TO BE DONE, COMMUTATION LEMMA NEEDED *) ] 447 % 507 >(stmt_at_sigma_commute … good … H) [%] 508 whd in match sigma_pc; normalize nodelta 509 @opt_safe_elim #pc' #H 510 cases (bind_opt_inversion ????? H) 511 #i * #EQ1 H #H 512 cases (bind_opt_inversion ????? H) 513 #pnt * #EQ2 whd in ⊢ (??%?→?); #EQ3 destruct 514 whd in match point_of_pc in ⊢ (???%); normalize nodelta >point_of_offset_of_point 515 lapply (opt_eq_from_res ???? fetchfn) >EQ1 #EQ4 destruct @EQ2 448 516 qed. 449 517 … … 461 529 (lin_abstract_status p p' lin_prog stack_sizes) 462 530 ≝ λp,p',graph_prog,stack_sizes,sigma,good. 463 let stack_sizes' ≝464 stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')465 ? graph_prog ? in466 531 mk_status_rel … 467 532 (* sem_rel ≝ *) (λs1,s2. 468 ∃prf: well_formed_status p p' graph_prog s tack_sizes' sigma s1.533 ∃prf: well_formed_status p p' graph_prog sigma s1. 469 534 s2 = sigma_state … s1 prf) 470 535 (* call_rel ≝ *) (λs1,s2. 471 ∃prf:well_formed_status p p' graph_prog s tack_sizes' sigma s1.536 ∃prf:well_formed_status p p' graph_prog sigma s1. 472 537 pc ? s2 = sigma_pc … (pc ? s1) (proj1 … prf)) 473 538 (* sim_final ≝ *) ?. … … 550 615 (*interpretation "exists in Type[1]" 'exists x = (ex_Type1 ? x).*) 551 616 617 lemma err_eq_from_io : ∀O,I,X,m,v. 618 err_to_io O I X m = return v → m = return v. 619 #O #I #X * #x #v normalize #EQ destruct % qed. 552 620 553 621 lemma linearise_ok: … … 566 634 #lin_stack_sizes 567 635 %{(linearise_status_rel p p' graph_prog lin_stack_sizes sigma good)} 568 whd 569 #st1 #cl #st1' #st2 #move_st1_st1' * #wf_st1 #rel_st1_st2 #classified_st1_cl 570 whd in move_st1_st1'; whd in match eval_state in move_st1_st1':(??%?); 571 normalize nodelta in move_st1_st1'; 572 cases (IO_bind_inversion ??????? move_st1_st1') * #fn #stmt * 573 #fetch_statement_spec move_st1_st1' #move_st1_st1' 636 whd whd in ⊢ (%→%→?); 637 change with (∀st1 : state_pc (p' (joint_closed_internal_function (mk_graph_params ?))).?) 638 #st1 639 change with (∀st1 : state_pc (p' (joint_closed_internal_function (mk_graph_params ?))).?) 640 #st1' 641 change with (∀st : state_pc (p' (joint_closed_internal_function (mk_lin_params ?))).?) 642 #st2 643 #ex * #wfprf #rel_st1_st2 644 whd in ex; 645 change with 646 (eval_state 647 (make_sem_graph_params p p') 648 (prog_var_names ?? graph_prog) 649 ? 650 st1 = ?) in ex; 651 whd in match eval_state in ex; 652 normalize nodelta in ex; 653 cases (IO_bind_inversion ??????? ex) in ⊢ ?; * #fn #stmt 654 change with (Σi.is_internal_function_of_program … graph_prog i) in fn; * 655 change with (globalenv_noinit ? graph_prog) in 656 ⊢ (??(???%?)?→?); 657 match (ge ?? (ev_genv ?)) in ⊢ (%→?); 658 st1' 659 whd in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ?  _ ⇒ ?  _ ⇒ ? ]); 660 >fetch_statement_spec in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ?  _ ⇒ ?  _ ⇒ ? ]); 661 whd in fetch_statement_spec : (??()%); 574 662 cases cl in classified_st1_cl; cl #classified_st1_cl whd 575 663 [4:
Note: See TracChangeset
for help on using the changeset viewer.