Changeset 465 for Deliverables/D4.1/Matita/BitVector.ma
 Timestamp:
 Jan 20, 2011, 6:10:07 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/BitVector.ma
r462 r465 2 2 (* BitVector.ma: Fixed length bitvectors, and common operations on them. *) 3 3 (* 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 *) 5 5 (* BitVector variants. *) 6 6 (* ===================================== *) 7 7 8 include "arithmetics/nat.ma". 9 10 include "Util.ma". 8 11 include "Vector.ma". 9 12 include "String.ma". … … 13 16 (* ===================================== *) 14 17 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))))))))))).18 ndefinition BitVector ≝ λn: nat. Vector bool n. 19 ndefinition Bit ≝ bool. 20 ndefinition Nibble ≝ BitVector (S (S (S (S O)))). 21 ndefinition Byte7 ≝ BitVector (S (S (S (S (S (S (S O))))))). 22 ndefinition Byte ≝ BitVector (S (S (S (S (S (S (S (S O)))))))). 23 ndefinition Word ≝ BitVector (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))). 24 ndefinition Word11 ≝ BitVector (S (S (S (S (S (S (S (S (S (S (S O))))))))))). 22 25 23 26 (* ===================================== *) … … 27 30 (* 28 31 ndefinition get_index_bv ≝ 29 λn: Nat.30 λb: BitVector n. 31 λm: Nat.32 λn: nat. 33 λb: BitVector n. 34 λm: nat. 32 35 λp: m < n. 33 get_index_bv Bool n b m p.36 get_index_bv bool n b m p. 34 37 35 38 interpretation "BitVector get_index" 'get_index b n = (get_index ? b n). 36 39 37 40 ndefinition set_index_bv ≝ 38 λn: Nat.39 λb: BitVector n. 40 λm: Nat.41 λn: nat. 42 λb: BitVector n. 43 λm: nat. 41 44 λ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. 44 47 45 48 ndefinition 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. 50 53 *) 51 54 … … 54 57 (* ===================================== *) 55 58 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.59 ndefinition zero: ∀n:nat. BitVector n ≝ 60 λn: nat. replicate bool n false. 61 62 ndefinition max: ∀n:nat. BitVector n ≝ 63 λn: nat. replicate bool n true. 61 64 62 65 (* 63 66 ndefinition append ≝ 64 λm, n: Nat.67 λm, n: nat. 65 68 λb: BitVector m. 66 69 λc: BitVector n. 67 append Bool m n b c.70 append bool m n b c. 68 71 *) 69 72 70 73 ndefinition pad ≝ 71 λm, n: Nat.72 λb: BitVector n. 73 let padding ≝ replicate Bool m false in74 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. 75 78 76 79 (* ===================================== *) … … 80 83 (* 81 84 ndefinition 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. 85 88 86 89 ndefinition 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. 90 93 *) 91 94 … … 94 97 (* ===================================== *) 95 98 96 ndefinition conjunction_bv ≝97 λn: Nat.98 λb: BitVector n. 99 λc: BitVector n. 100 zip_with Bool Bool Bool n conjunctionb c.101 102 interpretation "BitVector conjunction" 'conjunction b c = (conjunction ? b c).99 ndefinition 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 105 interpretation "BitVector conjunction" 'conjunction b c = (conjunction_bv ? b c). 103 106 104 107 ndefinition inclusive_disjunction_bv ≝ 105 λn: Nat.106 λb: BitVector n. 107 λc: BitVector n. 108 zip_with Bool Bool Bool n inclusive_disjunctionb c.108 λn: nat. 109 λb: BitVector n. 110 λc: BitVector n. 111 zip_with ? ? ? n (orb) b c. 109 112 110 113 interpretation "BitVector inclusive disjunction" 111 'inclusive_disjunction b c = (inclusive_disjunction ? b c).114 'inclusive_disjunction b c = (inclusive_disjunction_bv ? b c). 112 115 113 116 ndefinition exclusive_disjunction_bv ≝ 114 λn: Nat.115 λb: BitVector n. 116 λc: BitVector n. 117 zip_with Bool Bool Bool n exclusive_disjunctionb c.117 λn: nat. 118 λb: BitVector n. 119 λc: BitVector n. 120 zip_with ? ? ? n (exclusive_disjunction) b c. 118 121 119 122 interpretation "BitVector exclusive disjunction" … … 121 124 122 125 ndefinition 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 130 interpretation "BitVector negation" 'negation b c = (negation_bv ? b c). 128 131 129 132 (* ===================================== *) … … 133 136 (* 134 137 ndefinition 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. 138 141 139 142 ndefinition 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. 143 146 144 147 ndefinition 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. 149 152 150 153 ndefinition 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. 155 158 *) 156 159 … … 161 164 (* 162 165 ndefinition 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. 166 169 167 170 ndefinition 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 175 nlet rec bitvector_of_nat_aux (n: nat) (bound: nat) on bound ≝ 173 176 match bound with 174 [ Z ⇒ Empty Bool(* IT WILL NOT HAPPEN *)175  S bound ⇒176 let divrem ≝ divide_with_remainder n (S (S Z)) in177 let div ≝ f irst Nat Nat divrem in178 let rem ≝ s econd Nat Nat divrem in177 [ 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 179 182 match div with 180 [ Z⇒183 [ O ⇒ 181 184 match rem with 182 [ Z ⇒ Empty Bool183  S r ⇒ true :: (bitvector_of_nat_aux Z bound)185 [ O ⇒ [ ] 186  S r ⇒ true :: (bitvector_of_nat_aux O bound') 184 187 ] 185 188  S d ⇒ 186 189 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') 189 192 ] 190 193 ]]. 191 194 192 195 ndefinition eq_bv ≝ 193 λn: Nat.196 λn: nat. 194 197 λ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 198 200 true 199 201 else 200 202 false) b c. 201 203 202 nlet rec bitvector_of_nat (n: Nat) (m: Nat): BitVector n ≝203 let biglist ≝ rev erse? (bitvector_of_nat_aux m m) in204 nlet rec bitvector_of_nat (n: nat) (m: nat): BitVector n ≝ 205 let biglist ≝ rev ? (bitvector_of_nat_aux m m) in 204 206 let size ≝ length ? biglist in 205 207 let bitvector ≝ vector_of_list ? biglist in … … 208 210 (λH:size ≤ n. ((pad difference size bitvector)⌈BitVector (difference+size) ↦ BitVector n⌉)) 209 211 (λH:¬(size ≤ n). max n). 210 nnormalize; nrewrite > (plus_minus_inverse_right n ?); //; nassumption.212 nrewrite < plus_minus_m_m; //; nassumption; 211 213 nqed. 212 214 213 nlet rec nat_of_bitvector (n: Nat) (b: BitVector n) on b≝215 nlet rec nat_of_bitvector (n: nat) (b: BitVector n) on b: nat ≝ 214 216 match b with 215 [ VEmpty ⇒ Z217 [ VEmpty ⇒ O 216 218  VCons o hd tl ⇒ 217 let hdval ≝ match hd with [ true ⇒ S Z  false ⇒ Z] in218 ((exponential (S (S Z)) o) * hdval) + nat_of_bitvector o tl219 let hdval ≝ match hd with [ true ⇒ S O  false ⇒ O ] in 220 plus ((2^o) * hdval) (nat_of_bitvector o tl) 219 221 ]. 220 222 221 223 naxiom bitvector_of_string: 222 ∀n: Nat.224 ∀n: nat. 223 225 ∀s: String. 224 226 BitVector n. 225 227 226 228 naxiom string_of_bitvector: 227 ∀n: Nat.229 ∀n: nat. 228 230 ∀b: BitVector n. 229 231 String.
Note: See TracChangeset
for help on using the changeset viewer.