src/HOL/Tools/cnf_funcs.ML
 author webertj Fri Sep 23 22:58:50 2005 +0200 (2005-09-23) changeset 17618 1330157e156a child 17809 195045659c06 permissions -rw-r--r--
new sat tactic imports resolution proofs from zChaff
```     1 (*  Title:      HOL/Tools/cnf_funcs.ML
```
```     2     ID:         \$Id\$
```
```     3     Author:     Alwen Tiu, QSL Team, LORIA (http://qsl.loria.fr)
```
```     4     Copyright   2005
```
```     5
```
```     6   Description:
```
```     7   This file contains functions and tactics to transform a formula into
```
```     8   Conjunctive Normal Forms (CNF).
```
```     9   A formula in CNF is of the following form:
```
```    10
```
```    11       (x11 | x12 | .. x1m) & ... & (xm1 | xm2 | ... | xmn)
```
```    12
```
```    13   where each xij is a literal (i.e., positive or negative propositional
```
```    14   variables).
```
```    15   This kind of formula will simply be referred to as CNF.
```
```    16   A disjunction of literals is referred to as "clause".
```
```    17
```
```    18   For the purpose of SAT proof reconstruction, we also make use of another
```
```    19   representation of clauses, which we call the "raw clauses".
```
```    20   Raw clauses are of the form
```
```    21
```
```    22       (x1 ==> x2 ==> .. ==> xn ==> False)
```
```    23
```
```    24   where each xi is a literal. Note that the above raw clause corresponds
```
```    25   to the clause (x1' | ... | xn'), where each xi' is the negation normal
```
```    26   form of ~xi.
```
```    27
```
```    28   Notes for current revision:
```
```    29   - the "definitional CNF transformation" (anything with prefix cnfx_ )
```
```    30     introduces new literals of the form (lit_i) where i is an integer.
```
```    31     For these functions to work, it is necessary that no free variables
```
```    32     which names are of the form lit_i appears in the formula being
```
```    33     transformed.
```
```    34 *)
```
```    35
```
```    36
```
```    37 (***************************************************************************)
```
```    38
```
```    39 signature CNF =
```
```    40 sig
```
```    41   val cnf_tac : Tactical.tactic
```
```    42   val cnf_thin_tac : Tactical.tactic
```
```    43   val cnfx_thin_tac : Tactical.tactic
```
```    44   val cnf_concl_tac : Tactical.tactic
```
```    45   val weakening_tac : int -> Tactical.tactic
```
```    46   val mk_cnf_thm : Sign.sg -> Term.term -> Thm.thm
```
```    47   val mk_cnfx_thm : Sign.sg -> Term.term ->  Thm.thm
```
```    48   val is_atm : Term.term -> bool
```
```    49   val is_lit : Term.term -> bool
```
```    50   val is_clause : Term.term -> bool
```
```    51   val is_raw_clause : Term.term -> bool
```
```    52   val cnf2raw_thm : Thm.thm -> Thm.thm
```
```    53   val cnf2raw_thms : Thm.thm list -> Thm.thm list
```
```    54   val cnf2prop : Thm.thm list -> (PropLogic.prop_formula * ((Term.term * int) list))
```
```    55 end
```
```    56
```
```    57
```
```    58 (***************************************************************************)
```
```    59
```
```    60 structure cnf : CNF =
```
```    61 struct
```
```    62
```
```    63 val cur_thy = the_context();
```
```    64 val mk_disj = HOLogic.mk_disj;
```
```    65 val mk_conj = HOLogic.mk_conj;
```
```    66 val mk_imp  = HOLogic.mk_imp;
```
```    67 val Not = HOLogic.Not;
```
```    68 val false_const = HOLogic.false_const;
```
```    69 val true_const = HOLogic.true_const;
```
```    70
```
```    71
```
```    72 (* Index for new literals *)
```
```    73 val lit_id = ref 0;
```
```    74
```
```    75 fun thm_by_auto G =
```
```    76     prove_goal cur_thy G (fn prems => [cut_facts_tac prems 1, Auto_tac]);
```
```    77
```
```    78 (***************************************************************************)
```
```    79
```
```    80
```
```    81 val cnf_eq_id = thm_by_auto "(P :: bool) = P";
```
```    82
```
```    83 val cnf_eq_sym = thm_by_auto "(P :: bool) = Q ==> Q = P";
```
```    84
```
```    85 val cnf_not_true_false = thm_by_auto "~True = False";
```
```    86
```
```    87 val cnf_not_false_true = thm_by_auto "~False = True";
```
```    88
```
```    89 val cnf_imp2disj = thm_by_auto "(P --> Q) = (~P | Q)";
```
```    90
```
```    91 val cnf_neg_conj = thm_by_auto "(~(P & Q)) = (~P | ~Q)";
```
```    92
```
```    93 val cnf_neg_disj = thm_by_auto "(~(P | Q)) = (~P & ~Q)";
```
```    94
```
```    95 val cnf_neg_imp = thm_by_auto "(~(P --> Q)) = (P & ~Q)";
```
```    96
```
```    97 val cnf_double_neg = thm_by_auto "(~~P) = P";
```
```    98
```
```    99 val cnf_disj_conj = thm_by_auto "((P & Q) | R) = ((P | R) & (Q | R))";
```
```   100
```
```   101 val cnf_disj_imp = thm_by_auto "((P --> Q) | R) = (~P | (Q | R))";
```
```   102
```
```   103 val cnf_disj_disj = thm_by_auto "((P | Q) | R) = (P | (Q | R))";
```
```   104
```
```   105 val cnf_disj_false = thm_by_auto "(False | P) = P";
```
```   106
```
```   107 val cnf_disj_true = thm_by_auto "(True | P) = True";
```
```   108
```
```   109 val cnf_disj_not_false = thm_by_auto "(~False | P) = True";
```
```   110
```
```   111 val cnf_disj_not_true = thm_by_auto "(~True | P) = P";
```
```   112
```
```   113 val cnf_eq_trans = thm_by_auto "[| ( (P::bool) = Q) ; Q = R |] ==> (P = R)";
```
```   114
```
```   115 val cnf_comb2eq = thm_by_auto "[| P = Q ; R = T |] ==> (P & R) = (Q & T)";
```
```   116
```
```   117 val cnf_disj_sym = thm_by_auto "(P | Q) = (Q | P)";
```
```   118
```
```   119 val cnf_cong_disj = thm_by_auto "(P = Q) ==> (P | R) = (Q | R)";
```
```   120
```
```   121 val icnf_elim_disj1 = thm_by_auto "Q = R  ==> (~P | Q) = (P --> R)";
```
```   122
```
```   123 val icnf_elim_disj2 = thm_by_auto "Q = R ==> (P | Q) = (~P --> R)";
```
```   124
```
```   125 val icnf_neg_false1 = thm_by_auto "(~P) = (P --> False)";
```
```   126
```
```   127 val icnf_neg_false2 = thm_by_auto "P = (~P --> False)";
```
```   128
```
```   129 val weakening_thm = thm_by_auto "[| P ; Q |] ==> Q";
```
```   130
```
```   131 val cnf_newlit = thm_by_auto
```
```   132     "((P & Q) | R) = (EX (x :: bool). (~x | P) & (~x | Q) & (x | ~P | ~ Q) & (x | R))";
```
```   133
```
```   134 val cnf_all_ex = thm_by_auto
```
```   135     "(ALL (x :: bool). (P x = Q x)) ==> (EX x. P x) = (EX x. Q x)";
```
```   136
```
```   137 (* [| P ; ~P |] ==> False *)
```
```   138 val cnf_notE = read_instantiate [("R", "False")] (rotate_prems 1 notE);
```
```   139
```
```   140 val cnf_dneg = thm_by_auto "P ==> ~~P";
```
```   141
```
```   142 val cnf_neg_disjI = thm_by_auto "[| ~P ; ~Q |] ==> ~(P | Q)";
```
```   143
```
```   144 val cnf_eq_imp = thm_by_auto "[|((P::bool) = Q) ; P |] ==> Q";
```
```   145
```
```   146 (***************************************************************************)
```
```   147
```
```   148 fun is_atm (Const("Trueprop",_) \$ x) = is_atm x
```
```   149   | is_atm (Const("==>",_) \$ x \$ y) = false
```
```   150   | is_atm (Const("False",_)) = false
```
```   151   | is_atm (Const("True", _)) = false
```
```   152   | is_atm (Const("op &",_) \$ x \$ y) = false
```
```   153   | is_atm (Const("op |",_) \$ x \$ y) = false
```
```   154   | is_atm (Const("op -->",_) \$ x \$ y) = false
```
```   155   | is_atm (Const("Not",_) \$ x) = false
```
```   156   | is_atm t = true
```
```   157
```
```   158
```
```   159 fun is_lit (Const("Trueprop",_) \$ x) = is_lit x
```
```   160   | is_lit (Const("Not", _) \$ x) = is_atm x
```
```   161   | is_lit t = is_atm t
```
```   162
```
```   163 fun is_clause (Const("Trueprop",_) \$ x) = is_clause x
```
```   164   | is_clause (Const("op |", _) \$ x \$ y) =
```
```   165           (is_clause x) andalso (is_clause y)
```
```   166   | is_clause t = is_lit t
```
```   167
```
```   168 fun is_cnf (Const("Trueprop", _) \$ x) = is_cnf x
```
```   169   | is_cnf (Const("op &",_) \$ x \$ y) = (is_cnf x) andalso (is_cnf y)
```
```   170   | is_cnf t = is_clause t
```
```   171
```
```   172
```
```   173 (* Checking for raw clauses *)
```
```   174 fun is_raw_clause (Const("Trueprop",_) \$ x) = is_raw_clause x
```
```   175   | is_raw_clause (Const("==>",_) \$ x \$
```
```   176                    (Const("Trueprop",_) \$ Const("False",_))) = is_lit x
```
```   177   | is_raw_clause (Const("==>",_) \$ x \$ y) =
```
```   178         (is_lit x) andalso (is_raw_clause y)
```
```   179   | is_raw_clause t = false
```
```   180
```
```   181
```
```   182
```
```   183 (* Translate a CNF clause into a raw clause *)
```
```   184 fun cnf2raw_thm c =
```
```   185 let val nc = c RS cnf_notE
```
```   186 in
```
```   187 rule_by_tactic (REPEAT_SOME (fn i =>
```
```   188                rtac cnf_dneg i
```
```   189                ORELSE rtac cnf_neg_disjI i)) nc
```
```   190 handle THM _ => nc
```
```   191 end
```
```   192
```
```   193 fun cnf2raw_thms nil = nil
```
```   194   | cnf2raw_thms (c::l) =
```
```   195     let val t = term_of (cprop_of c)
```
```   196     in
```
```   197        if (is_clause t) then (cnf2raw_thm c) :: cnf2raw_thms l
```
```   198        else cnf2raw_thms l
```
```   199     end
```
```   200
```
```   201
```
```   202 (* Translating HOL formula (in CNF) to PropLogic formula. Returns also an
```
```   203    association list, relating literals to their indices *)
```
```   204
```
```   205 local
```
```   206   (* maps atomic formulas to variable numbers *)
```
```   207   val dictionary : ((Term.term * int) list) ref = ref nil;
```
```   208   val var_count = ref 0;
```
```   209   val pAnd = PropLogic.And;
```
```   210   val pOr = PropLogic.Or;
```
```   211   val pNot = PropLogic.Not;
```
```   212   val pFalse = PropLogic.False;
```
```   213   val pTrue = PropLogic.True;
```
```   214   val pVar = PropLogic.BoolVar;
```
```   215
```
```   216   fun mk_clause (Const("Trueprop",_) \$ x) = mk_clause x
```
```   217     | mk_clause (Const("op |",_) \$ x \$ y) = pOr(mk_clause x, mk_clause y)
```
```   218     | mk_clause (Const("Not", _) \$ x) = pNot (mk_clause x)
```
```   219     | mk_clause (Const("True",_)) = pTrue
```
```   220     | mk_clause (Const("False",_)) = pFalse
```
```   221     | mk_clause t =
```
```   222       let
```
```   223          val idx = AList.lookup op= (!dictionary) t
```
```   224       in
```
```   225          case idx of
```
```   226             (SOME x) => pVar x
```
```   227            | NONE =>
```
```   228              let
```
```   229                 val new_var = inc var_count
```
```   230              in
```
```   231                 dictionary := (t, new_var) :: (!dictionary);
```
```   232                 pVar new_var
```
```   233              end
```
```   234       end
```
```   235
```
```   236    fun mk_clauses nil = pTrue
```
```   237      | mk_clauses (x::nil) = mk_clause x
```
```   238      | mk_clauses (x::l) = pAnd(mk_clause x, mk_clauses l)
```
```   239
```
```   240 in
```
```   241    fun cnf2prop thms =
```
```   242    (
```
```   243      var_count := 0;
```
```   244      dictionary := nil;
```
```   245      (mk_clauses (map (fn x => term_of (cprop_of x)) thms), !dictionary)
```
```   246    )
```
```   247 end
```
```   248
```
```   249
```
```   250
```
```   251 (* Instantiate a theorem with a list of terms *)
```
```   252 fun inst_thm sign l thm =
```
```   253   instantiate' [] (map (fn x => SOME (cterm_of sign x)) l) thm
```
```   254
```
```   255 (* Tactic to remove the first hypothesis of the first subgoal. *)
```
```   256 fun weakening_tac i = (dtac weakening_thm i) THEN (atac (i+1));
```
```   257
```
```   258 (* Tactic for removing the n first hypotheses of the first subgoal. *)
```
```   259 fun weakenings_tac 0 state = all_tac state
```
```   260   | weakenings_tac n state = ((weakening_tac  1) THEN (weakenings_tac (n-1))) state
```
```   261
```
```   262
```
```   263 (*
```
```   264   Transform a formula into a "head" negation normal form, that is,
```
```   265   the top level connective is not a negation, with the exception
```
```   266   of negative literals. Returns the pair of the head normal term with
```
```   267   the theorem corresponding to the transformation.
```
```   268 *)
```
```   269 fun head_nnf sign (Const("Not",_)  \$ (Const("op &",_) \$ x \$ y)) =
```
```   270     let val t = mk_disj(Not \$ x, Not \$ y)
```
```   271         val neg_thm = inst_thm sign [x, y] cnf_neg_conj
```
```   272     in
```
```   273         (t, neg_thm)
```
```   274     end
```
```   275
```
```   276   | head_nnf sign (Const("Not", _) \$ (Const("op |",_) \$ x \$ y)) =
```
```   277     let val t = mk_conj(Not \$ x, Not \$ y)
```
```   278         val neg_thm =  inst_thm sign [x, y] cnf_neg_disj;
```
```   279     in
```
```   280         (t, neg_thm)
```
```   281     end
```
```   282
```
```   283   | head_nnf sign (Const("Not", _) \$ (Const("op -->",_) \$ x \$ y)) =
```
```   284     let val t = mk_conj(x, Not \$ y)
```
```   285         val neg_thm = inst_thm sign [x, y] cnf_neg_imp
```
```   286     in
```
```   287         (t, neg_thm)
```
```   288     end
```
```   289
```
```   290   | head_nnf sign (Const("Not",_) \$ (Const("Not",_) \$ x)) =
```
```   291     (x, inst_thm sign [x] cnf_double_neg)
```
```   292
```
```   293   | head_nnf sign (Const("Not",_) \$ Const("True",_)) =
```
```   294       (false_const, cnf_not_true_false)
```
```   295
```
```   296   | head_nnf sign (Const("Not",_) \$ Const("False",_)) =
```
```   297       (true_const, cnf_not_false_true)
```
```   298
```
```   299   | head_nnf sign t =
```
```   300     (t, inst_thm sign [t] cnf_eq_id)
```
```   301
```
```   302
```
```   303 (***************************************************************************)
```
```   304 (*                  Tactics for simple CNF transformation                  *)
```
```   305
```
```   306 (* A naive procedure for CNF transformation:
```
```   307    Given any t, produce a theorem t = t', where t' is in
```
```   308    conjunction normal form
```
```   309 *)
```
```   310 fun mk_cnf_thm sign (Const("Trueprop",_) \$ x) = mk_cnf_thm sign x
```
```   311   | mk_cnf_thm sign (t as (Const(_,_))) = inst_thm sign [t] cnf_eq_id
```
```   312   | mk_cnf_thm sign (t as (Free(_,_))) =  inst_thm sign [t] cnf_eq_id
```
```   313
```
```   314   | mk_cnf_thm sign (Const("op -->", _) \$ x \$ y) =
```
```   315        let val thm1 = inst_thm sign [x, y] cnf_imp2disj;
```
```   316            val thm2 = mk_cnf_thm sign (mk_disj(Not \$ x, y));
```
```   317        in
```
```   318            cnf_eq_trans OF [thm1, thm2]
```
```   319        end
```
```   320
```
```   321   | mk_cnf_thm sign (Const("op &", _) \$ x \$ y) =
```
```   322        let val cnf1 = mk_cnf_thm sign x;
```
```   323            val cnf2 = mk_cnf_thm sign y;
```
```   324        in
```
```   325            cnf_comb2eq OF [cnf1, cnf2]
```
```   326        end
```
```   327
```
```   328   | mk_cnf_thm sign (Const("Not",_) \$ Const("True",_)) =
```
```   329         cnf_not_true_false
```
```   330
```
```   331   | mk_cnf_thm sign (Const("Not",_) \$ Const("False",_)) =
```
```   332         cnf_not_false_true
```
```   333
```
```   334   | mk_cnf_thm sign (t as (Const("Not", _) \$ x)) =
```
```   335       (
```
```   336        if (is_atm x) then inst_thm sign [t] cnf_eq_id
```
```   337        else
```
```   338          let val (t1, hn_thm) = head_nnf sign t
```
```   339              val cnf_thm = mk_cnf_thm sign t1
```
```   340          in
```
```   341              cnf_eq_trans OF [hn_thm, cnf_thm]
```
```   342          end
```
```   343        )
```
```   344
```
```   345   | mk_cnf_thm sign (Const("op |",_) \$ (Const("op &", _) \$ p \$ q) \$ r) =
```
```   346        let val thm1 = inst_thm sign [p, q, r] cnf_disj_conj;
```
```   347            val thm2 = mk_cnf_thm sign (mk_conj(mk_disj(p, r), mk_disj(q,r)));
```
```   348        in
```
```   349           cnf_eq_trans OF [thm1, thm2]
```
```   350        end
```
```   351
```
```   352   | mk_cnf_thm sign (Const("op |",_) \$ (Const("op |", _) \$ p \$ q) \$ r) =
```
```   353        let val thm1 = inst_thm sign [p,q,r] cnf_disj_disj;
```
```   354            val thm2 = mk_cnf_thm sign (mk_disj(p, mk_disj(q,r)));
```
```   355        in
```
```   356           cnf_eq_trans OF [thm1, thm2]
```
```   357        end
```
```   358
```
```   359   | mk_cnf_thm sign (Const("op |",_) \$ (Const("op -->", _) \$ p \$ q) \$ r) =
```
```   360        let val thm1 = inst_thm sign [p,q,r] cnf_disj_imp;
```
```   361            val thm2 = mk_cnf_thm sign (mk_disj(Not \$ p, mk_disj(q, r)));
```
```   362        in
```
```   363            cnf_eq_trans OF [thm1, thm2]
```
```   364        end
```
```   365
```
```   366   | mk_cnf_thm sign (Const("op |",_) \$ Const("False",_) \$ p) =
```
```   367        let val thm1 = inst_thm sign [p] cnf_disj_false;
```
```   368            val thm2 = mk_cnf_thm sign p
```
```   369        in
```
```   370            cnf_eq_trans OF [thm1, thm2]
```
```   371        end
```
```   372
```
```   373   | mk_cnf_thm sign (Const("op |",_) \$ Const("True",_) \$ p) =
```
```   374        inst_thm sign [p] cnf_disj_true
```
```   375
```
```   376   | mk_cnf_thm sign (Const("op |",_) \$ (Const("Not",_) \$ Const("True",_)) \$ p) =
```
```   377        let val thm1 = inst_thm sign [p] cnf_disj_not_true;
```
```   378            val thm2 = mk_cnf_thm sign p
```
```   379        in
```
```   380            cnf_eq_trans OF [thm1, thm2]
```
```   381        end
```
```   382
```
```   383   | mk_cnf_thm sign (Const("op |",_) \$ (Const("Not",_) \$ Const("False",_)) \$ p) =
```
```   384        inst_thm sign [p] cnf_disj_not_false
```
```   385
```
```   386   | mk_cnf_thm sign (t as (Const("op |",_) \$ p \$ q)) =
```
```   387        if (is_lit p) then
```
```   388           (
```
```   389             if (is_clause t) then inst_thm sign [t] cnf_eq_id
```
```   390             else
```
```   391              let val thm1 = inst_thm sign [p, q] cnf_disj_sym;
```
```   392                  val thm2 = mk_cnf_thm sign (mk_disj(q, p))
```
```   393              in
```
```   394                 cnf_eq_trans OF [thm1, thm2]
```
```   395              end
```
```   396           )
```
```   397        else
```
```   398             let val (u, thm1) = head_nnf sign p;
```
```   399                 val thm2 = inst_thm sign [p,u,q] cnf_cong_disj;
```
```   400                 val thm3 = mk_cnf_thm sign (mk_disj(u, q))
```
```   401             in
```
```   402                 cnf_eq_trans OF [(thm1 RS thm2), thm3]
```
```   403             end
```
```   404
```
```   405  | mk_cnf_thm sign t = inst_thm sign [t] cnf_eq_id
```
```   406     (* error ("I don't know how to handle the formula " ^
```
```   407                           (Sign.string_of_term sign t))
```
```   408     *)
```
```   409
```
```   410 fun term_of_thm c = term_of (cprop_of c)
```
```   411
```
```   412
```
```   413 (* Transform a given list of theorems (thms) into CNF *)
```
```   414
```
```   415 fun mk_cnf_thms sg nil = nil
```
```   416   | mk_cnf_thms sg (x::l) =
```
```   417     let val t = term_of_thm x
```
```   418     in
```
```   419       if (is_clause t) then x :: mk_cnf_thms sg l
```
```   420       else
```
```   421        let val thm1 = mk_cnf_thm sg t
```
```   422            val thm2 = cnf_eq_imp OF [thm1, x]
```
```   423        in
```
```   424            thm2 :: mk_cnf_thms sg l
```
```   425        end
```
```   426     end
```
```   427
```
```   428
```
```   429 (* Count the number of hypotheses in a formula *)
```
```   430 fun num_of_hyps (Const("Trueprop", _) \$ x) = num_of_hyps x
```
```   431   | num_of_hyps (Const("==>",_) \$ x \$ y) = 1 + (num_of_hyps y)
```
```   432   | num_of_hyps t = 0
```
```   433
```
```   434 (* Tactic for converting to CNF (in primitive form):
```
```   435    it takes the first subgoal of the proof state, transform all its
```
```   436    hypotheses into CNF (in primivite form) and remove the original
```
```   437    hypotheses.
```
```   438 *)
```
```   439 fun cnf_thin_tac state =
```
```   440 let val sg = Thm.sign_of_thm state
```
```   441 in
```
```   442 case (prems_of state) of
```
```   443   [] => Seq.empty
```
```   444 | (subgoal::_) =>
```
```   445   let
```
```   446     val n = num_of_hyps (strip_all_body subgoal);
```
```   447     val tac1 = METAHYPS (fn l => cut_facts_tac (mk_cnf_thms sg l) 1) 1
```
```   448   in
```
```   449     (tac1 THEN weakenings_tac n THEN (REPEAT (etac conjE 1)) ) state
```
```   450   end
```
```   451 end
```
```   452
```
```   453 (* Tactic for converting to CNF (in primitive form), keeping
```
```   454    the original hypotheses. *)
```
```   455
```
```   456 fun cnf_tac state =
```
```   457 let val sg = Thm.sign_of_thm state
```
```   458 in
```
```   459 case (prems_of state) of
```
```   460   [] => Seq.empty
```
```   461 | (subgoal::_) =>
```
```   462    METAHYPS (fn l => cut_facts_tac (mk_cnf_thms sg l) 1
```
```   463                     THEN (REPEAT (etac conjE 1)) ) 1 state
```
```   464 end
```
```   465
```
```   466
```
```   467 (***************************************************************************)
```
```   468 (*            CNF transformation by introducing new literals               *)
```
```   469
```
```   470 (*** IMPORTANT:
```
```   471   This transformation uses variables of the form "lit_i", where i is a natural
```
```   472   number. For the transformation to work, these variables must not already
```
```   473   occur freely in the formula being transformed.
```
```   474 ***)
```
```   475
```
```   476 fun ext_conj x p q r =
```
```   477    mk_conj(
```
```   478     mk_disj(Not \$ x, p),
```
```   479     mk_conj(
```
```   480       mk_disj(Not \$ x, q),
```
```   481       mk_conj(
```
```   482         mk_disj(x, mk_disj(Not \$ p, Not \$ q)),
```
```   483         mk_disj(x, r)
```
```   484       )
```
```   485     )
```
```   486    )
```
```   487
```
```   488
```
```   489 (* Transform to CNF in primitive forms, possibly introduce extra variables *)
```
```   490 fun mk_cnfx_thm sign (Const("Trueprop",_) \$ x) = mk_cnfx_thm sign x
```
```   491   | mk_cnfx_thm sign (t as (Const(_,_)))  = inst_thm sign [t] cnf_eq_id
```
```   492   | mk_cnfx_thm sign (t as (Free(_,_)))  = inst_thm sign [t] cnf_eq_id
```
```   493   | mk_cnfx_thm sign (Const("op -->", _) \$ x \$ y)  =
```
```   494        let val thm1 = inst_thm sign [x, y] cnf_imp2disj;
```
```   495            val thm2 = mk_cnfx_thm sign (mk_disj(Not \$ x, y))
```
```   496        in
```
```   497            cnf_eq_trans OF [thm1, thm2]
```
```   498        end
```
```   499
```
```   500   | mk_cnfx_thm sign (Const("op &", _) \$ x \$ y)  =
```
```   501        let val cnf1 = mk_cnfx_thm sign x
```
```   502            val cnf2 = mk_cnfx_thm sign y
```
```   503        in
```
```   504            cnf_comb2eq OF [cnf1, cnf2]
```
```   505        end
```
```   506
```
```   507   | mk_cnfx_thm sign (Const("Not",_) \$ Const("True",_)) =
```
```   508         cnf_not_true_false
```
```   509
```
```   510   | mk_cnfx_thm sign (Const("Not",_) \$ Const("False",_))  =
```
```   511         cnf_not_false_true
```
```   512
```
```   513   | mk_cnfx_thm sign (t as (Const("Not", _) \$ x))  =
```
```   514       (
```
```   515        if (is_atm x) then inst_thm sign [t] cnf_eq_id
```
```   516        else
```
```   517          let val (t1, hn_thm) = head_nnf sign t
```
```   518              val cnf_thm = mk_cnfx_thm sign t1
```
```   519          in
```
```   520              cnf_eq_trans OF [hn_thm, cnf_thm]
```
```   521          end
```
```   522        )
```
```   523
```
```   524   | mk_cnfx_thm sign (Const("op |",_) \$ (Const("op &", _) \$ p \$ q) \$ r)  =
```
```   525       if (is_lit r) then
```
```   526         let val thm1 = inst_thm sign [p, q, r] cnf_disj_conj
```
```   527             val thm2 = mk_cnfx_thm sign (mk_conj(mk_disj(p, r), mk_disj(q,r)))
```
```   528         in
```
```   529            cnf_eq_trans OF [thm1, thm2]
```
```   530         end
```
```   531       else cnfx_newlit sign p q r
```
```   532
```
```   533   | mk_cnfx_thm sign (Const("op |",_) \$ (Const("op |", _) \$ p \$ q) \$ r)  =
```
```   534        let val thm1 = inst_thm sign [p,q,r] cnf_disj_disj
```
```   535            val thm2 = mk_cnfx_thm sign (mk_disj(p, mk_disj(q,r)))
```
```   536        in
```
```   537           cnf_eq_trans OF [thm1, thm2]
```
```   538        end
```
```   539
```
```   540   | mk_cnfx_thm sign (Const("op |",_) \$ (Const("op -->", _) \$ p \$ q) \$ r) =
```
```   541        let val thm1 = inst_thm sign [p,q,r] cnf_disj_imp
```
```   542            val thm2 = mk_cnfx_thm sign (mk_disj(Not \$ p, mk_disj(q, r)))
```
```   543        in
```
```   544            cnf_eq_trans OF [thm1, thm2]
```
```   545        end
```
```   546
```
```   547   | mk_cnfx_thm sign (Const("op |",_) \$ Const("False",_) \$ p)  =
```
```   548        let val thm1 = inst_thm sign [p] cnf_disj_false;
```
```   549            val thm2 = mk_cnfx_thm sign p
```
```   550        in
```
```   551            cnf_eq_trans OF [thm1, thm2]
```
```   552        end
```
```   553
```
```   554   | mk_cnfx_thm sign (Const("op |",_) \$ Const("True",_) \$ p)  =
```
```   555        inst_thm sign [p] cnf_disj_true
```
```   556
```
```   557   | mk_cnfx_thm sign (Const("op |",_) \$ (Const("Not",_) \$ Const("True",_)) \$ p)  =
```
```   558        let val thm1 = inst_thm sign [p] cnf_disj_not_true;
```
```   559            val thm2 = mk_cnfx_thm sign p
```
```   560        in
```
```   561            cnf_eq_trans OF [thm1, thm2]
```
```   562        end
```
```   563
```
```   564   | mk_cnfx_thm sign (Const("op |",_) \$ (Const("Not",_) \$ Const("False",_)) \$ p)  =
```
```   565        inst_thm sign [p] cnf_disj_not_false
```
```   566
```
```   567   | mk_cnfx_thm sign (t as (Const("op |",_) \$ p \$ q))  =
```
```   568        if (is_lit p) then
```
```   569           (
```
```   570             if (is_clause t) then inst_thm sign [t] cnf_eq_id
```
```   571             else
```
```   572              let val thm1 = inst_thm sign [p, q] cnf_disj_sym
```
```   573                  val thm2 = mk_cnfx_thm sign (mk_disj(q, p))
```
```   574              in
```
```   575                 cnf_eq_trans OF [thm1, thm2]
```
```   576              end
```
```   577           )
```
```   578        else
```
```   579             let val (u, thm1) = head_nnf sign p
```
```   580                 val thm2 = inst_thm sign [p,u,q] cnf_cong_disj
```
```   581                 val thm3 = mk_cnfx_thm sign (mk_disj(u, q))
```
```   582             in
```
```   583                 cnf_eq_trans OF [(thm1 RS thm2), thm3]
```
```   584             end
```
```   585
```
```   586  | mk_cnfx_thm sign t  = error ("I don't know how to handle the formula " ^
```
```   587                           (Sign.string_of_term sign t))
```
```   588
```
```   589 and cnfx_newlit sign p q r  =
```
```   590    let val lit = read ("lit_" ^ (Int.toString (!lit_id)) ^ " :: bool")
```
```   591        val _ = (lit_id := !lit_id + 1)
```
```   592        val ct_lit = cterm_of sign lit
```
```   593        val x_conj = ext_conj lit p q r
```
```   594        val thm1 = inst_thm sign [p,q,r] cnf_newlit
```
```   595        val thm2 = mk_cnfx_thm sign x_conj
```
```   596        val thm3 = forall_intr ct_lit thm2
```
```   597        val thm4 = strip_shyps (thm3 COMP allI)
```
```   598        val thm5 = strip_shyps (thm4 RS cnf_all_ex)
```
```   599    in
```
```   600        cnf_eq_trans OF [thm1, thm5]
```
```   601    end
```
```   602
```
```   603
```
```   604 (* Theorems for converting formula into CNF (in primitive form), with
```
```   605    new extra variables *)
```
```   606
```
```   607
```
```   608 fun mk_cnfx_thms sg nil = nil
```
```   609   | mk_cnfx_thms sg (x::l) =
```
```   610     let val t = term_of_thm x
```
```   611     in
```
```   612       if (is_clause t) then x :: mk_cnfx_thms sg l
```
```   613       else
```
```   614        let val thm1 = mk_cnfx_thm sg t
```
```   615            val thm2 = cnf_eq_imp OF [thm1,x]
```
```   616        in
```
```   617            thm2 :: mk_cnfx_thms sg l
```
```   618        end
```
```   619     end
```
```   620
```
```   621
```
```   622 (* Tactic for converting hypotheses into CNF, possibly
```
```   623    introducing new variables *)
```
```   624
```
```   625 fun cnfx_thin_tac state =
```
```   626 let val sg = Thm.sign_of_thm state
```
```   627 in
```
```   628 case (prems_of state) of
```
```   629   [] => Seq.empty
```
```   630 | (subgoal::_) =>
```
```   631    let val n = num_of_hyps (strip_all_body subgoal);
```
```   632        val tac1 =  METAHYPS (fn l => cut_facts_tac (mk_cnfx_thms sg l) 1) 1
```
```   633    in
```
```   634       EVERY [tac1, weakenings_tac n,
```
```   635              REPEAT (etac conjE 1 ORELSE etac exE 1)] state
```
```   636    end
```
```   637 end
```
```   638
```
```   639 (* Tactic for converting the conclusion of a goal into CNF *)
```
```   640
```
```   641 fun get_concl (Const("Trueprop", _) \$ x) = get_concl x
```
```   642   | get_concl (Const("==>",_) \$ x \$ y) = get_concl y
```
```   643   | get_concl t = t
```
```   644
```
```   645 fun cnf_concl_tac' state =
```
```   646 case (prems_of state) of
```
```   647   [] => Seq.empty
```
```   648 | (subgoal::_) =>
```
```   649   let val sg = Thm.sign_of_thm state
```
```   650       val c = get_concl subgoal
```
```   651       val thm1 = (mk_cnf_thm sg c) RS cnf_eq_sym
```
```   652       val thm2 = thm1 RS subst
```
```   653   in
```
```   654     rtac thm2 1 state
```
```   655   end
```
```   656
```
```   657 val cnf_concl_tac  = METAHYPS (fn l => cnf_concl_tac') 1
```
```   658
```
```   659
```
```   660 end (*of structure*)
```