1open HolKernel Parse boolLib
2open testutils TotalDefn
3val _ = Feedback.emit_MESG := false
4val _ = tprint "Testing mutually recursive function definition"
5
6val f_def = require (check_result (K true)) Define`
7  (f x = if x = 0 then T else ~g(x - 1)) /\
8  (g x = if x = 0 then F else ~f(x - 1))
9`
10
11val _ = tprint "Testing definition over literals"
12
13val h_def = Define`
14  (h 0 = T) /\ (h 1 = F)
15`;
16
17val _ = let
18  val cs = strip_conj (concl h_def)
19  val _ = if length cs = 2 then () else die "FAILED!"
20  val _ = if List.all (is_const o rhs) cs then () else die "FAILED!"
21in
22  OK()
23end
24
25val _ = tprint "Testing form of derived induction principle"
26val fact_def = Define`fact n = if n < 2 then 1 else n * fact(n - 1)`;
27
28val desired_ind =
29  ``!P. (!n. (~(n < 2) ==> P (n - 1)) ==> P n) ==> !v. P v``
30
31val _ = if aconv desired_ind (concl (theorem "fact_ind")) then OK()
32        else die "FAILED!\n"
33
34val _ = tprint "Define schema(1)"
35val _ = require (check_result (K true)) (quietly DefineSchema)
36                `(fs 0 y = z + y) /\ (fs x y = x)`;
37val _ = tprint "Define schema(2)"
38val _ = require (check_result (K true)) (quietly DefineSchema)
39                `(gs 0 y = x + y) /\ (gs x y = x)`;
40
41val _ = tprint "Testing 0-arg recursive function with lambda"
42
43val f1_def = require (check_result (K true)) (quietly Define)`
44  f1 = \x. case x of 0 => 0n | SUC n => f1 n
45`
46
47val _ = tprint "Testing 1-arg recursive function with lambda"
48
49val f1_def = require (check_result (K true)) (quietly Define)`
50  f2 (y : 'a) = \x. case x of 0 => 0n | SUC n => f2 y n
51`;
52
53val _ = tprint "Testing 2-arg recursive function with lambda"
54
55val f1_def = require (check_result (K true)) (quietly Define)`
56  f3 (y : 'a) (z : 'a) = \x. case x of 0 => 0n | SUC n => f3 y z n
57`;
58