(* Title: HOL/Analysis/Arcwise_Connected.thy Authors: LC Paulson, based on material from HOL Light *) section ‹Arcwise-Connected Sets› theory Arcwise_Connected imports Path_Connected Ordered_Euclidean_Space "HOL-Computational_Algebra.Primes" begin lemma path_connected_interval [simp]: fixes a b::"'a::ordered_euclidean_space" shows "path_connected {a..b}" using is_interval_cc is_interval_path_connected by blast lemma segment_to_closest_point: fixes S :: "'a :: euclidean_space set" shows "⟦closed S; S ≠ {}⟧ ⟹ open_segment a (closest_point S a) ∩ S = {}" unfolding disjoint_iff by (metis closest_point_le dist_commute dist_in_open_segment not_le) lemma segment_to_point_exists: fixes S :: "'a :: euclidean_space set" assumes "closed S" "S ≠ {}" obtains b where "b ∈ S" "open_segment a b ∩ S = {}" by (metis assms segment_to_closest_point closest_point_exists that) subsection ‹The Brouwer reduction theorem› theorem Brouwer_reduction_theorem_gen: fixes S :: "'a::euclidean_space set" assumes "closed S" "φ S" and φ: "⋀F. ⟦⋀n. closed(F n); ⋀n. φ(F n); ⋀n. F(Suc n) ⊆ F n⟧ ⟹ φ(⋂(range F))" obtains T where "T ⊆ S" "closed T" "φ T" "⋀U. ⟦U ⊆ S; closed U; φ U⟧ ⟹ ¬ (U ⊂ T)" proof - obtain B :: "nat ⇒ 'a set" where "inj B" "⋀n. open(B n)" and open_cov: "⋀S. open S ⟹ ∃K. S = ⋃(B ` K)" by (metis Setcompr_eq_image that univ_second_countable_sequence) define A where "A ≡ rec_nat S (λn a. if ∃U. U ⊆ a ∧ closed U ∧ φ U ∧ U ∩ (B n) = {} then SOME U. U ⊆ a ∧ closed U ∧ φ U ∧ U ∩ (B n) = {} else a)" have [simp]: "A 0 = S" by (simp add: A_def) have ASuc: "A(Suc n) = (if ∃U. U ⊆ A n ∧ closed U ∧ φ U ∧ U ∩ (B n) = {} then SOME U. U ⊆ A n ∧ closed U ∧ φ U ∧ U ∩ (B n) = {} else A n)" for n by (auto simp: A_def) have sub: "⋀n. A(Suc n) ⊆ A n" by (auto simp: ASuc dest!: someI_ex) have subS: "A n ⊆ S" for n by (induction n) (use sub in auto) have clo: "closed (A n) ∧ φ (A n)" for n by (induction n) (auto simp: assms ASuc dest!: someI_ex) show ?thesis proof show "⋂(range A) ⊆ S" using ‹⋀n. A n ⊆ S› by blast show "closed (⋂(A ` UNIV))" using clo by blast show "φ (⋂(A ` UNIV))" by (simp add: clo φ sub) show "¬ U ⊂ ⋂(A ` UNIV)" if "U ⊆ S" "closed U" "φ U" for U proof - have "∃y. x ∉ A y" if "x ∉ U" and Usub: "U ⊆ (⋂x. A x)" for x proof - obtain e where "e > 0" and e: "ball x e ⊆ -U" using ‹closed U› ‹x ∉ U› openE [of "-U"] by blast moreover obtain K where K: "ball x e = ⋃(B ` K)" using open_cov [of "ball x e"] by auto ultimately have "⋃(B ` K) ⊆ -U" by blast have "K ≠ {}" using ‹0 < e› ‹ball x e = ⋃(B ` K)› by auto then obtain n where "n ∈ K" "x ∈ B n" by (metis K UN_E ‹0 < e› centre_in_ball) then have "U ∩ B n = {}" using K e by auto show ?thesis proof (cases "∃U⊆A n. closed U ∧ φ U ∧ U ∩ B n = {}") case True then show ?thesis apply (rule_tac x="Suc n" in exI) apply (simp add: ASuc) apply (erule someI2_ex) using ‹x ∈ B n› by blast next case False then show ?thesis by (meson Inf_lower Usub ‹U ∩ B n = {}› ‹φ U› ‹closed U› range_eqI subset_trans) qed qed with that show ?thesis by (meson Inter_iff psubsetE rangeI subsetI) qed qed qed corollary Brouwer_reduction_theorem: fixes S :: "'a::euclidean_space set" assumes "compact S" "φ S" "S ≠ {}" and φ: "⋀F. ⟦⋀n. compact(F n); ⋀n. F n ≠ {}; ⋀n. φ(F n); ⋀n. F(Suc n) ⊆ F n⟧ ⟹ φ(⋂(range F))" obtains T where "T ⊆ S" "compact T" "T ≠ {}" "φ T" "⋀U. ⟦U ⊆ S; closed U; U ≠ {}; φ U⟧ ⟹ ¬ (U ⊂ T)" proof (rule Brouwer_reduction_theorem_gen [of S "λT. T ≠ {} ∧ T ⊆ S ∧ φ T"]) fix F assume cloF: "⋀n. closed (F n)" and F: "⋀n. F n ≠ {} ∧ F n ⊆ S ∧ φ (F n)" and Fsub: "⋀n. F (Suc n) ⊆ F n" show "⋂(F ` UNIV) ≠ {} ∧ ⋂(F ` UNIV) ⊆ S ∧ φ (⋂(F ` UNIV))" proof (intro conjI) show "⋂(F ` UNIV) ≠ {}" by (metis F Fsub ‹compact S› cloF closed_Int_compact compact_nest inf.orderE lift_Suc_antimono_le) show " ⋂(F ` UNIV) ⊆ S" using F by blast show "φ (⋂(F ` UNIV))" by (metis F Fsub φ ‹compact S› cloF closed_Int_compact inf.orderE) qed next show "S ≠ {} ∧ S ⊆ S ∧ φ S" by (simp add: assms) qed (meson assms compact_imp_closed seq_compact_closed_subset seq_compact_eq_compact)+ subsection✐‹tag unimportant›‹Arcwise Connections›(*FIX ME this subsection is empty(?) *) subsection‹Density of points with dyadic rational coordinates› 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" . with Ints_of_int show "∃k. ∃f ∈ Basis → ℤ. dist (∑b∈Basis. (f b / 2^k) *⇩_{R}b) x < e" by fastforce qed then show ?thesis by auto qed corollary closure_rational_coordinates: "closure (⋃f ∈ Basis → ℚ. { ∑i :: 'a :: euclidean_space ∈ Basis. f i *⇩_{R}i }) = UNIV" proof - have *: "(⋃k. ⋃f ∈ Basis → ℤ. { ∑i::'a ∈ Basis. (f i / 2^k) *⇩_{R}i }) ⊆ (⋃f ∈ Basis → ℚ. { ∑i ∈ Basis. f i *⇩_{R}i })" proof clarsimp fix k and f :: "'a ⇒ real" assume f: "f ∈ Basis → ℤ" show "∃x ∈ Basis → ℚ. (∑i ∈ Basis. (f i / 2^k) *⇩_{R}i) = (∑i ∈ Basis. x i *⇩_{R}i)" apply (rule_tac x="λi. f i / 2^k" in bexI) using Ints_subset_Rats f by auto qed show ?thesis using closure_dyadic_rationals closure_mono [OF *] by blast qed 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✐‹tag unimportant› dyadics :: "'a::field_char_0 set" where "dyadics ≡ ⋃k m. {of_nat m / 2^k}" lemma real_in_dyadics [simp]: "real m ∈ dyadics" by (simp add: dyadics_def) (metis divide_numeral_1 numeral_One power_0) lemma nat_neq_4k1: "of_nat m ≠ (4 * of_nat k + 1) / (2 * 2^n :: 'a::field_char_0)" proof assume "of_nat m = (4 * of_nat k + 1) / (2 * 2^n :: 'a)" then have "of_nat (m * (2 * 2^n)) = (of_nat (Suc (4 * k)) :: 'a)" by (simp add: field_split_simps) then have "m * (2 * 2^n) = Suc (4 * k)" using of_nat_eq_iff by blast then have "odd (m * (2 * 2^n))" by simp then show False by simp qed lemma nat_neq_4k3: "of_nat m ≠ (4 * of_nat k + 3) / (2 * 2^n :: 'a::field_char_0)" proof assume "of_nat m = (4 * of_nat k + 3) / (2 * 2^n :: 'a)" then have "of_nat (m * (2 * 2^n)) = (of_nat (4 * k + 3) :: 'a)" by (simp add: field_split_simps) then have "m * (2 * 2^n) = (4 * k) + 3" using of_nat_eq_iff by blast then have "odd (m * (2 * 2^n))" by simp then show False by simp qed lemma iff_4k: assumes "r = real k" "odd k" shows "(4 * real m + r) / (2 * 2^n) = (4 * real m' + r) / (2 * 2 ^ n') ⟷ m=m' ∧ n=n'" proof - { assume "(4 * real m + r) / (2 * 2^n) = (4 * real m' + r) / (2 * 2 ^ n')" then have "real ((4 * m + k) * (2 * 2 ^ n')) = real ((4 * m' + k) * (2 * 2^n))" using assms by (auto simp: field_simps) then have "(4 * m + k) * (2 * 2 ^ n') = (4 * m' + k) * (2 * 2^n)" using of_nat_eq_iff by blast then have "(4 * m + k) * (2 ^ n') = (4 * m' + k) * (2^n)" by linarith then obtain "4*m + k = 4*m' + k" "n=n'" using prime_power_cancel2 [OF two_is_prime_nat] assms by (metis even_mult_iff even_numeral odd_add) then have "m=m'" "n=n'" by auto } then show ?thesis by blast qed lemma neq_4k1_k43: "(4 * real m + 1) / (2 * 2^n) ≠ (4 * real m' + 3) / (2 * 2 ^ n')" proof assume "(4 * real m + 1) / (2 * 2^n) = (4 * real m' + 3) / (2 * 2 ^ n')" then have "real (Suc (4 * m) * (2 * 2 ^ n')) = real ((4 * m' + 3) * (2 * 2^n))" by (auto simp: field_simps) then have "Suc (4 * m) * (2 * 2 ^ n') = (4 * m' + 3) * (2 * 2^n)" using of_nat_eq_iff by blast then have "Suc (4 * m) * (2 ^ n') = (4 * m' + 3) * (2^n)" by linarith then have "Suc (4 * m) = (4 * m' + 3)" by (rule prime_power_cancel2 [OF two_is_prime_nat]) auto then have "1 + 2 * m' = 2 * m" using ‹Suc (4 * m) = 4 * m' + 3› by linarith then show False using even_Suc by presburger qed 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 have "range of_nat ⊆ (⋃k m. {(of_nat m::'a) / 2 ^ k})" by clarsimp (metis divide_numeral_1 numeral_One power_0) moreover have "⋀k m. ∃k' m'. ((1::'a) + 4 * of_nat m) / 2 ^ Suc k = of_nat m' / 2 ^ k'" by (metis (no_types) of_nat_Suc of_nat_mult of_nat_numeral) moreover have "⋀k m. ∃k' m'. (4 * of_nat m + (3::'a)) / 2 ^ Suc k = of_nat m' / 2 ^ k'" by (metis of_nat_add of_nat_mult of_nat_numeral) ultimately show "?rhs ⊆ dyadics" by (auto simp: dyadics_def Nats_def) qed function✐‹tag unimportant› (domintros) dyad_rec :: "[nat ⇒ 'a, 'a⇒'a, 'a⇒'a, real] ⇒ 'a" where "dyad_rec b l r (real m) = b m" | "dyad_rec b l r ((4 * real m + 1) / 2 ^ (Suc n)) = l (dyad_rec b l r ((2*m + 1) / 2^n))" | "dyad_rec b l r ((4 * real m + 3) / 2 ^ (Suc n)) = r (dyad_rec b l r ((2*m + 1) / 2^n))" | "x ∉ dyadics ⟹ dyad_rec b l r x = undefined" using iff_4k [of _ 1] iff_4k [of _ 3] apply (simp_all add: nat_neq_4k1 nat_neq_4k3 neq_4k1_k43 dyadics_iff Nats_def) by (fastforce simp: field_simps)+ lemma dyadics_levels: "dyadics = (⋃K. ⋃k<K. ⋃ m. {of_nat m / 2^k})" unfolding dyadics_def by auto 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))" proof (rule dyad_rec.psimps) show "dyad_rec_dom (b, l, r, (4 * real m + 1) / 2 ^ Suc n)" by (metis add.commute dyad_rec_level_termination lessI of_nat_Suc of_nat_mult of_nat_numeral) qed lemma dyad_rec_43 [simp]: "dyad_rec b l r ((4 * real m + 3) / 2 ^ (Suc n)) = r (dyad_rec b l r ((2*m + 1) / 2^n))" proof (rule dyad_rec.psimps) show "dyad_rec_dom (b, l, r, (4 * real m + 3) / 2 ^ Suc n)" by (metis dyad_rec_level_termination lessI of_nat_add of_nat_mult of_nat_numeral) qed lemma dyad_rec_41_times2: assumes "n > 0" shows "dyad_rec b l r (2 * ((4 * real m + 1) / 2^Suc n)) = l (dyad_rec b l r (2 * (2 * real m + 1) / 2^n))" proof - obtain n' where n': "n = Suc n'" using assms not0_implies_Suc by blast have "dyad_rec b l r (2 * ((4 * real m + 1) / 2^Suc n)) = dyad_rec b l r ((2 * (4 * real m + 1)) / (2 * 2^n))" by auto also have "... = dyad_rec b l r ((4 * real m + 1) / 2^n)" by (subst mult_divide_mult_cancel_left) auto also have "... = l (dyad_rec b l r ((2 * real m + 1) / 2 ^ n'))" by (simp add: add.commute [of 1] n' del: power_Suc) also have "... = l (dyad_rec b l r ((2 * (2 * real m + 1)) / (2 * 2 ^ n')))" by (subst mult_divide_mult_cancel_left) auto also have "... = l (dyad_rec b l r (2 * (2 * real m + 1) / 2^n))" by (simp add: add.commute n') finally show ?thesis . qed lemma dyad_rec_43_times2: assumes "n > 0" shows "dyad_rec b l r (2 * ((4 * real m + 3) / 2^Suc n)) = r (dyad_rec b l r (2 * (2 * real m + 1) / 2^n))" proof - obtain n' where n': "n = Suc n'" using assms not0_implies_Suc by blast have "dyad_rec b l r (2 * ((4 * real m + 3) / 2^Suc n)) = dyad_rec b l r ((2 * (4 * real m + 3)) / (2 * 2^n))" by auto also have "... = dyad_rec b l r ((4 * real m + 3) / 2^n)" by (subst mult_divide_mult_cancel_left) auto also have "... = r (dyad_rec b l r ((2 * real m + 1) / 2 ^ n'))" by (simp add: n' del: power_Suc) also have "... = r (dyad_rec b l r ((2 * (2 * real m + 1)) / (2 * 2 ^ n')))" by (subst mult_divide_mult_cancel_left) auto also have "... = r (dyad_rec b l r (2 * (2 * real m + 1) / 2^n))" by (simp add: n') finally show ?thesis . qed definition✐‹tag unimportant› 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✐‹tag unimportant› leftrec where "leftrec u v lc rc x ≡ fst (dyad_rec2 u v lc rc x)" abbreviation✐‹tag unimportant› rightrec where "rightrec u v lc rc x ≡ snd (dyad_rec2 u v lc rc x)" lemma leftrec_base: "leftrec u v lc rc (real m / 2) = u" by (simp add: dyad_rec2_def) lemma leftrec_41: "n > 0 ⟹ leftrec u v lc rc ((4 * real m + 1) / 2 ^ (Suc n)) = leftrec u v lc rc ((2 * real m + 1) / 2^n)" unfolding dyad_rec2_def dyad_rec_41_times2 by (simp add: case_prod_beta) lemma leftrec_43: "n > 0 ⟹ leftrec u v lc rc ((4 * real m + 3) / 2 ^ (Suc n)) = rc (leftrec u v lc rc ((2 * real m + 1) / 2^n)) (rightrec u v lc rc ((2 * real m + 1) / 2^n)) (midpoint (leftrec u v lc rc ((2 * real m + 1) / 2^n)) (rightrec u v lc rc ((2 * real m + 1) / 2^n)))" unfolding dyad_rec2_def dyad_rec_43_times2 by (simp add: case_prod_beta) lemma rightrec_base: "rightrec u v lc rc (real m / 2) = v" by (simp add: dyad_rec2_def) lemma rightrec_41: "n > 0 ⟹ rightrec u v lc rc ((4 * real m + 1) / 2 ^ (Suc n)) = lc (leftrec u v lc rc ((2 * real m + 1) / 2^n)) (rightrec u v lc rc ((2 * real m + 1) / 2^n)) (midpoint (leftrec u v lc rc ((2 * real m + 1) / 2^n)) (rightrec u v lc rc ((2 * real m + 1) / 2^n)))" unfolding dyad_rec2_def dyad_rec_41_times2 by (simp add: case_prod_beta) lemma rightrec_43: "n > 0 ⟹ rightrec u v lc rc ((4 * real m + 3) / 2 ^ (Suc n)) = rightrec u v lc rc ((2 * real m + 1) / 2^n)" unfolding dyad_rec2_def dyad_rec_43_times2 by (simp add: case_prod_beta) lemma dyadics_in_open_unit_interval: "{0<..<1} ∩ (⋃k m. {real m / 2^k}) = (⋃k. ⋃m ∈ {0<..<2^k}. {real m / 2^k})" by (auto simp: field_split_simps) lemma padic_rational_approximation_straddle: assumes "ε > 0" "p > 1" obtains n q r where "of_int q / p^n < x" "x < of_int r / p^n" "¦q / p^n - r / p^n ¦ < ε" proof - obtain n where n: "2 / ε < p ^ n" using ‹p>1› real_arch_pow by blast define q where "q ≡ ⌊p ^ n * x⌋ - 1" show thesis proof show "q / p ^ n < x" "x < real_of_int (q+2) / p ^ n" using assms by (simp_all add: q_def divide_simps floor_less_cancel mult.commute) show "¦q / p ^ n - real_of_int (q+2) / p ^ n¦ < ε" using assms n by (simp add: q_def divide_simps mult.commute) qed qed lemma padic_rational_approximation_straddle_pos: assumes "ε > 0" "p > 1" "x > 0" obtains n q r where "of_nat q / p^n < x" "x < of_nat r / p^n" "¦q / p^n - r / p^n ¦ < ε" proof - obtain n q r where *: "of_int q / p^n < x" "x < of_int r / p^n" "¦q / p^n - r / p^n ¦ < ε" using padic_rational_approximation_straddle assms by metis then have "r ≥ 0" using assms by (smt (verit, best) divide_nonpos_pos of_int_0_le_iff zero_less_power) show thesis proof show "real (max 0 (nat q)) / p ^ n < x" using * by (metis assms(3) div_0 max_nat.left_neutral nat_eq_iff2 of_nat_0 of_nat_nat) show "x < real (nat r) / p ^ n" using ‹r ≥ 0› * by force show "¦real (max 0 (nat q)) / p ^ n - real (nat r) / p ^ n¦ < ε" using * assms by (simp add: divide_simps) qed qed lemma padic_rational_approximation_straddle_pos_le: assumes "ε > 0" "p > 1" "x ≥ 0" obtains n q r where "of_nat q / p^n ≤ x" "x < of_nat r / p^n" "¦q / p^n - r / p^n ¦ < ε" proof - obtain n q r where *: "of_int q / p^n < x" "x < of_int r / p^n" "¦q / p^n - r / p^n ¦ < ε" using padic_rational_approximation_straddle assms by metis then have "r ≥ 0" using assms by (smt (verit, best) divide_nonpos_pos of_int_0_le_iff zero_less_power) show thesis proof show "real (max 0 (nat q)) / p ^ n ≤ x" using * assms(3) nle_le by fastforce show "x < real (nat r) / p ^ n" using ‹r ≥ 0› * by force show "¦real (max 0 (nat q)) / p ^ n - real (nat r) / p ^ n¦ < ε" using * assms by (simp add: divide_simps) qed qed subsubsection ‹Definition by recursion on dyadic rationals in [0,1]› lemma recursion_on_dyadic_fractions: assumes base: "R a b" and step: "⋀x y. R x y ⟹ ∃z. R x z ∧ R z y" and trans: "⋀x y z. ⟦R x y; R y z⟧ ⟹ R x z" shows "∃f :: real ⇒ 'a. f 0 = a ∧ f 1 = b ∧ (∀x ∈ dyadics ∩ {0..1}. ∀y ∈ dyadics ∩ {0..1}. x < y ⟶ R (f x) (f y))" proof - obtain mid where mid: "R x y ⟹ R x (mid x y)" "R x y ⟹ R (mid x y) y" for x y using step by metis define g where "g ≡ rec_nat (λk. if k = 0 then a else b) (λn r k. if even k then r (k div 2) else mid (r ((k - 1) div 2)) (r ((Suc k) div 2)))" have g0 [simp]: "g 0 = (λk. if k = 0 then a else b)" by (simp add: g_def) have gSuc [simp]: "⋀n. g(Suc n) = (λk. if even k then g n (k div 2) else mid (g n ((k - 1) div 2)) (g n ((Suc k) div 2)))" by (auto simp: g_def) have g_eq_g: "2 ^ d * k = k' ⟹ g n k = g (n + d) k'" for n d k k' by (induction d arbitrary: k k') auto have "g n k = g n' k'" if "real k / 2^n = real k' / 2^n'" "n' ≤ n" for k n k' n' proof - have "real k = real k' * 2 ^ (n-n')" using that by (simp add: power_diff divide_simps) then have "k = k' * 2 ^ (n-n')" using of_nat_eq_iff by fastforce with g_eq_g show ?thesis by (metis le_add_diff_inverse mult.commute that(2)) qed then have g_eq_g: "g n k = g n' k'" if "real k / 2 ^ n = real k' / 2 ^ n'" for k n k' n' by (metis nat_le_linear that) then obtain f where "(λ(k,n). g n k) = f ∘ (λ(k,n). k / 2 ^ n)" using function_factors_left by (smt (verit, del_insts) case_prod_beta') then have f_eq_g: "⋀k n. f(real k / 2 ^ n) = g n k" by (simp add: fun_eq_iff) show ?thesis proof (intro exI conjI strip) show "f 0 = a" by (metis f_eq_g g0 div_0 of_nat_0) show "f 1 = b" by (metis f_eq_g g0 div_by_1 of_nat_1_eq_iff power_0 zero_neq_one) show "R (f x) (f y)" if x: "x ∈ dyadics ∩ {0..1}" and y: "y ∈ dyadics ∩ {0..1}" and "x < y" for x y proof - obtain n1 k1 where xeq: "x = real k1 / 2^n1" "k1 ≤ 2^n1" using x by (auto simp: dyadics_def) obtain n2 k2 where yeq: "y = real k2 / 2^n2" "k2 ≤ 2^n2" using y by (auto simp: dyadics_def) have xcommon: "x = real(2^n2 * k1) / 2 ^ (n1+n2)" using xeq by (simp add: power_add) have ycommon: "y = real(2^n1 * k2) / 2 ^ (n1+n2)" using yeq by (simp add: power_add) have *: "R (g n j) (g n k)" if "j < k" "k ≤ 2^n" for n j k using that proof (induction n arbitrary: j k) case 0 then show ?case by (simp add: base) next case (Suc n) show ?case proof (cases "even j") case True then obtain a where [simp]: "j = 2*a" by blast show ?thesis proof (cases "even k") case True with Suc show ?thesis by (auto elim!: evenE) next case False then obtain b where [simp]: "k = Suc (2*b)" using oddE by fastforce show ?thesis using Suc apply simp by (smt (verit, ccfv_SIG) less_Suc_eq linorder_not_le local.trans mid(1) nat_mult_less_cancel1 pos2) qed next case False then obtain a where [simp]: "j = Suc (2*a)" using oddE by fastforce show ?thesis proof (cases "even k") case True then obtain b where [simp]: "k = 2*b" by blast show ?thesis using Suc apply simp by (smt (verit, ccfv_SIG) Suc_leI Suc_lessD le_trans lessI linorder_neqE_nat linorder_not_le local.trans mid(2) nat_mult_less_cancel1 pos2) next case False then obtain b where [simp]: "k = Suc (2*b)" using oddE by fastforce show ?thesis using Suc apply simp by (smt (verit) Suc_leI le_trans lessI less_or_eq_imp_le linorder_neqE_nat linorder_not_le local.trans mid(1) mid(2) nat_mult_less_cancel1 pos2) qed qed qed show ?thesis unfolding xcommon ycommon f_eq_g proof (rule *) show "2 ^ n2 * k1 < 2 ^ n1 * k2" using of_nat_less_iff ‹x < y› by (fastforce simp: xeq yeq field_simps) show "2 ^ n1 * k2 ≤ 2 ^ (n1 + n2)" by (simp add: power_add yeq) qed qed qed qed lemma dyadics_add: assumes "x ∈ dyadics" "y ∈ dyadics" shows "x+y ∈ dyadics" proof - obtain i j m n where x: "x = of_nat i / 2 ^ m" and y: "y = of_nat j / 2 ^ n" using assms by (auto simp: dyadics_def) have xcommon: "x = of_nat(2^n * i) / 2 ^ (m+n)" using x by (simp add: power_add) moreover have ycommon: "y = of_nat(2^m * j) / 2 ^ (m+n)" using y by (simp add: power_add) ultimately have "x+y = (of_nat(2^n * i + 2^m * j)) / 2 ^ (m+n)" by (simp add: field_simps) then show ?thesis unfolding dyadics_def by blast qed lemma dyadics_diff: fixes x :: "'a::linordered_field" assumes "x ∈ dyadics" "y ∈ dyadics" "y ≤ x" shows "x-y ∈ dyadics" proof - obtain i j m n where x: "x = of_nat i / 2 ^ m" and y: "y = of_nat j / 2 ^ n" using assms by (auto simp: dyadics_def) have j_le_i: "j * 2 ^ m ≤ i * 2 ^ n" using of_nat_le_iff ‹y ≤ x› unfolding x y by (fastforce simp add: divide_simps) have xcommon: "x = of_nat(2^n * i) / 2 ^ (m+n)" using x by (simp add: power_add) moreover have ycommon: "y = of_nat(2^m * j) / 2 ^ (m+n)" using y by (simp add: power_add) ultimately have "x-y = (of_nat(2^n * i - 2^m * j)) / 2 ^ (m+n)" by (simp add: xcommon ycommon field_simps j_le_i of_nat_diff) then show ?thesis unfolding dyadics_def by blast qed theorem homeomorphic_monotone_image_interval: fixes f :: "real ⇒ 'a::{real_normed_vector,complete_space}" assumes cont_f: "continuous_on {0..1} f" and conn: "⋀y. connected ({0..1} ∩ f -` {y})" and f_1not0: "f 1 ≠ f 0" shows "(f ` {0..1}) homeomorphic {0..1::real}" proof - have "∃c d. a ≤ c ∧ c ≤ m ∧ m ≤ d ∧ d ≤ b ∧ (∀x ∈ {c..d}. f x = f m) ∧ (∀x ∈ {a..<c}. (f x ≠ f m)) ∧ (∀x ∈ {d<..b}. (f x ≠ f m)) ∧ (∀x ∈ {a..<c}. ∀y ∈ {d<..b}. f x ≠ f y)" if m: "m ∈ {a..b}" and ab01: "{a..b} ⊆ {0..1}" for a b m proof - have comp: "compact (f -` {f m} ∩ {0..1})" by (simp add: compact_eq_bounded_closed bounded_Int closed_vimage_Int cont_f) obtain c0 d0 where cd0: "{0..1} ∩ f -` {f m} = {c0..d0}" using connected_compact_interval_1 [of "{0..1} ∩ f -` {f m}"] conn comp by (metis Int_commute) with that have "m ∈ cbox c0 d0" by auto obtain c d where cd: "{a..b} ∩ f -` {f m} = {c..d}" using ab01 cd0 by (rule_tac c="max a c0" and d="min b d0" in that) auto then have cdab: "{c..d} ⊆ {a..b}" by blast show ?thesis proof (intro exI conjI ballI) show "a ≤ c" "d ≤ b" using cdab cd m by auto show "c ≤ m" "m ≤ d" using cd m by auto show "⋀x. x ∈ {c..d} ⟹ f x = f m" using cd by blast show "f x ≠ f m" if "x ∈ {a..<c}" for x using that m cd [THEN equalityD1, THEN subsetD] ‹c ≤ m› by force show "f x ≠ f m" if "x ∈ {d<..b}" for x using that m cd [THEN equalityD1, THEN subsetD, of x] ‹m ≤ d› by force show "f x ≠ f y" if "x ∈ {a..<c}" "y ∈ {d<..b}" for x y proof (cases "f x = f m ∨ f y = f m") case True then show ?thesis using ‹⋀x. x ∈ {a..<c} ⟹ f x ≠ f m› that by auto next case False have False if "f x = f y" proof - have "x ≤ m" "m ≤ y" using ‹c ≤ m› ‹x ∈ {a..<c}› ‹m ≤ d› ‹y ∈ {d<..b}› by auto then have "x ∈ ({0..1} ∩ f -` {f y})" "y ∈ ({0..1} ∩ f -` {f y})" using ‹x ∈ {a..<c}› ‹y ∈ {d<..b}› ab01 by (auto simp: that) then have "m ∈ ({0..1} ∩ f -` {f y})" by (meson ‹m ≤ y› ‹x ≤ m› is_interval_connected_1 conn [of "f y"] is_interval_1) with False show False by auto qed then show ?thesis by auto qed qed qed then obtain leftcut rightcut where LR: "⋀a b m. ⟦m ∈ {a..b}; {a..b} ⊆ {0..1}⟧ ⟹ (a ≤ leftcut a b m ∧ leftcut a b m ≤ m ∧ m ≤ rightcut a b m ∧ rightcut a b m ≤ b ∧ (∀x ∈ {leftcut a b m..rightcut a b m}. f x = f m) ∧ (∀x ∈ {a..<leftcut a b m}. f x ≠ f m) ∧ (∀x ∈ {rightcut a b m<..b}. f x ≠ f m) ∧ (∀x ∈ {a..<leftcut a b m}. ∀y ∈ {rightcut a b m<..b}. f x ≠ f y))" apply atomize apply (clarsimp simp only: imp_conjL [symmetric] choice_iff choice_iff') apply (rule that, blast) done then have left_right: "⋀a b m. ⟦m ∈ {a..b}; {a..b} ⊆ {0..1}⟧ ⟹ a ≤ leftcut a b m ∧ rightcut a b m ≤ b" and left_right_m: "⋀a b m. ⟦m ∈ {a..b}; {a..b} ⊆ {0..1}⟧ ⟹ leftcut a b m ≤ m ∧ m ≤ rightcut a b m" by auto have left_neq: "⟦a ≤ x; x < leftcut a b m; a ≤ m; m ≤ b; {a..b} ⊆ {0..1}⟧ ⟹ f x ≠ f m" and right_neq: "⟦rightcut a b m < x; x ≤ b; a ≤ m; m ≤ b; {a..b} ⊆ {0..1}⟧ ⟹ f x ≠ f m" and left_right_neq: "⟦a ≤ x; x < leftcut a b m; rightcut a b m < y; y ≤ b; a ≤ m; m ≤ b; {a..b} ⊆ {0..1}⟧ ⟹ f x ≠ f m" and feqm: "⟦leftcut a b m ≤ x; x ≤ rightcut a b m; a ≤ m; m ≤ b; {a..b} ⊆ {0..1}⟧ ⟹ f x = f m" for a b m x y by (meson atLeastAtMost_iff greaterThanAtMost_iff atLeastLessThan_iff LR)+ have f_eqI: "⋀a b m x y. ⟦leftcut a b m ≤ x; x ≤ rightcut a b m; leftcut a b m ≤ y; y ≤ rightcut a b m; a ≤ m; m ≤ b; {a..b} ⊆ {0..1}⟧ ⟹ f x = f y" by (metis feqm) define u where "u ≡ rightcut 0 1 0" have lc[simp]: "leftcut 0 1 0 = 0" and u01: "0 ≤ u" "u ≤ 1" using LR [of 0 0 1] by (auto simp: u_def) have f0u: "⋀x. x ∈ {0..u} ⟹ f x = f 0" using LR [of 0 0 1] unfolding u_def [symmetric] by (metis ‹leftcut 0 1 0 = 0› atLeastAtMost_iff order_refl zero_le_one) have fu1: "⋀x. x ∈ {u<..1} ⟹ f x ≠ f 0" using LR [of 0 0 1] unfolding u_def [symmetric] by fastforce define v where "v ≡ leftcut u 1 1" have rc[simp]: "rightcut u 1 1 = 1" and v01: "u ≤ v" "v ≤ 1" using LR [of 1 u 1] u01 by (auto simp: v_def) have fuv: "⋀x. x ∈ {u..<v} ⟹ f x ≠ f 1" using LR [of 1 u 1] u01 v_def by fastforce have f0v: "⋀x. x ∈ {0..<v} ⟹ f x ≠ f 1" by (metis f_1not0 atLeastAtMost_iff atLeastLessThan_iff f0u fuv linear) have fv1: "⋀x. x ∈ {v..1} ⟹ f x = f 1" using LR [of 1 u 1] u01 v_def by (metis atLeastAtMost_iff atLeastatMost_subset_iff order_refl rc) define a where "a ≡ leftrec u v leftcut rightcut" define b where "b ≡ rightrec u v leftcut rightcut" define c where "c ≡ λx. midpoint (a x) (b x)" have a_real [simp]: "a (real j) = u" for j using a_def leftrec_base by (metis nonzero_mult_div_cancel_right of_nat_mult of_nat_numeral zero_neq_numeral) have b_real [simp]: "b (real j) = v" for j using b_def rightrec_base by (metis nonzero_mult_div_cancel_right of_nat_mult of_nat_numeral zero_neq_numeral) have a41: "a ((4 * real m + 1) / 2^Suc n) = a ((2 * real m + 1) / 2^n)" if "n > 0" for m n using that a_def leftrec_41 by blast have b41: "b ((4 * real m + 1) / 2^Suc n) = leftcut (a ((2 * real m + 1) / 2^n)) (b ((2 * real m + 1) / 2^n)) (c ((2 * real m + 1) / 2^n))" if "n > 0" for m n using that a_def b_def c_def rightrec_41 by blast have a43: "a ((4 * real m + 3) / 2^Suc n) = rightcut (a ((2 * real m + 1) / 2^n)) (b ((2 * real m + 1) / 2^n)) (c ((2 * real m + 1) / 2^n))" if "n > 0" for m n using that a_def b_def c_def leftrec_43 by blast have b43: "b ((4 * real m + 3) / 2^Suc n) = b ((2 * real m + 1) / 2^n)" if "n > 0" for m n using that b_def rightrec_43 by blast have uabv: "u ≤ a (real m / 2 ^ n) ∧ a (real m / 2 ^ n) ≤ b (real m / 2 ^ n) ∧ b (real m / 2 ^ n) ≤ v" for m n proof (induction n arbitrary: m) case 0 then show ?case by (simp add: v01) next case (Suc n p) show ?case proof (cases "even p") case True then obtain m where "p = 2*m" by (metis evenE) then show ?thesis by (simp add: Suc.IH) next case False then obtain m where m: "p = 2*m + 1" by (metis oddE) show ?thesis proof (cases n) case 0 then show ?thesis by (simp add: a_def b_def leftrec_base rightrec_base v01) next case (Suc n') then have "n > 0" by simp have a_le_c: "a (real m / 2^n) ≤ c (real m / 2^n)" for m unfolding c_def by (metis Suc.IH ge_midpoint_1) have c_le_b: "c (real m / 2^n) ≤ b (real m / 2^n)" for m unfolding c_def by (metis Suc.IH le_midpoint_1) have c_ge_u: "c (real m / 2^n) ≥ u" for m using Suc.IH a_le_c order_trans by blast have c_le_v: "c (real m / 2^n) ≤ v" for m using Suc.IH c_le_b order_trans by blast have a_ge_0: "0 ≤ a (real m / 2^n)" for m using Suc.IH order_trans u01(1) by blast have b_le_1: "b (real m / 2^n) ≤ 1" for m using Suc.IH order_trans v01(2) by blast have left_le: "leftcut (a ((real m) / 2^n)) (b ((real m) / 2^n)) (c ((real m) / 2^n)) ≤ c ((real m) / 2^n)" for m by (simp add: LR a_ge_0 a_le_c b_le_1 c_le_b) have right_ge: "rightcut (a ((real m) / 2^n)) (b ((real m) / 2^n)) (c ((real m) / 2^n)) ≥ c ((real m) / 2^n)" for m by (simp add: LR a_ge_0 a_le_c b_le_1 c_le_b) show ?thesis proof (cases "even m") case True then obtain r where r: "m = 2*r" by (metis evenE) show ?thesis using order_trans [OF left_le c_le_v, of "1+2*r"] Suc.IH [of "m+1"] using a_le_c [of "m+1"] c_le_b [of "m+1"] a_ge_0 [of "m+1"] b_le_1 [of "m+1"] left_right ‹n > 0› by (simp_all add: r m add.commute [of 1] a41 b41 del: power_Suc) next case False then obtain r where r: "m = 2*r + 1" by (metis oddE) show ?thesis using order_trans [OF c_ge_u right_ge, of "1+2*r"] Suc.IH [of "m"] using a_le_c [of "m"] c_le_b [of "m"] a_ge_0 [of "m"] b_le_1 [of "m"] left_right ‹n > 0› apply (simp_all add: r m add.commute [of 3] a43 b43 del: power_Suc) by (simp add: add.commute) qed qed qed qed have a_ge_0 [simp]: "0 ≤ a(m / 2^n)" and b_le_1 [simp]: "b(m / 2^n) ≤ 1" for m::nat and n using uabv order_trans u01 v01 by blast+ then have b_ge_0 [simp]: "0 ≤ b(m / 2^n)" and a_le_1 [simp]: "a(m / 2^n) ≤ 1" for m::nat and n using uabv order_trans by blast+ have alec [simp]: "a(m / 2^n) ≤ c(m / 2^n)" and cleb [simp]: "c(m / 2^n) ≤ b(m / 2^n)" for m::nat and n by (auto simp: c_def ge_midpoint_1 le_midpoint_1 uabv) have c_ge_0 [simp]: "0 ≤ c(m / 2^n)" and c_le_1 [simp]: "c(m / 2^n) ≤ 1" for m::nat and n using a_ge_0 alec b_le_1 cleb order_trans by blast+ have "⟦d = m-n; odd j; ¦real i / 2^m - real j / 2^n¦ < 1/2 ^ n⟧ ⟹ (a(j / 2^n)) ≤ (c(i / 2^m)) ∧ (c(i / 2^m)) ≤ (b(j / 2^n))" for d i j m n proof (induction d arbitrary: j n rule: less_induct) case (less d j n) show ?case proof (cases "m ≤ n") case True have "¦2^n¦ * ¦real i / 2^m - real j / 2^n¦ = 0" proof (rule Ints_nonzero_abs_less1) have "(real i * 2^n - real j * 2^m) / 2^m = (real i * 2^n) / 2^m - (real j * 2^m) / 2^m" using diff_divide_distrib by blast also have "... = (real i * 2 ^ (n-m)) - (real j)" using True by (auto simp: power_diff field_simps) also have "... ∈ ℤ" by simp finally have "(real i * 2^n - real j * 2^m) / 2^m ∈ ℤ" . with True Ints_abs show "¦2^n¦ * ¦real i / 2^m - real j / 2^n¦ ∈ ℤ" by (fastforce simp: field_split_simps) show "¦¦2^n¦ * ¦real i / 2^m - real j / 2^n¦¦ < 1" using less.prems by (auto simp: field_split_simps) qed then have "real i / 2^m = real j / 2^n" by auto then show ?thesis by auto next case False then have "n < m" by auto obtain k where k: "j = Suc (2*k)" using ‹odd j› oddE by fastforce show ?thesis proof (cases "n > 0") case False then have "a (real j / 2^n) = u" by simp also have "... ≤ c (real i / 2^m)" using alec uabv by (blast intro: order_trans) finally have ac: "a (real j / 2^n) ≤ c (real i / 2^m)" . have "c (real i / 2^m) ≤ v" using cleb uabv by (blast intro: order_trans) also have "... = b (real j / 2^n)" using False by simp finally show ?thesis by (auto simp: ac) next case True show ?thesis proof (cases "i / 2^m" "j / 2^n" rule: linorder_cases) case less moreover have "real (4 * k + 1) / 2 ^ Suc n + 1 / (2 ^ Suc n) = real j / 2 ^ n" using k by (force simp: field_split_simps) moreover have "¦real i / 2 ^ m - j / 2 ^ n¦ < 2 / (2 ^ Suc n)" using less.prems by simp ultimately have closer: "¦real i / 2 ^ m - real (4 * k + 1) / 2 ^ Suc n¦ < 1 / (2 ^ Suc n)" using less.prems by linarith have "a (real (4 * k + 1) / 2 ^ Suc n) ≤ c (i / 2 ^ m) ∧ c (real i / 2 ^ m) ≤ b (real (4 * k + 1) / 2 ^ Suc n)" proof (rule less.IH [OF _ refl]) show "m - Suc n < d" using ‹n < m› diff_less_mono2 less.prems(1) lessI by presburger show "¦real i / 2 ^ m - real (4 * k + 1) / 2 ^ Suc n¦ < 1 / 2 ^ Suc n" using closer ‹n < m› ‹d = m - n› by (auto simp: field_split_simps ‹n < m› diff_less_mono2) qed auto then show ?thesis using LR [of "c((2*k + 1) / 2^n)" "a((2*k + 1) / 2^n)" "b((2*k + 1) / 2^n)"] using alec [of "2*k+1"] cleb [of "2*k+1"] a_ge_0 [of "2*k+1"] b_le_1 [of "2*k+1"] using k a41 b41 ‹0 < n› by (simp add: add.commute) next case equal then show ?thesis by simp next case greater moreover have "real (4 * k + 3) / 2 ^ Suc n - 1 / (2 ^ Suc n) = real j / 2 ^ n" using k by (force simp: field_split_simps) moreover have "¦real i / 2 ^ m - real j / 2 ^ n¦ < 2 * 1 / (2 ^ Suc n)" using less.prems by simp ultimately have closer: "¦real i / 2 ^ m - real (4 * k + 3) / 2 ^ Suc n¦ < 1 / (2 ^ Suc n)" using less.prems by linarith have "a (real (4 * k + 3) / 2 ^ Suc n) ≤ c (real i / 2 ^ m) ∧ c (real i / 2 ^ m) ≤ b (real (4 * k + 3) / 2 ^ Suc n)" proof (rule less.IH [OF _ refl]) show "m - Suc n < d" using ‹n < m› diff_less_mono2 less.prems(1) by blast show "¦real i / 2 ^ m - real (4 * k + 3) / 2 ^ Suc n¦ < 1 / 2 ^ Suc n" using closer ‹n < m› ‹d = m - n› by (auto simp: field_split_simps ‹n < m› diff_less_mono2) qed auto then show ?thesis using LR [of "c((2*k + 1) / 2^n)" "a((2*k + 1) / 2^n)" "b((2*k + 1) / 2^n)"] using alec [of "2*k+1"] cleb [of "2*k+1"] a_ge_0 [of "2*k+1"] b_le_1 [of "2*k+1"] using k a43 b43 ‹0 < n› by (simp add: add.commute) qed qed qed qed then have aj_le_ci: