--- 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
--- 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)
--- 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})"
--- 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
--- 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