src/HOL/Tools/cnf_funcs.ML
 author paulson Thu Oct 11 15:59:31 2007 +0200 (2007-10-11) changeset 24958 ff15f76741bd parent 21576 8c11b1ce2f05 child 26341 2f5a4367a39e permissions -rw-r--r--
rationalized redundant code
1 (*  Title:      HOL/Tools/cnf_funcs.ML
2     ID:         \$Id\$
3     Author:     Alwen Tiu, QSL Team, LORIA (http://qsl.loria.fr)
4     Author:     Tjark Weber
7   FIXME: major overlaps with the code in meson.ML
9   Description:
10   This file contains functions and tactics to transform a formula into
11   Conjunctive Normal Form (CNF).
12   A formula in CNF is of the following form:
14       (x11 | x12 | ... | x1n) & ... & (xm1 | xm2 | ... | xmk)
15       False
16       True
18   where each xij is a literal (a positive or negative atomic Boolean term),
19   i.e. the formula is a conjunction of disjunctions of literals, or
20   "False", or "True".
22   A (non-empty) disjunction of literals is referred to as "clause".
24   For the purpose of SAT proof reconstruction, we also make use of another
25   representation of clauses, which we call the "raw clauses".
26   Raw clauses are of the form
28       [..., x1', x2', ..., xn'] |- False ,
30   where each xi is a literal, and each xi' is the negation normal form of ~xi.
32   Literals are successively removed from the hyps of raw clauses by resolution
33   during SAT proof reconstruction.
34 *)
36 signature CNF =
37 sig
38 	val is_atom           : Term.term -> bool
39 	val is_literal        : Term.term -> bool
40 	val is_clause         : Term.term -> bool
41 	val clause_is_trivial : Term.term -> bool
43 	val clause2raw_thm : Thm.thm -> Thm.thm
45 	val weakening_tac : int -> Tactical.tactic  (* removes the first hypothesis of a subgoal *)
47 	val make_cnf_thm  : theory -> Term.term -> Thm.thm
48 	val make_cnfx_thm : theory -> Term.term ->  Thm.thm
49 	val cnf_rewrite_tac  : int -> Tactical.tactic  (* converts all prems of a subgoal to CNF *)
50 	val cnfx_rewrite_tac : int -> Tactical.tactic  (* converts all prems of a subgoal to (almost) definitional CNF *)
51 end;
53 structure cnf : CNF =
54 struct
56 fun thm_by_auto (G : string) : thm =
57 	prove_goal (the_context ()) G (fn prems => [cut_facts_tac prems 1, Auto_tac]);
59 (* Thm.thm *)
60 val clause2raw_notE      = thm_by_auto "[| P; ~P |] ==> False";
61 val clause2raw_not_disj  = thm_by_auto "[| ~P; ~Q |] ==> ~(P | Q)";
62 val clause2raw_not_not   = thm_by_auto "P ==> ~~P";
64 val iff_refl             = thm_by_auto "(P::bool) = P";
65 val iff_trans            = thm_by_auto "[| (P::bool) = Q; Q = R |] ==> P = R";
66 val conj_cong            = thm_by_auto "[| P = P'; Q = Q' |] ==> (P & Q) = (P' & Q')";
67 val disj_cong            = thm_by_auto "[| P = P'; Q = Q' |] ==> (P | Q) = (P' | Q')";
69 val make_nnf_imp         = thm_by_auto "[| (~P) = P'; Q = Q' |] ==> (P --> Q) = (P' | Q')";
70 val make_nnf_iff         = thm_by_auto "[| P = P'; (~P) = NP; Q = Q'; (~Q) = NQ |] ==> (P = Q) = ((P' | NQ) & (NP | Q'))";
71 val make_nnf_not_false   = thm_by_auto "(~False) = True";
72 val make_nnf_not_true    = thm_by_auto "(~True) = False";
73 val make_nnf_not_conj    = thm_by_auto "[| (~P) = P'; (~Q) = Q' |] ==> (~(P & Q)) = (P' | Q')";
74 val make_nnf_not_disj    = thm_by_auto "[| (~P) = P'; (~Q) = Q' |] ==> (~(P | Q)) = (P' & Q')";
75 val make_nnf_not_imp     = thm_by_auto "[| P = P'; (~Q) = Q' |] ==> (~(P --> Q)) = (P' & Q')";
76 val make_nnf_not_iff     = thm_by_auto "[| P = P'; (~P) = NP; Q = Q'; (~Q) = NQ |] ==> (~(P = Q)) = ((P' | Q') & (NP | NQ))";
77 val make_nnf_not_not     = thm_by_auto "P = P' ==> (~~P) = P'";
79 val simp_TF_conj_True_l  = thm_by_auto "[| P = True; Q = Q' |] ==> (P & Q) = Q'";
80 val simp_TF_conj_True_r  = thm_by_auto "[| P = P'; Q = True |] ==> (P & Q) = P'";
81 val simp_TF_conj_False_l = thm_by_auto "P = False ==> (P & Q) = False";
82 val simp_TF_conj_False_r = thm_by_auto "Q = False ==> (P & Q) = False";
83 val simp_TF_disj_True_l  = thm_by_auto "P = True ==> (P | Q) = True";
84 val simp_TF_disj_True_r  = thm_by_auto "Q = True ==> (P | Q) = True";
85 val simp_TF_disj_False_l = thm_by_auto "[| P = False; Q = Q' |] ==> (P | Q) = Q'";
86 val simp_TF_disj_False_r = thm_by_auto "[| P = P'; Q = False |] ==> (P | Q) = P'";
88 val make_cnf_disj_conj_l = thm_by_auto "[| (P | R) = PR; (Q | R) = QR |] ==> ((P & Q) | R) = (PR & QR)";
89 val make_cnf_disj_conj_r = thm_by_auto "[| (P | Q) = PQ; (P | R) = PR |] ==> (P | (Q & R)) = (PQ & PR)";
91 val make_cnfx_disj_ex_l = thm_by_auto "((EX (x::bool). P x) | Q) = (EX x. P x | Q)";
92 val make_cnfx_disj_ex_r = thm_by_auto "(P | (EX (x::bool). Q x)) = (EX x. P | Q x)";
93 val make_cnfx_newlit    = thm_by_auto "(P | Q) = (EX x. (P | x) & (Q | ~x))";
94 val make_cnfx_ex_cong   = thm_by_auto "(ALL (x::bool). P x = Q x) ==> (EX x. P x) = (EX x. Q x)";
96 val weakening_thm        = thm_by_auto "[| P; Q |] ==> Q";
98 val cnftac_eq_imp        = thm_by_auto "[| P = Q; P |] ==> Q";
100 (* Term.term -> bool *)
101 fun is_atom (Const ("False", _))                                           = false
102   | is_atom (Const ("True", _))                                            = false
103   | is_atom (Const ("op &", _) \$ _ \$ _)                                    = false
104   | is_atom (Const ("op |", _) \$ _ \$ _)                                    = false
105   | is_atom (Const ("op -->", _) \$ _ \$ _)                                  = false
106   | is_atom (Const ("op =", Type ("fun", Type ("bool", []) :: _)) \$ _ \$ _) = false
107   | is_atom (Const ("Not", _) \$ _)                                         = false
108   | is_atom _                                                              = true;
110 (* Term.term -> bool *)
111 fun is_literal (Const ("Not", _) \$ x) = is_atom x
112   | is_literal x                      = is_atom x;
114 (* Term.term -> bool *)
115 fun is_clause (Const ("op |", _) \$ x \$ y) = is_clause x andalso is_clause y
116   | is_clause x                           = is_literal x;
118 (* ------------------------------------------------------------------------- *)
119 (* clause_is_trivial: a clause is trivially true if it contains both an atom *)
120 (*      and the atom's negation                                              *)
121 (* ------------------------------------------------------------------------- *)
123 (* Term.term -> bool *)
125 fun clause_is_trivial c =
126 	let
127 		(* Term.term -> Term.term *)
128 		fun dual (Const ("Not", _) \$ x) = x
129 		  | dual x                      = HOLogic.Not \$ x
130 		(* Term.term list -> bool *)
131 		fun has_duals []      = false
132 		  | has_duals (x::xs) = (dual x) mem xs orelse has_duals xs
133 	in
134 		has_duals (HOLogic.disjuncts c)
135 	end;
137 (* ------------------------------------------------------------------------- *)
138 (* clause2raw_thm: translates a clause into a raw clause, i.e.               *)
139 (*        [...] |- x1 | ... | xn                                             *)
140 (*      (where each xi is a literal) is translated to                        *)
141 (*        [..., x1', ..., xn'] |- False ,                                    *)
142 (*      where each xi' is the negation normal form of ~xi                    *)
143 (* ------------------------------------------------------------------------- *)
145 (* Thm.thm -> Thm.thm *)
147 fun clause2raw_thm clause =
148 let
149 	(* eliminates negated disjunctions from the i-th premise, possibly *)
150 	(* adding new premises, then continues with the (i+1)-th premise   *)
151 	(* int -> Thm.thm -> Thm.thm *)
152 	fun not_disj_to_prem i thm =
153 		if i > nprems_of thm then
154 			thm
155 		else
156 			not_disj_to_prem (i+1) (Seq.hd (REPEAT_DETERM (rtac clause2raw_not_disj i) thm))
157 	(* moves all premises to hyps, i.e. "[...] |- A1 ==> ... ==> An ==> B" *)
158 	(* becomes "[..., A1, ..., An] |- B"                                   *)
159 	(* Thm.thm -> Thm.thm *)
160 	fun prems_to_hyps thm =
161 		fold (fn cprem => fn thm' =>
162 			Thm.implies_elim thm' (Thm.assume cprem)) (cprems_of thm) thm
163 in
164 	(* [...] |- ~(x1 | ... | xn) ==> False *)
165 	(clause2raw_notE OF [clause])
166 	(* [...] |- ~x1 ==> ... ==> ~xn ==> False *)
167 	|> not_disj_to_prem 1
168 	(* [...] |- x1' ==> ... ==> xn' ==> False *)
169 	|> Seq.hd o TRYALL (rtac clause2raw_not_not)
170 	(* [..., x1', ..., xn'] |- False *)
171 	|> prems_to_hyps
172 end;
174 (* ------------------------------------------------------------------------- *)
175 (* inst_thm: instantiates a theorem with a list of terms                     *)
176 (* ------------------------------------------------------------------------- *)
178 fun inst_thm thy ts thm =
179 	instantiate' [] (map (SOME o cterm_of thy) ts) thm;
181 (* ------------------------------------------------------------------------- *)
182 (*                         Naive CNF transformation                          *)
183 (* ------------------------------------------------------------------------- *)
185 (* ------------------------------------------------------------------------- *)
186 (* make_nnf_thm: produces a theorem of the form t = t', where t' is the      *)
187 (*      negation normal form (i.e. negation only occurs in front of atoms)   *)
188 (*      of t; implications ("-->") and equivalences ("=" on bool) are        *)
189 (*      eliminated (possibly causing an exponential blowup)                  *)
190 (* ------------------------------------------------------------------------- *)
192 (* Theory.theory -> Term.term -> Thm.thm *)
194 fun make_nnf_thm thy (Const ("op &", _) \$ x \$ y) =
195 	let
196 		val thm1 = make_nnf_thm thy x
197 		val thm2 = make_nnf_thm thy y
198 	in
199 		conj_cong OF [thm1, thm2]
200 	end
201   | make_nnf_thm thy (Const ("op |", _) \$ x \$ y) =
202 	let
203 		val thm1 = make_nnf_thm thy x
204 		val thm2 = make_nnf_thm thy y
205 	in
206 		disj_cong OF [thm1, thm2]
207 	end
208   | make_nnf_thm thy (Const ("op -->", _) \$ x \$ y) =
209 	let
210 		val thm1 = make_nnf_thm thy (HOLogic.Not \$ x)
211 		val thm2 = make_nnf_thm thy y
212 	in
213 		make_nnf_imp OF [thm1, thm2]
214 	end
215   | make_nnf_thm thy (Const ("op =", Type ("fun", Type ("bool", []) :: _)) \$ x \$ y) =
216 	let
217 		val thm1 = make_nnf_thm thy x
218 		val thm2 = make_nnf_thm thy (HOLogic.Not \$ x)
219 		val thm3 = make_nnf_thm thy y
220 		val thm4 = make_nnf_thm thy (HOLogic.Not \$ y)
221 	in
222 		make_nnf_iff OF [thm1, thm2, thm3, thm4]
223 	end
224   | make_nnf_thm thy (Const ("Not", _) \$ Const ("False", _)) =
225 	make_nnf_not_false
226   | make_nnf_thm thy (Const ("Not", _) \$ Const ("True", _)) =
227 	make_nnf_not_true
228   | make_nnf_thm thy (Const ("Not", _) \$ (Const ("op &", _) \$ x \$ y)) =
229 	let
230 		val thm1 = make_nnf_thm thy (HOLogic.Not \$ x)
231 		val thm2 = make_nnf_thm thy (HOLogic.Not \$ y)
232 	in
233 		make_nnf_not_conj OF [thm1, thm2]
234 	end
235   | make_nnf_thm thy (Const ("Not", _) \$ (Const ("op |", _) \$ x \$ y)) =
236 	let
237 		val thm1 = make_nnf_thm thy (HOLogic.Not \$ x)
238 		val thm2 = make_nnf_thm thy (HOLogic.Not \$ y)
239 	in
240 		make_nnf_not_disj OF [thm1, thm2]
241 	end
242   | make_nnf_thm thy (Const ("Not", _) \$ (Const ("op -->", _) \$ x \$ y)) =
243 	let
244 		val thm1 = make_nnf_thm thy x
245 		val thm2 = make_nnf_thm thy (HOLogic.Not \$ y)
246 	in
247 		make_nnf_not_imp OF [thm1, thm2]
248 	end
249   | make_nnf_thm thy (Const ("Not", _) \$ (Const ("op =", Type ("fun", Type ("bool", []) :: _)) \$ x \$ y)) =
250 	let
251 		val thm1 = make_nnf_thm thy x
252 		val thm2 = make_nnf_thm thy (HOLogic.Not \$ x)
253 		val thm3 = make_nnf_thm thy y
254 		val thm4 = make_nnf_thm thy (HOLogic.Not \$ y)
255 	in
256 		make_nnf_not_iff OF [thm1, thm2, thm3, thm4]
257 	end
258   | make_nnf_thm thy (Const ("Not", _) \$ (Const ("Not", _) \$ x)) =
259 	let
260 		val thm1 = make_nnf_thm thy x
261 	in
262 		make_nnf_not_not OF [thm1]
263 	end
264   | make_nnf_thm thy t =
265 	inst_thm thy [t] iff_refl;
267 (* ------------------------------------------------------------------------- *)
268 (* simp_True_False_thm: produces a theorem t = t', where t' is equivalent to *)
269 (*      t, but simplified wrt. the following theorems:                       *)
270 (*        (True & x) = x                                                     *)
271 (*        (x & True) = x                                                     *)
272 (*        (False & x) = False                                                *)
273 (*        (x & False) = False                                                *)
274 (*        (True | x) = True                                                  *)
275 (*        (x | True) = True                                                  *)
276 (*        (False | x) = x                                                    *)
277 (*        (x | False) = x                                                    *)
278 (*      No simplification is performed below connectives other than & and |. *)
279 (*      Optimization: The right-hand side of a conjunction (disjunction) is  *)
280 (*      simplified only if the left-hand side does not simplify to False     *)
281 (*      (True, respectively).                                                *)
282 (* ------------------------------------------------------------------------- *)
284 (* Theory.theory -> Term.term -> Thm.thm *)
286 fun simp_True_False_thm thy (Const ("op &", _) \$ x \$ y) =
287 	let
288 		val thm1 = simp_True_False_thm thy x
289 		val x'   = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1
290 	in
291 		if x' = HOLogic.false_const then
292 			simp_TF_conj_False_l OF [thm1]  (* (x & y) = False *)
293 		else
294 			let
295 				val thm2 = simp_True_False_thm thy y
296 				val y'   = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm2
297 			in
298 				if x' = HOLogic.true_const then
299 					simp_TF_conj_True_l OF [thm1, thm2]  (* (x & y) = y' *)
300 				else if y' = HOLogic.false_const then
301 					simp_TF_conj_False_r OF [thm2]  (* (x & y) = False *)
302 				else if y' = HOLogic.true_const then
303 					simp_TF_conj_True_r OF [thm1, thm2]  (* (x & y) = x' *)
304 				else
305 					conj_cong OF [thm1, thm2]  (* (x & y) = (x' & y') *)
306 			end
307 	end
308   | simp_True_False_thm thy (Const ("op |", _) \$ x \$ y) =
309 	let
310 		val thm1 = simp_True_False_thm thy x
311 		val x'   = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1
312 	in
313 		if x' = HOLogic.true_const then
314 			simp_TF_disj_True_l OF [thm1]  (* (x | y) = True *)
315 		else
316 			let
317 				val thm2 = simp_True_False_thm thy y
318 				val y'   = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm2
319 			in
320 				if x' = HOLogic.false_const then
321 					simp_TF_disj_False_l OF [thm1, thm2]  (* (x | y) = y' *)
322 				else if y' = HOLogic.true_const then
323 					simp_TF_disj_True_r OF [thm2]  (* (x | y) = True *)
324 				else if y' = HOLogic.false_const then
325 					simp_TF_disj_False_r OF [thm1, thm2]  (* (x | y) = x' *)
326 				else
327 					disj_cong OF [thm1, thm2]  (* (x | y) = (x' | y') *)
328 			end
329 	end
330   | simp_True_False_thm thy t =
331 	inst_thm thy [t] iff_refl;  (* t = t *)
333 (* ------------------------------------------------------------------------- *)
334 (* make_cnf_thm: given any HOL term 't', produces a theorem t = t', where t' *)
335 (*      is in conjunction normal form.  May cause an exponential blowup      *)
336 (*      in the length of the term.                                           *)
337 (* ------------------------------------------------------------------------- *)
339 (* Theory.theory -> Term.term -> Thm.thm *)
341 fun make_cnf_thm thy t =
342 let
343 	(* Term.term -> Thm.thm *)
344 	fun make_cnf_thm_from_nnf (Const ("op &", _) \$ x \$ y) =
345 		let
346 			val thm1 = make_cnf_thm_from_nnf x
347 			val thm2 = make_cnf_thm_from_nnf y
348 		in
349 			conj_cong OF [thm1, thm2]
350 		end
351 	  | make_cnf_thm_from_nnf (Const ("op |", _) \$ x \$ y) =
352 		let
353 			(* produces a theorem "(x' | y') = t'", where x', y', and t' are in CNF *)
354 			fun make_cnf_disj_thm (Const ("op &", _) \$ x1 \$ x2) y' =
355 				let
356 					val thm1 = make_cnf_disj_thm x1 y'
357 					val thm2 = make_cnf_disj_thm x2 y'
358 				in
359 					make_cnf_disj_conj_l OF [thm1, thm2]  (* ((x1 & x2) | y') = ((x1 | y')' & (x2 | y')') *)
360 				end
361 			  | make_cnf_disj_thm x' (Const ("op &", _) \$ y1 \$ y2) =
362 				let
363 					val thm1 = make_cnf_disj_thm x' y1
364 					val thm2 = make_cnf_disj_thm x' y2
365 				in
366 					make_cnf_disj_conj_r OF [thm1, thm2]  (* (x' | (y1 & y2)) = ((x' | y1)' & (x' | y2)') *)
367 				end
368 			  | make_cnf_disj_thm x' y' =
369 				inst_thm thy [HOLogic.mk_disj (x', y')] iff_refl  (* (x' | y') = (x' | y') *)
370 			val thm1     = make_cnf_thm_from_nnf x
371 			val thm2     = make_cnf_thm_from_nnf y
372 			val x'       = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1
373 			val y'       = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm2
374 			val disj_thm = disj_cong OF [thm1, thm2]  (* (x | y) = (x' | y') *)
375 		in
376 			iff_trans OF [disj_thm, make_cnf_disj_thm x' y']
377 		end
378 	  | make_cnf_thm_from_nnf t =
379 		inst_thm thy [t] iff_refl
380 	(* convert 't' to NNF first *)
381 	val nnf_thm  = make_nnf_thm thy t
382 	val nnf      = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) nnf_thm
383 	(* then simplify wrt. True/False (this should preserve NNF) *)
384 	val simp_thm = simp_True_False_thm thy nnf
385 	val simp     = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) simp_thm
386 	(* finally, convert to CNF (this should preserve the simplification) *)
387 	val cnf_thm  = make_cnf_thm_from_nnf simp
388 in
389 	iff_trans OF [iff_trans OF [nnf_thm, simp_thm], cnf_thm]
390 end;
392 (* ------------------------------------------------------------------------- *)
393 (*            CNF transformation by introducing new literals                 *)
394 (* ------------------------------------------------------------------------- *)
396 (* ------------------------------------------------------------------------- *)
397 (* make_cnfx_thm: given any HOL term 't', produces a theorem t = t', where   *)
398 (*      t' is almost in conjunction normal form, except that conjunctions    *)
399 (*      and existential quantifiers may be nested.  (Use e.g. 'REPEAT_DETERM *)
400 (*      (etac exE i ORELSE etac conjE i)' afterwards to normalize.)  May     *)
401 (*      introduce new (existentially bound) literals.  Note: the current     *)
402 (*      implementation calls 'make_nnf_thm', causing an exponential blowup   *)
403 (*      in the case of nested equivalences.                                  *)
404 (* ------------------------------------------------------------------------- *)
406 (* Theory.theory -> Term.term -> Thm.thm *)
408 fun make_cnfx_thm thy t =
409 let
410 	val var_id = ref 0  (* properly initialized below *)
411 	(* unit -> Term.term *)
412 	fun new_free () =
413 		Free ("cnfx_" ^ string_of_int (inc var_id), HOLogic.boolT)
414 	(* Term.term -> Thm.thm *)
415 	fun make_cnfx_thm_from_nnf (Const ("op &", _) \$ x \$ y) =
416 		let
417 			val thm1 = make_cnfx_thm_from_nnf x
418 			val thm2 = make_cnfx_thm_from_nnf y
419 		in
420 			conj_cong OF [thm1, thm2]
421 		end
422 	  | make_cnfx_thm_from_nnf (Const ("op |", _) \$ x \$ y) =
423 		if is_clause x andalso is_clause y then
424 			inst_thm thy [HOLogic.mk_disj (x, y)] iff_refl
425 		else if is_literal y orelse is_literal x then let
426 			(* produces a theorem "(x' | y') = t'", where x', y', and t' are *)
427 			(* almost in CNF, and x' or y' is a literal                      *)
428 			fun make_cnfx_disj_thm (Const ("op &", _) \$ x1 \$ x2) y' =
429 				let
430 					val thm1 = make_cnfx_disj_thm x1 y'
431 					val thm2 = make_cnfx_disj_thm x2 y'
432 				in
433 					make_cnf_disj_conj_l OF [thm1, thm2]  (* ((x1 & x2) | y') = ((x1 | y')' & (x2 | y')') *)
434 				end
435 			  | make_cnfx_disj_thm x' (Const ("op &", _) \$ y1 \$ y2) =
436 				let
437 					val thm1 = make_cnfx_disj_thm x' y1
438 					val thm2 = make_cnfx_disj_thm x' y2
439 				in
440 					make_cnf_disj_conj_r OF [thm1, thm2]  (* (x' | (y1 & y2)) = ((x' | y1)' & (x' | y2)') *)
441 				end
442 			  | make_cnfx_disj_thm (Const ("Ex", _) \$ x') y' =
443 				let
444 					val thm1 = inst_thm thy [x', y'] make_cnfx_disj_ex_l   (* ((Ex x') | y') = (Ex (x' | y')) *)
445 					val var  = new_free ()
446 					val thm2 = make_cnfx_disj_thm (betapply (x', var)) y'  (* (x' | y') = body' *)
447 					val thm3 = forall_intr (cterm_of thy var) thm2         (* !!v. (x' | y') = body' *)
448 					val thm4 = strip_shyps (thm3 COMP allI)                (* ALL v. (x' | y') = body' *)
449 					val thm5 = strip_shyps (thm4 RS make_cnfx_ex_cong)     (* (EX v. (x' | y')) = (EX v. body') *)
450 				in
451 					iff_trans OF [thm1, thm5]  (* ((Ex x') | y') = (Ex v. body') *)
452 				end
453 			  | make_cnfx_disj_thm x' (Const ("Ex", _) \$ y') =
454 				let
455 					val thm1 = inst_thm thy [x', y'] make_cnfx_disj_ex_r   (* (x' | (Ex y')) = (Ex (x' | y')) *)
456 					val var  = new_free ()
457 					val thm2 = make_cnfx_disj_thm x' (betapply (y', var))  (* (x' | y') = body' *)
458 					val thm3 = forall_intr (cterm_of thy var) thm2         (* !!v. (x' | y') = body' *)
459 					val thm4 = strip_shyps (thm3 COMP allI)                (* ALL v. (x' | y') = body' *)
460 					val thm5 = strip_shyps (thm4 RS make_cnfx_ex_cong)     (* (EX v. (x' | y')) = (EX v. body') *)
461 				in
462 					iff_trans OF [thm1, thm5]  (* (x' | (Ex y')) = (EX v. body') *)
463 				end
464 			  | make_cnfx_disj_thm x' y' =
465 				inst_thm thy [HOLogic.mk_disj (x', y')] iff_refl  (* (x' | y') = (x' | y') *)
466 			val thm1     = make_cnfx_thm_from_nnf x
467 			val thm2     = make_cnfx_thm_from_nnf y
468 			val x'       = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1
469 			val y'       = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm2
470 			val disj_thm = disj_cong OF [thm1, thm2]  (* (x | y) = (x' | y') *)
471 		in
472 			iff_trans OF [disj_thm, make_cnfx_disj_thm x' y']
473 		end else let  (* neither 'x' nor 'y' is a literal: introduce a fresh variable *)
474 			val thm1 = inst_thm thy [x, y] make_cnfx_newlit     (* (x | y) = EX v. (x | v) & (y | ~v) *)
475 			val var  = new_free ()
476 			val body = HOLogic.mk_conj (HOLogic.mk_disj (x, var), HOLogic.mk_disj (y, HOLogic.Not \$ var))
477 			val thm2 = make_cnfx_thm_from_nnf body              (* (x | v) & (y | ~v) = body' *)
478 			val thm3 = forall_intr (cterm_of thy var) thm2      (* !!v. (x | v) & (y | ~v) = body' *)
479 			val thm4 = strip_shyps (thm3 COMP allI)             (* ALL v. (x | v) & (y | ~v) = body' *)
480 			val thm5 = strip_shyps (thm4 RS make_cnfx_ex_cong)  (* (EX v. (x | v) & (y | ~v)) = (EX v. body') *)
481 		in
482 			iff_trans OF [thm1, thm5]
483 		end
484 	  | make_cnfx_thm_from_nnf t =
485 		inst_thm thy [t] iff_refl
486 	(* convert 't' to NNF first *)
487 	val nnf_thm  = make_nnf_thm thy t
488 	val nnf      = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) nnf_thm
489 	(* then simplify wrt. True/False (this should preserve NNF) *)
490 	val simp_thm = simp_True_False_thm thy nnf
491 	val simp     = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) simp_thm
492 	(* initialize var_id, in case the term already contains variables of the form "cnfx_<int>" *)
493 	val _        = (var_id := fold (fn free => fn max =>
494 		let
495 			val (name, _) = dest_Free free
496 			val idx       = if String.isPrefix "cnfx_" name then
497 					(Int.fromString o String.extract) (name, String.size "cnfx_", NONE)
498 				else
499 					NONE
500 		in
501 			Int.max (max, getOpt (idx, 0))
502 		end) (term_frees simp) 0)
503 	(* finally, convert to definitional CNF (this should preserve the simplification) *)
504 	val cnfx_thm = make_cnfx_thm_from_nnf simp
505 in
506 	iff_trans OF [iff_trans OF [nnf_thm, simp_thm], cnfx_thm]
507 end;
509 (* ------------------------------------------------------------------------- *)
510 (*                                  Tactics                                  *)
511 (* ------------------------------------------------------------------------- *)
513 (* ------------------------------------------------------------------------- *)
514 (* weakening_tac: removes the first hypothesis of the 'i'-th subgoal         *)
515 (* ------------------------------------------------------------------------- *)
517 (* int -> Tactical.tactic *)
519 fun weakening_tac i =
520 	dtac weakening_thm i THEN atac (i+1);
522 (* ------------------------------------------------------------------------- *)
523 (* cnf_rewrite_tac: converts all premises of the 'i'-th subgoal to CNF       *)
524 (*      (possibly causing an exponential blowup in the length of each        *)
525 (*      premise)                                                             *)
526 (* ------------------------------------------------------------------------- *)
528 (* int -> Tactical.tactic *)
530 fun cnf_rewrite_tac i =
531 	(* cut the CNF formulas as new premises *)
532 	METAHYPS (fn prems =>
533 		let
534 			val cnf_thms = map (fn pr => make_cnf_thm (theory_of_thm pr) ((HOLogic.dest_Trueprop o prop_of) pr)) prems
535 			val cut_thms = map (fn (th, pr) => cnftac_eq_imp OF [th, pr]) (cnf_thms ~~ prems)
536 		in
537 			cut_facts_tac cut_thms 1
538 		end) i
539 	(* remove the original premises *)
540 	THEN SELECT_GOAL (fn thm =>
541 		let
542 			val n = Logic.count_prems ((Term.strip_all_body o fst o Logic.dest_implies o prop_of) thm)
543 		in
544 			PRIMITIVE (funpow (n div 2) (Seq.hd o weakening_tac 1)) thm
545 		end) i;
547 (* ------------------------------------------------------------------------- *)
548 (* cnfx_rewrite_tac: converts all premises of the 'i'-th subgoal to CNF      *)
549 (*      (possibly introducing new literals)                                  *)
550 (* ------------------------------------------------------------------------- *)
552 (* int -> Tactical.tactic *)
554 fun cnfx_rewrite_tac i =
555 	(* cut the CNF formulas as new premises *)
556 	METAHYPS (fn prems =>
557 		let
558 			val cnfx_thms = map (fn pr => make_cnfx_thm (theory_of_thm pr) ((HOLogic.dest_Trueprop o prop_of) pr)) prems
559 			val cut_thms  = map (fn (th, pr) => cnftac_eq_imp OF [th, pr]) (cnfx_thms ~~ prems)
560 		in
561 			cut_facts_tac cut_thms 1
562 		end) i
563 	(* remove the original premises *)
564 	THEN SELECT_GOAL (fn thm =>
565 		let
566 			val n = Logic.count_prems ((Term.strip_all_body o fst o Logic.dest_implies o prop_of) thm)
567 		in
568 			PRIMITIVE (funpow (n div 2) (Seq.hd o weakening_tac 1)) thm
569 		end) i;
571 end;  (* of structure *)