src/HOL/Analysis/Cauchy_Integral_Theorem.thy

 } then
 show ?thesis
   by (force simp: L contour_integral_integral)
 qed
 
-subsection\<open>Constancy of a function from a connected set into a finite, disconnected or discrete set\<close>
-
-text\<open>Still missing: versions for a set that is smaller than R, or countable.\<close>
-
-lemma continuous_disconnected_range_constant:
-  assumes s: "connected s"
-      and conf: "continuous_on s f"
-      and fim: "f ` s \<subseteq> t"
-      and cct: "\<And>y. y \<in> t \<Longrightarrow> connected_component_set t y = {y}"
-    shows "\<exists>a. \<forall>x \<in> s. f x = a"
-proof (cases "s = {}")
-  case True then show ?thesis by force
-next
-  case False
-  { fix x assume "x \<in> s"
-    then have "f ` s \<subseteq> {f x}"
-    by (metis connected_continuous_image conf connected_component_maximal fim image_subset_iff rev_image_eqI s cct)
-  }
-  with False show ?thesis
-    by blast
-qed
-
-lemma discrete_subset_disconnected:
-  fixes s :: "'a::topological_space set"
-  fixes t :: "'b::real_normed_vector set"
-  assumes conf: "continuous_on s f"
-      and no: "\<And>x. x \<in> s \<Longrightarrow> \<exists>e>0. \<forall>y. y \<in> s \<and> f y \<noteq> f x \<longrightarrow> e \<le> norm (f y - f x)"
-   shows "f ` s \<subseteq> {y. connected_component_set (f ` s) y = {y}}"
-proof -
-  { fix x assume x: "x \<in> s"
-    then obtain e where "e>0" and ele: "\<And>y. \<lbrakk>y \<in> s; f y \<noteq> f x\<rbrakk> \<Longrightarrow> e \<le> norm (f y - f x)"
-      using conf no [OF x] by auto
-    then have e2: "0 \<le> e / 2"
-      by simp
-    have "f y = f x" if "y \<in> s" and ccs: "f y \<in> connected_component_set (f ` s) (f x)" for y
-      apply (rule ccontr)
-      using connected_closed [of "connected_component_set (f ` s) (f x)"] \<open>e>0\<close>
-      apply (simp add: del: ex_simps)
-      apply (drule spec [where x="cball (f x) (e / 2)"])
-      apply (drule spec [where x="- ball(f x) e"])
-      apply (auto simp: dist_norm open_closed [symmetric] simp del: le_divide_eq_numeral1 dest!: connected_component_in)
-        apply (metis diff_self e2 ele norm_minus_commute norm_zero not_less)
-       using centre_in_cball connected_component_refl_eq e2 x apply blast
-      using ccs
-      apply (force simp: cball_def dist_norm norm_minus_commute dest: ele [OF \<open>y \<in> s\<close>])
-      done
-    moreover have "connected_component_set (f ` s) (f x) \<subseteq> f ` s"
-      by (auto simp: connected_component_in)
-    ultimately have "connected_component_set (f ` s) (f x) = {f x}"
-      by (auto simp: x)
-  }
-  with assms show ?thesis
-    by blast
-qed
-
-lemma finite_implies_discrete:
-  fixes s :: "'a::topological_space set"
-  assumes "finite (f ` s)"
-  shows "(\<forall>x \<in> s. \<exists>e>0. \<forall>y. y \<in> s \<and> f y \<noteq> f x \<longrightarrow> e \<le> norm (f y - f x))"
-proof -
-  have "\<exists>e>0. \<forall>y. y \<in> s \<and> f y \<noteq> f x \<longrightarrow> e \<le> norm (f y - f x)" if "x \<in> s" for x
-  proof (cases "f ` s - {f x} = {}")
-    case True
-    with zero_less_numeral show ?thesis
-      by (fastforce simp add: Set.image_subset_iff cong: conj_cong)
-  next
-    case False
-    then obtain z where z: "z \<in> s" "f z \<noteq> f x"
-      by blast
-    have finn: "finite {norm (z - f x) |z. z \<in> f ` s - {f x}}"
-      using assms by simp
-    then have *: "0 < Inf{norm(z - f x) | z. z \<in> f ` s - {f x}}"
-      apply (rule finite_imp_less_Inf)
-      using z apply force+
-      done
-    show ?thesis
-      by (force intro!: * cInf_le_finite [OF finn])
-  qed
-  with assms show ?thesis
-    by blast
-qed
-
-text\<open>This proof requires the existence of two separate values of the range type.\<close>
-lemma finite_range_constant_imp_connected:
-  assumes "\<And>f::'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1.
-              \<lbrakk>continuous_on s f; finite(f ` s)\<rbrakk> \<Longrightarrow> \<exists>a. \<forall>x \<in> s. f x = a"
-    shows "connected s"
-proof -
-  { fix t u
-    assume clt: "closedin (subtopology euclidean s) t"
-       and clu: "closedin (subtopology euclidean s) u"
-       and tue: "t \<inter> u = {}" and tus: "t \<union> u = s"
-    have conif: "continuous_on s (\<lambda>x. if x \<in> t then 0 else 1)"
-      apply (subst tus [symmetric])
-      apply (rule continuous_on_cases_local)
-      using clt clu tue
-      apply (auto simp: tus continuous_on_const)
-      done
-    have fi: "finite ((\<lambda>x. if x \<in> t then 0 else 1) ` s)"
-      by (rule finite_subset [of _ "{0,1}"]) auto
-    have "t = {} \<or> u = {}"
-      using assms [OF conif fi] tus [symmetric]
-      by (auto simp: Ball_def) (metis IntI empty_iff one_neq_zero tue)
-  }
-  then show ?thesis
-    by (simp add: connected_closedin_eq)
-qed
-
-lemma continuous_disconnected_range_constant_eq:
-      "(connected s \<longleftrightarrow>
-           (\<forall>f::'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1.
-            \<forall>t. continuous_on s f \<and> f ` s \<subseteq> t \<and> (\<forall>y \<in> t. connected_component_set t y = {y})
-            \<longrightarrow> (\<exists>a::'b. \<forall>x \<in> s. f x = a)))" (is ?thesis1)
-  and continuous_discrete_range_constant_eq:
-      "(connected s \<longleftrightarrow>
-         (\<forall>f::'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1.
-          continuous_on s f \<and>
-          (\<forall>x \<in> s. \<exists>e. 0 < e \<and> (\<forall>y. y \<in> s \<and> (f y \<noteq> f x) \<longrightarrow> e \<le> norm(f y - f x)))
-          \<longrightarrow> (\<exists>a::'b. \<forall>x \<in> s. f x = a)))" (is ?thesis2)
-  and continuous_finite_range_constant_eq:
-      "(connected s \<longleftrightarrow>
-         (\<forall>f::'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1.
-          continuous_on s f \<and> finite (f ` s)
-          \<longrightarrow> (\<exists>a::'b. \<forall>x \<in> s. f x = a)))" (is ?thesis3)
-proof -
-  have *: "\<And>s t u v. \<lbrakk>s \<Longrightarrow> t; t \<Longrightarrow> u; u \<Longrightarrow> v; v \<Longrightarrow> s\<rbrakk>
-    \<Longrightarrow> (s \<longleftrightarrow> t) \<and> (s \<longleftrightarrow> u) \<and> (s \<longleftrightarrow> v)"
-    by blast
-  have "?thesis1 \<and> ?thesis2 \<and> ?thesis3"
-    apply (rule *)
-    using continuous_disconnected_range_constant apply metis
-    apply clarify
-    apply (frule discrete_subset_disconnected; blast)
-    apply (blast dest: finite_implies_discrete)
-    apply (blast intro!: finite_range_constant_imp_connected)
-    done
-  then show ?thesis1 ?thesis2 ?thesis3
-    by blast+
-qed
-
-lemma continuous_discrete_range_constant:
-  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1"
-  assumes s: "connected s"
-      and "continuous_on s f"
-      and "\<And>x. x \<in> s \<Longrightarrow> \<exists>e>0. \<forall>y. y \<in> s \<and> f y \<noteq> f x \<longrightarrow> e \<le> norm (f y - f x)"
-    shows "\<exists>a. \<forall>x \<in> s. f x = a"
-  using continuous_discrete_range_constant_eq [THEN iffD1, OF s] assms
-  by blast
-
-lemma continuous_finite_range_constant:
-  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1"
-  assumes "connected s"
-      and "continuous_on s f"
-      and "finite (f ` s)"
-    shows "\<exists>a. \<forall>x \<in> s. f x = a"
-  using assms continuous_finite_range_constant_eq
-  by blast
-
-
 text\<open>We can treat even non-rectifiable paths as having a "length" for bounds on analytic functions in open sets.\<close>
 
 subsection\<open>Winding Numbers\<close>
 
 definition winding_number:: "[real \<Rightarrow> complex, complex] \<Rightarrow> complex" where