# Theory Metric_Arith

```(*  Title:      HOL/Analysis/Metric_Arith.thy
Author:     Maximilian Schäffeler (port from HOL Light)
*)

chapter ‹Functional Analysis›

section✐‹tag unimportant› ‹A decision procedure for metric spaces›

theory Metric_Arith
imports HOL.Real_Vector_Spaces
begin

text✐‹tag unimportant› ‹
A port of the decision procedure ``Formalization of metric spaces in HOL Light''
\<^cite>‹"DBLP:journals/jar/Maggesi18"› for the type class @{class metric_space},
with the ‹Argo› solver as backend.
›

named_theorems metric_prenex
named_theorems metric_nnf
named_theorems metric_unfold
named_theorems metric_pre_arith

lemmas pre_arith_simps =
max.bounded_iff max_less_iff_conj
le_max_iff_disj less_max_iff_disj
simp_thms HOL.eq_commute
declare pre_arith_simps [metric_pre_arith]

lemmas unfold_simps =
Un_iff subset_iff disjoint_iff_not_equal
Ball_def Bex_def
declare unfold_simps [metric_unfold]

declare HOL.nnf_simps(4) [metric_prenex]

lemma imp_prenex [metric_prenex]:
"⋀P Q. (∃x. P x) ⟶ Q ≡ ∀x. (P x ⟶ Q)"
"⋀P Q. P ⟶ (∃x. Q x) ≡ ∃x. (P ⟶ Q x)"
"⋀P Q. (∀x. P x) ⟶ Q ≡ ∃x. (P x ⟶ Q)"
"⋀P Q. P ⟶ (∀x. Q x) ≡ ∀x. (P ⟶ Q x)"
by simp_all

lemma ex_prenex [metric_prenex]:
"⋀P Q. (∃x. P x) ∧ Q ≡ ∃x. (P x ∧ Q)"
"⋀P Q. P ∧ (∃x. Q x) ≡ ∃x. (P ∧ Q x)"
"⋀P Q. (∃x. P x) ∨ Q ≡ ∃x. (P x ∨ Q)"
"⋀P Q. P ∨ (∃x. Q x) ≡ ∃x. (P ∨ Q x)"
"⋀P. ¬(∃x. P x) ≡ ∀x. ¬P x"
by simp_all

lemma all_prenex [metric_prenex]:
"⋀P Q. (∀x. P x) ∧ Q ≡ ∀x. (P x ∧ Q)"
"⋀P Q. P ∧ (∀x. Q x) ≡ ∀x. (P ∧ Q x)"
"⋀P Q. (∀x. P x) ∨ Q ≡ ∀x. (P x ∨ Q)"
"⋀P Q. P ∨ (∀x. Q x) ≡ ∀x. (P ∨ Q x)"
"⋀P. ¬(∀x. P x) ≡ ∃x. ¬P x"
by simp_all

lemma nnf_thms [metric_nnf]:
"(¬ (P ∧ Q)) = (¬ P ∨ ¬ Q)"
"(¬ (P ∨ Q)) = (¬ P ∧ ¬ Q)"
"(P ⟶ Q) = (¬ P ∨ Q)"
"(P = Q) ⟷ (P ∨ ¬ Q) ∧ (¬ P ∨ Q)"
"(¬ (P = Q)) ⟷ (¬ P ∨ ¬ Q) ∧ (P ∨ Q)"
"(¬ ¬ P) = P"
by blast+

lemmas nnf_simps = nnf_thms linorder_not_less linorder_not_le
declare nnf_simps[metric_nnf]

lemma ball_insert: "(∀x∈insert a B. P x) = (P a ∧ (∀x∈B. P x))"
by blast

lemma Sup_insert_insert:
fixes a::real
shows "Sup (insert a (insert b s)) = Sup (insert (max a b) s)"

lemma real_abs_dist: "¦dist x y¦ = dist x y"
by simp

lemma maxdist_thm [THEN HOL.eq_reflection]:
assumes "finite s" "x ∈ s" "y ∈ s"
defines "⋀a. f a ≡ ¦dist x a - dist a y¦"
shows "dist x y = Sup (f ` s)"
proof -
have "dist x y ≤ Sup (f ` s)"
proof -
have "finite (f ` s)"
moreover have "¦dist x y - dist y y¦ ∈ f ` s"
by (metis ‹y ∈ s› f_def imageI)
ultimately show ?thesis
using le_cSup_finite by simp
qed
also have "Sup (f ` s) ≤ dist x y"
using ‹x ∈ s› cSUP_least[of s f] abs_dist_diff_le
unfolding f_def
by blast
finally show ?thesis .
qed

theorem metric_eq_thm [THEN HOL.eq_reflection]:
"x ∈ s ⟹ y ∈ s ⟹ x = y ⟷ (∀a∈s. dist x a = dist y a)"
by auto

ML_file ‹metric_arith.ML›

method_setup metric = ‹
Scan.succeed (SIMPLE_METHOD' o Metric_Arith.metric_arith_tac)
› "prove simple linear statements in metric spaces (∀∃⇩p fragment)"

end
```