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;
```     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 *)
```