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