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