# HG changeset patch
# User paulson
# Date 819635937 -3600
# Node ID 1471e85624a79f226f4650f2e2a221e249fd0f9d
# Parent  04eabfa73d83ab471f1f65fe9a44f4dc8e8d5fed
Note that unfold is not exported, that mutual_induct can
be omitted (as the trivial theorem True), and comments on storage

Also uses Datatype instead of Univ/Quniv as parent theory for lists, and
omits quotes around types in theory files.

diff -r 04eabfa73d83 -r 1471e85624a7 doc-src/ind-defs.tex
--- a/doc-src/ind-defs.tex	Fri Dec 22 13:33:40 1995 +0100
+++ b/doc-src/ind-defs.tex	Fri Dec 22 13:38:57 1995 +0100
@@ -307,8 +307,12 @@
 The package returns its result as an ML structure, which consists of named
 components; we may regard it as a record.  The result structure contains
 the definitions of the recursive sets as a theorem list called {\tt defs}.
-It also contains, as the theorem {\tt unfold}, a fixedpoint equation such
-as
+It also contains some theorems; {\tt dom\_subset} is an inclusion such as 
+$\Fin(A)\sbs\pow(A)$, while {\tt bnd\_mono} asserts that the fixedpoint
+definition is monotonic.
+
+Internally the package uses the theorem {\tt unfold}, a fixedpoint equation
+such as
 \begin{eqnarray*}
   \Fin(A) & = &
   \begin{array}[t]{r@{\,}l}
@@ -316,8 +320,7 @@
              &(\exists a\,b. z=\{a\}\un b\conj a\in A\conj b\in \Fin(A))\}
   \end{array}
 \end{eqnarray*}
-It also contains, as the theorem {\tt dom\_subset}, an inclusion such as 
-$\Fin(A)\sbs\pow(A)$.
+In order to save space, this theorem is not exported.  
 
 
 \subsection{Mutual recursion} \label{mutual-sec}
@@ -508,7 +511,7 @@
 $\cons(a,b)$ abbreviates $\{a\}\un b$ in Isabelle/ZF.
 \begin{ttbox}
 Finite = Arith + 
-consts      Fin :: "i=>i"
+consts      Fin :: i=>i
 inductive
   domains   "Fin(A)" <= "Pow(A)"
   intrs
@@ -567,7 +570,7 @@
 specifying the domain as $\nat\times\lst(A)$:
 \begin{ttbox}
 ListN = List +
-consts  listn ::"i=>i"
+consts  listn :: i=>i
 inductive
   domains   "listn(A)" <= "nat*list(A)"
   intrs
@@ -687,7 +690,7 @@
 To make this coinductive definition, the theory file includes (after the
 declaration of $\llist(A)$) the following lines:
 \begin{ttbox}
-consts    lleq :: "i=>i"
+consts    lleq :: i=>i
 coinductive
   domains "lleq(A)" <= "llist(A) * llist(A)"
   intrs
@@ -749,7 +752,7 @@
   Pow\_mono}, which asserts that $\pow$ is monotonic.
 \begin{ttbox}
 Acc = WF + 
-consts    acc :: "i=>i"
+consts    acc :: i=>i
 inductive
   domains "acc(r)" <= "field(r)"
   intrs
@@ -825,8 +828,8 @@
 \begin{ttbox}
 Primrec = List +
 consts
-  primrec :: "i"
-  SC      :: "i"
+  primrec :: i
+  SC      :: i
   \(\vdots\)
 defs
   SC_def    "SC == lam l:list(nat).list_case(0, %x xs.succ(x), l)"
@@ -1000,15 +1003,15 @@
 \subsection{Example: lists and lazy lists}\label{lists-sec}
 Here is a theory file that declares the datatype of lists:
 \begin{ttbox} 
-List = Univ + 
-consts  list :: "i=>i"
+List = Datatype + 
+consts  list :: i=>i
 datatype "list(A)" = Nil | Cons ("a:A", "l: list(A)")
 end
 \end{ttbox}
 And here is the theory file that declares the codatatype of lazy lists:
 \begin{ttbox}
-LList = QUniv + 
-consts  llist :: "i=>i"
+LList = Datatype + 
+consts  llist :: i=>i
 codatatype "llist(A)" = LNil | LCons ("a: A", "l: llist(A)")
 end
 \end{ttbox}
@@ -1020,15 +1023,15 @@
 
 Each form of list has two constructors, one for the empty list and one for
 adding an element to a list.  Each takes a parameter, defining the set of
-lists over a given set~$A$.  Each uses the appropriate domain from a
-Isabelle/ZF theory:
+lists over a given set~$A$.  Each specifies {\tt Datatype} as the parent
+theory; this implicitly specifies {\tt Univ} and {\tt QUniv} as ancestors,
+making available the definitions of $\univ$ and $\quniv$.  Each is
+automatically given the appropriate domain:
 \begin{itemize}
-\item $\lst(A)$ requires the parent theory {\tt Univ}.  The package
-  automatically uses the domain $\univ(A)$ (the default choice can be
+\item $\lst(A)$ uses the domain $\univ(A)$ (the default choice can be
   overridden). 
 
-\item $\llist(A)$ requires the parent theory {\tt QUniv}.  The package
-  automatically uses the domain $\quniv(A)$.
+\item $\llist(A)$ uses the domain $\quniv(A)$.
 \end{itemize}
 
 Since $\lst(A)$ is a datatype, it enjoys a structural induction rule, {\tt
@@ -1084,7 +1087,7 @@
 $\Fnil$ and~$\Fcons$:
 \begin{ttbox}
 TF = List +
-consts  tree, forest, tree_forest    :: "i=>i"
+consts  tree, forest, tree_forest    :: i=>i
 datatype "tree(A)"   = Tcons ("a: A",  "f: forest(A)")
 and      "forest(A)" = Fnil  |  Fcons ("t: tree(A)",  "f: forest(A)")
 end
@@ -1152,8 +1155,8 @@
 Finally let us consider a fairly general datatype.  It has four
 constructors $\Con_0$, \ldots, $\Con_3$, with the corresponding arities.
 \begin{ttbox}
-Data = Univ +
-consts    data :: "[i,i] => i"
+Data = Datatype +
+consts    data :: [i,i] => i
 datatype  "data(A,B)" = Con0
                       | Con1 ("a: A")
                       | Con2 ("a: A", "b: B")
@@ -1324,6 +1327,14 @@
 The need for such efforts is not a drawback of the fixedpoint
 approach, for the alternative is to take such definitions on faith.
 
+Inductive and datatype definitions can take up considerable storage.  The
+introduction rules are replicated in slightly different forms as fixedpoint
+definitions, elimination rules and induction rules.  Here are two examples.
+Three datatypes and three inductive definitions specify the operational
+semantics of a simple imperative language; they occupy over 600K in total.
+One datatype definition, an enumeration type with 60 constructors, requires
+nearly 560K\@.
+
 The approach is not restricted to set theory.  It should be suitable for
 any logic that has some notion of set and the Knaster-Tarski Theorem.  I
 have ported the (co)inductive definition package from Isabelle/ZF to
@@ -1360,9 +1371,6 @@
 
 \item[\tt bnd\_mono] is a monotonicity theorem for the fixedpoint operator.
 
-\item[\tt unfold] is a fixedpoint equation for the recursive set (the union of
-the recursive sets, in the case of mutual recursion).
-
 \item[\tt dom\_subset] is a theorem stating inclusion in the domain.
 
 \item[\tt intrs] is the list of introduction rules, now proved as theorems, for
@@ -1376,7 +1384,9 @@
 \end{description}
 
 For an inductive definition, the result structure contains two induction rules,
-{\tt induct} and \verb|mutual_induct|.  For a coinductive definition, it
+{\tt induct} and \verb|mutual_induct|.  (To save storage, the latter rule is
+replaced by {\tt True} if it is not significantly different from
+{\tt induct}.)  For a coinductive definition, it
 contains the rule \verb|coinduct|.
 
 Figure~\ref{def-result-fig} summarizes the two result signatures,
@@ -1388,7 +1398,6 @@
 val thy          : theory
 val defs         : thm list
 val bnd_mono     : thm
-val unfold       : thm
 val dom_subset   : thm
 val intrs        : thm list
 val elim         : thm