17618
|
1 |
(* Title: HOL/Tools/cnf_funcs.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Alwen Tiu, QSL Team, LORIA (http://qsl.loria.fr)
|
|
4 |
Copyright 2005
|
|
5 |
|
|
6 |
Description:
|
|
7 |
This file contains functions and tactics to transform a formula into
|
|
8 |
Conjunctive Normal Forms (CNF).
|
|
9 |
A formula in CNF is of the following form:
|
|
10 |
|
|
11 |
(x11 | x12 | .. x1m) & ... & (xm1 | xm2 | ... | xmn)
|
|
12 |
|
|
13 |
where each xij is a literal (i.e., positive or negative propositional
|
|
14 |
variables).
|
|
15 |
This kind of formula will simply be referred to as CNF.
|
|
16 |
A disjunction of literals is referred to as "clause".
|
|
17 |
|
|
18 |
For the purpose of SAT proof reconstruction, we also make use of another
|
|
19 |
representation of clauses, which we call the "raw clauses".
|
|
20 |
Raw clauses are of the form
|
|
21 |
|
|
22 |
(x1 ==> x2 ==> .. ==> xn ==> False)
|
|
23 |
|
|
24 |
where each xi is a literal. Note that the above raw clause corresponds
|
|
25 |
to the clause (x1' | ... | xn'), where each xi' is the negation normal
|
|
26 |
form of ~xi.
|
|
27 |
|
|
28 |
Notes for current revision:
|
|
29 |
- the "definitional CNF transformation" (anything with prefix cnfx_ )
|
|
30 |
introduces new literals of the form (lit_i) where i is an integer.
|
|
31 |
For these functions to work, it is necessary that no free variables
|
|
32 |
which names are of the form lit_i appears in the formula being
|
|
33 |
transformed.
|
|
34 |
*)
|
|
35 |
|
|
36 |
|
|
37 |
(***************************************************************************)
|
|
38 |
|
|
39 |
signature CNF =
|
|
40 |
sig
|
|
41 |
val cnf_tac : Tactical.tactic
|
|
42 |
val cnf_thin_tac : Tactical.tactic
|
|
43 |
val cnfx_thin_tac : Tactical.tactic
|
|
44 |
val cnf_concl_tac : Tactical.tactic
|
|
45 |
val weakening_tac : int -> Tactical.tactic
|
|
46 |
val mk_cnf_thm : Sign.sg -> Term.term -> Thm.thm
|
|
47 |
val mk_cnfx_thm : Sign.sg -> Term.term -> Thm.thm
|
|
48 |
val is_atm : Term.term -> bool
|
|
49 |
val is_lit : Term.term -> bool
|
|
50 |
val is_clause : Term.term -> bool
|
|
51 |
val is_raw_clause : Term.term -> bool
|
|
52 |
val cnf2raw_thm : Thm.thm -> Thm.thm
|
|
53 |
val cnf2raw_thms : Thm.thm list -> Thm.thm list
|
|
54 |
val cnf2prop : Thm.thm list -> (PropLogic.prop_formula * ((Term.term * int) list))
|
|
55 |
end
|
|
56 |
|
|
57 |
|
|
58 |
(***************************************************************************)
|
|
59 |
|
|
60 |
structure cnf : CNF =
|
|
61 |
struct
|
|
62 |
|
|
63 |
val cur_thy = the_context();
|
|
64 |
val mk_disj = HOLogic.mk_disj;
|
|
65 |
val mk_conj = HOLogic.mk_conj;
|
|
66 |
val mk_imp = HOLogic.mk_imp;
|
|
67 |
val Not = HOLogic.Not;
|
|
68 |
val false_const = HOLogic.false_const;
|
|
69 |
val true_const = HOLogic.true_const;
|
|
70 |
|
|
71 |
|
|
72 |
(* Index for new literals *)
|
|
73 |
val lit_id = ref 0;
|
|
74 |
|
|
75 |
fun thm_by_auto G =
|
|
76 |
prove_goal cur_thy G (fn prems => [cut_facts_tac prems 1, Auto_tac]);
|
|
77 |
|
|
78 |
(***************************************************************************)
|
|
79 |
|
|
80 |
|
|
81 |
val cnf_eq_id = thm_by_auto "(P :: bool) = P";
|
|
82 |
|
|
83 |
val cnf_eq_sym = thm_by_auto "(P :: bool) = Q ==> Q = P";
|
|
84 |
|
|
85 |
val cnf_not_true_false = thm_by_auto "~True = False";
|
|
86 |
|
|
87 |
val cnf_not_false_true = thm_by_auto "~False = True";
|
|
88 |
|
|
89 |
val cnf_imp2disj = thm_by_auto "(P --> Q) = (~P | Q)";
|
|
90 |
|
|
91 |
val cnf_neg_conj = thm_by_auto "(~(P & Q)) = (~P | ~Q)";
|
|
92 |
|
|
93 |
val cnf_neg_disj = thm_by_auto "(~(P | Q)) = (~P & ~Q)";
|
|
94 |
|
|
95 |
val cnf_neg_imp = thm_by_auto "(~(P --> Q)) = (P & ~Q)";
|
|
96 |
|
|
97 |
val cnf_double_neg = thm_by_auto "(~~P) = P";
|
|
98 |
|
|
99 |
val cnf_disj_conj = thm_by_auto "((P & Q) | R) = ((P | R) & (Q | R))";
|
|
100 |
|
|
101 |
val cnf_disj_imp = thm_by_auto "((P --> Q) | R) = (~P | (Q | R))";
|
|
102 |
|
|
103 |
val cnf_disj_disj = thm_by_auto "((P | Q) | R) = (P | (Q | R))";
|
|
104 |
|
|
105 |
val cnf_disj_false = thm_by_auto "(False | P) = P";
|
|
106 |
|
|
107 |
val cnf_disj_true = thm_by_auto "(True | P) = True";
|
|
108 |
|
|
109 |
val cnf_disj_not_false = thm_by_auto "(~False | P) = True";
|
|
110 |
|
|
111 |
val cnf_disj_not_true = thm_by_auto "(~True | P) = P";
|
|
112 |
|
|
113 |
val cnf_eq_trans = thm_by_auto "[| ( (P::bool) = Q) ; Q = R |] ==> (P = R)";
|
|
114 |
|
|
115 |
val cnf_comb2eq = thm_by_auto "[| P = Q ; R = T |] ==> (P & R) = (Q & T)";
|
|
116 |
|
|
117 |
val cnf_disj_sym = thm_by_auto "(P | Q) = (Q | P)";
|
|
118 |
|
|
119 |
val cnf_cong_disj = thm_by_auto "(P = Q) ==> (P | R) = (Q | R)";
|
|
120 |
|
|
121 |
val icnf_elim_disj1 = thm_by_auto "Q = R ==> (~P | Q) = (P --> R)";
|
|
122 |
|
|
123 |
val icnf_elim_disj2 = thm_by_auto "Q = R ==> (P | Q) = (~P --> R)";
|
|
124 |
|
|
125 |
val icnf_neg_false1 = thm_by_auto "(~P) = (P --> False)";
|
|
126 |
|
|
127 |
val icnf_neg_false2 = thm_by_auto "P = (~P --> False)";
|
|
128 |
|
|
129 |
val weakening_thm = thm_by_auto "[| P ; Q |] ==> Q";
|
|
130 |
|
|
131 |
val cnf_newlit = thm_by_auto
|
|
132 |
"((P & Q) | R) = (EX (x :: bool). (~x | P) & (~x | Q) & (x | ~P | ~ Q) & (x | R))";
|
|
133 |
|
|
134 |
val cnf_all_ex = thm_by_auto
|
|
135 |
"(ALL (x :: bool). (P x = Q x)) ==> (EX x. P x) = (EX x. Q x)";
|
|
136 |
|
|
137 |
(* [| P ; ~P |] ==> False *)
|
|
138 |
val cnf_notE = read_instantiate [("R", "False")] (rotate_prems 1 notE);
|
|
139 |
|
|
140 |
val cnf_dneg = thm_by_auto "P ==> ~~P";
|
|
141 |
|
|
142 |
val cnf_neg_disjI = thm_by_auto "[| ~P ; ~Q |] ==> ~(P | Q)";
|
|
143 |
|
|
144 |
val cnf_eq_imp = thm_by_auto "[|((P::bool) = Q) ; P |] ==> Q";
|
|
145 |
|
|
146 |
(***************************************************************************)
|
|
147 |
|
|
148 |
fun is_atm (Const("Trueprop",_) $ x) = is_atm x
|
|
149 |
| is_atm (Const("==>",_) $ x $ y) = false
|
|
150 |
| is_atm (Const("False",_)) = false
|
|
151 |
| is_atm (Const("True", _)) = false
|
|
152 |
| is_atm (Const("op &",_) $ x $ y) = false
|
|
153 |
| is_atm (Const("op |",_) $ x $ y) = false
|
|
154 |
| is_atm (Const("op -->",_) $ x $ y) = false
|
|
155 |
| is_atm (Const("Not",_) $ x) = false
|
|
156 |
| is_atm t = true
|
|
157 |
|
|
158 |
|
|
159 |
fun is_lit (Const("Trueprop",_) $ x) = is_lit x
|
|
160 |
| is_lit (Const("Not", _) $ x) = is_atm x
|
|
161 |
| is_lit t = is_atm t
|
|
162 |
|
|
163 |
fun is_clause (Const("Trueprop",_) $ x) = is_clause x
|
|
164 |
| is_clause (Const("op |", _) $ x $ y) =
|
|
165 |
(is_clause x) andalso (is_clause y)
|
|
166 |
| is_clause t = is_lit t
|
|
167 |
|
|
168 |
fun is_cnf (Const("Trueprop", _) $ x) = is_cnf x
|
|
169 |
| is_cnf (Const("op &",_) $ x $ y) = (is_cnf x) andalso (is_cnf y)
|
|
170 |
| is_cnf t = is_clause t
|
|
171 |
|
|
172 |
|
|
173 |
(* Checking for raw clauses *)
|
|
174 |
fun is_raw_clause (Const("Trueprop",_) $ x) = is_raw_clause x
|
|
175 |
| is_raw_clause (Const("==>",_) $ x $
|
|
176 |
(Const("Trueprop",_) $ Const("False",_))) = is_lit x
|
|
177 |
| is_raw_clause (Const("==>",_) $ x $ y) =
|
|
178 |
(is_lit x) andalso (is_raw_clause y)
|
|
179 |
| is_raw_clause t = false
|
|
180 |
|
|
181 |
|
|
182 |
|
|
183 |
(* Translate a CNF clause into a raw clause *)
|
|
184 |
fun cnf2raw_thm c =
|
|
185 |
let val nc = c RS cnf_notE
|
|
186 |
in
|
|
187 |
rule_by_tactic (REPEAT_SOME (fn i =>
|
|
188 |
rtac cnf_dneg i
|
|
189 |
ORELSE rtac cnf_neg_disjI i)) nc
|
|
190 |
handle THM _ => nc
|
|
191 |
end
|
|
192 |
|
|
193 |
fun cnf2raw_thms nil = nil
|
|
194 |
| cnf2raw_thms (c::l) =
|
|
195 |
let val t = term_of (cprop_of c)
|
|
196 |
in
|
|
197 |
if (is_clause t) then (cnf2raw_thm c) :: cnf2raw_thms l
|
|
198 |
else cnf2raw_thms l
|
|
199 |
end
|
|
200 |
|
|
201 |
|
|
202 |
(* Translating HOL formula (in CNF) to PropLogic formula. Returns also an
|
|
203 |
association list, relating literals to their indices *)
|
|
204 |
|
|
205 |
local
|
|
206 |
(* maps atomic formulas to variable numbers *)
|
|
207 |
val dictionary : ((Term.term * int) list) ref = ref nil;
|
|
208 |
val var_count = ref 0;
|
|
209 |
val pAnd = PropLogic.And;
|
|
210 |
val pOr = PropLogic.Or;
|
|
211 |
val pNot = PropLogic.Not;
|
|
212 |
val pFalse = PropLogic.False;
|
|
213 |
val pTrue = PropLogic.True;
|
|
214 |
val pVar = PropLogic.BoolVar;
|
|
215 |
|
|
216 |
fun mk_clause (Const("Trueprop",_) $ x) = mk_clause x
|
|
217 |
| mk_clause (Const("op |",_) $ x $ y) = pOr(mk_clause x, mk_clause y)
|
|
218 |
| mk_clause (Const("Not", _) $ x) = pNot (mk_clause x)
|
|
219 |
| mk_clause (Const("True",_)) = pTrue
|
|
220 |
| mk_clause (Const("False",_)) = pFalse
|
|
221 |
| mk_clause t =
|
|
222 |
let
|
|
223 |
val idx = AList.lookup op= (!dictionary) t
|
|
224 |
in
|
|
225 |
case idx of
|
|
226 |
(SOME x) => pVar x
|
|
227 |
| NONE =>
|
|
228 |
let
|
|
229 |
val new_var = inc var_count
|
|
230 |
in
|
|
231 |
dictionary := (t, new_var) :: (!dictionary);
|
|
232 |
pVar new_var
|
|
233 |
end
|
|
234 |
end
|
|
235 |
|
|
236 |
fun mk_clauses nil = pTrue
|
|
237 |
| mk_clauses (x::nil) = mk_clause x
|
|
238 |
| mk_clauses (x::l) = pAnd(mk_clause x, mk_clauses l)
|
|
239 |
|
|
240 |
in
|
|
241 |
fun cnf2prop thms =
|
|
242 |
(
|
|
243 |
var_count := 0;
|
|
244 |
dictionary := nil;
|
|
245 |
(mk_clauses (map (fn x => term_of (cprop_of x)) thms), !dictionary)
|
|
246 |
)
|
|
247 |
end
|
|
248 |
|
|
249 |
|
|
250 |
|
|
251 |
(* Instantiate a theorem with a list of terms *)
|
|
252 |
fun inst_thm sign l thm =
|
|
253 |
instantiate' [] (map (fn x => SOME (cterm_of sign x)) l) thm
|
|
254 |
|
|
255 |
(* Tactic to remove the first hypothesis of the first subgoal. *)
|
|
256 |
fun weakening_tac i = (dtac weakening_thm i) THEN (atac (i+1));
|
|
257 |
|
|
258 |
(* Tactic for removing the n first hypotheses of the first subgoal. *)
|
|
259 |
fun weakenings_tac 0 state = all_tac state
|
|
260 |
| weakenings_tac n state = ((weakening_tac 1) THEN (weakenings_tac (n-1))) state
|
|
261 |
|
|
262 |
|
|
263 |
(*
|
|
264 |
Transform a formula into a "head" negation normal form, that is,
|
|
265 |
the top level connective is not a negation, with the exception
|
|
266 |
of negative literals. Returns the pair of the head normal term with
|
|
267 |
the theorem corresponding to the transformation.
|
|
268 |
*)
|
|
269 |
fun head_nnf sign (Const("Not",_) $ (Const("op &",_) $ x $ y)) =
|
|
270 |
let val t = mk_disj(Not $ x, Not $ y)
|
|
271 |
val neg_thm = inst_thm sign [x, y] cnf_neg_conj
|
|
272 |
in
|
|
273 |
(t, neg_thm)
|
|
274 |
end
|
|
275 |
|
|
276 |
| head_nnf sign (Const("Not", _) $ (Const("op |",_) $ x $ y)) =
|
|
277 |
let val t = mk_conj(Not $ x, Not $ y)
|
|
278 |
val neg_thm = inst_thm sign [x, y] cnf_neg_disj;
|
|
279 |
in
|
|
280 |
(t, neg_thm)
|
|
281 |
end
|
|
282 |
|
|
283 |
| head_nnf sign (Const("Not", _) $ (Const("op -->",_) $ x $ y)) =
|
|
284 |
let val t = mk_conj(x, Not $ y)
|
|
285 |
val neg_thm = inst_thm sign [x, y] cnf_neg_imp
|
|
286 |
in
|
|
287 |
(t, neg_thm)
|
|
288 |
end
|
|
289 |
|
|
290 |
| head_nnf sign (Const("Not",_) $ (Const("Not",_) $ x)) =
|
|
291 |
(x, inst_thm sign [x] cnf_double_neg)
|
|
292 |
|
|
293 |
| head_nnf sign (Const("Not",_) $ Const("True",_)) =
|
|
294 |
(false_const, cnf_not_true_false)
|
|
295 |
|
|
296 |
| head_nnf sign (Const("Not",_) $ Const("False",_)) =
|
|
297 |
(true_const, cnf_not_false_true)
|
|
298 |
|
|
299 |
| head_nnf sign t =
|
|
300 |
(t, inst_thm sign [t] cnf_eq_id)
|
|
301 |
|
|
302 |
|
|
303 |
(***************************************************************************)
|
|
304 |
(* Tactics for simple CNF transformation *)
|
|
305 |
|
|
306 |
(* A naive procedure for CNF transformation:
|
|
307 |
Given any t, produce a theorem t = t', where t' is in
|
|
308 |
conjunction normal form
|
|
309 |
*)
|
|
310 |
fun mk_cnf_thm sign (Const("Trueprop",_) $ x) = mk_cnf_thm sign x
|
|
311 |
| mk_cnf_thm sign (t as (Const(_,_))) = inst_thm sign [t] cnf_eq_id
|
|
312 |
| mk_cnf_thm sign (t as (Free(_,_))) = inst_thm sign [t] cnf_eq_id
|
|
313 |
|
|
314 |
| mk_cnf_thm sign (Const("op -->", _) $ x $ y) =
|
|
315 |
let val thm1 = inst_thm sign [x, y] cnf_imp2disj;
|
|
316 |
val thm2 = mk_cnf_thm sign (mk_disj(Not $ x, y));
|
|
317 |
in
|
|
318 |
cnf_eq_trans OF [thm1, thm2]
|
|
319 |
end
|
|
320 |
|
|
321 |
| mk_cnf_thm sign (Const("op &", _) $ x $ y) =
|
|
322 |
let val cnf1 = mk_cnf_thm sign x;
|
|
323 |
val cnf2 = mk_cnf_thm sign y;
|
|
324 |
in
|
|
325 |
cnf_comb2eq OF [cnf1, cnf2]
|
|
326 |
end
|
|
327 |
|
|
328 |
| mk_cnf_thm sign (Const("Not",_) $ Const("True",_)) =
|
|
329 |
cnf_not_true_false
|
|
330 |
|
|
331 |
| mk_cnf_thm sign (Const("Not",_) $ Const("False",_)) =
|
|
332 |
cnf_not_false_true
|
|
333 |
|
|
334 |
| mk_cnf_thm sign (t as (Const("Not", _) $ x)) =
|
|
335 |
(
|
|
336 |
if (is_atm x) then inst_thm sign [t] cnf_eq_id
|
|
337 |
else
|
|
338 |
let val (t1, hn_thm) = head_nnf sign t
|
|
339 |
val cnf_thm = mk_cnf_thm sign t1
|
|
340 |
in
|
|
341 |
cnf_eq_trans OF [hn_thm, cnf_thm]
|
|
342 |
end
|
|
343 |
)
|
|
344 |
|
|
345 |
| mk_cnf_thm sign (Const("op |",_) $ (Const("op &", _) $ p $ q) $ r) =
|
|
346 |
let val thm1 = inst_thm sign [p, q, r] cnf_disj_conj;
|
|
347 |
val thm2 = mk_cnf_thm sign (mk_conj(mk_disj(p, r), mk_disj(q,r)));
|
|
348 |
in
|
|
349 |
cnf_eq_trans OF [thm1, thm2]
|
|
350 |
end
|
|
351 |
|
|
352 |
| mk_cnf_thm sign (Const("op |",_) $ (Const("op |", _) $ p $ q) $ r) =
|
|
353 |
let val thm1 = inst_thm sign [p,q,r] cnf_disj_disj;
|
|
354 |
val thm2 = mk_cnf_thm sign (mk_disj(p, mk_disj(q,r)));
|
|
355 |
in
|
|
356 |
cnf_eq_trans OF [thm1, thm2]
|
|
357 |
end
|
|
358 |
|
|
359 |
| mk_cnf_thm sign (Const("op |",_) $ (Const("op -->", _) $ p $ q) $ r) =
|
|
360 |
let val thm1 = inst_thm sign [p,q,r] cnf_disj_imp;
|
|
361 |
val thm2 = mk_cnf_thm sign (mk_disj(Not $ p, mk_disj(q, r)));
|
|
362 |
in
|
|
363 |
cnf_eq_trans OF [thm1, thm2]
|
|
364 |
end
|
|
365 |
|
|
366 |
| mk_cnf_thm sign (Const("op |",_) $ Const("False",_) $ p) =
|
|
367 |
let val thm1 = inst_thm sign [p] cnf_disj_false;
|
|
368 |
val thm2 = mk_cnf_thm sign p
|
|
369 |
in
|
|
370 |
cnf_eq_trans OF [thm1, thm2]
|
|
371 |
end
|
|
372 |
|
|
373 |
| mk_cnf_thm sign (Const("op |",_) $ Const("True",_) $ p) =
|
|
374 |
inst_thm sign [p] cnf_disj_true
|
|
375 |
|
|
376 |
| mk_cnf_thm sign (Const("op |",_) $ (Const("Not",_) $ Const("True",_)) $ p) =
|
|
377 |
let val thm1 = inst_thm sign [p] cnf_disj_not_true;
|
|
378 |
val thm2 = mk_cnf_thm sign p
|
|
379 |
in
|
|
380 |
cnf_eq_trans OF [thm1, thm2]
|
|
381 |
end
|
|
382 |
|
|
383 |
| mk_cnf_thm sign (Const("op |",_) $ (Const("Not",_) $ Const("False",_)) $ p) =
|
|
384 |
inst_thm sign [p] cnf_disj_not_false
|
|
385 |
|
|
386 |
| mk_cnf_thm sign (t as (Const("op |",_) $ p $ q)) =
|
|
387 |
if (is_lit p) then
|
|
388 |
(
|
|
389 |
if (is_clause t) then inst_thm sign [t] cnf_eq_id
|
|
390 |
else
|
|
391 |
let val thm1 = inst_thm sign [p, q] cnf_disj_sym;
|
|
392 |
val thm2 = mk_cnf_thm sign (mk_disj(q, p))
|
|
393 |
in
|
|
394 |
cnf_eq_trans OF [thm1, thm2]
|
|
395 |
end
|
|
396 |
)
|
|
397 |
else
|
|
398 |
let val (u, thm1) = head_nnf sign p;
|
|
399 |
val thm2 = inst_thm sign [p,u,q] cnf_cong_disj;
|
|
400 |
val thm3 = mk_cnf_thm sign (mk_disj(u, q))
|
|
401 |
in
|
|
402 |
cnf_eq_trans OF [(thm1 RS thm2), thm3]
|
|
403 |
end
|
|
404 |
|
|
405 |
| mk_cnf_thm sign t = inst_thm sign [t] cnf_eq_id
|
|
406 |
(* error ("I don't know how to handle the formula " ^
|
|
407 |
(Sign.string_of_term sign t))
|
|
408 |
*)
|
|
409 |
|
|
410 |
fun term_of_thm c = term_of (cprop_of c)
|
|
411 |
|
|
412 |
|
|
413 |
(* Transform a given list of theorems (thms) into CNF *)
|
|
414 |
|
|
415 |
fun mk_cnf_thms sg nil = nil
|
|
416 |
| mk_cnf_thms sg (x::l) =
|
|
417 |
let val t = term_of_thm x
|
|
418 |
in
|
|
419 |
if (is_clause t) then x :: mk_cnf_thms sg l
|
|
420 |
else
|
|
421 |
let val thm1 = mk_cnf_thm sg t
|
|
422 |
val thm2 = cnf_eq_imp OF [thm1, x]
|
|
423 |
in
|
|
424 |
thm2 :: mk_cnf_thms sg l
|
|
425 |
end
|
|
426 |
end
|
|
427 |
|
|
428 |
|
|
429 |
(* Count the number of hypotheses in a formula *)
|
|
430 |
fun num_of_hyps (Const("Trueprop", _) $ x) = num_of_hyps x
|
|
431 |
| num_of_hyps (Const("==>",_) $ x $ y) = 1 + (num_of_hyps y)
|
|
432 |
| num_of_hyps t = 0
|
|
433 |
|
|
434 |
(* Tactic for converting to CNF (in primitive form):
|
|
435 |
it takes the first subgoal of the proof state, transform all its
|
|
436 |
hypotheses into CNF (in primivite form) and remove the original
|
|
437 |
hypotheses.
|
|
438 |
*)
|
|
439 |
fun cnf_thin_tac state =
|
|
440 |
let val sg = Thm.sign_of_thm state
|
|
441 |
in
|
|
442 |
case (prems_of state) of
|
|
443 |
[] => Seq.empty
|
|
444 |
| (subgoal::_) =>
|
|
445 |
let
|
|
446 |
val n = num_of_hyps (strip_all_body subgoal);
|
|
447 |
val tac1 = METAHYPS (fn l => cut_facts_tac (mk_cnf_thms sg l) 1) 1
|
|
448 |
in
|
|
449 |
(tac1 THEN weakenings_tac n THEN (REPEAT (etac conjE 1)) ) state
|
|
450 |
end
|
|
451 |
end
|
|
452 |
|
|
453 |
(* Tactic for converting to CNF (in primitive form), keeping
|
|
454 |
the original hypotheses. *)
|
|
455 |
|
|
456 |
fun cnf_tac state =
|
|
457 |
let val sg = Thm.sign_of_thm state
|
|
458 |
in
|
|
459 |
case (prems_of state) of
|
|
460 |
[] => Seq.empty
|
|
461 |
| (subgoal::_) =>
|
|
462 |
METAHYPS (fn l => cut_facts_tac (mk_cnf_thms sg l) 1
|
|
463 |
THEN (REPEAT (etac conjE 1)) ) 1 state
|
|
464 |
end
|
|
465 |
|
|
466 |
|
|
467 |
(***************************************************************************)
|
|
468 |
(* CNF transformation by introducing new literals *)
|
|
469 |
|
|
470 |
(*** IMPORTANT:
|
|
471 |
This transformation uses variables of the form "lit_i", where i is a natural
|
|
472 |
number. For the transformation to work, these variables must not already
|
|
473 |
occur freely in the formula being transformed.
|
|
474 |
***)
|
|
475 |
|
|
476 |
fun ext_conj x p q r =
|
|
477 |
mk_conj(
|
|
478 |
mk_disj(Not $ x, p),
|
|
479 |
mk_conj(
|
|
480 |
mk_disj(Not $ x, q),
|
|
481 |
mk_conj(
|
|
482 |
mk_disj(x, mk_disj(Not $ p, Not $ q)),
|
|
483 |
mk_disj(x, r)
|
|
484 |
)
|
|
485 |
)
|
|
486 |
)
|
|
487 |
|
|
488 |
|
|
489 |
(* Transform to CNF in primitive forms, possibly introduce extra variables *)
|
|
490 |
fun mk_cnfx_thm sign (Const("Trueprop",_) $ x) = mk_cnfx_thm sign x
|
|
491 |
| mk_cnfx_thm sign (t as (Const(_,_))) = inst_thm sign [t] cnf_eq_id
|
|
492 |
| mk_cnfx_thm sign (t as (Free(_,_))) = inst_thm sign [t] cnf_eq_id
|
|
493 |
| mk_cnfx_thm sign (Const("op -->", _) $ x $ y) =
|
|
494 |
let val thm1 = inst_thm sign [x, y] cnf_imp2disj;
|
|
495 |
val thm2 = mk_cnfx_thm sign (mk_disj(Not $ x, y))
|
|
496 |
in
|
|
497 |
cnf_eq_trans OF [thm1, thm2]
|
|
498 |
end
|
|
499 |
|
|
500 |
| mk_cnfx_thm sign (Const("op &", _) $ x $ y) =
|
|
501 |
let val cnf1 = mk_cnfx_thm sign x
|
|
502 |
val cnf2 = mk_cnfx_thm sign y
|
|
503 |
in
|
|
504 |
cnf_comb2eq OF [cnf1, cnf2]
|
|
505 |
end
|
|
506 |
|
|
507 |
| mk_cnfx_thm sign (Const("Not",_) $ Const("True",_)) =
|
|
508 |
cnf_not_true_false
|
|
509 |
|
|
510 |
| mk_cnfx_thm sign (Const("Not",_) $ Const("False",_)) =
|
|
511 |
cnf_not_false_true
|
|
512 |
|
|
513 |
| mk_cnfx_thm sign (t as (Const("Not", _) $ x)) =
|
|
514 |
(
|
|
515 |
if (is_atm x) then inst_thm sign [t] cnf_eq_id
|
|
516 |
else
|
|
517 |
let val (t1, hn_thm) = head_nnf sign t
|
|
518 |
val cnf_thm = mk_cnfx_thm sign t1
|
|
519 |
in
|
|
520 |
cnf_eq_trans OF [hn_thm, cnf_thm]
|
|
521 |
end
|
|
522 |
)
|
|
523 |
|
|
524 |
| mk_cnfx_thm sign (Const("op |",_) $ (Const("op &", _) $ p $ q) $ r) =
|
|
525 |
if (is_lit r) then
|
|
526 |
let val thm1 = inst_thm sign [p, q, r] cnf_disj_conj
|
|
527 |
val thm2 = mk_cnfx_thm sign (mk_conj(mk_disj(p, r), mk_disj(q,r)))
|
|
528 |
in
|
|
529 |
cnf_eq_trans OF [thm1, thm2]
|
|
530 |
end
|
|
531 |
else cnfx_newlit sign p q r
|
|
532 |
|
|
533 |
| mk_cnfx_thm sign (Const("op |",_) $ (Const("op |", _) $ p $ q) $ r) =
|
|
534 |
let val thm1 = inst_thm sign [p,q,r] cnf_disj_disj
|
|
535 |
val thm2 = mk_cnfx_thm sign (mk_disj(p, mk_disj(q,r)))
|
|
536 |
in
|
|
537 |
cnf_eq_trans OF [thm1, thm2]
|
|
538 |
end
|
|
539 |
|
|
540 |
| mk_cnfx_thm sign (Const("op |",_) $ (Const("op -->", _) $ p $ q) $ r) =
|
|
541 |
let val thm1 = inst_thm sign [p,q,r] cnf_disj_imp
|
|
542 |
val thm2 = mk_cnfx_thm sign (mk_disj(Not $ p, mk_disj(q, r)))
|
|
543 |
in
|
|
544 |
cnf_eq_trans OF [thm1, thm2]
|
|
545 |
end
|
|
546 |
|
|
547 |
| mk_cnfx_thm sign (Const("op |",_) $ Const("False",_) $ p) =
|
|
548 |
let val thm1 = inst_thm sign [p] cnf_disj_false;
|
|
549 |
val thm2 = mk_cnfx_thm sign p
|
|
550 |
in
|
|
551 |
cnf_eq_trans OF [thm1, thm2]
|
|
552 |
end
|
|
553 |
|
|
554 |
| mk_cnfx_thm sign (Const("op |",_) $ Const("True",_) $ p) =
|
|
555 |
inst_thm sign [p] cnf_disj_true
|
|
556 |
|
|
557 |
| mk_cnfx_thm sign (Const("op |",_) $ (Const("Not",_) $ Const("True",_)) $ p) =
|
|
558 |
let val thm1 = inst_thm sign [p] cnf_disj_not_true;
|
|
559 |
val thm2 = mk_cnfx_thm sign p
|
|
560 |
in
|
|
561 |
cnf_eq_trans OF [thm1, thm2]
|
|
562 |
end
|
|
563 |
|
|
564 |
| mk_cnfx_thm sign (Const("op |",_) $ (Const("Not",_) $ Const("False",_)) $ p) =
|
|
565 |
inst_thm sign [p] cnf_disj_not_false
|
|
566 |
|
|
567 |
| mk_cnfx_thm sign (t as (Const("op |",_) $ p $ q)) =
|
|
568 |
if (is_lit p) then
|
|
569 |
(
|
|
570 |
if (is_clause t) then inst_thm sign [t] cnf_eq_id
|
|
571 |
else
|
|
572 |
let val thm1 = inst_thm sign [p, q] cnf_disj_sym
|
|
573 |
val thm2 = mk_cnfx_thm sign (mk_disj(q, p))
|
|
574 |
in
|
|
575 |
cnf_eq_trans OF [thm1, thm2]
|
|
576 |
end
|
|
577 |
)
|
|
578 |
else
|
|
579 |
let val (u, thm1) = head_nnf sign p
|
|
580 |
val thm2 = inst_thm sign [p,u,q] cnf_cong_disj
|
|
581 |
val thm3 = mk_cnfx_thm sign (mk_disj(u, q))
|
|
582 |
in
|
|
583 |
cnf_eq_trans OF [(thm1 RS thm2), thm3]
|
|
584 |
end
|
|
585 |
|
|
586 |
| mk_cnfx_thm sign t = error ("I don't know how to handle the formula " ^
|
|
587 |
(Sign.string_of_term sign t))
|
|
588 |
|
|
589 |
and cnfx_newlit sign p q r =
|
|
590 |
let val lit = read ("lit_" ^ (Int.toString (!lit_id)) ^ " :: bool")
|
|
591 |
val _ = (lit_id := !lit_id + 1)
|
|
592 |
val ct_lit = cterm_of sign lit
|
|
593 |
val x_conj = ext_conj lit p q r
|
|
594 |
val thm1 = inst_thm sign [p,q,r] cnf_newlit
|
|
595 |
val thm2 = mk_cnfx_thm sign x_conj
|
|
596 |
val thm3 = forall_intr ct_lit thm2
|
|
597 |
val thm4 = strip_shyps (thm3 COMP allI)
|
|
598 |
val thm5 = strip_shyps (thm4 RS cnf_all_ex)
|
|
599 |
in
|
|
600 |
cnf_eq_trans OF [thm1, thm5]
|
|
601 |
end
|
|
602 |
|
|
603 |
|
|
604 |
(* Theorems for converting formula into CNF (in primitive form), with
|
|
605 |
new extra variables *)
|
|
606 |
|
|
607 |
|
|
608 |
fun mk_cnfx_thms sg nil = nil
|
|
609 |
| mk_cnfx_thms sg (x::l) =
|
|
610 |
let val t = term_of_thm x
|
|
611 |
in
|
|
612 |
if (is_clause t) then x :: mk_cnfx_thms sg l
|
|
613 |
else
|
|
614 |
let val thm1 = mk_cnfx_thm sg t
|
|
615 |
val thm2 = cnf_eq_imp OF [thm1,x]
|
|
616 |
in
|
|
617 |
thm2 :: mk_cnfx_thms sg l
|
|
618 |
end
|
|
619 |
end
|
|
620 |
|
|
621 |
|
|
622 |
(* Tactic for converting hypotheses into CNF, possibly
|
|
623 |
introducing new variables *)
|
|
624 |
|
|
625 |
fun cnfx_thin_tac state =
|
|
626 |
let val sg = Thm.sign_of_thm state
|
|
627 |
in
|
|
628 |
case (prems_of state) of
|
|
629 |
[] => Seq.empty
|
|
630 |
| (subgoal::_) =>
|
|
631 |
let val n = num_of_hyps (strip_all_body subgoal);
|
|
632 |
val tac1 = METAHYPS (fn l => cut_facts_tac (mk_cnfx_thms sg l) 1) 1
|
|
633 |
in
|
|
634 |
EVERY [tac1, weakenings_tac n,
|
|
635 |
REPEAT (etac conjE 1 ORELSE etac exE 1)] state
|
|
636 |
end
|
|
637 |
end
|
|
638 |
|
|
639 |
(* Tactic for converting the conclusion of a goal into CNF *)
|
|
640 |
|
|
641 |
fun get_concl (Const("Trueprop", _) $ x) = get_concl x
|
|
642 |
| get_concl (Const("==>",_) $ x $ y) = get_concl y
|
|
643 |
| get_concl t = t
|
|
644 |
|
|
645 |
fun cnf_concl_tac' state =
|
|
646 |
case (prems_of state) of
|
|
647 |
[] => Seq.empty
|
|
648 |
| (subgoal::_) =>
|
|
649 |
let val sg = Thm.sign_of_thm state
|
|
650 |
val c = get_concl subgoal
|
|
651 |
val thm1 = (mk_cnf_thm sg c) RS cnf_eq_sym
|
|
652 |
val thm2 = thm1 RS subst
|
|
653 |
in
|
|
654 |
rtac thm2 1 state
|
|
655 |
end
|
|
656 |
|
|
657 |
val cnf_concl_tac = METAHYPS (fn l => cnf_concl_tac') 1
|
|
658 |
|
|
659 |
|
|
660 |
end (*of structure*)
|