Datatype : hol_type quotation -> unit
spec ::= [ <binding> ; ]* <binding> binding ::= <ident> = [ <clause> | ]* <clause> | <ident> = <| [ <ident> : <type> ; ]* <ident> : <type> |> clause ::= <ident> <tyspec>* tyspec ::= ( <type> ) | <atomic-type>
When a datatype is successfully defined, a number of standard theorems are automatically proved about the new type: the constructors of the type are proved to be injective and disjoint, induction and case analysis theorems are proved, and each type also has a ‘size’ function defined for it. All these theorems are stored in the current theory and added to a database accessed via the functions in TypeBase.
The notation used to declare datatypes is, unfortunately, not the same as that of ML. If anything, the syntax is rather more like Haskell’s. For example, an ML declaration
datatype ('a,'b) btree = Leaf of 'a | Node of ('a,'b) btree * 'b * ('a,'b) btree
Datatype `btree = Leaf 'a | Node btree 'b btree`
When a record type is defined, the parser is adjusted to allow new syntax (appropriate for records), and a number of useful simplification theorems are also proved. The most useful of the latter are automatically stored in the TypeBase and can be inspected using the simpls_of function. For further details on record types, see the DESCRIPTION.
To start, enumerated types can be defined as in the following example:
Datatype `enum = A1 | A2 | A3 | A4 | A5 | A6 | A7 | A8 | A9 | A10 | A11 | A12 | A13 | A14 | A15 | A16 | A17 | A18 | A19 | A20 | A21 | A22 | A23 | A24 | A25 | A26 | A27 | A28 | A29 | A30`
Datatype `foo = N num | B bool | Fn ('a -> 'b) | Pr ('a # 'b`)
Datatype `tree = Leaf num | Node tree tree`
Datatype `tree = Leaf 'a | Node (tree # 'b # tree)`
The basic syntax of the named lambda calculus is easy to describe:
- load "stringTheory"; > val it = () : unit - Datatype `lambda = Var string | Const 'a | Comb lambda lambda | Abs lambda lambda`
Datatype `dB = Var string | Const 'a | Bound num | Comb dB dB | Abs dB`
Datatype `ntree = Node of 'a (ntree list)`
Datatype `term = Var string | Fnapp (string # term list)`
Datatype `atexp = var_exp string | let_exp dec exp ; exp = aexp atexp | app_exp exp atexp | fn_exp match ; match = match rule | matchl rule match ; rule = rule pat exp ; dec = val_dec valbind | local_dec dec dec | seq_dec dec dec ; valbind = bind pat exp | bindl pat exp valbind | rec_bind valbind ; pat = wild_pat | var_pat string`
Datatype `state = <| Reg1 : num; Reg2 : num; Waiting : bool |>`
Datatype `file = Text string | Dir directory ; directory = <| owner : string ; files : (string # file) list |>`
First, an empty type is not allowed in HOL, so the following attempt is doomed to fail.
Datatype `foo = A foo`
Datatype `btree = Leaf 'a | Node (('a # 'a) btree)`
Datatype `lazylist = Nil | Cons ('a # (one -> lazylist))`
Finally, for cardinality reasons, HOL does not allow the following attempt to model the untyped lambda calculus as a set (note the -> in the clause for the Abs constructor):
Datatype `lambda = Var string | Const 'a | Comb lambda lambda | Abs (lambda -> lambda)`
For example, invoking
Datatype `tree = Leaf num | Node tree tree`;
tree_case_def = |- (!a f f1. tree_CASE (Leaf a) f f1 = f a) /\ !a0 a1 f f1. tree_CASE (Node a0 a1) f f1 = f1 a0 a1 tree_size_def |- (!a. tree_size (Leaf a) = 1 + a) /\ !a0 a1. tree_size (Node a0 a1) = 1 + (tree_size a0 + tree_size a1)
tree_Axiom |- !f0 f1. ?fn. (!a. fn (Leaf a) = f0 a) /\ !a0 a1. fn (Node a0 a1) = f1 a0 a1 (fn a0) (fn a1) tree_induction |- !P. (!n. P (Leaf n)) /\ (!t t0. P t /\ P t0 ==> P (Node t t0)) ==> !t. P t tree_nchotomy |- !t. (?n. t = Leaf n) \/ ?t' t0. t = Node t' t0 tree_11 |- (!a a'. (Leaf a = Leaf a') = (a = a')) /\ !a0 a1 a0' a1'. (Node a0 a1 = Node a0' a1') = (a0=a0') /\ (a1=a1') tree_distinct |- !a1 a0 a. Leaf a <> Node a0 a1 tree_case_cong |- !M M' f f1. (M = M') /\ (!a. (M' = Leaf a) ==> (f a = f' a)) /\ (!a0 a1. (M' = Node a0 a1) ==> (f1 a0 a1 = f1' a0 a1)) ==> (tree_CASE M f f1 = tree_CASE M' f' f1')
A definition of mutually recursives types results in the above theorems and definitions being added for each of the defined types.