# Theory Arcwise_Connected

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

section ‹Arcwise-Connected Sets›

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

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

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

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

subsection ‹The Brouwer reduction theorem›

theorem Brouwer_reduction_theorem_gen:
fixes S :: "'a::euclidean_space set"
assumes "closed S" "φ S"
and φ: "⋀F. ⟦⋀n. closed(F n); ⋀n. φ(F n); ⋀n. F(Suc n) ⊆ F n⟧ ⟹ φ(⋂(range F))"
obtains T where "T ⊆ S" "closed T" "φ T" "⋀U. ⟦U ⊆ S; closed U; φ U⟧ ⟹ ¬ (U ⊂ T)"
proof -
obtain B :: "nat ⇒ 'a set"
where "inj B" "⋀n. open(B n)" and open_cov: "⋀S. open S ⟹ ∃K. S = ⋃(B ` K)"
by (metis Setcompr_eq_image that univ_second_countable_sequence)
define A where "A ≡ rec_nat S (λn a. if ∃U. U ⊆ a ∧ closed U ∧ φ U ∧ U ∩ (B n) = {}
then SOME U. U ⊆ a ∧ closed U ∧ φ U ∧ U ∩ (B n) = {}
else a)"
have [simp]: "A 0 = S"
by (simp add: A_def)
have ASuc: "A(Suc n) = (if ∃U. U ⊆ A n ∧ closed U ∧ φ U ∧ U ∩ (B n) = {}
then SOME U. U ⊆ A n ∧ closed U ∧ φ U ∧ U ∩ (B n) = {}
else A n)" for n
by (auto simp: A_def)
have sub: "⋀n. A(Suc n) ⊆ A n"
by (auto simp: ASuc dest!: someI_ex)
have subS: "A n ⊆ S" for n
by (induction n) (use sub in auto)
have clo: "closed (A n) ∧ φ (A n)" for n
by (induction n) (auto simp: assms ASuc dest!: someI_ex)
show ?thesis
proof
show "⋂(range A) ⊆ S"
using ‹⋀n. A n ⊆ S› by blast
show "closed (⋂(A ` UNIV))"
using clo by blast
show "φ (⋂(A ` UNIV))"
by (simp add: clo φ sub)
show "¬ U ⊂ ⋂(A ` UNIV)" if "U ⊆ S" "closed U" "φ U" for U
proof -
have "∃y. x ∉ A y" if "x ∉ U" and Usub: "U ⊆ (⋂x. A x)" for x
proof -
obtain e where "e > 0" and e: "ball x e ⊆ -U"
using ‹closed U› ‹x ∉ U› openE [of "-U"] by blast
moreover obtain K where K: "ball x e = ⋃(B ` K)"
using open_cov [of "ball x e"] by auto
ultimately have "⋃(B ` K) ⊆ -U"
by blast
have "K ≠ {}"
using ‹0 < e› ‹ball x e = ⋃(B ` K)› by auto
then obtain n where "n ∈ K" "x ∈ B n"
by (metis K UN_E ‹0 < e› centre_in_ball)
then have "U ∩ B n = {}"
using K e by auto
show ?thesis
proof (cases "∃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 ‹x ∈ B n› by blast
next
case False
then show ?thesis
by (meson Inf_lower Usub ‹U ∩ B n = {}› ‹φ U› ‹closed U› range_eqI subset_trans)
qed
qed
with that show ?thesis
by (meson Inter_iff psubsetE rangeI subsetI)
qed
qed
qed

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

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)"
by (simp add: euclidean_representation)
also have "... = norm ((∑i∈Basis. (real_of_int ⌊2^k*(x ∙ i)⌋ / 2^k) *⇩R i - (x ∙ i) *⇩R i))"
by (simp add: dist_norm sum_subtractf)
also have "... ≤ DIM('a)*((1/2)^k)"
proof (rule sum_norm_bound, simp add: algebra_simps)
fix i::'a
assume "i ∈ Basis"
then have "norm ((real_of_int ⌊x ∙ i*2^k⌋ / 2^k) *⇩R i - (x ∙ i) *⇩R i) =
¦real_of_int ⌊x ∙ i*2^k⌋ / 2^k - x ∙ i¦"
by (simp add: scaleR_left_diff_distrib [symmetric])
also have "... ≤ (1/2) ^ k"
by (simp add: divide_simps) linarith
finally show "norm ((real_of_int ⌊x ∙ i*2^k⌋ / 2^k) *⇩R i - (x ∙ i) *⇩R i) ≤ (1/2) ^ k" .
qed
also have "... < DIM('a)*(e/DIM('a))"
using DIM_positive k linordered_comm_semiring_strict_class.comm_mult_strict_left_mono of_nat_0_less_iff by blast
also have "... = e"
by simp
finally have "dist (∑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"
by (simp add: closure_rational_coordinates closure_convex_Int_superset)

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

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 real_in_dyadics [simp]: "real m ∈ dyadics"
by (simp add: dyadics_def) (metis divide_numeral_1 numeral_One power_0)

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

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

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

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

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

"(dyadics :: 'a::field_char_0 set) =
Nats ∪ (⋃k m. {of_nat (4*m + 1) / 2^Suc k}) ∪ (⋃k m. {of_nat (4*m + 3) / 2^Suc k})"
(is "_ = ?rhs")
proof
show "dyadics ⊆ ?rhs"
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✐‹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]
apply (simp_all add: nat_neq_4k1 nat_neq_4k3 neq_4k1_k43 dyadics_iff Nats_def)
by (fastforce simp:  field_simps)+

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

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
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')"
fix m n
assume "(4 * real m' + 3) / (2 * 2 ^ k') = (4 * real m + 1) / (2 * 2^n)"
then have "False"
by (metis neq_4k1_k43)
then show "dyad_rec_dom (b, l, r, (2 * real m + 1) / 2^n)" ..
next
fix m n
assume "(4 * real m' + 3) / (2 * 2 ^ k') = (4 * real m + 3) / (2 * 2^n)"
then have "m' = m" "k' = n" using iff_4k [of _ 3]
by auto
have "dyad_rec_dom (b, l, r, real (2 * m + 1) / 2 ^ k')"
using Suc.IH ‹k = K› ‹k' < k› by blast
then show "dyad_rec_dom (b, l, r, (2 * real m + 1) / 2^n)"
using ‹k' = n› by (auto simp: algebra_simps)
qed
then show ?case by (simp add: eq add_ac)
qed
qed
next
assume "k < K"
then show ?case
using Suc.IH by blast
qed
qed

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

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))"
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))"
by (simp add: 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)"
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)))"
by (simp add: case_prod_beta)

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)))"
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)"
by (simp add: case_prod_beta)

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

assumes "x ∈ dyadics" "y ∈ dyadics"
shows "x+y ∈ dyadics"
proof -
obtain i j m n where x: "x = of_nat i / 2 ^ m" and y: "y = of_nat j / 2 ^ n"
using assms by (auto simp: dyadics_def)
have xcommon: "x = of_nat(2^n * i) / 2 ^ (m+n)"
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: field_simps)
then show ?thesis
unfolding dyadics_def by blast
qed

fixes x :: "'a::linordered_field"
assumes "x ∈ dyadics" "y ∈ dyadics" "y ≤ x"
shows "x-y ∈ dyadics"
proof -
obtain i j m n where x: "x = of_nat i / 2 ^ m" and y: "y = of_nat j / 2 ^ n"
using assms by (auto simp: dyadics_def)
have j_le_i: "j * 2 ^ m ≤ i * 2 ^ n"
using of_nat_le_iff ‹y ≤ x› unfolding x y by (fastforce simp add: divide_simps)
have xcommon: "x = of_nat(2^n * i) / 2 ^ (m+n)"
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
unfolding dyadics_def by blast
qed

theorem homeomorphic_monotone_image_interval:
fixes f :: "real ⇒ 'a::{real_normed_vector,complete_space}"
assumes cont_f: "continuous_on {0..1} f"
and conn: "⋀y. connected ({0..1} ∩ f -` {y})"
and f_1not0: "f 1 ≠ f 0"
shows "(f ` {0..1}) homeomorphic {0..1::real}"
proof -
have "∃c d. a ≤ c ∧ c ≤ m ∧ m ≤ d ∧ d ≤ b ∧
(∀x ∈ {c..d}. f x = f m) ∧
(∀x ∈ {a..<c}. (f x ≠ f m)) ∧
(∀x ∈ {d<..b}. (f x ≠ f m)) ∧
(∀x ∈ {a..<c}. ∀y ∈ {d<..b}. f x ≠ f y)"
if m: "m ∈ {a..b}" and ab01: "{a..b} ⊆ {0..1}" for a b m
proof -
have comp: "compact (f -` {f m} ∩ {0..1})"
by (simp add: compact_eq_bounded_closed bounded_Int closed_vimage_Int cont_f)
obtain c0 d0 where cd0: "{0..1} ∩ f -` {f m} = {c0..d0}"
using connected_compact_interval_1 [of "{0..1} ∩ f -` {f m}"] conn comp
by (metis Int_commute)
with that have "m ∈ cbox c0 d0"
by auto
obtain c d where cd: "{a..b} ∩ f -` {f m} = {c..d}"
using ab01 cd0
by (rule_tac c="max a c0" and d="min b d0" in that) auto
then have cdab: "{c..d} ⊆ {a..b}"
by blast
show ?thesis
proof (intro exI conjI ballI)
show "a ≤ c" "d ≤ b"
using cdab cd m by auto
show "c ≤ m" "m ≤ d"
using cd m by auto
show "⋀x. x ∈ {c..d} ⟹ f x = f m"
using cd by blast
show "f x ≠ f m" if "x ∈ {a..<c}" for x
using that m cd [THEN equalityD1, THEN subsetD] ‹c ≤ m› by force
show "f x ≠ f m" if "x ∈ {d<..b}" for x
using that m cd [THEN equalityD1, THEN subsetD, of x] ‹m ≤ d› by force
show "f x ≠ f y" if "x ∈ {a..<c}" "y ∈ {d<..b}" for x y
proof (cases "f x = f m ∨ f y = f m")
case True
then show ?thesis
using ‹⋀x. x ∈ {a..<c} ⟹ f x ≠ f m› that by auto
next
case False
have False if "f x = f y"
proof -
have "x ≤ m" "m ≤ y"
using ‹c ≤ m› ‹x ∈ {a..<c}›  ‹m ≤ d› ‹y ∈ {d<..b}› by auto
then have "x ∈ ({0..1} ∩ f -` {f y})" "y ∈ ({0..1} ∩ f -` {f y})"
using ‹x ∈ {a..<c}› ‹y ∈ {d<..b}› ab01 by (auto simp: that)
then have "m ∈ ({0..1} ∩ f -` {f y})"
by (meson ‹m ≤ y› ‹x ≤ m› is_interval_connected_1 conn [of "f y"] is_interval_1)
with False show False by auto
qed
then show ?thesis by auto
qed
qed
qed
then obtain leftcut rightcut where LR:
"⋀a b m. ⟦m ∈ {a..b}; {a..b} ⊆ {0..1}⟧ ⟹
(a ≤ leftcut a b m ∧ leftcut a b m ≤ m ∧ m ≤ rightcut a b m ∧ rightcut a b m ≤ b ∧
(∀x ∈ {leftcut a b m..rightcut a b m}. f x = f m) ∧
(∀x ∈ {a..<leftcut a b m}. f x ≠ f m) ∧
(∀x ∈ {rightcut a b m<..b}. f x ≠ f m) ∧
(∀x ∈ {a..<leftcut a b m}. ∀y ∈ {rightcut a b m<..b}. f x ≠ f y))"
apply atomize
apply (clarsimp simp only: imp_conjL [symmetric] choice_iff choice_iff')
apply (rule that, blast)
done
then have left_right: "⋀a b m. ⟦m ∈ {a..b}; {a..b} ⊆ {0..1}⟧ ⟹ a ≤ leftcut a b m ∧ rightcut a b m ≤ b"
and  left_right_m: "⋀a b m. ⟦m ∈ {a..b}; {a..b} ⊆ {0..1}⟧ ⟹ leftcut a b m ≤ m ∧ m ≤ rightcut a b m"
by auto
have left_neq: "⟦a ≤ x; x < leftcut a b m; a ≤ m; m ≤ b; {a..b} ⊆ {0..1}⟧ ⟹ f x ≠ f m"
and right_neq: "⟦rightcut a b m < x; x ≤ b; a ≤ m; m ≤ b; {a..b} ⊆ {0..1}⟧ ⟹ f x ≠ f m"
and left_right_neq: "⟦a ≤ x; x < leftcut a b m; rightcut a b m < y; y ≤ b; a ≤ m; m ≤ b; {a..b} ⊆ {0..1}⟧ ⟹ f x ≠ f m"
and feqm: "⟦leftcut a b m ≤ x; x ≤ rightcut a b m; a ≤ m; m ≤ b; {a..b} ⊆ {0..1}⟧
⟹ f x = f m" for a b m x y
by (meson atLeastAtMost_iff greaterThanAtMost_iff atLeastLessThan_iff LR)+
have f_eqI: "⋀a b m x y. ⟦leftcut a b m ≤ x; x ≤ rightcut a b m; leftcut a b m ≤ y; y ≤ rightcut a b m;
a ≤ m; m ≤ b; {a..b} ⊆ {0..1}⟧  ⟹ f x = f y"
by (metis feqm)
define u where "u ≡ rightcut 0 1 0"
have lc[simp]: "leftcut 0 1 0 = 0" and u01: "0 ≤ u" "u ≤ 1"
using LR [of 0 0 1] by (auto simp: u_def)
have f0u: "⋀x. x ∈ {0..u} ⟹ f x = f 0"
using LR [of 0 0 1] unfolding u_def [symmetric]
by (metis ‹leftcut 0 1 0 = 0› atLeastAtMost_iff order_refl zero_le_one)
have fu1: "⋀x. x ∈ {u<..1} ⟹ f x ≠ f 0"
using LR [of 0 0 1] unfolding u_def [symmetric] by fastforce
define v where "v ≡ leftcut u 1 1"
have rc[simp]: "rightcut u 1 1 = 1" and v01: "u ≤ v" "v ≤ 1"
using LR [of 1 u 1] u01  by (auto simp: v_def)
have fuv: "⋀x. x ∈ {u..<v} ⟹ f x ≠ f 1"
using LR [of 1 u 1] u01 v_def by fastforce
have f0v: "⋀x. x ∈ {0..<v} ⟹ f x ≠ f 1"
by (metis f_1not0 atLeastAtMost_iff atLeastLessThan_iff f0u fuv linear)
have fv1: "⋀x. x ∈ {v..1} ⟹ f x = f 1"
using LR [of 1 u 1] u01 v_def by (metis atLeastAtMost_iff atLeastatMost_subset_iff order_refl rc)
define a where "a ≡ leftrec u v leftcut rightcut"
define b where "b ≡ rightrec u v leftcut rightcut"
define c where "c ≡ λx. midpoint (a x) (b x)"
have a_real [simp]: "a (real j) = u" for j
using a_def leftrec_base
by (metis nonzero_mult_div_cancel_right of_nat_mult of_nat_numeral zero_neq_numeral)
have b_real [simp]: "b (real j) = v" for j
using b_def rightrec_base
by (metis nonzero_mult_div_cancel_right of_nat_mult of_nat_numeral zero_neq_numeral)
have a41: "a ((4 * real m + 1) / 2^Suc n) = a ((2 * real m + 1) / 2^n)" if "n > 0" for m n
using that a_def leftrec_41 by blast
have b41: "b ((4 * real m + 1) / 2^Suc n) =
leftcut (a ((2 * real m + 1) / 2^n))
(b ((2 * real m + 1) / 2^n))
(c ((2 * real m + 1) / 2^n))" if "n > 0" for m n
using that a_def b_def c_def rightrec_41 by blast
have a43: "a ((4 * real m + 3) / 2^Suc n) =
rightcut (a ((2 * real m + 1) / 2^n))
(b ((2 * real m + 1) / 2^n))
(c ((2 * real m + 1) / 2^n))" if "n > 0" for m n
using that a_def b_def c_def leftrec_43 by blast
have b43: "b ((4 * real m + 3) / 2^Suc n) = b ((2 * real m + 1) / 2^n)" if "n > 0" for m n
using that b_def rightrec_43 by blast
have uabv: "u ≤ a (real m / 2 ^ n) ∧ a (real m / 2 ^ n) ≤ b (real m / 2 ^ n) ∧ b (real m / 2 ^ n) ≤ v" for m n
proof (induction n arbitrary: m)
case 0
then show ?case by (simp add: v01)
next
case (Suc n p)
show ?case
proof (cases "even p")
case True
then obtain m where "p = 2*m" by (metis evenE)
then show ?thesis
by (simp add: Suc.IH)
next
case False
then obtain m where m: "p = 2*m + 1" by (metis oddE)
show ?thesis
proof (cases n)
case 0
then show ?thesis
by (simp add: a_def b_def leftrec_base rightrec_base v01)
next
case (Suc n')
then have "n > 0" by simp
have a_le_c: "a (real m / 2^n) ≤ c (real m / 2^n)" for m
unfolding c_def by (metis Suc.IH ge_midpoint_1)
have c_le_b: "c (real m / 2^n) ≤ b (real m / 2^n)" for m
unfolding c_def by (metis Suc.IH le_midpoint_1)
have c_ge_u: "c (real m / 2^n) ≥ u" for m
using Suc.IH a_le_c order_trans by blast
have c_le_v: "c (real m / 2^n) ≤ v" for m
using Suc.IH c_le_b order_trans by blast
have a_ge_0: "0 ≤ a (real m / 2^n)" for m
using Suc.IH order_trans u01(1) by blast
have b_le_1: "b (real m / 2^n) ≤ 1" for m
using Suc.IH order_trans v01(2) by blast
have left_le: "leftcut (a ((real m) / 2^n)) (b ((real m) / 2^n)) (c ((real m) / 2^n)) ≤ c ((real m) / 2^n)" for m
by (simp add: LR a_ge_0 a_le_c b_le_1 c_le_b)
have right_ge: "rightcut (a ((real m) / 2^n)) (b ((real m) / 2^n)) (c ((real m) / 2^n)) ≥ c ((real m) / 2^n)" for m
by (simp add: LR a_ge_0 a_le_c b_le_1 c_le_b)
show ?thesis
proof (cases "even m")
case True
then obtain r where r: "m = 2*r" by (metis evenE)
show ?thesis
using order_trans [OF left_le c_le_v, of "1+2*r"] Suc.IH [of "m+1"]
using a_le_c [of "m+1"] c_le_b [of "m+1"] a_ge_0 [of "m+1"] b_le_1 [of "m+1"] left_right ‹n > 0›
by (simp_all add: r m add.commute [of 1]  a41 b41 del: power_Suc)
next
case False
then obtain r where r: "m = 2*r + 1" by (metis oddE)
show ?thesis
using order_trans [OF c_ge_u right_ge, of "1+2*r"] Suc.IH [of "m"]
using a_le_c [of "m"] c_le_b [of "m"] a_ge_0 [of "m"] b_le_1 [of "m"] left_right ‹n > 0›
apply (simp_all add: r m add.commute [of 3] a43 b43 del: power_Suc)
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›
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 "```