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