src/HOL/Tools/cnf.ML
author wenzelm
Sun Jul 19 00:03:10 2015 +0200 (2015-07-19)
changeset 60759 36d9f215c982
parent 60696 8304fb4fb823
child 60801 7664e0916eec
permissions -rw-r--r--
more symbols;
     1 (*  Title:      HOL/Tools/cnf.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: Proof.context -> thm -> thm
    43   val make_nnf_thm: theory -> term -> thm
    44 
    45   val weakening_tac: Proof.context -> 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 "\<lbrakk>P; \<not>P\<rbrakk> \<Longrightarrow> False" by auto};
    58 val clause2raw_not_disj  = @{lemma "\<lbrakk>\<not> P; \<not> Q\<rbrakk> \<Longrightarrow> \<not> (P \<or> Q)" by auto};
    59 val clause2raw_not_not   = @{lemma "P \<Longrightarrow> \<not>\<not> 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 \<and> Q) = (P' \<and> Q')" by auto};
    64 val disj_cong            = @{lemma "[| P = P'; Q = Q' |] ==> (P \<or> Q) = (P' \<or> Q')" by auto};
    65 
    66 val make_nnf_imp         = @{lemma "[| (~P) = P'; Q = Q' |] ==> (P \<longrightarrow> Q) = (P' \<or> Q')" by auto};
    67 val make_nnf_iff         = @{lemma "[| P = P'; (~P) = NP; Q = Q'; (~Q) = NQ |] ==> (P = Q) = ((P' \<or> NQ) \<and> (NP \<or> 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 \<and> Q)) = (P' \<or> Q')" by auto};
    71 val make_nnf_not_disj    = @{lemma "[| (~P) = P'; (~Q) = Q' |] ==> (~(P \<or> Q)) = (P' \<and> Q')" by auto};
    72 val make_nnf_not_imp     = @{lemma "[| P = P'; (~Q) = Q' |] ==> (~(P \<longrightarrow> Q)) = (P' \<and> Q')" by auto};
    73 val make_nnf_not_iff     = @{lemma "[| P = P'; (~P) = NP; Q = Q'; (~Q) = NQ |] ==> (~(P = Q)) = ((P' \<or> Q') \<and> (NP \<or> 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 \<and> Q) = Q'" by auto};
    77 val simp_TF_conj_True_r  = @{lemma "[| P = P'; Q = True |] ==> (P \<and> Q) = P'" by auto};
    78 val simp_TF_conj_False_l = @{lemma "P = False ==> (P \<and> Q) = False" by auto};
    79 val simp_TF_conj_False_r = @{lemma "Q = False ==> (P \<and> Q) = False" by auto};
    80 val simp_TF_disj_True_l  = @{lemma "P = True ==> (P \<or> Q) = True" by auto};
    81 val simp_TF_disj_True_r  = @{lemma "Q = True ==> (P \<or> Q) = True" by auto};
    82 val simp_TF_disj_False_l = @{lemma "[| P = False; Q = Q' |] ==> (P \<or> Q) = Q'" by auto};
    83 val simp_TF_disj_False_r = @{lemma "[| P = P'; Q = False |] ==> (P \<or> Q) = P'" by auto};
    84 
    85 val make_cnf_disj_conj_l = @{lemma "[| (P \<or> R) = PR; (Q \<or> R) = QR |] ==> ((P \<and> Q) \<or> R) = (PR \<and> QR)" by auto};
    86 val make_cnf_disj_conj_r = @{lemma "[| (P \<or> Q) = PQ; (P \<or> R) = PR |] ==> (P \<or> (Q \<and> R)) = (PQ \<and> PR)" by auto};
    87 
    88 val make_cnfx_disj_ex_l  = @{lemma "((EX (x::bool). P x) \<or> Q) = (EX x. P x \<or> Q)" by auto};
    89 val make_cnfx_disj_ex_r  = @{lemma "(P \<or> (EX (x::bool). Q x)) = (EX x. P \<or> Q x)" by auto};
    90 val make_cnfx_newlit     = @{lemma "(P \<or> Q) = (EX x. (P \<or> x) \<and> (Q \<or> ~x))" by auto};
    91 val make_cnfx_ex_cong    = @{lemma "(ALL (x::bool). P x = Q x) \<Longrightarrow> (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 ctxt 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 > Thm.nprems_of thm then
   142         thm
   143       else
   144         not_disj_to_prem (i+1)
   145           (Seq.hd (REPEAT_DETERM (resolve_tac ctxt [clause2raw_not_disj] i) thm))
   146     (* moves all premises to hyps, i.e. "[...] |- A1 ==> ... ==> An ==> B" *)
   147     (* becomes "[..., A1, ..., An] |- B"                                   *)
   148     (* Thm.thm -> Thm.thm *)
   149     fun prems_to_hyps thm =
   150       fold (fn cprem => fn thm' =>
   151         Thm.implies_elim thm' (Thm.assume cprem)) (cprems_of thm) thm
   152   in
   153     (* [...] |- ~(x1 | ... | xn) ==> False *)
   154     (clause2raw_notE OF [clause])
   155     (* [...] |- ~x1 ==> ... ==> ~xn ==> False *)
   156     |> not_disj_to_prem 1
   157     (* [...] |- x1' ==> ... ==> xn' ==> False *)
   158     |> Seq.hd o TRYALL (resolve_tac ctxt [clause2raw_not_not])
   159     (* [..., x1', ..., xn'] |- False *)
   160     |> prems_to_hyps
   161   end;
   162 
   163 (* ------------------------------------------------------------------------- *)
   164 (* inst_thm: instantiates a theorem with a list of terms                     *)
   165 (* ------------------------------------------------------------------------- *)
   166 
   167 fun inst_thm thy ts thm =
   168   instantiate' [] (map (SOME o Thm.global_cterm_of thy) ts) thm;
   169 
   170 (* ------------------------------------------------------------------------- *)
   171 (*                         Naive CNF transformation                          *)
   172 (* ------------------------------------------------------------------------- *)
   173 
   174 (* ------------------------------------------------------------------------- *)
   175 (* make_nnf_thm: produces a theorem of the form t = t', where t' is the      *)
   176 (*      negation normal form (i.e. negation only occurs in front of atoms)   *)
   177 (*      of t; implications ("-->") and equivalences ("=" on bool) are        *)
   178 (*      eliminated (possibly causing an exponential blowup)                  *)
   179 (* ------------------------------------------------------------------------- *)
   180 
   181 fun make_nnf_thm thy (Const (@{const_name HOL.conj}, _) $ x $ y) =
   182       let
   183         val thm1 = make_nnf_thm thy x
   184         val thm2 = make_nnf_thm thy y
   185       in
   186         conj_cong OF [thm1, thm2]
   187       end
   188   | make_nnf_thm thy (Const (@{const_name HOL.disj}, _) $ x $ y) =
   189       let
   190         val thm1 = make_nnf_thm thy x
   191         val thm2 = make_nnf_thm thy y
   192       in
   193         disj_cong OF [thm1, thm2]
   194       end
   195   | make_nnf_thm thy (Const (@{const_name HOL.implies}, _) $ x $ y) =
   196       let
   197         val thm1 = make_nnf_thm thy (HOLogic.Not $ x)
   198         val thm2 = make_nnf_thm thy y
   199       in
   200         make_nnf_imp OF [thm1, thm2]
   201       end
   202   | make_nnf_thm thy (Const (@{const_name HOL.eq}, Type ("fun", @{typ bool} :: _)) $ x $ y) =
   203       let
   204         val thm1 = make_nnf_thm thy x
   205         val thm2 = make_nnf_thm thy (HOLogic.Not $ x)
   206         val thm3 = make_nnf_thm thy y
   207         val thm4 = make_nnf_thm thy (HOLogic.Not $ y)
   208       in
   209         make_nnf_iff OF [thm1, thm2, thm3, thm4]
   210       end
   211   | make_nnf_thm _ (Const (@{const_name Not}, _) $ Const (@{const_name False}, _)) =
   212       make_nnf_not_false
   213   | make_nnf_thm _ (Const (@{const_name Not}, _) $ Const (@{const_name True}, _)) =
   214       make_nnf_not_true
   215   | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.conj}, _) $ x $ y)) =
   216       let
   217         val thm1 = make_nnf_thm thy (HOLogic.Not $ x)
   218         val thm2 = make_nnf_thm thy (HOLogic.Not $ y)
   219       in
   220         make_nnf_not_conj OF [thm1, thm2]
   221       end
   222   | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.disj}, _) $ x $ y)) =
   223       let
   224         val thm1 = make_nnf_thm thy (HOLogic.Not $ x)
   225         val thm2 = make_nnf_thm thy (HOLogic.Not $ y)
   226       in
   227         make_nnf_not_disj OF [thm1, thm2]
   228       end
   229   | make_nnf_thm thy
   230       (Const (@{const_name Not}, _) $
   231         (Const (@{const_name HOL.implies}, _) $ x $ y)) =
   232       let
   233         val thm1 = make_nnf_thm thy x
   234         val thm2 = make_nnf_thm thy (HOLogic.Not $ y)
   235       in
   236         make_nnf_not_imp OF [thm1, thm2]
   237       end
   238   | make_nnf_thm thy
   239       (Const (@{const_name Not}, _) $
   240         (Const (@{const_name HOL.eq}, Type ("fun", @{typ bool} :: _)) $ x $ y)) =
   241       let
   242         val thm1 = make_nnf_thm thy x
   243         val thm2 = make_nnf_thm thy (HOLogic.Not $ x)
   244         val thm3 = make_nnf_thm thy y
   245         val thm4 = make_nnf_thm thy (HOLogic.Not $ y)
   246       in
   247         make_nnf_not_iff OF [thm1, thm2, thm3, thm4]
   248       end
   249   | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name Not}, _) $ x)) =
   250       let
   251         val thm1 = make_nnf_thm thy x
   252       in
   253         make_nnf_not_not OF [thm1]
   254       end
   255   | make_nnf_thm thy t = inst_thm thy [t] iff_refl;
   256 
   257 val meta_eq_to_obj_eq = @{thm meta_eq_to_obj_eq}
   258 val eq_reflection = @{thm eq_reflection}
   259 
   260 fun make_under_quantifiers ctxt make t =
   261   let
   262     fun conv ctxt ct =
   263       (case Thm.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 (Thm.cterm_of ctxt 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 Thm.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 Thm.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 Thm.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 Thm.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 Thm.prop_of) thm1
   376             val y' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.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 Thm.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 Thm.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 (Thm.global_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 (Thm.global_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 Thm.prop_of) thm1
   475               val y' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.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 (Thm.global_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 Thm.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 Thm.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 ctxt i =
   532   dresolve_tac ctxt [weakening_thm] i THEN assume_tac ctxt (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, context = ctxt', ...} =>
   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 Thm.prop_of) thm)
   553     in
   554       PRIMITIVE (funpow (n div 2) (Seq.hd o weakening_tac ctxt 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, context = ctxt', ...} =>
   565     let
   566       val cnfx_thms = map (make_cnfx_thm ctxt' o HOLogic.dest_Trueprop o Thm.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 Thm.prop_of) thm)
   575     in
   576       PRIMITIVE (funpow (n div 2) (Seq.hd o weakening_tac ctxt 1)) thm
   577     end) i;
   578 
   579 end;