(* Title: Metric_Arith.thy
Author: Maximilian Schäffeler (port from HOL Light)
*)
chapter \<open>Functional Analysis\<close>
section\<^marker>\<open>tag unimportant\<close> \<open>A decision procedure for metric spaces\<close>
theory Metric_Arith
imports HOL.Real_Vector_Spaces
begin
text\<^marker>\<open>tag unimportant\<close> \<open>
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 \<open>Argo\<close> solver as backend.
\<close>
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: \<open>finite s\<close>)
moreover have "\dist x y - dist y y\ \ f ` s"
by (metis \<open>y \<in> s\<close> f_def imageI)
ultimately show ?thesis
using le_cSup_finite by simp
qed
also have "Sup (f ` s) \ dist x y"
using \<open>x \<in> s\<close> 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 = \<open>
Scan.succeed (SIMPLE_METHOD' o MetricArith.metric_arith_tac)
\<close> "prove simple linear statements in metric spaces (\<forall>\<exists>\<^sub>p fragment)"
end
¤ Dauer der Verarbeitung: 0.16 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
