|
1 (* Title: HOL/SMT_Examples/SMT_Tests.thy |
|
2 Author: Sascha Boehme, TU Muenchen |
|
3 Author: Mathias Fleury, MPII, JKU |
|
4 *) |
|
5 |
|
6 section \<open>Tests for the SMT binding\<close> |
|
7 |
|
8 theory SMT_Tests_Verit |
|
9 imports Complex_Main |
|
10 begin |
|
11 |
|
12 declare [[smt_solver=verit]] |
|
13 smt_status |
|
14 |
|
15 text \<open>Most examples are taken from the equivalent Z3 theory called \<^file>\<open>SMT_Tests.thy\<close>, |
|
16 and have been taken from various Isabelle and HOL4 developments.\<close> |
|
17 |
|
18 |
|
19 section \<open>Propositional logic\<close> |
|
20 |
|
21 lemma |
|
22 "True" |
|
23 "\<not> False" |
|
24 "\<not> \<not> True" |
|
25 "True \<and> True" |
|
26 "True \<or> False" |
|
27 "False \<longrightarrow> True" |
|
28 "\<not> (False \<longleftrightarrow> True)" |
|
29 by smt+ |
|
30 |
|
31 lemma |
|
32 "P \<or> \<not> P" |
|
33 "\<not> (P \<and> \<not> P)" |
|
34 "(True \<and> P) \<or> \<not> P \<or> (False \<and> P) \<or> P" |
|
35 "P \<longrightarrow> P" |
|
36 "P \<and> \<not> P \<longrightarrow> False" |
|
37 "P \<and> Q \<longrightarrow> Q \<and> P" |
|
38 "P \<or> Q \<longrightarrow> Q \<or> P" |
|
39 "P \<and> Q \<longrightarrow> P \<or> Q" |
|
40 "\<not> (P \<or> Q) \<longrightarrow> \<not> P" |
|
41 "\<not> (P \<or> Q) \<longrightarrow> \<not> Q" |
|
42 "\<not> P \<longrightarrow> \<not> (P \<and> Q)" |
|
43 "\<not> Q \<longrightarrow> \<not> (P \<and> Q)" |
|
44 "(P \<and> Q) \<longleftrightarrow> (\<not> (\<not> P \<or> \<not> Q))" |
|
45 "(P \<and> Q) \<and> R \<longrightarrow> P \<and> (Q \<and> R)" |
|
46 "(P \<or> Q) \<or> R \<longrightarrow> P \<or> (Q \<or> R)" |
|
47 "(P \<and> Q) \<or> R \<longrightarrow> (P \<or> R) \<and> (Q \<or> R)" |
|
48 "(P \<or> R) \<and> (Q \<or> R) \<longrightarrow> (P \<and> Q) \<or> R" |
|
49 "(P \<or> Q) \<and> R \<longrightarrow> (P \<and> R) \<or> (Q \<and> R)" |
|
50 "(P \<and> R) \<or> (Q \<and> R) \<longrightarrow> (P \<or> Q) \<and> R" |
|
51 "((P \<longrightarrow> Q) \<longrightarrow> P) \<longrightarrow> P" |
|
52 "(P \<longrightarrow> R) \<and> (Q \<longrightarrow> R) \<longleftrightarrow> (P \<or> Q \<longrightarrow> R)" |
|
53 "(P \<and> Q \<longrightarrow> R) \<longleftrightarrow> (P \<longrightarrow> (Q \<longrightarrow> R))" |
|
54 "((P \<longrightarrow> R) \<longrightarrow> R) \<longrightarrow> ((Q \<longrightarrow> R) \<longrightarrow> R) \<longrightarrow> (P \<and> Q \<longrightarrow> R) \<longrightarrow> R" |
|
55 "\<not> (P \<longrightarrow> R) \<longrightarrow> \<not> (Q \<longrightarrow> R) \<longrightarrow> \<not> (P \<and> Q \<longrightarrow> R)" |
|
56 "(P \<longrightarrow> Q \<and> R) \<longleftrightarrow> (P \<longrightarrow> Q) \<and> (P \<longrightarrow> R)" |
|
57 "P \<longrightarrow> (Q \<longrightarrow> P)" |
|
58 "(P \<longrightarrow> Q \<longrightarrow> R) \<longrightarrow> (P \<longrightarrow> Q)\<longrightarrow> (P \<longrightarrow> R)" |
|
59 "(P \<longrightarrow> Q) \<or> (P \<longrightarrow> R) \<longrightarrow> (P \<longrightarrow> Q \<or> R)" |
|
60 "((((P \<longrightarrow> Q) \<longrightarrow> P) \<longrightarrow> P) \<longrightarrow> Q) \<longrightarrow> Q" |
|
61 "(P \<longrightarrow> Q) \<longrightarrow> (\<not> Q \<longrightarrow> \<not> P)" |
|
62 "(P \<longrightarrow> Q \<or> R) \<longrightarrow> (P \<longrightarrow> Q) \<or> (P \<longrightarrow> R)" |
|
63 "(P \<longrightarrow> Q) \<and> (Q \<longrightarrow> P) \<longrightarrow> (P \<longleftrightarrow> Q)" |
|
64 "(P \<longleftrightarrow> Q) \<longleftrightarrow> (Q \<longleftrightarrow> P)" |
|
65 "\<not> (P \<longleftrightarrow> \<not> P)" |
|
66 "(P \<longrightarrow> Q) \<longleftrightarrow> (\<not> Q \<longrightarrow> \<not> P)" |
|
67 "P \<longleftrightarrow> P \<longleftrightarrow> P \<longleftrightarrow> P \<longleftrightarrow> P \<longleftrightarrow> P \<longleftrightarrow> P \<longleftrightarrow> P \<longleftrightarrow> P \<longleftrightarrow> P" |
|
68 by smt+ |
|
69 |
|
70 lemma |
|
71 "(if P then Q1 else Q2) \<longleftrightarrow> ((P \<longrightarrow> Q1) \<and> (\<not> P \<longrightarrow> Q2))" |
|
72 "if P then (Q \<longrightarrow> P) else (P \<longrightarrow> Q)" |
|
73 "(if P1 \<or> P2 then Q1 else Q2) \<longleftrightarrow> (if P1 then Q1 else if P2 then Q1 else Q2)" |
|
74 "(if P1 \<and> P2 then Q1 else Q2) \<longleftrightarrow> (if P1 then if P2 then Q1 else Q2 else Q2)" |
|
75 "(P1 \<longrightarrow> (if P2 then Q1 else Q2)) \<longleftrightarrow> |
|
76 (if P1 \<longrightarrow> P2 then P1 \<longrightarrow> Q1 else P1 \<longrightarrow> Q2)" |
|
77 by smt+ |
|
78 |
|
79 lemma |
|
80 "case P of True \<Rightarrow> P | False \<Rightarrow> \<not> P" |
|
81 "case P of False \<Rightarrow> \<not> P | True \<Rightarrow> P" |
|
82 "case \<not> P of True \<Rightarrow> \<not> P | False \<Rightarrow> P" |
|
83 "case P of True \<Rightarrow> (Q \<longrightarrow> P) | False \<Rightarrow> (P \<longrightarrow> Q)" |
|
84 by smt+ |
|
85 |
|
86 |
|
87 section \<open>First-order logic with equality\<close> |
|
88 |
|
89 lemma |
|
90 "x = x" |
|
91 "x = y \<longrightarrow> y = x" |
|
92 "x = y \<and> y = z \<longrightarrow> x = z" |
|
93 "x = y \<longrightarrow> f x = f y" |
|
94 "x = y \<longrightarrow> g x y = g y x" |
|
95 "f (f x) = x \<and> f (f (f (f (f x)))) = x \<longrightarrow> f x = x" |
|
96 "((if a then b else c) = d) = ((a \<longrightarrow> (b = d)) \<and> (\<not> a \<longrightarrow> (c = d)))" |
|
97 by smt+ |
|
98 |
|
99 lemma |
|
100 "\<forall>x. x = x" |
|
101 "(\<forall>x. P x) \<longleftrightarrow> (\<forall>y. P y)" |
|
102 "\<forall>x. P x \<longrightarrow> (\<forall>y. P x \<or> P y)" |
|
103 "(\<forall>x. P x \<and> Q x) \<longleftrightarrow> (\<forall>x. P x) \<and> (\<forall>x. Q x)" |
|
104 "(\<forall>x. P x) \<or> R \<longleftrightarrow> (\<forall>x. P x \<or> R)" |
|
105 "(\<forall>x y z. S x z) \<longleftrightarrow> (\<forall>x z. S x z)" |
|
106 "(\<forall>x y. S x y \<longrightarrow> S y x) \<longrightarrow> (\<forall>x. S x y) \<longrightarrow> S y x" |
|
107 "(\<forall>x. P x \<longrightarrow> P (f x)) \<and> P d \<longrightarrow> P (f(f(f(d))))" |
|
108 "(\<forall>x y. s x y = s y x) \<longrightarrow> a = a \<and> s a b = s b a" |
|
109 "(\<forall>s. q s \<longrightarrow> r s) \<and> \<not> r s \<and> (\<forall>s. \<not> r s \<and> \<not> q s \<longrightarrow> p t \<or> q t) \<longrightarrow> p t \<or> r t" |
|
110 by smt+ |
|
111 |
|
112 lemma |
|
113 "(\<forall>x. P x) \<and> R \<longleftrightarrow> (\<forall>x. P x \<and> R)" |
|
114 by smt |
|
115 |
|
116 lemma |
|
117 "\<exists>x. x = x" |
|
118 "(\<exists>x. P x) \<longleftrightarrow> (\<exists>y. P y)" |
|
119 "(\<exists>x. P x \<or> Q x) \<longleftrightarrow> (\<exists>x. P x) \<or> (\<exists>x. Q x)" |
|
120 "(\<exists>x. P x) \<and> R \<longleftrightarrow> (\<exists>x. P x \<and> R)" |
|
121 "(\<exists>x y z. S x z) \<longleftrightarrow> (\<exists>x z. S x z)" |
|
122 "\<not> ((\<exists>x. \<not> P x) \<and> ((\<exists>x. P x) \<or> (\<exists>x. P x \<and> Q x)) \<and> \<not> (\<exists>x. P x))" |
|
123 by smt+ |
|
124 |
|
125 lemma |
|
126 "\<exists>x y. x = y" |
|
127 "(\<exists>x. P x) \<or> R \<longleftrightarrow> (\<exists>x. P x \<or> R)" |
|
128 "\<exists>x. P x \<longrightarrow> P a \<and> P b" |
|
129 "(\<exists>x. Q \<longrightarrow> P x) \<longleftrightarrow> (Q \<longrightarrow> (\<exists>x. P x))" |
|
130 supply[[smt_trace]] |
|
131 by smt+ |
|
132 |
|
133 lemma |
|
134 "(\<not> (\<exists>x. P x)) \<longleftrightarrow> (\<forall>x. \<not> P x)" |
|
135 "(\<exists>x. P x \<longrightarrow> Q) \<longleftrightarrow> (\<forall>x. P x) \<longrightarrow> Q" |
|
136 "(\<forall>x y. R x y = x) \<longrightarrow> (\<exists>y. R x y) = R x c" |
|
137 "(if P x then \<not> (\<exists>y. P y) else (\<forall>y. \<not> P y)) \<longrightarrow> P x \<longrightarrow> P y" |
|
138 "(\<forall>x y. R x y = x) \<and> (\<forall>x. \<exists>y. R x y) = (\<forall>x. R x c) \<longrightarrow> (\<exists>y. R x y) = R x c" |
|
139 by smt+ |
|
140 |
|
141 lemma |
|
142 "\<forall>x. \<exists>y. f x y = f x (g x)" |
|
143 "(\<not> \<not> (\<exists>x. P x)) \<longleftrightarrow> (\<not> (\<forall>x. \<not> P x))" |
|
144 "\<forall>u. \<exists>v. \<forall>w. \<exists>x. f u v w x = f u (g u) w (h u w)" |
|
145 "\<exists>x. if x = y then (\<forall>y. y = x \<or> y \<noteq> x) else (\<forall>y. y = (x, x) \<or> y \<noteq> (x, x))" |
|
146 "\<exists>x. if x = y then (\<exists>y. y = x \<or> y \<noteq> x) else (\<exists>y. y = (x, x) \<or> y \<noteq> (x, x))" |
|
147 "(\<exists>x. \<forall>y. P x \<longleftrightarrow> P y) \<longrightarrow> ((\<exists>x. P x) \<longleftrightarrow> (\<forall>y. P y))" |
|
148 "(\<exists>y. \<forall>x. R x y) \<longrightarrow> (\<forall>x. \<exists>y. R x y)" |
|
149 by smt+ |
|
150 |
|
151 lemma |
|
152 "(\<exists>!x. P x) \<longrightarrow> (\<exists>x. P x)" |
|
153 "(\<exists>!x. P x) \<longleftrightarrow> (\<exists>x. P x \<and> (\<forall>y. y \<noteq> x \<longrightarrow> \<not> P y))" |
|
154 "P a \<longrightarrow> (\<forall>x. P x \<longrightarrow> x = a) \<longrightarrow> (\<exists>!x. P x)" |
|
155 "(\<exists>x. P x) \<and> (\<forall>x y. P x \<and> P y \<longrightarrow> x = y) \<longrightarrow> (\<exists>!x. P x)" |
|
156 "(\<exists>!x. P x) \<and> (\<forall>x. P x \<and> (\<forall>y. P y \<longrightarrow> y = x) \<longrightarrow> R) \<longrightarrow> R" |
|
157 by smt+ |
|
158 |
|
159 lemma |
|
160 "(\<forall>x\<in>M. P x) \<and> c \<in> M \<longrightarrow> P c" |
|
161 "(\<exists>x\<in>M. P x) \<or> \<not> (P c \<and> c \<in> M)" |
|
162 by smt+ |
|
163 |
|
164 lemma |
|
165 "let P = True in P" |
|
166 "let P = P1 \<or> P2 in P \<or> \<not> P" |
|
167 "let P1 = True; P2 = False in P1 \<and> P2 \<longrightarrow> P2 \<or> P1" |
|
168 "(let x = y in x) = y" |
|
169 "(let x = y in Q x) \<longleftrightarrow> (let z = y in Q z)" |
|
170 "(let x = y1; z = y2 in R x z) \<longleftrightarrow> (let z = y2; x = y1 in R x z)" |
|
171 "(let x = y1; z = y2 in R x z) \<longleftrightarrow> (let z = y1; x = y2 in R z x)" |
|
172 "let P = (\<forall>x. Q x) in if P then P else \<not> P" |
|
173 by smt+ |
|
174 |
|
175 lemma |
|
176 "a \<noteq> b \<and> a \<noteq> c \<and> b \<noteq> c \<and> (\<forall>x y. f x = f y \<longrightarrow> y = x) \<longrightarrow> f a \<noteq> f b" |
|
177 by smt |
|
178 |
|
179 lemma |
|
180 "(\<forall>x y z. f x y = f x z \<longrightarrow> y = z) \<and> b \<noteq> c \<longrightarrow> f a b \<noteq> f a c" |
|
181 "(\<forall>x y z. f x y = f z y \<longrightarrow> x = z) \<and> a \<noteq> d \<longrightarrow> f a b \<noteq> f d b" |
|
182 by smt+ |
|
183 |
|
184 |
|
185 section \<open>Guidance for quantifier heuristics: patterns\<close> |
|
186 |
|
187 lemma |
|
188 assumes "\<forall>x. |
|
189 SMT.trigger (SMT.Symb_Cons (SMT.Symb_Cons (SMT.pat (f x)) SMT.Symb_Nil) SMT.Symb_Nil) |
|
190 (f x = x)" |
|
191 shows "f 1 = 1" |
|
192 using assms by smt |
|
193 |
|
194 lemma |
|
195 assumes "\<forall>x y. |
|
196 SMT.trigger (SMT.Symb_Cons (SMT.Symb_Cons (SMT.pat (f x)) |
|
197 (SMT.Symb_Cons (SMT.pat (g y)) SMT.Symb_Nil)) SMT.Symb_Nil) (f x = g y)" |
|
198 shows "f a = g b" |
|
199 using assms by smt |
|
200 |
|
201 |
|
202 section \<open>Meta-logical connectives\<close> |
|
203 |
|
204 lemma |
|
205 "True \<Longrightarrow> True" |
|
206 "False \<Longrightarrow> True" |
|
207 "False \<Longrightarrow> False" |
|
208 "P' x \<Longrightarrow> P' x" |
|
209 "P \<Longrightarrow> P \<or> Q" |
|
210 "Q \<Longrightarrow> P \<or> Q" |
|
211 "\<not> P \<Longrightarrow> P \<longrightarrow> Q" |
|
212 "Q \<Longrightarrow> P \<longrightarrow> Q" |
|
213 "\<lbrakk>P; \<not> Q\<rbrakk> \<Longrightarrow> \<not> (P \<longrightarrow> Q)" |
|
214 "P' x \<equiv> P' x" |
|
215 "P' x \<equiv> Q' x \<Longrightarrow> P' x = Q' x" |
|
216 "P' x = Q' x \<Longrightarrow> P' x \<equiv> Q' x" |
|
217 "x \<equiv> y \<Longrightarrow> y \<equiv> z \<Longrightarrow> x \<equiv> (z::'a::type)" |
|
218 "x \<equiv> y \<Longrightarrow> (f x :: 'b::type) \<equiv> f y" |
|
219 "(\<And>x. g x) \<Longrightarrow> g a \<or> a" |
|
220 "(\<And>x y. h x y \<and> h y x) \<Longrightarrow> \<forall>x. h x x" |
|
221 "(p \<or> q) \<and> \<not> p \<Longrightarrow> q" |
|
222 "(a \<and> b) \<or> (c \<and> d) \<Longrightarrow> (a \<and> b) \<or> (c \<and> d)" |
|
223 by smt+ |
|
224 |
|
225 |
|
226 section \<open>Natural numbers\<close> |
|
227 |
|
228 declare [[smt_nat_as_int]] |
|
229 |
|
230 lemma |
|
231 "(0::nat) = 0" |
|
232 "(1::nat) = 1" |
|
233 "(0::nat) < 1" |
|
234 "(0::nat) \<le> 1" |
|
235 "(123456789::nat) < 2345678901" |
|
236 by smt+ |
|
237 |
|
238 lemma |
|
239 "Suc 0 = 1" |
|
240 "Suc x = x + 1" |
|
241 "x < Suc x" |
|
242 "(Suc x = Suc y) = (x = y)" |
|
243 "Suc (x + y) < Suc x + Suc y" |
|
244 by smt+ |
|
245 |
|
246 lemma |
|
247 "(x::nat) + 0 = x" |
|
248 "0 + x = x" |
|
249 "x + y = y + x" |
|
250 "x + (y + z) = (x + y) + z" |
|
251 "(x + y = 0) = (x = 0 \<and> y = 0)" |
|
252 by smt+ |
|
253 |
|
254 lemma |
|
255 "(x::nat) - 0 = x" |
|
256 "x < y \<longrightarrow> x - y = 0" |
|
257 "x - y = 0 \<or> y - x = 0" |
|
258 "(x - y) + y = (if x < y then y else x)" |
|
259 "x - y - z = x - (y + z)" |
|
260 by smt+ |
|
261 |
|
262 lemma |
|
263 "(x::nat) * 0 = 0" |
|
264 "0 * x = 0" |
|
265 "x * 1 = x" |
|
266 "1 * x = x" |
|
267 "3 * x = x * 3" |
|
268 by smt+ |
|
269 |
|
270 lemma |
|
271 "min (x::nat) y \<le> x" |
|
272 "min x y \<le> y" |
|
273 "min x y \<le> x + y" |
|
274 "z < x \<and> z < y \<longrightarrow> z < min x y" |
|
275 "min x y = min y x" |
|
276 "min x 0 = 0" |
|
277 by smt+ |
|
278 |
|
279 lemma |
|
280 "max (x::nat) y \<ge> x" |
|
281 "max x y \<ge> y" |
|
282 "max x y \<ge> (x - y) + (y - x)" |
|
283 "z > x \<and> z > y \<longrightarrow> z > max x y" |
|
284 "max x y = max y x" |
|
285 "max x 0 = x" |
|
286 by smt+ |
|
287 |
|
288 lemma |
|
289 "0 \<le> (x::nat)" |
|
290 "0 < x \<and> x \<le> 1 \<longrightarrow> x = 1" |
|
291 "x \<le> x" |
|
292 "x \<le> y \<longrightarrow> 3 * x \<le> 3 * y" |
|
293 "x < y \<longrightarrow> 3 * x < 3 * y" |
|
294 "x < y \<longrightarrow> x \<le> y" |
|
295 "(x < y) = (x + 1 \<le> y)" |
|
296 "\<not> (x < x)" |
|
297 "x \<le> y \<longrightarrow> y \<le> z \<longrightarrow> x \<le> z" |
|
298 "x < y \<longrightarrow> y \<le> z \<longrightarrow> x \<le> z" |
|
299 "x \<le> y \<longrightarrow> y < z \<longrightarrow> x \<le> z" |
|
300 "x < y \<longrightarrow> y < z \<longrightarrow> x < z" |
|
301 "x < y \<and> y < z \<longrightarrow> \<not> (z < x)" |
|
302 by smt+ |
|
303 |
|
304 declare [[smt_nat_as_int = false]] |
|
305 |
|
306 |
|
307 section \<open>Integers\<close> |
|
308 |
|
309 lemma |
|
310 "(0::int) = 0" |
|
311 "(0::int) = (- 0)" |
|
312 "(1::int) = 1" |
|
313 "\<not> (-1 = (1::int))" |
|
314 "(0::int) < 1" |
|
315 "(0::int) \<le> 1" |
|
316 "-123 + 345 < (567::int)" |
|
317 "(123456789::int) < 2345678901" |
|
318 "(-123456789::int) < 2345678901" |
|
319 by smt+ |
|
320 |
|
321 lemma |
|
322 "(x::int) + 0 = x" |
|
323 "0 + x = x" |
|
324 "x + y = y + x" |
|
325 "x + (y + z) = (x + y) + z" |
|
326 "(x + y = 0) = (x = -y)" |
|
327 by smt+ |
|
328 |
|
329 lemma |
|
330 "(-1::int) = - 1" |
|
331 "(-3::int) = - 3" |
|
332 "-(x::int) < 0 \<longleftrightarrow> x > 0" |
|
333 "x > 0 \<longrightarrow> -x < 0" |
|
334 "x < 0 \<longrightarrow> -x > 0" |
|
335 by smt+ |
|
336 |
|
337 lemma |
|
338 "(x::int) - 0 = x" |
|
339 "0 - x = -x" |
|
340 "x < y \<longrightarrow> x - y < 0" |
|
341 "x - y = -(y - x)" |
|
342 "x - y = -y + x" |
|
343 "x - y - z = x - (y + z)" |
|
344 by smt+ |
|
345 |
|
346 lemma |
|
347 "(x::int) * 0 = 0" |
|
348 "0 * x = 0" |
|
349 "x * 1 = x" |
|
350 "1 * x = x" |
|
351 "x * -1 = -x" |
|
352 "-1 * x = -x" |
|
353 "3 * x = x * 3" |
|
354 by smt+ |
|
355 |
|
356 lemma |
|
357 "\<bar>x::int\<bar> \<ge> 0" |
|
358 "(\<bar>x\<bar> = 0) = (x = 0)" |
|
359 "(x \<ge> 0) = (\<bar>x\<bar> = x)" |
|
360 "(x \<le> 0) = (\<bar>x\<bar> = -x)" |
|
361 "\<bar>\<bar>x\<bar>\<bar> = \<bar>x\<bar>" |
|
362 by smt+ |
|
363 |
|
364 lemma |
|
365 "min (x::int) y \<le> x" |
|
366 "min x y \<le> y" |
|
367 "z < x \<and> z < y \<longrightarrow> z < min x y" |
|
368 "min x y = min y x" |
|
369 "x \<ge> 0 \<longrightarrow> min x 0 = 0" |
|
370 "min x y \<le> \<bar>x + y\<bar>" |
|
371 by smt+ |
|
372 |
|
373 lemma |
|
374 "max (x::int) y \<ge> x" |
|
375 "max x y \<ge> y" |
|
376 "z > x \<and> z > y \<longrightarrow> z > max x y" |
|
377 "max x y = max y x" |
|
378 "x \<ge> 0 \<longrightarrow> max x 0 = x" |
|
379 "max x y \<ge> - \<bar>x\<bar> - \<bar>y\<bar>" |
|
380 by smt+ |
|
381 |
|
382 lemma |
|
383 "0 < (x::int) \<and> x \<le> 1 \<longrightarrow> x = 1" |
|
384 "x \<le> x" |
|
385 "x \<le> y \<longrightarrow> 3 * x \<le> 3 * y" |
|
386 "x < y \<longrightarrow> 3 * x < 3 * y" |
|
387 "x < y \<longrightarrow> x \<le> y" |
|
388 "(x < y) = (x + 1 \<le> y)" |
|
389 "\<not> (x < x)" |
|
390 "x \<le> y \<longrightarrow> y \<le> z \<longrightarrow> x \<le> z" |
|
391 "x < y \<longrightarrow> y \<le> z \<longrightarrow> x \<le> z" |
|
392 "x \<le> y \<longrightarrow> y < z \<longrightarrow> x \<le> z" |
|
393 "x < y \<longrightarrow> y < z \<longrightarrow> x < z" |
|
394 "x < y \<and> y < z \<longrightarrow> \<not> (z < x)" |
|
395 by smt+ |
|
396 |
|
397 |
|
398 section \<open>Reals\<close> |
|
399 |
|
400 lemma |
|
401 "(0::real) = 0" |
|
402 "(0::real) = -0" |
|
403 "(0::real) = (- 0)" |
|
404 "(1::real) = 1" |
|
405 "\<not> (-1 = (1::real))" |
|
406 "(0::real) < 1" |
|
407 "(0::real) \<le> 1" |
|
408 "-123 + 345 < (567::real)" |
|
409 "(123456789::real) < 2345678901" |
|
410 "(-123456789::real) < 2345678901" |
|
411 by smt+ |
|
412 |
|
413 lemma |
|
414 "(x::real) + 0 = x" |
|
415 "0 + x = x" |
|
416 "x + y = y + x" |
|
417 "x + (y + z) = (x + y) + z" |
|
418 "(x + y = 0) = (x = -y)" |
|
419 by smt+ |
|
420 |
|
421 lemma |
|
422 "(-1::real) = - 1" |
|
423 "(-3::real) = - 3" |
|
424 "-(x::real) < 0 \<longleftrightarrow> x > 0" |
|
425 "x > 0 \<longrightarrow> -x < 0" |
|
426 "x < 0 \<longrightarrow> -x > 0" |
|
427 by smt+ |
|
428 |
|
429 lemma |
|
430 "(x::real) - 0 = x" |
|
431 "0 - x = -x" |
|
432 "x < y \<longrightarrow> x - y < 0" |
|
433 "x - y = -(y - x)" |
|
434 "x - y = -y + x" |
|
435 "x - y - z = x - (y + z)" |
|
436 by smt+ |
|
437 |
|
438 lemma |
|
439 "(x::real) * 0 = 0" |
|
440 "0 * x = 0" |
|
441 "x * 1 = x" |
|
442 "1 * x = x" |
|
443 "x * -1 = -x" |
|
444 "-1 * x = -x" |
|
445 "3 * x = x * 3" |
|
446 by smt+ |
|
447 |
|
448 lemma |
|
449 "\<bar>x::real\<bar> \<ge> 0" |
|
450 "(\<bar>x\<bar> = 0) = (x = 0)" |
|
451 "(x \<ge> 0) = (\<bar>x\<bar> = x)" |
|
452 "(x \<le> 0) = (\<bar>x\<bar> = -x)" |
|
453 "\<bar>\<bar>x\<bar>\<bar> = \<bar>x\<bar>" |
|
454 by smt+ |
|
455 |
|
456 lemma |
|
457 "min (x::real) y \<le> x" |
|
458 "min x y \<le> y" |
|
459 "z < x \<and> z < y \<longrightarrow> z < min x y" |
|
460 "min x y = min y x" |
|
461 "x \<ge> 0 \<longrightarrow> min x 0 = 0" |
|
462 "min x y \<le> \<bar>x + y\<bar>" |
|
463 by smt+ |
|
464 |
|
465 lemma |
|
466 "max (x::real) y \<ge> x" |
|
467 "max x y \<ge> y" |
|
468 "z > x \<and> z > y \<longrightarrow> z > max x y" |
|
469 "max x y = max y x" |
|
470 "x \<ge> 0 \<longrightarrow> max x 0 = x" |
|
471 "max x y \<ge> - \<bar>x\<bar> - \<bar>y\<bar>" |
|
472 by smt+ |
|
473 |
|
474 lemma |
|
475 "x \<le> (x::real)" |
|
476 "x \<le> y \<longrightarrow> 3 * x \<le> 3 * y" |
|
477 "x < y \<longrightarrow> 3 * x < 3 * y" |
|
478 "x < y \<longrightarrow> x \<le> y" |
|
479 "\<not> (x < x)" |
|
480 "x \<le> y \<longrightarrow> y \<le> z \<longrightarrow> x \<le> z" |
|
481 "x < y \<longrightarrow> y \<le> z \<longrightarrow> x \<le> z" |
|
482 "x \<le> y \<longrightarrow> y < z \<longrightarrow> x \<le> z" |
|
483 "x < y \<longrightarrow> y < z \<longrightarrow> x < z" |
|
484 "x < y \<and> y < z \<longrightarrow> \<not> (z < x)" |
|
485 by smt+ |
|
486 |
|
487 |
|
488 section \<open>Datatypes, records, and typedefs\<close> |
|
489 |
|
490 subsection \<open>Without support by the SMT solver\<close> |
|
491 |
|
492 subsubsection \<open>Algebraic datatypes\<close> |
|
493 |
|
494 lemma |
|
495 "x = fst (x, y)" |
|
496 "y = snd (x, y)" |
|
497 "((x, y) = (y, x)) = (x = y)" |
|
498 "((x, y) = (u, v)) = (x = u \<and> y = v)" |
|
499 "(fst (x, y, z) = fst (u, v, w)) = (x = u)" |
|
500 "(snd (x, y, z) = snd (u, v, w)) = (y = v \<and> z = w)" |
|
501 "(fst (snd (x, y, z)) = fst (snd (u, v, w))) = (y = v)" |
|
502 "(snd (snd (x, y, z)) = snd (snd (u, v, w))) = (z = w)" |
|
503 "(fst (x, y) = snd (x, y)) = (x = y)" |
|
504 "p1 = (x, y) \<and> p2 = (y, x) \<longrightarrow> fst p1 = snd p2" |
|
505 "(fst (x, y) = snd (x, y)) = (x = y)" |
|
506 "(fst p = snd p) = (p = (snd p, fst p))" |
|
507 using fst_conv snd_conv prod.collapse |
|
508 by smt+ |
|
509 |
|
510 lemma |
|
511 "[x] \<noteq> Nil" |
|
512 "[x, y] \<noteq> Nil" |
|
513 "x \<noteq> y \<longrightarrow> [x] \<noteq> [y]" |
|
514 "hd (x # xs) = x" |
|
515 "tl (x # xs) = xs" |
|
516 "hd [x, y, z] = x" |
|
517 "tl [x, y, z] = [y, z]" |
|
518 "hd (tl [x, y, z]) = y" |
|
519 "tl (tl [x, y, z]) = [z]" |
|
520 using list.sel(1,3) list.simps |
|
521 by smt+ |
|
522 |
|
523 lemma |
|
524 "fst (hd [(a, b)]) = a" |
|
525 "snd (hd [(a, b)]) = b" |
|
526 using fst_conv snd_conv prod.collapse list.sel(1,3) list.simps |
|
527 by smt+ |
|
528 |
|
529 |
|
530 subsubsection \<open>Records\<close> |
|
531 |
|
532 record point = |
|
533 cx :: int |
|
534 cy :: int |
|
535 |
|
536 record bw_point = point + |
|
537 black :: bool |
|
538 |
|
539 lemma |
|
540 "\<lparr>cx = x, cy = y\<rparr> = \<lparr>cx = x', cy = y'\<rparr> \<Longrightarrow> x = x' \<and> y = y'" |
|
541 using point.simps |
|
542 by smt |
|
543 |
|
544 lemma |
|
545 "cx \<lparr> cx = 3, cy = 4 \<rparr> = 3" |
|
546 "cy \<lparr> cx = 3, cy = 4 \<rparr> = 4" |
|
547 "cx \<lparr> cx = 3, cy = 4 \<rparr> \<noteq> cy \<lparr> cx = 3, cy = 4 \<rparr>" |
|
548 "\<lparr> cx = 3, cy = 4 \<rparr> \<lparr> cx := 5 \<rparr> = \<lparr> cx = 5, cy = 4 \<rparr>" |
|
549 "\<lparr> cx = 3, cy = 4 \<rparr> \<lparr> cy := 6 \<rparr> = \<lparr> cx = 3, cy = 6 \<rparr>" |
|
550 "p = \<lparr> cx = 3, cy = 4 \<rparr> \<longrightarrow> p \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> = p" |
|
551 "p = \<lparr> cx = 3, cy = 4 \<rparr> \<longrightarrow> p \<lparr> cy := 4 \<rparr> \<lparr> cx := 3 \<rparr> = p" |
|
552 using point.simps |
|
553 by smt+ |
|
554 |
|
555 lemma |
|
556 "\<lparr>cx = x, cy = y, black = b\<rparr> = \<lparr>cx = x', cy = y', black = b'\<rparr> \<Longrightarrow> x = x' \<and> y = y' \<and> b = b'" |
|
557 using point.simps bw_point.simps |
|
558 by smt |
|
559 |
|
560 lemma |
|
561 "cx \<lparr> cx = 3, cy = 4, black = b \<rparr> = 3" |
|
562 "cy \<lparr> cx = 3, cy = 4, black = b \<rparr> = 4" |
|
563 "black \<lparr> cx = 3, cy = 4, black = b \<rparr> = b" |
|
564 "cx \<lparr> cx = 3, cy = 4, black = b \<rparr> \<noteq> cy \<lparr> cx = 3, cy = 4, black = b \<rparr>" |
|
565 "\<lparr> cx = 3, cy = 4, black = b \<rparr> \<lparr> cx := 5 \<rparr> = \<lparr> cx = 5, cy = 4, black = b \<rparr>" |
|
566 "\<lparr> cx = 3, cy = 4, black = b \<rparr> \<lparr> cy := 6 \<rparr> = \<lparr> cx = 3, cy = 6, black = b \<rparr>" |
|
567 "p = \<lparr> cx = 3, cy = 4, black = True \<rparr> \<longrightarrow> |
|
568 p \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> \<lparr> black := True \<rparr> = p" |
|
569 "p = \<lparr> cx = 3, cy = 4, black = True \<rparr> \<longrightarrow> |
|
570 p \<lparr> cy := 4 \<rparr> \<lparr> black := True \<rparr> \<lparr> cx := 3 \<rparr> = p" |
|
571 "p = \<lparr> cx = 3, cy = 4, black = True \<rparr> \<longrightarrow> |
|
572 p \<lparr> black := True \<rparr> \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> = p" |
|
573 using point.simps bw_point.simps |
|
574 by smt+ |
|
575 |
|
576 lemma |
|
577 "\<lparr> cx = 3, cy = 4, black = b \<rparr> \<lparr> black := w \<rparr> = \<lparr> cx = 3, cy = 4, black = w \<rparr>" |
|
578 "\<lparr> cx = 3, cy = 4, black = True \<rparr> \<lparr> black := False \<rparr> = |
|
579 \<lparr> cx = 3, cy = 4, black = False \<rparr>" |
|
580 "p \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> \<lparr> black := True \<rparr> = |
|
581 p \<lparr> black := True \<rparr> \<lparr> cy := 4 \<rparr> \<lparr> cx := 3 \<rparr>" |
|
582 apply (smt add_One add_inc bw_point.update_convs(1) default_unit_def inc.simps(2) one_plus_BitM |
|
583 semiring_norm(6,26)) |
|
584 apply (smt bw_point.update_convs(1)) |
|
585 apply (smt bw_point.cases_scheme bw_point.update_convs(1) point.update_convs(1,2)) |
|
586 done |
|
587 |
|
588 |
|
589 subsubsection \<open>Type definitions\<close> |
|
590 |
|
591 typedef int' = "UNIV::int set" by (rule UNIV_witness) |
|
592 |
|
593 definition n0 where "n0 = Abs_int' 0" |
|
594 definition n1 where "n1 = Abs_int' 1" |
|
595 definition n2 where "n2 = Abs_int' 2" |
|
596 definition plus' where "plus' n m = Abs_int' (Rep_int' n + Rep_int' m)" |
|
597 |
|
598 lemma |
|
599 "n0 \<noteq> n1" |
|
600 "plus' n1 n1 = n2" |
|
601 "plus' n0 n2 = n2" |
|
602 by (smt n0_def n1_def n2_def plus'_def Abs_int'_inverse Rep_int'_inverse UNIV_I)+ |
|
603 |
|
604 |
|
605 subsection \<open>With support by the SMT solver (but without proofs)\<close> |
|
606 |
|
607 subsubsection \<open>Algebraic datatypes\<close> |
|
608 |
|
609 lemma |
|
610 "x = fst (x, y)" |
|
611 "y = snd (x, y)" |
|
612 "((x, y) = (y, x)) = (x = y)" |
|
613 "((x, y) = (u, v)) = (x = u \<and> y = v)" |
|
614 "(fst (x, y, z) = fst (u, v, w)) = (x = u)" |
|
615 "(snd (x, y, z) = snd (u, v, w)) = (y = v \<and> z = w)" |
|
616 "(fst (snd (x, y, z)) = fst (snd (u, v, w))) = (y = v)" |
|
617 "(snd (snd (x, y, z)) = snd (snd (u, v, w))) = (z = w)" |
|
618 "(fst (x, y) = snd (x, y)) = (x = y)" |
|
619 "p1 = (x, y) \<and> p2 = (y, x) \<longrightarrow> fst p1 = snd p2" |
|
620 "(fst (x, y) = snd (x, y)) = (x = y)" |
|
621 "(fst p = snd p) = (p = (snd p, fst p))" |
|
622 using fst_conv snd_conv prod.collapse |
|
623 by smt+ |
|
624 |
|
625 lemma |
|
626 "x \<noteq> y \<longrightarrow> [x] \<noteq> [y]" |
|
627 "hd (x # xs) = x" |
|
628 "tl (x # xs) = xs" |
|
629 "hd [x, y, z] = x" |
|
630 "tl [x, y, z] = [y, z]" |
|
631 "hd (tl [x, y, z]) = y" |
|
632 "tl (tl [x, y, z]) = [z]" |
|
633 using list.sel(1,3) |
|
634 by smt+ |
|
635 |
|
636 lemma |
|
637 "fst (hd [(a, b)]) = a" |
|
638 "snd (hd [(a, b)]) = b" |
|
639 using fst_conv snd_conv prod.collapse list.sel(1,3) |
|
640 by smt+ |
|
641 |
|
642 |
|
643 subsubsection \<open>Records\<close> |
|
644 text \<open>The equivalent theory for Z3 contains more example, but unlike Z3, we are able |
|
645 to reconstruct the proofs.\<close> |
|
646 |
|
647 lemma |
|
648 "cx \<lparr> cx = 3, cy = 4 \<rparr> = 3" |
|
649 "cy \<lparr> cx = 3, cy = 4 \<rparr> = 4" |
|
650 "cx \<lparr> cx = 3, cy = 4 \<rparr> \<noteq> cy \<lparr> cx = 3, cy = 4 \<rparr>" |
|
651 "\<lparr> cx = 3, cy = 4 \<rparr> \<lparr> cx := 5 \<rparr> = \<lparr> cx = 5, cy = 4 \<rparr>" |
|
652 "\<lparr> cx = 3, cy = 4 \<rparr> \<lparr> cy := 6 \<rparr> = \<lparr> cx = 3, cy = 6 \<rparr>" |
|
653 "p = \<lparr> cx = 3, cy = 4 \<rparr> \<longrightarrow> p \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> = p" |
|
654 "p = \<lparr> cx = 3, cy = 4 \<rparr> \<longrightarrow> p \<lparr> cy := 4 \<rparr> \<lparr> cx := 3 \<rparr> = p" |
|
655 using point.simps |
|
656 by smt+ |
|
657 |
|
658 |
|
659 lemma |
|
660 "cx \<lparr> cx = 3, cy = 4, black = b \<rparr> = 3" |
|
661 "cy \<lparr> cx = 3, cy = 4, black = b \<rparr> = 4" |
|
662 "black \<lparr> cx = 3, cy = 4, black = b \<rparr> = b" |
|
663 "cx \<lparr> cx = 3, cy = 4, black = b \<rparr> \<noteq> cy \<lparr> cx = 3, cy = 4, black = b \<rparr>" |
|
664 "\<lparr> cx = 3, cy = 4, black = b \<rparr> \<lparr> cx := 5 \<rparr> = \<lparr> cx = 5, cy = 4, black = b \<rparr>" |
|
665 "\<lparr> cx = 3, cy = 4, black = b \<rparr> \<lparr> cy := 6 \<rparr> = \<lparr> cx = 3, cy = 6, black = b \<rparr>" |
|
666 "p = \<lparr> cx = 3, cy = 4, black = True \<rparr> \<longrightarrow> |
|
667 p \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> \<lparr> black := True \<rparr> = p" |
|
668 "p = \<lparr> cx = 3, cy = 4, black = True \<rparr> \<longrightarrow> |
|
669 p \<lparr> cy := 4 \<rparr> \<lparr> black := True \<rparr> \<lparr> cx := 3 \<rparr> = p" |
|
670 "p = \<lparr> cx = 3, cy = 4, black = True \<rparr> \<longrightarrow> |
|
671 p \<lparr> black := True \<rparr> \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> = p" |
|
672 using point.simps bw_point.simps |
|
673 by smt+ |
|
674 |
|
675 |
|
676 section \<open>Functions\<close> |
|
677 |
|
678 lemma "\<exists>f. map_option f (Some x) = Some (y + x)" |
|
679 by (smt option.map(2)) |
|
680 |
|
681 lemma |
|
682 "(f (i := v)) i = v" |
|
683 "i1 \<noteq> i2 \<longrightarrow> (f (i1 := v)) i2 = f i2" |
|
684 "i1 \<noteq> i2 \<longrightarrow> (f (i1 := v1, i2 := v2)) i1 = v1" |
|
685 "i1 \<noteq> i2 \<longrightarrow> (f (i1 := v1, i2 := v2)) i2 = v2" |
|
686 "i1 = i2 \<longrightarrow> (f (i1 := v1, i2 := v2)) i1 = v2" |
|
687 "i1 = i2 \<longrightarrow> (f (i1 := v1, i2 := v2)) i1 = v2" |
|
688 "i1 \<noteq> i2 \<and>i1 \<noteq> i3 \<and> i2 \<noteq> i3 \<longrightarrow> (f (i1 := v1, i2 := v2)) i3 = f i3" |
|
689 using fun_upd_same fun_upd_apply |
|
690 by smt+ |
|
691 |
|
692 |
|
693 section \<open>Sets\<close> |
|
694 |
|
695 lemma Empty: "x \<notin> {}" by simp |
|
696 |
|
697 lemmas smt_sets = Empty UNIV_I Un_iff Int_iff |
|
698 |
|
699 lemma |
|
700 "x \<notin> {}" |
|
701 "x \<in> UNIV" |
|
702 "x \<in> A \<union> B \<longleftrightarrow> x \<in> A \<or> x \<in> B" |
|
703 "x \<in> P \<union> {} \<longleftrightarrow> x \<in> P" |
|
704 "x \<in> P \<union> UNIV" |
|
705 "x \<in> P \<union> Q \<longleftrightarrow> x \<in> Q \<union> P" |
|
706 "x \<in> P \<union> P \<longleftrightarrow> x \<in> P" |
|
707 "x \<in> P \<union> (Q \<union> R) \<longleftrightarrow> x \<in> (P \<union> Q) \<union> R" |
|
708 "x \<in> A \<inter> B \<longleftrightarrow> x \<in> A \<and> x \<in> B" |
|
709 "x \<notin> P \<inter> {}" |
|
710 "x \<in> P \<inter> UNIV \<longleftrightarrow> x \<in> P" |
|
711 "x \<in> P \<inter> Q \<longleftrightarrow> x \<in> Q \<inter> P" |
|
712 "x \<in> P \<inter> P \<longleftrightarrow> x \<in> P" |
|
713 "x \<in> P \<inter> (Q \<inter> R) \<longleftrightarrow> x \<in> (P \<inter> Q) \<inter> R" |
|
714 "{x. x \<in> P} = {y. y \<in> P}" |
|
715 by (smt smt_sets)+ |
|
716 |
|
717 end |