Changeset 277 for Deliverables/D4.1/Matita/Arithmetic.ma
 Timestamp:
 Nov 24, 2010, 5:06:16 PM (11 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Arithmetic.ma
r275 r277 69 69 let c_as_nat ≝ nat_of_bitvector eight c in 70 70 let carry_as_nat ≝ nat_of_bool carry in 71 let temporary ≝ minus (modulus b_as_nat sixteen) (modulus c_as_nat sixteen) in 72 let ac_flag ≝ inclusive_disjunction 73 (negation (conjunction (less_than_or_equal_b (modulus b_as_nat sixteen) (modulus c_as_nat sixteen)) (less_than_or_equal_b temporary carry_as_nat))) 74 (conjunction (conjunction (decidable_equality b_as_nat Z) (decidable_equality c_as_nat Z)) (decidable_equality carry_as_nat Z)) in 75 let bit_six ≝ inclusive_disjunction 76 (negation (conjunction (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))) 77 (conjunction (conjunction (decidable_equality b_as_nat Z) (decidable_equality c_as_nat Z)) (decidable_equality carry_as_nat Z)) in 71 let temporary ≝ b_as_nat mod sixteen  c_as_nat mod sixteen in 72 let ac_flag ≝ negation (conjunction ((b_as_nat mod sixteen) ≤ (c_as_nat mod sixteen)) (temporary ≤ carry_as_nat)) in 73 let bit_six ≝ negation (conjunction ((b_as_nat mod one_hundred_and_twenty_eight) ≤ (c_as_nat mod one_hundred_and_twenty_eight)) (temporary ≤ carry_as_nat)) in 78 74 let old_result_1 ≝ b_as_nat  c_as_nat in 79 75 let old_result_2 ≝ old_result_1  carry_as_nat in 80 76 let ov_flag ≝ exclusive_disjunction carry bit_six in 81 match less_than_or_equal_b b_as_nat c_as_nat with 82 [ true ⇒ 83 match less_than_or_equal_b old_result_1 carry_as_nat with 84 [ true ⇒ 85 let cy_flag ≝ false in 86 mk_Cartesian … (bitvector_of_nat eight old_result_2) (cy_flag :: ac_flag :: ov_flag :: (Empty Bool)) 87  false ⇒ 88 let cy_flag ≝ true in 89 let new_result ≝ b_as_nat + two_hundred_and_fifty_six  c_as_nat  carry_as_nat in 90 mk_Cartesian … (bitvector_of_nat eight new_result) (cy_flag :: ac_flag :: ov_flag :: (Empty Bool)) 91 ] 92  false ⇒ 93 let cy_flag ≝ true in 94 let new_result ≝ b_as_nat + two_hundred_and_fifty_six  c_as_nat  carry_as_nat in 95 mk_Cartesian … (bitvector_of_nat eight new_result) (cy_flag :: ac_flag :: ov_flag :: (Empty Bool)) 77 match conjunction (b_as_nat ≤ c_as_nat) (old_result_1 ≤ carry_as_nat) with 78 [ false ⇒ 79 let cy_flag ≝ false in 80 〈 bitvector_of_nat eight old_result_2, [cy_flag ; ac_flag ; ov_flag ] 〉 81  true ⇒ 82 let cy_flag ≝ true in 83 let new_result ≝ b_as_nat + two_hundred_and_fifty_six  c_as_nat  carry_as_nat in 84 〈 bitvector_of_nat eight new_result, [ cy_flag ; ac_flag ; ov_flag ] 〉 96 85 ]. 97 86 98 87 ndefinition add_8_with_carry ≝ add_n_with_carry eight. 99 88 ndefinition add_16_with_carry ≝ add_n_with_carry sixteen.
Note: See TracChangeset
for help on using the changeset viewer.