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