capitalize proper names in lemma names
authornipkow
Sat Dec 29 15:43:53 2018 +0100 (4 months ago)
changeset 695294ab9657b3257
parent 69526 5574d504cf36
child 69530 fc0da2166cda
capitalize proper names in lemma names
src/HOL/Analysis/Abstract_Topology.thy
src/HOL/Analysis/Brouwer_Fixpoint.thy
src/HOL/Analysis/Cauchy_Integral_Theorem.thy
src/HOL/Analysis/Complex_Analysis_Basics.thy
src/HOL/Analysis/Complex_Transcendental.thy
src/HOL/Analysis/Connected.thy
src/HOL/Analysis/Convex_Euclidean_Space.thy
src/HOL/Analysis/Derivative.thy
src/HOL/Analysis/Elementary_Topology.thy
src/HOL/Analysis/Gamma_Function.thy
src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
src/HOL/Analysis/Infinite_Products.thy
src/HOL/Analysis/Starlike.thy
src/HOL/Analysis/Uniform_Limit.thy
src/HOL/Analysis/document/root.tex
src/HOL/Computational_Algebra/Fundamental_Theorem_Algebra.thy
src/HOL/Decision_Procs/Approximation.thy
src/HOL/MacLaurin.thy
src/HOL/Probability/Probability_Mass_Function.thy
src/HOL/Topological_Spaces.thy
     1.1 --- a/src/HOL/Analysis/Abstract_Topology.thy	Fri Dec 28 19:01:35 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Abstract_Topology.thy	Sat Dec 29 15:43:53 2018 +0100
     1.3 @@ -2433,7 +2433,7 @@
     1.4    using openin_subset by fastforce
     1.5  
     1.6  lemma compactin_euclideanreal_iff [simp]: "compactin euclideanreal S \<longleftrightarrow> compact S"
     1.7 -  by (simp add: compact_eq_heine_borel compactin_def) meson
     1.8 +  by (simp add: compact_eq_Heine_Borel compactin_def) meson
     1.9  
    1.10  lemma compactin_absolute [simp]:
    1.11     "compactin (subtopology X S) S \<longleftrightarrow> compactin X S"
    1.12 @@ -2725,7 +2725,7 @@
    1.13  lemma compact_space_discrete_topology: "compact_space(discrete_topology X) \<longleftrightarrow> finite X"
    1.14    by (simp add: compactin_discrete_topology compact_space_def)
    1.15  
    1.16 -lemma compact_space_imp_bolzano_weierstrass:
    1.17 +lemma compact_space_imp_Bolzano_Weierstrass:
    1.18    assumes "compact_space X" "infinite S" "S \<subseteq> topspace X"
    1.19    shows "X derived_set_of S \<noteq> {}"
    1.20  proof
    1.21 @@ -2738,19 +2738,19 @@
    1.22      by (metis \<open>infinite S\<close> compactin_subspace compact_space_discrete_topology inf_bot_right subtopology_eq_discrete_topology_eq)
    1.23  qed
    1.24  
    1.25 -lemma compactin_imp_bolzano_weierstrass:
    1.26 +lemma compactin_imp_Bolzano_Weierstrass:
    1.27     "\<lbrakk>compactin X S; infinite T \<and> T \<subseteq> S\<rbrakk> \<Longrightarrow> S \<inter> X derived_set_of T \<noteq> {}"
    1.28 -  using compact_space_imp_bolzano_weierstrass [of "subtopology X S"]
    1.29 +  using compact_space_imp_Bolzano_Weierstrass [of "subtopology X S"]
    1.30    by (simp add: compactin_subspace derived_set_of_subtopology inf_absorb2 topspace_subtopology)
    1.31  
    1.32 -lemma compact_closure_of_imp_bolzano_weierstrass:
    1.33 +lemma compact_closure_of_imp_Bolzano_Weierstrass:
    1.34     "\<lbrakk>compactin X (X closure_of S); infinite T; T \<subseteq> S; T \<subseteq> topspace X\<rbrakk> \<Longrightarrow> X derived_set_of T \<noteq> {}"
    1.35 -  using closure_of_mono closure_of_subset compactin_imp_bolzano_weierstrass by fastforce
    1.36 +  using closure_of_mono closure_of_subset compactin_imp_Bolzano_Weierstrass by fastforce
    1.37  
    1.38  lemma discrete_compactin_eq_finite:
    1.39     "S \<inter> X derived_set_of S = {} \<Longrightarrow> compactin X S \<longleftrightarrow> S \<subseteq> topspace X \<and> finite S"
    1.40    apply (rule iffI)
    1.41 -  using compactin_imp_bolzano_weierstrass compactin_subset_topspace apply blast
    1.42 +  using compactin_imp_Bolzano_Weierstrass compactin_subset_topspace apply blast
    1.43    by (simp add: finite_imp_compactin_eq)
    1.44  
    1.45  lemma discrete_compact_space_eq_finite:
     2.1 --- a/src/HOL/Analysis/Brouwer_Fixpoint.thy	Fri Dec 28 19:01:35 2018 +0100
     2.2 +++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy	Sat Dec 29 15:43:53 2018 +0100
     2.3 @@ -21,10 +21,12 @@
     2.4  (* FIXME mv topology euclidean space *)
     2.5  subsection \<open>Retractions\<close>
     2.6  
     2.7 -definition "retraction S T r \<longleftrightarrow> T \<subseteq> S \<and> continuous_on S r \<and> r ` S \<subseteq> T \<and> (\<forall>x\<in>T. r x = x)"
     2.8 -
     2.9 -definition retract_of (infixl "retract'_of" 50)
    2.10 -  where "(T retract_of S) \<longleftrightarrow> (\<exists>r. retraction S T r)"
    2.11 +definition%important retraction :: "('a::topological_space) set \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> bool"
    2.12 +where "retraction S T r \<longleftrightarrow>
    2.13 +  T \<subseteq> S \<and> continuous_on S r \<and> r ` S \<subseteq> T \<and> (\<forall>x\<in>T. r x = x)"
    2.14 +
    2.15 +definition%important retract_of (infixl "retract'_of" 50) where
    2.16 +"T retract_of S  \<longleftrightarrow>  (\<exists>r. retraction S T r)"
    2.17  
    2.18  lemma retraction_idempotent: "retraction S T r \<Longrightarrow> x \<in> S \<Longrightarrow>  r (r x) = r x"
    2.19    unfolding retraction_def by auto
    2.20 @@ -399,7 +401,7 @@
    2.21    qed
    2.22  qed
    2.23  
    2.24 -subsection \<open>Absolute retracts, absolute neighbourhood retracts (ANR) and Euclidean neighbourhood retracts (ENR)\<close>
    2.25 +subsection \<open>Absolute Retracts, Absolute Neighbourhood Retracts and Euclidean Neighbourhood Retracts\<close>
    2.26  
    2.27  text \<open>Absolute retracts (AR), absolute neighbourhood retracts (ANR) and also Euclidean neighbourhood
    2.28  retracts (ENR). We define AR and ANR by specializing the standard definitions for a set to embedding
    2.29 @@ -410,19 +412,17 @@
    2.30  definitions, but we need to split them into two implications because of the lack of type
    2.31  quantifiers. Then ENR turns out to be equivalent to ANR plus local compactness."\<close>
    2.32  
    2.33 -definition AR :: "'a::topological_space set => bool"
    2.34 -  where
    2.35 -   "AR S \<equiv> \<forall>U. \<forall>S'::('a * real) set. S homeomorphic S' \<and> closedin (subtopology euclidean U) S'
    2.36 -                \<longrightarrow> S' retract_of U"
    2.37 -
    2.38 -definition ANR :: "'a::topological_space set => bool"
    2.39 -  where
    2.40 -   "ANR S \<equiv> \<forall>U. \<forall>S'::('a * real) set. S homeomorphic S' \<and> closedin (subtopology euclidean U) S'
    2.41 -                \<longrightarrow> (\<exists>T. openin (subtopology euclidean U) T \<and>
    2.42 -                        S' retract_of T)"
    2.43 -
    2.44 -definition ENR :: "'a::topological_space set => bool"
    2.45 -  where "ENR S \<equiv> \<exists>U. open U \<and> S retract_of U"
    2.46 +definition%important AR :: "'a::topological_space set \<Rightarrow> bool" where
    2.47 +"AR S \<equiv> \<forall>U. \<forall>S'::('a * real) set.
    2.48 +  S homeomorphic S' \<and> closedin (subtopology euclidean U) S' \<longrightarrow> S' retract_of U"
    2.49 +
    2.50 +definition%important ANR :: "'a::topological_space set \<Rightarrow> bool" where
    2.51 +"ANR S \<equiv> \<forall>U. \<forall>S'::('a * real) set.
    2.52 +  S homeomorphic S' \<and> closedin (subtopology euclidean U) S'
    2.53 +  \<longrightarrow> (\<exists>T. openin (subtopology euclidean U) T \<and> S' retract_of T)"
    2.54 +
    2.55 +definition%important ENR :: "'a::topological_space set \<Rightarrow> bool" where
    2.56 +"ENR S \<equiv> \<exists>U. open U \<and> S retract_of U"
    2.57  
    2.58  text \<open>First, show that we do indeed get the "usual" properties of ARs and ANRs.\<close>
    2.59  
     3.1 --- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Fri Dec 28 19:01:35 2018 +0100
     3.2 +++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Sat Dec 29 15:43:53 2018 +0100
     3.3 @@ -3134,7 +3134,7 @@
     3.4    moreover have "path_image p \<subseteq> (\<Union>c\<in>path_image p. ball c (ee c / 3))"
     3.5      using ee by auto
     3.6    ultimately have "\<exists>D \<subseteq> cover. finite D \<and> path_image p \<subseteq> \<Union>D"
     3.7 -    by (simp add: compact_eq_heine_borel cover_def)
     3.8 +    by (simp add: compact_eq_Heine_Borel cover_def)
     3.9    then obtain D where D: "D \<subseteq> cover" "finite D" "path_image p \<subseteq> \<Union>D"
    3.10      by blast
    3.11    then obtain k where k: "k \<subseteq> {0..1}" "finite k" and D_eq: "D = ((\<lambda>z. ball z (ee z / 3)) \<circ> p) ` k"
    3.12 @@ -6764,7 +6764,7 @@
    3.13    obtains g g' where "\<forall>x \<in> S. ((\<lambda>n. f n x) sums g x) \<and> ((\<lambda>n. f' n x) sums g' x) \<and> (g has_field_derivative g' x) (at x)"
    3.14  proof -
    3.15    obtain g where g: "uniform_limit S (\<lambda>n x. \<Sum>i<n. f i x) g sequentially"
    3.16 -    using weierstrass_m_test_ev [OF to_g h]  by force
    3.17 +    using Weierstrass_m_test_ev [OF to_g h]  by force
    3.18    have *: "\<exists>d>0. cball x d \<subseteq> S \<and> uniform_limit (cball x d) (\<lambda>n x. \<Sum>i<n. f i x) g sequentially"
    3.19           if "x \<in> S" for x
    3.20    proof -
     4.1 --- a/src/HOL/Analysis/Complex_Analysis_Basics.thy	Fri Dec 28 19:01:35 2018 +0100
     4.2 +++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy	Sat Dec 29 15:43:53 2018 +0100
     4.3 @@ -972,7 +972,7 @@
     4.4      shows  "sum f {0..n} = f 0 - f (Suc n) + sum (\<lambda>i. f (Suc i)) {0..n}"
     4.5  by (induct n) auto
     4.6  
     4.7 -lemma field_taylor:
     4.8 +lemma field_Taylor:
     4.9    assumes S: "convex S"
    4.10        and f: "\<And>i x. x \<in> S \<Longrightarrow> i \<le> n \<Longrightarrow> (f i has_field_derivative f (Suc i) x) (at x within S)"
    4.11        and B: "\<And>x. x \<in> S \<Longrightarrow> norm (f (Suc n) x) \<le> B"
    4.12 @@ -1066,7 +1066,7 @@
    4.13    finally show ?thesis .
    4.14  qed
    4.15  
    4.16 -lemma complex_taylor:
    4.17 +lemma complex_Taylor:
    4.18    assumes S: "convex S"
    4.19        and f: "\<And>i x. x \<in> S \<Longrightarrow> i \<le> n \<Longrightarrow> (f i has_field_derivative f (Suc i) x) (at x within S)"
    4.20        and B: "\<And>x. x \<in> S \<Longrightarrow> cmod (f (Suc n) x) \<le> B"
    4.21 @@ -1074,7 +1074,7 @@
    4.22        and z: "z \<in> S"
    4.23      shows "cmod(f 0 z - (\<Sum>i\<le>n. f i w * (z-w) ^ i / (fact i)))
    4.24            \<le> B * cmod(z - w)^(Suc n) / fact n"
    4.25 -  using assms by (rule field_taylor)
    4.26 +  using assms by (rule field_Taylor)
    4.27  
    4.28  
    4.29  text\<open>Something more like the traditional MVT for real components\<close>
    4.30 @@ -1099,7 +1099,7 @@
    4.31      done
    4.32  qed
    4.33  
    4.34 -lemma complex_taylor_mvt:
    4.35 +lemma complex_Taylor_mvt:
    4.36    assumes "\<And>i x. \<lbrakk>x \<in> closed_segment w z; i \<le> n\<rbrakk> \<Longrightarrow> ((f i) has_field_derivative f (Suc i) x) (at x)"
    4.37      shows "\<exists>u. u \<in> closed_segment w z \<and>
    4.38              Re (f 0 z) =
     5.1 --- a/src/HOL/Analysis/Complex_Transcendental.thy	Fri Dec 28 19:01:35 2018 +0100
     5.2 +++ b/src/HOL/Analysis/Complex_Transcendental.thy	Sat Dec 29 15:43:53 2018 +0100
     5.3 @@ -700,7 +700,7 @@
     5.4  lemma Taylor_exp_field:
     5.5    fixes z::"'a::{banach,real_normed_field}"
     5.6    shows "norm (exp z - (\<Sum>i\<le>n. z ^ i / fact i)) \<le> exp (norm z) * (norm z ^ Suc n) / fact n"
     5.7 -proof (rule field_taylor[of _ n "\<lambda>k. exp" "exp (norm z)" 0 z, simplified])
     5.8 +proof (rule field_Taylor[of _ n "\<lambda>k. exp" "exp (norm z)" 0 z, simplified])
     5.9    show "convex (closed_segment 0 z)"
    5.10      by (rule convex_closed_segment [of 0 z])
    5.11  next
    5.12 @@ -721,7 +721,7 @@
    5.13  
    5.14  lemma Taylor_exp:
    5.15    "norm(exp z - (\<Sum>k\<le>n. z ^ k / (fact k))) \<le> exp\<bar>Re z\<bar> * (norm z) ^ (Suc n) / (fact n)"
    5.16 -proof (rule complex_taylor [of _ n "\<lambda>k. exp" "exp\<bar>Re z\<bar>" 0 z, simplified])
    5.17 +proof (rule complex_Taylor [of _ n "\<lambda>k. exp" "exp\<bar>Re z\<bar>" 0 z, simplified])
    5.18    show "convex (closed_segment 0 z)"
    5.19      by (rule convex_closed_segment [of 0 z])
    5.20  next
    5.21 @@ -778,7 +778,7 @@
    5.22    have *: "cmod (sin z -
    5.23                   (\<Sum>i\<le>n. (-1) ^ (i div 2) * (if even i then sin 0 else cos 0) * z ^ i / (fact i)))
    5.24             \<le> exp \<bar>Im z\<bar> * cmod z ^ Suc n / (fact n)"
    5.25 -  proof (rule complex_taylor [of "closed_segment 0 z" n
    5.26 +  proof (rule complex_Taylor [of "closed_segment 0 z" n
    5.27                                   "\<lambda>k x. (-1)^(k div 2) * (if even k then sin x else cos x)"
    5.28                                   "exp\<bar>Im z\<bar>" 0 z,  simplified])
    5.29      fix k x
    5.30 @@ -812,7 +812,7 @@
    5.31    have *: "cmod (cos z -
    5.32                   (\<Sum>i\<le>n. (-1) ^ (Suc i div 2) * (if even i then cos 0 else sin 0) * z ^ i / (fact i)))
    5.33             \<le> exp \<bar>Im z\<bar> * cmod z ^ Suc n / (fact n)"
    5.34 -  proof (rule complex_taylor [of "closed_segment 0 z" n "\<lambda>k x. (-1)^(Suc k div 2) * (if even k then cos x else sin x)" "exp\<bar>Im z\<bar>" 0 z,
    5.35 +  proof (rule complex_Taylor [of "closed_segment 0 z" n "\<lambda>k x. (-1)^(Suc k div 2) * (if even k then cos x else sin x)" "exp\<bar>Im z\<bar>" 0 z,
    5.36  simplified])
    5.37      fix k x
    5.38      assume "x \<in> closed_segment 0 z" "k \<le> n"
    5.39 @@ -2567,7 +2567,7 @@
    5.40      using e  by (simp add: field_simps)
    5.41    then have "\<exists>xo>0. \<forall>x\<ge>xo. x / e < exp (Re s * x)"
    5.42      using assms
    5.43 -    by (force intro: less_le_trans [OF _ exp_lower_taylor_quadratic])
    5.44 +    by (force intro: less_le_trans [OF _ exp_lower_Taylor_quadratic])
    5.45    then obtain xo where "xo > 0" and xo: "\<And>x. x \<ge> xo \<Longrightarrow> x < e * exp (Re s * x)"
    5.46      using e  by (auto simp: field_simps)
    5.47    have "norm (Ln (of_nat n) / of_nat n powr s) < e" if "n \<ge> nat \<lceil>exp xo\<rceil>" for n
     6.1 --- a/src/HOL/Analysis/Connected.thy	Fri Dec 28 19:01:35 2018 +0100
     6.2 +++ b/src/HOL/Analysis/Connected.thy	Sat Dec 29 15:43:53 2018 +0100
     6.3 @@ -5118,7 +5118,7 @@
     6.4          \<Longrightarrow> S \<inter> \<Inter>\<F> \<noteq> {}"
     6.5  by (metis Inf_greatest closed_imp_fip compact_eq_bounded_closed empty_subsetI finite.emptyI inf.orderE)
     6.6  
     6.7 -lemma closed_fip_heine_borel:
     6.8 +lemma closed_fip_Heine_Borel:
     6.9    fixes \<F> :: "'a::heine_borel set set"
    6.10    assumes "closed S" "T \<in> \<F>" "bounded T"
    6.11        and "\<And>T. T \<in> \<F> \<Longrightarrow> closed T"
    6.12 @@ -5130,12 +5130,12 @@
    6.13    then show ?thesis by simp
    6.14  qed
    6.15  
    6.16 -lemma compact_fip_heine_borel:
    6.17 +lemma compact_fip_Heine_Borel:
    6.18    fixes \<F> :: "'a::heine_borel set set"
    6.19    assumes clof: "\<And>T. T \<in> \<F> \<Longrightarrow> compact T"
    6.20        and none: "\<And>\<F>'. \<lbrakk>finite \<F>'; \<F>' \<subseteq> \<F>\<rbrakk> \<Longrightarrow> \<Inter>\<F>' \<noteq> {}"
    6.21      shows "\<Inter>\<F> \<noteq> {}"
    6.22 -by (metis InterI all_not_in_conv clof closed_fip_heine_borel compact_eq_bounded_closed none)
    6.23 +by (metis InterI all_not_in_conv clof closed_fip_Heine_Borel compact_eq_bounded_closed none)
    6.24  
    6.25  lemma compact_sequence_with_limit:
    6.26    fixes f :: "nat \<Rightarrow> 'a::heine_borel"
     7.1 --- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Fri Dec 28 19:01:35 2018 +0100
     7.2 +++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Sat Dec 29 15:43:53 2018 +0100
     7.3 @@ -5757,7 +5757,7 @@
     7.4  
     7.5  text "Formalized by Lars Schewe."
     7.6  
     7.7 -lemma radon_ex_lemma:
     7.8 +lemma Radon_ex_lemma:
     7.9    assumes "finite c" "affine_dependent c"
    7.10    shows "\<exists>u. sum u c = 0 \<and> (\<exists>v\<in>c. u v \<noteq> 0) \<and> sum (\<lambda>v. u v *\<^sub>R v) c = 0"
    7.11  proof -
    7.12 @@ -5772,7 +5772,7 @@
    7.13      done
    7.14  qed
    7.15  
    7.16 -lemma radon_s_lemma:
    7.17 +lemma Radon_s_lemma:
    7.18    assumes "finite s"
    7.19      and "sum f s = (0::real)"
    7.20    shows "sum f {x\<in>s. 0 < f x} = - sum f {x\<in>s. f x < 0}"
    7.21 @@ -5786,7 +5786,7 @@
    7.22      by assumption
    7.23  qed
    7.24  
    7.25 -lemma radon_v_lemma:
    7.26 +lemma Radon_v_lemma:
    7.27    assumes "finite s"
    7.28      and "sum f s = 0"
    7.29      and "\<forall>x. g x = (0::real) \<longrightarrow> f x = (0::'a::euclidean_space)"
    7.30 @@ -5802,12 +5802,12 @@
    7.31      done
    7.32  qed
    7.33  
    7.34 -lemma radon_partition:
    7.35 +lemma Radon_partition:
    7.36    assumes "finite c" "affine_dependent c"
    7.37    shows "\<exists>m p. m \<inter> p = {} \<and> m \<union> p = c \<and> (convex hull m) \<inter> (convex hull p) \<noteq> {}"
    7.38  proof -
    7.39    obtain u v where uv: "sum u c = 0" "v\<in>c" "u v \<noteq> 0"  "(\<Sum>v\<in>c. u v *\<^sub>R v) = 0"
    7.40 -    using radon_ex_lemma[OF assms] by auto
    7.41 +    using Radon_ex_lemma[OF assms] by auto
    7.42    have fin: "finite {x \<in> c. 0 < u x}" "finite {x \<in> c. 0 > u x}"
    7.43      using assms(1) by auto
    7.44    define z  where "z = inverse (sum u {x\<in>c. u x > 0}) *\<^sub>R sum (\<lambda>x. u x *\<^sub>R x) {x\<in>c. u x > 0}"
    7.45 @@ -5879,7 +5879,7 @@
    7.46      done
    7.47  qed
    7.48  
    7.49 -theorem radon:
    7.50 +theorem Radon:
    7.51    assumes "affine_dependent c"
    7.52    obtains m p where "m \<subseteq> c" "p \<subseteq> c" "m \<inter> p = {}" "(convex hull m) \<inter> (convex hull p) \<noteq> {}"
    7.53  proof -
    7.54 @@ -5889,7 +5889,7 @@
    7.55      by blast
    7.56    then have *: "finite s" "affine_dependent s" and s: "s \<subseteq> c"
    7.57      unfolding affine_dependent_explicit by auto
    7.58 -  from radon_partition[OF *]
    7.59 +  from Radon_partition[OF *]
    7.60    obtain m p where "m \<inter> p = {}" "m \<union> p = s" "convex hull m \<inter> convex hull p \<noteq> {}"
    7.61      by blast
    7.62    then show ?thesis
    7.63 @@ -5902,7 +5902,7 @@
    7.64  
    7.65  subsection \<open>Helly's theorem\<close>
    7.66  
    7.67 -lemma helly_induct:
    7.68 +lemma Helly_induct:
    7.69    fixes f :: "'a::euclidean_space set set"
    7.70    assumes "card f = n"
    7.71      and "n \<ge> DIM('a) + 1"
    7.72 @@ -5947,7 +5947,7 @@
    7.73      next
    7.74        case True
    7.75        then obtain m p where mp: "m \<inter> p = {}" "m \<union> p = X ` f" "convex hull m \<inter> convex hull p \<noteq> {}"
    7.76 -        using radon_partition[of "X ` f"] and affine_dependent_biggerset[of "X ` f"]
    7.77 +        using Radon_partition[of "X ` f"] and affine_dependent_biggerset[of "X ` f"]
    7.78          unfolding card_image[OF True] and \<open>card f = Suc n\<close>
    7.79          using Suc(3) \<open>finite f\<close> and False
    7.80          by auto
    7.81 @@ -5973,12 +5973,12 @@
    7.82    qed 
    7.83  qed
    7.84  
    7.85 -theorem helly:
    7.86 +theorem Helly:
    7.87    fixes f :: "'a::euclidean_space set set"
    7.88    assumes "card f \<ge> DIM('a) + 1" "\<forall>s\<in>f. convex s"
    7.89      and "\<And>t. \<lbrakk>t\<subseteq>f; card t = DIM('a) + 1\<rbrakk> \<Longrightarrow> \<Inter>t \<noteq> {}"
    7.90    shows "\<Inter>f \<noteq> {}"
    7.91 -  apply (rule helly_induct)
    7.92 +  apply (rule Helly_induct)
    7.93    using assms
    7.94    apply auto
    7.95    done
     8.1 --- a/src/HOL/Analysis/Derivative.thy	Fri Dec 28 19:01:35 2018 +0100
     8.2 +++ b/src/HOL/Analysis/Derivative.thy	Sat Dec 29 15:43:53 2018 +0100
     8.3 @@ -2325,7 +2325,7 @@
     8.4        \<forall>x\<in>T \<inter> {t - 1<..<t + 1}. norm (?e n x) \<le> norm (A ^ (n + 1) /\<^sub>R fact (n + 1))"
     8.5      by (auto simp: divide_simps power_abs intro!: mult_left_le_one_le power_le_one eventuallyI)
     8.6    then have "uniform_limit (T \<inter> {t - 1<..<t + 1}) (\<lambda>n x. \<Sum>i<n. ?e i x) (\<lambda>x. \<Sum>i. ?e i x) sequentially"
     8.7 -    by (rule weierstrass_m_test_ev) (intro summable_ignore_initial_segment summable_norm_exp)
     8.8 +    by (rule Weierstrass_m_test_ev) (intro summable_ignore_initial_segment summable_norm_exp)
     8.9    moreover
    8.10    have "\<forall>\<^sub>F x in sequentially. x > 0"
    8.11      by (metis eventually_gt_at_top)
    8.12 @@ -2333,7 +2333,7 @@
    8.13      "\<forall>\<^sub>F n in sequentially. ((\<lambda>x. \<Sum>i<n. ?e i x) \<longlongrightarrow> A) ?F"
    8.14      by eventually_elim
    8.15        (auto intro!: tendsto_eq_intros
    8.16 -        simp: power_0_left if_distrib if_distribR sum.delta
    8.17 +        simp: power_0_left if_distrib if_distribR
    8.18          cong: if_cong)
    8.19    ultimately
    8.20    have [tendsto_intros]: "((\<lambda>x. \<Sum>i. ?e i x) \<longlongrightarrow> A) ?F"
     9.1 --- a/src/HOL/Analysis/Elementary_Topology.thy	Fri Dec 28 19:01:35 2018 +0100
     9.2 +++ b/src/HOL/Analysis/Elementary_Topology.thy	Sat Dec 29 15:43:53 2018 +0100
     9.3 @@ -3090,7 +3090,7 @@
     9.4  
     9.5  subsubsection \<open>Bolzano-Weierstrass property\<close>
     9.6  
     9.7 -proposition heine_borel_imp_bolzano_weierstrass:
     9.8 +proposition Heine_Borel_imp_Bolzano_Weierstrass:
     9.9    assumes "compact s"
    9.10      and "infinite t"
    9.11      and "t \<subseteq> s"
    9.12 @@ -3102,7 +3102,7 @@
    9.13      using bchoice[of s "\<lambda> x T. x \<in> T \<and> open T \<and> (\<forall>y\<in>t. y \<in> T \<longrightarrow> y = x)"]
    9.14      by auto
    9.15    obtain g where g: "g \<subseteq> {t. \<exists>x. x \<in> s \<and> t = f x}" "finite g" "s \<subseteq> \<Union>g"
    9.16 -    using assms(1)[unfolded compact_eq_heine_borel, THEN spec[where x="{t. \<exists>x. x\<in>s \<and> t = f x}"]]
    9.17 +    using assms(1)[unfolded compact_eq_Heine_Borel, THEN spec[where x="{t. \<exists>x. x\<in>s \<and> t = f x}"]]
    9.18      using f by auto
    9.19    from g(1,3) have g':"\<forall>x\<in>g. \<exists>xa \<in> s. x = f xa"
    9.20      by auto
    9.21 @@ -3336,7 +3336,7 @@
    9.22      by simp
    9.23  qed
    9.24  
    9.25 -lemma bolzano_weierstrass_imp_closed:
    9.26 +lemma Bolzano_Weierstrass_imp_closed:
    9.27    fixes s :: "'a::{first_countable_topology,t2_space} set"
    9.28    assumes "\<forall>t. infinite t \<and> t \<subseteq> s --> (\<exists>x \<in> s. x islimpt t)"
    9.29    shows "closed s"
    9.30 @@ -3386,10 +3386,10 @@
    9.31    fix f
    9.32    assume *: "Ball f open" "s \<union> t \<subseteq> \<Union>f"
    9.33    from * \<open>compact s\<close> obtain s' where "s' \<subseteq> f \<and> finite s' \<and> s \<subseteq> \<Union>s'"
    9.34 -    unfolding compact_eq_heine_borel by (auto elim!: allE[of _ f])
    9.35 +    unfolding compact_eq_Heine_Borel by (auto elim!: allE[of _ f])
    9.36    moreover
    9.37    from * \<open>compact t\<close> obtain t' where "t' \<subseteq> f \<and> finite t' \<and> t \<subseteq> \<Union>t'"
    9.38 -    unfolding compact_eq_heine_borel by (auto elim!: allE[of _ f])
    9.39 +    unfolding compact_eq_Heine_Borel by (auto elim!: allE[of _ f])
    9.40    ultimately show "\<exists>f'\<subseteq>f. finite f' \<and> s \<union> t \<subseteq> \<Union>f'"
    9.41      by (auto intro!: exI[of _ "s' \<union> t'"])
    9.42  qed
    9.43 @@ -3416,7 +3416,7 @@
    9.44    using assms by (intro compact_Int_closed compact_imp_closed)
    9.45  
    9.46  lemma compact_sing [simp]: "compact {a}"
    9.47 -  unfolding compact_eq_heine_borel by auto
    9.48 +  unfolding compact_eq_Heine_Borel by auto
    9.49  
    9.50  lemma compact_insert [simp]:
    9.51    assumes "compact s"
    9.52 @@ -3571,7 +3571,7 @@
    9.53    using assms unfolding countably_compact_def by metis
    9.54  
    9.55  lemma compact_imp_countably_compact: "compact U \<Longrightarrow> countably_compact U"
    9.56 -  by (auto simp: compact_eq_heine_borel countably_compact_def)
    9.57 +  by (auto simp: compact_eq_Heine_Borel countably_compact_def)
    9.58  
    9.59  lemma countably_compact_imp_compact:
    9.60    assumes "countably_compact U"
    9.61 @@ -3579,7 +3579,7 @@
    9.62      and basis: "\<And>T x. open T \<Longrightarrow> x \<in> T \<Longrightarrow> x \<in> U \<Longrightarrow> \<exists>b\<in>B. x \<in> b \<and> b \<inter> U \<subseteq> T"
    9.63    shows "compact U"
    9.64    using \<open>countably_compact U\<close>
    9.65 -  unfolding compact_eq_heine_borel countably_compact_def
    9.66 +  unfolding compact_eq_Heine_Borel countably_compact_def
    9.67  proof safe
    9.68    fix A
    9.69    assume A: "\<forall>a\<in>A. open a" "U \<subseteq> \<Union>A"
    9.70 @@ -3886,7 +3886,7 @@
    9.71    shows "seq_compact U \<longleftrightarrow> compact U"
    9.72    using seq_compact_eq_countably_compact countably_compact_eq_compact by blast
    9.73  
    9.74 -proposition bolzano_weierstrass_imp_seq_compact:
    9.75 +proposition Bolzano_Weierstrass_imp_seq_compact:
    9.76    fixes s :: "'a::{t1_space, first_countable_topology} set"
    9.77    shows "\<forall>t. infinite t \<and> t \<subseteq> s \<longrightarrow> (\<exists>x \<in> s. x islimpt t) \<Longrightarrow> seq_compact s"
    9.78    by (rule countable_acc_point_imp_seq_compact) (metis islimpt_eq_acc_point)
    9.79 @@ -3929,7 +3929,7 @@
    9.80  
    9.81  subsubsection\<open>Heine-Borel theorem\<close>
    9.82  
    9.83 -proposition seq_compact_imp_heine_borel:
    9.84 +proposition seq_compact_imp_Heine_Borel:
    9.85    fixes s :: "'a :: metric_space set"
    9.86    assumes "seq_compact s"
    9.87    shows "compact s"
    9.88 @@ -3976,7 +3976,7 @@
    9.89  
    9.90  proposition compact_eq_seq_compact_metric:
    9.91    "compact (s :: 'a::metric_space set) \<longleftrightarrow> seq_compact s"
    9.92 -  using compact_imp_seq_compact seq_compact_imp_heine_borel by blast
    9.93 +  using compact_imp_seq_compact seq_compact_imp_Heine_Borel by blast
    9.94  
    9.95  proposition compact_def: \<comment> \<open>this is the definition of compactness in HOL Light\<close>
    9.96    "compact (S :: 'a::metric_space set) \<longleftrightarrow>
    9.97 @@ -3985,23 +3985,23 @@
    9.98  
    9.99  subsubsection \<open>Complete the chain of compactness variants\<close>
   9.100  
   9.101 -proposition compact_eq_bolzano_weierstrass:
   9.102 +proposition compact_eq_Bolzano_Weierstrass:
   9.103    fixes s :: "'a::metric_space set"
   9.104    shows "compact s \<longleftrightarrow> (\<forall>t. infinite t \<and> t \<subseteq> s --> (\<exists>x \<in> s. x islimpt t))"
   9.105    (is "?lhs = ?rhs")
   9.106  proof
   9.107    assume ?lhs
   9.108    then show ?rhs
   9.109 -    using heine_borel_imp_bolzano_weierstrass[of s] by auto
   9.110 +    using Heine_Borel_imp_Bolzano_Weierstrass[of s] by auto
   9.111  next
   9.112    assume ?rhs
   9.113    then show ?lhs
   9.114 -    unfolding compact_eq_seq_compact_metric by (rule bolzano_weierstrass_imp_seq_compact)
   9.115 +    unfolding compact_eq_seq_compact_metric by (rule Bolzano_Weierstrass_imp_seq_compact)
   9.116  qed
   9.117  
   9.118 -proposition bolzano_weierstrass_imp_bounded:
   9.119 +proposition Bolzano_Weierstrass_imp_bounded:
   9.120    "\<forall>t. infinite t \<and> t \<subseteq> s \<longrightarrow> (\<exists>x \<in> s. x islimpt t) \<Longrightarrow> bounded s"
   9.121 -  using compact_imp_bounded unfolding compact_eq_bolzano_weierstrass .
   9.122 +  using compact_imp_bounded unfolding compact_eq_Bolzano_Weierstrass .
   9.123  
   9.124  
   9.125  subsection \<open>Metric spaces with the Heine-Borel property\<close>
    10.1 --- a/src/HOL/Analysis/Gamma_Function.thy	Fri Dec 28 19:01:35 2018 +0100
    10.2 +++ b/src/HOL/Analysis/Gamma_Function.thy	Sat Dec 29 15:43:53 2018 +0100
    10.3 @@ -552,7 +552,7 @@
    10.4    shows "uniformly_convergent_on (ball z d)
    10.5              (\<lambda>k z. \<Sum>i<k. inverse (of_nat (Suc i)) - inverse (z + of_nat (Suc i)))"
    10.6             (is "uniformly_convergent_on _ (\<lambda>k z. \<Sum>i<k. ?f i z)")
    10.7 -proof (rule weierstrass_m_test'_ev)
    10.8 +proof (rule Weierstrass_m_test'_ev)
    10.9    {
   10.10      fix t assume t: "t \<in> ball z d"
   10.11      have "norm z = norm (t + (z - t))" by simp
   10.12 @@ -665,7 +665,7 @@
   10.13    fixes z :: "'a :: {real_normed_field,banach}"
   10.14    assumes z: "z \<noteq> 0" and n: "n \<ge> 2"
   10.15    shows "uniformly_convergent_on (ball z d) (\<lambda>k z. \<Sum>i<k. inverse ((z + of_nat i)^n))"
   10.16 -proof (rule weierstrass_m_test'_ev)
   10.17 +proof (rule Weierstrass_m_test'_ev)
   10.18    define e where "e = (1 + d / norm z)"
   10.19    define m where "m = nat \<lceil>norm z * e\<rceil>"
   10.20    {
   10.21 @@ -2528,29 +2528,29 @@
   10.22  
   10.23  subsubsection \<open>Weierstrass form\<close>
   10.24  
   10.25 -definition Gamma_series_weierstrass :: "'a :: {banach,real_normed_field} \<Rightarrow> nat \<Rightarrow> 'a" where
   10.26 -  "Gamma_series_weierstrass z n =
   10.27 +definition Gamma_series_Weierstrass :: "'a :: {banach,real_normed_field} \<Rightarrow> nat \<Rightarrow> 'a" where
   10.28 +  "Gamma_series_Weierstrass z n =
   10.29       exp (-euler_mascheroni * z) / z * (\<Prod>k=1..n. exp (z / of_nat k) / (1 + z / of_nat k))"
   10.30  
   10.31  definition%unimportant
   10.32 -  rGamma_series_weierstrass :: "'a :: {banach,real_normed_field} \<Rightarrow> nat \<Rightarrow> 'a" where
   10.33 -  "rGamma_series_weierstrass z n =
   10.34 +  rGamma_series_Weierstrass :: "'a :: {banach,real_normed_field} \<Rightarrow> nat \<Rightarrow> 'a" where
   10.35 +  "rGamma_series_Weierstrass z n =
   10.36       exp (euler_mascheroni * z) * z * (\<Prod>k=1..n. (1 + z / of_nat k) * exp (-z / of_nat k))"
   10.37  
   10.38 -lemma Gamma_series_weierstrass_nonpos_Ints:
   10.39 -  "eventually (\<lambda>k. Gamma_series_weierstrass (- of_nat n) k = 0) sequentially"
   10.40 -  using eventually_ge_at_top[of n] by eventually_elim (auto simp: Gamma_series_weierstrass_def)
   10.41 -
   10.42 -lemma rGamma_series_weierstrass_nonpos_Ints:
   10.43 -  "eventually (\<lambda>k. rGamma_series_weierstrass (- of_nat n) k = 0) sequentially"
   10.44 -  using eventually_ge_at_top[of n] by eventually_elim (auto simp: rGamma_series_weierstrass_def)
   10.45 -
   10.46 -theorem Gamma_weierstrass_complex: "Gamma_series_weierstrass z \<longlonglongrightarrow> Gamma (z :: complex)"
   10.47 +lemma Gamma_series_Weierstrass_nonpos_Ints:
   10.48 +  "eventually (\<lambda>k. Gamma_series_Weierstrass (- of_nat n) k = 0) sequentially"
   10.49 +  using eventually_ge_at_top[of n] by eventually_elim (auto simp: Gamma_series_Weierstrass_def)
   10.50 +
   10.51 +lemma rGamma_series_Weierstrass_nonpos_Ints:
   10.52 +  "eventually (\<lambda>k. rGamma_series_Weierstrass (- of_nat n) k = 0) sequentially"
   10.53 +  using eventually_ge_at_top[of n] by eventually_elim (auto simp: rGamma_series_Weierstrass_def)
   10.54 +
   10.55 +theorem Gamma_Weierstrass_complex: "Gamma_series_Weierstrass z \<longlonglongrightarrow> Gamma (z :: complex)"
   10.56  proof (cases "z \<in> \<int>\<^sub>\<le>\<^sub>0")
   10.57    case True
   10.58    then obtain n where "z = - of_nat n" by (elim nonpos_Ints_cases')
   10.59 -  also from True have "Gamma_series_weierstrass \<dots> \<longlonglongrightarrow> Gamma z"
   10.60 -    by (simp add: tendsto_cong[OF Gamma_series_weierstrass_nonpos_Ints] Gamma_nonpos_Int)
   10.61 +  also from True have "Gamma_series_Weierstrass \<dots> \<longlonglongrightarrow> Gamma z"
   10.62 +    by (simp add: tendsto_cong[OF Gamma_series_Weierstrass_nonpos_Ints] Gamma_nonpos_Int)
   10.63    finally show ?thesis .
   10.64  next
   10.65    case False
   10.66 @@ -2565,32 +2565,32 @@
   10.67    from tendsto_exp[OF this] False z have "?f \<longlonglongrightarrow> z * exp (euler_mascheroni * z) * Gamma z"
   10.68      by (simp add: exp_add exp_sum exp_diff mult_ac Gamma_complex_altdef A)
   10.69    from tendsto_mult[OF tendsto_const[of "exp (-euler_mascheroni * z) / z"] this] z
   10.70 -    show "Gamma_series_weierstrass z \<longlonglongrightarrow> Gamma z"
   10.71 -    by (simp add: exp_minus divide_simps Gamma_series_weierstrass_def [abs_def])
   10.72 +    show "Gamma_series_Weierstrass z \<longlonglongrightarrow> Gamma z"
   10.73 +    by (simp add: exp_minus divide_simps Gamma_series_Weierstrass_def [abs_def])
   10.74  qed
   10.75  
   10.76  lemma tendsto_complex_of_real_iff: "((\<lambda>x. complex_of_real (f x)) \<longlongrightarrow> of_real c) F = (f \<longlongrightarrow> c) F"
   10.77    by (rule tendsto_of_real_iff)
   10.78  
   10.79 -lemma Gamma_weierstrass_real: "Gamma_series_weierstrass x \<longlonglongrightarrow> Gamma (x :: real)"
   10.80 -  using Gamma_weierstrass_complex[of "of_real x"] unfolding Gamma_series_weierstrass_def[abs_def]
   10.81 +lemma Gamma_Weierstrass_real: "Gamma_series_Weierstrass x \<longlonglongrightarrow> Gamma (x :: real)"
   10.82 +  using Gamma_Weierstrass_complex[of "of_real x"] unfolding Gamma_series_Weierstrass_def[abs_def]
   10.83    by (subst tendsto_complex_of_real_iff [symmetric])
   10.84       (simp_all add: exp_of_real[symmetric] Gamma_complex_of_real)
   10.85  
   10.86 -lemma rGamma_weierstrass_complex: "rGamma_series_weierstrass z \<longlonglongrightarrow> rGamma (z :: complex)"
   10.87 +lemma rGamma_Weierstrass_complex: "rGamma_series_Weierstrass z \<longlonglongrightarrow> rGamma (z :: complex)"
   10.88  proof (cases "z \<in> \<int>\<^sub>\<le>\<^sub>0")
   10.89    case True
   10.90    then obtain n where "z = - of_nat n" by (elim nonpos_Ints_cases')
   10.91 -  also from True have "rGamma_series_weierstrass \<dots> \<longlonglongrightarrow> rGamma z"
   10.92 -    by (simp add: tendsto_cong[OF rGamma_series_weierstrass_nonpos_Ints] rGamma_nonpos_Int)
   10.93 +  also from True have "rGamma_series_Weierstrass \<dots> \<longlonglongrightarrow> rGamma z"
   10.94 +    by (simp add: tendsto_cong[OF rGamma_series_Weierstrass_nonpos_Ints] rGamma_nonpos_Int)
   10.95    finally show ?thesis .
   10.96  next
   10.97    case False
   10.98 -  have "rGamma_series_weierstrass z = (\<lambda>n. inverse (Gamma_series_weierstrass z n))"
   10.99 -    by (simp add: rGamma_series_weierstrass_def[abs_def] Gamma_series_weierstrass_def
  10.100 +  have "rGamma_series_Weierstrass z = (\<lambda>n. inverse (Gamma_series_Weierstrass z n))"
  10.101 +    by (simp add: rGamma_series_Weierstrass_def[abs_def] Gamma_series_Weierstrass_def
  10.102                    exp_minus divide_inverse prod_inversef[symmetric] mult_ac)
  10.103    also from False have "\<dots> \<longlonglongrightarrow> inverse (Gamma z)"
  10.104 -    by (intro tendsto_intros Gamma_weierstrass_complex) (simp add: Gamma_eq_zero_iff)
  10.105 +    by (intro tendsto_intros Gamma_Weierstrass_complex) (simp add: Gamma_eq_zero_iff)
  10.106    finally show ?thesis by (simp add: Gamma_def)
  10.107  qed
  10.108  
  10.109 @@ -3175,17 +3175,17 @@
  10.110    fixes z :: complex
  10.111    shows "(\<lambda>n. of_real pi * z * (\<Prod>k=1..n. 1 - z^2 / of_nat k^2)) \<longlonglongrightarrow> sin (of_real pi * z)"
  10.112  proof -
  10.113 -  let ?f = "rGamma_series_weierstrass"
  10.114 +  let ?f = "rGamma_series_Weierstrass"
  10.115    have "(\<lambda>n. (- of_real pi * inverse z) * (?f z n * ?f (- z) n))
  10.116              \<longlonglongrightarrow> (- of_real pi * inverse z) * (rGamma z * rGamma (- z))"
  10.117 -    by (intro tendsto_intros rGamma_weierstrass_complex)
  10.118 +    by (intro tendsto_intros rGamma_Weierstrass_complex)
  10.119    also have "(\<lambda>n. (- of_real pi * inverse z) * (?f z n * ?f (-z) n)) =
  10.120                      (\<lambda>n. of_real pi * z * (\<Prod>k=1..n. 1 - z^2 / of_nat k ^ 2))"
  10.121    proof
  10.122      fix n :: nat
  10.123      have "(- of_real pi * inverse z) * (?f z n * ?f (-z) n) =
  10.124                of_real pi * z * (\<Prod>k=1..n. (of_nat k - z) * (of_nat k + z) / of_nat k ^ 2)"
  10.125 -      by (simp add: rGamma_series_weierstrass_def mult_ac exp_minus
  10.126 +      by (simp add: rGamma_series_Weierstrass_def mult_ac exp_minus
  10.127                      divide_simps prod.distrib[symmetric] power2_eq_square)
  10.128      also have "(\<Prod>k=1..n. (of_nat k - z) * (of_nat k + z) / of_nat k ^ 2) =
  10.129                   (\<Prod>k=1..n. 1 - z^2 / of_nat k ^ 2)"
  10.130 @@ -3257,7 +3257,7 @@
  10.131    have "continuous_on (ball 0 1) f"
  10.132    proof (rule uniform_limit_theorem; (intro always_eventually allI)?)
  10.133      show "uniform_limit (ball 0 1) (\<lambda>n x. \<Sum>k<n. P x k / of_nat (Suc k)^2) f sequentially"
  10.134 -    proof (unfold f_def, rule weierstrass_m_test)
  10.135 +    proof (unfold f_def, rule Weierstrass_m_test)
  10.136        fix n :: nat and x :: real assume x: "x \<in> ball 0 1"
  10.137        {
  10.138          fix k :: nat assume k: "k \<ge> 1"
    11.1 --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Fri Dec 28 19:01:35 2018 +0100
    11.2 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Sat Dec 29 15:43:53 2018 +0100
    11.3 @@ -2806,11 +2806,11 @@
    11.4      (Df m has_vector_derivative Df (Suc m) t) (at t within {a..b})"
    11.5    and ivl: "a \<le> b"
    11.6    defines "i \<equiv> \<lambda>x. ((b - x) ^ (p - 1) / fact (p - 1)) *\<^sub>R Df p x"
    11.7 -  shows taylor_has_integral:
    11.8 +  shows Taylor_has_integral:
    11.9      "(i has_integral f b - (\<Sum>i<p. ((b-a) ^ i / fact i) *\<^sub>R Df i a)) {a..b}"
   11.10 -  and taylor_integral:
   11.11 +  and Taylor_integral:
   11.12      "f b = (\<Sum>i<p. ((b-a) ^ i / fact i) *\<^sub>R Df i a) + integral {a..b} i"
   11.13 -  and taylor_integrable:
   11.14 +  and Taylor_integrable:
   11.15      "i integrable_on {a..b}"
   11.16  proof goal_cases
   11.17    case 1
    12.1 --- a/src/HOL/Analysis/Infinite_Products.thy	Fri Dec 28 19:01:35 2018 +0100
    12.2 +++ b/src/HOL/Analysis/Infinite_Products.thy	Sat Dec 29 15:43:53 2018 +0100
    12.3 @@ -254,7 +254,7 @@
    12.4      by (auto simp: abs_convergent_prod_def intro!: convergent_prod_imp_convergent)
    12.5  qed (auto intro: abs_convergent_prodI)
    12.6  
    12.7 -lemma weierstrass_prod_ineq:
    12.8 +lemma Weierstrass_prod_ineq:
    12.9    fixes f :: "'a \<Rightarrow> real" 
   12.10    assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<in> {0..1}"
   12.11    shows   "1 - sum f A \<le> (\<Prod>x\<in>A. 1 - f x)"
   12.12 @@ -576,7 +576,7 @@
   12.13        proof (rule tendsto_le)
   12.14          show "eventually (\<lambda>n. 1 - (\<Sum>k\<le>n. norm (f (k+M+N) - 1)) \<le> 
   12.15                                  (\<Prod>k\<le>n. 1 - norm (f (k+M+N) - 1))) at_top"
   12.16 -          using M by (intro always_eventually allI weierstrass_prod_ineq) (auto intro: less_imp_le)
   12.17 +          using M by (intro always_eventually allI Weierstrass_prod_ineq) (auto intro: less_imp_le)
   12.18          show "(\<lambda>n. \<Prod>k\<le>n. 1 - norm (f (k+M+N) - 1)) \<longlonglongrightarrow> 0" by fact
   12.19          show "(\<lambda>n. 1 - (\<Sum>k\<le>n. norm (f (k + M + N) - 1)))
   12.20                    \<longlonglongrightarrow> 1 - (\<Sum>i. norm (f (i + M + N) - 1))"
    13.1 --- a/src/HOL/Analysis/Starlike.thy	Fri Dec 28 19:01:35 2018 +0100
    13.2 +++ b/src/HOL/Analysis/Starlike.thy	Sat Dec 29 15:43:53 2018 +0100
    13.3 @@ -5261,7 +5261,7 @@
    13.4      qed
    13.5      have "\<Inter>{{a. a \<in> K \<and> f a \<in> insert y (range (\<lambda>i. f(X(n + i))))} |n. n \<in> UNIV}
    13.6                 \<noteq> {}"
    13.7 -      apply (rule compact_fip_heine_borel)
    13.8 +      apply (rule compact_fip_Heine_Borel)
    13.9         using comf apply force
   13.10        using ne  apply (simp add: subset_iff del: insert_iff)
   13.11        done
    14.1 --- a/src/HOL/Analysis/Uniform_Limit.thy	Fri Dec 28 19:01:35 2018 +0100
    14.2 +++ b/src/HOL/Analysis/Uniform_Limit.thy	Sat Dec 29 15:43:53 2018 +0100
    14.3 @@ -319,7 +319,7 @@
    14.4  
    14.5  subsection \<open>Weierstrass M-Test\<close>
    14.6  
    14.7 -proposition weierstrass_m_test_ev:
    14.8 +proposition Weierstrass_m_test_ev:
    14.9  fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: banach"
   14.10  assumes "eventually (\<lambda>n. \<forall>x\<in>A. norm (f n x) \<le> M n) sequentially"
   14.11  assumes "summable M"
   14.12 @@ -375,28 +375,28 @@
   14.13      using le eventually_sequentially by auto
   14.14    show ?thesis
   14.15      apply (rule_tac x="(\<lambda>x. \<Sum>i. f x i)" in exI)
   14.16 -    apply (metis (no_types, lifting) eventually_sequentially uniform_limitD [OF weierstrass_m_test_ev [OF 1 g]])
   14.17 +    apply (metis (no_types, lifting) eventually_sequentially uniform_limitD [OF Weierstrass_m_test_ev [OF 1 g]])
   14.18      done
   14.19  qed
   14.20  
   14.21 -corollary%unimportant weierstrass_m_test:
   14.22 +corollary%unimportant Weierstrass_m_test:
   14.23    fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: banach"
   14.24    assumes "\<And>n x. x \<in> A \<Longrightarrow> norm (f n x) \<le> M n"
   14.25    assumes "summable M"
   14.26    shows "uniform_limit A (\<lambda>n x. \<Sum>i<n. f i x) (\<lambda>x. suminf (\<lambda>i. f i x)) sequentially"
   14.27 -  using assms by (intro weierstrass_m_test_ev always_eventually) auto
   14.28 +  using assms by (intro Weierstrass_m_test_ev always_eventually) auto
   14.29  
   14.30 -corollary%unimportant weierstrass_m_test'_ev:
   14.31 +corollary%unimportant Weierstrass_m_test'_ev:
   14.32    fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: banach"
   14.33    assumes "eventually (\<lambda>n. \<forall>x\<in>A. norm (f n x) \<le> M n) sequentially" "summable M"
   14.34    shows   "uniformly_convergent_on A (\<lambda>n x. \<Sum>i<n. f i x)"
   14.35 -  unfolding uniformly_convergent_on_def by (rule exI, rule weierstrass_m_test_ev[OF assms])
   14.36 +  unfolding uniformly_convergent_on_def by (rule exI, rule Weierstrass_m_test_ev[OF assms])
   14.37  
   14.38 -corollary%unimportant weierstrass_m_test':
   14.39 +corollary%unimportant Weierstrass_m_test':
   14.40    fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: banach"
   14.41    assumes "\<And>n x. x \<in> A \<Longrightarrow> norm (f n x) \<le> M n" "summable M"
   14.42    shows   "uniformly_convergent_on A (\<lambda>n x. \<Sum>i<n. f i x)"
   14.43 -  unfolding uniformly_convergent_on_def by (rule exI, rule weierstrass_m_test[OF assms])
   14.44 +  unfolding uniformly_convergent_on_def by (rule exI, rule Weierstrass_m_test[OF assms])
   14.45  
   14.46  lemma uniform_limit_eq_rhs: "uniform_limit X f l F \<Longrightarrow> l = m \<Longrightarrow> uniform_limit X f m F"
   14.47    by simp
   14.48 @@ -714,7 +714,7 @@
   14.49      using abs_summable_in_conv_radius [of "of_real r" a] assms
   14.50      by (simp add: norm_mult norm_power)
   14.51    show ?thesis
   14.52 -    by (simp add: weierstrass_m_test'_ev [OF _ *] norm_mult norm_power
   14.53 +    by (simp add: Weierstrass_m_test'_ev [OF _ *] norm_mult norm_power
   14.54                mult_left_mono power_mono dist_norm norm_minus_commute)
   14.55  next
   14.56    case False then show ?thesis by (simp add: not_le)
    15.1 --- a/src/HOL/Analysis/document/root.tex	Fri Dec 28 19:01:35 2018 +0100
    15.2 +++ b/src/HOL/Analysis/document/root.tex	Sat Dec 29 15:43:53 2018 +0100
    15.3 @@ -26,7 +26,7 @@
    15.4  
    15.5  \newpage
    15.6  
    15.7 -\renewcommand{\setisabellecontext}[1]{\markright{#1.thy}}
    15.8 +\renewcommand{\setisabellecontext}[1]{\markright{\href{#1.html}{#1.thy}}}
    15.9  
   15.10  \parindent 0pt\parskip 0.5ex
   15.11  \input{session}
    16.1 --- a/src/HOL/Computational_Algebra/Fundamental_Theorem_Algebra.thy	Fri Dec 28 19:01:35 2018 +0100
    16.2 +++ b/src/HOL/Computational_Algebra/Fundamental_Theorem_Algebra.thy	Sat Dec 29 15:43:53 2018 +0100
    16.3 @@ -234,7 +234,7 @@
    16.4    using real_sqrt_sum_squares_triangle_ineq[of "Re x - Re y" 0 0 "Im x - Im y"]
    16.5    unfolding cmod_def by simp
    16.6  
    16.7 -lemma bolzano_weierstrass_complex_disc:
    16.8 +lemma Bolzano_Weierstrass_complex_disc:
    16.9    assumes r: "\<forall>n. cmod (s n) \<le> r"
   16.10    shows "\<exists>f z. strict_mono (f :: nat \<Rightarrow> nat) \<and> (\<forall>e >0. \<exists>N. \<forall>n \<ge> N. cmod (s (f n) - z) < e)"
   16.11  proof -
   16.12 @@ -399,7 +399,7 @@
   16.13      from choice[OF th] obtain g where
   16.14          g: "\<forall>n. cmod (g n) \<le> r" "\<forall>n. cmod (poly p (g n)) <?m + 1 /real(Suc n)"
   16.15        by blast
   16.16 -    from bolzano_weierstrass_complex_disc[OF g(1)]
   16.17 +    from Bolzano_Weierstrass_complex_disc[OF g(1)]
   16.18      obtain f z where fz: "strict_mono (f :: nat \<Rightarrow> nat)" "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. cmod (g (f n) - z) < e"
   16.19        by blast
   16.20      {
    17.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Fri Dec 28 19:01:35 2018 +0100
    17.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Sat Dec 29 15:43:53 2018 +0100
    17.3 @@ -1259,7 +1259,7 @@
    17.4        case False
    17.5        have "lx \<le> real_of_float c" "real_of_float c \<le> ux" "lx \<le> xs!x" "xs!x \<le> ux"
    17.6          using Suc bnd_c \<open>bounded_by xs vs\<close>[THEN bounded_byE, OF \<open>x < length vs\<close>] bnd_x by auto
    17.7 -      from taylor[OF zero_less_Suc, of F, OF F0 DERIV[unfolded Suc] this False]
    17.8 +      from Taylor[OF zero_less_Suc, of F, OF F0 DERIV[unfolded Suc] this False]
    17.9        obtain t::real where t_bnd: "if xs ! x < c then xs ! x < t \<and> t < c else c < t \<and> t < xs ! x"
   17.10          and fl_eq: "interpret_floatarith f (xs[x := xs ! x]) =
   17.11             (\<Sum>m = 0..<Suc n'. F m c / (fact m) * (xs ! x - c) ^ m) +
    18.1 --- a/src/HOL/MacLaurin.thy	Fri Dec 28 19:01:35 2018 +0100
    18.2 +++ b/src/HOL/MacLaurin.thy	Sat Dec 29 15:43:53 2018 +0100
    18.3 @@ -319,14 +319,14 @@
    18.4    shows "\<exists>t. \<bar>t\<bar> \<le> \<bar>x\<bar> \<and> exp x = (\<Sum>m<n. (x ^ m) / fact m) + (exp t / fact n) * x ^ n"
    18.5    using Maclaurin_all_le_objl [where diff = "\<lambda>n. exp" and f = exp and x = x and n = n] by auto
    18.6  
    18.7 -corollary exp_lower_taylor_quadratic: "0 \<le> x \<Longrightarrow> 1 + x + x\<^sup>2 / 2 \<le> exp x"
    18.8 +corollary exp_lower_Taylor_quadratic: "0 \<le> x \<Longrightarrow> 1 + x + x\<^sup>2 / 2 \<le> exp x"
    18.9    for x :: real
   18.10    using Maclaurin_exp_le [of x 3] by (auto simp: numeral_3_eq_3 power2_eq_square)
   18.11  
   18.12  corollary ln_2_less_1: "ln 2 < (1::real)"
   18.13  proof -
   18.14    have "2 < 5/(2::real)" by simp
   18.15 -  also have "5/2 \<le> exp (1::real)" using exp_lower_taylor_quadratic[of 1, simplified] by simp
   18.16 +  also have "5/2 \<le> exp (1::real)" using exp_lower_Taylor_quadratic[of 1, simplified] by simp
   18.17    finally have "exp (ln 2) < exp (1::real)" by simp
   18.18    thus "ln 2 < (1::real)" by (subst (asm) exp_less_cancel_iff) simp
   18.19  qed
   18.20 @@ -530,7 +530,7 @@
   18.21    to prove Taylor's theorem.
   18.22  \<close>
   18.23  
   18.24 -lemma taylor_up:
   18.25 +lemma Taylor_up:
   18.26    assumes INIT: "n > 0" "diff 0 = f"
   18.27      and DERIV: "\<forall>m t. m < n \<and> a \<le> t \<and> t \<le> b \<longrightarrow> DERIV (diff m) t :> (diff (Suc m) t)"
   18.28      and INTERV: "a \<le> c" "c < b"
   18.29 @@ -565,7 +565,7 @@
   18.30    then show ?thesis by fastforce
   18.31  qed
   18.32  
   18.33 -lemma taylor_down:
   18.34 +lemma Taylor_down:
   18.35    fixes a :: real and n :: nat
   18.36    assumes INIT: "n > 0" "diff 0 = f"
   18.37      and DERIV: "(\<forall>m t. m < n \<and> a \<le> t \<and> t \<le> b \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t)"
   18.38 @@ -601,7 +601,7 @@
   18.39    then show ?thesis by fastforce
   18.40  qed
   18.41  
   18.42 -theorem taylor:
   18.43 +theorem Taylor:
   18.44    fixes a :: real and n :: nat
   18.45    assumes INIT: "n > 0" "diff 0 = f"
   18.46      and DERIV: "\<forall>m t. m < n \<and> a \<le> t \<and> t \<le> b \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
   18.47 @@ -619,7 +619,7 @@
   18.48      by simp
   18.49    ultimately have "\<exists>t>x. t < c \<and> f x =
   18.50      (\<Sum>m<n. diff m c / (fact m) * (x - c) ^ m) + diff n t / (fact n) * (x - c) ^ n"
   18.51 -    by (rule taylor_down)
   18.52 +    by (rule Taylor_down)
   18.53    with True show ?thesis by simp
   18.54  next
   18.55    case False
   18.56 @@ -632,7 +632,7 @@
   18.57      by arith
   18.58    ultimately have "\<exists>t>c. t < x \<and> f x =
   18.59      (\<Sum>m<n. diff m c / (fact m) * (x - c) ^ m) + diff n t / (fact n) * (x - c) ^ n"
   18.60 -    by (rule taylor_up)
   18.61 +    by (rule Taylor_up)
   18.62    with False show ?thesis by simp
   18.63  qed
   18.64  
    19.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Fri Dec 28 19:01:35 2018 +0100
    19.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Sat Dec 29 15:43:53 2018 +0100
    19.3 @@ -848,7 +848,7 @@
    19.4          by (simp add: sums_unique)
    19.5      next
    19.6        show "uniform_limit A (\<lambda>n a. \<Sum>i<n. ?f i a) (\<lambda>a. (\<Sum> n. ?f n a)) sequentially"
    19.7 -      proof (rule weierstrass_m_test)
    19.8 +      proof (rule Weierstrass_m_test)
    19.9          fix n a assume "a\<in>A"
   19.10          then show "norm (?f n a) \<le> pmf (map_pmf (to_nat_on M) M) n * B"
   19.11            using bnd by (auto intro!: mult_mono simp: from_nat_into set_pmf_not_empty)
    20.1 --- a/src/HOL/Topological_Spaces.thy	Fri Dec 28 19:01:35 2018 +0100
    20.2 +++ b/src/HOL/Topological_Spaces.thy	Sat Dec 29 15:43:53 2018 +0100
    20.3 @@ -2314,14 +2314,14 @@
    20.4  context topological_space
    20.5  begin
    20.6  
    20.7 -definition compact :: "'a set \<Rightarrow> bool"
    20.8 -  where compact_eq_heine_borel:  (* This name is used for backwards compatibility *)
    20.9 +definition compact :: "'a set \<Rightarrow> bool" where
   20.10 +compact_eq_Heine_Borel:  (* This name is used for backwards compatibility *)
   20.11      "compact S \<longleftrightarrow> (\<forall>C. (\<forall>c\<in>C. open c) \<and> S \<subseteq> \<Union>C \<longrightarrow> (\<exists>D\<subseteq>C. finite D \<and> S \<subseteq> \<Union>D))"
   20.12  
   20.13  lemma compactI:
   20.14    assumes "\<And>C. \<forall>t\<in>C. open t \<Longrightarrow> s \<subseteq> \<Union>C \<Longrightarrow> \<exists>C'. C' \<subseteq> C \<and> finite C' \<and> s \<subseteq> \<Union>C'"
   20.15    shows "compact s"
   20.16 -  unfolding compact_eq_heine_borel using assms by metis
   20.17 +  unfolding compact_eq_Heine_Borel using assms by metis
   20.18  
   20.19  lemma compact_empty[simp]: "compact {}"
   20.20    by (auto intro!: compactI)
   20.21 @@ -2329,7 +2329,7 @@
   20.22  lemma compactE: (*related to COMPACT_IMP_HEINE_BOREL in HOL Light*)
   20.23    assumes "compact S" "S \<subseteq> \<Union>\<T>" "\<And>B. B \<in> \<T> \<Longrightarrow> open B"
   20.24    obtains \<T>' where "\<T>' \<subseteq> \<T>" "finite \<T>'" "S \<subseteq> \<Union>\<T>'"
   20.25 -  by (meson assms compact_eq_heine_borel)
   20.26 +  by (meson assms compact_eq_Heine_Borel)
   20.27  
   20.28  lemma compactE_image:
   20.29    assumes "compact S"
   20.30 @@ -2353,7 +2353,7 @@
   20.31    moreover from cover have "S \<subseteq> \<Union>(C \<union> {- T})"
   20.32      by auto
   20.33    ultimately have "\<exists>D\<subseteq>C \<union> {- T}. finite D \<and> S \<subseteq> \<Union>D"
   20.34 -    using \<open>compact S\<close> unfolding compact_eq_heine_borel by auto
   20.35 +    using \<open>compact S\<close> unfolding compact_eq_Heine_Borel by auto
   20.36    then obtain D where "D \<subseteq> C \<union> {- T} \<and> finite D \<and> S \<subseteq> \<Union>D" ..
   20.37    then show "\<exists>D\<subseteq>C. finite D \<and> S \<inter> T \<subseteq> \<Union>D"
   20.38      by (intro exI[of _ "D - {-T}"]) auto
   20.39 @@ -2372,7 +2372,7 @@
   20.40    "compact U \<longleftrightarrow>
   20.41      (\<forall>A. (\<forall>a\<in>A. closed a) \<longrightarrow> (\<forall>B \<subseteq> A. finite B \<longrightarrow> U \<inter> \<Inter>B \<noteq> {}) \<longrightarrow> U \<inter> \<Inter>A \<noteq> {})"
   20.42    (is "_ \<longleftrightarrow> ?R")
   20.43 -proof (safe intro!: compact_eq_heine_borel[THEN iffD2])
   20.44 +proof (safe intro!: compact_eq_Heine_Borel[THEN iffD2])
   20.45    fix A
   20.46    assume "compact U"
   20.47    assume A: "\<forall>a\<in>A. closed a" "U \<inter> \<Inter>A = {}"
   20.48 @@ -2380,7 +2380,7 @@
   20.49    from A have "(\<forall>a\<in>uminus`A. open a) \<and> U \<subseteq> \<Union>(uminus`A)"
   20.50      by auto
   20.51    with \<open>compact U\<close> obtain B where "B \<subseteq> A" "finite (uminus`B)" "U \<subseteq> \<Union>(uminus`B)"
   20.52 -    unfolding compact_eq_heine_borel by (metis subset_image_iff)
   20.53 +    unfolding compact_eq_Heine_Borel by (metis subset_image_iff)
   20.54    with fin[THEN spec, of B] show False
   20.55      by (auto dest: finite_imageD intro: inj_setminus)
   20.56  next