--- a/src/HOL/Analysis/Arcwise_Connected.thy Fri Oct 30 18:49:01 2020 +0000
+++ b/src/HOL/Analysis/Arcwise_Connected.thy Sat Oct 31 21:18:31 2020 +0000
@@ -16,9 +16,8 @@
lemma segment_to_closest_point:
fixes S :: "'a :: euclidean_space set"
shows "\<lbrakk>closed S; S \<noteq> {}\<rbrakk> \<Longrightarrow> open_segment a (closest_point S a) \<inter> S = {}"
- apply (subst disjoint_iff_not_equal)
- apply (clarify dest!: dist_in_open_segment)
- by (metis closest_point_le dist_commute le_less_trans less_irrefl)
+ 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"
@@ -110,10 +109,7 @@
show "\<Inter>(F ` UNIV) \<noteq> {} \<and> \<Inter>(F ` UNIV) \<subseteq> S \<and> \<phi> (\<Inter>(F ` UNIV))"
proof (intro conjI)
show "\<Inter>(F ` UNIV) \<noteq> {}"
- apply (rule compact_nest)
- apply (meson F cloF \<open>compact S\<close> seq_compact_closed_subset seq_compact_eq_compact)
- apply (simp add: F)
- by (meson Fsub lift_Suc_antimono_le)
+ by (metis F Fsub \<open>compact S\<close> cloF closed_Int_compact compact_nest inf.orderE lift_Suc_antimono_le)
show " \<Inter>(F ` UNIV) \<subseteq> S"
using F by blast
show "\<phi> (\<Inter>(F ` UNIV))"
@@ -160,12 +156,9 @@
also have "... = e"
by simp
finally have "dist (\<Sum>i\<in>Basis. (\<lfloor>2^k*(x \<bullet> i)\<rfloor> / 2^k) *\<^sub>R i) x < e" .
- then
+ with Ints_of_int
show "\<exists>k. \<exists>f \<in> Basis \<rightarrow> \<int>. dist (\<Sum>b\<in>Basis. (f b / 2^k) *\<^sub>R b) x < e"
- apply (rule_tac x=k in exI)
- apply (rule_tac x="\<lambda>i. of_int (floor (2^k*(x \<bullet> i)))" in bexI)
- apply auto
- done
+ by fastforce
qed
then show ?thesis by auto
qed
@@ -223,8 +216,7 @@
definition\<^marker>\<open>tag unimportant\<close> dyadics :: "'a::field_char_0 set" where "dyadics \<equiv> \<Union>k m. {of_nat m / 2^k}"
lemma real_in_dyadics [simp]: "real m \<in> dyadics"
- apply (simp add: dyadics_def)
- by (metis divide_numeral_1 numeral_One power_0)
+ by (simp add: dyadics_def) (metis divide_numeral_1 numeral_One power_0)
lemma nat_neq_4k1: "of_nat m \<noteq> (4 * of_nat k + 1) / (2 * 2^n :: 'a::field_char_0)"
proof
@@ -264,8 +256,8 @@
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
+ 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
}
@@ -353,13 +345,14 @@
apply (rule dyadic_413_cases, force+)
done
next
- show "?rhs \<subseteq> 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)
+ have "range of_nat \<subseteq> (\<Union>k m. {(of_nat m::'a) / 2 ^ k})"
+ by clarsimp (metis divide_numeral_1 numeral_One power_0)
+ moreover have "\<And>k m. \<exists>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 "\<And>k m. \<exists>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 \<subseteq> dyadics"
+ by (auto simp: dyadics_def Nats_def)
qed
@@ -369,9 +362,8 @@
| "dyad_rec b l r ((4 * real m + 3) / 2 ^ (Suc n)) = r (dyad_rec b l r ((2*m + 1) / 2^n))"
| "x \<notin> dyadics \<Longrightarrow> 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
+ 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 = (\<Union>K. \<Union>k<K. \<Union> m. {of_nat m / 2^k})"
unfolding dyadics_def by auto
@@ -452,13 +444,16 @@
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)
-
+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))"
- apply (rule dyad_rec.psimps)
- by (metis dyad_rec_level_termination lessI of_nat_add of_nat_mult of_nat_numeral)
+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"
@@ -509,17 +504,15 @@
by (simp add: dyad_rec2_def)
lemma leftrec_41: "n > 0 \<Longrightarrow> 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
+ unfolding dyad_rec2_def dyad_rec_41_times2
+ by (simp add: case_prod_beta)
lemma leftrec_43: "n > 0 \<Longrightarrow>
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
+ 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)
@@ -528,14 +521,12 @@
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
+ unfolding dyad_rec2_def dyad_rec_41_times2
+ by (simp add: case_prod_beta)
lemma rightrec_43: "n > 0 \<Longrightarrow> 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
+ unfolding dyad_rec2_def dyad_rec_43_times2
+ by (simp add: case_prod_beta)
lemma dyadics_in_open_unit_interval:
"{0<..<1} \<inter> (\<Union>k m. {real m / 2^k}) = (\<Union>k. \<Union>m \<in> {0<..<2^k}. {real m / 2^k})"
@@ -565,8 +556,8 @@
with that have "m \<in> cbox c0 d0"
by auto
obtain c d where cd: "{a..b} \<inter> f -` {f m} = {c..d}"
- apply (rule_tac c="max a c0" and d="min b d0" in that)
- using ab01 cd0 by auto
+ using ab01 cd0
+ by (rule_tac c="max a c0" and d="min b d0" in that) auto
then have cdab: "{c..d} \<subseteq> {a..b}"
by blast
show ?thesis
@@ -614,7 +605,7 @@
apply (rule that, blast)
done
then have left_right: "\<And>a b m. \<lbrakk>m \<in> {a..b}; {a..b} \<subseteq> {0..1}\<rbrakk> \<Longrightarrow> a \<le> leftcut a b m \<and> rightcut a b m \<le> b"
- and left_right_m: "\<And>a b m. \<lbrakk>m \<in> {a..b}; {a..b} \<subseteq> {0..1}\<rbrakk> \<Longrightarrow> leftcut a b m \<le> m \<and> m \<le> rightcut a b m"
+ and left_right_m: "\<And>a b m. \<lbrakk>m \<in> {a..b}; {a..b} \<subseteq> {0..1}\<rbrakk> \<Longrightarrow> leftcut a b m \<le> m \<and> m \<le> rightcut a b m"
by auto
have left_neq: "\<lbrakk>a \<le> x; x < leftcut a b m; a \<le> m; m \<le> b; {a..b} \<subseteq> {0..1}\<rbrakk> \<Longrightarrow> f x \<noteq> f m"
and right_neq: "\<lbrakk>rightcut a b m < x; x \<le> b; a \<le> m; m \<le> b; {a..b} \<subseteq> {0..1}\<rbrakk> \<Longrightarrow> f x \<noteq> f m"
@@ -709,24 +700,17 @@
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] \<open>n > 0\<close> 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)
+ 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 \<open>n > 0\<close>
+ 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 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] \<open>n > 0\<close> 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
+ 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 \<open>n > 0\<close>
+ apply (simp_all add: r m add.commute [of 3] a43 b43 del: power_Suc)
+ by (simp add: add.commute)
qed
qed
qed
@@ -738,8 +722,7 @@
have alec [simp]: "a(m / 2^n) \<le> c(m / 2^n)" and cleb [simp]: "c(m / 2^n) \<le> 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 \<le> c(m / 2^n)" and c_le_1 [simp]: "c(m / 2^n) \<le> 1" for m::nat and n
- using a_ge_0 alec order_trans apply blast
- by (meson b_le_1 cleb order_trans)
+ using a_ge_0 alec b_le_1 cleb order_trans by blast+
have "\<lbrakk>d = m-n; odd j; \<bar>real i / 2^m - real j / 2^n\<bar> < 1/2 ^ n\<rbrakk>
\<Longrightarrow> (a(j / 2^n)) \<le> (c(i / 2^m)) \<and> (c(i / 2^m)) \<le> (b(j / 2^n))" for d i j m n
proof (induction d arbitrary: j n rule: less_induct)
@@ -786,25 +769,27 @@
by (auto simp: ac)
next
case True show ?thesis
- proof (cases "real i / 2^m" "real j / 2^n" rule: linorder_cases)
+ 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 "\<bar>real i / 2 ^ m - real j / 2 ^ n\<bar> < 2 / (2 ^ Suc n)"
+ moreover have "\<bar>real i / 2 ^ m - j / 2 ^ n\<bar> < 2 / (2 ^ Suc n)"
using less.prems by simp
ultimately have closer: "\<bar>real i / 2 ^ m - real (4 * k + 1) / 2 ^ Suc n\<bar> < 1 / (2 ^ Suc n)"
using less.prems by linarith
- have *: "a (real (4 * k + 1) / 2 ^ Suc n) \<le> c (real i / 2 ^ m) \<and>
+ have "a (real (4 * k + 1) / 2 ^ Suc n) \<le> c (i / 2 ^ m) \<and>
c (real i / 2 ^ m) \<le> b (real (4 * k + 1) / 2 ^ Suc n)"
- apply (rule less.IH [OF _ refl])
- using closer \<open>n < m\<close> \<open>d = m - n\<close> apply (auto simp: field_split_simps \<open>n < m\<close> diff_less_mono2)
- done
- show ?thesis
+ proof (rule less.IH [OF _ refl])
+ show "m - Suc n < d"
+ using \<open>n < m\<close> diff_less_mono2 less.prems(1) lessI by presburger
+ show "\<bar>real i / 2 ^ m - real (4 * k + 1) / 2 ^ Suc n\<bar> < 1 / 2 ^ Suc n"
+ using closer \<open>n < m\<close> \<open>d = m - n\<close> by (auto simp: field_split_simps \<open>n < m\<close> 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 * \<open>0 < n\<close>
- apply (simp add: add.commute)
- done
+ using k a41 b41 \<open>0 < n\<close>
+ by (simp add: add.commute)
next
case equal then show ?thesis by simp
next
@@ -815,17 +800,19 @@
using less.prems by simp
ultimately have closer: "\<bar>real i / 2 ^ m - real (4 * k + 3) / 2 ^ Suc n\<bar> < 1 / (2 ^ Suc n)"
using less.prems by linarith
- have *: "a (real (4 * k + 3) / 2 ^ Suc n) \<le> c (real i / 2 ^ m) \<and>
+ have "a (real (4 * k + 3) / 2 ^ Suc n) \<le> c (real i / 2 ^ m) \<and>
c (real i / 2 ^ m) \<le> b (real (4 * k + 3) / 2 ^ Suc n)"
- apply (rule less.IH [OF _ refl])
- using closer \<open>n < m\<close> \<open>d = m - n\<close> apply (auto simp: field_split_simps \<open>n < m\<close> diff_less_mono2)
- done
- show ?thesis
+ proof (rule less.IH [OF _ refl])
+ show "m - Suc n < d"
+ using \<open>n < m\<close> diff_less_mono2 less.prems(1) by blast
+ show "\<bar>real i / 2 ^ m - real (4 * k + 3) / 2 ^ Suc n\<bar> < 1 / 2 ^ Suc n"
+ using closer \<open>n < m\<close> \<open>d = m - n\<close> by (auto simp: field_split_simps \<open>n < m\<close> 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 * \<open>0 < n\<close>
- apply (simp add: add.commute)
- done
+ using k a43 b43 \<open>0 < n\<close>
+ by (simp add: add.commute)
qed
qed
qed
@@ -912,9 +899,7 @@
with \<open>0 < j\<close> have "k > 0" "2 * k < 2 ^ n"
using Suc.prems(2) k by auto
with k \<open>0 < n\<close> Suc.IH [of k] show ?thesis
- apply (simp add: m1_to_3 a41 b43 del: power_Suc)
- apply (subst of_nat_diff, auto)
- done
+ by (simp add: m1_to_3 a41 b43 del: power_Suc) (auto simp: of_nat_diff)
next
case False
then obtain k where k: "j = 2*k + 1" by (metis oddE)
@@ -924,8 +909,7 @@
= 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
+ by (auto simp: add.commute feqm [OF order_refl] feqm [OF _ order_refl, symmetric])
then
show ?thesis
by (simp add: k add.commute [of 1] add.commute [of 3] a43 b41\<open>0 < n\<close> del: power_Suc)
@@ -951,9 +935,7 @@
by auto
then show ?thesis
using Suc.IH [of k] k \<open>0 < k\<close>
- apply (simp add: less2n add.commute [of 1] m1_to_3 a41 b43 del: power_Suc)
- apply (auto simp: of_nat_diff)
- done
+ by (simp add: less2n add.commute [of 1] m1_to_3 a41 b43 del: power_Suc) (auto simp: of_nat_diff)
next
case False
then obtain k where k: "j = 2*k + 1" by (metis oddE)
@@ -1057,8 +1039,7 @@
show thesis
proof
show "(1::nat) < 2 ^ n"
- apply (subst one_less_power)
- using \<open>n > 0\<close> by auto
+ by (metis Suc_1 \<open>0 < n\<close> lessI one_less_power)
show "\<bar>real i / 2 ^ m - real 1/2 ^ n\<bar> < 1/2 ^ n"
using i less_j1 by (simp add: dist_norm field_simps True)
show "\<bar>real k / 2 ^ p - real 1/2 ^ n\<bar> < 1/2 ^ n"
@@ -1109,35 +1090,34 @@
qed
show ?thesis
proof
- have "real j < 2 ^ n"
- using j_le i k
- apply (auto simp: le_max_iff_disj simp del: of_nat_less_numeral_power_cancel_iff
- elim!: le_less_trans)
- apply (auto simp: field_simps)
- done
+ have "2 ^ n * real i / 2 ^ m < 2 ^ n" "2 ^ n * real k / 2 ^ p < 2 ^ n"
+ using i k by (auto simp: field_simps)
+ then have "max (2^n * i / 2^m) (2^n * k / 2^p) < 2^n"
+ by simp
+ with j_le have "real j < 2 ^ n" by linarith
then show "j < 2 ^ n"
by auto
- show "\<bar>real i / 2 ^ m - real j / 2 ^ n\<bar> < 1/2 ^ n"
+ have "\<bar>real i * 2 ^ n - real j * 2 ^ m\<bar> < 2 ^ m"
using clo less_j1 j_le
- apply (auto simp: le_max_iff_disj field_split_simps dist_norm)
- apply (auto simp: algebra_simps abs_if split: if_split_asm dest: 1 2)
- done
- show "\<bar>real k / 2 ^ p - real j / 2 ^ n\<bar> < 1/2 ^ n"
- using clo less_j1 j_le
- apply (auto simp: le_max_iff_disj field_split_simps dist_norm)
- apply (auto simp: algebra_simps not_less abs_if split: if_split_asm dest: 3 2)
- done
+ by (auto simp: le_max_iff_disj field_split_simps dist_norm abs_if split: if_split_asm dest: 1 2)
+ then show "\<bar>real i / 2 ^ m - real j / 2 ^ n\<bar> < 1/2 ^ n"
+ by (auto simp: field_split_simps)
+ have "\<bar>real k * 2 ^ n - real j * 2 ^ p\<bar> < 2 ^ p"
+ using clo less_j1 j_le
+ by (auto simp: le_max_iff_disj field_split_simps dist_norm abs_if split: if_split_asm dest: 3 2)
+ then show "\<bar>real k / 2 ^ p - real j / 2 ^ n\<bar> < 1/2 ^ n"
+ by (auto simp: le_max_iff_disj field_split_simps dist_norm)
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 \<open>0 < j\<close> \<open>j < 2 ^ n\<close> k clo_kj by auto
+ using \<open>0 < j\<close> \<open>j < 2 ^ n\<close> k clo_kj
+ by (intro dist_fc_close) auto
show "dist (f (c (real i / 2 ^ m))) (f (c (real j / 2 ^ n))) < e/2"
- apply (rule dist_fc_close)
- using \<open>0 < j\<close> \<open>j < 2 ^ n\<close> i clo_ij by auto
+ using \<open>0 < j\<close> \<open>j < 2 ^ n\<close> i clo_ij
+ by (intro dist_fc_close) auto
qed
qed
qed
@@ -1191,8 +1171,7 @@
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
+ using uabv [of 1 1] f0u [of u] f0u [of x] by force
next
case 2
then show ?thesis
@@ -1200,8 +1179,7 @@
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
+ using uabv [of 1 1] fv1 [of v] fv1 [of x] by force
qed
with \<open>n=0\<close> show ?thesis
by (rule_tac x=1 in exI) auto
@@ -1212,6 +1190,9 @@
and y: "y \<in> {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)
+ have j4: "4 * j + 1 < 2 ^ Suc n"
+ using mless j by (simp add: algebra_simps)
+
consider "y \<in> {a((2*j + 1) / 2^n) .. b((4*j + 1) / 2 ^ (Suc n))}"
| "y \<in> {b((4*j + 1) / 2 ^ (Suc n)) .. a((4*j + 3) / 2 ^ (Suc n))}"
| "y \<in> {a((4*j + 3) / 2 ^ (Suc n)) .. b((2*j + 1) / 2^n)}"
@@ -1219,33 +1200,35 @@
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 \<open>n \<noteq> 0\<close>
- apply (simp add: feq a41 b41 add.commute [of 1] del: power_Suc)
- apply (simp add: algebra_simps)
- done
+ show ?thesis
+ proof (intro exI conjI)
+ show "y \<in> {a (real (4 * j + 1) / 2 ^ Suc n)..b (real (4 * j + 1) / 2 ^ Suc n)}"
+ using mless j \<open>n \<noteq> 0\<close> 1 by (simp add: a41 b41 add.commute [of 1] del: power_Suc)
+ qed (use feq j4 in auto)
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 \<open>n \<noteq> 0\<close> 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
+ proof (intro exI conjI)
+ show "b (real (4 * j + 1) / 2 ^ Suc n) \<in> {a (real (4 * j + 1) / 2 ^ Suc n)..b (real (4 * j + 1) / 2 ^ Suc n)}"
+ using \<open>n \<noteq> 0\<close> 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)"]
+ by (simp add: a41 b41 add.commute [of 1] del: power_Suc)
+ show "f (b (real (4 * j + 1) / 2 ^ Suc n)) = f x"
+ using \<open>n \<noteq> 0\<close> 2
+ 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]
+ by (force simp add: b41 a43 add.commute [of 1] feq [symmetric] simp del: power_Suc intro: f_eqI)
+ qed (use j4 in auto)
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 \<open>n \<noteq> 0\<close>
- apply (simp add: feq a43 b43 del: power_Suc)
- apply (simp add: algebra_simps)
- done
+ show ?thesis
+ proof (intro exI conjI)
+ show "4 * j + 3 < 2 ^ Suc n"
+ using mless j by simp
+ show "f y = f x"
+ by fact
+ show "y \<in> {a (real (4 * j + 3) / 2 ^ Suc n) .. b (real (4 * j + 3) / 2 ^ Suc n)}"
+ using 3 False b43 [of n j] by (simp add: add.commute)
+ qed (use 3 in auto)
qed
qed
qed
@@ -1255,24 +1238,26 @@
by fastforce
with * obtain m::nat and y
where "odd m" "0 < m" and mless: "m < 2 ^ n"
- and y: "y \<in> {a(m / 2^n) .. b(m / 2^n)}" and feq: "f x = f y"
- by metis
+ and y: "a(m / 2^n) \<le> y \<and> y \<le> b(m / 2^n)" and feq: "f x = f y"
+ by (metis atLeastAtMost_iff)
then have "0 \<le> y" "y \<le> 1"
- by (metis atLeastAtMost_iff a_ge_0 b_le_1 order.trans)+
+ by (meson a_ge_0 b_le_1 order.trans)+
moreover have "y < \<delta> + c (real m / 2 ^ n)" "c (real m / 2 ^ n) < \<delta> + y"
- using y apply simp_all
- using alec [of m n] cleb [of m n] n field_sum_of_halves close_ab [OF \<open>odd m\<close>, of n]
+ using y alec [of m n] cleb [of m n] n field_sum_of_halves close_ab [OF \<open>odd m\<close>, of n]
by linarith+
moreover note \<open>0 < m\<close> mless \<open>0 \<le> x\<close> \<open>x \<le> 1\<close>
- ultimately show "\<exists>k. \<exists>m\<in>{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 \<delta>)
- done
+ ultimately have "dist (h (real m / 2 ^ n)) (f x) < e"
+ by (auto simp: dist_norm h_eq feq \<delta>)
+ then show "\<exists>k. \<exists>m\<in>{0<..<2 ^ k}. dist (h (real m / 2 ^ k)) (f x) < e"
+ using \<open>0 < m\<close> greaterThanLessThan_iff mless by blast
qed
also have "... \<subseteq> h ` {0..1}"
- apply (rule closure_minimal)
- using compact_continuous_image [OF cont_h] compact_imp_closed by (auto simp: D01_def)
+ proof (rule closure_minimal)
+ show "h ` D01 \<subseteq> h ` {0..1}"
+ using cloD01 closure_subset by blast
+ show "closed (h ` {0..1})"
+ using compact_continuous_image [OF cont_h] compact_imp_closed by auto
+ qed
finally show "f ` {0..1} \<subseteq> h ` {0..1}" .
qed
moreover have "inj_on h {0..1}"
@@ -1394,8 +1379,7 @@
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
+ using a_ge_0 [of m n] b_le_1 [of m n] by linarith+
have approx: "\<exists>j n. odd j \<and> n \<noteq> 0 \<and>
real i / 2^m \<le> real j / 2^n \<and>
real j / 2^n \<le> real k / 2^p \<and>
@@ -1423,7 +1407,7 @@
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' \<le> i"
+ have \<section>: False if "real i * 2 ^ p' < real k * 2 ^ m'" "k < 2 ^ p'" "2 ^ m' \<le> i"
proof -
have "real k * 2 ^ m' < 2 ^ p' * 2 ^ m'"
using that by simp
@@ -1431,11 +1415,13 @@
using that by linarith
with that show ?thesis by simp
qed
- then show ?thesis
+ moreover have *: "real i / 2 ^ m' < real k / 2^p'" "k < 2 ^ p'"
+ using less.prems \<open>m = Suc m'\<close> 2 Suc by (force simp: field_split_simps)+
+ moreover have "i < 2 ^ m' "
+ using \<section> * by (clarsimp simp: divide_simps linorder_not_le) (meson linorder_not_le)
+ ultimately show ?thesis
using less.IH [of "m'+p'" i m' k p'] less.prems \<open>m = Suc m'\<close> 2 Suc
- apply atomize
- apply (force simp: field_split_simps)
- done
+ by (force simp: field_split_simps)
qed
qed
next
@@ -1449,10 +1435,18 @@
case 0 with less.prems show ?thesis by auto
next
case (Suc p')
- then show ?thesis
+ have "real (i - 2 ^ m') / 2 ^ m' < real (k - 2 ^ p') / 2 ^ p'"
+ using less.prems \<open>m = Suc m'\<close> Suc 3 by (auto simp: field_simps of_nat_diff)
+ moreover have "k - 2 ^ p' < 2 ^ p'" "i - 2 ^ m' < 2 ^ m'"
+ using less.prems Suc \<open>m = Suc m'\<close> by auto
+ moreover
+ have "2 ^ p' \<le> k" "2 ^ p' \<noteq> k"
+ using less.prems \<open>m = Suc m'\<close> Suc 3 by auto
+ then have "2 ^ p' < k"
+ by linarith
+ ultimately show ?thesis
using less.IH [of "m'+p'" "i - 2^m'" m' "k - 2 ^ p'" p'] less.prems \<open>m = Suc m'\<close> Suc 3
- apply atomize
- apply (auto simp: field_simps of_nat_diff)
+ apply (clarsimp 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)
@@ -1476,15 +1470,10 @@
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 *: "\<lbrakk>i < q; abs(i - q) < s*2; q = r + s\<rbrakk> \<Longrightarrow> abs(i - r) < s" for i q s r::real
- by auto
- have "c(i / 2^m) \<le> 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: field_split_simps)
- done
+ with i_le_j clo_ij q have "\<bar>real i / 2 ^ m - real (4 * q + 1) / 2 ^ Suc n'\<bar> < 1 / 2 ^ Suc n'"
+ by (auto simp: field_split_simps)
+ then have "c(i / 2^m) \<le> b(real(4 * q + 1) / 2 ^ (Suc n'))"
+ by (meson ci_le_bj even_mult_iff even_numeral even_plus_one_iff)
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] \<open>n' \<noteq> 0\<close>
using left_right_m [of "c((2*q + 1) / 2^n')" "a((2*q + 1) / 2^n')" "b((2*q + 1) / 2^n')"]
@@ -1500,11 +1489,10 @@
by auto
have *: "\<lbrakk>q < i; abs(i - q) < s*2; r = q + s\<rbrakk> \<Longrightarrow> abs(i - r) < s" for i q s r::real
by auto
- have "a(real(4*q + 3) / 2 ^ (Suc n')) \<le> c(j / 2^n)"
- apply (rule aj_le_ci, force)
- apply (rule * [OF less])
- using j_le_j clo_jj q apply (auto simp: field_split_simps)
- done
+ have "\<bar>real j / 2 ^ n - real (4 * q + 3) / 2 ^ Suc n'\<bar> < 1 / 2 ^ Suc n'"
+ by (rule * [OF less]) (use j_le_j clo_jj q in \<open>auto simp: field_split_simps\<close>)
+ then have "a(real(4*q + 3) / 2 ^ (Suc n')) \<le> c(j / 2^n)"
+ by (metis Suc3_eq_add_3 add.commute aj_le_ci even_Suc even_mult_iff even_numeral)
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] \<open>n' \<noteq> 0\<close>
using left_right_m [of "c((2*q + 1) / 2^n')" "a((2*q + 1) / 2^n')" "b((2*q + 1) / 2^n')"]
@@ -1611,15 +1599,13 @@
using m by (auto simp: field_split_simps)
have closure0m: "{0..m / 2^n} = closure ({0<..< m / 2^n} \<inter> (\<Union>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} \<inter> (\<Union>k m. {real m / 2 ^ k}))"
- apply (subst closure_dyadic_rationals_in_convex_set_pos_1; simp add: not_le m)
- using \<open>0 < real m / 2 ^ n\<close> by linarith
+ have "2^n > m"
+ by (simp add: m(2) not_le)
+ then have closurem1: "{m / 2^n .. 1} = closure ({m / 2^n <..< 1} \<inter> (\<Union>k m. {real m / 2 ^ k}))"
+ using closure_dyadic_rationals_in_convex_set_pos_1 m_div(1) by fastforce
have cont_h': "continuous_on (closure ({u<..<v} \<inter> (\<Union>k m. {real m / 2 ^ k}))) h"
if "0 \<le> u" "v \<le> 1" for u v
- apply (rule continuous_on_subset [OF cont_h])
- apply (rule closure_minimal [OF subsetI])
- using that apply auto
- done
+ using that by (intro continuous_on_subset [OF cont_h] closure_minimal [OF subsetI]) auto
have closed_f': "closed (f ` {u..v})" if "0 \<le> u" "v \<le> 1" for u v
by (metis compact_continuous_image cont_f compact_interval atLeastatMost_subset_iff
compact_imp_closed continuous_on_subset that)
@@ -1629,20 +1615,18 @@
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: field_split_simps)
- apply (blast intro: p less_2I m_div less_trans)
- done
+ then have [simp]: "0 < p"
+ by (simp add: field_split_simps)
+ have [simp]: "p < 2 ^ q"
+ by (blast intro: p less_2I m_div less_trans)
have "f (c (real p / 2 ^ q)) \<in> f ` {0..c (real m / 2 ^ n)}"
by (auto simp: clec p m)
then show "h (real p / 2 ^ q) \<in> f ` {0..c (real m / 2 ^ n)}"
by (simp add: h_eq)
qed
- then have "h ` {0 .. m / 2^n} \<subseteq> f ` {0 .. c(m / 2^n)}"
+ with m_div have "h ` {0 .. m / 2^n} \<subseteq> 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
+ by (rule image_closure_subset [OF cont_h' closed_f']) auto
then have hx1: "h x1 \<in> f ` {0 .. c(m / 2^n)}"
using x12 less.prems(1) by auto
then obtain t1 where t1: "h x1 = f t1" "0 \<le> t1" "t1 \<le> c (m / 2 ^ n)"
@@ -1658,11 +1642,9 @@
then show "h (real p / 2 ^ q) \<in> f ` {c (real m / 2 ^ n)..1}"
by (simp add: h_eq)
qed
- then have "h ` {m / 2^n .. 1} \<subseteq> f ` {c(m / 2^n) .. 1}"
+ with m have "h ` {m / 2^n .. 1} \<subseteq> f ` {c(m / 2^n) .. 1}"
apply (subst closurem1)
- apply (rule image_closure_subset [OF cont_h' closed_f'])
- using m apply auto
- done
+ by (rule image_closure_subset [OF cont_h' closed_f']) auto
then have hx2: "h x2 \<in> 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) \<le> t2" "t2 \<le> 1"
@@ -1718,15 +1700,15 @@
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 \<in> {x<..<y}" and z: "z \<in> {x<..<y}"
+ define w where "w \<equiv> x + (min e (y - x) / 3)"
+ define z where "z \<equiv>y - (min e (y - x) / 3)"
+ have "w < z" and w: "w \<in> {x<..<y}" and z: "z \<in> {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 \<open>0 < e\<close> less by simp_all
+ using minxy \<open>0 < e\<close> less unfolding w_def z_def by auto
have Fclo: "\<And>T. T \<in> range F \<Longrightarrow> closed T"
by (metis \<open>\<And>n. closed (F n)\<close> image_iff)
have eq: "{w..z} \<inter> \<Inter>(F ` UNIV) = {}"
- 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)
+ using less w z by (simp add: open_segment_eq_real_ivl disjoint_iff)
then obtain K where "finite K" and K: "{w..z} \<inter> (\<Inter> (F ` K)) = {}"
by (metis finite_subset_image compact_imp_fip [OF compact_interval Fclo])
then have "K \<noteq> {}"
@@ -1752,8 +1734,7 @@
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)
+ by (auto simp add: disjoint_iff less_eq_real_def intro!: that)
qed
obtain v where v: "v \<in> F n" "v \<in> {z..y}" "({z..v} - {v}) \<inter> F n = {}"
proof (cases "z \<in> F n")
@@ -1771,9 +1752,10 @@
show "F n \<inter> {z..y} \<noteq> {}"
by (metis atLeastAtMost_iff disjoint_iff_not_equal greaterThanLessThan_iff less.prems(2) less_eq_real_def z)
show "\<And>b. \<lbrakk>b \<in> F n \<inter> {z..y}; open_segment z b \<inter> (F n \<inter> {z..y}) = {}\<rbrakk> \<Longrightarrow> 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)
+ proof
+ show "\<And>b. \<lbrakk>b \<in> F n \<inter> {z..y}; open_segment z b \<inter> (F n \<inter> {z..y}) = {}\<rbrakk> \<Longrightarrow> ({z..b} - {b}) \<inter> F n = {}"
+ using False by (auto simp: open_segment_eq_real_ivl less_eq_real_def)
+ qed auto
qed
qed
obtain u v where "u \<in> {0..1}" "v \<in> {0..1}" "norm(u - x) < e" "norm(v - y) < e" "p u = p v"
@@ -1807,8 +1789,7 @@
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)
+ by (metis dist_norm dist_triangle_half_r order_less_irrefl)
qed (auto simp: open_segment_commute)
show ?thesis
unfolding \<phi>_def by (metis (no_types, hide_lams) INT_I Inf_lower2 rangeI that(3) F01 subsetCE pqF)
@@ -1830,8 +1811,7 @@
have "insert x (open_segment x y \<union> open_segment x z) \<inter> T = {}"
by (metis False Int_Un_distrib2 Int_insert_left Un_empty_right xyT xzT)
moreover have "open_segment y z \<inter> T \<subseteq> insert x (open_segment x y \<union> open_segment x z) \<inter> T"
- apply auto
- by (metis greaterThanLessThan_iff less_eq_real_def less_le_trans linorder_neqE_linordered_idom open_segment_eq_real_ivl)
+ by (auto simp: open_segment_eq_real_ivl)
ultimately have "open_segment y z \<inter> T = {}"
by blast
with that peq show ?thesis by metis
@@ -1877,13 +1857,21 @@
have uvT: "closed (closed_segment u v \<inter> T)" "closed_segment u v \<inter> T \<noteq> {}"
using False open_closed_segment by (auto simp: \<open>closed T\<close> closed_Int)
obtain w where "w \<in> T" and w: "w \<in> closed_segment u v" "open_segment u w \<inter> 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)
+ proof (rule segment_to_point_exists [OF uvT])
+ fix b
+ assume "b \<in> closed_segment u v \<inter> T" "open_segment u b \<inter> (closed_segment u v \<inter> T) = {}"
+ then show thesis
+ by (metis IntD1 IntD2 ends_in_segment(1) inf.orderE inf_assoc subset_oc_segment that)
+ qed
then have puw: "dist (p u) (p w) < \<epsilon> / 2"
by (metis (no_types) \<open>T \<subseteq> {0..1}\<close> \<open>dist v u < \<delta>\<close> \<delta> dist_commute dist_in_closed_segment le_less_trans subsetCE)
obtain z where "z \<in> T" and z: "z \<in> closed_segment u v" "open_segment v z \<inter> 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)
+ proof (rule segment_to_point_exists [OF uvT])
+ fix b
+ assume "b \<in> closed_segment u v \<inter> T" "open_segment v b \<inter> (closed_segment u v \<inter> T) = {}"
+ then show thesis
+ by (metis IntD1 IntD2 ends_in_segment(2) inf.orderE inf_assoc subset_oc_segment that)
+ qed
then have "dist (p u) (p z) < \<epsilon> / 2"
by (metis \<open>T \<subseteq> {0..1}\<close> \<open>dist v u < \<delta>\<close> \<delta> dist_commute dist_in_closed_segment le_less_trans subsetCE)
then show ?thesis
@@ -2048,11 +2036,10 @@
with y \<open>r > 0\<close> obtain g where "arc g" and pig: "path_image g \<subseteq> ball z r"
and g: "pathstart g = y" "pathfinish g = z"
using \<open>y \<noteq> z\<close> by (force simp: path_connected_arcwise)
- have "compact (g -` frontier S \<inter> {0..1})"
- apply (simp add: compact_eq_bounded_closed bounded_Int)
- apply (rule closed_vimage_Int)
- using \<open>arc g\<close> apply (auto simp: arc_def path_def)
- done
+ have "continuous_on {0..1} g"
+ using \<open>arc g\<close> arc_imp_path path_def by blast
+ then have "compact (g -` frontier S \<inter> {0..1})"
+ by (simp add: bounded_Int closed_Diff closed_vimage_Int compact_eq_bounded_closed)
moreover have "g -` frontier S \<inter> {0..1} \<noteq> {}"
proof -
have "\<exists>r. r \<in> g -` frontier S \<and> r \<in> {0..1}"
@@ -2082,11 +2069,7 @@
then show "pathfinish (subpath 0 t g) \<in> 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 \<open>arc g\<close>]])
- using mult_le_one apply auto
- done
+ using t01 \<open>arc (subpath 0 t g)\<close> arc_imp_inj_on by blast
then have "subpath 0 t g ` {0..<1} \<subseteq> 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 \<noteq> {}"
@@ -2096,11 +2079,10 @@
have "subpath 0 t g ` {0..<1} \<inter> frontier S \<noteq> {}"
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: \<open>0 \<le> t\<close> \<open>t \<le> 1\<close> mult_le_one)
- done
+ proof (rule connected_continuous_image)
+ show "continuous_on {0..<1} (subpath 0 t g)"
+ by (meson \<open>arc (subpath 0 t g)\<close> arc_def atLeastLessThan_subseteq_atLeastAtMost_iff continuous_on_subset order_refl path_def)
+ qed auto
show "subpath 0 t g ` {0..<1} \<inter> S \<noteq> {}"
using \<open>y \<in> S\<close> g(1) by (force simp: subpath_def image_def pathstart_def)
qed
@@ -2139,17 +2121,18 @@
by (simp add: \<open>arc g\<close> arc_imp_path)
then obtain h where "arc h"
and h: "path_image h \<subseteq> path_image (f +++ g)" "pathstart h = x" "pathfinish h = pathfinish g"
- apply (rule path_contains_arc [of "f +++ g" x "pathfinish g"])
- using f \<open>x \<notin> V\<close> \<open>pathfinish g \<in> V\<close> by auto
- have "h ` {0..1} - {h 1} \<subseteq> S"
- using f g h apply (clarsimp simp: path_image_join)
+ using path_contains_arc [of "f +++ g" x "pathfinish g"] \<open>x \<notin> V\<close> \<open>pathfinish g \<in> V\<close> f
+ by (metis pathfinish_join pathstart_join)
+ have "path_image h \<subseteq> path_image f \<union> path_image g"
+ using h(1) path_image_join_subset by auto
+ then have "h ` {0..1} - {h 1} \<subseteq> S"
+ using f g h
apply (simp add: path_image_def pathfinish_def subset_iff image_def Bex_def)
by (metis le_less)
then have "h ` {0..<1} \<subseteq> S"
using \<open>arc h\<close> by (force simp: arc_def dest: inj_onD)
then show thesis
- apply (rule that [OF \<open>arc h\<close>])
- using h \<open>pathfinish g \<in> V\<close> by auto
+ using \<open>arc h\<close> g(3) h that by presburger
qed
lemma dense_access_fp_aux:
@@ -2188,9 +2171,10 @@
proof
show "arc \<gamma>" "pathstart \<gamma> \<in> U" "pathfinish \<gamma> \<in> V"
using \<gamma> \<open>arc \<gamma>\<close> \<open>pathfinish h \<in> U - {pathfinish g}\<close> \<open>pathfinish g \<in> V\<close> by auto
- have "\<gamma> ` {0..1} - {\<gamma> 0, \<gamma> 1} \<subseteq> S"
- using \<gamma> g h
- apply (simp add: path_image_join)
+ have "path_image \<gamma> \<subseteq> path_image h \<union> path_image g"
+ by (metis \<gamma>(1) g(2) h(2) path_image_join path_image_reversepath pathfinish_reversepath)
+ then have "\<gamma> ` {0..1} - {\<gamma> 0, \<gamma> 1} \<subseteq> S"
+ using \<gamma> g h
apply (simp add: path_image_def pathstart_def pathfinish_def subset_iff image_def Bex_def)
by (metis linorder_neqE_linordered_idom not_less)
then show "\<gamma> ` {0<..<1} \<subseteq> S"