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