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