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