Changeset 2143 for src/ASM/ASM.ma
 Timestamp:
 Jul 2, 2012, 11:37:34 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/ASM.ma
r2139 r2143 403 403 qed. 404 404 405 (* XXX: move back into ASM.ma *) 406 lemma subvector_with_to_subvector_with_tl: 407 ∀n: nat. 408 ∀m: nat. 409 ∀v. 410 ∀fixed_v. 411 ∀proof: (subvector_with addressing_mode_tag n (S m) eq_a v fixed_v). 412 ∀n': nat. 413 ∀hd: addressing_mode_tag. 414 ∀tl: Vector addressing_mode_tag n'. 415 ∀m_refl: S n'=n. 416 ∀v_refl: v≃hd:::tl. 417 subvector_with addressing_mode_tag n' (S m) eq_a tl fixed_v. 418 #n #m #v #fixed_v #proof #n' #hd #tl #m_refl #v_refl 419 generalize in match proof; destruct 420 whd in match (subvector_with … eq_a (hd:::tl) fixed_v); 421 cases (mem … eq_a ? fixed_v hd) normalize nodelta 422 [1: 423 whd in match (subvector_with … eq_a tl fixed_v); 424 #assm assumption 425 2: 426 normalize in ⊢ (% → ?); 427 #absurd cases absurd 428 ] 429 qed. 405 430 406 431 let rec subaddressing_mode_elim_type … … 437 462 ] (refl … n) (refl_jmeq … v). 438 463 [20: 439 generalize in match proof; destruct 440 whd in match (subvector_with … eq_a (hd:::tl) fixed_v); 441 cases (mem … eq_a ? fixed_v hd) normalize nodelta 442 [1: 443 whd in match (subvector_with … eq_a tl fixed_v); 444 #assm assumption 445 2: 446 normalize in ⊢ (% → ?); 447 #absurd cases absurd 448 ] 464 @(subvector_with_to_subvector_with_tl … proof … m_refl v_refl) 449 465 ] 450 466 @(is_in_subvector_is_in_supervector … proof) … … 460 476 (∀xaddr: v. ¬ is_in … w xaddr → Q xaddr) → 461 477 subaddressing_mode_elim_type n v addr Q m w H. 462 #n #v #addr #Q #m #w elim w 463 [ /2/ 464  #n' #hd #tl #IH cases hd #H 465 #INV whd #PO @IH #xaddr cases xaddr * 466 try (#b #IS_IN #ALREADYSEEN) try (#IS_IN #ALREADYSEEN) try @PO @INV 467 @ALREADYSEEN ] 478 #n #v #addr #Q #m #w elim w 479 [1: 480 /2/ 481 2: 482 #n' #hd #tl #IH cases hd #H 483 #INV whd #PO @IH #xaddr cases xaddr * 484 try (#b #IS_IN #ALREADYSEEN) try (#IS_IN #ALREADYSEEN) try @PO @INV 485 @ALREADYSEEN 486 ] 468 487 qed. 469 488 … … 474 493 ∀Q: v → Prop. 475 494 subaddressing_mode_elim_type n v addr Q (S n) v ?. 476 [ #n #v #addr #Q @subaddressing_mode_elim0 * #el #H #NH @⊥ >H in NH; // 477  @subvector_with_refl @eq_a_reflexive 478 ] 495 [1: 496 #n #v #addr #Q @subaddressing_mode_elim0 * #el #H #NH @⊥ >H in NH; // 497 2: 498 @subvector_with_refl @eq_a_reflexive 499 ] 479 500 qed. 480 501
Note: See TracChangeset
for help on using the changeset viewer.