deleted the appendices because documentation exists in the HOL and ZF manuals
authorpaulson
Wed Jan 13 16:38:52 1999 +0100 (1999-01-13)
changeset 61243aa7926f039a
parent 6123 4ba5066d01fc
child 6125 59507030d953
deleted the appendices because documentation exists in the HOL and ZF manuals
doc-src/Inductive/ind-defs.tex
     1.1 --- a/doc-src/Inductive/ind-defs.tex	Wed Jan 13 16:38:16 1999 +0100
     1.2 +++ b/doc-src/Inductive/ind-defs.tex	Wed Jan 13 16:38:52 1999 +0100
     1.3 @@ -524,7 +524,7 @@
     1.4    intrs
     1.5      emptyI  "0 : Fin(A)"
     1.6      consI   "[| a: A;  b: Fin(A) |] ==> cons(a,b) : Fin(A)"
     1.7 -  type_intrs "[empty_subsetI, cons_subsetI, PowI]"
     1.8 +  type_intrs  empty_subsetI, cons_subsetI, PowI
     1.9    type_elims "[make_elim PowD]"
    1.10  end
    1.11  \end{ttbox}
    1.12 @@ -760,7 +760,7 @@
    1.13    domains "acc(r)" <= "field(r)"
    1.14    intrs
    1.15      vimage  "[| r-``\{a\}: Pow(acc(r)); a: field(r) |] ==> a: acc(r)"
    1.16 -  monos     "[Pow_mono]"
    1.17 +  monos      Pow_mono
    1.18  \end{ttbox}
    1.19  The Isabelle theory proceeds to prove facts about $\acc(\prec)$.  For
    1.20  instance, $\prec$ is well-founded if and only if its field is contained in
    1.21 @@ -846,8 +846,8 @@
    1.22      PROJ     "i: nat ==> PROJ(i) : primrec"
    1.23      COMP     "[| g: primrec; fs: list(primrec) |] ==> COMP(g,fs): primrec"
    1.24      PREC     "[| f: primrec; g: primrec |] ==> PREC(f,g): primrec"
    1.25 -  monos      "[list_mono]"
    1.26 -  con_defs   "[SC_def,CONST_def,PROJ_def,COMP_def,PREC_def]"
    1.27 +  monos       list_mono
    1.28 +  con_defs    SC_def, CONST_def, PROJ_def, COMP_def, PREC_def
    1.29    type_intrs "nat_typechecks @ list.intrs @                      
    1.30                [lam_type, list_case_type, drop_type, map_type,    
    1.31                 apply_type, rec_type]"
    1.32 @@ -1330,262 +1330,4 @@
    1.33  \end{footnotesize}
    1.34  %%%%%\doendnotes
    1.35  
    1.36 -\ifshort\typeout{****Omitting appendices}
    1.37 -\else
    1.38 -\newpage
    1.39 -\appendix
    1.40 -\section{Inductive and coinductive definitions: users guide}
    1.41 -A theory file may contain any number of inductive and coinductive
    1.42 -definitions.  They may be intermixed with other declarations; in
    1.43 -particular, the (co)inductive sets \defn{must} be declared separately as
    1.44 -constants, and may have mixfix syntax or be subject to syntax translations.
    1.45 -
    1.46 -The syntax is rather complicated.  Please consult the examples above and the
    1.47 -theory files on the \textsc{zf} source directory.  
    1.48 -
    1.49 -Each (co)inductive definition adds definitions to the theory and also proves
    1.50 -some theorems.  Each definition creates an \textsc{ml} structure, which is a
    1.51 -substructure of the main theory structure.
    1.52 -
    1.53 -Inductive and datatype definitions can take up considerable storage.  The
    1.54 -introduction rules are replicated in slightly different forms as fixedpoint
    1.55 -definitions, elimination rules and induction rules.  L\"otzbeyer and Sandner's
    1.56 -six definitions occupy over 600K in total.  Defining the 60-constructor
    1.57 -datatype requires nearly 560K\@.
    1.58 -
    1.59 -\subsection{The result structure}
    1.60 -Many of the result structure's components have been discussed
    1.61 -in~\S\ref{basic-sec}; others are self-explanatory.
    1.62 -\begin{description}
    1.63 -\item[\tt thy] is the new theory containing the recursive sets.
    1.64 -
    1.65 -\item[\tt defs] is the list of definitions of the recursive sets.
    1.66 -
    1.67 -\item[\tt bnd\_mono] is a monotonicity theorem for the fixedpoint operator.
    1.68 -
    1.69 -\item[\tt dom\_subset] is a theorem stating inclusion in the domain.
    1.70 -
    1.71 -\item[\tt intrs] is the list of introduction rules, now proved as theorems, for
    1.72 -the recursive sets.  The rules are also available individually, using the
    1.73 -names given them in the theory file. 
    1.74 -
    1.75 -\item[\tt elim] is the elimination rule.
    1.76 -
    1.77 -\item[\tt mk\_cases] is a function to create simplified instances of {\tt
    1.78 -elim}, using freeness reasoning on some underlying datatype.
    1.79 -\end{description}
    1.80 -
    1.81 -For an inductive definition, the result structure contains two induction
    1.82 -rules, {\tt induct} and \verb|mutual_induct|.  (To save storage, the latter
    1.83 -rule is just {\tt True} unless more than one set is being defined.)  For a
    1.84 -coinductive definition, it contains the rule \verb|coinduct|.
    1.85 -
    1.86 -Figure~\ref{def-result-fig} summarizes the two result signatures,
    1.87 -specifying the types of all these components.
    1.88 -
    1.89 -\begin{figure}
    1.90 -\begin{ttbox}
    1.91 -sig
    1.92 -val thy          : theory
    1.93 -val defs         : thm list
    1.94 -val bnd_mono     : thm
    1.95 -val dom_subset   : thm
    1.96 -val intrs        : thm list
    1.97 -val elim         : thm
    1.98 -val mk_cases     : thm list -> string -> thm
    1.99 -{\it(Inductive definitions only)} 
   1.100 -val induct       : thm
   1.101 -val mutual_induct: thm
   1.102 -{\it(Coinductive definitions only)}
   1.103 -val coinduct    : thm
   1.104 -end
   1.105 -\end{ttbox}
   1.106 -\hrule
   1.107 -\caption{The result of a (co)inductive definition} \label{def-result-fig}
   1.108 -\end{figure}
   1.109 -
   1.110 -\subsection{The syntax of a (co)inductive definition}
   1.111 -An inductive definition has the form
   1.112 -\begin{ttbox}
   1.113 -inductive
   1.114 -  domains    {\it domain declarations}
   1.115 -  intrs      {\it introduction rules}
   1.116 -  monos      {\it monotonicity theorems}
   1.117 -  con_defs   {\it constructor definitions}
   1.118 -  type_intrs {\it introduction rules for type-checking}
   1.119 -  type_elims {\it elimination rules for type-checking}
   1.120 -\end{ttbox}
   1.121 -A coinductive definition is identical, but starts with the keyword
   1.122 -{\tt coinductive}.  
   1.123 -
   1.124 -The {\tt monos}, {\tt con\_defs}, {\tt type\_intrs} and {\tt type\_elims}
   1.125 -sections are optional.  If present, each is specified as a string, which
   1.126 -must be a valid \textsc{ml} expression of type {\tt thm list}.  It is simply
   1.127 -inserted into the {\tt .thy.ML} file; if it is ill-formed, it will trigger
   1.128 -\textsc{ml} error messages.  You can then inspect the file on your directory.
   1.129 -
   1.130 -\begin{description}
   1.131 -\item[\it domain declarations] consist of one or more items of the form
   1.132 -  {\it string\/}~{\tt <=}~{\it string}, associating each recursive set with
   1.133 -  its domain.
   1.134 -
   1.135 -\item[\it introduction rules] specify one or more introduction rules in
   1.136 -  the form {\it ident\/}~{\it string}, where the identifier gives the name of
   1.137 -  the rule in the result structure.
   1.138 -
   1.139 -\item[\it monotonicity theorems] are required for each operator applied to
   1.140 -  a recursive set in the introduction rules.  There \defn{must} be a theorem
   1.141 -  of the form $A\sbs B\Imp M(A)\sbs M(B)$, for each premise $t\in M(R_i)$
   1.142 -  in an introduction rule!
   1.143 -
   1.144 -\item[\it constructor definitions] contain definitions of constants
   1.145 -  appearing in the introduction rules.  The (co)datatype package supplies
   1.146 -  the constructors' definitions here.  Most (co)inductive definitions omit
   1.147 -  this section; one exception is the primitive recursive functions example
   1.148 -  (\S\ref{primrec-sec}).
   1.149 -
   1.150 -\item[\it type\_intrs] consists of introduction rules for type-checking the
   1.151 -  definition, as discussed in~\S\ref{basic-sec}.  They are applied using
   1.152 -  depth-first search; you can trace the proof by setting
   1.153 -
   1.154 -  \verb|trace_DEPTH_FIRST := true|.
   1.155 -
   1.156 -\item[\it type\_elims] consists of elimination rules for type-checking the
   1.157 -  definition.  They are presumed to be safe and are applied as much as
   1.158 -  possible, prior to the {\tt type\_intrs} search.
   1.159 -\end{description}
   1.160 -
   1.161 -The package has a few notable restrictions:
   1.162 -\begin{itemize}
   1.163 -\item The theory must separately declare the recursive sets as
   1.164 -  constants.
   1.165 -
   1.166 -\item The names of the recursive sets must be identifiers, not infix
   1.167 -operators.  
   1.168 -
   1.169 -\item Side-conditions must not be conjunctions.  However, an introduction rule
   1.170 -may contain any number of side-conditions.
   1.171 -
   1.172 -\item Side-conditions of the form $x=t$, where the variable~$x$ does not
   1.173 -  occur in~$t$, will be substituted through the rule \verb|mutual_induct|.
   1.174 -\end{itemize}
   1.175 -
   1.176 -Isabelle/\textsc{hol} uses a simplified syntax for inductive definitions,
   1.177 -thanks to type-checking.  There are no \texttt{domains}, \texttt{type\_intrs}
   1.178 -or \texttt{type\_elims} parts.
   1.179 -
   1.180 -
   1.181 -\section{Datatype and codatatype definitions: users guide}
   1.182 -This section explains how to include (co)datatype declarations in a theory
   1.183 -file.  Please include {\tt Datatype} as a parent theory; this makes available
   1.184 -the definitions of $\univ$ and $\quniv$.
   1.185 -
   1.186 -
   1.187 -\subsection{The result structure}
   1.188 -The result structure extends that of (co)inductive definitions
   1.189 -(Figure~\ref{def-result-fig}) with several additional items:
   1.190 -\begin{ttbox}
   1.191 -val con_defs  : thm list
   1.192 -val case_eqns : thm list
   1.193 -val free_iffs : thm list
   1.194 -val free_SEs  : thm list
   1.195 -val mk_free   : string -> thm
   1.196 -\end{ttbox}
   1.197 -Most of these have been discussed in~\S\ref{data-sec}.  Here is a summary:
   1.198 -\begin{description}
   1.199 -\item[\tt con\_defs] is a list of definitions: the case operator followed by
   1.200 -the constructors.  This theorem list can be supplied to \verb|mk_cases|, for
   1.201 -example.
   1.202 -
   1.203 -\item[\tt case\_eqns] is a list of equations, stating that the case operator
   1.204 -inverts each constructor.
   1.205 -
   1.206 -\item[\tt free\_iffs] is a list of logical equivalences to perform freeness
   1.207 -reasoning by rewriting.  A typical application has the form
   1.208 -\begin{ttbox}
   1.209 -by (asm_simp_tac (ZF_ss addsimps free_iffs) 1);
   1.210 -\end{ttbox}
   1.211 -
   1.212 -\item[\tt free\_SEs] is a list of safe elimination rules to perform freeness
   1.213 -reasoning.  It can be supplied to \verb|eresolve_tac| or to the classical
   1.214 -reasoner:
   1.215 -\begin{ttbox} 
   1.216 -by (fast_tac (ZF_cs addSEs free_SEs) 1);
   1.217 -\end{ttbox}
   1.218 -
   1.219 -\item[\tt mk\_free] is a function to prove freeness properties, specified as
   1.220 -strings.  The theorems can be expressed in various forms, such as logical
   1.221 -equivalences or elimination rules.
   1.222 -\end{description}
   1.223 -
   1.224 -The result structure also inherits everything from the underlying
   1.225 -(co)inductive definition, such as the introduction rules, elimination rule,
   1.226 -and (co)induction rule.
   1.227 -
   1.228 -
   1.229 -\subsection{The syntax of a (co)datatype definition}
   1.230 -A datatype definition has the form
   1.231 -\begin{ttbox}
   1.232 -datatype <={\it domain}
   1.233 - {\it datatype declaration} and {\it datatype declaration} and \ldots
   1.234 -  monos      {\it monotonicity theorems}
   1.235 -  type_intrs {\it introduction rules for type-checking}
   1.236 -  type_elims {\it elimination rules for type-checking}
   1.237 -\end{ttbox}
   1.238 -A codatatype definition is identical save that it starts with the keyword {\tt
   1.239 -  codatatype}.
   1.240 -
   1.241 -The {\tt monos}, {\tt type\_intrs} and {\tt type\_elims} sections are
   1.242 -optional.  They are treated like their counterparts in a (co)inductive
   1.243 -definition, as described above.  The package supplements your type-checking
   1.244 -rules (if any) with additional ones that should cope with any
   1.245 -finitely-branching (co)datatype definition.
   1.246 -
   1.247 -\begin{description}
   1.248 -\item[\it domain] specifies a single domain to use for all the mutually
   1.249 -  recursive (co)datatypes.  If it (and the preceeding~{\tt <=}) are
   1.250 -  omitted, the package supplies a domain automatically.  Suppose the
   1.251 -  definition involves the set parameters $A_1$, \ldots, $A_k$.  Then
   1.252 -  $\univ(A_1\un\cdots\un A_k)$ is used for a datatype definition and
   1.253 -  $\quniv(A_1\un\cdots\un A_k)$ is used for a codatatype definition.
   1.254 -
   1.255 -  These choices should work for all finitely-branching (co)datatype
   1.256 -  definitions.  For examples of infinitely-branching datatypes, 
   1.257 -  see file {\tt ZF/ex/Brouwer.thy}.
   1.258 -
   1.259 -\item[\it datatype declaration] has the form
   1.260 -\begin{quote}
   1.261 - {\it string\/} {\tt =} {\it constructor} {\tt|} {\it constructor} {\tt|}
   1.262 - \ldots 
   1.263 -\end{quote}
   1.264 -The {\it string\/} is the datatype, say {\tt"list(A)"}.  Each
   1.265 -{\it constructor\/} has the form 
   1.266 -\begin{quote}
   1.267 - {\it name\/} {\tt(} {\it premise} {\tt,} {\it premise} {\tt,} \ldots {\tt)}
   1.268 - {\it mixfix\/}
   1.269 -\end{quote}
   1.270 -The {\it name\/} specifies a new constructor while the {\it premises\/} its
   1.271 -typing conditions.  The optional {\it mixfix\/} phrase may give
   1.272 -the constructor infix, for example.
   1.273 -
   1.274 -Mutually recursive {\it datatype declarations\/} are separated by the
   1.275 -keyword~{\tt and}.
   1.276 -\end{description}
   1.277 -
   1.278 -Isabelle/\textsc{hol}'s datatype definition package is (as of this writing)
   1.279 -entirely different from Isabelle/\textsc{zf}'s.  The syntax is different, and
   1.280 -instead of making an inductive definition it asserts axioms.
   1.281 -
   1.282 -\paragraph*{Note.}
   1.283 -In the definitions of the constructors, the right-hand sides may overlap.
   1.284 -For instance, the datatype of combinators has constructors defined by
   1.285 -\begin{eqnarray*}
   1.286 -  {\tt K} & \equiv & \Inl(\emptyset) \\
   1.287 -  {\tt S} & \equiv & \Inr(\Inl(\emptyset)) \\
   1.288 -  p{\tt\#}q & \equiv & \Inr(\Inl(\pair{p,q})) 
   1.289 -\end{eqnarray*}
   1.290 -Unlike in previous versions of Isabelle, \verb|fold_tac| now ensures that the
   1.291 -longest right-hand sides are folded first.
   1.292 -
   1.293 -\fi
   1.294  \end{document}