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