header {* Automatic Theorem Provers (ATPs) *}
theory ATP
imports Meson
begin
ML_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 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 fequal_table:
"fequal x x = fTrue"
"x = y ∨ fequal x y = fFalse"
unfolding fFalse_def fTrue_def fequal_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 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 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 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
subsection {* 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.setup
end