# Theory ATP

Up to index of Isabelle/HOL-Proofs

theory ATP
imports Meson
`(*  Title:      HOL/ATP.thy    Author:     Fabian Immler, TU Muenchen    Author:     Jasmin Blanchette, TU Muenchen*)header {* Automatic Theorem Provers (ATPs) *}theory ATPimports MesonbeginML_file "Tools/lambda_lifting.ML"ML_file "Tools/monomorph.ML"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 [no_atp]:"fFalse <-> False"definition fTrue :: bool where [no_atp]:"fTrue <-> True"definition fNot :: "bool => bool" where [no_atp]:"fNot P <-> ¬ P"definition fComp :: "('a => bool) => 'a => bool" where [no_atp]:"fComp P = (λx. ¬ P x)"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"lemma fTrue_ne_fFalse: "fFalse ≠ fTrue"unfolding fFalse_def fTrue_def by simplemma fNot_table:"fNot fFalse = fTrue""fNot fTrue = fFalse"unfolding fFalse_def fTrue_def fNot_def by autolemma fconj_table:"fconj fFalse P = fFalse""fconj P fFalse = fFalse""fconj fTrue fTrue = fTrue"unfolding fFalse_def fTrue_def fconj_def by autolemma fdisj_table:"fdisj fTrue P = fTrue""fdisj P fTrue = fTrue""fdisj fFalse fFalse = fFalse"unfolding fFalse_def fTrue_def fdisj_def by autolemma fimplies_table:"fimplies P fTrue = fTrue""fimplies fFalse P = fTrue""fimplies fTrue fFalse = fFalse"unfolding fFalse_def fTrue_def fimplies_def by autolemma fequal_table:"fequal x x = fTrue""x = y ∨ fequal x y = fFalse"unfolding fFalse_def fTrue_def fequal_def by autolemma fAll_table:"Ex (fComp P) ∨ fAll P = fTrue""All P ∨ fAll P = fFalse"unfolding fFalse_def fTrue_def fComp_def fAll_def by autolemma fEx_table:"All (fComp P) ∨ fEx P = fTrue""Ex P ∨ fEx P = fFalse"unfolding fFalse_def fTrue_def fComp_def fEx_def by autolemma fNot_law:"fNot P ≠ P"unfolding fNot_def by autolemma 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 autolemma 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 autolemma 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 autolemma 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 autolemma fAll_law:"fNot (fAll R) <-> fEx (fComp R)"unfolding fNot_def fComp_def fAll_def fEx_def by autolemma fEx_law:"fNot (fEx R) <-> fAll (fComp R)"unfolding fNot_def fComp_def fAll_def fEx_def by autosubsection {* Setup *}ML_file "Tools/ATP/atp_problem_generate.ML"ML_file "Tools/ATP/atp_proof_reconstruct.ML"ML_file "Tools/ATP/atp_systems.ML"setup ATP_Systems.setupend`