Changeset 359


Ignore:
Timestamp:
Dec 2, 2010, 10:25:32 AM (9 years ago)
Author:
mulligan
Message:

add_n_with_carry and sub_n_with_carry now both return bitvectors of length three for holding the flags instead of lists.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Matita/Arithmetic.ma

    r357 r359  
    1010   
    1111ndefinition add_n_with_carry:
    12       ∀n: Nat. ∀b, c: BitVector n. ∀carry: Bool. Cartesian (BitVector n) (List Bool) ≝
     12      ∀n: Nat. ∀b, c: BitVector n. ∀carry: Bool. Cartesian (BitVector n) (BitVector three) ≝
    1313  λn: Nat.
    1414  λb: BitVector n.
     
    2828    let cy_flag ≝ (result_old ≳ ((S (S Z))^n)) in
    2929    let ov_flag ≝ exclusive_disjunction cy_flag bit_xxx in
    30       ? (mk_Cartesian (BitVector n) ? (? (bitvector_of_nat n result))
    31                           (cy_flag :: ac_flag :: ov_flag :: Empty Bool)).
    32     #H; nassumption;
    33 nqed.
     30      mk_Cartesian ? ? (bitvector_of_nat n result)
     31                       ([[ cy_flag ; ac_flag ; ov_flag ]]).
    3432
    35 ndefinition sub_8_with_carry: ∀b,c: BitVector eight. ∀carry: Bool. Cartesian (BitVector eight) (List Bool) ≝
     33ndefinition sub_8_with_carry: ∀b,c: BitVector eight. ∀carry: Bool. Cartesian (BitVector eight) (BitVector three) ≝
    3634  λb: BitVector eight.
    3735  λc: BitVector eight.
     
    4947        [ false ⇒
    5048           let cy_flag ≝ false in
    51             〈 bitvector_of_nat eight old_result_2, [cy_flag ; ac_flag ; ov_flag ]
     49            〈 bitvector_of_nat eight old_result_2, [[ cy_flag ; ac_flag ; ov_flag ]]
    5250        | true ⇒
    5351           let cy_flag ≝ true in
    5452           let new_result ≝ b_as_nat + two_hundred_and_fifty_six - c_as_nat - carry_as_nat in
    55             〈 bitvector_of_nat eight new_result, [ cy_flag ; ac_flag ; ov_flag ]
     53            〈 bitvector_of_nat eight new_result, [[ cy_flag ; ac_flag ; ov_flag ]]
    5654        ].
    5755         
Note: See TracChangeset for help on using the changeset viewer.