src/HOL/Tools/cnf_funcs.ML

clauses now use (meta-)hyps instead of (meta-)implications; significant speedup

(*  Title:      HOL/Tools/cnf_funcs.ML
    ID:         $Id$
    Author:     Alwen Tiu, QSL Team, LORIA (http://qsl.loria.fr)
    Author:     Tjark Weber
    Copyright   2005-2006

  Description:
  This file contains functions and tactics to transform a formula into
  Conjunctive Normal Form (CNF).
  A formula in CNF is of the following form:

      (x11 | x12 | ... | x1n) & ... & (xm1 | xm2 | ... | xmk)
      False
      True

  where each xij is a literal (a positive or negative atomic Boolean term),
  i.e. the formula is a conjunction of disjunctions of literals, or
  "False", or "True".

  A (non-empty) disjunction of literals is referred to as "clause".

  For the purpose of SAT proof reconstruction, we also make use of another
  representation of clauses, which we call the "raw clauses".
  Raw clauses are of the form

      x1', x2', ..., xn', ~ (x1 | x2 | ... | xn) ==> False |- False ,

  where each xi is a literal, and each xi' is the negation normal form of ~xi.

  Raw clauses may contain further hyps of the form "~ clause ==> False".
  Literals are successively removed from the hyps of raw clauses by resolution
  during SAT proof reconstruction.
*)

signature CNF =
sig
	val is_atom           : Term.term -> bool
	val is_literal        : Term.term -> bool
	val is_clause         : Term.term -> bool
	val clause_is_trivial : Term.term -> bool

	val clause2raw_thm         : Thm.thm -> Thm.thm
	val rawhyps2clausehyps_thm : Thm.thm -> Thm.thm

	val weakening_tac : int -> Tactical.tactic  (* removes the first hypothesis of a subgoal *)

	val make_cnf_thm  : Theory.theory -> Term.term -> Thm.thm
	val make_cnfx_thm : Theory.theory -> Term.term ->  Thm.thm
	val cnf_rewrite_tac  : int -> Tactical.tactic  (* converts all prems of a subgoal to CNF *)
	val cnfx_rewrite_tac : int -> Tactical.tactic  (* converts all prems of a subgoal to (almost) definitional CNF *)
end;

structure cnf : CNF =
struct

(* string -> Thm.thm *)
fun thm_by_auto G =
	prove_goal (the_context ()) G (fn prems => [cut_facts_tac prems 1, Auto_tac]);

(* Thm.thm *)
val clause2raw_notE      = thm_by_auto "[| P; ~P |] ==> False";
val clause2raw_not_disj  = thm_by_auto "[| ~P; ~Q |] ==> ~(P | Q)";
val clause2raw_not_not   = thm_by_auto "P ==> ~~P";

val iff_refl             = thm_by_auto "(P::bool) = P";
val iff_trans            = thm_by_auto "[| (P::bool) = Q; Q = R |] ==> P = R";
val conj_cong            = thm_by_auto "[| P = P'; Q = Q' |] ==> (P & Q) = (P' & Q')";
val disj_cong            = thm_by_auto "[| P = P'; Q = Q' |] ==> (P | Q) = (P' | Q')";

val make_nnf_imp         = thm_by_auto "[| (~P) = P'; Q = Q' |] ==> (P --> Q) = (P' | Q')";
val make_nnf_iff         = thm_by_auto "[| P = P'; (~P) = NP; Q = Q'; (~Q) = NQ |] ==> (P = Q) = ((P' | NQ) & (NP | Q'))";
val make_nnf_not_false   = thm_by_auto "(~False) = True";
val make_nnf_not_true    = thm_by_auto "(~True) = False";
val make_nnf_not_conj    = thm_by_auto "[| (~P) = P'; (~Q) = Q' |] ==> (~(P & Q)) = (P' | Q')";
val make_nnf_not_disj    = thm_by_auto "[| (~P) = P'; (~Q) = Q' |] ==> (~(P | Q)) = (P' & Q')";
val make_nnf_not_imp     = thm_by_auto "[| P = P'; (~Q) = Q' |] ==> (~(P --> Q)) = (P' & Q')";
val make_nnf_not_iff     = thm_by_auto "[| P = P'; (~P) = NP; Q = Q'; (~Q) = NQ |] ==> (~(P = Q)) = ((P' | Q') & (NP | NQ))";
val make_nnf_not_not     = thm_by_auto "P = P' ==> (~~P) = P'";

val simp_TF_conj_True_l  = thm_by_auto "[| P = True; Q = Q' |] ==> (P & Q) = Q'";
val simp_TF_conj_True_r  = thm_by_auto "[| P = P'; Q = True |] ==> (P & Q) = P'";
val simp_TF_conj_False_l = thm_by_auto "P = False ==> (P & Q) = False";
val simp_TF_conj_False_r = thm_by_auto "Q = False ==> (P & Q) = False";
val simp_TF_disj_True_l  = thm_by_auto "P = True ==> (P | Q) = True";
val simp_TF_disj_True_r  = thm_by_auto "Q = True ==> (P | Q) = True";
val simp_TF_disj_False_l = thm_by_auto "[| P = False; Q = Q' |] ==> (P | Q) = Q'";
val simp_TF_disj_False_r = thm_by_auto "[| P = P'; Q = False |] ==> (P | Q) = P'";

val make_cnf_disj_conj_l = thm_by_auto "[| (P | R) = PR; (Q | R) = QR |] ==> ((P & Q) | R) = (PR & QR)";
val make_cnf_disj_conj_r = thm_by_auto "[| (P | Q) = PQ; (P | R) = PR |] ==> (P | (Q & R)) = (PQ & PR)";

val make_cnfx_disj_ex_l = thm_by_auto "((EX (x::bool). P x) | Q) = (EX x. P x | Q)";
val make_cnfx_disj_ex_r = thm_by_auto "(P | (EX (x::bool). Q x)) = (EX x. P | Q x)";
val make_cnfx_newlit    = thm_by_auto "(P | Q) = (EX x. (P | x) & (Q | ~x))";
val make_cnfx_ex_cong   = thm_by_auto "(ALL (x::bool). P x = Q x) ==> (EX x. P x) = (EX x. Q x)";

val weakening_thm        = thm_by_auto "[| P; Q |] ==> Q";

val cnftac_eq_imp        = thm_by_auto "[| P = Q; P |] ==> Q";

(* Term.term -> bool *)
fun is_atom (Const ("False", _))                                           = false
  | is_atom (Const ("True", _))                                            = false
  | is_atom (Const ("op &", _) $ _ $ _)                                    = false
  | is_atom (Const ("op |", _) $ _ $ _)                                    = false
  | is_atom (Const ("op -->", _) $ _ $ _)                                  = false
  | is_atom (Const ("op =", Type ("fun", Type ("bool", []) :: _)) $ _ $ _) = false
  | is_atom (Const ("Not", _) $ _)                                         = false
  | is_atom _                                                              = true;

(* Term.term -> bool *)
fun is_literal (Const ("Not", _) $ x) = is_atom x
  | is_literal x                      = is_atom x;

(* Term.term -> bool *)
fun is_clause (Const ("op |", _) $ x $ y) = is_clause x andalso is_clause y
  | is_clause x                           = is_literal x;

(* ------------------------------------------------------------------------- *)
(* clause_is_trivial: a clause is trivially true if it contains both an atom *)
(*      and the atom's negation                                              *)
(* ------------------------------------------------------------------------- *)

(* Term.term -> bool *)

fun clause_is_trivial c =
	let
		(* Term.term -> Term.term list -> Term.term list *)
		fun collect_literals (Const ("op |", _) $ x $ y) ls = collect_literals x (collect_literals y ls)
		  | collect_literals x                           ls = x :: ls
		(* Term.term -> Term.term *)
		fun dual (Const ("Not", _) $ x) = x
		  | dual x                      = HOLogic.Not $ x
		(* Term.term list -> bool *)
		fun has_duals []      = false
		  | has_duals (x::xs) = (dual x) mem xs orelse has_duals xs
	in
		has_duals (collect_literals c [])
	end;

(* ------------------------------------------------------------------------- *)
(* clause2raw_thm: translates a clause into a raw clause, i.e.               *)
(*        ... |- x1 | ... | xn                                               *)
(*      (where each xi is a literal) is translated to                        *)
(*        ~(x1 | ... | xn) ==> False, x1', ..., xn' |- False ,               *)
(*      where each xi' is the negation normal form of ~xi.                   *)
(* ------------------------------------------------------------------------- *)

(* Thm.thm -> Thm.thm *)

fun clause2raw_thm c =
let
	val disj               = HOLogic.dest_Trueprop (prop_of c)
	val not_disj_imp_false = Logic.mk_implies (HOLogic.mk_Trueprop (HOLogic.mk_not disj), HOLogic.mk_Trueprop HOLogic.false_const)
	val thm1 = Thm.assume (cterm_of (theory_of_thm c) not_disj_imp_false)  (* ~(x1 | ... | xn) ==> False |- ~(x1 | ... | xn) ==> False *)
	(* eliminates negated disjunctions from the i-th premise, possibly *)
	(* adding new premises, then continues with the (i+1)-th premise   *)
	(* Thm.thm -> int -> Thm.thm *)
	fun not_disj_to_prem thm i =
		if i > nprems_of thm then
			thm
		else
			not_disj_to_prem (Seq.hd (REPEAT_DETERM (rtac clause2raw_not_disj i) thm)) (i+1)
	val thm2 = not_disj_to_prem thm1 1  (* ~(x1 | ... | xn) ==> False |- ~x1 ==> ... ==> ~xn ==> False *)
	val thm3 = Seq.hd (TRYALL (rtac clause2raw_not_not) thm2)  (* ~(x1 | ... | xn) ==> False |- x1' ==> ... ==> xn' ==> False *)
	val thy3 = theory_of_thm thm3
	val thm4 = fold (fn prem => fn thm => Thm.implies_elim thm (Thm.assume (cterm_of thy3 prem))) (prems_of thm3) thm3  (* ~(x1 | ... | xn) ==> False, x1', ..., xn' |- False *)
in
	thm4
end;

(* ------------------------------------------------------------------------- *)
(* rawhyps2clausehyps_thm: translates all hyps of the form "~P ==> False" to *)
(*      hyps of the form "P"                                                 *)
(* ------------------------------------------------------------------------- *)

(* Thm.thm -> Thm.thm *)

fun rawhyps2clausehyps_thm c =
	fold (fn hyp => fn thm =>
		case hyp of Const ("==>", _) $ (Const ("Trueprop", _) $ (Const ("Not", _) $ P)) $ (Const ("Trueprop", _) $ Const ("False", _)) =>
			let
				val cterm = cterm_of (theory_of_thm thm)
				val thm1  = Thm.implies_intr (cterm hyp) thm  (* hyps |- (~P ==> False) ==> goal *)
				val varP  = Var (("P", 0), HOLogic.boolT)
				val notE  = Thm.instantiate ([], [(cterm varP, cterm P)]) clause2raw_notE  (* P ==> ~P ==> False *)
				val notE' = Thm.implies_elim notE (Thm.assume (cterm (HOLogic.mk_Trueprop P)))  (* P |- ~P ==> False *)
				val thm2  = Thm.implies_elim thm1 notE'  (* hyps, P |- goal *)
			in
				thm2
			end
		          | _                                                                                                                  =>
			thm) (#hyps (rep_thm c)) c;

(* ------------------------------------------------------------------------- *)
(* inst_thm: instantiates a theorem with a list of terms                     *)
(* ------------------------------------------------------------------------- *)

(* Theory.theory -> Term.term list -> Thm.thm -> Thm.thm *)

fun inst_thm thy ts thm =
	instantiate' [] (map (SOME o cterm_of thy) ts) thm;

(* ------------------------------------------------------------------------- *)
(*                         Naive CNF transformation                          *)
(* ------------------------------------------------------------------------- *)

(* ------------------------------------------------------------------------- *)
(* make_nnf_thm: produces a theorem of the form t = t', where t' is the      *)
(*      negation normal form (i.e. negation only occurs in front of atoms)   *)
(*      of t; implications ("-->") and equivalences ("=" on bool) are        *)
(*      eliminated (possibly causing an exponential blowup)                  *)
(* ------------------------------------------------------------------------- *)

(* Theory.theory -> Term.term -> Thm.thm *)

fun make_nnf_thm thy (Const ("op &", _) $ x $ y) =
	let
		val thm1 = make_nnf_thm thy x
		val thm2 = make_nnf_thm thy y
	in
		conj_cong OF [thm1, thm2]
	end
  | make_nnf_thm thy (Const ("op |", _) $ x $ y) =
	let
		val thm1 = make_nnf_thm thy x
		val thm2 = make_nnf_thm thy y
	in
		disj_cong OF [thm1, thm2]
	end
  | make_nnf_thm thy (Const ("op -->", _) $ x $ y) =
	let
		val thm1 = make_nnf_thm thy (HOLogic.Not $ x)
		val thm2 = make_nnf_thm thy y
	in
		make_nnf_imp OF [thm1, thm2]
	end
  | make_nnf_thm thy (Const ("op =", Type ("fun", Type ("bool", []) :: _)) $ x $ y) =
	let
		val thm1 = make_nnf_thm thy x
		val thm2 = make_nnf_thm thy (HOLogic.Not $ x)
		val thm3 = make_nnf_thm thy y
		val thm4 = make_nnf_thm thy (HOLogic.Not $ y)
	in
		make_nnf_iff OF [thm1, thm2, thm3, thm4]
	end
  | make_nnf_thm thy (Const ("Not", _) $ Const ("False", _)) =
	make_nnf_not_false
  | make_nnf_thm thy (Const ("Not", _) $ Const ("True", _)) =
	make_nnf_not_true
  | make_nnf_thm thy (Const ("Not", _) $ (Const ("op &", _) $ x $ y)) =
	let
		val thm1 = make_nnf_thm thy (HOLogic.Not $ x)
		val thm2 = make_nnf_thm thy (HOLogic.Not $ y)
	in
		make_nnf_not_conj OF [thm1, thm2]
	end
  | make_nnf_thm thy (Const ("Not", _) $ (Const ("op |", _) $ x $ y)) =
	let
		val thm1 = make_nnf_thm thy (HOLogic.Not $ x)
		val thm2 = make_nnf_thm thy (HOLogic.Not $ y)
	in
		make_nnf_not_disj OF [thm1, thm2]
	end
  | make_nnf_thm thy (Const ("Not", _) $ (Const ("op -->", _) $ x $ y)) =
	let
		val thm1 = make_nnf_thm thy x
		val thm2 = make_nnf_thm thy (HOLogic.Not $ y)
	in
		make_nnf_not_imp OF [thm1, thm2]
	end
  | make_nnf_thm thy (Const ("Not", _) $ (Const ("op =", Type ("fun", Type ("bool", []) :: _)) $ x $ y)) =
	let
		val thm1 = make_nnf_thm thy x
		val thm2 = make_nnf_thm thy (HOLogic.Not $ x)
		val thm3 = make_nnf_thm thy y
		val thm4 = make_nnf_thm thy (HOLogic.Not $ y)
	in
		make_nnf_not_iff OF [thm1, thm2, thm3, thm4]
	end
  | make_nnf_thm thy (Const ("Not", _) $ (Const ("Not", _) $ x)) =
	let
		val thm1 = make_nnf_thm thy x
	in
		make_nnf_not_not OF [thm1]
	end
  | make_nnf_thm thy t =
	inst_thm thy [t] iff_refl;

(* ------------------------------------------------------------------------- *)
(* simp_True_False_thm: produces a theorem t = t', where t' is equivalent to *)
(*      t, but simplified wrt. the following theorems:                       *)
(*        (True & x) = x                                                     *)
(*        (x & True) = x                                                     *)
(*        (False & x) = False                                                *)
(*        (x & False) = False                                                *)
(*        (True | x) = True                                                  *)
(*        (x | True) = True                                                  *)
(*        (False | x) = x                                                    *)
(*        (x | False) = x                                                    *)
(*      No simplification is performed below connectives other than & and |. *)
(*      Optimization: The right-hand side of a conjunction (disjunction) is  *)
(*      simplified only if the left-hand side does not simplify to False     *)
(*      (True, respectively).                                                *)
(* ------------------------------------------------------------------------- *)

(* Theory.theory -> Term.term -> Thm.thm *)

fun simp_True_False_thm thy (Const ("op &", _) $ x $ y) =
	let
		val thm1 = simp_True_False_thm thy x
		val x'   = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1
	in
		if x' = HOLogic.false_const then
			simp_TF_conj_False_l OF [thm1]  (* (x & y) = False *)
		else
			let
				val thm2 = simp_True_False_thm thy y
				val y'   = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm2
			in
				if x' = HOLogic.true_const then
					simp_TF_conj_True_l OF [thm1, thm2]  (* (x & y) = y' *)
				else if y' = HOLogic.false_const then
					simp_TF_conj_False_r OF [thm2]  (* (x & y) = False *)
				else if y' = HOLogic.true_const then
					simp_TF_conj_True_r OF [thm1, thm2]  (* (x & y) = x' *)
				else
					conj_cong OF [thm1, thm2]  (* (x & y) = (x' & y') *)
			end
	end
  | simp_True_False_thm thy (Const ("op |", _) $ x $ y) =
	let
		val thm1 = simp_True_False_thm thy x
		val x'   = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1
	in
		if x' = HOLogic.true_const then
			simp_TF_disj_True_l OF [thm1]  (* (x | y) = True *)
		else
			let
				val thm2 = simp_True_False_thm thy y
				val y'   = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm2
			in
				if x' = HOLogic.false_const then
					simp_TF_disj_False_l OF [thm1, thm2]  (* (x | y) = y' *)
				else if y' = HOLogic.true_const then
					simp_TF_disj_True_r OF [thm2]  (* (x | y) = True *)
				else if y' = HOLogic.false_const then
					simp_TF_disj_False_r OF [thm1, thm2]  (* (x | y) = x' *)
				else
					disj_cong OF [thm1, thm2]  (* (x | y) = (x' | y') *)
			end
	end
  | simp_True_False_thm thy t =
	inst_thm thy [t] iff_refl;  (* t = t *)

(* ------------------------------------------------------------------------- *)
(* make_cnf_thm: given any HOL term 't', produces a theorem t = t', where t' *)
(*      is in conjunction normal form.  May cause an exponential blowup      *)
(*      in the length of the term.                                           *)
(* ------------------------------------------------------------------------- *)

(* Theory.theory -> Term.term -> Thm.thm *)

fun make_cnf_thm thy t =
let
	(* Term.term -> Thm.thm *)
	fun make_cnf_thm_from_nnf (Const ("op &", _) $ x $ y) =
		let
			val thm1 = make_cnf_thm_from_nnf x
			val thm2 = make_cnf_thm_from_nnf y
		in
			conj_cong OF [thm1, thm2]
		end
	  | make_cnf_thm_from_nnf (Const ("op |", _) $ x $ y) =
		let
			(* produces a theorem "(x' | y') = t'", where x', y', and t' are in CNF *)
			fun make_cnf_disj_thm (Const ("op &", _) $ x1 $ x2) y' =
				let
					val thm1 = make_cnf_disj_thm x1 y'
					val thm2 = make_cnf_disj_thm x2 y'
				in
					make_cnf_disj_conj_l OF [thm1, thm2]  (* ((x1 & x2) | y') = ((x1 | y')' & (x2 | y')') *)
				end
			  | make_cnf_disj_thm x' (Const ("op &", _) $ y1 $ y2) =
				let
					val thm1 = make_cnf_disj_thm x' y1
					val thm2 = make_cnf_disj_thm x' y2
				in
					make_cnf_disj_conj_r OF [thm1, thm2]  (* (x' | (y1 & y2)) = ((x' | y1)' & (x' | y2)') *)
				end
			  | make_cnf_disj_thm x' y' =
				inst_thm thy [HOLogic.mk_disj (x', y')] iff_refl  (* (x' | y') = (x' | y') *)
			val thm1     = make_cnf_thm_from_nnf x
			val thm2     = make_cnf_thm_from_nnf y
			val x'       = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1
			val y'       = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm2
			val disj_thm = disj_cong OF [thm1, thm2]  (* (x | y) = (x' | y') *)
		in
			iff_trans OF [disj_thm, make_cnf_disj_thm x' y']
		end
	  | make_cnf_thm_from_nnf t =
		inst_thm thy [t] iff_refl
	(* convert 't' to NNF first *)
	val nnf_thm  = make_nnf_thm thy t
	val nnf      = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) nnf_thm
	(* then simplify wrt. True/False (this should preserve NNF) *)
	val simp_thm = simp_True_False_thm thy nnf
	val simp     = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) simp_thm
	(* finally, convert to CNF (this should preserve the simplification) *)
	val cnf_thm  = make_cnf_thm_from_nnf simp
in
	iff_trans OF [iff_trans OF [nnf_thm, simp_thm], cnf_thm]
end;

(* ------------------------------------------------------------------------- *)
(*            CNF transformation by introducing new literals                 *)
(* ------------------------------------------------------------------------- *)

(* ------------------------------------------------------------------------- *)
(* make_cnfx_thm: given any HOL term 't', produces a theorem t = t', where   *)
(*      t' is almost in conjunction normal form, except that conjunctions    *)
(*      and existential quantifiers may be nested.  (Use e.g. 'REPEAT_DETERM *)
(*      (etac exE i ORELSE etac conjE i)' afterwards to normalize.)  May     *)
(*      introduce new (existentially bound) literals.  Note: the current     *)
(*      implementation calls 'make_nnf_thm', causing an exponential blowup   *)
(*      in the case of nested equivalences.                                  *)
(* ------------------------------------------------------------------------- *)

(* Theory.theory -> Term.term -> Thm.thm *)

fun make_cnfx_thm thy t =
let
	val var_id = ref 0  (* properly initialized below *)
	(* unit -> Term.term *)
	fun new_free () =
		Free ("cnfx_" ^ string_of_int (inc var_id), HOLogic.boolT)
	(* Term.term -> Thm.thm *)
	fun make_cnfx_thm_from_nnf (Const ("op &", _) $ x $ y) =
		let
			val thm1 = make_cnfx_thm_from_nnf x
			val thm2 = make_cnfx_thm_from_nnf y
		in
			conj_cong OF [thm1, thm2]
		end
	  | make_cnfx_thm_from_nnf (Const ("op |", _) $ x $ y) =
		if is_clause x andalso is_clause y then
			inst_thm thy [HOLogic.mk_disj (x, y)] iff_refl
		else if is_literal y orelse is_literal x then let
			(* produces a theorem "(x' | y') = t'", where x', y', and t' are *)
			(* almost in CNF, and x' or y' is a literal                      *)
			fun make_cnfx_disj_thm (Const ("op &", _) $ x1 $ x2) y' =
				let
					val thm1 = make_cnfx_disj_thm x1 y'
					val thm2 = make_cnfx_disj_thm x2 y'
				in
					make_cnf_disj_conj_l OF [thm1, thm2]  (* ((x1 & x2) | y') = ((x1 | y')' & (x2 | y')') *)
				end
			  | make_cnfx_disj_thm x' (Const ("op &", _) $ y1 $ y2) =
				let
					val thm1 = make_cnfx_disj_thm x' y1
					val thm2 = make_cnfx_disj_thm x' y2
				in
					make_cnf_disj_conj_r OF [thm1, thm2]  (* (x' | (y1 & y2)) = ((x' | y1)' & (x' | y2)') *)
				end
			  | make_cnfx_disj_thm (Const ("Ex", _) $ x') y' =
				let
					val thm1 = inst_thm thy [x', y'] make_cnfx_disj_ex_l   (* ((Ex x') | y') = (Ex (x' | y')) *)
					val var  = new_free ()
					val thm2 = make_cnfx_disj_thm (betapply (x', var)) y'  (* (x' | y') = body' *)
					val thm3 = forall_intr (cterm_of thy var) thm2         (* !!v. (x' | y') = body' *)
					val thm4 = strip_shyps (thm3 COMP allI)                (* ALL v. (x' | y') = body' *)
					val thm5 = strip_shyps (thm4 RS make_cnfx_ex_cong)     (* (EX v. (x' | y')) = (EX v. body') *)
				in
					iff_trans OF [thm1, thm5]  (* ((Ex x') | y') = (Ex v. body') *)
				end
			  | make_cnfx_disj_thm x' (Const ("Ex", _) $ y') =
				let
					val thm1 = inst_thm thy [x', y'] make_cnfx_disj_ex_r   (* (x' | (Ex y')) = (Ex (x' | y')) *)
					val var  = new_free ()
					val thm2 = make_cnfx_disj_thm x' (betapply (y', var))  (* (x' | y') = body' *)
					val thm3 = forall_intr (cterm_of thy var) thm2         (* !!v. (x' | y') = body' *)
					val thm4 = strip_shyps (thm3 COMP allI)                (* ALL v. (x' | y') = body' *)
					val thm5 = strip_shyps (thm4 RS make_cnfx_ex_cong)     (* (EX v. (x' | y')) = (EX v. body') *)
				in
					iff_trans OF [thm1, thm5]  (* (x' | (Ex y')) = (EX v. body') *)
				end
			  | make_cnfx_disj_thm x' y' =
				inst_thm thy [HOLogic.mk_disj (x', y')] iff_refl  (* (x' | y') = (x' | y') *)
			val thm1     = make_cnfx_thm_from_nnf x
			val thm2     = make_cnfx_thm_from_nnf y
			val x'       = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1
			val y'       = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm2
			val disj_thm = disj_cong OF [thm1, thm2]  (* (x | y) = (x' | y') *)
		in
			iff_trans OF [disj_thm, make_cnfx_disj_thm x' y']
		end else let  (* neither 'x' nor 'y' is a literal: introduce a fresh variable *)
			val thm1 = inst_thm thy [x, y] make_cnfx_newlit     (* (x | y) = EX v. (x | v) & (y | ~v) *)
			val var  = new_free ()
			val body = HOLogic.mk_conj (HOLogic.mk_disj (x, var), HOLogic.mk_disj (y, HOLogic.Not $ var))
			val thm2 = make_cnfx_thm_from_nnf body              (* (x | v) & (y | ~v) = body' *)
			val thm3 = forall_intr (cterm_of thy var) thm2      (* !!v. (x | v) & (y | ~v) = body' *)
			val thm4 = strip_shyps (thm3 COMP allI)             (* ALL v. (x | v) & (y | ~v) = body' *)
			val thm5 = strip_shyps (thm4 RS make_cnfx_ex_cong)  (* (EX v. (x | v) & (y | ~v)) = (EX v. body') *)
		in
			iff_trans OF [thm1, thm5]
		end
	  | make_cnfx_thm_from_nnf t =
		inst_thm thy [t] iff_refl
	(* convert 't' to NNF first *)
	val nnf_thm  = make_nnf_thm thy t
	val nnf      = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) nnf_thm
	(* then simplify wrt. True/False (this should preserve NNF) *)
	val simp_thm = simp_True_False_thm thy nnf
	val simp     = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) simp_thm
	(* initialize var_id, in case the term already contains variables of the form "cnfx_<int>" *)
	val _        = (var_id := fold (fn free => fn max =>
		let
			val (name, _) = dest_Free free
			val idx       = if String.isPrefix "cnfx_" name then
					(Int.fromString o String.extract) (name, String.size "cnfx_", NONE)
				else
					NONE
		in
			Int.max (max, getOpt (idx, 0))
		end) (term_frees simp) 0)
	(* finally, convert to definitional CNF (this should preserve the simplification) *)
	val cnfx_thm = make_cnfx_thm_from_nnf simp
in
	iff_trans OF [iff_trans OF [nnf_thm, simp_thm], cnfx_thm]
end;

(* ------------------------------------------------------------------------- *)
(*                                  Tactics                                  *)
(* ------------------------------------------------------------------------- *)

(* ------------------------------------------------------------------------- *)
(* weakening_tac: removes the first hypothesis of the 'i'-th subgoal         *)
(* ------------------------------------------------------------------------- *)

(* int -> Tactical.tactic *)

fun weakening_tac i =
	dtac weakening_thm i THEN atac (i+1);

(* ------------------------------------------------------------------------- *)
(* cnf_rewrite_tac: converts all premises of the 'i'-th subgoal to CNF       *)
(*      (possibly causing an exponential blowup in the length of each        *)
(*      premise)                                                             *)
(* ------------------------------------------------------------------------- *)

(* int -> Tactical.tactic *)

fun cnf_rewrite_tac i =
	(* cut the CNF formulas as new premises *)
	METAHYPS (fn prems =>
		let
			val cnf_thms = map (fn pr => make_cnf_thm (theory_of_thm pr) ((HOLogic.dest_Trueprop o prop_of) pr)) prems
			val cut_thms = map (fn (th, pr) => cnftac_eq_imp OF [th, pr]) (cnf_thms ~~ prems)
		in
			cut_facts_tac cut_thms 1
		end) i
	(* remove the original premises *)
	THEN SELECT_GOAL (fn thm =>
		let
			val n = Logic.count_prems ((Term.strip_all_body o fst o Logic.dest_implies o prop_of) thm, 0)
		in
			PRIMITIVE (funpow (n div 2) (Seq.hd o weakening_tac 1)) thm
		end) i;

(* ------------------------------------------------------------------------- *)
(* cnfx_rewrite_tac: converts all premises of the 'i'-th subgoal to CNF      *)
(*      (possibly introducing new literals)                                  *)
(* ------------------------------------------------------------------------- *)

(* int -> Tactical.tactic *)

fun cnfx_rewrite_tac i =
	(* cut the CNF formulas as new premises *)
	METAHYPS (fn prems =>
		let
			val cnfx_thms = map (fn pr => make_cnfx_thm (theory_of_thm pr) ((HOLogic.dest_Trueprop o prop_of) pr)) prems
			val cut_thms  = map (fn (th, pr) => cnftac_eq_imp OF [th, pr]) (cnfx_thms ~~ prems)
		in
			cut_facts_tac cut_thms 1
		end) i
	(* remove the original premises *)
	THEN SELECT_GOAL (fn thm =>
		let
			val n = Logic.count_prems ((Term.strip_all_body o fst o Logic.dest_implies o prop_of) thm, 0)
		in
			PRIMITIVE (funpow (n div 2) (Seq.hd o weakening_tac 1)) thm
		end) i;

end;  (* of structure *)