|
1 (* Title: HOL/Meson.thy |
|
2 Author: Lawrence C Paulson, Tobias Nipkow |
|
3 Copyright 2001 University of Cambridge |
|
4 *) |
|
5 |
|
6 header {* MESON Proof Procedure (Model Elimination) *} |
|
7 |
|
8 theory Meson |
|
9 imports Nat |
|
10 uses ("Tools/Meson/meson.ML") |
|
11 ("Tools/Meson/meson_clausify.ML") |
|
12 begin |
|
13 |
|
14 section {* Negation Normal Form *} |
|
15 |
|
16 text {* de Morgan laws *} |
|
17 |
|
18 lemma meson_not_conjD: "~(P&Q) ==> ~P | ~Q" |
|
19 and meson_not_disjD: "~(P|Q) ==> ~P & ~Q" |
|
20 and meson_not_notD: "~~P ==> P" |
|
21 and meson_not_allD: "!!P. ~(\<forall>x. P(x)) ==> \<exists>x. ~P(x)" |
|
22 and meson_not_exD: "!!P. ~(\<exists>x. P(x)) ==> \<forall>x. ~P(x)" |
|
23 by fast+ |
|
24 |
|
25 text {* Removal of @{text "-->"} and @{text "<->"} (positive and |
|
26 negative occurrences) *} |
|
27 |
|
28 lemma meson_imp_to_disjD: "P-->Q ==> ~P | Q" |
|
29 and meson_not_impD: "~(P-->Q) ==> P & ~Q" |
|
30 and meson_iff_to_disjD: "P=Q ==> (~P | Q) & (~Q | P)" |
|
31 and meson_not_iffD: "~(P=Q) ==> (P | Q) & (~P | ~Q)" |
|
32 -- {* Much more efficient than @{prop "(P & ~Q) | (Q & ~P)"} for computing CNF *} |
|
33 and meson_not_refl_disj_D: "x ~= x | P ==> P" |
|
34 by fast+ |
|
35 |
|
36 |
|
37 section {* Pulling out the existential quantifiers *} |
|
38 |
|
39 text {* Conjunction *} |
|
40 |
|
41 lemma meson_conj_exD1: "!!P Q. (\<exists>x. P(x)) & Q ==> \<exists>x. P(x) & Q" |
|
42 and meson_conj_exD2: "!!P Q. P & (\<exists>x. Q(x)) ==> \<exists>x. P & Q(x)" |
|
43 by fast+ |
|
44 |
|
45 |
|
46 text {* Disjunction *} |
|
47 |
|
48 lemma meson_disj_exD: "!!P Q. (\<exists>x. P(x)) | (\<exists>x. Q(x)) ==> \<exists>x. P(x) | Q(x)" |
|
49 -- {* DO NOT USE with forall-Skolemization: makes fewer schematic variables!! *} |
|
50 -- {* With ex-Skolemization, makes fewer Skolem constants *} |
|
51 and meson_disj_exD1: "!!P Q. (\<exists>x. P(x)) | Q ==> \<exists>x. P(x) | Q" |
|
52 and meson_disj_exD2: "!!P Q. P | (\<exists>x. Q(x)) ==> \<exists>x. P | Q(x)" |
|
53 by fast+ |
|
54 |
|
55 lemma meson_disj_assoc: "(P|Q)|R ==> P|(Q|R)" |
|
56 and meson_disj_comm: "P|Q ==> Q|P" |
|
57 and meson_disj_FalseD1: "False|P ==> P" |
|
58 and meson_disj_FalseD2: "P|False ==> P" |
|
59 by fast+ |
|
60 |
|
61 |
|
62 text{* Generation of contrapositives *} |
|
63 |
|
64 text{*Inserts negated disjunct after removing the negation; P is a literal. |
|
65 Model elimination requires assuming the negation of every attempted subgoal, |
|
66 hence the negated disjuncts.*} |
|
67 lemma make_neg_rule: "~P|Q ==> ((~P==>P) ==> Q)" |
|
68 by blast |
|
69 |
|
70 text{*Version for Plaisted's "Postive refinement" of the Meson procedure*} |
|
71 lemma make_refined_neg_rule: "~P|Q ==> (P ==> Q)" |
|
72 by blast |
|
73 |
|
74 text{*@{term P} should be a literal*} |
|
75 lemma make_pos_rule: "P|Q ==> ((P==>~P) ==> Q)" |
|
76 by blast |
|
77 |
|
78 text{*Versions of @{text make_neg_rule} and @{text make_pos_rule} that don't |
|
79 insert new assumptions, for ordinary resolution.*} |
|
80 |
|
81 lemmas make_neg_rule' = make_refined_neg_rule |
|
82 |
|
83 lemma make_pos_rule': "[|P|Q; ~P|] ==> Q" |
|
84 by blast |
|
85 |
|
86 text{* Generation of a goal clause -- put away the final literal *} |
|
87 |
|
88 lemma make_neg_goal: "~P ==> ((~P==>P) ==> False)" |
|
89 by blast |
|
90 |
|
91 lemma make_pos_goal: "P ==> ((P==>~P) ==> False)" |
|
92 by blast |
|
93 |
|
94 |
|
95 section {* Lemmas for Forward Proof *} |
|
96 |
|
97 text{*There is a similarity to congruence rules*} |
|
98 |
|
99 (*NOTE: could handle conjunctions (faster?) by |
|
100 nf(th RS conjunct2) RS (nf(th RS conjunct1) RS conjI) *) |
|
101 lemma conj_forward: "[| P'&Q'; P' ==> P; Q' ==> Q |] ==> P&Q" |
|
102 by blast |
|
103 |
|
104 lemma disj_forward: "[| P'|Q'; P' ==> P; Q' ==> Q |] ==> P|Q" |
|
105 by blast |
|
106 |
|
107 (*Version of @{text disj_forward} for removal of duplicate literals*) |
|
108 lemma disj_forward2: |
|
109 "[| P'|Q'; P' ==> P; [| Q'; P==>False |] ==> Q |] ==> P|Q" |
|
110 apply blast |
|
111 done |
|
112 |
|
113 lemma all_forward: "[| \<forall>x. P'(x); !!x. P'(x) ==> P(x) |] ==> \<forall>x. P(x)" |
|
114 by blast |
|
115 |
|
116 lemma ex_forward: "[| \<exists>x. P'(x); !!x. P'(x) ==> P(x) |] ==> \<exists>x. P(x)" |
|
117 by blast |
|
118 |
|
119 |
|
120 section {* Clausification helper *} |
|
121 |
|
122 lemma TruepropI: "P \<equiv> Q \<Longrightarrow> Trueprop P \<equiv> Trueprop Q" |
|
123 by simp |
|
124 |
|
125 |
|
126 text{* Combinator translation helpers *} |
|
127 |
|
128 definition COMBI :: "'a \<Rightarrow> 'a" where |
|
129 [no_atp]: "COMBI P = P" |
|
130 |
|
131 definition COMBK :: "'a \<Rightarrow> 'b \<Rightarrow> 'a" where |
|
132 [no_atp]: "COMBK P Q = P" |
|
133 |
|
134 definition COMBB :: "('b => 'c) \<Rightarrow> ('a => 'b) \<Rightarrow> 'a \<Rightarrow> 'c" where [no_atp]: |
|
135 "COMBB P Q R = P (Q R)" |
|
136 |
|
137 definition COMBC :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c" where |
|
138 [no_atp]: "COMBC P Q R = P R Q" |
|
139 |
|
140 definition COMBS :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c" where |
|
141 [no_atp]: "COMBS P Q R = P R (Q R)" |
|
142 |
|
143 lemma abs_S [no_atp]: "\<lambda>x. (f x) (g x) \<equiv> COMBS f g" |
|
144 apply (rule eq_reflection) |
|
145 apply (rule ext) |
|
146 apply (simp add: COMBS_def) |
|
147 done |
|
148 |
|
149 lemma abs_I [no_atp]: "\<lambda>x. x \<equiv> COMBI" |
|
150 apply (rule eq_reflection) |
|
151 apply (rule ext) |
|
152 apply (simp add: COMBI_def) |
|
153 done |
|
154 |
|
155 lemma abs_K [no_atp]: "\<lambda>x. y \<equiv> COMBK y" |
|
156 apply (rule eq_reflection) |
|
157 apply (rule ext) |
|
158 apply (simp add: COMBK_def) |
|
159 done |
|
160 |
|
161 lemma abs_B [no_atp]: "\<lambda>x. a (g x) \<equiv> COMBB a g" |
|
162 apply (rule eq_reflection) |
|
163 apply (rule ext) |
|
164 apply (simp add: COMBB_def) |
|
165 done |
|
166 |
|
167 lemma abs_C [no_atp]: "\<lambda>x. (f x) b \<equiv> COMBC f b" |
|
168 apply (rule eq_reflection) |
|
169 apply (rule ext) |
|
170 apply (simp add: COMBC_def) |
|
171 done |
|
172 |
|
173 |
|
174 section {* Skolemization helpers *} |
|
175 |
|
176 definition skolem :: "'a \<Rightarrow> 'a" where |
|
177 [no_atp]: "skolem = (\<lambda>x. x)" |
|
178 |
|
179 lemma skolem_COMBK_iff: "P \<longleftrightarrow> skolem (COMBK P (i\<Colon>nat))" |
|
180 unfolding skolem_def COMBK_def by (rule refl) |
|
181 |
|
182 lemmas skolem_COMBK_I = iffD1 [OF skolem_COMBK_iff] |
|
183 lemmas skolem_COMBK_D = iffD2 [OF skolem_COMBK_iff] |
|
184 |
|
185 |
|
186 section {* Meson package *} |
|
187 |
|
188 ML {* |
|
189 structure Meson_Choices = Named_Thms |
|
190 ( |
|
191 val name = "meson_choice" |
|
192 val description = "choice axioms for MESON's (and Metis's) skolemizer" |
|
193 ) |
|
194 *} |
|
195 |
|
196 use "Tools/Meson/meson.ML" |
|
197 use "Tools/Meson/meson_clausify.ML" |
|
198 |
|
199 setup {* |
|
200 Meson_Choices.setup |
|
201 #> Meson.setup |
|
202 #> Meson_Clausify.setup |
|
203 *} |
|
204 |
|
205 end |