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