# HG changeset patch
# User webertj
# Date 1078954537 -3600
# Node ID 6d5d6e78d8519b0eb2ecfbb4205e93cece5371e0
# Parent  cca28ec5f9a60ce8be6337633894e3e068121b3e
*** empty log message ***

diff -r cca28ec5f9a6 -r 6d5d6e78d851 src/HOL/Refute.thy
--- 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"