--- a/src/HOL/Analysis/Abstract_Topology_2.thy Tue Jan 03 18:23:52 2023 +0100
+++ b/src/HOL/Analysis/Abstract_Topology_2.thy Tue Jan 03 19:55:35 2023 +0000
@@ -17,9 +17,7 @@
lemma approachable_lt_le2:
"(\<exists>(d::real) > 0. \<forall>x. Q x \<longrightarrow> f x < d \<longrightarrow> P x) \<longleftrightarrow> (\<exists>d>0. \<forall>x. f x \<le> d \<longrightarrow> Q x \<longrightarrow> P x)"
- apply auto
- apply (rule_tac x="d/2" in exI, auto)
- done
+by (meson dense less_eq_real_def order_le_less_trans)
lemma triangle_lemma:
fixes x y z :: real
@@ -88,13 +86,18 @@
qed
qed
+lemma islimpt_closure:
+ "\<lbrakk>S \<subseteq> T; \<And>x. \<lbrakk>x islimpt S; x \<in> T\<rbrakk> \<Longrightarrow> x \<in> S\<rbrakk> \<Longrightarrow> S = T \<inter> closure S"
+ using closure_def by fastforce
+
lemma closedin_limpt:
"closedin (top_of_set T) S \<longleftrightarrow> S \<subseteq> T \<and> (\<forall>x. x islimpt S \<and> x \<in> T \<longrightarrow> x \<in> S)"
- apply (simp add: closedin_closed, safe)
- apply (simp add: closed_limpt islimpt_subset)
- apply (rule_tac x="closure S" in exI, simp)
- apply (force simp: closure_def)
- done
+proof -
+ have "\<And>U x. \<lbrakk>closed U; S = T \<inter> U; x islimpt S; x \<in> T\<rbrakk> \<Longrightarrow> x \<in> S"
+ by (meson IntI closed_limpt inf_le2 islimpt_subset)
+ then show ?thesis
+ by (metis closed_closure closedin_closed closedin_imp_subset islimpt_closure)
+qed
lemma closedin_closed_eq: "closed S \<Longrightarrow> closedin (top_of_set S) T \<longleftrightarrow> closed T \<and> T \<subseteq> S"
by (meson closedin_limpt closed_subset closedin_closed_trans)
@@ -104,8 +107,8 @@
\<Longrightarrow> connected S \<longleftrightarrow> (\<nexists>A B. closed A \<and> closed B \<and> A \<noteq> {} \<and> B \<noteq> {} \<and> A \<union> B = S \<and> A \<inter> B = {})"
unfolding connected_closedin_eq closedin_closed_eq connected_closedin_eq by blast
-text \<open>If a connnected set is written as the union of two nonempty closed sets, then these sets
-have to intersect.\<close>
+text \<open>If a connnected set is written as the union of two nonempty closed sets,
+ then these sets have to intersect.\<close>
lemma connected_as_closed_union:
assumes "connected C" "C = A \<union> B" "closed A" "closed B" "A \<noteq> {}" "B \<noteq> {}"
@@ -128,10 +131,7 @@
lemma closedin_compact_eq:
fixes S :: "'a::t2_space set"
- shows
- "compact S
- \<Longrightarrow> (closedin (top_of_set S) T \<longleftrightarrow>
- compact T \<and> T \<subseteq> S)"
+ shows "compact S \<Longrightarrow> (closedin (top_of_set S) T \<longleftrightarrow> compact T \<and> T \<subseteq> S)"
by (metis closedin_imp_subset closedin_compact closed_subset compact_imp_closed)
@@ -174,12 +174,11 @@
fix x and A and V
assume "x \<in> S" "V \<subseteq> A" "open V" "x \<in> V" "T \<inter> A = {}"
then have "openin (top_of_set S) (A \<inter> V \<inter> S)"
- by (auto simp: openin_open intro!: exI[where x="V"])
+ by (simp add: inf_absorb2 openin_subtopology_Int)
moreover have "A \<inter> V \<inter> S \<noteq> {}" using \<open>x \<in> V\<close> \<open>V \<subseteq> A\<close> \<open>x \<in> S\<close>
by auto
- ultimately have "T \<inter> (A \<inter> V \<inter> S) \<noteq> {}"
- by (rule assms)
- with \<open>T \<inter> A = {}\<close> show False by auto
+ ultimately show False
+ using \<open>T \<inter> A = {}\<close> assms by fastforce
qed
@@ -192,10 +191,10 @@
by (auto simp: frontier_of_def frontier_def)
lemma connected_Int_frontier:
- "\<lbrakk>connected s; s \<inter> t \<noteq> {}; s - t \<noteq> {}\<rbrakk> \<Longrightarrow> (s \<inter> frontier t \<noteq> {})"
+ "\<lbrakk>connected S; S \<inter> T \<noteq> {}; S - T \<noteq> {}\<rbrakk> \<Longrightarrow> S \<inter> frontier T \<noteq> {}"
apply (simp add: frontier_interiors connected_openin, safe)
- apply (drule_tac x="s \<inter> interior t" in spec, safe)
- apply (drule_tac [2] x="s \<inter> interior (-t)" in spec)
+ apply (drule_tac x="S \<inter> interior T" in spec, safe)
+ apply (drule_tac [2] x="S \<inter> interior (-T)" in spec)
apply (auto simp: disjoint_eq_subset_Compl dest: interior_subset [THEN subsetD])
done
@@ -203,8 +202,7 @@
lemma openin_delete:
fixes a :: "'a :: t1_space"
- shows "openin (top_of_set u) s
- \<Longrightarrow> openin (top_of_set u) (s - {a})"
+ shows "openin (top_of_set u) S \<Longrightarrow> openin (top_of_set u) (S - {a})"
by (metis Int_Diff open_delete openin_open)
lemma compact_eq_openin_cover:
@@ -241,8 +239,7 @@
from \<open>finite D\<close> show "finite ?D"
by (rule finite_imageI)
from \<open>S \<subseteq> \<Union>D\<close> show "S \<subseteq> \<Union>?D"
- apply (rule subset_trans)
- by (metis Int_Union Int_lower2 \<open>D \<subseteq> (\<inter>) S ` C\<close> image_inv_into_cancel)
+ by (metis \<open>D \<subseteq> (\<inter>) S ` C\<close> image_inv_into_cancel inf_Sup le_infE)
qed
then show "\<exists>D\<subseteq>C. finite D \<and> S \<subseteq> \<Union>D" ..
qed
@@ -332,49 +329,47 @@
subsection\<^marker>\<open>tag unimportant\<close> \<open>Continuity relative to a union.\<close>
lemma continuous_on_Un_local:
- "\<lbrakk>closedin (top_of_set (s \<union> t)) s; closedin (top_of_set (s \<union> t)) t;
- continuous_on s f; continuous_on t f\<rbrakk>
- \<Longrightarrow> continuous_on (s \<union> t) f"
+ "\<lbrakk>closedin (top_of_set (S \<union> T)) S; closedin (top_of_set (S \<union> T)) T;
+ continuous_on S f; continuous_on T f\<rbrakk>
+ \<Longrightarrow> continuous_on (S \<union> T) f"
unfolding continuous_on closedin_limpt
by (metis Lim_trivial_limit Lim_within_union Un_iff trivial_limit_within)
lemma continuous_on_cases_local:
- "\<lbrakk>closedin (top_of_set (s \<union> t)) s; closedin (top_of_set (s \<union> t)) t;
- continuous_on s f; continuous_on t g;
- \<And>x. \<lbrakk>x \<in> s \<and> \<not>P x \<or> x \<in> t \<and> P x\<rbrakk> \<Longrightarrow> f x = g x\<rbrakk>
- \<Longrightarrow> continuous_on (s \<union> t) (\<lambda>x. if P x then f x else g x)"
+ "\<lbrakk>closedin (top_of_set (S \<union> T)) S; closedin (top_of_set (S \<union> T)) T;
+ continuous_on S f; continuous_on T g;
+ \<And>x. \<lbrakk>x \<in> S \<and> \<not>P x \<or> x \<in> T \<and> P x\<rbrakk> \<Longrightarrow> f x = g x\<rbrakk>
+ \<Longrightarrow> continuous_on (S \<union> T) (\<lambda>x. if P x then f x else g x)"
by (rule continuous_on_Un_local) (auto intro: continuous_on_eq)
lemma continuous_on_cases_le:
fixes h :: "'a :: topological_space \<Rightarrow> real"
- assumes "continuous_on {t \<in> s. h t \<le> a} f"
- and "continuous_on {t \<in> s. a \<le> h t} g"
- and h: "continuous_on s h"
- and "\<And>t. \<lbrakk>t \<in> s; h t = a\<rbrakk> \<Longrightarrow> f t = g t"
- shows "continuous_on s (\<lambda>t. if h t \<le> a then f(t) else g(t))"
+ assumes "continuous_on {x \<in> S. h x \<le> a} f"
+ and "continuous_on {x \<in> S. a \<le> h x} g"
+ and h: "continuous_on S h"
+ and "\<And>x. \<lbrakk>x \<in> S; h x = a\<rbrakk> \<Longrightarrow> f x = g x"
+ shows "continuous_on S (\<lambda>x. if h x \<le> a then f(x) else g(x))"
proof -
- have s: "s = (s \<inter> h -` atMost a) \<union> (s \<inter> h -` atLeast a)"
+ have S: "S = (S \<inter> h -` atMost a) \<union> (S \<inter> h -` atLeast a)"
by force
- have 1: "closedin (top_of_set s) (s \<inter> h -` atMost a)"
+ have 1: "closedin (top_of_set S) (S \<inter> h -` atMost a)"
by (rule continuous_closedin_preimage [OF h closed_atMost])
- have 2: "closedin (top_of_set s) (s \<inter> h -` atLeast a)"
+ have 2: "closedin (top_of_set S) (S \<inter> h -` atLeast a)"
by (rule continuous_closedin_preimage [OF h closed_atLeast])
- have eq: "s \<inter> h -` {..a} = {t \<in> s. h t \<le> a}" "s \<inter> h -` {a..} = {t \<in> s. a \<le> h t}"
+ have [simp]: "S \<inter> h -` {..a} = {x \<in> S. h x \<le> a}" "S \<inter> h -` {a..} = {x \<in> S. a \<le> h x}"
by auto
- show ?thesis
- apply (rule continuous_on_subset [of s, OF _ order_refl])
- apply (subst s)
- apply (rule continuous_on_cases_local)
- using 1 2 s assms apply (auto simp: eq)
- done
+ have "continuous_on (S \<inter> h -` {..a} \<union> S \<inter> h -` {a..}) (\<lambda>x. if h x \<le> a then f x else g x)"
+ by (intro continuous_on_cases_local) (use 1 2 S assms in auto)
+ then show ?thesis
+ using S by force
qed
lemma continuous_on_cases_1:
- fixes s :: "real set"
- assumes "continuous_on {t \<in> s. t \<le> a} f"
- and "continuous_on {t \<in> s. a \<le> t} g"
- and "a \<in> s \<Longrightarrow> f a = g a"
- shows "continuous_on s (\<lambda>t. if t \<le> a then f(t) else g(t))"
+ fixes S :: "real set"
+ assumes "continuous_on {t \<in> S. t \<le> a} f"
+ and "continuous_on {t \<in> S. a \<le> t} g"
+ and "a \<in> S \<Longrightarrow> f a = g a"
+ shows "continuous_on S (\<lambda>t. if t \<le> a then f(t) else g(t))"
using assms
by (auto intro: continuous_on_cases_le [where h = id, simplified])
@@ -504,8 +499,7 @@
show "\<exists>\<U>\<subseteq>\<B> - {{}}. T = \<Union>\<U>" if "openin (top_of_set S) T" for T
using \<B> [OF that]
apply clarify
- apply (rule_tac x="\<U> - {{}}" in exI, auto)
- done
+ by (rule_tac x="\<U> - {{}}" in exI, auto)
qed auto
qed
@@ -666,16 +660,15 @@
and "U \<subseteq> f ` S"
shows "openin (top_of_set S) (S \<inter> f -` U) \<longleftrightarrow>
openin (top_of_set (f ` S)) U"
-apply (rule continuous_right_inverse_imp_quotient_map)
-using assms apply force+
-done
+ using assms
+ by (intro continuous_right_inverse_imp_quotient_map) auto
lemma continuous_imp_quotient_map:
fixes f :: "'a::t2_space \<Rightarrow> 'b::t2_space"
assumes "continuous_on S f" "f ` S = T" "compact S" "U \<subseteq> T"
shows "openin (top_of_set S) (S \<inter> f -` U) \<longleftrightarrow>
openin (top_of_set T) U"
- by (metis (no_types, lifting) assms closed_map_imp_quotient_map continuous_imp_closed_map)
+ by (simp add: assms closed_map_imp_quotient_map continuous_imp_closed_map)
subsection\<^marker>\<open>tag unimportant\<close>\<open>Pasting lemmas for functions, for of casewise definitions\<close>
@@ -747,14 +740,11 @@
by auto
have 1: "(\<Union>i\<in>I. T i \<inter> f i -` U) \<subseteq> topspace X"
using T by blast
- then have lf: "locally_finite_in X ((\<lambda>i. T i \<inter> f i -` U) ` I)"
+ then have "locally_finite_in X ((\<lambda>i. T i \<inter> f i -` U) ` I)"
unfolding locally_finite_in_def
using finite_subset [OF sub] fin by force
- show "closedin X (topspace X \<inter> g -` U)"
- apply (subst *)
- apply (rule closedin_locally_finite_Union)
- apply (auto intro: cTf lf)
- done
+ then show "closedin X (topspace X \<inter> g -` U)"
+ by (smt (verit, best) * cTf closedin_locally_finite_Union image_iff)
qed
subsubsection\<open>Likewise on closed sets, with a finiteness assumption\<close>
@@ -784,10 +774,8 @@
next
fix x i
assume "i \<in> I" and "x \<in> topspace X \<inter> T i"
- show "f (SOME i. i \<in> I \<and> x \<in> T i) x = f i x"
- apply (rule someI2_ex)
- using \<open>i \<in> I\<close> \<open>x \<in> topspace X \<inter> T i\<close> apply blast
- by (meson Int_iff \<open>i \<in> I\<close> \<open>x \<in> topspace X \<inter> T i\<close> f)
+ then show "f (SOME i. i \<in> I \<and> x \<in> T i) x = f i x"
+ by (metis (mono_tags, lifting) IntE IntI f someI2)
qed
lemma pasting_lemma_exists_closed:
@@ -824,26 +812,19 @@
show "?f i x = ?f j x"
if "i \<in> {True,False}" "j \<in> {True,False}" and x: "x \<in> topspace X \<inter> ?T i \<inter> ?T j" for i j x
proof -
- have "f x = g x"
- if "i" "\<not> j"
- apply (rule fg)
- unfolding frontier_of_closures eq
- using x that closure_of_restrict by fastforce
+ have "f x = g x" if "i" "\<not> j"
+ by (smt (verit, best) Diff_Diff_Int closure_of_interior_of closure_of_restrict eq fg
+ frontier_of_closures interior_of_complement that x)
moreover
have "g x = f x"
if "x \<in> X closure_of {x. \<not> P x}" "x \<in> X closure_of Collect P" "\<not> i" "j" for x
- apply (rule fg [symmetric])
- unfolding frontier_of_closures eq
- using x that closure_of_restrict by fastforce
+ by (metis IntI closure_of_restrict eq fg frontier_of_closures that)
ultimately show ?thesis
using that by (auto simp flip: closure_of_restrict)
qed
show "\<exists>j. j \<in> {True,False} \<and> x \<in> ?T j \<and> (if P x then f x else g x) = ?f j x"
if "x \<in> topspace X" for x
- apply simp
- apply safe
- apply (metis Int_iff closure_of inf_sup_absorb mem_Collect_eq that)
- by (metis DiffI eq closure_of_subset_Int contra_subsetD mem_Collect_eq that)
+ by simp (metis in_closure_of mem_Collect_eq that)
qed (auto simp: f g)
lemma continuous_map_cases_alt:
@@ -877,8 +858,7 @@
show "continuous_map (subtopology X ?T) Y g"
by (simp add: contg)
have "X closure_of {x \<in> topspace X. p x \<notin> U} \<subseteq> X closure_of {x \<in> topspace X. p x \<in> topspace Z - U}"
- apply (rule closure_of_mono)
- using continuous_map_closedin contp by fastforce
+ by (smt (verit, del_insts) DiffI mem_Collect_eq subset_iff closure_of_mono continuous_map_closedin contp)
then show "X closure_of {x \<in> topspace X. p x \<notin> U} \<subseteq> ?T"
by (rule order_trans [OF _ continuous_map_closure_preimage_subset [OF contp]])
qed
@@ -1047,10 +1027,8 @@
unfolding retract_of_def retraction_def by force
lemma retraction_comp:
- "\<lbrakk>retraction S T f; retraction T U g\<rbrakk>
- \<Longrightarrow> retraction S U (g \<circ> f)"
-apply (auto simp: retraction_def intro: continuous_on_compose2)
-by blast
+ "\<lbrakk>retraction S T f; retraction T U g\<rbrakk> \<Longrightarrow> retraction S U (g \<circ> f)"
+ by (smt (verit, best) comp_apply continuous_on_compose image_comp retraction subset_iff)
lemma retract_of_trans [trans]:
assumes "S retract_of T" and "T retract_of U"
@@ -1092,12 +1070,15 @@
by (metis Topological_Spaces.connected_continuous_image retract_of_def retraction)
lemma retraction_openin_vimage_iff:
- "openin (top_of_set S) (S \<inter> r -` U) \<longleftrightarrow> openin (top_of_set T) U"
- if retraction: "retraction S T r" and "U \<subseteq> T"
- using retraction apply (rule retractionE)
- apply (rule continuous_right_inverse_imp_quotient_map [where g=r])
- using \<open>U \<subseteq> T\<close> apply (auto elim: continuous_on_subset)
- done
+ assumes r: "retraction S T r" and "U \<subseteq> T"
+ shows "openin (top_of_set S) (S \<inter> r -` U) \<longleftrightarrow> openin (top_of_set T) U" (is "?lhs = ?rhs")
+proof
+ show "?lhs \<Longrightarrow> ?rhs"
+ using r retraction_def retractionE
+ by (smt (verit, best) continuous_right_inverse_imp_quotient_map retraction_subset \<open>U \<subseteq> T\<close>)
+ show "?rhs \<Longrightarrow> ?lhs"
+ by (meson continuous_openin_preimage r retraction_def)
+qed
lemma retract_of_Times:
"\<lbrakk>S retract_of s'; T retract_of t'\<rbrakk> \<Longrightarrow> (S \<times> T) retract_of (s' \<times> t')"
@@ -1317,11 +1298,13 @@
qed
lemma path_connectedin_discrete_topology:
- "path_connectedin (discrete_topology U) S \<longleftrightarrow> S \<subseteq> U \<and> (\<exists>a. S \<subseteq> {a})"
- apply safe
- using path_connectedin_subset_topspace apply fastforce
- apply (meson connectedin_discrete_topology path_connectedin_imp_connectedin)
- using subset_singletonD by fastforce
+ "path_connectedin (discrete_topology U) S \<longleftrightarrow> S \<subseteq> U \<and> (\<exists>a. S \<subseteq> {a})" (is "?lhs = ?rhs")
+proof
+ show "?lhs \<Longrightarrow> ?rhs"
+ by (meson connectedin_discrete_topology path_connectedin_imp_connectedin)
+ show "?rhs \<Longrightarrow> ?lhs"
+ using subset_singletonD by fastforce
+qed
lemma path_connected_space_discrete_topology:
"path_connected_space (discrete_topology U) \<longleftrightarrow> (\<exists>a. U \<subseteq> {a})"
@@ -1444,17 +1427,14 @@
have "connected_component_of_set X x = \<Union> {T. connectedin X T \<and> x \<in> T}"
by (auto simp: connected_component_of_def)
then show ?thesis
- apply (rule ssubst)
- by (blast intro: connectedin_Union)
+ by (metis (no_types, lifting) InterI connectedin_Union emptyE mem_Collect_eq)
qed
lemma Union_connected_components_of:
"\<Union>(connected_components_of X) = topspace X"
unfolding connected_components_of_def
- apply (rule equalityI)
- apply (simp add: SUP_least connected_component_of_subset_topspace)
- using connected_component_of_refl by fastforce
+ using connected_component_in_topspace connected_component_of_refl by fastforce
lemma connected_components_of_maximal:
"\<lbrakk>C \<in> connected_components_of X; connectedin X S; ~disjnt C S\<rbrakk> \<Longrightarrow> S \<subseteq> C"
@@ -1465,15 +1445,13 @@
lemma pairwise_disjoint_connected_components_of:
"pairwise disjnt (connected_components_of X)"
unfolding connected_components_of_def pairwise_def
- apply clarify
- by (metis connected_component_of_disjoint connected_component_of_equiv)
+ by (smt (verit, best) connected_component_of_disjoint connected_component_of_eq imageE)
lemma complement_connected_components_of_Union:
"C \<in> connected_components_of X
\<Longrightarrow> topspace X - C = \<Union> (connected_components_of X - {C})"
- apply (rule equalityI)
- using Union_connected_components_of apply fastforce
- by (metis Diff_cancel Diff_subset Union_connected_components_of cSup_singleton diff_Union_pairwise_disjoint equalityE insert_subsetI pairwise_disjoint_connected_components_of)
+ by (metis Union_connected_components_of bot.extremum ccpo_Sup_singleton diff_Union_pairwise_disjoint
+ insert_subset pairwise_disjoint_connected_components_of)
lemma nonempty_connected_components_of:
"C \<in> connected_components_of X \<Longrightarrow> C \<noteq> {}"
@@ -1495,16 +1473,18 @@
qed
lemma connected_component_in_connected_components_of:
- "connected_component_of_set X a \<in> connected_components_of X \<longleftrightarrow> a \<in> topspace X"
- apply (rule iffI)
- using connected_component_of_eq_empty nonempty_connected_components_of apply fastforce
- by (simp add: connected_components_of_def)
+ "connected_component_of_set X a \<in> connected_components_of X \<longleftrightarrow> a \<in> topspace X"
+ by (metis (no_types, lifting) connected_component_of_eq_empty connected_components_of_def image_iff)
lemma connected_space_iff_components_eq:
"connected_space X \<longleftrightarrow> (\<forall>C \<in> connected_components_of X. \<forall>C' \<in> connected_components_of X. C = C')"
- apply (rule iffI)
- apply (force simp: connected_components_of_def connected_space_connected_component_set image_iff)
- by (metis connected_component_in_connected_components_of connected_component_of_refl connected_space_iff_connected_component mem_Collect_eq)
+ (is "?lhs = ?rhs")
+proof
+ show "?lhs \<Longrightarrow> ?rhs"
+ by (simp add: connected_components_of_def connected_space_connected_component_set)
+ show "?rhs \<Longrightarrow> ?lhs"
+ by (metis Union_connected_components_of Union_iff connected_space_subconnected connectedin_connected_components_of)
+qed
lemma connected_components_of_eq_empty:
"connected_components_of X = {} \<longleftrightarrow> topspace X = {}"
@@ -1522,10 +1502,11 @@
by (simp add: connected_components_of_empty_space connected_space_topspace_empty)
next
case False
- then show ?thesis
- by (metis (no_types, opaque_lifting) Union_connected_components_of ccpo_Sup_singleton
- connected_components_of_eq_empty connected_space_iff_components_eq insertI1 singletonD
- subsetI subset_singleton_iff)
+ then have "\<lbrakk>connected_components_of X \<subseteq> {S}\<rbrakk> \<Longrightarrow> topspace X = S"
+ by (metis Sup_empty Union_connected_components_of ccpo_Sup_singleton subset_singleton_iff)
+ with False show ?thesis
+ unfolding connected_components_of_def
+ by (metis connected_space_connected_component_set empty_iff image_subset_iff insert_iff)
qed
lemma connected_space_iff_components_subset_singleton:
--- a/src/HOL/Analysis/Extended_Real_Limits.thy Tue Jan 03 18:23:52 2023 +0100
+++ b/src/HOL/Analysis/Extended_Real_Limits.thy Tue Jan 03 19:55:35 2023 +0000
@@ -757,8 +757,8 @@
have "N > C" if "u N \<ge> n" for N
proof (rule ccontr)
assume "\<not>(N > C)"
- have "u N \<le> Max {u n| n. n \<le> C}"
- apply (rule Max_ge) using \<open>\<not>(N > C)\<close> by auto
+ then have "u N \<le> Max {u n| n. n \<le> C}"
+ using Max_ge by (simp add: setcompr_eq_image not_less)
then show False using \<open>u N \<ge> n\<close> \<open>n \<ge> M\<close> unfolding M_def by auto
qed
then have **: "{N. u N \<ge> n} \<subseteq> {C..}" by fastforce
@@ -782,7 +782,7 @@
then obtain N1 where N1: "\<And>N. N \<ge> N1 \<Longrightarrow> u N \<ge> n + 1"
using eventually_sequentially by auto
have "{N. u N \<le> n} \<subseteq> {..<N1}"
- apply auto using N1 by (metis Suc_eq_plus1 not_less not_less_eq_eq)
+ by (metis (no_types, lifting) N1 Suc_eq_plus1 lessThan_iff less_le_not_le mem_Collect_eq nle_le not_less_eq_eq subset_eq)
then show "finite {N. u N \<le> n}" by (simp add: finite_subset)
qed
@@ -794,7 +794,7 @@
{
fix N0::nat
have "N0 \<le> Max {N. u N \<le> n}" if "n \<ge> u N0" for n
- apply (rule Max.coboundedI) using pseudo_inverse_finite_set[OF assms] that by auto
+ by (simp add: assms pseudo_inverse_finite_set that)
then have "eventually (\<lambda>n. N0 \<le> Max {N. u N \<le> n}) sequentially"
using eventually_sequentially by blast
}
@@ -895,12 +895,12 @@
"continuous_on (UNIV::ereal set) abs"
proof -
have "continuous_on ({..0} \<union> {(0::ereal)..}) abs"
- apply (rule continuous_on_closed_Un, auto)
- apply (rule iffD1[OF continuous_on_cong, of "{..0}" _ "\<lambda>x. -x"])
- using less_eq_ereal_def apply (auto simp: continuous_uminus_ereal)
- apply (rule iffD1[OF continuous_on_cong, of "{0..}" _ "\<lambda>x. x"])
- apply (auto)
- done
+ proof (intro continuous_on_closed_Un continuous_intros)
+ show "continuous_on {..0::ereal} abs"
+ by (metis abs_ereal_ge0 abs_ereal_less0 continuous_on_eq antisym_conv1 atMost_iff continuous_uminus_ereal ereal_uminus_zero)
+ show "continuous_on {0::ereal..} abs"
+ by (metis abs_ereal_ge0 atLeast_iff continuous_on_eq continuous_on_id)
+ qed
moreover have "(UNIV::ereal set) = {..0} \<union> {(0::ereal)..}" by auto
ultimately show ?thesis by auto
qed
@@ -926,7 +926,7 @@
shows "((\<lambda>n. u n - v n) \<longlongrightarrow> l - m) F"
proof -
have "((\<lambda>n. e2ennreal(enn2ereal(u n) - enn2ereal(v n))) \<longlongrightarrow> e2ennreal(enn2ereal l - enn2ereal m)) F"
- apply (intro tendsto_intros) using assms by auto
+ by (intro tendsto_intros) (use assms in auto)
then show ?thesis by auto
qed
@@ -936,8 +936,7 @@
shows "((\<lambda>n. u n * v n) \<longlongrightarrow> l * m) F"
proof -
have "((\<lambda>n. e2ennreal(enn2ereal (u n) * enn2ereal (v n))) \<longlongrightarrow> e2ennreal(enn2ereal l * enn2ereal m)) F"
- apply (intro tendsto_intros) using assms apply auto
- using enn2ereal_inject zero_ennreal.rep_eq by fastforce+
+ by (intro tendsto_intros) (use assms enn2ereal_inject zero_ennreal.rep_eq in fastforce)+
moreover have "e2ennreal(enn2ereal (u n) * enn2ereal (v n)) = u n * v n" for n
by (subst times_ennreal.abs_eq[symmetric], auto simp: eq_onp_same_args)
moreover have "e2ennreal(enn2ereal l * enn2ereal m) = l * m"
@@ -1095,25 +1094,8 @@
{
fix S :: "ereal set"
assume om: "open S" "mono_set S" "x0 \<in> S"
- {
- assume "S = UNIV"
- then have "\<exists>N. \<forall>n\<ge>N. x n \<in> S"
- by auto
- }
- moreover
- {
- assume "S \<noteq> UNIV"
- then obtain B where B: "S = {B<..}"
- using om ereal_open_mono_set by auto
- then have "B < x0"
- using om by auto
- then have "\<exists>N. \<forall>n\<ge>N. x n \<in> S"
- unfolding B
- using \<open>x0 \<le> liminf x\<close> liminf_bounded_iff
- by auto
- }
- ultimately have "\<exists>N. \<forall>n\<ge>N. x n \<in> S"
- by auto
+ then have "\<exists>N. \<forall>n\<ge>N. x n \<in> S"
+ by (metis \<open>x0 \<le> liminf x\<close> ereal_open_mono_set greaterThan_iff liminf_bounded_iff om UNIV_I)
}
then show "?P x0"
by auto
@@ -1126,9 +1108,9 @@
proof -
obtain C where C: "limsup u < C" "C < \<infinity>" using assms ereal_dense2 by blast
then have "C = ereal(real_of_ereal C)" using ereal_real by force
- have "eventually (\<lambda>n. u n < C) sequentially" using C(1) unfolding Limsup_def
- apply (auto simp: INF_less_iff)
- using SUP_lessD eventually_mono by fastforce
+ have "eventually (\<lambda>n. u n < C) sequentially"
+ using SUP_lessD eventually_mono C(1)
+ by (fastforce simp: INF_less_iff Limsup_def)
then obtain N where N: "\<And>n. n \<ge> N \<Longrightarrow> u n < C" using eventually_sequentially by auto
define D where "D = max (real_of_ereal C) (Max {u n |n. n \<le> N})"
have "\<And>n. u n \<le> D"
@@ -1156,9 +1138,9 @@
proof -
obtain C where C: "liminf u > C" "C > -\<infinity>" using assms using ereal_dense2 by blast
then have "C = ereal(real_of_ereal C)" using ereal_real by force
- have "eventually (\<lambda>n. u n > C) sequentially" using C(1) unfolding Liminf_def
- apply (auto simp: less_SUP_iff)
- using eventually_elim2 less_INF_D by fastforce
+ have "eventually (\<lambda>n. u n > C) sequentially"
+ using eventually_elim2 less_INF_D C(1)
+ by (fastforce simp: less_SUP_iff Liminf_def)
then obtain N where N: "\<And>n. n \<ge> N \<Longrightarrow> u n > C" using eventually_sequentially by auto
define D where "D = min (real_of_ereal C) (Min {u n |n. n \<le> N})"
have "\<And>n. u n \<ge> D"
@@ -1172,7 +1154,8 @@
assume "\<not>(n \<le> N)"
then have "n \<ge> N" by simp
then have "u n > C" using N by auto
- then have "u n > real_of_ereal C" using \<open>C = ereal(real_of_ereal C)\<close> less_ereal.simps(1) by fastforce
+ then have "u n > real_of_ereal C"
+ using \<open>C = ereal(real_of_ereal C)\<close> less_ereal.simps(1) by fastforce
then show "u n \<ge> D" unfolding D_def by linarith
qed
qed
@@ -1189,12 +1172,12 @@
"limsup (\<lambda>n. u (n+1)) = limsup u"
proof -
have "(SUP m\<in>{n+1..}. u m) = (SUP m\<in>{n..}. u (m + 1))" for n
- apply (rule SUP_eq) using Suc_le_D by auto
+ by (rule SUP_eq) (use Suc_le_D in auto)
then have a: "(INF n. SUP m\<in>{n..}. u (m + 1)) = (INF n. (SUP m\<in>{n+1..}. u m))" by auto
have b: "(INF n. (SUP m\<in>{n+1..}. u m)) = (INF n\<in>{1..}. (SUP m\<in>{n..}. u m))"
- apply (rule INF_eq) using Suc_le_D by auto
+ by (rule INF_eq) (use Suc_le_D in auto)
have "(INF n\<in>{1..}. v n) = (INF n. v n)" if "decseq v" for v::"nat \<Rightarrow> 'a"
- apply (rule INF_eq) using \<open>decseq v\<close> decseq_Suc_iff by auto
+ by (rule INF_eq) (use \<open>decseq v\<close> decseq_Suc_iff in auto)
moreover have "decseq (\<lambda>n. (SUP m\<in>{n..}. u m))" by (simp add: SUP_subset_mono decseq_def)
ultimately have c: "(INF n\<in>{1..}. (SUP m\<in>{n..}. u m)) = (INF n. (SUP m\<in>{n..}. u m))" by simp
have "(INF n. Sup (u ` {n..})) = (INF n. SUP m\<in>{n..}. u (m + 1))" using a b c by simp
@@ -1213,12 +1196,12 @@
"liminf (\<lambda>n. u (n+1)) = liminf u"
proof -
have "(INF m\<in>{n+1..}. u m) = (INF m\<in>{n..}. u (m + 1))" for n
- apply (rule INF_eq) using Suc_le_D by (auto)
+ by (rule INF_eq) (use Suc_le_D in auto)
then have a: "(SUP n. INF m\<in>{n..}. u (m + 1)) = (SUP n. (INF m\<in>{n+1..}. u m))" by auto
have b: "(SUP n. (INF m\<in>{n+1..}. u m)) = (SUP n\<in>{1..}. (INF m\<in>{n..}. u m))"
- apply (rule SUP_eq) using Suc_le_D by (auto)
+ by (rule SUP_eq) (use Suc_le_D in auto)
have "(SUP n\<in>{1..}. v n) = (SUP n. v n)" if "incseq v" for v::"nat \<Rightarrow> 'a"
- apply (rule SUP_eq) using \<open>incseq v\<close> incseq_Suc_iff by auto
+ by (rule SUP_eq) (use \<open>incseq v\<close> incseq_Suc_iff in auto)
moreover have "incseq (\<lambda>n. (INF m\<in>{n..}. u m))" by (simp add: INF_superset_mono mono_def)
ultimately have c: "(SUP n\<in>{1..}. (INF m\<in>{n..}. u m)) = (SUP n. (INF m\<in>{n..}. u m))" by simp
have "(SUP n. Inf (u ` {n..})) = (SUP n. INF m\<in>{n..}. u (m + 1))" using a b c by simp
@@ -1229,7 +1212,8 @@
"liminf (\<lambda>n. u (n+k)) = liminf u"
proof (induction k)
case (Suc k)
- have "liminf (\<lambda>n. u (n+k+1)) = liminf (\<lambda>n. u (n+k))" using liminf_shift[where ?u="\<lambda>n. u(n+k)"] by simp
+ have "liminf (\<lambda>n. u (n+k+1)) = liminf (\<lambda>n. u (n+k))"
+ using liminf_shift[where ?u="\<lambda>n. u(n+k)"] by simp
then show ?case using Suc.IH by simp
qed (auto)
@@ -1392,8 +1376,7 @@
have "u i \<ge> u p"
proof (cases)
assume "i \<le> x"
- then have "i \<in> {N<..x}" using i by simp
- then show ?thesis using a by simp
+ then show ?thesis using a \<open>i \<in> {N<..y}\<close> by force
next
assume "\<not>(i \<le> x)"
then have "i > x" by simp
@@ -1608,7 +1591,7 @@
unfolding w_def using that by (auto simp: ereal_divide_eq)
ultimately have "eventually (\<lambda>n. (w o s) n / (u o s) n = (v o s) n) sequentially" using eventually_elim2 by force
moreover have "(\<lambda>n. (w o s) n / (u o s) n) \<longlonglongrightarrow> (liminf w) / a"
- apply (rule tendsto_divide_ereal[OF s(2) *]) using assms(2) assms(3) by auto
+ using "*" assms s tendsto_divide_ereal by fastforce
ultimately have "(v o s) \<longlonglongrightarrow> (liminf w) / a" using Lim_transform_eventually by fastforce
then have "liminf (v o s) = (liminf w) / a" by (simp add: tendsto_iff_Liminf_eq_Limsup)
then have "liminf v \<le> (liminf w) / a" by (metis liminf_subseq_mono s(1))
@@ -1628,7 +1611,7 @@
then have **: "abs(liminf (\<lambda>n. -u n)) \<noteq> \<infinity>" using assms(2) by auto
have "liminf (\<lambda>n. u n + v n) \<ge> liminf u + liminf v"
- apply (rule ereal_liminf_add_mono) using * by auto
+ using abs_ereal.simps by (metis (full_types) "*" ereal_liminf_add_mono)
then have up: "liminf (\<lambda>n. u n + v n) \<ge> a + liminf v" using \<open>liminf u = a\<close> by simp
have a: "liminf (\<lambda>n. (u n + v n) + (-u n)) \<ge> liminf (\<lambda>n. u n + v n) + liminf (\<lambda>n. -u n)"
--- a/src/HOL/Analysis/Polytope.thy Tue Jan 03 18:23:52 2023 +0100
+++ b/src/HOL/Analysis/Polytope.thy Tue Jan 03 19:55:35 2023 +0000
@@ -474,10 +474,7 @@
using order.trans by fastforce
next
case False
- then show ?thesis
- apply simp
- apply (erule ex_forward)
- by blast
+ then show ?thesis by fastforce
qed
lemma faces_of_translation:
@@ -661,23 +658,16 @@
lemma exposed_face_of:
"T exposed_face_of S \<longleftrightarrow>
- T face_of S \<and>
- (T = {} \<or> T = S \<or>
+ T face_of S \<and> (T = {} \<or> T = S \<or>
(\<exists>a b. a \<noteq> 0 \<and> S \<subseteq> {x. a \<bullet> x \<le> b} \<and> T = S \<inter> {x. a \<bullet> x = b}))"
-proof (cases "T = {}")
- case False
- show ?thesis
- proof (cases "T = S")
- case True then show ?thesis
- by (simp add: face_of_refl_eq)
- next
- case False
- with \<open>T \<noteq> {}\<close> show ?thesis
- apply (auto simp: exposed_face_of_def)
- apply (metis inner_zero_left)
- done
- qed
-qed auto
+ (is "?lhs = ?rhs")
+proof
+ show "?lhs \<Longrightarrow> ?rhs"
+ by (smt (verit) Collect_cong exposed_face_of_def hyperplane_eq_empty inf.absorb_iff1
+ inf_bot_right inner_zero_left)
+ show "?rhs \<Longrightarrow> ?lhs"
+ using exposed_face_of_def face_of_imp_convex by fastforce
+qed
lemma exposed_face_of_Int_supporting_hyperplane_le:
"\<lbrakk>convex S; \<And>x. x \<in> S \<Longrightarrow> a \<bullet> x \<le> b\<rbrakk> \<Longrightarrow> (S \<inter> {x. a \<bullet> x = b}) exposed_face_of S"
@@ -780,10 +770,7 @@
proof -
have "\<And>x y. \<lbrakk>z = u \<bullet> (x + y); x \<in> S; y \<in> T\<rbrakk>
\<Longrightarrow> u \<bullet> x = u \<bullet> a0 \<and> u \<bullet> y = u \<bullet> b0"
- using z p \<open>a0 \<in> S\<close> \<open>b0 \<in> T\<close>
- apply (simp add: inner_right_distrib)
- apply (metis add_le_cancel_right antisym lez [unfolded inner_right_distrib] add.commute)
- done
+ by (smt (verit, best) z p \<open>a0 \<in> S\<close> \<open>b0 \<in> T\<close> inner_right_distrib lez)
then show ?thesis
using feq by blast
qed
@@ -815,18 +802,18 @@
then show ?thesis
proof
assume "affine hull S \<inter> {x. - a \<bullet> x \<le> - b} = {}"
- then show ?thesis
- apply (rule_tac x="0" in exI)
- apply (rule_tac x="1" in exI)
- using hull_subset by fastforce
+ then show ?thesis
+ apply (rule_tac x="0" in exI)
+ apply (rule_tac x="1" in exI)
+ using hull_subset by fastforce
+ next
+ assume "affine hull S \<subseteq> {x. - a \<bullet> x \<le> - b}"
+ then show ?thesis
+ apply (rule_tac x="0" in exI)
+ apply (rule_tac x="0" in exI)
+ using Ssub hull_subset by fastforce
+ qed
next
- assume "affine hull S \<subseteq> {x. - a \<bullet> x \<le> - b}"
- then show ?thesis
- apply (rule_tac x="0" in exI)
- apply (rule_tac x="0" in exI)
- using Ssub hull_subset by fastforce
- qed
- next
case False
then obtain a' b' where "a' \<noteq> 0"
and le: "affine hull S \<inter> {x. a' \<bullet> x \<le> b'} = affine hull S \<inter> {x. - a \<bullet> x \<le> - b}"
@@ -1472,9 +1459,8 @@
have "\<not> affine_dependent c"
using \<open>c \<subseteq> S\<close> affine_dependent_subset assms by blast
with affs have "card (S - c) = 1"
- apply (simp add: aff_dim_affine_independent [symmetric] aff_dim_convex_hull)
- by (metis aff_dim_affine_independent aff_independent_finite One_nat_def \<open>c \<subseteq> S\<close> add.commute
- add_diff_cancel_right' assms card_Diff_subset card_mono of_nat_1 of_nat_diff of_nat_eq_iff)
+ by (smt (verit) \<open>c \<subseteq> S\<close> aff_dim_affine_independent aff_independent_finite assms card_Diff_subset
+ card_mono of_nat_diff of_nat_eq_1_iff)
then obtain u where u: "u \<in> S - c"
by (metis DiffI \<open>c \<subseteq> S\<close> aff_independent_finite assms cancel_comm_monoid_add_class.diff_cancel
card_Diff_subset subsetI subset_antisym zero_neq_one)
@@ -3361,11 +3347,9 @@
ultimately show "convex hull (J - {?z}) \<in> \<U> \<inter> Pow (rel_frontier C)" by auto
let ?F = "convex hull insert ?z (convex hull (J - {?z}))"
have "F \<subseteq> ?F"
- apply (clarsimp simp: \<open>F = convex hull J\<close>)
- by (metis True subsetD hull_mono hull_subset subset_insert_iff)
+ by (simp add: \<open>F = convex hull J\<close> hull_mono hull_subset subset_insert_iff)
moreover have "?F \<subseteq> F"
- apply (clarsimp simp: \<open>F = convex hull J\<close>)
- by (metis (no_types, lifting) True convex_hull_eq_empty convex_hull_insert_segments hull_hull insert_Diff)
+ by (metis True \<open>F = convex hull J\<close> hull_insert insert_Diff set_eq_subset)
ultimately
show "F \<in> {?F}" by auto
qed
--- a/src/HOL/Complex_Analysis/Complex_Singularities.thy Tue Jan 03 18:23:52 2023 +0100
+++ b/src/HOL/Complex_Analysis/Complex_Singularities.thy Tue Jan 03 19:55:35 2023 +0000
@@ -43,16 +43,14 @@
hence "continuous_on (s-{z}) (inverse o f)" unfolding comp_def
by (auto elim!:continuous_on_inverse simp add:non_z)
hence "continuous_on (s-{z}) g" unfolding g_def
- apply (subst continuous_on_cong[where t="s-{z}" and g="inverse o f"])
- by auto
+ using continuous_on_eq by fastforce
ultimately have "continuous_on s g" using open_delete[OF \<open>open s\<close>] \<open>open s\<close>
by (auto simp add:continuous_on_eq_continuous_at)
moreover have "(inverse o f) holomorphic_on (s-{z})"
unfolding comp_def using f_holo
by (auto elim!:holomorphic_on_inverse simp add:non_z)
hence "g holomorphic_on (s-{z})"
- apply (subst holomorphic_cong[where t="s-{z}" and g="inverse o f"])
- by (auto simp add:g_def)
+ using g_def holomorphic_transform by force
ultimately show ?thesis unfolding g_def using \<open>open s\<close>
by (auto elim!: no_isolated_singularity)
qed
@@ -82,9 +80,8 @@
shows "is_pole (\<lambda>z. f z / g z) z"
proof -
have "filterlim (\<lambda>z. f z * inverse (g z)) at_infinity (at z)"
- by (intro tendsto_mult_filterlim_at_infinity[of _ "f z"]
- filterlim_compose[OF filterlim_inverse_at_infinity])+
- (insert assms, auto simp: isCont_def)
+ using assms filterlim_compose filterlim_inverse_at_infinity isCont_def
+ tendsto_mult_filterlim_at_infinity by blast
thus ?thesis by (simp add: field_split_simps is_pole_def)
qed
@@ -132,9 +129,7 @@
have "(h \<longlongrightarrow> 0) (at z within ball z r)"
proof (rule Lim_transform_within[OF _ \<open>r>0\<close>, where f="\<lambda>w. (w - z) powr (n - m) * g w"])
have "\<forall>w\<in>ball z r-{z}. h w = (w-z)powr(n-m) * g w"
- using \<open>n>m\<close> asm \<open>r>0\<close>
- apply (auto simp add:field_simps powr_diff)
- by force
+ using \<open>n>m\<close> asm \<open>r>0\<close> by (simp add: field_simps powr_diff) force
then show "\<lbrakk>x' \<in> ball z r; 0 < dist x' z;dist x' z < r\<rbrakk>
\<Longrightarrow> (x' - z) powr (n - m) * g x' = h x'" for x' by auto
next
@@ -142,8 +137,8 @@
define f' where "f' \<equiv> \<lambda>x. (x - z) powr (n-m)"
have "f' z=0" using \<open>n>m\<close> unfolding f'_def by auto
moreover have "continuous F f'" unfolding f'_def F_def continuous_def
- apply (subst Lim_ident_at)
- using \<open>n>m\<close> by (auto intro!:tendsto_powr_complex_0 tendsto_eq_intros)
+ using \<open>n>m\<close>
+ by (auto simp add: Lim_ident_at intro!:tendsto_powr_complex_0 tendsto_eq_intros)
ultimately have "(f' \<longlongrightarrow> 0) F" unfolding F_def
by (simp add: continuous_within)
moreover have "(g \<longlongrightarrow> g z) F"
@@ -162,8 +157,7 @@
have "(g \<longlongrightarrow> 0) (at z within ball z r)"
proof (rule Lim_transform_within[OF _ \<open>r>0\<close>, where f="\<lambda>w. (w - z) powr (m - n) * h w"])
have "\<forall>w\<in>ball z r -{z}. g w = (w-z) powr (m-n) * h w" using \<open>m>n\<close> asm
- apply (auto simp add:field_simps powr_diff)
- by force
+ by (simp add:field_simps powr_diff) force
then show "\<lbrakk>x' \<in> ball z r; 0 < dist x' z;dist x' z < r\<rbrakk>
\<Longrightarrow> (x' - z) powr (m - n) * h x' = g x'" for x' by auto
next
@@ -171,8 +165,8 @@
define f' where "f' \<equiv>\<lambda>x. (x - z) powr (m-n)"
have "f' z=0" using \<open>m>n\<close> unfolding f'_def by auto
moreover have "continuous F f'" unfolding f'_def F_def continuous_def
- apply (subst Lim_ident_at)
- using \<open>m>n\<close> by (auto intro!:tendsto_powr_complex_0 tendsto_eq_intros)
+ using \<open>m>n\<close>
+ by (auto simp: Lim_ident_at intro!:tendsto_powr_complex_0 tendsto_eq_intros)
ultimately have "(f' \<longlongrightarrow> 0) F" unfolding F_def
by (simp add: continuous_within)
moreover have "(h \<longlongrightarrow> h z) F"
@@ -222,22 +216,22 @@
"\<exists>z'. (h \<longlongrightarrow> z') (at z)" "isolated_singularity_at h z" "\<exists>\<^sub>Fw in (at z). h w\<noteq>0"
for h
proof -
- from that(2) obtain r where "r>0" "h analytic_on ball z r - {z}"
+ from that(2) obtain r where "r>0" and r: "h analytic_on ball z r - {z}"
unfolding isolated_singularity_at_def by auto
obtain z' where "(h \<longlongrightarrow> z') (at z)" using \<open>\<exists>z'. (h \<longlongrightarrow> z') (at z)\<close> by auto
define h' where "h'=(\<lambda>x. if x=z then z' else h x)"
have "h' holomorphic_on ball z r"
- apply (rule no_isolated_singularity'[of "{z}"])
- subgoal by (metis LIM_equal Lim_at_imp_Lim_at_within \<open>h \<midarrow>z\<rightarrow> z'\<close> empty_iff h'_def insert_iff)
- subgoal using \<open>h analytic_on ball z r - {z}\<close> analytic_imp_holomorphic h'_def holomorphic_transform
- by fastforce
- by auto
+ proof (rule no_isolated_singularity'[of "{z}"])
+ show "\<And>w. w \<in> {z} \<Longrightarrow> (h' \<longlongrightarrow> h' w) (at w within ball z r)"
+ by (simp add: LIM_cong Lim_at_imp_Lim_at_within \<open>h \<midarrow>z\<rightarrow> z'\<close> h'_def)
+ show "h' holomorphic_on ball z r - {z}"
+ using r analytic_imp_holomorphic h'_def holomorphic_transform by fastforce
+ qed auto
have ?thesis when "z'=0"
proof -
have "h' z=0" using that unfolding h'_def by auto
moreover have "\<not> h' constant_on ball z r"
using \<open>\<exists>\<^sub>Fw in (at z). h w\<noteq>0\<close> unfolding constant_on_def frequently_def eventually_at h'_def
- apply simp
by (metis \<open>0 < r\<close> centre_in_ball dist_commute mem_ball that)
moreover note \<open>h' holomorphic_on ball z r\<close>
ultimately obtain g r1 n where "0 < n" "0 < r1" "ball z r1 \<subseteq> ball z r" and
@@ -278,7 +272,7 @@
ultimately show ?thesis by auto
qed
- have ?thesis when "\<exists>x. (f \<longlongrightarrow> x) (at z)"
+ have ?thesis when "\<exists>x. (f \<longlongrightarrow> x) (at z)"
apply (rule_tac imp_unique[unfolded P_def])
using P_exist[OF that(1) f_iso non_zero] unfolding P_def .
moreover have ?thesis when "is_pole f z"
@@ -292,29 +286,23 @@
using that eventually_at[of "\<lambda>x. f x\<noteq>0" z UNIV,simplified] by (auto simp add:dist_commute)
obtain e2 where e2:"e2>0" "f holomorphic_on ball z e2 - {z}"
using f_iso analytic_imp_holomorphic unfolding isolated_singularity_at_def by auto
- define e where "e=min e1 e2"
show ?thesis
- apply (rule that[of e])
- using e1 e2 unfolding e_def by auto
+ using e1 e2 by (force intro: that[of "min e1 e2"])
qed
define h where "h \<equiv> \<lambda>x. inverse (f x)"
-
have "\<exists>n g r. P h n g r"
proof -
- have "h \<midarrow>z\<rightarrow> 0"
+ have "(\<lambda>x. inverse (f x)) analytic_on ball z e - {z}"
+ by (metis e_holo e_nz open_ball analytic_on_open holomorphic_on_inverse open_delete)
+ moreover have "h \<midarrow>z\<rightarrow> 0"
using Lim_transform_within_open assms(2) h_def is_pole_tendsto that by fastforce
moreover have "\<exists>\<^sub>Fw in (at z). h w\<noteq>0"
- using non_zero
- apply (elim frequently_rev_mp)
- unfolding h_def eventually_at by (auto intro:exI[where x=1])
- moreover have "isolated_singularity_at h z"
+ using non_zero by (simp add: h_def)
+ ultimately show ?thesis
+ using P_exist[of h] \<open>e > 0\<close>
unfolding isolated_singularity_at_def h_def
- apply (rule exI[where x=e])
- using e_holo e_nz \<open>e>0\<close> by (metis open_ball analytic_on_open
- holomorphic_on_inverse open_delete)
- ultimately show ?thesis
- using P_exist[of h] by auto
+ by blast
qed
then obtain n g r
where "0 < r" and
@@ -324,9 +312,8 @@
have "P f (-n) (inverse o g) r"
proof -
have "f w = inverse (g w) * (w - z) powr of_int (- n)" when "w\<in>cball z r - {z}" for w
- using g_fac[rule_format,of w] that unfolding h_def
- apply (auto simp add:powr_minus )
- by (metis inverse_inverse_eq inverse_mult_distrib)
+ by (metis g_fac h_def inverse_inverse_eq inverse_mult_distrib of_int_minus
+ powr_minus that)
then show ?thesis
unfolding P_def comp_def
using \<open>r>0\<close> g_holo g_fac \<open>g z\<noteq>0\<close> by (auto intro:holomorphic_intros)
@@ -378,33 +365,31 @@
have "(\<lambda>w. (f w) ^ (nat n)) \<midarrow>z\<rightarrow> x ^ nat n"
using that assms unfolding filterlim_at by (auto intro!:tendsto_eq_intros)
then have "fp \<midarrow>z\<rightarrow> x ^ nat n" unfolding fp_def
- apply (elim Lim_transform_within[where d=1],simp)
- by (metis less_le powr_0 powr_of_int that zero_less_nat_eq zero_power)
+ by (smt (verit, best) LIM_equal of_int_of_nat power_eq_0_iff powr_nat that zero_less_nat_eq)
then show ?thesis unfolding not_essential_def fp_def by auto
qed
moreover have ?thesis when "n=0"
proof -
- have "fp \<midarrow>z\<rightarrow> 1 "
- apply (subst tendsto_cong[where g="\<lambda>_.1"])
- using that filterlim_at_within_not_equal[OF assms,of 0] unfolding fp_def by auto
+ have "\<forall>\<^sub>F x in at z. fp x = 1"
+ using that filterlim_at_within_not_equal[OF assms] by (auto simp: fp_def)
+ then have "fp \<midarrow>z\<rightarrow> 1"
+ by (simp add: tendsto_eventually)
then show ?thesis unfolding fp_def not_essential_def by auto
qed
moreover have ?thesis when "n<0"
proof (cases "x=0")
case True
- have "LIM w (at z). inverse ((f w) ^ (nat (-n))) :> at_infinity"
- apply (subst filterlim_inverse_at_iff[symmetric],simp)
- apply (rule filterlim_atI)
- subgoal using assms True that unfolding filterlim_at by (auto intro!:tendsto_eq_intros)
- subgoal using filterlim_at_within_not_equal[OF assms,of 0]
- by (eventually_elim,insert that,auto)
- done
+ have "(\<lambda>x. f x ^ nat (- n)) \<midarrow>z\<rightarrow> 0"
+ using assms True that unfolding filterlim_at by (auto intro!:tendsto_eq_intros)
+ moreover have "\<forall>\<^sub>F x in at z. f x ^ nat (- n) \<noteq> 0"
+ by (smt (verit) True assms eventually_at_topological filterlim_at power_eq_0_iff)
+ ultimately have "LIM w (at z). inverse ((f w) ^ (nat (-n))) :> at_infinity"
+ by (metis filterlim_atI filterlim_compose filterlim_inverse_at_infinity)
then have "LIM w (at z). fp w :> at_infinity"
proof (elim filterlim_mono_eventually)
show "\<forall>\<^sub>F x in at z. inverse (f x ^ nat (- n)) = fp x"
using filterlim_at_within_not_equal[OF assms,of 0] unfolding fp_def
- apply eventually_elim
- using powr_of_int that by auto
+ by (smt (verit, ccfv_threshold) eventually_mono powr_of_int that)
qed auto
then show ?thesis unfolding fp_def not_essential_def is_pole_def by auto
next
@@ -412,10 +397,9 @@
let ?xx= "inverse (x ^ (nat (-n)))"
have "(\<lambda>w. inverse ((f w) ^ (nat (-n)))) \<midarrow>z\<rightarrow>?xx"
using assms False unfolding filterlim_at by (auto intro!:tendsto_eq_intros)
- then have "fp \<midarrow>z\<rightarrow>?xx"
- apply (elim Lim_transform_within[where d=1],simp)
- unfolding fp_def by (metis inverse_zero nat_mono_iff nat_zero_as_int neg_0_less_iff_less
- not_le power_eq_0_iff powr_0 powr_of_int that)
+ then have "fp \<midarrow>z\<rightarrow> ?xx"
+ by (smt (verit) LIM_cong fp_def inverse_nonzero_iff_nonzero power_eq_0_iff powr_eq_0_iff
+ powr_of_int that zero_less_nat_eq)
then show ?thesis unfolding fp_def not_essential_def by auto
qed
ultimately show ?thesis by linarith
@@ -433,14 +417,10 @@
using assms(2) unfolding eventually_at by auto
define r3 where "r3=min r1 r2"
have "(\<lambda>w. (f w) powr of_int n) holomorphic_on ball z r3 - {z}"
- apply (rule holomorphic_on_powr_of_int)
- subgoal unfolding r3_def using r1 by auto
- subgoal unfolding r3_def using r2 by (auto simp add:dist_commute)
- done
+ by (intro holomorphic_on_powr_of_int) (use r1 r2 in \<open>auto simp: dist_commute r3_def\<close>)
moreover have "r3>0" unfolding r3_def using \<open>0 < r1\<close> \<open>0 < r2\<close> by linarith
- ultimately show ?thesis unfolding isolated_singularity_at_def
- apply (subst (asm) analytic_on_open[symmetric])
- by auto
+ ultimately show ?thesis
+ by (meson open_ball analytic_on_open isolated_singularity_at_def open_delete)
qed
lemma non_zero_neighbour:
@@ -478,19 +458,17 @@
case True
from isolated_zeros[OF holo \<open>open S\<close> \<open>connected S\<close> \<open>z \<in> S\<close> True \<open>\<beta> \<in> S\<close> \<open>f \<beta> \<noteq> 0\<close>]
obtain r where "0 < r" "ball z r \<subseteq> S" "\<forall>w \<in> ball z r - {z}.f w \<noteq> 0" by metis
- then show ?thesis unfolding eventually_at
- apply (rule_tac x=r in exI)
- by (auto simp add:dist_commute)
+ then show ?thesis
+ by (smt (verit) open_ball centre_in_ball eventually_at_topological insertE insert_Diff subsetD)
next
case False
obtain r1 where r1:"r1>0" "\<forall>y. dist z y < r1 \<longrightarrow> f y \<noteq> 0"
using continuous_at_avoid[of z f, OF _ False] assms(2,4) continuous_on_eq_continuous_at
holo holomorphic_on_imp_continuous_on by blast
obtain r2 where r2:"r2>0" "ball z r2 \<subseteq> S"
- using assms(2) assms(4) openE by blast
+ using assms openE by blast
show ?thesis unfolding eventually_at
- apply (rule_tac x="min r1 r2" in exI)
- using r1 r2 by (auto simp add:dist_commute)
+ by (metis (no_types) dist_commute dual_order.strict_trans linorder_less_linear mem_ball r1 r2 subsetD)
qed
lemma not_essential_times[singularity_intros]:
@@ -541,10 +519,9 @@
have "(\<lambda>w. (fp w * gp w) * (w - z) ^ (nat (fn+gn))) \<midarrow>z\<rightarrow>0"
using that by (auto intro!:tendsto_eq_intros)
then have "fg \<midarrow>z\<rightarrow> 0"
- apply (elim Lim_transform_within[OF _ \<open>r1>0\<close>])
- by (metis (no_types, opaque_lifting) Diff_iff cball_trivial dist_commute dist_self
- eq_iff_diff_eq_0 fg_times less_le linorder_not_le mem_ball mem_cball powr_of_int
- that)
+ using Lim_transform_within[OF _ \<open>r1>0\<close>]
+ by (smt (verit, ccfv_SIG) DiffI dist_commute dist_nz fg_times mem_ball powr_of_int right_minus_eq
+ singletonD that)
then show ?thesis unfolding not_essential_def fg_def by auto
qed
moreover have ?thesis when "fn+gn=0"