# define_type "btree = LEAF A | NODE btree btree";;
val it : thm * thm =
(|- !P. (!a. P (LEAF a)) /\ (!a0 a1. P a0 /\ P a1 ==> P (NODE a0 a1))
==> (!x. P x),
|- !f0 f1.
?fn. (!a. fn (LEAF a) = f0 a) /\
(!a0 a1. fn (NODE a0 a1) = f1 a0 a1 (fn a0) (fn a1)))
The theorem returned by # define_type "term = Var num | Fn num (term list)";;
val it : thm * thm =
(|- !P0 P1.
(!a. P0 (Var a)) /\
(!a0 a1. P1 a1 ==> P0 (Fn a0 a1)) /\
P1 [] /\
(!a0 a1. P0 a0 /\ P1 a1 ==> P1 (CONS a0 a1))
==> (!x0. P0 x0) /\ (!x1. P1 x1),
|- !f0 f1 f2 f3.
?fn0 fn1.
(!a. fn1 (Var a) = f0 a) /\
(!a0 a1. fn1 (Fn a0 a1) = f1 a0 a1 (fn0 a1)) /\
fn0 [] = f2 /\
(!a0 a1. fn0 (CONS a0 a1) = f3 a0 a1 (fn1 a0) (fn0 a1)))
and here we have an example of mutual recursion, defining syntax
trees for commands and expressions for a hypothetical programming language:
# define_type "command = Assign num expression
| Ite expression command command;
expression = Variable num
| Constant num
| Plus expression expression
| Valof command";;
val it : thm * thm =
(|- !P0 P1.
(!a0 a1. P1 a1 ==> P0 (Assign a0 a1)) /\
(!a0 a1 a2. P1 a0 /\ P0 a1 /\ P0 a2 ==> P0 (Ite a0 a1 a2)) /\
(!a. P1 (Variable a)) /\
(!a. P1 (Constant a)) /\
(!a0 a1. P1 a0 /\ P1 a1 ==> P1 (Plus a0 a1)) /\
(!a. P0 a ==> P1 (Valof a))
==> (!x0. P0 x0) /\ (!x1. P1 x1),
|- !f0 f1 f2 f3 f4 f5.
?fn0 fn1.
(!a0 a1. fn0 (Assign a0 a1) = f0 a0 a1 (fn1 a1)) /\
(!a0 a1 a2.
fn0 (Ite a0 a1 a2) =
f1 a0 a1 a2 (fn1 a0) (fn0 a1) (fn0 a2)) /\
(!a. fn1 (Variable a) = f2 a) /\
(!a. fn1 (Constant a) = f3 a) /\
(!a0 a1. fn1 (Plus a0 a1) = f4 a0 a1 (fn1 a0) (fn1 a1)) /\
(!a. fn1 (Valof a) = f5 a (fn0 a)))