Note that unfold is not exported, that mutual_induct can
authorpaulson
Fri Dec 22 13:38:57 1995 +0100 (1995-12-22)
changeset 14211471e85624a7
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
     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