--- a/src/HOL/Library/Convex_Euclidean_Space.thy Thu May 28 14:36:21 2009 -0700
+++ b/src/HOL/Library/Convex_Euclidean_Space.thy Thu May 28 17:00:02 2009 -0700
@@ -118,7 +118,7 @@
lemma dist_triangle_eq:"dist x z = dist x y + dist y z \<longleftrightarrow> norm (x - y) *s (y - z) = norm (y - z) *s (x - y)"
proof- have *:"x - y + (y - z) = x - z" by auto
- show ?thesis unfolding dist_def norm_triangle_eq[of "x - y" "y - z", unfolded *]
+ show ?thesis unfolding dist_norm norm_triangle_eq[of "x - y" "y - z", unfolded *]
by(auto simp add:norm_minus_commute) qed
lemma norm_eqI:"x = y \<Longrightarrow> norm x = norm y" by auto
@@ -601,7 +601,7 @@
have "\<exists>x\<ge>0. x \<le> 1 \<and> (1 - x) *s x1 + x *s x2 \<notin> e1 \<and> (1 - x) *s x1 + x *s x2 \<notin> e2"
apply(rule connected_real_lemma) apply (simp add: `x1\<in>e1` `x2\<in>e2` dist_commute)+
- using * apply(simp add: dist_def)
+ using * apply(simp add: dist_norm)
using as(1,2)[unfolded open_def] apply simp
using as(1,2)[unfolded open_def] apply simp
using assms[unfolded convex_alt, THEN bspec[where x=x1], THEN bspec[where x=x2]] using x1 x2
@@ -675,14 +675,14 @@
using assms(2)[unfolded convex_on_def, THEN bspec[where x=x], THEN bspec[where x=y], THEN spec[where x="1-u"]] by auto
moreover
have *:"x - ((1 - u) *s x + u *s y) = u *s (x - y)" by (simp add: vector_ssub_ldistrib vector_sub_rdistrib)
- have "(1 - u) *s x + u *s y \<in> ball x e" unfolding mem_ball dist_def unfolding * and norm_mul and abs_of_pos[OF `0<u`] unfolding dist_def[THEN sym]
+ have "(1 - u) *s x + u *s y \<in> ball x e" unfolding mem_ball dist_norm unfolding * and norm_mul and abs_of_pos[OF `0<u`] unfolding dist_norm[THEN sym]
using u unfolding pos_less_divide_eq[OF xy] by auto
hence "f x \<le> f ((1 - u) *s x + u *s y)" using assms(4) by auto
ultimately show False using mult_strict_left_mono[OF y `u>0`] unfolding left_diff_distrib by auto
qed
lemma convex_distance: "convex_on s (\<lambda>x. dist a x)"
-proof(auto simp add: convex_on_def dist_def)
+proof(auto simp add: convex_on_def dist_norm)
fix x y assume "x\<in>s" "y\<in>s"
fix u v ::real assume "0 \<le> u" "0 \<le> v" "u + v = 1"
have "a = u *s a + v *s a" unfolding vector_sadd_rdistrib[THEN sym] and `u+v=1` by simp
@@ -782,7 +782,7 @@
proof- from assms obtain B where B:"\<forall>x\<in>s. norm x \<le> B" unfolding bounded_def by auto
show ?thesis apply(rule bounded_subset[OF bounded_cball, of _ 0 B])
unfolding subset_hull[unfolded mem_def, of convex, OF convex_cball]
- unfolding subset_eq mem_cball dist_def using B by auto qed
+ unfolding subset_eq mem_cball dist_norm using B by auto qed
lemma finite_imp_bounded_convex_hull:
"finite s \<Longrightarrow> bounded(convex hull s)"
@@ -1222,10 +1222,10 @@
show "0 < Min i" unfolding i_def and Min_gr_iff[OF finite_imageI[OF obt(1)] `b \` t\<noteq>{}`]
using b apply simp apply rule apply(erule_tac x=x in ballE) using `t\<subseteq>s` by auto
next fix y assume "y \<in> cball a (Min i)"
- hence y:"norm (a - y) \<le> Min i" unfolding dist_def[THEN sym] by auto
+ hence y:"norm (a - y) \<le> Min i" unfolding dist_norm[THEN sym] by auto
{ fix x assume "x\<in>t"
hence "Min i \<le> b x" unfolding i_def apply(rule_tac Min_le) using obt(1) by auto
- hence "x + (y - a) \<in> cball x (b x)" using y unfolding mem_cball dist_def by auto
+ hence "x + (y - a) \<in> cball x (b x)" using y unfolding mem_cball dist_norm by auto
moreover from `x\<in>t` have "x\<in>s" using obt(2) by auto
ultimately have "x + (y - a) \<in> s" using y and b[THEN bspec[where x=x]] unfolding subset_eq by auto }
moreover
@@ -1355,18 +1355,18 @@
proof(cases "a \<bullet> d - b \<bullet> d > 0")
case True hence "0 < d \<bullet> d + (a \<bullet> d * 2 - b \<bullet> d * 2)"
apply(rule_tac add_pos_pos) using assms by auto
- thus ?thesis apply(rule_tac disjI2) unfolding dist_def and real_vector_norm_def and real_sqrt_less_iff
+ thus ?thesis apply(rule_tac disjI2) unfolding dist_norm and real_vector_norm_def and real_sqrt_less_iff
by(simp add: dot_rsub dot_radd dot_lsub dot_ladd dot_sym field_simps)
next
case False hence "0 < d \<bullet> d + (b \<bullet> d * 2 - a \<bullet> d * 2)"
apply(rule_tac add_pos_nonneg) using assms by auto
- thus ?thesis apply(rule_tac disjI1) unfolding dist_def and real_vector_norm_def and real_sqrt_less_iff
+ thus ?thesis apply(rule_tac disjI1) unfolding dist_norm and real_vector_norm_def and real_sqrt_less_iff
by(simp add: dot_rsub dot_radd dot_lsub dot_ladd dot_sym field_simps)
qed
lemma norm_increases_online:
"(d::real^'n::finite) \<noteq> 0 \<Longrightarrow> norm(a + d) > norm a \<or> norm(a - d) > norm a"
- using dist_increases_online[of d a 0] unfolding dist_def by auto
+ using dist_increases_online[of d a 0] unfolding dist_norm by auto
lemma simplex_furthest_lt:
fixes s::"(real^'n::finite) set" assumes "finite s"
@@ -1402,7 +1402,7 @@
proof(erule_tac disjE)
assume "dist a y < dist a (y + w *s (x - b))"
hence "norm (y - a) < norm ((u + w) *s x + (v - w) *s b - a)"
- unfolding dist_commute[of a] unfolding dist_def obt(5) by (simp add: ring_simps)
+ unfolding dist_commute[of a] unfolding dist_norm obt(5) by (simp add: ring_simps)
moreover have "(u + w) *s x + (v - w) *s b \<in> convex hull insert x s"
unfolding convex_hull_insert[OF `s\<noteq>{}`] and mem_Collect_eq
apply(rule_tac x="u + w" in exI) apply rule defer
@@ -1411,7 +1411,7 @@
next
assume "dist a y < dist a (y - w *s (x - b))"
hence "norm (y - a) < norm ((u - w) *s x + (v + w) *s b - a)"
- unfolding dist_commute[of a] unfolding dist_def obt(5) by (simp add: ring_simps)
+ unfolding dist_commute[of a] unfolding dist_norm obt(5) by (simp add: ring_simps)
moreover have "(u - w) *s x + (v + w) *s b \<in> convex hull insert x s"
unfolding convex_hull_insert[OF `s\<noteq>{}`] and mem_Collect_eq
apply(rule_tac x="u - w" in exI) apply rule defer
@@ -1430,7 +1430,7 @@
have "convex hull s \<noteq> {}" using hull_subset[of s convex] and assms(2) by auto
then obtain x where x:"x\<in>convex hull s" "\<forall>y\<in>convex hull s. norm (y - a) \<le> norm (x - a)"
using distance_attains_sup[OF finite_imp_compact_convex_hull[OF assms(1)], of a]
- unfolding dist_commute[of a] unfolding dist_def by auto
+ unfolding dist_commute[of a] unfolding dist_norm by auto
thus ?thesis proof(cases "x\<in>s")
case False then obtain y where "y\<in>convex hull s" "norm (x - a) < norm (y - a)"
using simplex_furthest_lt[OF assms(1), THEN bspec[where x=x]] and x(1) by auto
@@ -1469,7 +1469,8 @@
subsection {* Closest point of a convex set is unique, with a continuous projection. *}
-definition
+definition
+ closest_point :: "(real ^ 'n::finite) set \<Rightarrow> real ^ 'n \<Rightarrow> real ^ 'n" where
"closest_point s a = (SOME x. x \<in> s \<and> (\<forall>y\<in>s. dist a x \<le> dist a y))"
lemma closest_point_exists:
@@ -1512,7 +1513,7 @@
proof- obtain u where "u>0" and u:"\<forall>v>0. v \<le> u \<longrightarrow> norm (v *s (z - x) - (y - x)) < norm (y - x)"
using closer_points_lemma[OF assms] by auto
show ?thesis apply(rule_tac x="min u 1" in exI) using u[THEN spec[where x="min u 1"]] and `u>0`
- unfolding dist_def by(auto simp add: norm_minus_commute field_simps) qed
+ unfolding dist_norm by(auto simp add: norm_minus_commute field_simps) qed
lemma any_closest_point_dot:
assumes "convex s" "closed s" "x \<in> s" "y \<in> s" "\<forall>z\<in>s. dist a x \<le> dist a z"
@@ -1555,7 +1556,7 @@
"(y - closest_point s y) \<bullet> (closest_point s x - closest_point s y) \<le> 0"
apply(rule_tac[!] any_closest_point_dot[OF assms(1-2)])
using closest_point_exists[OF assms(2-3)] by auto
- thus ?thesis unfolding dist_def and norm_le
+ thus ?thesis unfolding dist_norm and norm_le
using dot_pos_le[of "(x - closest_point s x) - (y - closest_point s y)"]
by (auto simp add: dot_sym dot_ladd dot_radd) qed
@@ -1686,9 +1687,9 @@
using hull_subset[of c convex] unfolding subset_eq and dot_rmult
apply- apply rule defer apply rule apply(rule mult_nonneg_nonneg)
by(auto simp add: dot_sym elim!: ballE)
- thus "frontier (cball 0 1) \<inter> \<Inter>f \<noteq> {}" unfolding c(1) frontier_cball dist_def by auto
+ thus "frontier (cball 0 1) \<inter> \<Inter>f \<noteq> {}" unfolding c(1) frontier_cball dist_norm by auto
qed(insert closed_halfspace_ge, auto)
- then obtain x where "norm x = 1" "\<forall>y\<in>s. x\<in>?k y" unfolding frontier_cball dist_def by auto
+ then obtain x where "norm x = 1" "\<forall>y\<in>s. x\<in>?k y" unfolding frontier_cball dist_norm by auto
thus ?thesis apply(rule_tac x=x in exI) by(auto simp add: dot_sym) qed
lemma separating_hyperplane_sets:
@@ -1719,7 +1720,7 @@
fix z assume "z \<in> ball ((1 - u) *s x + u *s y) (min d e)"
hence "(1- u) *s (z - u *s (y - x)) + u *s (z + (1 - u) *s (y - x)) \<in> s"
apply(rule_tac assms[unfolded convex_alt, rule_format])
- using ed(1,2) and u unfolding subset_eq mem_ball Ball_def dist_def by(auto simp add: ring_simps)
+ using ed(1,2) and u unfolding subset_eq mem_ball Ball_def dist_norm by(auto simp add: ring_simps)
thus "z \<in> s" using u by (auto simp add: ring_simps) qed(insert u ed(3-4), auto) qed
lemma convex_hull_eq_empty: "convex hull s = {} \<longleftrightarrow> s = {}"
@@ -1934,7 +1935,7 @@
fix e assume "0 < e" and as:"(u + e / 2 / norm x) *s x \<in> s"
hence "u + e / 2 / norm x > u" using`norm x > 0` by(auto simp del:zero_less_norm_iff intro!: divide_pos_pos)
thus False using u_max[OF _ as] by auto
- qed(insert `y\<in>s`, auto simp add: dist_def obt(3))
+ qed(insert `y\<in>s`, auto simp add: dist_norm obt(3))
thus ?thesis apply(rule_tac that[of u]) apply(rule obt(1), assumption)
apply(rule,rule,rule ccontr) apply(rule u_max) by auto qed
@@ -2004,7 +2005,7 @@
{ fix x assume as:"x \<in> cball (0::real^'n) 1"
have "norm x *s surf (pi x) \<in> s" proof(cases "x=0 \<or> norm x = 1")
- case False hence "pi x \<in> sphere" "norm x < 1" using pi(1)[of x] as by(auto simp add: dist_def)
+ case False hence "pi x \<in> sphere" "norm x < 1" using pi(1)[of x] as by(auto simp add: dist_norm)
thus ?thesis apply(rule_tac assms(3)[rule_format, THEN DiffD1])
apply(rule_tac fs[unfolded subset_eq, rule_format])
unfolding surf(5)[THEN sym] by auto
@@ -2027,7 +2028,7 @@
moreover have "pi x = pi ((inverse (norm (surf (pi x))) * norm x) *s surf (pi x))"
unfolding pi(2)[OF *] surf(4)[rule_format, OF pix] ..
moreover have "surf (pi x) \<in> frontier s" using surf(5) pix by auto
- hence "dist 0 (inverse (norm (surf (pi x))) *s x) \<le> 1" unfolding dist_def
+ hence "dist 0 (inverse (norm (surf (pi x))) *s x) \<le> 1" unfolding dist_norm
using ** and * using front_smul[THEN bspec[where x="surf (pi x)"], THEN spec[where x="norm x * ?a"]]
using False `x\<in>s` by(auto simp add:field_simps)
ultimately show ?thesis unfolding image_iff apply(rule_tac x="inverse (norm (surf(pi x))) *s x" in bexI)
@@ -2040,15 +2041,15 @@
prefer 4 apply(rule continuous_at_imp_continuous_on, rule) apply(rule_tac [3] hom2) proof-
fix x::"real^'n" assume as:"x \<in> cball 0 1"
thus "continuous (at x) (\<lambda>x. norm x *s surf (pi x))" proof(cases "x=0")
- case False thus ?thesis apply(rule_tac continuous_mul, rule_tac continuous_at_vec1_norm[THEN spec])
+ case False thus ?thesis apply(rule_tac continuous_mul, rule_tac continuous_at_vec1_norm)
using cont_surfpi unfolding continuous_on_eq_continuous_at[OF open_delete[OF open_UNIV]] o_def by auto
next guess a using UNIV_witness[where 'a = 'n] ..
obtain B where B:"\<forall>x\<in>s. norm x \<le> B" using compact_imp_bounded[OF assms(1)] unfolding bounded_def by auto
hence "B > 0" using assms(2) unfolding subset_eq apply(erule_tac x="basis a" in ballE) defer apply(erule_tac x="basis a" in ballE)
- unfolding Ball_def mem_cball dist_def by (auto simp add: norm_basis[unfolded One_nat_def])
+ unfolding Ball_def mem_cball dist_norm by (auto simp add: norm_basis[unfolded One_nat_def])
case True show ?thesis unfolding True continuous_at Lim_at apply(rule,rule) apply(rule_tac x="e / B" in exI)
apply(rule) apply(rule divide_pos_pos) prefer 3 apply(rule,rule,erule conjE)
- unfolding norm_0 vector_smult_lzero dist_def diff_0_right norm_mul abs_norm_cancel proof-
+ unfolding norm_0 vector_smult_lzero dist_norm diff_0_right norm_mul abs_norm_cancel proof-
fix e and x::"real^'n" assume as:"norm x < e / B" "0 < norm x" "0<e"
hence "surf (pi x) \<in> frontier s" using pi(1)[of x] unfolding surf(5)[THEN sym] by auto
hence "norm (surf (pi x)) \<le> B" using B fs by auto
@@ -2086,7 +2087,7 @@
unfolding centre_in_ball apply rule defer apply(rule) unfolding mem_ball proof-
fix y assume "dist (u *s x) y < 1 - u"
hence "inverse (1 - u) *s (y - u *s x) \<in> s"
- using assms(3) apply(erule_tac subsetD) unfolding mem_cball dist_commute dist_def
+ using assms(3) apply(erule_tac subsetD) unfolding mem_cball dist_commute dist_norm
unfolding group_add_class.diff_0 group_add_class.diff_0_right norm_minus_cancel norm_mul
apply (rule mult_left_le_imp_le[of "1 - u"])
unfolding class_semiring.mul_a using `u<1` by auto
@@ -2102,7 +2103,7 @@
let ?d = "inverse d" and ?n = "0::real^'n"
have "cball ?n 1 \<subseteq> (\<lambda>x. inverse d *s (x - a)) ` s"
apply(rule, rule_tac x="d *s x + a" in image_eqI) defer
- apply(rule d[unfolded subset_eq, rule_format]) using `d>0` unfolding mem_cball dist_def
+ apply(rule d[unfolded subset_eq, rule_format]) using `d>0` unfolding mem_cball dist_norm
by(auto simp add: mult_right_le_one_le)
hence "(\<lambda>x. inverse d *s (x - a)) ` s homeomorphic cball ?n 1"
using homeomorphic_convex_compact_lemma[of "(\<lambda>x. ?d *s -a + ?d *s x) ` s", OF convex_affinity compact_affinity]
@@ -2368,10 +2369,10 @@
show "\<bar>f y - f x\<bar> < e" proof(cases "y=x")
case False def t \<equiv> "k / norm (y - x)"
have "2 < t" "0<t" unfolding t_def using as False and `k>0` by(auto simp add:field_simps)
- have "y\<in>s" apply(rule k[unfolded subset_eq,rule_format]) unfolding mem_cball dist_def
+ have "y\<in>s" apply(rule k[unfolded subset_eq,rule_format]) unfolding mem_cball dist_norm
apply(rule order_trans[of _ "2 * norm (x - y)"]) using as by(auto simp add: field_simps norm_minus_commute)
{ def w \<equiv> "x + t *s (y - x)"
- have "w\<in>s" unfolding w_def apply(rule k[unfolded subset_eq,rule_format]) unfolding mem_cball dist_def
+ have "w\<in>s" unfolding w_def apply(rule k[unfolded subset_eq,rule_format]) unfolding mem_cball dist_norm
unfolding t_def using `k>0` by(auto simp add: norm_mul simp del: vector_ssub_ldistrib)
have "(1 / t) *s x + - x + ((t - 1) / t) *s x = (1 / t - 1 + (t - 1) / t) *s x" by auto
also have "\<dots> = 0" using `t>0` by(auto simp add:field_simps simp del:vector_sadd_rdistrib)
@@ -2384,7 +2385,7 @@
using `0<t` `2<t` and `x\<in>s` `w\<in>s` by(auto simp add:field_simps) }
moreover
{ def w \<equiv> "x - t *s (y - x)"
- have "w\<in>s" unfolding w_def apply(rule k[unfolded subset_eq,rule_format]) unfolding mem_cball dist_def
+ have "w\<in>s" unfolding w_def apply(rule k[unfolded subset_eq,rule_format]) unfolding mem_cball dist_norm
unfolding t_def using `k>0` by(auto simp add: norm_mul simp del: vector_ssub_ldistrib)
have "(1 / (1 + t)) *s x + (t / (1 + t)) *s x = (1 / (1 + t) + t / (1 + t)) *s x" by auto
also have "\<dots>=x" using `t>0` by (auto simp add:field_simps simp del:vector_sadd_rdistrib)
@@ -2409,7 +2410,7 @@
apply(rule) proof(cases "0 \<le> e") case True
fix y assume y:"y\<in>cball x e" def z \<equiv> "2 *s x - y"
have *:"x - (2 *s x - y) = y - x" by vector
- have z:"z\<in>cball x e" using y unfolding z_def mem_cball dist_def * by(auto simp add: norm_minus_commute)
+ have z:"z\<in>cball x e" using y unfolding z_def mem_cball dist_norm * by(auto simp add: norm_minus_commute)
have "(1 / 2) *s y + (1 / 2) *s z = x" unfolding z_def by auto
thus "\<bar>f y\<bar> \<le> b + 2 * \<bar>f x\<bar>" using assms(1)[unfolded convex_on_def,rule_format, OF y z, of "1/2" "1/2"]
using assms(2)[rule_format,OF y] assms(2)[rule_format,OF z] by(auto simp add:field_simps)
@@ -2438,7 +2439,7 @@
fix z assume z:"z\<in>{x - ?d..x + ?d}"
have e:"e = setsum (\<lambda>i. d) (UNIV::'n set)" unfolding setsum_constant d_def using dimge1
by (metis card_enum field_simps d_def not_one_le_zero of_nat_le_iff real_eq_of_nat real_of_nat_1)
- show "dist x z \<le> e" unfolding dist_def e apply(rule_tac order_trans[OF norm_le_l1], rule setsum_mono)
+ show "dist x z \<le> e" unfolding dist_norm e apply(rule_tac order_trans[OF norm_le_l1], rule setsum_mono)
using z[unfolded mem_interval] apply(erule_tac x=i in allE) by(auto simp add:field_simps vector_component_simps) qed
hence k:"\<forall>y\<in>{x - ?d..x + ?d}. f y \<le> k" unfolding c(2) apply(rule_tac convex_on_convex_hull_bound) apply assumption
unfolding k_def apply(rule, rule Max_ge) using c(1) by auto
@@ -2448,8 +2449,8 @@
hence "\<forall>y\<in>cball x d. abs (f y) \<le> k + 2 * abs (f x)" apply(rule_tac convex_bounds_lemma) apply assumption proof
fix y assume y:"y\<in>cball x d"
{ fix i::'n have "x $ i - d \<le> y $ i" "y $ i \<le> x $ i + d"
- using order_trans[OF component_le_norm y[unfolded mem_cball dist_def], of i] by(auto simp add: vector_component) }
- thus "f y \<le> k" apply(rule_tac k[rule_format]) unfolding mem_cball mem_interval dist_def
+ using order_trans[OF component_le_norm y[unfolded mem_cball dist_norm], of i] by(auto simp add: vector_component) }
+ thus "f y \<le> k" apply(rule_tac k[rule_format]) unfolding mem_cball mem_interval dist_norm
by(auto simp add: vector_component_simps) qed
hence "continuous_on (ball x d) (vec1 \<circ> f)" apply(rule_tac convex_on_bounded_continuous)
apply(rule open_ball, rule convex_on_subset[OF conv], rule ball_subset_cball) by auto
@@ -2484,10 +2485,10 @@
proof-
have *: "\<And>x y::real^'n::finite. 2 *s x = - y \<Longrightarrow> norm x = (norm y) / 2" unfolding equation_minus_iff by auto
have **:"\<And>x y::real^'n::finite. 2 *s x = y \<Longrightarrow> norm x = (norm y) / 2" by auto
- show ?t1 unfolding midpoint_def dist_def apply (rule **) by(auto,vector)
- show ?t2 unfolding midpoint_def dist_def apply (rule *) by(auto,vector)
- show ?t3 unfolding midpoint_def dist_def apply (rule *) by(auto,vector)
- show ?t4 unfolding midpoint_def dist_def apply (rule **) by(auto,vector) qed
+ show ?t1 unfolding midpoint_def dist_norm apply (rule **) by(auto,vector)
+ show ?t2 unfolding midpoint_def dist_norm apply (rule *) by(auto,vector)
+ show ?t3 unfolding midpoint_def dist_norm apply (rule *) by(auto,vector)
+ show ?t4 unfolding midpoint_def dist_norm apply (rule **) by(auto,vector) qed
lemma midpoint_eq_endpoint:
"midpoint a b = a \<longleftrightarrow> a = (b::real^'n::finite)"
@@ -2550,14 +2551,14 @@
unfolding norm_minus_commute[of x a] * norm_mul Cart_eq using as(2,3)
by(auto simp add: vector_component_simps field_simps)
next assume as:"dist a b = dist a x + dist x b"
- have "norm (a - x) / norm (a - b) \<le> 1" unfolding divide_le_eq_1_pos[OF Fal2] unfolding as[unfolded dist_def] norm_ge_zero by auto
+ have "norm (a - x) / norm (a - b) \<le> 1" unfolding divide_le_eq_1_pos[OF Fal2] unfolding as[unfolded dist_norm] norm_ge_zero by auto
thus "\<exists>u. x = (1 - u) *s a + u *s b \<and> 0 \<le> u \<and> u \<le> 1" apply(rule_tac x="dist a x / dist a b" in exI)
- unfolding dist_def Cart_eq apply- apply rule defer apply(rule, rule divide_nonneg_pos) prefer 4 proof rule
+ unfolding dist_norm Cart_eq apply- apply rule defer apply(rule, rule divide_nonneg_pos) prefer 4 proof rule
fix i::'n have "((1 - norm (a - x) / norm (a - b)) *s a + (norm (a - x) / norm (a - b)) *s b) $ i =
((norm (a - b) - norm (a - x)) * (a $ i) + norm (a - x) * (b $ i)) / norm (a - b)"
using Fal by(auto simp add:vector_component_simps field_simps)
also have "\<dots> = x$i" apply(rule divide_eq_imp[OF Fal])
- unfolding as[unfolded dist_def] using as[unfolded dist_triangle_eq Cart_eq,rule_format, of i]
+ unfolding as[unfolded dist_norm] using as[unfolded dist_triangle_eq Cart_eq,rule_format, of i]
by(auto simp add:field_simps vector_component_simps)
finally show "x $ i = ((1 - norm (a - x) / norm (a - b)) *s a + (norm (a - x) / norm (a - b)) *s b) $ i" by auto
qed(insert Fal2, auto) qed qed
@@ -2566,7 +2567,7 @@
"between (a,b) (midpoint a b)" (is ?t1)
"between (b,a) (midpoint a b)" (is ?t2)
proof- have *:"\<And>x y z. x = (1/2::real) *s z \<Longrightarrow> y = (1/2) *s z \<Longrightarrow> norm z = norm x + norm y" by auto
- show ?t1 ?t2 unfolding between midpoint_def dist_def apply(rule_tac[!] *)
+ show ?t1 ?t2 unfolding between midpoint_def dist_norm apply(rule_tac[!] *)
by(auto simp add:field_simps Cart_eq vector_component_simps) qed
lemma between_mem_convex_hull:
@@ -2584,10 +2585,10 @@
fix y assume as:"dist (x - e *s (x - c)) y < e * d"
have *:"y = (1 - (1 - e)) *s ((1 / e) *s y - ((1 - e) / e) *s x) + (1 - e) *s x" using `e>0` by auto
have "dist c ((1 / e) *s y - ((1 - e) / e) *s x) = abs(1/e) * norm (e *s c - y + (1 - e) *s x)"
- unfolding dist_def unfolding norm_mul[THEN sym] apply(rule norm_eqI) using `e>0`
+ unfolding dist_norm unfolding norm_mul[THEN sym] apply(rule norm_eqI) using `e>0`
by(auto simp add:vector_component_simps Cart_eq field_simps)
also have "\<dots> = abs(1/e) * norm (x - e *s (x - c) - y)" by(auto intro!:norm_eqI)
- also have "\<dots> < d" using as[unfolded dist_def] and `e>0`
+ also have "\<dots> < d" using as[unfolded dist_norm] and `e>0`
by(auto simp add:pos_divide_less_eq[OF `e>0`] real_mult_commute)
finally show "y \<in> s" apply(subst *) apply(rule assms(1)[unfolded convex_alt,rule_format])
apply(rule d[unfolded subset_eq,rule_format]) unfolding mem_ball using assms(3-5) by auto
@@ -2608,12 +2609,12 @@
using `e\<le>1` `e>0` `d>0` by(auto intro!:mult_pos_pos divide_pos_pos)
then obtain y where "y\<in>s" "y \<noteq> x" "dist y x < e * d / (1 - e)"
using x[unfolded islimpt_approachable,THEN spec[where x="e*d / (1 - e)"]] by auto
- thus ?thesis apply(rule_tac x=y in bexI) unfolding dist_def using pos_less_divide_eq[OF *] by auto qed qed
+ thus ?thesis apply(rule_tac x=y in bexI) unfolding dist_norm using pos_less_divide_eq[OF *] by auto qed qed
then obtain y where "y\<in>s" and y:"norm (y - x) * (1 - e) < e * d" by auto
def z \<equiv> "c + ((1 - e) / e) *s (x - y)"
have *:"x - e *s (x - c) = y - e *s (y - z)" unfolding z_def using `e>0` by auto
have "z\<in>interior s" apply(rule subset_interior[OF d,unfolded subset_eq,rule_format])
- unfolding interior_open[OF open_ball] mem_ball z_def dist_def using y and assms(4,5)
+ unfolding interior_open[OF open_ball] mem_ball z_def dist_norm using y and assms(4,5)
by(auto simp del:vector_ssub_ldistrib simp add:field_simps norm_minus_commute)
thus ?thesis unfolding * apply - apply(rule mem_interior_convex_shrink)
using assms(1,4-5) `y\<in>s` by auto qed
@@ -2656,10 +2657,10 @@
fix x::"real^'n" and e assume "0<e" and as:"\<forall>xa. dist x xa < e \<longrightarrow> (\<forall>x. 0 \<le> xa $ x) \<and> setsum (op $ xa) UNIV \<le> 1"
show "(\<forall>xa. 0 < x $ xa) \<and> setsum (op $ x) UNIV < 1" apply(rule,rule) proof-
fix i::'n show "0 < x $ i" using as[THEN spec[where x="x - (e / 2) *s basis i"]] and `e>0`
- unfolding dist_def by(auto simp add: norm_basis vector_component_simps basis_component elim:allE[where x=i])
+ unfolding dist_norm by(auto simp add: norm_basis vector_component_simps basis_component elim:allE[where x=i])
next guess a using UNIV_witness[where 'a='n] ..
have **:"dist x (x + (e / 2) *s basis a) < e" using `e>0` and norm_basis[of a]
- unfolding dist_def by(auto simp add: vector_component_simps basis_component intro!: mult_strict_left_mono_comm)
+ unfolding dist_norm by(auto simp add: vector_component_simps basis_component intro!: mult_strict_left_mono_comm)
have "\<And>i. (x + (e / 2) *s basis a) $ i = x$i + (if i = a then e/2 else 0)" by(auto simp add:vector_component_simps)
hence *:"setsum (op $ (x + (e / 2) *s basis a)) UNIV = setsum (\<lambda>i. x$i + (if a = i then e/2 else 0)) UNIV" by(rule_tac setsum_cong, auto)
have "setsum (op $ x) UNIV < setsum (op $ (x + (e / 2) *s basis a)) UNIV" unfolding * setsum_addf
@@ -2677,11 +2678,11 @@
fix y assume y:"dist x y < min (Min (op $ x ` UNIV)) ?d"
have "setsum (op $ y) UNIV \<le> setsum (\<lambda>i. x$i + ?d) UNIV" proof(rule setsum_mono)
fix i::'n have "abs (y$i - x$i) < ?d" apply(rule le_less_trans) using component_le_norm[of "y - x" i]
- using y[unfolded min_less_iff_conj dist_def, THEN conjunct2] by(auto simp add:vector_component_simps norm_minus_commute)
+ using y[unfolded min_less_iff_conj dist_norm, THEN conjunct2] by(auto simp add:vector_component_simps norm_minus_commute)
thus "y $ i \<le> x $ i + ?d" by auto qed
also have "\<dots> \<le> 1" unfolding setsum_addf setsum_constant card_enum real_eq_of_nat using dimindex_ge_1 by(auto simp add: Suc_le_eq)
finally show "(\<forall>i. 0 \<le> y $ i) \<and> setsum (op $ y) UNIV \<le> 1" apply- proof(rule,rule)
- fix i::'n have "norm (x - y) < x$i" using y[unfolded min_less_iff_conj dist_def, THEN conjunct1]
+ fix i::'n have "norm (x - y) < x$i" using y[unfolded min_less_iff_conj dist_norm, THEN conjunct1]
using Min_gr_iff[of "op $ x ` dimset x"] dimindex_ge_1 by auto
thus "0 \<le> y$i" using component_le_norm[of "x - y" i] and as(1)[rule_format, of i] by(auto simp add: vector_component_simps)
qed auto qed auto qed
@@ -3225,7 +3226,7 @@
unfolding image_iff apply(rule_tac x=x in bexI) unfolding mem_Collect_eq norm_mul by(auto intro!: ***)
have "continuous_on (UNIV - {0}) (vec1 \<circ> (\<lambda>x::real^'n. 1 / norm x))" unfolding o_def continuous_on_eq_continuous_within
apply(rule, rule continuous_at_within_inv[unfolded o_def inverse_eq_divide]) apply(rule continuous_at_within)
- apply(rule continuous_at_vec1_norm[unfolded o_def,THEN spec]) by auto
+ apply(rule continuous_at_vec1_norm[unfolded o_def]) by auto
thus ?thesis unfolding * ** using path_connected_punctured_universe[OF assms]
by(auto intro!: path_connected_continuous_image continuous_on_intros continuous_on_mul) qed
@@ -3234,4 +3235,4 @@
(** In continuous_at_vec1_norm : Use \<And> instead of \<forall>. **)
-end
\ No newline at end of file
+end
--- a/src/HOL/Library/Euclidean_Space.thy Thu May 28 14:36:21 2009 -0700
+++ b/src/HOL/Library/Euclidean_Space.thy Thu May 28 17:00:02 2009 -0700
@@ -509,6 +509,9 @@
definition vector_sgn_def:
"sgn (x::'a^'b) = scaleR (inverse (norm x)) x"
+definition dist_vector_def:
+ "dist (x::'a^'b) y = norm (x - y)"
+
instance proof
fix a :: real and x y :: "'a ^ 'b"
show "0 \<le> norm x"
@@ -527,6 +530,8 @@
by (simp add: norm_scaleR setL2_right_distrib)
show "sgn x = scaleR (inverse (norm x)) x"
by (rule vector_sgn_def)
+ show "dist x y = norm (x - y)"
+ by (rule dist_vector_def)
qed
end
@@ -621,7 +626,7 @@
by (simp add: norm_vector_1)
lemma dist_real: "dist(x::real ^ 1) y = abs((x$1) - (y$1))"
- by (auto simp add: norm_real dist_def)
+ by (auto simp add: norm_real dist_norm)
subsection {* A connectedness or intermediate value lemma with several applications. *}
@@ -953,37 +958,52 @@
text{* Hence more metric properties. *}
-lemma dist_triangle_alt: "dist y z <= dist x y + dist x z"
+lemma dist_triangle_alt:
+ fixes x y z :: "'a::metric_space"
+ shows "dist y z <= dist x y + dist x z"
using dist_triangle [of y z x] by (simp add: dist_commute)
-lemma dist_triangle2: "dist x y \<le> dist x z + dist y z"
-using dist_triangle [of x y z] by (simp add: dist_commute)
-
-lemma dist_pos_lt: "x \<noteq> y ==> 0 < dist x y" by (simp add: zero_less_dist_iff)
-lemma dist_nz: "x \<noteq> y \<longleftrightarrow> 0 < dist x y" by (simp add: zero_less_dist_iff)
-
-lemma dist_triangle_le: "dist x z + dist y z <= e \<Longrightarrow> dist x y <= e"
+lemma dist_pos_lt:
+ fixes x y :: "'a::metric_space"
+ shows "x \<noteq> y ==> 0 < dist x y"
+by (simp add: zero_less_dist_iff)
+
+lemma dist_nz:
+ fixes x y :: "'a::metric_space"
+ shows "x \<noteq> y \<longleftrightarrow> 0 < dist x y"
+by (simp add: zero_less_dist_iff)
+
+lemma dist_triangle_le:
+ fixes x y z :: "'a::metric_space"
+ shows "dist x z + dist y z <= e \<Longrightarrow> dist x y <= e"
by (rule order_trans [OF dist_triangle2])
-lemma dist_triangle_lt: "dist x z + dist y z < e ==> dist x y < e"
+lemma dist_triangle_lt:
+ fixes x y z :: "'a::metric_space"
+ shows "dist x z + dist y z < e ==> dist x y < e"
by (rule le_less_trans [OF dist_triangle2])
lemma dist_triangle_half_l:
- "dist x1 y < e / 2 \<Longrightarrow> dist x2 y < e / 2 \<Longrightarrow> dist x1 x2 < e"
+ fixes x1 x2 y :: "'a::metric_space"
+ shows "dist x1 y < e / 2 \<Longrightarrow> dist x2 y < e / 2 \<Longrightarrow> dist x1 x2 < e"
by (rule dist_triangle_lt [where z=y], simp)
lemma dist_triangle_half_r:
- "dist y x1 < e / 2 \<Longrightarrow> dist y x2 < e / 2 \<Longrightarrow> dist x1 x2 < e"
+ fixes x1 x2 y :: "'a::metric_space"
+ shows "dist y x1 < e / 2 \<Longrightarrow> dist y x2 < e / 2 \<Longrightarrow> dist x1 x2 < e"
by (rule dist_triangle_half_l, simp_all add: dist_commute)
-lemma dist_triangle_add: "dist (x + y) (x' + y') <= dist x x' + dist y y'"
-unfolding dist_def by (rule norm_diff_triangle_ineq)
+lemma dist_triangle_add:
+ fixes x y x' y' :: "'a::real_normed_vector"
+ shows "dist (x + y) (x' + y') <= dist x x' + dist y y'"
+unfolding dist_norm by (rule norm_diff_triangle_ineq)
lemma dist_mul[simp]: "dist (c *s x) (c *s y) = \<bar>c\<bar> * dist x y"
- unfolding dist_def vector_ssub_ldistrib[symmetric] norm_mul ..
+ unfolding dist_norm vector_ssub_ldistrib[symmetric] norm_mul ..
lemma dist_triangle_add_half:
- " dist x x' < e / 2 \<Longrightarrow> dist y y' < e / 2 \<Longrightarrow> dist(x + y) (x' + y') < e"
+ fixes x x' y y' :: "'a::real_normed_vector"
+ shows "dist x x' < e / 2 \<Longrightarrow> dist y y' < e / 2 \<Longrightarrow> dist(x + y) (x' + y') < e"
by (rule le_less_trans [OF dist_triangle_add], simp)
lemma setsum_component [simp]:
@@ -1222,7 +1242,7 @@
proof-
from vector_choose_size[OF e] obtain c:: "real ^'n" where "norm c = e"
by blast
- then have "dist x (x - c) = e" by (simp add: dist_def)
+ then have "dist x (x - c) = e" by (simp add: dist_norm)
then show ?thesis by blast
qed
@@ -2546,7 +2566,7 @@
qed
lemma dist_fstcart: "dist(fstcart (x::real^_)) (fstcart y) <= dist x y"
- by (metis dist_def fstcart_sub[symmetric] norm_fstcart)
+ by (metis dist_vector_def fstcart_sub[symmetric] norm_fstcart)
lemma norm_sndcart: "norm(sndcart x) <= norm (x::real ^('n::finite + 'm::finite))"
proof-
@@ -2561,7 +2581,7 @@
qed
lemma dist_sndcart: "dist(sndcart (x::real^_)) (sndcart y) <= dist x y"
- by (metis dist_def sndcart_sub[symmetric] norm_sndcart)
+ by (metis dist_vector_def sndcart_sub[symmetric] norm_sndcart)
lemma dot_pastecart: "(pastecart (x1::'a::{times,comm_monoid_add}^'n::finite) (x2::'a::{times,comm_monoid_add}^'m::finite)) \<bullet> (pastecart y1 y2) = x1 \<bullet> y1 + x2 \<bullet> y2"
by (simp add: dot_def setsum_UNIV_sum pastecart_def)
@@ -3901,7 +3921,7 @@
qed
lemma span_eq: "span S = span T \<longleftrightarrow> S \<subseteq> span T \<and> T \<subseteq> span S"
- by (metis set_eq_subset span_mono span_span span_inc)
+ by (metis set_eq_subset span_mono span_span span_inc) (* FIXME: slow *)
(* ------------------------------------------------------------------------- *)
(* Low-dimensional subset is in a hyperplane (weak orthogonal complement). *)
--- a/src/HOL/Library/Inner_Product.thy Thu May 28 14:36:21 2009 -0700
+++ b/src/HOL/Library/Inner_Product.thy Thu May 28 17:00:02 2009 -0700
@@ -10,7 +10,7 @@
subsection {* Real inner product spaces *}
-class real_inner = real_vector + sgn_div_norm +
+class real_inner = real_vector + sgn_div_norm + dist_norm +
fixes inner :: "'a \<Rightarrow> 'a \<Rightarrow> real"
assumes inner_commute: "inner x y = inner y x"
and inner_left_distrib: "inner (x + y) z = inner x z + inner y z"
--- a/src/HOL/Library/Topology_Euclidean_Space.thy Thu May 28 14:36:21 2009 -0700
+++ b/src/HOL/Library/Topology_Euclidean_Space.thy Thu May 28 17:00:02 2009 -0700
@@ -297,8 +297,8 @@
lemma mem_ball[simp]: "y \<in> ball x e \<longleftrightarrow> dist x y < e" by (simp add: ball_def)
lemma mem_cball[simp]: "y \<in> cball x e \<longleftrightarrow> dist x y \<le> e" by (simp add: cball_def)
-lemma mem_ball_0[simp]: "x \<in> ball 0 e \<longleftrightarrow> norm x < e" by (simp add: dist_def)
-lemma mem_cball_0[simp]: "x \<in> cball 0 e \<longleftrightarrow> norm x \<le> e" by (simp add: dist_def)
+lemma mem_ball_0[simp]: "x \<in> ball 0 e \<longleftrightarrow> norm x < e" by (simp add: dist_norm)
+lemma mem_cball_0[simp]: "x \<in> cball 0 e \<longleftrightarrow> norm x \<le> e" by (simp add: dist_norm)
lemma centre_in_cball[simp]: "x \<in> cball x e \<longleftrightarrow> 0\<le> e" by simp
lemma ball_subset_cball[simp,intro]: "ball x e \<subseteq> cball x e" by (simp add: subset_eq)
lemma subset_ball[intro]: "d <= e ==> ball x d \<subseteq> ball x e" by (simp add: subset_eq)
@@ -555,13 +555,15 @@
apply (simp only: vector_component)
by (rule th') auto
have th2: "\<bar>dist x x'\<bar> \<ge> \<bar>(x' - x)$i\<bar>" using component_le_norm[of "x'-x" i]
- apply (simp add: dist_def) by norm
+ apply (simp add: dist_norm) by norm
from th[OF th1 th2] x'(3) have False by (simp add: dist_commute) }
then show ?thesis unfolding closed_limpt islimpt_approachable
unfolding not_le[symmetric] by blast
qed
-lemma finite_set_avoid: assumes fS: "finite S" shows "\<exists>d>0. \<forall>x\<in>S. x \<noteq> a \<longrightarrow> d <= dist a x"
+lemma finite_set_avoid:
+ fixes a :: "real ^ 'n::finite"
+ assumes fS: "finite S" shows "\<exists>d>0. \<forall>x\<in>S. x \<noteq> a \<longrightarrow> d <= dist a x"
proof(induct rule: finite_induct[OF fS])
case 1 thus ?case apply auto by ferrack
next
@@ -602,7 +604,7 @@
from e2 y(2) have mp: "?m > 0" by (simp add: dist_nz[THEN sym])
from C[rule_format, OF mp] obtain z where z: "z \<in> S" "z\<noteq>x" "dist z x < ?m" by blast
have th: "norm (z - y) < e" using z y
- unfolding dist_def [symmetric]
+ unfolding dist_norm [symmetric]
by (intro dist_triangle_lt [where z=x], simp)
from d[rule_format, OF y(1) z(1) th] y z
have False by (auto simp add: dist_commute)}
@@ -1305,8 +1307,8 @@
then obtain y where y: "\<exists>x. netord net x y" "\<forall>x. netord net x y \<longrightarrow> dist (f x) l < e/b" by auto
{ fix x
have "netord net x y \<longrightarrow> dist (h (f x)) (h l) < e"
- using y(2) b unfolding dist_def using linear_sub[of h "f x" l] `linear h`
- apply auto by (metis b(1) b(2) dist_def dist_commute less_le_not_le linorder_not_le mult_imp_div_pos_le real_mult_commute xt1(7)) (* FIXME: VERY slow! *)
+ using y(2) b unfolding dist_norm using linear_sub[of h "f x" l] `linear h`
+ apply auto by (metis b(1) b(2) dist_vector_def dist_commute less_le_not_le linorder_not_le mult_imp_div_pos_le real_mult_commute xt1(7)) (* FIXME: VERY slow! *)
}
hence " (\<exists>y. (\<exists>x. netord net x y) \<and> (\<forall>x. netord net x y \<longrightarrow> dist (h (f x)) (h l) < e))" using y
by(rule_tac x="y" in exI) auto
@@ -1325,7 +1327,7 @@
done
lemma Lim_neg: "(f ---> l) net ==> ((\<lambda>x. -(f x)) ---> -l) net"
- apply (simp add: Lim dist_def group_simps)
+ apply (simp add: Lim dist_norm group_simps)
apply (subst minus_diff_eq[symmetric])
unfolding norm_minus_cancel by simp
@@ -1362,9 +1364,9 @@
unfolding diff_minus
by (simp add: Lim_add Lim_neg)
-lemma Lim_null: "(f ---> l) net \<longleftrightarrow> ((\<lambda>x. f(x) - l) ---> 0) net" by (simp add: Lim dist_def)
+lemma Lim_null: "(f ---> l) net \<longleftrightarrow> ((\<lambda>x. f(x) - l) ---> 0) net" by (simp add: Lim dist_norm)
lemma Lim_null_norm: "(f ---> 0) net \<longleftrightarrow> ((\<lambda>x. vec1(norm(f x))) ---> 0) net"
- by (simp add: Lim dist_def norm_vec1)
+ by (simp add: Lim dist_norm norm_vec1)
lemma Lim_null_comparison:
assumes "eventually (\<lambda>x. norm(f x) <= g x) net" "((\<lambda>x. vec1(g x)) ---> 0) net"
@@ -1374,7 +1376,7 @@
{ fix x
assume "norm (f x) \<le> g x" "dist (vec1 (g x)) 0 < e"
hence "dist (f x) 0 < e" unfolding vec_def using dist_vec1[of "g x" "0"]
- by (vector dist_def norm_vec1 real_vector_norm_def dot_def vec1_def)
+ by (vector dist_norm norm_vec1 real_vector_norm_def dot_def vec1_def)
}
thus "eventually (\<lambda>x. dist (f x) 0 < e) net"
using eventually_and[of "\<lambda>x. norm(f x) <= g x" "\<lambda>x. dist (vec1 (g x)) 0 < e" net]
@@ -1384,7 +1386,7 @@
lemma Lim_component: "(f ---> l) net
==> ((\<lambda>a. vec1((f a :: real ^'n::finite)$i)) ---> vec1(l$i)) net"
- apply (simp add: Lim dist_def vec1_sub[symmetric] norm_vec1 vector_minus_component[symmetric] del: vector_minus_component)
+ apply (simp add: Lim dist_norm vec1_sub[symmetric] norm_vec1 vector_minus_component[symmetric] del: vector_minus_component)
apply (auto simp del: vector_minus_component)
apply (erule_tac x=e in allE)
apply clarify
@@ -1475,7 +1477,7 @@
{ assume "norm (l - l') > 0"
hence "norm (l - l') = 0" using *[of "(norm (l - l')) /2"] using norm_ge_zero[of "l - l'"] by simp
}
- hence "l = l'" using norm_ge_zero[of "l - l'"] unfolding le_less and dist_nz[of l l', unfolded dist_def, THEN sym] by auto
+ hence "l = l'" using norm_ge_zero[of "l - l'"] unfolding le_less and dist_nz[of l l', unfolded dist_norm, THEN sym] by auto
thus ?thesis using assms using Lim_sub[of f l net f l'] by simp
qed
@@ -1534,12 +1536,12 @@
{ fix x assume "dist (f x) l < d \<and> dist (g x) m < d"
hence **:"norm (f x) * norm (g x - m) + norm (f x - l) * norm m < e / B"
- using d[THEN spec[where x="f x"], THEN spec[where x="g x"]] unfolding dist_def by auto
+ using d[THEN spec[where x="f x"], THEN spec[where x="g x"]] unfolding dist_norm by auto
have "norm (h (f x) (g x - m)) + norm (h (f x - l) m) \<le> B * norm (f x) * norm (g x - m) + B * norm (f x - l) * norm m"
using B[THEN spec[where x="f x"], THEN spec[where x="g x - m"]]
using B[THEN spec[where x="f x - l"], THEN spec[where x="m"]] by auto
also have "\<dots> < e" using ** and `B>0` by(auto simp add: field_simps)
- finally have "dist (h (f x) (g x)) (h l m) < e" unfolding dist_def and * using norm_triangle_lt by auto
+ finally have "dist (h (f x) (g x)) (h l m) < e" unfolding dist_norm and * using norm_triangle_lt by auto
}
moreover
obtain c where "(\<exists>x. netord net x c) \<and> (\<forall>x. netord net x c \<longrightarrow> dist (f x) l < d \<and> dist (g x) m < d)"
@@ -1561,7 +1563,7 @@
with `?lhs` obtain d where d:"d>0" "\<forall>x. 0 < dist x a \<and> dist x a < d \<longrightarrow> dist (f x) l < e" unfolding Lim_at by auto
{ fix x::"real^'a" assume "0 < dist x 0 \<and> dist x 0 < d"
hence "dist (f (a + x)) l < e" using d
- apply(erule_tac x="x+a" in allE) by(auto simp add: comm_monoid_add.mult_commute dist_def dist_commute)
+ apply(erule_tac x="x+a" in allE) by(auto simp add: comm_monoid_add.mult_commute dist_norm dist_commute)
}
hence "\<exists>d>0. \<forall>x. 0 < dist x 0 \<and> dist x 0 < d \<longrightarrow> dist (f (a + x)) l < e" using d(1) by auto
}
@@ -1573,7 +1575,7 @@
unfolding Lim_at by auto
{ fix x::"real^'a" assume "0 < dist x a \<and> dist x a < d"
hence "dist (f x) l < e" using d apply(erule_tac x="x-a" in allE)
- by(auto simp add: comm_monoid_add.mult_commute dist_def dist_commute)
+ by(auto simp add: comm_monoid_add.mult_commute dist_norm dist_commute)
}
hence "\<exists>d>0. \<forall>x. 0 < dist x a \<and> dist x a < d \<longrightarrow> dist (f x) l < e" using d(1) by auto
}
@@ -1730,7 +1732,7 @@
using real_arch_inv[of e] apply auto apply(rule_tac x=n in exI)
by (metis dlo_simps(4) le_imp_inverse_le linorder_not_less real_of_nat_gt_zero_cancel_iff real_of_nat_less_iff xt1(7))
}
- thus ?thesis unfolding Lim_sequentially dist_def apply simp unfolding norm_vec1 by auto
+ thus ?thesis unfolding Lim_sequentially dist_norm apply simp unfolding norm_vec1 by auto
qed
text{* More properties of closed balls. *}
@@ -1739,9 +1741,9 @@
proof-
{ fix xa::"nat\<Rightarrow>real^'a" and l assume as: "\<forall>n. dist x (xa n) \<le> e" "(xa ---> l) sequentially"
from as(2) have "((\<lambda>n. x - xa n) ---> x - l) sequentially" using Lim_sub[of "\<lambda>n. x" x sequentially xa l] Lim_const[of x sequentially] by auto
- moreover from as(1) have "eventually (\<lambda>n. norm (x - xa n) \<le> e) sequentially" unfolding eventually_sequentially dist_def by auto
+ moreover from as(1) have "eventually (\<lambda>n. norm (x - xa n) \<le> e) sequentially" unfolding eventually_sequentially dist_norm by auto
ultimately have "dist x l \<le> e"
- unfolding dist_def
+ unfolding dist_norm
using Lim_norm_ubound[of sequentially _ "x - l" e] using trivial_limit_sequentially by auto
}
thus ?thesis unfolding closed_sequential_limits by auto
@@ -1790,15 +1792,15 @@
have "dist x (y - (d / (2 * dist y x)) *s (y - x))
= norm (x - y + (d / (2 * norm (y - x))) *s (y - x))"
- unfolding mem_cball mem_ball dist_def diff_diff_eq2 diff_add_eq[THEN sym] by auto
+ unfolding mem_cball mem_ball dist_norm diff_diff_eq2 diff_add_eq[THEN sym] by auto
also have "\<dots> = \<bar>- 1 + d / (2 * norm (x - y))\<bar> * norm (x - y)"
using vector_sadd_rdistrib[of "- 1" "d / (2 * norm (y - x))", THEN sym, of "y - x"]
unfolding vector_smult_lneg vector_smult_lid
- by (auto simp add: dist_commute[unfolded dist_def] norm_mul)
+ by (auto simp add: norm_minus_commute)
also have "\<dots> = \<bar>- norm (x - y) + d / 2\<bar>"
unfolding abs_mult_pos[of "norm (x - y)", OF norm_ge_zero[of "x - y"]]
- unfolding real_add_mult_distrib using `x\<noteq>y`[unfolded dist_nz, unfolded dist_def] by auto
- also have "\<dots> \<le> e - d/2" using `d \<le> dist x y` and `d>0` and `?rhs` by(auto simp add: dist_def)
+ unfolding real_add_mult_distrib using `x\<noteq>y`[unfolded dist_nz, unfolded dist_norm] by auto
+ also have "\<dots> \<le> e - d/2" using `d \<le> dist x y` and `d>0` and `?rhs` by(auto simp add: dist_norm)
finally have "y - (d / (2 * dist y x)) *s (y - x) \<in> ball x e" using `d>0` by auto
moreover
@@ -1806,9 +1808,9 @@
have "(d / (2*dist y x)) *s (y - x) \<noteq> 0"
using `x\<noteq>y`[unfolded dist_nz] `d>0` unfolding vector_mul_eq_0 by (auto simp add: dist_commute)
moreover
- have "dist (y - (d / (2 * dist y x)) *s (y - x)) y < d" unfolding dist_def apply simp unfolding norm_minus_cancel norm_mul
+ have "dist (y - (d / (2 * dist y x)) *s (y - x)) y < d" unfolding dist_norm apply simp unfolding norm_minus_cancel norm_mul
using `d>0` `x\<noteq>y`[unfolded dist_nz] dist_commute[of x y]
- unfolding dist_def by auto
+ unfolding dist_norm by auto
ultimately show "\<exists>x'\<in>ball x e. x' \<noteq> y \<and> dist x' y < d" by (rule_tac x="y - (d / (2*dist y x)) *s (y - x)" in bexI) auto
qed
next
@@ -1858,7 +1860,7 @@
thus "y \<in> ball x e" using `x = y ` by simp
next
case False
- have "dist (y + (d / 2 / dist y x) *s (y - x)) y < d" unfolding dist_def
+ have "dist (y + (d / 2 / dist y x) *s (y - x)) y < d" unfolding dist_norm
using `d>0` norm_ge_zero[of "y - x"] `x \<noteq> y` by auto
hence *:"y + (d / 2 / dist y x) *s (y - x) \<in> cball x e" using d as(1)[unfolded subset_eq] by blast
have "y - x \<noteq> 0" using `x \<noteq> y` by auto
@@ -1866,11 +1868,11 @@
using `d>0` divide_pos_pos[of d "2*norm (y - x)"] by auto
have "dist (y + (d / 2 / dist y x) *s (y - x)) x = norm (y + (d / (2 * norm (y - x))) *s y - (d / (2 * norm (y - x))) *s x - x)"
- by (auto simp add: dist_def vector_ssub_ldistrib add_diff_eq)
+ by (auto simp add: dist_norm vector_ssub_ldistrib add_diff_eq)
also have "\<dots> = norm ((1 + d / (2 * norm (y - x))) *s (y - x))"
by (auto simp add: vector_sadd_rdistrib vector_smult_lid ring_simps vector_sadd_rdistrib vector_ssub_ldistrib)
also have "\<dots> = \<bar>1 + d / (2 * norm (y - x))\<bar> * norm (y - x)" using ** by auto
- also have "\<dots> = (dist y x) + d/2"using ** by (auto simp add: left_distrib dist_def)
+ also have "\<dots> = (dist y x) + d/2"using ** by (auto simp add: left_distrib dist_norm)
finally have "e \<ge> dist x y +d/2" using *[unfolded mem_cball] by (auto simp add: dist_commute)
thus "y \<in> ball x e" unfolding mem_ball using `d>0` by auto
qed }
@@ -2257,7 +2259,7 @@
< (\<Sum>i \<in> ?d. e / real_of_nat (card ?d))"
using setsum_strict_mono[of "?d" "\<lambda>i. \<bar>((f \<circ> r) n - l) $ i\<bar>" "\<lambda>i. e / (real_of_nat (card ?d))"] by auto
hence "(\<Sum>i \<in> ?d. \<bar>((f \<circ> r) n - l) $ i\<bar>) < e" unfolding setsum_constant by auto
- hence "dist ((f \<circ> r) n) l < e" unfolding dist_def using norm_le_l1[of "(f \<circ> r) n - l"] by auto }
+ hence "dist ((f \<circ> r) n) l < e" unfolding dist_norm using norm_le_l1[of "(f \<circ> r) n - l"] by auto }
hence "\<exists>N. \<forall>n\<ge>N. dist ((f \<circ> r) n) l < e" by auto }
hence *:"((f \<circ> r) ---> l) sequentially" unfolding Lim_sequentially by auto
moreover have "l\<in>s"
@@ -2316,8 +2318,8 @@
from assms obtain N::nat where "\<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (s m) (s n) < 1" unfolding cauchy_def apply(erule_tac x= 1 in allE) by auto
hence N:"\<forall>n. N \<le> n \<longrightarrow> dist (s N) (s n) < 1" by auto
{ fix n::nat assume "n\<ge>N"
- hence "norm (s n) \<le> norm (s N) + 1" using N apply(erule_tac x=n in allE) unfolding dist_def
- using norm_triangle_sub[of "s N" "s n"] by (auto, metis dist_def dist_commute le_add_right_mono norm_triangle_sub real_less_def)
+ hence "norm (s n) \<le> norm (s N) + 1" using N apply(erule_tac x=n in allE) unfolding dist_norm
+ using norm_triangle_sub[of "s N" "s n"] by (auto, metis dist_vector_def dist_commute le_add_right_mono norm_triangle_sub real_less_def)
}
hence "\<forall>n\<ge>N. norm (s n) \<le> norm (s N) + 1" by auto
moreover
@@ -2553,11 +2555,11 @@
proof(cases "m<n")
case True
hence "1 < norm (x n) - norm (x m)" using *[of m n] by auto
- thus ?thesis unfolding dist_commute[of "x m" "x n"] unfolding dist_def using norm_triangle_sub[of "x n" "x m"] by auto
+ thus ?thesis unfolding dist_commute[of "x m" "x n"] unfolding dist_norm using norm_triangle_sub[of "x n" "x m"] by auto
next
case False hence "n<m" using `m\<noteq>n` by auto
hence "1 < norm (x m) - norm (x n)" using *[of n m] by auto
- thus ?thesis unfolding dist_commute[of "x n" "x m"] unfolding dist_def using norm_triangle_sub[of "x m" "x n"] by auto
+ thus ?thesis unfolding dist_commute[of "x n" "x m"] unfolding dist_norm using norm_triangle_sub[of "x m" "x n"] by auto
qed } note ** = this
{ fix a b assume "x a = x b" "a \<noteq> b"
hence False using **[of a b] by auto }
@@ -3128,13 +3130,13 @@
{ fix e::real assume "e>0"
then obtain d where "d>0" and d:"\<forall>x\<in>s. \<forall>x'\<in>s. dist x' x < d \<longrightarrow> dist (f x') (f x) < e"
using `?lhs`[unfolded uniformly_continuous_on_def, THEN spec[where x=e]] by auto
- obtain N where N:"\<forall>n\<ge>N. norm (x n - y n - 0) < d" using xy[unfolded Lim_sequentially dist_def] and `d>0` by auto
+ obtain N where N:"\<forall>n\<ge>N. norm (x n - y n - 0) < d" using xy[unfolded Lim_sequentially dist_norm] and `d>0` by auto
{ fix n assume "n\<ge>N"
hence "norm (f (x n) - f (y n) - 0) < e"
using N[THEN spec[where x=n]] using d[THEN bspec[where x="x n"], THEN bspec[where x="y n"]] using x and y
- unfolding dist_commute and dist_def by simp }
+ unfolding dist_commute and dist_norm by simp }
hence "\<exists>N. \<forall>n\<ge>N. norm (f (x n) - f (y n) - 0) < e" by auto }
- hence "((\<lambda>n. f(x n) - f(y n)) ---> 0) sequentially" unfolding Lim_sequentially and dist_def by auto }
+ hence "((\<lambda>n. f(x n) - f(y n)) ---> 0) sequentially" unfolding Lim_sequentially and dist_norm by auto }
thus ?rhs by auto
next
assume ?rhs
@@ -3147,7 +3149,7 @@
def y \<equiv> "\<lambda>n::nat. snd (fa (inverse (real n + 1)))"
have xyn:"\<forall>n. x n \<in> s \<and> y n \<in> s" and xy0:"\<forall>n. dist (x n) (y n) < inverse (real n + 1)" and fxy:"\<forall>n. \<not> dist (f (x n)) (f (y n)) < e"
unfolding x_def and y_def using fa by auto
- have *:"\<And>x y. dist (x - y) 0 = dist x y" unfolding dist_def by auto
+ have *:"\<And>x (y::real^_). dist (x - y) 0 = dist x y" unfolding dist_norm by auto
{ fix e::real assume "e>0"
then obtain N::nat where "N \<noteq> 0" and N:"0 < inverse (real N) \<and> inverse (real N) < e" unfolding real_arch_inv[of e] by auto
{ fix n::nat assume "n\<ge>N"
@@ -3517,7 +3519,7 @@
have *:"f ` s \<subseteq> cball 0 b" using assms(2)[unfolded mem_cball_0[THEN sym]] by auto
show ?thesis
using image_closure_subset[OF assms(1) closed_cball[of 0 b] *] assms(3)
- unfolding subset_eq apply(erule_tac x="f x" in ballE) by (auto simp add: dist_def)
+ unfolding subset_eq apply(erule_tac x="f x" in ballE) by (auto simp add: dist_norm)
qed
text{* Making a continuous function avoid some value in a neighbourhood. *}
@@ -3580,10 +3582,10 @@
have "e * abs c > 0" using assms(1)[unfolded zero_less_abs_iff[THEN sym]] using real_mult_order[OF `e>0`] by auto
moreover
{ fix y assume "dist y (c *s x) < e * \<bar>c\<bar>"
- hence "norm ((1 / c) *s y - x) < e" unfolding dist_def
+ hence "norm ((1 / c) *s y - x) < e" unfolding dist_norm
using norm_mul[of c "(1 / c) *s y - x", unfolded vector_ssub_ldistrib, unfolded vector_smult_assoc] assms(1)
assms(1)[unfolded zero_less_abs_iff[THEN sym]] by (simp del:zero_less_abs_iff)
- hence "y \<in> op *s c ` s" using rev_image_eqI[of "(1 / c) *s y" s y "op *s c"] e[THEN spec[where x="(1 / c) *s y"]] assms(1) unfolding dist_def vector_smult_assoc by auto }
+ hence "y \<in> op *s c ` s" using rev_image_eqI[of "(1 / c) *s y" s y "op *s c"] e[THEN spec[where x="(1 / c) *s y"]] assms(1) unfolding dist_norm vector_smult_assoc by auto }
ultimately have "\<exists>e>0. \<forall>x'. dist x' (c *s x) < e \<longrightarrow> x' \<in> op *s c ` s" apply(rule_tac x="e * abs c" in exI) by auto }
thus ?thesis unfolding open_def by auto
qed
@@ -3612,14 +3614,14 @@
proof (rule set_ext, rule)
fix x assume "x \<in> interior (op + a ` s)"
then obtain e where "e>0" and e:"ball x e \<subseteq> op + a ` s" unfolding mem_interior by auto
- hence "ball (x - a) e \<subseteq> s" unfolding subset_eq Ball_def mem_ball dist_def apply auto apply(erule_tac x="a + xa" in allE) unfolding ab_group_add_class.diff_diff_eq[THEN sym] by auto
+ hence "ball (x - a) e \<subseteq> s" unfolding subset_eq Ball_def mem_ball dist_norm apply auto apply(erule_tac x="a + xa" in allE) unfolding ab_group_add_class.diff_diff_eq[THEN sym] by auto
thus "x \<in> op + a ` interior s" unfolding image_iff apply(rule_tac x="x - a" in bexI) unfolding mem_interior using `e > 0` by auto
next
fix x assume "x \<in> op + a ` interior s"
then obtain y e where "e>0" and e:"ball y e \<subseteq> s" and y:"x = a + y" unfolding image_iff Bex_def mem_interior by auto
{ fix z have *:"a + y - z = y + a - z" by auto
assume "z\<in>ball x e"
- hence "z - a \<in> s" using e[unfolded subset_eq, THEN bspec[where x="z - a"]] unfolding mem_ball dist_def y ab_group_add_class.diff_diff_eq2 * by auto
+ hence "z - a \<in> s" using e[unfolded subset_eq, THEN bspec[where x="z - a"]] unfolding mem_ball dist_norm y ab_group_add_class.diff_diff_eq2 * by auto
hence "z \<in> op + a ` s" unfolding image_iff by(auto intro!: bexI[where x="z - a"]) }
hence "ball x e \<subseteq> op + a ` s" unfolding subset_eq by auto
thus "x \<in> interior (op + a ` s)" unfolding mem_interior using `e>0` by auto
@@ -3732,8 +3734,8 @@
{ fix y assume "y\<in>s" "dist y x < d"
hence "dist (f n y) (f n x) < e / 3" using d[THEN bspec[where x=y]] by auto
hence "norm (f n y - g x) < 2 * e / 3" using norm_triangle_lt[of "f n y - f n x" "f n x - g x" "2*e/3"]
- using n(1)[THEN bspec[where x=x], OF `x\<in>s`] unfolding dist_def unfolding ab_group_add_class.ab_diff_minus by auto
- hence "dist (g y) (g x) < e" unfolding dist_def using n(1)[THEN bspec[where x=y], OF `y\<in>s`]
+ using n(1)[THEN bspec[where x=x], OF `x\<in>s`] unfolding dist_norm unfolding ab_group_add_class.ab_diff_minus by auto
+ hence "dist (g y) (g x) < e" unfolding dist_norm using n(1)[THEN bspec[where x=y], OF `y\<in>s`]
unfolding norm_minus_cancel[of "f n y - g y", THEN sym] using norm_triangle_lt[of "f n y - g x" "g y - f n y" e] by (auto simp add: uminus_add_conv_diff) }
hence "\<exists>d>0. \<forall>x'\<in>s. dist x' x < d \<longrightarrow> dist (g x') (g x) < e" using `d>0` by auto }
thus ?thesis unfolding continuous_on_def by auto
@@ -3750,7 +3752,7 @@
hence "B * norm x < e" using `B>0` using mult_strict_right_mono[of "norm x" " e / B" B] unfolding real_mult_commute by auto
hence "norm (f x) < e" using B[THEN spec[where x=x]] `B>0` using order_le_less_trans[of "norm (f x)" "B * norm x" e] by auto }
moreover have "e / B > 0" using `e>0` `B>0` divide_pos_pos by auto
- ultimately have "\<exists>d>0. \<forall>x. 0 < dist x 0 \<and> dist x 0 < d \<longrightarrow> dist (f x) 0 < e" unfolding dist_def by auto }
+ ultimately have "\<exists>d>0. \<forall>x. 0 < dist x 0 \<and> dist x 0 < d \<longrightarrow> dist (f x) 0 < e" unfolding dist_norm by auto }
thus ?thesis unfolding Lim_at by auto
qed
@@ -3808,13 +3810,13 @@
lemma continuous_at_vec1_range:
"continuous (at x) (vec1 o f) \<longleftrightarrow> (\<forall>e>0. \<exists>d>0.
\<forall>x'. norm(x' - x) < d --> abs(f x' - f x) < e)"
- unfolding continuous_at unfolding Lim_at apply simp unfolding dist_vec1 unfolding dist_nz[THEN sym] unfolding dist_def apply auto
+ unfolding continuous_at unfolding Lim_at apply simp unfolding dist_vec1 unfolding dist_nz[THEN sym] unfolding dist_norm apply auto
apply(erule_tac x=e in allE) apply auto apply (rule_tac x=d in exI) apply auto apply (erule_tac x=x' in allE) apply auto
apply(erule_tac x=e in allE) by auto
lemma continuous_on_vec1_range:
" continuous_on s (vec1 o f) \<longleftrightarrow> (\<forall>x \<in> s. \<forall>e>0. \<exists>d>0. (\<forall>x' \<in> s. norm(x' - x) < d --> abs(f x' - f x) < e))"
- unfolding continuous_on_def apply (simp del: dist_commute) unfolding dist_vec1 unfolding dist_def ..
+ unfolding continuous_on_def apply (simp del: dist_commute) unfolding dist_vec1 unfolding dist_norm ..
lemma continuous_at_vec1_norm:
"continuous (at x) (vec1 o norm)"
@@ -3828,7 +3830,7 @@
shows "continuous (at (a::real^'a::finite)) (\<lambda> x. vec1(x$i))"
proof-
{ fix e::real and x assume "0 < dist x a" "dist x a < e" "e>0"
- hence "\<bar>x $ i - a $ i\<bar> < e" using component_le_norm[of "x - a" i] unfolding dist_def by auto }
+ hence "\<bar>x $ i - a $ i\<bar> < e" using component_le_norm[of "x - a" i] unfolding dist_norm by auto }
thus ?thesis unfolding continuous_at tendsto_def eventually_at dist_vec1 by auto
qed
@@ -3837,12 +3839,12 @@
proof-
{ fix e::real and x xa assume "x\<in>s" "e>0" "xa\<in>s" "0 < norm (xa - x) \<and> norm (xa - x) < e"
hence "\<bar>xa $ i - x $ i\<bar> < e" using component_le_norm[of "xa - x" i] by auto }
- thus ?thesis unfolding continuous_on Lim_within dist_vec1 unfolding dist_def by auto
+ thus ?thesis unfolding continuous_on Lim_within dist_vec1 unfolding dist_norm by auto
qed
lemma continuous_at_vec1_infnorm:
"continuous (at x) (vec1 o infnorm)"
- unfolding continuous_at Lim_at o_def unfolding dist_vec1 unfolding dist_def
+ unfolding continuous_at Lim_at o_def unfolding dist_vec1 unfolding dist_norm
apply auto apply (rule_tac x=e in exI) apply auto
using order_trans[OF real_abs_sub_infnorm infnorm_le_norm, of _ x] by (metis xt1(7))
@@ -3898,7 +3900,7 @@
{ fix x' assume "x'\<in>s" and as:"norm (x' - x) < e"
hence "\<bar>norm (x' - a) - norm (x - a)\<bar> < e"
using real_abs_sub_norm[of "x' - a" "x - a"] by auto }
- hence "\<exists>d>0. \<forall>x'\<in>s. norm (x' - x) < d \<longrightarrow> \<bar>dist x' a - dist x a\<bar> < e" using `e>0` unfolding dist_def by auto }
+ hence "\<exists>d>0. \<forall>x'\<in>s. norm (x' - x) < d \<longrightarrow> \<bar>dist x' a - dist x a\<bar> < e" using `e>0` unfolding dist_norm by auto }
thus ?thesis using assms
using continuous_attains_sup[of s "\<lambda>x. dist a x"]
unfolding continuous_on_vec1_range by (auto simp add: dist_commute)
@@ -3920,7 +3922,7 @@
{ fix x' assume "x'\<in>?B" and as:"norm (x' - x) < e"
hence "\<bar>norm (x' - a) - norm (x - a)\<bar> < e"
using real_abs_sub_norm[of "x' - a" "x - a"] by auto }
- hence "\<exists>d>0. \<forall>x'\<in>?B. norm (x' - x) < d \<longrightarrow> \<bar>dist x' a - dist x a\<bar> < e" using `e>0` unfolding dist_def by auto }
+ hence "\<exists>d>0. \<forall>x'\<in>?B. norm (x' - x) < d \<longrightarrow> \<bar>dist x' a - dist x a\<bar> < e" using `e>0` unfolding dist_norm by auto }
hence "continuous_on (cball a (dist b a) \<inter> s) (vec1 \<circ> dist a)" unfolding continuous_on_vec1_range
by (auto simp add: dist_commute)
moreover have "compact ?B" using compact_cball[of a "dist b a"] unfolding compact_eq_bounded_closed using bounded_Int and closed_Int and assms(1) by auto
@@ -4120,7 +4122,7 @@
have "{x - y | x y . x\<in>s \<and> y\<in>s} \<noteq> {}" using `s \<noteq> {}` by auto
then obtain x where x:"x\<in>{x - y |x y. x \<in> s \<and> y \<in> s}" "\<forall>y\<in>{x - y |x y. x \<in> s \<and> y \<in> s}. norm y \<le> norm x"
using compact_differences[OF assms(1) assms(1)]
- using distance_attains_sup[unfolded dist_def, of "{x - y | x y . x\<in>s \<and> y\<in>s}" 0] by(auto simp add: norm_minus_cancel)
+ using distance_attains_sup[unfolded dist_norm, of "{x - y | x y . x\<in>s \<and> y\<in>s}" 0] by(auto simp add: norm_minus_cancel)
from x(1) obtain a b where "a\<in>s" "b\<in>s" "x = a - b" by auto
thus ?thesis using x(2)[unfolded `x = a - b`] by blast
qed
@@ -4193,7 +4195,7 @@
{ fix e::real assume "e>0"
hence "0 < e *\<bar>c\<bar>" using `c\<noteq>0` mult_pos_pos[of e "abs c"] by auto
then obtain N where "\<forall>n\<ge>N. dist (x n) l < e * \<bar>c\<bar>" using as(2)[unfolded Lim_sequentially, THEN spec[where x="e * abs c"]] by auto
- hence "\<exists>N. \<forall>n\<ge>N. dist ((1 / c) *s x n) ((1 / c) *s l) < e" unfolding dist_def unfolding vector_ssub_ldistrib[THEN sym] norm_mul
+ hence "\<exists>N. \<forall>n\<ge>N. dist ((1 / c) *s x n) ((1 / c) *s l) < e" unfolding dist_norm unfolding vector_ssub_ldistrib[THEN sym] norm_mul
using mult_imp_div_pos_less[of "abs c" _ e] `c\<noteq>0` by auto }
hence "((\<lambda>n. (1 / c) *s x n) ---> (1 / c) *s l) sequentially" unfolding Lim_sequentially by auto
ultimately have "l \<in> op *s c ` s" using assms[unfolded closed_sequential_limits, THEN spec[where x="\<lambda>n. (1/c) *s x n"], THEN spec[where x="(1/c) *s l"]]
@@ -4301,7 +4303,7 @@
hence "x - y \<in> {x - y |x y. x \<in> s \<and> y \<in> t}" by auto
hence "d \<le> dist (x - y) 0" using d[THEN bspec[where x="x - y"]] using dist_commute
by (auto simp add: dist_commute)
- hence "d \<le> dist x y" unfolding dist_def by auto }
+ hence "d \<le> dist x y" unfolding dist_norm by auto }
thus ?thesis using `d>0` by auto
qed
@@ -4504,7 +4506,7 @@
{ fix x' assume as:"dist x' x < ?d"
{ fix i
have "\<bar>x'$i - x $ i\<bar> < d i"
- using norm_bound_component_lt[OF as[unfolded dist_def], of i]
+ using norm_bound_component_lt[OF as[unfolded dist_norm], of i]
unfolding vector_minus_component and Min_gr_iff[OF **] by auto
hence "a $ i < x' $ i" "x' $ i < b $ i" using d[THEN spec[where x=i]] by auto }
hence "a < x' \<and> x' < b" unfolding vector_less_def by auto }
@@ -4518,13 +4520,13 @@
{ fix x i assume as:"\<forall>e>0. \<exists>x'\<in>{a..b}. x' \<noteq> x \<and> dist x' x < e"(* and xab:"a$i > x$i \<or> b$i < x$i"*)
{ assume xa:"a$i > x$i"
with as obtain y where y:"y\<in>{a..b}" "y \<noteq> x" "dist y x < a$i - x$i" by(erule_tac x="a$i - x$i" in allE)auto
- hence False unfolding mem_interval and dist_def
+ hence False unfolding mem_interval and dist_norm
using component_le_norm[of "y-x" i, unfolded vector_minus_component] and xa by(auto elim!: allE[where x=i])
} hence "a$i \<le> x$i" by(rule ccontr)auto
moreover
{ assume xb:"b$i < x$i"
with as obtain y where y:"y\<in>{a..b}" "y \<noteq> x" "dist y x < x$i - b$i" by(erule_tac x="x$i - b$i" in allE)auto
- hence False unfolding mem_interval and dist_def
+ hence False unfolding mem_interval and dist_norm
using component_le_norm[of "y-x" i, unfolded vector_minus_component] and xb by(auto elim!: allE[where x=i])
} hence "x$i \<le> b$i" by(rule ccontr)auto
ultimately
@@ -4543,7 +4545,7 @@
{ fix i
have "dist (x - (e / 2) *s basis i) x < e"
"dist (x + (e / 2) *s basis i) x < e"
- unfolding dist_def apply auto
+ unfolding dist_norm apply auto
unfolding norm_minus_cancel and norm_mul using norm_basis[of i] and `e>0` by auto
hence "a $ i \<le> (x - (e / 2) *s basis i) $ i"
"(x + (e / 2) *s basis i) $ i \<le> b $ i"
@@ -4761,7 +4763,7 @@
fix x::"real^'n" assume x:"\<forall>e>0. \<exists>x'\<in>{x. \<forall>i. x $ i \<le> b $ i}. x' \<noteq> x \<and> dist x' x < e"
{ assume "x$i > b$i"
then obtain y where "y $ i \<le> b $ i" "y \<noteq> x" "dist y x < x$i - b$i" using x[THEN spec[where x="x$i - b$i"]] by auto
- hence False using component_le_norm[of "y - x" i] unfolding dist_def and vector_minus_component by auto }
+ hence False using component_le_norm[of "y - x" i] unfolding dist_norm and vector_minus_component by auto }
hence "x$i \<le> b$i" by(rule ccontr)auto }
thus ?thesis unfolding closed_limpt unfolding islimpt_approachable by blast
qed
@@ -4773,7 +4775,7 @@
fix x::"real^'n" assume x:"\<forall>e>0. \<exists>x'\<in>{x. \<forall>i. a $ i \<le> x $ i}. x' \<noteq> x \<and> dist x' x < e"
{ assume "a$i > x$i"
then obtain y where "a $ i \<le> y $ i" "y \<noteq> x" "dist y x < a$i - x$i" using x[THEN spec[where x="a$i - x$i"]] by auto
- hence False using component_le_norm[of "y - x" i] unfolding dist_def and vector_minus_component by auto }
+ hence False using component_le_norm[of "y - x" i] unfolding dist_norm and vector_minus_component by auto }
hence "a$i \<le> x$i" by(rule ccontr)auto }
thus ?thesis unfolding closed_limpt unfolding islimpt_approachable by blast
qed
@@ -4810,7 +4812,7 @@
then obtain x y where x:"netord net x y" and y:"\<forall>x. netord net x y \<longrightarrow> dist l (f x) < e / norm a" apply(erule_tac x="e / norm a" in allE) apply auto using False using norm_ge_zero[of a] apply auto
using divide_pos_pos[of e "norm a"] by auto
{ fix z assume "netord net z y" hence "dist l (f z) < e / norm a" using y by blast
- hence "norm a * norm (l - f z) < e" unfolding dist_def and
+ hence "norm a * norm (l - f z) < e" unfolding dist_norm and
pos_less_divide_eq[OF False[unfolded vec_0 zero_less_norm_iff[of a, THEN sym]]] and real_mult_commute by auto
hence "\<bar>a \<bullet> l - a \<bullet> f z\<bar> < e" using order_le_less_trans[OF norm_cauchy_schwarz_abs[of a "l - f z"], of e] unfolding dot_rsub[symmetric] by auto }
hence "\<exists>y. (\<exists>x. netord net x y) \<and> (\<forall>x. netord net x y \<longrightarrow> \<bar>a \<bullet> l - a \<bullet> f x\<bar> < e)" using x by auto }
@@ -4980,7 +4982,7 @@
hence "\<forall>m n. m \<le> n \<longrightarrow> dest_vec1 (s m) \<le> dest_vec1 (s n)" by auto
then obtain l where "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<bar>dest_vec1 (s n) - l\<bar> < e" using convergent_bounded_monotone[OF a] by auto
thus ?thesis unfolding Lim_sequentially apply(rule_tac x="vec1 l" in exI)
- unfolding dist_def unfolding abs_dest_vec1 and dest_vec1_sub by auto
+ unfolding dist_norm unfolding abs_dest_vec1 and dest_vec1_sub by auto
qed
subsection{* Basic homeomorphism definitions. *}
@@ -5119,7 +5121,7 @@
show ?th unfolding homeomorphic_minimal
apply(rule_tac x="\<lambda>x. b + (e/d) *s (x - a)" in exI)
apply(rule_tac x="\<lambda>x. a + (d/e) *s (x - b)" in exI)
- apply (auto simp add: dist_commute) unfolding dist_def and vector_smult_assoc using assms apply auto
+ apply (auto simp add: dist_commute) unfolding dist_norm and vector_smult_assoc using assms apply auto
unfolding norm_minus_cancel and norm_mul
using continuous_on_add[OF continuous_on_const continuous_on_cmul[OF continuous_on_sub[OF continuous_on_id continuous_on_const]]]
apply (auto simp add: dist_commute)
@@ -5131,7 +5133,7 @@
show ?cth unfolding homeomorphic_minimal
apply(rule_tac x="\<lambda>x. b + (e/d) *s (x - a)" in exI)
apply(rule_tac x="\<lambda>x. a + (d/e) *s (x - b)" in exI)
- apply (auto simp add: dist_commute) unfolding dist_def and vector_smult_assoc using assms apply auto
+ apply (auto simp add: dist_commute) unfolding dist_norm and vector_smult_assoc using assms apply auto
unfolding norm_minus_cancel and norm_mul
using continuous_on_add[OF continuous_on_const continuous_on_cmul[OF continuous_on_sub[OF continuous_on_id continuous_on_const]]]
apply auto
@@ -5148,7 +5150,7 @@
proof-
{ fix d::real assume "d>0"
then obtain N where N:"\<forall>n\<ge>N. norm (f (x n) - f (x N)) < e * d"
- using cf[unfolded cauchy o_def dist_def, THEN spec[where x="e*d"]] and e and mult_pos_pos[of e d] by auto
+ using cf[unfolded cauchy o_def dist_norm, THEN spec[where x="e*d"]] and e and mult_pos_pos[of e d] by auto
{ fix n assume "n\<ge>N"
hence "norm (f (x n - x N)) < e * d" using N[THEN spec[where x=n]] unfolding linear_sub[OF f, THEN sym] by auto
moreover have "e * norm (x n - x N) \<le> norm (f (x n - x N))"
@@ -5157,7 +5159,7 @@
ultimately have "norm (x n - x N) < d" using `e>0`
using mult_left_less_imp_less[of e "norm (x n - x N)" d] by auto }
hence "\<exists>N. \<forall>n\<ge>N. norm (x n - x N) < d" by auto }
- thus ?thesis unfolding cauchy and dist_def by auto
+ thus ?thesis unfolding cauchy and dist_norm by auto
qed
lemma complete_isometric_image:
@@ -5178,7 +5180,10 @@
thus ?thesis unfolding complete_def by auto
qed
-lemma dist_0_norm:"dist 0 x = norm x" unfolding dist_def by(auto simp add: norm_minus_cancel)
+lemma dist_0_norm:
+ fixes x :: "'a::real_normed_vector"
+ shows "dist 0 x = norm x"
+unfolding dist_norm by simp
lemma injective_imp_isometric: fixes f::"real^'m::finite \<Rightarrow> real^'n::finite"
assumes s:"closed s" "subspace s" and f:"linear f" "\<forall>x\<in>s. (f x = 0) \<longrightarrow> (x = 0)"
@@ -5197,7 +5202,7 @@
let ?S' = "{x::real^'m. x\<in>s \<and> norm x = norm a}"
let ?S'' = "{x::real^'m. norm x = norm a}"
- have "?S'' = frontier(cball 0 (norm a))" unfolding frontier_cball and dist_def by (auto simp add: norm_minus_cancel)
+ have "?S'' = frontier(cball 0 (norm a))" unfolding frontier_cball and dist_norm by (auto simp add: norm_minus_cancel)
hence "compact ?S''" using compact_frontier[OF compact_cball, of 0 "norm a"] by auto
moreover have "?S' = s \<inter> ?S''" by auto
ultimately have "compact ?S'" using closed_inter_compact[of s ?S''] using s(1) by auto
@@ -5652,9 +5657,9 @@
unfolding o_def and h_def a_def b_def by auto
{ fix n::nat
- have *:"\<And>fx fy (x::real^_) y. dist fx fy \<le> dist x y \<Longrightarrow> \<not> (dist (fx - fy) (a - b) < dist a b - dist x y)" unfolding dist_def by norm
+ have *:"\<And>fx fy (x::real^_) y. dist fx fy \<le> dist x y \<Longrightarrow> \<not> (dist (fx - fy) (a - b) < dist a b - dist x y)" unfolding dist_norm by norm
{ fix x y ::"real^'a"
- have "dist (-x) (-y) = dist x y" unfolding dist_def
+ have "dist (-x) (-y) = dist x y" unfolding dist_norm
using norm_minus_cancel[of "x - y"] by (auto simp add: uminus_add_conv_diff) } note ** = this
{ assume as:"dist a b > dist (f n x) (f n y)"
--- a/src/HOL/RealVector.thy Thu May 28 14:36:21 2009 -0700
+++ b/src/HOL/RealVector.thy Thu May 28 17:00:02 2009 -0700
@@ -416,6 +416,45 @@
by (rule Reals_cases) auto
+subsection {* Metric spaces *}
+
+class dist =
+ fixes dist :: "'a \<Rightarrow> 'a \<Rightarrow> real"
+
+class metric_space = dist +
+ assumes dist_eq_0_iff [simp]: "dist x y = 0 \<longleftrightarrow> x = y"
+ assumes dist_triangle2: "dist x y \<le> dist x z + dist y z"
+begin
+
+lemma dist_self [simp]: "dist x x = 0"
+by simp
+
+lemma zero_le_dist [simp]: "0 \<le> dist x y"
+using dist_triangle2 [of x x y] by simp
+
+lemma zero_less_dist_iff: "0 < dist x y \<longleftrightarrow> x \<noteq> y"
+by (simp add: less_le)
+
+lemma dist_not_less_zero [simp]: "\<not> dist x y < 0"
+by (simp add: not_less)
+
+lemma dist_le_zero_iff [simp]: "dist x y \<le> 0 \<longleftrightarrow> x = y"
+by (simp add: le_less)
+
+lemma dist_commute: "dist x y = dist y x"
+proof (rule order_antisym)
+ show "dist x y \<le> dist y x"
+ using dist_triangle2 [of x y x] by simp
+ show "dist y x \<le> dist x y"
+ using dist_triangle2 [of y x y] by simp
+qed
+
+lemma dist_triangle: "dist x z \<le> dist x y + dist y z"
+using dist_triangle2 [of x z y] by (simp add: dist_commute)
+
+end
+
+
subsection {* Real normed vector spaces *}
class norm =
@@ -424,7 +463,10 @@
class sgn_div_norm = scaleR + norm + sgn +
assumes sgn_div_norm: "sgn x = x /\<^sub>R norm x"
-class real_normed_vector = real_vector + sgn_div_norm +
+class dist_norm = dist + norm + minus +
+ assumes dist_norm: "dist x y = norm (x - y)"
+
+class real_normed_vector = real_vector + sgn_div_norm + dist_norm +
assumes norm_ge_zero [simp]: "0 \<le> norm x"
and norm_eq_zero [simp]: "norm x = 0 \<longleftrightarrow> x = 0"
and norm_triangle_ineq: "norm (x + y) \<le> norm x + norm y"
@@ -458,8 +500,12 @@
definition
real_norm_def [simp]: "norm r = \<bar>r\<bar>"
+definition
+ dist_real_def: "dist x y = \<bar>x - y\<bar>"
+
instance
apply (intro_classes, unfold real_norm_def real_scaleR_def)
+apply (rule dist_real_def)
apply (simp add: real_sgn_def)
apply (rule abs_ge_zero)
apply (rule abs_eq_0)
@@ -637,43 +683,17 @@
shows "norm (x ^ n) = norm x ^ n"
by (induct n) (simp_all add: norm_mult)
-
-subsection {* Distance function *}
-
-(* TODO: There should be a metric_space class for this,
-which should be a superclass of real_normed_vector. *)
-
-definition
- dist :: "'a::real_normed_vector \<Rightarrow> 'a \<Rightarrow> real"
-where
- "dist x y = norm (x - y)"
-
-lemma zero_le_dist [simp]: "0 \<le> dist x y"
-unfolding dist_def by (rule norm_ge_zero)
-
-lemma dist_eq_0_iff [simp]: "dist x y = 0 \<longleftrightarrow> x = y"
-unfolding dist_def by simp
+text {* Every normed vector space is a metric space. *}
-lemma dist_self [simp]: "dist x x = 0"
-unfolding dist_def by simp
-
-lemma zero_less_dist_iff: "0 < dist x y \<longleftrightarrow> x \<noteq> y"
-by (simp add: less_le)
-
-lemma dist_not_less_zero [simp]: "\<not> dist x y < 0"
-by (simp add: not_less)
-
-lemma dist_le_zero_iff [simp]: "dist x y \<le> 0 \<longleftrightarrow> x = y"
-by (simp add: le_less)
-
-lemma dist_commute: "dist x y = dist y x"
-unfolding dist_def by (rule norm_minus_commute)
-
-lemma dist_triangle: "dist x z \<le> dist x y + dist y z"
-unfolding dist_def
-apply (rule ord_eq_le_trans [OF _ norm_triangle_ineq])
-apply (simp add: diff_minus)
-done
+instance real_normed_vector < metric_space
+proof
+ fix x y :: 'a show "dist x y = 0 \<longleftrightarrow> x = y"
+ unfolding dist_norm by simp
+next
+ fix x y z :: 'a show "dist x y \<le> dist x z + dist y z"
+ unfolding dist_norm
+ using norm_triangle_ineq4 [of "x - z" "y - z"] by simp
+qed
subsection {* Sign function *}