Theory HyperInt

(*  Title:  HyperInt.thy
    Author: Jacques D. Fleuriot, University of Edinburgh, 2026
*)

section‹Hyperinteger numbers›

theory HyperInt
  imports AuxiliaryNSA "HOL-Nonstandard_Analysis.NSA"
begin

type_synonym hypint = "int star"

abbreviation
  hypint_of_int :: "int ⇒ int star" where
  "hypint_of_int ≡ star_of"

abbreviation
  hypint_of_hypnat :: "hypnat ⇒ hypint" where
  "hypint_of_hypnat ≡ of_hypnat"

subsection‹Properties of Hyperintegers›

text‹Many properties hold by transfer from the integers›

lemma hypint_nat_mult_less_mono2_lemma:
     "(i::hypint)<j ⟹ 0<k ⟹ of_nat k * i < of_nat k * j"
by (metis mult_less_cancel_left_disj of_nat_0_less_iff)

lemma hypint_mult_less_mono2_lemma:
     "⋀i j k. (i::hypint)<j ⟹ 0<k ⟹ of_hypnat k * i < of_hypnat k * j"
by transfer (rule zmult_zless_mono2_lemma)

lemma zero_le_imp_eq_hypint: "⋀k. (0::hypint) ≤ k ⟹ ∃n. k = of_hypnat n"
by transfer (rule zero_le_imp_eq_int)

lemma zero_less_imp_eq_hypint: "⋀k. (0::hypint) < k ⟹ ∃n>0. k = of_hypnat n"
by transfer (rule zero_less_imp_eq_int)

lemma hypint_less_mono2: "⋀i j k. ⟦ i<j;  (0::hypint) < k ⟧ ⟹ k*i < k*j"
by transfer (rule zmult_zless_mono2)

lemma hypint_less_imp_add1_le: "⋀w z. w < z ⟹ w + (1::hypint) ≤ z"
by transfer (rule zless_imp_add1_zle)

lemma hypint_less_iff_hSuc_add:
  "⋀w z. (w :: hypint) < z ⟷ (∃n. z = w + of_hypnat (hSuc n))"
by transfer (rule zless_iff_Suc_zadd)

lemma hypint_le_iff_add:
  "⋀w z. (w :: hypint) ≤ z ⟷ (∃n. z = w + of_hypnat n)"
by transfer (simp add: zle_iff_zadd)

lemma hypint_le_iff_diff:
  "⋀w z. (w :: hypint) ≤ z ⟷ (∃n. w = z - of_hypnat n)"
using hypint_le_iff_add by auto

lemma hypint_less_zero_eq_minus_of_hypnat: "x < (0::hypint) ⟹ ∃n. x = - hypint_of_hypnat (n)"
by (metis minus_minus neg_0_less_iff_less zero_less_imp_eq_hypint)

lemma hypint_less_add1_eq: "⋀w z. (w < z + (1::hypint)) = (w<z | w=z)"
by transfer (rule zless_add1_eq)

lemma add1_hypint_le_eq: "⋀w z. (w + (1::hypint)≤ z) = (w<z)"
by transfer (rule add1_zle_eq)

lemma hypint_le_diff1_eq [simp]: "⋀w z. (w ≤ z - (1::hypint)) = (w<z)"
by transfer (rule zle_diff1_eq)

lemma hypint_le_add1_eq_le [simp]: "⋀w z. (w < z + (1::hypint)) = (w ≤ z)"
by transfer (rule zle_add1_eq_le)

lemma hypint_one_le_iff_zero_less: "⋀z. ((1::hypint) ≤ z) = (0 < z)"
by transfer (rule int_one_le_iff_zero_less)


subsection‹Embedding of the hyperintegers into other types› 

definition
  of_hypint :: "hypint => 'a::linordered_idom star" where
  of_hypint_def [transfer_unfold]: "of_hypint = *f* of_int"

lemma of_hypint_of_int [simp]: "of_hypint (of_int z) = of_int z"
by transfer simp

lemma of_hypint_hypint_of_int [simp]: "of_hypint (hypint_of_int z) = of_int z"
by transfer simp

lemma of_hypint_of_hypnat [simp]: "⋀z. of_hypint (of_hypnat z) = of_hypnat z"
by transfer simp

lemma of_hypint_of_nat [simp]: "of_hypint (of_nat z) = of_nat z"
by transfer simp

lemma of_hypint_0 [simp]: "of_hypint 0 = 0"
by transfer (rule of_int_0)

lemma of_hypint_1 [simp]: "of_hypint 1 = 1"
by transfer (rule of_int_1)

lemma of_hypint_add [simp]: "⋀w z. of_hypint (w+z) = of_hypint w + of_hypint z"
by transfer (rule of_int_add)

lemma of_hypint_minus [simp]: "⋀z. of_hypint (-z) = - (of_hypint z)"
by transfer (rule of_int_minus)

lemma of_hypint_diff [simp]: "⋀w z. of_hypint (w - z) = of_hypint w - of_hypint z"
by transfer (rule of_int_diff)

lemma of_hypint_mult [simp]: "⋀w z. of_hypint (w*z) = of_hypint w * of_hypint z"
by transfer (rule of_int_mult)

lemma of_hypint_of_nat_eq [simp]: "of_hypint (of_nat n) = of_nat n"
by (induct n) auto

lemma of_hypint_nat_power: "of_hypint (z ^ n) = of_hypint z ^ n"
  by (induct n) simp_all

lemma of_hypint_eq_iff [simp]:
   "⋀w z. of_hypint w = of_hypint z ⟷ w = z"
by transfer (rule of_int_eq_iff)

lemma of_hypint_eq_0_iff [simp]:
  "⋀z. of_hypint z = 0 ⟷ z = 0"
by transfer (rule of_int_eq_0_iff)

lemma of_hypint_0_eq_iff [simp]:
  "⋀z. 0 = of_hypint z ⟷ z = 0"
by transfer (rule of_int_0_eq_iff)

lemma of_hypint_le_iff [simp]:
  "⋀ w z. of_hypint w ≤ of_hypint z ⟷ w ≤ z"
by transfer (rule of_int_le_iff)

lemma of_hypint_less_iff [simp]:
  "⋀w z. of_hypint w < of_hypint z ⟷ w < z"
by transfer (rule of_int_less_iff)  

lemma of_hypint_0_le_iff [simp]:
  "⋀z. 0 ≤ of_hypint z ⟷ 0 ≤ z"
by transfer (rule of_int_0_le_iff)

lemma of_hypint_le_0_iff [simp]:
  "⋀z. of_hypint z ≤ 0 ⟷ z  ≤ 0"
by transfer (rule of_int_le_0_iff)

lemma of_hypint_0_less_iff [simp]:
  "⋀z. 0 < of_hypint z ⟷ 0 < z"
by transfer (rule of_int_0_less_iff)

lemma of_hypint_less_0_iff [simp]:
  "⋀z. of_hypint z < 0 ⟷ z < 0"
by transfer (rule of_int_less_0_iff)  

lemma of_hypint_abs: "⋀z. of_hypint (abs z) = abs(of_hypint z)"
by transfer (simp add: abs_if)

lemma of_hypint_add_one: "of_hypint z + (1 :: real star) = of_hypint (z + 1)"
by (metis of_hypint_1 of_hypint_add)

subsection‹Embedding the naturals into the hyperintegers›

abbreviation
  hypint_of_nat :: "nat => hypint" where
  "hypint_of_nat == of_nat"

lemma HypintNat_eq: "Nats = {z. ∃N. z = hypint_of_nat N}"
by (simp add: Nats_def image_def)

lemma hypint_of_nat:
     "hypint_of_nat m = star_n (%n. int m)"
by (fold star_of_def) simp

lemma HypintNat_ge_zero: "n ∈ ℕ ⟹ 0 ≤ (n :: hypint)"
by (auto simp add: Nats_def)

lemma hypint_of_hypnat_hypint_of_nat_eq [simp]:
     "⋀n. hypint_of_hypnat (hypnat_of_nat n) = hypint_of_nat n"
by (simp add: of_hypnat_def)

lemma abs_hypint_of_hypnat [simp]: "¦hypint_of_hypnat n¦ = hypint_of_hypnat n"
  by (auto simp add: abs_if)

lemma hypint_abs_less_one_iff [simp]: "⋀z. (¦z¦ < 1) = (z = (0::hypint))"
by transfer simp

lemma abs_hypint_mult_eq_1:
    "⋀m n. ¦m * n¦ = 1 ⟹ ¦m¦ = (1::hypint)"
by transfer (rule abs_zmult_eq_1)
 
lemma pos_hypint_mult_eq_1_iff_lemma: 
    "⋀m n. (m * n = 1) ==> m = (1::hypint) | m = -1"
by transfer (rule pos_zmult_eq_1_iff_lemma)

lemma pos_hypint_mult_eq_1_iff:
   "⋀m n. 0 < (m::hypint) ⟹ (m * n = 1) = (m = 1 ∧ n = 1)"
by transfer (rule pos_zmult_eq_1_iff)

lemma hypint_mult_eq_1_iff: 
   "⋀m n. (m*n = (1::hypint)) = ((m = 1 ∧ n = 1) ∨ (m = -1 ∧ n = -1))"
by transfer (rule zmult_eq_1_iff)

subsection‹Magnitude of a hyperinteger› 

definition
  hypnat :: "hypint => hypnat"
where
  [transfer_unfold]: "hypnat ≡ *f* nat"

lemma hypnat_hypint [simp]: "⋀n. hypnat (of_hypnat n) = n"
by transfer simp

lemma hypnat_zero [simp]: "hypnat 0 = 0"
by transfer simp

lemma hypnat_one [simp]: "hypnat 1 = 1"
by (metis hypnat_hypint of_hypnat_1)

lemma hypint_hypnat_eq [simp]: "⋀z. of_hypnat (hypnat z) = (if 0 ≤ z then z else 0)"
by transfer simp

corollary hypnat_0_le: "0 ≤ z ⟹ of_hypnat (hypnat z) = z"
by simp

lemma hypnat_le_0 [simp]: "⋀z. z ≤ 0 ⟹ hypnat z = 0"
by transfer simp

lemma hypnat_le_eq_zle: "⋀w z. 0 < w ∨ 0 ≤ z ⟹ (hypnat w  ≤ hypnat z) = (w ≤ z)"
by transfer (rule nat_le_eq_zle)

corollary hypnat_mono_iff: "0 < z ⟹ (hypnat w < hypnat z) = (w < z)"
by (simp add: hypnat_le_eq_zle linorder_not_le [symmetric])

corollary hypnat_less_eq_less: "0 ≤ w ⟹ (hypnat w < hypnat z) = (w<z)"
by (simp add: hypnat_le_eq_zle linorder_not_le [symmetric])  

lemma less_hypnat_conj [simp]: "⋀w z. (hypnat w < hypnat z) = (0 < z ∧ w < z)"
by transfer (rule zless_nat_conj)

lemma nonneg_eq_hypint:
  fixes z :: hypint
  assumes "0 ≤ z" and "⋀m. z = of_hypnat m ⟹ P"
  shows P
  using assms by (blast dest: hypnat_0_le sym)

lemma hypnat_eq_iff: 
  "⋀ m w. (hypnat w = m) = (if 0 ≤ w then w = of_hypnat m else m=0)"
by transfer (rule nat_eq_iff)

corollary hypnat_eq_iff2: "(m = hypnat w) = (if 0 ≤ w then w = of_hypnat m else m=0)"
by (simp only: eq_commute [of m] hypnat_eq_iff)

lemma hypnat_less_iff: "⋀m w. 0 ≤ w ⟹ (hypnat w < m) = (w < of_hypnat m)"
by transfer (rule nat_less_iff)

lemma hypnat_0_iff[simp]: "⋀i. hypnat i = 0 ⟷ i≤0"
by transfer simp

lemma hypint_eq_iff: "(of_hypnat m = z) = (m = hypnat z ∧ 0 ≤ z)"
by (auto simp add: hypnat_eq_iff2)

lemma zero_less_hypnat_eq [simp]: "(0 < hypnat z) = (0 < z)"
by (insert less_hypnat_conj [of 0], auto)

lemma hypnat_add_distrib:
     "⋀z z'. ⟦ (0::hypint) ≤ z;  0 ≤ z' ⟧ ⟹ hypnat (z+z') = hypnat z + hypnat z'"
by transfer (rule nat_add_distrib)

lemma hypnat_diff_distrib:
     "⋀z z'. ⟦ (0::hypint) ≤ z';  z' ≤ z ⟧ ⟹ hypnat (z-z') = hypnat z - hypnat z'"
by transfer (rule nat_diff_distrib)

lemma hypnat_minus_hypint [simp]: "⋀n. hypnat (- (of_hypnat n)) = 0"
by transfer simp

lemma less_hypnat_eq_hypint_less: "⋀m z. (m < hypnat z) = (of_hypnat m < z)"
  by transfer (rule zless_nat_eq_int_zless)

lemma hypnat_add_one: "0 ≤ z ⟹ hypnat z + (1 :: nat star) = hypnat (z + 1)"
by (metis hypint_eq_iff hypnat_add_distrib of_hypnat_1)

subsection‹The divides relation›

lemma hypint_dvd_antisym_nonneg:
    "⋀m n. 0 <= m ⟹ 0 <= n ⟹ m dvd n ⟹ n dvd m ⟹ m = (n::hypint)"
by transfer (rule zdvd_antisym_nonneg)
  
lemma  hypint_dvd_antisym_abs:
    "⋀a b. ⟦ (a::hypint) dvd b; b dvd a ⟧ ⟹ ¦a¦ = ¦b¦"
by transfer (rule zdvd_antisym_abs)

lemma hyperint_dvd_diffD: "⋀k m n. k dvd m - n ⟹ k dvd n ⟹ k dvd (m::hypint)"
by transfer (rule zdvd_zdiffD)

lemma hypint_dvd_reduce: "⋀k m n. (k dvd n + k * m) = (k dvd (n::hypint))"
by transfer (rule zdvd_reduce)

lemma hypint_dvd_imp_le_hypint:
    "⋀d i. ⟦ i ≠ 0; d dvd (i::hypint) ⟧ ⟹ ¦d¦ ≤ ¦i¦"
by transfer (rule dvd_imp_le_int)

lemma hypint_dvd_not_less:
    "⋀m n. ⟦ 0 < m; m < (n::hypint) ⟧ ⟹ ¬ n dvd m"
by transfer (rule zdvd_not_zless)

lemma hypint_dvd_mult_cancel: 
    "⋀k m n. ⟦ k * m dvd k * n; k ≠ (0::hypint) ⟧ ⟹ m dvd n"
by transfer (rule zdvd_mult_cancel)

theorem dvd_hypint_of_hypnat: 
  "⋀x y. ((x::hypnat) dvd y) = ((hypint_of_hypnat x) dvd  (hypint_of_hypnat y))"
  by transfer simp

lemma hypint_dvd1_eq[simp]: "⋀x. (x::hypint) dvd 1 = ( ¦x¦ = 1)"
by transfer (rule zdvd1_eq)

lemma hypint_dvd_mult_cancel1: 
  "⋀m n. m ≠ (0::hypint) ⟹ (m * n dvd m) = (¦n¦ = 1)"
by transfer (rule zdvd_mult_cancel1)

lemma hypint_of_hypnat_dvd_iff: 
  "⋀m z. ((of_hypnat m) dvd z) = (m dvd hypnat (abs z))"
  using dvd_hypint_of_hypnat by auto

lemma dvd_hypint_iff: "⋀m z. (z dvd of_hypnat m) = (hypnat (abs z) dvd m)"
  using nat_abs_dvd_iff by transfer blast

lemma hypnat_dvd_iff: "(hypnat z dvd m) = (if 0 ≤ z then (z dvd of_hypnat m) else m = 0)"
  by (auto simp add: dvd_hypint_iff)

lemma eq_hypnat_hypnat_iff:
  "0 ≤ z ⟹ 0 ≤ z' ⟹ hypnat z = hypnat z' ⟷ z = z'"
  by (auto elim!: nonneg_eq_hypint)

lemma hypnat_power_eq:
  "⋀z. 0 ≤ z ⟹ hypnat (z ^ n) = hypnat z ^ n"
by transfer (rule nat_power_eq)

lemma hypint_dvd_imp_le: 
  "⋀n z. ⟦ z dvd n; 0 < n ⟧ ⟹ z ≤ (n::hypint)"
by transfer (rule zdvd_imp_le)

lemma hypint_period: 
  "⋀a c d t x. (a::hypint) dvd d ⟹ a dvd (x + t) ⟷ a dvd ((x + c * d) + t)"
by transfer (rule zdvd_period)

subsection‹Division on @{typ hypint}› 

lemma hypint_of_nat_div: "hypint_of_nat(m div n) = hypint_of_nat m div (hypint_of_nat n)"
by transfer (simp add: zdiv_int)

lemma hypint_of_hypnat_div: "⋀m n. hypint_of_hypnat(m div n) = hypint_of_hypnat m div (hypint_of_hypnat n)"
by transfer (simp add: zdiv_int)

lemma HypintNats_div: "⟦(n::hypint) ∈ ℕ; m ∈ ℕ ⟧ ⟹ n div m ∈ ℕ"
  by (metis Nats_cases hypint_of_nat_div of_nat_in_Nats)

lemma hypint_div_mono1: "⋀a a' b. ⟦ a ≤ a';  0 < (b::hypint) ⟧ ⟹ a div b  ≤ a' div b"
by transfer (rule zdiv_mono1)

lemma hypint_div_neg_pos_less0: "⋀a b. ⟦ a < (0::hypint);  0 < b ⟧ ⟹  a div b < 0"
by transfer (rule div_neg_pos_less0)

lemma hypint_div_nonneg_neg_le0: "⋀a b. ⟦ (0::hypint) ≤ a; b < 0 ⟧ ⟹ a div b ≤ 0"
by transfer (rule div_nonneg_neg_le0)

lemma hypint_div_nonpos_pos_le0: "⋀a b. ⟦ (a::hypint) ≤ 0; b > 0 ⟧ ⟹ a div b  ≤ 0"
by transfer (rule div_nonpos_pos_le0)

lemma hypint_pos_imp_div_nonneg_iff: "⋀a b. (0::hypint) < b ⟹ (0 ≤ a div b) = (0 ≤ a)"
by transfer (rule pos_imp_zdiv_nonneg_iff)

lemma hypint_neg_imp_div_nonneg_iff:
  "⋀a b. b < (0::hypint) ⟹ (0  ≤ a div b) = (a ≤ (0::hypint))"
by transfer (rule neg_imp_zdiv_nonneg_iff)

lemma hypint_pos_imp_div_neg_iff: "⋀a b. (0::hypint) < b ⟹ (a div b < 0) = (a < 0)"
by transfer (rule pos_imp_zdiv_neg_iff)

lemma hypint_neg_imp_div_neg_iff: "⋀a b. b < (0::hypint) ⟹ (a div b < 0) = (0 < a)"
by transfer (rule neg_imp_zdiv_neg_iff)

lemma hypint_nonneg1_imp_div_pos_iff:
  "⋀a b. (0::hypint) ≤ a ⟹ (a div b > 0) = (a ≥ b ∧ b > 0)"
by transfer (rule nonneg1_imp_zdiv_pos_iff)

subsection‹Properties of the set of embedded integers›

lemma of_int_eq_star_of [simp]: "of_int = star_of"
proof
  fix z :: int
  show "of_int z = star_of z" by transfer simp
qed

lemma Ints_eq_Standard: "(ℤ :: int star set) = Standard"
by (auto simp add: Ints_def Standard_def)

lemma hypint_of_int_mem_Ints [simp]: "hypint_of_int z ∈ ℤ"
by (simp add: Ints_eq_Standard)

lemma hypint_of_nat_Suc [simp]:
     "hypint_of_nat (Suc n) = hypint_of_nat n + (1::hypint)"
by transfer simp

lemma of_int_eq_add [rule_format]:
     "∀d::hypint. of_int m = of_int n + d ⟶ d ∈ range of_int"
  by (metis add_diff_cancel_left' of_int_diff rangeI)

subsection‹Infinite hyperintegers›

definition
  (* the set of infinite hyperintegers *)
  HIntInfinite :: "hypint set" where
  "HIntInfinite = {z. z ∉ ℤ}"

lemma Ints_not_HIntInfinite_iff: "(x ∈ Ints) = (x ∉ HIntInfinite)"
by (simp add: HIntInfinite_def)

lemma HIntInfinite_not_Ints_iff: "(x ∈ HIntInfinite) = (x ∉ Ints)"
by (simp add: HIntInfinite_def)

lemma star_of_neq_HIntInfinite: "Z ∈ HIntInfinite ==> star_of n ≠ Z"
by (metis HIntInfinite_not_Ints_iff Ints_of_int of_hypint_hypint_of_int 
     of_hypint_of_int of_int_eq_iff star_of_int_def)

lemma HIntInfinite_minus_iff [simp]: 
  "(- Z ∈ HIntInfinite) =  (Z ∈ HIntInfinite)"
by (metis Ints_minus Ints_not_HIntInfinite_iff minus_minus)


lemma star_of_less_pos_HIntInfinite:
  assumes "0 < Z" and "Z ∈ HIntInfinite"
  shows "star_of z < Z"
proof (cases "z ≥ 0")
  case True
  then obtain n where z: "z = int n"
    using zero_le_imp_eq_int by blast
  have "hypint_of_int (int n) < Z"
  proof (induct n)
    case 0
    then show ?case
      by (simp add: assms(1)) 
  next
    case (Suc n)
    then show ?case
      by (metis assms(2) hypint_less_imp_add1_le hypint_of_nat_Suc 
          less_le star_of_neq_HIntInfinite star_of_of_nat) 
  qed
  then show ?thesis 
    using z by simp
next
  case False
  then obtain n where "z = - int (Suc n)"
    by (metis int_cases of_nat_0_le_iff)
  then show ?thesis
    by (metis False assms(1) le_less less_le_trans not_less star_of_less_0) 
qed

lemma star_of_gt_neg_HIntInfinite:
  assumes "Z < 0"
and  "Z ∈ HIntInfinite"
shows "Z < star_of z"
proof -
  have  "0 < - Z"
    by (simp add: assms(1))
  then show ?thesis using star_of_less_pos_HIntInfinite [of _ "-z"]
    using assms(2) by fastforce
qed

lemma zero_not_HIntInfinite [simp]: "0 ∉ HIntInfinite"
by (metis HIntInfinite_not_Ints_iff Ints_0)

lemma star_of_less_abs_HIntInfinite:
  "Z ∈ HIntInfinite ⟹ star_of z < abs Z"
by (auto intro: star_of_less_pos_HIntInfinite simp add: abs_if not_less le_less)

lemma hypint_of_nat_less_abs_HIntInfinite:
  "y ∈ HIntInfinite ⟹ hypint_of_nat n < ¦y¦"
by (metis star_of_less_abs_HIntInfinite star_of_nat_def)

lemma Ints_less_pos_HIntInfinite: "⟦ 0 < y; x ∈ ℤ; y ∈ HIntInfinite ⟧ ⟹ x < y"
by (auto simp add: Ints_def star_of_less_pos_HIntInfinite)

lemma Ints_gt_neg_HIntInfinite: "⟦ y < 0; x ∈ ℤ; y ∈ HIntInfinite ⟧ ⟹ y < x"
by (auto simp add: Ints_def star_of_gt_neg_HIntInfinite)

lemma Ints_less_abs_HIntInfinite: "⟦ x ∈ ℤ; y ∈ HIntInfinite ⟧ ⟹ x < abs y"
by (auto simp add: Ints_def star_of_less_abs_HIntInfinite)

lemma Ints_le_abs_HIntInfinite: "⟦ x ∈ ℤ; y ∈ HIntInfinite ⟧ ⟹ x ≤ abs y"
by (metis Ints_less_abs_HIntInfinite less_imp_le)

lemma Nats_less_abs_HIntInfinite: "⟦ x ∈ ℕ; y ∈ HIntInfinite ⟧ ⟹ x < abs y"
by (metis Nats_cases hypint_of_nat_less_abs_HIntInfinite)

lemma Nats_le_abs_HIntInfinite: "⟦ x ∈ ℕ; y ∈ HIntInfinite ⟧ ⟹ x < abs y"
by (metis Nats_less_abs_HIntInfinite)

lemma Ints_pos_downward_closed:
  "⟦ 0 ≤ y; x ∈ Ints; (y::hypint) ≤ x ⟧ ⟹ y ∈ ℤ"
  using HIntInfinite_not_Ints_iff Ints_le_abs_HIntInfinite by fastforce

lemma Ints_neg_upward_closed:
  "⟦ y ≤ 0; x ∈ Ints; x ≤ (y::hypint) ⟧ ⟹ y ∈ ℤ"
  by (metis HIntInfinite_not_Ints_iff Ints_0 Ints_gt_neg_HIntInfinite linorder_not_less order_le_less)

lemma HIntInfinite_pos_upward_closed:
  "⟦ 0 ≤ x; x ∈ HIntInfinite; x ≤ y ⟧ ⟹ y ∈ HIntInfinite"
by (auto intro: Ints_pos_downward_closed simp only: HIntInfinite_not_Ints_iff)

lemma HIntInfinite_neg_downward_closed:
  "⟦ x ≤ 0; x ∈ HIntInfinite; y ≤ x ⟧ ⟹ y ∈ HIntInfinite"
by (auto intro: Ints_neg_upward_closed simp only: HIntInfinite_not_Ints_iff)

lemma HIntInfinite_pos_add: 
  "⟦ 0 ≤ x; 0 ≤ y; x ∈ HIntInfinite ⟧ ⟹ x + y ∈ HIntInfinite"
by (metis HIntInfinite_pos_upward_closed add_increasing2 order_refl)

lemma HIntInfinite_neg_add: 
  "⟦ x ≤ 0; y ≤ 0; x ∈ HIntInfinite ⟧ ⟹ x + y ∈ HIntInfinite"
by (metis HIntInfinite_neg_downward_closed add_0_iff add_le_cancel_left)

lemma HIntInfinite_add_Ints: 
  "⟦ x ∈ HIntInfinite; y ∈ Ints ⟧ ⟹ x + y ∈ HIntInfinite"
  by (metis HIntInfinite_not_Ints_iff Ints_diff add.commute add_diff_cancel_left')

lemma HIntInfinite_diff: 
  "⟦ x ∈ HIntInfinite; y ∈ Ints ⟧ ⟹ x - y ∈ HIntInfinite"
by (metis HIntInfinite_not_Ints_iff Ints_add diff_add_cancel)

lemma Ints_def2: "ℤ = {z. ∃Z. z = hypint_of_int Z}"
by (auto simp add: Ints_def)

lemma HIntInfinite_hypint_of_hypnat_iff:
  "(hypint_of_hypnat n ∈ HIntInfinite) = (n ∈ HNatInfinite)"
proof 
  assume "hypint_of_hypnat n ∈ HIntInfinite" 
  then show "n ∈ HNatInfinite"
    using HNatInfinite_not_Nats_iff SHNat_eq hypint_of_nat_less_abs_HIntInfinite by force
next
  assume "n ∈ HNatInfinite"
  then have "∀N. n ≠ hypnat_of_nat N"
    using star_of_neq_HNatInfinite by blast
  then show "hypint_of_hypnat n ∈ HIntInfinite"
    by (metis Ifun_star_of Ints_cases Ints_not_HIntInfinite_iff hypnat_def 
        hypnat_hypint of_int_eq_star_of starfun_def)
qed

lemma two_hyperpow_ge_one [simp]: "(1::hypint)  ≤ 2 pow n"
  by (simp add: hyperpow_gt_zero hypint_one_le_iff_zero_less)

subsection‹Embedding of hypertintegers in hyperreals›

abbreviation
  hypreal_of_hypint :: "hypint ⇒ hypreal" where
  "hypreal_of_hypint ≡ of_hypint"

lemma of_hypint_numeral [simp]: "of_hypint (numeral v) = numeral v"
by transfer simp

lemma real_of_int_le_real_of_nat_iff: "(real_of_int a ≤ real_of_nat b) = (a ≤ int b)"
proof 
  assume "real_of_int a ≤ real b" then show "a ≤ int b"
    by auto 
next
  assume "a ≤ int b" then show "real_of_int a ≤ real b"
    by linarith 
qed

lemma minus_real_of_int_le_real_of_nat_iff: "(- real_of_int a ≤ real_of_nat b) = (- a ≤ int b)"
  by linarith

lemma hypreal_of_hypint_le_hypreal_of_hypnat_iff:
      "⋀a b.(hypreal_of_hypint a ≤ of_hypnat b) = (a ≤ of_hypnat b)"
by transfer (auto simp add: real_of_int_le_real_of_nat_iff)

lemma minus_hypreal_of_hypint_le_hypreal_of_hypnat_iff:
      "⋀a b.(- hypreal_of_hypint a ≤ hypreal_of_hypnat b) = (- a ≤ of_hypnat b)"
by transfer (auto simp add: minus_real_of_int_le_real_of_nat_iff)

lemma hnorm_of_hypint [simp]:  
   "⋀z. hnorm (of_hypint z::'a::{real_normed_algebra_1, linordered_idom} star) = abs(of_hypint z)"
  by transfer simp

lemma of_hypnat_hypnat [simp]: "⋀z. 0 ≤ z ⟹ of_hypnat(hypnat z) = of_hypint z"
  by transfer simp

(* Move to NSA.thy if HyperInt is moved before NSA.thy *)
lemma HInfinite_def3: "HInfinite = {x. ∀z ∈ Ints. hypreal_of_hypint z < hnorm x}"
proof (auto simp add: HInfinite_def2)
  fix x::"'a :: real_normed_vector star" and z::"int star"
  assume less_hnorm: "∀n∈ℕ. hypreal_of_hypnat n < hnorm x" and z: "z ∈ ℤ"
  then obtain z' where "z = of_int z'"
    using Ints_cases by blast
  moreover have  "∀n. hypreal_of_nat n < hnorm x"
    using less_hnorm of_nat_in_Nats by fastforce
  moreover have "of_int z' < hnorm x" using less_hnorm
    by (metis calculation(2) hnorm_ge_zero less_le_trans nonneg_int_cases not_le 
        of_int_less_0_iff of_int_of_nat_eq)
  ultimately show "hypreal_of_hypint z < hnorm x"
    by simp
next
  fix x::"'a :: real_normed_vector star" and n::"nat star"
  assume less_hnorm: "∀z∈ℤ. hypreal_of_hypint z < hnorm x" and n: "n ∈ ℕ"
  then have "hypint_of_hypnat n ∈ ℤ"
    by (metis Nats_cases hypint_of_hypnat_hypint_of_nat_eq hypint_of_int_mem_Ints star_of_nat_def)
  then have "hypreal_of_hypint (hypint_of_hypnat n) < hnorm x"
    using  less_hnorm by blast
  then show "hypreal_of_hypnat n < hnorm x"
    by simp
qed

lemma HInfinite_of_hypint_HNatInfinite_hypnat:
  "⟦ (of_hypint x :: 'a::{real_normed_algebra_1,linordered_idom} star) ∈ HInfinite; x > 0 ⟧ 
       ⟹ hypnat x ∈ HNatInfinite"
by (rule nonneg_eq_hypint [of x], auto simp add: HNatInfinite_of_hypnat_HInfinite_iff)

lemma HNatInfinite_hypnat_HInfinite_of_hypint:
  "hypnat x ∈ HNatInfinite 
      ⟹ (of_hypint x :: 'a::{real_normed_algebra_1,linordered_idom} star) ∈ HInfinite"
  by (metis HNatInfinite_of_hypnat_HInfinite_iff hypnat_eq_iff2 of_hypint_of_hypnat 
      zero_not_mem_HNatInfinite)

end