# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1493222311 -3600
# Node ID a043de9ad41e3c9bde3e91d242d251dfcb2cd65c
# Parent  1d9a96750a409ecc2160be1b9691c201e191328d
Some fixes related to compactE_image

diff -r 1d9a96750a40 -r a043de9ad41e src/HOL/Analysis/Brouwer_Fixpoint.thy
--- a/src/HOL/Analysis/Brouwer_Fixpoint.thy	Wed Apr 26 15:57:16 2017 +0100
+++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy	Wed Apr 26 16:58:31 2017 +0100
@@ -3604,7 +3604,7 @@
   obtains V where "openin (subtopology euclidean U) V" "(S \<union> T) retract_of V"
 proof (cases "S = {} \<or> T = {}")
   case True with assms that show ?thesis
-    by (auto simp: intro: ANR_imp_neighbourhood_retract)
+    by (metis ANR_imp_neighbourhood_retract Un_commute inf_bot_right sup_inf_absorb)
 next
   case False
   then have [simp]: "S \<noteq> {}" "T \<noteq> {}" by auto
diff -r 1d9a96750a40 -r a043de9ad41e src/HOL/Analysis/Complex_Transcendental.thy
--- a/src/HOL/Analysis/Complex_Transcendental.thy	Wed Apr 26 15:57:16 2017 +0100
+++ b/src/HOL/Analysis/Complex_Transcendental.thy	Wed Apr 26 16:58:31 2017 +0100
@@ -1017,6 +1017,7 @@
 definition ln_complex :: "complex \<Rightarrow> complex"
   where "ln_complex \<equiv> \<lambda>z. THE w. exp w = z & -pi < Im(w) & Im(w) \<le> pi"
 
+text\<open>NOTE: within this scope, the constant Ln is not yet available!\<close>
 lemma
   assumes "z \<noteq> 0"
     shows exp_Ln [simp]:  "exp(ln z) = z"
@@ -1046,9 +1047,6 @@
   apply auto
   done
 
-lemma Ln_eq_zero_iff [simp]: "x \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> Ln x = 0 \<longleftrightarrow> x = 1"
-  by auto (metis exp_Ln exp_zero nonpos_Reals_zero_I)
-
 subsection\<open>Relation to Real Logarithm\<close>
 
 lemma Ln_of_real:
@@ -1073,14 +1071,18 @@
 lemma cmod_Ln_Reals [simp]: "z \<in> \<real> \<Longrightarrow> 0 < Re z \<Longrightarrow> cmod (ln z) = norm (ln (Re z))"
   using Ln_of_real by force
 
-lemma Ln_1: "ln 1 = (0::complex)"
+lemma Ln_1 [simp]: "ln 1 = (0::complex)"
 proof -
   have "ln (exp 0) = (0::complex)"
     by (metis (mono_tags, hide_lams) Ln_of_real exp_zero ln_one of_real_0 of_real_1 zero_less_one)
   then show ?thesis
-    by simp
+    by simp                              
 qed
 
+  
+lemma Ln_eq_zero_iff [simp]: "x \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> ln x = 0 \<longleftrightarrow> x = 1" for x::complex
+  by auto (metis exp_Ln exp_zero nonpos_Reals_zero_I)
+
 instance
   by intro_classes (rule ln_complex_def Ln_1)
 
diff -r 1d9a96750a40 -r a043de9ad41e src/HOL/Analysis/Lebesgue_Measure.thy
--- a/src/HOL/Analysis/Lebesgue_Measure.thy	Wed Apr 26 15:57:16 2017 +0100
+++ b/src/HOL/Analysis/Lebesgue_Measure.thy	Wed Apr 26 16:58:31 2017 +0100
@@ -220,7 +220,7 @@
     proof (rule compactE_image)
       show "compact {a'..b}"
         by (rule compact_Icc)
-      show "\<forall>i \<in> S'. open ({l i<..<r i + delta i})" by auto
+      show "\<And>i. i \<in> S' \<Longrightarrow> open ({l i<..<r i + delta i})" by auto
       have "{a'..b} \<subseteq> {a <.. b}"
         by auto
       also have "{a <.. b} = (\<Union>i\<in>S'. {l i<..r i})"
diff -r 1d9a96750a40 -r a043de9ad41e src/HOL/Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Wed Apr 26 15:57:16 2017 +0100
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Wed Apr 26 16:58:31 2017 +0100
@@ -4538,7 +4538,7 @@
   have "compact U" "\<forall>x\<in>U. open (ball x 1)" "U \<subseteq> (\<Union>x\<in>U. ball x 1)"
     using assms by auto
   then obtain D where D: "D \<subseteq> U" "finite D" "U \<subseteq> (\<Union>x\<in>D. ball x 1)"
-    by (rule compactE_image)
+    by (metis compactE_image)
   from \<open>finite D\<close> have "bounded (\<Union>x\<in>D. ball x 1)"
     by (simp add: bounded_UN)
   then show "bounded U" using \<open>U \<subseteq> (\<Union>x\<in>D. ball x 1)\<close>
@@ -7717,14 +7717,14 @@
       and c: "\<And>y. y \<in> t \<Longrightarrow> c y \<in> C \<and> open (a y) \<and> open (b y) \<and> x \<in> a y \<and> y \<in> b y \<and> a y \<times> b y \<subseteq> c y"
       by metis
     then have "\<forall>y\<in>t. open (b y)" "t \<subseteq> (\<Union>y\<in>t. b y)" by auto
-    from compactE_image[OF \<open>compact t\<close> this] obtain D where D: "D \<subseteq> t" "finite D" "t \<subseteq> (\<Union>y\<in>D. b y)"
-      by auto
+    with compactE_image[OF \<open>compact t\<close>] obtain D where D: "D \<subseteq> t" "finite D" "t \<subseteq> (\<Union>y\<in>D. b y)"
+      by metis
     moreover from D c have "(\<Inter>y\<in>D. a y) \<times> t \<subseteq> (\<Union>y\<in>D. c y)"
       by (fastforce simp: subset_eq)
     ultimately show "\<exists>a. open a \<and> x \<in> a \<and> (\<exists>d\<subseteq>C. finite d \<and> a \<times> t \<subseteq> \<Union>d)"
       using c by (intro exI[of _ "c`D"] exI[of _ "\<Inter>(a`D)"] conjI) (auto intro!: open_INT)
   qed
-  then obtain a d where a: "\<forall>x\<in>s. open (a x)" "s \<subseteq> (\<Union>x\<in>s. a x)"
+  then obtain a d where a: "\<And>x. x\<in>s \<Longrightarrow> open (a x)" "s \<subseteq> (\<Union>x\<in>s. a x)"
     and d: "\<And>x. x \<in> s \<Longrightarrow> d x \<subseteq> C \<and> finite (d x) \<and> a x \<times> t \<subseteq> \<Union>d x"
     unfolding subset_eq UN_iff by metis
   moreover
diff -r 1d9a96750a40 -r a043de9ad41e src/HOL/Analysis/Weierstrass_Theorems.thy
--- a/src/HOL/Analysis/Weierstrass_Theorems.thy	Wed Apr 26 15:57:16 2017 +0100
+++ b/src/HOL/Analysis/Weierstrass_Theorems.thy	Wed Apr 26 16:58:31 2017 +0100
@@ -261,7 +261,7 @@
   then have *: "S-U \<subseteq> (\<Union>x \<in> S-U. Uf x)"
     by blast
   obtain subU where subU: "subU \<subseteq> S - U" "finite subU" "S - U \<subseteq> (\<Union>x \<in> subU. Uf x)"
-    by (blast intro: that open_Uf compactE_image [OF com_sU _ *])
+    by (blast intro: that compactE_image [OF com_sU open_Uf *])
   then have [simp]: "subU \<noteq> {}"
     using t1 by auto
   then have cardp: "card subU > 0" using subU
@@ -401,7 +401,7 @@
   have NN0: "(1/(k*\<delta>)) ^ (NN e) < e" if "e>0" for e
   proof -
     have "0 < ln (real k) + ln \<delta>"
-      using \<delta>01(1) \<open>0 < k\<close> k\<delta>(1) ln_gt_zero by fastforce
+      using \<delta>01(1) \<open>0 < k\<close> k\<delta>(1) ln_gt_zero ln_mult by fastforce 
     then have "real (NN e) * ln (1 / (real k * \<delta>)) < ln e"
       using k\<delta>(1) NN(2) [of e] that by (simp add: ln_div divide_simps)
     then have "exp (real (NN e) * ln (1 / (real k * \<delta>))) < e"
@@ -459,7 +459,7 @@
   have com_A: "compact A" using A
     by (metis compact compact_Int_closed inf.absorb_iff2)
   obtain subA where subA: "subA \<subseteq> A" "finite subA" "A \<subseteq> (\<Union>x \<in> subA. Vf x)"
-    by (blast intro: that open_Vf compactE_image [OF com_A _ sum_max_0])
+    by (blast intro: that compactE_image [OF com_A open_Vf sum_max_0])
   then have [simp]: "subA \<noteq> {}"
     using \<open>a \<in> A\<close> by auto
   then have cardp: "card subA > 0" using subA