src/HOL/Refute.thy
author webertj
Thu Mar 11 13:03:31 2004 +0100 (2004-03-11)
changeset 14463 ed09706ecc5d
parent 14457 6d5d6e78d851
child 14589 feae7b5fd425
permissions -rw-r--r--
Documentation updated
     1 (*  Title:      HOL/Refute.thy
     2     ID:         $Id$
     3     Author:     Tjark Weber
     4     Copyright   2003-2004
     5 
     6 Basic setup and documentation for the 'refute' (and 'refute_params') command.
     7 *)
     8 
     9 (* ------------------------------------------------------------------------- *)
    10 (* REFUTE                                                                    *)
    11 (*                                                                           *)
    12 (* We use a SAT solver to search for a (finite) model that refutes a given   *)
    13 (* HOL formula.                                                              *)
    14 (* ------------------------------------------------------------------------- *)
    15 
    16 (* ------------------------------------------------------------------------- *)
    17 (* NOTE                                                                      *)
    18 (*                                                                           *)
    19 (* I strongly recommend that you install a stand-alone SAT solver if you     *)
    20 (* want to use 'refute'.  For details see 'HOL/Tools/sat_solver.ML'.  If you *)
    21 (* have installed ZChaff, simply set 'ZCHAFF_HOME' in 'etc/settings'.        *)
    22 (* ------------------------------------------------------------------------- *)
    23 
    24 (* ------------------------------------------------------------------------- *)
    25 (* USAGE                                                                     *)
    26 (*                                                                           *)
    27 (* See the file 'HOL/ex/Refute_Examples.thy' for examples.  The supported    *)
    28 (* parameters are explained below.                                           *)
    29 (* ------------------------------------------------------------------------- *)
    30 
    31 (* ------------------------------------------------------------------------- *)
    32 (* CURRENT LIMITATIONS                                                       *)
    33 (*                                                                           *)
    34 (* 'refute' currently accepts formulas of higher-order predicate logic (with *)
    35 (* equality), including free/bound/schematic variables, lambda abstractions, *)
    36 (* sets and set membership, "arbitrary", "The", and "Eps".  Constants for    *)
    37 (* which a defining equation exists are unfolded automatically.  Non-        *)
    38 (* recursive inductive datatypes are supported.                              *)
    39 (*                                                                           *)
    40 (* The (space) complexity of the algorithm is exponential in both the length *)
    41 (* of the formula and the size of the model.                                 *)
    42 (*                                                                           *)
    43 (* NOT (YET) SUPPORTED ARE                                                   *)
    44 (*                                                                           *)
    45 (* - schematic type variables                                                *)
    46 (* - axioms, sorts                                                           *)
    47 (* - type constructors other than bool, =>, set, non-recursive IDTs          *)
    48 (* - inductively defined sets                                                *)
    49 (* - recursive functions                                                     *)
    50 (* - ...                                                                     *)
    51 (* ------------------------------------------------------------------------- *)
    52 
    53 (* ------------------------------------------------------------------------- *)
    54 (* PARAMETERS                                                                *)
    55 (*                                                                           *)
    56 (* The following global parameters are currently supported (and required):   *)
    57 (*                                                                           *)
    58 (* Name          Type    Description                                         *)
    59 (*                                                                           *)
    60 (* "minsize"     int     Only search for models with size at least           *)
    61 (*                       'minsize'.                                          *)
    62 (* "maxsize"     int     If >0, only search for models with size at most     *)
    63 (*                       'maxsize'.                                          *)
    64 (* "maxvars"     int     If >0, use at most 'maxvars' boolean variables      *)
    65 (*                       when transforming the term into a propositional     *)
    66 (*                       formula.                                            *)
    67 (* "satsolver"   string  Name of the SAT solver to be used.                  *)
    68 (*                                                                           *)
    69 (* See 'HOL/Main.thy' for default values.                                    *)
    70 (* ------------------------------------------------------------------------- *)
    71 
    72 (* ------------------------------------------------------------------------- *)
    73 (* FILES                                                                     *)
    74 (*                                                                           *)
    75 (* HOL/Tools/prop_logic.ML    Propositional logic                            *)
    76 (* HOL/Tools/sat_solver.ML    SAT solvers                                    *)
    77 (* HOL/Tools/refute.ML        Translation HOL -> propositional logic and     *)
    78 (*                            boolean assignment -> HOL model                *)
    79 (* HOL/Tools/refute_isar.ML   Adds 'refute'/'refute_params' to Isabelle's    *)
    80 (*                            syntax                                         *)
    81 (* HOL/Refute.thy             This file: loads the ML files, basic setup,    *)
    82 (*                            documentation                                  *)
    83 (* HOL/Main.thy               Sets default parameters                        *)
    84 (* HOL/ex/RefuteExamples.thy  Examples                                       *)
    85 (* ------------------------------------------------------------------------- *)
    86 
    87 header {* Refute *}
    88 
    89 theory Refute = Map
    90 
    91 files "Tools/prop_logic.ML"
    92       "Tools/sat_solver.ML"
    93       "Tools/refute.ML"
    94       "Tools/refute_isar.ML":
    95 
    96 use "Tools/prop_logic.ML"
    97 use "Tools/sat_solver.ML"
    98 use "Tools/refute.ML"
    99 use "Tools/refute_isar.ML"
   100 
   101 setup Refute.setup
   102 
   103 end