New theory of arcwise connected sets and other new material
authorpaulson <lp15@cam.ac.uk>
Thu Jan 05 16:03:23 2017 +0000 (2017-01-05)
changeset 64790ed38f9a834d8
parent 64789 6440577e34ee
child 64791 05a2b3b20664
New theory of arcwise connected sets and other new material
src/HOL/Analysis/Analysis.thy
src/HOL/Analysis/Arcwise_Connected.thy
src/HOL/Analysis/Complex_Transcendental.thy
src/HOL/Analysis/Further_Topology.thy
src/HOL/Analysis/Path_Connected.thy
     1.1 --- a/src/HOL/Analysis/Analysis.thy	Thu Jan 05 15:03:37 2017 +0000
     1.2 +++ b/src/HOL/Analysis/Analysis.thy	Thu Jan 05 16:03:23 2017 +0000
     1.3 @@ -12,6 +12,7 @@
     1.4    Weierstrass_Theorems
     1.5    Polytope
     1.6    Further_Topology
     1.7 +  Arcwise_Connected
     1.8    Poly_Roots
     1.9    Conformal_Mappings
    1.10    Generalised_Binomial_Theorem
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Analysis/Arcwise_Connected.thy	Thu Jan 05 16:03:23 2017 +0000
     2.3 @@ -0,0 +1,2213 @@
     2.4 +(*  Title:      HOL/Analysis/Arcwise_Connected.thy
     2.5 +    Authors:    LC Paulson, based on material from HOL Light
     2.6 +*)
     2.7 +
     2.8 +section \<open>Arcwise-connected sets\<close>
     2.9 +
    2.10 +theory Arcwise_Connected
    2.11 +  imports Path_Connected Ordered_Euclidean_Space "~~/src/HOL/Number_Theory/Primes"
    2.12 +
    2.13 +begin
    2.14 +
    2.15 +subsection\<open>The Brouwer reduction theorem\<close>
    2.16 +
    2.17 +theorem Brouwer_reduction_theorem_gen:
    2.18 +  fixes S :: "'a::euclidean_space set"
    2.19 +  assumes "closed S" "\<phi> S"
    2.20 +      and \<phi>: "\<And>F. \<lbrakk>\<And>n. closed(F n); \<And>n. \<phi>(F n); \<And>n. F(Suc n) \<subseteq> F n\<rbrakk> \<Longrightarrow> \<phi>(\<Inter>range F)"
    2.21 +  obtains T where "T \<subseteq> S" "closed T" "\<phi> T" "\<And>U. \<lbrakk>U \<subseteq> S; closed U; \<phi> U\<rbrakk> \<Longrightarrow> \<not> (U \<subset> T)"
    2.22 +proof -
    2.23 +  obtain B :: "nat \<Rightarrow> 'a set"
    2.24 +    where "inj B" "\<And>n. open(B n)" and open_cov: "\<And>S. open S \<Longrightarrow> \<exists>K. S = \<Union>(B ` K)"
    2.25 +      by (metis Setcompr_eq_image that univ_second_countable_sequence)
    2.26 +  define A where "A \<equiv> rec_nat S (\<lambda>n a. if \<exists>U. U \<subseteq> a \<and> closed U \<and> \<phi> U \<and> U \<inter> (B n) = {}
    2.27 +                                        then @U. U \<subseteq> a \<and> closed U \<and> \<phi> U \<and> U \<inter> (B n) = {}
    2.28 +                                        else a)"
    2.29 +  have [simp]: "A 0 = S"
    2.30 +    by (simp add: A_def)
    2.31 +  have ASuc: "A(Suc n) = (if \<exists>U. U \<subseteq> A n \<and> closed U \<and> \<phi> U \<and> U \<inter> (B n) = {}
    2.32 +                          then @U. U \<subseteq> A n \<and> closed U \<and> \<phi> U \<and> U \<inter> (B n) = {}
    2.33 +                          else A n)" for n
    2.34 +    by (auto simp: A_def)
    2.35 +  have sub: "\<And>n. A(Suc n) \<subseteq> A n"
    2.36 +    by (auto simp: ASuc dest!: someI_ex)
    2.37 +  have subS: "A n \<subseteq> S" for n
    2.38 +    by (induction n) (use sub in auto)
    2.39 +  have clo: "closed (A n) \<and> \<phi> (A n)" for n
    2.40 +    by (induction n) (auto simp: assms ASuc dest!: someI_ex)
    2.41 +  show ?thesis
    2.42 +  proof
    2.43 +    show "\<Inter>range A \<subseteq> S"
    2.44 +      using \<open>\<And>n. A n \<subseteq> S\<close> by blast
    2.45 +    show "closed (INTER UNIV A)"
    2.46 +      using clo by blast
    2.47 +    show "\<phi> (INTER UNIV A)"
    2.48 +      by (simp add: clo \<phi> sub)
    2.49 +    show "\<not> U \<subset> INTER UNIV A" if "U \<subseteq> S" "closed U" "\<phi> U" for U
    2.50 +    proof -
    2.51 +      have "\<exists>y. x \<notin> A y" if "x \<notin> U" and Usub: "U \<subseteq> (\<Inter>x. A x)" for x
    2.52 +      proof -
    2.53 +        obtain e where "e > 0" and e: "ball x e \<subseteq> -U"
    2.54 +          using \<open>closed U\<close> \<open>x \<notin> U\<close> openE [of "-U"] by blast
    2.55 +        moreover obtain K where K: "ball x e = UNION K B"
    2.56 +          using open_cov [of "ball x e"] by auto
    2.57 +        ultimately have "UNION K B \<subseteq> -U"
    2.58 +          by blast
    2.59 +        have "K \<noteq> {}"
    2.60 +          using \<open>0 < e\<close> \<open>ball x e = UNION K B\<close> by auto
    2.61 +        then obtain n where "n \<in> K" "x \<in> B n"
    2.62 +          by (metis K UN_E \<open>0 < e\<close> centre_in_ball)
    2.63 +        then have "U \<inter> B n = {}"
    2.64 +          using K e by auto
    2.65 +        show ?thesis
    2.66 +        proof (cases "\<exists>U\<subseteq>A n. closed U \<and> \<phi> U \<and> U \<inter> B n = {}")
    2.67 +          case True
    2.68 +          then show ?thesis
    2.69 +            apply (rule_tac x="Suc n" in exI)
    2.70 +            apply (simp add: ASuc)
    2.71 +            apply (erule someI2_ex)
    2.72 +            using \<open>x \<in> B n\<close> by blast
    2.73 +        next
    2.74 +          case False
    2.75 +          then show ?thesis
    2.76 +            by (meson Inf_lower Usub \<open>U \<inter> B n = {}\<close> \<open>\<phi> U\<close> \<open>closed U\<close> range_eqI subset_trans)
    2.77 +        qed
    2.78 +      qed
    2.79 +      with that show ?thesis
    2.80 +        by (meson Inter_iff psubsetE rangeI subsetI)
    2.81 +    qed
    2.82 +  qed
    2.83 +qed
    2.84 +
    2.85 +corollary Brouwer_reduction_theorem:
    2.86 +  fixes S :: "'a::euclidean_space set"
    2.87 +  assumes "compact S" "\<phi> S" "S \<noteq> {}"
    2.88 +      and \<phi>: "\<And>F. \<lbrakk>\<And>n. compact(F n); \<And>n. F n \<noteq> {}; \<And>n. \<phi>(F n); \<And>n. F(Suc n) \<subseteq> F n\<rbrakk> \<Longrightarrow> \<phi>(\<Inter>range F)"
    2.89 +  obtains T where "T \<subseteq> S" "compact T" "T \<noteq> {}" "\<phi> T"
    2.90 +                  "\<And>U. \<lbrakk>U \<subseteq> S; closed U; U \<noteq> {}; \<phi> U\<rbrakk> \<Longrightarrow> \<not> (U \<subset> T)"
    2.91 +proof (rule Brouwer_reduction_theorem_gen [of S "\<lambda>T. T \<noteq> {} \<and> T \<subseteq> S \<and> \<phi> T"])
    2.92 +  fix F
    2.93 +  assume cloF: "\<And>n. closed (F n)"
    2.94 +     and F: "\<And>n. F n \<noteq> {} \<and> F n \<subseteq> S \<and> \<phi> (F n)" and Fsub: "\<And>n. F (Suc n) \<subseteq> F n"
    2.95 +  show "INTER UNIV F \<noteq> {} \<and> INTER UNIV F \<subseteq> S \<and> \<phi> (INTER UNIV F)"
    2.96 +  proof (intro conjI)
    2.97 +    show "INTER UNIV F \<noteq> {}"
    2.98 +      apply (rule compact_nest)
    2.99 +      apply (meson F cloF \<open>compact S\<close> seq_compact_closed_subset seq_compact_eq_compact)
   2.100 +       apply (simp add: F)
   2.101 +      by (meson Fsub lift_Suc_antimono_le)
   2.102 +    show " INTER UNIV F \<subseteq> S"
   2.103 +      using F by blast
   2.104 +    show "\<phi> (INTER UNIV F)"
   2.105 +      by (metis F Fsub \<phi> \<open>compact S\<close> cloF closed_Int_compact inf.orderE)
   2.106 +  qed
   2.107 +next
   2.108 +  show "S \<noteq> {} \<and> S \<subseteq> S \<and> \<phi> S"
   2.109 +    by (simp add: assms)
   2.110 +qed (meson assms compact_imp_closed seq_compact_closed_subset seq_compact_eq_compact)+
   2.111 +
   2.112 +
   2.113 +subsection\<open>Arcwise Connections\<close>
   2.114 +
   2.115 +subsection\<open>Density of points with dyadic rational coordinates.\<close>
   2.116 +
   2.117 +proposition closure_dyadic_rationals:
   2.118 +    "closure (\<Union>k. \<Union>f \<in> Basis \<rightarrow> \<int>.
   2.119 +                   { \<Sum>i :: 'a :: euclidean_space \<in> Basis. (f i / 2^k) *\<^sub>R i }) = UNIV"
   2.120 +proof -
   2.121 +  have "x \<in> closure (\<Union>k. \<Union>f \<in> Basis \<rightarrow> \<int>. {\<Sum>i \<in> Basis. (f i / 2^k) *\<^sub>R i})" for x::'a
   2.122 +  proof (clarsimp simp: closure_approachable)
   2.123 +    fix e::real
   2.124 +    assume "e > 0"
   2.125 +    then obtain k where k: "(1/2)^k < e/DIM('a)"
   2.126 +      by (meson DIM_positive divide_less_eq_1_pos of_nat_0_less_iff one_less_numeral_iff real_arch_pow_inv semiring_norm(76) zero_less_divide_iff zero_less_numeral)
   2.127 +    have "dist (\<Sum>i\<in>Basis. (real_of_int \<lfloor>2^k*(x \<bullet> i)\<rfloor> / 2^k) *\<^sub>R i) x =
   2.128 +          dist (\<Sum>i\<in>Basis. (real_of_int \<lfloor>2^k*(x \<bullet> i)\<rfloor> / 2^k) *\<^sub>R i) (\<Sum>i\<in>Basis. (x \<bullet> i) *\<^sub>R i)"
   2.129 +      by (simp add: euclidean_representation)
   2.130 +    also have "... = norm ((\<Sum>i\<in>Basis. (real_of_int \<lfloor>2^k*(x \<bullet> i)\<rfloor> / 2^k) *\<^sub>R i - (x \<bullet> i) *\<^sub>R i))"
   2.131 +      by (simp add: dist_norm sum_subtractf)
   2.132 +    also have "... \<le> DIM('a)*((1/2)^k)"
   2.133 +    proof (rule sum_norm_bound, simp add: algebra_simps)
   2.134 +      fix i::'a
   2.135 +      assume "i \<in> Basis"
   2.136 +      then have "norm ((real_of_int \<lfloor>x \<bullet> i*2^k\<rfloor> / 2^k) *\<^sub>R i - (x \<bullet> i) *\<^sub>R i) =
   2.137 +                 \<bar>real_of_int \<lfloor>x \<bullet> i*2^k\<rfloor> / 2^k - x \<bullet> i\<bar>"
   2.138 +        by (simp add: scaleR_left_diff_distrib [symmetric])
   2.139 +      also have "... \<le> (1/2) ^ k"
   2.140 +        by (simp add: divide_simps) linarith
   2.141 +      finally show "norm ((real_of_int \<lfloor>x \<bullet> i*2^k\<rfloor> / 2^k) *\<^sub>R i - (x \<bullet> i) *\<^sub>R i) \<le> (1/2) ^ k" .
   2.142 +    qed
   2.143 +    also have "... < DIM('a)*(e/DIM('a))"
   2.144 +      using DIM_positive k linordered_comm_semiring_strict_class.comm_mult_strict_left_mono of_nat_0_less_iff by blast
   2.145 +    also have "... = e"
   2.146 +      by simp
   2.147 +    finally have "dist (\<Sum>i\<in>Basis. (\<lfloor>2^k*(x \<bullet> i)\<rfloor> / 2^k) *\<^sub>R i) x < e" .
   2.148 +    then
   2.149 +    show "\<exists>k. \<exists>f \<in> Basis \<rightarrow> \<int>. dist (\<Sum>b\<in>Basis. (f b / 2^k) *\<^sub>R b) x < e"
   2.150 +      apply (rule_tac x=k in exI)
   2.151 +      apply (rule_tac x="\<lambda>i. of_int (floor (2^k*(x \<bullet> i)))" in bexI)
   2.152 +       apply auto
   2.153 +      done
   2.154 +  qed
   2.155 +  then show ?thesis by auto
   2.156 +qed
   2.157 +
   2.158 +corollary closure_rational_coordinates:
   2.159 +    "closure (\<Union>f \<in> Basis \<rightarrow> \<rat>. { \<Sum>i :: 'a :: euclidean_space \<in> Basis. f i *\<^sub>R i }) = UNIV"
   2.160 +proof -
   2.161 +  have *: "(\<Union>k. \<Union>f \<in> Basis \<rightarrow> \<int>. { \<Sum>i::'a \<in> Basis. (f i / 2^k) *\<^sub>R i })
   2.162 +           \<subseteq> (\<Union>f \<in> Basis \<rightarrow> \<rat>. { \<Sum>i \<in> Basis. f i *\<^sub>R i })"
   2.163 +  proof clarsimp
   2.164 +    fix k and f :: "'a \<Rightarrow> real"
   2.165 +    assume f: "f \<in> Basis \<rightarrow> \<int>"
   2.166 +    show "\<exists>x \<in> Basis \<rightarrow> \<rat>. (\<Sum>i \<in> Basis. (f i / 2^k) *\<^sub>R i) = (\<Sum>i \<in> Basis. x i *\<^sub>R i)"
   2.167 +      apply (rule_tac x="\<lambda>i. f i / 2^k" in bexI)
   2.168 +      using Ints_subset_Rats f by auto
   2.169 +  qed
   2.170 +  show ?thesis
   2.171 +    using closure_dyadic_rationals closure_mono [OF *] by blast
   2.172 +qed
   2.173 +
   2.174 +lemma closure_dyadic_rationals_in_convex_set:
   2.175 +   "\<lbrakk>convex S; interior S \<noteq> {}\<rbrakk>
   2.176 +        \<Longrightarrow> closure(S \<inter>
   2.177 +                    (\<Union>k. \<Union>f \<in> Basis \<rightarrow> \<int>.
   2.178 +                   { \<Sum>i :: 'a :: euclidean_space \<in> Basis. (f i / 2^k) *\<^sub>R i })) =
   2.179 +            closure S"
   2.180 +  by (simp add: closure_dyadic_rationals closure_convex_Int_superset)
   2.181 +
   2.182 +lemma closure_rationals_in_convex_set:
   2.183 +   "\<lbrakk>convex S; interior S \<noteq> {}\<rbrakk>
   2.184 +    \<Longrightarrow> closure(S \<inter> (\<Union>f \<in> Basis \<rightarrow> \<rat>. { \<Sum>i :: 'a :: euclidean_space \<in> Basis. f i *\<^sub>R i })) =
   2.185 +        closure S"
   2.186 +  by (simp add: closure_rational_coordinates closure_convex_Int_superset)
   2.187 +
   2.188 +
   2.189 +text\<open> Every path between distinct points contains an arc, and hence
   2.190 +path connection is equivalent to arcwise connection for distinct points.
   2.191 +The proof is based on Whyburn's "Topological Analysis".\<close>
   2.192 +
   2.193 +lemma closure_dyadic_rationals_in_convex_set_pos_1:
   2.194 +  fixes S :: "real set"
   2.195 +  assumes "convex S" and intnz: "interior S \<noteq> {}" and pos: "\<And>x. x \<in> S \<Longrightarrow> 0 \<le> x"
   2.196 +    shows "closure(S \<inter> (\<Union>k m. {of_nat m / 2^k})) = closure S"
   2.197 +proof -
   2.198 +  have "\<exists>m. f 1/2^k = real m / 2^k" if "(f 1) / 2^k \<in> S" "f 1 \<in> \<int>" for k and f :: "real \<Rightarrow> real"
   2.199 +    using that by (force simp: Ints_def zero_le_divide_iff power_le_zero_eq dest: pos zero_le_imp_eq_int)
   2.200 +  then have "S \<inter> (\<Union>k m. {real m / 2^k}) = S \<inter>
   2.201 +             (\<Union>k. \<Union>f\<in>Basis \<rightarrow> \<int>. {\<Sum>i\<in>Basis. (f i / 2^k) *\<^sub>R i})"
   2.202 +    by force
   2.203 +  then show ?thesis
   2.204 +    using closure_dyadic_rationals_in_convex_set [OF \<open>convex S\<close> intnz] by simp
   2.205 +qed
   2.206 +
   2.207 +
   2.208 +definition dyadics :: "'a::field_char_0 set" where "dyadics \<equiv> \<Union>k m. {of_nat m / 2^k}"
   2.209 +
   2.210 +lemma real_in_dyadics [simp]: "real m \<in> dyadics"
   2.211 +  apply (simp add: dyadics_def)
   2.212 +  by (metis divide_numeral_1 numeral_One power_0)
   2.213 +
   2.214 +lemma nat_neq_4k1: "of_nat m \<noteq> (4 * of_nat k + 1) / (2 * 2^n :: 'a::field_char_0)"
   2.215 +proof
   2.216 +  assume "of_nat m = (4 * of_nat k + 1) / (2 * 2^n :: 'a)"
   2.217 +  then have "of_nat (m * (2 * 2^n)) = (of_nat (Suc (4 * k)) :: 'a)"
   2.218 +    by (simp add: divide_simps)
   2.219 +  then have "m * (2 * 2^n) = Suc (4 * k)"
   2.220 +    using of_nat_eq_iff by blast
   2.221 +  then have "odd (m * (2 * 2^n))"
   2.222 +    by simp
   2.223 +  then show False
   2.224 +    by simp
   2.225 +qed
   2.226 +
   2.227 +lemma nat_neq_4k3: "of_nat m \<noteq> (4 * of_nat k + 3) / (2 * 2^n :: 'a::field_char_0)"
   2.228 +proof
   2.229 +  assume "of_nat m = (4 * of_nat k + 3) / (2 * 2^n :: 'a)"
   2.230 +  then have "of_nat (m * (2 * 2^n)) = (of_nat (4 * k + 3) :: 'a)"
   2.231 +    by (simp add: divide_simps)
   2.232 +  then have "m * (2 * 2^n) = (4 * k) + 3"
   2.233 +    using of_nat_eq_iff by blast
   2.234 +  then have "odd (m * (2 * 2^n))"
   2.235 +    by simp
   2.236 +  then show False
   2.237 +    by simp
   2.238 +qed
   2.239 +
   2.240 +lemma iff_4k:
   2.241 +  assumes "r = real k" "odd k"
   2.242 +    shows "(4 * real m + r) / (2 * 2^n) = (4 * real m' + r) / (2 * 2 ^ n') \<longleftrightarrow> m=m' \<and> n=n'"
   2.243 +proof -
   2.244 +  { assume "(4 * real m + r) / (2 * 2^n) = (4 * real m' + r) / (2 * 2 ^ n')"
   2.245 +    then have "real ((4 * m + k) * (2 * 2 ^ n')) = real ((4 * m' + k) * (2 * 2^n))"
   2.246 +      using assms by (auto simp: field_simps)
   2.247 +    then have "(4 * m + k) * (2 * 2 ^ n') = (4 * m' + k) * (2 * 2^n)"
   2.248 +      using of_nat_eq_iff by blast
   2.249 +    then have "(4 * m + k) * (2 ^ n') = (4 * m' + k) * (2^n)"
   2.250 +      by linarith
   2.251 +    then obtain "4*m + k = 4*m' + k" "n=n'"
   2.252 +      apply (rule prime_power_cancel2 [OF two_is_prime_nat])
   2.253 +      using assms by auto
   2.254 +    then have "m=m'" "n=n'"
   2.255 +      by auto
   2.256 +  }
   2.257 +  then show ?thesis by blast
   2.258 +qed
   2.259 +
   2.260 +lemma neq_4k1_k43: "(4 * real m + 1) / (2 * 2^n) \<noteq> (4 * real m' + 3) / (2 * 2 ^ n')"
   2.261 +proof
   2.262 +  assume "(4 * real m + 1) / (2 * 2^n) = (4 * real m' + 3) / (2 * 2 ^ n')"
   2.263 +  then have "real (Suc (4 * m) * (2 * 2 ^ n')) = real ((4 * m' + 3) * (2 * 2^n))"
   2.264 +    by (auto simp: field_simps)
   2.265 +  then have "Suc (4 * m) * (2 * 2 ^ n') = (4 * m' + 3) * (2 * 2^n)"
   2.266 +    using of_nat_eq_iff by blast
   2.267 +  then have "Suc (4 * m) * (2 ^ n') = (4 * m' + 3) * (2^n)"
   2.268 +    by linarith
   2.269 +  then have "Suc (4 * m) = (4 * m' + 3)"
   2.270 +    by (rule prime_power_cancel2 [OF two_is_prime_nat]) auto
   2.271 +  then have "1 + 2 * m' = 2 * m"
   2.272 +    using \<open>Suc (4 * m) = 4 * m' + 3\<close> by linarith
   2.273 +  then show False
   2.274 +    using even_Suc by presburger
   2.275 +qed
   2.276 +
   2.277 +lemma dyadic_413_cases:
   2.278 +  obtains "(of_nat m::'a::field_char_0) / 2^k \<in> Nats"
   2.279 +  | m' k' where "k' < k" "(of_nat m:: 'a) / 2^k = of_nat (4*m' + 1) / 2^Suc k'"
   2.280 +  | m' k' where "k' < k" "(of_nat m:: 'a) / 2^k = of_nat (4*m' + 3) / 2^Suc k'"
   2.281 +proof (cases "m>0")
   2.282 +  case False
   2.283 +  then have "m=0" by simp
   2.284 +  with that show ?thesis by auto
   2.285 +next
   2.286 +  case True
   2.287 +  obtain k' m' where m': "odd m'" and k': "m = m' * 2^k'"
   2.288 +    using prime_power_canonical [OF two_is_prime_nat True] by blast
   2.289 +  then obtain q r where q: "m' = 4*q + r" and r: "r < 4"
   2.290 +    by (metis not_add_less2 split_div zero_neq_numeral)
   2.291 +  show ?thesis
   2.292 +  proof (cases "k \<le> k'")
   2.293 +    case True
   2.294 +    have "(of_nat m:: 'a) / 2^k = of_nat m' * (2 ^ k' / 2^k)"
   2.295 +      using k' by (simp add: field_simps)
   2.296 +    also have "... = (of_nat m'::'a) * 2 ^ (k'-k)"
   2.297 +      using k' True by (simp add: power_diff)
   2.298 +    also have "... \<in> \<nat>"
   2.299 +      by (metis Nats_mult of_nat_in_Nats of_nat_numeral of_nat_power)
   2.300 +    finally show ?thesis by (auto simp: that)
   2.301 +  next
   2.302 +    case False
   2.303 +    then obtain kd where kd: "Suc kd = k - k'"
   2.304 +      using Suc_diff_Suc not_less by blast
   2.305 +    have "(of_nat m:: 'a) / 2^k = of_nat m' * (2 ^ k' / 2^k)"
   2.306 +      using k' by (simp add: field_simps)
   2.307 +    also have "... = (of_nat m'::'a) / 2 ^ (k-k')"
   2.308 +      using k' False by (simp add: power_diff)
   2.309 +    also have "... = ((of_nat r + 4 * of_nat q)::'a) / 2 ^ (k-k')"
   2.310 +      using q by force
   2.311 +    finally have meq: "(of_nat m:: 'a) / 2^k = (of_nat r + 4 * of_nat q) / 2 ^ (k - k')" .
   2.312 +    have "r \<noteq> 0" "r \<noteq> 2"
   2.313 +      using q m' by presburger+
   2.314 +    with r consider "r = 1" | "r = 3"
   2.315 +      by linarith
   2.316 +    then show ?thesis
   2.317 +    proof cases
   2.318 +      assume "r = 1"
   2.319 +      with meq kd that(2) [of kd q] show ?thesis
   2.320 +        by simp
   2.321 +    next
   2.322 +      assume "r = 3"
   2.323 +      with meq kd that(3) [of kd q]  show ?thesis
   2.324 +        by simp
   2.325 +    qed
   2.326 +  qed
   2.327 +qed
   2.328 +
   2.329 +
   2.330 +lemma dyadics_iff:
   2.331 +   "(dyadics :: 'a::field_char_0 set) =
   2.332 +    Nats \<union> (\<Union>k m. {of_nat (4*m + 1) / 2^Suc k}) \<union> (\<Union>k m. {of_nat (4*m + 3) / 2^Suc k})"
   2.333 +           (is "_ = ?rhs")
   2.334 +proof
   2.335 +  show "dyadics \<subseteq> ?rhs"
   2.336 +    unfolding dyadics_def
   2.337 +    apply clarify
   2.338 +    apply (rule dyadic_413_cases, force+)
   2.339 +    done
   2.340 +next
   2.341 +  show "?rhs \<subseteq> dyadics"
   2.342 +    apply (clarsimp simp: dyadics_def Nats_def simp del: power_Suc)
   2.343 +    apply (intro conjI subsetI)
   2.344 +    apply (auto simp del: power_Suc)
   2.345 +      apply (metis divide_numeral_1 numeral_One power_0)
   2.346 +     apply (metis of_nat_Suc of_nat_mult of_nat_numeral)
   2.347 +    by (metis of_nat_add of_nat_mult of_nat_numeral)
   2.348 +qed
   2.349 +
   2.350 +
   2.351 +function (domintros) dyad_rec :: "[nat \<Rightarrow> 'a, 'a\<Rightarrow>'a, 'a\<Rightarrow>'a, real] \<Rightarrow> 'a" where
   2.352 +    "dyad_rec b l r (real m) = b m"
   2.353 +  | "dyad_rec b l r ((4 * real m + 1) / 2 ^ (Suc n)) = l (dyad_rec b l r ((2*m + 1) / 2^n))"
   2.354 +  | "dyad_rec b l r ((4 * real m + 3) / 2 ^ (Suc n)) = r (dyad_rec b l r ((2*m + 1) / 2^n))"
   2.355 +  | "x \<notin> dyadics \<Longrightarrow> dyad_rec b l r x = undefined"
   2.356 +  using iff_4k [of _ 1] iff_4k [of _ 3]
   2.357 +         apply (simp_all add: nat_neq_4k1 nat_neq_4k3 neq_4k1_k43, atomize_elim)
   2.358 +     apply (fastforce simp add: dyadics_iff Nats_def field_simps)+
   2.359 +  done
   2.360 +
   2.361 +lemma dyadics_levels: "dyadics = (\<Union>K. \<Union>k<K. \<Union> m. {of_nat m / 2^k})"
   2.362 +  unfolding dyadics_def by auto
   2.363 +
   2.364 +lemma dyad_rec_level_termination:
   2.365 +  assumes "k < K"
   2.366 +  shows "dyad_rec_dom(b, l, r, real m / 2^k)"
   2.367 +  using assms
   2.368 +proof (induction K arbitrary: k m)
   2.369 +  case 0
   2.370 +  then show ?case by auto
   2.371 +next
   2.372 +  case (Suc K)
   2.373 +  then consider "k = K" | "k < K"
   2.374 +    using less_antisym by blast
   2.375 +  then show ?case
   2.376 +  proof cases
   2.377 +    assume "k = K"
   2.378 +    show ?case
   2.379 +    proof (rule dyadic_413_cases [of m k, where 'a=real])
   2.380 +      show "real m / 2^k \<in> \<nat> \<Longrightarrow> dyad_rec_dom (b, l, r, real m / 2^k)"
   2.381 +        by (force simp: Nats_def nat_neq_4k1 nat_neq_4k3 intro: dyad_rec.domintros)
   2.382 +      show ?case if "k' < k" and eq: "real m / 2^k = real (4 * m' + 1) / 2^Suc k'" for m' k'
   2.383 +      proof -
   2.384 +        have "dyad_rec_dom (b, l, r, (4 * real m' + 1) / 2^Suc k')"
   2.385 +        proof (rule dyad_rec.domintros)
   2.386 +          fix m n
   2.387 +          assume "(4 * real m' + 1) / (2 * 2 ^ k') = (4 * real m + 1) / (2 * 2^n)"
   2.388 +          then have "m' = m" "k' = n" using iff_4k [of _ 1]
   2.389 +            by auto
   2.390 +          have "dyad_rec_dom (b, l, r, real (2 * m + 1) / 2 ^ k')"
   2.391 +            using Suc.IH \<open>k = K\<close> \<open>k' < k\<close> by blast
   2.392 +          then show "dyad_rec_dom (b, l, r, (2 * real m + 1) / 2^n)"
   2.393 +            using \<open>k' = n\<close> by (auto simp: algebra_simps)
   2.394 +        next
   2.395 +          fix m n
   2.396 +          assume "(4 * real m' + 1) / (2 * 2 ^ k') = (4 * real m + 3) / (2 * 2^n)"
   2.397 +          then have "False"
   2.398 +            by (metis neq_4k1_k43)
   2.399 +          then show "dyad_rec_dom (b, l, r, (2 * real m + 1) / 2^n)" ..
   2.400 +        qed
   2.401 +        then show ?case by (simp add: eq add_ac)
   2.402 +      qed
   2.403 +      show ?case if "k' < k" and eq: "real m / 2^k = real (4 * m' + 3) / 2^Suc k'" for m' k'
   2.404 +      proof -
   2.405 +        have "dyad_rec_dom (b, l, r, (4 * real m' + 3) / 2^Suc k')"
   2.406 +        proof (rule dyad_rec.domintros)
   2.407 +          fix m n
   2.408 +          assume "(4 * real m' + 3) / (2 * 2 ^ k') = (4 * real m + 1) / (2 * 2^n)"
   2.409 +          then have "False"
   2.410 +            by (metis neq_4k1_k43)
   2.411 +          then show "dyad_rec_dom (b, l, r, (2 * real m + 1) / 2^n)" ..
   2.412 +        next
   2.413 +          fix m n
   2.414 +          assume "(4 * real m' + 3) / (2 * 2 ^ k') = (4 * real m + 3) / (2 * 2^n)"
   2.415 +          then have "m' = m" "k' = n" using iff_4k [of _ 3]
   2.416 +            by auto
   2.417 +          have "dyad_rec_dom (b, l, r, real (2 * m + 1) / 2 ^ k')"
   2.418 +            using Suc.IH \<open>k = K\<close> \<open>k' < k\<close> by blast
   2.419 +          then show "dyad_rec_dom (b, l, r, (2 * real m + 1) / 2^n)"
   2.420 +            using \<open>k' = n\<close> by (auto simp: algebra_simps)
   2.421 +        qed
   2.422 +        then show ?case by (simp add: eq add_ac)
   2.423 +      qed
   2.424 +    qed
   2.425 +  next
   2.426 +    assume "k < K"
   2.427 +    then show ?case
   2.428 +      using Suc.IH by blast
   2.429 +  qed
   2.430 +qed
   2.431 +
   2.432 +
   2.433 +lemma dyad_rec_termination: "x \<in> dyadics \<Longrightarrow> dyad_rec_dom(b,l,r,x)"
   2.434 +  by (auto simp: dyadics_levels intro: dyad_rec_level_termination)
   2.435 +
   2.436 +lemma dyad_rec_of_nat [simp]: "dyad_rec b l r (real m) = b m"
   2.437 +  by (simp add: dyad_rec.psimps dyad_rec_termination)
   2.438 +
   2.439 +lemma dyad_rec_41 [simp]: "dyad_rec b l r ((4 * real m + 1) / 2 ^ (Suc n)) = l (dyad_rec b l r ((2*m + 1) / 2^n))"
   2.440 +  apply (rule dyad_rec.psimps)
   2.441 +  by (metis dyad_rec_level_termination lessI add.commute of_nat_Suc of_nat_mult of_nat_numeral)
   2.442 +
   2.443 +
   2.444 +lemma dyad_rec_43 [simp]: "dyad_rec b l r ((4 * real m + 3) / 2 ^ (Suc n)) = r (dyad_rec b l r ((2*m + 1) / 2^n))"
   2.445 +  apply (rule dyad_rec.psimps)
   2.446 +  by (metis dyad_rec_level_termination lessI of_nat_add of_nat_mult of_nat_numeral)
   2.447 +
   2.448 +lemma dyad_rec_41_times2:
   2.449 +  assumes "n > 0"
   2.450 +    shows "dyad_rec b l r (2 * ((4 * real m + 1) / 2^Suc n)) = l (dyad_rec b l r (2 * (2 * real m + 1) / 2^n))"
   2.451 +proof -
   2.452 +  obtain n' where n': "n = Suc n'"
   2.453 +    using assms not0_implies_Suc by blast
   2.454 +  have "dyad_rec b l r (2 * ((4 * real m + 1) / 2^Suc n)) = dyad_rec b l r ((2 * (4 * real m + 1)) / (2 * 2^n))"
   2.455 +    by auto
   2.456 +  also have "... = dyad_rec b l r ((4 * real m + 1) / 2^n)"
   2.457 +    by (subst mult_divide_mult_cancel_left) auto
   2.458 +  also have "... = l (dyad_rec b l r ((2 * real m + 1) / 2 ^ n'))"
   2.459 +    by (simp add: add.commute [of 1] n' del: power_Suc)
   2.460 +  also have "... = l (dyad_rec b l r ((2 * (2 * real m + 1)) / (2 * 2 ^ n')))"
   2.461 +    by (subst mult_divide_mult_cancel_left) auto
   2.462 +  also have "... = l (dyad_rec b l r (2 * (2 * real m + 1) / 2^n))"
   2.463 +    by (simp add: add.commute n')
   2.464 +  finally show ?thesis .
   2.465 +qed
   2.466 +
   2.467 +lemma dyad_rec_43_times2:
   2.468 +  assumes "n > 0"
   2.469 +    shows "dyad_rec b l r (2 * ((4 * real m + 3) / 2^Suc n)) = r (dyad_rec b l r (2 * (2 * real m + 1) / 2^n))"
   2.470 +proof -
   2.471 +  obtain n' where n': "n = Suc n'"
   2.472 +    using assms not0_implies_Suc by blast
   2.473 +  have "dyad_rec b l r (2 * ((4 * real m + 3) / 2^Suc n)) = dyad_rec b l r ((2 * (4 * real m + 3)) / (2 * 2^n))"
   2.474 +    by auto
   2.475 +  also have "... = dyad_rec b l r ((4 * real m + 3) / 2^n)"
   2.476 +    by (subst mult_divide_mult_cancel_left) auto
   2.477 +  also have "... = r (dyad_rec b l r ((2 * real m + 1) / 2 ^ n'))"
   2.478 +    by (simp add: n' del: power_Suc)
   2.479 +  also have "... = r (dyad_rec b l r ((2 * (2 * real m + 1)) / (2 * 2 ^ n')))"
   2.480 +    by (subst mult_divide_mult_cancel_left) auto
   2.481 +  also have "... = r (dyad_rec b l r (2 * (2 * real m + 1) / 2^n))"
   2.482 +    by (simp add: n')
   2.483 +  finally show ?thesis .
   2.484 +qed
   2.485 +
   2.486 +definition dyad_rec2
   2.487 +    where "dyad_rec2 u v lc rc x =
   2.488 +             dyad_rec (\<lambda>z. (u,v)) (\<lambda>(a,b). (a, lc a b (midpoint a b))) (\<lambda>(a,b). (rc a b (midpoint a b), b)) (2*x)"
   2.489 +
   2.490 +abbreviation leftrec where "leftrec u v lc rc x \<equiv> fst (dyad_rec2 u v lc rc x)"
   2.491 +abbreviation rightrec where "rightrec u v lc rc x \<equiv> snd (dyad_rec2 u v lc rc x)"
   2.492 +
   2.493 +lemma leftrec_base: "leftrec u v lc rc (real m / 2) = u"
   2.494 +  by (simp add: dyad_rec2_def)
   2.495 +
   2.496 +lemma leftrec_41: "n > 0 \<Longrightarrow> leftrec u v lc rc ((4 * real m + 1) / 2 ^ (Suc n)) = leftrec u v lc rc ((2 * real m + 1) / 2^n)"
   2.497 +  apply (simp only: dyad_rec2_def dyad_rec_41_times2)
   2.498 +  apply (simp add: case_prod_beta)
   2.499 +  done
   2.500 +
   2.501 +lemma leftrec_43: "n > 0 \<Longrightarrow>
   2.502 +             leftrec u v lc rc ((4 * real m + 3) / 2 ^ (Suc n)) =
   2.503 +                 rc (leftrec u v lc rc ((2 * real m + 1) / 2^n)) (rightrec u v lc rc ((2 * real m + 1) / 2^n))
   2.504 +                 (midpoint (leftrec u v lc rc ((2 * real m + 1) / 2^n)) (rightrec u v lc rc ((2 * real m + 1) / 2^n)))"
   2.505 +  apply (simp only: dyad_rec2_def dyad_rec_43_times2)
   2.506 +  apply (simp add: case_prod_beta)
   2.507 +  done
   2.508 +
   2.509 +lemma rightrec_base: "rightrec u v lc rc (real m / 2) = v"
   2.510 +  by (simp add: dyad_rec2_def)
   2.511 +
   2.512 +lemma rightrec_41: "n > 0 \<Longrightarrow>
   2.513 +             rightrec u v lc rc ((4 * real m + 1) / 2 ^ (Suc n)) =
   2.514 +                 lc (leftrec u v lc rc ((2 * real m + 1) / 2^n)) (rightrec u v lc rc ((2 * real m + 1) / 2^n))
   2.515 +                 (midpoint (leftrec u v lc rc ((2 * real m + 1) / 2^n)) (rightrec u v lc rc ((2 * real m + 1) / 2^n)))"
   2.516 +  apply (simp only: dyad_rec2_def dyad_rec_41_times2)
   2.517 +  apply (simp add: case_prod_beta)
   2.518 +  done
   2.519 +
   2.520 +lemma rightrec_43: "n > 0 \<Longrightarrow> rightrec u v lc rc ((4 * real m + 3) / 2 ^ (Suc n)) = rightrec u v lc rc ((2 * real m + 1) / 2^n)"
   2.521 +  apply (simp only: dyad_rec2_def dyad_rec_43_times2)
   2.522 +  apply (simp add: case_prod_beta)
   2.523 +  done
   2.524 +
   2.525 +lemma dyadics_in_open_unit_interval:
   2.526 +   "{0<..<1} \<inter> (\<Union>k m. {real m / 2^k}) = (\<Union>k. \<Union>m \<in> {0<..<2^k}. {real m / 2^k})"
   2.527 +  by (auto simp: divide_simps)
   2.528 +
   2.529 +
   2.530 +
   2.531 +theorem homeomorphic_monotone_image_interval:
   2.532 +  fixes f :: "real \<Rightarrow> 'a::{real_normed_vector,complete_space}"
   2.533 +  assumes cont_f: "continuous_on {0..1} f"
   2.534 +      and conn: "\<And>y. connected ({0..1} \<inter> f -` {y})"
   2.535 +      and f_1not0: "f 1 \<noteq> f 0"
   2.536 +    shows "(f ` {0..1}) homeomorphic {0..1::real}"
   2.537 +proof -
   2.538 +  have "\<exists>c d. a \<le> c \<and> c \<le> m \<and> m \<le> d \<and> d \<le> b \<and>
   2.539 +              (\<forall>x \<in> {c..d}. f x = f m) \<and>
   2.540 +              (\<forall>x \<in> {a..<c}. (f x \<noteq> f m)) \<and>
   2.541 +              (\<forall>x \<in> {d<..b}. (f x \<noteq> f m)) \<and>
   2.542 +              (\<forall>x \<in> {a..<c}. \<forall>y \<in> {d<..b}. f x \<noteq> f y)"
   2.543 +    if m: "m \<in> {a..b}" and ab01: "{a..b} \<subseteq> {0..1}" for a b m
   2.544 +  proof -
   2.545 +    have comp: "compact (f -` {f m} \<inter> {0..1})"
   2.546 +      by (simp add: compact_eq_bounded_closed bounded_Int closed_vimage_Int cont_f)
   2.547 +    obtain c0 d0 where cd0: "{0..1} \<inter> f -` {f m} = {c0..d0}"
   2.548 +      using connected_compact_interval_1 [of "{0..1} \<inter> f -` {f m}"] conn comp
   2.549 +      by (metis Int_commute)
   2.550 +    with that have "m \<in> cbox c0 d0"
   2.551 +      by auto
   2.552 +    obtain c d where cd: "{a..b} \<inter> f -` {f m} = {c..d}"
   2.553 +      apply (rule_tac c="max a c0" and d="min b d0" in that)
   2.554 +      using ab01 cd0 by auto
   2.555 +    then have cdab: "{c..d} \<subseteq> {a..b}"
   2.556 +      by blast
   2.557 +    show ?thesis
   2.558 +    proof (intro exI conjI ballI)
   2.559 +      show "a \<le> c" "d \<le> b"
   2.560 +        using cdab cd m by auto
   2.561 +      show "c \<le> m" "m \<le> d"
   2.562 +        using cd m by auto
   2.563 +      show "\<And>x. x \<in> {c..d} \<Longrightarrow> f x = f m"
   2.564 +        using cd by blast
   2.565 +      show "f x \<noteq> f m" if "x \<in> {a..<c}" for x
   2.566 +        using that m cd [THEN equalityD1, THEN subsetD] \<open>c \<le> m\<close> by force
   2.567 +      show "f x \<noteq> f m" if "x \<in> {d<..b}" for x
   2.568 +        using that m cd [THEN equalityD1, THEN subsetD, of x] \<open>m \<le> d\<close> by force
   2.569 +      show "f x \<noteq> f y" if "x \<in> {a..<c}" "y \<in> {d<..b}" for x y
   2.570 +      proof (cases "f x = f m \<or> f y = f m")
   2.571 +        case True
   2.572 +        then show ?thesis
   2.573 +          using \<open>\<And>x. x \<in> {a..<c} \<Longrightarrow> f x \<noteq> f m\<close> that by auto
   2.574 +      next
   2.575 +        case False
   2.576 +        have False if "f x = f y"
   2.577 +        proof -
   2.578 +          have "x \<le> m" "m \<le> y"
   2.579 +            using \<open>c \<le> m\<close> \<open>x \<in> {a..<c}\<close>  \<open>m \<le> d\<close> \<open>y \<in> {d<..b}\<close> by auto
   2.580 +          then have "x \<in> ({0..1} \<inter> f -` {f y})" "y \<in> ({0..1} \<inter> f -` {f y})"
   2.581 +            using \<open>x \<in> {a..<c}\<close> \<open>y \<in> {d<..b}\<close> ab01 by (auto simp: that)
   2.582 +          then have "m \<in> ({0..1} \<inter> f -` {f y})"
   2.583 +            by (meson \<open>m \<le> y\<close> \<open>x \<le> m\<close> is_interval_connected_1 conn [of "f y"] is_interval_1)
   2.584 +          with False show False by auto
   2.585 +        qed
   2.586 +        then show ?thesis by auto
   2.587 +      qed
   2.588 +    qed
   2.589 +  qed
   2.590 +  then obtain leftcut rightcut where LR:
   2.591 +    "\<And>a b m. \<lbrakk>m \<in> {a..b}; {a..b} \<subseteq> {0..1}\<rbrakk> \<Longrightarrow>
   2.592 +            (a \<le> leftcut a b m \<and> leftcut a b m \<le> m \<and> m \<le> rightcut a b m \<and> rightcut a b m \<le> b \<and>
   2.593 +            (\<forall>x \<in> {leftcut a b m..rightcut a b m}. f x = f m) \<and>
   2.594 +            (\<forall>x \<in> {a..<leftcut a b m}. f x \<noteq> f m) \<and>
   2.595 +            (\<forall>x \<in> {rightcut a b m<..b}. f x \<noteq> f m) \<and>
   2.596 +            (\<forall>x \<in> {a..<leftcut a b m}. \<forall>y \<in> {rightcut a b m<..b}. f x \<noteq> f y))"
   2.597 +    apply atomize
   2.598 +    apply (clarsimp simp only: imp_conjL [symmetric] choice_iff choice_iff')
   2.599 +    apply (rule that, blast)
   2.600 +    done
   2.601 +  then have left_right: "\<And>a b m. \<lbrakk>m \<in> {a..b}; {a..b} \<subseteq> {0..1}\<rbrakk> \<Longrightarrow> a \<le> leftcut a b m \<and> rightcut a b m \<le> b"
   2.602 +    and left_right_m: "\<And>a b m. \<lbrakk>m \<in> {a..b}; {a..b} \<subseteq> {0..1}\<rbrakk> \<Longrightarrow> leftcut a b m \<le> m \<and> m \<le> rightcut a b m"
   2.603 +    by auto
   2.604 +  have left_neq: "\<lbrakk>a \<le> x; x < leftcut a b m; a \<le> m; m \<le> b; {a..b} \<subseteq> {0..1}\<rbrakk> \<Longrightarrow> f x \<noteq> f m"
   2.605 +    and right_neq: "\<lbrakk>rightcut a b m < x; x \<le> b; a \<le> m; m \<le> b; {a..b} \<subseteq> {0..1}\<rbrakk> \<Longrightarrow> f x \<noteq> f m"
   2.606 +    and left_right_neq: "\<lbrakk>a \<le> x; x < leftcut a b m; rightcut a b m < y; y \<le> b; a \<le> m; m \<le> b; {a..b} \<subseteq> {0..1}\<rbrakk> \<Longrightarrow> f x \<noteq> f m"
   2.607 +    and feqm: "\<lbrakk>leftcut a b m \<le> x; x \<le> rightcut a b m; a \<le> m; m \<le> b; {a..b} \<subseteq> {0..1}\<rbrakk>
   2.608 +                         \<Longrightarrow> f x = f m" for a b m x y
   2.609 +    by (meson atLeastAtMost_iff greaterThanAtMost_iff atLeastLessThan_iff LR)+
   2.610 +  have f_eqI: "\<And>a b m x y. \<lbrakk>leftcut a b m \<le> x; x \<le> rightcut a b m; leftcut a b m \<le> y; y \<le> rightcut a b m;
   2.611 +                             a \<le> m; m \<le> b; {a..b} \<subseteq> {0..1}\<rbrakk>  \<Longrightarrow> f x = f y"
   2.612 +    by (metis feqm)
   2.613 +  define u where "u \<equiv> rightcut 0 1 0"
   2.614 +  have lc[simp]: "leftcut 0 1 0 = 0" and u01: "0 \<le> u" "u \<le> 1"
   2.615 +    using LR [of 0 0 1] by (auto simp: u_def)
   2.616 +  have f0u: "\<And>x. x \<in> {0..u} \<Longrightarrow> f x = f 0"
   2.617 +    using LR [of 0 0 1] unfolding u_def [symmetric]
   2.618 +    by (metis \<open>leftcut 0 1 0 = 0\<close> atLeastAtMost_iff order_refl zero_le_one)
   2.619 +  have fu1: "\<And>x. x \<in> {u<..1} \<Longrightarrow> f x \<noteq> f 0"
   2.620 +    using LR [of 0 0 1] unfolding u_def [symmetric] by fastforce
   2.621 +  define v where "v \<equiv> leftcut u 1 1"
   2.622 +  have rc[simp]: "rightcut u 1 1 = 1" and v01: "u \<le> v" "v \<le> 1"
   2.623 +    using LR [of 1 u 1] u01  by (auto simp: v_def)
   2.624 +  have fuv: "\<And>x. x \<in> {u..<v} \<Longrightarrow> f x \<noteq> f 1"
   2.625 +    using LR [of 1 u 1] u01 v_def by fastforce
   2.626 +  have f0v: "\<And>x. x \<in> {0..<v} \<Longrightarrow> f x \<noteq> f 1"
   2.627 +    by (metis f_1not0 atLeastAtMost_iff atLeastLessThan_iff f0u fuv linear)
   2.628 +  have fv1: "\<And>x. x \<in> {v..1} \<Longrightarrow> f x = f 1"
   2.629 +    using LR [of 1 u 1] u01 v_def by (metis atLeastAtMost_iff atLeastatMost_subset_iff order_refl rc)
   2.630 +  define a where "a \<equiv> leftrec u v leftcut rightcut"
   2.631 +  define b where "b \<equiv> rightrec u v leftcut rightcut"
   2.632 +  define c where "c \<equiv> \<lambda>x. midpoint (a x) (b x)"
   2.633 +  have a_real [simp]: "a (real j) = u" for j
   2.634 +    using a_def leftrec_base
   2.635 +    by (metis nonzero_mult_div_cancel_right of_nat_mult of_nat_numeral zero_neq_numeral)
   2.636 +  have b_real [simp]: "b (real j) = v" for j
   2.637 +    using b_def rightrec_base
   2.638 +    by (metis nonzero_mult_div_cancel_right of_nat_mult of_nat_numeral zero_neq_numeral)
   2.639 +  have a41: "a ((4 * real m + 1) / 2^Suc n) = a ((2 * real m + 1) / 2^n)" if "n > 0" for m n
   2.640 +    using that a_def leftrec_41 by blast
   2.641 +  have b41: "b ((4 * real m + 1) / 2^Suc n) =
   2.642 +               leftcut (a ((2 * real m + 1) / 2^n))
   2.643 +                       (b ((2 * real m + 1) / 2^n))
   2.644 +                       (c ((2 * real m + 1) / 2^n))" if "n > 0" for m n
   2.645 +    using that a_def b_def c_def rightrec_41 by blast
   2.646 +  have a43: "a ((4 * real m + 3) / 2^Suc n) =
   2.647 +               rightcut (a ((2 * real m + 1) / 2^n))
   2.648 +                        (b ((2 * real m + 1) / 2^n))
   2.649 +                        (c ((2 * real m + 1) / 2^n))" if "n > 0" for m n
   2.650 +    using that a_def b_def c_def leftrec_43 by blast
   2.651 +  have b43: "b ((4 * real m + 3) / 2^Suc n) = b ((2 * real m + 1) / 2^n)" if "n > 0" for m n
   2.652 +    using that b_def rightrec_43 by blast
   2.653 +  have uabv: "u \<le> a (real m / 2 ^ n) \<and> a (real m / 2 ^ n) \<le> b (real m / 2 ^ n) \<and> b (real m / 2 ^ n) \<le> v" for m n
   2.654 +  proof (induction n arbitrary: m)
   2.655 +    case 0
   2.656 +    then show ?case by (simp add: v01)
   2.657 +  next
   2.658 +    case (Suc n p)
   2.659 +    show ?case
   2.660 +    proof (cases "even p")
   2.661 +      case True
   2.662 +      then obtain m where "p = 2*m" by (metis evenE)
   2.663 +      then show ?thesis
   2.664 +        by (simp add: Suc.IH)
   2.665 +    next
   2.666 +      case False
   2.667 +      then obtain m where m: "p = 2*m + 1" by (metis oddE)
   2.668 +      show ?thesis
   2.669 +      proof (cases n)
   2.670 +        case 0
   2.671 +        then show ?thesis
   2.672 +          by (simp add: a_def b_def leftrec_base rightrec_base v01)
   2.673 +      next
   2.674 +        case (Suc n')
   2.675 +        then have "n > 0" by simp
   2.676 +        have a_le_c: "a (real m / 2^n) \<le> c (real m / 2^n)" for m
   2.677 +          unfolding c_def by (metis Suc.IH ge_midpoint_1)
   2.678 +        have c_le_b: "c (real m / 2^n) \<le> b (real m / 2^n)" for m
   2.679 +          unfolding c_def by (metis Suc.IH le_midpoint_1)
   2.680 +        have c_ge_u: "c (real m / 2^n) \<ge> u" for m
   2.681 +          using Suc.IH a_le_c order_trans by blast
   2.682 +        have c_le_v: "c (real m / 2^n) \<le> v" for m
   2.683 +          using Suc.IH c_le_b order_trans by blast
   2.684 +        have a_ge_0: "0 \<le> a (real m / 2^n)" for m
   2.685 +          using Suc.IH order_trans u01(1) by blast
   2.686 +        have b_le_1: "b (real m / 2^n) \<le> 1" for m
   2.687 +          using Suc.IH order_trans v01(2) by blast
   2.688 +        have left_le: "leftcut (a ((real m) / 2^n)) (b ((real m) / 2^n)) (c ((real m) / 2^n)) \<le> c ((real m) / 2^n)" for m
   2.689 +          by (simp add: LR a_ge_0 a_le_c b_le_1 c_le_b)
   2.690 +        have right_ge: "rightcut (a ((real m) / 2^n)) (b ((real m) / 2^n)) (c ((real m) / 2^n)) \<ge> c ((real m) / 2^n)" for m
   2.691 +          by (simp add: LR a_ge_0 a_le_c b_le_1 c_le_b)
   2.692 +        show ?thesis
   2.693 +        proof (cases "even m")
   2.694 +          case True
   2.695 +          then obtain r where r: "m = 2*r" by (metis evenE)
   2.696 +          show ?thesis
   2.697 +            using a_le_c [of "m+1"] c_le_b [of "m+1"] a_ge_0 [of "m+1"] b_le_1 [of "m+1"]
   2.698 +              Suc.IH [of "m+1"]
   2.699 +            apply (simp add: r m add.commute [of 1] \<open>n > 0\<close> a41 b41 del: power_Suc)
   2.700 +            apply (auto simp: left_right [THEN conjunct1])
   2.701 +            using  order_trans [OF left_le c_le_v]
   2.702 +            by (metis (no_types, hide_lams) add.commute mult_2 of_nat_Suc of_nat_add)
   2.703 +        next
   2.704 +          case False
   2.705 +          then obtain r where r: "m = 2*r + 1" by (metis oddE)
   2.706 +          show ?thesis
   2.707 +            using a_le_c [of "m"] c_le_b [of "m"] a_ge_0 [of "m"] b_le_1 [of "m"]
   2.708 +              Suc.IH [of "m+1"]
   2.709 +            apply (simp add: r m add.commute [of 3] \<open>n > 0\<close> a43 b43 del: power_Suc)
   2.710 +            apply (auto simp: add.commute left_right [THEN conjunct2])
   2.711 +            using  order_trans [OF c_ge_u right_ge]
   2.712 +             apply (metis (no_types, hide_lams) mult_2 numeral_One of_nat_add of_nat_numeral)
   2.713 +            apply (metis Suc.IH mult_2 of_nat_1 of_nat_add)
   2.714 +            done
   2.715 +        qed
   2.716 +      qed
   2.717 +    qed
   2.718 +  qed
   2.719 +  have a_ge_0 [simp]: "0 \<le> a(m / 2^n)" and b_le_1 [simp]: "b(m / 2^n) \<le> 1" for m::nat and n
   2.720 +    using uabv order_trans u01 v01 by blast+
   2.721 +  then have b_ge_0 [simp]: "0 \<le> b(m / 2^n)" and a_le_1 [simp]: "a(m / 2^n) \<le> 1" for m::nat and n
   2.722 +    using uabv order_trans by blast+
   2.723 +  have alec [simp]: "a(m / 2^n) \<le> c(m / 2^n)" and cleb [simp]: "c(m / 2^n) \<le> b(m / 2^n)" for m::nat and n
   2.724 +    by (auto simp: c_def ge_midpoint_1 le_midpoint_1 uabv)
   2.725 +  have c_ge_0 [simp]: "0 \<le> c(m / 2^n)" and c_le_1 [simp]: "c(m / 2^n) \<le> 1" for m::nat and n
   2.726 +    using a_ge_0 alec order_trans apply blast
   2.727 +    by (meson b_le_1 cleb order_trans)
   2.728 +  have "\<lbrakk>d = m-n; odd j; \<bar>real i / 2^m - real j / 2^n\<bar> < 1/2 ^ n\<rbrakk>
   2.729 +        \<Longrightarrow> (a(j / 2^n)) \<le> (c(i / 2^m)) \<and> (c(i / 2^m)) \<le> (b(j / 2^n))" for d i j m n
   2.730 +  proof (induction d arbitrary: j n rule: less_induct)
   2.731 +    case (less d j n)
   2.732 +    show ?case
   2.733 +    proof (cases "m \<le> n")
   2.734 +      case True
   2.735 +      have "\<bar>2^n\<bar> * \<bar>real i / 2^m - real j / 2^n\<bar> = 0"
   2.736 +      proof (rule Ints_nonzero_abs_less1)
   2.737 +        have "(real i * 2^n - real j * 2^m) / 2^m = (real i * 2^n) / 2^m - (real j * 2^m) / 2^m"
   2.738 +          using diff_divide_distrib by blast
   2.739 +        also have "... = (real i * 2 ^ (n-m)) - (real j)"
   2.740 +          using True by (auto simp: power_diff field_simps)
   2.741 +        also have "... \<in> \<int>"
   2.742 +          by simp
   2.743 +        finally have "(real i * 2^n - real j * 2^m) / 2^m \<in> \<int>" .
   2.744 +        with True Ints_abs show "\<bar>2^n\<bar> * \<bar>real i / 2^m - real j / 2^n\<bar> \<in> \<int>"
   2.745 +          by (fastforce simp: divide_simps)
   2.746 +        show "\<bar>\<bar>2^n\<bar> * \<bar>real i / 2^m - real j / 2^n\<bar>\<bar> < 1"
   2.747 +          using less.prems by (auto simp: divide_simps)
   2.748 +      qed
   2.749 +      then have "real i / 2^m = real j / 2^n"
   2.750 +        by auto
   2.751 +      then show ?thesis
   2.752 +        by auto
   2.753 +    next
   2.754 +      case False
   2.755 +      then have "n < m" by auto
   2.756 +      obtain k where k: "j = Suc (2*k)"
   2.757 +        using \<open>odd j\<close> oddE by fastforce
   2.758 +      show ?thesis
   2.759 +      proof (cases "n > 0")
   2.760 +        case False
   2.761 +        then have "a (real j / 2^n) = u"
   2.762 +          by simp
   2.763 +        also have "... \<le> c (real i / 2^m)"
   2.764 +          using alec uabv by (blast intro: order_trans)
   2.765 +        finally have ac: "a (real j / 2^n) \<le> c (real i / 2^m)" .
   2.766 +        have "c (real i / 2^m) \<le> v"
   2.767 +          using cleb uabv by (blast intro: order_trans)
   2.768 +        also have "... = b (real j / 2^n)"
   2.769 +          using False by simp
   2.770 +        finally show ?thesis
   2.771 +          by (auto simp: ac)
   2.772 +      next
   2.773 +        case True show ?thesis
   2.774 +        proof (cases "real i / 2^m" "real j / 2^n" rule: linorder_cases)
   2.775 +          case less
   2.776 +          moreover have "real (4 * k + 1) / 2 ^ Suc n + 1 / (2 ^ Suc n) = real j / 2 ^ n"
   2.777 +            using k by (force simp: divide_simps)
   2.778 +          moreover have "\<bar>real i / 2 ^ m - real j / 2 ^ n\<bar> < 2 / (2 ^ Suc n)"
   2.779 +            using less.prems by simp
   2.780 +          ultimately have closer: "\<bar>real i / 2 ^ m - real (4 * k + 1) / 2 ^ Suc n\<bar> < 1 / (2 ^ Suc n)"
   2.781 +            using less.prems by linarith
   2.782 +          have *: "a (real (4 * k + 1) / 2 ^ Suc n) \<le> c (real i / 2 ^ m) \<and>
   2.783 +                   c (real i / 2 ^ m) \<le> b (real (4 * k + 1) / 2 ^ Suc n)"
   2.784 +            apply (rule less.IH [OF _ refl])
   2.785 +            using closer \<open>n < m\<close> \<open>d = m - n\<close> apply (auto simp: divide_simps  \<open>n < m\<close> diff_less_mono2)
   2.786 +            done
   2.787 +          show ?thesis
   2.788 +            using LR [of "c((2*k + 1) / 2^n)" "a((2*k + 1) / 2^n)" "b((2*k + 1) / 2^n)"]
   2.789 +            using alec [of "2*k+1"] cleb [of "2*k+1"] a_ge_0 [of "2*k+1"] b_le_1 [of "2*k+1"]
   2.790 +            using k a41 b41 * \<open>0 < n\<close>
   2.791 +            apply (simp add: add.commute)
   2.792 +            done
   2.793 +        next
   2.794 +          case equal then show ?thesis by simp
   2.795 +        next
   2.796 +          case greater
   2.797 +          moreover have "real (4 * k + 3) / 2 ^ Suc n - 1 / (2 ^ Suc n) = real j / 2 ^ n"
   2.798 +            using k by (force simp: divide_simps)
   2.799 +          moreover have "\<bar>real i / 2 ^ m - real j / 2 ^ n\<bar> < 2 * 1 / (2 ^ Suc n)"
   2.800 +            using less.prems by simp
   2.801 +          ultimately have closer: "\<bar>real i / 2 ^ m - real (4 * k + 3) / 2 ^ Suc n\<bar> < 1 / (2 ^ Suc n)"
   2.802 +            using less.prems by linarith
   2.803 +          have *: "a (real (4 * k + 3) / 2 ^ Suc n) \<le> c (real i / 2 ^ m) \<and>
   2.804 +                   c (real i / 2 ^ m) \<le> b (real (4 * k + 3) / 2 ^ Suc n)"
   2.805 +            apply (rule less.IH [OF _ refl])
   2.806 +            using closer \<open>n < m\<close> \<open>d = m - n\<close> apply (auto simp: divide_simps  \<open>n < m\<close> diff_less_mono2)
   2.807 +            done
   2.808 +          show ?thesis
   2.809 +            using LR [of "c((2*k + 1) / 2^n)" "a((2*k + 1) / 2^n)" "b((2*k + 1) / 2^n)"]
   2.810 +            using alec [of "2*k+1"] cleb [of "2*k+1"] a_ge_0 [of "2*k+1"] b_le_1 [of "2*k+1"]
   2.811 +            using k a43 b43 * \<open>0 < n\<close>
   2.812 +            apply (simp add: add.commute)
   2.813 +            done
   2.814 +        qed
   2.815 +      qed
   2.816 +    qed
   2.817 +  qed
   2.818 +  then have aj_le_ci: "a (real j / 2 ^ n) \<le> c (real i / 2 ^ m)"
   2.819 +    and ci_le_bj: "c (real i / 2 ^ m) \<le> b (real j / 2 ^ n)" if "odd j" "\<bar>real i / 2^m - real j / 2^n\<bar> < 1/2 ^ n" for i j m n
   2.820 +    using that by blast+
   2.821 +  have close_ab: "odd m \<Longrightarrow> \<bar>a (real m / 2 ^ n) - b (real m / 2 ^ n)\<bar> \<le> 2 / 2^n" for m n
   2.822 +  proof (induction n arbitrary: m)
   2.823 +    case 0
   2.824 +    with u01 v01 show ?case by auto
   2.825 +  next
   2.826 +    case (Suc n m)
   2.827 +    with oddE obtain k where k: "m = Suc (2*k)" by fastforce
   2.828 +    show ?case
   2.829 +    proof (cases "n > 0")
   2.830 +      case False
   2.831 +      with u01 v01 show ?thesis
   2.832 +        by (simp add: a_def b_def leftrec_base rightrec_base)
   2.833 +    next
   2.834 +      case True
   2.835 +      show ?thesis
   2.836 +      proof (cases "even k")
   2.837 +        case True
   2.838 +        then obtain j where j: "k = 2*j" by (metis evenE)
   2.839 +        have "\<bar>a ((2 * real j + 1) / 2 ^ n) - (b ((2 * real j + 1) / 2 ^ n))\<bar> \<le> 2/2 ^ n"
   2.840 +        proof -
   2.841 +          have "odd (Suc k)"
   2.842 +            using True by auto
   2.843 +          then show ?thesis
   2.844 +            by (metis (no_types) Groups.add_ac(2) Suc.IH j of_nat_Suc of_nat_mult of_nat_numeral)
   2.845 +        qed
   2.846 +        moreover have "a ((2 * real j + 1) / 2 ^ n) \<le>
   2.847 +                       leftcut (a ((2 * real j + 1) / 2 ^ n)) (b ((2 * real j + 1) / 2 ^ n)) (c ((2 * real j + 1) / 2 ^ n))"
   2.848 +          using alec [of "2*j+1"] cleb [of "2*j+1"] a_ge_0 [of "2*j+1"]  b_le_1 [of "2*j+1"]
   2.849 +          by (auto simp: add.commute left_right)
   2.850 +        moreover have "leftcut (a ((2 * real j + 1) / 2 ^ n)) (b ((2 * real j + 1) / 2 ^ n)) (c ((2 * real j + 1) / 2 ^ n)) \<le>
   2.851 +                         c ((2 * real j + 1) / 2 ^ n)"
   2.852 +          using alec [of "2*j+1"] cleb [of "2*j+1"] a_ge_0 [of "2*j+1"]  b_le_1 [of "2*j+1"]
   2.853 +          by (auto simp: add.commute left_right_m)
   2.854 +        ultimately have "\<bar>a ((2 * real j + 1) / 2 ^ n) -
   2.855 +                          leftcut (a ((2 * real j + 1) / 2 ^ n)) (b ((2 * real j + 1) / 2 ^ n)) (c ((2 * real j + 1) / 2 ^ n))\<bar>
   2.856 +                   \<le> 2/2 ^ Suc n"
   2.857 +          by (simp add: c_def midpoint_def)
   2.858 +        with j k \<open>n > 0\<close> show ?thesis
   2.859 +          by (simp add: add.commute [of 1] a41 b41 del: power_Suc)
   2.860 +      next
   2.861 +        case False
   2.862 +        then obtain j where j: "k = 2*j + 1" by (metis oddE)
   2.863 +        have "\<bar>a ((2 * real j + 1) / 2 ^ n) - (b ((2 * real j + 1) / 2 ^ n))\<bar> \<le> 2/2 ^ n"
   2.864 +          using Suc.IH [OF False] j by (auto simp: algebra_simps)
   2.865 +        moreover have "c ((2 * real j + 1) / 2 ^ n) \<le>
   2.866 +                       rightcut (a ((2 * real j + 1) / 2 ^ n)) (b ((2 * real j + 1) / 2 ^ n)) (c ((2 * real j + 1) / 2 ^ n))"
   2.867 +          using alec [of "2*j+1"] cleb [of "2*j+1"] a_ge_0 [of "2*j+1"]  b_le_1 [of "2*j+1"]
   2.868 +          by (auto simp: add.commute left_right_m)
   2.869 +        moreover have "rightcut (a ((2 * real j + 1) / 2 ^ n)) (b ((2 * real j + 1) / 2 ^ n)) (c ((2 * real j + 1) / 2 ^ n)) \<le>
   2.870 +                         b ((2 * real j + 1) / 2 ^ n)"
   2.871 +          using alec [of "2*j+1"] cleb [of "2*j+1"] a_ge_0 [of "2*j+1"]  b_le_1 [of "2*j+1"]
   2.872 +          by (auto simp: add.commute left_right)
   2.873 +        ultimately have "\<bar>rightcut (a ((2 * real j + 1) / 2 ^ n)) (b ((2 * real j + 1) / 2 ^ n)) (c ((2 * real j + 1) / 2 ^ n)) -
   2.874 +                          b ((2 * real j + 1) / 2 ^ n)\<bar>  \<le>  2/2 ^ Suc n"
   2.875 +          by (simp add: c_def midpoint_def)
   2.876 +        with j k \<open>n > 0\<close> show ?thesis
   2.877 +          by (simp add: add.commute [of 3] a43 b43 del: power_Suc)
   2.878 +      qed
   2.879 +    qed
   2.880 +  qed
   2.881 +  have m1_to_3: "4 * real k - 1 = real (4 * (k-1)) + 3" if "0 < k" for k
   2.882 +    using that by auto
   2.883 +  have fb_eq_fa: "\<lbrakk>0 < j; 2*j < 2 ^ n\<rbrakk> \<Longrightarrow> f(b((2 * real j - 1) / 2^n)) = f(a((2 * real j + 1) / 2^n))" for n j
   2.884 +  proof (induction n arbitrary: j)
   2.885 +    case 0
   2.886 +    then show ?case by auto
   2.887 +  next
   2.888 +    case (Suc n j) show ?case
   2.889 +    proof (cases "n > 0")
   2.890 +      case False
   2.891 +      with Suc.prems show ?thesis by auto
   2.892 +    next
   2.893 +      case True
   2.894 +      show ?thesis proof (cases "even j")
   2.895 +        case True
   2.896 +        then obtain k where k: "j = 2*k" by (metis evenE)
   2.897 +        with \<open>0 < j\<close> have "k > 0" "2 * k < 2 ^ n"
   2.898 +          using Suc.prems(2) k by auto
   2.899 +        with k \<open>0 < n\<close> Suc.IH [of k] show ?thesis
   2.900 +          apply (simp add: m1_to_3 a41 b43 del: power_Suc)
   2.901 +          apply (subst of_nat_diff, auto)
   2.902 +          done
   2.903 +      next
   2.904 +        case False
   2.905 +        then obtain k where k: "j = 2*k + 1" by (metis oddE)
   2.906 +        have "f (leftcut (a ((2 * k + 1) / 2^n)) (b ((2 * k + 1) / 2^n)) (c ((2 * k + 1) / 2^n)))
   2.907 +              = f (c ((2 * k + 1) / 2^n))"
   2.908 +          "f (c ((2 * k + 1) / 2^n))
   2.909 +              = f (rightcut (a ((2 * k + 1) / 2^n)) (b ((2 * k + 1) / 2^n)) (c ((2 * k + 1) / 2^n)))"
   2.910 +          using alec [of "2*k+1" n] cleb [of "2*k+1" n] a_ge_0 [of "2*k+1" n]  b_le_1 [of "2*k+1" n] k
   2.911 +          using left_right_m [of "c((2*k + 1) / 2^n)" "a((2*k + 1) / 2^n)" "b((2*k + 1) / 2^n)"]
   2.912 +           apply (auto simp: add.commute  feqm [OF order_refl]  feqm [OF _ order_refl, symmetric])
   2.913 +          done
   2.914 +        then
   2.915 +        show ?thesis
   2.916 +          by (simp add: k add.commute [of 1] add.commute [of 3] a43 b41\<open>0 < n\<close> del: power_Suc)
   2.917 +      qed
   2.918 +    qed
   2.919 +  qed
   2.920 +  have f_eq_fc: "\<lbrakk>0 < j; j < 2 ^ n\<rbrakk>
   2.921 +                 \<Longrightarrow> f(b((2*j - 1) / 2 ^ (Suc n))) = f(c(j / 2^n)) \<and>
   2.922 +                     f(a((2*j + 1) / 2 ^ (Suc n))) = f(c(j / 2^n))" for n and j::nat
   2.923 +  proof (induction n arbitrary: j)
   2.924 +    case 0
   2.925 +    then show ?case by auto
   2.926 +  next
   2.927 +    case (Suc n)
   2.928 +    show ?case
   2.929 +    proof (cases "even j")
   2.930 +      case True
   2.931 +      then obtain k where k: "j = 2*k" by (metis evenE)
   2.932 +      then have less2n: "k < 2 ^ n"
   2.933 +        using Suc.prems(2) by auto
   2.934 +      have "0 < k" using \<open>0 < j\<close> k by linarith
   2.935 +      then have m1_to_3: "real (4 * k - Suc 0) = real (4 * (k-1)) + 3"
   2.936 +        by auto
   2.937 +      then show ?thesis
   2.938 +        using Suc.IH [of k] k \<open>0 < k\<close>
   2.939 +        apply (simp add: less2n add.commute [of 1] m1_to_3 a41 b43 del: power_Suc)
   2.940 +        apply (auto simp: of_nat_diff)
   2.941 +        done
   2.942 +    next
   2.943 +      case False
   2.944 +      then obtain k where k: "j = 2*k + 1" by (metis oddE)
   2.945 +      with Suc.prems have "k < 2^n" by auto
   2.946 +      show ?thesis
   2.947 +        using alec [of "2*k+1" "Suc n"] cleb [of "2*k+1" "Suc n"] a_ge_0 [of "2*k+1" "Suc n"]  b_le_1 [of "2*k+1" "Suc n"] k
   2.948 +        using left_right_m [of "c((2*k + 1) / 2 ^ Suc n)" "a((2*k + 1) / 2 ^ Suc n)" "b((2*k + 1) / 2 ^ Suc n)"]
   2.949 +        apply (simp add: add.commute [of 1] add.commute [of 3] m1_to_3 b41 a43 del: power_Suc)
   2.950 +        apply (force intro: feqm)
   2.951 +        done
   2.952 +    qed
   2.953 +  qed
   2.954 +  define D01 where "D01 \<equiv> {0<..<1} \<inter> (\<Union>k m. {real m / 2^k})"
   2.955 +  have cloD01 [simp]: "closure D01 = {0..1}"
   2.956 +    unfolding D01_def
   2.957 +    by (subst closure_dyadic_rationals_in_convex_set_pos_1) auto
   2.958 +  have "uniformly_continuous_on D01 (f \<circ> c)"
   2.959 +  proof (clarsimp simp: uniformly_continuous_on_def)
   2.960 +    fix e::real
   2.961 +    assume "0 < e"
   2.962 +    have ucontf: "uniformly_continuous_on {0..1} f"
   2.963 +      by (simp add: compact_uniformly_continuous [OF cont_f])
   2.964 +    then obtain d where "0 < d" and d: "\<And>x x'. \<lbrakk>x \<in> {0..1}; x' \<in> {0..1}; norm (x' - x) < d\<rbrakk> \<Longrightarrow> norm (f x' - f x) < e/2"
   2.965 +      unfolding uniformly_continuous_on_def dist_norm
   2.966 +      by (metis \<open>0 < e\<close> less_divide_eq_numeral1(1) mult_zero_left)
   2.967 +    obtain n where n: "1/2^n < min d 1"
   2.968 +      by (metis \<open>0 < d\<close> divide_less_eq_1 less_numeral_extra(1) min_def one_less_numeral_iff power_one_over real_arch_pow_inv semiring_norm(76) zero_less_numeral)
   2.969 +    with gr0I have "n > 0"
   2.970 +      by (force simp: divide_simps)
   2.971 +    show "\<exists>d>0. \<forall>x\<in>D01. \<forall>x'\<in>D01. dist x' x < d \<longrightarrow> dist (f (c x')) (f (c x)) < e"
   2.972 +    proof (intro exI ballI impI conjI)
   2.973 +      show "(0::real) < 1/2^n" by auto
   2.974 +    next
   2.975 +      have dist_fc_close: "dist (f(c(real i / 2^m))) (f(c(real j / 2^n))) < e/2"
   2.976 +        if i: "0 < i" "i < 2 ^ m" and j: "0 < j" "j < 2 ^ n" and clo: "abs(i / 2^m - j / 2^n) < 1/2 ^ n" for i j m
   2.977 +      proof -
   2.978 +        have abs3: "\<bar>x - a\<bar> < e \<Longrightarrow> x = a \<or> \<bar>x - (a - e/2)\<bar> < e/2 \<or> \<bar>x - (a + e/2)\<bar> < e/2" for x a e::real
   2.979 +          by linarith
   2.980 +        consider "i / 2 ^ m = j / 2 ^ n"
   2.981 +          | "\<bar>i / 2 ^ m - (2 * j - 1) / 2 ^ Suc n\<bar> < 1/2 ^ Suc n"
   2.982 +          | "\<bar>i / 2 ^ m - (2 * j + 1) / 2 ^ Suc n\<bar> < 1/2 ^ Suc n"
   2.983 +          using abs3 [OF clo] j by (auto simp: field_simps of_nat_diff)
   2.984 +        then show ?thesis
   2.985 +        proof cases
   2.986 +          case 1 with \<open>0 < e\<close> show ?thesis by auto
   2.987 +        next
   2.988 +          case 2
   2.989 +          have *: "abs(a - b) \<le> 1/2 ^ n \<and> 1/2 ^ n < d \<and> a \<le> c \<and> c \<le> b \<Longrightarrow> b - c < d" for a b c
   2.990 +            by auto
   2.991 +          have "norm (c (real i / 2 ^ m) - b (real (2 * j - 1) / 2 ^ Suc n)) < d"
   2.992 +            using 2 j n close_ab [of "2*j-1" "Suc n"]
   2.993 +            using b_ge_0 [of "2*j-1" "Suc n"] b_le_1 [of "2*j-1" "Suc n"]
   2.994 +            using aj_le_ci [of "2*j-1" i m "Suc n"]
   2.995 +            using ci_le_bj [of "2*j-1" i m "Suc n"]
   2.996 +            apply (simp add: divide_simps of_nat_diff del: power_Suc)
   2.997 +            apply (auto simp: divide_simps intro!: *)
   2.998 +            done
   2.999 +          moreover have "f(c(j / 2^n)) = f(b ((2*j - 1) / 2 ^ (Suc n)))"
  2.1000 +            using f_eq_fc [OF j] by metis
  2.1001 +          ultimately show ?thesis
  2.1002 +            by (metis dist_norm atLeastAtMost_iff b_ge_0 b_le_1 c_ge_0 c_le_1 d)
  2.1003 +        next
  2.1004 +          case 3
  2.1005 +          have *: "abs(a - b) \<le> 1/2 ^ n \<and> 1/2 ^ n < d \<and> a \<le> c \<and> c \<le> b \<Longrightarrow> c - a < d" for a b c
  2.1006 +            by auto
  2.1007 +          have "norm (c (real i / 2 ^ m) - a (real (2 * j + 1) / 2 ^ Suc n)) < d"
  2.1008 +            using 3 j n close_ab [of "2*j+1" "Suc n"]
  2.1009 +            using b_ge_0 [of "2*j+1" "Suc n"] b_le_1 [of "2*j+1" "Suc n"]
  2.1010 +            using aj_le_ci [of "2*j+1" i m "Suc n"]
  2.1011 +            using ci_le_bj [of "2*j+1" i m "Suc n"]
  2.1012 +            apply (simp add: divide_simps of_nat_diff del: power_Suc)
  2.1013 +            apply (auto simp: divide_simps intro!: *)
  2.1014 +            done
  2.1015 +          moreover have "f(c(j / 2^n)) = f(a ((2*j + 1) / 2 ^ (Suc n)))"
  2.1016 +            using f_eq_fc [OF j] by metis
  2.1017 +          ultimately show ?thesis
  2.1018 +            by (metis dist_norm a_ge_0 atLeastAtMost_iff a_ge_0 a_le_1 c_ge_0 c_le_1 d)
  2.1019 +        qed
  2.1020 +      qed
  2.1021 +      show "dist (f (c x')) (f (c x)) < e"
  2.1022 +        if "x \<in> D01" "x' \<in> D01" "dist x' x < 1/2^n" for x x'
  2.1023 +        using that unfolding D01_def dyadics_in_open_unit_interval
  2.1024 +      proof clarsimp
  2.1025 +        fix i k::nat and m p
  2.1026 +        assume i: "0 < i" "i < 2 ^ m" and k: "0<k" "k < 2 ^ p"
  2.1027 +        assume clo: "dist (real k / 2 ^ p) (real i / 2 ^ m) < 1/2 ^ n"
  2.1028 +        obtain j::nat where "0 < j" "j < 2 ^ n"
  2.1029 +          and clo_ij: "abs(i / 2^m - j / 2^n) < 1/2 ^ n"
  2.1030 +          and clo_kj: "abs(k / 2^p - j / 2^n) < 1/2 ^ n"
  2.1031 +        proof -
  2.1032 +          have "max (2^n * i / 2^m) (2^n * k / 2^p) \<ge> 0"
  2.1033 +            by (auto simp: le_max_iff_disj)
  2.1034 +          then obtain j where "floor (max (2^n*i / 2^m) (2^n*k / 2^p)) = int j"
  2.1035 +            using zero_le_floor zero_le_imp_eq_int by blast
  2.1036 +          then have j_le: "real j \<le> max (2^n * i / 2^m) (2^n * k / 2^p)"
  2.1037 +            and less_j1: "max (2^n * i / 2^m) (2^n * k / 2^p) < real j + 1"
  2.1038 +            using floor_correct [of "max (2^n * i / 2^m) (2^n * k / 2^p)"] by linarith+
  2.1039 +          show thesis
  2.1040 +          proof (cases "j = 0")
  2.1041 +            case True
  2.1042 +            show thesis
  2.1043 +            proof
  2.1044 +              show "(1::nat) < 2 ^ n"
  2.1045 +                apply (subst one_less_power)
  2.1046 +                using \<open>n > 0\<close> by auto
  2.1047 +              show "\<bar>real i / 2 ^ m - real 1/2 ^ n\<bar> < 1/2 ^ n"
  2.1048 +                using i less_j1 by (simp add: dist_norm field_simps True)
  2.1049 +              show "\<bar>real k / 2 ^ p - real 1/2 ^ n\<bar> < 1/2 ^ n"
  2.1050 +                using k less_j1 by (simp add: dist_norm field_simps True)
  2.1051 +            qed simp
  2.1052 +          next
  2.1053 +            case False
  2.1054 +            have 1: "real j * 2 ^ m < real i * 2 ^ n"
  2.1055 +              if j: "real j * 2 ^ p \<le> real k * 2 ^ n" and k: "real k * 2 ^ m < real i * 2 ^ p"
  2.1056 +              for i k m p
  2.1057 +            proof -
  2.1058 +              have "real j * 2 ^ p * 2 ^ m \<le> real k * 2 ^ n * 2 ^ m"
  2.1059 +                using j by simp
  2.1060 +              moreover have "real k * 2 ^ m * 2 ^ n < real i * 2 ^ p * 2 ^ n"
  2.1061 +                using k by simp
  2.1062 +              ultimately have "real j * 2 ^ p * 2 ^ m < real i * 2 ^ p * 2 ^ n"
  2.1063 +                by (simp only: mult_ac)
  2.1064 +              then show ?thesis
  2.1065 +                by simp
  2.1066 +            qed
  2.1067 +            have 2: "real j * 2 ^ m < 2 ^ m + real i * 2 ^ n"
  2.1068 +              if j: "real j * 2 ^ p \<le> real k * 2 ^ n" and k: "real k * (2 ^ m * 2 ^ n) < 2 ^ m * 2 ^ p + real i * (2 ^ n * 2 ^ p)"
  2.1069 +              for i k m p
  2.1070 +            proof -
  2.1071 +              have "real j * 2 ^ p * 2 ^ m \<le> real k * (2 ^ m * 2 ^ n)"
  2.1072 +                using j by simp
  2.1073 +              also have "... < 2 ^ m * 2 ^ p + real i * (2 ^ n * 2 ^ p)"
  2.1074 +                by (rule k)
  2.1075 +              finally have "(real j * 2 ^ m) * 2 ^ p < (2 ^ m + real i * 2 ^ n) * 2 ^ p"
  2.1076 +                by (simp add: algebra_simps)
  2.1077 +              then show ?thesis
  2.1078 +                by simp
  2.1079 +            qed
  2.1080 +            have 3: "real j * 2 ^ p < 2 ^ p + real k * 2 ^ n"
  2.1081 +              if j: "real j * 2 ^ m \<le> real i * 2 ^ n" and i: "real i * 2 ^ p \<le> real k * 2 ^ m"
  2.1082 +            proof -
  2.1083 +              have "real j * 2 ^ m * 2 ^ p \<le> real i * 2 ^ n * 2 ^ p"
  2.1084 +                using j by simp
  2.1085 +              moreover have "real i * 2 ^ p * 2 ^ n \<le> real k * 2 ^ m * 2 ^ n"
  2.1086 +                using i by simp
  2.1087 +              ultimately have "real j * 2 ^ m * 2 ^ p \<le> real k * 2 ^ m * 2 ^ n"
  2.1088 +                by (simp only: mult_ac)
  2.1089 +              then have "real j * 2 ^ p \<le> real k * 2 ^ n"
  2.1090 +                by simp
  2.1091 +              also have "... < 2 ^ p + real k * 2 ^ n"
  2.1092 +                by auto
  2.1093 +              finally show ?thesis by simp
  2.1094 +            qed
  2.1095 +            show ?thesis
  2.1096 +            proof
  2.1097 +              have "real j < 2 ^ n"
  2.1098 +                using j_le i k
  2.1099 +                apply (auto simp: le_max_iff_disj simp del: real_of_nat_less_numeral_power_cancel_iff elim!: le_less_trans)
  2.1100 +                 apply (auto simp: field_simps)
  2.1101 +                done
  2.1102 +              then show "j < 2 ^ n"
  2.1103 +                by auto
  2.1104 +              show "\<bar>real i / 2 ^ m - real j / 2 ^ n\<bar> < 1/2 ^ n"
  2.1105 +                using clo less_j1 j_le
  2.1106 +                apply (auto simp: le_max_iff_disj divide_simps dist_norm)
  2.1107 +                 apply (auto simp: algebra_simps abs_if split: if_split_asm dest: 1 2)
  2.1108 +                done
  2.1109 +              show "\<bar>real k / 2 ^ p - real j / 2 ^ n\<bar> < 1/2 ^ n"
  2.1110 +                using  clo less_j1 j_le
  2.1111 +                apply (auto simp: le_max_iff_disj divide_simps dist_norm)
  2.1112 +                 apply (auto simp: algebra_simps not_less abs_if split: if_split_asm dest: 3 2)
  2.1113 +                done
  2.1114 +            qed (use False in simp)
  2.1115 +          qed
  2.1116 +        qed
  2.1117 +        show "dist (f (c (real k / 2 ^ p))) (f (c (real i / 2 ^ m))) < e"
  2.1118 +        proof (rule dist_triangle_half_l)
  2.1119 +          show "dist (f (c (real k / 2 ^ p))) (f(c(j / 2^n))) < e/2"
  2.1120 +            apply (rule dist_fc_close)
  2.1121 +            using \<open>0 < j\<close> \<open>j < 2 ^ n\<close> k clo_kj by auto
  2.1122 +          show "dist (f (c (real i / 2 ^ m))) (f (c (real j / 2 ^ n))) < e/2"
  2.1123 +            apply (rule dist_fc_close)
  2.1124 +            using \<open>0 < j\<close> \<open>j < 2 ^ n\<close> i clo_ij by auto
  2.1125 +        qed
  2.1126 +      qed
  2.1127 +    qed
  2.1128 +  qed
  2.1129 +  then obtain h where ucont_h: "uniformly_continuous_on {0..1} h"
  2.1130 +    and fc_eq: "\<And>x. x \<in> D01 \<Longrightarrow> (f \<circ> c) x = h x"
  2.1131 +  proof (rule uniformly_continuous_on_extension_on_closure [of D01 "f \<circ> c"])
  2.1132 +  qed (use closure_subset [of D01] in \<open>auto intro!: that\<close>)
  2.1133 +  then have cont_h: "continuous_on {0..1} h"
  2.1134 +    using uniformly_continuous_imp_continuous by blast
  2.1135 +  have h_eq: "h (real k / 2 ^ m) = f (c (real k / 2 ^ m))" if "0 < k" "k < 2^m" for k m
  2.1136 +    using fc_eq that by (force simp: D01_def)
  2.1137 +  have "h ` {0..1} = f ` {0..1}"
  2.1138 +  proof
  2.1139 +    have "h ` (closure D01) \<subseteq> f ` {0..1}"
  2.1140 +    proof (rule image_closure_subset)
  2.1141 +      show "continuous_on (closure D01) h"
  2.1142 +        using cont_h by simp
  2.1143 +      show "closed (f ` {0..1})"
  2.1144 +        using compact_continuous_image [OF cont_f] compact_imp_closed by blast
  2.1145 +      show "h ` D01 \<subseteq> f ` {0..1}"
  2.1146 +        by (force simp: dyadics_in_open_unit_interval D01_def h_eq)
  2.1147 +    qed
  2.1148 +    with cloD01 show "h ` {0..1} \<subseteq> f ` {0..1}" by simp
  2.1149 +    have a12 [simp]: "a (1/2) = u"
  2.1150 +      by (metis a_def leftrec_base numeral_One of_nat_numeral)
  2.1151 +    have b12 [simp]: "b (1/2) = v"
  2.1152 +      by (metis b_def rightrec_base numeral_One of_nat_numeral)
  2.1153 +    have "f ` {0..1} \<subseteq> closure(h ` D01)"
  2.1154 +    proof (clarsimp simp: closure_approachable dyadics_in_open_unit_interval D01_def)
  2.1155 +      fix x e::real
  2.1156 +      assume "0 \<le> x" "x \<le> 1" "0 < e"
  2.1157 +      have ucont_f: "uniformly_continuous_on {0..1} f"
  2.1158 +        using compact_uniformly_continuous cont_f by blast
  2.1159 +      then obtain \<delta> where "\<delta> > 0"
  2.1160 +        and \<delta>: "\<And>x x'. \<lbrakk>x \<in> {0..1}; x' \<in> {0..1}; dist x' x < \<delta>\<rbrakk> \<Longrightarrow> norm (f x' - f x) < e"
  2.1161 +        using \<open>0 < e\<close> by (auto simp: uniformly_continuous_on_def dist_norm)
  2.1162 +      have *: "\<exists>m::nat. \<exists>y. odd m \<and> 0 < m \<and> m < 2 ^ n \<and> y \<in> {a(m / 2^n) .. b(m / 2^n)} \<and> f y = f x"
  2.1163 +        if "n \<noteq> 0" for n
  2.1164 +        using that
  2.1165 +      proof (induction n)
  2.1166 +        case 0 then show ?case by auto
  2.1167 +      next
  2.1168 +        case (Suc n)
  2.1169 +        show ?case
  2.1170 +        proof (cases "n=0")
  2.1171 +          case True
  2.1172 +          consider "x \<in> {0..u}" | "x \<in> {u..v}" | "x \<in> {v..1}"
  2.1173 +            using \<open>0 \<le> x\<close> \<open>x \<le> 1\<close> by force
  2.1174 +          then have "\<exists>y\<ge>a (real 1/2). y \<le> b (real 1/2) \<and> f y = f x"
  2.1175 +          proof cases
  2.1176 +            case 1
  2.1177 +            then show ?thesis
  2.1178 +              apply (rule_tac x=u in exI)
  2.1179 +              using uabv [of 1 1] f0u [of u] f0u [of x] by auto
  2.1180 +          next
  2.1181 +            case 2
  2.1182 +            then show ?thesis
  2.1183 +              by (rule_tac x=x in exI) auto
  2.1184 +          next
  2.1185 +            case 3
  2.1186 +            then show ?thesis
  2.1187 +              apply (rule_tac x=v in exI)
  2.1188 +              using uabv [of 1 1] fv1 [of v] fv1 [of x] by auto
  2.1189 +          qed
  2.1190 +          with \<open>n=0\<close> show ?thesis
  2.1191 +            by (rule_tac x=1 in exI) auto
  2.1192 +        next
  2.1193 +          case False
  2.1194 +          with Suc obtain m y
  2.1195 +            where "odd m" "0 < m" and mless: "m < 2 ^ n"
  2.1196 +              and y: "y \<in> {a (real m / 2 ^ n)..b (real m / 2 ^ n)}" and feq: "f y = f x"
  2.1197 +            by metis
  2.1198 +          then obtain j where j: "m = 2*j + 1" by (metis oddE)
  2.1199 +          consider "y \<in> {a((2*j + 1) / 2^n) .. b((4*j + 1) / 2 ^ (Suc n))}"
  2.1200 +            | "y \<in> {b((4*j + 1) / 2 ^ (Suc n)) .. a((4*j + 3) / 2 ^ (Suc n))}"
  2.1201 +            | "y \<in> {a((4*j + 3) / 2 ^ (Suc n)) .. b((2*j + 1) / 2^n)}"
  2.1202 +            using y j by force
  2.1203 +          then show ?thesis
  2.1204 +          proof cases
  2.1205 +            case 1
  2.1206 +            then show ?thesis
  2.1207 +              apply (rule_tac x="4*j + 1" in exI)
  2.1208 +              apply (rule_tac x=y in exI)
  2.1209 +              using mless j \<open>n \<noteq> 0\<close>
  2.1210 +              apply (simp add: feq a41 b41 add.commute [of 1] del: power_Suc)
  2.1211 +              apply (simp add: algebra_simps)
  2.1212 +              done
  2.1213 +          next
  2.1214 +            case 2
  2.1215 +            show ?thesis
  2.1216 +              apply (rule_tac x="4*j + 1" in exI)
  2.1217 +              apply (rule_tac x="b((4*j + 1) / 2 ^ (Suc n))" in exI)
  2.1218 +              using mless \<open>n \<noteq> 0\<close> 2 j
  2.1219 +              using alec [of "2*j+1" n] cleb [of "2*j+1" n] a_ge_0 [of "2*j+1" n]  b_le_1 [of "2*j+1" n]
  2.1220 +              using left_right [of "c((2*j + 1) / 2^n)" "a((2*j + 1) / 2^n)" "b((2*j + 1) / 2^n)"]
  2.1221 +              apply (simp add: a41 b41 a43 b43 add.commute [of 1] add.commute [of 3] del: power_Suc)
  2.1222 +              apply (auto simp: feq [symmetric] intro: f_eqI)
  2.1223 +              done
  2.1224 +          next
  2.1225 +            case 3
  2.1226 +            then show ?thesis
  2.1227 +              apply (rule_tac x="4*j + 3" in exI)
  2.1228 +              apply (rule_tac x=y in exI)
  2.1229 +              using mless j \<open>n \<noteq> 0\<close>
  2.1230 +              apply (simp add: feq a43 b43 del: power_Suc)
  2.1231 +              apply (simp add: algebra_simps)
  2.1232 +              done
  2.1233 +          qed
  2.1234 +        qed
  2.1235 +      qed
  2.1236 +      obtain n where n: "1/2^n < min (\<delta> / 2) 1"
  2.1237 +        by (metis \<open>0 < \<delta>\<close> divide_less_eq_1 less_numeral_extra(1) min_less_iff_conj one_less_numeral_iff power_one_over real_arch_pow_inv semiring_norm(76) zero_less_divide_iff zero_less_numeral)
  2.1238 +      with gr0I have "n \<noteq> 0"
  2.1239 +        by fastforce
  2.1240 +      with * obtain m::nat and y
  2.1241 +        where "odd m" "0 < m" and mless: "m < 2 ^ n"
  2.1242 +          and y: "y \<in> {a(m / 2^n) .. b(m / 2^n)}" and feq: "f x = f y"
  2.1243 +        by metis
  2.1244 +      then have "0 \<le> y" "y \<le> 1"
  2.1245 +        by (metis atLeastAtMost_iff a_ge_0 b_le_1 order.trans)+
  2.1246 +      moreover have "y < \<delta> + c (real m / 2 ^ n)" "c (real m / 2 ^ n) < \<delta> + y"
  2.1247 +        using y apply simp_all
  2.1248 +        using alec [of m n] cleb [of m n] n real_sum_of_halves close_ab [OF \<open>odd m\<close>, of n]
  2.1249 +        by linarith+
  2.1250 +      moreover note \<open>0 < m\<close> mless \<open>0 \<le> x\<close> \<open>x \<le> 1\<close>
  2.1251 +      ultimately show "\<exists>k. \<exists>m\<in>{0<..<2 ^ k}. dist (h (real m / 2 ^ k)) (f x) < e"
  2.1252 +        apply (rule_tac x=n in exI)
  2.1253 +        apply (rule_tac x=m in bexI)
  2.1254 +         apply (auto simp: dist_norm h_eq feq \<delta>)
  2.1255 +        done
  2.1256 +    qed
  2.1257 +    also have "... \<subseteq> h ` {0..1}"
  2.1258 +      apply (rule closure_minimal)
  2.1259 +      using compact_continuous_image [OF cont_h] compact_imp_closed by (auto simp: D01_def)
  2.1260 +    finally show "f ` {0..1} \<subseteq> h ` {0..1}" .
  2.1261 +  qed
  2.1262 +  moreover have "inj_on h {0..1}"
  2.1263 +  proof -
  2.1264 +    have "u < v"
  2.1265 +      by (metis atLeastAtMost_iff f0u f_1not0 fv1 order.not_eq_order_implies_strict u01(1) u01(2) v01(1))
  2.1266 +    have f_not_fu: "\<And>x. \<lbrakk>u < x; x \<le> v\<rbrakk> \<Longrightarrow> f x \<noteq> f u"
  2.1267 +      by (metis atLeastAtMost_iff f0u fu1 greaterThanAtMost_iff order_refl order_trans u01(1) v01(2))
  2.1268 +    have f_not_fv: "\<And>x. \<lbrakk>u \<le> x; x < v\<rbrakk> \<Longrightarrow> f x \<noteq> f v"
  2.1269 +      by (metis atLeastAtMost_iff order_refl order_trans v01(2) atLeastLessThan_iff fuv fv1)
  2.1270 +    have a_less_b:
  2.1271 +         "a(j / 2^n) < b(j / 2^n) \<and>
  2.1272 +          (\<forall>x. a(j / 2^n) < x \<longrightarrow> x \<le> b(j / 2^n) \<longrightarrow> f x \<noteq> f(a(j / 2^n))) \<and>
  2.1273 +          (\<forall>x. a(j / 2^n) \<le> x \<longrightarrow> x < b(j / 2^n) \<longrightarrow> f x \<noteq> f(b(j / 2^n)))" for n and j::nat
  2.1274 +    proof (induction n arbitrary: j)
  2.1275 +      case 0 then show ?case
  2.1276 +        by (simp add: \<open>u < v\<close> f_not_fu f_not_fv)
  2.1277 +    next
  2.1278 +      case (Suc n j) show ?case
  2.1279 +      proof (cases "n > 0")
  2.1280 +        case False then show ?thesis
  2.1281 +          by (auto simp: a_def b_def leftrec_base rightrec_base \<open>u < v\<close> f_not_fu f_not_fv)
  2.1282 +      next
  2.1283 +        case True show ?thesis
  2.1284 +        proof (cases "even j")
  2.1285 +          case True
  2.1286 +          with \<open>0 < n\<close> Suc.IH show ?thesis
  2.1287 +            by (auto elim!: evenE)
  2.1288 +        next
  2.1289 +          case False
  2.1290 +          then obtain k where k: "j = 2*k + 1" by (metis oddE)
  2.1291 +          then show ?thesis
  2.1292 +          proof (cases "even k")
  2.1293 +            case True
  2.1294 +            then obtain m where m: "k = 2*m" by (metis evenE)
  2.1295 +            have fleft: "f (leftcut (a ((2*m + 1) / 2^n)) (b ((2*m + 1) / 2^n)) (c ((2*m + 1) / 2^n))) =
  2.1296 +                         f (c((2*m + 1) / 2^n))"
  2.1297 +              using alec [of "2*m+1" n] cleb [of "2*m+1" n] a_ge_0 [of "2*m+1" n]  b_le_1 [of "2*m+1" n]
  2.1298 +              using left_right_m [of "c((2*m + 1) / 2^n)" "a((2*m + 1) / 2^n)" "b((2*m + 1) / 2^n)"]
  2.1299 +              by (auto intro: f_eqI)
  2.1300 +            show ?thesis
  2.1301 +            proof (intro conjI impI notI allI)
  2.1302 +              have False if "b (real j / 2 ^ Suc n) \<le> a (real j / 2 ^ Suc n)"
  2.1303 +              proof -
  2.1304 +                have "f (c ((1 + real m * 2) / 2 ^ n)) = f (a ((1 + real m * 2) / 2 ^ n))"
  2.1305 +                  using k m \<open>0 < n\<close> fleft that a41 [of n m] b41 [of n m]
  2.1306 +                  using alec [of "2*m+1" n] cleb [of "2*m+1" n] a_ge_0 [of "2*m+1" n]  b_le_1 [of "2*m+1" n]
  2.1307 +                  using left_right [of "c((2*m + 1) / 2^n)" "a((2*m + 1) / 2^n)" "b((2*m + 1) / 2^n)"]
  2.1308 +                  by (auto simp: algebra_simps)
  2.1309 +                moreover have "a (real (1 + m * 2) / 2 ^ n) < c (real (1 + m * 2) / 2 ^ n)"
  2.1310 +                  using Suc.IH [of "1 + m * 2"] by (simp add: c_def midpoint_def)
  2.1311 +                moreover have "c (real (1 + m * 2) / 2 ^ n) \<le> b (real (1 + m * 2) / 2 ^ n)"
  2.1312 +                  using cleb by blast
  2.1313 +                ultimately show ?thesis
  2.1314 +                  using Suc.IH [of "1 + m * 2"] by force
  2.1315 +              qed
  2.1316 +              then show "a (real j / 2 ^ Suc n) < b (real j / 2 ^ Suc n)" by force
  2.1317 +            next
  2.1318 +              fix x
  2.1319 +              assume "a (real j / 2 ^ Suc n) < x" "x \<le> b (real j / 2 ^ Suc n)" "f x = f (a (real j / 2 ^ Suc n))"
  2.1320 +              then show False
  2.1321 +                using Suc.IH [of "1 + m * 2", THEN conjunct2, THEN conjunct1]
  2.1322 +                using k m \<open>0 < n\<close> a41 [of n m] b41 [of n m]
  2.1323 +                using alec [of "2*m+1" n] cleb [of "2*m+1" n] a_ge_0 [of "2*m+1" n] b_le_1 [of "2*m+1" n]
  2.1324 +                using left_right_m [of "c((2*m + 1) / 2^n)" "a((2*m + 1) / 2^n)" "b((2*m + 1) / 2^n)"]
  2.1325 +                by (auto simp: algebra_simps)
  2.1326 +            next
  2.1327 +              fix x
  2.1328 +              assume "a (real j / 2 ^ Suc n) \<le> x" "x < b (real j / 2 ^ Suc n)" "f x = f (b (real j / 2 ^ Suc n))"
  2.1329 +              then show False
  2.1330 +                using k m \<open>0 < n\<close> a41 [of n m] b41 [of n m] fleft left_neq
  2.1331 +                using alec [of "2*m+1" n] cleb [of "2*m+1" n] a_ge_0 [of "2*m+1" n] b_le_1 [of "2*m+1" n]
  2.1332 +                by (auto simp: algebra_simps)
  2.1333 +            qed
  2.1334 +          next
  2.1335 +            case False
  2.1336 +            with oddE obtain m where m: "k = Suc (2*m)" by fastforce
  2.1337 +            have fright: "f (rightcut (a ((2*m + 1) / 2^n)) (b ((2*m + 1) / 2^n)) (c ((2*m + 1) / 2^n))) = f (c((2*m + 1) / 2^n))"
  2.1338 +              using alec [of "2*m+1" n] cleb [of "2*m+1" n] a_ge_0 [of "2*m+1" n]  b_le_1 [of "2*m+1" n]
  2.1339 +              using left_right_m [of "c((2*m + 1) / 2^n)" "a((2*m + 1) / 2^n)" "b((2*m + 1) / 2^n)"]
  2.1340 +              by (auto intro: f_eqI [OF _ order_refl])
  2.1341 +            show ?thesis
  2.1342 +            proof (intro conjI impI notI allI)
  2.1343 +              have False if "b (real j / 2 ^ Suc n) \<le> a (real j / 2 ^ Suc n)"
  2.1344 +              proof -
  2.1345 +                have "f (c ((1 + real m * 2) / 2 ^ n)) = f (b ((1 + real m * 2) / 2 ^ n))"
  2.1346 +                  using k m \<open>0 < n\<close> fright that a43 [of n m] b43 [of n m]
  2.1347 +                  using alec [of "2*m+1" n] cleb [of "2*m+1" n] a_ge_0 [of "2*m+1" n]  b_le_1 [of "2*m+1" n]
  2.1348 +                  using left_right [of "c((2*m + 1) / 2^n)" "a((2*m + 1) / 2^n)" "b((2*m + 1) / 2^n)"]
  2.1349 +                  by (auto simp: algebra_simps)
  2.1350 +                moreover have "a (real (1 + m * 2) / 2 ^ n) \<le> c (real (1 + m * 2) / 2 ^ n)"
  2.1351 +                  using alec by blast
  2.1352 +                moreover have "c (real (1 + m * 2) / 2 ^ n) < b (real (1 + m * 2) / 2 ^ n)"
  2.1353 +                  using Suc.IH [of "1 + m * 2"] by (simp add: c_def midpoint_def)
  2.1354 +                ultimately show ?thesis
  2.1355 +                  using Suc.IH [of "1 + m * 2"] by force
  2.1356 +              qed
  2.1357 +              then show "a (real j / 2 ^ Suc n) < b (real j / 2 ^ Suc n)" by force
  2.1358 +            next
  2.1359 +              fix x
  2.1360 +              assume "a (real j / 2 ^ Suc n) < x" "x \<le> b (real j / 2 ^ Suc n)" "f x = f (a (real j / 2 ^ Suc n))"
  2.1361 +              then show False
  2.1362 +                using k m \<open>0 < n\<close> a43 [of n m] b43 [of n m] fright right_neq
  2.1363 +                using alec [of "2*m+1" n] cleb [of "2*m+1" n] a_ge_0 [of "2*m+1" n] b_le_1 [of "2*m+1" n]
  2.1364 +                by (auto simp: algebra_simps)
  2.1365 +            next
  2.1366 +              fix x
  2.1367 +              assume "a (real j / 2 ^ Suc n) \<le> x" "x < b (real j / 2 ^ Suc n)" "f x = f (b (real j / 2 ^ Suc n))"
  2.1368 +              then show False
  2.1369 +                using Suc.IH [of "1 + m * 2", THEN conjunct2, THEN conjunct2]
  2.1370 +                using k m \<open>0 < n\<close> a43 [of n m] b43 [of n m]
  2.1371 +                using alec [of "2*m+1" n] cleb [of "2*m+1" n] a_ge_0 [of "2*m+1" n] b_le_1 [of "2*m+1" n]
  2.1372 +                using left_right_m [of "c((2*m + 1) / 2^n)" "a((2*m + 1) / 2^n)" "b((2*m + 1) / 2^n)"]
  2.1373 +                by (auto simp: algebra_simps fright simp del: power_Suc)
  2.1374 +            qed
  2.1375 +          qed
  2.1376 +        qed
  2.1377 +      qed
  2.1378 +    qed
  2.1379 +    have c_gt_0 [simp]: "0 < c(m / 2^n)" and c_less_1 [simp]: "c(m / 2^n) < 1" for m::nat and n
  2.1380 +      using a_less_b [of m n] apply (simp_all add: c_def midpoint_def)
  2.1381 +      using a_ge_0 [of m n] b_le_1 [of m n] apply linarith+
  2.1382 +      done
  2.1383 +    have approx: "\<exists>j n. odd j \<and> n \<noteq> 0 \<and>
  2.1384 +                        real i / 2^m \<le> real j / 2^n \<and>
  2.1385 +                        real j / 2^n \<le> real k / 2^p \<and>
  2.1386 +                        \<bar>real i / 2 ^ m - real j / 2 ^ n\<bar> < 1/2^n \<and>
  2.1387 +                        \<bar>real k / 2 ^ p - real j / 2 ^ n\<bar> < 1/2^n"
  2.1388 +      if "0 < i" "i < 2 ^ m" "0 < k" "k < 2 ^ p" "i / 2^m < k / 2^p" "m + p = N" for N m p i k
  2.1389 +      using that
  2.1390 +    proof (induction N arbitrary: m p i k rule: less_induct)
  2.1391 +      case (less N)
  2.1392 +      then consider "i / 2^m \<le> 1/2" "1/2 \<le> k / 2^p" | "k / 2^p < 1/2" | "k / 2^p \<ge> 1/2" "1/2 < i / 2^m"
  2.1393 +        by linarith
  2.1394 +      then show ?case
  2.1395 +      proof cases
  2.1396 +        case 1
  2.1397 +        with less.prems show ?thesis
  2.1398 +          by (rule_tac x=1 in exI)+ (fastforce simp: divide_simps)
  2.1399 +      next
  2.1400 +        case 2 show ?thesis
  2.1401 +        proof (cases m)
  2.1402 +          case 0 with less.prems show ?thesis
  2.1403 +            by auto
  2.1404 +        next
  2.1405 +          case (Suc m') show ?thesis
  2.1406 +          proof (cases p)
  2.1407 +            case 0 with less.prems show ?thesis by auto
  2.1408 +          next
  2.1409 +            case (Suc p')
  2.1410 +            have False if "real i * 2 ^ p' < real k * 2 ^ m'" "k < 2 ^ p'" "2 ^ m' \<le> i"
  2.1411 +            proof -
  2.1412 +              have "real k * 2 ^ m' < 2 ^ p' * 2 ^ m'"
  2.1413 +                using that by simp
  2.1414 +              then have "real i * 2 ^ p' < 2 ^ p' * 2 ^ m'"
  2.1415 +                using that by linarith
  2.1416 +              with that show ?thesis by simp
  2.1417 +            qed
  2.1418 +            then show ?thesis
  2.1419 +              using less.IH [of "m'+p'" i m' k p'] less.prems \<open>m = Suc m'\<close> 2 Suc
  2.1420 +              apply atomize
  2.1421 +              apply (force simp: divide_simps)
  2.1422 +              done
  2.1423 +          qed
  2.1424 +        qed
  2.1425 +      next
  2.1426 +        case 3 show ?thesis
  2.1427 +        proof (cases m)
  2.1428 +          case 0 with less.prems show ?thesis
  2.1429 +            by auto
  2.1430 +        next
  2.1431 +          case (Suc m') show ?thesis
  2.1432 +          proof (cases p)
  2.1433 +            case 0 with less.prems show ?thesis by auto
  2.1434 +          next
  2.1435 +            case (Suc p')
  2.1436 +            then show ?thesis
  2.1437 +              using less.IH [of "m'+p'" "i - 2^m'" m' "k - 2 ^ p'" p'] less.prems \<open>m = Suc m'\<close> Suc 3
  2.1438 +              apply atomize
  2.1439 +              apply (auto simp: field_simps of_nat_diff)
  2.1440 +              apply (rule_tac x="2 ^ n + j" in exI, simp)
  2.1441 +              apply (rule_tac x="Suc n" in exI)
  2.1442 +              apply (auto simp: field_simps)
  2.1443 +              done
  2.1444 +          qed
  2.1445 +        qed
  2.1446 +      qed
  2.1447 +    qed
  2.1448 +    have clec: "c(real i / 2^m) \<le> c(real j / 2^n)"
  2.1449 +      if i: "0 < i" "i < 2 ^ m" and j: "0 < j" "j < 2 ^ n" and ij: "i / 2^m < j / 2^n" for m i n j
  2.1450 +    proof -
  2.1451 +      obtain j' n' where "odd j'" "n' \<noteq> 0"
  2.1452 +        and i_le_j: "real i / 2 ^ m \<le> real j' / 2 ^ n'"
  2.1453 +        and j_le_j: "real j' / 2 ^ n' \<le> real j / 2 ^ n"
  2.1454 +        and clo_ij: "\<bar>real i / 2 ^ m - real j' / 2 ^ n'\<bar> < 1/2 ^ n'"
  2.1455 +        and clo_jj: "\<bar>real j / 2 ^ n - real j' / 2 ^ n'\<bar> < 1/2 ^ n'"
  2.1456 +        using approx [of i m j n "m+n"] that i j ij by auto
  2.1457 +      with oddE obtain q where q: "j' = Suc (2*q)" by fastforce
  2.1458 +      have "c (real i / 2 ^ m) \<le> c((2*q + 1) / 2^n')"
  2.1459 +      proof (cases "i / 2^m = (2*q + 1) / 2^n'")
  2.1460 +        case True then show ?thesis by simp
  2.1461 +      next
  2.1462 +        case False
  2.1463 +        with i_le_j q have less: "i / 2^m < (2*q + 1) / 2^n'"
  2.1464 +          by auto
  2.1465 +        have *: "\<lbrakk>i < q; abs(i - q) < s*2; q = r + s\<rbrakk> \<Longrightarrow> abs(i - r) < s" for i q s r::real
  2.1466 +          by auto
  2.1467 +        have "c(i / 2^m) \<le> b(real(4 * q + 1) / 2 ^ (Suc n'))"
  2.1468 +          apply (rule ci_le_bj, force)
  2.1469 +          apply (rule * [OF less])
  2.1470 +          using i_le_j clo_ij q apply (auto simp: divide_simps)
  2.1471 +          done
  2.1472 +        then show ?thesis
  2.1473 +          using alec [of "2*q+1" n'] cleb [of "2*q+1" n'] a_ge_0 [of "2*q+1" n'] b_le_1 [of "2*q+1" n'] b41 [of n' q] \<open>n' \<noteq> 0\<close>
  2.1474 +          using left_right_m [of "c((2*q + 1) / 2^n')" "a((2*q + 1) / 2^n')" "b((2*q + 1) / 2^n')"]
  2.1475 +          by (auto simp: algebra_simps)
  2.1476 +      qed
  2.1477 +      also have "... \<le> c(real j / 2^n)"
  2.1478 +      proof (cases "j / 2^n = (2*q + 1) / 2^n'")
  2.1479 +        case True
  2.1480 +        then show ?thesis by simp
  2.1481 +      next
  2.1482 +        case False
  2.1483 +        with j_le_j q have less: "(2*q + 1) / 2^n' < j / 2^n"
  2.1484 +          by auto
  2.1485 +        have *: "\<lbrakk>q < i; abs(i - q) < s*2; r = q + s\<rbrakk> \<Longrightarrow> abs(i - r) < s" for i q s r::real
  2.1486 +          by auto
  2.1487 +        have "a(real(4*q + 3) / 2 ^ (Suc n')) \<le> c(j / 2^n)"
  2.1488 +          apply (rule aj_le_ci, force)
  2.1489 +          apply (rule * [OF less])
  2.1490 +          using j_le_j clo_jj q apply (auto simp: divide_simps)
  2.1491 +          done
  2.1492 +        then show ?thesis
  2.1493 +          using alec [of "2*q+1" n'] cleb [of "2*q+1" n'] a_ge_0 [of "2*q+1" n'] b_le_1 [of "2*q+1" n'] a43 [of n' q] \<open>n' \<noteq> 0\<close>
  2.1494 +          using left_right_m [of "c((2*q + 1) / 2^n')" "a((2*q + 1) / 2^n')" "b((2*q + 1) / 2^n')"]
  2.1495 +          by (auto simp: algebra_simps)
  2.1496 +      qed
  2.1497 +      finally show ?thesis .
  2.1498 +    qed
  2.1499 +    have "x = y" if "0 \<le> x" "x \<le> 1" "0 \<le> y" "y \<le> 1" "h x = h y" for x y
  2.1500 +      using that
  2.1501 +    proof (induction x y rule: linorder_class.linorder_less_wlog)
  2.1502 +      case (less x1 x2)
  2.1503 +      obtain m n where m: "0 < m" "m < 2 ^ n"
  2.1504 +        and x12: "x1 < m / 2^n" "m / 2^n < x2"
  2.1505 +        and neq: "h x1 \<noteq> h (real m / 2^n)"
  2.1506 +      proof -
  2.1507 +        have "(x1 + x2) / 2 \<in> closure D01"
  2.1508 +          using cloD01 less.hyps less.prems by auto
  2.1509 +        with less obtain y where "y \<in> D01" and dist_y: "dist y ((x1 + x2) / 2) < (x2 - x1) / 64"
  2.1510 +          unfolding closure_approachable
  2.1511 +          by (metis diff_gt_0_iff_gt less_divide_eq_numeral1(1) mult_zero_left)
  2.1512 +        obtain m n where m: "0 < m" "m < 2 ^ n"
  2.1513 +                     and clo: "\<bar>real m / 2 ^ n - (x1 + x2) / 2\<bar> < (x2 - x1) / 64"
  2.1514 +                     and n: "1/2^n < (x2 - x1) / 128"
  2.1515 +        proof -
  2.1516 +          have "min 1 ((x2 - x1) / 128) > 0" "1/2 < (1::real)"
  2.1517 +            using less by auto
  2.1518 +          then obtain N where N: "1/2^N < min 1 ((x2 - x1) / 128)"
  2.1519 +            by (metis power_one_over real_arch_pow_inv)
  2.1520 +          then have "N > 0"
  2.1521 +            using less_divide_eq_1 by force
  2.1522 +          obtain p q where p: "p < 2 ^ q" "p \<noteq> 0" and yeq: "y = real p / 2 ^ q"
  2.1523 +            using \<open>y \<in> D01\<close> by (auto simp: zero_less_divide_iff D01_def)
  2.1524 +          show ?thesis
  2.1525 +          proof
  2.1526 +            show "0 < 2^N * p"
  2.1527 +              using p by auto
  2.1528 +            show "2 ^ N * p < 2 ^ (N+q)"
  2.1529 +              by (simp add: p power_add)
  2.1530 +            have "\<bar>real (2 ^ N * p) / 2 ^ (N + q) - (x1 + x2) / 2\<bar> = \<bar>real p / 2 ^ q - (x1 + x2) / 2\<bar>"
  2.1531 +              by (simp add: power_add)
  2.1532 +            also have "... = \<bar>y - (x1 + x2) / 2\<bar>"
  2.1533 +              by (simp add: yeq)
  2.1534 +            also have "... < (x2 - x1) / 64"
  2.1535 +              using dist_y by (simp add: dist_norm)
  2.1536 +            finally show "\<bar>real (2 ^ N * p) / 2 ^ (N + q) - (x1 + x2) / 2\<bar> < (x2 - x1) / 64" .
  2.1537 +            have "(1::real) / 2 ^ (N + q) \<le> 1/2^N"
  2.1538 +              by (simp add: field_simps)
  2.1539 +            also have "... < (x2 - x1) / 128"
  2.1540 +              using N by force
  2.1541 +            finally show "1/2 ^ (N + q) < (x2 - x1) / 128" .
  2.1542 +          qed
  2.1543 +        qed
  2.1544 +        obtain m' n' m'' n'' where "0 < m'" "m' < 2 ^ n'" "x1 < m' / 2^n'" "m' / 2^n' < x2"
  2.1545 +          and "0 < m''" "m'' < 2 ^ n''" "x1 < m'' / 2^n''" "m'' / 2^n'' < x2"
  2.1546 +          and neq: "h (real m'' / 2^n'') \<noteq> h (real m' / 2^n')"
  2.1547 +        proof
  2.1548 +          show "0 < Suc (2*m)"
  2.1549 +            by simp
  2.1550 +          show m21: "Suc (2*m) < 2 ^ Suc n"
  2.1551 +            using m by auto
  2.1552 +          show "x1 < real (Suc (2 * m)) / 2 ^ Suc n"
  2.1553 +            using clo by (simp add: field_simps abs_if split: if_split_asm)
  2.1554 +          show "real (Suc (2 * m)) / 2 ^ Suc n < x2"
  2.1555 +            using n clo by (simp add: field_simps abs_if split: if_split_asm)
  2.1556 +          show "0 < 4*m + 3"
  2.1557 +            by simp
  2.1558 +          have "m+1 \<le> 2 ^ n"
  2.1559 +            using m by simp
  2.1560 +          then have "4 * (m+1) \<le> 4 * (2 ^ n)"
  2.1561 +            by simp
  2.1562 +          then show m43: "4*m + 3 < 2 ^ (n+2)"
  2.1563 +            by (simp add: algebra_simps)
  2.1564 +          show "x1 < real (4 * m + 3) / 2 ^ (n + 2)"
  2.1565 +            using clo by (simp add: field_simps abs_if split: if_split_asm)
  2.1566 +          show "real (4 * m + 3) / 2 ^ (n + 2) < x2"
  2.1567 +            using n clo by (simp add: field_simps abs_if split: if_split_asm)
  2.1568 +          have c_fold: "midpoint (a ((2 * real m + 1) / 2 ^ Suc n)) (b ((2 * real m + 1) / 2 ^ Suc n)) = c ((2 * real m + 1) / 2 ^ Suc n)"
  2.1569 +            by (simp add: c_def)
  2.1570 +          define R where "R \<equiv> rightcut (a ((2 * real m + 1) / 2 ^ Suc n)) (b ((2 * real m + 1) / 2 ^ Suc n))  (c ((2 * real m + 1) / 2 ^ Suc n))"
  2.1571 +          have "R < b ((2 * real m + 1) / 2 ^ Suc n)"
  2.1572 +            unfolding R_def  using a_less_b [of "4*m + 3" "n+2"] a43 [of "Suc n" m] b43 [of "Suc n" m]
  2.1573 +            by simp
  2.1574 +          then have Rless: "R < midpoint R (b ((2 * real m + 1) / 2 ^ Suc n))"
  2.1575 +            by (simp add: midpoint_def)
  2.1576 +          have midR_le: "midpoint R (b ((2 * real m + 1) / 2 ^ Suc n)) \<le> b ((2 * real m + 1) / (2 * 2 ^ n))"
  2.1577 +            using \<open>R < b ((2 * real m + 1) / 2 ^ Suc n)\<close>
  2.1578 +            by (simp add: midpoint_def)
  2.1579 +          have "(real (Suc (2 * m)) / 2 ^ Suc n) \<in> D01"  "real (4 * m + 3) / 2 ^ (n + 2) \<in> D01"
  2.1580 +            by (simp_all add: D01_def m21 m43 del: power_Suc of_nat_Suc of_nat_add add_2_eq_Suc') blast+
  2.1581 +          then show "h (real (4 * m + 3) / 2 ^ (n + 2)) \<noteq> h (real (Suc (2 * m)) / 2 ^ Suc n)"
  2.1582 +            using a_less_b [of "4*m + 3" "n+2", THEN conjunct1]
  2.1583 +            using a43 [of "Suc n" m] b43 [of "Suc n" m]
  2.1584 +            using alec [of "2*m+1" "Suc n"] cleb [of "2*m+1" "Suc n"] a_ge_0 [of "2*m+1" "Suc n"]  b_le_1 [of "2*m+1" "Suc n"]
  2.1585 +            apply (simp add: fc_eq [symmetric] c_def del: power_Suc)
  2.1586 +            apply (simp only: add.commute [of 1] c_fold R_def [symmetric])
  2.1587 +            apply (rule right_neq)
  2.1588 +            using Rless apply (simp add: R_def)
  2.1589 +               apply (rule midR_le, auto)
  2.1590 +            done
  2.1591 +        qed
  2.1592 +        then show ?thesis by (metis that)
  2.1593 +      qed
  2.1594 +      have m_div: "0 < m / 2^n" "m / 2^n < 1"
  2.1595 +        using m  by (auto simp: divide_simps)
  2.1596 +      have closure0m: "{0..m / 2^n} = closure ({0<..< m / 2^n} \<inter> (\<Union>k m. {real m / 2 ^ k}))"
  2.1597 +        by (subst closure_dyadic_rationals_in_convex_set_pos_1, simp_all add: not_le m)
  2.1598 +      have closurem1: "{m / 2^n .. 1} = closure ({m / 2^n <..< 1} \<inter> (\<Union>k m. {real m / 2 ^ k}))"
  2.1599 +        apply (subst closure_dyadic_rationals_in_convex_set_pos_1; simp add: not_le m)
  2.1600 +        using \<open>0 < real m / 2 ^ n\<close> by linarith
  2.1601 +      have cont_h': "continuous_on (closure ({u<..<v} \<inter> (\<Union>k m. {real m / 2 ^ k}))) h"
  2.1602 +        if "0 \<le> u" "v \<le> 1" for u v
  2.1603 +        apply (rule continuous_on_subset [OF cont_h])
  2.1604 +        apply (rule closure_minimal [OF subsetI])
  2.1605 +        using that apply auto
  2.1606 +        done
  2.1607 +      have closed_f': "closed (f ` {u..v})" if "0 \<le> u" "v \<le> 1" for u v
  2.1608 +        by (metis compact_continuous_image cont_f compact_interval atLeastatMost_subset_iff
  2.1609 +            compact_imp_closed continuous_on_subset that)
  2.1610 +      have less_2I: "\<And>k i. real i / 2 ^ k < 1 \<Longrightarrow> i < 2 ^ k"
  2.1611 +        by simp
  2.1612 +      have "h ` ({0<..<m / 2 ^ n} \<inter> (\<Union>q p. {real p / 2 ^ q})) \<subseteq> f ` {0..c (m / 2 ^ n)}"
  2.1613 +      proof clarsimp
  2.1614 +        fix p q
  2.1615 +        assume p: "0 < real p / 2 ^ q" "real p / 2 ^ q < real m / 2 ^ n"
  2.1616 +        then have [simp]: "0 < p" "p < 2 ^ q"
  2.1617 +           apply (simp add: divide_simps)
  2.1618 +          apply (blast intro: p less_2I m_div less_trans)
  2.1619 +          done
  2.1620 +        have "f (c (real p / 2 ^ q)) \<in> f ` {0..c (real m / 2 ^ n)}"
  2.1621 +          by (auto simp: clec p m)
  2.1622 +        then show "h (real p / 2 ^ q) \<in> f ` {0..c (real m / 2 ^ n)}"
  2.1623 +          by (simp add: h_eq)
  2.1624 +      qed
  2.1625 +      then have "h ` {0 .. m / 2^n} \<subseteq> f ` {0 .. c(m / 2^n)}"
  2.1626 +        apply (subst closure0m)
  2.1627 +        apply (rule image_closure_subset [OF cont_h' closed_f'])
  2.1628 +        using m_div apply auto
  2.1629 +        done
  2.1630 +      then have hx1: "h x1 \<in> f ` {0 .. c(m / 2^n)}"
  2.1631 +        using x12 less.prems(1) by auto
  2.1632 +      then obtain t1 where t1: "h x1 = f t1" "0 \<le> t1" "t1 \<le> c (m / 2 ^ n)"
  2.1633 +        by auto
  2.1634 +      have "h ` ({m / 2 ^ n<..<1} \<inter> (\<Union>q p. {real p / 2 ^ q})) \<subseteq> f ` {c (m / 2 ^ n)..1}"
  2.1635 +      proof clarsimp
  2.1636 +        fix p q
  2.1637 +        assume p: "real m / 2 ^ n < real p / 2 ^ q" and [simp]: "p < 2 ^ q"
  2.1638 +        then have [simp]: "0 < p"
  2.1639 +          using gr_zeroI m_div by fastforce
  2.1640 +        have "f (c (real p / 2 ^ q)) \<in> f ` {c (m / 2 ^ n)..1}"
  2.1641 +          by (auto simp: clec p m)
  2.1642 +        then show "h (real p / 2 ^ q) \<in> f ` {c (real m / 2 ^ n)..1}"
  2.1643 +          by (simp add: h_eq)
  2.1644 +      qed
  2.1645 +      then have "h ` {m / 2^n .. 1} \<subseteq> f ` {c(m / 2^n) .. 1}"
  2.1646 +        apply (subst closurem1)
  2.1647 +        apply (rule image_closure_subset [OF cont_h' closed_f'])
  2.1648 +        using m apply auto
  2.1649 +        done
  2.1650 +      then have hx2: "h x2 \<in> f ` {c(m / 2^n)..1}"
  2.1651 +        using x12 less.prems by auto
  2.1652 +      then obtain t2 where t2: "h x2 = f t2" "c (m / 2 ^ n) \<le> t2" "t2 \<le> 1"
  2.1653 +        by auto
  2.1654 +      with t1 less neq have False
  2.1655 +        using conn [of "h x2", unfolded is_interval_connected_1 [symmetric] is_interval_1, rule_format, of t1 t2 "c(m / 2^n)"]
  2.1656 +        by (simp add: h_eq m)
  2.1657 +      then show ?case by blast
  2.1658 +    qed auto
  2.1659 +    then show ?thesis
  2.1660 +      by (auto simp: inj_on_def)
  2.1661 +  qed
  2.1662 +  ultimately have "{0..1::real} homeomorphic f ` {0..1}"
  2.1663 +    using homeomorphic_compact [OF _ cont_h] by blast
  2.1664 +  then show ?thesis
  2.1665 +    using homeomorphic_sym by blast
  2.1666 +qed
  2.1667 +
  2.1668 +
  2.1669 +theorem path_contains_arc:
  2.1670 +  fixes p :: "real \<Rightarrow> 'a::{complete_space,real_normed_vector}"
  2.1671 +  assumes "path p" and a: "pathstart p = a" and b: "pathfinish p = b" and "a \<noteq> b"
  2.1672 +  obtains q where "arc q" "path_image q \<subseteq> path_image p" "pathstart q = a" "pathfinish q = b"
  2.1673 +proof -
  2.1674 +  have ucont_p: "uniformly_continuous_on {0..1} p"
  2.1675 +    using \<open>path p\<close> unfolding path_def
  2.1676 +    by (metis compact_Icc compact_uniformly_continuous)
  2.1677 +  define \<phi> where "\<phi> \<equiv> \<lambda>S. S \<subseteq> {0..1} \<and> 0 \<in> S \<and> 1 \<in> S \<and>
  2.1678 +                           (\<forall>x \<in> S. \<forall>y \<in> S. open_segment x y \<inter> S = {} \<longrightarrow> p x = p y)"
  2.1679 +  obtain T where "closed T" "\<phi> T" and T: "\<And>U. \<lbrakk>closed U; \<phi> U\<rbrakk> \<Longrightarrow> \<not> (U \<subset> T)"
  2.1680 +  proof (rule Brouwer_reduction_theorem_gen [of "{0..1}" \<phi>])
  2.1681 +    have *: "{x<..<y} \<inter> {0..1} = {x<..<y}" if "0 \<le> x" "y \<le> 1" "x \<le> y" for x y::real
  2.1682 +      using that by auto
  2.1683 +    show "\<phi> {0..1}"
  2.1684 +      by (auto simp: \<phi>_def open_segment_eq_real_ivl *)
  2.1685 +    show "\<phi> (INTER UNIV F)"
  2.1686 +      if "\<And>n. closed (F n)" and \<phi>: "\<And>n. \<phi> (F n)" and Fsub: "\<And>n. F (Suc n) \<subseteq> F n" for F
  2.1687 +    proof -
  2.1688 +      have F01: "\<And>n. F n \<subseteq> {0..1} \<and> 0 \<in> F n \<and> 1 \<in> F n"
  2.1689 +        and peq: "\<And>n x y. \<lbrakk>x \<in> F n; y \<in> F n; open_segment x y \<inter> F n = {}\<rbrakk> \<Longrightarrow> p x = p y"
  2.1690 +        by (metis \<phi> \<phi>_def)+
  2.1691 +      have pqF: False if "\<forall>u. x \<in> F u" "\<forall>x. y \<in> F x" "open_segment x y \<inter> (\<Inter>x. F x) = {}" and neg: "p x \<noteq> p y"
  2.1692 +        for x y
  2.1693 +        using that
  2.1694 +      proof (induction x y rule: linorder_class.linorder_less_wlog)
  2.1695 +        case (less x y)
  2.1696 +        have xy: "x \<in> {0..1}" "y \<in> {0..1}"
  2.1697 +          by (metis less.prems subsetCE F01)+
  2.1698 +        have "norm(p x - p y) / 2 > 0"
  2.1699 +          using less by auto
  2.1700 +        then obtain e where "e > 0"
  2.1701 +          and e: "\<And>u v. \<lbrakk>u \<in> {0..1}; v \<in> {0..1}; dist v u < e\<rbrakk> \<Longrightarrow> dist (p v) (p u) < norm(p x - p y) / 2"
  2.1702 +          by (metis uniformly_continuous_onE [OF ucont_p])
  2.1703 +        have minxy: "min e (y - x)  < (y - x) * (3 / 2)"
  2.1704 +          by (subst min_less_iff_disj) (simp add: less)
  2.1705 +        obtain w z where "w < z" and w: "w \<in> {x<..<y}" and z: "z \<in> {x<..<y}"
  2.1706 +          and wxe: "norm(w - x) < e" and zye: "norm(z - y) < e"
  2.1707 +          apply (rule_tac w = "x + (min e (y - x) / 3)" and z = "y - (min e (y - x) / 3)" in that)
  2.1708 +          using minxy \<open>0 < e\<close> less by simp_all
  2.1709 +        have Fclo: "\<And>T. T \<in> range F \<Longrightarrow> closed T"
  2.1710 +          by (metis \<open>\<And>n. closed (F n)\<close> image_iff)
  2.1711 +        have eq: "{w..z} \<inter> INTER UNIV F = {}"
  2.1712 +          using less w z apply (auto simp: open_segment_eq_real_ivl)
  2.1713 +          by (metis (no_types, hide_lams) INT_I IntI empty_iff greaterThanLessThan_iff not_le order.trans)
  2.1714 +        then obtain K where "finite K" and K: "{w..z} \<inter> (\<Inter> (F ` K)) = {}"
  2.1715 +          by (metis finite_subset_image compact_imp_fip [OF compact_interval Fclo])
  2.1716 +        then have "K \<noteq> {}"
  2.1717 +          using \<open>w < z\<close> \<open>{w..z} \<inter> INTER K F = {}\<close> by auto
  2.1718 +        define n where "n \<equiv> Max K"
  2.1719 +        have "n \<in> K" unfolding n_def by (metis \<open>K \<noteq> {}\<close> \<open>finite K\<close> Max_in)
  2.1720 +        have "F n \<subseteq> \<Inter> (F ` K)"
  2.1721 +          unfolding n_def by (metis Fsub Max_ge \<open>K \<noteq> {}\<close> \<open>finite K\<close> cINF_greatest lift_Suc_antimono_le)
  2.1722 +        with K have wzF_null: "{w..z} \<inter> F n = {}"
  2.1723 +          by (metis disjoint_iff_not_equal subset_eq)
  2.1724 +        obtain u where u: "u \<in> F n" "u \<in> {x..w}" "({u..w} - {u}) \<inter> F n = {}"
  2.1725 +        proof (cases "w \<in> F n")
  2.1726 +          case True
  2.1727 +          then show ?thesis
  2.1728 +            by (metis wzF_null \<open>w < z\<close> atLeastAtMost_iff disjoint_iff_not_equal less_eq_real_def)
  2.1729 +        next
  2.1730 +          case False
  2.1731 +          obtain u where "u \<in> F n" "u \<in> {x..w}" "{u<..<w} \<inter> F n = {}"
  2.1732 +          proof (rule segment_to_point_exists [of "F n \<inter> {x..w}" w])
  2.1733 +            show "closed (F n \<inter> {x..w})"
  2.1734 +              by (metis \<open>\<And>n. closed (F n)\<close> closed_Int closed_real_atLeastAtMost)
  2.1735 +            show "F n \<inter> {x..w} \<noteq> {}"
  2.1736 +              by (metis atLeastAtMost_iff disjoint_iff_not_equal greaterThanLessThan_iff less.prems(1) less_eq_real_def w)
  2.1737 +          qed (auto simp: open_segment_eq_real_ivl intro!: that)
  2.1738 +          with False show thesis
  2.1739 +            apply (auto simp: disjoint_iff_not_equal intro!: that)
  2.1740 +            by (metis greaterThanLessThan_iff less_eq_real_def)
  2.1741 +        qed
  2.1742 +        obtain v where v: "v \<in> F n" "v \<in> {z..y}" "({z..v} - {v}) \<inter> F n = {}"
  2.1743 +        proof (cases "z \<in> F n")
  2.1744 +          case True
  2.1745 +          have "z \<in> {w..z}"
  2.1746 +            using \<open>w < z\<close> by auto
  2.1747 +          then show ?thesis
  2.1748 +            by (metis wzF_null Int_iff True empty_iff)
  2.1749 +        next
  2.1750 +          case False
  2.1751 +          show ?thesis
  2.1752 +          proof (rule segment_to_point_exists [of "F n \<inter> {z..y}" z])
  2.1753 +            show "closed (F n \<inter> {z..y})"
  2.1754 +              by (metis \<open>\<And>n. closed (F n)\<close> closed_Int closed_atLeastAtMost)
  2.1755 +            show "F n \<inter> {z..y} \<noteq> {}"
  2.1756 +              by (metis atLeastAtMost_iff disjoint_iff_not_equal greaterThanLessThan_iff less.prems(2) less_eq_real_def z)
  2.1757 +            show "\<And>b. \<lbrakk>b \<in> F n \<inter> {z..y}; open_segment z b \<inter> (F n \<inter> {z..y}) = {}\<rbrakk> \<Longrightarrow> thesis"
  2.1758 +              apply (rule that)
  2.1759 +                apply (auto simp: open_segment_eq_real_ivl)
  2.1760 +              by (metis DiffI Int_iff atLeastAtMost_diff_ends atLeastAtMost_iff atLeastatMost_empty_iff empty_iff insert_iff False)
  2.1761 +          qed
  2.1762 +        qed
  2.1763 +        obtain u v where "u \<in> {0..1}" "v \<in> {0..1}" "norm(u - x) < e" "norm(v - y) < e" "p u = p v"
  2.1764 +        proof
  2.1765 +          show "u \<in> {0..1}" "v \<in> {0..1}"
  2.1766 +            by (metis F01 \<open>u \<in> F n\<close> \<open>v \<in> F n\<close> subsetD)+
  2.1767 +          show "norm(u - x) < e" "norm (v - y) < e"
  2.1768 +            using \<open>u \<in> {x..w}\<close> \<open>v \<in> {z..y}\<close> atLeastAtMost_iff real_norm_def wxe zye by auto
  2.1769 +          show "p u = p v"
  2.1770 +          proof (rule peq)
  2.1771 +            show "u \<in> F n" "v \<in> F n"
  2.1772 +              by (auto simp: u v)
  2.1773 +            have "False" if "\<xi> \<in> F n" "u < \<xi>" "\<xi> < v" for \<xi>
  2.1774 +            proof -
  2.1775 +              have "\<xi> \<notin> {z..v}"
  2.1776 +                by (metis DiffI disjoint_iff_not_equal less_irrefl singletonD that v(3))
  2.1777 +              moreover have "\<xi> \<notin> {w..z} \<inter> F n"
  2.1778 +                by (metis equals0D wzF_null)
  2.1779 +              ultimately have "\<xi> \<in> {u..w}"
  2.1780 +                using that by auto
  2.1781 +              then show ?thesis
  2.1782 +                by (metis DiffI disjoint_iff_not_equal less_eq_real_def not_le singletonD that u(3))
  2.1783 +            qed
  2.1784 +            moreover
  2.1785 +            have "\<lbrakk>\<xi> \<in> F n; v < \<xi>; \<xi> < u\<rbrakk> \<Longrightarrow> False" for \<xi>
  2.1786 +              using \<open>u \<in> {x..w}\<close> \<open>v \<in> {z..y}\<close> \<open>w < z\<close> by simp
  2.1787 +            ultimately
  2.1788 +            show "open_segment u v \<inter> F n = {}"
  2.1789 +              by (force simp: open_segment_eq_real_ivl)
  2.1790 +          qed
  2.1791 +        qed
  2.1792 +        then show ?case
  2.1793 +          using e [of x u] e [of y v] xy
  2.1794 +          apply (simp add: open_segment_eq_real_ivl dist_norm del: divide_const_simps)
  2.1795 +          by (metis dist_norm dist_triangle_half_r less_irrefl)
  2.1796 +      qed (auto simp: open_segment_commute)
  2.1797 +      show ?thesis
  2.1798 +        unfolding \<phi>_def by (metis (no_types, hide_lams) INT_I Inf_lower2 rangeI that F01 subsetCE pqF)
  2.1799 +    qed
  2.1800 +    show "closed {0..1::real}" by auto
  2.1801 +  qed (meson \<phi>_def)
  2.1802 +  then have "T \<subseteq> {0..1}" "0 \<in> T" "1 \<in> T"
  2.1803 +    and peq: "\<And>x y. \<lbrakk>x \<in> T; y \<in> T; open_segment x y \<inter> T = {}\<rbrakk> \<Longrightarrow> p x = p y"
  2.1804 +    unfolding \<phi>_def by metis+
  2.1805 +  then have "T \<noteq> {}" by auto
  2.1806 +  define h where "h \<equiv> \<lambda>x. p(@y. y \<in> T \<and> open_segment x y \<inter> T = {})"
  2.1807 +  have "p y = p z" if "y \<in> T" "z \<in> T" and xyT: "open_segment x y \<inter> T = {}" and xzT: "open_segment x z \<inter> T = {}"
  2.1808 +    for x y z
  2.1809 +  proof (cases "x \<in> T")
  2.1810 +    case True
  2.1811 +    with that show ?thesis by (metis \<open>\<phi> T\<close> \<phi>_def)
  2.1812 +  next
  2.1813 +    case False
  2.1814 +    have "insert x (open_segment x y \<union> open_segment x z) \<inter> T = {}"
  2.1815 +      by (metis False Int_Un_distrib2 Int_insert_left Un_empty_right xyT xzT)
  2.1816 +    moreover have "open_segment y z \<inter> T \<subseteq> insert x (open_segment x y \<union> open_segment x z) \<inter> T"
  2.1817 +      apply auto
  2.1818 +      by (metis greaterThanLessThan_iff less_eq_real_def less_le_trans linorder_neqE_linordered_idom open_segment_eq_real_ivl)
  2.1819 +    ultimately have "open_segment y z \<inter> T = {}"
  2.1820 +      by blast
  2.1821 +    with that peq show ?thesis by metis
  2.1822 +  qed
  2.1823 +  then have h_eq_p_gen: "h x = p y" if "y \<in> T" "open_segment x y \<inter> T = {}" for x y
  2.1824 +    using that unfolding h_def
  2.1825 +    by (metis (mono_tags, lifting) some_eq_ex)
  2.1826 +  then have h_eq_p: "\<And>x. x \<in> T \<Longrightarrow> h x = p x"
  2.1827 +    by simp
  2.1828 +  have disjoint: "\<And>x. \<exists>y. y \<in> T \<and> open_segment x y \<inter> T = {}"
  2.1829 +    by (meson \<open>T \<noteq> {}\<close> \<open>closed T\<close> segment_to_point_exists)
  2.1830 +  have heq: "h x = h x'" if "open_segment x x' \<inter> T = {}" for x x'
  2.1831 +  proof (cases "x \<in> T \<or> x' \<in> T")
  2.1832 +    case True
  2.1833 +    then show ?thesis
  2.1834 +      by (metis h_eq_p h_eq_p_gen open_segment_commute that)
  2.1835 +  next
  2.1836 +    case False
  2.1837 +    obtain y y' where "y \<in> T" "open_segment x y \<inter> T = {}" "h x = p y"
  2.1838 +      "y' \<in> T" "open_segment x' y' \<inter> T = {}" "h x' = p y'"
  2.1839 +      by (meson disjoint h_eq_p_gen)
  2.1840 +    moreover have "open_segment y y' \<subseteq> (insert x (insert x' (open_segment x y \<union> open_segment x' y' \<union> open_segment x x')))"
  2.1841 +      by (auto simp: open_segment_eq_real_ivl)
  2.1842 +    ultimately show ?thesis
  2.1843 +      using False that by (fastforce simp add: h_eq_p intro!: peq)
  2.1844 +  qed
  2.1845 +  have "h ` {0..1} homeomorphic {0..1::real}"
  2.1846 +  proof (rule homeomorphic_monotone_image_interval)
  2.1847 +    show "continuous_on {0..1} h"
  2.1848 +    proof (clarsimp simp add: continuous_on_iff)
  2.1849 +      fix u \<epsilon>::real
  2.1850 +      assume "0 < \<epsilon>" "0 \<le> u" "u \<le> 1"
  2.1851 +      then obtain \<delta> where "\<delta> > 0" and \<delta>: "\<And>v. v \<in> {0..1} \<Longrightarrow> dist v u < \<delta> \<longrightarrow> dist (p v) (p u) < \<epsilon> / 2"
  2.1852 +        using ucont_p [unfolded uniformly_continuous_on_def]
  2.1853 +        by (metis atLeastAtMost_iff half_gt_zero_iff)
  2.1854 +      then have "dist (h v) (h u) < \<epsilon>" if "v \<in> {0..1}" "dist v u < \<delta>" for v
  2.1855 +      proof (cases "open_segment u v \<inter> T = {}")
  2.1856 +        case True
  2.1857 +        then show ?thesis
  2.1858 +          using \<open>0 < \<epsilon>\<close> heq by auto
  2.1859 +      next
  2.1860 +        case False
  2.1861 +        have uvT: "closed (closed_segment u v \<inter> T)" "closed_segment u v \<inter> T \<noteq> {}"
  2.1862 +          using False open_closed_segment by (auto simp: \<open>closed T\<close> closed_Int)
  2.1863 +        obtain w where "w \<in> T" and w: "w \<in> closed_segment u v" "open_segment u w \<inter> T = {}"
  2.1864 +          apply (rule segment_to_point_exists [OF uvT, of u])
  2.1865 +          by (metis IntD1 Int_commute Int_left_commute ends_in_segment(1) inf.orderE subset_oc_segment)
  2.1866 +        then have puw: "dist (p u) (p w) < \<epsilon> / 2"
  2.1867 +          by (metis (no_types) \<open>T \<subseteq> {0..1}\<close> \<open>dist v u < \<delta>\<close> \<delta> dist_commute dist_in_closed_segment le_less_trans subsetCE)
  2.1868 +        obtain z where "z \<in> T" and z: "z \<in> closed_segment u v" "open_segment v z \<inter> T = {}"
  2.1869 +          apply (rule segment_to_point_exists [OF uvT, of v])
  2.1870 +          by (metis IntD2 Int_commute Int_left_commute ends_in_segment(2) inf.orderE subset_oc_segment)
  2.1871 +        then have "dist (p u) (p z) < \<epsilon> / 2"
  2.1872 +          by (metis \<open>T \<subseteq> {0..1}\<close> \<open>dist v u < \<delta>\<close> \<delta> dist_commute dist_in_closed_segment le_less_trans subsetCE)
  2.1873 +        then show ?thesis
  2.1874 +          using puw by (metis (no_types) \<open>w \<in> T\<close> \<open>z \<in> T\<close> dist_commute dist_triangle_half_l h_eq_p_gen w(2) z(2))
  2.1875 +      qed
  2.1876 +      with \<open>0 < \<delta>\<close> show "\<exists>\<delta>>0. \<forall>v\<in>{0..1}. dist v u < \<delta> \<longrightarrow> dist (h v) (h u) < \<epsilon>" by blast
  2.1877 +    qed
  2.1878 +    show "connected ({0..1} \<inter> h -` {z})" for z
  2.1879 +    proof (clarsimp simp add: connected_iff_connected_component)
  2.1880 +      fix u v
  2.1881 +      assume huv_eq: "h v = h u" and uv: "0 \<le> u" "u \<le> 1" "0 \<le> v" "v \<le> 1"
  2.1882 +      have "\<exists>T. connected T \<and> T \<subseteq> {0..1} \<and> T \<subseteq> h -` {h u} \<and> u \<in> T \<and> v \<in> T"
  2.1883 +      proof (intro exI conjI)
  2.1884 +        show "connected (closed_segment u v)"
  2.1885 +          by simp
  2.1886 +        show "closed_segment u v \<subseteq> {0..1}"
  2.1887 +          by (simp add: uv closed_segment_eq_real_ivl)
  2.1888 +        have pxy: "p x = p y"
  2.1889 +          if "T \<subseteq> {0..1}" "0 \<in> T" "1 \<in> T" "x \<in> T" "y \<in> T"
  2.1890 +          and disjT: "open_segment x y \<inter> (T - open_segment u v) = {}"
  2.1891 +          and xynot: "x \<notin> open_segment u v" "y \<notin> open_segment u v"
  2.1892 +          for x y
  2.1893 +        proof (cases "open_segment x y \<inter> open_segment u v = {}")
  2.1894 +          case True
  2.1895 +          then show ?thesis
  2.1896 +            by (metis Diff_Int_distrib Diff_empty peq disjT \<open>x \<in> T\<close> \<open>y \<in> T\<close>)
  2.1897 +        next
  2.1898 +          case False
  2.1899 +          then have "open_segment x u \<union> open_segment y v \<subseteq> open_segment x y - open_segment u v \<or>
  2.1900 +                     open_segment y u \<union> open_segment x v \<subseteq> open_segment x y - open_segment u v" (is "?xuyv \<or> ?yuxv")
  2.1901 +            using xynot by (fastforce simp add: open_segment_eq_real_ivl not_le not_less split: if_split_asm)
  2.1902 +          then show "p x = p y"
  2.1903 +          proof
  2.1904 +            assume "?xuyv"
  2.1905 +            then have "open_segment x u \<inter> T = {}" "open_segment y v \<inter> T = {}"
  2.1906 +              using disjT by auto
  2.1907 +            then have "h x = h y"
  2.1908 +              using heq huv_eq by auto
  2.1909 +            then show ?thesis
  2.1910 +              using h_eq_p \<open>x \<in> T\<close> \<open>y \<in> T\<close> by auto
  2.1911 +          next
  2.1912 +            assume "?yuxv"
  2.1913 +            then have "open_segment y u \<inter> T = {}" "open_segment x v \<inter> T = {}"
  2.1914 +              using disjT by auto
  2.1915 +            then have "h x = h y"
  2.1916 +              using heq [of y u]  heq [of x v] huv_eq by auto
  2.1917 +            then show ?thesis
  2.1918 +              using h_eq_p \<open>x \<in> T\<close> \<open>y \<in> T\<close> by auto
  2.1919 +          qed
  2.1920 +        qed
  2.1921 +        have "\<not> T - open_segment u v \<subset> T"
  2.1922 +        proof (rule T)
  2.1923 +          show "closed (T - open_segment u v)"
  2.1924 +            by (simp add: closed_Diff [OF \<open>closed T\<close>] open_segment_eq_real_ivl)
  2.1925 +          have "0 \<notin> open_segment u v" "1 \<notin> open_segment u v"
  2.1926 +            using open_segment_eq_real_ivl uv by auto
  2.1927 +          then show "\<phi> (T - open_segment u v)"
  2.1928 +            using \<open>T \<subseteq> {0..1}\<close> \<open>0 \<in> T\<close> \<open>1 \<in> T\<close>
  2.1929 +            by (auto simp: \<phi>_def) (meson peq pxy)
  2.1930 +        qed
  2.1931 +        then have "open_segment u v \<inter> T = {}"
  2.1932 +          by blast
  2.1933 +        then show "closed_segment u v \<subseteq> h -` {h u}"
  2.1934 +          by (force intro: heq simp: open_segment_eq_real_ivl closed_segment_eq_real_ivl split: if_split_asm)+
  2.1935 +      qed auto
  2.1936 +      then show "connected_component ({0..1} \<inter> h -` {h u}) u v"
  2.1937 +        by (simp add: connected_component_def)
  2.1938 +    qed
  2.1939 +    show "h 1 \<noteq> h 0"
  2.1940 +      by (metis \<open>\<phi> T\<close> \<phi>_def a \<open>a \<noteq> b\<close> b h_eq_p pathfinish_def pathstart_def)
  2.1941 +  qed
  2.1942 +  then obtain f and g :: "real \<Rightarrow> 'a"
  2.1943 +    where gfeq: "(\<forall>x\<in>h ` {0..1}. (g(f x) = x))" and fhim: "f ` h ` {0..1} = {0..1}" and contf: "continuous_on (h ` {0..1}) f"
  2.1944 +      and fgeq: "(\<forall>y\<in>{0..1}. (f(g y) = y))" and pag: "path_image g = h ` {0..1}" and contg: "continuous_on {0..1} g"
  2.1945 +    by (auto simp: homeomorphic_def homeomorphism_def path_image_def)
  2.1946 +  then have "arc g"
  2.1947 +    by (metis arc_def path_def inj_on_def)
  2.1948 +  obtain u v where "u \<in> {0..1}" "a = g u" "v \<in> {0..1}" "b = g v"
  2.1949 +    by (metis (mono_tags, hide_lams) \<open>\<phi> T\<close> \<phi>_def a b fhim gfeq h_eq_p imageI path_image_def pathfinish_def pathfinish_in_path_image pathstart_def pathstart_in_path_image)
  2.1950 +  then have "a \<in> path_image g" "b \<in> path_image g"
  2.1951 +    using path_image_def by blast+
  2.1952 +  have ph: "path_image h \<subseteq> path_image p"
  2.1953 +    by (metis image_mono image_subset_iff path_image_def disjoint h_eq_p_gen \<open>T \<subseteq> {0..1}\<close>)
  2.1954 +  show ?thesis
  2.1955 +  proof
  2.1956 +    show "pathstart (subpath u v g) = a" "pathfinish (subpath u v g) = b"
  2.1957 +      by (simp_all add: \<open>a = g u\<close> \<open>b = g v\<close>)
  2.1958 +    show "path_image (subpath u v g) \<subseteq> path_image p"
  2.1959 +      by (metis \<open>arc g\<close> \<open>u \<in> {0..1}\<close> \<open>v \<in> {0..1}\<close> arc_imp_path order_trans pag path_image_def path_image_subpath_subset ph)
  2.1960 +    show "arc (subpath u v g)"
  2.1961 +      using \<open>arc g\<close> \<open>a = g u\<close> \<open>b = g v\<close> \<open>u \<in> {0..1}\<close> \<open>v \<in> {0..1}\<close> arc_subpath_arc \<open>a \<noteq> b\<close> by blast
  2.1962 +  qed
  2.1963 +qed
  2.1964 +
  2.1965 +
  2.1966 +corollary path_connected_arcwise:
  2.1967 +  fixes S :: "'a::{complete_space,real_normed_vector} set"
  2.1968 +  shows "path_connected S \<longleftrightarrow>
  2.1969 +         (\<forall>x \<in> S. \<forall>y \<in> S. x \<noteq> y \<longrightarrow> (\<exists>g. arc g \<and> path_image g \<subseteq> S \<and> pathstart g = x \<and> pathfinish g = y))"
  2.1970 +        (is "?lhs = ?rhs")
  2.1971 +proof (intro iffI impI ballI)
  2.1972 +  fix x y
  2.1973 +  assume "path_connected S" "x \<in> S" "y \<in> S" "x \<noteq> y"
  2.1974 +  then obtain p where p: "path p" "path_image p \<subseteq> S" "pathstart p = x" "pathfinish p = y"
  2.1975 +    by (force simp: path_connected_def)
  2.1976 +  then show "\<exists>g. arc g \<and> path_image g \<subseteq> S \<and> pathstart g = x \<and> pathfinish g = y"
  2.1977 +    by (metis \<open>x \<noteq> y\<close> order_trans path_contains_arc)
  2.1978 +next
  2.1979 +  assume R [rule_format]: ?rhs
  2.1980 +  show ?lhs
  2.1981 +    unfolding path_connected_def
  2.1982 +  proof (intro ballI)
  2.1983 +    fix x y
  2.1984 +    assume "x \<in> S" "y \<in> S"
  2.1985 +    show "\<exists>g. path g \<and> path_image g \<subseteq> S \<and> pathstart g = x \<and> pathfinish g = y"
  2.1986 +    proof (cases "x = y")
  2.1987 +      case True with \<open>x \<in> S\<close> path_component_def path_component_refl show ?thesis
  2.1988 +        by blast
  2.1989 +    next
  2.1990 +      case False with R [OF \<open>x \<in> S\<close> \<open>y \<in> S\<close>] show ?thesis
  2.1991 +        by (auto intro: arc_imp_path)
  2.1992 +    qed
  2.1993 +  qed
  2.1994 +qed
  2.1995 +
  2.1996 +
  2.1997 +corollary arc_connected_trans:
  2.1998 +  fixes g :: "real \<Rightarrow> 'a::{complete_space,real_normed_vector}"
  2.1999 +  assumes "arc g" "arc h" "pathfinish g = pathstart h" "pathstart g \<noteq> pathfinish h"
  2.2000 +  obtains i where "arc i" "path_image i \<subseteq> path_image g \<union> path_image h"
  2.2001 +                  "pathstart i = pathstart g" "pathfinish i = pathfinish h"
  2.2002 +  by (metis (no_types, hide_lams) arc_imp_path assms path_contains_arc path_image_join path_join pathfinish_join pathstart_join)
  2.2003 +
  2.2004 +
  2.2005 +
  2.2006 +
  2.2007 +subsection\<open>Accessibility of frontier points\<close>
  2.2008 +
  2.2009 +lemma dense_accessible_frontier_points:
  2.2010 +  fixes S :: "'a::{complete_space,real_normed_vector} set"
  2.2011 +  assumes "open S" and opeSV: "openin (subtopology euclidean (frontier S)) V" and "V \<noteq> {}"
  2.2012 +  obtains g where "arc g" "g ` {0..<1} \<subseteq> S" "pathstart g \<in> S" "pathfinish g \<in> V"
  2.2013 +proof -
  2.2014 +  obtain z where "z \<in> V"
  2.2015 +    using \<open>V \<noteq> {}\<close> by auto
  2.2016 +  then obtain r where "r > 0" and r: "ball z r \<inter> frontier S \<subseteq> V"
  2.2017 +    by (metis openin_contains_ball opeSV)
  2.2018 +  then have "z \<in> frontier S"
  2.2019 +    using \<open>z \<in> V\<close> opeSV openin_contains_ball by blast
  2.2020 +  then have "z \<in> closure S" "z \<notin> S"
  2.2021 +    by (simp_all add: frontier_def assms interior_open)
  2.2022 +  with \<open>r > 0\<close> have "infinite (S \<inter> ball z r)"
  2.2023 +    by (auto simp: closure_def islimpt_eq_infinite_ball)
  2.2024 +  then obtain y where "y \<in> S" and y: "y \<in> ball z r"
  2.2025 +    using infinite_imp_nonempty by force
  2.2026 +  then have "y \<notin> frontier S"
  2.2027 +    by (meson \<open>open S\<close> disjoint_iff_not_equal frontier_disjoint_eq)
  2.2028 +  have "y \<noteq> z"
  2.2029 +    using \<open>y \<in> S\<close> \<open>z \<notin> S\<close> by blast
  2.2030 +  have "path_connected(ball z r)"
  2.2031 +    by (simp add: convex_imp_path_connected)
  2.2032 +  with y \<open>r > 0\<close>  obtain g where "arc g" and pig: "path_image g \<subseteq> ball z r"
  2.2033 +                                 and g: "pathstart g = y" "pathfinish g = z"
  2.2034 +    using \<open>y \<noteq> z\<close> by (force simp: path_connected_arcwise)
  2.2035 +  have "compact (g -` frontier S \<inter> {0..1})"
  2.2036 +    apply (simp add: compact_eq_bounded_closed bounded_Int bounded_closed_interval)
  2.2037 +     apply (rule closed_vimage_Int)
  2.2038 +    using \<open>arc g\<close> apply (auto simp: arc_def path_def)
  2.2039 +    done
  2.2040 +  moreover have "g -` frontier S \<inter> {0..1} \<noteq> {}"
  2.2041 +  proof -
  2.2042 +    have "\<exists>r. r \<in> g -` frontier S \<and> r \<in> {0..1}"
  2.2043 +      by (metis \<open>z \<in> frontier S\<close> g(2) imageE path_image_def pathfinish_in_path_image vimageI2)
  2.2044 +    then show ?thesis
  2.2045 +      by blast
  2.2046 +  qed
  2.2047 +  ultimately obtain t where gt: "g t \<in> frontier S" and "0 \<le> t" "t \<le> 1"
  2.2048 +                and t: "\<And>u. \<lbrakk>g u \<in> frontier S; 0 \<le> u; u \<le> 1\<rbrakk> \<Longrightarrow> t \<le> u"
  2.2049 +    by (force simp: dest!: compact_attains_inf)
  2.2050 +  moreover have "t \<noteq> 0"
  2.2051 +    by (metis \<open>y \<notin> frontier S\<close> g(1) gt pathstart_def)
  2.2052 +  ultimately have  t01: "0 < t" "t \<le> 1"
  2.2053 +    by auto
  2.2054 +  have "V \<subseteq> frontier S"
  2.2055 +    using opeSV openin_contains_ball by blast
  2.2056 +  show ?thesis
  2.2057 +  proof
  2.2058 +    show "arc (subpath 0 t g)"
  2.2059 +      by (simp add: \<open>0 \<le> t\<close> \<open>t \<le> 1\<close> \<open>arc g\<close> \<open>t \<noteq> 0\<close> arc_subpath_arc)
  2.2060 +    have "g 0 \<in> S"
  2.2061 +      by (metis \<open>y \<in> S\<close> g(1) pathstart_def)
  2.2062 +    then show "pathstart (subpath 0 t g) \<in> S"
  2.2063 +      by auto
  2.2064 +    have "g t \<in> V"
  2.2065 +      by (metis IntI atLeastAtMost_iff gt image_eqI path_image_def pig r subsetCE \<open>0 \<le> t\<close> \<open>t \<le> 1\<close>)
  2.2066 +    then show "pathfinish (subpath 0 t g) \<in> V"
  2.2067 +      by auto
  2.2068 +    then have "inj_on (subpath 0 t g) {0..1}"
  2.2069 +      using t01
  2.2070 +      apply (clarsimp simp: inj_on_def subpath_def)
  2.2071 +      apply (drule inj_onD [OF arc_imp_inj_on [OF \<open>arc g\<close>]])
  2.2072 +      using mult_le_one apply auto
  2.2073 +      done
  2.2074 +    then have "subpath 0 t g ` {0..<1} \<subseteq> subpath 0 t g ` {0..1} - {subpath 0 t g 1}"
  2.2075 +      by (force simp: dest: inj_onD)
  2.2076 +    moreover have False if "subpath 0 t g ` ({0..<1}) - S \<noteq> {}"
  2.2077 +    proof -
  2.2078 +      have contg: "continuous_on {0..1} g"
  2.2079 +        using \<open>arc g\<close> by (auto simp: arc_def path_def)
  2.2080 +      have "subpath 0 t g ` {0..<1} \<inter> frontier S \<noteq> {}"
  2.2081 +      proof (rule connected_Int_frontier [OF _ _ that])
  2.2082 +        show "connected (subpath 0 t g ` {0..<1})"
  2.2083 +          apply (rule connected_continuous_image)
  2.2084 +           apply (simp add: subpath_def)
  2.2085 +           apply (intro continuous_intros continuous_on_compose2 [OF contg])
  2.2086 +           apply (auto simp: \<open>0 \<le> t\<close> \<open>t \<le> 1\<close> mult_le_one)
  2.2087 +          done
  2.2088 +        show "subpath 0 t g ` {0..<1} \<inter> S \<noteq> {}"
  2.2089 +          using \<open>y \<in> S\<close> g(1) by (force simp: subpath_def image_def pathstart_def)
  2.2090 +      qed
  2.2091 +      then obtain x where "x \<in> subpath 0 t g ` {0..<1}" "x \<in> frontier S"
  2.2092 +        by blast
  2.2093 +      with t01 \<open>0 \<le> t\<close> mult_le_one t show False
  2.2094 +        by (fastforce simp: subpath_def)
  2.2095 +    qed
  2.2096 +    then have "subpath 0 t g ` {0..1} - {subpath 0 t g 1} \<subseteq> S"
  2.2097 +      using subsetD by fastforce
  2.2098 +    ultimately  show "subpath 0 t g ` {0..<1} \<subseteq> S"
  2.2099 +      by auto
  2.2100 +  qed
  2.2101 +qed
  2.2102 +
  2.2103 +
  2.2104 +lemma dense_accessible_frontier_points_connected:
  2.2105 +  fixes S :: "'a::{complete_space,real_normed_vector} set"
  2.2106 +  assumes "open S" "connected S" "x \<in> S" "V \<noteq> {}"
  2.2107 +      and ope: "openin (subtopology euclidean (frontier S)) V"
  2.2108 +  obtains g where "arc g" "g ` {0..<1} \<subseteq> S" "pathstart g = x" "pathfinish g \<in> V"
  2.2109 +proof -
  2.2110 +  have "V \<subseteq> frontier S"
  2.2111 +    using ope openin_imp_subset by blast
  2.2112 +  with \<open>open S\<close> \<open>x \<in> S\<close> have "x \<notin> V"
  2.2113 +    using interior_open by (auto simp: frontier_def)
  2.2114 +  obtain g where "arc g" and g: "g ` {0..<1} \<subseteq> S" "pathstart g \<in> S" "pathfinish g \<in> V"
  2.2115 +    by (metis dense_accessible_frontier_points [OF \<open>open S\<close> ope \<open>V \<noteq> {}\<close>])
  2.2116 +  then have "path_connected S"
  2.2117 +    by (simp add: assms connected_open_path_connected)
  2.2118 +  with \<open>pathstart g \<in> S\<close> \<open>x \<in> S\<close> have "path_component S x (pathstart g)"
  2.2119 +    by (simp add: path_connected_component)
  2.2120 +  then obtain f where "path f" and f: "path_image f \<subseteq> S" "pathstart f = x" "pathfinish f = pathstart g"
  2.2121 +    by (auto simp: path_component_def)
  2.2122 +  then have "path (f +++ g)"
  2.2123 +    by (simp add: \<open>arc g\<close> arc_imp_path)
  2.2124 +  then obtain h where "arc h"
  2.2125 +                  and h: "path_image h \<subseteq> path_image (f +++ g)" "pathstart h = x" "pathfinish h = pathfinish g"
  2.2126 +    apply (rule path_contains_arc [of "f +++ g" x "pathfinish g"])
  2.2127 +    using f \<open>x \<notin> V\<close> \<open>pathfinish g \<in> V\<close> by auto
  2.2128 +  have "h ` {0..1} - {h 1} \<subseteq> S"
  2.2129 +    using f g h apply (clarsimp simp: path_image_join)
  2.2130 +    apply (simp add: path_image_def pathfinish_def subset_iff image_def Bex_def)
  2.2131 +    by (metis le_less)
  2.2132 +  then have "h ` {0..<1} \<subseteq> S"
  2.2133 +    using \<open>arc h\<close> by (force simp: arc_def dest: inj_onD)
  2.2134 +  then show thesis
  2.2135 +    apply (rule that [OF \<open>arc h\<close>])
  2.2136 +    using h \<open>pathfinish g \<in> V\<close> by auto
  2.2137 +qed
  2.2138 +
  2.2139 +lemma dense_access_fp_aux:
  2.2140 +  fixes S :: "'a::{complete_space,real_normed_vector} set"
  2.2141 +  assumes S: "open S" "connected S"
  2.2142 +      and opeSU: "openin (subtopology euclidean (frontier S)) U"
  2.2143 +      and opeSV: "openin (subtopology euclidean (frontier S)) V"
  2.2144 +      and "V \<noteq> {}" "\<not> U \<subseteq> V"
  2.2145 +  obtains g where "arc g" "pathstart g \<in> U" "pathfinish g \<in> V" "g ` {0<..<1} \<subseteq> S"
  2.2146 +proof -
  2.2147 +  have "S \<noteq> {}"
  2.2148 +    using opeSV \<open>V \<noteq> {}\<close> by (metis frontier_empty openin_subtopology_empty)
  2.2149 +  then obtain x where "x \<in> S" by auto
  2.2150 +  obtain g where "arc g" and g: "g ` {0..<1} \<subseteq> S" "pathstart g = x" "pathfinish g \<in> V"
  2.2151 +    using dense_accessible_frontier_points_connected [OF S \<open>x \<in> S\<close> \<open>V \<noteq> {}\<close> opeSV] by blast
  2.2152 +  obtain h where "arc h" and h: "h ` {0..<1} \<subseteq> S" "pathstart h = x" "pathfinish h \<in> U - {pathfinish g}"
  2.2153 +  proof (rule dense_accessible_frontier_points_connected [OF S \<open>x \<in> S\<close>])
  2.2154 +    show "U - {pathfinish g} \<noteq> {}"
  2.2155 +      using \<open>pathfinish g \<in> V\<close> \<open>\<not> U \<subseteq> V\<close> by blast
  2.2156 +    show "openin (subtopology euclidean (frontier S)) (U - {pathfinish g})"
  2.2157 +      by (simp add: opeSU openin_delete)
  2.2158 +  qed auto
  2.2159 +  obtain \<gamma> where "arc \<gamma>"
  2.2160 +             and \<gamma>: "path_image \<gamma> \<subseteq> path_image (reversepath h +++ g)"
  2.2161 +                    "pathstart \<gamma> = pathfinish h" "pathfinish \<gamma> = pathfinish g"
  2.2162 +  proof (rule path_contains_arc [of "(reversepath h +++ g)" "pathfinish h" "pathfinish g"])
  2.2163 +    show "path (reversepath h +++ g)"
  2.2164 +      by (simp add: \<open>arc g\<close> \<open>arc h\<close> \<open>pathstart g = x\<close> \<open>pathstart h = x\<close> arc_imp_path)
  2.2165 +    show "pathstart (reversepath h +++ g) = pathfinish h"
  2.2166 +         "pathfinish (reversepath h +++ g) = pathfinish g"
  2.2167 +      by auto
  2.2168 +    show "pathfinish h \<noteq> pathfinish g"
  2.2169 +      using \<open>pathfinish h \<in> U - {pathfinish g}\<close> by auto
  2.2170 +  qed auto
  2.2171 +  show ?thesis
  2.2172 +  proof
  2.2173 +    show "arc \<gamma>" "pathstart \<gamma> \<in> U" "pathfinish \<gamma> \<in> V"
  2.2174 +      using \<gamma> \<open>arc \<gamma>\<close> \<open>pathfinish h \<in> U - {pathfinish g}\<close>  \<open>pathfinish g \<in> V\<close> by auto
  2.2175 +    have "\<gamma> ` {0..1} - {\<gamma> 0, \<gamma> 1} \<subseteq> S"
  2.2176 +      using \<gamma> g h
  2.2177 +      apply (simp add: path_image_join)
  2.2178 +      apply (simp add: path_image_def pathstart_def pathfinish_def subset_iff image_def Bex_def)
  2.2179 +      by (metis linorder_neqE_linordered_idom not_less)
  2.2180 +    then show "\<gamma> ` {0<..<1} \<subseteq> S"
  2.2181 +      using \<open>arc h\<close> \<open>arc \<gamma>\<close>
  2.2182 +      by (metis arc_imp_simple_path path_image_def pathfinish_def pathstart_def simple_path_endless)
  2.2183 +  qed
  2.2184 +qed
  2.2185 +
  2.2186 +lemma dense_accessible_frontier_point_pairs:
  2.2187 +  fixes S :: "'a::{complete_space,real_normed_vector} set"
  2.2188 +  assumes S: "open S" "connected S"
  2.2189 +      and opeSU: "openin (subtopology euclidean (frontier S)) U"
  2.2190 +      and opeSV: "openin (subtopology euclidean (frontier S)) V"
  2.2191 +      and "U \<noteq> {}" "V \<noteq> {}" "U \<noteq> V"
  2.2192 +    obtains g where "arc g" "pathstart g \<in> U" "pathfinish g \<in> V" "g ` {0<..<1} \<subseteq> S"
  2.2193 +proof -
  2.2194 +  consider "\<not> U \<subseteq> V" | "\<not> V \<subseteq> U"
  2.2195 +    using \<open>U \<noteq> V\<close> by blast
  2.2196 +  then show ?thesis
  2.2197 +  proof cases
  2.2198 +    case 1 then show ?thesis
  2.2199 +      using assms dense_access_fp_aux [OF S opeSU opeSV] that by blast
  2.2200 +  next
  2.2201 +    case 2
  2.2202 +    obtain g where "arc g" and g: "pathstart g \<in> V" "pathfinish g \<in> U" "g ` {0<..<1} \<subseteq> S"
  2.2203 +      using assms dense_access_fp_aux [OF S opeSV opeSU] "2" by blast
  2.2204 +    show ?thesis
  2.2205 +    proof
  2.2206 +      show "arc (reversepath g)"
  2.2207 +        by (simp add: \<open>arc g\<close> arc_reversepath)
  2.2208 +      show "pathstart (reversepath g) \<in> U" "pathfinish (reversepath g) \<in> V"
  2.2209 +        using g by auto
  2.2210 +      show "reversepath g ` {0<..<1} \<subseteq> S"
  2.2211 +        using g by (auto simp: reversepath_def)
  2.2212 +    qed
  2.2213 +  qed
  2.2214 +qed
  2.2215 +
  2.2216 +end
     3.1 --- a/src/HOL/Analysis/Complex_Transcendental.thy	Thu Jan 05 15:03:37 2017 +0000
     3.2 +++ b/src/HOL/Analysis/Complex_Transcendental.thy	Thu Jan 05 16:03:23 2017 +0000
     3.3 @@ -3559,4 +3559,70 @@
     3.4    shows "S homotopy_eqv T \<Longrightarrow> simply_connected S \<longleftrightarrow> simply_connected T"
     3.5    by (simp add: simply_connected_eq_homotopic_circlemaps homotopy_eqv_homotopic_triviality)
     3.6  
     3.7 +
     3.8 +subsection\<open>Homeomorphism of simple closed curves to circles\<close>
     3.9 +
    3.10 +proposition homeomorphic_simple_path_image_circle:
    3.11 +  fixes a :: complex and \<gamma> :: "real \<Rightarrow> 'a::t2_space"
    3.12 +  assumes "simple_path \<gamma>" and loop: "pathfinish \<gamma> = pathstart \<gamma>" and "0 < r"
    3.13 +  shows "(path_image \<gamma>) homeomorphic sphere a r"
    3.14 +proof -
    3.15 +  have "homotopic_loops (path_image \<gamma>) \<gamma> \<gamma>"
    3.16 +    by (simp add: assms homotopic_loops_refl simple_path_imp_path)
    3.17 +  then have hom: "homotopic_with (\<lambda>h. True) (sphere 0 1) (path_image \<gamma>)
    3.18 +               (\<gamma> \<circ> (\<lambda>z. Arg z / (2*pi))) (\<gamma> \<circ> (\<lambda>z. Arg z / (2*pi)))"
    3.19 +    by (rule homotopic_loops_imp_homotopic_circlemaps)
    3.20 +  have "\<exists>g. homeomorphism (sphere 0 1) (path_image \<gamma>) (\<gamma> \<circ> (\<lambda>z. Arg z / (2*pi))) g"
    3.21 +  proof (rule homeomorphism_compact)
    3.22 +    show "continuous_on (sphere 0 1) (\<gamma> \<circ> (\<lambda>z. Arg z / (2*pi)))"
    3.23 +      using hom homotopic_with_imp_continuous by blast
    3.24 +    show "inj_on (\<gamma> \<circ> (\<lambda>z. Arg z / (2*pi))) (sphere 0 1)"
    3.25 +    proof
    3.26 +      fix x y
    3.27 +      assume xy: "x \<in> sphere 0 1" "y \<in> sphere 0 1"
    3.28 +         and eq: "(\<gamma> \<circ> (\<lambda>z. Arg z / (2*pi))) x = (\<gamma> \<circ> (\<lambda>z. Arg z / (2*pi))) y"
    3.29 +      then have "(Arg x / (2*pi)) = (Arg y / (2*pi))"
    3.30 +      proof -
    3.31 +        have "(Arg x / (2*pi)) \<in> {0..1}" "(Arg y / (2*pi)) \<in> {0..1}"
    3.32 +          using Arg_ge_0 Arg_lt_2pi dual_order.strict_iff_order by fastforce+
    3.33 +        with eq show ?thesis
    3.34 +          using \<open>simple_path \<gamma>\<close> Arg_lt_2pi unfolding simple_path_def o_def
    3.35 +          by (metis eq_divide_eq_1 not_less_iff_gr_or_eq)
    3.36 +      qed
    3.37 +      with xy show "x = y"
    3.38 +        by (metis Arg Arg_0 dist_0_norm divide_cancel_right dual_order.strict_iff_order mem_sphere)
    3.39 +    qed
    3.40 +    have "\<And>z. cmod z = 1 \<Longrightarrow> \<exists>x\<in>{0..1}. \<gamma> (Arg z / (2*pi)) = \<gamma> x"
    3.41 +       by (metis Arg_ge_0 Arg_lt_2pi atLeastAtMost_iff divide_less_eq_1 less_eq_real_def zero_less_mult_iff pi_gt_zero zero_le_divide_iff zero_less_numeral)
    3.42 +     moreover have "\<exists>z\<in>sphere 0 1. \<gamma> x = \<gamma> (Arg z / (2*pi))" if "0 \<le> x" "x \<le> 1" for x
    3.43 +     proof (cases "x=1")
    3.44 +       case True
    3.45 +       then show ?thesis
    3.46 +         apply (rule_tac x=1 in bexI)
    3.47 +         apply (metis loop Arg_of_real divide_eq_0_iff of_real_1 pathfinish_def pathstart_def \<open>0 \<le> x\<close>, auto)
    3.48 +         done
    3.49 +     next
    3.50 +       case False
    3.51 +       then have *: "(Arg (exp (\<i>*(2* of_real pi* of_real x))) / (2*pi)) = x"
    3.52 +         using that by (auto simp: Arg_exp divide_simps)
    3.53 +       show ?thesis
    3.54 +         by (rule_tac x="exp(ii* of_real(2*pi*x))" in bexI) (auto simp: *)
    3.55 +    qed
    3.56 +    ultimately show "(\<gamma> \<circ> (\<lambda>z. Arg z / (2*pi))) ` sphere 0 1 = path_image \<gamma>"
    3.57 +      by (auto simp: path_image_def image_iff)
    3.58 +    qed auto
    3.59 +    then have "path_image \<gamma> homeomorphic sphere (0::complex) 1"
    3.60 +      using homeomorphic_def homeomorphic_sym by blast
    3.61 +  also have "... homeomorphic sphere a r"
    3.62 +    by (simp add: assms homeomorphic_spheres)
    3.63 +  finally show ?thesis .
    3.64 +qed
    3.65 +
    3.66 +lemma homeomorphic_simple_path_images:
    3.67 +  fixes \<gamma>1 :: "real \<Rightarrow> 'a::t2_space" and \<gamma>2 :: "real \<Rightarrow> 'b::t2_space"
    3.68 +  assumes "simple_path \<gamma>1" and loop: "pathfinish \<gamma>1 = pathstart \<gamma>1"
    3.69 +  assumes "simple_path \<gamma>2" and loop: "pathfinish \<gamma>2 = pathstart \<gamma>2"
    3.70 +  shows "(path_image \<gamma>1) homeomorphic (path_image \<gamma>2)"
    3.71 +  by (meson assms homeomorphic_simple_path_image_circle homeomorphic_sym homeomorphic_trans loop pi_gt_zero)
    3.72 +
    3.73  end
     4.1 --- a/src/HOL/Analysis/Further_Topology.thy	Thu Jan 05 15:03:37 2017 +0000
     4.2 +++ b/src/HOL/Analysis/Further_Topology.thy	Thu Jan 05 16:03:23 2017 +0000
     4.3 @@ -3042,6 +3042,67 @@
     4.4    shows "0 < r \<Longrightarrow> \<not> simply_connected(sphere a r)"
     4.5  by (simp add: simply_connected_sphere_eq)
     4.6  
     4.7 +  
     4.8 +proposition simply_connected_punctured_convex:
     4.9 +  fixes a :: "'a::euclidean_space"
    4.10 +  assumes "convex S" and 3: "3 \<le> aff_dim S"
    4.11 +    shows "simply_connected(S - {a})"
    4.12 +proof (cases "a \<in> rel_interior S")
    4.13 +  case True
    4.14 +  then obtain e where "a \<in> S" "0 < e" and e: "cball a e \<inter> affine hull S \<subseteq> S"
    4.15 +    by (auto simp: rel_interior_cball)
    4.16 +  have con: "convex (cball a e \<inter> affine hull S)"
    4.17 +    by (simp add: convex_Int)
    4.18 +  have bo: "bounded (cball a e \<inter> affine hull S)"
    4.19 +    by (simp add: bounded_Int)
    4.20 +  have "affine hull S \<inter> interior (cball a e) \<noteq> {}"
    4.21 +    using \<open>0 < e\<close> \<open>a \<in> S\<close> hull_subset by fastforce
    4.22 +  then have "3 \<le> aff_dim (affine hull S \<inter> cball a e)"
    4.23 +    by (simp add: 3 aff_dim_convex_Int_nonempty_interior [OF convex_affine_hull])
    4.24 +  also have "... = aff_dim (cball a e \<inter> affine hull S)"
    4.25 +    by (simp add: Int_commute)
    4.26 +  finally have "3 \<le> aff_dim (cball a e \<inter> affine hull S)" .
    4.27 +  moreover have "rel_frontier (cball a e \<inter> affine hull S) homotopy_eqv S - {a}"
    4.28 +  proof (rule homotopy_eqv_rel_frontier_punctured_convex)
    4.29 +    show "a \<in> rel_interior (cball a e \<inter> affine hull S)"
    4.30 +      by (meson IntI Int_mono \<open>a \<in> S\<close> \<open>0 < e\<close> e \<open>cball a e \<inter> affine hull S \<subseteq> S\<close> ball_subset_cball centre_in_cball dual_order.strict_implies_order hull_inc hull_mono mem_rel_interior_ball)
    4.31 +    have "closed (cball a e \<inter> affine hull S)"
    4.32 +      by blast
    4.33 +    then show "rel_frontier (cball a e \<inter> affine hull S) \<subseteq> S"
    4.34 +      apply (simp add: rel_frontier_def)
    4.35 +      using e by blast
    4.36 +    show "S \<subseteq> affine hull (cball a e \<inter> affine hull S)"
    4.37 +      by (metis (no_types, lifting) IntI \<open>a \<in> S\<close> \<open>0 < e\<close> affine_hull_convex_Int_nonempty_interior centre_in_ball convex_affine_hull empty_iff hull_subset inf_commute interior_cball subsetCE subsetI)
    4.38 +    qed (auto simp: assms con bo)
    4.39 +  ultimately show ?thesis
    4.40 +    using homotopy_eqv_simple_connectedness simply_connected_sphere_gen [OF con bo]
    4.41 +    by blast
    4.42 +next
    4.43 +  case False
    4.44 +  show ?thesis
    4.45 +    apply (rule contractible_imp_simply_connected)
    4.46 +    apply (rule contractible_convex_tweak_boundary_points [OF \<open>convex S\<close>])
    4.47 +     apply (simp add: False rel_interior_subset subset_Diff_insert)
    4.48 +    by (meson Diff_subset closure_subset subset_trans)
    4.49 +qed
    4.50 +
    4.51 +corollary simply_connected_punctured_universe:
    4.52 +  fixes a :: "'a::euclidean_space"
    4.53 +  assumes "3 \<le> DIM('a)"
    4.54 +  shows "simply_connected(- {a})"
    4.55 +proof -
    4.56 +  have [simp]: "affine hull cball a 1 = UNIV"
    4.57 +    apply auto
    4.58 +    by (metis UNIV_I aff_dim_cball aff_dim_lt_full zero_less_one not_less_iff_gr_or_eq)
    4.59 +  have "simply_connected (rel_frontier (cball a 1)) = simply_connected (affine hull cball a 1 - {a})"
    4.60 +    apply (rule homotopy_eqv_simple_connectedness)
    4.61 +    apply (rule homotopy_eqv_rel_frontier_punctured_affine_hull)
    4.62 +      apply (force simp: rel_interior_cball intro: homotopy_eqv_simple_connectedness homotopy_eqv_rel_frontier_punctured_affine_hull)+
    4.63 +    done
    4.64 +  then show ?thesis
    4.65 +    using simply_connected_sphere [of a 1, OF assms] by (auto simp: Compl_eq_Diff_UNIV)
    4.66 +qed
    4.67 +
    4.68  
    4.69  subsection\<open>The power, squaring and exponential functions as covering maps\<close>
    4.70  
     5.1 --- a/src/HOL/Analysis/Path_Connected.thy	Thu Jan 05 15:03:37 2017 +0000
     5.2 +++ b/src/HOL/Analysis/Path_Connected.thy	Thu Jan 05 16:03:23 2017 +0000
     5.3 @@ -5302,6 +5302,106 @@
     5.4      using compact_eq_bounded_closed locally_mono by blast
     5.5  qed
     5.6  
     5.7 +lemma locally_compact_openin_Un:
     5.8 +  fixes S :: "'a::euclidean_space set"
     5.9 +  assumes LCS: "locally compact S" and LCT:"locally compact T"
    5.10 +      and opS: "openin (subtopology euclidean (S \<union> T)) S"
    5.11 +      and opT: "openin (subtopology euclidean (S \<union> T)) T"
    5.12 +    shows "locally compact (S \<union> T)"
    5.13 +proof -
    5.14 +  have "\<exists>e>0. closed (cball x e \<inter> (S \<union> T))" if "x \<in> S" for x
    5.15 +  proof -
    5.16 +    obtain e1 where "e1 > 0" and e1: "closed (cball x e1 \<inter> S)"
    5.17 +      using LCS \<open>x \<in> S\<close> unfolding locally_compact_Int_cball by blast
    5.18 +    moreover obtain e2 where "e2 > 0" and e2: "cball x e2 \<inter> (S \<union> T) \<subseteq> S"
    5.19 +      by (meson \<open>x \<in> S\<close> opS openin_contains_cball)
    5.20 +    then have "cball x e2 \<inter> (S \<union> T) = cball x e2 \<inter> S"
    5.21 +      by force
    5.22 +    ultimately show ?thesis
    5.23 +      apply (rule_tac x="min e1 e2" in exI)
    5.24 +      apply (auto simp: cball_min_Int \<open>e2 > 0\<close> inf_assoc closed_Int)
    5.25 +      by (metis closed_Int closed_cball inf_left_commute)
    5.26 +  qed
    5.27 +  moreover have "\<exists>e>0. closed (cball x e \<inter> (S \<union> T))" if "x \<in> T" for x
    5.28 +  proof -
    5.29 +    obtain e1 where "e1 > 0" and e1: "closed (cball x e1 \<inter> T)"
    5.30 +      using LCT \<open>x \<in> T\<close> unfolding locally_compact_Int_cball by blast
    5.31 +    moreover obtain e2 where "e2 > 0" and e2: "cball x e2 \<inter> (S \<union> T) \<subseteq> T"
    5.32 +      by (meson \<open>x \<in> T\<close> opT openin_contains_cball)
    5.33 +    then have "cball x e2 \<inter> (S \<union> T) = cball x e2 \<inter> T"
    5.34 +      by force
    5.35 +    ultimately show ?thesis
    5.36 +      apply (rule_tac x="min e1 e2" in exI)
    5.37 +      apply (auto simp: cball_min_Int \<open>e2 > 0\<close> inf_assoc closed_Int)
    5.38 +      by (metis closed_Int closed_cball inf_left_commute)
    5.39 +  qed
    5.40 +  ultimately show ?thesis
    5.41 +    by (force simp: locally_compact_Int_cball)
    5.42 +qed
    5.43 +
    5.44 +lemma locally_compact_closedin_Un:
    5.45 +  fixes S :: "'a::euclidean_space set"
    5.46 +  assumes LCS: "locally compact S" and LCT:"locally compact T"
    5.47 +      and clS: "closedin (subtopology euclidean (S \<union> T)) S"
    5.48 +      and clT: "closedin (subtopology euclidean (S \<union> T)) T"
    5.49 +    shows "locally compact (S \<union> T)"
    5.50 +proof -
    5.51 +  have "\<exists>e>0. closed (cball x e \<inter> (S \<union> T))" if "x \<in> S" "x \<in> T" for x
    5.52 +  proof -
    5.53 +    obtain e1 where "e1 > 0" and e1: "closed (cball x e1 \<inter> S)"
    5.54 +      using LCS \<open>x \<in> S\<close> unfolding locally_compact_Int_cball by blast
    5.55 +    moreover
    5.56 +    obtain e2 where "e2 > 0" and e2: "closed (cball x e2 \<inter> T)"
    5.57 +      using LCT \<open>x \<in> T\<close> unfolding locally_compact_Int_cball by blast
    5.58 +    ultimately show ?thesis
    5.59 +      apply (rule_tac x="min e1 e2" in exI)
    5.60 +      apply (auto simp: cball_min_Int \<open>e2 > 0\<close> inf_assoc closed_Int Int_Un_distrib)
    5.61 +      by (metis closed_Int closed_Un closed_cball inf_left_commute)
    5.62 +  qed
    5.63 +  moreover
    5.64 +  have "\<exists>e>0. closed (cball x e \<inter> (S \<union> T))" if x: "x \<in> S" "x \<notin> T" for x
    5.65 +  proof -
    5.66 +    obtain e1 where "e1 > 0" and e1: "closed (cball x e1 \<inter> S)"
    5.67 +      using LCS \<open>x \<in> S\<close> unfolding locally_compact_Int_cball by blast
    5.68 +    moreover
    5.69 +    obtain e2 where "e2>0" and "cball x e2 \<inter> (S \<union> T) \<subseteq> S - T"
    5.70 +      using clT x by (fastforce simp: openin_contains_cball closedin_def)
    5.71 +    then have "closed (cball x e2 \<inter> T)"
    5.72 +    proof -
    5.73 +      have "{} = T - (T - cball x e2)"
    5.74 +        using Diff_subset Int_Diff \<open>cball x e2 \<inter> (S \<union> T) \<subseteq> S - T\<close> by auto
    5.75 +      then show ?thesis
    5.76 +        by (simp add: Diff_Diff_Int inf_commute)
    5.77 +    qed
    5.78 +    ultimately show ?thesis
    5.79 +      apply (rule_tac x="min e1 e2" in exI)
    5.80 +      apply (auto simp: cball_min_Int \<open>e2 > 0\<close> inf_assoc closed_Int Int_Un_distrib)
    5.81 +      by (metis closed_Int closed_Un closed_cball inf_left_commute)
    5.82 +  qed
    5.83 +  moreover
    5.84 +  have "\<exists>e>0. closed (cball x e \<inter> (S \<union> T))" if x: "x \<notin> S" "x \<in> T" for x
    5.85 +  proof -
    5.86 +    obtain e1 where "e1 > 0" and e1: "closed (cball x e1 \<inter> T)"
    5.87 +      using LCT \<open>x \<in> T\<close> unfolding locally_compact_Int_cball by blast
    5.88 +    moreover
    5.89 +    obtain e2 where "e2>0" and "cball x e2 \<inter> (S \<union> T) \<subseteq> S \<union> T - S"
    5.90 +      using clS x by (fastforce simp: openin_contains_cball closedin_def)
    5.91 +    then have "closed (cball x e2 \<inter> S)"
    5.92 +      by (metis Diff_disjoint Int_empty_right closed_empty inf.left_commute inf.orderE inf_sup_absorb)
    5.93 +    ultimately show ?thesis
    5.94 +      apply (rule_tac x="min e1 e2" in exI)
    5.95 +      apply (auto simp: cball_min_Int \<open>e2 > 0\<close> inf_assoc closed_Int Int_Un_distrib)
    5.96 +      by (metis closed_Int closed_Un closed_cball inf_left_commute)
    5.97 +  qed
    5.98 +  ultimately show ?thesis
    5.99 +    by (auto simp: locally_compact_Int_cball)
   5.100 +qed
   5.101 +
   5.102 +lemma locally_compact_Times:
   5.103 +  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
   5.104 +  shows "\<lbrakk>locally compact S; locally compact T\<rbrakk> \<Longrightarrow> locally compact (S \<times> T)"
   5.105 +  by (auto simp: compact_Times locally_Times)
   5.106 +
   5.107  subsection\<open>Important special cases of local connectedness and path connectedness\<close>
   5.108  
   5.109  lemma locally_connected_1: