# Theory NSA

theory NSA
imports HyperDef Lub_Glb
(*  Title:      HOL/NSA/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 "~~/src/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
‹the `infinitely close' relation›
"(x ≈ y) = ((x - y) ∈ Infinitesimal)"

definition
st        :: "hypreal => hypreal" where
‹the standard part of a hyperreal›
"st = (%x. @r. x ∈ HFinite & r ∈ ℝ & r ≈ x)"

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}"

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"

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)

"⋀(x::'a::real_normed_vector star) y r s.
⟦hnorm x < r; hnorm y < s⟧ ⟹ hnorm (x + y) < r + s"

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"
apply (simp only: hnorm_scaleHR)
done

subsection‹Closure Laws for the Standard Reals›

lemma Reals_minus_iff [simp]: "(-x ∈ ℝ) = (x ∈ ℝ)"
apply auto
apply (drule Reals_minus, auto)
done

lemma Reals_add_cancel: "⟦x + y ∈ ℝ; y ∈ ℝ⟧ ⟹ x ∈ ℝ"
by (drule (1) Reals_diff, simp)

lemma SReal_hrabs: "(x::hypreal) ∈ ℝ ==> ¦x¦ ∈ ℝ"

lemma SReal_hypreal_of_real [simp]: "hypreal_of_real x ∈ ℝ"

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: "ε ∉ ℝ"
apply (auto simp add: hypreal_of_real_not_eq_epsilon [THEN not_sym])
done

lemma SReal_omega_not_mem: "ω ∉ ℝ"
apply (auto simp add: hypreal_of_real_not_eq_omega [THEN not_sym])
done

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

lemma SReal_iff: "(x ∈ ℝ) = (∃y. x = hypreal_of_real y)"

lemma hypreal_of_real_image: "hypreal_of_real `(UNIV::real set) = ℝ"

lemma inv_hypreal_of_real_image: "inv hypreal_of_real ` ℝ = UNIV"
apply (rule inj_star_of [THEN inv_f_f, THEN subst], blast)
done

lemma SReal_hypreal_of_real_image:
"[| ∃x. x: P; P ⊆ ℝ |] ==> ∃Q. P = hypreal_of_real ` Q"
by (simp add: SReal_def image_def, blast)

lemma SReal_dense:
"[| (x::hypreal) ∈ ℝ; y ∈ ℝ;  x<y |] ==> ∃r ∈ Reals. x<r & r<y"
apply (drule dense, auto)
done

text‹Completeness of Reals, but both lemmas are unused.›

lemma SReal_sup_lemma:
"P ⊆ ℝ ==> ((∃x ∈ P. y < x) =
(∃X. hypreal_of_real X ∈ P & y < hypreal_of_real X))"
by (blast dest!: SReal_iff [THEN iffD1])

lemma SReal_sup_lemma2:
"[| P ⊆ ℝ; ∃x. x ∈ P; ∃y ∈ Reals. ∀x ∈ P. x < y |]
==> (∃X. X ∈ {w. hypreal_of_real w ∈ P}) &
(∃Y. ∀X ∈ {w. hypreal_of_real w ∈ P}. X < Y)"
apply (rule conjI)
apply (fast dest!: SReal_iff [THEN iffD1])
apply (auto, frule subsetD, assumption)
apply (drule SReal_iff [THEN iffD1])
apply (auto, rule_tac x = ya in exI, auto)
done

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

lemma HFinite_add: "[|x ∈ HFinite; y ∈ HFinite|] ==> (x+y) ∈ HFinite"
done

lemma HFinite_mult:
fixes x y :: "'a::real_normed_algebra star"
shows "[|x ∈ HFinite; y ∈ HFinite|] ==> x*y ∈ HFinite"
apply (blast intro!: Reals_mult hnorm_mult_less)
done

lemma HFinite_scaleHR:
"[|x ∈ HFinite; y ∈ HFinite|] ==> scaleHR x y ∈ HFinite"
apply (blast intro!: Reals_mult hnorm_scaleHR_less)
done

lemma HFinite_minus_iff: "(-x ∈ HFinite) = (x ∈ HFinite)"

lemma HFinite_star_of [simp]: "star_of x ∈ HFinite"
apply (rule_tac x="star_of (norm x) + 1" in bexI)
apply (transfer, simp)
apply (blast intro: Reals_add SReal_hypreal_of_real Reals_1)
done

lemma SReal_subset_HFinite: "(ℝ::hypreal set) ⊆ HFinite"

lemma HFiniteD: "x ∈ HFinite ==> ∃t ∈ Reals. hnorm x < t"

lemma HFinite_hrabs_iff [iff]: "(¦x::hypreal¦ ∈ HFinite) = (x ∈ HFinite)"

lemma HFinite_hnorm_iff [iff]:
"(hnorm (x::hypreal) ∈ HFinite) = (x ∈ HFinite)"

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

(** 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:
fixes x :: "'a::{real_normed_algebra,monoid_mult} star"
shows "x ∈ HFinite ==> x ^ n ∈ HFinite"
apply (induct n)
apply (auto simp add: power_Suc intro: HFinite_mult)
done

lemma HFinite_bounded:
"[|(x::hypreal) ∈ HFinite; y ≤ x; 0 ≤ y |] ==> y ∈ HFinite"
apply (cases "x ≤ 0")
apply (drule_tac y = x in order_trans)
apply (drule_tac [2] order_antisym)
apply (auto intro: order_le_less_trans simp add: abs_if HFinite_def)
done

subsection‹Set of Infinitesimals is a Subring of the Hyperreals›

lemma InfinitesimalI:
"(⋀r. ⟦r ∈ ℝ; 0 < r⟧ ⟹ hnorm x < r) ⟹ x ∈ Infinitesimal"

lemma InfinitesimalD:
"x ∈ Infinitesimal ==> ∀r ∈ Reals. 0 < r --> hnorm x < r"

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"

lemma hypreal_sum_of_halves: "x/(2::hypreal) + x/(2::hypreal) = x"
by auto

"[| x ∈ Infinitesimal; y ∈ Infinitesimal |] ==> (x+y) ∈ Infinitesimal"
apply (rule InfinitesimalI)
apply (rule hypreal_sum_of_halves [THEN subst])
apply (drule half_gt_zero)
apply (blast intro: hnorm_add_less SReal_divide_numeral dest: InfinitesimalD)
done

lemma Infinitesimal_minus_iff [simp]: "(-x:Infinitesimal) = (x:Infinitesimal)"

lemma Infinitesimal_hnorm_iff:
"(hnorm x ∈ Infinitesimal) = (x ∈ Infinitesimal)"

lemma Infinitesimal_hrabs_iff [iff]:
"(¦x::hypreal¦ ∈ Infinitesimal) = (x ∈ Infinitesimal)"

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"
shows "[|x ∈ Infinitesimal; y ∈ Infinitesimal|] ==> (x * y) ∈ Infinitesimal"
apply (rule InfinitesimalI)
apply (subgoal_tac "hnorm (x * y) < 1 * r", simp only: mult_1)
apply (rule hnorm_mult_less)
done

lemma Infinitesimal_HFinite_mult:
fixes x y :: "'a::real_normed_algebra star"
shows "[| x ∈ Infinitesimal; y ∈ HFinite |] ==> (x * y) ∈ Infinitesimal"
apply (rule InfinitesimalI)
apply (drule HFiniteD, clarify)
apply (subgoal_tac "0 < t")
apply (subgoal_tac "hnorm (x * y) < (r / t) * t", simp)
apply (subgoal_tac "0 < r / t")
apply (rule hnorm_mult_less)
apply assumption
apply simp
apply (erule order_le_less_trans [OF hnorm_ge_zero])
done

lemma Infinitesimal_HFinite_scaleHR:
"[| x ∈ Infinitesimal; y ∈ HFinite |] ==> scaleHR x y ∈ Infinitesimal"
apply (rule InfinitesimalI)
apply (drule HFiniteD, clarify)
apply (drule InfinitesimalD)
apply (subgoal_tac "0 < t")
apply (subgoal_tac "¦x¦ * hnorm y < (r / t) * t", simp)
apply (subgoal_tac "0 < r / t")
apply (rule mult_strict_mono', simp_all)
apply (erule order_le_less_trans [OF hnorm_ge_zero])
done

lemma Infinitesimal_HFinite_mult2:
fixes x y :: "'a::real_normed_algebra star"
shows "[| x ∈ Infinitesimal; y ∈ HFinite |] ==> (y * x) ∈ Infinitesimal"
apply (rule InfinitesimalI)
apply (drule HFiniteD, clarify)
apply (subgoal_tac "0 < t")
apply (subgoal_tac "hnorm (y * x) < t * (r / t)", simp)
apply (subgoal_tac "0 < r / t")
apply (rule hnorm_mult_less)
apply assumption
apply simp
apply (erule order_le_less_trans [OF hnorm_ge_zero])
done

lemma Infinitesimal_scaleR2:
"x ∈ Infinitesimal ==> a *R x ∈ Infinitesimal"
apply (case_tac "a = 0", simp)
apply (rule InfinitesimalI)
apply (drule InfinitesimalD)
apply (drule_tac x="r / ¦star_of a¦" in bspec)
apply simp
apply (simp add: hnorm_scaleR pos_less_divide_eq mult.commute)
done

lemma Compl_HFinite: "- HFinite = HInfinite"
apply (auto simp add: HInfinite_def HFinite_def linorder_not_less)
apply (rule_tac y="r + 1" in order_less_le_trans, simp)
apply simp
done

lemma HInfinite_inverse_Infinitesimal:
fixes x :: "'a::real_normed_div_algebra star"
shows "x ∈ HInfinite ==> inverse x ∈ Infinitesimal"
apply (rule InfinitesimalI)
apply (subgoal_tac "x ≠ 0")
apply (rule inverse_less_imp_less)
apply assumption
apply (clarify, simp add: Compl_HFinite [symmetric])
done

lemma HInfiniteI: "(⋀r. r ∈ ℝ ⟹ r < hnorm x) ⟹ x ∈ HInfinite"

lemma HInfiniteD: "⟦x ∈ HInfinite; r ∈ ℝ⟧ ⟹ r < hnorm x"

lemma HInfinite_mult:
fixes x y :: "'a::real_normed_div_algebra star"
shows "[|x ∈ HInfinite; y ∈ HInfinite|] ==> (x*y) ∈ HInfinite"
apply (rule HInfiniteI, simp only: hnorm_mult)
apply (subgoal_tac "r * 1 < hnorm x * hnorm y", simp only: mult_1)
apply (case_tac "x = 0", simp add: HInfinite_def)
apply (rule mult_strict_mono)
done

lemma hypreal_add_zero_less_le_mono: "[|r < x; (0::hypreal) ≤ y|] ==> r < x+y"

"[|(x::hypreal) ∈ HInfinite; 0 ≤ y; 0 ≤ x|] ==> (x + y): HInfinite"

"[|(x::hypreal) ∈ HInfinite; 0 ≤ y; 0 ≤ x|] ==> (y + x): HInfinite"

"[|(x::hypreal) ∈ HInfinite; 0 < y; 0 < x|] ==> (x + y): HInfinite"

lemma HInfinite_minus_iff: "(-x ∈ HInfinite) = (x ∈ HInfinite)"

"[|(x::hypreal) ∈ HInfinite; y ≤ 0; x ≤ 0|] ==> (x + y): HInfinite"
apply (drule HInfinite_minus_iff [THEN iffD2])
apply (rule HInfinite_minus_iff [THEN iffD1])
apply simp_all
done

"[|(x::hypreal) ∈ HInfinite; y < 0; x < 0|] ==> (x + y): HInfinite"

lemma HFinite_sum_squares:
fixes a b c :: "'a::real_normed_algebra star"
shows "[|a: HFinite; b: HFinite; c: HFinite|]
==> a*a + b*b + c*c ∈ HFinite"

lemma not_Infinitesimal_not_zero: "x ∉ Infinitesimal ==> x ≠ 0"
by auto

lemma not_Infinitesimal_not_zero2: "x ∈ HFinite - Infinitesimal ==> x ≠ 0"
by auto

lemma HFinite_diff_Infinitesimal_hrabs:
"(x::hypreal) ∈ HFinite - Infinitesimal ==> ¦x¦ ∈ HFinite - Infinitesimal"
by blast

lemma hnorm_le_Infinitesimal:
"⟦e ∈ Infinitesimal; hnorm x ≤ e⟧ ⟹ x ∈ Infinitesimal"
by (auto simp add: 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::hypreal¦ ≤ e |] ==> x ∈ Infinitesimal"
by (erule hnorm_le_Infinitesimal, simp)

lemma hrabs_less_Infinitesimal:
"[| e ∈ Infinitesimal; ¦x::hypreal¦ < e |] ==> x ∈ Infinitesimal"
by (erule hnorm_less_Infinitesimal, simp)

lemma Infinitesimal_interval:
"[| e ∈ Infinitesimal; e' ∈ Infinitesimal; e' < x ; x < e |]
==> (x::hypreal) ∈ Infinitesimal"
by (auto simp add: Infinitesimal_def abs_less_iff)

lemma Infinitesimal_interval2:
"[| e ∈ Infinitesimal; e' ∈ Infinitesimal;
e' ≤ x ; x ≤ e |] ==> (x::hypreal) ∈ Infinitesimal"
by (auto intro: Infinitesimal_interval simp add: order_le_less)

lemma lemma_Infinitesimal_hyperpow:
"[| (x::hypreal) ∈ Infinitesimal; 0 < N |] ==> ¦x pow N¦ ≤ ¦x¦"
apply (unfold Infinitesimal_def)
apply (auto intro!: hyperpow_Suc_le_self2
simp add: hyperpow_hrabs [symmetric] hypnat_gt_zero_iff2 abs_ge_zero)
done

lemma Infinitesimal_hyperpow:
"[| (x::hypreal) ∈ Infinitesimal; 0 < N |] ==> x pow N ∈ Infinitesimal"
apply (rule hrabs_le_Infinitesimal)
apply (rule_tac [2] lemma_Infinitesimal_hyperpow, auto)
done

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::hypreal) ∈ Infinitesimal; 0 < n |] ==> x ^ n ∈ Infinitesimal"

lemma not_Infinitesimal_mult:
fixes x y :: "'a::real_normed_div_algebra star"
shows "[| x ∉ Infinitesimal;  y ∉ Infinitesimal|] ==> (x*y) ∉Infinitesimal"
apply (unfold Infinitesimal_def, clarify, rename_tac r s)
apply (simp only: linorder_not_less hnorm_mult)
apply (drule_tac x = "r * s" in bspec)
apply (fast intro: Reals_mult)
apply (simp)
apply (drule_tac c = s and d = "hnorm y" and a = r and b = "hnorm x" in mult_mono)
apply (simp_all (no_asm_simp))
done

lemma Infinitesimal_mult_disj:
fixes x y :: "'a::real_normed_div_algebra star"
shows "x*y ∈ Infinitesimal ==> x ∈ Infinitesimal | y ∈ Infinitesimal"
apply (rule ccontr)
apply (drule de_Morgan_disj [THEN iffD1])
apply (fast dest: not_Infinitesimal_mult)
done

lemma HFinite_Infinitesimal_not_zero: "x ∈ HFinite-Infinitesimal ==> x ≠ 0"
by blast

lemma HFinite_Infinitesimal_diff_mult:
fixes x y :: "'a::real_normed_div_algebra star"
shows "[| x ∈ HFinite - Infinitesimal;
y ∈ HFinite - Infinitesimal
|] ==> (x*y) ∈ HFinite - Infinitesimal"
apply clarify
apply (blast dest: HFinite_mult not_Infinitesimal_mult)
done

lemma Infinitesimal_subset_HFinite:
"Infinitesimal ⊆ HFinite"
apply (simp add: Infinitesimal_def HFinite_def, auto)
apply (rule_tac x = 1 in bexI, auto)
done

lemma Infinitesimal_star_of_mult:
fixes x :: "'a::real_normed_algebra star"
shows "x ∈ Infinitesimal ==> x * star_of r ∈ Infinitesimal"
by (erule HFinite_star_of [THEN [2] Infinitesimal_HFinite_mult])

lemma Infinitesimal_star_of_mult2:
fixes x :: "'a::real_normed_algebra star"
shows "x ∈ Infinitesimal ==> star_of r * x ∈ Infinitesimal"
by (erule HFinite_star_of [THEN [2] Infinitesimal_HFinite_mult2])

subsection‹The Infinitely Close Relation›

lemma mem_infmal_iff: "(x ∈ Infinitesimal) = (x ≈ 0)"

lemma approx_minus_iff: " (x ≈ y) = (x - y ≈ 0)"

lemma approx_minus_iff2: " (x ≈ y) = (-y + x ≈ 0)"

lemma approx_refl [iff]: "x ≈ x"

lemma hypreal_minus_distrib1: "-(y + -(x::'a::ab_group_add)) = x + -y"

lemma approx_sym: "x ≈ y ==> y ≈ x"
apply (drule Infinitesimal_minus_iff [THEN iffD2])
apply simp
done

lemma approx_trans: "[| x ≈ y; y ≈ z |] ==> x ≈ z"
apply simp
done

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)

(*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)

apply (auto dest: approx_sym elim!: approx_trans equalityCE)
done

lemma Infinitesimal_approx:
"[| x ∈ Infinitesimal; y ∈ Infinitesimal |] ==> x ≈ y"
apply (blast intro: approx_trans approx_sym)
done

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"
apply (rule approx_minus_iff [THEN iffD2, THEN approx_sym])
apply (drule approx_minus_iff [THEN iffD1])
done

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"

lemma approx_diff: "[| a ≈ b; c ≈ d |] ==> a - c ≈ b - d"
using approx_add [of a b "- c" "- d"] by simp

lemma approx_mult1:
fixes a b c :: "'a::real_normed_algebra star"
shows "[| a ≈ b; c: HFinite|] ==> a*c ≈ b*c"
left_diff_distrib [symmetric])

lemma approx_mult2:
fixes a b c :: "'a::real_normed_algebra star"
shows "[|a ≈ b; c: HFinite|] ==> c*a ≈ c*b"
right_diff_distrib [symmetric])

lemma approx_mult_subst:
fixes u v x y :: "'a::real_normed_algebra star"
shows "[|u ≈ v*x; x ≈ y; v ∈ HFinite|] ==> u ≈ v*y"
by (blast intro: approx_mult2 approx_trans)

lemma approx_mult_subst2:
fixes u v x y :: "'a::real_normed_algebra star"
shows "[| u ≈ x*v; x ≈ y; v ∈ HFinite |] ==> u ≈ y*v"
by (blast intro: approx_mult1 approx_trans)

lemma approx_mult_subst_star_of:
fixes u x y :: "'a::real_normed_algebra star"
shows "[| u ≈ x*star_of v; x ≈ y |] ==> u ≈ y*star_of v"
by (auto intro: approx_mult_subst2)

lemma approx_eq_imp: "a = b ==> a ≈ b"

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)"

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"
apply (rule bex_Infinitesimal_iff [THEN iffD1])
apply (drule Infinitesimal_minus_iff [THEN iffD2])
done

lemma Infinitesimal_add_approx_self: "y ∈ Infinitesimal ==> x ≈ x + y"
apply (rule bex_Infinitesimal_iff [THEN iffD1])
apply (drule Infinitesimal_minus_iff [THEN iffD2])
done

lemma Infinitesimal_add_approx_self2: "y ∈ Infinitesimal ==> x ≈ y + x"

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"
apply (drule_tac x = x in Infinitesimal_add_approx_self [THEN approx_sym])
apply (erule approx_trans3 [THEN approx_sym], assumption)
done

"[| y ∈ Infinitesimal; x ≈ z + y|] ==> x ≈ z"
apply (drule_tac x = z in Infinitesimal_add_approx_self2 [THEN approx_sym])
apply (erule approx_trans3 [THEN approx_sym])
apply (erule approx_sym)
done

lemma approx_add_left_cancel: "d + b  ≈ d + c ==> b ≈ c"
apply (drule approx_minus_iff [THEN iffD1])
apply (simp add: approx_minus_iff [symmetric] ac_simps)
done

lemma approx_add_right_cancel: "b + d ≈ c + d ==> b ≈ c"
done

lemma approx_add_mono1: "b ≈ c ==> d + b ≈ d + c"
apply (rule approx_minus_iff [THEN iffD2])
apply (simp add: approx_minus_iff [symmetric] ac_simps)
done

lemma approx_add_mono2: "b ≈ c ==> b + a ≈ c + a"

lemma approx_add_left_iff [simp]: "(a + b ≈ a + c) = (b ≈ c)"

lemma approx_add_right_iff [simp]: "(b + a ≈ c + a) = (b ≈ c)"

lemma approx_HFinite: "[| x ∈ HFinite; x ≈ y |] ==> y ∈ HFinite"
apply (drule bex_Infinitesimal_iff2 [THEN iffD2], safe)
apply (drule Infinitesimal_subset_HFinite [THEN subsetD, THEN HFinite_minus_iff [THEN iffD2]])
done

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

lemma approx_mult_HFinite:
fixes a b c d :: "'a::real_normed_algebra star"
shows "[|a ≈ b; c ≈ d; b: HFinite; d: HFinite|] ==> a*c ≈ b*d"
apply (rule approx_trans)
apply (rule_tac [2] approx_mult2)
apply (rule approx_mult1)
prefer 2 apply (blast intro: approx_HFinite approx_sym, auto)
done

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"
apply (unfold approx_def)
apply (drule (1) Infinitesimal_HFinite_scaleHR)
apply (simp only: scaleHR_left_diff_distrib)
apply (simp add: scaleHR_def star_scaleR_def [symmetric])
done

lemma approx_scaleR2:
"a ≈ b ==> c *R a ≈ c *R b"
scaleR_right_diff_distrib [symmetric])

lemma approx_scaleR_HFinite:
"[|a ≈ star_of b; c ≈ d; d: HFinite|] ==> scaleHR a c ≈ b *R d"
apply (rule approx_trans)
apply (rule_tac [2] approx_scaleR2)
apply (rule approx_scaleR1)
prefer 2 apply (blast intro: approx_HFinite approx_sym, auto)
done

lemma approx_mult_star_of:
fixes a c :: "'a::real_normed_algebra star"
shows "[|a ≈ star_of b; c ≈ star_of d |]
==> a*c ≈ star_of b*star_of d"
by (blast intro!: approx_mult_HFinite approx_star_of_HFinite HFinite_star_of)

lemma approx_SReal_mult_cancel_zero:
"[| (a::hypreal) ∈ ℝ; a ≠ 0; a*x ≈ 0 |] ==> x ≈ 0"
apply (drule Reals_inverse [THEN SReal_subset_HFinite [THEN subsetD]])
apply (auto dest: approx_mult2 simp add: mult.assoc [symmetric])
done

lemma approx_mult_SReal1: "[| (a::hypreal) ∈ ℝ; x ≈ 0 |] ==> x*a ≈ 0"
by (auto dest: SReal_subset_HFinite [THEN subsetD] approx_mult1)

lemma approx_mult_SReal2: "[| (a::hypreal) ∈ ℝ; x ≈ 0 |] ==> a*x ≈ 0"
by (auto dest: SReal_subset_HFinite [THEN subsetD] approx_mult2)

lemma approx_mult_SReal_zero_cancel_iff [simp]:
"[|(a::hypreal) ∈ ℝ; a ≠ 0 |] ==> (a*x ≈ 0) = (x ≈ 0)"
by (blast intro: approx_SReal_mult_cancel_zero approx_mult_SReal2)

lemma approx_SReal_mult_cancel:
"[| (a::hypreal) ∈ ℝ; a ≠ 0; a* w ≈ a*z |] ==> w ≈ z"
apply (drule Reals_inverse [THEN SReal_subset_HFinite [THEN subsetD]])
apply (auto dest: approx_mult2 simp add: mult.assoc [symmetric])
done

lemma approx_SReal_mult_cancel_iff1 [simp]:
"[| (a::hypreal) ∈ ℝ; a ≠ 0|] ==> (a* w ≈ a*z) = (w ≈ z)"
by (auto intro!: approx_mult2 SReal_subset_HFinite [THEN subsetD]
intro: approx_SReal_mult_cancel)

lemma approx_le_bound: "[| (z::hypreal) ≤ f; f ≈ g; g ≤ z |] ==> f ≈ z"
apply (simp add: bex_Infinitesimal_iff2 [symmetric], auto)
apply (rule_tac x = "g+y-z" in bexI)
apply (simp (no_asm))
apply (rule Infinitesimal_interval2)
apply (rule_tac [2] Infinitesimal_zero, auto)
done

lemma approx_hnorm:
fixes x y :: "'a::real_normed_vector star"
shows "x ≈ y ⟹ hnorm x ≈ hnorm y"
proof (unfold approx_def)
assume "x - y ∈ Infinitesimal"
hence 1: "hnorm (x - y) ∈ Infinitesimal"
by (simp only: Infinitesimal_hnorm_iff)
moreover have 2: "(0::real star) ∈ Infinitesimal"
by (rule Infinitesimal_zero)
moreover have 3: "0 ≤ ¦hnorm x - hnorm y¦"
by (rule abs_ge_zero)
moreover have 4: "¦hnorm x - hnorm y¦ ≤ hnorm (x - y)"
by (rule hnorm_triangle_ineq3)
ultimately have "¦hnorm x - hnorm y¦ ∈ Infinitesimal"
by (rule Infinitesimal_interval2)
thus "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::hypreal) ∈ ℝ; y ∈ Infinitesimal; 0 < x |] ==> y < x"
apply (rule abs_ge_self [THEN order_le_less_trans], auto)
done

lemma Infinitesimal_less_SReal2:
"(y::hypreal) ∈ Infinitesimal ==> ∀r ∈ Reals. 0 < r --> y < r"
by (blast intro: Infinitesimal_less_SReal)

lemma SReal_not_Infinitesimal:
"[| 0 < y;  (y::hypreal) ∈ ℝ|] ==> y ∉ Infinitesimal"
done

lemma SReal_minus_not_Infinitesimal:
"[| y < 0;  (y::hypreal) ∈ ℝ |] ==> y ∉ Infinitesimal"
apply (subst Infinitesimal_minus_iff [symmetric])
apply (rule SReal_not_Infinitesimal, auto)
done

lemma SReal_Int_Infinitesimal_zero: "ℝ Int Infinitesimal = {0::hypreal}"
apply auto
apply (cut_tac x = x and y = 0 in linorder_less_linear)
apply (blast dest: SReal_not_Infinitesimal SReal_minus_not_Infinitesimal)
done

lemma SReal_Infinitesimal_zero:
"[| (x::hypreal) ∈ ℝ; x ∈ Infinitesimal|] ==> x = 0"
by (cut_tac SReal_Int_Infinitesimal_zero, blast)

lemma SReal_HFinite_diff_Infinitesimal:
"[| (x::hypreal) ∈ ℝ; x ≠ 0 |] ==> x ∈ HFinite - Infinitesimal"
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)"
apply (drule_tac x="hnorm (star_of x)" in bspec)
apply (rule_tac x="norm x" in exI, simp)
apply simp
done

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])

(*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"
apply (simp only: star_one_def star_of_Infinitesimal_iff_0)
apply simp
done

lemma approx_SReal_not_zero:
"[| (y::hypreal) ∈ ℝ; x ≈ y; y≠ 0 |] ==> x ≠ 0"
apply (cut_tac x = 0 and y = y in linorder_less_linear, simp)
apply (blast dest: approx_sym [THEN mem_infmal_iff [THEN iffD2]] SReal_not_Infinitesimal SReal_minus_not_Infinitesimal)
done

lemma HFinite_diff_Infinitesimal_approx:
"[| x ≈ y; y ∈ HFinite - Infinitesimal |]
==> x ∈ HFinite - Infinitesimal"
apply (auto intro: approx_sym [THEN [2] approx_HFinite]
apply (drule approx_trans3, assumption)
apply (blast dest: approx_sym)
done

(*The premise y≠0 is essential; otherwise x/y =0 and we lose the
HFinite premise.*)
lemma Infinitesimal_ratio:
fixes x y :: "'a::{real_normed_div_algebra,field} star"
shows "[| y ≠ 0;  y ∈ Infinitesimal;  x/y ∈ HFinite |]
==> x ∈ Infinitesimal"
apply (drule Infinitesimal_HFinite_mult2, assumption)
done

lemma Infinitesimal_SReal_divide:
"[| (x::hypreal) ∈ Infinitesimal; y ∈ ℝ |] ==> x/y ∈ Infinitesimal"
apply (auto intro!: Infinitesimal_HFinite_mult
dest!: Reals_inverse [THEN SReal_subset_HFinite [THEN subsetD]])
done

(*------------------------------------------------------------------
Standard Part Theorem: 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)"
apply safe
apply (simp only: star_of_diff [symmetric])
apply (simp only: star_of_Infinitesimal_iff_0)
apply simp
done

lemma SReal_approx_iff:
"[|(x::hypreal) ∈ ℝ; y ∈ ℝ|] ==> (x ≈ y) = (x = y)"
apply auto
apply (drule (1) Reals_diff)
apply (drule (1) SReal_Infinitesimal_zero)
apply simp
done

lemma numeral_approx_iff [simp]:
"(numeral v ≈ (numeral w :: 'a::{numeral,real_normed_vector} star)) =
(numeral v = (numeral w :: 'a))"
apply (unfold star_numeral_def)
apply (rule star_of_approx_iff)
done

(*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))"
apply (unfold star_numeral_def star_zero_def star_one_def)
apply (unfold 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)"

lemma star_of_approx_one_iff [simp]: "(star_of k ≈ 1) = (k = 1)"

lemma approx_unique_real:
"[| (r::hypreal) ∈ ℝ; s ∈ ℝ; r ≈ x; s ≈ x|] ==> r = s"
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 :: real set) Q Y)"

lemma hypreal_of_real_isLub1:
"isLub ℝ (hypreal_of_real ` Q) (hypreal_of_real Y)
==> isLub (UNIV :: real set) Q Y"
apply (auto intro: hypreal_of_real_isUb_iff [THEN iffD2]
done

lemma hypreal_of_real_isLub2:
"isLub (UNIV :: real set) Q Y
==> isLub ℝ (hypreal_of_real ` Q) (hypreal_of_real Y)"
apply (auto simp add: isLub_def leastP_def hypreal_of_real_isUb_iff setge_def)
by (metis SReal_iff hypreal_of_real_isUb_iff isUbD2a star_of_le)

lemma hypreal_of_real_isLub_iff:
"(isLub ℝ (hypreal_of_real ` Q) (hypreal_of_real Y)) =
(isLub (UNIV :: real set) Q Y)"
by (blast intro: hypreal_of_real_isLub1 hypreal_of_real_isLub2)

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 lemma_isLub_hypreal_of_real2:
"∃Yo. isLub ℝ P (hypreal_of_real Yo) ==> ∃Y. isLub ℝ P Y"
by (auto simp add: isLub_def leastP_def isUb_def)

lemma SReal_complete:
"[| P ⊆ ℝ;  ∃x. x ∈ P;  ∃Y. isUb ℝ P Y |]
==> ∃t::hypreal. isLub ℝ P t"
apply (frule SReal_hypreal_of_real_image)
apply (auto, drule lemma_isUb_hypreal_of_real)
apply (auto intro!: reals_complete lemma_isLub_hypreal_of_real2
done

lemma lemma_st_part_ub:
"(x::hypreal) ∈ HFinite ==> ∃u. isUb ℝ {s. s ∈ ℝ & s < x} u"
apply (drule HFiniteD, safe)
apply (rule exI, rule isUbI)
apply (auto intro: setleI isUbI simp add: abs_less_iff)
done

lemma lemma_st_part_nonempty:
"(x::hypreal) ∈ HFinite ==> ∃y. y ∈ {s. s ∈ ℝ & s < x}"
apply (drule HFiniteD, safe)
apply (drule Reals_minus)
apply (rule_tac x = "-t" in exI)
done

lemma lemma_st_part_lub:
"(x::hypreal) ∈ HFinite ==> ∃t. isLub ℝ {s. s ∈ ℝ & s < x} t"
by (blast intro!: SReal_complete lemma_st_part_ub lemma_st_part_nonempty Collect_restrict)

lemma lemma_st_part_le1:
"[| (x::hypreal) ∈ HFinite;  isLub ℝ {s. s ∈ ℝ & s < x} t;
r ∈ ℝ;  0 < r |] ==> x ≤ t + r"
apply (frule isLubD1a)
apply (rule ccontr, drule linorder_not_le [THEN iffD2])
apply (drule_tac y = "r + t" in isLubD1 [THEN setleD], auto)
done

lemma hypreal_setle_less_trans:
"[| S *<= (x::hypreal); x < y |] ==> S *<= y"
apply (auto dest!: bspec order_le_less_trans intro: order_less_imp_le)
done

lemma hypreal_gt_isUb:
"[| isUb R S (x::hypreal); x < y; y ∈ R |] ==> isUb R S y"
apply (blast intro: hypreal_setle_less_trans)
done

lemma lemma_st_part_gt_ub:
"[| (x::hypreal) ∈ HFinite; x < y; y ∈ ℝ |]
==> isUb ℝ {s. s ∈ ℝ & s < x} y"
by (auto dest: order_less_trans intro: order_less_imp_le intro!: isUbI setleI)

lemma lemma_minus_le_zero: "t ≤ t + -r ==> r ≤ (0::hypreal)"
apply (drule_tac c = "-t" in add_left_mono)
done

lemma lemma_st_part_le2:
"[| (x::hypreal) ∈ HFinite;
isLub ℝ {s. s ∈ ℝ & s < x} t;
r ∈ ℝ; 0 < r |]
==> t + -r ≤ x"
apply (frule isLubD1a)
apply (rule ccontr, drule linorder_not_le [THEN iffD1])
apply (drule Reals_minus, drule_tac a = t in Reals_add, assumption)
apply (drule lemma_st_part_gt_ub, assumption+)
apply (drule isLub_le_isUb, assumption)
apply (drule lemma_minus_le_zero)
apply (auto dest: order_less_le_trans)
done

lemma lemma_st_part1a:
"[| (x::hypreal) ∈ HFinite;
isLub ℝ {s. s ∈ ℝ & s < x} t;
r ∈ ℝ; 0 < r |]
==> x + -t ≤ r"
apply (subgoal_tac "x ≤ t+r")
apply (auto intro: lemma_st_part_le1)
done

lemma lemma_st_part2a:
"[| (x::hypreal) ∈ HFinite;
isLub ℝ {s. s ∈ ℝ & s < x} t;
r ∈ ℝ;  0 < r |]
==> -(x + -t) ≤ r"
apply (subgoal_tac "(t + -r ≤ x)")
apply simp
apply (rule lemma_st_part_le2)
apply auto
done

lemma lemma_SReal_ub:
"(x::hypreal) ∈ ℝ ==> isUb ℝ {s. s ∈ ℝ & s < x} x"
by (auto intro: isUbI setleI order_less_imp_le)

lemma lemma_SReal_lub:
"(x::hypreal) ∈ ℝ ==> isLub ℝ {s. s ∈ ℝ & s < x} x"
apply (auto intro!: isLubI2 lemma_SReal_ub setgeI)
apply (frule isUbD2a)
apply (rule_tac x = x and y = y in linorder_cases)
apply (auto intro!: order_less_imp_le)
apply (drule SReal_dense, assumption, assumption, safe)
apply (drule_tac y = r in isUbD)
apply (auto dest: order_less_le_trans)
done

lemma lemma_st_part_not_eq1:
"[| (x::hypreal) ∈ HFinite;
isLub ℝ {s. s ∈ ℝ & s < x} t;
r ∈ ℝ; 0 < r |]
==> x + -t ≠ r"
apply auto
apply (frule isLubD1a [THEN Reals_minus])
using Reals_add_cancel [of x "- t"] apply simp
apply (drule_tac x = x in lemma_SReal_lub)
apply (drule isLub_unique, assumption, auto)
done

lemma lemma_st_part_not_eq2:
"[| (x::hypreal) ∈ HFinite;
isLub ℝ {s. s ∈ ℝ & s < x} t;
r ∈ ℝ; 0 < r |]
==> -(x + -t) ≠ r"
apply (auto)
apply (frule isLubD1a)
using Reals_add_cancel [of "- x" t] apply simp
apply (drule_tac x = x in lemma_SReal_lub)
apply (drule isLub_unique, assumption, auto)
done

lemma lemma_st_part_major:
"[| (x::hypreal) ∈ HFinite;
isLub ℝ {s. s ∈ ℝ & s < x} t;
r ∈ ℝ; 0 < r |]
==> ¦x - t¦ < r"
apply (frule lemma_st_part1a)
apply (frule_tac [4] lemma_st_part2a, auto)
apply (drule order_le_imp_less_or_eq)+
apply auto
using lemma_st_part_not_eq2 apply fastforce
using lemma_st_part_not_eq1 apply fastforce
done

lemma lemma_st_part_major2:
"[| (x::hypreal) ∈ HFinite; isLub ℝ {s. s ∈ ℝ & s < x} t |]
==> ∀r ∈ Reals. 0 < r --> ¦x - t¦ < r"
by (blast dest!: lemma_st_part_major)

text‹Existence of real and Standard Part Theorem›
lemma lemma_st_part_Ex:
"(x::hypreal) ∈ HFinite
==> ∃t ∈ Reals. ∀r ∈ Reals. 0 < r --> ¦x - t¦ < r"
apply (frule lemma_st_part_lub, safe)
apply (frule isLubD1a)
apply (blast dest: lemma_st_part_major2)
done

lemma st_part_Ex:
"(x::hypreal) ∈ HFinite ==> ∃t ∈ Reals. x ≈ t"
apply (drule lemma_st_part_Ex, auto)
done

text‹There is a unique real infinitely close›
lemma st_part_Ex1: "x ∈ HFinite ==> EX! t::hypreal. t ∈ ℝ & x ≈ t"
apply (drule st_part_Ex, safe)
apply (drule_tac [2] approx_sym, drule_tac [2] approx_sym, drule_tac [2] approx_sym)
apply (auto intro!: approx_unique_real)
done

subsection‹Finite, Infinite and Infinitesimal›

lemma HFinite_Int_HInfinite_empty [simp]: "HFinite Int HInfinite = {}"
apply (auto dest: order_less_trans)
done

lemma HFinite_not_HInfinite:
assumes x: "x ∈ HFinite" shows "x ∉ HInfinite"
proof
assume x': "x ∈ HInfinite"
with x have "x ∈ HFinite ∩ HInfinite" by blast
thus False by auto
qed

lemma not_HFinite_HInfinite: "x∉ HFinite ==> x ∈ HInfinite"
apply (simp add: HInfinite_def HFinite_def, auto)
apply (drule_tac x = "r + 1" in bspec)
apply (auto)
done

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)"

lemma HInfinite_diff_HFinite_Infinitesimal_disj:
"x ∉ Infinitesimal ==> x ∈ HInfinite | x ∈ HFinite - Infinitesimal"
by (fast intro: not_HFinite_HInfinite)

lemma HFinite_inverse:
fixes x :: "'a::real_normed_div_algebra star"
shows "[| x ∈ HFinite; x ∉ Infinitesimal |] ==> inverse x ∈ HFinite"
apply (subgoal_tac "x ≠ 0")
apply (cut_tac x = "inverse x" in HInfinite_HFinite_disj)
apply (auto dest!: HInfinite_inverse_Infinitesimal
done

lemma HFinite_inverse2:
fixes x :: "'a::real_normed_div_algebra star"
shows "x ∈ HFinite - Infinitesimal ==> inverse x ∈ HFinite"
by (blast intro: HFinite_inverse)

(* stronger statement possible in fact *)
lemma Infinitesimal_inverse_HFinite:
fixes x :: "'a::real_normed_div_algebra star"
shows "x ∉ Infinitesimal ==> inverse(x) ∈ HFinite"
apply (drule HInfinite_diff_HFinite_Infinitesimal_disj)
apply (blast intro: HFinite_inverse HInfinite_inverse_Infinitesimal Infinitesimal_subset_HFinite [THEN subsetD])
done

lemma HFinite_not_Infinitesimal_inverse:
fixes x :: "'a::real_normed_div_algebra star"
shows "x ∈ HFinite - Infinitesimal ==> inverse x ∈ HFinite - Infinitesimal"
apply (auto intro: Infinitesimal_inverse_HFinite)
apply (drule Infinitesimal_HFinite_mult2, assumption)
done

lemma approx_inverse:
fixes x y :: "'a::real_normed_div_algebra star"
shows
"[| x ≈ y; y ∈  HFinite - Infinitesimal |]
==> inverse x ≈ inverse y"
apply (frule HFinite_diff_Infinitesimal_approx, assumption)
apply (frule not_Infinitesimal_not_zero2)
apply (frule_tac x = x in not_Infinitesimal_not_zero2)
apply (drule HFinite_inverse2)+
apply (drule approx_mult2, assumption, auto)
apply (drule_tac c = "inverse x" in approx_mult1, assumption)
apply (auto intro: approx_sym simp add: mult.assoc)
done

(*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]

fixes x h :: "'a::real_normed_div_algebra star"
shows
"[| x ∈ HFinite - Infinitesimal;
h ∈ Infinitesimal |] ==> inverse(x + h) ≈ inverse x"
apply (auto intro: approx_inverse approx_sym Infinitesimal_add_approx_self)
done

fixes x h :: "'a::real_normed_div_algebra star"
shows
"[| x ∈ HFinite - Infinitesimal;
h ∈ Infinitesimal |] ==> inverse(h + x) ≈ inverse x"
done

fixes x h :: "'a::real_normed_div_algebra star"
shows
"[| x ∈ HFinite - Infinitesimal;
h ∈ Infinitesimal |] ==> inverse(x + h) - inverse x ≈ h"
apply (rule approx_trans2)
done

lemma Infinitesimal_square_iff:
fixes x :: "'a::real_normed_div_algebra star"
shows "(x ∈ Infinitesimal) = (x*x ∈ Infinitesimal)"
apply (auto intro: Infinitesimal_mult)
apply (rule ccontr, frule Infinitesimal_inverse_HFinite)
apply (frule not_Infinitesimal_not_zero)
apply (auto dest: Infinitesimal_HFinite_mult simp add: mult.assoc)
done
declare Infinitesimal_square_iff [symmetric, simp]

lemma HFinite_square_iff [simp]:
fixes x :: "'a::real_normed_div_algebra star"
shows "(x*x ∈ HFinite) = (x ∈ HFinite)"
apply (auto intro: HFinite_mult)
apply (auto dest: HInfinite_mult simp add: HFinite_HInfinite_iff)
done

lemma HInfinite_square_iff [simp]:
fixes x :: "'a::real_normed_div_algebra star"
shows "(x*x ∈ HInfinite) = (x ∈ HInfinite)"

lemma approx_HFinite_mult_cancel:
fixes a w z :: "'a::real_normed_div_algebra star"
shows "[| a: HFinite-Infinitesimal; a* w ≈ a*z |] ==> w ≈ z"
apply safe
apply (frule HFinite_inverse, assumption)
apply (drule not_Infinitesimal_not_zero)
apply (auto dest: approx_mult2 simp add: mult.assoc [symmetric])
done

lemma approx_HFinite_mult_cancel_iff1:
fixes a w z :: "'a::real_normed_div_algebra star"
shows "a: HFinite-Infinitesimal ==> (a * w ≈ a * z) = (w ≈ z)"
by (auto intro: approx_mult2 approx_HFinite_mult_cancel)

"[| x + y ∈ HInfinite; y ∈ HFinite |] ==> x ∈ HInfinite"
apply (rule ccontr)
apply (drule HFinite_HInfinite_iff [THEN iffD2])
done

"[| x ∈ HInfinite; y ∈ HFinite |] ==> x + y ∈ HInfinite"
apply (rule_tac y = "-y" in HInfinite_HFinite_add_cancel)
done

lemma HInfinite_ge_HInfinite:
"[| (x::hypreal) ∈ HInfinite; x ≤ y; 0 ≤ x |] ==> y ∈ HInfinite"
by (auto intro: HFinite_bounded simp add: HInfinite_HFinite_iff)

lemma Infinitesimal_inverse_HInfinite:
fixes x :: "'a::real_normed_div_algebra star"
shows "[| x ∈ Infinitesimal; x ≠ 0 |] ==> inverse x ∈ HInfinite"
apply (rule ccontr, drule HFinite_HInfinite_iff [THEN iffD2])
apply (auto dest: Infinitesimal_HFinite_mult2)
done

lemma HInfinite_HFinite_not_Infinitesimal_mult:
fixes x y :: "'a::real_normed_div_algebra star"
shows "[| x ∈ HInfinite; y ∈ HFinite - Infinitesimal |]
==> x * y ∈ HInfinite"
apply (rule ccontr, drule HFinite_HInfinite_iff [THEN iffD2])
apply (frule HFinite_Infinitesimal_not_zero)
apply (drule HFinite_not_Infinitesimal_inverse)
apply (safe, drule HFinite_mult)
apply (auto simp add: mult.assoc HFinite_HInfinite_iff)
done

lemma HInfinite_HFinite_not_Infinitesimal_mult2:
fixes x y :: "'a::real_normed_div_algebra star"
shows "[| x ∈ HInfinite; y ∈ HFinite - Infinitesimal |]
==> y * x ∈ HInfinite"
apply (rule ccontr, drule HFinite_HInfinite_iff [THEN iffD2])
apply (frule HFinite_Infinitesimal_not_zero)
apply (drule HFinite_not_Infinitesimal_inverse)
apply (safe, drule_tac x="inverse y" in HFinite_mult)
apply assumption
apply (auto simp add: mult.assoc [symmetric] HFinite_HInfinite_iff)
done

lemma HInfinite_gt_SReal:
"[| (x::hypreal) ∈ HInfinite; 0 < x; y ∈ ℝ |] ==> y < x"
by (auto dest!: bspec simp add: HInfinite_def abs_if order_less_imp_le)

lemma HInfinite_gt_zero_gt_one:
"[| (x::hypreal) ∈ HInfinite; 0 < x |] ==> 1 < x"
by (auto intro: HInfinite_gt_SReal)

lemma not_HInfinite_one [simp]: "1 ∉ HInfinite"
done

lemma approx_hrabs_disj: "¦x::hypreal¦ ≈ x ∨ ¦x¦ ≈ -x"
by (cut_tac x = x in hrabs_disj, auto)

by (rule_tac x1 = x in hrabs_disj [THEN disjE], auto)

done

apply (rule_tac x1 = x in hrabs_disj [THEN disjE])
done

subsection‹Proof that @{term "x ≈ y"} implies @{term"¦x¦ ≈ ¦y¦"}›

apply (simp (no_asm))
done

apply (drule approx_sym)
done

apply (blast intro!: approx_sym)
done

done

lemma Infinitesimal_approx_hrabs:
"[| x ≈ y; (x::hypreal) ∈ Infinitesimal |] ==> ¦x¦ ≈ ¦y¦"
done

lemma less_Infinitesimal_less:
"[| 0 < x;  (x::hypreal) ∉Infinitesimal;  e :Infinitesimal |] ==> e < x"
apply (rule ccontr)
apply (auto intro: Infinitesimal_zero [THEN [2] Infinitesimal_interval]
done

"[| 0 < (x::hypreal);  x ∉ Infinitesimal; u ∈ monad x |] ==> 0 < u"
apply (erule bex_Infinitesimal_iff2 [THEN iffD2, THEN bexE])
apply (drule_tac e = "-xa" in less_Infinitesimal_less, auto)
done

"[| (x::hypreal) < 0; x ∉ Infinitesimal; u ∈ monad x |] ==> u < 0"
apply (erule bex_Infinitesimal_iff [THEN iffD2, THEN bexE])
apply (cut_tac x = "-x" and e = xa in less_Infinitesimal_less, auto)
done

lemma lemma_approx_gt_zero:
"[|0 < (x::hypreal); x ∉ Infinitesimal; x ≈ y|] ==> 0 < y"

lemma lemma_approx_less_zero:
"[|(x::hypreal) < 0; x ∉ Infinitesimal; x ≈ y|] ==> y < 0"

theorem approx_hrabs: "(x::hypreal) ≈ y ==> ¦x¦ ≈ ¦y¦"
by (drule approx_hnorm, simp)

lemma approx_hrabs_zero_cancel: "¦x::hypreal¦ ≈ 0 ==> x ≈ 0"
apply (cut_tac x = x in hrabs_disj)
apply (auto dest: approx_minus)
done

"(e::hypreal) ∈ Infinitesimal ==> ¦x¦ ≈ ¦x + e¦"

"(e::hypreal) ∈ Infinitesimal ==> ¦x¦ ≈ ¦x + -e¦"

"[| (e::hypreal) ∈ Infinitesimal; e' ∈ Infinitesimal;
¦x + e¦ = ¦y + e'¦|] ==> ¦x¦ ≈ ¦y¦"
apply (drule_tac x = x in approx_hrabs_add_Infinitesimal)
apply (drule_tac x = y in approx_hrabs_add_Infinitesimal)
apply (auto intro: approx_trans2)
done

"[| (e::hypreal) ∈ Infinitesimal; e' ∈ Infinitesimal;
¦x + -e¦ = ¦y + -e'¦|] ==> ¦x¦ ≈ ¦y¦"
apply (drule_tac x = x in approx_hrabs_add_minus_Infinitesimal)
apply (drule_tac x = y in approx_hrabs_add_minus_Infinitesimal)
apply (auto intro: approx_trans2)
done

subsection ‹More @{term HFinite} and @{term Infinitesimal} Theorems›

(* interesting slightly counterintuitive theorem: necessary
for proving that an open interval is an NS open set
*)
"[| x < y;  u ∈ Infinitesimal |]
==> hypreal_of_real x + u < hypreal_of_real y"
apply (drule_tac x = "hypreal_of_real y + -hypreal_of_real x" in bspec, simp)
done

"[| x ∈ Infinitesimal; ¦hypreal_of_real r¦ < hypreal_of_real y |]
==> ¦hypreal_of_real r + x¦ < hypreal_of_real y"
apply (drule_tac x = "hypreal_of_real r" in approx_hrabs_add_Infinitesimal)
apply (drule approx_sym [THEN bex_Infinitesimal_iff2 [THEN iffD2]])
simp del: star_of_abs
done

"[| x ∈ Infinitesimal;  ¦hypreal_of_real r¦ < hypreal_of_real y |]
==> ¦x + hypreal_of_real r¦ < hypreal_of_real y"
done

"[| u ∈ Infinitesimal; v ∈ Infinitesimal;
hypreal_of_real x + u ≤ hypreal_of_real y + v |]
==> hypreal_of_real x ≤ hypreal_of_real y"
apply (simp add: linorder_not_less [symmetric], auto)
apply (drule_tac u = "v-u" in Infinitesimal_add_hypreal_of_real_less)
done

"[| u ∈ Infinitesimal; v ∈ Infinitesimal;
hypreal_of_real x + u ≤ hypreal_of_real y + v |]
==> x ≤ y"
by (blast intro: star_of_le [THEN iffD1]

lemma hypreal_of_real_less_Infinitesimal_le_zero:
"[| hypreal_of_real x < e; e ∈ Infinitesimal |] ==> hypreal_of_real x ≤ 0"
apply (rule linorder_not_less [THEN iffD1], safe)
apply (drule Infinitesimal_interval)
apply (drule_tac [4] SReal_hypreal_of_real [THEN SReal_Infinitesimal_zero], auto)
done

(*used once, in Lim/NSDERIV_inverse*)
"[| h ∈ Infinitesimal; x ≠ 0 |] ==> star_of x + h ≠ 0"
apply auto
apply (subgoal_tac "h = - star_of x", auto intro: minus_unique [symmetric])
done

lemma Infinitesimal_square_cancel [simp]:
"(x::hypreal)*x + y*y ∈ Infinitesimal ==> x*x ∈ Infinitesimal"
apply (rule Infinitesimal_interval2)
apply (rule_tac [3] zero_le_square, assumption)
apply (auto)
done

lemma HFinite_square_cancel [simp]:
"(x::hypreal)*x + y*y ∈ HFinite ==> x*x ∈ HFinite"
apply (rule HFinite_bounded, assumption)
apply (auto)
done

lemma Infinitesimal_square_cancel2 [simp]:
"(x::hypreal)*x + y*y ∈ Infinitesimal ==> y*y ∈ Infinitesimal"
apply (rule Infinitesimal_square_cancel)
apply (simp (no_asm))
done

lemma HFinite_square_cancel2 [simp]:
"(x::hypreal)*x + y*y ∈ HFinite ==> y*y ∈ HFinite"
apply (rule HFinite_square_cancel)
apply (simp (no_asm))
done

lemma Infinitesimal_sum_square_cancel [simp]:
"(x::hypreal)*x + y*y + z*z ∈ Infinitesimal ==> x*x ∈ Infinitesimal"
apply (rule Infinitesimal_interval2, assumption)
apply (rule_tac [2] zero_le_square, simp)
apply (insert zero_le_square [of y])
apply (insert zero_le_square [of z], simp del:zero_le_square)
done

lemma HFinite_sum_square_cancel [simp]:
"(x::hypreal)*x + y*y + z*z ∈ HFinite ==> x*x ∈ HFinite"
apply (rule HFinite_bounded, assumption)
apply (rule_tac [2] zero_le_square)
apply (insert zero_le_square [of y])
apply (insert zero_le_square [of z], simp del:zero_le_square)
done

lemma Infinitesimal_sum_square_cancel2 [simp]:
"(y::hypreal)*y + x*x + z*z ∈ Infinitesimal ==> x*x ∈ Infinitesimal"
apply (rule Infinitesimal_sum_square_cancel)
done

lemma HFinite_sum_square_cancel2 [simp]:
"(y::hypreal)*y + x*x + z*z ∈ HFinite ==> x*x ∈ HFinite"
apply (rule HFinite_sum_square_cancel)
done

lemma Infinitesimal_sum_square_cancel3 [simp]:
"(z::hypreal)*z + y*y + x*x ∈ Infinitesimal ==> x*x ∈ Infinitesimal"
apply (rule Infinitesimal_sum_square_cancel)
done

lemma HFinite_sum_square_cancel3 [simp]:
"(z::hypreal)*z + y*y + x*x ∈ HFinite ==> x*x ∈ HFinite"
apply (rule HFinite_sum_square_cancel)
done

"[| y ∈ monad x; 0 < hypreal_of_real e |]
==> ¦y - x¦ < hypreal_of_real e"
apply (drule bex_Infinitesimal_iff [THEN iffD2])
apply (auto dest!: InfinitesimalD)
done

"x ∈ monad (hypreal_of_real  a) ==> x ∈ HFinite"
apply (drule bex_Infinitesimal_iff2 [THEN iffD2])
apply (safe dest!: Infinitesimal_subset_HFinite [THEN subsetD])
apply (erule SReal_hypreal_of_real [THEN SReal_subset_HFinite [THEN subsetD], THEN HFinite_add])
done

lemma st_approx_self: "x ∈ HFinite ==> st x ≈ x"
apply (frule st_part_Ex, safe)
apply (rule someI2)
apply (auto intro: approx_sym)
done

lemma st_SReal: "x ∈ HFinite ==> st x ∈ ℝ"
apply (frule st_part_Ex, safe)
apply (rule someI2)
apply (auto intro: approx_sym)
done

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"
apply (frule SReal_subset_HFinite [THEN subsetD])
apply (drule (1) approx_HFinite)
apply (unfold st_def)
apply (rule some_equality)
apply (auto intro: approx_unique_real)
done

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)

"[| x ∈ ℝ; e ∈ Infinitesimal |] ==> st(x + e) = x"
apply (erule st_unique)
done

"[| x ∈ ℝ; e ∈ Infinitesimal |] ==> st(e + x) = x"
apply (erule st_unique)
done

"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"

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"
proof -
from Reals_numeral have "numeral w ∈ ℝ" .
then have "- numeral w ∈ ℝ" by simp
with st_SReal_eq show ?thesis .
qed

lemma st_0 [simp]: "st 0 = 0"

lemma st_1 [simp]: "st 1 = 1"

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

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"

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)"
apply (rule_tac c1 = "st x" in mult_left_cancel [THEN iffD1])
apply (auto simp add: st_mult [symmetric] st_not_Infinitesimal HFinite_inverse)
apply (subst right_inverse, auto)
done

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)

"[| x ∈ HFinite; y ∈ HFinite; u ∈ Infinitesimal; st x < st y |]
==> st x + u < st y"
apply (drule st_SReal)+
done

"[| x ∈ HFinite; y ∈ HFinite;
u ∈ Infinitesimal; st x ≤ st y + u
|] ==> st x ≤ st y"
done

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"
apply (subst st_0 [symmetric])
apply (rule st_le, auto)
done

lemma st_zero_ge: "[| x ≤ 0;  x ∈ HFinite |] ==> st x ≤ 0"
apply (subst st_0 [symmetric])
apply (rule st_le, auto)
done

lemma st_hrabs: "x ∈ HFinite ==> ¦st x¦ = st ¦x¦"
apply (simp add: linorder_not_le st_zero_le abs_if st_minus
linorder_not_less)
apply (auto dest!: st_zero_ge [OF order_less_imp_le])
done

subsection ‹Alternative Definitions using Free Ultrafilter›

subsubsection ‹@{term HFinite}›

lemma HFinite_FreeUltrafilterNat:
"star_n X ∈ HFinite
==> ∃u. eventually (λn. norm (X n) < u) FreeUltrafilterNat"
apply (auto simp add: HFinite_def SReal_def)
apply (rule_tac x=r in exI)
apply (simp add: hnorm_def star_of_def starfun_star_n)
done

lemma FreeUltrafilterNat_HFinite:
"∃u. eventually (λn. norm (X n) < u) FreeUltrafilterNat
==>  star_n X ∈ HFinite"
apply (auto simp add: HFinite_def mem_Rep_star_iff)
apply (rule_tac x="star_of u" in bexI)
apply (simp add: hnorm_def starfun_star_n star_of_def)
done

lemma HFinite_FreeUltrafilterNat_iff:
"(star_n X ∈ HFinite) = (∃u. eventually (λn. norm (X n) < u) FreeUltrafilterNat)"
by (blast intro!: HFinite_FreeUltrafilterNat FreeUltrafilterNat_HFinite)

subsubsection ‹@{term HInfinite}›

lemma lemma_Compl_eq: "- {n. u < norm (f n)} = {n. norm (f n) ≤ u}"
by auto

lemma lemma_Compl_eq2: "- {n. norm (f n) < u} = {n. u ≤ norm (f n)}"
by auto

lemma lemma_Int_eq1:
"{n. norm (f n) ≤ u} Int {n. u ≤ norm (f n)} = {n. norm(f n) = u}"
by auto

lemma lemma_FreeUltrafilterNat_one:
"{n. norm (f n) = u} ≤ {n. norm (f n) < u + (1::real)}"
by auto

(*-------------------------------------
Exclude this type of sets from free
ultrafilter for Infinite numbers!
-------------------------------------*)
lemma FreeUltrafilterNat_const_Finite:
"eventually (λn. norm (X n) = u) FreeUltrafilterNat ==> star_n X ∈ HFinite"
apply (rule FreeUltrafilterNat_HFinite)
apply (rule_tac x = "u + 1" in exI)
apply (auto elim: eventually_mono)
done

lemma HInfinite_FreeUltrafilterNat:
"star_n X ∈ HInfinite ==> ∀u. eventually (λn. u < norm (X n)) FreeUltrafilterNat"
apply (drule HInfinite_HFinite_iff [THEN iffD1])
apply (rule allI, drule_tac x="u + 1" in spec)
apply (auto elim: eventually_mono)
done

lemma lemma_Int_HI:
"{n. norm (Xa n) < u} Int {n. X n = Xa n} ⊆ {n. norm (X n) < (u::real)}"
by auto

lemma lemma_Int_HIa: "{n. u < norm (X n)} Int {n. norm (X n) < u} = {}"
by (auto intro: order_less_asym)

lemma FreeUltrafilterNat_HInfinite:
"∀u. eventually (λn. u < norm (X n)) FreeUltrafilterNat ==> star_n X ∈ HInfinite"
apply (rule HInfinite_HFinite_iff [THEN iffD2])
apply (safe, drule HFinite_FreeUltrafilterNat, safe)
apply (drule_tac x = u in spec)
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 show False
qed

lemma HInfinite_FreeUltrafilterNat_iff:
"(star_n X ∈ HInfinite) = (∀u. eventually (λn. u < norm (X n)) FreeUltrafilterNat)"
by (blast intro!: HInfinite_FreeUltrafilterNat FreeUltrafilterNat_HInfinite)

subsubsection ‹@{term Infinitesimal}›

lemma ball_SReal_eq: "(∀x::hypreal ∈ Reals. P x) = (∀x::real. P (star_of x))"
by (unfold SReal_def, auto)

lemma Infinitesimal_FreeUltrafilterNat:
"star_n X ∈ Infinitesimal ==> ∀u>0. eventually (λn. norm (X n) < u) 𝒰"
apply (simp add: hnorm_def starfun_star_n star_of_def)
done

lemma FreeUltrafilterNat_Infinitesimal:
"∀u>0. eventually (λn. norm (X n) < u) 𝒰 ==> star_n X ∈ Infinitesimal"
apply (simp add: hnorm_def starfun_star_n star_of_def)
done

lemma Infinitesimal_FreeUltrafilterNat_iff:
"(star_n X ∈ Infinitesimal) = (∀u>0. eventually (λn. norm (X n) < u) 𝒰)"
by (blast intro!: Infinitesimal_FreeUltrafilterNat FreeUltrafilterNat_Infinitesimal)

(*------------------------------------------------------------------------
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)))"
apply (auto simp del: of_nat_Suc)
apply (blast dest!: reals_Archimedean intro: order_less_trans)
done

lemma lemma_Infinitesimal2:
"(∀r ∈ Reals. 0 < r --> x < r) =
(∀n. x < inverse(hypreal_of_nat (Suc n)))"
apply safe
apply (drule_tac x = "inverse (hypreal_of_real (real (Suc n))) " in bspec)
apply simp_all
using less_imp_of_nat_less apply fastforce
apply (auto dest!: reals_Archimedean simp add: SReal_iff simp del: of_nat_Suc)
apply (drule star_of_less [THEN iffD2])
apply simp
apply (blast intro: order_less_trans)
done

lemma Infinitesimal_hypreal_of_nat_iff:
"Infinitesimal = {x. ∀n. hnorm x < inverse (hypreal_of_nat (Suc n))}"
done

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}"

(*-------------------------------------------
Prove that any segment is finite and hence cannot belong to FreeUltrafilterNat
-------------------------------------------*)

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

lemma finite_real_of_nat_less_real: "finite {n::nat. real n < u}"
apply (cut_tac x = u in reals_Archimedean2, safe)
apply (rule finite_real_of_nat_segment [THEN [2] finite_subset])
apply (auto dest: order_less_trans)
done

lemma lemma_real_le_Un_eq:
"{n. f n ≤ u} = {n. f n < u} Un {n. u = (f n :: real)}"
by (auto dest: order_le_imp_less_or_eq simp add: order_less_imp_le)

lemma finite_real_of_nat_le_real: "finite {n::nat. real n ≤ u}"
by (auto simp add: lemma_real_le_Un_eq lemma_finite_omega_set finite_real_of_nat_less_real)

lemma finite_rabs_real_of_nat_le_real: "finite {n::nat. ¦real n¦ ≤ u}"
done

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

lemma FreeUltrafilterNat_nat_gt_real: "eventually (λn. u < real n) FreeUltrafilterNat"
apply (rule FreeUltrafilterNat.finite')
apply (subgoal_tac "{n::nat. ¬ u < real n} = {n. real n ≤ u}")
done

(*--------------------------------------------------------------
The complement of {n. ¦real n¦ ≤ u} =
{n. u < ¦real n¦} is in FreeUltrafilterNat
by property of (free) ultrafilters
--------------------------------------------------------------*)

lemma Compl_real_le_eq: "- {n::nat. real n ≤ u} = {n. u < real n}"
by (auto dest!: order_le_less_trans simp add: linorder_not_le)

text‹@{term ω} is a member of @{term HInfinite}›

theorem HInfinite_omega [simp]: "ω ∈ HInfinite"
apply (rule FreeUltrafilterNat_HInfinite)
apply clarify
apply (rule_tac u1 = "u-1" in eventually_mono [OF FreeUltrafilterNat_nat_gt_real])
apply auto
done

(*-----------------------------------------------
Epsilon is a member of Infinitesimal
-----------------------------------------------*)

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

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

lemma epsilon_approx_zero [simp]: "ε ≈ 0"
apply (simp (no_asm) add: mem_infmal_iff [symmetric])
done

(*------------------------------------------------------------------------
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)"
apply (subst pos_less_divide_eq, assumption)
apply (subst pos_less_divide_eq)
apply simp
done

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
thus "finite {n. real (Suc n) < inverse u}"
using finite_real_of_nat_less_real [of "inverse u - 1"] by auto
qed

lemma lemma_real_le_Un_eq2:
"{n. u ≤ inverse(real(Suc n))} =
{n. u < inverse(real(Suc n))} Un {n. u = inverse(real(Suc n))}"
by (auto dest: order_le_imp_less_or_eq simp add: order_less_imp_le)

lemma finite_inverse_real_of_posnat_ge_real:
"0 < u ==> finite {n. u ≤ inverse(real(Suc n))}"
by (auto simp add: lemma_real_le_Un_eq2 lemma_finite_epsilon_set finite_inverse_real_of_posnat_gt_real
simp del: of_nat_Suc)

lemma inverse_real_of_posnat_ge_real_FreeUltrafilterNat:
"0 < u ==> ¬ eventually (λn. u ≤ inverse(real(Suc n))) FreeUltrafilterNat"
by (blast intro!: FreeUltrafilterNat.finite finite_inverse_real_of_posnat_ge_real)

(*--------------------------------------------------------------
The complement of  {n. u ≤ inverse(real(Suc n))} =
{n. inverse(real(Suc n)) < u} is in FreeUltrafilterNat
by property of (free) ultrafilters
--------------------------------------------------------------*)
lemma Compl_le_inverse_eq:
"- {n. u ≤ inverse(real(Suc n))} = {n. inverse(real(Suc n)) < u}"
by (auto dest!: order_le_less_trans simp add: linorder_not_le)

lemma FreeUltrafilterNat_inverse_real_of_posnat:
"0 < u ==> eventually (λn. inverse(real(Suc n)) < u) FreeUltrafilterNat"
by (drule inverse_real_of_posnat_ge_real_FreeUltrafilterNat)

text‹Example of an hypersequence (i.e. an extended standard sequence)
whose term with an hypernatural suffix is an infinitesimal i.e.
the whn'nth term of the hypersequence is a member of Infinitesimal›

lemma SEQ_Infinitesimal:
"( *f* (%n::nat. inverse(real(Suc n)))) whn : Infinitesimal"
by (simp add: hypnat_omega_def starfun_star_n star_n_inverse Infinitesimal_FreeUltrafilterNat_iff
FreeUltrafilterNat_inverse_real_of_posnat del: of_nat_Suc)

text‹Example where we get a hyperreal from a real sequence
for which a particular property holds. The theorem is
used in proofs about equivalence of nonstandard and
standard neighbourhoods. Also used for equivalence of
nonstandard ans standard definitions of pointwise
limit.›

(*-----------------------------------------------------
|X(n) - x| < 1/n ==> [<X n>] - hypreal_of_real x| ∈ Infinitesimal
-----------------------------------------------------*)
lemma real_seq_to_hypreal_Infinitesimal:
"∀n. norm(X n - x) < inverse(real(Suc n))
==> star_n X - star_of x ∈ Infinitesimal"
unfolding star_n_diff star_of_def Infinitesimal_FreeUltrafilterNat_iff star_n_inverse
by (auto dest!: FreeUltrafilterNat_inverse_real_of_posnat
intro: order_less_trans elim!: eventually_mono)

lemma real_seq_to_hypreal_approx:
"∀n. norm(X n - x) < inverse(real(Suc n))
==> star_n X ≈ star_of x"
by (metis bex_Infinitesimal_iff real_seq_to_hypreal_Infinitesimal)

lemma real_seq_to_hypreal_approx2:
"∀n. norm(x - X n) < inverse(real(Suc n))
==> star_n X ≈ star_of x"
by (metis norm_minus_commute real_seq_to_hypreal_approx)

lemma real_seq_to_hypreal_Infinitesimal2:
"∀n. norm(X n - Y n) < inverse(real(Suc n))
==> star_n X - star_n Y ∈ Infinitesimal"
unfolding Infinitesimal_FreeUltrafilterNat_iff star_n_diff
by (auto dest!: FreeUltrafilterNat_inverse_real_of_posnat
intro: order_less_trans elim!: eventually_mono)

end