# HG changeset patch # User hoelzl # Date 1396456507 -7200 # Node ID fb9ae0727548bea146b9bb224d17f9386e48e348 # Parent 7c717ba55a0b604b96d151f88482a8a66ff6606d extend continuous_intros; remove continuous_on_intros and isCont_intros diff -r 7c717ba55a0b -r fb9ae0727548 NEWS --- 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: diff -r 7c717ba55a0b -r fb9ae0727548 src/HOL/Deriv.thy --- 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: "\x. a \ x \ x \ b \ isCont ?F x" - using con by (fast intro: isCont_intros) + using con by (fast intro: continuous_intros) have difF: "\x. a < x \ x < b \ ?F differentiable (at x)" proof (clarify) fix x::real diff -r 7c717ba55a0b -r fb9ae0727548 src/HOL/Library/Product_Vector.thy --- 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 \ continuous F g \ continuous F (\x. (f x, g x))" unfolding continuous_def by (rule tendsto_Pair) -lemma continuous_on_fst[continuous_on_intros]: "continuous_on s f \ continuous_on s (\x. fst (f x))" +lemma continuous_on_fst[continuous_intros]: "continuous_on s f \ continuous_on s (\x. fst (f x))" unfolding continuous_on_def by (auto intro: tendsto_fst) -lemma continuous_on_snd[continuous_on_intros]: "continuous_on s f \ continuous_on s (\x. snd (f x))" +lemma continuous_on_snd[continuous_intros]: "continuous_on s f \ continuous_on s (\x. snd (f x))" unfolding continuous_on_def by (auto intro: tendsto_snd) -lemma continuous_on_Pair[continuous_on_intros]: "continuous_on s f \ continuous_on s g \ continuous_on s (\x. (f x, g x))" +lemma continuous_on_Pair[continuous_intros]: "continuous_on s f \ continuous_on s g \ continuous_on s (\x. (f x, g x))" unfolding continuous_on_def by (auto intro: tendsto_Pair) lemma isCont_fst [simp]: "isCont f a \ isCont (\x. fst (f x)) a" diff -r 7c717ba55a0b -r fb9ae0727548 src/HOL/Limits.thy --- 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 \ continuous F g \ continuous F (\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 :: "_ \ 'a :: metric_space" shows "continuous_on s f \ continuous_on s g \ continuous_on s (\x. dist (f x) (g x))" unfolding continuous_on_def by (auto intro: tendsto_dist) @@ -449,7 +449,7 @@ "continuous F f \ continuous F (\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 \ continuous_on s (\x. norm (f x))" unfolding continuous_on_def by (auto intro: tendsto_norm) @@ -473,7 +473,7 @@ "continuous F f \ continuous F (\x. \f x :: real\)" 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 \ continuous_on s (\x. \f x :: real\)" unfolding real_norm_def[symmetric] by (rule continuous_on_norm) @@ -501,7 +501,7 @@ shows "continuous F f \ continuous F g \ continuous F (\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 :: "_ \ '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_add) @@ -521,7 +521,7 @@ shows "continuous F f \ continuous F (\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 :: "_ \ 'b::real_normed_vector" shows "continuous_on s f \ continuous_on s (\x. - f x)" unfolding continuous_on_def by (auto intro: tendsto_minus) @@ -546,7 +546,7 @@ shows "continuous F f \ continuous F g \ continuous F (\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 \ '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_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 \ continuous F (\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 :: "_ \ 'b::{power,real_normed_algebra}" shows "continuous_on s f \ continuous_on s (\x. (f x)^n)" unfolding continuous_on_def by (auto intro: tendsto_power) @@ -820,7 +820,7 @@ shows "isCont (\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 \ 'b::real_normed_div_algebra" assumes "continuous_on s f" and "\x\s. f x \ 0" shows "continuous_on s (\x. inverse (f x))" @@ -850,7 +850,7 @@ shows "isCont (\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 \ 'b::real_normed_field" assumes "continuous_on s f" "continuous_on s g" and "\x\s. g x \ 0" shows "continuous_on s (\x. (f x) / (g x))" @@ -879,7 +879,7 @@ shows "isCont (\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 \ 'b::real_normed_vector" assumes "continuous_on s f" and "\x\s. f x \ 0" shows "continuous_on s (\x. sgn (f x))" @@ -1685,11 +1685,6 @@ shows "\i\A. isCont (f i) a \ isCont (\x. \i\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 diff -r 7c717ba55a0b -r fb9ae0727548 src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy --- 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 \ 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 \ s" "\y\s. (norm \ f) x \ (norm \ f) y" using continuous_attains_inf[OF assms(1), of "norm \ f"] unfolding o_def @@ -1460,7 +1460,7 @@ obtain d where d: "d > 0" "\x. x \ unit_cube \ d \ 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 *: "\x. x \ unit_cube \ f x \ 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 diff -r 7c717ba55a0b -r fb9ae0727548 src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy --- 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 \ continuous_on s (\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 \ 'b::real_normed_algebra" shows "uniformly_continuous_on s f \ uniformly_continuous_on s (\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 \ 'b::real_normed_algebra" assumes "uniformly_continuous_on s f" shows "uniformly_continuous_on s (\x. c * f x)" diff -r 7c717ba55a0b -r fb9ae0727548 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy --- 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 \ A" "a \ s" and b: "b \ B" "b \ s" by auto def f \ "\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] diff -r 7c717ba55a0b -r fb9ae0727548 src/HOL/Multivariate_Analysis/Derivative.thy --- 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 "((\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)" 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 \ {a <..< b}" "(\xa. f' x xa - (f b - f a) / (b - a) * xa) = (\v. 0)" .. @@ -749,7 +749,7 @@ have "\x\{a<.. f b - (f b - f a) \ f a = (f b - f a) \ 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 \ ?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 "\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) (\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) diff -r 7c717ba55a0b -r fb9ae0727548 src/HOL/Multivariate_Analysis/Fashoda.thy --- 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) \ {}" unfolding interval_eq_empty_cart by auto have 2: "continuous_on (cbox -1 1) (negatex \ sqprojection \ ?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 \ iscale) ` {- 1..1} \ cbox -1 1" "(g \ iscale) ` {- 1..1} \ 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 \ iscale)" "continuous_on {- 1..1} (g \ iscale)" apply - apply (rule_tac[!] continuous_on_compose[OF *]) diff -r 7c717ba55a0b -r fb9ae0727548 src/HOL/Multivariate_Analysis/Integration.thy --- 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 \ c" note conv = assms(1)[unfolded convex_alt,rule_format] have as1: "continuous_on {0 ..1} (f \ (\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) diff -r 7c717ba55a0b -r fb9ae0727548 src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy --- 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 = "(\x. x \ b) ` X" from assms have "compact ?proj" "?proj \ {}" - 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\(\x. x \ b) ` X" "\t. t\(\x. x \ b) ` X \ s \ t" @@ -133,7 +133,7 @@ proof atomize_elim let ?proj = "(\x. x \ b) ` X" from assms have "compact ?proj" "?proj \ {}" - 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\(\x. x \ b) ` X" "\t. t\(\x. x \ b) ` X \ t \ s" diff -r 7c717ba55a0b -r fb9ae0727548 src/HOL/Multivariate_Analysis/Path_Connected.thy --- 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 *: "\g. path g \ path (reversepath g)" unfolding path_def reversepath_def apply (rule continuous_on_compose[unfolded o_def, of _ "\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} \ {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 \ (\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="\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 \ x \ s" @@ -977,11 +977,11 @@ done have "continuous_on (UNIV - {0}) (\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 \ DIM('a::euclidean_space) \ connected {x::'a. norm (x - a) = r}" diff -r 7c717ba55a0b -r fb9ae0727548 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy --- 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 -` {.. continuous_on s (\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 \ '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 (\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 (\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 \ '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 (\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 (\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 \ 'b::real_normed_vector" assumes "uniformly_continuous_on s f" shows "uniformly_continuous_on s (\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 \ 'b::real_normed_vector" shows "uniformly_continuous_on s f \ uniformly_continuous_on s (\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 \ '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 \ '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 \ f)" proof - @@ -6972,7 +6972,7 @@ 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 simp add: continuous_on_intros) + apply (auto simp add: continuous_intros) done lemma homeomorphic_translation: @@ -7010,14 +7010,14 @@ apply(rule_tac x="\x. b + (e/d) *\<^sub>R (x - a)" in exI) apply(rule_tac x="\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="\x. b + (e/d) *\<^sub>R (x - a)" in exI) apply(rule_tac x="\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 diff -r 7c717ba55a0b -r fb9ae0727548 src/HOL/NthRoot.thy --- 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 = "\y::real. sgn y * \y\^n" have "continuous_on ({0..} \ {.. 0}) (\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]: "\x. isCont ?f x" @@ -275,7 +275,7 @@ "continuous F f \ continuous F (\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 \ continuous_on s (\x. root n (f x))" unfolding continuous_on_def by (auto intro: tendsto_real_root) @@ -454,7 +454,7 @@ "continuous F f \ continuous F (\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 \ 0 < n \ continuous_on s (\x. sqrt (f x))" unfolding sqrt_def by (rule continuous_on_real_root) diff -r 7c717ba55a0b -r fb9ae0727548 src/HOL/Probability/Borel_Space.thy --- 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 \ borel_measurable M" shows "(\x. f x \ g x) \ 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\linorder_topology" @@ -287,7 +287,7 @@ by auto also have "\ \ 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 \ 'b::{second_countable_topology, real_normed_vector}" assumes g: "g \ borel_measurable M" shows "(\x. - g x) \ 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 \ 'b::{second_countable_topology, real_normed_vector}" assumes f: "f \ borel_measurable M" assumes g: "g \ borel_measurable M" shows "(\x. f x + g x) \ 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 \ 'a \ 'b::{second_countable_topology, real_normed_vector}" @@ -689,7 +689,7 @@ assumes f: "f \ borel_measurable M" assumes g: "g \ borel_measurable M" shows "(\x. f x * g x) \ 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 \ 'a \ 'b::{second_countable_topology, real_normed_field}" @@ -705,14 +705,14 @@ assumes f: "f \ borel_measurable M" assumes g: "g \ borel_measurable M" shows "(\x. dist (f x) (g x)) \ 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 \ 'b::{second_countable_topology, real_normed_vector}" assumes f: "f \ borel_measurable M" assumes g: "g \ borel_measurable M" shows "(\x. f x *\<^sub>R g x) \ 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 \ 'x::real_normed_vector" @@ -749,7 +749,7 @@ shows "(\x. inverse (f x)) \ borel_measurable M" proof - have "(\x::'b. if x \ UNIV - {0} then inverse x else inverse 0) \ 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 "(\x::'b. if x \ UNIV - {0} then inverse x else inverse 0) = inverse" by (intro ext) auto finally show ?thesis using f by simp diff -r 7c717ba55a0b -r fb9ae0727548 src/HOL/Probability/Distributions.thy --- 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 (\x. x * exp (-x)) x :> exp (-x) - x * exp (-x)" by (auto intro!: DERIV_intros) show "isCont (\x. exp (- x) - x * exp (- x)) x " - by (intro isCont_intros isCont_exp') + by (intro continuous_intros) qed fact also have "(\x. (exp (-x)) * indicator {0 .. b} x \lborel) = - exp (- b) - - exp (- 0)" by (rule integral_FTC_atLeastAtMost) (auto intro!: DERIV_intros) diff -r 7c717ba55a0b -r fb9ae0727548 src/HOL/Topological_Spaces.thy --- 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 \ bool" where "closed S \ 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 \ open T \ open (S \ T)" +lemma open_Un [continuous_intros, intro]: "open S \ open T \ open (S \ T)" using open_Union [of "{S, T}"] by simp -lemma open_UN [intro]: "\x\A. open (B x) \ open (\x\A. B x)" +lemma open_UN [continuous_intros, intro]: "\x\A. open (B x) \ open (\x\A. B x)" using open_Union [of "B ` A"] by simp -lemma open_Inter [intro]: "finite S \ \T\S. open T \ open (\S)" +lemma open_Inter [continuous_intros, intro]: "finite S \ \T\S. open T \ open (\S)" by (induct set: finite) auto -lemma open_INT [intro]: "finite A \ \x\A. open (B x) \ open (\x\A. B x)" +lemma open_INT [continuous_intros, intro]: "finite A \ \x\A. open (B x) \ open (\x\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 \ closed T \ closed (S \ T)" +lemma closed_Un [continuous_intros, intro]: "closed S \ closed T \ closed (S \ 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 \ closed T \ closed (S \ T)" +lemma closed_Int [continuous_intros, intro]: "closed S \ closed T \ closed (S \ T)" unfolding closed_def by auto -lemma closed_INT [intro]: "\x\A. closed (B x) \ closed (\x\A. B x)" +lemma closed_INT [continuous_intros, intro]: "\x\A. closed (B x) \ closed (\x\A. B x)" unfolding closed_def by auto -lemma closed_Inter [intro]: "\S\K. closed S \ closed (\ K)" +lemma closed_Inter [continuous_intros, intro]: "\S\K. closed S \ closed (\ K)" unfolding closed_def uminus_Inf by auto -lemma closed_Union [intro]: "finite S \ \T\S. closed T \ closed (\S)" +lemma closed_Union [continuous_intros, intro]: "finite S \ \T\S. closed T \ closed (\S)" by (induct set: finite) auto -lemma closed_UN [intro]: "finite A \ \x\A. closed (B x) \ closed (\x\A. B x)" +lemma closed_UN [continuous_intros, intro]: "finite A \ \x\A. closed (B x) \ closed (\x\A. B x)" using closed_Union [of "B ` A"] by simp lemma open_closed: "open S \ closed (- S)" @@ -78,16 +90,16 @@ lemma closed_open: "closed S \ open (- S)" unfolding closed_def by simp -lemma open_Diff [intro]: "open S \ closed T \ open (S - T)" +lemma open_Diff [continuous_intros, intro]: "open S \ closed T \ open (S - T)" unfolding closed_open Diff_eq by (rule open_Int) -lemma closed_Diff [intro]: "closed S \ open T \ closed (S - T)" +lemma closed_Diff [continuous_intros, intro]: "closed S \ open T \ closed (S - T)" unfolding open_closed Diff_eq by (rule closed_Int) -lemma open_Compl [intro]: "closed S \ open (- S)" +lemma open_Compl [continuous_intros, intro]: "closed S \ open (- S)" unfolding closed_open . -lemma closed_Compl [intro]: "open S \ closed (- S)" +lemma closed_Compl [continuous_intros, intro]: "open S \ 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 ..} \ {.. 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: "(\s. s \ S \ open s) \ (\s. s \ S \ continuous_on s f) \ continuous_on (\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 (\x. x)" +lemma continuous_on_id[continuous_intros]: "continuous_on s (\x. x)" unfolding continuous_on_def by (fast intro: tendsto_ident_at) -lemma continuous_on_const[continuous_on_intros]: "continuous_on s (\x. c)" +lemma continuous_on_const[continuous_intros]: "continuous_on s (\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 \ continuous_on (f ` s) g \ continuous_on s (g o f)" unfolding continuous_on_topological by simp metis @@ -1801,18 +1807,6 @@ definition continuous :: "'a::t2_space filter \ ('a \ 'b::topological_space) \ bool" where "continuous F f \ (f ---> f (Lim F (\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 diff -r 7c717ba55a0b -r fb9ae0727548 src/HOL/Transcendental.thy --- 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 \ continuous F (\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 \ continuous_on s (\x. exp (f x))" unfolding continuous_on_def by (auto intro: tendsto_exp) @@ -1303,7 +1303,7 @@ "continuous (at x within s) f \ 0 < f x \ continuous (at x within s) (\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 \