Tactics sat and satx reimplemented, several improvements
authorwebertj
Sun Oct 09 17:06:03 2005 +0200 (2005-10-09)
changeset 17809195045659c06
parent 17808 81c113e4d6fc
child 17810 3bdf516d93d8
Tactics sat and satx reimplemented, several improvements
NEWS
src/HOL/SAT.thy
src/HOL/Tools/cnf_funcs.ML
src/HOL/Tools/prop_logic.ML
src/HOL/Tools/sat_funcs.ML
src/HOL/ex/SAT_Examples.thy
     1.1 --- a/NEWS	Sat Oct 08 23:43:15 2005 +0200
     1.2 +++ b/NEWS	Sun Oct 09 17:06:03 2005 +0200
     1.3 @@ -28,6 +28,11 @@
     1.4  "t = s" to False (by simproc "neq_simproc"). For backward compatibility
     1.5  this can be disabled by ML"reset use_neq_simproc".
     1.6  
     1.7 +* Tactics 'sat' and 'satx' reimplemented, several improvements: goals
     1.8 +no longer need to be stated as "<prems> ==> False", equivalences (i.e.
     1.9 +"=" on type bool) are handled, variable names of the form "lit_<n>" are
    1.10 +no longer reserved, significant speedup.
    1.11 +
    1.12  
    1.13  New in Isabelle2005 (October 2005)
    1.14  ----------------------------------
     2.1 --- a/src/HOL/SAT.thy	Sat Oct 08 23:43:15 2005 +0200
     2.2 +++ b/src/HOL/SAT.thy	Sun Oct 09 17:06:03 2005 +0200
     2.3 @@ -30,10 +30,10 @@
     2.4  
     2.5  ML {* structure sat = SATFunc(structure cnf = cnf); *}
     2.6  
     2.7 -method_setup sat = {* Method.no_args (Method.SIMPLE_METHOD sat.sat_tac) *}
     2.8 +method_setup sat = {* Method.no_args (Method.SIMPLE_METHOD (sat.sat_tac 1)) *}
     2.9    "SAT solver"
    2.10  
    2.11 -method_setup satx = {* Method.no_args (Method.SIMPLE_METHOD sat.satx_tac) *}
    2.12 +method_setup satx = {* Method.no_args (Method.SIMPLE_METHOD (sat.satx_tac 1)) *}
    2.13    "SAT solver (with definitional CNF)"
    2.14  
    2.15  end
     3.1 --- a/src/HOL/Tools/cnf_funcs.ML	Sat Oct 08 23:43:15 2005 +0200
     3.2 +++ b/src/HOL/Tools/cnf_funcs.ML	Sun Oct 09 17:06:03 2005 +0200
     3.3 @@ -1,660 +1,579 @@
     3.4  (*  Title:      HOL/Tools/cnf_funcs.ML
     3.5      ID:         $Id$
     3.6      Author:     Alwen Tiu, QSL Team, LORIA (http://qsl.loria.fr)
     3.7 +    Author:     Tjark Weber
     3.8      Copyright   2005
     3.9  
    3.10    Description:
    3.11 -  This file contains functions and tactics to transform a formula into 
    3.12 -  Conjunctive Normal Forms (CNF). 
    3.13 +  This file contains functions and tactics to transform a formula into
    3.14 +  Conjunctive Normal Form (CNF).
    3.15    A formula in CNF is of the following form:
    3.16  
    3.17 -      (x11 | x12 | .. x1m) & ... & (xm1 | xm2 | ... | xmn)
    3.18 +      (x11 | x12 | .. x1n) & ... & (xm1 | xm2 | ... | xmk)
    3.19 +      False
    3.20 +      True
    3.21  
    3.22 -  where each xij is a literal (i.e., positive or negative propositional
    3.23 -  variables).
    3.24 -  This kind of formula will simply be referred to as CNF.
    3.25 -  A disjunction of literals is referred to as "clause".
    3.26 +  where each xij is a literal (a positive or negative atomic Boolean term),
    3.27 +  i.e. the formula is a conjunction of disjunctions of literals, or
    3.28 +  "False", or "True".
    3.29 +
    3.30 +  A (non-empty) disjunction of literals is referred to as "clause".
    3.31  
    3.32    For the purpose of SAT proof reconstruction, we also make use of another
    3.33    representation of clauses, which we call the "raw clauses".
    3.34    Raw clauses are of the form
    3.35  
    3.36 -      (x1 ==> x2 ==> .. ==> xn ==> False)
    3.37 +      x1 ==> x2 ==> .. ==> xn ==> False ,
    3.38  
    3.39    where each xi is a literal. Note that the above raw clause corresponds
    3.40    to the clause (x1' | ... | xn'), where each xi' is the negation normal
    3.41    form of ~xi.
    3.42 -
    3.43 -  Notes for current revision:
    3.44 -  - the "definitional CNF transformation" (anything with prefix cnfx_ )
    3.45 -    introduces new literals of the form (lit_i) where i is an integer.
    3.46 -    For these functions to work, it is necessary that no free variables
    3.47 -    which names are of the form lit_i appears in the formula being
    3.48 -    transformed.
    3.49  *)
    3.50  
    3.51 -
    3.52 -(***************************************************************************)
    3.53 -
    3.54  signature CNF =
    3.55  sig
    3.56 -  val cnf_tac : Tactical.tactic
    3.57 -  val cnf_thin_tac : Tactical.tactic
    3.58 -  val cnfx_thin_tac : Tactical.tactic
    3.59 -  val cnf_concl_tac : Tactical.tactic
    3.60 -  val weakening_tac : int -> Tactical.tactic
    3.61 -  val mk_cnf_thm : Sign.sg -> Term.term -> Thm.thm
    3.62 -  val mk_cnfx_thm : Sign.sg -> Term.term ->  Thm.thm
    3.63 -  val is_atm : Term.term -> bool
    3.64 -  val is_lit : Term.term -> bool
    3.65 -  val is_clause : Term.term -> bool
    3.66 -  val is_raw_clause : Term.term -> bool
    3.67 -  val cnf2raw_thm : Thm.thm -> Thm.thm
    3.68 -  val cnf2raw_thms : Thm.thm list -> Thm.thm list
    3.69 -  val cnf2prop : Thm.thm list -> (PropLogic.prop_formula * ((Term.term * int) list))
    3.70 -end
    3.71 +	val is_atom           : Term.term -> bool
    3.72 +	val is_literal        : Term.term -> bool
    3.73 +	val is_clause         : Term.term -> bool
    3.74 +	val clause_is_trivial : Term.term -> bool
    3.75 +
    3.76 +	val is_raw_clause  : Term.term -> bool
    3.77 +	val clause2raw_thm : Thm.thm -> Thm.thm
    3.78  
    3.79 +	val weakening_tac : int -> Tactical.tactic  (* removes the first hypothesis of a subgoal *)
    3.80  
    3.81 -(***************************************************************************)
    3.82 +	val make_cnf_thm  : Theory.theory -> Term.term -> Thm.thm
    3.83 +	val make_cnfx_thm : Theory.theory -> Term.term ->  Thm.thm
    3.84 +	val cnf_rewrite_tac  : int -> Tactical.tactic  (* converts all prems of a subgoal to CNF *)
    3.85 +	val cnfx_rewrite_tac : int -> Tactical.tactic  (* converts all prems of a subgoal to (almost) definitional CNF *)
    3.86 +end;
    3.87  
    3.88  structure cnf : CNF =
    3.89  struct
    3.90  
    3.91 -val cur_thy = the_context();
    3.92 -val mk_disj = HOLogic.mk_disj;
    3.93 -val mk_conj = HOLogic.mk_conj;
    3.94 -val mk_imp  = HOLogic.mk_imp;
    3.95 -val Not = HOLogic.Not;
    3.96 -val false_const = HOLogic.false_const;
    3.97 -val true_const = HOLogic.true_const;
    3.98 -
    3.99 -
   3.100 -(* Index for new literals *)
   3.101 -val lit_id = ref 0;
   3.102 -
   3.103 +(* string -> Thm.thm *)
   3.104  fun thm_by_auto G =
   3.105 -    prove_goal cur_thy G (fn prems => [cut_facts_tac prems 1, Auto_tac]);
   3.106 -
   3.107 -(***************************************************************************)
   3.108 +	prove_goal (the_context ()) G (fn prems => [cut_facts_tac prems 1, Auto_tac]);
   3.109  
   3.110 -
   3.111 -val cnf_eq_id = thm_by_auto "(P :: bool) = P";
   3.112 -
   3.113 -val cnf_eq_sym = thm_by_auto "(P :: bool) = Q ==> Q = P";
   3.114 -
   3.115 -val cnf_not_true_false = thm_by_auto "~True = False";
   3.116 +(* Thm.thm *)
   3.117 +val clause2raw_notE      = thm_by_auto "[| P; ~P |] ==> False";
   3.118 +val clause2raw_not_disj  = thm_by_auto "[| ~P; ~Q |] ==> ~(P | Q)";
   3.119 +val clause2raw_not_not   = thm_by_auto "P ==> ~~P";
   3.120  
   3.121 -val cnf_not_false_true = thm_by_auto "~False = True";
   3.122 -
   3.123 -val cnf_imp2disj = thm_by_auto "(P --> Q) = (~P | Q)";
   3.124 -
   3.125 -val cnf_neg_conj = thm_by_auto "(~(P & Q)) = (~P | ~Q)";
   3.126 -
   3.127 -val cnf_neg_disj = thm_by_auto "(~(P | Q)) = (~P & ~Q)";
   3.128 -
   3.129 -val cnf_neg_imp = thm_by_auto "(~(P --> Q)) = (P & ~Q)";
   3.130 +val iff_refl             = thm_by_auto "(P::bool) = P";
   3.131 +val iff_trans            = thm_by_auto "[| (P::bool) = Q; Q = R |] ==> P = R";
   3.132 +val conj_cong            = thm_by_auto "[| P = P'; Q = Q' |] ==> (P & Q) = (P' & Q')";
   3.133 +val disj_cong            = thm_by_auto "[| P = P'; Q = Q' |] ==> (P | Q) = (P' | Q')";
   3.134  
   3.135 -val cnf_double_neg = thm_by_auto "(~~P) = P";
   3.136 - 
   3.137 -val cnf_disj_conj = thm_by_auto "((P & Q) | R) = ((P | R) & (Q | R))";
   3.138 -
   3.139 -val cnf_disj_imp = thm_by_auto "((P --> Q) | R) = (~P | (Q | R))";
   3.140 -
   3.141 -val cnf_disj_disj = thm_by_auto "((P | Q) | R) = (P | (Q | R))";
   3.142 -
   3.143 -val cnf_disj_false = thm_by_auto "(False | P) = P";
   3.144 -
   3.145 -val cnf_disj_true = thm_by_auto "(True | P) = True";
   3.146 -
   3.147 -val cnf_disj_not_false = thm_by_auto "(~False | P) = True";
   3.148 -
   3.149 -val cnf_disj_not_true = thm_by_auto "(~True | P) = P";
   3.150 -
   3.151 -val cnf_eq_trans = thm_by_auto "[| ( (P::bool) = Q) ; Q = R |] ==> (P = R)";
   3.152 +val make_nnf_imp         = thm_by_auto "[| (~P) = P'; Q = Q' |] ==> (P --> Q) = (P' | Q')";
   3.153 +val make_nnf_iff         = thm_by_auto "[| P = P'; (~P) = NP; Q = Q'; (~Q) = NQ |] ==> (P = Q) = ((P' | NQ) & (NP | Q'))";
   3.154 +val make_nnf_not_false   = thm_by_auto "(~False) = True";
   3.155 +val make_nnf_not_true    = thm_by_auto "(~True) = False";
   3.156 +val make_nnf_not_conj    = thm_by_auto "[| (~P) = P'; (~Q) = Q' |] ==> (~(P & Q)) = (P' | Q')";
   3.157 +val make_nnf_not_disj    = thm_by_auto "[| (~P) = P'; (~Q) = Q' |] ==> (~(P | Q)) = (P' & Q')";
   3.158 +val make_nnf_not_imp     = thm_by_auto "[| P = P'; (~Q) = Q' |] ==> (~(P --> Q)) = (P' & Q')";
   3.159 +val make_nnf_not_iff     = thm_by_auto "[| P = P'; (~P) = NP; Q = Q'; (~Q) = NQ |] ==> (~(P = Q)) = ((P' | Q') & (NP | NQ))";
   3.160 +val make_nnf_not_not     = thm_by_auto "P = P' ==> (~~P) = P'";
   3.161  
   3.162 -val cnf_comb2eq = thm_by_auto "[| P = Q ; R = T |] ==> (P & R) = (Q & T)";
   3.163 -
   3.164 -val cnf_disj_sym = thm_by_auto "(P | Q) = (Q | P)";
   3.165 -
   3.166 -val cnf_cong_disj = thm_by_auto "(P = Q) ==> (P | R) = (Q | R)";
   3.167 -
   3.168 -val icnf_elim_disj1 = thm_by_auto "Q = R  ==> (~P | Q) = (P --> R)";
   3.169 +val simp_TF_conj_True_l  = thm_by_auto "[| P = True; Q = Q' |] ==> (P & Q) = Q'";
   3.170 +val simp_TF_conj_True_r  = thm_by_auto "[| P = P'; Q = True |] ==> (P & Q) = P'";
   3.171 +val simp_TF_conj_False_l = thm_by_auto "P = False ==> (P & Q) = False";
   3.172 +val simp_TF_conj_False_r = thm_by_auto "Q = False ==> (P & Q) = False";
   3.173 +val simp_TF_disj_True_l  = thm_by_auto "P = True ==> (P | Q) = True";
   3.174 +val simp_TF_disj_True_r  = thm_by_auto "Q = True ==> (P | Q) = True";
   3.175 +val simp_TF_disj_False_l = thm_by_auto "[| P = False; Q = Q' |] ==> (P | Q) = Q'";
   3.176 +val simp_TF_disj_False_r = thm_by_auto "[| P = P'; Q = False |] ==> (P | Q) = P'";
   3.177  
   3.178 -val icnf_elim_disj2 = thm_by_auto "Q = R ==> (P | Q) = (~P --> R)";
   3.179 -
   3.180 -val icnf_neg_false1 = thm_by_auto "(~P) = (P --> False)";
   3.181 +val make_cnf_disj_conj_l = thm_by_auto "[| (P | R) = PR; (Q | R) = QR |] ==> ((P & Q) | R) = (PR & QR)";
   3.182 +val make_cnf_disj_conj_r = thm_by_auto "[| (P | Q) = PQ; (P | R) = PR |] ==> (P | (Q & R)) = (PQ & PR)";
   3.183  
   3.184 -val icnf_neg_false2 = thm_by_auto "P = (~P --> False)";
   3.185 +val make_cnfx_disj_ex_l = thm_by_auto "((EX (x::bool). P x) | Q) = (EX x. P x | Q)";
   3.186 +val make_cnfx_disj_ex_r = thm_by_auto "(P | (EX (x::bool). Q x)) = (EX x. P | Q x)";
   3.187 +val make_cnfx_newlit    = thm_by_auto "(P | Q) = (EX x. (P | x) & (Q | ~x))";
   3.188 +val make_cnfx_ex_cong   = thm_by_auto "(ALL (x::bool). P x = Q x) ==> (EX x. P x) = (EX x. Q x)";
   3.189  
   3.190 -val weakening_thm = thm_by_auto "[| P ; Q |] ==> Q";
   3.191 +val weakening_thm        = thm_by_auto "[| P; Q |] ==> Q";
   3.192  
   3.193 -val cnf_newlit = thm_by_auto 
   3.194 -    "((P & Q) | R) = (EX (x :: bool). (~x | P) & (~x | Q) & (x | ~P | ~ Q) & (x | R))";
   3.195 +val cnftac_eq_imp        = thm_by_auto "[| P = Q; P |] ==> Q";
   3.196  
   3.197 -val cnf_all_ex = thm_by_auto 
   3.198 -    "(ALL (x :: bool). (P x = Q x)) ==> (EX x. P x) = (EX x. Q x)";
   3.199 -
   3.200 -(* [| P ; ~P |] ==> False *)
   3.201 -val cnf_notE = read_instantiate [("R", "False")] (rotate_prems 1 notE);
   3.202 -
   3.203 -val cnf_dneg = thm_by_auto "P ==> ~~P";
   3.204 -
   3.205 -val cnf_neg_disjI = thm_by_auto "[| ~P ; ~Q |] ==> ~(P | Q)";
   3.206 -
   3.207 -val cnf_eq_imp = thm_by_auto "[|((P::bool) = Q) ; P |] ==> Q";
   3.208 -
   3.209 -(***************************************************************************)
   3.210 +(* Term.term -> bool *)
   3.211 +fun is_atom (Const ("False", _))                                           = false
   3.212 +  | is_atom (Const ("True", _))                                            = false
   3.213 +  | is_atom (Const ("op &", _) $ _ $ _)                                    = false
   3.214 +  | is_atom (Const ("op |", _) $ _ $ _)                                    = false
   3.215 +  | is_atom (Const ("op -->", _) $ _ $ _)                                  = false
   3.216 +  | is_atom (Const ("op =", Type ("fun", Type ("bool", []) :: _)) $ _ $ _) = false
   3.217 +  | is_atom (Const ("Not", _) $ _)                                         = false
   3.218 +  | is_atom _                                                              = true;
   3.219  
   3.220 -fun is_atm (Const("Trueprop",_) $ x) = is_atm x
   3.221 -  | is_atm (Const("==>",_) $ x $ y) = false
   3.222 -  | is_atm (Const("False",_)) = false
   3.223 -  | is_atm (Const("True", _)) = false
   3.224 -  | is_atm (Const("op &",_) $ x $ y) = false
   3.225 -  | is_atm (Const("op |",_) $ x $ y) = false
   3.226 -  | is_atm (Const("op -->",_) $ x $ y) = false
   3.227 -  | is_atm (Const("Not",_) $ x) = false
   3.228 -  | is_atm t = true
   3.229 +(* Term.term -> bool *)
   3.230 +fun is_literal (Const ("Not", _) $ x) = is_atom x
   3.231 +  | is_literal x                      = is_atom x;
   3.232  
   3.233 -
   3.234 -fun is_lit (Const("Trueprop",_) $ x) = is_lit x
   3.235 -  | is_lit (Const("Not", _) $ x) = is_atm x
   3.236 -  | is_lit t = is_atm t
   3.237 +(* Term.term -> bool *)
   3.238 +fun is_clause (Const ("op |", _) $ x $ y) = is_clause x andalso is_clause y
   3.239 +  | is_clause x                           = is_literal x;
   3.240  
   3.241 -fun is_clause (Const("Trueprop",_) $ x) = is_clause x
   3.242 -  | is_clause (Const("op |", _) $ x $ y) = 
   3.243 -          (is_clause x) andalso (is_clause y)
   3.244 -  | is_clause t = is_lit t
   3.245 +(* ------------------------------------------------------------------------- *)
   3.246 +(* clause_is_trivial: a clause is trivially true if it contains both an atom *)
   3.247 +(*      and the atom's negation                                              *)
   3.248 +(* ------------------------------------------------------------------------- *)
   3.249 +
   3.250 +(* Term.term -> bool *)
   3.251  
   3.252 -fun is_cnf (Const("Trueprop", _) $ x) = is_cnf x
   3.253 -  | is_cnf (Const("op &",_) $ x $ y) = (is_cnf x) andalso (is_cnf y)
   3.254 -  | is_cnf t = is_clause t
   3.255 -
   3.256 -
   3.257 -(* Checking for raw clauses *)
   3.258 -fun is_raw_clause (Const("Trueprop",_) $ x) = is_raw_clause x
   3.259 -  | is_raw_clause (Const("==>",_) $ x $ 
   3.260 -                   (Const("Trueprop",_) $ Const("False",_))) = is_lit x
   3.261 -  | is_raw_clause (Const("==>",_) $ x $ y) = 
   3.262 -        (is_lit x) andalso (is_raw_clause y)
   3.263 -  | is_raw_clause t = false
   3.264 -
   3.265 -
   3.266 +fun clause_is_trivial c =
   3.267 +	let
   3.268 +		(* Term.term -> Term.term list -> Term.term list *)
   3.269 +		fun collect_literals (Const ("op |", _) $ x $ y) ls = collect_literals x (collect_literals y ls)
   3.270 +		  | collect_literals x                           ls = x :: ls
   3.271 +		(* Term.term -> Term.term *)
   3.272 +		fun dual (Const ("Not", _) $ x) = x
   3.273 +		  | dual x                      = HOLogic.Not $ x
   3.274 +		(* Term.term list -> bool *)
   3.275 +		fun has_duals []      = false
   3.276 +		  | has_duals (x::xs) = (dual x) mem xs orelse has_duals xs
   3.277 +	in
   3.278 +		has_duals (collect_literals c [])
   3.279 +	end;
   3.280  
   3.281 -(* Translate a CNF clause into a raw clause *)
   3.282 -fun cnf2raw_thm c =
   3.283 -let val nc = c RS cnf_notE
   3.284 -in
   3.285 -rule_by_tactic (REPEAT_SOME (fn i => 
   3.286 -               rtac cnf_dneg i 
   3.287 -               ORELSE rtac cnf_neg_disjI i)) nc
   3.288 -handle THM _ => nc
   3.289 -end
   3.290 +(* ------------------------------------------------------------------------- *)
   3.291 +(* is_raw_clause: returns true iff the term is of the form                   *)
   3.292 +(*        x1 ==> ... ==> xn ==> False ,                                      *)
   3.293 +(*      with n >= 1, where each xi is a literal                              *)
   3.294 +(* ------------------------------------------------------------------------- *)
   3.295 +
   3.296 +(* Term.term -> bool *)
   3.297  
   3.298 -fun cnf2raw_thms nil = nil
   3.299 -  | cnf2raw_thms (c::l) =
   3.300 -    let val t = term_of (cprop_of c)
   3.301 -    in
   3.302 -       if (is_clause t) then (cnf2raw_thm c) :: cnf2raw_thms l
   3.303 -       else cnf2raw_thms l
   3.304 -    end
   3.305 +fun is_raw_clause (Const ("==>", _) $ x $ y) =
   3.306 +	is_literal x andalso
   3.307 +		(y = HOLogic.mk_Trueprop HOLogic.false_const orelse is_raw_clause y)
   3.308 +  | is_raw_clause _                          =
   3.309 +	false;
   3.310  
   3.311 +(* ------------------------------------------------------------------------- *)
   3.312 +(* clause2raw_thm: translates a clause into a raw clause, i.e.               *)
   3.313 +(*        x1 | ... | xn                                                      *)
   3.314 +(*      (where each xi is a literal) is translated to                        *)
   3.315 +(*        x1' ==> ... ==> xn' ==> False ,                                    *)
   3.316 +(*      where each xi' is the negation normal form of ~xi.                   *)
   3.317 +(* ------------------------------------------------------------------------- *)
   3.318  
   3.319 -(* Translating HOL formula (in CNF) to PropLogic formula. Returns also an
   3.320 -   association list, relating literals to their indices *)
   3.321 +(* Thm.thm -> Thm.thm *)
   3.322  
   3.323 -local
   3.324 -  (* maps atomic formulas to variable numbers *)
   3.325 -  val dictionary : ((Term.term * int) list) ref = ref nil;
   3.326 -  val var_count = ref 0;
   3.327 -  val pAnd = PropLogic.And;
   3.328 -  val pOr = PropLogic.Or;
   3.329 -  val pNot = PropLogic.Not;
   3.330 -  val pFalse = PropLogic.False;
   3.331 -  val pTrue = PropLogic.True;
   3.332 -  val pVar = PropLogic.BoolVar;
   3.333 -
   3.334 -  fun mk_clause (Const("Trueprop",_) $ x) = mk_clause x
   3.335 -    | mk_clause (Const("op |",_) $ x $ y) = pOr(mk_clause x, mk_clause y)
   3.336 -    | mk_clause (Const("Not", _) $ x) = pNot (mk_clause x)
   3.337 -    | mk_clause (Const("True",_)) = pTrue
   3.338 -    | mk_clause (Const("False",_)) = pFalse
   3.339 -    | mk_clause t =
   3.340 -      let
   3.341 -         val idx = AList.lookup op= (!dictionary) t
   3.342 -      in
   3.343 -         case idx of
   3.344 -            (SOME x) => pVar x
   3.345 -           | NONE =>
   3.346 -             let
   3.347 -                val new_var = inc var_count
   3.348 -             in
   3.349 -                dictionary := (t, new_var) :: (!dictionary);
   3.350 -                pVar new_var
   3.351 -             end
   3.352 -      end
   3.353 -
   3.354 -   fun mk_clauses nil = pTrue
   3.355 -     | mk_clauses (x::nil) = mk_clause x
   3.356 -     | mk_clauses (x::l) = pAnd(mk_clause x, mk_clauses l)
   3.357 +fun clause2raw_thm c =
   3.358 +let
   3.359 +	val thm1 = c RS clause2raw_notE  (* ~(x1 | ... | xn) ==> False *)
   3.360 +	(* eliminates negated disjunctions from the i-th premise, possibly *)
   3.361 +	(* adding new premises, then continues with the (i+1)-th premise   *)
   3.362 +	(* Thm.thm -> int -> Thm.thm *)
   3.363 +	fun not_disj_to_prem thm i =
   3.364 +		if i > nprems_of thm then
   3.365 +			thm
   3.366 +		else
   3.367 +			not_disj_to_prem (Seq.hd (REPEAT_DETERM (rtac clause2raw_not_disj i) thm)) (i+1)
   3.368 +	val thm2 = not_disj_to_prem thm1 1  (* ~x1 ==> ... ==> ~xn ==> False *)
   3.369 +	val thm3 = Seq.hd (TRYALL (rtac clause2raw_not_not) thm2)  (* x1' ==> ... ==> xn' ==> False *)
   3.370 +in
   3.371 +	thm3
   3.372 +end;
   3.373  
   3.374 -in
   3.375 -   fun cnf2prop thms =
   3.376 -   (
   3.377 -     var_count := 0;
   3.378 -     dictionary := nil;
   3.379 -     (mk_clauses (map (fn x => term_of (cprop_of x)) thms), !dictionary)
   3.380 -   )
   3.381 -end
   3.382 +(* ------------------------------------------------------------------------- *)
   3.383 +(* inst_thm: instantiates a theorem with a list of terms                     *)
   3.384 +(* ------------------------------------------------------------------------- *)
   3.385  
   3.386 -
   3.387 +(* Theory.theory -> Term.term list -> Thm.thm -> Thm.thm *)
   3.388  
   3.389 -(* Instantiate a theorem with a list of terms *)
   3.390 -fun inst_thm sign l thm = 
   3.391 -  instantiate' [] (map (fn x => SOME (cterm_of sign x)) l) thm
   3.392 -
   3.393 -(* Tactic to remove the first hypothesis of the first subgoal. *) 
   3.394 -fun weakening_tac i = (dtac weakening_thm i) THEN (atac (i+1));
   3.395 +fun inst_thm thy ts thm =
   3.396 +	instantiate' [] (map (SOME o cterm_of thy) ts) thm;
   3.397  
   3.398 -(* Tactic for removing the n first hypotheses of the first subgoal. *)
   3.399 -fun weakenings_tac 0 state = all_tac state
   3.400 -  | weakenings_tac n state = ((weakening_tac  1) THEN (weakenings_tac (n-1))) state
   3.401 -
   3.402 +(* ------------------------------------------------------------------------- *)
   3.403 +(*                         Naive CNF transformation                          *)
   3.404 +(* ------------------------------------------------------------------------- *)
   3.405  
   3.406 -(* 
   3.407 -  Transform a formula into a "head" negation normal form, that is, 
   3.408 -  the top level connective is not a negation, with the exception
   3.409 -  of negative literals. Returns the pair of the head normal term with
   3.410 -  the theorem corresponding to the transformation.
   3.411 -*)
   3.412 -fun head_nnf sign (Const("Not",_)  $ (Const("op &",_) $ x $ y)) =
   3.413 -    let val t = mk_disj(Not $ x, Not $ y)
   3.414 -        val neg_thm = inst_thm sign [x, y] cnf_neg_conj 
   3.415 -    in
   3.416 -        (t, neg_thm)
   3.417 -    end
   3.418 +(* ------------------------------------------------------------------------- *)
   3.419 +(* make_nnf_thm: produces a theorem of the form t = t', where t' is the      *)
   3.420 +(*      negation normal form (i.e. negation only occurs in front of atoms)   *)
   3.421 +(*      of t; implications ("-->") and equivalences ("=" on bool) are        *)
   3.422 +(*      eliminated (possibly causing an exponential blowup)                  *)
   3.423 +(* ------------------------------------------------------------------------- *)
   3.424 +
   3.425 +(* Theory.theory -> Term.term -> Thm.thm *)
   3.426  
   3.427 -  | head_nnf sign (Const("Not", _) $ (Const("op |",_) $ x $ y)) =
   3.428 -    let val t = mk_conj(Not $ x, Not $ y)
   3.429 -        val neg_thm =  inst_thm sign [x, y] cnf_neg_disj; 
   3.430 -    in
   3.431 -        (t, neg_thm)
   3.432 -    end
   3.433 -
   3.434 -  | head_nnf sign (Const("Not", _) $ (Const("op -->",_) $ x $ y)) = 
   3.435 -    let val t = mk_conj(x, Not $ y)
   3.436 -        val neg_thm = inst_thm sign [x, y] cnf_neg_imp
   3.437 -    in
   3.438 -        (t, neg_thm)
   3.439 -    end
   3.440 -
   3.441 -  | head_nnf sign (Const("Not",_) $ (Const("Not",_) $ x)) =
   3.442 -    (x, inst_thm sign [x] cnf_double_neg)
   3.443 -
   3.444 -  | head_nnf sign (Const("Not",_) $ Const("True",_)) = 
   3.445 -      (false_const, cnf_not_true_false)
   3.446 -
   3.447 -  | head_nnf sign (Const("Not",_) $ Const("False",_)) = 
   3.448 -      (true_const, cnf_not_false_true)  
   3.449 -
   3.450 -  | head_nnf sign t = 
   3.451 -    (t, inst_thm sign [t] cnf_eq_id)
   3.452 -
   3.453 -
   3.454 -(***************************************************************************)
   3.455 -(*                  Tactics for simple CNF transformation                  *)
   3.456 +fun make_nnf_thm thy (Const ("op &", _) $ x $ y) =
   3.457 +	let
   3.458 +		val thm1 = make_nnf_thm thy x
   3.459 +		val thm2 = make_nnf_thm thy y
   3.460 +	in
   3.461 +		conj_cong OF [thm1, thm2]
   3.462 +	end
   3.463 +  | make_nnf_thm thy (Const ("op |", _) $ x $ y) =
   3.464 +	let
   3.465 +		val thm1 = make_nnf_thm thy x
   3.466 +		val thm2 = make_nnf_thm thy y
   3.467 +	in
   3.468 +		disj_cong OF [thm1, thm2]
   3.469 +	end
   3.470 +  | make_nnf_thm thy (Const ("op -->", _) $ x $ y) =
   3.471 +	let
   3.472 +		val thm1 = make_nnf_thm thy (HOLogic.Not $ x)
   3.473 +		val thm2 = make_nnf_thm thy y
   3.474 +	in
   3.475 +		make_nnf_imp OF [thm1, thm2]
   3.476 +	end
   3.477 +  | make_nnf_thm thy (Const ("op =", Type ("fun", Type ("bool", []) :: _)) $ x $ y) =
   3.478 +	let
   3.479 +		val thm1 = make_nnf_thm thy x
   3.480 +		val thm2 = make_nnf_thm thy (HOLogic.Not $ x)
   3.481 +		val thm3 = make_nnf_thm thy y
   3.482 +		val thm4 = make_nnf_thm thy (HOLogic.Not $ y)
   3.483 +	in
   3.484 +		make_nnf_iff OF [thm1, thm2, thm3, thm4]
   3.485 +	end
   3.486 +  | make_nnf_thm thy (Const ("Not", _) $ Const ("False", _)) =
   3.487 +	make_nnf_not_false
   3.488 +  | make_nnf_thm thy (Const ("Not", _) $ Const ("True", _)) =
   3.489 +	make_nnf_not_true
   3.490 +  | make_nnf_thm thy (Const ("Not", _) $ (Const ("op &", _) $ x $ y)) =
   3.491 +	let
   3.492 +		val thm1 = make_nnf_thm thy (HOLogic.Not $ x)
   3.493 +		val thm2 = make_nnf_thm thy (HOLogic.Not $ y)
   3.494 +	in
   3.495 +		make_nnf_not_conj OF [thm1, thm2]
   3.496 +	end
   3.497 +  | make_nnf_thm thy (Const ("Not", _) $ (Const ("op |", _) $ x $ y)) =
   3.498 +	let
   3.499 +		val thm1 = make_nnf_thm thy (HOLogic.Not $ x)
   3.500 +		val thm2 = make_nnf_thm thy (HOLogic.Not $ y)
   3.501 +	in
   3.502 +		make_nnf_not_disj OF [thm1, thm2]
   3.503 +	end
   3.504 +  | make_nnf_thm thy (Const ("Not", _) $ (Const ("op -->", _) $ x $ y)) =
   3.505 +	let
   3.506 +		val thm1 = make_nnf_thm thy x
   3.507 +		val thm2 = make_nnf_thm thy (HOLogic.Not $ y)
   3.508 +	in
   3.509 +		make_nnf_not_imp OF [thm1, thm2]
   3.510 +	end
   3.511 +  | make_nnf_thm thy (Const ("Not", _) $ (Const ("op =", Type ("fun", Type ("bool", []) :: _)) $ x $ y)) =
   3.512 +	let
   3.513 +		val thm1 = make_nnf_thm thy x
   3.514 +		val thm2 = make_nnf_thm thy (HOLogic.Not $ x)
   3.515 +		val thm3 = make_nnf_thm thy y
   3.516 +		val thm4 = make_nnf_thm thy (HOLogic.Not $ y)
   3.517 +	in
   3.518 +		make_nnf_not_iff OF [thm1, thm2, thm3, thm4]
   3.519 +	end
   3.520 +  | make_nnf_thm thy (Const ("Not", _) $ (Const ("Not", _) $ x)) =
   3.521 +	let
   3.522 +		val thm1 = make_nnf_thm thy x
   3.523 +	in
   3.524 +		make_nnf_not_not OF [thm1]
   3.525 +	end
   3.526 +  | make_nnf_thm thy t =
   3.527 +	inst_thm thy [t] iff_refl;
   3.528  
   3.529 -(* A naive procedure for CNF transformation:
   3.530 -   Given any t, produce a theorem t = t', where t' is in
   3.531 -   conjunction normal form 
   3.532 -*)
   3.533 -fun mk_cnf_thm sign (Const("Trueprop",_) $ x) = mk_cnf_thm sign x
   3.534 -  | mk_cnf_thm sign (t as (Const(_,_))) = inst_thm sign [t] cnf_eq_id
   3.535 -  | mk_cnf_thm sign (t as (Free(_,_))) =  inst_thm sign [t] cnf_eq_id
   3.536 - 
   3.537 -  | mk_cnf_thm sign (Const("op -->", _) $ x $ y) =
   3.538 -       let val thm1 = inst_thm sign [x, y] cnf_imp2disj;
   3.539 -           val thm2 = mk_cnf_thm sign (mk_disj(Not $ x, y));
   3.540 -       in
   3.541 -           cnf_eq_trans OF [thm1, thm2]
   3.542 -       end
   3.543 -
   3.544 -  | mk_cnf_thm sign (Const("op &", _) $ x $ y) = 
   3.545 -       let val cnf1 = mk_cnf_thm sign x;
   3.546 -           val cnf2 = mk_cnf_thm sign y;
   3.547 -       in
   3.548 -           cnf_comb2eq OF [cnf1, cnf2]
   3.549 -       end
   3.550 -
   3.551 -  | mk_cnf_thm sign (Const("Not",_) $ Const("True",_)) = 
   3.552 -        cnf_not_true_false
   3.553 +(* ------------------------------------------------------------------------- *)
   3.554 +(* simp_True_False_thm: produces a theorem t = t', where t' is equivalent to *)
   3.555 +(*      t, but simplified wrt. the following theorems:                       *)
   3.556 +(*        (True & x) = x                                                     *)
   3.557 +(*        (x & True) = x                                                     *)
   3.558 +(*        (False & x) = False                                                *)
   3.559 +(*        (x & False) = False                                                *)
   3.560 +(*        (True | x) = True                                                  *)
   3.561 +(*        (x | True) = True                                                  *)
   3.562 +(*        (False | x) = x                                                    *)
   3.563 +(*        (x | False) = x                                                    *)
   3.564 +(*      No simplification is performed below connectives other than & and |. *)
   3.565 +(*      Optimization: The right-hand side of a conjunction (disjunction) is  *)
   3.566 +(*      simplified only if the left-hand side does not simplify to False     *)
   3.567 +(*      (True, respectively).                                                *)
   3.568 +(* ------------------------------------------------------------------------- *)
   3.569  
   3.570 -  | mk_cnf_thm sign (Const("Not",_) $ Const("False",_)) = 
   3.571 -        cnf_not_false_true
   3.572 -
   3.573 -  | mk_cnf_thm sign (t as (Const("Not", _) $ x)) =
   3.574 -      ( 
   3.575 -       if (is_atm x) then inst_thm sign [t] cnf_eq_id
   3.576 -       else
   3.577 -         let val (t1, hn_thm) = head_nnf sign t
   3.578 -             val cnf_thm = mk_cnf_thm sign t1
   3.579 -         in
   3.580 -             cnf_eq_trans OF [hn_thm, cnf_thm]
   3.581 -         end
   3.582 -       ) 
   3.583 -
   3.584 -  | mk_cnf_thm sign (Const("op |",_) $ (Const("op &", _) $ p $ q) $ r) =
   3.585 -       let val thm1 = inst_thm sign [p, q, r] cnf_disj_conj;
   3.586 -           val thm2 = mk_cnf_thm sign (mk_conj(mk_disj(p, r), mk_disj(q,r)));
   3.587 -       in
   3.588 -          cnf_eq_trans OF [thm1, thm2]
   3.589 -       end
   3.590 -
   3.591 -  | mk_cnf_thm sign (Const("op |",_) $ (Const("op |", _) $ p $ q) $ r) =
   3.592 -       let val thm1 = inst_thm sign [p,q,r] cnf_disj_disj;
   3.593 -           val thm2 = mk_cnf_thm sign (mk_disj(p, mk_disj(q,r)));
   3.594 -       in
   3.595 -          cnf_eq_trans OF [thm1, thm2]
   3.596 -       end
   3.597 +(* Theory.theory -> Term.term -> Thm.thm *)
   3.598  
   3.599 -  | mk_cnf_thm sign (Const("op |",_) $ (Const("op -->", _) $ p $ q) $ r) =                       
   3.600 -       let val thm1 = inst_thm sign [p,q,r] cnf_disj_imp;
   3.601 -           val thm2 = mk_cnf_thm sign (mk_disj(Not $ p, mk_disj(q, r)));
   3.602 -       in
   3.603 -           cnf_eq_trans OF [thm1, thm2]
   3.604 -       end
   3.605 -
   3.606 -  | mk_cnf_thm sign (Const("op |",_) $ Const("False",_) $ p) =
   3.607 -       let val thm1 = inst_thm sign [p] cnf_disj_false;
   3.608 -           val thm2 = mk_cnf_thm sign p
   3.609 -       in
   3.610 -           cnf_eq_trans OF [thm1, thm2]
   3.611 -       end
   3.612 -
   3.613 -  | mk_cnf_thm sign (Const("op |",_) $ Const("True",_) $ p) =
   3.614 -       inst_thm sign [p] cnf_disj_true
   3.615 -
   3.616 -  | mk_cnf_thm sign (Const("op |",_) $ (Const("Not",_) $ Const("True",_)) $ p) =
   3.617 -       let val thm1 = inst_thm sign [p] cnf_disj_not_true;
   3.618 -           val thm2 = mk_cnf_thm sign p
   3.619 -       in
   3.620 -           cnf_eq_trans OF [thm1, thm2]
   3.621 -       end
   3.622 -
   3.623 -  | mk_cnf_thm sign (Const("op |",_) $ (Const("Not",_) $ Const("False",_)) $ p) =
   3.624 -       inst_thm sign [p] cnf_disj_not_false
   3.625 +fun simp_True_False_thm thy (Const ("op &", _) $ x $ y) =
   3.626 +	let
   3.627 +		val thm1 = simp_True_False_thm thy x
   3.628 +		val x'   = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1
   3.629 +	in
   3.630 +		if x' = HOLogic.false_const then
   3.631 +			simp_TF_conj_False_l OF [thm1]  (* (x & y) = False *)
   3.632 +		else
   3.633 +			let
   3.634 +				val thm2 = simp_True_False_thm thy y
   3.635 +				val y'   = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm2
   3.636 +			in
   3.637 +				if x' = HOLogic.true_const then
   3.638 +					simp_TF_conj_True_l OF [thm1, thm2]  (* (x & y) = y' *)
   3.639 +				else if y' = HOLogic.false_const then
   3.640 +					simp_TF_conj_False_r OF [thm2]  (* (x & y) = False *)
   3.641 +				else if y' = HOLogic.true_const then
   3.642 +					simp_TF_conj_True_r OF [thm1, thm2]  (* (x & y) = x' *)
   3.643 +				else
   3.644 +					conj_cong OF [thm1, thm2]  (* (x & y) = (x' & y') *)
   3.645 +			end
   3.646 +	end
   3.647 +  | simp_True_False_thm thy (Const ("op |", _) $ x $ y) =
   3.648 +	let
   3.649 +		val thm1 = simp_True_False_thm thy x
   3.650 +		val x'   = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1
   3.651 +	in
   3.652 +		if x' = HOLogic.true_const then
   3.653 +			simp_TF_disj_True_l OF [thm1]  (* (x | y) = True *)
   3.654 +		else
   3.655 +			let
   3.656 +				val thm2 = simp_True_False_thm thy y
   3.657 +				val y'   = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm2
   3.658 +			in
   3.659 +				if x' = HOLogic.false_const then
   3.660 +					simp_TF_disj_False_l OF [thm1, thm2]  (* (x | y) = y' *)
   3.661 +				else if y' = HOLogic.true_const then
   3.662 +					simp_TF_disj_True_r OF [thm2]  (* (x | y) = True *)
   3.663 +				else if y' = HOLogic.false_const then
   3.664 +					simp_TF_disj_False_r OF [thm1, thm2]  (* (x | y) = x' *)
   3.665 +				else
   3.666 +					disj_cong OF [thm1, thm2]  (* (x | y) = (x' | y') *)
   3.667 +			end
   3.668 +	end
   3.669 +  | simp_True_False_thm thy t =
   3.670 +	inst_thm thy [t] iff_refl;  (* t = t *)
   3.671  
   3.672 -  | mk_cnf_thm sign (t as (Const("op |",_) $ p $ q)) = 
   3.673 -       if (is_lit p) then
   3.674 -          (
   3.675 -            if (is_clause t) then inst_thm sign [t] cnf_eq_id
   3.676 -            else 
   3.677 -             let val thm1 = inst_thm sign [p, q] cnf_disj_sym;
   3.678 -                 val thm2 = mk_cnf_thm sign (mk_disj(q, p))
   3.679 -             in
   3.680 -                cnf_eq_trans OF [thm1, thm2]
   3.681 -             end
   3.682 -          )
   3.683 -       else 
   3.684 -            let val (u, thm1) = head_nnf sign p;
   3.685 -                val thm2 = inst_thm sign [p,u,q] cnf_cong_disj;
   3.686 -                val thm3 = mk_cnf_thm sign (mk_disj(u, q))
   3.687 -            in
   3.688 -                cnf_eq_trans OF [(thm1 RS thm2), thm3]
   3.689 -            end
   3.690 -
   3.691 - | mk_cnf_thm sign t = inst_thm sign [t] cnf_eq_id
   3.692 -    (* error ("I don't know how to handle the formula " ^ 
   3.693 -                          (Sign.string_of_term sign t))
   3.694 -    *)
   3.695 +(* ------------------------------------------------------------------------- *)
   3.696 +(* make_cnf_thm: given any HOL term 't', produces a theorem t = t', where t' *)
   3.697 +(*      is in conjunction normal form.  May cause an exponential blowup      *)
   3.698 +(*      in the length of the term.                                           *)
   3.699 +(* ------------------------------------------------------------------------- *)
   3.700  
   3.701 -fun term_of_thm c = term_of (cprop_of c)
   3.702 -
   3.703 -
   3.704 -(* Transform a given list of theorems (thms) into CNF *)
   3.705 -
   3.706 -fun mk_cnf_thms sg nil = nil
   3.707 -  | mk_cnf_thms sg (x::l) = 
   3.708 -    let val t = term_of_thm x
   3.709 -    in
   3.710 -      if (is_clause t) then x :: mk_cnf_thms sg l
   3.711 -      else 
   3.712 -       let val thm1 = mk_cnf_thm sg t
   3.713 -           val thm2 = cnf_eq_imp OF [thm1, x]
   3.714 -       in 
   3.715 -           thm2 :: mk_cnf_thms sg l
   3.716 -       end
   3.717 -    end
   3.718 -
   3.719 -
   3.720 -(* Count the number of hypotheses in a formula *)
   3.721 -fun num_of_hyps (Const("Trueprop", _) $ x) = num_of_hyps x
   3.722 -  | num_of_hyps (Const("==>",_) $ x $ y) = 1 + (num_of_hyps y)
   3.723 -  | num_of_hyps t = 0
   3.724 +(* Theory.theory -> Term.term -> Thm.thm *)
   3.725  
   3.726 -(* Tactic for converting to CNF (in primitive form): 
   3.727 -   it takes the first subgoal of the proof state, transform all its
   3.728 -   hypotheses into CNF (in primivite form) and remove the original 
   3.729 -   hypotheses.
   3.730 -*)
   3.731 -fun cnf_thin_tac state =
   3.732 -let val sg = Thm.sign_of_thm state
   3.733 +fun make_cnf_thm thy t =
   3.734 +let
   3.735 +	(* Term.term -> Thm.thm *)
   3.736 +	fun make_cnf_thm_from_nnf (Const ("op &", _) $ x $ y) =
   3.737 +		let
   3.738 +			val thm1 = make_cnf_thm_from_nnf x
   3.739 +			val thm2 = make_cnf_thm_from_nnf y
   3.740 +		in
   3.741 +			conj_cong OF [thm1, thm2]
   3.742 +		end
   3.743 +	  | make_cnf_thm_from_nnf (Const ("op |", _) $ x $ y) =
   3.744 +		let
   3.745 +			(* produces a theorem "(x' | y') = t'", where x', y', and t' are in CNF *)
   3.746 +			fun make_cnf_disj_thm (Const ("op &", _) $ x1 $ x2) y' =
   3.747 +				let
   3.748 +					val thm1 = make_cnf_disj_thm x1 y'
   3.749 +					val thm2 = make_cnf_disj_thm x2 y'
   3.750 +				in
   3.751 +					make_cnf_disj_conj_l OF [thm1, thm2]  (* ((x1 & x2) | y') = ((x1 | y')' & (x2 | y')') *)
   3.752 +				end
   3.753 +			  | make_cnf_disj_thm x' (Const ("op &", _) $ y1 $ y2) =
   3.754 +				let
   3.755 +					val thm1 = make_cnf_disj_thm x' y1
   3.756 +					val thm2 = make_cnf_disj_thm x' y2
   3.757 +				in
   3.758 +					make_cnf_disj_conj_r OF [thm1, thm2]  (* (x' | (y1 & y2)) = ((x' | y1)' & (x' | y2)') *)
   3.759 +				end
   3.760 +			  | make_cnf_disj_thm x' y' =
   3.761 +				inst_thm thy [HOLogic.mk_disj (x', y')] iff_refl  (* (x' | y') = (x' | y') *)
   3.762 +			val thm1     = make_cnf_thm_from_nnf x
   3.763 +			val thm2     = make_cnf_thm_from_nnf y
   3.764 +			val x'       = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1
   3.765 +			val y'       = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm2
   3.766 +			val disj_thm = disj_cong OF [thm1, thm2]  (* (x | y) = (x' | y') *)
   3.767 +		in
   3.768 +			iff_trans OF [disj_thm, make_cnf_disj_thm x' y']
   3.769 +		end
   3.770 +	  | make_cnf_thm_from_nnf t =
   3.771 +		inst_thm thy [t] iff_refl
   3.772 +	(* convert 't' to NNF first *)
   3.773 +	val nnf_thm  = make_nnf_thm thy t
   3.774 +	val nnf      = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) nnf_thm
   3.775 +	(* then simplify wrt. True/False (this should preserve NNF) *)
   3.776 +	val simp_thm = simp_True_False_thm thy nnf
   3.777 +	val simp     = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) simp_thm
   3.778 +	(* finally, convert to CNF (this should preserve the simplification) *)
   3.779 +	val cnf_thm  = make_cnf_thm_from_nnf simp
   3.780  in
   3.781 -case (prems_of state) of 
   3.782 -  [] => Seq.empty
   3.783 -| (subgoal::_) => 
   3.784 -  let 
   3.785 -    val n = num_of_hyps (strip_all_body subgoal);
   3.786 -    val tac1 = METAHYPS (fn l => cut_facts_tac (mk_cnf_thms sg l) 1) 1
   3.787 -  in
   3.788 -    (tac1 THEN weakenings_tac n THEN (REPEAT (etac conjE 1)) ) state
   3.789 -  end
   3.790 -end
   3.791 -
   3.792 -(* Tactic for converting to CNF (in primitive form), keeping 
   3.793 -   the original hypotheses. *)
   3.794 -
   3.795 -fun cnf_tac state =
   3.796 -let val sg = Thm.sign_of_thm state
   3.797 -in
   3.798 -case (prems_of state) of 
   3.799 -  [] => Seq.empty
   3.800 -| (subgoal::_) => 
   3.801 -   METAHYPS (fn l => cut_facts_tac (mk_cnf_thms sg l) 1 
   3.802 -                    THEN (REPEAT (etac conjE 1)) ) 1 state
   3.803 -end
   3.804 -
   3.805 -
   3.806 -(***************************************************************************)
   3.807 -(*            CNF transformation by introducing new literals               *)
   3.808 +	iff_trans OF [iff_trans OF [nnf_thm, simp_thm], cnf_thm]
   3.809 +end;
   3.810  
   3.811 -(*** IMPORTANT: 
   3.812 -  This transformation uses variables of the form "lit_i", where i is a natural
   3.813 -  number. For the transformation to work, these variables must not already
   3.814 -  occur freely in the formula being transformed.
   3.815 -***)
   3.816 -
   3.817 -fun ext_conj x p q r =
   3.818 -   mk_conj(
   3.819 -    mk_disj(Not $ x, p),
   3.820 -    mk_conj(
   3.821 -      mk_disj(Not $ x, q),
   3.822 -      mk_conj(
   3.823 -        mk_disj(x, mk_disj(Not $ p, Not $ q)),
   3.824 -        mk_disj(x, r)
   3.825 -      )
   3.826 -    )
   3.827 -   )
   3.828 -
   3.829 +(* ------------------------------------------------------------------------- *)
   3.830 +(*            CNF transformation by introducing new literals                 *)
   3.831 +(* ------------------------------------------------------------------------- *)
   3.832  
   3.833 -(* Transform to CNF in primitive forms, possibly introduce extra variables *)
   3.834 -fun mk_cnfx_thm sign (Const("Trueprop",_) $ x) = mk_cnfx_thm sign x 
   3.835 -  | mk_cnfx_thm sign (t as (Const(_,_)))  = inst_thm sign [t] cnf_eq_id
   3.836 -  | mk_cnfx_thm sign (t as (Free(_,_)))  = inst_thm sign [t] cnf_eq_id
   3.837 -  | mk_cnfx_thm sign (Const("op -->", _) $ x $ y)  =
   3.838 -       let val thm1 = inst_thm sign [x, y] cnf_imp2disj;
   3.839 -           val thm2 = mk_cnfx_thm sign (mk_disj(Not $ x, y)) 
   3.840 -       in
   3.841 -           cnf_eq_trans OF [thm1, thm2]
   3.842 -       end
   3.843 +(* ------------------------------------------------------------------------- *)
   3.844 +(* make_cnfx_thm: given any HOL term 't', produces a theorem t = t', where   *)
   3.845 +(*      t' is almost in conjunction normal form, except that conjunctions    *)
   3.846 +(*      and existential quantifiers may be nested.  (Use e.g. 'REPEAT_DETERM *)
   3.847 +(*      (etac exE i ORELSE etac conjE i)' afterwards to normalize.)  May     *)
   3.848 +(*      introduce new (existentially bound) literals.  Note: the current     *)
   3.849 +(*      implementation calls 'make_nnf_thm', causing an exponential blowup   *)
   3.850 +(*      in the case of nested equivalences.                                  *)
   3.851 +(* ------------------------------------------------------------------------- *)
   3.852  
   3.853 -  | mk_cnfx_thm sign (Const("op &", _) $ x $ y)  = 
   3.854 -       let val cnf1 = mk_cnfx_thm sign x
   3.855 -           val cnf2 = mk_cnfx_thm sign y
   3.856 -       in
   3.857 -           cnf_comb2eq OF [cnf1, cnf2]
   3.858 -       end
   3.859 -
   3.860 -  | mk_cnfx_thm sign (Const("Not",_) $ Const("True",_)) = 
   3.861 -        cnf_not_true_false
   3.862 +(* Theory.theory -> Term.term -> Thm.thm *)
   3.863  
   3.864 -  | mk_cnfx_thm sign (Const("Not",_) $ Const("False",_))  = 
   3.865 -        cnf_not_false_true
   3.866 -
   3.867 -  | mk_cnfx_thm sign (t as (Const("Not", _) $ x))  =
   3.868 -      ( 
   3.869 -       if (is_atm x) then inst_thm sign [t] cnf_eq_id
   3.870 -       else
   3.871 -         let val (t1, hn_thm) = head_nnf sign t
   3.872 -             val cnf_thm = mk_cnfx_thm sign t1 
   3.873 -         in
   3.874 -             cnf_eq_trans OF [hn_thm, cnf_thm]
   3.875 -         end
   3.876 -       ) 
   3.877 -
   3.878 -  | mk_cnfx_thm sign (Const("op |",_) $ (Const("op &", _) $ p $ q) $ r)  =
   3.879 -      if (is_lit r) then
   3.880 -        let val thm1 = inst_thm sign [p, q, r] cnf_disj_conj
   3.881 -            val thm2 = mk_cnfx_thm sign (mk_conj(mk_disj(p, r), mk_disj(q,r)))
   3.882 -        in
   3.883 -           cnf_eq_trans OF [thm1, thm2]
   3.884 -        end
   3.885 -      else cnfx_newlit sign p q r 
   3.886 -
   3.887 -  | mk_cnfx_thm sign (Const("op |",_) $ (Const("op |", _) $ p $ q) $ r)  =
   3.888 -       let val thm1 = inst_thm sign [p,q,r] cnf_disj_disj
   3.889 -           val thm2 = mk_cnfx_thm sign (mk_disj(p, mk_disj(q,r))) 
   3.890 -       in
   3.891 -          cnf_eq_trans OF [thm1, thm2]
   3.892 -       end
   3.893 -
   3.894 -  | mk_cnfx_thm sign (Const("op |",_) $ (Const("op -->", _) $ p $ q) $ r) =                       
   3.895 -       let val thm1 = inst_thm sign [p,q,r] cnf_disj_imp
   3.896 -           val thm2 = mk_cnfx_thm sign (mk_disj(Not $ p, mk_disj(q, r))) 
   3.897 -       in
   3.898 -           cnf_eq_trans OF [thm1, thm2]
   3.899 -       end
   3.900 -
   3.901 -  | mk_cnfx_thm sign (Const("op |",_) $ Const("False",_) $ p)  =
   3.902 -       let val thm1 = inst_thm sign [p] cnf_disj_false;
   3.903 -           val thm2 = mk_cnfx_thm sign p 
   3.904 -       in
   3.905 -           cnf_eq_trans OF [thm1, thm2]
   3.906 -       end
   3.907 -
   3.908 -  | mk_cnfx_thm sign (Const("op |",_) $ Const("True",_) $ p)  =
   3.909 -       inst_thm sign [p] cnf_disj_true
   3.910 -
   3.911 -  | mk_cnfx_thm sign (Const("op |",_) $ (Const("Not",_) $ Const("True",_)) $ p)  =
   3.912 -       let val thm1 = inst_thm sign [p] cnf_disj_not_true;
   3.913 -           val thm2 = mk_cnfx_thm sign p 
   3.914 -       in
   3.915 -           cnf_eq_trans OF [thm1, thm2]
   3.916 -       end
   3.917 -
   3.918 -  | mk_cnfx_thm sign (Const("op |",_) $ (Const("Not",_) $ Const("False",_)) $ p)  =
   3.919 -       inst_thm sign [p] cnf_disj_not_false
   3.920 -
   3.921 -  | mk_cnfx_thm sign (t as (Const("op |",_) $ p $ q))  = 
   3.922 -       if (is_lit p) then
   3.923 -          (
   3.924 -            if (is_clause t) then inst_thm sign [t] cnf_eq_id
   3.925 -            else 
   3.926 -             let val thm1 = inst_thm sign [p, q] cnf_disj_sym
   3.927 -                 val thm2 = mk_cnfx_thm sign (mk_disj(q, p)) 
   3.928 -             in
   3.929 -                cnf_eq_trans OF [thm1, thm2]
   3.930 -             end
   3.931 -          )
   3.932 -       else 
   3.933 -            let val (u, thm1) = head_nnf sign p
   3.934 -                val thm2 = inst_thm sign [p,u,q] cnf_cong_disj
   3.935 -                val thm3 = mk_cnfx_thm sign (mk_disj(u, q)) 
   3.936 -            in
   3.937 -                cnf_eq_trans OF [(thm1 RS thm2), thm3]
   3.938 -            end
   3.939 +fun make_cnfx_thm thy t =
   3.940 +let
   3.941 +	val var_id = ref 0  (* properly initialized below *)
   3.942 +	(* unit -> Term.term *)
   3.943 +	fun new_free () =
   3.944 +		Free ("cnfx_" ^ string_of_int (inc var_id), HOLogic.boolT)
   3.945 +	(* Term.term -> Thm.thm *)
   3.946 +	fun make_cnfx_thm_from_nnf (Const ("op &", _) $ x $ y) =
   3.947 +		let
   3.948 +			val thm1 = make_cnfx_thm_from_nnf x
   3.949 +			val thm2 = make_cnfx_thm_from_nnf y
   3.950 +		in
   3.951 +			conj_cong OF [thm1, thm2]
   3.952 +		end
   3.953 +	  | make_cnfx_thm_from_nnf (Const ("op |", _) $ x $ y) =
   3.954 +		if is_clause x andalso is_clause y then
   3.955 +			inst_thm thy [HOLogic.mk_disj (x, y)] iff_refl
   3.956 +		else if is_literal y orelse is_literal x then let
   3.957 +			(* produces a theorem "(x' | y') = t'", where x', y', and t' are *)
   3.958 +			(* almost in CNF, and x' or y' is a literal                      *)
   3.959 +			fun make_cnfx_disj_thm (Const ("op &", _) $ x1 $ x2) y' =
   3.960 +				let
   3.961 +					val thm1 = make_cnfx_disj_thm x1 y'
   3.962 +					val thm2 = make_cnfx_disj_thm x2 y'
   3.963 +				in
   3.964 +					make_cnf_disj_conj_l OF [thm1, thm2]  (* ((x1 & x2) | y') = ((x1 | y')' & (x2 | y')') *)
   3.965 +				end
   3.966 +			  | make_cnfx_disj_thm x' (Const ("op &", _) $ y1 $ y2) =
   3.967 +				let
   3.968 +					val thm1 = make_cnfx_disj_thm x' y1
   3.969 +					val thm2 = make_cnfx_disj_thm x' y2
   3.970 +				in
   3.971 +					make_cnf_disj_conj_r OF [thm1, thm2]  (* (x' | (y1 & y2)) = ((x' | y1)' & (x' | y2)') *)
   3.972 +				end
   3.973 +			  | make_cnfx_disj_thm (Const ("Ex", _) $ x') y' =
   3.974 +				let
   3.975 +					val thm1 = inst_thm thy [x', y'] make_cnfx_disj_ex_l   (* ((Ex x') | y') = (Ex (x' | y')) *)
   3.976 +					val var  = new_free ()
   3.977 +					val thm2 = make_cnfx_disj_thm (betapply (x', var)) y'  (* (x' | y') = body' *)
   3.978 +					val thm3 = forall_intr (cterm_of thy var) thm2         (* !!v. (x' | y') = body' *)
   3.979 +					val thm4 = strip_shyps (thm3 COMP allI)                (* ALL v. (x' | y') = body' *)
   3.980 +					val thm5 = strip_shyps (thm4 RS make_cnfx_ex_cong)     (* (EX v. (x' | y')) = (EX v. body') *)
   3.981 +				in
   3.982 +					iff_trans OF [thm1, thm5]  (* ((Ex x') | y') = (Ex v. body') *)
   3.983 +				end
   3.984 +			  | make_cnfx_disj_thm x' (Const ("Ex", _) $ y') =
   3.985 +				let
   3.986 +					val thm1 = inst_thm thy [x', y'] make_cnfx_disj_ex_r   (* (x' | (Ex y')) = (Ex (x' | y')) *)
   3.987 +					val var  = new_free ()
   3.988 +					val thm2 = make_cnfx_disj_thm x' (betapply (y', var))  (* (x' | y') = body' *)
   3.989 +					val thm3 = forall_intr (cterm_of thy var) thm2         (* !!v. (x' | y') = body' *)
   3.990 +					val thm4 = strip_shyps (thm3 COMP allI)                (* ALL v. (x' | y') = body' *)
   3.991 +					val thm5 = strip_shyps (thm4 RS make_cnfx_ex_cong)     (* (EX v. (x' | y')) = (EX v. body') *)
   3.992 +				in
   3.993 +					iff_trans OF [thm1, thm5]  (* (x' | (Ex y')) = (EX v. body') *)
   3.994 +				end
   3.995 +			  | make_cnfx_disj_thm x' y' =
   3.996 +				inst_thm thy [HOLogic.mk_disj (x', y')] iff_refl  (* (x' | y') = (x' | y') *)
   3.997 +			val thm1     = make_cnfx_thm_from_nnf x
   3.998 +			val thm2     = make_cnfx_thm_from_nnf y
   3.999 +			val x'       = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1
  3.1000 +			val y'       = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm2
  3.1001 +			val disj_thm = disj_cong OF [thm1, thm2]  (* (x | y) = (x' | y') *)
  3.1002 +		in
  3.1003 +			iff_trans OF [disj_thm, make_cnfx_disj_thm x' y']
  3.1004 +		end else let  (* neither 'x' nor 'y' is a literal: introduce a fresh variable *)
  3.1005 +			val thm1 = inst_thm thy [x, y] make_cnfx_newlit     (* (x | y) = EX v. (x | v) & (y | ~v) *)
  3.1006 +			val var  = new_free ()
  3.1007 +			val body = HOLogic.mk_conj (HOLogic.mk_disj (x, var), HOLogic.mk_disj (y, HOLogic.Not $ var))
  3.1008 +			val thm2 = make_cnfx_thm_from_nnf body              (* (x | v) & (y | ~v) = body' *)
  3.1009 +			val thm3 = forall_intr (cterm_of thy var) thm2      (* !!v. (x | v) & (y | ~v) = body' *)
  3.1010 +			val thm4 = strip_shyps (thm3 COMP allI)             (* ALL v. (x | v) & (y | ~v) = body' *)
  3.1011 +			val thm5 = strip_shyps (thm4 RS make_cnfx_ex_cong)  (* (EX v. (x | v) & (y | ~v)) = (EX v. body') *)
  3.1012 +		in
  3.1013 +			iff_trans OF [thm1, thm5]
  3.1014 +		end
  3.1015 +	  | make_cnfx_thm_from_nnf t =
  3.1016 +		inst_thm thy [t] iff_refl
  3.1017 +	(* convert 't' to NNF first *)
  3.1018 +	val nnf_thm  = make_nnf_thm thy t
  3.1019 +	val nnf      = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) nnf_thm
  3.1020 +	(* then simplify wrt. True/False (this should preserve NNF) *)
  3.1021 +	val simp_thm = simp_True_False_thm thy nnf
  3.1022 +	val simp     = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) simp_thm
  3.1023 +	(* initialize var_id, in case the term already contains variables of the form "cnfx_<int>" *)
  3.1024 +	val _        = (var_id := fold (fn free => fn max =>
  3.1025 +		let
  3.1026 +			val (name, _) = dest_Free free
  3.1027 +			val idx       = if String.isPrefix "cnfx_" name then
  3.1028 +					(Int.fromString o String.extract) (name, String.size "cnfx_", NONE)
  3.1029 +				else
  3.1030 +					NONE
  3.1031 +		in
  3.1032 +			Int.max (max, getOpt (idx, 0))
  3.1033 +		end) (term_frees simp) 0)
  3.1034 +	(* finally, convert to definitional CNF (this should preserve the simplification) *)
  3.1035 +	val cnfx_thm = make_cnfx_thm_from_nnf simp
  3.1036 +in
  3.1037 +	iff_trans OF [iff_trans OF [nnf_thm, simp_thm], cnfx_thm]
  3.1038 +end;
  3.1039  
  3.1040 - | mk_cnfx_thm sign t  = error ("I don't know how to handle the formula " ^ 
  3.1041 -                          (Sign.string_of_term sign t))
  3.1042 +(* ------------------------------------------------------------------------- *)
  3.1043 +(*                                  Tactics                                  *)
  3.1044 +(* ------------------------------------------------------------------------- *)
  3.1045  
  3.1046 -and cnfx_newlit sign p q r  = 
  3.1047 -   let val lit = read ("lit_" ^ (Int.toString (!lit_id)) ^ " :: bool")
  3.1048 -       val _ = (lit_id := !lit_id + 1)
  3.1049 -       val ct_lit = cterm_of sign lit
  3.1050 -       val x_conj = ext_conj lit p q r
  3.1051 -       val thm1 = inst_thm sign [p,q,r] cnf_newlit
  3.1052 -       val thm2 = mk_cnfx_thm sign x_conj 
  3.1053 -       val thm3 = forall_intr ct_lit thm2
  3.1054 -       val thm4 = strip_shyps (thm3 COMP allI)
  3.1055 -       val thm5 = strip_shyps (thm4 RS cnf_all_ex)
  3.1056 -   in
  3.1057 -       cnf_eq_trans OF [thm1, thm5]
  3.1058 -   end
  3.1059 +(* ------------------------------------------------------------------------- *)
  3.1060 +(* weakening_tac: removes the first hypothesis of the 'i'-th subgoal         *)
  3.1061 +(* ------------------------------------------------------------------------- *)
  3.1062  
  3.1063 +(* int -> Tactical.tactic *)
  3.1064  
  3.1065 -(* Theorems for converting formula into CNF (in primitive form), with 
  3.1066 -   new extra variables *)
  3.1067 -
  3.1068 +fun weakening_tac i =
  3.1069 +	dtac weakening_thm i THEN atac (i+1);
  3.1070  
  3.1071 -fun mk_cnfx_thms sg nil = nil
  3.1072 -  | mk_cnfx_thms sg (x::l) = 
  3.1073 -    let val t = term_of_thm x
  3.1074 -    in
  3.1075 -      if (is_clause t) then x :: mk_cnfx_thms sg l
  3.1076 -      else 
  3.1077 -       let val thm1 = mk_cnfx_thm sg t
  3.1078 -           val thm2 = cnf_eq_imp OF [thm1,x]
  3.1079 -       in 
  3.1080 -           thm2 :: mk_cnfx_thms sg l
  3.1081 -       end
  3.1082 -    end
  3.1083 +(* ------------------------------------------------------------------------- *)
  3.1084 +(* cnf_rewrite_tac: converts all premises of the 'i'-th subgoal to CNF       *)
  3.1085 +(*      (possibly causing an exponential blowup in the length of each        *)
  3.1086 +(*      premise)                                                             *)
  3.1087 +(* ------------------------------------------------------------------------- *)
  3.1088  
  3.1089 +(* int -> Tactical.tactic *)
  3.1090  
  3.1091 -(* Tactic for converting hypotheses into CNF, possibly
  3.1092 -   introducing new variables *)
  3.1093 -
  3.1094 -fun cnfx_thin_tac state =
  3.1095 -let val sg = Thm.sign_of_thm state
  3.1096 -in
  3.1097 -case (prems_of state) of 
  3.1098 -  [] => Seq.empty
  3.1099 -| (subgoal::_) => 
  3.1100 -   let val n = num_of_hyps (strip_all_body subgoal);
  3.1101 -       val tac1 =  METAHYPS (fn l => cut_facts_tac (mk_cnfx_thms sg l) 1) 1
  3.1102 -   in
  3.1103 -      EVERY [tac1, weakenings_tac n, 
  3.1104 -             REPEAT (etac conjE 1 ORELSE etac exE 1)] state
  3.1105 -   end
  3.1106 -end
  3.1107 -
  3.1108 -(* Tactic for converting the conclusion of a goal into CNF *)
  3.1109 +fun cnf_rewrite_tac i =
  3.1110 +	(* cut the CNF formulas as new premises *)
  3.1111 +	METAHYPS (fn prems =>
  3.1112 +		let
  3.1113 +			val cnf_thms = map (fn pr => make_cnf_thm (theory_of_thm pr) ((HOLogic.dest_Trueprop o prop_of) pr)) prems
  3.1114 +			val cut_thms = map (fn (th, pr) => cnftac_eq_imp OF [th, pr]) (cnf_thms ~~ prems)
  3.1115 +		in
  3.1116 +			cut_facts_tac cut_thms 1
  3.1117 +		end) i
  3.1118 +	(* remove the original premises *)
  3.1119 +	THEN SELECT_GOAL (fn thm =>
  3.1120 +		let
  3.1121 +			val n = Logic.count_prems ((Term.strip_all_body o fst o Logic.dest_implies o prop_of) thm, 0)
  3.1122 +		in
  3.1123 +			PRIMITIVE (funpow (n div 2) (Seq.hd o weakening_tac 1)) thm
  3.1124 +		end) i;
  3.1125  
  3.1126 -fun get_concl (Const("Trueprop", _) $ x) = get_concl x
  3.1127 -  | get_concl (Const("==>",_) $ x $ y) = get_concl y
  3.1128 -  | get_concl t = t
  3.1129 +(* ------------------------------------------------------------------------- *)
  3.1130 +(* cnfx_rewrite_tac: converts all premises of the 'i'-th subgoal to CNF      *)
  3.1131 +(*      (possibly introducing new literals)                                  *)
  3.1132 +(* ------------------------------------------------------------------------- *)
  3.1133 +
  3.1134 +(* int -> Tactical.tactic *)
  3.1135  
  3.1136 -fun cnf_concl_tac' state =
  3.1137 -case (prems_of state) of 
  3.1138 -  [] => Seq.empty
  3.1139 -| (subgoal::_) =>
  3.1140 -  let val sg = Thm.sign_of_thm state
  3.1141 -      val c = get_concl subgoal
  3.1142 -      val thm1 = (mk_cnf_thm sg c) RS cnf_eq_sym
  3.1143 -      val thm2 = thm1 RS subst
  3.1144 -  in
  3.1145 -    rtac thm2 1 state
  3.1146 -  end
  3.1147 +fun cnfx_rewrite_tac i =
  3.1148 +	(* cut the CNF formulas as new premises *)
  3.1149 +	METAHYPS (fn prems =>
  3.1150 +		let
  3.1151 +			val cnfx_thms = map (fn pr => make_cnfx_thm (theory_of_thm pr) ((HOLogic.dest_Trueprop o prop_of) pr)) prems
  3.1152 +			val cut_thms  = map (fn (th, pr) => cnftac_eq_imp OF [th, pr]) (cnfx_thms ~~ prems)
  3.1153 +		in
  3.1154 +			cut_facts_tac cut_thms 1
  3.1155 +		end) i
  3.1156 +	(* remove the original premises *)
  3.1157 +	THEN SELECT_GOAL (fn thm =>
  3.1158 +		let
  3.1159 +			val n = Logic.count_prems ((Term.strip_all_body o fst o Logic.dest_implies o prop_of) thm, 0)
  3.1160 +		in
  3.1161 +			PRIMITIVE (funpow (n div 2) (Seq.hd o weakening_tac 1)) thm
  3.1162 +		end) i;
  3.1163  
  3.1164 -val cnf_concl_tac  = METAHYPS (fn l => cnf_concl_tac') 1 
  3.1165 -
  3.1166 -
  3.1167 -end (*of structure*)
  3.1168 +end;  (* of structure *)
     4.1 --- a/src/HOL/Tools/prop_logic.ML	Sat Oct 08 23:43:15 2005 +0200
     4.2 +++ b/src/HOL/Tools/prop_logic.ML	Sun Oct 09 17:06:03 2005 +0200
     4.3 @@ -34,6 +34,9 @@
     4.4  	val defcnf : prop_formula -> prop_formula  (* definitional cnf *)
     4.5  
     4.6  	val eval : (int -> bool) -> prop_formula -> bool  (* semantics *)
     4.7 +
     4.8 +	val prop_formula_of_term : Term.term -> int Termtab.table -> prop_formula * int Termtab.table
     4.9 +		(* propositional representation of HOL terms *)
    4.10  end;
    4.11  
    4.12  structure PropLogic : PROP_LOGIC =
    4.13 @@ -421,4 +424,66 @@
    4.14  	  | eval a (Or (fm1,fm2))  = (eval a fm1) orelse (eval a fm2)
    4.15  	  | eval a (And (fm1,fm2)) = (eval a fm1) andalso (eval a fm2);
    4.16  
    4.17 +(* ------------------------------------------------------------------------- *)
    4.18 +(* prop_formula_of_term: returns the propositional structure of a HOL term,  *)
    4.19 +(*      with subterms replaced by Boolean variables.  Also returns a table   *)
    4.20 +(*      of terms and corresponding variables that extends the table that was *)
    4.21 +(*      given as an argument.  Usually, you'll just want to use              *)
    4.22 +(*      'Termtab.empty' as value for 'table'.                                *)
    4.23 +(* ------------------------------------------------------------------------- *)
    4.24 +
    4.25 +(* Note: The implementation is somewhat optimized; the next index to be used *)
    4.26 +(*       is computed only when it is actually needed.  However, when         *)
    4.27 +(*       'prop_formula_of_term' is invoked many times, it might be more      *)
    4.28 +(*       efficient to pass and return this value as an additional parameter, *)
    4.29 +(*       so that it does not have to be recomputed (by folding over the      *)
    4.30 +(*       table) for each invocation.                                         *)
    4.31 +
    4.32 +	(* Term.term -> int Termtab.table -> prop_formula * int Termtab.table *)
    4.33 +	fun prop_formula_of_term t table =
    4.34 +	let
    4.35 +		val next_idx_is_valid = ref false
    4.36 +		val next_idx          = ref 0
    4.37 +		fun get_next_idx () =
    4.38 +			if !next_idx_is_valid then
    4.39 +				inc next_idx
    4.40 +			else (
    4.41 +				next_idx          := Termtab.fold (curry Int.max o snd) table 0;
    4.42 +				next_idx_is_valid := true;
    4.43 +				inc next_idx
    4.44 +			)
    4.45 +		fun aux (Const ("True", _))         table =
    4.46 +			(True, table)
    4.47 +		  | aux (Const ("False", _))        table =
    4.48 +			(False, table)
    4.49 +		  | aux (Const ("Not", _) $ x)      table =
    4.50 +			apfst Not (aux x table)
    4.51 +		  | aux (Const ("op |", _) $ x $ y) table =
    4.52 +			let
    4.53 +				val (fm1, table1) = aux x table
    4.54 +				val (fm2, table2) = aux y table1
    4.55 +			in
    4.56 +				(Or (fm1, fm2), table2)
    4.57 +			end
    4.58 +		  | aux (Const ("op &", _) $ x $ y) table =
    4.59 +			let
    4.60 +				val (fm1, table1) = aux x table
    4.61 +				val (fm2, table2) = aux y table1
    4.62 +			in
    4.63 +				(And (fm1, fm2), table2)
    4.64 +			end
    4.65 +		  | aux x                           table =
    4.66 +			(case Termtab.lookup table x of
    4.67 +			  SOME i =>
    4.68 +				(BoolVar i, table)
    4.69 +			| NONE   =>
    4.70 +				let
    4.71 +					val i = get_next_idx ()
    4.72 +				in
    4.73 +					(BoolVar i, Termtab.update (x, i) table)
    4.74 +				end)
    4.75 +	in
    4.76 +		aux t table
    4.77 +	end;
    4.78 +
    4.79  end;
     5.1 --- a/src/HOL/Tools/sat_funcs.ML	Sat Oct 08 23:43:15 2005 +0200
     5.2 +++ b/src/HOL/Tools/sat_funcs.ML	Sun Oct 09 17:06:03 2005 +0200
     5.3 @@ -19,7 +19,7 @@
     5.4            [| l1; l2; ...; lm |] ==> False,
     5.5      where each li is a literal (see also comments in cnf_funcs.ML).
     5.6  
     5.7 -    -- observe that this is the "dualized" version of the standard
     5.8 +    -- Observe that this is the "dualized" version of the standard
     5.9         clausal form
    5.10             l1' \/ l2' \/ ... \/ lm', where li is the negation normal
    5.11         form of ~li'.
    5.12 @@ -53,8 +53,8 @@
    5.13  signature SAT =
    5.14  sig
    5.15  	val trace_sat : bool ref  (* print trace messages *)
    5.16 -	val sat_tac   : Tactical.tactic
    5.17 -	val satx_tac  : Tactical.tactic
    5.18 +	val sat_tac   : int -> Tactical.tactic
    5.19 +	val satx_tac  : int -> Tactical.tactic
    5.20  end
    5.21  
    5.22  functor SATFunc (structure cnf : CNF) : SAT =
    5.23 @@ -65,193 +65,190 @@
    5.24  val counter = ref 0;
    5.25  
    5.26  (* ------------------------------------------------------------------------- *)
    5.27 -(* rev_lookup: look up the Isabelle/HOL atom corresponding to a DIMACS       *)
    5.28 -(*      variable index in the dictionary.  This index should exist in the    *)
    5.29 -(*      dictionary, otherwise exception Option is raised.                    *)
    5.30 +(* swap_prem: convert raw clauses of the form                                *)
    5.31 +(*        [| l1; l2; ...; li; ... |] ==> False                               *)
    5.32 +(*      to                                                                   *)
    5.33 +(*        [| l1; l2; ... |] ==> ~li .                                        *)
    5.34 +(*      Note that ~li may be equal to ~~a for some atom a.                   *)
    5.35  (* ------------------------------------------------------------------------- *)
    5.36  
    5.37 -(* 'b -> ('a * 'b) list -> 'a *)
    5.38 -
    5.39 -fun rev_lookup idx []                   = raise Option
    5.40 -  | rev_lookup idx ((key, entry)::dict) = if entry=idx then key else rev_lookup idx dict;
    5.41 +(* Thm.thm -> int -> Thm.thm *)
    5.42  
    5.43 -(* ------------------------------------------------------------------------- *)
    5.44 -(* swap_prem: convert rules of the form                                      *)
    5.45 -(*       l1 ==> l2 ==> .. ==> li ==> .. ==> False                            *)
    5.46 -(*     to                                                                    *)
    5.47 -(*       l1 ==> l2 ==> .... ==> ~li                                          *)
    5.48 -(* ------------------------------------------------------------------------- *)
    5.49 -
    5.50 -fun swap_prem rslv c =
    5.51 -let
    5.52 -	val thm1 = rule_by_tactic (metacut_tac c 1 THEN (atac 1) THEN (REPEAT_SOME atac)) rslv
    5.53 -in
    5.54 -	rule_by_tactic (ALLGOALS (cnf.weakening_tac)) thm1
    5.55 -end;
    5.56 +fun swap_prem raw_cl i =
    5.57 +	Seq.hd ((metacut_tac raw_cl 1  (* [| [| ?P; False |] ==> False; ?P ==> l1; ...; ?P ==> li; ... |] ==> ~ ?P *)
    5.58 +		THEN atac (i+1)            (* [| [| li; False |] ==> False; li ==> l1; ... |] ==> ~ li *)
    5.59 +		THEN atac 1                (* [| li ==> l1; ... |] ==> ~ li *)
    5.60 +		THEN ALLGOALS cnf.weakening_tac) notI);
    5.61  
    5.62  (* ------------------------------------------------------------------------- *)
    5.63 -(* is_dual: check if two atoms are dual to each other                        *)
    5.64 -(* ------------------------------------------------------------------------- *)
    5.65 -
    5.66 -(* Term.term -> Term.term -> bool *)
    5.67 -
    5.68 -fun is_dual (Const ("Trueprop", _) $ x) y = is_dual x y
    5.69 -  | is_dual x (Const ("Trueprop", _) $ y) = is_dual x y
    5.70 -  | is_dual (Const ("Not", _) $ x) y      = (x = y)
    5.71 -  | is_dual x (Const ("Not", _) $ y)      = (x = y)
    5.72 -  | is_dual x y                           = false;
    5.73 -
    5.74 -(* ------------------------------------------------------------------------- *)
    5.75 -(* dual_mem: check if an atom has a dual in a list of atoms                  *)
    5.76 -(* ------------------------------------------------------------------------- *)
    5.77 -
    5.78 -(* Term.term -> Term.term list -> bool *)
    5.79 -
    5.80 -fun dual_mem x []      = false
    5.81 -  | dual_mem x (y::ys) = is_dual x y orelse dual_mem x ys;
    5.82 -
    5.83 -(* ------------------------------------------------------------------------- *)
    5.84 -(* replay_chain: proof reconstruction: given two clauses                     *)
    5.85 -(*        [| x1 ; .. ; a ; .. ; xn |] ==> False                              *)
    5.86 +(* resolve_raw_clauses: given a non-empty list of raw clauses, we fold       *)
    5.87 +(*      resolution over the list (starting with its head), i.e. with two raw *)
    5.88 +(*      clauses                                                              *)
    5.89 +(*        [| x1; ... ; a; ...; xn |] ==> False                               *)
    5.90  (*      and                                                                  *)
    5.91 -(*        [| y1 ; .. ; ~a ; .. ; ym |] ==> False ,                           *)
    5.92 -(*      we first convert the first clause into                               *)
    5.93 -(*        [| x1 ; ... ; xn |] ==> ~a     (using swap_prem)                   *)
    5.94 -(*      and do a resolution with the second clause to produce                *)
    5.95 -(*        [| y1 ; ... ; x1 ; ... ; xn ; ... ; yn |] ==> False                *)
    5.96 +(*        [| y1; ... ; a'; ...; ym |] ==> False                              *)
    5.97 +(*      (where a and a' are dual to each other), we first convert the first  *)
    5.98 +(*      clause to                                                            *)
    5.99 +(*        [| x1; ...; xn |] ==> a'                                           *)
   5.100 +(*      (using swap_prem and perhaps notnotD), and then do a resolution with *)
   5.101 +(*      the second clause to produce                                         *)
   5.102 +(*        [| y1; ...; x1; ...; xn; ...; yn |] ==> False                      *)
   5.103 +(*      amd finally remove duplicate literals.                               *)
   5.104  (* ------------------------------------------------------------------------- *)
   5.105  
   5.106 -(* Theory.theory -> Thm.thm option Array.array -> int -> int list -> unit *)
   5.107 +(* Thm.thm list -> Thm.thm *)
   5.108  
   5.109 -fun replay_chain sg clauses idx (c::cs) =
   5.110 -let
   5.111 -	val fc = (valOf o Array.sub) (clauses, c)
   5.112 +fun resolve_raw_clauses [] =
   5.113 +	raise THM ("Proof reconstruction failed (empty list of resolvents)!", 0, [])
   5.114 +  | resolve_raw_clauses (c::cs) =
   5.115 +	let
   5.116 +		fun dual (Const ("Not", _) $ x) = x
   5.117 +		  | dual x                      = HOLogic.Not $ x
   5.118 +
   5.119 +		fun is_neg (Const ("Not", _) $ _) = true
   5.120 +		  | is_neg _                      = false
   5.121  
   5.122 -	fun strip_neg (Const ("Trueprop", _) $ x) = strip_neg x
   5.123 -	  | strip_neg (Const ("Not", _) $ x)      = x
   5.124 -	  | strip_neg x                           = x
   5.125 +		(* find out which premises are used in the resolution *)
   5.126 +		(* Term.term list -> Term.term list -> int -> (int * int * bool) *)
   5.127 +		fun res_prems []      _  _    =
   5.128 +			raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, [])
   5.129 +		  | res_prems (x::xs) ys idx1 =
   5.130 +			let
   5.131 +				val x'   = HOLogic.dest_Trueprop x
   5.132 +				val idx2 = find_index_eq (dual x') ys
   5.133 +			in
   5.134 +				if idx2 = (~1) then
   5.135 +					res_prems xs ys (idx1+1)
   5.136 +				else
   5.137 +					(idx1, idx2, is_neg x')
   5.138 +			end
   5.139  
   5.140 -	(* find out which atom (literal) is used in the resolution *)
   5.141 -	fun res_atom []      _  = raise THM ("Proof reconstruction failed!", 0, [])
   5.142 -	  | res_atom (x::xs) ys = if dual_mem x ys then strip_neg x else res_atom xs ys
   5.143 -
   5.144 -	fun replay old []        =
   5.145 -		old
   5.146 -	  | replay old (cl::cls) =
   5.147 +		(* Thm.thm -> Thm.thm -> Thm.thm *)
   5.148 +		fun resolution c1 c2 =
   5.149  		let
   5.150 -			val icl  = (valOf o Array.sub) (clauses, cl)
   5.151 -			val var  = res_atom (prems_of old) (prems_of icl)
   5.152 -			val atom = cterm_of sg var
   5.153 -			val rslv = instantiate' [] [SOME atom] notI
   5.154  			val _ = if !trace_sat then
   5.155 -					tracing ("Resolving clause: " ^ string_of_thm old ^
   5.156 -						"\nwith clause: " ^ string_of_thm icl ^
   5.157 -						"\nusing literal " ^ string_of_cterm atom ^ ".")
   5.158 +					tracing ("Resolving clause: " ^ string_of_thm c1 ^ "\nwith clause: " ^ string_of_thm c2)
   5.159  				else ()
   5.160 -			val thm1 = (rule_by_tactic (REPEAT_SOME (rtac (swap_prem rslv old))) icl
   5.161 -				handle THM _ => rule_by_tactic (REPEAT_SOME (rtac (swap_prem rslv icl))) old)
   5.162 -			val new  = rule_by_tactic distinct_subgoals_tac thm1
   5.163 -			val _    = if !trace_sat then tracing ("Resulting clause: " ^ string_of_thm new) else ()
   5.164 -			val _    = inc counter
   5.165 -		in
   5.166 -			replay new cls
   5.167 -		end
   5.168 +
   5.169 +			val prems2                   = map HOLogic.dest_Trueprop (prems_of c2)
   5.170 +			val (idx1, idx2, is_neg_lit) = res_prems (prems_of c1) prems2 0
   5.171 +			val swap_c1                  = swap_prem c1 (idx1+1)
   5.172 +			val swap_c1_nnf              = if is_neg_lit then Seq.hd (rtac swap_c1 1 notnotD) else swap_c1  (* deal with double-negation *)
   5.173 +			val c_new                    = Seq.hd ((rtac swap_c1_nnf (idx2+1) THEN distinct_subgoals_tac) c2)
   5.174  
   5.175 -	val _ = Array.update (clauses, idx, SOME (replay fc cs))
   5.176 -
   5.177 -	val _ = if !trace_sat then
   5.178 -			tracing ("Replay chain successful; clause stored at #" ^ string_of_int idx)
   5.179 -		else ()
   5.180 -in
   5.181 -	()
   5.182 -end;
   5.183 +			val _ = if !trace_sat then tracing ("Resulting clause: " ^ string_of_thm c_new) else ()
   5.184 +			val _ = inc counter
   5.185 +		in
   5.186 +			c_new
   5.187 +		end
   5.188 +	in
   5.189 +		fold resolution cs c
   5.190 +	end;
   5.191  
   5.192  (* ------------------------------------------------------------------------- *)
   5.193 -(* replay_proof: replay the resolution proof returned by the SAT solver; cf. *)
   5.194 -(*      SatSolver.proof for details of the proof format.  Returns the        *)
   5.195 -(*      theorem established by the proof (which is just False).              *)
   5.196 +(* replay_proof: replays the resolution proof returned by the SAT solver;    *)
   5.197 +(*      cf. SatSolver.proof for details of the proof format.  Updates the    *)
   5.198 +(*      'clauses' array with derived clauses, and returns the derived clause *)
   5.199 +(*      at index 'empty_id' (which should just be "False" if proof           *)
   5.200 +(*      reconstruction was successful, with the used clauses as hyps).       *)
   5.201  (* ------------------------------------------------------------------------- *)
   5.202  
   5.203 -(* Theory.theory -> Thm.thm option Array.array -> SatSolver.proof -> Thm.thm *)
   5.204 +(* Thm.thm option Array.array -> SatSolver.proof -> Thm.thm *)
   5.205  
   5.206 -fun replay_proof sg clauses (clause_table, empty_id) =
   5.207 +fun replay_proof clauses (clause_table, empty_id) =
   5.208  let
   5.209 -	(* int -> unit *)
   5.210 +	(* int -> Thm.thm *)
   5.211  	fun prove_clause id =
   5.212  		case Array.sub (clauses, id) of
   5.213 -		  SOME _ =>
   5.214 -			()
   5.215 -		| NONE   =>
   5.216 +		  SOME thm =>
   5.217 +			thm
   5.218 +		| NONE     =>
   5.219  			let
   5.220 +				val _   = if !trace_sat then tracing ("Proving clause #" ^ string_of_int id ^ " ...") else ()
   5.221  				val ids = valOf (Inttab.lookup clause_table id)
   5.222 -				val _   = map prove_clause ids
   5.223 +				val thm = resolve_raw_clauses (map prove_clause ids)
   5.224 +				val _   = Array.update (clauses, id, SOME thm)
   5.225 +				val _   = if !trace_sat then tracing ("Replay chain successful; clause stored at #" ^ string_of_int id) else ()
   5.226  			in
   5.227 -				replay_chain sg clauses id ids
   5.228 +				thm
   5.229  			end
   5.230  
   5.231 -	val _ = counter := 0
   5.232 -
   5.233 -	val _ = prove_clause empty_id
   5.234 -
   5.235 -	val _ = if !trace_sat then
   5.236 -			tracing (string_of_int (!counter) ^ " resolution step(s) total.")
   5.237 -		else ()
   5.238 +	val _            = counter := 0
   5.239 +	val empty_clause = prove_clause empty_id
   5.240 +	val _            = if !trace_sat then tracing ("Proof reconstruction successful; " ^ string_of_int (!counter) ^ " resolution step(s) total.") else ()
   5.241  in
   5.242 -	(valOf o Array.sub) (clauses, empty_id)
   5.243 +	empty_clause
   5.244  end;
   5.245  
   5.246 -(* ------------------------------------------------------------------------- *)
   5.247 -(* Functions to build the sat tactic                                         *)
   5.248 -(* ------------------------------------------------------------------------- *)
   5.249 -
   5.250 -fun collect_atoms (Const ("Trueprop", _) $ x) ls = collect_atoms x ls
   5.251 -  | collect_atoms (Const ("op |", _) $ x $ y) ls = collect_atoms x (collect_atoms y ls)
   5.252 -  | collect_atoms x                           ls = x ins ls;
   5.253 -
   5.254 -fun has_duals []      = false
   5.255 -  | has_duals (x::xs) = dual_mem x xs orelse has_duals xs;
   5.256 -
   5.257 -fun is_trivial_clause (Const ("True", _)) = true
   5.258 -  | is_trivial_clause c                   = has_duals (collect_atoms c []);
   5.259 +(* PropLogic.prop_formula -> string *)
   5.260 +fun string_of_prop_formula PropLogic.True             = "True"
   5.261 +  | string_of_prop_formula PropLogic.False            = "False"
   5.262 +  | string_of_prop_formula (PropLogic.BoolVar i)      = "x" ^ string_of_int i
   5.263 +  | string_of_prop_formula (PropLogic.Not fm)         = "~" ^ string_of_prop_formula fm
   5.264 +  | string_of_prop_formula (PropLogic.Or (fm1, fm2))  = "(" ^ string_of_prop_formula fm1 ^ " v " ^ string_of_prop_formula fm2 ^ ")"
   5.265 +  | string_of_prop_formula (PropLogic.And (fm1, fm2)) = "(" ^ string_of_prop_formula fm1 ^ " & " ^ string_of_prop_formula fm2 ^ ")";
   5.266  
   5.267  (* ------------------------------------------------------------------------- *)
   5.268  (* rawsat_thm: run external SAT solver with the given clauses.  Reconstructs *)
   5.269 -(*      a proof from the resulting proof trace of the SAT solver.            *)
   5.270 +(*      a proof from the resulting proof trace of the SAT solver.  Each      *)
   5.271 +(*      premise in 'prems' that is not a clause is ignored, and the theorem  *)
   5.272 +(*      returned is just "False" (with some clauses as hyps).                *)
   5.273  (* ------------------------------------------------------------------------- *)
   5.274  
   5.275 -fun rawsat_thm sg prems =
   5.276 +(* Thm.thm list -> Thm.thm *)
   5.277 +
   5.278 +fun rawsat_thm prems =
   5.279  let
   5.280 -	val thms       = filter (not o is_trivial_clause o term_of o cprop_of) prems  (* remove trivial clauses *)
   5.281 -	val (fm, dict) = cnf.cnf2prop thms
   5.282 -	val _          = if !trace_sat then tracing "Invoking SAT solver ..." else ()
   5.283 +	(* remove premises that equal "True" *)
   5.284 +	val non_triv_prems    = filter (fn thm =>
   5.285 +		(not_equal HOLogic.true_const o HOLogic.dest_Trueprop o prop_of) thm
   5.286 +			handle TERM ("dest_Trueprop", _) => true) prems
   5.287 +	(* remove non-clausal premises -- of course this shouldn't actually   *)
   5.288 +	(* remove anything as long as 'rawsat_thm' is only called after the   *)
   5.289 +	(* premises have been converted to clauses                            *)
   5.290 +	val clauses           = filter (fn thm =>
   5.291 +		((cnf.is_clause o HOLogic.dest_Trueprop o prop_of) thm handle TERM ("dest_Trueprop", _) => false)
   5.292 +		orelse (warning ("Ignoring non-clausal premise " ^ (string_of_cterm o cprop_of) thm); false)) non_triv_prems
   5.293 +	(* remove trivial clauses -- this is necessary because zChaff removes *)
   5.294 +	(* trivial clauses during preprocessing, and otherwise our clause     *)
   5.295 +	(* numbering would be off                                             *)
   5.296 +	val non_triv_clauses  = filter (not o cnf.clause_is_trivial o HOLogic.dest_Trueprop o prop_of) clauses
   5.297 +	(* translate clauses from HOL terms to PropLogic.prop_formula *)
   5.298 +	val (fms, atom_table) = fold_map (PropLogic.prop_formula_of_term o HOLogic.dest_Trueprop o prop_of) non_triv_clauses Termtab.empty
   5.299 +	val _                 = if !trace_sat then
   5.300 +			tracing ("Invoking SAT solver on clauses:\n" ^ space_implode "\n" (map string_of_prop_formula fms))
   5.301 +		else ()
   5.302 +	val fm                = PropLogic.all fms
   5.303  in
   5.304  	case SatSolver.invoke_solver "zchaff_with_proofs" fm of
   5.305  	  SatSolver.UNSATISFIABLE (SOME (clause_table, empty_id)) =>
   5.306  		let
   5.307 -			val _         = if !trace_sat then
   5.308 +			val _          = if !trace_sat then
   5.309  					tracing ("Proof trace from SAT solver:\n" ^
   5.310  						"clauses: [" ^ commas (map (fn (c, cs) =>
   5.311  							"(" ^ string_of_int c ^ ", [" ^ commas (map string_of_int cs) ^ "])") (Inttab.dest clause_table)) ^ "]\n" ^
   5.312  						"empty clause: " ^ string_of_int empty_id)
   5.313  				else ()
   5.314 -			val raw_thms  = cnf.cnf2raw_thms thms
   5.315 -			val raw_thms' = map (rule_by_tactic distinct_subgoals_tac) raw_thms
   5.316 -			(* initialize the clause array with the original clauses *)
   5.317 -			val max_idx   = valOf (Inttab.max_key clause_table)
   5.318 -			val clauses   = Array.array (max_idx + 1, NONE)
   5.319 -			val _         = fold (fn thm => fn idx => (Array.update (clauses, idx, SOME thm); idx+1)) raw_thms' 0
   5.320 +			(* initialize the clause array with the given clauses, *)
   5.321 +			(* but converted to raw clause format                  *)
   5.322 +			val max_idx     = valOf (Inttab.max_key clause_table)
   5.323 +			val clause_arr  = Array.array (max_idx + 1, NONE)
   5.324 +			val raw_clauses = map (Seq.hd o distinct_subgoals_tac o cnf.clause2raw_thm) non_triv_clauses
   5.325 +			val _           = fold (fn thm => fn idx => (Array.update (clause_arr, idx, SOME thm); idx+1)) raw_clauses 0
   5.326  		in
   5.327 -			replay_proof sg clauses (clause_table, empty_id)
   5.328 +			(* replay the proof to derive the empty clause *)
   5.329 +			replay_proof clause_arr (clause_table, empty_id)
   5.330  		end
   5.331  	| SatSolver.UNSATISFIABLE NONE =>
   5.332  		raise THM ("SAT solver claims the formula to be unsatisfiable, but did not provide a proof", 0, [])
   5.333  	| SatSolver.SATISFIABLE assignment =>
   5.334  		let
   5.335  			val msg = "SAT solver found a countermodel:\n"
   5.336 -				^ (enclose "{" "}"
   5.337 -					o commas
   5.338 -					o map (Sign.string_of_term sg o fst)
   5.339 -					o filter (fn (_, idx) => getOpt (assignment idx, false))) dict
   5.340 +				^ (commas
   5.341 +					o map (fn (term, idx) =>
   5.342 +						Sign.string_of_term (the_context ()) term ^ ": "
   5.343 +							^ (case assignment idx of NONE => "arbitrary" | SOME true => "true" | SOME false => "false")))
   5.344 +					(Termtab.dest atom_table)
   5.345  		in
   5.346  			raise THM (msg, 0, [])
   5.347  		end
   5.348 @@ -263,27 +260,73 @@
   5.349  (* Tactics                                                                   *)
   5.350  (* ------------------------------------------------------------------------- *)
   5.351  
   5.352 -fun cnfsat_basic_tac state =
   5.353 -let
   5.354 -	val sg = Thm.sign_of_thm state
   5.355 -in
   5.356 -	METAHYPS (fn prems => rtac (rawsat_thm sg prems) 1) 1 state
   5.357 -end;
   5.358 +(* ------------------------------------------------------------------------- *)
   5.359 +(* rawsat_tac: solves the i-th subgoal of the proof state; this subgoal      *)
   5.360 +(*      should be of the form                                                *)
   5.361 +(*        [| c1; c2; ...; ck |] ==> False                                    *)
   5.362 +(*      where each cj is a non-empty clause (i.e. a disjunction of literals) *)
   5.363 +(*      or "True"                                                            *)
   5.364 +(* ------------------------------------------------------------------------- *)
   5.365 +
   5.366 +(* int -> Tactical.tactic *)
   5.367 +
   5.368 +fun rawsat_tac i = METAHYPS (fn prems => rtac (rawsat_thm prems) 1) i;
   5.369  
   5.370 -(* a trivial tactic, used in preprocessing before calling the main tactic *)
   5.371 -val pre_sat_tac = (REPEAT (etac conjE 1)) THEN (REPEAT ((atac 1) ORELSE (etac FalseE 1)));
   5.372 +(* ------------------------------------------------------------------------- *)
   5.373 +(* pre_cnf_tac: converts the i-th subgoal                                    *)
   5.374 +(*        [| A1 ; ... ; An |] ==> B                                          *)
   5.375 +(*      to                                                                   *)
   5.376 +(*        [| A1; ... ; An ; ~B |] ==> False                                  *)
   5.377 +(*      (handling meta-logical connectives in B properly before negating),   *)
   5.378 +(*      then replaces meta-logical connectives in the premises (i.e. "==>",  *)
   5.379 +(*      "!!" and "==") by connectives of the HOL object-logic (i.e. by       *)
   5.380 +(*      "-->", "!", and "=")                                                 *)
   5.381 +(* ------------------------------------------------------------------------- *)
   5.382 +
   5.383 +(* int -> Tactical.tactic *)
   5.384 +
   5.385 +fun pre_cnf_tac i = rtac ccontr i THEN ObjectLogic.atomize_tac i;
   5.386 +
   5.387 +(* ------------------------------------------------------------------------- *)
   5.388 +(* cnfsat_tac: checks if the empty clause "False" occurs among the premises; *)
   5.389 +(*      if not, eliminates conjunctions (i.e. each clause of the CNF formula *)
   5.390 +(*      becomes a separate premise), then applies 'rawsat_tac' to solve the  *)
   5.391 +(*      subgoal                                                              *)
   5.392 +(* ------------------------------------------------------------------------- *)
   5.393  
   5.394 -(* tactic for calling external SAT solver, taking as input CNF clauses *)
   5.395 -val cnfsat_tac = pre_sat_tac THEN (IF_UNSOLVED cnfsat_basic_tac);
   5.396 +(* int -> Tactical.tactic *)
   5.397 +
   5.398 +fun cnfsat_tac i = (etac FalseE i) ORELSE (REPEAT_DETERM (etac conjE i) THEN rawsat_tac i);
   5.399  
   5.400 -(* tactic for calling external SAT solver, taking as input arbitrary formula *)
   5.401 -val sat_tac = cnf.cnf_thin_tac THEN cnfsat_tac;
   5.402 +(* ------------------------------------------------------------------------- *)
   5.403 +(* cnfxsat_tac: checks if the empty clause "False" occurs among the          *)
   5.404 +(*      premises; if not, eliminates conjunctions (i.e. each clause of the   *)
   5.405 +(*      CNF formula becomes a separate premise) and existential quantifiers, *)
   5.406 +(*      then applies 'rawsat_tac' to solve the subgoal                       *)
   5.407 +(* ------------------------------------------------------------------------- *)
   5.408 +
   5.409 +(* int -> Tactical.tactic *)
   5.410 +
   5.411 +fun cnfxsat_tac i = (etac FalseE i) ORELSE (REPEAT_DETERM (etac conjE i ORELSE etac exE i) THEN rawsat_tac i);
   5.412  
   5.413 -(*
   5.414 -  Tactic for calling external SAT solver, taking as input arbitrary formula.
   5.415 -  The input is translated to CNF (in primitive form), possibly introducing
   5.416 -  new literals.
   5.417 -*)
   5.418 -val satx_tac = cnf.cnfx_thin_tac THEN cnfsat_tac;
   5.419 +(* ------------------------------------------------------------------------- *)
   5.420 +(* sat_tac: tactic for calling an external SAT solver, taking as input an    *)
   5.421 +(*      arbitrary formula.  The input is translated to CNF, possibly causing *)
   5.422 +(*      an exponential blowup.                                               *)
   5.423 +(* ------------------------------------------------------------------------- *)
   5.424 +
   5.425 +(* int -> Tactical.tactic *)
   5.426 +
   5.427 +fun sat_tac i = pre_cnf_tac i THEN cnf.cnf_rewrite_tac i THEN cnfsat_tac i;
   5.428 +
   5.429 +(* ------------------------------------------------------------------------- *)
   5.430 +(* satx_tac: tactic for calling an external SAT solver, taking as input an   *)
   5.431 +(*      arbitrary formula.  The input is translated to CNF, possibly         *)
   5.432 +(*      introducing new literals.                                            *)
   5.433 +(* ------------------------------------------------------------------------- *)
   5.434 +
   5.435 +(* int -> Tactical.tactic *)
   5.436 +
   5.437 +fun satx_tac i = pre_cnf_tac i THEN cnf.cnfx_rewrite_tac i THEN cnfxsat_tac i;
   5.438  
   5.439  end;  (* of structure *)
     6.1 --- a/src/HOL/ex/SAT_Examples.thy	Sat Oct 08 23:43:15 2005 +0200
     6.2 +++ b/src/HOL/ex/SAT_Examples.thy	Sun Oct 09 17:06:03 2005 +0200
     6.3 @@ -12,6 +12,63 @@
     6.4  
     6.5  ML {* set sat.trace_sat; *}
     6.6  
     6.7 +lemma "True"
     6.8 +by sat
     6.9 +
    6.10 +lemma "a | ~a"
    6.11 +by sat
    6.12 +
    6.13 +lemma "(a | b) & ~a \<Longrightarrow> b"
    6.14 +by sat
    6.15 +
    6.16 +lemma "(a & b) | (c & d) \<Longrightarrow> (a & b) | (c & d)"
    6.17 +apply (tactic {* cnf.cnf_rewrite_tac 1 *})
    6.18 +by sat
    6.19 +
    6.20 +lemma "(a & b) | (c & d) \<Longrightarrow> (a & b) | (c & d)"
    6.21 +apply (tactic {* cnf.cnfx_rewrite_tac 1 *})
    6.22 +apply (erule exE | erule conjE)+
    6.23 +by satx
    6.24 +
    6.25 +lemma "(a & b | c & d) & (e & f | g & h) | (i & j | k & l) & (m & n | p & q) \<Longrightarrow>
    6.26 +  (a & b | c & d) & (e & f | g & h) | (i & j | k & l) & (m & n | p & q)"
    6.27 +apply (tactic {* cnf.cnf_rewrite_tac 1 *})
    6.28 +by sat
    6.29 +
    6.30 +lemma "(a & b | c & d) & (e & f | g & h) | (i & j | k & l) & (m & n | p & q) \<Longrightarrow>
    6.31 +  (a & b | c & d) & (e & f | g & h) | (i & j | k & l) & (m & n | p & q)"
    6.32 +apply (tactic {* cnf.cnfx_rewrite_tac 1 *})
    6.33 +apply (erule exE | erule conjE)+
    6.34 +by satx
    6.35 +
    6.36 +lemma "P=P=P=P=P=P=P=P=P=P"
    6.37 +by sat
    6.38 +
    6.39 +lemma "P=P=P=P=P=P=P=P=P=P"
    6.40 +by satx
    6.41 +
    6.42 +lemma  "!! a b c. [| a | b | c | d ;
    6.43 +e | f | (a & d) ;
    6.44 +~(a | (c & ~c)) | b ;
    6.45 +~(b & (x | ~x)) | c ;
    6.46 +~(d | False) | c ;
    6.47 +~(c | (~p & (p | (q & ~q)))) |] ==> False"
    6.48 +by sat
    6.49 +
    6.50 +lemma  "!! a b c. [| a | b | c | d ;
    6.51 +e | f | (a & d) ;
    6.52 +~(a | (c & ~c)) | b ;
    6.53 +~(b & (x | ~x)) | c ;
    6.54 +~(d | False) | c ;
    6.55 +~(c | (~p & (p | (q & ~q)))) |] ==> False"
    6.56 +by satx
    6.57 +
    6.58 +ML {* reset sat.trace_sat; *}
    6.59 +
    6.60 +(*
    6.61 +ML {* Toplevel.profiling := 1; *}
    6.62 +*)
    6.63 +
    6.64  (* Translated from TPTP problem library: PUZ015-2.006.dimacs *)
    6.65  
    6.66  lemma assumes 1: "~x0"
    6.67 @@ -199,16 +256,240 @@
    6.68  and 183: "~x29 | ~x58"
    6.69  and 184: "~x28 | ~x58"
    6.70  shows "False"
    6.71 -using 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 
    6.72 -20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 
    6.73 -40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 
    6.74 -60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 
    6.75 -80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 
    6.76 -100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 
    6.77 -120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 
    6.78 -140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 
    6.79 -160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 
    6.80 -180 181 182 183 184 
    6.81 +using 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19
    6.82 +20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39
    6.83 +40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59
    6.84 +60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79
    6.85 +80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99
    6.86 +100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119
    6.87 +120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139
    6.88 +140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159
    6.89 +160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179
    6.90 +180 181 182 183 184
    6.91  by sat
    6.92  
    6.93 +(* Translated from TPTP problem library: MSC007-1.008.dimacs *)
    6.94 +
    6.95 +lemma assumes 1: "x0 | x1 | x2 | x3 | x4 | x5 | x6"
    6.96 +and 2: "x7 | x8 | x9 | x10 | x11 | x12 | x13"
    6.97 +and 3: "x14 | x15 | x16 | x17 | x18 | x19 | x20"
    6.98 +and 4: "x21 | x22 | x23 | x24 | x25 | x26 | x27"
    6.99 +and 5: "x28 | x29 | x30 | x31 | x32 | x33 | x34"
   6.100 +and 6: "x35 | x36 | x37 | x38 | x39 | x40 | x41"
   6.101 +and 7: "x42 | x43 | x44 | x45 | x46 | x47 | x48"
   6.102 +and 8: "x49 | x50 | x51 | x52 | x53 | x54 | x55"
   6.103 +and 9: "~x0 | ~x7"
   6.104 +and 10: "~x0 | ~x14"
   6.105 +and 11: "~x0 | ~x21"
   6.106 +and 12: "~x0 | ~x28"
   6.107 +and 13: "~x0 | ~x35"
   6.108 +and 14: "~x0 | ~x42"
   6.109 +and 15: "~x0 | ~x49"
   6.110 +and 16: "~x7 | ~x14"
   6.111 +and 17: "~x7 | ~x21"
   6.112 +and 18: "~x7 | ~x28"
   6.113 +and 19: "~x7 | ~x35"
   6.114 +and 20: "~x7 | ~x42"
   6.115 +and 21: "~x7 | ~x49"
   6.116 +and 22: "~x14 | ~x21"
   6.117 +and 23: "~x14 | ~x28"
   6.118 +and 24: "~x14 | ~x35"
   6.119 +and 25: "~x14 | ~x42"
   6.120 +and 26: "~x14 | ~x49"
   6.121 +and 27: "~x21 | ~x28"
   6.122 +and 28: "~x21 | ~x35"
   6.123 +and 29: "~x21 | ~x42"
   6.124 +and 30: "~x21 | ~x49"
   6.125 +and 31: "~x28 | ~x35"
   6.126 +and 32: "~x28 | ~x42"
   6.127 +and 33: "~x28 | ~x49"
   6.128 +and 34: "~x35 | ~x42"
   6.129 +and 35: "~x35 | ~x49"
   6.130 +and 36: "~x42 | ~x49"
   6.131 +and 37: "~x1 | ~x8"
   6.132 +and 38: "~x1 | ~x15"
   6.133 +and 39: "~x1 | ~x22"
   6.134 +and 40: "~x1 | ~x29"
   6.135 +and 41: "~x1 | ~x36"
   6.136 +and 42: "~x1 | ~x43"
   6.137 +and 43: "~x1 | ~x50"
   6.138 +and 44: "~x8 | ~x15"
   6.139 +and 45: "~x8 | ~x22"
   6.140 +and 46: "~x8 | ~x29"
   6.141 +and 47: "~x8 | ~x36"
   6.142 +and 48: "~x8 | ~x43"
   6.143 +and 49: "~x8 | ~x50"
   6.144 +and 50: "~x15 | ~x22"
   6.145 +and 51: "~x15 | ~x29"
   6.146 +and 52: "~x15 | ~x36"
   6.147 +and 53: "~x15 | ~x43"
   6.148 +and 54: "~x15 | ~x50"
   6.149 +and 55: "~x22 | ~x29"
   6.150 +and 56: "~x22 | ~x36"
   6.151 +and 57: "~x22 | ~x43"
   6.152 +and 58: "~x22 | ~x50"
   6.153 +and 59: "~x29 | ~x36"
   6.154 +and 60: "~x29 | ~x43"
   6.155 +and 61: "~x29 | ~x50"
   6.156 +and 62: "~x36 | ~x43"
   6.157 +and 63: "~x36 | ~x50"
   6.158 +and 64: "~x43 | ~x50"
   6.159 +and 65: "~x2 | ~x9"
   6.160 +and 66: "~x2 | ~x16"
   6.161 +and 67: "~x2 | ~x23"
   6.162 +and 68: "~x2 | ~x30"
   6.163 +and 69: "~x2 | ~x37"
   6.164 +and 70: "~x2 | ~x44"
   6.165 +and 71: "~x2 | ~x51"
   6.166 +and 72: "~x9 | ~x16"
   6.167 +and 73: "~x9 | ~x23"
   6.168 +and 74: "~x9 | ~x30"
   6.169 +and 75: "~x9 | ~x37"
   6.170 +and 76: "~x9 | ~x44"
   6.171 +and 77: "~x9 | ~x51"
   6.172 +and 78: "~x16 | ~x23"
   6.173 +and 79: "~x16 | ~x30"
   6.174 +and 80: "~x16 | ~x37"
   6.175 +and 81: "~x16 | ~x44"
   6.176 +and 82: "~x16 | ~x51"
   6.177 +and 83: "~x23 | ~x30"
   6.178 +and 84: "~x23 | ~x37"
   6.179 +and 85: "~x23 | ~x44"
   6.180 +and 86: "~x23 | ~x51"
   6.181 +and 87: "~x30 | ~x37"
   6.182 +and 88: "~x30 | ~x44"
   6.183 +and 89: "~x30 | ~x51"
   6.184 +and 90: "~x37 | ~x44"
   6.185 +and 91: "~x37 | ~x51"
   6.186 +and 92: "~x44 | ~x51"
   6.187 +and 93: "~x3 | ~x10"
   6.188 +and 94: "~x3 | ~x17"
   6.189 +and 95: "~x3 | ~x24"
   6.190 +and 96: "~x3 | ~x31"
   6.191 +and 97: "~x3 | ~x38"
   6.192 +and 98: "~x3 | ~x45"
   6.193 +and 99: "~x3 | ~x52"
   6.194 +and 100: "~x10 | ~x17"
   6.195 +and 101: "~x10 | ~x24"
   6.196 +and 102: "~x10 | ~x31"
   6.197 +and 103: "~x10 | ~x38"
   6.198 +and 104: "~x10 | ~x45"
   6.199 +and 105: "~x10 | ~x52"
   6.200 +and 106: "~x17 | ~x24"
   6.201 +and 107: "~x17 | ~x31"
   6.202 +and 108: "~x17 | ~x38"
   6.203 +and 109: "~x17 | ~x45"
   6.204 +and 110: "~x17 | ~x52"
   6.205 +and 111: "~x24 | ~x31"
   6.206 +and 112: "~x24 | ~x38"
   6.207 +and 113: "~x24 | ~x45"
   6.208 +and 114: "~x24 | ~x52"
   6.209 +and 115: "~x31 | ~x38"
   6.210 +and 116: "~x31 | ~x45"
   6.211 +and 117: "~x31 | ~x52"
   6.212 +and 118: "~x38 | ~x45"
   6.213 +and 119: "~x38 | ~x52"
   6.214 +and 120: "~x45 | ~x52"
   6.215 +and 121: "~x4 | ~x11"
   6.216 +and 122: "~x4 | ~x18"
   6.217 +and 123: "~x4 | ~x25"
   6.218 +and 124: "~x4 | ~x32"
   6.219 +and 125: "~x4 | ~x39"
   6.220 +and 126: "~x4 | ~x46"
   6.221 +and 127: "~x4 | ~x53"
   6.222 +and 128: "~x11 | ~x18"
   6.223 +and 129: "~x11 | ~x25"
   6.224 +and 130: "~x11 | ~x32"
   6.225 +and 131: "~x11 | ~x39"
   6.226 +and 132: "~x11 | ~x46"
   6.227 +and 133: "~x11 | ~x53"
   6.228 +and 134: "~x18 | ~x25"
   6.229 +and 135: "~x18 | ~x32"
   6.230 +and 136: "~x18 | ~x39"
   6.231 +and 137: "~x18 | ~x46"
   6.232 +and 138: "~x18 | ~x53"
   6.233 +and 139: "~x25 | ~x32"
   6.234 +and 140: "~x25 | ~x39"
   6.235 +and 141: "~x25 | ~x46"
   6.236 +and 142: "~x25 | ~x53"
   6.237 +and 143: "~x32 | ~x39"
   6.238 +and 144: "~x32 | ~x46"
   6.239 +and 145: "~x32 | ~x53"
   6.240 +and 146: "~x39 | ~x46"
   6.241 +and 147: "~x39 | ~x53"
   6.242 +and 148: "~x46 | ~x53"
   6.243 +and 149: "~x5 | ~x12"
   6.244 +and 150: "~x5 | ~x19"
   6.245 +and 151: "~x5 | ~x26"
   6.246 +and 152: "~x5 | ~x33"
   6.247 +and 153: "~x5 | ~x40"
   6.248 +and 154: "~x5 | ~x47"
   6.249 +and 155: "~x5 | ~x54"
   6.250 +and 156: "~x12 | ~x19"
   6.251 +and 157: "~x12 | ~x26"
   6.252 +and 158: "~x12 | ~x33"
   6.253 +and 159: "~x12 | ~x40"
   6.254 +and 160: "~x12 | ~x47"
   6.255 +and 161: "~x12 | ~x54"
   6.256 +and 162: "~x19 | ~x26"
   6.257 +and 163: "~x19 | ~x33"
   6.258 +and 164: "~x19 | ~x40"
   6.259 +and 165: "~x19 | ~x47"
   6.260 +and 166: "~x19 | ~x54"
   6.261 +and 167: "~x26 | ~x33"
   6.262 +and 168: "~x26 | ~x40"
   6.263 +and 169: "~x26 | ~x47"
   6.264 +and 170: "~x26 | ~x54"
   6.265 +and 171: "~x33 | ~x40"
   6.266 +and 172: "~x33 | ~x47"
   6.267 +and 173: "~x33 | ~x54"
   6.268 +and 174: "~x40 | ~x47"
   6.269 +and 175: "~x40 | ~x54"
   6.270 +and 176: "~x47 | ~x54"
   6.271 +and 177: "~x6 | ~x13"
   6.272 +and 178: "~x6 | ~x20"
   6.273 +and 179: "~x6 | ~x27"
   6.274 +and 180: "~x6 | ~x34"
   6.275 +and 181: "~x6 | ~x41"
   6.276 +and 182: "~x6 | ~x48"
   6.277 +and 183: "~x6 | ~x55"
   6.278 +and 184: "~x13 | ~x20"
   6.279 +and 185: "~x13 | ~x27"
   6.280 +and 186: "~x13 | ~x34"
   6.281 +and 187: "~x13 | ~x41"
   6.282 +and 188: "~x13 | ~x48"
   6.283 +and 189: "~x13 | ~x55"
   6.284 +and 190: "~x20 | ~x27"
   6.285 +and 191: "~x20 | ~x34"
   6.286 +and 192: "~x20 | ~x41"
   6.287 +and 193: "~x20 | ~x48"
   6.288 +and 194: "~x20 | ~x55"
   6.289 +and 195: "~x27 | ~x34"
   6.290 +and 196: "~x27 | ~x41"
   6.291 +and 197: "~x27 | ~x48"
   6.292 +and 198: "~x27 | ~x55"
   6.293 +and 199: "~x34 | ~x41"
   6.294 +and 200: "~x34 | ~x48"
   6.295 +and 201: "~x34 | ~x55"
   6.296 +and 202: "~x41 | ~x48"
   6.297 +and 203: "~x41 | ~x55"
   6.298 +and 204: "~x48 | ~x55"
   6.299 +shows "False"
   6.300 +using 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19
   6.301 +20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39
   6.302 +40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59
   6.303 +60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79
   6.304 +80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99
   6.305 +100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119
   6.306 +120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139
   6.307 +140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159
   6.308 +160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179
   6.309 +180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199
   6.310 +200 201 202 203 204
   6.311 +by sat
   6.312 +
   6.313 +(*
   6.314 +ML {* Toplevel.profiling := 0; *}
   6.315 +*)
   6.316 +
   6.317  end