# File cnf_funcs.ML

    (*  Title:      HOL/Tools/cnf_funcs.ML
        ID:         $Id: cnf_funcs.ML,v 1.1 2005/09/23 20:58:50 webertj Exp $
        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*)