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*)