Theory Number_Toolkit

section ‹ Number Toolkit ›

theory Number_Toolkit
  imports Function_Toolkit
begin

text ‹ The numeric operators are all implemented in HOL (@{const "plus"}, @{const "minus"}, 
  @{const times}, etc.), and there seems little to be gained by repackaging them. However,
  we do make some syntactic additions. ›

subsection ‹ Successor ›

abbreviation (input) "succ n ≡ n + 1"

subsection ‹ Integers ›

type_notation int ("ℤ")

subsection ‹ Natural numbers ›

type_notation nat ("ℕ")

subsection ‹ Rational numbers ›

type_notation rat ("ℚ")

subsection ‹ Real numbers ›

type_notation real ("ℝ")

subsection ‹ Strictly positive natural numbers ›

definition Nats1 ("ℕ⇩1") where "ℕ⇩1 = {x ∈ ℕ. ¬ x = 0}"

subsection ‹ Non-zero integers ›

definition Ints1 ("ℤ⇩1") where "ℤ⇩1 = {x ∈ ℤ. ¬ x = 0}"

end