# 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