src/HOL/Library/Euclidean_Space.thy
 changeset 31285 0a3f9ee4117c parent 31275 1ba01cdd9a9a child 31289 847f00f435d4
```     1.1 --- a/src/HOL/Library/Euclidean_Space.thy	Thu May 28 15:54:20 2009 +0200
1.2 +++ b/src/HOL/Library/Euclidean_Space.thy	Thu May 28 13:41:41 2009 -0700
1.3 @@ -620,12 +620,6 @@
1.4  lemma norm_real: "norm(x::real ^ 1) = abs(x\$1)"
1.6
1.7 -text{* Metric *}
1.8 -
1.9 -text {* FIXME: generalize to arbitrary @{text real_normed_vector} types *}
1.10 -definition dist:: "real ^ 'n::finite \<Rightarrow> real ^ 'n \<Rightarrow> real" where
1.11 -  "dist x y = norm (x - y)"
1.12 -
1.13  lemma dist_real: "dist(x::real ^ 1) y = abs((x\$1) - (y\$1))"
1.14    by (auto simp add: norm_real dist_def)
1.15
1.16 @@ -959,38 +953,38 @@
1.17
1.18  text{* Hence more metric properties. *}
1.19
1.20 -lemma dist_refl[simp]: "dist x x = 0" by norm
1.21 -
1.22 -lemma dist_sym: "dist x y = dist y x"by norm
1.23 -
1.24 -lemma dist_pos_le[simp]: "0 <= dist x y" by norm
1.25 -
1.26 -lemma dist_triangle: "dist x z <= dist x y + dist y z" by norm
1.27 -
1.28 -lemma dist_triangle_alt: "dist y z <= dist x y + dist x z" by norm
1.29 -
1.30 -lemma dist_eq_0[simp]: "dist x y = 0 \<longleftrightarrow> x = y" by norm
1.31 -
1.32 -lemma dist_pos_lt: "x \<noteq> y ==> 0 < dist x y" by norm
1.33 -lemma dist_nz:  "x \<noteq> y \<longleftrightarrow> 0 < dist x y" by norm
1.34 -
1.35 -lemma dist_triangle_le: "dist x z + dist y z <= e \<Longrightarrow> dist x y <= e" by norm
1.36 -
1.37 -lemma dist_triangle_lt: "dist x z + dist y z < e ==> dist x y < e" by norm
1.38 -
1.39 -lemma dist_triangle_half_l: "dist x1 y < e / 2 \<Longrightarrow> dist x2 y < e / 2 ==> dist x1 x2 < e" by norm
1.40 -
1.41 -lemma dist_triangle_half_r: "dist y x1 < e / 2 \<Longrightarrow> dist y x2 < e / 2 ==> dist x1 x2 < e" by norm
1.42 +lemma dist_triangle_alt: "dist y z <= dist x y + dist x z"
1.43 +using dist_triangle [of y z x] by (simp add: dist_commute)
1.44 +
1.45 +lemma dist_triangle2: "dist x y \<le> dist x z + dist y z"
1.46 +using dist_triangle [of x y z] by (simp add: dist_commute)
1.47 +
1.48 +lemma dist_pos_lt: "x \<noteq> y ==> 0 < dist x y" by (simp add: zero_less_dist_iff)
1.49 +lemma dist_nz:  "x \<noteq> y \<longleftrightarrow> 0 < dist x y" by (simp add: zero_less_dist_iff)
1.50 +
1.51 +lemma dist_triangle_le: "dist x z + dist y z <= e \<Longrightarrow> dist x y <= e"
1.52 +by (rule order_trans [OF dist_triangle2])
1.53 +
1.54 +lemma dist_triangle_lt: "dist x z + dist y z < e ==> dist x y < e"
1.55 +by (rule le_less_trans [OF dist_triangle2])
1.56 +
1.57 +lemma dist_triangle_half_l:
1.58 +  "dist x1 y < e / 2 \<Longrightarrow> dist x2 y < e / 2 \<Longrightarrow> dist x1 x2 < e"
1.59 +by (rule dist_triangle_lt [where z=y], simp)
1.60 +
1.61 +lemma dist_triangle_half_r:
1.62 +  "dist y x1 < e / 2 \<Longrightarrow> dist y x2 < e / 2 \<Longrightarrow> dist x1 x2 < e"
1.63 +by (rule dist_triangle_half_l, simp_all add: dist_commute)
1.64
1.65  lemma dist_triangle_add: "dist (x + y) (x' + y') <= dist x x' + dist y y'"
1.66 -  by norm
1.67 +unfolding dist_def by (rule norm_diff_triangle_ineq)
1.68
1.69  lemma dist_mul[simp]: "dist (c *s x) (c *s y) = \<bar>c\<bar> * dist x y"
1.70    unfolding dist_def vector_ssub_ldistrib[symmetric] norm_mul ..
1.71
1.72 -lemma dist_triangle_add_half: " dist x x' < e / 2 \<Longrightarrow> dist y y' < e / 2 ==> dist(x + y) (x' + y') < e" by norm
1.73 -
1.74 -lemma dist_le_0[simp]: "dist x y <= 0 \<longleftrightarrow> x = y" by norm