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