1(* Title: HOL/ATP.thy 2 Author: Fabian Immler, TU Muenchen 3 Author: Jasmin Blanchette, TU Muenchen 4*) 5 6section \<open>Automatic Theorem Provers (ATPs)\<close> 7 8theory ATP 9 imports Meson 10begin 11 12subsection \<open>ATP problems and proofs\<close> 13 14ML_file "Tools/ATP/atp_util.ML" 15ML_file "Tools/ATP/atp_problem.ML" 16ML_file "Tools/ATP/atp_proof.ML" 17ML_file "Tools/ATP/atp_proof_redirect.ML" 18ML_file "Tools/ATP/atp_satallax.ML" 19 20 21subsection \<open>Higher-order reasoning helpers\<close> 22 23definition fFalse :: bool where 24"fFalse \<longleftrightarrow> False" 25 26definition fTrue :: bool where 27"fTrue \<longleftrightarrow> True" 28 29definition fNot :: "bool \<Rightarrow> bool" where 30"fNot P \<longleftrightarrow> \<not> P" 31 32definition fComp :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" where 33"fComp P = (\<lambda>x. \<not> P x)" 34 35definition fconj :: "bool \<Rightarrow> bool \<Rightarrow> bool" where 36"fconj P Q \<longleftrightarrow> P \<and> Q" 37 38definition fdisj :: "bool \<Rightarrow> bool \<Rightarrow> bool" where 39"fdisj P Q \<longleftrightarrow> P \<or> Q" 40 41definition fimplies :: "bool \<Rightarrow> bool \<Rightarrow> bool" where 42"fimplies P Q \<longleftrightarrow> (P \<longrightarrow> Q)" 43 44definition fAll :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where 45"fAll P \<longleftrightarrow> All P" 46 47definition fEx :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where 48"fEx P \<longleftrightarrow> Ex P" 49 50definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where 51"fequal x y \<longleftrightarrow> (x = y)" 52 53lemma fTrue_ne_fFalse: "fFalse \<noteq> fTrue" 54unfolding fFalse_def fTrue_def by simp 55 56lemma fNot_table: 57"fNot fFalse = fTrue" 58"fNot fTrue = fFalse" 59unfolding fFalse_def fTrue_def fNot_def by auto 60 61lemma fconj_table: 62"fconj fFalse P = fFalse" 63"fconj P fFalse = fFalse" 64"fconj fTrue fTrue = fTrue" 65unfolding fFalse_def fTrue_def fconj_def by auto 66 67lemma fdisj_table: 68"fdisj fTrue P = fTrue" 69"fdisj P fTrue = fTrue" 70"fdisj fFalse fFalse = fFalse" 71unfolding fFalse_def fTrue_def fdisj_def by auto 72 73lemma fimplies_table: 74"fimplies P fTrue = fTrue" 75"fimplies fFalse P = fTrue" 76"fimplies fTrue fFalse = fFalse" 77unfolding fFalse_def fTrue_def fimplies_def by auto 78 79lemma fAll_table: 80"Ex (fComp P) \<or> fAll P = fTrue" 81"All P \<or> fAll P = fFalse" 82unfolding fFalse_def fTrue_def fComp_def fAll_def by auto 83 84lemma fEx_table: 85"All (fComp P) \<or> fEx P = fTrue" 86"Ex P \<or> fEx P = fFalse" 87unfolding fFalse_def fTrue_def fComp_def fEx_def by auto 88 89lemma fequal_table: 90"fequal x x = fTrue" 91"x = y \<or> fequal x y = fFalse" 92unfolding fFalse_def fTrue_def fequal_def by auto 93 94lemma fNot_law: 95"fNot P \<noteq> P" 96unfolding fNot_def by auto 97 98lemma fComp_law: 99"fComp P x \<longleftrightarrow> \<not> P x" 100unfolding fComp_def .. 101 102lemma fconj_laws: 103"fconj P P \<longleftrightarrow> P" 104"fconj P Q \<longleftrightarrow> fconj Q P" 105"fNot (fconj P Q) \<longleftrightarrow> fdisj (fNot P) (fNot Q)" 106unfolding fNot_def fconj_def fdisj_def by auto 107 108lemma fdisj_laws: 109"fdisj P P \<longleftrightarrow> P" 110"fdisj P Q \<longleftrightarrow> fdisj Q P" 111"fNot (fdisj P Q) \<longleftrightarrow> fconj (fNot P) (fNot Q)" 112unfolding fNot_def fconj_def fdisj_def by auto 113 114lemma fimplies_laws: 115"fimplies P Q \<longleftrightarrow> fdisj (\<not> P) Q" 116"fNot (fimplies P Q) \<longleftrightarrow> fconj P (fNot Q)" 117unfolding fNot_def fconj_def fdisj_def fimplies_def by auto 118 119lemma fAll_law: 120"fNot (fAll R) \<longleftrightarrow> fEx (fComp R)" 121unfolding fNot_def fComp_def fAll_def fEx_def by auto 122 123lemma fEx_law: 124"fNot (fEx R) \<longleftrightarrow> fAll (fComp R)" 125unfolding fNot_def fComp_def fAll_def fEx_def by auto 126 127lemma fequal_laws: 128"fequal x y = fequal y x" 129"fequal x y = fFalse \<or> fequal y z = fFalse \<or> fequal x z = fTrue" 130"fequal x y = fFalse \<or> fequal (f x) (f y) = fTrue" 131unfolding fFalse_def fTrue_def fequal_def by auto 132 133 134subsection \<open>Waldmeister helpers\<close> 135 136(* Has all needed simplification lemmas for logic. *) 137lemma boolean_equality: "(P \<longleftrightarrow> P) = True" 138 by simp 139 140lemma boolean_comm: "(P \<longleftrightarrow> Q) = (Q \<longleftrightarrow> P)" 141 by auto 142 143lemmas waldmeister_fol = boolean_equality boolean_comm 144 simp_thms(1-5,7-8,11-25,27-33) disj_comms disj_assoc conj_comms conj_assoc 145 146 147subsection \<open>Basic connection between ATPs and HOL\<close> 148 149ML_file "Tools/lambda_lifting.ML" 150ML_file "Tools/monomorph.ML" 151ML_file "Tools/ATP/atp_problem_generate.ML" 152ML_file "Tools/ATP/atp_proof_reconstruct.ML" 153ML_file "Tools/ATP/atp_systems.ML" 154ML_file "Tools/ATP/atp_waldmeister.ML" 155 156hide_fact (open) waldmeister_fol boolean_equality boolean_comm 157 158end 159