Changeset 274


Ignore:
Timestamp:
Nov 24, 2010, 3:28:04 PM (9 years ago)
Author:
mulligan
Message:

First attempt at sub8_with_c complete.

File:
1 edited

Legend:

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

    r273 r274  
    6262nqed.
    6363
    64 naxiom less_than_b: Nat → Nat → Bool.
     64naxiom less_than_or_equal_b: Nat → Nat → Bool.
     65naxiom ior: Bool → Bool → Bool.
     66naxiom neg: Bool → Bool.
     67naxiom con: Bool → Bool → Bool.
     68naxiom eq: Nat → Nat → Bool.
    6569
    66 ndefinition sub_8_with_carry
     70ndefinition sub_8_with_carry: ∀b,c: BitVector eight. ∀carry: Bool. Cartesian (BitVector eight) (List Bool)
    6771  λb: BitVector eight.
    6872  λc: BitVector eight.
     
    7175    let c_as_nat ≝ nat_of_bitvector eight c in
    7276    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        ].
    73103   
    74104ndefinition add_8_with_carry ≝ add_n_with_carry eight.
Note: See TracChangeset for help on using the changeset viewer.