Filter
Top Products
11.2. FREE RECURSIVE TYPES 89
#let finite_RULES,finite_INDUCT,finite_CASES =
new_inductive_definition
‘finite {} /\
!x s. finite s ==> finite (x INSERT s)‘;;
Warning: inventing type variables
finite_RULES : thm =
|- finite EMPTY /\ (!x s. finite s ==> finite (x INSERT s))
finite_INDUCT : thm =
|- !finite’. finite’ EMPTY /\ (!x s. finite’ s ==> finite’ (x INSERT s))
==> (!a. finite a ==> finite’ a)
finite_CASES : thm =
|- !a. finite a = (a = EMPTY) \/ (?x s. (a = x INSERT s) /\ finite s)
HOL Light allows the user to define mutually inductive relations. For example
here are predicates for evenness and oddity:
#let even_odd_RULES,even_odd_INDUCT,even_odd_CASES =
new_inductive_definition
‘even 0 /\
(!n. even(n) ==> odd(n + 1)) /\
(!n. odd(n) ==> even(n + 1))‘;;
even_odd_RULES : thm =
|- even 0 /\ (!n. even n ==> odd (n + 1)) /\ (!n. odd n ==> even (n + 1))
even_odd_INDUCT : thm =
|- !odd’ even’.
even’ 0 /\
(!n. even’ n ==> odd’ (n + 1)) /\
(!n. odd’ n ==> even’ (n + 1))
==> (!a0. odd a0 ==> odd’ a0) /\ (!a1. even a1 ==> even’ a1)
even_odd_CASES : thm =
|- (!a0. odd a0 = (?n. (a0 = n + 1) /\ even n)) /\
(!a1. even a1 = (a1 = 0) \/ (?n. (a1 = n + 1) /\ odd n))
The induction theorem can be applied conveniently during backward proof using
the tactical RULE INDUCT THEN, or in simple cases just with MATCH MP TAC.
11.2 Free recursive types
HOL Light’s primitive type definition facility is rather awkward to work with. One
of the most useful, and complicated, derived rules in HOL Light allows one to define
recursive types much as in CAML, even using a similar syntax. There are some
restrictions; for example a function space involving the type being defined cannot be
used. However types can be defined mutually recursively and can involve instances
of previously defined type constructors. The primitive function is define type, and
it always returns two theorems, the first a kind of induction theorem for the new
type, the second a justification of definition by primitive recursion. For example we
can define binary trees: