src/HOL/Refute.thy
author webertj
Sat Jan 10 13:35:10 2004 +0100 (2004-01-10)
changeset 14350 41b32020d0b3
child 14457 6d5d6e78d851
permissions -rw-r--r--
Adding 'refute' to HOL.
     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 (* INSTALLATION                                                              *)
    18 (*                                                                           *)
    19 (* 1. Install a stand-alone SAT solver.  The default parameters in           *)
    20 (*    'HOL/Main.thy' assume that ZChaff 2003.12.04 (available for Solaris/   *)
    21 (*    Linux/Cygwin/Windows at http://ee.princeton.edu/~chaff/zchaff.php) is  *)
    22 (*    installed as '$HOME/bin/zchaff'.  If you want to use a different SAT   *)
    23 (*    solver (or install ZChaff to a different location), you will need to   *)
    24 (*    modify at least the values for 'command' and (probably) 'success'.     *)
    25 (*                                                                           *)
    26 (* 2. That's it. You can now use the 'refute' command in your own theories.  *)
    27 (* ------------------------------------------------------------------------- *)
    28 
    29 (* ------------------------------------------------------------------------- *)
    30 (* USAGE                                                                     *)
    31 (*                                                                           *)
    32 (* See the file 'HOL/ex/Refute_Examples.thy' for examples.  The supported    *)
    33 (* parameters are explained below.                                           *)
    34 (* ------------------------------------------------------------------------- *)
    35 
    36 (* ------------------------------------------------------------------------- *)
    37 (* CURRENT LIMITATIONS                                                       *)
    38 (*                                                                           *)
    39 (* 'refute' currently accepts formulas of higher-order predicate logic (with *)
    40 (* equality), including free/bound/schematic variables, lambda abstractions, *)
    41 (* sets and set membership.                                                  *)
    42 (*                                                                           *)
    43 (* NOT (YET) SUPPORTED ARE                                                   *)
    44 (*                                                                           *)
    45 (* - schematic type variables                                                *)
    46 (* - type constructors other than =>, set, unit, and inductive datatypes     *)
    47 (* - constants, including constructors of inductive datatypes and recursive  *)
    48 (*   functions on inductive datatypes                                        *)
    49 (*                                                                           *)
    50 (* Unfolding of constants currently needs to be done manually, e.g. using    *)
    51 (* 'apply (unfold xxx_def)'.                                                 *)
    52 (*                                                                           *)
    53 (* For formulas that contain (variables of) an inductive datatype, a         *)
    54 (* spurious countermodel may be returned.  Currently no warning is issued in *)
    55 (* this case.                                                                *)
    56 (* ------------------------------------------------------------------------- *)
    57 
    58 (* ------------------------------------------------------------------------- *)
    59 (* PARAMETERS                                                                *)
    60 (*                                                                           *)
    61 (* The following global parameters are currently supported (and required):   *)
    62 (*                                                                           *)
    63 (* Name          Type    Description                                         *)
    64 (*                                                                           *)
    65 (* "minsize"     int     Only search for models with size at least           *)
    66 (*                       'minsize'.                                          *)
    67 (* "maxsize"     int     If >0, only search for models with size at most     *)
    68 (*                       'maxsize'.                                          *)
    69 (* "maxvars"     int     If >0, use at most 'maxvars' boolean variables      *)
    70 (*                       when transforming the term into a propositional     *)
    71 (*                       formula.                                            *)
    72 (* "satfile"     string  Name of the file used to store the propositional    *)
    73 (*                       formula, i.e. the input to the SAT solver.          *)
    74 (* "satformat"   string  Format of the SAT solver's input file.  Must be     *)
    75 (*                       either "cnf", "defcnf", or "sat".  Since "sat" is   *)
    76 (*                       not supported by most SAT solvers, and "cnf" can    *)
    77 (*                       cause exponential blowup of the formula, "defcnf"   *)
    78 (*                       is recommended.                                     *)
    79 (* "resultfile"  string  Name of the file containing the SAT solver's        *)
    80 (*                       output.                                             *)
    81 (* "success"     string  Part of the line in the SAT solver's output that    *)
    82 (*                       precedes a list of integers representing the        *)
    83 (*                       satisfying assignment.                              *)
    84 (* "command"     string  System command used to execute the SAT solver.      *)
    85 (*                       Note that you if you change 'satfile' or            *)
    86 (*                       'resultfile', you will also need to change          *)
    87 (*                       'command'.                                          *)
    88 (* ------------------------------------------------------------------------- *)
    89 
    90 (* ------------------------------------------------------------------------- *)
    91 (* FILES                                                                     *)
    92 (*                                                                           *)
    93 (* HOL/Tools/refute.ML        Implementation of the algorithm.               *)
    94 (* HOL/Tools/refute_isar.ML   Adds 'refute'/'refute_params' to Isabelle's    *)
    95 (*                            syntax.                                        *)
    96 (* HOL/Refute.thy             This file. Loads the ML files, basic setup,    *)
    97 (*                            documentation.                                 *)
    98 (* HOL/Main.thy               Sets default parameters.                       *)
    99 (* HOL/ex/RefuteExamples.thy  Examples.                                      *)
   100 (* ------------------------------------------------------------------------- *)
   101 
   102 header {* Refute *}
   103 
   104 theory Refute = Map
   105 
   106 files "Tools/refute.ML"
   107       "Tools/refute_isar.ML":
   108 
   109 (* Setting up the 'refute' and 'refute\_params' commands *)
   110 
   111 use "Tools/refute.ML"
   112 use "Tools/refute_isar.ML"
   113 
   114 setup Refute.setup
   115 
   116 end