author  boehmes 
Fri, 29 Oct 2010 18:17:04 +0200  
changeset 40274  6486c610a549 
parent 40162  7f58a9a843c2 
child 40277  4e3a3461c1a6 
permissions  rwrr 
36898  1 
(* Title: HOL/SMT.thy 
2 
Author: Sascha Boehme, TU Muenchen 

3 
*) 

4 

5 
header {* Bindings to Satisfiability Modulo Theories (SMT) solvers *} 

6 

7 
theory SMT 

8 
imports List 

9 
uses 

39483
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
39298
diff
changeset

10 
"Tools/Datatype/datatype_selectors.ML" 
36898  11 
("Tools/SMT/smt_monomorph.ML") 
12 
("Tools/SMT/smt_normalize.ML") 

13 
("Tools/SMT/smt_translate.ML") 

14 
("Tools/SMT/smt_solver.ML") 

15 
("Tools/SMT/smtlib_interface.ML") 

16 
("Tools/SMT/z3_proof_parser.ML") 

17 
("Tools/SMT/z3_proof_tools.ML") 

18 
("Tools/SMT/z3_proof_literals.ML") 

19 
("Tools/SMT/z3_proof_reconstruction.ML") 

20 
("Tools/SMT/z3_model.ML") 

21 
("Tools/SMT/z3_interface.ML") 

40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

22 
("Tools/SMT/smt_setup_solvers.ML") 
36898  23 
begin 
24 

25 

26 

36902
c6bae4456741
use 'subsection' instead of 'section', to maintain 1 chapter per file in generated document
huffman
parents:
36899
diff
changeset

27 
subsection {* Triggers for quantifier instantiation *} 
36898  28 

29 
text {* 

30 
Some SMT solvers support triggers for quantifier instantiation. 

31 
Each trigger consists of one ore more patterns. A pattern may either 

37124  32 
be a list of positive subterms (each being tagged by "pat"), or a 
33 
list of negative subterms (each being tagged by "nopat"). 

34 

35 
When an SMT solver finds a term matching a positive pattern (a 

36 
pattern with positive subterms only), it instantiates the 

37 
corresponding quantifier accordingly. Negative patterns inhibit 

38 
quantifier instantiations. Each pattern should mention all preceding 

39 
bound variables. 

36898  40 
*} 
41 

42 
datatype pattern = Pattern 

43 

37124  44 
definition pat :: "'a \<Rightarrow> pattern" where "pat _ = Pattern" 
45 
definition nopat :: "'a \<Rightarrow> pattern" where "nopat _ = Pattern" 

36898  46 

37124  47 
definition trigger :: "pattern list list \<Rightarrow> bool \<Rightarrow> bool" 
36898  48 
where "trigger _ P = P" 
49 

50 

51 

40274
6486c610a549
introduced SMT.distinct as a representation of the solvers' builtin predicate; check that SMT.distinct is always applied to an explicit list
boehmes
parents:
40162
diff
changeset

52 
subsection {* Distinctness *} 
6486c610a549
introduced SMT.distinct as a representation of the solvers' builtin predicate; check that SMT.distinct is always applied to an explicit list
boehmes
parents:
40162
diff
changeset

53 

6486c610a549
introduced SMT.distinct as a representation of the solvers' builtin predicate; check that SMT.distinct is always applied to an explicit list
boehmes
parents:
40162
diff
changeset

54 
text {* 
6486c610a549
introduced SMT.distinct as a representation of the solvers' builtin predicate; check that SMT.distinct is always applied to an explicit list
boehmes
parents:
40162
diff
changeset

55 
As an abbreviation for a quadratic number of inequalities, SMT solvers 
6486c610a549
introduced SMT.distinct as a representation of the solvers' builtin predicate; check that SMT.distinct is always applied to an explicit list
boehmes
parents:
40162
diff
changeset

56 
provide a builtin @{text distinct}. To avoid confusion with the 
6486c610a549
introduced SMT.distinct as a representation of the solvers' builtin predicate; check that SMT.distinct is always applied to an explicit list
boehmes
parents:
40162
diff
changeset

57 
already defined (and more general) @{term List.distinct}, a separate 
6486c610a549
introduced SMT.distinct as a representation of the solvers' builtin predicate; check that SMT.distinct is always applied to an explicit list
boehmes
parents:
40162
diff
changeset

58 
constant is defined. 
6486c610a549
introduced SMT.distinct as a representation of the solvers' builtin predicate; check that SMT.distinct is always applied to an explicit list
boehmes
parents:
40162
diff
changeset

59 
*} 
6486c610a549
introduced SMT.distinct as a representation of the solvers' builtin predicate; check that SMT.distinct is always applied to an explicit list
boehmes
parents:
40162
diff
changeset

60 

6486c610a549
introduced SMT.distinct as a representation of the solvers' builtin predicate; check that SMT.distinct is always applied to an explicit list
boehmes
parents:
40162
diff
changeset

61 
definition distinct :: "'a list \<Rightarrow> bool" 
6486c610a549
introduced SMT.distinct as a representation of the solvers' builtin predicate; check that SMT.distinct is always applied to an explicit list
boehmes
parents:
40162
diff
changeset

62 
where "distinct xs = List.distinct xs" 
6486c610a549
introduced SMT.distinct as a representation of the solvers' builtin predicate; check that SMT.distinct is always applied to an explicit list
boehmes
parents:
40162
diff
changeset

63 

6486c610a549
introduced SMT.distinct as a representation of the solvers' builtin predicate; check that SMT.distinct is always applied to an explicit list
boehmes
parents:
40162
diff
changeset

64 

6486c610a549
introduced SMT.distinct as a representation of the solvers' builtin predicate; check that SMT.distinct is always applied to an explicit list
boehmes
parents:
40162
diff
changeset

65 

36902
c6bae4456741
use 'subsection' instead of 'section', to maintain 1 chapter per file in generated document
huffman
parents:
36899
diff
changeset

66 
subsection {* Higherorder encoding *} 
36898  67 

68 
text {* 

69 
Application is made explicit for constants occurring with varying 

70 
numbers of arguments. This is achieved by the introduction of the 

71 
following constant. 

72 
*} 

73 

37153
8feed34275ce
renamed constant "apply" to "fun_app" (which is closer to the related "fun_upd")
boehmes
parents:
37151
diff
changeset

74 
definition fun_app where "fun_app f x = f x" 
36898  75 

76 
text {* 

77 
Some solvers support a theory of arrays which can be used to encode 

78 
higherorder functions. The following set of lemmas specifies the 

79 
properties of such (extensional) arrays. 

80 
*} 

81 

82 
lemmas array_rules = ext fun_upd_apply fun_upd_same fun_upd_other 

37157  83 
fun_upd_upd fun_app_def 
36898  84 

85 

86 

36902
c6bae4456741
use 'subsection' instead of 'section', to maintain 1 chapter per file in generated document
huffman
parents:
36899
diff
changeset

87 
subsection {* Firstorder logic *} 
36898  88 

89 
text {* 

90 
Some SMT solvers require a strict separation between formulas and 

91 
terms. When translating higherorder into firstorder problems, 

92 
all uninterpreted constants (those not builtin in the target solver) 

93 
are treated as function symbols in the firstorder sense. Their 

94 
occurrences as head symbols in atoms (i.e., as predicate symbols) is 

95 
turned into terms by equating such atoms with @{term True} using the 

96 
following termlevel equation symbol. 

97 
*} 

98 

37124  99 
definition term_eq :: "bool \<Rightarrow> bool \<Rightarrow> bool" where "term_eq x y = (x = y)" 
36898  100 

101 

102 

37151  103 
subsection {* Integer division and modulo for Z3 *} 
104 

105 
definition z3div :: "int \<Rightarrow> int \<Rightarrow> int" where 

106 
"z3div k l = (if 0 \<le> l then k div l else (k div (l)))" 

107 

108 
definition z3mod :: "int \<Rightarrow> int \<Rightarrow> int" where 

109 
"z3mod k l = (if 0 \<le> l then k mod l else k mod (l))" 

110 

111 
lemma div_by_z3div: "k div l = ( 

112 
if k = 0 \<or> l = 0 then 0 

113 
else if (0 < k \<and> 0 < l) \<or> (k < 0 \<and> 0 < l) then z3div k l 

114 
else z3div (k) (l))" 

115 
by (auto simp add: z3div_def) 

116 

117 
lemma mod_by_z3mod: "k mod l = ( 

118 
if l = 0 then k 

119 
else if k = 0 then 0 

120 
else if (0 < k \<and> 0 < l) \<or> (k < 0 \<and> 0 < l) then z3mod k l 

121 
else  z3mod (k) (l))" 

122 
by (auto simp add: z3mod_def) 

123 

124 

125 

36902
c6bae4456741
use 'subsection' instead of 'section', to maintain 1 chapter per file in generated document
huffman
parents:
36899
diff
changeset

126 
subsection {* Setup *} 
36898  127 

128 
use "Tools/SMT/smt_monomorph.ML" 

129 
use "Tools/SMT/smt_normalize.ML" 

130 
use "Tools/SMT/smt_translate.ML" 

131 
use "Tools/SMT/smt_solver.ML" 

132 
use "Tools/SMT/smtlib_interface.ML" 

133 
use "Tools/SMT/z3_interface.ML" 

134 
use "Tools/SMT/z3_proof_parser.ML" 

135 
use "Tools/SMT/z3_proof_tools.ML" 

136 
use "Tools/SMT/z3_proof_literals.ML" 

137 
use "Tools/SMT/z3_proof_reconstruction.ML" 

138 
use "Tools/SMT/z3_model.ML" 

40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

139 
use "Tools/SMT/smt_setup_solvers.ML" 
36898  140 

141 
setup {* 

142 
SMT_Solver.setup #> 

143 
Z3_Proof_Reconstruction.setup #> 

40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

144 
SMT_Setup_Solvers.setup 
36898  145 
*} 
146 

147 

148 

36902
c6bae4456741
use 'subsection' instead of 'section', to maintain 1 chapter per file in generated document
huffman
parents:
36899
diff
changeset

149 
subsection {* Configuration *} 
36898  150 

151 
text {* 

36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

152 
The current configuration can be printed by the command 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

153 
@{text smt_status}, which shows the values of most options. 
36898  154 
*} 
155 

156 

157 

158 
subsection {* General configuration options *} 

159 

160 
text {* 

161 
The option @{text smt_solver} can be used to change the target SMT 

162 
solver. The possible values are @{text cvc3}, @{text yices}, and 

163 
@{text z3}. It is advisable to locally install the selected solver, 

164 
although this is not necessary for @{text cvc3} and @{text z3}, which 

165 
can also be used over an Internetbased service. 

166 

167 
When using local SMT solvers, the path to their binaries should be 

168 
declared by setting the following environment variables: 

169 
@{text CVC3_SOLVER}, @{text YICES_SOLVER}, and @{text Z3_SOLVER}. 

170 
*} 

171 

172 
declare [[ smt_solver = z3 ]] 

173 

174 
text {* 

175 
Since SMT solvers are potentially nonterminating, there is a timeout 

176 
(given in seconds) to restrict their runtime. A value greater than 

177 
120 (seconds) is in most cases not advisable. 

178 
*} 

179 

180 
declare [[ smt_timeout = 20 ]] 

181 

40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

182 
text {* 
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

183 
In general, the binding to SMT solvers runs as an oracle, i.e, the SMT 
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

184 
solvers are fully trusted without additional checks. The following 
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

185 
option can cause the SMT solver to run in proofproducing mode, giving 
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

186 
a checkable certificate. This is currently only implemented for Z3. 
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

187 
*} 
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

188 

7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

189 
declare [[ smt_oracle = false ]] 
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

190 

7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

191 
text {* 
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

192 
Each SMT solver provides several commandline options to tweak its 
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

193 
behaviour. They can be passed to the solver by setting the following 
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

194 
options. 
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

195 
*} 
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

196 

7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

197 
declare [[ cvc3_options = "", yices_options = "", z3_options = "" ]] 
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

198 

7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

199 
text {* 
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

200 
Enable the following option to use builtin support for datatypes and 
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

201 
records. Currently, this is only implemented for Z3 running in oracle 
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

202 
mode. 
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

203 
*} 
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

204 

7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

205 
declare [[ smt_datatypes = false ]] 
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

206 

36898  207 

208 

209 
subsection {* Certificates *} 

210 

211 
text {* 

212 
By setting the option @{text smt_certificates} to the name of a file, 

213 
all following applications of an SMT solver a cached in that file. 

214 
Any further application of the same SMT solver (using the very same 

215 
configuration) reuses the cached certificate instead of invoking the 

216 
solver. An empty string disables caching certificates. 

217 

218 
The filename should be given as an explicit path. It is good 

219 
practice to use the name of the current theory (with ending 

220 
@{text ".certs"} instead of @{text ".thy"}) as the certificates file. 

221 
*} 

222 

223 
declare [[ smt_certificates = "" ]] 

224 

225 
text {* 

226 
The option @{text smt_fixed} controls whether only stored 

227 
certificates are should be used or invocation of an SMT solver is 

228 
allowed. When set to @{text true}, no SMT solver will ever be 

229 
invoked and only the existing certificates found in the configured 

230 
cache are used; when set to @{text false} and there is no cached 

231 
certificate for some proposition, then the configured SMT solver is 

232 
invoked. 

233 
*} 

234 

235 
declare [[ smt_fixed = false ]] 

236 

237 

238 

239 
subsection {* Tracing *} 

240 

241 
text {* 

242 
For tracing the generated problem file given to the SMT solver as 

243 
well as the returned result of the solver, the option 

244 
@{text smt_trace} should be set to @{text true}. 

245 
*} 

246 

247 
declare [[ smt_trace = false ]] 

248 

249 
text {* 

40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

250 
From the set of assumptions given to the SMT solver, those assumptions 
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

251 
used in the proof are traced when the following option is set to 
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

252 
@{term true}. This only works for Z3 when it runs in nonoracle mode 
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

253 
(see options @{text smt_solver} and @{text smt_oracle} above). 
36898  254 
*} 
255 

40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

256 
declare [[ smt_trace_used_facts = false ]] 
39298
5aefb5bc8a93
added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents:
37818
diff
changeset

257 

36898  258 

259 

36902
c6bae4456741
use 'subsection' instead of 'section', to maintain 1 chapter per file in generated document
huffman
parents:
36899
diff
changeset

260 
subsection {* Schematic rules for Z3 proof reconstruction *} 
36898  261 

262 
text {* 

263 
Several prof rules of Z3 are not very well documented. There are two 

264 
lemma groups which can turn failing Z3 proof reconstruction attempts 

265 
into succeeding ones: the facts in @{text z3_rule} are tried prior to 

266 
any implemented reconstruction procedure for all uncertain Z3 proof 

267 
rules; the facts in @{text z3_simp} are only fed to invocations of 

268 
the simplifier when reconstructing theoryspecific proof steps. 

269 
*} 

270 

271 
lemmas [z3_rule] = 

272 
refl eq_commute conj_commute disj_commute simp_thms nnf_simps 

273 
ring_distribs field_simps times_divide_eq_right times_divide_eq_left 

274 
if_True if_False not_not 

275 

276 
lemma [z3_rule]: 

277 
"(P \<longrightarrow> Q) = (Q \<or> \<not>P)" 

278 
"(\<not>P \<longrightarrow> Q) = (P \<or> Q)" 

279 
"(\<not>P \<longrightarrow> Q) = (Q \<or> P)" 

280 
by auto 

281 

282 
lemma [z3_rule]: 

283 
"((P = Q) \<longrightarrow> R) = (R  (Q = (\<not>P)))" 

284 
by auto 

285 

286 
lemma [z3_rule]: 

287 
"((\<not>P) = P) = False" 

288 
"(P = (\<not>P)) = False" 

289 
"(P \<noteq> Q) = (Q = (\<not>P))" 

290 
"(P = Q) = ((\<not>P \<or> Q) \<and> (P \<or> \<not>Q))" 

291 
"(P \<noteq> Q) = ((\<not>P \<or> \<not>Q) \<and> (P \<or> Q))" 

292 
by auto 

293 

294 
lemma [z3_rule]: 

295 
"(if P then P else \<not>P) = True" 

296 
"(if \<not>P then \<not>P else P) = True" 

297 
"(if P then True else False) = P" 

298 
"(if P then False else True) = (\<not>P)" 

299 
"(if \<not>P then x else y) = (if P then y else x)" 

300 
by auto 

301 

302 
lemma [z3_rule]: 

303 
"P = Q \<or> P \<or> Q" 

304 
"P = Q \<or> \<not>P \<or> \<not>Q" 

305 
"(\<not>P) = Q \<or> \<not>P \<or> Q" 

306 
"(\<not>P) = Q \<or> P \<or> \<not>Q" 

307 
"P = (\<not>Q) \<or> \<not>P \<or> Q" 

308 
"P = (\<not>Q) \<or> P \<or> \<not>Q" 

309 
"P \<noteq> Q \<or> P \<or> \<not>Q" 

310 
"P \<noteq> Q \<or> \<not>P \<or> Q" 

311 
"P \<noteq> (\<not>Q) \<or> P \<or> Q" 

312 
"(\<not>P) \<noteq> Q \<or> P \<or> Q" 

313 
"P \<or> Q \<or> P \<noteq> (\<not>Q)" 

314 
"P \<or> Q \<or> (\<not>P) \<noteq> Q" 

315 
"P \<or> \<not>Q \<or> P \<noteq> Q" 

316 
"\<not>P \<or> Q \<or> P \<noteq> Q" 

317 
by auto 

318 

319 
lemma [z3_rule]: 

320 
"0 + (x::int) = x" 

321 
"x + 0 = x" 

322 
"0 * x = 0" 

323 
"1 * x = x" 

324 
"x + y = y + x" 

325 
by auto 

326 

37124  327 

328 

329 
hide_type (open) pattern 

37153
8feed34275ce
renamed constant "apply" to "fun_app" (which is closer to the related "fun_upd")
boehmes
parents:
37151
diff
changeset

330 
hide_const Pattern term_eq 
40274
6486c610a549
introduced SMT.distinct as a representation of the solvers' builtin predicate; check that SMT.distinct is always applied to an explicit list
boehmes
parents:
40162
diff
changeset

331 
hide_const (open) trigger pat nopat distinct fun_app z3div z3mod 
37124  332 

39483
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
39298
diff
changeset

333 

9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
39298
diff
changeset

334 

9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
39298
diff
changeset

335 
subsection {* Selectors for datatypes *} 
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
39298
diff
changeset

336 

9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
39298
diff
changeset

337 
setup {* Datatype_Selectors.setup *} 
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
39298
diff
changeset

338 

9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
39298
diff
changeset

339 
declare [[ selector Pair 1 = fst, selector Pair 2 = snd ]] 
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
39298
diff
changeset

340 
declare [[ selector Cons 1 = hd, selector Cons 2 = tl ]] 
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
39298
diff
changeset

341 

36898  342 
end 