author | paulson |

Wed Jan 13 16:38:52 1999 +0100 (1999-01-13) | |

changeset 6124 | 3aa7926f039a |

parent 6123 | 4ba5066d01fc |

child 6125 | 59507030d953 |

deleted the appendices because documentation exists in the HOL and ZF manuals

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}