summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

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.

--- 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