blanchet@39951: (*  Title:      HOL/ATP.thy
blanchet@39951:     Author:     Fabian Immler, TU Muenchen
blanchet@39951:     Author:     Jasmin Blanchette, TU Muenchen
blanchet@39951: *)
blanchet@39951: 
blanchet@39958: header {* Automatic Theorem Provers (ATPs) *}
blanchet@39951: 
blanchet@39951: theory ATP
fleury@57714: imports Meson
blanchet@39951: begin
blanchet@39951: 
blanchet@57263: subsection {* ATP problems and proofs *}
blanchet@57263: 
wenzelm@48891: ML_file "Tools/ATP/atp_util.ML"
wenzelm@48891: ML_file "Tools/ATP/atp_problem.ML"
wenzelm@48891: ML_file "Tools/ATP/atp_proof.ML"
wenzelm@48891: ML_file "Tools/ATP/atp_proof_redirect.ML"
fleury@57707: ML_file "Tools/ATP/atp_satallax.ML"
fleury@57707: 
wenzelm@48891: 
blanchet@43085: subsection {* Higher-order reasoning helpers *}
blanchet@43085: 
blanchet@54148: definition fFalse :: bool where
blanchet@43085: "fFalse \<longleftrightarrow> False"
blanchet@43085: 
blanchet@54148: definition fTrue :: bool where
blanchet@43085: "fTrue \<longleftrightarrow> True"
blanchet@43085: 
blanchet@54148: definition fNot :: "bool \<Rightarrow> bool" where
blanchet@43085: "fNot P \<longleftrightarrow> \<not> P"
blanchet@43085: 
blanchet@54148: definition fComp :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" where
blanchet@47946: "fComp P = (\<lambda>x. \<not> P x)"
blanchet@47946: 
blanchet@54148: definition fconj :: "bool \<Rightarrow> bool \<Rightarrow> bool" where
blanchet@43085: "fconj P Q \<longleftrightarrow> P \<and> Q"
blanchet@43085: 
blanchet@54148: definition fdisj :: "bool \<Rightarrow> bool \<Rightarrow> bool" where
blanchet@43085: "fdisj P Q \<longleftrightarrow> P \<or> Q"
blanchet@43085: 
blanchet@54148: definition fimplies :: "bool \<Rightarrow> bool \<Rightarrow> bool" where
blanchet@43085: "fimplies P Q \<longleftrightarrow> (P \<longrightarrow> Q)"
blanchet@43085: 
blanchet@54148: definition fAll :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where
nik@43678: "fAll P \<longleftrightarrow> All P"
nik@43678: 
blanchet@54148: definition fEx :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where
nik@43678: "fEx P \<longleftrightarrow> Ex P"
blanchet@43085: 
blanchet@56946: definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where
blanchet@56946: "fequal x y \<longleftrightarrow> (x = y)"
blanchet@56946: 
blanchet@47946: lemma fTrue_ne_fFalse: "fFalse \<noteq> fTrue"
blanchet@47946: unfolding fFalse_def fTrue_def by simp
blanchet@47946: 
blanchet@47946: lemma fNot_table:
blanchet@47946: "fNot fFalse = fTrue"
blanchet@47946: "fNot fTrue = fFalse"
blanchet@47946: unfolding fFalse_def fTrue_def fNot_def by auto
blanchet@47946: 
blanchet@47946: lemma fconj_table:
blanchet@47946: "fconj fFalse P = fFalse"
blanchet@47946: "fconj P fFalse = fFalse"
blanchet@47946: "fconj fTrue fTrue = fTrue"
blanchet@47946: unfolding fFalse_def fTrue_def fconj_def by auto
blanchet@47946: 
blanchet@47946: lemma fdisj_table:
blanchet@47946: "fdisj fTrue P = fTrue"
blanchet@47946: "fdisj P fTrue = fTrue"
blanchet@47946: "fdisj fFalse fFalse = fFalse"
blanchet@47946: unfolding fFalse_def fTrue_def fdisj_def by auto
blanchet@47946: 
blanchet@47946: lemma fimplies_table:
blanchet@47946: "fimplies P fTrue = fTrue"
blanchet@47946: "fimplies fFalse P = fTrue"
blanchet@47946: "fimplies fTrue fFalse = fFalse"
blanchet@47946: unfolding fFalse_def fTrue_def fimplies_def by auto
blanchet@47946: 
blanchet@47946: lemma fAll_table:
blanchet@47946: "Ex (fComp P) \<or> fAll P = fTrue"
blanchet@47946: "All P \<or> fAll P = fFalse"
blanchet@47946: unfolding fFalse_def fTrue_def fComp_def fAll_def by auto
blanchet@47946: 
blanchet@47946: lemma fEx_table:
blanchet@47946: "All (fComp P) \<or> fEx P = fTrue"
blanchet@47946: "Ex P \<or> fEx P = fFalse"
blanchet@47946: unfolding fFalse_def fTrue_def fComp_def fEx_def by auto
blanchet@47946: 
blanchet@56946: lemma fequal_table:
blanchet@56946: "fequal x x = fTrue"
blanchet@56946: "x = y \<or> fequal x y = fFalse"
blanchet@56946: unfolding fFalse_def fTrue_def fequal_def by auto
blanchet@56946: 
blanchet@47946: lemma fNot_law:
blanchet@47946: "fNot P \<noteq> P"
blanchet@47946: unfolding fNot_def by auto
blanchet@47946: 
blanchet@47946: lemma fComp_law:
blanchet@47946: "fComp P x \<longleftrightarrow> \<not> P x"
blanchet@47946: unfolding fComp_def ..
blanchet@47946: 
blanchet@47946: lemma fconj_laws:
blanchet@47946: "fconj P P \<longleftrightarrow> P"
blanchet@47946: "fconj P Q \<longleftrightarrow> fconj Q P"
blanchet@47946: "fNot (fconj P Q) \<longleftrightarrow> fdisj (fNot P) (fNot Q)"
blanchet@47946: unfolding fNot_def fconj_def fdisj_def by auto
blanchet@47946: 
blanchet@47946: lemma fdisj_laws:
blanchet@47946: "fdisj P P \<longleftrightarrow> P"
blanchet@47946: "fdisj P Q \<longleftrightarrow> fdisj Q P"
blanchet@47946: "fNot (fdisj P Q) \<longleftrightarrow> fconj (fNot P) (fNot Q)"
blanchet@47946: unfolding fNot_def fconj_def fdisj_def by auto
blanchet@47946: 
blanchet@47946: lemma fimplies_laws:
blanchet@47946: "fimplies P Q \<longleftrightarrow> fdisj (\<not> P) Q"
blanchet@47946: "fNot (fimplies P Q) \<longleftrightarrow> fconj P (fNot Q)"
blanchet@47946: unfolding fNot_def fconj_def fdisj_def fimplies_def by auto
blanchet@47946: 
blanchet@47946: lemma fAll_law:
blanchet@47946: "fNot (fAll R) \<longleftrightarrow> fEx (fComp R)"
blanchet@47946: unfolding fNot_def fComp_def fAll_def fEx_def by auto
blanchet@47946: 
blanchet@47946: lemma fEx_law:
blanchet@47946: "fNot (fEx R) \<longleftrightarrow> fAll (fComp R)"
blanchet@47946: unfolding fNot_def fComp_def fAll_def fEx_def by auto
blanchet@47946: 
blanchet@56946: lemma fequal_laws:
blanchet@56946: "fequal x y = fequal y x"
blanchet@56946: "fequal x y = fFalse \<or> fequal y z = fFalse \<or> fequal x z = fTrue"
blanchet@56946: "fequal x y = fFalse \<or> fequal (f x) (f y) = fTrue"
blanchet@56946: unfolding fFalse_def fTrue_def fequal_def by auto
blanchet@56946: 
blanchet@56946: 
blanchet@57262: subsection {* Waldmeister helpers *}
blanchet@57262: 
steckerm@58406: (* Has all needed simplification lemmas for logic. *)
steckerm@58406: lemma boolean_equality: "(P \<longleftrightarrow> P) = True"
steckerm@58406:   by simp
steckerm@58406: 
steckerm@58406: lemma boolean_comm: "(P \<longleftrightarrow> Q) = (Q \<longleftrightarrow> P)"
steckerm@58407:   by auto
steckerm@58406: 
steckerm@58406: lemmas waldmeister_fol = boolean_equality boolean_comm
steckerm@58406:   simp_thms(1-5,7-8,11-25,27-33) disj_comms disj_assoc conj_comms conj_assoc
blanchet@57262: 
blanchet@57262: 
blanchet@57263: subsection {* Basic connection between ATPs and HOL *}
blanchet@43085: 
blanchet@57263: ML_file "Tools/lambda_lifting.ML"
blanchet@57263: ML_file "Tools/monomorph.ML"
wenzelm@48891: ML_file "Tools/ATP/atp_problem_generate.ML"
wenzelm@48891: ML_file "Tools/ATP/atp_proof_reconstruct.ML"
wenzelm@48891: ML_file "Tools/ATP/atp_systems.ML"
blanchet@57262: ML_file "Tools/ATP/atp_waldmeister.ML"
blanchet@43085: 
steckerm@58406: hide_fact (open) waldmeister_fol boolean_equality boolean_comm
blanchet@39951: 
blanchet@39951: end