(* Title : NSA.thy Author : Jacques D. Fleuriot Copyright : 1998 University of Cambridge Converted to Isar and polished by lcp *) header{*Infinite Numbers, Infinitesimals, Infinitely Close Relation*} theory NSA imports HyperArith "../Real/RComplete" begin constdefs Infinitesimal :: "hypreal set" "Infinitesimal == {x. ∀r ∈ Reals. 0 < r --> abs x < r}" HFinite :: "hypreal set" "HFinite == {x. ∃r ∈ Reals. abs x < r}" HInfinite :: "hypreal set" "HInfinite == {x. ∀r ∈ Reals. r < abs x}" approx :: "[hypreal, hypreal] => bool" (infixl "@=" 50) --{*the `infinitely close' relation*} "x @= y == (x + -y) ∈ Infinitesimal" st :: "hypreal => hypreal" --{*the standard part of a hyperreal*} "st == (%x. @r. x ∈ HFinite & r ∈ Reals & r @= x)" monad :: "hypreal => hypreal set" "monad x == {y. x @= y}" galaxy :: "hypreal => hypreal set" "galaxy x == {y. (x + -y) ∈ HFinite}" defs (overloaded) SReal_def: "Reals == {x. ∃r. x = hypreal_of_real r}" --{*the standard real numbers as a subset of the hyperreals*} syntax (xsymbols) approx :: "[hypreal, hypreal] => bool" (infixl "≈" 50) syntax (HTML output) approx :: "[hypreal, hypreal] => bool" (infixl "≈" 50) subsection{*Closure Laws for the Standard Reals*} lemma SReal_add [simp]: "[| (x::hypreal) ∈ Reals; y ∈ Reals |] ==> x + y ∈ Reals" apply (auto simp add: SReal_def) apply (rule_tac x = "r + ra" in exI, simp) done lemma SReal_mult: "[| (x::hypreal) ∈ Reals; y ∈ Reals |] ==> x * y ∈ Reals" apply (simp add: SReal_def, safe) apply (rule_tac x = "r * ra" in exI) apply (simp (no_asm)) done lemma SReal_inverse: "(x::hypreal) ∈ Reals ==> inverse x ∈ Reals" apply (simp add: SReal_def) apply (blast intro: star_of_inverse [symmetric]) done lemma SReal_divide: "[| (x::hypreal) ∈ Reals; y ∈ Reals |] ==> x/y ∈ Reals" by (simp (no_asm_simp) add: SReal_mult SReal_inverse divide_inverse) lemma SReal_minus: "(x::hypreal) ∈ Reals ==> -x ∈ Reals" apply (simp add: SReal_def) apply (blast intro: star_of_minus [symmetric]) done lemma SReal_minus_iff [simp]: "(-x ∈ Reals) = ((x::hypreal) ∈ Reals)" apply auto apply (erule_tac [2] SReal_minus) apply (drule SReal_minus, auto) done lemma SReal_add_cancel: "[| (x::hypreal) + y ∈ Reals; y ∈ Reals |] ==> x ∈ Reals" apply (drule_tac x = y in SReal_minus) apply (drule SReal_add, assumption, auto) done lemma SReal_hrabs: "(x::hypreal) ∈ Reals ==> abs x ∈ Reals" apply (auto simp add: SReal_def) apply (rule_tac x="abs r" in exI) apply simp done lemma SReal_hypreal_of_real [simp]: "hypreal_of_real x ∈ Reals" by (simp add: SReal_def) lemma SReal_number_of [simp]: "(number_of w ::hypreal) ∈ Reals" apply (simp only: star_of_number_of [symmetric]) apply (rule SReal_hypreal_of_real) done (** As always with numerals, 0 and 1 are special cases **) lemma Reals_0 [simp]: "(0::hypreal) ∈ Reals" apply (subst numeral_0_eq_0 [symmetric]) apply (rule SReal_number_of) done lemma Reals_1 [simp]: "(1::hypreal) ∈ Reals" apply (subst numeral_1_eq_1 [symmetric]) apply (rule SReal_number_of) done lemma SReal_divide_number_of: "r ∈ Reals ==> r/(number_of w::hypreal) ∈ Reals" apply (simp only: divide_inverse) apply (blast intro!: SReal_number_of SReal_mult SReal_inverse) done text{*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]) done lemma SReal_omega_not_mem: "omega ∉ Reals" apply (simp add: SReal_def) apply (auto simp add: hypreal_of_real_not_eq_omega [THEN not_sym]) done lemma SReal_UNIV_real: "{x. hypreal_of_real x ∈ Reals} = (UNIV::real set)" by (simp add: SReal_def) lemma 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 (auto simp add: SReal_def) lemma inv_hypreal_of_real_image: "inv hypreal_of_real ` Reals = UNIV" apply (auto simp add: SReal_def) apply (rule inj_hypreal_of_real [THEN inv_f_f, THEN subst], blast) done lemma SReal_hypreal_of_real_image: "[| ∃x. x: P; P ⊆ Reals |] ==> ∃Q. P = hypreal_of_real ` Q" apply (simp add: SReal_def, blast) done lemma SReal_dense: "[| (x::hypreal) ∈ Reals; y ∈ Reals; x<y |] ==> ∃r ∈ Reals. x<r & r<y" apply (auto simp add: SReal_iff) apply (drule dense, safe) apply (rule_tac x = "hypreal_of_real r" in bexI, auto) done text{*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) done subsection{*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) done lemma 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 assumption apply (drule_tac x = xa in spec) apply (auto simp add: hypreal_of_real_isUb_iff) done lemma 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 subsection{* 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!: SReal_add hrabs_add_less) done lemma HFinite_mult: "[|x ∈ HFinite; y ∈ HFinite|] ==> x*y ∈ HFinite" apply (simp add: HFinite_def abs_mult) apply (blast intro!: SReal_mult abs_mult_less) done lemma HFinite_minus_iff: "(-x ∈ HFinite) = (x ∈ HFinite)" by (simp add: HFinite_def) lemma SReal_subset_HFinite: "Reals ⊆ HFinite" apply (auto simp add: SReal_def HFinite_def) apply (rule_tac x = "1 + abs (hypreal_of_real r) " in exI) apply (rule conjI, rule_tac x = "1 + abs r" in exI) apply simp_all done lemma HFinite_hypreal_of_real [simp]: "hypreal_of_real x ∈ HFinite" by (auto intro: SReal_subset_HFinite [THEN subsetD]) lemma HFiniteD: "x ∈ HFinite ==> ∃t ∈ Reals. abs x < t" by (simp add: HFinite_def) lemma HFinite_hrabs_iff [iff]: "(abs x ∈ HFinite) = (x ∈ HFinite)" by (simp add: HFinite_def) lemma HFinite_number_of [simp]: "number_of w ∈ HFinite" by (rule SReal_number_of [THEN SReal_subset_HFinite [THEN subsetD]]) (** As always with numerals, 0 and 1 are special cases **) lemma HFinite_0 [simp]: "0 ∈ HFinite" apply (subst numeral_0_eq_0 [symmetric]) apply (rule HFinite_number_of) done lemma HFinite_1 [simp]: "1 ∈ HFinite" apply (subst numeral_1_eq_1 [symmetric]) apply (rule HFinite_number_of) done lemma HFinite_bounded: "[|x ∈ HFinite; y ≤ x; 0 ≤ y |] ==> y ∈ HFinite" apply (case_tac "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) done subsection{* Set of Infinitesimals is a Subring of the Hyperreals*} lemma InfinitesimalD: "x ∈ Infinitesimal ==> ∀r ∈ Reals. 0 < r --> abs x < r" by (simp add: Infinitesimal_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 auto lemma Infinitesimal_add: "[| x ∈ Infinitesimal; y ∈ Infinitesimal |] ==> (x+y) ∈ Infinitesimal" apply (auto simp add: Infinitesimal_def) apply (rule hypreal_sum_of_halves [THEN subst]) apply (drule half_gt_zero) apply (blast intro: hrabs_add_less SReal_divide_number_of) done lemma Infinitesimal_minus_iff [simp]: "(-x:Infinitesimal) = (x:Infinitesimal)" by (simp add: Infinitesimal_def) lemma Infinitesimal_diff: "[| x ∈ Infinitesimal; y ∈ Infinitesimal |] ==> x-y ∈ Infinitesimal" by (simp add: diff_def Infinitesimal_add) lemma Infinitesimal_mult: "[| x ∈ Infinitesimal; y ∈ Infinitesimal |] ==> (x * y) ∈ Infinitesimal" apply (auto simp add: Infinitesimal_def abs_mult) apply (case_tac "y=0", simp) apply (cut_tac a = "abs x" and b = 1 and c = "abs y" and d = r in mult_strict_mono, auto) done lemma Infinitesimal_HFinite_mult: "[| x ∈ Infinitesimal; y ∈ HFinite |] ==> (x * y) ∈ Infinitesimal" apply (auto dest!: HFiniteD simp add: Infinitesimal_def abs_mult) apply (frule hrabs_less_gt_zero) apply (drule_tac x = "r/t" in bspec) apply (blast intro: SReal_divide) apply (cut_tac a = "abs x" and b = "r/t" and c = "abs y" in mult_strict_mono) apply (auto simp add: zero_less_divide_iff) done lemma Infinitesimal_HFinite_mult2: "[| x ∈ Infinitesimal; y ∈ HFinite |] ==> (y * x) ∈ Infinitesimal" by (auto dest: Infinitesimal_HFinite_mult simp add: mult_commute) (*** rather long proof ***) lemma HInfinite_inverse_Infinitesimal: "x ∈ HInfinite ==> inverse x: Infinitesimal" apply (auto simp add: HInfinite_def Infinitesimal_def) apply (erule_tac x = "inverse r" in ballE) apply (frule_tac a1 = r and z = "abs x" in positive_imp_inverse_positive [THEN order_less_trans], assumption) apply (drule inverse_inverse_eq [symmetric, THEN subst]) apply (rule inverse_less_iff_less [THEN iffD1]) apply (auto simp add: SReal_inverse) done lemma HInfinite_mult: "[|x ∈ HInfinite;y ∈ HInfinite|] ==> (x*y) ∈ HInfinite" apply (auto simp add: HInfinite_def abs_mult) apply (erule_tac x = 1 in ballE) apply (erule_tac x = r in ballE) apply (case_tac "y=0", simp) apply (cut_tac c = 1 and d = "abs x" and a = r and b = "abs y" in mult_strict_mono) apply (auto simp add: mult_ac) done lemma 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 ∈ 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 ∈ 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 ∈ 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 ∈ 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) done lemma HInfinite_add_lt_zero: "[|x ∈ HInfinite; y < 0; x < 0|] ==> (x + y): HInfinite" by (blast intro: HInfinite_add_le_zero order_less_imp_le) lemma HFinite_sum_squares: "[|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 auto lemma not_Infinitesimal_not_zero2: "x ∈ HFinite - Infinitesimal ==> x ≠ 0" by auto lemma Infinitesimal_hrabs_iff [iff]: "(abs x ∈ Infinitesimal) = (x ∈ Infinitesimal)" by (auto simp add: abs_if) lemma HFinite_diff_Infinitesimal_hrabs: "x ∈ HFinite - Infinitesimal ==> abs x ∈ HFinite - Infinitesimal" by blast lemma hrabs_less_Infinitesimal: "[| e ∈ Infinitesimal; abs x < e |] ==> x ∈ Infinitesimal" by (auto simp add: Infinitesimal_def abs_less_iff) lemma hrabs_le_Infinitesimal: "[| e ∈ Infinitesimal; abs x ≤ e |] ==> x ∈ Infinitesimal" by (blast dest: order_le_imp_less_or_eq intro: hrabs_less_Infinitesimal) lemma Infinitesimal_interval: "[| e ∈ Infinitesimal; e' ∈ Infinitesimal; e' < x ; x < e |] ==> x ∈ Infinitesimal" by (auto simp add: Infinitesimal_def abs_less_iff) lemma Infinitesimal_interval2: "[| e ∈ Infinitesimal; e' ∈ Infinitesimal; e' ≤ x ; x ≤ e |] ==> x ∈ Infinitesimal" by (auto intro: Infinitesimal_interval simp add: order_le_less) lemma not_Infinitesimal_mult: "[| x ∉ Infinitesimal; y ∉ Infinitesimal|] ==> (x*y) ∉Infinitesimal" apply (unfold Infinitesimal_def, clarify) apply (simp add: linorder_not_less abs_mult) apply (erule_tac x = "r*ra" in ballE) prefer 2 apply (fast intro: SReal_mult) apply (auto simp add: zero_less_mult_iff) apply (cut_tac c = ra and d = "abs y" and a = r and b = "abs x" in mult_mono, auto) done lemma Infinitesimal_mult_disj: "x*y ∈ Infinitesimal ==> x ∈ Infinitesimal | y ∈ Infinitesimal" apply (rule ccontr) apply (drule de_Morgan_disj [THEN iffD1]) apply (fast dest: not_Infinitesimal_mult) done lemma HFinite_Infinitesimal_not_zero: "x ∈ HFinite-Infinitesimal ==> x ≠ 0" by blast lemma HFinite_Infinitesimal_diff_mult: "[| x ∈ HFinite - Infinitesimal; y ∈ HFinite - Infinitesimal |] ==> (x*y) ∈ HFinite - Infinitesimal" apply clarify apply (blast dest: HFinite_mult not_Infinitesimal_mult) done lemma Infinitesimal_subset_HFinite: "Infinitesimal ⊆ HFinite" apply (simp add: Infinitesimal_def HFinite_def, auto) apply (rule_tac x = 1 in bexI, auto) done lemma Infinitesimal_hypreal_of_real_mult: "x ∈ Infinitesimal ==> x * hypreal_of_real r ∈ Infinitesimal" by (erule HFinite_hypreal_of_real [THEN [2] Infinitesimal_HFinite_mult]) lemma Infinitesimal_hypreal_of_real_mult2: "x ∈ Infinitesimal ==> hypreal_of_real r * x ∈ Infinitesimal" by (erule HFinite_hypreal_of_real [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 hypreal_minus_distrib1: "-(y + -(x::hypreal)) = x + -y" by (simp add: add_commute) lemma approx_sym: "x @= y ==> y @= x" apply (simp add: approx_def) apply (rule hypreal_minus_distrib1 [THEN subst]) apply (erule Infinitesimal_minus_iff [THEN iffD2]) done lemma approx_trans: "[| x @= y; y @= z |] ==> x @= z" apply (simp add: approx_def) apply (drule Infinitesimal_add, assumption, auto) done lemma approx_trans2: "[| r @= x; s @= x |] ==> r @= s" by (blast intro: approx_sym approx_trans) lemma approx_trans3: "[| x @= r; x @= s|] ==> r @= s" by (blast intro: approx_sym approx_trans) lemma number_of_approx_reorient: "(number_of w @= x) = (x @= number_of w)" by (blast intro: approx_sym) lemma zero_approx_reorient: "(0 @= x) = (x @= 0)" by (blast intro: approx_sym) lemma one_approx_reorient: "(1 @= x) = (x @= 1)" by (blast intro: approx_sym) ML {* val SReal_add = thm "SReal_add"; val SReal_mult = thm "SReal_mult"; val SReal_inverse = thm "SReal_inverse"; val SReal_divide = thm "SReal_divide"; val SReal_minus = thm "SReal_minus"; val SReal_minus_iff = thm "SReal_minus_iff"; val SReal_add_cancel = thm "SReal_add_cancel"; val SReal_hrabs = thm "SReal_hrabs"; val SReal_hypreal_of_real = thm "SReal_hypreal_of_real"; val SReal_number_of = thm "SReal_number_of"; val Reals_0 = thm "Reals_0"; val Reals_1 = thm "Reals_1"; val SReal_divide_number_of = thm "SReal_divide_number_of"; val SReal_epsilon_not_mem = thm "SReal_epsilon_not_mem"; val SReal_omega_not_mem = thm "SReal_omega_not_mem"; val SReal_UNIV_real = thm "SReal_UNIV_real"; val SReal_iff = thm "SReal_iff"; val hypreal_of_real_image = thm "hypreal_of_real_image"; val inv_hypreal_of_real_image = thm "inv_hypreal_of_real_image"; val SReal_hypreal_of_real_image = thm "SReal_hypreal_of_real_image"; val SReal_dense = thm "SReal_dense"; val hypreal_of_real_isUb_iff = thm "hypreal_of_real_isUb_iff"; val hypreal_of_real_isLub1 = thm "hypreal_of_real_isLub1"; val hypreal_of_real_isLub2 = thm "hypreal_of_real_isLub2"; val hypreal_of_real_isLub_iff = thm "hypreal_of_real_isLub_iff"; val lemma_isUb_hypreal_of_real = thm "lemma_isUb_hypreal_of_real"; val lemma_isLub_hypreal_of_real = thm "lemma_isLub_hypreal_of_real"; val lemma_isLub_hypreal_of_real2 = thm "lemma_isLub_hypreal_of_real2"; val SReal_complete = thm "SReal_complete"; val HFinite_add = thm "HFinite_add"; val HFinite_mult = thm "HFinite_mult"; val HFinite_minus_iff = thm "HFinite_minus_iff"; val SReal_subset_HFinite = thm "SReal_subset_HFinite"; val HFinite_hypreal_of_real = thm "HFinite_hypreal_of_real"; val HFiniteD = thm "HFiniteD"; val HFinite_hrabs_iff = thm "HFinite_hrabs_iff"; val HFinite_number_of = thm "HFinite_number_of"; val HFinite_0 = thm "HFinite_0"; val HFinite_1 = thm "HFinite_1"; val HFinite_bounded = thm "HFinite_bounded"; val InfinitesimalD = thm "InfinitesimalD"; val Infinitesimal_zero = thm "Infinitesimal_zero"; val hypreal_sum_of_halves = thm "hypreal_sum_of_halves"; val Infinitesimal_add = thm "Infinitesimal_add"; val Infinitesimal_minus_iff = thm "Infinitesimal_minus_iff"; val Infinitesimal_diff = thm "Infinitesimal_diff"; val Infinitesimal_mult = thm "Infinitesimal_mult"; val Infinitesimal_HFinite_mult = thm "Infinitesimal_HFinite_mult"; val Infinitesimal_HFinite_mult2 = thm "Infinitesimal_HFinite_mult2"; val HInfinite_inverse_Infinitesimal = thm "HInfinite_inverse_Infinitesimal"; val HInfinite_mult = thm "HInfinite_mult"; val HInfinite_add_ge_zero = thm "HInfinite_add_ge_zero"; val HInfinite_add_ge_zero2 = thm "HInfinite_add_ge_zero2"; val HInfinite_add_gt_zero = thm "HInfinite_add_gt_zero"; val HInfinite_minus_iff = thm "HInfinite_minus_iff"; val HInfinite_add_le_zero = thm "HInfinite_add_le_zero"; val HInfinite_add_lt_zero = thm "HInfinite_add_lt_zero"; val HFinite_sum_squares = thm "HFinite_sum_squares"; val not_Infinitesimal_not_zero = thm "not_Infinitesimal_not_zero"; val not_Infinitesimal_not_zero2 = thm "not_Infinitesimal_not_zero2"; val Infinitesimal_hrabs_iff = thm "Infinitesimal_hrabs_iff"; val HFinite_diff_Infinitesimal_hrabs = thm "HFinite_diff_Infinitesimal_hrabs"; val hrabs_less_Infinitesimal = thm "hrabs_less_Infinitesimal"; val hrabs_le_Infinitesimal = thm "hrabs_le_Infinitesimal"; val Infinitesimal_interval = thm "Infinitesimal_interval"; val Infinitesimal_interval2 = thm "Infinitesimal_interval2"; val not_Infinitesimal_mult = thm "not_Infinitesimal_mult"; val Infinitesimal_mult_disj = thm "Infinitesimal_mult_disj"; val HFinite_Infinitesimal_not_zero = thm "HFinite_Infinitesimal_not_zero"; val HFinite_Infinitesimal_diff_mult = thm "HFinite_Infinitesimal_diff_mult"; val Infinitesimal_subset_HFinite = thm "Infinitesimal_subset_HFinite"; val Infinitesimal_hypreal_of_real_mult = thm "Infinitesimal_hypreal_of_real_mult"; val Infinitesimal_hypreal_of_real_mult2 = thm "Infinitesimal_hypreal_of_real_mult2"; val mem_infmal_iff = thm "mem_infmal_iff"; val approx_minus_iff = thm "approx_minus_iff"; val approx_minus_iff2 = thm "approx_minus_iff2"; val approx_refl = thm "approx_refl"; val approx_sym = thm "approx_sym"; val approx_trans = thm "approx_trans"; val approx_trans2 = thm "approx_trans2"; val approx_trans3 = thm "approx_trans3"; val number_of_approx_reorient = thm "number_of_approx_reorient"; val zero_approx_reorient = thm "zero_approx_reorient"; val one_approx_reorient = thm "one_approx_reorient"; (*** re-orientation, following HOL/Integ/Bin.ML We re-orient x @=y where x is 0, 1 or a numeral, unless y is as well! ***) (*reorientation simprules using ==, for the following simproc*) val meta_zero_approx_reorient = zero_approx_reorient RS eq_reflection; val meta_one_approx_reorient = one_approx_reorient RS eq_reflection; val meta_number_of_approx_reorient = number_of_approx_reorient RS eq_reflection (*reorientation simplification procedure: reorients (polymorphic) 0 = x, 1 = x, nnn = x provided x isn't 0, 1 or a numeral.*) fun reorient_proc sg _ (_ $ t $ u) = case u of Const("0", _) => NONE | Const("1", _) => NONE | Const("Numeral.number_of", _) $ _ => NONE | _ => SOME (case t of Const("0", _) => meta_zero_approx_reorient | Const("1", _) => meta_one_approx_reorient | Const("Numeral.number_of", _) $ _ => meta_number_of_approx_reorient); val approx_reorient_simproc = Bin_Simprocs.prep_simproc ("reorient_simproc", ["0@=x", "1@=x", "number_of w @= x"], reorient_proc); Addsimprocs [approx_reorient_simproc]; *} lemma Infinitesimal_approx_minus: "(x-y ∈ Infinitesimal) = (x @= y)" by (auto simp add: diff_def 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) done lemma Infinitesimal_approx: "[| x ∈ Infinitesimal; y ∈ Infinitesimal |] ==> x @= y" apply (simp add: mem_infmal_iff) apply (blast intro: approx_trans approx_sym) done lemma approx_add: "[| a @= b; c @= d |] ==> a+c @= b+d" proof (unfold approx_def) assume inf: "a + - b ∈ Infinitesimal" "c + - d ∈ Infinitesimal" have "a + c + - (b + d) = (a + - b) + (c + - d)" by arith also have "... ∈ Infinitesimal" using inf by (rule Infinitesimal_add) finally show "a + c + - (b + d) ∈ Infinitesimal" . qed lemma approx_minus: "a @= b ==> -a @= -b" apply (rule approx_minus_iff [THEN iffD2, THEN approx_sym]) apply (drule approx_minus_iff [THEN iffD1]) apply (simp (no_asm) add: add_commute) done lemma approx_minus2: "-a @= -b ==> a @= b" by (auto dest: approx_minus) lemma approx_minus_cancel [simp]: "(-a @= -b) = (a @= b)" by (blast intro: approx_minus approx_minus2) lemma approx_add_minus: "[| a @= b; c @= d |] ==> a + -c @= b + -d" by (blast intro!: approx_add approx_minus) lemma approx_mult1: "[| a @= b; c: HFinite|] ==> a*c @= b*c" by (simp add: approx_def Infinitesimal_HFinite_mult minus_mult_left left_distrib [symmetric] del: minus_mult_left [symmetric]) lemma approx_mult2: "[|a @= b; c: HFinite|] ==> c*a @= c*b" by (simp add: approx_mult1 mult_commute) lemma approx_mult_subst: "[|u @= v*x; x @= y; v ∈ HFinite|] ==> u @= v*y" by (blast intro: approx_mult2 approx_trans) lemma approx_mult_subst2: "[| u @= x*v; x @= y; v ∈ HFinite |] ==> u @= y*v" by (blast intro: approx_mult1 approx_trans) lemma approx_mult_subst_SReal: "[| u @= x*hypreal_of_real v; x @= y |] ==> u @= y*hypreal_of_real 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]) done lemma Infinitesimal_add_approx_self: "y ∈ Infinitesimal ==> x @= x + y" apply (rule bex_Infinitesimal_iff [THEN iffD1]) apply (drule Infinitesimal_minus_iff [THEN iffD2]) apply (auto simp add: add_assoc [symmetric]) done 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" apply (drule_tac x = x in Infinitesimal_add_approx_self [THEN approx_sym]) apply (erule approx_trans3 [THEN approx_sym], assumption) done lemma 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) done lemma approx_add_left_cancel: "d + b @= d + c ==> b @= c" apply (drule approx_minus_iff [THEN iffD1]) apply (simp add: approx_minus_iff [symmetric] add_ac) done lemma approx_add_right_cancel: "b + d @= c + d ==> b @= c" apply (rule approx_add_left_cancel) apply (simp add: add_commute) done lemma approx_add_mono1: "b @= c ==> d + b @= d + c" apply (rule approx_minus_iff [THEN iffD2]) apply (simp add: approx_minus_iff [symmetric] add_ac) done 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" 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) done lemma approx_hypreal_of_real_HFinite: "x @= hypreal_of_real 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" apply (rule approx_trans) apply (rule_tac [2] approx_mult2) apply (rule approx_mult1) prefer 2 apply (blast intro: approx_HFinite approx_sym, auto) done lemma approx_mult_hypreal_of_real: "[|a @= hypreal_of_real b; c @= hypreal_of_real d |] ==> a*c @= hypreal_of_real b*hypreal_of_real d" by (blast intro!: approx_mult_HFinite approx_hypreal_of_real_HFinite HFinite_hypreal_of_real) lemma approx_SReal_mult_cancel_zero: "[| a ∈ Reals; a ≠ 0; a*x @= 0 |] ==> x @= 0" apply (drule SReal_inverse [THEN SReal_subset_HFinite [THEN subsetD]]) apply (auto dest: approx_mult2 simp add: mult_assoc [symmetric]) done lemma approx_mult_SReal1: "[| a ∈ Reals; x @= 0 |] ==> x*a @= 0" by (auto dest: SReal_subset_HFinite [THEN subsetD] approx_mult1) lemma approx_mult_SReal2: "[| a ∈ 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 ∈ 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 ∈ Reals; a ≠ 0; a* w @= a*z |] ==> w @= z" apply (drule SReal_inverse [THEN SReal_subset_HFinite [THEN subsetD]]) apply (auto dest: approx_mult2 simp add: mult_assoc [symmetric]) done lemma approx_SReal_mult_cancel_iff1 [simp]: "[| a ∈ 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 ≤ f; f @= g; g ≤ z |] ==> f @= z" apply (simp add: bex_Infinitesimal_iff2 [symmetric], auto) apply (rule_tac x = "g+y-z" in bexI) apply (simp (no_asm)) apply (rule Infinitesimal_interval2) apply (rule_tac [2] Infinitesimal_zero, auto) done subsection{* Zero is the Only Infinitesimal that is also a Real*} lemma Infinitesimal_less_SReal: "[| x ∈ Reals; y ∈ Infinitesimal; 0 < x |] ==> y < x" apply (simp add: Infinitesimal_def) apply (rule abs_ge_self [THEN order_le_less_trans], auto) done lemma Infinitesimal_less_SReal2: "y ∈ Infinitesimal ==> ∀r ∈ Reals. 0 < r --> y < r" by (blast intro: Infinitesimal_less_SReal) lemma SReal_not_Infinitesimal: "[| 0 < y; y ∈ Reals|] ==> y ∉ Infinitesimal" apply (simp add: Infinitesimal_def) apply (auto simp add: abs_if) done lemma SReal_minus_not_Infinitesimal: "[| y < 0; y ∈ Reals |] ==> y ∉ Infinitesimal" apply (subst Infinitesimal_minus_iff [symmetric]) apply (rule SReal_not_Infinitesimal, auto) done lemma SReal_Int_Infinitesimal_zero: "Reals Int Infinitesimal = {0}" apply auto apply (cut_tac x = x and y = 0 in linorder_less_linear) apply (blast dest: SReal_not_Infinitesimal SReal_minus_not_Infinitesimal) done lemma SReal_Infinitesimal_zero: "[| x ∈ Reals; x ∈ Infinitesimal|] ==> x = 0" by (cut_tac SReal_Int_Infinitesimal_zero, blast) lemma SReal_HFinite_diff_Infinitesimal: "[| x ∈ 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 hypreal_of_real_Infinitesimal_iff_0 [iff]: "(hypreal_of_real x ∈ Infinitesimal) = (x=0)" apply auto apply (rule ccontr) apply (rule hypreal_of_real_HFinite_diff_Infinitesimal [THEN DiffD2], auto) done lemma number_of_not_Infinitesimal [simp]: "number_of w ≠ (0::hypreal) ==> number_of w ∉ Infinitesimal" by (fast dest: SReal_number_of [THEN SReal_Infinitesimal_zero]) (*again: 1 is a special case, but not 0 this time*) lemma one_not_Infinitesimal [simp]: "1 ∉ Infinitesimal" apply (subst numeral_1_eq_1 [symmetric]) apply (rule number_of_not_Infinitesimal) apply (simp (no_asm)) done lemma approx_SReal_not_zero: "[| y ∈ 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) done lemma 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: "[| y ≠ 0; y ∈ Infinitesimal; x/y ∈ HFinite |] ==> x ∈ Infinitesimal" apply (drule Infinitesimal_HFinite_mult2, assumption) apply (simp add: divide_inverse mult_assoc) done lemma Infinitesimal_SReal_divide: "[| x ∈ Infinitesimal; y ∈ Reals |] ==> x/y ∈ Infinitesimal" apply (simp add: divide_inverse) apply (auto intro!: Infinitesimal_HFinite_mult dest!: SReal_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 SReal_approx_iff: "[|x ∈ Reals; y ∈ Reals|] ==> (x @= y) = (x = y)" apply auto apply (simp add: approx_def) apply (drule_tac x = y in SReal_minus) apply (drule SReal_add, assumption) apply (drule SReal_Infinitesimal_zero, assumption) apply (drule sym) apply (simp add: hypreal_eq_minus_iff [symmetric]) done lemma number_of_approx_iff [simp]: "(number_of v @= number_of w) = (number_of v = (number_of w :: hypreal))" by (auto simp add: SReal_approx_iff) (*And also for 0 @= #nn and 1 @= #nn, #nn @= 0 and #nn @= 1.*) lemma [simp]: "(0 @= number_of w) = ((number_of w :: hypreal) = 0)" "(number_of w @= 0) = ((number_of w :: hypreal) = 0)" "(1 @= number_of w) = ((number_of w :: hypreal) = 1)" "(number_of w @= 1) = ((number_of w :: hypreal) = 1)" "~ (0 @= 1)" "~ (1 @= 0)" by (auto simp only: SReal_number_of SReal_approx_iff Reals_0 Reals_1) lemma hypreal_of_real_approx_iff [simp]: "(hypreal_of_real k @= hypreal_of_real m) = (k = m)" apply auto apply (rule inj_hypreal_of_real [THEN injD]) apply (rule SReal_approx_iff [THEN iffD1], auto) done lemma hypreal_of_real_approx_number_of_iff [simp]: "(hypreal_of_real k @= number_of w) = (k = number_of w)" by (subst hypreal_of_real_approx_iff [symmetric], auto) (*And also for 0 and 1.*) (*And also for 0 @= #nn and 1 @= #nn, #nn @= 0 and #nn @= 1.*) lemma [simp]: "(hypreal_of_real k @= 0) = (k = 0)" "(hypreal_of_real k @= 1) = (k = 1)" by (simp_all add: hypreal_of_real_approx_iff [symmetric]) lemma approx_unique_real: "[| r ∈ 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*} (* 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) done lemma lemma_st_part_ub: "x ∈ 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) done lemma lemma_st_part_nonempty: "x ∈ HFinite ==> ∃y. y ∈ {s. s ∈ Reals & s < x}" apply (drule HFiniteD, safe) apply (drule SReal_minus) apply (rule_tac x = "-t" in exI) apply (auto simp add: abs_less_iff) done lemma lemma_st_part_subset: "{s. s ∈ Reals & s < x} ⊆ Reals" by auto lemma lemma_st_part_lub: "x ∈ 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 safe apply (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]) done lemma lemma_st_part_le1: "[| x ∈ 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_tac x = t in SReal_add, assumption) apply (drule_tac y = "t + r" in isLubD1 [THEN setleD], auto) done lemma hypreal_setle_less_trans: "!!x::hypreal. [| S *<= x; x < y |] ==> S *<= y" apply (simp add: setle_def) apply (auto dest!: bspec order_le_less_trans intro: order_less_imp_le) done lemma hypreal_gt_isUb: "!!x::hypreal. [| isUb R S x; x < y; y ∈ R |] ==> isUb R S y" apply (simp add: isUb_def) apply (blast intro: hypreal_setle_less_trans) done lemma lemma_st_part_gt_ub: "[| x ∈ 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]) done lemma lemma_st_part_le2: "[| x ∈ 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 SReal_minus, drule_tac x = t in SReal_add, assumption) apply (drule lemma_st_part_gt_ub, assumption+) apply (drule isLub_le_isUb, assumption) apply (drule lemma_minus_le_zero) apply (auto dest: order_less_le_trans) done lemma lemma_st_part1a: "[| x ∈ 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) done lemma lemma_st_part2a: "[| x ∈ 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) done lemma 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) done lemma lemma_st_part_not_eq1: "[| x ∈ HFinite; isLub Reals {s. s ∈ Reals & s < x} t; r ∈ Reals; 0 < r |] ==> x + -t ≠ r" apply auto apply (frule isLubD1a [THEN SReal_minus]) apply (drule SReal_add_cancel, assumption) apply (drule_tac x = x in lemma_SReal_lub) apply (drule hypreal_isLub_unique, assumption, auto) done lemma lemma_st_part_not_eq2: "[| x ∈ HFinite; isLub Reals {s. s ∈ Reals & s < x} t; r ∈ Reals; 0 < r |] ==> -(x + -t) ≠ r" apply (auto) apply (frule isLubD1a) apply (drule SReal_add_cancel, assumption) apply (drule_tac x = "-x" in SReal_minus, simp) apply (drule_tac x = x in lemma_SReal_lub) apply (drule hypreal_isLub_unique, assumption, auto) done lemma lemma_st_part_major: "[| x ∈ 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) done lemma lemma_st_part_major2: "[| x ∈ 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 ∈ 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) done lemma st_part_Ex: "x ∈ HFinite ==> ∃t ∈ Reals. x @= t" apply (simp add: approx_def Infinitesimal_def) apply (drule lemma_st_part_Ex, auto) done text{*There is a unique real infinitely close*} lemma st_part_Ex1: "x ∈ HFinite ==> EX! t. 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) done subsection{* 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) done lemma HFinite_not_HInfinite: assumes x: "x ∈ HFinite" shows "x ∉ HInfinite" proof assume x': "x ∈ HInfinite" with x have "x ∈ HFinite ∩ HInfinite" by blast thus False by auto qed lemma not_HFinite_HInfinite: "x∉ HFinite ==> x ∈ HInfinite" apply (simp add: HInfinite_def HFinite_def, auto) apply (drule_tac x = "r + 1" in bspec) apply (auto) done lemma HInfinite_HFinite_disj: "x ∈ HInfinite | x ∈ HFinite" by (blast intro: not_HFinite_HInfinite) lemma HInfinite_HFinite_iff: "(x ∈ HInfinite) = (x ∉ HFinite)" by (blast dest: HFinite_not_HInfinite not_HFinite_HInfinite) lemma HFinite_HInfinite_iff: "(x ∈ HFinite) = (x ∉ HInfinite)" 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" apply (cut_tac x = "inverse x" in HInfinite_HFinite_disj) apply (auto dest!: HInfinite_inverse_Infinitesimal) done lemma HFinite_inverse2: "x ∈ HFinite - Infinitesimal ==> inverse x ∈ HFinite" by (blast intro: HFinite_inverse) (* stronger statement possible in fact *) lemma Infinitesimal_inverse_HFinite: "x ∉ Infinitesimal ==> inverse(x) ∈ HFinite" apply (drule HInfinite_diff_HFinite_Infinitesimal_disj) apply (blast intro: HFinite_inverse HInfinite_inverse_Infinitesimal Infinitesimal_subset_HFinite [THEN subsetD]) done lemma HFinite_not_Infinitesimal_inverse: "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) done lemma approx_inverse: "[| 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 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" apply (auto intro: approx_inverse approx_sym Infinitesimal_add_approx_self) done lemma inverse_add_Infinitesimal_approx2: "[| x ∈ HFinite - Infinitesimal; h ∈ Infinitesimal |] ==> inverse(h + x) @= inverse x" apply (rule add_commute [THEN subst]) apply (blast intro: inverse_add_Infinitesimal_approx) done lemma inverse_add_Infinitesimal_approx_Infinitesimal: "[| 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]) done lemma Infinitesimal_square_iff: "(x ∈ Infinitesimal) = (x*x ∈ Infinitesimal)" apply (auto intro: Infinitesimal_mult) apply (rule ccontr, frule Infinitesimal_inverse_HFinite) apply (frule not_Infinitesimal_not_zero) apply (auto dest: Infinitesimal_HFinite_mult simp add: mult_assoc) done declare Infinitesimal_square_iff [symmetric, simp] lemma HFinite_square_iff [simp]: "(x*x ∈ HFinite) = (x ∈ HFinite)" apply (auto intro: HFinite_mult) apply (auto dest: HInfinite_mult simp add: HFinite_HInfinite_iff) done lemma HInfinite_square_iff [simp]: "(x*x ∈ HInfinite) = (x ∈ HInfinite)" by (auto simp add: HInfinite_HFinite_iff) lemma approx_HFinite_mult_cancel: "[| a: HFinite-Infinitesimal; a* w @= a*z |] ==> w @= z" apply safe apply (frule HFinite_inverse, assumption) apply (drule not_Infinitesimal_not_zero) apply (auto dest: approx_mult2 simp add: mult_assoc [symmetric]) done lemma approx_HFinite_mult_cancel_iff1: "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) done lemma 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) done lemma HInfinite_ge_HInfinite: "[| x ∈ HInfinite; x ≤ y; 0 ≤ x |] ==> y ∈ HInfinite" by (auto intro: HFinite_bounded simp add: HInfinite_HFinite_iff) lemma Infinitesimal_inverse_HInfinite: "[| x ∈ Infinitesimal; x ≠ 0 |] ==> inverse x ∈ HInfinite" apply (rule ccontr, drule HFinite_HInfinite_iff [THEN iffD2]) apply (auto dest: Infinitesimal_HFinite_mult2) done lemma HInfinite_HFinite_not_Infinitesimal_mult: "[| x ∈ HInfinite; y ∈ HFinite - Infinitesimal |] ==> x * y ∈ HInfinite" apply (rule ccontr, drule HFinite_HInfinite_iff [THEN iffD2]) apply (frule HFinite_Infinitesimal_not_zero) apply (drule HFinite_not_Infinitesimal_inverse) apply (safe, drule HFinite_mult) apply (auto simp add: mult_assoc HFinite_HInfinite_iff) done lemma HInfinite_HFinite_not_Infinitesimal_mult2: "[| x ∈ HInfinite; y ∈ HFinite - Infinitesimal |] ==> y * x ∈ HInfinite" by (auto simp add: mult_commute HInfinite_HFinite_not_Infinitesimal_mult) lemma HInfinite_gt_SReal: "[| x ∈ 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 ∈ 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) done lemma approx_hrabs_disj: "abs x @= 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) 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]) done lemma monad_zero_hrabs_iff: "(x ∈ 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]) done 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" apply (simp (no_asm)) apply (simp add: approx_monad_iff) done lemma approx_subset_monad2: "x @= y ==> {x,y} ≤ monad y" apply (drule approx_sym) apply (fast dest: approx_subset_monad) done 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" apply (simp add: monad_def) apply (blast intro!: approx_sym) done lemma 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) done lemma Infinitesimal_approx_hrabs: "[| x @= y; x ∈ 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) done lemma less_Infinitesimal_less: "[| 0 < x; x ∉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) done lemma Ball_mem_monad_gt_zero: "[| 0 < x; 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) done lemma Ball_mem_monad_less_zero: "[| x < 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) done lemma lemma_approx_gt_zero: "[|0 < x; x ∉ Infinitesimal; x @= y|] ==> 0 < y" by (blast dest: Ball_mem_monad_gt_zero approx_subset_monad) lemma lemma_approx_less_zero: "[|x < 0; x ∉ Infinitesimal; x @= y|] ==> y < 0" by (blast dest: Ball_mem_monad_less_zero approx_subset_monad) theorem approx_hrabs: "x @= y ==> abs x @= abs y" apply (case_tac "x ∈ Infinitesimal") apply (simp add: Infinitesimal_approx_hrabs) apply (rule linorder_cases [of 0 x]) apply (frule lemma_approx_gt_zero [of x y]) apply (auto simp add: lemma_approx_less_zero [of x y] abs_of_neg) done lemma approx_hrabs_zero_cancel: "abs(x) @= 0 ==> x @= 0" apply (cut_tac x = x in hrabs_disj) apply (auto dest: approx_minus) done lemma approx_hrabs_add_Infinitesimal: "e ∈ Infinitesimal ==> abs x @= abs(x+e)" by (fast intro: approx_hrabs Infinitesimal_add_approx_self) lemma approx_hrabs_add_minus_Infinitesimal: "e ∈ Infinitesimal ==> abs x @= abs(x + -e)" by (fast intro: approx_hrabs Infinitesimal_add_minus_approx_self) lemma hrabs_add_Infinitesimal_cancel: "[| e ∈ 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) done lemma hrabs_add_minus_Infinitesimal_cancel: "[| e ∈ 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) done (* 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) done lemma 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: hypreal_of_real_hrabs) done lemma 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) done lemma 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) done 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" 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 |] ==> hypreal_of_real x + h ≠ 0" apply auto apply (subgoal_tac "h = - hypreal_of_real x", auto) done lemma Infinitesimal_square_cancel [simp]: "x*x + y*y ∈ Infinitesimal ==> x*x ∈ Infinitesimal" apply (rule Infinitesimal_interval2) apply (rule_tac [3] zero_le_square, assumption) apply (auto simp add: zero_le_square) done lemma HFinite_square_cancel [simp]: "x*x + y*y ∈ HFinite ==> x*x ∈ HFinite" apply (rule HFinite_bounded, assumption) apply (auto simp add: zero_le_square) done lemma Infinitesimal_square_cancel2 [simp]: "x*x + y*y ∈ Infinitesimal ==> y*y ∈ Infinitesimal" apply (rule Infinitesimal_square_cancel) apply (rule add_commute [THEN subst]) apply (simp (no_asm)) done lemma HFinite_square_cancel2 [simp]: "x*x + y*y ∈ HFinite ==> y*y ∈ HFinite" apply (rule HFinite_square_cancel) apply (rule add_commute [THEN subst]) apply (simp (no_asm)) done lemma Infinitesimal_sum_square_cancel [simp]: "x*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) done lemma HFinite_sum_square_cancel [simp]: "x*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) done lemma Infinitesimal_sum_square_cancel2 [simp]: "y*y + x*x + z*z ∈ Infinitesimal ==> x*x ∈ Infinitesimal" apply (rule Infinitesimal_sum_square_cancel) apply (simp add: add_ac) done lemma HFinite_sum_square_cancel2 [simp]: "y*y + x*x + z*z ∈ HFinite ==> x*x ∈ HFinite" apply (rule HFinite_sum_square_cancel) apply (simp add: add_ac) done lemma Infinitesimal_sum_square_cancel3 [simp]: "z*z + y*y + x*x ∈ Infinitesimal ==> x*x ∈ Infinitesimal" apply (rule Infinitesimal_sum_square_cancel) apply (simp add: add_ac) done lemma HFinite_sum_square_cancel3 [simp]: "z*z + y*y + x*x ∈ HFinite ==> x*x ∈ HFinite" apply (rule HFinite_sum_square_cancel) apply (simp add: add_ac) done lemma 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) done lemma 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]) done subsection{* 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) done lemma 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) done lemma st_HFinite: "x ∈ HFinite ==> st x ∈ HFinite" by (erule st_SReal [THEN SReal_subset_HFinite [THEN subsetD]]) lemma st_SReal_eq: "x ∈ Reals ==> st x = x" apply (simp add: st_def) apply (rule some_equality) apply (fast intro: SReal_subset_HFinite [THEN subsetD]) apply (blast dest: SReal_approx_iff [THEN iffD1]) done 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 ∈ HFinite" and "y ∈ HFinite" and "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 prems) with prems 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 ∈ Reals; e ∈ Infinitesimal |] ==> st(x + e) = x" apply (frule st_SReal_eq [THEN subst]) prefer 2 apply assumption apply (frule SReal_subset_HFinite [THEN subsetD]) apply (frule Infinitesimal_subset_HFinite [THEN subsetD]) apply (drule st_SReal_eq) apply (rule approx_st_eq) apply (auto intro: HFinite_add simp add: Infinitesimal_add_approx_self [THEN approx_sym]) done lemma st_Infinitesimal_add_SReal2: "[| x ∈ Reals; e ∈ Infinitesimal |] ==> st(e + x) = x" apply (rule add_commute [THEN subst]) apply (blast intro!: st_Infinitesimal_add_SReal) done 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: assumes x: "x ∈ HFinite" and y: "y ∈ HFinite" shows "st (x + y) = st(x) + st(y)" proof - from HFinite_st_Infinitesimal_add [OF x] obtain ex where ex: "ex ∈ Infinitesimal" "st x + ex = x" by (blast intro: sym) from HFinite_st_Infinitesimal_add [OF y] obtain ey where ey: "ey ∈ Infinitesimal" "st y + ey = y" by (blast intro: sym) have "st (x + y) = st ((st x + ex) + (st y + ey))" by (simp add: ex ey) also have "... = st ((ex + ey) + (st x + st y))" by (simp add: add_ac) also have "... = st x + st y" by (simp add: prems st_SReal Infinitesimal_add st_Infinitesimal_add_SReal2) finally show ?thesis . qed lemma st_number_of [simp]: "st (number_of w) = number_of w" by (rule SReal_number_of [THEN st_SReal_eq]) (*the theorem above for the special cases of zero and one*) lemma [simp]: "st 0 = 0" "st 1 = 1" by (simp_all add: st_SReal_eq) lemma st_minus: assumes "y ∈ HFinite" shows "st(-y) = -st(y)" proof - have "st (- y) + st y = 0" by (simp add: prems st_add [symmetric] HFinite_minus_iff) thus ?thesis by arith qed lemma st_diff: "[| x ∈ HFinite; y ∈ HFinite |] ==> st (x-y) = st(x) - st(y)" apply (simp add: diff_def) apply (frule_tac y1 = y in st_minus [symmetric]) apply (drule_tac x1 = y in HFinite_minus_iff [THEN iffD2]) apply (simp (no_asm_simp) add: st_add) done lemma lemma_st_mult: "[| x ∈ HFinite; y ∈ HFinite; e ∈ Infinitesimal; ea ∈ Infinitesimal |] ==> e*y + x*ea + e*ea ∈ Infinitesimal" apply (frule_tac x = e and y = y in Infinitesimal_HFinite_mult) apply (frule_tac [2] x = ea and y = x in Infinitesimal_HFinite_mult) apply (drule_tac [3] Infinitesimal_mult) apply (auto intro: Infinitesimal_add simp add: add_ac mult_ac) done lemma st_mult: "[| x ∈ HFinite; y ∈ HFinite |] ==> st (x * y) = st(x) * st(y)" apply (frule HFinite_st_Infinitesimal_add) apply (frule_tac x = y in HFinite_st_Infinitesimal_add, safe) apply (subgoal_tac "st (x * y) = st ((st x + e) * (st y + ea))") apply (drule_tac [2] sym, drule_tac [2] sym) prefer 2 apply simp apply (erule_tac V = "x = st x + e" in thin_rl) apply (erule_tac V = "y = st y + ea" in thin_rl) apply (simp add: left_distrib right_distrib) apply (drule st_SReal)+ apply (simp (no_asm_use) add: add_assoc) apply (rule st_Infinitesimal_add_SReal) apply (blast intro!: SReal_mult) apply (drule SReal_subset_HFinite [THEN subsetD])+ apply (rule add_assoc [THEN subst]) apply (blast intro!: lemma_st_mult) done lemma st_Infinitesimal: "x ∈ Infinitesimal ==> st x = 0" apply (subst numeral_0_eq_0 [symmetric]) apply (rule st_number_of [THEN subst]) apply (rule approx_st_eq) apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD] simp add: mem_infmal_iff [symmetric]) done 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) done lemma st_divide [simp]: "[| x ∈ HFinite; y ∈ HFinite; st y ≠ 0 |] ==> st(x/y) = (st x) / (st y)" by (simp add: divide_inverse st_mult st_not_Infinitesimal HFinite_inverse st_inverse) lemma st_idempotent [simp]: "x ∈ HFinite ==> st(st(x)) = st(x)" by (blast intro: st_HFinite st_approx_self approx_st_eq) 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) done lemma 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) done lemma 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]) done lemma st_zero_le: "[| 0 ≤ x; x ∈ HFinite |] ==> 0 ≤ st x" apply (subst numeral_0_eq_0 [symmetric]) apply (rule st_number_of [THEN subst]) apply (rule st_le, auto) done lemma st_zero_ge: "[| x ≤ 0; x ∈ HFinite |] ==> st x ≤ 0" apply (subst numeral_0_eq_0 [symmetric]) apply (rule st_number_of [THEN subst]) apply (rule st_le, auto) done lemma 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]) done subsection{*Alternative Definitions for @{term HFinite} using Free Ultrafilter*} lemma FreeUltrafilterNat_Rep_hypreal: "[| X ∈ Rep_star x; Y ∈ Rep_star x |] ==> {n. X n = Y n} ∈ FreeUltrafilterNat" by (cases x, unfold star_n_def, auto, ultra) lemma HFinite_FreeUltrafilterNat: "x ∈ HFinite ==> ∃X ∈ Rep_star x. ∃u. {n. abs (X n) < u} ∈ FreeUltrafilterNat" apply (cases x) apply (auto simp add: HFinite_def abs_less_iff minus_less_iff [of x] star_of_def star_n_less SReal_iff star_n_minus) apply (rule_tac x=X in bexI) apply (rule_tac x=y in exI, ultra) apply simp done lemma FreeUltrafilterNat_HFinite: "∃X ∈ Rep_star x. ∃u. {n. abs (X n) < u} ∈ FreeUltrafilterNat ==> x ∈ HFinite" apply (cases x) apply (auto simp add: HFinite_def abs_less_iff minus_less_iff [of x]) apply (rule_tac x = "hypreal_of_real u" in bexI) apply (auto simp add: star_n_less SReal_iff star_n_minus star_of_def) apply ultra+ done lemma HFinite_FreeUltrafilterNat_iff: "(x ∈ HFinite) = (∃X ∈ Rep_star x. ∃u. {n. abs (X n) < u} ∈ FreeUltrafilterNat)" by (blast intro!: HFinite_FreeUltrafilterNat FreeUltrafilterNat_HFinite) subsection{*Alternative Definitions for @{term HInfinite} using Free Ultrafilter*} lemma lemma_Compl_eq: "- {n. (u::real) < abs (xa n)} = {n. abs (xa n) ≤ u}" by auto lemma lemma_Compl_eq2: "- {n. abs (xa n) < (u::real)} = {n. u ≤ abs (xa n)}" by auto lemma lemma_Int_eq1: "{n. abs (xa n) ≤ (u::real)} Int {n. u ≤ abs (xa n)} = {n. abs(xa n) = u}" by auto lemma lemma_FreeUltrafilterNat_one: "{n. abs (xa n) = u} ≤ {n. abs (xa n) < u + (1::real)}" by auto (*------------------------------------- Exclude this type of sets from free ultrafilter for Infinite numbers! -------------------------------------*) lemma FreeUltrafilterNat_const_Finite: "[| xa: Rep_star x; {n. abs (xa n) = u} ∈ FreeUltrafilterNat |] ==> x ∈ HFinite" apply (rule FreeUltrafilterNat_HFinite) apply (rule_tac x = xa in bexI) apply (rule_tac x = "u + 1" in exI) apply (ultra, assumption) done lemma HInfinite_FreeUltrafilterNat: "x ∈ HInfinite ==> ∃X ∈ Rep_star x. ∀u. {n. u < abs (X n)} ∈ FreeUltrafilterNat" apply (frule HInfinite_HFinite_iff [THEN iffD1]) apply (cut_tac x = x in Rep_hypreal_nonempty) apply (auto simp del: Rep_hypreal_nonempty simp add: HFinite_FreeUltrafilterNat_iff Bex_def) apply (drule spec)+ apply auto apply (drule_tac x = u in spec) apply (drule FreeUltrafilterNat_Compl_mem)+ apply (drule FreeUltrafilterNat_Int, assumption) apply (simp add: lemma_Compl_eq lemma_Compl_eq2 lemma_Int_eq1) apply (auto dest: FreeUltrafilterNat_const_Finite simp add: HInfinite_HFinite_iff [THEN iffD1]) done lemma lemma_Int_HI: "{n. abs (Xa n) < u} Int {n. X n = Xa n} ⊆ {n. abs (X n) < (u::real)}" by auto lemma lemma_Int_HIa: "{n. u < abs (X n)} Int {n. abs (X n) < (u::real)} = {}" by (auto intro: order_less_asym) lemma FreeUltrafilterNat_HInfinite: "∃X ∈ Rep_star x. ∀u. {n. u < abs (X n)} ∈ FreeUltrafilterNat ==> x ∈ HInfinite" apply (rule HInfinite_HFinite_iff [THEN iffD2]) apply (safe, drule HFinite_FreeUltrafilterNat, auto) apply (drule_tac x = u in spec) apply (drule FreeUltrafilterNat_Rep_hypreal, assumption) apply (drule_tac Y = "{n. X n = Xa n}" in FreeUltrafilterNat_Int, simp) apply (drule lemma_Int_HI [THEN [2] FreeUltrafilterNat_subset]) apply (drule_tac Y = "{n. abs (X n) < u}" in FreeUltrafilterNat_Int) apply (auto simp add: lemma_Int_HIa) done lemma HInfinite_FreeUltrafilterNat_iff: "(x ∈ HInfinite) = (∃X ∈ Rep_star x. ∀u. {n. u < abs (X n)} ∈ FreeUltrafilterNat)" by (blast intro!: HInfinite_FreeUltrafilterNat FreeUltrafilterNat_HInfinite) subsection{*Alternative Definitions for @{term Infinitesimal} using Free Ultrafilter*} lemma Infinitesimal_FreeUltrafilterNat: "x ∈ Infinitesimal ==> ∃X ∈ Rep_star x. ∀u. 0 < u --> {n. abs (X n) < u} ∈ FreeUltrafilterNat" apply (simp add: Infinitesimal_def) apply (auto simp add: abs_less_iff minus_less_iff [of x]) apply (cases x) apply (auto, rule bexI [OF _ Rep_star_star_n], safe) apply (drule star_of_less [THEN iffD2]) apply (drule_tac x = "hypreal_of_real u" in bspec, auto) apply (auto simp add: star_n_less star_n_minus star_of_def, ultra) done lemma FreeUltrafilterNat_Infinitesimal: "∃X ∈ Rep_star x. ∀u. 0 < u --> {n. abs (X n) < u} ∈ FreeUltrafilterNat ==> x ∈ Infinitesimal" apply (simp add: Infinitesimal_def) apply (cases x) apply (auto simp add: abs_less_iff abs_interval_iff minus_less_iff [of x]) apply (auto simp add: SReal_iff) apply (drule_tac [!] x=y in spec) apply (auto simp add: star_n_less star_n_minus star_of_def, ultra+) done lemma Infinitesimal_FreeUltrafilterNat_iff: "(x ∈ Infinitesimal) = (∃X ∈ Rep_star x. ∀u. 0 < u --> {n. abs (X n) < u} ∈ FreeUltrafilterNat)" 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) done lemma of_nat_in_Reals [simp]: "(of_nat n::hypreal) ∈ \<real>" apply (induct n) apply (simp_all) done lemma lemma_Infinitesimal2: "(∀r ∈ Reals. 0 < r --> x < r) = (∀n. x < inverse(hypreal_of_nat (Suc n)))" apply safe apply (drule_tac x = "inverse (hypreal_of_real (real (Suc n))) " in bspec) apply (simp (no_asm_use) add: SReal_inverse) 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 assumption apply (simp add: real_of_nat_Suc_gt_zero hypreal_of_nat_eq) apply (auto dest!: reals_Archimedean simp add: SReal_iff) apply (drule star_of_less [THEN iffD2]) apply (simp add: real_of_nat_Suc_gt_zero hypreal_of_nat_eq) apply (blast intro: order_less_trans) done lemma Infinitesimal_hypreal_of_nat_iff: "Infinitesimal = {x. ∀n. abs x < inverse (hypreal_of_nat (Suc n))}" apply (simp add: Infinitesimal_def) apply (auto simp add: lemma_Infinitesimal2) done subsection{*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) done lemma 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) done lemma lemma_real_le_Un_eq: "{n. f n ≤ u} = {n. f n < u} Un {n. u = (f n :: real)}" by (auto dest: order_le_imp_less_or_eq simp add: order_less_imp_le) lemma finite_real_of_nat_le_real: "finite {n::nat. real n ≤ u}" by (auto simp add: lemma_real_le_Un_eq lemma_finite_omega_set finite_real_of_nat_less_real) lemma finite_rabs_real_of_nat_le_real: "finite {n::nat. abs(real n) ≤ u}" apply (simp (no_asm) add: real_of_nat_Suc_gt_zero finite_real_of_nat_le_real) done lemma 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_Compl_mem) apply (subgoal_tac "- {n::nat. u < real n} = {n. real n ≤ u}") prefer 2 apply force apply (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_Compl_mem simp add: Compl_real_le_eq) done theorem HInfinite_omega [simp]: "omega ∈ HInfinite" apply (simp add: omega_def star_n_def) apply (auto intro!: FreeUltrafilterNat_HInfinite) apply (rule bexI) apply (rule_tac [2] lemma_starrel_refl, auto) apply (simp (no_asm) add: 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: real_mult_commute) done lemma 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) done lemma lemma_real_le_Un_eq2: "{n. u ≤ inverse(real(Suc n))} = {n. u < inverse(real(Suc n))} Un {n. u = inverse(real(Suc n))}" apply (auto dest: order_le_imp_less_or_eq simp add: order_less_imp_le) done lemma real_of_nat_inverse_le_iff: "(inverse (real(Suc n)) ≤ r) = (1 ≤ r * real(Suc n))" apply (simp (no_asm) add: linorder_not_less [symmetric]) apply (simp (no_asm) add: inverse_eq_divide) apply (subst pos_less_divide_eq) apply (simp (no_asm) add: real_of_nat_Suc_gt_zero) apply (simp (no_asm) add: real_mult_commute) done lemma 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 real_not_refl2 [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) done lemma finite_inverse_real_of_posnat_ge_real: "0 < u ==> finite {n. u ≤ inverse(real(Suc n))}" by (auto simp add: lemma_real_le_Un_eq2 lemma_finite_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) done lemma 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_Compl_mem simp add: Compl_le_inverse_eq) done text{* Example where we get a hyperreal from a real sequence for which a particular property holds. The theorem is used in proofs about equivalence of nonstandard and standard neighbourhoods. Also used for equivalence of nonstandard ans standard definitions of pointwise limit.*} (*----------------------------------------------------- |X(n) - x| < 1/n ==> [<X n>] - hypreal_of_real x| ∈ Infinitesimal -----------------------------------------------------*) lemma real_seq_to_hypreal_Infinitesimal: "∀n. abs(X n + -x) < inverse(real(Suc n)) ==> star_n X + -hypreal_of_real x ∈ Infinitesimal" apply (auto intro!: bexI dest: FreeUltrafilterNat_inverse_real_of_posnat FreeUltrafilterNat_all FreeUltrafilterNat_Int intro: order_less_trans FreeUltrafilterNat_subset simp add: star_n_minus star_of_def star_n_add Infinitesimal_FreeUltrafilterNat_iff star_n_inverse) done lemma real_seq_to_hypreal_approx: "∀n. abs(X n + -x) < inverse(real(Suc n)) ==> star_n X @= hypreal_of_real x" apply (subst approx_minus_iff) apply (rule mem_infmal_iff [THEN subst]) apply (erule real_seq_to_hypreal_Infinitesimal) done lemma real_seq_to_hypreal_approx2: "∀n. abs(x + -X n) < inverse(real(Suc n)) ==> star_n X @= hypreal_of_real x" apply (simp add: abs_minus_add_cancel real_seq_to_hypreal_approx) done lemma real_seq_to_hypreal_Infinitesimal2: "∀n. abs(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_all FreeUltrafilterNat_Int intro: order_less_trans FreeUltrafilterNat_subset simp add: Infinitesimal_FreeUltrafilterNat_iff star_n_minus star_n_add star_n_inverse) ML {* val Infinitesimal_def = thm"Infinitesimal_def"; val HFinite_def = thm"HFinite_def"; val HInfinite_def = thm"HInfinite_def"; val st_def = thm"st_def"; val monad_def = thm"monad_def"; val galaxy_def = thm"galaxy_def"; val approx_def = thm"approx_def"; val SReal_def = thm"SReal_def"; val Infinitesimal_approx_minus = thm "Infinitesimal_approx_minus"; val approx_monad_iff = thm "approx_monad_iff"; val Infinitesimal_approx = thm "Infinitesimal_approx"; val approx_add = thm "approx_add"; val approx_minus = thm "approx_minus"; val approx_minus2 = thm "approx_minus2"; val approx_minus_cancel = thm "approx_minus_cancel"; val approx_add_minus = thm "approx_add_minus"; val approx_mult1 = thm "approx_mult1"; val approx_mult2 = thm "approx_mult2"; val approx_mult_subst = thm "approx_mult_subst"; val approx_mult_subst2 = thm "approx_mult_subst2"; val approx_mult_subst_SReal = thm "approx_mult_subst_SReal"; val approx_eq_imp = thm "approx_eq_imp"; val Infinitesimal_minus_approx = thm "Infinitesimal_minus_approx"; val bex_Infinitesimal_iff = thm "bex_Infinitesimal_iff"; val bex_Infinitesimal_iff2 = thm "bex_Infinitesimal_iff2"; val Infinitesimal_add_approx = thm "Infinitesimal_add_approx"; val Infinitesimal_add_approx_self = thm "Infinitesimal_add_approx_self"; val Infinitesimal_add_approx_self2 = thm "Infinitesimal_add_approx_self2"; val Infinitesimal_add_minus_approx_self = thm "Infinitesimal_add_minus_approx_self"; val Infinitesimal_add_cancel = thm "Infinitesimal_add_cancel"; val Infinitesimal_add_right_cancel = thm "Infinitesimal_add_right_cancel"; val approx_add_left_cancel = thm "approx_add_left_cancel"; val approx_add_right_cancel = thm "approx_add_right_cancel"; val approx_add_mono1 = thm "approx_add_mono1"; val approx_add_mono2 = thm "approx_add_mono2"; val approx_add_left_iff = thm "approx_add_left_iff"; val approx_add_right_iff = thm "approx_add_right_iff"; val approx_HFinite = thm "approx_HFinite"; val approx_hypreal_of_real_HFinite = thm "approx_hypreal_of_real_HFinite"; val approx_mult_HFinite = thm "approx_mult_HFinite"; val approx_mult_hypreal_of_real = thm "approx_mult_hypreal_of_real"; val approx_SReal_mult_cancel_zero = thm "approx_SReal_mult_cancel_zero"; val approx_mult_SReal1 = thm "approx_mult_SReal1"; val approx_mult_SReal2 = thm "approx_mult_SReal2"; val approx_mult_SReal_zero_cancel_iff = thm "approx_mult_SReal_zero_cancel_iff"; val approx_SReal_mult_cancel = thm "approx_SReal_mult_cancel"; val approx_SReal_mult_cancel_iff1 = thm "approx_SReal_mult_cancel_iff1"; val approx_le_bound = thm "approx_le_bound"; val Infinitesimal_less_SReal = thm "Infinitesimal_less_SReal"; val Infinitesimal_less_SReal2 = thm "Infinitesimal_less_SReal2"; val SReal_not_Infinitesimal = thm "SReal_not_Infinitesimal"; val SReal_minus_not_Infinitesimal = thm "SReal_minus_not_Infinitesimal"; val SReal_Int_Infinitesimal_zero = thm "SReal_Int_Infinitesimal_zero"; val SReal_Infinitesimal_zero = thm "SReal_Infinitesimal_zero"; val SReal_HFinite_diff_Infinitesimal = thm "SReal_HFinite_diff_Infinitesimal"; val hypreal_of_real_HFinite_diff_Infinitesimal = thm "hypreal_of_real_HFinite_diff_Infinitesimal"; val hypreal_of_real_Infinitesimal_iff_0 = thm "hypreal_of_real_Infinitesimal_iff_0"; val number_of_not_Infinitesimal = thm "number_of_not_Infinitesimal"; val one_not_Infinitesimal = thm "one_not_Infinitesimal"; val approx_SReal_not_zero = thm "approx_SReal_not_zero"; val HFinite_diff_Infinitesimal_approx = thm "HFinite_diff_Infinitesimal_approx"; val Infinitesimal_ratio = thm "Infinitesimal_ratio"; val SReal_approx_iff = thm "SReal_approx_iff"; val number_of_approx_iff = thm "number_of_approx_iff"; val hypreal_of_real_approx_iff = thm "hypreal_of_real_approx_iff"; val hypreal_of_real_approx_number_of_iff = thm "hypreal_of_real_approx_number_of_iff"; val approx_unique_real = thm "approx_unique_real"; val hypreal_isLub_unique = thm "hypreal_isLub_unique"; val hypreal_setle_less_trans = thm "hypreal_setle_less_trans"; val hypreal_gt_isUb = thm "hypreal_gt_isUb"; val st_part_Ex = thm "st_part_Ex"; val st_part_Ex1 = thm "st_part_Ex1"; val HFinite_Int_HInfinite_empty = thm "HFinite_Int_HInfinite_empty"; val HFinite_not_HInfinite = thm "HFinite_not_HInfinite"; val not_HFinite_HInfinite = thm "not_HFinite_HInfinite"; val HInfinite_HFinite_disj = thm "HInfinite_HFinite_disj"; val HInfinite_HFinite_iff = thm "HInfinite_HFinite_iff"; val HFinite_HInfinite_iff = thm "HFinite_HInfinite_iff"; val HInfinite_diff_HFinite_Infinitesimal_disj = thm "HInfinite_diff_HFinite_Infinitesimal_disj"; val HFinite_inverse = thm "HFinite_inverse"; val HFinite_inverse2 = thm "HFinite_inverse2"; val Infinitesimal_inverse_HFinite = thm "Infinitesimal_inverse_HFinite"; val HFinite_not_Infinitesimal_inverse = thm "HFinite_not_Infinitesimal_inverse"; val approx_inverse = thm "approx_inverse"; val hypreal_of_real_approx_inverse = thm "hypreal_of_real_approx_inverse"; val inverse_add_Infinitesimal_approx = thm "inverse_add_Infinitesimal_approx"; val inverse_add_Infinitesimal_approx2 = thm "inverse_add_Infinitesimal_approx2"; val inverse_add_Infinitesimal_approx_Infinitesimal = thm "inverse_add_Infinitesimal_approx_Infinitesimal"; val Infinitesimal_square_iff = thm "Infinitesimal_square_iff"; val HFinite_square_iff = thm "HFinite_square_iff"; val HInfinite_square_iff = thm "HInfinite_square_iff"; val approx_HFinite_mult_cancel = thm "approx_HFinite_mult_cancel"; val approx_HFinite_mult_cancel_iff1 = thm "approx_HFinite_mult_cancel_iff1"; val approx_hrabs_disj = thm "approx_hrabs_disj"; val monad_hrabs_Un_subset = thm "monad_hrabs_Un_subset"; val Infinitesimal_monad_eq = thm "Infinitesimal_monad_eq"; val mem_monad_iff = thm "mem_monad_iff"; val Infinitesimal_monad_zero_iff = thm "Infinitesimal_monad_zero_iff"; val monad_zero_minus_iff = thm "monad_zero_minus_iff"; val monad_zero_hrabs_iff = thm "monad_zero_hrabs_iff"; val mem_monad_self = thm "mem_monad_self"; val approx_subset_monad = thm "approx_subset_monad"; val approx_subset_monad2 = thm "approx_subset_monad2"; val mem_monad_approx = thm "mem_monad_approx"; val approx_mem_monad = thm "approx_mem_monad"; val approx_mem_monad2 = thm "approx_mem_monad2"; val approx_mem_monad_zero = thm "approx_mem_monad_zero"; val Infinitesimal_approx_hrabs = thm "Infinitesimal_approx_hrabs"; val less_Infinitesimal_less = thm "less_Infinitesimal_less"; val Ball_mem_monad_gt_zero = thm "Ball_mem_monad_gt_zero"; val Ball_mem_monad_less_zero = thm "Ball_mem_monad_less_zero"; val approx_hrabs = thm "approx_hrabs"; val approx_hrabs_zero_cancel = thm "approx_hrabs_zero_cancel"; val approx_hrabs_add_Infinitesimal = thm "approx_hrabs_add_Infinitesimal"; val approx_hrabs_add_minus_Infinitesimal = thm "approx_hrabs_add_minus_Infinitesimal"; val hrabs_add_Infinitesimal_cancel = thm "hrabs_add_Infinitesimal_cancel"; val hrabs_add_minus_Infinitesimal_cancel = thm "hrabs_add_minus_Infinitesimal_cancel"; val Infinitesimal_add_hypreal_of_real_less = thm "Infinitesimal_add_hypreal_of_real_less"; val Infinitesimal_add_hrabs_hypreal_of_real_less = thm "Infinitesimal_add_hrabs_hypreal_of_real_less"; val Infinitesimal_add_hrabs_hypreal_of_real_less2 = thm "Infinitesimal_add_hrabs_hypreal_of_real_less2"; val hypreal_of_real_le_add_Infininitesimal_cancel2 = thm"hypreal_of_real_le_add_Infininitesimal_cancel2"; val hypreal_of_real_less_Infinitesimal_le_zero = thm "hypreal_of_real_less_Infinitesimal_le_zero"; val Infinitesimal_add_not_zero = thm "Infinitesimal_add_not_zero"; val Infinitesimal_square_cancel = thm "Infinitesimal_square_cancel"; val HFinite_square_cancel = thm "HFinite_square_cancel"; val Infinitesimal_square_cancel2 = thm "Infinitesimal_square_cancel2"; val HFinite_square_cancel2 = thm "HFinite_square_cancel2"; val Infinitesimal_sum_square_cancel = thm "Infinitesimal_sum_square_cancel"; val HFinite_sum_square_cancel = thm "HFinite_sum_square_cancel"; val Infinitesimal_sum_square_cancel2 = thm "Infinitesimal_sum_square_cancel2"; val HFinite_sum_square_cancel2 = thm "HFinite_sum_square_cancel2"; val Infinitesimal_sum_square_cancel3 = thm "Infinitesimal_sum_square_cancel3"; val HFinite_sum_square_cancel3 = thm "HFinite_sum_square_cancel3"; val monad_hrabs_less = thm "monad_hrabs_less"; val mem_monad_SReal_HFinite = thm "mem_monad_SReal_HFinite"; val st_approx_self = thm "st_approx_self"; val st_SReal = thm "st_SReal"; val st_HFinite = thm "st_HFinite"; val st_SReal_eq = thm "st_SReal_eq"; val st_hypreal_of_real = thm "st_hypreal_of_real"; val st_eq_approx = thm "st_eq_approx"; val approx_st_eq = thm "approx_st_eq"; val st_eq_approx_iff = thm "st_eq_approx_iff"; val st_Infinitesimal_add_SReal = thm "st_Infinitesimal_add_SReal"; val st_Infinitesimal_add_SReal2 = thm "st_Infinitesimal_add_SReal2"; val HFinite_st_Infinitesimal_add = thm "HFinite_st_Infinitesimal_add"; val st_add = thm "st_add"; val st_number_of = thm "st_number_of"; val st_minus = thm "st_minus"; val st_diff = thm "st_diff"; val st_mult = thm "st_mult"; val st_Infinitesimal = thm "st_Infinitesimal"; val st_not_Infinitesimal = thm "st_not_Infinitesimal"; val st_inverse = thm "st_inverse"; val st_divide = thm "st_divide"; val st_idempotent = thm "st_idempotent"; val Infinitesimal_add_st_less = thm "Infinitesimal_add_st_less"; val Infinitesimal_add_st_le_cancel = thm "Infinitesimal_add_st_le_cancel"; val st_le = thm "st_le"; val st_zero_le = thm "st_zero_le"; val st_zero_ge = thm "st_zero_ge"; val st_hrabs = thm "st_hrabs"; val FreeUltrafilterNat_HFinite = thm "FreeUltrafilterNat_HFinite"; val HFinite_FreeUltrafilterNat_iff = thm "HFinite_FreeUltrafilterNat_iff"; val FreeUltrafilterNat_const_Finite = thm "FreeUltrafilterNat_const_Finite"; val FreeUltrafilterNat_HInfinite = thm "FreeUltrafilterNat_HInfinite"; val HInfinite_FreeUltrafilterNat_iff = thm "HInfinite_FreeUltrafilterNat_iff"; val Infinitesimal_FreeUltrafilterNat = thm "Infinitesimal_FreeUltrafilterNat"; val FreeUltrafilterNat_Infinitesimal = thm "FreeUltrafilterNat_Infinitesimal"; val Infinitesimal_FreeUltrafilterNat_iff = thm "Infinitesimal_FreeUltrafilterNat_iff"; val Infinitesimal_hypreal_of_nat_iff = thm "Infinitesimal_hypreal_of_nat_iff"; val Suc_Un_eq = thm "Suc_Un_eq"; val finite_nat_segment = thm "finite_nat_segment"; val finite_real_of_nat_segment = thm "finite_real_of_nat_segment"; val finite_real_of_nat_less_real = thm "finite_real_of_nat_less_real"; val finite_real_of_nat_le_real = thm "finite_real_of_nat_le_real"; val finite_rabs_real_of_nat_le_real = thm "finite_rabs_real_of_nat_le_real"; val rabs_real_of_nat_le_real_FreeUltrafilterNat = thm "rabs_real_of_nat_le_real_FreeUltrafilterNat"; val FreeUltrafilterNat_nat_gt_real = thm "FreeUltrafilterNat_nat_gt_real"; val FreeUltrafilterNat_omega = thm "FreeUltrafilterNat_omega"; val HInfinite_omega = thm "HInfinite_omega"; val Infinitesimal_epsilon = thm "Infinitesimal_epsilon"; val HFinite_epsilon = thm "HFinite_epsilon"; val epsilon_approx_zero = thm "epsilon_approx_zero"; val real_of_nat_less_inverse_iff = thm "real_of_nat_less_inverse_iff"; val finite_inverse_real_of_posnat_gt_real = thm "finite_inverse_real_of_posnat_gt_real"; val real_of_nat_inverse_le_iff = thm "real_of_nat_inverse_le_iff"; val real_of_nat_inverse_eq_iff = thm "real_of_nat_inverse_eq_iff"; val finite_inverse_real_of_posnat_ge_real = thm "finite_inverse_real_of_posnat_ge_real"; val inverse_real_of_posnat_ge_real_FreeUltrafilterNat = thm "inverse_real_of_posnat_ge_real_FreeUltrafilterNat"; val FreeUltrafilterNat_inverse_real_of_posnat = thm "FreeUltrafilterNat_inverse_real_of_posnat"; val real_seq_to_hypreal_Infinitesimal = thm "real_seq_to_hypreal_Infinitesimal"; val real_seq_to_hypreal_approx = thm "real_seq_to_hypreal_approx"; val real_seq_to_hypreal_approx2 = thm "real_seq_to_hypreal_approx2"; val real_seq_to_hypreal_Infinitesimal2 = thm "real_seq_to_hypreal_Infinitesimal2"; val HInfinite_HFinite_add = thm "HInfinite_HFinite_add"; val HInfinite_ge_HInfinite = thm "HInfinite_ge_HInfinite"; val Infinitesimal_inverse_HInfinite = thm "Infinitesimal_inverse_HInfinite"; val HInfinite_HFinite_not_Infinitesimal_mult = thm "HInfinite_HFinite_not_Infinitesimal_mult"; val HInfinite_HFinite_not_Infinitesimal_mult2 = thm "HInfinite_HFinite_not_Infinitesimal_mult2"; val HInfinite_gt_SReal = thm "HInfinite_gt_SReal"; val HInfinite_gt_zero_gt_one = thm "HInfinite_gt_zero_gt_one"; val not_HInfinite_one = thm "not_HInfinite_one"; *} end
lemma SReal_add:
[| x ∈ Reals; y ∈ Reals |] ==> x + y ∈ Reals
lemma SReal_mult:
[| x ∈ Reals; y ∈ Reals |] ==> x * y ∈ Reals
lemma SReal_inverse:
x ∈ Reals ==> inverse x ∈ Reals
lemma SReal_divide:
[| x ∈ Reals; y ∈ Reals |] ==> x / y ∈ Reals
lemma SReal_minus:
x ∈ Reals ==> - x ∈ Reals
lemma SReal_minus_iff:
(- x ∈ Reals) = (x ∈ Reals)
lemma SReal_add_cancel:
[| x + y ∈ Reals; y ∈ Reals |] ==> x ∈ Reals
lemma SReal_hrabs:
x ∈ Reals ==> ¦x¦ ∈ Reals
lemma SReal_hypreal_of_real:
star_of x ∈ Reals
lemma SReal_number_of:
number_of w ∈ Reals
lemma Reals_0:
0 ∈ Reals
lemma Reals_1:
1 ∈ Reals
lemma SReal_divide_number_of:
r ∈ Reals ==> r / number_of w ∈ Reals
lemma SReal_epsilon_not_mem:
ε ∉ Reals
lemma SReal_omega_not_mem:
ω ∉ Reals
lemma SReal_UNIV_real:
{x. star_of x ∈ Reals} = UNIV
lemma SReal_iff:
(x ∈ Reals) = (∃y. x = star_of y)
lemma hypreal_of_real_image:
range star_of = Reals
lemma inv_hypreal_of_real_image:
inv star_of ` Reals = UNIV
lemma SReal_hypreal_of_real_image:
[| ∃x. x ∈ P; P ⊆ Reals |] ==> ∃Q. P = star_of ` Q
lemma SReal_dense:
[| x ∈ Reals; y ∈ Reals; x < y |] ==> ∃r∈Reals. x < r ∧ r < y
lemma SReal_sup_lemma:
P ⊆ Reals ==> (∃x∈P. y < x) = (∃X. star_of X ∈ P ∧ y < star_of X)
lemma SReal_sup_lemma2:
[| P ⊆ Reals; ∃x. x ∈ P; ∃y∈Reals. ∀x∈P. x < y |] ==> (∃X. X ∈ {w. star_of w ∈ P}) ∧ (∃Y. ∀X∈{w. star_of w ∈ P}. X < Y)
lemma hypreal_of_real_isUb_iff:
isUb Reals (star_of ` Q) (star_of Y) = isUb UNIV Q Y
lemma hypreal_of_real_isLub1:
isLub Reals (star_of ` Q) (star_of Y) ==> isLub UNIV Q Y
lemma hypreal_of_real_isLub2:
isLub UNIV Q Y ==> isLub Reals (star_of ` Q) (star_of Y)
lemma hypreal_of_real_isLub_iff:
isLub Reals (star_of ` Q) (star_of Y) = isLub UNIV Q Y
lemma lemma_isUb_hypreal_of_real:
isUb Reals P Y ==> ∃Yo. isUb Reals P (star_of Yo)
lemma lemma_isLub_hypreal_of_real:
isLub Reals P Y ==> ∃Yo. isLub Reals P (star_of Yo)
lemma lemma_isLub_hypreal_of_real2:
∃Yo. isLub Reals P (star_of Yo) ==> ∃Y. isLub Reals P Y
lemma SReal_complete:
[| P ⊆ Reals; ∃x. x ∈ P; ∃Y. isUb Reals P Y |] ==> ∃t. isLub Reals P t
lemma HFinite_add:
[| x ∈ HFinite; y ∈ HFinite |] ==> x + y ∈ HFinite
lemma HFinite_mult:
[| x ∈ HFinite; y ∈ HFinite |] ==> x * y ∈ HFinite
lemma HFinite_minus_iff:
(- x ∈ HFinite) = (x ∈ HFinite)
lemma SReal_subset_HFinite:
Reals ⊆ HFinite
lemma HFinite_hypreal_of_real:
star_of x ∈ HFinite
lemma HFiniteD:
x ∈ HFinite ==> ∃t∈Reals. ¦x¦ < t
lemma HFinite_hrabs_iff:
(¦x¦ ∈ HFinite) = (x ∈ HFinite)
lemma HFinite_number_of:
number_of w ∈ HFinite
lemma HFinite_0:
0 ∈ HFinite
lemma HFinite_1:
1 ∈ HFinite
lemma HFinite_bounded:
[| x ∈ HFinite; y ≤ x; 0 ≤ y |] ==> y ∈ HFinite
lemma InfinitesimalD:
x ∈ Infinitesimal ==> ∀r∈Reals. 0 < r --> ¦x¦ < r
lemma Infinitesimal_zero:
0 ∈ Infinitesimal
lemma hypreal_sum_of_halves:
x / 2 + x / 2 = x
lemma Infinitesimal_add:
[| x ∈ Infinitesimal; y ∈ Infinitesimal |] ==> x + y ∈ Infinitesimal
lemma Infinitesimal_minus_iff:
(- x ∈ Infinitesimal) = (x ∈ Infinitesimal)
lemma Infinitesimal_diff:
[| x ∈ Infinitesimal; y ∈ Infinitesimal |] ==> x - y ∈ Infinitesimal
lemma Infinitesimal_mult:
[| x ∈ Infinitesimal; y ∈ Infinitesimal |] ==> x * y ∈ Infinitesimal
lemma Infinitesimal_HFinite_mult:
[| x ∈ Infinitesimal; y ∈ HFinite |] ==> x * y ∈ Infinitesimal
lemma Infinitesimal_HFinite_mult2:
[| x ∈ Infinitesimal; y ∈ HFinite |] ==> y * x ∈ Infinitesimal
lemma HInfinite_inverse_Infinitesimal:
x ∈ HInfinite ==> inverse x ∈ Infinitesimal
lemma HInfinite_mult:
[| x ∈ HInfinite; y ∈ HInfinite |] ==> x * y ∈ HInfinite
lemma hypreal_add_zero_less_le_mono:
[| r < x; 0 ≤ y |] ==> r < x + y
lemma HInfinite_add_ge_zero:
[| x ∈ HInfinite; 0 ≤ y; 0 ≤ x |] ==> x + y ∈ HInfinite
lemma HInfinite_add_ge_zero2:
[| x ∈ HInfinite; 0 ≤ y; 0 ≤ x |] ==> y + x ∈ HInfinite
lemma HInfinite_add_gt_zero:
[| x ∈ HInfinite; 0 < y; 0 < x |] ==> x + y ∈ HInfinite
lemma HInfinite_minus_iff:
(- x ∈ HInfinite) = (x ∈ HInfinite)
lemma HInfinite_add_le_zero:
[| x ∈ HInfinite; y ≤ 0; x ≤ 0 |] ==> x + y ∈ HInfinite
lemma HInfinite_add_lt_zero:
[| x ∈ HInfinite; y < 0; x < 0 |] ==> x + y ∈ HInfinite
lemma HFinite_sum_squares:
[| a ∈ HFinite; b ∈ HFinite; c ∈ HFinite |] ==> a * a + b * b + c * c ∈ HFinite
lemma not_Infinitesimal_not_zero:
x ∉ Infinitesimal ==> x ≠ 0
lemma not_Infinitesimal_not_zero2:
x ∈ HFinite - Infinitesimal ==> x ≠ 0
lemma Infinitesimal_hrabs_iff:
(¦x¦ ∈ Infinitesimal) = (x ∈ Infinitesimal)
lemma HFinite_diff_Infinitesimal_hrabs:
x ∈ HFinite - Infinitesimal ==> ¦x¦ ∈ HFinite - Infinitesimal
lemma hrabs_less_Infinitesimal:
[| e ∈ Infinitesimal; ¦x¦ < e |] ==> x ∈ Infinitesimal
lemma hrabs_le_Infinitesimal:
[| e ∈ Infinitesimal; ¦x¦ ≤ e |] ==> x ∈ Infinitesimal
lemma Infinitesimal_interval:
[| e ∈ Infinitesimal; e' ∈ Infinitesimal; e' < x; x < e |] ==> x ∈ Infinitesimal
lemma Infinitesimal_interval2:
[| e ∈ Infinitesimal; e' ∈ Infinitesimal; e' ≤ x; x ≤ e |] ==> x ∈ Infinitesimal
lemma not_Infinitesimal_mult:
[| x ∉ Infinitesimal; y ∉ Infinitesimal |] ==> x * y ∉ Infinitesimal
lemma Infinitesimal_mult_disj:
x * y ∈ Infinitesimal ==> x ∈ Infinitesimal ∨ y ∈ Infinitesimal
lemma HFinite_Infinitesimal_not_zero:
x ∈ HFinite - Infinitesimal ==> x ≠ 0
lemma HFinite_Infinitesimal_diff_mult:
[| x ∈ HFinite - Infinitesimal; y ∈ HFinite - Infinitesimal |] ==> x * y ∈ HFinite - Infinitesimal
lemma Infinitesimal_subset_HFinite:
Infinitesimal ⊆ HFinite
lemma Infinitesimal_hypreal_of_real_mult:
x ∈ Infinitesimal ==> x * star_of r ∈ Infinitesimal
lemma Infinitesimal_hypreal_of_real_mult2:
x ∈ Infinitesimal ==> star_of r * x ∈ Infinitesimal
lemma mem_infmal_iff:
(x ∈ Infinitesimal) = (x ≈ 0)
lemma approx_minus_iff:
(x ≈ y) = (x + - y ≈ 0)
lemma approx_minus_iff2:
(x ≈ y) = (- y + x ≈ 0)
lemma approx_refl:
x ≈ x
lemma hypreal_minus_distrib1:
- (y + - x) = x + - y
lemma approx_sym:
x ≈ y ==> y ≈ x
lemma approx_trans:
[| x ≈ y; y ≈ z |] ==> x ≈ z
lemma approx_trans2:
[| r ≈ x; s ≈ x |] ==> r ≈ s
lemma approx_trans3:
[| x ≈ r; x ≈ s |] ==> r ≈ s
lemma number_of_approx_reorient:
(number_of w ≈ x) = (x ≈ number_of w)
lemma zero_approx_reorient:
(0 ≈ x) = (x ≈ 0)
lemma one_approx_reorient:
(1 ≈ x) = (x ≈ 1)
lemma Infinitesimal_approx_minus:
(x - y ∈ Infinitesimal) = (x ≈ y)
lemma approx_monad_iff:
(x ≈ y) = (monad x = monad y)
lemma Infinitesimal_approx:
[| x ∈ Infinitesimal; y ∈ Infinitesimal |] ==> x ≈ y
lemma approx_add:
[| a ≈ b; c ≈ d |] ==> a + c ≈ b + d
lemma approx_minus:
a ≈ b ==> - a ≈ - b
lemma approx_minus2:
- a ≈ - b ==> a ≈ b
lemma approx_minus_cancel:
(- a ≈ - b) = (a ≈ b)
lemma approx_add_minus:
[| a ≈ b; c ≈ d |] ==> a + - c ≈ b + - d
lemma approx_mult1:
[| a ≈ b; c ∈ HFinite |] ==> a * c ≈ b * c
lemma approx_mult2:
[| a ≈ b; c ∈ HFinite |] ==> c * a ≈ c * b
lemma approx_mult_subst:
[| u ≈ v * x; x ≈ y; v ∈ HFinite |] ==> u ≈ v * y
lemma approx_mult_subst2:
[| u ≈ x * v; x ≈ y; v ∈ HFinite |] ==> u ≈ y * v
lemma approx_mult_subst_SReal:
[| u ≈ x * star_of v; x ≈ y |] ==> u ≈ y * star_of v
lemma approx_eq_imp:
a = b ==> a ≈ b
lemma Infinitesimal_minus_approx:
x ∈ Infinitesimal ==> - x ≈ x
lemma bex_Infinitesimal_iff:
(∃y∈Infinitesimal. x + - z = y) = (x ≈ z)
lemma bex_Infinitesimal_iff2:
(∃y∈Infinitesimal. x = z + y) = (x ≈ z)
lemma Infinitesimal_add_approx:
[| y ∈ Infinitesimal; x + y = z |] ==> x ≈ z
lemma Infinitesimal_add_approx_self:
y ∈ Infinitesimal ==> x ≈ x + y
lemma Infinitesimal_add_approx_self2:
y ∈ Infinitesimal ==> x ≈ y + x
lemma Infinitesimal_add_minus_approx_self:
y ∈ Infinitesimal ==> x ≈ x + - y
lemma Infinitesimal_add_cancel:
[| y ∈ Infinitesimal; x + y ≈ z |] ==> x ≈ z
lemma Infinitesimal_add_right_cancel:
[| y ∈ Infinitesimal; x ≈ z + y |] ==> x ≈ z
lemma approx_add_left_cancel:
d + b ≈ d + c ==> b ≈ c
lemma approx_add_right_cancel:
b + d ≈ c + d ==> b ≈ c
lemma approx_add_mono1:
b ≈ c ==> d + b ≈ d + c
lemma approx_add_mono2:
b ≈ c ==> b + a ≈ c + a
lemma approx_add_left_iff:
(a + b ≈ a + c) = (b ≈ c)
lemma approx_add_right_iff:
(b + a ≈ c + a) = (b ≈ c)
lemma approx_HFinite:
[| x ∈ HFinite; x ≈ y |] ==> y ∈ HFinite
lemma approx_hypreal_of_real_HFinite:
x ≈ star_of D ==> x ∈ HFinite
lemma approx_mult_HFinite:
[| a ≈ b; c ≈ d; b ∈ HFinite; d ∈ HFinite |] ==> a * c ≈ b * d
lemma approx_mult_hypreal_of_real:
[| a ≈ star_of b; c ≈ star_of d |] ==> a * c ≈ star_of b * star_of d
lemma approx_SReal_mult_cancel_zero:
[| a ∈ Reals; a ≠ 0; a * x ≈ 0 |] ==> x ≈ 0
lemma approx_mult_SReal1:
[| a ∈ Reals; x ≈ 0 |] ==> x * a ≈ 0
lemma approx_mult_SReal2:
[| a ∈ Reals; x ≈ 0 |] ==> a * x ≈ 0
lemma approx_mult_SReal_zero_cancel_iff:
[| a ∈ Reals; a ≠ 0 |] ==> (a * x ≈ 0) = (x ≈ 0)
lemma approx_SReal_mult_cancel:
[| a ∈ Reals; a ≠ 0; a * w ≈ a * z |] ==> w ≈ z
lemma approx_SReal_mult_cancel_iff1:
[| a ∈ Reals; a ≠ 0 |] ==> (a * w ≈ a * z) = (w ≈ z)
lemma approx_le_bound:
[| z ≤ f; f ≈ g; g ≤ z |] ==> f ≈ z
lemma Infinitesimal_less_SReal:
[| x ∈ Reals; y ∈ Infinitesimal; 0 < x |] ==> y < x
lemma Infinitesimal_less_SReal2:
y ∈ Infinitesimal ==> ∀r∈Reals. 0 < r --> y < r
lemma SReal_not_Infinitesimal:
[| 0 < y; y ∈ Reals |] ==> y ∉ Infinitesimal
lemma SReal_minus_not_Infinitesimal:
[| y < 0; y ∈ Reals |] ==> y ∉ Infinitesimal
lemma SReal_Int_Infinitesimal_zero:
Reals ∩ Infinitesimal = {0}
lemma SReal_Infinitesimal_zero:
[| x ∈ Reals; x ∈ Infinitesimal |] ==> x = 0
lemma SReal_HFinite_diff_Infinitesimal:
[| x ∈ Reals; x ≠ 0 |] ==> x ∈ HFinite - Infinitesimal
lemma hypreal_of_real_HFinite_diff_Infinitesimal:
star_of x ≠ 0 ==> star_of x ∈ HFinite - Infinitesimal
lemma hypreal_of_real_Infinitesimal_iff_0:
(star_of x ∈ Infinitesimal) = (x = 0)
lemma number_of_not_Infinitesimal:
number_of w ≠ 0 ==> number_of w ∉ Infinitesimal
lemma one_not_Infinitesimal:
1 ∉ Infinitesimal
lemma approx_SReal_not_zero:
[| y ∈ Reals; x ≈ y; y ≠ 0 |] ==> x ≠ 0
lemma HFinite_diff_Infinitesimal_approx:
[| x ≈ y; y ∈ HFinite - Infinitesimal |] ==> x ∈ HFinite - Infinitesimal
lemma Infinitesimal_ratio:
[| y ≠ 0; y ∈ Infinitesimal; x / y ∈ HFinite |] ==> x ∈ Infinitesimal
lemma Infinitesimal_SReal_divide:
[| x ∈ Infinitesimal; y ∈ Reals |] ==> x / y ∈ Infinitesimal
lemma SReal_approx_iff:
[| x ∈ Reals; y ∈ Reals |] ==> (x ≈ y) = (x = y)
lemma number_of_approx_iff:
(number_of v ≈ number_of w) = (number_of v = number_of w)
lemma
(0 ≈ number_of w) = (number_of w = 0)
(number_of w ≈ 0) = (number_of w = 0)
(1 ≈ number_of w) = (number_of w = 1)
(number_of w ≈ 1) = (number_of w = 1)
¬ 0 ≈ 1
¬ 1 ≈ 0
lemma hypreal_of_real_approx_iff:
(star_of k ≈ star_of m) = (k = m)
lemma hypreal_of_real_approx_number_of_iff:
(star_of k ≈ number_of w) = (k = number_of w)
lemma
(star_of k ≈ 0) = (k = 0)
(star_of k ≈ 1) = (k = 1)
lemma approx_unique_real:
[| r ∈ Reals; s ∈ Reals; r ≈ x; s ≈ x |] ==> r = s
lemma hypreal_isLub_unique:
[| isLub R S x; isLub R S y |] ==> x = y
lemma lemma_st_part_ub:
x ∈ HFinite ==> ∃u. isUb Reals {s : Reals. s < x} u
lemma lemma_st_part_nonempty:
x ∈ HFinite ==> ∃y. y ∈ {s : Reals. s < x}
lemma lemma_st_part_subset:
{s : Reals. s < x} ⊆ Reals
lemma lemma_st_part_lub:
x ∈ HFinite ==> ∃t. isLub Reals {s : Reals. s < x} t
lemma lemma_hypreal_le_left_cancel:
(t + r ≤ t) = (r ≤ 0)
lemma lemma_st_part_le1:
[| x ∈ HFinite; isLub Reals {s : Reals. s < x} t; r ∈ Reals; 0 < r |] ==> x ≤ t + r
lemma hypreal_setle_less_trans:
[| S *<= x; x < y |] ==> S *<= y
lemma hypreal_gt_isUb:
[| isUb R S x; x < y; y ∈ R |] ==> isUb R S y
lemma lemma_st_part_gt_ub:
[| x ∈ HFinite; x < y; y ∈ Reals |] ==> isUb Reals {s : Reals. s < x} y
lemma lemma_minus_le_zero:
t ≤ t + - r ==> r ≤ 0
lemma lemma_st_part_le2:
[| x ∈ HFinite; isLub Reals {s : Reals. s < x} t; r ∈ Reals; 0 < r |] ==> t + - r ≤ x
lemma lemma_st_part1a:
[| x ∈ HFinite; isLub Reals {s : Reals. s < x} t; r ∈ Reals; 0 < r |] ==> x + - t ≤ r
lemma lemma_st_part2a:
[| x ∈ HFinite; isLub Reals {s : Reals. s < x} t; r ∈ Reals; 0 < r |] ==> - (x + - t) ≤ r
lemma lemma_SReal_ub:
x ∈ Reals ==> isUb Reals {s : Reals. s < x} x
lemma lemma_SReal_lub:
x ∈ Reals ==> isLub Reals {s : Reals. s < x} x
lemma lemma_st_part_not_eq1:
[| x ∈ HFinite; isLub Reals {s : Reals. s < x} t; r ∈ Reals; 0 < r |] ==> x + - t ≠ r
lemma lemma_st_part_not_eq2:
[| x ∈ HFinite; isLub Reals {s : Reals. s < x} t; r ∈ Reals; 0 < r |] ==> - (x + - t) ≠ r
lemma lemma_st_part_major:
[| x ∈ HFinite; isLub Reals {s : Reals. s < x} t; r ∈ Reals; 0 < r |] ==> ¦x + - t¦ < r
lemma lemma_st_part_major2:
[| x ∈ HFinite; isLub Reals {s : Reals. s < x} t |] ==> ∀r∈Reals. 0 < r --> ¦x + - t¦ < r
lemma lemma_st_part_Ex:
x ∈ HFinite ==> ∃t∈Reals. ∀r∈Reals. 0 < r --> ¦x + - t¦ < r
lemma st_part_Ex:
x ∈ HFinite ==> ∃t∈Reals. x ≈ t
lemma st_part_Ex1:
x ∈ HFinite ==> ∃!t. t ∈ Reals ∧ x ≈ t
lemma HFinite_Int_HInfinite_empty:
HFinite ∩ HInfinite = {}
lemma HFinite_not_HInfinite:
x ∈ HFinite ==> x ∉ HInfinite
lemma not_HFinite_HInfinite:
x ∉ HFinite ==> x ∈ HInfinite
lemma HInfinite_HFinite_disj:
x ∈ HInfinite ∨ x ∈ HFinite
lemma HInfinite_HFinite_iff:
(x ∈ HInfinite) = (x ∉ HFinite)
lemma HFinite_HInfinite_iff:
(x ∈ HFinite) = (x ∉ HInfinite)
lemma HInfinite_diff_HFinite_Infinitesimal_disj:
x ∉ Infinitesimal ==> x ∈ HInfinite ∨ x ∈ HFinite - Infinitesimal
lemma HFinite_inverse:
[| x ∈ HFinite; x ∉ Infinitesimal |] ==> inverse x ∈ HFinite
lemma HFinite_inverse2:
x ∈ HFinite - Infinitesimal ==> inverse x ∈ HFinite
lemma Infinitesimal_inverse_HFinite:
x ∉ Infinitesimal ==> inverse x ∈ HFinite
lemma HFinite_not_Infinitesimal_inverse:
x ∈ HFinite - Infinitesimal ==> inverse x ∈ HFinite - Infinitesimal
lemma approx_inverse:
[| x ≈ y; y ∈ HFinite - Infinitesimal |] ==> inverse x ≈ inverse y
lemmas hypreal_of_real_approx_inverse:
[| x ≈ star_of x1; star_of x1 ≠ 0 |] ==> inverse x ≈ inverse (star_of x1)
lemmas hypreal_of_real_approx_inverse:
[| x ≈ star_of x1; star_of x1 ≠ 0 |] ==> inverse x ≈ inverse (star_of x1)
lemma inverse_add_Infinitesimal_approx:
[| x ∈ HFinite - Infinitesimal; h ∈ Infinitesimal |] ==> inverse (x + h) ≈ inverse x
lemma inverse_add_Infinitesimal_approx2:
[| x ∈ HFinite - Infinitesimal; h ∈ Infinitesimal |] ==> inverse (h + x) ≈ inverse x
lemma inverse_add_Infinitesimal_approx_Infinitesimal:
[| x ∈ HFinite - Infinitesimal; h ∈ Infinitesimal |] ==> inverse (x + h) + - inverse x ≈ h
lemma Infinitesimal_square_iff:
(x ∈ Infinitesimal) = (x * x ∈ Infinitesimal)
lemma HFinite_square_iff:
(x * x ∈ HFinite) = (x ∈ HFinite)
lemma HInfinite_square_iff:
(x * x ∈ HInfinite) = (x ∈ HInfinite)
lemma approx_HFinite_mult_cancel:
[| a ∈ HFinite - Infinitesimal; a * w ≈ a * z |] ==> w ≈ z
lemma approx_HFinite_mult_cancel_iff1:
a ∈ HFinite - Infinitesimal ==> (a * w ≈ a * z) = (w ≈ z)
lemma HInfinite_HFinite_add_cancel:
[| x + y ∈ HInfinite; y ∈ HFinite |] ==> x ∈ HInfinite
lemma HInfinite_HFinite_add:
[| x ∈ HInfinite; y ∈ HFinite |] ==> x + y ∈ HInfinite
lemma HInfinite_ge_HInfinite:
[| x ∈ HInfinite; x ≤ y; 0 ≤ x |] ==> y ∈ HInfinite
lemma Infinitesimal_inverse_HInfinite:
[| x ∈ Infinitesimal; x ≠ 0 |] ==> inverse x ∈ HInfinite
lemma HInfinite_HFinite_not_Infinitesimal_mult:
[| x ∈ HInfinite; y ∈ HFinite - Infinitesimal |] ==> x * y ∈ HInfinite
lemma HInfinite_HFinite_not_Infinitesimal_mult2:
[| x ∈ HInfinite; y ∈ HFinite - Infinitesimal |] ==> y * x ∈ HInfinite
lemma HInfinite_gt_SReal:
[| x ∈ HInfinite; 0 < x; y ∈ Reals |] ==> y < x
lemma HInfinite_gt_zero_gt_one:
[| x ∈ HInfinite; 0 < x |] ==> 1 < x
lemma not_HInfinite_one:
1 ∉ HInfinite
lemma approx_hrabs_disj:
¦x¦ ≈ x ∨ ¦x¦ ≈ - x
lemma monad_hrabs_Un_subset:
monad ¦x¦ ⊆ monad x ∪ monad (- x)
lemma Infinitesimal_monad_eq:
e ∈ Infinitesimal ==> monad (x + e) = monad x
lemma mem_monad_iff:
(u ∈ monad x) = (- u ∈ monad (- x))
lemma Infinitesimal_monad_zero_iff:
(x ∈ Infinitesimal) = (x ∈ monad 0)
lemma monad_zero_minus_iff:
(x ∈ monad 0) = (- x ∈ monad 0)
lemma monad_zero_hrabs_iff:
(x ∈ monad 0) = (¦x¦ ∈ monad 0)
lemma mem_monad_self:
x ∈ monad x
lemma approx_subset_monad:
x ≈ y ==> {x, y} ⊆ monad x
lemma approx_subset_monad2:
x ≈ y ==> {x, y} ⊆ monad y
lemma mem_monad_approx:
u ∈ monad x ==> x ≈ u
lemma approx_mem_monad:
x ≈ u ==> u ∈ monad x
lemma approx_mem_monad2:
x ≈ u ==> x ∈ monad u
lemma approx_mem_monad_zero:
[| x ≈ y; x ∈ monad 0 |] ==> y ∈ monad 0
lemma Infinitesimal_approx_hrabs:
[| x ≈ y; x ∈ Infinitesimal |] ==> ¦x¦ ≈ ¦y¦
lemma less_Infinitesimal_less:
[| 0 < x; x ∉ Infinitesimal; e ∈ Infinitesimal |] ==> e < x
lemma Ball_mem_monad_gt_zero:
[| 0 < x; x ∉ Infinitesimal; u ∈ monad x |] ==> 0 < u
lemma Ball_mem_monad_less_zero:
[| x < 0; x ∉ Infinitesimal; u ∈ monad x |] ==> u < 0
lemma lemma_approx_gt_zero:
[| 0 < x; x ∉ Infinitesimal; x ≈ y |] ==> 0 < y
lemma lemma_approx_less_zero:
[| x < 0; x ∉ Infinitesimal; x ≈ y |] ==> y < 0
theorem approx_hrabs:
x ≈ y ==> ¦x¦ ≈ ¦y¦
lemma approx_hrabs_zero_cancel:
¦x¦ ≈ 0 ==> x ≈ 0
lemma approx_hrabs_add_Infinitesimal:
e ∈ Infinitesimal ==> ¦x¦ ≈ ¦x + e¦
lemma approx_hrabs_add_minus_Infinitesimal:
e ∈ Infinitesimal ==> ¦x¦ ≈ ¦x + - e¦
lemma hrabs_add_Infinitesimal_cancel:
[| e ∈ Infinitesimal; e' ∈ Infinitesimal; ¦x + e¦ = ¦y + e'¦ |] ==> ¦x¦ ≈ ¦y¦
lemma hrabs_add_minus_Infinitesimal_cancel:
[| e ∈ Infinitesimal; e' ∈ Infinitesimal; ¦x + - e¦ = ¦y + - e'¦ |] ==> ¦x¦ ≈ ¦y¦
lemma Infinitesimal_add_hypreal_of_real_less:
[| x < y; u ∈ Infinitesimal |] ==> star_of x + u < star_of y
lemma Infinitesimal_add_hrabs_hypreal_of_real_less:
[| x ∈ Infinitesimal; ¦star_of r¦ < star_of y |] ==> ¦star_of r + x¦ < star_of y
lemma Infinitesimal_add_hrabs_hypreal_of_real_less2:
[| x ∈ Infinitesimal; ¦star_of r¦ < star_of y |] ==> ¦x + star_of r¦ < star_of y
lemma hypreal_of_real_le_add_Infininitesimal_cancel:
[| u ∈ Infinitesimal; v ∈ Infinitesimal; star_of x + u ≤ star_of y + v |] ==> star_of x ≤ star_of y
lemma hypreal_of_real_le_add_Infininitesimal_cancel2:
[| u ∈ Infinitesimal; v ∈ Infinitesimal; star_of x + u ≤ star_of y + v |] ==> x ≤ y
lemma hypreal_of_real_less_Infinitesimal_le_zero:
[| star_of x < e; e ∈ Infinitesimal |] ==> star_of x ≤ 0
lemma Infinitesimal_add_not_zero:
[| h ∈ Infinitesimal; x ≠ 0 |] ==> star_of x + h ≠ 0
lemma Infinitesimal_square_cancel:
x * x + y * y ∈ Infinitesimal ==> x * x ∈ Infinitesimal
lemma HFinite_square_cancel:
x * x + y * y ∈ HFinite ==> x * x ∈ HFinite
lemma Infinitesimal_square_cancel2:
x * x + y * y ∈ Infinitesimal ==> y * y ∈ Infinitesimal
lemma HFinite_square_cancel2:
x * x + y * y ∈ HFinite ==> y * y ∈ HFinite
lemma Infinitesimal_sum_square_cancel:
x * x + y * y + z * z ∈ Infinitesimal ==> x * x ∈ Infinitesimal
lemma HFinite_sum_square_cancel:
x * x + y * y + z * z ∈ HFinite ==> x * x ∈ HFinite
lemma Infinitesimal_sum_square_cancel2:
y * y + x * x + z * z ∈ Infinitesimal ==> x * x ∈ Infinitesimal
lemma HFinite_sum_square_cancel2:
y * y + x * x + z * z ∈ HFinite ==> x * x ∈ HFinite
lemma Infinitesimal_sum_square_cancel3:
z * z + y * y + x * x ∈ Infinitesimal ==> x * x ∈ Infinitesimal
lemma HFinite_sum_square_cancel3:
z * z + y * y + x * x ∈ HFinite ==> x * x ∈ HFinite
lemma monad_hrabs_less:
[| y ∈ monad x; 0 < star_of e |] ==> ¦y + - x¦ < star_of e
lemma mem_monad_SReal_HFinite:
x ∈ monad (star_of a) ==> x ∈ HFinite
lemma st_approx_self:
x ∈ HFinite ==> st x ≈ x
lemma st_SReal:
x ∈ HFinite ==> st x ∈ Reals
lemma st_HFinite:
x ∈ HFinite ==> st x ∈ HFinite
lemma st_SReal_eq:
x ∈ Reals ==> st x = x
lemma st_hypreal_of_real:
st (star_of x) = star_of x
lemma st_eq_approx:
[| x ∈ HFinite; y ∈ HFinite; st x = st y |] ==> x ≈ y
lemma approx_st_eq:
[| x ∈ HFinite; y ∈ HFinite; x ≈ y |] ==> st x = st y
lemma st_eq_approx_iff:
[| x ∈ HFinite; y ∈ HFinite |] ==> (x ≈ y) = (st x = st y)
lemma st_Infinitesimal_add_SReal:
[| x ∈ Reals; e ∈ Infinitesimal |] ==> st (x + e) = x
lemma st_Infinitesimal_add_SReal2:
[| x ∈ Reals; e ∈ Infinitesimal |] ==> st (e + x) = x
lemma HFinite_st_Infinitesimal_add:
x ∈ HFinite ==> ∃e∈Infinitesimal. x = st x + e
lemma st_add:
[| x ∈ HFinite; y ∈ HFinite |] ==> st (x + y) = st x + st y
lemma st_number_of:
st (number_of w) = number_of w
lemma
st 0 = 0
st 1 = 1
lemma st_minus:
y ∈ HFinite ==> st (- y) = - st y
lemma st_diff:
[| x ∈ HFinite; y ∈ HFinite |] ==> st (x - y) = st x - st y
lemma lemma_st_mult:
[| x ∈ HFinite; y ∈ HFinite; e ∈ Infinitesimal; ea ∈ Infinitesimal |] ==> e * y + x * ea + e * ea ∈ Infinitesimal
lemma st_mult:
[| x ∈ HFinite; y ∈ HFinite |] ==> st (x * y) = st x * st y
lemma st_Infinitesimal:
x ∈ Infinitesimal ==> st x = 0
lemma st_not_Infinitesimal:
st x ≠ 0 ==> x ∉ Infinitesimal
lemma st_inverse:
[| x ∈ HFinite; st x ≠ 0 |] ==> st (inverse x) = inverse (st x)
lemma st_divide:
[| x ∈ HFinite; y ∈ HFinite; st y ≠ 0 |] ==> st (x / y) = st x / st y
lemma st_idempotent:
x ∈ HFinite ==> st (st x) = st x
lemma Infinitesimal_add_st_less:
[| x ∈ HFinite; y ∈ HFinite; u ∈ Infinitesimal; st x < st y |] ==> st x + u < st y
lemma Infinitesimal_add_st_le_cancel:
[| x ∈ HFinite; y ∈ HFinite; u ∈ Infinitesimal; st x ≤ st y + u |] ==> st x ≤ st y
lemma st_le:
[| x ∈ HFinite; y ∈ HFinite; x ≤ y |] ==> st x ≤ st y
lemma st_zero_le:
[| 0 ≤ x; x ∈ HFinite |] ==> 0 ≤ st x
lemma st_zero_ge:
[| x ≤ 0; x ∈ HFinite |] ==> st x ≤ 0
lemma st_hrabs:
x ∈ HFinite ==> ¦st x¦ = st ¦x¦
lemma FreeUltrafilterNat_Rep_hypreal:
[| X ∈ Rep_star x; Y ∈ Rep_star x |] ==> {n. X n = Y n} ∈ \<U>
lemma HFinite_FreeUltrafilterNat:
x ∈ HFinite ==> ∃X∈Rep_star x. ∃u. {n. ¦X n¦ < u} ∈ \<U>
lemma FreeUltrafilterNat_HFinite:
∃X∈Rep_star x. ∃u. {n. ¦X n¦ < u} ∈ \<U> ==> x ∈ HFinite
lemma HFinite_FreeUltrafilterNat_iff:
(x ∈ HFinite) = (∃X∈Rep_star x. ∃u. {n. ¦X n¦ < u} ∈ \<U>)
lemma lemma_Compl_eq:
- {n. u < ¦xa n¦} = {n. ¦xa n¦ ≤ u}
lemma lemma_Compl_eq2:
- {n. ¦xa n¦ < u} = {n. u ≤ ¦xa n¦}
lemma lemma_Int_eq1:
{n. ¦xa n¦ ≤ u} ∩ {n. u ≤ ¦xa n¦} = {n. ¦xa n¦ = u}
lemma lemma_FreeUltrafilterNat_one:
{n. ¦xa n¦ = u} ⊆ {n. ¦xa n¦ < u + 1}
lemma FreeUltrafilterNat_const_Finite:
[| xa ∈ Rep_star x; {n. ¦xa n¦ = u} ∈ \<U> |] ==> x ∈ HFinite
lemma HInfinite_FreeUltrafilterNat:
x ∈ HInfinite ==> ∃X∈Rep_star x. ∀u. {n. u < ¦X n¦} ∈ \<U>
lemma lemma_Int_HI:
{n. ¦Xa n¦ < u} ∩ {n. X n = Xa n} ⊆ {n. ¦X n¦ < u}
lemma lemma_Int_HIa:
{n. u < ¦X n¦} ∩ {n. ¦X n¦ < u} = {}
lemma FreeUltrafilterNat_HInfinite:
∃X∈Rep_star x. ∀u. {n. u < ¦X n¦} ∈ \<U> ==> x ∈ HInfinite
lemma HInfinite_FreeUltrafilterNat_iff:
(x ∈ HInfinite) = (∃X∈Rep_star x. ∀u. {n. u < ¦X n¦} ∈ \<U>)
lemma Infinitesimal_FreeUltrafilterNat:
x ∈ Infinitesimal ==> ∃X∈Rep_star x. ∀u>0. {n. ¦X n¦ < u} ∈ \<U>
lemma FreeUltrafilterNat_Infinitesimal:
∃X∈Rep_star x. ∀u>0. {n. ¦X n¦ < u} ∈ \<U> ==> x ∈ Infinitesimal
lemma Infinitesimal_FreeUltrafilterNat_iff:
(x ∈ Infinitesimal) = (∃X∈Rep_star x. ∀u>0. {n. ¦X n¦ < u} ∈ \<U>)
lemma lemma_Infinitesimal:
(∀r>0. x < r) = (∀n. x < inverse (real (Suc n)))
lemma of_nat_in_Reals:
of_nat n ∈ Reals
lemma lemma_Infinitesimal2:
(∀r∈Reals. 0 < r --> x < r) = (∀n. x < inverse (hypreal_of_nat (Suc n)))
lemma Infinitesimal_hypreal_of_nat_iff:
Infinitesimal = {x. ∀n. ¦x¦ < inverse (hypreal_of_nat (Suc n))}
lemma Suc_Un_eq:
{n. n < Suc m} = {n. n < m} ∪ {n. n = m}
lemma finite_nat_segment:
finite {n. n < m}
lemma finite_real_of_nat_segment:
finite {n. real n < real m}
lemma finite_real_of_nat_less_real:
finite {n. real n < u}
lemma lemma_real_le_Un_eq:
{n. f n ≤ u} = {n. f n < u} ∪ {n. u = f n}
lemma finite_real_of_nat_le_real:
finite {n. real n ≤ u}
lemma finite_rabs_real_of_nat_le_real:
finite {n. ¦real n¦ ≤ u}
lemma rabs_real_of_nat_le_real_FreeUltrafilterNat:
{n. ¦real n¦ ≤ u} ∉ \<U>
lemma FreeUltrafilterNat_nat_gt_real:
{n. u < real n} ∈ \<U>
lemma Compl_real_le_eq:
- {n. real n ≤ u} = {n. u < real n}
lemma FreeUltrafilterNat_omega:
{n. u < real n} ∈ \<U>
theorem HInfinite_omega:
ω ∈ HInfinite
lemma Infinitesimal_epsilon:
ε ∈ Infinitesimal
lemma HFinite_epsilon:
ε ∈ HFinite
lemma epsilon_approx_zero:
ε ≈ 0
lemma real_of_nat_less_inverse_iff:
0 < u ==> (u < inverse (real (Suc n))) = (real (Suc n) < inverse u)
lemma finite_inverse_real_of_posnat_gt_real:
0 < u ==> finite {n. u < inverse (real (Suc n))}
lemma lemma_real_le_Un_eq2:
{n. u ≤ inverse (real (Suc n))} = {n. u < inverse (real (Suc n))} ∪ {n. u = inverse (real (Suc n))}
lemma real_of_nat_inverse_le_iff:
(inverse (real (Suc n)) ≤ r) = (1 ≤ r * real (Suc n))
lemma real_of_nat_inverse_eq_iff:
(u = inverse (real (Suc n))) = (real (Suc n) = inverse u)
lemma lemma_finite_omega_set2:
finite {n. u = inverse (real (Suc n))}
lemma finite_inverse_real_of_posnat_ge_real:
0 < u ==> finite {n. u ≤ inverse (real (Suc n))}
lemma inverse_real_of_posnat_ge_real_FreeUltrafilterNat:
0 < u ==> {n. u ≤ inverse (real (Suc n))} ∉ \<U>
lemma Compl_le_inverse_eq:
- {n. u ≤ inverse (real (Suc n))} = {n. inverse (real (Suc n)) < u}
lemma FreeUltrafilterNat_inverse_real_of_posnat:
0 < u ==> {n. inverse (real (Suc n)) < u} ∈ \<U>
lemma real_seq_to_hypreal_Infinitesimal:
∀n. ¦X n + - x¦ < inverse (real (Suc n)) ==> star_n X + - star_of x ∈ Infinitesimal
lemma real_seq_to_hypreal_approx:
∀n. ¦X n + - x¦ < inverse (real (Suc n)) ==> star_n X ≈ star_of x
lemma real_seq_to_hypreal_approx2:
∀n. ¦x + - X n¦ < inverse (real (Suc n)) ==> star_n X ≈ star_of x
lemma real_seq_to_hypreal_Infinitesimal2:
∀n. ¦X n + - Y n¦ < inverse (real (Suc n)) ==> star_n X + - star_n Y ∈ Infinitesimal