1(* Copyright (c) 2009-2012 Tjark Weber. All rights reserved. *)
2
3(* Unit tests for HolSmtLib *)
4
5val _ = print "Testing HolSmtLib\n"
6
7(*****************************************************************************)
8(* tracing/pretty-printing options useful for debugging                      *)
9(*****************************************************************************)
10
11(*
12val _ = Globals.show_tags := true
13val _ = Globals.show_assums := true
14val _ = Globals.show_types := true
15val _ = wordsLib.add_word_cast_printer ()
16*)
17
18val _ = Feedback.set_trace "HolSmtLib" 0
19(*
20val _ = Feedback.set_trace "HolSmtLib" 4
21*)
22
23(*****************************************************************************)
24(* check whether SMT solvers are installed                                   *)
25(*****************************************************************************)
26
27val _ = if Yices.is_configured () then () else
28  print "(Yices not configured, some tests will be skipped.)\n"
29
30val _ = if Z3.is_configured () then () else
31  print "(Z3 not configured, some tests will be skipped.)\n"
32
33(*****************************************************************************)
34(* utility functions                                                         *)
35(*****************************************************************************)
36
37local
38
39fun die s =
40  if !Globals.interactive then
41    raise (Fail s)
42  else (
43    print ("\n" ^ s ^ "\n");
44    OS.Process.exit OS.Process.failure
45  )
46
47(* provable terms: theorem expected *)
48fun expect_thm name smt_tac t =
49  let
50    open boolLib
51    val thm = Tactical.TAC_PROOF (([], t), smt_tac)
52      handle Feedback.HOL_ERR {origin_structure, origin_function, message} =>
53        die ("Test of solver '" ^ name ^ "' failed on term '" ^
54          Hol_pp.term_to_string t ^ "': exception HOL_ERR (in " ^
55          origin_structure ^ "." ^ origin_function ^ ", message: " ^ message ^
56          ")")
57  in
58    if null (Thm.hyp thm) andalso Thm.concl thm ~~ t then ()
59    else
60      die ("Test of solver '" ^ name ^ "' failed on term '" ^
61        Hol_pp.term_to_string t ^ "': theorem differs (" ^
62        Hol_pp.thm_to_string thm ^ ")")
63  end
64
65(* unprovable terms: satisfiability expected *)
66fun expect_sat name smt_tac t =
67  let
68    val _ = Tactical.TAC_PROOF (([], t), smt_tac)
69  in
70    die ("Test of solver '" ^ name ^ "' failed on term '" ^
71      Hol_pp.term_to_string t ^ "': exception expected")
72  end handle Feedback.HOL_ERR {origin_structure, origin_function, message} =>
73    if origin_structure = "HolSmtLib" andalso
74       origin_function = "GENERIC_SMT_TAC" andalso
75       (message = "solver reports negated term to be 'satisfiable'" orelse
76        message = "solver reports negated term to be 'satisfiable' (model returned)")
77    then
78      ()
79    else
80      die ("Test of solver '" ^ name ^ "' failed on term '" ^
81        Hol_pp.term_to_string t ^
82        "': exception HOL_ERR has unexpected argument values (in " ^
83        origin_structure ^ "." ^ origin_function ^ ", message: " ^ message ^
84        ")")
85
86fun mk_test_fun is_configured expect_fun name smt_tac =
87  if is_configured then
88    (fn g => (expect_fun name smt_tac g; print "."))
89  else
90    Lib.K ()
91
92(*****************************************************************************)
93(* a built-in automated semi-decision procedure that *very* loosely          *)
94(* resembles SMT solvers (in terms of coverage; not so much in terms of      *)
95(* performance)                                                              *)
96(*****************************************************************************)
97
98fun auto_tac (_, t) =
99  let
100    val simpset = bossLib.++ (bossLib.srw_ss (), wordsLib.WORD_ss)
101    val t_eq_t' = simpLib.SIMP_CONV simpset [integerTheory.INT_ABS,
102      integerTheory.INT_MAX, integerTheory.INT_MIN]
103      t
104      handle Conv.UNCHANGED =>
105        Thm.REFL t
106    val t' = boolSyntax.rhs (Thm.concl t_eq_t')
107    val t'_thm = bossLib.DECIDE t'
108      handle Feedback.HOL_ERR _ =>
109        bossLib.METIS_PROVE [] t'
110      handle Feedback.HOL_ERR _ =>
111        intLib.ARITH_PROVE t'
112      handle Feedback.HOL_ERR _ =>
113        realLib.REAL_ARITH t'
114      handle Feedback.HOL_ERR _ =>
115        wordsLib.WORD_DECIDE t'
116      handle Feedback.HOL_ERR _ =>
117        Tactical.prove (t', blastLib.BBLAST_TAC)
118    val thm = Thm.EQ_MP (Thm.SYM t_eq_t') t'_thm
119  in
120    ([], fn _ => thm)
121  end
122
123val thm_AUTO =
124  mk_test_fun true expect_thm "AUTO" (Tactical.THEN (Library.SET_SIMP_TAC, auto_tac))
125
126fun mk_Yices expect_fun =
127  mk_test_fun (Yices.is_configured ()) expect_fun "Yices" HolSmtLib.YICES_TAC
128
129val thm_YO = mk_Yices expect_thm
130val sat_YO = mk_Yices expect_sat
131
132fun mk_Z3 expect_fun =
133  mk_test_fun (Z3.is_configured ()) expect_fun "Z3" HolSmtLib.Z3_ORACLE_TAC
134
135val thm_Z3 = mk_Z3 expect_thm
136val sat_Z3 = mk_Z3 expect_sat
137
138fun mk_Z3p expect_fun =
139  mk_test_fun (Z3.is_configured ()) expect_fun "Z3 (proofs)" HolSmtLib.Z3_TAC
140
141val thm_Z3p = mk_Z3p expect_thm
142val sat_Z3p = mk_Z3p expect_sat
143
144(*****************************************************************************)
145(* HOL definitions (e.g., user-defined data types)                           *)
146(*****************************************************************************)
147
148val _ = bossLib.Hol_datatype `dt1 = foo | bar | baz`
149
150val _ = bossLib.Hol_datatype `person = <| employed :bool; age :num |>`
151
152in
153
154(*****************************************************************************)
155(* test cases                                                                *)
156(*****************************************************************************)
157
158  val tests = [
159
160    (* propositional logic *)
161    (``T``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
162    (``F``, [sat_YO, sat_Z3, sat_Z3p]),
163    (``p = (p:bool)``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
164    (``p ==> p``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
165    (``p \/ ~ p``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
166    (``p /\ q ==> q /\ p``,
167      [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
168    (``(p ==> q) /\ (q ==> p) ==> (p = q)``,
169      [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
170    (``(p ==> q) /\ (q ==> p) <=> (p = q)``,
171      [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
172    (``p \/ q ==> p /\ q``, [sat_YO, sat_Z3, sat_Z3p]),
173    (``if p then (q ==> p) else (p ==> q)``,
174      [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
175    (``case p of T => p | F => ~ p``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
176    (``case p of T => (q ==> p) | F => (p ==> q)``,
177      [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
178
179    (* numerals *)
180
181    (* FIXME: SMT-LIB 2 does not provide a theory of natural numbers, but only
182              integers and reals.  We should add support for naturals (via an
183              embedding into integers), but for now, they are treated as
184              uninterpreted. *)
185
186    (* num *)
187
188    (``0n = 0n``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
189    (``1n = 1n``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
190    (``0n = 1n``, [sat_YO, sat_Z3, sat_Z3p]),
191    (``42n = 42n``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
192
193    (* int *)
194
195    (``0i = 0i``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
196    (``1i = 1i``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
197    (``0i = 1i``, [sat_YO, sat_Z3, sat_Z3p]),
198    (``42i = 42i``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
199    (``0i = ~0i``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
200    (``~0i = 0i``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
201    (``~0i = ~0i``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
202    (``~42i = ~42i``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
203
204    (* real *)
205
206    (* Z3 2.19 prints reals as integers in its proofs; I see no way to
207       reliably distinguish between them. *)
208
209    (``0r = 0r``, [thm_AUTO, thm_YO, thm_Z3(*, thm_Z3p*)]),
210    (``1r = 1r``, [thm_AUTO, thm_YO, thm_Z3(*, thm_Z3p*)]),
211    (``0r = 1r``, [sat_YO, sat_Z3, sat_Z3p]),
212    (``42r = 42r``, [thm_AUTO, thm_YO, thm_Z3(*, thm_Z3p*)]),
213    (``0r = ~0r``, [thm_AUTO, thm_YO, thm_Z3(*, thm_Z3p*)]),
214    (``~0r = 0r``, [thm_AUTO, thm_YO, thm_Z3(*, thm_Z3p*)]),
215    (``~0r = ~0r``, [thm_AUTO, thm_YO, thm_Z3(*, thm_Z3p*)]),
216    (``~42r = ~42r``, [thm_AUTO, thm_YO, thm_Z3(*, thm_Z3p*)]),
217    (``~42r = 42r``, [sat_YO, sat_Z3, sat_Z3p]),
218    (``42r = ~42r``, [sat_YO, sat_Z3, sat_Z3p]),
219
220    (* arithmetic operators: SUC, +, -, *, /, DIV, MOD, ABS, MIN, MAX *)
221
222    (* num *)
223
224    (``SUC 0 = 1``, [thm_AUTO, thm_YO]),
225    (``SUC x = x + 1``, [thm_AUTO, thm_YO]),
226    (``x < SUC x``, [thm_AUTO, thm_YO]),
227    (``(SUC x = SUC y) = (x = y)``, [thm_AUTO, thm_YO]),
228    (``SUC (x + y) = (SUC x + SUC y)``, [sat_YO, sat_Z3, sat_Z3p]),
229
230    (``(x:num) + 0 = x``, [thm_AUTO, thm_YO]),
231    (``0 + (x:num) = x``, [thm_AUTO, thm_YO]),
232    (``(x:num) + y = y + x``, [thm_AUTO, thm_YO]),
233    (``(x:num) + (y + z) = (x + y) + z``, [thm_AUTO, thm_YO]),
234    (``((x:num) + y = 0) <=> (x = 0) /\ (y = 0)``, [thm_AUTO, thm_YO]),
235
236    (``(x:num) - 0 = x``, [thm_AUTO, thm_YO]),
237    (``(x:num) - y = y - x``, [sat_YO, sat_Z3, sat_Z3p]),
238    (``(x:num) - y - z = x - (y + z)``, [thm_AUTO, thm_YO]),
239    (``(x:num) <= y ==> (x - y = 0)``, [thm_AUTO, thm_YO]),
240    (``((x:num) - y = 0) \/ (y - x = 0)``, [thm_AUTO, thm_YO]),
241
242    (``(x:num) * 0 = 0``, [thm_AUTO, thm_YO]),
243    (``0 * (x:num) = 0``, [thm_AUTO, thm_YO]),
244    (``(x:num) * 1 = x``, [thm_AUTO, thm_YO]),
245    (``1 * (x:num) = x``, [thm_AUTO, thm_YO]),
246    (``(x:num) * 42 = 42 * x``, [thm_AUTO, thm_YO]),
247
248    (``(0:num) DIV 1 = 0``, [thm_AUTO, thm_YO]),
249    (``(1:num) DIV 1 = 1``, [thm_AUTO, thm_YO]),
250    (``(42:num) DIV 1 = 42``, [thm_AUTO, thm_YO]),
251    (``(0:num) DIV 42 = 0``, [thm_AUTO, thm_YO]),
252    (``(1:num) DIV 42 = 0``, [thm_AUTO, thm_YO]),
253    (``(42:num) DIV 42 = 1``, [thm_AUTO, thm_YO]),
254    (``(x:num) DIV 1 = x``, [thm_AUTO, thm_YO]),
255    (``(x:num) DIV 42 <= x``, [thm_AUTO, thm_YO]),
256    (``((x:num) DIV 42 = x) = (x = 0)``, [thm_AUTO, thm_YO]),
257    (``(x:num) DIV 0 = x``, [sat_YO, sat_Z3, sat_Z3p]),
258    (``(x:num) DIV 0 = 0``, [sat_YO, sat_Z3, sat_Z3p]),
259    (``(0:num) DIV 0 = 0``, [sat_YO, sat_Z3, sat_Z3p]),
260    (``(0:num) DIV 0 = 1``, [sat_YO, sat_Z3, sat_Z3p]),
261    (``(x:num) DIV 0 = x DIV 0``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
262
263    (``(0:num) MOD 1 = 0``, [thm_AUTO, thm_YO]),
264    (``(1:num) MOD 1 = 0``, [thm_AUTO, thm_YO]),
265    (``(42:num) MOD 1 = 0``, [thm_AUTO, thm_YO]),
266    (``(0:num) MOD 42 = 0``, [thm_AUTO, thm_YO]),
267    (``(1:num) MOD 42 = 1``, [thm_AUTO, thm_YO]),
268    (``(42:num) MOD 42 = 0``, [thm_AUTO, thm_YO]),
269    (``(x:num) MOD 1 = 0``, [thm_AUTO, thm_YO]),
270    (``(x:num) MOD 42 < 42``, [thm_AUTO, thm_YO]),
271    (``((x:num) MOD 42 = x) = (x < 42)``, [thm_AUTO, thm_YO]),
272    (``(x:num) MOD 0 = x``, [sat_YO, sat_Z3, sat_Z3p]),
273    (``(x:num) MOD 0 = 0``, [sat_YO, sat_Z3, sat_Z3p]),
274    (``(0:num) MOD 0 = 0``, [sat_YO, sat_Z3, sat_Z3p]),
275    (``(0:num) MOD 0 = 1``, [sat_YO, sat_Z3, sat_Z3p]),
276    (``(x:num) MOD 0 = x MOD 0``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
277
278    (* cf. arithmeticTheory.DIVISION *)
279    (``((x:num) = x DIV 1 * 1 + x MOD 1) /\ x MOD 1 < 1``, [thm_AUTO, thm_YO]),
280    (``((x:num) = x DIV 42 * 42 + x MOD 42) /\ x MOD 42 < 42``,
281      [thm_AUTO, thm_YO]),
282
283    (``MIN (x:num) y <= x``, [thm_AUTO, thm_YO]),
284    (``MIN (x:num) y <= y``, [thm_AUTO, thm_YO]),
285    (``(z:num) < x /\ z < y ==> z < MIN x y``, [thm_AUTO, thm_YO]),
286    (``MIN (x:num) y < x``, [sat_YO, sat_Z3, sat_Z3p]),
287    (``MIN (x:num) 0 = 0``, [thm_AUTO, thm_YO]),
288
289    (``MAX (x:num) y >= x``, [(*thm_AUTO,*) thm_YO]),
290    (``MAX (x:num) y >= y``, [(*thm_AUTO,*) thm_YO]),
291    (``(z:num) > x /\ z > y ==> z > MAX x y``, [(*thm_AUTO,*) thm_YO]),
292    (``MAX (x:num) y > x``, [sat_YO, sat_Z3, sat_Z3p]),
293    (``MAX (x:num) 0 = x``, [thm_AUTO, thm_YO]),
294
295    (* int *)
296
297    (``(x:int) + 0 = x``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
298    (``0 + (x:int) = x``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
299    (``(x:int) + y = y + x``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
300    (``(x:int) + (y + z) = (x + y) + z``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
301    (``((x:int) + y = 0) = (x = 0) /\ (y = 0)``, [sat_YO, sat_Z3, sat_Z3p]),
302    (``((x:int) + y = 0) = (x = ~y)``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
303
304    (``(x:int) - 0 = x``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
305    (``(x:int) - y = y - x``, [sat_YO, sat_Z3, sat_Z3p]),
306    (``(x:int) - y - z = x - (y + z)``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
307    (``(x:int) <= y ==> (x - y = 0)``, [sat_YO, sat_Z3, sat_Z3p]),
308    (``((x:int) - y = 0) \/ (y - x = 0)``, [sat_YO, sat_Z3, sat_Z3p]),
309    (``(x:int) - y = x + ~y``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
310
311    (``(x:int) * 0 = 0``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
312    (``0 * (x:int) = 0``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
313    (``(x:int) * 1 = x``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
314    (``1 * (x:int) = x``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
315    (``(x:int) * ~1 = ~x``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
316    (``~1 * (x:int) = ~x``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
317    (``(x:int) * 42 = 42 * x``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
318
319    (``(~42:int) / ~42 = 1``, [thm_AUTO, thm_YO]),
320    (``(~1:int) / ~42 = 0``, [thm_AUTO, thm_YO]),
321    (``(0:int) / ~42 = 0``, [thm_AUTO, thm_YO]),
322    (``(1:int) / ~42 = ~1``, [thm_AUTO, thm_YO]),
323    (``(42:int) / ~42 = ~1``, [thm_AUTO, thm_YO]),
324    (``(~42:int) / ~1 = 42``, [thm_AUTO, thm_YO]),
325    (``(~1:int) / ~1 = 1``, [thm_AUTO, thm_YO]),
326    (``(0:int) / ~1 = 0``, [thm_AUTO, thm_YO]),
327    (``(1:int) / ~1 = ~1``, [thm_AUTO, thm_YO]),
328    (``(42:int) / ~1 = ~42``, [thm_AUTO, thm_YO]),
329    (``(~42:int) / 1 = ~42``, [thm_AUTO, thm_YO]),
330    (``(~1:int) / 1 = ~1``, [thm_AUTO, thm_YO]),
331    (``(0:int) / 1 = 0``, [thm_AUTO, thm_YO]),
332    (``(1:int) / 1 = 1``, [thm_AUTO, thm_YO]),
333    (``(42:int) / 1 = 42``, [thm_AUTO, thm_YO]),
334    (``(~42:int) / 42 = ~1``, [thm_AUTO, thm_YO]),
335    (``(~1:int) / 42 = ~1``, [thm_AUTO, thm_YO]),
336    (``(0:int) / 42 = 0``, [thm_AUTO, thm_YO]),
337    (``(1:int) / 42 = 0``, [thm_AUTO, thm_YO]),
338    (``(42:int) / 42 = 1``, [thm_AUTO, thm_YO]),
339    (``(x:int) / 1 = x``, [thm_AUTO, thm_YO]),
340    (``(x:int) / ~1 = ~x``, [thm_AUTO, thm_YO]),
341    (``(x:int) / 42 <= x``, [sat_YO, sat_Z3, sat_Z3p]),
342    (``(x:int) / 42 <= ABS x``, [thm_AUTO, thm_YO(*, thm_Z3, thm_Z3p*)]),
343    (``((x:int) / 42 = x) = (x = 0)``, [sat_YO, sat_Z3, sat_Z3p]),
344    (``((x:int) / 42 = x) = (x = 0) \/ (x = ~1)``, [thm_AUTO, thm_YO]),
345    (``(x:int) / 0 = x``, [sat_YO, sat_Z3, sat_Z3p]),
346    (``(x:int) / 0 = 0``, [sat_YO, sat_Z3, sat_Z3p]),
347    (``(0:int) / 0 = 0``, [sat_YO, sat_Z3, sat_Z3p]),
348    (``(0:int) / 0 = 1``, [sat_YO, sat_Z3, sat_Z3p]),
349    (``(0:int) / 0 = 1 / 0``, [sat_YO, sat_Z3, sat_Z3p]),
350    (``(x:int) / 0 = x / 0``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
351
352    (* cf. integerTheory.int_div *)
353    (``(x:int) < 0 ==> (x / 1 = ~(~x / 1) + if ~x % 1 = 0 then 0 else ~1)``,
354      [thm_AUTO, thm_YO]),
355    (``(x:int) < 0 ==> (x / 42 = ~(~x / 42) + if ~x % 42 = 0 then 0 else ~1)``,
356      [thm_AUTO, thm_YO]),
357    (``0 <= (x:int) ==> (x / ~42 = ~(x / 42) + if x % 42 = 0 then 0 else ~1)``,
358      [thm_AUTO, thm_YO]),
359    (``0 <= (x:int) ==> (x / ~1 = ~(x / 1) + if x % 1 = 0 then 0 else ~1)``,
360      [thm_AUTO, thm_YO]),
361    (``(x:int) < 0 ==> (x / ~42 = ~x / 42)``, [thm_AUTO, thm_YO]),
362    (``(x:int) < 0 ==> (x / ~1 = ~x / 1)``, [thm_AUTO, thm_YO]),
363
364    (``(~42:int) % ~42 = 0``, [thm_AUTO, thm_YO]),
365    (``(~1:int) % ~42 = ~1``, [thm_AUTO, thm_YO]),
366    (``(0:int) % ~42 = 0``, [thm_AUTO, thm_YO]),
367    (``(1:int) % ~42 = ~41``, [thm_AUTO, thm_YO]),
368    (``(42:int) % ~42 = 0``, [thm_AUTO, thm_YO]),
369    (``(~42:int) % ~1 = 0``, [thm_AUTO, thm_YO]),
370    (``(~1:int) % ~1 = 0``, [thm_AUTO, thm_YO]),
371    (``(0:int) % ~1 = 0``, [thm_AUTO, thm_YO]),
372    (``(1:int) % ~1 = 0``, [thm_AUTO, thm_YO]),
373    (``(42:int) % ~1 = 0``, [thm_AUTO, thm_YO]),
374    (``(~42:int) % 1 = 0``, [thm_AUTO, thm_YO]),
375    (``(~1:int) % 1 = 0``, [thm_AUTO, thm_YO]),
376    (``(0:int) % 1 = 0``, [thm_AUTO, thm_YO]),
377    (``(1:int) % 1 = 0``, [thm_AUTO, thm_YO]),
378    (``(42:int) % 1 = 0``, [thm_AUTO, thm_YO]),
379    (``(~42:int) % 42 = 0``, [thm_AUTO, thm_YO]),
380    (``(~1:int) % 42 = 41``, [thm_AUTO, thm_YO]),
381    (``(0:int) % 42 = 0``, [thm_AUTO, thm_YO]),
382    (``(1:int) % 42 = 1``, [thm_AUTO, thm_YO]),
383    (``(42:int) % 42 = 0``, [thm_AUTO, thm_YO]),
384    (``(x:int) % 1 = 0``, [thm_AUTO, thm_YO]),
385    (``(x:int) % ~1 = 0``, [thm_AUTO, thm_YO]),
386    (``(x:int) % 42 < 42``, [thm_AUTO, thm_YO]),
387    (``((x:int) % 42 = x) = (x < 42)``, [sat_YO, sat_Z3, sat_Z3p]),
388    (``((x:int) % 42 = x) <=> (0 <= x) /\ (x < 42)``, [thm_AUTO, thm_YO]),
389    (``(x:int) % 0 = x``, [sat_YO, sat_Z3, sat_Z3p]),
390    (``(x:int) % 0 = 0``, [sat_YO, sat_Z3, sat_Z3p]),
391    (``(0:int) % 0 = 0``, [sat_YO, sat_Z3, sat_Z3p]),
392    (``(0:int) % 0 = 1``, [sat_YO, sat_Z3, sat_Z3p]),
393    (``(x:int) % 0 = x % 0``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
394
395    (* cf. integerTheory.int_mod *)
396    (``(x:int) % ~42 = x - x / ~42 * ~42``, [thm_AUTO, thm_YO]),
397    (``(x:int) % ~1 = x - x / ~1 * ~1``, [thm_AUTO, thm_YO]),
398    (``(x:int) % 1 = x - x / 1 * 1``, [thm_AUTO, thm_YO]),
399    (``(x:int) % 42 = x - x / 42 * 42``, [thm_AUTO, thm_YO]),
400
401    (``ABS (x:int) >= 0``, [thm_AUTO, thm_YO(*, thm_Z3, thm_Z3p*)]),
402    (``(ABS (x:int) = 0) = (x = 0)``, [thm_AUTO, thm_YO(*, thm_Z3, thm_Z3p*)]),
403    (``(x:int) >= 0 ==> (ABS x = x)``, [thm_AUTO, thm_YO(*, thm_Z3, thm_Z3p*)]),
404    (``(x:int) <= 0 ==> (ABS x = ~x)``, [thm_AUTO, thm_YO(*, thm_Z3, thm_Z3p*)]),
405    (``ABS (ABS (x:int)) = ABS x``, [thm_AUTO, thm_YO(*, thm_Z3, thm_Z3p*)]),
406    (``ABS (x:int) = x``, [sat_YO, sat_Z3, sat_Z3p]),
407
408    (``int_min (x:int) y <= x``, [thm_AUTO, thm_YO]),
409    (``int_min (x:int) y <= y``, [thm_AUTO, thm_YO]),
410    (``(z:int) < x /\ z < y ==> z < int_min x y``, [thm_AUTO, thm_YO]),
411    (``int_min (x:int) y < x``, [sat_YO, sat_Z3, sat_Z3p]),
412    (``int_min (x:int) 0 = 0``, [sat_YO, sat_Z3, sat_Z3p]),
413    (``(x:int) >= 0 ==> (int_min x 0 = 0)``, [thm_AUTO, thm_YO]),
414
415    (``int_max (x:int) y >= x``, [thm_AUTO, thm_YO]),
416    (``int_max (x:int) y >= y``, [thm_AUTO, thm_YO]),
417    (``(z:int) > x /\ z > y ==> z > int_max x y``, [thm_AUTO, thm_YO]),
418    (``int_max (x:int) y > x``, [sat_YO, sat_Z3, sat_Z3p]),
419    (``(x:int) >= 0 ==> (int_max x 0 = x)``, [thm_AUTO, thm_YO]),
420
421    (* real *)
422
423    (``(x:real) + 0 = x``, [thm_AUTO, thm_YO, thm_Z3(*, thm_Z3p*)]),
424    (``0 + (x:real) = x``, [thm_AUTO, thm_YO, thm_Z3(*, thm_Z3p*)]),
425    (``(x:real) + y = y + x``, [thm_AUTO, thm_YO, thm_Z3(*, thm_Z3p*)]),
426    (``(x:real) + (y + z) = (x + y) + z``, [thm_AUTO, thm_YO, thm_Z3(*, thm_Z3p*)]),
427    (``((x:real) + y = 0) = (x = 0) /\ (y = 0)``, [sat_YO, sat_Z3, sat_Z3p]),
428    (``((x:real) + y = 0) = (x = ~y)``, [thm_AUTO, thm_YO, thm_Z3(*, thm_Z3p*)]),
429
430    (``(x:real) - 0 = x``, [thm_AUTO, thm_YO]),
431    (``(x:real) - y = y - x``, [sat_YO, sat_Z3, sat_Z3p]),
432    (``(x:real) - y - z = x - (y + z)``, [thm_AUTO, thm_YO]),
433    (``(x:real) <= y ==> (x - y = 0)``, [sat_YO, sat_Z3, sat_Z3p]),
434    (``((x:real) - y = 0) \/ (y - x = 0)``, [sat_YO, sat_Z3, sat_Z3p]),
435    (``(x:real) - y = x + ~y``, [thm_AUTO, thm_YO]),
436
437    (``(x:real) * 0 = 0``, [thm_AUTO, thm_YO]),
438    (``0 * (x:real) = 0``, [thm_AUTO, thm_YO]),
439    (``(x:real) * 1 = x``, [thm_AUTO, thm_YO]),
440    (``1 * (x:real) = x``, [thm_AUTO, thm_YO]),
441    (``(x:real) * 42 = 42 * x``, [thm_AUTO, thm_YO]),
442
443    (``(x:real) / 1 = x``, [thm_AUTO, thm_YO]),
444    (``x > 0 ==> (x:real) / 42 < x``, [(*thm_AUTO,*) thm_YO]),
445    (``x < 0 ==> (x:real) / 42 > x``, [(*thm_AUTO,*) thm_YO]),
446
447    (``abs (x:real) >= 0``, [thm_AUTO, thm_YO]),
448    (``(abs (x:real) = 0) = (x = 0)``, [thm_AUTO, thm_YO]),
449    (``(x:real) >= 0 ==> (abs x = x)``, [thm_AUTO, thm_YO]),
450    (``(x:real) <= 0 ==> (abs x = ~x)``, [thm_AUTO, thm_YO]),
451    (``abs (abs (x:real)) = abs x``, [thm_AUTO, thm_YO]),
452    (``abs (x:real) = x``, [sat_YO, sat_Z3, sat_Z3p]),
453
454    (``min (x:real) y <= x``, [(*thm_AUTO,*) thm_YO]),
455    (``min (x:real) y <= y``, [(*thm_AUTO,*) thm_YO]),
456    (``(z:real) < x /\ z < y ==> z < min x y``, [(*thm_AUTO,*) thm_YO]),
457    (``min (x:real) y < x``, [sat_YO, sat_Z3, sat_Z3p]),
458    (``min (x:real) 0 = 0``, [sat_YO, sat_Z3, sat_Z3p]),
459    (``(x:real) >= 0 ==> (min x 0 = 0)``, [(*thm_AUTO,*) thm_YO]),
460
461    (``max (x:real) y >= x``, [(*thm_AUTO,*) thm_YO]),
462    (``max (x:real) y >= y``, [(*thm_AUTO,*) thm_YO]),
463    (``(z:real) > x /\ z > y ==> z > max x y``, [(*thm_AUTO,*) thm_YO]),
464    (``max (x:real) y > x``, [sat_YO, sat_Z3, sat_Z3p]),
465    (``(x:real) >= 0 ==> (max x 0 = x)``, [(*thm_AUTO,*) thm_YO]),
466
467    (* arithmetic inequalities: <, <=, >, >= *)
468
469    (* num *)
470
471    (``0n < 1n``, [thm_AUTO, thm_YO]),
472    (``1n < 0n``, [sat_YO, sat_Z3, sat_Z3p]),
473    (``(x:num) < x``, [sat_YO, sat_Z3, sat_Z3p]),
474    (``(x:num) < y ==> 42 * x < 42 * y``, [thm_AUTO, thm_YO]),
475
476    (``0n <= 1n``, [thm_AUTO, thm_YO]),
477    (``1n <= 0n``, [sat_YO, sat_Z3, sat_Z3p]),
478    (``(x:num) <= x``, [thm_AUTO, thm_YO]),
479    (``(x:num) <= y ==> 42 * x <= 42 * y``, [thm_AUTO, thm_YO]),
480
481    (``1n > 0n``, [thm_AUTO, thm_YO]),
482    (``0n > 1n``, [sat_YO, sat_Z3, sat_Z3p]),
483    (``(x:num) > x``, [sat_YO, sat_Z3, sat_Z3p]),
484    (``(x:num) > y ==> 42 * x > 42 * y``, [thm_AUTO, thm_YO]),
485
486    (``1n >= 0n``, [thm_AUTO, thm_YO]),
487    (``0n >= 1n``, [sat_YO, sat_Z3, sat_Z3p]),
488    (``(x:num) >= x``, [thm_AUTO, thm_YO]),
489    (``(x:num) >= y ==> 42 * x >= 42 * y``, [thm_AUTO, thm_YO]),
490
491    (``((x:num) < y) = (y > x)``, [thm_AUTO, thm_YO]),
492    (``((x:num) <= y) = (y >= x)``, [thm_AUTO, thm_YO]),
493    (``(x:num) < y /\ y <= z ==> x < z``, [thm_AUTO, thm_YO]),
494    (``(x:num) <= y /\ y <= z ==> x <= z``, [thm_AUTO, thm_YO]),
495    (``(x:num) > y /\ y >= z ==> x > z``, [thm_AUTO, thm_YO]),
496    (``(x:num) >= y /\ y >= z ==> x >= z``, [thm_AUTO, thm_YO]),
497
498    (``(x:num) >= 0``, [thm_AUTO, thm_YO]),
499    (``0 < (x:num) /\ x <= 1 ==> (x = 1)``, [thm_AUTO, thm_YO]),
500
501    (* int *)
502
503    (``0i < 1i``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
504    (``1i < 0i``, [sat_YO, sat_Z3, sat_Z3p]),
505    (``(x:int) < x``, [sat_YO, sat_Z3, sat_Z3p]),
506    (``(x:int) < y ==> 42 * x < 42 * y``,
507      [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
508
509    (``0i <= 1i``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
510    (``1i <= 0i``, [sat_YO, sat_Z3, sat_Z3p]),
511    (``(x:int) <= x``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
512    (``(x:int) <= y ==> 42 * x <= 42 * y``,
513      [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
514
515    (``1i > 0i``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
516    (``0i > 1i``, [sat_YO, sat_Z3, sat_Z3p]),
517    (``(x:int) > x``, [sat_YO, sat_Z3, sat_Z3p]),
518    (``(x:int) > y ==> 42 * x > 42 * y``,
519      [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
520
521    (``1i >= 0i``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
522    (``0i >= 1i``, [sat_YO, sat_Z3, sat_Z3p]),
523    (``(x:int) >= x``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
524    (``(x:int) >= y ==> 42 * x >= 42 * y``,
525      [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
526
527    (``((x:int) < y) = (y > x)``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
528    (``((x:int) <= y) = (y >= x)``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
529    (``(x:int) < y /\ y <= z ==> x < z``, [thm_AUTO, thm_YO, thm_Z3(*, thm_Z3p*)]),
530    (``(x:int) <= y /\ y <= z ==> x <= z``, [thm_AUTO, thm_YO, thm_Z3(*, thm_Z3p*)]),
531    (``(x:int) > y /\ y >= z ==> x > z``, [thm_AUTO, thm_YO, thm_Z3(*, thm_Z3p*)]),
532    (``(x:int) >= y /\ y >= z ==> x >= z``, [thm_AUTO, thm_YO, thm_Z3(*, thm_Z3p*)]),
533
534    (``(x:int) >= 0``, [sat_YO, sat_Z3, sat_Z3p]),
535    (``0 < (x:int) /\ x <= 1 ==> (x = 1)``, [thm_AUTO, thm_YO, thm_Z3(*, thm_Z3p*)]),
536
537    (* real *)
538
539    (``0r < 1r``, [thm_AUTO, thm_YO]),
540    (``1r < 0r``, [sat_YO, sat_Z3, sat_Z3p]),
541    (``(x:real) < x``, [sat_YO, sat_Z3, sat_Z3p]),
542    (``(x:real) < y ==> 42 * x < 42 * y``, [thm_AUTO, thm_YO]),
543
544    (``0n <= 1n``, [thm_AUTO, thm_YO]),
545    (``1n <= 0n``, [sat_YO, sat_Z3, sat_Z3p]),
546    (``(x:num) <= x``, [thm_AUTO, thm_YO]),
547    (``(x:num) <= y ==> 2 * x <= 2 * y``, [thm_AUTO, thm_YO]),
548
549    (``1r > 0r``, [thm_AUTO, thm_YO]),
550    (``0r > 1r``, [sat_YO, sat_Z3, sat_Z3p]),
551    (``(x:real) > x``, [sat_YO, sat_Z3, sat_Z3p]),
552    (``(x:real) > y ==> 42 * x > 42 * y``, [thm_AUTO, thm_YO]),
553
554    (``1r >= 0r``, [thm_AUTO, thm_YO]),
555    (``0r >= 1r``, [sat_YO, sat_Z3, sat_Z3p]),
556    (``(x:real) >= x``, [thm_AUTO, thm_YO]),
557    (``(x:real) >= y ==> 42 * x >= 42 * y``, [thm_AUTO, thm_YO]),
558
559    (``((x:real) < y) = (y > x)``, [thm_AUTO, thm_YO]),
560    (``((x:real) <= y) = (y >= x)``, [thm_AUTO, thm_YO]),
561    (``(x:real) < y /\ y <= z ==> x < z``, [thm_AUTO, thm_YO]),
562    (``(x:real) <= y /\ y <= z ==> x <= z``, [thm_AUTO, thm_YO]),
563    (``(x:real) > y /\ y >= z ==> x > z``, [thm_AUTO, thm_YO]),
564    (``(x:real) >= y /\ y >= z ==> x >= z``, [thm_AUTO, thm_YO]),
565
566    (``(x:real) >= 0``, [sat_YO, sat_Z3, sat_Z3p]),
567    (``0 < (x:real) /\ x <= 1 ==> (x = 1)``,
568      [sat_YO, sat_Z3, sat_Z3p]),
569
570    (* uninterpreted functions *)
571
572    (``(x = y) ==> (f x = f y)``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
573    (``(x = y) ==> (f x y = f y x)``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
574    (``(f (f x) = x) /\ (f (f (f (f (f x)))) = x) ==> (f x = x)``,
575      [(*thm_AUTO,*) thm_YO, thm_Z3, thm_Z3p]),
576    (``(f x = f y) ==> (x = y)``, [sat_YO, sat_Z3, sat_Z3p]),
577
578    (* predicates *)
579
580    (``P x ==> P x``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
581    (``P x ==> Q x``, [sat_YO, sat_Z3, sat_Z3p]),
582    (``P x ==> P y``, [sat_YO, sat_Z3, sat_Z3p]),
583    (``P x y ==> P x x``, [sat_YO, sat_Z3, sat_Z3p]),
584    (``P x y ==> P y x``, [sat_YO, sat_Z3, sat_Z3p]),
585    (``P x y ==> P y y``, [sat_YO, sat_Z3, sat_Z3p]),
586
587    (* quantifiers *)
588
589    (``!x. x = x``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
590    (* Yices 1.0.28 reports `unknown' for the next goal, while Z3 2.13
591       (somewhat surprisingly, as SMT-LIB does not seem to require
592       non-empty sorts) can prove it *)
593    (``?x. x = x``, [thm_AUTO, thm_Z3(*, thm_Z3p*)]),
594    (* Z3 2.13 reports `unknown' for the next goal *)
595    (``(?y. !x. P x y) ==> (!x. ?y. P x y)``, [thm_AUTO, thm_YO]),
596    (* Yices 1.0.28 and Z3 2.13 report `unknown' for the next goal *)
597    (``(!x. ?y. P x y) ==> (?y. !x. P x y)``, []),
598    (* Z3 2.13 reports `unknown' for the next goal *)
599    (``(?x. P x) ==> !x. P x``, [sat_YO]),
600    (* Z3 2.13 reports `unknown' for the next goal *)
601    (``?x. P x ==> !x. P x``, [thm_AUTO, thm_YO]),
602
603    (* let binders *)
604
605    (``let x = y in let x = (x /\ z) in x <=> y /\ z``,
606      [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
607    (``let x = u in let x = x in let y = v in x /\ y <=> u /\ v``,
608      [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
609
610    (* lambda abstractions *)
611
612    (``(\x. x) = (\y. y)``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
613    (``(\x. \x. x) x x = (\y. \y. y) y x``,
614      [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
615    (``(\x. x (\x. x)) = (\y. y (\x. x))``,
616      [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
617    (* Yices 1.0.29 fails to decide this one *)
618    (``(\x. x (\x. x)) = (\y. y x)``, [(*sat_YO,*) sat_Z3, sat_Z3p]),
619    (``f x = (\x. f x) x``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
620    (``f x = (\y. f y) x``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
621
622    (* higher-order logic *)
623
624    (* Z3 2.19 unexpectedly replaces certain implications by conjunctions in
625       its proof *)
626
627    (``(P (f x) ==> Q f) ==> P (f x) ==> Q f``,
628      [thm_AUTO, thm_YO, thm_Z3(*, thm_Z3p*)]),
629    (``(Q f ==> P (f x)) ==> Q f ==> P (f x)``,
630      [thm_AUTO, thm_YO, thm_Z3(*, thm_Z3p*)]),
631
632    (* tuples, FST, SND *)
633
634    (``(x, y) = (x, z)``, [sat_YO, sat_Z3, sat_Z3p]),
635    (``(x, y) = (z, y)``, [sat_YO, sat_Z3, sat_Z3p]),
636    (``(x, y) = (y, x)``, [sat_YO, sat_Z3, sat_Z3p]),
637    (``((x, y) = (y, x)) = (x = y)``, [(*thm_AUTO,*) thm_YO]),
638    (``((x, y, z) = (y, z, x)) <=> (x = y) /\ (y = z)``,
639      [(*thm_AUTO,*) thm_YO]),
640    (``((x, y) = (u, v)) <=> (x = u) /\ (y = v)``, [thm_AUTO, thm_YO]),
641
642    (``y = FST (x, y)``, [sat_YO, sat_Z3, sat_Z3p]),
643    (``x = FST (x, y)``, [thm_AUTO, thm_YO]),
644    (``(FST (x, y, z) = FST (u, v, w)) = (x = u)``, [thm_AUTO, thm_YO]),
645    (``(FST (x, y, z) = FST (u, v, w)) <=> (x = u) /\ (y = w)``,
646      [sat_YO, sat_Z3, sat_Z3p]),
647
648    (``y = SND (x, y)``, [thm_AUTO, thm_YO]),
649    (``x = SND (x, y)``, [sat_YO, sat_Z3, sat_Z3p]),
650    (``(SND (x, y, z) = SND (u, v, w)) = (y = v)``,
651       [sat_YO, sat_Z3, sat_Z3p]),
652    (``(SND (x, y, z) = SND (u, v, w)) = (z = w)``,
653       [sat_YO, sat_Z3, sat_Z3p]),
654    (``(SND (x, y, z) = SND (u, v, w)) <=> (y = v) /\ (z = w)``,
655      [thm_AUTO, thm_YO]),
656
657    (``(FST (x, y) = SND (x, y)) = (x = y)``, [thm_AUTO, thm_YO]),
658    (``(FST p = SND p) = (p = (SND p, FST p))``, [(*thm_AUTO,*) thm_YO]),
659    (``((\p. FST p) (x, y)= (\p. SND p) (x, y)) = (x = y)``,
660      [thm_AUTO, thm_YO]),
661
662    (* words (i.e., bit vectors) *)
663
664    (``x:word2 = x``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
665    (``x:word3 = x``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
666    (``x:word4 = x``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
667    (``x:word5 = x``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
668    (``x:word6 = x``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
669    (``x:word7 = x``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
670    (``x:word8 = x``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
671    (``x:word12 = x``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
672    (``x:word16 = x``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
673    (``x:word20 = x``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
674    (``x:word24 = x``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
675    (``x:word28 = x``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
676    (``x:word30 = x``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
677    (``x:word32 = x``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
678    (``x:word64 = x``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
679
680    (``x:word32 && x = x``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
681    (``x:word32 && y = y && x``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
682    (``(x:word32 && y) && z = x && (y && z)``,
683      [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
684    (``x:word32 && 0w = 0w``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
685    (``x:word32 && 0w = x``, [sat_YO, sat_Z3, sat_Z3p]),
686
687    (``x:word32 || x = x``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
688    (``x:word32 || y = y || x``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
689    (``(x:word32 || y) || z = x || (y || z)``,
690      [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
691    (``x:word32 || 0w = 0w``, [sat_YO, sat_Z3, sat_Z3p]),
692    (``x:word32 || 0w = x``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
693
694    (``x:word32 ?? x = 0w``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
695    (``x:word32 ?? y = y ?? x``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
696    (``(x:word32 ?? y) ?? z = x ?? (y ?? z)``,
697      [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
698    (``x:word32 ?? 0w = 0w``, [sat_YO, sat_Z3, sat_Z3p]),
699    (``x:word32 ?? 0w = x``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
700
701    (``~ ~ x:word32 = x``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
702    (``~ 0w = 0w:word32``, [sat_YO, sat_Z3, sat_Z3p]),
703
704    (* Yices does not support bit-vector division *)
705    (* Z3 2.19 prints "extract" wrongly in its proofs *)
706
707    (``x:word32 / 4w = x / 2w / 2w``, [(*thm_AUTO, thm_YO,*) thm_Z3(*, thm_Z3p*)]),
708    (``x:word32 / 6w = x / 2w / 3w``, [(*thm_AUTO, thm_YO,*) thm_Z3(*, thm_Z3p*)]),
709    (``x:word32 / x = 1w``, [sat_YO, sat_Z3, sat_Z3p]),
710    (``x:word32 <> 0w ==> (x / x = 1w)``, [(*thm_AUTO, thm_YO,*) thm_Z3(*, thm_Z3p*)]),
711    (``y:word8 <> 0w ==> (x / y = -x / -y)``, [sat_YO, sat_Z3, sat_Z3p]),
712    (``y:word8 <> 0w ==> (x / y = -(-x / y))``, [sat_YO, sat_Z3, sat_Z3p]),
713    (``y:word8 <> 0w ==> (x / y = -(x / -y))``, [sat_YO, sat_Z3, sat_Z3p]),
714    (``x:word8 <> 0x80w /\ y <> 0w ==> (x / y = -x / -y)``,
715      [(*thm_AUTO, thm_YO,*) thm_Z3(*, thm_Z3p*)]),
716    (``x:word8 <> 0x80w /\ y <> 0w ==> (x / y = -(-x / y))``,
717      [(*thm_AUTO, thm_YO,*) thm_Z3(*, thm_Z3p*)]),
718    (``x:word8 <> 0x80w /\ y <> 0w ==> (x / y = -(x / -y))``,
719      [(*thm_AUTO, thm_YO,*) thm_Z3(*, thm_Z3p*)]),
720
721    (``x:word32 // 4w = x // 2w // 2w``, [thm_AUTO, (*thm_YO,*) thm_Z3(*, thm_Z3p*)]),
722    (``x:word32 // 6w = x // 2w // 3w``, [(*thm_AUTO, thm_YO,*) thm_Z3(*, thm_Z3p*)]),
723    (``x:word32 // x = 1w``, [sat_YO, sat_Z3, sat_Z3p]),
724    (``x:word32 <> 0w ==> (x // x = 1w)``, [(*thm_AUTO, thm_YO,*) thm_Z3(*, thm_Z3p*)]),
725
726    (``y:word8 <> 0w ==> (x = x // y * y + word_mod x y)``,
727      [(*thm_AUTO, thm_YO,*) thm_Z3(*, thm_Z3p*)]),
728    (``y:word8 <> 0w ==> word_mod x y <+ y``,
729      [(*thm_AUTO, thm_YO,*) thm_Z3(*, thm_Z3p*)]),
730
731    (``y:word8 <> 0w ==> (x = x / y * y + word_rem x y)``,
732      [(*thm_AUTO, thm_YO,*) thm_Z3(*, thm_Z3p*)]),
733
734    (* Z3 2.19 does not handle "bvsrem ... bv0" correctly *)
735
736    (``x:word8 < 0w /\ y < 0w  ==> (word_rem x y = -word_mod (-x) (-y))``,
737      [(*thm_AUTO, thm_YO,*)thm_Z3(*, thm_Z3p*)]),
738    (``x:word8 < 0w /\ y >= 0w ==> (word_rem x y = -word_mod (-x) y)``,
739      [(*thm_AUTO, thm_YO, thm_Z3, thm_Z3p*)]),
740    (``x:word8 >= 0w /\ y < 0w ==> (word_rem x y = word_mod x (-y))``,
741      [(*thm_AUTO, thm_YO,*)thm_Z3(*, thm_Z3p*)]),
742    (``x:word8 >= 0w /\ y >= 0w ==> (word_rem x y = word_mod x y)``,
743      [(*thm_AUTO, thm_YO, thm_Z3, thm_Z3p*)]),
744
745    (``x:word8 < 0w /\ y < 0w  ==> (word_smod x y = -word_mod (-x) (-y))``,
746      [(*thm_AUTO, thm_YO,*)thm_Z3(*, thm_Z3p*)]),
747    (``x:word8 < 0w /\ y >= 0w ==> (word_smod x y = -word_mod (-x) y + y)``,
748      [(*thm_AUTO, thm_YO, thm_Z3, thm_Z3p*)]),
749(* this is false: consider x = 99, y = 255
750    (``x:word8 >= 0w /\ y < 0w ==> (word_smod x y = word_mod x (-y) + y)``,
751      [(*thm_AUTO, thm_YO,*)thm_Z3(*, thm_Z3p*)]),
752*)
753    (``x:word8 >= 0w /\ y >= 0w ==> (word_smod x y = word_mod x y)``,
754      [(*thm_AUTO, thm_YO, thm_Z3, thm_Z3p*)]),
755
756    (``x:word32 << 0 = x``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
757    (``x:word32 << 31 = 0w``, [sat_YO, sat_Z3, sat_Z3p]),
758    (``(x:word32 << 31 = 0w) \/ (x << 31 = 1w << 31)``,
759      [thm_AUTO, thm_YO, thm_Z3(*, thm_Z3p*)]),
760
761    (* Yices does not support shifting by more than the word length *)
762
763    (``x:word32 << 99 = 0w``, [thm_AUTO, (*thm_YO,*) thm_Z3, thm_Z3p]),
764
765    (* Yices does not support shifting by a non-constant *)
766
767    (``x:word32 << n = x``, [(*sat_YO,*) sat_Z3, sat_Z3p]),
768
769    (``x:word32 <<~ 0w = x``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
770    (``x:word32 <<~ 31w = 0w``, [sat_YO, sat_Z3, sat_Z3p]),
771    (``(x:word32 <<~ 31w = 0w) \/ (x <<~ 31w = 1w <<~ 31w)``,
772      [thm_AUTO, thm_YO, thm_Z3(*, thm_Z3p*)]),
773    (``(x:word32 <<~ x) && 1w = 0w``,
774      [thm_AUTO, thm_YO, thm_Z3(*, thm_Z3p*)]),
775    (``x:word32 <<~ y = y <<~ x``, [sat_YO, sat_Z3, sat_Z3p]),
776    (``(x:word32 <<~ y) <<~ z = x <<~ (y <<~ z)``, [sat_YO, sat_Z3, sat_Z3p]),
777
778    (``x:word32 >>> 0 = x``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
779    (``x:word32 >>> 31 = 0w``, [sat_YO, sat_Z3, sat_Z3p]),
780    (``(x:word32 >>> 31 = 0w) \/ (x >>> 31 = 1w)``,
781      [thm_AUTO, thm_YO, thm_Z3(*, thm_Z3p*)]),
782
783    (* Yices does not support right-shift by a (non-constant) bit-vector
784       amount *)
785
786    (``x:word32 >>>~ 0w = x``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
787    (``x:word32 >>>~ 31w = 0w``, [sat_YO, sat_Z3, sat_Z3p]),
788    (``(x:word32 >>>~ 31w = 0w) \/ (x >>>~ 31w = 1w)``,
789      [thm_AUTO, thm_YO, thm_Z3(*, thm_Z3p*)]),
790    (``(x:word32 >>>~ x) = 0w``, [thm_AUTO, (*thm_YO,*) thm_Z3(*, thm_Z3p*)]),
791    (``x:word32 >>>~ y = y >>>~ x``, [(*sat_YO,*) sat_Z3, sat_Z3p]),
792    (``(x:word32 >>>~ y) >>>~ z = x >>>~ (y >>>~ z)``,
793      [(*sat_YO,*) sat_Z3, sat_Z3p]),
794
795    (* Yices does not support arithmetical shift-right *)
796
797    (``x:word32 >> 0 = x``, [thm_AUTO, (*thm_YO,*) thm_Z3, thm_Z3p]),
798    (``x:word32 >> 31 = 0w``, [sat_YO, sat_Z3, sat_Z3p]),
799    (``(x:word32 >> 31 = 0w) \/ (x >> 31 = 0xFFFFFFFFw)``,
800      [thm_AUTO, (*thm_YO,*) thm_Z3(*, thm_Z3p*)]),
801
802    (``x:word32 >>~ 0w = x``, [thm_AUTO, (*thm_YO,*) thm_Z3, thm_Z3p]),
803    (``x:word32 >>~ 31w = 0w``, [sat_YO, sat_Z3, sat_Z3p]),
804    (``(x:word32 >>~ 31w = 0w) \/ (x >>~ 31w = 0xFFFFFFFFw)``,
805      [thm_AUTO, (*thm_YO,*) thm_Z3(*, thm_Z3p*)]),
806    (``(x:word32 >>~ x = 0w)  \/ (x >>~ x = 0xFFFFFFFFw)``,
807      [thm_AUTO, (*thm_YO,*) thm_Z3(*, thm_Z3p*)]),
808    (``x:word32 >>~ y = y >>~ x``, [sat_YO, sat_Z3, sat_Z3p]),
809    (``(x:word32 >>~ y) >>~ z = x >>~ (y >>~ z)``, [sat_YO, sat_Z3, sat_Z3p]),
810
811    (* Yices does not support bit-vector rotation *)
812
813    (``x:word32 #<< 0 = x``, [thm_AUTO, (*thm_YO,*) thm_Z3(*, thm_Z3p*)]),
814    (``x:word32 #<< 32 = x``, [thm_AUTO, (*thm_YO,*) thm_Z3(*, thm_Z3p*)]),
815    (``x:word32 #<< 64 = x``, [thm_AUTO, (*thm_YO,*) thm_Z3(*, thm_Z3p*)]),
816    (``x:word32 #<< 1 <> x``, [sat_YO, sat_Z3, sat_Z3p]),
817
818    (``x:word32 #<<~ 0w = x``, [thm_AUTO, (*thm_YO,*) thm_Z3(*, thm_Z3p*)]),
819    (``x:word32 #<<~ 32w = x``, [thm_AUTO, (*thm_YO,*) thm_Z3(*, thm_Z3p*)]),
820    (``x:word32 #<<~ 64w = x``, [thm_AUTO, (*thm_YO,*) thm_Z3(*, thm_Z3p*)]),
821    (``x:word32 #<<~ 1w = x``, [sat_YO, sat_Z3, sat_Z3p]),
822
823    (``x:word32 #>> 0 = x``, [thm_AUTO, (*thm_YO,*) thm_Z3(*, thm_Z3p*)]),
824    (``x:word32 #>> 32 = x``, [thm_AUTO, (*thm_YO,*) thm_Z3(*, thm_Z3p*)]),
825    (``x:word32 #>> 64 = x``, [thm_AUTO, (*thm_YO,*) thm_Z3(*, thm_Z3p*)]),
826    (``x:word32 #>> 1 <> x``, [sat_YO, sat_Z3, sat_Z3p]),
827
828    (``x:word32 #>>~ 0w = x``, [thm_AUTO, (*thm_YO,*) thm_Z3(*, thm_Z3p*)]),
829    (``x:word32 #>>~ 32w = x``, [thm_AUTO, (*thm_YO,*) thm_Z3(*, thm_Z3p*)]),
830    (``x:word32 #>>~ 64w = x``, [thm_AUTO, (*thm_YO,*) thm_Z3(*, thm_Z3p*)]),
831    (``x:word32 #>>~ 1w = x``, [sat_YO, sat_Z3, sat_Z3p]),
832
833    (``1w:word2 @@ 1w:word2 = 5w:word4``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
834    (``((x @@ y):word32 = y @@ x) = (x:word16 = y)``,
835      [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
836
837    (``(31 >< 0) x:word32 = x``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
838    (``(1 >< 0) (0w:word32) = 0w:word2``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
839    (``(32 >< 0) (x:word32) :bool[33] = w2w x``,
840      [thm_AUTO, thm_YO(*, thm_Z3, thm_Z3p*)]),
841    (``(0 >< 1) (x:word32) = 0w:word32``,
842      [thm_AUTO, thm_YO(*, thm_Z3, thm_Z3p*)]),
843
844    (``(x:word2 = y) <=> (x ' 0 = y ' 0) /\ (x ' 1 = y ' 1)``,
845      [thm_AUTO, thm_YO, thm_Z3(*, thm_Z3p*)]),
846
847    (``0w:word32 = w2w (0w:word16)``, [thm_AUTO, thm_YO, thm_Z3(*, thm_Z3p*)]),
848    (``0w:word32 = w2w (0w:word32)``, [thm_AUTO, thm_YO, thm_Z3(*, thm_Z3p*)]),
849    (``0w:word32 = w2w (0w:word64)``, [thm_AUTO, thm_YO(*, thm_Z3, thm_Z3p*)]),
850    (``x:word32 = w2w x``, [thm_AUTO, thm_YO, thm_Z3(*, thm_Z3p*)]),
851
852    (``0w:word32 = sw2sw (0w:word16)``, [thm_AUTO, thm_YO, thm_Z3(*, thm_Z3p*)]),
853    (``0w:word32 = sw2sw (0w:word32)``, [thm_AUTO, thm_YO, thm_Z3(*, thm_Z3p*)]),
854    (``0w:word32 = sw2sw (0w:word64)``, [thm_AUTO, thm_YO(*, thm_Z3, thm_Z3p*)]),
855    (``x:word32 = sw2sw x``, [thm_AUTO, thm_YO, thm_Z3(*, thm_Z3p*)]),
856
857    (``(x:word32) + x = x``, [sat_YO, sat_Z3, sat_Z3p]),
858    (``(x:word32) + y = y + x``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
859    (``((x:word32) + y) + z = x + (y + z)``,
860      [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
861    (``(x:word32) + 0w = 0w``, [sat_YO, sat_Z3, sat_Z3p]),
862    (``(x:word32) + 0w = x``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
863
864    (``(x:word32) - x = x``, [sat_YO, sat_Z3, sat_Z3p]),
865    (``(x:word32) - x = 0w``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
866    (``(x:word32) - y = y - x``, [sat_YO, sat_Z3, sat_Z3p]),
867    (``((x:word32) - y) - z = x - (y - z)``,
868      [sat_YO, sat_Z3, sat_Z3p]),
869    (``(x:word32) - 0w = 0w``, [sat_YO, sat_Z3, sat_Z3p]),
870    (``(x:word32) - 0w = x``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
871
872    (``(x:word32) * x = x``, [sat_YO, sat_Z3, sat_Z3p]),
873    (``(x:word32) * y = y * x``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
874    (``((x:word32) * y) * z = x * (y * z)``,
875      [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
876    (``(x:word32) * 0w = 0w``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
877    (``(x:word32) * 0w = x``, [sat_YO, sat_Z3, sat_Z3p]),
878    (``(x:word32) * 1w = x``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
879
880    (``- (x:word32) = x``, [sat_YO, sat_Z3, sat_Z3p]),
881    (``- 0w = 0w:word32``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
882    (``- - (x:word32) = x``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
883
884    (``0w < 1w:word32``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
885    (``~ 0w < 0w:word32``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
886
887    (``0w <= 1w:word32``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
888    (``x <= y:word32 <=> x < y \/ (x = y)``, [thm_AUTO, thm_YO, thm_Z3(*, thm_Z3p*)]),
889    (``~ 0w <= 0w:word32``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
890
891    (``1w > 0w:word32``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
892    (``0w > ~ 0w:word32``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
893
894    (``1w >= 0w:word32``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
895    (``x >= y:word32 <=> x > y \/ (x = y)``, [thm_AUTO, thm_YO, thm_Z3(*, thm_Z3p*)]),
896    (``0w >= ~ 0w:word32``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
897
898    (``0w <+ 1w:word32``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
899    (``0w <+ ~ 0w:word32``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
900
901    (``0w <=+ 1w:word32``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
902    (``x <=+ y:word32 <=> x <+ y \/ (x = y)``,
903      [thm_AUTO, thm_YO, thm_Z3(*, thm_Z3p*)]),
904    (``0w <=+ ~ 0w:word32``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
905
906    (``1w >+ 0w:word32``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
907    (``~ 0w >+ 0w:word32``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
908
909    (``1w >=+ 0w:word32``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
910    (``x >=+ y:word32 <=> x >+ y \/ (x = y)``,
911      [thm_AUTO, thm_YO, thm_Z3(*, thm_Z3p*)]),
912    (``~ 0w >=+ 0w:word32``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
913
914    (* from Magnus Myreen *)
915    (``!(a:word32) b.
916     (((word_msb (a - b) <=>
917        (word_msb a <=/=> word_msb b) /\
918        (word_msb a <=/=> word_msb (a - b))) <=> b <= a) /\
919      ((word_msb (a - b) <=>
920        (word_msb b <=/=> word_msb a) /\
921        (word_msb a <=/=> word_msb (a - b))) <=> b <= a) /\
922      ((word_msb (a - b) <=>
923        (word_msb a <=/=> word_msb b) /\
924        (word_msb (a - b) <=/=> word_msb a)) <=> b <= a) /\
925      ((word_msb (a - b) <=>
926        (word_msb b <=/=> word_msb a) /\
927        (word_msb (a - b) <=/=> word_msb a)) <=> b <= a) /\
928      ((word_msb (a - b) <=>
929        (word_msb a <=/=> word_msb (a - b)) /\
930        (word_msb a <=/=> word_msb b)) <=> b <= a) /\
931      ((word_msb (a - b) <=>
932        (word_msb a <=/=> word_msb (a - b)) /\
933        (word_msb b <=/=> word_msb a)) <=> b <= a) /\
934      ((word_msb (a - b) <=>
935        (word_msb (a - b) <=/=> word_msb a) /\
936        (word_msb a <=/=> word_msb b)) <=> b <= a) /\
937      ((word_msb (a - b) <=>
938        (word_msb (a - b) <=/=> word_msb a) /\
939        (word_msb b <=/=> word_msb a)) <=> b <= a) /\
940      (((word_msb a <=/=> word_msb b) /\
941        (word_msb a <=/=> word_msb (a - b)) <=> word_msb (a - b)) <=>
942       b <= a) /\
943      (((word_msb b <=/=> word_msb a) /\
944        (word_msb a <=/=> word_msb (a - b)) <=> word_msb (a - b)) <=>
945       b <= a) /\
946      (((word_msb a <=/=> word_msb b) /\
947        (word_msb (a - b) <=/=> word_msb a) <=> word_msb (a - b)) <=>
948       b <= a) /\
949      (((word_msb b <=/=> word_msb a) /\
950        (word_msb (a - b) <=/=> word_msb a) <=> word_msb (a - b)) <=>
951       b <= a) /\
952      (((word_msb a <=/=> word_msb (a - b)) /\
953        (word_msb a <=/=> word_msb b) <=> word_msb (a - b)) <=>
954       b <= a) /\
955      (((word_msb a <=/=> word_msb (a - b)) /\
956        (word_msb b <=/=> word_msb a) <=> word_msb (a - b)) <=>
957       b <= a) /\
958      (((word_msb (a - b) <=/=> word_msb a) /\
959        (word_msb a <=/=> word_msb b) <=> word_msb (a - b)) <=>
960       b <= a) /\
961      (((word_msb (a - b) <=/=> word_msb a) /\
962        (word_msb b <=/=> word_msb a) <=> word_msb (a - b)) <=>
963       b <= a)) /\ (a >= b <=> b <= a) /\ (a > b <=> b < a) /\
964     (~(a <=+ b) <=> b <+ a) /\ (~(a <+ b) <=> b <=+ a) /\
965     (a <+ b \/ (a = b) <=> a <=+ b) /\ (~(a < b) <=> b <= a) /\
966     (~(a <= b) <=> b < a) /\ (a < b \/ (a = b) <=> a <= b) /\
967     ((a = b) \/ a < b <=> a <= b) /\ (a <+ b \/ (a = b) <=> a <=+ b) /\
968     ((a = b) \/ a <+ b <=> a <=+ b) /\
969     (b <=+ a /\ a <> b <=> b <+ a) /\ (a <> b /\ b <=+ a <=> b <+ a) /\
970     (b <= a /\ a <> b <=> b < a) /\ (a <> b /\ b <= a <=> b < a) /\
971     (((v:word32) - w = 0w) <=> (v = w)) /\ (w - 0w = w)``,
972      [(*thm_AUTO,*) thm_YO(*, thm_Z3, thm_Z3p*)]),
973
974    (* from Yogesh Mahajan *)
975    (``!(w: 18 word). (sw2sw w): 32 word = w2w ((16 >< 0) w: 17 word) +
976     0xfffe0000w + ((0 >< 0) (~(17 >< 17) w: bool[unit]) << 17): 32 word``,
977      [thm_AUTO, thm_YO(*, thm_Z3, thm_Z3p*)]),
978
979    (* The Yices translation currently rejects polymorphic-width bit
980       vectors; the SMT-LIB translation treats their type -- and
981       operations on them -- as uninterpreted. *)
982
983    (``x <=+ x``, [thm_AUTO(*, thm_YO, thm_Z3, thm_Z3p*)]),
984
985    (* data types: constructors *)
986
987    (``foo <> bar``, [thm_AUTO, thm_YO]),
988    (``foo <> baz``, [thm_AUTO, thm_YO]),
989    (``bar <> baz``, [thm_AUTO, thm_YO]),
990    (``[] <> x::xs``, [thm_AUTO, thm_YO]),
991    (``xs <> x::xs``, [thm_AUTO, thm_YO]),
992    (``(x::xs = y::ys) <=> (x = y) /\ (xs = ys)``, [thm_AUTO, thm_YO]),
993
994    (* data types: case constants *)
995
996    (``dt1_CASE foo f b z = f``, [thm_AUTO, thm_YO]),
997    (``dt1_CASE bar f b z = b``, [thm_AUTO, thm_YO]),
998    (``dt1_CASE baz f b z = z``, [thm_AUTO, thm_YO]),
999    (``dt1_CASE x c c c = c``, [(*thm_AUTO,*) thm_YO]),
1000    (``list_CASE [] n c = n``, [thm_AUTO, thm_YO]),
1001    (``list_CASE (x::xs) n c = c x xs``, [thm_AUTO, thm_YO]),
1002
1003    (* records: field selectors *)
1004
1005    (``(x = y) <=> (x.employed = y.employed) /\ (x.age = y.age)``,
1006      [(*thm_AUTO,*) thm_YO]),
1007
1008    (* records: field updates *)
1009
1010    (``(x with employed := e).employed = e``, [thm_AUTO, thm_YO]),
1011
1012    (``x with <| employed := e; age := a |> =
1013     y with <| employed := e; age := a |>``, [thm_AUTO, thm_YO]),
1014
1015    (* records: literals *)
1016
1017    (``(<| employed := e1; age := a1 |> = <| employed := e2; age := a2 |>)
1018     <=> (e1 = e2) /\ (a1 = a2)``, [thm_AUTO, thm_YO]),
1019
1020    (* sets (as predicates -- every set expression must be applied to an
1021       argument!) *)
1022
1023    (``x IN P <=> P x``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
1024
1025    (``x IN {x | P x} <=> P x``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
1026
1027    (``x NOTIN {}``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
1028    (``x IN UNIV``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
1029
1030    (``x IN P UNION Q <=> P x \/ Q x``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
1031    (``x IN P UNION {} <=> x IN P``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
1032    (``x IN P UNION UNIV``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
1033    (``x IN P UNION Q <=> x IN Q UNION P``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
1034    (``x IN P UNION (Q UNION R) <=> x IN (P UNION Q) UNION R``,
1035      [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
1036
1037    (``x IN P INTER Q <=> P x /\ Q x``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
1038    (``x NOTIN P INTER {}``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
1039    (``x IN P INTER UNIV <=> x IN P``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
1040    (``x IN P INTER Q <=> x IN Q INTER P``, [thm_AUTO, thm_YO, thm_Z3, thm_Z3p]),
1041    (``x IN P INTER (Q INTER R) <=> x IN (P INTER Q) INTER R``,
1042      [thm_AUTO, thm_YO, thm_Z3, thm_Z3p])
1043
1044  ]  (* tests *)
1045end
1046
1047(*****************************************************************************)
1048(* actually perform tests                                                    *)
1049(*****************************************************************************)
1050
1051val _ = map (fn (term, test_funs) =>
1052               map (fn test_fun => test_fun term) test_funs) tests
1053
1054(*****************************************************************************)
1055
1056val _ = print " done, all tests successful.\n"
1057
1058val _ = OS.Process.exit OS.Process.success
1059