129 "fequal x y = fFalse \<or> fequal y z = fFalse \<or> fequal x z = fTrue" |
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" |
130 "fequal x y = fFalse \<or> fequal (f x) (f y) = fTrue" |
131 unfolding fFalse_def fTrue_def fequal_def by auto |
131 unfolding fFalse_def fTrue_def fequal_def by auto |
132 |
132 |
133 |
133 |
134 subsection \<open>Waldmeister helpers\<close> |
|
135 |
|
136 (* Has all needed simplification lemmas for logic. *) |
|
137 lemma boolean_equality: "(P \<longleftrightarrow> P) = True" |
|
138 by simp |
|
139 |
|
140 lemma boolean_comm: "(P \<longleftrightarrow> Q) = (Q \<longleftrightarrow> P)" |
|
141 by auto |
|
142 |
|
143 lemmas 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 |
|
147 subsection \<open>Basic connection between ATPs and HOL\<close> |
134 subsection \<open>Basic connection between ATPs and HOL\<close> |
148 |
135 |
149 ML_file \<open>Tools/lambda_lifting.ML\<close> |
136 ML_file \<open>Tools/lambda_lifting.ML\<close> |
150 ML_file \<open>Tools/monomorph.ML\<close> |
137 ML_file \<open>Tools/monomorph.ML\<close> |
151 ML_file \<open>Tools/ATP/atp_problem_generate.ML\<close> |
138 ML_file \<open>Tools/ATP/atp_problem_generate.ML\<close> |
152 ML_file \<open>Tools/ATP/atp_proof_reconstruct.ML\<close> |
139 ML_file \<open>Tools/ATP/atp_proof_reconstruct.ML\<close> |
153 ML_file \<open>Tools/ATP/atp_systems.ML\<close> |
140 ML_file \<open>Tools/ATP/atp_systems.ML\<close> |
154 ML_file \<open>Tools/ATP/atp_waldmeister.ML\<close> |
|
155 |
|
156 hide_fact (open) waldmeister_fol boolean_equality boolean_comm |
|
157 |
141 |
158 end |
142 end |