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