Theory NSA

(*  Title:      HOL/Nonstandard_Analysis/NSA.thy
    Author:     Jacques D. Fleuriot, University of Cambridge
    Author:     Lawrence C Paulson, University of Cambridge
*)

section Infinite Numbers, Infinitesimals, Infinitely Close Relation

theory NSA
  imports HyperDef "HOL-Library.Lub_Glb" 
begin

definition hnorm :: "'a::real_normed_vector star  real star"
  where [transfer_unfold]: "hnorm = *f* norm"

definition Infinitesimal  :: "('a::real_normed_vector) star set"
  where "Infinitesimal = {x. r  Reals. 0 < r  hnorm x < r}"

definition HFinite :: "('a::real_normed_vector) star set"
  where "HFinite = {x. r  Reals. hnorm x < r}"

definition HInfinite :: "('a::real_normed_vector) star set"
  where "HInfinite = {x. r  Reals. r < hnorm x}"

definition approx :: "'a::real_normed_vector star  'a star  bool"  (infixl "" 50)
  where "x  y  x - y  Infinitesimal"
    ― ‹the ``infinitely close'' relation

definition st :: "hypreal  hypreal"
  where "st = (λx. SOME r. x  HFinite  r    r  x)"
    ― ‹the standard part of a hyperreal

definition monad :: "'a::real_normed_vector star  'a star set"
  where "monad x = {y. x  y}"

definition galaxy :: "'a::real_normed_vector star  'a star set"
  where "galaxy x = {y. (x + -y)  HFinite}"

lemma SReal_def: "  {x. r. x = hypreal_of_real r}"
  by (simp add: Reals_def image_def)


subsection Nonstandard Extension of the Norm Function

definition scaleHR :: "real star  'a star  'a::real_normed_vector star"
  where [transfer_unfold]: "scaleHR = starfun2 scaleR"

lemma Standard_hnorm [simp]: "x  Standard  hnorm x  Standard"
  by (simp add: hnorm_def)

lemma star_of_norm [simp]: "star_of (norm x) = hnorm (star_of x)"
  by transfer (rule refl)

lemma hnorm_ge_zero [simp]: "x::'a::real_normed_vector star. 0  hnorm x"
  by transfer (rule norm_ge_zero)

lemma hnorm_eq_zero [simp]: "x::'a::real_normed_vector star. hnorm x = 0  x = 0"
  by transfer (rule norm_eq_zero)

lemma hnorm_triangle_ineq: "x y::'a::real_normed_vector star. hnorm (x + y)  hnorm x + hnorm y"
  by transfer (rule norm_triangle_ineq)

lemma hnorm_triangle_ineq3: "x y::'a::real_normed_vector star. ¦hnorm x - hnorm y¦  hnorm (x - y)"
  by transfer (rule norm_triangle_ineq3)

lemma hnorm_scaleR: "x::'a::real_normed_vector star. hnorm (a *R x) = ¦star_of a¦ * hnorm x"
  by transfer (rule norm_scaleR)

lemma hnorm_scaleHR: "a (x::'a::real_normed_vector star). hnorm (scaleHR a x) = ¦a¦ * hnorm x"
  by transfer (rule norm_scaleR)

lemma hnorm_mult_ineq: "x y::'a::real_normed_algebra star. hnorm (x * y)  hnorm x * hnorm y"
  by transfer (rule norm_mult_ineq)

lemma hnorm_mult: "x y::'a::real_normed_div_algebra star. hnorm (x * y) = hnorm x * hnorm y"
  by transfer (rule norm_mult)

lemma hnorm_hyperpow: "(x::'a::{real_normed_div_algebra} star) n. hnorm (x pow n) = hnorm x pow n"
  by transfer (rule norm_power)

lemma hnorm_one [simp]: "hnorm (1::'a::real_normed_div_algebra star) = 1"
  by transfer (rule norm_one)

lemma hnorm_zero [simp]: "hnorm (0::'a::real_normed_vector star) = 0"
  by transfer (rule norm_zero)

lemma zero_less_hnorm_iff [simp]: "x::'a::real_normed_vector star. 0 < hnorm x  x  0"
  by transfer (rule zero_less_norm_iff)

lemma hnorm_minus_cancel [simp]: "x::'a::real_normed_vector star. hnorm (- x) = hnorm x"
  by transfer (rule norm_minus_cancel)

lemma hnorm_minus_commute: "a b::'a::real_normed_vector star. hnorm (a - b) = hnorm (b - a)"
  by transfer (rule norm_minus_commute)

lemma hnorm_triangle_ineq2: "a b::'a::real_normed_vector star. hnorm a - hnorm b  hnorm (a - b)"
  by transfer (rule norm_triangle_ineq2)

lemma hnorm_triangle_ineq4: "a b::'a::real_normed_vector star. hnorm (a - b)  hnorm a + hnorm b"
  by transfer (rule norm_triangle_ineq4)

lemma abs_hnorm_cancel [simp]: "a::'a::real_normed_vector star. ¦hnorm a¦ = hnorm a"
  by transfer (rule abs_norm_cancel)

lemma hnorm_of_hypreal [simp]: "r. hnorm (of_hypreal r::'a::real_normed_algebra_1 star) = ¦r¦"
  by transfer (rule norm_of_real)

lemma nonzero_hnorm_inverse:
  "a::'a::real_normed_div_algebra star. a  0  hnorm (inverse a) = inverse (hnorm a)"
  by transfer (rule nonzero_norm_inverse)

lemma hnorm_inverse:
  "a::'a::{real_normed_div_algebra, division_ring} star. hnorm (inverse a) = inverse (hnorm a)"
  by transfer (rule norm_inverse)

lemma hnorm_divide: "a b::'a::{real_normed_field, field} star. hnorm (a / b) = hnorm a / hnorm b"
  by transfer (rule norm_divide)

lemma hypreal_hnorm_def [simp]: "r::hypreal. hnorm r = ¦r¦"
  by transfer (rule real_norm_def)

lemma hnorm_add_less:
  "(x::'a::real_normed_vector star) y r s. hnorm x < r  hnorm y < s  hnorm (x + y) < r + s"
  by transfer (rule norm_add_less)

lemma hnorm_mult_less:
  "(x::'a::real_normed_algebra star) y r s. hnorm x < r  hnorm y < s  hnorm (x * y) < r * s"
  by transfer (rule norm_mult_less)

lemma hnorm_scaleHR_less: "¦x¦ < r  hnorm y < s  hnorm (scaleHR x y) < r * s"
 by (simp only: hnorm_scaleHR) (simp add: mult_strict_mono')


subsection Closure Laws for the Standard Reals

lemma Reals_add_cancel: "x + y    y    x  "
  by (drule (1) Reals_diff) simp

lemma SReal_hrabs: "x    ¦x¦  "
  for x :: hypreal
  by (simp add: Reals_eq_Standard)

lemma SReal_hypreal_of_real [simp]: "hypreal_of_real x  "
  by (simp add: Reals_eq_Standard)

lemma SReal_divide_numeral: "r    r / (numeral w::hypreal)  "
  by simp

text ε› is not in Reals because it is an infinitesimal
lemma SReal_epsilon_not_mem: "ε  "
  by (auto simp: SReal_def hypreal_of_real_not_eq_epsilon [symmetric])

lemma SReal_omega_not_mem: "ω  "
  by (auto simp: SReal_def hypreal_of_real_not_eq_omega [symmetric])

lemma SReal_UNIV_real: "{x. hypreal_of_real x  } = (UNIV::real set)"
  by simp

lemma SReal_iff: "x    (y. x = hypreal_of_real y)"
  by (simp add: SReal_def)

lemma hypreal_of_real_image: "hypreal_of_real `(UNIV::real set) = "
  by (simp add: Reals_eq_Standard Standard_def)

lemma inv_hypreal_of_real_image: "inv hypreal_of_real `  = UNIV"
  by (simp add: Reals_eq_Standard Standard_def inj_star_of)

lemma SReal_dense: "x    y    x < y  r  Reals. x < r  r < y"
  for x y :: hypreal
  using dense by (fastforce simp add: SReal_def)


subsection Set of Finite Elements is a Subring of the Extended Reals

lemma HFinite_add: "x  HFinite  y  HFinite  x + y  HFinite"
  unfolding HFinite_def by (blast intro!: Reals_add hnorm_add_less)

lemma HFinite_mult: "x  HFinite  y  HFinite  x * y  HFinite"
  for x y :: "'a::real_normed_algebra star"
  unfolding HFinite_def by (blast intro!: Reals_mult hnorm_mult_less)

lemma HFinite_scaleHR: "x  HFinite  y  HFinite  scaleHR x y  HFinite"
  by (auto simp: HFinite_def intro!: Reals_mult hnorm_scaleHR_less)

lemma HFinite_minus_iff: "- x  HFinite  x  HFinite"
  by (simp add: HFinite_def)

lemma HFinite_star_of [simp]: "star_of x  HFinite"
  by (simp add: HFinite_def) (metis SReal_hypreal_of_real gt_ex star_of_less star_of_norm)

lemma SReal_subset_HFinite: "(::hypreal set)  HFinite"
  by (auto simp add: SReal_def)

lemma HFiniteD: "x  HFinite  t  Reals. hnorm x < t"
  by (simp add: HFinite_def)

lemma HFinite_hrabs_iff [iff]: "¦x¦  HFinite  x  HFinite"
  for x :: hypreal
  by (simp add: HFinite_def)

lemma HFinite_hnorm_iff [iff]: "hnorm x  HFinite  x  HFinite"
  for x :: hypreal
  by (simp add: HFinite_def)

lemma HFinite_numeral [simp]: "numeral w  HFinite"
  unfolding star_numeral_def by (rule HFinite_star_of)

text As always with numerals, 0› and 1› are special cases.

lemma HFinite_0 [simp]: "0  HFinite"
  unfolding star_zero_def by (rule HFinite_star_of)

lemma HFinite_1 [simp]: "1  HFinite"
  unfolding star_one_def by (rule HFinite_star_of)

lemma hrealpow_HFinite: "x  HFinite  x ^ n  HFinite"
  for x :: "'a::{real_normed_algebra,monoid_mult} star"
  by (induct n) (auto intro: HFinite_mult)

lemma HFinite_bounded: 
  fixes x y :: hypreal
  assumes "x  HFinite" and y: "y  x" "0  y" shows "y  HFinite"
proof (cases "x  0")
  case True
  then have "y = 0"
    using y by auto
  then show ?thesis
    by simp
next
  case False
  then show ?thesis
    using assms le_less_trans by (auto simp: HFinite_def)
qed


subsection Set of Infinitesimals is a Subring of the Hyperreals

lemma InfinitesimalI: "(r. r    0 < r  hnorm x < r)  x  Infinitesimal"
  by (simp add: Infinitesimal_def)

lemma InfinitesimalD: "x  Infinitesimal  r  Reals. 0 < r  hnorm x < r"
  by (simp add: Infinitesimal_def)

lemma InfinitesimalI2: "(r. 0 < r  hnorm x < star_of r)  x  Infinitesimal"
  by (auto simp add: Infinitesimal_def SReal_def)

lemma InfinitesimalD2: "x  Infinitesimal  0 < r  hnorm x < star_of r"
  by (auto simp add: Infinitesimal_def SReal_def)

lemma Infinitesimal_zero [iff]: "0  Infinitesimal"
  by (simp add: Infinitesimal_def)

lemma Infinitesimal_add:
  assumes "x  Infinitesimal" "y  Infinitesimal"
  shows "x + y  Infinitesimal"
proof (rule InfinitesimalI)
  show "hnorm (x + y) < r"
    if "r  " and "0 < r" for r :: "real star"
  proof -
    have "hnorm x < r/2" "hnorm y < r/2"
      using InfinitesimalD SReal_divide_numeral assms half_gt_zero that by blast+
    then show ?thesis
      using hnorm_add_less by fastforce
  qed
qed

lemma Infinitesimal_minus_iff [simp]: "- x  Infinitesimal  x  Infinitesimal"
  by (simp add: Infinitesimal_def)

lemma Infinitesimal_hnorm_iff: "hnorm x  Infinitesimal  x  Infinitesimal"
  by (simp add: Infinitesimal_def)

lemma Infinitesimal_hrabs_iff [iff]: "¦x¦  Infinitesimal  x  Infinitesimal"
  for x :: hypreal
  by (simp add: abs_if)

lemma Infinitesimal_of_hypreal_iff [simp]:
  "(of_hypreal x::'a::real_normed_algebra_1 star)  Infinitesimal  x  Infinitesimal"
  by (subst Infinitesimal_hnorm_iff [symmetric]) simp

lemma Infinitesimal_diff: "x  Infinitesimal  y  Infinitesimal  x - y  Infinitesimal"
  using Infinitesimal_add [of x "- y"] by simp

lemma Infinitesimal_mult: 
  fixes x y :: "'a::real_normed_algebra star"
  assumes "x  Infinitesimal" "y  Infinitesimal"
  shows "x * y  Infinitesimal"
  proof (rule InfinitesimalI)
  show "hnorm (x * y) < r"
    if "r  " and "0 < r" for r :: "real star"
  proof -
    have "hnorm x < 1" "hnorm y < r"
      using assms that  by (auto simp add: InfinitesimalD)
    then show ?thesis
      using hnorm_mult_less by fastforce
  qed
qed

lemma Infinitesimal_HFinite_mult:
  fixes x y :: "'a::real_normed_algebra star"
  assumes "x  Infinitesimal" "y  HFinite"
  shows "x * y  Infinitesimal"
proof (rule InfinitesimalI)
  obtain t where "hnorm y < t" "t  Reals"
    using HFiniteD y  HFinite by blast
  then have "t > 0"
    using hnorm_ge_zero le_less_trans by blast
  show "hnorm (x * y) < r"
    if "r  " and "0 < r" for r :: "real star"
  proof -
    have "hnorm x < r/t"
      by (meson InfinitesimalD Reals_divide hnorm y < t t   assms(1) divide_pos_pos hnorm_ge_zero le_less_trans that) 
    then have "hnorm (x * y) < (r / t) * t"
      using hnorm y < t hnorm_mult_less by blast
    then show ?thesis
      using 0 < t by auto
  qed
qed

lemma Infinitesimal_HFinite_scaleHR:
  assumes "x  Infinitesimal" "y  HFinite"
  shows "scaleHR x y  Infinitesimal"
proof (rule InfinitesimalI)
  obtain t where "hnorm y < t" "t  Reals"
    using HFiniteD y  HFinite by blast
  then have "t > 0"
    using hnorm_ge_zero le_less_trans by blast
  show "hnorm (scaleHR x y) < r"
    if "r  " and "0 < r" for r :: "real star"
  proof -
    have "¦x¦ * hnorm y < (r / t) * t"
      by (metis InfinitesimalD Reals_divide 0 < t hnorm y < t t   assms(1) divide_pos_pos hnorm_ge_zero hypreal_hnorm_def mult_strict_mono' that)
    then show ?thesis
      by (simp add: 0 < t hnorm_scaleHR less_imp_not_eq2)
  qed
qed

lemma Infinitesimal_HFinite_mult2:
  fixes x y :: "'a::real_normed_algebra star"
  assumes "x  Infinitesimal" "y  HFinite"
  shows  "y * x  Infinitesimal"
proof (rule InfinitesimalI)
  obtain t where "hnorm y < t" "t  Reals"
    using HFiniteD y  HFinite by blast
  then have "t > 0"
    using hnorm_ge_zero le_less_trans by blast
  show "hnorm (y * x) < r"
    if "r  " and "0 < r" for r :: "real star"
  proof -
    have "hnorm x < r/t"
      by (meson InfinitesimalD Reals_divide hnorm y < t t   assms(1) divide_pos_pos hnorm_ge_zero le_less_trans that) 
    then have "hnorm (y * x) < t * (r / t)"
      using hnorm y < t hnorm_mult_less by blast
    then show ?thesis
      using 0 < t by auto
  qed
qed

lemma Infinitesimal_scaleR2: 
  assumes "x  Infinitesimal" shows "a *R x  Infinitesimal"
    by (metis HFinite_star_of Infinitesimal_HFinite_mult2 Infinitesimal_hnorm_iff assms hnorm_scaleR hypreal_hnorm_def star_of_norm)

lemma Compl_HFinite: "- HFinite = HInfinite"
  proof -
  have "r < hnorm x" if *: "s. s    s  hnorm x" and "r  "
    for x :: "'a star" and r :: hypreal
    using * [of "r+1"] r   by auto
  then show ?thesis
    by (auto simp add: HInfinite_def HFinite_def linorder_not_less)
qed

lemma HInfinite_inverse_Infinitesimal:
  "x  HInfinite  inverse x  Infinitesimal"
  for x :: "'a::real_normed_div_algebra star"
  by (simp add: HInfinite_def InfinitesimalI hnorm_inverse inverse_less_imp_less)

lemma inverse_Infinitesimal_iff_HInfinite:
  "x  0  inverse x  Infinitesimal  x  HInfinite"
  for x :: "'a::real_normed_div_algebra star"
  by (metis Compl_HFinite Compl_iff HInfinite_inverse_Infinitesimal InfinitesimalD Infinitesimal_HFinite_mult Reals_1 hnorm_one left_inverse less_irrefl zero_less_one)

lemma HInfiniteI: "(r. r    r < hnorm x)  x  HInfinite"
  by (simp add: HInfinite_def)

lemma HInfiniteD: "x  HInfinite  r    r < hnorm x"
  by (simp add: HInfinite_def)

lemma HInfinite_mult: 
  fixes x y :: "'a::real_normed_div_algebra star"
  assumes "x  HInfinite" "y  HInfinite" shows "x * y  HInfinite"
proof (rule HInfiniteI, simp only: hnorm_mult)
  have "x  0"
    using Compl_HFinite HFinite_0 assms by blast
  show "r < hnorm x * hnorm y"
    if "r  " for r :: "real star"
  proof -
    have "r = r * 1"
      by simp
    also have " < hnorm x * hnorm y"
      by (meson HInfiniteD Reals_1 x  0 assms le_numeral_extra(1) mult_strict_mono that zero_less_hnorm_iff)
    finally show ?thesis .
  qed
qed

lemma hypreal_add_zero_less_le_mono: "r < x  0  y  r < x + y"
  for r x y :: hypreal
  by simp

lemma HInfinite_add_ge_zero: "x  HInfinite  0  y  0  x  x + y  HInfinite"
  for x y :: hypreal
  by (auto simp: abs_if add.commute HInfinite_def)

lemma HInfinite_add_ge_zero2: "x  HInfinite  0  y  0  x  y + x  HInfinite"
  for x y :: hypreal
  by (auto intro!: HInfinite_add_ge_zero simp add: add.commute)

lemma HInfinite_add_gt_zero: "x  HInfinite  0 < y  0 < x  x + y  HInfinite"
  for x y :: hypreal
  by (blast intro: HInfinite_add_ge_zero order_less_imp_le)

lemma HInfinite_minus_iff: "- x  HInfinite  x  HInfinite"
  by (simp add: HInfinite_def)

lemma HInfinite_add_le_zero: "x  HInfinite  y  0  x  0  x + y  HInfinite"
  for x y :: hypreal
  by (metis (no_types, lifting) HInfinite_add_ge_zero2 HInfinite_minus_iff add.inverse_distrib_swap neg_0_le_iff_le)

lemma HInfinite_add_lt_zero: "x  HInfinite  y < 0  x < 0  x + y  HInfinite"
  for x y :: hypreal
  by (blast intro: HInfinite_add_le_zero order_less_imp_le)

lemma not_Infinitesimal_not_zero: "x  Infinitesimal  x  0"
  by auto

lemma HFinite_diff_Infinitesimal_hrabs:
  "x  HFinite - Infinitesimal  ¦x¦  HFinite - Infinitesimal"
  for x :: hypreal
  by blast

lemma hnorm_le_Infinitesimal: "e  Infinitesimal  hnorm x  e  x  Infinitesimal"
  by (auto simp: Infinitesimal_def abs_less_iff)

lemma hnorm_less_Infinitesimal: "e  Infinitesimal  hnorm x < e  x  Infinitesimal"
  by (erule hnorm_le_Infinitesimal, erule order_less_imp_le)

lemma hrabs_le_Infinitesimal: "e  Infinitesimal  ¦x¦  e  x  Infinitesimal"
  for x :: hypreal
  by (erule hnorm_le_Infinitesimal) simp

lemma hrabs_less_Infinitesimal: "e  Infinitesimal  ¦x¦ < e  x  Infinitesimal"
  for x :: hypreal
  by (erule hnorm_less_Infinitesimal) simp

lemma Infinitesimal_interval:
  "e  Infinitesimal  e'  Infinitesimal  e' < x  x < e  x  Infinitesimal"
  for x :: hypreal
  by (auto simp add: Infinitesimal_def abs_less_iff)

lemma Infinitesimal_interval2:
  "e  Infinitesimal  e'  Infinitesimal  e'  x  x  e  x  Infinitesimal"
  for x :: hypreal
  by (auto intro: Infinitesimal_interval simp add: order_le_less)

lemma lemma_Infinitesimal_hyperpow: "x  Infinitesimal  0 < N  ¦x pow N¦  ¦x¦"
  for x :: hypreal
  apply (clarsimp simp: Infinitesimal_def)
  by (metis Reals_1 abs_ge_zero hyperpow_Suc_le_self2 hyperpow_hrabs hypnat_gt_zero_iff2 zero_less_one)

lemma Infinitesimal_hyperpow: "x  Infinitesimal  0 < N  x pow N  Infinitesimal"
  for x :: hypreal
  using hrabs_le_Infinitesimal lemma_Infinitesimal_hyperpow by blast

lemma hrealpow_hyperpow_Infinitesimal_iff:
  "(x ^ n  Infinitesimal)  x pow (hypnat_of_nat n)  Infinitesimal"
  by (simp only: hyperpow_hypnat_of_nat)

lemma Infinitesimal_hrealpow: "x  Infinitesimal  0 < n  x ^ n  Infinitesimal"
  for x :: hypreal
  by (simp add: hrealpow_hyperpow_Infinitesimal_iff Infinitesimal_hyperpow)

lemma not_Infinitesimal_mult:
  "x  Infinitesimal  y  Infinitesimal  x * y  Infinitesimal"
  for x y :: "'a::real_normed_div_algebra star"
  by (metis (no_types, lifting) inverse_Infinitesimal_iff_HInfinite ComplI Compl_HFinite Infinitesimal_HFinite_mult divide_inverse eq_divide_imp inverse_inverse_eq mult_zero_right)

lemma Infinitesimal_mult_disj: "x * y  Infinitesimal  x  Infinitesimal  y  Infinitesimal"
  for x y :: "'a::real_normed_div_algebra star"
  using not_Infinitesimal_mult by blast

lemma HFinite_Infinitesimal_not_zero: "x  HFinite-Infinitesimal  x  0"
  by blast

lemma HFinite_Infinitesimal_diff_mult:
  "x  HFinite - Infinitesimal  y  HFinite - Infinitesimal  x * y  HFinite - Infinitesimal"
  for x y :: "'a::real_normed_div_algebra star"
  by (simp add: HFinite_mult not_Infinitesimal_mult)

lemma Infinitesimal_subset_HFinite: "Infinitesimal  HFinite"
  using HFinite_def InfinitesimalD Reals_1 zero_less_one by blast

lemma Infinitesimal_star_of_mult: "x  Infinitesimal  x * star_of r  Infinitesimal"
  for x :: "'a::real_normed_algebra star"
  by (erule HFinite_star_of [THEN [2] Infinitesimal_HFinite_mult])

lemma Infinitesimal_star_of_mult2: "x  Infinitesimal  star_of r * x  Infinitesimal"
  for x :: "'a::real_normed_algebra star"
  by (erule HFinite_star_of [THEN [2] Infinitesimal_HFinite_mult2])


subsection The Infinitely Close Relation

lemma mem_infmal_iff: "x  Infinitesimal  x  0"
  by (simp add: Infinitesimal_def approx_def)

lemma approx_minus_iff: "x  y  x - y  0"
  by (simp add: approx_def)

lemma approx_minus_iff2: "x  y  - y + x  0"
  by (simp add: approx_def add.commute)

lemma approx_refl [iff]: "x  x"
  by (simp add: approx_def Infinitesimal_def)

lemma approx_sym: "x  y  y  x"
  by (metis Infinitesimal_minus_iff approx_def minus_diff_eq)

lemma approx_trans:
  assumes "x  y" "y  z" shows "x  z"
proof -
  have "x - y  Infinitesimal" "z - y  Infinitesimal"
    using assms approx_def approx_sym by auto
  then have "x - z  Infinitesimal"
    using Infinitesimal_diff by force
  then show ?thesis
    by (simp add: approx_def)
qed

lemma approx_trans2: "r  x  s  x  r  s"
  by (blast intro: approx_sym approx_trans)

lemma approx_trans3: "x  r  x  s  r  s"
  by (blast intro: approx_sym approx_trans)

lemma approx_reorient: "x  y  y  x"
  by (blast intro: approx_sym)

text Reorientation simplification procedure: reorients (polymorphic)
  0 = x›, 1 = x›, nnn = x› provided x› isn't 0›, 1› or a numeral.
simproc_setup approx_reorient_simproc
  ("0  x" | "1  y" | "numeral w  z" | "- 1  y" | "- numeral w  r") =

  let val rule = @{thm approx_reorient} RS eq_reflection
      fun proc phi ss ct =
        case Thm.term_of ct of
          _ $ t $ u => if can HOLogic.dest_number u then NONE
            else if can HOLogic.dest_number t then SOME rule else NONE
        | _ => NONE
  in proc end


lemma Infinitesimal_approx_minus: "x - y  Infinitesimal  x  y"
  by (simp add: approx_minus_iff [symmetric] mem_infmal_iff)

lemma approx_monad_iff: "x  y  monad x = monad y"
  apply (simp add: monad_def set_eq_iff)
  using approx_reorient approx_trans by blast

lemma Infinitesimal_approx: "x  Infinitesimal  y  Infinitesimal  x  y"
  by (simp add: Infinitesimal_diff approx_def)

lemma approx_add: "a  b  c  d  a + c  b + d"
proof (unfold approx_def)
  assume inf: "a - b  Infinitesimal" "c - d  Infinitesimal"
  have "a + c - (b + d) = (a - b) + (c - d)" by simp
  also have "...  Infinitesimal"
    using inf by (rule Infinitesimal_add)
  finally show "a + c - (b + d)  Infinitesimal" .
qed

lemma approx_minus: "a  b  - a  - b"
  by (metis approx_def approx_sym minus_diff_eq minus_diff_minus)

lemma approx_minus2: "- a  - b  a  b"
  by (auto dest: approx_minus)

lemma approx_minus_cancel [simp]: "- a  - b  a  b"
  by (blast intro: approx_minus approx_minus2)

lemma approx_add_minus: "a  b  c  d  a + - c  b + - d"
  by (blast intro!: approx_add approx_minus)

lemma approx_diff: "a  b  c  d  a - c  b - d"
  using approx_add [of a b "- c" "- d"] by simp

lemma approx_mult1: "a  b  c  HFinite  a * c  b * c"
  for a b c :: "'a::real_normed_algebra star"
  by (simp add: approx_def Infinitesimal_HFinite_mult left_diff_distrib [symmetric])

lemma approx_mult2: "a  b  c  HFinite  c * a  c * b"
  for a b c :: "'a::real_normed_algebra star"
  by (simp add: approx_def Infinitesimal_HFinite_mult2 right_diff_distrib [symmetric])

lemma approx_mult_subst: "u  v * x  x  y  v  HFinite  u  v * y"
  for u v x y :: "'a::real_normed_algebra star"
  by (blast intro: approx_mult2 approx_trans)

lemma approx_mult_subst2: "u  x * v  x  y  v  HFinite  u  y * v"
  for u v x y :: "'a::real_normed_algebra star"
  by (blast intro: approx_mult1 approx_trans)

lemma approx_mult_subst_star_of: "u  x * star_of v  x  y  u  y * star_of v"
  for u x y :: "'a::real_normed_algebra star"
  by (auto intro: approx_mult_subst2)

lemma approx_eq_imp: "a = b  a  b"
  by (simp add: approx_def)

lemma Infinitesimal_minus_approx: "x  Infinitesimal  - x  x"
  by (blast intro: Infinitesimal_minus_iff [THEN iffD2] mem_infmal_iff [THEN iffD1] approx_trans2)

lemma bex_Infinitesimal_iff: "(y  Infinitesimal. x - z = y)  x  z"
  by (simp add: approx_def)

lemma bex_Infinitesimal_iff2: "(y  Infinitesimal. x = z + y)  x  z"
  by (force simp add: bex_Infinitesimal_iff [symmetric])

lemma Infinitesimal_add_approx: "y  Infinitesimal  x + y = z  x  z"
  using approx_sym bex_Infinitesimal_iff2 by blast

lemma Infinitesimal_add_approx_self: "y  Infinitesimal  x  x + y"
  by (simp add: Infinitesimal_add_approx)

lemma Infinitesimal_add_approx_self2: "y  Infinitesimal  x  y + x"
  by (auto dest: Infinitesimal_add_approx_self simp add: add.commute)

lemma Infinitesimal_add_minus_approx_self: "y  Infinitesimal  x  x + - y"
  by (blast intro!: Infinitesimal_add_approx_self Infinitesimal_minus_iff [THEN iffD2])

lemma Infinitesimal_add_cancel: "y  Infinitesimal  x + y  z  x  z"
  using Infinitesimal_add_approx approx_trans by blast

lemma Infinitesimal_add_right_cancel: "y  Infinitesimal  x  z + y  x  z"
  by (metis Infinitesimal_add_approx_self approx_monad_iff)

lemma approx_add_left_cancel: "d + b  d + c  b  c"
  by (metis add_diff_cancel_left bex_Infinitesimal_iff)

lemma approx_add_right_cancel: "b + d  c + d  b  c"
  by (simp add: approx_def)

lemma approx_add_mono1: "b  c  d + b  d + c"
  by (simp add: approx_add)

lemma approx_add_mono2: "b  c  b + a  c + a"
  by (simp add: add.commute approx_add_mono1)

lemma approx_add_left_iff [simp]: "a + b  a + c  b  c"
  by (fast elim: approx_add_left_cancel approx_add_mono1)

lemma approx_add_right_iff [simp]: "b + a  c + a  b  c"
  by (simp add: add.commute)

lemma approx_HFinite: "x  HFinite  x  y  y  HFinite"
  by (metis HFinite_add Infinitesimal_subset_HFinite approx_sym subsetD bex_Infinitesimal_iff2)

lemma approx_star_of_HFinite: "x  star_of D  x  HFinite"
  by (rule approx_sym [THEN [2] approx_HFinite], auto)

lemma approx_mult_HFinite: "a  b  c  d  b  HFinite  d  HFinite  a * c  b * d"
  for a b c d :: "'a::real_normed_algebra star"
  by (meson approx_HFinite approx_mult2 approx_mult_subst2 approx_sym)

lemma scaleHR_left_diff_distrib: "a b x. scaleHR (a - b) x = scaleHR a x - scaleHR b x"
  by transfer (rule scaleR_left_diff_distrib)

lemma approx_scaleR1: "a  star_of b  c  HFinite  scaleHR a c  b *R c"
  unfolding approx_def
  by (metis Infinitesimal_HFinite_scaleHR scaleHR_def scaleHR_left_diff_distrib star_scaleR_def starfun2_star_of)

lemma approx_scaleR2: "a  b  c *R a  c *R b"
  by (simp add: approx_def Infinitesimal_scaleR2 scaleR_right_diff_distrib [symmetric])

lemma approx_scaleR_HFinite: "a  star_of b  c  d  d  HFinite  scaleHR a c  b *R d"
  by (meson approx_HFinite approx_scaleR1 approx_scaleR2 approx_sym approx_trans)

lemma approx_mult_star_of: "a  star_of b  c  star_of d  a * c  star_of b * star_of d"
  for a c :: "'a::real_normed_algebra star"
  by (blast intro!: approx_mult_HFinite approx_star_of_HFinite HFinite_star_of)

lemma approx_SReal_mult_cancel_zero:
  fixes a x :: hypreal
  assumes "a  " "a  0" "a * x  0" shows "x  0"
proof -
  have "inverse a  HFinite"
    using Reals_inverse SReal_subset_HFinite assms(1) by blast
  then show ?thesis
    using assms by (auto dest: approx_mult2 simp add: mult.assoc [symmetric])
qed

lemma approx_mult_SReal1: "a    x  0  x * a  0"
  for a x :: hypreal
  by (auto dest: SReal_subset_HFinite [THEN subsetD] approx_mult1)

lemma approx_mult_SReal2: "a    x  0  a * x  0"
  for a x :: hypreal
  by (auto dest: SReal_subset_HFinite [THEN subsetD] approx_mult2)

lemma approx_mult_SReal_zero_cancel_iff [simp]: "a    a  0  a * x  0  x  0"
  for a x :: hypreal
  by (blast intro: approx_SReal_mult_cancel_zero approx_mult_SReal2)

lemma approx_SReal_mult_cancel:
  fixes a w z :: hypreal
  assumes "a  " "a  0" "a * w  a * z" shows "w  z"
proof -
  have "inverse a  HFinite"
    using Reals_inverse SReal_subset_HFinite assms(1) by blast
  then show ?thesis
    using assms by (auto dest: approx_mult2 simp add: mult.assoc [symmetric])
qed

lemma approx_SReal_mult_cancel_iff1 [simp]: "a    a  0  a * w  a * z  w  z"
  for a w z :: hypreal
  by (meson SReal_subset_HFinite approx_SReal_mult_cancel approx_mult2 subsetD)

lemma approx_le_bound:
  fixes z :: hypreal
  assumes "z  f" " f  g" "g  z" shows "f  z"
proof -
  obtain y where "z  g + y" and "y  Infinitesimal" "f = g + y"
    using assms bex_Infinitesimal_iff2 by auto
  then have "z - g  Infinitesimal"
    using assms(3) hrabs_le_Infinitesimal by auto 
  then show ?thesis
    by (metis approx_def approx_trans2 assms(2))
qed

lemma approx_hnorm: "x  y  hnorm x  hnorm y"
  for x y :: "'a::real_normed_vector star"
proof (unfold approx_def)
  assume "x - y  Infinitesimal"
  then have "hnorm (x - y)  Infinitesimal"
    by (simp only: Infinitesimal_hnorm_iff)
  moreover have "(0::real star)  Infinitesimal"
    by (rule Infinitesimal_zero)
  moreover have "0  ¦hnorm x - hnorm y¦"
    by (rule abs_ge_zero)
  moreover have "¦hnorm x - hnorm y¦  hnorm (x - y)"
    by (rule hnorm_triangle_ineq3)
  ultimately have "¦hnorm x - hnorm y¦  Infinitesimal"
    by (rule Infinitesimal_interval2)
  then show "hnorm x - hnorm y  Infinitesimal"
    by (simp only: Infinitesimal_hrabs_iff)
qed


subsection Zero is the Only Infinitesimal that is also a Real

lemma Infinitesimal_less_SReal: "x    y  Infinitesimal  0 < x  y < x"
  for x y :: hypreal
  using InfinitesimalD by fastforce

lemma Infinitesimal_less_SReal2: "y  Infinitesimal  r  Reals. 0 < r  y < r"
  for y :: hypreal
  by (blast intro: Infinitesimal_less_SReal)

lemma SReal_not_Infinitesimal: "0 < y  y   ==> y  Infinitesimal"
  for y :: hypreal
  by (auto simp add: Infinitesimal_def abs_if)

lemma SReal_minus_not_Infinitesimal: "y < 0  y    y  Infinitesimal"
  for y :: hypreal
  using Infinitesimal_minus_iff Reals_minus SReal_not_Infinitesimal neg_0_less_iff_less by blast

lemma SReal_Int_Infinitesimal_zero: " Int Infinitesimal = {0::hypreal}"
  proof -
  have "x = 0" if "x  " "x  Infinitesimal" for x :: "real star"
    using that SReal_minus_not_Infinitesimal SReal_not_Infinitesimal not_less_iff_gr_or_eq by blast
  then show ?thesis
    by auto
qed

lemma SReal_Infinitesimal_zero: "x    x  Infinitesimal  x = 0"
  for x :: hypreal
  using SReal_Int_Infinitesimal_zero by blast

lemma SReal_HFinite_diff_Infinitesimal: "x    x  0  x  HFinite - Infinitesimal"
  for x :: hypreal
  by (auto dest: SReal_Infinitesimal_zero SReal_subset_HFinite [THEN subsetD])

lemma hypreal_of_real_HFinite_diff_Infinitesimal:
  "hypreal_of_real x  0  hypreal_of_real x  HFinite - Infinitesimal"
  by (rule SReal_HFinite_diff_Infinitesimal) auto

lemma star_of_Infinitesimal_iff_0 [iff]: "star_of x  Infinitesimal  x = 0"
proof
  show "x = 0" if "star_of x  Infinitesimal"
  proof -
    have "hnorm (star_n (λn. x))  Standard"
      by (metis Reals_eq_Standard SReal_iff star_of_def star_of_norm)
    then show ?thesis
      by (metis InfinitesimalD2 less_irrefl star_of_norm that zero_less_norm_iff)
  qed
qed auto

lemma star_of_HFinite_diff_Infinitesimal: "x  0  star_of x  HFinite - Infinitesimal"
  by simp

lemma numeral_not_Infinitesimal [simp]:
  "numeral w  (0::hypreal)  (numeral w :: hypreal)  Infinitesimal"
  by (fast dest: Reals_numeral [THEN SReal_Infinitesimal_zero])

text Again: 1› is a special case, but not 0› this time.
lemma one_not_Infinitesimal [simp]:
  "(1::'a::{real_normed_vector,zero_neq_one} star)  Infinitesimal"
  by (metis star_of_Infinitesimal_iff_0 star_one_def zero_neq_one)

lemma approx_SReal_not_zero: "y    x  y  y  0  x  0"
  for x y :: hypreal
  using SReal_Infinitesimal_zero approx_sym mem_infmal_iff by auto

lemma HFinite_diff_Infinitesimal_approx:
  "x  y  y  HFinite - Infinitesimal  x  HFinite - Infinitesimal"
  by (meson Diff_iff approx_HFinite approx_sym approx_trans3 mem_infmal_iff)

text The premise y ≠ 0› is essential; otherwise x / y = 0› and we lose the
  HFinite› premise.
lemma Infinitesimal_ratio:
  "y  0  y  Infinitesimal  x / y  HFinite  x  Infinitesimal"
  for x y :: "'a::{real_normed_div_algebra,field} star"
  using Infinitesimal_HFinite_mult by fastforce

lemma Infinitesimal_SReal_divide: "x  Infinitesimal  y    x / y  Infinitesimal"
  for x y :: hypreal
  by (metis HFinite_star_of Infinitesimal_HFinite_mult Reals_inverse SReal_iff divide_inverse)


section Standard Part Theorem

text 
  Every finite x ∈ R*› is infinitely close to a unique real number
  (i.e. a member of Reals›).



subsection Uniqueness: Two Infinitely Close Reals are Equal

lemma star_of_approx_iff [simp]: "star_of x  star_of y  x = y"
  by (metis approx_def right_minus_eq star_of_Infinitesimal_iff_0 star_of_simps(2))

lemma SReal_approx_iff: "x    y    x  y  x = y"
  for x y :: hypreal
  by (meson Reals_diff SReal_Infinitesimal_zero approx_def approx_refl right_minus_eq)

lemma numeral_approx_iff [simp]:
  "(numeral v  (numeral w :: 'a::{numeral,real_normed_vector} star)) = (numeral v = (numeral w :: 'a))"
  by (metis star_of_approx_iff star_of_numeral)

text And also for 0 ≈ #nn› and 1 ≈ #nn›, #nn ≈ 0› and #nn ≈ 1›.
lemma [simp]:
  "(numeral w  (0::'a::{numeral,real_normed_vector} star)) = (numeral w = (0::'a))"
  "((0::'a::{numeral,real_normed_vector} star)  numeral w) = (numeral w = (0::'a))"
  "(numeral w  (1::'b::{numeral,one,real_normed_vector} star)) = (numeral w = (1::'b))"
  "((1::'b::{numeral,one,real_normed_vector} star)  numeral w) = (numeral w = (1::'b))"
  "¬ (0  (1::'c::{zero_neq_one,real_normed_vector} star))"
  "¬ (1  (0::'c::{zero_neq_one,real_normed_vector} star))"
  unfolding star_numeral_def star_zero_def star_one_def star_of_approx_iff
  by (auto intro: sym)

lemma star_of_approx_numeral_iff [simp]: "star_of k  numeral w  k = numeral w"
  by (subst star_of_approx_iff [symmetric]) auto

lemma star_of_approx_zero_iff [simp]: "star_of k  0  k = 0"
  by (simp_all add: star_of_approx_iff [symmetric])

lemma star_of_approx_one_iff [simp]: "star_of k  1  k = 1"
  by (simp_all add: star_of_approx_iff [symmetric])

lemma approx_unique_real: "r    s    r  x  s  x  r = s"
  for r s :: hypreal
  by (blast intro: SReal_approx_iff [THEN iffD1] approx_trans2)


subsection Existence of Unique Real Infinitely Close

subsubsection Lifting of the Ub and Lub Properties

lemma hypreal_of_real_isUb_iff: "isUb  (hypreal_of_real ` Q) (hypreal_of_real Y) = isUb UNIV Q Y"
  for Q :: "real set" and Y :: real
  by (simp add: isUb_def setle_def)

lemma hypreal_of_real_isLub_iff:
  "isLub  (hypreal_of_real ` Q) (hypreal_of_real Y) = isLub (UNIV :: real set) Q Y"  (is "?lhs = ?rhs")
  for Q :: "real set" and Y :: real
proof 
  assume ?lhs
  then show ?rhs
    by (simp add: isLub_def leastP_def) (metis hypreal_of_real_isUb_iff mem_Collect_eq setge_def star_of_le)
next
  assume ?rhs
  then show ?lhs
  apply (simp add: isLub_def leastP_def hypreal_of_real_isUb_iff setge_def)
    by (metis SReal_iff hypreal_of_real_isUb_iff isUb_def star_of_le)
qed

lemma lemma_isUb_hypreal_of_real: "isUb  P Y  Yo. isUb  P (hypreal_of_real Yo)"
  by (auto simp add: SReal_iff isUb_def)

lemma lemma_isLub_hypreal_of_real: "isLub  P Y  Yo. isLub  P (hypreal_of_real Yo)"
  by (auto simp add: isLub_def leastP_def isUb_def SReal_iff)

lemma SReal_complete:
  fixes P :: "hypreal set"
  assumes "isUb  P Y" "P  " "P  {}"
    shows "t. isLub  P t"
proof -
  obtain Q where "P = hypreal_of_real ` Q"
    by (metis P   hypreal_of_real_image subset_imageE)
  then show ?thesis
    by (metis assms(1) P  {} equals0I hypreal_of_real_isLub_iff hypreal_of_real_isUb_iff image_empty lemma_isUb_hypreal_of_real reals_complete)
qed


text Lemmas about lubs.

lemma lemma_st_part_lub:
  fixes x :: hypreal
  assumes "x  HFinite"
  shows "t. isLub  {s. s    s < x} t"
proof -
  obtain t where t: "t  " "hnorm x < t"
    using HFiniteD assms by blast
  then have "isUb  {s. s    s < x} t"
    by (simp add: abs_less_iff isUbI le_less_linear less_imp_not_less setleI)
  moreover have "y. y    y < x"
    using t by (rule_tac x = "-t" in exI) (auto simp add: abs_less_iff)
  ultimately show ?thesis
    using SReal_complete by fastforce
qed

lemma hypreal_setle_less_trans: "S *<= x  x < y  S *<= y"
  for x y :: hypreal
  by (meson le_less_trans less_imp_le setle_def)

lemma hypreal_gt_isUb: "isUb R S x  x < y  y  R  isUb R S y"
  for x y :: hypreal
  using hypreal_setle_less_trans isUb_def by blast

lemma lemma_SReal_ub: "x    isUb  {s. s    s < x} x"
  for x :: hypreal
  by (auto intro: isUbI setleI order_less_imp_le)

lemma lemma_SReal_lub: 
  fixes x :: hypreal
  assumes "x  " shows "isLub  {s. s    s < x} x"
proof -
  have "x  y" if "isUb  {s  . s < x} y" for y
  proof -
    have "y  "
      using isUbD2a that by blast
    show ?thesis
    proof (cases x y rule: linorder_cases)
      case greater
      then obtain r where "y < r" "r < x"
        using dense by blast
      then show ?thesis
        using isUbD [OF that]
        by simp (meson SReal_dense y   assms greater not_le)
    qed auto
  qed
  with assms show ?thesis
    by (simp add: isLubI2 isUbI setgeI setleI)
qed

lemma lemma_st_part_major:
  fixes x r t :: hypreal
  assumes x: "x  HFinite" and r: "r  " "0 < r" and t: "isLub  {s. s    s < x} t"
  shows "¦x - t¦ < r"
proof -
  have "t  "
    using isLubD1a t by blast
  have lemma_st_part_gt_ub: "x < r  r    isUb  {s. s    s < x} r"
    for  r :: hypreal
    by (auto dest: order_less_trans intro: order_less_imp_le intro!: isUbI setleI)

  have "isUb  {s  . s < x} t"
    by (simp add: t isLub_isUb)
  then have "¬ r + t < x"
    by (metis (mono_tags, lifting) Reals_add t   add_le_same_cancel2 isUbD leD mem_Collect_eq r)
  then have "x - t  r"
    by simp
  moreover have "¬ x < t - r"
    using lemma_st_part_gt_ub isLub_le_isUb t   r t x by fastforce
  then have "- (x - t)  r"
    by linarith
  moreover have False if "x - t = r  - (x - t) = r"
  proof -
    have "x  "
      by (metis t   r   that Reals_add_cancel Reals_minus_iff add_uminus_conv_diff)
    then have "isLub  {s  . s < x} x"
      by (rule lemma_SReal_lub)
    then show False
      using r t that x isLub_unique by force
  qed
  ultimately show ?thesis
    using abs_less_iff dual_order.order_iff_strict by blast
qed

lemma lemma_st_part_major2:
  "x  HFinite  isLub  {s. s    s < x} t  r  Reals. 0 < r  ¦x - t¦ < r"
  for x t :: hypreal
  by (blast dest!: lemma_st_part_major)


textExistence of real and Standard Part Theorem.

lemma lemma_st_part_Ex: "x  HFinite  tReals. r  Reals. 0 < r  ¦x - t¦ < r"
  for x :: hypreal
  by (meson isLubD1a lemma_st_part_lub lemma_st_part_major2)

lemma st_part_Ex: "x  HFinite  tReals. x  t"
  for x :: hypreal
  by (metis InfinitesimalI approx_def hypreal_hnorm_def lemma_st_part_Ex)

text There is a unique real infinitely close.
lemma st_part_Ex1: "x  HFinite  ∃!t::hypreal. t    x  t"
  by (meson SReal_approx_iff approx_trans2 st_part_Ex)


subsection Finite, Infinite and Infinitesimal

lemma HFinite_Int_HInfinite_empty [simp]: "HFinite Int HInfinite = {}"
  using Compl_HFinite by blast

lemma HFinite_not_HInfinite:
  assumes x: "x  HFinite" shows "x  HInfinite"
  using Compl_HFinite x by blast

lemma not_HFinite_HInfinite: "x  HFinite  x  HInfinite"
  using Compl_HFinite by blast

lemma HInfinite_HFinite_disj: "x  HInfinite  x  HFinite"
  by (blast intro: not_HFinite_HInfinite)

lemma HInfinite_HFinite_iff: "x  HInfinite  x  HFinite"
  by (blast dest: HFinite_not_HInfinite not_HFinite_HInfinite)

lemma HFinite_HInfinite_iff: "x  HFinite  x  HInfinite"
  by (simp add: HInfinite_HFinite_iff)

lemma HInfinite_diff_HFinite_Infinitesimal_disj:
  "x  Infinitesimal  x  HInfinite  x  HFinite - Infinitesimal"
  by (fast intro: not_HFinite_HInfinite)

lemma HFinite_inverse: "x  HFinite  x  Infinitesimal  inverse x  HFinite"
  for x :: "'a::real_normed_div_algebra star"
  using HInfinite_inverse_Infinitesimal not_HFinite_HInfinite by force

lemma HFinite_inverse2: "x  HFinite - Infinitesimal  inverse x  HFinite"
  for x :: "'a::real_normed_div_algebra star"
  by (blast intro: HFinite_inverse)

text Stronger statement possible in fact.
lemma Infinitesimal_inverse_HFinite: "x  Infinitesimal  inverse x  HFinite"
  for x :: "'a::real_normed_div_algebra star"
  using HFinite_HInfinite_iff HInfinite_inverse_Infinitesimal by fastforce

lemma HFinite_not_Infinitesimal_inverse:
  "x  HFinite - Infinitesimal  inverse x  HFinite - Infinitesimal"
  for x :: "'a::real_normed_div_algebra star"
  using HFinite_Infinitesimal_not_zero HFinite_inverse2 Infinitesimal_HFinite_mult2 by fastforce

lemma approx_inverse: 
  fixes x y :: "'a::real_normed_div_algebra star"
  assumes "x  y" and y: "y  HFinite - Infinitesimal" shows "inverse x  inverse y"
proof -
  have x: "x  HFinite - Infinitesimal"
    using HFinite_diff_Infinitesimal_approx assms(1) y by blast
  with y HFinite_inverse2 have "inverse x  HFinite" "inverse y  HFinite"
    by blast+
  then have "inverse y * x  1"
    by (metis Diff_iff approx_mult2 assms(1) left_inverse not_Infinitesimal_not_zero y)
  then show ?thesis
    by (metis (no_types, lifting) DiffD2 HFinite_Infinitesimal_not_zero Infinitesimal_mult_disj x approx_def approx_sym left_diff_distrib left_inverse)
qed

(*Used for NSLIM_inverse, NSLIMSEQ_inverse*)
lemmas star_of_approx_inverse = star_of_HFinite_diff_Infinitesimal [THEN [2] approx_inverse]
lemmas hypreal_of_real_approx_inverse =  hypreal_of_real_HFinite_diff_Infinitesimal [THEN [2] approx_inverse]

lemma inverse_add_Infinitesimal_approx:
  "x  HFinite - Infinitesimal  h  Infinitesimal  inverse (x + h)  inverse x"
  for x h :: "'a::real_normed_div_algebra star"
  by (auto intro: approx_inverse approx_sym Infinitesimal_add_approx_self)

lemma inverse_add_Infinitesimal_approx2:
  "x  HFinite - Infinitesimal  h  Infinitesimal  inverse (h + x)  inverse x"
  for x h :: "'a::real_normed_div_algebra star"
  by (metis add.commute inverse_add_Infinitesimal_approx)

lemma inverse_add_Infinitesimal_approx_Infinitesimal:
  "x  HFinite - Infinitesimal  h  Infinitesimal  inverse (x + h) - inverse x  h"
  for x h :: "'a::real_normed_div_algebra star"
  by (meson Infinitesimal_approx bex_Infinitesimal_iff inverse_add_Infinitesimal_approx)

lemma Infinitesimal_square_iff: "x  Infinitesimal  x * x  Infinitesimal"
  for x :: "'a::real_normed_div_algebra star"
  using Infinitesimal_mult Infinitesimal_mult_disj by auto
declare Infinitesimal_square_iff [symmetric, simp]

lemma HFinite_square_iff [simp]: "x * x  HFinite  x  HFinite"
  for x :: "'a::real_normed_div_algebra star"
  using HFinite_HInfinite_iff HFinite_mult HInfinite_mult by blast

lemma HInfinite_square_iff [simp]: "x * x  HInfinite  x  HInfinite"
  for x :: "'a::real_normed_div_algebra star"
  by (auto simp add: HInfinite_HFinite_iff)

lemma approx_HFinite_mult_cancel: "a  HFinite - Infinitesimal  a * w  a * z  w  z"
  for a w z :: "'a::real_normed_div_algebra star"
  by (metis DiffD2 Infinitesimal_mult_disj bex_Infinitesimal_iff right_diff_distrib)

lemma approx_HFinite_mult_cancel_iff1: "a  HFinite - Infinitesimal  a * w  a * z  w  z"
  for a w z :: "'a::real_normed_div_algebra star"
  by (auto intro: approx_mult2 approx_HFinite_mult_cancel)

lemma HInfinite_HFinite_add_cancel: "x + y  HInfinite  y  HFinite  x  HInfinite"
  using HFinite_add HInfinite_HFinite_iff by blast

lemma HInfinite_HFinite_add: "x  HInfinite  y  HFinite  x + y  HInfinite"
  by (metis (no_types, opaque_lifting) HFinite_HInfinite_iff HFinite_add HFinite_minus_iff add.commute add_minus_cancel)

lemma HInfinite_ge_HInfinite: "x  HInfinite  x  y  0  x  y  HInfinite"
  for x y :: hypreal
  by (auto intro: HFinite_bounded simp add: HInfinite_HFinite_iff)

lemma Infinitesimal_inverse_HInfinite: "x  Infinitesimal  x  0  inverse x  HInfinite"
  for x :: "'a::real_normed_div_algebra star"
  by (metis Infinitesimal_HFinite_mult not_HFinite_HInfinite one_not_Infinitesimal right_inverse)

lemma HInfinite_HFinite_not_Infinitesimal_mult:
  "x  HInfinite  y  HFinite - Infinitesimal  x * y  HInfinite"
  for x y :: "'a::real_normed_div_algebra star"
  by (metis (no_types, opaque_lifting) HFinite_HInfinite_iff HFinite_Infinitesimal_not_zero HFinite_inverse2 HFinite_mult mult.assoc mult.right_neutral right_inverse)

lemma HInfinite_HFinite_not_Infinitesimal_mult2:
  "x  HInfinite  y  HFinite - Infinitesimal  y * x  HInfinite"
  for x y :: "'a::real_normed_div_algebra star"
  by (metis Diff_iff HInfinite_HFinite_iff HInfinite_inverse_Infinitesimal Infinitesimal_HFinite_mult2 divide_inverse mult_zero_right nonzero_eq_divide_eq)

lemma HInfinite_gt_SReal: "x  HInfinite  0 < x  y    y < x"
  for x y :: hypreal
  by (auto dest!: bspec simp add: HInfinite_def abs_if order_less_imp_le)

lemma HInfinite_gt_zero_gt_one: "x  HInfinite  0 < x  1 < x"
  for x :: hypreal
  by (auto intro: HInfinite_gt_SReal)

lemma not_HInfinite_one [simp]: "1  HInfinite"
  by (simp add: HInfinite_HFinite_iff)

lemma approx_hrabs_disj: "¦x¦  x  ¦x¦  -x"
  for x :: hypreal
  by (simp add: abs_if)


subsection Theorems about Monads

lemma monad_hrabs_Un_subset: "monad ¦x¦  monad x  monad (- x)"
  for x :: hypreal
  by (simp add: abs_if)

lemma Infinitesimal_monad_eq: "e  Infinitesimal  monad (x + e) = monad x"
  by (fast intro!: Infinitesimal_add_approx_self [THEN approx_sym] approx_monad_iff [THEN iffD1])

lemma mem_monad_iff: "u  monad x  - u  monad (- x)"
  by (simp add: monad_def)

lemma Infinitesimal_monad_zero_iff: "x  Infinitesimal  x  monad 0"
  by (auto intro: approx_sym simp add: monad_def mem_infmal_iff)

lemma monad_zero_minus_iff: "x  monad 0  - x  monad 0"
  by (simp add: Infinitesimal_monad_zero_iff [symmetric])

lemma monad_zero_hrabs_iff: "x  monad 0  ¦x¦  monad 0"
  for x :: hypreal
  using Infinitesimal_monad_zero_iff by blast

lemma mem_monad_self [simp]: "x  monad x"
  by (simp add: monad_def)


subsection Proof that termx  y implies term¦x¦  ¦y¦

lemma approx_subset_monad: "x  y  {x, y}  monad x"
  by (simp (no_asm)) (simp add: approx_monad_iff)

lemma approx_subset_monad2: "x  y  {x, y}  monad y"
  using approx_subset_monad approx_sym by auto

lemma mem_monad_approx: "u  monad x  x  u"
  by (simp add: monad_def)

lemma approx_mem_monad: "x  u  u  monad x"
  by (simp add: monad_def)

lemma approx_mem_monad2: "x  u  x  monad u"
  using approx_mem_monad approx_sym by blast

lemma approx_mem_monad_zero: "x  y  x  monad 0  y  monad 0"
  using approx_trans monad_def by blast

lemma Infinitesimal_approx_hrabs: "x  y  x  Infinitesimal  ¦x¦  ¦y¦"
  for x y :: hypreal
  using approx_hnorm by fastforce

lemma less_Infinitesimal_less: "0 < x  x  Infinitesimal  e  Infinitesimal  e < x"
  for x :: hypreal
  using Infinitesimal_interval less_linear by blast

lemma Ball_mem_monad_gt_zero: "0 < x  x  Infinitesimal  u  monad x  0 < u"
  for u x :: hypreal
  by (metis bex_Infinitesimal_iff2 less_Infinitesimal_less less_add_same_cancel2 mem_monad_approx)

lemma Ball_mem_monad_less_zero: "x < 0  x  Infinitesimal  u  monad x  u < 0"
  for u x :: hypreal
  by (metis Ball_mem_monad_gt_zero approx_monad_iff less_asym linorder_neqE_linordered_idom mem_infmal_iff mem_monad_approx mem_monad_self)

lemma lemma_approx_gt_zero: "0 < x  x  Infinitesimal  x  y  0 < y"
  for x y :: hypreal
  by (blast dest: Ball_mem_monad_gt_zero approx_subset_monad)

lemma lemma_approx_less_zero: "x < 0  x  Infinitesimal  x  y  y < 0"
  for x y :: hypreal
  by (blast dest: Ball_mem_monad_less_zero approx_subset_monad)

lemma approx_hrabs: "x  y  ¦x¦  ¦y¦"
  for x y :: hypreal
  by (drule approx_hnorm) simp

lemma approx_hrabs_zero_cancel: "¦x¦  0  x  0"
  for x :: hypreal
  using mem_infmal_iff by blast

lemma approx_hrabs_add_Infinitesimal: "e  Infinitesimal  ¦x¦  ¦x + e¦"
  for e x :: hypreal
  by (fast intro: approx_hrabs Infinitesimal_add_approx_self)

lemma approx_hrabs_add_minus_Infinitesimal: "e  Infinitesimal ==> ¦x¦  ¦x + -e¦"
  for e x :: hypreal
  by (fast intro: approx_hrabs Infinitesimal_add_minus_approx_self)

lemma hrabs_add_Infinitesimal_cancel:
  "e  Infinitesimal  e'  Infinitesimal  ¦x + e¦ = ¦y + e'¦  ¦x¦  ¦y¦"
  for e e' x y :: hypreal
  by (metis approx_hrabs_add_Infinitesimal approx_trans2)

lemma hrabs_add_minus_Infinitesimal_cancel:
  "e  Infinitesimal  e'  Infinitesimal  ¦x + -e¦ = ¦y + -e'¦  ¦x¦  ¦y¦"
  for e e' x y :: hypreal
  by (meson Infinitesimal_minus_iff hrabs_add_Infinitesimal_cancel)


subsection More termHFinite and termInfinitesimal Theorems

text 
  Interesting slightly counterintuitive theorem: necessary
  for proving that an open interval is an NS open set.

lemma Infinitesimal_add_hypreal_of_real_less:
  assumes "x < y" and u: "u  Infinitesimal"
  shows "hypreal_of_real x + u < hypreal_of_real y"
proof -
  have "¦u¦ < hypreal_of_real y - hypreal_of_real x"
    using InfinitesimalD x < y u by fastforce
  then show ?thesis
    by (simp add: abs_less_iff)
qed

lemma Infinitesimal_add_hrabs_hypreal_of_real_less:
  "x  Infinitesimal  ¦hypreal_of_real r¦ < hypreal_of_real y 
    ¦hypreal_of_real r + x¦ < hypreal_of_real y"
  by (metis Infinitesimal_add_hypreal_of_real_less approx_hrabs_add_Infinitesimal approx_sym bex_Infinitesimal_iff2 star_of_abs star_of_less)

lemma Infinitesimal_add_hrabs_hypreal_of_real_less2:
  "x  Infinitesimal  ¦hypreal_of_real r¦ < hypreal_of_real y 
    ¦x + hypreal_of_real r¦ < hypreal_of_real y"
  using Infinitesimal_add_hrabs_hypreal_of_real_less by fastforce

lemma hypreal_of_real_le_add_Infininitesimal_cancel:
  assumes le: "hypreal_of_real x + u  hypreal_of_real y + v" 
      and u: "u  Infinitesimal" and v: "v  Infinitesimal"
  shows "hypreal_of_real x  hypreal_of_real y"
proof (rule ccontr)
  assume "¬ hypreal_of_real x  hypreal_of_real y"
  then have "hypreal_of_real y + (v - u) < hypreal_of_real x"
    by (simp add: Infinitesimal_add_hypreal_of_real_less Infinitesimal_diff u v)
  then show False
    by (simp add: add_diff_eq add_le_imp_le_diff le leD)
qed

lemma hypreal_of_real_le_add_Infininitesimal_cancel2:
  "u  Infinitesimal  v  Infinitesimal 
    hypreal_of_real x + u  hypreal_of_real y + v  x  y"
  by (blast intro: star_of_le [THEN iffD1] intro!: hypreal_of_real_le_add_Infininitesimal_cancel)

lemma hypreal_of_real_less_Infinitesimal_le_zero:
  "hypreal_of_real x < e  e  Infinitesimal  hypreal_of_real x  0"
  by (metis Infinitesimal_interval eq_iff le_less_linear star_of_Infinitesimal_iff_0 star_of_eq_0)

lemma Infinitesimal_add_not_zero: "h  Infinitesimal  x  0  star_of x + h  0"
  by (metis Infinitesimal_add_approx_self star_of_approx_zero_iff)

lemma monad_hrabs_less: "y  monad x  0 < hypreal_of_real e  ¦y - x¦ < hypreal_of_real e"
  by (simp add: Infinitesimal_approx_minus approx_sym less_Infinitesimal_less mem_monad_approx)

lemma mem_monad_SReal_HFinite: "x  monad (hypreal_of_real  a)  x  HFinite"
  using HFinite_star_of approx_HFinite mem_monad_approx by blast


subsection Theorems about Standard Part

lemma st_approx_self: "x  HFinite  st x  x"
  by (metis (no_types, lifting) approx_refl approx_trans3 someI_ex st_def st_part_Ex st_part_Ex1)

lemma st_SReal: "x  HFinite  st x  "
  by (metis (mono_tags, lifting) approx_sym someI_ex st_def st_part_Ex)

lemma st_HFinite: "x  HFinite  st x  HFinite"
  by (erule st_SReal [THEN SReal_subset_HFinite [THEN subsetD]])

lemma st_unique: "r    r  x  st x = r"
  by (meson SReal_subset_HFinite approx_HFinite approx_unique_real st_SReal st_approx_self subsetD)

lemma st_SReal_eq: "x    st x = x"
  by (metis approx_refl st_unique)

lemma st_hypreal_of_real [simp]: "st (hypreal_of_real x) = hypreal_of_real x"
  by (rule SReal_hypreal_of_real [THEN st_SReal_eq])

lemma st_eq_approx: "x  HFinite  y  HFinite  st x = st y  x  y"
  by (auto dest!: st_approx_self elim!: approx_trans3)

lemma approx_st_eq:
  assumes x: "x  HFinite" and y: "y  HFinite" and xy: "x  y"
  shows "st x = st y"
proof -
  have "st x  x" "st y  y" "st x  " "st y  "
    by (simp_all add: st_approx_self st_SReal x y)
  with xy show ?thesis
    by (fast elim: approx_trans approx_trans2 SReal_approx_iff [THEN iffD1])
qed

lemma st_eq_approx_iff: "x  HFinite  y  HFinite  x  y  st x = st y"
  by (blast intro: approx_st_eq st_eq_approx)

lemma st_Infinitesimal_add_SReal: "x    e  Infinitesimal  st (x + e) = x"
  by (simp add: Infinitesimal_add_approx_self st_unique)

lemma st_Infinitesimal_add_SReal2: "x    e  Infinitesimal  st (e + x) = x"
  by (metis add.commute st_Infinitesimal_add_SReal)

lemma HFinite_st_Infinitesimal_add: "x  HFinite  e  Infinitesimal. x = st(x) + e"
  by (blast dest!: st_approx_self [THEN approx_sym] bex_Infinitesimal_iff2 [THEN iffD2])

lemma st_add: "x  HFinite  y  HFinite  st (x + y) = st x + st y"
  by (simp add: st_unique st_SReal st_approx_self approx_add)

lemma st_numeral [simp]: "st (numeral w) = numeral w"
  by (rule Reals_numeral [THEN st_SReal_eq])

lemma st_neg_numeral [simp]: "st (- numeral w) = - numeral w"
  using st_unique by auto

lemma st_0 [simp]: "st 0 = 0"
  by (simp add: st_SReal_eq)

lemma st_1 [simp]: "st 1 = 1"
  by (simp add: st_SReal_eq)

lemma st_neg_1 [simp]: "st (- 1) = - 1"
  by (simp add: st_SReal_eq)

lemma st_minus: "x  HFinite  st (- x) = - st x"
  by (simp add: st_unique st_SReal st_approx_self approx_minus)

lemma st_diff: "x  HFinite; y  HFinite  st (x - y) = st x - st y"
  by (simp add: st_unique st_SReal st_approx_self approx_diff)

lemma st_mult: "x  HFinite; y  HFinite  st (x * y) = st x * st y"
  by (simp add: st_unique st_SReal st_approx_self approx_mult_HFinite)

lemma st_Infinitesimal: "x  Infinitesimal  st x = 0"
  by (simp add: st_unique mem_infmal_iff)

lemma st_not_Infinitesimal: "st(x)  0  x  Infinitesimal"
by (fast intro: st_Infinitesimal)

lemma st_inverse: "x  HFinite  st x  0  st (inverse x) = inverse (st x)"
  by (simp add: approx_inverse st_SReal st_approx_self st_not_Infinitesimal st_unique)

lemma st_divide [simp]: "x  HFinite  y  HFinite  st y  0  st (x / y) = st x / st y"
  by (simp add: divide_inverse st_mult st_not_Infinitesimal HFinite_inverse st_inverse)

lemma st_idempotent [simp]: "x  HFinite  st (st x) = st x"
  by (blast intro: st_HFinite st_approx_self approx_st_eq)

lemma Infinitesimal_add_st_less:
  "x  HFinite  y  HFinite  u  Infinitesimal  st x < st y  st x + u < st y"
  by (metis Infinitesimal_add_hypreal_of_real_less SReal_iff st_SReal star_of_less)

lemma Infinitesimal_add_st_le_cancel:
  "x  HFinite  y  HFinite  u  Infinitesimal 
    st x  st y + u  st x  st y"
  by (meson Infinitesimal_add_st_less leD le_less_linear)

lemma st_le: "x  HFinite  y  HFinite  x  y  st x  st y"
  by (metis approx_le_bound approx_sym linear st_SReal st_approx_self st_part_Ex1)

lemma st_zero_le: "0  x  x  HFinite  0  st x"
  by (metis HFinite_0 st_0 st_le)

lemma st_zero_ge: "x  0  x  HFinite  st x  0"
  by (metis HFinite_0 st_0 st_le)

lemma st_hrabs: "x  HFinite  ¦st x¦ = st ¦x¦"
  by (simp add: order_class.order.antisym st_zero_ge linorder_not_le st_zero_le abs_if st_minus linorder_not_less)


subsection Alternative Definitions using Free Ultrafilter

subsubsection termHFinite

lemma HFinite_FreeUltrafilterNat:
  assumes "star_n X  HFinite"
  shows "u. eventually (λn. norm (X n) < u) 𝒰"
proof -
  obtain r where "hnorm (star_n X) < hypreal_of_real r"
    using HFiniteD SReal_iff assms by fastforce
  then have "F n in 𝒰. norm (X n) < r"
    by (simp add: hnorm_def star_n_less star_of_def starfun_star_n)
  then show ?thesis ..
qed

lemma FreeUltrafilterNat_HFinite:
  assumes "eventually (λn. norm (X n) < u) 𝒰"
  shows "star_n X  HFinite"
proof -
  have "hnorm (star_n X) < hypreal_of_real u"
    by (simp add: assms hnorm_def star_n_less star_of_def starfun_star_n)
  then show ?thesis
    by (meson HInfiniteD SReal_hypreal_of_real less_asym not_HFinite_HInfinite)
qed

lemma HFinite_FreeUltrafilterNat_iff:
  "star_n X  HFinite  (u. eventually (λn. norm (X n) < u) 𝒰)"
  using FreeUltrafilterNat_HFinite HFinite_FreeUltrafilterNat by blast


subsubsection termHInfinite

text Exclude this type of sets from free ultrafilter for Infinite numbers!
lemma FreeUltrafilterNat_const_Finite:
  "eventually (λn. norm (X n) = u) 𝒰  star_n X  HFinite"
  by (simp add: FreeUltrafilterNat_HFinite [where u = "u+1"] eventually_mono)

lemma HInfinite_FreeUltrafilterNat:
  assumes "star_n X  HInfinite" shows "F n in 𝒰. u < norm (X n)"
proof -
have "¬ (F n in 𝒰. norm (X n) < u + 1)"
  using FreeUltrafilterNat_HFinite HFinite_HInfinite_iff assms by auto
  then show ?thesis
    by (auto simp flip: FreeUltrafilterNat.eventually_not_iff elim: eventually_mono)
qed

lemma FreeUltrafilterNat_HInfinite:
  assumes "u. eventually (λn. u < norm (X n)) 𝒰"
  shows "star_n X  HInfinite"
proof -
  { fix u
    assume "Fn in 𝒰. norm (X n) < u" "Fn in 𝒰. u < norm (X n)"
    then have "F x in 𝒰. False"
      by eventually_elim auto
    then have False
      by (simp add: eventually_False FreeUltrafilterNat.proper) }
  then show ?thesis
    using HFinite_FreeUltrafilterNat HInfinite_HFinite_iff assms by blast
qed

lemma HInfinite_FreeUltrafilterNat_iff:
  "star_n X  HInfinite  (u. eventually (λn. u < norm (X n)) 𝒰)"
  using HInfinite_FreeUltrafilterNat FreeUltrafilterNat_HInfinite by blast


subsubsection termInfinitesimal

lemma ball_SReal_eq: "(x::hypreal  Reals. P x)  (x::real. P (star_of x))"
  by (auto simp: SReal_def)


lemma Infinitesimal_FreeUltrafilterNat_iff:
  "(star_n X  Infinitesimal) = (u>0. eventually (λn. norm (X n) < u) 𝒰)"  (is "?lhs = ?rhs")
proof -
  have "?lhs  (r>0. hnorm (star_n X) < hypreal_of_real r)"
    by (simp add: Infinitesimal_def ball_SReal_eq)
  also have "...  ?rhs"
    by (simp add: hnorm_def starfun_star_n star_of_def star_less_def starP2_star_n)
  finally show ?thesis .
qed


text Infinitesimals as smaller than 1/n› for all n::nat (> 0)›.

lemma lemma_Infinitesimal: "(r. 0 < r  x < r)  (n. x < inverse (real (Suc n)))"
  by (meson inverse_positive_iff_positive less_trans of_nat_0_less_iff reals_Archimedean zero_less_Suc)

lemma lemma_Infinitesimal2:
  "(r  Reals. 0 < r  x < r)  (n. x < inverse(hypreal_of_nat (Suc n)))" (is "_ = ?rhs")
proof (intro iffI strip)
  assume R: ?rhs
  fix r::hypreal
  assume "r  " "0 < r"
  then obtain n y where "inverse (real (Suc n)) < y" and r: "r = hypreal_of_real y"
    by (metis SReal_iff reals_Archimedean star_of_0_less)
  then have "inverse (1 + hypreal_of_nat n) < hypreal_of_real y"
    by (metis of_nat_Suc star_of_inverse star_of_less star_of_nat_def)
  then show "x < r"
    by (metis R r le_less_trans less_imp_le of_nat_Suc)
qed (meson Reals_inverse Reals_of_nat of_nat_0_less_iff positive_imp_inverse_positive zero_less_Suc)


lemma Infinitesimal_hypreal_of_nat_iff:
  "Infinitesimal = {x. n. hnorm x < inverse (hypreal_of_nat (Suc n))}"
  using Infinitesimal_def lemma_Infinitesimal2 by auto


subsection Proof that ω› is an infinite number

text It will follow that ε› is an infinitesimal number.

lemma Suc_Un_eq: "{n. n < Suc m} = {n. n < m} Un {n. n = m}"
  by (auto simp add: less_Suc_eq)


text Prove that any segment is finite and hence cannot belong to 𝒰›.

lemma finite_real_of_nat_segment: "finite {n::nat. real n < real (m::nat)}"
  by auto

lemma finite_real_of_nat_less_real: "finite {n::nat. real n < u}"
proof -
  obtain m where "u < real m"
    using reals_Archimedean2 by blast
  then have "{n. real n < u}  {..<m}"
    by force
  then show ?thesis
    using finite_nat_iff_bounded by force
qed

lemma finite_real_of_nat_le_real: "finite {n::nat. real n  u}"
  by (metis infinite_nat_iff_unbounded leD le_nat_floor mem_Collect_eq)

lemma finite_rabs_real_of_nat_le_real: "finite {n::nat. ¦real n¦  u}"
  by (simp add: finite_real_of_nat_le_real)

lemma rabs_real_of_nat_le_real_FreeUltrafilterNat:
  "¬ eventually (λn. ¦real n¦  u) 𝒰"
  by (blast intro!: FreeUltrafilterNat.finite finite_rabs_real_of_nat_le_real)

lemma FreeUltrafilterNat_nat_gt_real: "eventually (λn. u < real n) 𝒰"
proof -
  have "{n::nat. ¬ u < real n} = {n. real n  u}"
    by auto
  then show ?thesis
    by (auto simp add: FreeUltrafilterNat.finite' finite_real_of_nat_le_real)
qed

text The complement of {n. ¦real n¦ ≤ u} = {n. u < ¦real n¦}› is in
  𝒰› by property of (free) ultrafilters.

text termω is a member of termHInfinite.
theorem HInfinite_omega [simp]: "ω  HInfinite"
proof -
  have "F n in 𝒰. u < norm (1 + real n)" for u
    using FreeUltrafilterNat_nat_gt_real [of "u-1"] eventually_mono by fastforce
  then show ?thesis
    by (simp add: omega_def FreeUltrafilterNat_HInfinite)
qed


text Epsilon is a member of Infinitesimal.

lemma Infinitesimal_epsilon [simp]: "ε  Infinitesimal"
  by (auto intro!: HInfinite_inverse_Infinitesimal HInfinite_omega
      simp add: epsilon_inverse_omega)

lemma HFinite_epsilon [simp]: "ε  HFinite"
  by (auto intro: Infinitesimal_subset_HFinite [THEN subsetD])

lemma epsilon_approx_zero [simp]: "ε  0"
  by (simp add: mem_infmal_iff [symmetric])

text Needed for proof that we define a hyperreal [<X(n)] ≈ hypreal_of_real a› given
  that ∀n. |X n - a| < 1/n›. Used in proof of NSLIM ⇒ LIM›.
lemma real_of_nat_less_inverse_iff: "0 < u  u < inverse (real(Suc n))  real(Suc n) < inverse u"
  using less_imp_inverse_less by force

lemma finite_inverse_real_of_posnat_gt_real: "0 < u  finite {n. u < inverse (real (Suc n))}"
proof (simp only: real_of_nat_less_inverse_iff)
  have "{n. 1 + real n < inverse u} = {n. real n < inverse u - 1}"
    by fastforce
  then show "finite {n. real (Suc n) < inverse u}"
    using finite_real_of_nat_less_real [of "inverse u - 1"]
    by auto
qed

lemma finite_inverse_real_of_posnat_ge_real:
  assumes "0 < u"
  shows "finite {n. u  inverse (real (Suc n))}"
proof -
  have "na. u  inverse (1 + real na)  na  ceiling (inverse u)