# HG changeset patch # User paulson # Date 1745356012 -3600 # Node ID ad31be996dcbfa3ec4c595177cc85e3042013955 # Parent 3dfd62b4e2c839e20dd1d067efb8455a27b203ea# Parent fadbfb9e65f32ead06fd1670adfb6b0a3bf3a1d9 merged diff -r 3dfd62b4e2c8 -r ad31be996dcb src/HOL/Analysis/Cartesian_Euclidean_Space.thy --- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy Tue Apr 22 19:02:33 2025 +0200 +++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy Tue Apr 22 22:06:52 2025 +0100 @@ -202,8 +202,8 @@ unfolding bounded_def apply clarify apply (rule_tac x="x $ i" in exI) - apply (rule_tac x="e" in exI) - apply clarify + apply (rule_tac x="\" in exI) + apply clarify apply (rule order_trans [OF dist_vec_nth_le], simp) done diff -r 3dfd62b4e2c8 -r ad31be996dcb src/HOL/Analysis/Cartesian_Space.thy --- a/src/HOL/Analysis/Cartesian_Space.thy Tue Apr 22 19:02:33 2025 +0200 +++ b/src/HOL/Analysis/Cartesian_Space.thy Tue Apr 22 22:06:52 2025 +0100 @@ -205,10 +205,13 @@ proof - have "\B x. A ** B = mat 1 \ \y. x = A *v y" by (metis matrix_vector_mul_assoc matrix_vector_mul_lid) - moreover have "\x. \xa. x = A *v xa \ \B. A ** B = mat 1" - by (metis (mono_tags, lifting) matrix_compose_gen matrix_id_mat_1 matrix_of_matrix_vector_mul surj_def vec.linear_axioms vec.linear_surjective_right_inverse) + moreover + have "\B. A ** B = mat 1" if "surj ((*v) A)" + by (metis (no_types, opaque_lifting) matrix_compose_gen matrix_id_mat_1 + matrix_of_matrix_vector_mul vec.linear_axioms + vec.linear_surjective_right_inverse that) ultimately show ?thesis - by (auto simp: image_def set_eq_iff) + by (auto simp: image_def set_eq_iff surj_def) qed lemma matrix_left_invertible_independent_columns: @@ -301,24 +304,27 @@ "(\(B::real^'m^'n). B ** (A::real^'n^'m) = mat 1) \ span (rows A) = UNIV" using matrix_left_invertible_span_rows_gen[of A] by (simp add: span_vec_eq) + +lemma matrix_left_right_inverse1: + fixes A A' :: "'a::{field}^'n^'n" + assumes AA': "A ** A' = mat 1" + shows "A' ** A = mat 1" +proof - + have sA: "surj ((*v) A)" + using AA' matrix_right_invertible_surjective by auto + obtain f' :: "'a ^'n \ 'a ^'n" + where f': "Vector_Spaces.linear (*s) (*s) f'" "\x. f' (A *v x) = x" "\x. A *v f' x = x" + using sA vec.linear_surjective_isomorphism by blast + have "matrix f' ** A = mat 1" + by (metis f' matrix_eq matrix_vector_mul_assoc matrix_vector_mul_lid matrix_works) + thus "A' ** A = mat 1" + by (metis AA' matrix_mul_assoc matrix_mul_lid) +qed + lemma matrix_left_right_inverse: fixes A A' :: "'a::{field}^'n^'n" shows "A ** A' = mat 1 \ A' ** A = mat 1" -proof - - { fix A A' :: "'a ^'n^'n" - assume AA': "A ** A' = mat 1" - have sA: "surj ((*v) A)" - using AA' matrix_right_invertible_surjective by auto - obtain f' :: "'a ^'n \ 'a ^'n" - where f': "Vector_Spaces.linear (*s) (*s) f'" "\x. f' (A *v x) = x" "\x. A *v f' x = x" - using sA vec.linear_surjective_isomorphism by blast - have "matrix f' ** A = mat 1" - by (metis f' matrix_eq matrix_vector_mul_assoc matrix_vector_mul_lid matrix_works) - hence "A' ** A = mat 1" - by (metis AA' matrix_mul_assoc matrix_mul_lid) - } - then show ?thesis by blast -qed + using matrix_left_right_inverse1 by blast lemma invertible_left_inverse: fixes A :: "'a::{field}^'n^'n" @@ -445,8 +451,8 @@ then obtain i where "v = row i A" by (auto simp: rows_def) with 0 show ?case - unfolding orthogonal_def inner_vec_def matrix_vector_mult_def row_def - by (simp add: mult.commute) (metis (no_types) vec_lambda_beta zero_index) + by (metis inner_commute matrix_vector_mul_component orthogonal_def row_def vec_lambda_eta + zero_index) qed lemma nullspace_inter_rowspace: @@ -490,7 +496,7 @@ finally show ?thesis . qed then show ?thesis - by (simp) + by simp qed lemma column_rank_def: @@ -612,15 +618,15 @@ by (metis exhaust_4) lemma UNIV_1 [simp]: "UNIV = {1::1}" - by (auto simp add: num1_eq_iff) + by auto -lemma UNIV_2: "UNIV = {1::2, 2::2}" +lemma UNIV_2: "UNIV = {1, 2::2}" using exhaust_2 by auto -lemma UNIV_3: "UNIV = {1::3, 2::3, 3::3}" +lemma UNIV_3: "UNIV = {1, 2, 3::3}" using exhaust_3 by auto -lemma UNIV_4: "UNIV = {1::4, 2::4, 3::4, 4::4}" +lemma UNIV_4: "UNIV = {1, 2, 3, 4::4}" using exhaust_4 by auto lemma sum_1: "sum f (UNIV::1 set) = f 1" @@ -715,7 +721,7 @@ have "P v" if "\x y. P (vector [x, y])" for v proof - have "vector [v$1, v$2] = v" - by (smt (verit, best) exhaust_2 vec_eq_iff vector_2) + unfolding vec_eq_iff by (metis (mono_tags) exhaust_2 vector_2) then show ?thesis by (metis that) qed @@ -727,7 +733,7 @@ have "P v" if "\x y z. P (vector [x, y, z])" for v proof - have "vector [v$1, v$2, v$3] = v" - by (smt (verit, best) exhaust_3 vec_eq_iff vector_3) + unfolding vec_eq_iff by (metis (mono_tags) exhaust_3 vector_3) then show ?thesis by (metis that) qed @@ -825,8 +831,7 @@ lemma vector_cart: fixes f :: "real^'n \ real" shows "(\ i. f (axis i 1)) = (\i\Basis. f i *\<^sub>R i)" - unfolding euclidean_eq_iff[where 'a="real^'n"] - by simp (simp add: Basis_vec_def inner_axis) + by (simp add: euclidean_eq_iff[where 'a="real^'n"]) (simp add: Basis_vec_def inner_axis) lemma const_vector_cart:"((\ i. d)::real^'n) = (\i\Basis. d *\<^sub>R i)" by (rule vector_cart) @@ -1258,10 +1263,9 @@ next fix A :: "real^'n^'n" and i assume "row i A = 0" - show "P ((*v) A)" - using matrix_vector_mul_linear - by (rule zeroes[where i=i]) - (metis \row i A = 0\ inner_zero_left matrix_vector_mul_component row_def vec_lambda_eta) + with matrix_vector_mul_linear show "P ((*v) A)" + by (metis matrix_vector_mul_component matrix_vector_mult_0 row_def + vec_lambda_eta zero_index zeroes) next fix A :: "real^'n^'n" assume 0: "\i j. i \ j \ A $ i $ j = 0" diff -r 3dfd62b4e2c8 -r ad31be996dcb src/HOL/Analysis/Connected.thy --- a/src/HOL/Analysis/Connected.thy Tue Apr 22 19:02:33 2025 +0200 +++ b/src/HOL/Analysis/Connected.thy Tue Apr 22 22:06:52 2025 +0100 @@ -2,7 +2,7 @@ Material split off from Topology_Euclidean_Space *) -section \Connected Components\ +chapter \Connected Components\ theory Connected imports @@ -38,7 +38,7 @@ then have th0: "connected S \ \ (\e2 e1. closed e2 \ open e1 \ S \ e1 \ (- e2) \ e1 \ (- e2) \ S = {} \ e1 \ S \ {} \ (- e2) \ S \ {})" (is " _ \ \ (\e2 e1. ?P e2 e1)") - by (simp add: closed_def) metis + unfolding closed_def by metis have th1: "?rhs \ \ (\t' t. closed t'\t = S\t' \ t\{} \ t\S \ (\t'. open t' \ t = S \ t'))" (is "_ \ \ (\t' t. ?Q t' t)") unfolding connected_def openin_open closedin_closed by auto @@ -49,8 +49,6 @@ then show ?thesis by metis qed - then have "\e2. (\e1. ?P e2 e1) \ (\t. ?Q e2 t)" - by blast then show ?thesis by (simp add: th0 th1) qed @@ -94,7 +92,10 @@ lemma connected_iff_eq_connected_component_set: "connected S \ (\x \ S. connected_component_set S x = S)" - by (metis connected_component_def connected_component_in connected_connected_component mem_Collect_eq subsetI subset_antisym) +proof + show "\x\S. connected_component_set S x = S \ connected S" + by (metis connectedI_const connected_connected_component) +qed (auto simp: connected_component_def) lemma connected_component_subset: "connected_component_set S x \ S" using connected_component_in by blast @@ -152,8 +153,7 @@ lemma connected_component_disjoint: "connected_component_set S a \ connected_component_set S b = {} \ a \ connected_component_set S b" - by (smt (verit) connected_component_eq connected_component_eq_empty connected_component_refl_eq - disjoint_iff_not_equal mem_Collect_eq) + using connected_component_eq connected_component_sym by fastforce lemma connected_component_nonoverlap: "connected_component_set S a \ connected_component_set S b = {} \ @@ -180,13 +180,18 @@ lemma connected_component_idemp: "connected_component_set (connected_component_set S x) x = connected_component_set S x" - by (metis Int_absorb connected_component_disjoint connected_component_eq_empty connected_component_eq_self connected_connected_component) +proof + show "connected_component_set S x \ connected_component_set (connected_component_set S x) x" + by (metis connected_component_eq_empty connected_component_maximal order.refl + connected_component_refl connected_connected_component mem_Collect_eq) +qed (simp add: connected_component_subset) lemma connected_component_unique: "\x \ c; c \ S; connected c; \c'. \x \ c'; c' \ S; connected c'\ \ c' \ c\ \ connected_component_set S x = c" - by (meson connected_component_maximal connected_component_subset connected_connected_component subsetD subset_antisym) + by (simp add: connected_component_maximal connected_component_subset subsetD + subset_antisym) lemma joinable_connected_component_eq: "\connected T; T \ S; @@ -237,12 +242,13 @@ lemma connected_component_set_homeomorphism: assumes "homeomorphism A B f g" "x \ A" - shows "connected_component_set B (f x) = f ` connected_component_set A x" (is "?lhs = ?rhs") + shows "connected_component_set B (f x) = f ` connected_component_set A x" proof - - have "y \ ?lhs \ y \ ?rhs" for y - by (smt (verit, best) assms connected_component_homeomorphism_iff homeomorphism_def image_iff mem_Collect_eq) - thus ?thesis - by blast + have "\y. connected_component B (f x) y + \ \u. u \ A \ connected_component B (f x) (f u) \ y = f u" + using assms by (metis connected_component_in homeomorphism_def image_iff) + with assms show ?thesis + by (auto simp: image_iff connected_component_homeomorphism_iff) qed subsection \The set of connected components of a set\ @@ -279,7 +285,7 @@ lemma in_components_maximal: "C \ components S \ - C \ {} \ C \ S \ connected C \ (\d. d \ {} \ C \ d \ d \ S \ connected d \ d = C)" + C \ {} \ C \ S \ connected C \ (\D. D \ {} \ C \ D \ D \ S \ connected D \ D = C)" (is "?lhs \ ?rhs") proof assume L: ?lhs @@ -289,7 +295,8 @@ by (metis (full_types) L components_iff connected_component_maximal connected_component_refl empty_iff mem_Collect_eq subsetD subset_antisym) next show "?rhs \ ?lhs" - by (metis bot.extremum_uniqueI components_iff connected_component_eq_empty connected_component_maximal connected_component_subset connected_connected_component subset_emptyI) + by (metis bot.extremum componentsI connected_component_maximal connected_component_subset + connected_connected_component order_antisym_conv subset_iff) qed @@ -335,7 +342,8 @@ by (metis components_empty components_eq_sing_iff empty_iff in_components_connected insertI1) lemma components_maximal: "\C \ components S; connected T; T \ S; C \ T \ {}\ \ T \ C" - by (smt (verit, best) Int_Un_eq(4) Un_upper1 bot_eq_sup_iff connected_Un in_components_maximal inf.orderE sup.mono sup.orderI) + by (metis (lifting) ext Int_Un_eq(4) Int_absorb Un_upper1 bot_eq_sup_iff connected_Un + in_components_maximal sup.mono sup.orderI) lemma exists_component_superset: "\T \ S; S \ {}; connected T\ \ \C. C \ components S \ T \ C" by (meson componentsI connected_component_maximal equals0I subset_eq) @@ -583,8 +591,7 @@ assume clo3: "closedin (top_of_set (U - C)) H3" and clo4: "closedin (top_of_set (U - C)) H4" and H34: "H3 \ H4 = U - C" "H3 \ H4 = {}" and "H3 \ {}" and "H4 \ {}" - and * [rule_format]: - "\H1 H2. \ closedin (top_of_set S) H1 \ + and * [rule_format]: "\H1 H2. \ closedin (top_of_set S) H1 \ \ closedin (top_of_set S) H2 \ H1 \ H2 \ S \ H1 \ H2 \ {} \ \ H1 \ {} \ \ H2 \ {}" then have "H3 \ U-C" and ope3: "openin (top_of_set (U - C)) (U - C - H3)" @@ -641,7 +648,7 @@ lemma finite_range_constant_imp_connected: assumes "\f::'a::topological_space \ 'b::real_normed_algebra_1. \continuous_on S f; finite(f ` S)\ \ f constant_on S" - shows "connected S" + shows "connected S" proof - { fix T U assume clt: "closedin (top_of_set S) T" diff -r 3dfd62b4e2c8 -r ad31be996dcb src/HOL/Analysis/Derivative.thy --- a/src/HOL/Analysis/Derivative.thy Tue Apr 22 19:02:33 2025 +0200 +++ b/src/HOL/Analysis/Derivative.thy Tue Apr 22 22:06:52 2025 +0100 @@ -2866,7 +2866,7 @@ have "dist (x + (y - f x)) (xh + (y - f xh)) * 2 \ dist x xh" if "norm x \ \" and "norm xh \ \" for x xh using that 4 [of x "xh-x"] by (auto simp: dist_norm norm_minus_commute algebra_simps) - then show "\x\cball 0 \. \ya\cball 0 \. dist (x + (y - f x)) (ya + (y - f ya)) \ (1/2) * dist x ya" + then show "\x z. \x\cball 0 \; z\cball 0 \\ \ dist (x + (y - f x)) (z + (y - f z)) \ (1/2) * dist x z" by auto qed (auto simp: complete_eq_closed) then show ?thesis diff -r 3dfd62b4e2c8 -r ad31be996dcb src/HOL/Analysis/Elementary_Metric_Spaces.thy --- a/src/HOL/Analysis/Elementary_Metric_Spaces.thy Tue Apr 22 19:02:33 2025 +0200 +++ b/src/HOL/Analysis/Elementary_Metric_Spaces.thy Tue Apr 22 22:06:52 2025 +0100 @@ -16,21 +16,21 @@ section \Open and closed balls\ definition\<^marker>\tag important\ ball :: "'a::metric_space \ real \ 'a set" - where "ball x e = {y. dist x y < e}" + where "ball x \ = {y. dist x y < \}" definition\<^marker>\tag important\ cball :: "'a::metric_space \ real \ 'a set" - where "cball x e = {y. dist x y \ e}" + where "cball x \ = {y. dist x y \ \}" definition\<^marker>\tag important\ sphere :: "'a::metric_space \ real \ 'a set" - where "sphere x e = {y. dist x y = e}" - -lemma mem_ball [simp, metric_unfold]: "y \ ball x e \ dist x y < e" + where "sphere x \ = {y. dist x y = \}" + +lemma mem_ball [simp, metric_unfold]: "y \ ball x \ \ dist x y < \" by (simp add: ball_def) -lemma mem_cball [simp, metric_unfold]: "y \ cball x e \ dist x y \ e" +lemma mem_cball [simp, metric_unfold]: "y \ cball x \ \ dist x y \ \" by (simp add: cball_def) -lemma mem_sphere [simp]: "y \ sphere x e \ dist x y = e" +lemma mem_sphere [simp]: "y \ sphere x \ \ dist x y = \" by (simp add: sphere_def) lemma ball_trivial [simp]: "ball x 0 = {}" @@ -52,16 +52,16 @@ for a :: "'a::metric_space" by auto -lemma centre_in_ball [simp]: "x \ ball x e \ 0 < e" +lemma centre_in_ball [simp]: "x \ ball x \ \ 0 < \" by simp -lemma centre_in_cball [simp]: "x \ cball x e \ 0 \ e" +lemma centre_in_cball [simp]: "x \ cball x \ \ 0 \ \" by simp -lemma ball_subset_cball [simp, intro]: "ball x e \ cball x e" +lemma ball_subset_cball [simp, intro]: "ball x \ \ cball x \" by (simp add: subset_eq) -lemma mem_ball_imp_mem_cball: "x \ ball y e \ x \ cball y e" +lemma mem_ball_imp_mem_cball: "x \ ball y \ \ x \ cball y \" by auto lemma sphere_cball [simp,intro]: "sphere z r \ cball z r" @@ -70,16 +70,16 @@ lemma cball_diff_sphere: "cball a r - sphere a r = ball a r" by auto -lemma subset_ball[intro]: "d \ e \ ball x d \ ball x e" +lemma subset_ball[intro]: "\ \ \ \ ball x \ \ ball x \" by auto -lemma subset_cball[intro]: "d \ e \ cball x d \ cball x e" +lemma subset_cball[intro]: "\ \ \ \ cball x \ \ cball x \" by auto -lemma mem_ball_leI: "x \ ball y e \ e \ f \ x \ ball y f" +lemma mem_ball_leI: "x \ ball y \ \ \ \ f \ x \ ball y f" by auto -lemma mem_cball_leI: "x \ cball y e \ e \ f \ x \ cball y f" +lemma mem_cball_leI: "x \ cball y \ \ \ \ f \ x \ cball y f" by auto lemma cball_trans: "y \ cball z b \ x \ cball y a \ x \ cball z (b + a)" @@ -100,70 +100,66 @@ lemma cball_diff_eq_sphere: "cball a r - ball a r = sphere a r" by auto -lemma open_ball [intro, simp]: "open (ball x e)" +lemma open_ball [intro, simp]: "open (ball x \)" proof - - have "open (dist x -` {..})" by (intro open_vimage open_lessThan continuous_intros) - also have "dist x -` {..} = ball x \" by auto finally show ?thesis . qed -lemma open_contains_ball: "open S \ (\x\S. \e>0. ball x e \ S)" +lemma open_contains_ball: "open S \ (\x\S. \\>0. ball x \ \ S)" by (simp add: open_dist subset_eq Ball_def dist_commute) -lemma openI [intro?]: "(\x. x\S \ \e>0. ball x e \ S) \ open S" +lemma openI [intro?]: "(\x. x\S \ \\>0. ball x \ \ S) \ open S" by (auto simp: open_contains_ball) lemma openE[elim?]: assumes "open S" "x\S" - obtains e where "e>0" "ball x e \ S" + obtains \ where "\>0" "ball x \ \ S" using assms unfolding open_contains_ball by auto -lemma open_contains_ball_eq: "open S \ x\S \ (\e>0. ball x e \ S)" +lemma open_contains_ball_eq: "open S \ x\S \ (\\>0. ball x \ \ S)" by (metis open_contains_ball subset_eq centre_in_ball) -lemma ball_eq_empty[simp]: "ball x e = {} \ e \ 0" +lemma ball_eq_empty[simp]: "ball x \ = {} \ \ \ 0" unfolding mem_ball set_eq_iff by (simp add: not_less) metric -lemma ball_empty: "e \ 0 \ ball x e = {}" +lemma ball_empty: "\ \ 0 \ ball x \ = {}" by simp -lemma closed_cball [iff]: "closed (cball x e)" +lemma closed_cball [iff]: "closed (cball x \)" proof - - have "closed (dist x -` {..e})" + have "closed (dist x -` {..\})" by (intro closed_vimage closed_atMost continuous_intros) - also have "dist x -` {..e} = cball x e" + also have "dist x -` {..\} = cball x \" by auto finally show ?thesis . qed -lemma open_contains_cball: "open S \ (\x\S. \e>0. cball x e \ S)" -proof - - { - fix x and e::real - assume "x\S" "e>0" "ball x e \ S" - then have "\d>0. cball x d \ S" - unfolding subset_eq by (intro exI [where x="e/2"], auto) - } - then show ?thesis - unfolding open_contains_ball by force -qed - -lemma open_contains_cball_eq: "open S \ (\x. x \ S \ (\e>0. cball x e \ S))" +lemma cball_subset_ball: + assumes "\>0" + shows "\\>0. cball x \ \ ball x \" + using assms unfolding subset_eq by (intro exI [where x="\/2"], auto) + +lemma open_contains_cball: "open S \ (\x\S. \\>0. cball x \ \ S)" + by (meson ball_subset_cball cball_subset_ball open_contains_ball subset_trans) + +lemma open_contains_cball_eq: "open S \ (\x. x \ S \ (\\>0. cball x \ \ S))" by (metis open_contains_cball subset_eq order_less_imp_le centre_in_cball) -lemma eventually_nhds_ball: "d > 0 \ eventually (\x. x \ ball z d) (nhds z)" +lemma eventually_nhds_ball: "\ > 0 \ eventually (\x. x \ ball z \) (nhds z)" by (rule eventually_nhds_in_open) simp_all -lemma eventually_at_ball: "d > 0 \ eventually (\t. t \ ball z d \ t \ A) (at z within A)" - unfolding eventually_at by (intro exI[of _ d]) (simp_all add: dist_commute) - -lemma eventually_at_ball': "d > 0 \ eventually (\t. t \ ball z d \ t \ z \ t \ A) (at z within A)" - unfolding eventually_at by (intro exI[of _ d]) (simp_all add: dist_commute) - -lemma at_within_ball: "e > 0 \ dist x y < e \ at y within ball x e = at y" +lemma eventually_at_ball: "\ > 0 \ eventually (\t. t \ ball z \ \ t \ A) (at z within A)" + unfolding eventually_at by (intro exI[of _ \]) (simp_all add: dist_commute) + +lemma eventually_at_ball': "\ > 0 \ eventually (\t. t \ ball z \ \ t \ z \ t \ A) (at z within A)" + unfolding eventually_at by (intro exI[of _ \]) (simp_all add: dist_commute) + +lemma at_within_ball: "\ > 0 \ dist x y < \ \ at y within ball x \ = at y" by (subst at_within_open) auto lemma atLeastAtMost_eq_cball: @@ -186,30 +182,42 @@ shows "ball a b = {a - b <..< a + b}" by (auto simp: dist_real_def) -lemma interior_ball [simp]: "interior (ball x e) = ball x e" +lemma interior_ball [simp]: "interior (ball x \) = ball x \" by (simp add: interior_open) -lemma cball_eq_empty [simp]: "cball x e = {} \ e < 0" - by (smt (verit, best) Diff_empty ball_eq_empty cball_diff_sphere centre_in_ball centre_in_cball sphere_empty) - -lemma cball_empty [simp]: "e < 0 \ cball x e = {}" +lemma cball_eq_empty [simp]: "cball x \ = {} \ \ < 0" + by (metis centre_in_cball order.trans ex_in_conv linorder_not_le mem_cball + zero_le_dist) + +lemma cball_empty [simp]: "\ < 0 \ cball x \ = {}" by simp lemma cball_sing: fixes x :: "'a::metric_space" - shows "e = 0 \ cball x e = {x}" + shows "\ = 0 \ cball x \ = {x}" by simp -lemma ball_divide_subset: "d \ 1 \ ball x (e/d) \ ball x e" +lemma ball_divide_subset: "\ \ 1 \ ball x (\/\) \ ball x \" by (metis ball_eq_empty div_by_1 frac_le linear subset_ball zero_less_one) -lemma ball_divide_subset_numeral: "ball x (e / numeral w) \ ball x e" +lemma ball_divide_subset_numeral: "ball x (\ / numeral w) \ ball x \" using ball_divide_subset one_le_numeral by blast -lemma cball_divide_subset: "d \ 1 \ cball x (e/d) \ cball x e" - by (smt (verit, best) cball_empty div_by_1 frac_le subset_cball zero_le_divide_iff) - -lemma cball_divide_subset_numeral: "cball x (e / numeral w) \ cball x e" +lemma cball_divide_subset: + assumes "\ \ 1" + shows "cball x (\/\) \ cball x \" +proof (cases "\\0") + case True + then show ?thesis + by (metis assms div_by_1 divide_mono order_le_less subset_cball zero_less_one) +next + case False + then have "(\/\) < 0" + using assms divide_less_0_iff by fastforce + then show ?thesis by auto +qed + +lemma cball_divide_subset_numeral: "cball x (\ / numeral w) \ cball x \" using cball_divide_subset one_le_numeral by blast lemma cball_scale: @@ -302,21 +310,21 @@ have "filterlim f (nhds x) sequentially" unfolding tendsto_iff proof clarify - fix e :: real - assume e: "e > 0" - then obtain n where n: "Suc n > 1 / e" + fix \ :: real + assume \: "\ > 0" + then obtain n where n: "Suc n > 1 / \" by (meson le_nat_floor lessI not_le) - have "dist (f k) x < e" if "k \ n" for k + have "dist (f k) x < \" if "k \ n" for k proof - have "dist (f k) x < 1 / real (Suc k)" using f[of k] by (auto simp: dist_commute) also have "\ \ 1 / real (Suc n)" using that by (intro divide_left_mono) auto - also have "\ < e" - using n e by (simp add: field_simps) + also have "\ < \" + using n \ by (simp add: field_simps) finally show ?thesis . qed - thus "\\<^sub>F k in sequentially. dist (f k) x < e" + thus "\\<^sub>F k in sequentially. dist (f k) x < \" unfolding eventually_at_top_linorder by blast qed moreover have "f n \ x" for n @@ -331,10 +339,10 @@ lemma islimpt_approachable: fixes x :: "'a::metric_space" - shows "x islimpt S \ (\e>0. \x'\S. x' \ x \ dist x' x < e)" + shows "x islimpt S \ (\\>0. \x'\S. x' \ x \ dist x' x < \)" unfolding islimpt_iff_eventually eventually_at by fast -lemma islimpt_approachable_le: "x islimpt S \ (\e>0. \x'\ S. x' \ x \ dist x' x \ e)" +lemma islimpt_approachable_le: "x islimpt S \ (\\>0. \x'\ S. x' \ x \ dist x' x \ \)" for x :: "'a::metric_space" unfolding islimpt_approachable using approachable_lt_le2 [where f="\y. dist y x" and P="\y. y \ S \ y = x" and Q="\x. True"] @@ -351,13 +359,13 @@ for x :: "'a::metric_space" by (auto simp: closure_def islimpt_Un dest: limpt_of_limpts) -lemma islimpt_eq_infinite_ball: "x islimpt S \ (\e>0. infinite(S \ ball x e))" +lemma islimpt_eq_infinite_ball: "x islimpt S \ (\\>0. infinite(S \ ball x \))" unfolding islimpt_eq_acc_point by (metis open_ball Int_commute Int_mono finite_subset open_contains_ball_eq subset_eq) -lemma islimpt_eq_infinite_cball: "x islimpt S \ (\e>0. infinite(S \ cball x e))" +lemma islimpt_eq_infinite_cball: "x islimpt S \ (\\>0. infinite(S \ cball x \))" unfolding islimpt_eq_infinite_ball - by (metis open_ball ball_subset_cball centre_in_ball finite_Int inf.absorb_iff2 inf_assoc open_contains_cball_eq) + by (metis ball_subset_cball cball_subset_ball finite_Int inf.absorb_iff2 inf_assoc) section \Perfect Metric Spaces\ @@ -374,9 +382,10 @@ lemma cball_eq_sing: fixes x :: "'a::{metric_space,perfect_space}" - shows "cball x e = {x} \ e = 0" - by (metis cball_trivial centre_in_cball finite.emptyI finite.insertI finite_Int - islimpt_UNIV islimpt_eq_infinite_cball less_eq_real_def) + shows "cball x \ = {x} \ \ = 0" + using cball_eq_empty [of x \] + by (metis open_ball ball_subset_cball cball_trivial + centre_in_ball not_less_iff_gr_or_eq not_open_singleton subset_singleton_iff) section \Finite and discrete\ @@ -384,26 +393,26 @@ lemma finite_ball_include: fixes a :: "'a::metric_space" assumes "finite S" - shows "\e>0. S \ ball a e" + shows "\\>0. S \ ball a \" using assms proof induction case (insert x S) - then obtain e0 where "e0>0" and e0:"S \ ball a e0" by auto - define e where "e = max e0 (2 * dist a x)" - have "e>0" unfolding e_def using \e0>0\ by auto - moreover have "insert x S \ ball a e" - using e0 \e>0\ unfolding e_def by auto + then obtain e0 where "e0>0" and e0:"S \ ball a e0" by auto + define \ where "\ = max e0 (2 * dist a x)" + have "\>0" unfolding \_def using \e0>0\ by auto + moreover have "insert x S \ ball a \" + using e0 \\>0\ unfolding \_def by auto ultimately show ?case by auto qed (auto intro: zero_less_one) lemma finite_set_avoid: fixes a :: "'a::metric_space" assumes "finite S" - shows "\d>0. \x\S. x \ a \ d \ dist a x" + shows "\\>0. \x\S. x \ a \ \ \ dist a x" using assms proof induction case (insert x S) - then obtain d where "d > 0" and d: "\x\S. x \ a \ d \ dist a x" + then obtain \ where "\ > 0" and \: "\x\S. x \ a \ \ \ dist a x" by blast then show ?case by (metis dist_nz dual_order.strict_implies_order insertE leI order.strict_trans2) @@ -411,17 +420,17 @@ lemma discrete_imp_closed: fixes S :: "'a::metric_space set" - assumes e: "0 < e" - and d: "\x \ S. \y \ S. dist y x < e \ y = x" + assumes \: "0 < \" + and \: "\x \ S. \y \ S. dist y x < \ \ y = x" shows "closed S" proof - - have False if C: "\e. e>0 \ \x'\S. x' \ x \ dist x' x < e" for x + have False if C: "\\. \>0 \ \x'\S. x' \ x \ dist x' x < \" for x proof - - obtain y where y: "y \ S" "y \ x" "dist y x < e/2" - by (meson C e half_gt_zero) - then have mp: "min (e/2) (dist x y) > 0" + obtain y where y: "y \ S" "y \ x" "dist y x < \/2" + by (meson C \ half_gt_zero) + then have mp: "min (\/2) (dist x y) > 0" by (simp add: dist_commute) - from d y C[OF mp] show ?thesis + from \ y C[OF mp] show ?thesis by metric qed then show ?thesis @@ -429,19 +438,19 @@ qed lemma discrete_imp_not_islimpt: - assumes e: "0 < e" - and d: "\x y. x \ S \ y \ S \ dist y x < e \ y = x" + assumes \: "0 < \" + and \: "\x y. x \ S \ y \ S \ dist y x < \ \ y = x" shows "\ x islimpt S" - by (metis closed_limpt d discrete_imp_closed e islimpt_approachable) + by (metis closed_limpt \ discrete_imp_closed \ islimpt_approachable) section \Interior\ -lemma mem_interior: "x \ interior S \ (\e>0. ball x e \ S)" +lemma mem_interior: "x \ interior S \ (\\>0. ball x \ \ S)" using open_contains_ball_eq [where S="interior S"] by (simp add: open_subset_interior) -lemma mem_interior_cball: "x \ interior S \ (\e>0. cball x e \ S)" +lemma mem_interior_cball: "x \ interior S \ (\\>0. cball x \ \ S)" by (meson ball_subset_cball interior_subset mem_interior open_contains_cball open_interior subset_trans) @@ -453,33 +462,33 @@ lemma frontier_straddle: fixes a :: "'a::metric_space" - shows "a \ frontier S \ (\e>0. (\x\S. dist a x < e) \ (\x. x \ S \ dist a x < e))" + shows "a \ frontier S \ (\\>0. (\x\S. dist a x < \) \ (\x. x \ S \ dist a x < \))" unfolding frontier_def closure_interior by (auto simp: mem_interior subset_eq ball_def) section \Limits\ -proposition Lim: "(f \ l) net \ trivial_limit net \ (\e>0. eventually (\x. dist (f x) l < e) net)" +proposition Lim: "(f \ l) net \ trivial_limit net \ (\\>0. eventually (\x. dist (f x) l < \) net)" by (auto simp: tendsto_iff trivial_limit_eq) text \Show that they yield usual definitions in the various cases.\ proposition Lim_within_le: "(f \ l)(at a within S) \ - (\e>0. \d>0. \x\S. 0 < dist x a \ dist x a \ d \ dist (f x) l < e)" + (\\>0. \\>0. \x\S. 0 < dist x a \ dist x a \ \ \ dist (f x) l < \)" by (auto simp: tendsto_iff eventually_at_le) proposition Lim_within: "(f \ l) (at a within S) \ - (\e >0. \d>0. \x \ S. 0 < dist x a \ dist x a < d \ dist (f x) l < e)" + (\\ >0. \\>0. \x \ S. 0 < dist x a \ dist x a < \ \ dist (f x) l < \)" by (auto simp: tendsto_iff eventually_at) corollary Lim_withinI [intro?]: - assumes "\e. e > 0 \ \d>0. \x \ S. 0 < dist x a \ dist x a < d \ dist (f x) l \ e" + assumes "\\. \ > 0 \ \\>0. \x \ S. 0 < dist x a \ dist x a < \ \ dist (f x) l \ \" shows "(f \ l) (at a within S)" - unfolding Lim_within by (smt (verit, ccfv_SIG) assms zero_less_dist_iff) + unfolding Lim_within by (smt (verit, best) assms) proposition Lim_at: "(f \ l) (at a) \ - (\e >0. \d>0. \x. 0 < dist x a \ dist x a < d \ dist (f x) l < e)" + (\\ >0. \\>0. \x. 0 < dist x a \ dist x a < \ \ dist (f x) l < \)" by (auto simp: tendsto_iff eventually_at) lemma Lim_transform_within_set: @@ -497,9 +506,9 @@ (is "?lhs = ?rhs") proof assume ?lhs - then have "\e>0. \x'\S. x' \ x \ dist x' x < e" + then have "\\>0. \x'\S. x' \ x \ dist x' x < \" by (force simp: islimpt_approachable) - then obtain y where y: "\e. e>0 \ y e \ S \ y e \ x \ dist (y e) x < e" + then obtain y where y: "\\. \>0 \ y \ \ S \ y \ \ x \ dist (y \) x < \" by metis define f where "f \ rec_nat (y 1) (\n fn. y (min (inverse(2 ^ (Suc n))) (dist fn x)))" have [simp]: "f 0 = y 1" @@ -510,8 +519,13 @@ case 0 show ?case by (simp add: y) next - case (Suc n) then show ?case - by (smt (verit, best) fSuc dist_pos_lt inverse_positive_iff_positive y zero_less_power) + case (Suc n) + then have "dist (f (Suc n)) x < inverse (2 ^ Suc n)" + unfolding fSuc + by (metis dist_nz min_less_iff_conj positive_imp_inverse_positive y zero_less_numeral + zero_less_power) + with Suc show ?case + by (auto simp: y fSuc) qed show ?rhs proof (intro exI conjI allI) @@ -525,14 +539,15 @@ case (Suc n) then consider "m < n" | "m = n" using less_Suc_eq by blast then show ?case - by (smt (verit, ccfv_threshold) Suc.IH dist_nz f fSuc y) + unfolding fSuc + by (smt (verit, ccfv_threshold) Suc.IH dist_nz f y) qed then show "inj f" by (metis less_irrefl linorder_injI) - have "\e n. \0 < e; nat \1 / e::real\ \ n\ \ inverse (2 ^ n) < e" + have "\\ n. \0 < \; nat \1 / \::real\ \ n\ \ inverse (2 ^ n) < \" by (simp add: divide_simps order_le_less_trans) then show "f \ x" - by (metis dual_order.strict_trans f lim_sequentially) + by (meson order.strict_trans f lim_sequentially) qed next assume ?rhs @@ -543,8 +558,8 @@ lemma Lim_dist_ubound: assumes "\(trivial_limit net)" and "(f \ l) net" - and "eventually (\x. dist a (f x) \ e) net" - shows "dist a l \ e" + and "eventually (\x. dist a (f x) \ \) net" + shows "dist a l \ \" using assms by (fast intro: tendsto_le tendsto_intros) @@ -553,24 +568,24 @@ text\Derive the epsilon-delta forms, which we often use as "definitions"\ proposition continuous_within_eps_delta: - "continuous (at x within s) f \ (\e>0. \d>0. \x'\ s. dist x' x < d --> dist (f x') (f x) < e)" + "continuous (at x within s) f \ (\\>0. \\>0. \x'\ s. dist x' x < \ --> dist (f x') (f x) < \)" unfolding continuous_within and Lim_within by fastforce corollary continuous_at_eps_delta: - "continuous (at x) f \ (\e > 0. \d > 0. \x'. dist x' x < d \ dist (f x') (f x) < e)" + "continuous (at x) f \ (\\ > 0. \\ > 0. \x'. dist x' x < \ \ dist (f x') (f x) < \)" using continuous_within_eps_delta [of x UNIV f] by simp lemma continuous_at_right_real_increasing: fixes f :: "real \ real" assumes nondecF: "\x y. x \ y \ f x \ f y" - shows "continuous (at_right a) f \ (\e>0. \d>0. f (a + d) - f a < e)" + shows "continuous (at_right a) f \ (\\>0. \\>0. f (a + \) - f a < \)" apply (simp add: greaterThan_def dist_real_def continuous_within Lim_within_le) apply (intro all_cong ex_cong) by (smt (verit, best) nondecF) lemma continuous_at_left_real_increasing: assumes nondecF: "\ x y. x \ y \ f x \ ((f y) :: real)" - shows "(continuous (at_left (a :: real)) f) \ (\e > 0. \delta > 0. f a - f (a - delta) < e)" + shows "(continuous (at_left (a :: real)) f) \ (\\ > 0. \\ > 0. f a - f (a - \) < \)" apply (simp add: lessThan_def dist_real_def continuous_within Lim_within_le) apply (intro all_cong ex_cong) by (smt (verit) nondecF) @@ -579,21 +594,19 @@ lemma continuous_within_ball: "continuous (at x within S) f \ - (\e > 0. \d > 0. f ` (ball x d \ S) \ ball (f x) e)" + (\\ > 0. \\ > 0. f ` (ball x \ \ S) \ ball (f x) \)" (is "?lhs = ?rhs") proof assume ?lhs { - fix e :: real - assume "e > 0" - then obtain d where "d>0" and d: "\y\S. 0 < dist y x \ dist y x < d \ dist (f y) (f x) < e" + fix \ :: real + assume "\ > 0" + then obtain \ where "\>0" and \: "\y\S. 0 < dist y x \ dist y x < \ \ dist (f y) (f x) < \" using \?lhs\[unfolded continuous_within Lim_within] by auto - { fix y - assume "y \ f ` (ball x d \ S)" then have "y \ ball (f x) e" - using d \e > 0\ by (auto simp: dist_commute) - } - then have "\d>0. f ` (ball x d \ S) \ ball (f x) e" - using \d > 0\ by blast + have "y \ ball (f x) \" if "y \ f ` (ball x \ \ S)" for y + using that \ \\ > 0\ by (auto simp: dist_commute) + then have "\\>0. f ` (ball x \ \ S) \ ball (f x) \" + using \\ > 0\ by blast } then show ?rhs by auto next @@ -603,38 +616,35 @@ by (metis (mono_tags, lifting) Int_iff dist_commute mem_Collect_eq) qed -lemma continuous_at_ball: - "continuous (at x) f \ (\e>0. \d>0. f ` (ball x d) \ ball (f x) e)" - apply (simp add: continuous_at Lim_at subset_eq Ball_def Bex_def image_iff) - by (smt (verit, ccfv_threshold) dist_commute dist_self) +corollary continuous_at_ball: + "continuous (at x) f \ (\\>0. \\>0. f ` (ball x \) \ ball (f x) \)" + by (simp add: continuous_within_ball) text\Define setwise continuity in terms of limits within the set.\ lemma continuous_on_iff: "continuous_on s f \ - (\x\s. \e>0. \d>0. \x'\s. dist x' x < d \ dist (f x') (f x) < e)" + (\x\s. \\>0. \\>0. \x'\s. dist x' x < \ \ dist (f x') (f x) < \)" unfolding continuous_on_def Lim_within by (metis dist_pos_lt dist_self) lemma continuous_within_E: - assumes "continuous (at x within S) f" "e>0" - obtains d where "d>0" "\x'. \x'\ S; dist x' x \ d\ \ dist (f x') (f x) < e" + assumes "continuous (at x within S) f" "\>0" + obtains \ where "\>0" "\x'. \x'\ S; dist x' x \ \\ \ dist (f x') (f x) < \" using assms unfolding continuous_within_eps_delta by (metis dense order_le_less_trans) lemma continuous_onI [intro?]: - assumes "\x e. \e > 0; x \ S\ \ \d>0. \x'\S. dist x' x < d \ dist (f x') (f x) \ e" + assumes "\x \. \\ > 0; x \ S\ \ \\>0. \x'\S. dist x' x < \ \ dist (f x') (f x) \ \" shows "continuous_on S f" -apply (simp add: continuous_on_iff, clarify) -apply (rule ex_forward [OF assms [OF half_gt_zero]], auto) -done + using assms [OF half_gt_zero] by (force simp add: continuous_on_iff) text\Some simple consequential lemmas.\ lemma continuous_onE: - assumes "continuous_on s f" "x\s" "e>0" - obtains d where "d>0" "\x'. \x' \ s; dist x' x \ d\ \ dist (f x') (f x) < e" + assumes "continuous_on s f" "x\s" "\>0" + obtains \ where "\>0" "\x'. \x' \ s; dist x' x \ \\ \ dist (f x') (f x) < \" using assms unfolding continuous_on_iff by (metis dense order_le_less_trans) @@ -643,9 +653,9 @@ lemma continuous_transform_within: fixes f g :: "'a::metric_space \ 'b::topological_space" assumes "continuous (at x within s) f" - and "0 < d" + and "0 < \" and "x \ s" - and "\x'. \x' \ s; dist x' x < d\ \ f x' = g x'" + and "\x'. \x' \ s; dist x' x < \\ \ f x' = g x'" shows "continuous (at x within s) g" using assms unfolding continuous_within by (force intro: Lim_transform_within) @@ -655,23 +665,23 @@ lemma closure_approachable: fixes S :: "'a::metric_space set" - shows "x \ closure S \ (\e>0. \y\S. dist y x < e)" + shows "x \ closure S \ (\\>0. \y\S. dist y x < \)" using dist_self by (force simp: closure_def islimpt_approachable) lemma closure_approachable_le: fixes S :: "'a::metric_space set" - shows "x \ closure S \ (\e>0. \y\S. dist y x \ e)" + shows "x \ closure S \ (\\>0. \y\S. dist y x \ \)" unfolding closure_approachable using dense by force lemma closure_approachableD: - assumes "x \ closure S" "e>0" - shows "\y\S. dist x y < e" + assumes "x \ closure S" "\>0" + shows "\y\S. dist x y < \" using assms unfolding closure_approachable by (auto simp: dist_commute) lemma closed_approachable: fixes S :: "'a::metric_space set" - shows "closed S \ (\e>0. \y\S. dist y x < e) \ x \ S" + shows "closed S \ (\\>0. \y\S. dist y x < \) \ x \ S" by (metis closure_closed closure_approachable) lemma closure_contains_Inf: @@ -681,12 +691,12 @@ proof - have *: "\x\S. Inf S \ x" using cInf_lower[of _ S] assms by metis - { fix e :: real - assume "e > 0" - then have "Inf S < Inf S + e" by simp - with assms obtain x where "x \ S" "x < Inf S + e" + { fix \ :: real + assume "\ > 0" + then have "Inf S < Inf S + \" by simp + with assms obtain x where "x \ S" "x < Inf S + \" using cInf_lessD by blast - with * have "\x\S. dist x (Inf S) < e" + with * have "\x\S. dist x (Inf S) < \" using dist_real_def by force } then show ?thesis unfolding closure_approachable by auto @@ -700,43 +710,43 @@ have *: "\x\S. x \ Sup S" using cSup_upper[of _ S] assms by metis { - fix e :: real - assume "e > 0" - then have "Sup S - e < Sup S" by simp - with assms obtain x where "x \ S" "Sup S - e < x" + fix \ :: real + assume "\ > 0" + then have "Sup S - \ < Sup S" by simp + with assms obtain x where "x \ S" "Sup S - \ < x" using less_cSupE by blast - with * have "\x\S. dist x (Sup S) < e" + with * have "\x\S. dist x (Sup S) < \" using dist_real_def by force } then show ?thesis unfolding closure_approachable by auto qed lemma not_trivial_limit_within_ball: - "\ trivial_limit (at x within S) \ (\e>0. S \ ball x e - {x} \ {})" + "\ trivial_limit (at x within S) \ (\\>0. S \ ball x \ - {x} \ {})" (is "?lhs \ ?rhs") proof show ?rhs if ?lhs proof - - { fix e :: real - assume "e > 0" - then obtain y where "y \ S - {x}" and "dist y x < e" + { fix \ :: real + assume "\ > 0" + then obtain y where "y \ S - {x}" and "dist y x < \" using \?lhs\ not_trivial_limit_within[of x S] closure_approachable[of x "S - {x}"] by auto - then have "y \ S \ ball x e - {x}" + then have "y \ S \ ball x \ - {x}" unfolding ball_def by (simp add: dist_commute) - then have "S \ ball x e - {x} \ {}" by blast + then have "S \ ball x \ - {x} \ {}" by blast } then show ?thesis by auto qed show ?lhs if ?rhs proof - - { fix e :: real - assume "e > 0" - then obtain y where "y \ S \ ball x e - {x}" + { fix \ :: real + assume "\ > 0" + then obtain y where "y \ S \ ball x \ - {x}" using \?rhs\ by blast - then have "y \ S - {x}" and "dist y x < e" + then have "y \ S - {x}" and "dist y x < \" unfolding ball_def by (simp_all add: dist_commute) - then have "\y \ S - {x}. dist y x < e" + then have "\y \ S - {x}. dist y x < \" by auto } then show ?thesis @@ -750,12 +760,12 @@ (* FIXME: This has to be unified with BSEQ!! *) definition\<^marker>\tag important\ (in metric_space) bounded :: "'a set \ bool" - where "bounded S \ (\x e. \y\S. dist x y \ e)" - -lemma bounded_subset_cball: "bounded S \ (\e x. S \ cball x e \ 0 \ e)" + where "bounded S \ (\x \. \y\S. dist x y \ \)" + +lemma bounded_subset_cball: "bounded S \ (\\ x. S \ cball x \ \ 0 \ \)" unfolding bounded_def subset_eq by auto (meson order_trans zero_le_dist) -lemma bounded_any_center: "bounded S \ (\e. \y\S. dist a y \ e)" +lemma bounded_any_center: "bounded S \ (\\. \y\S. dist a y \ \)" unfolding bounded_def by auto (metis add.commute add_le_cancel_right dist_commute dist_triangle_le) @@ -806,14 +816,15 @@ lemma bounded_closure_image: "bounded (f ` closure S) \ bounded (f ` S)" by (simp add: bounded_subset closure_subset image_mono) -lemma bounded_cball[simp,intro]: "bounded (cball x e)" +lemma bounded_cball[simp,intro]: "bounded (cball x \)" unfolding bounded_def using mem_cball by blast -lemma bounded_ball[simp,intro]: "bounded (ball x e)" +lemma bounded_ball[simp,intro]: "bounded (ball x \)" by (metis ball_subset_cball bounded_cball bounded_subset) lemma bounded_Un[simp]: "bounded (S \ T) \ bounded S \ bounded T" - by (auto simp: bounded_def) (metis Un_iff bounded_any_center le_max_iff_disj) + unfolding bounded_def + by (metis Un_iff bounded_any_center order.trans linorder_linear) lemma bounded_Union[intro]: "finite F \ \S\F. bounded S \ bounded (\F)" by (induct rule: finite_induct[of F]) auto @@ -822,14 +833,7 @@ by auto lemma bounded_insert [simp]: "bounded (insert x S) \ bounded S" -proof - - have "\y\{x}. dist x y \ 0" - by simp - then have "bounded {x}" - unfolding bounded_def by fast - then show ?thesis - by (metis insert_is_Un bounded_Un) -qed + by (metis bounded_Un bounded_cball cball_trivial insert_is_Un) lemma bounded_subset_ballI: "S \ ball x r \ bounded S" by (meson bounded_ball bounded_subset) @@ -837,10 +841,10 @@ lemma bounded_subset_ballD: assumes "bounded S" shows "\r. 0 < r \ S \ ball x r" proof - - obtain e::real and y where "S \ cball y e" "0 \ e" + obtain \::real and y where "S \ cball y \" "0 \ \" using assms by (auto simp: bounded_subset_cball) then show ?thesis - by (intro exI[where x="dist x y + e + 1"]) metric + by (intro exI[where x="dist x y + \ + 1"]) metric qed lemma finite_imp_bounded [intro]: "finite S \ bounded S" @@ -866,12 +870,12 @@ qed lemma bounded_Times: - assumes "bounded s" "bounded t" - shows "bounded (s \ t)" + assumes "bounded S" "bounded T" + shows "bounded (S \ T)" proof - - obtain x y a b where "\z\s. dist x z \ a" "\z\t. dist y z \ b" + obtain x y a b where "\z\S. dist x z \ a" "\z\T. dist y z \ b" using assms [unfolded bounded_def] by auto - then have "\z\s \ t. dist (x, y) z \ sqrt (a\<^sup>2 + b\<^sup>2)" + then have "\z\S \ T. dist (x, y) z \ sqrt (a\<^sup>2 + b\<^sup>2)" by (auto simp: dist_Pair_Pair real_sqrt_le_mono add_mono power_mono) then show ?thesis unfolding bounded_any_center [where a="(x, y)"] by auto qed @@ -931,26 +935,26 @@ \ lemma compact_subset_open_imp_ball_epsilon_subset: assumes "compact A" "open B" "A \ B" - obtains e where "e > 0" "(\x\A. ball x e) \ B" + obtains \ where "\ > 0" "(\x\A. ball x \) \ B" proof - - have "\x\A. \e. e > 0 \ ball x e \ B" + have "\x\A. \\. \ > 0 \ ball x \ \ B" using assms unfolding open_contains_ball by blast - then obtain e where e: "\x. x \ A \ e x > 0" "\x. x \ A \ ball x (e x) \ B" + then obtain \ where \: "\x. x \ A \ \ x > 0" "\x. x \ A \ ball x (\ x) \ B" by metis - define C where "C = e ` A" - obtain X where X: "X \ A" "finite X" "A \ (\c\X. ball c (e c / 2))" - using assms(1) + define C where "C = \ ` A" + obtain X where X: "X \ A" "finite X" "A \ (\c\X. ball c (\ c / 2))" + using \compact A\ proof (rule compactE_image) - show "open (ball x (e x / 2))" if "x \ A" for x + show "open (ball x (\ x / 2))" if "x \ A" for x by simp - show "A \ (\c\A. ball c (e c / 2))" - using e by auto + show "A \ (\c\A. ball c (\ c / 2))" + using \ by auto qed auto - define e' where "e' = Min (insert 1 ((\x. e x / 2) ` X))" + define e' where "e' = Min (insert 1 ((\x. \ x / 2) ` X))" have "e' > 0" - unfolding e'_def using e X by (subst Min_gr_iff) auto - have e': "e' \ e x / 2" if "x \ X" for x + unfolding e'_def using \ X by (subst Min_gr_iff) auto + have e': "e' \ \ x / 2" if "x \ X" for x using that X unfolding e'_def by (intro Min.coboundedI) auto show ?thesis @@ -961,20 +965,20 @@ show "(\x\A. ball x e') \ B" proof clarify fix x y assume xy: "x \ A" "y \ ball x e'" - from xy(1) X obtain z where z: "z \ X" "x \ ball z (e z / 2)" + from xy(1) X obtain z where z: "z \ X" "x \ ball z (\ z / 2)" by auto have "dist y z \ dist x y + dist z x" by (metis dist_commute dist_triangle) - also have "dist z x < e z / 2" + also have "dist z x < \ z / 2" using xy z by auto also have "dist x y < e'" using xy by auto - also have "\ \ e z / 2" + also have "\ \ \ z / 2" using z by (intro e') auto - finally have "y \ ball z (e z)" + finally have "y \ ball z (\ z)" by (simp add: dist_commute) also have "\ \ B" - using z X by (intro e) auto + using z X by (intro \) auto finally show "y \ B" . qed qed @@ -982,42 +986,42 @@ lemma compact_subset_open_imp_cball_epsilon_subset: assumes "compact A" "open B" "A \ B" - obtains e where "e > 0" "(\x\A. cball x e) \ B" + obtains \ where "\ > 0" "(\x\A. cball x \) \ B" proof - - obtain e where "e > 0" and e: "(\x\A. ball x e) \ B" + obtain \ where "\ > 0" and \: "(\x\A. ball x \) \ B" using compact_subset_open_imp_ball_epsilon_subset [OF assms] by blast - then have "(\x\A. cball x (e / 2)) \ (\x\A. ball x e)" + then have "(\x\A. cball x (\ / 2)) \ (\x\A. ball x \)" by auto - with \0 < e\ that show ?thesis - by (metis e half_gt_zero_iff order_trans) + with \0 < \\ that show ?thesis + by (metis \ half_gt_zero_iff order_trans) qed subsubsection\Totally bounded\ proposition seq_compact_imp_totally_bounded: assumes "seq_compact S" - shows "\e>0. \k. finite k \ k \ S \ S \ (\x\k. ball x e)" + shows "\\>0. \k. finite k \ k \ S \ S \ (\x\k. ball x \)" proof - - { fix e::real assume "e > 0" assume *: "\k. finite k \ k \ S \ \ S \ (\x\k. ball x e)" - let ?Q = "\x n r. r \ S \ (\m < (n::nat). \ (dist (x m) r < e))" + { fix \::real assume "\ > 0" assume *: "\k. finite k \ k \ S \ \ S \ (\x\k. ball x \)" + let ?Q = "\x n r. r \ S \ (\m < (n::nat). \ (dist (x m) r < \))" have "\x. \n::nat. ?Q x n (x n)" proof (rule dependent_wellorder_choice) fix n x assume "\y. y < n \ ?Q x y (x y)" - then have "\ S \ (\x\x ` {0.. S \ (\x\x ` {0..)" using *[of "x ` {0 ..< n}"] by (auto simp: subset_eq) - then obtain z where z:"z\S" "z \ (\x\x ` {0..S" "z \ (\x\x ` {0..)" unfolding subset_eq by auto show "\r. ?Q x n r" using z by auto qed simp - then obtain x where "\n::nat. x n \ S" and x:"\n m. m < n \ \ (dist (x m) (x n) < e)" + then obtain x where "\n::nat. x n \ S" and x:"\n m. m < n \ \ (dist (x m) (x n) < \)" by blast - then obtain l r where "l \ S" and r:"strict_mono r" and "((x \ r) \ l) sequentially" + then obtain l r where "l \ S" and r:"strict_mono r" and "(x \ r) \ l" using assms by (metis seq_compact_def) then have "Cauchy (x \ r)" using LIMSEQ_imp_Cauchy by auto - then obtain N::nat where "\m n. N \ m \ N \ n \ dist ((x \ r) m) ((x \ r) n) < e" - unfolding Cauchy_def using \e > 0\ by blast + then obtain N::nat where "\m n. N \ m \ N \ n \ dist ((x \ r) m) ((x \ r) n) < \" + unfolding Cauchy_def using \\ > 0\ by blast then have False using x[of "r N" "r (N+1)"] r by (auto simp: strict_mono_def) } then show ?thesis @@ -1031,39 +1035,38 @@ assumes "seq_compact S" shows "compact S" proof - - from seq_compact_imp_totally_bounded[OF \seq_compact S\] - obtain f where f: "\e>0. finite (f e) \ f e \ S \ S \ (\x\f e. ball x e)" - unfolding choice_iff' .. - define K where "K = (\(x, r). ball x r) ` ((\e \ \ \ {0 <..}. f e) \ \)" + obtain f where f: "\\>0. finite (f \) \ f \ \ S \ S \ (\x\f \. ball x \)" + by (metis assms seq_compact_imp_totally_bounded) + define K where "K = (\(x, r). ball x r) ` ((\\ \ \ \ {0 <..}. f \) \ \)" have "countably_compact S" using \seq_compact S\ by (rule seq_compact_imp_countably_compact) then show "compact S" proof (rule countably_compact_imp_compact) show "countable K" unfolding K_def using f - by (auto intro: countable_finite countable_subset countable_rat - intro!: countable_image countable_SIGMA countable_UN) + by (meson countable_Int1 countable_SIGMA countable_UN countable_finite + countable_image countable_rat greaterThan_iff inf_le2 subset_iff) show "\b\K. open b" by (auto simp: K_def) next fix T x assume T: "open T" "x \ T" and x: "x \ S" - from openE[OF T] obtain e where "0 < e" "ball x e \ T" + from openE[OF T] obtain \ where "0 < \" "ball x \ \ T" by auto - then have "0 < e/2" "ball x (e/2) \ T" + then have "0 < \/2" "ball x (\/2) \ T" by auto - from Rats_dense_in_real[OF \0 < e/2\] obtain r where "r \ \" "0 < r" "r < e/2" + from Rats_dense_in_real[OF \0 < \/2\] obtain r where "r \ \" "0 < r" "r < \/2" by auto from f[rule_format, of r] \0 < r\ \x \ S\ obtain k where "k \ f r" "x \ ball k r" by auto from \r \ \\ \0 < r\ \k \ f r\ have "ball k r \ K" by (auto simp: K_def) then show "\b\K. x \ b \ b \ S \ T" - proof (rule bexI[rotated], safe) + proof (rule rev_bexI, intro conjI subsetI) fix y - assume "y \ ball k r" - with \r < e/2\ \x \ ball k r\ have "dist x y < e" - by (intro dist_triangle_half_r [of k _ e]) (auto simp: dist_commute) - with \ball x e \ T\ show "y \ T" + assume "y \ ball k r \ S" + with \r < \/2\ \x \ ball k r\ have "dist x y < \" + by (intro dist_triangle_half_r [of k _ \]) (auto simp: dist_commute) + with \ball x \ \ T\ show "y \ T" by auto next show "x \ ball k r" by fact @@ -1095,37 +1098,34 @@ section \Banach fixed point theorem\ theorem Banach_fix: - assumes s: "complete s" "s \ {}" + assumes S: "complete S" "S \ {}" and c: "0 \ c" "c < 1" - and f: "f ` s \ s" - and lipschitz: "\x\s. \y\s. dist (f x) (f y) \ c * dist x y" - shows "\!x\s. f x = x" + and f: "f ` S \ S" + and lipschitz: "\x y. \x\S; y\S\ \ dist (f x) (f y) \ c * dist x y" + shows "\!x\S. f x = x" proof - - from c have "1 - c > 0" by simp - - from s(2) obtain z0 where z0: "z0 \ s" by blast + from S obtain z0 where z0: "z0 \ S" by blast define z where "z n = (f ^^ n) z0" for n - with f z0 have z_in_s: "z n \ s" for n :: nat + with f z0 have z_in_s: "z n \ S" for n :: nat by (induct n) auto - define d where "d = dist (z 0) (z 1)" + define \ where "\ = dist (z 0) (z 1)" have fzn: "f (z n) = z (Suc n)" for n by (simp add: z_def) - have cf_z: "dist (z n) (z (Suc n)) \ (c ^ n) * d" for n :: nat + have cf_z: "dist (z n) (z (Suc n)) \ (c ^ n) * \" for n :: nat proof (induct n) case 0 then show ?case - by (simp add: d_def) + by (simp add: \_def) next case (Suc m) - with \0 \ c\ have "c * dist (z m) (z (Suc m)) \ c ^ Suc m * d" - using mult_left_mono[of "dist (z m) (z (Suc m))" "c ^ m * d" c] by simp + with \0 \ c\ have "c * dist (z m) (z (Suc m)) \ c ^ Suc m * \" + using mult_left_mono[of "dist (z m) (z (Suc m))" "c ^ m * \" c] by simp then show ?case - using lipschitz[THEN bspec[where x="z m"], OF z_in_s, THEN bspec[where x="z (Suc m)"], OF z_in_s] - by (simp add: fzn mult_le_cancel_left) + by (metis fzn lipschitz order_trans z_in_s) qed - have cf_z2: "(1 - c) * dist (z m) (z (m + n)) \ (c ^ m) * d * (1 - c ^ n)" for n m :: nat + have cf_z2: "(1 - c) * dist (z m) (z (m + n)) \ (c ^ m) * \ * (1 - c ^ n)" for n m :: nat proof (induct n) case 0 show ?case by simp @@ -1134,100 +1134,97 @@ from c have "(1 - c) * dist (z m) (z (m + Suc k)) \ (1 - c) * (dist (z m) (z (m + k)) + dist (z (m + k)) (z (Suc (m + k))))" by (simp add: dist_triangle) - also from c cf_z[of "m + k"] have "\ \ (1 - c) * (dist (z m) (z (m + k)) + c ^ (m + k) * d)" + also from c cf_z[of "m + k"] have "\ \ (1 - c) * (dist (z m) (z (m + k)) + c ^ (m + k) * \)" by simp - also from Suc have "\ \ c ^ m * d * (1 - c ^ k) + (1 - c) * c ^ (m + k) * d" + also from Suc have "\ \ c ^ m * \ * (1 - c ^ k) + (1 - c) * c ^ (m + k) * \" by (simp add: field_simps) - also have "\ = (c ^ m) * (d * (1 - c ^ k) + (1 - c) * c ^ k * d)" + also have "\ = (c ^ m) * (\ * (1 - c ^ k) + (1 - c) * c ^ k * \)" by (simp add: power_add field_simps) - also from c have "\ \ (c ^ m) * d * (1 - c ^ Suc k)" + also from c have "\ \ (c ^ m) * \ * (1 - c ^ Suc k)" by (simp add: field_simps) - finally show ?case by simp + finally show ?case . qed - have "\N. \m n. N \ m \ N \ n \ dist (z m) (z n) < e" if "e > 0" for e - proof (cases "d = 0") + have "\N. \m n. N \ m \ N \ n \ dist (z m) (z n) < \" if "\ > 0" for \ + proof (cases "\ = 0") case True - from \1 - c > 0\ have "(1 - c) * x \ 0 \ x \ 0" for x - by (simp add: mult_le_0_iff) + have "(1 - c) * x \ 0 \ x \ 0" for x + using c mult_le_0_iff nle_le by fastforce with c cf_z2[of 0] True have "z n = z0" for n by (simp add: z_def) - with \e > 0\ show ?thesis by simp + with \\ > 0\ show ?thesis by simp next case False - with zero_le_dist[of "z 0" "z 1"] have "d > 0" - by (metis d_def less_le) - with \1 - c > 0\ \e > 0\ have "0 < e * (1 - c) / d" + with zero_le_dist[of "z 0" "z 1"] have "\ > 0" + by (metis \_def less_le) + with c \\ > 0\ have "0 < \ * (1 - c) / \" by simp - with c obtain N where N: "c ^ N < e * (1 - c) / d" - using real_arch_pow_inv[of "e * (1 - c) / d" c] by auto - have *: "dist (z m) (z n) < e" if "m > n" and as: "m \ N" "n \ N" for m n :: nat + with c obtain N where N: "c ^ N < \ * (1 - c) / \" + using real_arch_pow_inv[of "\ * (1 - c) / \" c] by auto + have *: "dist (z m) (z n) < \" if "m > n" and as: "m \ N" "n \ N" for m n :: nat proof - - from c \n \ N\ have *: "c ^ n \ c ^ N" - using power_decreasing[OF \n\N\, of c] by simp - from c \m > n\ have "1 - c ^ (m - n) > 0" - using power_strict_mono[of c 1 "m - n"] by simp - with \d > 0\ \0 < 1 - c\ have **: "d * (1 - c ^ (m - n)) / (1 - c) > 0" + have *: "c ^ n \ c ^ N" + using power_decreasing[OF \n\N\, of c] c by simp + have "1 - c ^ (m - n) > 0" + using power_strict_mono[of c 1 "m - n"] c \m > n\ by simp + with \\ > 0\ c have **: "\ * (1 - c ^ (m - n)) / (1 - c) > 0" by simp from cf_z2[of n "m - n"] \m > n\ - have "dist (z m) (z n) \ c ^ n * d * (1 - c ^ (m - n)) / (1 - c)" - by (simp add: pos_le_divide_eq[OF \1 - c > 0\] mult.commute dist_commute) - also have "\ \ c ^ N * d * (1 - c ^ (m - n)) / (1 - c)" + have "dist (z m) (z n) \ c ^ n * \ * (1 - c ^ (m - n)) / (1 - c)" + by (simp add: pos_le_divide_eq c mult.commute dist_commute) + also have "\ \ c ^ N * \ * (1 - c ^ (m - n)) / (1 - c)" using mult_right_mono[OF * order_less_imp_le[OF **]] by (simp add: mult.assoc) - also have "\ < (e * (1 - c) / d) * d * (1 - c ^ (m - n)) / (1 - c)" + also have "\ < (\ * (1 - c) / \) * \ * (1 - c ^ (m - n)) / (1 - c)" using mult_strict_right_mono[OF N **] by (auto simp: mult.assoc) - also from c \1 - c ^ (m - n) > 0\ \e > 0\ have "\ \ e" - using mult_right_le_one_le[of e "1 - c ^ (m - n)"] by auto - finally show ?thesis by simp + also from c \1 - c ^ (m - n) > 0\ \\ > 0\ have "\ \ \" + using mult_right_le_one_le[of \ "1 - c ^ (m - n)"] by auto + finally show ?thesis . qed - have "dist (z n) (z m) < e" if "N \ m" "N \ n" for m n :: nat - using *[of n m] *[of m n] - using \0 < e\ dist_commute_lessI that by fastforce + have "dist (z n) (z m) < \" if "N \ m" "N \ n" for m n :: nat + using *[of n m] *[of m n] + using \0 < \\ dist_commute_lessI that by fastforce then show ?thesis by auto qed then have "Cauchy z" by (metis metric_CauchyI) - then obtain x where "x\s" and x:"(z \ x) sequentially" - using s(1)[unfolded compact_def complete_def, THEN spec[where x=z]] and z_in_s by auto - - define e where "e = dist (f x) x" - have "e = 0" + then obtain x where "x\S" and x:"(z \ x) sequentially" + using \complete S\ complete_def z_in_s by blast + + define \ where "\ = dist (f x) x" + have "\ = 0" proof (rule ccontr) - assume "e \ 0" - then have "e > 0" - unfolding e_def using zero_le_dist[of "f x" x] - by (metis dist_eq_0_iff dist_nz e_def) - then obtain N where N:"\n\N. dist (z n) x < e/2" - using x[unfolded lim_sequentially, THEN spec[where x="e/2"]] by auto - then have N':"dist (z N) x < e/2" by auto + assume "\ \ 0" + then have "\ > 0" + unfolding \_def using zero_le_dist[of "f x" x] + by (metis dist_eq_0_iff dist_nz \_def) + then obtain N where N:"\n\N. dist (z n) x < \/2" + using x[unfolded lim_sequentially, THEN spec[where x="\/2"]] by auto + then have N':"dist (z N) x < \/2" by auto have *: "c * dist (z N) x \ dist (z N) x" unfolding mult_le_cancel_right2 using zero_le_dist[of "z N" x] and c by (metis dist_eq_0_iff dist_nz order_less_asym less_le) have "dist (f (z N)) (f x) \ c * dist (z N) x" - using lipschitz[THEN bspec[where x="z N"], THEN bspec[where x=x]] - using z_in_s[of N] \x\s\ c - by auto - also have "\ < e/2" + by (simp add: \x \ S\ lipschitz z_in_s) + also have "\ < \/2" using N' and c using * by auto finally show False unfolding fzn - using N[THEN spec[where x="Suc N"]] and dist_triangle_half_r[of "z (Suc N)" "f x" e x] - unfolding e_def - by auto + by (metis N \_def dist_commute dist_triangle_half_l le_eq_less_or_eq lessI + order_less_irrefl) qed - then have "f x = x" by (auto simp: e_def) - moreover have "y = x" if "f y = y" "y \ s" for y + then have "f x = x" by (auto simp: \_def) + moreover have "y = x" if "f y = y" "y \ S" for y proof - - from \x \ s\ \f x = x\ that have "dist x y \ c * dist x y" + from \x \ S\ \f x = x\ that have "dist x y \ c * dist x y" using lipschitz by fastforce with c and zero_le_dist[of x y] have "dist x y = 0" by (simp add: mult_le_cancel_right1) then show ?thesis by simp qed ultimately show ?thesis - using \x\s\ by blast + using \x\S\ by blast qed @@ -1237,7 +1234,7 @@ fixes S :: "'a::metric_space set" assumes S: "compact S" "S \ {}" and gs: "(g ` S) \ S" - and dist: "\x\S. \y\S. x \ y \ dist (g x) (g y) < dist x y" + and dist: "\x y. \x\S; y\S\ \ x \ y \ dist (g x) (g y) < dist x y" shows "\!x\S. g x = x" proof - let ?D = "(\x. (x, x)) ` S" @@ -1245,7 +1242,7 @@ by (rule compact_continuous_image) (auto intro!: S continuous_Pair continuous_ident simp: continuous_on_eq_continuous_within) - have "\x y e. x \ S \ y \ S \ 0 < e \ dist y x < e \ dist (g y) (g x) < e" + have "\x y \. x \ S \ y \ S \ 0 < \ \ dist y x < \ \ dist (g y) (g x) < \" using dist by fastforce then have "continuous_on S g" by (auto simp: continuous_on_iff) @@ -1260,7 +1257,7 @@ have "g a = a" by (metis \a \ S\ dist gs image_subset_iff le order.strict_iff_not) moreover have "\x. x \ S \ g x = x \ x = a" - using dist[THEN bspec[where x=a]] \g a = a\ and \a\S\ by auto + using \a \ S\ calculation dist by fastforce ultimately show "\!x\S. g x = x" using \a \ S\ by blast qed @@ -1277,9 +1274,9 @@ by (auto simp: diameter_def) lemma diameter_le: - assumes "S \ {} \ 0 \ d" - and no: "\x y. \x \ S; y \ S\ \ norm(x - y) \ d" - shows "diameter S \ d" + assumes "S \ {} \ 0 \ \" + and no: "\x y. \x \ S; y \ S\ \ norm(x - y) \ \" + shows "diameter S \ \" using assms by (auto simp: dist_norm diameter_def intro: cSUP_least) @@ -1288,14 +1285,14 @@ assumes S: "bounded S" "x \ S" "y \ S" shows "dist x y \ diameter S" proof - - from S obtain z d where z: "\x. x \ S \ dist z x \ d" + from S obtain z \ where z: "\x. x \ S \ dist z x \ \" unfolding bounded_def by auto have "bdd_above (case_prod dist ` (S\S))" proof (intro bdd_aboveI, safe) fix a b assume "a \ S" "b \ S" with z[of a] z[of b] dist_triangle[of a b z] - show "dist a b \ 2 * d" + show "dist a b \ 2 * \" by (simp add: dist_commute) qed moreover have "(x,y) \ S\S" using S by auto @@ -1308,25 +1305,25 @@ lemma diameter_lower_bounded: fixes S :: "'a :: metric_space set" assumes S: "bounded S" - and d: "0 < d" "d < diameter S" - shows "\x\S. \y\S. d < dist x y" + and \: "0 < \" "\ < diameter S" + shows "\x\S. \y\S. \ < dist x y" proof (rule ccontr) assume contr: "\ ?thesis" moreover have "S \ {}" - using d by (auto simp: diameter_def) - ultimately have "diameter S \ d" + using \ by (auto simp: diameter_def) + ultimately have "diameter S \ \" by (auto simp: not_less diameter_def intro!: cSUP_least) - with \d < diameter S\ show False by auto + with \\ < diameter S\ show False by auto qed lemma diameter_bounded: assumes "bounded S" shows "\x\S. \y\S. dist x y \ diameter S" - and "\d>0. d < diameter S \ (\x\S. \y\S. dist x y > d)" + and "\\>0. \ < diameter S \ (\x\S. \y\S. dist x y > \)" using diameter_bounded_bound[of S] diameter_lower_bounded[of S] assms by auto -lemma bounded_two_points: "bounded S \ (\e. \x\S. \y\S. dist x y \ e)" +lemma bounded_two_points: "bounded S \ (\\. \x\S. \y\S. dist x y \ \)" by (meson bounded_def diameter_bounded(1)) lemma diameter_compact_attained: @@ -1347,7 +1344,7 @@ lemma diameter_ge_0: assumes "bounded S" shows "0 \ diameter S" - by (metis all_not_in_conv assms diameter_bounded_bound diameter_empty dist_self order_refl) + by (metis assms diameter_bounded(1) diameter_empty dist_self equals0I order.refl) lemma diameter_subset: assumes "S \ T" "bounded T" @@ -1361,38 +1358,43 @@ then have "bdd_above ((\x. case x of (x, xa) \ dist x xa) ` (T \ T))" using \bounded T\ diameter_bounded_bound by (force simp: bdd_above_def) with False \S \ T\ show ?thesis - apply (simp add: diameter_def) - apply (rule cSUP_subset_mono, auto) - done + by (simp add: diameter_def cSUP_subset_mono times_subset_iff) qed lemma diameter_closure: assumes "bounded S" shows "diameter(closure S) = diameter S" proof (rule order_antisym) - have "False" if d_less_d: "diameter S < diameter (closure S)" + have False if d_less_d: "diameter S < diameter (closure S)" proof - - define d where "d = diameter(closure S) - diameter(S)" - have "d > 0" - using that by (simp add: d_def) - then have dle: "diameter(closure(S)) - d / 2 < diameter(closure(S))" + define \ where "\ = diameter(closure S) - diameter(S)" + have "\ > 0" + using that by (simp add: \_def) + then have dle: "diameter(closure(S)) - \ / 2 < diameter(closure(S))" by simp - have dd: "diameter (closure S) - d / 2 = (diameter(closure(S)) + diameter(S)) / 2" - by (simp add: d_def field_split_simps) + have dd: "diameter (closure S) - \ / 2 = (diameter(closure(S)) + diameter(S)) / 2" + by (simp add: \_def field_split_simps) have bocl: "bounded (closure S)" using assms by blast - moreover have "0 \ diameter S" - using assms diameter_ge_0 by blast - ultimately obtain x y where "x \ closure S" "y \ closure S" and xy: "diameter(closure(S)) - d / 2 < dist x y" - by (smt (verit) dle d_less_d d_def dd diameter_lower_bounded) - then obtain x' y' where x'y': "x' \ S" "dist x' x < d/4" "y' \ S" "dist y' y < d/4" - by (metis \0 < d\ zero_less_divide_iff zero_less_numeral closure_approachable) + moreover + have "diameter S \ 0" + using diameter_bounded_bound [OF assms] + by (metis closure_closed discrete_imp_closed dist_le_zero_iff not_less_iff_gr_or_eq + that) + then have "0 < diameter S" + using assms diameter_ge_0 by fastforce + ultimately obtain x y where "x \ closure S" "y \ closure S" and xy: "diameter(closure(S)) - \ / 2 < dist x y" + using diameter_lower_bounded [OF bocl, of "diameter S"] + by (metis d_less_d diameter_bounded(2) dist_not_less_zero dist_self dle + not_less_iff_gr_or_eq) + then obtain x' y' where x'y': "x' \ S" "dist x' x < \/4" "y' \ S" "dist y' y < \/4" + by (metis \0 < \\ zero_less_divide_iff zero_less_numeral closure_approachable) then have "dist x' y' \ diameter S" using assms diameter_bounded_bound by blast - with x'y' have "dist x y \ d / 4 + diameter S + d / 4" + with x'y' have "dist x y \ \ / 4 + diameter S + \ / 4" by (meson add_mono dist_triangle dist_triangle3 less_eq_real_def order_trans) then show ?thesis - using xy d_def by linarith + using xy \_def by linarith qed then show "diameter (closure S) \ diameter S" by fastforce @@ -1410,14 +1412,9 @@ by (metis \\ \ {}\ zero_less_one empty_subsetI equals0I subset_trans that) next case False - { fix x assume "x \ S" - then obtain C where C: "x \ C" "C \ \" - using \S \ \\\ by blast - then obtain r where r: "r>0" "ball x (2*r) \ C" - by (metis field_sum_of_halves half_gt_zero mult.commute mult_2_right ope open_contains_ball) - then have "\r C. r > 0 \ ball x (2*r) \ C \ C \ \" - using C by blast - } + have "\r C. r > 0 \ ball x (2*r) \ C \ C \ \" if "x \ S" for x + by (metis \S \ \\\ field_sum_of_halves half_gt_zero mult.commute mult_2_right + UnionE ope open_contains_ball subset_eq that) then obtain r where r: "\x. x \ S \ r x > 0 \ (\C \ \. ball x (2*r x) \ C)" by metis then have "S \ (\x \ S. ball x (r x))" @@ -1437,10 +1434,6 @@ by (simp add: \0 < \\) show "\B \ \. T \ B" if "T \ S" and dia: "diameter T < \" for T proof (cases "T = {}") - case True - then show ?thesis - using \\ \ {}\ by blast - next case False then obtain y where "y \ T" by blast then have "y \ S" @@ -1449,7 +1442,7 @@ using \S \ \\\ S0 that by blast have "ball y \ \ ball y (r x)" by (metis \_def \S0 \ {}\ \finite S0\ \x \ S0\ empty_is_image finite_imageI finite_less_Inf_iff imageI less_irrefl not_le subset_ball) - also have "... \ ball x (2*r x)" + also have "\ \ ball x (2*r x)" using x by metric finally obtain C where "C \ \" "ball y \ \ C" by (meson r \S0 \ S\ \x \ S0\ dual_order.trans subsetCE) @@ -1459,7 +1452,7 @@ using \y \ T\ dia diameter_bounded_bound by fastforce then show ?thesis by (meson \C \ \\ \ball y \ \ C\ subset_eq) - qed + qed (use \\ \ {}\ in auto) qed qed @@ -1536,30 +1529,30 @@ fixes unproj:: "('b \ 'c) \ 'a" assumes finite_basis: "finite basis" assumes bounded_proj: "\k. k \ basis \ bounded ((\x. x proj k) ` range f)" - assumes proj_unproj: "\e k. k \ basis \ (unproj e) proj k = e k" + assumes proj_unproj: "\\ k. k \ basis \ (unproj \) proj k = \ k" assumes unproj_proj: "\x. unproj (\k. x proj k) = x" - shows "\d\basis. \l::'a. \ r::nat\nat. - strict_mono r \ (\e>0. eventually (\n. \i\d. dist (f (r n) proj i) (l proj i) < e) sequentially)" + shows "\\\basis. \l::'a. \ r::nat\nat. + strict_mono r \ (\\>0. eventually (\n. \i\\. dist (f (r n) proj i) (l proj i) < \) sequentially)" proof safe - fix d :: "'b set" - assume d: "d \ basis" - with finite_basis have "finite d" + fix \ :: "'b set" + assume \: "\ \ basis" + with finite_basis have "finite \" by (blast intro: finite_subset) - from this d show "\l::'a. \r::nat\nat. strict_mono r \ - (\e>0. eventually (\n. \i\d. dist (f (r n) proj i) (l proj i) < e) sequentially)" - proof (induct d) + from this \ show "\l::'a. \r::nat\nat. strict_mono r \ + (\\>0. eventually (\n. \i\\. dist (f (r n) proj i) (l proj i) < \) sequentially)" + proof (induct \) case empty then show ?case unfolding strict_mono_def by auto next - case (insert k d) + case (insert k \) have k[intro]: "k \ basis" using insert by auto have s': "bounded ((\x. x proj k) ` range f)" using k by (rule bounded_proj) obtain l1::"'a" and r1 where r1: "strict_mono r1" - and lr1: "\e > 0. \\<^sub>F n in sequentially. \i\d. dist (f (r1 n) proj i) (l1 proj i) < e" + and lr1: "\\ > 0. \\<^sub>F n in sequentially. \i\\. dist (f (r1 n) proj i) (l1 proj i) < \" using insert by auto have f': "\n. f (r1 n) proj k \ (\x. x proj k) ` range f" by simp @@ -1573,15 +1566,15 @@ using r1 and r2 unfolding r_def o_def strict_mono_def by auto moreover define l where "l = unproj (\i. if i = k then l2 else l1 proj i)" - { fix e::real - assume "e > 0" - from lr1 \e > 0\ have N1: "\\<^sub>F n in sequentially. \i\d. dist (f (r1 n) proj i) (l1 proj i) < e" + { fix \::real + assume "\ > 0" + from lr1 \\ > 0\ have N1: "\\<^sub>F n in sequentially. \i\\. dist (f (r1 n) proj i) (l1 proj i) < \" by blast - from lr2 \e > 0\ have N2: "\\<^sub>F n in sequentially. dist (f (r1 (r2 n)) proj k) l2 < e" + from lr2 \\ > 0\ have N2: "\\<^sub>F n in sequentially. dist (f (r1 (r2 n)) proj k) l2 < \" by (rule tendstoD) - from r2 N1 have N1': "\\<^sub>F n in sequentially. \i\d. dist (f (r1 (r2 n)) proj i) (l1 proj i) < e" + from r2 N1 have N1': "\\<^sub>F n in sequentially. \i\\. dist (f (r1 (r2 n)) proj i) (l1 proj i) < \" by (rule eventually_subseq) - have "\\<^sub>F n in sequentially. \i\insert k d. dist (f (r n) proj i) (l proj i) < e" + have "\\<^sub>F n in sequentially. \i\insert k \. dist (f (r n) proj i) (l proj i) < \" using N1' N2 by eventually_elim (use insert.prems in \auto simp: l_def r_def o_def proj_unproj\) } @@ -1649,37 +1642,37 @@ note lr' = seq_suble [OF lr(2)] { - fix e :: real - assume "e > 0" - from as(2) obtain N where N:"\m n. N \ m \ N \ n \ dist (f m) (f n) < e/2" - unfolding Cauchy_def using \e > 0\ by (meson half_gt_zero) - then obtain M where M:"\n\M. dist ((f \ r) n) l < e/2" + fix \ :: real + assume "\ > 0" + from as(2) obtain N where N:"\m n. N \ m \ N \ n \ dist (f m) (f n) < \/2" + unfolding Cauchy_def using \\ > 0\ by (meson half_gt_zero) + then obtain M where M:"\n\M. dist ((f \ r) n) l < \/2" by (metis dist_self lim_sequentially lr(3)) { fix n :: nat assume n: "n \ max N M" - have "dist ((f \ r) n) l < e/2" + have "dist ((f \ r) n) l < \/2" using n M by auto moreover have "r n \ N" using lr'[of n] n by auto - then have "dist (f n) ((f \ r) n) < e/2" + then have "dist (f n) ((f \ r) n) < \/2" using N and n by auto - ultimately have "dist (f n) l < e" using n M + ultimately have "dist (f n) l < \" using n M by metric } - then have "\N. \n\N. dist (f n) l < e" by blast + then have "\N. \n\N. dist (f n) l < \" by blast } then show "\l\S. (f \ l) sequentially" using \l\S\ unfolding lim_sequentially by auto qed proposition compact_eq_totally_bounded: - "compact S \ complete S \ (\e>0. \k. finite k \ S \ (\x\k. ball x e))" + "compact S \ complete S \ (\\>0. \k. finite k \ S \ (\x\k. ball x \))" (is "_ \ ?rhs") proof assume assms: "?rhs" - then obtain k where k: "\e. 0 < e \ finite (k e)" "\e. 0 < e \ S \ (\x\k e. ball x e)" - by (auto simp: choice_iff') + then obtain k where k: "\\. 0 < \ \ finite (k \)" "\\. 0 < \ \ S \ (\x\k \. ball x \)" + by metis show "compact S" proof cases @@ -1693,21 +1686,21 @@ fix f :: "nat \ 'a" assume f: "\n. f n \ S" - define e where "e n = 1 / (2 * Suc n)" for n - then have [simp]: "\n. 0 < e n" by auto - define B where "B n U = (SOME b. infinite {n. f n \ b} \ (\x. b \ ball x (e n) \ U))" for n U + define \ where "\ n = 1 / (2 * Suc n)" for n + then have [simp]: "\n. 0 < \ n" by auto + define B where "B n U = (SOME b. infinite {n. f n \ b} \ (\x. b \ ball x (\ n) \ U))" for n U { fix n U assume "infinite {n. f n \ U}" - then have "\b\k (e n). infinite {i\{n. f n \ U}. f i \ ball b (e n)}" + then have "\b\k (\ n). infinite {i\{n. f n \ U}. f i \ ball b (\ n)}" using k f by (intro pigeonhole_infinite_rel) (auto simp: subset_eq) then obtain a where - "a \ k (e n)" - "infinite {i \ {n. f n \ U}. f i \ ball a (e n)}" .. - then have "\b. infinite {i. f i \ b} \ (\x. b \ ball x (e n) \ U)" - by (intro exI[of _ "ball a (e n) \ U"] exI[of _ a]) (auto simp: ac_simps) + "a \ k (\ n)" + "infinite {i \ {n. f n \ U}. f i \ ball a (\ n)}" .. + then have "\b. infinite {i. f i \ b} \ (\x. b \ ball x (\ n) \ U)" + by (intro exI[of _ "ball a (\ n) \ U"] exI[of _ a]) (auto simp: ac_simps) from someI_ex[OF this] - have "infinite {i. f i \ B n U}" "\x. B n U \ ball x (e n) \ U" + have "infinite {i. f i \ B n U}" "\x. B n U \ ball x (\ n) \ U" unfolding B_def by auto } note B = this @@ -1718,20 +1711,20 @@ have "infinite {i. f i \ F n}" by (induct n) (auto simp: F_def B) } - then have F: "\n. \x. F (Suc n) \ ball x (e n) \ F n" + then have F: "\n. \x. F (Suc n) \ ball x (\ n) \ F n" using B by (simp add: F_def) then have F_dec: "\m n. m \ n \ F n \ F m" using decseq_SucI[of F] by (auto simp: decseq_def) - - obtain sel where sel: "\k i. i < sel k i" "\k i. f (sel k i) \ F k" - proof (atomize_elim, unfold all_conj_distrib[symmetric], intro choice allI) - fix k i + have "\x>i. f x \ F k" for k i + proof - have "infinite ({n. f n \ F k} - {.. i})" using \infinite {n. f n \ F k}\ by auto from infinite_imp_nonempty[OF this] show "\x>i. f x \ F k" by (simp add: set_eq_iff not_le conj_commute) qed + then obtain sel where sel: "\k i. i < sel k i" "\k i. f (sel k i) \ F k" + by meson define t where "t = rec_nat (sel 0 0) (\n i. sel (Suc n) i)" have "strict_mono t" @@ -1746,11 +1739,11 @@ proof (safe intro!: metric_CauchyI exI elim!: nat_approx_posE) fix r :: real and N n m assume "1 / Suc N < r" "Suc N \ n" "Suc N \ m" - then have "(f \ t) n \ F (Suc N)" "(f \ t) m \ F (Suc N)" "2 * e N < r" - using F_dec t by (auto simp: e_def field_simps) - with F[of N] obtain x where "dist x ((f \ t) n) < e N" "dist x ((f \ t) m) < e N" + then have "(f \ t) n \ F (Suc N)" "(f \ t) m \ F (Suc N)" "2 * \ N < r" + using F_dec t by (auto simp: \_def field_simps) + with F[of N] obtain x where "dist x ((f \ t) n) < \ N" "dist x ((f \ t) m) < \ N" by (auto simp: subset_eq) - with \2 * e N < r\ show "dist ((f \ t) m) ((f \ t) n) < r" + with \2 * \ N < r\ show "dist ((f \ t) m) ((f \ t) n) < r" by metric qed @@ -1758,7 +1751,10 @@ using assms unfolding complete_def by blast qed qed -qed (metis compact_imp_complete compact_imp_seq_compact seq_compact_imp_totally_bounded) +next + show "compact S \ ?rhs" + by (metis compact_imp_complete compact_imp_seq_compact seq_compact_imp_totally_bounded) +qed lemma cauchy_imp_bounded: assumes "Cauchy S" @@ -1772,11 +1768,10 @@ using finite_imp_bounded[of "S ` {1..N}"] by auto then obtain a where a:"\x\S ` {0..N}. dist (S N) x \ a" unfolding bounded_any_center [where a="S N"] by auto - ultimately show "?thesis" - unfolding bounded_any_center [where a="S N"] - apply (intro exI [where x="max a 1"]) - apply (force simp: le_max_iff_disj less_le_not_le) - done + ultimately have "\y\range S. dist (S N) y \ max a 1" + by (force simp: le_max_iff_disj less_le_not_le) + then show ?thesis + unfolding bounded_any_center [where a="S N"] by blast qed instance heine_borel < complete_space @@ -1805,18 +1800,12 @@ fixes S :: "'a::metric_space set" assumes "closed S" and "S \ t" and "complete t" shows "complete S" - using assms complete_Int_closed [of t S] by (simp add: Int_absorb1) + by (metis assms complete_Int_closed inf.absorb_iff2) lemma complete_eq_closed: fixes S :: "('a::complete_space) set" shows "complete S \ closed S" -proof - assume "closed S" then show "complete S" - using subset_UNIV complete_UNIV by (rule complete_closed_subset) -next - assume "complete S" then show "closed S" - by (rule complete_imp_closed) -qed + using complete_UNIV complete_closed_subset complete_imp_closed by auto lemma convergent_eq_Cauchy: fixes S :: "nat \ 'a::complete_space" @@ -1856,7 +1845,8 @@ lemma uniformly_continuous_imp_Cauchy_continuous: fixes f :: "'a::metric_space \ 'b::metric_space" shows "uniformly_continuous_on S f \ Cauchy_continuous_on S f" - by (simp add: uniformly_continuous_on_def Cauchy_continuous_on_def Cauchy_def image_subset_iff) metis + by (metis (no_types, lifting) ext Cauchy_continuous_on_def UNIV_I image_subset_iff + o_apply uniformly_continuous_on_Cauchy) lemma Cauchy_continuous_on_imp_continuous: fixes f :: "'a::metric_space \ 'b::metric_space" @@ -1873,14 +1863,15 @@ have "\ \ x" unfolding tendsto_iff proof (intro strip) - fix e :: real - assume "e>0" - then obtain N where "inverse (Suc N) < e" + fix \ :: real + assume "\>0" + then obtain N where "inverse (Suc N) < \" using reals_Archimedean by blast - then have "\n. N \ n \ dist (\ n) x < e" - by (smt (verit, ccfv_SIG) dx inverse_Suc inverse_less_iff_less inverse_positive_iff_positive of_nat_Suc of_nat_mono) - with \e>0\ show "\\<^sub>F n in sequentially. dist (\ n) x < e" - by (auto simp add: eventually_sequentially \_def) + then have "\n. N \ n \ dist (\ n) x < \" + by (metis dx inverse_positive_iff_positive le_imp_inverse_le nless_le not_less_eq_eq + of_nat_mono order_le_less_trans zero_le_dist) + with \\>0\ show "\\<^sub>F n in sequentially. dist (\ n) x < \" + by (auto simp: eventually_sequentially \_def) qed then have "Cauchy \" by (intro LIMSEQ_imp_Cauchy) @@ -1889,15 +1880,15 @@ have "(f \ \) \ f x" unfolding tendsto_iff proof (intro strip) - fix e :: real - assume "e>0" - then obtain N where N: "\m\N. \n\N. dist ((f \ \) m) ((f \ \) n) < e" + fix \ :: real + assume "\>0" + then obtain N where N: "\m\N. \n\N. dist ((f \ \) m) ((f \ \) n) < \" using Cf unfolding Cauchy_def by presburger moreover have "(f \ \) (Suc(N+N)) = f x" by (simp add: \_def) - ultimately have "\n\N. dist ((f \ \) n) (f x) < e" + ultimately have "\n\N. dist ((f \ \) n) (f x) < \" by (metis add_Suc le_add2) - then show "\\<^sub>F n in sequentially. dist ((f \ \) n) (f x) < e" + then show "\\<^sub>F n in sequentially. dist ((f \ \) n) (f x) < \" using eventually_sequentially by blast qed moreover have "\n. \ dist (f (\ (2*n))) (f x) < \" @@ -1919,13 +1910,19 @@ assumes "closed S" and T: "T \ \" "bounded T" and clof: "\T. T \ \ \ closed T" - and "\\'. \finite \'; \' \ \\ \ S \ \\' \ {}" + and \
: "\\'. \finite \'; \' \ \\ \ S \ \\' \ {}" shows "S \ \\ \ {}" proof - - have "compact (S \ T)" - using \closed S\ clof compact_eq_bounded_closed T by blast - then have "(S \ T) \ \\ \ {}" - by (smt (verit, best) Inf_insert Int_assoc assms compact_imp_fip finite_insert insert_subset) + have "(S \ T) \ \\ \ {}" + proof (rule compact_imp_fip) + show "compact (S \ T)" + using \closed S\ clof compact_eq_bounded_closed T by blast + next + fix F' + assume "finite F'" and "F' \ \" + then show "S \ T \ \ F' \ {}" + by (metis Inf_insert Int_assoc \T \ \\ finite_insert insert_subset \
) + qed (simp add: clof) then show ?thesis by blast qed @@ -1961,7 +1958,7 @@ lemma compact_cball[simp]: fixes x :: "'a::heine_borel" - shows "compact (cball x e)" + shows "compact (cball x \)" using compact_eq_bounded_closed bounded_cball closed_cball by blast lemma compact_frontier_bounded[intro]: @@ -2041,7 +2038,7 @@ lemma infdist_le: "a \ A \ infdist x A \ dist x a" by (auto intro: cINF_lower simp add: infdist_def) -lemma infdist_le2: "a \ A \ dist x a \ d \ infdist x A \ d" +lemma infdist_le2: "a \ A \ dist x a \ \ \ infdist x A \ \" by (auto intro!: cINF_lower2 simp add: infdist_def) lemma infdist_zero[simp]: "a \ A \ infdist a A = 0" @@ -2063,13 +2060,13 @@ proof (rule cInf_greatest) from \A \ {}\ show "{dist x y + dist y a |a. a \ A} \ {}" by simp - fix d - assume "d \ {dist x y + dist y a |a. a \ A}" - then obtain a where d: "d = dist x y + dist y a" "a \ A" + fix \ + assume "\ \ {dist x y + dist y a |a. a \ A}" + then obtain a where \: "\ = dist x y + dist y a" "a \ A" by auto - show "infdist x A \ d" + show "infdist x A \ \" using infdist_notempty[OF \A \ {}\] - by (metis d dist_commute dist_triangle3 infdist_le2) + by (metis \ dist_commute dist_triangle3 infdist_le2) qed also have "\ = dist x y + infdist y A" proof (rule cInf_eq, safe) @@ -2079,7 +2076,7 @@ by (auto intro: infdist_le) next fix i - assume inf: "\d. d \ {dist x y + dist y a |a. a \ A} \ i \ d" + assume inf: "\\. \ \ {dist x y + dist y a |a. a \ A} \ i \ \" then have "i - dist x y \ infdist y A" unfolding infdist_notempty[OF \A \ {}\] using \a \ A\ by (intro cINF_greatest) (auto simp: field_simps) @@ -2112,12 +2109,12 @@ assume x: "infdist x A = 0" then obtain a where "a \ A" by atomize_elim (metis all_not_in_conv assms) - have False if "e > 0" "\ (\y\A. dist y x < e)" for e + have False if "\ > 0" "\ (\y\A. dist y x < \)" for \ proof - - have "infdist x A \ e" using \a \ A\ + have "infdist x A \ \" using \a \ A\ unfolding infdist_def using that by (force simp: dist_commute intro: cINF_greatest) - with x \e > 0\ show False by auto + with x \\ > 0\ show False by auto qed then show "x \ closure A" using closure_approachable by blast @@ -2179,12 +2176,12 @@ fix z assume H: "dist x z * 2 < infdist x T" "dist y z * 2 < infdist y S" have "2 * dist x y \ 2 * dist x z + 2 * dist y z" by metric - also have "... < infdist x T + infdist y S" + also have "\ < infdist x T + infdist y S" using H by auto finally have "dist x y < infdist x T \ dist x y < infdist y S" by auto then show False - using infdist_le[OF \x \ S\, of y] infdist_le[OF \y \ T\, of x] by (auto simp add: dist_commute) + using infdist_le[OF \x \ S\, of y] infdist_le[OF \y \ T\, of x] by (auto simp: dist_commute) qed then have E: "U \ V = {}" unfolding U_def V_def by auto @@ -2197,17 +2194,17 @@ assumes f: "(f \ l) F" shows "((\x. infdist (f x) A) \ infdist l A) F" proof (rule tendstoI) - fix e ::real - assume "e > 0" + fix \ ::real + assume "\ > 0" from tendstoD[OF f this] - show "eventually (\x. dist (infdist (f x) A) (infdist l A) < e) F" + show "eventually (\x. dist (infdist (f x) A) (infdist l A) < \) F" proof (eventually_elim) fix x from infdist_triangle[of l A "f x"] infdist_triangle[of "f x" A l] have "dist (infdist (f x) A) (infdist l A) \ dist (f x) l" by (simp add: dist_commute dist_real_def) - also assume "dist (f x) l < e" - finally show "dist (infdist (f x) A) (infdist l A) < e" . + also assume "dist (f x) l < \" + finally show "dist (infdist (f x) A) (infdist l A) < \" . qed qed @@ -2225,27 +2222,27 @@ fixes A::"'a::heine_borel set" assumes "A \ {}" assumes "compact A" - assumes "e > 0" - shows "compact {x. infdist x A \ e}" + assumes "\ > 0" + shows "compact {x. infdist x A \ \}" proof - - from continuous_closed_vimage[of "{0..e}" "\x. infdist x A"] + from continuous_closed_vimage[of "{0..\}" "\x. infdist x A"] continuous_infdist[OF continuous_ident, of _ UNIV A] - have "closed {x. infdist x A \ e}" by (auto simp: vimage_def infdist_nonneg) + have "closed {x. infdist x A \ \}" by (auto simp: vimage_def infdist_nonneg) moreover from assms obtain x0 b where b: "\x. x \ A \ dist x0 x \ b" "closed A" by (auto simp: compact_eq_bounded_closed bounded_def) { fix y - assume "infdist y A \ e" + assume "infdist y A \ \" moreover from infdist_attains_inf[OF \closed A\ \A \ {}\, of y] obtain z where "z \ A" "infdist y A = dist y z" by blast ultimately - have "dist x0 y \ b + e" using b by metric + have "dist x0 y \ b + \" using b by metric } then - have "bounded {x. infdist x A \ e}" - by (auto simp: bounded_any_center[where a=x0] intro!: exI[where x="b + e"]) - ultimately show "compact {x. infdist x A \ e}" + have "bounded {x. infdist x A \ \}" + by (auto simp: bounded_any_center[where a=x0] intro!: exI[where x="b + \"]) + ultimately show "compact {x. infdist x A \ \}" by (simp add: compact_eq_bounded_closed) qed @@ -2255,14 +2252,14 @@ proposition separate_point_closed: fixes S :: "'a::heine_borel set" assumes "closed S" and "a \ S" - shows "\d>0. \x\S. d \ dist a x" + shows "\\>0. \x\S. \ \ dist a x" by (metis assms distance_attains_inf empty_iff gt_ex zero_less_dist_iff) proposition separate_compact_closed: fixes S T :: "'a::heine_borel set" assumes "compact S" and T: "closed T" "S \ T = {}" - shows "\d>0. \x\S. \y\T. d \ dist x y" + shows "\\>0. \x\S. \y\T. \ \ dist x y" proof cases assume "S \ {} \ T \ {}" then have "S \ {}" "T \ {}" by auto @@ -2283,7 +2280,7 @@ assumes S: "closed S" and T: "compact T" and dis: "S \ T = {}" - shows "\d>0. \x\S. \y\T. d \ dist x y" + shows "\\>0. \x\S. \y\T. \ \ dist x y" by (metis separate_compact_closed[OF T S] dis dist_commute inf_commute) proposition compact_in_open_separated: @@ -2291,24 +2288,24 @@ assumes A: "A \ {}" "compact A" assumes "open B" assumes "A \ B" - obtains e where "e > 0" "{x. infdist x A \ e} \ B" + obtains \ where "\ > 0" "{x. infdist x A \ \} \ B" proof atomize_elim have "closed (- B)" "compact A" "- B \ A = {}" using assms by (auto simp: open_Diff compact_eq_bounded_closed) from separate_closed_compact[OF this] obtain d'::real where d': "d'>0" "\x y. x \ B \ y \ A \ d' \ dist x y" by auto - define d where "d = d' / 2" - hence "d>0" "d < d'" using d' by auto - with d' have d: "\x y. x \ B \ y \ A \ d < dist x y" + define \ where "\ = d' / 2" + hence "\>0" "\ < d'" using d' by auto + with d' have \: "\x y. x \ B \ y \ A \ \ < dist x y" by force - show "\e>0. {x. infdist x A \ e} \ B" + show "\\>0. {x. infdist x A \ \} \ B" proof (rule ccontr) - assume "\e. 0 < e \ {x. infdist x A \ e} \ B" - with \d > 0\ obtain x where x: "infdist x A \ d" "x \ B" + assume "\\. 0 < \ \ {x. infdist x A \ \} \ B" + with \\ > 0\ obtain x where x: "infdist x A \ \" "x \ B" by auto then show False - by (metis A compact_eq_bounded_closed infdist_attains_inf x d linorder_not_less) + by (metis A compact_eq_bounded_closed infdist_attains_inf x \ linorder_not_less) qed qed @@ -2316,8 +2313,8 @@ section \Uniform Continuity\ lemma uniformly_continuous_onE: - assumes "uniformly_continuous_on s f" "0 < e" - obtains d where "d>0" "\x x'. \x\s; x'\s; dist x' x < d\ \ dist (f x') (f x) < e" + assumes "uniformly_continuous_on s f" "0 < \" + obtains \ where "\>0" "\x x'. \x\s; x'\s; dist x' x < \\ \ dist (f x') (f x) < \" using assms by (auto simp: uniformly_continuous_on_def) @@ -2332,14 +2329,14 @@ and y: "\n. y n \ s" and xy: "((\n. dist (x n) (y n)) \ 0) sequentially" { - fix e :: real - assume "e > 0" - then obtain d where "d > 0" and d: "\x\s. \x'\s. dist x' x < d \ dist (f x') (f x) < e" + fix \ :: real + assume "\ > 0" + then obtain \ where "\ > 0" and \: "\x\s. \x'\s. dist x' x < \ \ dist (f x') (f x) < \" by (metis \?lhs\ uniformly_continuous_onE) - obtain N where N: "\n\N. dist (x n) (y n) < d" - using xy[unfolded lim_sequentially dist_norm] and \d>0\ by auto - then have "\N. \n\N. dist (f (x n)) (f (y n)) < e" - using d x y by blast + obtain N where N: "\n\N. dist (x n) (y n) < \" + using xy[unfolded lim_sequentially dist_norm] and \\>0\ by auto + then have "\N. \n\N. dist (f (x n)) (f (y n)) < \" + using \ x y by blast } then have "((\n. dist (f(x n)) (f(y n))) \ 0) sequentially" unfolding lim_sequentially and dist_real_def by auto @@ -2349,32 +2346,31 @@ assume ?rhs { assume "\ ?lhs" - then obtain e where "e > 0" "\d>0. \x\s. \x'\s. dist x' x < d \ \ dist (f x') (f x) < e" + then obtain \ where "\ > 0" "\\>0. \x\s. \x'\s. dist x' x < \ \ \ dist (f x') (f x) < \" unfolding uniformly_continuous_on_def by auto then obtain fa where fa: - "\x. 0 < x \ fst (fa x) \ s \ snd (fa x) \ s \ dist (fst (fa x)) (snd (fa x)) < x \ \ dist (f (fst (fa x))) (f (snd (fa x))) < e" - using choice[of "\d x. d>0 \ fst x \ s \ snd x \ s \ dist (snd x) (fst x) < d \ \ dist (f (snd x)) (f (fst x)) < e"] + "\x. 0 < x \ fst (fa x) \ s \ snd (fa x) \ s \ dist (fst (fa x)) (snd (fa x)) < x \ \ dist (f (fst (fa x))) (f (snd (fa x))) < \" + using choice[of "\\ x. \>0 \ fst x \ s \ snd x \ s \ dist (snd x) (fst x) < \ \ \ dist (f (snd x)) (f (fst x)) < \"] by (auto simp: Bex_def dist_commute) define x where "x n = fst (fa (inverse (real n + 1)))" for n define y where "y n = snd (fa (inverse (real n + 1)))" for n have xyn: "\n. x n \ s \ y n \ s" and xy0: "\n. dist (x n) (y n) < inverse (real n + 1)" - and fxy:"\n. \ dist (f (x n)) (f (y n)) < e" + and fxy:"\n. \ dist (f (x n)) (f (y n)) < \" unfolding x_def and y_def using fa by auto { - fix e :: real - assume "e > 0" - then obtain N :: nat where "N \ 0" and N: "0 < inverse (real N) \ inverse (real N) < e" - unfolding real_arch_inverse[of e] by auto - with xy0 have "\N. \n\N. dist (x n) (y n) < e" + fix \ :: real + assume "\ > 0" + then obtain N :: nat where "N \ 0" and N: "0 < inverse (real N) \ inverse (real N) < \" + unfolding real_arch_inverse[of \] by auto + with xy0 have "\N. \n\N. dist (x n) (y n) < \" by (metis order.strict_trans inverse_positive_iff_positive less_imp_inverse_less nat_le_real_less) } - then have "\e>0. \N. \n\N. dist (f (x n)) (f (y n)) < e" - using \?rhs\[THEN spec[where x=x], THEN spec[where x=y]] and xyn - unfolding lim_sequentially dist_real_def by auto - then have False using fxy and \e>0\ by auto + then have "\\>0. \N. \n\N. dist (f (x n)) (f (y n)) < \" + using \?rhs\ xyn by (auto simp: lim_sequentially dist_real_def) + then have False using fxy and \\>0\ by auto } then show ?lhs unfolding uniformly_continuous_on_def by blast @@ -2388,9 +2384,9 @@ lemma Heine_Borel_lemma: assumes "compact S" and Ssub: "S \ \\" and opn: "\G. G \ \ \ open G" - obtains e where "0 < e" "\x. x \ S \ \G \ \. ball x e \ G" + obtains \ where "0 < \" "\x. x \ S \ \G \ \. ball x \ \ G" proof - - have False if neg: "\e. 0 < e \ \x \ S. \G \ \. \ ball x e \ G" + have False if neg: "\\. 0 < \ \ \x \ S. \G \ \. \ ball x \ \ G" proof - have "\x \ S. \G \ \. \ ball x (1 / Suc n) \ G" for n using neg by simp @@ -2400,29 +2396,29 @@ using \compact S\ compact_def that by metis then obtain G where "l \ G" "G \ \" using Ssub by auto - then obtain e where "0 < e" and e: "\z. dist z l < e \ z \ G" + then obtain \ where "0 < \" and \: "\z. dist z l < \ \ z \ G" using opn open_dist by blast - obtain N1 where N1: "\n. n \ N1 \ dist (f (r n)) l < e/2" - by (metis \0 < e\ half_gt_zero lim_sequentially o_apply to_l) - obtain N2 where N2: "of_nat N2 > 2/e" + obtain N1 where N1: "\n. n \ N1 \ dist (f (r n)) l < \/2" + by (metis \0 < \\ half_gt_zero lim_sequentially o_apply to_l) + obtain N2 where N2: "of_nat N2 > 2/\" using reals_Archimedean2 by blast obtain x where "x \ ball (f (r (max N1 N2))) (1 / real (Suc (r (max N1 N2))))" and "x \ G" using fG [OF \G \ \\, of "r (max N1 N2)"] by blast then have "dist (f (r (max N1 N2))) x < 1 / real (Suc (r (max N1 N2)))" by simp - also have "... \ 1 / real (Suc (max N1 N2))" + also have "\ \ 1 / real (Suc (max N1 N2))" by (meson Suc_le_mono \strict_mono r\ inverse_of_nat_le nat.discI seq_suble) - also have "... \ 1 / real (Suc N2)" + also have "\ \ 1 / real (Suc N2)" by (simp add: field_simps) - also have "... < e/2" - using N2 \0 < e\ by (simp add: field_simps) - finally have "dist (f (r (max N1 N2))) x < e/2" . - moreover have "dist (f (r (max N1 N2))) l < e/2" + also have "\ < \/2" + using N2 \0 < \\ by (simp add: field_simps) + finally have "dist (f (r (max N1 N2))) x < \/2" . + moreover have "dist (f (r (max N1 N2))) l < \/2" using N1 max.cobounded1 by blast - ultimately have "dist x l < e" + ultimately have "dist x l < \" by metric then show ?thesis - using e \x \ G\ by blast + using \ \x \ G\ by blast qed then show ?thesis by (meson that) @@ -2430,33 +2426,33 @@ lemma compact_uniformly_equicontinuous: assumes "compact S" - and cont: "\x e. \x \ S; 0 < e\ - \ \d. 0 < d \ - (\f \ \. \x' \ S. dist x' x < d \ dist (f x') (f x) < e)" - and "0 < e" - obtains d where "0 < d" - "\f x x'. \f \ \; x \ S; x' \ S; dist x' x < d\ \ dist (f x') (f x) < e" + and cont: "\x \. \x \ S; 0 < \\ + \ \\. 0 < \ \ + (\f \ \. \x' \ S. dist x' x < \ \ dist (f x') (f x) < \)" + and "0 < \" + obtains \ where "0 < \" + "\f x x'. \f \ \; x \ S; x' \ S; dist x' x < \\ \ dist (f x') (f x) < \" proof - - obtain d where d_pos: "\x e. \x \ S; 0 < e\ \ 0 < d x e" - and d_dist : "\x x' e f. \dist x' x < d x e; x \ S; x' \ S; 0 < e; f \ \\ \ dist (f x') (f x) < e" + obtain \ where d_pos: "\x \. \x \ S; 0 < \\ \ 0 < \ x \" + and d_dist : "\x x' \ f. \dist x' x < \ x \; x \ S; x' \ S; 0 < \; f \ \\ \ dist (f x') (f x) < \" using cont by metis - let ?\ = "((\x. ball x (d x (e/2))) ` S)" + let ?\ = "((\x. ball x (\ x (\/2))) ` S)" have Ssub: "S \ \ ?\" - using \0 < e\ d_pos by auto + using \0 < \\ d_pos by auto then obtain k where "0 < k" and k: "\x. x \ S \ \G \ ?\. ball x k \ G" by (rule Heine_Borel_lemma [OF \compact S\]) auto - moreover have "dist (f v) (f u) < e" if "f \ \" "u \ S" "v \ S" "dist v u < k" for f u v + moreover have "dist (f v) (f u) < \" if "f \ \" "u \ S" "v \ S" "dist v u < k" for f u v proof - obtain G where "G \ ?\" "u \ G" "v \ G" using k that by (metis \dist v u < k\ \u \ S\ \0 < k\ centre_in_ball subsetD dist_commute mem_ball) - then obtain w where w: "dist w u < d w (e/2)" "dist w v < d w (e/2)" "w \ S" + then obtain w where w: "dist w u < \ w (\/2)" "dist w v < \ w (\/2)" "w \ S" by auto - with that d_dist have "dist (f w) (f v) < e/2" - by (metis \0 < e\ dist_commute half_gt_zero) + with that d_dist have "dist (f w) (f v) < \/2" + by (metis \0 < \\ dist_commute half_gt_zero) moreover - have "dist (f w) (f u) < e/2" - using that d_dist w by (metis \0 < e\ dist_commute divide_pos_pos zero_less_numeral) + have "dist (f w) (f u) < \/2" + using that d_dist w by (metis \0 < \\ dist_commute divide_pos_pos zero_less_numeral) ultimately show ?thesis using dist_triangle_half_r by blast qed @@ -2476,8 +2472,8 @@ lemma continuous_on_closure: "continuous_on (closure S) f \ - (\x e. x \ closure S \ 0 < e - \ (\d. 0 < d \ (\y. y \ S \ dist y x < d \ dist (f y) (f x) < e)))" + (\x \. x \ closure S \ 0 < \ + \ (\\. 0 < \ \ (\y. y \ S \ dist y x < \ \ dist (f y) (f x) < \)))" (is "?lhs = ?rhs") proof assume ?lhs then show ?rhs @@ -2486,27 +2482,27 @@ assume R [rule_format]: ?rhs show ?lhs proof - fix x and e::real - assume "0 < e" and x: "x \ closure S" + fix x and \::real + assume "0 < \" and x: "x \ closure S" obtain \::real where "\ > 0" - and \: "\y. \y \ S; dist y x < \\ \ dist (f y) (f x) < e/2" - using R [of x "e/2"] \0 < e\ x by auto - have "dist (f y) (f x) \ e" if y: "y \ closure S" and dyx: "dist y x < \/2" for y + and \: "\y. \y \ S; dist y x < \\ \ dist (f y) (f x) < \/2" + using R [of x "\/2"] \0 < \\ x by auto + have "dist (f y) (f x) \ \" if y: "y \ closure S" and dyx: "dist y x < \/2" for y proof - obtain \'::real where "\' > 0" - and \': "\z. \z \ S; dist z y < \'\ \ dist (f z) (f y) < e/2" - using R [of y "e/2"] \0 < e\ y by auto + and \': "\z. \z \ S; dist z y < \'\ \ dist (f z) (f y) < \/2" + using R [of y "\/2"] \0 < \\ y by auto obtain z where "z \ S" and z: "dist z y < min \' \ / 2" using closure_approachable y by (metis \0 < \'\ \0 < \\ divide_pos_pos min_less_iff_conj zero_less_numeral) - have "dist (f z) (f y) < e/2" + have "dist (f z) (f y) < \/2" using \' [OF \z \ S\] z \0 < \'\ by metric - moreover have "dist (f z) (f x) < e/2" + moreover have "dist (f z) (f x) < \/2" using \[OF \z \ S\] z dyx by metric ultimately show ?thesis by metric qed - then show "\d>0. \x'\closure S. dist x' x < d \ dist (f x') (f x) \ e" + then show "\\>0. \x'\closure S. dist x' x < \ \ dist (f x') (f x) \ \" by (rule_tac x="\/2" in exI) (simp add: \\ > 0\) qed qed @@ -2519,9 +2515,9 @@ (is "?lhs = ?rhs") proof - have "continuous_on (closure S) f \ - (\x \ closure S. continuous (at x within S) f)" + (\x \ closure S. continuous (at x within S) f)" by (force simp: continuous_on_closure continuous_within_eps_delta) - also have "... = ?rhs" + also have "\ = ?rhs" by (force simp: continuous_within_sequentially) finally show ?thesis . qed @@ -2533,38 +2529,38 @@ shows "uniformly_continuous_on (closure S) f" unfolding uniformly_continuous_on_def proof (intro allI impI) - fix e::real - assume "0 < e" - then obtain d::real - where "d>0" - and d: "\x x'. \x\S; x'\S; dist x' x < d\ \ dist (f x') (f x) < e/3" - using ucont [unfolded uniformly_continuous_on_def, rule_format, of "e/3"] by auto - show "\d>0. \x\closure S. \x'\closure S. dist x' x < d \ dist (f x') (f x) < e" - proof (rule exI [where x="d/3"], clarsimp simp: \d > 0\) + fix \::real + assume "0 < \" + then obtain \::real + where "\>0" + and \: "\x x'. \x\S; x'\S; dist x' x < \\ \ dist (f x') (f x) < \/3" + using ucont [unfolded uniformly_continuous_on_def, rule_format, of "\/3"] by auto + show "\\>0. \x\closure S. \x'\closure S. dist x' x < \ \ dist (f x') (f x) < \" + proof (rule exI [where x="\/3"], clarsimp simp: \\ > 0\) fix x y - assume x: "x \ closure S" and y: "y \ closure S" and dyx: "dist y x * 3 < d" + assume x: "x \ closure S" and y: "y \ closure S" and dyx: "dist y x * 3 < \" obtain d1::real where "d1 > 0" - and d1: "\w. \w \ closure S; dist w x < d1\ \ dist (f w) (f x) < e/3" - using cont [unfolded continuous_on_iff, rule_format, of "x" "e/3"] \0 < e\ x by auto - obtain x' where "x' \ S" and x': "dist x' x < min d1 (d / 3)" + and d1: "\w. \w \ closure S; dist w x < d1\ \ dist (f w) (f x) < \/3" + using cont [unfolded continuous_on_iff, rule_format, of "x" "\/3"] \0 < \\ x by auto + obtain x' where "x' \ S" and x': "dist x' x < min d1 (\ / 3)" using closure_approachable [of x S] - by (metis \0 < d1\ \0 < d\ divide_pos_pos min_less_iff_conj x zero_less_numeral) + by (metis \0 < d1\ \0 < \\ divide_pos_pos min_less_iff_conj x zero_less_numeral) obtain d2::real where "d2 > 0" - and d2: "\w \ closure S. dist w y < d2 \ dist (f w) (f y) < e/3" - using cont [unfolded continuous_on_iff, rule_format, of "y" "e/3"] \0 < e\ y by auto - obtain y' where "y' \ S" and y': "dist y' y < min d2 (d / 3)" + and d2: "\w \ closure S. dist w y < d2 \ dist (f w) (f y) < \/3" + using cont [unfolded continuous_on_iff, rule_format, of "y" "\/3"] \0 < \\ y by auto + obtain y' where "y' \ S" and y': "dist y' y < min d2 (\ / 3)" using closure_approachable [of y S] - by (metis \0 < d2\ \0 < d\ divide_pos_pos min_less_iff_conj y zero_less_numeral) - have "dist x' x < d/3" using x' by auto - then have "dist x' y' < d" + by (metis \0 < d2\ \0 < \\ divide_pos_pos min_less_iff_conj y zero_less_numeral) + have "dist x' x < \/3" using x' by auto + then have "dist x' y' < \" using dyx y' by metric - then have "dist (f x') (f y') < e/3" - by (rule d [OF \y' \ S\ \x' \ S\]) - moreover have "dist (f x') (f x) < e/3" using \x' \ S\ closure_subset x' d1 + then have "dist (f x') (f y') < \/3" + by (rule \ [OF \y' \ S\ \x' \ S\]) + moreover have "dist (f x') (f x) < \/3" using \x' \ S\ closure_subset x' d1 by (simp add: closure_def) - moreover have "dist (f y') (f y) < e/3" using \y' \ S\ closure_subset y' d2 + moreover have "dist (f y') (f y) < \/3" using \y' \ S\ closure_subset y' d2 by (simp add: closure_def) - ultimately show "dist (f y) (f x) < e" by metric + ultimately show "dist (f y) (f x) < \" by metric qed qed @@ -2594,28 +2590,27 @@ show "(\n. f (xs' n)) \ l" proof (rule tendstoI) - fix e::real assume "e > 0" - define e' where "e' \ e/2" - have "e' > 0" using \e > 0\ by (simp add: e'_def) + fix \::real assume "\ > 0" + define e' where "e' \ \/2" + have "e' > 0" using \\ > 0\ by (simp add: e'_def) have "\\<^sub>F n in sequentially. dist (f (xs n)) l < e'" by (simp add: \0 < e'\ l tendstoD) moreover - from uc[unfolded uniformly_continuous_on_def, rule_format, OF \e' > 0\] - obtain d where d: "d > 0" "\x x'. x \ X \ x' \ X \ dist x x' < d \ dist (f x) (f x') < e'" - by auto - have "\\<^sub>F n in sequentially. dist (xs n) (xs' n) < d" - by (auto intro!: \0 < d\ order_tendstoD tendsto_eq_intros xs xs') + obtain \ where \: "\ > 0" "\x x'. x \ X \ x' \ X \ dist x x' < \ \ dist (f x) (f x') < e'" + by (metis \0 < e'\ uc uniformly_continuous_on_def) + have "\\<^sub>F n in sequentially. dist (xs n) (xs' n) < \" + by (auto intro!: \0 < \\ order_tendstoD tendsto_eq_intros xs xs') ultimately - show "\\<^sub>F n in sequentially. dist (f (xs' n)) l < e" + show "\\<^sub>F n in sequentially. dist (f (xs' n)) l < \" proof eventually_elim case (elim n) have "dist (f (xs' n)) l \ dist (f (xs n)) (f (xs' n)) + dist (f (xs n)) l" by metric also have "dist (f (xs n)) (f (xs' n)) < e'" - by (auto intro!: d xs \xs' _ \ _\ elim) + by (auto intro!: \ xs \xs' _ \ _\ elim) also note \dist (f (xs n)) l < e'\ - also have "e' + e' = e" by (simp add: e'_def) + also have "e' + e' = \" by (simp add: e'_def) finally show ?case by simp qed qed @@ -2638,15 +2633,14 @@ have "uniformly_continuous_on (closure X) ?g" unfolding uniformly_continuous_on_def proof safe - fix e::real assume "e > 0" - define e' where "e' \ e / 3" - have "e' > 0" using \e > 0\ by (simp add: e'_def) - from uc[unfolded uniformly_continuous_on_def, rule_format, OF \0 < e'\] - obtain d where "d > 0" and d: "\x x'. x \ X \ x' \ X \ dist x' x < d \ dist (f x') (f x) < e'" - by auto - define d' where "d' = d / 3" - have "d' > 0" using \d > 0\ by (simp add: d'_def) - show "\d>0. \x\closure X. \x'\closure X. dist x' x < d \ dist (?g x') (?g x) < e" + fix \::real assume "\ > 0" + define e' where "e' \ \ / 3" + have "e' > 0" using \\ > 0\ by (simp add: e'_def) + obtain \ where "\ > 0" and \: "\x x'. x \ X \ x' \ X \ dist x' x < \ \ dist (f x') (f x) < e'" + using \0 < e'\ uc uniformly_continuous_onE by blast + define d' where "d' = \ / 3" + have "d' > 0" using \\ > 0\ by (simp add: d'_def) + show "\\>0. \x\closure X. \x'\closure X. dist x' x < \ \ dist (?g x') (?g x) < \" proof (safe intro!: exI[where x=d'] \d' > 0\) fix x x' assume x: "x \ closure X" and x': "x' \ closure X" and dist: "dist x' x < d'" then obtain xs xs' where xs: "xs \ x" "\n. xs n \ X" @@ -2656,7 +2650,8 @@ and "\\<^sub>F n in sequentially. dist (xs n) x < d'" by (auto intro!: \0 < d'\ order_tendstoD tendsto_eq_intros xs xs') moreover - have "(\x. f (xs x)) \ y x" if "x \ closure X" "x \ X" "xs \ x" "\n. xs n \ X" for xs x + have "(\x. f (xs x)) \ y x" + if "x \ closure X" "x \ X" "xs \ x" "\n. xs n \ X" for xs x using that not_eventuallyD by (force intro!: filterlim_compose[OF y[OF \x \ closure X\]] simp: filterlim_at) then have "(\x. f (xs' x)) \ ?g x'" "(\x. f (xs x)) \ ?g x" @@ -2666,7 +2661,7 @@ "\\<^sub>F n in sequentially. dist (f (xs n)) (?g x) < e'" by (auto intro!: \0 < e'\ order_tendstoD tendsto_eq_intros) ultimately - have "\\<^sub>F n in sequentially. dist (?g x') (?g x) < e" + have "\\<^sub>F n in sequentially. dist (?g x') (?g x) < \" proof eventually_elim case (elim n) have "dist (?g x') (?g x) \ @@ -2674,17 +2669,18 @@ by (metis add.commute add_le_cancel_left dist_commute dist_triangle dist_triangle_le) also from \dist (xs' n) x' < d'\ \dist x' x < d'\ \dist (xs n) x < d'\ - have "dist (xs' n) (xs n) < d" unfolding d'_def by metric + have "dist (xs' n) (xs n) < \" unfolding d'_def by metric with \xs _ \ X\ \xs' _ \ X\ have "dist (f (xs' n)) (f (xs n)) < e'" - by (rule d) + by (rule \) also note \dist (f (xs' n)) (?g x') < e'\ also note \dist (f (xs n)) (?g x) < e'\ finally show ?case by (simp add: e'_def) qed - then show "dist (?g x') (?g x) < e" by simp + then show "dist (?g x') (?g x) < \" by simp qed qed - moreover have "f x = ?g x" if "x \ X" for x using that by simp + moreover have "f x = ?g x" if "x \ X" for x + using that by simp moreover { fix Y h x @@ -2702,8 +2698,8 @@ using \x \ X\ not_eventuallyD xs(2) by (force intro!: filterlim_compose[OF y[OF \x \ closure X\]] simp: filterlim_at xs) with hx have "h x = y x" by (rule LIMSEQ_unique) - } then - have "h x = ?g x" + } + then have "h x = ?g x" using extension by auto } ultimately show ?thesis .. @@ -2713,28 +2709,39 @@ fixes f :: "'a :: heine_borel \ 'b :: heine_borel" assumes "uniformly_continuous_on S f" "bounded S" shows "bounded(f ` S)" - by (metis (no_types) assms bounded_closure_image compact_closure compact_continuous_image compact_eq_bounded_closed image_cong uniformly_continuous_imp_continuous uniformly_continuous_on_extension_on_closure) +proof - + obtain g where "uniformly_continuous_on (closure S) g" and g: "\x. x \ S \ f x = g x" + using uniformly_continuous_on_extension_on_closure assms by metis + then have "compact (g ` closure S)" + using \bounded S\ compact_closure compact_continuous_image + uniformly_continuous_imp_continuous by blast + then show ?thesis + using g bounded_closure_image compact_eq_bounded_closed + by auto +qed section \With Abstract Topology (TODO: move and remove dependency?)\ lemma openin_contains_ball: "openin (top_of_set T) S \ - S \ T \ (\x \ S. \e. 0 < e \ ball x e \ T \ S)" + S \ T \ (\x \ S. \\. 0 < \ \ ball x \ \ T \ S)" (is "?lhs = ?rhs") proof assume ?lhs then show ?rhs by (metis IntD2 Int_commute Int_lower1 Int_mono inf.idem openE openin_open) next - assume ?rhs - then show ?lhs - by (smt (verit) open_ball Int_commute Int_iff centre_in_ball in_mono openin_open_Int openin_subopen) + assume R: ?rhs + then have "\x\S. \R. openin (top_of_set T) R \ x \ R \ R \ S" + by (metis open_ball Int_iff centre_in_ball inf_sup_aci(1) openin_open_Int subsetD) + with R show ?lhs + using openin_subopen by auto qed lemma openin_contains_cball: "openin (top_of_set T) S \ - S \ T \ (\x \ S. \e. 0 < e \ cball x e \ T \ S)" + S \ T \ (\x \ S. \\. 0 < \ \ cball x \ \ T \ S)" by (fastforce simp: openin_contains_ball intro: exI [where x="_/2"]) @@ -2752,7 +2759,7 @@ obtains a where "\n. a \ S n" proof - from assms(2) obtain x where x: "\n. x n \ S n" - using choice[of "\n x. x \ S n"] by auto + by (meson ex_in_conv) from assms(4,1) have "seq_compact (S 0)" by (simp add: bounded_closed_imp_seq_compact) then obtain l r where lr: "l \ S 0" "strict_mono r" "(x \ r) \ l" @@ -2766,10 +2773,8 @@ using x and assms(3) and lr(2) [THEN seq_suble] by auto then have "\i. (x \ r) (i + n) \ S n" using assms(3) by (fast intro!: le_add2) - moreover have "(\i. (x \ r) (i + n)) \ l" - using lr(3) by (rule LIMSEQ_ignore_initial_segment) ultimately show "l \ S n" - by (metis closed_sequentially) + by (metis LIMSEQ_ignore_initial_segment closed_sequential_limits lr(3)) qed then show ?thesis using that by blast @@ -2782,7 +2787,7 @@ assumes "\n. closed (S n)" "\n. S n \ {}" "\m n. m \ n \ S n \ S m" - "\e. e>0 \ \n. \x\S n. \y\S n. dist x y < e" + "\\. \>0 \ \n. \x\S n. \y\S n. dist x y < \" obtains a where "\n. a \ S n" proof - obtain t where t: "\n. t n \ S n" @@ -2814,7 +2819,7 @@ then obtain N :: nat where N: "\n\N. dist (t n) l < \" using l[unfolded lim_sequentially] by auto have "t (max n N) \ S n" - by (meson assms(3) contra_subsetD max.cobounded1 t) + by (meson assms(3) subsetD max.cobounded1 t) then have "\y\S n. dist y l < \" using N max.cobounded2 by blast } @@ -2835,11 +2840,8 @@ proof - obtain a where a: "\n. a \ S n" using decreasing_closed_nest[of S] using assms by auto - { fix b - assume b: "b \ \(range S)" - then have "dist a b = 0" - by (meson InterE a \
linorder_neq_iff linorder_not_less range_eqI zero_le_dist) - } + then have "dist a b = 0" if "b \ \(range S)" for b + by (meson that InterE \
linorder_neq_iff linorder_not_less range_eqI zero_le_dist) with a have "\(range S) = {a}" unfolding image_def by auto then show ?thesis .. @@ -2851,26 +2853,22 @@ fixes f :: "'a::metric_space \ 'b::t1_space" assumes "continuous (at x within S) f" and "f x \ a" - shows "\e>0. \y \ S. dist x y < e --> f y \ a" + shows "\\>0. \y \ S. dist x y < \ \ f y \ a" proof - obtain U where "open U" and "f x \ U" and "a \ U" using t1_space [OF \f x \ a\] by fast - have "(f \ f x) (at x within S)" - using assms(1) by (simp add: continuous_within) - then have "eventually (\y. f y \ U) (at x within S)" + have "\\<^sub>F y in at x within S. f y \ U" using \open U\ and \f x \ U\ - unfolding tendsto_def by fast - then have "eventually (\y. f y \ a) (at x within S)" - using \a \ U\ by (fast elim: eventually_mono) - then show ?thesis - using \f x \ a\ by (auto simp: dist_commute eventually_at) + using assms(1) continuous_within tendsto_def by blast + with \f x \ a\ \a \ U\ show ?thesis + by (metis (no_types, lifting) dist_commute eventually_at) qed lemma continuous_at_avoid: fixes f :: "'a::metric_space \ 'b::t1_space" assumes "continuous (at x) f" and "f x \ a" - shows "\e>0. \y. dist x y < e \ f y \ a" + shows "\\>0. \y. dist x y < \ \ f y \ a" using assms continuous_within_avoid[of x UNIV f a] by simp lemma continuous_on_avoid: @@ -2878,7 +2876,7 @@ assumes "continuous_on S f" and "x \ S" and "f x \ a" - shows "\e>0. \y \ S. dist x y < e \ f y \ a" + shows "\\>0. \y \ S. dist x y < \ \ f y \ a" using continuous_within_avoid[of x S f a] assms by (meson continuous_on_eq_continuous_within) @@ -2888,7 +2886,7 @@ and "open S" and "x \ S" and "f x \ a" - shows "\e>0. \y. dist x y < e \ f y \ a" + shows "\\>0. \y. dist x y < \ \ f y \ a" using continuous_at_avoid[of x f a] assms by (meson continuous_on_eq_continuous_at) @@ -2907,7 +2905,7 @@ lemma closed_contains_Sup: fixes S :: "real set" shows "S \ {} \ bdd_above S \ closed S \ Sup S \ S" - by (subst closure_closed[symmetric], assumption, rule closure_contains_Sup) + by (metis closure_closed closure_contains_Sup) lemma closed_subset_contains_Sup: fixes A C :: "real set" @@ -2917,8 +2915,8 @@ lemma atLeastAtMost_subset_contains_Inf: fixes A :: "real set" and a b :: real shows "A \ {} \ a \ b \ A \ {a..b} \ Inf A \ {a..b}" - by (rule closed_subset_contains_Inf) - (auto intro: closed_real_atLeastAtMost intro!: bdd_belowI[of A a]) + by (meson bdd_below_Icc bdd_below_mono closed_real_atLeastAtMost + closed_subset_contains_Inf) lemma bounded_real: "bounded (S::real set) \ (\a. \x\S. \x\ \ a)" by (simp add: bounded_iff) @@ -2966,49 +2964,49 @@ by (auto simp: bounded_imp_bdd_below inf_min cInf_insert_If) lemma open_real: - fixes s :: "real set" - shows "open s \ (\x \ s. \e>0. \x'. \x' - x\ < e --> x' \ s)" + fixes S :: "real set" + shows "open S \ (\x \ S. \\>0. \x'. \x' - x\ < \ --> x' \ S)" unfolding open_dist dist_norm by simp lemma islimpt_approachable_real: - fixes s :: "real set" - shows "x islimpt s \ (\e>0. \x'\ s. x' \ x \ \x' - x\ < e)" + fixes S :: "real set" + shows "x islimpt S \ (\\>0. \x'\ S. x' \ x \ \x' - x\ < \)" unfolding islimpt_approachable dist_norm by simp lemma closed_real: - fixes s :: "real set" - shows "closed s \ (\x. (\e>0. \x' \ s. x' \ x \ \x' - x\ < e) \ x \ s)" + fixes S :: "real set" + shows "closed S \ (\x. (\\>0. \x' \ S. x' \ x \ \x' - x\ < \) \ x \ S)" unfolding closed_limpt islimpt_approachable dist_norm by simp lemma continuous_at_real_range: fixes f :: "'a::real_normed_vector \ real" - shows "continuous (at x) f \ (\e>0. \d>0. \x'. norm(x' - x) < d --> \f x' - f x\ < e)" - by (metis (mono_tags, opaque_lifting) LIM_eq continuous_within norm_eq_zero real_norm_def right_minus_eq) + shows "continuous (at x) f \ (\\>0. \\>0. \x'. norm(x' - x) < \ \ \f x' - f x\ < \)" + by (simp add: continuous_at_eps_delta dist_norm) lemma continuous_on_real_range: fixes f :: "'a::real_normed_vector \ real" - shows "continuous_on s f \ - (\x \ s. \e>0. \d>0. (\x' \ s. norm(x' - x) < d \ \f x' - f x\ < e))" + shows "continuous_on S f \ + (\x \ S. \\>0. \\>0. (\x' \ S. norm(x' - x) < \ \ \f x' - f x\ < \))" unfolding continuous_on_iff dist_norm by simp lemma continuous_on_closed_Collect_le: fixes f g :: "'a::topological_space \ real" - assumes f: "continuous_on s f" and g: "continuous_on s g" and s: "closed s" - shows "closed {x \ s. f x \ g x}" + assumes f: "continuous_on S f" and g: "continuous_on S g" and S: "closed S" + shows "closed {x \ S. f x \ g x}" proof - - have "closed ((\x. g x - f x) -` {0..} \ s)" + have "closed ((\x. g x - f x) -` {0..} \ S)" using closed_real_atLeast continuous_on_diff [OF g f] - by (simp add: continuous_on_closed_vimage [OF s]) - also have "((\x. g x - f x) -` {0..} \ s) = {x\s. f x \ g x}" + by (simp add: continuous_on_closed_vimage [OF S]) + also have "((\x. g x - f x) -` {0..} \ S) = {x\S. f x \ g x}" by auto finally show ?thesis . qed lemma continuous_le_on_closure: fixes a::real - assumes f: "continuous_on (closure s) f" - and x: "x \ closure(s)" - and xlo: "\x. x \ s ==> f(x) \ a" + assumes f: "continuous_on (closure S) f" + and x: "x \ closure(S)" + and xlo: "\x. x \ S \ f(x) \ a" shows "f(x) \ a" using image_closure_subset [OF f, where T=" {x. x \ a}" ] assms continuous_on_closed_Collect_le[of "UNIV" "\x. x" "\x. a"] @@ -3016,9 +3014,9 @@ lemma continuous_ge_on_closure: fixes a::real - assumes f: "continuous_on (closure s) f" - and x: "x \ closure(s)" - and xlo: "\x. x \ s ==> f(x) \ a" + assumes f: "continuous_on (closure S) f" + and x: "x \ closure S" + and xlo: "\x. x \ S \ f(x) \ a" shows "f(x) \ a" using image_closure_subset [OF f, where T=" {x. a \ x}"] assms continuous_on_closed_Collect_le[of "UNIV" "\x. a" "\x. x"] @@ -3028,33 +3026,36 @@ section\The infimum of the distance between two sets\ definition\<^marker>\tag important\ setdist :: "'a::metric_space set \ 'a set \ real" where - "setdist s t \ - (if s = {} \ t = {} then 0 - else Inf {dist x y| x y. x \ s \ y \ t})" - -lemma setdist_empty1 [simp]: "setdist {} t = 0" + "setdist S T \ + (if S = {} \ T = {} then 0 + else Inf {dist x y| x y. x \ S \ y \ T})" + +lemma setdist_empty1 [simp]: "setdist {} T = 0" by (simp add: setdist_def) -lemma setdist_empty2 [simp]: "setdist t {} = 0" +lemma setdist_empty2 [simp]: "setdist T {} = 0" by (simp add: setdist_def) -lemma setdist_pos_le [simp]: "0 \ setdist s t" +lemma setdist_pos_le [simp]: "0 \ setdist S T" by (auto simp: setdist_def ex_in_conv [symmetric] intro: cInf_greatest) lemma le_setdistI: - assumes "s \ {}" "t \ {}" "\x y. \x \ s; y \ t\ \ d \ dist x y" - shows "d \ setdist s t" + assumes "S \ {}" "T \ {}" "\x y. \x \ S; y \ T\ \ \ \ dist x y" + shows "\ \ setdist S T" using assms by (auto simp: setdist_def Set.ex_in_conv [symmetric] intro: cInf_greatest) -lemma setdist_le_dist: "\x \ s; y \ t\ \ setdist s t \ dist x y" +lemma setdist_le_dist: "\x \ S; y \ T\ \ setdist S T \ dist x y" unfolding setdist_def by (auto intro!: bdd_belowI [where m=0] cInf_lower) lemma le_setdist_iff: - "d \ setdist S T \ - (\x \ S. \y \ T. d \ dist x y) \ (S = {} \ T = {} \ d \ 0)" - by (smt (verit) le_setdistI setdist_def setdist_le_dist) + "\ \ setdist S T \ (\x \ S. \y \ T. \ \ dist x y) \ (S = {} \ T = {} \ \ \ 0)" + (is "?lhs = ?rhs") +proof + show "?rhs \ ?lhs" + by (meson le_setdistI order_trans setdist_pos_le) +qed (use setdist_le_dist in fastforce) lemma setdist_ltE: assumes "setdist S T < b" "S \ {}" "T \ {}" @@ -3063,7 +3064,10 @@ by (auto simp: not_le [symmetric] le_setdist_iff) lemma setdist_refl: "setdist S S = 0" - by (metis dist_eq_0_iff ex_in_conv order_antisym setdist_def setdist_le_dist setdist_pos_le) +proof (rule antisym) + show "setdist S S \ 0" + by (metis dist_self equals0I order_refl setdist_empty1 setdist_le_dist) +qed simp lemma setdist_sym: "setdist S T = setdist T S" by (force simp: setdist_def dist_commute intro!: arg_cong [where f=Inf]) @@ -3074,8 +3078,10 @@ using setdist_pos_le by fastforce next case False - then have "\x. x \ S \ setdist S T - dist x a \ setdist {a} T" - by (smt (verit, best) dist_self dist_triangle3 empty_not_insert le_setdist_iff setdist_le_dist singleton_iff) + then have "setdist S T - dist x a \ setdist {a} T" if "x \ S" for x + unfolding le_setdist_iff + by (metis diff_le_eq dist_commute dist_triangle3 order.trans empty_not_insert + setdist_le_dist singleton_iff that) then have "setdist S T - setdist {a} T \ setdist S {a}" using False by (fastforce intro: le_setdistI) then show ?thesis @@ -3127,11 +3133,11 @@ by (metis antisym dist_self setdist_le_dist setdist_pos_le) lemma setdist_unique: - "\a \ S; b \ T; \x y. x \ S \ y \ T ==> dist a b \ dist x y\ + "\a \ S; b \ T; \x y. x \ S \ y \ T \ dist a b \ dist x y\ \ setdist S T = dist a b" by (force simp: setdist_le_dist le_setdist_iff intro: antisym) -lemma setdist_le_sing: "x \ S ==> setdist S T \ setdist {x} T" +lemma setdist_le_sing: "x \ S \ setdist S T \ setdist {x} T" using setdist_subset_left by auto lemma infdist_eq_setdist: "infdist x A = setdist {x} A" @@ -3143,12 +3149,12 @@ if "b \ B" "a \ A" for a b proof (rule order_antisym) have "Inf {dist x y |x y. x \ A \ y \ B} \ Inf (dist x ` B)" - if "b \ B" "a \ A" "x \ A" for x + if "b \ B" "a \ A" "x \ A" for x proof - have "\b'. b' \ B \ Inf {dist x y |x y. x \ A \ y \ B} \ dist x b'" - by (metis (mono_tags, lifting) ex_in_conv setdist_def setdist_le_dist that(3)) + by (metis (mono_tags, lifting) ex_in_conv setdist_def setdist_le_dist \x \ A\) then show ?thesis - by (smt (verit) cINF_greatest ex_in_conv \b \ B\) + by (metis (lifting) cINF_greatest emptyE \b \ B\) qed then show "Inf {dist x y |x y. x \ A \ y \ B} \ (INF x\A. Inf (dist x ` B))" by (metis (mono_tags, lifting) cINF_greatest emptyE that) @@ -3207,11 +3213,12 @@ lemma diameter_comp_strict_mono: fixes s :: "nat \ 'a :: metric_space" - assumes "strict_mono r" "bounded {s i |i. r n \ i}" + assumes "strict_mono r" and bnd: "bounded {s i |i. r n \ i}" shows "diameter {s (r i) | i. n \ i} \ diameter {s i | i. r n \ i}" proof (rule diameter_subset) - show "{s (r i) | i. n \ i} \ {s i | i. r n \ i}" using assms(1) monotoneD strict_mono_mono by fastforce -qed (intro assms(2)) + show "{s (r i) | i. n \ i} \ {s i | i. r n \ i}" + using \strict_mono r\ monotoneD strict_mono_mono by fastforce +qed (intro bnd) lemma diameter_bounded_bound': fixes S :: "'a :: metric_space set" @@ -3227,44 +3234,63 @@ lemma bounded_imp_dist_bounded: assumes "bounded (range s)" shows "bounded ((\(i, j). dist (s i) (s j)) ` ({n..} \ {n..}))" - using bounded_dist_comp[OF bounded_fst bounded_snd, OF bounded_Times(1,1)[OF assms(1,1)]] by (rule bounded_subset, force) - -text \A sequence is Cauchy, if and only if it is bounded and its diameter tends to zero. The diameter is well-defined only if the sequence is bounded.\ + unfolding image_iff case_prod_unfold + by (intro bounded_dist_comp; meson assms bounded_dist_comp bounded_dist_comp bounded_subset image_subset_iff rangeI) + +text \A sequence is Cauchy, if and only if it is bounded and its diameter tends to zero. + The diameter is well-defined only if the sequence is bounded.\ lemma cauchy_iff_diameter_tends_to_zero_and_bounded: fixes s :: "nat \ 'a :: metric_space" shows "Cauchy s \ ((\n. diameter {s i | i. i \ n}) \ 0 \ bounded (range s))" + (is "_ = ?rhs") proof - have "{s i |i. N \ i} \ {}" for N by blast - hence diameter_SUP: "diameter {s i |i. N \ i} = (SUP (i, j) \ {N..} \ {N..}. dist (s i) (s j))" for N unfolding diameter_def by (auto intro!: arg_cong[of _ _ Sup]) + hence diameter_SUP: "diameter {s i |i. N \ i} = (SUP (i, j) \ {N..} \ {N..}. dist (s i) (s j))" for N + unfolding diameter_def by (auto intro!: arg_cong[of _ _ Sup]) show ?thesis proof (intro iffI) - assume asm: "Cauchy s" - have "\N. \n\N. norm (diameter {s i |i. n \ i}) < e" if e_pos: "e > 0" for e + assume "Cauchy s" + have "\N. \n\N. norm (diameter {s i |i. n \ i}) < \" if e_pos: "\ > 0" for \ proof - - obtain N where dist_less: "dist (s n) (s m) < (1/2) * e" if "n \ N" "m \ N" for n m using asm e_pos by (metis Cauchy_def mult_pos_pos zero_less_divide_iff zero_less_numeral zero_less_one) - { - fix r assume "r \ N" - hence "dist (s n) (s m) < (1/2) * e" if "n \ r" "m \ r" for n m using dist_less that by simp - hence "(SUP (i, j) \ {r..} \ {r..}. dist (s i) (s j)) \ (1/2) * e" by (intro cSup_least) fastforce+ - also have "... < e" using e_pos by simp - finally have "diameter {s i |i. r \ i} < e" using diameter_SUP by presburger - } - moreover have "diameter {s i |i. r \ i} \ 0" for r unfolding diameter_SUP using bounded_imp_dist_bounded[OF cauchy_imp_bounded, THEN bounded_imp_bdd_above, OF asm] by (intro cSup_upper2, auto) - ultimately show ?thesis by auto + obtain N where dist_less: "dist (s n) (s m) < (1/2) * \" + if "n \ N" "m \ N" for n m + using \Cauchy s\ e_pos + by (meson half_gt_zero less_numeral_extra(1) metric_CauchyD mult_pos_pos) + have "diameter {s i |i. r \ i} < \" + if "r \ N" for r + proof - + have "dist (s n) (s m) < (1/2) * \" if "n \ r" "m \ r" for n m + using \r \ N\ dist_less that by simp + hence "(SUP (i, j) \ {r..} \ {r..}. dist (s i) (s j)) \ (1/2) * \" + by (intro cSup_least) fastforce+ + also have "\ < \" using e_pos by simp + finally show ?thesis + using diameter_SUP by presburger + qed + moreover have "diameter {s i |i. r \ i} \ 0" for r + unfolding diameter_SUP + using bounded_imp_dist_bounded[OF cauchy_imp_bounded, THEN bounded_imp_bdd_above] \Cauchy s\ + by (force intro: cSup_upper2) + ultimately show ?thesis + by auto qed - thus "(\n. diameter {s i |i. n \ i}) \ 0 \ bounded (range s)" using cauchy_imp_bounded[OF asm] by (simp add: LIMSEQ_iff) + thus "(\n. diameter {s i |i. n \ i}) \ 0 \ bounded (range s)" + using cauchy_imp_bounded[OF \Cauchy s\] by (simp add: LIMSEQ_iff) next - assume asm: "(\n. diameter {s i |i. n \ i}) \ 0 \ bounded (range s)" - have "\N. \n\N. \m\N. dist (s n) (s m) < e" if e_pos: "e > 0" for e + assume R: ?rhs + have "\N. \n\N. \m\N. dist (s n) (s m) < \" if e_pos: "\ > 0" for \ proof - - obtain N where diam_less: "diameter {s i |i. r \ i} < e" if "r \ N" for r using LIMSEQ_D asm(1) e_pos by fastforce - { - fix n m assume "n \ N" "m \ N" - hence "dist (s n) (s m) < e" using cSUP_lessD[OF bounded_imp_dist_bounded[THEN bounded_imp_bdd_above], OF _ diam_less[unfolded diameter_SUP]] asm by auto - } + obtain N where diam_less: "diameter {s i |i. r \ i} < \" if "r \ N" for r + using LIMSEQ_D R e_pos by fastforce + have "dist (s n) (s m) < \" + if "n \ N" "m \ N" for n m + using cSUP_lessD[OF bounded_imp_dist_bounded[THEN bounded_imp_bdd_above], + OF _ diam_less[unfolded diameter_SUP]] + using R that by auto thus ?thesis by blast qed - then show "Cauchy s" by (simp add: Cauchy_def) + then show "Cauchy s" + by (simp add: Cauchy_def) qed qed diff -r 3dfd62b4e2c8 -r ad31be996dcb src/HOL/Analysis/Homotopy.thy --- a/src/HOL/Analysis/Homotopy.thy Tue Apr 22 19:02:33 2025 +0200 +++ b/src/HOL/Analysis/Homotopy.thy Tue Apr 22 22:06:52 2025 +0100 @@ -5222,13 +5222,12 @@ next case False show ?thesis - proof (rule continuous_transform_within [where f=g and d = "norm(x-a)"]) - have "\d>0. \x'\cball a r. - dist x' x < d \ dist (g x') (g x) < e" if "e>0" for e + proof (rule continuous_transform_within [where f=g and \ = "norm(x-a)"]) + have "\d>0. \x'\cball a r. dist x' x < d \ dist (g x') (g x) < e" + if "e>0" for e proof - obtain d where "d > 0" - and d: "\x'. \dist x' a \ r; x' \ a; dist x' x < d\ \ - dist (g x') (g x) < e" + and d: "\y. \dist y a \ r; y \ a; dist y x < d\ \ dist (g y) (g x) < e" using contg False x \e>0\ unfolding continuous_on_iff by (fastforce simp: dist_commute intro: that) show ?thesis diff -r 3dfd62b4e2c8 -r ad31be996dcb src/HOL/Analysis/Measurable.thy --- a/src/HOL/Analysis/Measurable.thy Tue Apr 22 19:02:33 2025 +0200 +++ b/src/HOL/Analysis/Measurable.thy Tue Apr 22 22:06:52 2025 +0100 @@ -290,7 +290,7 @@ {x\space M. if (\i. \n\i. P n x) then the None = n else if (\i. P i x) then P n x \ (\i>n. \ P i x) else Max {} = n}" - by (intro arg_cong[where f=Collect] ext conj_cong) + by (intro arg_cong[where f=Collect] ext) (auto simp add: 1 2 3 not_le[symmetric] intro!: Max_eqI) also have "\ \ sets M" by measurable @@ -317,7 +317,7 @@ {x\space M. if (\i. \n\i. P n x) then the None = n else if (\i. P i x) then P n x \ (\i P i x) else Min {} = n}" - by (intro arg_cong[where f=Collect] ext conj_cong) + by (intro arg_cong[where f=Collect] ext) (auto simp add: 1 2 3 not_le[symmetric] intro!: Min_eqI) also have "\ \ sets M" by measurable @@ -378,7 +378,7 @@ assumes [measurable]: "\i. i \ I \ F i \ measurable M (count_space UNIV)" shows "(\x. SUP i\I. F i x) \ measurable M (count_space UNIV)" unfolding measurable_count_space_eq2_countable -proof (safe intro!: UNIV_I) +proof (intro conjI strip) fix a have "(\x. SUP i\I. F i x) -` {a} \ space M = {x\space M. (\i\I. F i x \ a) \ (\b. (\i\I. F i x \ b) \ a \ b)}" @@ -386,7 +386,7 @@ also have "\ \ sets M" by measurable finally show "(\x. SUP i\I. F i x) -` {a} \ space M \ sets M" . -qed +qed auto lemma measurable_INF[measurable]: fixes F :: "'i \ 'a \ 'b::{complete_lattice, countable}" @@ -394,7 +394,7 @@ assumes [measurable]: "\i. i \ I \ F i \ measurable M (count_space UNIV)" shows "(\x. INF i\I. F i x) \ measurable M (count_space UNIV)" unfolding measurable_count_space_eq2_countable -proof (safe intro!: UNIV_I) +proof (intro conjI strip) fix a have "(\x. INF i\I. F i x) -` {a} \ space M = {x\space M. (\i\I. a \ F i x) \ (\b. (\i\I. b \ F i x) \ b \ a)}" @@ -402,7 +402,7 @@ also have "\ \ sets M" by measurable finally show "(\x. INF i\I. F i x) -` {a} \ space M \ sets M" . -qed +qed auto lemma measurable_lfp_coinduct[consumes 1, case_names continuity step]: fixes F :: "('a \ 'b) \ ('a \ 'b::{complete_lattice, countable})" @@ -628,10 +628,10 @@ lemma measurable_case_enat[measurable (raw)]: assumes f: "f \ M \\<^sub>M count_space UNIV" and g: "\i. g i \ M \\<^sub>M N" and h: "h \ M \\<^sub>M N" shows "(\x. case f x of enat i \ g i x | \ \ h x) \ M \\<^sub>M N" - apply (rule measurable_compose_countable[OF _ f]) - subgoal for i +proof (rule measurable_compose_countable[OF _ f]) + show "(\x. case i of enat i \ g i x | \ \ h x) \ M \\<^sub>M N" for i by (cases i) (auto intro: g h) - done +qed hide_const (open) pred diff -r 3dfd62b4e2c8 -r ad31be996dcb src/HOL/Analysis/Measure_Space.thy --- a/src/HOL/Analysis/Measure_Space.thy Tue Apr 22 19:02:33 2025 +0200 +++ b/src/HOL/Analysis/Measure_Space.thy Tue Apr 22 22:06:52 2025 +0100 @@ -68,13 +68,10 @@ proof fix n show "(\i < Suc (Suc n). f (binaryset A B i)) = f A + f B" - by (induct n) (auto simp add: binaryset_def f) + by (induct n) (auto simp: binaryset_def f) qed - moreover - have "\ \ f A + f B" by (rule tendsto_const) - ultimately have "(\n. \i< n+2. f (binaryset A B i)) \ f A + f B" - by simp - thus ?thesis by (rule LIMSEQ_offset [where k=2]) + thus ?thesis + by (simp add: LIMSEQ_imp_Suc) qed lemma binaryset_sums: @@ -98,7 +95,7 @@ "subadditive M f \ (\x\M. \y\M. x \ y = {} \ f (x \ y) \ f x + f y)" lemma subadditiveD: "subadditive M f \ x \ y = {} \ x \ M \ y \ M \ f (x \ y) \ f x + f y" - by (auto simp add: subadditive_def) + by (auto simp: subadditive_def) definition countably_subadditive where "countably_subadditive M f \ @@ -108,20 +105,20 @@ fixes f :: "'a set \ ennreal" assumes f: "positive M f" and cs: "countably_subadditive M f" shows "subadditive M f" -proof (auto simp add: subadditive_def) +proof (auto simp: subadditive_def) fix x y assume x: "x \ M" and y: "y \ M" and "x \ y = {}" hence "disjoint_family (binaryset x y)" - by (auto simp add: disjoint_family_on_def binaryset_def) + by (auto simp: disjoint_family_on_def binaryset_def) hence "range (binaryset x y) \ M \ (\i. binaryset x y i) \ M \ f (\i. binaryset x y i) \ (\ n. f (binaryset x y n))" - using cs by (auto simp add: countably_subadditive_def) + using cs by (auto simp: countably_subadditive_def) hence "{x,y,{}} \ M \ x \ y \ M \ f (x \ y) \ (\ n. f (binaryset x y n))" by (simp add: range_binaryset_eq UN_binaryset_eq) thus "f (x \ y) \ f x + f y" using f x y - by (auto simp add: Un o_def suminf_binaryset_eq positive_def) + by (auto simp: Un o_def suminf_binaryset_eq positive_def) qed definition additive where @@ -134,15 +131,15 @@ lemma positiveD_empty: "positive M f \ f {} = 0" - by (auto simp add: positive_def) + by (auto simp: positive_def) lemma additiveD: "additive M f \ x \ y = {} \ x \ M \ y \ M \ f (x \ y) = f x + f y" - by (auto simp add: additive_def) + by (auto simp: additive_def) lemma increasingD: "increasing M f \ x \ y \ x\M \ y\M \ f x \ f y" - by (auto simp add: increasing_def) + by (auto simp: increasing_def) lemma countably_additiveI[case_names countably]: "(\A. \range A \ M; disjoint_family A; (\i. A i) \ M\ \ (\i. f(A i)) = f(\i. A i)) @@ -175,22 +172,22 @@ next case (insert s S) then have "A s \ (\i\S. A i) = {}" - by (auto simp add: disjoint_family_on_def neq_iff) + by (auto simp: disjoint_family_on_def neq_iff) moreover have "A s \ M" using insert by blast moreover have "(\i\S. A i) \ M" using insert \finite S\ by auto ultimately have "f (A s \ (\i\S. A i)) = f (A s) + f(\i\S. A i)" - using ad UNION_in_sets A by (auto simp add: additive_def) + using ad UNION_in_sets A by (auto simp: additive_def) with insert show ?case using ad disjoint_family_on_mono[of S "insert s S" A] - by (auto simp add: additive_def subset_insertI) + by (auto simp: additive_def subset_insertI) qed lemma (in ring_of_sets) additive_increasing: fixes f :: "'a set \ ennreal" assumes posf: "positive M f" and addf: "additive M f" shows "increasing M f" -proof (auto simp add: increasing_def) +proof (auto simp: increasing_def) fix x y assume xy: "x \ M" "y \ M" "x \ y" then have "y - x \ M" by auto @@ -231,11 +228,11 @@ fixes f :: "'a set \ ennreal" assumes posf: "positive M f" and ca: "countably_additive M f" shows "additive M f" -proof (auto simp add: additive_def) +proof (auto simp: additive_def) fix x y assume x: "x \ M" and y: "y \ M" and "x \ y = {}" hence "disjoint_family (binaryset x y)" - by (auto simp add: disjoint_family_on_def binaryset_def) + by (auto simp: disjoint_family_on_def binaryset_def) hence "range (binaryset x y) \ M \ (\i. binaryset x y i) \ M \ f (\i. binaryset x y i) = (\ n. f (binaryset x y n))" @@ -243,7 +240,7 @@ hence "{x,y,{}} \ M \ x \ y \ M \ f (x \ y) = (\n. f (binaryset x y n))" by (simp add: range_binaryset_eq UN_binaryset_eq) thus "f (x \ y) = f x + f y" using posf x y - by (auto simp add: Un suminf_binaryset_eq positive_def) + by (auto simp: Un suminf_binaryset_eq positive_def) qed lemma (in algebra) increasing_additive_bound: @@ -261,7 +258,7 @@ also have "\ \ f \" using space_closed A by (intro increasingD[OF inc] finite_UN) auto finally show "(\i f \" by simp -qed (insert f A, auto simp: positive_def) +qed (use f A in \auto simp: positive_def\) lemma (in ring_of_sets) countably_additiveI_finite: fixes \ :: "'a set \ ennreal" @@ -388,7 +385,8 @@ moreover { fix n have "f (A n - (\i. A i)) + f (\i. A i) = f ((A n - (\i. A i)) \ (\i. A i))" - using A by (subst f(2)[THEN additiveD]) auto + using A f(2) + by (metis (no_types) Diff Diff_disjoint add.commute additiveD range_subsetD sup_commute) also have "(A n - (\i. A i)) \ (\i. A i) = A n" by auto finally have "f (A n - (\i. A i)) + f (\i. A i) = f (A n)" . } @@ -493,21 +491,27 @@ by (metis emeasure_mono emeasure_notin_sets sets.sets_into_space sets.top zero_le) lemma emeasure_Diff: - assumes "emeasure M B \ \" + assumes \: "emeasure M B \ \" and "A \ sets M" "B \ sets M" and "B \ A" - shows "emeasure M (A - B) = emeasure M A - emeasure M B" - by (smt (verit, best) add_diff_self_ennreal assms emeasure_Un emeasure_mono - ennreal_add_left_cancel le_iff_sup) +shows "emeasure M (A - B) = emeasure M A - emeasure M B" +proof - + have "emeasure M B + emeasure M (A - B) = emeasure M (B \ (A-B))" + by (simp add: assms emeasure_Un) + also have "... = emeasure M A" + using Diff_partition \B \ A\ by fastforce + finally show ?thesis + by (metis \ ennreal_add_diff_cancel_left infinity_ennreal_def) +qed lemma emeasure_compl: "s \ sets M \ emeasure M s \ \ \ emeasure M (space M - s) = emeasure M (space M) - emeasure M s" - by (rule emeasure_Diff) (auto dest: sets.sets_into_space) + by (simp add: emeasure_Diff sets.sets_into_space) lemma Lim_emeasure_incseq: "range A \ sets M \ incseq A \ (\i. (emeasure M (A i))) \ emeasure M (\i. A i)" using emeasure_countably_additive - by (auto simp add: sets.countably_additive_iff_continuous_from_below emeasure_positive - emeasure_additive) + by (metis emeasure_additive emeasure_positive sets.countable_UN + sets.countably_additive_iff_continuous_from_below) lemma incseq_emeasure: assumes "range B \ sets M" "incseq B" @@ -543,12 +547,15 @@ show "range (\n. A 0 - A n) \ sets M" using A by auto show "incseq (\n. A 0 - A n)" - using \decseq A\ by (auto simp add: incseq_def decseq_def) + using \decseq A\ by (auto simp: incseq_def decseq_def) qed also have "\ = emeasure M (A 0) - emeasure M (\i. A i)" using A finite * by (simp, subst emeasure_Diff) auto - finally show ?thesis - by (smt (verit, best) Inf_lower diff_diff_ennreal le_MI finite range_eqI) + finally have "emeasure M (A 0) - (INF n. emeasure M (A n)) = + emeasure M (A 0) - emeasure M (\ (range A))" . + then show ?thesis + by (metis Inf_lower ennreal_minus_cancel infinity_ennreal_def le_MI local.finite + range_eqI) qed lemma INF_emeasure_decseq': @@ -606,17 +613,17 @@ proof (intro INF_emeasure_decseq[symmetric]) show "decseq (\i. F (L i))" using L by (intro antimonoI F L_mono) auto - qed (insert L fin, auto) + qed (use L fin in auto) also have "\ = (INF i\I. emeasure M (F i))" proof (intro antisym INF_greatest) show "i \ I \ (INF i. emeasure M (F (L i))) \ emeasure M (F i)" for i by (intro INF_lower2[of i]) auto - qed (insert L, auto intro: INF_lower) + qed (use L in \auto intro: INF_lower\) also have "(\i. F (L i)) = (\i\I. F i)" proof (intro antisym INF_greatest) show "i \ I \ (\i. F (L i)) \ F i" for i - by (intro INF_lower2[of i]) auto - qed (insert L, auto) + by (metis Inf_lower L_eq rangeI) + qed (use L in auto) finally show ?thesis . qed @@ -633,9 +640,9 @@ shows "emeasure M {x\space M. lfp F x} = (SUP i. emeasure M {x\space M. (F ^^ i) (\x. False) x})" proof - have "emeasure M {x\space M. lfp F x} = emeasure M (\i. {x\space M. (F ^^ i) (\x. False) x})" - using sup_continuous_lfp[OF cont] by (auto simp add: bot_fun_def intro!: arg_cong2[where f=emeasure]) + using sup_continuous_lfp[OF cont] by (auto simp: bot_fun_def intro!: arg_cong2[where f=emeasure]) moreover { fix i from \P M\ have "{x\space M. (F ^^ i) (\x. False) x} \ sets M" - by (induct i arbitrary: M) (auto simp add: pred_def[symmetric] intro: *) } + by (induct i arbitrary: M) (auto simp: pred_def[symmetric] intro: *) } moreover have "incseq (\i. {x\space M. (F ^^ i) (\x. False) x})" proof (rule incseq_SucI) fix i @@ -663,7 +670,7 @@ then show "(\s. emeasure (M s) {x \ space N. (SUP i. C i) x}) = (SUP i. (\s. emeasure (M s) {x \ space N. C i x}))" unfolding SUP_apply by (subst SUP_emeasure_incseq) (auto simp: mono_def fun_eq_iff intro!: arg_cong2[where f=emeasure]) -qed (auto simp add: iter le_fun_def SUP_apply intro!: meas cont) +qed (auto simp: iter le_fun_def SUP_apply intro!: meas cont) lemma emeasure_subadditive_finite: "finite I \ A ` I \ sets M \ emeasure M (\i\I. A i) \ (\i\I. emeasure M (A i))" @@ -717,7 +724,7 @@ show "disjoint_family_on (\i. A \ B i) S" using \disjoint_family_on B S\ unfolding disjoint_family_on_def by auto - qed (insert assms, auto) + qed (use assms in auto) also have "(\i\S. A \ (B i)) = A" using A by auto finally show ?thesis by simp @@ -768,11 +775,13 @@ using sets.top[of M] sets.space_closed[of M] S.top S.space_closed \sets M = sigma_sets \ E\ by blast - { fix F D assume "F \ E" and "?\ F \ \" - then have [intro]: "F \ sigma_sets \ E" by auto + have *: "emeasure M (F \ D) = emeasure N (F \ D)" + if "F \ E" and "?\ F \ \" and D: "D \ sets M" for F D + proof - + have [intro]: "F \ sigma_sets \ E" + using that by auto have "?\ F \ \" using \?\ F \ \\ \F \ E\ eq by simp - assume "D \ sets M" - with \Int_stable E\ \E \ Pow \\ have "emeasure M (F \ D) = emeasure N (F \ D)" + from \Int_stable E\ \E \ Pow \\ D show ?thesis unfolding M proof (induct rule: sigma_sets_induct_disjoint) case (basic A) @@ -803,8 +812,8 @@ by (subst (1 2) suminf_emeasure[symmetric]) (auto simp: disjoint_family_on_def subset_eq M N) with A show ?case by auto - qed } - note * = this + qed + qed show "M = N" proof (rule measure_eqI) show "sets M = sets N" @@ -815,7 +824,7 @@ let ?D = "disjointed (\i. F \ A i)" from \space M = \\ have F_eq: "F = (\i. ?D i)" using \F \ sets M\[THEN sets.sets_into_space] A(2)[symmetric] by (auto simp: UN_disjointed_eq) - have [simp, intro]: "\i. ?D i \ sets M" + have DinM[simp]: "\i. ?D i \ sets M" using sets.range_disjointed_sets[of "\i. F \ A i" M] \F \ sets M\ by (auto simp: subset_eq) have "disjoint_family ?D" @@ -826,11 +835,11 @@ fix i have "A i \ ?D i = ?D i" by (auto simp: disjointed_def) - then show "emeasure M (?D i) = emeasure N (?D i)" - using *[of "A i" "?D i", OF _ A(3)] A(1) by auto + with A show "emeasure M (?D i) = emeasure N (?D i)" + by (metis "*" DinM range_subsetD) qed ultimately show "emeasure M F = emeasure N F" - by (simp add: image_subset_iff \sets M = sets N\[symmetric] F_eq[symmetric] suminf_emeasure) + by (metis DinM F_eq \sets M = sets N\ image_subset_iff suminf_emeasure) qed qed @@ -847,8 +856,8 @@ assume "\ = {}" have *: "sigma_sets \ E = sets (sigma \ E)" using E(2) by simp - have "space M = \" "space N = \" - using sets E(2) unfolding * by (auto dest: sets_eq_imp_space_eq simp del: sets_measure_of) + obtain "space M = \" "space N = \" + by (simp add: "*" sets sets_eq_imp_space_eq space_measure_of_conv) then show "M = N" unfolding \\ = {}\ by (auto dest: space_empty) next @@ -910,13 +919,7 @@ lemma UN_from_nat_into: assumes I: "countable I" "I \ {}" shows "(\i\I. N i) = (\i. N (from_nat_into I i))" -proof - - have "(\i\I. N i) = \(N ` range (from_nat_into I))" - using I by simp - also have "\ = (\i. (N \ from_nat_into I) i)" - by simp - finally show ?thesis by simp -qed + using assms by (simp add: UN_extend_simps) lemma null_sets_UN': assumes "countable I" @@ -949,7 +952,7 @@ proof (intro CollectI conjI null_setsI) show "emeasure M (A \ B) = 0" using assms by (intro emeasure_eq_0[of B _ "A \ B"]) auto -qed (insert assms, auto) +qed (use assms in auto) lemma null_set_Int2: assumes "B \ null_sets M" "A \ sets M" shows "B \ A \ null_sets M" @@ -969,15 +972,17 @@ lemma null_set_Diff: assumes "B \ null_sets M" "A \ sets M" shows "B - A \ null_sets M" proof (intro CollectI conjI null_setsI) - show "emeasure M (B - A) = 0" using assms by (intro emeasure_eq_0[of B _ "B - A"]) auto -qed (insert assms, auto) + show "emeasure M (B - A) = 0" + using assms by (intro emeasure_eq_0[of B _ "B - A"]) auto +qed (use assms in auto) lemma emeasure_Un_null_set: assumes "A \ sets M" "B \ null_sets M" shows "emeasure M (A \ B) = emeasure M A" proof - have *: "A \ B = A \ (B - A)" by auto - have "B - A \ null_sets M" using assms(2,1) by (rule null_set_Diff) + have "B - A \ null_sets M" using assms + using null_set_Diff by blast then show ?thesis unfolding * using assms by (subst plus_emeasure[symmetric]) auto @@ -1035,8 +1040,8 @@ proof assume "AE x in M. P x" then obtain N where N: "N \ sets M" "?P \ N" "emeasure M N = 0" unfolding eventually_ae_filter by auto - have "emeasure M ?P \ emeasure M N" - using assms N(1,2) by (auto intro: emeasure_mono) + then have "emeasure M ?P \ emeasure M N" + using emeasure_mono by blast then have "emeasure M ?P = 0" unfolding \emeasure M N = 0\ by auto then show "?P \ null_sets M" using assms by auto @@ -1132,7 +1137,7 @@ qed lemma AE_space: "AE x in M. x \ space M" - by (rule AE_I[where N="{}"]) auto + by (auto intro: AE_I[where N="{}"]) lemma AE_I2[simp, intro]: "(\x. x \ space M \ P x) \ AE x in M. P x" @@ -1153,8 +1158,8 @@ "(AE x in M. \i. P i x) \ (\i::'i::countable. AE x in M. P i x)" proof assume "\i. AE x in M. P i x" - from this[unfolded eventually_ae_filter Bex_def, THEN choice] - obtain N where N: "\i. N i \ null_sets M" "\i. {x\space M. \ P i x} \ N i" by auto + then obtain N where N: "\i. N i \ null_sets M" "\i. {x\space M. \ P i x} \ N i" + unfolding eventually_ae_filter by metis have "{x\space M. \ (\i. P i x)} \ (\i. {x\space M. \ P i x})" by auto also have "\ \ (\i. N i)" using N by auto finally have "{x\space M. \ (\i. P i x)} \ (\i. N i)" . @@ -1169,9 +1174,8 @@ shows "(AE x in M. \y\X. P x y) \ (\y\X. AE x in M. P x y)" proof assume "\y\X. AE x in M. P x y" - from this[unfolded eventually_ae_filter Bex_def, THEN bchoice] - obtain N where N: "\y. y \ X \ N y \ null_sets M" "\y. y \ X \ {x\space M. \ P x y} \ N y" - by auto + then obtain N where N: "\y. y \ X \ N y \ null_sets M" "\y. y \ X \ {x\space M. \ P x y} \ N y" + unfolding eventually_ae_filter by metis have "{x\space M. \ (\y\X. P x y)} \ (\y\X. {x\space M. \ P x y})" by auto also have "\ \ (\y\X. N y)" @@ -1202,14 +1206,12 @@ by auto qed -lemma AE_finite_all: - assumes f: "finite S" shows "(AE x in M. \i\S. P i x) \ (\i\S. AE x in M. P i x)" - using f by induct auto +lemmas AE_finite_all = eventually_ball_finite_distrib lemma AE_finite_allI: assumes "finite S" shows "(\s. s \ S \ AE x in M. Q s x) \ AE x in M. \s\S. Q s x" - using AE_finite_all[OF \finite S\] by auto + by (simp add: AE_ball_countable' assms countable_finite) lemma emeasure_mono_AE: assumes imp: "AE x in M. x \ A \ x \ B" @@ -1229,10 +1231,9 @@ qed (simp add: emeasure_notin_sets) lemma emeasure_eq_AE: - assumes iff: "AE x in M. x \ A \ x \ B" - assumes A: "A \ sets M" and B: "B \ sets M" + assumes "AE x in M. x \ A \ x \ B" "A \ sets M" "B \ sets M" shows "emeasure M A = emeasure M B" - using assms by (safe intro!: antisym emeasure_mono_AE) auto + using assms by (force intro!: antisym emeasure_mono_AE) lemma emeasure_Collect_eq_AE: "AE x in M. P x \ Q x \ Measurable.pred M Q \ Measurable.pred M P \ @@ -1255,11 +1256,11 @@ shows "emeasure M C = emeasure M A + emeasure M B" proof - have "emeasure M C = emeasure M (A \ B)" - by (rule emeasure_eq_AE) (insert 1, auto) + by (rule emeasure_eq_AE) (use 1 in auto) also have "\ = emeasure M A + emeasure M (B - A)" by (subst plus_emeasure) auto also have "emeasure M (B - A) = emeasure M B" - by (rule emeasure_eq_AE) (insert 2, auto) + by (rule emeasure_eq_AE) (use 2 in auto) finally show ?thesis . qed @@ -1309,16 +1310,12 @@ proof (rule that[of "disjointed A"]) show "range (disjointed A) \ sets M" by (rule sets.range_disjointed_sets[OF range]) - show "(\i. disjointed A i) = space M" - and "disjoint_family (disjointed A)" + show "(\i. disjointed A i) = space M" and "disjoint_family (disjointed A)" using disjoint_family_disjointed UN_disjointed_eq[of A] space range by auto show "emeasure M (disjointed A i) \ \" for i - proof - - have "emeasure M (disjointed A i) \ emeasure M (A i)" - using range disjointed_subset[of A i] by (auto intro!: emeasure_mono) - then show ?thesis using measure[of i] by (auto simp: top_unique) - qed + using range disjointed_subset[of A i] measure[of i] + by (simp add: emeasure_mono neq_top_trans) qed qed @@ -1334,10 +1331,7 @@ show "range (\n. \i\n. F i) \ sets M" using F by (force simp: incseq_def) show "(\n. \i\n. F i) = space M" - proof - - from F have "\x. x \ space M \ \i. x \ F i" by auto - with F show ?thesis by fastforce - qed + using F(2) by fastforce show "emeasure M (\i\n. F i) \ \" for n proof - have "emeasure M (\i\n. F i) \ (\i\n. emeasure M (F i))" @@ -1361,16 +1355,19 @@ where A: "range A \ sets M" "(\i. A i) = space M" "\i. emeasure M (A i) \ \" "incseq A" using sigma_finite_incseq by blast define B where "B = (\i. W \ A i)" - have B_meas: "\i. B i \ sets M" using W_meas \range A \ sets M\ B_def by blast - have b: "\i. B i \ W" using B_def by blast - - { fix i + have B_meas: "\i. B i \ sets M" + using W_meas \range A \ sets M\ B_def by blast + have BsubW: "\i. B i \ W" + using B_def by blast + + have Bfinite: "emeasure M (B i) < \" for i + proof - have "emeasure M (B i) \ emeasure M (A i)" using A by (intro emeasure_mono) (auto simp: B_def) also have "emeasure M (A i) < \" using \\i. emeasure M (A i) \ \\ by (simp add: less_top) - finally have "emeasure M (B i) < \" . } - note c = this + finally show ?thesis . + qed have "W = (\i. B i)" using B_def \(\i. A i) = space M\ W_meas by auto moreover have "incseq B" using B_def \incseq A\ by (simp add: incseq_def subset_eq) @@ -1378,10 +1375,10 @@ by (simp add: B_meas Lim_emeasure_incseq image_subset_iff) then have "(\i. emeasure M (B i)) \ \" using W_inf by simp from order_tendstoD(1)[OF this, of C] - obtain i where d: "emeasure M (B i) > C" + obtain i where "emeasure M (B i) > C" by (auto simp: eventually_sequentially) - have "B i \ sets M" "B i \ W" "emeasure M (B i) < \" "emeasure M (B i) > C" - using B_meas b c d by auto + then have "B i \ sets M" "B i \ W" "emeasure M (B i) < \" "emeasure M (B i) > C" + using B_meas BsubW Bfinite by auto then show ?thesis using that by blast qed @@ -1446,8 +1443,8 @@ proof (subst (1 2) emeasure_Collect_distr[symmetric, where X=f]) show "f \ measurable M' M" "f \ measurable M' M" using f[OF \P M\] by auto - { fix i show "Measurable.pred M ((F ^^ i) (\x. False))" - using \P M\ by (induction i arbitrary: M) (auto intro!: *) } + show "Measurable.pred M ((F ^^ i) (\x. False))" for i + using \P M\ by (induction i arbitrary: M) (auto intro!: *) show "Measurable.pred M (lfp F)" using \P M\ cont * by (rule measurable_lfp_coinduct[of P]) @@ -1484,8 +1481,8 @@ proof (rule measure_eqI) fix A assume "A \ sets (distr M N f)" with assms show "emeasure (distr M N f) A = emeasure (distr K L g) A" - by (auto simp add: emeasure_distr intro!: emeasure_eq_AE measurable_sets) -qed (insert 1, simp) + by (auto simp: emeasure_distr intro!: emeasure_eq_AE measurable_sets) +qed (use 1 in simp) lemma AE_distrD: assumes f: "f \ measurable M M'" @@ -1509,31 +1506,34 @@ have "f -` {x\space N. \ P x} \ space M = {x \ space M. \ P (f x)}" using f[THEN measurable_space] by auto then show "(emeasure (distr M N f) {x \ space (distr M N f). \ P x} = 0) = - (emeasure M {x \ space M. \ P (f x)} = 0)" + (emeasure M {x \ space M. \ P (f x)} = 0)" by (simp add: emeasure_distr) qed auto lemma null_sets_distr_iff: "f \ measurable M N \ A \ null_sets (distr M N f) \ f -` A \ space M \ null_sets M \ A \ sets N" - by (auto simp add: null_sets_def emeasure_distr) + by (auto simp: null_sets_def emeasure_distr) proposition distr_distr: "g \ measurable N L \ f \ measurable M N \ distr (distr M N f) L g = distr M L (g \ f)" - by (auto simp add: emeasure_distr measurable_space + by (auto simp: emeasure_distr measurable_space intro!: arg_cong[where f="emeasure M"] measure_eqI) subsection\<^marker>\tag unimportant\ \Real measure values\ lemma ring_of_finite_sets: "ring_of_sets (space M) {A\sets M. emeasure M A \ top}" -proof (rule ring_of_setsI) - show "a \ {A \ sets M. emeasure M A \ top} \ b \ {A \ sets M. emeasure M A \ top} \ - a \ b \ {A \ sets M. emeasure M A \ top}" for a b - using emeasure_subadditive[of a M b] by (auto simp: top_unique) - - show "a \ {A \ sets M. emeasure M A \ top} \ b \ {A \ sets M. emeasure M A \ top} \ - a - b \ {A \ sets M. emeasure M A \ top}" for a b - using emeasure_mono[of "a - b" a M] by (auto simp: top_unique) -qed (auto dest: sets.sets_into_space) +proof - + have False + if "a \ sets M" and "emeasure M a \ top" + and "b \ sets M" and "emeasure M b \ top" + and "emeasure M (a - b) = top" + for a b + using that + by (metis emeasure_Un emeasure_Un_Int ennreal_add_eq_top) + then show ?thesis + using emeasure_Un_Int + by (fastforce intro!: sets.sets_into_space ring_of_setsI) +qed lemma measure_nonneg[simp]: "0 \ measure M A" unfolding measure_def by auto @@ -1542,7 +1542,7 @@ using measure_nonneg not_le by blast lemma zero_less_measure_iff: "0 < measure M A \ measure M A \ 0" - using measure_nonneg[of M A] by (auto simp add: le_less) + using measure_nonneg[of M A] by (auto simp: le_less) lemma measure_le_0_iff: "measure M X \ 0 \ measure M X = 0" using measure_nonneg[of M X] by linarith @@ -1602,16 +1602,12 @@ assumes finite: "emeasure M (\i. A i) \ \" shows "(\i. measure M (A i)) sums (measure M (\i. A i))" proof - - have "(\i. emeasure M (A i)) sums (emeasure M (\i. A i))" + have \
: "(\i. emeasure M (A i)) sums (emeasure M (\i. A i))" unfolding suminf_emeasure[OF measurable, symmetric] by (simp add: summable_sums) - moreover - { fix i - have "emeasure M (A i) \ emeasure M (\i. A i)" - using measurable by (auto intro!: emeasure_mono) - then have "emeasure M (A i) = ennreal ((measure M (A i)))" - using finite by (intro emeasure_eq_ennreal_measure) (auto simp: top_unique) } - ultimately show ?thesis using finite - by (subst (asm) (2) emeasure_eq_ennreal_measure) simp_all + then have "emeasure M (A i) = ennreal ((measure M (A i)))" for i + by (metis assms(3) emeasure_eq_ennreal_measure ennreal_suminf_lessD + infinity_ennreal_def less_top sums_unique) + with \
show ?thesis using finite emeasure_eq_ennreal_measure by fastforce qed lemma measure_subadditive: @@ -1623,7 +1619,7 @@ using emeasure_subadditive[OF measurable] fin by (auto simp: top_unique) then show "(measure M (A \ B)) \ (measure M A) + (measure M B)" unfolding measure_def - by (metis emeasure_subadditive[OF measurable] fin enn2real_mono enn2real_plus + by (metis emeasure_subadditive[OF measurable] fin enn2real_mono enn2real_plus ennreal_add_less_top infinity_ennreal_def less_top) qed @@ -1631,12 +1627,9 @@ assumes A: "finite I" "A`I \ sets M" and fin: "\i. i \ I \ emeasure M (A i) \ \" shows "measure M (\i\I. A i) \ (\i\I. measure M (A i))" proof - - { have "emeasure M (\i\I. A i) \ (\i\I. emeasure M (A i))" - using emeasure_subadditive_finite[OF A] . - also have "\ < \" - using fin by (simp add: less_top A) - finally have "emeasure M (\i\I. A i) \ top" by simp } - note * = this + have *: "emeasure M (\i\I. A i) \ top" + using emeasure_subadditive_finite[OF A] fin + by (metis \finite I\ ennreal_sum_eq_top infinity_ennreal_def neq_top_trans) show ?thesis using emeasure_subadditive_finite[OF A] fin unfolding emeasure_eq_ennreal_measure[OF *] @@ -1660,7 +1653,7 @@ using emeasure_subadditive_countably[OF A] . also have "\ = ennreal (\i. measure M (A i))" using fin unfolding emeasure_eq_ennreal_measure[OF **] - by (subst suminf_ennreal) (auto simp: **) + by (metis infinity_ennreal_def measure_nonneg suminf_ennreal) finally show ?thesis using ge0 ennreal_le_iff by blast qed @@ -1781,7 +1774,7 @@ lemma measurable_Un_null_set: assumes "B \ null_sets M" shows "(A \ B \ fmeasurable M \ A \ sets M) \ A \ fmeasurable M" - using assms by (fastforce simp add: fmeasurable.Un fmeasurableI_null_sets intro: fmeasurableI2) + using assms by (fastforce simp: fmeasurable.Un fmeasurableI_null_sets intro: fmeasurableI2) lemma measurable_Diff_null_set: assumes "B \ null_sets M" @@ -1800,7 +1793,7 @@ qed lemma measure_Un2: - "A \ fmeasurable M \ B \ fmeasurable M \ measure M (A \ B) = measure M A + measure M (B - A)" + "\A \ fmeasurable M; B \ fmeasurable M\ \ measure M (A\B) = measure M A + measure M (B - A)" using measure_Union[of M A "B - A"] by (auto simp: fmeasurableD2 fmeasurable.Diff) lemma measure_Un3: @@ -1991,7 +1984,7 @@ fixes f :: "nat \ 'a::real_normed_vector" assumes "summable f" shows "(\n. (\k. f(k+n))) \ 0" -by (subst lim_sequentially, auto simp add: dist_norm suminf_exist_split[OF _ assms]) +by (subst lim_sequentially, auto simp: dist_norm suminf_exist_split[OF _ assms]) lemma emeasure_union_summable: assumes [measurable]: "\n. A n \ sets M" @@ -2000,17 +1993,18 @@ proof - define B where "B = (\N. (\n\{.. sets M" for N unfolding B_def by auto - have "(\N. emeasure M (B N)) \ emeasure M (\N. B N)" - apply (rule Lim_emeasure_incseq) unfolding B_def by (auto simp add: SUP_subset_mono incseq_def) + have "incseq B" + by (auto simp: SUP_subset_mono B_def incseq_def) + then have "(\N. emeasure M (B N)) \ emeasure M (\N. B N)" + by (simp add: Lim_emeasure_incseq image_subset_iff) moreover have "emeasure M (B N) \ ennreal (\n. measure M (A n))" for N proof - have *: "(\n (\n. measure M (A n))" - using assms(3) measure_nonneg sum_le_suminf by blast - + using \summable _\ measure_nonneg sum_le_suminf by blast have "emeasure M (B N) \ (\n = (\n = ennreal (\n \ ennreal (\n. measure M (A n))" @@ -2027,24 +2021,24 @@ lemma borel_cantelli_limsup1: assumes [measurable]: "\n. A n \ sets M" - and "\n. emeasure M (A n) < \" "summable (\n. measure M (A n))" + and "\n. emeasure M (A n) < \" and sum: "summable (\n. measure M (A n))" shows "limsup A \ null_sets M" proof - have "emeasure M (limsup A) \ 0" proof (rule LIMSEQ_le_const) - have "(\n. (\k. measure M (A (k+n)))) \ 0" by (rule suminf_exist_split2[OF assms(3)]) + have "(\n. (\k. measure M (A (k+n)))) \ 0" by (rule suminf_exist_split2[OF sum]) then show "(\n. ennreal (\k. measure M (A (k+n)))) \ 0" unfolding ennreal_0[symmetric] by (intro tendsto_ennrealI) have "emeasure M (limsup A) \ (\k. measure M (A (k+n)))" for n proof - have I: "(\k\{n..}. A k) = (\k. A (k+n))" by (auto, metis le_add_diff_inverse2, fastforce) have "emeasure M (limsup A) \ emeasure M (\k\{n..}. A k)" - by (rule emeasure_mono, auto simp add: limsup_INF_SUP) + by (rule emeasure_mono, auto simp: limsup_INF_SUP) also have "\ = emeasure M (\k. A (k+n))" using I by auto also have "\ \ (\k. measure M (A (k+n)))" apply (rule emeasure_union_summable) - using assms summable_ignore_initial_segment[OF assms(3), of n] by auto + using assms summable_ignore_initial_segment[OF sum, of n] by auto finally show ?thesis by simp qed then show "\N. \n\N. emeasure M (limsup A) \ (\k. measure M (A (k+n)))" @@ -2113,11 +2107,6 @@ assumes "A \ B" "B \ sets M" shows "measure M A \ measure M B" using emeasure_mono[OF assms] emeasure_real[of A] emeasure_real[of B] by (auto simp: measure_def) -lemma (in finite_measure) finite_measure_subadditive: - assumes m: "A \ sets M" "B \ sets M" - shows "measure M (A \ B) \ measure M A + measure M B" - using measure_subadditive[OF m] by simp - lemma (in finite_measure) finite_measure_subadditive_finite: assumes "finite I" "A`I \ sets M" shows "measure M (\i\I. A i) \ (\i\I. measure M (A i))" using measure_subadditive_finite[OF assms] by simp @@ -2163,21 +2152,21 @@ by (auto intro!: finite_measure_mono simp: increasing_def) lemma (in finite_measure) measure_zero_union: - assumes "s \ sets M" "t \ sets M" "measure M t = 0" - shows "measure M (s \ t) = measure M s" + assumes "S \ sets M" "T \ sets M" "measure M T = 0" + shows "measure M (S \ T) = measure M S" using assms proof - - have "measure M (s \ t) \ measure M s" - using finite_measure_subadditive[of s t] assms by auto - moreover have "measure M (s \ t) \ measure M s" + have "measure M (S \ T) \ measure M S" + by (metis add.right_neutral assms measure_Un_le) + moreover have "measure M (S \ T) \ measure M S" using assms by (blast intro: finite_measure_mono) ultimately show ?thesis by simp qed lemma (in finite_measure) measure_eq_compl: - assumes "s \ sets M" "t \ sets M" - assumes "measure M (space M - s) = measure M (space M - t)" - shows "measure M s = measure M t" + assumes "S \ sets M" "T \ sets M" + assumes "measure M (space M - S) = measure M (space M - T)" + shows "measure M S = measure M T" using assms finite_measure_compl by auto lemma (in finite_measure) measure_eq_bigunion_image: @@ -2204,53 +2193,53 @@ qed simp lemma (in finite_measure) measure_space_inter: - assumes events:"s \ sets M" "t \ sets M" - assumes "measure M t = measure M (space M)" - shows "measure M (s \ t) = measure M s" + assumes events:"S \ sets M" "T \ sets M" + assumes "measure M T = measure M (space M)" + shows "measure M (S \ T) = measure M S" proof - - have "measure M ((space M - s) \ (space M - t)) = measure M (space M - s)" - using events assms finite_measure_compl[of "t"] by (auto intro!: measure_zero_union) - also have "(space M - s) \ (space M - t) = space M - (s \ t)" + have "measure M ((space M - S) \ (space M - T)) = measure M (space M - S)" + using events assms finite_measure_compl[of "T"] by (auto intro!: measure_zero_union) + also have "(space M - S) \ (space M - T) = space M - (S \ T)" by blast - finally show "measure M (s \ t) = measure M s" - using events by (auto intro!: measure_eq_compl[of "s \ t" s]) + finally show "measure M (S \ T) = measure M S" + using events by (auto intro!: measure_eq_compl[of "S \ T" S]) qed lemma (in finite_measure) measure_equiprobable_finite_unions: - assumes s: "finite s" "\x. x \ s \ {x} \ sets M" - assumes "\ x y. \x \ s; y \ s\ \ measure M {x} = measure M {y}" - shows "measure M s = real (card s) * measure M {SOME x. x \ s}" + assumes S: "finite S" "\x. x \ S \ {x} \ sets M" + assumes "\ x y. \x \ S; y \ S\ \ measure M {x} = measure M {y}" + shows "measure M S = real (card S) * measure M {SOME x. x \ S}" proof cases - assume "s \ {}" - then have "\ x. x \ s" by blast + assume "S \ {}" + then have "\ x. x \ S" by blast from someI_ex[OF this] assms - have prob_some: "\ x. x \ s \ measure M {x} = measure M {SOME y. y \ s}" by blast - have "measure M s = (\ x \ s. measure M {x})" - using finite_measure_eq_sum_singleton[OF s] by simp - also have "\ = (\ x \ s. measure M {SOME y. y \ s})" using prob_some by auto - also have "\ = real (card s) * measure M {(SOME x. x \ s)}" + have prob_some: "\ x. x \ S \ measure M {x} = measure M {SOME y. y \ S}" by blast + have "measure M S = (\ x \ S. measure M {x})" + using finite_measure_eq_sum_singleton[OF S] by simp + also have "\ = (\ x \ S. measure M {SOME y. y \ S})" using prob_some by auto + also have "\ = real (card S) * measure M {(SOME x. x \ S)}" using sum_constant assms by simp finally show ?thesis by simp qed simp lemma (in finite_measure) measure_real_sum_image_fn: assumes "e \ sets M" - assumes "\ x. x \ s \ e \ f x \ sets M" - assumes "finite s" - assumes disjoint: "\ x y. \x \ s ; y \ s ; x \ y\ \ f x \ f y = {}" - assumes upper: "space M \ (\i \ s. f i)" - shows "measure M e = (\ x \ s. measure M (e \ f x))" + assumes "\ x. x \ S \ e \ f x \ sets M" + assumes "finite S" + assumes disjoint: "\ x y. \x \ S ; y \ S ; x \ y\ \ f x \ f y = {}" + assumes upper: "space M \ (\i \ S. f i)" + shows "measure M e = (\ x \ S. measure M (e \ f x))" proof - - have "e \ (\i\s. f i)" + have "e \ (\i\S. f i)" using \e \ sets M\ sets.sets_into_space upper by blast - then have e: "e = (\i \ s. e \ f i)" + then have e: "e = (\i \ S. e \ f i)" by auto - hence "measure M e = measure M (\i \ s. e \ f i)" by simp - also have "\ = (\ x \ s. measure M (e \ f x))" + hence "measure M e = measure M (\i \ S. e \ f i)" by simp + also have "\ = (\ x \ S. measure M (e \ f x))" proof (rule finite_measure_finite_Union) - show "finite s" by fact - show "(\i. e \ f i)`s \ sets M" using assms(2) by auto - show "disjoint_family_on (\i. e \ f i) s" + show "finite S" by fact + show "(\i. e \ f i)`S \ sets M" using assms(2) by auto + show "disjoint_family_on (\i. e \ f i) S" using disjoint by (auto simp: disjoint_family_on_def) qed finally show ?thesis . @@ -2286,7 +2275,7 @@ next show "f x \ (\s. emeasure (M s) {x \ space N. F top x})" for x using bound[of x] sets_eq_imp_space_eq[OF sets] by (simp add: iter) -qed (auto simp add: iter le_fun_def INF_apply[abs_def] intro!: meas cont) +qed (auto simp: iter le_fun_def INF_apply[abs_def] intro!: meas cont) subsection\<^marker>\tag unimportant\ \Counting space\ @@ -2357,8 +2346,8 @@ by (rule infinite_super[OF _ 1]) auto then have "infinite (\i. F i)" by auto - ultimately show ?thesis by (simp only:) simp - + ultimately show ?thesis + by (metis (mono_tags, lifting) infinity_ennreal_def) qed qed qed @@ -2391,8 +2380,9 @@ using emeasure_count_space[of X A] by simp lemma measure_count_space: "measure (count_space A) X = (if X \ A then of_nat (card X) else 0)" - by (cases "finite X") (auto simp: measure_notin_sets ennreal_of_nat_eq_real_of_nat - measure_zero_top measure_eq_emeasure_eq_ennreal) + by (cases "finite X") + (auto simp: measure_notin_sets ennreal_of_nat_eq_real_of_nat + measure_zero_top measure_eq_emeasure_eq_ennreal) lemma emeasure_count_space_eq_0: "emeasure (count_space A) X = 0 \ (X \ A \ X = {})" @@ -2407,19 +2397,19 @@ qed (simp add: emeasure_notin_sets) lemma null_sets_count_space: "null_sets (count_space A) = { {} }" - unfolding null_sets_def by (auto simp add: emeasure_count_space_eq_0) + unfolding null_sets_def by (auto simp: emeasure_count_space_eq_0) lemma AE_count_space: "(AE x in count_space A. P x) \ (\x\A. P x)" - unfolding eventually_ae_filter by (auto simp add: null_sets_count_space) + unfolding eventually_ae_filter by (auto simp: null_sets_count_space) lemma sigma_finite_measure_count_space_countable: assumes A: "countable A" shows "sigma_finite_measure (count_space A)" - proof qed (insert A, auto intro!: exI[of _ "(\a. {a}) ` A"]) + proof qed (use A in \auto intro!: exI[of _ "(\a. {a}) ` A"]\) lemma sigma_finite_measure_count_space: fixes A :: "'a::countable set" shows "sigma_finite_measure (count_space A)" - by (rule sigma_finite_measure_count_space_countable) auto + using countableI_type sigma_finite_measure_count_space_countable by blast lemma finite_measure_count_space: assumes [simp]: "finite A" @@ -2428,10 +2418,7 @@ lemma sigma_finite_measure_count_space_finite: assumes A: "finite A" shows "sigma_finite_measure (count_space A)" -proof - - interpret finite_measure "count_space A" using A by (rule finite_measure_count_space) - show "sigma_finite_measure (count_space A)" .. -qed + by (simp add: assms finite_measure.axioms(1) finite_measure_count_space) subsection\<^marker>\tag unimportant\ \Measure restricted to space\ @@ -2453,15 +2440,13 @@ by (fastforce simp: sets_restrict_space_iff[OF assms(1)] image_subset_iff dest: sets.sets_into_space)+ then show "(\i. emeasure M (A i)) = emeasure M (\i. A i)" - by (subst suminf_emeasure) (auto simp: disjoint_family_subset) + by (simp add: image_subset_iff suminf_emeasure) qed qed next case False - with assms have "A \ sets (restrict_space M \)" - by (simp add: sets_restrict_space_iff) - with False show ?thesis - by (simp add: emeasure_notin_sets) + with assms show ?thesis + by (metis emeasure_notin_sets sets_restrict_space_iff) qed lemma measure_restrict_space: @@ -2475,14 +2460,12 @@ proof - have ex_cong: "\P Q f. (\x. P x \ Q x) \ (\x. Q x \ P (f x)) \ (\x. P x) \ (\x. Q x)" by auto - { fix X assume X: "X \ sets M" "emeasure M X = 0" - then have "emeasure M (\ \ space M \ X) \ emeasure M X" - by (intro emeasure_mono) auto - then have "emeasure M (\ \ space M \ X) = 0" - using X by (auto intro!: antisym) } + have "emeasure M (\ \ space M \ X) = 0" + if "X \ sets M" "emeasure M X = 0" for X + by (meson emeasure_eq_0 inf_le2 that) with assms show ?thesis unfolding eventually_ae_filter - by (auto simp add: space_restrict_space null_sets_def sets_restrict_space_iff + by (auto simp: space_restrict_space null_sets_def sets_restrict_space_iff emeasure_restrict_space cong: conj_cong intro!: ex_cong[where f="\X. (\ \ space M) \ X"]) qed @@ -2509,7 +2492,7 @@ moreover fix X assume "X \ sets (restrict_space (count_space B) A)" ultimately have "X \ A \ B" by auto then show "emeasure (restrict_space (count_space B) A) X = emeasure (count_space (A \ B)) X" - by (cases "finite X") (auto simp add: emeasure_restrict_space) + by (cases "finite X") (auto simp: emeasure_restrict_space) qed lemma sigma_finite_measure_restrict_space: @@ -2523,28 +2506,24 @@ by blast let ?C = "(\) A ` C" from C have "countable ?C" "?C \ sets (restrict_space M A)" "(\?C) = space (restrict_space M A)" - by(auto simp add: sets_restrict_space space_restrict_space) + by(auto simp: sets_restrict_space space_restrict_space) moreover { fix a assume "a \ ?C" then obtain a' where "a = A \ a'" "a' \ C" .. then have "emeasure (restrict_space M A) a \ emeasure M a'" - using A C by(auto simp add: emeasure_restrict_space intro: emeasure_mono) - also have "\ < \" using C(4)[rule_format, of a'] \a' \ C\ by (simp add: less_top) + using A C by(auto simp: emeasure_restrict_space intro: emeasure_mono) + also have "\ < \" using C(4) \a' \ C\ top.not_eq_extremum by auto finally have "emeasure (restrict_space M A) a \ \" by simp } ultimately show ?thesis - by unfold_locales (rule exI conjI|assumption|blast)+ + by (meson sigma_finite_measure_def) qed lemma finite_measure_restrict_space: assumes "finite_measure M" and A: "A \ sets M" shows "finite_measure (restrict_space M A)" -proof - - interpret finite_measure M by fact - show ?thesis - by(rule finite_measureI)(simp add: emeasure_restrict_space A space_restrict_space) -qed + by (simp add: assms emeasure_restrict_space finite_measure.emeasure_finite finite_measureI) lemma restrict_distr: assumes [measurable]: "f \ measurable M N" @@ -2554,9 +2533,8 @@ proof (rule measure_eqI) fix A assume "A \ sets (restrict_space (distr M N f) \)" with restrict show "emeasure ?l A = emeasure ?r A" - by (subst emeasure_distr) - (auto simp: sets_restrict_space_iff emeasure_restrict_space emeasure_distr - intro!: measurable_restrict_space2) + by (simp add: emeasure_distr emeasure_restrict_space measurable_restrict_space2 + sets_restrict_space_iff) qed (simp add: sets_restrict_space) lemma measure_eqI_restrict_generator: @@ -2570,12 +2548,13 @@ proof (rule measure_eqI) fix X assume X: "X \ sets M" then have "emeasure M X = emeasure (restrict_space M \) (X \ \)" - using ae \ by (auto simp add: emeasure_restrict_space intro!: emeasure_eq_AE) + using ae \ by (auto simp: emeasure_restrict_space intro!: emeasure_eq_AE) also have "restrict_space M \ = restrict_space N \" proof (rule measure_eqI_generator_eq) fix X assume "X \ E" then show "emeasure (restrict_space M \) X = emeasure (restrict_space N \) X" - using E \ by (subst (1 2) emeasure_restrict_space) (auto simp: sets_eq sets_eq[THEN sets_eq_imp_space_eq]) + using \ E + by (metis Pow_iff emeasure_restrict_space inf.orderE sets.sets_into_space sets_eq subsetD) next show "range (from_nat_into A) \ E" "(\i. from_nat_into A i) = \" using A by (auto cong del: SUP_cong_simp) @@ -2588,7 +2567,7 @@ by (auto intro: from_nat_into) qed fact+ also have "emeasure (restrict_space N \) (X \ \) = emeasure N X" - using X ae \ by (auto simp add: emeasure_restrict_space sets_eq intro!: emeasure_eq_AE) + using X ae \ by (auto simp: emeasure_restrict_space sets_eq intro!: emeasure_eq_AE) finally show "emeasure M X = emeasure N X" . qed fact @@ -2695,14 +2674,10 @@ have le_\[intro]: "X \ sets M \ d X \ \" for X by (auto simp: \_def intro!: cSUP_upper) - have "\f. \n. f n \ sets M \ d (f n) > \ - 1 / 2^n" - proof (intro choice_iff[THEN iffD1] allI) - fix n - have "\X\sets M. \ - 1 / 2^n < d X" - unfolding \_def by (intro less_cSUP_iff[THEN iffD1]) auto - then show "\y. y \ sets M \ \ - 1 / 2 ^ n < d y" - by auto - qed + have "\X\sets M. \ - 1 / 2^n < d X" for n + unfolding \_def by (intro less_cSUP_iff[THEN iffD1]) auto + then have "\f. \n. f n \ sets M \ d (f n) > \ - 1 / 2^n" + by metis then obtain E where [measurable]: "E n \ sets M" and E: "d (E n) > \ - 1 / 2^n" for n by auto @@ -2987,9 +2962,8 @@ using sets.sigma_sets_subset[of \ x] by auto lemma sigma_le_iff: "\ \ Pow \ \ sigma \ \ \ x \ (\ \ space x \ (space x = \ \ \ \ sets x))" - by (cases "\ = space x") - (simp_all add: eq_commute[of _ "sets x"] le_measure_iff emeasure_sigma le_fun_def - sigma_sets_superset_generator sigma_sets_le_sets_iff) + apply (simp add: le_measure_iff le_fun_def emeasure_sigma) + by (metis order_refl sets_measure_of sigma_sets_le_sets_iff) instantiation measure :: (type) semilattice_sup begin @@ -3057,7 +3031,7 @@ by (intro less_eq_measure.intros(2)) simp_all next case 3 with \z \ y\ \x \ y\ show ?thesis - by (auto simp add: le_measure intro!: emeasure_sup_measure'_le2) + by (auto simp: le_measure intro!: emeasure_sup_measure'_le2) qed next assume **: "x \ y" "z \ y" "space x = space z" "\ sets z \ sets x" "\ sets x \ sets z" @@ -3083,7 +3057,7 @@ by (auto dest: sets_eq_imp_space_eq simp add: le_measure_iff split: if_split_asm) lemma sets_sup: "sets A = sets M \ sets B = sets M \ sets (sup A B) = sets M" - by (auto simp add: sup_measure_def sup_lexord_def dest: sets_eq_imp_space_eq) + by (auto simp: sup_measure_def sup_lexord_def dest: sets_eq_imp_space_eq) lemma le_measureD1: "A \ B \ space A \ space B" by (auto simp: le_measure_iff split: if_split_asm) @@ -3110,18 +3084,13 @@ by (auto simp: Sup_lexord_def Let_def) lemma Sup_lexord1: - assumes A: "A \ {}" "(\a. a \ A \ k a = (\a\A. k a))" "P (c A)" + assumes A: "A \ {}" and eq: "(\a. a \ A \ k a = (\a\A. k a))" and P: "P (c A)" shows "P (Sup_lexord k c s A)" - unfolding Sup_lexord_def Let_def -proof (clarsimp, safe) - show "\a\A. k a \ (\x\A. k x) \ P (s A)" - by (metis assms(1,2) ex_in_conv) -next - fix a assume "a \ A" "k a = (\x\A. k x)" - then have "{a \ A. k a = (\x\A. k x)} = {a \ A. k a = k a}" - by (metis A(2)[symmetric]) - then show "P (c {a \ A. k a = (\x\A. k x)})" - by (simp add: A(3)) +proof - + have "{a \ A. k a = \(k ` A)} = A" for a :: 'a + by (metis (mono_tags, lifting) Collect_cong Collect_mem_eq eq) + then show ?thesis + using A P by (auto simp: Sup_lexord_def Let_def) qed instantiation measure :: (type) complete_lattice @@ -3137,19 +3106,8 @@ by simp next case (insert i J) - show ?case - proof cases - assume "i \ I" with insert show ?thesis - by (auto simp: insert_absorb) - next - assume "i \ I" - have "sup_measure.F id I \ sup_measure.F id (I \ J)" - by (intro insert) - also have "\ \ sup_measure.F id (insert i (I \ J))" - using insert \i \ I\ by (subst sup_measure.insert) auto - finally show ?thesis - by auto - qed + then show ?case + by (metis finite.insertI sup.orderE sup_ge1 sup_ge2 sup_measure.union_diff2 sup_measure.union_inter) qed lemma sup_measure_F_mono: "finite I \ J \ I \ sup_measure.F id J \ sup_measure.F id I" @@ -3214,9 +3172,10 @@ proof (intro arg_cong [of _ _ Sup] image_cong refl) fix i assume i: "i \ {P. finite P \ P \ M}" show "(\n. ?\ i (F n)) = ?\ i (\(F ` UNIV))" - proof cases - assume "i \ {}" with i ** show ?thesis - by (smt (verit, best) "1"(2) Measure_Space.sets_sup_measure_F assms(1) mem_Collect_eq subset_eq suminf_cong suminf_emeasure) + proof (cases "i = {}") + case False + with i ** sets_eq show ?thesis + by (smt (verit, best) "1"(2) Measure_Space.sets_sup_measure_F mem_Collect_eq subset_eq suminf_cong suminf_emeasure) qed simp qed qed @@ -3300,7 +3259,7 @@ proof (subst emeasure_Sup_measure'[OF _ \X \ sets x\]) show "emeasure x X \ (SUP P \ {P. finite P \ P \ S'}. emeasure (sup_measure.F id P) X)" using \x\S'\ by (intro SUP_upper2[where i="{x}"]) auto - qed (insert \x\S'\ S', auto) + qed (use \x\S'\ S' in auto) qed next assume "x \ S'" @@ -3309,15 +3268,12 @@ moreover have "sets x \ sets b" using \x\S\ unfolding b by auto ultimately show ?thesis - using * \x \ S\ - by (intro less_eq_measure.intros(2)) - (simp_all add: * \space x = space b\ less_le) + using * \x \ S\ by (simp add: le_measure_iff sets_le_imp_space_le) qed next assume "x \ S" with \x\A\ \x \ S\ \space b = space a\ show ?thesis - by (intro less_eq_measure.intros) - (simp_all add: * less_le a SUP_upper S) + by (simp add: "*" S SUP_upper2 a le_measure_iff) qed qed show least: "Sup A \ x" if x: "\z. z \ A \ z \ x" for x :: "'a measure" and A @@ -3397,7 +3353,7 @@ next assume "space x \ space a" then have "space a < space x" - using le_measureD1[OF x[OF \a\A\]] by auto + by (simp add: \a \ A\ le_measureD1 psubsetI x) then show "Sup_measure' S' \ x" by (intro less_eq_measure.intros) (simp add: * \space b = space a\) qed @@ -3447,15 +3403,15 @@ show "\j\{J. J \ {} \ finite J \ J \ I}. sup_measure.F id J X \ (SUP i\j. M i) X" proof cases assume "J' = {}" with \i \ I\ show ?thesis - by (auto simp add: J) + by (auto simp: J) next assume "J' \ {}" with J J' show ?thesis - by (intro bexI[of _ "J'"]) (auto simp add: eq simp del: id_apply) + using eq by auto qed next fix J assume J: "J \ {P. P \ {} \ finite P \ P \ I}" show "\J'\{J. finite J \ J \ M`I}. (SUP i\J. M i) X \ sup_measure.F id J' X" - using J by (intro bexI[of _ "M`J"]) (auto simp add: eq simp del: id_apply) + using J by (intro bexI[of _ "M`J"]) (auto simp: eq simp del: id_apply) qed finally show ?thesis . qed @@ -3485,9 +3441,15 @@ lemma space_Sup_eq_UN: "space (Sup M) = (\x\M. space x)" (is "?L=?R") proof show "?L \ ?R" - using Sup_lexord[where P="\x. space x = _"] - apply (clarsimp simp: Sup_measure_def) - by (smt (verit) Sup_lexord_def UN_E mem_Collect_eq space_Sup_measure'2 space_measure_of_conv) + proof - + define A where "A \ {a \ M. space a = \ (space ` M)}" + have "\x\M. a \ space x" + if "a \ space (Sup_measure' {a \ A. sets a = \ (sets ` A)})" + for a + by (metis (no_types, lifting) A_def UN_E mem_Collect_eq space_Sup_measure'2 that) + then show ?thesis + by (auto simp: A_def space_measure_of_conv Sup_measure_def Sup_lexord_def Let_def split: if_splits) + qed qed (use Sup_upper le_measureD1 in fastforce) @@ -3546,7 +3508,7 @@ shows "f \ measurable (Sup M) N" proof - have "space (Sup M) = space m" - using m by (auto simp add: space_Sup_eq_UN dest: const_space) + using m by (auto simp: space_Sup_eq_UN dest: const_space) then show ?thesis using m f unfolding measurable_def by (auto intro: in_sets_Sup[OF const_space]) qed @@ -3581,13 +3543,13 @@ assumes [simp]: "M \ {}" and M: "\m. m \ M \ m \ Pow \" shows "sets (SUP m\M. sigma \ m) = sets (sigma \ (\M))" proof - - { fix a m assume "a \ sigma_sets \ m" "m \ M" - then have "a \ sigma_sets \ (\M)" - by induction (auto intro: sigma_sets.intros(2-)) } + have "a \ sigma_sets \ (\M)" + if "a \ sigma_sets \ m" "m \ M" for a m + using that by induction (auto intro: sigma_sets.intros) then have "sigma_sets \ (\ (sigma_sets \ ` M)) = sigma_sets \ (\ M)" by (smt (verit, best) UN_iff Union_iff sigma_sets.Basic sigma_sets_eqI) then show "sets (SUP m\M. sigma \ m) = sets (sigma \ (\M))" - by (subst sets_Sup_eq) (fastforce simp add: M Union_least)+ + by (subst sets_Sup_eq) (fastforce simp: M Union_least)+ qed lemma Sup_sigma: @@ -3600,10 +3562,10 @@ proof (intro less_eq_measure.intros(3)) show "space (sigma \ (\M)) = space (SUP m\M. sigma \ m)" "sets (sigma \ (\M)) = sets (SUP m\M. sigma \ m)" - by (auto simp add: M sets_Sup_sigma sets_eq_imp_space_eq space_measure_of_conv) + by (auto simp: M sets_Sup_sigma sets_eq_imp_space_eq space_measure_of_conv) qed (simp add: emeasure_sigma le_fun_def) fix m assume "m \ M" then show "sigma \ m \ sigma \ (\M)" - by (subst sigma_le_iff) (auto simp add: M *) + by (subst sigma_le_iff) (auto simp: M *) qed lemma SUP_sigma_sigma: @@ -3615,29 +3577,25 @@ shows "sets (vimage_algebra X f (Sup M)) = sets (SUP m \ M. vimage_algebra X f m)" (is "?L = ?R") proof - have "\m. m \ M \ f \ Sup (vimage_algebra X f ` M) \\<^sub>M m" - using assms - by (smt (verit, del_insts) Pi_iff imageE image_eqI measurable_Sup1 - measurable_vimage_algebra1 space_vimage_algebra) + { fix m + assume "m \ M" + then have "f \ vimage_algebra X f m \\<^sub>M m" + by (simp add: assms measurable_vimage_algebra1) + then have "f \ Sup (vimage_algebra X f ` M) \\<^sub>M m" + using \m \ M\ by (force simp: intro: measurable_Sup1) + } then show "?L \ ?R" - by (intro sets_image_in_sets measurable_Sup2) (simp_all add: space_Sup_eq_UN *) + by (intro sets_image_in_sets measurable_Sup2) (simp_all add: space_Sup_eq_UN *) show "?R \ ?L" apply (intro sets_Sup_in_sets) - apply (force simp add: * space_Sup_eq_UN sets_vimage_algebra2 intro: in_sets_Sup)+ + apply (force simp: * space_Sup_eq_UN sets_vimage_algebra2 intro: in_sets_Sup)+ done qed lemma restrict_space_eq_vimage_algebra': "sets (restrict_space M \) = sets (vimage_algebra (\ \ space M) (\x. x) M)" -proof - - have *: "{A \ (\ \ space M) |A. A \ sets M} = {A \ \ |A. A \ sets M}" - using sets.sets_into_space[of _ M] by blast - - show ?thesis - unfolding restrict_space_def - by (subst sets_measure_of) - (auto simp add: image_subset_iff sets_vimage_algebra * dest: sets.sets_into_space intro!: arg_cong2[where f=sigma_sets]) -qed + by (metis Int_assoc image_cong inf_le2 restrict_space_eq_vimage_algebra + sets.Int_space_eq1 sets_restrict_space) lemma sigma_le_sets: assumes [simp]: "A \ Pow X" shows "sets (sigma X A) \ sets N \ X \ sets N \ A \ sets N" @@ -3657,8 +3615,13 @@ lemma measurable_iff_sets: "f \ measurable M N \ (f \ space M \ space N \ sets (vimage_algebra (space M) f N) \ sets M)" - unfolding measurable_def - by (smt (verit, ccfv_threshold) mem_Collect_eq sets_vimage_algebra sigma_sets_le_sets_iff subset_eq) + (is "?L = ?R") +proof + show "?L \ ?R" + by (simp add: measurable_space sets_image_in_sets) + show "?R \ ?L" + by (simp add: in_vimage_algebra measurable_def subset_eq) +qed lemma sets_vimage_algebra_space: "X \ sets (vimage_algebra X f M)" using sets.top[of "vimage_algebra X f M"] by simp @@ -3669,19 +3632,21 @@ shows "measurable M N \ measurable M' N'" unfolding measurable_def proof safe - fix f A assume "f \ space M \ space N" "A \ sets N'" - moreover assume "\y\sets N. f -` y \ space M \ sets M" note this[THEN bspec, of A] - ultimately show "f -` A \ space M' \ sets M'" - using assms by auto + fix f A + assume "f \ space M \ space N" "A \ sets N'" + "\y\sets N. f -` y \ space M \ sets M" + then show "f -` A \ space M' \ sets M'" + using assms by (metis subset_eq) qed (use N M in auto) lemma measurable_Sup_measurable: assumes f: "f \ space N \ A" shows "f \ measurable N (Sup {M. space M = A \ f \ measurable N M})" proof (rule measurable_Sup2) - show "{M. space M = A \ f \ measurable N M} \ {}" - using f unfolding ex_in_conv[symmetric] - by (intro exI[of _ "sigma A {}"]) (auto intro!: measurable_measure_of) + have "f \ N \\<^sub>M sigma A {}" + by (meson empty_subsetI equals0D f measurable_measure_of) + then show "{M. space M = A \ f \ measurable N M} \ {}" + by fastforce qed auto lemma (in sigma_algebra) sigma_sets_subset': @@ -3709,9 +3674,7 @@ lemma mono_vimage_algebra: "sets M \ sets N \ sets (vimage_algebra X f M) \ sets (vimage_algebra X f N)" - using sets.top[of "sigma X {f -` A \ X |A. A \ sets N}"] - unfolding vimage_algebra_def - by (smt (verit, del_insts) space_measure_of sigma_le_sets Pow_iff inf_le2 mem_Collect_eq subset_eq) + by (simp add: in_vimage_algebra sets_image_in_sets' sets_vimage_algebra_space subsetD) lemma mono_restrict_space: "sets M \ sets N \ sets (restrict_space M X) \ sets (restrict_space N X)" unfolding sets_restrict_space by (rule image_mono) diff -r 3dfd62b4e2c8 -r ad31be996dcb src/HOL/Analysis/Weierstrass_Theorems.thy --- a/src/HOL/Analysis/Weierstrass_Theorems.thy Tue Apr 22 19:02:33 2025 +0200 +++ b/src/HOL/Analysis/Weierstrass_Theorems.thy Tue Apr 22 22:06:52 2025 +0100 @@ -81,7 +81,7 @@ have ucontf: "uniformly_continuous_on {0..1} f" using compact_uniformly_continuous contf by blast then obtain d where d: "d>0" "\x x'. \ x \ {0..1}; x' \ {0..1}; \x' - x\ < d\ \ \f x' - f x\ < e/2" - apply (rule uniformly_continuous_onE [where e = "e/2"]) + apply (rule uniformly_continuous_onE [where \ = "e/2"]) using e by (auto simp: dist_norm) { fix n::nat and x::real assume n: "Suc (nat\4*M/(e*d\<^sup>2)\) \ n" and x: "0 \ x" "x \ 1" diff -r 3dfd62b4e2c8 -r ad31be996dcb src/HOL/Complex_Analysis/Cauchy_Integral_Formula.thy --- a/src/HOL/Complex_Analysis/Cauchy_Integral_Formula.thy Tue Apr 22 19:02:33 2025 +0200 +++ b/src/HOL/Complex_Analysis/Cauchy_Integral_Formula.thy Tue Apr 22 22:06:52 2025 +0100 @@ -1887,7 +1887,7 @@ and \: "\x x'. \x\?TZ; x'\?TZ; dist x' x < \\ \ dist ((\(x,y). F x y) x') ((\(x,y). F x y) x) < \/norm(b-a)" using \0 < \\ \a \ b\ - by (auto elim: uniformly_continuous_onE [where e = "\/norm(b-a)"]) + by (auto elim: uniformly_continuous_onE [where \ = "\/norm(b-a)"]) have \: "\norm (w - x1) \ \; x2 \ closed_segment a b; norm (w - x1') \ \; x2' \ closed_segment a b; norm ((x1', x2') - (x1, x2)) < \\ \ norm (F x1' x2' - F x1 x2) \ \ / cmod (b-a)" @@ -2239,7 +2239,7 @@ then obtain kk where "kk>0" and kk: "\x x'. \x \ ?ddpa; x' \ ?ddpa; dist x' x < kk\ \ dist ((\(x,y). d x y) x') ((\(x,y). d x y) x) < ee" - by (rule uniformly_continuous_onE [where e = ee]) (use \0 < ee\ in auto) + by (rule uniformly_continuous_onE [where \ = ee]) (use \0 < ee\ in auto) have kk: "\norm (w-x) \ dd; z \ path_image \; norm ((w, z) - (x, z)) < kk\ \ norm (d w z - d x z) < ee" for w z using \dd>0\ kk [of "(x,z)" "(w,z)"] by (force simp: norm_minus_commute dist_norm) diff -r 3dfd62b4e2c8 -r ad31be996dcb src/HOL/Complex_Analysis/Conformal_Mappings.thy --- a/src/HOL/Complex_Analysis/Conformal_Mappings.thy Tue Apr 22 19:02:33 2025 +0200 +++ b/src/HOL/Complex_Analysis/Conformal_Mappings.thy Tue Apr 22 22:06:52 2025 +0100 @@ -1703,7 +1703,7 @@ then have [simp]: "closure {r'<.. = "min d e/2"]) apply (auto simp: \d>0\ \e>0\ dist_norm wnwn) done qed diff -r 3dfd62b4e2c8 -r ad31be996dcb src/HOL/Probability/Sinc_Integral.thy --- a/src/HOL/Probability/Sinc_Integral.thy Tue Apr 22 19:02:33 2025 +0200 +++ b/src/HOL/Probability/Sinc_Integral.thy Tue Apr 22 22:06:52 2025 +0100 @@ -128,7 +128,7 @@ by (auto simp: isCont_def sinc_at_0) next assume "x \ 0" show ?thesis - by (rule continuous_transform_within [where d = "abs x" and f = "\x. sin x / x"]) + by (rule continuous_transform_within [where \ = "abs x" and f = "\x. sin x / x"]) (auto simp add: dist_real_def \x \ 0\) qed