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