Theory ATP

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

header {* Automatic Theorem Provers (ATPs) *}

theory ATP
imports Meson
uses "Tools/lambda_lifting.ML"
     "Tools/monomorph.ML"
     "Tools/ATP/atp_util.ML"
     "Tools/ATP/atp_problem.ML"
     "Tools/ATP/atp_proof.ML"
     "Tools/ATP/atp_proof_redirect.ML"
     ("Tools/ATP/atp_problem_generate.ML")
     ("Tools/ATP/atp_proof_reconstruct.ML")
     ("Tools/ATP/atp_systems.ML")
begin

subsection {* Higher-order reasoning helpers *}

definition fFalse :: bool where [no_atp]:
"fFalse <-> False"

definition fTrue :: bool where [no_atp]:
"fTrue <-> True"

definition fNot :: "bool => bool" where [no_atp]:
"fNot P <-> ¬ P"

definition fconj :: "bool => bool => bool" where [no_atp]:
"fconj P Q <-> P ∧ Q"

definition fdisj :: "bool => bool => bool" where [no_atp]:
"fdisj P Q <-> P ∨ Q"

definition fimplies :: "bool => bool => bool" where [no_atp]:
"fimplies P Q <-> (P --> Q)"

definition fequal :: "'a => 'a => bool" where [no_atp]:
"fequal x y <-> (x = y)"

definition fAll :: "('a => bool) => bool" where [no_atp]:
"fAll P <-> All P"

definition fEx :: "('a => bool) => bool" where [no_atp]:
"fEx P <-> Ex P"

subsection {* Setup *}

use "Tools/ATP/atp_problem_generate.ML"
use "Tools/ATP/atp_proof_reconstruct.ML"
use "Tools/ATP/atp_systems.ML"

setup ATP_Systems.setup

end