src/HOL/Analysis/Arcwise_Connected.thy
 author nipkow Sat Dec 29 15:43:53 2018 +0100 (6 months ago) changeset 69529 4ab9657b3257 parent 69517 dc20f278e8f3 child 69652 3417a8f154eb permissions -rw-r--r--
capitalize proper names in lemma names
```     1 (*  Title:      HOL/Analysis/Arcwise_Connected.thy
```
```     2     Authors:    LC Paulson, based on material from HOL Light
```
```     3 *)
```
```     4
```
```     5 section \<open>Arcwise-Connected Sets\<close>
```
```     6
```
```     7 theory Arcwise_Connected
```
```     8 imports Path_Connected Ordered_Euclidean_Space "HOL-Computational_Algebra.Primes"
```
```     9 begin
```
```    10
```
```    11 subsection%important \<open>The Brouwer reduction theorem\<close>
```
```    12
```
```    13 theorem%important Brouwer_reduction_theorem_gen:
```
```    14   fixes S :: "'a::euclidean_space set"
```
```    15   assumes "closed S" "\<phi> S"
```
```    16       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)"
```
```    17   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)"
```
```    18 proof%unimportant -
```
```    19   obtain B :: "nat \<Rightarrow> 'a set"
```
```    20     where "inj B" "\<And>n. open(B n)" and open_cov: "\<And>S. open S \<Longrightarrow> \<exists>K. S = \<Union>(B ` K)"
```
```    21       by (metis Setcompr_eq_image that univ_second_countable_sequence)
```
```    22   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) = {}
```
```    23                                         then SOME U. U \<subseteq> a \<and> closed U \<and> \<phi> U \<and> U \<inter> (B n) = {}
```
```    24                                         else a)"
```
```    25   have [simp]: "A 0 = S"
```
```    26     by (simp add: A_def)
```
```    27   have ASuc: "A(Suc n) = (if \<exists>U. U \<subseteq> A n \<and> closed U \<and> \<phi> U \<and> U \<inter> (B n) = {}
```
```    28                           then SOME U. U \<subseteq> A n \<and> closed U \<and> \<phi> U \<and> U \<inter> (B n) = {}
```
```    29                           else A n)" for n
```
```    30     by (auto simp: A_def)
```
```    31   have sub: "\<And>n. A(Suc n) \<subseteq> A n"
```
```    32     by (auto simp: ASuc dest!: someI_ex)
```
```    33   have subS: "A n \<subseteq> S" for n
```
```    34     by (induction n) (use sub in auto)
```
```    35   have clo: "closed (A n) \<and> \<phi> (A n)" for n
```
```    36     by (induction n) (auto simp: assms ASuc dest!: someI_ex)
```
```    37   show ?thesis
```
```    38   proof
```
```    39     show "\<Inter>range A \<subseteq> S"
```
```    40       using \<open>\<And>n. A n \<subseteq> S\<close> by blast
```
```    41     show "closed (\<Inter>(A ` UNIV))"
```
```    42       using clo by blast
```
```    43     show "\<phi> (\<Inter>(A ` UNIV))"
```
```    44       by (simp add: clo \<phi> sub)
```
```    45     show "\<not> U \<subset> \<Inter>(A ` UNIV)" if "U \<subseteq> S" "closed U" "\<phi> U" for U
```
```    46     proof -
```
```    47       have "\<exists>y. x \<notin> A y" if "x \<notin> U" and Usub: "U \<subseteq> (\<Inter>x. A x)" for x
```
```    48       proof -
```
```    49         obtain e where "e > 0" and e: "ball x e \<subseteq> -U"
```
```    50           using \<open>closed U\<close> \<open>x \<notin> U\<close> openE [of "-U"] by blast
```
```    51         moreover obtain K where K: "ball x e = \<Union>(B ` K)"
```
```    52           using open_cov [of "ball x e"] by auto
```
```    53         ultimately have "\<Union>(B ` K) \<subseteq> -U"
```
```    54           by blast
```
```    55         have "K \<noteq> {}"
```
```    56           using \<open>0 < e\<close> \<open>ball x e = \<Union>(B ` K)\<close> by auto
```
```    57         then obtain n where "n \<in> K" "x \<in> B n"
```
```    58           by (metis K UN_E \<open>0 < e\<close> centre_in_ball)
```
```    59         then have "U \<inter> B n = {}"
```
```    60           using K e by auto
```
```    61         show ?thesis
```
```    62         proof (cases "\<exists>U\<subseteq>A n. closed U \<and> \<phi> U \<and> U \<inter> B n = {}")
```
```    63           case True
```
```    64           then show ?thesis
```
```    65             apply (rule_tac x="Suc n" in exI)
```
```    66             apply (simp add: ASuc)
```
```    67             apply (erule someI2_ex)
```
```    68             using \<open>x \<in> B n\<close> by blast
```
```    69         next
```
```    70           case False
```
```    71           then show ?thesis
```
```    72             by (meson Inf_lower Usub \<open>U \<inter> B n = {}\<close> \<open>\<phi> U\<close> \<open>closed U\<close> range_eqI subset_trans)
```
```    73         qed
```
```    74       qed
```
```    75       with that show ?thesis
```
```    76         by (meson Inter_iff psubsetE rangeI subsetI)
```
```    77     qed
```
```    78   qed
```
```    79 qed
```
```    80
```
```    81 corollary%important Brouwer_reduction_theorem:
```
```    82   fixes S :: "'a::euclidean_space set"
```
```    83   assumes "compact S" "\<phi> S" "S \<noteq> {}"
```
```    84       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)"
```
```    85   obtains T where "T \<subseteq> S" "compact T" "T \<noteq> {}" "\<phi> T"
```
```    86                   "\<And>U. \<lbrakk>U \<subseteq> S; closed U; U \<noteq> {}; \<phi> U\<rbrakk> \<Longrightarrow> \<not> (U \<subset> T)"
```
```    87 proof%unimportant (rule Brouwer_reduction_theorem_gen [of S "\<lambda>T. T \<noteq> {} \<and> T \<subseteq> S \<and> \<phi> T"])
```
```    88   fix F
```
```    89   assume cloF: "\<And>n. closed (F n)"
```
```    90      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"
```
```    91   show "\<Inter>(F ` UNIV) \<noteq> {} \<and> \<Inter>(F ` UNIV) \<subseteq> S \<and> \<phi> (\<Inter>(F ` UNIV))"
```
```    92   proof (intro conjI)
```
```    93     show "\<Inter>(F ` UNIV) \<noteq> {}"
```
```    94       apply (rule compact_nest)
```
```    95       apply (meson F cloF \<open>compact S\<close> seq_compact_closed_subset seq_compact_eq_compact)
```
```    96        apply (simp add: F)
```
```    97       by (meson Fsub lift_Suc_antimono_le)
```
```    98     show " \<Inter>(F ` UNIV) \<subseteq> S"
```
```    99       using F by blast
```
```   100     show "\<phi> (\<Inter>(F ` UNIV))"
```
```   101       by (metis F Fsub \<phi> \<open>compact S\<close> cloF closed_Int_compact inf.orderE)
```
```   102   qed
```
```   103 next
```
```   104   show "S \<noteq> {} \<and> S \<subseteq> S \<and> \<phi> S"
```
```   105     by (simp add: assms)
```
```   106 qed (meson assms compact_imp_closed seq_compact_closed_subset seq_compact_eq_compact)+
```
```   107
```
```   108
```
```   109 subsection%important\<open>Arcwise Connections\<close>(*FIX ME this subsection is empty(?) *)
```
```   110
```
```   111 subsection%important\<open>Density of points with dyadic rational coordinates\<close>
```
```   112
```
```   113 proposition%important closure_dyadic_rationals:
```
```   114     "closure (\<Union>k. \<Union>f \<in> Basis \<rightarrow> \<int>.
```
```   115                    { \<Sum>i :: 'a :: euclidean_space \<in> Basis. (f i / 2^k) *\<^sub>R i }) = UNIV"
```
```   116 proof%unimportant -
```
```   117   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
```
```   118   proof (clarsimp simp: closure_approachable)
```
```   119     fix e::real
```
```   120     assume "e > 0"
```
```   121     then obtain k where k: "(1/2)^k < e/DIM('a)"
```
```   122       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)
```
```   123     have "dist (\<Sum>i\<in>Basis. (real_of_int \<lfloor>2^k*(x \<bullet> i)\<rfloor> / 2^k) *\<^sub>R i) x =
```
```   124           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)"
```
```   125       by (simp add: euclidean_representation)
```
```   126     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))"
```
```   127       by (simp add: dist_norm sum_subtractf)
```
```   128     also have "... \<le> DIM('a)*((1/2)^k)"
```
```   129     proof (rule sum_norm_bound, simp add: algebra_simps)
```
```   130       fix i::'a
```
```   131       assume "i \<in> Basis"
```
```   132       then have "norm ((real_of_int \<lfloor>x \<bullet> i*2^k\<rfloor> / 2^k) *\<^sub>R i - (x \<bullet> i) *\<^sub>R i) =
```
```   133                  \<bar>real_of_int \<lfloor>x \<bullet> i*2^k\<rfloor> / 2^k - x \<bullet> i\<bar>"
```
```   134         by (simp add: scaleR_left_diff_distrib [symmetric])
```
```   135       also have "... \<le> (1/2) ^ k"
```
```   136         by (simp add: divide_simps) linarith
```
```   137       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" .
```
```   138     qed
```
```   139     also have "... < DIM('a)*(e/DIM('a))"
```
```   140       using DIM_positive k linordered_comm_semiring_strict_class.comm_mult_strict_left_mono of_nat_0_less_iff by blast
```
```   141     also have "... = e"
```
```   142       by simp
```
```   143     finally have "dist (\<Sum>i\<in>Basis. (\<lfloor>2^k*(x \<bullet> i)\<rfloor> / 2^k) *\<^sub>R i) x < e" .
```
```   144     then
```
```   145     show "\<exists>k. \<exists>f \<in> Basis \<rightarrow> \<int>. dist (\<Sum>b\<in>Basis. (f b / 2^k) *\<^sub>R b) x < e"
```
```   146       apply (rule_tac x=k in exI)
```
```   147       apply (rule_tac x="\<lambda>i. of_int (floor (2^k*(x \<bullet> i)))" in bexI)
```
```   148        apply auto
```
```   149       done
```
```   150   qed
```
```   151   then show ?thesis by auto
```
```   152 qed
```
```   153
```
```   154 corollary%important closure_rational_coordinates:
```
```   155     "closure (\<Union>f \<in> Basis \<rightarrow> \<rat>. { \<Sum>i :: 'a :: euclidean_space \<in> Basis. f i *\<^sub>R i }) = UNIV"
```
```   156 proof%unimportant -
```
```   157   have *: "(\<Union>k. \<Union>f \<in> Basis \<rightarrow> \<int>. { \<Sum>i::'a \<in> Basis. (f i / 2^k) *\<^sub>R i })
```
```   158            \<subseteq> (\<Union>f \<in> Basis \<rightarrow> \<rat>. { \<Sum>i \<in> Basis. f i *\<^sub>R i })"
```
```   159   proof clarsimp
```
```   160     fix k and f :: "'a \<Rightarrow> real"
```
```   161     assume f: "f \<in> Basis \<rightarrow> \<int>"
```
```   162     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)"
```
```   163       apply (rule_tac x="\<lambda>i. f i / 2^k" in bexI)
```
```   164       using Ints_subset_Rats f by auto
```
```   165   qed
```
```   166   show ?thesis
```
```   167     using closure_dyadic_rationals closure_mono [OF *] by blast
```
```   168 qed
```
```   169
```
```   170 lemma%unimportant closure_dyadic_rationals_in_convex_set:
```
```   171    "\<lbrakk>convex S; interior S \<noteq> {}\<rbrakk>
```
```   172         \<Longrightarrow> closure(S \<inter>
```
```   173                     (\<Union>k. \<Union>f \<in> Basis \<rightarrow> \<int>.
```
```   174                    { \<Sum>i :: 'a :: euclidean_space \<in> Basis. (f i / 2^k) *\<^sub>R i })) =
```
```   175             closure S"
```
```   176   by (simp add: closure_dyadic_rationals closure_convex_Int_superset)
```
```   177
```
```   178 lemma%unimportant closure_rationals_in_convex_set:
```
```   179    "\<lbrakk>convex S; interior S \<noteq> {}\<rbrakk>
```
```   180     \<Longrightarrow> closure(S \<inter> (\<Union>f \<in> Basis \<rightarrow> \<rat>. { \<Sum>i :: 'a :: euclidean_space \<in> Basis. f i *\<^sub>R i })) =
```
```   181         closure S"
```
```   182   by (simp add: closure_rational_coordinates closure_convex_Int_superset)
```
```   183
```
```   184
```
```   185 text\<open> Every path between distinct points contains an arc, and hence
```
```   186 path connection is equivalent to arcwise connection for distinct points.
```
```   187 The proof is based on Whyburn's "Topological Analysis".\<close>
```
```   188
```
```   189 lemma%important closure_dyadic_rationals_in_convex_set_pos_1:
```
```   190   fixes S :: "real set"
```
```   191   assumes "convex S" and intnz: "interior S \<noteq> {}" and pos: "\<And>x. x \<in> S \<Longrightarrow> 0 \<le> x"
```
```   192     shows "closure(S \<inter> (\<Union>k m. {of_nat m / 2^k})) = closure S"
```
```   193 proof%unimportant -
```
```   194   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"
```
```   195     using that by (force simp: Ints_def zero_le_divide_iff power_le_zero_eq dest: pos zero_le_imp_eq_int)
```
```   196   then have "S \<inter> (\<Union>k m. {real m / 2^k}) = S \<inter>
```
```   197              (\<Union>k. \<Union>f\<in>Basis \<rightarrow> \<int>. {\<Sum>i\<in>Basis. (f i / 2^k) *\<^sub>R i})"
```
```   198     by force
```
```   199   then show ?thesis
```
```   200     using closure_dyadic_rationals_in_convex_set [OF \<open>convex S\<close> intnz] by simp
```
```   201 qed
```
```   202
```
```   203
```
```   204 definition%important dyadics :: "'a::field_char_0 set" where "dyadics \<equiv> \<Union>k m. {of_nat m / 2^k}"
```
```   205
```
```   206 lemma%unimportant real_in_dyadics [simp]: "real m \<in> dyadics"
```
```   207   apply (simp add: dyadics_def)
```
```   208   by (metis divide_numeral_1 numeral_One power_0)
```
```   209
```
```   210 lemma%unimportant nat_neq_4k1: "of_nat m \<noteq> (4 * of_nat k + 1) / (2 * 2^n :: 'a::field_char_0)"
```
```   211 proof
```
```   212   assume "of_nat m = (4 * of_nat k + 1) / (2 * 2^n :: 'a)"
```
```   213   then have "of_nat (m * (2 * 2^n)) = (of_nat (Suc (4 * k)) :: 'a)"
```
```   214     by (simp add: divide_simps)
```
```   215   then have "m * (2 * 2^n) = Suc (4 * k)"
```
```   216     using of_nat_eq_iff by blast
```
```   217   then have "odd (m * (2 * 2^n))"
```
```   218     by simp
```
```   219   then show False
```
```   220     by simp
```
```   221 qed
```
```   222
```
```   223 lemma%important nat_neq_4k3: "of_nat m \<noteq> (4 * of_nat k + 3) / (2 * 2^n :: 'a::field_char_0)"
```
```   224 proof%unimportant
```
```   225   assume "of_nat m = (4 * of_nat k + 3) / (2 * 2^n :: 'a)"
```
```   226   then have "of_nat (m * (2 * 2^n)) = (of_nat (4 * k + 3) :: 'a)"
```
```   227     by (simp add: divide_simps)
```
```   228   then have "m * (2 * 2^n) = (4 * k) + 3"
```
```   229     using of_nat_eq_iff by blast
```
```   230   then have "odd (m * (2 * 2^n))"
```
```   231     by simp
```
```   232   then show False
```
```   233     by simp
```
```   234 qed
```
```   235
```
```   236 lemma%important iff_4k:
```
```   237   assumes "r = real k" "odd k"
```
```   238     shows "(4 * real m + r) / (2 * 2^n) = (4 * real m' + r) / (2 * 2 ^ n') \<longleftrightarrow> m=m' \<and> n=n'"
```
```   239 proof%unimportant -
```
```   240   { assume "(4 * real m + r) / (2 * 2^n) = (4 * real m' + r) / (2 * 2 ^ n')"
```
```   241     then have "real ((4 * m + k) * (2 * 2 ^ n')) = real ((4 * m' + k) * (2 * 2^n))"
```
```   242       using assms by (auto simp: field_simps)
```
```   243     then have "(4 * m + k) * (2 * 2 ^ n') = (4 * m' + k) * (2 * 2^n)"
```
```   244       using of_nat_eq_iff by blast
```
```   245     then have "(4 * m + k) * (2 ^ n') = (4 * m' + k) * (2^n)"
```
```   246       by linarith
```
```   247     then obtain "4*m + k = 4*m' + k" "n=n'"
```
```   248       apply (rule prime_power_cancel2 [OF two_is_prime_nat])
```
```   249       using assms by auto
```
```   250     then have "m=m'" "n=n'"
```
```   251       by auto
```
```   252   }
```
```   253   then show ?thesis by blast
```
```   254 qed
```
```   255
```
```   256 lemma%important neq_4k1_k43: "(4 * real m + 1) / (2 * 2^n) \<noteq> (4 * real m' + 3) / (2 * 2 ^ n')"
```
```   257 proof%unimportant
```
```   258   assume "(4 * real m + 1) / (2 * 2^n) = (4 * real m' + 3) / (2 * 2 ^ n')"
```
```   259   then have "real (Suc (4 * m) * (2 * 2 ^ n')) = real ((4 * m' + 3) * (2 * 2^n))"
```
```   260     by (auto simp: field_simps)
```
```   261   then have "Suc (4 * m) * (2 * 2 ^ n') = (4 * m' + 3) * (2 * 2^n)"
```
```   262     using of_nat_eq_iff by blast
```
```   263   then have "Suc (4 * m) * (2 ^ n') = (4 * m' + 3) * (2^n)"
```
```   264     by linarith
```
```   265   then have "Suc (4 * m) = (4 * m' + 3)"
```
```   266     by (rule prime_power_cancel2 [OF two_is_prime_nat]) auto
```
```   267   then have "1 + 2 * m' = 2 * m"
```
```   268     using \<open>Suc (4 * m) = 4 * m' + 3\<close> by linarith
```
```   269   then show False
```
```   270     using even_Suc by presburger
```
```   271 qed
```
```   272
```
```   273 lemma%important dyadic_413_cases:
```
```   274   obtains "(of_nat m::'a::field_char_0) / 2^k \<in> Nats"
```
```   275   | m' k' where "k' < k" "(of_nat m:: 'a) / 2^k = of_nat (4*m' + 1) / 2^Suc k'"
```
```   276   | m' k' where "k' < k" "(of_nat m:: 'a) / 2^k = of_nat (4*m' + 3) / 2^Suc k'"
```
```   277 proof%unimportant (cases "m>0")
```
```   278   case False
```
```   279   then have "m=0" by simp
```
```   280   with that show ?thesis by auto
```
```   281 next
```
```   282   case True
```
```   283   obtain k' m' where m': "odd m'" and k': "m = m' * 2^k'"
```
```   284     using prime_power_canonical [OF two_is_prime_nat True] by blast
```
```   285   then obtain q r where q: "m' = 4*q + r" and r: "r < 4"
```
```   286     by (metis not_add_less2 split_div zero_neq_numeral)
```
```   287   show ?thesis
```
```   288   proof (cases "k \<le> k'")
```
```   289     case True
```
```   290     have "(of_nat m:: 'a) / 2^k = of_nat m' * (2 ^ k' / 2^k)"
```
```   291       using k' by (simp add: field_simps)
```
```   292     also have "... = (of_nat m'::'a) * 2 ^ (k'-k)"
```
```   293       using k' True by (simp add: power_diff)
```
```   294     also have "... \<in> \<nat>"
```
```   295       by (metis Nats_mult of_nat_in_Nats of_nat_numeral of_nat_power)
```
```   296     finally show ?thesis by (auto simp: that)
```
```   297   next
```
```   298     case False
```
```   299     then obtain kd where kd: "Suc kd = k - k'"
```
```   300       using Suc_diff_Suc not_less by blast
```
```   301     have "(of_nat m:: 'a) / 2^k = of_nat m' * (2 ^ k' / 2^k)"
```
```   302       using k' by (simp add: field_simps)
```
```   303     also have "... = (of_nat m'::'a) / 2 ^ (k-k')"
```
```   304       using k' False by (simp add: power_diff)
```
```   305     also have "... = ((of_nat r + 4 * of_nat q)::'a) / 2 ^ (k-k')"
```
```   306       using q by force
```
```   307     finally have meq: "(of_nat m:: 'a) / 2^k = (of_nat r + 4 * of_nat q) / 2 ^ (k - k')" .
```
```   308     have "r \<noteq> 0" "r \<noteq> 2"
```
```   309       using q m' by presburger+
```
```   310     with r consider "r = 1" | "r = 3"
```
```   311       by linarith
```
```   312     then show ?thesis
```
```   313     proof cases
```
```   314       assume "r = 1"
```
```   315       with meq kd that(2) [of kd q] show ?thesis
```
```   316         by simp
```
```   317     next
```
```   318       assume "r = 3"
```
```   319       with meq kd that(3) [of kd q]  show ?thesis
```
```   320         by simp
```
```   321     qed
```
```   322   qed
```
```   323 qed
```
```   324
```
```   325
```
```   326 lemma%important dyadics_iff:
```
```   327    "(dyadics :: 'a::field_char_0 set) =
```
```   328     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})"
```
```   329            (is "_ = ?rhs")
```
```   330 proof%unimportant
```
```   331   show "dyadics \<subseteq> ?rhs"
```
```   332     unfolding dyadics_def
```
```   333     apply clarify
```
```   334     apply (rule dyadic_413_cases, force+)
```
```   335     done
```
```   336 next
```
```   337   show "?rhs \<subseteq> dyadics"
```
```   338     apply (clarsimp simp: dyadics_def Nats_def simp del: power_Suc)
```
```   339     apply (intro conjI subsetI)
```
```   340     apply (auto simp del: power_Suc)
```
```   341       apply (metis divide_numeral_1 numeral_One power_0)
```
```   342      apply (metis of_nat_Suc of_nat_mult of_nat_numeral)
```
```   343     by (metis of_nat_add of_nat_mult of_nat_numeral)
```
```   344 qed
```
```   345
```
```   346
```
```   347 function (domintros) dyad_rec :: "[nat \<Rightarrow> 'a, 'a\<Rightarrow>'a, 'a\<Rightarrow>'a, real] \<Rightarrow> 'a" where
```
```   348     "dyad_rec b l r (real m) = b m"
```
```   349   | "dyad_rec b l r ((4 * real m + 1) / 2 ^ (Suc n)) = l (dyad_rec b l r ((2*m + 1) / 2^n))"
```
```   350   | "dyad_rec b l r ((4 * real m + 3) / 2 ^ (Suc n)) = r (dyad_rec b l r ((2*m + 1) / 2^n))"
```
```   351   | "x \<notin> dyadics \<Longrightarrow> dyad_rec b l r x = undefined"
```
```   352   using iff_4k [of _ 1] iff_4k [of _ 3]
```
```   353          apply (simp_all add: nat_neq_4k1 nat_neq_4k3 neq_4k1_k43, atomize_elim)
```
```   354      apply (fastforce simp add: dyadics_iff Nats_def field_simps)+
```
```   355   done
```
```   356
```
```   357 lemma%unimportant dyadics_levels: "dyadics = (\<Union>K. \<Union>k<K. \<Union> m. {of_nat m / 2^k})"
```
```   358   unfolding dyadics_def by auto
```
```   359
```
```   360 lemma%important dyad_rec_level_termination:
```
```   361   assumes "k < K"
```
```   362   shows "dyad_rec_dom(b, l, r, real m / 2^k)"
```
```   363   using assms
```
```   364 proof%unimportant (induction K arbitrary: k m)
```
```   365   case 0
```
```   366   then show ?case by auto
```
```   367 next
```
```   368   case (Suc K)
```
```   369   then consider "k = K" | "k < K"
```
```   370     using less_antisym by blast
```
```   371   then show ?case
```
```   372   proof cases
```
```   373     assume "k = K"
```
```   374     show ?case
```
```   375     proof (rule dyadic_413_cases [of m k, where 'a=real])
```
```   376       show "real m / 2^k \<in> \<nat> \<Longrightarrow> dyad_rec_dom (b, l, r, real m / 2^k)"
```
```   377         by (force simp: Nats_def nat_neq_4k1 nat_neq_4k3 intro: dyad_rec.domintros)
```
```   378       show ?case if "k' < k" and eq: "real m / 2^k = real (4 * m' + 1) / 2^Suc k'" for m' k'
```
```   379       proof -
```
```   380         have "dyad_rec_dom (b, l, r, (4 * real m' + 1) / 2^Suc k')"
```
```   381         proof (rule dyad_rec.domintros)
```
```   382           fix m n
```
```   383           assume "(4 * real m' + 1) / (2 * 2 ^ k') = (4 * real m + 1) / (2 * 2^n)"
```
```   384           then have "m' = m" "k' = n" using iff_4k [of _ 1]
```
```   385             by auto
```
```   386           have "dyad_rec_dom (b, l, r, real (2 * m + 1) / 2 ^ k')"
```
```   387             using Suc.IH \<open>k = K\<close> \<open>k' < k\<close> by blast
```
```   388           then show "dyad_rec_dom (b, l, r, (2 * real m + 1) / 2^n)"
```
```   389             using \<open>k' = n\<close> by (auto simp: algebra_simps)
```
```   390         next
```
```   391           fix m n
```
```   392           assume "(4 * real m' + 1) / (2 * 2 ^ k') = (4 * real m + 3) / (2 * 2^n)"
```
```   393           then have "False"
```
```   394             by (metis neq_4k1_k43)
```
```   395           then show "dyad_rec_dom (b, l, r, (2 * real m + 1) / 2^n)" ..
```
```   396         qed
```
```   397         then show ?case by (simp add: eq add_ac)
```
```   398       qed
```
```   399       show ?case if "k' < k" and eq: "real m / 2^k = real (4 * m' + 3) / 2^Suc k'" for m' k'
```
```   400       proof -
```
```   401         have "dyad_rec_dom (b, l, r, (4 * real m' + 3) / 2^Suc k')"
```
```   402         proof (rule dyad_rec.domintros)
```
```   403           fix m n
```
```   404           assume "(4 * real m' + 3) / (2 * 2 ^ k') = (4 * real m + 1) / (2 * 2^n)"
```
```   405           then have "False"
```
```   406             by (metis neq_4k1_k43)
```
```   407           then show "dyad_rec_dom (b, l, r, (2 * real m + 1) / 2^n)" ..
```
```   408         next
```
```   409           fix m n
```
```   410           assume "(4 * real m' + 3) / (2 * 2 ^ k') = (4 * real m + 3) / (2 * 2^n)"
```
```   411           then have "m' = m" "k' = n" using iff_4k [of _ 3]
```
```   412             by auto
```
```   413           have "dyad_rec_dom (b, l, r, real (2 * m + 1) / 2 ^ k')"
```
```   414             using Suc.IH \<open>k = K\<close> \<open>k' < k\<close> by blast
```
```   415           then show "dyad_rec_dom (b, l, r, (2 * real m + 1) / 2^n)"
```
```   416             using \<open>k' = n\<close> by (auto simp: algebra_simps)
```
```   417         qed
```
```   418         then show ?case by (simp add: eq add_ac)
```
```   419       qed
```
```   420     qed
```
```   421   next
```
```   422     assume "k < K"
```
```   423     then show ?case
```
```   424       using Suc.IH by blast
```
```   425   qed
```
```   426 qed
```
```   427
```
```   428
```
```   429 lemma%unimportant dyad_rec_termination: "x \<in> dyadics \<Longrightarrow> dyad_rec_dom(b,l,r,x)"
```
```   430   by (auto simp: dyadics_levels intro: dyad_rec_level_termination)
```
```   431
```
```   432 lemma%unimportant dyad_rec_of_nat [simp]: "dyad_rec b l r (real m) = b m"
```
```   433   by (simp add: dyad_rec.psimps dyad_rec_termination)
```
```   434
```
```   435 lemma%unimportant 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))"
```
```   436   apply (rule dyad_rec.psimps)
```
```   437   by (metis dyad_rec_level_termination lessI add.commute of_nat_Suc of_nat_mult of_nat_numeral)
```
```   438
```
```   439
```
```   440 lemma%unimportant 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))"
```
```   441   apply (rule dyad_rec.psimps)
```
```   442   by (metis dyad_rec_level_termination lessI of_nat_add of_nat_mult of_nat_numeral)
```
```   443
```
```   444 lemma%unimportant dyad_rec_41_times2:
```
```   445   assumes "n > 0"
```
```   446     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))"
```
```   447 proof -
```
```   448   obtain n' where n': "n = Suc n'"
```
```   449     using assms not0_implies_Suc by blast
```
```   450   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))"
```
```   451     by auto
```
```   452   also have "... = dyad_rec b l r ((4 * real m + 1) / 2^n)"
```
```   453     by (subst mult_divide_mult_cancel_left) auto
```
```   454   also have "... = l (dyad_rec b l r ((2 * real m + 1) / 2 ^ n'))"
```
```   455     by (simp add: add.commute [of 1] n' del: power_Suc)
```
```   456   also have "... = l (dyad_rec b l r ((2 * (2 * real m + 1)) / (2 * 2 ^ n')))"
```
```   457     by (subst mult_divide_mult_cancel_left) auto
```
```   458   also have "... = l (dyad_rec b l r (2 * (2 * real m + 1) / 2^n))"
```
```   459     by (simp add: add.commute n')
```
```   460   finally show ?thesis .
```
```   461 qed
```
```   462
```
```   463 lemma%important dyad_rec_43_times2:
```
```   464   assumes "n > 0"
```
```   465     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))"
```
```   466 proof%unimportant -
```
```   467   obtain n' where n': "n = Suc n'"
```
```   468     using assms not0_implies_Suc by blast
```
```   469   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))"
```
```   470     by auto
```
```   471   also have "... = dyad_rec b l r ((4 * real m + 3) / 2^n)"
```
```   472     by (subst mult_divide_mult_cancel_left) auto
```
```   473   also have "... = r (dyad_rec b l r ((2 * real m + 1) / 2 ^ n'))"
```
```   474     by (simp add: n' del: power_Suc)
```
```   475   also have "... = r (dyad_rec b l r ((2 * (2 * real m + 1)) / (2 * 2 ^ n')))"
```
```   476     by (subst mult_divide_mult_cancel_left) auto
```
```   477   also have "... = r (dyad_rec b l r (2 * (2 * real m + 1) / 2^n))"
```
```   478     by (simp add: n')
```
```   479   finally show ?thesis .
```
```   480 qed
```
```   481
```
```   482 definition%important dyad_rec2
```
```   483     where "dyad_rec2 u v lc rc x =
```
```   484              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)"
```
```   485
```
```   486 abbreviation leftrec where "leftrec u v lc rc x \<equiv> fst (dyad_rec2 u v lc rc x)"
```
```   487 abbreviation rightrec where "rightrec u v lc rc x \<equiv> snd (dyad_rec2 u v lc rc x)"
```
```   488
```
```   489 lemma%unimportant leftrec_base: "leftrec u v lc rc (real m / 2) = u"
```
```   490   by (simp add: dyad_rec2_def)
```
```   491
```
```   492 lemma%unimportant 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)"
```
```   493   apply (simp only: dyad_rec2_def dyad_rec_41_times2)
```
```   494   apply (simp add: case_prod_beta)
```
```   495   done
```
```   496
```
```   497 lemma%unimportant leftrec_43: "n > 0 \<Longrightarrow>
```
```   498              leftrec u v lc rc ((4 * real m + 3) / 2 ^ (Suc n)) =
```
```   499                  rc (leftrec u v lc rc ((2 * real m + 1) / 2^n)) (rightrec u v lc rc ((2 * real m + 1) / 2^n))
```
```   500                  (midpoint (leftrec u v lc rc ((2 * real m + 1) / 2^n)) (rightrec u v lc rc ((2 * real m + 1) / 2^n)))"
```
```   501   apply (simp only: dyad_rec2_def dyad_rec_43_times2)
```
```   502   apply (simp add: case_prod_beta)
```
```   503   done
```
```   504
```
```   505 lemma%unimportant rightrec_base: "rightrec u v lc rc (real m / 2) = v"
```
```   506   by (simp add: dyad_rec2_def)
```
```   507
```
```   508 lemma%unimportant rightrec_41: "n > 0 \<Longrightarrow>
```
```   509              rightrec u v lc rc ((4 * real m + 1) / 2 ^ (Suc n)) =
```
```   510                  lc (leftrec u v lc rc ((2 * real m + 1) / 2^n)) (rightrec u v lc rc ((2 * real m + 1) / 2^n))
```
```   511                  (midpoint (leftrec u v lc rc ((2 * real m + 1) / 2^n)) (rightrec u v lc rc ((2 * real m + 1) / 2^n)))"
```
```   512   apply (simp only: dyad_rec2_def dyad_rec_41_times2)
```
```   513   apply (simp add: case_prod_beta)
```
```   514   done
```
```   515
```
```   516 lemma%unimportant 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)"
```
```   517   apply (simp only: dyad_rec2_def dyad_rec_43_times2)
```
```   518   apply (simp add: case_prod_beta)
```
```   519   done
```
```   520
```
```   521 lemma%unimportant dyadics_in_open_unit_interval:
```
```   522    "{0<..<1} \<inter> (\<Union>k m. {real m / 2^k}) = (\<Union>k. \<Union>m \<in> {0<..<2^k}. {real m / 2^k})"
```
```   523   by (auto simp: divide_simps)
```
```   524
```
```   525
```
```   526
```
```   527 theorem%important homeomorphic_monotone_image_interval:
```
```   528   fixes f :: "real \<Rightarrow> 'a::{real_normed_vector,complete_space}"
```
```   529   assumes cont_f: "continuous_on {0..1} f"
```
```   530       and conn: "\<And>y. connected ({0..1} \<inter> f -` {y})"
```
```   531       and f_1not0: "f 1 \<noteq> f 0"
```
```   532     shows "(f ` {0..1}) homeomorphic {0..1::real}"
```
```   533 proof%unimportant -
```
```   534   have "\<exists>c d. a \<le> c \<and> c \<le> m \<and> m \<le> d \<and> d \<le> b \<and>
```
```   535               (\<forall>x \<in> {c..d}. f x = f m) \<and>
```
```   536               (\<forall>x \<in> {a..<c}. (f x \<noteq> f m)) \<and>
```
```   537               (\<forall>x \<in> {d<..b}. (f x \<noteq> f m)) \<and>
```
```   538               (\<forall>x \<in> {a..<c}. \<forall>y \<in> {d<..b}. f x \<noteq> f y)"
```
```   539     if m: "m \<in> {a..b}" and ab01: "{a..b} \<subseteq> {0..1}" for a b m
```
```   540   proof -
```
```   541     have comp: "compact (f -` {f m} \<inter> {0..1})"
```
```   542       by (simp add: compact_eq_bounded_closed bounded_Int closed_vimage_Int cont_f)
```
```   543     obtain c0 d0 where cd0: "{0..1} \<inter> f -` {f m} = {c0..d0}"
```
```   544       using connected_compact_interval_1 [of "{0..1} \<inter> f -` {f m}"] conn comp
```
```   545       by (metis Int_commute)
```
```   546     with that have "m \<in> cbox c0 d0"
```
```   547       by auto
```
```   548     obtain c d where cd: "{a..b} \<inter> f -` {f m} = {c..d}"
```
```   549       apply (rule_tac c="max a c0" and d="min b d0" in that)
```
```   550       using ab01 cd0 by auto
```
```   551     then have cdab: "{c..d} \<subseteq> {a..b}"
```
```   552       by blast
```
```   553     show ?thesis
```
```   554     proof (intro exI conjI ballI)
```
```   555       show "a \<le> c" "d \<le> b"
```
```   556         using cdab cd m by auto
```
```   557       show "c \<le> m" "m \<le> d"
```
```   558         using cd m by auto
```
```   559       show "\<And>x. x \<in> {c..d} \<Longrightarrow> f x = f m"
```
```   560         using cd by blast
```
```   561       show "f x \<noteq> f m" if "x \<in> {a..<c}" for x
```
```   562         using that m cd [THEN equalityD1, THEN subsetD] \<open>c \<le> m\<close> by force
```
```   563       show "f x \<noteq> f m" if "x \<in> {d<..b}" for x
```
```   564         using that m cd [THEN equalityD1, THEN subsetD, of x] \<open>m \<le> d\<close> by force
```
```   565       show "f x \<noteq> f y" if "x \<in> {a..<c}" "y \<in> {d<..b}" for x y
```
```   566       proof (cases "f x = f m \<or> f y = f m")
```
```   567         case True
```
```   568         then show ?thesis
```
```   569           using \<open>\<And>x. x \<in> {a..<c} \<Longrightarrow> f x \<noteq> f m\<close> that by auto
```
```   570       next
```
```   571         case False
```
```   572         have False if "f x = f y"
```
```   573         proof -
```
```   574           have "x \<le> m" "m \<le> y"
```
```   575             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
```
```   576           then have "x \<in> ({0..1} \<inter> f -` {f y})" "y \<in> ({0..1} \<inter> f -` {f y})"
```
```   577             using \<open>x \<in> {a..<c}\<close> \<open>y \<in> {d<..b}\<close> ab01 by (auto simp: that)
```
```   578           then have "m \<in> ({0..1} \<inter> f -` {f y})"
```
```   579             by (meson \<open>m \<le> y\<close> \<open>x \<le> m\<close> is_interval_connected_1 conn [of "f y"] is_interval_1)
```
```   580           with False show False by auto
```
```   581         qed
```
```   582         then show ?thesis by auto
```
```   583       qed
```
```   584     qed
```
```   585   qed
```
```   586   then obtain leftcut rightcut where LR:
```
```   587     "\<And>a b m. \<lbrakk>m \<in> {a..b}; {a..b} \<subseteq> {0..1}\<rbrakk> \<Longrightarrow>
```
```   588             (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>
```
```   589             (\<forall>x \<in> {leftcut a b m..rightcut a b m}. f x = f m) \<and>
```
```   590             (\<forall>x \<in> {a..<leftcut a b m}. f x \<noteq> f m) \<and>
```
```   591             (\<forall>x \<in> {rightcut a b m<..b}. f x \<noteq> f m) \<and>
```
```   592             (\<forall>x \<in> {a..<leftcut a b m}. \<forall>y \<in> {rightcut a b m<..b}. f x \<noteq> f y))"
```
```   593     apply atomize
```
```   594     apply (clarsimp simp only: imp_conjL [symmetric] choice_iff choice_iff')
```
```   595     apply (rule that, blast)
```
```   596     done
```
```   597   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"
```
```   598     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"
```
```   599     by auto
```
```   600   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"
```
```   601     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"
```
```   602     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"
```
```   603     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>
```
```   604                          \<Longrightarrow> f x = f m" for a b m x y
```
```   605     by (meson atLeastAtMost_iff greaterThanAtMost_iff atLeastLessThan_iff LR)+
```
```   606   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;
```
```   607                              a \<le> m; m \<le> b; {a..b} \<subseteq> {0..1}\<rbrakk>  \<Longrightarrow> f x = f y"
```
```   608     by (metis feqm)
```
```   609   define u where "u \<equiv> rightcut 0 1 0"
```
```   610   have lc[simp]: "leftcut 0 1 0 = 0" and u01: "0 \<le> u" "u \<le> 1"
```
```   611     using LR [of 0 0 1] by (auto simp: u_def)
```
```   612   have f0u: "\<And>x. x \<in> {0..u} \<Longrightarrow> f x = f 0"
```
```   613     using LR [of 0 0 1] unfolding u_def [symmetric]
```
```   614     by (metis \<open>leftcut 0 1 0 = 0\<close> atLeastAtMost_iff order_refl zero_le_one)
```
```   615   have fu1: "\<And>x. x \<in> {u<..1} \<Longrightarrow> f x \<noteq> f 0"
```
```   616     using LR [of 0 0 1] unfolding u_def [symmetric] by fastforce
```
```   617   define v where "v \<equiv> leftcut u 1 1"
```
```   618   have rc[simp]: "rightcut u 1 1 = 1" and v01: "u \<le> v" "v \<le> 1"
```
```   619     using LR [of 1 u 1] u01  by (auto simp: v_def)
```
```   620   have fuv: "\<And>x. x \<in> {u..<v} \<Longrightarrow> f x \<noteq> f 1"
```
```   621     using LR [of 1 u 1] u01 v_def by fastforce
```
```   622   have f0v: "\<And>x. x \<in> {0..<v} \<Longrightarrow> f x \<noteq> f 1"
```
```   623     by (metis f_1not0 atLeastAtMost_iff atLeastLessThan_iff f0u fuv linear)
```
```   624   have fv1: "\<And>x. x \<in> {v..1} \<Longrightarrow> f x = f 1"
```
```   625     using LR [of 1 u 1] u01 v_def by (metis atLeastAtMost_iff atLeastatMost_subset_iff order_refl rc)
```
```   626   define a where "a \<equiv> leftrec u v leftcut rightcut"
```
```   627   define b where "b \<equiv> rightrec u v leftcut rightcut"
```
```   628   define c where "c \<equiv> \<lambda>x. midpoint (a x) (b x)"
```
```   629   have a_real [simp]: "a (real j) = u" for j
```
```   630     using a_def leftrec_base
```
```   631     by (metis nonzero_mult_div_cancel_right of_nat_mult of_nat_numeral zero_neq_numeral)
```
```   632   have b_real [simp]: "b (real j) = v" for j
```
```   633     using b_def rightrec_base
```
```   634     by (metis nonzero_mult_div_cancel_right of_nat_mult of_nat_numeral zero_neq_numeral)
```
```   635   have a41: "a ((4 * real m + 1) / 2^Suc n) = a ((2 * real m + 1) / 2^n)" if "n > 0" for m n
```
```   636     using that a_def leftrec_41 by blast
```
```   637   have b41: "b ((4 * real m + 1) / 2^Suc n) =
```
```   638                leftcut (a ((2 * real m + 1) / 2^n))
```
```   639                        (b ((2 * real m + 1) / 2^n))
```
```   640                        (c ((2 * real m + 1) / 2^n))" if "n > 0" for m n
```
```   641     using that a_def b_def c_def rightrec_41 by blast
```
```   642   have a43: "a ((4 * real m + 3) / 2^Suc n) =
```
```   643                rightcut (a ((2 * real m + 1) / 2^n))
```
```   644                         (b ((2 * real m + 1) / 2^n))
```
```   645                         (c ((2 * real m + 1) / 2^n))" if "n > 0" for m n
```
```   646     using that a_def b_def c_def leftrec_43 by blast
```
```   647   have b43: "b ((4 * real m + 3) / 2^Suc n) = b ((2 * real m + 1) / 2^n)" if "n > 0" for m n
```
```   648     using that b_def rightrec_43 by blast
```
```   649   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
```
```   650   proof (induction n arbitrary: m)
```
```   651     case 0
```
```   652     then show ?case by (simp add: v01)
```
```   653   next
```
```   654     case (Suc n p)
```
```   655     show ?case
```
```   656     proof (cases "even p")
```
```   657       case True
```
```   658       then obtain m where "p = 2*m" by (metis evenE)
```
```   659       then show ?thesis
```
```   660         by (simp add: Suc.IH)
```
```   661     next
```
```   662       case False
```
```   663       then obtain m where m: "p = 2*m + 1" by (metis oddE)
```
```   664       show ?thesis
```
```   665       proof (cases n)
```
```   666         case 0
```
```   667         then show ?thesis
```
```   668           by (simp add: a_def b_def leftrec_base rightrec_base v01)
```
```   669       next
```
```   670         case (Suc n')
```
```   671         then have "n > 0" by simp
```
```   672         have a_le_c: "a (real m / 2^n) \<le> c (real m / 2^n)" for m
```
```   673           unfolding c_def by (metis Suc.IH ge_midpoint_1)
```
```   674         have c_le_b: "c (real m / 2^n) \<le> b (real m / 2^n)" for m
```
```   675           unfolding c_def by (metis Suc.IH le_midpoint_1)
```
```   676         have c_ge_u: "c (real m / 2^n) \<ge> u" for m
```
```   677           using Suc.IH a_le_c order_trans by blast
```
```   678         have c_le_v: "c (real m / 2^n) \<le> v" for m
```
```   679           using Suc.IH c_le_b order_trans by blast
```
```   680         have a_ge_0: "0 \<le> a (real m / 2^n)" for m
```
```   681           using Suc.IH order_trans u01(1) by blast
```
```   682         have b_le_1: "b (real m / 2^n) \<le> 1" for m
```
```   683           using Suc.IH order_trans v01(2) by blast
```
```   684         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
```
```   685           by (simp add: LR a_ge_0 a_le_c b_le_1 c_le_b)
```
```   686         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
```
```   687           by (simp add: LR a_ge_0 a_le_c b_le_1 c_le_b)
```
```   688         show ?thesis
```
```   689         proof (cases "even m")
```
```   690           case True
```
```   691           then obtain r where r: "m = 2*r" by (metis evenE)
```
```   692           show ?thesis
```
```   693             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"]
```
```   694               Suc.IH [of "m+1"]
```
```   695             apply (simp add: r m add.commute [of 1] \<open>n > 0\<close> a41 b41 del: power_Suc)
```
```   696             apply (auto simp: left_right [THEN conjunct1])
```
```   697             using  order_trans [OF left_le c_le_v]
```
```   698             by (metis (no_types, hide_lams) add.commute mult_2 of_nat_Suc of_nat_add)
```
```   699         next
```
```   700           case False
```
```   701           then obtain r where r: "m = 2*r + 1" by (metis oddE)
```
```   702           show ?thesis
```
```   703             using a_le_c [of "m"] c_le_b [of "m"] a_ge_0 [of "m"] b_le_1 [of "m"]
```
```   704               Suc.IH [of "m+1"]
```
```   705             apply (simp add: r m add.commute [of 3] \<open>n > 0\<close> a43 b43 del: power_Suc)
```
```   706             apply (auto simp: add.commute left_right [THEN conjunct2])
```
```   707             using  order_trans [OF c_ge_u right_ge]
```
```   708              apply (metis (no_types, hide_lams) mult_2 numeral_One of_nat_add of_nat_numeral)
```
```   709             apply (metis Suc.IH mult_2 of_nat_1 of_nat_add)
```
```   710             done
```
```   711         qed
```
```   712       qed
```
```   713     qed
```
```   714   qed
```
```   715   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
```
```   716     using uabv order_trans u01 v01 by blast+
```
```   717   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
```
```   718     using uabv order_trans by blast+
```
```   719   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
```
```   720     by (auto simp: c_def ge_midpoint_1 le_midpoint_1 uabv)
```
```   721   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
```
```   722     using a_ge_0 alec order_trans apply blast
```
```   723     by (meson b_le_1 cleb order_trans)
```
```   724   have "\<lbrakk>d = m-n; odd j; \<bar>real i / 2^m - real j / 2^n\<bar> < 1/2 ^ n\<rbrakk>
```
```   725         \<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
```
```   726   proof (induction d arbitrary: j n rule: less_induct)
```
```   727     case (less d j n)
```
```   728     show ?case
```
```   729     proof (cases "m \<le> n")
```
```   730       case True
```
```   731       have "\<bar>2^n\<bar> * \<bar>real i / 2^m - real j / 2^n\<bar> = 0"
```
```   732       proof (rule Ints_nonzero_abs_less1)
```
```   733         have "(real i * 2^n - real j * 2^m) / 2^m = (real i * 2^n) / 2^m - (real j * 2^m) / 2^m"
```
```   734           using diff_divide_distrib by blast
```
```   735         also have "... = (real i * 2 ^ (n-m)) - (real j)"
```
```   736           using True by (auto simp: power_diff field_simps)
```
```   737         also have "... \<in> \<int>"
```
```   738           by simp
```
```   739         finally have "(real i * 2^n - real j * 2^m) / 2^m \<in> \<int>" .
```
```   740         with True Ints_abs show "\<bar>2^n\<bar> * \<bar>real i / 2^m - real j / 2^n\<bar> \<in> \<int>"
```
```   741           by (fastforce simp: divide_simps)
```
```   742         show "\<bar>\<bar>2^n\<bar> * \<bar>real i / 2^m - real j / 2^n\<bar>\<bar> < 1"
```
```   743           using less.prems by (auto simp: divide_simps)
```
```   744       qed
```
```   745       then have "real i / 2^m = real j / 2^n"
```
```   746         by auto
```
```   747       then show ?thesis
```
```   748         by auto
```
```   749     next
```
```   750       case False
```
```   751       then have "n < m" by auto
```
```   752       obtain k where k: "j = Suc (2*k)"
```
```   753         using \<open>odd j\<close> oddE by fastforce
```
```   754       show ?thesis
```
```   755       proof (cases "n > 0")
```
```   756         case False
```
```   757         then have "a (real j / 2^n) = u"
```
```   758           by simp
```
```   759         also have "... \<le> c (real i / 2^m)"
```
```   760           using alec uabv by (blast intro: order_trans)
```
```   761         finally have ac: "a (real j / 2^n) \<le> c (real i / 2^m)" .
```
```   762         have "c (real i / 2^m) \<le> v"
```
```   763           using cleb uabv by (blast intro: order_trans)
```
```   764         also have "... = b (real j / 2^n)"
```
```   765           using False by simp
```
```   766         finally show ?thesis
```
```   767           by (auto simp: ac)
```
```   768       next
```
```   769         case True show ?thesis
```
```   770         proof (cases "real i / 2^m" "real j / 2^n" rule: linorder_cases)
```
```   771           case less
```
```   772           moreover have "real (4 * k + 1) / 2 ^ Suc n + 1 / (2 ^ Suc n) = real j / 2 ^ n"
```
```   773             using k by (force simp: divide_simps)
```
```   774           moreover have "\<bar>real i / 2 ^ m - real j / 2 ^ n\<bar> < 2 / (2 ^ Suc n)"
```
```   775             using less.prems by simp
```
```   776           ultimately have closer: "\<bar>real i / 2 ^ m - real (4 * k + 1) / 2 ^ Suc n\<bar> < 1 / (2 ^ Suc n)"
```
```   777             using less.prems by linarith
```
```   778           have *: "a (real (4 * k + 1) / 2 ^ Suc n) \<le> c (real i / 2 ^ m) \<and>
```
```   779                    c (real i / 2 ^ m) \<le> b (real (4 * k + 1) / 2 ^ Suc n)"
```
```   780             apply (rule less.IH [OF _ refl])
```
```   781             using closer \<open>n < m\<close> \<open>d = m - n\<close> apply (auto simp: divide_simps  \<open>n < m\<close> diff_less_mono2)
```
```   782             done
```
```   783           show ?thesis
```
```   784             using LR [of "c((2*k + 1) / 2^n)" "a((2*k + 1) / 2^n)" "b((2*k + 1) / 2^n)"]
```
```   785             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"]
```
```   786             using k a41 b41 * \<open>0 < n\<close>
```
```   787             apply (simp add: add.commute)
```
```   788             done
```
```   789         next
```
```   790           case equal then show ?thesis by simp
```
```   791         next
```
```   792           case greater
```
```   793           moreover have "real (4 * k + 3) / 2 ^ Suc n - 1 / (2 ^ Suc n) = real j / 2 ^ n"
```
```   794             using k by (force simp: divide_simps)
```
```   795           moreover have "\<bar>real i / 2 ^ m - real j / 2 ^ n\<bar> < 2 * 1 / (2 ^ Suc n)"
```
```   796             using less.prems by simp
```
```   797           ultimately have closer: "\<bar>real i / 2 ^ m - real (4 * k + 3) / 2 ^ Suc n\<bar> < 1 / (2 ^ Suc n)"
```
```   798             using less.prems by linarith
```
```   799           have *: "a (real (4 * k + 3) / 2 ^ Suc n) \<le> c (real i / 2 ^ m) \<and>
```
```   800                    c (real i / 2 ^ m) \<le> b (real (4 * k + 3) / 2 ^ Suc n)"
```
```   801             apply (rule less.IH [OF _ refl])
```
```   802             using closer \<open>n < m\<close> \<open>d = m - n\<close> apply (auto simp: divide_simps  \<open>n < m\<close> diff_less_mono2)
```
```   803             done
```
```   804           show ?thesis
```
```   805             using LR [of "c((2*k + 1) / 2^n)" "a((2*k + 1) / 2^n)" "b((2*k + 1) / 2^n)"]
```
```   806             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"]
```
```   807             using k a43 b43 * \<open>0 < n\<close>
```
```   808             apply (simp add: add.commute)
```
```   809             done
```
```   810         qed
```
```   811       qed
```
```   812     qed
```
```   813   qed
```
```   814   then have aj_le_ci: "a (real j / 2 ^ n) \<le> c (real i / 2 ^ m)"
```
```   815     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
```
```   816     using that by blast+
```
```   817   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
```
```   818   proof (induction n arbitrary: m)
```
```   819     case 0
```
```   820     with u01 v01 show ?case by auto
```
```   821   next
```
```   822     case (Suc n m)
```
```   823     with oddE obtain k where k: "m = Suc (2*k)" by fastforce
```
```   824     show ?case
```
```   825     proof (cases "n > 0")
```
```   826       case False
```
```   827       with u01 v01 show ?thesis
```
```   828         by (simp add: a_def b_def leftrec_base rightrec_base)
```
```   829     next
```
```   830       case True
```
```   831       show ?thesis
```
```   832       proof (cases "even k")
```
```   833         case True
```
```   834         then obtain j where j: "k = 2*j" by (metis evenE)
```
```   835         have "\<bar>a ((2 * real j + 1) / 2 ^ n) - (b ((2 * real j + 1) / 2 ^ n))\<bar> \<le> 2/2 ^ n"
```
```   836         proof -
```
```   837           have "odd (Suc k)"
```
```   838             using True by auto
```
```   839           then show ?thesis
```
```   840             by (metis (no_types) Groups.add_ac(2) Suc.IH j of_nat_Suc of_nat_mult of_nat_numeral)
```
```   841         qed
```
```   842         moreover have "a ((2 * real j + 1) / 2 ^ n) \<le>
```
```   843                        leftcut (a ((2 * real j + 1) / 2 ^ n)) (b ((2 * real j + 1) / 2 ^ n)) (c ((2 * real j + 1) / 2 ^ n))"
```
```   844           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"]
```
```   845           by (auto simp: add.commute left_right)
```
```   846         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>
```
```   847                          c ((2 * real j + 1) / 2 ^ n)"
```
```   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"]
```
```   849           by (auto simp: add.commute left_right_m)
```
```   850         ultimately have "\<bar>a ((2 * real j + 1) / 2 ^ n) -
```
```   851                           leftcut (a ((2 * real j + 1) / 2 ^ n)) (b ((2 * real j + 1) / 2 ^ n)) (c ((2 * real j + 1) / 2 ^ n))\<bar>
```
```   852                    \<le> 2/2 ^ Suc n"
```
```   853           by (simp add: c_def midpoint_def)
```
```   854         with j k \<open>n > 0\<close> show ?thesis
```
```   855           by (simp add: add.commute [of 1] a41 b41 del: power_Suc)
```
```   856       next
```
```   857         case False
```
```   858         then obtain j where j: "k = 2*j + 1" by (metis oddE)
```
```   859         have "\<bar>a ((2 * real j + 1) / 2 ^ n) - (b ((2 * real j + 1) / 2 ^ n))\<bar> \<le> 2/2 ^ n"
```
```   860           using Suc.IH [OF False] j by (auto simp: algebra_simps)
```
```   861         moreover have "c ((2 * real j + 1) / 2 ^ n) \<le>
```
```   862                        rightcut (a ((2 * real j + 1) / 2 ^ n)) (b ((2 * real j + 1) / 2 ^ n)) (c ((2 * real j + 1) / 2 ^ n))"
```
```   863           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"]
```
```   864           by (auto simp: add.commute left_right_m)
```
```   865         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>
```
```   866                          b ((2 * real j + 1) / 2 ^ n)"
```
```   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"]
```
```   868           by (auto simp: add.commute left_right)
```
```   869         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)) -
```
```   870                           b ((2 * real j + 1) / 2 ^ n)\<bar>  \<le>  2/2 ^ Suc n"
```
```   871           by (simp add: c_def midpoint_def)
```
```   872         with j k \<open>n > 0\<close> show ?thesis
```
```   873           by (simp add: add.commute [of 3] a43 b43 del: power_Suc)
```
```   874       qed
```
```   875     qed
```
```   876   qed
```
```   877   have m1_to_3: "4 * real k - 1 = real (4 * (k-1)) + 3" if "0 < k" for k
```
```   878     using that by auto
```
```   879   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
```
```   880   proof (induction n arbitrary: j)
```
```   881     case 0
```
```   882     then show ?case by auto
```
```   883   next
```
```   884     case (Suc n j) show ?case
```
```   885     proof (cases "n > 0")
```
```   886       case False
```
```   887       with Suc.prems show ?thesis by auto
```
```   888     next
```
```   889       case True
```
```   890       show ?thesis proof (cases "even j")
```
```   891         case True
```
```   892         then obtain k where k: "j = 2*k" by (metis evenE)
```
```   893         with \<open>0 < j\<close> have "k > 0" "2 * k < 2 ^ n"
```
```   894           using Suc.prems(2) k by auto
```
```   895         with k \<open>0 < n\<close> Suc.IH [of k] show ?thesis
```
```   896           apply (simp add: m1_to_3 a41 b43 del: power_Suc)
```
```   897           apply (subst of_nat_diff, auto)
```
```   898           done
```
```   899       next
```
```   900         case False
```
```   901         then obtain k where k: "j = 2*k + 1" by (metis oddE)
```
```   902         have "f (leftcut (a ((2 * k + 1) / 2^n)) (b ((2 * k + 1) / 2^n)) (c ((2 * k + 1) / 2^n)))
```
```   903               = f (c ((2 * k + 1) / 2^n))"
```
```   904           "f (c ((2 * k + 1) / 2^n))
```
```   905               = f (rightcut (a ((2 * k + 1) / 2^n)) (b ((2 * k + 1) / 2^n)) (c ((2 * k + 1) / 2^n)))"
```
```   906           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
```
```   907           using left_right_m [of "c((2*k + 1) / 2^n)" "a((2*k + 1) / 2^n)" "b((2*k + 1) / 2^n)"]
```
```   908            apply (auto simp: add.commute  feqm [OF order_refl]  feqm [OF _ order_refl, symmetric])
```
```   909           done
```
```   910         then
```
```   911         show ?thesis
```
```   912           by (simp add: k add.commute [of 1] add.commute [of 3] a43 b41\<open>0 < n\<close> del: power_Suc)
```
```   913       qed
```
```   914     qed
```
```   915   qed
```
```   916   have f_eq_fc: "\<lbrakk>0 < j; j < 2 ^ n\<rbrakk>
```
```   917                  \<Longrightarrow> f(b((2*j - 1) / 2 ^ (Suc n))) = f(c(j / 2^n)) \<and>
```
```   918                      f(a((2*j + 1) / 2 ^ (Suc n))) = f(c(j / 2^n))" for n and j::nat
```
```   919   proof (induction n arbitrary: j)
```
```   920     case 0
```
```   921     then show ?case by auto
```
```   922   next
```
```   923     case (Suc n)
```
```   924     show ?case
```
```   925     proof (cases "even j")
```
```   926       case True
```
```   927       then obtain k where k: "j = 2*k" by (metis evenE)
```
```   928       then have less2n: "k < 2 ^ n"
```
```   929         using Suc.prems(2) by auto
```
```   930       have "0 < k" using \<open>0 < j\<close> k by linarith
```
```   931       then have m1_to_3: "real (4 * k - Suc 0) = real (4 * (k-1)) + 3"
```
```   932         by auto
```
```   933       then show ?thesis
```
```   934         using Suc.IH [of k] k \<open>0 < k\<close>
```
```   935         apply (simp add: less2n add.commute [of 1] m1_to_3 a41 b43 del: power_Suc)
```
```   936         apply (auto simp: of_nat_diff)
```
```   937         done
```
```   938     next
```
```   939       case False
```
```   940       then obtain k where k: "j = 2*k + 1" by (metis oddE)
```
```   941       with Suc.prems have "k < 2^n" by auto
```
```   942       show ?thesis
```
```   943         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
```
```   944         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)"]
```
```   945         apply (simp add: add.commute [of 1] add.commute [of 3] m1_to_3 b41 a43 del: power_Suc)
```
```   946         apply (force intro: feqm)
```
```   947         done
```
```   948     qed
```
```   949   qed
```
```   950   define D01 where "D01 \<equiv> {0<..<1} \<inter> (\<Union>k m. {real m / 2^k})"
```
```   951   have cloD01 [simp]: "closure D01 = {0..1}"
```
```   952     unfolding D01_def
```
```   953     by (subst closure_dyadic_rationals_in_convex_set_pos_1) auto
```
```   954   have "uniformly_continuous_on D01 (f \<circ> c)"
```
```   955   proof (clarsimp simp: uniformly_continuous_on_def)
```
```   956     fix e::real
```
```   957     assume "0 < e"
```
```   958     have ucontf: "uniformly_continuous_on {0..1} f"
```
```   959       by (simp add: compact_uniformly_continuous [OF cont_f])
```
```   960     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"
```
```   961       unfolding uniformly_continuous_on_def dist_norm
```
```   962       by (metis \<open>0 < e\<close> less_divide_eq_numeral1(1) mult_zero_left)
```
```   963     obtain n where n: "1/2^n < min d 1"
```
```   964       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)
```
```   965     with gr0I have "n > 0"
```
```   966       by (force simp: divide_simps)
```
```   967     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"
```
```   968     proof (intro exI ballI impI conjI)
```
```   969       show "(0::real) < 1/2^n" by auto
```
```   970     next
```
```   971       have dist_fc_close: "dist (f(c(real i / 2^m))) (f(c(real j / 2^n))) < e/2"
```
```   972         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
```
```   973       proof -
```
```   974         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
```
```   975           by linarith
```
```   976         consider "i / 2 ^ m = j / 2 ^ n"
```
```   977           | "\<bar>i / 2 ^ m - (2 * j - 1) / 2 ^ Suc n\<bar> < 1/2 ^ Suc n"
```
```   978           | "\<bar>i / 2 ^ m - (2 * j + 1) / 2 ^ Suc n\<bar> < 1/2 ^ Suc n"
```
```   979           using abs3 [OF clo] j by (auto simp: field_simps of_nat_diff)
```
```   980         then show ?thesis
```
```   981         proof cases
```
```   982           case 1 with \<open>0 < e\<close> show ?thesis by auto
```
```   983         next
```
```   984           case 2
```
```   985           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
```
```   986             by auto
```
```   987           have "norm (c (real i / 2 ^ m) - b (real (2 * j - 1) / 2 ^ Suc n)) < d"
```
```   988             using 2 j n close_ab [of "2*j-1" "Suc n"]
```
```   989             using b_ge_0 [of "2*j-1" "Suc n"] b_le_1 [of "2*j-1" "Suc n"]
```
```   990             using aj_le_ci [of "2*j-1" i m "Suc n"]
```
```   991             using ci_le_bj [of "2*j-1" i m "Suc n"]
```
```   992             apply (simp add: divide_simps of_nat_diff del: power_Suc)
```
```   993             apply (auto simp: divide_simps intro!: *)
```
```   994             done
```
```   995           moreover have "f(c(j / 2^n)) = f(b ((2*j - 1) / 2 ^ (Suc n)))"
```
```   996             using f_eq_fc [OF j] by metis
```
```   997           ultimately show ?thesis
```
```   998             by (metis dist_norm atLeastAtMost_iff b_ge_0 b_le_1 c_ge_0 c_le_1 d)
```
```   999         next
```
```  1000           case 3
```
```  1001           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
```
```  1002             by auto
```
```  1003           have "norm (c (real i / 2 ^ m) - a (real (2 * j + 1) / 2 ^ Suc n)) < d"
```
```  1004             using 3 j n close_ab [of "2*j+1" "Suc n"]
```
```  1005             using b_ge_0 [of "2*j+1" "Suc n"] b_le_1 [of "2*j+1" "Suc n"]
```
```  1006             using aj_le_ci [of "2*j+1" i m "Suc n"]
```
```  1007             using ci_le_bj [of "2*j+1" i m "Suc n"]
```
```  1008             apply (simp add: divide_simps of_nat_diff del: power_Suc)
```
```  1009             apply (auto simp: divide_simps intro!: *)
```
```  1010             done
```
```  1011           moreover have "f(c(j / 2^n)) = f(a ((2*j + 1) / 2 ^ (Suc n)))"
```
```  1012             using f_eq_fc [OF j] by metis
```
```  1013           ultimately show ?thesis
```
```  1014             by (metis dist_norm a_ge_0 atLeastAtMost_iff a_ge_0 a_le_1 c_ge_0 c_le_1 d)
```
```  1015         qed
```
```  1016       qed
```
```  1017       show "dist (f (c x')) (f (c x)) < e"
```
```  1018         if "x \<in> D01" "x' \<in> D01" "dist x' x < 1/2^n" for x x'
```
```  1019         using that unfolding D01_def dyadics_in_open_unit_interval
```
```  1020       proof clarsimp
```
```  1021         fix i k::nat and m p
```
```  1022         assume i: "0 < i" "i < 2 ^ m" and k: "0<k" "k < 2 ^ p"
```
```  1023         assume clo: "dist (real k / 2 ^ p) (real i / 2 ^ m) < 1/2 ^ n"
```
```  1024         obtain j::nat where "0 < j" "j < 2 ^ n"
```
```  1025           and clo_ij: "abs(i / 2^m - j / 2^n) < 1/2 ^ n"
```
```  1026           and clo_kj: "abs(k / 2^p - j / 2^n) < 1/2 ^ n"
```
```  1027         proof -
```
```  1028           have "max (2^n * i / 2^m) (2^n * k / 2^p) \<ge> 0"
```
```  1029             by (auto simp: le_max_iff_disj)
```
```  1030           then obtain j where "floor (max (2^n*i / 2^m) (2^n*k / 2^p)) = int j"
```
```  1031             using zero_le_floor zero_le_imp_eq_int by blast
```
```  1032           then have j_le: "real j \<le> max (2^n * i / 2^m) (2^n * k / 2^p)"
```
```  1033             and less_j1: "max (2^n * i / 2^m) (2^n * k / 2^p) < real j + 1"
```
```  1034             using floor_correct [of "max (2^n * i / 2^m) (2^n * k / 2^p)"] by linarith+
```
```  1035           show thesis
```
```  1036           proof (cases "j = 0")
```
```  1037             case True
```
```  1038             show thesis
```
```  1039             proof
```
```  1040               show "(1::nat) < 2 ^ n"
```
```  1041                 apply (subst one_less_power)
```
```  1042                 using \<open>n > 0\<close> by auto
```
```  1043               show "\<bar>real i / 2 ^ m - real 1/2 ^ n\<bar> < 1/2 ^ n"
```
```  1044                 using i less_j1 by (simp add: dist_norm field_simps True)
```
```  1045               show "\<bar>real k / 2 ^ p - real 1/2 ^ n\<bar> < 1/2 ^ n"
```
```  1046                 using k less_j1 by (simp add: dist_norm field_simps True)
```
```  1047             qed simp
```
```  1048           next
```
```  1049             case False
```
```  1050             have 1: "real j * 2 ^ m < real i * 2 ^ n"
```
```  1051               if j: "real j * 2 ^ p \<le> real k * 2 ^ n" and k: "real k * 2 ^ m < real i * 2 ^ p"
```
```  1052               for i k m p
```
```  1053             proof -
```
```  1054               have "real j * 2 ^ p * 2 ^ m \<le> real k * 2 ^ n * 2 ^ m"
```
```  1055                 using j by simp
```
```  1056               moreover have "real k * 2 ^ m * 2 ^ n < real i * 2 ^ p * 2 ^ n"
```
```  1057                 using k by simp
```
```  1058               ultimately have "real j * 2 ^ p * 2 ^ m < real i * 2 ^ p * 2 ^ n"
```
```  1059                 by (simp only: mult_ac)
```
```  1060               then show ?thesis
```
```  1061                 by simp
```
```  1062             qed
```
```  1063             have 2: "real j * 2 ^ m < 2 ^ m + real i * 2 ^ n"
```
```  1064               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)"
```
```  1065               for i k m p
```
```  1066             proof -
```
```  1067               have "real j * 2 ^ p * 2 ^ m \<le> real k * (2 ^ m * 2 ^ n)"
```
```  1068                 using j by simp
```
```  1069               also have "... < 2 ^ m * 2 ^ p + real i * (2 ^ n * 2 ^ p)"
```
```  1070                 by (rule k)
```
```  1071               finally have "(real j * 2 ^ m) * 2 ^ p < (2 ^ m + real i * 2 ^ n) * 2 ^ p"
```
```  1072                 by (simp add: algebra_simps)
```
```  1073               then show ?thesis
```
```  1074                 by simp
```
```  1075             qed
```
```  1076             have 3: "real j * 2 ^ p < 2 ^ p + real k * 2 ^ n"
```
```  1077               if j: "real j * 2 ^ m \<le> real i * 2 ^ n" and i: "real i * 2 ^ p \<le> real k * 2 ^ m"
```
```  1078             proof -
```
```  1079               have "real j * 2 ^ m * 2 ^ p \<le> real i * 2 ^ n * 2 ^ p"
```
```  1080                 using j by simp
```
```  1081               moreover have "real i * 2 ^ p * 2 ^ n \<le> real k * 2 ^ m * 2 ^ n"
```
```  1082                 using i by simp
```
```  1083               ultimately have "real j * 2 ^ m * 2 ^ p \<le> real k * 2 ^ m * 2 ^ n"
```
```  1084                 by (simp only: mult_ac)
```
```  1085               then have "real j * 2 ^ p \<le> real k * 2 ^ n"
```
```  1086                 by simp
```
```  1087               also have "... < 2 ^ p + real k * 2 ^ n"
```
```  1088                 by auto
```
```  1089               finally show ?thesis by simp
```
```  1090             qed
```
```  1091             show ?thesis
```
```  1092             proof
```
```  1093               have "real j < 2 ^ n"
```
```  1094                 using j_le i k
```
```  1095                 apply (auto simp: le_max_iff_disj simp del: of_nat_less_numeral_power_cancel_iff
```
```  1096                     elim!: le_less_trans)
```
```  1097                  apply (auto simp: field_simps)
```
```  1098                 done
```
```  1099               then show "j < 2 ^ n"
```
```  1100                 by auto
```
```  1101               show "\<bar>real i / 2 ^ m - real j / 2 ^ n\<bar> < 1/2 ^ n"
```
```  1102                 using clo less_j1 j_le
```
```  1103                 apply (auto simp: le_max_iff_disj divide_simps dist_norm)
```
```  1104                  apply (auto simp: algebra_simps abs_if split: if_split_asm dest: 1 2)
```
```  1105                 done
```
```  1106               show "\<bar>real k / 2 ^ p - real j / 2 ^ n\<bar> < 1/2 ^ n"
```
```  1107                 using  clo less_j1 j_le
```
```  1108                 apply (auto simp: le_max_iff_disj divide_simps dist_norm)
```
```  1109                  apply (auto simp: algebra_simps not_less abs_if split: if_split_asm dest: 3 2)
```
```  1110                 done
```
```  1111             qed (use False in simp)
```
```  1112           qed
```
```  1113         qed
```
```  1114         show "dist (f (c (real k / 2 ^ p))) (f (c (real i / 2 ^ m))) < e"
```
```  1115         proof (rule dist_triangle_half_l)
```
```  1116           show "dist (f (c (real k / 2 ^ p))) (f(c(j / 2^n))) < e/2"
```
```  1117             apply (rule dist_fc_close)
```
```  1118             using \<open>0 < j\<close> \<open>j < 2 ^ n\<close> k clo_kj by auto
```
```  1119           show "dist (f (c (real i / 2 ^ m))) (f (c (real j / 2 ^ n))) < e/2"
```
```  1120             apply (rule dist_fc_close)
```
```  1121             using \<open>0 < j\<close> \<open>j < 2 ^ n\<close> i clo_ij by auto
```
```  1122         qed
```
```  1123       qed
```
```  1124     qed
```
```  1125   qed
```
```  1126   then obtain h where ucont_h: "uniformly_continuous_on {0..1} h"
```
```  1127     and fc_eq: "\<And>x. x \<in> D01 \<Longrightarrow> (f \<circ> c) x = h x"
```
```  1128   proof (rule uniformly_continuous_on_extension_on_closure [of D01 "f \<circ> c"])
```
```  1129   qed (use closure_subset [of D01] in \<open>auto intro!: that\<close>)
```
```  1130   then have cont_h: "continuous_on {0..1} h"
```
```  1131     using uniformly_continuous_imp_continuous by blast
```
```  1132   have h_eq: "h (real k / 2 ^ m) = f (c (real k / 2 ^ m))" if "0 < k" "k < 2^m" for k m
```
```  1133     using fc_eq that by (force simp: D01_def)
```
```  1134   have "h ` {0..1} = f ` {0..1}"
```
```  1135   proof
```
```  1136     have "h ` (closure D01) \<subseteq> f ` {0..1}"
```
```  1137     proof (rule image_closure_subset)
```
```  1138       show "continuous_on (closure D01) h"
```
```  1139         using cont_h by simp
```
```  1140       show "closed (f ` {0..1})"
```
```  1141         using compact_continuous_image [OF cont_f] compact_imp_closed by blast
```
```  1142       show "h ` D01 \<subseteq> f ` {0..1}"
```
```  1143         by (force simp: dyadics_in_open_unit_interval D01_def h_eq)
```
```  1144     qed
```
```  1145     with cloD01 show "h ` {0..1} \<subseteq> f ` {0..1}" by simp
```
```  1146     have a12 [simp]: "a (1/2) = u"
```
```  1147       by (metis a_def leftrec_base numeral_One of_nat_numeral)
```
```  1148     have b12 [simp]: "b (1/2) = v"
```
```  1149       by (metis b_def rightrec_base numeral_One of_nat_numeral)
```
```  1150     have "f ` {0..1} \<subseteq> closure(h ` D01)"
```
```  1151     proof (clarsimp simp: closure_approachable dyadics_in_open_unit_interval D01_def)
```
```  1152       fix x e::real
```
```  1153       assume "0 \<le> x" "x \<le> 1" "0 < e"
```
```  1154       have ucont_f: "uniformly_continuous_on {0..1} f"
```
```  1155         using compact_uniformly_continuous cont_f by blast
```
```  1156       then obtain \<delta> where "\<delta> > 0"
```
```  1157         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"
```
```  1158         using \<open>0 < e\<close> by (auto simp: uniformly_continuous_on_def dist_norm)
```
```  1159       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"
```
```  1160         if "n \<noteq> 0" for n
```
```  1161         using that
```
```  1162       proof (induction n)
```
```  1163         case 0 then show ?case by auto
```
```  1164       next
```
```  1165         case (Suc n)
```
```  1166         show ?case
```
```  1167         proof (cases "n=0")
```
```  1168           case True
```
```  1169           consider "x \<in> {0..u}" | "x \<in> {u..v}" | "x \<in> {v..1}"
```
```  1170             using \<open>0 \<le> x\<close> \<open>x \<le> 1\<close> by force
```
```  1171           then have "\<exists>y\<ge>a (real 1/2). y \<le> b (real 1/2) \<and> f y = f x"
```
```  1172           proof cases
```
```  1173             case 1
```
```  1174             then show ?thesis
```
```  1175               apply (rule_tac x=u in exI)
```
```  1176               using uabv [of 1 1] f0u [of u] f0u [of x] by auto
```
```  1177           next
```
```  1178             case 2
```
```  1179             then show ?thesis
```
```  1180               by (rule_tac x=x in exI) auto
```
```  1181           next
```
```  1182             case 3
```
```  1183             then show ?thesis
```
```  1184               apply (rule_tac x=v in exI)
```
```  1185               using uabv [of 1 1] fv1 [of v] fv1 [of x] by auto
```
```  1186           qed
```
```  1187           with \<open>n=0\<close> show ?thesis
```
```  1188             by (rule_tac x=1 in exI) auto
```
```  1189         next
```
```  1190           case False
```
```  1191           with Suc obtain m y
```
```  1192             where "odd m" "0 < m" and mless: "m < 2 ^ n"
```
```  1193               and y: "y \<in> {a (real m / 2 ^ n)..b (real m / 2 ^ n)}" and feq: "f y = f x"
```
```  1194             by metis
```
```  1195           then obtain j where j: "m = 2*j + 1" by (metis oddE)
```
```  1196           consider "y \<in> {a((2*j + 1) / 2^n) .. b((4*j + 1) / 2 ^ (Suc n))}"
```
```  1197             | "y \<in> {b((4*j + 1) / 2 ^ (Suc n)) .. a((4*j + 3) / 2 ^ (Suc n))}"
```
```  1198             | "y \<in> {a((4*j + 3) / 2 ^ (Suc n)) .. b((2*j + 1) / 2^n)}"
```
```  1199             using y j by force
```
```  1200           then show ?thesis
```
```  1201           proof cases
```
```  1202             case 1
```
```  1203             then show ?thesis
```
```  1204               apply (rule_tac x="4*j + 1" in exI)
```
```  1205               apply (rule_tac x=y in exI)
```
```  1206               using mless j \<open>n \<noteq> 0\<close>
```
```  1207               apply (simp add: feq a41 b41 add.commute [of 1] del: power_Suc)
```
```  1208               apply (simp add: algebra_simps)
```
```  1209               done
```
```  1210           next
```
```  1211             case 2
```
```  1212             show ?thesis
```
```  1213               apply (rule_tac x="4*j + 1" in exI)
```
```  1214               apply (rule_tac x="b((4*j + 1) / 2 ^ (Suc n))" in exI)
```
```  1215               using mless \<open>n \<noteq> 0\<close> 2 j
```
```  1216               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]
```
```  1217               using left_right [of "c((2*j + 1) / 2^n)" "a((2*j + 1) / 2^n)" "b((2*j + 1) / 2^n)"]
```
```  1218               apply (simp add: a41 b41 a43 b43 add.commute [of 1] add.commute [of 3] del: power_Suc)
```
```  1219               apply (auto simp: feq [symmetric] intro: f_eqI)
```
```  1220               done
```
```  1221           next
```
```  1222             case 3
```
```  1223             then show ?thesis
```
```  1224               apply (rule_tac x="4*j + 3" in exI)
```
```  1225               apply (rule_tac x=y in exI)
```
```  1226               using mless j \<open>n \<noteq> 0\<close>
```
```  1227               apply (simp add: feq a43 b43 del: power_Suc)
```
```  1228               apply (simp add: algebra_simps)
```
```  1229               done
```
```  1230           qed
```
```  1231         qed
```
```  1232       qed
```
```  1233       obtain n where n: "1/2^n < min (\<delta> / 2) 1"
```
```  1234         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)
```
```  1235       with gr0I have "n \<noteq> 0"
```
```  1236         by fastforce
```
```  1237       with * obtain m::nat and y
```
```  1238         where "odd m" "0 < m" and mless: "m < 2 ^ n"
```
```  1239           and y: "y \<in> {a(m / 2^n) .. b(m / 2^n)}" and feq: "f x = f y"
```
```  1240         by metis
```
```  1241       then have "0 \<le> y" "y \<le> 1"
```
```  1242         by (metis atLeastAtMost_iff a_ge_0 b_le_1 order.trans)+
```
```  1243       moreover have "y < \<delta> + c (real m / 2 ^ n)" "c (real m / 2 ^ n) < \<delta> + y"
```
```  1244         using y apply simp_all
```
```  1245         using alec [of m n] cleb [of m n] n field_sum_of_halves close_ab [OF \<open>odd m\<close>, of n]
```
```  1246         by linarith+
```
```  1247       moreover note \<open>0 < m\<close> mless \<open>0 \<le> x\<close> \<open>x \<le> 1\<close>
```
```  1248       ultimately show "\<exists>k. \<exists>m\<in>{0<..<2 ^ k}. dist (h (real m / 2 ^ k)) (f x) < e"
```
```  1249         apply (rule_tac x=n in exI)
```
```  1250         apply (rule_tac x=m in bexI)
```
```  1251          apply (auto simp: dist_norm h_eq feq \<delta>)
```
```  1252         done
```
```  1253     qed
```
```  1254     also have "... \<subseteq> h ` {0..1}"
```
```  1255       apply (rule closure_minimal)
```
```  1256       using compact_continuous_image [OF cont_h] compact_imp_closed by (auto simp: D01_def)
```
```  1257     finally show "f ` {0..1} \<subseteq> h ` {0..1}" .
```
```  1258   qed
```
```  1259   moreover have "inj_on h {0..1}"
```
```  1260   proof -
```
```  1261     have "u < v"
```
```  1262       by (metis atLeastAtMost_iff f0u f_1not0 fv1 order.not_eq_order_implies_strict u01(1) u01(2) v01(1))
```
```  1263     have f_not_fu: "\<And>x. \<lbrakk>u < x; x \<le> v\<rbrakk> \<Longrightarrow> f x \<noteq> f u"
```
```  1264       by (metis atLeastAtMost_iff f0u fu1 greaterThanAtMost_iff order_refl order_trans u01(1) v01(2))
```
```  1265     have f_not_fv: "\<And>x. \<lbrakk>u \<le> x; x < v\<rbrakk> \<Longrightarrow> f x \<noteq> f v"
```
```  1266       by (metis atLeastAtMost_iff order_refl order_trans v01(2) atLeastLessThan_iff fuv fv1)
```
```  1267     have a_less_b:
```
```  1268          "a(j / 2^n) < b(j / 2^n) \<and>
```
```  1269           (\<forall>x. a(j / 2^n) < x \<longrightarrow> x \<le> b(j / 2^n) \<longrightarrow> f x \<noteq> f(a(j / 2^n))) \<and>
```
```  1270           (\<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
```
```  1271     proof (induction n arbitrary: j)
```
```  1272       case 0 then show ?case
```
```  1273         by (simp add: \<open>u < v\<close> f_not_fu f_not_fv)
```
```  1274     next
```
```  1275       case (Suc n j) show ?case
```
```  1276       proof (cases "n > 0")
```
```  1277         case False then show ?thesis
```
```  1278           by (auto simp: a_def b_def leftrec_base rightrec_base \<open>u < v\<close> f_not_fu f_not_fv)
```
```  1279       next
```
```  1280         case True show ?thesis
```
```  1281         proof (cases "even j")
```
```  1282           case True
```
```  1283           with \<open>0 < n\<close> Suc.IH show ?thesis
```
```  1284             by (auto elim!: evenE)
```
```  1285         next
```
```  1286           case False
```
```  1287           then obtain k where k: "j = 2*k + 1" by (metis oddE)
```
```  1288           then show ?thesis
```
```  1289           proof (cases "even k")
```
```  1290             case True
```
```  1291             then obtain m where m: "k = 2*m" by (metis evenE)
```
```  1292             have fleft: "f (leftcut (a ((2*m + 1) / 2^n)) (b ((2*m + 1) / 2^n)) (c ((2*m + 1) / 2^n))) =
```
```  1293                          f (c((2*m + 1) / 2^n))"
```
```  1294               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]
```
```  1295               using left_right_m [of "c((2*m + 1) / 2^n)" "a((2*m + 1) / 2^n)" "b((2*m + 1) / 2^n)"]
```
```  1296               by (auto intro: f_eqI)
```
```  1297             show ?thesis
```
```  1298             proof (intro conjI impI notI allI)
```
```  1299               have False if "b (real j / 2 ^ Suc n) \<le> a (real j / 2 ^ Suc n)"
```
```  1300               proof -
```
```  1301                 have "f (c ((1 + real m * 2) / 2 ^ n)) = f (a ((1 + real m * 2) / 2 ^ n))"
```
```  1302                   using k m \<open>0 < n\<close> fleft that a41 [of n m] b41 [of n m]
```
```  1303                   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]
```
```  1304                   using left_right [of "c((2*m + 1) / 2^n)" "a((2*m + 1) / 2^n)" "b((2*m + 1) / 2^n)"]
```
```  1305                   by (auto simp: algebra_simps)
```
```  1306                 moreover have "a (real (1 + m * 2) / 2 ^ n) < c (real (1 + m * 2) / 2 ^ n)"
```
```  1307                   using Suc.IH [of "1 + m * 2"] by (simp add: c_def midpoint_def)
```
```  1308                 moreover have "c (real (1 + m * 2) / 2 ^ n) \<le> b (real (1 + m * 2) / 2 ^ n)"
```
```  1309                   using cleb by blast
```
```  1310                 ultimately show ?thesis
```
```  1311                   using Suc.IH [of "1 + m * 2"] by force
```
```  1312               qed
```
```  1313               then show "a (real j / 2 ^ Suc n) < b (real j / 2 ^ Suc n)" by force
```
```  1314             next
```
```  1315               fix x
```
```  1316               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))"
```
```  1317               then show False
```
```  1318                 using Suc.IH [of "1 + m * 2", THEN conjunct2, THEN conjunct1]
```
```  1319                 using k m \<open>0 < n\<close> a41 [of n m] b41 [of n m]
```
```  1320                 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]
```
```  1321                 using left_right_m [of "c((2*m + 1) / 2^n)" "a((2*m + 1) / 2^n)" "b((2*m + 1) / 2^n)"]
```
```  1322                 by (auto simp: algebra_simps)
```
```  1323             next
```
```  1324               fix x
```
```  1325               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))"
```
```  1326               then show False
```
```  1327                 using k m \<open>0 < n\<close> a41 [of n m] b41 [of n m] fleft left_neq
```
```  1328                 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]
```
```  1329                 by (auto simp: algebra_simps)
```
```  1330             qed
```
```  1331           next
```
```  1332             case False
```
```  1333             with oddE obtain m where m: "k = Suc (2*m)" by fastforce
```
```  1334             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))"
```
```  1335               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]
```
```  1336               using left_right_m [of "c((2*m + 1) / 2^n)" "a((2*m + 1) / 2^n)" "b((2*m + 1) / 2^n)"]
```
```  1337               by (auto intro: f_eqI [OF _ order_refl])
```
```  1338             show ?thesis
```
```  1339             proof (intro conjI impI notI allI)
```
```  1340               have False if "b (real j / 2 ^ Suc n) \<le> a (real j / 2 ^ Suc n)"
```
```  1341               proof -
```
```  1342                 have "f (c ((1 + real m * 2) / 2 ^ n)) = f (b ((1 + real m * 2) / 2 ^ n))"
```
```  1343                   using k m \<open>0 < n\<close> fright that a43 [of n m] b43 [of n m]
```
```  1344                   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]
```
```  1345                   using left_right [of "c((2*m + 1) / 2^n)" "a((2*m + 1) / 2^n)" "b((2*m + 1) / 2^n)"]
```
```  1346                   by (auto simp: algebra_simps)
```
```  1347                 moreover have "a (real (1 + m * 2) / 2 ^ n) \<le> c (real (1 + m * 2) / 2 ^ n)"
```
```  1348                   using alec by blast
```
```  1349                 moreover have "c (real (1 + m * 2) / 2 ^ n) < b (real (1 + m * 2) / 2 ^ n)"
```
```  1350                   using Suc.IH [of "1 + m * 2"] by (simp add: c_def midpoint_def)
```
```  1351                 ultimately show ?thesis
```
```  1352                   using Suc.IH [of "1 + m * 2"] by force
```
```  1353               qed
```
```  1354               then show "a (real j / 2 ^ Suc n) < b (real j / 2 ^ Suc n)" by force
```
```  1355             next
```
```  1356               fix x
```
```  1357               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))"
```
```  1358               then show False
```
```  1359                 using k m \<open>0 < n\<close> a43 [of n m] b43 [of n m] fright right_neq
```
```  1360                 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]
```
```  1361                 by (auto simp: algebra_simps)
```
```  1362             next
```
```  1363               fix x
```
```  1364               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))"
```
```  1365               then show False
```
```  1366                 using Suc.IH [of "1 + m * 2", THEN conjunct2, THEN conjunct2]
```
```  1367                 using k m \<open>0 < n\<close> a43 [of n m] b43 [of n m]
```
```  1368                 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]
```
```  1369                 using left_right_m [of "c((2*m + 1) / 2^n)" "a((2*m + 1) / 2^n)" "b((2*m + 1) / 2^n)"]
```
```  1370                 by (auto simp: algebra_simps fright simp del: power_Suc)
```
```  1371             qed
```
```  1372           qed
```
```  1373         qed
```
```  1374       qed
```
```  1375     qed
```
```  1376     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
```
```  1377       using a_less_b [of m n] apply (simp_all add: c_def midpoint_def)
```
```  1378       using a_ge_0 [of m n] b_le_1 [of m n] apply linarith+
```
```  1379       done
```
```  1380     have approx: "\<exists>j n. odd j \<and> n \<noteq> 0 \<and>
```
```  1381                         real i / 2^m \<le> real j / 2^n \<and>
```
```  1382                         real j / 2^n \<le> real k / 2^p \<and>
```
```  1383                         \<bar>real i / 2 ^ m - real j / 2 ^ n\<bar> < 1/2^n \<and>
```
```  1384                         \<bar>real k / 2 ^ p - real j / 2 ^ n\<bar> < 1/2^n"
```
```  1385       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
```
```  1386       using that
```
```  1387     proof (induction N arbitrary: m p i k rule: less_induct)
```
```  1388       case (less N)
```
```  1389       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"
```
```  1390         by linarith
```
```  1391       then show ?case
```
```  1392       proof cases
```
```  1393         case 1
```
```  1394         with less.prems show ?thesis
```
```  1395           by (rule_tac x=1 in exI)+ (fastforce simp: divide_simps)
```
```  1396       next
```
```  1397         case 2 show ?thesis
```
```  1398         proof (cases m)
```
```  1399           case 0 with less.prems show ?thesis
```
```  1400             by auto
```
```  1401         next
```
```  1402           case (Suc m') show ?thesis
```
```  1403           proof (cases p)
```
```  1404             case 0 with less.prems show ?thesis by auto
```
```  1405           next
```
```  1406             case (Suc p')
```
```  1407             have False if "real i * 2 ^ p' < real k * 2 ^ m'" "k < 2 ^ p'" "2 ^ m' \<le> i"
```
```  1408             proof -
```
```  1409               have "real k * 2 ^ m' < 2 ^ p' * 2 ^ m'"
```
```  1410                 using that by simp
```
```  1411               then have "real i * 2 ^ p' < 2 ^ p' * 2 ^ m'"
```
```  1412                 using that by linarith
```
```  1413               with that show ?thesis by simp
```
```  1414             qed
```
```  1415             then show ?thesis
```
```  1416               using less.IH [of "m'+p'" i m' k p'] less.prems \<open>m = Suc m'\<close> 2 Suc
```
```  1417               apply atomize
```
```  1418               apply (force simp: divide_simps)
```
```  1419               done
```
```  1420           qed
```
```  1421         qed
```
```  1422       next
```
```  1423         case 3 show ?thesis
```
```  1424         proof (cases m)
```
```  1425           case 0 with less.prems show ?thesis
```
```  1426             by auto
```
```  1427         next
```
```  1428           case (Suc m') show ?thesis
```
```  1429           proof (cases p)
```
```  1430             case 0 with less.prems show ?thesis by auto
```
```  1431           next
```
```  1432             case (Suc p')
```
```  1433             then show ?thesis
```
```  1434               using less.IH [of "m'+p'" "i - 2^m'" m' "k - 2 ^ p'" p'] less.prems \<open>m = Suc m'\<close> Suc 3
```
```  1435               apply atomize
```
```  1436               apply (auto simp: field_simps of_nat_diff)
```
```  1437               apply (rule_tac x="2 ^ n + j" in exI, simp)
```
```  1438               apply (rule_tac x="Suc n" in exI)
```
```  1439               apply (auto simp: field_simps)
```
```  1440               done
```
```  1441           qed
```
```  1442         qed
```
```  1443       qed
```
```  1444     qed
```
```  1445     have clec: "c(real i / 2^m) \<le> c(real j / 2^n)"
```
```  1446       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
```
```  1447     proof -
```
```  1448       obtain j' n' where "odd j'" "n' \<noteq> 0"
```
```  1449         and i_le_j: "real i / 2 ^ m \<le> real j' / 2 ^ n'"
```
```  1450         and j_le_j: "real j' / 2 ^ n' \<le> real j / 2 ^ n"
```
```  1451         and clo_ij: "\<bar>real i / 2 ^ m - real j' / 2 ^ n'\<bar> < 1/2 ^ n'"
```
```  1452         and clo_jj: "\<bar>real j / 2 ^ n - real j' / 2 ^ n'\<bar> < 1/2 ^ n'"
```
```  1453         using approx [of i m j n "m+n"] that i j ij by auto
```
```  1454       with oddE obtain q where q: "j' = Suc (2*q)" by fastforce
```
```  1455       have "c (real i / 2 ^ m) \<le> c((2*q + 1) / 2^n')"
```
```  1456       proof (cases "i / 2^m = (2*q + 1) / 2^n'")
```
```  1457         case True then show ?thesis by simp
```
```  1458       next
```
```  1459         case False
```
```  1460         with i_le_j q have less: "i / 2^m < (2*q + 1) / 2^n'"
```
```  1461           by auto
```
```  1462         have *: "\<lbrakk>i < q; abs(i - q) < s*2; q = r + s\<rbrakk> \<Longrightarrow> abs(i - r) < s" for i q s r::real
```
```  1463           by auto
```
```  1464         have "c(i / 2^m) \<le> b(real(4 * q + 1) / 2 ^ (Suc n'))"
```
```  1465           apply (rule ci_le_bj, force)
```
```  1466           apply (rule * [OF less])
```
```  1467           using i_le_j clo_ij q apply (auto simp: divide_simps)
```
```  1468           done
```
```  1469         then show ?thesis
```
```  1470           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>
```
```  1471           using left_right_m [of "c((2*q + 1) / 2^n')" "a((2*q + 1) / 2^n')" "b((2*q + 1) / 2^n')"]
```
```  1472           by (auto simp: algebra_simps)
```
```  1473       qed
```
```  1474       also have "... \<le> c(real j / 2^n)"
```
```  1475       proof (cases "j / 2^n = (2*q + 1) / 2^n'")
```
```  1476         case True
```
```  1477         then show ?thesis by simp
```
```  1478       next
```
```  1479         case False
```
```  1480         with j_le_j q have less: "(2*q + 1) / 2^n' < j / 2^n"
```
```  1481           by auto
```
```  1482         have *: "\<lbrakk>q < i; abs(i - q) < s*2; r = q + s\<rbrakk> \<Longrightarrow> abs(i - r) < s" for i q s r::real
```
```  1483           by auto
```
```  1484         have "a(real(4*q + 3) / 2 ^ (Suc n')) \<le> c(j / 2^n)"
```
```  1485           apply (rule aj_le_ci, force)
```
```  1486           apply (rule * [OF less])
```
```  1487           using j_le_j clo_jj q apply (auto simp: divide_simps)
```
```  1488           done
```
```  1489         then show ?thesis
```
```  1490           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>
```
```  1491           using left_right_m [of "c((2*q + 1) / 2^n')" "a((2*q + 1) / 2^n')" "b((2*q + 1) / 2^n')"]
```
```  1492           by (auto simp: algebra_simps)
```
```  1493       qed
```
```  1494       finally show ?thesis .
```
```  1495     qed
```
```  1496     have "x = y" if "0 \<le> x" "x \<le> 1" "0 \<le> y" "y \<le> 1" "h x = h y" for x y
```
```  1497       using that
```
```  1498     proof (induction x y rule: linorder_class.linorder_less_wlog)
```
```  1499       case (less x1 x2)
```
```  1500       obtain m n where m: "0 < m" "m < 2 ^ n"
```
```  1501         and x12: "x1 < m / 2^n" "m / 2^n < x2"
```
```  1502         and neq: "h x1 \<noteq> h (real m / 2^n)"
```
```  1503       proof -
```
```  1504         have "(x1 + x2) / 2 \<in> closure D01"
```
```  1505           using cloD01 less.hyps less.prems by auto
```
```  1506         with less obtain y where "y \<in> D01" and dist_y: "dist y ((x1 + x2) / 2) < (x2 - x1) / 64"
```
```  1507           unfolding closure_approachable
```
```  1508           by (metis diff_gt_0_iff_gt less_divide_eq_numeral1(1) mult_zero_left)
```
```  1509         obtain m n where m: "0 < m" "m < 2 ^ n"
```
```  1510                      and clo: "\<bar>real m / 2 ^ n - (x1 + x2) / 2\<bar> < (x2 - x1) / 64"
```
```  1511                      and n: "1/2^n < (x2 - x1) / 128"
```
```  1512         proof -
```
```  1513           have "min 1 ((x2 - x1) / 128) > 0" "1/2 < (1::real)"
```
```  1514             using less by auto
```
```  1515           then obtain N where N: "1/2^N < min 1 ((x2 - x1) / 128)"
```
```  1516             by (metis power_one_over real_arch_pow_inv)
```
```  1517           then have "N > 0"
```
```  1518             using less_divide_eq_1 by force
```
```  1519           obtain p q where p: "p < 2 ^ q" "p \<noteq> 0" and yeq: "y = real p / 2 ^ q"
```
```  1520             using \<open>y \<in> D01\<close> by (auto simp: zero_less_divide_iff D01_def)
```
```  1521           show ?thesis
```
```  1522           proof
```
```  1523             show "0 < 2^N * p"
```
```  1524               using p by auto
```
```  1525             show "2 ^ N * p < 2 ^ (N+q)"
```
```  1526               by (simp add: p power_add)
```
```  1527             have "\<bar>real (2 ^ N * p) / 2 ^ (N + q) - (x1 + x2) / 2\<bar> = \<bar>real p / 2 ^ q - (x1 + x2) / 2\<bar>"
```
```  1528               by (simp add: power_add)
```
```  1529             also have "... = \<bar>y - (x1 + x2) / 2\<bar>"
```
```  1530               by (simp add: yeq)
```
```  1531             also have "... < (x2 - x1) / 64"
```
```  1532               using dist_y by (simp add: dist_norm)
```
```  1533             finally show "\<bar>real (2 ^ N * p) / 2 ^ (N + q) - (x1 + x2) / 2\<bar> < (x2 - x1) / 64" .
```
```  1534             have "(1::real) / 2 ^ (N + q) \<le> 1/2^N"
```
```  1535               by (simp add: field_simps)
```
```  1536             also have "... < (x2 - x1) / 128"
```
```  1537               using N by force
```
```  1538             finally show "1/2 ^ (N + q) < (x2 - x1) / 128" .
```
```  1539           qed
```
```  1540         qed
```
```  1541         obtain m' n' m'' n'' where "0 < m'" "m' < 2 ^ n'" "x1 < m' / 2^n'" "m' / 2^n' < x2"
```
```  1542           and "0 < m''" "m'' < 2 ^ n''" "x1 < m'' / 2^n''" "m'' / 2^n'' < x2"
```
```  1543           and neq: "h (real m'' / 2^n'') \<noteq> h (real m' / 2^n')"
```
```  1544         proof
```
```  1545           show "0 < Suc (2*m)"
```
```  1546             by simp
```
```  1547           show m21: "Suc (2*m) < 2 ^ Suc n"
```
```  1548             using m by auto
```
```  1549           show "x1 < real (Suc (2 * m)) / 2 ^ Suc n"
```
```  1550             using clo by (simp add: field_simps abs_if split: if_split_asm)
```
```  1551           show "real (Suc (2 * m)) / 2 ^ Suc n < x2"
```
```  1552             using n clo by (simp add: field_simps abs_if split: if_split_asm)
```
```  1553           show "0 < 4*m + 3"
```
```  1554             by simp
```
```  1555           have "m+1 \<le> 2 ^ n"
```
```  1556             using m by simp
```
```  1557           then have "4 * (m+1) \<le> 4 * (2 ^ n)"
```
```  1558             by simp
```
```  1559           then show m43: "4*m + 3 < 2 ^ (n+2)"
```
```  1560             by (simp add: algebra_simps)
```
```  1561           show "x1 < real (4 * m + 3) / 2 ^ (n + 2)"
```
```  1562             using clo by (simp add: field_simps abs_if split: if_split_asm)
```
```  1563           show "real (4 * m + 3) / 2 ^ (n + 2) < x2"
```
```  1564             using n clo by (simp add: field_simps abs_if split: if_split_asm)
```
```  1565           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)"
```
```  1566             by (simp add: c_def)
```
```  1567           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))"
```
```  1568           have "R < b ((2 * real m + 1) / 2 ^ Suc n)"
```
```  1569             unfolding R_def  using a_less_b [of "4*m + 3" "n+2"] a43 [of "Suc n" m] b43 [of "Suc n" m]
```
```  1570             by simp
```
```  1571           then have Rless: "R < midpoint R (b ((2 * real m + 1) / 2 ^ Suc n))"
```
```  1572             by (simp add: midpoint_def)
```
```  1573           have midR_le: "midpoint R (b ((2 * real m + 1) / 2 ^ Suc n)) \<le> b ((2 * real m + 1) / (2 * 2 ^ n))"
```
```  1574             using \<open>R < b ((2 * real m + 1) / 2 ^ Suc n)\<close>
```
```  1575             by (simp add: midpoint_def)
```
```  1576           have "(real (Suc (2 * m)) / 2 ^ Suc n) \<in> D01"  "real (4 * m + 3) / 2 ^ (n + 2) \<in> D01"
```
```  1577             by (simp_all add: D01_def m21 m43 del: power_Suc of_nat_Suc of_nat_add add_2_eq_Suc') blast+
```
```  1578           then show "h (real (4 * m + 3) / 2 ^ (n + 2)) \<noteq> h (real (Suc (2 * m)) / 2 ^ Suc n)"
```
```  1579             using a_less_b [of "4*m + 3" "n+2", THEN conjunct1]
```
```  1580             using a43 [of "Suc n" m] b43 [of "Suc n" m]
```
```  1581             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"]
```
```  1582             apply (simp add: fc_eq [symmetric] c_def del: power_Suc)
```
```  1583             apply (simp only: add.commute [of 1] c_fold R_def [symmetric])
```
```  1584             apply (rule right_neq)
```
```  1585             using Rless apply (simp add: R_def)
```
```  1586                apply (rule midR_le, auto)
```
```  1587             done
```
```  1588         qed
```
```  1589         then show ?thesis by (metis that)
```
```  1590       qed
```
```  1591       have m_div: "0 < m / 2^n" "m / 2^n < 1"
```
```  1592         using m  by (auto simp: divide_simps)
```
```  1593       have closure0m: "{0..m / 2^n} = closure ({0<..< m / 2^n} \<inter> (\<Union>k m. {real m / 2 ^ k}))"
```
```  1594         by (subst closure_dyadic_rationals_in_convex_set_pos_1, simp_all add: not_le m)
```
```  1595       have closurem1: "{m / 2^n .. 1} = closure ({m / 2^n <..< 1} \<inter> (\<Union>k m. {real m / 2 ^ k}))"
```
```  1596         apply (subst closure_dyadic_rationals_in_convex_set_pos_1; simp add: not_le m)
```
```  1597         using \<open>0 < real m / 2 ^ n\<close> by linarith
```
```  1598       have cont_h': "continuous_on (closure ({u<..<v} \<inter> (\<Union>k m. {real m / 2 ^ k}))) h"
```
```  1599         if "0 \<le> u" "v \<le> 1" for u v
```
```  1600         apply (rule continuous_on_subset [OF cont_h])
```
```  1601         apply (rule closure_minimal [OF subsetI])
```
```  1602         using that apply auto
```
```  1603         done
```
```  1604       have closed_f': "closed (f ` {u..v})" if "0 \<le> u" "v \<le> 1" for u v
```
```  1605         by (metis compact_continuous_image cont_f compact_interval atLeastatMost_subset_iff
```
```  1606             compact_imp_closed continuous_on_subset that)
```
```  1607       have less_2I: "\<And>k i. real i / 2 ^ k < 1 \<Longrightarrow> i < 2 ^ k"
```
```  1608         by simp
```
```  1609       have "h ` ({0<..<m / 2 ^ n} \<inter> (\<Union>q p. {real p / 2 ^ q})) \<subseteq> f ` {0..c (m / 2 ^ n)}"
```
```  1610       proof clarsimp
```
```  1611         fix p q
```
```  1612         assume p: "0 < real p / 2 ^ q" "real p / 2 ^ q < real m / 2 ^ n"
```
```  1613         then have [simp]: "0 < p" "p < 2 ^ q"
```
```  1614            apply (simp add: divide_simps)
```
```  1615           apply (blast intro: p less_2I m_div less_trans)
```
```  1616           done
```
```  1617         have "f (c (real p / 2 ^ q)) \<in> f ` {0..c (real m / 2 ^ n)}"
```
```  1618           by (auto simp: clec p m)
```
```  1619         then show "h (real p / 2 ^ q) \<in> f ` {0..c (real m / 2 ^ n)}"
```
```  1620           by (simp add: h_eq)
```
```  1621       qed
```
```  1622       then have "h ` {0 .. m / 2^n} \<subseteq> f ` {0 .. c(m / 2^n)}"
```
```  1623         apply (subst closure0m)
```
```  1624         apply (rule image_closure_subset [OF cont_h' closed_f'])
```
```  1625         using m_div apply auto
```
```  1626         done
```
```  1627       then have hx1: "h x1 \<in> f ` {0 .. c(m / 2^n)}"
```
```  1628         using x12 less.prems(1) by auto
```
```  1629       then obtain t1 where t1: "h x1 = f t1" "0 \<le> t1" "t1 \<le> c (m / 2 ^ n)"
```
```  1630         by auto
```
```  1631       have "h ` ({m / 2 ^ n<..<1} \<inter> (\<Union>q p. {real p / 2 ^ q})) \<subseteq> f ` {c (m / 2 ^ n)..1}"
```
```  1632       proof clarsimp
```
```  1633         fix p q
```
```  1634         assume p: "real m / 2 ^ n < real p / 2 ^ q" and [simp]: "p < 2 ^ q"
```
```  1635         then have [simp]: "0 < p"
```
```  1636           using gr_zeroI m_div by fastforce
```
```  1637         have "f (c (real p / 2 ^ q)) \<in> f ` {c (m / 2 ^ n)..1}"
```
```  1638           by (auto simp: clec p m)
```
```  1639         then show "h (real p / 2 ^ q) \<in> f ` {c (real m / 2 ^ n)..1}"
```
```  1640           by (simp add: h_eq)
```
```  1641       qed
```
```  1642       then have "h ` {m / 2^n .. 1} \<subseteq> f ` {c(m / 2^n) .. 1}"
```
```  1643         apply (subst closurem1)
```
```  1644         apply (rule image_closure_subset [OF cont_h' closed_f'])
```
```  1645         using m apply auto
```
```  1646         done
```
```  1647       then have hx2: "h x2 \<in> f ` {c(m / 2^n)..1}"
```
```  1648         using x12 less.prems by auto
```
```  1649       then obtain t2 where t2: "h x2 = f t2" "c (m / 2 ^ n) \<le> t2" "t2 \<le> 1"
```
```  1650         by auto
```
```  1651       with t1 less neq have False
```
```  1652         using conn [of "h x2", unfolded is_interval_connected_1 [symmetric] is_interval_1, rule_format, of t1 t2 "c(m / 2^n)"]
```
```  1653         by (simp add: h_eq m)
```
```  1654       then show ?case by blast
```
```  1655     qed auto
```
```  1656     then show ?thesis
```
```  1657       by (auto simp: inj_on_def)
```
```  1658   qed
```
```  1659   ultimately have "{0..1::real} homeomorphic f ` {0..1}"
```
```  1660     using homeomorphic_compact [OF _ cont_h] by blast
```
```  1661   then show ?thesis
```
```  1662     using homeomorphic_sym by blast
```
```  1663 qed
```
```  1664
```
```  1665
```
```  1666 theorem%important path_contains_arc:
```
```  1667   fixes p :: "real \<Rightarrow> 'a::{complete_space,real_normed_vector}"
```
```  1668   assumes "path p" and a: "pathstart p = a" and b: "pathfinish p = b" and "a \<noteq> b"
```
```  1669   obtains q where "arc q" "path_image q \<subseteq> path_image p" "pathstart q = a" "pathfinish q = b"
```
```  1670 proof%unimportant -
```
```  1671   have ucont_p: "uniformly_continuous_on {0..1} p"
```
```  1672     using \<open>path p\<close> unfolding path_def
```
```  1673     by (metis compact_Icc compact_uniformly_continuous)
```
```  1674   define \<phi> where "\<phi> \<equiv> \<lambda>S. S \<subseteq> {0..1} \<and> 0 \<in> S \<and> 1 \<in> S \<and>
```
```  1675                            (\<forall>x \<in> S. \<forall>y \<in> S. open_segment x y \<inter> S = {} \<longrightarrow> p x = p y)"
```
```  1676   obtain T where "closed T" "\<phi> T" and T: "\<And>U. \<lbrakk>closed U; \<phi> U\<rbrakk> \<Longrightarrow> \<not> (U \<subset> T)"
```
```  1677   proof (rule Brouwer_reduction_theorem_gen [of "{0..1}" \<phi>])
```
```  1678     have *: "{x<..<y} \<inter> {0..1} = {x<..<y}" if "0 \<le> x" "y \<le> 1" "x \<le> y" for x y::real
```
```  1679       using that by auto
```
```  1680     show "\<phi> {0..1}"
```
```  1681       by (auto simp: \<phi>_def open_segment_eq_real_ivl *)
```
```  1682     show "\<phi> (\<Inter>(F ` UNIV))"
```
```  1683       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
```
```  1684     proof -
```
```  1685       have F01: "\<And>n. F n \<subseteq> {0..1} \<and> 0 \<in> F n \<and> 1 \<in> F n"
```
```  1686         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"
```
```  1687         by (metis \<phi> \<phi>_def)+
```
```  1688       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"
```
```  1689         for x y
```
```  1690         using that
```
```  1691       proof (induction x y rule: linorder_class.linorder_less_wlog)
```
```  1692         case (less x y)
```
```  1693         have xy: "x \<in> {0..1}" "y \<in> {0..1}"
```
```  1694           by (metis less.prems subsetCE F01)+
```
```  1695         have "norm(p x - p y) / 2 > 0"
```
```  1696           using less by auto
```
```  1697         then obtain e where "e > 0"
```
```  1698           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"
```
```  1699           by (metis uniformly_continuous_onE [OF ucont_p])
```
```  1700         have minxy: "min e (y - x)  < (y - x) * (3 / 2)"
```
```  1701           by (subst min_less_iff_disj) (simp add: less)
```
```  1702         obtain w z where "w < z" and w: "w \<in> {x<..<y}" and z: "z \<in> {x<..<y}"
```
```  1703           and wxe: "norm(w - x) < e" and zye: "norm(z - y) < e"
```
```  1704           apply (rule_tac w = "x + (min e (y - x) / 3)" and z = "y - (min e (y - x) / 3)" in that)
```
```  1705           using minxy \<open>0 < e\<close> less by simp_all
```
```  1706         have Fclo: "\<And>T. T \<in> range F \<Longrightarrow> closed T"
```
```  1707           by (metis \<open>\<And>n. closed (F n)\<close> image_iff)
```
```  1708         have eq: "{w..z} \<inter> \<Inter>(F ` UNIV) = {}"
```
```  1709           using less w z apply (auto simp: open_segment_eq_real_ivl)
```
```  1710           by (metis (no_types, hide_lams) INT_I IntI empty_iff greaterThanLessThan_iff not_le order.trans)
```
```  1711         then obtain K where "finite K" and K: "{w..z} \<inter> (\<Inter> (F ` K)) = {}"
```
```  1712           by (metis finite_subset_image compact_imp_fip [OF compact_interval Fclo])
```
```  1713         then have "K \<noteq> {}"
```
```  1714           using \<open>w < z\<close> \<open>{w..z} \<inter> \<Inter>(F ` K) = {}\<close> by auto
```
```  1715         define n where "n \<equiv> Max K"
```
```  1716         have "n \<in> K" unfolding n_def by (metis \<open>K \<noteq> {}\<close> \<open>finite K\<close> Max_in)
```
```  1717         have "F n \<subseteq> \<Inter> (F ` K)"
```
```  1718           unfolding n_def by (metis Fsub Max_ge \<open>K \<noteq> {}\<close> \<open>finite K\<close> cINF_greatest lift_Suc_antimono_le)
```
```  1719         with K have wzF_null: "{w..z} \<inter> F n = {}"
```
```  1720           by (metis disjoint_iff_not_equal subset_eq)
```
```  1721         obtain u where u: "u \<in> F n" "u \<in> {x..w}" "({u..w} - {u}) \<inter> F n = {}"
```
```  1722         proof (cases "w \<in> F n")
```
```  1723           case True
```
```  1724           then show ?thesis
```
```  1725             by (metis wzF_null \<open>w < z\<close> atLeastAtMost_iff disjoint_iff_not_equal less_eq_real_def)
```
```  1726         next
```
```  1727           case False
```
```  1728           obtain u where "u \<in> F n" "u \<in> {x..w}" "{u<..<w} \<inter> F n = {}"
```
```  1729           proof (rule segment_to_point_exists [of "F n \<inter> {x..w}" w])
```
```  1730             show "closed (F n \<inter> {x..w})"
```
```  1731               by (metis \<open>\<And>n. closed (F n)\<close> closed_Int closed_real_atLeastAtMost)
```
```  1732             show "F n \<inter> {x..w} \<noteq> {}"
```
```  1733               by (metis atLeastAtMost_iff disjoint_iff_not_equal greaterThanLessThan_iff less.prems(1) less_eq_real_def w)
```
```  1734           qed (auto simp: open_segment_eq_real_ivl intro!: that)
```
```  1735           with False show thesis
```
```  1736             apply (auto simp: disjoint_iff_not_equal intro!: that)
```
```  1737             by (metis greaterThanLessThan_iff less_eq_real_def)
```
```  1738         qed
```
```  1739         obtain v where v: "v \<in> F n" "v \<in> {z..y}" "({z..v} - {v}) \<inter> F n = {}"
```
```  1740         proof (cases "z \<in> F n")
```
```  1741           case True
```
```  1742           have "z \<in> {w..z}"
```
```  1743             using \<open>w < z\<close> by auto
```
```  1744           then show ?thesis
```
```  1745             by (metis wzF_null Int_iff True empty_iff)
```
```  1746         next
```
```  1747           case False
```
```  1748           show ?thesis
```
```  1749           proof (rule segment_to_point_exists [of "F n \<inter> {z..y}" z])
```
```  1750             show "closed (F n \<inter> {z..y})"
```
```  1751               by (metis \<open>\<And>n. closed (F n)\<close> closed_Int closed_atLeastAtMost)
```
```  1752             show "F n \<inter> {z..y} \<noteq> {}"
```
```  1753               by (metis atLeastAtMost_iff disjoint_iff_not_equal greaterThanLessThan_iff less.prems(2) less_eq_real_def z)
```
```  1754             show "\<And>b. \<lbrakk>b \<in> F n \<inter> {z..y}; open_segment z b \<inter> (F n \<inter> {z..y}) = {}\<rbrakk> \<Longrightarrow> thesis"
```
```  1755               apply (rule that)
```
```  1756                 apply (auto simp: open_segment_eq_real_ivl)
```
```  1757               by (metis DiffI Int_iff atLeastAtMost_diff_ends atLeastAtMost_iff atLeastatMost_empty_iff empty_iff insert_iff False)
```
```  1758           qed
```
```  1759         qed
```
```  1760         obtain u v where "u \<in> {0..1}" "v \<in> {0..1}" "norm(u - x) < e" "norm(v - y) < e" "p u = p v"
```
```  1761         proof
```
```  1762           show "u \<in> {0..1}" "v \<in> {0..1}"
```
```  1763             by (metis F01 \<open>u \<in> F n\<close> \<open>v \<in> F n\<close> subsetD)+
```
```  1764           show "norm(u - x) < e" "norm (v - y) < e"
```
```  1765             using \<open>u \<in> {x..w}\<close> \<open>v \<in> {z..y}\<close> atLeastAtMost_iff real_norm_def wxe zye by auto
```
```  1766           show "p u = p v"
```
```  1767           proof (rule peq)
```
```  1768             show "u \<in> F n" "v \<in> F n"
```
```  1769               by (auto simp: u v)
```
```  1770             have "False" if "\<xi> \<in> F n" "u < \<xi>" "\<xi> < v" for \<xi>
```
```  1771             proof -
```
```  1772               have "\<xi> \<notin> {z..v}"
```
```  1773                 by (metis DiffI disjoint_iff_not_equal less_irrefl singletonD that v(3))
```
```  1774               moreover have "\<xi> \<notin> {w..z} \<inter> F n"
```
```  1775                 by (metis equals0D wzF_null)
```
```  1776               ultimately have "\<xi> \<in> {u..w}"
```
```  1777                 using that by auto
```
```  1778               then show ?thesis
```
```  1779                 by (metis DiffI disjoint_iff_not_equal less_eq_real_def not_le singletonD that u(3))
```
```  1780             qed
```
```  1781             moreover
```
```  1782             have "\<lbrakk>\<xi> \<in> F n; v < \<xi>; \<xi> < u\<rbrakk> \<Longrightarrow> False" for \<xi>
```
```  1783               using \<open>u \<in> {x..w}\<close> \<open>v \<in> {z..y}\<close> \<open>w < z\<close> by simp
```
```  1784             ultimately
```
```  1785             show "open_segment u v \<inter> F n = {}"
```
```  1786               by (force simp: open_segment_eq_real_ivl)
```
```  1787           qed
```
```  1788         qed
```
```  1789         then show ?case
```
```  1790           using e [of x u] e [of y v] xy
```
```  1791           apply (simp add: open_segment_eq_real_ivl dist_norm del: divide_const_simps)
```
```  1792           by (metis dist_norm dist_triangle_half_r less_irrefl)
```
```  1793       qed (auto simp: open_segment_commute)
```
```  1794       show ?thesis
```
```  1795         unfolding \<phi>_def by (metis (no_types, hide_lams) INT_I Inf_lower2 rangeI that F01 subsetCE pqF)
```
```  1796     qed
```
```  1797     show "closed {0..1::real}" by auto
```
```  1798   qed (meson \<phi>_def)
```
```  1799   then have "T \<subseteq> {0..1}" "0 \<in> T" "1 \<in> T"
```
```  1800     and peq: "\<And>x y. \<lbrakk>x \<in> T; y \<in> T; open_segment x y \<inter> T = {}\<rbrakk> \<Longrightarrow> p x = p y"
```
```  1801     unfolding \<phi>_def by metis+
```
```  1802   then have "T \<noteq> {}" by auto
```
```  1803   define h where "h \<equiv> \<lambda>x. p(SOME y. y \<in> T \<and> open_segment x y \<inter> T = {})"
```
```  1804   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 = {}"
```
```  1805     for x y z
```
```  1806   proof (cases "x \<in> T")
```
```  1807     case True
```
```  1808     with that show ?thesis by (metis \<open>\<phi> T\<close> \<phi>_def)
```
```  1809   next
```
```  1810     case False
```
```  1811     have "insert x (open_segment x y \<union> open_segment x z) \<inter> T = {}"
```
```  1812       by (metis False Int_Un_distrib2 Int_insert_left Un_empty_right xyT xzT)
```
```  1813     moreover have "open_segment y z \<inter> T \<subseteq> insert x (open_segment x y \<union> open_segment x z) \<inter> T"
```
```  1814       apply auto
```
```  1815       by (metis greaterThanLessThan_iff less_eq_real_def less_le_trans linorder_neqE_linordered_idom open_segment_eq_real_ivl)
```
```  1816     ultimately have "open_segment y z \<inter> T = {}"
```
```  1817       by blast
```
```  1818     with that peq show ?thesis by metis
```
```  1819   qed
```
```  1820   then have h_eq_p_gen: "h x = p y" if "y \<in> T" "open_segment x y \<inter> T = {}" for x y
```
```  1821     using that unfolding h_def
```
```  1822     by (metis (mono_tags, lifting) some_eq_ex)
```
```  1823   then have h_eq_p: "\<And>x. x \<in> T \<Longrightarrow> h x = p x"
```
```  1824     by simp
```
```  1825   have disjoint: "\<And>x. \<exists>y. y \<in> T \<and> open_segment x y \<inter> T = {}"
```
```  1826     by (meson \<open>T \<noteq> {}\<close> \<open>closed T\<close> segment_to_point_exists)
```
```  1827   have heq: "h x = h x'" if "open_segment x x' \<inter> T = {}" for x x'
```
```  1828   proof (cases "x \<in> T \<or> x' \<in> T")
```
```  1829     case True
```
```  1830     then show ?thesis
```
```  1831       by (metis h_eq_p h_eq_p_gen open_segment_commute that)
```
```  1832   next
```
```  1833     case False
```
```  1834     obtain y y' where "y \<in> T" "open_segment x y \<inter> T = {}" "h x = p y"
```
```  1835       "y' \<in> T" "open_segment x' y' \<inter> T = {}" "h x' = p y'"
```
```  1836       by (meson disjoint h_eq_p_gen)
```
```  1837     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')))"
```
```  1838       by (auto simp: open_segment_eq_real_ivl)
```
```  1839     ultimately show ?thesis
```
```  1840       using False that by (fastforce simp add: h_eq_p intro!: peq)
```
```  1841   qed
```
```  1842   have "h ` {0..1} homeomorphic {0..1::real}"
```
```  1843   proof (rule homeomorphic_monotone_image_interval)
```
```  1844     show "continuous_on {0..1} h"
```
```  1845     proof (clarsimp simp add: continuous_on_iff)
```
```  1846       fix u \<epsilon>::real
```
```  1847       assume "0 < \<epsilon>" "0 \<le> u" "u \<le> 1"
```
```  1848       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"
```
```  1849         using ucont_p [unfolded uniformly_continuous_on_def]
```
```  1850         by (metis atLeastAtMost_iff half_gt_zero_iff)
```
```  1851       then have "dist (h v) (h u) < \<epsilon>" if "v \<in> {0..1}" "dist v u < \<delta>" for v
```
```  1852       proof (cases "open_segment u v \<inter> T = {}")
```
```  1853         case True
```
```  1854         then show ?thesis
```
```  1855           using \<open>0 < \<epsilon>\<close> heq by auto
```
```  1856       next
```
```  1857         case False
```
```  1858         have uvT: "closed (closed_segment u v \<inter> T)" "closed_segment u v \<inter> T \<noteq> {}"
```
```  1859           using False open_closed_segment by (auto simp: \<open>closed T\<close> closed_Int)
```
```  1860         obtain w where "w \<in> T" and w: "w \<in> closed_segment u v" "open_segment u w \<inter> T = {}"
```
```  1861           apply (rule segment_to_point_exists [OF uvT, of u])
```
```  1862           by (metis IntD1 Int_commute Int_left_commute ends_in_segment(1) inf.orderE subset_oc_segment)
```
```  1863         then have puw: "dist (p u) (p w) < \<epsilon> / 2"
```
```  1864           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)
```
```  1865         obtain z where "z \<in> T" and z: "z \<in> closed_segment u v" "open_segment v z \<inter> T = {}"
```
```  1866           apply (rule segment_to_point_exists [OF uvT, of v])
```
```  1867           by (metis IntD2 Int_commute Int_left_commute ends_in_segment(2) inf.orderE subset_oc_segment)
```
```  1868         then have "dist (p u) (p z) < \<epsilon> / 2"
```
```  1869           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)
```
```  1870         then show ?thesis
```
```  1871           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))
```
```  1872       qed
```
```  1873       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
```
```  1874     qed
```
```  1875     show "connected ({0..1} \<inter> h -` {z})" for z
```
```  1876     proof (clarsimp simp add: connected_iff_connected_component)
```
```  1877       fix u v
```
```  1878       assume huv_eq: "h v = h u" and uv: "0 \<le> u" "u \<le> 1" "0 \<le> v" "v \<le> 1"
```
```  1879       have "\<exists>T. connected T \<and> T \<subseteq> {0..1} \<and> T \<subseteq> h -` {h u} \<and> u \<in> T \<and> v \<in> T"
```
```  1880       proof (intro exI conjI)
```
```  1881         show "connected (closed_segment u v)"
```
```  1882           by simp
```
```  1883         show "closed_segment u v \<subseteq> {0..1}"
```
```  1884           by (simp add: uv closed_segment_eq_real_ivl)
```
```  1885         have pxy: "p x = p y"
```
```  1886           if "T \<subseteq> {0..1}" "0 \<in> T" "1 \<in> T" "x \<in> T" "y \<in> T"
```
```  1887           and disjT: "open_segment x y \<inter> (T - open_segment u v) = {}"
```
```  1888           and xynot: "x \<notin> open_segment u v" "y \<notin> open_segment u v"
```
```  1889           for x y
```
```  1890         proof (cases "open_segment x y \<inter> open_segment u v = {}")
```
```  1891           case True
```
```  1892           then show ?thesis
```
```  1893             by (metis Diff_Int_distrib Diff_empty peq disjT \<open>x \<in> T\<close> \<open>y \<in> T\<close>)
```
```  1894         next
```
```  1895           case False
```
```  1896           then have "open_segment x u \<union> open_segment y v \<subseteq> open_segment x y - open_segment u v \<or>
```
```  1897                      open_segment y u \<union> open_segment x v \<subseteq> open_segment x y - open_segment u v" (is "?xuyv \<or> ?yuxv")
```
```  1898             using xynot by (fastforce simp add: open_segment_eq_real_ivl not_le not_less split: if_split_asm)
```
```  1899           then show "p x = p y"
```
```  1900           proof
```
```  1901             assume "?xuyv"
```
```  1902             then have "open_segment x u \<inter> T = {}" "open_segment y v \<inter> T = {}"
```
```  1903               using disjT by auto
```
```  1904             then have "h x = h y"
```
```  1905               using heq huv_eq by auto
```
```  1906             then show ?thesis
```
```  1907               using h_eq_p \<open>x \<in> T\<close> \<open>y \<in> T\<close> by auto
```
```  1908           next
```
```  1909             assume "?yuxv"
```
```  1910             then have "open_segment y u \<inter> T = {}" "open_segment x v \<inter> T = {}"
```
```  1911               using disjT by auto
```
```  1912             then have "h x = h y"
```
```  1913               using heq [of y u]  heq [of x v] huv_eq by auto
```
```  1914             then show ?thesis
```
```  1915               using h_eq_p \<open>x \<in> T\<close> \<open>y \<in> T\<close> by auto
```
```  1916           qed
```
```  1917         qed
```
```  1918         have "\<not> T - open_segment u v \<subset> T"
```
```  1919         proof (rule T)
```
```  1920           show "closed (T - open_segment u v)"
```
```  1921             by (simp add: closed_Diff [OF \<open>closed T\<close>] open_segment_eq_real_ivl)
```
```  1922           have "0 \<notin> open_segment u v" "1 \<notin> open_segment u v"
```
```  1923             using open_segment_eq_real_ivl uv by auto
```
```  1924           then show "\<phi> (T - open_segment u v)"
```
```  1925             using \<open>T \<subseteq> {0..1}\<close> \<open>0 \<in> T\<close> \<open>1 \<in> T\<close>
```
```  1926             by (auto simp: \<phi>_def) (meson peq pxy)
```
```  1927         qed
```
```  1928         then have "open_segment u v \<inter> T = {}"
```
```  1929           by blast
```
```  1930         then show "closed_segment u v \<subseteq> h -` {h u}"
```
```  1931           by (force intro: heq simp: open_segment_eq_real_ivl closed_segment_eq_real_ivl split: if_split_asm)+
```
```  1932       qed auto
```
```  1933       then show "connected_component ({0..1} \<inter> h -` {h u}) u v"
```
```  1934         by (simp add: connected_component_def)
```
```  1935     qed
```
```  1936     show "h 1 \<noteq> h 0"
```
```  1937       by (metis \<open>\<phi> T\<close> \<phi>_def a \<open>a \<noteq> b\<close> b h_eq_p pathfinish_def pathstart_def)
```
```  1938   qed
```
```  1939   then obtain f and g :: "real \<Rightarrow> 'a"
```
```  1940     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"
```
```  1941       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"
```
```  1942     by (auto simp: homeomorphic_def homeomorphism_def path_image_def)
```
```  1943   then have "arc g"
```
```  1944     by (metis arc_def path_def inj_on_def)
```
```  1945   obtain u v where "u \<in> {0..1}" "a = g u" "v \<in> {0..1}" "b = g v"
```
```  1946     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)
```
```  1947   then have "a \<in> path_image g" "b \<in> path_image g"
```
```  1948     using path_image_def by blast+
```
```  1949   have ph: "path_image h \<subseteq> path_image p"
```
```  1950     by (metis image_mono image_subset_iff path_image_def disjoint h_eq_p_gen \<open>T \<subseteq> {0..1}\<close>)
```
```  1951   show ?thesis
```
```  1952   proof
```
```  1953     show "pathstart (subpath u v g) = a" "pathfinish (subpath u v g) = b"
```
```  1954       by (simp_all add: \<open>a = g u\<close> \<open>b = g v\<close>)
```
```  1955     show "path_image (subpath u v g) \<subseteq> path_image p"
```
```  1956       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)
```
```  1957     show "arc (subpath u v g)"
```
```  1958       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
```
```  1959   qed
```
```  1960 qed
```
```  1961
```
```  1962
```
```  1963 corollary%important path_connected_arcwise:
```
```  1964   fixes S :: "'a::{complete_space,real_normed_vector} set"
```
```  1965   shows "path_connected S \<longleftrightarrow>
```
```  1966          (\<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))"
```
```  1967         (is "?lhs = ?rhs")
```
```  1968 proof%unimportant (intro iffI impI ballI)
```
```  1969   fix x y
```
```  1970   assume "path_connected S" "x \<in> S" "y \<in> S" "x \<noteq> y"
```
```  1971   then obtain p where p: "path p" "path_image p \<subseteq> S" "pathstart p = x" "pathfinish p = y"
```
```  1972     by (force simp: path_connected_def)
```
```  1973   then show "\<exists>g. arc g \<and> path_image g \<subseteq> S \<and> pathstart g = x \<and> pathfinish g = y"
```
```  1974     by (metis \<open>x \<noteq> y\<close> order_trans path_contains_arc)
```
```  1975 next
```
```  1976   assume R [rule_format]: ?rhs
```
```  1977   show ?lhs
```
```  1978     unfolding path_connected_def
```
```  1979   proof (intro ballI)
```
```  1980     fix x y
```
```  1981     assume "x \<in> S" "y \<in> S"
```
```  1982     show "\<exists>g. path g \<and> path_image g \<subseteq> S \<and> pathstart g = x \<and> pathfinish g = y"
```
```  1983     proof (cases "x = y")
```
```  1984       case True with \<open>x \<in> S\<close> path_component_def path_component_refl show ?thesis
```
```  1985         by blast
```
```  1986     next
```
```  1987       case False with R [OF \<open>x \<in> S\<close> \<open>y \<in> S\<close>] show ?thesis
```
```  1988         by (auto intro: arc_imp_path)
```
```  1989     qed
```
```  1990   qed
```
```  1991 qed
```
```  1992
```
```  1993
```
```  1994 corollary%important arc_connected_trans:
```
```  1995   fixes g :: "real \<Rightarrow> 'a::{complete_space,real_normed_vector}"
```
```  1996   assumes "arc g" "arc h" "pathfinish g = pathstart h" "pathstart g \<noteq> pathfinish h"
```
```  1997   obtains i where "arc i" "path_image i \<subseteq> path_image g \<union> path_image h"
```
```  1998                   "pathstart i = pathstart g" "pathfinish i = pathfinish h"
```
```  1999   by%unimportant (metis (no_types, hide_lams) arc_imp_path assms path_contains_arc path_image_join path_join pathfinish_join pathstart_join)
```
```  2000
```
```  2001
```
```  2002
```
```  2003
```
```  2004 subsection%important\<open>Accessibility of frontier points\<close>
```
```  2005
```
```  2006 lemma%important dense_accessible_frontier_points:
```
```  2007   fixes S :: "'a::{complete_space,real_normed_vector} set"
```
```  2008   assumes "open S" and opeSV: "openin (subtopology euclidean (frontier S)) V" and "V \<noteq> {}"
```
```  2009   obtains g where "arc g" "g ` {0..<1} \<subseteq> S" "pathstart g \<in> S" "pathfinish g \<in> V"
```
```  2010 proof%unimportant -
```
```  2011   obtain z where "z \<in> V"
```
```  2012     using \<open>V \<noteq> {}\<close> by auto
```
```  2013   then obtain r where "r > 0" and r: "ball z r \<inter> frontier S \<subseteq> V"
```
```  2014     by (metis openin_contains_ball opeSV)
```
```  2015   then have "z \<in> frontier S"
```
```  2016     using \<open>z \<in> V\<close> opeSV openin_contains_ball by blast
```
```  2017   then have "z \<in> closure S" "z \<notin> S"
```
```  2018     by (simp_all add: frontier_def assms interior_open)
```
```  2019   with \<open>r > 0\<close> have "infinite (S \<inter> ball z r)"
```
```  2020     by (auto simp: closure_def islimpt_eq_infinite_ball)
```
```  2021   then obtain y where "y \<in> S" and y: "y \<in> ball z r"
```
```  2022     using infinite_imp_nonempty by force
```
```  2023   then have "y \<notin> frontier S"
```
```  2024     by (meson \<open>open S\<close> disjoint_iff_not_equal frontier_disjoint_eq)
```
```  2025   have "y \<noteq> z"
```
```  2026     using \<open>y \<in> S\<close> \<open>z \<notin> S\<close> by blast
```
```  2027   have "path_connected(ball z r)"
```
```  2028     by (simp add: convex_imp_path_connected)
```
```  2029   with y \<open>r > 0\<close>  obtain g where "arc g" and pig: "path_image g \<subseteq> ball z r"
```
```  2030                                  and g: "pathstart g = y" "pathfinish g = z"
```
```  2031     using \<open>y \<noteq> z\<close> by (force simp: path_connected_arcwise)
```
```  2032   have "compact (g -` frontier S \<inter> {0..1})"
```
```  2033     apply (simp add: compact_eq_bounded_closed bounded_Int bounded_closed_interval)
```
```  2034      apply (rule closed_vimage_Int)
```
```  2035     using \<open>arc g\<close> apply (auto simp: arc_def path_def)
```
```  2036     done
```
```  2037   moreover have "g -` frontier S \<inter> {0..1} \<noteq> {}"
```
```  2038   proof -
```
```  2039     have "\<exists>r. r \<in> g -` frontier S \<and> r \<in> {0..1}"
```
```  2040       by (metis \<open>z \<in> frontier S\<close> g(2) imageE path_image_def pathfinish_in_path_image vimageI2)
```
```  2041     then show ?thesis
```
```  2042       by blast
```
```  2043   qed
```
```  2044   ultimately obtain t where gt: "g t \<in> frontier S" and "0 \<le> t" "t \<le> 1"
```
```  2045                 and t: "\<And>u. \<lbrakk>g u \<in> frontier S; 0 \<le> u; u \<le> 1\<rbrakk> \<Longrightarrow> t \<le> u"
```
```  2046     by (force simp: dest!: compact_attains_inf)
```
```  2047   moreover have "t \<noteq> 0"
```
```  2048     by (metis \<open>y \<notin> frontier S\<close> g(1) gt pathstart_def)
```
```  2049   ultimately have  t01: "0 < t" "t \<le> 1"
```
```  2050     by auto
```
```  2051   have "V \<subseteq> frontier S"
```
```  2052     using opeSV openin_contains_ball by blast
```
```  2053   show ?thesis
```
```  2054   proof
```
```  2055     show "arc (subpath 0 t g)"
```
```  2056       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)
```
```  2057     have "g 0 \<in> S"
```
```  2058       by (metis \<open>y \<in> S\<close> g(1) pathstart_def)
```
```  2059     then show "pathstart (subpath 0 t g) \<in> S"
```
```  2060       by auto
```
```  2061     have "g t \<in> V"
```
```  2062       by (metis IntI atLeastAtMost_iff gt image_eqI path_image_def pig r subsetCE \<open>0 \<le> t\<close> \<open>t \<le> 1\<close>)
```
```  2063     then show "pathfinish (subpath 0 t g) \<in> V"
```
```  2064       by auto
```
```  2065     then have "inj_on (subpath 0 t g) {0..1}"
```
```  2066       using t01
```
```  2067       apply (clarsimp simp: inj_on_def subpath_def)
```
```  2068       apply (drule inj_onD [OF arc_imp_inj_on [OF \<open>arc g\<close>]])
```
```  2069       using mult_le_one apply auto
```
```  2070       done
```
```  2071     then have "subpath 0 t g ` {0..<1} \<subseteq> subpath 0 t g ` {0..1} - {subpath 0 t g 1}"
```
```  2072       by (force simp: dest: inj_onD)
```
```  2073     moreover have False if "subpath 0 t g ` ({0..<1}) - S \<noteq> {}"
```
```  2074     proof -
```
```  2075       have contg: "continuous_on {0..1} g"
```
```  2076         using \<open>arc g\<close> by (auto simp: arc_def path_def)
```
```  2077       have "subpath 0 t g ` {0..<1} \<inter> frontier S \<noteq> {}"
```
```  2078       proof (rule connected_Int_frontier [OF _ _ that])
```
```  2079         show "connected (subpath 0 t g ` {0..<1})"
```
```  2080           apply (rule connected_continuous_image)
```
```  2081            apply (simp add: subpath_def)
```
```  2082            apply (intro continuous_intros continuous_on_compose2 [OF contg])
```
```  2083            apply (auto simp: \<open>0 \<le> t\<close> \<open>t \<le> 1\<close> mult_le_one)
```
```  2084           done
```
```  2085         show "subpath 0 t g ` {0..<1} \<inter> S \<noteq> {}"
```
```  2086           using \<open>y \<in> S\<close> g(1) by (force simp: subpath_def image_def pathstart_def)
```
```  2087       qed
```
```  2088       then obtain x where "x \<in> subpath 0 t g ` {0..<1}" "x \<in> frontier S"
```
```  2089         by blast
```
```  2090       with t01 \<open>0 \<le> t\<close> mult_le_one t show False
```
```  2091         by (fastforce simp: subpath_def)
```
```  2092     qed
```
```  2093     then have "subpath 0 t g ` {0..1} - {subpath 0 t g 1} \<subseteq> S"
```
```  2094       using subsetD by fastforce
```
```  2095     ultimately  show "subpath 0 t g ` {0..<1} \<subseteq> S"
```
```  2096       by auto
```
```  2097   qed
```
```  2098 qed
```
```  2099
```
```  2100
```
```  2101 lemma%important dense_accessible_frontier_points_connected:
```
```  2102   fixes S :: "'a::{complete_space,real_normed_vector} set"
```
```  2103   assumes "open S" "connected S" "x \<in> S" "V \<noteq> {}"
```
```  2104       and ope: "openin (subtopology euclidean (frontier S)) V"
```
```  2105   obtains g where "arc g" "g ` {0..<1} \<subseteq> S" "pathstart g = x" "pathfinish g \<in> V"
```
```  2106 proof%unimportant -
```
```  2107   have "V \<subseteq> frontier S"
```
```  2108     using ope openin_imp_subset by blast
```
```  2109   with \<open>open S\<close> \<open>x \<in> S\<close> have "x \<notin> V"
```
```  2110     using interior_open by (auto simp: frontier_def)
```
```  2111   obtain g where "arc g" and g: "g ` {0..<1} \<subseteq> S" "pathstart g \<in> S" "pathfinish g \<in> V"
```
```  2112     by (metis dense_accessible_frontier_points [OF \<open>open S\<close> ope \<open>V \<noteq> {}\<close>])
```
```  2113   then have "path_connected S"
```
```  2114     by (simp add: assms connected_open_path_connected)
```
```  2115   with \<open>pathstart g \<in> S\<close> \<open>x \<in> S\<close> have "path_component S x (pathstart g)"
```
```  2116     by (simp add: path_connected_component)
```
```  2117   then obtain f where "path f" and f: "path_image f \<subseteq> S" "pathstart f = x" "pathfinish f = pathstart g"
```
```  2118     by (auto simp: path_component_def)
```
```  2119   then have "path (f +++ g)"
```
```  2120     by (simp add: \<open>arc g\<close> arc_imp_path)
```
```  2121   then obtain h where "arc h"
```
```  2122                   and h: "path_image h \<subseteq> path_image (f +++ g)" "pathstart h = x" "pathfinish h = pathfinish g"
```
```  2123     apply (rule path_contains_arc [of "f +++ g" x "pathfinish g"])
```
```  2124     using f \<open>x \<notin> V\<close> \<open>pathfinish g \<in> V\<close> by auto
```
```  2125   have "h ` {0..1} - {h 1} \<subseteq> S"
```
```  2126     using f g h apply (clarsimp simp: path_image_join)
```
```  2127     apply (simp add: path_image_def pathfinish_def subset_iff image_def Bex_def)
```
```  2128     by (metis le_less)
```
```  2129   then have "h ` {0..<1} \<subseteq> S"
```
```  2130     using \<open>arc h\<close> by (force simp: arc_def dest: inj_onD)
```
```  2131   then show thesis
```
```  2132     apply (rule that [OF \<open>arc h\<close>])
```
```  2133     using h \<open>pathfinish g \<in> V\<close> by auto
```
```  2134 qed
```
```  2135
```
```  2136 lemma%important dense_access_fp_aux:
```
```  2137   fixes S :: "'a::{complete_space,real_normed_vector} set"
```
```  2138   assumes S: "open S" "connected S"
```
```  2139       and opeSU: "openin (subtopology euclidean (frontier S)) U"
```
```  2140       and opeSV: "openin (subtopology euclidean (frontier S)) V"
```
```  2141       and "V \<noteq> {}" "\<not> U \<subseteq> V"
```
```  2142   obtains g where "arc g" "pathstart g \<in> U" "pathfinish g \<in> V" "g ` {0<..<1} \<subseteq> S"
```
```  2143 proof%unimportant -
```
```  2144   have "S \<noteq> {}"
```
```  2145     using opeSV \<open>V \<noteq> {}\<close> by (metis frontier_empty openin_subtopology_empty)
```
```  2146   then obtain x where "x \<in> S" by auto
```
```  2147   obtain g where "arc g" and g: "g ` {0..<1} \<subseteq> S" "pathstart g = x" "pathfinish g \<in> V"
```
```  2148     using dense_accessible_frontier_points_connected [OF S \<open>x \<in> S\<close> \<open>V \<noteq> {}\<close> opeSV] by blast
```
```  2149   obtain h where "arc h" and h: "h ` {0..<1} \<subseteq> S" "pathstart h = x" "pathfinish h \<in> U - {pathfinish g}"
```
```  2150   proof (rule dense_accessible_frontier_points_connected [OF S \<open>x \<in> S\<close>])
```
```  2151     show "U - {pathfinish g} \<noteq> {}"
```
```  2152       using \<open>pathfinish g \<in> V\<close> \<open>\<not> U \<subseteq> V\<close> by blast
```
```  2153     show "openin (subtopology euclidean (frontier S)) (U - {pathfinish g})"
```
```  2154       by (simp add: opeSU openin_delete)
```
```  2155   qed auto
```
```  2156   obtain \<gamma> where "arc \<gamma>"
```
```  2157              and \<gamma>: "path_image \<gamma> \<subseteq> path_image (reversepath h +++ g)"
```
```  2158                     "pathstart \<gamma> = pathfinish h" "pathfinish \<gamma> = pathfinish g"
```
```  2159   proof (rule path_contains_arc [of "(reversepath h +++ g)" "pathfinish h" "pathfinish g"])
```
```  2160     show "path (reversepath h +++ g)"
```
```  2161       by (simp add: \<open>arc g\<close> \<open>arc h\<close> \<open>pathstart g = x\<close> \<open>pathstart h = x\<close> arc_imp_path)
```
```  2162     show "pathstart (reversepath h +++ g) = pathfinish h"
```
```  2163          "pathfinish (reversepath h +++ g) = pathfinish g"
```
```  2164       by auto
```
```  2165     show "pathfinish h \<noteq> pathfinish g"
```
```  2166       using \<open>pathfinish h \<in> U - {pathfinish g}\<close> by auto
```
```  2167   qed auto
```
```  2168   show ?thesis
```
```  2169   proof
```
```  2170     show "arc \<gamma>" "pathstart \<gamma> \<in> U" "pathfinish \<gamma> \<in> V"
```
```  2171       using \<gamma> \<open>arc \<gamma>\<close> \<open>pathfinish h \<in> U - {pathfinish g}\<close>  \<open>pathfinish g \<in> V\<close> by auto
```
```  2172     have "\<gamma> ` {0..1} - {\<gamma> 0, \<gamma> 1} \<subseteq> S"
```
```  2173       using \<gamma> g h
```
```  2174       apply (simp add: path_image_join)
```
```  2175       apply (simp add: path_image_def pathstart_def pathfinish_def subset_iff image_def Bex_def)
```
```  2176       by (metis linorder_neqE_linordered_idom not_less)
```
```  2177     then show "\<gamma> ` {0<..<1} \<subseteq> S"
```
```  2178       using \<open>arc h\<close> \<open>arc \<gamma>\<close>
```
```  2179       by (metis arc_imp_simple_path path_image_def pathfinish_def pathstart_def simple_path_endless)
```
```  2180   qed
```
```  2181 qed
```
```  2182
```
```  2183 lemma%important dense_accessible_frontier_point_pairs:
```
```  2184   fixes S :: "'a::{complete_space,real_normed_vector} set"
```
```  2185   assumes S: "open S" "connected S"
```
```  2186       and opeSU: "openin (subtopology euclidean (frontier S)) U"
```
```  2187       and opeSV: "openin (subtopology euclidean (frontier S)) V"
```
```  2188       and "U \<noteq> {}" "V \<noteq> {}" "U \<noteq> V"
```
```  2189     obtains g where "arc g" "pathstart g \<in> U" "pathfinish g \<in> V" "g ` {0<..<1} \<subseteq> S"
```
```  2190 proof%unimportant -
```
```  2191   consider "\<not> U \<subseteq> V" | "\<not> V \<subseteq> U"
```
```  2192     using \<open>U \<noteq> V\<close> by blast
```
```  2193   then show ?thesis
```
```  2194   proof cases
```
```  2195     case 1 then show ?thesis
```
```  2196       using assms dense_access_fp_aux [OF S opeSU opeSV] that by blast
```
```  2197   next
```
```  2198     case 2
```
```  2199     obtain g where "arc g" and g: "pathstart g \<in> V" "pathfinish g \<in> U" "g ` {0<..<1} \<subseteq> S"
```
```  2200       using assms dense_access_fp_aux [OF S opeSV opeSU] "2" by blast
```
```  2201     show ?thesis
```
```  2202     proof
```
```  2203       show "arc (reversepath g)"
```
```  2204         by (simp add: \<open>arc g\<close> arc_reversepath)
```
```  2205       show "pathstart (reversepath g) \<in> U" "pathfinish (reversepath g) \<in> V"
```
```  2206         using g by auto
```
```  2207       show "reversepath g ` {0<..<1} \<subseteq> S"
```
```  2208         using g by (auto simp: reversepath_def)
```
```  2209     qed
```
```  2210   qed
```
```  2211 qed
```
```  2212
```
```  2213 end
```