Quelle Metric_Arith.thy Sprache: Isabelle

(*  Title:      HOL/Analysis/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>\<open>"DBLP:journals/jar/Maggesi18"\<close> 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 \<open>metric_arith.ML\<close>

method_setup metric = \<open>
  Scan.succeed (SIMPLE_METHOD' o Metric_Arith.metric_arith_tac)
\<close> "prove simple linear statements in metric spaces (\<forall>\<exists>\<^sub>p fragment)"

end

quality97%

¤ Dauer der Verarbeitung: 0.2 Sekunden (vorverarbeitet) ¤

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.

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.