Theory Arcwise_Connected

(*  Title:      HOL/Analysis/Arcwise_Connected.thy
    Authors:    LC Paulson, based on material from HOL Light
*)

section ‹Arcwise-Connected Sets›

theory Arcwise_Connected
imports Path_Connected Ordered_Euclidean_Space "HOL-Computational_Algebra.Primes"
begin

lemma path_connected_interval [simp]:
  fixes a b::"'a::ordered_euclidean_space"
  shows "path_connected {a..b}"
  using is_interval_cc is_interval_path_connected by blast

lemma segment_to_closest_point:
  fixes S :: "'a :: euclidean_space set"
  shows "closed S; S  {}  open_segment a (closest_point S a)  S = {}"
  unfolding disjoint_iff
  by (metis closest_point_le dist_commute dist_in_open_segment not_le)

lemma segment_to_point_exists:
  fixes S :: "'a :: euclidean_space set"
    assumes "closed S" "S  {}"
    obtains b where "b  S" "open_segment a b  S = {}"
  by (metis assms segment_to_closest_point closest_point_exists that)


subsection ‹The Brouwer reduction theorem›

theorem Brouwer_reduction_theorem_gen:
  fixes S :: "'a::euclidean_space set"
  assumes "closed S" "φ S"
      and φ: "F. n. closed(F n); n. φ(F n); n. F(Suc n)  F n  φ((range F))"
  obtains T where "T  S" "closed T" "φ T" "U. U  S; closed U; φ U  ¬ (U  T)"
proof -
  obtain B :: "nat  'a set"
    where "inj B" "n. open(B n)" and open_cov: "S. open S  K. S = (B ` K)"
      by (metis Setcompr_eq_image that univ_second_countable_sequence)
  define A where "A  rec_nat S (λn a. if U. U  a  closed U  φ U  U  (B n) = {}
                                        then SOME U. U  a  closed U  φ U  U  (B n) = {}
                                        else a)"
  have [simp]: "A 0 = S"
    by (simp add: A_def)
  have ASuc: "A(Suc n) = (if U. U  A n  closed U  φ U  U  (B n) = {}
                          then SOME U. U  A n  closed U  φ U  U  (B n) = {}
                          else A n)" for n
    by (auto simp: A_def)
  have sub: "n. A(Suc n)  A n"
    by (auto simp: ASuc dest!: someI_ex)
  have subS: "A n  S" for n
    by (induction n) (use sub in auto)
  have clo: "closed (A n)  φ (A n)" for n
    by (induction n) (auto simp: assms ASuc dest!: someI_ex)
  show ?thesis
  proof
    show "(range A)  S"
      using n. A n  S by blast
    show "closed ((A ` UNIV))"
      using clo by blast
    show "φ ((A ` UNIV))"
      by (simp add: clo φ sub)
    show "¬ U  (A ` UNIV)" if "U  S" "closed U" "φ U" for U
    proof -
      have "y. x  A y" if "x  U" and Usub: "U  (x. A x)" for x
      proof -
        obtain e where "e > 0" and e: "ball x e  -U"
          using closed U x  U openE [of "-U"] by blast
        moreover obtain K where K: "ball x e = (B ` K)"
          using open_cov [of "ball x e"] by auto
        ultimately have "(B ` K)  -U"
          by blast
        have "K  {}"
          using 0 < e ball x e = (B ` K) by auto
        then obtain n where "n  K" "x  B n"
          by (metis K UN_E 0 < e centre_in_ball)
        then have "U  B n = {}"
          using K e by auto
        show ?thesis
        proof (cases "UA n. closed U  φ U  U  B n = {}")
          case True
          then show ?thesis
            apply (rule_tac x="Suc n" in exI)
            apply (simp add: ASuc)
            apply (erule someI2_ex)
            using x  B n by blast
        next
          case False
          then show ?thesis
            by (meson Inf_lower Usub U  B n = {} φ U closed U range_eqI subset_trans)
        qed
      qed
      with that show ?thesis
        by (meson Inter_iff psubsetE rangeI subsetI)
    qed
  qed
qed

corollary Brouwer_reduction_theorem:
  fixes S :: "'a::euclidean_space set"
  assumes "compact S" "φ S" "S  {}"
      and φ: "F. n. compact(F n); n. F n  {}; n. φ(F n); n. F(Suc n)  F n  φ((range F))"
  obtains T where "T  S" "compact T" "T  {}" "φ T"
                  "U. U  S; closed U; U  {}; φ U  ¬ (U  T)"
proof (rule Brouwer_reduction_theorem_gen [of S "λT. T  {}  T  S  φ T"])
  fix F
  assume cloF: "n. closed (F n)"
     and F: "n. F n  {}  F n  S  φ (F n)" and Fsub: "n. F (Suc n)  F n"
  show "(F ` UNIV)  {}  (F ` UNIV)  S  φ ((F ` UNIV))"
  proof (intro conjI)
    show "(F ` UNIV)  {}"
      by (metis F Fsub compact S cloF closed_Int_compact compact_nest inf.orderE lift_Suc_antimono_le)
    show " (F ` UNIV)  S"
      using F by blast
    show "φ ((F ` UNIV))"
      by (metis F Fsub φ compact S cloF closed_Int_compact inf.orderE)
  qed
next
  show "S  {}  S  S  φ S"
    by (simp add: assms)
qed (meson assms compact_imp_closed seq_compact_closed_subset seq_compact_eq_compact)+


subsectiontag unimportant›‹Arcwise Connections›(*FIX ME this subsection is empty(?) *)

subsection‹Density of points with dyadic rational coordinates›

proposition closure_dyadic_rationals:
    "closure (k. f  Basis  .
                   { i :: 'a :: euclidean_space  Basis. (f i / 2^k) *R i }) = UNIV"
proof -
  have "x  closure (k. f  Basis  . {i  Basis. (f i / 2^k) *R i})" for x::'a
  proof (clarsimp simp: closure_approachable)
    fix e::real
    assume "e > 0"
    then obtain k where k: "(1/2)^k < e/DIM('a)"
      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)
    have "dist (iBasis. (real_of_int 2^k*(x  i) / 2^k) *R i) x =
          dist (iBasis. (real_of_int 2^k*(x  i) / 2^k) *R i) (iBasis. (x  i) *R i)"
      by (simp add: euclidean_representation)
    also have "... = norm ((iBasis. (real_of_int 2^k*(x  i) / 2^k) *R i - (x  i) *R i))"
      by (simp add: dist_norm sum_subtractf)
    also have "...  DIM('a)*((1/2)^k)"
    proof (rule sum_norm_bound, simp add: algebra_simps)
      fix i::'a
      assume "i  Basis"
      then have "norm ((real_of_int x  i*2^k / 2^k) *R i - (x  i) *R i) =
                 ¦real_of_int x  i*2^k / 2^k - x  i¦"
        by (simp add: scaleR_left_diff_distrib [symmetric])
      also have "...  (1/2) ^ k"
        by (simp add: divide_simps) linarith
      finally show "norm ((real_of_int x  i*2^k / 2^k) *R i - (x  i) *R i)  (1/2) ^ k" .
    qed
    also have "... < DIM('a)*(e/DIM('a))"
      using DIM_positive k linordered_comm_semiring_strict_class.comm_mult_strict_left_mono of_nat_0_less_iff by blast
    also have "... = e"
      by simp
    finally have "dist (iBasis. (2^k*(x  i) / 2^k) *R i) x < e" .
    with Ints_of_int
    show "k. f  Basis  . dist (bBasis. (f b / 2^k) *R b) x < e"
      by fastforce
  qed
  then show ?thesis by auto
qed

corollary closure_rational_coordinates:
    "closure (f  Basis  . { i :: 'a :: euclidean_space  Basis. f i *R i }) = UNIV"
proof -
  have *: "(k. f  Basis  . { i::'a  Basis. (f i / 2^k) *R i })
            (f  Basis  . { i  Basis. f i *R i })"
  proof clarsimp
    fix k and f :: "'a  real"
    assume f: "f  Basis  "
    show "x  Basis  . (i  Basis. (f i / 2^k) *R i) = (i  Basis. x i *R i)"
      apply (rule_tac x="λi. f i / 2^k" in bexI)
      using Ints_subset_Rats f by auto
  qed
  show ?thesis
    using closure_dyadic_rationals closure_mono [OF *] by blast
qed

lemma closure_dyadic_rationals_in_convex_set:
   "convex S; interior S  {}
         closure(S 
                    (k. f  Basis  .
                   { i :: 'a :: euclidean_space  Basis. (f i / 2^k) *R i })) =
            closure S"
  by (simp add: closure_dyadic_rationals closure_convex_Int_superset)

lemma closure_rationals_in_convex_set:
   "convex S; interior S  {}
     closure(S  (f  Basis  . { i :: 'a :: euclidean_space  Basis. f i *R i })) =
        closure S"
  by (simp add: closure_rational_coordinates closure_convex_Int_superset)


text‹ Every path between distinct points contains an arc, and hence
path connection is equivalent to arcwise connection for distinct points.
The proof is based on Whyburn's "Topological Analysis".›

lemma closure_dyadic_rationals_in_convex_set_pos_1:
  fixes S :: "real set"
  assumes "convex S" and intnz: "interior S  {}" and pos: "x. x  S  0  x"
    shows "closure(S  (k m. {of_nat m / 2^k})) = closure S"
proof -
  have "m. f 1/2^k = real m / 2^k" if "(f 1) / 2^k  S" "f 1  " for k and f :: "real  real"
    using that by (force simp: Ints_def zero_le_divide_iff power_le_zero_eq dest: pos zero_le_imp_eq_int)
  then have "S  (k m. {real m / 2^k}) = S 
             (k. fBasis  . {iBasis. (f i / 2^k) *R i})"
    by force
  then show ?thesis
    using closure_dyadic_rationals_in_convex_set [OF convex S intnz] by simp
qed


definitiontag unimportant› dyadics :: "'a::field_char_0 set" where "dyadics  k m. {of_nat m / 2^k}"

lemma real_in_dyadics [simp]: "real m  dyadics"
  by (simp add: dyadics_def) (metis divide_numeral_1 numeral_One power_0)

lemma nat_neq_4k1: "of_nat m  (4 * of_nat k + 1) / (2 * 2^n :: 'a::field_char_0)"
proof
  assume "of_nat m = (4 * of_nat k + 1) / (2 * 2^n :: 'a)"
  then have "of_nat (m * (2 * 2^n)) = (of_nat (Suc (4 * k)) :: 'a)"
    by (simp add: field_split_simps)
  then have "m * (2 * 2^n) = Suc (4 * k)"
    using of_nat_eq_iff by blast
  then have "odd (m * (2 * 2^n))"
    by simp
  then show False
    by simp
qed

lemma nat_neq_4k3: "of_nat m  (4 * of_nat k + 3) / (2 * 2^n :: 'a::field_char_0)"
proof
  assume "of_nat m = (4 * of_nat k + 3) / (2 * 2^n :: 'a)"
  then have "of_nat (m * (2 * 2^n)) = (of_nat (4 * k + 3) :: 'a)"
    by (simp add: field_split_simps)
  then have "m * (2 * 2^n) = (4 * k) + 3"
    using of_nat_eq_iff by blast
  then have "odd (m * (2 * 2^n))"
    by simp
  then show False
    by simp
qed

lemma iff_4k:
  assumes "r = real k" "odd k"
    shows "(4 * real m + r) / (2 * 2^n) = (4 * real m' + r) / (2 * 2 ^ n')  m=m'  n=n'"
proof -
  { assume "(4 * real m + r) / (2 * 2^n) = (4 * real m' + r) / (2 * 2 ^ n')"
    then have "real ((4 * m + k) * (2 * 2 ^ n')) = real ((4 * m' + k) * (2 * 2^n))"
      using assms by (auto simp: field_simps)
    then have "(4 * m + k) * (2 * 2 ^ n') = (4 * m' + k) * (2 * 2^n)"
      using of_nat_eq_iff by blast
    then have "(4 * m + k) * (2 ^ n') = (4 * m' + k) * (2^n)"
      by linarith
    then obtain "4*m + k = 4*m' + k" "n=n'"
      using prime_power_cancel2 [OF two_is_prime_nat] assms
      by (metis even_mult_iff even_numeral odd_add)
    then have "m=m'" "n=n'"
      by auto
  }
  then show ?thesis by blast
qed

lemma neq_4k1_k43: "(4 * real m + 1) / (2 * 2^n)  (4 * real m' + 3) / (2 * 2 ^ n')"
proof
  assume "(4 * real m + 1) / (2 * 2^n) = (4 * real m' + 3) / (2 * 2 ^ n')"
  then have "real (Suc (4 * m) * (2 * 2 ^ n')) = real ((4 * m' + 3) * (2 * 2^n))"
    by (auto simp: field_simps)
  then have "Suc (4 * m) * (2 * 2 ^ n') = (4 * m' + 3) * (2 * 2^n)"
    using of_nat_eq_iff by blast
  then have "Suc (4 * m) * (2 ^ n') = (4 * m' + 3) * (2^n)"
    by linarith
  then have "Suc (4 * m) = (4 * m' + 3)"
    by (rule prime_power_cancel2 [OF two_is_prime_nat]) auto
  then have "1 + 2 * m' = 2 * m"
    using Suc (4 * m) = 4 * m' + 3 by linarith
  then show False
    using even_Suc by presburger
qed

lemma dyadic_413_cases:
  obtains "(of_nat m::'a::field_char_0) / 2^k  Nats"
  | m' k' where "k' < k" "(of_nat m:: 'a) / 2^k = of_nat (4*m' + 1) / 2^Suc k'"
  | m' k' where "k' < k" "(of_nat m:: 'a) / 2^k = of_nat (4*m' + 3) / 2^Suc k'"
proof (cases "m>0")
  case False
  then have "m=0" by simp
  with that show ?thesis by auto
next
  case True
  obtain k' m' where m': "odd m'" and k': "m = m' * 2^k'"
    using prime_power_canonical [OF two_is_prime_nat True] by blast
  then obtain q r where q: "m' = 4*q + r" and r: "r < 4"
    by (metis not_add_less2 split_div zero_neq_numeral)
  show ?thesis
  proof (cases "k  k'")
    case True
    have "(of_nat m:: 'a) / 2^k = of_nat m' * (2 ^ k' / 2^k)"
      using k' by (simp add: field_simps)
    also have "... = (of_nat m'::'a) * 2 ^ (k'-k)"
      using k' True by (simp add: power_diff)
    also have "...  "
      by (metis Nats_mult of_nat_in_Nats of_nat_numeral of_nat_power)
    finally show ?thesis by (auto simp: that)
  next
    case False
    then obtain kd where kd: "Suc kd = k - k'"
      using Suc_diff_Suc not_less by blast
    have "(of_nat m:: 'a) / 2^k = of_nat m' * (2 ^ k' / 2^k)"
      using k' by (simp add: field_simps)
    also have "... = (of_nat m'::'a) / 2 ^ (k-k')"
      using k' False by (simp add: power_diff)
    also have "... = ((of_nat r + 4 * of_nat q)::'a) / 2 ^ (k-k')"
      using q by force
    finally have meq: "(of_nat m:: 'a) / 2^k = (of_nat r + 4 * of_nat q) / 2 ^ (k - k')" .
    have "r  0" "r  2"
      using q m' by presburger+
    with r consider "r = 1" | "r = 3"
      by linarith
    then show ?thesis
    proof cases
      assume "r = 1"
      with meq kd that(2) [of kd q] show ?thesis
        by simp
    next
      assume "r = 3"
      with meq kd that(3) [of kd q]  show ?thesis
        by simp
    qed
  qed
qed


lemma dyadics_iff:
   "(dyadics :: 'a::field_char_0 set) =
    Nats  (k m. {of_nat (4*m + 1) / 2^Suc k})  (k m. {of_nat (4*m + 3) / 2^Suc k})"
           (is "_ = ?rhs")
proof
  show "dyadics  ?rhs"
    unfolding dyadics_def
    apply clarify
    apply (rule dyadic_413_cases, force+)
    done
next
  have "range of_nat  (k m. {(of_nat m::'a) / 2 ^ k})"
    by clarsimp (metis divide_numeral_1 numeral_One power_0)
  moreover have "k m. k' m'. ((1::'a) + 4 * of_nat m) / 2 ^ Suc k = of_nat m' / 2 ^ k'"
    by (metis (no_types) of_nat_Suc of_nat_mult of_nat_numeral)
  moreover have "k m. k' m'. (4 * of_nat m + (3::'a)) / 2 ^ Suc k = of_nat m' / 2 ^ k'"
    by (metis of_nat_add of_nat_mult of_nat_numeral)
  ultimately show "?rhs  dyadics"
    by (auto simp: dyadics_def Nats_def)
qed


functiontag unimportant› (domintros) dyad_rec :: "[nat  'a, 'a'a, 'a'a, real]  'a" where
    "dyad_rec b l r (real m) = b m"
  | "dyad_rec b l r ((4 * real m + 1) / 2 ^ (Suc n)) = l (dyad_rec b l r ((2*m + 1) / 2^n))"
  | "dyad_rec b l r ((4 * real m + 3) / 2 ^ (Suc n)) = r (dyad_rec b l r ((2*m + 1) / 2^n))"
  | "x  dyadics  dyad_rec b l r x = undefined"
  using iff_4k [of _ 1] iff_4k [of _ 3]
         apply (simp_all add: nat_neq_4k1 nat_neq_4k3 neq_4k1_k43 dyadics_iff Nats_def)
  by (fastforce simp:  field_simps)+

lemma dyadics_levels: "dyadics = (K. k<K.  m. {of_nat m / 2^k})"
  unfolding dyadics_def by auto

lemma dyad_rec_level_termination:
  assumes "k < K"
  shows "dyad_rec_dom(b, l, r, real m / 2^k)"
  using assms
proof (induction K arbitrary: k m)
  case 0
  then show ?case by auto
next
  case (Suc K)
  then consider "k = K" | "k < K"
    using less_antisym by blast
  then show ?case
  proof cases
    assume "k = K"
    show ?case
    proof (rule dyadic_413_cases [of m k, where 'a=real])
      show "real m / 2^k    dyad_rec_dom (b, l, r, real m / 2^k)"
        by (force simp: Nats_def nat_neq_4k1 nat_neq_4k3 intro: dyad_rec.domintros)
      show ?case if "k' < k" and eq: "real m / 2^k = real (4 * m' + 1) / 2^Suc k'" for m' k'
      proof -
        have "dyad_rec_dom (b, l, r, (4 * real m' + 1) / 2^Suc k')"
        proof (rule dyad_rec.domintros)
          fix m n
          assume "(4 * real m' + 1) / (2 * 2 ^ k') = (4 * real m + 1) / (2 * 2^n)"
          then have "m' = m" "k' = n" using iff_4k [of _ 1]
            by auto
          have "dyad_rec_dom (b, l, r, real (2 * m + 1) / 2 ^ k')"
            using Suc.IH k = K k' < k by blast
          then show "dyad_rec_dom (b, l, r, (2 * real m + 1) / 2^n)"
            using k' = n by (auto simp: algebra_simps)
        next
          fix m n
          assume "(4 * real m' + 1) / (2 * 2 ^ k') = (4 * real m + 3) / (2 * 2^n)"
          then have "False"
            by (metis neq_4k1_k43)
          then show "dyad_rec_dom (b, l, r, (2 * real m + 1) / 2^n)" ..
        qed
        then show ?case by (simp add: eq add_ac)
      qed
      show ?case if "k' < k" and eq: "real m / 2^k = real (4 * m' + 3) / 2^Suc k'" for m' k'
      proof -
        have "dyad_rec_dom (b, l, r, (4 * real m' + 3) / 2^Suc k')"
        proof (rule dyad_rec.domintros)
          fix m n
          assume "(4 * real m' + 3) / (2 * 2 ^ k') = (4 * real m + 1) / (2 * 2^n)"
          then have "False"
            by (metis neq_4k1_k43)
          then show "dyad_rec_dom (b, l, r, (2 * real m + 1) / 2^n)" ..
        next
          fix m n
          assume "(4 * real m' + 3) / (2 * 2 ^ k') = (4 * real m + 3) / (2 * 2^n)"
          then have "m' = m" "k' = n" using iff_4k [of _ 3]
            by auto
          have "dyad_rec_dom (b, l, r, real (2 * m + 1) / 2 ^ k')"
            using Suc.IH k = K k' < k by blast
          then show "dyad_rec_dom (b, l, r, (2 * real m + 1) / 2^n)"
            using k' = n by (auto simp: algebra_simps)
        qed
        then show ?case by (simp add: eq add_ac)
      qed
    qed
  next
    assume "k < K"
    then show ?case
      using Suc.IH by blast
  qed
qed


lemma dyad_rec_termination: "x  dyadics  dyad_rec_dom(b,l,r,x)"
  by (auto simp: dyadics_levels intro: dyad_rec_level_termination)

lemma dyad_rec_of_nat [simp]: "dyad_rec b l r (real m) = b m"
  by (simp add: dyad_rec.psimps dyad_rec_termination)

lemma dyad_rec_41 [simp]: "dyad_rec b l r ((4 * real m + 1) / 2 ^ (Suc n)) = l (dyad_rec b l r ((2*m + 1) / 2^n))"
proof (rule dyad_rec.psimps)
  show "dyad_rec_dom (b, l, r, (4 * real m + 1) / 2 ^ Suc n)"
    by (metis add.commute dyad_rec_level_termination lessI of_nat_Suc of_nat_mult of_nat_numeral)
qed

lemma dyad_rec_43 [simp]: "dyad_rec b l r ((4 * real m + 3) / 2 ^ (Suc n)) = r (dyad_rec b l r ((2*m + 1) / 2^n))"
proof (rule dyad_rec.psimps)
  show "dyad_rec_dom (b, l, r, (4 * real m + 3) / 2 ^ Suc n)"
    by (metis dyad_rec_level_termination lessI of_nat_add of_nat_mult of_nat_numeral)
qed

lemma dyad_rec_41_times2:
  assumes "n > 0"
    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))"
proof -
  obtain n' where n': "n = Suc n'"
    using assms not0_implies_Suc by blast
  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))"
    by auto
  also have "... = dyad_rec b l r ((4 * real m + 1) / 2^n)"
    by (subst mult_divide_mult_cancel_left) auto
  also have "... = l (dyad_rec b l r ((2 * real m + 1) / 2 ^ n'))"
    by (simp add: add.commute [of 1] n' del: power_Suc)
  also have "... = l (dyad_rec b l r ((2 * (2 * real m + 1)) / (2 * 2 ^ n')))"
    by (subst mult_divide_mult_cancel_left) auto
  also have "... = l (dyad_rec b l r (2 * (2 * real m + 1) / 2^n))"
    by (simp add: add.commute n')
  finally show ?thesis .
qed

lemma dyad_rec_43_times2:
  assumes "n > 0"
    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))"
proof -
  obtain n' where n': "n = Suc n'"
    using assms not0_implies_Suc by blast
  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))"
    by auto
  also have "... = dyad_rec b l r ((4 * real m + 3) / 2^n)"
    by (subst mult_divide_mult_cancel_left) auto
  also have "... = r (dyad_rec b l r ((2 * real m + 1) / 2 ^ n'))"
    by (simp add: n' del: power_Suc)
  also have "... = r (dyad_rec b l r ((2 * (2 * real m + 1)) / (2 * 2 ^ n')))"
    by (subst mult_divide_mult_cancel_left) auto
  also have "... = r (dyad_rec b l r (2 * (2 * real m + 1) / 2^n))"
    by (simp add: n')
  finally show ?thesis .
qed

definitiontag unimportant› dyad_rec2
    where "dyad_rec2 u v lc rc x =
             dyad_rec (λz. (u,v)) (λ(a,b). (a, lc a b (midpoint a b))) (λ(a,b). (rc a b (midpoint a b), b)) (2*x)"

abbreviationtag unimportant› leftrec where "leftrec u v lc rc x  fst (dyad_rec2 u v lc rc x)"
abbreviationtag unimportant› rightrec where "rightrec u v lc rc x  snd (dyad_rec2 u v lc rc x)"

lemma leftrec_base: "leftrec u v lc rc (real m / 2) = u"
  by (simp add: dyad_rec2_def)

lemma leftrec_41: "n > 0  leftrec u v lc rc ((4 * real m + 1) / 2 ^ (Suc n)) = leftrec u v lc rc ((2 * real m + 1) / 2^n)"
  unfolding dyad_rec2_def dyad_rec_41_times2
  by (simp add: case_prod_beta)

lemma leftrec_43: "n > 0 
             leftrec u v lc rc ((4 * real m + 3) / 2 ^ (Suc n)) =
                 rc (leftrec u v lc rc ((2 * real m + 1) / 2^n)) (rightrec u v lc rc ((2 * real m + 1) / 2^n))
                 (midpoint (leftrec u v lc rc ((2 * real m + 1) / 2^n)) (rightrec u v lc rc ((2 * real m + 1) / 2^n)))"
  unfolding dyad_rec2_def dyad_rec_43_times2
  by (simp add: case_prod_beta)

lemma rightrec_base: "rightrec u v lc rc (real m / 2) = v"
  by (simp add: dyad_rec2_def)

lemma rightrec_41: "n > 0 
             rightrec u v lc rc ((4 * real m + 1) / 2 ^ (Suc n)) =
                 lc (leftrec u v lc rc ((2 * real m + 1) / 2^n)) (rightrec u v lc rc ((2 * real m + 1) / 2^n))
                 (midpoint (leftrec u v lc rc ((2 * real m + 1) / 2^n)) (rightrec u v lc rc ((2 * real m + 1) / 2^n)))"
  unfolding dyad_rec2_def dyad_rec_41_times2
  by (simp add: case_prod_beta)

lemma rightrec_43: "n > 0  rightrec u v lc rc ((4 * real m + 3) / 2 ^ (Suc n)) = rightrec u v lc rc ((2 * real m + 1) / 2^n)"
  unfolding dyad_rec2_def dyad_rec_43_times2
  by (simp add: case_prod_beta)

lemma dyadics_in_open_unit_interval:
   "{0<..<1}  (k m. {real m / 2^k}) = (k. m  {0<..<2^k}. {real m / 2^k})"
  by (auto simp: field_split_simps)


lemma padic_rational_approximation_straddle:
  assumes "ε > 0" "p > 1"
  obtains n q r 
    where "of_int q / p^n < x" "x < of_int r / p^n" "¦q / p^n - r / p^n ¦ < ε"
proof -
  obtain n where n: "2 / ε < p ^ n"
    using p>1 real_arch_pow by blast
  define q where "q  p ^ n * x - 1"
  show thesis
    proof
      show "q / p ^ n < x" "x < real_of_int (q+2) / p ^ n"
        using assms by (simp_all add: q_def divide_simps floor_less_cancel mult.commute)
      show "¦q / p ^ n - real_of_int (q+2) / p ^ n¦ < ε"
        using assms n by (simp add: q_def divide_simps mult.commute)
    qed
qed

lemma padic_rational_approximation_straddle_pos:
  assumes "ε > 0" "p > 1" "x > 0"
  obtains n q r 
    where "of_nat q / p^n < x" "x < of_nat r / p^n" "¦q / p^n - r / p^n ¦ < ε"
proof -
  obtain n q r 
    where *: "of_int q / p^n < x" "x < of_int r / p^n" "¦q / p^n - r / p^n ¦ < ε"
    using padic_rational_approximation_straddle assms by metis
  then have "r  0"
    using assms by (smt (verit, best) divide_nonpos_pos of_int_0_le_iff zero_less_power)
  show thesis
  proof
    show "real (max 0 (nat q)) / p ^ n < x"
      using * by (metis assms(3) div_0 max_nat.left_neutral nat_eq_iff2 of_nat_0 of_nat_nat) 
    show "x < real (nat r) / p ^ n"
      using r  0 * by force
    show "¦real (max 0 (nat q)) / p ^ n - real (nat r) / p ^ n¦ < ε"
      using * assms by (simp add: divide_simps)
  qed
qed

lemma padic_rational_approximation_straddle_pos_le:
  assumes "ε > 0" "p > 1" "x  0"
  obtains n q r 
    where "of_nat q / p^n  x" "x < of_nat r / p^n" "¦q / p^n - r / p^n ¦ < ε"
proof -
  obtain n q r 
    where *: "of_int q / p^n < x" "x < of_int r / p^n" "¦q / p^n - r / p^n ¦ < ε"
    using padic_rational_approximation_straddle assms by metis
  then have "r  0"
    using assms by (smt (verit, best) divide_nonpos_pos of_int_0_le_iff zero_less_power)
  show thesis
  proof
    show "real (max 0 (nat q)) / p ^ n  x"
      using * assms(3) nle_le by fastforce
    show "x < real (nat r) / p ^ n"
      using r  0 * by force
    show "¦real (max 0 (nat q)) / p ^ n - real (nat r) / p ^ n¦ < ε"
       using * assms by (simp add: divide_simps)
  qed
qed


subsubsection ‹Definition by recursion on dyadic rationals in [0,1]›

lemma recursion_on_dyadic_fractions:
  assumes base: "R a b"
    and step: "x y. R x y  z. R x z  R z y" and trans: "x y z. R x y; R y z  R x z"
  shows "f :: real  'a. f 0 = a  f 1 = b 
               (x  dyadics  {0..1}. y  dyadics  {0..1}. x < y  R (f x) (f y))"
proof -
  obtain mid where mid: "R x y  R x (mid x y)" "R x y  R (mid x y) y" for x y 
    using step by metis
  define g where "g  rec_nat (λk. if k = 0 then a else b) (λn r k. if even k then r (k div 2) else mid (r ((k - 1) div 2)) (r ((Suc k) div 2)))"
  have g0 [simp]: "g 0 = (λk. if k = 0 then a else b)"
    by (simp add: g_def)
  have gSuc [simp]: "n. g(Suc n) = (λk. if even k then g n (k div 2) else mid (g n ((k - 1) div 2)) (g n ((Suc k) div 2)))"
    by (auto simp: g_def)
  have g_eq_g: "2 ^ d * k = k'  g n k = g (n + d) k'" for n d k k'
    by (induction d arbitrary: k k') auto
  have "g n k = g n' k'" if "real k / 2^n = real k' / 2^n'" "n'  n" for k n k' n'
  proof -
    have "real k = real k' * 2 ^ (n-n')"
      using that by (simp add: power_diff divide_simps)
    then have "k = k' * 2 ^ (n-n')"
      using of_nat_eq_iff by fastforce
    with g_eq_g show ?thesis
      by (metis le_add_diff_inverse mult.commute that(2))
  qed
  then have g_eq_g: "g n k = g n' k'" if "real k / 2 ^ n = real k' / 2 ^ n'" for k n k' n'
    by (metis nat_le_linear that)
  then obtain f where "(λ(k,n). g n k) = f  (λ(k,n). k / 2 ^ n)"
    using function_factors_left by (smt (verit, del_insts) case_prod_beta')
  then have f_eq_g: "k n. f(real k / 2 ^ n) = g n k"
    by (simp add: fun_eq_iff)
  show ?thesis
  proof (intro exI conjI strip)
    show "f 0 = a"
      by (metis f_eq_g g0 div_0 of_nat_0)
    show "f 1 = b"
      by (metis f_eq_g g0 div_by_1 of_nat_1_eq_iff power_0 zero_neq_one)
    show "R (f x) (f y)" 
      if x: "x  dyadics  {0..1}" and y: "y  dyadics  {0..1}" and "x < y" for x y
    proof -
      obtain n1 k1 where xeq: "x = real k1 / 2^n1" "k1  2^n1"
        using x by (auto simp: dyadics_def)
      obtain n2 k2 where yeq: "y = real k2 / 2^n2" "k2  2^n2"
        using y by (auto simp: dyadics_def)
      have xcommon: "x = real(2^n2 * k1) / 2 ^ (n1+n2)"
        using xeq by (simp add: power_add)
      have ycommon: "y = real(2^n1 * k2) / 2 ^ (n1+n2)"
        using yeq by (simp add: power_add)
      have *: "R (g n j) (g n k)" if "j < k" "k  2^n" for n j k
        using that
      proof (induction n arbitrary: j k)
        case 0
        then show ?case
          by (simp add: base)
      next
        case (Suc n)
        show ?case
        proof (cases "even j")
          case True
          then obtain a where [simp]: "j = 2*a"
            by blast
          show ?thesis 
          proof (cases "even k")
            case True
            with Suc show ?thesis
              by (auto elim!: evenE)
          next
            case False
            then obtain b where [simp]: "k = Suc (2*b)"
              using oddE by fastforce
            show ?thesis
              using Suc
              apply simp
              by (smt (verit, ccfv_SIG) less_Suc_eq linorder_not_le local.trans mid(1) nat_mult_less_cancel1 pos2)
          qed
        next
          case False
          then obtain a where [simp]: "j = Suc (2*a)"
            using oddE by fastforce
          show ?thesis
          proof (cases "even k")
            case True
            then obtain b where [simp]: "k = 2*b"
              by blast
            show ?thesis
              using Suc 
              apply simp
              by (smt (verit, ccfv_SIG) Suc_leI Suc_lessD le_trans lessI linorder_neqE_nat linorder_not_le local.trans mid(2) nat_mult_less_cancel1 pos2)
          next
            case False
            then obtain b where [simp]: "k = Suc (2*b)"
              using oddE by fastforce
            show ?thesis
              using Suc 
              apply simp
              by (smt (verit) Suc_leI le_trans lessI less_or_eq_imp_le linorder_neqE_nat linorder_not_le local.trans mid(1) mid(2) nat_mult_less_cancel1 pos2)
            qed
        qed
      qed
      show ?thesis
        unfolding xcommon ycommon f_eq_g
      proof (rule *)
        show "2 ^ n2 * k1 < 2 ^ n1 * k2"
          using of_nat_less_iff x < y by (fastforce simp: xeq yeq field_simps)
        show "2 ^ n1 * k2  2 ^ (n1 + n2)"
          by (simp add: power_add yeq)
      qed
    qed
  qed
qed

lemma dyadics_add:
  assumes "x  dyadics" "y  dyadics"
  shows "x+y  dyadics"
proof -
  obtain i j m n where x: "x = of_nat i / 2 ^ m" and y: "y = of_nat j / 2 ^ n"
    using assms by (auto simp: dyadics_def)
  have xcommon: "x = of_nat(2^n * i) / 2 ^ (m+n)"
    using x by (simp add: power_add)
  moreover
  have ycommon: "y = of_nat(2^m * j) / 2 ^ (m+n)"
    using y by (simp add: power_add)
  ultimately have "x+y = (of_nat(2^n * i + 2^m * j)) / 2 ^ (m+n)"
    by (simp add: field_simps)
  then show ?thesis
    unfolding dyadics_def by blast
qed

lemma dyadics_diff:
  fixes x :: "'a::linordered_field"
  assumes "x  dyadics" "y  dyadics" "y  x"
  shows "x-y  dyadics"
proof -
  obtain i j m n where x: "x = of_nat i / 2 ^ m" and y: "y = of_nat j / 2 ^ n"
    using assms by (auto simp: dyadics_def)
  have j_le_i: "j * 2 ^ m  i * 2 ^ n"
    using of_nat_le_iff y  x unfolding x y by (fastforce simp add: divide_simps)
  have xcommon: "x = of_nat(2^n * i) / 2 ^ (m+n)"
    using x by (simp add: power_add)
  moreover
  have ycommon: "y = of_nat(2^m * j) / 2 ^ (m+n)"
    using y by (simp add: power_add)
  ultimately have "x-y = (of_nat(2^n * i - 2^m * j)) / 2 ^ (m+n)"
    by (simp add: xcommon ycommon field_simps j_le_i of_nat_diff)
  then show ?thesis
    unfolding dyadics_def by blast
qed



theorem homeomorphic_monotone_image_interval:
  fixes f :: "real  'a::{real_normed_vector,complete_space}"
  assumes cont_f: "continuous_on {0..1} f"
      and conn: "y. connected ({0..1}  f -` {y})"
      and f_1not0: "f 1  f 0"
    shows "(f ` {0..1}) homeomorphic {0..1::real}"
proof -
  have "c d. a  c  c  m  m  d  d  b 
              (x  {c..d}. f x = f m) 
              (x  {a..<c}. (f x  f m)) 
              (x  {d<..b}. (f x  f m)) 
              (x  {a..<c}. y  {d<..b}. f x  f y)"
    if m: "m  {a..b}" and ab01: "{a..b}  {0..1}" for a b m
  proof -
    have comp: "compact (f -` {f m}  {0..1})"
      by (simp add: compact_eq_bounded_closed bounded_Int closed_vimage_Int cont_f)
    obtain c0 d0 where cd0: "{0..1}  f -` {f m} = {c0..d0}"
      using connected_compact_interval_1 [of "{0..1}  f -` {f m}"] conn comp
      by (metis Int_commute)
    with that have "m  cbox c0 d0"
      by auto
    obtain c d where cd: "{a..b}  f -` {f m} = {c..d}"
      using ab01 cd0
      by (rule_tac c="max a c0" and d="min b d0" in that) auto
    then have cdab: "{c..d}  {a..b}"
      by blast
    show ?thesis
    proof (intro exI conjI ballI)
      show "a  c" "d  b"
        using cdab cd m by auto
      show "c  m" "m  d"
        using cd m by auto
      show "x. x  {c..d}  f x = f m"
        using cd by blast
      show "f x  f m" if "x  {a..<c}" for x
        using that m cd [THEN equalityD1, THEN subsetD] c  m by force
      show "f x  f m" if "x  {d<..b}" for x
        using that m cd [THEN equalityD1, THEN subsetD, of x] m  d by force
      show "f x  f y" if "x  {a..<c}" "y  {d<..b}" for x y
      proof (cases "f x = f m  f y = f m")
        case True
        then show ?thesis
          using x. x  {a..<c}  f x  f m that by auto
      next
        case False
        have False if "f x = f y"
        proof -
          have "x  m" "m  y"
            using c  m x  {a..<c}  m  d y  {d<..b} by auto
          then have "x  ({0..1}  f -` {f y})" "y  ({0..1}  f -` {f y})"
            using x  {a..<c} y  {d<..b} ab01 by (auto simp: that)
          then have "m  ({0..1}  f -` {f y})"
            by (meson m  y x  m is_interval_connected_1 conn [of "f y"] is_interval_1)
          with False show False by auto
        qed
        then show ?thesis by auto
      qed
    qed
  qed
  then obtain leftcut rightcut where LR:
    "a b m. m  {a..b}; {a..b}  {0..1} 
            (a  leftcut a b m  leftcut a b m  m  m  rightcut a b m  rightcut a b m  b 
            (x  {leftcut a b m..rightcut a b m}. f x = f m) 
            (x  {a..<leftcut a b m}. f x  f m) 
            (x  {rightcut a b m<..b}. f x  f m) 
            (x  {a..<leftcut a b m}. y  {rightcut a b m<..b}. f x  f y))"
    apply atomize
    apply (clarsimp simp only: imp_conjL [symmetric] choice_iff choice_iff')
    apply (rule that, blast)
    done
  then have left_right: "a b m. m  {a..b}; {a..b}  {0..1}  a  leftcut a b m  rightcut a b m  b"
       and  left_right_m: "a b m. m  {a..b}; {a..b}  {0..1}  leftcut a b m  m  m  rightcut a b m"
    by auto
  have left_neq: "a  x; x < leftcut a b m; a  m; m  b; {a..b}  {0..1}  f x  f m"
    and right_neq: "rightcut a b m < x; x  b; a  m; m  b; {a..b}  {0..1}  f x  f m"
    and left_right_neq: "a  x; x < leftcut a b m; rightcut a b m < y; y  b; a  m; m  b; {a..b}  {0..1}  f x  f m"
    and feqm: "leftcut a b m  x; x  rightcut a b m; a  m; m  b; {a..b}  {0..1}
                          f x = f m" for a b m x y
    by (meson atLeastAtMost_iff greaterThanAtMost_iff atLeastLessThan_iff LR)+
  have f_eqI: "a b m x y. leftcut a b m  x; x  rightcut a b m; leftcut a b m  y; y  rightcut a b m;
                             a  m; m  b; {a..b}  {0..1}   f x = f y"
    by (metis feqm)
  define u where "u  rightcut 0 1 0"
  have lc[simp]: "leftcut 0 1 0 = 0" and u01: "0  u" "u  1"
    using LR [of 0 0 1] by (auto simp: u_def)
  have f0u: "x. x  {0..u}  f x = f 0"
    using LR [of 0 0 1] unfolding u_def [symmetric]
    by (metis leftcut 0 1 0 = 0 atLeastAtMost_iff order_refl zero_le_one)
  have fu1: "x. x  {u<..1}  f x  f 0"
    using LR [of 0 0 1] unfolding u_def [symmetric] by fastforce
  define v where "v  leftcut u 1 1"
  have rc[simp]: "rightcut u 1 1 = 1" and v01: "u  v" "v  1"
    using LR [of 1 u 1] u01  by (auto simp: v_def)
  have fuv: "x. x  {u..<v}  f x  f 1"
    using LR [of 1 u 1] u01 v_def by fastforce
  have f0v: "x. x  {0..<v}  f x  f 1"
    by (metis f_1not0 atLeastAtMost_iff atLeastLessThan_iff f0u fuv linear)
  have fv1: "x. x  {v..1}  f x = f 1"
    using LR [of 1 u 1] u01 v_def by (metis atLeastAtMost_iff atLeastatMost_subset_iff order_refl rc)
  define a where "a  leftrec u v leftcut rightcut"
  define b where "b  rightrec u v leftcut rightcut"
  define c where "c  λx. midpoint (a x) (b x)"
  have a_real [simp]: "a (real j) = u" for j
    using a_def leftrec_base
    by (metis nonzero_mult_div_cancel_right of_nat_mult of_nat_numeral zero_neq_numeral)
  have b_real [simp]: "b (real j) = v" for j
    using b_def rightrec_base
    by (metis nonzero_mult_div_cancel_right of_nat_mult of_nat_numeral zero_neq_numeral)
  have a41: "a ((4 * real m + 1) / 2^Suc n) = a ((2 * real m + 1) / 2^n)" if "n > 0" for m n
    using that a_def leftrec_41 by blast
  have b41: "b ((4 * real m + 1) / 2^Suc n) =
               leftcut (a ((2 * real m + 1) / 2^n))
                       (b ((2 * real m + 1) / 2^n))
                       (c ((2 * real m + 1) / 2^n))" if "n > 0" for m n
    using that a_def b_def c_def rightrec_41 by blast
  have a43: "a ((4 * real m + 3) / 2^Suc n) =
               rightcut (a ((2 * real m + 1) / 2^n))
                        (b ((2 * real m + 1) / 2^n))
                        (c ((2 * real m + 1) / 2^n))" if "n > 0" for m n
    using that a_def b_def c_def leftrec_43 by blast
  have b43: "b ((4 * real m + 3) / 2^Suc n) = b ((2 * real m + 1) / 2^n)" if "n > 0" for m n
    using that b_def rightrec_43 by blast
  have uabv: "u  a (real m / 2 ^ n)  a (real m / 2 ^ n)  b (real m / 2 ^ n)  b (real m / 2 ^ n)  v" for m n
  proof (induction n arbitrary: m)
    case 0
    then show ?case by (simp add: v01)
  next
    case (Suc n p)
    show ?case
    proof (cases "even p")
      case True
      then obtain m where "p = 2*m" by (metis evenE)
      then show ?thesis
        by (simp add: Suc.IH)
    next
      case False
      then obtain m where m: "p = 2*m + 1" by (metis oddE)
      show ?thesis
      proof (cases n)
        case 0
        then show ?thesis
          by (simp add: a_def b_def leftrec_base rightrec_base v01)
      next
        case (Suc n')
        then have "n > 0" by simp
        have a_le_c: "a (real m / 2^n)  c (real m / 2^n)" for m
          unfolding c_def by (metis Suc.IH ge_midpoint_1)
        have c_le_b: "c (real m / 2^n)  b (real m / 2^n)" for m
          unfolding c_def by (metis Suc.IH le_midpoint_1)
        have c_ge_u: "c (real m / 2^n)  u" for m
          using Suc.IH a_le_c order_trans by blast
        have c_le_v: "c (real m / 2^n)  v" for m
          using Suc.IH c_le_b order_trans by blast
        have a_ge_0: "0  a (real m / 2^n)" for m
          using Suc.IH order_trans u01(1) by blast
        have b_le_1: "b (real m / 2^n)  1" for m
          using Suc.IH order_trans v01(2) by blast
        have left_le: "leftcut (a ((real m) / 2^n)) (b ((real m) / 2^n)) (c ((real m) / 2^n))  c ((real m) / 2^n)" for m
          by (simp add: LR a_ge_0 a_le_c b_le_1 c_le_b)
        have right_ge: "rightcut (a ((real m) / 2^n)) (b ((real m) / 2^n)) (c ((real m) / 2^n))  c ((real m) / 2^n)" for m
          by (simp add: LR a_ge_0 a_le_c b_le_1 c_le_b)
        show ?thesis
        proof (cases "even m")
          case True
          then obtain r where r: "m = 2*r" by (metis evenE)
          show ?thesis
            using order_trans [OF left_le c_le_v, of "1+2*r"] Suc.IH [of "m+1"] 
            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"] left_right n > 0
            by (simp_all add: r m add.commute [of 1]  a41 b41 del: power_Suc)
        next
          case False
          then obtain r where r: "m = 2*r + 1" by (metis oddE)
          show ?thesis
            using order_trans [OF c_ge_u right_ge, of "1+2*r"] Suc.IH [of "m"]
            using a_le_c [of "m"] c_le_b [of "m"] a_ge_0 [of "m"] b_le_1 [of "m"] left_right n > 0
            apply (simp_all add: r m add.commute [of 3] a43 b43 del: power_Suc)
            by (simp add: add.commute)
        qed
      qed
    qed
  qed
  have a_ge_0 [simp]: "0  a(m / 2^n)" and b_le_1 [simp]: "b(m / 2^n)  1" for m::nat and n
    using uabv order_trans u01 v01 by blast+
  then have b_ge_0 [simp]: "0  b(m / 2^n)" and a_le_1 [simp]: "a(m / 2^n)  1" for m::nat and n
    using uabv order_trans by blast+
  have alec [simp]: "a(m / 2^n)  c(m / 2^n)" and cleb [simp]: "c(m / 2^n)  b(m / 2^n)" for m::nat and n
    by (auto simp: c_def ge_midpoint_1 le_midpoint_1 uabv)
  have c_ge_0 [simp]: "0  c(m / 2^n)" and c_le_1 [simp]: "c(m / 2^n)  1" for m::nat and n
    using a_ge_0 alec b_le_1 cleb order_trans by blast+
  have "d = m-n; odd j; ¦real i / 2^m - real j / 2^n¦ < 1/2 ^ n
         (a(j / 2^n))  (c(i / 2^m))  (c(i / 2^m))  (b(j / 2^n))" for d i j m n
  proof (induction d arbitrary: j n rule: less_induct)
    case (less d j n)
    show ?case
    proof (cases "m  n")
      case True
      have "¦2^n¦ * ¦real i / 2^m - real j / 2^n¦ = 0"
      proof (rule Ints_nonzero_abs_less1)
        have "(real i * 2^n - real j * 2^m) / 2^m = (real i * 2^n) / 2^m - (real j * 2^m) / 2^m"
          using diff_divide_distrib by blast
        also have "... = (real i * 2 ^ (n-m)) - (real j)"
          using True by (auto simp: power_diff field_simps)
        also have "...  "
          by simp
        finally have "(real i * 2^n - real j * 2^m) / 2^m  " .
        with True Ints_abs show "¦2^n¦ * ¦real i / 2^m - real j / 2^n¦  "
          by (fastforce simp: field_split_simps)
        show "¦¦2^n¦ * ¦real i / 2^m - real j / 2^n¦¦ < 1"
          using less.prems by (auto simp: field_split_simps)
      qed
      then have "real i / 2^m = real j / 2^n"
        by auto
      then show ?thesis
        by auto
    next
      case False
      then have "n < m" by auto
      obtain k where k: "j = Suc (2*k)"
        using odd j oddE by fastforce
      show ?thesis
      proof (cases "n > 0")
        case False
        then have "a (real j / 2^n) = u"
          by simp
        also have "...  c (real i / 2^m)"
          using alec uabv by (blast intro: order_trans)
        finally have ac: "a (real j / 2^n)  c (real i / 2^m)" .
        have "c (real i / 2^m)  v"
          using cleb uabv by (blast intro: order_trans)
        also have "... = b (real j / 2^n)"
          using False by simp
        finally show ?thesis
          by (auto simp: ac)
      next
        case True show ?thesis
        proof (cases "i / 2^m" "j / 2^n" rule: linorder_cases)
          case less
          moreover have "real (4 * k + 1) / 2 ^ Suc n + 1 / (2 ^ Suc n) = real j / 2 ^ n"
            using k by (force simp: field_split_simps)
          moreover have "¦real i / 2 ^ m - j / 2 ^ n¦ < 2 / (2 ^ Suc n)"
            using less.prems by simp
          ultimately have closer: "¦real i / 2 ^ m - real (4 * k + 1) / 2 ^ Suc n¦ < 1 / (2 ^ Suc n)"
            using less.prems by linarith
          have "a (real (4 * k + 1) / 2 ^ Suc n)  c (i / 2 ^ m) 
                   c (real i / 2 ^ m)  b (real (4 * k + 1) / 2 ^ Suc n)"
          proof (rule less.IH [OF _ refl])
            show "m - Suc n < d"
              using n < m diff_less_mono2 less.prems(1) lessI by presburger
            show "¦real i / 2 ^ m - real (4 * k + 1) / 2 ^ Suc n¦ < 1 / 2 ^ Suc n"
              using closer n < m d = m - n by (auto simp: field_split_simps n < m diff_less_mono2)
          qed auto
          then show ?thesis
            using LR [of "c((2*k + 1) / 2^n)" "a((2*k + 1) / 2^n)" "b((2*k + 1) / 2^n)"]
            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"]
            using k a41 b41 0 < n
            by (simp add: add.commute)
        next
          case equal then show ?thesis by simp
        next
          case greater
          moreover have "real (4 * k + 3) / 2 ^ Suc n - 1 / (2 ^ Suc n) = real j / 2 ^ n"
            using k by (force simp: field_split_simps)
          moreover have "¦real i / 2 ^ m - real j / 2 ^ n¦ < 2 * 1 / (2 ^ Suc n)"
            using less.prems by simp
          ultimately have closer: "¦real i / 2 ^ m - real (4 * k + 3) / 2 ^ Suc n¦ < 1 / (2 ^ Suc n)"
            using less.prems by linarith
          have "a (real (4 * k + 3) / 2 ^ Suc n)  c (real i / 2 ^ m) 
                   c (real i / 2 ^ m)  b (real (4 * k + 3) / 2 ^ Suc n)"
          proof (rule less.IH [OF _ refl])
            show "m - Suc n < d"
              using n < m diff_less_mono2 less.prems(1) by blast
            show "¦real i / 2 ^ m - real (4 * k + 3) / 2 ^ Suc n¦ < 1 / 2 ^ Suc n"
              using closer n < m d = m - n by (auto simp: field_split_simps  n < m diff_less_mono2)
          qed auto
          then show ?thesis
            using LR [of "c((2*k + 1) / 2^n)" "a((2*k + 1) / 2^n)" "b((2*k + 1) / 2^n)"]
            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"]
            using k a43 b43 0 < n
            by (simp add: add.commute)
        qed
      qed
    qed
  qed
  then have aj_le_ci: "a (real j / 2 ^ n)  c (real i / 2 ^ m)"
    and ci_le_bj: "c (real i / 2 ^ m)  b (real j / 2 ^ n)" if "odd j" "¦real i / 2^m - real j / 2^n¦ < 1/2 ^ n" for i j m n
    using that by blast+
  have close_ab: "odd m  ¦a (real m / 2 ^ n) - b (real m / 2 ^ n)¦  2 / 2^n" for m n
  proof (induction n arbitrary: m)
    case 0
    with u01 v01 show ?case by auto
  next
    case (Suc n m)
    with oddE obtain k where k: "m = Suc (2*k)" by fastforce
    show ?case
    proof (cases "n > 0")
      case False
      with u01 v01 show ?thesis
        by (simp add: a_def b_def leftrec_base rightrec_base)
    next
      case True
      show ?thesis
      proof (cases "even k")
        case True
        then obtain j where j: "k = 2*j" by (metis evenE)
        have "¦a ((2 * real j + 1) / 2 ^ n) - (b ((2 * real j + 1) / 2 ^ n))¦  2/2 ^ n"
        proof -
          have "odd (Suc k)"
            using True by auto
          then show ?thesis
            by (metis (no_types) Groups.add_ac(2) Suc.IH j of_nat_Suc of_nat_mult of_nat_numeral)
        qed
        moreover have "a ((2 * real j + 1) / 2 ^ n) 
                       leftcut (a ((2 * real j + 1) / 2 ^ n)) (b ((2 * real j + 1) / 2 ^ n)) (c ((2 * real j + 1) / 2 ^ n))"
          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"]
          by (auto simp: add.commute left_right)
        moreover have "leftcut (a ((2 * real j + 1) / 2 ^ n)) (b ((2 * real j + 1) / 2 ^ n)) (c ((2 * real j + 1) / 2 ^ n)) 
                         c ((2 * real j + 1) / 2 ^ n)"
          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"]
          by (auto simp: add.commute left_right_m)
        ultimately have "¦a ((2 * real j + 1) / 2 ^ n) -
                          leftcut (a ((2 * real j + 1) / 2 ^ n)) (b ((2 * real j + 1) / 2 ^ n)) (c ((2 * real j + 1) / 2 ^ n))¦
                    2/2 ^ Suc n"
          by (simp add: c_def midpoint_def)
        with j k n > 0 show ?thesis
          by (simp add: add.commute [of 1] a41 b41 del: power_Suc)
      next
        case False
        then obtain j where j: "k = 2*j + 1" by (metis oddE)
        have "¦a ((2 * real j + 1) / 2 ^ n) - (b ((2 * real j + 1) / 2 ^ n))¦  2/2 ^ n"
          using Suc.IH [OF False] j by (auto simp: algebra_simps)
        moreover have "c ((2 * real j + 1) / 2 ^ n) 
                       rightcut (a ((2 * real j + 1) / 2 ^ n)) (b ((2 * real j + 1) / 2 ^ n)) (c ((2 * real j + 1) / 2 ^ n))"
          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"]
          by (auto simp: add.commute left_right_m)
        moreover have "rightcut (a ((2 * real j + 1) / 2 ^ n)) (b ((2 * real j + 1) / 2 ^ n)) (c ((2 * real j + 1) / 2 ^ n)) 
                         b ((2 * real j + 1) / 2 ^ n)"
          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"]
          by (auto simp: add.commute left_right)
        ultimately have "¦rightcut (a ((2 * real j + 1) / 2 ^ n)) (b ((2 * real j + 1) / 2 ^ n)) (c ((2 * real j + 1) / 2 ^ n)) -
                          b ((2 * real j + 1) / 2 ^ n)¦    2/2 ^ Suc n"
          by (simp add: c_def midpoint_def)
        with j k n > 0 show ?thesis
          by (simp add: add.commute [of 3] a43 b43 del: power_Suc)
      qed
    qed
  qed
  have m1_to_3: "4 * real k - 1 = real (4 * (k-1)) + 3" if "0 < k" for k
    using that by auto
  have fb_eq_fa: "0 < j; 2*j < 2 ^ n  f(b((2 * real j - 1) / 2^n)) = f(a((2 * real j + 1) / 2^n))" for n j
  proof (induction n arbitrary: j)
    case 0
    then show ?case by auto
  next
    case (Suc n j) show ?case
    proof (cases "n > 0")
      case False
      with Suc.prems show ?thesis by auto
    next
      case True
      show ?thesis 
      proof (cases "even j")
        case True
        then obtain k where k: "j = 2*k" by (metis evenE)
        with 0 < j have "k > 0" "2 * k < 2 ^ n"
          using Suc.prems(2) k by auto
        with k 0 < n Suc.IH [of k] show ?thesis
          apply (simp add: m1_to_3 a41 b43 del: power_Suc of_nat_diff)
          by simp
      next
        case False
        then obtain k where k: "j = 2*k + 1" by (metis oddE)
        have "f (leftcut (a ((2 * k + 1) / 2^n)) (b ((2 * k + 1) / 2^n)) (c ((2 * k + 1) / 2^n)))
              = f (c ((2 * k + 1) / 2^n))"
          "f (c ((2 * k + 1) / 2^n))
              = f (rightcut (a ((2 * k + 1) / 2^n)) (b ((2 * k + 1) / 2^n)) (c ((2 * k + 1) / 2^n)))"
          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
          using left_right_m [of "c((2*k + 1) / 2^n)" "a((2*k + 1) / 2^n)" "b((2*k + 1) / 2^n)"]
          by (auto simp: add.commute  feqm [OF order_refl]  feqm [OF _ order_refl, symmetric])
        then
        show ?thesis
          by (simp add: k add.commute [of 1] add.commute [of 3] a43 b410 < n del: power_Suc)
      qed
    qed
  qed
  have f_eq_fc: "0 < j; j < 2 ^ n
                  f(b((2*j - 1) / 2 ^ (Suc n))) = f(c(j / 2^n)) 
                     f(a((2*j + 1) / 2 ^ (Suc n))) = f(c(j / 2^n))" for n and j::nat
  proof (induction n arbitrary: j)
    case 0
    then show ?case by auto
  next
    case (Suc n)
    show ?case
    proof (cases "even j")
      case True
      then obtain k where k: "j = 2*k" by (metis evenE)
      then have less2n: "k < 2 ^ n"
        using Suc.prems(2) by auto
      have "0 < k" using 0 < j k by linarith
      then have m1_to_3: "real (4 * k - Suc 0) = real (4 * (k-1)) + 3"
        by auto
      then show ?thesis
        using Suc.IH [of k] k 0 < k
        by (simp add: less2n add.commute [of 1] m1_to_3 a41 b43 del: power_Suc of_nat_diff) auto
    next
      case False
      then obtain k where k: "j = 2*k + 1" by (metis oddE)
      with Suc.prems have "k < 2^n" by auto
      show ?thesis
        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
        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)"]
        apply (simp add: add.commute [of 1] add.commute [of 3] m1_to_3 b41 a43 del: power_Suc)
        apply (force intro: feqm)
        done
    qed
  qed
  define D01 where "D01  {0<..<1}  (k m. {real m / 2^k})"
  have cloD01 [simp]: "closure D01 = {0..1}"
    unfolding D01_def
    by (subst closure_dyadic_rationals_in_convex_set_pos_1) auto
  have "uniformly_continuous_on D01 (f  c)"
  proof (clarsimp simp: uniformly_continuous_on_def)
    fix e::real
    assume "0 < e"
    have ucontf: "uniformly_continuous_on {0..1} f"
      by (simp add: compact_uniformly_continuous [OF cont_f])
    then obtain d where "0 < d" and d: "x x'. x  {0..1}; x'  {0..1}; norm (x' - x) < d  norm (f x' - f x) < e/2"
      unfolding uniformly_continuous_on_def dist_norm
      by (metis 0 < e less_divide_eq_numeral1(1) mult_zero_left)
    obtain n where n: "1/2^n < min d 1"
      by (metis 0 < d 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)
    with gr0I have "n > 0"
      by (force simp: field_split_simps)
    show "d>0. xD01. x'D01. dist x' x < d  dist (f (c x')) (f (c x)) < e"
    proof (intro exI ballI impI conjI)
      show "(0::real) < 1/2^n" by auto
    next
      have dist_fc_close: "dist (f(c(real i / 2^m))) (f(c(real j / 2^n))) < e/2"
        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
      proof -
        have abs3: "¦x - a¦ < e  x = a  ¦x - (a - e/2)¦ < e/2  ¦x - (a + e/2)¦ < e/2" for x a e::real
          by linarith
        consider "i / 2 ^ m = j / 2 ^ n"
          | "¦i / 2 ^ m - (2 * j - 1) / 2 ^ Suc n¦ < 1/2 ^ Suc n"
          | "¦i / 2 ^ m - (2 * j + 1) / 2 ^ Suc n¦ < 1/2 ^ Suc n"
          using abs3 [OF clo] j by (auto simp: field_simps of_nat_diff)
        then show ?thesis
        proof cases
          case 1 with 0 < e show ?thesis by auto
        next
          case 2
          have *: "abs(a - b)  1/2 ^ n  1/2 ^ n < d  a  c  c  b  b - c < d" for a b c
            by auto
          have "norm (c (real i / 2 ^ m) - b (real (2 * j - 1) / 2 ^ Suc n)) < d"
            using 2 j n close_ab [of "2*j-1" "Suc n"]
            using b_ge_0 [of "2*j-1" "Suc n"] b_le_1 [of "2*j-1" "Suc n"]
            using aj_le_ci [of "2*j-1" i m "Suc n"]
            using ci_le_bj [of "2*j-1" i m "Suc n"]
            apply (simp add: divide_simps of_nat_diff del: power_Suc)
            apply (auto simp: divide_simps intro!: *)
            done
          moreover have "f(c(j / 2^n)) = f(b ((2*j - 1) / 2 ^ (Suc n)))"
            using f_eq_fc [OF j] by metis
          ultimately show ?thesis
            by (metis dist_norm atLeastAtMost_iff b_ge_0 b_le_1 c_ge_0 c_le_1 d)
        next
          case 3
          have *: "abs(a - b)  1/2 ^ n  1/2 ^ n < d  a  c  c  b  c - a < d" for a b c
            by auto
          have "norm (c (real i / 2 ^ m) - a (real (2 * j + 1) / 2 ^ Suc n)) < d"
            using 3 j n close_ab [of "2*j+1" "Suc n"]
            using b_ge_0 [of "2*j+1" "Suc n"] b_le_1 [of "2*j+1" "Suc n"]
            using aj_le_ci [of "2*j+1" i m "Suc n"]
            using ci_le_bj [of "2*j+1" i m "Suc n"]
            apply (simp add: divide_simps of_nat_diff del: power_Suc)
            apply (auto simp: divide_simps intro!: *)
            done
          moreover have "f(c(j / 2^n)) = f(a ((2*j + 1) / 2 ^ (Suc n)))"
            using f_eq_fc [OF j] by metis
          ultimately show ?thesis
            by (metis dist_norm a_ge_0 atLeastAtMost_iff a_ge_0 a_le_1 c_ge_0 c_le_1 d)
        qed
      qed
      show "dist (f (c x')) (f (c x)) < e"
        if "x  D01" "x'  D01" "dist x' x < 1/2^n" for x x'
        using that unfolding D01_def dyadics_in_open_unit_interval
      proof clarsimp
        fix i k::nat and m p
        assume i: "0 < i" "i < 2 ^ m" and k: "0<k" "k < 2 ^ p"
        assume clo: "dist (real k / 2 ^ p) (real i / 2 ^ m) < 1/2 ^ n"
        obtain j::nat where "0 < j" "j < 2 ^ n"
          and clo_ij: "abs(i / 2^m - j / 2^n) < 1/2 ^ n"
          and clo_kj: "abs(k / 2^p - j / 2^n) < 1/2 ^ n"
        proof -
          have "max (2^n * i / 2^m) (2^n * k / 2^p)  0"
            by (auto simp: le_max_iff_disj)
          then obtain j where "floor (max (2^n*i / 2^m) (2^n*k / 2^p)) = int j"
            using zero_le_floor zero_le_imp_eq_int by blast
          then have j_le: "real j  max (2^n * i / 2^m) (2^n * k / 2^p)"
            and less_j1: "max (2^n * i / 2^m) (2^n * k / 2^p) < real j + 1"
            using floor_correct [of "max (2^n * i / 2^m) (2^n * k / 2^p)"] by linarith+
          show thesis
          proof (cases "j = 0")
            case True
            show thesis
            proof
              show "(1::nat) < 2 ^ n"
                by (metis Suc_1 0 < n lessI one_less_power)
              show "¦real i / 2 ^ m - real 1/2 ^ n¦ < 1/2 ^ n"
                using i less_j1 by (simp add: dist_norm field_simps True)
              show "¦real k / 2 ^ p - real 1/2 ^ n¦ < 1/2 ^ n"
                using k less_j1 by (simp add: dist_norm field_simps True)
            qed simp
          next
            case False
            have 1: "real j * 2 ^ m < real i * 2 ^ n"
              if j: "real j * 2 ^ p  real k * 2 ^ n" and k: "real k * 2 ^ m < real i * 2 ^ p"
              for i k m p
            proof -
              have "real j * 2 ^ p * 2 ^ m  real k * 2 ^ n * 2 ^ m"
                using j by simp
              moreover have "real k * 2 ^ m * 2 ^ n < real i * 2 ^ p * 2 ^ n"
                using k by simp
              ultimately have "real j * 2 ^ p * 2 ^ m < real i * 2 ^ p * 2 ^ n"
                by (simp only: mult_ac)
              then show ?thesis
                by simp
            qed
            have 2: "real j * 2 ^ m < 2 ^ m + real i * 2 ^ n"
              if j: "real j * 2 ^ p  real k * 2 ^ n" and k: "real k * (2 ^ m * 2 ^ n) < 2 ^ m * 2 ^ p + real i * (2 ^ n * 2 ^ p)"
              for i k m p
            proof -
              have "real j * 2 ^ p * 2 ^ m  real k * (2 ^ m * 2 ^ n)"
                using j by simp
              also have "... < 2 ^ m * 2 ^ p + real i * (2 ^ n * 2 ^ p)"
                by (rule k)
              finally have "(real j * 2 ^ m) * 2 ^ p < (2 ^ m + real i * 2 ^ n) * 2 ^ p"
                by (simp add: algebra_simps)
              then show ?thesis
                by simp
            qed
            have 3: "real j * 2 ^ p < 2 ^ p + real k * 2 ^ n"
              if j: "real j * 2 ^ m  real i * 2 ^ n" and i: "real i * 2 ^ p  real k * 2 ^ m"
            proof -
              have "real j * 2 ^ m * 2 ^ p  real i * 2 ^ n * 2 ^ p"
                using j by simp
              moreover have "real i * 2 ^ p * 2 ^ n  real k * 2 ^ m * 2 ^ n"
                using i by simp
              ultimately have "real j * 2 ^ m * 2 ^ p  real k * 2 ^ m * 2 ^ n"
                by (simp only: mult_ac)
              then have "real j * 2 ^ p  real k * 2 ^ n"
                by simp
              also have "... < 2 ^ p + real k * 2 ^ n"
                by auto
              finally show ?thesis by simp
            qed
            show ?thesis
            proof
              have "2 ^ n * real i / 2 ^ m < 2 ^ n" "2 ^ n * real k / 2 ^ p < 2 ^ n"
                using i k by (auto simp: field_simps)
              then have "max (2^n * i / 2^m) (2^n * k / 2^p) < 2^n"
                by simp
              with j_le have "real j < 2 ^ n" by linarith 
              then show "j < 2 ^ n"
                by auto
              have "¦real i * 2 ^ n - real j * 2 ^ m¦ < 2 ^ m"
                using clo less_j1 j_le
                 by (auto simp: le_max_iff_disj field_split_simps dist_norm abs_if split: if_split_asm dest: 1 2)
              then show "¦real i / 2 ^ m - real j / 2 ^ n¦ < 1/2 ^ n"
                by (auto simp: field_split_simps)
              have "¦real k * 2 ^ n - real j * 2 ^ p¦ < 2 ^ p"
                using clo less_j1 j_le
                by (auto simp: le_max_iff_disj field_split_simps dist_norm abs_if split: if_split_asm dest: 3 2)
              then show "¦real k / 2 ^ p - real j / 2 ^ n¦ < 1/2 ^ n"
                by (auto simp: le_max_iff_disj field_split_simps dist_norm)
            qed (use False in simp)
          qed
        qed
        show "dist (f (c (real k / 2 ^ p))) (f (c (real i / 2 ^ m))) < e"
        proof (rule dist_triangle_half_l)
          show "dist (f (c (real k / 2 ^ p))) (f(c(j / 2^n))) < e/2"
            using 0 < j j < 2 ^ n k clo_kj 
            by (intro dist_fc_close) auto
          show "dist (f (c (real i / 2 ^ m))) (f (c (real j / 2 ^ n))) < e/2"
            using 0 < j j < 2 ^ n i clo_ij 
            by (intro dist_fc_close) auto
        qed
      qed
    qed
  qed
  then obtain h where ucont_h: "uniformly_continuous_on {0..1} h"
    and fc_eq: "x. x  D01  (f  c) x = h x"
  proof (rule uniformly_continuous_on_extension_on_closure [of D01 "f  c"])
  qed (use closure_subset [of D01] in auto intro!: that)
  then have cont_h: "continuous_on {0..1} h"
    using uniformly_continuous_imp_continuous by blast
  have h_eq: "h (real k / 2 ^ m) = f (c (real k / 2 ^ m))" if "0 < k" "k < 2^m" for k m
    using fc_eq that by (force simp: D01_def)
  have "h ` {0..1} = f ` {0..1}"
  proof
    have "h ` (closure D01)  f ` {0..1}"
    proof (rule image_closure_subset)
      show "continuous_on (closure D01) h"
        using cont_h by simp
      show "closed (f ` {0..1})"
        using compact_continuous_image [OF cont_f] compact_imp_closed by blast
      show "h ` D01  f ` {0..1}"
        by (force simp: dyadics_in_open_unit_interval D01_def h_eq)
    qed
    with cloD01 show "h ` {0..1}  f ` {0..1}" by simp
    have a12 [simp]: "a (1/2) = u"
      by (metis a_def leftrec_base numeral_One of_nat_numeral)
    have b12 [simp]: "b (1/2) = v"
      by (metis b_def rightrec_base numeral_One of_nat_numeral)
    have "f ` {0..1}  closure(h ` D01)"
    proof (clarsimp simp: closure_approachable dyadics_in_open_unit_interval D01_def)
      fix x e::real
      assume "0  x" "x  1" "0 < e"
      have ucont_f: "uniformly_continuous_on {0..1} f"
        using compact_uniformly_continuous cont_f by blast
      then obtain δ where "δ > 0"
        and δ: "x x'. x  {0..1}; x'  {0..1}; dist x' x < δ  norm (f x' - f x) < e"
        using 0 < e by (auto simp: uniformly_continuous_on_def dist_norm)
      have *: "m::nat. y. odd m  0 < m  m < 2 ^ n  y  {a(m / 2^n) .. b(m / 2^n)}  f y = f x"
        if "n  0" for n
        using that
      proof (induction n)
        case 0 then show ?case by auto
      next
        case (Suc n)
        show ?case
        proof (cases "n=0")
          case True
          consider "x  {0..u}" | "x  {u..v}" | "x  {v..1}"
            using 0  x x  1 by force
          then have "ya (real 1/2). y  b (real 1/2)  f y = f x"
          proof cases
            case 1
            then show ?thesis
              using uabv [of 1 1] f0u [of u] f0u [of x] by force
          next
            case 2
            then show ?thesis
              by (rule_tac x=x in exI) auto
          next
            case 3
            then show ?thesis
              using uabv [of 1 1] fv1 [of v] fv1 [of x] by force
          qed
          with n=0 show ?thesis
            by (rule_tac x=1 in exI) auto
        next
          case False
          with Suc obtain m y
            where "odd m" "0 < m" and mless: "m < 2 ^ n"
              and y: "y  {a (real m / 2 ^ n)..b (real m / 2 ^ n)}" and feq: "f y = f x"
            by metis
          then obtain j where j: "m = 2*j + 1" by (metis oddE)
          have j4: "4 * j + 1 < 2 ^ Suc n"
            using mless j by (simp add: algebra_simps)

          consider "y  {a((2*j + 1) / 2^n) .. b((4*j + 1) / 2 ^ (Suc n))}"
            | "y  {b((4*j + 1) / 2 ^ (Suc n)) .. a((4*j + 3) / 2 ^ (Suc n))}"
            | "y  {a((4*j + 3) / 2 ^ (Suc n)) .. b((2*j + 1) / 2^n)}"
            using y j by force
          then show ?thesis
          proof cases
            case 1
            show ?thesis
            proof (intro exI conjI)
              show "y  {a (real (4 * j + 1) / 2 ^ Suc n)..b (real (4 * j + 1) / 2 ^ Suc n)}"
                using mless j n  0 1 by (simp add: a41 b41 add.commute [of 1] del: power_Suc)
            qed (use feq j4 in auto)
          next
            case 2
            show ?thesis
            proof (intro exI conjI)
              show "b (real (4 * j + 1) / 2 ^ Suc n)  {a (real (4 * j + 1) / 2 ^ Suc n)..b (real (4 * j + 1) / 2 ^ Suc n)}"
                using n  0 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]
                using left_right [of "c((2*j + 1) / 2^n)" "a((2*j + 1) / 2^n)" "b((2*j + 1) / 2^n)"]
                by (simp add: a41 b41 add.commute [of 1] del: power_Suc)
              show "f (b (real (4 * j + 1) / 2 ^ Suc n)) = f x"
                using n  0 2 
                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]
                by (force simp add: b41 a43 add.commute [of 1] feq [symmetric] simp del: power_Suc intro: f_eqI)
            qed (use j4 in auto)
          next
            case 3
            show ?thesis
            proof (intro exI conjI)
              show "4 * j + 3 < 2 ^ Suc n"
                using mless j by simp
              show "f y = f x"
                by fact
              show "y  {a (real (4 * j + 3) / 2 ^ Suc n) .. b (real (4 * j + 3) / 2 ^ Suc n)}"
                using 3 False b43 [of n j] by (simp add: add.commute)
            qed (use 3 in auto)
          qed
        qed
      qed
      obtain n where n: "1/2^n < min (δ / 2) 1"
        by (metis 0 < δ 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)
      with gr0I have "n  0"
        by fastforce
      with * obtain m::nat and y
        where "odd m" "0 < m" and mless: "m < 2 ^ n"
          and y: "a(m / 2^n)  y  y  b(m / 2^n)" and feq: "f x = f y"
        by (metis atLeastAtMost_iff)
      then have "0  y" "y  1"
        by (meson a_ge_0 b_le_1 order.trans)+
      moreover have "y < δ + c (real m / 2 ^ n)" "c (real m / 2 ^ n) < δ + y"
        using y alec [of m n] cleb [of m n] n field_sum_of_halves close_ab [OF odd m, of n]
        by linarith+
      moreover note 0 < m mless 0  x x  1
      ultimately have "dist (h (real m / 2 ^ n)) (f x) < e"
        by (auto simp: dist_norm h_eq feq δ)
      then show "k. m{0<..<2 ^ k}. dist (h (real m / 2 ^ k)) (f x) < e"
        using 0 < m greaterThanLessThan_iff mless by blast
    qed
    also have "...  h ` {0..1}"
    proof (rule closure_minimal)
      show "h ` D01  h ` {0..1}"
        using cloD01 closure_subset by blast
      show "closed (h ` {0..1})"
        using compact_continuous_image [OF cont_h] compact_imp_closed by auto
    qed
    finally show "f ` {0..1}  h ` {0..1}" .
  qed
  moreover have "inj_on h {0..1}"
  proof -
    have "u < v"
      by (metis atLeastAtMost_iff f0u f_1not0 fv1 order.not_eq_order_implies_strict u01(1) u01(2) v01(1))
    have f_not_fu: "x. u < x; x  v  f x  f u"
      by (metis atLeastAtMost_iff f0u fu1 greaterThanAtMost_iff order_refl order_trans u01(1) v01(2))
    have f_not_fv: "x. u  x; x < v  f x  f v"
      by (metis atLeastAtMost_iff order_refl order_trans v01(2) atLeastLessThan_iff fuv fv1)
    have a_less_b:
         "a(j / 2^n) < b(j / 2^n) 
          (x. a(j / 2^n) < x  x  b(j / 2^n)  f x  f(a(j / 2^n))) 
          (x. a(j / 2^n)  x  x < b(j / 2^n)  f x  f(b(j / 2^n)))" for n and j::nat
    proof (induction n arbitrary: j)
      case 0 then show ?case
        by (simp add: u < v f_not_fu f_not_fv)
    next
      case (Suc n j) show ?case
      proof (cases "n > 0")
        case False then show ?thesis
          by (auto simp: a_def b_def leftrec_base rightrec_base u < v f_not_fu f_not_fv)
      next
        case True show ?thesis
        proof (cases "even j")
          case True
          with 0 < n Suc.IH show ?thesis
            by (auto elim!: evenE)
        next
          case False
          then obtain k where k: "j = 2*k + 1" by (metis oddE)
          then show ?thesis
          proof (cases "even k")
            case True
            then obtain m where m: "k = 2*m" by (metis evenE)
            have fleft: "f (leftcut (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))"
              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]
              using left_right_m [of "c((2*m + 1) / 2^n)" "a((2*m + 1) / 2^n)" "b((2*m + 1) / 2^n)"]
              by (auto intro: f_eqI)
            show ?thesis
            proof (intro conjI impI notI allI)
              have False if "b (real j / 2 ^ Suc n)  a (real j / 2 ^ Suc n)"
              proof -
                have "f (c ((1 + real m * 2) / 2 ^ n)) = f (a ((1 + real m * 2) / 2 ^ n))"
                  using k m 0 < n fleft that a41 [of n m] b41 [of n m]
                  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]
                  using left_right [of "c((2*m + 1) / 2^n)" "a((2*m + 1) / 2^n)" "b((2*m + 1) / 2^n)"]
                  by (auto simp: algebra_simps)
                moreover have "a (real (1 + m * 2) / 2 ^ n) < c (real (1 + m * 2) / 2 ^ n)"
                  using Suc.IH [of "1 + m * 2"] by (simp add: c_def midpoint_def)
                moreover have "c (real (1 + m * 2) / 2 ^ n)  b (real (1 + m * 2) / 2 ^ n)"
                  using cleb by blast
                ultimately show ?thesis
                  using Suc.IH [of "1 + m * 2"] by force
              qed
              then show "a (real j / 2 ^ Suc n) < b (real j / 2 ^ Suc n)" by force
            next
              fix x
              assume "a (real j / 2 ^ Suc n) < x" "x  b (real j / 2 ^ Suc n)" "f x = f (a (real j / 2 ^ Suc n))"
              then show False
                using Suc.IH [of "1 + m * 2", THEN conjunct2, THEN conjunct1]
                using k m 0 < n a41 [of n m] b41 [of n m]
                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]
                using left_right_m [of "c((2*m + 1) / 2^n)" "a((2*m + 1) / 2^n)" "b((2*m + 1) / 2^n)"]
                by (auto simp: algebra_simps)
            next
              fix x
              assume "a (real j / 2 ^ Suc n)  x" "x < b (real j / 2 ^ Suc n)" "f x = f (b (real j / 2 ^ Suc n))"
              then show False
                using k m 0 < n a41 [of n m] b41 [of n m] fleft left_neq
                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]
                by (auto simp: algebra_simps)
            qed
          next
            case False
            with oddE obtain m where m: "k = Suc (2*m)" by fastforce
            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))"
              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]
              using left_right_m [of "c((2*m + 1) / 2^n)" "a((2*m + 1) / 2^n)" "b((2*m + 1) / 2^n)"]
              by (auto intro: f_eqI [OF _ order_refl])
            show ?thesis
            proof (intro conjI impI notI allI)
              have False if "b (real j / 2 ^ Suc n)  a (real j / 2 ^ Suc n)"
              proof -
                have "f (c ((1 + real m * 2) / 2 ^ n)) = f (b ((1 + real m * 2) / 2 ^ n))"
                  using k m 0 < n fright that a43 [of n m] b43 [of n m]
                  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]
                  using left_right [of "c((2*m + 1) / 2^n)" "a((2*m + 1) / 2^n)" "b((2*m + 1) / 2^n)"]
                  by (auto simp: algebra_simps)
                moreover have "a (real (1 + m * 2) / 2 ^ n)  c (real (1 + m * 2) / 2 ^ n)"
                  using alec by blast
                moreover have "c (real (1 + m * 2) / 2 ^ n) < b (real (1 + m * 2) / 2 ^ n)"
                  using Suc.IH [of "1 + m * 2"] by (simp add: c_def midpoint_def)
                ultimately show ?thesis
                  using Suc.IH [of "1 + m * 2"] by force
              qed
              then show "a (real j / 2 ^ Suc n) < b (real j / 2 ^ Suc n)" by force
            next
              fix x
              assume "a (real j / 2 ^ Suc n) < x" "x  b (real j / 2 ^ Suc n)" "f x = f (a (real j / 2 ^ Suc n))"
              then show False
                using k m 0 < n a43 [of n m] b43 [of n m] fright right_neq
                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]
                by (auto simp: algebra_simps)
            next
              fix x
              assume "a (real j / 2 ^ Suc n)  x" "x < b (real j / 2 ^ Suc n)" "f x = f (b (real j / 2 ^ Suc n))"
              then show False
                using Suc.IH [of "1 + m * 2", THEN conjunct2, THEN conjunct2]
                using k m 0 < n a43 [of n m] b43 [of n m]
                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]
                using left_right_m [of "c((2*m + 1) / 2^n)" "a((2*m + 1) / 2^n)" "b((2*m + 1) / 2^n)"]
                by (auto simp: algebra_simps fright simp del: power_Suc)
            qed
          qed
        qed
      qed
    qed
    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
      using a_less_b [of m n] apply (simp_all add: c_def midpoint_def)
      using a_ge_0 [of m n] b_le_1 [of m n] by linarith+
    have approx: "j n. odd j  n  0 
                        real i / 2^m  real j / 2^n 
                        real j / 2^n  real k / 2^p 
                        ¦real i / 2 ^ m - real j / 2 ^ n¦ < 1/2^n 
                        ¦real k / 2 ^ p - real j / 2 ^ n¦ < 1/2^n"
      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
      using that
    proof (induction N arbitrary: m p i k rule: less_induct)
      case (less N)
      then consider "i / 2^m  1/2" "1/2  k / 2^p" | "k / 2^p < 1/2" | "k / 2^p  1/2" "1/2 < i / 2^m"
        by linarith
      then show ?case
      proof cases
        case 1
        with less.prems show ?thesis
          by (rule_tac x=1 in exI)+ (fastforce simp: field_split_simps)
      next
        case 2 show ?thesis
        proof (cases m)
          case 0 with less.prems show ?thesis
            by auto
        next
          case (Suc m') show ?thesis
          proof (cases p)
            case 0 with less.prems show ?thesis by auto
          next
            case (Suc p')
            have §: False if "real i * 2 ^ p' < real k * 2 ^ m'" "k < 2 ^ p'" "2 ^ m'  i"
            proof -
              have "real k * 2 ^ m' < 2 ^ p' * 2 ^ m'"
                using that by simp
              then have "real i * 2 ^ p' < 2 ^ p' * 2 ^ m'"
                using that by linarith
              with that show ?thesis by simp
            qed
            moreover have *: "real i / 2 ^ m' < real k / 2^p'"  "k < 2 ^ p'"
              using less.prems m = Suc m' 2 Suc by (force simp: field_split_simps)+
            moreover have "i < 2 ^ m' "
              using § * by (clarsimp simp: divide_simps linorder_not_le) (meson linorder_not_le)
            ultimately show ?thesis
              using less.IH [of "m'+p'" i m' k p'] less.prems m = Suc m' 2 Suc
              by (force simp: field_split_simps)
          qed
        qed
      next
        case 3 show ?thesis
        proof (cases m)
          case 0 with less.prems show ?thesis
            by auto
        next
          case (Suc m') show ?thesis
          proof (cases p)
            case 0 with less.prems show ?thesis by auto
          next
            case (Suc p')
            have "real (i - 2 ^ m') / 2 ^ m' < real (k - 2 ^ p') / 2 ^ p'"
              using less.prems m = Suc m' Suc 3  by (auto simp: field_simps of_nat_diff)
            moreover have "k - 2 ^ p' < 2 ^ p'" "i - 2 ^ m' < 2 ^ m'"
              using less.prems Suc m = Suc m' by auto
            moreover 
            have "2 ^ p'  k" "2 ^ p'  k"
              using less.prems m = Suc m' Suc 3 by auto
            then have "2 ^ p' < k"
              by linarith
            ultimately show ?thesis
              using less.IH [of "m'+p'" "i - 2^m'" m' "k - 2 ^ p'" p'] less.prems m = Suc m' Suc 3
              apply (clarsimp simp: field_simps of_nat_diff)
              apply (rule_tac x="2 ^ n + j" in exI, simp)
              apply (rule_tac x="Suc n" in exI)
              apply (auto simp: field_simps)
              done
          qed
        qed
      qed
    qed
    have clec: "c(real i / 2^m)  c(real j / 2^n)"
      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
    proof -
      obtain j' n' where "odd j'" "n'  0"
        and i_le_j: "real i / 2 ^ m  real j' / 2 ^ n'"
        and j_le_j: "real j' / 2 ^ n'  real j / 2 ^ n"
        and clo_ij: "¦real i / 2 ^ m - real j' / 2 ^ n'¦ < 1/2 ^ n'"
        and clo_jj: "¦real j / 2 ^ n - real j' / 2 ^ n'¦ < 1/2 ^ n'"
        using approx [of i m j n "m+n"] that i j ij by auto
      with oddE obtain q where q: "j' = Suc (2*q)" by fastforce
      have "c (real i / 2 ^ m)  c((2*q + 1) / 2^n')"
      proof (cases "i / 2^m = (2*q + 1) / 2^n'")
        case True then show ?thesis by simp
      next
        case False
        with i_le_j clo_ij q have "¦real i / 2 ^ m - real (4 * q + 1) / 2 ^ Suc n'¦ < 1 / 2 ^ Suc n'"
          by (auto simp: field_split_simps)
        then have "c(i / 2^m)  b(real(4 * q + 1) / 2 ^ (Suc n'))"
          by (meson ci_le_bj even_mult_iff even_numeral even_plus_one_iff)
        then show ?thesis
          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] n'  0
          using left_right_m [of "c((2*q + 1) / 2^n')" "a((2*q + 1) / 2^n')" "b((2*q + 1) / 2^n')"]
          by (auto simp: algebra_simps)
      qed
      also have "...  c(real j / 2^n)"
      proof (cases "j / 2^n = (2*q + 1) / 2^n'")
        case True
        then show ?thesis by simp
      next
        case False
        with j_le_j q have less: "(2*q + 1) / 2^n' < j / 2^n"
          by auto
        have *: "q < i; abs(i - q) < s*2; r = q + s  abs(i - r) < s" for i q s r::real
          by auto
        have "¦real j / 2 ^ n - real (4 * q + 3) / 2 ^ Suc n'¦ < 1 / 2 ^ Suc n'"
          by (rule * [OF less]) (use j_le_j clo_jj q  in auto simp: field_split_simps)
        then have "a(real(4*q + 3) / 2 ^ (Suc n'))  c(j / 2^n)"
          by (metis Suc3_eq_add_3 add.commute aj_le_ci even_Suc even_mult_iff even_numeral)
        then show ?thesis
          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] n'  0
          using left_right_m [of "c((2*q + 1) / 2^n')" "a((2*q + 1) / 2^n')" "b((2*q + 1) / 2^n')"]
          by (auto simp: algebra_simps)
      qed
      finally show ?thesis .
    qed
    have "x = y" if "0  x" "x  1" "0  y" "y  1" "h x = h y" for x y
      using that
    proof (induction x y rule: linorder_class.linorder_less_wlog)
      case (less x1 x2)
      obtain m n where m: "0 < m" "m < 2 ^ n"
        and x12: "x1 < m / 2^n" "m / 2^n < x2"
        and neq: "h x1  h (real m / 2^n)"
      proof -
        have "(x1 + x2) / 2  closure D01"
          using cloD01 less.hyps less.prems by auto
        with less obtain y where "y  D01" and dist_y: "dist y ((x1 + x2) / 2) < (x2 - x1) / 64"
          unfolding closure_approachable
          by (metis diff_gt_0_iff_gt less_divide_eq_numeral1(1) mult_zero_left)
        obtain m n where m: "0 < m" "m < 2 ^ n"
                     and clo: "¦real m / 2 ^ n - (x1 + x2) / 2¦ < (x2 - x1) / 64"
                     and n: "1/2^n < (x2 - x1) / 128"
        proof -
          have "min 1 ((x2 - x1) / 128) > 0" "1/2 < (1::real)"
            using less by auto
          then obtain N where N: "1/2^N < min 1 ((x2 - x1) / 128)"
            by (metis power_one_over real_arch_pow_inv)
          then have "N > 0"
            using less_divide_eq_1 by force
          obtain p q where p: "p < 2 ^ q" "p  0" and yeq: "y = real p / 2 ^ q"
            using y  D01 by (auto simp: zero_less_divide_iff D01_def)
          show ?thesis
          proof
            show "0 < 2^N * p"
              using p by auto
            show "2 ^ N * p < 2 ^ (N+q)"
              by (simp add: p power_add)
            have "¦real (2 ^ N * p) / 2 ^ (N + q) - (x1 + x2) / 2¦ = ¦real p / 2 ^ q - (x1 + x2) / 2¦"
              by (simp add: power_add)
            also have "... = ¦y - (x1 + x2) / 2¦"
              by (simp add: yeq)
            also have "... < (x2 - x1) / 64"
              using dist_y by (simp add: dist_norm)
            finally show "¦real (2 ^ N * p) / 2 ^ (N + q) - (x1 + x2) / 2¦ < (x2 - x1) / 64" .
            have "(1::real) / 2 ^ (N + q)  1/2^N"
              by (simp add: field_simps)
            also have "... < (x2 - x1) / 128"
              using N by force
            finally show "1/2 ^ (N + q) < (x2 - x1) / 128" .
          qed
        qed
        obtain m' n' m'' n'' where "0 < m'" "m' < 2 ^ n'" "x1 < m' / 2^n'" "m' / 2^n' < x2"
          and "0 < m''" "m'' < 2 ^ n''" "x1 < m'' / 2^n''" "m'' / 2^n'' < x2"
          and neq: "h (real m'' / 2^n'')  h (real m' / 2^n')"
        proof
          show "0 < Suc (2*m)"
            by simp
          show m21: "Suc (2*m) < 2 ^ Suc n"
            using m by auto
          show "x1 < real (Suc (2 * m)) / 2 ^ Suc n"
            using clo by (simp add: field_simps abs_if split: if_split_asm)
          show "real (Suc (2 * m)) / 2 ^ Suc n < x2"
            using n clo by (simp add: field_simps abs_if split: if_split_asm)
          show "0 < 4*m + 3"
            by simp
          have "m+1  2 ^ n"
            using m by simp
          then have "4 * (m+1)  4 * (2 ^ n)"
            by simp
          then show m43: "4*m + 3 < 2 ^ (n+2)"
            by (simp add: algebra_simps)
          show "x1 < real (4 * m + 3) / 2 ^ (n + 2)"
            using clo by (simp add: field_simps abs_if split: if_split_asm)
          show "real (4 * m + 3) / 2 ^ (n + 2) < x2"
            using n clo by (simp add: field_simps abs_if split: if_split_asm)
          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)"
            by (simp add: c_def)
          define R where "R  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))"
          have "R < b ((2 * real m + 1) / 2 ^ Suc n)"
            unfolding R_def  using a_less_b [of "4*m + 3" "n+2"] a43 [of "Suc n" m] b43 [of "Suc n" m]
            by simp
          then have Rless: "R < midpoint R (b ((2 * real m + 1) / 2 ^ Suc n))"
            by (simp add: midpoint_def)
          have midR_le: "midpoint R (b ((2 * real m + 1) / 2 ^ Suc n))  b ((2 * real m + 1) / (2 * 2 ^ n))"
            using R < b ((2 * real m + 1) / 2 ^ Suc n)
            by (simp add: midpoint_def)
          have "(real (Suc (2 * m)) / 2 ^ Suc n)  D01"  "real (4 * m + 3) / 2 ^ (n + 2)  D01"
            by (simp_all add: D01_def m21 m43 del: power_Suc of_nat_Suc of_nat_add add_2_eq_Suc') blast+
          then show "h (real (4 * m + 3) / 2 ^ (n + 2))  h (real (Suc (2 * m)) / 2 ^ Suc n)"
            using a_less_b [of "4*m + 3" "n+2", THEN conjunct1]
            using a43 [of "Suc n" m] b43 [of "Suc n" m]
            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"]
            apply (simp add: fc_eq [symmetric] c_def del: power_Suc)
            apply (simp only: add.commute [of 1] c_fold R_def [symmetric])
            apply (rule right_neq)
            using Rless apply (simp add: R_def)
               apply (rule midR_le, auto)
            done
        qed
        then show ?thesis by (metis that)
      qed
      have m_div: "0 < m / 2^n" "m / 2^n < 1"
        using m  by (auto simp: field_split_simps)
      have closure0m: "{0..m / 2^n} = closure ({0<..< m / 2^n}  (k m. {real m / 2 ^ k}))"
        by (subst closure_dyadic_rationals_in_convex_set_pos_1, simp_all add: not_le m)
      have "2^n > m"
        by (simp add: m(2) not_le)
      then have closurem1: "{m / 2^n .. 1} = closure ({m / 2^n <..< 1}  (k m. {real m / 2 ^ k}))"
        using closure_dyadic_rationals_in_convex_set_pos_1 m_div(1) by fastforce
      have cont_h': "continuous_on (closure ({u<..<v}  (k m. {real m / 2 ^ k}))) h"
        if "0  u" "v  1" for u v
        using that by (intro continuous_on_subset [OF cont_h] closure_minimal [OF subsetI]) auto
      have closed_f': "closed (f ` {u..v})" if "0  u" "v  1" for u v
        by (metis compact_continuous_image cont_f compact_interval atLeastatMost_subset_iff
            compact_imp_closed continuous_on_subset that)
      have less_2I: "k i. real i / 2 ^ k < 1  i < 2 ^ k"
        by simp
      have "h ` ({0<..<m / 2 ^ n}  (q p. {real p / 2 ^ q}))  f ` {0..c (m / 2 ^ n)}"
      proof clarsimp
        fix p q
        assume p: "0 < real p / 2 ^ q" "real p / 2 ^ q < real m / 2 ^ n"
        then have [simp]: "0 < p"
          by (simp add: field_split_simps)
        have [simp]: "p < 2 ^ q"
          by (blast intro: p less_2I m_div less_trans)
        have "f (c (real p / 2 ^ q))  f ` {0..c (real m / 2 ^ n)}"
          by (auto simp: clec p m)
        then show "h (real p / 2 ^ q)  f ` {0..c (real m / 2 ^ n)}"
          by (simp add: h_eq)
      qed
      with m_div have "h ` {0 .. m / 2^n}  f ` {0 .. c(m / 2^n)}"
        apply (subst closure0m)
        by (rule image_closure_subset [OF cont_h' closed_f']) auto
      then have hx1: "h x1  f ` {0 .. c(m / 2^n)}"
        using x12 less.prems(1) by auto
      then obtain t1 where t1: "h x1 = f t1" "0  t1" "t1  c (m / 2 ^ n)"
        by auto
      have "h ` ({m / 2 ^ n<..<1}  (q p. {real p / 2 ^ q}))  f ` {c (m / 2 ^ n)..1}"
      proof clarsimp
        fix p q
        assume p: "real m / 2 ^ n < real p / 2 ^ q" and [simp]: "p < 2 ^ q"
        then have [simp]: "0 < p"
          using gr_zeroI m_div by fastforce
        have "f (c (real p / 2 ^ q))  f ` {c (m / 2 ^ n)..1}"
          by (auto simp: clec p m)
        then show "h (real p / 2 ^ q)  f ` {c (real m / 2 ^ n)..1}"
          by (simp add: h_eq)
      qed
      with m have "h ` {m / 2^n .. 1}  f ` {c(m / 2^n) .. 1}"
        apply (subst closurem1)
        by (rule image_closure_subset [OF cont_h' closed_f']) auto
      then have hx2: "h x2  f ` {c(m / 2^n)..1}"
        using x12 less.prems by auto
      then obtain t2 where t2: "h x2 = f t2" "c (m / 2 ^ n)  t2" "t2  1"
        by auto
      with t1 less neq have False
        using conn [of "h x2", unfolded is_interval_connected_1 [symmetric] is_interval_1, rule_format, of t1 t2 "c(m / 2^n)"]
        by (simp add: h_eq m)
      then show ?case by blast
    qed auto
    then show ?thesis
      by (auto simp: inj_on_def)
  qed
  ultimately have "{0..1::real} homeomorphic f ` {0..1}"
    using homeomorphic_compact [OF _ cont_h] by blast
  then show ?thesis
    using homeomorphic_sym by blast
qed


theorem path_contains_arc:
  fixes p :: "real  'a::{complete_space,real_normed_vector}"
  assumes "path p" and a: "pathstart p = a" and b: "pathfinish p = b" and "a  b"
  obtains q where "arc q" "path_image q  path_image p" "pathstart q = a" "pathfinish q = b"
proof -
  have ucont_p: "uniformly_continuous_on {0..1} p"
    using path p unfolding path_def
    by (metis compact_Icc compact_uniformly_continuous)
  define φ where "φ  λS. S  {0..1}  0  S  1  S 
                           (x  S. y  S. open_segment x y  S = {}  p x = p y)"
  obtain T where "closed T" "φ T" and T: "U. closed U; φ U  ¬ (U  T)"
  proof (rule Brouwer_reduction_theorem_gen [of "{0..1}" φ])
    have *: "{x<..<y}  {0..1} = {x<..<y}" if "0  x" "y  1" "x  y" for x y::real
      using that by auto
    show "φ {0..1}"
      by (auto simp: φ_def open_segment_eq_real_ivl *)
    show "φ ((F ` UNIV))"
      if "n. closed (F n)" and φ: "n. φ (F n)" and Fsub: "n. F (Suc n)  F n" for F
    proof -
      have F01: "n. F n  {0..1}  0  F n  1  F n"
        and peq: "n x y. x  F n; y  F n; open_segment x y  F n = {}  p x = p y"
        by (metis φ φ_def)+
      have pqF: False if "u. x  F u" "x. y  F x" "open_segment x y  (x. F x) = {}" and neg: "p x  p y"
        for x y
        using that
      proof (induction x y rule: linorder_class.linorder_less_wlog)
        case (less x y)
        have xy: "x  {0..1}" "y  {0..1}"
          by (metis less.prems subsetCE F01)+
        have "norm(p x - p y) / 2 > 0"
          using less by auto
        then obtain e where "e > 0"
          and e: "u v. u  {0..1}; v  {0..1}; dist v u < e  dist (p v) (p u) < norm(p x - p y) / 2"
          by (metis uniformly_continuous_onE [OF ucont_p])
        have minxy: "min e (y - x)  < (y - x) * (3 / 2)"
          by (subst min_less_iff_disj) (simp add: less)
        define w where "w  x + (min e (y - x) / 3)" 
        define z where "z y - (min e (y - x) / 3)"
        have "w < z" and w: "w  {x<..<y}" and z: "z  {x<..<y}"
          and wxe: "norm(w - x) < e" and zye: "norm(z - y) < e"
          using minxy 0 < e less unfolding w_def z_def by auto
        have Fclo: "T. T  range F  closed T"
          by (metis n. closed (F n) image_iff)
        have eq: "{w..z}  (F ` UNIV) = {}"
          using less w z by (simp add: open_segment_eq_real_ivl disjoint_iff)
        then obtain K where "finite K" and K: "{w..z}  ( (F ` K)) = {}"
          by (metis finite_subset_image compact_imp_fip [OF compact_interval Fclo])
        then have "K  {}"
          using w < z {w..z}  (F ` K) = {} by auto
        define n where "n  Max K"
        have "n  K" unfolding n_def by (metis K  {} finite K Max_in)
        have "F n   (F ` K)"
          unfolding n_def by (metis Fsub Max_ge K  {} finite K cINF_greatest lift_Suc_antimono_le)
        with K have wzF_null: "{w..z}  F n = {}"
          by (metis disjoint_iff_not_equal subset_eq)
        obtain u where u: "u  F n" "u  {x..w}" "({u..w} - {u})  F n = {}"
        proof (cases "w  F n")
          case True
          then show ?thesis
            by (metis wzF_null w < z atLeastAtMost_iff disjoint_iff_not_equal less_eq_real_def)
        next
          case False
          obtain u where "u  F n" "u  {x..w}" "{u<..<w}  F n = {}"
          proof (rule segment_to_point_exists [of "F n  {x..w}" w])
            show "closed (F n  {x..w})"
              by (metis n. closed (F n) closed_Int closed_real_atLeastAtMost)
            show "F n  {x..w}  {}"
              by (metis atLeastAtMost_iff disjoint_iff_not_equal greaterThanLessThan_iff less.prems(1) less_eq_real_def w)
          qed (auto simp: open_segment_eq_real_ivl intro!: that)
          with False show thesis
            by (auto simp add: disjoint_iff less_eq_real_def intro!: that)
        qed
        obtain v where v: "v  F n" "v  {z..y}" "({z..v} - {v})  F n = {}"
        proof (cases "z  F n")
          case True
          have "z  {w..z}"
            using w < z by auto
          then show ?thesis
            by (metis wzF_null Int_iff True empty_iff)
        next
          case False
          show ?thesis
          proof (rule segment_to_point_exists [of "F n  {z..y}" z])
            show "closed (F n  {z..y})"
              by (metis n. closed (F n) closed_Int closed_atLeastAtMost)
            show "F n  {z..y}  {}"
              by (metis atLeastAtMost_iff disjoint_iff_not_equal greaterThanLessThan_iff less.prems(2) less_eq_real_def z)
            show "b. b  F n  {z..y}; open_segment z b  (F n  {z..y}) = {}  thesis"
            proof
              show "b. b  F n  {z..y}; open_segment z b  (F n  {z..y}) = {}  ({z..b} - {b})  F n = {}"
                using False by (auto simp: open_segment_eq_real_ivl less_eq_real_def)
            qed auto
          qed
        qed
        obtain u v where "u  {0..1}" "v  {0..1}" "norm(u - x) < e" "norm(v - y) < e" "p u = p v"
        proof
          show "u  {0..1}" "v  {0..1}"
            by (metis F01 u  F n v  F n subsetD)+
          show "norm(u - x) < e" "norm (v - y) < e"
            using u  {x..w} v  {z..y} atLeastAtMost_iff real_norm_def wxe zye by auto
          show "p u = p v"
          proof (rule peq)
            show "u  F n" "v  F n"
              by (auto simp: u v)
            have "False" if "ξ  F n" "u < ξ" "ξ < v" for ξ
            proof -
              have "ξ  {z..v}"
                by (metis DiffI disjoint_iff_not_equal less_irrefl singletonD that(1,3) v(3))
              moreover have "ξ  {w..z}  F n"
                by (metis equals0D wzF_null)
              ultimately have "ξ  {u..w}"
                using that by auto
              then show ?thesis
                by (metis DiffI disjoint_iff_not_equal less_eq_real_def not_le singletonD that(1,2) u(3))
            qed
            moreover
            have "ξ  F n; v < ξ; ξ < u  False" for ξ
              using u  {x..w} v  {z..y} w < z by simp
            ultimately
            show "open_segment u v  F n = {}"
              by (force simp: open_segment_eq_real_ivl)
          qed
        qed
        then show ?case
          using e [of x u] e [of y v] xy
          by (metis dist_norm dist_triangle_half_r order_less_irrefl)
      qed (auto simp: open_segment_commute)
      show ?thesis
        unfolding φ_def by (metis (no_types, opaque_lifting) INT_I Inf_lower2 rangeI that(3) F01 subsetCE pqF)
    qed
    show "closed {0..1::real}" by auto
  qed (meson φ_def)
  then have "T  {0..1}" "0  T" "1  T"
    and peq: "x y. x  T; y  T; open_segment x y  T = {}  p x = p y"
    unfolding φ_def by metis+
  then have "T  {}" by auto
  define h where "h  λx. p(SOME y. y  T  open_segment x y  T = {})"
  have "p y = p z" if "y  T" "z  T" and xyT: "open_segment x y  T = {}" and xzT: "open_segment x z  T = {}"
    for x y z
  proof (cases "x  T")
    case True
    with that show ?thesis by (metis φ T φ_def)
  next
    case False
    have "insert x (open_segment x y  open_segment x z)  T = {}"
      by (metis False Int_Un_distrib2 Int_insert_left Un_empty_right xyT xzT)
    moreover have "open_segment y z  T  insert x (open_segment x y  open_segment x z)  T"
      by (auto simp: open_segment_eq_real_ivl)
    ultimately have "open_segment y z  T = {}"
      by blast
    with that peq show ?thesis by metis
  qed
  then have h_eq_p_gen: "h x = p y" if "y  T" "open_segment x y  T = {}" for x y
    using that unfolding h_def
    by (metis (mono_tags, lifting) some_eq_ex)
  then have h_eq_p: "x. x  T  h x = p x"
    by simp
  have disjoint: "x. y. y  T  open_segment x y  T = {}"
    by (meson T  {} closed T segment_to_point_exists)
  have heq: "h x = h x'" if "open_segment x x'  T = {}" for x x'
  proof (cases "x  T  x'  T")
    case True
    then show ?thesis
      by (metis h_eq_p h_eq_p_gen open_segment_commute that)
  next
    case False
    obtain y y' where "y  T" "open_segment x y  T = {}" "h x = p y"
      "y'  T" "open_segment x' y'  T = {}" "h x' = p y'"
      by (meson disjoint h_eq_p_gen)
    moreover have "open_segment y y'  (insert x (insert x' (open_segment x y  open_segment x' y'  open_segment x x')))"
      by (auto simp: open_segment_eq_real_ivl)
    ultimately show ?thesis
      using False that by (fastforce simp add: h_eq_p intro!: peq)
  qed
  have "h ` {0..1} homeomorphic {0..1::real}"
  proof (rule homeomorphic_monotone_image_interval)
    show "continuous_on {0..1} h"
    proof (clarsimp simp add: continuous_on_iff)
      fix u ε::real
      assume "0 < ε" "0  u" "u  1"
      then obtain δ where "δ > 0" and δ: "v. v  {0..1}  dist v u < δ  dist (p v) (p u) < ε / 2"
        using ucont_p [unfolded uniformly_continuous_on_def]
        by (metis atLeastAtMost_iff half_gt_zero_iff)
      then have "dist (h v) (h u) < ε" if "v  {0..1}" "dist v u < δ" for v
      proof (cases "open_segment u v  T = {}")
        case True
        then show ?thesis
          using 0 < ε heq by auto
      next
        case False
        have uvT: "closed (closed_segment u v  T)" "closed_segment u v  T  {}"
          using False open_closed_segment by (auto simp: closed T closed_Int)
        obtain w where "w  T" and w: "w  closed_segment u v" "open_segment u w  T = {}"
        proof (rule segment_to_point_exists [OF uvT])
          fix b
          assume "b  closed_segment u v  T" "open_segment u b  (closed_segment u v  T) = {}"
          then show thesis
            by (metis IntD1 IntD2 ends_in_segment(1) inf.orderE inf_assoc subset_oc_segment that)
        qed
        then have puw: "dist (p u) (p w) < ε / 2"
          by (metis (no_types) T  {0..1} dist v u < δ δ dist_commute dist_in_closed_segment le_less_trans subsetCE)
        obtain z where "z  T" and z: "z  closed_segment u v" "open_segment v z  T = {}"
        proof (rule segment_to_point_exists [OF uvT])
          fix b
          assume "b  closed_segment u v  T" "open_segment v b  (closed_segment u v  T) = {}"
          then show thesis
            by (metis IntD1 IntD2 ends_in_segment(2) inf.orderE inf_assoc subset_oc_segment that)
        qed
        then have "dist (p u) (p z) < ε / 2"
          by (metis T  {0..1} dist v u < δ δ dist_commute dist_in_closed_segment le_less_trans subsetCE)
        then show ?thesis
          using puw by (metis (no_types) w  T z  T dist_commute dist_triangle_half_l h_eq_p_gen w(2) z(2))
      qed
      with 0 < δ show "δ>0. v{0..1}. dist v u < δ  dist (h v) (h u) < ε" by blast
    qed
    show "connected ({0..1}  h -` {z})" for z
    proof (clarsimp simp add: connected_iff_connected_component)
      fix u v
      assume huv_eq: "h v = h u" and uv: "0  u" "u  1" "0  v" "v  1"
      have "T. connected T  T  {0..1}  T  h -` {h u}  u  T  v  T"
      proof (intro exI conjI)
        show "connected (closed_segment u v)"
          by simp
        show "closed_segment u v  {0..1}"
          by (simp add: uv closed_segment_eq_real_ivl)
        have pxy: "p x = p y"
          if "T  {0..1}" "0  T" "1  T" "x  T" "y  T"
          and disjT: "open_segment x y  (T - open_segment u v) = {}"
          and xynot: "x  open_segment u v" "y  open_segment u v"
          for x y
        proof (cases "open_segment x y  open_segment u v = {}")
          case True
          then show ?thesis
            by (metis Diff_Int_distrib Diff_empty peq disjT x  T y  T)
        next
          case False
          then have "open_segment x u  open_segment y v  open_segment x y - open_segment u v 
                     open_segment y u  open_segment x v  open_segment x y - open_segment u v" (is "?xuyv  ?yuxv")
            using xynot by (fastforce simp add: open_segment_eq_real_ivl not_le not_less split: if_split_asm)
          then show "p x = p y"
          proof
            assume "?xuyv"
            then have "open_segment x u  T = {}" "open_segment y v  T = {}"
              using disjT by auto
            then have "h x = h y"
              using heq huv_eq by auto
            then show ?thesis
              using h_eq_p x  T y  T by auto
          next
            assume "?yuxv"
            then have "open_segment y u  T = {}" "open_segment x v  T = {}"
              using disjT by auto
            then have "h x = h y"
              using heq [of y u]  heq [of x v] huv_eq by auto
            then show ?thesis
              using h_eq_p x  T y  T by auto
          qed
        qed
        have "¬ T - open_segment u v  T"
        proof (rule T)
          show "closed (T - open_segment u v)"
            by (simp add: closed_Diff [OF closed T] open_segment_eq_real_ivl)
          have "0  open_segment u v" "1  open_segment u v"
            using open_segment_eq_real_ivl uv by auto
          then show "φ (T - open_segment u v)"
            using T  {0..1} 0  T 1  T
            by (auto simp: φ_def) (meson peq pxy)
        qed
        then have "open_segment u v  T = {}"
          by blast
        then show "closed_segment u v  h -` {h u}"
          by (force intro: heq simp: open_segment_eq_real_ivl closed_segment_eq_real_ivl split: if_split_asm)+
      qed auto
      then show "connected_component ({0..1}  h -` {h u}) u v"
        by (simp add: connected_component_def)
    qed
    show "h 1  h 0"
      by (metis φ T φ_def a a  b b h_eq_p pathfinish_def pathstart_def)
  qed
  then obtain f and g :: "real  'a"
    where gfeq: "(xh ` {0..1}. (g(f x) = x))" and fhim: "f ` h ` {0..1} = {0..1}" and contf: "continuous_on (h ` {0..1}) f"
      and fgeq: "(y{0..1}. (f(g y) = y))" and pag: "path_image g = h ` {0..1}" and contg: "continuous_on {0..1} g"
    by (auto simp: homeomorphic_def homeomorphism_def path_image_def)
  then have "arc g"
    by (metis arc_def path_def inj_on_def)
  obtain u v where "u  {0..1}" "a = g u" "v  {0..1}" "b = g v"
    by (metis (mono_tags, opaque_lifting) φ T φ_def a b fhim gfeq h_eq_p imageI path_image_def pathfinish_def pathfinish_in_path_image pathstart_def pathstart_in_path_image)
  then have "a  path_image g" "b  path_image g"
    using path_image_def by blast+
  have ph: "path_image h  path_image p"
    by (metis image_mono image_subset_iff path_image_def disjoint h_eq_p_gen T  {0..1})
  show ?thesis
  proof
    show "pathstart (subpath u v g) = a" "pathfinish (subpath u v g) = b"
      by (simp_all add: a = g u b = g v)
    show "path_image (subpath u v g)  path_image p"
      by (metis u  {0..1} v  {0..1} order_trans pag path_image_def path_image_subpath_subset ph)
    show "arc (subpath u v g)"
      using arc g a = g u b = g v u  {0..1} v  {0..1} arc_subpath_arc a  b by blast
  qed
qed


corollary path_connected_arcwise:
  fixes S :: "'a::{complete_space,real_normed_vector} set"
  shows "path_connected S 
         (x  S. y  S. x  y  (g. arc g  path_image g  S  pathstart g = x  pathfinish g = y))"
        (is "?lhs = ?rhs")
proof (intro iffI impI ballI)
  fix x y
  assume "path_connected S" "x  S" "y  S" "x  y"
  then obtain p where p: "path p" "path_image p  S" "pathstart p = x" "pathfinish p = y"
    by (force simp: path_connected_def)
  then show "g. arc g  path_image g  S  pathstart g = x  pathfinish g = y"
    by (metis x  y order_trans path_contains_arc)
next
  assume R [rule_format]: ?rhs
  show ?lhs
    unfolding path_connected_def
  proof (intro ballI)
    fix x y
    assume "x  S" "y  S"
    show "g. path g  path_image g  S  pathstart g = x  pathfinish g = y"
    proof (cases "x = y")
      case True with x  S path_component_def path_component_refl show ?thesis
        by blast
    next
      case False with R [OF x  S y  S] show ?thesis
        by (auto intro: arc_imp_path)
    qed
  qed
qed


corollary arc_connected_trans:
  fixes g :: "real  'a::{complete_space,real_normed_vector}"
  assumes "arc g" "arc h" "pathfinish g = pathstart h" "pathstart g  pathfinish h"
  obtains i where "arc i" "path_image i  path_image g  path_image h"
                  "pathstart i = pathstart g" "pathfinish i = pathfinish h"
  by (metis (no_types, opaque_lifting) arc_imp_path assms path_contains_arc path_image_join path_join pathfinish_join pathstart_join)




subsection‹Accessibility of frontier points›

lemma dense_accessible_frontier_points:
  fixes S :: "'a::{complete_space,real_normed_vector} set"
  assumes "open S" and opeSV: "openin (top_of_set (frontier S)) V" and "V  {}"
  obtains g where "arc g" "g ` {0..<1}  S" "pathstart g  S" "pathfinish g  V"
proof -
  obtain z where "z  V"
    using V  {} by auto
  then obtain r where "r > 0" and r: "ball z r  frontier S  V"
    by (metis openin_contains_ball opeSV)
  then have "z  frontier S"
    using z  V opeSV openin_contains_ball by blast
  then have "z  closure S" "z  S"
    by (simp_all add: frontier_def assms interior_open)
  with r > 0 have "infinite (S  ball z r)"
    by (auto simp: closure_def islimpt_eq_infinite_ball)
  then obtain y where "y  S" and y: "y  ball z r"
    using infinite_imp_nonempty by force
  then have "y  frontier S"
    by (meson open S disjoint_iff_not_equal frontier_disjoint_eq)
  have "y  z"
    using y  S z  S by blast
  have "path_connected(ball z r)"
    by (simp add: convex_imp_path_connected)
  with y r > 0  obtain g where "arc g" and pig: "path_image g  ball z r"
                                 and g: "pathstart g = y" "pathfinish g = z"
    using y  z by (force simp: path_connected_arcwise)
  have "continuous_on {0..1} g"
    using arc g arc_imp_path path_def by blast
  then have "compact (g -` frontier S  {0..1})"
    by (simp add: bounded_Int closed_Diff closed_vimage_Int compact_eq_bounded_closed)
  moreover have "g -` frontier S  {0..1}  {}"
  proof -
    have "r. r  g -` frontier S  r  {0..1}"
      by (metis z  frontier S g(2) imageE path_image_def pathfinish_in_path_image vimageI2)
    then show ?thesis
      by blast
  qed
  ultimately obtain t where gt: "g t  frontier S" and "0  t" "t  1"
                and t: "u. g u  frontier S; 0  u; u  1  t  u"
    by (force simp: dest!: compact_attains_inf)
  moreover have "t  0"
    by (metis y  frontier S g(1) gt pathstart_def)
  ultimately have  t01: "0 < t" "t  1"
    by auto
  have "V  frontier S"
    using opeSV openin_contains_ball by blast
  show ?thesis
  proof
    show "arc (subpath 0 t g)"
      by (simp add: 0  t t  1 arc g t  0 arc_subpath_arc)
    have "g 0  S"
      by (metis y  S g(1) pathstart_def)
    then show "pathstart (subpath 0 t g)  S"
      by auto
    have "g t  V"
      by (metis IntI atLeastAtMost_iff gt image_eqI path_image_def pig r subsetCE 0  t t  1)
    then show "pathfinish (subpath 0 t g)  V"
      by auto
    then have "inj_on (subpath 0 t g) {0..1}"
      using t01 arc (subpath 0 t g) arc_imp_inj_on by blast
    then have "subpath 0 t g ` {0..<1}  subpath 0 t g ` {0..1} - {subpath 0 t g 1}"
      by (force simp: dest: inj_onD)
    moreover have False if "subpath 0 t g ` ({0..<1}) - S  {}"
    proof -
      have contg: "continuous_on {0..1} g"
        using arc g by (auto simp: arc_def path_def)
      have "subpath 0 t g ` {0..<1}  frontier S  {}"
      proof (rule connected_Int_frontier [OF _ _ that])
        show "connected (subpath 0 t g ` {0..<1})"
        proof (rule connected_continuous_image)
          show "continuous_on {0..<1} (subpath 0 t g)"
            by (meson arc (subpath 0 t g) arc_def atLeastLessThan_subseteq_atLeastAtMost_iff continuous_on_subset order_refl path_def)
        qed auto
        show "subpath 0 t g ` {0..<1}  S  {}"
          using y  S g(1) by (force simp: subpath_def image_def pathstart_def)
      qed
      then obtain x where "x  subpath 0 t g ` {0..<1}" "x  frontier S"
        by blast
      with t01 0  t mult_le_one t show False
        by (fastforce simp: subpath_def)
    qed
    then have "subpath 0 t g ` {0..1} - {subpath 0 t g 1}  S"
      using subsetD by fastforce
    ultimately  show "subpath 0 t g ` {0..<1}  S"
      by auto
  qed
qed


lemma dense_accessible_frontier_points_connected:
  fixes S :: "'a::{complete_space,real_normed_vector} set"
  assumes "open S" "connected S" "x  S" "V  {}"
      and ope: "openin (top_of_set (frontier S)) V"
  obtains g where "arc g" "g ` {0..<1}  S" "pathstart g = x" "pathfinish g  V"
proof -
  have "V  frontier S"
    using ope openin_imp_subset by blast
  with open S x  S have "x  V"
    using interior_open by (auto simp: frontier_def)
  obtain g where "arc g" and g: "g ` {0..<1}  S" "pathstart g  S" "pathfinish g  V"
    by (metis dense_accessible_frontier_points [OF open S ope V  {}])
  then have "path_connected S"
    by (simp add: assms connected_open_path_connected)
  with pathstart g  S x  S have "path_component S x (pathstart g)"
    by (simp add: path_connected_component)
  then obtain f where "path f" and f: "path_image f  S" "pathstart f = x" "pathfinish f = pathstart g"
    by (auto simp: path_component_def)
  then have "path (f +++ g)"
    by (simp add: arc g arc_imp_path)
  then obtain h where "arc h"
                  and h: "path_image h  path_image (f +++ g)" "pathstart h = x" "pathfinish h = pathfinish g"
    using path_contains_arc [of "f +++ g" x "pathfinish g"] x  V pathfinish g  V f
    by (metis pathfinish_join pathstart_join)
  have "path_image h  path_image f  path_image g"
    using h(1) path_image_join_subset by auto
  then have "h ` {0..1} - {h 1}  S"
    using f g h
    apply (simp add: path_image_def pathfinish_def subset_iff image_def Bex_def)
    by (metis le_less)
  then have "h ` {0..<1}  S"
    using arc h by (force simp: arc_def dest: inj_onD)
  then show thesis
    using arc h g(3) h that by presburger
qed

lemma dense_access_fp_aux:
  fixes S :: "'a::{complete_space,real_normed_vector} set"
  assumes S: "open S" "connected S"
      and opeSU: "openin (top_of_set (frontier S)) U"
      and opeSV: "openin (top_of_set (frontier S)) V"
      and "V  {}" "¬ U  V"
  obtains g where "arc g" "pathstart g  U" "pathfinish g  V" "g ` {0<..<1}  S"
proof -
  have "S  {}"
    using opeSV V  {} by (metis frontier_empty openin_subtopology_empty)
  then obtain x where "x  S" by auto
  obtain g where "arc g" and g: "g ` {0..<1}  S" "pathstart g = x" "pathfinish g  V"
    using dense_accessible_frontier_points_connected [OF S x  S V  {} opeSV] by blast
  obtain h where "arc h" and h: "h ` {0..<1}  S" "pathstart h = x" "pathfinish h  U - {pathfinish g}"
  proof (rule dense_accessible_frontier_points_connected [OF S x  S])
    show "U - {pathfinish g}  {}"
      using pathfinish g  V ¬ U  V by blast
    show "openin (top_of_set (frontier S)) (U - {pathfinish g})"
      by (simp add: opeSU openin_delete)
  qed auto
  obtain γ where "arc γ"
             and γ: "path_image γ  path_image (reversepath h +++ g)"
                    "pathstart γ = pathfinish h" "pathfinish γ = pathfinish g"
  proof (rule path_contains_arc [of "(reversepath h +++ g)" "pathfinish h" "pathfinish g"])
    show "path (reversepath h +++ g)"
      by (simp add: arc g arc h pathstart g = x pathstart h = x arc_imp_path)
    show "pathstart (reversepath h +++ g) = pathfinish h"
         "pathfinish (reversepath h +++ g) = pathfinish g"
      by auto
    show "pathfinish h  pathfinish g"
      using pathfinish h  U - {pathfinish g} by auto
  qed auto
  show ?thesis
  proof
    show "arc γ" "pathstart γ  U" "pathfinish γ  V"
      using γ arc γ pathfinish h  U - {pathfinish g}  pathfinish g  V by auto
    have "path_image γ  path_image h  path_image g"
      by (metis γ(1) g(2) h(2) path_image_join path_image_reversepath pathfinish_reversepath)
    then have "γ ` {0..1} - {γ 0, γ 1}  S"
      using γ g h 
      apply (simp add: path_image_def pathstart_def pathfinish_def subset_iff image_def Bex_def)
      by (metis linorder_neqE_linordered_idom not_less)
    then show "γ ` {0<..<1}  S"
      using arc h arc γ
      by (metis arc_imp_simple_path path_image_def pathfinish_def pathstart_def simple_path_endless)
  qed
qed

lemma dense_accessible_frontier_point_pairs:
  fixes S :: "'a::{complete_space,real_normed_vector} set"
  assumes S: "open S" "connected S"
      and opeSU: "openin (top_of_set (frontier S)) U"
      and opeSV: "openin (top_of_set (frontier S)) V"
      and "U  {}" "V  {}" "U  V"
    obtains g where "arc g" "pathstart g  U" "pathfinish g  V" "g ` {0<..<1}  S"
proof -
  consider "¬ U  V" | "¬ V  U"
    using U  V by blast
  then show ?thesis
  proof cases
    case 1 then show ?thesis
      using assms dense_access_fp_aux [OF S opeSU opeSV] that by blast
  next
    case 2
    obtain g where "arc g" and g: "pathstart g  V" "pathfinish g  U" "g ` {0<..<1}  S"
      using assms dense_access_fp_aux [OF S opeSV opeSU] "2" by blast
    show ?thesis
    proof
      show "arc (reversepath g)"
        by (simp add: arc g arc_reversepath)
      show "pathstart (reversepath g)  U" "pathfinish (reversepath g)  V"
        using g by auto
      show "reversepath g ` {0<..<1}  S"
        using g by (auto simp: reversepath_def)
    qed
  qed
qed

end