(* 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