Theory HOL-Analysis.Metric_Arith

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

chapter ‹Functional Analysis›

sectiontag unimportant› ‹A decision procedure for metric spaces›

theory Metric_Arith
  imports HOL.Real_Vector_Spaces
begin

texttag 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: "(xinsert a B. P x) = (P a  (xB. P x))"
  by blast

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

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)"
      by (simp add: finite 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  (as. 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