src/HOL/Library/Refute.thy
author Manuel Eberl <eberlm@in.tum.de>
Mon Mar 26 16:14:16 2018 +0200 (18 months ago)
changeset 67951 655aa11359dc
parent 63432 ba7901e94e7b
child 69605 a96320074298
permissions -rw-r--r--
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
wenzelm@50530
     1
(*  Title:      HOL/Library/Refute.thy
webertj@14350
     2
    Author:     Tjark Weber
webertj@22058
     3
    Copyright   2003-2007
webertj@14350
     4
webertj@14350
     5
Basic setup and documentation for the 'refute' (and 'refute_params') command.
webertj@14350
     6
*)
webertj@14350
     7
wenzelm@60500
     8
section \<open>Refute\<close>
wenzelm@14589
     9
nipkow@15131
    10
theory Refute
blanchet@54556
    11
imports Main
wenzelm@63432
    12
keywords
wenzelm@63432
    13
  "refute" :: diag and
wenzelm@63432
    14
  "refute_params" :: thy_decl
nipkow@15131
    15
begin
wenzelm@14589
    16
blanchet@49985
    17
ML_file "refute.ML"
wenzelm@14589
    18
wenzelm@46960
    19
refute_params
wenzelm@46960
    20
 [itself = 1,
wenzelm@46960
    21
  minsize = 1,
wenzelm@46960
    22
  maxsize = 8,
wenzelm@46960
    23
  maxvars = 10000,
wenzelm@46960
    24
  maxtime = 60,
wenzelm@46960
    25
  satsolver = auto,
wenzelm@46960
    26
  no_assms = false]
wenzelm@46960
    27
wenzelm@60500
    28
text \<open>
wenzelm@14589
    29
\small
wenzelm@14589
    30
\begin{verbatim}
webertj@14350
    31
(* ------------------------------------------------------------------------- *)
webertj@14350
    32
(* REFUTE                                                                    *)
webertj@14350
    33
(*                                                                           *)
webertj@14350
    34
(* We use a SAT solver to search for a (finite) model that refutes a given   *)
webertj@14350
    35
(* HOL formula.                                                              *)
webertj@14350
    36
(* ------------------------------------------------------------------------- *)
webertj@14350
    37
webertj@14350
    38
(* ------------------------------------------------------------------------- *)
webertj@14457
    39
(* NOTE                                                                      *)
webertj@14350
    40
(*                                                                           *)
webertj@14457
    41
(* I strongly recommend that you install a stand-alone SAT solver if you     *)
webertj@14463
    42
(* want to use 'refute'.  For details see 'HOL/Tools/sat_solver.ML'.  If you *)
webertj@15293
    43
(* have installed (a supported version of) zChaff, simply set 'ZCHAFF_HOME'  *)
webertj@15293
    44
(* in 'etc/settings'.                                                        *)
webertj@14350
    45
(* ------------------------------------------------------------------------- *)
webertj@14350
    46
webertj@14350
    47
(* ------------------------------------------------------------------------- *)
webertj@14350
    48
(* USAGE                                                                     *)
webertj@14350
    49
(*                                                                           *)
webertj@14350
    50
(* See the file 'HOL/ex/Refute_Examples.thy' for examples.  The supported    *)
webertj@14350
    51
(* parameters are explained below.                                           *)
webertj@14350
    52
(* ------------------------------------------------------------------------- *)
webertj@14350
    53
webertj@14350
    54
(* ------------------------------------------------------------------------- *)
webertj@14350
    55
(* CURRENT LIMITATIONS                                                       *)
webertj@14350
    56
(*                                                                           *)
webertj@14350
    57
(* 'refute' currently accepts formulas of higher-order predicate logic (with *)
webertj@14350
    58
(* equality), including free/bound/schematic variables, lambda abstractions, *)
webertj@16870
    59
(* sets and set membership, "arbitrary", "The", "Eps", records and           *)
webertj@22058
    60
(* inductively defined sets.  Constants are unfolded automatically, and sort *)
webertj@22058
    61
(* axioms are added as well.  Other, user-asserted axioms however are        *)
webertj@22058
    62
(* ignored.  Inductive datatypes and recursive functions are supported, but  *)
webertj@22058
    63
(* may lead to spurious countermodels.                                       *)
webertj@14463
    64
(*                                                                           *)
webertj@14808
    65
(* The (space) complexity of the algorithm is non-elementary.                *)
webertj@14350
    66
(*                                                                           *)
webertj@16870
    67
(* Schematic type variables are not supported.                               *)
webertj@14350
    68
(* ------------------------------------------------------------------------- *)
webertj@14350
    69
webertj@14350
    70
(* ------------------------------------------------------------------------- *)
webertj@14350
    71
(* PARAMETERS                                                                *)
webertj@14350
    72
(*                                                                           *)
blanchet@34120
    73
(* The following global parameters are currently supported (and required,    *)
blanchet@34120
    74
(* except for "expect"):                                                     *)
webertj@14350
    75
(*                                                                           *)
webertj@14350
    76
(* Name          Type    Description                                         *)
webertj@14350
    77
(*                                                                           *)
webertj@14350
    78
(* "minsize"     int     Only search for models with size at least           *)
webertj@14350
    79
(*                       'minsize'.                                          *)
webertj@14350
    80
(* "maxsize"     int     If >0, only search for models with size at most     *)
webertj@14350
    81
(*                       'maxsize'.                                          *)
webertj@14350
    82
(* "maxvars"     int     If >0, use at most 'maxvars' boolean variables      *)
webertj@14350
    83
(*                       when transforming the term into a propositional     *)
webertj@14350
    84
(*                       formula.                                            *)
webertj@14808
    85
(* "maxtime"     int     If >0, terminate after at most 'maxtime' seconds.   *)
webertj@14808
    86
(*                       This value is ignored under some ML compilers.      *)
webertj@14457
    87
(* "satsolver"   string  Name of the SAT solver to be used.                  *)
blanchet@34120
    88
(* "no_assms"    bool    If "true", assumptions in structured proofs are     *)
blanchet@34120
    89
(*                       not considered.                                     *)
blanchet@34120
    90
(* "expect"      string  Expected result ("genuine", "potential", "none", or *)
blanchet@34120
    91
(*                       "unknown").                                         *)
webertj@14457
    92
(*                                                                           *)
webertj@14808
    93
(* The size of particular types can be specified in the form type=size       *)
webertj@14808
    94
(* (where 'type' is a string, and 'size' is an int).  Examples:              *)
webertj@14808
    95
(* "'a"=1                                                                    *)
webertj@14808
    96
(* "List.list"=2                                                             *)
webertj@14350
    97
(* ------------------------------------------------------------------------- *)
webertj@14350
    98
webertj@14350
    99
(* ------------------------------------------------------------------------- *)
webertj@14350
   100
(* FILES                                                                     *)
webertj@14350
   101
(*                                                                           *)
wenzelm@39048
   102
(* HOL/Tools/prop_logic.ML     Propositional logic                           *)
wenzelm@39048
   103
(* HOL/Tools/sat_solver.ML     SAT solvers                                   *)
wenzelm@39048
   104
(* HOL/Tools/refute.ML         Translation HOL -> propositional logic and    *)
wenzelm@39048
   105
(*                             Boolean assignment -> HOL model               *)
wenzelm@39048
   106
(* HOL/Refute.thy              This file: loads the ML files, basic setup,   *)
wenzelm@39048
   107
(*                             documentation                                 *)
wenzelm@39048
   108
(* HOL/SAT.thy                 Sets default parameters                       *)
wenzelm@39048
   109
(* HOL/ex/Refute_Examples.thy  Examples                                      *)
webertj@14350
   110
(* ------------------------------------------------------------------------- *)
wenzelm@14589
   111
\end{verbatim}
wenzelm@60500
   112
\<close>
webertj@14350
   113
webertj@14350
   114
end