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