# HG changeset patch # User nipkow # Date 1574978782 -3600 # Node ID 575b3a818de59d5d1d43ef3833f6e8d2a3114b5c # Parent a25b6f79043f29a93f050e76f99dde01881ea995 tuned diff -r a25b6f79043f -r 575b3a818de5 src/HOL/Analysis/Abstract_Euclidean_Space.thy --- a/src/HOL/Analysis/Abstract_Euclidean_Space.thy Thu Nov 28 20:38:07 2019 +0100 +++ b/src/HOL/Analysis/Abstract_Euclidean_Space.thy Thu Nov 28 23:06:22 2019 +0100 @@ -144,7 +144,7 @@ unfolding homeomorphic_space_def homeomorphic_maps_def apply (rule_tac x="\f. restrict f {.. real" where "p \ \i. if i = k then 1 else 0" have "p \ topspace(nsphere n)" using assms - by (simp add: nsphere topspace_subtopology p_def power2_eq_square if_distrib [where f = "\x. x * _"] cong: if_cong) + by (simp add: nsphere p_def power2_eq_square if_distrib [where f = "\x. x * _"] cong: if_cong) let ?g = "\x i. x i / sqrt(\j\n. x j ^ 2)" let ?h = "\(t,q) i. (1 - t) * q i + t * p i" let ?Y = "subtopology (Euclidean_space (Suc n)) {x. 0 \ x k \ (\i\n. x i \ 0)}" @@ -262,7 +262,7 @@ by (metis add.commute add_le_same_cancel2 diff_ge_0_iff_ge diff_zero less_eq_real_def mult_eq_0_iff mult_nonneg_nonneg not_le numeral_One zero_neq_numeral) show "continuous_map (prod_topology (top_of_set {0..1}) (subtopology (nsphere n) {x. 0 \ x k})) ?Y ?h" using assms - apply (auto simp: * nsphere topspace_subtopology continuous_map_componentwise_UNIV + apply (auto simp: * nsphere continuous_map_componentwise_UNIV prod_topology_subtopology subtopology_subtopology case_prod_unfold continuous_map_in_subtopology Euclidean_space_def p_def if_distrib [where f = "\x. _ * x"] cong: if_cong) apply (intro continuous_map_prod_snd continuous_intros continuous_map_from_subtopology) @@ -286,7 +286,7 @@ moreover have "(?g \ ?h) (0, x) = x" if "x \ topspace (subtopology (nsphere n) {x. 0 \ x k})" for x using that - by (simp add: assms topspace_subtopology nsphere) + by (simp add: assms nsphere) moreover have "(?g \ ?h) (1, x) = p" if "x \ topspace (subtopology (nsphere n) {x. 0 \ x k})" for x diff -r a25b6f79043f -r 575b3a818de5 src/HOL/Analysis/Abstract_Limits.thy --- a/src/HOL/Analysis/Abstract_Limits.thy Thu Nov 28 20:38:07 2019 +0100 +++ b/src/HOL/Analysis/Abstract_Limits.thy Thu Nov 28 23:06:22 2019 +0100 @@ -79,16 +79,16 @@ have "\\<^sub>F b in F. f b \ topspace X \ S" by (metis (no_types) limitin_def openin_topspace topspace_subtopology) with L show ?rhs - apply (clarsimp simp add: limitin_def eventually_mono topspace_subtopology openin_subtopology_alt) + apply (clarsimp simp add: limitin_def eventually_mono openin_subtopology_alt) apply (drule_tac x="S \ U" in spec, force simp: elim: eventually_mono) done next assume ?rhs then show ?lhs using eventually_elim2 - by (fastforce simp add: limitin_def topspace_subtopology openin_subtopology_alt) + by (fastforce simp add: limitin_def openin_subtopology_alt) qed -qed (auto simp: limitin_def topspace_subtopology) +qed (auto simp: limitin_def) lemma limitin_canonical_iff_gen [simp]: diff -r a25b6f79043f -r 575b3a818de5 src/HOL/Analysis/Abstract_Topology.thy --- a/src/HOL/Analysis/Abstract_Topology.thy Thu Nov 28 20:38:07 2019 +0100 +++ b/src/HOL/Analysis/Abstract_Topology.thy Thu Nov 28 23:06:22 2019 +0100 @@ -299,7 +299,7 @@ lemma topspace_subtopology_subset: "S \ topspace X \ topspace(subtopology X S) = S" - by (simp add: inf.absorb_iff2 topspace_subtopology) + by (simp add: inf.absorb_iff2) lemma closedin_subtopology: "closedin (subtopology U V) S \ (\T. closedin U T \ S = T \ V)" unfolding closedin_def topspace_subtopology @@ -391,7 +391,7 @@ lemma closedin_imp_subset: "closedin (subtopology U S) T \ T \ S" -by (simp add: closedin_def topspace_subtopology) +by (simp add: closedin_def) lemma openin_open_subtopology: "openin X S \ openin (subtopology X S) T \ openin X T \ T \ S" @@ -436,7 +436,7 @@ by (force simp: topspace_def) lemma topspace_euclidean_subtopology[simp]: "topspace (top_of_set S) = S" - by (simp add: topspace_subtopology) + by (simp) lemma closed_closedin: "closed S \ closedin euclidean S" by (simp add: closed_def closedin_def Compl_eq_Diff_UNIV) @@ -623,7 +623,7 @@ lemma derived_set_of_subtopology: "(subtopology X U) derived_set_of S = U \ (X derived_set_of (U \ S))" - by (simp add: derived_set_of_def openin_subtopology topspace_subtopology) blast + by (simp add: derived_set_of_def openin_subtopology) blast lemma derived_set_of_subset_subtopology: "(subtopology X S) derived_set_of T \ S" @@ -666,7 +666,7 @@ lemma subtopology_eq_discrete_topology_eq: "subtopology X U = discrete_topology U \ U \ topspace X \ U \ X derived_set_of U = {}" using discrete_topology_unique_derived_set [of U "subtopology X U"] - by (auto simp: eq_commute topspace_subtopology derived_set_of_subtopology) + by (auto simp: eq_commute derived_set_of_subtopology) lemma subtopology_eq_discrete_topology: "S \ topspace X \ S \ X derived_set_of S = {} @@ -816,7 +816,7 @@ lemma closedin_derived_set: "closedin (subtopology X T) S \ S \ topspace X \ S \ T \ (\x. x \ X derived_set_of S \ x \ T \ x \ S)" - by (auto simp: closedin_contains_derived_set topspace_subtopology derived_set_of_subtopology Int_absorb1) + by (auto simp: closedin_contains_derived_set derived_set_of_subtopology Int_absorb1) lemma closedin_Int_closure_of: "closedin (subtopology X S) T \ S \ X closure_of T = T" @@ -1348,7 +1348,7 @@ with fin show "finite {U \ \. U \ (S \ V) \ {}}" using finite_subset by auto show "x \ S \ V" - using x \x \ V\ by (simp add: topspace_subtopology) + using x \x \ V\ by (simp) qed next show "\x A. \x \ A; A \ \\ \ x \ topspace (subtopology X S)" @@ -1672,13 +1672,13 @@ show ?lhs using R unfolding continuous_map - by (auto simp: topspace_subtopology openin_subtopology eq) + by (auto simp: openin_subtopology eq) qed lemma continuous_map_from_subtopology: "continuous_map X X' f \ continuous_map (subtopology X S) X' f" - by (auto simp: continuous_map topspace_subtopology openin_subtopology) + by (auto simp: continuous_map openin_subtopology) lemma continuous_map_into_fulltopology: "continuous_map X (subtopology X' T) f \ continuous_map X X' f" @@ -2134,17 +2134,17 @@ unfolding quotient_map_def proof (intro conjI allI impI) show "f ` topspace (subtopology X U) = topspace (subtopology Y V)" - using sub U fim by (auto simp: topspace_subtopology) + using sub U fim by (auto) next fix Y' :: "'b set" assume "Y' \ topspace (subtopology Y V)" then have "Y' \ topspace Y" "Y' \ V" - by (simp_all add: topspace_subtopology) + by (simp_all) then have eq: "{x \ topspace X. x \ U \ f x \ Y'} = {x \ topspace X. f x \ Y'}" using U by blast then show "openin (subtopology X U) {x \ topspace (subtopology X U). f x \ Y'} = openin (subtopology Y V) Y'" using U V Y \openin X U\ \Y' \ topspace Y\ \Y' \ V\ - by (simp add: topspace_subtopology openin_open_subtopology eq) (auto simp: openin_closedin_eq) + by (simp add: openin_open_subtopology eq) (auto simp: openin_closedin_eq) qed next assume V: "closedin Y V" @@ -2159,17 +2159,17 @@ unfolding quotient_map_closedin proof (intro conjI allI impI) show "f ` topspace (subtopology X U) = topspace (subtopology Y V)" - using sub U fim by (auto simp: topspace_subtopology) + using sub U fim by (auto) next fix Y' :: "'b set" assume "Y' \ topspace (subtopology Y V)" then have "Y' \ topspace Y" "Y' \ V" - by (simp_all add: topspace_subtopology) + by (simp_all) then have eq: "{x \ topspace X. x \ U \ f x \ Y'} = {x \ topspace X. f x \ Y'}" using U by blast then show "closedin (subtopology X U) {x \ topspace (subtopology X U). f x \ Y'} = closedin (subtopology Y V) Y'" using U V Y \closedin X U\ \Y' \ topspace Y\ \Y' \ V\ - by (simp add: topspace_subtopology closedin_closed_subtopology eq) (auto simp: closedin_def) + by (simp add: closedin_closed_subtopology eq) (auto simp: closedin_def) qed qed @@ -2264,7 +2264,7 @@ lemma separatedin_subtopology: "separatedin (subtopology X U) S T \ S \ U \ T \ U \ separatedin X S T" - apply (simp add: separatedin_def closure_of_subtopology topspace_subtopology) + apply (simp add: separatedin_def closure_of_subtopology) apply (safe; metis Int_absorb1 inf.assoc inf.orderE insert_disjoint(2) mk_disjoint_insert) done @@ -2715,13 +2715,13 @@ "\homeomorphic_maps X Y f g; f ` (topspace X \ S) = topspace Y \ T\ \ homeomorphic_maps (subtopology X S) (subtopology Y T) f g" unfolding homeomorphic_maps_def - by (force simp: continuous_map_from_subtopology topspace_subtopology continuous_map_in_subtopology) + by (force simp: continuous_map_from_subtopology continuous_map_in_subtopology) lemma homeomorphic_maps_subtopologies_alt: "\homeomorphic_maps X Y f g; f ` (topspace X \ S) \ T; g ` (topspace Y \ T) \ S\ \ homeomorphic_maps (subtopology X S) (subtopology Y T) f g" unfolding homeomorphic_maps_def - by (force simp: continuous_map_from_subtopology topspace_subtopology continuous_map_in_subtopology) + by (force simp: continuous_map_from_subtopology continuous_map_in_subtopology) lemma homeomorphic_map_subtopologies: "\homeomorphic_map X Y f; f ` (topspace X \ S) = topspace Y \ T\ @@ -2810,7 +2810,7 @@ lemma connectedin_subtopology: "connectedin (subtopology X S) T \ connectedin X T \ T \ S" - by (force simp: connectedin_def subtopology_subtopology topspace_subtopology inf_absorb2) + by (force simp: connectedin_def subtopology_subtopology inf_absorb2) lemma connected_space_eq: "connected_space X \ @@ -3256,7 +3256,7 @@ have eq: "(\U \ \. \Y. openin X Y \ U = Y \ S) \ \ \ (\Y. Y \ S) ` {y. openin X y}" for \ by auto show ?thesis - by (auto simp: compactin_def topspace_subtopology openin_subtopology eq imp_conjL all_subset_image ex_finite_subset_image) + by (auto simp: compactin_def openin_subtopology eq imp_conjL all_subset_image ex_finite_subset_image) qed lemma compactin_subspace: "compactin X S \ S \ topspace X \ compact_space (subtopology X S)" @@ -3267,7 +3267,7 @@ by (simp add: compactin_subspace) lemma compactin_subtopology: "compactin (subtopology X S) T \ compactin X T \ T \ S" -apply (simp add: compactin_subspace topspace_subtopology) +apply (simp add: compactin_subspace) by (metis inf.orderE inf_commute subtopology_subtopology) @@ -3361,7 +3361,7 @@ lemma compactin_subtopology_imp_compact: assumes "compactin (subtopology X S) K" shows "compactin X K" using assms -proof (clarsimp simp add: compactin_def topspace_subtopology) +proof (clarsimp simp add: compactin_def) fix \ define \ where "\ \ (\U. U \ S) ` \" assume "K \ topspace X" and "K \ S" and "\x\\. openin X x" and "K \ \\" @@ -3394,7 +3394,7 @@ lemma compact_imp_compactin_subtopology: assumes "compactin X K" "K \ S" shows "compactin (subtopology X S) K" using assms -proof (clarsimp simp add: compactin_def topspace_subtopology) +proof (clarsimp simp add: compactin_def) fix \ :: "'a set set" define \ where "\ \ {V. openin X V \ (\U \ \. U = V \ S)}" assume "K \ S" and "K \ topspace X" and "\U\\. openin (subtopology X S) U" and "K \ \\" @@ -3556,7 +3556,7 @@ lemma compactin_imp_Bolzano_Weierstrass: "\compactin X S; infinite T \ T \ S\ \ S \ X derived_set_of T \ {}" using compact_space_imp_Bolzano_Weierstrass [of "subtopology X S"] - by (simp add: compactin_subspace derived_set_of_subtopology inf_absorb2 topspace_subtopology) + by (simp add: compactin_subspace derived_set_of_subtopology inf_absorb2) lemma compact_closure_of_imp_Bolzano_Weierstrass: "\compactin X (X closure_of S); infinite T; T \ S; T \ topspace X\ \ X derived_set_of T \ {}" @@ -3739,7 +3739,7 @@ lemma section_imp_embedding_map: "section_map X Y f \ embedding_map X Y f" unfolding section_map_def embedding_map_def homeomorphic_map_maps retraction_maps_def homeomorphic_maps_def - by (force simp: continuous_map_in_subtopology continuous_map_from_subtopology topspace_subtopology) + by (force simp: continuous_map_in_subtopology continuous_map_from_subtopology) lemma retraction_imp_quotient_map: assumes "retraction_map X Y f" diff -r a25b6f79043f -r 575b3a818de5 src/HOL/Analysis/Abstract_Topology_2.thy --- a/src/HOL/Analysis/Abstract_Topology_2.thy Thu Nov 28 20:38:07 2019 +0100 +++ b/src/HOL/Analysis/Abstract_Topology_2.thy Thu Nov 28 23:06:22 2019 +0100 @@ -87,7 +87,7 @@ assume int: "x \ interior A" then obtain U where U: "open U" "x \ U" "U \ A" unfolding interior_def by auto hence "\y\U. indicator A y = (1::real)" unfolding indicator_def by auto - hence "continuous_on U (indicator A)" by (simp add: continuous_on_const indicator_eq_1_iff) + hence "continuous_on U (indicator A)" by (simp add: indicator_eq_1_iff) thus ?thesis using U continuous_on_eq_continuous_at by auto next assume ext: "x \ interior (-A)" @@ -388,7 +388,7 @@ and "a \ s \ f a = g a" shows "continuous_on s (\t. if t \ a then f(t) else g(t))" using assms -by (auto simp: continuous_on_id intro: continuous_on_cases_le [where h = id, simplified]) +by (auto intro: continuous_on_cases_le [where h = id, simplified]) subsection\<^marker>\tag unimportant\\Inverse function property for open/closed maps\ @@ -1249,7 +1249,7 @@ lemma path_connectedin_absolute [simp]: "path_connectedin (subtopology X S) S \ path_connectedin X S" - by (simp add: path_connectedin_def subtopology_subtopology topspace_subtopology) + by (simp add: path_connectedin_def subtopology_subtopology) lemma path_connectedin_subset_topspace: "path_connectedin X S \ S \ topspace X" @@ -1257,14 +1257,14 @@ lemma path_connectedin_subtopology: "path_connectedin (subtopology X S) T \ path_connectedin X T \ T \ S" - by (auto simp: path_connectedin_def subtopology_subtopology topspace_subtopology inf.absorb2) + by (auto simp: path_connectedin_def subtopology_subtopology inf.absorb2) lemma path_connectedin: "path_connectedin X S \ S \ topspace X \ (\x \ S. \y \ S. \g. pathin X g \ g ` {0..1} \ S \ g 0 = x \ g 1 = y)" unfolding path_connectedin_def path_connected_space_def pathin_def continuous_map_in_subtopology - by (intro conj_cong refl ball_cong) (simp_all add: inf.absorb_iff2 topspace_subtopology) + by (intro conj_cong refl ball_cong) (simp_all add: inf.absorb_iff2) lemma path_connectedin_topspace: "path_connectedin X (topspace X) \ path_connected_space X" diff -r a25b6f79043f -r 575b3a818de5 src/HOL/Analysis/Bounded_Continuous_Function.thy --- a/src/HOL/Analysis/Bounded_Continuous_Function.thy Thu Nov 28 20:38:07 2019 +0100 +++ b/src/HOL/Analysis/Bounded_Continuous_Function.thy Thu Nov 28 23:06:22 2019 +0100 @@ -33,7 +33,7 @@ by (blast intro: apply_bcontfun_cases assms ) lemma const_bcontfun: "(\x. b) \ bcontfun" - by (auto simp: bcontfun_def continuous_on_const image_def) + by (auto simp: bcontfun_def image_def) lift_definition const_bcontfun::"'b::metric_space \ ('a::topological_space \\<^sub>C 'b)" is "\c _. c" by (rule const_bcontfun) diff -r a25b6f79043f -r 575b3a818de5 src/HOL/Analysis/Bounded_Linear_Function.thy --- a/src/HOL/Analysis/Bounded_Linear_Function.thy Thu Nov 28 20:38:07 2019 +0100 +++ b/src/HOL/Analysis/Bounded_Linear_Function.thy Thu Nov 28 23:06:22 2019 +0100 @@ -548,7 +548,7 @@ fix e::real let ?d = "real_of_nat DIM('a) * real_of_nat DIM('b)" assume "e > 0" - hence "e / ?d > 0" by (simp add: DIM_positive) + hence "e / ?d > 0" by (simp) with l have "eventually (\n. \i\Basis. dist (f (r n) i) (l i) < e / ?d) sequentially" by simp moreover diff -r a25b6f79043f -r 575b3a818de5 src/HOL/Analysis/Brouwer_Fixpoint.thy --- a/src/HOL/Analysis/Brouwer_Fixpoint.thy Thu Nov 28 20:38:07 2019 +0100 +++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy Thu Nov 28 23:06:22 2019 +0100 @@ -717,7 +717,7 @@ then have "a = enum 0" using \a \ s\ na by (subst enum_0_bot) (auto simp: le_less intro!: less[of a _ n]) then have s_eq: "s - {a} = enum ` Suc ` {.. n}" - using s_eq by (simp add: atMost_Suc_eq_insert_0 insert_ident zero_notin_Suc_image in_enum_image subset_eq) + using s_eq by (simp add: atMost_Suc_eq_insert_0 insert_ident in_enum_image subset_eq) then have "enum 1 \ s - {a}" by auto then have "upd 0 = n" @@ -1212,7 +1212,7 @@ have "c = t.enum (Suc l)" unfolding c_eq .. also have "t.enum (Suc l) = b.enum (Suc i')" using u \l < k\ \k \ n\ \Suc i' < n\ - by (simp_all add: enum_Suc t.enum_Suc l b.enum_Suc \b.enum i' = enum i'\ swap_apply1) + by (simp_all add: enum_Suc t.enum_Suc l b.enum_Suc \b.enum i' = enum i'\) (simp add: Suc_i') also have "\ = b.enum i" using i by (simp add: i'_def) @@ -1576,7 +1576,7 @@ proof (rule ccontr) define n where "n = DIM('a)" have n: "1 \ n" "0 < n" "n \ 0" - unfolding n_def by (auto simp: Suc_le_eq DIM_positive) + unfolding n_def by (auto simp: Suc_le_eq) assume "\ ?thesis" then have *: "\ (\x\cbox 0 One. f x - x = 0)" by auto @@ -1633,7 +1633,7 @@ \(f(z) - z)\i\ < d / (real n)" proof - have d': "d / real n / 8 > 0" - using d(1) by (simp add: n_def DIM_positive) + using d(1) by (simp add: n_def) have *: "uniformly_continuous_on (cbox 0 One) f" by (rule compact_uniformly_continuous[OF assms(1) compact_cbox]) obtain e where e: @@ -1732,7 +1732,7 @@ { fix x :: "nat \ nat" and i assume "\i p" "i < n" "x i = p \ x i = 0" then have "(\i\Basis. (real (x (b' i)) / real p) *\<^sub>R i) \ (cbox 0 One::'a set)" using b'_Basis - by (auto simp: cbox_def inner_simps bij_betw_def zero_le_divide_iff divide_le_eq_1) } + by (auto simp: cbox_def bij_betw_def zero_le_divide_iff divide_le_eq_1) } note cube = this have q2: "\x. (\i p) \ (\i (label (\i\Basis. (real (x (b' i)) / real p) *\<^sub>R i) \ b) i = 0)" @@ -1855,7 +1855,7 @@ proof (rule interiorI) let ?I = "(\i\Basis. {x::'a. 0 < x \ i} \ {x. x \ i < 1})" show "open ?I" - by (intro open_INT finite_Basis ballI open_Int, auto intro: open_Collect_less simp: continuous_on_inner continuous_on_const continuous_on_id) + by (intro open_INT finite_Basis ballI open_Int, auto intro: open_Collect_less simp: continuous_on_inner) show "\Basis /\<^sub>R 2 \ ?I" by simp show "?I \ cbox 0 One" @@ -1963,7 +1963,7 @@ case False then show ?thesis unfolding contractible_def nullhomotopic_from_sphere_extension - using continuous_on_const less_eq_real_def by auto + using less_eq_real_def by auto qed corollary connected_sphere_eq: @@ -2028,9 +2028,7 @@ have "continuous_on (closure S \ closure(-S)) g" unfolding g_def apply (rule continuous_on_cases) - using fros fid frontier_closures - apply (auto simp: contf continuous_on_id) - done + using fros fid frontier_closures by (auto simp: contf) moreover have "closure S \ closure(- S) = UNIV" using closure_Un by fastforce ultimately have contg: "continuous_on UNIV g" by metis diff -r a25b6f79043f -r 575b3a818de5 src/HOL/Analysis/Cartesian_Euclidean_Space.thy --- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy Thu Nov 28 20:38:07 2019 +0100 +++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy Thu Nov 28 23:06:22 2019 +0100 @@ -127,7 +127,7 @@ lemma component_le_onorm: fixes f :: "real^'m \ real^'n" shows "linear f \ \matrix f $ i $ j\ \ onorm f" - by (metis linear_matrix_vector_mul_eq matrix_component_le_onorm matrix_vector_mul) + by (metis matrix_component_le_onorm matrix_vector_mul(2)) lemma onorm_le_matrix_component_sum: fixes A :: "real^'n^'m" @@ -223,7 +223,7 @@ unfolding continuous_on_def by (auto intro: tendsto_vec_lambda) lemma closed_positive_orthant: "closed {x::real^'n. \i. 0 \x$i}" - by (simp add: Collect_all_eq closed_INT closed_Collect_le continuous_on_const continuous_on_id continuous_on_component) + by (simp add: Collect_all_eq closed_INT closed_Collect_le continuous_on_component) lemma bounded_component_cart: "bounded s \ bounded ((\x. x $ i) ` s)" unfolding bounded_def @@ -243,7 +243,7 @@ proof - have "\d' \ d. ?th d'" by (rule compact_lemma_general[where unproj=vec_lambda]) - (auto intro!: f bounded_component_cart simp: vec_lambda_eta) + (auto intro!: f bounded_component_cart) then show "?th d" by simp qed @@ -372,12 +372,12 @@ lemma closed_interval_left_cart: fixes b :: "real^'n" shows "closed {x::real^'n. \i. x$i \ b$i}" - by (simp add: Collect_all_eq closed_INT closed_Collect_le continuous_on_const continuous_on_id continuous_on_component) + by (simp add: Collect_all_eq closed_INT closed_Collect_le continuous_on_component) lemma closed_interval_right_cart: fixes a::"real^'n" shows "closed {x::real^'n. \i. a$i \ x$i}" - by (simp add: Collect_all_eq closed_INT closed_Collect_le continuous_on_const continuous_on_id continuous_on_component) + by (simp add: Collect_all_eq closed_INT closed_Collect_le continuous_on_component) lemma is_interval_cart: "is_interval (s::(real^'n) set) \ @@ -430,7 +430,7 @@ proof - { fix i::'n have "closed {x::'a ^ 'n. P i \ x$i = 0}" - by (cases "P i") (simp_all add: closed_Collect_eq continuous_on_const continuous_on_id continuous_on_component) } + by (cases "P i") (simp_all add: closed_Collect_eq continuous_on_component) } thus ?thesis unfolding Collect_all_eq by (simp add: closed_INT) qed diff -r a25b6f79043f -r 575b3a818de5 src/HOL/Analysis/Cauchy_Integral_Theorem.thy --- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Thu Nov 28 20:38:07 2019 +0100 +++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Thu Nov 28 23:06:22 2019 +0100 @@ -406,10 +406,10 @@ by (simp add: C1_differentiable_on_eq differentiable_at_imp_differentiable_on) lemma C1_differentiable_on_ident [simp, derivative_intros]: "(\x. x) C1_differentiable_on S" - by (auto simp: C1_differentiable_on_eq continuous_on_const) + by (auto simp: C1_differentiable_on_eq) lemma C1_differentiable_on_const [simp, derivative_intros]: "(\z. a) C1_differentiable_on S" - by (auto simp: C1_differentiable_on_eq continuous_on_const) + by (auto simp: C1_differentiable_on_eq) lemma C1_differentiable_on_add [simp, derivative_intros]: "f C1_differentiable_on S \ g C1_differentiable_on S \ (\x. f x + g x) C1_differentiable_on S" @@ -498,7 +498,7 @@ proof (cases "m = 0") case True then show ?thesis - unfolding o_def by (auto simp: piecewise_C1_differentiable_on_def continuous_on_const) + unfolding o_def by (auto simp: piecewise_C1_differentiable_on_def) next case False have *: "\x. finite (S \ {y. m * y + c = x})" @@ -919,7 +919,7 @@ unfolding reversepath_def apply (rule C1_differentiable_compose [of "\x::real. 1-x" _ g, unfolded o_def]) using S - by (force simp: finite_vimageI inj_on_def C1_differentiable_on_eq continuous_on_const elim!: continuous_on_subset)+ + by (force simp: finite_vimageI inj_on_def C1_differentiable_on_eq elim!: continuous_on_subset)+ ultimately show ?thesis using assms by (auto simp: valid_path_def piecewise_C1_differentiable_on_def path_def [symmetric]) qed @@ -1342,7 +1342,7 @@ lemma has_contour_integral_linepath: shows "(f has_contour_integral i) (linepath a b) \ ((\x. f(linepath a b x) * (b - a)) has_integral i) {0..1}" - by (simp add: has_contour_integral vector_derivative_linepath_at) + by (simp add: has_contour_integral) lemma linepath_in_path: shows "x \ {0..1} \ linepath a b x \ closed_segment a b" @@ -1432,7 +1432,7 @@ using has_contour_integral_subpath_refl contour_integrable_on_def by blast lemma contour_integral_subpath_refl [simp]: "contour_integral (subpath u u g) f = 0" - by (simp add: has_contour_integral_subpath_refl contour_integral_unique) + by (simp add: contour_integral_unique) lemma has_contour_integral_subpath: assumes f: "f contour_integrable_on g" and g: "valid_path g" @@ -1544,14 +1544,14 @@ apply simp apply (elim disjE) apply (auto simp: * contour_integral_reversepath contour_integrable_subpath - valid_path_reversepath valid_path_subpath algebra_simps) + valid_path_subpath algebra_simps) done next case False then show ?thesis - apply (auto simp: contour_integral_subpath_refl) + apply (auto) using assms - by (metis eq_neg_iff_add_eq_0 contour_integrable_subpath contour_integral_reversepath reversepath_subpath valid_path_subpath) + by (metis eq_neg_iff_add_eq_0 contour_integral_reversepath reversepath_subpath valid_path_subpath) qed lemma contour_integral_integral: @@ -1699,10 +1699,10 @@ done lemma contour_integrable_on_const [iff]: "(\x. c) contour_integrable_on (linepath a b)" - by (simp add: continuous_on_const contour_integrable_continuous_linepath) + by (simp add: contour_integrable_continuous_linepath) lemma contour_integrable_on_id [iff]: "(\x. x) contour_integrable_on (linepath a b)" - by (simp add: continuous_on_id contour_integrable_continuous_linepath) + by (simp add: contour_integrable_continuous_linepath) subsection\<^marker>\tag unimportant\ \Arithmetical combining theorems\ @@ -4546,7 +4546,7 @@ moreover have "\Re (winding_number \ z')\ < 1/2" apply (rule winding_number_lt_half [OF \ *]) using azb \d>0\ pag - apply (auto simp: add_strict_increasing anz field_split_simps algebra_simps dest!: subsetD) + apply (auto simp: add_strict_increasing anz field_split_simps dest!: subsetD) done ultimately have False by simp @@ -5719,7 +5719,7 @@ using \x \ path_image \\ ball_divide_subset_numeral d by fastforce then show ?thesis using \d > 0\ apply (simp add: ff_def norm_mult norm_divide norm_power dist_norm canc) - using dpow_le apply (simp add: algebra_simps field_split_simps mult_less_0_iff) + using dpow_le apply (simp add: field_split_simps) done qed have ub: "u \ ball w (d/2)" @@ -6187,7 +6187,7 @@ apply (rule deriv_cmult) apply (rule analytic_on_imp_differentiable_at [OF _ Suc.prems]) apply (rule analytic_on_compose_gen [where g="(deriv ^^ n) f" and T=T, unfolded o_def]) - apply (simp add: analytic_on_linear) + apply (simp) apply (simp add: analytic_on_open f holomorphic_higher_deriv T) apply (blast intro: fg) done @@ -6195,7 +6195,7 @@ apply (subst complex_derivative_chain [where g = "(deriv ^^ n) f" and f = "(*) u", unfolded o_def]) apply (rule derivative_intros) using Suc.prems field_differentiable_def f fg has_field_derivative_higher_deriv T apply blast - apply (simp add: deriv_linear) + apply (simp) done finally show ?case by simp @@ -6540,7 +6540,7 @@ assumes "f holomorphic_on UNIV" and "(f \ l) at_infinity" shows "f z = l" using Liouville_weak_0 [of "\z. f z - l"] - by (simp add: assms holomorphic_on_const holomorphic_on_diff LIM_zero) + by (simp add: assms holomorphic_on_diff LIM_zero) proposition Liouville_weak_inverse: assumes "f holomorphic_on UNIV" and unbounded: "\B. eventually (\x. norm (f x) \ B) at_infinity" @@ -6548,11 +6548,11 @@ proof - { assume f: "\z. f z \ 0" have 1: "(\x. 1 / f x) holomorphic_on UNIV" - by (simp add: holomorphic_on_divide holomorphic_on_const assms f) + by (simp add: holomorphic_on_divide assms f) have 2: "((\x. 1 / f x) \ 0) at_infinity" apply (rule tendstoI [OF eventually_mono]) apply (rule_tac B="2/e" in unbounded) - apply (simp add: dist_norm norm_divide field_split_simps mult_ac) + apply (simp add: dist_norm norm_divide field_split_simps) done have False using Liouville_weak_0 [OF 1 2] f by simp @@ -7473,7 +7473,7 @@ apply (rule mult_mono) using that D interior_subset apply blast using \L>0\ \e>0\ \D>0\ DL2 - apply (auto simp: norm_divide field_split_simps algebra_simps) + apply (auto simp: norm_divide field_split_simps) done finally show ?thesis . qed diff -r a25b6f79043f -r 575b3a818de5 src/HOL/Analysis/Change_Of_Vars.thy --- a/src/HOL/Analysis/Change_Of_Vars.thy Thu Nov 28 20:38:07 2019 +0100 +++ b/src/HOL/Analysis/Change_Of_Vars.thy Thu Nov 28 23:06:22 2019 +0100 @@ -1433,7 +1433,7 @@ with \r > 0\ \d > 0\ \e > 0\ show ?thesis apply (simp add: content_cbox_if_cart mem_box_cart) apply (auto simp: prod_nonneg) - apply (simp add: abs if_distrib prod.delta_remove prod_constant field_simps power_diff split: if_split_asm) + apply (simp add: abs if_distrib prod.delta_remove field_simps power_diff split: if_split_asm) done qed also have "\ \ e/2 * measure lebesgue (cball ?x' (min d r))" diff -r a25b6f79043f -r 575b3a818de5 src/HOL/Analysis/Connected.thy --- a/src/HOL/Analysis/Connected.thy Thu Nov 28 20:38:07 2019 +0100 +++ b/src/HOL/Analysis/Connected.thy Thu Nov 28 23:06:22 2019 +0100 @@ -726,7 +726,7 @@ apply (subst tus [symmetric]) apply (rule continuous_on_cases_local) using clt clu tue - apply (auto simp: tus continuous_on_const) + apply (auto simp: tus) done have fi: "finite ((\x. if x \ t then 0 else 1) ` S)" by (rule finite_subset [of _ "{0,1}"]) auto diff -r a25b6f79043f -r 575b3a818de5 src/HOL/Analysis/Continuous_Extension.thy --- a/src/HOL/Analysis/Continuous_Extension.thy Thu Nov 28 20:38:07 2019 +0100 +++ b/src/HOL/Analysis/Continuous_Extension.thy Thu Nov 28 23:06:22 2019 +0100 @@ -91,7 +91,7 @@ done qed moreover have "\U \ \; x \ S\ \ 0 \ F U x" for U x - using nonneg [of x] by (simp add: F_def field_split_simps setdist_pos_le) + using nonneg [of x] by (simp add: F_def field_split_simps) ultimately show "\U. U \ \ \ continuous_on S (F U) \ (\x\S. 0 \ F U x)" by metis next @@ -194,7 +194,7 @@ show ?thesis proof (cases "T = U") case True with \S = {}\ \a \ b\ show ?thesis - by (rule_tac f = "\x. b" in that) (auto simp: continuous_on_const) + by (rule_tac f = "\x. b" in that) (auto) next case False with UT closedin_subset obtain c where c: "c \ U" "c \ T" @@ -220,7 +220,7 @@ case True show ?thesis proof (cases "S = U") case True with \T = {}\ \a \ b\ show ?thesis - by (rule_tac f = "\x. a" in that) (auto simp: continuous_on_const) + by (rule_tac f = "\x. a" in that) (auto) next case False with US closedin_subset obtain c where c: "c \ U" "c \ S" @@ -260,7 +260,7 @@ "\x. x \ T \ f x = b" proof (cases "a = b") case True then show ?thesis - by (rule_tac f = "\x. b" in that) (auto simp: continuous_on_const) + by (rule_tac f = "\x. b" in that) (auto) next case False then show ?thesis diff -r a25b6f79043f -r 575b3a818de5 src/HOL/Analysis/Convex_Euclidean_Space.thy --- a/src/HOL/Analysis/Convex_Euclidean_Space.thy Thu Nov 28 20:38:07 2019 +0100 +++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy Thu Nov 28 23:06:22 2019 +0100 @@ -2233,7 +2233,7 @@ unfolding 2 by (clarsimp simp: dist_norm) (metis inner_commute inner_diff_right norm_bound_Basis_le) have e': "e = (\(i::'a)\Basis. d)" - by (simp add: d_def DIM_positive) + by (simp add: d_def) show "convex hull c \ cball x e" unfolding 2 apply clarsimp diff -r a25b6f79043f -r 575b3a818de5 src/HOL/Analysis/Extended_Real_Limits.thy --- a/src/HOL/Analysis/Extended_Real_Limits.thy Thu Nov 28 20:38:07 2019 +0100 +++ b/src/HOL/Analysis/Extended_Real_Limits.thy Thu Nov 28 23:06:22 2019 +0100 @@ -939,7 +939,7 @@ apply (rule iffD1[OF continuous_on_cong, of "{..0}" _ "\x. -x"]) using less_eq_ereal_def apply (auto simp add: continuous_uminus_ereal) apply (rule iffD1[OF continuous_on_cong, of "{0..}" _ "\x. x"]) - apply (auto simp add: continuous_on_id) + apply (auto) done moreover have "(UNIV::ereal set) = {..0} \ {(0::ereal)..}" by auto ultimately show ?thesis by auto diff -r a25b6f79043f -r 575b3a818de5 src/HOL/Analysis/Function_Topology.thy --- a/src/HOL/Analysis/Function_Topology.thy Thu Nov 28 20:38:07 2019 +0100 +++ b/src/HOL/Analysis/Function_Topology.thy Thu Nov 28 23:06:22 2019 +0100 @@ -285,7 +285,7 @@ unfolding topology_eq apply clarify apply (simp add: openin_product_topology flip: openin_relative_to) - apply (simp add: arbitrary_union_of_relative_to topspace_product_topology topspace_subtopology flip: PiE_Int) + apply (simp add: arbitrary_union_of_relative_to flip: PiE_Int) done qed @@ -1960,8 +1960,7 @@ lemma connectedin_PiE: "connectedin (product_topology X I) (PiE I S) \ PiE I S = {} \ (\i \ I. connectedin (X i) (S i))" - by (fastforce simp add: connectedin_def subtopology_PiE connected_space_product_topology subset_PiE PiE_eq_empty_iff - topspace_subtopology_subset) + by (fastforce simp add: connectedin_def subtopology_PiE connected_space_product_topology subset_PiE PiE_eq_empty_iff) lemma path_connected_space_product_topology: "path_connected_space(product_topology X I) \ diff -r a25b6f79043f -r 575b3a818de5 src/HOL/Analysis/Further_Topology.thy --- a/src/HOL/Analysis/Further_Topology.thy Thu Nov 28 20:38:07 2019 +0100 +++ b/src/HOL/Analysis/Further_Topology.thy Thu Nov 28 23:06:22 2019 +0100 @@ -1536,7 +1536,7 @@ then obtain y where "y \ rel_frontier U" by auto with \S = {}\ show ?thesis - by (rule_tac K="{}" and g="\x. y" in that) (auto simp: continuous_on_const) + by (rule_tac K="{}" and g="\x. y" in that) (auto) qed next case False @@ -1662,7 +1662,7 @@ proof (cases "r = 0") case True with fim show ?thesis - by (rule_tac K="{}" and g = "\x. a" in that) (auto simp: continuous_on_const) + by (rule_tac K="{}" and g = "\x. a" in that) (auto) next case False with assms have "0 < r" by auto @@ -2836,7 +2836,7 @@ proof - have "homotopic_loops S (f \ exp \ (\t. of_real(2 * pi * t) * \)) (g \ exp \ (\t. of_real(2 * pi * t) * \))" apply (rule S [unfolded simply_connected_homotopic_loops, rule_format]) - apply (simp add: homotopic_circlemaps_imp_homotopic_loops homotopic_with_refl contf fim contg gim) + apply (simp add: homotopic_circlemaps_imp_homotopic_loops contf fim contg gim) done then show ?thesis apply (rule homotopic_with_eq [OF homotopic_loops_imp_homotopic_circlemaps]) @@ -2854,8 +2854,7 @@ shows "\a. homotopic_with_canon (\h. True) (sphere 0 1) S h (\x. a)" apply (rule_tac x="h 1" in exI) apply (rule hom) - using assms - by (auto simp: continuous_on_const) + using assms by (auto) lemma simply_connected_eq_homotopic_circlemaps2b: fixes S :: "'a::real_normed_vector set" @@ -2869,7 +2868,7 @@ assume "a \ S" "b \ S" then show "homotopic_loops S (linepath a a) (linepath b b)" using homotopic_circlemaps_imp_homotopic_loops [OF assms [of "\x. a" "\x. b"]] - by (auto simp: o_def continuous_on_const linepath_def) + by (auto simp: o_def linepath_def) qed lemma simply_connected_eq_homotopic_circlemaps3: @@ -3876,7 +3875,7 @@ apply (rule continuous_intros) using homotopic_with_imp_continuous [OF L] apply blast apply (rule continuous_on_subset [of "sphere 0 1", OF continuous_on_inverse]) - apply (auto simp: continuous_on_id) + apply (auto) done have "homotopic_with_canon (\x. True) S (sphere 0 1) (\x. f x / g x) (\x. 1)" using homotopic_with_sphere_times [OF L cont] @@ -4473,7 +4472,7 @@ apply (auto simp: retract_of_def retraction_def) apply (erule (1) Borsukian_retraction_gen) apply (meson retraction retraction_def) - apply (auto simp: continuous_on_id) + apply (auto) done lemma homeomorphic_Borsukian: "\Borsukian S; S homeomorphic T\ \ Borsukian T" @@ -5595,8 +5594,7 @@ show ?rhs proof (cases "S = {}") case True - with a show ?thesis - using continuous_on_const by force + with a show ?thesis by force next case False have anr: "ANR (-{0::complex})" diff -r a25b6f79043f -r 575b3a818de5 src/HOL/Analysis/Henstock_Kurzweil_Integration.thy --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Thu Nov 28 20:38:07 2019 +0100 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Thu Nov 28 23:06:22 2019 +0100 @@ -7263,7 +7263,7 @@ \ e * content (cbox w z) / content ?CBOX/2 * content (cbox u v)" apply (rule integrable_bound [OF _ _ normint_wz]) using cbp \0 < e/content ?CBOX\ - apply (auto simp: field_split_simps content_pos_le integrable_diff int_integrable integrable_const) + apply (auto simp: field_split_simps integrable_diff int_integrable integrable_const) done also have "... \ e * content (cbox (u,w) (v,z)) / content ?CBOX/2" by (simp add: content_Pair field_split_simps) @@ -7430,7 +7430,7 @@ inverse (real (Suc k)) powr (a + 1) / (a + 1)) {inverse (real (Suc k))..c}" using True a by (intro fundamental_theorem_of_calculus) (auto intro!: derivative_eq_intros continuous_on_powr' continuous_on_const - continuous_on_id simp: has_field_derivative_iff_has_vector_derivative [symmetric]) + simp: has_field_derivative_iff_has_vector_derivative [symmetric]) with True show ?thesis unfolding f_def F_def by (subst has_integral_restrict) simp_all next case False diff -r a25b6f79043f -r 575b3a818de5 src/HOL/Analysis/Homeomorphism.thy --- a/src/HOL/Analysis/Homeomorphism.thy Thu Nov 28 20:38:07 2019 +0100 +++ b/src/HOL/Analysis/Homeomorphism.thy Thu Nov 28 23:06:22 2019 +0100 @@ -177,7 +177,7 @@ by (simp add: proj_def) (metis surf xy homeomorphism_def) qed have co01: "compact ?SPHER" - by (simp add: closed_affine_hull compact_Int_closed) + by (simp add: compact_Int_closed) show "?SMINUS homeomorphic ?SPHER" apply (subst homeomorphic_sym) apply (rule homeomorphic_compact [OF co01 cont_nosp [unfolded o_def] no_sp_im inj_spher]) @@ -293,7 +293,7 @@ qed qed have co01: "compact ?CBALL" - by (simp add: closed_affine_hull compact_Int_closed) + by (simp add: compact_Int_closed) show "S homeomorphic ?CBALL" apply (subst homeomorphic_sym) apply (rule homeomorphic_compact [OF co01 cont_nosp2 [unfolded o_def] im_cball inj_cball]) @@ -1446,9 +1446,9 @@ obtain t where "t \ tk" and t: "{real n / real N .. (1 + real n) / real N} \ K t" proof (rule bexE [OF \]) show "{real n / real N .. (1 + real n) / real N} \ {0..1}" - using Suc.prems by (auto simp: field_split_simps algebra_simps) + using Suc.prems by (auto simp: field_split_simps) show diameter_less: "diameter {real n / real N .. (1 + real n) / real N} < \" - using \0 < \\ N by (auto simp: field_split_simps algebra_simps) + using \0 < \\ N by (auto simp: field_split_simps) qed blast have t01: "t \ {0..1}" using \t \ tk\ \tk \ {0..1}\ by blast @@ -1458,7 +1458,7 @@ and homuu: "\U. U \ \ \ \q. homeomorphism U (UU (X t)) p q" using inUS [OF t01] UU by meson have n_div_N_in: "real n / real N \ {real n / real N .. (1 + real n) / real N}" - using N by (auto simp: field_split_simps algebra_simps) + using N by (auto simp: field_split_simps) with t have nN_in_kkt: "real n / real N \ K t" by blast have "k (real n / real N, y) \ C \ p -` UU (X t)" @@ -1850,7 +1850,7 @@ and hpk: "\z. z \ {0..1} \ {0..1} \ h z = p (k z)" apply (rule covering_space_lift_homotopy_alt [OF cov conth him, of "\x. h2 0"]) using h1h2 ph1 ph2 apply (force simp: heq0 pathstart_def pathfinish_def) - using path_image_def pih2 continuous_on_const by fastforce+ + using path_image_def pih2 by fastforce+ have contg1: "continuous_on {0..1} g1" and contg2: "continuous_on {0..1} g2" using \path g1\ \path g2\ path_def by blast+ have g1im: "g1 ` {0..1} \ S" and g2im: "g2 ` {0..1} \ S" @@ -1892,7 +1892,7 @@ by (intro continuous_intros continuous_on_compose2 [OF contk]) auto show "\x. x \ {0..1} \ g1 1 = p ((k \ Pair x) 1)" using heq1 hpk by auto - qed (use contk kim g1im h1im that in \auto simp: ph1 continuous_on_const\) + qed (use contk kim g1im h1im that in \auto simp: ph1\) qed (use contk kim in auto) qed @@ -1993,7 +1993,7 @@ have "q' t = (h \ (*\<^sub>R) 2) t" if "0 \ t" "t \ 1/2" for t proof (rule covering_space_lift_unique [OF cov, of q' 0 "h \ (*\<^sub>R) 2" "{0..1/2}" "f \ g \ (*\<^sub>R) 2" t]) show "q' 0 = (h \ (*\<^sub>R) 2) 0" - by (metis \pathstart q' = pathstart q\ comp_def g h pastq pathstart_def pth_4(2)) + by (metis \pathstart q' = pathstart q\ comp_def h pastq pathstart_def pth_4(2)) show "continuous_on {0..1/2} (f \ g \ (*\<^sub>R) 2)" apply (intro continuous_intros continuous_on_compose continuous_on_path [OF \path g\] continuous_on_subset [OF contf]) using g(2) path_image_def by fastforce+ diff -r a25b6f79043f -r 575b3a818de5 src/HOL/Analysis/Homotopy.thy --- a/src/HOL/Analysis/Homotopy.thy Thu Nov 28 20:38:07 2019 +0100 +++ b/src/HOL/Analysis/Homotopy.thy Thu Nov 28 23:06:22 2019 +0100 @@ -217,7 +217,7 @@ (k2 \ (\x. (2 *\<^sub>R fst x -1, snd x)))" apply (rule fst continuous_map_compose [OF _ contk2] continuous_intros continuous_map_into_subtopology | simp)+ apply (rule continuous_intros fst continuous_map_from_subtopology | simp)+ - apply (force simp: topspace_subtopology prod_topology_subtopology) + apply (force simp: prod_topology_subtopology) using continuous_map_snd continuous_map_from_subtopology by blast show "(k1 \ (\x. (2 *\<^sub>R fst x, snd x))) y = (k2 \ (\x. (2 *\<^sub>R fst x -1, snd x))) y" if "y \ topspace ?X01" and "fst y = 1/2" for y @@ -481,7 +481,7 @@ have pab: "path_component T a b" if "a \ T" "b \ T" for a b proof - have "homotopic_with_canon (\x. True) S T (\x. a) (\x. b)" - by (simp add: LHS continuous_on_const image_subset_iff that) + by (simp add: LHS image_subset_iff that) then show ?thesis using False homotopic_constant_maps [of "top_of_set S" "top_of_set T" a b] by auto qed @@ -572,7 +572,7 @@ "\path p; path_image p \ s; \t. t \ {0..1} \ p t = q t\ \ homotopic_paths s p q" apply (simp add: homotopic_paths_def) apply (rule homotopic_with_eq) - apply (auto simp: path_def homotopic_with_refl pathstart_def pathfinish_def path_image_def elim: continuous_on_eq) + apply (auto simp: path_def pathstart_def pathfinish_def path_image_def elim: continuous_on_eq) done proposition homotopic_paths_reparametrize: @@ -1414,7 +1414,7 @@ obtains c where "homotopic_with_canon (\h. True) S T f (\x. c)" apply (rule nullhomotopic_through_contractible [OF f, of id T]) using assms -apply (auto simp: continuous_on_id) +apply (auto) done lemma nullhomotopic_from_contractible: @@ -3583,7 +3583,7 @@ by (rule homotopic_with_trans [OF f]) next show "retraction_maps X (subtopology X S) r id" - by (simp add: r req retraction_maps_def topspace_subtopology) + by (simp add: r req retraction_maps_def) qed qed (use True in \auto simp: retraction_maps_def topspace_subtopology_subset continuous_map_in_subtopology\) ultimately show ?thesis by simp @@ -3824,8 +3824,6 @@ qed - - lemma contractible_space_product_topology: "contractible_space(product_topology X I) \ topspace (product_topology X I) = {} \ (\i \ I. contractible_space(X i))" @@ -3846,7 +3844,7 @@ using cs unfolding contractible_space_def by metis have "homotopic_with (\x. True) (product_topology X I) (product_topology X I) id (\x. restrict f I)" - by (rule homotopic_with_eq [OF homotopic_with_product_topology [OF f]]) (auto simp: topspace_product_topology) + by (rule homotopic_with_eq [OF homotopic_with_product_topology [OF f]]) (auto) then show ?thesis by (auto simp: contractible_space_def) qed @@ -4101,7 +4099,7 @@ apply (rule_tac x="\x. b" in exI) apply (rule_tac x="\x. a" in exI) apply (intro assms conjI continuous_on_id' homotopic_into_contractible) - apply (auto simp: o_def continuous_on_const) + apply (auto simp: o_def) done qed @@ -4578,7 +4576,7 @@ proof (cases "S = {}") case True then show ?thesis - by (simp add: path_connected_empty) + by (simp) next case False show ?thesis @@ -4714,7 +4712,7 @@ using \r > 0\\0 \ v\ by (simp add: dist_norm n) moreover have "x - v *\<^sub>R (u - a) \ T" - by (simp add: f_def \affine T\ \u \ T\ \x \ T\ assms mem_affine_3_minus2) + by (simp add: f_def \u \ T\ \x \ T\ assms mem_affine_3_minus2) ultimately show "x - v *\<^sub>R (u - a) \ cball a r \ T" by blast qed @@ -4782,7 +4780,7 @@ apply (simp add: ff_def) apply (rule continuous_on_cases) using homeomorphism_cont1 [OF hom] - apply (auto simp: affine_closed \affine T\ continuous_on_id fid) + apply (auto simp: affine_closed \affine T\ fid) done then show "continuous_on S ff" apply (rule continuous_on_subset) @@ -4791,7 +4789,7 @@ apply (simp add: gg_def) apply (rule continuous_on_cases) using homeomorphism_cont2 [OF hom] - apply (auto simp: affine_closed \affine T\ continuous_on_id gid) + apply (auto simp: affine_closed \affine T\ gid) done then show "continuous_on S gg" apply (rule continuous_on_subset) @@ -5039,7 +5037,7 @@ using assms by auto have "f ` {a..b} = {c..d}" unfolding f_def image_affinity_atLeastAtMost - using assms sum_sqs_eq by (auto simp: field_split_simps algebra_simps) + using assms sum_sqs_eq by (auto simp: field_split_simps) then show "f ` cbox a b = cbox c d" by auto show "inj_on f (cbox a b)" @@ -5051,7 +5049,7 @@ show "f a = c" by (simp add: f_def) show "f b = d" - using assms sum_sqs_eq [of a b] by (auto simp: f_def field_split_simps algebra_simps) + using assms sum_sqs_eq [of a b] by (auto simp: f_def field_split_simps) qed qed @@ -5078,7 +5076,7 @@ show "continuous_on (cbox a c) f" apply (simp add: f_def) apply (rule continuous_on_cases_le [OF continuous_on_subset [OF cf1] continuous_on_subset [OF cf2]]) - using le eq apply (force simp: continuous_on_id)+ + using le eq apply (force)+ done have "f ` cbox a b = f1 ` cbox a b" "f ` cbox b c = f2 ` cbox b c" unfolding f_def using eq by force+ @@ -5390,7 +5388,7 @@ using \U \ {}\ \K \ S\ openin_imp_subset [OF opeU] by blast show ?thesis apply (rule that [of id id]) - using \K \ U\ by (auto simp: continuous_on_id intro: homeomorphismI) + using \K \ U\ by (auto intro: homeomorphismI) next assume "aff_dim S = 1" then have "affine hull S homeomorphic (UNIV :: real set)" diff -r a25b6f79043f -r 575b3a818de5 src/HOL/Analysis/Lebesgue_Measure.thy --- a/src/HOL/Analysis/Lebesgue_Measure.thy Thu Nov 28 20:38:07 2019 +0100 +++ b/src/HOL/Analysis/Lebesgue_Measure.thy Thu Nov 28 23:06:22 2019 +0100 @@ -363,7 +363,7 @@ qed show "((\a. ennreal (F b - F a)) \ F b - F a) (at_left a)" by (rule continuous_on_tendsto_compose[where g="\x. x" and s=UNIV]) - (auto simp: continuous_on_ennreal continuous_on_diff cont_F continuous_on_const) + (auto simp: continuous_on_ennreal continuous_on_diff cont_F) qed (rule trivial_limit_at_left_real) lemma\<^marker>\tag important\ sigma_finite_interval_measure: @@ -745,7 +745,7 @@ have "((\f. f 1) -` {l..u} \ space (Pi\<^sub>M {1} (\b. interval_measure (\x. x)))) = {1::real} \\<^sub>E {l..u}" by (auto simp: space_PiM) then show ?thesis - by (simp add: lborel_def emeasure_distr emeasure_PiM emeasure_interval_measure_Icc continuous_on_id) + by (simp add: lborel_def emeasure_distr emeasure_PiM emeasure_interval_measure_Icc) qed lemma emeasure_lborel_Icc_eq: "emeasure lborel {l .. u} = ennreal (if l \ u then u - l else 0)" @@ -821,7 +821,7 @@ lemma emeasure_lborel_singleton[simp]: "emeasure lborel {x} = 0" using emeasure_lborel_cbox[of x x] nonempty_Basis - by (auto simp del: emeasure_lborel_cbox nonempty_Basis simp add: prod_constant) + by (auto simp del: emeasure_lborel_cbox nonempty_Basis) lemma fmeasurable_cbox [iff]: "cbox a b \ fmeasurable lborel" and fmeasurable_box [iff]: "box a b \ fmeasurable lborel" @@ -872,14 +872,14 @@ have "... \ (2::real) ^ card ?Ba * real (Suc n) ^ card ?Ba" apply (rule mult_left_mono) apply (metis DIM_positive One_nat_def less_eq_Suc_le less_imp_le of_nat_le_iff of_nat_power self_le_power zero_less_Suc) - apply (simp add: DIM_positive) + apply (simp) done finally have "real n \ (2::real) ^ card ?Ba * real (Suc n) ^ card ?Ba" . } note [intro!] = this show ?thesis unfolding UN_box_eq_UNIV[symmetric] apply (subst SUP_emeasure_incseq[symmetric]) - apply (auto simp: incseq_def subset_box inner_add_left prod_constant + apply (auto simp: incseq_def subset_box inner_add_left simp del: Sup_eq_top_iff SUP_eq_top_iff intro!: ennreal_SUP_eq_top) done @@ -1001,7 +1001,7 @@ using c by (auto simp: box_def T_def field_simps inner_simps divide_less_eq) with le c show "emeasure ?D (box l u) = (\b\?B. (u - l) \ b)" by (auto simp: emeasure_density emeasure_distr nn_integral_multc emeasure_lborel_box_eq inner_simps - field_simps field_split_simps ennreal_mult'[symmetric] prod_nonneg prod.distrib[symmetric] + field_split_simps ennreal_mult'[symmetric] prod_nonneg prod.distrib[symmetric] intro!: prod.cong) qed simp @@ -1153,7 +1153,7 @@ apply (subst lebesgue_affine_euclidean[of "\_. m" \]) apply (simp_all add: emeasure_density trans_eq_T nn_integral_cmult emeasure_distr del: space_completion emeasure_completion) - apply (simp add: vimage_comp s_comp_s prod_constant) + apply (simp add: vimage_comp s_comp_s) done next assume "S \ sets lebesgue" diff -r a25b6f79043f -r 575b3a818de5 src/HOL/Analysis/Locally.thy --- a/src/HOL/Analysis/Locally.thy Thu Nov 28 20:38:07 2019 +0100 +++ b/src/HOL/Analysis/Locally.thy Thu Nov 28 23:06:22 2019 +0100 @@ -155,7 +155,7 @@ lemma locally_path_connected_space_open_path_components: "locally_path_connected_space X \ (\U c. openin X U \ c \ path_components_of(subtopology X U) \ openin X c)" - apply (auto simp: locally_path_connected_space_eq_open_path_component_of path_components_of_def topspace_subtopology) + apply (auto simp: locally_path_connected_space_eq_open_path_component_of path_components_of_def) by (metis imageI inf.absorb_iff2 openin_closedin_eq) lemma openin_path_component_of_locally_path_connected_space: @@ -275,7 +275,7 @@ by (metis (no_types, lifting) \f x \ C\ x disjnt_iff image_eqI) qed then show "?T \ {x \ topspace X. f x \ C}" - by (force simp: path_component_of_equiv topspace_subtopology) + by (force simp: path_component_of_equiv) qed qed then show "openin Y C" diff -r a25b6f79043f -r 575b3a818de5 src/HOL/Analysis/Path_Connected.thy --- a/src/HOL/Analysis/Path_Connected.thy Thu Nov 28 20:38:07 2019 +0100 +++ b/src/HOL/Analysis/Path_Connected.thy Thu Nov 28 23:06:22 2019 +0100 @@ -457,7 +457,7 @@ qed lemma path_join_imp: "\path g1; path g2; pathfinish g1 = pathstart g2\ \ path(g1 +++ g2)" - by (simp add: path_join) + by (simp) lemma simple_path_join_loop: assumes "arc g1" "arc g2" @@ -547,7 +547,7 @@ } note * = this show ?thesis apply (simp add: arc_def inj_on_def) - apply (clarsimp simp add: arc_imp_path assms path_join) + apply (clarsimp simp add: arc_imp_path assms) apply (simp add: joinpaths_def split: if_split_asm) apply (force dest: inj_onD [OF injg1]) apply (metis *) @@ -831,7 +831,7 @@ lemma sum_le_prod1: fixes a::real shows "\a \ 1; b \ 1\ \ a + b \ 1 + a * b" -by (metis add.commute affine_ineq less_eq_real_def mult.right_neutral) +by (metis add.commute affine_ineq mult.right_neutral) lemma simple_path_subpath_eq: "simple_path(subpath u v g) \ @@ -1545,7 +1545,7 @@ then obtain g where g: "path g" "path_image g \ S" "pathstart g = x1" "pathfinish g = x2" using assms[unfolded path_connected_def,rule_format,of x1 x2] by auto have *: "connected {0..1::real}" - by (auto intro!: convex_connected convex_real_interval) + by (auto intro!: convex_connected) have "{0..1} \ {x \ {0..1}. g x \ e1} \ {x \ {0..1}. g x \ e2}" using as(3) g(2)[unfolded path_defs] by blast moreover have "{x \ {0..1}. g x \ e1} \ {x \ {0..1}. g x \ e2} = {}" @@ -1691,7 +1691,7 @@ apply clarify apply (rule_tac x="\x. a" in exI) apply (simp add: image_constant_conv) - apply (simp add: path_def continuous_on_const) + apply (simp add: path_def) done lemma path_connected_Un: @@ -1796,7 +1796,7 @@ case True show ?thesis apply (rule subset_antisym) apply (simp add: path_component_subset) - by (simp add: True path_component_maximal path_component_refl path_connected_path_component) + by (simp add: True path_component_maximal path_component_refl) next case False then show ?thesis by (metis False empty_iff path_component_eq_empty) @@ -2183,7 +2183,7 @@ obtain a where "\S. S \ \ \ a \ S" using assms by blast then have "\x. x \ topspace (subtopology X (\\)) \ path_component_of (subtopology X (\\)) a x" - apply (simp add: topspace_subtopology) + apply (simp) by (meson Union_upper \ path_component_of path_connectedin_subtopology) then show ?thesis using \ unfolding path_connectedin_def @@ -2429,11 +2429,11 @@ proof (cases r "0::real" rule: linorder_cases) case less then show ?thesis - by (simp add: path_connected_empty) + by (simp) next case equal then show ?thesis - by (simp add: path_connected_singleton) + by (simp) next case greater then have eq: "(sphere (0::'a) r) = (\x. (r / norm x) *\<^sub>R x) ` (- {0::'a})" @@ -3303,7 +3303,7 @@ qed lemma inside_empty [simp]: "inside {} = ({} :: 'a :: {real_normed_vector, perfect_space} set)" - by (simp add: inside_def connected_component_UNIV) + by (simp add: inside_def) lemma outside_empty [simp]: "outside {} = (UNIV :: 'a :: {real_normed_vector, perfect_space} set)" using inside_empty inside_Un_outside by blast @@ -3346,7 +3346,7 @@ by (simp add: scaleR_add_left [symmetric] field_split_simps) then have False using convexD_alt [OF s \a \ s\ ins, of "1/(u*C + 1)"] \C>0\ \z \ s\ Cpos u - by (simp add: * field_split_simps algebra_simps) + by (simp add: * field_split_simps) } note contra = this have "connected_component (- s) z (z + C *\<^sub>R (z-a))" apply (rule connected_componentI [OF connected_segment [of z "z + C *\<^sub>R (z-a)"]]) diff -r a25b6f79043f -r 575b3a818de5 src/HOL/Analysis/Retracts.thy --- a/src/HOL/Analysis/Retracts.thy Thu Nov 28 20:38:07 2019 +0100 +++ b/src/HOL/Analysis/Retracts.thy Thu Nov 28 23:06:22 2019 +0100 @@ -604,7 +604,7 @@ show "continuous_on W (\x. if x \ W - V then a else h (j x, g x))" apply (subst Weq) apply (rule continuous_on_cases_local) - apply (simp_all add: Weq [symmetric] WWV continuous_on_const *) + apply (simp_all add: Weq [symmetric] WWV *) using WV' closedin_diff apply fastforce apply (auto simp: j0 j1) done @@ -1408,7 +1408,7 @@ proof (intro exI conjI) show "continuous_on (S \ T) (\x. if x \ S then x else r x)" apply (rule continuous_on_cases_local [OF clS clT]) - using r by (auto simp: continuous_on_id) + using r by (auto) qed (use r in auto) also have "\ retract_of U" by (rule Un) @@ -2136,7 +2136,7 @@ proof have "continuous_on (T \ (S - T)) ?g" apply (rule continuous_on_cases_local) - using Seq clo ope by (auto simp: contf continuous_on_const intro: continuous_on_cases_local) + using Seq clo ope by (auto simp: contf intro: continuous_on_cases_local) with Seq show "continuous_on S ?g" by metis show "?g ` S \ U" diff -r a25b6f79043f -r 575b3a818de5 src/HOL/Analysis/Starlike.thy --- a/src/HOL/Analysis/Starlike.thy Thu Nov 28 20:38:07 2019 +0100 +++ b/src/HOL/Analysis/Starlike.thy Thu Nov 28 23:06:22 2019 +0100 @@ -644,7 +644,7 @@ fix i :: 'a assume i: "i \ Basis" show "0 < ?a \ i" - unfolding **[OF i] by (auto simp add: Suc_le_eq DIM_positive) + unfolding **[OF i] by (auto simp add: Suc_le_eq) next have "sum ((\) ?a) ?D = sum (\i. inverse (2 * real DIM('a))) ?D" apply (rule sum.cong) @@ -3676,7 +3676,7 @@ case False { assume "card s = Suc (card Basis)" then have cs: "Suc 0 < card s" - by (simp add: DIM_positive) + by (simp) with subset_singletonD have "\y \ s. y \ x" by (cases "s \ {x}") fastforce+ } note [dest!] = this @@ -4242,9 +4242,9 @@ show "{x. 0 < f x} \ {x. f x < 0} = {}" by auto show "open {x. 0 < f x}" - by (simp add: open_Collect_less contf continuous_on_const) + by (simp add: open_Collect_less contf) show "open {x. f x < 0}" - by (simp add: open_Collect_less contf continuous_on_const) + by (simp add: open_Collect_less contf) show "S \ {x. 0 < f x}" apply (clarsimp simp add: f_def setdist_sing_in_set) using assms diff -r a25b6f79043f -r 575b3a818de5 src/HOL/Analysis/Topology_Euclidean_Space.thy --- a/src/HOL/Analysis/Topology_Euclidean_Space.thy Thu Nov 28 20:38:07 2019 +0100 +++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Thu Nov 28 23:06:22 2019 +0100 @@ -347,7 +347,7 @@ then have "span (cball 0 e) = (UNIV :: 'n::euclidean_space set)" by auto then show ?thesis - using dim_span[of "cball (0 :: 'n::euclidean_space) e"] by (auto simp: dim_UNIV) + using dim_span[of "cball (0 :: 'n::euclidean_space) e"] by (auto) qed @@ -424,7 +424,7 @@ proof - define e' where "e' = e / (2 * sqrt (real (DIM ('a))))" then have e: "e' > 0" - using assms by (auto simp: DIM_positive) + using assms by (auto) have "\i. \y. y \ \ \ y < x \ i \ x \ i - y < e'" (is "\i. ?th i") proof fix i @@ -884,7 +884,7 @@ by (simp add: dual_order.antisym euclidean_eqI) } moreover have "c \ cbox (m *\<^sub>R a + c) (m *\<^sub>R b + c)" - unfolding True by (auto simp: cbox_sing) + unfolding True by (auto) ultimately show ?thesis using True by (auto simp: cbox_def) next case False @@ -1171,16 +1171,16 @@ subsection\<^marker>\tag unimportant\ \Openness of halfspaces.\ lemma open_halfspace_lt: "open {x. inner a x < b}" - by (simp add: open_Collect_less continuous_on_inner continuous_on_const continuous_on_id) + by (simp add: open_Collect_less continuous_on_inner) lemma open_halfspace_gt: "open {x. inner a x > b}" - by (simp add: open_Collect_less continuous_on_inner continuous_on_const continuous_on_id) + by (simp add: open_Collect_less continuous_on_inner) lemma open_halfspace_component_lt: "open {x::'a::euclidean_space. x\i < a}" - by (simp add: open_Collect_less continuous_on_inner continuous_on_const continuous_on_id) + by (simp add: open_Collect_less continuous_on_inner) lemma open_halfspace_component_gt: "open {x::'a::euclidean_space. x\i > a}" - by (simp add: open_Collect_less continuous_on_inner continuous_on_const continuous_on_id) + by (simp add: open_Collect_less continuous_on_inner) lemma eucl_less_eq_halfspaces: fixes a :: "'a::euclidean_space" @@ -1199,29 +1199,29 @@ unfolding continuous_at by (intro tendsto_intros) lemma closed_halfspace_le: "closed {x. inner a x \ b}" - by (simp add: closed_Collect_le continuous_on_inner continuous_on_const continuous_on_id) + by (simp add: closed_Collect_le continuous_on_inner) lemma closed_halfspace_ge: "closed {x. inner a x \ b}" - by (simp add: closed_Collect_le continuous_on_inner continuous_on_const continuous_on_id) + by (simp add: closed_Collect_le continuous_on_inner) lemma closed_hyperplane: "closed {x. inner a x = b}" - by (simp add: closed_Collect_eq continuous_on_inner continuous_on_const continuous_on_id) + by (simp add: closed_Collect_eq continuous_on_inner) lemma closed_halfspace_component_le: "closed {x::'a::euclidean_space. x\i \ a}" - by (simp add: closed_Collect_le continuous_on_inner continuous_on_const continuous_on_id) + by (simp add: closed_Collect_le continuous_on_inner) lemma closed_halfspace_component_ge: "closed {x::'a::euclidean_space. x\i \ a}" - by (simp add: closed_Collect_le continuous_on_inner continuous_on_const continuous_on_id) + by (simp add: closed_Collect_le continuous_on_inner) lemma closed_interval_left: fixes b :: "'a::euclidean_space" shows "closed {x::'a. \i\Basis. x\i \ b\i}" - by (simp add: Collect_ball_eq closed_INT closed_Collect_le continuous_on_inner continuous_on_const continuous_on_id) + by (simp add: Collect_ball_eq closed_INT closed_Collect_le continuous_on_inner) lemma closed_interval_right: fixes a :: "'a::euclidean_space" shows "closed {x::'a. \i\Basis. a\i \ x\i}" - by (simp add: Collect_ball_eq closed_INT closed_Collect_le continuous_on_inner continuous_on_const continuous_on_id) + by (simp add: Collect_ball_eq closed_INT closed_Collect_le continuous_on_inner) lemma interior_halfspace_le [simp]: assumes "a \ 0" @@ -1646,7 +1646,7 @@ { fix e::real assume "e > 0" - hence "e / real_of_nat DIM('a) > 0" by (simp add: DIM_positive) + hence "e / real_of_nat DIM('a) > 0" by (simp) with l have "eventually (\n. \i\Basis. dist (f (r n) \ i) (l \ i) < e / (real_of_nat DIM('a))) sequentially" by simp moreover @@ -1948,7 +1948,7 @@ fix e :: real assume "e > 0" moreover have "clamp a b x \ cbox a b" - by (simp add: clamp_in_interval le) + by (simp add: le) moreover note f_cont[simplified continuous_on_iff] ultimately obtain d where d: "0 < d" @@ -2192,7 +2192,7 @@ qed then show "\y. dist y (f x) < \ \ y \ f ` A" using \e > 0\ \B > 0\ - by (auto simp: \_def field_split_simps mult_less_0_iff) + by (auto simp: \_def field_split_simps) qed qed @@ -2349,8 +2349,7 @@ proof - let ?D = "{i\Basis. P i}" have "closed (\i\?D. {x::'a. x\i = 0})" - by (simp add: closed_INT closed_Collect_eq continuous_on_inner - continuous_on_const continuous_on_id) + by (simp add: closed_INT closed_Collect_eq continuous_on_inner) also have "(\i\?D. {x::'a. x\i = 0}) = ?A" by auto finally show "closed ?A" . @@ -2392,7 +2391,7 @@ lemma closed_span [iff]: "closed (span s)" for s :: "'a::euclidean_space set" - by (simp add: closed_subspace subspace_span) + by (simp add: closed_subspace) lemma dim_closure [simp]: "dim (closure s) = dim s" (is "?dc = ?d") for s :: "'a::euclidean_space set" diff -r a25b6f79043f -r 575b3a818de5 src/HOL/Analysis/Weierstrass_Theorems.thy --- a/src/HOL/Analysis/Weierstrass_Theorems.thy Thu Nov 28 20:38:07 2019 +0100 +++ b/src/HOL/Analysis/Weierstrass_Theorems.thy Thu Nov 28 23:06:22 2019 +0100 @@ -526,7 +526,7 @@ using Bernoulli_inequality [of "-e / card subA" "card subA"] e cardp by (auto simp: field_simps) also have "... = (\w \ subA. 1 - e / card subA)" - by (simp add: prod_constant subA(2)) + by (simp add: subA(2)) also have "... < pff x" apply (simp add: pff_def) apply (rule prod_mono_strict [where f = "\x. 1 - e / card subA", simplified]) @@ -1117,7 +1117,7 @@ have "\p. real_polynomial_function p \ (\x \ S. \f x \ b - p x\ < e / DIM('b))" apply (rule exE [OF Stone_Weierstrass_real_polynomial_function [OF S _, of "\x. f x \ b" "e / card Basis"]]) using e f - apply (auto simp: Euclidean_Space.DIM_positive intro: continuous_intros) + apply (auto intro: continuous_intros) done } then obtain pf where pf: @@ -1140,7 +1140,7 @@ apply (rule DIM_positive) done also have "... = e" - using DIM_positive by (simp add: field_simps) + by (simp add: field_simps) finally have "norm (\b\Basis. (f x \ b) *\<^sub>R b - pf b x *\<^sub>R b) < e" . } ultimately