Documentation reflecting preference for Datatype over Hol_datatype.

Some code changes as well, most importantly in TUTORIAL's
examples/ind_def/clScript.sml.

Manual/Description/libraries.tex

@@ -2122,7 +2122,7 @@ \subsubsection{The ``stateful'' \simpset---\ml{srw\_ss()}}
 This versatility is illustrated in the following example:
 \begin{session}
 \begin{verbatim}
-- Hol_datatype `tree = Leaf | Node of num => tree => tree`;
+- Datatype `tree = Leaf | Node num tree tree`;
 <<HOL message: Defined type: "tree">>
 > val it = () : unit
 

Manual/Description/misc.tex

@@ -971,10 +971,10 @@ \subsection{Munging Commands}
 %
 This prints the specified theorem with a leading turnstile.
 %
-\index{Hol_datatype@\ml{Hol\_datatype}!printing in LaTeX@printing in \LaTeX{}}
-However, as a special case, if the theorem specified is a ``datatype theorem'' (with a name of the form \texttt{datatype\_}$\langle$\textit{type-name}$\rangle$), a BNF-style description of the given type (one that has been defined with \ml{Hol\_datatype}) will be printed.
+\index{Datatype@\ml{Datatype}!printing in LaTeX@printing in \LaTeX{}}
+However, as a special case, if the theorem specified is a ``datatype theorem'' (with a name of the form \texttt{datatype\_}$\langle$\textit{type-name}$\rangle$), a BNF-style description of the given type (one that has been defined with \ml{Datatype}) will be printed.
 %
-Datatype theorems with these names are automatically generated when \ml{Hol\_datatype} is run.
+Datatype theorems with these names are automatically generated when \ml{Datatype} is run.
 
 By default, the output is \emph{not} wrapped in an \texttt{\bs{}mbox}, making it best suited for inclusion in an environment such as \texttt{alltt}.
 (The important characteristics of the \texttt{alltt} environment are that it respects layout in terms of newlines, while also allowing the insertion of \LaTeX{} commands.

Manual/Tutorial/combin.tex

@@ -40,7 +40,7 @@ \section{The type of combinators}
 \setcounter{sessioncount}{0}
 \begin{session}
 \begin{verbatim}
-- Hol_datatype `cl = K | S | # of cl => cl`;
+- Datatype `cl = K | S | # cl cl`;
 > val it = () : unit
 \end{verbatim}
 \end{session}

examples/computability/lambda/Holmakefile

@@ -10,6 +10,8 @@ BARE_THYS = ../../lambda/barendregt/normal_orderTheory \
             ../../lambda/other-models/pure_dBTheory
 DEPS = $(patsubst %,%.uo,$(BARE_THYS))
 
+alltheories: $(patsubst %Script.sml,%Theory.uo,$(wildcard *Script.sml))
+
 $(HOLHEAP): $(DEPS)
 	$(protect $(HOLDIR)/bin/buildheap) -o computability-heap $(BARE_THYS)
 

examples/ind_def/clScript.sml

@@ -4,7 +4,7 @@ open bossLib simpLib
 
 val _ = new_theory "cl";
 
-val _ = Hol_datatype `cl = S | K | # of cl => cl`;
+val _ = Datatype `cl = S | K | # cl cl`;
 
 val _ = set_fixity "#"  (Infixl 1100);
 

examples/lambda/basics/generic_termsScript.sml

@@ -17,9 +17,9 @@ val _ = new_theory "generic_terms"
 
 val _ = computeLib.auto_import_definitions := false
 
-val _ = Hol_datatype `
-  pregterm = var of string => 'v
-           | lam of string => 'b => pregterm list => pregterm list
+val _ = Datatype `
+  pregterm = var string 'v
+           | lam string 'b (pregterm list) (pregterm list)
 `;
 
 val fv_def = Define `

examples/lambda/other-models/lnamelessScript.sml

@@ -20,12 +20,7 @@ fun Store_thm (p as (n,t,tac)) = store_thm p before export_rewrites [n]
 
 val _ = new_theory "lnameless"
 
-val _ = Hol_datatype `
-  lnt = var of string
-      | bnd of num
-      | app of lnt => lnt
-      | abs of lnt
-`;
+val _ = Hol_datatype`lnt = var string | bnd num | app lnt lnt | abs lnt`;
 
 val open_def = Define`
   (open k u (bnd i) = if i = k then u else bnd i) /\
@@ -205,7 +200,7 @@ val lclosed_abs_cofin = store_thm(
     METIS_TAC [abs_lclosed_I]
   ]);
 
-val _ = Hol_datatype `ltype = tyOne | tyFun of ltype => ltype`;
+val _ = Datatype `ltype = tyOne | tyFun ltype ltype`;
 
 val _ = set_fixity "-->" (Infixr 700)
 val _ = overload_on ("-->", ``tyFun``);
@@ -461,4 +456,3 @@ val typing_cotyping = store_thm(
   METIS_TAC [cotyping_rules]);
 
 val _ = export_theory();
-

examples/lambda/other-models/pure_dBScript.sml

@@ -11,7 +11,7 @@ val _ = new_theory "pure_dB"
 val _ = set_fixity "=" (Infix(NONASSOC, 100))
 
 (* the type of pure de Bruijn terms *)
-val _ = Hol_datatype`pdb = dV of num | dAPP of pdb => pdb | dABS of pdb`
+val _ = Datatype`pdb = dV num | dAPP pdb pdb | dABS pdb`
 
 (* Definitions of lift and substitution from Nipkow's "More Church-Rosser
    proofs" *)

help/Docfiles/bossLib.Datatype.doc

@@ -0,0 +1,285 @@
+\DOC Datatype
+
+\TYPE {Datatype : type quotation -> unit}
+
+\SYNOPSIS
+Define a concrete datatype.
+
+\KEYWORDS
+type, concrete, definition.
+
+\DESCRIBE
+Many formalizations require the definition of new types.  For
+example, ML-style datatypes are commonly used to model the abstract
+syntax of programming languages and the state-space of elaborate
+transition systems.  In HOL, such datatypes (at least, those that are
+inductive, or, alternatively, have a model in an initial algebra) may be
+specified using the invocation {Datatype `<spec>`}, where
+{<spec>} should conform to the following grammar:
+{
+   spec    ::= [ <binding> ; ]* <binding>
+
+   binding ::= <ident> = [ <clause> | ]* <clause>
+            |  <ident> = <| [ <ident> : <type> ; ]* <ident> : <type> |>
+
+   clause  ::= <ident> <tyspec>*
+
+   tyspec  ::= ( <type> )
+            |  <atomic-type>
+}
+where {<atomic-type>} is a single token denoting a type. For example,
+{num}, {bool} and {'a}.
+
+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
+}
+would most likely be declared in HOL as
+{
+   Datatype `btree = Leaf 'a
+                   | Node btree 'b btree`
+}
+Note that any type parameters for the new type are not allowed; they
+are inferred from the right hand side of the binding. The type
+variables in the specification become arguments to the new type
+operator in alphabetic order.
+
+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.
+
+\EXAMPLE
+In the following, we shall give an overview of the kinds of types that
+may be defined by {Datatype}.
+
+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`
+
+}
+Other non-recursive types may be defined as well:
+{
+   Datatype `foo = N num
+                 | B bool
+                 | Fn ('a -> 'b)
+                 | Pr ('a # 'b`)
+}
+Turning to recursive types, we can define a type of binary trees
+where the leaves are numbers.
+{
+   Datatype `tree = Leaf num | Node tree tree`
+}
+We have already seen a type of binary trees having polymorphic values
+at internal nodes. This time, we will declare it in ``paired'' format.
+{
+    Datatype `tree = Leaf 'a
+                   | Node (tree # 'b # tree)`
+}
+This specification seems closer to the declaration that one might make
+in ML, but is more difficult to deal with in proof than the curried format
+used above.
+
+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`
+}
+The syntax for `de Bruijn' terms is roughly similar:
+{
+   Datatype `dB = Var string
+                | Const 'a
+                | Bound num
+                | Comb dB dB
+                | Abs dB`
+}
+Arbitrarily branching trees may be defined by allowing a node to hold
+the list of its subtrees. In such a case, leaf nodes do not need to be
+explicitly declared.
+{
+   Datatype `ntree = Node of 'a (ntree list)`
+}
+A (tupled) type of `first order terms' can be declared as follows:
+{
+   Datatype `term = Var string
+                  | Fnapp (string # term list)`
+}
+Mutally recursive types may also be defined. The following, extracted by
+Elsa Gunter from the Definition of Standard ML, captures a subset of
+Core ML.
+{
+   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`
+}
+Simple record types may be introduced using the {<| ... |>} notation.
+{
+    Datatype `state = <| Reg1 : num; Reg2 : num; Waiting : bool |>`
+}
+The use of record types may be recursive. For example, the following
+declaration could be used to formalize a simple file system.
+{
+   Datatype
+     `file = Text string
+           | Dir directory
+       ;
+      directory = <| owner : string ;
+                     files : (string # file) list |>`
+}
+
+\FAILURE
+Now we address some types that cannot be declared with {Datatype}. In
+some cases they cannot exist in HOL at all; in others, the type can be
+built in the HOL logic, but {Datatype} is not able to make the
+definition.
+
+First, an empty type is not allowed in HOL, so the following attempt
+is doomed to fail.
+{
+   Datatype `foo = A foo`
+}
+So called `nested types', which are occasionally quite useful, cannot
+at present be built with {Datatype}:
+{
+   Datatype `btree = Leaf 'a
+                   | Node (('a # 'a) btree)`
+}
+Co-algebraic types may not currently be built with {Datatype}, not
+even by attempting to encode the remainder of the list as a function:
+{
+   Datatype `lazylist = Nil
+                      | Cons ('a # (one -> lazylist))`
+}
+Indeed, this specification corresponds to an algebraic type isomorphic
+to ``standard'' lists, but {Datatype} rejects it because it cannot
+handle recursion to the right of a function arrow. The type of
+co-algebraic lists can be built in HOL: see {llistTheory}.
+
+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)`
+}
+Instead, one would have to build a theory of complete partial orders
+(or something similar) with which to model the untyped lambda calculus.
+
+\COMMENTS
+
+The consequences of an invocation of {Datatype} are stored in the
+current theory segment and in {TypeBase}. The principal consequences
+of a datatype definition are the primitive recursion and induction
+theorems. These provide the ability to define simple functions over
+the type, and an induction principle for the type. For a type named
+{ty}, the primitive recursion theorem is stored under {ty_Axiom} and
+the induction theorem is put under {ty_induction}. Other consequences
+include the distinctness of constructors ({ty_distinct}), and the
+injectivity of constructors ({ty_11}). A `degenerate' version of
+{ty_induction} is also stored under {ty_nchotomy}: it provides for
+reasoning by cases on the construction of elements of {ty}. Finally,
+some special-purpose theorems are stored: {ty_case_cong} gives a
+congruence theorem for ``case'' statements on elements of {ty}. These
+case statements are introduced by {ty_case_def}. Also, a definition of
+the ``size'' of the type is added to the current theory, under the name
+{ty_size_def}.
+
+For example, invoking
+{
+   Datatype `tree = Leaf num | Node tree tree`;
+}
+results in the definitions
+{
+   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)
+}
+being added to the current theory. The following theorems about the datatype
+are also stored in the current theory.
+{
+   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')
+}
+When a type involving records is defined, many more definitions are
+made and added to the current theory.
+
+A definition of mutually recursives types results in the above theorems and
+definitions being added for each of the defined types.
+
+\SEEALSO
+Definition.new_type_definition, TotalDefn.Define, IndDefLib.Hol_reln,
+TypeBase.
+
+\ENDDOC