# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1675698083 0
# Node ID 8f2e6186408f742cad316846deb482f0d7bdaf18
# Parent  7d7786585ab0d8dbd7ce56d8b5361c2d5e3a4401
Some more new material and some tidying of existing proofs

diff -r 7d7786585ab0 -r 8f2e6186408f src/HOL/Analysis/Complex_Analysis_Basics.thy
--- a/src/HOL/Analysis/Complex_Analysis_Basics.thy	Sun Feb 05 20:09:39 2023 +0100
+++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy	Mon Feb 06 15:41:23 2023 +0000
@@ -6,7 +6,7 @@
 text \<open>Definitions of analytic and holomorphic functions, limit theorems, complex differentiation\<close>
 
 theory Complex_Analysis_Basics
-  imports Derivative "HOL-Library.Nonpos_Ints"
+  imports Derivative "HOL-Library.Nonpos_Ints" Uncountable_Sets
 begin
 
 subsection\<^marker>\<open>tag unimportant\<close>\<open>General lemmas\<close>
@@ -51,6 +51,50 @@
   by (intro open_Collect_less closed_Collect_le closed_Collect_eq continuous_on_Re
             continuous_on_Im continuous_on_id continuous_on_const)+
 
+lemma uncountable_halfspace_Im_gt: "uncountable {z. Im z > c}"
+proof -
+  obtain r where r: "r > 0" "ball ((c + 1) *\<^sub>R \<i>) r \<subseteq> {z. Im z > c}"
+    using open_halfspace_Im_gt[of c] unfolding open_contains_ball by force
+  then show ?thesis
+    using countable_subset uncountable_ball by blast
+qed
+
+lemma uncountable_halfspace_Im_lt: "uncountable {z. Im z < c}"
+proof -
+  obtain r where r: "r > 0" "ball ((c - 1) *\<^sub>R \<i>) r \<subseteq> {z. Im z < c}"
+    using open_halfspace_Im_lt[of c] unfolding open_contains_ball by force
+  then show ?thesis
+    using countable_subset uncountable_ball by blast
+qed
+
+lemma uncountable_halfspace_Re_gt: "uncountable {z. Re z > c}"
+proof -
+  obtain r where r: "r > 0" "ball (of_real(c + 1)) r \<subseteq> {z. Re z > c}"
+    using open_halfspace_Re_gt[of c] unfolding open_contains_ball by force
+  then show ?thesis
+    using countable_subset uncountable_ball by blast
+qed
+
+lemma uncountable_halfspace_Re_lt: "uncountable {z. Re z < c}"
+proof -
+  obtain r where r: "r > 0" "ball (of_real(c - 1)) r \<subseteq> {z. Re z < c}"
+    using open_halfspace_Re_lt[of c] unfolding open_contains_ball by force
+  then show ?thesis
+    using countable_subset uncountable_ball by blast
+qed
+
+lemma connected_halfspace_Im_gt [intro]: "connected {z. c < Im z}"
+  by (intro convex_connected convex_halfspace_Im_gt)
+
+lemma connected_halfspace_Im_lt [intro]: "connected {z. c > Im z}"
+  by (intro convex_connected convex_halfspace_Im_lt)
+
+lemma connected_halfspace_Re_gt [intro]: "connected {z. c < Re z}"
+  by (intro convex_connected convex_halfspace_Re_gt)
+
+lemma connected_halfspace_Re_lt [intro]: "connected {z. c > Re z}"
+  by (intro convex_connected convex_halfspace_Re_lt)
+  
 lemma closed_complex_Reals: "closed (\<real> :: complex set)"
 proof -
   have "(\<real> :: complex set) = {z. Im z = 0}"
diff -r 7d7786585ab0 -r 8f2e6186408f src/HOL/Analysis/Complex_Transcendental.thy
--- a/src/HOL/Analysis/Complex_Transcendental.thy	Sun Feb 05 20:09:39 2023 +0100
+++ b/src/HOL/Analysis/Complex_Transcendental.thy	Mon Feb 06 15:41:23 2023 +0000
@@ -84,6 +84,41 @@
   "f holomorphic_on s \<Longrightarrow> (\<lambda>x. exp (f x)) holomorphic_on s"
   using holomorphic_on_compose[OF _ holomorphic_on_exp] by (simp add: o_def)
 
+lemma exp_analytic_on [analytic_intros]:
+  assumes "f analytic_on A"
+  shows   "(\<lambda>z. exp (f z)) analytic_on A"
+  by (metis analytic_on_holomorphic assms holomorphic_on_exp')
+
+lemma
+  assumes "\<And>w. w \<in> A \<Longrightarrow> exp (f w) = w"
+  assumes "f holomorphic_on A" "z \<in> A" "open A"
+  shows   deriv_complex_logarithm: "deriv f z = 1 / z"
+    and   has_field_derivative_complex_logarithm: "(f has_field_derivative 1 / z) (at z)"
+proof -
+  have [simp]: "z \<noteq> 0"
+    using assms(1)[of z] assms(3) by auto
+  have deriv [derivative_intros]: "(f has_field_derivative deriv f z) (at z)"
+    using assms holomorphic_derivI by blast
+  have "((\<lambda>w. w) has_field_derivative 1) (at z)"
+    by (intro derivative_intros)
+  also have "?this \<longleftrightarrow> ((\<lambda>w. exp (f w)) has_field_derivative 1) (at z)"
+  proof (rule DERIV_cong_ev)
+    have "eventually (\<lambda>w. w \<in> A) (nhds z)"
+      using assms by (intro eventually_nhds_in_open) auto
+    thus "eventually (\<lambda>w. w = exp (f w)) (nhds z)"
+      by eventually_elim (use assms in auto)
+  qed auto
+  finally have "((\<lambda>w. exp (f w)) has_field_derivative 1) (at z)" .
+  moreover have "((\<lambda>w. exp (f w)) has_field_derivative exp (f z) * deriv f z) (at z)"
+    by (rule derivative_eq_intros refl)+
+  ultimately have "exp (f z) * deriv f z = 1"
+    using DERIV_unique by blast
+  with assms show "deriv f z = 1 / z"
+    by (simp add: field_simps)
+  with deriv show "(f has_field_derivative 1 / z) (at z)"
+    by simp
+qed
+  
 subsection\<open>Euler and de Moivre formulas\<close>
 
 text\<open>The sine series times \<^term>\<open>i\<close>\<close>
@@ -2602,6 +2637,9 @@
 lemma norm_powr_real: "w \<in> \<real> \<Longrightarrow> 0 < Re w \<Longrightarrow> norm(w powr z) = exp(Re z * ln(Re w))"
   using Ln_Reals_eq norm_exp_eq_Re by (auto simp: Im_Ln_eq_0 powr_def norm_complex_def)
 
+lemma norm_powr_real_powr': "w \<in> \<real> \<Longrightarrow> norm (z powr w) = norm z powr Re w"
+  by (auto simp: powr_def Reals_def)
+
 lemma powr_complexpow [simp]:
   fixes x::complex shows "x \<noteq> 0 \<Longrightarrow> x powr (of_nat n) = x^n"
   by (induct n) (auto simp: ac_simps powr_add)
diff -r 7d7786585ab0 -r 8f2e6186408f src/HOL/Analysis/Continuum_Not_Denumerable.thy
--- a/src/HOL/Analysis/Continuum_Not_Denumerable.thy	Sun Feb 05 20:09:39 2023 +0100
+++ b/src/HOL/Analysis/Continuum_Not_Denumerable.thy	Mon Feb 06 15:41:23 2023 +0000
@@ -176,9 +176,7 @@
 qed
 
 lemma uncountable_closed_interval: "uncountable {a..b} \<longleftrightarrow> a < b" for a b :: real
-  apply (rule iffI)
-   apply (metis atLeastAtMost_singleton atLeastatMost_empty countable_finite finite.emptyI finite_insert linorder_neqE_linordered_idom)
-  using real_interval_avoid_countable_set by fastforce
+  using infinite_Icc_iff by (fastforce dest: countable_finite real_interval_avoid_countable_set)
 
 lemma open_minus_countable:
   fixes S A :: "real set"
diff -r 7d7786585ab0 -r 8f2e6186408f src/HOL/Analysis/Elementary_Topology.thy
--- a/src/HOL/Analysis/Elementary_Topology.thy	Sun Feb 05 20:09:39 2023 +0100
+++ b/src/HOL/Analysis/Elementary_Topology.thy	Mon Feb 06 15:41:23 2023 +0000
@@ -618,31 +618,18 @@
 lemma islimpt_Un: "x islimpt (S \<union> T) \<longleftrightarrow> x islimpt S \<or> x islimpt T"
   by (simp add: islimpt_iff_eventually eventually_conj_iff)
 
+lemma islimpt_finite_union_iff:
+  assumes "finite A"
+  shows   "z islimpt (\<Union>x\<in>A. B x) \<longleftrightarrow> (\<exists>x\<in>A. z islimpt B x)"
+  using assms by (induction rule: finite_induct) (simp_all add: islimpt_Un)
 
 lemma islimpt_insert:
   fixes x :: "'a::t1_space"
   shows "x islimpt (insert a s) \<longleftrightarrow> x islimpt s"
 proof
-  assume *: "x islimpt (insert a s)"
-  show "x islimpt s"
-  proof (rule islimptI)
-    fix t
-    assume t: "x \<in> t" "open t"
-    show "\<exists>y\<in>s. y \<in> t \<and> y \<noteq> x"
-    proof (cases "x = a")
-      case True
-      obtain y where "y \<in> insert a s" "y \<in> t" "y \<noteq> x"
-        using * t by (rule islimptE)
-      with \<open>x = a\<close> show ?thesis by auto
-    next
-      case False
-      with t have t': "x \<in> t - {a}" "open (t - {a})"
-        by (simp_all add: open_Diff)
-      obtain y where "y \<in> insert a s" "y \<in> t - {a}" "y \<noteq> x"
-        using * t' by (rule islimptE)
-      then show ?thesis by auto
-    qed
-  qed
+  assume "x islimpt (insert a s)"
+  then show "x islimpt s"
+    by (metis closed_limpt closed_singleton empty_iff insert_iff insert_is_Un islimpt_Un islimpt_def)
 next
   assume "x islimpt s"
   then show "x islimpt (insert a s)"
diff -r 7d7786585ab0 -r 8f2e6186408f src/HOL/Analysis/Homeomorphism.thy
--- a/src/HOL/Analysis/Homeomorphism.thy	Sun Feb 05 20:09:39 2023 +0100
+++ b/src/HOL/Analysis/Homeomorphism.thy	Mon Feb 06 15:41:23 2023 +0000
@@ -1017,6 +1017,14 @@
                         pairwise disjnt v \<and>
                         (\<forall>u \<in> v. \<exists>q. homeomorphism u T p q)))"
 
+lemma covering_spaceI [intro?]:
+  assumes "continuous_on c p" "p ` c = S"
+          "\<And>x. x \<in> S \<Longrightarrow> \<exists>T. x \<in> T \<and> openin (top_of_set S) T \<and>
+                             (\<exists>v. \<Union>v = c \<inter> p -` T \<and> (\<forall>u \<in> v. openin (top_of_set c) u) \<and>
+                             pairwise disjnt v \<and> (\<forall>u \<in> v. \<exists>q. homeomorphism u T p q))"
+  shows "covering_space c p S"
+  using assms unfolding covering_space_def by auto
+
 lemma covering_space_imp_continuous: "covering_space c p S \<Longrightarrow> continuous_on c p"
   by (simp add: covering_space_def)
 
diff -r 7d7786585ab0 -r 8f2e6186408f src/HOL/Analysis/Homotopy.thy
--- a/src/HOL/Analysis/Homotopy.thy	Sun Feb 05 20:09:39 2023 +0100
+++ b/src/HOL/Analysis/Homotopy.thy	Mon Feb 06 15:41:23 2023 +0000
@@ -5,7 +5,7 @@
 section \<open>Homotopy of Maps\<close>
 
 theory Homotopy
-  imports Path_Connected Continuum_Not_Denumerable Product_Topology
+  imports Path_Connected Product_Topology Uncountable_Sets
 begin
 
 definition\<^marker>\<open>tag important\<close> homotopic_with
@@ -4169,144 +4169,16 @@
     by blast
 qed
 
-
-subsection\<^marker>\<open>tag unimportant\<close>\<open>Some Uncountable Sets\<close>
-
-lemma uncountable_closed_segment:
-  fixes a :: "'a::real_normed_vector"
-  assumes "a \<noteq> b" shows "uncountable (closed_segment a b)"
-unfolding path_image_linepath [symmetric] path_image_def
-  using inj_on_linepath [OF assms] uncountable_closed_interval [of 0 1]
-        countable_image_inj_on by auto
-
-lemma uncountable_open_segment:
-  fixes a :: "'a::real_normed_vector"
-  assumes "a \<noteq> b" shows "uncountable (open_segment a b)"
-  by (simp add: assms open_segment_def uncountable_closed_segment uncountable_minus_countable)
-
-lemma uncountable_convex:
-  fixes a :: "'a::real_normed_vector"
-  assumes "convex S" "a \<in> S" "b \<in> S" "a \<noteq> b"
-    shows "uncountable S"
-proof -
-  have "uncountable (closed_segment a b)"
-    by (simp add: uncountable_closed_segment assms)
-  then show ?thesis
-    by (meson assms convex_contains_segment countable_subset)
-qed
-
-lemma uncountable_ball:
-  fixes a :: "'a::euclidean_space"
-  assumes "r > 0"
-    shows "uncountable (ball a r)"
-proof -
-  have "uncountable (open_segment a (a + r *\<^sub>R (SOME i. i \<in> Basis)))"
-    by (metis Basis_zero SOME_Basis add_cancel_right_right assms less_le scale_eq_0_iff uncountable_open_segment)
-  moreover have "open_segment a (a + r *\<^sub>R (SOME i. i \<in> Basis)) \<subseteq> ball a r"
-    using assms by (auto simp: in_segment algebra_simps dist_norm SOME_Basis)
-  ultimately show ?thesis
-    by (metis countable_subset)
-qed
-
-lemma ball_minus_countable_nonempty:
-  assumes "countable (A :: 'a :: euclidean_space set)" "r > 0"
-  shows   "ball z r - A \<noteq> {}"
-proof
-  assume *: "ball z r - A = {}"
-  have "uncountable (ball z r - A)"
-    by (intro uncountable_minus_countable assms uncountable_ball)
-  thus False by (subst (asm) *) auto
-qed
-
-lemma uncountable_cball:
-  fixes a :: "'a::euclidean_space"
-  assumes "r > 0"
-  shows "uncountable (cball a r)"
-  using assms countable_subset uncountable_ball by auto
-
-lemma pairwise_disjnt_countable:
-  fixes \<N> :: "nat set set"
-  assumes "pairwise disjnt \<N>"
-    shows "countable \<N>"
-proof -
-  have "inj_on (\<lambda>X. SOME n. n \<in> X) (\<N> - {{}})"
-    by (clarsimp simp: inj_on_def) (metis assms disjnt_iff pairwiseD some_in_eq)
-  then show ?thesis
-    by (metis countable_Diff_eq countable_def)
-qed
-
-lemma pairwise_disjnt_countable_Union:
-    assumes "countable (\<Union>\<N>)" and pwd: "pairwise disjnt \<N>"
-    shows "countable \<N>"
-proof -
-  obtain f :: "_ \<Rightarrow> nat" where f: "inj_on f (\<Union>\<N>)"
-    using assms by blast
-  then have "pairwise disjnt (\<Union> X \<in> \<N>. {f ` X})"
-    using assms by (force simp: pairwise_def disjnt_inj_on_iff [OF f])
-  then have "countable (\<Union> X \<in> \<N>. {f ` X})"
-    using pairwise_disjnt_countable by blast
-  then show ?thesis
-    by (meson pwd countable_image_inj_on disjoint_image f inj_on_image pairwise_disjnt_countable)
-qed
-
-lemma connected_uncountable:
+lemma connected_card_eq_iff_nontrivial:
   fixes S :: "'a::metric_space set"
-  assumes "connected S" "a \<in> S" "b \<in> S" "a \<noteq> b" shows "uncountable S"
-proof -
-  have "continuous_on S (dist a)"
-    by (intro continuous_intros)
-  then have "connected (dist a ` S)"
-    by (metis connected_continuous_image \<open>connected S\<close>)
-  then have "closed_segment 0 (dist a b) \<subseteq> (dist a ` S)"
-    by (simp add: assms closed_segment_subset is_interval_connected_1 is_interval_convex)
-  then have "uncountable (dist a ` S)"
-    by (metis \<open>a \<noteq> b\<close> countable_subset dist_eq_0_iff uncountable_closed_segment)
-  then show ?thesis
-    by blast
-qed
-
-lemma path_connected_uncountable:
-  fixes S :: "'a::metric_space set"
-  assumes "path_connected S" "a \<in> S" "b \<in> S" "a \<noteq> b" shows "uncountable S"
-  using path_connected_imp_connected assms connected_uncountable by metis
+  shows "connected S \<Longrightarrow> uncountable S \<longleftrightarrow> \<not>(\<exists>a. S \<subseteq> {a})"
+  by (metis connected_uncountable finite.emptyI finite.insertI rev_finite_subset singleton_iff subsetI uncountable_infinite)
 
 lemma connected_finite_iff_sing:
   fixes S :: "'a::metric_space set"
   assumes "connected S"
-  shows "finite S \<longleftrightarrow> S = {} \<or> (\<exists>a. S = {a})"  (is "_ = ?rhs")
-proof -
-  have "uncountable S" if "\<not> ?rhs"
-    using connected_uncountable assms that by blast
-  then show ?thesis
-    using uncountable_infinite by auto
-qed
-
-lemma connected_card_eq_iff_nontrivial:
-  fixes S :: "'a::metric_space set"
-  shows "connected S \<Longrightarrow> uncountable S \<longleftrightarrow> \<not>(\<exists>a. S \<subseteq> {a})"
-  by (metis connected_uncountable finite.emptyI finite.insertI rev_finite_subset singleton_iff subsetI uncountable_infinite)
-
-lemma simple_path_image_uncountable: 
-  fixes g :: "real \<Rightarrow> 'a::metric_space"
-  assumes "simple_path g"
-  shows "uncountable (path_image g)"
-proof -
-  have "g 0 \<in> path_image g" "g (1/2) \<in> path_image g"
-    by (simp_all add: path_defs)
-  moreover have "g 0 \<noteq> g (1/2)"
-    using assms by (fastforce simp add: simple_path_def loop_free_def)
-  ultimately have "\<forall>a. \<not> path_image g \<subseteq> {a}"
-    by blast
-  then show ?thesis
-    using assms connected_simple_path_image connected_uncountable by blast
-qed
-
-lemma arc_image_uncountable:
-  fixes g :: "real \<Rightarrow> 'a::metric_space"
-  assumes "arc g"
-  shows "uncountable (path_image g)"
-  by (simp add: arc_imp_simple_path assms simple_path_image_uncountable)
-
+  shows "finite S \<longleftrightarrow> S = {} \<or> (\<exists>a. S = {a})" 
+  using assms connected_uncountable countable_finite by blast
 
 subsection\<^marker>\<open>tag unimportant\<close>\<open> Some simple positive connection theorems\<close>
 
diff -r 7d7786585ab0 -r 8f2e6186408f src/HOL/Analysis/Isolated.thy
--- a/src/HOL/Analysis/Isolated.thy	Sun Feb 05 20:09:39 2023 +0100
+++ b/src/HOL/Analysis/Isolated.thy	Mon Feb 06 15:41:23 2023 +0000
@@ -3,49 +3,49 @@
 
 begin
 
-subsection \<open>Isolate and discrete\<close>  
-  
-definition (in topological_space) isolate:: "'a \<Rightarrow> 'a set \<Rightarrow> bool"  (infixr "isolate" 60)
-  where "x isolate S \<longleftrightarrow> (x\<in>S \<and> (\<exists>T. open T \<and> T \<inter> S = {x}))"  
-    
-definition (in topological_space) discrete:: "'a set \<Rightarrow> bool" 
-  where "discrete S \<longleftrightarrow> (\<forall>x\<in>S. x isolate S)"  
-    
+subsection \<open>Isolate and discrete\<close>
+
+definition (in topological_space) isolated_in:: "'a \<Rightarrow> 'a set \<Rightarrow> bool"  (infixr "isolated'_in" 60)
+  where "x isolated_in S \<longleftrightarrow> (x\<in>S \<and> (\<exists>T. open T \<and> T \<inter> S = {x}))"
+
+definition (in topological_space) discrete:: "'a set \<Rightarrow> bool"
+  where "discrete S \<longleftrightarrow> (\<forall>x\<in>S. x isolated_in S)"
+
 definition (in metric_space) uniform_discrete :: "'a set \<Rightarrow> bool" where
   "uniform_discrete S \<longleftrightarrow> (\<exists>e>0. \<forall>x\<in>S. \<forall>y\<in>S. dist x y < e \<longrightarrow> x = y)"
-  
+
 lemma uniformI1:
   assumes "e>0" "\<And>x y. \<lbrakk>x\<in>S;y\<in>S;dist x y<e\<rbrakk> \<Longrightarrow> x =y "
-  shows "uniform_discrete S"  
+  shows "uniform_discrete S"
 unfolding uniform_discrete_def using assms by auto
 
 lemma uniformI2:
   assumes "e>0" "\<And>x y. \<lbrakk>x\<in>S;y\<in>S;x\<noteq>y\<rbrakk> \<Longrightarrow> dist x y\<ge>e "
-  shows "uniform_discrete S"  
+  shows "uniform_discrete S"
 unfolding uniform_discrete_def using assms not_less by blast
-  
-lemma isolate_islimpt_iff:"(x isolate S) \<longleftrightarrow> (\<not> (x islimpt S) \<and> x\<in>S)"
-  unfolding isolate_def islimpt_def by auto
-  
-lemma isolate_dist_Ex_iff:
+
+lemma isolated_in_islimpt_iff:"(x isolated_in S) \<longleftrightarrow> (\<not> (x islimpt S) \<and> x\<in>S)"
+  unfolding isolated_in_def islimpt_def by auto
+
+lemma isolated_in_dist_Ex_iff:
   fixes x::"'a::metric_space"
-  shows "x isolate S \<longleftrightarrow> (x\<in>S \<and> (\<exists>e>0. \<forall>y\<in>S. dist x y < e \<longrightarrow> y=x))"
-unfolding isolate_islimpt_iff islimpt_approachable by (metis dist_commute)
-  
+  shows "x isolated_in S \<longleftrightarrow> (x\<in>S \<and> (\<exists>e>0. \<forall>y\<in>S. dist x y < e \<longrightarrow> y=x))"
+unfolding isolated_in_islimpt_iff islimpt_approachable by (metis dist_commute)
+
 lemma discrete_empty[simp]: "discrete {}"
   unfolding discrete_def by auto
 
 lemma uniform_discrete_empty[simp]: "uniform_discrete {}"
   unfolding uniform_discrete_def by (simp add: gt_ex)
-  
-lemma isolate_insert: 
+
+lemma isolated_in_insert:
   fixes x :: "'a::t1_space"
-  shows "x isolate (insert a S) \<longleftrightarrow> x isolate S \<or> (x=a \<and> \<not> (x islimpt S))"
-by (meson insert_iff islimpt_insert isolate_islimpt_iff)
-    
+  shows "x isolated_in (insert a S) \<longleftrightarrow> x isolated_in S \<or> (x=a \<and> \<not> (x islimpt S))"
+by (meson insert_iff islimpt_insert isolated_in_islimpt_iff)
+
 (*
-TODO. 
-Other than 
+TODO.
+Other than
 
   uniform_discrete S \<longrightarrow> discrete S
   uniform_discrete S \<longrightarrow> closed S
@@ -58,31 +58,31 @@
 
 http://topology.auburn.edu/tp/reprints/v30/tp30120.pdf
 http://msp.org/pjm/1959/9-2/pjm-v9-n2-p19-s.pdf
-*)  
-  
+*)
+
 lemma uniform_discrete_imp_closed:
-  "uniform_discrete S \<Longrightarrow> closed S" 
-  by (meson discrete_imp_closed uniform_discrete_def) 
-    
+  "uniform_discrete S \<Longrightarrow> closed S"
+  by (meson discrete_imp_closed uniform_discrete_def)
+
 lemma uniform_discrete_imp_discrete:
   "uniform_discrete S \<Longrightarrow> discrete S"
-  by (metis discrete_def isolate_dist_Ex_iff uniform_discrete_def)
-  
-lemma isolate_subset:"x isolate S \<Longrightarrow> T \<subseteq> S \<Longrightarrow> x\<in>T \<Longrightarrow> x isolate T"
-  unfolding isolate_def by fastforce
+  by (metis discrete_def isolated_in_dist_Ex_iff uniform_discrete_def)
+
+lemma isolated_in_subset:"x isolated_in S \<Longrightarrow> T \<subseteq> S \<Longrightarrow> x\<in>T \<Longrightarrow> x isolated_in T"
+  unfolding isolated_in_def by fastforce
 
 lemma discrete_subset[elim]: "discrete S \<Longrightarrow> T \<subseteq> S \<Longrightarrow> discrete T"
-  unfolding discrete_def using islimpt_subset isolate_islimpt_iff by blast
-    
+  unfolding discrete_def using islimpt_subset isolated_in_islimpt_iff by blast
+
 lemma uniform_discrete_subset[elim]: "uniform_discrete S \<Longrightarrow> T \<subseteq> S \<Longrightarrow> uniform_discrete T"
   by (meson subsetD uniform_discrete_def)
-        
-lemma continuous_on_discrete: "discrete S \<Longrightarrow> continuous_on S f" 
-  unfolding continuous_on_topological by (metis discrete_def islimptI isolate_islimpt_iff)
-   
+
+lemma continuous_on_discrete: "discrete S \<Longrightarrow> continuous_on S f"
+  unfolding continuous_on_topological by (metis discrete_def islimptI isolated_in_islimpt_iff)
+
 lemma uniform_discrete_insert: "uniform_discrete (insert a S) \<longleftrightarrow> uniform_discrete S"
-proof 
-  assume asm:"uniform_discrete S" 
+proof
+  assume asm:"uniform_discrete S"
   let ?thesis = "uniform_discrete (insert a S)"
   have ?thesis when "a\<in>S" using that asm by (simp add: insert_absorb)
   moreover have ?thesis when "S={}" using that asm by (simp add: uniform_discrete_def)
@@ -94,44 +94,38 @@
     have "closed S" using asm uniform_discrete_imp_closed by auto
     then have "e2>0"
       by (smt (verit) \<open>0 < e1\<close> e2_def infdist_eq_setdist infdist_pos_not_in_closed that)
-    moreover have "x = y" when "x\<in>insert a S" "y\<in>insert a S" "dist x y < e2 " for x y
-    proof -
-      have ?thesis when "x=a" "y=a" using that by auto
-      moreover have ?thesis when "x=a" "y\<in>S"
-        using that setdist_le_dist[of x "{a}" y S] \<open>dist x y < e2\<close> unfolding e2_def
-        by fastforce
-      moreover have ?thesis when "y=a" "x\<in>S"
-        using that setdist_le_dist[of y "{a}" x S] \<open>dist x y < e2\<close> unfolding e2_def
-        by (simp add: dist_commute)
-      moreover have ?thesis when "x\<in>S" "y\<in>S"
-        using e1_dist[rule_format, OF that] \<open>dist x y < e2\<close> unfolding e2_def
-        by (simp add: dist_commute)
-      ultimately show ?thesis using that by auto
+    moreover have "x = y" if "x\<in>insert a S" "y\<in>insert a S" "dist x y < e2" for x y
+    proof (cases "x=a \<or> y=a")
+      case True then show ?thesis
+        by (smt (verit, best) dist_commute e2_def infdist_eq_setdist infdist_le insertE that)
+    next
+      case False then show ?thesis
+        using e1_dist e2_def that by force
     qed
     ultimately show ?thesis unfolding uniform_discrete_def by meson
   qed
   ultimately show ?thesis by auto
 qed (simp add: subset_insertI uniform_discrete_subset)
-    
+
 lemma discrete_compact_finite_iff:
   fixes S :: "'a::t1_space set"
   shows "discrete S \<and> compact S \<longleftrightarrow> finite S"
-proof 
+proof
   assume "finite S"
   then have "compact S" using finite_imp_compact by auto
   moreover have "discrete S"
-    unfolding discrete_def using isolate_islimpt_iff islimpt_finite[OF \<open>finite S\<close>] by auto 
+    unfolding discrete_def using isolated_in_islimpt_iff islimpt_finite[OF \<open>finite S\<close>] by auto
   ultimately show "discrete S \<and> compact S" by auto
 next
   assume "discrete S \<and> compact S"
-  then show "finite S" 
-    by (meson discrete_def Heine_Borel_imp_Bolzano_Weierstrass isolate_islimpt_iff order_refl)
+  then show "finite S"
+    by (meson discrete_def Heine_Borel_imp_Bolzano_Weierstrass isolated_in_islimpt_iff order_refl)
 qed
-  
+
 lemma uniform_discrete_finite_iff:
   fixes S :: "'a::heine_borel set"
   shows "uniform_discrete S \<and> bounded S \<longleftrightarrow> finite S"
-proof 
+proof
   assume "uniform_discrete S \<and> bounded S"
   then have "discrete S" "compact S"
     using uniform_discrete_imp_discrete uniform_discrete_imp_closed compact_eq_bounded_closed
@@ -145,46 +139,42 @@
   proof -
     have "\<forall>x. \<exists>d>0. \<forall>y\<in>S. y \<noteq> x \<longrightarrow> d \<le> dist x y"
       using finite_set_avoid[OF \<open>finite S\<close>] by auto
-    then obtain f where f_pos:"f x>0" 
+    then obtain f where f_pos:"f x>0"
         and f_dist: "\<forall>y\<in>S. y \<noteq> x \<longrightarrow> f x \<le> dist x y"
-        if "x\<in>S" for x 
+        if "x\<in>S" for x
       by metis
-    define f_min where "f_min \<equiv> Min (f ` S)" 
+    define f_min where "f_min \<equiv> Min (f ` S)"
     have "f_min > 0"
-      unfolding f_min_def 
+      unfolding f_min_def
       by (simp add: asm f_pos that)
     moreover have "\<forall>x\<in>S. \<forall>y\<in>S. f_min > dist x y \<longrightarrow> x=y"
-      using f_dist unfolding f_min_def 
-      by (metis Min_gr_iff all_not_in_conv asm dual_order.irrefl eq_iff finite_imageI imageI 
-          less_eq_real_def)
-    ultimately have "uniform_discrete S" 
+      using f_dist unfolding f_min_def
+      by (metis Min_le asm finite_imageI imageI le_less_trans linorder_not_less)
+    ultimately have "uniform_discrete S"
       unfolding uniform_discrete_def by auto
     moreover have "bounded S" using \<open>finite S\<close> by auto
     ultimately show ?thesis by auto
   qed
   ultimately show ?thesis by blast
 qed
-  
+
 lemma uniform_discrete_image_scale:
   assumes "uniform_discrete S" and dist:"\<forall>x\<in>S. \<forall>y\<in>S. dist x y = c * dist (f x) (f y)"
-  shows "uniform_discrete (f ` S)"  
+  shows "uniform_discrete (f ` S)"
 proof -
   have ?thesis when "S={}" using that by auto
   moreover have ?thesis when "S\<noteq>{}" "c\<le>0"
   proof -
     obtain x1 where "x1\<in>S" using \<open>S\<noteq>{}\<close> by auto
     have ?thesis when "S-{x1} = {}"
-    proof -
-      have "S={x1}" using that \<open>S\<noteq>{}\<close> by auto
-      then show ?thesis using uniform_discrete_insert[of "f x1"] by auto
-    qed
+      using \<open>x1 \<in> S\<close> subset_antisym that uniform_discrete_insert by fastforce
     moreover have ?thesis when "S-{x1} \<noteq> {}"
     proof -
       obtain x2 where "x2\<in>S-{x1}" using \<open>S-{x1} \<noteq> {}\<close> by auto
       then have "x2\<in>S" "x1\<noteq>x2" by auto
       then have "dist x1 x2 > 0" by auto
       moreover have "dist x1 x2 = c * dist (f x1) (f x2)"
-        using dist[rule_format, OF \<open>x1\<in>S\<close> \<open>x2\<in>S\<close>] .
+        by (simp add: \<open>x1 \<in> S\<close> \<open>x2 \<in> S\<close> dist)
       moreover have "dist (f x2) (f x2) \<ge> 0" by auto
       ultimately have False using \<open>c\<le>0\<close> by (simp add: zero_less_mult_iff)
       then show ?thesis by auto
@@ -195,21 +185,13 @@
   proof -
     obtain e1 where "e1>0" and e1_dist:"\<forall>x\<in>S. \<forall>y\<in>S. dist y x < e1 \<longrightarrow> y = x"
       using \<open>uniform_discrete S\<close> unfolding uniform_discrete_def by auto
-    define e where "e= e1/c"
-    have "x1 = x2" when "x1\<in> f ` S" "x2\<in> f ` S" "dist x1 x2 < e " for x1 x2 
-    proof -
-      obtain y1 where y1:"y1\<in>S" "x1=f y1" using \<open>x1\<in> f ` S\<close> by auto
-      obtain y2 where y2:"y2\<in>S" "x2=f y2" using \<open>x2\<in> f ` S\<close> by auto    
-      have "dist y1 y2 < e1"
-        by (smt (verit) \<open>0 < c\<close> dist divide_right_mono e_def nonzero_mult_div_cancel_left that(3) y1 y2)
-      then have "y1=y2"    
-        using e1_dist[rule_format, OF y2(1) y1(1)] by simp
-      then show "x1=x2" using y1(2) y2(2) by auto
-    qed
+    define e where "e \<equiv> e1/c"
+    have "x1 = x2" when "x1 \<in> f ` S" "x2 \<in> f ` S" and d: "dist x1 x2 < e" for x1 x2
+      by (smt (verit) \<open>0 < c\<close> d dist divide_right_mono e1_dist e_def imageE nonzero_mult_div_cancel_left that)
     moreover have "e>0" using \<open>e1>0\<close> \<open>c>0\<close> unfolding e_def by auto
     ultimately show ?thesis unfolding uniform_discrete_def by meson
   qed
   ultimately show ?thesis by fastforce
 qed
- 
+
 end
diff -r 7d7786585ab0 -r 8f2e6186408f src/HOL/Analysis/Uncountable_Sets.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Analysis/Uncountable_Sets.thy	Mon Feb 06 15:41:23 2023 +0000
@@ -0,0 +1,121 @@
+section \<open>Some Uncountable Sets\<close>
+
+theory Uncountable_Sets
+  imports Path_Connected Continuum_Not_Denumerable  
+begin
+
+lemma uncountable_closed_segment:
+  fixes a :: "'a::real_normed_vector"
+  assumes "a \<noteq> b" shows "uncountable (closed_segment a b)"
+unfolding path_image_linepath [symmetric] path_image_def
+  using inj_on_linepath [OF assms] uncountable_closed_interval [of 0 1]
+        countable_image_inj_on by auto
+
+lemma uncountable_open_segment:
+  fixes a :: "'a::real_normed_vector"
+  assumes "a \<noteq> b" shows "uncountable (open_segment a b)"
+  by (simp add: assms open_segment_def uncountable_closed_segment uncountable_minus_countable)
+
+lemma uncountable_convex:
+  fixes a :: "'a::real_normed_vector"
+  assumes "convex S" "a \<in> S" "b \<in> S" "a \<noteq> b"
+    shows "uncountable S"
+proof -
+  have "uncountable (closed_segment a b)"
+    by (simp add: uncountable_closed_segment assms)
+  then show ?thesis
+    by (meson assms convex_contains_segment countable_subset)
+qed
+
+lemma uncountable_ball:
+  fixes a :: "'a::euclidean_space"
+  assumes "r > 0"
+    shows "uncountable (ball a r)"
+proof -
+  have "uncountable (open_segment a (a + r *\<^sub>R (SOME i. i \<in> Basis)))"
+    by (metis Basis_zero SOME_Basis add_cancel_right_right assms less_le scale_eq_0_iff uncountable_open_segment)
+  moreover have "open_segment a (a + r *\<^sub>R (SOME i. i \<in> Basis)) \<subseteq> ball a r"
+    using assms by (auto simp: in_segment algebra_simps dist_norm SOME_Basis)
+  ultimately show ?thesis
+    by (metis countable_subset)
+qed
+
+lemma ball_minus_countable_nonempty:
+  assumes "countable (A :: 'a :: euclidean_space set)" "r > 0"
+  shows   "ball z r - A \<noteq> {}"
+proof
+  assume *: "ball z r - A = {}"
+  have "uncountable (ball z r - A)"
+    by (intro uncountable_minus_countable assms uncountable_ball)
+  thus False by (subst (asm) *) auto
+qed
+
+lemma uncountable_cball:
+  fixes a :: "'a::euclidean_space"
+  assumes "r > 0"
+  shows "uncountable (cball a r)"
+  using assms countable_subset uncountable_ball by auto
+
+lemma pairwise_disjnt_countable:
+  fixes \<N> :: "nat set set"
+  assumes "pairwise disjnt \<N>"
+    shows "countable \<N>"
+  by (simp add: assms countable_disjoint_open_subsets open_discrete)
+
+lemma pairwise_disjnt_countable_Union:
+    assumes "countable (\<Union>\<N>)" and pwd: "pairwise disjnt \<N>"
+    shows "countable \<N>"
+proof -
+  obtain f :: "_ \<Rightarrow> nat" where f: "inj_on f (\<Union>\<N>)"
+    using assms by blast
+  then have "pairwise disjnt (\<Union> X \<in> \<N>. {f ` X})"
+    using assms by (force simp: pairwise_def disjnt_inj_on_iff [OF f])
+  then have "countable (\<Union> X \<in> \<N>. {f ` X})"
+    using pairwise_disjnt_countable by blast
+  then show ?thesis
+    by (meson pwd countable_image_inj_on disjoint_image f inj_on_image pairwise_disjnt_countable)
+qed
+
+lemma connected_uncountable:
+  fixes S :: "'a::metric_space set"
+  assumes "connected S" "a \<in> S" "b \<in> S" "a \<noteq> b" shows "uncountable S"
+proof -
+  have "continuous_on S (dist a)"
+    by (intro continuous_intros)
+  then have "connected (dist a ` S)"
+    by (metis connected_continuous_image \<open>connected S\<close>)
+  then have "closed_segment 0 (dist a b) \<subseteq> (dist a ` S)"
+    by (simp add: assms closed_segment_subset is_interval_connected_1 is_interval_convex)
+  then have "uncountable (dist a ` S)"
+    by (metis \<open>a \<noteq> b\<close> countable_subset dist_eq_0_iff uncountable_closed_segment)
+  then show ?thesis
+    by blast
+qed
+
+lemma path_connected_uncountable:
+  fixes S :: "'a::metric_space set"
+  assumes "path_connected S" "a \<in> S" "b \<in> S" "a \<noteq> b" shows "uncountable S"
+  using path_connected_imp_connected assms connected_uncountable by metis
+
+lemma simple_path_image_uncountable: 
+  fixes g :: "real \<Rightarrow> 'a::metric_space"
+  assumes "simple_path g"
+  shows "uncountable (path_image g)"
+proof -
+  have "g 0 \<in> path_image g" "g (1/2) \<in> path_image g"
+    by (simp_all add: path_defs)
+  moreover have "g 0 \<noteq> g (1/2)"
+    using assms by (fastforce simp add: simple_path_def loop_free_def)
+  ultimately have "\<forall>a. \<not> path_image g \<subseteq> {a}"
+    by blast
+  then show ?thesis
+    using assms connected_simple_path_image connected_uncountable by blast
+qed
+
+lemma arc_image_uncountable:
+  fixes g :: "real \<Rightarrow> 'a::metric_space"
+  assumes "arc g"
+  shows "uncountable (path_image g)"
+  by (simp add: arc_imp_simple_path assms simple_path_image_uncountable)
+
+end
diff -r 7d7786585ab0 -r 8f2e6186408f src/HOL/Library/Landau_Symbols.thy
--- a/src/HOL/Library/Landau_Symbols.thy	Sun Feb 05 20:09:39 2023 +0100
+++ b/src/HOL/Library/Landau_Symbols.thy	Mon Feb 06 15:41:23 2023 +0000
@@ -618,7 +618,48 @@
 
 lemmas mult = big_mult small_big_mult big_small_mult small_mult
 
+lemma big_power:
+  assumes "f \<in> L F (g)"
+  shows   "(\<lambda>x. f x ^ m) \<in> L F (\<lambda>x. g x ^ m)"
+  using assms by (induction m) (auto intro: mult)
 
+lemma (in landau_pair) small_power:
+  assumes "f \<in> l F (g)" "m > 0"
+  shows   "(\<lambda>x. f x ^ m) \<in> l F (\<lambda>x. g x ^ m)"
+proof -
+  have "(\<lambda>x. f x * f x ^ (m - 1)) \<in> l F (\<lambda>x. g x * g x ^ (m - 1))"
+    by (intro small_big_mult assms big_power[OF small_imp_big])
+  thus ?thesis
+    using assms by (cases m) (simp_all add: mult_ac)
+qed
+
+lemma big_power_increasing:
+  assumes "(\<lambda>_. 1) \<in> L F f" "m \<le> n"
+  shows   "(\<lambda>x. f x ^ m) \<in> L F (\<lambda>x. f x ^ n)"
+proof -
+  have "(\<lambda>x. f x ^ m * 1 ^ (n - m)) \<in> L F (\<lambda>x. f x ^ m * f x ^ (n - m))"
+    using assms by (intro mult big_power) auto
+  also have "(\<lambda>x. f x ^ m * f x ^ (n - m)) = (\<lambda>x. f x ^ (m + (n - m)))"
+    by (subst power_add [symmetric]) (rule refl)
+  also have "m + (n - m) = n"
+    using assms by simp
+  finally show ?thesis by simp
+qed
+
+lemma small_power_increasing:
+  assumes "(\<lambda>_. 1) \<in> l F f" "m < n"
+  shows   "(\<lambda>x. f x ^ m) \<in> l F (\<lambda>x. f x ^ n)"
+proof -
+  note [trans] = small_big_trans
+  have "(\<lambda>x. f x ^ m * 1) \<in> l F (\<lambda>x. f x ^ m * f x)"
+    using assms by (intro big_small_mult) auto
+  also have "(\<lambda>x. f x ^ m * f x) = (\<lambda>x. f x ^ Suc m)"
+    by (simp add: mult_ac)
+  also have "\<dots> \<in> L F (\<lambda>x. f x ^ n)"
+    using assms by (intro big_power_increasing[OF small_imp_big]) auto
+  finally show ?thesis by simp
+qed
+  
 sublocale big: landau_symbol L L' Lr
 proof
   have L: "L = bigo \<or> L = bigomega"
@@ -1779,6 +1820,9 @@
   by (intro asymp_equivI tendsto_eventually)
      (insert assms, auto elim!: eventually_mono)
 
+lemma asymp_equiv_nhds_iff: "f \<sim>[nhds (z :: 'a :: t1_space)] g \<longleftrightarrow> f \<sim>[at z] g \<and> f z = g z"
+  by (auto simp: asymp_equiv_def tendsto_nhds_iff)
+
 lemma asymp_equiv_sandwich:
   fixes f g h :: "'a \<Rightarrow> 'b :: {real_normed_field, order_topology, linordered_field}"
   assumes "eventually (\<lambda>x. f x \<ge> 0) F"
@@ -2191,8 +2235,6 @@
   assumes "l1 \<sim>[F] u1" "u1 \<sim>[F] l2" "l2 \<sim>[F] u2"
           "eventually (\<lambda>x. f x \<in> {l1 x..u1 x}) F" "eventually (\<lambda>x. g x \<in> {l2 x..u2 x}) F"
   shows   "f \<sim>[F] g"
-  by (rule asymp_equiv_sandwich_real[OF asymp_equiv_sandwich_real'[OF _ _ assms(5)]
-             asymp_equiv_sandwich_real'[OF _ _ assms(5)] assms(4)];
-      blast intro: asymp_equiv_trans assms(1,2,3))+
+  by (meson assms asymp_equiv_sandwich_real asymp_equiv_sandwich_real' asymp_equiv_trans)
 
 end
diff -r 7d7786585ab0 -r 8f2e6186408f src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Sun Feb 05 20:09:39 2023 +0100
+++ b/src/HOL/Transcendental.thy	Mon Feb 06 15:41:23 2023 +0000
@@ -2521,20 +2521,7 @@
 lemma powr_real_of_int':
   assumes "x \<ge> 0" "x \<noteq> 0 \<or> n > 0"
   shows   "x powr real_of_int n = power_int x n"
-proof (cases "x = 0")
-  case False
-  with assms have "x > 0" by simp
-  show ?thesis
-  proof (cases n rule: int_cases4)
-    case (nonneg n)
-    thus ?thesis using \<open>x > 0\<close>
-      by (auto simp add: powr_realpow)
-  next
-    case (neg n)
-    thus ?thesis using \<open>x > 0\<close>
-      by (auto simp add: powr_realpow powr_minus power_int_minus)
-  qed
-qed (use assms in auto)
+  by (metis assms exp_ln_iff exp_power_int nless_le power_int_eq_0_iff powr_def)
 
 lemma log_ln: "ln x = log (exp(1)) x"
   by (simp add: log_def)