# HG changeset patch # User hoelzl # Date 1264434984 -3600 # Node ID 4e8be3c04d37138e978e911b65b243a6a054bc09 # Parent 366a1a44aac22b48595268381c68a95b23ff3821 Replaced vec1 and dest_vec1 by abbreviation. diff -r 366a1a44aac2 -r 4e8be3c04d37 src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy --- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Fri Jan 22 16:59:21 2010 +0100 +++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Mon Jan 25 16:56:24 2010 +0100 @@ -1460,8 +1460,7 @@ let ?F = "(\w::real^2. (f \ vec1 \ (\x. x$1)) w - (g \ vec1 \ (\x. x$2)) w)" have *:"\i. vec1 ` (\x::real^2. x $ i) ` {- 1..1} = {- 1..1::real^1}" apply(rule set_ext) unfolding image_iff Bex_def mem_interval apply rule defer - apply(rule_tac x="dest_vec1 x" in exI) apply rule apply(rule_tac x="vec (dest_vec1 x)" in exI) - by(auto simp add: dest_vec1_def[THEN sym]) + apply(rule_tac x="dest_vec1 x" in exI) apply rule apply(rule_tac x="vec (dest_vec1 x)" in exI) by auto { fix x assume "x \ (\w. (f \ vec1 \ (\x. x $ 1)) w - (g \ vec1 \ (\x. x $ 2)) w) ` {- 1..1::real^2}" then guess w unfolding image_iff .. note w = this hence "x \ 0" using as[of "vec1 (w$1)" "vec1 (w$2)"] unfolding mem_interval by auto} note x0=this @@ -1539,7 +1538,7 @@ obtains z where "z \ path_image f" "z \ path_image g" proof- note assms=assms[unfolded path_def pathstart_def pathfinish_def path_image_def] def iscale \ "\z::real^1. inverse 2 *\<^sub>R (z + 1)" - have isc:"iscale ` {- 1..1} \ {0..1}" unfolding iscale_def by(auto simp add:dest_vec1_add dest_vec1_neg) + have isc:"iscale ` {- 1..1} \ {0..1}" unfolding iscale_def by(auto) have "\s\{- 1..1}. \t\{- 1..1}. (f \ iscale) s = (g \ iscale) t" proof(rule fashoda_unit) show "(f \ iscale) ` {- 1..1} \ {- 1..1}" "(g \ iscale) ` {- 1..1} \ {- 1..1}" using isc and assms(3-4) unfolding image_compose by auto diff -r 366a1a44aac2 -r 4e8be3c04d37 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri Jan 22 16:59:21 2010 +0100 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Mon Jan 25 16:56:24 2010 +0100 @@ -19,21 +19,14 @@ declare dot_lmult[simp] dot_rmult[simp] dot_lneg[simp] dot_rneg[simp] declare UNIV_1[simp] -lemma dim1in[intro]:"Suc 0 \ {1::nat .. CARD(1)}" by auto - -lemmas vector_component_simps = vector_minus_component vector_smult_component vector_add_component vector_le_def Cart_lambda_beta dest_vec1_def basis_component vector_uminus_component - -lemmas continuous_intros = continuous_add continuous_vmul continuous_cmul continuous_const continuous_sub continuous_at_id continuous_within_id - -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 - uniformly_continuous_on_add uniformly_continuous_on_const uniformly_continuous_on_id uniformly_continuous_on_compose uniformly_continuous_on_cmul uniformly_continuous_on_neg uniformly_continuous_on_sub +(*lemma dim1in[intro]:"Suc 0 \ {1::nat .. CARD(1)}" by auto*) + +lemmas vector_component_simps = vector_minus_component vector_smult_component vector_add_component vector_le_def Cart_lambda_beta basis_component vector_uminus_component lemma dest_vec1_simps[simp]: fixes a::"real^1" shows "a$1 = 0 \ a = 0" (*"a \ 1 \ dest_vec1 a \ 1" "0 \ a \ 0 \ dest_vec1 a"*) "a \ b \ dest_vec1 a \ dest_vec1 b" "dest_vec1 (1::real^1) = 1" - by(auto simp add:vector_component_simps all_1 Cart_eq) - -lemma nequals0I:"x\A \ A \ {}" by auto + by(auto simp add:vector_component_simps forall_1 Cart_eq) lemma norm_not_0:"(x::real^'n)\0 \ norm x \ 0" by auto @@ -59,7 +52,7 @@ lemma mem_interval_1: fixes x :: "real^1" shows "(x \ {a .. b} \ dest_vec1 a \ dest_vec1 x \ dest_vec1 x \ dest_vec1 b)" "(x \ {a<.. dest_vec1 a < dest_vec1 x \ dest_vec1 x < dest_vec1 b)" -by(simp_all add: Cart_eq vector_less_def vector_le_def dest_vec1_def all_1) +by(simp_all add: Cart_eq vector_less_def vector_le_def forall_1) lemma image_smult_interval:"(\x. m *\<^sub>R (x::real^'n)) ` {a..b} = (if {a..b} = {} then {} else if 0 \ m then {m *\<^sub>R a..m *\<^sub>R b} else {m *\<^sub>R b..m *\<^sub>R a})" @@ -75,8 +68,8 @@ apply(rule_tac [!] allI)apply(rule_tac [!] impI) apply(rule_tac[2] x="vec1 x" in exI)apply(rule_tac[4] x="vec1 x" in exI) apply(rule_tac[6] x="vec1 x" in exI)apply(rule_tac[8] x="vec1 x" in exI) - by (auto simp add: vector_less_def vector_le_def all_1 dest_vec1_def - vec1_dest_vec1[unfolded dest_vec1_def One_nat_def]) + by (auto simp add: vector_less_def vector_le_def forall_1 + vec1_dest_vec1[unfolded One_nat_def]) lemma dest_vec1_setsum: assumes "finite S" shows " dest_vec1 (setsum f S) = setsum (\x. dest_vec1 (f x)) S" @@ -611,7 +604,7 @@ subsection {* One rather trivial consequence. *} -lemma connected_UNIV: "connected (UNIV :: 'a::real_normed_vector set)" +lemma connected_UNIV[intro]: "connected (UNIV :: 'a::real_normed_vector set)" by(simp add: convex_connected convex_UNIV) subsection {* Convex functions into the reals. *} @@ -624,7 +617,7 @@ lemma convex_on_subset: "convex_on t f \ s \ t \ convex_on s f" unfolding convex_on_def by auto -lemma convex_add: +lemma convex_add[intro]: assumes "convex_on s f" "convex_on s g" shows "convex_on s (\x. f x + g x)" proof- @@ -638,7 +631,7 @@ thus ?thesis unfolding convex_on_def by auto qed -lemma convex_cmul: +lemma convex_cmul[intro]: assumes "0 \ (c::real)" "convex_on s f" shows "convex_on s (\x. c * f x)" proof- @@ -680,7 +673,7 @@ ultimately show False using mult_strict_left_mono[OF y `u>0`] unfolding left_diff_distrib by auto qed -lemma convex_distance: +lemma convex_distance[intro]: fixes s :: "'a::real_normed_vector set" shows "convex_on s (\x. dist a x)" proof(auto simp add: convex_on_def dist_norm) @@ -1248,7 +1241,7 @@ subsection {* Openness and compactness are preserved by convex hull operation. *} -lemma open_convex_hull: +lemma open_convex_hull[intro]: fixes s :: "'a::real_normed_vector set" assumes "open s" shows "open(convex hull s)" @@ -1287,8 +1280,7 @@ qed lemma open_dest_vec1_vimage: "open S \ open (dest_vec1 -` S)" -unfolding open_vector_def all_1 -by (auto simp add: dest_vec1_def) +unfolding open_vector_def forall_1 by auto lemma tendsto_dest_vec1 [tendsto_intros]: "(f ---> l) net \ ((\x. dest_vec1 (f x)) ---> dest_vec1 l) net" @@ -1837,7 +1829,7 @@ using ed(1,2) and u unfolding subset_eq mem_ball Ball_def dist_norm by(auto simp add: algebra_simps) thus "z \ s" using u by (auto simp add: algebra_simps) qed(insert u ed(3-4), auto) qed -lemma convex_hull_eq_empty: "convex hull s = {} \ s = {}" +lemma convex_hull_eq_empty[simp]: "convex hull s = {} \ s = {}" using hull_subset[of s convex] convex_hull_empty by auto subsection {* Moving and scaling convex hulls. *} @@ -2247,12 +2239,19 @@ lemma mem_epigraph: "(pastecart x (vec1 y)) \ epigraph s f \ x \ s \ f x \ y" unfolding epigraph_def by auto +(** move this**) +lemma forall_dest_vec1: "(\x. P x) \ (\x. P(dest_vec1 x))" + apply safe defer apply(erule_tac x="vec1 x" in allE) by auto + +(** This might break sooner or later. In fact it did already once. **) lemma convex_epigraph: "convex(epigraph s f) \ convex_on s f \ convex s" unfolding convex_def convex_on_def unfolding Ball_def forall_pastecart epigraph_def - unfolding mem_Collect_eq fstcart_pastecart sndcart_pastecart sndcart_add sndcart_cmul [where 'a=real, unfolded smult_conv_scaleR] fstcart_add fstcart_cmul [where 'a=real, unfolded smult_conv_scaleR] - unfolding Ball_def[symmetric] unfolding dest_vec1_add dest_vec1_cmul [where 'a=real, unfolded smult_conv_scaleR] - apply(subst forall_dest_vec1[THEN sym])+ by(meson real_le_refl real_le_trans add_mono mult_left_mono) + unfolding mem_Collect_eq fstcart_pastecart sndcart_pastecart sndcart_add sndcart_cmul [where 'a=real, unfolded smult_conv_scaleR] fstcart_add fstcart_cmul [where 'a=real, unfolded smult_conv_scaleR] Ball_def[symmetric] unfolding vector_add_component vector_scaleR_component + apply(subst forall_dest_vec1[THEN sym])+ + apply safe defer apply(erule_tac x=x in allE,erule_tac x="f x" in allE) apply safe + apply(erule_tac x=xa in allE,erule_tac x="f xa" in allE) prefer 3 + apply(rule_tac y="u * f x + v * f xb" in order_trans) defer by(auto intro!:mult_left_mono add_mono) lemma convex_epigraphI: assumes "convex_on s f" "convex s" shows "convex(epigraph s f)" using assms unfolding convex_epigraph by auto @@ -2284,13 +2283,13 @@ f (setsum (\i. u i *\<^sub>R x i) {1..k} ) \ setsum (\i. u i * f(x i)) {1..k} ) " unfolding convex_epigraph_convex[OF assms] convex epigraph_def Ball_def mem_Collect_eq unfolding sndcart_setsum[OF finite_atLeastAtMost] fstcart_setsum[OF finite_atLeastAtMost] dest_vec1_setsum[OF finite_atLeastAtMost] - unfolding fstcart_pastecart sndcart_pastecart sndcart_add sndcart_cmul [where 'a=real, unfolded smult_conv_scaleR] fstcart_add fstcart_cmul [where 'a=real, unfolded smult_conv_scaleR] - unfolding dest_vec1_add dest_vec1_cmul [where 'a=real, unfolded smult_conv_scaleR] apply(subst forall_of_pastecart)+ apply(subst forall_of_dest_vec1)+ apply rule + unfolding fstcart_pastecart sndcart_pastecart sndcart_add sndcart_cmul [where 'a=real, unfolded smult_conv_scaleR] fstcart_add fstcart_cmul [where 'a=real, unfolded smult_conv_scaleR] unfolding vector_scaleR_component + apply(subst forall_of_pastecart)+ apply(subst forall_of_dest_vec1)+ apply rule using assms[unfolded convex] apply simp apply(rule,rule,rule) apply(erule_tac x=k in allE, erule_tac x=u in allE, erule_tac x=x in allE) apply rule apply rule apply rule defer apply(rule_tac j="\i = 1..k. u i * f (x i)" in real_le_trans) - defer apply(rule setsum_mono) apply(erule conjE)+ apply(erule_tac x=i in allE)apply(rule mult_left_mono) - using assms[unfolded convex] by auto + defer apply(rule setsum_mono) apply(erule conjE)+ apply(erule_tac x=i in allE) unfolding real_scaleR_def + apply(rule mult_left_mono)using assms[unfolded convex] by auto subsection {* Convexity of general and special intervals. *} @@ -2324,7 +2323,7 @@ lemma is_interval_1: "is_interval s \ (\a\s. \b\s. \ x. dest_vec1 a \ dest_vec1 x \ dest_vec1 x \ dest_vec1 b \ x \ s)" - unfolding is_interval_def dest_vec1_def forall_1 by auto + unfolding is_interval_def forall_1 by auto lemma is_interval_connected_1: "is_interval s \ connected (s::(real^1) set)" apply(rule, rule is_interval_connected, assumption) unfolding is_interval_1 @@ -2333,8 +2332,8 @@ hence *:"dest_vec1 a < dest_vec1 x" "dest_vec1 x < dest_vec1 b" apply(rule_tac [!] ccontr) unfolding not_less by auto let ?halfl = "{z. inner (basis 1) z < dest_vec1 x} " and ?halfr = "{z. inner (basis 1) z > dest_vec1 x} " { fix y assume "y \ s" have "y \ ?halfr \ ?halfl" apply(rule ccontr) - using as(6) `y\s` by (auto simp add: inner_vector_def dest_vec1_eq [unfolded dest_vec1_def] dest_vec1_def) } - moreover have "a\?halfl" "b\?halfr" using * by (auto simp add: inner_vector_def dest_vec1_def) + using as(6) `y\s` by (auto simp add: inner_vector_def dest_vec1_eq) } + moreover have "a\?halfl" "b\?halfr" using * by (auto simp add: inner_vector_def) hence "?halfl \ s \ {}" "?halfr \ s \ {}" using as(2-3) by auto ultimately show False apply(rule_tac notE[OF as(1)[unfolded connected_def]]) apply(rule_tac x="?halfl" in exI, rule_tac x="?halfr" in exI) @@ -2355,7 +2354,7 @@ assumes "dest_vec1 a \ dest_vec1 b" "continuous_on {a .. b} f" "(f a)$k \ y" "y \ (f b)$k" shows "\x\{a..b}. (f x)$k = y" proof- have "f a \ f ` {a..b}" "f b \ f ` {a..b}" apply(rule_tac[!] imageI) - using assms(1) by(auto simp add: vector_le_def dest_vec1_def) + using assms(1) by(auto simp add: vector_le_def) thus ?thesis using connected_ivt_component[of "f ` {a..b}" "f a" "f b" k y] using connected_continuous_image[OF assms(2) convex_connected[OF convex_interval(1)]] using assms by(auto intro!: imageI) qed @@ -2919,8 +2918,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(rule continuous_on_sub, rule continuous_on_const, rule continuous_on_id) - apply(rule continuous_on_subset[of "{0..1}"], assumption) - by (auto, auto simp add:vector_le_def vector_component_simps elim!:ballE) + apply(rule continuous_on_subset[of "{0..1}"], assumption) by auto show ?thesis using *[of g] *[of "reversepath g"] unfolding reversepath_reversepath by auto qed lemmas reversepath_simps = path_reversepath path_image_reversepath pathstart_reversepath pathfinish_reversepath @@ -2931,7 +2929,7 @@ have *:"g1 = (\x. g1 (2 *\<^sub>R x)) \ (\x. (1/2) *\<^sub>R x)" "g2 = (\x. g2 (2 *\<^sub>R x - 1)) \ (\x. (1/2) *\<^sub>R (x + 1))" unfolding o_def by auto have "op *\<^sub>R (1 / 2) ` {0::real^1..1} \ {0..1}" "(\x. (1 / 2) *\<^sub>R (x + 1)) ` {(0::real^1)..1} \ {0..1}" - unfolding image_smult_interval by (auto, auto simp add:vector_le_def vector_component_simps elim!:ballE) + unfolding image_smult_interval 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 @@ -3000,9 +2998,8 @@ apply(erule_tac x="1-x" in ballE, erule_tac x="1-y" in ballE) unfolding mem_interval_1 by(auto simp add:vector_component_simps) -lemma dest_vec1_scaleR [simp]: - "dest_vec1 (scaleR a x) = scaleR a (dest_vec1 x)" -unfolding dest_vec1_def by simp +(** move this **) +declare vector_scaleR_component[simp] lemma simple_path_join_loop: assumes "injective_path g1" "injective_path g2" "pathfinish g2 = pathstart g1" @@ -3013,14 +3010,13 @@ fix x y::"real^1" assume xy:"x \ {0..1}" "y \ {0..1}" "?g x = ?g y" show "x = y \ x = 0 \ y = 1 \ x = 1 \ y = 0" proof(case_tac "x$1 \ 1/2",case_tac[!] "y$1 \ 1/2", unfold not_le) assume as:"x $ 1 \ 1 / 2" "y $ 1 \ 1 / 2" - hence "g1 (2 *\<^sub>R x) = g1 (2 *\<^sub>R y)" using xy(3) unfolding joinpaths_def dest_vec1_def by auto + hence "g1 (2 *\<^sub>R x) = g1 (2 *\<^sub>R y)" using xy(3) unfolding joinpaths_def by auto moreover have "2 *\<^sub>R x \ {0..1}" "2 *\<^sub>R y \ {0..1}" using xy(1,2) as - unfolding mem_interval_1 dest_vec1_def by(auto simp add:vector_component_simps) + unfolding mem_interval_1 by(auto simp add:vector_component_simps) ultimately show ?thesis using inj(1)[of "2*\<^sub>R x" "2*\<^sub>R y"] by auto next assume as:"x $ 1 > 1 / 2" "y $ 1 > 1 / 2" - hence "g2 (2 *\<^sub>R x - 1) = g2 (2 *\<^sub>R y - 1)" using xy(3) unfolding joinpaths_def dest_vec1_def by auto - moreover have "2 *\<^sub>R x - 1 \ {0..1}" "2 *\<^sub>R y - 1 \ {0..1}" using xy(1,2) as - unfolding mem_interval_1 dest_vec1_def by(auto simp add:vector_component_simps) + hence "g2 (2 *\<^sub>R x - 1) = g2 (2 *\<^sub>R y - 1)" using xy(3) unfolding joinpaths_def by auto + moreover have "2 *\<^sub>R x - 1 \ {0..1}" "2 *\<^sub>R y - 1 \ {0..1}" using xy(1,2) as unfolding mem_interval_1 by(auto simp add:vector_component_simps) ultimately show ?thesis using inj(2)[of "2*\<^sub>R x - 1" "2*\<^sub>R y - 1"] by auto next assume as:"x $ 1 \ 1 / 2" "y $ 1 > 1 / 2" hence "?g x \ path_image g1" "?g y \ path_image g2" unfolding path_image_def joinpaths_def @@ -3055,6 +3051,7 @@ shows "injective_path(g1 +++ g2)" unfolding injective_path_def proof(rule,rule,rule) let ?g = "g1 +++ g2" note inj = assms(1,2)[unfolded injective_path_def, rule_format] + have *:"\x y::real^1. 2 *\<^sub>R x = 1 \ 2 *\<^sub>R y = 1 \ x = y" unfolding Cart_eq forall_1 by(auto simp del:dest_vec1_eq) fix x y assume xy:"x \ {0..1}" "y \ {0..1}" "(g1 +++ g2) x = (g1 +++ g2) y" show "x = y" proof(cases "x$1 \ 1/2", case_tac[!] "y$1 \ 1/2", unfold not_le) assume "x $ 1 \ 1 / 2" "y $ 1 \ 1 / 2" thus ?thesis using inj(1)[of "2*\<^sub>R x" "2*\<^sub>R y"] and xy @@ -3067,14 +3064,14 @@ hence "?g x = pathfinish g1" "?g y = pathstart g2" using assms(4) unfolding assms(3) xy(3) by auto thus ?thesis using as and inj(1)[of "2 *\<^sub>R x" 1] inj(2)[of "2 *\<^sub>R y - 1" 0] and xy(1,2) unfolding pathstart_def pathfinish_def joinpaths_def mem_interval_1 - by(auto simp add:vector_component_simps Cart_eq forall_1) + by(auto simp add:vector_component_simps intro:*) next assume as:"x $ 1 > 1 / 2" "y $ 1 \ 1 / 2" hence "?g x \ path_image g2" "?g y \ path_image g1" unfolding path_image_def joinpaths_def using xy(1,2)[unfolded mem_interval_1] by(auto simp add:vector_component_simps intro!: imageI) hence "?g x = pathstart g2" "?g y = pathfinish g1" using assms(4) unfolding assms(3) xy(3) by auto thus ?thesis using as and inj(2)[of "2 *\<^sub>R x - 1" 0] inj(1)[of "2 *\<^sub>R y" 1] and xy(1,2) unfolding pathstart_def pathfinish_def joinpaths_def mem_interval_1 - by(auto simp add:vector_component_simps forall_1 Cart_eq) qed qed + by(auto simp add:vector_component_simps intro:*) qed qed lemmas join_paths_simps = path_join path_image_join pathstart_join pathfinish_join @@ -3345,6 +3342,7 @@ next case True hence d:"1\{1..CARD('n)}" "2\{1..CARD('n)}" using Suc(2) by auto have ***:"Suc 1 = 2" by auto have **:"\s t P Q. s \ t \ {x. P x \ Q x} = (s \ {x. P x}) \ (t \ {x. Q x})" by auto + have nequals0I:"\x A. x\A \ A \ {}" by auto have "\ 2 \ \ (Suc 0)" apply(rule ccontr) using \[unfolded bij_betw_def inj_on_def, THEN conjunct1, THEN bspec[where x=2]] using assms by auto thus ?thesis unfolding * True unfolding ** neq_iff bex_disj_distrib apply - apply(rule path_connected_Un, rule_tac[1-2] path_connected_Un) defer 3 apply(rule_tac[1-4] convex_imp_path_connected) diff -r 366a1a44aac2 -r 4e8be3c04d37 src/HOL/Multivariate_Analysis/Derivative.thy --- a/src/HOL/Multivariate_Analysis/Derivative.thy Fri Jan 22 16:59:21 2010 +0100 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy Mon Jan 25 16:56:24 2010 +0100 @@ -212,7 +212,7 @@ using assms[unfolded has_derivative_def Lim] by auto thus "eventually (\x. dist (1 / norm (x - netlimit net) * (c x $ k - (c (netlimit net) $ k + c' (x - netlimit net) $ k))) 0 < e) net" proof (rule eventually_elim1) - case goal1 thus ?case apply - unfolding vector_dist_norm vec1_vec apply(rule le_less_trans) prefer 2 apply assumption unfolding * ** and norm_vec1[unfolded vec1_vec] + case goal1 thus ?case apply - unfolding vector_dist_norm apply(rule le_less_trans) prefer 2 apply assumption unfolding * ** and norm_vec1 using component_le_norm[of "(1 / norm (x - netlimit net)) *\<^sub>R (c x - (c (netlimit net) + c' (x - netlimit net))) - 0" k] by auto qed qed(insert assms[unfolded has_derivative_def], auto simp add:linear_conv_bounded_linear) qed @@ -619,7 +619,7 @@ note deriv = assms(3)[unfolded has_derivative_at_vec1] obtain e where e:"e>0" "ball x e \ s" using assms(2)[unfolded open_contains_ball] and assms(1) by auto hence **:"(jacobian (vec1 \ f) (at x)) $ 1 = 0" using differential_zero_maxmin_component[of e x "\x. vec1 (f x)" 1] - unfolding dest_vec1_def[THEN sym] vec1_dest_vec1 using assms(4) and assms(3)[unfolded has_derivative_at_vec1 o_def] + using assms(4) and assms(3)[unfolded has_derivative_at_vec1 o_def] unfolding differentiable_def o_def by auto have *:"jacobian (vec1 \ f) (at x) = matrix (vec1 \ f')" unfolding jacobian_def and frechet_derivative_at[OF deriv] .. have "vec1 \ f' = (\x. 0)" apply(rule) unfolding matrix_works[OF derivative_is_linear[OF deriv],THEN sym] @@ -651,7 +651,7 @@ hence "f' x \ dest_vec1 = (\v. 0)" apply(rule_tac differential_zero_maxmin[of "vec1 x" "vec1 ` {a<.. dest_vec1" "(f' x) \ dest_vec1"]) unfolding vec1_interval defer apply(rule open_interval) apply(rule assms(4)[unfolded has_derivative_at_dest_vec1[THEN sym],THEN bspec[where x=x]],assumption) - unfolding o_def apply(erule disjE,rule disjI2) by(auto simp add: vector_less_def dest_vec1_def) + unfolding o_def apply(erule disjE,rule disjI2) by(auto simp add: vector_less_def) thus ?thesis apply(rule_tac x=x in bexI) unfolding o_def apply rule apply(drule_tac x="vec1 v" in fun_cong) unfolding vec1_dest_vec1 using x(1) by auto qed @@ -738,12 +738,14 @@ also have "\ \ B * norm(y - x)" apply(rule **) using * and u by auto finally show ?thesis by(auto simp add:norm_minus_commute) qed +(** move this **) +declare norm_vec1[simp] + lemma onorm_vec1: fixes f::"real \ real" shows "onorm (\x. vec1 (f (dest_vec1 x))) = onorm f" proof- - have "\x::real^1. norm x = 1 \ x\{vec1 -1, vec1 (1::real)}" unfolding forall_vec1 unfolding norm_vec1 by auto + have "\x::real^1. norm x = 1 \ x\{vec1 -1, vec1 (1::real)}" unfolding forall_vec1 by(auto simp add:Cart_eq) hence 1:"{x. norm x = 1} = {vec1 -1, vec1 (1::real)}" by(auto simp add:norm_vec1) have 2:"{norm (vec1 (f (dest_vec1 x))) |x. norm x = 1} = (\x. norm (vec1 (f (dest_vec1 x)))) ` {x. norm x=1}" by auto - have "\x::real. norm x = 1 \ x\{-1, 1}" by auto hence 3:"{x. norm x = 1} = {-1, (1::real)}" by auto have 4:"{norm (f x) |x. norm x = 1} = (\x. norm (f x)) ` {x. norm x=1}" by auto show ?thesis unfolding onorm_def 1 2 3 4 by(simp add:Sup_finite_Max norm_vec1) qed diff -r 366a1a44aac2 -r 4e8be3c04d37 src/HOL/Multivariate_Analysis/Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Fri Jan 22 16:59:21 2010 +0100 +++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Mon Jan 25 16:56:24 2010 +0100 @@ -14,9 +14,12 @@ text{* Some common special cases.*} -lemma forall_1: "(\i::1. P i) \ P 1" +lemma forall_1[simp]: "(\i::1. P i) \ P 1" by (metis num1_eq_iff) +lemma ex_1[simp]: "(\x::1. P x) \ P 1" + by auto (metis num1_eq_iff) + lemma exhaust_2: fixes x :: 2 shows "x = 1 \ x = 2" proof (induct x) @@ -196,7 +199,6 @@ instance cart :: (semigroup_add,finite) semigroup_add apply (intro_classes) by (vector add_assoc) - instance cart :: (monoid_add,finite) monoid_add apply (intro_classes) by vector+ @@ -2418,87 +2420,65 @@ (* "lift" from 'a to 'a^1 and "drop" from 'a^1 to 'a -- FIXME: potential use of transfer *) -definition vec1:: "'a \ 'a ^ 1" where "vec1 x = (\ i. x)" - -definition dest_vec1:: "'a ^1 \ 'a" - where "dest_vec1 x = (x$1)" +abbreviation vec1:: "'a \ 'a ^ 1" where "vec1 x \ vec x" + +abbreviation dest_vec1:: "'a ^1 \ 'a" + where "dest_vec1 x \ (x$1)" lemma vec1_component[simp]: "(vec1 x)$1 = x" - by (simp add: vec1_def) + by (simp add: ) lemma vec1_dest_vec1[simp]: "vec1(dest_vec1 x) = x" "dest_vec1(vec1 y) = y" - by (simp_all add: vec1_def dest_vec1_def Cart_eq forall_1) + by (simp_all add: Cart_eq forall_1) lemma forall_vec1: "(\x. P x) \ (\x. P (vec1 x))" by (metis vec1_dest_vec1) lemma exists_vec1: "(\x. P x) \ (\x. P(vec1 x))" by (metis vec1_dest_vec1) -lemma forall_dest_vec1: "(\x. P x) \ (\x. P(dest_vec1 x))" by (metis vec1_dest_vec1) - -lemma exists_dest_vec1: "(\x. P x) \ (\x. P(dest_vec1 x))"by (metis vec1_dest_vec1) - lemma vec1_eq[simp]: "vec1 x = vec1 y \ x = y" by (metis vec1_dest_vec1) lemma dest_vec1_eq[simp]: "dest_vec1 x = dest_vec1 y \ x = y" by (metis vec1_dest_vec1) -lemma vec1_in_image_vec1: "vec1 x \ (vec1 ` S) \ x \ S" by auto - -lemma vec1_vec: "vec1 x = vec x" by (vector vec1_def) - -lemma vec1_add: "vec1(x + y) = vec1 x + vec1 y" by (vector vec1_def) -lemma vec1_sub: "vec1(x - y) = vec1 x - vec1 y" by (vector vec1_def) -lemma vec1_cmul: "vec1(c* x) = c *s vec1 x " by (vector vec1_def) -lemma vec1_neg: "vec1(- x) = - vec1 x " by (vector vec1_def) - -lemma vec1_0[simp]:"vec1 0 = 0" unfolding vec1_def Cart_eq by auto +lemma vec_in_image_vec: "vec x \ (vec ` S) \ x \ S" by auto + +lemma vec_add: "vec(x + y) = vec x + vec y" by (vector vec_def) +lemma vec_sub: "vec(x - y) = vec x - vec y" by (vector vec_def) +lemma vec_cmul: "vec(c* x) = c *s vec x " by (vector vec_def) +lemma vec_neg: "vec(- x) = - vec x " by (vector vec_def) lemma range_vec1[simp]:"range vec1 = UNIV" apply(rule set_ext,rule) unfolding image_iff defer apply(rule_tac x="dest_vec1 x" in bexI) by auto -lemma vec1_setsum: assumes fS: "finite S" - shows "vec1(setsum f S) = setsum (vec1 o f) S" +lemma vec_setsum: assumes fS: "finite S" + shows "vec(setsum f S) = setsum (vec o f) S" apply (induct rule: finite_induct[OF fS]) - apply (simp add: vec1_vec) - apply (auto simp add: vec1_add) + apply (simp) + apply (auto simp add: vec_add) done lemma dest_vec1_lambda: "dest_vec1(\ i. x i) = x 1" - by (simp add: dest_vec1_def) + by (simp) lemma dest_vec1_vec: "dest_vec1(vec x) = x" - by (simp add: vec1_vec[symmetric]) - -lemma dest_vec1_add: "dest_vec1(x + y) = dest_vec1 x + dest_vec1 y" - by (metis vec1_dest_vec1 vec1_add) - -lemma dest_vec1_sub: "dest_vec1(x - y) = dest_vec1 x - dest_vec1 y" - by (metis vec1_dest_vec1 vec1_sub) - -lemma dest_vec1_cmul: "dest_vec1(c*sx) = c * dest_vec1 x" - by (metis vec1_dest_vec1 vec1_cmul) - -lemma dest_vec1_neg: "dest_vec1(- x) = - dest_vec1 x" - by (metis vec1_dest_vec1 vec1_neg) - -lemma dest_vec1_0[simp]: "dest_vec1 0 = 0" by (metis vec_0 dest_vec1_vec) + by (simp) lemma dest_vec1_sum: assumes fS: "finite S" shows "dest_vec1(setsum f S) = setsum (dest_vec1 o f) S" apply (induct rule: finite_induct[OF fS]) apply (simp add: dest_vec1_vec) - apply (auto simp add: dest_vec1_add) + apply (auto simp add:vector_minus_component) done lemma norm_vec1: "norm(vec1 x) = abs(x)" - by (simp add: vec1_def norm_real) + by (simp add: vec_def norm_real) lemma dist_vec1: "dist(vec1 x) (vec1 y) = abs(x - y)" by (simp only: dist_real vec1_component) lemma abs_dest_vec1: "norm x = \dest_vec1 x\" by (metis vec1_dest_vec1 norm_vec1) -lemmas vec1_dest_vec1_simps = forall_vec1 vec1_add[THEN sym] dist_vec1 vec1_sub[THEN sym] vec1_dest_vec1 norm_vec1 dest_vec1_cmul - vec1_eq vec1_cmul[THEN sym] smult_conv_scaleR[THEN sym] o_def dist_real_def norm_vec1 real_norm_def +lemmas vec1_dest_vec1_simps = forall_vec1 vec_add[THEN sym] dist_vec1 vec_sub[THEN sym] vec1_dest_vec1 norm_vec1 vector_smult_component + vec1_eq vec_cmul[THEN sym] smult_conv_scaleR[THEN sym] o_def dist_real_def norm_vec1 real_norm_def lemma bounded_linear_vec1:"bounded_linear (vec1::real\real^1)" unfolding bounded_linear_def additive_def bounded_linear_axioms_def @@ -2508,7 +2488,6 @@ lemma linear_vmul_dest_vec1: fixes f:: "'a::semiring_1^_ \ 'a^1" shows "linear f \ linear (\x. dest_vec1(f x) *s v)" - unfolding dest_vec1_def apply (rule linear_vmul_component) by auto @@ -2517,14 +2496,14 @@ shows "f = (\x. dest_vec1 x *s column 1 (matrix f))" apply (rule ext) apply (subst matrix_works[OF lf, symmetric]) - apply (auto simp add: Cart_eq matrix_vector_mult_def dest_vec1_def column_def mult_commute UNIV_1) + apply (auto simp add: Cart_eq matrix_vector_mult_def column_def mult_commute UNIV_1) done lemma linear_to_scalars: assumes lf: "linear (f::'a::comm_ring_1 ^'n \ 'a^1)" shows "f = (\x. vec1(row 1 (matrix f) \ x))" apply (rule ext) apply (subst matrix_works[OF lf, symmetric]) - apply (simp add: Cart_eq matrix_vector_mult_def vec1_def row_def dot_def mult_commute forall_1) + apply (simp add: Cart_eq matrix_vector_mult_def row_def dot_def mult_commute forall_1) done lemma dest_vec1_eq_0: "dest_vec1 x = 0 \ x = 0" @@ -2532,7 +2511,7 @@ lemma setsum_scalars: assumes fS: "finite S" shows "setsum f S = vec1 (setsum (dest_vec1 o f) S)" - unfolding vec1_setsum[OF fS] by simp + unfolding vec_setsum[OF fS] by simp lemma dest_vec1_wlog_le: "(\(x::'a::linorder ^ 1) y. P x y \ P y x) \ (\x y. dest_vec1 x <= dest_vec1 y ==> P x y) \ P x y" apply (cases "dest_vec1 x \ dest_vec1 y") @@ -2543,10 +2522,10 @@ text{* Pasting vectors. *} -lemma linear_fstcart: "linear fstcart" +lemma linear_fstcart[intro]: "linear fstcart" by (auto simp add: linear_def Cart_eq) -lemma linear_sndcart: "linear sndcart" +lemma linear_sndcart[intro]: "linear sndcart" by (auto simp add: linear_def Cart_eq) lemma fstcart_vec[simp]: "fstcart(vec x) = vec x" @@ -2690,7 +2669,7 @@ lemma hull_hull: "S hull (S hull s) = S hull s" unfolding hull_def by blast -lemma hull_subset: "s \ (S hull s)" +lemma hull_subset[intro]: "s \ (S hull s)" unfolding hull_def by blast lemma hull_mono: " s \ t ==> (S hull s) \ (S hull t)" diff -r 366a1a44aac2 -r 4e8be3c04d37 src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy --- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Fri Jan 22 16:59:21 2010 +0100 +++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Mon Jan 25 16:56:24 2010 +0100 @@ -77,13 +77,13 @@ lemma finite_sum_image: "(UNIV::('a + 'b) set) = range Inl \ range Inr" by (auto, case_tac x, auto) -lemma fstcart_pastecart: "fstcart (pastecart x y) = x" +lemma fstcart_pastecart[simp]: "fstcart (pastecart x y) = x" by (simp add: Cart_eq) -lemma sndcart_pastecart: "sndcart (pastecart x y) = y" +lemma sndcart_pastecart[simp]: "sndcart (pastecart x y) = y" by (simp add: Cart_eq) -lemma pastecart_fst_snd: "pastecart (fstcart z) (sndcart z) = z" +lemma pastecart_fst_snd[simp]: "pastecart (fstcart z) (sndcart z) = z" by (simp add: Cart_eq pastecart_def fstcart_def sndcart_def split: sum.split) lemma pastecart_eq: "(x = y) \ (fstcart x = fstcart y) \ (sndcart x = sndcart y)" diff -r 366a1a44aac2 -r 4e8be3c04d37 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri Jan 22 16:59:21 2010 +0100 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Jan 25 16:56:24 2010 +0100 @@ -9,8 +9,6 @@ imports SEQ Euclidean_Space Product_Vector begin -declare fstcart_pastecart[simp] sndcart_pastecart[simp] - subsection{* General notion of a topology *} definition "istopology L \ {} \ L \ (\S \L. \T \L. S \ T \ L) \ (\K. K \L \ \ K \ L)" @@ -947,7 +945,7 @@ lemma frontier_subset_closed: "closed S \ frontier S \ S" by (metis frontier_def closure_closed Diff_subset) -lemma frontier_empty: "frontier {} = {}" +lemma frontier_empty[simp]: "frontier {} = {}" by (simp add: frontier_def closure_empty) lemma frontier_subset_eq: "frontier S \ S \ closed S" @@ -1038,7 +1036,7 @@ apply (simp add: norm_sgn) done -lemma trivial_limit_sequentially: "\ trivial_limit sequentially" +lemma trivial_limit_sequentially[intro]: "\ trivial_limit sequentially" by (auto simp add: trivial_limit_def Rep_net_sequentially) subsection{* Some property holds "sufficiently close" to the limit point. *} @@ -1248,10 +1246,9 @@ lemma Lim_ident_at: "((\x. x) ---> a) (at a)" unfolding tendsto_def Limits.eventually_at_topological by fast -lemma Lim_const: "((\x. a) ---> a) net" - by (rule tendsto_const) - -lemma Lim_cmul: +lemma Lim_const[intro]: "((\x. a) ---> a) net" by (rule tendsto_const) + +lemma Lim_cmul[intro]: fixes f :: "'a \ 'b::real_normed_vector" shows "(f ---> l) net ==> ((\x. c *\<^sub>R f x) ---> c *\<^sub>R l) net" by (intro tendsto_intros) @@ -3417,6 +3414,7 @@ shows "continuous net f \ continuous net g \ continuous net (\x. f x - g x)" by (auto simp add: continuous_def Lim_sub) + text{* Same thing for setwise continuity. *} lemma continuous_on_const: @@ -4219,6 +4217,8 @@ ==> continuous net (\x. c(x) *\<^sub>R f x) " unfolding continuous_def by (intro tendsto_intros) +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)" @@ -4231,6 +4231,10 @@ ==> continuous_on s (\x. c(x) *\<^sub>R f x)" unfolding continuous_on_eq_continuous_within using continuous_mul[of _ c] by auto +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 + uniformly_continuous_on_add uniformly_continuous_on_const uniformly_continuous_on_id uniformly_continuous_on_compose uniformly_continuous_on_cmul uniformly_continuous_on_neg uniformly_continuous_on_sub + continuous_on_mul continuous_on_vmul + text{* And so we have continuity of inverse. *} lemma Lim_inv: @@ -4300,7 +4304,7 @@ using assms(1)[unfolded closed_sequential_limits, THEN spec[where x="\n. fstcart (x n)"], THEN spec[where x="fstcart l"]] using assms(2)[unfolded closed_sequential_limits, THEN spec[where x="\n. sndcart (x n)"], THEN spec[where x="sndcart l"]] unfolding Lim_sequentially by auto - hence "l \ {pastecart x y |x y. x \ s \ y \ t}" using pastecart_fst_snd[THEN sym, of l] by auto } + hence "l \ {pastecart x y |x y. x \ s \ y \ t}" apply- unfolding mem_Collect_eq apply(rule_tac x="fstcart l" in exI,rule_tac x="sndcart l" in exI) by auto } thus ?thesis unfolding closed_sequential_limits by auto qed @@ -4636,13 +4640,13 @@ lemma mem_interval_1: fixes x :: "real^1" shows "(x \ {a .. b} \ dest_vec1 a \ dest_vec1 x \ dest_vec1 x \ dest_vec1 b)" "(x \ {a<.. dest_vec1 a < dest_vec1 x \ dest_vec1 x < dest_vec1 b)" -by(simp_all add: Cart_eq vector_less_def vector_le_def dest_vec1_def forall_1) +by(simp_all add: Cart_eq vector_less_def vector_le_def forall_1) lemma vec1_interval:fixes a::"real" shows "vec1 ` {a .. b} = {vec1 a .. vec1 b}" "vec1 ` {a<.. x < b ==> (\d>0. \x'. abs(x' - x) < d --> a < x' \ x' < b)" by(rule_tac x="min (x - a) (b - x)" in exI, auto) -lemma open_interval: fixes a :: "real^'n" shows "open {a<..{a<..e>0. \x'\{a..b}. x' \ x \ dist x' x < e"(* and xab:"a$i > x$i \ b$i < x$i"*) { assume xa:"a$i > x$i" @@ -4853,7 +4857,7 @@ thus ?thesis unfolding closed_limpt islimpt_approachable mem_interval by auto qed -lemma interior_closed_interval: fixes a :: "real^'n" shows +lemma interior_closed_interval[intro]: fixes a :: "real^'n" shows "interior {a .. b} = {a<.. ?L" using interior_maximal[OF interval_open_subset_closed open_interval] by auto @@ -5025,25 +5029,19 @@ (* Some special cases for intervals in R^1. *) -lemma all_1: "(\x::1. P x) \ P 1" - by (metis num1_eq_iff) - -lemma ex_1: "(\x::1. P x) \ P 1" - by auto (metis num1_eq_iff) - lemma interval_cases_1: fixes x :: "real^1" shows "x \ {a .. b} ==> x \ {a<.. (x = a) \ (x = b)" - by(simp add: Cart_eq vector_less_def vector_le_def all_1, auto) + unfolding Cart_eq vector_less_def vector_le_def mem_interval by(auto simp del:dest_vec1_eq) lemma in_interval_1: fixes x :: "real^1" shows "(x \ {a .. b} \ dest_vec1 a \ dest_vec1 x \ dest_vec1 x \ dest_vec1 b) \ (x \ {a<.. dest_vec1 a < dest_vec1 x \ dest_vec1 x < dest_vec1 b)" -by(simp add: Cart_eq vector_less_def vector_le_def all_1 dest_vec1_def) + unfolding Cart_eq vector_less_def vector_le_def mem_interval by(auto simp del:dest_vec1_eq) lemma interval_eq_empty_1: fixes a :: "real^1" shows "{a .. b} = {} \ dest_vec1 b < dest_vec1 a" "{a<.. dest_vec1 b \ dest_vec1 a" - unfolding interval_eq_empty and ex_1 and dest_vec1_def by auto + unfolding interval_eq_empty and ex_1 by auto lemma subset_interval_1: fixes a :: "real^1" shows "({a .. b} \ {c .. d} \ dest_vec1 b < dest_vec1 a \ @@ -5054,30 +5052,30 @@ dest_vec1 c \ dest_vec1 a \ dest_vec1 a < dest_vec1 b \ dest_vec1 b \ dest_vec1 d)" "({a<.. {c<.. dest_vec1 b \ dest_vec1 a \ dest_vec1 c \ dest_vec1 a \ dest_vec1 a < dest_vec1 b \ dest_vec1 b \ dest_vec1 d)" - unfolding subset_interval[of a b c d] unfolding all_1 and dest_vec1_def by auto + unfolding subset_interval[of a b c d] unfolding forall_1 by auto lemma eq_interval_1: fixes a :: "real^1" shows "{a .. b} = {c .. d} \ dest_vec1 b < dest_vec1 a \ dest_vec1 d < dest_vec1 c \ dest_vec1 a = dest_vec1 c \ dest_vec1 b = dest_vec1 d" -using set_eq_subset[of "{a .. b}" "{c .. d}"] -using subset_interval_1(1)[of a b c d] -using subset_interval_1(1)[of c d a b] -by auto (* FIXME: slow *) +unfolding set_eq_subset[of "{a .. b}" "{c .. d}"] +unfolding subset_interval_1(1)[of a b c d] +unfolding subset_interval_1(1)[of c d a b] +by auto lemma disjoint_interval_1: fixes a :: "real^1" shows "{a .. b} \ {c .. d} = {} \ dest_vec1 b < dest_vec1 a \ dest_vec1 d < dest_vec1 c \ dest_vec1 b < dest_vec1 c \ dest_vec1 d < dest_vec1 a" "{a .. b} \ {c<.. dest_vec1 b < dest_vec1 a \ dest_vec1 d \ dest_vec1 c \ dest_vec1 b \ dest_vec1 c \ dest_vec1 d \ dest_vec1 a" "{a<.. {c .. d} = {} \ dest_vec1 b \ dest_vec1 a \ dest_vec1 d < dest_vec1 c \ dest_vec1 b \ dest_vec1 c \ dest_vec1 d \ dest_vec1 a" "{a<.. {c<.. dest_vec1 b \ dest_vec1 a \ dest_vec1 d \ dest_vec1 c \ dest_vec1 b \ dest_vec1 c \ dest_vec1 d \