 Timestamp:
 Aug 31, 2011, 12:30:13 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Util.ma
r1094 r1159 10 10 example daemon: False. generalize in match IMPOSSIBLE; #IMPOSSIBLE destruct(IMPOSSIBLE) qed. 11 11 example not_implemented: False. cases daemon qed. 12 13 notation "⊥" with precedence 90 14 for @{ match ? in False with [ ] }. 12 15 13 16 notation > "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)" … … 614 617 ] 615 618 qed. 619 620 lemma nth_append_first: 621 ∀A:Type[0]. 622 ∀n:nat.∀l1,l2:list A.∀d:A. 623 n < l1 → nth n A (l1@l2) d = nth n A l1 d. 624 #A #n #l1 #l2 #d 625 generalize in match n; n; elim l1 626 [ normalize #k #Hk @⊥ @(absurd … Hk) @not_le_Sn_O 627  #h #t #Hind #k normalize 628 cases k k 629 [ #Hk normalize @refl 630  #k #Hk normalize @(Hind k) @le_S_S_to_le @Hk 631 ] 632 ] 633 qed. 634 635 lemma nth_append_second: 636 ∀A: Type[0].∀n.∀l1,l2:list A.∀d.n ≥ length A l1 > 637 nth n A (l1@l2) d = nth (n  length A l1) A l2 d. 638 #A #n #l1 #l2 #d 639 generalize in match n; n; elim l1 640 [ normalize #k #Hk <(minus_n_O) @refl 641  #h #t #Hind #k normalize 642 cases k k; 643 [ #Hk @⊥ @(absurd (S (t) ≤ 0)) [ @Hk  @not_le_Sn_O ] 644  #k #Hk normalize @(Hind k) @le_S_S_to_le @Hk 645 ] 646 ] 647 qed. 648 616 649 617 650 notation > "'if' term 19 e 'then' term 19 t 'else' term 48 f" non associative with precedence 19 … … 699 732 qed. 700 733 701 702 notation "⊥" with precedence 90703 for @{ match ? in False with [ ] }.704 734 705 735 let rec exclusive_disjunction (b: bool) (c: bool) on b ≝
Note: See TracChangeset
for help on using the changeset viewer.