--- 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="\<lambda>f. restrict f {..<n}" in exI)
apply (rule_tac x="\<lambda>f i. if i < n then f i else 0" in exI)
- apply (simp add: Euclidean_space_def topspace_subtopology continuous_map_in_subtopology)
+ apply (simp add: Euclidean_space_def continuous_map_in_subtopology)
apply (intro conjI continuous_map_from_subtopology)
apply (force simp: continuous_map_componentwise cm intro: continuous_map_product_projection)+
done
@@ -247,7 +247,7 @@
define p:: "nat \<Rightarrow> real" where "p \<equiv> \<lambda>i. if i = k then 1 else 0"
have "p \<in> topspace(nsphere n)"
using assms
- by (simp add: nsphere topspace_subtopology p_def power2_eq_square if_distrib [where f = "\<lambda>x. x * _"] cong: if_cong)
+ by (simp add: nsphere p_def power2_eq_square if_distrib [where f = "\<lambda>x. x * _"] cong: if_cong)
let ?g = "\<lambda>x i. x i / sqrt(\<Sum>j\<le>n. x j ^ 2)"
let ?h = "\<lambda>(t,q) i. (1 - t) * q i + t * p i"
let ?Y = "subtopology (Euclidean_space (Suc n)) {x. 0 \<le> x k \<and> (\<exists>i\<le>n. x i \<noteq> 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 \<le> 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 = "\<lambda>x. _ * x"] cong: if_cong)
apply (intro continuous_map_prod_snd continuous_intros continuous_map_from_subtopology)
@@ -286,7 +286,7 @@
moreover have "(?g \<circ> ?h) (0, x) = x"
if "x \<in> topspace (subtopology (nsphere n) {x. 0 \<le> x k})" for x
using that
- by (simp add: assms topspace_subtopology nsphere)
+ by (simp add: assms nsphere)
moreover
have "(?g \<circ> ?h) (1, x) = p"
if "x \<in> topspace (subtopology (nsphere n) {x. 0 \<le> x k})" for x
--- 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 "\<forall>\<^sub>F b in F. f b \<in> topspace X \<inter> 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 \<inter> 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]:
--- 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 \<subseteq> topspace X \<Longrightarrow> 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 \<longleftrightarrow> (\<exists>T. closedin U T \<and> S = T \<inter> V)"
unfolding closedin_def topspace_subtopology
@@ -391,7 +391,7 @@
lemma closedin_imp_subset:
"closedin (subtopology U S) T \<Longrightarrow> T \<subseteq> S"
-by (simp add: closedin_def topspace_subtopology)
+by (simp add: closedin_def)
lemma openin_open_subtopology:
"openin X S \<Longrightarrow> openin (subtopology X S) T \<longleftrightarrow> openin X T \<and> T \<subseteq> 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 \<longleftrightarrow> 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 \<inter> (X derived_set_of (U \<inter> 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 \<subseteq> S"
@@ -666,7 +666,7 @@
lemma subtopology_eq_discrete_topology_eq:
"subtopology X U = discrete_topology U \<longleftrightarrow> U \<subseteq> topspace X \<and> U \<inter> 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 \<subseteq> topspace X \<and> S \<inter> X derived_set_of S = {}
@@ -816,7 +816,7 @@
lemma closedin_derived_set:
"closedin (subtopology X T) S \<longleftrightarrow>
S \<subseteq> topspace X \<and> S \<subseteq> T \<and> (\<forall>x. x \<in> X derived_set_of S \<and> x \<in> T \<longrightarrow> x \<in> 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 \<longleftrightarrow> S \<inter> X closure_of T = T"
@@ -1348,7 +1348,7 @@
with fin show "finite {U \<in> \<A>. U \<inter> (S \<inter> V) \<noteq> {}}"
using finite_subset by auto
show "x \<in> S \<inter> V"
- using x \<open>x \<in> V\<close> by (simp add: topspace_subtopology)
+ using x \<open>x \<in> V\<close> by (simp)
qed
next
show "\<And>x A. \<lbrakk>x \<in> A; A \<in> \<A>\<rbrakk> \<Longrightarrow> x \<in> 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 \<Longrightarrow> 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 \<Longrightarrow> 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' \<subseteq> topspace (subtopology Y V)"
then have "Y' \<subseteq> topspace Y" "Y' \<subseteq> V"
- by (simp_all add: topspace_subtopology)
+ by (simp_all)
then have eq: "{x \<in> topspace X. x \<in> U \<and> f x \<in> Y'} = {x \<in> topspace X. f x \<in> Y'}"
using U by blast
then show "openin (subtopology X U) {x \<in> topspace (subtopology X U). f x \<in> Y'} = openin (subtopology Y V) Y'"
using U V Y \<open>openin X U\<close> \<open>Y' \<subseteq> topspace Y\<close> \<open>Y' \<subseteq> V\<close>
- 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' \<subseteq> topspace (subtopology Y V)"
then have "Y' \<subseteq> topspace Y" "Y' \<subseteq> V"
- by (simp_all add: topspace_subtopology)
+ by (simp_all)
then have eq: "{x \<in> topspace X. x \<in> U \<and> f x \<in> Y'} = {x \<in> topspace X. f x \<in> Y'}"
using U by blast
then show "closedin (subtopology X U) {x \<in> topspace (subtopology X U). f x \<in> Y'} = closedin (subtopology Y V) Y'"
using U V Y \<open>closedin X U\<close> \<open>Y' \<subseteq> topspace Y\<close> \<open>Y' \<subseteq> V\<close>
- 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 \<longleftrightarrow> S \<subseteq> U \<and> T \<subseteq> U \<and> 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 @@
"\<lbrakk>homeomorphic_maps X Y f g; f ` (topspace X \<inter> S) = topspace Y \<inter> T\<rbrakk>
\<Longrightarrow> 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:
"\<lbrakk>homeomorphic_maps X Y f g; f ` (topspace X \<inter> S) \<subseteq> T; g ` (topspace Y \<inter> T) \<subseteq> S\<rbrakk>
\<Longrightarrow> 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:
"\<lbrakk>homeomorphic_map X Y f; f ` (topspace X \<inter> S) = topspace Y \<inter> T\<rbrakk>
@@ -2810,7 +2810,7 @@
lemma connectedin_subtopology:
"connectedin (subtopology X S) T \<longleftrightarrow> connectedin X T \<and> T \<subseteq> 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 \<longleftrightarrow>
@@ -3256,7 +3256,7 @@
have eq: "(\<forall>U \<in> \<U>. \<exists>Y. openin X Y \<and> U = Y \<inter> S) \<longleftrightarrow> \<U> \<subseteq> (\<lambda>Y. Y \<inter> S) ` {y. openin X y}" for \<U>
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 \<longleftrightarrow> S \<subseteq> topspace X \<and> compact_space (subtopology X S)"
@@ -3267,7 +3267,7 @@
by (simp add: compactin_subspace)
lemma compactin_subtopology: "compactin (subtopology X S) T \<longleftrightarrow> compactin X T \<and> T \<subseteq> 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 \<U>
define \<V> where "\<V> \<equiv> (\<lambda>U. U \<inter> S) ` \<U>"
assume "K \<subseteq> topspace X" and "K \<subseteq> S" and "\<forall>x\<in>\<U>. openin X x" and "K \<subseteq> \<Union>\<U>"
@@ -3394,7 +3394,7 @@
lemma compact_imp_compactin_subtopology:
assumes "compactin X K" "K \<subseteq> S" shows "compactin (subtopology X S) K"
using assms
-proof (clarsimp simp add: compactin_def topspace_subtopology)
+proof (clarsimp simp add: compactin_def)
fix \<U> :: "'a set set"
define \<V> where "\<V> \<equiv> {V. openin X V \<and> (\<exists>U \<in> \<U>. U = V \<inter> S)}"
assume "K \<subseteq> S" and "K \<subseteq> topspace X" and "\<forall>U\<in>\<U>. openin (subtopology X S) U" and "K \<subseteq> \<Union>\<U>"
@@ -3556,7 +3556,7 @@
lemma compactin_imp_Bolzano_Weierstrass:
"\<lbrakk>compactin X S; infinite T \<and> T \<subseteq> S\<rbrakk> \<Longrightarrow> S \<inter> X derived_set_of T \<noteq> {}"
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:
"\<lbrakk>compactin X (X closure_of S); infinite T; T \<subseteq> S; T \<subseteq> topspace X\<rbrakk> \<Longrightarrow> X derived_set_of T \<noteq> {}"
@@ -3739,7 +3739,7 @@
lemma section_imp_embedding_map:
"section_map X Y f \<Longrightarrow> 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"
--- 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 \<in> interior A"
then obtain U where U: "open U" "x \<in> U" "U \<subseteq> A" unfolding interior_def by auto
hence "\<forall>y\<in>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 \<in> interior (-A)"
@@ -388,7 +388,7 @@
and "a \<in> s \<Longrightarrow> f a = g a"
shows "continuous_on s (\<lambda>t. if t \<le> 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>\<open>tag unimportant\<close>\<open>Inverse function property for open/closed maps\<close>
@@ -1249,7 +1249,7 @@
lemma path_connectedin_absolute [simp]:
"path_connectedin (subtopology X S) S \<longleftrightarrow> 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 \<Longrightarrow> S \<subseteq> topspace X"
@@ -1257,14 +1257,14 @@
lemma path_connectedin_subtopology:
"path_connectedin (subtopology X S) T \<longleftrightarrow> path_connectedin X T \<and> T \<subseteq> 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 \<longleftrightarrow>
S \<subseteq> topspace X \<and>
(\<forall>x \<in> S. \<forall>y \<in> S. \<exists>g. pathin X g \<and> g ` {0..1} \<subseteq> S \<and> g 0 = x \<and> 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) \<longleftrightarrow> path_connected_space X"
--- 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: "(\<lambda>x. b) \<in> 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 \<Rightarrow> ('a::topological_space \<Rightarrow>\<^sub>C 'b)" is "\<lambda>c _. c"
by (rule const_bcontfun)
--- 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 (\<lambda>n. \<forall>i\<in>Basis. dist (f (r n) i) (l i) < e / ?d) sequentially"
by simp
moreover
--- 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 \<open>a \<in> s\<close> 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 \<in> 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 \<open>l < k\<close> \<open>k \<le> n\<close> \<open>Suc i' < n\<close>
- by (simp_all add: enum_Suc t.enum_Suc l b.enum_Suc \<open>b.enum i' = enum i'\<close> swap_apply1)
+ by (simp_all add: enum_Suc t.enum_Suc l b.enum_Suc \<open>b.enum i' = enum i'\<close>)
(simp add: Suc_i')
also have "\<dots> = 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 \<le> n" "0 < n" "n \<noteq> 0"
- unfolding n_def by (auto simp: Suc_le_eq DIM_positive)
+ unfolding n_def by (auto simp: Suc_le_eq)
assume "\<not> ?thesis"
then have *: "\<not> (\<exists>x\<in>cbox 0 One. f x - x = 0)"
by auto
@@ -1633,7 +1633,7 @@
\<bar>(f(z) - z)\<bullet>i\<bar> < 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 \<Rightarrow> nat" and i assume "\<forall>i<n. x i \<le> p" "i < n" "x i = p \<or> x i = 0"
then have "(\<Sum>i\<in>Basis. (real (x (b' i)) / real p) *\<^sub>R i) \<in> (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: "\<forall>x. (\<forall>i<n. x i \<le> p) \<longrightarrow> (\<forall>i<n. x i = 0 \<longrightarrow>
(label (\<Sum>i\<in>Basis. (real (x (b' i)) / real p) *\<^sub>R i) \<circ> b) i = 0)"
@@ -1855,7 +1855,7 @@
proof (rule interiorI)
let ?I = "(\<Inter>i\<in>Basis. {x::'a. 0 < x \<bullet> i} \<inter> {x. x \<bullet> 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 "\<Sum>Basis /\<^sub>R 2 \<in> ?I"
by simp
show "?I \<subseteq> 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 \<union> 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 \<union> closure(- S) = UNIV"
using closure_Un by fastforce
ultimately have contg: "continuous_on UNIV g" by metis
--- 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 \<Rightarrow> real^'n"
shows "linear f \<Longrightarrow> \<bar>matrix f $ i $ j\<bar> \<le> 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. \<forall>i. 0 \<le>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 \<Longrightarrow> bounded ((\<lambda>x. x $ i) ` s)"
unfolding bounded_def
@@ -243,7 +243,7 @@
proof -
have "\<forall>d' \<subseteq> 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. \<forall>i. x$i \<le> 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. \<forall>i. a$i \<le> 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) \<longleftrightarrow>
@@ -430,7 +430,7 @@
proof -
{ fix i::'n
have "closed {x::'a ^ 'n. P i \<longrightarrow> 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
--- 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]: "(\<lambda>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]: "(\<lambda>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 \<Longrightarrow> g C1_differentiable_on S \<Longrightarrow> (\<lambda>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 *: "\<And>x. finite (S \<inter> {y. m * y + c = x})"
@@ -919,7 +919,7 @@
unfolding reversepath_def
apply (rule C1_differentiable_compose [of "\<lambda>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) \<longleftrightarrow>
((\<lambda>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 \<in> {0..1} \<Longrightarrow> linepath a b x \<in> 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]: "(\<lambda>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]: "(\<lambda>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>\<open>tag unimportant\<close> \<open>Arithmetical combining theorems\<close>
@@ -4546,7 +4546,7 @@
moreover have "\<bar>Re (winding_number \<gamma> z')\<bar> < 1/2"
apply (rule winding_number_lt_half [OF \<gamma> *])
using azb \<open>d>0\<close> 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 \<open>x \<in> path_image \<gamma>\<close> ball_divide_subset_numeral d by fastforce
then show ?thesis
using \<open>d > 0\<close> 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 \<in> 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 \<longlongrightarrow> l) at_infinity"
shows "f z = l"
using Liouville_weak_0 [of "\<lambda>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: "\<And>B. eventually (\<lambda>x. norm (f x) \<ge> B) at_infinity"
@@ -6548,11 +6548,11 @@
proof -
{ assume f: "\<And>z. f z \<noteq> 0"
have 1: "(\<lambda>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: "((\<lambda>x. 1 / f x) \<longlongrightarrow> 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 \<open>L>0\<close> \<open>e>0\<close> \<open>D>0\<close> DL2
- apply (auto simp: norm_divide field_split_simps algebra_simps)
+ apply (auto simp: norm_divide field_split_simps)
done
finally show ?thesis .
qed
--- 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 \<open>r > 0\<close> \<open>d > 0\<close> \<open>e > 0\<close> 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 "\<dots> \<le> e/2 * measure lebesgue (cball ?x' (min d r))"
--- 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 ((\<lambda>x. if x \<in> t then 0 else 1) ` S)"
by (rule finite_subset [of _ "{0,1}"]) auto
--- 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 "\<lbrakk>U \<in> \<C>; x \<in> S\<rbrakk> \<Longrightarrow> 0 \<le> 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 "\<And>U. U \<in> \<C> \<Longrightarrow> continuous_on S (F U) \<and> (\<forall>x\<in>S. 0 \<le> F U x)"
by metis
next
@@ -194,7 +194,7 @@
show ?thesis
proof (cases "T = U")
case True with \<open>S = {}\<close> \<open>a \<noteq> b\<close> show ?thesis
- by (rule_tac f = "\<lambda>x. b" in that) (auto simp: continuous_on_const)
+ by (rule_tac f = "\<lambda>x. b" in that) (auto)
next
case False
with UT closedin_subset obtain c where c: "c \<in> U" "c \<notin> T"
@@ -220,7 +220,7 @@
case True show ?thesis
proof (cases "S = U")
case True with \<open>T = {}\<close> \<open>a \<noteq> b\<close> show ?thesis
- by (rule_tac f = "\<lambda>x. a" in that) (auto simp: continuous_on_const)
+ by (rule_tac f = "\<lambda>x. a" in that) (auto)
next
case False
with US closedin_subset obtain c where c: "c \<in> U" "c \<notin> S"
@@ -260,7 +260,7 @@
"\<And>x. x \<in> T \<Longrightarrow> f x = b"
proof (cases "a = b")
case True then show ?thesis
- by (rule_tac f = "\<lambda>x. b" in that) (auto simp: continuous_on_const)
+ by (rule_tac f = "\<lambda>x. b" in that) (auto)
next
case False
then show ?thesis
--- 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 = (\<Sum>(i::'a)\<in>Basis. d)"
- by (simp add: d_def DIM_positive)
+ by (simp add: d_def)
show "convex hull c \<subseteq> cball x e"
unfolding 2
apply clarsimp
--- 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}" _ "\<lambda>x. -x"])
using less_eq_ereal_def apply (auto simp add: continuous_uminus_ereal)
apply (rule iffD1[OF continuous_on_cong, of "{0..}" _ "\<lambda>x. x"])
- apply (auto simp add: continuous_on_id)
+ apply (auto)
done
moreover have "(UNIV::ereal set) = {..0} \<union> {(0::ereal)..}" by auto
ultimately show ?thesis by auto
--- 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) \<longleftrightarrow>
PiE I S = {} \<or> (\<forall>i \<in> 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) \<longleftrightarrow>
--- 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 \<in> rel_frontier U"
by auto
with \<open>S = {}\<close> show ?thesis
- by (rule_tac K="{}" and g="\<lambda>x. y" in that) (auto simp: continuous_on_const)
+ by (rule_tac K="{}" and g="\<lambda>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 = "\<lambda>x. a" in that) (auto simp: continuous_on_const)
+ by (rule_tac K="{}" and g = "\<lambda>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 \<circ> exp \<circ> (\<lambda>t. of_real(2 * pi * t) * \<i>)) (g \<circ> exp \<circ> (\<lambda>t. of_real(2 * pi * t) * \<i>))"
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 "\<exists>a. homotopic_with_canon (\<lambda>h. True) (sphere 0 1) S h (\<lambda>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 \<in> S" "b \<in> S"
then show "homotopic_loops S (linepath a a) (linepath b b)"
using homotopic_circlemaps_imp_homotopic_loops [OF assms [of "\<lambda>x. a" "\<lambda>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 (\<lambda>x. True) S (sphere 0 1) (\<lambda>x. f x / g x) (\<lambda>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: "\<lbrakk>Borsukian S; S homeomorphic T\<rbrakk> \<Longrightarrow> 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})"
--- 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 @@
\<le> e * content (cbox w z) / content ?CBOX/2 * content (cbox u v)"
apply (rule integrable_bound [OF _ _ normint_wz])
using cbp \<open>0 < e/content ?CBOX\<close>
- 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 "... \<le> 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
--- 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 \<in> tk" and t: "{real n / real N .. (1 + real n) / real N} \<subseteq> K t"
proof (rule bexE [OF \<delta>])
show "{real n / real N .. (1 + real n) / real N} \<subseteq> {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} < \<delta>"
- using \<open>0 < \<delta>\<close> N by (auto simp: field_split_simps algebra_simps)
+ using \<open>0 < \<delta>\<close> N by (auto simp: field_split_simps)
qed blast
have t01: "t \<in> {0..1}"
using \<open>t \<in> tk\<close> \<open>tk \<subseteq> {0..1}\<close> by blast
@@ -1458,7 +1458,7 @@
and homuu: "\<And>U. U \<in> \<V> \<Longrightarrow> \<exists>q. homeomorphism U (UU (X t)) p q"
using inUS [OF t01] UU by meson
have n_div_N_in: "real n / real N \<in> {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 \<in> K t"
by blast
have "k (real n / real N, y) \<in> C \<inter> p -` UU (X t)"
@@ -1850,7 +1850,7 @@
and hpk: "\<And>z. z \<in> {0..1} \<times> {0..1} \<Longrightarrow> h z = p (k z)"
apply (rule covering_space_lift_homotopy_alt [OF cov conth him, of "\<lambda>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 \<open>path g1\<close> \<open>path g2\<close> path_def by blast+
have g1im: "g1 ` {0..1} \<subseteq> S" and g2im: "g2 ` {0..1} \<subseteq> S"
@@ -1892,7 +1892,7 @@
by (intro continuous_intros continuous_on_compose2 [OF contk]) auto
show "\<And>x. x \<in> {0..1} \<Longrightarrow> g1 1 = p ((k \<circ> Pair x) 1)"
using heq1 hpk by auto
- qed (use contk kim g1im h1im that in \<open>auto simp: ph1 continuous_on_const\<close>)
+ qed (use contk kim g1im h1im that in \<open>auto simp: ph1\<close>)
qed (use contk kim in auto)
qed
@@ -1993,7 +1993,7 @@
have "q' t = (h \<circ> (*\<^sub>R) 2) t" if "0 \<le> t" "t \<le> 1/2" for t
proof (rule covering_space_lift_unique [OF cov, of q' 0 "h \<circ> (*\<^sub>R) 2" "{0..1/2}" "f \<circ> g \<circ> (*\<^sub>R) 2" t])
show "q' 0 = (h \<circ> (*\<^sub>R) 2) 0"
- by (metis \<open>pathstart q' = pathstart q\<close> comp_def g h pastq pathstart_def pth_4(2))
+ by (metis \<open>pathstart q' = pathstart q\<close> comp_def h pastq pathstart_def pth_4(2))
show "continuous_on {0..1/2} (f \<circ> g \<circ> (*\<^sub>R) 2)"
apply (intro continuous_intros continuous_on_compose continuous_on_path [OF \<open>path g\<close>] continuous_on_subset [OF contf])
using g(2) path_image_def by fastforce+
--- 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 \<circ> (\<lambda>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 \<circ> (\<lambda>x. (2 *\<^sub>R fst x, snd x))) y = (k2 \<circ> (\<lambda>x. (2 *\<^sub>R fst x -1, snd x))) y"
if "y \<in> topspace ?X01" and "fst y = 1/2" for y
@@ -481,7 +481,7 @@
have pab: "path_component T a b" if "a \<in> T" "b \<in> T" for a b
proof -
have "homotopic_with_canon (\<lambda>x. True) S T (\<lambda>x. a) (\<lambda>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 @@
"\<lbrakk>path p; path_image p \<subseteq> s; \<And>t. t \<in> {0..1} \<Longrightarrow> p t = q t\<rbrakk> \<Longrightarrow> 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 (\<lambda>h. True) S T f (\<lambda>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 \<open>auto simp: retraction_maps_def topspace_subtopology_subset continuous_map_in_subtopology\<close>)
ultimately show ?thesis by simp
@@ -3824,8 +3824,6 @@
qed
-
-
lemma contractible_space_product_topology:
"contractible_space(product_topology X I) \<longleftrightarrow>
topspace (product_topology X I) = {} \<or> (\<forall>i \<in> I. contractible_space(X i))"
@@ -3846,7 +3844,7 @@
using cs unfolding contractible_space_def by metis
have "homotopic_with (\<lambda>x. True)
(product_topology X I) (product_topology X I) id (\<lambda>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="\<lambda>x. b" in exI)
apply (rule_tac x="\<lambda>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 \<open>r > 0\<close>\<open>0 \<le> v\<close>
by (simp add: dist_norm n)
moreover have "x - v *\<^sub>R (u - a) \<in> T"
- by (simp add: f_def \<open>affine T\<close> \<open>u \<in> T\<close> \<open>x \<in> T\<close> assms mem_affine_3_minus2)
+ by (simp add: f_def \<open>u \<in> T\<close> \<open>x \<in> T\<close> assms mem_affine_3_minus2)
ultimately show "x - v *\<^sub>R (u - a) \<in> cball a r \<inter> 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 \<open>affine T\<close> continuous_on_id fid)
+ apply (auto simp: affine_closed \<open>affine T\<close> 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 \<open>affine T\<close> continuous_on_id gid)
+ apply (auto simp: affine_closed \<open>affine T\<close> 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 \<open>U \<noteq> {}\<close> \<open>K \<subseteq> S\<close> openin_imp_subset [OF opeU] by blast
show ?thesis
apply (rule that [of id id])
- using \<open>K \<subseteq> U\<close> by (auto simp: continuous_on_id intro: homeomorphismI)
+ using \<open>K \<subseteq> U\<close> by (auto intro: homeomorphismI)
next
assume "aff_dim S = 1"
then have "affine hull S homeomorphic (UNIV :: real set)"
--- 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 "((\<lambda>a. ennreal (F b - F a)) \<longlongrightarrow> F b - F a) (at_left a)"
by (rule continuous_on_tendsto_compose[where g="\<lambda>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>\<open>tag important\<close> sigma_finite_interval_measure:
@@ -745,7 +745,7 @@
have "((\<lambda>f. f 1) -` {l..u} \<inter> space (Pi\<^sub>M {1} (\<lambda>b. interval_measure (\<lambda>x. x)))) = {1::real} \<rightarrow>\<^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 \<le> 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 \<in> fmeasurable lborel"
and fmeasurable_box [iff]: "box a b \<in> fmeasurable lborel"
@@ -872,14 +872,14 @@
have "... \<le> (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 \<le> (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) = (\<Prod>b\<in>?B. (u - l) \<bullet> 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 "\<lambda>_. m" \<delta>])
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 \<notin> sets lebesgue"
--- 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 \<longleftrightarrow>
(\<forall>U c. openin X U \<and> c \<in> path_components_of(subtopology X U) \<longrightarrow> 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) \<open>f x \<in> C\<close> x disjnt_iff image_eqI)
qed
then show "?T \<subseteq> {x \<in> topspace X. f x \<in> C}"
- by (force simp: path_component_of_equiv topspace_subtopology)
+ by (force simp: path_component_of_equiv)
qed
qed
then show "openin Y C"
--- 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: "\<lbrakk>path g1; path g2; pathfinish g1 = pathstart g2\<rbrakk> \<Longrightarrow> 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 "\<lbrakk>a \<le> 1; b \<le> 1\<rbrakk> \<Longrightarrow> a + b \<le> 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) \<longleftrightarrow>
@@ -1545,7 +1545,7 @@
then obtain g where g: "path g" "path_image g \<subseteq> 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} \<subseteq> {x \<in> {0..1}. g x \<in> e1} \<union> {x \<in> {0..1}. g x \<in> e2}"
using as(3) g(2)[unfolded path_defs] by blast
moreover have "{x \<in> {0..1}. g x \<in> e1} \<inter> {x \<in> {0..1}. g x \<in> e2} = {}"
@@ -1691,7 +1691,7 @@
apply clarify
apply (rule_tac x="\<lambda>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 "\<And>S. S \<in> \<A> \<Longrightarrow> a \<in> S"
using assms by blast
then have "\<And>x. x \<in> topspace (subtopology X (\<Union>\<A>)) \<Longrightarrow> path_component_of (subtopology X (\<Union>\<A>)) a x"
- apply (simp add: topspace_subtopology)
+ apply (simp)
by (meson Union_upper \<A> path_component_of path_connectedin_subtopology)
then show ?thesis
using \<A> 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) = (\<lambda>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 \<open>a \<in> s\<close> ins, of "1/(u*C + 1)"] \<open>C>0\<close> \<open>z \<notin> s\<close> 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)"]])
--- 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 (\<lambda>x. if x \<in> 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 \<union> T) (\<lambda>x. if x \<in> 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 "\<dots> retract_of U"
by (rule Un)
@@ -2136,7 +2136,7 @@
proof
have "continuous_on (T \<union> (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 \<subseteq> U"
--- 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 \<in> Basis"
show "0 < ?a \<bullet> 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 ((\<bullet>) ?a) ?D = sum (\<lambda>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 "\<exists>y \<in> s. y \<noteq> x"
by (cases "s \<le> {x}") fastforce+
} note [dest!] = this
@@ -4242,9 +4242,9 @@
show "{x. 0 < f x} \<inter> {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 \<subseteq> {x. 0 < f x}"
apply (clarsimp simp add: f_def setdist_sing_in_set)
using assms
--- 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 "\<forall>i. \<exists>y. y \<in> \<rat> \<and> y < x \<bullet> i \<and> x \<bullet> i - y < e'" (is "\<forall>i. ?th i")
proof
fix i
@@ -884,7 +884,7 @@
by (simp add: dual_order.antisym euclidean_eqI)
}
moreover have "c \<in> 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>\<open>tag unimportant\<close> \<open>Openness of halfspaces.\<close>
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\<bullet>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\<bullet>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 \<le> 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 \<ge> 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\<bullet>i \<le> 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\<bullet>i \<ge> 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. \<forall>i\<in>Basis. x\<bullet>i \<le> b\<bullet>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. \<forall>i\<in>Basis. a\<bullet>i \<le> x\<bullet>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 \<noteq> 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 (\<lambda>n. \<forall>i\<in>Basis. dist (f (r n) \<bullet> i) (l \<bullet> 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 \<in> 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 "\<forall>y. dist y (f x) < \<delta> \<longrightarrow> y \<in> f ` A"
using \<open>e > 0\<close> \<open>B > 0\<close>
- by (auto simp: \<delta>_def field_split_simps mult_less_0_iff)
+ by (auto simp: \<delta>_def field_split_simps)
qed
qed
@@ -2349,8 +2349,7 @@
proof -
let ?D = "{i\<in>Basis. P i}"
have "closed (\<Inter>i\<in>?D. {x::'a. x\<bullet>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 "(\<Inter>i\<in>?D. {x::'a. x\<bullet>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"
--- 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 "... = (\<Prod>w \<in> 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 = "\<lambda>x. 1 - e / card subA", simplified])
@@ -1117,7 +1117,7 @@
have "\<exists>p. real_polynomial_function p \<and> (\<forall>x \<in> S. \<bar>f x \<bullet> b - p x\<bar> < e / DIM('b))"
apply (rule exE [OF Stone_Weierstrass_real_polynomial_function [OF S _, of "\<lambda>x. f x \<bullet> 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 (\<Sum>b\<in>Basis. (f x \<bullet> b) *\<^sub>R b - pf b x *\<^sub>R b) < e" .
}
ultimately