author paulson Fri Dec 22 13:38:57 1995 +0100 (1995-12-22) 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 | revisions
     1.1 --- a/doc-src/ind-defs.tex	Fri Dec 22 13:33:40 1995 +0100
1.2 +++ b/doc-src/ind-defs.tex	Fri Dec 22 13:38:57 1995 +0100
1.3 @@ -307,8 +307,12 @@
1.4  The package returns its result as an ML structure, which consists of named
1.5  components; we may regard it as a record.  The result structure contains
1.6  the definitions of the recursive sets as a theorem list called {\tt defs}.
1.7 -It also contains, as the theorem {\tt unfold}, a fixedpoint equation such
1.8 -as
1.9 +It also contains some theorems; {\tt dom\_subset} is an inclusion such as
1.10 +$\Fin(A)\sbs\pow(A)$, while {\tt bnd\_mono} asserts that the fixedpoint
1.11 +definition is monotonic.
1.12 +
1.13 +Internally the package uses the theorem {\tt unfold}, a fixedpoint equation
1.14 +such as
1.15  \begin{eqnarray*}
1.16    \Fin(A) & = &
1.17    \begin{array}[t]{r@{\,}l}
1.18 @@ -316,8 +320,7 @@
1.19               &(\exists a\,b. z=\{a\}\un b\conj a\in A\conj b\in \Fin(A))\}
1.20    \end{array}
1.21  \end{eqnarray*}
1.22 -It also contains, as the theorem {\tt dom\_subset}, an inclusion such as
1.23 -$\Fin(A)\sbs\pow(A)$.
1.24 +In order to save space, this theorem is not exported.
1.25
1.26
1.27  \subsection{Mutual recursion} \label{mutual-sec}
1.28 @@ -508,7 +511,7 @@
1.29  $\cons(a,b)$ abbreviates $\{a\}\un b$ in Isabelle/ZF.
1.30  \begin{ttbox}
1.31  Finite = Arith +
1.32 -consts      Fin :: "i=>i"
1.33 +consts      Fin :: i=>i
1.34  inductive
1.35    domains   "Fin(A)" <= "Pow(A)"
1.36    intrs
1.37 @@ -567,7 +570,7 @@
1.38  specifying the domain as $\nat\times\lst(A)$:
1.39  \begin{ttbox}
1.40  ListN = List +
1.41 -consts  listn ::"i=>i"
1.42 +consts  listn :: i=>i
1.43  inductive
1.44    domains   "listn(A)" <= "nat*list(A)"
1.45    intrs
1.46 @@ -687,7 +690,7 @@
1.47  To make this coinductive definition, the theory file includes (after the
1.48  declaration of $\llist(A)$) the following lines:
1.49  \begin{ttbox}
1.50 -consts    lleq :: "i=>i"
1.51 +consts    lleq :: i=>i
1.52  coinductive
1.53    domains "lleq(A)" <= "llist(A) * llist(A)"
1.54    intrs
1.55 @@ -749,7 +752,7 @@
1.56    Pow\_mono}, which asserts that $\pow$ is monotonic.
1.57  \begin{ttbox}
1.58  Acc = WF +
1.59 -consts    acc :: "i=>i"
1.60 +consts    acc :: i=>i
1.61  inductive
1.62    domains "acc(r)" <= "field(r)"
1.63    intrs
1.64 @@ -825,8 +828,8 @@
1.65  \begin{ttbox}
1.66  Primrec = List +
1.67  consts
1.68 -  primrec :: "i"
1.69 -  SC      :: "i"
1.70 +  primrec :: i
1.71 +  SC      :: i
1.72    $$\vdots$$
1.73  defs
1.74    SC_def    "SC == lam l:list(nat).list_case(0, %x xs.succ(x), l)"
1.75 @@ -1000,15 +1003,15 @@
1.76  \subsection{Example: lists and lazy lists}\label{lists-sec}
1.77  Here is a theory file that declares the datatype of lists:
1.78  \begin{ttbox}
1.79 -List = Univ +
1.80 -consts  list :: "i=>i"
1.81 +List = Datatype +
1.82 +consts  list :: i=>i
1.83  datatype "list(A)" = Nil | Cons ("a:A", "l: list(A)")
1.84  end
1.85  \end{ttbox}
1.86  And here is the theory file that declares the codatatype of lazy lists:
1.87  \begin{ttbox}
1.88 -LList = QUniv +
1.89 -consts  llist :: "i=>i"
1.90 +LList = Datatype +
1.91 +consts  llist :: i=>i
1.92  codatatype "llist(A)" = LNil | LCons ("a: A", "l: llist(A)")
1.93  end
1.94  \end{ttbox}
1.95 @@ -1020,15 +1023,15 @@
1.96
1.97  Each form of list has two constructors, one for the empty list and one for
1.98  adding an element to a list.  Each takes a parameter, defining the set of
1.99 -lists over a given set~$A$.  Each uses the appropriate domain from a
1.100 -Isabelle/ZF theory:
1.101 +lists over a given set~$A$.  Each specifies {\tt Datatype} as the parent
1.102 +theory; this implicitly specifies {\tt Univ} and {\tt QUniv} as ancestors,
1.103 +making available the definitions of $\univ$ and $\quniv$.  Each is
1.104 +automatically given the appropriate domain:
1.105  \begin{itemize}
1.106 -\item $\lst(A)$ requires the parent theory {\tt Univ}.  The package
1.107 -  automatically uses the domain $\univ(A)$ (the default choice can be
1.108 +\item $\lst(A)$ uses the domain $\univ(A)$ (the default choice can be
1.109    overridden).
1.110
1.111 -\item $\llist(A)$ requires the parent theory {\tt QUniv}.  The package
1.112 -  automatically uses the domain $\quniv(A)$.
1.113 +\item $\llist(A)$ uses the domain $\quniv(A)$.
1.114  \end{itemize}
1.115
1.116  Since $\lst(A)$ is a datatype, it enjoys a structural induction rule, {\tt
1.117 @@ -1084,7 +1087,7 @@
1.118  $\Fnil$ and~$\Fcons$:
1.119  \begin{ttbox}
1.120  TF = List +
1.121 -consts  tree, forest, tree_forest    :: "i=>i"
1.122 +consts  tree, forest, tree_forest    :: i=>i
1.123  datatype "tree(A)"   = Tcons ("a: A",  "f: forest(A)")
1.124  and      "forest(A)" = Fnil  |  Fcons ("t: tree(A)",  "f: forest(A)")
1.125  end
1.126 @@ -1152,8 +1155,8 @@
1.127  Finally let us consider a fairly general datatype.  It has four
1.128  constructors $\Con_0$, \ldots, $\Con_3$, with the corresponding arities.
1.129  \begin{ttbox}
1.130 -Data = Univ +
1.131 -consts    data :: "[i,i] => i"
1.132 +Data = Datatype +
1.133 +consts    data :: [i,i] => i
1.134  datatype  "data(A,B)" = Con0
1.135                        | Con1 ("a: A")
1.136                        | Con2 ("a: A", "b: B")
1.137 @@ -1324,6 +1327,14 @@
1.138  The need for such efforts is not a drawback of the fixedpoint
1.139  approach, for the alternative is to take such definitions on faith.
1.140
1.141 +Inductive and datatype definitions can take up considerable storage.  The
1.142 +introduction rules are replicated in slightly different forms as fixedpoint
1.143 +definitions, elimination rules and induction rules.  Here are two examples.
1.144 +Three datatypes and three inductive definitions specify the operational
1.145 +semantics of a simple imperative language; they occupy over 600K in total.
1.146 +One datatype definition, an enumeration type with 60 constructors, requires
1.147 +nearly 560K\@.
1.148 +
1.149  The approach is not restricted to set theory.  It should be suitable for
1.150  any logic that has some notion of set and the Knaster-Tarski Theorem.  I
1.151  have ported the (co)inductive definition package from Isabelle/ZF to
1.152 @@ -1360,9 +1371,6 @@
1.153
1.154  \item[\tt bnd\_mono] is a monotonicity theorem for the fixedpoint operator.
1.155
1.156 -\item[\tt unfold] is a fixedpoint equation for the recursive set (the union of
1.157 -the recursive sets, in the case of mutual recursion).
1.158 -
1.159  \item[\tt dom\_subset] is a theorem stating inclusion in the domain.
1.160
1.161  \item[\tt intrs] is the list of introduction rules, now proved as theorems, for
1.162 @@ -1376,7 +1384,9 @@
1.163  \end{description}
1.164
1.165  For an inductive definition, the result structure contains two induction rules,
1.166 -{\tt induct} and \verb|mutual_induct|.  For a coinductive definition, it
1.167 +{\tt induct} and \verb|mutual_induct|.  (To save storage, the latter rule is
1.168 +replaced by {\tt True} if it is not significantly different from
1.169 +{\tt induct}.)  For a coinductive definition, it
1.170  contains the rule \verb|coinduct|.
1.171
1.172  Figure~\ref{def-result-fig} summarizes the two result signatures,
1.173 @@ -1388,7 +1398,6 @@
1.174  val thy          : theory
1.175  val defs         : thm list
1.176  val bnd_mono     : thm
1.177 -val unfold       : thm
1.178  val dom_subset   : thm
1.179  val intrs        : thm list
1.180  val elim         : thm