src/HOL/Refute.thy
author wenzelm
Fri Mar 28 19:43:54 2008 +0100 (2008-03-28)
changeset 26462 dac4e2bce00d
parent 22058 49faa8c7a5d9
child 26521 f8c4e79db153
permissions -rw-r--r--
avoid rebinding of existing facts;
     1 (*  Title:      HOL/Refute.thy
     2     ID:         $Id$
     3     Author:     Tjark Weber
     4     Copyright   2003-2007
     5 
     6 Basic setup and documentation for the 'refute' (and 'refute_params') command.
     7 *)
     8 
     9 header {* Refute *}
    10 
    11 theory Refute
    12 imports Datatype
    13 uses "Tools/prop_logic.ML"
    14      "Tools/sat_solver.ML"
    15      "Tools/refute.ML"
    16      "Tools/refute_isar.ML"
    17 begin
    18 
    19 setup Refute.setup
    20 
    21 text {*
    22 \small
    23 \begin{verbatim}
    24 (* ------------------------------------------------------------------------- *)
    25 (* REFUTE                                                                    *)
    26 (*                                                                           *)
    27 (* We use a SAT solver to search for a (finite) model that refutes a given   *)
    28 (* HOL formula.                                                              *)
    29 (* ------------------------------------------------------------------------- *)
    30 
    31 (* ------------------------------------------------------------------------- *)
    32 (* NOTE                                                                      *)
    33 (*                                                                           *)
    34 (* I strongly recommend that you install a stand-alone SAT solver if you     *)
    35 (* want to use 'refute'.  For details see 'HOL/Tools/sat_solver.ML'.  If you *)
    36 (* have installed (a supported version of) zChaff, simply set 'ZCHAFF_HOME'  *)
    37 (* in 'etc/settings'.                                                        *)
    38 (* ------------------------------------------------------------------------- *)
    39 
    40 (* ------------------------------------------------------------------------- *)
    41 (* USAGE                                                                     *)
    42 (*                                                                           *)
    43 (* See the file 'HOL/ex/Refute_Examples.thy' for examples.  The supported    *)
    44 (* parameters are explained below.                                           *)
    45 (* ------------------------------------------------------------------------- *)
    46 
    47 (* ------------------------------------------------------------------------- *)
    48 (* CURRENT LIMITATIONS                                                       *)
    49 (*                                                                           *)
    50 (* 'refute' currently accepts formulas of higher-order predicate logic (with *)
    51 (* equality), including free/bound/schematic variables, lambda abstractions, *)
    52 (* sets and set membership, "arbitrary", "The", "Eps", records and           *)
    53 (* inductively defined sets.  Constants are unfolded automatically, and sort *)
    54 (* axioms are added as well.  Other, user-asserted axioms however are        *)
    55 (* ignored.  Inductive datatypes and recursive functions are supported, but  *)
    56 (* may lead to spurious countermodels.                                       *)
    57 (*                                                                           *)
    58 (* The (space) complexity of the algorithm is non-elementary.                *)
    59 (*                                                                           *)
    60 (* Schematic type variables are not supported.                               *)
    61 (* ------------------------------------------------------------------------- *)
    62 
    63 (* ------------------------------------------------------------------------- *)
    64 (* PARAMETERS                                                                *)
    65 (*                                                                           *)
    66 (* The following global parameters are currently supported (and required):   *)
    67 (*                                                                           *)
    68 (* Name          Type    Description                                         *)
    69 (*                                                                           *)
    70 (* "minsize"     int     Only search for models with size at least           *)
    71 (*                       'minsize'.                                          *)
    72 (* "maxsize"     int     If >0, only search for models with size at most     *)
    73 (*                       'maxsize'.                                          *)
    74 (* "maxvars"     int     If >0, use at most 'maxvars' boolean variables      *)
    75 (*                       when transforming the term into a propositional     *)
    76 (*                       formula.                                            *)
    77 (* "maxtime"     int     If >0, terminate after at most 'maxtime' seconds.   *)
    78 (*                       This value is ignored under some ML compilers.      *)
    79 (* "satsolver"   string  Name of the SAT solver to be used.                  *)
    80 (*                                                                           *)
    81 (* See 'HOL/SAT.thy' for default values.                                     *)
    82 (*                                                                           *)
    83 (* The size of particular types can be specified in the form type=size       *)
    84 (* (where 'type' is a string, and 'size' is an int).  Examples:              *)
    85 (* "'a"=1                                                                    *)
    86 (* "List.list"=2                                                             *)
    87 (* ------------------------------------------------------------------------- *)
    88 
    89 (* ------------------------------------------------------------------------- *)
    90 (* FILES                                                                     *)
    91 (*                                                                           *)
    92 (* HOL/Tools/prop_logic.ML    Propositional logic                            *)
    93 (* HOL/Tools/sat_solver.ML    SAT solvers                                    *)
    94 (* HOL/Tools/refute.ML        Translation HOL -> propositional logic and     *)
    95 (*                            Boolean assignment -> HOL model                *)
    96 (* HOL/Tools/refute_isar.ML   Adds 'refute'/'refute_params' to Isabelle's    *)
    97 (*                            syntax                                         *)
    98 (* HOL/Refute.thy             This file: loads the ML files, basic setup,    *)
    99 (*                            documentation                                  *)
   100 (* HOL/SAT.thy                Sets default parameters                        *)
   101 (* HOL/ex/RefuteExamples.thy  Examples                                       *)
   102 (* ------------------------------------------------------------------------- *)
   103 \end{verbatim}
   104 *}
   105 
   106 end