Filter
Top Products
90 CHAPTER 11. PRINCIPLES OF DEFINITION
#let btree_INDUCT,btree_RECURSION = define_type
"btree = Leaf A
| Branch btree btree";;
btree_INDUCT : thm =
|- !P. (!a. P (Leaf a)) /\ (!a0 a1. P a0 /\ P a1 ==> P (Branch a0 a1))
==> (!x. P x)
btree_RECURSION : thm =
|- !f0 f1.
?fn. (!a. fn (Leaf a) = f0 a) /\
(!a0 a1. fn (Branch a0 a1) = f1 a0 a1 (fn a0) (fn a1))
This defines a new type constructor (A)btree, since the definition contained a
free type variable A. The recursion theorem can be used later to define functions
by ‘primitive recursion’, i.e. defining a function on a type constructor in terms of
the function on its arguments. For example here are functions to reflect a tree, i.e.
swap left and right subtrees, and add up all the integers in an (int)btree:
#let reflect = new_recursive_definition btree_RECURSION
‘(reflect(Leaf x) = Leaf x) /\
(reflect(Branch t1 t2) = Branch (reflect t2) (reflect t1))‘;;
Warning: inventing type variables
reflect : thm =
|- (reflect (Leaf x) = Leaf x) /\
(reflect (Branch t1 t2) = Branch (reflect t2) (reflect t1))
#let addup = new_recursive_definition btree_RECURSION
‘(addup (Leaf n) = n) /\
(addup (Branch t1 t2) = addup t1 + addup t2)‘;;
addup : thm =
|- (addup (Leaf n) = n) /\ (addup (Branch t1 t2) = addup t1 + addup t2)
The induction theorem can be used to prove theorems about objects of the new
type. In simple cases one can just use MATCH MP TAC; for example:
#let ADDUP_REFLECT = prove
(‘!t. addup(reflect t) = addup t‘,
MATCH_MP_TAC btree_INDUCT THEN
SIMP_TAC[addup; reflect; ADD_AC]);;
ADDUP_REFLECT : thm = |- !t. addup (reflect t) = addup t
Having defined a type constructor like btree, it can itself be used in the defini-
tion of new types. For example HOL Light already has a type of lists defined using
the definition list = NIL | CONS A list, and we can create a type of finitely-
branching trees like this: