src/HOL/Tools/cnf_funcs.ML
author wenzelm
Wed Nov 29 04:11:09 2006 +0100 (2006-11-29)
changeset 21576 8c11b1ce2f05
parent 20547 796ae7fa1049
child 24958 ff15f76741bd
permissions -rw-r--r--
simplified Logic.count_prems;
     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 -> Term.term -> Thm.thm
    46 	val make_cnfx_thm : 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 fun inst_thm thy ts thm =
   180 	instantiate' [] (map (SOME o cterm_of thy) ts) thm;
   181 
   182 (* ------------------------------------------------------------------------- *)
   183 (*                         Naive CNF transformation                          *)
   184 (* ------------------------------------------------------------------------- *)
   185 
   186 (* ------------------------------------------------------------------------- *)
   187 (* make_nnf_thm: produces a theorem of the form t = t', where t' is the      *)
   188 (*      negation normal form (i.e. negation only occurs in front of atoms)   *)
   189 (*      of t; implications ("-->") and equivalences ("=" on bool) are        *)
   190 (*      eliminated (possibly causing an exponential blowup)                  *)
   191 (* ------------------------------------------------------------------------- *)
   192 
   193 (* Theory.theory -> Term.term -> Thm.thm *)
   194 
   195 fun make_nnf_thm thy (Const ("op &", _) $ x $ y) =
   196 	let
   197 		val thm1 = make_nnf_thm thy x
   198 		val thm2 = make_nnf_thm thy y
   199 	in
   200 		conj_cong OF [thm1, thm2]
   201 	end
   202   | make_nnf_thm thy (Const ("op |", _) $ x $ y) =
   203 	let
   204 		val thm1 = make_nnf_thm thy x
   205 		val thm2 = make_nnf_thm thy y
   206 	in
   207 		disj_cong OF [thm1, thm2]
   208 	end
   209   | make_nnf_thm thy (Const ("op -->", _) $ x $ y) =
   210 	let
   211 		val thm1 = make_nnf_thm thy (HOLogic.Not $ x)
   212 		val thm2 = make_nnf_thm thy y
   213 	in
   214 		make_nnf_imp OF [thm1, thm2]
   215 	end
   216   | make_nnf_thm thy (Const ("op =", Type ("fun", Type ("bool", []) :: _)) $ x $ y) =
   217 	let
   218 		val thm1 = make_nnf_thm thy x
   219 		val thm2 = make_nnf_thm thy (HOLogic.Not $ x)
   220 		val thm3 = make_nnf_thm thy y
   221 		val thm4 = make_nnf_thm thy (HOLogic.Not $ y)
   222 	in
   223 		make_nnf_iff OF [thm1, thm2, thm3, thm4]
   224 	end
   225   | make_nnf_thm thy (Const ("Not", _) $ Const ("False", _)) =
   226 	make_nnf_not_false
   227   | make_nnf_thm thy (Const ("Not", _) $ Const ("True", _)) =
   228 	make_nnf_not_true
   229   | make_nnf_thm thy (Const ("Not", _) $ (Const ("op &", _) $ x $ y)) =
   230 	let
   231 		val thm1 = make_nnf_thm thy (HOLogic.Not $ x)
   232 		val thm2 = make_nnf_thm thy (HOLogic.Not $ y)
   233 	in
   234 		make_nnf_not_conj OF [thm1, thm2]
   235 	end
   236   | make_nnf_thm thy (Const ("Not", _) $ (Const ("op |", _) $ x $ y)) =
   237 	let
   238 		val thm1 = make_nnf_thm thy (HOLogic.Not $ x)
   239 		val thm2 = make_nnf_thm thy (HOLogic.Not $ y)
   240 	in
   241 		make_nnf_not_disj OF [thm1, thm2]
   242 	end
   243   | make_nnf_thm thy (Const ("Not", _) $ (Const ("op -->", _) $ x $ y)) =
   244 	let
   245 		val thm1 = make_nnf_thm thy x
   246 		val thm2 = make_nnf_thm thy (HOLogic.Not $ y)
   247 	in
   248 		make_nnf_not_imp OF [thm1, thm2]
   249 	end
   250   | make_nnf_thm thy (Const ("Not", _) $ (Const ("op =", Type ("fun", Type ("bool", []) :: _)) $ x $ y)) =
   251 	let
   252 		val thm1 = make_nnf_thm thy x
   253 		val thm2 = make_nnf_thm thy (HOLogic.Not $ x)
   254 		val thm3 = make_nnf_thm thy y
   255 		val thm4 = make_nnf_thm thy (HOLogic.Not $ y)
   256 	in
   257 		make_nnf_not_iff OF [thm1, thm2, thm3, thm4]
   258 	end
   259   | make_nnf_thm thy (Const ("Not", _) $ (Const ("Not", _) $ x)) =
   260 	let
   261 		val thm1 = make_nnf_thm thy x
   262 	in
   263 		make_nnf_not_not OF [thm1]
   264 	end
   265   | make_nnf_thm thy t =
   266 	inst_thm thy [t] iff_refl;
   267 
   268 (* ------------------------------------------------------------------------- *)
   269 (* simp_True_False_thm: produces a theorem t = t', where t' is equivalent to *)
   270 (*      t, but simplified wrt. the following theorems:                       *)
   271 (*        (True & x) = x                                                     *)
   272 (*        (x & True) = x                                                     *)
   273 (*        (False & x) = False                                                *)
   274 (*        (x & False) = False                                                *)
   275 (*        (True | x) = True                                                  *)
   276 (*        (x | True) = True                                                  *)
   277 (*        (False | x) = x                                                    *)
   278 (*        (x | False) = x                                                    *)
   279 (*      No simplification is performed below connectives other than & and |. *)
   280 (*      Optimization: The right-hand side of a conjunction (disjunction) is  *)
   281 (*      simplified only if the left-hand side does not simplify to False     *)
   282 (*      (True, respectively).                                                *)
   283 (* ------------------------------------------------------------------------- *)
   284 
   285 (* Theory.theory -> Term.term -> Thm.thm *)
   286 
   287 fun simp_True_False_thm thy (Const ("op &", _) $ x $ y) =
   288 	let
   289 		val thm1 = simp_True_False_thm thy x
   290 		val x'   = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1
   291 	in
   292 		if x' = HOLogic.false_const then
   293 			simp_TF_conj_False_l OF [thm1]  (* (x & y) = False *)
   294 		else
   295 			let
   296 				val thm2 = simp_True_False_thm thy y
   297 				val y'   = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm2
   298 			in
   299 				if x' = HOLogic.true_const then
   300 					simp_TF_conj_True_l OF [thm1, thm2]  (* (x & y) = y' *)
   301 				else if y' = HOLogic.false_const then
   302 					simp_TF_conj_False_r OF [thm2]  (* (x & y) = False *)
   303 				else if y' = HOLogic.true_const then
   304 					simp_TF_conj_True_r OF [thm1, thm2]  (* (x & y) = x' *)
   305 				else
   306 					conj_cong OF [thm1, thm2]  (* (x & y) = (x' & y') *)
   307 			end
   308 	end
   309   | simp_True_False_thm thy (Const ("op |", _) $ x $ y) =
   310 	let
   311 		val thm1 = simp_True_False_thm thy x
   312 		val x'   = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1
   313 	in
   314 		if x' = HOLogic.true_const then
   315 			simp_TF_disj_True_l OF [thm1]  (* (x | y) = True *)
   316 		else
   317 			let
   318 				val thm2 = simp_True_False_thm thy y
   319 				val y'   = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm2
   320 			in
   321 				if x' = HOLogic.false_const then
   322 					simp_TF_disj_False_l OF [thm1, thm2]  (* (x | y) = y' *)
   323 				else if y' = HOLogic.true_const then
   324 					simp_TF_disj_True_r OF [thm2]  (* (x | y) = True *)
   325 				else if y' = HOLogic.false_const then
   326 					simp_TF_disj_False_r OF [thm1, thm2]  (* (x | y) = x' *)
   327 				else
   328 					disj_cong OF [thm1, thm2]  (* (x | y) = (x' | y') *)
   329 			end
   330 	end
   331   | simp_True_False_thm thy t =
   332 	inst_thm thy [t] iff_refl;  (* t = t *)
   333 
   334 (* ------------------------------------------------------------------------- *)
   335 (* make_cnf_thm: given any HOL term 't', produces a theorem t = t', where t' *)
   336 (*      is in conjunction normal form.  May cause an exponential blowup      *)
   337 (*      in the length of the term.                                           *)
   338 (* ------------------------------------------------------------------------- *)
   339 
   340 (* Theory.theory -> Term.term -> Thm.thm *)
   341 
   342 fun make_cnf_thm thy t =
   343 let
   344 	(* Term.term -> Thm.thm *)
   345 	fun make_cnf_thm_from_nnf (Const ("op &", _) $ x $ y) =
   346 		let
   347 			val thm1 = make_cnf_thm_from_nnf x
   348 			val thm2 = make_cnf_thm_from_nnf y
   349 		in
   350 			conj_cong OF [thm1, thm2]
   351 		end
   352 	  | make_cnf_thm_from_nnf (Const ("op |", _) $ x $ y) =
   353 		let
   354 			(* produces a theorem "(x' | y') = t'", where x', y', and t' are in CNF *)
   355 			fun make_cnf_disj_thm (Const ("op &", _) $ x1 $ x2) y' =
   356 				let
   357 					val thm1 = make_cnf_disj_thm x1 y'
   358 					val thm2 = make_cnf_disj_thm x2 y'
   359 				in
   360 					make_cnf_disj_conj_l OF [thm1, thm2]  (* ((x1 & x2) | y') = ((x1 | y')' & (x2 | y')') *)
   361 				end
   362 			  | make_cnf_disj_thm x' (Const ("op &", _) $ y1 $ y2) =
   363 				let
   364 					val thm1 = make_cnf_disj_thm x' y1
   365 					val thm2 = make_cnf_disj_thm x' y2
   366 				in
   367 					make_cnf_disj_conj_r OF [thm1, thm2]  (* (x' | (y1 & y2)) = ((x' | y1)' & (x' | y2)') *)
   368 				end
   369 			  | make_cnf_disj_thm x' y' =
   370 				inst_thm thy [HOLogic.mk_disj (x', y')] iff_refl  (* (x' | y') = (x' | y') *)
   371 			val thm1     = make_cnf_thm_from_nnf x
   372 			val thm2     = make_cnf_thm_from_nnf y
   373 			val x'       = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1
   374 			val y'       = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm2
   375 			val disj_thm = disj_cong OF [thm1, thm2]  (* (x | y) = (x' | y') *)
   376 		in
   377 			iff_trans OF [disj_thm, make_cnf_disj_thm x' y']
   378 		end
   379 	  | make_cnf_thm_from_nnf t =
   380 		inst_thm thy [t] iff_refl
   381 	(* convert 't' to NNF first *)
   382 	val nnf_thm  = make_nnf_thm thy t
   383 	val nnf      = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) nnf_thm
   384 	(* then simplify wrt. True/False (this should preserve NNF) *)
   385 	val simp_thm = simp_True_False_thm thy nnf
   386 	val simp     = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) simp_thm
   387 	(* finally, convert to CNF (this should preserve the simplification) *)
   388 	val cnf_thm  = make_cnf_thm_from_nnf simp
   389 in
   390 	iff_trans OF [iff_trans OF [nnf_thm, simp_thm], cnf_thm]
   391 end;
   392 
   393 (* ------------------------------------------------------------------------- *)
   394 (*            CNF transformation by introducing new literals                 *)
   395 (* ------------------------------------------------------------------------- *)
   396 
   397 (* ------------------------------------------------------------------------- *)
   398 (* make_cnfx_thm: given any HOL term 't', produces a theorem t = t', where   *)
   399 (*      t' is almost in conjunction normal form, except that conjunctions    *)
   400 (*      and existential quantifiers may be nested.  (Use e.g. 'REPEAT_DETERM *)
   401 (*      (etac exE i ORELSE etac conjE i)' afterwards to normalize.)  May     *)
   402 (*      introduce new (existentially bound) literals.  Note: the current     *)
   403 (*      implementation calls 'make_nnf_thm', causing an exponential blowup   *)
   404 (*      in the case of nested equivalences.                                  *)
   405 (* ------------------------------------------------------------------------- *)
   406 
   407 (* Theory.theory -> Term.term -> Thm.thm *)
   408 
   409 fun make_cnfx_thm thy t =
   410 let
   411 	val var_id = ref 0  (* properly initialized below *)
   412 	(* unit -> Term.term *)
   413 	fun new_free () =
   414 		Free ("cnfx_" ^ string_of_int (inc var_id), HOLogic.boolT)
   415 	(* Term.term -> Thm.thm *)
   416 	fun make_cnfx_thm_from_nnf (Const ("op &", _) $ x $ y) =
   417 		let
   418 			val thm1 = make_cnfx_thm_from_nnf x
   419 			val thm2 = make_cnfx_thm_from_nnf y
   420 		in
   421 			conj_cong OF [thm1, thm2]
   422 		end
   423 	  | make_cnfx_thm_from_nnf (Const ("op |", _) $ x $ y) =
   424 		if is_clause x andalso is_clause y then
   425 			inst_thm thy [HOLogic.mk_disj (x, y)] iff_refl
   426 		else if is_literal y orelse is_literal x then let
   427 			(* produces a theorem "(x' | y') = t'", where x', y', and t' are *)
   428 			(* almost in CNF, and x' or y' is a literal                      *)
   429 			fun make_cnfx_disj_thm (Const ("op &", _) $ x1 $ x2) y' =
   430 				let
   431 					val thm1 = make_cnfx_disj_thm x1 y'
   432 					val thm2 = make_cnfx_disj_thm x2 y'
   433 				in
   434 					make_cnf_disj_conj_l OF [thm1, thm2]  (* ((x1 & x2) | y') = ((x1 | y')' & (x2 | y')') *)
   435 				end
   436 			  | make_cnfx_disj_thm x' (Const ("op &", _) $ y1 $ y2) =
   437 				let
   438 					val thm1 = make_cnfx_disj_thm x' y1
   439 					val thm2 = make_cnfx_disj_thm x' y2
   440 				in
   441 					make_cnf_disj_conj_r OF [thm1, thm2]  (* (x' | (y1 & y2)) = ((x' | y1)' & (x' | y2)') *)
   442 				end
   443 			  | make_cnfx_disj_thm (Const ("Ex", _) $ x') y' =
   444 				let
   445 					val thm1 = inst_thm thy [x', y'] make_cnfx_disj_ex_l   (* ((Ex x') | y') = (Ex (x' | y')) *)
   446 					val var  = new_free ()
   447 					val thm2 = make_cnfx_disj_thm (betapply (x', var)) y'  (* (x' | y') = body' *)
   448 					val thm3 = forall_intr (cterm_of thy var) thm2         (* !!v. (x' | y') = body' *)
   449 					val thm4 = strip_shyps (thm3 COMP allI)                (* ALL v. (x' | y') = body' *)
   450 					val thm5 = strip_shyps (thm4 RS make_cnfx_ex_cong)     (* (EX v. (x' | y')) = (EX v. body') *)
   451 				in
   452 					iff_trans OF [thm1, thm5]  (* ((Ex x') | y') = (Ex v. body') *)
   453 				end
   454 			  | make_cnfx_disj_thm x' (Const ("Ex", _) $ y') =
   455 				let
   456 					val thm1 = inst_thm thy [x', y'] make_cnfx_disj_ex_r   (* (x' | (Ex y')) = (Ex (x' | y')) *)
   457 					val var  = new_free ()
   458 					val thm2 = make_cnfx_disj_thm x' (betapply (y', var))  (* (x' | y') = body' *)
   459 					val thm3 = forall_intr (cterm_of thy var) thm2         (* !!v. (x' | y') = body' *)
   460 					val thm4 = strip_shyps (thm3 COMP allI)                (* ALL v. (x' | y') = body' *)
   461 					val thm5 = strip_shyps (thm4 RS make_cnfx_ex_cong)     (* (EX v. (x' | y')) = (EX v. body') *)
   462 				in
   463 					iff_trans OF [thm1, thm5]  (* (x' | (Ex y')) = (EX v. body') *)
   464 				end
   465 			  | make_cnfx_disj_thm x' y' =
   466 				inst_thm thy [HOLogic.mk_disj (x', y')] iff_refl  (* (x' | y') = (x' | y') *)
   467 			val thm1     = make_cnfx_thm_from_nnf x
   468 			val thm2     = make_cnfx_thm_from_nnf y
   469 			val x'       = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1
   470 			val y'       = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm2
   471 			val disj_thm = disj_cong OF [thm1, thm2]  (* (x | y) = (x' | y') *)
   472 		in
   473 			iff_trans OF [disj_thm, make_cnfx_disj_thm x' y']
   474 		end else let  (* neither 'x' nor 'y' is a literal: introduce a fresh variable *)
   475 			val thm1 = inst_thm thy [x, y] make_cnfx_newlit     (* (x | y) = EX v. (x | v) & (y | ~v) *)
   476 			val var  = new_free ()
   477 			val body = HOLogic.mk_conj (HOLogic.mk_disj (x, var), HOLogic.mk_disj (y, HOLogic.Not $ var))
   478 			val thm2 = make_cnfx_thm_from_nnf body              (* (x | v) & (y | ~v) = body' *)
   479 			val thm3 = forall_intr (cterm_of thy var) thm2      (* !!v. (x | v) & (y | ~v) = body' *)
   480 			val thm4 = strip_shyps (thm3 COMP allI)             (* ALL v. (x | v) & (y | ~v) = body' *)
   481 			val thm5 = strip_shyps (thm4 RS make_cnfx_ex_cong)  (* (EX v. (x | v) & (y | ~v)) = (EX v. body') *)
   482 		in
   483 			iff_trans OF [thm1, thm5]
   484 		end
   485 	  | make_cnfx_thm_from_nnf t =
   486 		inst_thm thy [t] iff_refl
   487 	(* convert 't' to NNF first *)
   488 	val nnf_thm  = make_nnf_thm thy t
   489 	val nnf      = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) nnf_thm
   490 	(* then simplify wrt. True/False (this should preserve NNF) *)
   491 	val simp_thm = simp_True_False_thm thy nnf
   492 	val simp     = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) simp_thm
   493 	(* initialize var_id, in case the term already contains variables of the form "cnfx_<int>" *)
   494 	val _        = (var_id := fold (fn free => fn max =>
   495 		let
   496 			val (name, _) = dest_Free free
   497 			val idx       = if String.isPrefix "cnfx_" name then
   498 					(Int.fromString o String.extract) (name, String.size "cnfx_", NONE)
   499 				else
   500 					NONE
   501 		in
   502 			Int.max (max, getOpt (idx, 0))
   503 		end) (term_frees simp) 0)
   504 	(* finally, convert to definitional CNF (this should preserve the simplification) *)
   505 	val cnfx_thm = make_cnfx_thm_from_nnf simp
   506 in
   507 	iff_trans OF [iff_trans OF [nnf_thm, simp_thm], cnfx_thm]
   508 end;
   509 
   510 (* ------------------------------------------------------------------------- *)
   511 (*                                  Tactics                                  *)
   512 (* ------------------------------------------------------------------------- *)
   513 
   514 (* ------------------------------------------------------------------------- *)
   515 (* weakening_tac: removes the first hypothesis of the 'i'-th subgoal         *)
   516 (* ------------------------------------------------------------------------- *)
   517 
   518 (* int -> Tactical.tactic *)
   519 
   520 fun weakening_tac i =
   521 	dtac weakening_thm i THEN atac (i+1);
   522 
   523 (* ------------------------------------------------------------------------- *)
   524 (* cnf_rewrite_tac: converts all premises of the 'i'-th subgoal to CNF       *)
   525 (*      (possibly causing an exponential blowup in the length of each        *)
   526 (*      premise)                                                             *)
   527 (* ------------------------------------------------------------------------- *)
   528 
   529 (* int -> Tactical.tactic *)
   530 
   531 fun cnf_rewrite_tac i =
   532 	(* cut the CNF formulas as new premises *)
   533 	METAHYPS (fn prems =>
   534 		let
   535 			val cnf_thms = map (fn pr => make_cnf_thm (theory_of_thm pr) ((HOLogic.dest_Trueprop o prop_of) pr)) prems
   536 			val cut_thms = map (fn (th, pr) => cnftac_eq_imp OF [th, pr]) (cnf_thms ~~ prems)
   537 		in
   538 			cut_facts_tac cut_thms 1
   539 		end) i
   540 	(* remove the original premises *)
   541 	THEN SELECT_GOAL (fn thm =>
   542 		let
   543 			val n = Logic.count_prems ((Term.strip_all_body o fst o Logic.dest_implies o prop_of) thm)
   544 		in
   545 			PRIMITIVE (funpow (n div 2) (Seq.hd o weakening_tac 1)) thm
   546 		end) i;
   547 
   548 (* ------------------------------------------------------------------------- *)
   549 (* cnfx_rewrite_tac: converts all premises of the 'i'-th subgoal to CNF      *)
   550 (*      (possibly introducing new literals)                                  *)
   551 (* ------------------------------------------------------------------------- *)
   552 
   553 (* int -> Tactical.tactic *)
   554 
   555 fun cnfx_rewrite_tac i =
   556 	(* cut the CNF formulas as new premises *)
   557 	METAHYPS (fn prems =>
   558 		let
   559 			val cnfx_thms = map (fn pr => make_cnfx_thm (theory_of_thm pr) ((HOLogic.dest_Trueprop o prop_of) pr)) prems
   560 			val cut_thms  = map (fn (th, pr) => cnftac_eq_imp OF [th, pr]) (cnfx_thms ~~ prems)
   561 		in
   562 			cut_facts_tac cut_thms 1
   563 		end) i
   564 	(* remove the original premises *)
   565 	THEN SELECT_GOAL (fn thm =>
   566 		let
   567 			val n = Logic.count_prems ((Term.strip_all_body o fst o Logic.dest_implies o prop_of) thm)
   568 		in
   569 			PRIMITIVE (funpow (n div 2) (Seq.hd o weakening_tac 1)) thm
   570 		end) i;
   571 
   572 end;  (* of structure *)