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

Removed all axioms from Arithmetic.ma and replaced them with implemented functions from other files. Implemented decidable equality on Nats.

File:
1 edited

Legend:

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

    r274 r275  
    6262nqed.
    6363
    64 naxiom less_than_or_equal_b: Nat → Nat → Bool.
    65 naxiom ior: Bool → Bool → Bool.
    66 naxiom neg: Bool → Bool.
    67 naxiom con: Bool → Bool → Bool.
    68 naxiom eq: Nat → Nat → Bool.
    69 
    7064ndefinition sub_8_with_carry: ∀b,c: BitVector eight. ∀carry: Bool. Cartesian (BitVector eight) (List Bool) ≝
    7165  λb: BitVector eight.
     
    7670    let carry_as_nat ≝ nat_of_bool carry in
    7771    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
     72    let ac_flag ≝ inclusive_disjunction
     73                    (negation (conjunction (less_than_or_equal_b (modulus b_as_nat sixteen) (modulus c_as_nat sixteen)) (less_than_or_equal_b temporary carry_as_nat)))
     74                    (conjunction (conjunction (decidable_equality b_as_nat Z) (decidable_equality c_as_nat Z)) (decidable_equality carry_as_nat Z)) in
     75    let bit_six ≝ inclusive_disjunction
     76                    (negation (conjunction (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)))
     77                    (conjunction (conjunction (decidable_equality b_as_nat Z) (decidable_equality c_as_nat Z)) (decidable_equality carry_as_nat Z)) in
    8478    let old_result_1 ≝ b_as_nat - c_as_nat in
    8579    let old_result_2 ≝ old_result_1 - carry_as_nat in
Note: See TracChangeset for help on using the changeset viewer.