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