author  webertj 
Fri, 19 Oct 2012 15:12:52 +0200  
changeset 49962  a8cc904a6820 
parent 48891  c0eafbd55de3 
permissions  rwrr 
14350  1 
(* Title: HOL/Refute.thy 
2 
Author: Tjark Weber 

22058
49faa8c7a5d9
updated to mention the automatic unfolding of constants
webertj
parents:
21332
diff
changeset

3 
Copyright 20032007 
14350  4 

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

6 
*) 

7 

14589  8 
header {* Refute *} 
9 

15131  10 
theory Refute 
40178
00152d17855b
reverted e7a80c6752c9  there's not much point in putting a diagnosis tool (as opposed to a proof method) in Plain, but more importantly Sledgehammer must be in Main to use SMT solvers
blanchet
parents:
40121
diff
changeset

11 
imports Hilbert_Choice List Sledgehammer 
46950
d0181abdbdac
declare command keywords via theory header, including strict checking outside Pure;
wenzelm
parents:
40178
diff
changeset

12 
keywords "refute" :: diag and "refute_params" :: thy_decl 
15131  13 
begin 
14589  14 

48891  15 
ML_file "Tools/refute.ML" 
14589  16 
setup Refute.setup 
17 

46960  18 
refute_params 
19 
[itself = 1, 

20 
minsize = 1, 

21 
maxsize = 8, 

22 
maxvars = 10000, 

23 
maxtime = 60, 

24 
satsolver = auto, 

25 
no_assms = false] 

26 

14589  27 
text {* 
28 
\small 

29 
\begin{verbatim} 

14350  30 
(*  *) 
31 
(* REFUTE *) 

32 
(* *) 

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

34 
(* HOL formula. *) 

35 
(*  *) 

36 

37 
(*  *) 

14457  38 
(* NOTE *) 
14350  39 
(* *) 
14457  40 
(* I strongly recommend that you install a standalone SAT solver if you *) 
14463  41 
(* 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

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

43 
(* in 'etc/settings'. *) 
14350  44 
(*  *) 
45 

46 
(*  *) 

47 
(* USAGE *) 

48 
(* *) 

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

50 
(* parameters are explained below. *) 

51 
(*  *) 

52 

53 
(*  *) 

54 
(* CURRENT LIMITATIONS *) 

55 
(* *) 

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

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

16870  58 
(* sets and set membership, "arbitrary", "The", "Eps", records and *) 
22058
49faa8c7a5d9
updated to mention the automatic unfolding of constants
webertj
parents:
21332
diff
changeset

59 
(* inductively defined sets. Constants are unfolded automatically, and sort *) 
49faa8c7a5d9
updated to mention the automatic unfolding of constants
webertj
parents:
21332
diff
changeset

60 
(* axioms are added as well. Other, userasserted axioms however are *) 
49faa8c7a5d9
updated to mention the automatic unfolding of constants
webertj
parents:
21332
diff
changeset

61 
(* ignored. Inductive datatypes and recursive functions are supported, but *) 
49faa8c7a5d9
updated to mention the automatic unfolding of constants
webertj
parents:
21332
diff
changeset

62 
(* may lead to spurious countermodels. *) 
14463  63 
(* *) 
14808  64 
(* The (space) complexity of the algorithm is nonelementary. *) 
14350  65 
(* *) 
16870  66 
(* Schematic type variables are not supported. *) 
14350  67 
(*  *) 
68 

69 
(*  *) 

70 
(* PARAMETERS *) 

71 
(* *) 

34120
f9920a3ddf50
added "no_assms" option to Refute, and include structured proof assumptions by default;
blanchet
parents:
34018
diff
changeset

72 
(* The following global parameters are currently supported (and required, *) 
f9920a3ddf50
added "no_assms" option to Refute, and include structured proof assumptions by default;
blanchet
parents:
34018
diff
changeset

73 
(* except for "expect"): *) 
14350  74 
(* *) 
75 
(* Name Type Description *) 

76 
(* *) 

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

78 
(* 'minsize'. *) 

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

80 
(* 'maxsize'. *) 

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

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

83 
(* formula. *) 

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

14457  86 
(* "satsolver" string Name of the SAT solver to be used. *) 
34120
f9920a3ddf50
added "no_assms" option to Refute, and include structured proof assumptions by default;
blanchet
parents:
34018
diff
changeset

87 
(* "no_assms" bool If "true", assumptions in structured proofs are *) 
f9920a3ddf50
added "no_assms" option to Refute, and include structured proof assumptions by default;
blanchet
parents:
34018
diff
changeset

88 
(* not considered. *) 
f9920a3ddf50
added "no_assms" option to Refute, and include structured proof assumptions by default;
blanchet
parents:
34018
diff
changeset

89 
(* "expect" string Expected result ("genuine", "potential", "none", or *) 
f9920a3ddf50
added "no_assms" option to Refute, and include structured proof assumptions by default;
blanchet
parents:
34018
diff
changeset

90 
(* "unknown"). *) 
14457  91 
(* *) 
14808  92 
(* The size of particular types can be specified in the form type=size *) 
93 
(* (where 'type' is a string, and 'size' is an int). Examples: *) 

94 
(* "'a"=1 *) 

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

14350  96 
(*  *) 
97 

98 
(*  *) 

99 
(* FILES *) 

100 
(* *) 

39048  101 
(* HOL/Tools/prop_logic.ML Propositional logic *) 
102 
(* HOL/Tools/sat_solver.ML SAT solvers *) 

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

104 
(* Boolean assignment > HOL model *) 

105 
(* HOL/Refute.thy This file: loads the ML files, basic setup, *) 

106 
(* documentation *) 

107 
(* HOL/SAT.thy Sets default parameters *) 

108 
(* HOL/ex/Refute_Examples.thy Examples *) 

14350  109 
(*  *) 
14589  110 
\end{verbatim} 
111 
*} 

14350  112 

113 
end 