1structure test_cases :> test_cases = 2struct 3 4open Abbrev 5open HolKernel Parse; 6 7fun test_term c (n,t,b) = let 8 val _ = print (StringCvt.padRight #" " 25 n) 9 val _ = Profile.reset_all() 10 val timer = Timer.startCPUTimer () 11 val result = SOME (SOME (c t)) 12 handle Interrupt => SOME NONE 13 | _ => NONE 14 val {usr,sys} = Timer.checkCPUTimer timer 15 val gc = Timer.checkGCTime timer 16 val (verdictmsg, verdict) = 17 case result of 18 SOME (SOME th) => let 19 in 20 case Lib.total boolSyntax.rhs (concl th) of 21 SOME r => 22 if b andalso r = boolSyntax.T orelse 23 not b andalso r = boolSyntax.F 24 then 25 ("OK", true) 26 else ("Bad EQN", false) 27 | NONE => ("Not an EQN", false) 28 end 29 | SOME NONE => ("Interrupted", false) 30 | NONE => ("Raised exception", false) 31 val _ = print (StringCvt.padRight #" " 17 verdictmsg) 32 val pl = StringCvt.padLeft #" " 6 33 val _ = print (pl (Time.toString usr)^" "^pl (Time.toString sys)^" "^ 34 pl (Time.toString gc)) 35 val _ = print "\n" 36in 37 verdict 38end 39 40fun A s = ("at."^s, concl (DB.fetch "arithmetic" s), true) 41fun I s = ("it."^s, concl (DB.fetch "integer" s), true) 42fun L (t,s) = (s,t,true) 43fun T (s,t) = (s,t,true) 44 45val terms_to_test = 46 [T ("INT_GROUP", Term`?!x:int. (!y. x + y = y) /\ (!y. ?!z. y + z = x)`), 47 T ("Mike1", 48 ``?(k:num) (j:num) (i:num). 49 (i >= 0 /\ j >= 0 /\ k >= 0 /\ ~((i = 0) \/ (j = 0) \/ (k = 0)) /\ 50 ~(i = j) /\ ~(i = k) /\ (j = k)) /\ i < j + k``), 51 T ("Mike2", 52 ``?(k:num) (j:num) (i:num). 53 (((((i >= 0 /\ j >= 0 /\ k >= 0) /\ 54 ~(((i = 0) \/ (j = 0)) \/ (k = 0))) /\ ~(i = j)) /\ ~(i = k)) /\ 55 (j = k)) /\ i < j + k``), 56 T ("NAT MAX 1", ``x:num <= MAX x y``), 57 T ("NAT MAX 2", ``!y:num. 0 < y ==> ?x:num. x < MAX x y``), 58 T ("INT MAX 1", ``x <= int_max x y``), 59 T ("INT MAX 2", ``!y. ?x:int. x < int_max x y``), 60 T ("BUG1", 61 ``(?x. y <= x /\ x <= z /\ 2i * z + 1 <= x /\ x <= 2 * y) = 62 y <= z /\ 2 * z + 1 <= 2 * y /\ y <= 2 * y /\ 2 * z + 1 <= z``), 63 T ("ILP1", Term`?z y x. 2n * x + 3 * y < 4 * z ==> 5 * x < 3 * y + z`), 64 T ("ILP2", 65 Term`?z y x v u. ~9 * u + ~12 * v + 4 * x + 5 * y + ~10 * z = 17`), 66 ("aILP1", 67 Term`!z y x v u. 68 (3 * u + 6 * v + ~9 * x + ~5 * y + 6 * z = 86) ==> 69 (1 * u + 4 * v + 17 * x + ~18 * y + ~5 * z = ~24)`, false), 70 ("PUGH1", Term`?x y:int. 27 <= 11 * x + 13 * y /\ 11 * x + 13 * y <= 45 /\ 71 ~10 <= 7 * x - 9 * y /\ 7 * x - 9 * y <= 4`, 72 false), 73 T ("3-5", Term`!n:num. 7 < n ==> ?i j. 3 * i + 5 * j = n`), 74 T ("SUNRISE1", Term`!x0:num x:num y0:num y:num. 75 (x0 = x) /\ (y0 = y) ==> 76 (if 100 < y then 77 (if 100 < y0 then y - 10 = y0 - 10 else y - 10 = 91) 78 else 79 101 - (y + 11) < 101 - y0 /\ 80 !x. 81 (if 100 < y + 11 then x = y + 11 - 10 else x = 91) ==> 82 101 - x < 101 - y0 /\ 83 !x1. 84 (if 100 < x then x1 = x - 10 else x1 = 91) ==> 85 (if 100 < y0 then x1 = y0 - 10 else x1 = 91))`), 86 ("DIV1", Term`!x. 0 <= x = x / 2 <= x`, false), 87 ("DIV2", Term`!x. (x / 2 = x) = (x = 0)`, false), 88 T ("DIV3", Term`!i. (i % 10) % 10 = i % 10`), 89 T ("DIV4", Term`?!i. 2 < i /\ (i / 2 = 1)`), 90 T ("NDIV1", Term`!x. 0 < x ==> x DIV 2 < x`), 91 T ("NDIV2", Term`(x MOD 2) MOD 2 = x MOD 2`), 92 T ("NDIV3", Term`?!n. 2 < n /\ (n DIV 2 = 1)`), 93 T ("KXSDIV1", Term`!n. ~(n = 0) /\ EVEN n ==> (n - 2) DIV 2 < n`), 94 T ("KXSDIV2", Term`!n. ~(n = 0) /\ ~EVEN n ==> (n - 1) DIV 2 < n`), 95 T ("ECODD1", ``!n. ODD n ==> ~ODD (n - 1)``), 96 T ("simp_divides1", ``!x. 0 < x /\ 2 int_divides x ==> 1 < x``), 97 T ("simp_divides2", ``!x. 0 <= x /\ ~(2 int_divides x) ==> 1 <= x``), 98 T ("sub_zero_coeff", Term`!x y:int. 0 < x ==> y - x < y`), 99 T ("10000.9391", 100 Term`~(v < 101 SUC 102 (SUC z + (SUC (SUC (SUC (SUC v)) + (v + (SUC u + v))) + u + y) + 103 v)) ==> 104 SUC 0 < 0 + (v + x) + SUC (v + v) /\ 105 (z + z >= 0 + v \/ (z + v = 0) /\ u <= u)`), 106 T ("10000.2223", 107 Term`SUC 0 < (u :num) + 108 (0 + 109 SUC 110 (SUC 111 ((z :num) + 112 (SUC (0 + u) + SUC (v :num) + SUC u + u + 113 (0 + SUC (SUC z + (x :num)) + 0) + 0))) + 114 SUC (z + u)) + x + ((y :num) + z + u) + 0`), 115 T ("EX1_NOT_COMM", ``~((?!x y. (x = y) \/ (x = SUC y)) = 116 (?!y x. (x = y) \/ (x = SUC y)))``), 117 T ("NUM1", Term`!n:num m. n + m > 10 ==> n + 2 * m > 10`), 118 T ("ABS1", Term `!p. 0 <= ABS(p)`), 119 T ("ABS2", Term `!p. ABS (ABS(p)) = ABS(p)`), 120 T ("ABS3", Term `!p. (ABS(p) = 0) = (p = 0)`), 121 T ("ABS4", Term `!p. (ABS(p) = p) = 0 <= p`), 122 T ("ABS5", Term `!p. ABS ~p = ABS p`), 123 T ("ABS6", Term `!p. ABS(p) <= 0 = (p = 0)`), 124 T ("ABS7", Term `!p. ~(ABS(p) < 0)`), 125 T ("ABS8", Term `!p q. 126 (ABS(p) < q = p < q /\ ~q < p) /\ 127 (q < ABS(p) = q < p \/ p < ~q) /\ 128 (~1*ABS(p) < q = ~q < p \/ p < q) /\ 129 (q < ~1*ABS(p) = p < ~q /\ q < p)`), 130 T ("ABS9", Term `!p q. 131 (ABS(p) <= q = p <= q /\ ~q <= p) /\ 132 (q <= ABS(p) = q <= p \/ p <= ~q) /\ 133 (~1*ABS(p) <= q = ~q <= p \/ p <= q) /\ 134 (q <= ~1*ABS(p) = p <= ~q /\ q <= p)`), 135 T ("ABS10", Term `!p q. 136 ((ABS(p) = q) = (p = q) /\ 0 < q \/ (p = ~q) /\ 0 <= q) /\ 137 ((q = ABS(p)) = (p = q) /\ 0 < q \/ (p = ~q) /\ 0 <= q)`), 138 A "ADD", 139 A "EVEN", 140 A "EQ_ADD_LCANCEL", 141 I "INT_DOUBLE", 142 I "INT_EQ_NEG", 143 I "INT_ADD_RID_UNIQ", 144 T ("BIGINT1", Term`!x. 100i * x > 213 ==> 100 * x > 251`), 145 T ("BIGINT2", Term`!x. ~213 < 100i * x ==> ~251 < 100 * x`), 146 T ("MIKE.NUM", Term`!q r:num. (7 = r + q * 3) /\ r < 3 ==> (r = 1)`), 147 T ("INT_MULT_NORM", Term`(2 * m = r + k' * (2 * p)) ==> ?s. r = 2i * s`), 148 T ("NUM_MULT_NORM", Term`(2 * m = r + k' * (2 * p)) ==> ?s. r = 2n * s`), 149 A "ZERO_LESS_EQ", A "TWO", A "TIMES2", A "SUC_SUB1", A "SUC_ONE_ADD", 150 A "SUC_NOT", A "SUC_ADD_SYM", A "SUB_SUB", A "SUB_RIGHT_SUB", 151 A "SUB_RIGHT_LESS_EQ", A "SUB_RIGHT_LESS", A "SUB_RIGHT_GREATER_EQ", 152 A "SUB_RIGHT_GREATER", A "SUB_RIGHT_EQ", A "SUB_RIGHT_ADD", A "SUB_PLUS", 153 A "SUB_MONO_EQ", A "SUB_LESS_OR", A "SUB_LESS_EQ_ADD", A "SUB_LESS_EQ", 154 A "SUB_LESS_0", A "SUB_LEFT_SUC", A "SUB_LEFT_SUB", 155 A "SUB_LEFT_LESS_EQ", A "SUB_LEFT_LESS", A "SUB_LEFT_GREATER_EQ", 156 A "SUB_LEFT_GREATER", A "SUB_LEFT_EQ", A "SUB_LEFT_ADD", 157 A "SUB_EQUAL_0", A "SUB_EQ_EQ_0", A "SUB_EQ_0", 158 A "SUB_CANCEL", 159 160 A "SUB_ADD", A "SUB_0", A "SUB", 161 A "PRE_SUC_EQ", A "PRE_SUB1", A "PRE_SUB", 162 A "OR_LESS", A "ONE", A "ODD_OR_EVEN", 163 A "ODD_EXISTS", A "ODD_EVEN", A "ODD_DOUBLE", A "ODD_ADD", A "ODD", 164 A "num_CASES", 165 A "NOT_ZERO_LT_ZERO", A "NOT_SUC_LESS_EQ_0", A "NOT_SUC_LESS_EQ", 166 A "NOT_SUC_ADD_LESS_EQ", A "NOT_ODD_EQ_EVEN", A "NOT_NUM_EQ", 167 A "NOT_LESS_EQUAL", A "NOT_LESS", A "NOT_LEQ", A "NOT_GREATER_EQ", 168 A "NOT_GREATER", A "MULT_RIGHT_1", A "MULT_LEFT_1", A "MULT_0", 169 170 A "LESS_TRANS", 171 A "LESS_SUC_NOT", 172 A "LESS_SUC_EQ_COR", 173 A "LESS_SUB_ADD_LESS", 174 A "LESS_OR_EQ_ADD", 175 A "LESS_OR_EQ", 176 A "LESS_OR", 177 A "LESS_NOT_SUC", 178 A "LESS_MONO_REV", 179 A "LESS_MONO_EQ", 180 A "LESS_MONO_ADD_INV", 181 A "LESS_MONO_ADD_EQ", 182 A "LESS_MONO_ADD", 183 A "LESS_LESS_SUC", 184 A "LESS_LESS_EQ_TRANS", 185 A "LESS_LESS_CASES", 186 A "LESS_IMP_LESS_OR_EQ", 187 A "LESS_IMP_LESS_ADD", 188 A "LESS_EQUAL_ANTISYM", 189 A "LESS_EQUAL_ADD", 190 A "LESS_EQ_TRANS", 191 A "LESS_EQ_SUC_REFL", 192 A "LESS_EQ_SUB_LESS", 193 A "LESS_EQ_REFL", 194 A "LESS_EQ_MONO_ADD_EQ", 195 A "LESS_EQ_MONO", 196 A "LESS_EQ_LESS_TRANS", 197 A "LESS_EQ_LESS_EQ_MONO", 198 A "LESS_EQ_IMP_LESS_SUC", 199 A "LESS_EQ_EXISTS", 200 A "LESS_EQ_CASES", 201 A "LESS_EQ_ANTISYM", 202 A "LESS_EQ_ADD_SUB", 203 A "LESS_EQ_ADD", 204 A "LESS_EQ_0", 205 A "LESS_EQ", 206 A "LESS_CASES_IMP", 207 A "LESS_CASES", 208 A "LESS_ANTISYM", 209 A "LESS_ADD_SUC", 210 A "LESS_ADD_NONZERO", 211 A "LESS_ADD_1", 212 A "LESS_ADD", 213 A "LESS_0_CASES", 214 A "LE", 215 A "INV_PRE_LESS_EQ", 216 A "INV_PRE_LESS", 217 A "INV_PRE_EQ", 218 L (Term`!x:int y z. x < y /\ y < z ==> x < z`, "pt1"), 219 L (Term`?x y:int. 4 * x + 3 * y = 10`, "pt2"), 220 L (Term`!x. 3i * x < 4 * x ==> x > 0`, "pt3"), 221 L (Term`?y. !x:int. x + y = x`, "pt4"), 222 L (Term`?y. (!x:int. x + y = x) /\ 223 !y'. (!x. x + y' = x) ==> (y = y')`, "pt5"), 224 L (Term`!x. 3 int_divides x /\ 2 int_divides x ==> 6 int_divides x`, "pt6"), 225 L (Term`?!y:int. !x. x + y = x`, "pt7"), 226 L (Term`!x. ?!y. x + y = 0i`, "pt8"), 227 L (Term`?x y. (x + y = 6i) /\ (2 * x + 3 * y = 11)`, "pt9"), 228 L (Term`!x z:int. ?!y. x - y = z`, "pt10"), 229 L (Term`!x y z:int. 2 * x < y /\ y < 2 * z ==> 230 ?w. ((y = 2 * w) \/ (y = 2 * w + 1)) /\ 231 x <= w /\ w < z`, "pt11"), 232 L (Term`(0 :num) < SUC (u' :num) ==> (0 :num) < (m :num) ==> 233 (0 :num) < (n :num) ==> ~(m = (0 :num)) ==> 234 n + (u' * m + m) < m ==> u' * m + m <= n ==> F`, "NONPB1"), 235 L (Term`((n :num) = (r :num) + (i :num) * (m :num)) ==> 236 r < m ==> (n MOD m = r) ==> (n DIV m = i) ==> 237 ~(m = (0 :num))`, "NONPB2"), 238 L (Term`(e*bv_c+e*(2*bv_cout+wb_sum)+wbs_sum = 239 bv_cin+e*(bv_c+wb_a+wb_b)+wbs_a+wbs_b) 240 ==> 241 (2n*e*bv_cout+e*wb_sum+wbs_sum = bv_cin+e*wb_a+e*wb_b+wbs_a+wbs_b)`, 242 "AG_NAT"), 243 L (Term`(e*bv_c+e*(2*bv_cout+wb_sum)+wbs_sum = 244 bv_cin+e*(bv_c+wb_a+wb_b)+wbs_a+wbs_b) 245 ==> 246 (2i*e*bv_cout+e*wb_sum+wbs_sum = bv_cin+e*wb_a+e*wb_b+wbs_a+wbs_b)`, 247 "AG_INT"), 248 L (Term`x * y < y * x + 1i`, "IMUL_NORM"), 249 L (Term`x * y < y * x + 1n`, "NMUL_NORM"), 250 L (``Num i < SUC (Num i)``, "Num1"), 251 L (``0 < i ==> (ODD (Num i) = ?j. i = 2 * j + 1)``, "Num2"), 252 L (``0i < & (Num (ABS a1 - 1)) + 1``, "Num3"), 253 L (``0i < &(Num (f (x:'a) - 1)) + 1``, "Num4a"), 254 L (``0i < (if 0 <= f (x:'a) - 1i then f x - 1 else &(g (f x - 1))) + 1``, 255 "Num4b") 256]; 257 258val omega_test_terms = [ 259 L (``(x MOD 1001 + y MOD 1001) MOD 1001 = (x + y) MOD 1001``, "MOD_ADD1001"), 260 L (``((n DIV 100000) MOD 2 = 0) ==> n MOD 200000 < 100000``, "DIV_LT100000"), 261 L (``i < (nb - 1) % 256 /\ 0 <= nb /\ nb < 256 /\ 0 <= i /\ i < 256 ==> 262 i < (i + 1) % 256``, "MATTHEWS_I256"), 263 L (``i < (nb - 1) MOD 256 /\ 0 <= nb /\ nb < 256 /\ 0 <= i /\ i < 256 ==> 264 i < (i + 1) MOD 256``, "MATTHEWS_N256"), 265 L (``i < (nb - 1) % 2147483648 /\ 0 <= nb /\ nb < 2147483648 /\ 0 <= i /\ 266 i < 2147483648 ==> i < (i + 1) % 2147483648``, "MATTHEWS_I2^31"), 267 L (``i < (nb - 1) MOD 2147483648 /\ 0 <= nb /\ nb < 2147483648 /\ 0 <= i /\ 268 i < 2147483648 ==> i < (i + 1) MOD 2147483648``, "MATTHEWS_N2^31"), 269 L (``0 <= i /\ i <= 100 ==> (Num i + 11 = (Num i + 11) MOD 429467296)``, 270 "MATTHEWS_Num"), 271 L (``0 <= i /\ i <= 100 ==> (Num (i + 11) = (Num i + 11) MOD 429467296)``, 272 "MATTHEWS_Num'") 273] 274 275val cooper_test_terms = [ 276(* L (``?s:int e n d m oh r y. 277 0 < s /\ s <= 9 /\ 0 <= e /\ e <= 9 /\ 0 <= n /\ n <= 9 /\ 278 0 <= d /\ d <= 9 /\ 0 < m /\ m <= 9 /\ 0 <= oh /\ oh <= 9 /\ 279 0 <= r /\ r <= 9 /\ 0 <= y /\ y <= 9 /\ ~(s = e) /\ ~(s = n) /\ 280 ~(s = d) /\ ~(s = m) /\ ~(s = oh) /\ ~(s = r) /\ ~(s = y) /\ 281 ~(e = n) /\ ~(e = d) /\ ~(e = m) /\ ~(e = oh) /\ ~(e = r) /\ 282 ~(e = y) /\ ~(n = d) /\ ~(n = m) /\ ~(n = oh) /\ ~(n = r) /\ 283 ~(n = y) /\ ~(d = m) /\ ~(d = oh) /\ ~(d = r) /\ ~(d = y) /\ 284 ~(m = oh) /\ ~(m = r) /\ ~(m = y) /\ ~(oh = r) /\ ~(oh = y) /\ 285 ~(r = y) /\ 286 (1000 * s + 100 * e + 10 * n + d + 1000 * m + 100 * oh + 10 * r + 287 e = 288 10000 * m + 1000 * oh + 100 * n + 10 * e + y)``, 289 "SEND_MORE_MONEY") *) 290] 291 292val goals_to_test = [ 293 ("van Leeuwen", 294 ([``0i <= i``, ``i :int < maxchar``, 295 ``!n. 0i <= n /\ n < i ==> (skips ArrayApp n = 0i)``], 296 ``maxchar - i > 0i``)), 297 ("natural number 1", ([``n:num > 4``], ``n:num > 3``)), 298 ("natural number 2", 299 ([``n:num < p + 1``, ``!m:num. m < p ==> ~(n < m + 1)``], ``p:num = n``)) 300] 301 302fun test_goal tac (name, g) = let 303 val _ = print (StringCvt.padRight #" " 25 name) 304 val result = SOME (SOME (tac g)) handle Interrupt => SOME NONE 305 | _ => NONE 306 val (verdictmsg, verdict) = 307 case result of 308 SOME (SOME (subgoals, _)) => if null subgoals then ("OK", true) 309 else ("Subgoals remain", false) 310 | SOME NONE => ("Interrupted", false) 311 | NONE => ("Raised exception", false) 312 val _ = print (verdictmsg ^ "\n") 313in 314 verdict 315end 316 317 318fun perform_tests conv tactic = 319 (print "Testing terms\n"; 320 List.all (test_term conv) terms_to_test) andalso 321 (print "Testing goals\n"; 322 List.all (test_goal tactic) goals_to_test) 323 324fun perform_omega_tests conv = 325 (print "Testing Omega terms\n"; 326 List.all (test_term conv) omega_test_terms) 327 328fun perform_cooper_tests conv = 329 (print "Testing Cooper terms\n"; 330 List.all (test_term conv) cooper_test_terms) 331 332end; (* struct *) 333