# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1660597075 -3600
# Node ID 9eeed5c424f9a7c55a29f4b8a070b53a8d7a1ec2
# Parent  62c64e3e47410964cb6f82ea08f75513b5f0c43c
A bit of cleaning up

diff -r 62c64e3e4741 -r 9eeed5c424f9 src/HOL/Nonstandard_Analysis/CLim.thy
--- a/src/HOL/Nonstandard_Analysis/CLim.thy	Mon Aug 15 12:50:24 2022 +0100
+++ b/src/HOL/Nonstandard_Analysis/CLim.thy	Mon Aug 15 21:57:55 2022 +0100
@@ -20,22 +20,7 @@
 
 text \<open>Changing the quantified variable. Install earlier?\<close>
 lemma all_shift: "(\<forall>x::'a::comm_ring_1. P x) \<longleftrightarrow> (\<forall>x. P (x - a))"
-  apply auto
-  apply (drule_tac x = "x + a" in spec)
-  apply (simp add: add.assoc)
-  done
-
-lemma complex_add_minus_iff [simp]: "x + - a = 0 \<longleftrightarrow> x = a"
-  for x a :: complex
-  by (simp add: diff_eq_eq)
-
-lemma complex_add_eq_0_iff [iff]: "x + y = 0 \<longleftrightarrow> y = - x"
-  for x y :: complex
-  apply auto
-  apply (drule sym [THEN diff_eq_eq [THEN iffD2]])
-  apply auto
-  done
-
+  by (metis add_diff_cancel)
 
 subsection \<open>Limit of Complex to Complex Function\<close>
 
diff -r 62c64e3e4741 -r 9eeed5c424f9 src/HOL/Nonstandard_Analysis/HSeries.thy
--- a/src/HOL/Nonstandard_Analysis/HSeries.thy	Mon Aug 15 12:50:24 2022 +0100
+++ b/src/HOL/Nonstandard_Analysis/HSeries.thy	Mon Aug 15 21:57:55 2022 +0100
@@ -91,21 +91,16 @@
 lemma sumhr_hypreal_of_hypnat_omega: "sumhr (0, whn, \<lambda>i. 1) = hypreal_of_hypnat whn"
   by (simp add: sumhr_const)
 
+lemma whn_eq_\<omega>m1: "hypreal_of_hypnat whn = \<omega> - 1"
+  unfolding star_class_defs omega_def hypnat_omega_def of_hypnat_def star_of_def
+  by (simp add: starfun_star_n starfun2_star_n)
+
 lemma sumhr_hypreal_omega_minus_one: "sumhr(0, whn, \<lambda>i. 1) = \<omega> - 1"
-  apply (simp add: sumhr_const)
-    (* FIXME: need lemma: hypreal_of_hypnat whn = \<omega> - 1 *)
-    (* maybe define \<omega> = hypreal_of_hypnat whn + 1 *)
-  apply (unfold star_class_defs omega_def hypnat_omega_def of_hypnat_def star_of_def)
-  apply (simp add: starfun_star_n starfun2_star_n)
-  done
+  by (simp add: sumhr_const whn_eq_\<omega>m1)
 
 lemma sumhr_minus_one_realpow_zero [simp]: "\<And>N. sumhr (0, N + N, \<lambda>i. (-1) ^ (i + 1)) = 0"
   unfolding sumhr_app
-  apply transfer
-  apply (simp del: power_Suc add: mult_2 [symmetric])
-  apply (induct_tac N)
-   apply simp_all
-  done
+  by transfer (induct_tac N, auto)
 
 lemma sumhr_interval_const:
   "(\<forall>n. m \<le> Suc n \<longrightarrow> f n = r) \<and> m \<le> na \<Longrightarrow>
@@ -145,17 +140,19 @@
   by (auto simp add: sums_NSsums_iff [symmetric] not_le[symmetric] intro!: sums_finite)
 
 lemma NSsummable_NSCauchy:
-  "NSsummable f \<longleftrightarrow> (\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite. \<bar>sumhr (M, N, f)\<bar> \<approx> 0)"
-  apply (auto simp add: summable_NSsummable_iff [symmetric]
-      summable_iff_convergent convergent_NSconvergent_iff atLeast0LessThan[symmetric]
-      NSCauchy_NSconvergent_iff [symmetric] NSCauchy_def starfunNat_sumr)
-  apply (cut_tac x = M and y = N in linorder_less_linear)
-  by (metis approx_hrabs_zero_cancel approx_minus_iff approx_refl approx_sym sumhr_split_diff)
+  "NSsummable f \<longleftrightarrow> (\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite. \<bar>sumhr (M, N, f)\<bar> \<approx> 0)" (is "?L=?R")
+proof -
+  have "?L = (\<forall>M\<in>HNatInfinite. \<forall>N\<in>HNatInfinite. sumhr (0, M, f) \<approx> sumhr (0, N, f))"
+    by (auto simp add: summable_iff_convergent convergent_NSconvergent_iff NSCauchy_def starfunNat_sumr 
+        simp flip: NSCauchy_NSconvergent_iff summable_NSsummable_iff atLeast0LessThan)
+  also have "... \<longleftrightarrow> ?R"
+    by (metis approx_hrabs_zero_cancel approx_minus_iff approx_refl approx_sym linorder_less_linear sumhr_hrabs_approx sumhr_split_diff)
+  finally show ?thesis .
+qed
 
 text \<open>Terms of a convergent series tend to zero.\<close>
 lemma NSsummable_NSLIMSEQ_zero: "NSsummable f \<Longrightarrow> f \<longlonglongrightarrow>\<^sub>N\<^sub>S 0"
-  apply (auto simp add: NSLIMSEQ_def NSsummable_NSCauchy)
-  by (metis HNatInfinite_add approx_hrabs_zero_cancel sumhr_Suc)
+  by (metis HNatInfinite_add NSLIMSEQ_def NSsummable_NSCauchy approx_hrabs_zero_cancel star_of_zero sumhr_Suc)
 
 text \<open>Nonstandard comparison test.\<close>
 lemma NSsummable_comparison_test: "\<exists>N. \<forall>n. N \<le> n \<longrightarrow> \<bar>f n\<bar> \<le> g n \<Longrightarrow> NSsummable g \<Longrightarrow> NSsummable f"
diff -r 62c64e3e4741 -r 9eeed5c424f9 src/HOL/Nonstandard_Analysis/HTranscendental.thy
--- a/src/HOL/Nonstandard_Analysis/HTranscendental.thy	Mon Aug 15 12:50:24 2022 +0100
+++ b/src/HOL/Nonstandard_Analysis/HTranscendental.thy	Mon Aug 15 21:57:55 2022 +0100
@@ -122,7 +122,7 @@
 
 lemma HFinite_hypreal_sqrt_imp_HFinite:
   "\<lbrakk>0 \<le> x; ( *f* sqrt) x \<in> HFinite\<rbrakk> \<Longrightarrow> x \<in> HFinite"
-  by (metis HFinite_mult hrealpow_two hypreal_sqrt_pow2_iff numeral_2_eq_2)
+  by (metis HFinite_mult hypreal_sqrt_pow2_iff power2_eq_square)
 
 lemma HFinite_hypreal_sqrt_iff [simp]:
   "0 \<le> x \<Longrightarrow> (( *f* sqrt) x \<in> HFinite) = (x \<in> HFinite)"
diff -r 62c64e3e4741 -r 9eeed5c424f9 src/HOL/Nonstandard_Analysis/HyperDef.thy
--- a/src/HOL/Nonstandard_Analysis/HyperDef.thy	Mon Aug 15 12:50:24 2022 +0100
+++ b/src/HOL/Nonstandard_Analysis/HyperDef.thy	Mon Aug 15 21:57:55 2022 +0100
@@ -278,46 +278,6 @@
   for r :: hypreal
   by (rule power_Suc)
 
-lemma hrealpow_two: "r ^ Suc (Suc 0) = r * r"
-  for r :: hypreal
-  by simp
-
-lemma hrealpow_two_le [simp]: "0 \<le> r ^ Suc (Suc 0)"
-  for r :: hypreal
-  by (auto simp add: zero_le_mult_iff)
-
-lemma hrealpow_two_le_add_order [simp]: "0 \<le> u ^ Suc (Suc 0) + v ^ Suc (Suc 0)"
-  for u v :: hypreal
-  by (simp only: hrealpow_two_le add_nonneg_nonneg)
-
-lemma hrealpow_two_le_add_order2 [simp]: "0 \<le> u ^ Suc (Suc 0) + v ^ Suc (Suc 0) + w ^ Suc (Suc 0)"
-  for u v w :: hypreal
-  by (simp only: hrealpow_two_le add_nonneg_nonneg)
-
-lemma hypreal_add_nonneg_eq_0_iff: "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> x + y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
-  for x y :: hypreal
-  by arith
-
-
-(* FIXME: DELETE THESE *)
-lemma hypreal_three_squares_add_zero_iff: "x * x + y * y + z * z = 0 \<longleftrightarrow> x = 0 \<and> y = 0 \<and> z = 0"
-  for x y z :: hypreal
-  by (simp only: zero_le_square add_nonneg_nonneg hypreal_add_nonneg_eq_0_iff) auto
-
-lemma hrealpow_three_squares_add_zero_iff [simp]:
-  "x ^ Suc (Suc 0) + y ^ Suc (Suc 0) + z ^ Suc (Suc 0) = 0 \<longleftrightarrow> x = 0 \<and> y = 0 \<and> z = 0"
-  for x y z :: hypreal
-  by (simp only: hypreal_three_squares_add_zero_iff hrealpow_two)
-
-(*FIXME: This and RealPow.abs_realpow_two should be replaced by an abstract
-  result proved in Rings or Fields*)
-lemma hrabs_hrealpow_two [simp]: "\<bar>x ^ Suc (Suc 0)\<bar> = x ^ Suc (Suc 0)"
-  for x :: hypreal
-  by (simp add: abs_mult)
-
-lemma two_hrealpow_ge_one [simp]: "(1::hypreal) \<le> 2 ^ n"
-  using power_increasing [of 0 n "2::hypreal"] by simp
-
 lemma hrealpow: "star_n X ^ m = star_n (\<lambda>n. (X n::real) ^ m)"
   by (induct m) (auto simp: star_n_one_num star_n_mult)
 
@@ -336,14 +296,6 @@
   "(- numeral v :: hypreal) ^ n = hypreal_of_real ((- numeral v) ^ n)"
   by simp
 declare power_hypreal_of_real_neg_numeral [of _ "numeral w", simp] for w
-(*
-lemma hrealpow_HFinite:
-  fixes x :: "'a::{real_normed_algebra,power} star"
-  shows "x \<in> HFinite ==> x ^ n \<in> HFinite"
-apply (induct_tac "n")
-apply (auto simp add: power_Suc intro: HFinite_mult)
-done
-*)
 
 
 subsection \<open>Powers with Hypernatural Exponents\<close>
diff -r 62c64e3e4741 -r 9eeed5c424f9 src/HOL/Nonstandard_Analysis/NSA.thy
--- a/src/HOL/Nonstandard_Analysis/NSA.thy	Mon Aug 15 12:50:24 2022 +0100
+++ b/src/HOL/Nonstandard_Analysis/NSA.thy	Mon Aug 15 21:57:55 2022 +0100
@@ -460,7 +460,6 @@
   for x :: hypreal
   by (auto intro: Infinitesimal_interval simp add: order_le_less)
 
-
 lemma lemma_Infinitesimal_hyperpow: "x \<in> Infinitesimal \<Longrightarrow> 0 < N \<Longrightarrow> \<bar>x pow N\<bar> \<le> \<bar>x\<bar>"
   for x :: hypreal
   apply (clarsimp simp: Infinitesimal_def)
@@ -1465,13 +1464,13 @@
   by (simp add: FreeUltrafilterNat_HFinite [where u = "u+1"] eventually_mono)
 
 lemma HInfinite_FreeUltrafilterNat:
-  "star_n X \<in> HInfinite \<Longrightarrow> eventually (\<lambda>n. u < norm (X n)) \<U>"
-  apply (drule HInfinite_HFinite_iff [THEN iffD1])
-  apply (simp add: HFinite_FreeUltrafilterNat_iff)
-  apply (drule_tac x="u + 1" in spec)
-  apply (simp add: FreeUltrafilterNat.eventually_not_iff[symmetric])
-  apply (auto elim: eventually_mono)
-  done
+  assumes "star_n X \<in> HInfinite" shows "\<forall>\<^sub>F n in \<U>. u < norm (X n)"
+proof -
+have "\<not> (\<forall>\<^sub>F n in \<U>. norm (X n) < u + 1)"
+  using FreeUltrafilterNat_HFinite HFinite_HInfinite_iff assms by auto
+  then show ?thesis
+    by (auto simp flip: FreeUltrafilterNat.eventually_not_iff elim: eventually_mono)
+qed
 
 lemma FreeUltrafilterNat_HInfinite:
   assumes "\<And>u. eventually (\<lambda>n. u < norm (X n)) \<U>"
@@ -1500,18 +1499,12 @@
 
 lemma Infinitesimal_FreeUltrafilterNat_iff:
   "(star_n X \<in> Infinitesimal) = (\<forall>u>0. eventually (\<lambda>n. norm (X n) < u) \<U>)"  (is "?lhs = ?rhs")
-proof 
-  assume ?lhs
-  then show ?rhs
-    apply (simp add: Infinitesimal_def ball_SReal_eq)
-    apply (simp add: hnorm_def starfun_star_n star_of_def star_less_def starP2_star_n)
-    done
-next
-  assume ?rhs
-  then show ?lhs
-    apply (simp add: Infinitesimal_def ball_SReal_eq)
-    apply (simp add: hnorm_def starfun_star_n star_of_def star_less_def starP2_star_n)
-    done
+proof -
+  have "?lhs \<longleftrightarrow> (\<forall>r>0. hnorm (star_n X) < hypreal_of_real r)"
+    by (simp add: Infinitesimal_def ball_SReal_eq)
+  also have "... \<longleftrightarrow> ?rhs"
+    by (simp add: hnorm_def starfun_star_n star_of_def star_less_def starP2_star_n)
+  finally show ?thesis .
 qed
 
 
@@ -1521,16 +1514,18 @@
   by (meson inverse_positive_iff_positive less_trans of_nat_0_less_iff reals_Archimedean zero_less_Suc)
 
 lemma lemma_Infinitesimal2:
-  "(\<forall>r \<in> Reals. 0 < r \<longrightarrow> x < r) \<longleftrightarrow> (\<forall>n. x < inverse(hypreal_of_nat (Suc n)))"
-  apply safe
-   apply (drule_tac x = "inverse (hypreal_of_real (real (Suc n))) " in bspec)
-    apply simp_all
-  using less_imp_of_nat_less apply fastforce
-  apply (auto dest!: reals_Archimedean simp add: SReal_iff simp del: of_nat_Suc)
-  apply (drule star_of_less [THEN iffD2])
-  apply simp
-  apply (blast intro: order_less_trans)
-  done
+  "(\<forall>r \<in> Reals. 0 < r \<longrightarrow> x < r) \<longleftrightarrow> (\<forall>n. x < inverse(hypreal_of_nat (Suc n)))" (is "_ = ?rhs")
+proof (intro iffI strip)
+  assume R: ?rhs
+  fix r::hypreal
+  assume "r \<in> \<real>" "0 < r"
+  then obtain n y where "inverse (real (Suc n)) < y" and r: "r = hypreal_of_real y"
+    by (metis SReal_iff reals_Archimedean star_of_0_less)
+  then have "inverse (1 + hypreal_of_nat n) < hypreal_of_real y"
+    by (metis of_nat_Suc star_of_inverse star_of_less star_of_nat_def)
+  then show "x < r"
+    by (metis R r le_less_trans less_imp_le of_nat_Suc)
+qed (meson Reals_inverse Reals_of_nat of_nat_0_less_iff positive_imp_inverse_positive zero_less_Suc)
 
 
 lemma Infinitesimal_hypreal_of_nat_iff:
@@ -1552,10 +1547,14 @@
   by auto
 
 lemma finite_real_of_nat_less_real: "finite {n::nat. real n < u}"
-  apply (cut_tac x = u in reals_Archimedean2, safe)
-  apply (rule finite_real_of_nat_segment [THEN [2] finite_subset])
-  apply (auto dest: order_less_trans)
-  done
+proof -
+  obtain m where "u < real m"
+    using reals_Archimedean2 by blast
+  then have "{n. real n < u} \<subseteq> {..<m}"
+    by force
+  then show ?thesis
+    using finite_nat_iff_bounded by force
+qed
 
 lemma finite_real_of_nat_le_real: "finite {n::nat. real n \<le> u}"
   by (metis infinite_nat_iff_unbounded leD le_nat_floor mem_Collect_eq)
@@ -1619,7 +1618,7 @@
   shows "finite {n. u \<le> inverse (real (Suc n))}"
 proof -
   have "\<forall>na. u \<le> inverse (1 + real na) \<longrightarrow> na \<le> ceiling (inverse u)"
-    by (metis add.commute add1_zle_eq assms ceiling_mono ceiling_of_nat dual_order.order_iff_strict inverse_inverse_eq le_imp_inverse_le semiring_1_class.of_nat_simps(2))
+    by (smt (verit, best) assms ceiling_less_cancel ceiling_of_nat inverse_inverse_eq inverse_le_iff_le)
   then show ?thesis
     apply (auto simp add: finite_nat_set_iff_bounded_le)
     by (meson assms inverse_positive_iff_positive le_nat_iff less_imp_le zero_less_ceiling)