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