--- a/NEWS Thu Aug 25 16:50:55 2011 -0700
+++ b/NEWS Thu Aug 25 19:41:38 2011 -0700
@@ -221,6 +221,13 @@
Lim_inner ~> tendsto_inner [OF tendsto_const]
dot_lsum ~> inner_setsum_left
dot_rsum ~> inner_setsum_right
+ continuous_on_neg ~> continuous_on_minus
+ continuous_on_sub ~> continuous_on_diff
+ continuous_on_cmul ~> continuous_on_scaleR [OF continuous_on_const]
+ continuous_on_vmul ~> continuous_on_scaleR [OF _ continuous_on_const]
+ continuous_on_mul ~> continuous_on_scaleR
+ continuous_on_mul_real ~> continuous_on_mult
+ continuous_on_inner ~> continuous_on_inner [OF continuous_on_const]
subset_interior ~> interior_mono
subset_closure ~> closure_mono
closure_univ ~> closure_UNIV
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Thu Aug 25 16:50:55 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Thu Aug 25 19:41:38 2011 -0700
@@ -3643,8 +3643,8 @@
assumes "a \<le> b" "continuous_on {a .. b} f" "(f b)$$k \<le> y" "y \<le> (f a)$$k"
shows "\<exists>x\<in>{a..b}. (f x)$$k = y"
apply(subst neg_equal_iff_equal[THEN sym])
- using ivt_increasing_component_on_1[of a b "\<lambda>x. - f x" k "- y"] using assms using continuous_on_neg
- by auto
+ using ivt_increasing_component_on_1[of a b "\<lambda>x. - f x" k "- y"]
+ using assms using continuous_on_minus by auto
lemma ivt_decreasing_component_1: fixes f::"real \<Rightarrow> 'a::euclidean_space"
shows "a \<le> b \<Longrightarrow> \<forall>x\<in>{a .. b}. continuous (at x) f
--- a/src/HOL/Multivariate_Analysis/Derivative.thy Thu Aug 25 16:50:55 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Thu Aug 25 19:41:38 2011 -0700
@@ -785,7 +785,7 @@
have "\<exists>x\<in>{a<..<b}. (\<lambda>xa. f' x xa - (f b - f a) / (b - a) * xa) = (\<lambda>v. 0)"
apply(rule rolle[OF assms(1), of "\<lambda>x. f x - (f b - f a) / (b - a) * x"])
defer
- apply(rule continuous_on_intros assms(2) continuous_on_cmul[where 'b=real, unfolded real_scaleR_def])+
+ apply(rule continuous_on_intros assms(2))+
proof
fix x assume x:"x \<in> {a<..<b}"
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)"
@@ -869,7 +869,7 @@
unfolding scaleR_left_diff_distrib scaleR_right_diff_distrib
by (auto simp add: algebra_simps)
hence 1:"continuous_on {0..1} (f \<circ> ?p)" apply-
- apply(rule continuous_on_intros continuous_on_vmul)+
+ apply(rule continuous_on_intros)+
unfolding continuous_on_eq_continuous_within
apply(rule,rule differentiable_imp_continuous_within)
unfolding differentiable_def apply(rule_tac x="f' xa" in exI)
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Thu Aug 25 16:50:55 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Thu Aug 25 19:41:38 2011 -0700
@@ -149,7 +149,7 @@
assumes "\<And>i. i < DIM('a) \<Longrightarrow> x $$ i = y $$ i" shows "x = y"
proof -
from assms have "\<forall>i<DIM('a). (x - y) $$ i = 0"
- by (simp add: euclidean_component_diff)
+ by simp
then show "x = y"
unfolding euclidean_component_def euclidean_all_zero by simp
qed
--- a/src/HOL/Multivariate_Analysis/Fashoda.thy Thu Aug 25 16:50:55 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Fashoda.thy Thu Aug 25 19:41:38 2011 -0700
@@ -44,7 +44,7 @@
have 2:"continuous_on {- 1..1} (negatex \<circ> sqprojection \<circ> ?F)" apply(rule continuous_on_intros continuous_on_component continuous_on_vec1)+
prefer 2 apply(rule continuous_on_intros continuous_on_component continuous_on_vec1)+ unfolding *
apply(rule assms)+ apply(rule continuous_on_compose,subst sqprojection_def)
- apply(rule continuous_on_mul ) apply(rule continuous_at_imp_continuous_on,rule) apply(rule continuous_at_inv[unfolded o_def])
+ apply(rule continuous_on_scaleR) apply(rule continuous_at_imp_continuous_on,rule) apply(rule continuous_at_inv[unfolded o_def])
apply(rule continuous_at_infnorm) unfolding infnorm_eq_0 defer apply(rule continuous_on_id) apply(rule linear_continuous_on) proof-
show "bounded_linear negatex" apply(rule bounded_linearI') unfolding vec_eq_iff proof(rule_tac[!] allI) fix i::2 and x y::"real^2" and c::real
show "negatex (x + y) $ i = (negatex x + negatex y) $ i" "negatex (c *\<^sub>R x) $ i = (c *\<^sub>R negatex x) $ i"
--- a/src/HOL/Multivariate_Analysis/Path_Connected.thy Thu Aug 25 16:50:55 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy Thu Aug 25 19:41:38 2011 -0700
@@ -92,7 +92,7 @@
lemma path_reversepath[simp]: "path(reversepath g) \<longleftrightarrow> path g" proof-
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(rule continuous_on_sub, rule continuous_on_const, rule continuous_on_id)
+ apply(intro continuous_on_intros)
apply(rule continuous_on_subset[of "{0..1}"], assumption) by auto
show ?thesis using *[of "reversepath g"] *[of g] unfolding reversepath_reversepath by (rule iffI) qed
@@ -108,8 +108,9 @@
by auto
thus "continuous_on {0..1} g1 \<and> continuous_on {0..1} g2" apply -apply rule
apply(subst *) defer apply(subst *) apply (rule_tac[!] continuous_on_compose)
- apply (rule continuous_on_cmul, rule continuous_on_add, rule continuous_on_id, rule continuous_on_const) defer
- apply (rule continuous_on_cmul, rule continuous_on_id) apply(rule_tac[!] continuous_on_eq[of _ "g1 +++ g2"]) defer prefer 3
+ apply (intro continuous_on_intros) defer
+ apply (intro continuous_on_intros)
+ apply(rule_tac[!] continuous_on_eq[of _ "g1 +++ g2"]) defer prefer 3
apply(rule_tac[1-2] continuous_on_subset[of "{0 .. 1}"]) apply(rule as, assumption, rule as, assumption)
apply(rule) defer apply rule proof-
fix x assume "x \<in> op *\<^sub>R (1 / 2) ` {0::real..1}"
@@ -132,10 +133,10 @@
done
show "continuous_on {0..1} (g1 +++ g2)" unfolding * apply(rule continuous_on_union) apply (rule closed_real_atLeastAtMost)+ proof-
show "continuous_on {0..(1 / 2) *\<^sub>R 1} (g1 +++ g2)" apply(rule continuous_on_eq[of _ "\<lambda>x. g1 (2 *\<^sub>R x)"]) defer
- unfolding o_def[THEN sym] apply(rule continuous_on_compose) apply(rule continuous_on_cmul, rule continuous_on_id)
+ unfolding o_def[THEN sym] apply(rule continuous_on_compose) apply (intro continuous_on_intros)
unfolding ** apply(rule as(1)) unfolding joinpaths_def by auto next
show "continuous_on {(1/2)*\<^sub>R1..1} (g1 +++ g2)" apply(rule continuous_on_eq[of _ "g2 \<circ> (\<lambda>x. 2 *\<^sub>R x - 1)"]) defer
- apply(rule continuous_on_compose) apply(rule continuous_on_sub, rule continuous_on_cmul, rule continuous_on_id, rule continuous_on_const)
+ apply(rule continuous_on_compose) apply (intro continuous_on_intros)
unfolding *** o_def joinpaths_def apply(rule as(2)) using assms[unfolded pathstart_def pathfinish_def]
by (auto simp add: mult_ac) qed qed
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Thu Aug 25 16:50:55 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Thu Aug 25 19:41:38 2011 -0700
@@ -3473,16 +3473,10 @@
text{* Same thing for setwise continuity. *}
-lemma continuous_on_const:
- "continuous_on s (\<lambda>x. c)"
+lemma continuous_on_const: "continuous_on s (\<lambda>x. c)"
unfolding continuous_on_def by (auto intro: tendsto_intros)
-lemma continuous_on_cmul:
- fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
- shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. c *\<^sub>R (f x))"
- unfolding continuous_on_def by (auto intro: tendsto_intros)
-
-lemma continuous_on_neg:
+lemma continuous_on_minus:
fixes f :: "'a::topological_space \<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_intros)
@@ -3493,12 +3487,46 @@
\<Longrightarrow> continuous_on s (\<lambda>x. f x + g x)"
unfolding continuous_on_def by (auto intro: tendsto_intros)
-lemma continuous_on_sub:
+lemma continuous_on_diff:
fixes f g :: "'a::topological_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_intros)
+lemma (in bounded_linear) continuous_on:
+ "continuous_on s g \<Longrightarrow> continuous_on s (\<lambda>x. f (g x))"
+ unfolding continuous_on_def by (fast intro: tendsto)
+
+lemma (in bounded_bilinear) continuous_on:
+ "\<lbrakk>continuous_on s f; continuous_on s g\<rbrakk> \<Longrightarrow> continuous_on s (\<lambda>x. f x ** g x)"
+ unfolding continuous_on_def by (fast intro: tendsto)
+
+lemma continuous_on_scaleR:
+ fixes g :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
+ assumes "continuous_on s f" and "continuous_on s g"
+ shows "continuous_on s (\<lambda>x. f x *\<^sub>R g x)"
+ using bounded_bilinear_scaleR assms
+ by (rule bounded_bilinear.continuous_on)
+
+lemma continuous_on_mult:
+ fixes g :: "'a::topological_space \<Rightarrow> 'b::real_normed_algebra"
+ assumes "continuous_on s f" and "continuous_on s g"
+ shows "continuous_on s (\<lambda>x. f x * g x)"
+ using bounded_bilinear_mult assms
+ by (rule bounded_bilinear.continuous_on)
+
+lemma continuous_on_inner:
+ fixes g :: "'a::topological_space \<Rightarrow> 'b::real_inner"
+ assumes "continuous_on s f" and "continuous_on s g"
+ shows "continuous_on s (\<lambda>x. inner (f x) (g x))"
+ using bounded_bilinear_inner assms
+ by (rule bounded_bilinear.continuous_on)
+
+lemma continuous_on_euclidean_component:
+ "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. f x $$ i)"
+ using bounded_linear_euclidean_component
+ by (rule bounded_linear.continuous_on)
+
text{* Same thing for uniform continuity, using sequential formulations. *}
lemma uniformly_continuous_on_const:
@@ -3942,28 +3970,10 @@
lemmas continuous_intros = continuous_add continuous_vmul continuous_cmul
continuous_const continuous_sub continuous_at_id continuous_within_id continuous_mul
-lemma continuous_on_vmul:
- fixes c :: "'a::metric_space \<Rightarrow> real" and v :: "'b::real_normed_vector"
- shows "continuous_on s c ==> continuous_on s (\<lambda>x. c(x) *\<^sub>R v)"
- unfolding continuous_on_eq_continuous_within using continuous_vmul[of _ c] by auto
-
-lemma continuous_on_mul:
- fixes c :: "'a::metric_space \<Rightarrow> real"
- fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
- shows "continuous_on s c \<Longrightarrow> continuous_on s f
- ==> continuous_on s (\<lambda>x. c(x) *\<^sub>R f x)"
- unfolding continuous_on_eq_continuous_within using continuous_mul[of _ c] by auto
-
-lemma continuous_on_mul_real:
- fixes f :: "'a::metric_space \<Rightarrow> real"
- fixes g :: "'a::metric_space \<Rightarrow> real"
- shows "continuous_on s f \<Longrightarrow> continuous_on s g
- ==> continuous_on s (\<lambda>x. f x * g x)"
- using continuous_on_mul[of s f g] unfolding real_scaleR_def .
-
lemmas continuous_on_intros = continuous_on_add continuous_on_const
- continuous_on_id continuous_on_compose continuous_on_cmul continuous_on_neg
- continuous_on_sub continuous_on_mul continuous_on_vmul continuous_on_mul_real
+ continuous_on_id continuous_on_compose continuous_on_minus
+ continuous_on_diff continuous_on_scaleR continuous_on_mult
+ continuous_on_inner continuous_on_euclidean_component
uniformly_continuous_on_add uniformly_continuous_on_const
uniformly_continuous_on_id uniformly_continuous_on_compose
uniformly_continuous_on_cmul uniformly_continuous_on_neg
@@ -5110,11 +5120,6 @@
lemma continuous_at_euclidean_component[intro!, simp]: "continuous (at x) (\<lambda>x. x $$ i)"
unfolding euclidean_component_def by (rule continuous_at_inner)
-lemma continuous_on_inner:
- fixes s :: "'a::real_inner set"
- shows "continuous_on s (inner a)"
- unfolding continuous_on by (rule ballI) (intro tendsto_intros)
-
lemma closed_halfspace_le: "closed {x. inner a x \<le> b}"
by (simp add: closed_Collect_le)
@@ -5391,8 +5396,7 @@
unfolding homeomorphic_minimal
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
- using continuous_on_cmul[OF continuous_on_id] by auto
+ using assms by (auto simp add: continuous_on_intros)
lemma homeomorphic_translation:
fixes s :: "'a::real_normed_vector set"