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