2 Author: Fabian Immler, TU Muenchen
3 Author: Jasmin Blanchette, TU Muenchen
6 header {* Automatic Theorem Provers (ATPs) *}
10 uses "Tools/lambda_lifting.ML"
12 "Tools/ATP/atp_util.ML"
13 "Tools/ATP/atp_problem.ML"
14 "Tools/ATP/atp_proof.ML"
15 "Tools/ATP/atp_proof_redirect.ML"
16 ("Tools/ATP/atp_problem_generate.ML")
17 ("Tools/ATP/atp_proof_reconstruct.ML")
18 ("Tools/ATP/atp_systems.ML")
21 subsection {* Higher-order reasoning helpers *}
23 definition fFalse :: bool where [no_atp]:
24 "fFalse \<longleftrightarrow> False"
26 definition fTrue :: bool where [no_atp]:
27 "fTrue \<longleftrightarrow> True"
29 definition fNot :: "bool \<Rightarrow> bool" where [no_atp]:
30 "fNot P \<longleftrightarrow> \<not> P"
32 definition fconj :: "bool \<Rightarrow> bool \<Rightarrow> bool" where [no_atp]:
33 "fconj P Q \<longleftrightarrow> P \<and> Q"
35 definition fdisj :: "bool \<Rightarrow> bool \<Rightarrow> bool" where [no_atp]:
36 "fdisj P Q \<longleftrightarrow> P \<or> Q"
38 definition fimplies :: "bool \<Rightarrow> bool \<Rightarrow> bool" where [no_atp]:
39 "fimplies P Q \<longleftrightarrow> (P \<longrightarrow> Q)"
41 definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where [no_atp]:
42 "fequal x y \<longleftrightarrow> (x = y)"
44 definition fAll :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where [no_atp]:
45 "fAll P \<longleftrightarrow> All P"
47 definition fEx :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where [no_atp]:
48 "fEx P \<longleftrightarrow> Ex P"
50 subsection {* Setup *}
52 use "Tools/ATP/atp_problem_generate.ML"
53 use "Tools/ATP/atp_proof_reconstruct.ML"
54 use "Tools/ATP/atp_systems.ML"
56 setup ATP_Systems.setup