--- a/src/HOL/Refute.thy Wed Mar 10 22:33:48 2004 +0100
+++ b/src/HOL/Refute.thy Wed Mar 10 22:35:37 2004 +0100
@@ -14,16 +14,10 @@
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
-(* INSTALLATION *)
+(* NOTE *)
(* *)
-(* 1. Install a stand-alone SAT solver. The default parameters in *)
-(* 'HOL/Main.thy' assume that ZChaff 2003.12.04 (available for Solaris/ *)
-(* Linux/Cygwin/Windows at http://ee.princeton.edu/~chaff/zchaff.php) is *)
-(* installed as '$HOME/bin/zchaff'. If you want to use a different SAT *)
-(* solver (or install ZChaff to a different location), you will need to *)
-(* modify at least the values for 'command' and (probably) 'success'. *)
-(* *)
-(* 2. That's it. You can now use the 'refute' command in your own theories. *)
+(* I strongly recommend that you install a stand-alone SAT solver if you *)
+(* want to use 'refute'. For details see 'HOL/Tools/sat_solver.ML'. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
@@ -38,17 +32,15 @@
(* *)
(* 'refute' currently accepts formulas of higher-order predicate logic (with *)
(* equality), including free/bound/schematic variables, lambda abstractions, *)
-(* sets and set membership. *)
+(* sets and set membership, "arbitrary", "The", and "Eps". Constants for *)
+(* which a defining equation exists are unfolded automatically. *)
(* *)
(* NOT (YET) SUPPORTED ARE *)
(* *)
(* - schematic type variables *)
-(* - type constructors other than =>, set, unit, and inductive datatypes *)
-(* - constants, including constructors of inductive datatypes and recursive *)
-(* functions on inductive datatypes *)
-(* *)
-(* Unfolding of constants currently needs to be done manually, e.g. using *)
-(* 'apply (unfold xxx_def)'. *)
+(* - type constructors other than bool, =>, set *)
+(* - other constants, including constructors of inductive datatypes, *)
+(* inductively defined sets and recursive functions *)
(* *)
(* For formulas that contain (variables of) an inductive datatype, a *)
(* spurious countermodel may be returned. Currently no warning is issued in *)
@@ -69,45 +61,37 @@
(* "maxvars" int If >0, use at most 'maxvars' boolean variables *)
(* when transforming the term into a propositional *)
(* formula. *)
-(* "satfile" string Name of the file used to store the propositional *)
-(* formula, i.e. the input to the SAT solver. *)
-(* "satformat" string Format of the SAT solver's input file. Must be *)
-(* either "cnf", "defcnf", or "sat". Since "sat" is *)
-(* not supported by most SAT solvers, and "cnf" can *)
-(* cause exponential blowup of the formula, "defcnf" *)
-(* is recommended. *)
-(* "resultfile" string Name of the file containing the SAT solver's *)
-(* output. *)
-(* "success" string Part of the line in the SAT solver's output that *)
-(* precedes a list of integers representing the *)
-(* satisfying assignment. *)
-(* "command" string System command used to execute the SAT solver. *)
-(* Note that you if you change 'satfile' or *)
-(* 'resultfile', you will also need to change *)
-(* 'command'. *)
+(* "satsolver" string Name of the SAT solver to be used. *)
+(* *)
+(* See 'HOL/Main.thy' for default values. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* FILES *)
(* *)
-(* HOL/Tools/refute.ML Implementation of the algorithm. *)
+(* HOL/Tools/prop_logic.ML Propositional logic *)
+(* HOL/Tools/sat_solver.ML SAT solvers *)
+(* HOL/Tools/refute.ML Translation HOL -> propositional logic and *)
+(* boolean assignment -> HOL model *)
(* HOL/Tools/refute_isar.ML Adds 'refute'/'refute_params' to Isabelle's *)
-(* syntax. *)
-(* HOL/Refute.thy This file. Loads the ML files, basic setup, *)
-(* documentation. *)
-(* HOL/Main.thy Sets default parameters. *)
-(* HOL/ex/RefuteExamples.thy Examples. *)
+(* syntax *)
+(* HOL/Refute.thy This file: loads the ML files, basic setup, *)
+(* documentation *)
+(* HOL/Main.thy Sets default parameters *)
+(* HOL/ex/RefuteExamples.thy Examples *)
(* ------------------------------------------------------------------------- *)
header {* Refute *}
theory Refute = Map
-files "Tools/refute.ML"
+files "Tools/prop_logic.ML"
+ "Tools/sat_solver.ML"
+ "Tools/refute.ML"
"Tools/refute_isar.ML":
-(* Setting up the 'refute' and 'refute\_params' commands *)
-
+use "Tools/prop_logic.ML"
+use "Tools/sat_solver.ML"
use "Tools/refute.ML"
use "Tools/refute_isar.ML"