extend continuous_intros; remove continuous_on_intros and isCont_intros
authorhoelzl
Wed Apr 02 18:35:07 2014 +0200 (2014-04-02)
changeset 56371fb9ae0727548
parent 56370 7c717ba55a0b
child 56372 fadb0fef09d7
extend continuous_intros; remove continuous_on_intros and isCont_intros
NEWS
src/HOL/Deriv.thy
src/HOL/Library/Product_Vector.thy
src/HOL/Limits.thy
src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy
src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy
src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Derivative.thy
src/HOL/Multivariate_Analysis/Fashoda.thy
src/HOL/Multivariate_Analysis/Integration.thy
src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Path_Connected.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/NthRoot.thy
src/HOL/Probability/Borel_Space.thy
src/HOL/Probability/Distributions.thy
src/HOL/Topological_Spaces.thy
src/HOL/Transcendental.thy
     1.1 --- a/NEWS	Wed Apr 02 18:35:02 2014 +0200
     1.2 +++ b/NEWS	Wed Apr 02 18:35:07 2014 +0200
     1.3 @@ -543,6 +543,9 @@
     1.4      deriv_fderiv              ~>  has_field_derivative_def
     1.5  INCOMPATIBILITY.
     1.6  
     1.7 +* Include more theorems in continuous_intros. Remove the continuous_on_intros,
     1.8 +  isCont_intros collections, these facts are now in continuous_intros.
     1.9 +
    1.10  * Removed solvers remote_cvc3 and remote_z3. Use cvc3 and z3 instead.
    1.11  
    1.12  * Nitpick:
     2.1 --- a/src/HOL/Deriv.thy	Wed Apr 02 18:35:02 2014 +0200
     2.2 +++ b/src/HOL/Deriv.thy	Wed Apr 02 18:35:07 2014 +0200
     2.3 @@ -1116,7 +1116,7 @@
     2.4  proof -
     2.5    let ?F = "%x. f x - ((f b - f a) / (b-a)) * x"
     2.6    have contF: "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont ?F x"
     2.7 -    using con by (fast intro: isCont_intros)
     2.8 +    using con by (fast intro: continuous_intros)
     2.9    have difF: "\<forall>x. a < x \<and> x < b \<longrightarrow> ?F differentiable (at x)"
    2.10    proof (clarify)
    2.11      fix x::real
     3.1 --- a/src/HOL/Library/Product_Vector.thy	Wed Apr 02 18:35:02 2014 +0200
     3.2 +++ b/src/HOL/Library/Product_Vector.thy	Wed Apr 02 18:35:07 2014 +0200
     3.3 @@ -204,13 +204,13 @@
     3.4  lemma continuous_Pair[continuous_intros]: "continuous F f \<Longrightarrow> continuous F g \<Longrightarrow> continuous F (\<lambda>x. (f x, g x))"
     3.5    unfolding continuous_def by (rule tendsto_Pair)
     3.6  
     3.7 -lemma continuous_on_fst[continuous_on_intros]: "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. fst (f x))"
     3.8 +lemma continuous_on_fst[continuous_intros]: "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. fst (f x))"
     3.9    unfolding continuous_on_def by (auto intro: tendsto_fst)
    3.10  
    3.11 -lemma continuous_on_snd[continuous_on_intros]: "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. snd (f x))"
    3.12 +lemma continuous_on_snd[continuous_intros]: "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. snd (f x))"
    3.13    unfolding continuous_on_def by (auto intro: tendsto_snd)
    3.14  
    3.15 -lemma continuous_on_Pair[continuous_on_intros]: "continuous_on s f \<Longrightarrow> continuous_on s g \<Longrightarrow> continuous_on s (\<lambda>x. (f x, g x))"
    3.16 +lemma continuous_on_Pair[continuous_intros]: "continuous_on s f \<Longrightarrow> continuous_on s g \<Longrightarrow> continuous_on s (\<lambda>x. (f x, g x))"
    3.17    unfolding continuous_on_def by (auto intro: tendsto_Pair)
    3.18  
    3.19  lemma isCont_fst [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. fst (f x)) a"
     4.1 --- a/src/HOL/Limits.thy	Wed Apr 02 18:35:02 2014 +0200
     4.2 +++ b/src/HOL/Limits.thy	Wed Apr 02 18:35:07 2014 +0200
     4.3 @@ -436,7 +436,7 @@
     4.4    shows "continuous F f \<Longrightarrow> continuous F g \<Longrightarrow> continuous F (\<lambda>x. dist (f x) (g x))"
     4.5    unfolding continuous_def by (rule tendsto_dist)
     4.6  
     4.7 -lemma continuous_on_dist[continuous_on_intros]:
     4.8 +lemma continuous_on_dist[continuous_intros]:
     4.9    fixes f g :: "_ \<Rightarrow> 'a :: metric_space"
    4.10    shows "continuous_on s f \<Longrightarrow> continuous_on s g \<Longrightarrow> continuous_on s (\<lambda>x. dist (f x) (g x))"
    4.11    unfolding continuous_on_def by (auto intro: tendsto_dist)
    4.12 @@ -449,7 +449,7 @@
    4.13    "continuous F f \<Longrightarrow> continuous F (\<lambda>x. norm (f x))"
    4.14    unfolding continuous_def by (rule tendsto_norm)
    4.15  
    4.16 -lemma continuous_on_norm [continuous_on_intros]:
    4.17 +lemma continuous_on_norm [continuous_intros]:
    4.18    "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. norm (f x))"
    4.19    unfolding continuous_on_def by (auto intro: tendsto_norm)
    4.20  
    4.21 @@ -473,7 +473,7 @@
    4.22    "continuous F f \<Longrightarrow> continuous F (\<lambda>x. \<bar>f x :: real\<bar>)"
    4.23    unfolding real_norm_def[symmetric] by (rule continuous_norm)
    4.24  
    4.25 -lemma continuous_on_rabs [continuous_on_intros]:
    4.26 +lemma continuous_on_rabs [continuous_intros]:
    4.27    "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. \<bar>f x :: real\<bar>)"
    4.28    unfolding real_norm_def[symmetric] by (rule continuous_on_norm)
    4.29  
    4.30 @@ -501,7 +501,7 @@
    4.31    shows "continuous F f \<Longrightarrow> continuous F g \<Longrightarrow> continuous F (\<lambda>x. f x + g x)"
    4.32    unfolding continuous_def by (rule tendsto_add)
    4.33  
    4.34 -lemma continuous_on_add [continuous_on_intros]:
    4.35 +lemma continuous_on_add [continuous_intros]:
    4.36    fixes f g :: "_ \<Rightarrow> 'b::real_normed_vector"
    4.37    shows "continuous_on s f \<Longrightarrow> continuous_on s g \<Longrightarrow> continuous_on s (\<lambda>x. f x + g x)"
    4.38    unfolding continuous_on_def by (auto intro: tendsto_add)
    4.39 @@ -521,7 +521,7 @@
    4.40    shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. - f x)"
    4.41    unfolding continuous_def by (rule tendsto_minus)
    4.42  
    4.43 -lemma continuous_on_minus [continuous_on_intros]:
    4.44 +lemma continuous_on_minus [continuous_intros]:
    4.45    fixes f :: "_ \<Rightarrow> 'b::real_normed_vector"
    4.46    shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. - f x)"
    4.47    unfolding continuous_on_def by (auto intro: tendsto_minus)
    4.48 @@ -546,7 +546,7 @@
    4.49    shows "continuous F f \<Longrightarrow> continuous F g \<Longrightarrow> continuous F (\<lambda>x. f x - g x)"
    4.50    unfolding continuous_def by (rule tendsto_diff)
    4.51  
    4.52 -lemma continuous_on_diff [continuous_on_intros]:
    4.53 +lemma continuous_on_diff [continuous_intros]:
    4.54    fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
    4.55    shows "continuous_on s f \<Longrightarrow> continuous_on s g \<Longrightarrow> continuous_on s (\<lambda>x. f x - g x)"
    4.56    unfolding continuous_on_def by (auto intro: tendsto_diff)
    4.57 @@ -638,13 +638,13 @@
    4.58  lemmas continuous_mult [continuous_intros] =
    4.59    bounded_bilinear.continuous [OF bounded_bilinear_mult]
    4.60  
    4.61 -lemmas continuous_on_of_real [continuous_on_intros] =
    4.62 +lemmas continuous_on_of_real [continuous_intros] =
    4.63    bounded_linear.continuous_on [OF bounded_linear_of_real]
    4.64  
    4.65 -lemmas continuous_on_scaleR [continuous_on_intros] =
    4.66 +lemmas continuous_on_scaleR [continuous_intros] =
    4.67    bounded_bilinear.continuous_on [OF bounded_bilinear_scaleR]
    4.68  
    4.69 -lemmas continuous_on_mult [continuous_on_intros] =
    4.70 +lemmas continuous_on_mult [continuous_intros] =
    4.71    bounded_bilinear.continuous_on [OF bounded_bilinear_mult]
    4.72  
    4.73  lemmas tendsto_mult_zero =
    4.74 @@ -666,7 +666,7 @@
    4.75    shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. (f x)^n)"
    4.76    unfolding continuous_def by (rule tendsto_power)
    4.77  
    4.78 -lemma continuous_on_power [continuous_on_intros]:
    4.79 +lemma continuous_on_power [continuous_intros]:
    4.80    fixes f :: "_ \<Rightarrow> 'b::{power,real_normed_algebra}"
    4.81    shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. (f x)^n)"
    4.82    unfolding continuous_on_def by (auto intro: tendsto_power)
    4.83 @@ -820,7 +820,7 @@
    4.84    shows "isCont (\<lambda>x. inverse (f x)) a"
    4.85    using assms unfolding continuous_at by (rule tendsto_inverse)
    4.86  
    4.87 -lemma continuous_on_inverse[continuous_on_intros]:
    4.88 +lemma continuous_on_inverse[continuous_intros]:
    4.89    fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_div_algebra"
    4.90    assumes "continuous_on s f" and "\<forall>x\<in>s. f x \<noteq> 0"
    4.91    shows "continuous_on s (\<lambda>x. inverse (f x))"
    4.92 @@ -850,7 +850,7 @@
    4.93    shows "isCont (\<lambda>x. (f x) / g x) a"
    4.94    using assms unfolding continuous_at by (rule tendsto_divide)
    4.95  
    4.96 -lemma continuous_on_divide[continuous_on_intros]:
    4.97 +lemma continuous_on_divide[continuous_intros]:
    4.98    fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_field"
    4.99    assumes "continuous_on s f" "continuous_on s g" and "\<forall>x\<in>s. g x \<noteq> 0"
   4.100    shows "continuous_on s (\<lambda>x. (f x) / (g x))"
   4.101 @@ -879,7 +879,7 @@
   4.102    shows "isCont (\<lambda>x. sgn (f x)) a"
   4.103    using assms unfolding continuous_at by (rule tendsto_sgn)
   4.104  
   4.105 -lemma continuous_on_sgn[continuous_on_intros]:
   4.106 +lemma continuous_on_sgn[continuous_intros]:
   4.107    fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
   4.108    assumes "continuous_on s f" and "\<forall>x\<in>s. f x \<noteq> 0"
   4.109    shows "continuous_on s (\<lambda>x. sgn (f x))"
   4.110 @@ -1685,11 +1685,6 @@
   4.111    shows "\<forall>i\<in>A. isCont (f i) a \<Longrightarrow> isCont (\<lambda>x. \<Sum>i\<in>A. f i x) a"
   4.112    by (auto intro: continuous_setsum)
   4.113  
   4.114 -lemmas isCont_intros =
   4.115 -  isCont_ident isCont_const isCont_norm isCont_rabs isCont_add isCont_minus
   4.116 -  isCont_diff isCont_mult isCont_inverse isCont_divide isCont_scaleR
   4.117 -  isCont_of_real isCont_power isCont_sgn isCont_setsum
   4.118 -
   4.119  subsection {* Uniform Continuity *}
   4.120  
   4.121  definition
     5.1 --- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Wed Apr 02 18:35:02 2014 +0200
     5.2 +++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Wed Apr 02 18:35:07 2014 +0200
     5.3 @@ -107,7 +107,7 @@
     5.4  next
     5.5    case False
     5.6    have "continuous_on s (norm \<circ> f)"
     5.7 -    by (rule continuous_on_intros continuous_on_norm assms(2))+
     5.8 +    by (rule continuous_intros continuous_on_norm assms(2))+
     5.9    with False obtain x where x: "x \<in> s" "\<forall>y\<in>s. (norm \<circ> f) x \<le> (norm \<circ> f) y"
    5.10      using continuous_attains_inf[OF assms(1), of "norm \<circ> f"]
    5.11      unfolding o_def
    5.12 @@ -1460,7 +1460,7 @@
    5.13    obtain d where
    5.14        d: "d > 0" "\<And>x. x \<in> unit_cube \<Longrightarrow> d \<le> norm (f x - x)"
    5.15      apply (rule brouwer_compactness_lemma[OF compact_unit_cube _ *])
    5.16 -    apply (rule continuous_on_intros assms)+
    5.17 +    apply (rule continuous_intros assms)+
    5.18      apply blast
    5.19      done
    5.20    have *: "\<forall>x. x \<in> unit_cube \<longrightarrow> f x \<in> unit_cube"
    5.21 @@ -2023,7 +2023,7 @@
    5.22      apply assumption+
    5.23      apply (rule_tac x=x in bexI)
    5.24      apply assumption+
    5.25 -    apply (rule continuous_on_intros)+
    5.26 +    apply (rule continuous_intros)+
    5.27      unfolding frontier_cball subset_eq Ball_def image_iff
    5.28      apply rule
    5.29      apply rule
     6.1 --- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Wed Apr 02 18:35:02 2014 +0200
     6.2 +++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Wed Apr 02 18:35:07 2014 +0200
     6.3 @@ -119,12 +119,12 @@
     6.4    shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. f x * c)"
     6.5  by (rule continuous_on_mult [OF _ continuous_on_const])
     6.6  
     6.7 -lemma uniformly_continuous_on_cmul_right [continuous_on_intros]:
     6.8 +lemma uniformly_continuous_on_cmul_right [continuous_intros]:
     6.9    fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra"
    6.10    shows "uniformly_continuous_on s f \<Longrightarrow> uniformly_continuous_on s (\<lambda>x. f x * c)"
    6.11    using bounded_linear.uniformly_continuous_on[OF bounded_linear_mult_left] . 
    6.12  
    6.13 -lemma uniformly_continuous_on_cmul_left[continuous_on_intros]:
    6.14 +lemma uniformly_continuous_on_cmul_left[continuous_intros]:
    6.15    fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra"
    6.16    assumes "uniformly_continuous_on s f"
    6.17      shows "uniformly_continuous_on s (\<lambda>x. c * f x)"
     7.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Wed Apr 02 18:35:02 2014 +0200
     7.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Wed Apr 02 18:35:07 2014 +0200
     7.3 @@ -1316,7 +1316,7 @@
     7.4    then obtain a b where a: "a \<in> A" "a \<in> s" and b: "b \<in> B" "b \<in> s" by auto
     7.5    def f \<equiv> "\<lambda>u. u *\<^sub>R a + (1 - u) *\<^sub>R b"
     7.6    then have "continuous_on {0 .. 1} f"
     7.7 -    by (auto intro!: continuous_on_intros)
     7.8 +    by (auto intro!: continuous_intros)
     7.9    then have "connected (f ` {0 .. 1})"
    7.10      by (auto intro!: connected_continuous_image)
    7.11    note connectedD[OF this, of A B]
     8.1 --- a/src/HOL/Multivariate_Analysis/Derivative.thy	Wed Apr 02 18:35:02 2014 +0200
     8.2 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Wed Apr 02 18:35:07 2014 +0200
     8.3 @@ -678,7 +678,7 @@
     8.4      show "((\<lambda>x. f x - (f b - f a) / (b - a) * x) has_derivative
     8.5          (\<lambda>xa. f' x xa - (f b - f a) / (b - a) * xa)) (at x)"
     8.6        by (intro has_derivative_intros assms(3)[rule_format,OF x] mult_right_has_derivative)
     8.7 -  qed (insert assms(1,2), auto intro!: continuous_on_intros simp: field_simps)
     8.8 +  qed (insert assms(1,2), auto intro!: continuous_intros simp: field_simps)
     8.9    then obtain x where
    8.10      "x \<in> {a <..< b}"
    8.11      "(\<lambda>xa. f' x xa - (f b - f a) / (b - a) * xa) = (\<lambda>v. 0)" ..
    8.12 @@ -749,7 +749,7 @@
    8.13    have "\<exists>x\<in>{a<..<b}. (f b - f a) \<bullet> f b - (f b - f a) \<bullet> f a = (f b - f a) \<bullet> f' x (b - a)"
    8.14      apply (rule mvt)
    8.15      apply (rule assms(1))
    8.16 -    apply (intro continuous_on_intros assms(2))
    8.17 +    apply (intro continuous_intros assms(2))
    8.18      using assms(3)
    8.19      apply (fast intro: has_derivative_inner_right)
    8.20      done
    8.21 @@ -798,7 +798,7 @@
    8.22      by (auto simp add: algebra_simps)
    8.23    then have 1: "continuous_on {0 .. 1} (f \<circ> ?p)"
    8.24      apply -
    8.25 -    apply (rule continuous_on_intros)+
    8.26 +    apply (rule continuous_intros)+
    8.27      unfolding continuous_on_eq_continuous_within
    8.28      apply rule
    8.29      apply (rule differentiable_imp_continuous_within)
    8.30 @@ -1138,7 +1138,7 @@
    8.31    show ?thesis
    8.32      unfolding *
    8.33      apply (rule brouwer[OF assms(1-3), of "\<lambda>y. x + (y - f y)"])
    8.34 -    apply (rule continuous_on_intros assms)+
    8.35 +    apply (rule continuous_intros assms)+
    8.36      using assms(4-6)
    8.37      apply auto
    8.38      done
    8.39 @@ -1209,7 +1209,7 @@
    8.40      show "continuous_on (cball (f x) e) (\<lambda>y. f (x + g' (y - f x)))"
    8.41        unfolding g'.diff
    8.42        apply (rule continuous_on_compose[of _ _ f, unfolded o_def])
    8.43 -      apply (rule continuous_on_intros linear_continuous_on[OF assms(5)])+
    8.44 +      apply (rule continuous_intros linear_continuous_on[OF assms(5)])+
    8.45        apply (rule continuous_on_subset[OF assms(2)])
    8.46        apply rule
    8.47        apply (unfold image_iff)
     9.1 --- a/src/HOL/Multivariate_Analysis/Fashoda.thy	Wed Apr 02 18:35:02 2014 +0200
     9.2 +++ b/src/HOL/Multivariate_Analysis/Fashoda.thy	Wed Apr 02 18:35:07 2014 +0200
     9.3 @@ -152,11 +152,11 @@
     9.4    have 1: "box (- 1) (1::real^2) \<noteq> {}"
     9.5      unfolding interval_eq_empty_cart by auto
     9.6    have 2: "continuous_on (cbox -1 1) (negatex \<circ> sqprojection \<circ> ?F)"
     9.7 -    apply (intro continuous_on_intros continuous_on_component)
     9.8 +    apply (intro continuous_intros continuous_on_component)
     9.9      unfolding *
    9.10      apply (rule assms)+
    9.11      apply (subst sqprojection_def)
    9.12 -    apply (intro continuous_on_intros)
    9.13 +    apply (intro continuous_intros)
    9.14      apply (simp add: infnorm_eq_0 x0)
    9.15      apply (rule linear_continuous_on)
    9.16    proof -
    9.17 @@ -370,7 +370,7 @@
    9.18      show "(f \<circ> iscale) ` {- 1..1} \<subseteq> cbox -1 1" "(g \<circ> iscale) ` {- 1..1} \<subseteq> cbox -1 1"
    9.19        using isc and assms(3-4) by (auto simp add: image_comp [symmetric])
    9.20      have *: "continuous_on {- 1..1} iscale"
    9.21 -      unfolding iscale_def by (rule continuous_on_intros)+
    9.22 +      unfolding iscale_def by (rule continuous_intros)+
    9.23      show "continuous_on {- 1..1} (f \<circ> iscale)" "continuous_on {- 1..1} (g \<circ> iscale)"
    9.24        apply -
    9.25        apply (rule_tac[!] continuous_on_compose[OF *])
    10.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Wed Apr 02 18:35:02 2014 +0200
    10.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Wed Apr 02 18:35:07 2014 +0200
    10.3 @@ -8747,7 +8747,7 @@
    10.4    assume "x \<noteq> c"
    10.5    note conv = assms(1)[unfolded convex_alt,rule_format]
    10.6    have as1: "continuous_on {0 ..1} (f \<circ> (\<lambda>t. (1 - t) *\<^sub>R c + t *\<^sub>R x))"
    10.7 -    apply (rule continuous_on_intros)+
    10.8 +    apply (rule continuous_intros)+
    10.9      apply (rule continuous_on_subset[OF assms(3)])
   10.10      apply safe
   10.11      apply (rule conv)
    11.1 --- a/src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy	Wed Apr 02 18:35:02 2014 +0200
    11.2 +++ b/src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy	Wed Apr 02 18:35:07 2014 +0200
    11.3 @@ -110,7 +110,7 @@
    11.4  proof atomize_elim
    11.5    let ?proj = "(\<lambda>x. x \<bullet> b) ` X"
    11.6    from assms have "compact ?proj" "?proj \<noteq> {}"
    11.7 -    by (auto intro!: compact_continuous_image continuous_on_intros)
    11.8 +    by (auto intro!: compact_continuous_image continuous_intros)
    11.9    from compact_attains_inf[OF this]
   11.10    obtain s x
   11.11      where s: "s\<in>(\<lambda>x. x \<bullet> b) ` X" "\<And>t. t\<in>(\<lambda>x. x \<bullet> b) ` X \<Longrightarrow> s \<le> t"
   11.12 @@ -133,7 +133,7 @@
   11.13  proof atomize_elim
   11.14    let ?proj = "(\<lambda>x. x \<bullet> b) ` X"
   11.15    from assms have "compact ?proj" "?proj \<noteq> {}"
   11.16 -    by (auto intro!: compact_continuous_image continuous_on_intros)
   11.17 +    by (auto intro!: compact_continuous_image continuous_intros)
   11.18    from compact_attains_sup[OF this]
   11.19    obtain s x
   11.20      where s: "s\<in>(\<lambda>x. x \<bullet> b) ` X" "\<And>t. t\<in>(\<lambda>x. x \<bullet> b) ` X \<Longrightarrow> t \<le> s"
    12.1 --- a/src/HOL/Multivariate_Analysis/Path_Connected.thy	Wed Apr 02 18:35:02 2014 +0200
    12.2 +++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy	Wed Apr 02 18:35:07 2014 +0200
    12.3 @@ -108,7 +108,7 @@
    12.4    have *: "\<And>g. path g \<Longrightarrow> path (reversepath g)"
    12.5      unfolding path_def reversepath_def
    12.6      apply (rule continuous_on_compose[unfolded o_def, of _ "\<lambda>x. 1 - x"])
    12.7 -    apply (intro continuous_on_intros)
    12.8 +    apply (intro continuous_intros)
    12.9      apply (rule continuous_on_subset[of "{0..1}"])
   12.10      apply assumption
   12.11      apply auto
   12.12 @@ -135,7 +135,7 @@
   12.13      by (intro continuous_on_cong refl) (auto simp: joinpaths_def pathfinish_def pathstart_def)
   12.14    show "continuous_on {0..1} g1" and "continuous_on {0..1} g2"
   12.15      unfolding g1 g2
   12.16 -    by (auto intro!: continuous_on_intros continuous_on_subset[OF cont] simp del: o_apply)
   12.17 +    by (auto intro!: continuous_intros continuous_on_subset[OF cont] simp del: o_apply)
   12.18  next
   12.19    assume g1g2: "continuous_on {0..1} g1" "continuous_on {0..1} g2"
   12.20    have 01: "{0 .. 1} = {0..1/2} \<union> {1/2 .. 1::real}"
   12.21 @@ -157,7 +157,7 @@
   12.22    show "continuous_on {0..1} (g1 +++ g2)"
   12.23      using assms
   12.24      unfolding joinpaths_def 01
   12.25 -    apply (intro continuous_on_cases closed_atLeastAtMost g1g2[THEN continuous_on_compose2] continuous_on_intros)
   12.26 +    apply (intro continuous_on_cases closed_atLeastAtMost g1g2[THEN continuous_on_compose2] continuous_intros)
   12.27      apply (auto simp: field_simps pathfinish_def pathstart_def intro!: 1 2)
   12.28      done
   12.29  qed
   12.30 @@ -423,9 +423,9 @@
   12.31      apply (rule continuous_on_eq[of _ "g \<circ> (\<lambda>x. a - 1 + x)"])
   12.32      defer
   12.33      prefer 3
   12.34 -    apply (rule continuous_on_intros)+
   12.35 +    apply (rule continuous_intros)+
   12.36      prefer 2
   12.37 -    apply (rule continuous_on_intros)+
   12.38 +    apply (rule continuous_intros)+
   12.39      apply (rule_tac[1-2] continuous_on_subset[OF assms(1)[unfolded path_def]])
   12.40      using assms(3) and **
   12.41      apply auto
   12.42 @@ -589,7 +589,7 @@
   12.43    unfolding path_defs
   12.44    apply (rule_tac x="\<lambda>u. x" in exI)
   12.45    using assms
   12.46 -  apply (auto intro!: continuous_on_intros)
   12.47 +  apply (auto intro!: continuous_intros)
   12.48    done
   12.49  
   12.50  lemma path_component_refl_eq: "path_component s x x \<longleftrightarrow> x \<in> s"
   12.51 @@ -977,11 +977,11 @@
   12.52      done
   12.53    have "continuous_on (UNIV - {0}) (\<lambda>x::'a. 1 / norm x)"
   12.54      unfolding field_divide_inverse
   12.55 -    by (simp add: continuous_on_intros)
   12.56 +    by (simp add: continuous_intros)
   12.57    then show ?thesis
   12.58      unfolding * **
   12.59      using path_connected_punctured_universe[OF assms]
   12.60 -    by (auto intro!: path_connected_continuous_image continuous_on_intros)
   12.61 +    by (auto intro!: path_connected_continuous_image continuous_intros)
   12.62  qed
   12.63  
   12.64  lemma connected_sphere: "2 \<le> DIM('a::euclidean_space) \<Longrightarrow> connected {x::'a. norm (x - a) = r}"
    13.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Apr 02 18:35:02 2014 +0200
    13.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Apr 02 18:35:07 2014 +0200
    13.3 @@ -791,7 +791,7 @@
    13.4  lemma open_ball [intro, simp]: "open (ball x e)"
    13.5  proof -
    13.6    have "open (dist x -` {..<e})"
    13.7 -    by (intro open_vimage open_lessThan continuous_on_intros)
    13.8 +    by (intro open_vimage open_lessThan continuous_intros)
    13.9    also have "dist x -` {..<e} = ball x e"
   13.10      by auto
   13.11    finally show ?thesis .
   13.12 @@ -2375,7 +2375,7 @@
   13.13  lemma closed_cball: "closed (cball x e)"
   13.14  proof -
   13.15    have "closed (dist x -` {..e})"
   13.16 -    by (intro closed_vimage closed_atMost continuous_on_intros)
   13.17 +    by (intro closed_vimage closed_atMost continuous_intros)
   13.18    also have "dist x -` {..e} = cball x e"
   13.19      by auto
   13.20    finally show ?thesis .
   13.21 @@ -4931,11 +4931,11 @@
   13.22  
   13.23  subsubsection {* Structural rules for setwise continuity *}
   13.24  
   13.25 -lemma continuous_on_infnorm[continuous_on_intros]:
   13.26 +lemma continuous_on_infnorm[continuous_intros]:
   13.27    "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. infnorm (f x))"
   13.28    unfolding continuous_on by (fast intro: tendsto_infnorm)
   13.29  
   13.30 -lemma continuous_on_inner[continuous_on_intros]:
   13.31 +lemma continuous_on_inner[continuous_intros]:
   13.32    fixes g :: "'a::topological_space \<Rightarrow> 'b::real_inner"
   13.33    assumes "continuous_on s f"
   13.34      and "continuous_on s g"
   13.35 @@ -4945,15 +4945,15 @@
   13.36  
   13.37  subsubsection {* Structural rules for uniform continuity *}
   13.38  
   13.39 -lemma uniformly_continuous_on_id[continuous_on_intros]:
   13.40 +lemma uniformly_continuous_on_id[continuous_intros]:
   13.41    "uniformly_continuous_on s (\<lambda>x. x)"
   13.42    unfolding uniformly_continuous_on_def by auto
   13.43  
   13.44 -lemma uniformly_continuous_on_const[continuous_on_intros]:
   13.45 +lemma uniformly_continuous_on_const[continuous_intros]:
   13.46    "uniformly_continuous_on s (\<lambda>x. c)"
   13.47    unfolding uniformly_continuous_on_def by simp
   13.48  
   13.49 -lemma uniformly_continuous_on_dist[continuous_on_intros]:
   13.50 +lemma uniformly_continuous_on_dist[continuous_intros]:
   13.51    fixes f g :: "'a::metric_space \<Rightarrow> 'b::metric_space"
   13.52    assumes "uniformly_continuous_on s f"
   13.53      and "uniformly_continuous_on s g"
   13.54 @@ -4979,20 +4979,20 @@
   13.55      unfolding dist_real_def by simp
   13.56  qed
   13.57  
   13.58 -lemma uniformly_continuous_on_norm[continuous_on_intros]:
   13.59 +lemma uniformly_continuous_on_norm[continuous_intros]:
   13.60    assumes "uniformly_continuous_on s f"
   13.61    shows "uniformly_continuous_on s (\<lambda>x. norm (f x))"
   13.62    unfolding norm_conv_dist using assms
   13.63    by (intro uniformly_continuous_on_dist uniformly_continuous_on_const)
   13.64  
   13.65 -lemma (in bounded_linear) uniformly_continuous_on[continuous_on_intros]:
   13.66 +lemma (in bounded_linear) uniformly_continuous_on[continuous_intros]:
   13.67    assumes "uniformly_continuous_on s g"
   13.68    shows "uniformly_continuous_on s (\<lambda>x. f (g x))"
   13.69    using assms unfolding uniformly_continuous_on_sequentially
   13.70    unfolding dist_norm tendsto_norm_zero_iff diff[symmetric]
   13.71    by (auto intro: tendsto_zero)
   13.72  
   13.73 -lemma uniformly_continuous_on_cmul[continuous_on_intros]:
   13.74 +lemma uniformly_continuous_on_cmul[continuous_intros]:
   13.75    fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
   13.76    assumes "uniformly_continuous_on s f"
   13.77    shows "uniformly_continuous_on s (\<lambda>x. c *\<^sub>R f(x))"
   13.78 @@ -5004,12 +5004,12 @@
   13.79    shows "dist (- x) (- y) = dist x y"
   13.80    unfolding dist_norm minus_diff_minus norm_minus_cancel ..
   13.81  
   13.82 -lemma uniformly_continuous_on_minus[continuous_on_intros]:
   13.83 +lemma uniformly_continuous_on_minus[continuous_intros]:
   13.84    fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
   13.85    shows "uniformly_continuous_on s f \<Longrightarrow> uniformly_continuous_on s (\<lambda>x. - f x)"
   13.86    unfolding uniformly_continuous_on_def dist_minus .
   13.87  
   13.88 -lemma uniformly_continuous_on_add[continuous_on_intros]:
   13.89 +lemma uniformly_continuous_on_add[continuous_intros]:
   13.90    fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
   13.91    assumes "uniformly_continuous_on s f"
   13.92      and "uniformly_continuous_on s g"
   13.93 @@ -5019,7 +5019,7 @@
   13.94    unfolding dist_norm tendsto_norm_zero_iff add_diff_add
   13.95    by (auto intro: tendsto_add_zero)
   13.96  
   13.97 -lemma uniformly_continuous_on_diff[continuous_on_intros]:
   13.98 +lemma uniformly_continuous_on_diff[continuous_intros]:
   13.99    fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
  13.100    assumes "uniformly_continuous_on s f"
  13.101      and "uniformly_continuous_on s g"
  13.102 @@ -5031,7 +5031,7 @@
  13.103  
  13.104  lemmas continuous_at_compose = isCont_o
  13.105  
  13.106 -lemma uniformly_continuous_on_compose[continuous_on_intros]:
  13.107 +lemma uniformly_continuous_on_compose[continuous_intros]:
  13.108    assumes "uniformly_continuous_on s f"  "uniformly_continuous_on (f ` s) g"
  13.109    shows "uniformly_continuous_on s (g \<circ> f)"
  13.110  proof -
  13.111 @@ -6972,7 +6972,7 @@
  13.112    apply (rule_tac x="\<lambda>x. c *\<^sub>R x" in exI)
  13.113    apply (rule_tac x="\<lambda>x. (1 / c) *\<^sub>R x" in exI)
  13.114    using assms
  13.115 -  apply (auto simp add: continuous_on_intros)
  13.116 +  apply (auto simp add: continuous_intros)
  13.117    done
  13.118  
  13.119  lemma homeomorphic_translation:
  13.120 @@ -7010,14 +7010,14 @@
  13.121      apply(rule_tac x="\<lambda>x. b + (e/d) *\<^sub>R (x - a)" in exI)
  13.122      apply(rule_tac x="\<lambda>x. a + (d/e) *\<^sub>R (x - b)" in exI)
  13.123      using assms
  13.124 -    apply (auto intro!: continuous_on_intros
  13.125 +    apply (auto intro!: continuous_intros
  13.126        simp: dist_commute dist_norm pos_divide_less_eq mult_strict_left_mono)
  13.127      done
  13.128    show ?cth unfolding homeomorphic_minimal
  13.129      apply(rule_tac x="\<lambda>x. b + (e/d) *\<^sub>R (x - a)" in exI)
  13.130      apply(rule_tac x="\<lambda>x. a + (d/e) *\<^sub>R (x - b)" in exI)
  13.131      using assms
  13.132 -    apply (auto intro!: continuous_on_intros
  13.133 +    apply (auto intro!: continuous_intros
  13.134        simp: dist_commute dist_norm pos_divide_le_eq mult_strict_left_mono)
  13.135      done
  13.136  qed
    14.1 --- a/src/HOL/NthRoot.thy	Wed Apr 02 18:35:02 2014 +0200
    14.2 +++ b/src/HOL/NthRoot.thy	Wed Apr 02 18:35:07 2014 +0200
    14.3 @@ -255,7 +255,7 @@
    14.4    assume n: "0 < n"
    14.5    let ?f = "\<lambda>y::real. sgn y * \<bar>y\<bar>^n"
    14.6    have "continuous_on ({0..} \<union> {.. 0}) (\<lambda>x. if 0 < x then x ^ n else - ((-x) ^ n) :: real)"
    14.7 -    using n by (intro continuous_on_If continuous_on_intros) auto
    14.8 +    using n by (intro continuous_on_If continuous_intros) auto
    14.9    then have "continuous_on UNIV ?f"
   14.10      by (rule continuous_on_cong[THEN iffD1, rotated 2]) (auto simp: not_less real_sgn_neg le_less n)
   14.11    then have [simp]: "\<And>x. isCont ?f x"
   14.12 @@ -275,7 +275,7 @@
   14.13    "continuous F f \<Longrightarrow> continuous F (\<lambda>x. root n (f x))"
   14.14    unfolding continuous_def by (rule tendsto_real_root)
   14.15    
   14.16 -lemma continuous_on_real_root[continuous_on_intros]:
   14.17 +lemma continuous_on_real_root[continuous_intros]:
   14.18    "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. root n (f x))"
   14.19    unfolding continuous_on_def by (auto intro: tendsto_real_root)
   14.20  
   14.21 @@ -454,7 +454,7 @@
   14.22    "continuous F f \<Longrightarrow> continuous F (\<lambda>x. sqrt (f x))"
   14.23    unfolding sqrt_def by (rule continuous_real_root)
   14.24    
   14.25 -lemma continuous_on_real_sqrt[continuous_on_intros]:
   14.26 +lemma continuous_on_real_sqrt[continuous_intros]:
   14.27    "continuous_on s f \<Longrightarrow> 0 < n \<Longrightarrow> continuous_on s (\<lambda>x. sqrt (f x))"
   14.28    unfolding sqrt_def by (rule continuous_on_real_root)
   14.29  
    15.1 --- a/src/HOL/Probability/Borel_Space.thy	Wed Apr 02 18:35:02 2014 +0200
    15.2 +++ b/src/HOL/Probability/Borel_Space.thy	Wed Apr 02 18:35:07 2014 +0200
    15.3 @@ -221,7 +221,7 @@
    15.4    assumes "g \<in> borel_measurable M"
    15.5    shows "(\<lambda>x. f x \<bullet> g x) \<in> borel_measurable M"
    15.6    using assms
    15.7 -  by (rule borel_measurable_continuous_Pair) (intro continuous_on_intros)
    15.8 +  by (rule borel_measurable_continuous_Pair) (intro continuous_intros)
    15.9  
   15.10  lemma [measurable]:
   15.11    fixes a b :: "'a\<Colon>linorder_topology"
   15.12 @@ -287,7 +287,7 @@
   15.13      by auto
   15.14    also have "\<dots> \<in> sets M"
   15.15      by (intro measurable_sets[OF borel_measurable_Pair borel_open, OF assms open_Collect_less]
   15.16 -              continuous_on_intros)
   15.17 +              continuous_intros)
   15.18    finally show ?thesis .
   15.19  qed
   15.20  
   15.21 @@ -659,14 +659,14 @@
   15.22    fixes g :: "'a \<Rightarrow> 'b::{second_countable_topology, real_normed_vector}"
   15.23    assumes g: "g \<in> borel_measurable M"
   15.24    shows "(\<lambda>x. - g x) \<in> borel_measurable M"
   15.25 -  by (rule borel_measurable_continuous_on[OF _ g]) (intro continuous_on_intros)
   15.26 +  by (rule borel_measurable_continuous_on[OF _ g]) (intro continuous_intros)
   15.27  
   15.28  lemma borel_measurable_add[measurable (raw)]:
   15.29    fixes f g :: "'a \<Rightarrow> 'b::{second_countable_topology, real_normed_vector}"
   15.30    assumes f: "f \<in> borel_measurable M"
   15.31    assumes g: "g \<in> borel_measurable M"
   15.32    shows "(\<lambda>x. f x + g x) \<in> borel_measurable M"
   15.33 -  using f g by (rule borel_measurable_continuous_Pair) (intro continuous_on_intros)
   15.34 +  using f g by (rule borel_measurable_continuous_Pair) (intro continuous_intros)
   15.35  
   15.36  lemma borel_measurable_setsum[measurable (raw)]:
   15.37    fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> 'b::{second_countable_topology, real_normed_vector}"
   15.38 @@ -689,7 +689,7 @@
   15.39    assumes f: "f \<in> borel_measurable M"
   15.40    assumes g: "g \<in> borel_measurable M"
   15.41    shows "(\<lambda>x. f x * g x) \<in> borel_measurable M"
   15.42 -  using f g by (rule borel_measurable_continuous_Pair) (intro continuous_on_intros)
   15.43 +  using f g by (rule borel_measurable_continuous_Pair) (intro continuous_intros)
   15.44  
   15.45  lemma borel_measurable_setprod[measurable (raw)]:
   15.46    fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> 'b::{second_countable_topology, real_normed_field}"
   15.47 @@ -705,14 +705,14 @@
   15.48    assumes f: "f \<in> borel_measurable M"
   15.49    assumes g: "g \<in> borel_measurable M"
   15.50    shows "(\<lambda>x. dist (f x) (g x)) \<in> borel_measurable M"
   15.51 -  using f g by (rule borel_measurable_continuous_Pair) (intro continuous_on_intros)
   15.52 +  using f g by (rule borel_measurable_continuous_Pair) (intro continuous_intros)
   15.53    
   15.54  lemma borel_measurable_scaleR[measurable (raw)]:
   15.55    fixes g :: "'a \<Rightarrow> 'b::{second_countable_topology, real_normed_vector}"
   15.56    assumes f: "f \<in> borel_measurable M"
   15.57    assumes g: "g \<in> borel_measurable M"
   15.58    shows "(\<lambda>x. f x *\<^sub>R g x) \<in> borel_measurable M"
   15.59 -  using f g by (rule borel_measurable_continuous_Pair) (intro continuous_on_intros)
   15.60 +  using f g by (rule borel_measurable_continuous_Pair) (intro continuous_intros)
   15.61  
   15.62  lemma affine_borel_measurable_vector:
   15.63    fixes f :: "'a \<Rightarrow> 'x::real_normed_vector"
   15.64 @@ -749,7 +749,7 @@
   15.65    shows "(\<lambda>x. inverse (f x)) \<in> borel_measurable M"
   15.66  proof -
   15.67    have "(\<lambda>x::'b. if x \<in> UNIV - {0} then inverse x else inverse 0) \<in> borel_measurable borel"
   15.68 -    by (intro borel_measurable_continuous_on_open' continuous_on_intros) auto
   15.69 +    by (intro borel_measurable_continuous_on_open' continuous_intros) auto
   15.70    also have "(\<lambda>x::'b. if x \<in> UNIV - {0} then inverse x else inverse 0) = inverse"
   15.71      by (intro ext) auto
   15.72    finally show ?thesis using f by simp
    16.1 --- a/src/HOL/Probability/Distributions.thy	Wed Apr 02 18:35:02 2014 +0200
    16.2 +++ b/src/HOL/Probability/Distributions.thy	Wed Apr 02 18:35:07 2014 +0200
    16.3 @@ -180,7 +180,7 @@
    16.4        show "DERIV (\<lambda>x. x * exp (-x)) x :> exp (-x) - x * exp (-x)"
    16.5          by (auto intro!: DERIV_intros)
    16.6        show "isCont (\<lambda>x. exp (- x) - x * exp (- x)) x "
    16.7 -        by (intro isCont_intros isCont_exp')
    16.8 +        by (intro continuous_intros)
    16.9      qed fact
   16.10      also have "(\<integral>x. (exp (-x)) * indicator {0 .. b} x \<partial>lborel) = - exp (- b) - - exp (- 0)"
   16.11        by (rule integral_FTC_atLeastAtMost) (auto intro!: DERIV_intros)
    17.1 --- a/src/HOL/Topological_Spaces.thy	Wed Apr 02 18:35:02 2014 +0200
    17.2 +++ b/src/HOL/Topological_Spaces.thy	Wed Apr 02 18:35:07 2014 +0200
    17.3 @@ -9,6 +9,18 @@
    17.4  imports Main Conditionally_Complete_Lattices
    17.5  begin
    17.6  
    17.7 +ML {*
    17.8 +
    17.9 +structure Continuous_Intros = Named_Thms
   17.10 +(
   17.11 +  val name = @{binding continuous_intros}
   17.12 +  val description = "Structural introduction rules for continuity"
   17.13 +)
   17.14 +
   17.15 +*}
   17.16 +
   17.17 +setup Continuous_Intros.setup
   17.18 +
   17.19  subsection {* Topological space *}
   17.20  
   17.21  class "open" =
   17.22 @@ -24,19 +36,19 @@
   17.23    closed :: "'a set \<Rightarrow> bool" where
   17.24    "closed S \<longleftrightarrow> open (- S)"
   17.25  
   17.26 -lemma open_empty [intro, simp]: "open {}"
   17.27 +lemma open_empty [continuous_intros, intro, simp]: "open {}"
   17.28    using open_Union [of "{}"] by simp
   17.29  
   17.30 -lemma open_Un [intro]: "open S \<Longrightarrow> open T \<Longrightarrow> open (S \<union> T)"
   17.31 +lemma open_Un [continuous_intros, intro]: "open S \<Longrightarrow> open T \<Longrightarrow> open (S \<union> T)"
   17.32    using open_Union [of "{S, T}"] by simp
   17.33  
   17.34 -lemma open_UN [intro]: "\<forall>x\<in>A. open (B x) \<Longrightarrow> open (\<Union>x\<in>A. B x)"
   17.35 +lemma open_UN [continuous_intros, intro]: "\<forall>x\<in>A. open (B x) \<Longrightarrow> open (\<Union>x\<in>A. B x)"
   17.36    using open_Union [of "B ` A"] by simp
   17.37  
   17.38 -lemma open_Inter [intro]: "finite S \<Longrightarrow> \<forall>T\<in>S. open T \<Longrightarrow> open (\<Inter>S)"
   17.39 +lemma open_Inter [continuous_intros, intro]: "finite S \<Longrightarrow> \<forall>T\<in>S. open T \<Longrightarrow> open (\<Inter>S)"
   17.40    by (induct set: finite) auto
   17.41  
   17.42 -lemma open_INT [intro]: "finite A \<Longrightarrow> \<forall>x\<in>A. open (B x) \<Longrightarrow> open (\<Inter>x\<in>A. B x)"
   17.43 +lemma open_INT [continuous_intros, intro]: "finite A \<Longrightarrow> \<forall>x\<in>A. open (B x) \<Longrightarrow> open (\<Inter>x\<in>A. B x)"
   17.44    using open_Inter [of "B ` A"] by simp
   17.45  
   17.46  lemma openI:
   17.47 @@ -48,28 +60,28 @@
   17.48    ultimately show "open S" by simp
   17.49  qed
   17.50  
   17.51 -lemma closed_empty [intro, simp]:  "closed {}"
   17.52 +lemma closed_empty [continuous_intros, intro, simp]:  "closed {}"
   17.53    unfolding closed_def by simp
   17.54  
   17.55 -lemma closed_Un [intro]: "closed S \<Longrightarrow> closed T \<Longrightarrow> closed (S \<union> T)"
   17.56 +lemma closed_Un [continuous_intros, intro]: "closed S \<Longrightarrow> closed T \<Longrightarrow> closed (S \<union> T)"
   17.57    unfolding closed_def by auto
   17.58  
   17.59 -lemma closed_UNIV [intro, simp]: "closed UNIV"
   17.60 +lemma closed_UNIV [continuous_intros, intro, simp]: "closed UNIV"
   17.61    unfolding closed_def by simp
   17.62  
   17.63 -lemma closed_Int [intro]: "closed S \<Longrightarrow> closed T \<Longrightarrow> closed (S \<inter> T)"
   17.64 +lemma closed_Int [continuous_intros, intro]: "closed S \<Longrightarrow> closed T \<Longrightarrow> closed (S \<inter> T)"
   17.65    unfolding closed_def by auto
   17.66  
   17.67 -lemma closed_INT [intro]: "\<forall>x\<in>A. closed (B x) \<Longrightarrow> closed (\<Inter>x\<in>A. B x)"
   17.68 +lemma closed_INT [continuous_intros, intro]: "\<forall>x\<in>A. closed (B x) \<Longrightarrow> closed (\<Inter>x\<in>A. B x)"
   17.69    unfolding closed_def by auto
   17.70  
   17.71 -lemma closed_Inter [intro]: "\<forall>S\<in>K. closed S \<Longrightarrow> closed (\<Inter> K)"
   17.72 +lemma closed_Inter [continuous_intros, intro]: "\<forall>S\<in>K. closed S \<Longrightarrow> closed (\<Inter> K)"
   17.73    unfolding closed_def uminus_Inf by auto
   17.74  
   17.75 -lemma closed_Union [intro]: "finite S \<Longrightarrow> \<forall>T\<in>S. closed T \<Longrightarrow> closed (\<Union>S)"
   17.76 +lemma closed_Union [continuous_intros, intro]: "finite S \<Longrightarrow> \<forall>T\<in>S. closed T \<Longrightarrow> closed (\<Union>S)"
   17.77    by (induct set: finite) auto
   17.78  
   17.79 -lemma closed_UN [intro]: "finite A \<Longrightarrow> \<forall>x\<in>A. closed (B x) \<Longrightarrow> closed (\<Union>x\<in>A. B x)"
   17.80 +lemma closed_UN [continuous_intros, intro]: "finite A \<Longrightarrow> \<forall>x\<in>A. closed (B x) \<Longrightarrow> closed (\<Union>x\<in>A. B x)"
   17.81    using closed_Union [of "B ` A"] by simp
   17.82  
   17.83  lemma open_closed: "open S \<longleftrightarrow> closed (- S)"
   17.84 @@ -78,16 +90,16 @@
   17.85  lemma closed_open: "closed S \<longleftrightarrow> open (- S)"
   17.86    unfolding closed_def by simp
   17.87  
   17.88 -lemma open_Diff [intro]: "open S \<Longrightarrow> closed T \<Longrightarrow> open (S - T)"
   17.89 +lemma open_Diff [continuous_intros, intro]: "open S \<Longrightarrow> closed T \<Longrightarrow> open (S - T)"
   17.90    unfolding closed_open Diff_eq by (rule open_Int)
   17.91  
   17.92 -lemma closed_Diff [intro]: "closed S \<Longrightarrow> open T \<Longrightarrow> closed (S - T)"
   17.93 +lemma closed_Diff [continuous_intros, intro]: "closed S \<Longrightarrow> open T \<Longrightarrow> closed (S - T)"
   17.94    unfolding open_closed Diff_eq by (rule closed_Int)
   17.95  
   17.96 -lemma open_Compl [intro]: "closed S \<Longrightarrow> open (- S)"
   17.97 +lemma open_Compl [continuous_intros, intro]: "closed S \<Longrightarrow> open (- S)"
   17.98    unfolding closed_open .
   17.99  
  17.100 -lemma closed_Compl [intro]: "open S \<Longrightarrow> closed (- S)"
  17.101 +lemma closed_Compl [continuous_intros, intro]: "open S \<Longrightarrow> closed (- S)"
  17.102    unfolding open_closed .
  17.103  
  17.104  end
  17.105 @@ -119,7 +131,7 @@
  17.106    finally show "closed {a}" unfolding closed_def .
  17.107  qed
  17.108  
  17.109 -lemma closed_insert [simp]:
  17.110 +lemma closed_insert [continuous_intros, simp]:
  17.111    fixes a :: "'a::t1_space"
  17.112    assumes "closed S" shows "closed (insert a S)"
  17.113  proof -
  17.114 @@ -185,26 +197,26 @@
  17.115    unfolding open_generated_order
  17.116    by (rule topological_space_generate_topology)
  17.117  
  17.118 -lemma open_greaterThan [simp]: "open {a <..}"
  17.119 +lemma open_greaterThan [continuous_intros, simp]: "open {a <..}"
  17.120    unfolding open_generated_order by (auto intro: generate_topology.Basis)
  17.121  
  17.122 -lemma open_lessThan [simp]: "open {..< a}"
  17.123 +lemma open_lessThan [continuous_intros, simp]: "open {..< a}"
  17.124    unfolding open_generated_order by (auto intro: generate_topology.Basis)
  17.125  
  17.126 -lemma open_greaterThanLessThan [simp]: "open {a <..< b}"
  17.127 +lemma open_greaterThanLessThan [continuous_intros, simp]: "open {a <..< b}"
  17.128     unfolding greaterThanLessThan_eq by (simp add: open_Int)
  17.129  
  17.130  end
  17.131  
  17.132  class linorder_topology = linorder + order_topology
  17.133  
  17.134 -lemma closed_atMost [simp]: "closed {.. a::'a::linorder_topology}"
  17.135 +lemma closed_atMost [continuous_intros, simp]: "closed {.. a::'a::linorder_topology}"
  17.136    by (simp add: closed_open)
  17.137  
  17.138 -lemma closed_atLeast [simp]: "closed {a::'a::linorder_topology ..}"
  17.139 +lemma closed_atLeast [continuous_intros, simp]: "closed {a::'a::linorder_topology ..}"
  17.140    by (simp add: closed_open)
  17.141  
  17.142 -lemma closed_atLeastAtMost [simp]: "closed {a::'a::linorder_topology .. b}"
  17.143 +lemma closed_atLeastAtMost [continuous_intros, simp]: "closed {a::'a::linorder_topology .. b}"
  17.144  proof -
  17.145    have "{a .. b} = {a ..} \<inter> {.. b}"
  17.146      by auto
  17.147 @@ -1725,7 +1737,7 @@
  17.148      shows "open (f -` B)"
  17.149  by (metis assms continuous_on_open_vimage le_iff_inf)
  17.150  
  17.151 -corollary open_vimage:
  17.152 +corollary open_vimage[continuous_intros]:
  17.153    assumes "open s" and "continuous_on UNIV f"
  17.154    shows "open (f -` s)"
  17.155    using assms unfolding continuous_on_open_vimage [OF open_UNIV]
  17.156 @@ -1745,6 +1757,12 @@
  17.157    unfolding continuous_on_closed_invariant
  17.158    by (metis closed_Int Int_absorb Int_commute[of s] Int_assoc[of _ _ s])
  17.159  
  17.160 +corollary closed_vimage[continuous_intros]:
  17.161 +  assumes "closed s" and "continuous_on UNIV f"
  17.162 +  shows "closed (f -` s)"
  17.163 +  using assms unfolding continuous_on_closed_vimage [OF closed_UNIV]
  17.164 +  by simp
  17.165 +
  17.166  lemma continuous_on_open_Union:
  17.167    "(\<And>s. s \<in> S \<Longrightarrow> open s) \<Longrightarrow> (\<And>s. s \<in> S \<Longrightarrow> continuous_on s f) \<Longrightarrow> continuous_on (\<Union>S) f"
  17.168    unfolding continuous_on_def by safe (metis open_Union at_within_open UnionI)
  17.169 @@ -1770,25 +1788,13 @@
  17.170      by (rule continuous_on_closed_Un)
  17.171  qed
  17.172  
  17.173 -ML {*
  17.174 -
  17.175 -structure Continuous_On_Intros = Named_Thms
  17.176 -(
  17.177 -  val name = @{binding continuous_on_intros}
  17.178 -  val description = "Structural introduction rules for setwise continuity"
  17.179 -)
  17.180 -
  17.181 -*}
  17.182 -
  17.183 -setup Continuous_On_Intros.setup
  17.184 -
  17.185 -lemma continuous_on_id[continuous_on_intros]: "continuous_on s (\<lambda>x. x)"
  17.186 +lemma continuous_on_id[continuous_intros]: "continuous_on s (\<lambda>x. x)"
  17.187    unfolding continuous_on_def by (fast intro: tendsto_ident_at)
  17.188  
  17.189 -lemma continuous_on_const[continuous_on_intros]: "continuous_on s (\<lambda>x. c)"
  17.190 +lemma continuous_on_const[continuous_intros]: "continuous_on s (\<lambda>x. c)"
  17.191    unfolding continuous_on_def by (auto intro: tendsto_const)
  17.192  
  17.193 -lemma continuous_on_compose[continuous_on_intros]:
  17.194 +lemma continuous_on_compose[continuous_intros]:
  17.195    "continuous_on s f \<Longrightarrow> continuous_on (f ` s) g \<Longrightarrow> continuous_on s (g o f)"
  17.196    unfolding continuous_on_topological by simp metis
  17.197  
  17.198 @@ -1801,18 +1807,6 @@
  17.199  definition continuous :: "'a::t2_space filter \<Rightarrow> ('a \<Rightarrow> 'b::topological_space) \<Rightarrow> bool" where
  17.200    "continuous F f \<longleftrightarrow> (f ---> f (Lim F (\<lambda>x. x))) F"
  17.201  
  17.202 -ML {*
  17.203 -
  17.204 -structure Continuous_Intros = Named_Thms
  17.205 -(
  17.206 -  val name = @{binding continuous_intros}
  17.207 -  val description = "Structural introduction rules for pointwise continuity"
  17.208 -)
  17.209 -
  17.210 -*}
  17.211 -
  17.212 -setup Continuous_Intros.setup
  17.213 -
  17.214  lemma continuous_bot[continuous_intros, simp]: "continuous bot f"
  17.215    unfolding continuous_def by auto
  17.216  
    18.1 --- a/src/HOL/Transcendental.thy	Wed Apr 02 18:35:02 2014 +0200
    18.2 +++ b/src/HOL/Transcendental.thy	Wed Apr 02 18:35:07 2014 +0200
    18.3 @@ -994,7 +994,7 @@
    18.4    "continuous F f \<Longrightarrow> continuous F (\<lambda>x. exp (f x))"
    18.5    unfolding continuous_def by (rule tendsto_exp)
    18.6  
    18.7 -lemma continuous_on_exp [continuous_on_intros]:
    18.8 +lemma continuous_on_exp [continuous_intros]:
    18.9    "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. exp (f x))"
   18.10    unfolding continuous_on_def by (auto intro: tendsto_exp)
   18.11  
   18.12 @@ -1303,7 +1303,7 @@
   18.13    "continuous (at x within s) f \<Longrightarrow> 0 < f x \<Longrightarrow> continuous (at x within s) (\<lambda>x. ln (f x))"
   18.14    unfolding continuous_within by (rule tendsto_ln)
   18.15  
   18.16 -lemma continuous_on_ln [continuous_on_intros]:
   18.17 +lemma continuous_on_ln [continuous_intros]:
   18.18    "continuous_on s f \<Longrightarrow> (\<forall>x\<in>s. 0 < f x) \<Longrightarrow> continuous_on s (\<lambda>x. ln (f x))"
   18.19    unfolding continuous_on_def by (auto intro: tendsto_ln)
   18.20  
   18.21 @@ -1747,7 +1747,7 @@
   18.22    shows "isCont (\<lambda>x. log (f x) (g x)) a"
   18.23    using assms unfolding continuous_at by (rule tendsto_log)
   18.24  
   18.25 -lemma continuous_on_log[continuous_on_intros]:
   18.26 +lemma continuous_on_log[continuous_intros]:
   18.27    assumes "continuous_on s f" "continuous_on s g"
   18.28      and "\<forall>x\<in>s. 0 < f x" "\<forall>x\<in>s. f x \<noteq> 1" "\<forall>x\<in>s. 0 < g x"
   18.29    shows "continuous_on s (\<lambda>x. log (f x) (g x))"
   18.30 @@ -2076,7 +2076,7 @@
   18.31    shows "isCont (\<lambda>x. (f x) powr g x) a"
   18.32    using assms unfolding continuous_at by (rule tendsto_powr)
   18.33  
   18.34 -lemma continuous_on_powr[continuous_on_intros]:
   18.35 +lemma continuous_on_powr[continuous_intros]:
   18.36    assumes "continuous_on s f" "continuous_on s g" and "\<forall>x\<in>s. 0 < f x"
   18.37    shows "continuous_on s (\<lambda>x. (f x) powr (g x))"
   18.38    using assms unfolding continuous_on_def by (fast intro: tendsto_powr)
   18.39 @@ -2215,7 +2215,7 @@
   18.40    "continuous F f \<Longrightarrow> continuous F (\<lambda>x. sin (f x))"
   18.41    unfolding continuous_def by (rule tendsto_sin)
   18.42  
   18.43 -lemma continuous_on_sin [continuous_on_intros]:
   18.44 +lemma continuous_on_sin [continuous_intros]:
   18.45    "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. sin (f x))"
   18.46    unfolding continuous_on_def by (auto intro: tendsto_sin)
   18.47  
   18.48 @@ -2223,7 +2223,7 @@
   18.49    "continuous F f \<Longrightarrow> continuous F (\<lambda>x. cos (f x))"
   18.50    unfolding continuous_def by (rule tendsto_cos)
   18.51  
   18.52 -lemma continuous_on_cos [continuous_on_intros]:
   18.53 +lemma continuous_on_cos [continuous_intros]:
   18.54    "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. cos (f x))"
   18.55    unfolding continuous_on_def by (auto intro: tendsto_cos)
   18.56  
   18.57 @@ -2884,7 +2884,7 @@
   18.58    "continuous (at x within s) f \<Longrightarrow> cos (f x) \<noteq> 0 \<Longrightarrow> continuous (at x within s) (\<lambda>x. tan (f x))"
   18.59    unfolding continuous_within by (rule tendsto_tan)
   18.60  
   18.61 -lemma continuous_on_tan [continuous_on_intros]:
   18.62 +lemma continuous_on_tan [continuous_intros]:
   18.63    "continuous_on s f \<Longrightarrow> (\<forall>x\<in>s. cos (f x) \<noteq> 0) \<Longrightarrow> continuous_on s (\<lambda>x. tan (f x))"
   18.64    unfolding continuous_on_def by (auto intro: tendsto_tan)
   18.65  
   18.66 @@ -3232,7 +3232,7 @@
   18.67  lemma continuous_on_arcsin': "continuous_on {-1 .. 1} arcsin"
   18.68  proof -
   18.69    have "continuous_on (sin ` {- pi / 2 .. pi / 2}) arcsin"
   18.70 -    by (rule continuous_on_inv) (auto intro: continuous_on_intros simp: arcsin_sin)
   18.71 +    by (rule continuous_on_inv) (auto intro: continuous_intros simp: arcsin_sin)
   18.72    also have "sin ` {- pi / 2 .. pi / 2} = {-1 .. 1}"
   18.73    proof safe
   18.74      fix x :: real
   18.75 @@ -3244,7 +3244,7 @@
   18.76    finally show ?thesis .
   18.77  qed
   18.78  
   18.79 -lemma continuous_on_arcsin [continuous_on_intros]:
   18.80 +lemma continuous_on_arcsin [continuous_intros]:
   18.81    "continuous_on s f \<Longrightarrow> (\<forall>x\<in>s. -1 \<le> f x \<and> f x \<le> 1) \<Longrightarrow> continuous_on s (\<lambda>x. arcsin (f x))"
   18.82    using continuous_on_compose[of s f, OF _ continuous_on_subset[OF  continuous_on_arcsin']]
   18.83    by (auto simp: comp_def subset_eq)
   18.84 @@ -3256,7 +3256,7 @@
   18.85  lemma continuous_on_arccos': "continuous_on {-1 .. 1} arccos"
   18.86  proof -
   18.87    have "continuous_on (cos ` {0 .. pi}) arccos"
   18.88 -    by (rule continuous_on_inv) (auto intro: continuous_on_intros simp: arccos_cos)
   18.89 +    by (rule continuous_on_inv) (auto intro: continuous_intros simp: arccos_cos)
   18.90    also have "cos ` {0 .. pi} = {-1 .. 1}"
   18.91    proof safe
   18.92      fix x :: real
   18.93 @@ -3268,7 +3268,7 @@
   18.94    finally show ?thesis .
   18.95  qed
   18.96  
   18.97 -lemma continuous_on_arccos [continuous_on_intros]:
   18.98 +lemma continuous_on_arccos [continuous_intros]:
   18.99    "continuous_on s f \<Longrightarrow> (\<forall>x\<in>s. -1 \<le> f x \<and> f x \<le> 1) \<Longrightarrow> continuous_on s (\<lambda>x. arccos (f x))"
  18.100    using continuous_on_compose[of s f, OF _ continuous_on_subset[OF  continuous_on_arccos']]
  18.101    by (auto simp: comp_def subset_eq)
  18.102 @@ -3292,7 +3292,7 @@
  18.103  lemma continuous_arctan [continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. arctan (f x))"
  18.104    unfolding continuous_def by (rule tendsto_arctan)
  18.105  
  18.106 -lemma continuous_on_arctan [continuous_on_intros]: "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. arctan (f x))"
  18.107 +lemma continuous_on_arctan [continuous_intros]: "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. arctan (f x))"
  18.108    unfolding continuous_on_def by (auto intro: tendsto_arctan)
  18.109  
  18.110  lemma DERIV_arcsin: