(* 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
''
🍋‹"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)"
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 \ (\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 (\\\<^sub>p fragment)"
end
