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