Ignore:
Timestamp:
Nov 22, 2010, 11:43:04 AM (10 years ago)
Author:
mulligan
Message:

More changes. Added datatype for addressing modes.

File:
1 edited

Legend:

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

    r246 r248  
    1 include "Infrastructure/Universes.ma".
    2 include "Infrastructure/Equality.ma".
    3 include "Infrastructure/Connectives.ma".
    4 
    5 include "Common/Nat/Nat.ma".
    6 include "Common/Nat/Addition.ma".
    7 include "Common/Nat/Multiplication.ma".
    8 include "Common/Nat/Division_Modulus.ma".
    9 include "Common/Nat/Order.ma".
    10 
    11 include "Programming/Datatypes/Bool.ma".
    12 
    13 include "Programming/Datatypes/Listlike/Vector/BitVector.ma".
    14 include "Programming/Datatypes/Listlike/List/List.ma".
     1include "Universes.ma".
     2include "Equality.ma".
     3include "Connectives.ma".
     4include "Nat.ma".
     5include "Exponential.ma".
     6include "Bool.ma".
     7include "BitVector.ma".
     8include "List.ma".
    159   
    1610ndefinition eight ≝ exponential (S(S(Z))) (S(S(S(Z)))).
    1711ndefinition sixteen ≝ eight + eight.
    18 ndefinition one_hundred_and_twenty_eight ≝ sixteen × eight.
     12ndefinition one_hundred_and_twenty_eight ≝ sixteen * eight.
    1913ndefinition two_hundred_and_fifty_six ≝
    2014  one_hundred_and_twenty_eight + one_hundred_and_twenty_eight.                                         
     15   
     16ndefinition nat_of_bool ≝
     17  λb: Bool.
     18    match b with
     19      [ False ⇒ Z
     20      | True ⇒ S Z
     21      ].
    2122   
    2223ndefinition add_n_with_carry:
     
    3031    let carry_as_nat ≝ nat_of_bool carry in
    3132    let result_old ≝ b_as_nat + c_as_nat + carry_as_nat in
    32     let ac_flag ≝ ((modulus b_as_nat ((S (S Z)) × n)) +
    33                   (modulus c_as_nat ((S (S Z)) × n)) +
    34                   c_as_nat) ≥ ((S (S Z)) × n) in
     33    let ac_flag ≝ ((modulus b_as_nat ((S (S Z)) * n)) +
     34                  (modulus c_as_nat ((S (S Z)) * n)) +
     35                  c_as_nat) ≥ ((S (S Z)) * n) in
    3536    let bit_xxx ≝ (((modulus b_as_nat ((S (S Z))^(n - (S Z)))) +
    3637                  (modulus c_as_nat ((S (S Z))^(n - (S Z)))) +
     
    3940    let cy_flag ≝ (result_old ≥ ((S (S Z))^n)) in
    4041    let ov_flag ≝ exclusive_disjunction cy_flag bit_xxx in
    41       ? (mk_Cartesian (BitVector n) ? (bitvector_of_nat n result)
     42      ? (mk_Cartesian (BitVector n) ? (? (bitvector_of_nat n result))
    4243                          (cy_flag :: ac_flag :: ov_flag :: Empty Bool)).
    4344    //.
     
    6465ndefinition add_16_with_carry ≝ add_n_with_carry sixteen.
    6566
     67(*
    6668ndefinition increment ≝
    6769  λn: Nat.
     
    7072    let overflow ≝ b_as_nat ≥ (S (S Z))^n in
    7173      match overflow with
    72         [ True ⇒ bitvector_of_nat n Z
    73         | False ⇒ bitvector_of_nat n b_as_nat
     74        [ False ⇒ bitvector_of_nat n b_as_nat
     75        | True ⇒ bitvector_of_nat n Z
    7476        ].
    7577       
     
    9294  //.
    9395nqed.
     96
     97*)
Note: See TracChangeset for help on using the changeset viewer.