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