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