# HG changeset patch # User huffman # Date 1314326498 25200 # Node ID 1d477a2b1572f4a94d106b0df881f970f989296b # Parent adb18b07b34113b28dfb7ac82ee3dfaf104be36e replace some continuous_on lemmas with more general versions diff -r adb18b07b341 -r 1d477a2b1572 NEWS --- 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 diff -r adb18b07b341 -r 1d477a2b1572 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy --- 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 \ b" "continuous_on {a .. b} f" "(f b)$$k \ y" "y \ (f a)$$k" shows "\x\{a..b}. (f x)$$k = y" apply(subst neg_equal_iff_equal[THEN sym]) - using ivt_increasing_component_on_1[of a b "\x. - f x" k "- y"] using assms using continuous_on_neg - by auto + using ivt_increasing_component_on_1[of a b "\x. - f x" k "- y"] + using assms using continuous_on_minus by auto lemma ivt_decreasing_component_1: fixes f::"real \ 'a::euclidean_space" shows "a \ b \ \x\{a .. b}. continuous (at x) f diff -r adb18b07b341 -r 1d477a2b1572 src/HOL/Multivariate_Analysis/Derivative.thy --- 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 "\x\{a<..xa. f' x xa - (f b - f a) / (b - a) * xa) = (\v. 0)" apply(rule rolle[OF assms(1), of "\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 \ {a<..x. f x - (f b - f a) / (b - a) * x) has_derivative (\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 \ ?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) diff -r adb18b07b341 -r 1d477a2b1572 src/HOL/Multivariate_Analysis/Euclidean_Space.thy --- 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 "\i. i < DIM('a) \ x $$ i = y $$ i" shows "x = y" proof - from assms have "\i sqprojection \ ?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" diff -r adb18b07b341 -r 1d477a2b1572 src/HOL/Multivariate_Analysis/Path_Connected.thy --- 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) \ path g" proof- have *:"\g. path g \ path(reversepath g)" unfolding path_def reversepath_def apply(rule continuous_on_compose[unfolded o_def, of _ "\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 \ 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 \ 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 _ "\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 \ (\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 diff -r adb18b07b341 -r 1d477a2b1572 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy --- 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 (\x. c)" +lemma continuous_on_const: "continuous_on s (\x. c)" unfolding continuous_on_def by (auto intro: tendsto_intros) -lemma continuous_on_cmul: - fixes f :: "'a::topological_space \ 'b::real_normed_vector" - shows "continuous_on s f \ continuous_on s (\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 \ 'b::real_normed_vector" shows "continuous_on s f \ continuous_on s (\x. - f x)" unfolding continuous_on_def by (auto intro: tendsto_intros) @@ -3493,12 +3487,46 @@ \ continuous_on s (\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 \ 'b::real_normed_vector" shows "continuous_on s f \ continuous_on s g \ continuous_on s (\x. f x - g x)" unfolding continuous_on_def by (auto intro: tendsto_intros) +lemma (in bounded_linear) continuous_on: + "continuous_on s g \ continuous_on s (\x. f (g x))" + unfolding continuous_on_def by (fast intro: tendsto) + +lemma (in bounded_bilinear) continuous_on: + "\continuous_on s f; continuous_on s g\ \ continuous_on s (\x. f x ** g x)" + unfolding continuous_on_def by (fast intro: tendsto) + +lemma continuous_on_scaleR: + fixes g :: "'a::topological_space \ 'b::real_normed_vector" + assumes "continuous_on s f" and "continuous_on s g" + shows "continuous_on s (\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 \ 'b::real_normed_algebra" + assumes "continuous_on s f" and "continuous_on s g" + shows "continuous_on s (\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 \ 'b::real_inner" + assumes "continuous_on s f" and "continuous_on s g" + shows "continuous_on s (\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 \ continuous_on s (\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 \ real" and v :: "'b::real_normed_vector" - shows "continuous_on s c ==> continuous_on s (\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 \ real" - fixes f :: "'a::metric_space \ 'b::real_normed_vector" - shows "continuous_on s c \ continuous_on s f - ==> continuous_on s (\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 \ real" - fixes g :: "'a::metric_space \ real" - shows "continuous_on s f \ continuous_on s g - ==> continuous_on s (\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) (\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 \ b}" by (simp add: closed_Collect_le) @@ -5391,8 +5396,7 @@ unfolding homeomorphic_minimal apply(rule_tac x="\x. c *\<^sub>R x" in exI) apply(rule_tac x="\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"