author  haftmann 
Fri, 17 Jun 2005 16:12:49 +0200  
changeset 16417  9bc16273c2d4 
parent 15293  7797a04cc188 
child 16870  a1155e140597 
permissions  rwrr 
14350  1 
(* Title: HOL/Refute.thy 
2 
ID: $Id$ 

3 
Author: Tjark Weber 

4 
Copyright 20032004 

5 

6 
Basic setup and documentation for the 'refute' (and 'refute_params') command. 

7 
*) 

8 

14589  9 
header {* Refute *} 
10 

15131  11 
theory Refute 
15140  12 
imports Map 
16417  13 
uses "Tools/prop_logic.ML" 
14589  14 
"Tools/sat_solver.ML" 
15 
"Tools/refute.ML" 

15131  16 
"Tools/refute_isar.ML" 
17 
begin 

14589  18 

19 
setup Refute.setup 

20 

21 
text {* 

22 
\small 

23 
\begin{verbatim} 

14350  24 
(*  *) 
25 
(* REFUTE *) 

26 
(* *) 

27 
(* We use a SAT solver to search for a (finite) model that refutes a given *) 

28 
(* HOL formula. *) 

29 
(*  *) 

30 

31 
(*  *) 

14457  32 
(* NOTE *) 
14350  33 
(* *) 
14457  34 
(* I strongly recommend that you install a standalone SAT solver if you *) 
14463  35 
(* want to use 'refute'. For details see 'HOL/Tools/sat_solver.ML'. If you *) 
15293
7797a04cc188
removed explicit mentioning of zChaffs version number
webertj
parents:
15140
diff
changeset

36 
(* have installed (a supported version of) zChaff, simply set 'ZCHAFF_HOME' *) 
7797a04cc188
removed explicit mentioning of zChaffs version number
webertj
parents:
15140
diff
changeset

37 
(* in 'etc/settings'. *) 
14350  38 
(*  *) 
39 

40 
(*  *) 

41 
(* USAGE *) 

42 
(* *) 

43 
(* See the file 'HOL/ex/Refute_Examples.thy' for examples. The supported *) 

44 
(* parameters are explained below. *) 

45 
(*  *) 

46 

47 
(*  *) 

48 
(* CURRENT LIMITATIONS *) 

49 
(* *) 

50 
(* 'refute' currently accepts formulas of higherorder predicate logic (with *) 

51 
(* equality), including free/bound/schematic variables, lambda abstractions, *) 

14808  52 
(* sets and set membership, "arbitrary", "The", and "Eps". Defining *) 
53 
(* equations for constants are added automatically. Inductive datatypes are *) 

54 
(* supported, but may lead to spurious countermodels. *) 

14463  55 
(* *) 
14808  56 
(* The (space) complexity of the algorithm is nonelementary. *) 
14350  57 
(* *) 
58 
(* NOT (YET) SUPPORTED ARE *) 

59 
(* *) 

60 
(*  schematic type variables *) 

14463  61 
(*  axioms, sorts *) 
62 
(*  inductively defined sets *) 

14808  63 
(*  recursive functions on IDTs (case, recursion operators, size) *) 
14463  64 
(*  ... *) 
14350  65 
(*  *) 
66 

67 
(*  *) 

68 
(* PARAMETERS *) 

69 
(* *) 

70 
(* The following global parameters are currently supported (and required): *) 

71 
(* *) 

72 
(* Name Type Description *) 

73 
(* *) 

74 
(* "minsize" int Only search for models with size at least *) 

75 
(* 'minsize'. *) 

76 
(* "maxsize" int If >0, only search for models with size at most *) 

77 
(* 'maxsize'. *) 

78 
(* "maxvars" int If >0, use at most 'maxvars' boolean variables *) 

79 
(* when transforming the term into a propositional *) 

80 
(* formula. *) 

14808  81 
(* "maxtime" int If >0, terminate after at most 'maxtime' seconds. *) 
82 
(* This value is ignored under some ML compilers. *) 

14457  83 
(* "satsolver" string Name of the SAT solver to be used. *) 
84 
(* *) 

85 
(* See 'HOL/Main.thy' for default values. *) 

14808  86 
(* *) 
87 
(* The size of particular types can be specified in the form type=size *) 

88 
(* (where 'type' is a string, and 'size' is an int). Examples: *) 

89 
(* "'a"=1 *) 

90 
(* "List.list"=2 *) 

14350  91 
(*  *) 
92 

93 
(*  *) 

94 
(* FILES *) 

95 
(* *) 

14457  96 
(* HOL/Tools/prop_logic.ML Propositional logic *) 
97 
(* HOL/Tools/sat_solver.ML SAT solvers *) 

98 
(* HOL/Tools/refute.ML Translation HOL > propositional logic and *) 

14808  99 
(* Boolean assignment > HOL model *) 
14350  100 
(* HOL/Tools/refute_isar.ML Adds 'refute'/'refute_params' to Isabelle's *) 
14457  101 
(* syntax *) 
102 
(* HOL/Refute.thy This file: loads the ML files, basic setup, *) 

103 
(* documentation *) 

104 
(* HOL/Main.thy Sets default parameters *) 

105 
(* HOL/ex/RefuteExamples.thy Examples *) 

14350  106 
(*  *) 
14589  107 
\end{verbatim} 
108 
*} 

14350  109 

110 
end 