Ignore:
Timestamp:
Nov 24, 2010, 1:43:28 PM (10 years ago)
Author:
mulligan
Message:

Changes from this morning.

File:
1 edited

Legend:

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

    r260 r272  
    6262nqed.
    6363
    64 (*
     64naxiom less_than_b: Nat → Nat → Bool.
     65
    6566ndefinition sub_8_with_carry ≝
    6667  λb: BitVector eight.
     
    7071    let c_as_nat ≝ nat_of_bitvector eight c in
    7172    let carry_as_nat ≝ nat_of_bool carry in
    72     let result_old_1 ≝ subtraction_underflow b_as_nat c_as_nat in
    73       match result_old_1 with
    74         [ Nothing ⇒
    75           let ac_flag ≝ True in
    76          
    77         | Just result_old_1' ⇒
    78         ]
    79 *)
     73    let result_old_1 ≝ minus (minus b_as_nat c_as_nat) carry_as_nat in
     74    let modulus_1 ≝ (modulus b_as_nat sixteen) - (modulus c_as_nat sixteen) in
     75      match less_than_b (modulus b_as_nat sixteen) (modulus c_as_nat sixteen) with
     76        [ true ⇒
     77          let ac_flag ≝ true in
     78          let result_old_2 ≝ (minus (modulus b_as_nat one_hundred_and_twenty_eight)
     79                                   (modulus c_as_nat one_hundred_and_twenty_eight)) in
     80            match less_than_b (modulus b_as_nat one_hundred_and_twenty_eight)
     81                              (modulus c_as_nat one_hundred_and_twenty_eight) with
     82            [ true ⇒
     83              let bit_six ≝ true in
     84              let result_carry ≝ mk_Cartesian … result_old_1 false in
     85              let ov_flag ≝ exclusive_disjunction cy_flag bit_six in
     86                mk_Cartesian … (first … result_carry) (second … result_carry :: ac_flag :: ov_flag :: Empty Bool)
     87            | false ⇒ ?
     88            ]
     89        | false ⇒ ?
     90        ].
     91   
    8092   
    8193ndefinition add_8_with_carry ≝ add_n_with_carry eight.
Note: See TracChangeset for help on using the changeset viewer.