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