Changeset 274 for Deliverables/D4.1/Matita/Arithmetic.ma
 Timestamp:
 Nov 24, 2010, 3:28:04 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Arithmetic.ma
r273 r274 62 62 nqed. 63 63 64 naxiom less_than_b: Nat → Nat → Bool. 64 naxiom less_than_or_equal_b: Nat → Nat → Bool. 65 naxiom ior: Bool → Bool → Bool. 66 naxiom neg: Bool → Bool. 67 naxiom con: Bool → Bool → Bool. 68 naxiom eq: Nat → Nat → Bool. 65 69 66 ndefinition sub_8_with_carry ≝70 ndefinition sub_8_with_carry: ∀b,c: BitVector eight. ∀carry: Bool. Cartesian (BitVector eight) (List Bool) ≝ 67 71 λb: BitVector eight. 68 72 λc: BitVector eight. … … 71 75 let c_as_nat ≝ nat_of_bitvector eight c in 72 76 let carry_as_nat ≝ nat_of_bool carry in 77 let temporary ≝ minus (modulus b_as_nat sixteen) (modulus c_as_nat sixteen) in 78 let ac_flag ≝ ior 79 (neg (con (less_than_or_equal_b (modulus b_as_nat sixteen) (modulus c_as_nat sixteen)) (less_than_or_equal_b temporary carry_as_nat))) 80 (con (con (eq b_as_nat Z) (eq c_as_nat Z)) (eq carry_as_nat Z)) in 81 let bit_six ≝ ior 82 (neg (con (less_than_or_equal_b (modulus b_as_nat one_hundred_and_twenty_eight) (modulus c_as_nat one_hundred_and_twenty_eight)) (less_than_or_equal_b temporary carry_as_nat))) 83 (con (con (eq b_as_nat Z) (eq c_as_nat Z)) (eq carry_as_nat Z)) in 84 let old_result_1 ≝ b_as_nat  c_as_nat in 85 let old_result_2 ≝ old_result_1  carry_as_nat in 86 let ov_flag ≝ exclusive_disjunction carry bit_six in 87 match less_than_or_equal_b b_as_nat c_as_nat with 88 [ true ⇒ 89 match less_than_or_equal_b old_result_1 carry_as_nat with 90 [ true ⇒ 91 let cy_flag ≝ false in 92 mk_Cartesian … (bitvector_of_nat eight old_result_2) (cy_flag :: ac_flag :: ov_flag :: (Empty Bool)) 93  false ⇒ 94 let cy_flag ≝ true in 95 let new_result ≝ b_as_nat + two_hundred_and_fifty_six  c_as_nat  carry_as_nat in 96 mk_Cartesian … (bitvector_of_nat eight new_result) (cy_flag :: ac_flag :: ov_flag :: (Empty Bool)) 97 ] 98  false ⇒ 99 let cy_flag ≝ true in 100 let new_result ≝ b_as_nat + two_hundred_and_fifty_six  c_as_nat  carry_as_nat in 101 mk_Cartesian … (bitvector_of_nat eight new_result) (cy_flag :: ac_flag :: ov_flag :: (Empty Bool)) 102 ]. 73 103 74 104 ndefinition add_8_with_carry ≝ add_n_with_carry eight.
Note: See TracChangeset
for help on using the changeset viewer.