author  wenzelm 
Wed, 17 Jun 2015 11:03:05 +0200  
changeset 60500  903bb1495239 
parent 58881  b9556a055632 
child 63432  ba7901e94e7b 
permissions  rwrr 
50530  1 
(* Title: HOL/Library/Refute.thy 
14350  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 

60500  8 
section \<open>Refute\<close> 
14589  9 

15131  10 
theory Refute 
54556  11 
imports Main 
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 

49985
5b4b0e4e5205
moved Refute to "HOL/Library" to speed up building "Main" even more
blanchet
parents:
48891
diff
changeset

15 
ML_file "refute.ML" 
14589  16 

46960  17 
refute_params 
18 
[itself = 1, 

19 
minsize = 1, 

20 
maxsize = 8, 

21 
maxvars = 10000, 

22 
maxtime = 60, 

23 
satsolver = auto, 

24 
no_assms = false] 

25 

60500  26 
text \<open> 
14589  27 
\small 
28 
\begin{verbatim} 

14350  29 
(*  *) 
30 
(* REFUTE *) 

31 
(* *) 

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

33 
(* HOL formula. *) 

34 
(*  *) 

35 

36 
(*  *) 

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

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

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

45 
(*  *) 

46 
(* USAGE *) 

47 
(* *) 

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

49 
(* parameters are explained below. *) 

50 
(*  *) 

51 

52 
(*  *) 

53 
(* CURRENT LIMITATIONS *) 

54 
(* *) 

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

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

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

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

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

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

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

68 
(*  *) 

69 
(* PARAMETERS *) 

70 
(* *) 

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

71 
(* 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

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

75 
(* *) 

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

77 
(* 'minsize'. *) 

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

79 
(* 'maxsize'. *) 

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

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

82 
(* formula. *) 

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

14457  85 
(* "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

86 
(* "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

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

88 
(* "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

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

93 
(* "'a"=1 *) 

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

14350  95 
(*  *) 
96 

97 
(*  *) 

98 
(* FILES *) 

99 
(* *) 

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

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

103 
(* Boolean assignment > HOL model *) 

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

105 
(* documentation *) 

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

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

14350  108 
(*  *) 
14589  109 
\end{verbatim} 
60500  110 
\<close> 
14350  111 

112 
end 