doc-src/Inductive/ind-defs.tex
 changeset 6631 ccae8c659762 parent 6141 a6922171b396 child 6637 57abed64dc14
--- a/doc-src/Inductive/ind-defs.tex	Mon May 10 17:45:16 1999 +0200
+++ b/doc-src/Inductive/ind-defs.tex	Tue May 11 10:32:10 1999 +0200
@@ -582,7 +582,7 @@
domains   "listn(A)" <= "nat*list(A)"
intrs
NilI  "<0,Nil>: listn(A)"
-    ConsI "[| a: A;  <n,l>: listn(A) |] ==> <succ(n), Cons(a,l)>: listn(A)"
+    ConsI "[| a:A; <n,l>:listn(A) |] ==> <succ(n), Cons(a,l)>: listn(A)"
type_intrs "nat_typechecks @ list.intrs"
end
\end{ttbox}
@@ -696,15 +696,17 @@
\]
To make this coinductive definition, the theory file includes (after the
declaration of $\llist(A)$) the following lines:
+\bgroup\leftmargini=\parindent
\begin{ttbox}
consts    lleq :: i=>i
coinductive
domains "lleq(A)" <= "llist(A) * llist(A)"
intrs
LNil  "<LNil,LNil> : lleq(A)"
-    LCons "[| a:A; <l,l'>: lleq(A) |] ==> <LCons(a,l),LCons(a,l')>: lleq(A)"
+    LCons "[| a:A; <l,l'>:lleq(A) |] ==> <LCons(a,l),LCons(a,l')>: lleq(A)"
type_intrs  "llist.intrs"
\end{ttbox}
+\egroup
The domain of $\lleq(A)$ is $\llist(A)\times\llist(A)$.  The type-checking
rules include the introduction rules for $\llist(A)$, whose
declaration is discussed below (\S\ref{lists-sec}).
@@ -830,27 +832,29 @@

\begin{figure}
\begin{ttbox}
-Primrec = List +
-consts
-  primrec :: i
-  SC      :: i
-  $$\vdots$$
+Primrec_defs = Main +
+consts SC :: i
+ $$\vdots$$
defs
-  SC_def    "SC == lam l:list(nat).list_case(0, \%x xs.succ(x), l)"
-  $$\vdots$$
+ SC_def    "SC == lam l:list(nat).list_case(0, \%x xs.succ(x), l)"
+ $$\vdots$$
+end
+
+Primrec = Primrec_defs +
+consts prim_rec :: i
inductive
-  domains "primrec" <= "list(nat)->nat"
-  intrs
-    SC       "SC : primrec"
-    CONST    "k: nat ==> CONST(k) : primrec"
-    PROJ     "i: nat ==> PROJ(i) : primrec"
-    COMP     "[| g: primrec; fs: list(primrec) |] ==> COMP(g,fs): primrec"
-    PREC     "[| f: primrec; g: primrec |] ==> PREC(f,g): primrec"
-  monos       list_mono
-  con_defs    SC_def, CONST_def, PROJ_def, COMP_def, PREC_def
-  type_intrs "nat_typechecks @ list.intrs @
-              [lam_type, list_case_type, drop_type, map_type,
-               apply_type, rec_type]"
+ domains "primrec" <= "list(nat)->nat"
+ intrs
+   SC     "SC : primrec"
+   CONST  "k: nat ==> CONST(k) : primrec"
+   PROJ   "i: nat ==> PROJ(i) : primrec"
+   COMP   "[| g: primrec; fs: list(primrec) |] ==> COMP(g,fs): primrec"
+   PREC   "[| f: primrec; g: primrec |] ==> PREC(f,g): primrec"
+ monos       list_mono
+ con_defs    SC_def, CONST_def, PROJ_def, COMP_def, PREC_def
+ type_intrs "nat_typechecks @ list.intrs @
+             [lam_type, list_case_type, drop_type, map_type,
+              apply_type, rec_type]"
end
\end{ttbox}
\hrule
@@ -937,7 +941,7 @@
$\QInl(a)$ and $\QInr(b)$ for $a$, $b\in\quniv(A)$.  In a typical codatatype
definition with set parameters $A_1$, \ldots, $A_k$, a suitable domain is
$\quniv(A_1\un\cdots\un A_k)$.  Details are published
-elsewhere~\cite{paulson-final}.
+elsewhere~\cite{paulson-mscs}.

\subsection{The case analysis operator}
The (co)datatype package automatically defines a case analysis operator,
@@ -1000,7 +1004,7 @@
\ifshort
Now $\lst(A)$ is a datatype and enjoys the usual induction rule.
\else
-Since $\lst(A)$ is a datatype, it enjoys a structural induction rule, {\tt
+Since $\lst(A)$ is a datatype, it has a structural induction rule, {\tt
list.induct}:
$\infer{P(x)}{x\in\lst(A) & P(\Nil) & \infer*{P(\Cons(a,l))}{[a\in A & l\in\lst(A) & P(l)]_{a,l}} } @@ -1079,7 +1083,7 @@ \right]_{t,f}} }$
This rule establishes a single predicate for $\TF(A)$, the union of the
-recursive sets.  Although such reasoning is sometimes useful
+recursive sets.  Although such reasoning can be useful
\cite[\S4.5]{paulson-set-II}, a proper mutual induction rule should establish
separate predicates for $\tree(A)$ and $\forest(A)$.  The package calls this
rule {\tt tree\_forest.mutual\_induct}.  Observe the usage of $P$ and $Q$ in
@@ -1292,7 +1296,7 @@
Isabelle/\textsc{zf} instead uses a variant notion of ordered pairing, which
can be generalized to a variant notion of function.  Elsewhere I have
proved that this simple approach works (yielding final coalgebras) for a broad
-class of definitions~\cite{paulson-final}.
+class of definitions~\cite{paulson-mscs}.

Several large studies make heavy use of inductive definitions.  L\"otzbeyer
and Sandner have formalized two chapters of a semantics book~\cite{winskel93},
@@ -1318,15 +1322,12 @@
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/\textsc{zf} to
-Isabelle/\textsc{hol} (higher-order logic).  V\"olker~\cite{voelker95}
-is investigating how to port the (co)datatype package.  \textsc{hol}
-represents sets by unary predicates; defining the corresponding types may
-cause complications.
+Isabelle/\textsc{hol} (higher-order logic).

\begin{footnotesize}
\bibliographystyle{springer}
-\bibliography{string-abbrv,atp,theory,funprog,isabelle,crossref}
+\bibliography{../manual}
\end{footnotesize}
%%%%%\doendnotes