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