Quelle ATP.thy Sprache: Isabelle

(*  Title:      HOL/ATP.thy
    Author:     Fabian Immler, TU Muenchen
    Author:     Jasmin Blanchette, TU Muenchen
    Author:     Martin Desharnais, UniBw Muenchen
*)

section \<open>Automatic Theorem Provers (ATPs)\<close>

theory ATP
  imports Meson Hilbert_Choice
begin

subsection \<open>ATP problems and proofs\<close>

ML_file \<open>Tools/ATP/atp_util.ML\<close>
ML_file \<open>Tools/ATP/atp_problem.ML\<close>
ML_file \<open>Tools/ATP/atp_proof.ML\<close>
ML_file \<open>Tools/ATP/atp_proof_redirect.ML\<close>

subsection \<open>Higher-order reasoning helpers\<close>

definition fFalse :: bool where
"fFalse \ False"

definition fTrue :: bool where
"fTrue \ True"

definition fNot :: "bool \ bool" where
"fNot P \ \ P"

definition fComp :: "('a \ bool) \ 'a \ bool" where
"fComp P = (\x. \ P x)"

definition fconj :: "bool \ bool \ bool" where
"fconj P Q \ P \ Q"

definition fdisj :: "bool \ bool \ bool" where
"fdisj P Q \ P \ Q"

definition fimplies :: "bool \ bool \ bool" where
"fimplies P Q \ (P \ Q)"

definition fAll :: "('a \ bool) \ bool" where
"fAll P \ All P"

definition fEx :: "('a \ bool) \ bool" where
"fEx P \ Ex P"

definition fequal :: "'a \ 'a \ bool" where
"fequal x y \ (x = y)"

definition fChoice :: "('a \ bool) \ 'a" where
  "fChoice \ Hilbert_Choice.Eps"

lemma fTrue_ne_fFalse: "fFalse \ fTrue"
unfolding fFalse_def fTrue_def by simp

lemma fNot_table:
"fNot fFalse = fTrue"
"fNot fTrue = fFalse"
unfolding fFalse_def fTrue_def fNot_def by auto

lemma fconj_table:
"fconj fFalse P = fFalse"
"fconj P fFalse = fFalse"
"fconj fTrue fTrue = fTrue"
unfolding fFalse_def fTrue_def fconj_def by auto

lemma fdisj_table:
"fdisj fTrue P = fTrue"
"fdisj P fTrue = fTrue"
"fdisj fFalse fFalse = fFalse"
unfolding fFalse_def fTrue_def fdisj_def by auto

lemma fimplies_table:
"fimplies P fTrue = fTrue"
"fimplies fFalse P = fTrue"
"fimplies fTrue fFalse = fFalse"
unfolding fFalse_def fTrue_def fimplies_def by auto

lemma fAll_table:
"Ex (fComp P) \ fAll P = fTrue"
"All P \ fAll P = fFalse"
unfolding fFalse_def fTrue_def fComp_def fAll_def by auto

lemma fEx_table:
"All (fComp P) \ fEx P = fTrue"
"Ex P \ fEx P = fFalse"
unfolding fFalse_def fTrue_def fComp_def fEx_def by auto

lemma fequal_table:
"fequal x x = fTrue"
"x = y \ fequal x y = fFalse"
unfolding fFalse_def fTrue_def fequal_def by auto

lemma fNot_law:
"fNot P \ P"
unfolding fNot_def by auto

lemma fComp_law:
"fComp P x \ \ P x"
unfolding fComp_def ..

lemma fconj_laws:
"fconj P P \ P"
"fconj P Q \ fconj Q P"
"fNot (fconj P Q) \ fdisj (fNot P) (fNot Q)"
unfolding fNot_def fconj_def fdisj_def by auto

lemma fdisj_laws:
"fdisj P P \ P"
"fdisj P Q \ fdisj Q P"
"fNot (fdisj P Q) \ fconj (fNot P) (fNot Q)"
unfolding fNot_def fconj_def fdisj_def by auto

lemma fimplies_laws:
"fimplies P Q \ fdisj (\ P) Q"
"fNot (fimplies P Q) \ fconj P (fNot Q)"
unfolding fNot_def fconj_def fdisj_def fimplies_def by auto

lemma fAll_law:
"fNot (fAll R) \ fEx (fComp R)"
unfolding fNot_def fComp_def fAll_def fEx_def by auto

lemma fEx_law:
"fNot (fEx R) \ fAll (fComp R)"
unfolding fNot_def fComp_def fAll_def fEx_def by auto

lemma fequal_laws:
"fequal x y = fequal y x"
"fequal x y = fFalse \ fequal y z = fFalse \ fequal x z = fTrue"
"fequal x y = fFalse \ fequal (f x) (f y) = fTrue"
unfolding fFalse_def fTrue_def fequal_def by auto

lemma fChoice_iff_Ex: "P (fChoice P) \ HOL.Ex P"
  unfolding fChoice_def
  by (fact some_eq_ex)

text \<open>
We use the @{const HOL.Ex} constant on the right-hand side of @{thm [source] fChoice_iff_Ex} because
we want to use the TPTP-native version if fChoice is introduced in a logic that supports FOOL.
In logics that don't support it, it gets replaced by fEx during processing.
Notice that we cannot use @{term "\x. P x"}, as existentials are not skolimized by the metis proof
method but @{term "Ex P"} is eta-expanded if FOOL is supported.\<close>

subsection \<open>Basic connection between ATPs and HOL\<close>

ML_file \<open>Tools/lambda_lifting.ML\<close>
ML_file \<open>Tools/monomorph.ML\<close>
ML_file \<open>Tools/ATP/atp_problem_generate.ML\<close>
ML_file \<open>Tools/ATP/atp_proof_reconstruct.ML\<close>

end

quality100%

¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.