Theory Metric_Arith_Examples

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