Changeset 2108 for src/ASM/Assembly.ma
 Timestamp:
 Jun 25, 2012, 2:39:06 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Assembly.ma
r2101 r2108 604 604 qed. 605 605 606 axiom eq_identifier_eq: 606 axiom eqb_succ_injective_Pos: 607 ∀l, r: Pos. 608 eqb (succ l) (succ r) = true → eqb l r = true. 609 610 lemma eqb_true_to_refl_Pos: 611 ∀l, r: Pos. 612 eqb l r = true → l = r. 613 #l #r @(pos_elim2 … l r) 614 [1: 615 #r cases r 616 [1: 617 #_ % 618 2,3: 619 #l normalize in ⊢ (% → ?); #absurd destruct(absurd) 620 ] 621 2: 622 #l cases l 623 [1: 624 normalize in ⊢ (% → ?); #absurd destruct(absurd) 625 2,3: 626 #l' normalize in ⊢ (% → ?); #absurd destruct(absurd) 627 ] 628 3: 629 #l #r #inductive_hypothesis #relevant @eq_f 630 @inductive_hypothesis @eqb_succ_injective_Pos 631 assumption 632 ] 633 qed. 634 635 lemma eq_identifier_eq: 607 636 ∀tag: String. 608 637 ∀l. 609 638 ∀r. 610 639 eq_identifier tag l r = true → l = r. 640 #tag #l #r cases l cases r 641 #pos_l #pos_r 642 cases pos_l cases pos_r 643 [1: 644 #_ % 645 2,3,4,7: 646 #p1_l normalize in ⊢ (% → ?); 647 #absurd destruct(absurd) 648 5,9: 649 #p1_l #p1_r normalize in ⊢ (% → ?); 650 #relevant 651 >(eqb_true_to_refl_Pos … relevant) % 652 *: 653 #p_l #p_r normalize in ⊢ (% → ?); 654 #absurd destruct(absurd) 655 ] 656 qed. 611 657 612 658 axiom neq_identifier_neq: … … 614 660 ∀l, r: identifier tag. 615 661 eq_identifier tag l r = false → (l = r → False). 616 662 617 663 (* label_map: identifier ↦ pseudo program counter *) 618 664 definition label_map ≝ identifier_map ASMTag ℕ.
Note: See TracChangeset
for help on using the changeset viewer.