src/HOL/Nonstandard_Analysis/NSA.thy
author wenzelm
Fri Sep 16 21:28:09 2016 +0200 (2016-09-16)
changeset 63901 4ce989e962e0
parent 62479 716336f19aa9
child 64435 c93b0e6131c3
permissions -rw-r--r--
more symbols;
     1 (*  Title:      HOL/Nonstandard_Analysis/NSA.thy
     2     Author:     Jacques D. Fleuriot, University of Cambridge
     3     Author:     Lawrence C Paulson, University of Cambridge
     4 *)
     5 
     6 section\<open>Infinite Numbers, Infinitesimals, Infinitely Close Relation\<close>
     7 
     8 theory NSA
     9 imports HyperDef "~~/src/HOL/Library/Lub_Glb"
    10 begin
    11 
    12 definition
    13   hnorm :: "'a::real_normed_vector star \<Rightarrow> real star" where
    14   [transfer_unfold]: "hnorm = *f* norm"
    15 
    16 definition
    17   Infinitesimal  :: "('a::real_normed_vector) star set" where
    18   "Infinitesimal = {x. \<forall>r \<in> Reals. 0 < r --> hnorm x < r}"
    19 
    20 definition
    21   HFinite :: "('a::real_normed_vector) star set" where
    22   "HFinite = {x. \<exists>r \<in> Reals. hnorm x < r}"
    23 
    24 definition
    25   HInfinite :: "('a::real_normed_vector) star set" where
    26   "HInfinite = {x. \<forall>r \<in> Reals. r < hnorm x}"
    27 
    28 definition
    29   approx :: "['a::real_normed_vector star, 'a star] => bool"  (infixl "\<approx>" 50) where
    30     \<comment>\<open>the `infinitely close' relation\<close>
    31   "(x \<approx> y) = ((x - y) \<in> Infinitesimal)"
    32 
    33 definition
    34   st        :: "hypreal => hypreal" where
    35     \<comment>\<open>the standard part of a hyperreal\<close>
    36   "st = (%x. @r. x \<in> HFinite & r \<in> \<real> & r \<approx> x)"
    37 
    38 definition
    39   monad     :: "'a::real_normed_vector star => 'a star set" where
    40   "monad x = {y. x \<approx> y}"
    41 
    42 definition
    43   galaxy    :: "'a::real_normed_vector star => 'a star set" where
    44   "galaxy x = {y. (x + -y) \<in> HFinite}"
    45 
    46 lemma SReal_def: "\<real> == {x. \<exists>r. x = hypreal_of_real r}"
    47 by (simp add: Reals_def image_def)
    48 
    49 subsection \<open>Nonstandard Extension of the Norm Function\<close>
    50 
    51 definition
    52   scaleHR :: "real star \<Rightarrow> 'a star \<Rightarrow> 'a::real_normed_vector star" where
    53   [transfer_unfold]: "scaleHR = starfun2 scaleR"
    54 
    55 lemma Standard_hnorm [simp]: "x \<in> Standard \<Longrightarrow> hnorm x \<in> Standard"
    56 by (simp add: hnorm_def)
    57 
    58 lemma star_of_norm [simp]: "star_of (norm x) = hnorm (star_of x)"
    59 by transfer (rule refl)
    60 
    61 lemma hnorm_ge_zero [simp]:
    62   "\<And>x::'a::real_normed_vector star. 0 \<le> hnorm x"
    63 by transfer (rule norm_ge_zero)
    64 
    65 lemma hnorm_eq_zero [simp]:
    66   "\<And>x::'a::real_normed_vector star. (hnorm x = 0) = (x = 0)"
    67 by transfer (rule norm_eq_zero)
    68 
    69 lemma hnorm_triangle_ineq:
    70   "\<And>x y::'a::real_normed_vector star. hnorm (x + y) \<le> hnorm x + hnorm y"
    71 by transfer (rule norm_triangle_ineq)
    72 
    73 lemma hnorm_triangle_ineq3:
    74   "\<And>x y::'a::real_normed_vector star. \<bar>hnorm x - hnorm y\<bar> \<le> hnorm (x - y)"
    75 by transfer (rule norm_triangle_ineq3)
    76 
    77 lemma hnorm_scaleR:
    78   "\<And>x::'a::real_normed_vector star.
    79    hnorm (a *\<^sub>R x) = \<bar>star_of a\<bar> * hnorm x"
    80 by transfer (rule norm_scaleR)
    81 
    82 lemma hnorm_scaleHR:
    83   "\<And>a (x::'a::real_normed_vector star).
    84    hnorm (scaleHR a x) = \<bar>a\<bar> * hnorm x"
    85 by transfer (rule norm_scaleR)
    86 
    87 lemma hnorm_mult_ineq:
    88   "\<And>x y::'a::real_normed_algebra star. hnorm (x * y) \<le> hnorm x * hnorm y"
    89 by transfer (rule norm_mult_ineq)
    90 
    91 lemma hnorm_mult:
    92   "\<And>x y::'a::real_normed_div_algebra star. hnorm (x * y) = hnorm x * hnorm y"
    93 by transfer (rule norm_mult)
    94 
    95 lemma hnorm_hyperpow:
    96   "\<And>(x::'a::{real_normed_div_algebra} star) n.
    97    hnorm (x pow n) = hnorm x pow n"
    98 by transfer (rule norm_power)
    99 
   100 lemma hnorm_one [simp]:
   101   "hnorm (1::'a::real_normed_div_algebra star) = 1"
   102 by transfer (rule norm_one)
   103 
   104 lemma hnorm_zero [simp]:
   105   "hnorm (0::'a::real_normed_vector star) = 0"
   106 by transfer (rule norm_zero)
   107 
   108 lemma zero_less_hnorm_iff [simp]:
   109   "\<And>x::'a::real_normed_vector star. (0 < hnorm x) = (x \<noteq> 0)"
   110 by transfer (rule zero_less_norm_iff)
   111 
   112 lemma hnorm_minus_cancel [simp]:
   113   "\<And>x::'a::real_normed_vector star. hnorm (- x) = hnorm x"
   114 by transfer (rule norm_minus_cancel)
   115 
   116 lemma hnorm_minus_commute:
   117   "\<And>a b::'a::real_normed_vector star. hnorm (a - b) = hnorm (b - a)"
   118 by transfer (rule norm_minus_commute)
   119 
   120 lemma hnorm_triangle_ineq2:
   121   "\<And>a b::'a::real_normed_vector star. hnorm a - hnorm b \<le> hnorm (a - b)"
   122 by transfer (rule norm_triangle_ineq2)
   123 
   124 lemma hnorm_triangle_ineq4:
   125   "\<And>a b::'a::real_normed_vector star. hnorm (a - b) \<le> hnorm a + hnorm b"
   126 by transfer (rule norm_triangle_ineq4)
   127 
   128 lemma abs_hnorm_cancel [simp]:
   129   "\<And>a::'a::real_normed_vector star. \<bar>hnorm a\<bar> = hnorm a"
   130 by transfer (rule abs_norm_cancel)
   131 
   132 lemma hnorm_of_hypreal [simp]:
   133   "\<And>r. hnorm (of_hypreal r::'a::real_normed_algebra_1 star) = \<bar>r\<bar>"
   134 by transfer (rule norm_of_real)
   135 
   136 lemma nonzero_hnorm_inverse:
   137   "\<And>a::'a::real_normed_div_algebra star.
   138    a \<noteq> 0 \<Longrightarrow> hnorm (inverse a) = inverse (hnorm a)"
   139 by transfer (rule nonzero_norm_inverse)
   140 
   141 lemma hnorm_inverse:
   142   "\<And>a::'a::{real_normed_div_algebra, division_ring} star.
   143    hnorm (inverse a) = inverse (hnorm a)"
   144 by transfer (rule norm_inverse)
   145 
   146 lemma hnorm_divide:
   147   "\<And>a b::'a::{real_normed_field, field} star.
   148    hnorm (a / b) = hnorm a / hnorm b"
   149 by transfer (rule norm_divide)
   150 
   151 lemma hypreal_hnorm_def [simp]:
   152   "\<And>r::hypreal. hnorm r = \<bar>r\<bar>"
   153 by transfer (rule real_norm_def)
   154 
   155 lemma hnorm_add_less:
   156   "\<And>(x::'a::real_normed_vector star) y r s.
   157    \<lbrakk>hnorm x < r; hnorm y < s\<rbrakk> \<Longrightarrow> hnorm (x + y) < r + s"
   158 by transfer (rule norm_add_less)
   159 
   160 lemma hnorm_mult_less:
   161   "\<And>(x::'a::real_normed_algebra star) y r s.
   162    \<lbrakk>hnorm x < r; hnorm y < s\<rbrakk> \<Longrightarrow> hnorm (x * y) < r * s"
   163 by transfer (rule norm_mult_less)
   164 
   165 lemma hnorm_scaleHR_less:
   166   "\<lbrakk>\<bar>x\<bar> < r; hnorm y < s\<rbrakk> \<Longrightarrow> hnorm (scaleHR x y) < r * s"
   167 apply (simp only: hnorm_scaleHR)
   168 apply (simp add: mult_strict_mono')
   169 done
   170 
   171 subsection\<open>Closure Laws for the Standard Reals\<close>
   172 
   173 lemma Reals_minus_iff [simp]: "(-x \<in> \<real>) = (x \<in> \<real>)"
   174 apply auto
   175 apply (drule Reals_minus, auto)
   176 done
   177 
   178 lemma Reals_add_cancel: "\<lbrakk>x + y \<in> \<real>; y \<in> \<real>\<rbrakk> \<Longrightarrow> x \<in> \<real>"
   179 by (drule (1) Reals_diff, simp)
   180 
   181 lemma SReal_hrabs: "(x::hypreal) \<in> \<real> ==> \<bar>x\<bar> \<in> \<real>"
   182 by (simp add: Reals_eq_Standard)
   183 
   184 lemma SReal_hypreal_of_real [simp]: "hypreal_of_real x \<in> \<real>"
   185 by (simp add: Reals_eq_Standard)
   186 
   187 lemma SReal_divide_numeral: "r \<in> \<real> ==> r/(numeral w::hypreal) \<in> \<real>"
   188 by simp
   189 
   190 text \<open>\<open>\<epsilon>\<close> is not in Reals because it is an infinitesimal\<close>
   191 lemma SReal_epsilon_not_mem: "\<epsilon> \<notin> \<real>"
   192 apply (simp add: SReal_def)
   193 apply (auto simp add: hypreal_of_real_not_eq_epsilon [THEN not_sym])
   194 done
   195 
   196 lemma SReal_omega_not_mem: "\<omega> \<notin> \<real>"
   197 apply (simp add: SReal_def)
   198 apply (auto simp add: hypreal_of_real_not_eq_omega [THEN not_sym])
   199 done
   200 
   201 lemma SReal_UNIV_real: "{x. hypreal_of_real x \<in> \<real>} = (UNIV::real set)"
   202 by simp
   203 
   204 lemma SReal_iff: "(x \<in> \<real>) = (\<exists>y. x = hypreal_of_real y)"
   205 by (simp add: SReal_def)
   206 
   207 lemma hypreal_of_real_image: "hypreal_of_real `(UNIV::real set) = \<real>"
   208 by (simp add: Reals_eq_Standard Standard_def)
   209 
   210 lemma inv_hypreal_of_real_image: "inv hypreal_of_real ` \<real> = UNIV"
   211 apply (auto simp add: SReal_def)
   212 apply (rule inj_star_of [THEN inv_f_f, THEN subst], blast)
   213 done
   214 
   215 lemma SReal_hypreal_of_real_image:
   216       "[| \<exists>x. x: P; P \<subseteq> \<real> |] ==> \<exists>Q. P = hypreal_of_real ` Q"
   217 by (simp add: SReal_def image_def, blast)
   218 
   219 lemma SReal_dense:
   220      "[| (x::hypreal) \<in> \<real>; y \<in> \<real>;  x<y |] ==> \<exists>r \<in> Reals. x<r & r<y"
   221 apply (auto simp add: SReal_def)
   222 apply (drule dense, auto)
   223 done
   224 
   225 text\<open>Completeness of Reals, but both lemmas are unused.\<close>
   226 
   227 lemma SReal_sup_lemma:
   228      "P \<subseteq> \<real> ==> ((\<exists>x \<in> P. y < x) =
   229       (\<exists>X. hypreal_of_real X \<in> P & y < hypreal_of_real X))"
   230 by (blast dest!: SReal_iff [THEN iffD1])
   231 
   232 lemma SReal_sup_lemma2:
   233      "[| P \<subseteq> \<real>; \<exists>x. x \<in> P; \<exists>y \<in> Reals. \<forall>x \<in> P. x < y |]
   234       ==> (\<exists>X. X \<in> {w. hypreal_of_real w \<in> P}) &
   235           (\<exists>Y. \<forall>X \<in> {w. hypreal_of_real w \<in> P}. X < Y)"
   236 apply (rule conjI)
   237 apply (fast dest!: SReal_iff [THEN iffD1])
   238 apply (auto, frule subsetD, assumption)
   239 apply (drule SReal_iff [THEN iffD1])
   240 apply (auto, rule_tac x = ya in exI, auto)
   241 done
   242 
   243 
   244 subsection\<open>Set of Finite Elements is a Subring of the Extended Reals\<close>
   245 
   246 lemma HFinite_add: "[|x \<in> HFinite; y \<in> HFinite|] ==> (x+y) \<in> HFinite"
   247 apply (simp add: HFinite_def)
   248 apply (blast intro!: Reals_add hnorm_add_less)
   249 done
   250 
   251 lemma HFinite_mult:
   252   fixes x y :: "'a::real_normed_algebra star"
   253   shows "[|x \<in> HFinite; y \<in> HFinite|] ==> x*y \<in> HFinite"
   254 apply (simp add: HFinite_def)
   255 apply (blast intro!: Reals_mult hnorm_mult_less)
   256 done
   257 
   258 lemma HFinite_scaleHR:
   259   "[|x \<in> HFinite; y \<in> HFinite|] ==> scaleHR x y \<in> HFinite"
   260 apply (simp add: HFinite_def)
   261 apply (blast intro!: Reals_mult hnorm_scaleHR_less)
   262 done
   263 
   264 lemma HFinite_minus_iff: "(-x \<in> HFinite) = (x \<in> HFinite)"
   265 by (simp add: HFinite_def)
   266 
   267 lemma HFinite_star_of [simp]: "star_of x \<in> HFinite"
   268 apply (simp add: HFinite_def)
   269 apply (rule_tac x="star_of (norm x) + 1" in bexI)
   270 apply (transfer, simp)
   271 apply (blast intro: Reals_add SReal_hypreal_of_real Reals_1)
   272 done
   273 
   274 lemma SReal_subset_HFinite: "(\<real>::hypreal set) \<subseteq> HFinite"
   275 by (auto simp add: SReal_def)
   276 
   277 lemma HFiniteD: "x \<in> HFinite ==> \<exists>t \<in> Reals. hnorm x < t"
   278 by (simp add: HFinite_def)
   279 
   280 lemma HFinite_hrabs_iff [iff]: "(\<bar>x::hypreal\<bar> \<in> HFinite) = (x \<in> HFinite)"
   281 by (simp add: HFinite_def)
   282 
   283 lemma HFinite_hnorm_iff [iff]:
   284   "(hnorm (x::hypreal) \<in> HFinite) = (x \<in> HFinite)"
   285 by (simp add: HFinite_def)
   286 
   287 lemma HFinite_numeral [simp]: "numeral w \<in> HFinite"
   288 unfolding star_numeral_def by (rule HFinite_star_of)
   289 
   290 (** As always with numerals, 0 and 1 are special cases **)
   291 
   292 lemma HFinite_0 [simp]: "0 \<in> HFinite"
   293 unfolding star_zero_def by (rule HFinite_star_of)
   294 
   295 lemma HFinite_1 [simp]: "1 \<in> HFinite"
   296 unfolding star_one_def by (rule HFinite_star_of)
   297 
   298 lemma hrealpow_HFinite:
   299   fixes x :: "'a::{real_normed_algebra,monoid_mult} star"
   300   shows "x \<in> HFinite ==> x ^ n \<in> HFinite"
   301 apply (induct n)
   302 apply (auto simp add: power_Suc intro: HFinite_mult)
   303 done
   304 
   305 lemma HFinite_bounded:
   306   "[|(x::hypreal) \<in> HFinite; y \<le> x; 0 \<le> y |] ==> y \<in> HFinite"
   307 apply (cases "x \<le> 0")
   308 apply (drule_tac y = x in order_trans)
   309 apply (drule_tac [2] order_antisym)
   310 apply (auto simp add: linorder_not_le)
   311 apply (auto intro: order_le_less_trans simp add: abs_if HFinite_def)
   312 done
   313 
   314 
   315 subsection\<open>Set of Infinitesimals is a Subring of the Hyperreals\<close>
   316 
   317 lemma InfinitesimalI:
   318   "(\<And>r. \<lbrakk>r \<in> \<real>; 0 < r\<rbrakk> \<Longrightarrow> hnorm x < r) \<Longrightarrow> x \<in> Infinitesimal"
   319 by (simp add: Infinitesimal_def)
   320 
   321 lemma InfinitesimalD:
   322       "x \<in> Infinitesimal ==> \<forall>r \<in> Reals. 0 < r --> hnorm x < r"
   323 by (simp add: Infinitesimal_def)
   324 
   325 lemma InfinitesimalI2:
   326   "(\<And>r. 0 < r \<Longrightarrow> hnorm x < star_of r) \<Longrightarrow> x \<in> Infinitesimal"
   327 by (auto simp add: Infinitesimal_def SReal_def)
   328 
   329 lemma InfinitesimalD2:
   330   "\<lbrakk>x \<in> Infinitesimal; 0 < r\<rbrakk> \<Longrightarrow> hnorm x < star_of r"
   331 by (auto simp add: Infinitesimal_def SReal_def)
   332 
   333 lemma Infinitesimal_zero [iff]: "0 \<in> Infinitesimal"
   334 by (simp add: Infinitesimal_def)
   335 
   336 lemma hypreal_sum_of_halves: "x/(2::hypreal) + x/(2::hypreal) = x"
   337 by auto
   338 
   339 lemma Infinitesimal_add:
   340      "[| x \<in> Infinitesimal; y \<in> Infinitesimal |] ==> (x+y) \<in> Infinitesimal"
   341 apply (rule InfinitesimalI)
   342 apply (rule hypreal_sum_of_halves [THEN subst])
   343 apply (drule half_gt_zero)
   344 apply (blast intro: hnorm_add_less SReal_divide_numeral dest: InfinitesimalD)
   345 done
   346 
   347 lemma Infinitesimal_minus_iff [simp]: "(-x:Infinitesimal) = (x:Infinitesimal)"
   348 by (simp add: Infinitesimal_def)
   349 
   350 lemma Infinitesimal_hnorm_iff:
   351   "(hnorm x \<in> Infinitesimal) = (x \<in> Infinitesimal)"
   352 by (simp add: Infinitesimal_def)
   353 
   354 lemma Infinitesimal_hrabs_iff [iff]:
   355   "(\<bar>x::hypreal\<bar> \<in> Infinitesimal) = (x \<in> Infinitesimal)"
   356 by (simp add: abs_if)
   357 
   358 lemma Infinitesimal_of_hypreal_iff [simp]:
   359   "((of_hypreal x::'a::real_normed_algebra_1 star) \<in> Infinitesimal) =
   360    (x \<in> Infinitesimal)"
   361 by (subst Infinitesimal_hnorm_iff [symmetric], simp)
   362 
   363 lemma Infinitesimal_diff:
   364      "[| x \<in> Infinitesimal;  y \<in> Infinitesimal |] ==> x-y \<in> Infinitesimal"
   365   using Infinitesimal_add [of x "- y"] by simp
   366 
   367 lemma Infinitesimal_mult:
   368   fixes x y :: "'a::real_normed_algebra star"
   369   shows "[|x \<in> Infinitesimal; y \<in> Infinitesimal|] ==> (x * y) \<in> Infinitesimal"
   370 apply (rule InfinitesimalI)
   371 apply (subgoal_tac "hnorm (x * y) < 1 * r", simp only: mult_1)
   372 apply (rule hnorm_mult_less)
   373 apply (simp_all add: InfinitesimalD)
   374 done
   375 
   376 lemma Infinitesimal_HFinite_mult:
   377   fixes x y :: "'a::real_normed_algebra star"
   378   shows "[| x \<in> Infinitesimal; y \<in> HFinite |] ==> (x * y) \<in> Infinitesimal"
   379 apply (rule InfinitesimalI)
   380 apply (drule HFiniteD, clarify)
   381 apply (subgoal_tac "0 < t")
   382 apply (subgoal_tac "hnorm (x * y) < (r / t) * t", simp)
   383 apply (subgoal_tac "0 < r / t")
   384 apply (rule hnorm_mult_less)
   385 apply (simp add: InfinitesimalD)
   386 apply assumption
   387 apply simp
   388 apply (erule order_le_less_trans [OF hnorm_ge_zero])
   389 done
   390 
   391 lemma Infinitesimal_HFinite_scaleHR:
   392   "[| x \<in> Infinitesimal; y \<in> HFinite |] ==> scaleHR x y \<in> Infinitesimal"
   393 apply (rule InfinitesimalI)
   394 apply (drule HFiniteD, clarify)
   395 apply (drule InfinitesimalD)
   396 apply (simp add: hnorm_scaleHR)
   397 apply (subgoal_tac "0 < t")
   398 apply (subgoal_tac "\<bar>x\<bar> * hnorm y < (r / t) * t", simp)
   399 apply (subgoal_tac "0 < r / t")
   400 apply (rule mult_strict_mono', simp_all)
   401 apply (erule order_le_less_trans [OF hnorm_ge_zero])
   402 done
   403 
   404 lemma Infinitesimal_HFinite_mult2:
   405   fixes x y :: "'a::real_normed_algebra star"
   406   shows "[| x \<in> Infinitesimal; y \<in> HFinite |] ==> (y * x) \<in> Infinitesimal"
   407 apply (rule InfinitesimalI)
   408 apply (drule HFiniteD, clarify)
   409 apply (subgoal_tac "0 < t")
   410 apply (subgoal_tac "hnorm (y * x) < t * (r / t)", simp)
   411 apply (subgoal_tac "0 < r / t")
   412 apply (rule hnorm_mult_less)
   413 apply assumption
   414 apply (simp add: InfinitesimalD)
   415 apply simp
   416 apply (erule order_le_less_trans [OF hnorm_ge_zero])
   417 done
   418 
   419 lemma Infinitesimal_scaleR2:
   420   "x \<in> Infinitesimal ==> a *\<^sub>R x \<in> Infinitesimal"
   421 apply (case_tac "a = 0", simp)
   422 apply (rule InfinitesimalI)
   423 apply (drule InfinitesimalD)
   424 apply (drule_tac x="r / \<bar>star_of a\<bar>" in bspec)
   425 apply (simp add: Reals_eq_Standard)
   426 apply simp
   427 apply (simp add: hnorm_scaleR pos_less_divide_eq mult.commute)
   428 done
   429 
   430 lemma Compl_HFinite: "- HFinite = HInfinite"
   431 apply (auto simp add: HInfinite_def HFinite_def linorder_not_less)
   432 apply (rule_tac y="r + 1" in order_less_le_trans, simp)
   433 apply simp
   434 done
   435 
   436 lemma HInfinite_inverse_Infinitesimal:
   437   fixes x :: "'a::real_normed_div_algebra star"
   438   shows "x \<in> HInfinite ==> inverse x \<in> Infinitesimal"
   439 apply (rule InfinitesimalI)
   440 apply (subgoal_tac "x \<noteq> 0")
   441 apply (rule inverse_less_imp_less)
   442 apply (simp add: nonzero_hnorm_inverse)
   443 apply (simp add: HInfinite_def Reals_inverse)
   444 apply assumption
   445 apply (clarify, simp add: Compl_HFinite [symmetric])
   446 done
   447 
   448 lemma HInfiniteI: "(\<And>r. r \<in> \<real> \<Longrightarrow> r < hnorm x) \<Longrightarrow> x \<in> HInfinite"
   449 by (simp add: HInfinite_def)
   450 
   451 lemma HInfiniteD: "\<lbrakk>x \<in> HInfinite; r \<in> \<real>\<rbrakk> \<Longrightarrow> r < hnorm x"
   452 by (simp add: HInfinite_def)
   453 
   454 lemma HInfinite_mult:
   455   fixes x y :: "'a::real_normed_div_algebra star"
   456   shows "[|x \<in> HInfinite; y \<in> HInfinite|] ==> (x*y) \<in> HInfinite"
   457 apply (rule HInfiniteI, simp only: hnorm_mult)
   458 apply (subgoal_tac "r * 1 < hnorm x * hnorm y", simp only: mult_1)
   459 apply (case_tac "x = 0", simp add: HInfinite_def)
   460 apply (rule mult_strict_mono)
   461 apply (simp_all add: HInfiniteD)
   462 done
   463 
   464 lemma hypreal_add_zero_less_le_mono: "[|r < x; (0::hypreal) \<le> y|] ==> r < x+y"
   465 by (auto dest: add_less_le_mono)
   466 
   467 lemma HInfinite_add_ge_zero:
   468      "[|(x::hypreal) \<in> HInfinite; 0 \<le> y; 0 \<le> x|] ==> (x + y): HInfinite"
   469 by (auto intro!: hypreal_add_zero_less_le_mono
   470        simp add: abs_if add.commute add_nonneg_nonneg HInfinite_def)
   471 
   472 lemma HInfinite_add_ge_zero2:
   473      "[|(x::hypreal) \<in> HInfinite; 0 \<le> y; 0 \<le> x|] ==> (y + x): HInfinite"
   474 by (auto intro!: HInfinite_add_ge_zero simp add: add.commute)
   475 
   476 lemma HInfinite_add_gt_zero:
   477      "[|(x::hypreal) \<in> HInfinite; 0 < y; 0 < x|] ==> (x + y): HInfinite"
   478 by (blast intro: HInfinite_add_ge_zero order_less_imp_le)
   479 
   480 lemma HInfinite_minus_iff: "(-x \<in> HInfinite) = (x \<in> HInfinite)"
   481 by (simp add: HInfinite_def)
   482 
   483 lemma HInfinite_add_le_zero:
   484      "[|(x::hypreal) \<in> HInfinite; y \<le> 0; x \<le> 0|] ==> (x + y): HInfinite"
   485 apply (drule HInfinite_minus_iff [THEN iffD2])
   486 apply (rule HInfinite_minus_iff [THEN iffD1])
   487 apply (simp only: minus_add add.commute)
   488 apply (rule HInfinite_add_ge_zero)
   489 apply simp_all
   490 done
   491 
   492 lemma HInfinite_add_lt_zero:
   493      "[|(x::hypreal) \<in> HInfinite; y < 0; x < 0|] ==> (x + y): HInfinite"
   494 by (blast intro: HInfinite_add_le_zero order_less_imp_le)
   495 
   496 lemma HFinite_sum_squares:
   497   fixes a b c :: "'a::real_normed_algebra star"
   498   shows "[|a: HFinite; b: HFinite; c: HFinite|]
   499       ==> a*a + b*b + c*c \<in> HFinite"
   500 by (auto intro: HFinite_mult HFinite_add)
   501 
   502 lemma not_Infinitesimal_not_zero: "x \<notin> Infinitesimal ==> x \<noteq> 0"
   503 by auto
   504 
   505 lemma not_Infinitesimal_not_zero2: "x \<in> HFinite - Infinitesimal ==> x \<noteq> 0"
   506 by auto
   507 
   508 lemma HFinite_diff_Infinitesimal_hrabs:
   509   "(x::hypreal) \<in> HFinite - Infinitesimal ==> \<bar>x\<bar> \<in> HFinite - Infinitesimal"
   510 by blast
   511 
   512 lemma hnorm_le_Infinitesimal:
   513   "\<lbrakk>e \<in> Infinitesimal; hnorm x \<le> e\<rbrakk> \<Longrightarrow> x \<in> Infinitesimal"
   514 by (auto simp add: Infinitesimal_def abs_less_iff)
   515 
   516 lemma hnorm_less_Infinitesimal:
   517   "\<lbrakk>e \<in> Infinitesimal; hnorm x < e\<rbrakk> \<Longrightarrow> x \<in> Infinitesimal"
   518 by (erule hnorm_le_Infinitesimal, erule order_less_imp_le)
   519 
   520 lemma hrabs_le_Infinitesimal:
   521      "[| e \<in> Infinitesimal; \<bar>x::hypreal\<bar> \<le> e |] ==> x \<in> Infinitesimal"
   522 by (erule hnorm_le_Infinitesimal, simp)
   523 
   524 lemma hrabs_less_Infinitesimal:
   525       "[| e \<in> Infinitesimal; \<bar>x::hypreal\<bar> < e |] ==> x \<in> Infinitesimal"
   526 by (erule hnorm_less_Infinitesimal, simp)
   527 
   528 lemma Infinitesimal_interval:
   529       "[| e \<in> Infinitesimal; e' \<in> Infinitesimal; e' < x ; x < e |]
   530        ==> (x::hypreal) \<in> Infinitesimal"
   531 by (auto simp add: Infinitesimal_def abs_less_iff)
   532 
   533 lemma Infinitesimal_interval2:
   534      "[| e \<in> Infinitesimal; e' \<in> Infinitesimal;
   535          e' \<le> x ; x \<le> e |] ==> (x::hypreal) \<in> Infinitesimal"
   536 by (auto intro: Infinitesimal_interval simp add: order_le_less)
   537 
   538 
   539 lemma lemma_Infinitesimal_hyperpow:
   540      "[| (x::hypreal) \<in> Infinitesimal; 0 < N |] ==> \<bar>x pow N\<bar> \<le> \<bar>x\<bar>"
   541 apply (unfold Infinitesimal_def)
   542 apply (auto intro!: hyperpow_Suc_le_self2
   543           simp add: hyperpow_hrabs [symmetric] hypnat_gt_zero_iff2 abs_ge_zero)
   544 done
   545 
   546 lemma Infinitesimal_hyperpow:
   547      "[| (x::hypreal) \<in> Infinitesimal; 0 < N |] ==> x pow N \<in> Infinitesimal"
   548 apply (rule hrabs_le_Infinitesimal)
   549 apply (rule_tac [2] lemma_Infinitesimal_hyperpow, auto)
   550 done
   551 
   552 lemma hrealpow_hyperpow_Infinitesimal_iff:
   553      "(x ^ n \<in> Infinitesimal) = (x pow (hypnat_of_nat n) \<in> Infinitesimal)"
   554 by (simp only: hyperpow_hypnat_of_nat)
   555 
   556 lemma Infinitesimal_hrealpow:
   557      "[| (x::hypreal) \<in> Infinitesimal; 0 < n |] ==> x ^ n \<in> Infinitesimal"
   558 by (simp add: hrealpow_hyperpow_Infinitesimal_iff Infinitesimal_hyperpow)
   559 
   560 lemma not_Infinitesimal_mult:
   561   fixes x y :: "'a::real_normed_div_algebra star"
   562   shows "[| x \<notin> Infinitesimal;  y \<notin> Infinitesimal|] ==> (x*y) \<notin>Infinitesimal"
   563 apply (unfold Infinitesimal_def, clarify, rename_tac r s)
   564 apply (simp only: linorder_not_less hnorm_mult)
   565 apply (drule_tac x = "r * s" in bspec)
   566 apply (fast intro: Reals_mult)
   567 apply (simp)
   568 apply (drule_tac c = s and d = "hnorm y" and a = r and b = "hnorm x" in mult_mono)
   569 apply (simp_all (no_asm_simp))
   570 done
   571 
   572 lemma Infinitesimal_mult_disj:
   573   fixes x y :: "'a::real_normed_div_algebra star"
   574   shows "x*y \<in> Infinitesimal ==> x \<in> Infinitesimal | y \<in> Infinitesimal"
   575 apply (rule ccontr)
   576 apply (drule de_Morgan_disj [THEN iffD1])
   577 apply (fast dest: not_Infinitesimal_mult)
   578 done
   579 
   580 lemma HFinite_Infinitesimal_not_zero: "x \<in> HFinite-Infinitesimal ==> x \<noteq> 0"
   581 by blast
   582 
   583 lemma HFinite_Infinitesimal_diff_mult:
   584   fixes x y :: "'a::real_normed_div_algebra star"
   585   shows "[| x \<in> HFinite - Infinitesimal;
   586                    y \<in> HFinite - Infinitesimal
   587                 |] ==> (x*y) \<in> HFinite - Infinitesimal"
   588 apply clarify
   589 apply (blast dest: HFinite_mult not_Infinitesimal_mult)
   590 done
   591 
   592 lemma Infinitesimal_subset_HFinite:
   593       "Infinitesimal \<subseteq> HFinite"
   594 apply (simp add: Infinitesimal_def HFinite_def, auto)
   595 apply (rule_tac x = 1 in bexI, auto)
   596 done
   597 
   598 lemma Infinitesimal_star_of_mult:
   599   fixes x :: "'a::real_normed_algebra star"
   600   shows "x \<in> Infinitesimal ==> x * star_of r \<in> Infinitesimal"
   601 by (erule HFinite_star_of [THEN [2] Infinitesimal_HFinite_mult])
   602 
   603 lemma Infinitesimal_star_of_mult2:
   604   fixes x :: "'a::real_normed_algebra star"
   605   shows "x \<in> Infinitesimal ==> star_of r * x \<in> Infinitesimal"
   606 by (erule HFinite_star_of [THEN [2] Infinitesimal_HFinite_mult2])
   607 
   608 
   609 subsection\<open>The Infinitely Close Relation\<close>
   610 
   611 lemma mem_infmal_iff: "(x \<in> Infinitesimal) = (x \<approx> 0)"
   612 by (simp add: Infinitesimal_def approx_def)
   613 
   614 lemma approx_minus_iff: " (x \<approx> y) = (x - y \<approx> 0)"
   615 by (simp add: approx_def)
   616 
   617 lemma approx_minus_iff2: " (x \<approx> y) = (-y + x \<approx> 0)"
   618 by (simp add: approx_def add.commute)
   619 
   620 lemma approx_refl [iff]: "x \<approx> x"
   621 by (simp add: approx_def Infinitesimal_def)
   622 
   623 lemma hypreal_minus_distrib1: "-(y + -(x::'a::ab_group_add)) = x + -y"
   624 by (simp add: add.commute)
   625 
   626 lemma approx_sym: "x \<approx> y ==> y \<approx> x"
   627 apply (simp add: approx_def)
   628 apply (drule Infinitesimal_minus_iff [THEN iffD2])
   629 apply simp
   630 done
   631 
   632 lemma approx_trans: "[| x \<approx> y; y \<approx> z |] ==> x \<approx> z"
   633 apply (simp add: approx_def)
   634 apply (drule (1) Infinitesimal_add)
   635 apply simp
   636 done
   637 
   638 lemma approx_trans2: "[| r \<approx> x; s \<approx> x |] ==> r \<approx> s"
   639 by (blast intro: approx_sym approx_trans)
   640 
   641 lemma approx_trans3: "[| x \<approx> r; x \<approx> s|] ==> r \<approx> s"
   642 by (blast intro: approx_sym approx_trans)
   643 
   644 lemma approx_reorient: "(x \<approx> y) = (y \<approx> x)"
   645 by (blast intro: approx_sym)
   646 
   647 (*reorientation simplification procedure: reorients (polymorphic)
   648   0 = x, 1 = x, nnn = x provided x isn't 0, 1 or a numeral.*)
   649 simproc_setup approx_reorient_simproc
   650   ("0 \<approx> x" | "1 \<approx> y" | "numeral w \<approx> z" | "- 1 \<approx> y" | "- numeral w \<approx> r") =
   651 \<open>
   652   let val rule = @{thm approx_reorient} RS eq_reflection
   653       fun proc phi ss ct =
   654         case Thm.term_of ct of
   655           _ $ t $ u => if can HOLogic.dest_number u then NONE
   656             else if can HOLogic.dest_number t then SOME rule else NONE
   657         | _ => NONE
   658   in proc end
   659 \<close>
   660 
   661 lemma Infinitesimal_approx_minus: "(x-y \<in> Infinitesimal) = (x \<approx> y)"
   662 by (simp add: approx_minus_iff [symmetric] mem_infmal_iff)
   663 
   664 lemma approx_monad_iff: "(x \<approx> y) = (monad(x)=monad(y))"
   665 apply (simp add: monad_def)
   666 apply (auto dest: approx_sym elim!: approx_trans equalityCE)
   667 done
   668 
   669 lemma Infinitesimal_approx:
   670      "[| x \<in> Infinitesimal; y \<in> Infinitesimal |] ==> x \<approx> y"
   671 apply (simp add: mem_infmal_iff)
   672 apply (blast intro: approx_trans approx_sym)
   673 done
   674 
   675 lemma approx_add: "[| a \<approx> b; c \<approx> d |] ==> a+c \<approx> b+d"
   676 proof (unfold approx_def)
   677   assume inf: "a - b \<in> Infinitesimal" "c - d \<in> Infinitesimal"
   678   have "a + c - (b + d) = (a - b) + (c - d)" by simp
   679   also have "... \<in> Infinitesimal" using inf by (rule Infinitesimal_add)
   680   finally show "a + c - (b + d) \<in> Infinitesimal" .
   681 qed
   682 
   683 lemma approx_minus: "a \<approx> b ==> -a \<approx> -b"
   684 apply (rule approx_minus_iff [THEN iffD2, THEN approx_sym])
   685 apply (drule approx_minus_iff [THEN iffD1])
   686 apply (simp add: add.commute)
   687 done
   688 
   689 lemma approx_minus2: "-a \<approx> -b ==> a \<approx> b"
   690 by (auto dest: approx_minus)
   691 
   692 lemma approx_minus_cancel [simp]: "(-a \<approx> -b) = (a \<approx> b)"
   693 by (blast intro: approx_minus approx_minus2)
   694 
   695 lemma approx_add_minus: "[| a \<approx> b; c \<approx> d |] ==> a + -c \<approx> b + -d"
   696 by (blast intro!: approx_add approx_minus)
   697 
   698 lemma approx_diff: "[| a \<approx> b; c \<approx> d |] ==> a - c \<approx> b - d"
   699   using approx_add [of a b "- c" "- d"] by simp
   700 
   701 lemma approx_mult1:
   702   fixes a b c :: "'a::real_normed_algebra star"
   703   shows "[| a \<approx> b; c: HFinite|] ==> a*c \<approx> b*c"
   704 by (simp add: approx_def Infinitesimal_HFinite_mult
   705               left_diff_distrib [symmetric])
   706 
   707 lemma approx_mult2:
   708   fixes a b c :: "'a::real_normed_algebra star"
   709   shows "[|a \<approx> b; c: HFinite|] ==> c*a \<approx> c*b"
   710 by (simp add: approx_def Infinitesimal_HFinite_mult2
   711               right_diff_distrib [symmetric])
   712 
   713 lemma approx_mult_subst:
   714   fixes u v x y :: "'a::real_normed_algebra star"
   715   shows "[|u \<approx> v*x; x \<approx> y; v \<in> HFinite|] ==> u \<approx> v*y"
   716 by (blast intro: approx_mult2 approx_trans)
   717 
   718 lemma approx_mult_subst2:
   719   fixes u v x y :: "'a::real_normed_algebra star"
   720   shows "[| u \<approx> x*v; x \<approx> y; v \<in> HFinite |] ==> u \<approx> y*v"
   721 by (blast intro: approx_mult1 approx_trans)
   722 
   723 lemma approx_mult_subst_star_of:
   724   fixes u x y :: "'a::real_normed_algebra star"
   725   shows "[| u \<approx> x*star_of v; x \<approx> y |] ==> u \<approx> y*star_of v"
   726 by (auto intro: approx_mult_subst2)
   727 
   728 lemma approx_eq_imp: "a = b ==> a \<approx> b"
   729 by (simp add: approx_def)
   730 
   731 lemma Infinitesimal_minus_approx: "x \<in> Infinitesimal ==> -x \<approx> x"
   732 by (blast intro: Infinitesimal_minus_iff [THEN iffD2]
   733                     mem_infmal_iff [THEN iffD1] approx_trans2)
   734 
   735 lemma bex_Infinitesimal_iff: "(\<exists>y \<in> Infinitesimal. x - z = y) = (x \<approx> z)"
   736 by (simp add: approx_def)
   737 
   738 lemma bex_Infinitesimal_iff2: "(\<exists>y \<in> Infinitesimal. x = z + y) = (x \<approx> z)"
   739 by (force simp add: bex_Infinitesimal_iff [symmetric])
   740 
   741 lemma Infinitesimal_add_approx: "[| y \<in> Infinitesimal; x + y = z |] ==> x \<approx> z"
   742 apply (rule bex_Infinitesimal_iff [THEN iffD1])
   743 apply (drule Infinitesimal_minus_iff [THEN iffD2])
   744 apply (auto simp add: add.assoc [symmetric])
   745 done
   746 
   747 lemma Infinitesimal_add_approx_self: "y \<in> Infinitesimal ==> x \<approx> x + y"
   748 apply (rule bex_Infinitesimal_iff [THEN iffD1])
   749 apply (drule Infinitesimal_minus_iff [THEN iffD2])
   750 apply (auto simp add: add.assoc [symmetric])
   751 done
   752 
   753 lemma Infinitesimal_add_approx_self2: "y \<in> Infinitesimal ==> x \<approx> y + x"
   754 by (auto dest: Infinitesimal_add_approx_self simp add: add.commute)
   755 
   756 lemma Infinitesimal_add_minus_approx_self: "y \<in> Infinitesimal ==> x \<approx> x + -y"
   757 by (blast intro!: Infinitesimal_add_approx_self Infinitesimal_minus_iff [THEN iffD2])
   758 
   759 lemma Infinitesimal_add_cancel: "[| y \<in> Infinitesimal; x+y \<approx> z|] ==> x \<approx> z"
   760 apply (drule_tac x = x in Infinitesimal_add_approx_self [THEN approx_sym])
   761 apply (erule approx_trans3 [THEN approx_sym], assumption)
   762 done
   763 
   764 lemma Infinitesimal_add_right_cancel:
   765      "[| y \<in> Infinitesimal; x \<approx> z + y|] ==> x \<approx> z"
   766 apply (drule_tac x = z in Infinitesimal_add_approx_self2 [THEN approx_sym])
   767 apply (erule approx_trans3 [THEN approx_sym])
   768 apply (simp add: add.commute)
   769 apply (erule approx_sym)
   770 done
   771 
   772 lemma approx_add_left_cancel: "d + b  \<approx> d + c ==> b \<approx> c"
   773 apply (drule approx_minus_iff [THEN iffD1])
   774 apply (simp add: approx_minus_iff [symmetric] ac_simps)
   775 done
   776 
   777 lemma approx_add_right_cancel: "b + d \<approx> c + d ==> b \<approx> c"
   778 apply (rule approx_add_left_cancel)
   779 apply (simp add: add.commute)
   780 done
   781 
   782 lemma approx_add_mono1: "b \<approx> c ==> d + b \<approx> d + c"
   783 apply (rule approx_minus_iff [THEN iffD2])
   784 apply (simp add: approx_minus_iff [symmetric] ac_simps)
   785 done
   786 
   787 lemma approx_add_mono2: "b \<approx> c ==> b + a \<approx> c + a"
   788 by (simp add: add.commute approx_add_mono1)
   789 
   790 lemma approx_add_left_iff [simp]: "(a + b \<approx> a + c) = (b \<approx> c)"
   791 by (fast elim: approx_add_left_cancel approx_add_mono1)
   792 
   793 lemma approx_add_right_iff [simp]: "(b + a \<approx> c + a) = (b \<approx> c)"
   794 by (simp add: add.commute)
   795 
   796 lemma approx_HFinite: "[| x \<in> HFinite; x \<approx> y |] ==> y \<in> HFinite"
   797 apply (drule bex_Infinitesimal_iff2 [THEN iffD2], safe)
   798 apply (drule Infinitesimal_subset_HFinite [THEN subsetD, THEN HFinite_minus_iff [THEN iffD2]])
   799 apply (drule HFinite_add)
   800 apply (auto simp add: add.assoc)
   801 done
   802 
   803 lemma approx_star_of_HFinite: "x \<approx> star_of D ==> x \<in> HFinite"
   804 by (rule approx_sym [THEN [2] approx_HFinite], auto)
   805 
   806 lemma approx_mult_HFinite:
   807   fixes a b c d :: "'a::real_normed_algebra star"
   808   shows "[|a \<approx> b; c \<approx> d; b: HFinite; d: HFinite|] ==> a*c \<approx> b*d"
   809 apply (rule approx_trans)
   810 apply (rule_tac [2] approx_mult2)
   811 apply (rule approx_mult1)
   812 prefer 2 apply (blast intro: approx_HFinite approx_sym, auto)
   813 done
   814 
   815 lemma scaleHR_left_diff_distrib:
   816   "\<And>a b x. scaleHR (a - b) x = scaleHR a x - scaleHR b x"
   817 by transfer (rule scaleR_left_diff_distrib)
   818 
   819 lemma approx_scaleR1:
   820   "[| a \<approx> star_of b; c: HFinite|] ==> scaleHR a c \<approx> b *\<^sub>R c"
   821 apply (unfold approx_def)
   822 apply (drule (1) Infinitesimal_HFinite_scaleHR)
   823 apply (simp only: scaleHR_left_diff_distrib)
   824 apply (simp add: scaleHR_def star_scaleR_def [symmetric])
   825 done
   826 
   827 lemma approx_scaleR2:
   828   "a \<approx> b ==> c *\<^sub>R a \<approx> c *\<^sub>R b"
   829 by (simp add: approx_def Infinitesimal_scaleR2
   830               scaleR_right_diff_distrib [symmetric])
   831 
   832 lemma approx_scaleR_HFinite:
   833   "[|a \<approx> star_of b; c \<approx> d; d: HFinite|] ==> scaleHR a c \<approx> b *\<^sub>R d"
   834 apply (rule approx_trans)
   835 apply (rule_tac [2] approx_scaleR2)
   836 apply (rule approx_scaleR1)
   837 prefer 2 apply (blast intro: approx_HFinite approx_sym, auto)
   838 done
   839 
   840 lemma approx_mult_star_of:
   841   fixes a c :: "'a::real_normed_algebra star"
   842   shows "[|a \<approx> star_of b; c \<approx> star_of d |]
   843       ==> a*c \<approx> star_of b*star_of d"
   844 by (blast intro!: approx_mult_HFinite approx_star_of_HFinite HFinite_star_of)
   845 
   846 lemma approx_SReal_mult_cancel_zero:
   847      "[| (a::hypreal) \<in> \<real>; a \<noteq> 0; a*x \<approx> 0 |] ==> x \<approx> 0"
   848 apply (drule Reals_inverse [THEN SReal_subset_HFinite [THEN subsetD]])
   849 apply (auto dest: approx_mult2 simp add: mult.assoc [symmetric])
   850 done
   851 
   852 lemma approx_mult_SReal1: "[| (a::hypreal) \<in> \<real>; x \<approx> 0 |] ==> x*a \<approx> 0"
   853 by (auto dest: SReal_subset_HFinite [THEN subsetD] approx_mult1)
   854 
   855 lemma approx_mult_SReal2: "[| (a::hypreal) \<in> \<real>; x \<approx> 0 |] ==> a*x \<approx> 0"
   856 by (auto dest: SReal_subset_HFinite [THEN subsetD] approx_mult2)
   857 
   858 lemma approx_mult_SReal_zero_cancel_iff [simp]:
   859      "[|(a::hypreal) \<in> \<real>; a \<noteq> 0 |] ==> (a*x \<approx> 0) = (x \<approx> 0)"
   860 by (blast intro: approx_SReal_mult_cancel_zero approx_mult_SReal2)
   861 
   862 lemma approx_SReal_mult_cancel:
   863      "[| (a::hypreal) \<in> \<real>; a \<noteq> 0; a* w \<approx> a*z |] ==> w \<approx> z"
   864 apply (drule Reals_inverse [THEN SReal_subset_HFinite [THEN subsetD]])
   865 apply (auto dest: approx_mult2 simp add: mult.assoc [symmetric])
   866 done
   867 
   868 lemma approx_SReal_mult_cancel_iff1 [simp]:
   869      "[| (a::hypreal) \<in> \<real>; a \<noteq> 0|] ==> (a* w \<approx> a*z) = (w \<approx> z)"
   870 by (auto intro!: approx_mult2 SReal_subset_HFinite [THEN subsetD]
   871          intro: approx_SReal_mult_cancel)
   872 
   873 lemma approx_le_bound: "[| (z::hypreal) \<le> f; f \<approx> g; g \<le> z |] ==> f \<approx> z"
   874 apply (simp add: bex_Infinitesimal_iff2 [symmetric], auto)
   875 apply (rule_tac x = "g+y-z" in bexI)
   876 apply (simp (no_asm))
   877 apply (rule Infinitesimal_interval2)
   878 apply (rule_tac [2] Infinitesimal_zero, auto)
   879 done
   880 
   881 lemma approx_hnorm:
   882   fixes x y :: "'a::real_normed_vector star"
   883   shows "x \<approx> y \<Longrightarrow> hnorm x \<approx> hnorm y"
   884 proof (unfold approx_def)
   885   assume "x - y \<in> Infinitesimal"
   886   hence 1: "hnorm (x - y) \<in> Infinitesimal"
   887     by (simp only: Infinitesimal_hnorm_iff)
   888   moreover have 2: "(0::real star) \<in> Infinitesimal"
   889     by (rule Infinitesimal_zero)
   890   moreover have 3: "0 \<le> \<bar>hnorm x - hnorm y\<bar>"
   891     by (rule abs_ge_zero)
   892   moreover have 4: "\<bar>hnorm x - hnorm y\<bar> \<le> hnorm (x - y)"
   893     by (rule hnorm_triangle_ineq3)
   894   ultimately have "\<bar>hnorm x - hnorm y\<bar> \<in> Infinitesimal"
   895     by (rule Infinitesimal_interval2)
   896   thus "hnorm x - hnorm y \<in> Infinitesimal"
   897     by (simp only: Infinitesimal_hrabs_iff)
   898 qed
   899 
   900 
   901 subsection\<open>Zero is the Only Infinitesimal that is also a Real\<close>
   902 
   903 lemma Infinitesimal_less_SReal:
   904      "[| (x::hypreal) \<in> \<real>; y \<in> Infinitesimal; 0 < x |] ==> y < x"
   905 apply (simp add: Infinitesimal_def)
   906 apply (rule abs_ge_self [THEN order_le_less_trans], auto)
   907 done
   908 
   909 lemma Infinitesimal_less_SReal2:
   910      "(y::hypreal) \<in> Infinitesimal ==> \<forall>r \<in> Reals. 0 < r --> y < r"
   911 by (blast intro: Infinitesimal_less_SReal)
   912 
   913 lemma SReal_not_Infinitesimal:
   914      "[| 0 < y;  (y::hypreal) \<in> \<real>|] ==> y \<notin> Infinitesimal"
   915 apply (simp add: Infinitesimal_def)
   916 apply (auto simp add: abs_if)
   917 done
   918 
   919 lemma SReal_minus_not_Infinitesimal:
   920      "[| y < 0;  (y::hypreal) \<in> \<real> |] ==> y \<notin> Infinitesimal"
   921 apply (subst Infinitesimal_minus_iff [symmetric])
   922 apply (rule SReal_not_Infinitesimal, auto)
   923 done
   924 
   925 lemma SReal_Int_Infinitesimal_zero: "\<real> Int Infinitesimal = {0::hypreal}"
   926 apply auto
   927 apply (cut_tac x = x and y = 0 in linorder_less_linear)
   928 apply (blast dest: SReal_not_Infinitesimal SReal_minus_not_Infinitesimal)
   929 done
   930 
   931 lemma SReal_Infinitesimal_zero:
   932   "[| (x::hypreal) \<in> \<real>; x \<in> Infinitesimal|] ==> x = 0"
   933 by (cut_tac SReal_Int_Infinitesimal_zero, blast)
   934 
   935 lemma SReal_HFinite_diff_Infinitesimal:
   936      "[| (x::hypreal) \<in> \<real>; x \<noteq> 0 |] ==> x \<in> HFinite - Infinitesimal"
   937 by (auto dest: SReal_Infinitesimal_zero SReal_subset_HFinite [THEN subsetD])
   938 
   939 lemma hypreal_of_real_HFinite_diff_Infinitesimal:
   940      "hypreal_of_real x \<noteq> 0 ==> hypreal_of_real x \<in> HFinite - Infinitesimal"
   941 by (rule SReal_HFinite_diff_Infinitesimal, auto)
   942 
   943 lemma star_of_Infinitesimal_iff_0 [iff]:
   944   "(star_of x \<in> Infinitesimal) = (x = 0)"
   945 apply (auto simp add: Infinitesimal_def)
   946 apply (drule_tac x="hnorm (star_of x)" in bspec)
   947 apply (simp add: SReal_def)
   948 apply (rule_tac x="norm x" in exI, simp)
   949 apply simp
   950 done
   951 
   952 lemma star_of_HFinite_diff_Infinitesimal:
   953      "x \<noteq> 0 ==> star_of x \<in> HFinite - Infinitesimal"
   954 by simp
   955 
   956 lemma numeral_not_Infinitesimal [simp]:
   957      "numeral w \<noteq> (0::hypreal) ==> (numeral w :: hypreal) \<notin> Infinitesimal"
   958 by (fast dest: Reals_numeral [THEN SReal_Infinitesimal_zero])
   959 
   960 (*again: 1 is a special case, but not 0 this time*)
   961 lemma one_not_Infinitesimal [simp]:
   962   "(1::'a::{real_normed_vector,zero_neq_one} star) \<notin> Infinitesimal"
   963 apply (simp only: star_one_def star_of_Infinitesimal_iff_0)
   964 apply simp
   965 done
   966 
   967 lemma approx_SReal_not_zero:
   968   "[| (y::hypreal) \<in> \<real>; x \<approx> y; y\<noteq> 0 |] ==> x \<noteq> 0"
   969 apply (cut_tac x = 0 and y = y in linorder_less_linear, simp)
   970 apply (blast dest: approx_sym [THEN mem_infmal_iff [THEN iffD2]] SReal_not_Infinitesimal SReal_minus_not_Infinitesimal)
   971 done
   972 
   973 lemma HFinite_diff_Infinitesimal_approx:
   974      "[| x \<approx> y; y \<in> HFinite - Infinitesimal |]
   975       ==> x \<in> HFinite - Infinitesimal"
   976 apply (auto intro: approx_sym [THEN [2] approx_HFinite]
   977             simp add: mem_infmal_iff)
   978 apply (drule approx_trans3, assumption)
   979 apply (blast dest: approx_sym)
   980 done
   981 
   982 (*The premise y\<noteq>0 is essential; otherwise x/y =0 and we lose the
   983   HFinite premise.*)
   984 lemma Infinitesimal_ratio:
   985   fixes x y :: "'a::{real_normed_div_algebra,field} star"
   986   shows "[| y \<noteq> 0;  y \<in> Infinitesimal;  x/y \<in> HFinite |]
   987          ==> x \<in> Infinitesimal"
   988 apply (drule Infinitesimal_HFinite_mult2, assumption)
   989 apply (simp add: divide_inverse mult.assoc)
   990 done
   991 
   992 lemma Infinitesimal_SReal_divide:
   993   "[| (x::hypreal) \<in> Infinitesimal; y \<in> \<real> |] ==> x/y \<in> Infinitesimal"
   994 apply (simp add: divide_inverse)
   995 apply (auto intro!: Infinitesimal_HFinite_mult
   996             dest!: Reals_inverse [THEN SReal_subset_HFinite [THEN subsetD]])
   997 done
   998 
   999 (*------------------------------------------------------------------
  1000        Standard Part Theorem: Every finite x: R* is infinitely
  1001        close to a unique real number (i.e a member of Reals)
  1002  ------------------------------------------------------------------*)
  1003 
  1004 subsection\<open>Uniqueness: Two Infinitely Close Reals are Equal\<close>
  1005 
  1006 lemma star_of_approx_iff [simp]: "(star_of x \<approx> star_of y) = (x = y)"
  1007 apply safe
  1008 apply (simp add: approx_def)
  1009 apply (simp only: star_of_diff [symmetric])
  1010 apply (simp only: star_of_Infinitesimal_iff_0)
  1011 apply simp
  1012 done
  1013 
  1014 lemma SReal_approx_iff:
  1015   "[|(x::hypreal) \<in> \<real>; y \<in> \<real>|] ==> (x \<approx> y) = (x = y)"
  1016 apply auto
  1017 apply (simp add: approx_def)
  1018 apply (drule (1) Reals_diff)
  1019 apply (drule (1) SReal_Infinitesimal_zero)
  1020 apply simp
  1021 done
  1022 
  1023 lemma numeral_approx_iff [simp]:
  1024      "(numeral v \<approx> (numeral w :: 'a::{numeral,real_normed_vector} star)) =
  1025       (numeral v = (numeral w :: 'a))"
  1026 apply (unfold star_numeral_def)
  1027 apply (rule star_of_approx_iff)
  1028 done
  1029 
  1030 (*And also for 0 \<approx> #nn and 1 \<approx> #nn, #nn \<approx> 0 and #nn \<approx> 1.*)
  1031 lemma [simp]:
  1032   "(numeral w \<approx> (0::'a::{numeral,real_normed_vector} star)) =
  1033    (numeral w = (0::'a))"
  1034   "((0::'a::{numeral,real_normed_vector} star) \<approx> numeral w) =
  1035    (numeral w = (0::'a))"
  1036   "(numeral w \<approx> (1::'b::{numeral,one,real_normed_vector} star)) =
  1037    (numeral w = (1::'b))"
  1038   "((1::'b::{numeral,one,real_normed_vector} star) \<approx> numeral w) =
  1039    (numeral w = (1::'b))"
  1040   "~ (0 \<approx> (1::'c::{zero_neq_one,real_normed_vector} star))"
  1041   "~ (1 \<approx> (0::'c::{zero_neq_one,real_normed_vector} star))"
  1042 apply (unfold star_numeral_def star_zero_def star_one_def)
  1043 apply (unfold star_of_approx_iff)
  1044 by (auto intro: sym)
  1045 
  1046 lemma star_of_approx_numeral_iff [simp]:
  1047      "(star_of k \<approx> numeral w) = (k = numeral w)"
  1048 by (subst star_of_approx_iff [symmetric], auto)
  1049 
  1050 lemma star_of_approx_zero_iff [simp]: "(star_of k \<approx> 0) = (k = 0)"
  1051 by (simp_all add: star_of_approx_iff [symmetric])
  1052 
  1053 lemma star_of_approx_one_iff [simp]: "(star_of k \<approx> 1) = (k = 1)"
  1054 by (simp_all add: star_of_approx_iff [symmetric])
  1055 
  1056 lemma approx_unique_real:
  1057      "[| (r::hypreal) \<in> \<real>; s \<in> \<real>; r \<approx> x; s \<approx> x|] ==> r = s"
  1058 by (blast intro: SReal_approx_iff [THEN iffD1] approx_trans2)
  1059 
  1060 
  1061 subsection\<open>Existence of Unique Real Infinitely Close\<close>
  1062 
  1063 subsubsection\<open>Lifting of the Ub and Lub Properties\<close>
  1064 
  1065 lemma hypreal_of_real_isUb_iff:
  1066       "(isUb \<real> (hypreal_of_real ` Q) (hypreal_of_real Y)) =
  1067        (isUb (UNIV :: real set) Q Y)"
  1068 by (simp add: isUb_def setle_def)
  1069 
  1070 lemma hypreal_of_real_isLub1:
  1071      "isLub \<real> (hypreal_of_real ` Q) (hypreal_of_real Y)
  1072       ==> isLub (UNIV :: real set) Q Y"
  1073 apply (simp add: isLub_def leastP_def)
  1074 apply (auto intro: hypreal_of_real_isUb_iff [THEN iffD2]
  1075             simp add: hypreal_of_real_isUb_iff setge_def)
  1076 done
  1077 
  1078 lemma hypreal_of_real_isLub2:
  1079       "isLub (UNIV :: real set) Q Y
  1080        ==> isLub \<real> (hypreal_of_real ` Q) (hypreal_of_real Y)"
  1081 apply (auto simp add: isLub_def leastP_def hypreal_of_real_isUb_iff setge_def)
  1082 by (metis SReal_iff hypreal_of_real_isUb_iff isUbD2a star_of_le)
  1083 
  1084 lemma hypreal_of_real_isLub_iff:
  1085      "(isLub \<real> (hypreal_of_real ` Q) (hypreal_of_real Y)) =
  1086       (isLub (UNIV :: real set) Q Y)"
  1087 by (blast intro: hypreal_of_real_isLub1 hypreal_of_real_isLub2)
  1088 
  1089 lemma lemma_isUb_hypreal_of_real:
  1090      "isUb \<real> P Y ==> \<exists>Yo. isUb \<real> P (hypreal_of_real Yo)"
  1091 by (auto simp add: SReal_iff isUb_def)
  1092 
  1093 lemma lemma_isLub_hypreal_of_real:
  1094      "isLub \<real> P Y ==> \<exists>Yo. isLub \<real> P (hypreal_of_real Yo)"
  1095 by (auto simp add: isLub_def leastP_def isUb_def SReal_iff)
  1096 
  1097 lemma lemma_isLub_hypreal_of_real2:
  1098      "\<exists>Yo. isLub \<real> P (hypreal_of_real Yo) ==> \<exists>Y. isLub \<real> P Y"
  1099 by (auto simp add: isLub_def leastP_def isUb_def)
  1100 
  1101 lemma SReal_complete:
  1102      "[| P \<subseteq> \<real>;  \<exists>x. x \<in> P;  \<exists>Y. isUb \<real> P Y |]
  1103       ==> \<exists>t::hypreal. isLub \<real> P t"
  1104 apply (frule SReal_hypreal_of_real_image)
  1105 apply (auto, drule lemma_isUb_hypreal_of_real)
  1106 apply (auto intro!: reals_complete lemma_isLub_hypreal_of_real2
  1107             simp add: hypreal_of_real_isLub_iff hypreal_of_real_isUb_iff)
  1108 done
  1109 
  1110 (* lemma about lubs *)
  1111 
  1112 lemma lemma_st_part_ub:
  1113      "(x::hypreal) \<in> HFinite ==> \<exists>u. isUb \<real> {s. s \<in> \<real> & s < x} u"
  1114 apply (drule HFiniteD, safe)
  1115 apply (rule exI, rule isUbI)
  1116 apply (auto intro: setleI isUbI simp add: abs_less_iff)
  1117 done
  1118 
  1119 lemma lemma_st_part_nonempty:
  1120   "(x::hypreal) \<in> HFinite ==> \<exists>y. y \<in> {s. s \<in> \<real> & s < x}"
  1121 apply (drule HFiniteD, safe)
  1122 apply (drule Reals_minus)
  1123 apply (rule_tac x = "-t" in exI)
  1124 apply (auto simp add: abs_less_iff)
  1125 done
  1126 
  1127 lemma lemma_st_part_lub:
  1128      "(x::hypreal) \<in> HFinite ==> \<exists>t. isLub \<real> {s. s \<in> \<real> & s < x} t"
  1129 by (blast intro!: SReal_complete lemma_st_part_ub lemma_st_part_nonempty Collect_restrict)
  1130 
  1131 lemma lemma_st_part_le1:
  1132      "[| (x::hypreal) \<in> HFinite;  isLub \<real> {s. s \<in> \<real> & s < x} t;
  1133          r \<in> \<real>;  0 < r |] ==> x \<le> t + r"
  1134 apply (frule isLubD1a)
  1135 apply (rule ccontr, drule linorder_not_le [THEN iffD2])
  1136 apply (drule (1) Reals_add)
  1137 apply (drule_tac y = "r + t" in isLubD1 [THEN setleD], auto)
  1138 done
  1139 
  1140 lemma hypreal_setle_less_trans:
  1141      "[| S *<= (x::hypreal); x < y |] ==> S *<= y"
  1142 apply (simp add: setle_def)
  1143 apply (auto dest!: bspec order_le_less_trans intro: order_less_imp_le)
  1144 done
  1145 
  1146 lemma hypreal_gt_isUb:
  1147      "[| isUb R S (x::hypreal); x < y; y \<in> R |] ==> isUb R S y"
  1148 apply (simp add: isUb_def)
  1149 apply (blast intro: hypreal_setle_less_trans)
  1150 done
  1151 
  1152 lemma lemma_st_part_gt_ub:
  1153      "[| (x::hypreal) \<in> HFinite; x < y; y \<in> \<real> |]
  1154       ==> isUb \<real> {s. s \<in> \<real> & s < x} y"
  1155 by (auto dest: order_less_trans intro: order_less_imp_le intro!: isUbI setleI)
  1156 
  1157 lemma lemma_minus_le_zero: "t \<le> t + -r ==> r \<le> (0::hypreal)"
  1158 apply (drule_tac c = "-t" in add_left_mono)
  1159 apply (auto simp add: add.assoc [symmetric])
  1160 done
  1161 
  1162 lemma lemma_st_part_le2:
  1163      "[| (x::hypreal) \<in> HFinite;
  1164          isLub \<real> {s. s \<in> \<real> & s < x} t;
  1165          r \<in> \<real>; 0 < r |]
  1166       ==> t + -r \<le> x"
  1167 apply (frule isLubD1a)
  1168 apply (rule ccontr, drule linorder_not_le [THEN iffD1])
  1169 apply (drule Reals_minus, drule_tac a = t in Reals_add, assumption)
  1170 apply (drule lemma_st_part_gt_ub, assumption+)
  1171 apply (drule isLub_le_isUb, assumption)
  1172 apply (drule lemma_minus_le_zero)
  1173 apply (auto dest: order_less_le_trans)
  1174 done
  1175 
  1176 lemma lemma_st_part1a:
  1177      "[| (x::hypreal) \<in> HFinite;
  1178          isLub \<real> {s. s \<in> \<real> & s < x} t;
  1179          r \<in> \<real>; 0 < r |]
  1180       ==> x + -t \<le> r"
  1181 apply (subgoal_tac "x \<le> t+r")
  1182 apply (auto intro: lemma_st_part_le1)
  1183 done
  1184 
  1185 lemma lemma_st_part2a:
  1186      "[| (x::hypreal) \<in> HFinite;
  1187          isLub \<real> {s. s \<in> \<real> & s < x} t;
  1188          r \<in> \<real>;  0 < r |]
  1189       ==> -(x + -t) \<le> r"
  1190 apply (subgoal_tac "(t + -r \<le> x)")
  1191 apply simp
  1192 apply (rule lemma_st_part_le2)
  1193 apply auto
  1194 done
  1195 
  1196 lemma lemma_SReal_ub:
  1197      "(x::hypreal) \<in> \<real> ==> isUb \<real> {s. s \<in> \<real> & s < x} x"
  1198 by (auto intro: isUbI setleI order_less_imp_le)
  1199 
  1200 lemma lemma_SReal_lub:
  1201      "(x::hypreal) \<in> \<real> ==> isLub \<real> {s. s \<in> \<real> & s < x} x"
  1202 apply (auto intro!: isLubI2 lemma_SReal_ub setgeI)
  1203 apply (frule isUbD2a)
  1204 apply (rule_tac x = x and y = y in linorder_cases)
  1205 apply (auto intro!: order_less_imp_le)
  1206 apply (drule SReal_dense, assumption, assumption, safe)
  1207 apply (drule_tac y = r in isUbD)
  1208 apply (auto dest: order_less_le_trans)
  1209 done
  1210 
  1211 lemma lemma_st_part_not_eq1:
  1212      "[| (x::hypreal) \<in> HFinite;
  1213          isLub \<real> {s. s \<in> \<real> & s < x} t;
  1214          r \<in> \<real>; 0 < r |]
  1215       ==> x + -t \<noteq> r"
  1216 apply auto
  1217 apply (frule isLubD1a [THEN Reals_minus])
  1218 using Reals_add_cancel [of x "- t"] apply simp
  1219 apply (drule_tac x = x in lemma_SReal_lub)
  1220 apply (drule isLub_unique, assumption, auto)
  1221 done
  1222 
  1223 lemma lemma_st_part_not_eq2:
  1224      "[| (x::hypreal) \<in> HFinite;
  1225          isLub \<real> {s. s \<in> \<real> & s < x} t;
  1226          r \<in> \<real>; 0 < r |]
  1227       ==> -(x + -t) \<noteq> r"
  1228 apply (auto)
  1229 apply (frule isLubD1a)
  1230 using Reals_add_cancel [of "- x" t] apply simp
  1231 apply (drule_tac x = x in lemma_SReal_lub)
  1232 apply (drule isLub_unique, assumption, auto)
  1233 done
  1234 
  1235 lemma lemma_st_part_major:
  1236      "[| (x::hypreal) \<in> HFinite;
  1237          isLub \<real> {s. s \<in> \<real> & s < x} t;
  1238          r \<in> \<real>; 0 < r |]
  1239       ==> \<bar>x - t\<bar> < r"
  1240 apply (frule lemma_st_part1a)
  1241 apply (frule_tac [4] lemma_st_part2a, auto)
  1242 apply (drule order_le_imp_less_or_eq)+
  1243 apply auto
  1244 using lemma_st_part_not_eq2 apply fastforce
  1245 using lemma_st_part_not_eq1 apply fastforce
  1246 done
  1247 
  1248 lemma lemma_st_part_major2:
  1249      "[| (x::hypreal) \<in> HFinite; isLub \<real> {s. s \<in> \<real> & s < x} t |]
  1250       ==> \<forall>r \<in> Reals. 0 < r --> \<bar>x - t\<bar> < r"
  1251 by (blast dest!: lemma_st_part_major)
  1252 
  1253 
  1254 
  1255 text\<open>Existence of real and Standard Part Theorem\<close>
  1256 lemma lemma_st_part_Ex:
  1257      "(x::hypreal) \<in> HFinite
  1258        ==> \<exists>t \<in> Reals. \<forall>r \<in> Reals. 0 < r --> \<bar>x - t\<bar> < r"
  1259 apply (frule lemma_st_part_lub, safe)
  1260 apply (frule isLubD1a)
  1261 apply (blast dest: lemma_st_part_major2)
  1262 done
  1263 
  1264 lemma st_part_Ex:
  1265      "(x::hypreal) \<in> HFinite ==> \<exists>t \<in> Reals. x \<approx> t"
  1266 apply (simp add: approx_def Infinitesimal_def)
  1267 apply (drule lemma_st_part_Ex, auto)
  1268 done
  1269 
  1270 text\<open>There is a unique real infinitely close\<close>
  1271 lemma st_part_Ex1: "x \<in> HFinite ==> \<exists>!t::hypreal. t \<in> \<real> & x \<approx> t"
  1272 apply (drule st_part_Ex, safe)
  1273 apply (drule_tac [2] approx_sym, drule_tac [2] approx_sym, drule_tac [2] approx_sym)
  1274 apply (auto intro!: approx_unique_real)
  1275 done
  1276 
  1277 subsection\<open>Finite, Infinite and Infinitesimal\<close>
  1278 
  1279 lemma HFinite_Int_HInfinite_empty [simp]: "HFinite Int HInfinite = {}"
  1280 apply (simp add: HFinite_def HInfinite_def)
  1281 apply (auto dest: order_less_trans)
  1282 done
  1283 
  1284 lemma HFinite_not_HInfinite:
  1285   assumes x: "x \<in> HFinite" shows "x \<notin> HInfinite"
  1286 proof
  1287   assume x': "x \<in> HInfinite"
  1288   with x have "x \<in> HFinite \<inter> HInfinite" by blast
  1289   thus False by auto
  1290 qed
  1291 
  1292 lemma not_HFinite_HInfinite: "x\<notin> HFinite ==> x \<in> HInfinite"
  1293 apply (simp add: HInfinite_def HFinite_def, auto)
  1294 apply (drule_tac x = "r + 1" in bspec)
  1295 apply (auto)
  1296 done
  1297 
  1298 lemma HInfinite_HFinite_disj: "x \<in> HInfinite | x \<in> HFinite"
  1299 by (blast intro: not_HFinite_HInfinite)
  1300 
  1301 lemma HInfinite_HFinite_iff: "(x \<in> HInfinite) = (x \<notin> HFinite)"
  1302 by (blast dest: HFinite_not_HInfinite not_HFinite_HInfinite)
  1303 
  1304 lemma HFinite_HInfinite_iff: "(x \<in> HFinite) = (x \<notin> HInfinite)"
  1305 by (simp add: HInfinite_HFinite_iff)
  1306 
  1307 
  1308 lemma HInfinite_diff_HFinite_Infinitesimal_disj:
  1309      "x \<notin> Infinitesimal ==> x \<in> HInfinite | x \<in> HFinite - Infinitesimal"
  1310 by (fast intro: not_HFinite_HInfinite)
  1311 
  1312 lemma HFinite_inverse:
  1313   fixes x :: "'a::real_normed_div_algebra star"
  1314   shows "[| x \<in> HFinite; x \<notin> Infinitesimal |] ==> inverse x \<in> HFinite"
  1315 apply (subgoal_tac "x \<noteq> 0")
  1316 apply (cut_tac x = "inverse x" in HInfinite_HFinite_disj)
  1317 apply (auto dest!: HInfinite_inverse_Infinitesimal
  1318             simp add: nonzero_inverse_inverse_eq)
  1319 done
  1320 
  1321 lemma HFinite_inverse2:
  1322   fixes x :: "'a::real_normed_div_algebra star"
  1323   shows "x \<in> HFinite - Infinitesimal ==> inverse x \<in> HFinite"
  1324 by (blast intro: HFinite_inverse)
  1325 
  1326 (* stronger statement possible in fact *)
  1327 lemma Infinitesimal_inverse_HFinite:
  1328   fixes x :: "'a::real_normed_div_algebra star"
  1329   shows "x \<notin> Infinitesimal ==> inverse(x) \<in> HFinite"
  1330 apply (drule HInfinite_diff_HFinite_Infinitesimal_disj)
  1331 apply (blast intro: HFinite_inverse HInfinite_inverse_Infinitesimal Infinitesimal_subset_HFinite [THEN subsetD])
  1332 done
  1333 
  1334 lemma HFinite_not_Infinitesimal_inverse:
  1335   fixes x :: "'a::real_normed_div_algebra star"
  1336   shows "x \<in> HFinite - Infinitesimal ==> inverse x \<in> HFinite - Infinitesimal"
  1337 apply (auto intro: Infinitesimal_inverse_HFinite)
  1338 apply (drule Infinitesimal_HFinite_mult2, assumption)
  1339 apply (simp add: not_Infinitesimal_not_zero)
  1340 done
  1341 
  1342 lemma approx_inverse:
  1343   fixes x y :: "'a::real_normed_div_algebra star"
  1344   shows
  1345      "[| x \<approx> y; y \<in>  HFinite - Infinitesimal |]
  1346       ==> inverse x \<approx> inverse y"
  1347 apply (frule HFinite_diff_Infinitesimal_approx, assumption)
  1348 apply (frule not_Infinitesimal_not_zero2)
  1349 apply (frule_tac x = x in not_Infinitesimal_not_zero2)
  1350 apply (drule HFinite_inverse2)+
  1351 apply (drule approx_mult2, assumption, auto)
  1352 apply (drule_tac c = "inverse x" in approx_mult1, assumption)
  1353 apply (auto intro: approx_sym simp add: mult.assoc)
  1354 done
  1355 
  1356 (*Used for NSLIM_inverse, NSLIMSEQ_inverse*)
  1357 lemmas star_of_approx_inverse = star_of_HFinite_diff_Infinitesimal [THEN [2] approx_inverse]
  1358 lemmas hypreal_of_real_approx_inverse =  hypreal_of_real_HFinite_diff_Infinitesimal [THEN [2] approx_inverse]
  1359 
  1360 lemma inverse_add_Infinitesimal_approx:
  1361   fixes x h :: "'a::real_normed_div_algebra star"
  1362   shows
  1363      "[| x \<in> HFinite - Infinitesimal;
  1364          h \<in> Infinitesimal |] ==> inverse(x + h) \<approx> inverse x"
  1365 apply (auto intro: approx_inverse approx_sym Infinitesimal_add_approx_self)
  1366 done
  1367 
  1368 lemma inverse_add_Infinitesimal_approx2:
  1369   fixes x h :: "'a::real_normed_div_algebra star"
  1370   shows
  1371      "[| x \<in> HFinite - Infinitesimal;
  1372          h \<in> Infinitesimal |] ==> inverse(h + x) \<approx> inverse x"
  1373 apply (rule add.commute [THEN subst])
  1374 apply (blast intro: inverse_add_Infinitesimal_approx)
  1375 done
  1376 
  1377 lemma inverse_add_Infinitesimal_approx_Infinitesimal:
  1378   fixes x h :: "'a::real_normed_div_algebra star"
  1379   shows
  1380      "[| x \<in> HFinite - Infinitesimal;
  1381          h \<in> Infinitesimal |] ==> inverse(x + h) - inverse x \<approx> h"
  1382 apply (rule approx_trans2)
  1383 apply (auto intro: inverse_add_Infinitesimal_approx
  1384             simp add: mem_infmal_iff approx_minus_iff [symmetric])
  1385 done
  1386 
  1387 lemma Infinitesimal_square_iff:
  1388   fixes x :: "'a::real_normed_div_algebra star"
  1389   shows "(x \<in> Infinitesimal) = (x*x \<in> Infinitesimal)"
  1390 apply (auto intro: Infinitesimal_mult)
  1391 apply (rule ccontr, frule Infinitesimal_inverse_HFinite)
  1392 apply (frule not_Infinitesimal_not_zero)
  1393 apply (auto dest: Infinitesimal_HFinite_mult simp add: mult.assoc)
  1394 done
  1395 declare Infinitesimal_square_iff [symmetric, simp]
  1396 
  1397 lemma HFinite_square_iff [simp]:
  1398   fixes x :: "'a::real_normed_div_algebra star"
  1399   shows "(x*x \<in> HFinite) = (x \<in> HFinite)"
  1400 apply (auto intro: HFinite_mult)
  1401 apply (auto dest: HInfinite_mult simp add: HFinite_HInfinite_iff)
  1402 done
  1403 
  1404 lemma HInfinite_square_iff [simp]:
  1405   fixes x :: "'a::real_normed_div_algebra star"
  1406   shows "(x*x \<in> HInfinite) = (x \<in> HInfinite)"
  1407 by (auto simp add: HInfinite_HFinite_iff)
  1408 
  1409 lemma approx_HFinite_mult_cancel:
  1410   fixes a w z :: "'a::real_normed_div_algebra star"
  1411   shows "[| a: HFinite-Infinitesimal; a* w \<approx> a*z |] ==> w \<approx> z"
  1412 apply safe
  1413 apply (frule HFinite_inverse, assumption)
  1414 apply (drule not_Infinitesimal_not_zero)
  1415 apply (auto dest: approx_mult2 simp add: mult.assoc [symmetric])
  1416 done
  1417 
  1418 lemma approx_HFinite_mult_cancel_iff1:
  1419   fixes a w z :: "'a::real_normed_div_algebra star"
  1420   shows "a: HFinite-Infinitesimal ==> (a * w \<approx> a * z) = (w \<approx> z)"
  1421 by (auto intro: approx_mult2 approx_HFinite_mult_cancel)
  1422 
  1423 lemma HInfinite_HFinite_add_cancel:
  1424      "[| x + y \<in> HInfinite; y \<in> HFinite |] ==> x \<in> HInfinite"
  1425 apply (rule ccontr)
  1426 apply (drule HFinite_HInfinite_iff [THEN iffD2])
  1427 apply (auto dest: HFinite_add simp add: HInfinite_HFinite_iff)
  1428 done
  1429 
  1430 lemma HInfinite_HFinite_add:
  1431      "[| x \<in> HInfinite; y \<in> HFinite |] ==> x + y \<in> HInfinite"
  1432 apply (rule_tac y = "-y" in HInfinite_HFinite_add_cancel)
  1433 apply (auto simp add: add.assoc HFinite_minus_iff)
  1434 done
  1435 
  1436 lemma HInfinite_ge_HInfinite:
  1437      "[| (x::hypreal) \<in> HInfinite; x \<le> y; 0 \<le> x |] ==> y \<in> HInfinite"
  1438 by (auto intro: HFinite_bounded simp add: HInfinite_HFinite_iff)
  1439 
  1440 lemma Infinitesimal_inverse_HInfinite:
  1441   fixes x :: "'a::real_normed_div_algebra star"
  1442   shows "[| x \<in> Infinitesimal; x \<noteq> 0 |] ==> inverse x \<in> HInfinite"
  1443 apply (rule ccontr, drule HFinite_HInfinite_iff [THEN iffD2])
  1444 apply (auto dest: Infinitesimal_HFinite_mult2)
  1445 done
  1446 
  1447 lemma HInfinite_HFinite_not_Infinitesimal_mult:
  1448   fixes x y :: "'a::real_normed_div_algebra star"
  1449   shows "[| x \<in> HInfinite; y \<in> HFinite - Infinitesimal |]
  1450       ==> x * y \<in> HInfinite"
  1451 apply (rule ccontr, drule HFinite_HInfinite_iff [THEN iffD2])
  1452 apply (frule HFinite_Infinitesimal_not_zero)
  1453 apply (drule HFinite_not_Infinitesimal_inverse)
  1454 apply (safe, drule HFinite_mult)
  1455 apply (auto simp add: mult.assoc HFinite_HInfinite_iff)
  1456 done
  1457 
  1458 lemma HInfinite_HFinite_not_Infinitesimal_mult2:
  1459   fixes x y :: "'a::real_normed_div_algebra star"
  1460   shows "[| x \<in> HInfinite; y \<in> HFinite - Infinitesimal |]
  1461       ==> y * x \<in> HInfinite"
  1462 apply (rule ccontr, drule HFinite_HInfinite_iff [THEN iffD2])
  1463 apply (frule HFinite_Infinitesimal_not_zero)
  1464 apply (drule HFinite_not_Infinitesimal_inverse)
  1465 apply (safe, drule_tac x="inverse y" in HFinite_mult)
  1466 apply assumption
  1467 apply (auto simp add: mult.assoc [symmetric] HFinite_HInfinite_iff)
  1468 done
  1469 
  1470 lemma HInfinite_gt_SReal:
  1471   "[| (x::hypreal) \<in> HInfinite; 0 < x; y \<in> \<real> |] ==> y < x"
  1472 by (auto dest!: bspec simp add: HInfinite_def abs_if order_less_imp_le)
  1473 
  1474 lemma HInfinite_gt_zero_gt_one:
  1475   "[| (x::hypreal) \<in> HInfinite; 0 < x |] ==> 1 < x"
  1476 by (auto intro: HInfinite_gt_SReal)
  1477 
  1478 
  1479 lemma not_HInfinite_one [simp]: "1 \<notin> HInfinite"
  1480 apply (simp (no_asm) add: HInfinite_HFinite_iff)
  1481 done
  1482 
  1483 lemma approx_hrabs_disj: "\<bar>x::hypreal\<bar> \<approx> x \<or> \<bar>x\<bar> \<approx> -x"
  1484 by (cut_tac x = x in hrabs_disj, auto)
  1485 
  1486 
  1487 subsection\<open>Theorems about Monads\<close>
  1488 
  1489 lemma monad_hrabs_Un_subset: "monad \<bar>x\<bar> \<le> monad(x::hypreal) Un monad(-x)"
  1490 by (rule_tac x1 = x in hrabs_disj [THEN disjE], auto)
  1491 
  1492 lemma Infinitesimal_monad_eq: "e \<in> Infinitesimal ==> monad (x+e) = monad x"
  1493 by (fast intro!: Infinitesimal_add_approx_self [THEN approx_sym] approx_monad_iff [THEN iffD1])
  1494 
  1495 lemma mem_monad_iff: "(u \<in> monad x) = (-u \<in> monad (-x))"
  1496 by (simp add: monad_def)
  1497 
  1498 lemma Infinitesimal_monad_zero_iff: "(x \<in> Infinitesimal) = (x \<in> monad 0)"
  1499 by (auto intro: approx_sym simp add: monad_def mem_infmal_iff)
  1500 
  1501 lemma monad_zero_minus_iff: "(x \<in> monad 0) = (-x \<in> monad 0)"
  1502 apply (simp (no_asm) add: Infinitesimal_monad_zero_iff [symmetric])
  1503 done
  1504 
  1505 lemma monad_zero_hrabs_iff: "((x::hypreal) \<in> monad 0) = (\<bar>x\<bar> \<in> monad 0)"
  1506 apply (rule_tac x1 = x in hrabs_disj [THEN disjE])
  1507 apply (auto simp add: monad_zero_minus_iff [symmetric])
  1508 done
  1509 
  1510 lemma mem_monad_self [simp]: "x \<in> monad x"
  1511 by (simp add: monad_def)
  1512 
  1513 
  1514 subsection\<open>Proof that @{term "x \<approx> y"} implies @{term"\<bar>x\<bar> \<approx> \<bar>y\<bar>"}\<close>
  1515 
  1516 lemma approx_subset_monad: "x \<approx> y ==> {x,y} \<le> monad x"
  1517 apply (simp (no_asm))
  1518 apply (simp add: approx_monad_iff)
  1519 done
  1520 
  1521 lemma approx_subset_monad2: "x \<approx> y ==> {x,y} \<le> monad y"
  1522 apply (drule approx_sym)
  1523 apply (fast dest: approx_subset_monad)
  1524 done
  1525 
  1526 lemma mem_monad_approx: "u \<in> monad x ==> x \<approx> u"
  1527 by (simp add: monad_def)
  1528 
  1529 lemma approx_mem_monad: "x \<approx> u ==> u \<in> monad x"
  1530 by (simp add: monad_def)
  1531 
  1532 lemma approx_mem_monad2: "x \<approx> u ==> x \<in> monad u"
  1533 apply (simp add: monad_def)
  1534 apply (blast intro!: approx_sym)
  1535 done
  1536 
  1537 lemma approx_mem_monad_zero: "[| x \<approx> y;x \<in> monad 0 |] ==> y \<in> monad 0"
  1538 apply (drule mem_monad_approx)
  1539 apply (fast intro: approx_mem_monad approx_trans)
  1540 done
  1541 
  1542 lemma Infinitesimal_approx_hrabs:
  1543      "[| x \<approx> y; (x::hypreal) \<in> Infinitesimal |] ==> \<bar>x\<bar> \<approx> \<bar>y\<bar>"
  1544 apply (drule Infinitesimal_monad_zero_iff [THEN iffD1])
  1545 apply (blast intro: approx_mem_monad_zero monad_zero_hrabs_iff [THEN iffD1] mem_monad_approx approx_trans3)
  1546 done
  1547 
  1548 lemma less_Infinitesimal_less:
  1549      "[| 0 < x;  (x::hypreal) \<notin>Infinitesimal;  e :Infinitesimal |] ==> e < x"
  1550 apply (rule ccontr)
  1551 apply (auto intro: Infinitesimal_zero [THEN [2] Infinitesimal_interval]
  1552             dest!: order_le_imp_less_or_eq simp add: linorder_not_less)
  1553 done
  1554 
  1555 lemma Ball_mem_monad_gt_zero:
  1556      "[| 0 < (x::hypreal);  x \<notin> Infinitesimal; u \<in> monad x |] ==> 0 < u"
  1557 apply (drule mem_monad_approx [THEN approx_sym])
  1558 apply (erule bex_Infinitesimal_iff2 [THEN iffD2, THEN bexE])
  1559 apply (drule_tac e = "-xa" in less_Infinitesimal_less, auto)
  1560 done
  1561 
  1562 lemma Ball_mem_monad_less_zero:
  1563      "[| (x::hypreal) < 0; x \<notin> Infinitesimal; u \<in> monad x |] ==> u < 0"
  1564 apply (drule mem_monad_approx [THEN approx_sym])
  1565 apply (erule bex_Infinitesimal_iff [THEN iffD2, THEN bexE])
  1566 apply (cut_tac x = "-x" and e = xa in less_Infinitesimal_less, auto)
  1567 done
  1568 
  1569 lemma lemma_approx_gt_zero:
  1570      "[|0 < (x::hypreal); x \<notin> Infinitesimal; x \<approx> y|] ==> 0 < y"
  1571 by (blast dest: Ball_mem_monad_gt_zero approx_subset_monad)
  1572 
  1573 lemma lemma_approx_less_zero:
  1574      "[|(x::hypreal) < 0; x \<notin> Infinitesimal; x \<approx> y|] ==> y < 0"
  1575 by (blast dest: Ball_mem_monad_less_zero approx_subset_monad)
  1576 
  1577 theorem approx_hrabs: "(x::hypreal) \<approx> y ==> \<bar>x\<bar> \<approx> \<bar>y\<bar>"
  1578 by (drule approx_hnorm, simp)
  1579 
  1580 lemma approx_hrabs_zero_cancel: "\<bar>x::hypreal\<bar> \<approx> 0 ==> x \<approx> 0"
  1581 apply (cut_tac x = x in hrabs_disj)
  1582 apply (auto dest: approx_minus)
  1583 done
  1584 
  1585 lemma approx_hrabs_add_Infinitesimal:
  1586   "(e::hypreal) \<in> Infinitesimal ==> \<bar>x\<bar> \<approx> \<bar>x + e\<bar>"
  1587 by (fast intro: approx_hrabs Infinitesimal_add_approx_self)
  1588 
  1589 lemma approx_hrabs_add_minus_Infinitesimal:
  1590      "(e::hypreal) \<in> Infinitesimal ==> \<bar>x\<bar> \<approx> \<bar>x + -e\<bar>"
  1591 by (fast intro: approx_hrabs Infinitesimal_add_minus_approx_self)
  1592 
  1593 lemma hrabs_add_Infinitesimal_cancel:
  1594      "[| (e::hypreal) \<in> Infinitesimal; e' \<in> Infinitesimal;
  1595          \<bar>x + e\<bar> = \<bar>y + e'\<bar>|] ==> \<bar>x\<bar> \<approx> \<bar>y\<bar>"
  1596 apply (drule_tac x = x in approx_hrabs_add_Infinitesimal)
  1597 apply (drule_tac x = y in approx_hrabs_add_Infinitesimal)
  1598 apply (auto intro: approx_trans2)
  1599 done
  1600 
  1601 lemma hrabs_add_minus_Infinitesimal_cancel:
  1602      "[| (e::hypreal) \<in> Infinitesimal; e' \<in> Infinitesimal;
  1603          \<bar>x + -e\<bar> = \<bar>y + -e'\<bar>|] ==> \<bar>x\<bar> \<approx> \<bar>y\<bar>"
  1604 apply (drule_tac x = x in approx_hrabs_add_minus_Infinitesimal)
  1605 apply (drule_tac x = y in approx_hrabs_add_minus_Infinitesimal)
  1606 apply (auto intro: approx_trans2)
  1607 done
  1608 
  1609 subsection \<open>More @{term HFinite} and @{term Infinitesimal} Theorems\<close>
  1610 
  1611 (* interesting slightly counterintuitive theorem: necessary
  1612    for proving that an open interval is an NS open set
  1613 *)
  1614 lemma Infinitesimal_add_hypreal_of_real_less:
  1615      "[| x < y;  u \<in> Infinitesimal |]
  1616       ==> hypreal_of_real x + u < hypreal_of_real y"
  1617 apply (simp add: Infinitesimal_def)
  1618 apply (drule_tac x = "hypreal_of_real y + -hypreal_of_real x" in bspec, simp)
  1619 apply (simp add: abs_less_iff)
  1620 done
  1621 
  1622 lemma Infinitesimal_add_hrabs_hypreal_of_real_less:
  1623      "[| x \<in> Infinitesimal; \<bar>hypreal_of_real r\<bar> < hypreal_of_real y |]
  1624       ==> \<bar>hypreal_of_real r + x\<bar> < hypreal_of_real y"
  1625 apply (drule_tac x = "hypreal_of_real r" in approx_hrabs_add_Infinitesimal)
  1626 apply (drule approx_sym [THEN bex_Infinitesimal_iff2 [THEN iffD2]])
  1627 apply (auto intro!: Infinitesimal_add_hypreal_of_real_less
  1628             simp del: star_of_abs
  1629             simp add: star_of_abs [symmetric])
  1630 done
  1631 
  1632 lemma Infinitesimal_add_hrabs_hypreal_of_real_less2:
  1633      "[| x \<in> Infinitesimal;  \<bar>hypreal_of_real r\<bar> < hypreal_of_real y |]
  1634       ==> \<bar>x + hypreal_of_real r\<bar> < hypreal_of_real y"
  1635 apply (rule add.commute [THEN subst])
  1636 apply (erule Infinitesimal_add_hrabs_hypreal_of_real_less, assumption)
  1637 done
  1638 
  1639 lemma hypreal_of_real_le_add_Infininitesimal_cancel:
  1640      "[| u \<in> Infinitesimal; v \<in> Infinitesimal;
  1641          hypreal_of_real x + u \<le> hypreal_of_real y + v |]
  1642       ==> hypreal_of_real x \<le> hypreal_of_real y"
  1643 apply (simp add: linorder_not_less [symmetric], auto)
  1644 apply (drule_tac u = "v-u" in Infinitesimal_add_hypreal_of_real_less)
  1645 apply (auto simp add: Infinitesimal_diff)
  1646 done
  1647 
  1648 lemma hypreal_of_real_le_add_Infininitesimal_cancel2:
  1649      "[| u \<in> Infinitesimal; v \<in> Infinitesimal;
  1650          hypreal_of_real x + u \<le> hypreal_of_real y + v |]
  1651       ==> x \<le> y"
  1652 by (blast intro: star_of_le [THEN iffD1]
  1653           intro!: hypreal_of_real_le_add_Infininitesimal_cancel)
  1654 
  1655 lemma hypreal_of_real_less_Infinitesimal_le_zero:
  1656     "[| hypreal_of_real x < e; e \<in> Infinitesimal |] ==> hypreal_of_real x \<le> 0"
  1657 apply (rule linorder_not_less [THEN iffD1], safe)
  1658 apply (drule Infinitesimal_interval)
  1659 apply (drule_tac [4] SReal_hypreal_of_real [THEN SReal_Infinitesimal_zero], auto)
  1660 done
  1661 
  1662 (*used once, in Lim/NSDERIV_inverse*)
  1663 lemma Infinitesimal_add_not_zero:
  1664      "[| h \<in> Infinitesimal; x \<noteq> 0 |] ==> star_of x + h \<noteq> 0"
  1665 apply auto
  1666 apply (subgoal_tac "h = - star_of x", auto intro: minus_unique [symmetric])
  1667 done
  1668 
  1669 lemma Infinitesimal_square_cancel [simp]:
  1670      "(x::hypreal)*x + y*y \<in> Infinitesimal ==> x*x \<in> Infinitesimal"
  1671 apply (rule Infinitesimal_interval2)
  1672 apply (rule_tac [3] zero_le_square, assumption)
  1673 apply (auto)
  1674 done
  1675 
  1676 lemma HFinite_square_cancel [simp]:
  1677   "(x::hypreal)*x + y*y \<in> HFinite ==> x*x \<in> HFinite"
  1678 apply (rule HFinite_bounded, assumption)
  1679 apply (auto)
  1680 done
  1681 
  1682 lemma Infinitesimal_square_cancel2 [simp]:
  1683      "(x::hypreal)*x + y*y \<in> Infinitesimal ==> y*y \<in> Infinitesimal"
  1684 apply (rule Infinitesimal_square_cancel)
  1685 apply (rule add.commute [THEN subst])
  1686 apply (simp (no_asm))
  1687 done
  1688 
  1689 lemma HFinite_square_cancel2 [simp]:
  1690   "(x::hypreal)*x + y*y \<in> HFinite ==> y*y \<in> HFinite"
  1691 apply (rule HFinite_square_cancel)
  1692 apply (rule add.commute [THEN subst])
  1693 apply (simp (no_asm))
  1694 done
  1695 
  1696 lemma Infinitesimal_sum_square_cancel [simp]:
  1697      "(x::hypreal)*x + y*y + z*z \<in> Infinitesimal ==> x*x \<in> Infinitesimal"
  1698 apply (rule Infinitesimal_interval2, assumption)
  1699 apply (rule_tac [2] zero_le_square, simp)
  1700 apply (insert zero_le_square [of y])
  1701 apply (insert zero_le_square [of z], simp del:zero_le_square)
  1702 done
  1703 
  1704 lemma HFinite_sum_square_cancel [simp]:
  1705      "(x::hypreal)*x + y*y + z*z \<in> HFinite ==> x*x \<in> HFinite"
  1706 apply (rule HFinite_bounded, assumption)
  1707 apply (rule_tac [2] zero_le_square)
  1708 apply (insert zero_le_square [of y])
  1709 apply (insert zero_le_square [of z], simp del:zero_le_square)
  1710 done
  1711 
  1712 lemma Infinitesimal_sum_square_cancel2 [simp]:
  1713      "(y::hypreal)*y + x*x + z*z \<in> Infinitesimal ==> x*x \<in> Infinitesimal"
  1714 apply (rule Infinitesimal_sum_square_cancel)
  1715 apply (simp add: ac_simps)
  1716 done
  1717 
  1718 lemma HFinite_sum_square_cancel2 [simp]:
  1719      "(y::hypreal)*y + x*x + z*z \<in> HFinite ==> x*x \<in> HFinite"
  1720 apply (rule HFinite_sum_square_cancel)
  1721 apply (simp add: ac_simps)
  1722 done
  1723 
  1724 lemma Infinitesimal_sum_square_cancel3 [simp]:
  1725      "(z::hypreal)*z + y*y + x*x \<in> Infinitesimal ==> x*x \<in> Infinitesimal"
  1726 apply (rule Infinitesimal_sum_square_cancel)
  1727 apply (simp add: ac_simps)
  1728 done
  1729 
  1730 lemma HFinite_sum_square_cancel3 [simp]:
  1731      "(z::hypreal)*z + y*y + x*x \<in> HFinite ==> x*x \<in> HFinite"
  1732 apply (rule HFinite_sum_square_cancel)
  1733 apply (simp add: ac_simps)
  1734 done
  1735 
  1736 lemma monad_hrabs_less:
  1737      "[| y \<in> monad x; 0 < hypreal_of_real e |]
  1738       ==> \<bar>y - x\<bar> < hypreal_of_real e"
  1739 apply (drule mem_monad_approx [THEN approx_sym])
  1740 apply (drule bex_Infinitesimal_iff [THEN iffD2])
  1741 apply (auto dest!: InfinitesimalD)
  1742 done
  1743 
  1744 lemma mem_monad_SReal_HFinite:
  1745      "x \<in> monad (hypreal_of_real  a) ==> x \<in> HFinite"
  1746 apply (drule mem_monad_approx [THEN approx_sym])
  1747 apply (drule bex_Infinitesimal_iff2 [THEN iffD2])
  1748 apply (safe dest!: Infinitesimal_subset_HFinite [THEN subsetD])
  1749 apply (erule SReal_hypreal_of_real [THEN SReal_subset_HFinite [THEN subsetD], THEN HFinite_add])
  1750 done
  1751 
  1752 
  1753 subsection\<open>Theorems about Standard Part\<close>
  1754 
  1755 lemma st_approx_self: "x \<in> HFinite ==> st x \<approx> x"
  1756 apply (simp add: st_def)
  1757 apply (frule st_part_Ex, safe)
  1758 apply (rule someI2)
  1759 apply (auto intro: approx_sym)
  1760 done
  1761 
  1762 lemma st_SReal: "x \<in> HFinite ==> st x \<in> \<real>"
  1763 apply (simp add: st_def)
  1764 apply (frule st_part_Ex, safe)
  1765 apply (rule someI2)
  1766 apply (auto intro: approx_sym)
  1767 done
  1768 
  1769 lemma st_HFinite: "x \<in> HFinite ==> st x \<in> HFinite"
  1770 by (erule st_SReal [THEN SReal_subset_HFinite [THEN subsetD]])
  1771 
  1772 lemma st_unique: "\<lbrakk>r \<in> \<real>; r \<approx> x\<rbrakk> \<Longrightarrow> st x = r"
  1773 apply (frule SReal_subset_HFinite [THEN subsetD])
  1774 apply (drule (1) approx_HFinite)
  1775 apply (unfold st_def)
  1776 apply (rule some_equality)
  1777 apply (auto intro: approx_unique_real)
  1778 done
  1779 
  1780 lemma st_SReal_eq: "x \<in> \<real> ==> st x = x"
  1781   by (metis approx_refl st_unique)
  1782 
  1783 lemma st_hypreal_of_real [simp]: "st (hypreal_of_real x) = hypreal_of_real x"
  1784 by (rule SReal_hypreal_of_real [THEN st_SReal_eq])
  1785 
  1786 lemma st_eq_approx: "[| x \<in> HFinite; y \<in> HFinite; st x = st y |] ==> x \<approx> y"
  1787 by (auto dest!: st_approx_self elim!: approx_trans3)
  1788 
  1789 lemma approx_st_eq:
  1790   assumes x: "x \<in> HFinite" and y: "y \<in> HFinite" and xy: "x \<approx> y"
  1791   shows "st x = st y"
  1792 proof -
  1793   have "st x \<approx> x" "st y \<approx> y" "st x \<in> \<real>" "st y \<in> \<real>"
  1794     by (simp_all add: st_approx_self st_SReal x y)
  1795   with xy show ?thesis
  1796     by (fast elim: approx_trans approx_trans2 SReal_approx_iff [THEN iffD1])
  1797 qed
  1798 
  1799 lemma st_eq_approx_iff:
  1800      "[| x \<in> HFinite; y \<in> HFinite|]
  1801                    ==> (x \<approx> y) = (st x = st y)"
  1802 by (blast intro: approx_st_eq st_eq_approx)
  1803 
  1804 lemma st_Infinitesimal_add_SReal:
  1805      "[| x \<in> \<real>; e \<in> Infinitesimal |] ==> st(x + e) = x"
  1806 apply (erule st_unique)
  1807 apply (erule Infinitesimal_add_approx_self)
  1808 done
  1809 
  1810 lemma st_Infinitesimal_add_SReal2:
  1811      "[| x \<in> \<real>; e \<in> Infinitesimal |] ==> st(e + x) = x"
  1812 apply (erule st_unique)
  1813 apply (erule Infinitesimal_add_approx_self2)
  1814 done
  1815 
  1816 lemma HFinite_st_Infinitesimal_add:
  1817      "x \<in> HFinite ==> \<exists>e \<in> Infinitesimal. x = st(x) + e"
  1818 by (blast dest!: st_approx_self [THEN approx_sym] bex_Infinitesimal_iff2 [THEN iffD2])
  1819 
  1820 lemma st_add: "\<lbrakk>x \<in> HFinite; y \<in> HFinite\<rbrakk> \<Longrightarrow> st (x + y) = st x + st y"
  1821 by (simp add: st_unique st_SReal st_approx_self approx_add)
  1822 
  1823 lemma st_numeral [simp]: "st (numeral w) = numeral w"
  1824 by (rule Reals_numeral [THEN st_SReal_eq])
  1825 
  1826 lemma st_neg_numeral [simp]: "st (- numeral w) = - numeral w"
  1827 proof -
  1828   from Reals_numeral have "numeral w \<in> \<real>" .
  1829   then have "- numeral w \<in> \<real>" by simp
  1830   with st_SReal_eq show ?thesis .
  1831 qed
  1832 
  1833 lemma st_0 [simp]: "st 0 = 0"
  1834 by (simp add: st_SReal_eq)
  1835 
  1836 lemma st_1 [simp]: "st 1 = 1"
  1837 by (simp add: st_SReal_eq)
  1838 
  1839 lemma st_neg_1 [simp]: "st (- 1) = - 1"
  1840 by (simp add: st_SReal_eq)
  1841 
  1842 lemma st_minus: "x \<in> HFinite \<Longrightarrow> st (- x) = - st x"
  1843 by (simp add: st_unique st_SReal st_approx_self approx_minus)
  1844 
  1845 lemma st_diff: "\<lbrakk>x \<in> HFinite; y \<in> HFinite\<rbrakk> \<Longrightarrow> st (x - y) = st x - st y"
  1846 by (simp add: st_unique st_SReal st_approx_self approx_diff)
  1847 
  1848 lemma st_mult: "\<lbrakk>x \<in> HFinite; y \<in> HFinite\<rbrakk> \<Longrightarrow> st (x * y) = st x * st y"
  1849 by (simp add: st_unique st_SReal st_approx_self approx_mult_HFinite)
  1850 
  1851 lemma st_Infinitesimal: "x \<in> Infinitesimal ==> st x = 0"
  1852 by (simp add: st_unique mem_infmal_iff)
  1853 
  1854 lemma st_not_Infinitesimal: "st(x) \<noteq> 0 ==> x \<notin> Infinitesimal"
  1855 by (fast intro: st_Infinitesimal)
  1856 
  1857 lemma st_inverse:
  1858      "[| x \<in> HFinite; st x \<noteq> 0 |]
  1859       ==> st(inverse x) = inverse (st x)"
  1860 apply (rule_tac c1 = "st x" in mult_left_cancel [THEN iffD1])
  1861 apply (auto simp add: st_mult [symmetric] st_not_Infinitesimal HFinite_inverse)
  1862 apply (subst right_inverse, auto)
  1863 done
  1864 
  1865 lemma st_divide [simp]:
  1866      "[| x \<in> HFinite; y \<in> HFinite; st y \<noteq> 0 |]
  1867       ==> st(x/y) = (st x) / (st y)"
  1868 by (simp add: divide_inverse st_mult st_not_Infinitesimal HFinite_inverse st_inverse)
  1869 
  1870 lemma st_idempotent [simp]: "x \<in> HFinite ==> st(st(x)) = st(x)"
  1871 by (blast intro: st_HFinite st_approx_self approx_st_eq)
  1872 
  1873 lemma Infinitesimal_add_st_less:
  1874      "[| x \<in> HFinite; y \<in> HFinite; u \<in> Infinitesimal; st x < st y |]
  1875       ==> st x + u < st y"
  1876 apply (drule st_SReal)+
  1877 apply (auto intro!: Infinitesimal_add_hypreal_of_real_less simp add: SReal_iff)
  1878 done
  1879 
  1880 lemma Infinitesimal_add_st_le_cancel:
  1881      "[| x \<in> HFinite; y \<in> HFinite;
  1882          u \<in> Infinitesimal; st x \<le> st y + u
  1883       |] ==> st x \<le> st y"
  1884 apply (simp add: linorder_not_less [symmetric])
  1885 apply (auto dest: Infinitesimal_add_st_less)
  1886 done
  1887 
  1888 lemma st_le: "[| x \<in> HFinite; y \<in> HFinite; x \<le> y |] ==> st(x) \<le> st(y)"
  1889 by (metis approx_le_bound approx_sym linear st_SReal st_approx_self st_part_Ex1)
  1890 
  1891 lemma st_zero_le: "[| 0 \<le> x;  x \<in> HFinite |] ==> 0 \<le> st x"
  1892 apply (subst st_0 [symmetric])
  1893 apply (rule st_le, auto)
  1894 done
  1895 
  1896 lemma st_zero_ge: "[| x \<le> 0;  x \<in> HFinite |] ==> st x \<le> 0"
  1897 apply (subst st_0 [symmetric])
  1898 apply (rule st_le, auto)
  1899 done
  1900 
  1901 lemma st_hrabs: "x \<in> HFinite ==> \<bar>st x\<bar> = st \<bar>x\<bar>"
  1902 apply (simp add: linorder_not_le st_zero_le abs_if st_minus
  1903    linorder_not_less)
  1904 apply (auto dest!: st_zero_ge [OF order_less_imp_le])
  1905 done
  1906 
  1907 
  1908 
  1909 subsection \<open>Alternative Definitions using Free Ultrafilter\<close>
  1910 
  1911 subsubsection \<open>@{term HFinite}\<close>
  1912 
  1913 lemma HFinite_FreeUltrafilterNat:
  1914     "star_n X \<in> HFinite
  1915    ==> \<exists>u. eventually (\<lambda>n. norm (X n) < u) FreeUltrafilterNat"
  1916 apply (auto simp add: HFinite_def SReal_def)
  1917 apply (rule_tac x=r in exI)
  1918 apply (simp add: hnorm_def star_of_def starfun_star_n)
  1919 apply (simp add: star_less_def starP2_star_n)
  1920 done
  1921 
  1922 lemma FreeUltrafilterNat_HFinite:
  1923      "\<exists>u. eventually (\<lambda>n. norm (X n) < u) FreeUltrafilterNat
  1924        ==>  star_n X \<in> HFinite"
  1925 apply (auto simp add: HFinite_def mem_Rep_star_iff)
  1926 apply (rule_tac x="star_of u" in bexI)
  1927 apply (simp add: hnorm_def starfun_star_n star_of_def)
  1928 apply (simp add: star_less_def starP2_star_n)
  1929 apply (simp add: SReal_def)
  1930 done
  1931 
  1932 lemma HFinite_FreeUltrafilterNat_iff:
  1933      "(star_n X \<in> HFinite) = (\<exists>u. eventually (\<lambda>n. norm (X n) < u) FreeUltrafilterNat)"
  1934 by (blast intro!: HFinite_FreeUltrafilterNat FreeUltrafilterNat_HFinite)
  1935 
  1936 subsubsection \<open>@{term HInfinite}\<close>
  1937 
  1938 lemma lemma_Compl_eq: "- {n. u < norm (f n)} = {n. norm (f n) \<le> u}"
  1939 by auto
  1940 
  1941 lemma lemma_Compl_eq2: "- {n. norm (f n) < u} = {n. u \<le> norm (f n)}"
  1942 by auto
  1943 
  1944 lemma lemma_Int_eq1:
  1945      "{n. norm (f n) \<le> u} Int {n. u \<le> norm (f n)} = {n. norm(f n) = u}"
  1946 by auto
  1947 
  1948 lemma lemma_FreeUltrafilterNat_one:
  1949      "{n. norm (f n) = u} \<le> {n. norm (f n) < u + (1::real)}"
  1950 by auto
  1951 
  1952 (*-------------------------------------
  1953   Exclude this type of sets from free
  1954   ultrafilter for Infinite numbers!
  1955  -------------------------------------*)
  1956 lemma FreeUltrafilterNat_const_Finite:
  1957      "eventually (\<lambda>n. norm (X n) = u) FreeUltrafilterNat ==> star_n X \<in> HFinite"
  1958 apply (rule FreeUltrafilterNat_HFinite)
  1959 apply (rule_tac x = "u + 1" in exI)
  1960 apply (auto elim: eventually_mono)
  1961 done
  1962 
  1963 lemma HInfinite_FreeUltrafilterNat:
  1964      "star_n X \<in> HInfinite ==> \<forall>u. eventually (\<lambda>n. u < norm (X n)) FreeUltrafilterNat"
  1965 apply (drule HInfinite_HFinite_iff [THEN iffD1])
  1966 apply (simp add: HFinite_FreeUltrafilterNat_iff)
  1967 apply (rule allI, drule_tac x="u + 1" in spec)
  1968 apply (simp add: FreeUltrafilterNat.eventually_not_iff[symmetric])
  1969 apply (auto elim: eventually_mono)
  1970 done
  1971 
  1972 lemma lemma_Int_HI:
  1973      "{n. norm (Xa n) < u} Int {n. X n = Xa n} \<subseteq> {n. norm (X n) < (u::real)}"
  1974 by auto
  1975 
  1976 lemma lemma_Int_HIa: "{n. u < norm (X n)} Int {n. norm (X n) < u} = {}"
  1977 by (auto intro: order_less_asym)
  1978 
  1979 lemma FreeUltrafilterNat_HInfinite:
  1980      "\<forall>u. eventually (\<lambda>n. u < norm (X n)) FreeUltrafilterNat ==> star_n X \<in> HInfinite"
  1981 apply (rule HInfinite_HFinite_iff [THEN iffD2])
  1982 apply (safe, drule HFinite_FreeUltrafilterNat, safe)
  1983 apply (drule_tac x = u in spec)
  1984 proof -
  1985   fix u assume "\<forall>\<^sub>Fn in \<U>. norm (X n) < u" "\<forall>\<^sub>Fn in \<U>. u < norm (X n)"
  1986   then have "\<forall>\<^sub>F x in \<U>. False"
  1987     by eventually_elim auto
  1988   then show False
  1989     by (simp add: eventually_False FreeUltrafilterNat.proper)
  1990 qed
  1991 
  1992 lemma HInfinite_FreeUltrafilterNat_iff:
  1993      "(star_n X \<in> HInfinite) = (\<forall>u. eventually (\<lambda>n. u < norm (X n)) FreeUltrafilterNat)"
  1994 by (blast intro!: HInfinite_FreeUltrafilterNat FreeUltrafilterNat_HInfinite)
  1995 
  1996 subsubsection \<open>@{term Infinitesimal}\<close>
  1997 
  1998 lemma ball_SReal_eq: "(\<forall>x::hypreal \<in> Reals. P x) = (\<forall>x::real. P (star_of x))"
  1999 by (unfold SReal_def, auto)
  2000 
  2001 lemma Infinitesimal_FreeUltrafilterNat:
  2002      "star_n X \<in> Infinitesimal ==> \<forall>u>0. eventually (\<lambda>n. norm (X n) < u) \<U>"
  2003 apply (simp add: Infinitesimal_def ball_SReal_eq)
  2004 apply (simp add: hnorm_def starfun_star_n star_of_def)
  2005 apply (simp add: star_less_def starP2_star_n)
  2006 done
  2007 
  2008 lemma FreeUltrafilterNat_Infinitesimal:
  2009      "\<forall>u>0. eventually (\<lambda>n. norm (X n) < u) \<U> ==> star_n X \<in> Infinitesimal"
  2010 apply (simp add: Infinitesimal_def ball_SReal_eq)
  2011 apply (simp add: hnorm_def starfun_star_n star_of_def)
  2012 apply (simp add: star_less_def starP2_star_n)
  2013 done
  2014 
  2015 lemma Infinitesimal_FreeUltrafilterNat_iff:
  2016      "(star_n X \<in> Infinitesimal) = (\<forall>u>0. eventually (\<lambda>n. norm (X n) < u) \<U>)"
  2017 by (blast intro!: Infinitesimal_FreeUltrafilterNat FreeUltrafilterNat_Infinitesimal)
  2018 
  2019 (*------------------------------------------------------------------------
  2020          Infinitesimals as smaller than 1/n for all n::nat (> 0)
  2021  ------------------------------------------------------------------------*)
  2022 
  2023 lemma lemma_Infinitesimal:
  2024      "(\<forall>r. 0 < r --> x < r) = (\<forall>n. x < inverse(real (Suc n)))"
  2025 apply (auto simp del: of_nat_Suc)
  2026 apply (blast dest!: reals_Archimedean intro: order_less_trans)
  2027 done
  2028 
  2029 lemma lemma_Infinitesimal2:
  2030      "(\<forall>r \<in> Reals. 0 < r --> x < r) =
  2031       (\<forall>n. x < inverse(hypreal_of_nat (Suc n)))"
  2032 apply safe
  2033  apply (drule_tac x = "inverse (hypreal_of_real (real (Suc n))) " in bspec)
  2034   apply simp_all
  2035   using less_imp_of_nat_less apply fastforce
  2036 apply (auto dest!: reals_Archimedean simp add: SReal_iff simp del: of_nat_Suc)
  2037 apply (drule star_of_less [THEN iffD2])
  2038 apply simp
  2039 apply (blast intro: order_less_trans)
  2040 done
  2041 
  2042 
  2043 lemma Infinitesimal_hypreal_of_nat_iff:
  2044      "Infinitesimal = {x. \<forall>n. hnorm x < inverse (hypreal_of_nat (Suc n))}"
  2045 apply (simp add: Infinitesimal_def)
  2046 apply (auto simp add: lemma_Infinitesimal2)
  2047 done
  2048 
  2049 
  2050 subsection\<open>Proof that \<open>\<omega>\<close> is an infinite number\<close>
  2051 
  2052 text\<open>It will follow that \<open>\<epsilon>\<close> is an infinitesimal number.\<close>
  2053 
  2054 lemma Suc_Un_eq: "{n. n < Suc m} = {n. n < m} Un {n. n = m}"
  2055 by (auto simp add: less_Suc_eq)
  2056 
  2057 (*-------------------------------------------
  2058   Prove that any segment is finite and hence cannot belong to FreeUltrafilterNat
  2059  -------------------------------------------*)
  2060 
  2061 lemma finite_real_of_nat_segment: "finite {n::nat. real n < real (m::nat)}"
  2062   by (auto intro: finite_Collect_less_nat)
  2063 
  2064 lemma finite_real_of_nat_less_real: "finite {n::nat. real n < u}"
  2065 apply (cut_tac x = u in reals_Archimedean2, safe)
  2066 apply (rule finite_real_of_nat_segment [THEN [2] finite_subset])
  2067 apply (auto dest: order_less_trans)
  2068 done
  2069 
  2070 lemma lemma_real_le_Un_eq:
  2071      "{n. f n \<le> u} = {n. f n < u} Un {n. u = (f n :: real)}"
  2072 by (auto dest: order_le_imp_less_or_eq simp add: order_less_imp_le)
  2073 
  2074 lemma finite_real_of_nat_le_real: "finite {n::nat. real n \<le> u}"
  2075 by (auto simp add: lemma_real_le_Un_eq lemma_finite_omega_set finite_real_of_nat_less_real)
  2076 
  2077 lemma finite_rabs_real_of_nat_le_real: "finite {n::nat. \<bar>real n\<bar> \<le> u}"
  2078 apply (simp (no_asm) add: finite_real_of_nat_le_real)
  2079 done
  2080 
  2081 lemma rabs_real_of_nat_le_real_FreeUltrafilterNat:
  2082      "\<not> eventually (\<lambda>n. \<bar>real n\<bar> \<le> u) FreeUltrafilterNat"
  2083 by (blast intro!: FreeUltrafilterNat.finite finite_rabs_real_of_nat_le_real)
  2084 
  2085 lemma FreeUltrafilterNat_nat_gt_real: "eventually (\<lambda>n. u < real n) FreeUltrafilterNat"
  2086 apply (rule FreeUltrafilterNat.finite')
  2087 apply (subgoal_tac "{n::nat. \<not> u < real n} = {n. real n \<le> u}")
  2088 apply (auto simp add: finite_real_of_nat_le_real)
  2089 done
  2090 
  2091 (*--------------------------------------------------------------
  2092  The complement of {n. \<bar>real n\<bar> \<le> u} =
  2093  {n. u < \<bar>real n\<bar>} is in FreeUltrafilterNat
  2094  by property of (free) ultrafilters
  2095  --------------------------------------------------------------*)
  2096 
  2097 lemma Compl_real_le_eq: "- {n::nat. real n \<le> u} = {n. u < real n}"
  2098 by (auto dest!: order_le_less_trans simp add: linorder_not_le)
  2099 
  2100 text\<open>@{term \<omega>} is a member of @{term HInfinite}\<close>
  2101 
  2102 theorem HInfinite_omega [simp]: "\<omega> \<in> HInfinite"
  2103 apply (simp add: omega_def)
  2104 apply (rule FreeUltrafilterNat_HInfinite)
  2105 apply clarify
  2106 apply (rule_tac u1 = "u-1" in eventually_mono [OF FreeUltrafilterNat_nat_gt_real])
  2107 apply auto
  2108 done
  2109 
  2110 (*-----------------------------------------------
  2111        Epsilon is a member of Infinitesimal
  2112  -----------------------------------------------*)
  2113 
  2114 lemma Infinitesimal_epsilon [simp]: "\<epsilon> \<in> Infinitesimal"
  2115 by (auto intro!: HInfinite_inverse_Infinitesimal HInfinite_omega simp add: hypreal_epsilon_inverse_omega)
  2116 
  2117 lemma HFinite_epsilon [simp]: "\<epsilon> \<in> HFinite"
  2118 by (auto intro: Infinitesimal_subset_HFinite [THEN subsetD])
  2119 
  2120 lemma epsilon_approx_zero [simp]: "\<epsilon> \<approx> 0"
  2121 apply (simp (no_asm) add: mem_infmal_iff [symmetric])
  2122 done
  2123 
  2124 (*------------------------------------------------------------------------
  2125   Needed for proof that we define a hyperreal [<X(n)] \<approx> hypreal_of_real a given
  2126   that \<forall>n. |X n - a| < 1/n. Used in proof of NSLIM => LIM.
  2127  -----------------------------------------------------------------------*)
  2128 
  2129 lemma real_of_nat_less_inverse_iff:
  2130      "0 < u  ==> (u < inverse (real(Suc n))) = (real(Suc n) < inverse u)"
  2131 apply (simp add: inverse_eq_divide)
  2132 apply (subst pos_less_divide_eq, assumption)
  2133 apply (subst pos_less_divide_eq)
  2134  apply simp
  2135 apply (simp add: mult.commute)
  2136 done
  2137 
  2138 lemma finite_inverse_real_of_posnat_gt_real:
  2139      "0 < u ==> finite {n. u < inverse(real(Suc n))}"
  2140 proof (simp only: real_of_nat_less_inverse_iff)
  2141   have "{n. 1 + real n < inverse u} = {n. real n < inverse u - 1}"
  2142     by fastforce
  2143   thus "finite {n. real (Suc n) < inverse u}"
  2144     using finite_real_of_nat_less_real [of "inverse u - 1"] by auto
  2145 qed
  2146 
  2147 lemma lemma_real_le_Un_eq2:
  2148      "{n. u \<le> inverse(real(Suc n))} =
  2149      {n. u < inverse(real(Suc n))} Un {n. u = inverse(real(Suc n))}"
  2150 by (auto dest: order_le_imp_less_or_eq simp add: order_less_imp_le)
  2151 
  2152 lemma finite_inverse_real_of_posnat_ge_real:
  2153      "0 < u ==> finite {n. u \<le> inverse(real(Suc n))}"
  2154 by (auto simp add: lemma_real_le_Un_eq2 lemma_finite_epsilon_set finite_inverse_real_of_posnat_gt_real
  2155             simp del: of_nat_Suc)
  2156 
  2157 lemma inverse_real_of_posnat_ge_real_FreeUltrafilterNat:
  2158      "0 < u ==> \<not> eventually (\<lambda>n. u \<le> inverse(real(Suc n))) FreeUltrafilterNat"
  2159 by (blast intro!: FreeUltrafilterNat.finite finite_inverse_real_of_posnat_ge_real)
  2160 
  2161 (*--------------------------------------------------------------
  2162     The complement of  {n. u \<le> inverse(real(Suc n))} =
  2163     {n. inverse(real(Suc n)) < u} is in FreeUltrafilterNat
  2164     by property of (free) ultrafilters
  2165  --------------------------------------------------------------*)
  2166 lemma Compl_le_inverse_eq:
  2167      "- {n. u \<le> inverse(real(Suc n))} = {n. inverse(real(Suc n)) < u}"
  2168 by (auto dest!: order_le_less_trans simp add: linorder_not_le)
  2169 
  2170 
  2171 lemma FreeUltrafilterNat_inverse_real_of_posnat:
  2172      "0 < u ==> eventually (\<lambda>n. inverse(real(Suc n)) < u) FreeUltrafilterNat"
  2173 by (drule inverse_real_of_posnat_ge_real_FreeUltrafilterNat)
  2174    (simp add: FreeUltrafilterNat.eventually_not_iff not_le[symmetric])
  2175 
  2176 text\<open>Example of an hypersequence (i.e. an extended standard sequence)
  2177    whose term with an hypernatural suffix is an infinitesimal i.e.
  2178    the whn'nth term of the hypersequence is a member of Infinitesimal\<close>
  2179 
  2180 lemma SEQ_Infinitesimal:
  2181       "( *f* (%n::nat. inverse(real(Suc n)))) whn : Infinitesimal"
  2182 by (simp add: hypnat_omega_def starfun_star_n star_n_inverse Infinitesimal_FreeUltrafilterNat_iff
  2183         FreeUltrafilterNat_inverse_real_of_posnat del: of_nat_Suc)
  2184 
  2185 text\<open>Example where we get a hyperreal from a real sequence
  2186       for which a particular property holds. The theorem is
  2187       used in proofs about equivalence of nonstandard and
  2188       standard neighbourhoods. Also used for equivalence of
  2189       nonstandard ans standard definitions of pointwise
  2190       limit.\<close>
  2191 
  2192 (*-----------------------------------------------------
  2193     |X(n) - x| < 1/n ==> [<X n>] - hypreal_of_real x| \<in> Infinitesimal
  2194  -----------------------------------------------------*)
  2195 lemma real_seq_to_hypreal_Infinitesimal:
  2196      "\<forall>n. norm(X n - x) < inverse(real(Suc n))
  2197      ==> star_n X - star_of x \<in> Infinitesimal"
  2198 unfolding star_n_diff star_of_def Infinitesimal_FreeUltrafilterNat_iff star_n_inverse
  2199 by (auto dest!: FreeUltrafilterNat_inverse_real_of_posnat
  2200          intro: order_less_trans elim!: eventually_mono)
  2201 
  2202 lemma real_seq_to_hypreal_approx:
  2203      "\<forall>n. norm(X n - x) < inverse(real(Suc n))
  2204       ==> star_n X \<approx> star_of x"
  2205 by (metis bex_Infinitesimal_iff real_seq_to_hypreal_Infinitesimal)
  2206 
  2207 lemma real_seq_to_hypreal_approx2:
  2208      "\<forall>n. norm(x - X n) < inverse(real(Suc n))
  2209                ==> star_n X \<approx> star_of x"
  2210 by (metis norm_minus_commute real_seq_to_hypreal_approx)
  2211 
  2212 lemma real_seq_to_hypreal_Infinitesimal2:
  2213      "\<forall>n. norm(X n - Y n) < inverse(real(Suc n))
  2214       ==> star_n X - star_n Y \<in> Infinitesimal"
  2215 unfolding Infinitesimal_FreeUltrafilterNat_iff star_n_diff
  2216 by (auto dest!: FreeUltrafilterNat_inverse_real_of_posnat
  2217          intro: order_less_trans elim!: eventually_mono)
  2218 
  2219 end