Changeset 260


Ignore:
Timestamp:
Nov 23, 2010, 2:30:10 PM (9 years ago)
Author:
sacerdot
Message:
  • Minimal changes to make it compile with the standard distribution of Matita once this directory is substituted to nlibrary
  • ambiguity reduced by lower-casing booleans
Location:
Deliverables/D4.1/Matita
Files:
5 added
11 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Matita/ASM.ma

    r256 r260  
    11include "Universes.ma".
    2 include "Equality.ma".
     2include "Plogic/equality.ma".
    33include "Either.ma".
    44include "BitVector.ma".
     
    3636nlet rec is_a (d:all_types) (A:addressing_mode) on d ≝
    3737  match d with
    38    [ reg ⇒ match A with [ REGISTER _ _ _ ⇒ True | _ ⇒ False ]
    39    | data ⇒ match A with [ DATA _ ⇒ True | _ ⇒ False ]
    40    | rel ⇒ match A with [ RELATIVE _ ⇒ True | _ ⇒ False ]
    41    | acc ⇒ match A with [ ACCUMULATORA ⇒ True | _ ⇒ False ]
    42    | direct ⇒ match A with [ DIRECT _ ⇒ True | _ ⇒ False ]
    43    | indirect ⇒ match A with [ INDIRECT _ ⇒ True | _ ⇒ False ]].
     38   [ reg ⇒ match A with [ REGISTER _ _ _ ⇒ true | _ ⇒ false ]
     39   | data ⇒ match A with [ DATA _ ⇒ true | _ ⇒ false ]
     40   | rel ⇒ match A with [ RELATIVE _ ⇒ true | _ ⇒ false ]
     41   | acc ⇒ match A with [ ACCUMULATORA ⇒ true | _ ⇒ false ]
     42   | direct ⇒ match A with [ DIRECT _ ⇒ true | _ ⇒ false ]
     43   | indirect ⇒ match A with [ INDIRECT _ ⇒ true | _ ⇒ false ]].
    4444
    4545interpretation "Bool" 'or a b = (inclusive_disjunction a b).
     
    5959 { subaddressing_modeel:> addressing_mode;
    6060   subaddressing_modein:
    61     match is_in ? l subaddressing_modeel with [ True ⇒ (? : Prop) | False ⇒ (? : Prop) ]
     61    match is_in ? l subaddressing_modeel with [ true ⇒ (? : Prop) | false ⇒ (? : Prop) ]
    6262 }.
    6363##[ napply True | napply False ]
     
    8787
    8888ndefinition xxx: Jump Nat.
    89  napply (DJNZ ? (mk_subaddressing_mode ?? (REGISTER [True] [True] [True]) ?) (Z: Nat)).
     89 napply (DJNZ ? (mk_subaddressing_mode ?? (REGISTER [true] [true] [true]) ?) (Z: Nat)).
    9090 napply I;
    9191nqed.
     
    110110interpretation "Sigma" 'sigma T = (Sigma ? T).
    111111
    112 ndefinition true: Bool ≝ True.
    113 ndefinition false: Bool ≝ False.
    114112naxiom daemon: False.
    115113
  • Deliverables/D4.1/Matita/Arithmetic.ma

    r257 r260  
    11include "Universes.ma".
    2 include "Equality.ma".
     2include "Plogic/equality.ma".
    33include "Connectives.ma".
    44include "Nat.ma".
     
    3434  λb: Bool.
    3535    match b with
    36       [ False ⇒ Z
    37       | True ⇒ S Z
     36      [ false ⇒ Z
     37      | true ⇒ S Z
    3838      ].
    3939   
  • Deliverables/D4.1/Matita/BitVector.ma

    r257 r260  
    5555ndefinition zero ≝
    5656  λn: Nat.
    57     ((replicate Bool n False): BitVector n).
     57    ((replicate Bool n false): BitVector n).
    5858   
    5959ndefinition max ≝
    6060  λn: Nat.
    61     ((replicate Bool n True): BitVector n).
     61    ((replicate Bool n true): BitVector n).
    6262   
    6363ndefinition append ≝
     
    7272  λm, n: Nat.
    7373  λb: BitVector n.
    74     let padding ≝ replicate Bool m False in
     74    let padding ≝ replicate Bool m false in
    7575      append Bool m n padding b.
    7676     
     
    173173        match rem with
    174174          [ Z ⇒ Empty Bool
    175           | S r ⇒ ? (True :: (bitvector_of_nat_aux Z))
     175          | S r ⇒ ? (true :: (bitvector_of_nat_aux Z))
    176176          ]
    177177      | S d ⇒
    178178        match rem with
    179           [ Z ⇒ ? (False :: (bitvector_of_nat_aux (S d)))
    180           | S r ⇒ ? (True :: (bitvector_of_nat_aux (S d)))
     179          [ Z ⇒ ? (false :: (bitvector_of_nat_aux (S d)))
     180          | S r ⇒ ? (true :: (bitvector_of_nat_aux (S d)))
    181181          ]
    182182      ].
     
    196196    [ Empty ⇒ Z
    197197    | Cons o hd tl ⇒
    198       let hdval ≝ match hd with [ True ⇒ S Z | False ⇒ Z ] in
     198      let hdval ≝ match hd with [ true ⇒ S Z | false ⇒ Z ] in
    199199        ((exponential (S (S Z)) o) * hdval) + nat_of_bitvector o tl
    200200    ].
  • Deliverables/D4.1/Matita/BitVectorTrie.ma

    r248 r260  
    11include "BitVector.ma".
    2 include "Compare.ma".
     2(*include "Compare.ma".*)
    33include "Bool.ma".
    44include "Maybe.ma".
     
    3131        | Node h l r ⇒
    3232           match hd with
    33              [ True ⇒ λK. lookup A h (tl⌈h ↦ o⌉) l a
    34              | False ⇒ λK. lookup A h (tl⌈h ↦ o⌉) r a
     33             [ true ⇒ λK. lookup A h (tl⌈h ↦ o⌉) l a
     34             | false ⇒ λK. lookup A h (tl⌈h ↦ o⌉) r a
    3535             ]
    3636        | Stub s ⇒ λ_. a
     
    4747    | Cons o hd tl ⇒
    4848      match hd with
    49         [ True ⇒  Node A o (Stub A o) (prepare_trie_for_insertion A o tl a)
    50         | False ⇒ Node A o (prepare_trie_for_insertion A o tl a) (Stub A o)
     49        [ true ⇒  Node A o (Stub A o) (prepare_trie_for_insertion A o tl a)
     50        | false ⇒ Node A o (prepare_trie_for_insertion A o tl a) (Stub A o)
    5151        ]
    5252    ].
     
    6262            | Node p l r ⇒ λprf.
    6363               match hd with
    64                 [ True ⇒  Node A o (l⌈o ↦ p⌉) (insert A o tl a (r⌈o ↦ p⌉))
    65                 | False ⇒ Node A o (insert A o tl a (l⌈o ↦ p⌉)) (r⌈o ↦ p⌉)
     64                [ true ⇒  Node A o (l⌈o ↦ p⌉) (insert A o tl a (r⌈o ↦ p⌉))
     65                | false ⇒ Node A o (insert A o tl a (l⌈o ↦ p⌉)) (r⌈o ↦ p⌉)
    6666                ]
    6767            | Stub p ⇒ λprf. ? (prepare_trie_for_insertion A ? b a)
  • Deliverables/D4.1/Matita/Bool.ma

    r246 r260  
    22
    33ninductive Bool: Type[0] ≝
    4   True: Bool
    5 | False: Bool.
     4  true: Bool
     5| false: Bool.
    66
    77nlet rec if_then_else (A: Type[0]) (b: Bool) (t: A) (f: A) on b ≝
    88  match b with
    9     [ True ⇒ t
    10     | False ⇒ f
     9    [ true ⇒ t
     10    | false ⇒ f
    1111    ].
    1212   
     
    2020  λb, c: Bool.
    2121    match b with
    22       [ True ⇒ c
    23       | False ⇒ False
     22      [ true ⇒ c
     23      | false ⇒ false
    2424      ].
    2525   
    2626nlet rec inclusive_disjunction (b: Bool) (c: Bool) on b ≝
    2727  match b with
    28     [ True ⇒ True
    29     | False ⇒ c
     28    [ true ⇒ true
     29    | false ⇒ c
    3030    ].
    3131
    3232nlet rec exclusive_disjunction (b: Bool) (c: Bool) on b ≝
    3333  match b with
    34     [ True ⇒
     34    [ true ⇒
    3535      match c with
    36         [ False ⇒ True
    37         | True ⇒ False
     36        [ false ⇒ true
     37        | true ⇒ false
    3838        ]
    39     | False ⇒
     39    | false ⇒
    4040      match c with
    41         [ False ⇒ False
    42         | True ⇒ True
     41        [ false ⇒ false
     42        | true ⇒ true
    4343        ]
    4444    ].
     
    4646nlet rec negation (b: Bool) on b ≝
    4747  match b with
    48     [ True ⇒ False
    49     | False ⇒ True
     48    [ true ⇒ false
     49    | false ⇒ true
    5050    ]. 
    5151 
  • Deliverables/D4.1/Matita/Connectives.ma

    r258 r260  
    1313(**************************************************************************)
    1414
    15 include "Equality.ma".
     15include "Plogic/equality.ma".
    1616
    1717ninductive True: Prop ≝ 
  • Deliverables/D4.1/Matita/Either.ma

    r247 r260  
    1212  λe: Either A B.
    1313    match e with
    14       [ Left l ⇒ True
    15       | Right r ⇒ False
     14      [ Left l ⇒ true
     15      | Right r ⇒ false
    1616      ].
    1717     
     
    2020  λe: Either A B.
    2121    match e with
    22       [ Left l ⇒ False
    23       | Right r ⇒ True
     22      [ Left l ⇒ false
     23      | Right r ⇒ true
    2424      ].
    2525
  • Deliverables/D4.1/Matita/List.ma

    r256 r260  
    88include "Nat.ma".
    99(* include "Maybe.ma". *)
    10 include "Equality.ma".
     10include "Plogic/equality.ma".
    1111
    1212(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    136136    | Cons hd tl ⇒
    137137      match f hd a with
    138         [ True ⇒ (reverse A b) @ tl
    139         | False ⇒ remove_first_with_aux A f a tl (hd :: b)
     138        [ true ⇒ (reverse A b) @ tl
     139        | false ⇒ remove_first_with_aux A f a tl (hd :: b)
    140140        ]
    141141    ].
     
    154154    | Cons hd tl ⇒
    155155      match f hd a with
    156         [ True ⇒ remove_all_with_aux A f a tl b
    157         | False ⇒ remove_all_with_aux A f a tl (hd :: b)
     156        [ true ⇒ remove_all_with_aux A f a tl b
     157        | false ⇒ remove_all_with_aux A f a tl (hd :: b)
    158158        ]
    159159    ].
     
    171171    | Cons hd tl ⇒
    172172      match f hd with
    173         [ True ⇒ drop_while A f tl
    174         | False ⇒ Cons A hd tl
     173        [ true ⇒ drop_while A f tl
     174        | false ⇒ Cons A hd tl
    175175        ]
    176176    ].
     
    203203    | Cons hd tl ⇒
    204204      match f hd with
    205         [ True ⇒ hd :: (filter A f tl)
    206         | False ⇒ filter A f tl
     205        [ true ⇒ hd :: (filter A f tl)
     206        | false ⇒ filter A f tl
    207207        ]
    208208    ].
     
    210210nlet rec member_with (A: Type[0]) (a: A) (f: A → A → Bool) (l: List A) on l: Bool ≝
    211211  match l with
    212     [ Empty ⇒ cic:/matita/Cerco/Bool/Bool.con(0,2,0)
     212    [ Empty ⇒ false
    213213    | Cons hd tl ⇒ inclusive_disjunction (f hd a) (member_with A a f tl)
    214214    ].
     
    219219    | Cons hd tl ⇒
    220220      match member_with A hd f tl with
    221         [ True ⇒ nub_with A f tl
    222         | False ⇒ hd :: (nub_with A f tl)
     221        [ true ⇒ nub_with A f tl
     222        | false ⇒ hd :: (nub_with A f tl)
    223223        ]
    224224    ].
     
    257257    | Cons hd tl ⇒
    258258      match member_with A hd f m with
    259         [ True ⇒ hd :: (intersection_with A f tl m)
    260         | False ⇒ intersection_with A f tl m
     259        [ true ⇒ hd :: (intersection_with A f tl m)
     260        | false ⇒ intersection_with A f tl m
    261261        ]
    262262    ].
  • Deliverables/D4.1/Matita/Maybe.ma

    r247 r260  
    22
    33include "Universes.ma".
    4 include "Equality.ma".
     4include "Plogic/equality.ma".
    55
    66ninductive Maybe (A: Type[0]): Type[0] ≝
     
    1212  λm: Maybe A.
    1313    match m with
    14       [ Nothing ⇒ False
    15       | Just j ⇒ True
     14      [ Nothing ⇒ false
     15      | Just j ⇒ true
    1616      ].
    1717     
     
    2020  λm: Maybe A.
    2121    match m with
    22       [ Nothing ⇒ True
    23       | Just j ⇒ False
     22      [ Nothing ⇒ true
     23      | Just j ⇒ false
    2424      ].
    2525     
     
    2929  λa: A.
    3030    match b with
    31       [ True ⇒ Just A a
    32       | False ⇒ Nothing A
     31      [ true ⇒ Just A a
     32      | false ⇒ Nothing A
    3333      ].
    3434     
  • Deliverables/D4.1/Matita/Nat.ma

    r247 r260  
    2424nlet rec less_than_or_equal_b (m: Nat) (n: Nat) on m: Bool ≝
    2525  match m with
    26     [ Z ⇒ True
     26    [ Z ⇒ true
    2727    | S o ⇒
    2828      match n with
    29         [ Z ⇒ False
     29        [ Z ⇒ false
    3030        | S p ⇒ less_than_or_equal_b o p
    3131        ]
     
    125125nlet rec division_aux (m: Nat) (n : Nat) (p: Nat) ≝
    126126  match n ≤ p with
    127     [ True ⇒ Z
    128     | False ⇒
     127    [ true ⇒ Z
     128    | false ⇒
    129129      match m with
    130130        [ Z ⇒ Z
     
    148148nlet rec modulus_aux (m: Nat) (n: Nat) (p: Nat) ≝
    149149  match n ≤ p with
    150     [ True ⇒ n
    151     | False ⇒
     150    [ true ⇒ n
     151    | false ⇒
    152152      match m with
    153153        [ Z ⇒ n
  • Deliverables/D4.1/Matita/Vector.ma

    r259 r260  
    1212include "Cartesian.ma".
    1313include "Maybe.ma".
    14 include "Equality.ma".
     14include "Plogic/equality.ma".
    1515
    1616(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    244244                        (v: Vector A n) on v ≝
    245245  match v return λn.λv. List A with
    246     [ Empty ⇒ ? (cic:/matita/Cerco/List/List.con(0,1,1) A)
     246    [ Empty ⇒ ? (cic:/matita/ng/List/List.con(0,1,1) A)
    247247    | Cons o hd tl ⇒ hd :: (list_of_vector A o tl)
    248248    ].
     
    252252nlet rec vector_of_list (A: Type[0]) (l: List A) on l ≝
    253253  match l return λl. Vector A (length A l) with
    254     [ Empty ⇒ ? (cic:/matita/Cerco/Vector/Vector.con(0,1,1) A)
     254    [ Empty ⇒ ? (cic:/matita/ng/Vector/Vector.con(0,1,1) A)
    255255    | Cons hd tl ⇒ ? (hd :: (vector_of_list A tl))
    256256    ].
Note: See TracChangeset for help on using the changeset viewer.