(* 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" by (simp add: A_def) 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 (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 "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) apply (simp add: F) 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" by (simp add: assms) 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.› proposition closure_dyadic_rationals: "closure (⋃k. ⋃f ∈ Basis → ℤ. { ∑i :: 'a :: euclidean_space ∈ Basis. (f i / 2^k) *⇩_{R}i }) = UNIV" proof - have "x ∈ closure (⋃k. ⋃f ∈ Basis → ℤ. {∑i ∈ Basis. (f i / 2^k) *⇩_{R}i})" for x::'a proof (clarsimp simp: closure_approachable) fix e::real assume "e > 0" then obtain k where k: "(1/2)^k < e/DIM('a)" by (meson DIM_positive divide_less_eq_1_pos of_nat_0_less_iff one_less_numeral_iff real_arch_pow_inv semiring_norm(76) zero_less_divide_iff zero_less_numeral) have "dist (∑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" . 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 lemma closure_dyadic_rationals_in_convex_set: "⟦convex S; interior S ≠ {}⟧ ⟹ closure(S ∩ (⋃k. ⋃f ∈ Basis → ℤ. { ∑i :: 'a :: euclidean_space ∈ Basis. (f i / 2^k) *⇩_{R}i })) = closure S" by (simp add: closure_dyadic_rationals closure_convex_Int_superset) lemma closure_rationals_in_convex_set: "⟦convex S; interior S ≠ {}⟧ ⟹ closure(S ∩ (⋃f ∈ Basis → ℚ. { ∑i :: 'a :: euclidean_space ∈ Basis. f i *⇩_{R}i })) = closure S" by (simp add: closure_rational_coordinates closure_convex_Int_superset) text‹ Every path between distinct points contains an arc, and hence path connection is equivalent to arcwise connection for distinct points. The proof is based on Whyburn's "Topological Analysis".› lemma closure_dyadic_rationals_in_convex_set_pos_1: fixes S :: "real set" assumes "convex S" and intnz: "interior S ≠ {}" and pos: "⋀x. x ∈ S ⟹ 0 ≤ x" shows "closure(S ∩ (⋃k m. {of_nat m / 2^k})) = closure S" proof - have "∃m. f 1/2^k = real m / 2^k" if "(f 1) / 2^k ∈ S" "f 1 ∈ ℤ" for k and f :: "real ⇒ real" using that by (force simp: Ints_def zero_le_divide_iff power_le_zero_eq dest: pos zero_le_imp_eq_int) then have "S ∩ (⋃k m. {real m / 2^k}) = S ∩ (⋃k. ⋃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}" lemma real_in_dyadics [simp]: "real m ∈ dyadics" apply (simp add: dyadics_def) 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)" by (simp add: divide_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: divide_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'" 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 lemma dyadic_413_cases: obtains "(of_nat m::'a::field_char_0) / 2^k ∈ Nats" | m' k' where "k' < k" "(of_nat m:: 'a) / 2^k = of_nat (4*m' + 1) / 2^Suc k'" | m' k' where "k' < k" "(of_nat m:: 'a) / 2^k = of_nat (4*m' + 3) / 2^Suc k'" proof (cases "m>0") case False then have "m=0" by simp with that show ?thesis by auto next case True obtain k' m' where m': "odd m'" and k': "m = m' * 2^k'" using prime_power_canonical [OF two_is_prime_nat True] by blast then obtain q r where q: "m' = 4*q + r" and r: "r < 4" by (metis not_add_less2 split_div zero_neq_numeral) show ?thesis proof (cases "k ≤ k'") case True have "(of_nat m:: 'a) / 2^k = of_nat m' * (2 ^ k' / 2^k)" using k' by (simp add: field_simps) also have "... = (of_nat m'::'a) * 2 ^ (k'-k)" using k' True by (simp add: power_diff) also have "... ∈ ℕ" by (metis Nats_mult of_nat_in_Nats of_nat_numeral of_nat_power) finally show ?thesis by (auto simp: that) next case False then obtain kd where kd: "Suc kd = k - k'" using Suc_diff_Suc not_less by blast have "(of_nat m:: 'a) / 2^k = of_nat m' * (2 ^ k' / 2^k)" using k' by (simp add: field_simps) also have "... = (of_nat m'::'a) / 2 ^ (k-k')" using k' False by (simp add: power_diff) also have "... = ((of_nat r + 4 * of_nat q)::'a) / 2 ^ (k-k')" using q by force finally have meq: "(of_nat m:: 'a) / 2^k = (of_nat r + 4 * of_nat q) / 2 ^ (k - k')" . have "r ≠ 0" "r ≠ 2" using q m' by presburger+ with r consider "r = 1" | "r = 3" by linarith then show ?thesis proof cases assume "r = 1" with meq kd that(2) [of kd q] show ?thesis by simp next assume "r = 3" with meq kd that(3) [of kd q] show ?thesis by simp qed qed qed lemma dyadics_iff: "(dyadics :: 'a::field_char_0 set) = Nats ∪ (⋃k m. {of_nat (4*m + 1) / 2^Suc k}) ∪ (⋃k m. {of_nat (4*m + 3) / 2^Suc k})" (is "_ = ?rhs") proof show "dyadics ⊆ ?rhs" unfolding dyadics_def apply clarify apply (rule dyadic_413_cases, force+) done next show "?rhs ⊆ dyadics" 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) by (metis of_nat_add 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) apply (fastforce simp add: dyadics_iff Nats_def field_simps)+ done lemma dyadics_levels: "dyadics = (⋃K. ⋃k<K. ⋃ m. {of_nat m / 2^k})" unfolding dyadics_def by auto lemma dyad_rec_level_termination: assumes "k < K" shows "dyad_rec_dom(b, l, r, real m / 2^k)" using assms proof (induction K arbitrary: k m) case 0 then show ?case by auto next case (Suc K) then consider "k = K" | "k < K" using less_antisym by blast then show ?case proof cases assume "k = K" show ?case proof (rule dyadic_413_cases [of m k, where 'a=real]) show "real m / 2^k ∈ ℕ ⟹ dyad_rec_dom (b, l, r, real m / 2^k)" by (force simp: Nats_def nat_neq_4k1 nat_neq_4k3 intro: dyad_rec.domintros) show ?case if "k' < k" and eq: "real m / 2^k = real (4 * m' + 1) / 2^Suc k'" for m' k' proof - have "dyad_rec_dom (b, l, r, (4 * real m' + 1) / 2^Suc k')" proof (rule dyad_rec.domintros) fix m n assume "(4 * real m' + 1) / (2 * 2 ^ k') = (4 * real m + 1) / (2 * 2^n)" then have "m' = m" "k' = n" using iff_4k [of _ 1] by auto have "dyad_rec_dom (b, l, r, real (2 * m + 1) / 2 ^ k')" using Suc.IH ‹k = K› ‹k' < k› by blast then show "dyad_rec_dom (b, l, r, (2 * real m + 1) / 2^n)" using ‹k' = n› by (auto simp: algebra_simps) next fix m n assume "(4 * real m' + 1) / (2 * 2 ^ k') = (4 * real m + 3) / (2 * 2^n)" then have "False" by (metis neq_4k1_k43) then show "dyad_rec_dom (b, l, r, (2 * real m + 1) / 2^n)" .. qed then show ?case by (simp add: eq add_ac) qed show ?case if "k' < k" and eq: "real m / 2^k = real (4 * m' + 3) / 2^Suc k'" for m' k' proof - have "dyad_rec_dom (b, l, r, (4 * real m' + 3) / 2^Suc k')" proof (rule dyad_rec.domintros) fix m n assume "(4 * real m' + 3) / (2 * 2 ^ k') = (4 * real m + 1) / (2 * 2^n)" then have "False" by (metis neq_4k1_k43) then show "dyad_rec_dom (b, l, r, (2 * real m + 1) / 2^n)" .. next fix m n assume "(4 * real m' + 3) / (2 * 2 ^ k') = (4 * real m + 3) / (2 * 2^n)" then have "m' = m" "k' = n" using iff_4k [of _ 3] by auto have "dyad_rec_dom (b, l, r, real (2 * m + 1) / 2 ^ k')" using Suc.IH ‹k = K› ‹k' < k› by blast then show "dyad_rec_dom (b, l, r, (2 * real m + 1) / 2^n)" using ‹k' = n› by (auto simp: algebra_simps) qed then show ?case by (simp add: eq add_ac) qed qed next assume "k < K" then show ?case using Suc.IH by blast qed qed lemma dyad_rec_termination: "x ∈ dyadics ⟹ dyad_rec_dom(b,l,r,x)" by (auto simp: dyadics_levels intro: dyad_rec_level_termination) lemma dyad_rec_of_nat [simp]: "dyad_rec b l r (real m) = b m" by (simp add: dyad_rec.psimps dyad_rec_termination) lemma dyad_rec_41 [simp]: "dyad_rec b l r ((4 * real m + 1) / 2 ^ (Suc n)) = l (dyad_rec b l r ((2*m + 1) / 2^n))" apply (rule dyad_rec.psimps) by (metis dyad_rec_level_termination lessI add.commute of_nat_Suc of_nat_mult of_nat_numeral) 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))" apply (rule dyad_rec.psimps) by (metis dyad_rec_level_termination lessI of_nat_add of_nat_mult of_nat_numeral) lemma dyad_rec_41_times2: assumes "n > 0" shows "dyad_rec b l r (2 * ((4 * real m + 1) / 2^Suc n)) = l (dyad_rec b l r (2 * (2 * real m + 1) / 2^n))" proof - obtain n' where n': "n = Suc n'" using assms not0_implies_Suc by blast have "dyad_rec b l r (2 * ((4 * real m + 1) / 2^Suc n)) = dyad_rec b l r ((2 * (4 * real m + 1)) / (2 * 2^n))" by auto also have "... = dyad_rec b l r ((4 * real m + 1) / 2^n)" by (subst mult_divide_mult_cancel_left) auto also have "... = l (dyad_rec b l r ((2 * real m + 1) / 2 ^ n'))" by (simp add: add.commute [of 1] n' del: power_Suc) also have "... = l (dyad_rec b l r ((2 * (2 * real m + 1)) / (2 * 2 ^ n')))" by (subst mult_divide_mult_cancel_left) auto also have "... = l (dyad_rec b l r (2 * (2 * real m + 1) / 2^n))" by (simp add: add.commute n') finally show ?thesis . qed lemma dyad_rec_43_times2: assumes "n > 0" shows "dyad_rec b l r (2 * ((4 * real m + 3) / 2^Suc n)) = r (dyad_rec b l r (2 * (2 * real m + 1) / 2^n))" proof - obtain n' where n': "n = Suc n'" using assms not0_implies_Suc by blast have "dyad_rec b l r (2 * ((4 * real m + 3) / 2^Suc n)) = dyad_rec b l r ((2 * (4 * real m + 3)) / (2 * 2^n))" by auto also have "... = dyad_rec b l r ((4 * real m + 3) / 2^n)" by (subst mult_divide_mult_cancel_left) auto also have "... = r (dyad_rec b l r ((2 * real m + 1) / 2 ^ n'))" by (simp add: n' del: power_Suc) also have "... = r (dyad_rec b l r ((2 * (2 * real m + 1)) / (2 * 2 ^ n')))" by (subst mult_divide_mult_cancel_left) auto also have "... = r (dyad_rec b l r (2 * (2 * real m + 1) / 2^n))" by (simp add: n') finally show ?thesis . qed definition dyad_rec2 where "dyad_rec2 u v lc rc x = dyad_rec (λz. (u,v)) (λ(a,b). (a, lc a b (midpoint a b))) (λ(a,b). (rc a b (midpoint a b), b)) (2*x)" 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" by (simp add: dyad_rec2_def) lemma leftrec_41: "n > 0 ⟹ leftrec u v lc rc ((4 * real m + 1) / 2 ^ (Suc n)) = leftrec u v lc rc ((2 * real m + 1) / 2^n)" apply (simp only: dyad_rec2_def dyad_rec_41_times2) apply (simp add: case_prod_beta) 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)))" apply (simp only: dyad_rec2_def dyad_rec_43_times2) apply (simp add: case_prod_beta) done lemma rightrec_base: "rightrec u v lc rc (real m / 2) = v" by (simp add: dyad_rec2_def) lemma rightrec_41: "n > 0 ⟹ rightrec u v lc rc ((4 * real m + 1) / 2 ^ (Suc n)) = lc (leftrec u v lc rc ((2 * real m + 1) / 2^n)) (rightrec u v lc rc ((2 * real m + 1) / 2^n)) (midpoint (leftrec u v lc rc ((2 * real m + 1) / 2^n)) (rightrec u v lc rc ((2 * real m + 1) / 2^n)))" apply (simp only: dyad_rec2_def dyad_rec_41_times2) apply (simp add: case_prod_beta) 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)" apply (simp only: dyad_rec2_def dyad_rec_43_times2) apply (simp add: case_prod_beta) done lemma dyadics_in_open_unit_interval: "{0<..<1} ∩ (⋃k m. {real m / 2^k}) = (⋃k. ⋃m ∈ {0<..<2^k}. {real m / 2^k})" by (auto simp: 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 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 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] by (metis (no_types, hide_lams) add.commute mult_2 of_nat_Suc of_nat_add) 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› apply (simp add: add.commute) 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› apply (simp add: add.commute) 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"] by (auto simp: add.commute left_right) moreover have "leftcut (a ((2 * real j + 1) / 2 ^ n)) (b ((2 * real j + 1) / 2 ^ n)) (c ((2 * real j + 1) / 2 ^ n)) ≤ c ((2 * real j + 1) / 2 ^ n)" using alec [of "2*j+1"] cleb [of "2*j+1"] a_ge_0 [of "2*j+1"] b_le_1 [of "2*j+1"] by (auto simp: add.commute left_right_m) ultimately have "¦a ((2 * real j + 1) / 2 ^ n) - leftcut (a ((2 * real j + 1) / 2 ^ n)) (b ((2 * real j + 1) / 2 ^ n)) (c ((2 * real j + 1) / 2 ^ n))¦ ≤ 2/2 ^ Suc n" by (simp add: c_def midpoint_def) with j k ‹n > 0› show ?thesis by (simp add: add.commute [of 1] a41 b41 del: power_Suc) next case False then obtain j where j: "k = 2*j + 1" by (metis oddE) have "¦a ((2 * real j + 1) / 2 ^ n) - (b ((2 * real j + 1) / 2 ^ n))¦ ≤ 2/2 ^ n" using Suc.IH [OF False] j by (auto simp: algebra_simps) moreover have "c ((2 * real j + 1) / 2 ^ n) ≤ rightcut (a ((2 * real j + 1) / 2 ^ n)) (b ((2 * real j + 1) / 2 ^ n)) (c ((2 * real j + 1) / 2 ^ n))" using alec [of "2*j+1"] cleb [of "2*j+1"] a_ge_0 [of "2*j+1"] b_le_1 [of "2*j+1"] by (auto simp: add.commute left_right_m) moreover have "rightcut (a ((2 * real j + 1) / 2 ^ n)) (b ((2 * real j + 1) / 2 ^ n)) (c ((2 * real j + 1) / 2 ^ n)) ≤ b ((2 * real j + 1) / 2 ^ n)" using alec [of "2*j+1"] cleb [of "2*j+1"] a_ge_0 [of "2*j+1"] b_le_1 [of "2*j+1"] by (auto simp: add.commute left_right) ultimately have "¦rightcut (a ((2 * real j + 1) / 2 ^ n)) (b ((2 * real j + 1) / 2 ^ n)) (c ((2 * real j + 1) / 2 ^ n)) - b ((2 * real j + 1) / 2 ^ n)¦ ≤ 2/2 ^ Suc n" by (simp add: c_def midpoint_def) with j k ‹n > 0› show ?thesis by (simp add: add.commute [of 3] a43 b43 del: power_Suc) qed qed qed have m1_to_3: "4 * real k - 1 = real (4 * (k-1)) + 3" if "0 < k" for k using that by auto have fb_eq_fa: "⟦0 < j; 2*j < 2 ^ n⟧ ⟹ f(b((2 * real j - 1) / 2^n)) = f(a((2 * real j + 1) / 2^n))" for n j proof (induction n arbitrary: j) case 0 then show ?case by auto next case (Suc n j) show ?case proof (cases "n > 0") case False with Suc.prems show ?thesis by auto next case True show ?thesis proof (cases "even j") case True then obtain k where k: "j = 2*k" by (metis evenE) with ‹0 < j› have "k > 0" "2 * k < 2 ^ n" using Suc.prems(2) k by auto with k ‹0 < n› Suc.IH [of k] show ?thesis apply (simp add: m1_to_3 a41 b43 del: power_Suc) 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 by (simp add: k add.commute [of 1] add.commute [of 3] a43 b41‹0 < n› del: power_Suc) qed qed qed have f_eq_fc: "⟦0 < j; j < 2 ^ n⟧ ⟹ f(b((2*j - 1) / 2 ^ (Suc n))) = f(c(j / 2^n)) ∧ f(a((2*j + 1) / 2 ^ (Suc n))) = f(c(j / 2^n))" for n and j::nat proof (induction n arbitrary: j) case 0 then show ?case by auto next case (Suc n) show ?case proof (cases "even j") case True then obtain k where k: "j = 2*k" by (metis evenE) then have less2n: "k < 2 ^ n" using Suc.prems(2) by auto have "0 < k" using ‹0 < j› k by linarith then have m1_to_3: "real (4 * k - Suc 0) = real (4 * (k-1)) + 3" by auto then show ?thesis using Suc.IH [of k] k ‹0 < k› 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 (simp add: add.commute [of 1] add.commute [of 3] m1_to_3 b41 a43 del: power_Suc) apply (force intro: feqm) done qed qed define D01 where "D01 ≡ {0<..<1} ∩ (⋃k m. {real m / 2^k})" have cloD01 [simp]: "closure D01 = {0..1}" unfolding D01_def by (subst closure_dyadic_rationals_in_convex_set_pos_1) auto have "uniformly_continuous_on D01 (f ∘ c)" proof (clarsimp simp: uniformly_continuous_on_def) fix e::real assume "0 < e" have ucontf: "uniformly_continuous_on {0..1} f" by (simp add: compact_uniformly_continuous [OF cont_f]) then obtain d where "0 < d" and d: "⋀x x'. ⟦x ∈ {0..1}; x' ∈ {0..1}; norm (x' - x) < d⟧ ⟹ norm (f x' - f x) < e/2" unfolding uniformly_continuous_on_def dist_norm by (metis ‹0 < e› less_divide_eq_numeral1(1) mult_zero_left) obtain n where n: "1/2^n < min d 1" by (metis ‹0 < d› divide_less_eq_1 less_numeral_extra(1) min_def one_less_numeral_iff power_one_over real_arch_pow_inv semiring_norm(76) zero_less_numeral) with gr0I have "n > 0" by (force simp: 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' using that unfolding D01_def dyadics_in_open_unit_interval proof clarsimp fix i k::nat and m p assume i: "0 < i" "i < 2 ^ m" and k: "0<k" "k < 2 ^ p" assume clo: "dist (real k / 2 ^ p) (real i / 2 ^ m) < 1/2 ^ n" obtain j::nat where "0 < j" "j < 2 ^ n" and clo_ij: "abs(i / 2^m - j / 2^n) < 1/2 ^ n" and clo_kj: "abs(k / 2^p - j / 2^n) < 1/2 ^ n" proof - have "max (2^n * i / 2^m) (2^n * k / 2^p) ≥ 0" by (auto simp: le_max_iff_disj) then obtain j where "floor (max (2^n*i / 2^m) (2^n*k / 2^p)) = int j" using zero_le_floor zero_le_imp_eq_int by blast then have j_le: "real j ≤ max (2^n * i / 2^m) (2^n * k / 2^p)" and less_j1: "max (2^n * i / 2^m) (2^n * k / 2^p) < real j + 1" using floor_correct [of "max (2^n * i / 2^m) (2^n * k / 2^p)"] by linarith+ show thesis proof (cases "j = 0") case True show thesis proof show "(1::nat) < 2 ^ n" 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" by (simp add: algebra_simps) then show ?thesis by simp qed have 3: "real j * 2 ^ p < 2 ^ p + real k * 2 ^ n" if j: "real j * 2 ^ m ≤ real i * 2 ^ n" and i: "real i * 2 ^ p ≤ real k * 2 ^ m" proof - have "real j * 2 ^ m * 2 ^ p ≤ real i * 2 ^ n * 2 ^ p" using j by simp moreover have "real i * 2 ^ p * 2 ^ n ≤ real k * 2 ^ m * 2 ^ n" using i by simp ultimately have "real j * 2 ^ m * 2 ^ p ≤ real k * 2 ^ m * 2 ^ n" by (simp only: mult_ac) then have "real j * 2 ^ p ≤ real k * 2 ^ n" by simp also have "... < 2 ^ p + real k * 2 ^ n" by auto finally show ?thesis by simp qed show ?thesis proof have "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› apply (simp add: feq a41 b41 add.commute [of 1] del: power_Suc) apply (simp add: algebra_simps) 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 (simp add: a41 b41 a43 b43 add.commute [of 1] add.commute [of 3] del: power_Suc) 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) apply (simp add: algebra_simps) 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)" by (simp add: p power_add) have "¦real (2 ^ N * p) / 2 ^ (N + q) - (x1 + x2) / 2¦ = ¦real p / 2 ^ q - (x1 + x2) / 2¦" by (simp add: power_add) also have "... = ¦y - (x1 + x2) / 2¦" by (simp add: yeq) also have "... < (x2 - x1) / 64" using dist_y by (simp add: dist_norm) finally show "¦real (2 ^ N * p) / 2 ^ (N + q) - (x1 + x2) / 2¦ < (x2 - x1) / 64" . have "(1::real) / 2 ^ (N + q) ≤ 1/2^N" by (simp add: field_simps) also have "... < (x2 - x1) / 128" using N by force finally show "1/2 ^ (N + q) < (x2 - x1) / 128" . qed qed obtain m' n' m'' n'' where "0 < m'" "m' < 2 ^ n'" "x1 < m' / 2^n'" "m' / 2^n' < x2" and "0 < m''" "m'' < 2 ^ n''" "x1 < m'' / 2^n''" "m'' / 2^n'' < x2" and neq: "h (real m'' / 2^n'') ≠ h (real m' / 2^n')" proof show "0 < Suc (2*m)" by simp show m21: "Suc (2*m) < 2 ^ Suc n" using m by auto show "x1 < real (Suc (2 * m)) / 2 ^ Suc n" using clo by (simp add: field_simps abs_if split: if_split_asm) show "real (Suc (2 * m)) / 2 ^ Suc n < x2" using n clo by (simp add: field_simps abs_if split: if_split_asm) show "0 < 4*m + 3" by simp have "m+1 ≤ 2 ^ n" using m by simp then have "4 * (m+1) ≤ 4 * (2 ^ n)" by simp then show m43: "4*m + 3 < 2 ^ (n+2)" by (simp add: algebra_simps) show "x1 < real (4 * m + 3) / 2 ^ (n + 2)" using clo by (simp add: field_simps abs_if split: if_split_asm) show "real (4 * m + 3) / 2 ^ (n + 2) < x2" using n clo by (simp add: field_simps abs_if split: if_split_asm) have c_fold: "midpoint (a ((2 * real m + 1) / 2 ^ Suc n)) (b ((2 * real m + 1) / 2 ^ Suc n)) = c ((2 * real m + 1) / 2 ^ Suc n)" by (simp add: c_def) define R where "R ≡ rightcut (a ((2 * real m + 1) / 2 ^ Suc n)) (b ((2 * real m + 1) / 2 ^ Suc n)) (c ((2 * real m + 1) / 2 ^ Suc n))" have "R < b ((2 * real m + 1) / 2 ^ Suc n)" unfolding R_def using a_less_b [of "4*m + 3" "n+2"] a43 [of "Suc n" m] b43 [of "Suc n" m] by simp then have Rless: "R < midpoint R (b ((2 * real m + 1) / 2 ^ Suc n))" by (simp add: midpoint_def) have midR_le: "midpoint R (b ((2 * real m + 1) / 2 ^ Suc n)) ≤ b ((2 * real m + 1) / (2 * 2 ^ n))" using ‹R < b ((2 * real m + 1) / 2 ^ Suc n)› by (simp add: midpoint_def) have "(real (Suc (2 * m)) / 2 ^ Suc n) ∈ D01" "real (4 * m + 3) / 2 ^ (n + 2) ∈ D01" by (simp_all add: D01_def m21 m43 del: power_Suc of_nat_Suc of_nat_add add_2_eq_Suc') blast+ then show "h (real (4 * m + 3) / 2 ^ (n + 2)) ≠ h (real (Suc (2 * m)) / 2 ^ Suc n)" using a_less_b [of "4*m + 3" "n+2", THEN conjunct1] using a43 [of "Suc n" m] b43 [of "Suc n" m] using alec [of "2*m+1" "Suc n"] cleb [of "2*m+1" "Suc n"] a_ge_0 [of "2*m+1" "Suc n"] b_le_1 [of "2*m+1" "Suc n"] apply (simp add: fc_eq [symmetric] c_def del: power_Suc) apply (simp only: add.commute [of 1] c_fold R_def [symmetric]) apply (rule right_neq) using Rless apply (simp add: R_def) apply (rule midR_le, auto) done qed then show ?thesis by (metis that) qed have m_div: "0 < m / 2^n" "m / 2^n < 1" using m by (auto simp: divide_simps) have closure0m: "{0..m / 2^n} = closure ({0<..< m / 2^n} ∩ (⋃k m. {real m / 2 ^ k}))" by (subst closure_dyadic_rationals_in_convex_set_pos_1, simp_all add: not_le m) have closurem1: "{m / 2^n .. 1} = closure ({m / 2^n <..< 1} ∩ (⋃k m. {real m / 2 ^ k}))" apply (subst closure_dyadic_rationals_in_convex_set_pos_1; simp add: not_le m) 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 (simp add: divide_simps) 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)}" by (simp add: h_eq) 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}" by (simp add: h_eq) 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)"] by (simp add: h_eq m) then show ?case by blast qed auto then show ?thesis by (auto simp: inj_on_def) qed ultimately have "{0..1::real} homeomorphic f ` {0..1}" using homeomorphic_compact [OF _ cont_h] by blast then show ?thesis using homeomorphic_sym by blast qed theorem path_contains_arc: fixes p :: "real ⇒ 'a::{complete_space,real_normed_vector}" assumes "path p" and a: "pathstart p = a" and b: "pathfinish p = b" and "a ≠ b" obtains q where "arc q" "path_image q ⊆ path_image p" "pathstart q = a" "pathfinish q = b" proof - have ucont_p: "uniformly_continuous_on {0..1} p" using ‹path p› unfolding path_def by (metis compact_Icc compact_uniformly_continuous) define φ where "φ ≡ λS. S ⊆ {0..1} ∧ 0 ∈ S ∧ 1 ∈ S ∧ (∀x ∈ S. ∀y ∈ S. open_segment x y ∩ S = {} ⟶ p x = p y)" obtain T where "closed T" "φ T" and T: "⋀U. ⟦closed U; φ U⟧ ⟹ ¬ (U ⊂ T)" proof (rule Brouwer_reduction_theorem_gen [of "{0..1}" φ]) have *: "{x<..<y} ∩ {0..1} = {x<..<y}" if "0 ≤ x" "y ≤ 1" "x ≤ y" for x y::real using that by auto show "φ {0..1}" by (auto simp: φ_def open_segment_eq_real_ivl *) show "φ (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" proof (clarsimp simp add: continuous_on_iff) fix u ε::real assume "0 < ε" "0 ≤ u" "u ≤ 1" then obtain δ where "δ > 0" and δ: "⋀v. v ∈ {0..1} ⟹ dist v u < δ ⟶ dist (p v) (p u) < ε / 2" using ucont_p [unfolded uniformly_continuous_on_def] by (metis atLeastAtMost_iff half_gt_zero_iff) then have "dist (h v) (h u) < ε" if "v ∈ {0..1}" "dist v u < δ" for v proof (cases "open_segment u v ∩ T = {}") case True then show ?thesis using ‹0 < ε› heq by auto next case False have uvT: "closed (closed_segment u v ∩ T)" "closed_segment u v ∩ T ≠ {}" using False open_closed_segment by (auto simp: ‹closed T› closed_Int) obtain w where "w ∈ T" and w: "w ∈ closed_segment u v" "open_segment u w ∩ T = {}" 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 proof (clarsimp simp add: connected_iff_connected_component) fix u v assume huv_eq: "h v = h u" and uv: "0 ≤ u" "u ≤ 1" "0 ≤ v" "v ≤ 1" have "∃T. connected T ∧ T ⊆ {0..1} ∧ T ⊆ h -` {h u} ∧ u ∈ T ∧ v ∈ T" proof (intro exI conjI) show "connected (closed_segment u v)" by simp show "closed_segment u v ⊆ {0..1}" by (simp add: uv closed_segment_eq_real_ivl) have pxy: "p x = p y" if "T ⊆ {0..1}" "0 ∈ T" "1 ∈ T" "x ∈ T" "y ∈ T" and disjT: "open_segment x y ∩ (T - open_segment u v) = {}" and xynot: "x ∉ open_segment u v" "y ∉ open_segment u v" for x y proof (cases "open_segment x y ∩ open_segment u v = {}") case True then show ?thesis by (metis Diff_Int_distrib Diff_empty peq disjT ‹x ∈ T› ‹y ∈ T›) next case False then have "open_segment x u ∪ open_segment y v ⊆ open_segment x y - open_segment u v ∨ open_segment y u ∪ open_segment x v ⊆ open_segment x y - open_segment u v" (is "?xuyv ∨ ?yuxv") using xynot by (fastforce simp add: open_segment_eq_real_ivl not_le not_less split: if_split_asm) then show "p x = p y" proof assume "?xuyv" then have "open_segment x u ∩ T = {}" "open_segment y v ∩ T = {}" using disjT by auto then have "h x = h y" using heq huv_eq by auto then show ?thesis using h_eq_p ‹x ∈ T› ‹y ∈ T› by auto next assume "?yuxv" then have "open_segment y u ∩ T = {}" "open_segment x v ∩ T = {}" using disjT by auto then have "h x = h y" using heq [of y u] heq [of x v] huv_eq by auto then show ?thesis using h_eq_p ‹x ∈ T› ‹y ∈ T› by auto qed qed have "¬ T - open_segment u v ⊂ T" proof (rule T) show "closed (T - open_segment u v)" by (simp add: closed_Diff [OF ‹closed T›] open_segment_eq_real_ivl) have "0 ∉ open_segment u v" "1 ∉ open_segment u v" using open_segment_eq_real_ivl uv by auto then show "φ (T - open_segment u v)" using ‹T ⊆ {0..1}› ‹0 ∈ T› ‹1 ∈ T› by (auto simp: φ_def) (meson peq pxy) qed then have "open_segment u v ∩ T = {}" by blast then show "closed_segment u v ⊆ h -` {h u}" by (force intro: heq simp: open_segment_eq_real_ivl closed_segment_eq_real_ivl split: if_split_asm)+ qed auto then show "connected_component ({0..1} ∩ h -` {h u}) u v" by (simp add: connected_component_def) qed show "h 1 ≠ h 0" by (metis ‹φ T› φ_def a ‹a ≠ b› b h_eq_p pathfinish_def pathstart_def) qed then obtain f and g :: "real ⇒ 'a" where gfeq: "(∀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)" by (simp add: convex_imp_path_connected) with y ‹r > 0› obtain g where "arc g" and pig: "path_image g ⊆ ball z r" and g: "pathstart g = y" "pathfinish g = z" using ‹y ≠ z› by (force simp: path_connected_arcwise) have "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 (simp add: subpath_def) 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" by (simp add: assms connected_open_path_connected) with ‹pathstart g ∈ S› ‹x ∈ S› have "path_component S x (pathstart g)" by (simp add: path_connected_component) then obtain f where "path f" and f: "path_image f ⊆ S" "pathstart f = x" "pathfinish f = pathstart g" by (auto simp: path_component_def) then have "path (f +++ g)" by (simp add: ‹arc g› arc_imp_path) then obtain h where "arc h" and h: "path_image h ⊆ path_image (f +++ g)" "pathstart h = x" "pathfinish h = pathfinish g" 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})" by (simp add: opeSU openin_delete) qed auto obtain γ where "arc γ" and γ: "path_image γ ⊆ path_image (reversepath h +++ g)" "pathstart γ = pathfinish h" "pathfinish γ = pathfinish g" proof (rule path_contains_arc [of "(reversepath h +++ g)" "pathfinish h" "pathfinish g"]) show "path (reversepath h +++ g)" by (simp add: ‹arc g› ‹arc h› ‹pathstart g = x› ‹pathstart h = x› arc_imp_path) show "pathstart (reversepath h +++ g) = pathfinish h" "pathfinish (reversepath h +++ g) = pathfinish g" by auto show "pathfinish h ≠ pathfinish g" using ‹pathfinish h ∈ U - {pathfinish g}› by auto qed auto show ?thesis proof show "arc γ" "pathstart γ ∈ U" "pathfinish γ ∈ V" using γ ‹arc γ› ‹pathfinish h ∈ U - {pathfinish g}› ‹pathfinish g ∈ V› by auto have "γ ` {0..1} - {γ 0, γ 1} ⊆ S" using γ g h apply (simp add: path_image_join) 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