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