Changeset 273 for Deliverables
 Timestamp:
 Nov 24, 2010, 2:28:34 PM (11 years ago)
 Location:
 Deliverables/D4.1/Matita
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Arithmetic.ma
r272 r273 59 59 ? (mk_Cartesian (BitVector n) ? (? (bitvector_of_nat n result)) 60 60 (cy_flag :: ac_flag :: ov_flag :: Empty Bool)). 61 //.61 #H; nassumption; 62 62 nqed. 63 63 … … 71 71 let c_as_nat ≝ nat_of_bitvector eight c in 72 72 let carry_as_nat ≝ nat_of_bool carry in 73 let result_old_1 ≝ minus (minus b_as_nat c_as_nat) carry_as_nat in74 let modulus_1 ≝ (modulus b_as_nat sixteen)  (modulus c_as_nat sixteen) in75 match less_than_b (modulus b_as_nat sixteen) (modulus c_as_nat sixteen) with76 [ true ⇒77 let ac_flag ≝ true in78 let result_old_2 ≝ (minus (modulus b_as_nat one_hundred_and_twenty_eight)79 (modulus c_as_nat one_hundred_and_twenty_eight)) in80 match less_than_b (modulus b_as_nat one_hundred_and_twenty_eight)81 (modulus c_as_nat one_hundred_and_twenty_eight) with82 [ true ⇒83 let bit_six ≝ true in84 let result_carry ≝ mk_Cartesian … result_old_1 false in85 let ov_flag ≝ exclusive_disjunction cy_flag bit_six in86 mk_Cartesian … (first … result_carry) (second … result_carry :: ac_flag :: ov_flag :: Empty Bool)87  false ⇒ ?88 ]89  false ⇒ ?90 ].91 92 73 93 74 ndefinition add_8_with_carry ≝ add_n_with_carry eight. 94 75 ndefinition add_16_with_carry ≝ add_n_with_carry sixteen. 95 76 96 (*97 77 ndefinition increment ≝ 98 78 λn: Nat. … … 101 81 let overflow ≝ b_as_nat ≥ (S (S Z))^n in 102 82 match overflow with 103 [ False ⇒ bitvector_of_nat n b_as_nat104  True ⇒ bitvector_of_nat n Z83 [ false ⇒ bitvector_of_nat n b_as_nat 84  true ⇒ zero n 105 85 ]. 106 86 … … 121 101 λb: Bool. 122 102 ? (pad (n  (S Z)) (S Z) (Cons Bool ? b (Empty Bool))). 123 //. 103 nrewrite > (plus_minus_inverse_right n ?); 104 #H; 105 nassumption; 124 106 nqed. 125 126 *) 
Deliverables/D4.1/Matita/BitVector.ma
r271 r273 185 185 nqed. 186 186 187 ndefinition bitvector_of_nat ≝ 188 λm, n: Nat. 189 let biglist ≝ reverse Bool (bitvector_of_nat_aux m) in 190 let size ≝ length Bool biglist in 191 let bitvector ≝ bitvector_of_list biglist in 192 let difference ≝ n  size in 193 pad difference size bitvector. 187 naxiom plus_minus_inverse_left: 188 ∀m, n: Nat. 189 (m + n)  n = m. 190 191 naxiom plus_minus_inverse_right: 192 ∀m, n: Nat. 193 (m  n) + n = m. 194 195 naxiom greater_than_b: Nat → Nat → Bool. 196 197 nlet rec bitvector_of_nat (n: Nat) (m: Nat): BitVector n ≝ 198 let biglist ≝ reverse ? (bitvector_of_nat_aux m) in 199 let size ≝ length ? biglist in 200 let bitvector ≝ bitvector_of_list biglist in 201 let difference ≝ n  size in 202 match greater_than_b size n with 203 [ true ⇒ max n 204  false ⇒ ? (pad difference size bitvector) 205 ]. 206 nnormalize. 207 nrewrite > (plus_minus_inverse_right n ?). 208 #H. 209 nassumption. 210 nqed. 211 212 ncheck bitvector_of_nat. 194 213 195 214 nlet rec nat_of_bitvector (n: Nat) (b: BitVector n) on b ≝
Note: See TracChangeset
for help on using the changeset viewer.