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.5    by (simp add: norm_vector_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
    1.75 +lemma dist_triangle_add_half:
    1.76 +  " dist x x' < e / 2 \<Longrightarrow> dist y y' < e / 2 \<Longrightarrow> dist(x + y) (x' + y') < e"
    1.77 +by (rule le_less_trans [OF dist_triangle_add], simp)
    1.78  
    1.79  lemma setsum_component [simp]:
    1.80    fixes f:: " 'a \<Rightarrow> ('b::comm_monoid_add) ^'n"