namespace http://mathhub.info/MitM/core/arithmetics ❚
import base http://mathhub.info/MitM/Foundation ❚
theory IntegerNumbers : base:?Logic =
include ?NaturalNumbers ❙
include ☞base:?IntLiterals ❙
axiom_natsAreInt : nat_lit <* int_lit ❙
axiom_natsAreInt2 : NAT <* int_lit ❙
axiom_posAreInt : pos_lit <* int_lit ❙
negative : ℤ ⟶ ℤ ❘ = minus_int_lit❙
axiom_negZeroIsZero : ⊦ negative 0 ≐ 0 ❙
axiom_negPosIsNotId: {n : ℕ+} ⊦ neq int_lit (negative n) n ❙
axiom_negPosIsInj: {n,m: ℕ} ⊦ negative n ≐ negative m ⟶ ⊦ n ≐ m ❙
❚
theory IntegerArithmetics : base:?Logic =
include ?NaturalArithmetics ❙
include ?IntegerNumbers ❙
/T Negation ❙
uminus : ℤ ⟶ ℤ ❘ # - 1 prec 34 ❘ = minus_int_lit ❙
axiom_uminusIsNeg : {n: ℕ} ⊦ -n ≐ negative n ❙
axiom_uminusIsNilp : {z:ℤ} ⊦ - (- z) ≐ z ❙
/T Addition ❙
addition : ℤ ⟶ ℤ ⟶ ℤ ❘ # 1 + 2 prec 14 ❘ = plus_int_lit ❙
axiom_intPlusIsNatplus : {x : ℕ, y : ℕ} ⊦ arithmetics?IntegerArithmetics?addition x y ≐ arithmetics?NaturalArithmetics?addition x y ❙
axiom_additionCommutative : {x : ℤ, y : ℤ} ⊦ x + y ≐ y + x ❘ # axiom_additionCommutative ❙
axiom_plusUminus : {x : ℤ} ⊦ x + (-x) ≐ 0 ❘ # axiom_plusUminus ❙
/T Subtraction ❙
subtraction : ℤ ⟶ ℤ ⟶ ℤ ❘ = [a,b] a + (-b) ❘ # 1 - 2 prec 14 ❙
/T Multiplication ❙
multiplication : ℤ ⟶ ℤ ⟶ ℤ ❘ # 1 ⋅ 2 prec 24 ❘ = times_int_lit ❙
axiom_intTimesIsNattimes : {x : ℕ, y : ℕ} ⊦ arithmetics?IntegerArithmetics?multiplication x y ≐ arithmetics?NaturalArithmetics?multiplication x y ❙
/T Division ❙
div : {x : ℤ, y : ℤ, p : ⊦ ∃! [z] y ⋅ z ≐ x} ℤ ❘ = [x,y,p] ι [z] y ⋅ z ≐ x ❘ # 1 / 2 %I3 prec 24 ❙
/T Exponentiation ❙
exponentiation : ℤ ⟶ ℤ ⟶ ℤ ❘ # 1 ^ 2 prec 34 ❙
axiom_intExpIsNatexp : {x : ℕ, y : ℕ} ⊦ arithmetics?IntegerArithmetics?exponentiation x y ≐ arithmetics?NaturalArithmetics?exponentiation x y ❙
/T Roots ❙
root : {n : ℤ, m : ℕ, p : ⊦ ∃![x] x^m ≐ n}ℤ ❘ = [n,m,p] ι [x] x^m ≐ n ❘ # 2 √ 1 %I3 prec 34 ❙
// squareRoot : {n : ℤ, p : ⊦ ∃![m] m^2 ≐ n}ℤ ❘ = [n,p] 2 √ n ❘ # √ 1 %I2 prec 34 ❙
// squareRoot is technically only defined on naturals anyway ❙
/T Order ❙
leq : ℤ ⟶ ℤ ⟶ bool ❘ = [x,y] ∃ [n: ℕ] eq ℤ (arithmetics?IntegerArithmetics?addition x n) y ❘ # 1 ≤ 2 prec 104 ❙
geq : ℤ ⟶ ℤ ⟶ bool ❘ = [n,m] m ≤ n ❘ # 1 ≥ 2 prec 104 ❙
lessthan : ℤ ⟶ ℤ ⟶ bool ❘ = [n,m] n ≤ m ∧ n ≠ m ❘ # 1 < 2 prec 104 ❙
morethan : ℤ ⟶ ℤ ⟶ bool ❘ = [n,m] n ≥ m ∧ n ≠ m ❘ # 1 > 2 prec 104 ❙
max : ℤ ⟶ ℤ ⟶ ℤ ❘ # max 1 2 ❙
min : ℤ ⟶ ℤ ⟶ ℤ ❘ # min 1 2 ❙
axiom_intLeqIsNatLeq : {x : ℕ, y : ℕ} ⊦ arithmetics?NaturalArithmetics?leq x y ≐ arithmetics?IntegerArithmetics?leq x y ❙
/T Others ❙
mod : ℤ ⟶ ℤ ⟶ ℤ ❘ # 1 mod 2 prec 24 ❙
up : {z : ℤ, p : ⊦ z ≥ 0}ℕ ❘ # ℤtoℕ 1 %I2 ❙
axiom_up : {n : ℕ,p : ⊦ n ≥ 0} ⊦ ℤtoℕ n ≐ n ❙
// natissub : ℕ ≐≐ ⟨ ℤ | ([z] ⊦ ¬ z < 0) ⟩ ❙
posisneqzero : ℕ+ <* ⟨ x: ℤ | ⊦ x ≠ 0 ⟩ ❙
absolute : ℤ ⟶ ℕ ❙ // ❘ = [z] case z <0 ⟹ up (-z) . up z ❘ # | 1 | prec 10 ❙
// TODO: axioms for the other ones as well.❙
/T Group Axioms ❙
axiom_associativePlus : {x: ℤ,y,z} ⊦ arithmetics?IntegerArithmetics?addition x (arithmetics?IntegerArithmetics?addition y z) ≐
arithmetics?IntegerArithmetics?addition (arithmetics?IntegerArithmetics?addition x y) z ❘ # associative_plus_int 1 2 3❙
axiom_associativeTimes : {x: ℤ,y,z} ⊦ x ⋅ (y ⋅ z) ≐ (x ⋅ y) ⋅ z ❘ # associative_times_int 1 2 3 ❙
axiom_leftUnitalPlus : {x : ℤ} ⊦ arithmetics?IntegerArithmetics?addition 0 x ≐ x ❘ # leftunital_plus_int 1 ❙
axiom_rightUnitalPlus : {x : ℤ} ⊦ arithmetics?IntegerArithmetics?addition x 0 ≐ x ❘ # rightunital_plus_int 1❙
axiom_leftUnitalTimes : {x : ℤ} ⊦ 1 ⋅ x ≐ x ❘ # leftunital_times_int 1 ❙
axiom_rightUnitalTimes : {x : ℤ} ⊦ x ⋅ 1 ≐ x ❘ # rightunital_times_int 1 ❙
axiom_distributive : {x : ℤ, y : ℤ, z : ℤ} ⊦ arithmetics?IntegerArithmetics?multiplication x (arithmetics?IntegerArithmetics?addition y z) ≐
arithmetics?IntegerArithmetics?addition (arithmetics?IntegerArithmetics?multiplication x y) (arithmetics?IntegerArithmetics?multiplication x z) ❘ # distributive_int 1 2 3 ❙
❚