--- /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*)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/sat_funcs.ML Fri Sep 23 22:58:50 2005 +0200
@@ -0,0 +1,328 @@
+(* Title: HOL/Tools/sat_funcs.ML
+ ID: $Id$
+ Author: Stephan Merz and Alwen Tiu, QSL Team, LORIA (http://qsl.loria.fr)
+ Copyright 2005
+
+
+Proof reconstruction from SAT solvers.
+
+ Description:
+ This file defines several tactics to invoke a proof-producing
+ SAT solver on a propositional goal in clausal form.
+
+ We use a sequent presentation of clauses to speed up resolution
+ proof reconstruction.
+ We call such clauses as "raw clauses", which are of the form
+ [| c1; c2; ...; ck |] ==> False
+ where each clause ci is of the form
+ [|l1, l2, ..., lm |] ==> False,
+ where li is a literal (see also comments in cnf_funcs.ML).
+
+ -- observe that this is the "dualized" version of the standard
+ clausal form
+ l1' \/ l2' \/ ... \/ lm', where li is the negation normal
+ form of ~li'.
+ The tactic produces a clause representation of the given goal
+ in DIMACS format and invokes a SAT solver, which should return
+ a proof consisting of a sequence of resolution steps, indicating
+ the two input clauses and the variable resolved upon, and resulting
+ in new clauses, leading to the empty clause (i.e., False).
+ The tactic replays this proof in Isabelle and thus solves the
+ overall goal.
+
+ There are two SAT tactics available. They differ in the CNF transformation
+ used. The "sat_tac" uses naive CNF transformation to transform the theorem
+ to be proved before giving it to SAT solver. The naive transformation in
+ some worst case can lead to explonential blow up in formula size.
+ The other tactic, the "satx_tac" uses the "definitional CNF transformation"
+ which produces formula of linear size increase compared to the input formula.
+ This transformation introduces new variables. See also cnf_funcs.ML for
+ more comments.
+
+
+ Notes for the current revision:
+ - The current version supports only zChaff prover.
+ - The environment variable ZCHAFF_HOME must be set to point to
+ the directory where zChaff executable resides
+ - The environment variable ZCHAFF_VERSION must be set according to
+ the version of zChaff used. Current supported version of zChaff:
+ zChaff version 2004.11.15
+
+*)
+
+(***************************************************************************)
+(** Array of clauses **)
+
+signature CLAUSEARR =
+sig
+ val init : int -> unit
+ val register_at : int -> Thm.thm -> unit
+ val register_list : Thm.thm list -> unit
+ val getClause : int -> Thm.thm option
+end
+
+structure ClauseArr : CLAUSEARR =
+struct
+
+val clauses : ((Thm.thm option) array) ref = ref (Array.array(1, NONE));
+
+fun init size = (clauses := Array.array(size, NONE))
+
+fun register_at i c = Array.update (!clauses, i, (SOME c))
+
+fun reg_list n nil = ()
+ | reg_list n (x::l) =
+ (register_at n x; reg_list (n+1) l)
+
+fun register_list l = reg_list 0 l
+
+fun getClause i = Array.sub (!clauses, i)
+
+end
+
+
+(***************************************************************************)
+
+signature SAT =
+sig
+ val trace_sat : bool ref (* trace tactic *)
+ val sat_tac : Tactical.tactic
+ val satx_tac : Tactical.tactic
+end
+
+functor SATFunc (structure cnf_struct : CNF) : SAT =
+struct
+
+structure cnf = cnf_struct
+
+val trace_sat = ref false; (* debugging flag *)
+
+
+(* Look up the Isabelle atom corresponding to a DIMACS index in the
+ reverse dictionary. This entry should exist, otherwise an error
+ is raised.
+*)
+fun rev_lookup idx dictionary =
+let
+ fun rev_assoc [] = NONE
+ | rev_assoc ((key, entry)::list) =
+ if entry = idx then SOME key else rev_assoc list
+in
+ the (rev_assoc dictionary)
+end;
+
+
+(* Convert rules of the form
+ l1 ==> l2 ==> .. ==> li ==> .. ==> False
+ to
+ l1 ==> l2 ==> .... ==> ~li
+*)
+fun swap_prem rslv c =
+let
+ val thm1 = rule_by_tactic (metacut_tac c 1 THEN
+ (atac 1) THEN (REPEAT_SOME atac)) rslv
+in
+ rule_by_tactic (ALLGOALS (cnf.weakening_tac)) thm1
+end
+
+(*** Proof reconstruction: given two clauses
+ [| x1 ; .. ; a ; .. ; xn |] ==> False
+ and
+ [| y1 ; .. ; ~a ; .. ; ym |] ==> False ,
+
+ we firt convert the first clause into
+
+ [| x1 ; ... ; xn |] ==> ~a (using swap_prem)
+
+ and do a resolution with the second clause to produce
+ [| y1 ; ... ; x1 ; ... ; xn ; ... ; yn |] ==> False
+
+***)
+
+fun dual (Const("Trueprop",_) $ x) (Const("Trueprop",_) $ y) = dual x y
+ | dual (Const("Not",_) $ x) y = (x = y)
+ | dual x (Const("Not",_) $ y) = (x = y)
+ | dual x y = false
+
+(* Check if an atom has a dual in a list of atoms *)
+
+fun dual_mem x nil = false
+ | dual_mem x (y::l) = if (dual x y) then true else dual_mem x l
+
+
+fun replay_chain sg idx (c::cs) =
+let
+ val (SOME fc) = ClauseArr.getClause c;
+
+ fun strip_neg (Const("Trueprop", _) $ x) = strip_neg x
+ | strip_neg (Const("Not",_) $ x) = x
+ | strip_neg x = x
+
+ (* Find out which atom (literal) is used in the resolution *)
+ fun res_atom nil l = raise THM ("Proof reconstruction failed!", 0, [])
+ | res_atom (x::l1) l2 =
+ if (dual_mem x l2) then strip_neg x
+ else res_atom l1 l2
+
+ fun replay old [] = old
+ | replay old (cls :: clss) =
+ let
+ val (SOME icls) = ClauseArr.getClause cls;
+ val var = res_atom (prems_of old) (prems_of icls);
+ val atom = cterm_of sg var;
+ val rslv = instantiate' [] [SOME atom] notI;
+
+ val _ = if (!trace_sat) then
+ (
+ writeln "-- resolving clause:";
+ print_thm old;
+ writeln "-- with clause: ";
+ print_thm icls;
+ writeln "-- using ";
+ writeln (string_of_cterm atom)
+ ) else ();
+
+ val thm1 = (
+ rule_by_tactic (REPEAT_SOME (rtac (swap_prem rslv old))) icls
+ handle THM _ =>
+ rule_by_tactic (REPEAT_SOME (rtac (swap_prem rslv icls))) old );
+
+ val new = rule_by_tactic distinct_subgoals_tac thm1;
+ val _ = if (!trace_sat) then (writeln "-- resulting clause:"; print_thm new)
+ else ()
+ in
+ replay new clss
+ end
+in
+ ClauseArr.register_at idx (replay fc cs);
+ if (!trace_sat) then (
+ writeln ("-- Replay chain successful. " ^
+ "The resulting clause stored at #" ^ (Int.toString idx))
+ ) else ()
+end
+
+
+(* Replay the resolution proof from file prf_file with hypotheses hyps.
+ Returns the theorem established by the proof (which is just False).
+*)
+fun replay_prf sg tab size =
+ let
+ val prf = Inttab.dest tab;
+
+ fun complete nil = true
+ | complete (x::l) = (
+ case ClauseArr.getClause x of
+ NONE => false
+ | (SOME _) => complete l)
+
+ fun do_chains [] = ()
+ | do_chains (pr :: rs) =
+ let val (idx, cls) = pr
+ in
+ if (complete cls) then
+ (replay_chain sg idx cls; do_chains rs)
+ else do_chains (rs @ [pr])
+ end
+ in
+ if (!trace_sat) then (
+ writeln "Proof trace from SAT solver: ";
+ print prf ; ()
+ ) else () ;
+ do_chains prf;
+ ClauseArr.getClause size
+ end;
+
+
+(***************************************************************************)
+(*** Functions to build the sat tactic ***)
+
+(* A trivial tactic, used in preprocessing before calling the main
+ tactic *)
+
+val pre_sat_tac = (REPEAT (etac conjE 1)) THEN
+ (REPEAT ((atac 1) ORELSE (etac FalseE 1)))
+
+fun collect_atoms (Const("Trueprop",_) $ x) l = collect_atoms x l
+ | collect_atoms (Const("op |", _) $ x $ y) l =
+ collect_atoms x (collect_atoms y l)
+ | collect_atoms x l = if (x mem l) then l else (x::l)
+
+fun has_duals nil = false
+ | has_duals (x::l) = if (dual_mem x l) then true else has_duals l
+
+fun trivial_clause (Const("True",_)) = true
+ | trivial_clause c = has_duals (collect_atoms c nil)
+
+(* Remove trivial clauses *)
+fun filter_clauses nil = nil
+ | filter_clauses (x::l) =
+ if (trivial_clause (term_of (cprop_of x))) then filter_clauses l
+ else (x:: filter_clauses l)
+
+fun is_true assignment x =
+ case (assignment x) of
+ NONE => false
+ | SOME b => b
+
+fun get_model dict assignment =
+ map (fn (x,y) => x) (List.filter (fn (x,y) => is_true assignment y) dict)
+
+fun string_of_model sg nil = ""
+ | string_of_model sg [x] = Sign.string_of_term sg x
+ | string_of_model sg (x::l) = (Sign.string_of_term sg x) ^ ", " ^ (string_of_model sg l)
+
+(* Run external SAT solver with the given clauses. Reconstruct a proof from
+ the resulting proof trace of the SAT solver.
+*)
+
+fun rawsat_thm sg prems =
+let val thms = filter_clauses prems
+ val (fm, dict) = cnf.cnf2prop thms
+ val raw_thms = cnf.cnf2raw_thms thms
+in
+ let
+ val result = SatSolver.invoke_solver "zchaff_with_proofs" fm;
+ in
+ case result of
+ (SatSolver.UNSATISFIABLE (SOME (table, size))) =>
+ let val _ = ClauseArr.init (size + 1);
+ val _ = ClauseArr.register_list
+ (map (fn x => (rule_by_tactic distinct_subgoals_tac x)) raw_thms);
+ val (SOME thm1) = replay_prf sg table size
+ in
+ thm1
+ end
+ | (SatSolver.SATISFIABLE model) =>
+ let val msg = "\nSAT solver found a countermodel:\n{ " ^
+ (string_of_model sg (get_model dict model)) ^ " }\n"
+ in
+ raise THM (msg, 0, [])
+ end
+ | _ => raise THM ("SAT solver failed!\n", 0, [])
+
+ end
+end
+
+fun cnfsat_basic_tac state =
+let val sg = Thm.sign_of_thm state
+in
+ METAHYPS (fn prems => rtac (rawsat_thm sg prems) 1) 1 state
+end
+
+(* Tactic for calling external SAT solver, taking as input CNF clauses *)
+val cnfsat_tac = pre_sat_tac THEN (IF_UNSOLVED cnfsat_basic_tac)
+
+
+(*
+ Tactic for calling external SAT solver, taking as input arbitrary formula.
+*)
+val sat_tac = cnf.cnf_thin_tac THEN cnfsat_tac;
+
+(*
+ Tactic for calling external SAT solver, taking as input arbitratry formula.
+ The input is translated to CNF (in primitive form), possibly introducing
+ new literals.
+*)
+val satx_tac = cnf.cnfx_thin_tac THEN cnfsat_tac;
+
+end (*of structure*)