namespace http://mathhub.info/MitM/core/arithmetics ❚
import base http://mathhub.info/MitM/Foundation ❚
theory NaturalNumbers : base:?Logic =
include ☞base:?NatLiterals ❙
succ : ℕ ⟶ ℕ ❘ # Succ 1 prec 5 ❘ = [n] succ_nat_lit n ❙
axiom_succ1 : {x} ⊦ 0 ≠ Succ x ❙
axiom_succ2 : {x:ℕ,y:ℕ} ⊦ Succ x ≐ Succ y ⟶ ⊦ x ≐ y ❙
axiom_Induction: {A : ℕ ⟶ bool} ⊦ A 0 ⟶ ({x}⊦ A x ⟶ ⊦ A (Succ x)) ⟶ {x} ⊦ A x ❙
❚
theory NaturalArithmetics : base:?Logic =
include ?NaturalNumbers ❙
include ☞base:?DescriptionOperator ❙
/T Addition ❙
addition : ℕ ⟶ ℕ ⟶ ℕ ❘ # 1 + 2 prec 15 ❘ = plus_nat_lit ❙
axiom_plus1 : {x} ⊦ x + 0 ≐ x ❘ # axiom_plus1 ❙
axiom_plus2 : {x,y} ⊦ x + Succ y ≐ Succ (x + y) ❙
/T Subtraction ❙
subtraction : {n : ℕ, m : ℕ, p : ⊦ ∃! [x : ℕ] m + x ≐ n}ℕ ❘ = [n,m,p] ι [x: ℕ] m + x ≐ n ❘ # 1 - 2 %I3 prec 15 ❙
// TODO proof arguments are in the way ❙
// theorem_sub1: ⊦ ∀[n] n - zero ≐ n ❙
// theorem_sub2: ⊦ ∀[n] ∀[m] m ≤ n ⇒ (S n) - (S m) ≐ n - m ❙
/T Multiplication ❙
multiplication : ℕ ⟶ ℕ ⟶ ℕ ❘ # 1 ⋅ 2 prec 25 ❘ = times_nat_lit ❙
axiom_times1 : {x : ℕ} ⊦ x ⋅ 1 ≐ x ❙
axiom_times2 : {x,y} ⊦ x ⋅ Succ y ≐ x + x ⋅ y ❙
axiom_times3 : {x: ℕ} ⊦ x ⋅ 0 ≐ 0 ∧ 0 ⋅ x ≐ 0 ❙
/T Division ❙
divides : ℕ ⟶ ℕ ⟶ bool ❘ = [n,m] ∃! [r : ℕ] n ⋅ r ≐ m ❘ # 1 | 2 prec 105 ❙
div : {n : ℕ, m : ℕ, p : ⊦ ∃! [r : ℕ] n ⋅ r ≐ m} ℕ ❘ = [n,m,p] ι ([r : ℕ] n ⋅ r ≐ m) ❘ # 1 / 2 %I3 prec 105 ❙
// theorem_div1: ⊦ ∀[n] ¬ (n ≐ 0) ⇒ zero / n ≐ zero ❙
// theorem_div2: ⊦ ∀[n] ∀[m] ¬(m ≐ zero) ∧ (m | n) ⇒ n / m ≐ S ((n - m) / m) ❙
/T Exponentiation ❙
exponentiation : ℕ ⟶ ℕ ⟶ ℕ ❘ # 1 ^ 2 prec 35 ❙
axiom_exp1 : {x} ⊦ x ^ 0 ≐ 1 ❙
axiom_exp2 : {x,y} ⊦ x ^ Succ y ≐ x ⋅ x ^ y ❙
/T Roots ❙
root : {n : ℕ, m : ℕ, p : ⊦ ∃![x] x^m ≐ n}ℕ ❘ = [n,m,p] ι [x] x^m ≐ n ❘ # 2 √ 1 %I3 prec 35❙
squareRoot : {n : ℕ, p : ⊦ ∃![m] m^2 ≐ n}ℕ ❘ = [n,p] 2 √ n ❘ # √ 1 %I2 prec 35 ❙
/T Order ❙
leq : ℕ ⟶ ℕ ⟶ bool ❘ = [n,m] ∃! [x] n + x ≐ m ❘ # 1 ≤ 2 prec 105 ❙
geq : ℕ ⟶ ℕ ⟶ bool ❘ = [n,m] m ≤ n ❘ # 1 ≥ 2 prec 105 ❙
lessthan : ℕ ⟶ ℕ ⟶ bool ❘ = [n,m] n ≤ m ∧ n ≠ m ❘ # 1 < 2 prec 105 ❙
morethan : ℕ ⟶ ℕ ⟶ bool ❘ = [n,m] n ≥ m ∧ n ≠ m ❘ # 1 > 2 prec 105 ❙
/T Others ❙
max : ℕ ⟶ ℕ ⟶ ℕ ❘ # max 1 2 ❙
min : ℕ ⟶ ℕ ⟶ ℕ ❘ # min 1 2 ❙
mod : ℕ ⟶ ℕ ⟶ ℕ ❘ # 1 mod 2 prec 25 ❙
// axiom_mod1: ⊦ ∀[n] ∀[m] n < m ⇒ (n mod m) ≐ n ❙
// axiom_mod2: ⊦ ∀[n] ∀[m] (m ≤ n) ⇒ ((n mod m) ≐ ((n - m) mod m)) ❙
primes : type ❘ = ⟨ x : ℕ+ | ⊦ x ≠ 1 ∧ ∀ [y : ℕ] (y | x) ⇒ (y ≐ 1 ∨ y ≐ x) ⟩ ❙
fromOneTo : ℕ+ ⟶ type ❘ = [n] ⟨ x: ℕ+ | ⊦ 1 ≤ x ∧ x ≤ n ⟩ ❙
/T Monoid Axioms ❙
axiom_associativePlus : {x: ℕ,y,z} ⊦ x + (y + z) ≐ (x + y) + z ❘ # associative_plus_nat 1 2 3❙
axiom_leftUnitalPlus : {x : ℕ} ⊦ 0 + x ≐ x ❘ # leftunital_plus_nat ❙
lemma_rightUnitalPlus : {x : ℕ} ⊦ x + 0 ≐ x ❘ = axiom_plus1 ❘ # rightunital_plus_nat ❙
❚