Some fixes related to compactE_image
authorpaulson <lp15@cam.ac.uk>
Wed Apr 26 16:58:31 2017 +0100 (2017-04-26)
changeset 65585a043de9ad41e
parent 65584 1d9a96750a40
child 65586 91e451bc0f1f
Some fixes related to compactE_image
src/HOL/Analysis/Brouwer_Fixpoint.thy
src/HOL/Analysis/Complex_Transcendental.thy
src/HOL/Analysis/Lebesgue_Measure.thy
src/HOL/Analysis/Topology_Euclidean_Space.thy
src/HOL/Analysis/Weierstrass_Theorems.thy
     1.1 --- a/src/HOL/Analysis/Brouwer_Fixpoint.thy	Wed Apr 26 15:57:16 2017 +0100
     1.2 +++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy	Wed Apr 26 16:58:31 2017 +0100
     1.3 @@ -3604,7 +3604,7 @@
     1.4    obtains V where "openin (subtopology euclidean U) V" "(S \<union> T) retract_of V"
     1.5  proof (cases "S = {} \<or> T = {}")
     1.6    case True with assms that show ?thesis
     1.7 -    by (auto simp: intro: ANR_imp_neighbourhood_retract)
     1.8 +    by (metis ANR_imp_neighbourhood_retract Un_commute inf_bot_right sup_inf_absorb)
     1.9  next
    1.10    case False
    1.11    then have [simp]: "S \<noteq> {}" "T \<noteq> {}" by auto
     2.1 --- a/src/HOL/Analysis/Complex_Transcendental.thy	Wed Apr 26 15:57:16 2017 +0100
     2.2 +++ b/src/HOL/Analysis/Complex_Transcendental.thy	Wed Apr 26 16:58:31 2017 +0100
     2.3 @@ -1017,6 +1017,7 @@
     2.4  definition ln_complex :: "complex \<Rightarrow> complex"
     2.5    where "ln_complex \<equiv> \<lambda>z. THE w. exp w = z & -pi < Im(w) & Im(w) \<le> pi"
     2.6  
     2.7 +text\<open>NOTE: within this scope, the constant Ln is not yet available!\<close>
     2.8  lemma
     2.9    assumes "z \<noteq> 0"
    2.10      shows exp_Ln [simp]:  "exp(ln z) = z"
    2.11 @@ -1046,9 +1047,6 @@
    2.12    apply auto
    2.13    done
    2.14  
    2.15 -lemma Ln_eq_zero_iff [simp]: "x \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> Ln x = 0 \<longleftrightarrow> x = 1"
    2.16 -  by auto (metis exp_Ln exp_zero nonpos_Reals_zero_I)
    2.17 -
    2.18  subsection\<open>Relation to Real Logarithm\<close>
    2.19  
    2.20  lemma Ln_of_real:
    2.21 @@ -1073,14 +1071,18 @@
    2.22  lemma cmod_Ln_Reals [simp]: "z \<in> \<real> \<Longrightarrow> 0 < Re z \<Longrightarrow> cmod (ln z) = norm (ln (Re z))"
    2.23    using Ln_of_real by force
    2.24  
    2.25 -lemma Ln_1: "ln 1 = (0::complex)"
    2.26 +lemma Ln_1 [simp]: "ln 1 = (0::complex)"
    2.27  proof -
    2.28    have "ln (exp 0) = (0::complex)"
    2.29      by (metis (mono_tags, hide_lams) Ln_of_real exp_zero ln_one of_real_0 of_real_1 zero_less_one)
    2.30    then show ?thesis
    2.31 -    by simp
    2.32 +    by simp                              
    2.33  qed
    2.34  
    2.35 +  
    2.36 +lemma Ln_eq_zero_iff [simp]: "x \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> ln x = 0 \<longleftrightarrow> x = 1" for x::complex
    2.37 +  by auto (metis exp_Ln exp_zero nonpos_Reals_zero_I)
    2.38 +
    2.39  instance
    2.40    by intro_classes (rule ln_complex_def Ln_1)
    2.41  
     3.1 --- a/src/HOL/Analysis/Lebesgue_Measure.thy	Wed Apr 26 15:57:16 2017 +0100
     3.2 +++ b/src/HOL/Analysis/Lebesgue_Measure.thy	Wed Apr 26 16:58:31 2017 +0100
     3.3 @@ -220,7 +220,7 @@
     3.4      proof (rule compactE_image)
     3.5        show "compact {a'..b}"
     3.6          by (rule compact_Icc)
     3.7 -      show "\<forall>i \<in> S'. open ({l i<..<r i + delta i})" by auto
     3.8 +      show "\<And>i. i \<in> S' \<Longrightarrow> open ({l i<..<r i + delta i})" by auto
     3.9        have "{a'..b} \<subseteq> {a <.. b}"
    3.10          by auto
    3.11        also have "{a <.. b} = (\<Union>i\<in>S'. {l i<..r i})"
     4.1 --- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Wed Apr 26 15:57:16 2017 +0100
     4.2 +++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Wed Apr 26 16:58:31 2017 +0100
     4.3 @@ -4538,7 +4538,7 @@
     4.4    have "compact U" "\<forall>x\<in>U. open (ball x 1)" "U \<subseteq> (\<Union>x\<in>U. ball x 1)"
     4.5      using assms by auto
     4.6    then obtain D where D: "D \<subseteq> U" "finite D" "U \<subseteq> (\<Union>x\<in>D. ball x 1)"
     4.7 -    by (rule compactE_image)
     4.8 +    by (metis compactE_image)
     4.9    from \<open>finite D\<close> have "bounded (\<Union>x\<in>D. ball x 1)"
    4.10      by (simp add: bounded_UN)
    4.11    then show "bounded U" using \<open>U \<subseteq> (\<Union>x\<in>D. ball x 1)\<close>
    4.12 @@ -7717,14 +7717,14 @@
    4.13        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"
    4.14        by metis
    4.15      then have "\<forall>y\<in>t. open (b y)" "t \<subseteq> (\<Union>y\<in>t. b y)" by auto
    4.16 -    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)"
    4.17 -      by auto
    4.18 +    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)"
    4.19 +      by metis
    4.20      moreover from D c have "(\<Inter>y\<in>D. a y) \<times> t \<subseteq> (\<Union>y\<in>D. c y)"
    4.21        by (fastforce simp: subset_eq)
    4.22      ultimately show "\<exists>a. open a \<and> x \<in> a \<and> (\<exists>d\<subseteq>C. finite d \<and> a \<times> t \<subseteq> \<Union>d)"
    4.23        using c by (intro exI[of _ "c`D"] exI[of _ "\<Inter>(a`D)"] conjI) (auto intro!: open_INT)
    4.24    qed
    4.25 -  then obtain a d where a: "\<forall>x\<in>s. open (a x)" "s \<subseteq> (\<Union>x\<in>s. a x)"
    4.26 +  then obtain a d where a: "\<And>x. x\<in>s \<Longrightarrow> open (a x)" "s \<subseteq> (\<Union>x\<in>s. a x)"
    4.27      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"
    4.28      unfolding subset_eq UN_iff by metis
    4.29    moreover
     5.1 --- a/src/HOL/Analysis/Weierstrass_Theorems.thy	Wed Apr 26 15:57:16 2017 +0100
     5.2 +++ b/src/HOL/Analysis/Weierstrass_Theorems.thy	Wed Apr 26 16:58:31 2017 +0100
     5.3 @@ -261,7 +261,7 @@
     5.4    then have *: "S-U \<subseteq> (\<Union>x \<in> S-U. Uf x)"
     5.5      by blast
     5.6    obtain subU where subU: "subU \<subseteq> S - U" "finite subU" "S - U \<subseteq> (\<Union>x \<in> subU. Uf x)"
     5.7 -    by (blast intro: that open_Uf compactE_image [OF com_sU _ *])
     5.8 +    by (blast intro: that compactE_image [OF com_sU open_Uf *])
     5.9    then have [simp]: "subU \<noteq> {}"
    5.10      using t1 by auto
    5.11    then have cardp: "card subU > 0" using subU
    5.12 @@ -401,7 +401,7 @@
    5.13    have NN0: "(1/(k*\<delta>)) ^ (NN e) < e" if "e>0" for e
    5.14    proof -
    5.15      have "0 < ln (real k) + ln \<delta>"
    5.16 -      using \<delta>01(1) \<open>0 < k\<close> k\<delta>(1) ln_gt_zero by fastforce
    5.17 +      using \<delta>01(1) \<open>0 < k\<close> k\<delta>(1) ln_gt_zero ln_mult by fastforce 
    5.18      then have "real (NN e) * ln (1 / (real k * \<delta>)) < ln e"
    5.19        using k\<delta>(1) NN(2) [of e] that by (simp add: ln_div divide_simps)
    5.20      then have "exp (real (NN e) * ln (1 / (real k * \<delta>))) < e"
    5.21 @@ -459,7 +459,7 @@
    5.22    have com_A: "compact A" using A
    5.23      by (metis compact compact_Int_closed inf.absorb_iff2)
    5.24    obtain subA where subA: "subA \<subseteq> A" "finite subA" "A \<subseteq> (\<Union>x \<in> subA. Vf x)"
    5.25 -    by (blast intro: that open_Vf compactE_image [OF com_A _ sum_max_0])
    5.26 +    by (blast intro: that compactE_image [OF com_A open_Vf sum_max_0])
    5.27    then have [simp]: "subA \<noteq> {}"
    5.28      using \<open>a \<in> A\<close> by auto
    5.29    then have cardp: "card subA > 0" using subA