src/HOL/Refute.thy
author paulson
Tue Jun 28 15:27:45 2005 +0200 (2005-06-28)
changeset 16587 b34c8aa657a5
parent 16417 9bc16273c2d4
child 16870 a1155e140597
permissions -rw-r--r--
Constant "If" is now local
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
wenzelm@14589
     9
header {* Refute *}
wenzelm@14589
    10
nipkow@15131
    11
theory Refute
nipkow@15140
    12
imports Map
haftmann@16417
    13
uses "Tools/prop_logic.ML"
wenzelm@14589
    14
      "Tools/sat_solver.ML"
wenzelm@14589
    15
      "Tools/refute.ML"
nipkow@15131
    16
      "Tools/refute_isar.ML"
nipkow@15131
    17
begin
wenzelm@14589
    18
wenzelm@14589
    19
setup Refute.setup
wenzelm@14589
    20
wenzelm@14589
    21
text {*
wenzelm@14589
    22
\small
wenzelm@14589
    23
\begin{verbatim}
webertj@14350
    24
(* ------------------------------------------------------------------------- *)
webertj@14350
    25
(* REFUTE                                                                    *)
webertj@14350
    26
(*                                                                           *)
webertj@14350
    27
(* We use a SAT solver to search for a (finite) model that refutes a given   *)
webertj@14350
    28
(* HOL formula.                                                              *)
webertj@14350
    29
(* ------------------------------------------------------------------------- *)
webertj@14350
    30
webertj@14350
    31
(* ------------------------------------------------------------------------- *)
webertj@14457
    32
(* NOTE                                                                      *)
webertj@14350
    33
(*                                                                           *)
webertj@14457
    34
(* I strongly recommend that you install a stand-alone SAT solver if you     *)
webertj@14463
    35
(* want to use 'refute'.  For details see 'HOL/Tools/sat_solver.ML'.  If you *)
webertj@15293
    36
(* have installed (a supported version of) zChaff, simply set 'ZCHAFF_HOME'  *)
webertj@15293
    37
(* in 'etc/settings'.                                                        *)
webertj@14350
    38
(* ------------------------------------------------------------------------- *)
webertj@14350
    39
webertj@14350
    40
(* ------------------------------------------------------------------------- *)
webertj@14350
    41
(* USAGE                                                                     *)
webertj@14350
    42
(*                                                                           *)
webertj@14350
    43
(* See the file 'HOL/ex/Refute_Examples.thy' for examples.  The supported    *)
webertj@14350
    44
(* parameters are explained below.                                           *)
webertj@14350
    45
(* ------------------------------------------------------------------------- *)
webertj@14350
    46
webertj@14350
    47
(* ------------------------------------------------------------------------- *)
webertj@14350
    48
(* CURRENT LIMITATIONS                                                       *)
webertj@14350
    49
(*                                                                           *)
webertj@14350
    50
(* 'refute' currently accepts formulas of higher-order predicate logic (with *)
webertj@14350
    51
(* equality), including free/bound/schematic variables, lambda abstractions, *)
webertj@14808
    52
(* sets and set membership, "arbitrary", "The", and "Eps".  Defining         *)
webertj@14808
    53
(* equations for constants are added automatically.  Inductive datatypes are *)
webertj@14808
    54
(* supported, but may lead to spurious countermodels.                        *)
webertj@14463
    55
(*                                                                           *)
webertj@14808
    56
(* The (space) complexity of the algorithm is non-elementary.                *)
webertj@14350
    57
(*                                                                           *)
webertj@14350
    58
(* NOT (YET) SUPPORTED ARE                                                   *)
webertj@14350
    59
(*                                                                           *)
webertj@14350
    60
(* - schematic type variables                                                *)
webertj@14463
    61
(* - axioms, sorts                                                           *)
webertj@14463
    62
(* - inductively defined sets                                                *)
webertj@14808
    63
(* - recursive functions on IDTs (case, recursion operators, size)           *)
webertj@14463
    64
(* - ...                                                                     *)
webertj@14350
    65
(* ------------------------------------------------------------------------- *)
webertj@14350
    66
webertj@14350
    67
(* ------------------------------------------------------------------------- *)
webertj@14350
    68
(* PARAMETERS                                                                *)
webertj@14350
    69
(*                                                                           *)
webertj@14350
    70
(* The following global parameters are currently supported (and required):   *)
webertj@14350
    71
(*                                                                           *)
webertj@14350
    72
(* Name          Type    Description                                         *)
webertj@14350
    73
(*                                                                           *)
webertj@14350
    74
(* "minsize"     int     Only search for models with size at least           *)
webertj@14350
    75
(*                       'minsize'.                                          *)
webertj@14350
    76
(* "maxsize"     int     If >0, only search for models with size at most     *)
webertj@14350
    77
(*                       'maxsize'.                                          *)
webertj@14350
    78
(* "maxvars"     int     If >0, use at most 'maxvars' boolean variables      *)
webertj@14350
    79
(*                       when transforming the term into a propositional     *)
webertj@14350
    80
(*                       formula.                                            *)
webertj@14808
    81
(* "maxtime"     int     If >0, terminate after at most 'maxtime' seconds.   *)
webertj@14808
    82
(*                       This value is ignored under some ML compilers.      *)
webertj@14457
    83
(* "satsolver"   string  Name of the SAT solver to be used.                  *)
webertj@14457
    84
(*                                                                           *)
webertj@14457
    85
(* See 'HOL/Main.thy' for default values.                                    *)
webertj@14808
    86
(*                                                                           *)
webertj@14808
    87
(* The size of particular types can be specified in the form type=size       *)
webertj@14808
    88
(* (where 'type' is a string, and 'size' is an int).  Examples:              *)
webertj@14808
    89
(* "'a"=1                                                                    *)
webertj@14808
    90
(* "List.list"=2                                                             *)
webertj@14350
    91
(* ------------------------------------------------------------------------- *)
webertj@14350
    92
webertj@14350
    93
(* ------------------------------------------------------------------------- *)
webertj@14350
    94
(* FILES                                                                     *)
webertj@14350
    95
(*                                                                           *)
webertj@14457
    96
(* HOL/Tools/prop_logic.ML    Propositional logic                            *)
webertj@14457
    97
(* HOL/Tools/sat_solver.ML    SAT solvers                                    *)
webertj@14457
    98
(* HOL/Tools/refute.ML        Translation HOL -> propositional logic and     *)
webertj@14808
    99
(*                            Boolean assignment -> HOL model                *)
webertj@14350
   100
(* HOL/Tools/refute_isar.ML   Adds 'refute'/'refute_params' to Isabelle's    *)
webertj@14457
   101
(*                            syntax                                         *)
webertj@14457
   102
(* HOL/Refute.thy             This file: loads the ML files, basic setup,    *)
webertj@14457
   103
(*                            documentation                                  *)
webertj@14457
   104
(* HOL/Main.thy               Sets default parameters                        *)
webertj@14457
   105
(* HOL/ex/RefuteExamples.thy  Examples                                       *)
webertj@14350
   106
(* ------------------------------------------------------------------------- *)
wenzelm@14589
   107
\end{verbatim}
wenzelm@14589
   108
*}
webertj@14350
   109
webertj@14350
   110
end