src/HOL/Tools/cnf_funcs.ML
author wenzelm
Thu Aug 03 17:30:36 2006 +0200 (2006-08-03)
changeset 20328 5b240a4216b0
parent 19236 150e8b0fb991
child 20440 e6fe74eebda3
permissions -rw-r--r--
RuleInsts.bires_inst_tac;
     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 *)