Ignore:
Timestamp:
Jan 20, 2011, 6:10:07 PM (9 years ago)
Author:
mulligan
Message:

Moved over to standard library.

File:
1 edited

Legend:

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

    r462 r465  
    22(* BitVector.ma: Fixed length bitvectors, and common operations on them.      *)
    33(*               Most functions are specialised versions of those found in    *)
    4 (*               Vector.ma as a courtesy, or Boolean functions lifted into    *)
     4(*               Vector.ma as a courtesy, or boolean functions lifted into    *)
    55(*               BitVector variants.                                          *)
    66(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    77
     8include "arithmetics/nat.ma".
     9
     10include "Util.ma".
    811include "Vector.ma".
    912include "String.ma".
     
    1316(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    1417
    15 ndefinition BitVector ≝ λn: Nat. Vector Bool n.
    16 ndefinition Bit ≝ Bool.
    17 ndefinition Nibble ≝ BitVector (S (S (S (S Z)))).
    18 ndefinition Byte7 ≝ BitVector (S (S (S (S (S (S (S Z))))))).
    19 ndefinition Byte ≝ BitVector (S (S (S (S (S (S (S (S Z)))))))).
    20 ndefinition Word ≝ BitVector (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))).
    21 ndefinition Word11 ≝ BitVector (S (S (S (S (S (S (S (S (S (S (S Z))))))))))).
     18ndefinition BitVector ≝ λn: nat. Vector bool n.
     19ndefinition Bit ≝ bool.
     20ndefinition Nibble ≝ BitVector (S (S (S (S O)))).
     21ndefinition Byte7 ≝ BitVector (S (S (S (S (S (S (S O))))))).
     22ndefinition Byte ≝ BitVector (S (S (S (S (S (S (S (S O)))))))).
     23ndefinition Word ≝ BitVector (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))).
     24ndefinition Word11 ≝ BitVector (S (S (S (S (S (S (S (S (S (S (S O))))))))))).
    2225
    2326(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    2730(*
    2831ndefinition get_index_bv ≝
    29   λn: Nat.
    30   λb: BitVector n.
    31   λm: Nat.
     32  λn: nat.
     33  λb: BitVector n.
     34  λm: nat.
    3235  λp: m < n.
    33     get_index_bv Bool n b m p.
     36    get_index_bv bool n b m p.
    3437   
    3538interpretation "BitVector get_index" 'get_index b n = (get_index ? b n).
    3639   
    3740ndefinition set_index_bv ≝
    38   λn: Nat.
    39   λb: BitVector n.
    40   λm: Nat.
     41  λn: nat.
     42  λb: BitVector n.
     43  λm: nat.
    4144  λp: m < n.
    42   λc: Bool.
    43     set_index Bool n b m c.
     45  λc: bool.
     46    set_index bool n b m c.
    4447   
    4548ndefinition drop ≝
    46   λn: Nat.
    47   λb: BitVector n.
    48   λm: Nat.
    49     drop Bool n b m.
     49  λn: nat.
     50  λb: BitVector n.
     51  λm: nat.
     52    drop bool n b m.
    5053*)
    5154
     
    5457(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    5558
    56 ndefinition zero: ∀n:Nat. BitVector n ≝
    57   λn: Nat. replicate Bool n false.
    58    
    59 ndefinition max: ∀n:Nat. BitVector n ≝
    60   λn: Nat. replicate Bool n true.
     59ndefinition zero: ∀n:nat. BitVector n ≝
     60  λn: nat. replicate bool n false.
     61   
     62ndefinition max: ∀n:nat. BitVector n ≝
     63  λn: nat. replicate bool n true.
    6164
    6265(*
    6366ndefinition append ≝
    64   λm, n: Nat.
     67  λm, n: nat.
    6568  λb: BitVector m.
    6669  λc: BitVector n.
    67     append Bool m n b c.
     70    append bool m n b c.
    6871*)
    6972 
    7073ndefinition pad ≝
    71   λm, n: Nat.
    72   λb: BitVector n.
    73     let padding ≝ replicate Bool m false in
    74       append Bool m n padding b.
     74  λm, n: nat.
     75  λb: BitVector n.
     76    let padding ≝ replicate bool m false in
     77      append bool m n padding b.
    7578     
    7679(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    8083(*
    8184ndefinition reverse ≝
    82   λn: Nat.
    83   λb: BitVector n.
    84     reverse Bool n b.
     85  λn: nat.
     86  λb: BitVector n.
     87    reverse bool n b.
    8588
    8689ndefinition length ≝
    87   λn: Nat.
    88   λb: BitVector n.
    89     length Bool n b.
     90  λn: nat.
     91  λb: BitVector n.
     92    length bool n b.
    9093*)
    9194
     
    9497(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    9598   
    96 ndefinition conjunction_bv
    97   λn: Nat.
    98   λb: BitVector n.
    99   λc: BitVector n.
    100     zip_with Bool Bool Bool n conjunction b c.
    101    
    102 interpretation "BitVector conjunction" 'conjunction b c = (conjunction ? b c).
     99ndefinition conjunction_bv: ∀n. ∀b, c: BitVector n. BitVector n
     100  λn: nat.
     101  λb: BitVector n.
     102  λc: BitVector n.
     103    zip_with ? ? ? n (andb) b c.
     104   
     105interpretation "BitVector conjunction" 'conjunction b c = (conjunction_bv ? b c).
    103106   
    104107ndefinition inclusive_disjunction_bv ≝
    105   λn: Nat.
    106   λb: BitVector n.
    107   λc: BitVector n.
    108     zip_with Bool Bool Bool n inclusive_disjunction b c.
     108  λn: nat.
     109  λb: BitVector n.
     110  λc: BitVector n.
     111    zip_with ? ? ? n (orb) b c.
    109112   
    110113interpretation "BitVector inclusive disjunction"
    111   'inclusive_disjunction b c = (inclusive_disjunction ? b c).
     114  'inclusive_disjunction b c = (inclusive_disjunction_bv ? b c).
    112115         
    113116ndefinition exclusive_disjunction_bv ≝
    114   λn: Nat.
    115   λb: BitVector n.
    116   λc: BitVector n.
    117     zip_with Bool Bool Bool n exclusive_disjunction b c.
     117  λn: nat.
     118  λb: BitVector n.
     119  λc: BitVector n.
     120    zip_with ? ? ? n (exclusive_disjunction) b c.
    118121   
    119122interpretation "BitVector exclusive disjunction"
     
    121124   
    122125ndefinition negation_bv ≝
    123   λn: Nat.
    124   λb: BitVector n.
    125     map Bool Bool n (negation) b.
    126    
    127 interpretation "BitVector negation" 'negation b c = (negation ? b c).
     126  λn: nat.
     127  λb: BitVector n.
     128    map bool bool n (notb) b.
     129   
     130interpretation "BitVector negation" 'negation b c = (negation_bv ? b c).
    128131
    129132(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    133136(*
    134137ndefinition rotate_left_bv ≝
    135   λn, m: Nat.
    136   λb: BitVector n.
    137     rotate_left Bool n m b.
     138  λn, m: nat.
     139  λb: BitVector n.
     140    rotate_left bool n m b.
    138141
    139142ndefinition rotate_right_bv ≝
    140   λn, m: Nat.
    141   λb: BitVector n.
    142     rotate_right Bool n m b.
     143  λn, m: nat.
     144  λb: BitVector n.
     145    rotate_right bool n m b.
    143146   
    144147ndefinition shift_left_bv ≝
    145   λn, m: Nat.
    146   λb: BitVector n.
    147   λc: Bool.
    148     shift_left Bool n m b c.
     148  λn, m: nat.
     149  λb: BitVector n.
     150  λc: bool.
     151    shift_left bool n m b c.
    149152   
    150153ndefinition shift_right_bv ≝
    151   λn, m: Nat.
    152   λb: BitVector n.
    153   λc: Bool.
    154     shift_right Bool n m b c.
     154  λn, m: nat.
     155  λb: BitVector n.
     156  λc: bool.
     157    shift_right bool n m b c.
    155158*)
    156159 
     
    161164(*
    162165ndefinition list_of_bitvector ≝
    163   λn: Nat.
    164   λb: BitVector n.
    165     list_of_vector Bool n b.
     166  λn: nat.
     167  λb: BitVector n.
     168    list_of_vector bool n b.
    166169   
    167170ndefinition bitvector_of_list ≝
    168   λl: List Bool.
    169     vector_of_list Bool l.
    170 *)
    171 
    172 nlet rec bitvector_of_nat_aux (n: Nat) (bound: Nat) on bound ≝
     171  λl: List bool.
     172    vector_of_list bool l.
     173*)
     174
     175nlet rec bitvector_of_nat_aux (n: nat) (bound: nat) on bound ≝
    173176 match bound with
    174   [ Z ⇒ Empty Bool (* IT WILL NOT HAPPEN *)
    175   | S bound
    176     let divrem ≝ divide_with_remainder n (S (S Z)) in
    177     let div ≝ first Nat Nat divrem in
    178     let rem ≝ second Nat Nat divrem in
     177  [ O ⇒ [ ] (* IT WILL NOT HAPPEN *)
     178  | S bound'
     179    let divrem ≝ divide_with_remainder n (S (S O)) in
     180    let div ≝ fst nat nat divrem in
     181    let rem ≝ snd nat nat divrem in
    179182      match div with
    180         [ Z
     183        [ O
    181184          match rem with
    182             [ Z ⇒ Empty Bool
    183             | S r ⇒ true :: (bitvector_of_nat_aux Z bound)
     185            [ O ⇒ [ ]
     186            | S r ⇒ true :: (bitvector_of_nat_aux O bound')
    184187            ]
    185188        | S d ⇒
    186189          match rem with
    187             [ Z ⇒ false :: (bitvector_of_nat_aux (S d) bound)
    188             | S r ⇒ true :: (bitvector_of_nat_aux (S d) bound)
     190            [ O ⇒ false :: (bitvector_of_nat_aux (S d) bound')
     191            | S r ⇒ true :: (bitvector_of_nat_aux (S d) bound')
    189192            ]
    190193        ]].
    191194
    192195ndefinition eq_bv ≝
    193   λn: Nat.
     196  λn: nat.
    194197  λb, c: BitVector n.
    195     eq_v Bool n (λd, e.
    196       if inclusive_disjunction (conjunction d e) (conjunction (negation d)
    197                                                               (negation e)) then
     198    eq_v bool n (λd, e.
     199      if (d ∧ e) ∨ ((¬d) ∧ (¬e)) then
    198200        true
    199201      else
    200202        false) b c.
    201203
    202 nlet rec bitvector_of_nat (n: Nat) (m: Nat): BitVector n ≝
    203   let biglist ≝ reverse ? (bitvector_of_nat_aux m m) in
     204nlet rec bitvector_of_nat (n: nat) (m: nat): BitVector n ≝
     205  let biglist ≝ rev ? (bitvector_of_nat_aux m m) in
    204206  let size ≝ length ? biglist in
    205207  let bitvector ≝ vector_of_list ? biglist in
     
    208210    (λH:size ≤ n. ((pad difference size bitvector)⌈BitVector (difference+size) ↦ BitVector n⌉))
    209211    (λH:¬(size ≤ n). max n).
    210  nnormalize; nrewrite > (plus_minus_inverse_right n ?); //; nassumption.
     212    nrewrite < plus_minus_m_m; //; nassumption;
    211213nqed.
    212214
    213 nlet rec nat_of_bitvector (n: Nat) (b: BitVector n) on b
     215nlet rec nat_of_bitvector (n: nat) (b: BitVector n) on b: nat
    214216  match b with
    215     [ VEmpty ⇒ Z
     217    [ VEmpty ⇒ O
    216218    | VCons o hd tl ⇒
    217       let hdval ≝ match hd with [ true ⇒ S Z | false ⇒ Z ] in
    218         ((exponential (S (S Z)) o) * hdval) + nat_of_bitvector o tl
     219      let hdval ≝ match hd with [ true ⇒ S O | false ⇒ O ] in
     220        plus ((2^o) * hdval) (nat_of_bitvector o tl)
    219221    ].
    220222   
    221223naxiom bitvector_of_string:
    222   ∀n: Nat.
     224  ∀n: nat.
    223225  ∀s: String.
    224226    BitVector n.
    225227   
    226228naxiom string_of_bitvector:
    227   ∀n: Nat.
     229  ∀n: nat.
    228230  ∀b: BitVector n.
    229231    String.
Note: See TracChangeset for help on using the changeset viewer.