--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/cnf_funcs.ML Fri Sep 23 22:58:50 2005 +0200
@@ -0,0 +1,660 @@
+(* Title: HOL/Tools/cnf_funcs.ML
+ ID: $Id$
+ Author: Alwen Tiu, QSL Team, LORIA (http://qsl.loria.fr)
+ Copyright 2005
+
+ Description:
+ This file contains functions and tactics to transform a formula into
+ Conjunctive Normal Forms (CNF).
+ A formula in CNF is of the following form:
+
+ (x11 | x12 | .. x1m) & ... & (xm1 | xm2 | ... | xmn)
+
+ where each xij is a literal (i.e., positive or negative propositional
+ variables).
+ This kind of formula will simply be referred to as CNF.
+ A disjunction of literals is referred to as "clause".
+
+ For the purpose of SAT proof reconstruction, we also make use of another
+ representation of clauses, which we call the "raw clauses".
+ Raw clauses are of the form
+
+ (x1 ==> x2 ==> .. ==> xn ==> False)
+
+ where each xi is a literal. Note that the above raw clause corresponds
+ to the clause (x1' | ... | xn'), where each xi' is the negation normal
+ form of ~xi.
+
+ Notes for current revision:
+ - the "definitional CNF transformation" (anything with prefix cnfx_ )
+ introduces new literals of the form (lit_i) where i is an integer.
+ For these functions to work, it is necessary that no free variables
+ which names are of the form lit_i appears in the formula being
+ transformed.
+*)
+
+
+(***************************************************************************)
+
+signature CNF =
+sig
+ val cnf_tac : Tactical.tactic
+ val cnf_thin_tac : Tactical.tactic
+ val cnfx_thin_tac : Tactical.tactic
+ val cnf_concl_tac : Tactical.tactic
+ val weakening_tac : int -> Tactical.tactic
+ val mk_cnf_thm : Sign.sg -> Term.term -> Thm.thm
+ val mk_cnfx_thm : Sign.sg -> Term.term -> Thm.thm
+ val is_atm : Term.term -> bool
+ val is_lit : Term.term -> bool
+ val is_clause : Term.term -> bool
+ val is_raw_clause : Term.term -> bool
+ val cnf2raw_thm : Thm.thm -> Thm.thm
+ val cnf2raw_thms : Thm.thm list -> Thm.thm list
+ val cnf2prop : Thm.thm list -> (PropLogic.prop_formula * ((Term.term * int) list))
+end
+
+
+(***************************************************************************)
+
+structure cnf : CNF =
+struct
+
+val cur_thy = the_context();
+val mk_disj = HOLogic.mk_disj;
+val mk_conj = HOLogic.mk_conj;
+val mk_imp = HOLogic.mk_imp;
+val Not = HOLogic.Not;
+val false_const = HOLogic.false_const;
+val true_const = HOLogic.true_const;
+
+
+(* Index for new literals *)
+val lit_id = ref 0;
+
+fun thm_by_auto G =
+ prove_goal cur_thy G (fn prems => [cut_facts_tac prems 1, Auto_tac]);
+
+(***************************************************************************)
+
+
+val cnf_eq_id = thm_by_auto "(P :: bool) = P";
+
+val cnf_eq_sym = thm_by_auto "(P :: bool) = Q ==> Q = P";
+
+val cnf_not_true_false = thm_by_auto "~True = False";
+
+val cnf_not_false_true = thm_by_auto "~False = True";
+
+val cnf_imp2disj = thm_by_auto "(P --> Q) = (~P | Q)";
+
+val cnf_neg_conj = thm_by_auto "(~(P & Q)) = (~P | ~Q)";
+
+val cnf_neg_disj = thm_by_auto "(~(P | Q)) = (~P & ~Q)";
+
+val cnf_neg_imp = thm_by_auto "(~(P --> Q)) = (P & ~Q)";
+
+val cnf_double_neg = thm_by_auto "(~~P) = P";
+
+val cnf_disj_conj = thm_by_auto "((P & Q) | R) = ((P | R) & (Q | R))";
+
+val cnf_disj_imp = thm_by_auto "((P --> Q) | R) = (~P | (Q | R))";
+
+val cnf_disj_disj = thm_by_auto "((P | Q) | R) = (P | (Q | R))";
+
+val cnf_disj_false = thm_by_auto "(False | P) = P";
+
+val cnf_disj_true = thm_by_auto "(True | P) = True";
+
+val cnf_disj_not_false = thm_by_auto "(~False | P) = True";
+
+val cnf_disj_not_true = thm_by_auto "(~True | P) = P";
+
+val cnf_eq_trans = thm_by_auto "[| ( (P::bool) = Q) ; Q = R |] ==> (P = R)";
+
+val cnf_comb2eq = thm_by_auto "[| P = Q ; R = T |] ==> (P & R) = (Q & T)";
+
+val cnf_disj_sym = thm_by_auto "(P | Q) = (Q | P)";
+
+val cnf_cong_disj = thm_by_auto "(P = Q) ==> (P | R) = (Q | R)";
+
+val icnf_elim_disj1 = thm_by_auto "Q = R ==> (~P | Q) = (P --> R)";
+
+val icnf_elim_disj2 = thm_by_auto "Q = R ==> (P | Q) = (~P --> R)";
+
+val icnf_neg_false1 = thm_by_auto "(~P) = (P --> False)";
+
+val icnf_neg_false2 = thm_by_auto "P = (~P --> False)";
+
+val weakening_thm = thm_by_auto "[| P ; Q |] ==> Q";
+
+val cnf_newlit = thm_by_auto
+ "((P & Q) | R) = (EX (x :: bool). (~x | P) & (~x | Q) & (x | ~P | ~ Q) & (x | R))";
+
+val cnf_all_ex = thm_by_auto
+ "(ALL (x :: bool). (P x = Q x)) ==> (EX x. P x) = (EX x. Q x)";
+
+(* [| P ; ~P |] ==> False *)
+val cnf_notE = read_instantiate [("R", "False")] (rotate_prems 1 notE);
+
+val cnf_dneg = thm_by_auto "P ==> ~~P";
+
+val cnf_neg_disjI = thm_by_auto "[| ~P ; ~Q |] ==> ~(P | Q)";
+
+val cnf_eq_imp = thm_by_auto "[|((P::bool) = Q) ; P |] ==> Q";
+
+(***************************************************************************)
+
+fun is_atm (Const("Trueprop",_) $ x) = is_atm x
+ | is_atm (Const("==>",_) $ x $ y) = false
+ | is_atm (Const("False",_)) = false
+ | is_atm (Const("True", _)) = false
+ | is_atm (Const("op &",_) $ x $ y) = false
+ | is_atm (Const("op |",_) $ x $ y) = false
+ | is_atm (Const("op -->",_) $ x $ y) = false
+ | is_atm (Const("Not",_) $ x) = false
+ | is_atm t = true
+
+
+fun is_lit (Const("Trueprop",_) $ x) = is_lit x
+ | is_lit (Const("Not", _) $ x) = is_atm x
+ | is_lit t = is_atm t
+
+fun is_clause (Const("Trueprop",_) $ x) = is_clause x
+ | is_clause (Const("op |", _) $ x $ y) =
+ (is_clause x) andalso (is_clause y)
+ | is_clause t = is_lit t
+
+fun is_cnf (Const("Trueprop", _) $ x) = is_cnf x
+ | is_cnf (Const("op &",_) $ x $ y) = (is_cnf x) andalso (is_cnf y)
+ | is_cnf t = is_clause t
+
+
+(* Checking for raw clauses *)
+fun is_raw_clause (Const("Trueprop",_) $ x) = is_raw_clause x
+ | is_raw_clause (Const("==>",_) $ x $
+ (Const("Trueprop",_) $ Const("False",_))) = is_lit x
+ | is_raw_clause (Const("==>",_) $ x $ y) =
+ (is_lit x) andalso (is_raw_clause y)
+ | is_raw_clause t = false
+
+
+
+(* Translate a CNF clause into a raw clause *)
+fun cnf2raw_thm c =
+let val nc = c RS cnf_notE
+in
+rule_by_tactic (REPEAT_SOME (fn i =>
+ rtac cnf_dneg i
+ ORELSE rtac cnf_neg_disjI i)) nc
+handle THM _ => nc
+end
+
+fun cnf2raw_thms nil = nil
+ | cnf2raw_thms (c::l) =
+ let val t = term_of (cprop_of c)
+ in
+ if (is_clause t) then (cnf2raw_thm c) :: cnf2raw_thms l
+ else cnf2raw_thms l
+ end
+
+
+(* Translating HOL formula (in CNF) to PropLogic formula. Returns also an
+ association list, relating literals to their indices *)
+
+local
+ (* maps atomic formulas to variable numbers *)
+ val dictionary : ((Term.term * int) list) ref = ref nil;
+ val var_count = ref 0;
+ val pAnd = PropLogic.And;
+ val pOr = PropLogic.Or;
+ val pNot = PropLogic.Not;
+ val pFalse = PropLogic.False;
+ val pTrue = PropLogic.True;
+ val pVar = PropLogic.BoolVar;
+
+ fun mk_clause (Const("Trueprop",_) $ x) = mk_clause x
+ | mk_clause (Const("op |",_) $ x $ y) = pOr(mk_clause x, mk_clause y)
+ | mk_clause (Const("Not", _) $ x) = pNot (mk_clause x)
+ | mk_clause (Const("True",_)) = pTrue
+ | mk_clause (Const("False",_)) = pFalse
+ | mk_clause t =
+ let
+ val idx = AList.lookup op= (!dictionary) t
+ in
+ case idx of
+ (SOME x) => pVar x
+ | NONE =>
+ let
+ val new_var = inc var_count
+ in
+ dictionary := (t, new_var) :: (!dictionary);
+ pVar new_var
+ end
+ end
+
+ fun mk_clauses nil = pTrue
+ | mk_clauses (x::nil) = mk_clause x
+ | mk_clauses (x::l) = pAnd(mk_clause x, mk_clauses l)
+
+in
+ fun cnf2prop thms =
+ (
+ var_count := 0;
+ dictionary := nil;
+ (mk_clauses (map (fn x => term_of (cprop_of x)) thms), !dictionary)
+ )
+end
+
+
+
+(* Instantiate a theorem with a list of terms *)
+fun inst_thm sign l thm =
+ instantiate' [] (map (fn x => SOME (cterm_of sign x)) l) thm
+
+(* Tactic to remove the first hypothesis of the first subgoal. *)
+fun weakening_tac i = (dtac weakening_thm i) THEN (atac (i+1));
+
+(* Tactic for removing the n first hypotheses of the first subgoal. *)
+fun weakenings_tac 0 state = all_tac state
+ | weakenings_tac n state = ((weakening_tac 1) THEN (weakenings_tac (n-1))) state
+
+
+(*
+ Transform a formula into a "head" negation normal form, that is,
+ the top level connective is not a negation, with the exception
+ of negative literals. Returns the pair of the head normal term with
+ the theorem corresponding to the transformation.
+*)
+fun head_nnf sign (Const("Not",_) $ (Const("op &",_) $ x $ y)) =
+ let val t = mk_disj(Not $ x, Not $ y)
+ val neg_thm = inst_thm sign [x, y] cnf_neg_conj
+ in
+ (t, neg_thm)
+ end
+
+ | head_nnf sign (Const("Not", _) $ (Const("op |",_) $ x $ y)) =
+ let val t = mk_conj(Not $ x, Not $ y)
+ val neg_thm = inst_thm sign [x, y] cnf_neg_disj;
+ in
+ (t, neg_thm)
+ end
+
+ | head_nnf sign (Const("Not", _) $ (Const("op -->",_) $ x $ y)) =
+ let val t = mk_conj(x, Not $ y)
+ val neg_thm = inst_thm sign [x, y] cnf_neg_imp
+ in
+ (t, neg_thm)
+ end
+
+ | head_nnf sign (Const("Not",_) $ (Const("Not",_) $ x)) =
+ (x, inst_thm sign [x] cnf_double_neg)
+
+ | head_nnf sign (Const("Not",_) $ Const("True",_)) =
+ (false_const, cnf_not_true_false)
+
+ | head_nnf sign (Const("Not",_) $ Const("False",_)) =
+ (true_const, cnf_not_false_true)
+
+ | head_nnf sign t =
+ (t, inst_thm sign [t] cnf_eq_id)
+
+
+(***************************************************************************)
+(* Tactics for simple CNF transformation *)
+
+(* A naive procedure for CNF transformation:
+ Given any t, produce a theorem t = t', where t' is in
+ conjunction normal form
+*)
+fun mk_cnf_thm sign (Const("Trueprop",_) $ x) = mk_cnf_thm sign x
+ | mk_cnf_thm sign (t as (Const(_,_))) = inst_thm sign [t] cnf_eq_id
+ | mk_cnf_thm sign (t as (Free(_,_))) = inst_thm sign [t] cnf_eq_id
+
+ | mk_cnf_thm sign (Const("op -->", _) $ x $ y) =
+ let val thm1 = inst_thm sign [x, y] cnf_imp2disj;
+ val thm2 = mk_cnf_thm sign (mk_disj(Not $ x, y));
+ in
+ cnf_eq_trans OF [thm1, thm2]
+ end
+
+ | mk_cnf_thm sign (Const("op &", _) $ x $ y) =
+ let val cnf1 = mk_cnf_thm sign x;
+ val cnf2 = mk_cnf_thm sign y;
+ in
+ cnf_comb2eq OF [cnf1, cnf2]
+ end
+
+ | mk_cnf_thm sign (Const("Not",_) $ Const("True",_)) =
+ cnf_not_true_false
+
+ | mk_cnf_thm sign (Const("Not",_) $ Const("False",_)) =
+ cnf_not_false_true
+
+ | mk_cnf_thm sign (t as (Const("Not", _) $ x)) =
+ (
+ if (is_atm x) then inst_thm sign [t] cnf_eq_id
+ else
+ let val (t1, hn_thm) = head_nnf sign t
+ val cnf_thm = mk_cnf_thm sign t1
+ in
+ cnf_eq_trans OF [hn_thm, cnf_thm]
+ end
+ )
+
+ | mk_cnf_thm sign (Const("op |",_) $ (Const("op &", _) $ p $ q) $ r) =
+ let val thm1 = inst_thm sign [p, q, r] cnf_disj_conj;
+ val thm2 = mk_cnf_thm sign (mk_conj(mk_disj(p, r), mk_disj(q,r)));
+ in
+ cnf_eq_trans OF [thm1, thm2]
+ end
+
+ | mk_cnf_thm sign (Const("op |",_) $ (Const("op |", _) $ p $ q) $ r) =
+ let val thm1 = inst_thm sign [p,q,r] cnf_disj_disj;
+ val thm2 = mk_cnf_thm sign (mk_disj(p, mk_disj(q,r)));
+ in
+ cnf_eq_trans OF [thm1, thm2]
+ end
+
+ | mk_cnf_thm sign (Const("op |",_) $ (Const("op -->", _) $ p $ q) $ r) =
+ let val thm1 = inst_thm sign [p,q,r] cnf_disj_imp;
+ val thm2 = mk_cnf_thm sign (mk_disj(Not $ p, mk_disj(q, r)));
+ in
+ cnf_eq_trans OF [thm1, thm2]
+ end
+
+ | mk_cnf_thm sign (Const("op |",_) $ Const("False",_) $ p) =
+ let val thm1 = inst_thm sign [p] cnf_disj_false;
+ val thm2 = mk_cnf_thm sign p
+ in
+ cnf_eq_trans OF [thm1, thm2]
+ end
+
+ | mk_cnf_thm sign (Const("op |",_) $ Const("True",_) $ p) =
+ inst_thm sign [p] cnf_disj_true
+
+ | mk_cnf_thm sign (Const("op |",_) $ (Const("Not",_) $ Const("True",_)) $ p) =
+ let val thm1 = inst_thm sign [p] cnf_disj_not_true;
+ val thm2 = mk_cnf_thm sign p
+ in
+ cnf_eq_trans OF [thm1, thm2]
+ end
+
+ | mk_cnf_thm sign (Const("op |",_) $ (Const("Not",_) $ Const("False",_)) $ p) =
+ inst_thm sign [p] cnf_disj_not_false
+
+ | mk_cnf_thm sign (t as (Const("op |",_) $ p $ q)) =
+ if (is_lit p) then
+ (
+ if (is_clause t) then inst_thm sign [t] cnf_eq_id
+ else
+ let val thm1 = inst_thm sign [p, q] cnf_disj_sym;
+ val thm2 = mk_cnf_thm sign (mk_disj(q, p))
+ in
+ cnf_eq_trans OF [thm1, thm2]
+ end
+ )
+ else
+ let val (u, thm1) = head_nnf sign p;
+ val thm2 = inst_thm sign [p,u,q] cnf_cong_disj;
+ val thm3 = mk_cnf_thm sign (mk_disj(u, q))
+ in
+ cnf_eq_trans OF [(thm1 RS thm2), thm3]
+ end
+
+ | mk_cnf_thm sign t = inst_thm sign [t] cnf_eq_id
+ (* error ("I don't know how to handle the formula " ^
+ (Sign.string_of_term sign t))
+ *)
+
+fun term_of_thm c = term_of (cprop_of c)
+
+
+(* Transform a given list of theorems (thms) into CNF *)
+
+fun mk_cnf_thms sg nil = nil
+ | mk_cnf_thms sg (x::l) =
+ let val t = term_of_thm x
+ in
+ if (is_clause t) then x :: mk_cnf_thms sg l
+ else
+ let val thm1 = mk_cnf_thm sg t
+ val thm2 = cnf_eq_imp OF [thm1, x]
+ in
+ thm2 :: mk_cnf_thms sg l
+ end
+ end
+
+
+(* Count the number of hypotheses in a formula *)
+fun num_of_hyps (Const("Trueprop", _) $ x) = num_of_hyps x
+ | num_of_hyps (Const("==>",_) $ x $ y) = 1 + (num_of_hyps y)
+ | num_of_hyps t = 0
+
+(* Tactic for converting to CNF (in primitive form):
+ it takes the first subgoal of the proof state, transform all its
+ hypotheses into CNF (in primivite form) and remove the original
+ hypotheses.
+*)
+fun cnf_thin_tac state =
+let val sg = Thm.sign_of_thm state
+in
+case (prems_of state) of
+ [] => Seq.empty
+| (subgoal::_) =>
+ let
+ val n = num_of_hyps (strip_all_body subgoal);
+ val tac1 = METAHYPS (fn l => cut_facts_tac (mk_cnf_thms sg l) 1) 1
+ in
+ (tac1 THEN weakenings_tac n THEN (REPEAT (etac conjE 1)) ) state
+ end
+end
+
+(* Tactic for converting to CNF (in primitive form), keeping
+ the original hypotheses. *)
+
+fun cnf_tac state =
+let val sg = Thm.sign_of_thm state
+in
+case (prems_of state) of
+ [] => Seq.empty
+| (subgoal::_) =>
+ METAHYPS (fn l => cut_facts_tac (mk_cnf_thms sg l) 1
+ THEN (REPEAT (etac conjE 1)) ) 1 state
+end
+
+
+(***************************************************************************)
+(* CNF transformation by introducing new literals *)
+
+(*** IMPORTANT:
+ This transformation uses variables of the form "lit_i", where i is a natural
+ number. For the transformation to work, these variables must not already
+ occur freely in the formula being transformed.
+***)
+
+fun ext_conj x p q r =
+ mk_conj(
+ mk_disj(Not $ x, p),
+ mk_conj(
+ mk_disj(Not $ x, q),
+ mk_conj(
+ mk_disj(x, mk_disj(Not $ p, Not $ q)),
+ mk_disj(x, r)
+ )
+ )
+ )
+
+
+(* Transform to CNF in primitive forms, possibly introduce extra variables *)
+fun mk_cnfx_thm sign (Const("Trueprop",_) $ x) = mk_cnfx_thm sign x
+ | mk_cnfx_thm sign (t as (Const(_,_))) = inst_thm sign [t] cnf_eq_id
+ | mk_cnfx_thm sign (t as (Free(_,_))) = inst_thm sign [t] cnf_eq_id
+ | mk_cnfx_thm sign (Const("op -->", _) $ x $ y) =
+ let val thm1 = inst_thm sign [x, y] cnf_imp2disj;
+ val thm2 = mk_cnfx_thm sign (mk_disj(Not $ x, y))
+ in
+ cnf_eq_trans OF [thm1, thm2]
+ end
+
+ | mk_cnfx_thm sign (Const("op &", _) $ x $ y) =
+ let val cnf1 = mk_cnfx_thm sign x
+ val cnf2 = mk_cnfx_thm sign y
+ in
+ cnf_comb2eq OF [cnf1, cnf2]
+ end
+
+ | mk_cnfx_thm sign (Const("Not",_) $ Const("True",_)) =
+ cnf_not_true_false
+
+ | mk_cnfx_thm sign (Const("Not",_) $ Const("False",_)) =
+ cnf_not_false_true
+
+ | mk_cnfx_thm sign (t as (Const("Not", _) $ x)) =
+ (
+ if (is_atm x) then inst_thm sign [t] cnf_eq_id
+ else
+ let val (t1, hn_thm) = head_nnf sign t
+ val cnf_thm = mk_cnfx_thm sign t1
+ in
+ cnf_eq_trans OF [hn_thm, cnf_thm]
+ end
+ )
+
+ | mk_cnfx_thm sign (Const("op |",_) $ (Const("op &", _) $ p $ q) $ r) =
+ if (is_lit r) then
+ let val thm1 = inst_thm sign [p, q, r] cnf_disj_conj
+ val thm2 = mk_cnfx_thm sign (mk_conj(mk_disj(p, r), mk_disj(q,r)))
+ in
+ cnf_eq_trans OF [thm1, thm2]
+ end
+ else cnfx_newlit sign p q r
+
+ | mk_cnfx_thm sign (Const("op |",_) $ (Const("op |", _) $ p $ q) $ r) =
+ let val thm1 = inst_thm sign [p,q,r] cnf_disj_disj
+ val thm2 = mk_cnfx_thm sign (mk_disj(p, mk_disj(q,r)))
+ in
+ cnf_eq_trans OF [thm1, thm2]
+ end
+
+ | mk_cnfx_thm sign (Const("op |",_) $ (Const("op -->", _) $ p $ q) $ r) =
+ let val thm1 = inst_thm sign [p,q,r] cnf_disj_imp
+ val thm2 = mk_cnfx_thm sign (mk_disj(Not $ p, mk_disj(q, r)))
+ in
+ cnf_eq_trans OF [thm1, thm2]
+ end
+
+ | mk_cnfx_thm sign (Const("op |",_) $ Const("False",_) $ p) =
+ let val thm1 = inst_thm sign [p] cnf_disj_false;
+ val thm2 = mk_cnfx_thm sign p
+ in
+ cnf_eq_trans OF [thm1, thm2]
+ end
+
+ | mk_cnfx_thm sign (Const("op |",_) $ Const("True",_) $ p) =
+ inst_thm sign [p] cnf_disj_true
+
+ | mk_cnfx_thm sign (Const("op |",_) $ (Const("Not",_) $ Const("True",_)) $ p) =
+ let val thm1 = inst_thm sign [p] cnf_disj_not_true;
+ val thm2 = mk_cnfx_thm sign p
+ in
+ cnf_eq_trans OF [thm1, thm2]
+ end
+
+ | mk_cnfx_thm sign (Const("op |",_) $ (Const("Not",_) $ Const("False",_)) $ p) =
+ inst_thm sign [p] cnf_disj_not_false
+
+ | mk_cnfx_thm sign (t as (Const("op |",_) $ p $ q)) =
+ if (is_lit p) then
+ (
+ if (is_clause t) then inst_thm sign [t] cnf_eq_id
+ else
+ let val thm1 = inst_thm sign [p, q] cnf_disj_sym
+ val thm2 = mk_cnfx_thm sign (mk_disj(q, p))
+ in
+ cnf_eq_trans OF [thm1, thm2]
+ end
+ )
+ else
+ let val (u, thm1) = head_nnf sign p
+ val thm2 = inst_thm sign [p,u,q] cnf_cong_disj
+ val thm3 = mk_cnfx_thm sign (mk_disj(u, q))
+ in
+ cnf_eq_trans OF [(thm1 RS thm2), thm3]
+ end
+
+ | mk_cnfx_thm sign t = error ("I don't know how to handle the formula " ^
+ (Sign.string_of_term sign t))
+
+and cnfx_newlit sign p q r =
+ let val lit = read ("lit_" ^ (Int.toString (!lit_id)) ^ " :: bool")
+ val _ = (lit_id := !lit_id + 1)
+ val ct_lit = cterm_of sign lit
+ val x_conj = ext_conj lit p q r
+ val thm1 = inst_thm sign [p,q,r] cnf_newlit
+ val thm2 = mk_cnfx_thm sign x_conj
+ val thm3 = forall_intr ct_lit thm2
+ val thm4 = strip_shyps (thm3 COMP allI)
+ val thm5 = strip_shyps (thm4 RS cnf_all_ex)
+ in
+ cnf_eq_trans OF [thm1, thm5]
+ end
+
+
+(* Theorems for converting formula into CNF (in primitive form), with
+ new extra variables *)
+
+
+fun mk_cnfx_thms sg nil = nil
+ | mk_cnfx_thms sg (x::l) =
+ let val t = term_of_thm x
+ in
+ if (is_clause t) then x :: mk_cnfx_thms sg l
+ else
+ let val thm1 = mk_cnfx_thm sg t
+ val thm2 = cnf_eq_imp OF [thm1,x]
+ in
+ thm2 :: mk_cnfx_thms sg l
+ end
+ end
+
+
+(* Tactic for converting hypotheses into CNF, possibly
+ introducing new variables *)
+
+fun cnfx_thin_tac state =
+let val sg = Thm.sign_of_thm state
+in
+case (prems_of state) of
+ [] => Seq.empty
+| (subgoal::_) =>
+ let val n = num_of_hyps (strip_all_body subgoal);
+ val tac1 = METAHYPS (fn l => cut_facts_tac (mk_cnfx_thms sg l) 1) 1
+ in
+ EVERY [tac1, weakenings_tac n,
+ REPEAT (etac conjE 1 ORELSE etac exE 1)] state
+ end
+end
+
+(* Tactic for converting the conclusion of a goal into CNF *)
+
+fun get_concl (Const("Trueprop", _) $ x) = get_concl x
+ | get_concl (Const("==>",_) $ x $ y) = get_concl y
+ | get_concl t = t
+
+fun cnf_concl_tac' state =
+case (prems_of state) of
+ [] => Seq.empty
+| (subgoal::_) =>
+ let val sg = Thm.sign_of_thm state
+ val c = get_concl subgoal
+ val thm1 = (mk_cnf_thm sg c) RS cnf_eq_sym
+ val thm2 = thm1 RS subst
+ in
+ rtac thm2 1 state
+ end
+
+val cnf_concl_tac = METAHYPS (fn l => cnf_concl_tac') 1
+
+
+end (*of structure*)