src/HOL/Tools/cnf_funcs.ML
changeset 17618 1330157e156a
child 17809 195045659c06
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Tools/cnf_funcs.ML	Fri Sep 23 22:58:50 2005 +0200
     1.3 @@ -0,0 +1,660 @@
     1.4 +(*  Title:      HOL/Tools/cnf_funcs.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Alwen Tiu, QSL Team, LORIA (http://qsl.loria.fr)
     1.7 +    Copyright   2005
     1.8 +
     1.9 +  Description:
    1.10 +  This file contains functions and tactics to transform a formula into 
    1.11 +  Conjunctive Normal Forms (CNF). 
    1.12 +  A formula in CNF is of the following form:
    1.13 +
    1.14 +      (x11 | x12 | .. x1m) & ... & (xm1 | xm2 | ... | xmn)
    1.15 +
    1.16 +  where each xij is a literal (i.e., positive or negative propositional
    1.17 +  variables).
    1.18 +  This kind of formula will simply be referred to as CNF.
    1.19 +  A disjunction of literals is referred to as "clause".
    1.20 +
    1.21 +  For the purpose of SAT proof reconstruction, we also make use of another
    1.22 +  representation of clauses, which we call the "raw clauses".
    1.23 +  Raw clauses are of the form
    1.24 +
    1.25 +      (x1 ==> x2 ==> .. ==> xn ==> False)
    1.26 +
    1.27 +  where each xi is a literal. Note that the above raw clause corresponds
    1.28 +  to the clause (x1' | ... | xn'), where each xi' is the negation normal
    1.29 +  form of ~xi.
    1.30 +
    1.31 +  Notes for current revision:
    1.32 +  - the "definitional CNF transformation" (anything with prefix cnfx_ )
    1.33 +    introduces new literals of the form (lit_i) where i is an integer.
    1.34 +    For these functions to work, it is necessary that no free variables
    1.35 +    which names are of the form lit_i appears in the formula being
    1.36 +    transformed.
    1.37 +*)
    1.38 +
    1.39 +
    1.40 +(***************************************************************************)
    1.41 +
    1.42 +signature CNF =
    1.43 +sig
    1.44 +  val cnf_tac : Tactical.tactic
    1.45 +  val cnf_thin_tac : Tactical.tactic
    1.46 +  val cnfx_thin_tac : Tactical.tactic
    1.47 +  val cnf_concl_tac : Tactical.tactic
    1.48 +  val weakening_tac : int -> Tactical.tactic
    1.49 +  val mk_cnf_thm : Sign.sg -> Term.term -> Thm.thm
    1.50 +  val mk_cnfx_thm : Sign.sg -> Term.term ->  Thm.thm
    1.51 +  val is_atm : Term.term -> bool
    1.52 +  val is_lit : Term.term -> bool
    1.53 +  val is_clause : Term.term -> bool
    1.54 +  val is_raw_clause : Term.term -> bool
    1.55 +  val cnf2raw_thm : Thm.thm -> Thm.thm
    1.56 +  val cnf2raw_thms : Thm.thm list -> Thm.thm list
    1.57 +  val cnf2prop : Thm.thm list -> (PropLogic.prop_formula * ((Term.term * int) list))
    1.58 +end
    1.59 +
    1.60 +
    1.61 +(***************************************************************************)
    1.62 +
    1.63 +structure cnf : CNF =
    1.64 +struct
    1.65 +
    1.66 +val cur_thy = the_context();
    1.67 +val mk_disj = HOLogic.mk_disj;
    1.68 +val mk_conj = HOLogic.mk_conj;
    1.69 +val mk_imp  = HOLogic.mk_imp;
    1.70 +val Not = HOLogic.Not;
    1.71 +val false_const = HOLogic.false_const;
    1.72 +val true_const = HOLogic.true_const;
    1.73 +
    1.74 +
    1.75 +(* Index for new literals *)
    1.76 +val lit_id = ref 0;
    1.77 +
    1.78 +fun thm_by_auto G =
    1.79 +    prove_goal cur_thy G (fn prems => [cut_facts_tac prems 1, Auto_tac]);
    1.80 +
    1.81 +(***************************************************************************)
    1.82 +
    1.83 +
    1.84 +val cnf_eq_id = thm_by_auto "(P :: bool) = P";
    1.85 +
    1.86 +val cnf_eq_sym = thm_by_auto "(P :: bool) = Q ==> Q = P";
    1.87 +
    1.88 +val cnf_not_true_false = thm_by_auto "~True = False";
    1.89 +
    1.90 +val cnf_not_false_true = thm_by_auto "~False = True";
    1.91 +
    1.92 +val cnf_imp2disj = thm_by_auto "(P --> Q) = (~P | Q)";
    1.93 +
    1.94 +val cnf_neg_conj = thm_by_auto "(~(P & Q)) = (~P | ~Q)";
    1.95 +
    1.96 +val cnf_neg_disj = thm_by_auto "(~(P | Q)) = (~P & ~Q)";
    1.97 +
    1.98 +val cnf_neg_imp = thm_by_auto "(~(P --> Q)) = (P & ~Q)";
    1.99 +
   1.100 +val cnf_double_neg = thm_by_auto "(~~P) = P";
   1.101 + 
   1.102 +val cnf_disj_conj = thm_by_auto "((P & Q) | R) = ((P | R) & (Q | R))";
   1.103 +
   1.104 +val cnf_disj_imp = thm_by_auto "((P --> Q) | R) = (~P | (Q | R))";
   1.105 +
   1.106 +val cnf_disj_disj = thm_by_auto "((P | Q) | R) = (P | (Q | R))";
   1.107 +
   1.108 +val cnf_disj_false = thm_by_auto "(False | P) = P";
   1.109 +
   1.110 +val cnf_disj_true = thm_by_auto "(True | P) = True";
   1.111 +
   1.112 +val cnf_disj_not_false = thm_by_auto "(~False | P) = True";
   1.113 +
   1.114 +val cnf_disj_not_true = thm_by_auto "(~True | P) = P";
   1.115 +
   1.116 +val cnf_eq_trans = thm_by_auto "[| ( (P::bool) = Q) ; Q = R |] ==> (P = R)";
   1.117 +
   1.118 +val cnf_comb2eq = thm_by_auto "[| P = Q ; R = T |] ==> (P & R) = (Q & T)";
   1.119 +
   1.120 +val cnf_disj_sym = thm_by_auto "(P | Q) = (Q | P)";
   1.121 +
   1.122 +val cnf_cong_disj = thm_by_auto "(P = Q) ==> (P | R) = (Q | R)";
   1.123 +
   1.124 +val icnf_elim_disj1 = thm_by_auto "Q = R  ==> (~P | Q) = (P --> R)";
   1.125 +
   1.126 +val icnf_elim_disj2 = thm_by_auto "Q = R ==> (P | Q) = (~P --> R)";
   1.127 +
   1.128 +val icnf_neg_false1 = thm_by_auto "(~P) = (P --> False)";
   1.129 +
   1.130 +val icnf_neg_false2 = thm_by_auto "P = (~P --> False)";
   1.131 +
   1.132 +val weakening_thm = thm_by_auto "[| P ; Q |] ==> Q";
   1.133 +
   1.134 +val cnf_newlit = thm_by_auto 
   1.135 +    "((P & Q) | R) = (EX (x :: bool). (~x | P) & (~x | Q) & (x | ~P | ~ Q) & (x | R))";
   1.136 +
   1.137 +val cnf_all_ex = thm_by_auto 
   1.138 +    "(ALL (x :: bool). (P x = Q x)) ==> (EX x. P x) = (EX x. Q x)";
   1.139 +
   1.140 +(* [| P ; ~P |] ==> False *)
   1.141 +val cnf_notE = read_instantiate [("R", "False")] (rotate_prems 1 notE);
   1.142 +
   1.143 +val cnf_dneg = thm_by_auto "P ==> ~~P";
   1.144 +
   1.145 +val cnf_neg_disjI = thm_by_auto "[| ~P ; ~Q |] ==> ~(P | Q)";
   1.146 +
   1.147 +val cnf_eq_imp = thm_by_auto "[|((P::bool) = Q) ; P |] ==> Q";
   1.148 +
   1.149 +(***************************************************************************)
   1.150 +
   1.151 +fun is_atm (Const("Trueprop",_) $ x) = is_atm x
   1.152 +  | is_atm (Const("==>",_) $ x $ y) = false
   1.153 +  | is_atm (Const("False",_)) = false
   1.154 +  | is_atm (Const("True", _)) = false
   1.155 +  | is_atm (Const("op &",_) $ x $ y) = false
   1.156 +  | is_atm (Const("op |",_) $ x $ y) = false
   1.157 +  | is_atm (Const("op -->",_) $ x $ y) = false
   1.158 +  | is_atm (Const("Not",_) $ x) = false
   1.159 +  | is_atm t = true
   1.160 +
   1.161 +
   1.162 +fun is_lit (Const("Trueprop",_) $ x) = is_lit x
   1.163 +  | is_lit (Const("Not", _) $ x) = is_atm x
   1.164 +  | is_lit t = is_atm t
   1.165 +
   1.166 +fun is_clause (Const("Trueprop",_) $ x) = is_clause x
   1.167 +  | is_clause (Const("op |", _) $ x $ y) = 
   1.168 +          (is_clause x) andalso (is_clause y)
   1.169 +  | is_clause t = is_lit t
   1.170 +
   1.171 +fun is_cnf (Const("Trueprop", _) $ x) = is_cnf x
   1.172 +  | is_cnf (Const("op &",_) $ x $ y) = (is_cnf x) andalso (is_cnf y)
   1.173 +  | is_cnf t = is_clause t
   1.174 +
   1.175 +
   1.176 +(* Checking for raw clauses *)
   1.177 +fun is_raw_clause (Const("Trueprop",_) $ x) = is_raw_clause x
   1.178 +  | is_raw_clause (Const("==>",_) $ x $ 
   1.179 +                   (Const("Trueprop",_) $ Const("False",_))) = is_lit x
   1.180 +  | is_raw_clause (Const("==>",_) $ x $ y) = 
   1.181 +        (is_lit x) andalso (is_raw_clause y)
   1.182 +  | is_raw_clause t = false
   1.183 +
   1.184 +
   1.185 +
   1.186 +(* Translate a CNF clause into a raw clause *)
   1.187 +fun cnf2raw_thm c =
   1.188 +let val nc = c RS cnf_notE
   1.189 +in
   1.190 +rule_by_tactic (REPEAT_SOME (fn i => 
   1.191 +               rtac cnf_dneg i 
   1.192 +               ORELSE rtac cnf_neg_disjI i)) nc
   1.193 +handle THM _ => nc
   1.194 +end
   1.195 +
   1.196 +fun cnf2raw_thms nil = nil
   1.197 +  | cnf2raw_thms (c::l) =
   1.198 +    let val t = term_of (cprop_of c)
   1.199 +    in
   1.200 +       if (is_clause t) then (cnf2raw_thm c) :: cnf2raw_thms l
   1.201 +       else cnf2raw_thms l
   1.202 +    end
   1.203 +
   1.204 +
   1.205 +(* Translating HOL formula (in CNF) to PropLogic formula. Returns also an
   1.206 +   association list, relating literals to their indices *)
   1.207 +
   1.208 +local
   1.209 +  (* maps atomic formulas to variable numbers *)
   1.210 +  val dictionary : ((Term.term * int) list) ref = ref nil;
   1.211 +  val var_count = ref 0;
   1.212 +  val pAnd = PropLogic.And;
   1.213 +  val pOr = PropLogic.Or;
   1.214 +  val pNot = PropLogic.Not;
   1.215 +  val pFalse = PropLogic.False;
   1.216 +  val pTrue = PropLogic.True;
   1.217 +  val pVar = PropLogic.BoolVar;
   1.218 +
   1.219 +  fun mk_clause (Const("Trueprop",_) $ x) = mk_clause x
   1.220 +    | mk_clause (Const("op |",_) $ x $ y) = pOr(mk_clause x, mk_clause y)
   1.221 +    | mk_clause (Const("Not", _) $ x) = pNot (mk_clause x)
   1.222 +    | mk_clause (Const("True",_)) = pTrue
   1.223 +    | mk_clause (Const("False",_)) = pFalse
   1.224 +    | mk_clause t =
   1.225 +      let
   1.226 +         val idx = AList.lookup op= (!dictionary) t
   1.227 +      in
   1.228 +         case idx of
   1.229 +            (SOME x) => pVar x
   1.230 +           | NONE =>
   1.231 +             let
   1.232 +                val new_var = inc var_count
   1.233 +             in
   1.234 +                dictionary := (t, new_var) :: (!dictionary);
   1.235 +                pVar new_var
   1.236 +             end
   1.237 +      end
   1.238 +
   1.239 +   fun mk_clauses nil = pTrue
   1.240 +     | mk_clauses (x::nil) = mk_clause x
   1.241 +     | mk_clauses (x::l) = pAnd(mk_clause x, mk_clauses l)
   1.242 +
   1.243 +in
   1.244 +   fun cnf2prop thms =
   1.245 +   (
   1.246 +     var_count := 0;
   1.247 +     dictionary := nil;
   1.248 +     (mk_clauses (map (fn x => term_of (cprop_of x)) thms), !dictionary)
   1.249 +   )
   1.250 +end
   1.251 +
   1.252 +
   1.253 +
   1.254 +(* Instantiate a theorem with a list of terms *)
   1.255 +fun inst_thm sign l thm = 
   1.256 +  instantiate' [] (map (fn x => SOME (cterm_of sign x)) l) thm
   1.257 +
   1.258 +(* Tactic to remove the first hypothesis of the first subgoal. *) 
   1.259 +fun weakening_tac i = (dtac weakening_thm i) THEN (atac (i+1));
   1.260 +
   1.261 +(* Tactic for removing the n first hypotheses of the first subgoal. *)
   1.262 +fun weakenings_tac 0 state = all_tac state
   1.263 +  | weakenings_tac n state = ((weakening_tac  1) THEN (weakenings_tac (n-1))) state
   1.264 +
   1.265 +
   1.266 +(* 
   1.267 +  Transform a formula into a "head" negation normal form, that is, 
   1.268 +  the top level connective is not a negation, with the exception
   1.269 +  of negative literals. Returns the pair of the head normal term with
   1.270 +  the theorem corresponding to the transformation.
   1.271 +*)
   1.272 +fun head_nnf sign (Const("Not",_)  $ (Const("op &",_) $ x $ y)) =
   1.273 +    let val t = mk_disj(Not $ x, Not $ y)
   1.274 +        val neg_thm = inst_thm sign [x, y] cnf_neg_conj 
   1.275 +    in
   1.276 +        (t, neg_thm)
   1.277 +    end
   1.278 +
   1.279 +  | head_nnf sign (Const("Not", _) $ (Const("op |",_) $ x $ y)) =
   1.280 +    let val t = mk_conj(Not $ x, Not $ y)
   1.281 +        val neg_thm =  inst_thm sign [x, y] cnf_neg_disj; 
   1.282 +    in
   1.283 +        (t, neg_thm)
   1.284 +    end
   1.285 +
   1.286 +  | head_nnf sign (Const("Not", _) $ (Const("op -->",_) $ x $ y)) = 
   1.287 +    let val t = mk_conj(x, Not $ y)
   1.288 +        val neg_thm = inst_thm sign [x, y] cnf_neg_imp
   1.289 +    in
   1.290 +        (t, neg_thm)
   1.291 +    end
   1.292 +
   1.293 +  | head_nnf sign (Const("Not",_) $ (Const("Not",_) $ x)) =
   1.294 +    (x, inst_thm sign [x] cnf_double_neg)
   1.295 +
   1.296 +  | head_nnf sign (Const("Not",_) $ Const("True",_)) = 
   1.297 +      (false_const, cnf_not_true_false)
   1.298 +
   1.299 +  | head_nnf sign (Const("Not",_) $ Const("False",_)) = 
   1.300 +      (true_const, cnf_not_false_true)  
   1.301 +
   1.302 +  | head_nnf sign t = 
   1.303 +    (t, inst_thm sign [t] cnf_eq_id)
   1.304 +
   1.305 +
   1.306 +(***************************************************************************)
   1.307 +(*                  Tactics for simple CNF transformation                  *)
   1.308 +
   1.309 +(* A naive procedure for CNF transformation:
   1.310 +   Given any t, produce a theorem t = t', where t' is in
   1.311 +   conjunction normal form 
   1.312 +*)
   1.313 +fun mk_cnf_thm sign (Const("Trueprop",_) $ x) = mk_cnf_thm sign x
   1.314 +  | mk_cnf_thm sign (t as (Const(_,_))) = inst_thm sign [t] cnf_eq_id
   1.315 +  | mk_cnf_thm sign (t as (Free(_,_))) =  inst_thm sign [t] cnf_eq_id
   1.316 + 
   1.317 +  | mk_cnf_thm sign (Const("op -->", _) $ x $ y) =
   1.318 +       let val thm1 = inst_thm sign [x, y] cnf_imp2disj;
   1.319 +           val thm2 = mk_cnf_thm sign (mk_disj(Not $ x, y));
   1.320 +       in
   1.321 +           cnf_eq_trans OF [thm1, thm2]
   1.322 +       end
   1.323 +
   1.324 +  | mk_cnf_thm sign (Const("op &", _) $ x $ y) = 
   1.325 +       let val cnf1 = mk_cnf_thm sign x;
   1.326 +           val cnf2 = mk_cnf_thm sign y;
   1.327 +       in
   1.328 +           cnf_comb2eq OF [cnf1, cnf2]
   1.329 +       end
   1.330 +
   1.331 +  | mk_cnf_thm sign (Const("Not",_) $ Const("True",_)) = 
   1.332 +        cnf_not_true_false
   1.333 +
   1.334 +  | mk_cnf_thm sign (Const("Not",_) $ Const("False",_)) = 
   1.335 +        cnf_not_false_true
   1.336 +
   1.337 +  | mk_cnf_thm sign (t as (Const("Not", _) $ x)) =
   1.338 +      ( 
   1.339 +       if (is_atm x) then inst_thm sign [t] cnf_eq_id
   1.340 +       else
   1.341 +         let val (t1, hn_thm) = head_nnf sign t
   1.342 +             val cnf_thm = mk_cnf_thm sign t1
   1.343 +         in
   1.344 +             cnf_eq_trans OF [hn_thm, cnf_thm]
   1.345 +         end
   1.346 +       ) 
   1.347 +
   1.348 +  | mk_cnf_thm sign (Const("op |",_) $ (Const("op &", _) $ p $ q) $ r) =
   1.349 +       let val thm1 = inst_thm sign [p, q, r] cnf_disj_conj;
   1.350 +           val thm2 = mk_cnf_thm sign (mk_conj(mk_disj(p, r), mk_disj(q,r)));
   1.351 +       in
   1.352 +          cnf_eq_trans OF [thm1, thm2]
   1.353 +       end
   1.354 +
   1.355 +  | mk_cnf_thm sign (Const("op |",_) $ (Const("op |", _) $ p $ q) $ r) =
   1.356 +       let val thm1 = inst_thm sign [p,q,r] cnf_disj_disj;
   1.357 +           val thm2 = mk_cnf_thm sign (mk_disj(p, mk_disj(q,r)));
   1.358 +       in
   1.359 +          cnf_eq_trans OF [thm1, thm2]
   1.360 +       end
   1.361 +
   1.362 +  | mk_cnf_thm sign (Const("op |",_) $ (Const("op -->", _) $ p $ q) $ r) =                       
   1.363 +       let val thm1 = inst_thm sign [p,q,r] cnf_disj_imp;
   1.364 +           val thm2 = mk_cnf_thm sign (mk_disj(Not $ p, mk_disj(q, r)));
   1.365 +       in
   1.366 +           cnf_eq_trans OF [thm1, thm2]
   1.367 +       end
   1.368 +
   1.369 +  | mk_cnf_thm sign (Const("op |",_) $ Const("False",_) $ p) =
   1.370 +       let val thm1 = inst_thm sign [p] cnf_disj_false;
   1.371 +           val thm2 = mk_cnf_thm sign p
   1.372 +       in
   1.373 +           cnf_eq_trans OF [thm1, thm2]
   1.374 +       end
   1.375 +
   1.376 +  | mk_cnf_thm sign (Const("op |",_) $ Const("True",_) $ p) =
   1.377 +       inst_thm sign [p] cnf_disj_true
   1.378 +
   1.379 +  | mk_cnf_thm sign (Const("op |",_) $ (Const("Not",_) $ Const("True",_)) $ p) =
   1.380 +       let val thm1 = inst_thm sign [p] cnf_disj_not_true;
   1.381 +           val thm2 = mk_cnf_thm sign p
   1.382 +       in
   1.383 +           cnf_eq_trans OF [thm1, thm2]
   1.384 +       end
   1.385 +
   1.386 +  | mk_cnf_thm sign (Const("op |",_) $ (Const("Not",_) $ Const("False",_)) $ p) =
   1.387 +       inst_thm sign [p] cnf_disj_not_false
   1.388 +
   1.389 +  | mk_cnf_thm sign (t as (Const("op |",_) $ p $ q)) = 
   1.390 +       if (is_lit p) then
   1.391 +          (
   1.392 +            if (is_clause t) then inst_thm sign [t] cnf_eq_id
   1.393 +            else 
   1.394 +             let val thm1 = inst_thm sign [p, q] cnf_disj_sym;
   1.395 +                 val thm2 = mk_cnf_thm sign (mk_disj(q, p))
   1.396 +             in
   1.397 +                cnf_eq_trans OF [thm1, thm2]
   1.398 +             end
   1.399 +          )
   1.400 +       else 
   1.401 +            let val (u, thm1) = head_nnf sign p;
   1.402 +                val thm2 = inst_thm sign [p,u,q] cnf_cong_disj;
   1.403 +                val thm3 = mk_cnf_thm sign (mk_disj(u, q))
   1.404 +            in
   1.405 +                cnf_eq_trans OF [(thm1 RS thm2), thm3]
   1.406 +            end
   1.407 +
   1.408 + | mk_cnf_thm sign t = inst_thm sign [t] cnf_eq_id
   1.409 +    (* error ("I don't know how to handle the formula " ^ 
   1.410 +                          (Sign.string_of_term sign t))
   1.411 +    *)
   1.412 +
   1.413 +fun term_of_thm c = term_of (cprop_of c)
   1.414 +
   1.415 +
   1.416 +(* Transform a given list of theorems (thms) into CNF *)
   1.417 +
   1.418 +fun mk_cnf_thms sg nil = nil
   1.419 +  | mk_cnf_thms sg (x::l) = 
   1.420 +    let val t = term_of_thm x
   1.421 +    in
   1.422 +      if (is_clause t) then x :: mk_cnf_thms sg l
   1.423 +      else 
   1.424 +       let val thm1 = mk_cnf_thm sg t
   1.425 +           val thm2 = cnf_eq_imp OF [thm1, x]
   1.426 +       in 
   1.427 +           thm2 :: mk_cnf_thms sg l
   1.428 +       end
   1.429 +    end
   1.430 +
   1.431 +
   1.432 +(* Count the number of hypotheses in a formula *)
   1.433 +fun num_of_hyps (Const("Trueprop", _) $ x) = num_of_hyps x
   1.434 +  | num_of_hyps (Const("==>",_) $ x $ y) = 1 + (num_of_hyps y)
   1.435 +  | num_of_hyps t = 0
   1.436 +
   1.437 +(* Tactic for converting to CNF (in primitive form): 
   1.438 +   it takes the first subgoal of the proof state, transform all its
   1.439 +   hypotheses into CNF (in primivite form) and remove the original 
   1.440 +   hypotheses.
   1.441 +*)
   1.442 +fun cnf_thin_tac state =
   1.443 +let val sg = Thm.sign_of_thm state
   1.444 +in
   1.445 +case (prems_of state) of 
   1.446 +  [] => Seq.empty
   1.447 +| (subgoal::_) => 
   1.448 +  let 
   1.449 +    val n = num_of_hyps (strip_all_body subgoal);
   1.450 +    val tac1 = METAHYPS (fn l => cut_facts_tac (mk_cnf_thms sg l) 1) 1
   1.451 +  in
   1.452 +    (tac1 THEN weakenings_tac n THEN (REPEAT (etac conjE 1)) ) state
   1.453 +  end
   1.454 +end
   1.455 +
   1.456 +(* Tactic for converting to CNF (in primitive form), keeping 
   1.457 +   the original hypotheses. *)
   1.458 +
   1.459 +fun cnf_tac state =
   1.460 +let val sg = Thm.sign_of_thm state
   1.461 +in
   1.462 +case (prems_of state) of 
   1.463 +  [] => Seq.empty
   1.464 +| (subgoal::_) => 
   1.465 +   METAHYPS (fn l => cut_facts_tac (mk_cnf_thms sg l) 1 
   1.466 +                    THEN (REPEAT (etac conjE 1)) ) 1 state
   1.467 +end
   1.468 +
   1.469 +
   1.470 +(***************************************************************************)
   1.471 +(*            CNF transformation by introducing new literals               *)
   1.472 +
   1.473 +(*** IMPORTANT: 
   1.474 +  This transformation uses variables of the form "lit_i", where i is a natural
   1.475 +  number. For the transformation to work, these variables must not already
   1.476 +  occur freely in the formula being transformed.
   1.477 +***)
   1.478 +
   1.479 +fun ext_conj x p q r =
   1.480 +   mk_conj(
   1.481 +    mk_disj(Not $ x, p),
   1.482 +    mk_conj(
   1.483 +      mk_disj(Not $ x, q),
   1.484 +      mk_conj(
   1.485 +        mk_disj(x, mk_disj(Not $ p, Not $ q)),
   1.486 +        mk_disj(x, r)
   1.487 +      )
   1.488 +    )
   1.489 +   )
   1.490 +
   1.491 +
   1.492 +(* Transform to CNF in primitive forms, possibly introduce extra variables *)
   1.493 +fun mk_cnfx_thm sign (Const("Trueprop",_) $ x) = mk_cnfx_thm sign x 
   1.494 +  | mk_cnfx_thm sign (t as (Const(_,_)))  = inst_thm sign [t] cnf_eq_id
   1.495 +  | mk_cnfx_thm sign (t as (Free(_,_)))  = inst_thm sign [t] cnf_eq_id
   1.496 +  | mk_cnfx_thm sign (Const("op -->", _) $ x $ y)  =
   1.497 +       let val thm1 = inst_thm sign [x, y] cnf_imp2disj;
   1.498 +           val thm2 = mk_cnfx_thm sign (mk_disj(Not $ x, y)) 
   1.499 +       in
   1.500 +           cnf_eq_trans OF [thm1, thm2]
   1.501 +       end
   1.502 +
   1.503 +  | mk_cnfx_thm sign (Const("op &", _) $ x $ y)  = 
   1.504 +       let val cnf1 = mk_cnfx_thm sign x
   1.505 +           val cnf2 = mk_cnfx_thm sign y
   1.506 +       in
   1.507 +           cnf_comb2eq OF [cnf1, cnf2]
   1.508 +       end
   1.509 +
   1.510 +  | mk_cnfx_thm sign (Const("Not",_) $ Const("True",_)) = 
   1.511 +        cnf_not_true_false
   1.512 +
   1.513 +  | mk_cnfx_thm sign (Const("Not",_) $ Const("False",_))  = 
   1.514 +        cnf_not_false_true
   1.515 +
   1.516 +  | mk_cnfx_thm sign (t as (Const("Not", _) $ x))  =
   1.517 +      ( 
   1.518 +       if (is_atm x) then inst_thm sign [t] cnf_eq_id
   1.519 +       else
   1.520 +         let val (t1, hn_thm) = head_nnf sign t
   1.521 +             val cnf_thm = mk_cnfx_thm sign t1 
   1.522 +         in
   1.523 +             cnf_eq_trans OF [hn_thm, cnf_thm]
   1.524 +         end
   1.525 +       ) 
   1.526 +
   1.527 +  | mk_cnfx_thm sign (Const("op |",_) $ (Const("op &", _) $ p $ q) $ r)  =
   1.528 +      if (is_lit r) then
   1.529 +        let val thm1 = inst_thm sign [p, q, r] cnf_disj_conj
   1.530 +            val thm2 = mk_cnfx_thm sign (mk_conj(mk_disj(p, r), mk_disj(q,r)))
   1.531 +        in
   1.532 +           cnf_eq_trans OF [thm1, thm2]
   1.533 +        end
   1.534 +      else cnfx_newlit sign p q r 
   1.535 +
   1.536 +  | mk_cnfx_thm sign (Const("op |",_) $ (Const("op |", _) $ p $ q) $ r)  =
   1.537 +       let val thm1 = inst_thm sign [p,q,r] cnf_disj_disj
   1.538 +           val thm2 = mk_cnfx_thm sign (mk_disj(p, mk_disj(q,r))) 
   1.539 +       in
   1.540 +          cnf_eq_trans OF [thm1, thm2]
   1.541 +       end
   1.542 +
   1.543 +  | mk_cnfx_thm sign (Const("op |",_) $ (Const("op -->", _) $ p $ q) $ r) =                       
   1.544 +       let val thm1 = inst_thm sign [p,q,r] cnf_disj_imp
   1.545 +           val thm2 = mk_cnfx_thm sign (mk_disj(Not $ p, mk_disj(q, r))) 
   1.546 +       in
   1.547 +           cnf_eq_trans OF [thm1, thm2]
   1.548 +       end
   1.549 +
   1.550 +  | mk_cnfx_thm sign (Const("op |",_) $ Const("False",_) $ p)  =
   1.551 +       let val thm1 = inst_thm sign [p] cnf_disj_false;
   1.552 +           val thm2 = mk_cnfx_thm sign p 
   1.553 +       in
   1.554 +           cnf_eq_trans OF [thm1, thm2]
   1.555 +       end
   1.556 +
   1.557 +  | mk_cnfx_thm sign (Const("op |",_) $ Const("True",_) $ p)  =
   1.558 +       inst_thm sign [p] cnf_disj_true
   1.559 +
   1.560 +  | mk_cnfx_thm sign (Const("op |",_) $ (Const("Not",_) $ Const("True",_)) $ p)  =
   1.561 +       let val thm1 = inst_thm sign [p] cnf_disj_not_true;
   1.562 +           val thm2 = mk_cnfx_thm sign p 
   1.563 +       in
   1.564 +           cnf_eq_trans OF [thm1, thm2]
   1.565 +       end
   1.566 +
   1.567 +  | mk_cnfx_thm sign (Const("op |",_) $ (Const("Not",_) $ Const("False",_)) $ p)  =
   1.568 +       inst_thm sign [p] cnf_disj_not_false
   1.569 +
   1.570 +  | mk_cnfx_thm sign (t as (Const("op |",_) $ p $ q))  = 
   1.571 +       if (is_lit p) then
   1.572 +          (
   1.573 +            if (is_clause t) then inst_thm sign [t] cnf_eq_id
   1.574 +            else 
   1.575 +             let val thm1 = inst_thm sign [p, q] cnf_disj_sym
   1.576 +                 val thm2 = mk_cnfx_thm sign (mk_disj(q, p)) 
   1.577 +             in
   1.578 +                cnf_eq_trans OF [thm1, thm2]
   1.579 +             end
   1.580 +          )
   1.581 +       else 
   1.582 +            let val (u, thm1) = head_nnf sign p
   1.583 +                val thm2 = inst_thm sign [p,u,q] cnf_cong_disj
   1.584 +                val thm3 = mk_cnfx_thm sign (mk_disj(u, q)) 
   1.585 +            in
   1.586 +                cnf_eq_trans OF [(thm1 RS thm2), thm3]
   1.587 +            end
   1.588 +
   1.589 + | mk_cnfx_thm sign t  = error ("I don't know how to handle the formula " ^ 
   1.590 +                          (Sign.string_of_term sign t))
   1.591 +
   1.592 +and cnfx_newlit sign p q r  = 
   1.593 +   let val lit = read ("lit_" ^ (Int.toString (!lit_id)) ^ " :: bool")
   1.594 +       val _ = (lit_id := !lit_id + 1)
   1.595 +       val ct_lit = cterm_of sign lit
   1.596 +       val x_conj = ext_conj lit p q r
   1.597 +       val thm1 = inst_thm sign [p,q,r] cnf_newlit
   1.598 +       val thm2 = mk_cnfx_thm sign x_conj 
   1.599 +       val thm3 = forall_intr ct_lit thm2
   1.600 +       val thm4 = strip_shyps (thm3 COMP allI)
   1.601 +       val thm5 = strip_shyps (thm4 RS cnf_all_ex)
   1.602 +   in
   1.603 +       cnf_eq_trans OF [thm1, thm5]
   1.604 +   end
   1.605 +
   1.606 +
   1.607 +(* Theorems for converting formula into CNF (in primitive form), with 
   1.608 +   new extra variables *)
   1.609 +
   1.610 +
   1.611 +fun mk_cnfx_thms sg nil = nil
   1.612 +  | mk_cnfx_thms sg (x::l) = 
   1.613 +    let val t = term_of_thm x
   1.614 +    in
   1.615 +      if (is_clause t) then x :: mk_cnfx_thms sg l
   1.616 +      else 
   1.617 +       let val thm1 = mk_cnfx_thm sg t
   1.618 +           val thm2 = cnf_eq_imp OF [thm1,x]
   1.619 +       in 
   1.620 +           thm2 :: mk_cnfx_thms sg l
   1.621 +       end
   1.622 +    end
   1.623 +
   1.624 +
   1.625 +(* Tactic for converting hypotheses into CNF, possibly
   1.626 +   introducing new variables *)
   1.627 +
   1.628 +fun cnfx_thin_tac state =
   1.629 +let val sg = Thm.sign_of_thm state
   1.630 +in
   1.631 +case (prems_of state) of 
   1.632 +  [] => Seq.empty
   1.633 +| (subgoal::_) => 
   1.634 +   let val n = num_of_hyps (strip_all_body subgoal);
   1.635 +       val tac1 =  METAHYPS (fn l => cut_facts_tac (mk_cnfx_thms sg l) 1) 1
   1.636 +   in
   1.637 +      EVERY [tac1, weakenings_tac n, 
   1.638 +             REPEAT (etac conjE 1 ORELSE etac exE 1)] state
   1.639 +   end
   1.640 +end
   1.641 +
   1.642 +(* Tactic for converting the conclusion of a goal into CNF *)
   1.643 +
   1.644 +fun get_concl (Const("Trueprop", _) $ x) = get_concl x
   1.645 +  | get_concl (Const("==>",_) $ x $ y) = get_concl y
   1.646 +  | get_concl t = t
   1.647 +
   1.648 +fun cnf_concl_tac' state =
   1.649 +case (prems_of state) of 
   1.650 +  [] => Seq.empty
   1.651 +| (subgoal::_) =>
   1.652 +  let val sg = Thm.sign_of_thm state
   1.653 +      val c = get_concl subgoal
   1.654 +      val thm1 = (mk_cnf_thm sg c) RS cnf_eq_sym
   1.655 +      val thm2 = thm1 RS subst
   1.656 +  in
   1.657 +    rtac thm2 1 state
   1.658 +  end
   1.659 +
   1.660 +val cnf_concl_tac  = METAHYPS (fn l => cnf_concl_tac') 1 
   1.661 +
   1.662 +
   1.663 +end (*of structure*)