Theory Metric

(*  Title:       Metric and semimetric spaces
    Author:      Tim Makarios <tjm1983 at gmail.com>, 2012
    Maintainer:  Tim Makarios <tjm1983 at gmail.com>
*)

section "Metric and semimetric spaces"

theory Metric
imports "HOL-Analysis.Multivariate_Analysis"
begin

locale semimetric =
  fixes dist :: "'p ⇒ 'p ⇒ real"
  assumes nonneg [simp]: "dist x y ≥ 0"
  and eq_0 [simp]: "dist x y = 0 ⟷ x = y"
  and symm: "dist x y = dist y x"
begin
  lemma refl [simp]: "dist x x = 0"
    by simp
end

locale metric =
  fixes dist :: "'p ⇒ 'p ⇒ real"
  assumes [simp]: "dist x y = 0 ⟷ x = y"
  and triangle: "dist x z ≤ dist y x + dist y z"

sublocale metric < semimetric
proof
  { fix w
    have "dist w w = 0" by simp }
  note [simp] = this
  fix x y
  show "0 ≤ dist x y"
  proof -
    from triangle [of y y x] show "0 ≤ dist x y" by simp
  qed
  show "dist x y = 0 ⟷ x = y" by simp
  show "dist x y = dist y x"
  proof -
    { fix w z
      have "dist w z ≤ dist z w"
      proof -
        from triangle [of w z z] show "dist w z ≤ dist z w" by simp
      qed }
    hence "dist x y ≤ dist y x" and "dist y x ≤ dist x y" by simp+
    thus "dist x y = dist y x" by simp
  qed
qed

definition norm_dist :: "('a::real_normed_vector) ⇒ 'a ⇒ real" where
[simp]: "norm_dist x y ≡ norm (x - y)"

interpretation norm_metric: metric norm_dist
proof
  fix x y
  show "norm_dist x y = 0 ⟷ x = y" by simp
  fix z
  from norm_triangle_ineq [of "x - y" "y - z"] have
    "norm (x - z) ≤ norm (x - y) + norm (y - z)" by simp
  with norm_minus_commute [of x y] show
    "norm_dist x z ≤ norm_dist y x + norm_dist y z" by simp
qed

end