# Theory Arcwise_Connected

theory Arcwise_Connected
imports Ordered_Euclidean_Space Primes
```(*  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

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 @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 @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 (INTER UNIV A)"
using clo by blast
show "φ (INTER UNIV A)"
by (simp add: clo φ sub)
show "¬ U ⊂ INTER UNIV A" 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 = UNION K B"
using open_cov [of "ball x e"] by auto
ultimately have "UNION K B ⊆ -U"
by blast
have "K ≠ {}"
using ‹0 < e› ‹ball x e = UNION K B› 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 "INTER UNIV F ≠ {} ∧ INTER UNIV F ⊆ S ∧ φ (INTER UNIV F)"
proof (intro conjI)
show "INTER UNIV F ≠ {}"
apply (rule compact_nest)
apply (meson F cloF ‹compact S› seq_compact_closed_subset seq_compact_eq_compact)
by (meson Fsub lift_Suc_antimono_le)
show " INTER UNIV F ⊆ S"
using F by blast
show "φ (INTER UNIV F)"
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‹Arcwise Connections›

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" .
then
show "∃k. ∃f ∈ Basis → ℤ. dist (∑b∈Basis. (f b / 2^k) *⇩R b) x < e"
apply (rule_tac x=k in exI)
apply (rule_tac x="λi. of_int (floor (2^k*(x ∙ i)))" in bexI)
apply auto
done
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 dyadics :: "'a::field_char_0 set" where "dyadics ≡ ⋃k m. {of_nat m / 2^k}"

by (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)"
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'"
apply (rule prime_power_cancel2 [OF two_is_prime_nat])
using assms by auto
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
apply (clarsimp simp: dyadics_def Nats_def simp del: power_Suc)
apply (intro conjI subsetI)
apply (auto simp del: power_Suc)
apply (metis divide_numeral_1 numeral_One power_0)
apply (metis of_nat_Suc of_nat_mult of_nat_numeral)
qed

function (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, atomize_elim)
done

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

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

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 leftrec where "leftrec u v lc rc x ≡ fst (dyad_rec2 u v lc rc x)"
abbreviation 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)"
done

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

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

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

"{0<..<1} ∩ (⋃k m. {real m / 2^k}) = (⋃k. ⋃m ∈ {0<..<2^k}. {real m / 2^k})"
by (auto simp: divide_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 ∧
(∀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}"
apply (rule_tac c="max a c0" and d="min b d0" in that)
using ab01 cd0 by 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 a_le_c [of "m+1"] c_le_b [of "m+1"] a_ge_0 [of "m+1"] b_le_1 [of "m+1"]
Suc.IH [of "m+1"]
apply (simp add: r m add.commute [of 1] ‹n > 0› a41 b41 del: power_Suc)
apply (auto simp: left_right [THEN conjunct1])
using  order_trans [OF left_le c_le_v]
next
case False
then obtain r where r: "m = 2*r + 1" by (metis oddE)
show ?thesis
using a_le_c [of "m"] c_le_b [of "m"] a_ge_0 [of "m"] b_le_1 [of "m"]
Suc.IH [of "m+1"]
apply (simp add: r m add.commute [of 3] ‹n > 0› a43 b43 del: power_Suc)
apply (auto simp: add.commute left_right [THEN conjunct2])
using  order_trans [OF c_ge_u right_ge]
apply (metis (no_types, hide_lams) mult_2 numeral_One of_nat_add of_nat_numeral)
apply (metis Suc.IH mult_2 of_nat_1 of_nat_add)
done
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 order_trans apply blast
by (meson b_le_1 cleb order_trans)
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: divide_simps)
show "¦¦2^n¦ * ¦real i / 2^m - real j / 2^n¦¦ < 1"
using less.prems by (auto simp: divide_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 "real i / 2^m" "real 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: divide_simps)
moreover have "¦real i / 2 ^ m - real 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 (real i / 2 ^ m) ∧
c (real i / 2 ^ m) ≤ b (real (4 * k + 1) / 2 ^ Suc n)"
apply (rule less.IH [OF _ refl])
using closer ‹n < m› ‹d = m - n› apply (auto simp: divide_simps  ‹n < m› diff_less_mono2)
done
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›
done
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: divide_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)"
apply (rule less.IH [OF _ refl])
using closer ‹n < m› ‹d = m - n› apply (auto simp: divide_simps  ‹n < m› diff_less_mono2)
done
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›
done
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"]
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"]
ultimately have "¦a ((2 * real j + 1) / 2 ^ n) -
leftcut (a ((2 * real j + 1) / 2 ^ n)) (b ((2 * real j + 1) / 2 ^ n)) (c ((2 * real j + 1) / 2 ^ n))¦
≤ 2/2 ^ Suc n"
with j k ‹n > 0› show ?thesis
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"]
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"]
ultimately have "¦rightcut (a ((2 * real j + 1) / 2 ^ n)) (b ((2 * real j + 1) / 2 ^ n)) (c ((2 * real j + 1) / 2 ^ n)) -
b ((2 * real j + 1) / 2 ^ n)¦  ≤  2/2 ^ Suc n"
with j k ‹n > 0› show ?thesis
qed
qed
qed
have m1_to_3: "4 * real k - 1 = real (4 * (k-1)) + 3" if "0 < k" for k
using that by auto
have fb_eq_fa: "⟦0 < j; 2*j < 2 ^ n⟧ ⟹ f(b((2 * real j - 1) / 2^n)) = f(a((2 * real j + 1) / 2^n))" for n j
proof (induction n arbitrary: j)
case 0
then show ?case by auto
next
case (Suc n j) show ?case
proof (cases "n > 0")
case False
with Suc.prems show ?thesis by auto
next
case True
show ?thesis proof (cases "even j")
case True
then obtain k where k: "j = 2*k" by (metis evenE)
with ‹0 < j› have "k > 0" "2 * k < 2 ^ n"
using Suc.prems(2) k by auto
with k ‹0 < n› Suc.IH [of k] show ?thesis
apply (simp add: m1_to_3 a41 b43 del: power_Suc)
apply (subst of_nat_diff, auto)
done
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)"]
apply (auto simp: add.commute  feqm [OF order_refl]  feqm [OF _ order_refl, symmetric])
done
then
show ?thesis
qed
qed
qed
have f_eq_fc: "⟦0 < j; j < 2 ^ n⟧
⟹ f(b((2*j - 1) / 2 ^ (Suc n))) = f(c(j / 2^n)) ∧
f(a((2*j + 1) / 2 ^ (Suc n))) = f(c(j / 2^n))" for n and j::nat
proof (induction n arbitrary: j)
case 0
then show ?case by auto
next
case (Suc n)
show ?case
proof (cases "even j")
case True
then obtain k where k: "j = 2*k" by (metis evenE)
then have less2n: "k < 2 ^ n"
using Suc.prems(2) by auto
have "0 < k" using ‹0 < j› k by linarith
then have m1_to_3: "real (4 * k - Suc 0) = real (4 * (k-1)) + 3"
by auto
then show ?thesis
using Suc.IH [of k] k ‹0 < k›
apply (simp add: less2n add.commute [of 1] m1_to_3 a41 b43 del: power_Suc)
apply (auto simp: of_nat_diff)
done
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 (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
have "uniformly_continuous_on D01 (f ∘ c)"
proof (clarsimp simp: uniformly_continuous_on_def)
fix e::real
assume "0 < e"
have ucontf: "uniformly_continuous_on {0..1} f"
by (simp add: compact_uniformly_continuous [OF cont_f])
then obtain d where "0 < d" and d: "⋀x x'. ⟦x ∈ {0..1}; x' ∈ {0..1}; norm (x' - x) < d⟧ ⟹ norm (f x' - f x) < e/2"
unfolding uniformly_continuous_on_def dist_norm
by (metis ‹0 < e› less_divide_eq_numeral1(1) mult_zero_left)
obtain n where n: "1/2^n < min d 1"
by (metis ‹0 < d› divide_less_eq_1 less_numeral_extra(1) min_def one_less_numeral_iff power_one_over real_arch_pow_inv semiring_norm(76) zero_less_numeral)
with gr0I have "n > 0"
by (force simp: divide_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 ‹0 < e› show ?thesis by auto
next
case 2
have *: "abs(a - b) ≤ 1/2 ^ n ∧ 1/2 ^ n < d ∧ a ≤ c ∧ c ≤ b ⟹ b - c < d" for a b c
by auto
have "norm (c (real i / 2 ^ m) - b (real (2 * j - 1) / 2 ^ Suc n)) < d"
using 2 j n close_ab [of "2*j-1" "Suc n"]
using b_ge_0 [of "2*j-1" "Suc n"] b_le_1 [of "2*j-1" "Suc n"]
using aj_le_ci [of "2*j-1" i m "Suc n"]
using ci_le_bj [of "2*j-1" i m "Suc n"]
apply (simp add: divide_simps of_nat_diff del: power_Suc)
apply (auto simp: divide_simps intro!: *)
done
moreover have "f(c(j / 2^n)) = f(b ((2*j - 1) / 2 ^ (Suc n)))"
using f_eq_fc [OF j] by metis
ultimately show ?thesis
by (metis dist_norm atLeastAtMost_iff b_ge_0 b_le_1 c_ge_0 c_le_1 d)
next
case 3
have *: "abs(a - b) ≤ 1/2 ^ n ∧ 1/2 ^ n < d ∧ a ≤ c ∧ c ≤ b ⟹ c - a < d" for a b c
by auto
have "norm (c (real i / 2 ^ m) - a (real (2 * j + 1) / 2 ^ Suc n)) < d"
using 3 j n close_ab [of "2*j+1" "Suc n"]
using b_ge_0 [of "2*j+1" "Suc n"] b_le_1 [of "2*j+1" "Suc n"]
using aj_le_ci [of "2*j+1" i m "Suc n"]
using ci_le_bj [of "2*j+1" i m "Suc n"]
apply (simp add: divide_simps of_nat_diff del: power_Suc)
apply (auto simp: divide_simps intro!: *)
done
moreover have "f(c(j / 2^n)) = f(a ((2*j + 1) / 2 ^ (Suc n)))"
using f_eq_fc [OF j] by metis
ultimately show ?thesis
by (metis dist_norm a_ge_0 atLeastAtMost_iff a_ge_0 a_le_1 c_ge_0 c_le_1 d)
qed
qed
show "dist (f (c x')) (f (c x)) < e"
if "x ∈ D01" "x' ∈ D01" "dist x' x < 1/2^n" for x x'
proof clarsimp
fix i k::nat and m p
assume i: "0 < i" "i < 2 ^ m" and k: "0<k" "k < 2 ^ p"
assume clo: "dist (real k / 2 ^ p) (real i / 2 ^ m) < 1/2 ^ n"
obtain j::nat where "0 < j" "j < 2 ^ n"
and clo_ij: "abs(i / 2^m - j / 2^n) < 1/2 ^ n"
and clo_kj: "abs(k / 2^p - j / 2^n) < 1/2 ^ n"
proof -
have "max (2^n * i / 2^m) (2^n * k / 2^p) ≥ 0"
by (auto simp: le_max_iff_disj)
then obtain j where "floor (max (2^n*i / 2^m) (2^n*k / 2^p)) = int j"
using zero_le_floor zero_le_imp_eq_int by blast
then have j_le: "real j ≤ max (2^n * i / 2^m) (2^n * k / 2^p)"
and less_j1: "max (2^n * i / 2^m) (2^n * k / 2^p) < real j + 1"
using floor_correct [of "max (2^n * i / 2^m) (2^n * k / 2^p)"] by linarith+
show thesis
proof (cases "j = 0")
case True
show thesis
proof
show "(1::nat) < 2 ^ n"
apply (subst one_less_power)
using ‹n > 0› by auto
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"
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 "real j < 2 ^ n"
using j_le i k
apply (auto simp: le_max_iff_disj simp del: real_of_nat_less_numeral_power_cancel_iff elim!: le_less_trans)
apply (auto simp: field_simps)
done
then show "j < 2 ^ n"
by auto
show "¦real i / 2 ^ m - real j / 2 ^ n¦ < 1/2 ^ n"
using clo less_j1 j_le
apply (auto simp: le_max_iff_disj divide_simps dist_norm)
apply (auto simp: algebra_simps abs_if split: if_split_asm dest: 1 2)
done
show "¦real k / 2 ^ p - real j / 2 ^ n¦ < 1/2 ^ n"
using  clo less_j1 j_le
apply (auto simp: le_max_iff_disj divide_simps dist_norm)
apply (auto simp: algebra_simps not_less abs_if split: if_split_asm dest: 3 2)
done
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"
apply (rule dist_fc_close)
using ‹0 < j› ‹j < 2 ^ n› k clo_kj by auto
show "dist (f (c (real i / 2 ^ m))) (f (c (real j / 2 ^ n))) < e/2"
apply (rule dist_fc_close)
using ‹0 < j› ‹j < 2 ^ n› i clo_ij by auto
qed
qed
qed
qed
then obtain h where ucont_h: "uniformly_continuous_on {0..1} h"
and fc_eq: "⋀x. x ∈ D01 ⟹ (f ∘ c) x = h x"
proof (rule uniformly_continuous_on_extension_on_closure [of D01 "f ∘ c"])
qed (use closure_subset [of D01] in ‹auto intro!: that›)
then have cont_h: "continuous_on {0..1} h"
using uniformly_continuous_imp_continuous by blast
have h_eq: "h (real k / 2 ^ m) = f (c (real k / 2 ^ m))" if "0 < k" "k < 2^m" for k m
using fc_eq that by (force simp: D01_def)
have "h ` {0..1} = f ` {0..1}"
proof
have "h ` (closure D01) ⊆ f ` {0..1}"
proof (rule image_closure_subset)
show "continuous_on (closure D01) h"
using cont_h by simp
show "closed (f ` {0..1})"
using compact_continuous_image [OF cont_f] compact_imp_closed by blast
show "h ` D01 ⊆ f ` {0..1}"
by (force simp: dyadics_in_open_unit_interval D01_def h_eq)
qed
with cloD01 show "h ` {0..1} ⊆ f ` {0..1}" by simp
have a12 [simp]: "a (1/2) = u"
by (metis a_def leftrec_base numeral_One of_nat_numeral)
have b12 [simp]: "b (1/2) = v"
by (metis b_def rightrec_base numeral_One of_nat_numeral)
have "f ` {0..1} ⊆ closure(h ` D01)"
proof (clarsimp simp: closure_approachable dyadics_in_open_unit_interval D01_def)
fix x e::real
assume "0 ≤ x" "x ≤ 1" "0 < e"
have ucont_f: "uniformly_continuous_on {0..1} f"
using compact_uniformly_continuous cont_f by blast
then obtain δ where "δ > 0"
and δ: "⋀x x'. ⟦x ∈ {0..1}; x' ∈ {0..1}; dist x' x < δ⟧ ⟹ norm (f x' - f x) < e"
using ‹0 < e› by (auto simp: uniformly_continuous_on_def dist_norm)
have *: "∃m::nat. ∃y. odd m ∧ 0 < m ∧ m < 2 ^ n ∧ y ∈ {a(m / 2^n) .. b(m / 2^n)} ∧ f y = f x"
if "n ≠ 0" for n
using that
proof (induction n)
case 0 then show ?case by auto
next
case (Suc n)
show ?case
proof (cases "n=0")
case True
consider "x ∈ {0..u}" | "x ∈ {u..v}" | "x ∈ {v..1}"
using ‹0 ≤ x› ‹x ≤ 1› by force
then have "∃y≥a (real 1/2). y ≤ b (real 1/2) ∧ f y = f x"
proof cases
case 1
then show ?thesis
apply (rule_tac x=u in exI)
using uabv [of 1 1] f0u [of u] f0u [of x] by auto
next
case 2
then show ?thesis
by (rule_tac x=x in exI) auto
next
case 3
then show ?thesis
apply (rule_tac x=v in exI)
using uabv [of 1 1] fv1 [of v] fv1 [of x] by auto
qed
with ‹n=0› show ?thesis
by (rule_tac x=1 in exI) auto
next
case False
with Suc obtain m y
where "odd m" "0 < m" and mless: "m < 2 ^ n"
and y: "y ∈ {a (real m / 2 ^ n)..b (real m / 2 ^ n)}" and feq: "f y = f x"
by metis
then obtain j where j: "m = 2*j + 1" by (metis oddE)
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
then show ?thesis
apply (rule_tac x="4*j + 1" in exI)
apply (rule_tac x=y in exI)
using mless j ‹n ≠ 0›
done
next
case 2
show ?thesis
apply (rule_tac x="4*j + 1" in exI)
apply (rule_tac x="b((4*j + 1) / 2 ^ (Suc n))" in exI)
using mless ‹n ≠ 0› 2 j
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]
using left_right [of "c((2*j + 1) / 2^n)" "a((2*j + 1) / 2^n)" "b((2*j + 1) / 2^n)"]
apply (auto simp: feq [symmetric] intro: f_eqI)
done
next
case 3
then show ?thesis
apply (rule_tac x="4*j + 3" in exI)
apply (rule_tac x=y in exI)
using mless j ‹n ≠ 0›
apply (simp add: feq a43 b43 del: power_Suc)
done
qed
qed
qed
obtain n where n: "1/2^n < min (δ / 2) 1"
by (metis ‹0 < δ› divide_less_eq_1 less_numeral_extra(1) min_less_iff_conj one_less_numeral_iff power_one_over real_arch_pow_inv semiring_norm(76) zero_less_divide_iff zero_less_numeral)
with gr0I have "n ≠ 0"
by fastforce
with * obtain m::nat and y
where "odd m" "0 < m" and mless: "m < 2 ^ n"
and y: "y ∈ {a(m / 2^n) .. b(m / 2^n)}" and feq: "f x = f y"
by metis
then have "0 ≤ y" "y ≤ 1"
by (metis atLeastAtMost_iff a_ge_0 b_le_1 order.trans)+
moreover have "y < δ + c (real m / 2 ^ n)" "c (real m / 2 ^ n) < δ + y"
using y apply simp_all
using alec [of m n] cleb [of m n] n real_sum_of_halves close_ab [OF ‹odd m›, of n]
by linarith+
moreover note ‹0 < m› mless ‹0 ≤ x› ‹x ≤ 1›
ultimately show "∃k. ∃m∈{0<..<2 ^ k}. dist (h (real m / 2 ^ k)) (f x) < e"
apply (rule_tac x=n in exI)
apply (rule_tac x=m in bexI)
apply (auto simp: dist_norm h_eq feq δ)
done
qed
also have "... ⊆ h ` {0..1}"
apply (rule closure_minimal)
using compact_continuous_image [OF cont_h] compact_imp_closed by (auto simp: D01_def)
finally show "f ` {0..1} ⊆ h ` {0..1}" .
qed
moreover have "inj_on h {0..1}"
proof -
have "u < v"
by (metis atLeastAtMost_iff f0u f_1not0 fv1 order.not_eq_order_implies_strict u01(1) u01(2) v01(1))
have f_not_fu: "⋀x. ⟦u < x; x ≤ v⟧ ⟹ f x ≠ f u"
by (metis atLeastAtMost_iff f0u fu1 greaterThanAtMost_iff order_refl order_trans u01(1) v01(2))
have f_not_fv: "⋀x. ⟦u ≤ x; x < v⟧ ⟹ f x ≠ f v"
by (metis atLeastAtMost_iff order_refl order_trans v01(2) atLeastLessThan_iff fuv fv1)
have a_less_b:
"a(j / 2^n) < b(j / 2^n) ∧
(∀x. a(j / 2^n) < x ⟶ x ≤ b(j / 2^n) ⟶ f x ≠ f(a(j / 2^n))) ∧
(∀x. a(j / 2^n) ≤ x ⟶ x < b(j / 2^n) ⟶ f x ≠ f(b(j / 2^n)))" for n and j::nat
proof (induction n arbitrary: j)
case 0 then show ?case
by (simp add: ‹u < v› f_not_fu f_not_fv)
next
case (Suc n j) show ?case
proof (cases "n > 0")
case False then show ?thesis
by (auto simp: a_def b_def leftrec_base rightrec_base ‹u < v› f_not_fu f_not_fv)
next
case True show ?thesis
proof (cases "even j")
case True
with ‹0 < n› Suc.IH show ?thesis
by (auto elim!: evenE)
next
case False
then obtain k where k: "j = 2*k + 1" by (metis oddE)
then show ?thesis
proof (cases "even k")
case True
then obtain m where m: "k = 2*m" by (metis evenE)
have fleft: "f (leftcut (a ((2*m + 1) / 2^n)) (b ((2*m + 1) / 2^n)) (c ((2*m + 1) / 2^n))) =
f (c((2*m + 1) / 2^n))"
using alec [of "2*m+1" n] cleb [of "2*m+1" n] a_ge_0 [of "2*m+1" n]  b_le_1 [of "2*m+1" n]
using left_right_m [of "c((2*m + 1) / 2^n)" "a((2*m + 1) / 2^n)" "b((2*m + 1) / 2^n)"]
by (auto intro: f_eqI)
show ?thesis
proof (intro conjI impI notI allI)
have False if "b (real j / 2 ^ Suc n) ≤ a (real j / 2 ^ Suc n)"
proof -
have "f (c ((1 + real m * 2) / 2 ^ n)) = f (a ((1 + real m * 2) / 2 ^ n))"
using k m ‹0 < n› fleft that a41 [of n m] b41 [of n m]
using alec [of "2*m+1" n] cleb [of "2*m+1" n] a_ge_0 [of "2*m+1" n]  b_le_1 [of "2*m+1" n]
using left_right [of "c((2*m + 1) / 2^n)" "a((2*m + 1) / 2^n)" "b((2*m + 1) / 2^n)"]
by (auto simp: algebra_simps)
moreover have "a (real (1 + m * 2) / 2 ^ n) < c (real (1 + m * 2) / 2 ^ n)"
using Suc.IH [of "1 + m * 2"] by (simp add: c_def midpoint_def)
moreover have "c (real (1 + m * 2) / 2 ^ n) ≤ b (real (1 + m * 2) / 2 ^ n)"
using cleb by blast
ultimately show ?thesis
using Suc.IH [of "1 + m * 2"] by force
qed
then show "a (real j / 2 ^ Suc n) < b (real j / 2 ^ Suc n)" by force
next
fix x
assume "a (real j / 2 ^ Suc n) < x" "x ≤ b (real j / 2 ^ Suc n)" "f x = f (a (real j / 2 ^ Suc n))"
then show False
using Suc.IH [of "1 + m * 2", THEN conjunct2, THEN conjunct1]
using k m ‹0 < n› a41 [of n m] b41 [of n m]
using alec [of "2*m+1" n] cleb [of "2*m+1" n] a_ge_0 [of "2*m+1" n] b_le_1 [of "2*m+1" n]
using left_right_m [of "c((2*m + 1) / 2^n)" "a((2*m + 1) / 2^n)" "b((2*m + 1) / 2^n)"]
by (auto simp: algebra_simps)
next
fix x
assume "a (real j / 2 ^ Suc n) ≤ x" "x < b (real j / 2 ^ Suc n)" "f x = f (b (real j / 2 ^ Suc n))"
then show False
using k m ‹0 < n› a41 [of n m] b41 [of n m] fleft left_neq
using alec [of "2*m+1" n] cleb [of "2*m+1" n] a_ge_0 [of "2*m+1" n] b_le_1 [of "2*m+1" n]
by (auto simp: algebra_simps)
qed
next
case False
with oddE obtain m where m: "k = Suc (2*m)" by fastforce
have fright: "f (rightcut (a ((2*m + 1) / 2^n)) (b ((2*m + 1) / 2^n)) (c ((2*m + 1) / 2^n))) = f (c((2*m + 1) / 2^n))"
using alec [of "2*m+1" n] cleb [of "2*m+1" n] a_ge_0 [of "2*m+1" n]  b_le_1 [of "2*m+1" n]
using left_right_m [of "c((2*m + 1) / 2^n)" "a((2*m + 1) / 2^n)" "b((2*m + 1) / 2^n)"]
by (auto intro: f_eqI [OF _ order_refl])
show ?thesis
proof (intro conjI impI notI allI)
have False if "b (real j / 2 ^ Suc n) ≤ a (real j / 2 ^ Suc n)"
proof -
have "f (c ((1 + real m * 2) / 2 ^ n)) = f (b ((1 + real m * 2) / 2 ^ n))"
using k m ‹0 < n› fright that a43 [of n m] b43 [of n m]
using alec [of "2*m+1" n] cleb [of "2*m+1" n] a_ge_0 [of "2*m+1" n]  b_le_1 [of "2*m+1" n]
using left_right [of "c((2*m + 1) / 2^n)" "a((2*m + 1) / 2^n)" "b((2*m + 1) / 2^n)"]
by (auto simp: algebra_simps)
moreover have "a (real (1 + m * 2) / 2 ^ n) ≤ c (real (1 + m * 2) / 2 ^ n)"
using alec by blast
moreover have "c (real (1 + m * 2) / 2 ^ n) < b (real (1 + m * 2) / 2 ^ n)"
using Suc.IH [of "1 + m * 2"] by (simp add: c_def midpoint_def)
ultimately show ?thesis
using Suc.IH [of "1 + m * 2"] by force
qed
then show "a (real j / 2 ^ Suc n) < b (real j / 2 ^ Suc n)" by force
next
fix x
assume "a (real j / 2 ^ Suc n) < x" "x ≤ b (real j / 2 ^ Suc n)" "f x = f (a (real j / 2 ^ Suc n))"
then show False
using k m ‹0 < n› a43 [of n m] b43 [of n m] fright right_neq
using alec [of "2*m+1" n] cleb [of "2*m+1" n] a_ge_0 [of "2*m+1" n] b_le_1 [of "2*m+1" n]
by (auto simp: algebra_simps)
next
fix x
assume "a (real j / 2 ^ Suc n) ≤ x" "x < b (real j / 2 ^ Suc n)" "f x = f (b (real j / 2 ^ Suc n))"
then show False
using Suc.IH [of "1 + m * 2", THEN conjunct2, THEN conjunct2]
using k m ‹0 < n› a43 [of n m] b43 [of n m]
using alec [of "2*m+1" n] cleb [of "2*m+1" n] a_ge_0 [of "2*m+1" n] b_le_1 [of "2*m+1" n]
using left_right_m [of "c((2*m + 1) / 2^n)" "a((2*m + 1) / 2^n)" "b((2*m + 1) / 2^n)"]
by (auto simp: algebra_simps fright simp del: power_Suc)
qed
qed
qed
qed
qed
have c_gt_0 [simp]: "0 < c(m / 2^n)" and c_less_1 [simp]: "c(m / 2^n) < 1" for m::nat and n
using a_less_b [of m n] apply (simp_all add: c_def midpoint_def)
using a_ge_0 [of m n] b_le_1 [of m n] apply linarith+
done
have approx: "∃j n. odd j ∧ n ≠ 0 ∧
real i / 2^m ≤ real j / 2^n ∧
real j / 2^n ≤ real k / 2^p ∧
¦real i / 2 ^ m - real j / 2 ^ n¦ < 1/2^n ∧
¦real k / 2 ^ p - real j / 2 ^ n¦ < 1/2^n"
if "0 < i" "i < 2 ^ m" "0 < k" "k < 2 ^ p" "i / 2^m < k / 2^p" "m + p = N" for N m p i k
using that
proof (induction N arbitrary: m p i k rule: less_induct)
case (less N)
then consider "i / 2^m ≤ 1/2" "1/2 ≤ k / 2^p" | "k / 2^p < 1/2" | "k / 2^p ≥ 1/2" "1/2 < i / 2^m"
by linarith
then show ?case
proof cases
case 1
with less.prems show ?thesis
by (rule_tac x=1 in exI)+ (fastforce simp: divide_simps)
next
case 2 show ?thesis
proof (cases m)
case 0 with less.prems show ?thesis
by auto
next
case (Suc m') show ?thesis
proof (cases p)
case 0 with less.prems show ?thesis by auto
next
case (Suc p')
have False if "real i * 2 ^ p' < real k * 2 ^ m'" "k < 2 ^ p'" "2 ^ m' ≤ i"
proof -
have "real k * 2 ^ m' < 2 ^ p' * 2 ^ m'"
using that by simp
then have "real i * 2 ^ p' < 2 ^ p' * 2 ^ m'"
using that by linarith
with that show ?thesis by simp
qed
then show ?thesis
using less.IH [of "m'+p'" i m' k p'] less.prems ‹m = Suc m'› 2 Suc
apply atomize
apply (force simp: divide_simps)
done
qed
qed
next
case 3 show ?thesis
proof (cases m)
case 0 with less.prems show ?thesis
by auto
next
case (Suc m') show ?thesis
proof (cases p)
case 0 with less.prems show ?thesis by auto
next
case (Suc p')
then show ?thesis
using less.IH [of "m'+p'" "i - 2^m'" m' "k - 2 ^ p'" p'] less.prems ‹m = Suc m'› Suc 3
apply atomize
apply (auto simp: field_simps of_nat_diff)
apply (rule_tac x="2 ^ n + j" in exI, simp)
apply (rule_tac x="Suc n" in exI)
apply (auto simp: field_simps)
done
qed
qed
qed
qed
have clec: "c(real i / 2^m) ≤ c(real j / 2^n)"
if i: "0 < i" "i < 2 ^ m" and j: "0 < j" "j < 2 ^ n" and ij: "i / 2^m < j / 2^n" for m i n j
proof -
obtain j' n' where "odd j'" "n' ≠ 0"
and i_le_j: "real i / 2 ^ m ≤ real j' / 2 ^ n'"
and j_le_j: "real j' / 2 ^ n' ≤ real j / 2 ^ n"
and clo_ij: "¦real i / 2 ^ m - real j' / 2 ^ n'¦ < 1/2 ^ n'"
and clo_jj: "¦real j / 2 ^ n - real j' / 2 ^ n'¦ < 1/2 ^ n'"
using approx [of i m j n "m+n"] that i j ij by auto
with oddE obtain q where q: "j' = Suc (2*q)" by fastforce
have "c (real i / 2 ^ m) ≤ c((2*q + 1) / 2^n')"
proof (cases "i / 2^m = (2*q + 1) / 2^n'")
case True then show ?thesis by simp
next
case False
with i_le_j q have less: "i / 2^m < (2*q + 1) / 2^n'"
by auto
have *: "⟦i < q; abs(i - q) < s*2; q = r + s⟧ ⟹ abs(i - r) < s" for i q s r::real
by auto
have "c(i / 2^m) ≤ b(real(4 * q + 1) / 2 ^ (Suc n'))"
apply (rule ci_le_bj, force)
apply (rule * [OF less])
using i_le_j clo_ij q apply (auto simp: divide_simps)
done
then show ?thesis
using alec [of "2*q+1" n'] cleb [of "2*q+1" n'] a_ge_0 [of "2*q+1" n'] b_le_1 [of "2*q+1" n'] b41 [of n' q] ‹n' ≠ 0›
using left_right_m [of "c((2*q + 1) / 2^n')" "a((2*q + 1) / 2^n')" "b((2*q + 1) / 2^n')"]
by (auto simp: algebra_simps)
qed
also have "... ≤ c(real j / 2^n)"
proof (cases "j / 2^n = (2*q + 1) / 2^n'")
case True
then show ?thesis by simp
next
case False
with j_le_j q have less: "(2*q + 1) / 2^n' < j / 2^n"
by auto
have *: "⟦q < i; abs(i - q) < s*2; r = q + s⟧ ⟹ abs(i - r) < s" for i q s r::real
by auto
have "a(real(4*q + 3) / 2 ^ (Suc n')) ≤ c(j / 2^n)"
apply (rule aj_le_ci, force)
apply (rule * [OF less])
using j_le_j clo_jj q apply (auto simp: divide_simps)
done
then show ?thesis
using alec [of "2*q+1" n'] cleb [of "2*q+1" n'] a_ge_0 [of "2*q+1" n'] b_le_1 [of "2*q+1" n'] a43 [of n' q] ‹n' ≠ 0›
using left_right_m [of "c((2*q + 1) / 2^n')" "a((2*q + 1) / 2^n')" "b((2*q + 1) / 2^n')"]
by (auto simp: algebra_simps)
qed
finally show ?thesis .
qed
have "x = y" if "0 ≤ x" "x ≤ 1" "0 ≤ y" "y ≤ 1" "h x = h y" for x y
using that
proof (induction x y rule: linorder_class.linorder_less_wlog)
case (less x1 x2)
obtain m n where m: "0 < m" "m < 2 ^ n"
and x12: "x1 < m / 2^n" "m / 2^n < x2"
and neq: "h x1 ≠ h (real m / 2^n)"
proof -
have "(x1 + x2) / 2 ∈ closure D01"
using cloD01 less.hyps less.prems by auto
with less obtain y where "y ∈ D01" and dist_y: "dist y ((x1 + x2) / 2) < (x2 - x1) / 64"
unfolding closure_approachable
by (metis diff_gt_0_iff_gt less_divide_eq_numeral1(1) mult_zero_left)
obtain m n where m: "0 < m" "m < 2 ^ n"
and clo: "¦real m / 2 ^ n - (x1 + x2) / 2¦ < (x2 - x1) / 64"
and n: "1/2^n < (x2 - x1) / 128"
proof -
have "min 1 ((x2 - x1) / 128) > 0" "1/2 < (1::real)"
using less by auto
then obtain N where N: "1/2^N < min 1 ((x2 - x1) / 128)"
by (metis power_one_over real_arch_pow_inv)
then have "N > 0"
using less_divide_eq_1 by force
obtain p q where p: "p < 2 ^ q" "p ≠ 0" and yeq: "y = real p / 2 ^ q"
using ‹y ∈ D01› by (auto simp: zero_less_divide_iff D01_def)
show ?thesis
proof
show "0 < 2^N * p"
using p by auto
show "2 ^ N * p < 2 ^ (N+q)"
have "¦real (2 ^ N * p) / 2 ^ (N + q) - (x1 + x2) / 2¦ = ¦real p / 2 ^ q - (x1 + x2) / 2¦"
also have "... = ¦y - (x1 + x2) / 2¦"
also have "... < (x2 - x1) / 64"
using dist_y by (simp add: dist_norm)
finally show "¦real (2 ^ N * p) / 2 ^ (N + q) - (x1 + x2) / 2¦ < (x2 - x1) / 64" .
have "(1::real) / 2 ^ (N + q) ≤ 1/2^N"
also have "... < (x2 - x1) / 128"
using N by force
finally show "1/2 ^ (N + q) < (x2 - x1) / 128" .
qed
qed
obtain m' n' m'' n'' where "0 < m'" "m' < 2 ^ n'" "x1 < m' / 2^n'" "m' / 2^n' < x2"
and "0 < m''" "m'' < 2 ^ n''" "x1 < m'' / 2^n''" "m'' / 2^n'' < x2"
and neq: "h (real m'' / 2^n'') ≠ h (real m' / 2^n')"
proof
show "0 < Suc (2*m)"
by simp
show m21: "Suc (2*m) < 2 ^ Suc n"
using m by auto
show "x1 < real (Suc (2 * m)) / 2 ^ Suc n"
using clo by (simp add: field_simps abs_if split: if_split_asm)
show "real (Suc (2 * m)) / 2 ^ Suc n < x2"
using n clo by (simp add: field_simps abs_if split: if_split_asm)
show "0 < 4*m + 3"
by simp
have "m+1 ≤ 2 ^ n"
using m by simp
then have "4 * (m+1) ≤ 4 * (2 ^ n)"
by simp
then show m43: "4*m + 3 < 2 ^ (n+2)"
show "x1 < real (4 * m + 3) / 2 ^ (n + 2)"
using clo by (simp add: field_simps abs_if split: if_split_asm)
show "real (4 * m + 3) / 2 ^ (n + 2) < x2"
using n clo by (simp add: field_simps abs_if split: if_split_asm)
have c_fold: "midpoint (a ((2 * real m + 1) / 2 ^ Suc n)) (b ((2 * real m + 1) / 2 ^ Suc n)) = c ((2 * real m + 1) / 2 ^ Suc n)"
define R where "R ≡ rightcut (a ((2 * real m + 1) / 2 ^ Suc n)) (b ((2 * real m + 1) / 2 ^ Suc n))  (c ((2 * real m + 1) / 2 ^ Suc n))"
have "R < b ((2 * real m + 1) / 2 ^ Suc n)"
unfolding R_def  using a_less_b [of "4*m + 3" "n+2"] a43 [of "Suc n" m] b43 [of "Suc n" m]
by simp
then have Rless: "R < midpoint R (b ((2 * real m + 1) / 2 ^ Suc n))"
have midR_le: "midpoint R (b ((2 * real m + 1) / 2 ^ Suc n)) ≤ b ((2 * real m + 1) / (2 * 2 ^ n))"
using ‹R < b ((2 * real m + 1) / 2 ^ Suc n)›
have "(real (Suc (2 * m)) / 2 ^ Suc n) ∈ D01"  "real (4 * m + 3) / 2 ^ (n + 2) ∈ D01"
then show "h (real (4 * m + 3) / 2 ^ (n + 2)) ≠ h (real (Suc (2 * m)) / 2 ^ Suc n)"
using a_less_b [of "4*m + 3" "n+2", THEN conjunct1]
using a43 [of "Suc n" m] b43 [of "Suc n" m]
using alec [of "2*m+1" "Suc n"] cleb [of "2*m+1" "Suc n"] a_ge_0 [of "2*m+1" "Suc n"]  b_le_1 [of "2*m+1" "Suc n"]
apply (simp add: fc_eq [symmetric] c_def del: power_Suc)
apply (simp only: add.commute [of 1] c_fold R_def [symmetric])
apply (rule right_neq)
using Rless apply (simp add: R_def)
apply (rule midR_le, auto)
done
qed
then show ?thesis by (metis that)
qed
have m_div: "0 < m / 2^n" "m / 2^n < 1"
using m  by (auto simp: divide_simps)
have closure0m: "{0..m / 2^n} = closure ({0<..< m / 2^n} ∩ (⋃k m. {real m / 2 ^ k}))"
have closurem1: "{m / 2^n .. 1} = closure ({m / 2^n <..< 1} ∩ (⋃k m. {real m / 2 ^ k}))"
using ‹0 < real m / 2 ^ n› by linarith
have cont_h': "continuous_on (closure ({u<..<v} ∩ (⋃k m. {real m / 2 ^ k}))) h"
if "0 ≤ u" "v ≤ 1" for u v
apply (rule continuous_on_subset [OF cont_h])
apply (rule closure_minimal [OF subsetI])
using that apply auto
done
have closed_f': "closed (f ` {u..v})" if "0 ≤ u" "v ≤ 1" for u v
by (metis compact_continuous_image cont_f compact_interval atLeastatMost_subset_iff
compact_imp_closed continuous_on_subset that)
have less_2I: "⋀k i. real i / 2 ^ k < 1 ⟹ i < 2 ^ k"
by simp
have "h ` ({0<..<m / 2 ^ n} ∩ (⋃q p. {real p / 2 ^ q})) ⊆ f ` {0..c (m / 2 ^ n)}"
proof clarsimp
fix p q
assume p: "0 < real p / 2 ^ q" "real p / 2 ^ q < real m / 2 ^ n"
then have [simp]: "0 < p" "p < 2 ^ q"
apply (blast intro: p less_2I m_div less_trans)
done
have "f (c (real p / 2 ^ q)) ∈ f ` {0..c (real m / 2 ^ n)}"
by (auto simp: clec p m)
then show "h (real p / 2 ^ q) ∈ f ` {0..c (real m / 2 ^ n)}"
qed
then have "h ` {0 .. m / 2^n} ⊆ f ` {0 .. c(m / 2^n)}"
apply (subst closure0m)
apply (rule image_closure_subset [OF cont_h' closed_f'])
using m_div apply auto
done
then have hx1: "h x1 ∈ f ` {0 .. c(m / 2^n)}"
using x12 less.prems(1) by auto
then obtain t1 where t1: "h x1 = f t1" "0 ≤ t1" "t1 ≤ c (m / 2 ^ n)"
by auto
have "h ` ({m / 2 ^ n<..<1} ∩ (⋃q p. {real p / 2 ^ q})) ⊆ f ` {c (m / 2 ^ n)..1}"
proof clarsimp
fix p q
assume p: "real m / 2 ^ n < real p / 2 ^ q" and [simp]: "p < 2 ^ q"
then have [simp]: "0 < p"
using gr_zeroI m_div by fastforce
have "f (c (real p / 2 ^ q)) ∈ f ` {c (m / 2 ^ n)..1}"
by (auto simp: clec p m)
then show "h (real p / 2 ^ q) ∈ f ` {c (real m / 2 ^ n)..1}"
qed
then have "h ` {m / 2^n .. 1} ⊆ f ` {c(m / 2^n) .. 1}"
apply (subst closurem1)
apply (rule image_closure_subset [OF cont_h' closed_f'])
using m apply auto
done
then have hx2: "h x2 ∈ f ` {c(m / 2^n)..1}"
using x12 less.prems by auto
then obtain t2 where t2: "h x2 = f t2" "c (m / 2 ^ n) ≤ t2" "t2 ≤ 1"
by auto
with t1 less neq have False
using conn [of "h x2", unfolded is_interval_connected_1 [symmetric] is_interval_1, rule_format, of t1 t2 "c(m / 2^n)"]
then show ?case by blast
qed auto
then show ?thesis
by (auto simp: inj_on_def)
qed
ultimately have "{0..1::real} homeomorphic f ` {0..1}"
using homeomorphic_compact [OF _ cont_h] by blast
then show ?thesis
using homeomorphic_sym by blast
qed

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

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

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

subsection‹Accessibility of frontier points›

lemma dense_accessible_frontier_points:
fixes S :: "'a::{complete_space,real_normed_vector} set"
assumes "open S" and opeSV: "openin (subtopology euclidean (frontier S)) V" and "V ≠ {}"
obtains g where "arc g" "g ` {0..<1} ⊆ S" "pathstart g ∈ S" "pathfinish g ∈ V"
proof -
obtain z where "z ∈ V"
using ‹V ≠ {}› by auto
then obtain r where "r > 0" and r: "ball z r ∩ frontier S ⊆ V"
by (metis openin_contains_ball opeSV)
then have "z ∈ frontier S"
using ‹z ∈ V› opeSV openin_contains_ball by blast
then have "z ∈ closure S" "z ∉ S"
by (simp_all add: frontier_def assms interior_open)
with ‹r > 0› have "infinite (S ∩ ball z r)"
by (auto simp: closure_def islimpt_eq_infinite_ball)
then obtain y where "y ∈ S" and y: "y ∈ ball z r"
using infinite_imp_nonempty by force
then have "y ∉ frontier S"
by (meson ‹open S› disjoint_iff_not_equal frontier_disjoint_eq)
have "y ≠ z"
using ‹y ∈ S› ‹z ∉ S› by blast
have "path_connected(ball z r)"
with y ‹r > 0›  obtain g where "arc g" and pig: "path_image g ⊆ ball z r"
and g: "pathstart g = y" "pathfinish g = z"
using ‹y ≠ z› by (force simp: path_connected_arcwise)
have "compact (g -` frontier S ∩ {0..1})"
apply (simp add: compact_eq_bounded_closed bounded_Int bounded_closed_interval)
apply (rule closed_vimage_Int)
using ‹arc g› apply (auto simp: arc_def path_def)
done
moreover have "g -` frontier S ∩ {0..1} ≠ {}"
proof -
have "∃r. r ∈ g -` frontier S ∧ r ∈ {0..1}"
by (metis ‹z ∈ frontier S› g(2) imageE path_image_def pathfinish_in_path_image vimageI2)
then show ?thesis
by blast
qed
ultimately obtain t where gt: "g t ∈ frontier S" and "0 ≤ t" "t ≤ 1"
and t: "⋀u. ⟦g u ∈ frontier S; 0 ≤ u; u ≤ 1⟧ ⟹ t ≤ u"
by (force simp: dest!: compact_attains_inf)
moreover have "t ≠ 0"
by (metis ‹y ∉ frontier S› g(1) gt pathstart_def)
ultimately have  t01: "0 < t" "t ≤ 1"
by auto
have "V ⊆ frontier S"
using opeSV openin_contains_ball by blast
show ?thesis
proof
show "arc (subpath 0 t g)"
by (simp add: ‹0 ≤ t› ‹t ≤ 1› ‹arc g› ‹t ≠ 0› arc_subpath_arc)
have "g 0 ∈ S"
by (metis ‹y ∈ S› g(1) pathstart_def)
then show "pathstart (subpath 0 t g) ∈ S"
by auto
have "g t ∈ V"
by (metis IntI atLeastAtMost_iff gt image_eqI path_image_def pig r subsetCE ‹0 ≤ t› ‹t ≤ 1›)
then show "pathfinish (subpath 0 t g) ∈ V"
by auto
then have "inj_on (subpath 0 t g) {0..1}"
using t01
apply (clarsimp simp: inj_on_def subpath_def)
apply (drule inj_onD [OF arc_imp_inj_on [OF ‹arc g›]])
using mult_le_one apply auto
done
then have "subpath 0 t g ` {0..<1} ⊆ subpath 0 t g ` {0..1} - {subpath 0 t g 1}"
by (force simp: dest: inj_onD)
moreover have False if "subpath 0 t g ` ({0..<1}) - S ≠ {}"
proof -
have contg: "continuous_on {0..1} g"
using ‹arc g› by (auto simp: arc_def path_def)
have "subpath 0 t g ` {0..<1} ∩ frontier S ≠ {}"
proof (rule connected_Int_frontier [OF _ _ that])
show "connected (subpath 0 t g ` {0..<1})"
apply (rule connected_continuous_image)
apply (intro continuous_intros continuous_on_compose2 [OF contg])
apply (auto simp: ‹0 ≤ t› ‹t ≤ 1› mult_le_one)
done
show "subpath 0 t g ` {0..<1} ∩ S ≠ {}"
using ‹y ∈ S› g(1) by (force simp: subpath_def image_def pathstart_def)
qed
then obtain x where "x ∈ subpath 0 t g ` {0..<1}" "x ∈ frontier S"
by blast
with t01 ‹0 ≤ t› mult_le_one t show False
by (fastforce simp: subpath_def)
qed
then have "subpath 0 t g ` {0..1} - {subpath 0 t g 1} ⊆ S"
using subsetD by fastforce
ultimately  show "subpath 0 t g ` {0..<1} ⊆ S"
by auto
qed
qed

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

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

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

end
```