huge de-apply effort
authorpaulson <lp15@cam.ac.uk>
Tue Apr 30 21:04:08 2019 +0100 (6 months ago)
changeset 70221bca14283e1a8
parent 70211 2388e0d2827b
child 70222 bde8ccb73fd2
huge de-apply effort
src/HOL/Nonstandard_Analysis/NSA.thy
     1.1 --- a/src/HOL/Nonstandard_Analysis/NSA.thy	Mon Apr 29 00:36:54 2019 +0100
     1.2 +++ b/src/HOL/Nonstandard_Analysis/NSA.thy	Tue Apr 30 21:04:08 2019 +0100
     1.3 @@ -6,7 +6,7 @@
     1.4  section \<open>Infinite Numbers, Infinitesimals, Infinitely Close Relation\<close>
     1.5  
     1.6  theory NSA
     1.7 -  imports HyperDef "HOL-Library.Lub_Glb"
     1.8 +  imports HyperDef "HOL-Library.Lub_Glb" 
     1.9  begin
    1.10  
    1.11  definition hnorm :: "'a::real_normed_vector star \<Rightarrow> real star"
    1.12 @@ -162,37 +162,11 @@
    1.13    by (simp add: Reals_eq_Standard Standard_def)
    1.14  
    1.15  lemma inv_hypreal_of_real_image: "inv hypreal_of_real ` \<real> = UNIV"
    1.16 -  apply (auto simp add: SReal_def)
    1.17 -  apply (rule inj_star_of [THEN inv_f_f, THEN subst], blast)
    1.18 -  done
    1.19 -
    1.20 -lemma SReal_hypreal_of_real_image: "\<exists>x. x \<in> P \<Longrightarrow> P \<subseteq> \<real> \<Longrightarrow> \<exists>Q. P = hypreal_of_real ` Q"
    1.21 -  unfolding SReal_def image_def by blast
    1.22 +  by (simp add: Reals_eq_Standard Standard_def inj_star_of)
    1.23  
    1.24  lemma SReal_dense: "x \<in> \<real> \<Longrightarrow> y \<in> \<real> \<Longrightarrow> x < y \<Longrightarrow> \<exists>r \<in> Reals. x < r \<and> r < y"
    1.25    for x y :: hypreal
    1.26 -  apply (auto simp: SReal_def)
    1.27 -  apply (drule dense)
    1.28 -  apply auto
    1.29 -  done
    1.30 -
    1.31 -
    1.32 -text \<open>Completeness of Reals, but both lemmas are unused.\<close>
    1.33 -
    1.34 -lemma SReal_sup_lemma:
    1.35 -  "P \<subseteq> \<real> \<Longrightarrow> (\<exists>x \<in> P. y < x) = (\<exists>X. hypreal_of_real X \<in> P \<and> y < hypreal_of_real X)"
    1.36 -  by (blast dest!: SReal_iff [THEN iffD1])
    1.37 -
    1.38 -lemma SReal_sup_lemma2:
    1.39 -  "P \<subseteq> \<real> \<Longrightarrow> \<exists>x. x \<in> P \<Longrightarrow> \<exists>y \<in> Reals. \<forall>x \<in> P. x < y \<Longrightarrow>
    1.40 -    (\<exists>X. X \<in> {w. hypreal_of_real w \<in> P}) \<and>
    1.41 -    (\<exists>Y. \<forall>X \<in> {w. hypreal_of_real w \<in> P}. X < Y)"
    1.42 -  apply (rule conjI)
    1.43 -   apply (fast dest!: SReal_iff [THEN iffD1])
    1.44 -  apply (auto, frule subsetD, assumption)
    1.45 -  apply (drule SReal_iff [THEN iffD1])
    1.46 -  apply (auto, rule_tac x = ya in exI, auto)
    1.47 -  done
    1.48 +  using dense by (fastforce simp add: SReal_def)
    1.49  
    1.50  
    1.51  subsection \<open>Set of Finite Elements is a Subring of the Extended Reals\<close>
    1.52 @@ -211,11 +185,7 @@
    1.53    by (simp add: HFinite_def)
    1.54  
    1.55  lemma HFinite_star_of [simp]: "star_of x \<in> HFinite"
    1.56 -  apply (simp add: HFinite_def)
    1.57 -  apply (rule_tac x="star_of (norm x) + 1" in bexI)
    1.58 -   apply (transfer, simp)
    1.59 -  apply (blast intro: Reals_add SReal_hypreal_of_real Reals_1)
    1.60 -  done
    1.61 +  by (simp add: HFinite_def) (metis SReal_hypreal_of_real gt_ex star_of_less star_of_norm)
    1.62  
    1.63  lemma SReal_subset_HFinite: "(\<real>::hypreal set) \<subseteq> HFinite"
    1.64    by (auto simp add: SReal_def)
    1.65 @@ -244,16 +214,22 @@
    1.66  
    1.67  lemma hrealpow_HFinite: "x \<in> HFinite \<Longrightarrow> x ^ n \<in> HFinite"
    1.68    for x :: "'a::{real_normed_algebra,monoid_mult} star"
    1.69 -  by (induct n) (auto simp add: power_Suc intro: HFinite_mult)
    1.70 +  by (induct n) (auto intro: HFinite_mult)
    1.71  
    1.72 -lemma HFinite_bounded: "x \<in> HFinite \<Longrightarrow> y \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> y \<in> HFinite"
    1.73 -  for x y :: hypreal
    1.74 -  apply (cases "x \<le> 0")
    1.75 -   apply (drule_tac y = x in order_trans)
    1.76 -    apply (drule_tac [2] order_antisym)
    1.77 -     apply (auto simp add: linorder_not_le)
    1.78 -  apply (auto intro: order_le_less_trans simp add: abs_if HFinite_def)
    1.79 -  done
    1.80 +lemma HFinite_bounded: 
    1.81 +  fixes x y :: hypreal
    1.82 +  assumes "x \<in> HFinite" and y: "y \<le> x" "0 \<le> y" shows "y \<in> HFinite"
    1.83 +proof (cases "x \<le> 0")
    1.84 +  case True
    1.85 +  then have "y = 0"
    1.86 +    using y by auto
    1.87 +  then show ?thesis
    1.88 +    by simp
    1.89 +next
    1.90 +  case False
    1.91 +  then show ?thesis
    1.92 +    using assms le_less_trans by (auto simp: HFinite_def)
    1.93 +qed
    1.94  
    1.95  
    1.96  subsection \<open>Set of Infinitesimals is a Subring of the Hyperreals\<close>
    1.97 @@ -273,12 +249,19 @@
    1.98  lemma Infinitesimal_zero [iff]: "0 \<in> Infinitesimal"
    1.99    by (simp add: Infinitesimal_def)
   1.100  
   1.101 -lemma Infinitesimal_add: "x \<in> Infinitesimal \<Longrightarrow> y \<in> Infinitesimal \<Longrightarrow> x + y \<in> Infinitesimal"
   1.102 -  apply (rule InfinitesimalI)
   1.103 -  apply (rule field_sum_of_halves [THEN subst])
   1.104 -  apply (drule half_gt_zero)
   1.105 -  apply (blast intro: hnorm_add_less SReal_divide_numeral dest: InfinitesimalD)
   1.106 -  done
   1.107 +lemma Infinitesimal_add:
   1.108 +  assumes "x \<in> Infinitesimal" "y \<in> Infinitesimal"
   1.109 +  shows "x + y \<in> Infinitesimal"
   1.110 +proof (rule InfinitesimalI)
   1.111 +  show "hnorm (x + y) < r"
   1.112 +    if "r \<in> \<real>" and "0 < r" for r :: "real star"
   1.113 +  proof -
   1.114 +    have "hnorm x < r/2" "hnorm y < r/2"
   1.115 +      using InfinitesimalD SReal_divide_numeral assms half_gt_zero that by blast+
   1.116 +    then show ?thesis
   1.117 +      using hnorm_add_less by fastforce
   1.118 +  qed
   1.119 +qed
   1.120  
   1.121  lemma Infinitesimal_minus_iff [simp]: "- x \<in> Infinitesimal \<longleftrightarrow> x \<in> Infinitesimal"
   1.122    by (simp add: Infinitesimal_def)
   1.123 @@ -297,83 +280,103 @@
   1.124  lemma Infinitesimal_diff: "x \<in> Infinitesimal \<Longrightarrow> y \<in> Infinitesimal \<Longrightarrow> x - y \<in> Infinitesimal"
   1.125    using Infinitesimal_add [of x "- y"] by simp
   1.126  
   1.127 -lemma Infinitesimal_mult: "x \<in> Infinitesimal \<Longrightarrow> y \<in> Infinitesimal \<Longrightarrow> x * y \<in> Infinitesimal"
   1.128 -  for x y :: "'a::real_normed_algebra star"
   1.129 -  apply (rule InfinitesimalI)
   1.130 -  apply (subgoal_tac "hnorm (x * y) < 1 * r")
   1.131 -   apply (simp only: mult_1)
   1.132 -  apply (rule hnorm_mult_less)
   1.133 -   apply (simp_all add: InfinitesimalD)
   1.134 -  done
   1.135 +lemma Infinitesimal_mult: 
   1.136 +  fixes x y :: "'a::real_normed_algebra star"
   1.137 +  assumes "x \<in> Infinitesimal" "y \<in> Infinitesimal"
   1.138 +  shows "x * y \<in> Infinitesimal"
   1.139 +  proof (rule InfinitesimalI)
   1.140 +  show "hnorm (x * y) < r"
   1.141 +    if "r \<in> \<real>" and "0 < r" for r :: "real star"
   1.142 +  proof -
   1.143 +    have "hnorm x < 1" "hnorm y < r"
   1.144 +      using assms that  by (auto simp add: InfinitesimalD)
   1.145 +    then show ?thesis
   1.146 +      using hnorm_mult_less by fastforce
   1.147 +  qed
   1.148 +qed
   1.149  
   1.150 -lemma Infinitesimal_HFinite_mult: "x \<in> Infinitesimal \<Longrightarrow> y \<in> HFinite \<Longrightarrow> x * y \<in> Infinitesimal"
   1.151 -  for x y :: "'a::real_normed_algebra star"
   1.152 -  apply (rule InfinitesimalI)
   1.153 -  apply (drule HFiniteD, clarify)
   1.154 -  apply (subgoal_tac "0 < t")
   1.155 -   apply (subgoal_tac "hnorm (x * y) < (r / t) * t", simp)
   1.156 -   apply (subgoal_tac "0 < r / t")
   1.157 -    apply (rule hnorm_mult_less)
   1.158 -     apply (simp add: InfinitesimalD)
   1.159 -    apply assumption
   1.160 -   apply simp
   1.161 -  apply (erule order_le_less_trans [OF hnorm_ge_zero])
   1.162 -  done
   1.163 +lemma Infinitesimal_HFinite_mult:
   1.164 +  fixes x y :: "'a::real_normed_algebra star"
   1.165 +  assumes "x \<in> Infinitesimal" "y \<in> HFinite"
   1.166 +  shows "x * y \<in> Infinitesimal"
   1.167 +proof (rule InfinitesimalI)
   1.168 +  obtain t where "hnorm y < t" "t \<in> Reals"
   1.169 +    using HFiniteD \<open>y \<in> HFinite\<close> by blast
   1.170 +  then have "t > 0"
   1.171 +    using hnorm_ge_zero le_less_trans by blast
   1.172 +  show "hnorm (x * y) < r"
   1.173 +    if "r \<in> \<real>" and "0 < r" for r :: "real star"
   1.174 +  proof -
   1.175 +    have "hnorm x < r/t"
   1.176 +      by (meson InfinitesimalD Reals_divide \<open>hnorm y < t\<close> \<open>t \<in> \<real>\<close> assms(1) divide_pos_pos hnorm_ge_zero le_less_trans that) 
   1.177 +    then have "hnorm (x * y) < (r / t) * t"
   1.178 +      using \<open>hnorm y < t\<close> hnorm_mult_less by blast
   1.179 +    then show ?thesis
   1.180 +      using \<open>0 < t\<close> by auto
   1.181 +  qed
   1.182 +qed
   1.183  
   1.184  lemma Infinitesimal_HFinite_scaleHR:
   1.185 -  "x \<in> Infinitesimal \<Longrightarrow> y \<in> HFinite \<Longrightarrow> scaleHR x y \<in> Infinitesimal"
   1.186 -  apply (rule InfinitesimalI)
   1.187 -  apply (drule HFiniteD, clarify)
   1.188 -  apply (drule InfinitesimalD)
   1.189 -  apply (simp add: hnorm_scaleHR)
   1.190 -  apply (subgoal_tac "0 < t")
   1.191 -   apply (subgoal_tac "\<bar>x\<bar> * hnorm y < (r / t) * t", simp)
   1.192 -   apply (subgoal_tac "0 < r / t")
   1.193 -    apply (rule mult_strict_mono', simp_all)
   1.194 -  apply (erule order_le_less_trans [OF hnorm_ge_zero])
   1.195 -  done
   1.196 +  assumes "x \<in> Infinitesimal" "y \<in> HFinite"
   1.197 +  shows "scaleHR x y \<in> Infinitesimal"
   1.198 +proof (rule InfinitesimalI)
   1.199 +  obtain t where "hnorm y < t" "t \<in> Reals"
   1.200 +    using HFiniteD \<open>y \<in> HFinite\<close> by blast
   1.201 +  then have "t > 0"
   1.202 +    using hnorm_ge_zero le_less_trans by blast
   1.203 +  show "hnorm (scaleHR x y) < r"
   1.204 +    if "r \<in> \<real>" and "0 < r" for r :: "real star"
   1.205 +  proof -
   1.206 +    have "\<bar>x\<bar> * hnorm y < (r / t) * t"
   1.207 +      by (metis InfinitesimalD Reals_divide \<open>0 < t\<close> \<open>hnorm y < t\<close> \<open>t \<in> \<real>\<close> assms(1) divide_pos_pos hnorm_ge_zero hypreal_hnorm_def mult_strict_mono' that)
   1.208 +    then show ?thesis
   1.209 +      by (simp add: \<open>0 < t\<close> hnorm_scaleHR less_imp_not_eq2)
   1.210 +  qed
   1.211 +qed
   1.212  
   1.213  lemma Infinitesimal_HFinite_mult2:
   1.214 -  "x \<in> Infinitesimal \<Longrightarrow> y \<in> HFinite \<Longrightarrow> y * x \<in> Infinitesimal"
   1.215 -  for x y :: "'a::real_normed_algebra star"
   1.216 -  apply (rule InfinitesimalI)
   1.217 -  apply (drule HFiniteD, clarify)
   1.218 -  apply (subgoal_tac "0 < t")
   1.219 -   apply (subgoal_tac "hnorm (y * x) < t * (r / t)", simp)
   1.220 -   apply (subgoal_tac "0 < r / t")
   1.221 -    apply (rule hnorm_mult_less)
   1.222 -     apply assumption
   1.223 -    apply (simp add: InfinitesimalD)
   1.224 -   apply simp
   1.225 -  apply (erule order_le_less_trans [OF hnorm_ge_zero])
   1.226 -  done
   1.227 +  fixes x y :: "'a::real_normed_algebra star"
   1.228 +  assumes "x \<in> Infinitesimal" "y \<in> HFinite"
   1.229 +  shows  "y * x \<in> Infinitesimal"
   1.230 +proof (rule InfinitesimalI)
   1.231 +  obtain t where "hnorm y < t" "t \<in> Reals"
   1.232 +    using HFiniteD \<open>y \<in> HFinite\<close> by blast
   1.233 +  then have "t > 0"
   1.234 +    using hnorm_ge_zero le_less_trans by blast
   1.235 +  show "hnorm (y * x) < r"
   1.236 +    if "r \<in> \<real>" and "0 < r" for r :: "real star"
   1.237 +  proof -
   1.238 +    have "hnorm x < r/t"
   1.239 +      by (meson InfinitesimalD Reals_divide \<open>hnorm y < t\<close> \<open>t \<in> \<real>\<close> assms(1) divide_pos_pos hnorm_ge_zero le_less_trans that) 
   1.240 +    then have "hnorm (y * x) < t * (r / t)"
   1.241 +      using \<open>hnorm y < t\<close> hnorm_mult_less by blast
   1.242 +    then show ?thesis
   1.243 +      using \<open>0 < t\<close> by auto
   1.244 +  qed
   1.245 +qed
   1.246  
   1.247 -lemma Infinitesimal_scaleR2: "x \<in> Infinitesimal \<Longrightarrow> a *\<^sub>R x \<in> Infinitesimal"
   1.248 -  apply (case_tac "a = 0", simp)
   1.249 -  apply (rule InfinitesimalI)
   1.250 -  apply (drule InfinitesimalD)
   1.251 -  apply (drule_tac x="r / \<bar>star_of a\<bar>" in bspec)
   1.252 -   apply (simp add: Reals_eq_Standard)
   1.253 -  apply simp
   1.254 -  apply (simp add: hnorm_scaleR pos_less_divide_eq mult.commute)
   1.255 -  done
   1.256 +lemma Infinitesimal_scaleR2: 
   1.257 +  assumes "x \<in> Infinitesimal" shows "a *\<^sub>R x \<in> Infinitesimal"
   1.258 +    by (metis HFinite_star_of Infinitesimal_HFinite_mult2 Infinitesimal_hnorm_iff assms hnorm_scaleR hypreal_hnorm_def star_of_norm)
   1.259  
   1.260  lemma Compl_HFinite: "- HFinite = HInfinite"
   1.261 -  apply (auto simp add: HInfinite_def HFinite_def linorder_not_less)
   1.262 -  apply (rule_tac y="r + 1" in order_less_le_trans, simp)
   1.263 -  apply simp
   1.264 -  done
   1.265 +  proof -
   1.266 +  have "r < hnorm x" if *: "\<And>s. s \<in> \<real> \<Longrightarrow> s \<le> hnorm x" and "r \<in> \<real>"
   1.267 +    for x :: "'a star" and r :: hypreal
   1.268 +    using * [of "r+1"] \<open>r \<in> \<real>\<close> by auto
   1.269 +  then show ?thesis
   1.270 +    by (auto simp add: HInfinite_def HFinite_def linorder_not_less)
   1.271 +qed
   1.272  
   1.273 -lemma HInfinite_inverse_Infinitesimal: "x \<in> HInfinite \<Longrightarrow> inverse x \<in> Infinitesimal"
   1.274 +lemma HInfinite_inverse_Infinitesimal:
   1.275 +  "x \<in> HInfinite \<Longrightarrow> inverse x \<in> Infinitesimal"
   1.276    for x :: "'a::real_normed_div_algebra star"
   1.277 -  apply (rule InfinitesimalI)
   1.278 -  apply (subgoal_tac "x \<noteq> 0")
   1.279 -   apply (rule inverse_less_imp_less)
   1.280 -    apply (simp add: nonzero_hnorm_inverse)
   1.281 -    apply (simp add: HInfinite_def Reals_inverse)
   1.282 -   apply assumption
   1.283 -  apply (clarify, simp add: Compl_HFinite [symmetric])
   1.284 -  done
   1.285 +  by (simp add: HInfinite_def InfinitesimalI hnorm_inverse inverse_less_imp_less)
   1.286 +
   1.287 +lemma inverse_Infinitesimal_iff_HInfinite:
   1.288 +  "x \<noteq> 0 \<Longrightarrow> inverse x \<in> Infinitesimal \<longleftrightarrow> x \<in> HInfinite"
   1.289 +  for x :: "'a::real_normed_div_algebra star"
   1.290 +  by (metis Compl_HFinite Compl_iff HInfinite_inverse_Infinitesimal InfinitesimalD Infinitesimal_HFinite_mult Reals_1 hnorm_one left_inverse less_irrefl zero_less_one)
   1.291  
   1.292  lemma HInfiniteI: "(\<And>r. r \<in> \<real> \<Longrightarrow> r < hnorm x) \<Longrightarrow> x \<in> HInfinite"
   1.293    by (simp add: HInfinite_def)
   1.294 @@ -381,18 +384,26 @@
   1.295  lemma HInfiniteD: "x \<in> HInfinite \<Longrightarrow> r \<in> \<real> \<Longrightarrow> r < hnorm x"
   1.296    by (simp add: HInfinite_def)
   1.297  
   1.298 -lemma HInfinite_mult: "x \<in> HInfinite \<Longrightarrow> y \<in> HInfinite \<Longrightarrow> x * y \<in> HInfinite"
   1.299 -  for x y :: "'a::real_normed_div_algebra star"
   1.300 -  apply (rule HInfiniteI, simp only: hnorm_mult)
   1.301 -  apply (subgoal_tac "r * 1 < hnorm x * hnorm y", simp only: mult_1)
   1.302 -  apply (case_tac "x = 0", simp add: HInfinite_def)
   1.303 -  apply (rule mult_strict_mono)
   1.304 -     apply (simp_all add: HInfiniteD)
   1.305 -  done
   1.306 +lemma HInfinite_mult: 
   1.307 +  fixes x y :: "'a::real_normed_div_algebra star"
   1.308 +  assumes "x \<in> HInfinite" "y \<in> HInfinite" shows "x * y \<in> HInfinite"
   1.309 +proof (rule HInfiniteI, simp only: hnorm_mult)
   1.310 +  have "x \<noteq> 0"
   1.311 +    using Compl_HFinite HFinite_0 assms by blast
   1.312 +  show "r < hnorm x * hnorm y"
   1.313 +    if "r \<in> \<real>" for r :: "real star"
   1.314 +  proof -
   1.315 +    have "r = r * 1"
   1.316 +      by simp
   1.317 +    also have "\<dots> < hnorm x * hnorm y"
   1.318 +      by (meson HInfiniteD Reals_1 \<open>x \<noteq> 0\<close> assms le_numeral_extra(1) mult_strict_mono that zero_less_hnorm_iff)
   1.319 +    finally show ?thesis .
   1.320 +  qed
   1.321 +qed
   1.322  
   1.323  lemma hypreal_add_zero_less_le_mono: "r < x \<Longrightarrow> 0 \<le> y \<Longrightarrow> r < x + y"
   1.324    for r x y :: hypreal
   1.325 -  by (auto dest: add_less_le_mono)
   1.326 +  by simp
   1.327  
   1.328  lemma HInfinite_add_ge_zero: "x \<in> HInfinite \<Longrightarrow> 0 \<le> y \<Longrightarrow> 0 \<le> x \<Longrightarrow> x + y \<in> HInfinite"
   1.329    for x y :: hypreal
   1.330 @@ -411,12 +422,7 @@
   1.331  
   1.332  lemma HInfinite_add_le_zero: "x \<in> HInfinite \<Longrightarrow> y \<le> 0 \<Longrightarrow> x \<le> 0 \<Longrightarrow> x + y \<in> HInfinite"
   1.333    for x y :: hypreal
   1.334 -  apply (drule HInfinite_minus_iff [THEN iffD2])
   1.335 -  apply (rule HInfinite_minus_iff [THEN iffD1])
   1.336 -  apply (simp only: minus_add add.commute)
   1.337 -  apply (rule HInfinite_add_ge_zero)
   1.338 -    apply simp_all
   1.339 -  done
   1.340 +  by (metis (no_types, lifting) HInfinite_add_ge_zero2 HInfinite_minus_iff add.inverse_distrib_swap neg_0_le_iff_le)
   1.341  
   1.342  lemma HInfinite_add_lt_zero: "x \<in> HInfinite \<Longrightarrow> y < 0 \<Longrightarrow> x < 0 \<Longrightarrow> x + y \<in> HInfinite"
   1.343    for x y :: hypreal
   1.344 @@ -465,17 +471,12 @@
   1.345  
   1.346  lemma lemma_Infinitesimal_hyperpow: "x \<in> Infinitesimal \<Longrightarrow> 0 < N \<Longrightarrow> \<bar>x pow N\<bar> \<le> \<bar>x\<bar>"
   1.347    for x :: hypreal
   1.348 -  apply (unfold Infinitesimal_def)
   1.349 -  apply (auto intro!: hyperpow_Suc_le_self2
   1.350 -      simp: hyperpow_hrabs [symmetric] hypnat_gt_zero_iff2 abs_ge_zero)
   1.351 -  done
   1.352 +  apply (clarsimp simp: Infinitesimal_def)
   1.353 +  by (metis Reals_1 abs_ge_zero hyperpow_Suc_le_self2 hyperpow_hrabs hypnat_gt_zero_iff2 zero_less_one)
   1.354  
   1.355  lemma Infinitesimal_hyperpow: "x \<in> Infinitesimal \<Longrightarrow> 0 < N \<Longrightarrow> x pow N \<in> Infinitesimal"
   1.356    for x :: hypreal
   1.357 -  apply (rule hrabs_le_Infinitesimal)
   1.358 -   apply (rule_tac [2] lemma_Infinitesimal_hyperpow)
   1.359 -  apply auto
   1.360 -  done
   1.361 +  using hrabs_le_Infinitesimal lemma_Infinitesimal_hyperpow by blast
   1.362  
   1.363  lemma hrealpow_hyperpow_Infinitesimal_iff:
   1.364    "(x ^ n \<in> Infinitesimal) \<longleftrightarrow> x pow (hypnat_of_nat n) \<in> Infinitesimal"
   1.365 @@ -488,21 +489,11 @@
   1.366  lemma not_Infinitesimal_mult:
   1.367    "x \<notin> Infinitesimal \<Longrightarrow> y \<notin> Infinitesimal \<Longrightarrow> x * y \<notin> Infinitesimal"
   1.368    for x y :: "'a::real_normed_div_algebra star"
   1.369 -  apply (unfold Infinitesimal_def, clarify, rename_tac r s)
   1.370 -  apply (simp only: linorder_not_less hnorm_mult)
   1.371 -  apply (drule_tac x = "r * s" in bspec)
   1.372 -   apply (fast intro: Reals_mult)
   1.373 -  apply simp
   1.374 -  apply (drule_tac c = s and d = "hnorm y" and a = r and b = "hnorm x" in mult_mono)
   1.375 -     apply simp_all
   1.376 -  done
   1.377 +  by (metis (no_types, lifting) inverse_Infinitesimal_iff_HInfinite ComplI Compl_HFinite Infinitesimal_HFinite_mult divide_inverse eq_divide_imp inverse_inverse_eq mult_zero_right)
   1.378  
   1.379  lemma Infinitesimal_mult_disj: "x * y \<in> Infinitesimal \<Longrightarrow> x \<in> Infinitesimal \<or> y \<in> Infinitesimal"
   1.380    for x y :: "'a::real_normed_div_algebra star"
   1.381 -  apply (rule ccontr)
   1.382 -  apply (drule de_Morgan_disj [THEN iffD1])
   1.383 -  apply (fast dest: not_Infinitesimal_mult)
   1.384 -  done
   1.385 +  using not_Infinitesimal_mult by blast
   1.386  
   1.387  lemma HFinite_Infinitesimal_not_zero: "x \<in> HFinite-Infinitesimal \<Longrightarrow> x \<noteq> 0"
   1.388    by blast
   1.389 @@ -510,16 +501,10 @@
   1.390  lemma HFinite_Infinitesimal_diff_mult:
   1.391    "x \<in> HFinite - Infinitesimal \<Longrightarrow> y \<in> HFinite - Infinitesimal \<Longrightarrow> x * y \<in> HFinite - Infinitesimal"
   1.392    for x y :: "'a::real_normed_div_algebra star"
   1.393 -  apply clarify
   1.394 -  apply (blast dest: HFinite_mult not_Infinitesimal_mult)
   1.395 -  done
   1.396 +  by (simp add: HFinite_mult not_Infinitesimal_mult)
   1.397  
   1.398  lemma Infinitesimal_subset_HFinite: "Infinitesimal \<subseteq> HFinite"
   1.399 -  apply (simp add: Infinitesimal_def HFinite_def)
   1.400 -  apply auto
   1.401 -  apply (rule_tac x = 1 in bexI)
   1.402 -  apply auto
   1.403 -  done
   1.404 +  using HFinite_def InfinitesimalD Reals_1 zero_less_one by blast
   1.405  
   1.406  lemma Infinitesimal_star_of_mult: "x \<in> Infinitesimal \<Longrightarrow> x * star_of r \<in> Infinitesimal"
   1.407    for x :: "'a::real_normed_algebra star"
   1.408 @@ -544,21 +529,19 @@
   1.409  lemma approx_refl [iff]: "x \<approx> x"
   1.410    by (simp add: approx_def Infinitesimal_def)
   1.411  
   1.412 -lemma hypreal_minus_distrib1: "- (y + - x) = x + -y"
   1.413 -  for x y :: "'a::ab_group_add"
   1.414 -  by (simp add: add.commute)
   1.415 +lemma approx_sym: "x \<approx> y \<Longrightarrow> y \<approx> x"
   1.416 +  by (metis Infinitesimal_minus_iff approx_def minus_diff_eq)
   1.417  
   1.418 -lemma approx_sym: "x \<approx> y \<Longrightarrow> y \<approx> x"
   1.419 -  apply (simp add: approx_def)
   1.420 -  apply (drule Infinitesimal_minus_iff [THEN iffD2])
   1.421 -  apply simp
   1.422 -  done
   1.423 -
   1.424 -lemma approx_trans: "x \<approx> y \<Longrightarrow> y \<approx> z \<Longrightarrow> x \<approx> z"
   1.425 -  apply (simp add: approx_def)
   1.426 -  apply (drule (1) Infinitesimal_add)
   1.427 -  apply simp
   1.428 -  done
   1.429 +lemma approx_trans:
   1.430 +  assumes "x \<approx> y" "y \<approx> z" shows "x \<approx> z"
   1.431 +proof -
   1.432 +  have "x - y \<in> Infinitesimal" "z - y \<in> Infinitesimal"
   1.433 +    using assms approx_def approx_sym by auto
   1.434 +  then have "x - z \<in> Infinitesimal"
   1.435 +    using Infinitesimal_diff by force
   1.436 +  then show ?thesis
   1.437 +    by (simp add: approx_def)
   1.438 +qed
   1.439  
   1.440  lemma approx_trans2: "r \<approx> x \<Longrightarrow> s \<approx> x \<Longrightarrow> r \<approx> s"
   1.441    by (blast intro: approx_sym approx_trans)
   1.442 @@ -587,12 +570,11 @@
   1.443    by (simp add: approx_minus_iff [symmetric] mem_infmal_iff)
   1.444  
   1.445  lemma approx_monad_iff: "x \<approx> y \<longleftrightarrow> monad x = monad y"
   1.446 -  by (auto simp add: monad_def dest: approx_sym elim!: approx_trans equalityCE)
   1.447 +  apply (simp add: monad_def set_eq_iff)
   1.448 +  using approx_reorient approx_trans by blast
   1.449  
   1.450  lemma Infinitesimal_approx: "x \<in> Infinitesimal \<Longrightarrow> y \<in> Infinitesimal \<Longrightarrow> x \<approx> y"
   1.451 -  apply (simp add: mem_infmal_iff)
   1.452 -  apply (blast intro: approx_trans approx_sym)
   1.453 -  done
   1.454 +  by (simp add: Infinitesimal_diff approx_def)
   1.455  
   1.456  lemma approx_add: "a \<approx> b \<Longrightarrow> c \<approx> d \<Longrightarrow> a + c \<approx> b + d"
   1.457  proof (unfold approx_def)
   1.458 @@ -604,10 +586,7 @@
   1.459  qed
   1.460  
   1.461  lemma approx_minus: "a \<approx> b \<Longrightarrow> - a \<approx> - b"
   1.462 -  apply (rule approx_minus_iff [THEN iffD2, THEN approx_sym])
   1.463 -  apply (drule approx_minus_iff [THEN iffD1])
   1.464 -  apply (simp add: add.commute)
   1.465 -  done
   1.466 +  by (metis approx_def approx_sym minus_diff_eq minus_diff_minus)
   1.467  
   1.468  lemma approx_minus2: "- a \<approx> - b \<Longrightarrow> a \<approx> b"
   1.469    by (auto dest: approx_minus)
   1.470 @@ -654,16 +633,10 @@
   1.471    by (force simp add: bex_Infinitesimal_iff [symmetric])
   1.472  
   1.473  lemma Infinitesimal_add_approx: "y \<in> Infinitesimal \<Longrightarrow> x + y = z \<Longrightarrow> x \<approx> z"
   1.474 -  apply (rule bex_Infinitesimal_iff [THEN iffD1])
   1.475 -  apply (drule Infinitesimal_minus_iff [THEN iffD2])
   1.476 -  apply (auto simp add: add.assoc [symmetric])
   1.477 -  done
   1.478 +  using approx_sym bex_Infinitesimal_iff2 by blast
   1.479  
   1.480  lemma Infinitesimal_add_approx_self: "y \<in> Infinitesimal \<Longrightarrow> x \<approx> x + y"
   1.481 -  apply (rule bex_Infinitesimal_iff [THEN iffD1])
   1.482 -  apply (drule Infinitesimal_minus_iff [THEN iffD2])
   1.483 -  apply (auto simp add: add.assoc [symmetric])
   1.484 -  done
   1.485 +  by (simp add: Infinitesimal_add_approx)
   1.486  
   1.487  lemma Infinitesimal_add_approx_self2: "y \<in> Infinitesimal \<Longrightarrow> x \<approx> y + x"
   1.488    by (auto dest: Infinitesimal_add_approx_self simp add: add.commute)
   1.489 @@ -672,31 +645,19 @@
   1.490    by (blast intro!: Infinitesimal_add_approx_self Infinitesimal_minus_iff [THEN iffD2])
   1.491  
   1.492  lemma Infinitesimal_add_cancel: "y \<in> Infinitesimal \<Longrightarrow> x + y \<approx> z \<Longrightarrow> x \<approx> z"
   1.493 -  apply (drule_tac x = x in Infinitesimal_add_approx_self [THEN approx_sym])
   1.494 -  apply (erule approx_trans3 [THEN approx_sym], assumption)
   1.495 -  done
   1.496 +  using Infinitesimal_add_approx approx_trans by blast
   1.497  
   1.498  lemma Infinitesimal_add_right_cancel: "y \<in> Infinitesimal \<Longrightarrow> x \<approx> z + y \<Longrightarrow> x \<approx> z"
   1.499 -  apply (drule_tac x = z in Infinitesimal_add_approx_self2 [THEN approx_sym])
   1.500 -  apply (erule approx_trans3 [THEN approx_sym])
   1.501 -  apply (simp add: add.commute)
   1.502 -  apply (erule approx_sym)
   1.503 -  done
   1.504 +  by (metis Infinitesimal_add_approx_self approx_monad_iff)
   1.505  
   1.506 -lemma approx_add_left_cancel: "d + b  \<approx> d + c \<Longrightarrow> b \<approx> c"
   1.507 -  apply (drule approx_minus_iff [THEN iffD1])
   1.508 -  apply (simp add: approx_minus_iff [symmetric] ac_simps)
   1.509 -  done
   1.510 +lemma approx_add_left_cancel: "d + b \<approx> d + c \<Longrightarrow> b \<approx> c"
   1.511 +  by (metis add_diff_cancel_left bex_Infinitesimal_iff)
   1.512  
   1.513  lemma approx_add_right_cancel: "b + d \<approx> c + d \<Longrightarrow> b \<approx> c"
   1.514 -  apply (rule approx_add_left_cancel)
   1.515 -  apply (simp add: add.commute)
   1.516 -  done
   1.517 +  by (simp add: approx_def)
   1.518  
   1.519  lemma approx_add_mono1: "b \<approx> c \<Longrightarrow> d + b \<approx> d + c"
   1.520 -  apply (rule approx_minus_iff [THEN iffD2])
   1.521 -  apply (simp add: approx_minus_iff [symmetric] ac_simps)
   1.522 -  done
   1.523 +  by (simp add: approx_add)
   1.524  
   1.525  lemma approx_add_mono2: "b \<approx> c \<Longrightarrow> b + a \<approx> c + a"
   1.526    by (simp add: add.commute approx_add_mono1)
   1.527 @@ -708,52 +669,41 @@
   1.528    by (simp add: add.commute)
   1.529  
   1.530  lemma approx_HFinite: "x \<in> HFinite \<Longrightarrow> x \<approx> y \<Longrightarrow> y \<in> HFinite"
   1.531 -  apply (drule bex_Infinitesimal_iff2 [THEN iffD2], safe)
   1.532 -  apply (drule Infinitesimal_subset_HFinite [THEN subsetD, THEN HFinite_minus_iff [THEN iffD2]])
   1.533 -  apply (drule HFinite_add)
   1.534 -   apply (auto simp add: add.assoc)
   1.535 -  done
   1.536 +  by (metis HFinite_add Infinitesimal_subset_HFinite approx_sym subsetD bex_Infinitesimal_iff2)
   1.537  
   1.538  lemma approx_star_of_HFinite: "x \<approx> star_of D \<Longrightarrow> x \<in> HFinite"
   1.539    by (rule approx_sym [THEN [2] approx_HFinite], auto)
   1.540  
   1.541  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"
   1.542    for a b c d :: "'a::real_normed_algebra star"
   1.543 -  apply (rule approx_trans)
   1.544 -   apply (rule_tac [2] approx_mult2)
   1.545 -    apply (rule approx_mult1)
   1.546 -     prefer 2 apply (blast intro: approx_HFinite approx_sym, auto)
   1.547 -  done
   1.548 +  by (meson approx_HFinite approx_mult2 approx_mult_subst2 approx_sym)
   1.549  
   1.550  lemma scaleHR_left_diff_distrib: "\<And>a b x. scaleHR (a - b) x = scaleHR a x - scaleHR b x"
   1.551    by transfer (rule scaleR_left_diff_distrib)
   1.552  
   1.553  lemma approx_scaleR1: "a \<approx> star_of b \<Longrightarrow> c \<in> HFinite \<Longrightarrow> scaleHR a c \<approx> b *\<^sub>R c"
   1.554 -  apply (unfold approx_def)
   1.555 -  apply (drule (1) Infinitesimal_HFinite_scaleHR)
   1.556 -  apply (simp only: scaleHR_left_diff_distrib)
   1.557 -  apply (simp add: scaleHR_def star_scaleR_def [symmetric])
   1.558 -  done
   1.559 +  unfolding approx_def
   1.560 +  by (metis Infinitesimal_HFinite_scaleHR scaleHR_def scaleHR_left_diff_distrib star_scaleR_def starfun2_star_of)
   1.561  
   1.562  lemma approx_scaleR2: "a \<approx> b \<Longrightarrow> c *\<^sub>R a \<approx> c *\<^sub>R b"
   1.563    by (simp add: approx_def Infinitesimal_scaleR2 scaleR_right_diff_distrib [symmetric])
   1.564  
   1.565  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"
   1.566 -  apply (rule approx_trans)
   1.567 -   apply (rule_tac [2] approx_scaleR2)
   1.568 -   apply (rule approx_scaleR1)
   1.569 -    prefer 2 apply (blast intro: approx_HFinite approx_sym, auto)
   1.570 -  done
   1.571 +  by (meson approx_HFinite approx_scaleR1 approx_scaleR2 approx_sym approx_trans)
   1.572  
   1.573  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"
   1.574    for a c :: "'a::real_normed_algebra star"
   1.575    by (blast intro!: approx_mult_HFinite approx_star_of_HFinite HFinite_star_of)
   1.576  
   1.577 -lemma approx_SReal_mult_cancel_zero: "a \<in> \<real> \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> a * x \<approx> 0 \<Longrightarrow> x \<approx> 0"
   1.578 -  for a x :: hypreal
   1.579 -  apply (drule Reals_inverse [THEN SReal_subset_HFinite [THEN subsetD]])
   1.580 -  apply (auto dest: approx_mult2 simp add: mult.assoc [symmetric])
   1.581 -  done
   1.582 +lemma approx_SReal_mult_cancel_zero:
   1.583 +  fixes a x :: hypreal
   1.584 +  assumes "a \<in> \<real>" "a \<noteq> 0" "a * x \<approx> 0" shows "x \<approx> 0"
   1.585 +proof -
   1.586 +  have "inverse a \<in> HFinite"
   1.587 +    using Reals_inverse SReal_subset_HFinite assms(1) by blast
   1.588 +  then show ?thesis
   1.589 +    using assms by (auto dest: approx_mult2 simp add: mult.assoc [symmetric])
   1.590 +qed
   1.591  
   1.592  lemma approx_mult_SReal1: "a \<in> \<real> \<Longrightarrow> x \<approx> 0 \<Longrightarrow> x * a \<approx> 0"
   1.593    for a x :: hypreal
   1.594 @@ -767,25 +717,31 @@
   1.595    for a x :: hypreal
   1.596    by (blast intro: approx_SReal_mult_cancel_zero approx_mult_SReal2)
   1.597  
   1.598 -lemma approx_SReal_mult_cancel: "a \<in> \<real> \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> a * w \<approx> a * z \<Longrightarrow> w \<approx> z"
   1.599 -  for a w z :: hypreal
   1.600 -  apply (drule Reals_inverse [THEN SReal_subset_HFinite [THEN subsetD]])
   1.601 -  apply (auto dest: approx_mult2 simp add: mult.assoc [symmetric])
   1.602 -  done
   1.603 +lemma approx_SReal_mult_cancel:
   1.604 +  fixes a w z :: hypreal
   1.605 +  assumes "a \<in> \<real>" "a \<noteq> 0" "a * w \<approx> a * z" shows "w \<approx> z"
   1.606 +proof -
   1.607 +  have "inverse a \<in> HFinite"
   1.608 +    using Reals_inverse SReal_subset_HFinite assms(1) by blast
   1.609 +  then show ?thesis
   1.610 +    using assms by (auto dest: approx_mult2 simp add: mult.assoc [symmetric])
   1.611 +qed
   1.612  
   1.613  lemma approx_SReal_mult_cancel_iff1 [simp]: "a \<in> \<real> \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> a * w \<approx> a * z \<longleftrightarrow> w \<approx> z"
   1.614    for a w z :: hypreal
   1.615 -  by (auto intro!: approx_mult2 SReal_subset_HFinite [THEN subsetD]
   1.616 -      intro: approx_SReal_mult_cancel)
   1.617 +  by (meson SReal_subset_HFinite approx_SReal_mult_cancel approx_mult2 subsetD)
   1.618  
   1.619 -lemma approx_le_bound: "z \<le> f \<Longrightarrow> f \<approx> g \<Longrightarrow> g \<le> z ==> f \<approx> z"
   1.620 -  for z :: hypreal
   1.621 -  apply (simp add: bex_Infinitesimal_iff2 [symmetric], auto)
   1.622 -  apply (rule_tac x = "g + y - z" in bexI)
   1.623 -   apply simp
   1.624 -  apply (rule Infinitesimal_interval2)
   1.625 -     apply (rule_tac [2] Infinitesimal_zero, auto)
   1.626 -  done
   1.627 +lemma approx_le_bound:
   1.628 +  fixes z :: hypreal
   1.629 +  assumes "z \<le> f" " f \<approx> g" "g \<le> z" shows "f \<approx> z"
   1.630 +proof -
   1.631 +  obtain y where "z \<le> g + y" and "y \<in> Infinitesimal" "f = g + y"
   1.632 +    using assms bex_Infinitesimal_iff2 by auto
   1.633 +  then have "z - g \<in> Infinitesimal"
   1.634 +    using assms(3) hrabs_le_Infinitesimal by auto 
   1.635 +  then show ?thesis
   1.636 +    by (metis approx_def approx_trans2 assms(2))
   1.637 +qed
   1.638  
   1.639  lemma approx_hnorm: "x \<approx> y \<Longrightarrow> hnorm x \<approx> hnorm y"
   1.640    for x y :: "'a::real_normed_vector star"
   1.641 @@ -810,9 +766,7 @@
   1.642  
   1.643  lemma Infinitesimal_less_SReal: "x \<in> \<real> \<Longrightarrow> y \<in> Infinitesimal \<Longrightarrow> 0 < x \<Longrightarrow> y < x"
   1.644    for x y :: hypreal
   1.645 -  apply (simp add: Infinitesimal_def)
   1.646 -  apply (rule abs_ge_self [THEN order_le_less_trans], auto)
   1.647 -  done
   1.648 +  using InfinitesimalD by fastforce
   1.649  
   1.650  lemma Infinitesimal_less_SReal2: "y \<in> Infinitesimal \<Longrightarrow> \<forall>r \<in> Reals. 0 < r \<longrightarrow> y < r"
   1.651    for y :: hypreal
   1.652 @@ -820,21 +774,19 @@
   1.653  
   1.654  lemma SReal_not_Infinitesimal: "0 < y \<Longrightarrow> y \<in> \<real> ==> y \<notin> Infinitesimal"
   1.655    for y :: hypreal
   1.656 -  apply (simp add: Infinitesimal_def)
   1.657 -  apply (auto simp add: abs_if)
   1.658 -  done
   1.659 +  by (auto simp add: Infinitesimal_def abs_if)
   1.660  
   1.661  lemma SReal_minus_not_Infinitesimal: "y < 0 \<Longrightarrow> y \<in> \<real> \<Longrightarrow> y \<notin> Infinitesimal"
   1.662    for y :: hypreal
   1.663 -  apply (subst Infinitesimal_minus_iff [symmetric])
   1.664 -  apply (rule SReal_not_Infinitesimal, auto)
   1.665 -  done
   1.666 +  using Infinitesimal_minus_iff Reals_minus SReal_not_Infinitesimal neg_0_less_iff_less by blast
   1.667  
   1.668  lemma SReal_Int_Infinitesimal_zero: "\<real> Int Infinitesimal = {0::hypreal}"
   1.669 -  apply auto
   1.670 -  apply (cut_tac x = x and y = 0 in linorder_less_linear)
   1.671 -  apply (blast dest: SReal_not_Infinitesimal SReal_minus_not_Infinitesimal)
   1.672 -  done
   1.673 +  proof -
   1.674 +  have "x = 0" if "x \<in> \<real>" "x \<in> Infinitesimal" for x :: "real star"
   1.675 +    using that SReal_minus_not_Infinitesimal SReal_not_Infinitesimal not_less_iff_gr_or_eq by blast
   1.676 +  then show ?thesis
   1.677 +    by auto
   1.678 +qed
   1.679  
   1.680  lemma SReal_Infinitesimal_zero: "x \<in> \<real> \<Longrightarrow> x \<in> Infinitesimal \<Longrightarrow> x = 0"
   1.681    for x :: hypreal
   1.682 @@ -849,12 +801,15 @@
   1.683    by (rule SReal_HFinite_diff_Infinitesimal) auto
   1.684  
   1.685  lemma star_of_Infinitesimal_iff_0 [iff]: "star_of x \<in> Infinitesimal \<longleftrightarrow> x = 0"
   1.686 -  apply (auto simp add: Infinitesimal_def)
   1.687 -  apply (drule_tac x="hnorm (star_of x)" in bspec)
   1.688 -   apply (simp add: SReal_def)
   1.689 -   apply (rule_tac x="norm x" in exI, simp)
   1.690 -  apply simp
   1.691 -  done
   1.692 +proof
   1.693 +  show "x = 0" if "star_of x \<in> Infinitesimal"
   1.694 +  proof -
   1.695 +    have "hnorm (star_n (\<lambda>n. x)) \<in> Standard"
   1.696 +      by (metis Reals_eq_Standard SReal_iff star_of_def star_of_norm)
   1.697 +    then show ?thesis
   1.698 +      by (metis InfinitesimalD2 less_irrefl star_of_norm that zero_less_norm_iff)
   1.699 +  qed
   1.700 +qed auto
   1.701  
   1.702  lemma star_of_HFinite_diff_Infinitesimal: "x \<noteq> 0 \<Longrightarrow> star_of x \<in> HFinite - Infinitesimal"
   1.703    by simp
   1.704 @@ -866,39 +821,26 @@
   1.705  text \<open>Again: \<open>1\<close> is a special case, but not \<open>0\<close> this time.\<close>
   1.706  lemma one_not_Infinitesimal [simp]:
   1.707    "(1::'a::{real_normed_vector,zero_neq_one} star) \<notin> Infinitesimal"
   1.708 -  apply (simp only: star_one_def star_of_Infinitesimal_iff_0)
   1.709 -  apply simp
   1.710 -  done
   1.711 +  by (metis star_of_Infinitesimal_iff_0 star_one_def zero_neq_one)
   1.712  
   1.713  lemma approx_SReal_not_zero: "y \<in> \<real> \<Longrightarrow> x \<approx> y \<Longrightarrow> y \<noteq> 0 \<Longrightarrow> x \<noteq> 0"
   1.714    for x y :: hypreal
   1.715 -  apply (cut_tac x = 0 and y = y in linorder_less_linear, simp)
   1.716 -  apply (blast dest: approx_sym [THEN mem_infmal_iff [THEN iffD2]]
   1.717 -      SReal_not_Infinitesimal SReal_minus_not_Infinitesimal)
   1.718 -  done
   1.719 +  using SReal_Infinitesimal_zero approx_sym mem_infmal_iff by auto
   1.720  
   1.721  lemma HFinite_diff_Infinitesimal_approx:
   1.722    "x \<approx> y \<Longrightarrow> y \<in> HFinite - Infinitesimal \<Longrightarrow> x \<in> HFinite - Infinitesimal"
   1.723 -  apply (auto intro: approx_sym [THEN [2] approx_HFinite] simp: mem_infmal_iff)
   1.724 -  apply (drule approx_trans3, assumption)
   1.725 -  apply (blast dest: approx_sym)
   1.726 -  done
   1.727 +  by (meson Diff_iff approx_HFinite approx_sym approx_trans3 mem_infmal_iff)
   1.728  
   1.729  text \<open>The premise \<open>y \<noteq> 0\<close> is essential; otherwise \<open>x / y = 0\<close> and we lose the
   1.730    \<open>HFinite\<close> premise.\<close>
   1.731  lemma Infinitesimal_ratio:
   1.732    "y \<noteq> 0 \<Longrightarrow> y \<in> Infinitesimal \<Longrightarrow> x / y \<in> HFinite \<Longrightarrow> x \<in> Infinitesimal"
   1.733    for x y :: "'a::{real_normed_div_algebra,field} star"
   1.734 -  apply (drule Infinitesimal_HFinite_mult2, assumption)
   1.735 -  apply (simp add: divide_inverse mult.assoc)
   1.736 -  done
   1.737 +  using Infinitesimal_HFinite_mult by fastforce
   1.738  
   1.739  lemma Infinitesimal_SReal_divide: "x \<in> Infinitesimal \<Longrightarrow> y \<in> \<real> \<Longrightarrow> x / y \<in> Infinitesimal"
   1.740    for x y :: hypreal
   1.741 -  apply (simp add: divide_inverse)
   1.742 -  apply (auto intro!: Infinitesimal_HFinite_mult
   1.743 -      dest!: Reals_inverse [THEN SReal_subset_HFinite [THEN subsetD]])
   1.744 -  done
   1.745 +  by (metis HFinite_star_of Infinitesimal_HFinite_mult Reals_inverse SReal_iff divide_inverse)
   1.746  
   1.747  
   1.748  section \<open>Standard Part Theorem\<close>
   1.749 @@ -912,28 +854,15 @@
   1.750  subsection \<open>Uniqueness: Two Infinitely Close Reals are Equal\<close>
   1.751  
   1.752  lemma star_of_approx_iff [simp]: "star_of x \<approx> star_of y \<longleftrightarrow> x = y"
   1.753 -  apply safe
   1.754 -  apply (simp add: approx_def)
   1.755 -  apply (simp only: star_of_diff [symmetric])
   1.756 -  apply (simp only: star_of_Infinitesimal_iff_0)
   1.757 -  apply simp
   1.758 -  done
   1.759 +  by (metis approx_def right_minus_eq star_of_Infinitesimal_iff_0 star_of_simps(2))
   1.760  
   1.761  lemma SReal_approx_iff: "x \<in> \<real> \<Longrightarrow> y \<in> \<real> \<Longrightarrow> x \<approx> y \<longleftrightarrow> x = y"
   1.762    for x y :: hypreal
   1.763 -  apply auto
   1.764 -  apply (simp add: approx_def)
   1.765 -  apply (drule (1) Reals_diff)
   1.766 -  apply (drule (1) SReal_Infinitesimal_zero)
   1.767 -  apply simp
   1.768 -  done
   1.769 +  by (meson Reals_diff SReal_Infinitesimal_zero approx_def approx_refl right_minus_eq)
   1.770  
   1.771  lemma numeral_approx_iff [simp]:
   1.772 -  "(numeral v \<approx> (numeral w :: 'a::{numeral,real_normed_vector} star)) =
   1.773 -    (numeral v = (numeral w :: 'a))"
   1.774 -  apply (unfold star_numeral_def)
   1.775 -  apply (rule star_of_approx_iff)
   1.776 -  done
   1.777 +  "(numeral v \<approx> (numeral w :: 'a::{numeral,real_normed_vector} star)) = (numeral v = (numeral w :: 'a))"
   1.778 +  by (metis star_of_approx_iff star_of_numeral)
   1.779  
   1.780  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>
   1.781  lemma [simp]:
   1.782 @@ -943,10 +872,8 @@
   1.783    "((1::'b::{numeral,one,real_normed_vector} star) \<approx> numeral w) = (numeral w = (1::'b))"
   1.784    "\<not> (0 \<approx> (1::'c::{zero_neq_one,real_normed_vector} star))"
   1.785    "\<not> (1 \<approx> (0::'c::{zero_neq_one,real_normed_vector} star))"
   1.786 -       apply (unfold star_numeral_def star_zero_def star_one_def)
   1.787 -       apply (unfold star_of_approx_iff)
   1.788 -       apply (auto intro: sym)
   1.789 -  done
   1.790 +  unfolding star_numeral_def star_zero_def star_one_def star_of_approx_iff
   1.791 +  by (auto intro: sym)
   1.792  
   1.793  lemma star_of_approx_numeral_iff [simp]: "star_of k \<approx> numeral w \<longleftrightarrow> k = numeral w"
   1.794    by (subst star_of_approx_iff [symmetric]) auto
   1.795 @@ -970,23 +897,19 @@
   1.796    for Q :: "real set" and Y :: real
   1.797    by (simp add: isUb_def setle_def)
   1.798  
   1.799 -lemma hypreal_of_real_isLub1: "isLub \<real> (hypreal_of_real ` Q) (hypreal_of_real Y) \<Longrightarrow> isLub UNIV Q Y"
   1.800 -  for Q :: "real set" and Y :: real
   1.801 -  apply (simp add: isLub_def leastP_def)
   1.802 -  apply (auto intro: hypreal_of_real_isUb_iff [THEN iffD2]
   1.803 -      simp add: hypreal_of_real_isUb_iff setge_def)
   1.804 -  done
   1.805 -
   1.806 -lemma hypreal_of_real_isLub2: "isLub UNIV Q Y \<Longrightarrow> isLub \<real> (hypreal_of_real ` Q) (hypreal_of_real Y)"
   1.807 +lemma hypreal_of_real_isLub_iff:
   1.808 +  "isLub \<real> (hypreal_of_real ` Q) (hypreal_of_real Y) = isLub (UNIV :: real set) Q Y" (is "?lhs = ?rhs")
   1.809    for Q :: "real set" and Y :: real
   1.810 -  apply (auto simp add: isLub_def leastP_def hypreal_of_real_isUb_iff setge_def)
   1.811 -  apply (metis SReal_iff hypreal_of_real_isUb_iff isUbD2a star_of_le)
   1.812 -  done
   1.813 -
   1.814 -lemma hypreal_of_real_isLub_iff:
   1.815 -  "isLub \<real> (hypreal_of_real ` Q) (hypreal_of_real Y) = isLub (UNIV :: real set) Q Y"
   1.816 -  for Q :: "real set" and Y :: real
   1.817 -  by (blast intro: hypreal_of_real_isLub1 hypreal_of_real_isLub2)
   1.818 +proof 
   1.819 +  assume ?lhs
   1.820 +  then show ?rhs
   1.821 +    by (simp add: isLub_def leastP_def) (metis hypreal_of_real_isUb_iff mem_Collect_eq setge_def star_of_le)
   1.822 +next
   1.823 +  assume ?rhs
   1.824 +  then show ?lhs
   1.825 +  apply (simp add: isLub_def leastP_def hypreal_of_real_isUb_iff setge_def)
   1.826 +    by (metis SReal_iff hypreal_of_real_isUb_iff isUb_def star_of_le)
   1.827 +qed
   1.828  
   1.829  lemma lemma_isUb_hypreal_of_real: "isUb \<real> P Y \<Longrightarrow> \<exists>Yo. isUb \<real> P (hypreal_of_real Yo)"
   1.830    by (auto simp add: SReal_iff isUb_def)
   1.831 @@ -994,58 +917,47 @@
   1.832  lemma lemma_isLub_hypreal_of_real: "isLub \<real> P Y \<Longrightarrow> \<exists>Yo. isLub \<real> P (hypreal_of_real Yo)"
   1.833    by (auto simp add: isLub_def leastP_def isUb_def SReal_iff)
   1.834  
   1.835 -lemma lemma_isLub_hypreal_of_real2: "\<exists>Yo. isLub \<real> P (hypreal_of_real Yo) \<Longrightarrow> \<exists>Y. isLub \<real> P Y"
   1.836 -  by (auto simp add: isLub_def leastP_def isUb_def)
   1.837 -
   1.838 -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"
   1.839 -  apply (frule SReal_hypreal_of_real_image)
   1.840 -   apply (auto, drule lemma_isUb_hypreal_of_real)
   1.841 -  apply (auto intro!: reals_complete lemma_isLub_hypreal_of_real2
   1.842 -      simp add: hypreal_of_real_isLub_iff hypreal_of_real_isUb_iff)
   1.843 -  done
   1.844 +lemma SReal_complete:
   1.845 +  fixes P :: "hypreal set"
   1.846 +  assumes "isUb \<real> P Y" "P \<subseteq> \<real>" "P \<noteq> {}"
   1.847 +    shows "\<exists>t. isLub \<real> P t"
   1.848 +proof -
   1.849 +  obtain Q where "P = hypreal_of_real ` Q"
   1.850 +    by (metis \<open>P \<subseteq> \<real>\<close> hypreal_of_real_image subset_imageE)
   1.851 +  then show ?thesis
   1.852 +    by (metis assms(1) \<open>P \<noteq> {}\<close> equals0I hypreal_of_real_isLub_iff hypreal_of_real_isUb_iff image_empty lemma_isUb_hypreal_of_real reals_complete)
   1.853 +qed
   1.854  
   1.855  
   1.856  text \<open>Lemmas about lubs.\<close>
   1.857  
   1.858 -lemma lemma_st_part_ub: "x \<in> HFinite \<Longrightarrow> \<exists>u. isUb \<real> {s. s \<in> \<real> \<and> s < x} u"
   1.859 -  for x :: hypreal
   1.860 -  apply (drule HFiniteD, safe)
   1.861 -  apply (rule exI, rule isUbI)
   1.862 -   apply (auto intro: setleI isUbI simp add: abs_less_iff)
   1.863 -  done
   1.864 -
   1.865 -lemma lemma_st_part_nonempty: "x \<in> HFinite \<Longrightarrow> \<exists>y. y \<in> {s. s \<in> \<real> \<and> s < x}"
   1.866 -  for x :: hypreal
   1.867 -  apply (drule HFiniteD, safe)
   1.868 -  apply (drule Reals_minus)
   1.869 -  apply (rule_tac x = "-t" in exI)
   1.870 -  apply (auto simp add: abs_less_iff)
   1.871 -  done
   1.872 -
   1.873 -lemma lemma_st_part_lub: "x \<in> HFinite \<Longrightarrow> \<exists>t. isLub \<real> {s. s \<in> \<real> \<and> s < x} t"
   1.874 -  for x :: hypreal
   1.875 -  by (blast intro!: SReal_complete lemma_st_part_ub lemma_st_part_nonempty Collect_restrict)
   1.876 +lemma lemma_st_part_lub:
   1.877 +  fixes x :: hypreal
   1.878 +  assumes "x \<in> HFinite"
   1.879 +  shows "\<exists>t. isLub \<real> {s. s \<in> \<real> \<and> s < x} t"
   1.880 +proof -
   1.881 +  obtain t where t: "t \<in> \<real>" "hnorm x < t"
   1.882 +    using HFiniteD assms by blast
   1.883 +  then have "isUb \<real> {s. s \<in> \<real> \<and> s < x} t"
   1.884 +    by (simp add: abs_less_iff isUbI le_less_linear less_imp_not_less setleI)
   1.885 +  moreover have "\<exists>y. y \<in> \<real> \<and> y < x"
   1.886 +    using t by (rule_tac x = "-t" in exI) (auto simp add: abs_less_iff)
   1.887 +  ultimately show ?thesis
   1.888 +    using SReal_complete by fastforce
   1.889 +qed
   1.890  
   1.891  lemma lemma_st_part_le1:
   1.892    "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"
   1.893    for x r t :: hypreal
   1.894 -  apply (frule isLubD1a)
   1.895 -  apply (rule ccontr, drule linorder_not_le [THEN iffD2])
   1.896 -  apply (drule (1) Reals_add)
   1.897 -  apply (drule_tac y = "r + t" in isLubD1 [THEN setleD], auto)
   1.898 -  done
   1.899 +  by (metis (no_types, lifting) Reals_add add.commute isLubD1a isLubD2 less_add_same_cancel2 mem_Collect_eq not_le)
   1.900  
   1.901  lemma hypreal_setle_less_trans: "S *<= x \<Longrightarrow> x < y \<Longrightarrow> S *<= y"
   1.902    for x y :: hypreal
   1.903 -  apply (simp add: setle_def)
   1.904 -  apply (auto dest!: bspec order_le_less_trans intro: order_less_imp_le)
   1.905 -  done
   1.906 +  by (meson le_less_trans less_imp_le setle_def)
   1.907  
   1.908  lemma hypreal_gt_isUb: "isUb R S x \<Longrightarrow> x < y \<Longrightarrow> y \<in> R \<Longrightarrow> isUb R S y"
   1.909    for x y :: hypreal
   1.910 -  apply (simp add: isUb_def)
   1.911 -  apply (blast intro: hypreal_setle_less_trans)
   1.912 -  done
   1.913 +  using hypreal_setle_less_trans isUb_def by blast
   1.914  
   1.915  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"
   1.916    for x y :: hypreal
   1.917 @@ -1053,9 +965,7 @@
   1.918  
   1.919  lemma lemma_minus_le_zero: "t \<le> t + -r \<Longrightarrow> r \<le> 0"
   1.920    for r t :: hypreal
   1.921 -  apply (drule_tac c = "-t" in add_left_mono)
   1.922 -  apply (auto simp add: add.assoc [symmetric])
   1.923 -  done
   1.924 +  by simp
   1.925  
   1.926  lemma lemma_st_part_le2:
   1.927    "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"
   1.928 @@ -1072,9 +982,7 @@
   1.929  lemma lemma_st_part1a:
   1.930    "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"
   1.931    for x r t :: hypreal
   1.932 -  apply (subgoal_tac "x \<le> t + r")
   1.933 -   apply (auto intro: lemma_st_part_le1)
   1.934 -  done
   1.935 +  using lemma_st_part_le1 by fastforce
   1.936  
   1.937  lemma lemma_st_part2a:
   1.938    "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"
   1.939 @@ -1141,46 +1049,28 @@
   1.940  
   1.941  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"
   1.942    for x :: hypreal
   1.943 -  apply (frule lemma_st_part_lub, safe)
   1.944 -  apply (frule isLubD1a)
   1.945 -  apply (blast dest: lemma_st_part_major2)
   1.946 -  done
   1.947 +  by (meson isLubD1a lemma_st_part_lub lemma_st_part_major2)
   1.948  
   1.949  lemma st_part_Ex: "x \<in> HFinite \<Longrightarrow> \<exists>t\<in>Reals. x \<approx> t"
   1.950    for x :: hypreal
   1.951 -  apply (simp add: approx_def Infinitesimal_def)
   1.952 -  apply (drule lemma_st_part_Ex, auto)
   1.953 -  done
   1.954 +  by (metis InfinitesimalI approx_def hypreal_hnorm_def lemma_st_part_Ex)
   1.955  
   1.956  text \<open>There is a unique real infinitely close.\<close>
   1.957  lemma st_part_Ex1: "x \<in> HFinite \<Longrightarrow> \<exists>!t::hypreal. t \<in> \<real> \<and> x \<approx> t"
   1.958 -  apply (drule st_part_Ex, safe)
   1.959 -   apply (drule_tac [2] approx_sym, drule_tac [2] approx_sym, drule_tac [2] approx_sym)
   1.960 -   apply (auto intro!: approx_unique_real)
   1.961 -  done
   1.962 +  by (meson SReal_approx_iff approx_trans2 st_part_Ex)
   1.963  
   1.964  
   1.965  subsection \<open>Finite, Infinite and Infinitesimal\<close>
   1.966  
   1.967  lemma HFinite_Int_HInfinite_empty [simp]: "HFinite Int HInfinite = {}"
   1.968 -  apply (simp add: HFinite_def HInfinite_def)
   1.969 -  apply (auto dest: order_less_trans)
   1.970 -  done
   1.971 +  using Compl_HFinite by blast
   1.972  
   1.973  lemma HFinite_not_HInfinite:
   1.974 -  assumes x: "x \<in> HFinite"
   1.975 -  shows "x \<notin> HInfinite"
   1.976 -proof
   1.977 -  assume x': "x \<in> HInfinite"
   1.978 -  with x have "x \<in> HFinite \<inter> HInfinite" by blast
   1.979 -  then show False by auto
   1.980 -qed
   1.981 +  assumes x: "x \<in> HFinite" shows "x \<notin> HInfinite"
   1.982 +  using Compl_HFinite x by blast
   1.983  
   1.984  lemma not_HFinite_HInfinite: "x \<notin> HFinite \<Longrightarrow> x \<in> HInfinite"
   1.985 -  apply (simp add: HInfinite_def HFinite_def, auto)
   1.986 -  apply (drule_tac x = "r + 1" in bspec)
   1.987 -   apply (auto)
   1.988 -  done
   1.989 +  using Compl_HFinite by blast
   1.990  
   1.991  lemma HInfinite_HFinite_disj: "x \<in> HInfinite \<or> x \<in> HFinite"
   1.992    by (blast intro: not_HFinite_HInfinite)
   1.993 @@ -1191,17 +1081,13 @@
   1.994  lemma HFinite_HInfinite_iff: "x \<in> HFinite \<longleftrightarrow> x \<notin> HInfinite"
   1.995    by (simp add: HInfinite_HFinite_iff)
   1.996  
   1.997 -
   1.998  lemma HInfinite_diff_HFinite_Infinitesimal_disj:
   1.999    "x \<notin> Infinitesimal \<Longrightarrow> x \<in> HInfinite \<or> x \<in> HFinite - Infinitesimal"
  1.1000    by (fast intro: not_HFinite_HInfinite)
  1.1001  
  1.1002  lemma HFinite_inverse: "x \<in> HFinite \<Longrightarrow> x \<notin> Infinitesimal \<Longrightarrow> inverse x \<in> HFinite"
  1.1003    for x :: "'a::real_normed_div_algebra star"
  1.1004 -  apply (subgoal_tac "x \<noteq> 0")
  1.1005 -   apply (cut_tac x = "inverse x" in HInfinite_HFinite_disj)
  1.1006 -   apply (auto dest!: HInfinite_inverse_Infinitesimal simp: nonzero_inverse_inverse_eq)
  1.1007 -  done
  1.1008 +  using HInfinite_inverse_Infinitesimal not_HFinite_HInfinite by force
  1.1009  
  1.1010  lemma HFinite_inverse2: "x \<in> HFinite - Infinitesimal \<Longrightarrow> inverse x \<in> HFinite"
  1.1011    for x :: "'a::real_normed_div_algebra star"
  1.1012 @@ -1210,17 +1096,12 @@
  1.1013  text \<open>Stronger statement possible in fact.\<close>
  1.1014  lemma Infinitesimal_inverse_HFinite: "x \<notin> Infinitesimal \<Longrightarrow> inverse x \<in> HFinite"
  1.1015    for x :: "'a::real_normed_div_algebra star"
  1.1016 -  apply (drule HInfinite_diff_HFinite_Infinitesimal_disj)
  1.1017 -  apply (blast intro: HFinite_inverse HInfinite_inverse_Infinitesimal Infinitesimal_subset_HFinite [THEN subsetD])
  1.1018 -  done
  1.1019 +  using HFinite_HInfinite_iff HInfinite_inverse_Infinitesimal by fastforce
  1.1020  
  1.1021  lemma HFinite_not_Infinitesimal_inverse:
  1.1022    "x \<in> HFinite - Infinitesimal \<Longrightarrow> inverse x \<in> HFinite - Infinitesimal"
  1.1023    for x :: "'a::real_normed_div_algebra star"
  1.1024 -  apply (auto intro: Infinitesimal_inverse_HFinite)
  1.1025 -  apply (drule Infinitesimal_HFinite_mult2, assumption)
  1.1026 -  apply (simp add: not_Infinitesimal_not_zero)
  1.1027 -  done
  1.1028 +  using HFinite_Infinitesimal_not_zero HFinite_inverse2 Infinitesimal_HFinite_mult2 by fastforce
  1.1029  
  1.1030  lemma approx_inverse: "x \<approx> y \<Longrightarrow> y \<in> HFinite - Infinitesimal \<Longrightarrow> inverse x \<approx> inverse y"
  1.1031    for x y :: "'a::real_normed_div_algebra star"
  1.1032 @@ -1245,32 +1126,21 @@
  1.1033  lemma inverse_add_Infinitesimal_approx2:
  1.1034    "x \<in> HFinite - Infinitesimal \<Longrightarrow> h \<in> Infinitesimal \<Longrightarrow> inverse (h + x) \<approx> inverse x"
  1.1035    for x h :: "'a::real_normed_div_algebra star"
  1.1036 -  apply (rule add.commute [THEN subst])
  1.1037 -  apply (blast intro: inverse_add_Infinitesimal_approx)
  1.1038 -  done
  1.1039 +  by (metis add.commute inverse_add_Infinitesimal_approx)
  1.1040  
  1.1041  lemma inverse_add_Infinitesimal_approx_Infinitesimal:
  1.1042    "x \<in> HFinite - Infinitesimal \<Longrightarrow> h \<in> Infinitesimal \<Longrightarrow> inverse (x + h) - inverse x \<approx> h"
  1.1043    for x h :: "'a::real_normed_div_algebra star"
  1.1044 -  apply (rule approx_trans2)
  1.1045 -   apply (auto intro: inverse_add_Infinitesimal_approx
  1.1046 -      simp add: mem_infmal_iff approx_minus_iff [symmetric])
  1.1047 -  done
  1.1048 +  by (meson Infinitesimal_approx bex_Infinitesimal_iff inverse_add_Infinitesimal_approx)
  1.1049  
  1.1050  lemma Infinitesimal_square_iff: "x \<in> Infinitesimal \<longleftrightarrow> x * x \<in> Infinitesimal"
  1.1051    for x :: "'a::real_normed_div_algebra star"
  1.1052 -  apply (auto intro: Infinitesimal_mult)
  1.1053 -  apply (rule ccontr, frule Infinitesimal_inverse_HFinite)
  1.1054 -  apply (frule not_Infinitesimal_not_zero)
  1.1055 -  apply (auto dest: Infinitesimal_HFinite_mult simp add: mult.assoc)
  1.1056 -  done
  1.1057 +  using Infinitesimal_mult Infinitesimal_mult_disj by auto
  1.1058  declare Infinitesimal_square_iff [symmetric, simp]
  1.1059  
  1.1060  lemma HFinite_square_iff [simp]: "x * x \<in> HFinite \<longleftrightarrow> x \<in> HFinite"
  1.1061    for x :: "'a::real_normed_div_algebra star"
  1.1062 -  apply (auto intro: HFinite_mult)
  1.1063 -  apply (auto dest: HInfinite_mult simp add: HFinite_HInfinite_iff)
  1.1064 -  done
  1.1065 +  using HFinite_HInfinite_iff HFinite_mult HInfinite_mult by blast
  1.1066  
  1.1067  lemma HInfinite_square_iff [simp]: "x * x \<in> HInfinite \<longleftrightarrow> x \<in> HInfinite"
  1.1068    for x :: "'a::real_normed_div_algebra star"
  1.1069 @@ -1278,26 +1148,17 @@
  1.1070  
  1.1071  lemma approx_HFinite_mult_cancel: "a \<in> HFinite - Infinitesimal \<Longrightarrow> a * w \<approx> a * z \<Longrightarrow> w \<approx> z"
  1.1072    for a w z :: "'a::real_normed_div_algebra star"
  1.1073 -  apply safe
  1.1074 -  apply (frule HFinite_inverse, assumption)
  1.1075 -  apply (drule not_Infinitesimal_not_zero)
  1.1076 -  apply (auto dest: approx_mult2 simp add: mult.assoc [symmetric])
  1.1077 -  done
  1.1078 +  by (metis DiffD2 Infinitesimal_mult_disj bex_Infinitesimal_iff right_diff_distrib)
  1.1079  
  1.1080  lemma approx_HFinite_mult_cancel_iff1: "a \<in> HFinite - Infinitesimal \<Longrightarrow> a * w \<approx> a * z \<longleftrightarrow> w \<approx> z"
  1.1081    for a w z :: "'a::real_normed_div_algebra star"
  1.1082    by (auto intro: approx_mult2 approx_HFinite_mult_cancel)
  1.1083  
  1.1084  lemma HInfinite_HFinite_add_cancel: "x + y \<in> HInfinite \<Longrightarrow> y \<in> HFinite \<Longrightarrow> x \<in> HInfinite"
  1.1085 -  apply (rule ccontr)
  1.1086 -  apply (drule HFinite_HInfinite_iff [THEN iffD2])
  1.1087 -  apply (auto dest: HFinite_add simp add: HInfinite_HFinite_iff)
  1.1088 -  done
  1.1089 +  using HFinite_add HInfinite_HFinite_iff by blast
  1.1090  
  1.1091  lemma HInfinite_HFinite_add: "x \<in> HInfinite \<Longrightarrow> y \<in> HFinite \<Longrightarrow> x + y \<in> HInfinite"
  1.1092 -  apply (rule_tac y = "-y" in HInfinite_HFinite_add_cancel)
  1.1093 -   apply (auto simp add: add.assoc HFinite_minus_iff)
  1.1094 -  done
  1.1095 +  by (metis (no_types, hide_lams) HFinite_HInfinite_iff HFinite_add HFinite_minus_iff add.commute add_minus_cancel)
  1.1096  
  1.1097  lemma HInfinite_ge_HInfinite: "x \<in> HInfinite \<Longrightarrow> x \<le> y \<Longrightarrow> 0 \<le> x \<Longrightarrow> y \<in> HInfinite"
  1.1098    for x y :: hypreal
  1.1099 @@ -1305,30 +1166,17 @@
  1.1100  
  1.1101  lemma Infinitesimal_inverse_HInfinite: "x \<in> Infinitesimal \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> inverse x \<in> HInfinite"
  1.1102    for x :: "'a::real_normed_div_algebra star"
  1.1103 -  apply (rule ccontr, drule HFinite_HInfinite_iff [THEN iffD2])
  1.1104 -  apply (auto dest: Infinitesimal_HFinite_mult2)
  1.1105 -  done
  1.1106 +  by (metis Infinitesimal_HFinite_mult not_HFinite_HInfinite one_not_Infinitesimal right_inverse)
  1.1107  
  1.1108  lemma HInfinite_HFinite_not_Infinitesimal_mult:
  1.1109    "x \<in> HInfinite \<Longrightarrow> y \<in> HFinite - Infinitesimal \<Longrightarrow> x * y \<in> HInfinite"
  1.1110    for x y :: "'a::real_normed_div_algebra star"
  1.1111 -  apply (rule ccontr, drule HFinite_HInfinite_iff [THEN iffD2])
  1.1112 -  apply (frule HFinite_Infinitesimal_not_zero)
  1.1113 -  apply (drule HFinite_not_Infinitesimal_inverse)
  1.1114 -  apply (safe, drule HFinite_mult)
  1.1115 -   apply (auto simp add: mult.assoc HFinite_HInfinite_iff)
  1.1116 -  done
  1.1117 +  by (metis (no_types, hide_lams) HFinite_HInfinite_iff HFinite_Infinitesimal_not_zero HFinite_inverse2 HFinite_mult mult.assoc mult.right_neutral right_inverse)
  1.1118  
  1.1119  lemma HInfinite_HFinite_not_Infinitesimal_mult2:
  1.1120    "x \<in> HInfinite \<Longrightarrow> y \<in> HFinite - Infinitesimal \<Longrightarrow> y * x \<in> HInfinite"
  1.1121    for x y :: "'a::real_normed_div_algebra star"
  1.1122 -  apply (rule ccontr, drule HFinite_HInfinite_iff [THEN iffD2])
  1.1123 -  apply (frule HFinite_Infinitesimal_not_zero)
  1.1124 -  apply (drule HFinite_not_Infinitesimal_inverse)
  1.1125 -  apply (safe, drule_tac x="inverse y" in HFinite_mult)
  1.1126 -   apply assumption
  1.1127 -  apply (auto simp add: mult.assoc [symmetric] HFinite_HInfinite_iff)
  1.1128 -  done
  1.1129 +  by (metis Diff_iff HInfinite_HFinite_iff HInfinite_inverse_Infinitesimal Infinitesimal_HFinite_mult2 divide_inverse mult_zero_right nonzero_eq_divide_eq)
  1.1130  
  1.1131  lemma HInfinite_gt_SReal: "x \<in> HInfinite \<Longrightarrow> 0 < x \<Longrightarrow> y \<in> \<real> \<Longrightarrow> y < x"
  1.1132    for x y :: hypreal
  1.1133 @@ -1338,7 +1186,6 @@
  1.1134    for x :: hypreal
  1.1135    by (auto intro: HInfinite_gt_SReal)
  1.1136  
  1.1137 -
  1.1138  lemma not_HInfinite_one [simp]: "1 \<notin> HInfinite"
  1.1139    by (simp add: HInfinite_HFinite_iff)
  1.1140  
  1.1141 @@ -1379,9 +1226,7 @@
  1.1142    by (simp (no_asm)) (simp add: approx_monad_iff)
  1.1143  
  1.1144  lemma approx_subset_monad2: "x \<approx> y \<Longrightarrow> {x, y} \<le> monad y"
  1.1145 -  apply (drule approx_sym)
  1.1146 -  apply (fast dest: approx_subset_monad)
  1.1147 -  done
  1.1148 +  using approx_subset_monad approx_sym by auto
  1.1149  
  1.1150  lemma mem_monad_approx: "u \<in> monad x \<Longrightarrow> x \<approx> u"
  1.1151    by (simp add: monad_def)
  1.1152 @@ -1390,28 +1235,18 @@
  1.1153    by (simp add: monad_def)
  1.1154  
  1.1155  lemma approx_mem_monad2: "x \<approx> u \<Longrightarrow> x \<in> monad u"
  1.1156 -  apply (simp add: monad_def)
  1.1157 -  apply (blast intro!: approx_sym)
  1.1158 -  done
  1.1159 +  using approx_mem_monad approx_sym by blast
  1.1160  
  1.1161  lemma approx_mem_monad_zero: "x \<approx> y \<Longrightarrow> x \<in> monad 0 \<Longrightarrow> y \<in> monad 0"
  1.1162 -  apply (drule mem_monad_approx)
  1.1163 -  apply (fast intro: approx_mem_monad approx_trans)
  1.1164 -  done
  1.1165 +  using approx_trans monad_def by blast
  1.1166  
  1.1167  lemma Infinitesimal_approx_hrabs: "x \<approx> y \<Longrightarrow> x \<in> Infinitesimal \<Longrightarrow> \<bar>x\<bar> \<approx> \<bar>y\<bar>"
  1.1168    for x y :: hypreal
  1.1169 -  apply (drule Infinitesimal_monad_zero_iff [THEN iffD1])
  1.1170 -  apply (blast intro: approx_mem_monad_zero monad_zero_hrabs_iff [THEN iffD1]
  1.1171 -      mem_monad_approx approx_trans3)
  1.1172 -  done
  1.1173 +  using approx_hnorm by fastforce
  1.1174  
  1.1175  lemma less_Infinitesimal_less: "0 < x \<Longrightarrow> x \<notin> Infinitesimal \<Longrightarrow> e \<in> Infinitesimal \<Longrightarrow> e < x"
  1.1176    for x :: hypreal
  1.1177 -  apply (rule ccontr)
  1.1178 -  apply (auto intro: Infinitesimal_zero [THEN [2] Infinitesimal_interval]
  1.1179 -      dest!: order_le_imp_less_or_eq simp add: linorder_not_less)
  1.1180 -  done
  1.1181 +  using Infinitesimal_interval less_linear by blast
  1.1182  
  1.1183  lemma Ball_mem_monad_gt_zero: "0 < x \<Longrightarrow> x \<notin> Infinitesimal \<Longrightarrow> u \<in> monad x \<Longrightarrow> 0 < u"
  1.1184    for u x :: hypreal
  1.1185 @@ -1454,18 +1289,12 @@
  1.1186  lemma hrabs_add_Infinitesimal_cancel:
  1.1187    "e \<in> Infinitesimal \<Longrightarrow> e' \<in> Infinitesimal \<Longrightarrow> \<bar>x + e\<bar> = \<bar>y + e'\<bar> \<Longrightarrow> \<bar>x\<bar> \<approx> \<bar>y\<bar>"
  1.1188    for e e' x y :: hypreal
  1.1189 -  apply (drule_tac x = x in approx_hrabs_add_Infinitesimal)
  1.1190 -  apply (drule_tac x = y in approx_hrabs_add_Infinitesimal)
  1.1191 -  apply (auto intro: approx_trans2)
  1.1192 -  done
  1.1193 +  by (metis approx_hrabs_add_Infinitesimal approx_trans2)
  1.1194  
  1.1195  lemma hrabs_add_minus_Infinitesimal_cancel:
  1.1196    "e \<in> Infinitesimal \<Longrightarrow> e' \<in> Infinitesimal \<Longrightarrow> \<bar>x + -e\<bar> = \<bar>y + -e'\<bar> \<Longrightarrow> \<bar>x\<bar> \<approx> \<bar>y\<bar>"
  1.1197    for e e' x y :: hypreal
  1.1198 -  apply (drule_tac x = x in approx_hrabs_add_minus_Infinitesimal)
  1.1199 -  apply (drule_tac x = y in approx_hrabs_add_minus_Infinitesimal)
  1.1200 -  apply (auto intro: approx_trans2)
  1.1201 -  done
  1.1202 +  by (meson Infinitesimal_minus_iff hrabs_add_Infinitesimal_cancel)
  1.1203  
  1.1204  
  1.1205  subsection \<open>More \<^term>\<open>HFinite\<close> and \<^term>\<open>Infinitesimal\<close> Theorems\<close>
  1.1206 @@ -1493,9 +1322,7 @@
  1.1207  lemma Infinitesimal_add_hrabs_hypreal_of_real_less2:
  1.1208    "x \<in> Infinitesimal \<Longrightarrow> \<bar>hypreal_of_real r\<bar> < hypreal_of_real y \<Longrightarrow>
  1.1209      \<bar>x + hypreal_of_real r\<bar> < hypreal_of_real y"
  1.1210 -  apply (rule add.commute [THEN subst])
  1.1211 -  apply (erule Infinitesimal_add_hrabs_hypreal_of_real_less, assumption)
  1.1212 -  done
  1.1213 +  using Infinitesimal_add_hrabs_hypreal_of_real_less by fastforce
  1.1214  
  1.1215  lemma hypreal_of_real_le_add_Infininitesimal_cancel:
  1.1216    "u \<in> Infinitesimal \<Longrightarrow> v \<in> Infinitesimal \<Longrightarrow>
  1.1217 @@ -1513,10 +1340,7 @@
  1.1218  
  1.1219  lemma hypreal_of_real_less_Infinitesimal_le_zero:
  1.1220    "hypreal_of_real x < e \<Longrightarrow> e \<in> Infinitesimal \<Longrightarrow> hypreal_of_real x \<le> 0"
  1.1221 -  apply (rule linorder_not_less [THEN iffD1], safe)
  1.1222 -  apply (drule Infinitesimal_interval)
  1.1223 -     apply (drule_tac [4] SReal_hypreal_of_real [THEN SReal_Infinitesimal_zero], auto)
  1.1224 -  done
  1.1225 +  by (metis Infinitesimal_interval eq_iff le_less_linear star_of_Infinitesimal_iff_0 star_of_eq_0)
  1.1226  
  1.1227  (*used once, in Lim/NSDERIV_inverse*)
  1.1228  lemma Infinitesimal_add_not_zero: "h \<in> Infinitesimal \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> star_of x + h \<noteq> 0"
  1.1229 @@ -1527,16 +1351,11 @@
  1.1230  
  1.1231  lemma Infinitesimal_square_cancel [simp]: "x * x + y * y \<in> Infinitesimal \<Longrightarrow> x * x \<in> Infinitesimal"
  1.1232    for x y :: hypreal
  1.1233 -  apply (rule Infinitesimal_interval2)
  1.1234 -     apply (rule_tac [3] zero_le_square, assumption)
  1.1235 -   apply auto
  1.1236 -  done
  1.1237 +  by (meson Infinitesimal_interval2 le_add_same_cancel1 not_Infinitesimal_not_zero zero_le_square)
  1.1238  
  1.1239  lemma HFinite_square_cancel [simp]: "x * x + y * y \<in> HFinite \<Longrightarrow> x * x \<in> HFinite"
  1.1240    for x y :: hypreal
  1.1241 -  apply (rule HFinite_bounded, assumption)
  1.1242 -   apply auto
  1.1243 -  done
  1.1244 +  using HFinite_bounded le_add_same_cancel1 zero_le_square by blast
  1.1245  
  1.1246  lemma Infinitesimal_square_cancel2 [simp]: "x * x + y * y \<in> Infinitesimal \<Longrightarrow> y * y \<in> Infinitesimal"
  1.1247    for x y :: hypreal
  1.1248 @@ -1596,27 +1415,16 @@
  1.1249    done
  1.1250  
  1.1251  lemma monad_hrabs_less: "y \<in> monad x \<Longrightarrow> 0 < hypreal_of_real e \<Longrightarrow> \<bar>y - x\<bar> < hypreal_of_real e"
  1.1252 -  apply (drule mem_monad_approx [THEN approx_sym])
  1.1253 -  apply (drule bex_Infinitesimal_iff [THEN iffD2])
  1.1254 -  apply (auto dest!: InfinitesimalD)
  1.1255 -  done
  1.1256 +  by (simp add: Infinitesimal_approx_minus approx_sym less_Infinitesimal_less mem_monad_approx)
  1.1257  
  1.1258  lemma mem_monad_SReal_HFinite: "x \<in> monad (hypreal_of_real  a) \<Longrightarrow> x \<in> HFinite"
  1.1259 -  apply (drule mem_monad_approx [THEN approx_sym])
  1.1260 -  apply (drule bex_Infinitesimal_iff2 [THEN iffD2])
  1.1261 -  apply (safe dest!: Infinitesimal_subset_HFinite [THEN subsetD])
  1.1262 -  apply (erule SReal_hypreal_of_real [THEN SReal_subset_HFinite [THEN subsetD], THEN HFinite_add])
  1.1263 -  done
  1.1264 +  using HFinite_star_of approx_HFinite mem_monad_approx by blast
  1.1265  
  1.1266  
  1.1267  subsection \<open>Theorems about Standard Part\<close>
  1.1268  
  1.1269  lemma st_approx_self: "x \<in> HFinite \<Longrightarrow> st x \<approx> x"
  1.1270 -  apply (simp add: st_def)
  1.1271 -  apply (frule st_part_Ex, safe)
  1.1272 -  apply (rule someI2)
  1.1273 -   apply (auto intro: approx_sym)
  1.1274 -  done
  1.1275 +  by (metis (no_types, lifting) approx_refl approx_trans3 someI_ex st_def st_part_Ex st_part_Ex1)
  1.1276  
  1.1277  lemma st_SReal: "x \<in> HFinite \<Longrightarrow> st x \<in> \<real>"
  1.1278    apply (simp add: st_def)
  1.1279 @@ -1813,9 +1621,6 @@
  1.1280    for u :: real
  1.1281    by auto
  1.1282  
  1.1283 -lemma lemma_Int_HIa: "{n. u < norm (X n)} \<inter> {n. norm (X n) < u} = {}"
  1.1284 -  by (auto intro: order_less_asym)
  1.1285 -
  1.1286  lemma FreeUltrafilterNat_HInfinite:
  1.1287    "\<forall>u. eventually (\<lambda>n. u < norm (X n)) \<U> \<Longrightarrow> star_n X \<in> HInfinite"
  1.1288    apply (rule HInfinite_HFinite_iff [THEN iffD2])
  1.1289 @@ -1862,9 +1667,7 @@
  1.1290  text \<open>Infinitesimals as smaller than \<open>1/n\<close> for all \<open>n::nat (> 0)\<close>.\<close>
  1.1291  
  1.1292  lemma lemma_Infinitesimal: "(\<forall>r. 0 < r \<longrightarrow> x < r) \<longleftrightarrow> (\<forall>n. x < inverse (real (Suc n)))"
  1.1293 -  apply (auto simp del: of_nat_Suc)
  1.1294 -  apply (blast dest!: reals_Archimedean intro: order_less_trans)
  1.1295 -  done
  1.1296 +  by (meson inverse_positive_iff_positive less_trans of_nat_0_less_iff reals_Archimedean zero_less_Suc)
  1.1297  
  1.1298  lemma lemma_Infinitesimal2:
  1.1299    "(\<forall>r \<in> Reals. 0 < r \<longrightarrow> x < r) \<longleftrightarrow> (\<forall>n. x < inverse(hypreal_of_nat (Suc n)))"
  1.1300 @@ -1881,9 +1684,7 @@
  1.1301  
  1.1302  lemma Infinitesimal_hypreal_of_nat_iff:
  1.1303    "Infinitesimal = {x. \<forall>n. hnorm x < inverse (hypreal_of_nat (Suc n))}"
  1.1304 -  apply (simp add: Infinitesimal_def)
  1.1305 -  apply (auto simp add: lemma_Infinitesimal2)
  1.1306 -  done
  1.1307 +  using Infinitesimal_def lemma_Infinitesimal2 by auto
  1.1308  
  1.1309  
  1.1310  subsection \<open>Proof that \<open>\<omega>\<close> is an infinite number\<close>
  1.1311 @@ -1905,11 +1706,8 @@
  1.1312    apply (auto dest: order_less_trans)
  1.1313    done
  1.1314  
  1.1315 -lemma lemma_real_le_Un_eq: "{n. f n \<le> u} = {n. f n < u} \<union> {n. u = (f n :: real)}"
  1.1316 -  by (auto dest: order_le_imp_less_or_eq simp add: order_less_imp_le)
  1.1317 -
  1.1318  lemma finite_real_of_nat_le_real: "finite {n::nat. real n \<le> u}"
  1.1319 -  by (auto simp add: lemma_real_le_Un_eq lemma_finite_omega_set finite_real_of_nat_less_real)
  1.1320 +  by (metis infinite_nat_iff_unbounded leD le_nat_floor mem_Collect_eq)
  1.1321  
  1.1322  lemma finite_rabs_real_of_nat_le_real: "finite {n::nat. \<bar>real n\<bar> \<le> u}"
  1.1323    by (simp add: finite_real_of_nat_le_real)
  1.1324 @@ -1927,9 +1725,6 @@
  1.1325  text \<open>The complement of \<open>{n. \<bar>real n\<bar> \<le> u} = {n. u < \<bar>real n\<bar>}\<close> is in
  1.1326    \<open>\<U>\<close> by property of (free) ultrafilters.\<close>
  1.1327  
  1.1328 -lemma Compl_real_le_eq: "- {n::nat. real n \<le> u} = {n. u < real n}"
  1.1329 -  by (auto dest!: order_le_less_trans simp add: linorder_not_le)
  1.1330 -
  1.1331  text \<open>\<^term>\<open>\<omega>\<close> is a member of \<^term>\<open>HInfinite\<close>.\<close>
  1.1332  theorem HInfinite_omega [simp]: "\<omega> \<in> HInfinite"
  1.1333    apply (simp add: omega_def)
  1.1334 @@ -1955,12 +1750,7 @@
  1.1335  text \<open>Needed for proof that we define a hyperreal \<open>[<X(n)] \<approx> hypreal_of_real a\<close> given
  1.1336    that \<open>\<forall>n. |X n - a| < 1/n\<close>. Used in proof of \<open>NSLIM \<Rightarrow> LIM\<close>.\<close>
  1.1337  lemma real_of_nat_less_inverse_iff: "0 < u \<Longrightarrow> u < inverse (real(Suc n)) \<longleftrightarrow> real(Suc n) < inverse u"
  1.1338 -  apply (simp add: inverse_eq_divide)
  1.1339 -  apply (subst pos_less_divide_eq, assumption)
  1.1340 -  apply (subst pos_less_divide_eq)
  1.1341 -   apply simp
  1.1342 -  apply (simp add: mult.commute)
  1.1343 -  done
  1.1344 +  using less_imp_inverse_less by force
  1.1345  
  1.1346  lemma finite_inverse_real_of_posnat_gt_real: "0 < u \<Longrightarrow> finite {n. u < inverse (real (Suc n))}"
  1.1347  proof (simp only: real_of_nat_less_inverse_iff)