src/HOL/Tools/cnf_funcs.ML
author wenzelm
Thu Jul 30 12:20:43 2009 +0200 (2009-07-30)
changeset 32283 3bebc195c124
parent 32232 6c394343360f
child 32740 9dd0a2f83429
permissions -rw-r--r--
qualified Subgoal.FOCUS;
     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 = ref 0  (* properly initialized below *)
   403 	(* unit -> Term.term *)
   404 	fun new_free () =
   405 		Free ("cnfx_" ^ string_of_int (inc var_id), HOLogic.boolT)
   406 	(* Term.term -> Thm.thm *)
   407 	fun make_cnfx_thm_from_nnf (Const ("op &", _) $ x $ y) =
   408 		let
   409 			val thm1 = make_cnfx_thm_from_nnf x
   410 			val thm2 = make_cnfx_thm_from_nnf y
   411 		in
   412 			conj_cong OF [thm1, thm2]
   413 		end
   414 	  | make_cnfx_thm_from_nnf (Const ("op |", _) $ x $ y) =
   415 		if is_clause x andalso is_clause y then
   416 			inst_thm thy [HOLogic.mk_disj (x, y)] iff_refl
   417 		else if is_literal y orelse is_literal x then let
   418 			(* produces a theorem "(x' | y') = t'", where x', y', and t' are *)
   419 			(* almost in CNF, and x' or y' is a literal                      *)
   420 			fun make_cnfx_disj_thm (Const ("op &", _) $ x1 $ x2) y' =
   421 				let
   422 					val thm1 = make_cnfx_disj_thm x1 y'
   423 					val thm2 = make_cnfx_disj_thm x2 y'
   424 				in
   425 					make_cnf_disj_conj_l OF [thm1, thm2]  (* ((x1 & x2) | y') = ((x1 | y')' & (x2 | y')') *)
   426 				end
   427 			  | make_cnfx_disj_thm x' (Const ("op &", _) $ y1 $ y2) =
   428 				let
   429 					val thm1 = make_cnfx_disj_thm x' y1
   430 					val thm2 = make_cnfx_disj_thm x' y2
   431 				in
   432 					make_cnf_disj_conj_r OF [thm1, thm2]  (* (x' | (y1 & y2)) = ((x' | y1)' & (x' | y2)') *)
   433 				end
   434 			  | make_cnfx_disj_thm (Const ("Ex", _) $ x') y' =
   435 				let
   436 					val thm1 = inst_thm thy [x', y'] make_cnfx_disj_ex_l   (* ((Ex x') | y') = (Ex (x' | y')) *)
   437 					val var  = new_free ()
   438 					val thm2 = make_cnfx_disj_thm (betapply (x', var)) y'  (* (x' | y') = body' *)
   439 					val thm3 = forall_intr (cterm_of thy var) thm2         (* !!v. (x' | y') = body' *)
   440 					val thm4 = strip_shyps (thm3 COMP allI)                (* ALL v. (x' | y') = body' *)
   441 					val thm5 = strip_shyps (thm4 RS make_cnfx_ex_cong)     (* (EX v. (x' | y')) = (EX v. body') *)
   442 				in
   443 					iff_trans OF [thm1, thm5]  (* ((Ex x') | y') = (Ex v. body') *)
   444 				end
   445 			  | make_cnfx_disj_thm x' (Const ("Ex", _) $ y') =
   446 				let
   447 					val thm1 = inst_thm thy [x', y'] make_cnfx_disj_ex_r   (* (x' | (Ex y')) = (Ex (x' | y')) *)
   448 					val var  = new_free ()
   449 					val thm2 = make_cnfx_disj_thm x' (betapply (y', var))  (* (x' | y') = body' *)
   450 					val thm3 = forall_intr (cterm_of thy var) thm2         (* !!v. (x' | y') = body' *)
   451 					val thm4 = strip_shyps (thm3 COMP allI)                (* ALL v. (x' | y') = body' *)
   452 					val thm5 = strip_shyps (thm4 RS make_cnfx_ex_cong)     (* (EX v. (x' | y')) = (EX v. body') *)
   453 				in
   454 					iff_trans OF [thm1, thm5]  (* (x' | (Ex y')) = (EX v. body') *)
   455 				end
   456 			  | make_cnfx_disj_thm x' y' =
   457 				inst_thm thy [HOLogic.mk_disj (x', y')] iff_refl  (* (x' | y') = (x' | y') *)
   458 			val thm1     = make_cnfx_thm_from_nnf x
   459 			val thm2     = make_cnfx_thm_from_nnf y
   460 			val x'       = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1
   461 			val y'       = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm2
   462 			val disj_thm = disj_cong OF [thm1, thm2]  (* (x | y) = (x' | y') *)
   463 		in
   464 			iff_trans OF [disj_thm, make_cnfx_disj_thm x' y']
   465 		end else let  (* neither 'x' nor 'y' is a literal: introduce a fresh variable *)
   466 			val thm1 = inst_thm thy [x, y] make_cnfx_newlit     (* (x | y) = EX v. (x | v) & (y | ~v) *)
   467 			val var  = new_free ()
   468 			val body = HOLogic.mk_conj (HOLogic.mk_disj (x, var), HOLogic.mk_disj (y, HOLogic.Not $ var))
   469 			val thm2 = make_cnfx_thm_from_nnf body              (* (x | v) & (y | ~v) = body' *)
   470 			val thm3 = forall_intr (cterm_of thy var) thm2      (* !!v. (x | v) & (y | ~v) = body' *)
   471 			val thm4 = strip_shyps (thm3 COMP allI)             (* ALL v. (x | v) & (y | ~v) = body' *)
   472 			val thm5 = strip_shyps (thm4 RS make_cnfx_ex_cong)  (* (EX v. (x | v) & (y | ~v)) = (EX v. body') *)
   473 		in
   474 			iff_trans OF [thm1, thm5]
   475 		end
   476 	  | make_cnfx_thm_from_nnf t =
   477 		inst_thm thy [t] iff_refl
   478 	(* convert 't' to NNF first *)
   479 	val nnf_thm  = make_nnf_thm thy t
   480 	val nnf      = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) nnf_thm
   481 	(* then simplify wrt. True/False (this should preserve NNF) *)
   482 	val simp_thm = simp_True_False_thm thy nnf
   483 	val simp     = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) simp_thm
   484 	(* initialize var_id, in case the term already contains variables of the form "cnfx_<int>" *)
   485 	val _        = (var_id := fold (fn free => fn max =>
   486 		let
   487 			val (name, _) = dest_Free free
   488 			val idx       = if String.isPrefix "cnfx_" name then
   489 					(Int.fromString o String.extract) (name, String.size "cnfx_", NONE)
   490 				else
   491 					NONE
   492 		in
   493 			Int.max (max, getOpt (idx, 0))
   494 		end) (OldTerm.term_frees simp) 0)
   495 	(* finally, convert to definitional CNF (this should preserve the simplification) *)
   496 	val cnfx_thm = make_cnfx_thm_from_nnf simp
   497 in
   498 	iff_trans OF [iff_trans OF [nnf_thm, simp_thm], cnfx_thm]
   499 end;
   500 
   501 (* ------------------------------------------------------------------------- *)
   502 (*                                  Tactics                                  *)
   503 (* ------------------------------------------------------------------------- *)
   504 
   505 (* ------------------------------------------------------------------------- *)
   506 (* weakening_tac: removes the first hypothesis of the 'i'-th subgoal         *)
   507 (* ------------------------------------------------------------------------- *)
   508 
   509 fun weakening_tac i =
   510 	dtac weakening_thm i THEN atac (i+1);
   511 
   512 (* ------------------------------------------------------------------------- *)
   513 (* cnf_rewrite_tac: converts all premises of the 'i'-th subgoal to CNF       *)
   514 (*      (possibly causing an exponential blowup in the length of each        *)
   515 (*      premise)                                                             *)
   516 (* ------------------------------------------------------------------------- *)
   517 
   518 fun cnf_rewrite_tac ctxt i =
   519 	(* cut the CNF formulas as new premises *)
   520 	Subgoal.FOCUS (fn {prems, ...} =>
   521 		let
   522 		  val thy = ProofContext.theory_of ctxt
   523 			val cnf_thms = map (make_cnf_thm thy o HOLogic.dest_Trueprop o Thm.prop_of) prems
   524 			val cut_thms = map (fn (th, pr) => cnftac_eq_imp OF [th, pr]) (cnf_thms ~~ prems)
   525 		in
   526 			cut_facts_tac cut_thms 1
   527 		end) ctxt i
   528 	(* remove the original premises *)
   529 	THEN SELECT_GOAL (fn thm =>
   530 		let
   531 			val n = Logic.count_prems ((Term.strip_all_body o fst o Logic.dest_implies o prop_of) thm)
   532 		in
   533 			PRIMITIVE (funpow (n div 2) (Seq.hd o weakening_tac 1)) thm
   534 		end) i;
   535 
   536 (* ------------------------------------------------------------------------- *)
   537 (* cnfx_rewrite_tac: converts all premises of the 'i'-th subgoal to CNF      *)
   538 (*      (possibly introducing new literals)                                  *)
   539 (* ------------------------------------------------------------------------- *)
   540 
   541 fun cnfx_rewrite_tac ctxt i =
   542 	(* cut the CNF formulas as new premises *)
   543 	Subgoal.FOCUS (fn {prems, ...} =>
   544 		let
   545 		  val thy = ProofContext.theory_of ctxt;
   546 			val cnfx_thms = map (make_cnfx_thm thy o HOLogic.dest_Trueprop o prop_of) prems
   547 			val cut_thms  = map (fn (th, pr) => cnftac_eq_imp OF [th, pr]) (cnfx_thms ~~ prems)
   548 		in
   549 			cut_facts_tac cut_thms 1
   550 		end) ctxt i
   551 	(* remove the original premises *)
   552 	THEN SELECT_GOAL (fn thm =>
   553 		let
   554 			val n = Logic.count_prems ((Term.strip_all_body o fst o Logic.dest_implies o prop_of) thm)
   555 		in
   556 			PRIMITIVE (funpow (n div 2) (Seq.hd o weakening_tac 1)) thm
   557 		end) i;
   558 
   559 end;  (* of structure *)