Changeset 351 for Deliverables/D4.1/Matita/Arithmetic.ma
 Timestamp:
 Dec 1, 2010, 4:30:46 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Arithmetic.ma
r350 r351 78 78 let ac_flag ≝ ((modulus b_as_nat ((S (S Z)) * n)) + 79 79 (modulus c_as_nat ((S (S Z)) * n)) + 80 c_as_nat) ≥((S (S Z)) * n) in80 c_as_nat) ≳ ((S (S Z)) * n) in 81 81 let bit_xxx ≝ (((modulus b_as_nat ((S (S Z))^(n  (S Z)))) + 82 82 (modulus c_as_nat ((S (S Z))^(n  (S Z)))) + 83 c_as_nat) ≥((S (S Z))^(n  (S Z)))) in83 c_as_nat) ≳ ((S (S Z))^(n  (S Z)))) in 84 84 let result ≝ modulus result_old ((S (S Z))^n) in 85 let cy_flag ≝ (result_old ≥((S (S Z))^n)) in85 let cy_flag ≝ (result_old ≳ ((S (S Z))^n)) in 86 86 let ov_flag ≝ exclusive_disjunction cy_flag bit_xxx in 87 87 ? (mk_Cartesian (BitVector n) ? (? (bitvector_of_nat n result)) … … 98 98 let carry_as_nat ≝ nat_of_bool carry in 99 99 let temporary ≝ b_as_nat mod sixteen  c_as_nat mod sixteen in 100 let ac_flag ≝ negation (conjunction ((b_as_nat mod sixteen) ≤ (c_as_nat mod sixteen)) (temporary ≤carry_as_nat)) in101 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)) in100 let ac_flag ≝ negation (conjunction ((b_as_nat mod sixteen) ≲ (c_as_nat mod sixteen)) (temporary ≲ carry_as_nat)) in 101 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 102 102 let old_result_1 ≝ b_as_nat  c_as_nat in 103 103 let old_result_2 ≝ old_result_1  carry_as_nat in 104 104 let ov_flag ≝ exclusive_disjunction carry bit_six in 105 match conjunction (b_as_nat ≤ c_as_nat) (old_result_1 ≤carry_as_nat) with105 match conjunction (b_as_nat ≲ c_as_nat) (old_result_1 ≲ carry_as_nat) with 106 106 [ false ⇒ 107 107 let cy_flag ≝ false in … … 120 120 λb: BitVector n. 121 121 let b_as_nat ≝ (nat_of_bitvector n b) + (S Z) in 122 let overflow ≝ b_as_nat ≥(S (S Z))^n in122 let overflow ≝ b_as_nat ≳ (S (S Z))^n in 123 123 match overflow with 124 124 [ false ⇒ bitvector_of_nat n b_as_nat … … 138 138 139 139 ndefinition bitvector_of_bool: 140 ∀n: Nat. ∀b: Bool. BitVector n≝140 ∀n: Nat. ∀b: Bool. BitVector (S n) ≝ 141 141 λn: Nat. 142 142 λb: Bool. 143 ? (pad (n  (S Z)) (S Z) (Cons Bool ? b (Empty Bool))). 144 nrewrite > (plus_minus_inverse_right n ?); 145 #H; 146 nassumption; 143 ? (pad (S n  (S Z)) (S Z) (Cons Bool ? b (Empty Bool))). 144 nrewrite > plus_minus_inverse_right 145 [ napply (λx.x)  /2/] 147 146 nqed. 148 147
Note: See TracChangeset
for help on using the changeset viewer.