Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Interval_Integral.thy Sprache: Isabelle

Original von: Isabelle^©

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

section \<open>Arcwise-Connected Sets\<close>

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 \<open>The Brouwer reduction theorem\<close>

theorem Brouwer_reduction_theorem_gen:
  fixes S :: "'a::euclidean_space set"
  assumes "closed S" "\ S"
      and \<phi>: "\<And>F. \<lbrakk>\<And>n. closed(F n); \<And>n. \<phi>(F n); \<And>n. F(Suc n) \<subseteq> F n\<rbrakk> \<Longrightarrow> \<phi>(\<Inter>(range F))"
  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 \<subseteq> a \<and> closed U \<and> \<phi> U \<and> U \<inter> (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 \<subseteq> A n \<and> closed U \<and> \<phi> U \<and> U \<inter> (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 \<open>\<And>n. A n \<subseteq> S\<close> by blast
    show "closed (\(A ` UNIV))"
      using clo by blast
    show "\ (\(A ` UNIV))"
      by (simp add: clo \<phi> 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 \<open>closed U\<close> \<open>x \<notin> U\<close> 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 \<open>0 < e\<close> \<open>ball x e = \<Union>(B ` K)\<close> by auto
        then obtain n where "n \ K" "x \ B n"
          by (metis K UN_E \<open>0 < e\<close> centre_in_ball)
        then have "U \ B n = {}"
          using K e by auto
        show ?thesis
        proof (cases "\U\A 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 \<open>x \<in> B n\<close> by blast
        next
          case False
          then show ?thesis
            by (meson Inf_lower Usub \<open>U \<inter> B n = {}\<close> \<open>\<phi> U\<close> \<open>closed U\<close> 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 \<phi>: "\<And>F. \<lbrakk>\<And>n. compact(F n); \<And>n. F n \<noteq> {}; \<And>n. \<phi>(F n); \<And>n. F(Suc n) \<subseteq> F n\<rbrakk> \<Longrightarrow> \<phi>(\<Inter>(range F))"
  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 \<open>compact S\<close> 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 \<phi> \<open>compact S\<close> 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)+

subsection\<^marker>\<open>tag unimportant\<close>\<open>Arcwise Connections\<close>(*FIX ME this subsection is empty(?) *)

subsection\<open>Density of points with dyadic rational coordinates\<close>

proposition closure_dyadic_rationals:
    "closure (\k. \f \ Basis \ \.
                   { \<Sum>i :: 'a :: euclidean_space \<in> Basis. (f i / 2^k) *\<^sub>R i }) = UNIV"
proof -
  have "x \ closure (\k. \f \ Basis \ \. {\i \ Basis. (f i / 2^k) *\<^sub>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 (\i\Basis. (real_of_int \2^k*(x \ i)\ / 2^k) *\<^sub>R i) x =
          dist (\<Sum>i\<in>Basis. (real_of_int \<lfloor>2^k*(x \<bullet> i)\<rfloor> / 2^k) *\<^sub>R i) (\<Sum>i\<in>Basis. (x \<bullet> i) *\<^sub>R i)"
      by (simp add: euclidean_representation)
    also have "... = norm ((\i\Basis. (real_of_int \2^k*(x \ i)\ / 2^k) *\<^sub>R i - (x \ i) *\<^sub>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) *\<^sub>R i - (x \ i) *\<^sub>R i) =
                 \<bar>real_of_int \<lfloor>x \<bullet> i*2^k\<rfloor> / 2^k - x \<bullet> i\<bar>"
        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) *\<^sub>R i - (x \ i) *\<^sub>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 (\i\Basis. (\2^k*(x \ i)\ / 2^k) *\<^sub>R i) x < e" .
    with Ints_of_int
    show "\k. \f \ Basis \ \. dist (\b\Basis. (f b / 2^k) *\<^sub>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 *\<^sub>R i }) = UNIV"
proof -
  have *: "(\k. \f \ Basis \ \. { \i::'a \ Basis. (f i / 2^k) *\<^sub>R i })
           \<subseteq> (\<Union>f \<in> Basis \<rightarrow> \<rat>. { \<Sum>i \<in> Basis. f i *\<^sub>R i })"
  proof clarsimp
    fix k and f :: "'a \ real"
    assume f: "f \ Basis \ \"
    show "\x \ Basis \ \. (\i \ Basis. (f i / 2^k) *\<^sub>R i) = (\i \ Basis. x i *\<^sub>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 \ {}\
        \<Longrightarrow> closure(S \<inter>
                    (\<Union>k. \<Union>f \<in> Basis \<rightarrow> \<int>.
                   { \<Sum>i :: 'a :: euclidean_space \<in> Basis. (f i / 2^k) *\<^sub>R i })) =
            closure S"
  by (simp add: closure_dyadic_rationals closure_convex_Int_superset)

lemma closure_rationals_in_convex_set:
   "\convex S; interior S \ {}\
    \<Longrightarrow> closure(S \<inter> (\<Union>f \<in> Basis \<rightarrow> \<rat>. { \<Sum>i :: 'a :: euclidean_space \<in> Basis. f i *\<^sub>R i })) =
        closure S"
  by (simp add: closure_rational_coordinates closure_convex_Int_superset)

text\<open> 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 \
             (\<Union>k. \<Union>f\<in>Basis \<rightarrow> \<int>. {\<Sum>i\<in>Basis. (f i / 2^k) *\<^sub>R i})"
    by force
  then show ?thesis
    using closure_dyadic_rationals_in_convex_set [OF \<open>convex S\<close> intnz] by simp
qed

definition\<^marker>\<open>tag unimportant\<close> dyadics :: "'a::field_char_0 set" where "dyadics \<equiv> \<Union>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 \<open>Suc (4 * m) = 4 * m' + 3\<close> 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 \<union> (\<Union>k m. {of_nat (4*m + 1) / 2^Suc k}) \<union> (\<Union>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

function\<^marker>\<open>tag unimportant\<close> (domintros) dyad_rec :: "[nat \<Rightarrow> 'a, 'a\<Rightarrow>'a, 'a\<Rightarrow>'a, real] \<Rightarrow> '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 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 \<open>k = K\<close> \<open>k' < k\<close> by blast
          then show "dyad_rec_dom (b, l, r, (2 * real m + 1) / 2^n)"
            using \<open>k' = n\<close> 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 \<open>k = K\<close> \<open>k' < k\<close> by blast
          then show "dyad_rec_dom (b, l, r, (2 * real m + 1) / 2^n)"
            using \<open>k' = n\<close> 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

definition\<^marker>\<open>tag unimportant\<close> dyad_rec2
    where "dyad_rec2 u v lc rc x =
             dyad_rec (\<lambda>z. (u,v)) (\<lambda>(a,b). (a, lc a b (midpoint a b))) (\<lambda>(a,b). (rc a b (midpoint a b), b)) (2*x)"

abbreviation\<^marker>\<open>tag unimportant\<close> leftrec where "leftrec u v lc rc x \<equiv> fst (dyad_rec2 u v lc rc x)"
abbreviation\<^marker>\<open>tag unimportant\<close> rightrec where "rightrec u v lc rc x \<equiv> 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)

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 \
              (\<forall>x \<in> {c..d}. f x = f m) \<and>
              (\<forall>x \<in> {a..<c}. (f x \<noteq> f m)) \<and>
              (\<forall>x \<in> {d<..b}. (f x \<noteq> f m)) \<and>
              (\<forall>x \<in> {a..<c}. \<forall>y \<in> {d<..b}. f x \<noteq> 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..
        using that m cd [THEN equalityD1, THEN subsetD] \<open>c \<le> m\<close> by force
      show "f x \ f m" if "x \ {d<..b}" for x
        using that m cd [THEN equalityD1, THEN subsetD, of x] \<open>m \<le> d\<close> by force
      show "f x \ f y" if "x \ {a.. {d<..b}" for x y
      proof (cases "f x = f m \ f y = f m")
        case True
        then show ?thesis
          using \<open>\<And>x. x \<in> {a..<c} \<Longrightarrow> f x \<noteq> f m\<close> that by auto
      next
        case False
        have False if "f x = f y"
        proof -
          have "x \ m" "m \ y"
            using \<open>c \<le> m\<close> \<open>x \<in> {a..<c}\<close>  \<open>m \<le> d\<close> \<open>y \<in> {d<..b}\<close> by auto
          then have "x \ ({0..1} \ f -` {f y})" "y \ ({0..1} \ f -` {f y})"
            using \<open>x \<in> {a..<c}\<close> \<open>y \<in> {d<..b}\<close> ab01 by (auto simp: that)
          then have "m \ ({0..1} \ f -` {f y})"
            by (meson \<open>m \<le> y\<close> \<open>x \<le> m\<close> 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 \<le> leftcut a b m \<and> leftcut a b m \<le> m \<and> m \<le> rightcut a b m \<and> rightcut a b m \<le> b \<and>
            (\<forall>x \<in> {leftcut a b m..rightcut a b m}. f x = f m) \<and>
            (\<forall>x \<in> {a..<leftcut a b m}. f x \<noteq> f m) \<and>
            (\<forall>x \<in> {rightcut a b m<..b}. f x \<noteq> f m) \<and>
            (\<forall>x \<in> {a..<leftcut a b m}. \<forall>y \<in> {rightcut a b m<..b}. f x \<noteq> 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}\
                         \<Longrightarrow> 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 \<le> m; m \<le> b; {a..b} \<subseteq> {0..1}\<rbrakk>  \<Longrightarrow> 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 \<open>leftcut 0 1 0 = 0\<close> 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.. f x \ f 1"
    using LR [of 1 u 1] u01 v_def by fastforce
  have f0v: "\x. x \ {0.. 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 \<open>n > 0\<close>
            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 \<open>n > 0\<close>
            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\
        \<Longrightarrow> (a(j / 2^n)) \<le> (c(i / 2^m)) \<and> (c(i / 2^m)) \<le> (b(j / 2^n))" for d i j m n
  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 \<open>odd j\<close> 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) \<le> b (real (4 * k + 1) / 2 ^ Suc n)"
          proof (rule less.IH [OF _ refl])
            show "m - Suc n < d"
              using \<open>n < m\<close> 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 \<open>n < m\<close> \<open>d = m - n\<close> by (auto simp: field_split_simps \<open>n < m\<close> 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 \<open>0 < n\<close>
            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) \<le> b (real (4 * k + 3) / 2 ^ Suc n)"
          proof (rule less.IH [OF _ refl])
            show "m - Suc n < d"
              using \<open>n < m\<close> 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 \<open>n < m\<close> \<open>d = m - n\<close> by (auto simp: field_split_simps  \<open>n < m\<close> 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 \<open>0 < n\<close>
            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))\<bar>
                   \<le> 2/2 ^ Suc n"
          by (simp add: c_def midpoint_def)
        with j k \<open>n > 0\<close> 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)\<bar>  \<le>  2/2 ^ Suc n"
          by (simp add: c_def midpoint_def)
        with j k \<open>n > 0\<close> 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 \<open>0 < j\<close> have "k > 0" "2 * k < 2 ^ n"
          using Suc.prems(2) k by auto
        with k \<open>0 < n\<close> Suc.IH [of k] show ?thesis
          by (simp add: m1_to_3 a41 b43 del: power_Suc) (auto simp: of_nat_diff)
      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 b41\<open>0 < n\<close> del: power_Suc)
      qed
    qed
  qed
  have f_eq_fc: "\0 < j; j < 2 ^ n\
                 \<Longrightarrow> f(b((2*j - 1) / 2 ^ (Suc n))) = f(c(j / 2^n)) \<and>
                     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 \<open>0 < j\<close> 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 \<open>0 < k\<close>
        by (simp add: less2n add.commute [of 1] m1_to_3 a41 b43 del: power_Suc) (auto simp: of_nat_diff)
    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 \<open>0 < e\<close> less_divide_eq_numeral1(1) mult_zero_left)
    obtain n where n: "1/2^n < min d 1"
      by (metis \<open>0 < d\<close> divide_less_eq_1 less_numeral_extra(1) min_def one_less_numeral_iff power_one_over real_arch_pow_inv semiring_norm(76) zero_less_numeral)
    with gr0I have "n > 0"
      by (force simp: field_split_simps)
    show "\d>0. \x\D01. \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 \<open>0 < e\<close> 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 < 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 \<open>0 < n\<close> 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 \<open>0 < j\<close> \<open>j < 2 ^ n\<close> 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 \<open>0 < j\<close> \<open>j < 2 ^ n\<close> 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 \<open>auto intro!: that\<close>)
  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 \<delta> where "\<delta> > 0"
        and \<delta>: "\<And>x x'. \<lbrakk>x \<in> {0..1}; x' \<in> {0..1}; dist x' x < \<delta>\<rbrakk> \<Longrightarrow> norm (f x' - f x) < e"
        using \<open>0 < e\<close> 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 \<open>0 \<le> x\<close> \<open>x \<le> 1\<close> by force
          then have "\y\a (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 \<open>n=0\<close> 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 \<open>n \<noteq> 0\<close> 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 \<open>n \<noteq> 0\<close> 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 \<open>n \<noteq> 0\<close> 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 \<open>0 < \<delta>\<close> divide_less_eq_1 less_numeral_extra(1) min_less_iff_conj one_less_numeral_iff power_one_over real_arch_pow_inv semiring_norm(76) zero_less_divide_iff zero_less_numeral)
      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 \<open>odd m\<close>, of n]
        by linarith+
      moreover note \<open>0 < m\<close> mless \<open>0 \<le> x\<close> \<open>x \<le> 1\<close>
      ultimately have "dist (h (real m / 2 ^ n)) (f x) < e"
        by (auto simp: dist_norm h_eq feq \<delta>)
      then show "\k. \m\{0<..<2 ^ k}. dist (h (real m / 2 ^ k)) (f x) < e"
        using \<open>0 < m\<close> 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) \
          (\<forall>x. a(j / 2^n) < x \<longrightarrow> x \<le> b(j / 2^n) \<longrightarrow> f x \<noteq> f(a(j / 2^n))) \<and>
          (\<forall>x. a(j / 2^n) \<le> x \<longrightarrow> x < b(j / 2^n) \<longrightarrow> f x \<noteq> f(b(j / 2^n)))" for n and j::nat
    proof (induction n arbitrary: j)
      case 0 then show ?case
        by (simp add: \<open>u < v\<close> 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 \<open>u < v\<close> f_not_fu f_not_fv)
      next
        case True show ?thesis
        proof (cases "even j")
          case True
          with \<open>0 < n\<close> 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 \<open>0 < n\<close> 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)
--> --------------------

--> maximum size reached

--> --------------------

¤ Dauer der Verarbeitung: 0.67 Sekunden (vorverarbeitet) ¤

Druckansicht unsichere Verbindung
Druckansicht sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.