Quelle  Metric_Arith_Examples.thy

theory Metric_Arith_Examples
imports "HOL-Analysis.Elementary_Metric_Spaces"
begin


text ‹simple examples›

lemma "∃x::'a::metric_space. x=x"
  by metric
lemma "∀(x::'a::metric_space). ∃y. x = y"
  by metric


text ‹reasoning with "dist x y = 0 ⟷ x = y"›

lemma "∃x y. dist x y = 0"
  by metric

lemma "∃y. dist x y = 0"
  by metric

lemma "0 = dist x y ==> x = y"
  by metric

lemma "x ≠ y ==> dist x y ≠ 0"
  by metric

lemma "∃y. dist x y ≠ 1"
  by metric

lemma "x = y ⟷ dist x x = dist y x ∧ dist x y = dist y y"
  by metric

lemma "dist a b ≠ dist a c ==> b ≠ c"
  by metric

text ‹reasoning with positive semidefiniteness›

lemma "dist y x + c ≥ c"
  by metric

lemma "dist x y + dist x z ≥ 0"
  by metric

lemma "dist x y ≥ v ==> dist x y + dist (a::'a) b ≥ v" for x::"('a::metric_space)"
  by metric

lemma "dist x y < 0 ⟶ P"
  by metric

text ‹reasoning with the triangle inequality›

lemma "dist a d ≤ dist a b + dist b c + dist c d"
  by metric

lemma "dist a e ≤ dist a b + dist b c + dist c d + dist d e"
  by metric

lemma "max (dist x y) ∣dist x z - dist z y∣ = dist x y"
  by metric

lemma
  "dist w x < e/3 ==> dist x y < e/3 ==> dist y z < e/3 ==> dist w x < e"
  by metric

lemma "dist w x < e/4 ==> dist x y < e/4 ==> dist y z < e/2 ==> dist w z < e"
  by metric


text ‹more complex examples›

lemma "dist x y ≤ e ==> dist x z ≤ e ==> dist y z ≤ e
  ==> p ∈ (cball x e ∪ cball y e ∪ cball z e) ==> dist p x ≤ 2*e"
  by metric

lemma hol_light_example:
  "¬ disjnt (ball x r) (ball y s) ⟶
    (∀p q. p ∈ ball x r ∪ ball y s ∧ q ∈ ball x r ∪ ball y s ⟶ dist p q < 2 * (r + s))"
  unfolding disjnt_iff
  by metric

lemma "dist x y ≤ e ==> z ∈ ball x f ==> dist z y < e + f"
  by metric

lemma "dist x y = r / 2 ==> (∀z. dist x z < r / 4 ⟶ dist y z ≤ 3 * r / 4)"
  by metric

lemma "s ≥ 0 ==> t ≥ 0 ==> z ∈ (ball x s) ∪ (ball y t) ==> dist z y ≤ dist x y + s + t"
  by metric

lemma "0 < r ==> ball x r ⊆ ball y s ==> ball x r ⊆ ball z t ==> dist y z ≤ s + t"
  by metric


text ‹non-trivial quantifier structure›

lemma "∃x. ∀r≤0. ∃z. dist x z ≥ r"
  by metric

lemma "∧a r x y. dist x a + dist a y = r ==> ∀z. r ≤ dist x z + dist z y ==> dist x y = r"
  by metric

end