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