1 (******************************************************************************)
2 (* FILE : clausal_form.ml *)
3 (* DESCRIPTION : Functions for putting a formula into clausal form. *)
5 (* READS FILES : <none> *)
6 (* WRITES FILES : <none> *)
8 (* AUTHOR : R.J.Boulton *)
9 (* DATE : 13th May 1991 *)
11 (* LAST MODIFIED : R.J.Boulton *)
12 (* DATE : 12th October 1992 *)
14 (* LAST MODIFIED : P. Papapanagiotou (University of Edinburgh) *)
16 (******************************************************************************)
18 let IMP_DISJ_THM = TAUT `!t1 t2. t1 ==> t2 <=> ~t1 \/ t2`;;
19 let RIGHT_OR_OVER_AND = TAUT `!t1 t2 t3. t2 /\ t3 \/ t1 <=> (t2 \/ t1) /\ (t3 \/ t1)`;;
20 let LEFT_OR_OVER_AND = TAUT `!t1 t2 t3. t1 \/ t2 /\ t3 <=> (t1 \/ t2) /\ (t1 \/ t3)`;;
22 (*============================================================================*)
23 (* Theorems for normalizing Boolean terms *)
24 (*============================================================================*)
26 (*----------------------------------------------------------------------------*)
27 (* EQ_EXPAND = |- (x = y) = ((~x \/ y) /\ (~y \/ x)) *)
28 (*----------------------------------------------------------------------------*)
32 (`(x = y) = ((~x \/ y) /\ (~y \/ x))`,
33 BOOL_CASES_TAC `x:bool` THEN
34 BOOL_CASES_TAC `y:bool` THEN
37 (*----------------------------------------------------------------------------*)
38 (* IMP_EXPAND = |- (x ==> y) = (~x \/ y) *)
39 (*----------------------------------------------------------------------------*)
41 let IMP_EXPAND = SPEC `y:bool` (SPEC `x:bool` IMP_DISJ_THM);;
43 (*----------------------------------------------------------------------------*)
44 (* COND_EXPAND = |- (x => y | z) = ((~x \/ y) /\ (x \/ z)) *)
45 (*----------------------------------------------------------------------------*)
49 (`(if x then y else z) = ((~x \/ y) /\ (x \/ z))`,
50 BOOL_CASES_TAC `x:bool` THEN
51 BOOL_CASES_TAC `y:bool` THEN
52 BOOL_CASES_TAC `z:bool` THEN
55 (*----------------------------------------------------------------------------*)
56 (* NOT_NOT_NORM = |- ~~x = x *)
57 (*----------------------------------------------------------------------------*)
59 let NOT_NOT_NORM = SPEC `x:bool` (CONJUNCT1 NOT_CLAUSES);;
61 (*----------------------------------------------------------------------------*)
62 (* NOT_CONJ_NORM = |- ~(x /\ y) = (~x \/ ~y) *)
63 (*----------------------------------------------------------------------------*)
65 let NOT_CONJ_NORM = CONJUNCT1 (SPEC `y:bool` (SPEC `x:bool` DE_MORGAN_THM));;
67 (*----------------------------------------------------------------------------*)
68 (* NOT_DISJ_NORM = |- ~(x \/ y) = (~x /\ ~y) *)
69 (*----------------------------------------------------------------------------*)
71 let NOT_DISJ_NORM = CONJUNCT2 (SPEC `y:bool` (SPEC `x:bool` DE_MORGAN_THM));;
73 (*----------------------------------------------------------------------------*)
74 (* LEFT_DIST_NORM = |- x \/ (y /\ z) = (x \/ y) /\ (x \/ z) *)
75 (*----------------------------------------------------------------------------*)
78 SPEC `z:bool` (SPEC `y:bool` (SPEC `x:bool` LEFT_OR_OVER_AND));;
80 (*----------------------------------------------------------------------------*)
81 (* RIGHT_DIST_NORM = |- (x /\ y) \/ z = (x \/ z) /\ (y \/ z) *)
82 (*----------------------------------------------------------------------------*)
85 SPEC `y:bool` (SPEC `x:bool` (SPEC `z:bool` RIGHT_OR_OVER_AND));;
87 (*----------------------------------------------------------------------------*)
88 (* CONJ_ASSOC_NORM = |- (x /\ y) /\ z = x /\ (y /\ z) *)
89 (*----------------------------------------------------------------------------*)
92 SYM (SPEC `z:bool` (SPEC `y:bool` (SPEC `x:bool` CONJ_ASSOC)));;
94 (*----------------------------------------------------------------------------*)
95 (* DISJ_ASSOC_NORM = |- (x \/ y) \/ z = x \/ (y \/ z) *)
96 (*----------------------------------------------------------------------------*)
99 SYM (SPEC `z:bool` (SPEC `y:bool` (SPEC `x:bool` DISJ_ASSOC)));;
101 (*============================================================================*)
102 (* Conversions for rewriting Boolean terms *)
103 (*============================================================================*)
105 let COND_EXPAND_CONV = REWR_CONV COND_EXPAND;;
106 let CONJ_ASSOC_NORM_CONV = REWR_CONV CONJ_ASSOC_NORM;;
107 let DISJ_ASSOC_NORM_CONV = REWR_CONV DISJ_ASSOC_NORM;;
108 let EQ_EXPAND_CONV = REWR_CONV EQ_EXPAND;;
109 let IMP_EXPAND_CONV = REWR_CONV IMP_EXPAND;;
110 let LEFT_DIST_NORM_CONV = REWR_CONV LEFT_DIST_NORM;;
111 let NOT_CONJ_NORM_CONV = REWR_CONV NOT_CONJ_NORM;;
112 let NOT_DISJ_NORM_CONV = REWR_CONV NOT_DISJ_NORM;;
113 let NOT_NOT_NORM_CONV = REWR_CONV NOT_NOT_NORM;;
114 let RIGHT_DIST_NORM_CONV = REWR_CONV RIGHT_DIST_NORM;;
116 (*----------------------------------------------------------------------------*)
117 (* NOT_CONV : conv *)
122 (*----------------------------------------------------------------------------*)
126 let [th1;th2;th3] = CONJUNCTS NOT_CLAUSES
128 (let arg = dest_neg tm
129 in if (is_T arg) then th2
130 else if (is_F arg) then th3
131 else SPEC (dest_neg arg) th1
133 ) with Failure _ -> failwith "NOT_CONV";;
135 (*----------------------------------------------------------------------------*)
136 (* AND_CONV : conv *)
143 (*----------------------------------------------------------------------------*)
147 let [th1;th2;th3;th4;th5] = map GEN_ALL (CONJUNCTS (SPEC_ALL AND_CLAUSES))
149 (let (arg1,arg2) = dest_conj tm
150 in if (is_T arg1) then SPEC arg2 th1
151 else if (is_T arg2) then SPEC arg1 th2
152 else if (is_F arg1) then SPEC arg2 th3
153 else if (is_F arg2) then SPEC arg1 th4
154 else if (arg1 = arg2) then SPEC arg1 th5
157 ) with Failure _ -> failwith "AND_CONV" ;;
159 (*----------------------------------------------------------------------------*)
167 (*----------------------------------------------------------------------------*)
171 let [th1;th2;th3;th4;th5] = map GEN_ALL (CONJUNCTS (SPEC_ALL OR_CLAUSES))
173 (let (arg1,arg2) = dest_disj tm
174 in if (is_T arg1) then SPEC arg2 th1
175 else if (is_T arg2) then SPEC arg1 th2
176 else if (is_F arg1) then SPEC arg2 th3
177 else if (is_F arg2) then SPEC arg1 th4
178 else if (arg1 = arg2) then SPEC arg1 th5
181 ) with Failure _ -> failwith "OR_CONV";;
183 (*============================================================================*)
184 (* Conversions for obtaining `clausal' form *)
185 (*============================================================================*)
187 (*----------------------------------------------------------------------------*)
188 (* EQ_IMP_COND_ELIM_CONV : (term -> bool) -> conv *)
190 (* Eliminates Boolean equalities, Boolean conditionals, and implications from *)
191 (* terms consisting of =,==>,COND,/\,\/,~ and atoms. The atoms are specified *)
192 (* by the predicate that the conversion takes as its first argument. *)
193 (*----------------------------------------------------------------------------*)
195 let rec EQ_IMP_COND_ELIM_CONV is_atom tm =
197 (if (is_atom tm) then ALL_CONV tm
198 else if (is_neg tm) then (RAND_CONV (EQ_IMP_COND_ELIM_CONV is_atom)) tm
199 else if (is_eq tm) then
200 ((RATOR_CONV (RAND_CONV (EQ_IMP_COND_ELIM_CONV is_atom))) THENC
201 (RAND_CONV (EQ_IMP_COND_ELIM_CONV is_atom)) THENC
203 else if (is_imp tm) then
204 ((RATOR_CONV (RAND_CONV (EQ_IMP_COND_ELIM_CONV is_atom))) THENC
205 (RAND_CONV (EQ_IMP_COND_ELIM_CONV is_atom)) THENC
207 else if (is_cond tm) then
209 (RATOR_CONV (RAND_CONV (EQ_IMP_COND_ELIM_CONV is_atom)))) THENC
210 (RATOR_CONV (RAND_CONV (EQ_IMP_COND_ELIM_CONV is_atom))) THENC
211 (RAND_CONV (EQ_IMP_COND_ELIM_CONV is_atom)) THENC
213 else ((RATOR_CONV (RAND_CONV (EQ_IMP_COND_ELIM_CONV is_atom))) THENC
214 (RAND_CONV (EQ_IMP_COND_ELIM_CONV is_atom))) tm
215 ) with Failure _ -> failwith "EQ_IMP_COND_ELIM_CONV";;
217 (*----------------------------------------------------------------------------*)
218 (* MOVE_NOT_DOWN_CONV : (term -> bool) -> conv -> conv *)
220 (* Moves negations down through a term consisting of /\,\/,~ and atoms. The *)
221 (* atoms are specified by a predicate (first argument). When a negation has *)
222 (* reached an atom, the conversion `conv' (second argument) is applied to the *)
223 (* negation of the atom. `conv' is also applied to any non-negated atoms *)
224 (* encountered. T and F are eliminated. *)
225 (*----------------------------------------------------------------------------*)
227 let rec MOVE_NOT_DOWN_CONV is_atom conv tm =
229 (if (is_atom tm) then (conv tm)
231 then ((let tm' = rand tm
232 in if (is_atom tm') then ((conv THENC (TRY_CONV NOT_CONV)) tm)
233 else if (is_neg tm') then (NOT_NOT_NORM_CONV THENC
234 (MOVE_NOT_DOWN_CONV is_atom conv)) tm
235 else if (is_conj tm') then
236 (NOT_CONJ_NORM_CONV THENC
237 (RATOR_CONV (RAND_CONV (MOVE_NOT_DOWN_CONV is_atom conv)))
239 (RAND_CONV (MOVE_NOT_DOWN_CONV is_atom conv)) THENC
240 (TRY_CONV AND_CONV)) tm
241 else if (is_disj tm') then
242 (NOT_DISJ_NORM_CONV THENC
243 (RATOR_CONV (RAND_CONV (MOVE_NOT_DOWN_CONV is_atom conv)))
245 (RAND_CONV (MOVE_NOT_DOWN_CONV is_atom conv)) THENC
246 (TRY_CONV OR_CONV)) tm
248 else if (is_conj tm) then
249 ((RATOR_CONV (RAND_CONV (MOVE_NOT_DOWN_CONV is_atom conv))) THENC
250 (RAND_CONV (MOVE_NOT_DOWN_CONV is_atom conv)) THENC
251 (TRY_CONV AND_CONV)) tm
252 else if (is_disj tm) then
253 ((RATOR_CONV (RAND_CONV (MOVE_NOT_DOWN_CONV is_atom conv))) THENC
254 (RAND_CONV (MOVE_NOT_DOWN_CONV is_atom conv)) THENC
255 (TRY_CONV OR_CONV)) tm
257 ) with Failure _ -> failwith "MOVE_NOT_DOWN_CONV";;
259 (*----------------------------------------------------------------------------*)
260 (* CONJ_LINEAR_CONV : conv *)
262 (* Linearizes conjuncts using the following conversion applied recursively: *)
264 (* "(x /\ y) /\ z" *)
265 (* ================================ *)
266 (* |- (x /\ y) /\ z = x /\ (y /\ z) *)
267 (*----------------------------------------------------------------------------*)
269 let rec CONJ_LINEAR_CONV tm =
271 (if ((is_conj tm) & (is_conj (rand (rator tm))))
272 then (CONJ_ASSOC_NORM_CONV THENC
273 (RAND_CONV (TRY_CONV CONJ_LINEAR_CONV)) THENC
274 (TRY_CONV CONJ_LINEAR_CONV)) tm
276 ) with Failure _ -> failwith "CONJ_LINEAR_CONV";;
278 (*----------------------------------------------------------------------------*)
279 (* CONJ_NORM_FORM_CONV : conv *)
281 (* Puts a term involving /\ and \/ into conjunctive normal form. Anything *)
282 (* other than /\ and \/ is taken to be an atom and is not processed. *)
284 (* The conjunction returned is linear, i.e. the conjunctions are associated *)
285 (* to the right. Each conjunct is a linear disjunction. *)
286 (*----------------------------------------------------------------------------*)
288 let rec CONJ_NORM_FORM_CONV tm =
290 (if (is_disj tm) then
291 (if (is_conj (rand (rator tm))) then
293 (RAND_CONV ((RATOR_CONV (RAND_CONV CONJ_NORM_FORM_CONV)) THENC
294 (RAND_CONV CONJ_NORM_FORM_CONV)))) THENC
295 (RAND_CONV CONJ_NORM_FORM_CONV) THENC
296 RIGHT_DIST_NORM_CONV THENC
297 (RATOR_CONV (RAND_CONV CONJ_NORM_FORM_CONV)) THENC
298 (RAND_CONV CONJ_NORM_FORM_CONV) THENC
299 (TRY_CONV CONJ_LINEAR_CONV)) tm
300 else if (is_conj (rand tm)) then
301 ((RATOR_CONV (RAND_CONV CONJ_NORM_FORM_CONV)) THENC
302 (RAND_CONV ((RATOR_CONV (RAND_CONV CONJ_NORM_FORM_CONV)) THENC
303 (RAND_CONV CONJ_NORM_FORM_CONV))) THENC
304 LEFT_DIST_NORM_CONV THENC
305 (RATOR_CONV (RAND_CONV CONJ_NORM_FORM_CONV)) THENC
306 (RAND_CONV CONJ_NORM_FORM_CONV) THENC
307 (TRY_CONV CONJ_LINEAR_CONV)) tm
308 else if (is_disj (rand (rator tm))) then
309 (DISJ_ASSOC_NORM_CONV THENC CONJ_NORM_FORM_CONV) tm
310 else (let th = RAND_CONV CONJ_NORM_FORM_CONV tm
311 in let tm' = rhs (concl th)
312 in if (is_conj (rand tm'))
313 then (TRANS th (CONJ_NORM_FORM_CONV tm'))
315 else if (is_conj tm) then
316 ((RATOR_CONV (RAND_CONV CONJ_NORM_FORM_CONV)) THENC
317 (RAND_CONV CONJ_NORM_FORM_CONV) THENC
318 (TRY_CONV CONJ_LINEAR_CONV)) tm
320 ) with Failure _ -> failwith "CONJ_NORM_FORM_CONV";;
322 (*----------------------------------------------------------------------------*)
323 (* has_boolean_args_and_result : term -> bool *)
325 (* Yields true if and only if the term is of type ":bool", and if it is a *)
326 (* function application, all the arguments are of type ":bool". *)
327 (*----------------------------------------------------------------------------*)
329 let has_boolean_args_and_result tm =
331 (let args = snd (strip_comb tm)
332 in let types = (type_of tm)::(map type_of args)
333 in (subtract (setify types) [`:bool`]) = [] )
334 with Failure _ -> (type_of tm = `:bool`);;
336 (*----------------------------------------------------------------------------*)
337 (* CLAUSAL_FORM_CONV : conv *)
339 (* Puts into clausal form terms consisting of =,==>,COND,/\,\/,~ and atoms. *)
340 (*----------------------------------------------------------------------------*)
342 let CLAUSAL_FORM_CONV tm =
345 (not (has_boolean_args_and_result tm)) or (is_var tm) or (is_const tm)
347 ((EQ_IMP_COND_ELIM_CONV is_atom) THENC
348 (MOVE_NOT_DOWN_CONV is_atom ALL_CONV) THENC
349 CONJ_NORM_FORM_CONV) tm
350 ) with Failure _ -> failwith "CLAUSAL_FORM_CONV";;