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 ❙
❚