--- 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>
--- 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"
--- 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)"
--- 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>
--- 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)