diff -r 8d92e426eb38 -r 41b32020d0b3 src/HOL/Refute.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Refute.thy	Sat Jan 10 13:35:10 2004 +0100
@@ -0,0 +1,116 @@
+(*  Title:      HOL/Refute.thy
+    ID:         $Id$
+    Author:     Tjark Weber
+    Copyright   2003-2004
+
+Basic setup and documentation for the 'refute' (and 'refute_params') command.
+*)
+
+(* ------------------------------------------------------------------------- *)
+(* REFUTE                                                                    *)
+(*                                                                           *)
+(* We use a SAT solver to search for a (finite) model that refutes a given   *)
+(* HOL formula.                                                              *)
+(* ------------------------------------------------------------------------- *)
+
+(* ------------------------------------------------------------------------- *)
+(* INSTALLATION                                                              *)
+(*                                                                           *)
+(* 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.  *)
+(* ------------------------------------------------------------------------- *)
+
+(* ------------------------------------------------------------------------- *)
+(* USAGE                                                                     *)
+(*                                                                           *)
+(* See the file 'HOL/ex/Refute_Examples.thy' for examples.  The supported    *)
+(* parameters are explained below.                                           *)
+(* ------------------------------------------------------------------------- *)
+
+(* ------------------------------------------------------------------------- *)
+(* CURRENT LIMITATIONS                                                       *)
+(*                                                                           *)
+(* 'refute' currently accepts formulas of higher-order predicate logic (with *)
+(* equality), including free/bound/schematic variables, lambda abstractions, *)
+(* sets and set membership.                                                  *)
+(*                                                                           *)
+(* 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)'.                                                 *)
+(*                                                                           *)
+(* For formulas that contain (variables of) an inductive datatype, a         *)
+(* spurious countermodel may be returned.  Currently no warning is issued in *)
+(* this case.                                                                *)
+(* ------------------------------------------------------------------------- *)
+
+(* ------------------------------------------------------------------------- *)
+(* PARAMETERS                                                                *)
+(*                                                                           *)
+(* The following global parameters are currently supported (and required):   *)
+(*                                                                           *)
+(* Name          Type    Description                                         *)
+(*                                                                           *)
+(* "minsize"     int     Only search for models with size at least           *)
+(*                       'minsize'.                                          *)
+(* "maxsize"     int     If >0, only search for models with size at most     *)
+(*                       'maxsize'.                                          *)
+(* "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'.                                          *)
+(* ------------------------------------------------------------------------- *)
+
+(* ------------------------------------------------------------------------- *)
+(* FILES                                                                     *)
+(*                                                                           *)
+(* HOL/Tools/refute.ML        Implementation of the algorithm.               *)
+(* 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.                                      *)
+(* ------------------------------------------------------------------------- *)
+
+header {* Refute *}
+
+theory Refute = Map
+
+files "Tools/refute.ML"
+      "Tools/refute_isar.ML":
+
+(* Setting up the 'refute' and 'refute\_params' commands *)
+
+use "Tools/refute.ML"
+use "Tools/refute_isar.ML"
+
+setup Refute.setup
+
+end