Changeset 362 for Deliverables/D4.1/Matita/BitVector.ma
 Timestamp:
 Dec 2, 2010, 11:53:49 AM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/BitVector.ma
r357 r362 24 24 (* ===================================== *) 25 25 26 (* 26 27 ndefinition get_index_bv ≝ 27 28 λn: Nat. … … 29 30 λm: Nat. 30 31 λp: m < n. 31 get_index Bool n b m p.32 get_index_bv Bool n b m p. 32 33 33 34 interpretation "BitVector get_index" 'get_index b n = (get_index ? b n). … … 46 47 λm: Nat. 47 48 drop Bool n b m. 49 *) 48 50 49 51 (* ===================================== *) … … 51 53 (* ===================================== *) 52 54 53 ndefinition zero ≝ 54 λn: Nat. 55 ((replicate Bool n false): BitVector n). 56 57 ndefinition max ≝ 58 λn: Nat. 59 ((replicate Bool n true): BitVector n). 60 55 ndefinition zero: ∀n:Nat. BitVector n ≝ 56 λn: Nat. replicate Bool n false. 57 58 ndefinition max: ∀n:Nat. BitVector n ≝ 59 λn: Nat. replicate Bool n true. 60 61 (* 61 62 ndefinition append ≝ 62 63 λm, n: Nat. … … 64 65 λc: BitVector n. 65 66 append Bool m n b c. 66 67 *) 68 67 69 ndefinition pad ≝ 68 70 λm, n: Nat. … … 75 77 (* ===================================== *) 76 78 79 (* 77 80 ndefinition reverse ≝ 78 81 λn: Nat. … … 84 87 λb: BitVector n. 85 88 length Bool n b. 89 *) 86 90 87 91 (* ===================================== *) … … 126 130 (* ===================================== *) 127 131 132 (* 128 133 ndefinition rotate_left_bv ≝ 129 134 λn, m: Nat. … … 147 152 λc: Bool. 148 153 shift_right Bool n m b c. 149 154 *) 155 150 156 (* ===================================== *) 151 157 (* Conversions to and from lists and natural numbers. *) 152 158 (* ===================================== *) 153 159 160 (* 154 161 ndefinition list_of_bitvector ≝ 155 162 λn: Nat. … … 160 167 λl: List Bool. 161 168 vector_of_list Bool l. 169 *) 162 170 163 171 nlet rec bitvector_of_nat_aux (n: Nat) (bound: Nat) on bound ≝ … … 194 202 let biglist ≝ reverse ? (bitvector_of_nat_aux m m) in 195 203 let size ≝ length ? biglist in 196 let bitvector ≝ bitvector_of_listbiglist in204 let bitvector ≝ vector_of_list ? biglist in 197 205 let difference ≝ n  size in 198 206 less_than_or_equal_b_elim …
Note: See TracChangeset
for help on using the changeset viewer.