src/HOL/Tools/cnf_funcs.ML
author wenzelm
Wed Mar 19 22:47:39 2008 +0100 (2008-03-19)
changeset 26341 2f5a4367a39e
parent 24958 ff15f76741bd
child 29265 5b4247055bd7
permissions -rw-r--r--
avoid Auto_tac;
     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   FIXME: major overlaps with the code in meson.ML
     8 
     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:
    13 
    14       (x11 | x12 | ... | x1n) & ... & (xm1 | xm2 | ... | xmk)
    15       False
    16       True
    17 
    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".
    21 
    22   A (non-empty) disjunction of literals is referred to as "clause".
    23 
    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
    27 
    28       [..., x1', x2', ..., xn'] |- False ,
    29 
    30   where each xi is a literal, and each xi' is the negation normal form of ~xi.
    31 
    32   Literals are successively removed from the hyps of raw clauses by resolution
    33   during SAT proof reconstruction.
    34 *)
    35 
    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
    42 
    43 	val clause2raw_thm : Thm.thm -> Thm.thm
    44 
    45 	val weakening_tac : int -> Tactical.tactic  (* removes the first hypothesis of a subgoal *)
    46 
    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;
    52 
    53 structure cnf : CNF =
    54 struct
    55 
    56 fun thm_by_auto (G : string) : thm =
    57 	prove_goal (the_context ()) G (fn prems => [cut_facts_tac prems 1, CLASIMPSET auto_tac]);
    58 
    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";
    63 
    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')";
    68 
    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'";
    78 
    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'";
    87 
    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)";
    90 
    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)";
    95 
    96 val weakening_thm        = thm_by_auto "[| P; Q |] ==> Q";
    97 
    98 val cnftac_eq_imp        = thm_by_auto "[| P = Q; P |] ==> Q";
    99 
   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;
   109 
   110 (* Term.term -> bool *)
   111 fun is_literal (Const ("Not", _) $ x) = is_atom x
   112   | is_literal x                      = is_atom x;
   113 
   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;
   117 
   118 (* ------------------------------------------------------------------------- *)
   119 (* clause_is_trivial: a clause is trivially true if it contains both an atom *)
   120 (*      and the atom's negation                                              *)
   121 (* ------------------------------------------------------------------------- *)
   122 
   123 (* Term.term -> bool *)
   124 
   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;
   136 
   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 (* ------------------------------------------------------------------------- *)
   144 
   145 (* Thm.thm -> Thm.thm *)
   146 
   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;
   173 
   174 (* ------------------------------------------------------------------------- *)
   175 (* inst_thm: instantiates a theorem with a list of terms                     *)
   176 (* ------------------------------------------------------------------------- *)
   177 
   178 fun inst_thm thy ts thm =
   179 	instantiate' [] (map (SOME o cterm_of thy) ts) thm;
   180 
   181 (* ------------------------------------------------------------------------- *)
   182 (*                         Naive CNF transformation                          *)
   183 (* ------------------------------------------------------------------------- *)
   184 
   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 (* ------------------------------------------------------------------------- *)
   191 
   192 (* Theory.theory -> Term.term -> Thm.thm *)
   193 
   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;
   266 
   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 (* ------------------------------------------------------------------------- *)
   283 
   284 (* Theory.theory -> Term.term -> Thm.thm *)
   285 
   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 *)
   332 
   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 (* ------------------------------------------------------------------------- *)
   338 
   339 (* Theory.theory -> Term.term -> Thm.thm *)
   340 
   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;
   391 
   392 (* ------------------------------------------------------------------------- *)
   393 (*            CNF transformation by introducing new literals                 *)
   394 (* ------------------------------------------------------------------------- *)
   395 
   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 (* ------------------------------------------------------------------------- *)
   405 
   406 (* Theory.theory -> Term.term -> Thm.thm *)
   407 
   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;
   508 
   509 (* ------------------------------------------------------------------------- *)
   510 (*                                  Tactics                                  *)
   511 (* ------------------------------------------------------------------------- *)
   512 
   513 (* ------------------------------------------------------------------------- *)
   514 (* weakening_tac: removes the first hypothesis of the 'i'-th subgoal         *)
   515 (* ------------------------------------------------------------------------- *)
   516 
   517 (* int -> Tactical.tactic *)
   518 
   519 fun weakening_tac i =
   520 	dtac weakening_thm i THEN atac (i+1);
   521 
   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 (* ------------------------------------------------------------------------- *)
   527 
   528 (* int -> Tactical.tactic *)
   529 
   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;
   546 
   547 (* ------------------------------------------------------------------------- *)
   548 (* cnfx_rewrite_tac: converts all premises of the 'i'-th subgoal to CNF      *)
   549 (*      (possibly introducing new literals)                                  *)
   550 (* ------------------------------------------------------------------------- *)
   551 
   552 (* int -> Tactical.tactic *)
   553 
   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;
   570 
   571 end;  (* of structure *)