----------------------------------------------------------------------
TypeBase
----------------------------------------------------------------------
structure TypeBase

SYNOPSIS
A database of facts stemming from datatype declarations.

KEYWORDS
type, datatype, constructor, induction, primitive recursion.

DESCRIBE
The structure {TypeBase} provides an interface to a database that
is updated when a new datatype is introduced with {Hol_datatype}.
When a new datatype is declared, a collection of theorems "about" the
type can be automatically derived. These are indeed proved, and are
stored in the current theory segment. They are also automatically stored
in {TypeBase}.

The interface to {TypeBase} is intended to provide support for writers
of high-level tools for reasoning about datatypes.

EXAMPLE

   > Datatype `tree = Leaf | Node 'a tree tree`;
   <<HOL message: Defined type: "tree">>
   val it = () : unit

   > TypeBase.read {Thy = current_theory(), Tyop = "tree"};
   val it =
      SOME
       -----------------------
       -----------------------
       HOL datatype: "scratch$tree"
       Primitive recursion:
        |- !f0 f1.
               ?fn.
                   (fn Leaf = f0) /\
                   !a0 a1 a2. fn (Node a0 a1 a2) = f1 a0 a1 a2 (fn a1) (fn a2)
       Case analysis:
        |- (!v f. tree_CASE Leaf v f = v) /\
           !a0 a1 a2 v f. tree_CASE (Node a0 a1 a2) v f = f a0 a1 a2
       Size:
        |- (!f. tree_size f Leaf = 0) /\
           !f a0 a1 a2.
               tree_size f (Node a0 a1 a2) =
               1 + (f a0 + (tree_size f a1 + tree_size f a2))
       Induction:
        |- !P.
               P Leaf /\ (!t t0. P t /\ P t0 ==> !a. P (Node a t t0)) ==>
               !t. P t
       Case completeness: |- !tt. (tt = Leaf) \/ ?a t t0. tt = Node a t t0
       Case-const equality split:
        |- (tree_CASE x v f = v') <=>
           (x = Leaf) /\ (v = v') \/
           ?a t t0. (x = Node a t t0) /\ (f a t t0 = v')
       Extras: [ ]
       One-to-one:
        |- !a0 a1 a2 a0' a1' a2'.
               (Node a0 a1 a2 = Node a0' a1' a2') <=>
               (a0 = a0') /\ (a1 = a1') /\ (a2 = a2')
       Distinctness: |- !a2 a1 a0. Leaf <> Node a0 a1 a2: tyinfo option


SEEALSO
bossLib.Datatype.

----------------------------------------------------------------------