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