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