Changeset 275


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.

Location:
Deliverables/D4.1/Matita
Files:
3 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
  • Deliverables/D4.1/Matita/BitVector.ma

    r273 r275  
    210210nqed.
    211211
    212 ncheck bitvector_of_nat.
    213 
    214212nlet rec nat_of_bitvector (n: Nat) (b: BitVector n) on b ≝
    215213  match b with
     
    219217        ((exponential (S (S Z)) o) * hdval) + nat_of_bitvector o tl
    220218    ].
    221 
    222 (*
    223 nlet rec equality (n: Nat) (b: BitVector n) (c: BitVector n) on b ≝
    224   match b with
    225     [ Empty ⇒
    226       match c return λx.λ_. x = Z → Bool with
    227         [ Empty ⇒ True
    228         | Cons o hd tl ⇒ λabsd1: ?
    229     | Cons
    230     ].
    231 *)
  • Deliverables/D4.1/Matita/Nat.ma

    r265 r275  
    4343    n ≤ m.
    4444
    45 ndefinition greater_than_or_equal_b
     45ndefinition greater_than_or_equal_b: ∀m, n: Nat. Bool
    4646  λm, n: Nat.
    4747    n ≤ m.
     
    190190interpretation "Nat exponential" 'exponential n m = (exponential n m).
    191191
     192nlet rec decidable_equality (m: Nat) (n: Nat) on m: Bool ≝
     193  match m with
     194    [ Z ⇒
     195      match n with
     196        [ Z ⇒ true
     197        | _ ⇒ false
     198        ]
     199    | S o ⇒
     200      match n with
     201        [ S p ⇒ decidable_equality o p
     202        | _ ⇒ false
     203        ]
     204    ].
     205
    192206(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    193207(* Greatest common divisor and least common multiple.                         *)
Note: See TracChangeset for help on using the changeset viewer.