--- 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 *}