src/HOL/RealVector.thy
changeset 31289 847f00f435d4
parent 31285 0a3f9ee4117c
child 31413 729d90a531e4
     1.1 --- a/src/HOL/RealVector.thy	Thu May 28 14:36:21 2009 -0700
     1.2 +++ b/src/HOL/RealVector.thy	Thu May 28 17:00:02 2009 -0700
     1.3 @@ -416,6 +416,45 @@
     1.4    by (rule Reals_cases) auto
     1.5  
     1.6  
     1.7 +subsection {* Metric spaces *}
     1.8 +
     1.9 +class dist =
    1.10 +  fixes dist :: "'a \<Rightarrow> 'a \<Rightarrow> real"
    1.11 +
    1.12 +class metric_space = dist +
    1.13 +  assumes dist_eq_0_iff [simp]: "dist x y = 0 \<longleftrightarrow> x = y"
    1.14 +  assumes dist_triangle2: "dist x y \<le> dist x z + dist y z"
    1.15 +begin
    1.16 +
    1.17 +lemma dist_self [simp]: "dist x x = 0"
    1.18 +by simp
    1.19 +
    1.20 +lemma zero_le_dist [simp]: "0 \<le> dist x y"
    1.21 +using dist_triangle2 [of x x y] by simp
    1.22 +
    1.23 +lemma zero_less_dist_iff: "0 < dist x y \<longleftrightarrow> x \<noteq> y"
    1.24 +by (simp add: less_le)
    1.25 +
    1.26 +lemma dist_not_less_zero [simp]: "\<not> dist x y < 0"
    1.27 +by (simp add: not_less)
    1.28 +
    1.29 +lemma dist_le_zero_iff [simp]: "dist x y \<le> 0 \<longleftrightarrow> x = y"
    1.30 +by (simp add: le_less)
    1.31 +
    1.32 +lemma dist_commute: "dist x y = dist y x"
    1.33 +proof (rule order_antisym)
    1.34 +  show "dist x y \<le> dist y x"
    1.35 +    using dist_triangle2 [of x y x] by simp
    1.36 +  show "dist y x \<le> dist x y"
    1.37 +    using dist_triangle2 [of y x y] by simp
    1.38 +qed
    1.39 +
    1.40 +lemma dist_triangle: "dist x z \<le> dist x y + dist y z"
    1.41 +using dist_triangle2 [of x z y] by (simp add: dist_commute)
    1.42 +
    1.43 +end
    1.44 +
    1.45 +
    1.46  subsection {* Real normed vector spaces *}
    1.47  
    1.48  class norm =
    1.49 @@ -424,7 +463,10 @@
    1.50  class sgn_div_norm = scaleR + norm + sgn +
    1.51    assumes sgn_div_norm: "sgn x = x /\<^sub>R norm x"
    1.52  
    1.53 -class real_normed_vector = real_vector + sgn_div_norm +
    1.54 +class dist_norm = dist + norm + minus +
    1.55 +  assumes dist_norm: "dist x y = norm (x - y)"
    1.56 +
    1.57 +class real_normed_vector = real_vector + sgn_div_norm + dist_norm +
    1.58    assumes norm_ge_zero [simp]: "0 \<le> norm x"
    1.59    and norm_eq_zero [simp]: "norm x = 0 \<longleftrightarrow> x = 0"
    1.60    and norm_triangle_ineq: "norm (x + y) \<le> norm x + norm y"
    1.61 @@ -458,8 +500,12 @@
    1.62  definition
    1.63    real_norm_def [simp]: "norm r = \<bar>r\<bar>"
    1.64  
    1.65 +definition
    1.66 +  dist_real_def: "dist x y = \<bar>x - y\<bar>"
    1.67 +
    1.68  instance
    1.69  apply (intro_classes, unfold real_norm_def real_scaleR_def)
    1.70 +apply (rule dist_real_def)
    1.71  apply (simp add: real_sgn_def)
    1.72  apply (rule abs_ge_zero)
    1.73  apply (rule abs_eq_0)
    1.74 @@ -637,43 +683,17 @@
    1.75    shows "norm (x ^ n) = norm x ^ n"
    1.76  by (induct n) (simp_all add: norm_mult)
    1.77  
    1.78 -
    1.79 -subsection {* Distance function *}
    1.80 -
    1.81 -(* TODO: There should be a metric_space class for this,
    1.82 -which should be a superclass of real_normed_vector. *)
    1.83 -
    1.84 -definition
    1.85 -  dist :: "'a::real_normed_vector \<Rightarrow> 'a \<Rightarrow> real"
    1.86 -where
    1.87 -  "dist x y = norm (x - y)"
    1.88 -
    1.89 -lemma zero_le_dist [simp]: "0 \<le> dist x y"
    1.90 -unfolding dist_def by (rule norm_ge_zero)
    1.91 -
    1.92 -lemma dist_eq_0_iff [simp]: "dist x y = 0 \<longleftrightarrow> x = y"
    1.93 -unfolding dist_def by simp
    1.94 +text {* Every normed vector space is a metric space. *}
    1.95  
    1.96 -lemma dist_self [simp]: "dist x x = 0"
    1.97 -unfolding dist_def by simp
    1.98 -
    1.99 -lemma zero_less_dist_iff: "0 < dist x y \<longleftrightarrow> x \<noteq> y"
   1.100 -by (simp add: less_le)
   1.101 -
   1.102 -lemma dist_not_less_zero [simp]: "\<not> dist x y < 0"
   1.103 -by (simp add: not_less)
   1.104 -
   1.105 -lemma dist_le_zero_iff [simp]: "dist x y \<le> 0 \<longleftrightarrow> x = y"
   1.106 -by (simp add: le_less)
   1.107 -
   1.108 -lemma dist_commute: "dist x y = dist y x"
   1.109 -unfolding dist_def by (rule norm_minus_commute)
   1.110 -
   1.111 -lemma dist_triangle: "dist x z \<le> dist x y + dist y z"
   1.112 -unfolding dist_def
   1.113 -apply (rule ord_eq_le_trans [OF _ norm_triangle_ineq])
   1.114 -apply (simp add: diff_minus)
   1.115 -done
   1.116 +instance real_normed_vector < metric_space
   1.117 +proof
   1.118 +  fix x y :: 'a show "dist x y = 0 \<longleftrightarrow> x = y"
   1.119 +    unfolding dist_norm by simp
   1.120 +next
   1.121 +  fix x y z :: 'a show "dist x y \<le> dist x z + dist y z"
   1.122 +    unfolding dist_norm
   1.123 +    using norm_triangle_ineq4 [of "x - z" "y - z"] by simp
   1.124 +qed
   1.125  
   1.126  
   1.127  subsection {* Sign function *}