# Theory NSA

Up to index of Isabelle/HOL/HOL-NSA

theory NSA
imports HyperDef
`(*  Title:      HOL/NSA/NSA.thy    Author:     Jacques D. Fleuriot, University of Cambridge    Author:     Lawrence C Paulson, University of Cambridge*)header{*Infinite Numbers, Infinitesimals, Infinitely Close Relation*}theory NSAimports HyperDef RCompletebegindefinition  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 ∈ Reals & 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}"notation (xsymbols)  approx  (infixl "≈" 50)notation (HTML output)  approx  (infixl "≈" 50)lemma SReal_def: "Reals == {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_inverse_zero} star.   hnorm (inverse a) = inverse (hnorm a)"by transfer (rule norm_inverse)lemma hnorm_divide:  "!!a b::'a::{real_normed_field, field_inverse_zero} 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"apply (simp only: hnorm_scaleHR)apply (simp add: mult_strict_mono')donesubsection{*Closure Laws for the Standard Reals*}lemma Reals_minus_iff [simp]: "(-x ∈ Reals) = (x ∈ Reals)"apply autoapply (drule Reals_minus, auto)donelemma Reals_add_cancel: "[|x + y ∈ Reals; y ∈ Reals|] ==> x ∈ Reals"by (drule (1) Reals_diff, simp)lemma SReal_hrabs: "(x::hypreal) ∈ Reals ==> abs x ∈ Reals"by (simp add: Reals_eq_Standard)lemma SReal_hypreal_of_real [simp]: "hypreal_of_real x ∈ Reals"by (simp add: Reals_eq_Standard)lemma SReal_divide_numeral: "r ∈ Reals ==> r/(numeral w::hypreal) ∈ Reals"by simptext{*epsilon is not in Reals because it is an infinitesimal*}lemma SReal_epsilon_not_mem: "epsilon ∉ Reals"apply (simp add: SReal_def)apply (auto simp add: hypreal_of_real_not_eq_epsilon [THEN not_sym])donelemma SReal_omega_not_mem: "omega ∉ Reals"apply (simp add: SReal_def)apply (auto simp add: hypreal_of_real_not_eq_omega [THEN not_sym])donelemma SReal_UNIV_real: "{x. hypreal_of_real x ∈ Reals} = (UNIV::real set)"by simplemma SReal_iff: "(x ∈ Reals) = (∃y. x = hypreal_of_real y)"by (simp add: SReal_def)lemma hypreal_of_real_image: "hypreal_of_real `(UNIV::real set) = Reals"by (simp add: Reals_eq_Standard Standard_def)lemma inv_hypreal_of_real_image: "inv hypreal_of_real ` Reals = UNIV"apply (auto simp add: SReal_def)apply (rule inj_star_of [THEN inv_f_f, THEN subst], blast)donelemma SReal_hypreal_of_real_image:      "[| ∃x. x: P; P ⊆ Reals |] ==> ∃Q. P = hypreal_of_real ` Q"by (simp add: SReal_def image_def, blast)lemma SReal_dense:     "[| (x::hypreal) ∈ Reals; y ∈ Reals;  x<y |] ==> ∃r ∈ Reals. x<r & r<y"apply (auto simp add: SReal_def)apply (drule dense, auto)donetext{*Completeness of Reals, but both lemmas are unused.*}lemma SReal_sup_lemma:     "P ⊆ Reals ==> ((∃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 ⊆ Reals; ∃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)donesubsection{* Set of Finite Elements is a Subring of the Extended Reals*}lemma HFinite_add: "[|x ∈ HFinite; y ∈ HFinite|] ==> (x+y) ∈ HFinite"apply (simp add: HFinite_def)apply (blast intro!: Reals_add hnorm_add_less)donelemma HFinite_mult:  fixes x y :: "'a::real_normed_algebra star"  shows "[|x ∈ HFinite; y ∈ HFinite|] ==> x*y ∈ HFinite"apply (simp add: HFinite_def)apply (blast intro!: Reals_mult hnorm_mult_less)donelemma HFinite_scaleHR:  "[|x ∈ HFinite; y ∈ HFinite|] ==> scaleHR x y ∈ HFinite"apply (simp add: HFinite_def)apply (blast intro!: Reals_mult hnorm_scaleHR_less)donelemma HFinite_minus_iff: "(-x ∈ HFinite) = (x ∈ HFinite)"by (simp add: HFinite_def)lemma HFinite_star_of [simp]: "star_of x ∈ HFinite"apply (simp add: HFinite_def)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)donelemma SReal_subset_HFinite: "(Reals::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]: "(abs (x::hypreal) ∈ HFinite) = (x ∈ HFinite)"by (simp add: HFinite_def)lemma HFinite_hnorm_iff [iff]:  "(hnorm (x::hypreal) ∈ HFinite) = (x ∈ HFinite)"by (simp add: HFinite_def)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)donelemma 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 simp add: linorder_not_le)apply (auto intro: order_le_less_trans simp add: abs_if HFinite_def)donesubsection{* Set of Infinitesimals is a Subring of the Hyperreals*}lemma InfinitesimalI:  "(!!r. [|r ∈ \<real>; 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 hypreal_sum_of_halves: "x/(2::hypreal) + x/(2::hypreal) = x"by autolemma Infinitesimal_add:     "[| 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)donelemma 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]:  "(abs (x::hypreal) ∈ Infinitesimal) = (x ∈ Infinitesimal)"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"by (simp add: diff_minus Infinitesimal_add)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)apply (simp_all add: InfinitesimalD)donelemma 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 (simp add: InfinitesimalD Reals_divide)apply assumptionapply (simp only: divide_pos_pos)apply (erule order_le_less_trans [OF hnorm_ge_zero])donelemma Infinitesimal_HFinite_scaleHR:  "[| x ∈ Infinitesimal; y ∈ HFinite |] ==> scaleHR x y ∈ Infinitesimal"apply (rule InfinitesimalI)apply (drule HFiniteD, clarify)apply (drule InfinitesimalD)apply (simp add: hnorm_scaleHR)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 (simp only: divide_pos_pos)apply (erule order_le_less_trans [OF hnorm_ge_zero])donelemma 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 assumptionapply (simp add: InfinitesimalD Reals_divide)apply (simp only: divide_pos_pos)apply (erule order_le_less_trans [OF hnorm_ge_zero])donelemma 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 add: Reals_eq_Standard)apply (simp add: divide_pos_pos)apply (simp add: hnorm_scaleR pos_less_divide_eq mult_commute)donelemma 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 simpdonelemma 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 (simp add: nonzero_hnorm_inverse)apply (simp add: HInfinite_def Reals_inverse)apply assumptionapply (clarify, simp add: Compl_HFinite [symmetric])donelemma HInfiniteI: "(!!r. r ∈ \<real> ==> r < hnorm x) ==> x ∈ HInfinite"by (simp add: HInfinite_def)lemma HInfiniteD: "[|x ∈ HInfinite; r ∈ \<real>|] ==> r < hnorm x"by (simp add: HInfinite_def)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)apply (simp_all add: HInfiniteD)donelemma hypreal_add_zero_less_le_mono: "[|r < x; (0::hypreal) ≤ y|] ==> r < x+y"by (auto dest: add_less_le_mono)lemma HInfinite_add_ge_zero:     "[|(x::hypreal) ∈ HInfinite; 0 ≤ y; 0 ≤ x|] ==> (x + y): HInfinite"by (auto intro!: hypreal_add_zero_less_le_mono        simp add: abs_if add_commute add_nonneg_nonneg HInfinite_def)lemma HInfinite_add_ge_zero2:     "[|(x::hypreal) ∈ HInfinite; 0 ≤ y; 0 ≤ x|] ==> (y + x): HInfinite"by (auto intro!: HInfinite_add_ge_zero simp add: add_commute)lemma HInfinite_add_gt_zero:     "[|(x::hypreal) ∈ HInfinite; 0 < y; 0 < x|] ==> (x + y): HInfinite"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::hypreal) ∈ HInfinite; y ≤ 0; x ≤ 0|] ==> (x + y): HInfinite"apply (drule HInfinite_minus_iff [THEN iffD2])apply (rule HInfinite_minus_iff [THEN iffD1])apply (auto intro: HInfinite_add_ge_zero)donelemma HInfinite_add_lt_zero:     "[|(x::hypreal) ∈ HInfinite; y < 0; x < 0|] ==> (x + y): HInfinite"by (blast intro: HInfinite_add_le_zero order_less_imp_le)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"by (auto intro: HFinite_mult HFinite_add)lemma not_Infinitesimal_not_zero: "x ∉ Infinitesimal ==> x ≠ 0"by autolemma not_Infinitesimal_not_zero2: "x ∈ HFinite - Infinitesimal ==> x ≠ 0"by autolemma HFinite_diff_Infinitesimal_hrabs:  "(x::hypreal) ∈ HFinite - Infinitesimal ==> abs x ∈ HFinite - Infinitesimal"by blastlemma 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; abs (x::hypreal) ≤ e |] ==> x ∈ Infinitesimal"by (erule hnorm_le_Infinitesimal, simp)lemma hrabs_less_Infinitesimal:      "[| e ∈ Infinitesimal; abs (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 |] ==> abs (x pow N) ≤ abs x"apply (unfold Infinitesimal_def)apply (auto intro!: hyperpow_Suc_le_self2           simp add: hyperpow_hrabs [symmetric] hypnat_gt_zero_iff2 abs_ge_zero)donelemma Infinitesimal_hyperpow:     "[| (x::hypreal) ∈ Infinitesimal; 0 < N |] ==> x pow N ∈ Infinitesimal"apply (rule hrabs_le_Infinitesimal)apply (rule_tac [2] lemma_Infinitesimal_hyperpow, auto)donelemma 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"by (simp add: hrealpow_hyperpow_Infinitesimal_iff Infinitesimal_hyperpow)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 (drule mp, blast intro: mult_pos_pos)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))donelemma 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)donelemma HFinite_Infinitesimal_not_zero: "x ∈ HFinite-Infinitesimal ==> x ≠ 0"by blastlemma 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 clarifyapply (blast dest: HFinite_mult not_Infinitesimal_mult)donelemma Infinitesimal_subset_HFinite:      "Infinitesimal ⊆ HFinite"apply (simp add: Infinitesimal_def HFinite_def, auto)apply (rule_tac x = 1 in bexI, auto)donelemma 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)"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 diff_minus add_commute)lemma approx_refl [iff]: "x @= x"by (simp add: approx_def Infinitesimal_def)lemma hypreal_minus_distrib1: "-(y + -(x::'a::ab_group_add)) = x + -y"by (simp add: add_commute)lemma approx_sym: "x @= y ==> y @= x"apply (simp add: approx_def)apply (drule Infinitesimal_minus_iff [THEN iffD2])apply simpdonelemma approx_trans: "[| x @= y; y @= z |] ==> x @= z"apply (simp add: approx_def)apply (drule (1) Infinitesimal_add)apply (simp add: diff_minus)donelemma 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" | "neg_numeral w @= r") ={*  let val rule = @{thm approx_reorient} RS eq_reflection      fun proc phi ss ct = case term_of ct of          _ \$ t \$ u => if can HOLogic.dest_number u then NONE            else if can HOLogic.dest_number t then SOME rule else NONE        | _ => NONE  in proc end*}lemma Infinitesimal_approx_minus: "(x-y ∈ Infinitesimal) = (x @= y)"by (simp add: approx_minus_iff [symmetric] mem_infmal_iff)lemma approx_monad_iff: "(x @= y) = (monad(x)=monad(y))"apply (simp add: monad_def)apply (auto dest: approx_sym elim!: approx_trans equalityCE)donelemma Infinitesimal_approx:     "[| x ∈ Infinitesimal; y ∈ Infinitesimal |] ==> x @= y"apply (simp add: mem_infmal_iff)apply (blast intro: approx_trans approx_sym)donelemma 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" .qedlemma approx_minus: "a @= b ==> -a @= -b"apply (rule approx_minus_iff [THEN iffD2, THEN approx_sym])apply (drule approx_minus_iff [THEN iffD1])apply (simp add: add_commute diff_minus)donelemma 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"by (simp only: diff_minus approx_add approx_minus)lemma approx_mult1:  fixes a b c :: "'a::real_normed_algebra star"  shows "[| a @= b; c: HFinite|] ==> a*c @= b*c"by (simp add: approx_def Infinitesimal_HFinite_mult              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"by (simp add: approx_def Infinitesimal_HFinite_mult2              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"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"apply (rule bex_Infinitesimal_iff [THEN iffD1])apply (drule Infinitesimal_minus_iff [THEN iffD2])apply (auto simp add: add_assoc [symmetric])donelemma Infinitesimal_add_approx_self: "y ∈ Infinitesimal ==> x @= x + y"apply (rule bex_Infinitesimal_iff [THEN iffD1])apply (drule Infinitesimal_minus_iff [THEN iffD2])apply (auto simp add: add_assoc [symmetric])donelemma 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"apply (drule_tac x = x in Infinitesimal_add_approx_self [THEN approx_sym])apply (erule approx_trans3 [THEN approx_sym], assumption)donelemma Infinitesimal_add_right_cancel:     "[| 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 (simp add: add_commute)apply (erule approx_sym)donelemma approx_add_left_cancel: "d + b  @= d + c ==> b @= c"apply (drule approx_minus_iff [THEN iffD1])apply (simp add: approx_minus_iff [symmetric] add_ac)donelemma approx_add_right_cancel: "b + d @= c + d ==> b @= c"apply (rule approx_add_left_cancel)apply (simp add: add_commute)donelemma approx_add_mono1: "b @= c ==> d + b @= d + c"apply (rule approx_minus_iff [THEN iffD2])apply (simp add: approx_minus_iff [symmetric] add_ac)donelemma 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"apply (drule bex_Infinitesimal_iff2 [THEN iffD2], safe)apply (drule Infinitesimal_subset_HFinite [THEN subsetD, THEN HFinite_minus_iff [THEN iffD2]])apply (drule HFinite_add)apply (auto simp add: add_assoc)donelemma 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)donelemma 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])donelemma 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"apply (rule approx_trans)apply (rule_tac [2] approx_scaleR2)apply (rule approx_scaleR1)prefer 2 apply (blast intro: approx_HFinite approx_sym, auto)donelemma 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) ∈ Reals; 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])donelemma approx_mult_SReal1: "[| (a::hypreal) ∈ Reals; x @= 0 |] ==> x*a @= 0"by (auto dest: SReal_subset_HFinite [THEN subsetD] approx_mult1)lemma approx_mult_SReal2: "[| (a::hypreal) ∈ Reals; 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) ∈ Reals; 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) ∈ Reals; 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])donelemma approx_SReal_mult_cancel_iff1 [simp]:     "[| (a::hypreal) ∈ Reals; 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)donelemma 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)qedsubsection{* Zero is the Only Infinitesimal that is also a Real*}lemma Infinitesimal_less_SReal:     "[| (x::hypreal) ∈ Reals; y ∈ Infinitesimal; 0 < x |] ==> y < x"apply (simp add: Infinitesimal_def)apply (rule abs_ge_self [THEN order_le_less_trans], auto)donelemma 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) ∈ Reals|] ==> y ∉ Infinitesimal"apply (simp add: Infinitesimal_def)apply (auto simp add: abs_if)donelemma SReal_minus_not_Infinitesimal:     "[| y < 0;  (y::hypreal) ∈ Reals |] ==> y ∉ Infinitesimal"apply (subst Infinitesimal_minus_iff [symmetric])apply (rule SReal_not_Infinitesimal, auto)donelemma SReal_Int_Infinitesimal_zero: "Reals Int Infinitesimal = {0::hypreal}"apply autoapply (cut_tac x = x and y = 0 in linorder_less_linear)apply (blast dest: SReal_not_Infinitesimal SReal_minus_not_Infinitesimal)donelemma SReal_Infinitesimal_zero:  "[| (x::hypreal) ∈ Reals; x ∈ Infinitesimal|] ==> x = 0"by (cut_tac SReal_Int_Infinitesimal_zero, blast)lemma SReal_HFinite_diff_Infinitesimal:     "[| (x::hypreal) ∈ Reals; 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 (auto simp add: Infinitesimal_def)apply (drule_tac x="hnorm (star_of x)" in bspec)apply (simp add: SReal_def)apply (rule_tac x="norm x" in exI, simp)apply simpdonelemma star_of_HFinite_diff_Infinitesimal:     "x ≠ 0 ==> star_of x ∈ HFinite - Infinitesimal"by simplemma 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 simpdonelemma approx_SReal_not_zero:  "[| (y::hypreal) ∈ Reals; 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)donelemma HFinite_diff_Infinitesimal_approx:     "[| x @= y; y ∈ HFinite - Infinitesimal |]      ==> x ∈ HFinite - Infinitesimal"apply (auto intro: approx_sym [THEN [2] approx_HFinite]            simp add: mem_infmal_iff)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)apply (simp add: divide_inverse mult_assoc)donelemma Infinitesimal_SReal_divide:   "[| (x::hypreal) ∈ Infinitesimal; y ∈ Reals |] ==> x/y ∈ Infinitesimal"apply (simp add: divide_inverse)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 safeapply (simp add: approx_def)apply (simp only: star_of_diff [symmetric])apply (simp only: star_of_Infinitesimal_iff_0)apply simpdonelemma SReal_approx_iff:  "[|(x::hypreal) ∈ Reals; y ∈ Reals|] ==> (x @= y) = (x = y)"apply autoapply (simp add: approx_def)apply (drule (1) Reals_diff)apply (drule (1) SReal_Infinitesimal_zero)apply simpdonelemma 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)"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::hypreal) ∈ Reals; s ∈ Reals; 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 (Reals) (hypreal_of_real ` Q) (hypreal_of_real Y)) =       (isUb (UNIV :: real set) Q Y)"by (simp add: isUb_def setle_def)lemma hypreal_of_real_isLub1:     "isLub Reals (hypreal_of_real ` Q) (hypreal_of_real Y)      ==> isLub (UNIV :: real set) Q Y"apply (simp add: isLub_def leastP_def)apply (auto intro: hypreal_of_real_isUb_iff [THEN iffD2]            simp add: hypreal_of_real_isUb_iff setge_def)donelemma hypreal_of_real_isLub2:      "isLub (UNIV :: real set) Q Y       ==> isLub Reals (hypreal_of_real ` Q) (hypreal_of_real Y)"apply (simp add: isLub_def leastP_def)apply (auto simp add: hypreal_of_real_isUb_iff setge_def)apply (frule_tac x2 = x in isUbD2a [THEN SReal_iff [THEN iffD1], THEN exE]) prefer 2 apply assumptionapply (drule_tac x = xa in spec)apply (auto simp add: hypreal_of_real_isUb_iff)donelemma hypreal_of_real_isLub_iff:     "(isLub Reals (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 Reals P Y ==> ∃Yo. isUb Reals P (hypreal_of_real Yo)"by (auto simp add: SReal_iff isUb_def)lemma lemma_isLub_hypreal_of_real:     "isLub Reals P Y ==> ∃Yo. isLub Reals 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 Reals P (hypreal_of_real Yo) ==> ∃Y. isLub Reals P Y"by (auto simp add: isLub_def leastP_def isUb_def)lemma SReal_complete:     "[| P ⊆ Reals;  ∃x. x ∈ P;  ∃Y. isUb Reals P Y |]      ==> ∃t::hypreal. isLub Reals 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            simp add: hypreal_of_real_isLub_iff hypreal_of_real_isUb_iff)done(* lemma about lubs *)lemma hypreal_isLub_unique:     "[| isLub R S x; isLub R S y |] ==> x = (y::hypreal)"apply (frule isLub_isUb)apply (frule_tac x = y in isLub_isUb)apply (blast intro!: order_antisym dest!: isLub_le_isUb)donelemma lemma_st_part_ub:     "(x::hypreal) ∈ HFinite ==> ∃u. isUb Reals {s. s ∈ Reals & s < x} u"apply (drule HFiniteD, safe)apply (rule exI, rule isUbI)apply (auto intro: setleI isUbI simp add: abs_less_iff)donelemma lemma_st_part_nonempty:  "(x::hypreal) ∈ HFinite ==> ∃y. y ∈ {s. s ∈ Reals & s < x}"apply (drule HFiniteD, safe)apply (drule Reals_minus)apply (rule_tac x = "-t" in exI)apply (auto simp add: abs_less_iff)donelemma lemma_st_part_subset: "{s. s ∈ Reals & s < x} ⊆ Reals"by autolemma lemma_st_part_lub:     "(x::hypreal) ∈ HFinite ==> ∃t. isLub Reals {s. s ∈ Reals & s < x} t"by (blast intro!: SReal_complete lemma_st_part_ub lemma_st_part_nonempty lemma_st_part_subset)lemma lemma_hypreal_le_left_cancel: "((t::hypreal) + r ≤ t) = (r ≤ 0)"apply safeapply (drule_tac c = "-t" in add_left_mono)apply (drule_tac [2] c = t in add_left_mono)apply (auto simp add: add_assoc [symmetric])donelemma lemma_st_part_le1:     "[| (x::hypreal) ∈ HFinite;  isLub Reals {s. s ∈ Reals & s < x} t;         r ∈ Reals;  0 < r |] ==> x ≤ t + r"apply (frule isLubD1a)apply (rule ccontr, drule linorder_not_le [THEN iffD2])apply (drule (1) Reals_add)apply (drule_tac y = "r + t" in isLubD1 [THEN setleD], auto)donelemma hypreal_setle_less_trans:     "[| S *<= (x::hypreal); x < y |] ==> S *<= y"apply (simp add: setle_def)apply (auto dest!: bspec order_le_less_trans intro: order_less_imp_le)donelemma hypreal_gt_isUb:     "[| isUb R S (x::hypreal); x < y; y ∈ R |] ==> isUb R S y"apply (simp add: isUb_def)apply (blast intro: hypreal_setle_less_trans)donelemma lemma_st_part_gt_ub:     "[| (x::hypreal) ∈ HFinite; x < y; y ∈ Reals |]      ==> isUb Reals {s. s ∈ Reals & 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)apply (auto simp add: add_assoc [symmetric])donelemma lemma_st_part_le2:     "[| (x::hypreal) ∈ HFinite;         isLub Reals {s. s ∈ Reals & s < x} t;         r ∈ Reals; 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)donelemma lemma_st_part1a:     "[| (x::hypreal) ∈ HFinite;         isLub Reals {s. s ∈ Reals & s < x} t;         r ∈ Reals; 0 < r |]      ==> x + -t ≤ r"apply (subgoal_tac "x ≤ t+r") apply (auto intro: lemma_st_part_le1)donelemma lemma_st_part2a:     "[| (x::hypreal) ∈ HFinite;         isLub Reals {s. s ∈ Reals & s < x} t;         r ∈ Reals;  0 < r |]      ==> -(x + -t) ≤ r"apply (subgoal_tac "(t + -r ≤ x)") apply (auto intro: lemma_st_part_le2)donelemma lemma_SReal_ub:     "(x::hypreal) ∈ Reals ==> isUb Reals {s. s ∈ Reals & s < x} x"by (auto intro: isUbI setleI order_less_imp_le)lemma lemma_SReal_lub:     "(x::hypreal) ∈ Reals ==> isLub Reals {s. s ∈ Reals & 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)donelemma lemma_st_part_not_eq1:     "[| (x::hypreal) ∈ HFinite;         isLub Reals {s. s ∈ Reals & s < x} t;         r ∈ Reals; 0 < r |]      ==> x + -t ≠ r"apply autoapply (frule isLubD1a [THEN Reals_minus])apply (drule Reals_add_cancel, assumption)apply (drule_tac x = x in lemma_SReal_lub)apply (drule hypreal_isLub_unique, assumption, auto)donelemma lemma_st_part_not_eq2:     "[| (x::hypreal) ∈ HFinite;         isLub Reals {s. s ∈ Reals & s < x} t;         r ∈ Reals; 0 < r |]      ==> -(x + -t) ≠ r"apply (auto)apply (frule isLubD1a)apply (drule Reals_add_cancel, assumption)apply (drule_tac a = "-x" in Reals_minus, simp)apply (drule_tac x = x in lemma_SReal_lub)apply (drule hypreal_isLub_unique, assumption, auto)donelemma lemma_st_part_major:     "[| (x::hypreal) ∈ HFinite;         isLub Reals {s. s ∈ Reals & s < x} t;         r ∈ Reals; 0 < r |]      ==> abs (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 dest: lemma_st_part_not_eq1 lemma_st_part_not_eq2 simp add: abs_less_iff)donelemma lemma_st_part_major2:     "[| (x::hypreal) ∈ HFinite; isLub Reals {s. s ∈ Reals & s < x} t |]      ==> ∀r ∈ Reals. 0 < r --> abs (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 --> abs (x - t) < r"apply (frule lemma_st_part_lub, safe)apply (frule isLubD1a)apply (blast dest: lemma_st_part_major2)donelemma st_part_Ex:     "(x::hypreal) ∈ HFinite ==> ∃t ∈ Reals. x @= t"apply (simp add: approx_def Infinitesimal_def)apply (drule lemma_st_part_Ex, auto)donetext{*There is a unique real infinitely close*}lemma st_part_Ex1: "x ∈ HFinite ==> EX! t::hypreal. t ∈ Reals & 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)donesubsection{* Finite, Infinite and Infinitesimal*}lemma HFinite_Int_HInfinite_empty [simp]: "HFinite Int HInfinite = {}"apply (simp add: HFinite_def HInfinite_def)apply (auto dest: order_less_trans)donelemma 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 autoqedlemma 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)donelemma 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:  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            simp add: nonzero_inverse_inverse_eq)donelemma 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])donelemma 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)apply (simp add: not_Infinitesimal_not_zero right_inverse)donelemma 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]lemma inverse_add_Infinitesimal_approx:  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)donelemma inverse_add_Infinitesimal_approx2:  fixes x h :: "'a::real_normed_div_algebra star"  shows     "[| x ∈ HFinite - Infinitesimal;         h ∈ Infinitesimal |] ==> inverse(h + x) @= inverse x"apply (rule add_commute [THEN subst])apply (blast intro: inverse_add_Infinitesimal_approx)donelemma inverse_add_Infinitesimal_approx_Infinitesimal:  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)apply (auto intro: inverse_add_Infinitesimal_approx             simp add: mem_infmal_iff approx_minus_iff [symmetric])donelemma 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)donedeclare 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)donelemma HInfinite_square_iff [simp]:  fixes x :: "'a::real_normed_div_algebra star"  shows "(x*x ∈ HInfinite) = (x ∈ HInfinite)"by (auto simp add: HInfinite_HFinite_iff)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 safeapply (frule HFinite_inverse, assumption)apply (drule not_Infinitesimal_not_zero)apply (auto dest: approx_mult2 simp add: mult_assoc [symmetric])donelemma 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)lemma HInfinite_HFinite_add_cancel:     "[| x + y ∈ HInfinite; y ∈ HFinite |] ==> x ∈ HInfinite"apply (rule ccontr)apply (drule HFinite_HInfinite_iff [THEN iffD2])apply (auto dest: HFinite_add simp add: HInfinite_HFinite_iff)donelemma HInfinite_HFinite_add:     "[| x ∈ HInfinite; y ∈ HFinite |] ==> x + y ∈ HInfinite"apply (rule_tac y = "-y" in HInfinite_HFinite_add_cancel)apply (auto simp add: add_assoc HFinite_minus_iff)donelemma 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)donelemma 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)donelemma 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 assumptionapply (auto simp add: mult_assoc [symmetric] HFinite_HInfinite_iff)donelemma HInfinite_gt_SReal:  "[| (x::hypreal) ∈ HInfinite; 0 < x; y ∈ Reals |] ==> 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"apply (simp (no_asm) add: HInfinite_HFinite_iff)donelemma approx_hrabs_disj: "abs (x::hypreal) @= x | abs x @= -x"by (cut_tac x = x in hrabs_disj, auto)subsection{*Theorems about Monads*}lemma monad_hrabs_Un_subset: "monad (abs x) ≤ monad(x::hypreal) Un monad(-x)"by (rule_tac x1 = x in hrabs_disj [THEN disjE], auto)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)"apply (simp (no_asm) add: Infinitesimal_monad_zero_iff [symmetric])donelemma monad_zero_hrabs_iff: "((x::hypreal) ∈ monad 0) = (abs x ∈ monad 0)"apply (rule_tac x1 = x in hrabs_disj [THEN disjE])apply (auto simp add: monad_zero_minus_iff [symmetric])donelemma 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"apply (simp (no_asm))apply (simp add: approx_monad_iff)donelemma approx_subset_monad2: "x @= y ==> {x,y} ≤ monad y"apply (drule approx_sym)apply (fast dest: approx_subset_monad)donelemma 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"apply (simp add: monad_def)apply (blast intro!: approx_sym)donelemma approx_mem_monad_zero: "[| x @= y;x ∈ monad 0 |] ==> y ∈ monad 0"apply (drule mem_monad_approx)apply (fast intro: approx_mem_monad approx_trans)donelemma Infinitesimal_approx_hrabs:     "[| x @= y; (x::hypreal) ∈ Infinitesimal |] ==> abs x @= abs y"apply (drule Infinitesimal_monad_zero_iff [THEN iffD1])apply (blast intro: approx_mem_monad_zero monad_zero_hrabs_iff [THEN iffD1] mem_monad_approx approx_trans3)donelemma less_Infinitesimal_less:     "[| 0 < x;  (x::hypreal) ∉Infinitesimal;  e :Infinitesimal |] ==> e < x"apply (rule ccontr)apply (auto intro: Infinitesimal_zero [THEN [2] Infinitesimal_interval]             dest!: order_le_imp_less_or_eq simp add: linorder_not_less)donelemma Ball_mem_monad_gt_zero:     "[| 0 < (x::hypreal);  x ∉ Infinitesimal; u ∈ monad x |] ==> 0 < u"apply (drule mem_monad_approx [THEN approx_sym])apply (erule bex_Infinitesimal_iff2 [THEN iffD2, THEN bexE])apply (drule_tac e = "-xa" in less_Infinitesimal_less, auto)donelemma Ball_mem_monad_less_zero:     "[| (x::hypreal) < 0; x ∉ Infinitesimal; u ∈ monad x |] ==> u < 0"apply (drule mem_monad_approx [THEN approx_sym])apply (erule bex_Infinitesimal_iff [THEN iffD2, THEN bexE])apply (cut_tac x = "-x" and e = xa in less_Infinitesimal_less, auto)donelemma lemma_approx_gt_zero:     "[|0 < (x::hypreal); x ∉ Infinitesimal; x @= y|] ==> 0 < y"by (blast dest: Ball_mem_monad_gt_zero approx_subset_monad)lemma lemma_approx_less_zero:     "[|(x::hypreal) < 0; x ∉ Infinitesimal; x @= y|] ==> y < 0"by (blast dest: Ball_mem_monad_less_zero approx_subset_monad)theorem approx_hrabs: "(x::hypreal) @= y ==> abs x @= abs y"by (drule approx_hnorm, simp)lemma approx_hrabs_zero_cancel: "abs(x::hypreal) @= 0 ==> x @= 0"apply (cut_tac x = x in hrabs_disj)apply (auto dest: approx_minus)donelemma approx_hrabs_add_Infinitesimal:  "(e::hypreal) ∈ Infinitesimal ==> abs x @= abs(x+e)"by (fast intro: approx_hrabs Infinitesimal_add_approx_self)lemma approx_hrabs_add_minus_Infinitesimal:     "(e::hypreal) ∈ Infinitesimal ==> abs x @= abs(x + -e)"by (fast intro: approx_hrabs Infinitesimal_add_minus_approx_self)lemma hrabs_add_Infinitesimal_cancel:     "[| (e::hypreal) ∈ Infinitesimal; e' ∈ Infinitesimal;         abs(x+e) = abs(y+e')|] ==> abs x @= abs 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)donelemma hrabs_add_minus_Infinitesimal_cancel:     "[| (e::hypreal) ∈ Infinitesimal; e' ∈ Infinitesimal;         abs(x + -e) = abs(y + -e')|] ==> abs x @= abs 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)donesubsection {* More @{term HFinite} and @{term Infinitesimal} Theorems *}(* interesting slightly counterintuitive theorem: necessary   for proving that an open interval is an NS open set*)lemma Infinitesimal_add_hypreal_of_real_less:     "[| x < y;  u ∈ Infinitesimal |]      ==> hypreal_of_real x + u < hypreal_of_real y"apply (simp add: Infinitesimal_def)apply (drule_tac x = "hypreal_of_real y + -hypreal_of_real x" in bspec, simp)apply (simp add: abs_less_iff)donelemma Infinitesimal_add_hrabs_hypreal_of_real_less:     "[| x ∈ Infinitesimal; abs(hypreal_of_real r) < hypreal_of_real y |]      ==> abs (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]])apply (auto intro!: Infinitesimal_add_hypreal_of_real_less            simp del: star_of_abs            simp add: star_of_abs [symmetric])donelemma Infinitesimal_add_hrabs_hypreal_of_real_less2:     "[| x ∈ Infinitesimal;  abs(hypreal_of_real r) < hypreal_of_real y |]      ==> abs (x + hypreal_of_real r) < hypreal_of_real y"apply (rule add_commute [THEN subst])apply (erule Infinitesimal_add_hrabs_hypreal_of_real_less, assumption)donelemma hypreal_of_real_le_add_Infininitesimal_cancel:     "[| 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)apply (auto simp add: Infinitesimal_diff)donelemma 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"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*)lemma Infinitesimal_add_not_zero:     "[| h ∈ Infinitesimal; x ≠ 0 |] ==> star_of x + h ≠ 0"apply autoapply (subgoal_tac "h = - star_of x", auto intro: minus_unique [symmetric])donelemma 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)donelemma HFinite_square_cancel [simp]:  "(x::hypreal)*x + y*y ∈ HFinite ==> x*x ∈ HFinite"apply (rule HFinite_bounded, assumption)apply (auto)donelemma Infinitesimal_square_cancel2 [simp]:     "(x::hypreal)*x + y*y ∈ Infinitesimal ==> y*y ∈ Infinitesimal"apply (rule Infinitesimal_square_cancel)apply (rule add_commute [THEN subst])apply (simp (no_asm))donelemma HFinite_square_cancel2 [simp]:  "(x::hypreal)*x + y*y ∈ HFinite ==> y*y ∈ HFinite"apply (rule HFinite_square_cancel)apply (rule add_commute [THEN subst])apply (simp (no_asm))donelemma 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)donelemma 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)donelemma Infinitesimal_sum_square_cancel2 [simp]:     "(y::hypreal)*y + x*x + z*z ∈ Infinitesimal ==> x*x ∈ Infinitesimal"apply (rule Infinitesimal_sum_square_cancel)apply (simp add: add_ac)donelemma HFinite_sum_square_cancel2 [simp]:     "(y::hypreal)*y + x*x + z*z ∈ HFinite ==> x*x ∈ HFinite"apply (rule HFinite_sum_square_cancel)apply (simp add: add_ac)donelemma Infinitesimal_sum_square_cancel3 [simp]:     "(z::hypreal)*z + y*y + x*x ∈ Infinitesimal ==> x*x ∈ Infinitesimal"apply (rule Infinitesimal_sum_square_cancel)apply (simp add: add_ac)donelemma HFinite_sum_square_cancel3 [simp]:     "(z::hypreal)*z + y*y + x*x ∈ HFinite ==> x*x ∈ HFinite"apply (rule HFinite_sum_square_cancel)apply (simp add: add_ac)donelemma monad_hrabs_less:     "[| y ∈ monad x; 0 < hypreal_of_real e |]      ==> abs (y - x) < hypreal_of_real e"apply (drule mem_monad_approx [THEN approx_sym])apply (drule bex_Infinitesimal_iff [THEN iffD2])apply (auto dest!: InfinitesimalD)donelemma mem_monad_SReal_HFinite:     "x ∈ monad (hypreal_of_real  a) ==> x ∈ HFinite"apply (drule mem_monad_approx [THEN approx_sym])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])donesubsection{* Theorems about Standard Part*}lemma st_approx_self: "x ∈ HFinite ==> st x @= x"apply (simp add: st_def)apply (frule st_part_Ex, safe)apply (rule someI2)apply (auto intro: approx_sym)donelemma st_SReal: "x ∈ HFinite ==> st x ∈ Reals"apply (simp add: st_def)apply (frule st_part_Ex, safe)apply (rule someI2)apply (auto intro: approx_sym)donelemma st_HFinite: "x ∈ HFinite ==> st x ∈ HFinite"by (erule st_SReal [THEN SReal_subset_HFinite [THEN subsetD]])lemma st_unique: "[|r ∈ \<real>; 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)donelemma st_SReal_eq: "x ∈ Reals ==> st x = x"apply (erule st_unique)apply (rule approx_refl)donelemma 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 ∈ Reals" "st y ∈ Reals"    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])qedlemma 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 ∈ Reals; e ∈ Infinitesimal |] ==> st(x + e) = x"apply (erule st_unique)apply (erule Infinitesimal_add_approx_self)donelemma st_Infinitesimal_add_SReal2:     "[| x ∈ Reals; e ∈ Infinitesimal |] ==> st(e + x) = x"apply (erule st_unique)apply (erule Infinitesimal_add_approx_self2)donelemma 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 (neg_numeral w) = neg_numeral w"by (rule Reals_neg_numeral [THEN st_SReal_eq])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_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)"apply (rule_tac c1 = "st x" in hypreal_mult_left_cancel [THEN iffD1])apply (auto simp add: st_mult [symmetric] st_not_Infinitesimal HFinite_inverse)apply (subst right_inverse, auto)donelemma 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"apply (drule st_SReal)+apply (auto intro!: Infinitesimal_add_hypreal_of_real_less simp add: SReal_iff)donelemma Infinitesimal_add_st_le_cancel:     "[| x ∈ HFinite; y ∈ HFinite;         u ∈ Infinitesimal; st x ≤ st y + u      |] ==> st x ≤ st y"apply (simp add: linorder_not_less [symmetric])apply (auto dest: Infinitesimal_add_st_less)donelemma st_le: "[| x ∈ HFinite; y ∈ HFinite; x ≤ y |] ==> st(x) ≤ st(y)"apply (frule HFinite_st_Infinitesimal_add)apply (rotate_tac 1)apply (frule HFinite_st_Infinitesimal_add, safe)apply (rule Infinitesimal_add_st_le_cancel)apply (rule_tac [3] x = ea and y = e in Infinitesimal_diff)apply (auto simp add: add_assoc [symmetric])donelemma st_zero_le: "[| 0 ≤ x;  x ∈ HFinite |] ==> 0 ≤ st x"apply (subst st_0 [symmetric])apply (rule st_le, auto)donelemma st_zero_ge: "[| x ≤ 0;  x ∈ HFinite |] ==> st x ≤ 0"apply (subst st_0 [symmetric])apply (rule st_le, auto)donelemma st_hrabs: "x ∈ HFinite ==> abs(st x) = st(abs 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]) donesubsection {* Alternative Definitions using Free Ultrafilter *}subsubsection {* @{term HFinite} *}lemma HFinite_FreeUltrafilterNat:    "star_n X ∈ HFinite      ==> ∃u. {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)apply (simp add: star_less_def starP2_star_n)donelemma FreeUltrafilterNat_HFinite:     "∃u. {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)apply (simp add: star_less_def starP2_star_n)apply (simp add: SReal_def)donelemma HFinite_FreeUltrafilterNat_iff:     "(star_n X ∈ HFinite) = (∃u. {n. norm (X n) < u} ∈ FreeUltrafilterNat)"by (blast intro!: HFinite_FreeUltrafilterNat FreeUltrafilterNat_HFinite)subsubsection {* @{term HInfinite} *}lemma lemma_Compl_eq: "- {n. u < norm (xa n)} = {n. norm (xa n) ≤ u}"by autolemma lemma_Compl_eq2: "- {n. norm (xa n) < u} = {n. u ≤ norm (xa n)}"by autolemma lemma_Int_eq1:     "{n. norm (xa n) ≤ u} Int {n. u ≤ norm (xa n)}          = {n. norm(xa n) = u}"by autolemma lemma_FreeUltrafilterNat_one:     "{n. norm (xa n) = u} ≤ {n. norm (xa n) < u + (1::real)}"by auto(*-------------------------------------  Exclude this type of sets from free  ultrafilter for Infinite numbers! -------------------------------------*)lemma FreeUltrafilterNat_const_Finite:     "{n. norm (X n) = u} ∈ FreeUltrafilterNat ==> star_n X ∈ HFinite"apply (rule FreeUltrafilterNat_HFinite)apply (rule_tac x = "u + 1" in exI)apply (erule ultra, simp)donelemma HInfinite_FreeUltrafilterNat:     "star_n X ∈ HInfinite ==> ∀u. {n. u < norm (X n)} ∈ FreeUltrafilterNat"apply (drule HInfinite_HFinite_iff [THEN iffD1])apply (simp add: HFinite_FreeUltrafilterNat_iff)apply (rule allI, drule_tac x="u + 1" in spec)apply (drule FreeUltrafilterNat.not_memD)apply (simp add: Collect_neg_eq [symmetric] linorder_not_less)apply (erule ultra, simp)donelemma lemma_Int_HI:     "{n. norm (Xa n) < u} Int {n. X n = Xa n} ⊆ {n. norm (X n) < (u::real)}"by autolemma lemma_Int_HIa: "{n. u < norm (X n)} Int {n. norm (X n) < u} = {}"by (auto intro: order_less_asym)lemma FreeUltrafilterNat_HInfinite:     "∀u. {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)apply (drule (1) FreeUltrafilterNat.Int)apply (simp add: Collect_conj_eq [symmetric])apply (subgoal_tac "∀n. ¬ (norm (X n) < u ∧ u < norm (X n))", auto)donelemma HInfinite_FreeUltrafilterNat_iff:     "(star_n X ∈ HInfinite) = (∀u. {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. {n. norm (X n) < u} ∈ \<U>"apply (simp add: Infinitesimal_def ball_SReal_eq)apply (simp add: hnorm_def starfun_star_n star_of_def)apply (simp add: star_less_def starP2_star_n)donelemma FreeUltrafilterNat_Infinitesimal:     "∀u>0. {n. norm (X n) < u} ∈ \<U> ==> star_n X ∈ Infinitesimal"apply (simp add: Infinitesimal_def ball_SReal_eq)apply (simp add: hnorm_def starfun_star_n star_of_def)apply (simp add: star_less_def starP2_star_n)donelemma Infinitesimal_FreeUltrafilterNat_iff:     "(star_n X ∈ Infinitesimal) = (∀u>0. {n. norm (X n) < u} ∈ \<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 add: real_of_nat_Suc_gt_zero)apply (blast dest!: reals_Archimedean intro: order_less_trans)donelemma lemma_Infinitesimal2:     "(∀r ∈ Reals. 0 < r --> x < r) =      (∀n. x < inverse(hypreal_of_nat (Suc n)))"apply safeapply (drule_tac x = "inverse (hypreal_of_real (real (Suc n))) " in bspec)apply (simp (no_asm_use))apply (rule real_of_nat_Suc_gt_zero [THEN positive_imp_inverse_positive, THEN star_of_less [THEN iffD2], THEN [2] impE])prefer 2 apply assumptionapply (simp add: real_of_nat_def)apply (auto dest!: reals_Archimedean simp add: SReal_iff)apply (drule star_of_less [THEN iffD2])apply (simp add: real_of_nat_def)apply (blast intro: order_less_trans)donelemma Infinitesimal_hypreal_of_nat_iff:     "Infinitesimal = {x. ∀n. hnorm x < inverse (hypreal_of_nat (Suc n))}"apply (simp add: Infinitesimal_def)apply (auto simp add: lemma_Infinitesimal2)donesubsection{*Proof that @{term omega} is an infinite number*}text{*It will follow that epsilon 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)(*-------------------------------------------  Prove that any segment is finite and  hence cannot belong to FreeUltrafilterNat -------------------------------------------*)lemma finite_nat_segment: "finite {n::nat. n < m}"apply (induct "m")apply (auto simp add: Suc_Un_eq)donelemma finite_real_of_nat_segment: "finite {n::nat. real n < real (m::nat)}"by (auto intro: finite_nat_segment)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)donelemma 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. abs(real n) ≤ u}"apply (simp (no_asm) add: real_of_nat_Suc_gt_zero finite_real_of_nat_le_real)donelemma rabs_real_of_nat_le_real_FreeUltrafilterNat:     "{n. abs(real n) ≤ u} ∉ FreeUltrafilterNat"by (blast intro!: FreeUltrafilterNat.finite finite_rabs_real_of_nat_le_real)lemma FreeUltrafilterNat_nat_gt_real: "{n. u < real n} ∈ FreeUltrafilterNat"apply (rule ccontr, drule FreeUltrafilterNat.not_memD)apply (subgoal_tac "- {n::nat. u < real n} = {n. real n ≤ u}")prefer 2 apply forceapply (simp add: finite_real_of_nat_le_real [THEN FreeUltrafilterNat.finite])done(*-------------------------------------------------------------- The complement of {n. abs(real n) ≤ u} = {n. u < abs (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 omega} is a member of @{term HInfinite}*}lemma FreeUltrafilterNat_omega: "{n. u < real n} ∈ FreeUltrafilterNat"apply (cut_tac u = u in rabs_real_of_nat_le_real_FreeUltrafilterNat)apply (auto dest: FreeUltrafilterNat.not_memD simp add: Compl_real_le_eq)donetheorem HInfinite_omega [simp]: "omega ∈ HInfinite"apply (simp add: omega_def)apply (rule FreeUltrafilterNat_HInfinite)apply (simp (no_asm) add: real_norm_def real_of_nat_Suc diff_less_eq [symmetric] FreeUltrafilterNat_omega)done(*-----------------------------------------------       Epsilon is a member of Infinitesimal -----------------------------------------------*)lemma Infinitesimal_epsilon [simp]: "epsilon ∈ Infinitesimal"by (auto intro!: HInfinite_inverse_Infinitesimal HInfinite_omega simp add: hypreal_epsilon_inverse_omega)lemma HFinite_epsilon [simp]: "epsilon ∈ HFinite"by (auto intro: Infinitesimal_subset_HFinite [THEN subsetD])lemma epsilon_approx_zero [simp]: "epsilon @= 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 (simp add: inverse_eq_divide)apply (subst pos_less_divide_eq, assumption)apply (subst pos_less_divide_eq) apply (simp add: real_of_nat_Suc_gt_zero)apply (simp add: mult_commute)donelemma finite_inverse_real_of_posnat_gt_real:     "0 < u ==> finite {n. u < inverse(real(Suc n))}"apply (simp (no_asm_simp) add: real_of_nat_less_inverse_iff)apply (simp (no_asm_simp) add: real_of_nat_Suc less_diff_eq [symmetric])apply (rule finite_real_of_nat_less_real)donelemma lemma_real_le_Un_eq2:     "{n. u ≤ inverse(real(Suc n))} =     {n. u < inverse(real(Suc n))} Un {n. u = inverse(real(Suc n))}"apply (auto dest: order_le_imp_less_or_eq simp add: order_less_imp_le)donelemma real_of_nat_inverse_eq_iff:     "(u = inverse (real(Suc n))) = (real(Suc n) = inverse u)"by (auto simp add: real_of_nat_Suc_gt_zero less_imp_neq [THEN not_sym])lemma lemma_finite_omega_set2: "finite {n::nat. u = inverse(real(Suc n))}"apply (simp (no_asm_simp) add: real_of_nat_inverse_eq_iff)apply (cut_tac x = "inverse u - 1" in lemma_finite_omega_set)apply (simp add: real_of_nat_Suc diff_eq_eq [symmetric] eq_commute)donelemma 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_omega_set2 finite_inverse_real_of_posnat_gt_real)lemma inverse_real_of_posnat_ge_real_FreeUltrafilterNat:     "0 < u ==> {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}"apply (auto dest!: order_le_less_trans simp add: linorder_not_le)donelemma FreeUltrafilterNat_inverse_real_of_posnat:     "0 < u ==>      {n. inverse(real(Suc n)) < u} ∈ FreeUltrafilterNat"apply (cut_tac u = u in inverse_real_of_posnat_ge_real_FreeUltrafilterNat)apply (auto dest: FreeUltrafilterNat.not_memD simp add: Compl_le_inverse_eq)donetext{* 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"apply (simp add: hypnat_omega_def starfun_star_n star_n_inverse)apply (simp add: Infinitesimal_FreeUltrafilterNat_iff)apply (simp add: real_of_nat_Suc_gt_zero FreeUltrafilterNat_inverse_real_of_posnat)donetext{* 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"apply (auto intro!: bexI dest: FreeUltrafilterNat_inverse_real_of_posnat FreeUltrafilterNat.Int intro: order_less_trans FreeUltrafilterNat.subset simp add: star_n_diff star_of_def Infinitesimal_FreeUltrafilterNat_iff star_n_inverse)donelemma real_seq_to_hypreal_approx:     "∀n. norm(X n - x) < inverse(real(Suc n))      ==> star_n X @= star_of x"apply (subst approx_minus_iff)apply (rule mem_infmal_iff [THEN subst])apply (erule real_seq_to_hypreal_Infinitesimal)donelemma real_seq_to_hypreal_approx2:     "∀n. norm(x - X n) < inverse(real(Suc n))               ==> star_n X @= star_of x"apply (rule real_seq_to_hypreal_approx)apply (subst norm_minus_cancel [symmetric])apply (simp del: norm_minus_cancel)donelemma real_seq_to_hypreal_Infinitesimal2:     "∀n. norm(X n - Y n) < inverse(real(Suc n))      ==> star_n X - star_n Y ∈ Infinitesimal"by (auto intro!: bexI         dest: FreeUltrafilterNat_inverse_real_of_posnat                FreeUltrafilterNat.Int         intro: order_less_trans FreeUltrafilterNat.subset          simp add: Infinitesimal_FreeUltrafilterNat_iff star_n_diff                    star_n_inverse)end`