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