changed continuous_on_intros into a named theorems collection
authorhoelzl
Wed Mar 06 16:56:21 2013 +0100 (2013-03-06)
changeset 51362dac3f564a98d
parent 51361 21e5b6efb317
child 51363 d4d00c804645
changed continuous_on_intros into a named theorems collection
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Mar 06 16:56:21 2013 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Mar 06 16:56:21 2013 +0100
     1.3 @@ -4257,67 +4257,79 @@
     1.4  
     1.5  subsubsection {* Structural rules for setwise continuity *}
     1.6  
     1.7 -lemma continuous_on_id: "continuous_on s (\<lambda>x. x)"
     1.8 +ML {*
     1.9 +
    1.10 +structure Continuous_On_Intros = Named_Thms
    1.11 +(
    1.12 +  val name = @{binding continuous_on_intros}
    1.13 +  val description = "Structural introduction rules for setwise continuity"
    1.14 +)
    1.15 +
    1.16 +*}
    1.17 +
    1.18 +setup Continuous_On_Intros.setup
    1.19 +
    1.20 +lemma continuous_on_id[continuous_on_intros]: "continuous_on s (\<lambda>x. x)"
    1.21    unfolding continuous_on_def by (fast intro: tendsto_ident_at_within)
    1.22  
    1.23 -lemma continuous_on_const: "continuous_on s (\<lambda>x. c)"
    1.24 +lemma continuous_on_const[continuous_on_intros]: "continuous_on s (\<lambda>x. c)"
    1.25    unfolding continuous_on_def by (auto intro: tendsto_intros)
    1.26  
    1.27 -lemma continuous_on_norm:
    1.28 +lemma continuous_on_norm[continuous_on_intros]:
    1.29    shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. norm (f x))"
    1.30    unfolding continuous_on_def by (fast intro: tendsto_norm)
    1.31  
    1.32 -lemma continuous_on_infnorm:
    1.33 +lemma continuous_on_infnorm[continuous_on_intros]:
    1.34    shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. infnorm (f x))"
    1.35    unfolding continuous_on by (fast intro: tendsto_infnorm)
    1.36  
    1.37 -lemma continuous_on_minus:
    1.38 +lemma continuous_on_minus[continuous_on_intros]:
    1.39    fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
    1.40    shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. - f x)"
    1.41    unfolding continuous_on_def by (auto intro: tendsto_intros)
    1.42  
    1.43 -lemma continuous_on_add:
    1.44 +lemma continuous_on_add[continuous_on_intros]:
    1.45    fixes f g :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
    1.46    shows "continuous_on s f \<Longrightarrow> continuous_on s g
    1.47             \<Longrightarrow> continuous_on s (\<lambda>x. f x + g x)"
    1.48    unfolding continuous_on_def by (auto intro: tendsto_intros)
    1.49  
    1.50 -lemma continuous_on_diff:
    1.51 +lemma continuous_on_diff[continuous_on_intros]:
    1.52    fixes f g :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
    1.53    shows "continuous_on s f \<Longrightarrow> continuous_on s g
    1.54             \<Longrightarrow> continuous_on s (\<lambda>x. f x - g x)"
    1.55    unfolding continuous_on_def by (auto intro: tendsto_intros)
    1.56  
    1.57 -lemma (in bounded_linear) continuous_on:
    1.58 +lemma (in bounded_linear) continuous_on[continuous_on_intros]:
    1.59    "continuous_on s g \<Longrightarrow> continuous_on s (\<lambda>x. f (g x))"
    1.60    unfolding continuous_on_def by (fast intro: tendsto)
    1.61  
    1.62 -lemma (in bounded_bilinear) continuous_on:
    1.63 +lemma (in bounded_bilinear) continuous_on[continuous_on_intros]:
    1.64    "\<lbrakk>continuous_on s f; continuous_on s g\<rbrakk> \<Longrightarrow> continuous_on s (\<lambda>x. f x ** g x)"
    1.65    unfolding continuous_on_def by (fast intro: tendsto)
    1.66  
    1.67 -lemma continuous_on_scaleR:
    1.68 +lemma continuous_on_scaleR[continuous_on_intros]:
    1.69    fixes g :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
    1.70    assumes "continuous_on s f" and "continuous_on s g"
    1.71    shows "continuous_on s (\<lambda>x. f x *\<^sub>R g x)"
    1.72    using bounded_bilinear_scaleR assms
    1.73    by (rule bounded_bilinear.continuous_on)
    1.74  
    1.75 -lemma continuous_on_mult:
    1.76 +lemma continuous_on_mult[continuous_on_intros]:
    1.77    fixes g :: "'a::topological_space \<Rightarrow> 'b::real_normed_algebra"
    1.78    assumes "continuous_on s f" and "continuous_on s g"
    1.79    shows "continuous_on s (\<lambda>x. f x * g x)"
    1.80    using bounded_bilinear_mult assms
    1.81    by (rule bounded_bilinear.continuous_on)
    1.82  
    1.83 -lemma continuous_on_inner:
    1.84 +lemma continuous_on_inner[continuous_on_intros]:
    1.85    fixes g :: "'a::topological_space \<Rightarrow> 'b::real_inner"
    1.86    assumes "continuous_on s f" and "continuous_on s g"
    1.87    shows "continuous_on s (\<lambda>x. inner (f x) (g x))"
    1.88    using bounded_bilinear_inner assms
    1.89    by (rule bounded_bilinear.continuous_on)
    1.90  
    1.91 -lemma continuous_on_inverse:
    1.92 +lemma continuous_on_inverse[continuous_on_intros]:
    1.93    fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_div_algebra"
    1.94    assumes "continuous_on s f" and "\<forall>x\<in>s. f x \<noteq> 0"
    1.95    shows "continuous_on s (\<lambda>x. inverse (f x))"
    1.96 @@ -4325,15 +4337,15 @@
    1.97  
    1.98  subsubsection {* Structural rules for uniform continuity *}
    1.99  
   1.100 -lemma uniformly_continuous_on_id:
   1.101 +lemma uniformly_continuous_on_id[continuous_on_intros]:
   1.102    shows "uniformly_continuous_on s (\<lambda>x. x)"
   1.103    unfolding uniformly_continuous_on_def by auto
   1.104  
   1.105 -lemma uniformly_continuous_on_const:
   1.106 +lemma uniformly_continuous_on_const[continuous_on_intros]:
   1.107    shows "uniformly_continuous_on s (\<lambda>x. c)"
   1.108    unfolding uniformly_continuous_on_def by simp
   1.109  
   1.110 -lemma uniformly_continuous_on_dist:
   1.111 +lemma uniformly_continuous_on_dist[continuous_on_intros]:
   1.112    fixes f g :: "'a::metric_space \<Rightarrow> 'b::metric_space"
   1.113    assumes "uniformly_continuous_on s f"
   1.114    assumes "uniformly_continuous_on s g"
   1.115 @@ -4355,20 +4367,20 @@
   1.116      unfolding dist_real_def by simp
   1.117  qed
   1.118  
   1.119 -lemma uniformly_continuous_on_norm:
   1.120 +lemma uniformly_continuous_on_norm[continuous_on_intros]:
   1.121    assumes "uniformly_continuous_on s f"
   1.122    shows "uniformly_continuous_on s (\<lambda>x. norm (f x))"
   1.123    unfolding norm_conv_dist using assms
   1.124    by (intro uniformly_continuous_on_dist uniformly_continuous_on_const)
   1.125  
   1.126 -lemma (in bounded_linear) uniformly_continuous_on:
   1.127 +lemma (in bounded_linear) uniformly_continuous_on[continuous_on_intros]:
   1.128    assumes "uniformly_continuous_on s g"
   1.129    shows "uniformly_continuous_on s (\<lambda>x. f (g x))"
   1.130    using assms unfolding uniformly_continuous_on_sequentially
   1.131    unfolding dist_norm tendsto_norm_zero_iff diff[symmetric]
   1.132    by (auto intro: tendsto_zero)
   1.133  
   1.134 -lemma uniformly_continuous_on_cmul:
   1.135 +lemma uniformly_continuous_on_cmul[continuous_on_intros]:
   1.136    fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
   1.137    assumes "uniformly_continuous_on s f"
   1.138    shows "uniformly_continuous_on s (\<lambda>x. c *\<^sub>R f(x))"
   1.139 @@ -4380,12 +4392,12 @@
   1.140    shows "dist (- x) (- y) = dist x y"
   1.141    unfolding dist_norm minus_diff_minus norm_minus_cancel ..
   1.142  
   1.143 -lemma uniformly_continuous_on_minus:
   1.144 +lemma uniformly_continuous_on_minus[continuous_on_intros]:
   1.145    fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
   1.146    shows "uniformly_continuous_on s f \<Longrightarrow> uniformly_continuous_on s (\<lambda>x. - f x)"
   1.147    unfolding uniformly_continuous_on_def dist_minus .
   1.148  
   1.149 -lemma uniformly_continuous_on_add:
   1.150 +lemma uniformly_continuous_on_add[continuous_on_intros]:
   1.151    fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
   1.152    assumes "uniformly_continuous_on s f"
   1.153    assumes "uniformly_continuous_on s g"
   1.154 @@ -4394,7 +4406,7 @@
   1.155    unfolding dist_norm tendsto_norm_zero_iff add_diff_add
   1.156    by (auto intro: tendsto_add_zero)
   1.157  
   1.158 -lemma uniformly_continuous_on_diff:
   1.159 +lemma uniformly_continuous_on_diff[continuous_on_intros]:
   1.160    fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
   1.161    assumes "uniformly_continuous_on s f" and "uniformly_continuous_on s g"
   1.162    shows "uniformly_continuous_on s (\<lambda>x. f x - g x)"
   1.163 @@ -4411,13 +4423,13 @@
   1.164  unfolding tendsto_def Limits.eventually_within eventually_at_topological
   1.165  by (intro ball_cong [OF refl] all_cong imp_cong ex_cong conj_cong refl) auto
   1.166  
   1.167 -lemma continuous_within_compose:
   1.168 +lemma continuous_within_compose[continuous_intros]:
   1.169    assumes "continuous (at x within s) f"
   1.170    assumes "continuous (at (f x) within f ` s) g"
   1.171    shows "continuous (at x within s) (g o f)"
   1.172  using assms unfolding continuous_within_topological by simp metis
   1.173  
   1.174 -lemma continuous_at_compose:
   1.175 +lemma continuous_at_compose[continuous_intros]:
   1.176    assumes "continuous (at x) f" and "continuous (at (f x)) g"
   1.177    shows "continuous (at x) (g o f)"
   1.178  proof-
   1.179 @@ -4427,11 +4439,11 @@
   1.180      using continuous_within_compose[of x UNIV f g] by simp
   1.181  qed
   1.182  
   1.183 -lemma continuous_on_compose:
   1.184 +lemma continuous_on_compose[continuous_on_intros]:
   1.185    "continuous_on s f \<Longrightarrow> continuous_on (f ` s) g \<Longrightarrow> continuous_on s (g o f)"
   1.186    unfolding continuous_on_topological by simp metis
   1.187  
   1.188 -lemma uniformly_continuous_on_compose:
   1.189 +lemma uniformly_continuous_on_compose[continuous_on_intros]:
   1.190    assumes "uniformly_continuous_on s f"  "uniformly_continuous_on (f ` s) g"
   1.191    shows "uniformly_continuous_on s (g o f)"
   1.192  proof-
   1.193 @@ -4442,17 +4454,6 @@
   1.194    thus ?thesis using assms unfolding uniformly_continuous_on_def by auto
   1.195  qed
   1.196  
   1.197 -lemmas continuous_on_intros = continuous_on_id continuous_on_const
   1.198 -  continuous_on_compose continuous_on_norm continuous_on_infnorm
   1.199 -  continuous_on_add continuous_on_minus continuous_on_diff
   1.200 -  continuous_on_scaleR continuous_on_mult continuous_on_inverse
   1.201 -  continuous_on_inner
   1.202 -  uniformly_continuous_on_id uniformly_continuous_on_const
   1.203 -  uniformly_continuous_on_dist uniformly_continuous_on_norm
   1.204 -  uniformly_continuous_on_compose uniformly_continuous_on_add
   1.205 -  uniformly_continuous_on_minus uniformly_continuous_on_diff
   1.206 -  uniformly_continuous_on_cmul
   1.207 -
   1.208  text{* Continuity in terms of open preimages. *}
   1.209  
   1.210  lemma continuous_at_open: