# HG changeset patch
# User Manuel Eberl <eberlm@in.tum.de>
# Date 1589456684 -7200
# Node ID 8ed78bb0b915f6e934a37edbe7ccc1e120dbd39d
# Parent  0bbe0866b7e6f0e94bf0fdacf44e3d123a2dcb50
Tuned some proofs in HOL-Analysis

diff -r 0bbe0866b7e6 -r 8ed78bb0b915 src/HOL/Analysis/Abstract_Topology.thy
--- 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;
diff -r 0bbe0866b7e6 -r 8ed78bb0b915 src/HOL/Analysis/Affine.thy
--- 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:
diff -r 0bbe0866b7e6 -r 8ed78bb0b915 src/HOL/Analysis/Bochner_Integration.thy
--- 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
diff -r 0bbe0866b7e6 -r 8ed78bb0b915 src/HOL/Analysis/Finite_Cartesian_Product.thy
--- 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
diff -r 0bbe0866b7e6 -r 8ed78bb0b915 src/HOL/Analysis/Further_Topology.thy
--- 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})"
diff -r 0bbe0866b7e6 -r 8ed78bb0b915 src/HOL/Analysis/Measure_Space.thy
--- 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
diff -r 0bbe0866b7e6 -r 8ed78bb0b915 src/HOL/Analysis/Polytope.thy
--- 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)"
diff -r 0bbe0866b7e6 -r 8ed78bb0b915 src/HOL/Library/Infinite_Set.thy
--- 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: