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