src/HOL/ATP.thy
 author steckerm Sat Sep 20 10:44:24 2014 +0200 (2014-09-20) changeset 58406 539cc471186f parent 58142 d6a2e3567f95 child 58407 111d801b5d5d permissions -rw-r--r--
Minor fixes in ATP_Waldmeister
1 (*  Title:      HOL/ATP.thy
2     Author:     Fabian Immler, TU Muenchen
3     Author:     Jasmin Blanchette, TU Muenchen
4 *)
6 header {* Automatic Theorem Provers (ATPs) *}
8 theory ATP
9 imports Meson
10 begin
12 subsection {* ATP problems and proofs *}
14 ML_file "Tools/ATP/atp_util.ML"
15 ML_file "Tools/ATP/atp_problem.ML"
16 ML_file "Tools/ATP/atp_proof.ML"
17 ML_file "Tools/ATP/atp_proof_redirect.ML"
18 ML_file "Tools/ATP/atp_satallax.ML"
21 subsection {* Higher-order reasoning helpers *}
23 definition fFalse :: bool where
24 "fFalse \<longleftrightarrow> False"
26 definition fTrue :: bool where
27 "fTrue \<longleftrightarrow> True"
29 definition fNot :: "bool \<Rightarrow> bool" where
30 "fNot P \<longleftrightarrow> \<not> P"
32 definition fComp :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" where
33 "fComp P = (\<lambda>x. \<not> P x)"
35 definition fconj :: "bool \<Rightarrow> bool \<Rightarrow> bool" where
36 "fconj P Q \<longleftrightarrow> P \<and> Q"
38 definition fdisj :: "bool \<Rightarrow> bool \<Rightarrow> bool" where
39 "fdisj P Q \<longleftrightarrow> P \<or> Q"
41 definition fimplies :: "bool \<Rightarrow> bool \<Rightarrow> bool" where
42 "fimplies P Q \<longleftrightarrow> (P \<longrightarrow> Q)"
44 definition fAll :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where
45 "fAll P \<longleftrightarrow> All P"
47 definition fEx :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where
48 "fEx P \<longleftrightarrow> Ex P"
50 definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where
51 "fequal x y \<longleftrightarrow> (x = y)"
53 lemma fTrue_ne_fFalse: "fFalse \<noteq> fTrue"
54 unfolding fFalse_def fTrue_def by simp
56 lemma fNot_table:
57 "fNot fFalse = fTrue"
58 "fNot fTrue = fFalse"
59 unfolding fFalse_def fTrue_def fNot_def by auto
61 lemma fconj_table:
62 "fconj fFalse P = fFalse"
63 "fconj P fFalse = fFalse"
64 "fconj fTrue fTrue = fTrue"
65 unfolding fFalse_def fTrue_def fconj_def by auto
67 lemma fdisj_table:
68 "fdisj fTrue P = fTrue"
69 "fdisj P fTrue = fTrue"
70 "fdisj fFalse fFalse = fFalse"
71 unfolding fFalse_def fTrue_def fdisj_def by auto
73 lemma fimplies_table:
74 "fimplies P fTrue = fTrue"
75 "fimplies fFalse P = fTrue"
76 "fimplies fTrue fFalse = fFalse"
77 unfolding fFalse_def fTrue_def fimplies_def by auto
79 lemma fAll_table:
80 "Ex (fComp P) \<or> fAll P = fTrue"
81 "All P \<or> fAll P = fFalse"
82 unfolding fFalse_def fTrue_def fComp_def fAll_def by auto
84 lemma fEx_table:
85 "All (fComp P) \<or> fEx P = fTrue"
86 "Ex P \<or> fEx P = fFalse"
87 unfolding fFalse_def fTrue_def fComp_def fEx_def by auto
89 lemma fequal_table:
90 "fequal x x = fTrue"
91 "x = y \<or> fequal x y = fFalse"
92 unfolding fFalse_def fTrue_def fequal_def by auto
94 lemma fNot_law:
95 "fNot P \<noteq> P"
96 unfolding fNot_def by auto
98 lemma fComp_law:
99 "fComp P x \<longleftrightarrow> \<not> P x"
100 unfolding fComp_def ..
102 lemma 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)"
106 unfolding fNot_def fconj_def fdisj_def by auto
108 lemma 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)"
112 unfolding fNot_def fconj_def fdisj_def by auto
114 lemma fimplies_laws:
115 "fimplies P Q \<longleftrightarrow> fdisj (\<not> P) Q"
116 "fNot (fimplies P Q) \<longleftrightarrow> fconj P (fNot Q)"
117 unfolding fNot_def fconj_def fdisj_def fimplies_def by auto
119 lemma fAll_law:
120 "fNot (fAll R) \<longleftrightarrow> fEx (fComp R)"
121 unfolding fNot_def fComp_def fAll_def fEx_def by auto
123 lemma fEx_law:
124 "fNot (fEx R) \<longleftrightarrow> fAll (fComp R)"
125 unfolding fNot_def fComp_def fAll_def fEx_def by auto
127 lemma 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"
131 unfolding fFalse_def fTrue_def fequal_def by auto
134 subsection {* Waldmeister helpers *}
136 (* Has all needed simplification lemmas for logic. *)
137 lemma boolean_equality: "(P \<longleftrightarrow> P) = True"
138   by simp
140 lemma boolean_comm: "(P \<longleftrightarrow> Q) = (Q \<longleftrightarrow> P)"
141   by metis
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
147 subsection {* Basic connection between ATPs and HOL *}
149 ML_file "Tools/lambda_lifting.ML"
150 ML_file "Tools/monomorph.ML"
151 ML_file "Tools/ATP/atp_problem_generate.ML"
152 ML_file "Tools/ATP/atp_proof_reconstruct.ML"
153 ML_file "Tools/ATP/atp_systems.ML"
154 ML_file "Tools/ATP/atp_waldmeister.ML"
156 hide_fact (open) waldmeister_fol boolean_equality boolean_comm
158 end