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