Changeset 664 for Deliverables/D4.1/DemoMarch2011/matita/Arithmetic.ma
 Timestamp:
 Mar 10, 2011, 11:48:33 AM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/DemoMarch2011/matita/Arithmetic.ma
r644 r664 31 31 ([[ cy_flag ; ac_flag ; ov_flag ]]). 32 32 33 ndefinition sub_8_with_carry: ∀b,c: BitVector eight. ∀carry: Bool. Cartesian (BitVector eight) (BitVector three) ≝ 34 λb: BitVector eight. 35 λc: BitVector eight. 33 ndefinition sub_n_with_carry: ∀n: Nat. ∀b,c: BitVector n. ∀carry: Bool. Cartesian (BitVector n) (BitVector three) ≝ 34 λn: Nat. 35 λb: BitVector n. 36 λc: BitVector n. 36 37 λcarry: Bool. 37 let b_as_nat ≝ nat_of_bitvector eightb in38 let c_as_nat ≝ nat_of_bitvector eightc in39 let carry_as_nat ≝ nat_of_bool carry in40 let temporary ≝ b_as_nat mod sixteen  c_as_nat mod sixteenin41 let ac_flag ≝ negation (conjunction ((b_as_nat mod sixteen) ≲ (c_as_nat mod sixteen)) (temporary ≲ carry_as_nat)) in42 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)) in43 let old_result_1 ≝ b_as_nat  c_as_nat in44 let old_result_2 ≝ old_result_1  carry_as_nat in45 let ov_flag ≝ exclusive_disjunction carry bit_six in46 match conjunction (b_as_nat ≲ c_as_nat) (old_result_1 ≲ carry_as_nat) with47 [ false ⇒48 let cy_flag ≝ falsein49 〈 bitvector_of_nat eight old_result_2, [[ cy_flag ; ac_flag ; ov_flag ]]〉50  true ⇒51 let cy_flag ≝ true in 52 let new_result ≝ b_as_nat + two_hundred_and_fifty_six  c_as_nat  carry_as_nat in 53 〈 bitvector_of_nat eight new_result, [[ cy_flag ; ac_flag ; ov_flag ]]〉 54 ].38 let b_as_nat ≝ nat_of_bitvector n b in 39 let c_as_nat ≝ nat_of_bitvector n c in 40 let carry_as_nat ≝ nat_of_bool carry in 41 let temporary ≝ (b_as_nat mod (two * n))  (c_as_nat mod (two * n)) in 42 let ac_flag ≝ less_than_b (b_as_nat mod (two * n)) ((c_as_nat mod (two * n)) + carry_as_nat) in 43 let bit_six ≝ less_than_b (b_as_nat mod (two^(n  one))) ((c_as_nat mod (two^(n  one))) + carry_as_nat) in 44 let 〈b',cy_flag〉 ≝ 45 if greater_than_or_equal_b b_as_nat (c_as_nat + carry_as_nat) then 46 〈b_as_nat, false〉 47 else 48 〈b_as_nat + (two^n), true〉 49 in 50 let ov_flag ≝ exclusive_disjunction cy_flag bit_six in 51 〈bitvector_of_nat n ((b'  c_as_nat)  carry_as_nat), [[ cy_flag; ac_flag; ov_flag ]]〉. 52 53 54 ndefinition sub_8_with_carry ≝ sub_n_with_carry eight. 55 ndefinition sub_16_with_carry ≝ sub_n_with_carry sixteen. 55 56 56 57 ndefinition add_8_with_carry ≝ add_n_with_carry eight.
Note: See TracChangeset
for help on using the changeset viewer.