more tidying and de-applying
authorpaulson <lp15@cam.ac.uk>
Wed May 01 14:38:42 2019 +0100 (6 months ago)
changeset 702243706106c2e0f
parent 70223 13f8f89f5c41
child 70225 129757af1096
more tidying and de-applying
src/HOL/Nonstandard_Analysis/NSA.thy
src/HOL/Nonstandard_Analysis/Star.thy
     1.1 --- a/src/HOL/Nonstandard_Analysis/NSA.thy	Tue Apr 30 22:44:06 2019 +0100
     1.2 +++ b/src/HOL/Nonstandard_Analysis/NSA.thy	Wed May 01 14:38:42 2019 +0100
     1.3 @@ -428,17 +428,9 @@
     1.4    for x y :: hypreal
     1.5    by (blast intro: HInfinite_add_le_zero order_less_imp_le)
     1.6  
     1.7 -lemma HFinite_sum_squares:
     1.8 -  "a \<in> HFinite \<Longrightarrow> b \<in> HFinite \<Longrightarrow> c \<in> HFinite \<Longrightarrow> a * a + b * b + c * c \<in> HFinite"
     1.9 -  for a b c :: "'a::real_normed_algebra star"
    1.10 -  by (auto intro: HFinite_mult HFinite_add)
    1.11 -
    1.12  lemma not_Infinitesimal_not_zero: "x \<notin> Infinitesimal \<Longrightarrow> x \<noteq> 0"
    1.13    by auto
    1.14  
    1.15 -lemma not_Infinitesimal_not_zero2: "x \<in> HFinite - Infinitesimal \<Longrightarrow> x \<noteq> 0"
    1.16 -  by auto
    1.17 -
    1.18  lemma HFinite_diff_Infinitesimal_hrabs:
    1.19    "x \<in> HFinite - Infinitesimal \<Longrightarrow> \<bar>x\<bar> \<in> HFinite - Infinitesimal"
    1.20    for x :: hypreal
    1.21 @@ -898,7 +890,7 @@
    1.22    by (simp add: isUb_def setle_def)
    1.23  
    1.24  lemma hypreal_of_real_isLub_iff:
    1.25 -  "isLub \<real> (hypreal_of_real ` Q) (hypreal_of_real Y) = isLub (UNIV :: real set) Q Y" (is "?lhs = ?rhs")
    1.26 +  "isLub \<real> (hypreal_of_real ` Q) (hypreal_of_real Y) = isLub (UNIV :: real set) Q Y"  (is "?lhs = ?rhs")
    1.27    for Q :: "real set" and Y :: real
    1.28  proof 
    1.29    assume ?lhs
    1.30 @@ -946,11 +938,6 @@
    1.31      using SReal_complete by fastforce
    1.32  qed
    1.33  
    1.34 -lemma lemma_st_part_le1:
    1.35 -  "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.36 -  for x r t :: hypreal
    1.37 -  by (metis (no_types, lifting) Reals_add add.commute isLubD1a isLubD2 less_add_same_cancel2 mem_Collect_eq not_le)
    1.38 -
    1.39  lemma hypreal_setle_less_trans: "S *<= x \<Longrightarrow> x < y \<Longrightarrow> S *<= y"
    1.40    for x y :: hypreal
    1.41    by (meson le_less_trans less_imp_le setle_def)
    1.42 @@ -959,85 +946,65 @@
    1.43    for x y :: hypreal
    1.44    using hypreal_setle_less_trans isUb_def by blast
    1.45  
    1.46 -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.47 -  for x y :: hypreal
    1.48 -  by (auto dest: order_less_trans intro: order_less_imp_le intro!: isUbI setleI)
    1.49 -
    1.50 -lemma lemma_minus_le_zero: "t \<le> t + -r \<Longrightarrow> r \<le> 0"
    1.51 -  for r t :: hypreal
    1.52 -  by simp
    1.53 -
    1.54 -lemma lemma_st_part_le2:
    1.55 -  "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.56 -  for x r t :: hypreal
    1.57 -  apply (frule isLubD1a)
    1.58 -  apply (rule ccontr, drule linorder_not_le [THEN iffD1])
    1.59 -  apply (drule Reals_minus, drule_tac a = t in Reals_add, assumption)
    1.60 -  apply (drule lemma_st_part_gt_ub, assumption+)
    1.61 -  apply (drule isLub_le_isUb, assumption)
    1.62 -  apply (drule lemma_minus_le_zero)
    1.63 -  apply (auto dest: order_less_le_trans)
    1.64 -  done
    1.65 -
    1.66 -lemma lemma_st_part1a:
    1.67 -  "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.68 -  for x r t :: hypreal
    1.69 -  using lemma_st_part_le1 by fastforce
    1.70 -
    1.71 -lemma lemma_st_part2a:
    1.72 -  "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.73 -  for x r t :: hypreal
    1.74 -  apply (subgoal_tac "(t + -r \<le> x)")
    1.75 -   apply simp
    1.76 -  apply (rule lemma_st_part_le2)
    1.77 -     apply auto
    1.78 -  done
    1.79 -
    1.80  lemma lemma_SReal_ub: "x \<in> \<real> \<Longrightarrow> isUb \<real> {s. s \<in> \<real> \<and> s < x} x"
    1.81    for x :: hypreal
    1.82    by (auto intro: isUbI setleI order_less_imp_le)
    1.83  
    1.84 -lemma lemma_SReal_lub: "x \<in> \<real> \<Longrightarrow> isLub \<real> {s. s \<in> \<real> \<and> s < x} x"
    1.85 -  for x :: hypreal
    1.86 -  apply (auto intro!: isLubI2 lemma_SReal_ub setgeI)
    1.87 -  apply (frule isUbD2a)
    1.88 -  apply (rule_tac x = x and y = y in linorder_cases)
    1.89 -    apply (auto intro!: order_less_imp_le)
    1.90 -  apply (drule SReal_dense, assumption, assumption, safe)
    1.91 -  apply (drule_tac y = r in isUbD)
    1.92 -   apply (auto dest: order_less_le_trans)
    1.93 -  done
    1.94 -
    1.95 -lemma lemma_st_part_not_eq1:
    1.96 -  "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"
    1.97 -  for x r t :: hypreal
    1.98 -  apply auto
    1.99 -  apply (frule isLubD1a [THEN Reals_minus])
   1.100 -  using Reals_add_cancel [of x "- t"] apply simp
   1.101 -  apply (drule_tac x = x in lemma_SReal_lub)
   1.102 -  apply (drule isLub_unique, assumption, auto)
   1.103 -  done
   1.104 -
   1.105 -lemma lemma_st_part_not_eq2:
   1.106 -  "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"
   1.107 -  for x r t :: hypreal
   1.108 -  apply (auto)
   1.109 -  apply (frule isLubD1a)
   1.110 -  using Reals_add_cancel [of "- x" t] apply simp
   1.111 -  apply (drule_tac x = x in lemma_SReal_lub)
   1.112 -  apply (drule isLub_unique, assumption, auto)
   1.113 -  done
   1.114 +lemma lemma_SReal_lub: 
   1.115 +  fixes x :: hypreal
   1.116 +  assumes "x \<in> \<real>" shows "isLub \<real> {s. s \<in> \<real> \<and> s < x} x"
   1.117 +proof -
   1.118 +  have "x \<le> y" if "isUb \<real> {s \<in> \<real>. s < x} y" for y
   1.119 +  proof -
   1.120 +    have "y \<in> \<real>"
   1.121 +      using isUbD2a that by blast
   1.122 +    show ?thesis
   1.123 +    proof (cases x y rule: linorder_cases)
   1.124 +      case greater
   1.125 +      then obtain r where "y < r" "r < x"
   1.126 +        using dense by blast
   1.127 +      then show ?thesis
   1.128 +        using isUbD [OF that] apply (simp add: )
   1.129 +        by (meson SReal_dense \<open>y \<in> \<real>\<close> assms greater not_le)
   1.130 +    qed auto
   1.131 +  qed
   1.132 +  with assms show ?thesis
   1.133 +    by (simp add: isLubI2 isUbI setgeI setleI)
   1.134 +qed
   1.135  
   1.136  lemma lemma_st_part_major:
   1.137 -  "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"
   1.138 -  for x r t :: hypreal
   1.139 -  apply (frule lemma_st_part1a)
   1.140 -     apply (frule_tac [4] lemma_st_part2a, auto)
   1.141 -  apply (drule order_le_imp_less_or_eq)+
   1.142 -  apply auto
   1.143 -  using lemma_st_part_not_eq2 apply fastforce
   1.144 -  using lemma_st_part_not_eq1 apply fastforce
   1.145 -  done
   1.146 +  fixes x r t :: hypreal
   1.147 +  assumes x: "x \<in> HFinite" and r: "r \<in> \<real>" "0 < r" and t: "isLub \<real> {s. s \<in> \<real> \<and> s < x} t"
   1.148 +  shows "\<bar>x - t\<bar> < r"
   1.149 +proof -
   1.150 +  have "t \<in> \<real>"
   1.151 +    using isLubD1a t by blast
   1.152 +  have lemma_st_part_gt_ub: "x < r \<Longrightarrow> r \<in> \<real> \<Longrightarrow> isUb \<real> {s. s \<in> \<real> \<and> s < x} r"
   1.153 +    for  r :: hypreal
   1.154 +    by (auto dest: order_less_trans intro: order_less_imp_le intro!: isUbI setleI)
   1.155 +
   1.156 +  have "isUb \<real> {s \<in> \<real>. s < x} t"
   1.157 +    by (simp add: t isLub_isUb)
   1.158 +  then have "\<not> r + t < x"
   1.159 +    by (metis (mono_tags, lifting) Reals_add \<open>t \<in> \<real>\<close> add_le_same_cancel2 isUbD leD mem_Collect_eq r)
   1.160 +  then have "x - t \<le> r"
   1.161 +    by simp
   1.162 +  moreover have "\<not> x < t - r"
   1.163 +    using lemma_st_part_gt_ub isLub_le_isUb \<open>t \<in> \<real>\<close> r t x by fastforce
   1.164 +  then have "- (x - t) \<le> r"
   1.165 +    by linarith
   1.166 +  moreover have False if "x - t = r \<or> - (x - t) = r"
   1.167 +  proof -
   1.168 +    have "x \<in> \<real>"
   1.169 +      by (metis \<open>t \<in> \<real>\<close> \<open>r \<in> \<real>\<close> that Reals_add_cancel Reals_minus_iff add_uminus_conv_diff)
   1.170 +    then have "isLub \<real> {s \<in> \<real>. s < x} x"
   1.171 +      by (rule lemma_SReal_lub)
   1.172 +    then show False
   1.173 +      using r t that x isLub_unique by force
   1.174 +  qed
   1.175 +  ultimately show ?thesis
   1.176 +    using abs_less_iff dual_order.order_iff_strict by blast
   1.177 +qed
   1.178  
   1.179  lemma lemma_st_part_major2:
   1.180    "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"
   1.181 @@ -1103,16 +1070,19 @@
   1.182    for x :: "'a::real_normed_div_algebra star"
   1.183    using HFinite_Infinitesimal_not_zero HFinite_inverse2 Infinitesimal_HFinite_mult2 by fastforce
   1.184  
   1.185 -lemma approx_inverse: "x \<approx> y \<Longrightarrow> y \<in> HFinite - Infinitesimal \<Longrightarrow> inverse x \<approx> inverse y"
   1.186 -  for x y :: "'a::real_normed_div_algebra star"
   1.187 -  apply (frule HFinite_diff_Infinitesimal_approx, assumption)
   1.188 -  apply (frule not_Infinitesimal_not_zero2)
   1.189 -  apply (frule_tac x = x in not_Infinitesimal_not_zero2)
   1.190 -  apply (drule HFinite_inverse2)+
   1.191 -  apply (drule approx_mult2, assumption, auto)
   1.192 -  apply (drule_tac c = "inverse x" in approx_mult1, assumption)
   1.193 -  apply (auto intro: approx_sym simp add: mult.assoc)
   1.194 -  done
   1.195 +lemma approx_inverse: 
   1.196 +  fixes x y :: "'a::real_normed_div_algebra star"
   1.197 +  assumes "x \<approx> y" and y: "y \<in> HFinite - Infinitesimal" shows "inverse x \<approx> inverse y"
   1.198 +proof -
   1.199 +  have x: "x \<in> HFinite - Infinitesimal"
   1.200 +    using HFinite_diff_Infinitesimal_approx assms(1) y by blast
   1.201 +  with y HFinite_inverse2 have "inverse x \<in> HFinite" "inverse y \<in> HFinite"
   1.202 +    by blast+
   1.203 +  then have "inverse y * x \<approx> 1"
   1.204 +    by (metis Diff_iff approx_mult2 assms(1) left_inverse not_Infinitesimal_not_zero y)
   1.205 +  then show ?thesis
   1.206 +    by (metis (no_types, lifting) DiffD2 HFinite_Infinitesimal_not_zero Infinitesimal_mult_disj x approx_def approx_sym left_diff_distrib left_inverse)
   1.207 +qed
   1.208  
   1.209  (*Used for NSLIM_inverse, NSLIMSEQ_inverse*)
   1.210  lemmas star_of_approx_inverse = star_of_HFinite_diff_Infinitesimal [THEN [2] approx_inverse]
   1.211 @@ -1250,17 +1220,11 @@
   1.212  
   1.213  lemma Ball_mem_monad_gt_zero: "0 < x \<Longrightarrow> x \<notin> Infinitesimal \<Longrightarrow> u \<in> monad x \<Longrightarrow> 0 < u"
   1.214    for u x :: hypreal
   1.215 -  apply (drule mem_monad_approx [THEN approx_sym])
   1.216 -  apply (erule bex_Infinitesimal_iff2 [THEN iffD2, THEN bexE])
   1.217 -  apply (drule_tac e = "-xa" in less_Infinitesimal_less, auto)
   1.218 -  done
   1.219 +  by (metis bex_Infinitesimal_iff2 less_Infinitesimal_less less_add_same_cancel2 mem_monad_approx)
   1.220  
   1.221  lemma Ball_mem_monad_less_zero: "x < 0 \<Longrightarrow> x \<notin> Infinitesimal \<Longrightarrow> u \<in> monad x \<Longrightarrow> u < 0"
   1.222    for u x :: hypreal
   1.223 -  apply (drule mem_monad_approx [THEN approx_sym])
   1.224 -  apply (erule bex_Infinitesimal_iff [THEN iffD2, THEN bexE])
   1.225 -  apply (cut_tac x = "-x" and e = xa in less_Infinitesimal_less, auto)
   1.226 -  done
   1.227 +  by (metis Ball_mem_monad_gt_zero approx_monad_iff less_asym linorder_neqE_linordered_idom mem_infmal_iff mem_monad_approx mem_monad_self)
   1.228  
   1.229  lemma lemma_approx_gt_zero: "0 < x \<Longrightarrow> x \<notin> Infinitesimal \<Longrightarrow> x \<approx> y \<Longrightarrow> 0 < y"
   1.230    for x y :: hypreal
   1.231 @@ -1304,20 +1268,19 @@
   1.232    for proving that an open interval is an NS open set.
   1.233  \<close>
   1.234  lemma Infinitesimal_add_hypreal_of_real_less:
   1.235 -  "x < y \<Longrightarrow> u \<in> Infinitesimal \<Longrightarrow> hypreal_of_real x + u < hypreal_of_real y"
   1.236 -  apply (simp add: Infinitesimal_def)
   1.237 -  apply (drule_tac x = "hypreal_of_real y + -hypreal_of_real x" in bspec, simp)
   1.238 -  apply (simp add: abs_less_iff)
   1.239 -  done
   1.240 +  assumes "x < y" and u: "u \<in> Infinitesimal"
   1.241 +  shows "hypreal_of_real x + u < hypreal_of_real y"
   1.242 +proof -
   1.243 +  have "\<bar>u\<bar> < hypreal_of_real y - hypreal_of_real x"
   1.244 +    using InfinitesimalD \<open>x < y\<close> u by fastforce
   1.245 +  then show ?thesis
   1.246 +    by (simp add: abs_less_iff)
   1.247 +qed
   1.248  
   1.249  lemma Infinitesimal_add_hrabs_hypreal_of_real_less:
   1.250    "x \<in> Infinitesimal \<Longrightarrow> \<bar>hypreal_of_real r\<bar> < hypreal_of_real y \<Longrightarrow>
   1.251      \<bar>hypreal_of_real r + x\<bar> < hypreal_of_real y"
   1.252 -  apply (drule_tac x = "hypreal_of_real r" in approx_hrabs_add_Infinitesimal)
   1.253 -  apply (drule approx_sym [THEN bex_Infinitesimal_iff2 [THEN iffD2]])
   1.254 -  apply (auto intro!: Infinitesimal_add_hypreal_of_real_less
   1.255 -      simp del: star_of_abs simp add: star_of_abs [symmetric])
   1.256 -  done
   1.257 +  by (metis Infinitesimal_add_hypreal_of_real_less approx_hrabs_add_Infinitesimal approx_sym bex_Infinitesimal_iff2 star_of_abs star_of_less)
   1.258  
   1.259  lemma Infinitesimal_add_hrabs_hypreal_of_real_less2:
   1.260    "x \<in> Infinitesimal \<Longrightarrow> \<bar>hypreal_of_real r\<bar> < hypreal_of_real y \<Longrightarrow>
   1.261 @@ -1325,13 +1288,16 @@
   1.262    using Infinitesimal_add_hrabs_hypreal_of_real_less by fastforce
   1.263  
   1.264  lemma hypreal_of_real_le_add_Infininitesimal_cancel:
   1.265 -  "u \<in> Infinitesimal \<Longrightarrow> v \<in> Infinitesimal \<Longrightarrow>
   1.266 -    hypreal_of_real x + u \<le> hypreal_of_real y + v \<Longrightarrow>
   1.267 -    hypreal_of_real x \<le> hypreal_of_real y"
   1.268 -  apply (simp add: linorder_not_less [symmetric], auto)
   1.269 -  apply (drule_tac u = "v-u" in Infinitesimal_add_hypreal_of_real_less)
   1.270 -   apply (auto simp add: Infinitesimal_diff)
   1.271 -  done
   1.272 +  assumes le: "hypreal_of_real x + u \<le> hypreal_of_real y + v" 
   1.273 +      and u: "u \<in> Infinitesimal" and v: "v \<in> Infinitesimal"
   1.274 +  shows "hypreal_of_real x \<le> hypreal_of_real y"
   1.275 +proof (rule ccontr)
   1.276 +  assume "\<not> hypreal_of_real x \<le> hypreal_of_real y"
   1.277 +  then have "hypreal_of_real y + (v - u) < hypreal_of_real x"
   1.278 +    by (simp add: Infinitesimal_add_hypreal_of_real_less Infinitesimal_diff u v)
   1.279 +  then show False
   1.280 +    by (simp add: add_diff_eq add_le_imp_le_diff le leD)
   1.281 +qed
   1.282  
   1.283  lemma hypreal_of_real_le_add_Infininitesimal_cancel2:
   1.284    "u \<in> Infinitesimal \<Longrightarrow> v \<in> Infinitesimal \<Longrightarrow>
   1.285 @@ -1342,77 +1308,8 @@
   1.286    "hypreal_of_real x < e \<Longrightarrow> e \<in> Infinitesimal \<Longrightarrow> hypreal_of_real x \<le> 0"
   1.287    by (metis Infinitesimal_interval eq_iff le_less_linear star_of_Infinitesimal_iff_0 star_of_eq_0)
   1.288  
   1.289 -(*used once, in Lim/NSDERIV_inverse*)
   1.290  lemma Infinitesimal_add_not_zero: "h \<in> Infinitesimal \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> star_of x + h \<noteq> 0"
   1.291 -  apply auto
   1.292 -  apply (subgoal_tac "h = - star_of x")
   1.293 -   apply (auto intro: minus_unique [symmetric])
   1.294 -  done
   1.295 -
   1.296 -lemma Infinitesimal_square_cancel [simp]: "x * x + y * y \<in> Infinitesimal \<Longrightarrow> x * x \<in> Infinitesimal"
   1.297 -  for x y :: hypreal
   1.298 -  by (meson Infinitesimal_interval2 le_add_same_cancel1 not_Infinitesimal_not_zero zero_le_square)
   1.299 -
   1.300 -lemma HFinite_square_cancel [simp]: "x * x + y * y \<in> HFinite \<Longrightarrow> x * x \<in> HFinite"
   1.301 -  for x y :: hypreal
   1.302 -  using HFinite_bounded le_add_same_cancel1 zero_le_square by blast
   1.303 -
   1.304 -lemma Infinitesimal_square_cancel2 [simp]: "x * x + y * y \<in> Infinitesimal \<Longrightarrow> y * y \<in> Infinitesimal"
   1.305 -  for x y :: hypreal
   1.306 -  apply (rule Infinitesimal_square_cancel)
   1.307 -  apply (rule add.commute [THEN subst])
   1.308 -  apply simp
   1.309 -  done
   1.310 -
   1.311 -lemma HFinite_square_cancel2 [simp]: "x * x + y * y \<in> HFinite \<Longrightarrow> y * y \<in> HFinite"
   1.312 -  for x y :: hypreal
   1.313 -  apply (rule HFinite_square_cancel)
   1.314 -  apply (rule add.commute [THEN subst])
   1.315 -  apply simp
   1.316 -  done
   1.317 -
   1.318 -lemma Infinitesimal_sum_square_cancel [simp]:
   1.319 -  "x * x + y * y + z * z \<in> Infinitesimal \<Longrightarrow> x * x \<in> Infinitesimal"
   1.320 -  for x y z :: hypreal
   1.321 -  apply (rule Infinitesimal_interval2, assumption)
   1.322 -    apply (rule_tac [2] zero_le_square, simp)
   1.323 -  apply (insert zero_le_square [of y])
   1.324 -  apply (insert zero_le_square [of z], simp del:zero_le_square)
   1.325 -  done
   1.326 -
   1.327 -lemma HFinite_sum_square_cancel [simp]: "x * x + y * y + z * z \<in> HFinite \<Longrightarrow> x * x \<in> HFinite"
   1.328 -  for x y z :: hypreal
   1.329 -  apply (rule HFinite_bounded, assumption)
   1.330 -   apply (rule_tac [2] zero_le_square)
   1.331 -  apply (insert zero_le_square [of y])
   1.332 -  apply (insert zero_le_square [of z], simp del:zero_le_square)
   1.333 -  done
   1.334 -
   1.335 -lemma Infinitesimal_sum_square_cancel2 [simp]:
   1.336 -  "y * y + x * x + z * z \<in> Infinitesimal \<Longrightarrow> x * x \<in> Infinitesimal"
   1.337 -  for x y z :: hypreal
   1.338 -  apply (rule Infinitesimal_sum_square_cancel)
   1.339 -  apply (simp add: ac_simps)
   1.340 -  done
   1.341 -
   1.342 -lemma HFinite_sum_square_cancel2 [simp]: "y * y + x * x + z * z \<in> HFinite \<Longrightarrow> x * x \<in> HFinite"
   1.343 -  for x y z :: hypreal
   1.344 -  apply (rule HFinite_sum_square_cancel)
   1.345 -  apply (simp add: ac_simps)
   1.346 -  done
   1.347 -
   1.348 -lemma Infinitesimal_sum_square_cancel3 [simp]:
   1.349 -  "z * z + y * y + x * x \<in> Infinitesimal \<Longrightarrow> x * x \<in> Infinitesimal"
   1.350 -  for x y z :: hypreal
   1.351 -  apply (rule Infinitesimal_sum_square_cancel)
   1.352 -  apply (simp add: ac_simps)
   1.353 -  done
   1.354 -
   1.355 -lemma HFinite_sum_square_cancel3 [simp]: "z * z + y * y + x * x \<in> HFinite \<Longrightarrow> x * x \<in> HFinite"
   1.356 -  for x y z :: hypreal
   1.357 -  apply (rule HFinite_sum_square_cancel)
   1.358 -  apply (simp add: ac_simps)
   1.359 -  done
   1.360 +  by (metis Infinitesimal_add_approx_self star_of_approx_zero_iff)
   1.361  
   1.362  lemma monad_hrabs_less: "y \<in> monad x \<Longrightarrow> 0 < hypreal_of_real e \<Longrightarrow> \<bar>y - x\<bar> < hypreal_of_real e"
   1.363    by (simp add: Infinitesimal_approx_minus approx_sym less_Infinitesimal_less mem_monad_approx)
   1.364 @@ -1427,22 +1324,13 @@
   1.365    by (metis (no_types, lifting) approx_refl approx_trans3 someI_ex st_def st_part_Ex st_part_Ex1)
   1.366  
   1.367  lemma st_SReal: "x \<in> HFinite \<Longrightarrow> st x \<in> \<real>"
   1.368 -  apply (simp add: st_def)
   1.369 -  apply (frule st_part_Ex, safe)
   1.370 -  apply (rule someI2)
   1.371 -   apply (auto intro: approx_sym)
   1.372 -  done
   1.373 +  by (metis (mono_tags, lifting) approx_sym someI_ex st_def st_part_Ex)
   1.374  
   1.375  lemma st_HFinite: "x \<in> HFinite \<Longrightarrow> st x \<in> HFinite"
   1.376    by (erule st_SReal [THEN SReal_subset_HFinite [THEN subsetD]])
   1.377  
   1.378  lemma st_unique: "r \<in> \<real> \<Longrightarrow> r \<approx> x \<Longrightarrow> st x = r"
   1.379 -  apply (frule SReal_subset_HFinite [THEN subsetD])
   1.380 -  apply (drule (1) approx_HFinite)
   1.381 -  apply (unfold st_def)
   1.382 -  apply (rule some_equality)
   1.383 -   apply (auto intro: approx_unique_real)
   1.384 -  done
   1.385 +  by (meson SReal_subset_HFinite approx_HFinite approx_unique_real st_SReal st_approx_self subsetD)
   1.386  
   1.387  lemma st_SReal_eq: "x \<in> \<real> \<Longrightarrow> st x = x"
   1.388    by (metis approx_refl st_unique)
   1.389 @@ -1467,14 +1355,10 @@
   1.390    by (blast intro: approx_st_eq st_eq_approx)
   1.391  
   1.392  lemma st_Infinitesimal_add_SReal: "x \<in> \<real> \<Longrightarrow> e \<in> Infinitesimal \<Longrightarrow> st (x + e) = x"
   1.393 -  apply (erule st_unique)
   1.394 -  apply (erule Infinitesimal_add_approx_self)
   1.395 -  done
   1.396 +  by (simp add: Infinitesimal_add_approx_self st_unique)
   1.397  
   1.398  lemma st_Infinitesimal_add_SReal2: "x \<in> \<real> \<Longrightarrow> e \<in> Infinitesimal \<Longrightarrow> st (e + x) = x"
   1.399 -  apply (erule st_unique)
   1.400 -  apply (erule Infinitesimal_add_approx_self2)
   1.401 -  done
   1.402 +  by (metis add.commute st_Infinitesimal_add_SReal)
   1.403  
   1.404  lemma HFinite_st_Infinitesimal_add: "x \<in> HFinite \<Longrightarrow> \<exists>e \<in> Infinitesimal. x = st(x) + e"
   1.405    by (blast dest!: st_approx_self [THEN approx_sym] bex_Infinitesimal_iff2 [THEN iffD2])
   1.406 @@ -1486,11 +1370,7 @@
   1.407    by (rule Reals_numeral [THEN st_SReal_eq])
   1.408  
   1.409  lemma st_neg_numeral [simp]: "st (- numeral w) = - numeral w"
   1.410 -proof -
   1.411 -  from Reals_numeral have "numeral w \<in> \<real>" .
   1.412 -  then have "- numeral w \<in> \<real>" by simp
   1.413 -  with st_SReal_eq show ?thesis .
   1.414 -qed
   1.415 +  using st_unique by auto
   1.416  
   1.417  lemma st_0 [simp]: "st 0 = 0"
   1.418    by (simp add: st_SReal_eq)
   1.419 @@ -1517,10 +1397,7 @@
   1.420  by (fast intro: st_Infinitesimal)
   1.421  
   1.422  lemma st_inverse: "x \<in> HFinite \<Longrightarrow> st x \<noteq> 0 \<Longrightarrow> st (inverse x) = inverse (st x)"
   1.423 -  apply (rule_tac c1 = "st x" in mult_left_cancel [THEN iffD1])
   1.424 -   apply (auto simp add: st_mult [symmetric] st_not_Infinitesimal HFinite_inverse)
   1.425 -  apply (subst right_inverse, auto)
   1.426 -  done
   1.427 +  by (simp add: approx_inverse st_SReal st_approx_self st_not_Infinitesimal st_unique)
   1.428  
   1.429  lemma st_divide [simp]: "x \<in> HFinite \<Longrightarrow> y \<in> HFinite \<Longrightarrow> st y \<noteq> 0 \<Longrightarrow> st (x / y) = st x / st y"
   1.430    by (simp add: divide_inverse st_mult st_not_Infinitesimal HFinite_inverse st_inverse)
   1.431 @@ -1530,34 +1407,24 @@
   1.432  
   1.433  lemma Infinitesimal_add_st_less:
   1.434    "x \<in> HFinite \<Longrightarrow> y \<in> HFinite \<Longrightarrow> u \<in> Infinitesimal \<Longrightarrow> st x < st y \<Longrightarrow> st x + u < st y"
   1.435 -  apply (drule st_SReal)+
   1.436 -  apply (auto intro!: Infinitesimal_add_hypreal_of_real_less simp add: SReal_iff)
   1.437 -  done
   1.438 +  by (metis Infinitesimal_add_hypreal_of_real_less SReal_iff st_SReal star_of_less)
   1.439  
   1.440  lemma Infinitesimal_add_st_le_cancel:
   1.441    "x \<in> HFinite \<Longrightarrow> y \<in> HFinite \<Longrightarrow> u \<in> Infinitesimal \<Longrightarrow>
   1.442      st x \<le> st y + u \<Longrightarrow> st x \<le> st y"
   1.443 -  apply (simp add: linorder_not_less [symmetric])
   1.444 -  apply (auto dest: Infinitesimal_add_st_less)
   1.445 -  done
   1.446 +  by (meson Infinitesimal_add_st_less leD le_less_linear)
   1.447  
   1.448  lemma st_le: "x \<in> HFinite \<Longrightarrow> y \<in> HFinite \<Longrightarrow> x \<le> y \<Longrightarrow> st x \<le> st y"
   1.449    by (metis approx_le_bound approx_sym linear st_SReal st_approx_self st_part_Ex1)
   1.450  
   1.451  lemma st_zero_le: "0 \<le> x \<Longrightarrow> x \<in> HFinite \<Longrightarrow> 0 \<le> st x"
   1.452 -  apply (subst st_0 [symmetric])
   1.453 -  apply (rule st_le, auto)
   1.454 -  done
   1.455 +  by (metis HFinite_0 st_0 st_le)
   1.456  
   1.457  lemma st_zero_ge: "x \<le> 0 \<Longrightarrow> x \<in> HFinite \<Longrightarrow> st x \<le> 0"
   1.458 -  apply (subst st_0 [symmetric])
   1.459 -  apply (rule st_le, auto)
   1.460 -  done
   1.461 +  by (metis HFinite_0 st_0 st_le)
   1.462  
   1.463  lemma st_hrabs: "x \<in> HFinite \<Longrightarrow> \<bar>st x\<bar> = st \<bar>x\<bar>"
   1.464 -  apply (simp add: linorder_not_le st_zero_le abs_if st_minus linorder_not_less)
   1.465 -  apply (auto dest!: st_zero_ge [OF order_less_imp_le])
   1.466 -  done
   1.467 +  by (simp add: order_class.order.antisym st_zero_ge linorder_not_le st_zero_le abs_if st_minus linorder_not_less)
   1.468  
   1.469  
   1.470  subsection \<open>Alternative Definitions using Free Ultrafilter\<close>
   1.471 @@ -1565,79 +1432,64 @@
   1.472  subsubsection \<open>\<^term>\<open>HFinite\<close>\<close>
   1.473  
   1.474  lemma HFinite_FreeUltrafilterNat:
   1.475 -  "star_n X \<in> HFinite \<Longrightarrow> \<exists>u. eventually (\<lambda>n. norm (X n) < u) \<U>"
   1.476 -  apply (auto simp add: HFinite_def SReal_def)
   1.477 -  apply (rule_tac x=r in exI)
   1.478 -  apply (simp add: hnorm_def star_of_def starfun_star_n)
   1.479 -  apply (simp add: star_less_def starP2_star_n)
   1.480 -  done
   1.481 +  assumes "star_n X \<in> HFinite"
   1.482 +  shows "\<exists>u. eventually (\<lambda>n. norm (X n) < u) \<U>"
   1.483 +proof -
   1.484 +  obtain r where "hnorm (star_n X) < hypreal_of_real r"
   1.485 +    using HFiniteD SReal_iff assms by fastforce
   1.486 +  then have "\<forall>\<^sub>F n in \<U>. norm (X n) < r"
   1.487 +    by (simp add: hnorm_def star_n_less star_of_def starfun_star_n)
   1.488 +  then show ?thesis ..
   1.489 +qed
   1.490  
   1.491  lemma FreeUltrafilterNat_HFinite:
   1.492 -  "\<exists>u. eventually (\<lambda>n. norm (X n) < u) \<U> \<Longrightarrow> star_n X \<in> HFinite"
   1.493 -  apply (auto simp add: HFinite_def mem_Rep_star_iff)
   1.494 -  apply (rule_tac x="star_of u" in bexI)
   1.495 -   apply (simp add: hnorm_def starfun_star_n star_of_def)
   1.496 -   apply (simp add: star_less_def starP2_star_n)
   1.497 -  apply (simp add: SReal_def)
   1.498 -  done
   1.499 +  assumes "eventually (\<lambda>n. norm (X n) < u) \<U>"
   1.500 +  shows "star_n X \<in> HFinite"
   1.501 +proof -
   1.502 +  have "hnorm (star_n X) < hypreal_of_real u"
   1.503 +    by (simp add: assms hnorm_def star_n_less star_of_def starfun_star_n)
   1.504 +  then show ?thesis
   1.505 +    by (meson HInfiniteD SReal_hypreal_of_real less_asym not_HFinite_HInfinite)
   1.506 +qed
   1.507  
   1.508  lemma HFinite_FreeUltrafilterNat_iff:
   1.509    "star_n X \<in> HFinite \<longleftrightarrow> (\<exists>u. eventually (\<lambda>n. norm (X n) < u) \<U>)"
   1.510 -  by (blast intro!: HFinite_FreeUltrafilterNat FreeUltrafilterNat_HFinite)
   1.511 +  using FreeUltrafilterNat_HFinite HFinite_FreeUltrafilterNat by blast
   1.512  
   1.513  
   1.514  subsubsection \<open>\<^term>\<open>HInfinite\<close>\<close>
   1.515  
   1.516 -lemma lemma_Compl_eq: "- {n. u < norm (f n)} = {n. norm (f n) \<le> u}"
   1.517 -  by auto
   1.518 -
   1.519 -lemma lemma_Compl_eq2: "- {n. norm (f n) < u} = {n. u \<le> norm (f n)}"
   1.520 -  by auto
   1.521 -
   1.522 -lemma lemma_Int_eq1: "{n. norm (f n) \<le> u} Int {n. u \<le> norm (f n)} = {n. norm(f n) = u}"
   1.523 -  by auto
   1.524 -
   1.525 -lemma lemma_FreeUltrafilterNat_one: "{n. norm (f n) = u} \<le> {n. norm (f n) < u + (1::real)}"
   1.526 -  by auto
   1.527 -
   1.528  text \<open>Exclude this type of sets from free ultrafilter for Infinite numbers!\<close>
   1.529  lemma FreeUltrafilterNat_const_Finite:
   1.530    "eventually (\<lambda>n. norm (X n) = u) \<U> \<Longrightarrow> star_n X \<in> HFinite"
   1.531 -  apply (rule FreeUltrafilterNat_HFinite)
   1.532 -  apply (rule_tac x = "u + 1" in exI)
   1.533 -  apply (auto elim: eventually_mono)
   1.534 -  done
   1.535 +  by (simp add: FreeUltrafilterNat_HFinite [where u = "u+1"] eventually_mono)
   1.536  
   1.537  lemma HInfinite_FreeUltrafilterNat:
   1.538 -  "star_n X \<in> HInfinite \<Longrightarrow> \<forall>u. eventually (\<lambda>n. u < norm (X n)) \<U>"
   1.539 +  "star_n X \<in> HInfinite \<Longrightarrow> eventually (\<lambda>n. u < norm (X n)) \<U>"
   1.540    apply (drule HInfinite_HFinite_iff [THEN iffD1])
   1.541    apply (simp add: HFinite_FreeUltrafilterNat_iff)
   1.542 -  apply (rule allI, drule_tac x="u + 1" in spec)
   1.543 +  apply (drule_tac x="u + 1" in spec)
   1.544    apply (simp add: FreeUltrafilterNat.eventually_not_iff[symmetric])
   1.545    apply (auto elim: eventually_mono)
   1.546    done
   1.547  
   1.548 -lemma lemma_Int_HI: "{n. norm (Xa n) < u} \<inter> {n. X n = Xa n} \<subseteq> {n. norm (X n) < u}"
   1.549 -  for u :: real
   1.550 -  by auto
   1.551 -
   1.552  lemma FreeUltrafilterNat_HInfinite:
   1.553 -  "\<forall>u. eventually (\<lambda>n. u < norm (X n)) \<U> \<Longrightarrow> star_n X \<in> HInfinite"
   1.554 -  apply (rule HInfinite_HFinite_iff [THEN iffD2])
   1.555 -  apply (safe, drule HFinite_FreeUltrafilterNat, safe)
   1.556 -  apply (drule_tac x = u in spec)
   1.557 +  assumes "\<And>u. eventually (\<lambda>n. u < norm (X n)) \<U>"
   1.558 +  shows "star_n X \<in> HInfinite"
   1.559  proof -
   1.560 -  fix u
   1.561 -  assume "\<forall>\<^sub>Fn in \<U>. norm (X n) < u" "\<forall>\<^sub>Fn in \<U>. u < norm (X n)"
   1.562 -  then have "\<forall>\<^sub>F x in \<U>. False"
   1.563 -    by eventually_elim auto
   1.564 -  then show False
   1.565 -    by (simp add: eventually_False FreeUltrafilterNat.proper)
   1.566 +  { fix u
   1.567 +    assume "\<forall>\<^sub>Fn in \<U>. norm (X n) < u" "\<forall>\<^sub>Fn in \<U>. u < norm (X n)"
   1.568 +    then have "\<forall>\<^sub>F x in \<U>. False"
   1.569 +      by eventually_elim auto
   1.570 +    then have False
   1.571 +      by (simp add: eventually_False FreeUltrafilterNat.proper) }
   1.572 +  then show ?thesis
   1.573 +    using HFinite_FreeUltrafilterNat HInfinite_HFinite_iff assms by blast
   1.574  qed
   1.575  
   1.576  lemma HInfinite_FreeUltrafilterNat_iff:
   1.577    "star_n X \<in> HInfinite \<longleftrightarrow> (\<forall>u. eventually (\<lambda>n. u < norm (X n)) \<U>)"
   1.578 -  by (blast intro!: HInfinite_FreeUltrafilterNat FreeUltrafilterNat_HInfinite)
   1.579 +  using HInfinite_FreeUltrafilterNat FreeUltrafilterNat_HInfinite by blast
   1.580  
   1.581  
   1.582  subsubsection \<open>\<^term>\<open>Infinitesimal\<close>\<close>
   1.583 @@ -1645,23 +1497,22 @@
   1.584  lemma ball_SReal_eq: "(\<forall>x::hypreal \<in> Reals. P x) \<longleftrightarrow> (\<forall>x::real. P (star_of x))"
   1.585    by (auto simp: SReal_def)
   1.586  
   1.587 -lemma Infinitesimal_FreeUltrafilterNat:
   1.588 -  "star_n X \<in> Infinitesimal \<Longrightarrow> \<forall>u>0. eventually (\<lambda>n. norm (X n) < u) \<U>"
   1.589 -  apply (simp add: Infinitesimal_def ball_SReal_eq)
   1.590 -  apply (simp add: hnorm_def starfun_star_n star_of_def)
   1.591 -  apply (simp add: star_less_def starP2_star_n)
   1.592 -  done
   1.593 -
   1.594 -lemma FreeUltrafilterNat_Infinitesimal:
   1.595 -  "\<forall>u>0. eventually (\<lambda>n. norm (X n) < u) \<U> \<Longrightarrow> star_n X \<in> Infinitesimal"
   1.596 -  apply (simp add: Infinitesimal_def ball_SReal_eq)
   1.597 -  apply (simp add: hnorm_def starfun_star_n star_of_def)
   1.598 -  apply (simp add: star_less_def starP2_star_n)
   1.599 -  done
   1.600  
   1.601  lemma Infinitesimal_FreeUltrafilterNat_iff:
   1.602 -  "(star_n X \<in> Infinitesimal) = (\<forall>u>0. eventually (\<lambda>n. norm (X n) < u) \<U>)"
   1.603 -  by (blast intro!: Infinitesimal_FreeUltrafilterNat FreeUltrafilterNat_Infinitesimal)
   1.604 +  "(star_n X \<in> Infinitesimal) = (\<forall>u>0. eventually (\<lambda>n. norm (X n) < u) \<U>)"  (is "?lhs = ?rhs")
   1.605 +proof 
   1.606 +  assume ?lhs
   1.607 +  then show ?rhs
   1.608 +    apply (simp add: Infinitesimal_def ball_SReal_eq)
   1.609 +    apply (simp add: hnorm_def starfun_star_n star_of_def star_less_def starP2_star_n)
   1.610 +    done
   1.611 +next
   1.612 +  assume ?rhs
   1.613 +  then show ?lhs
   1.614 +    apply (simp add: Infinitesimal_def ball_SReal_eq)
   1.615 +    apply (simp add: hnorm_def starfun_star_n star_of_def star_less_def starP2_star_n)
   1.616 +    done
   1.617 +qed
   1.618  
   1.619  
   1.620  text \<open>Infinitesimals as smaller than \<open>1/n\<close> for all \<open>n::nat (> 0)\<close>.\<close>
   1.621 @@ -1717,22 +1568,24 @@
   1.622    by (blast intro!: FreeUltrafilterNat.finite finite_rabs_real_of_nat_le_real)
   1.623  
   1.624  lemma FreeUltrafilterNat_nat_gt_real: "eventually (\<lambda>n. u < real n) \<U>"
   1.625 -  apply (rule FreeUltrafilterNat.finite')
   1.626 -  apply (subgoal_tac "{n::nat. \<not> u < real n} = {n. real n \<le> u}")
   1.627 -   apply (auto simp add: finite_real_of_nat_le_real)
   1.628 -  done
   1.629 +proof -
   1.630 +  have "{n::nat. \<not> u < real n} = {n. real n \<le> u}"
   1.631 +    by auto
   1.632 +  then show ?thesis
   1.633 +    by (auto simp add: FreeUltrafilterNat.finite' finite_real_of_nat_le_real)
   1.634 +qed
   1.635  
   1.636  text \<open>The complement of \<open>{n. \<bar>real n\<bar> \<le> u} = {n. u < \<bar>real n\<bar>}\<close> is in
   1.637    \<open>\<U>\<close> by property of (free) ultrafilters.\<close>
   1.638  
   1.639  text \<open>\<^term>\<open>\<omega>\<close> is a member of \<^term>\<open>HInfinite\<close>.\<close>
   1.640  theorem HInfinite_omega [simp]: "\<omega> \<in> HInfinite"
   1.641 -  apply (simp add: omega_def)
   1.642 -  apply (rule FreeUltrafilterNat_HInfinite)
   1.643 -  apply clarify
   1.644 -  apply (rule_tac u1 = "u-1" in eventually_mono [OF FreeUltrafilterNat_nat_gt_real])
   1.645 -  apply auto
   1.646 -  done
   1.647 +proof -
   1.648 +  have "\<forall>\<^sub>F n in \<U>. u < norm (1 + real n)" for u
   1.649 +    using FreeUltrafilterNat_nat_gt_real [of "u-1"] eventually_mono by fastforce
   1.650 +  then show ?thesis
   1.651 +    by (simp add: omega_def FreeUltrafilterNat_HInfinite)
   1.652 +qed
   1.653  
   1.654  
   1.655  text \<open>Epsilon is a member of Infinitesimal.\<close>
     2.1 --- a/src/HOL/Nonstandard_Analysis/Star.thy	Tue Apr 30 22:44:06 2019 +0100
     2.2 +++ b/src/HOL/Nonstandard_Analysis/Star.thy	Wed May 01 14:38:42 2019 +0100
     2.3 @@ -56,9 +56,6 @@
     2.4  lemma lemma_not_starA: "x \<notin> star_of ` A \<Longrightarrow> \<forall>y \<in> A. x \<noteq> star_of y"
     2.5    by auto
     2.6  
     2.7 -lemma lemma_Compl_eq: "- {n. X n = xa} = {n. X n \<noteq> xa}"
     2.8 -  by auto
     2.9 -
    2.10  lemma STAR_real_seq_to_hypreal: "\<forall>n. (X n) \<notin> M \<Longrightarrow> star_n X \<notin> *s* M"
    2.11    by (simp add: starset_def star_of_def Iset_star_n FreeUltrafilterNat.proper)
    2.12