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