Filter
Top Products
11.2. FREE RECURSIVE TYPES 91
#let xtree_INDUCTION,xtree_RECURSION = define_type
"xtree = Lf A
| Br (xtree list)";;
xtree_INDUCTION : thm =
|- !P0 P1.
(!a. P0 (Lf a)) /\
(!a. P1 a ==> P0 (Br a)) /\
P1 [] /\
(!a0 a1. P0 a0 /\ P1 a1 ==> P1 (CONS a0 a1))
==> (!x0. P0 x0) /\ (!x1. P1 x1)
xtree_RECURSION : thm =
|- !f0 f1 f2 f3.
?fn0 fn1.
(!a. fn1 (Lf a) = f0 a) /\
(!a. fn1 (Br a) = f1 a (fn0 a)) /\
(fn0 [] = f2) /\
(!a0 a1. fn0 (CONS a0 a1) = f3 a0 a1 (fn1 a0) (fn0 a1))
The induction and recursion theorems are as if the list constructor had been
defined mutually recursively, but it uses the standard type of lists.