--- a/src/HOL/Analysis/Abstract_Topology.thy Thu May 14 10:26:33 2020 +0100
+++ b/src/HOL/Analysis/Abstract_Topology.thy Thu May 14 13:44:44 2020 +0200
@@ -524,8 +524,7 @@
\<not>(\<exists>E1 E2. openin (top_of_set S) E1 \<and>
openin (top_of_set S) E2 \<and>
S \<subseteq> E1 \<union> E2 \<and> E1 \<inter> E2 = {} \<and> E1 \<noteq> {} \<and> E2 \<noteq> {})"
- apply (simp add: connected_def openin_open disjoint_iff_not_equal, safe)
- by (simp_all, blast+) (* SLOW *)
+ unfolding connected_def openin_open disjoint_iff_not_equal by blast
lemma connected_openin_eq:
"connected S \<longleftrightarrow>
@@ -2260,7 +2259,8 @@
lemma separatedin_closed_sets:
"\<lbrakk>closedin X S; closedin X T\<rbrakk> \<Longrightarrow> separatedin X S T \<longleftrightarrow> disjnt S T"
- by (metis closedin_def closure_of_eq disjnt_def inf_commute separatedin_def)
+ unfolding closure_of_eq disjnt_def separatedin_def
+ by (metis closedin_def closure_of_eq inf_commute)
lemma separatedin_subtopology:
"separatedin (subtopology X U) S T \<longleftrightarrow> S \<subseteq> U \<and> T \<subseteq> U \<and> separatedin X S T"
@@ -4153,10 +4153,16 @@
qed
lemma topology_base_unique:
- "\<lbrakk>\<And>S. P S \<Longrightarrow> openin X S;
- \<And>U x. \<lbrakk>openin X U; x \<in> U\<rbrakk> \<Longrightarrow> \<exists>B. P B \<and> x \<in> B \<and> B \<subseteq> U\<rbrakk>
- \<Longrightarrow> topology(arbitrary union_of P) = X"
- by (metis openin_topology_base_unique openin_inverse [of X])
+ assumes "\<And>S. P S \<Longrightarrow> openin X S"
+ "\<And>U x. \<lbrakk>openin X U; x \<in> U\<rbrakk> \<Longrightarrow> \<exists>B. P B \<and> x \<in> B \<and> B \<subseteq> U"
+ shows "topology (arbitrary union_of P) = X"
+proof -
+ have "X = topology (openin X)"
+ by (simp add: openin_inverse)
+ also from assms have "openin X = arbitrary union_of P"
+ by (subst openin_topology_base_unique) auto
+ finally show ?thesis ..
+qed
lemma topology_bases_eq_aux:
"\<lbrakk>(arbitrary union_of P) S;
--- a/src/HOL/Analysis/Affine.thy Thu May 14 10:26:33 2020 +0100
+++ b/src/HOL/Analysis/Affine.thy Thu May 14 13:44:44 2020 +0200
@@ -391,7 +391,7 @@
qed (use \<open>F \<subseteq> insert a S\<close> in auto)
qed
then show ?thesis
- unfolding affine_hull_explicit span_explicit by blast
+ unfolding affine_hull_explicit span_explicit by fast
qed
lemma affine_hull_insert_span:
--- a/src/HOL/Analysis/Bochner_Integration.thy Thu May 14 10:26:33 2020 +0100
+++ b/src/HOL/Analysis/Bochner_Integration.thy Thu May 14 13:44:44 2020 +0200
@@ -219,9 +219,17 @@
by (simp add: indicator_def[abs_def])
next
case (insert x F)
- then show ?case
- by (auto intro!: add mult set sum_nonneg split: split_indicator split_indicator_asm
- simp del: sum_mult_indicator simp: sum_nonneg_eq_0_iff)
+ from insert.prems have nonneg: "x \<ge> 0" "\<And>y. y \<in> F \<Longrightarrow> y \<ge> 0"
+ by simp_all
+ hence *: "P (\<lambda>xa. x * indicat_real {x' \<in> space M. U' i x' = x} xa)"
+ by (intro mult set) auto
+ have "P (\<lambda>z. x * indicat_real {x' \<in> space M. U' i x' = x} z +
+ (\<Sum>y\<in>F. y * indicat_real {x \<in> space M. U' i x = y} z))"
+ using insert(1-3)
+ by (intro add * sum_nonneg mult_nonneg_nonneg)
+ (auto simp: nonneg indicator_def sum_nonneg_eq_0_iff)
+ thus ?case
+ using insert.hyps by (subst sum.insert) auto
qed
with U' show "P (U' i)" by simp
qed
--- a/src/HOL/Analysis/Finite_Cartesian_Product.thy Thu May 14 10:26:33 2020 +0100
+++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy Thu May 14 13:44:44 2020 +0200
@@ -957,7 +957,7 @@
by (metis eq_iff_diff_eq_0 vector_mul_eq_0 vector_ssub_ldistrib)
lemma vector_mul_rcancel[simp]: "a *s x = b *s x \<longleftrightarrow> (a::'a::field) = b \<or> x = 0"
- by (metis eq_iff_diff_eq_0 vector_mul_eq_0 vector_sub_rdistrib)
+ by (subst eq_iff_diff_eq_0, subst vector_sub_rdistrib [symmetric]) simp
lemma scalar_mult_eq_scaleR [abs_def]: "c *s x = c *\<^sub>R x"
unfolding scaleR_vec_def vector_scalar_mult_def by simp
--- a/src/HOL/Analysis/Further_Topology.thy Thu May 14 10:26:33 2020 +0100
+++ b/src/HOL/Analysis/Further_Topology.thy Thu May 14 13:44:44 2020 +0200
@@ -1255,7 +1255,7 @@
using \<open>C \<subseteq> U - S\<close> \<open>S \<subseteq> U\<close> \<open>a \<in> C\<close> by force
show "continuous_on (j ` (S \<union> (C - {a}))) k"
apply (rule continuous_on_subset [OF homeomorphism_cont2 [OF homhk]])
- using jim \<open>C \<subseteq> U - S\<close> \<open>S \<subseteq> U\<close> \<open>ball a d \<inter> U \<subseteq> C\<close> j_def by fastforce
+ using jim \<open>C \<subseteq> U - S\<close> \<open>S \<subseteq> U\<close> \<open>ball a d \<inter> U \<subseteq> C\<close> j_def by blast
show "continuous_on (k ` j ` (S \<union> (C - {a}))) f"
proof (clarify intro!: continuous_on_subset [OF contf])
fix y assume "y \<in> S \<union> (C - {a})"
--- a/src/HOL/Analysis/Measure_Space.thy Thu May 14 10:26:33 2020 +0100
+++ b/src/HOL/Analysis/Measure_Space.thy Thu May 14 13:44:44 2020 +0200
@@ -1897,8 +1897,10 @@
"finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> F i \<in> sets M) \<Longrightarrow> measure M (\<Union>i\<in>I. F i) \<le> (\<Sum>i\<in>I. measure M (F i))"
proof (induction I rule: finite_induct)
case (insert i I)
- then have "measure M (\<Union>i\<in>insert i I. F i) \<le> measure M (F i) + measure M (\<Union>i\<in>I. F i)"
- by (auto intro!: measure_Un_le)
+ then have "measure M (\<Union>i\<in>insert i I. F i) = measure M (F i \<union> \<Union> (F ` I))"
+ by simp
+ also from insert have "measure M (F i \<union> \<Union> (F ` I)) \<le> measure M (F i) + measure M (\<Union> (F ` I))"
+ by (intro measure_Un_le sets.finite_Union) auto
also have "measure M (\<Union>i\<in>I. F i) \<le> (\<Sum>i\<in>I. measure M (F i))"
using insert by auto
finally show ?case
--- a/src/HOL/Analysis/Polytope.thy Thu May 14 10:26:33 2020 +0100
+++ b/src/HOL/Analysis/Polytope.thy Thu May 14 13:44:44 2020 +0200
@@ -2577,7 +2577,7 @@
have hface: "h face_of S"
and "\<exists>a b. a \<noteq> 0 \<and> S \<subseteq> {x. a \<bullet> x \<le> b} \<and> h = S \<inter> {x. a \<bullet> x = b}"
if "h \<in> F" for h
- using exposed_face_of F_def that by simp_all auto
+ using exposed_face_of F_def that by blast+
then obtain a b where ab:
"\<And>h. h \<in> F \<Longrightarrow> a h \<noteq> 0 \<and> S \<subseteq> {x. a h \<bullet> x \<le> b h} \<and> h = S \<inter> {x. a h \<bullet> x = b h}"
by metis
@@ -3026,7 +3026,7 @@
show "norm (x - y) \<le> e / 2" if "x \<in> X" "y \<in> X" for x y
proof -
have "norm x < B" "norm y < B"
- using B \<open>X \<in> \<F>'\<close> eq that by fastforce+
+ using B \<open>X \<in> \<F>'\<close> eq that by blast+
have "norm (x - y) \<le> (\<Sum>b\<in>Basis. \<bar>(x-y) \<bullet> b\<bar>)"
by (rule norm_le_l1)
also have "... \<le> of_nat (DIM('a)) * (e / 2 / DIM('a))"
@@ -3034,8 +3034,7 @@
fix i::'a
assume "i \<in> Basis"
then have I': "\<And>z b. \<lbrakk>z \<in> C; b = z * e / (2 * real DIM('a))\<rbrakk> \<Longrightarrow> i \<bullet> x \<le> b \<and> i \<bullet> y \<le> b \<or> i \<bullet> x \<ge> b \<and> i \<bullet> y \<ge> b"
- using I \<open>X \<in> \<F>'\<close> that
- by (fastforce simp: I_def)
+ using I[of X x y] \<open>X \<in> \<F>'\<close> that unfolding I_def by auto
show "\<bar>(x - y) \<bullet> i\<bar> \<le> e / 2 / real DIM('a)"
proof (rule ccontr)
assume "\<not> \<bar>(x - y) \<bullet> i\<bar> \<le> e / 2 / real DIM('a)"
--- a/src/HOL/Library/Infinite_Set.thy Thu May 14 10:26:33 2020 +0100
+++ b/src/HOL/Library/Infinite_Set.thy Thu May 14 13:44:44 2020 +0200
@@ -371,8 +371,9 @@
then show ?case by simp
next
case (insert a A)
- with R show ?case
- by (metis empty_iff insert_iff) (* somewhat slow *)
+ have False
+ using R(1)[of a] R(2)[of _ a] insert(3,4) by blast
+ thus ?case ..
qed
corollary Union_maximal_sets: