webertj@14350: (*  Title:      HOL/Refute.thy
webertj@14350:     ID:         $Id$
webertj@14350:     Author:     Tjark Weber
webertj@22058:     Copyright   2003-2007
webertj@14350: 
webertj@14350: Basic setup and documentation for the 'refute' (and 'refute_params') command.
webertj@14350: *)
webertj@14350: 
wenzelm@14589: header {* Refute *}
wenzelm@14589: 
nipkow@15131: theory Refute
blanchet@29820: imports Hilbert_Choice List Record
haftmann@26521: uses
haftmann@26521:   "Tools/prop_logic.ML"
haftmann@26521:   "Tools/sat_solver.ML"
haftmann@26521:   "Tools/refute.ML"
haftmann@26521:   "Tools/refute_isar.ML"
nipkow@15131: begin
wenzelm@14589: 
wenzelm@14589: setup Refute.setup
wenzelm@14589: 
wenzelm@14589: text {*
wenzelm@14589: \small
wenzelm@14589: \begin{verbatim}
webertj@14350: (* ------------------------------------------------------------------------- *)
webertj@14350: (* REFUTE                                                                    *)
webertj@14350: (*                                                                           *)
webertj@14350: (* We use a SAT solver to search for a (finite) model that refutes a given   *)
webertj@14350: (* HOL formula.                                                              *)
webertj@14350: (* ------------------------------------------------------------------------- *)
webertj@14350: 
webertj@14350: (* ------------------------------------------------------------------------- *)
webertj@14457: (* NOTE                                                                      *)
webertj@14350: (*                                                                           *)
webertj@14457: (* I strongly recommend that you install a stand-alone SAT solver if you     *)
webertj@14463: (* want to use 'refute'.  For details see 'HOL/Tools/sat_solver.ML'.  If you *)
webertj@15293: (* have installed (a supported version of) zChaff, simply set 'ZCHAFF_HOME'  *)
webertj@15293: (* in 'etc/settings'.                                                        *)
webertj@14350: (* ------------------------------------------------------------------------- *)
webertj@14350: 
webertj@14350: (* ------------------------------------------------------------------------- *)
webertj@14350: (* USAGE                                                                     *)
webertj@14350: (*                                                                           *)
webertj@14350: (* See the file 'HOL/ex/Refute_Examples.thy' for examples.  The supported    *)
webertj@14350: (* parameters are explained below.                                           *)
webertj@14350: (* ------------------------------------------------------------------------- *)
webertj@14350: 
webertj@14350: (* ------------------------------------------------------------------------- *)
webertj@14350: (* CURRENT LIMITATIONS                                                       *)
webertj@14350: (*                                                                           *)
webertj@14350: (* 'refute' currently accepts formulas of higher-order predicate logic (with *)
webertj@14350: (* equality), including free/bound/schematic variables, lambda abstractions, *)
webertj@16870: (* sets and set membership, "arbitrary", "The", "Eps", records and           *)
webertj@22058: (* inductively defined sets.  Constants are unfolded automatically, and sort *)
webertj@22058: (* axioms are added as well.  Other, user-asserted axioms however are        *)
webertj@22058: (* ignored.  Inductive datatypes and recursive functions are supported, but  *)
webertj@22058: (* may lead to spurious countermodels.                                       *)
webertj@14463: (*                                                                           *)
webertj@14808: (* The (space) complexity of the algorithm is non-elementary.                *)
webertj@14350: (*                                                                           *)
webertj@16870: (* Schematic type variables are not supported.                               *)
webertj@14350: (* ------------------------------------------------------------------------- *)
webertj@14350: 
webertj@14350: (* ------------------------------------------------------------------------- *)
webertj@14350: (* PARAMETERS                                                                *)
webertj@14350: (*                                                                           *)
webertj@14350: (* The following global parameters are currently supported (and required):   *)
webertj@14350: (*                                                                           *)
webertj@14350: (* Name          Type    Description                                         *)
webertj@14350: (*                                                                           *)
webertj@14350: (* "minsize"     int     Only search for models with size at least           *)
webertj@14350: (*                       'minsize'.                                          *)
webertj@14350: (* "maxsize"     int     If >0, only search for models with size at most     *)
webertj@14350: (*                       'maxsize'.                                          *)
webertj@14350: (* "maxvars"     int     If >0, use at most 'maxvars' boolean variables      *)
webertj@14350: (*                       when transforming the term into a propositional     *)
webertj@14350: (*                       formula.                                            *)
webertj@14808: (* "maxtime"     int     If >0, terminate after at most 'maxtime' seconds.   *)
webertj@14808: (*                       This value is ignored under some ML compilers.      *)
webertj@14457: (* "satsolver"   string  Name of the SAT solver to be used.                  *)
webertj@14457: (*                                                                           *)
wenzelm@17721: (* See 'HOL/SAT.thy' for default values.                                     *)
webertj@14808: (*                                                                           *)
webertj@14808: (* The size of particular types can be specified in the form type=size       *)
webertj@14808: (* (where 'type' is a string, and 'size' is an int).  Examples:              *)
webertj@14808: (* "'a"=1                                                                    *)
webertj@14808: (* "List.list"=2                                                             *)
webertj@14350: (* ------------------------------------------------------------------------- *)
webertj@14350: 
webertj@14350: (* ------------------------------------------------------------------------- *)
webertj@14350: (* FILES                                                                     *)
webertj@14350: (*                                                                           *)
webertj@14457: (* HOL/Tools/prop_logic.ML    Propositional logic                            *)
webertj@14457: (* HOL/Tools/sat_solver.ML    SAT solvers                                    *)
webertj@14457: (* HOL/Tools/refute.ML        Translation HOL -> propositional logic and     *)
webertj@14808: (*                            Boolean assignment -> HOL model                *)
webertj@14350: (* HOL/Tools/refute_isar.ML   Adds 'refute'/'refute_params' to Isabelle's    *)
webertj@14457: (*                            syntax                                         *)
webertj@14457: (* HOL/Refute.thy             This file: loads the ML files, basic setup,    *)
webertj@14457: (*                            documentation                                  *)
wenzelm@17721: (* HOL/SAT.thy                Sets default parameters                        *)
webertj@14457: (* HOL/ex/RefuteExamples.thy  Examples                                       *)
webertj@14350: (* ------------------------------------------------------------------------- *)
wenzelm@14589: \end{verbatim}
wenzelm@14589: *}
webertj@14350: 
webertj@14350: end