# 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"
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 "∃U⊆A n. closed U ∧ φ U ∧ U ∩ B n = {}")
case True
then show ?thesis
apply (rule_tac x="Suc n" in exI)
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"
qed (meson assms compact_imp_closed seq_compact_closed_subset seq_compact_eq_compact)+

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

subsection‹Density of points with dyadic rational coordinates›

"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 (∑i∈Basis. (real_of_int ⌊2^k*(x ∙ i)⌋ / 2^k) *⇩R i) x =
dist (∑i∈Basis. (real_of_int ⌊2^k*(x ∙ i)⌋ / 2^k) *⇩R i) (∑i∈Basis. (x ∙ i) *⇩R i)"
also have "... = norm ((∑i∈Basis. (real_of_int ⌊2^k*(x ∙ i)⌋ / 2^k) *⇩R i - (x ∙ i) *⇩R i))"
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¦"
also have "... ≤ (1/2) ^ k"
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 (∑i∈Basis. (⌊2^k*(x ∙ i)⌋ / 2^k) *⇩R i) x < e" .
with Ints_of_int
show "∃k. ∃f ∈ Basis → ℤ. dist (∑b∈Basis. (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

"⟦convex S; interior S ≠ {}⟧
⟹ closure(S ∩
(⋃k. ⋃f ∈ Basis → ℤ.
{ ∑i :: 'a :: euclidean_space ∈ Basis. (f i / 2^k) *⇩R i })) =
closure S"

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"

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".›

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. ⋃f∈Basis → ℤ. {∑i∈Basis. (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

definition✐‹tag unimportant› dyadics :: "'a::field_char_0 set" where "dyadics ≡ ⋃k m. {of_nat m / 2^k}"

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)"
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)"
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
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

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"
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

Nats ∪ (⋃k m. {of_nat (4*m + 1) / 2^Suc k}) ∪ (⋃k m. {of_nat (4*m + 3) / 2^Suc k})"
(is "_ = ?rhs")
proof
apply clarify
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'"
qed

function✐‹tag 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]
by (fastforce simp:  field_simps)+

lemma dyadics_levels: "dyadics = (⋃K. ⋃k<K. ⋃ m. {of_nat m / 2^k})"

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')"
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
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')"
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
qed
qed
next
assume "k < K"
then show ?case
using Suc.IH by blast
qed
qed

lemma dyad_rec_of_nat [simp]: "dyad_rec b l r (real m) = b m"

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))"
show "dyad_rec_dom (b, l, r, (4 * real m + 1) / 2 ^ Suc n)"
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))"
show "dyad_rec_dom (b, l, r, (4 * real m + 3) / 2 ^ Suc n)"
qed

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'))"
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))"
finally show ?thesis .
qed

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))"
finally show ?thesis .
qed

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)"

abbreviation✐‹tag unimportant› leftrec where "leftrec u v lc rc x ≡ fst (dyad_rec2 u v lc rc x)"
abbreviation✐‹tag 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"

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)"

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)))"

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

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)))"

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)"

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

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

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 ¦ < ε"
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

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 ¦ < ε"
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]›

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)"
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
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"
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)"
have ycommon: "y = real(2^n1 * k2) / 2 ^ (n1+n2)"
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
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)"
qed
qed
qed
qed

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)"
moreover
have ycommon: "y = of_nat(2^m * j) / 2 ^ (m+n)"
ultimately have "x+y = (of_nat(2^n * i + 2^m * j)) / 2 ^ (m+n)"
then show ?thesis
qed

fixes x :: "'a::linordered_field"
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)"
moreover
have ycommon: "y = of_nat(2^m * j) / 2 ^ (m+n)"
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
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
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)
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›
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›