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