author paulson Fri, 22 Dec 1995 13:38:57 +0100 changeset 1421 1471e85624a7 parent 1420 04eabfa73d83 child 1422 bc628f4ef0cb
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.
 doc-src/ind-defs.tex file | annotate | diff | comparison | revisions
--- 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