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