Changeset 1159


Ignore:
Timestamp:
Aug 31, 2011, 12:30:13 PM (8 years ago)
Author:
boender
Message:
  • added 'nth' theorems
  • moved up \bot a bit
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Util.ma

    r1094 r1159  
    1010example daemon: False. generalize in match IMPOSSIBLE; #IMPOSSIBLE destruct(IMPOSSIBLE) qed.
    1111example not_implemented: False. cases daemon qed.
     12
     13notation "⊥" with precedence 90
     14  for @{ match ? in False with [ ] }.
    1215
    1316notation > "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)"
     
    614617  ]
    615618qed.
     619
     620lemma 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 ]
     633qed.
     634
     635lemma 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 ]
     647qed.
     648
    616649   
    617650notation > "'if' term 19 e 'then' term 19 t 'else' term 48 f" non associative with precedence 19
     
    699732qed.
    700733
    701 
    702 notation "⊥" with precedence 90
    703   for @{ match ? in False with [ ] }.
    704734
    705735let rec exclusive_disjunction (b: bool) (c: bool) on b ≝
Note: See TracChangeset for help on using the changeset viewer.