Theory ATP

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

section ‹Automatic Theorem Provers (ATPs)›

theory ATP
  imports Meson
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"
ML_file "Tools/ATP/atp_satallax.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)"

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


subsection ‹Waldmeister helpers›

(* Has all needed simplification lemmas for logic. *)
lemma boolean_equality: "(P ⟷ P) = True"
  by simp

lemma boolean_comm: "(P ⟷ Q) = (Q ⟷ P)"
  by auto

lemmas waldmeister_fol = boolean_equality boolean_comm
  simp_thms(1-5,7-8,11-25,27-33) disj_comms disj_assoc conj_comms conj_assoc


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"
ML_file "Tools/ATP/atp_systems.ML"
ML_file "Tools/ATP/atp_waldmeister.ML"

hide_fact (open) waldmeister_fol boolean_equality boolean_comm

end