Ignore:
Timestamp:
Sep 7, 2011, 12:10:27 PM (9 years ago)
Author:
campbell
Message:

Merge trunk to branch.

Location:
Deliverables/D3.3/id-lookup-branch
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.3/id-lookup-branch

  • Deliverables/D3.3/id-lookup-branch/ASM

  • Deliverables/D3.3/id-lookup-branch/ASM/Util.ma

    r1098 r1197  
    1111example not_implemented: False. cases daemon qed.
    1212
     13notation "⊥" with precedence 90
     14  for @{ match ? in False with [ ] }.
     15
    1316notation > "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)"
    1417 with precedence 10
    1518for @{ match $t with [ pair ${ident x} ${ident y} ⇒ $s ] }.
     19
     20(*
     21notation > "hvbox('let' 〈ident x, ident y, ident z〉 ≝ t 'in' s)"
     22 with precedence 10
     23for @{
     24  match $t with
     25  [ pair ${ident x} y' ⇒
     26    match y' with
     27    [ pair ${ident y} ${ident z} ⇒ $s ]
     28  ]
     29}.
     30*)
    1631
    1732definition ltb ≝
     
    3247  [ O ⇒ match m with [ O ⇒ true | _ ⇒ false ]
    3348  | S n' ⇒ match m with [ S m' ⇒ eq_nat n' m' | _ ⇒ false ]
     49  ].
     50
     51let rec forall
     52  (A: Type[0]) (f: A → bool) (l: list A)
     53    on l ≝
     54  match l with
     55  [ nil        ⇒ true
     56  | cons hd tl ⇒ f hd ∧ forall A f tl
    3457  ].
    3558
     
    614637  ]
    615638qed.
     639
     640lemma nth_append_first:
     641 ∀A:Type[0].
     642 ∀n:nat.∀l1,l2:list A.∀d:A.
     643   n < |l1| → nth n A (l1@l2) d = nth n A l1 d.
     644 #A #n #l1 #l2 #d
     645 generalize in match n; -n; elim l1
     646 [ normalize #k #Hk @⊥ @(absurd … Hk) @not_le_Sn_O
     647 | #h #t #Hind #k normalize
     648   cases k -k
     649   [ #Hk normalize @refl
     650   | #k #Hk normalize @(Hind k) @le_S_S_to_le @Hk
     651   ] 
     652 ]
     653qed.
     654
     655lemma nth_append_second:
     656 ∀A: Type[0].∀n.∀l1,l2:list A.∀d.n ≥ length A l1 ->
     657  nth n A (l1@l2) d = nth (n - length A l1) A l2 d.
     658 #A #n #l1 #l2 #d
     659 generalize in match n; -n; elim l1
     660 [ normalize #k #Hk <(minus_n_O) @refl
     661 | #h #t #Hind #k normalize
     662   cases k -k;
     663   [ #Hk @⊥ @(absurd (S (|t|) ≤ 0)) [ @Hk | @not_le_Sn_O ]
     664   | #k #Hk normalize @(Hind k) @le_S_S_to_le @Hk
     665   ]
     666 ]
     667qed.
     668
    616669   
    617670notation > "'if' term 19 e 'then' term 19 t 'else' term 48 f" non associative with precedence 19
     
    699752qed.
    700753
    701 
    702 notation "⊥" with precedence 90
    703   for @{ match ? in False with [ ] }.
    704754
    705755let rec exclusive_disjunction (b: bool) (c: bool) on b ≝
Note: See TracChangeset for help on using the changeset viewer.