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