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