--- a/NEWS Wed Apr 02 18:35:02 2014 +0200
+++ b/NEWS Wed Apr 02 18:35:07 2014 +0200
@@ -543,6 +543,9 @@
deriv_fderiv ~> has_field_derivative_def
INCOMPATIBILITY.
+* Include more theorems in continuous_intros. Remove the continuous_on_intros,
+ isCont_intros collections, these facts are now in continuous_intros.
+
* Removed solvers remote_cvc3 and remote_z3. Use cvc3 and z3 instead.
* Nitpick:
--- a/src/HOL/Deriv.thy Wed Apr 02 18:35:02 2014 +0200
+++ b/src/HOL/Deriv.thy Wed Apr 02 18:35:07 2014 +0200
@@ -1116,7 +1116,7 @@
proof -
let ?F = "%x. f x - ((f b - f a) / (b-a)) * x"
have contF: "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont ?F x"
- using con by (fast intro: isCont_intros)
+ using con by (fast intro: continuous_intros)
have difF: "\<forall>x. a < x \<and> x < b \<longrightarrow> ?F differentiable (at x)"
proof (clarify)
fix x::real
--- a/src/HOL/Library/Product_Vector.thy Wed Apr 02 18:35:02 2014 +0200
+++ b/src/HOL/Library/Product_Vector.thy Wed Apr 02 18:35:07 2014 +0200
@@ -204,13 +204,13 @@
lemma continuous_Pair[continuous_intros]: "continuous F f \<Longrightarrow> continuous F g \<Longrightarrow> continuous F (\<lambda>x. (f x, g x))"
unfolding continuous_def by (rule tendsto_Pair)
-lemma continuous_on_fst[continuous_on_intros]: "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. fst (f x))"
+lemma continuous_on_fst[continuous_intros]: "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. fst (f x))"
unfolding continuous_on_def by (auto intro: tendsto_fst)
-lemma continuous_on_snd[continuous_on_intros]: "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. snd (f x))"
+lemma continuous_on_snd[continuous_intros]: "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. snd (f x))"
unfolding continuous_on_def by (auto intro: tendsto_snd)
-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))"
+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))"
unfolding continuous_on_def by (auto intro: tendsto_Pair)
lemma isCont_fst [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. fst (f x)) a"
--- a/src/HOL/Limits.thy Wed Apr 02 18:35:02 2014 +0200
+++ b/src/HOL/Limits.thy Wed Apr 02 18:35:07 2014 +0200
@@ -436,7 +436,7 @@
shows "continuous F f \<Longrightarrow> continuous F g \<Longrightarrow> continuous F (\<lambda>x. dist (f x) (g x))"
unfolding continuous_def by (rule tendsto_dist)
-lemma continuous_on_dist[continuous_on_intros]:
+lemma continuous_on_dist[continuous_intros]:
fixes f g :: "_ \<Rightarrow> 'a :: metric_space"
shows "continuous_on s f \<Longrightarrow> continuous_on s g \<Longrightarrow> continuous_on s (\<lambda>x. dist (f x) (g x))"
unfolding continuous_on_def by (auto intro: tendsto_dist)
@@ -449,7 +449,7 @@
"continuous F f \<Longrightarrow> continuous F (\<lambda>x. norm (f x))"
unfolding continuous_def by (rule tendsto_norm)
-lemma continuous_on_norm [continuous_on_intros]:
+lemma continuous_on_norm [continuous_intros]:
"continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. norm (f x))"
unfolding continuous_on_def by (auto intro: tendsto_norm)
@@ -473,7 +473,7 @@
"continuous F f \<Longrightarrow> continuous F (\<lambda>x. \<bar>f x :: real\<bar>)"
unfolding real_norm_def[symmetric] by (rule continuous_norm)
-lemma continuous_on_rabs [continuous_on_intros]:
+lemma continuous_on_rabs [continuous_intros]:
"continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. \<bar>f x :: real\<bar>)"
unfolding real_norm_def[symmetric] by (rule continuous_on_norm)
@@ -501,7 +501,7 @@
shows "continuous F f \<Longrightarrow> continuous F g \<Longrightarrow> continuous F (\<lambda>x. f x + g x)"
unfolding continuous_def by (rule tendsto_add)
-lemma continuous_on_add [continuous_on_intros]:
+lemma continuous_on_add [continuous_intros]:
fixes f g :: "_ \<Rightarrow> 'b::real_normed_vector"
shows "continuous_on s f \<Longrightarrow> continuous_on s g \<Longrightarrow> continuous_on s (\<lambda>x. f x + g x)"
unfolding continuous_on_def by (auto intro: tendsto_add)
@@ -521,7 +521,7 @@
shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. - f x)"
unfolding continuous_def by (rule tendsto_minus)
-lemma continuous_on_minus [continuous_on_intros]:
+lemma continuous_on_minus [continuous_intros]:
fixes f :: "_ \<Rightarrow> 'b::real_normed_vector"
shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. - f x)"
unfolding continuous_on_def by (auto intro: tendsto_minus)
@@ -546,7 +546,7 @@
shows "continuous F f \<Longrightarrow> continuous F g \<Longrightarrow> continuous F (\<lambda>x. f x - g x)"
unfolding continuous_def by (rule tendsto_diff)
-lemma continuous_on_diff [continuous_on_intros]:
+lemma continuous_on_diff [continuous_intros]:
fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
shows "continuous_on s f \<Longrightarrow> continuous_on s g \<Longrightarrow> continuous_on s (\<lambda>x. f x - g x)"
unfolding continuous_on_def by (auto intro: tendsto_diff)
@@ -638,13 +638,13 @@
lemmas continuous_mult [continuous_intros] =
bounded_bilinear.continuous [OF bounded_bilinear_mult]
-lemmas continuous_on_of_real [continuous_on_intros] =
+lemmas continuous_on_of_real [continuous_intros] =
bounded_linear.continuous_on [OF bounded_linear_of_real]
-lemmas continuous_on_scaleR [continuous_on_intros] =
+lemmas continuous_on_scaleR [continuous_intros] =
bounded_bilinear.continuous_on [OF bounded_bilinear_scaleR]
-lemmas continuous_on_mult [continuous_on_intros] =
+lemmas continuous_on_mult [continuous_intros] =
bounded_bilinear.continuous_on [OF bounded_bilinear_mult]
lemmas tendsto_mult_zero =
@@ -666,7 +666,7 @@
shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. (f x)^n)"
unfolding continuous_def by (rule tendsto_power)
-lemma continuous_on_power [continuous_on_intros]:
+lemma continuous_on_power [continuous_intros]:
fixes f :: "_ \<Rightarrow> 'b::{power,real_normed_algebra}"
shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. (f x)^n)"
unfolding continuous_on_def by (auto intro: tendsto_power)
@@ -820,7 +820,7 @@
shows "isCont (\<lambda>x. inverse (f x)) a"
using assms unfolding continuous_at by (rule tendsto_inverse)
-lemma continuous_on_inverse[continuous_on_intros]:
+lemma continuous_on_inverse[continuous_intros]:
fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_div_algebra"
assumes "continuous_on s f" and "\<forall>x\<in>s. f x \<noteq> 0"
shows "continuous_on s (\<lambda>x. inverse (f x))"
@@ -850,7 +850,7 @@
shows "isCont (\<lambda>x. (f x) / g x) a"
using assms unfolding continuous_at by (rule tendsto_divide)
-lemma continuous_on_divide[continuous_on_intros]:
+lemma continuous_on_divide[continuous_intros]:
fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_field"
assumes "continuous_on s f" "continuous_on s g" and "\<forall>x\<in>s. g x \<noteq> 0"
shows "continuous_on s (\<lambda>x. (f x) / (g x))"
@@ -879,7 +879,7 @@
shows "isCont (\<lambda>x. sgn (f x)) a"
using assms unfolding continuous_at by (rule tendsto_sgn)
-lemma continuous_on_sgn[continuous_on_intros]:
+lemma continuous_on_sgn[continuous_intros]:
fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
assumes "continuous_on s f" and "\<forall>x\<in>s. f x \<noteq> 0"
shows "continuous_on s (\<lambda>x. sgn (f x))"
@@ -1685,11 +1685,6 @@
shows "\<forall>i\<in>A. isCont (f i) a \<Longrightarrow> isCont (\<lambda>x. \<Sum>i\<in>A. f i x) a"
by (auto intro: continuous_setsum)
-lemmas isCont_intros =
- isCont_ident isCont_const isCont_norm isCont_rabs isCont_add isCont_minus
- isCont_diff isCont_mult isCont_inverse isCont_divide isCont_scaleR
- isCont_of_real isCont_power isCont_sgn isCont_setsum
-
subsection {* Uniform Continuity *}
definition
--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Wed Apr 02 18:35:02 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Wed Apr 02 18:35:07 2014 +0200
@@ -107,7 +107,7 @@
next
case False
have "continuous_on s (norm \<circ> f)"
- by (rule continuous_on_intros continuous_on_norm assms(2))+
+ by (rule continuous_intros continuous_on_norm assms(2))+
with False obtain x where x: "x \<in> s" "\<forall>y\<in>s. (norm \<circ> f) x \<le> (norm \<circ> f) y"
using continuous_attains_inf[OF assms(1), of "norm \<circ> f"]
unfolding o_def
@@ -1460,7 +1460,7 @@
obtain d where
d: "d > 0" "\<And>x. x \<in> unit_cube \<Longrightarrow> d \<le> norm (f x - x)"
apply (rule brouwer_compactness_lemma[OF compact_unit_cube _ *])
- apply (rule continuous_on_intros assms)+
+ apply (rule continuous_intros assms)+
apply blast
done
have *: "\<forall>x. x \<in> unit_cube \<longrightarrow> f x \<in> unit_cube"
@@ -2023,7 +2023,7 @@
apply assumption+
apply (rule_tac x=x in bexI)
apply assumption+
- apply (rule continuous_on_intros)+
+ apply (rule continuous_intros)+
unfolding frontier_cball subset_eq Ball_def image_iff
apply rule
apply rule
--- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Wed Apr 02 18:35:02 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Wed Apr 02 18:35:07 2014 +0200
@@ -119,12 +119,12 @@
shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. f x * c)"
by (rule continuous_on_mult [OF _ continuous_on_const])
-lemma uniformly_continuous_on_cmul_right [continuous_on_intros]:
+lemma uniformly_continuous_on_cmul_right [continuous_intros]:
fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra"
shows "uniformly_continuous_on s f \<Longrightarrow> uniformly_continuous_on s (\<lambda>x. f x * c)"
using bounded_linear.uniformly_continuous_on[OF bounded_linear_mult_left] .
-lemma uniformly_continuous_on_cmul_left[continuous_on_intros]:
+lemma uniformly_continuous_on_cmul_left[continuous_intros]:
fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra"
assumes "uniformly_continuous_on s f"
shows "uniformly_continuous_on s (\<lambda>x. c * f x)"
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Wed Apr 02 18:35:02 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Wed Apr 02 18:35:07 2014 +0200
@@ -1316,7 +1316,7 @@
then obtain a b where a: "a \<in> A" "a \<in> s" and b: "b \<in> B" "b \<in> s" by auto
def f \<equiv> "\<lambda>u. u *\<^sub>R a + (1 - u) *\<^sub>R b"
then have "continuous_on {0 .. 1} f"
- by (auto intro!: continuous_on_intros)
+ by (auto intro!: continuous_intros)
then have "connected (f ` {0 .. 1})"
by (auto intro!: connected_continuous_image)
note connectedD[OF this, of A B]
--- a/src/HOL/Multivariate_Analysis/Derivative.thy Wed Apr 02 18:35:02 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Wed Apr 02 18:35:07 2014 +0200
@@ -678,7 +678,7 @@
show "((\<lambda>x. f x - (f b - f a) / (b - a) * x) has_derivative
(\<lambda>xa. f' x xa - (f b - f a) / (b - a) * xa)) (at x)"
by (intro has_derivative_intros assms(3)[rule_format,OF x] mult_right_has_derivative)
- qed (insert assms(1,2), auto intro!: continuous_on_intros simp: field_simps)
+ qed (insert assms(1,2), auto intro!: continuous_intros simp: field_simps)
then obtain x where
"x \<in> {a <..< b}"
"(\<lambda>xa. f' x xa - (f b - f a) / (b - a) * xa) = (\<lambda>v. 0)" ..
@@ -749,7 +749,7 @@
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)"
apply (rule mvt)
apply (rule assms(1))
- apply (intro continuous_on_intros assms(2))
+ apply (intro continuous_intros assms(2))
using assms(3)
apply (fast intro: has_derivative_inner_right)
done
@@ -798,7 +798,7 @@
by (auto simp add: algebra_simps)
then have 1: "continuous_on {0 .. 1} (f \<circ> ?p)"
apply -
- apply (rule continuous_on_intros)+
+ apply (rule continuous_intros)+
unfolding continuous_on_eq_continuous_within
apply rule
apply (rule differentiable_imp_continuous_within)
@@ -1138,7 +1138,7 @@
show ?thesis
unfolding *
apply (rule brouwer[OF assms(1-3), of "\<lambda>y. x + (y - f y)"])
- apply (rule continuous_on_intros assms)+
+ apply (rule continuous_intros assms)+
using assms(4-6)
apply auto
done
@@ -1209,7 +1209,7 @@
show "continuous_on (cball (f x) e) (\<lambda>y. f (x + g' (y - f x)))"
unfolding g'.diff
apply (rule continuous_on_compose[of _ _ f, unfolded o_def])
- apply (rule continuous_on_intros linear_continuous_on[OF assms(5)])+
+ apply (rule continuous_intros linear_continuous_on[OF assms(5)])+
apply (rule continuous_on_subset[OF assms(2)])
apply rule
apply (unfold image_iff)
--- a/src/HOL/Multivariate_Analysis/Fashoda.thy Wed Apr 02 18:35:02 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Fashoda.thy Wed Apr 02 18:35:07 2014 +0200
@@ -152,11 +152,11 @@
have 1: "box (- 1) (1::real^2) \<noteq> {}"
unfolding interval_eq_empty_cart by auto
have 2: "continuous_on (cbox -1 1) (negatex \<circ> sqprojection \<circ> ?F)"
- apply (intro continuous_on_intros continuous_on_component)
+ apply (intro continuous_intros continuous_on_component)
unfolding *
apply (rule assms)+
apply (subst sqprojection_def)
- apply (intro continuous_on_intros)
+ apply (intro continuous_intros)
apply (simp add: infnorm_eq_0 x0)
apply (rule linear_continuous_on)
proof -
@@ -370,7 +370,7 @@
show "(f \<circ> iscale) ` {- 1..1} \<subseteq> cbox -1 1" "(g \<circ> iscale) ` {- 1..1} \<subseteq> cbox -1 1"
using isc and assms(3-4) by (auto simp add: image_comp [symmetric])
have *: "continuous_on {- 1..1} iscale"
- unfolding iscale_def by (rule continuous_on_intros)+
+ unfolding iscale_def by (rule continuous_intros)+
show "continuous_on {- 1..1} (f \<circ> iscale)" "continuous_on {- 1..1} (g \<circ> iscale)"
apply -
apply (rule_tac[!] continuous_on_compose[OF *])
--- a/src/HOL/Multivariate_Analysis/Integration.thy Wed Apr 02 18:35:02 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Wed Apr 02 18:35:07 2014 +0200
@@ -8747,7 +8747,7 @@
assume "x \<noteq> c"
note conv = assms(1)[unfolded convex_alt,rule_format]
have as1: "continuous_on {0 ..1} (f \<circ> (\<lambda>t. (1 - t) *\<^sub>R c + t *\<^sub>R x))"
- apply (rule continuous_on_intros)+
+ apply (rule continuous_intros)+
apply (rule continuous_on_subset[OF assms(3)])
apply safe
apply (rule conv)
--- a/src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy Wed Apr 02 18:35:02 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy Wed Apr 02 18:35:07 2014 +0200
@@ -110,7 +110,7 @@
proof atomize_elim
let ?proj = "(\<lambda>x. x \<bullet> b) ` X"
from assms have "compact ?proj" "?proj \<noteq> {}"
- by (auto intro!: compact_continuous_image continuous_on_intros)
+ by (auto intro!: compact_continuous_image continuous_intros)
from compact_attains_inf[OF this]
obtain s x
where s: "s\<in>(\<lambda>x. x \<bullet> b) ` X" "\<And>t. t\<in>(\<lambda>x. x \<bullet> b) ` X \<Longrightarrow> s \<le> t"
@@ -133,7 +133,7 @@
proof atomize_elim
let ?proj = "(\<lambda>x. x \<bullet> b) ` X"
from assms have "compact ?proj" "?proj \<noteq> {}"
- by (auto intro!: compact_continuous_image continuous_on_intros)
+ by (auto intro!: compact_continuous_image continuous_intros)
from compact_attains_sup[OF this]
obtain s x
where s: "s\<in>(\<lambda>x. x \<bullet> b) ` X" "\<And>t. t\<in>(\<lambda>x. x \<bullet> b) ` X \<Longrightarrow> t \<le> s"
--- a/src/HOL/Multivariate_Analysis/Path_Connected.thy Wed Apr 02 18:35:02 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy Wed Apr 02 18:35:07 2014 +0200
@@ -108,7 +108,7 @@
have *: "\<And>g. path g \<Longrightarrow> path (reversepath g)"
unfolding path_def reversepath_def
apply (rule continuous_on_compose[unfolded o_def, of _ "\<lambda>x. 1 - x"])
- apply (intro continuous_on_intros)
+ apply (intro continuous_intros)
apply (rule continuous_on_subset[of "{0..1}"])
apply assumption
apply auto
@@ -135,7 +135,7 @@
by (intro continuous_on_cong refl) (auto simp: joinpaths_def pathfinish_def pathstart_def)
show "continuous_on {0..1} g1" and "continuous_on {0..1} g2"
unfolding g1 g2
- by (auto intro!: continuous_on_intros continuous_on_subset[OF cont] simp del: o_apply)
+ by (auto intro!: continuous_intros continuous_on_subset[OF cont] simp del: o_apply)
next
assume g1g2: "continuous_on {0..1} g1" "continuous_on {0..1} g2"
have 01: "{0 .. 1} = {0..1/2} \<union> {1/2 .. 1::real}"
@@ -157,7 +157,7 @@
show "continuous_on {0..1} (g1 +++ g2)"
using assms
unfolding joinpaths_def 01
- apply (intro continuous_on_cases closed_atLeastAtMost g1g2[THEN continuous_on_compose2] continuous_on_intros)
+ apply (intro continuous_on_cases closed_atLeastAtMost g1g2[THEN continuous_on_compose2] continuous_intros)
apply (auto simp: field_simps pathfinish_def pathstart_def intro!: 1 2)
done
qed
@@ -423,9 +423,9 @@
apply (rule continuous_on_eq[of _ "g \<circ> (\<lambda>x. a - 1 + x)"])
defer
prefer 3
- apply (rule continuous_on_intros)+
+ apply (rule continuous_intros)+
prefer 2
- apply (rule continuous_on_intros)+
+ apply (rule continuous_intros)+
apply (rule_tac[1-2] continuous_on_subset[OF assms(1)[unfolded path_def]])
using assms(3) and **
apply auto
@@ -589,7 +589,7 @@
unfolding path_defs
apply (rule_tac x="\<lambda>u. x" in exI)
using assms
- apply (auto intro!: continuous_on_intros)
+ apply (auto intro!: continuous_intros)
done
lemma path_component_refl_eq: "path_component s x x \<longleftrightarrow> x \<in> s"
@@ -977,11 +977,11 @@
done
have "continuous_on (UNIV - {0}) (\<lambda>x::'a. 1 / norm x)"
unfolding field_divide_inverse
- by (simp add: continuous_on_intros)
+ by (simp add: continuous_intros)
then show ?thesis
unfolding * **
using path_connected_punctured_universe[OF assms]
- by (auto intro!: path_connected_continuous_image continuous_on_intros)
+ by (auto intro!: path_connected_continuous_image continuous_intros)
qed
lemma connected_sphere: "2 \<le> DIM('a::euclidean_space) \<Longrightarrow> connected {x::'a. norm (x - a) = r}"
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Wed Apr 02 18:35:02 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Wed Apr 02 18:35:07 2014 +0200
@@ -791,7 +791,7 @@
lemma open_ball [intro, simp]: "open (ball x e)"
proof -
have "open (dist x -` {..<e})"
- by (intro open_vimage open_lessThan continuous_on_intros)
+ by (intro open_vimage open_lessThan continuous_intros)
also have "dist x -` {..<e} = ball x e"
by auto
finally show ?thesis .
@@ -2375,7 +2375,7 @@
lemma closed_cball: "closed (cball x e)"
proof -
have "closed (dist x -` {..e})"
- by (intro closed_vimage closed_atMost continuous_on_intros)
+ by (intro closed_vimage closed_atMost continuous_intros)
also have "dist x -` {..e} = cball x e"
by auto
finally show ?thesis .
@@ -4931,11 +4931,11 @@
subsubsection {* Structural rules for setwise continuity *}
-lemma continuous_on_infnorm[continuous_on_intros]:
+lemma continuous_on_infnorm[continuous_intros]:
"continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. infnorm (f x))"
unfolding continuous_on by (fast intro: tendsto_infnorm)
-lemma continuous_on_inner[continuous_on_intros]:
+lemma continuous_on_inner[continuous_intros]:
fixes g :: "'a::topological_space \<Rightarrow> 'b::real_inner"
assumes "continuous_on s f"
and "continuous_on s g"
@@ -4945,15 +4945,15 @@
subsubsection {* Structural rules for uniform continuity *}
-lemma uniformly_continuous_on_id[continuous_on_intros]:
+lemma uniformly_continuous_on_id[continuous_intros]:
"uniformly_continuous_on s (\<lambda>x. x)"
unfolding uniformly_continuous_on_def by auto
-lemma uniformly_continuous_on_const[continuous_on_intros]:
+lemma uniformly_continuous_on_const[continuous_intros]:
"uniformly_continuous_on s (\<lambda>x. c)"
unfolding uniformly_continuous_on_def by simp
-lemma uniformly_continuous_on_dist[continuous_on_intros]:
+lemma uniformly_continuous_on_dist[continuous_intros]:
fixes f g :: "'a::metric_space \<Rightarrow> 'b::metric_space"
assumes "uniformly_continuous_on s f"
and "uniformly_continuous_on s g"
@@ -4979,20 +4979,20 @@
unfolding dist_real_def by simp
qed
-lemma uniformly_continuous_on_norm[continuous_on_intros]:
+lemma uniformly_continuous_on_norm[continuous_intros]:
assumes "uniformly_continuous_on s f"
shows "uniformly_continuous_on s (\<lambda>x. norm (f x))"
unfolding norm_conv_dist using assms
by (intro uniformly_continuous_on_dist uniformly_continuous_on_const)
-lemma (in bounded_linear) uniformly_continuous_on[continuous_on_intros]:
+lemma (in bounded_linear) uniformly_continuous_on[continuous_intros]:
assumes "uniformly_continuous_on s g"
shows "uniformly_continuous_on s (\<lambda>x. f (g x))"
using assms unfolding uniformly_continuous_on_sequentially
unfolding dist_norm tendsto_norm_zero_iff diff[symmetric]
by (auto intro: tendsto_zero)
-lemma uniformly_continuous_on_cmul[continuous_on_intros]:
+lemma uniformly_continuous_on_cmul[continuous_intros]:
fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
assumes "uniformly_continuous_on s f"
shows "uniformly_continuous_on s (\<lambda>x. c *\<^sub>R f(x))"
@@ -5004,12 +5004,12 @@
shows "dist (- x) (- y) = dist x y"
unfolding dist_norm minus_diff_minus norm_minus_cancel ..
-lemma uniformly_continuous_on_minus[continuous_on_intros]:
+lemma uniformly_continuous_on_minus[continuous_intros]:
fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
shows "uniformly_continuous_on s f \<Longrightarrow> uniformly_continuous_on s (\<lambda>x. - f x)"
unfolding uniformly_continuous_on_def dist_minus .
-lemma uniformly_continuous_on_add[continuous_on_intros]:
+lemma uniformly_continuous_on_add[continuous_intros]:
fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
assumes "uniformly_continuous_on s f"
and "uniformly_continuous_on s g"
@@ -5019,7 +5019,7 @@
unfolding dist_norm tendsto_norm_zero_iff add_diff_add
by (auto intro: tendsto_add_zero)
-lemma uniformly_continuous_on_diff[continuous_on_intros]:
+lemma uniformly_continuous_on_diff[continuous_intros]:
fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
assumes "uniformly_continuous_on s f"
and "uniformly_continuous_on s g"
@@ -5031,7 +5031,7 @@
lemmas continuous_at_compose = isCont_o
-lemma uniformly_continuous_on_compose[continuous_on_intros]:
+lemma uniformly_continuous_on_compose[continuous_intros]:
assumes "uniformly_continuous_on s f" "uniformly_continuous_on (f ` s) g"
shows "uniformly_continuous_on s (g \<circ> f)"
proof -
@@ -6972,7 +6972,7 @@
apply (rule_tac x="\<lambda>x. c *\<^sub>R x" in exI)
apply (rule_tac x="\<lambda>x. (1 / c) *\<^sub>R x" in exI)
using assms
- apply (auto simp add: continuous_on_intros)
+ apply (auto simp add: continuous_intros)
done
lemma homeomorphic_translation:
@@ -7010,14 +7010,14 @@
apply(rule_tac x="\<lambda>x. b + (e/d) *\<^sub>R (x - a)" in exI)
apply(rule_tac x="\<lambda>x. a + (d/e) *\<^sub>R (x - b)" in exI)
using assms
- apply (auto intro!: continuous_on_intros
+ apply (auto intro!: continuous_intros
simp: dist_commute dist_norm pos_divide_less_eq mult_strict_left_mono)
done
show ?cth unfolding homeomorphic_minimal
apply(rule_tac x="\<lambda>x. b + (e/d) *\<^sub>R (x - a)" in exI)
apply(rule_tac x="\<lambda>x. a + (d/e) *\<^sub>R (x - b)" in exI)
using assms
- apply (auto intro!: continuous_on_intros
+ apply (auto intro!: continuous_intros
simp: dist_commute dist_norm pos_divide_le_eq mult_strict_left_mono)
done
qed
--- a/src/HOL/NthRoot.thy Wed Apr 02 18:35:02 2014 +0200
+++ b/src/HOL/NthRoot.thy Wed Apr 02 18:35:07 2014 +0200
@@ -255,7 +255,7 @@
assume n: "0 < n"
let ?f = "\<lambda>y::real. sgn y * \<bar>y\<bar>^n"
have "continuous_on ({0..} \<union> {.. 0}) (\<lambda>x. if 0 < x then x ^ n else - ((-x) ^ n) :: real)"
- using n by (intro continuous_on_If continuous_on_intros) auto
+ using n by (intro continuous_on_If continuous_intros) auto
then have "continuous_on UNIV ?f"
by (rule continuous_on_cong[THEN iffD1, rotated 2]) (auto simp: not_less real_sgn_neg le_less n)
then have [simp]: "\<And>x. isCont ?f x"
@@ -275,7 +275,7 @@
"continuous F f \<Longrightarrow> continuous F (\<lambda>x. root n (f x))"
unfolding continuous_def by (rule tendsto_real_root)
-lemma continuous_on_real_root[continuous_on_intros]:
+lemma continuous_on_real_root[continuous_intros]:
"continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. root n (f x))"
unfolding continuous_on_def by (auto intro: tendsto_real_root)
@@ -454,7 +454,7 @@
"continuous F f \<Longrightarrow> continuous F (\<lambda>x. sqrt (f x))"
unfolding sqrt_def by (rule continuous_real_root)
-lemma continuous_on_real_sqrt[continuous_on_intros]:
+lemma continuous_on_real_sqrt[continuous_intros]:
"continuous_on s f \<Longrightarrow> 0 < n \<Longrightarrow> continuous_on s (\<lambda>x. sqrt (f x))"
unfolding sqrt_def by (rule continuous_on_real_root)
--- a/src/HOL/Probability/Borel_Space.thy Wed Apr 02 18:35:02 2014 +0200
+++ b/src/HOL/Probability/Borel_Space.thy Wed Apr 02 18:35:07 2014 +0200
@@ -221,7 +221,7 @@
assumes "g \<in> borel_measurable M"
shows "(\<lambda>x. f x \<bullet> g x) \<in> borel_measurable M"
using assms
- by (rule borel_measurable_continuous_Pair) (intro continuous_on_intros)
+ by (rule borel_measurable_continuous_Pair) (intro continuous_intros)
lemma [measurable]:
fixes a b :: "'a\<Colon>linorder_topology"
@@ -287,7 +287,7 @@
by auto
also have "\<dots> \<in> sets M"
by (intro measurable_sets[OF borel_measurable_Pair borel_open, OF assms open_Collect_less]
- continuous_on_intros)
+ continuous_intros)
finally show ?thesis .
qed
@@ -659,14 +659,14 @@
fixes g :: "'a \<Rightarrow> 'b::{second_countable_topology, real_normed_vector}"
assumes g: "g \<in> borel_measurable M"
shows "(\<lambda>x. - g x) \<in> borel_measurable M"
- by (rule borel_measurable_continuous_on[OF _ g]) (intro continuous_on_intros)
+ by (rule borel_measurable_continuous_on[OF _ g]) (intro continuous_intros)
lemma borel_measurable_add[measurable (raw)]:
fixes f g :: "'a \<Rightarrow> 'b::{second_countable_topology, real_normed_vector}"
assumes f: "f \<in> borel_measurable M"
assumes g: "g \<in> borel_measurable M"
shows "(\<lambda>x. f x + g x) \<in> borel_measurable M"
- using f g by (rule borel_measurable_continuous_Pair) (intro continuous_on_intros)
+ using f g by (rule borel_measurable_continuous_Pair) (intro continuous_intros)
lemma borel_measurable_setsum[measurable (raw)]:
fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> 'b::{second_countable_topology, real_normed_vector}"
@@ -689,7 +689,7 @@
assumes f: "f \<in> borel_measurable M"
assumes g: "g \<in> borel_measurable M"
shows "(\<lambda>x. f x * g x) \<in> borel_measurable M"
- using f g by (rule borel_measurable_continuous_Pair) (intro continuous_on_intros)
+ using f g by (rule borel_measurable_continuous_Pair) (intro continuous_intros)
lemma borel_measurable_setprod[measurable (raw)]:
fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> 'b::{second_countable_topology, real_normed_field}"
@@ -705,14 +705,14 @@
assumes f: "f \<in> borel_measurable M"
assumes g: "g \<in> borel_measurable M"
shows "(\<lambda>x. dist (f x) (g x)) \<in> borel_measurable M"
- using f g by (rule borel_measurable_continuous_Pair) (intro continuous_on_intros)
+ using f g by (rule borel_measurable_continuous_Pair) (intro continuous_intros)
lemma borel_measurable_scaleR[measurable (raw)]:
fixes g :: "'a \<Rightarrow> 'b::{second_countable_topology, real_normed_vector}"
assumes f: "f \<in> borel_measurable M"
assumes g: "g \<in> borel_measurable M"
shows "(\<lambda>x. f x *\<^sub>R g x) \<in> borel_measurable M"
- using f g by (rule borel_measurable_continuous_Pair) (intro continuous_on_intros)
+ using f g by (rule borel_measurable_continuous_Pair) (intro continuous_intros)
lemma affine_borel_measurable_vector:
fixes f :: "'a \<Rightarrow> 'x::real_normed_vector"
@@ -749,7 +749,7 @@
shows "(\<lambda>x. inverse (f x)) \<in> borel_measurable M"
proof -
have "(\<lambda>x::'b. if x \<in> UNIV - {0} then inverse x else inverse 0) \<in> borel_measurable borel"
- by (intro borel_measurable_continuous_on_open' continuous_on_intros) auto
+ by (intro borel_measurable_continuous_on_open' continuous_intros) auto
also have "(\<lambda>x::'b. if x \<in> UNIV - {0} then inverse x else inverse 0) = inverse"
by (intro ext) auto
finally show ?thesis using f by simp
--- a/src/HOL/Probability/Distributions.thy Wed Apr 02 18:35:02 2014 +0200
+++ b/src/HOL/Probability/Distributions.thy Wed Apr 02 18:35:07 2014 +0200
@@ -180,7 +180,7 @@
show "DERIV (\<lambda>x. x * exp (-x)) x :> exp (-x) - x * exp (-x)"
by (auto intro!: DERIV_intros)
show "isCont (\<lambda>x. exp (- x) - x * exp (- x)) x "
- by (intro isCont_intros isCont_exp')
+ by (intro continuous_intros)
qed fact
also have "(\<integral>x. (exp (-x)) * indicator {0 .. b} x \<partial>lborel) = - exp (- b) - - exp (- 0)"
by (rule integral_FTC_atLeastAtMost) (auto intro!: DERIV_intros)
--- a/src/HOL/Topological_Spaces.thy Wed Apr 02 18:35:02 2014 +0200
+++ b/src/HOL/Topological_Spaces.thy Wed Apr 02 18:35:07 2014 +0200
@@ -9,6 +9,18 @@
imports Main Conditionally_Complete_Lattices
begin
+ML {*
+
+structure Continuous_Intros = Named_Thms
+(
+ val name = @{binding continuous_intros}
+ val description = "Structural introduction rules for continuity"
+)
+
+*}
+
+setup Continuous_Intros.setup
+
subsection {* Topological space *}
class "open" =
@@ -24,19 +36,19 @@
closed :: "'a set \<Rightarrow> bool" where
"closed S \<longleftrightarrow> open (- S)"
-lemma open_empty [intro, simp]: "open {}"
+lemma open_empty [continuous_intros, intro, simp]: "open {}"
using open_Union [of "{}"] by simp
-lemma open_Un [intro]: "open S \<Longrightarrow> open T \<Longrightarrow> open (S \<union> T)"
+lemma open_Un [continuous_intros, intro]: "open S \<Longrightarrow> open T \<Longrightarrow> open (S \<union> T)"
using open_Union [of "{S, T}"] by simp
-lemma open_UN [intro]: "\<forall>x\<in>A. open (B x) \<Longrightarrow> open (\<Union>x\<in>A. B x)"
+lemma open_UN [continuous_intros, intro]: "\<forall>x\<in>A. open (B x) \<Longrightarrow> open (\<Union>x\<in>A. B x)"
using open_Union [of "B ` A"] by simp
-lemma open_Inter [intro]: "finite S \<Longrightarrow> \<forall>T\<in>S. open T \<Longrightarrow> open (\<Inter>S)"
+lemma open_Inter [continuous_intros, intro]: "finite S \<Longrightarrow> \<forall>T\<in>S. open T \<Longrightarrow> open (\<Inter>S)"
by (induct set: finite) auto
-lemma open_INT [intro]: "finite A \<Longrightarrow> \<forall>x\<in>A. open (B x) \<Longrightarrow> open (\<Inter>x\<in>A. B x)"
+lemma open_INT [continuous_intros, intro]: "finite A \<Longrightarrow> \<forall>x\<in>A. open (B x) \<Longrightarrow> open (\<Inter>x\<in>A. B x)"
using open_Inter [of "B ` A"] by simp
lemma openI:
@@ -48,28 +60,28 @@
ultimately show "open S" by simp
qed
-lemma closed_empty [intro, simp]: "closed {}"
+lemma closed_empty [continuous_intros, intro, simp]: "closed {}"
unfolding closed_def by simp
-lemma closed_Un [intro]: "closed S \<Longrightarrow> closed T \<Longrightarrow> closed (S \<union> T)"
+lemma closed_Un [continuous_intros, intro]: "closed S \<Longrightarrow> closed T \<Longrightarrow> closed (S \<union> T)"
unfolding closed_def by auto
-lemma closed_UNIV [intro, simp]: "closed UNIV"
+lemma closed_UNIV [continuous_intros, intro, simp]: "closed UNIV"
unfolding closed_def by simp
-lemma closed_Int [intro]: "closed S \<Longrightarrow> closed T \<Longrightarrow> closed (S \<inter> T)"
+lemma closed_Int [continuous_intros, intro]: "closed S \<Longrightarrow> closed T \<Longrightarrow> closed (S \<inter> T)"
unfolding closed_def by auto
-lemma closed_INT [intro]: "\<forall>x\<in>A. closed (B x) \<Longrightarrow> closed (\<Inter>x\<in>A. B x)"
+lemma closed_INT [continuous_intros, intro]: "\<forall>x\<in>A. closed (B x) \<Longrightarrow> closed (\<Inter>x\<in>A. B x)"
unfolding closed_def by auto
-lemma closed_Inter [intro]: "\<forall>S\<in>K. closed S \<Longrightarrow> closed (\<Inter> K)"
+lemma closed_Inter [continuous_intros, intro]: "\<forall>S\<in>K. closed S \<Longrightarrow> closed (\<Inter> K)"
unfolding closed_def uminus_Inf by auto
-lemma closed_Union [intro]: "finite S \<Longrightarrow> \<forall>T\<in>S. closed T \<Longrightarrow> closed (\<Union>S)"
+lemma closed_Union [continuous_intros, intro]: "finite S \<Longrightarrow> \<forall>T\<in>S. closed T \<Longrightarrow> closed (\<Union>S)"
by (induct set: finite) auto
-lemma closed_UN [intro]: "finite A \<Longrightarrow> \<forall>x\<in>A. closed (B x) \<Longrightarrow> closed (\<Union>x\<in>A. B x)"
+lemma closed_UN [continuous_intros, intro]: "finite A \<Longrightarrow> \<forall>x\<in>A. closed (B x) \<Longrightarrow> closed (\<Union>x\<in>A. B x)"
using closed_Union [of "B ` A"] by simp
lemma open_closed: "open S \<longleftrightarrow> closed (- S)"
@@ -78,16 +90,16 @@
lemma closed_open: "closed S \<longleftrightarrow> open (- S)"
unfolding closed_def by simp
-lemma open_Diff [intro]: "open S \<Longrightarrow> closed T \<Longrightarrow> open (S - T)"
+lemma open_Diff [continuous_intros, intro]: "open S \<Longrightarrow> closed T \<Longrightarrow> open (S - T)"
unfolding closed_open Diff_eq by (rule open_Int)
-lemma closed_Diff [intro]: "closed S \<Longrightarrow> open T \<Longrightarrow> closed (S - T)"
+lemma closed_Diff [continuous_intros, intro]: "closed S \<Longrightarrow> open T \<Longrightarrow> closed (S - T)"
unfolding open_closed Diff_eq by (rule closed_Int)
-lemma open_Compl [intro]: "closed S \<Longrightarrow> open (- S)"
+lemma open_Compl [continuous_intros, intro]: "closed S \<Longrightarrow> open (- S)"
unfolding closed_open .
-lemma closed_Compl [intro]: "open S \<Longrightarrow> closed (- S)"
+lemma closed_Compl [continuous_intros, intro]: "open S \<Longrightarrow> closed (- S)"
unfolding open_closed .
end
@@ -119,7 +131,7 @@
finally show "closed {a}" unfolding closed_def .
qed
-lemma closed_insert [simp]:
+lemma closed_insert [continuous_intros, simp]:
fixes a :: "'a::t1_space"
assumes "closed S" shows "closed (insert a S)"
proof -
@@ -185,26 +197,26 @@
unfolding open_generated_order
by (rule topological_space_generate_topology)
-lemma open_greaterThan [simp]: "open {a <..}"
+lemma open_greaterThan [continuous_intros, simp]: "open {a <..}"
unfolding open_generated_order by (auto intro: generate_topology.Basis)
-lemma open_lessThan [simp]: "open {..< a}"
+lemma open_lessThan [continuous_intros, simp]: "open {..< a}"
unfolding open_generated_order by (auto intro: generate_topology.Basis)
-lemma open_greaterThanLessThan [simp]: "open {a <..< b}"
+lemma open_greaterThanLessThan [continuous_intros, simp]: "open {a <..< b}"
unfolding greaterThanLessThan_eq by (simp add: open_Int)
end
class linorder_topology = linorder + order_topology
-lemma closed_atMost [simp]: "closed {.. a::'a::linorder_topology}"
+lemma closed_atMost [continuous_intros, simp]: "closed {.. a::'a::linorder_topology}"
by (simp add: closed_open)
-lemma closed_atLeast [simp]: "closed {a::'a::linorder_topology ..}"
+lemma closed_atLeast [continuous_intros, simp]: "closed {a::'a::linorder_topology ..}"
by (simp add: closed_open)
-lemma closed_atLeastAtMost [simp]: "closed {a::'a::linorder_topology .. b}"
+lemma closed_atLeastAtMost [continuous_intros, simp]: "closed {a::'a::linorder_topology .. b}"
proof -
have "{a .. b} = {a ..} \<inter> {.. b}"
by auto
@@ -1725,7 +1737,7 @@
shows "open (f -` B)"
by (metis assms continuous_on_open_vimage le_iff_inf)
-corollary open_vimage:
+corollary open_vimage[continuous_intros]:
assumes "open s" and "continuous_on UNIV f"
shows "open (f -` s)"
using assms unfolding continuous_on_open_vimage [OF open_UNIV]
@@ -1745,6 +1757,12 @@
unfolding continuous_on_closed_invariant
by (metis closed_Int Int_absorb Int_commute[of s] Int_assoc[of _ _ s])
+corollary closed_vimage[continuous_intros]:
+ assumes "closed s" and "continuous_on UNIV f"
+ shows "closed (f -` s)"
+ using assms unfolding continuous_on_closed_vimage [OF closed_UNIV]
+ by simp
+
lemma continuous_on_open_Union:
"(\<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"
unfolding continuous_on_def by safe (metis open_Union at_within_open UnionI)
@@ -1770,25 +1788,13 @@
by (rule continuous_on_closed_Un)
qed
-ML {*
-
-structure Continuous_On_Intros = Named_Thms
-(
- val name = @{binding continuous_on_intros}
- val description = "Structural introduction rules for setwise continuity"
-)
-
-*}
-
-setup Continuous_On_Intros.setup
-
-lemma continuous_on_id[continuous_on_intros]: "continuous_on s (\<lambda>x. x)"
+lemma continuous_on_id[continuous_intros]: "continuous_on s (\<lambda>x. x)"
unfolding continuous_on_def by (fast intro: tendsto_ident_at)
-lemma continuous_on_const[continuous_on_intros]: "continuous_on s (\<lambda>x. c)"
+lemma continuous_on_const[continuous_intros]: "continuous_on s (\<lambda>x. c)"
unfolding continuous_on_def by (auto intro: tendsto_const)
-lemma continuous_on_compose[continuous_on_intros]:
+lemma continuous_on_compose[continuous_intros]:
"continuous_on s f \<Longrightarrow> continuous_on (f ` s) g \<Longrightarrow> continuous_on s (g o f)"
unfolding continuous_on_topological by simp metis
@@ -1801,18 +1807,6 @@
definition continuous :: "'a::t2_space filter \<Rightarrow> ('a \<Rightarrow> 'b::topological_space) \<Rightarrow> bool" where
"continuous F f \<longleftrightarrow> (f ---> f (Lim F (\<lambda>x. x))) F"
-ML {*
-
-structure Continuous_Intros = Named_Thms
-(
- val name = @{binding continuous_intros}
- val description = "Structural introduction rules for pointwise continuity"
-)
-
-*}
-
-setup Continuous_Intros.setup
-
lemma continuous_bot[continuous_intros, simp]: "continuous bot f"
unfolding continuous_def by auto
--- a/src/HOL/Transcendental.thy Wed Apr 02 18:35:02 2014 +0200
+++ b/src/HOL/Transcendental.thy Wed Apr 02 18:35:07 2014 +0200
@@ -994,7 +994,7 @@
"continuous F f \<Longrightarrow> continuous F (\<lambda>x. exp (f x))"
unfolding continuous_def by (rule tendsto_exp)
-lemma continuous_on_exp [continuous_on_intros]:
+lemma continuous_on_exp [continuous_intros]:
"continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. exp (f x))"
unfolding continuous_on_def by (auto intro: tendsto_exp)
@@ -1303,7 +1303,7 @@
"continuous (at x within s) f \<Longrightarrow> 0 < f x \<Longrightarrow> continuous (at x within s) (\<lambda>x. ln (f x))"
unfolding continuous_within by (rule tendsto_ln)
-lemma continuous_on_ln [continuous_on_intros]:
+lemma continuous_on_ln [continuous_intros]:
"continuous_on s f \<Longrightarrow> (\<forall>x\<in>s. 0 < f x) \<Longrightarrow> continuous_on s (\<lambda>x. ln (f x))"
unfolding continuous_on_def by (auto intro: tendsto_ln)
@@ -1747,7 +1747,7 @@
shows "isCont (\<lambda>x. log (f x) (g x)) a"
using assms unfolding continuous_at by (rule tendsto_log)
-lemma continuous_on_log[continuous_on_intros]:
+lemma continuous_on_log[continuous_intros]:
assumes "continuous_on s f" "continuous_on s g"
and "\<forall>x\<in>s. 0 < f x" "\<forall>x\<in>s. f x \<noteq> 1" "\<forall>x\<in>s. 0 < g x"
shows "continuous_on s (\<lambda>x. log (f x) (g x))"
@@ -2076,7 +2076,7 @@
shows "isCont (\<lambda>x. (f x) powr g x) a"
using assms unfolding continuous_at by (rule tendsto_powr)
-lemma continuous_on_powr[continuous_on_intros]:
+lemma continuous_on_powr[continuous_intros]:
assumes "continuous_on s f" "continuous_on s g" and "\<forall>x\<in>s. 0 < f x"
shows "continuous_on s (\<lambda>x. (f x) powr (g x))"
using assms unfolding continuous_on_def by (fast intro: tendsto_powr)
@@ -2215,7 +2215,7 @@
"continuous F f \<Longrightarrow> continuous F (\<lambda>x. sin (f x))"
unfolding continuous_def by (rule tendsto_sin)
-lemma continuous_on_sin [continuous_on_intros]:
+lemma continuous_on_sin [continuous_intros]:
"continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. sin (f x))"
unfolding continuous_on_def by (auto intro: tendsto_sin)
@@ -2223,7 +2223,7 @@
"continuous F f \<Longrightarrow> continuous F (\<lambda>x. cos (f x))"
unfolding continuous_def by (rule tendsto_cos)
-lemma continuous_on_cos [continuous_on_intros]:
+lemma continuous_on_cos [continuous_intros]:
"continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. cos (f x))"
unfolding continuous_on_def by (auto intro: tendsto_cos)
@@ -2884,7 +2884,7 @@
"continuous (at x within s) f \<Longrightarrow> cos (f x) \<noteq> 0 \<Longrightarrow> continuous (at x within s) (\<lambda>x. tan (f x))"
unfolding continuous_within by (rule tendsto_tan)
-lemma continuous_on_tan [continuous_on_intros]:
+lemma continuous_on_tan [continuous_intros]:
"continuous_on s f \<Longrightarrow> (\<forall>x\<in>s. cos (f x) \<noteq> 0) \<Longrightarrow> continuous_on s (\<lambda>x. tan (f x))"
unfolding continuous_on_def by (auto intro: tendsto_tan)
@@ -3232,7 +3232,7 @@
lemma continuous_on_arcsin': "continuous_on {-1 .. 1} arcsin"
proof -
have "continuous_on (sin ` {- pi / 2 .. pi / 2}) arcsin"
- by (rule continuous_on_inv) (auto intro: continuous_on_intros simp: arcsin_sin)
+ by (rule continuous_on_inv) (auto intro: continuous_intros simp: arcsin_sin)
also have "sin ` {- pi / 2 .. pi / 2} = {-1 .. 1}"
proof safe
fix x :: real
@@ -3244,7 +3244,7 @@
finally show ?thesis .
qed
-lemma continuous_on_arcsin [continuous_on_intros]:
+lemma continuous_on_arcsin [continuous_intros]:
"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))"
using continuous_on_compose[of s f, OF _ continuous_on_subset[OF continuous_on_arcsin']]
by (auto simp: comp_def subset_eq)
@@ -3256,7 +3256,7 @@
lemma continuous_on_arccos': "continuous_on {-1 .. 1} arccos"
proof -
have "continuous_on (cos ` {0 .. pi}) arccos"
- by (rule continuous_on_inv) (auto intro: continuous_on_intros simp: arccos_cos)
+ by (rule continuous_on_inv) (auto intro: continuous_intros simp: arccos_cos)
also have "cos ` {0 .. pi} = {-1 .. 1}"
proof safe
fix x :: real
@@ -3268,7 +3268,7 @@
finally show ?thesis .
qed
-lemma continuous_on_arccos [continuous_on_intros]:
+lemma continuous_on_arccos [continuous_intros]:
"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))"
using continuous_on_compose[of s f, OF _ continuous_on_subset[OF continuous_on_arccos']]
by (auto simp: comp_def subset_eq)
@@ -3292,7 +3292,7 @@
lemma continuous_arctan [continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. arctan (f x))"
unfolding continuous_def by (rule tendsto_arctan)
-lemma continuous_on_arctan [continuous_on_intros]: "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. arctan (f x))"
+lemma continuous_on_arctan [continuous_intros]: "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. arctan (f x))"
unfolding continuous_on_def by (auto intro: tendsto_arctan)
lemma DERIV_arcsin: