Theory NSA
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"
definition st :: "hypreal ⇒ hypreal"
where "st = (λx. SOME 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}"
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 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 K (K 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)
text‹Existence of real and Standard Part Theorem.›
lemma lemma_st_part_Ex: "x ∈ HFinite ⟹ ∃t∈Reals. ∀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 ⟹ ∃t∈Reals. 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
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 \<^term>‹x ≈ 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 \<^term>‹HFinite› and \<^term>‹Infinitesimal› 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 ‹\<^term>‹HFinite››
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 ‹\<^term>‹HInfinite››
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 ‹\<^term>‹Infinitesimal››
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 \<^term>‹HInfinite›.›
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)"
by (smt (verit, best) assms ceiling_less_cancel ceiling_of_nat inverse_inverse_eq inverse_le_iff_le)
then show ?thesis
apply (auto simp add: finite_nat_set_iff_bounded_le)
by (meson assms inverse_positive_iff_positive le_nat_iff less_imp_le zero_less_ceiling)
qed
lemma inverse_real_of_posnat_ge_real_FreeUltrafilterNat:
"0 < u ⟹ ¬ eventually (λn. u ≤ inverse(real(Suc n))) 𝒰"
by (blast intro!: FreeUltrafilterNat.finite finite_inverse_real_of_posnat_ge_real)
lemma FreeUltrafilterNat_inverse_real_of_posnat:
"0 < u ⟹ eventually (λn. inverse(real(Suc n)) < u) 𝒰"
by (drule inverse_real_of_posnat_ge_real_FreeUltrafilterNat)
(simp add: FreeUltrafilterNat.eventually_not_iff not_le[symmetric])
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.›
text ‹‹|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