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 ‹Automatic Theorem Provers (ATPs)›

theory ATP
  imports Meson Hilbert_Choice
begin

subsection ‹ATP problems and proofs›

ML_file ‹Tools/ATP/atp_util.ML›
ML_file ‹Tools/ATP/atp_problem.ML›
ML_file ‹Tools/ATP/atp_proof.ML›
ML_file ‹Tools/ATP/atp_proof_redirect.ML›


subsection ‹Higher-order reasoning helpers›

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 ‹
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.›

subsection ‹Basic connection between ATPs and HOL›

ML_file ‹Tools/lambda_lifting.ML›
ML_file ‹Tools/monomorph.ML›
ML_file ‹Tools/ATP/atp_problem_generate.ML›
ML_file ‹Tools/ATP/atp_proof_reconstruct.ML›

end