1.1 --- a/doc-src/Inductive/ind-defs.tex Mon May 10 17:45:16 1999 +0200
1.2 +++ b/doc-src/Inductive/ind-defs.tex Tue May 11 10:32:10 1999 +0200
1.3 @@ -582,7 +582,7 @@
1.4 domains "listn(A)" <= "nat*list(A)"
1.5 intrs
1.6 NilI "<0,Nil>: listn(A)"
1.7 - ConsI "[| a: A; <n,l>: listn(A) |] ==> <succ(n), Cons(a,l)>: listn(A)"
1.8 + ConsI "[| a:A; <n,l>:listn(A) |] ==> <succ(n), Cons(a,l)>: listn(A)"
1.9 type_intrs "nat_typechecks @ list.intrs"
1.10 end
1.11 \end{ttbox}
1.12 @@ -696,15 +696,17 @@
1.13 \]
1.14 To make this coinductive definition, the theory file includes (after the
1.15 declaration of $\llist(A)$) the following lines:
1.16 +\bgroup\leftmargini=\parindent
1.17 \begin{ttbox}
1.18 consts lleq :: i=>i
1.19 coinductive
1.20 domains "lleq(A)" <= "llist(A) * llist(A)"
1.21 intrs
1.22 LNil "<LNil,LNil> : lleq(A)"
1.23 - LCons "[| a:A; <l,l'>: lleq(A) |] ==> <LCons(a,l),LCons(a,l')>: lleq(A)"
1.24 + LCons "[| a:A; <l,l'>:lleq(A) |] ==> <LCons(a,l),LCons(a,l')>: lleq(A)"
1.25 type_intrs "llist.intrs"
1.26 \end{ttbox}
1.27 +\egroup
1.28 The domain of $\lleq(A)$ is $\llist(A)\times\llist(A)$. The type-checking
1.29 rules include the introduction rules for $\llist(A)$, whose
1.30 declaration is discussed below (\S\ref{lists-sec}).
1.31 @@ -830,27 +832,29 @@
1.32
1.33 \begin{figure}
1.34 \begin{ttbox}
1.35 -Primrec = List +
1.36 -consts
1.37 - primrec :: i
1.38 - SC :: i
1.39 - \(\vdots\)
1.40 +Primrec_defs = Main +
1.41 +consts SC :: i
1.42 + \(\vdots\)
1.43 defs
1.44 - SC_def "SC == lam l:list(nat).list_case(0, \%x xs.succ(x), l)"
1.45 - \(\vdots\)
1.46 + SC_def "SC == lam l:list(nat).list_case(0, \%x xs.succ(x), l)"
1.47 + \(\vdots\)
1.48 +end
1.49 +
1.50 +Primrec = Primrec_defs +
1.51 +consts prim_rec :: i
1.52 inductive
1.53 - domains "primrec" <= "list(nat)->nat"
1.54 - intrs
1.55 - SC "SC : primrec"
1.56 - CONST "k: nat ==> CONST(k) : primrec"
1.57 - PROJ "i: nat ==> PROJ(i) : primrec"
1.58 - COMP "[| g: primrec; fs: list(primrec) |] ==> COMP(g,fs): primrec"
1.59 - PREC "[| f: primrec; g: primrec |] ==> PREC(f,g): primrec"
1.60 - monos list_mono
1.61 - con_defs SC_def, CONST_def, PROJ_def, COMP_def, PREC_def
1.62 - type_intrs "nat_typechecks @ list.intrs @
1.63 - [lam_type, list_case_type, drop_type, map_type,
1.64 - apply_type, rec_type]"
1.65 + domains "primrec" <= "list(nat)->nat"
1.66 + intrs
1.67 + SC "SC : primrec"
1.68 + CONST "k: nat ==> CONST(k) : primrec"
1.69 + PROJ "i: nat ==> PROJ(i) : primrec"
1.70 + COMP "[| g: primrec; fs: list(primrec) |] ==> COMP(g,fs): primrec"
1.71 + PREC "[| f: primrec; g: primrec |] ==> PREC(f,g): primrec"
1.72 + monos list_mono
1.73 + con_defs SC_def, CONST_def, PROJ_def, COMP_def, PREC_def
1.74 + type_intrs "nat_typechecks @ list.intrs @
1.75 + [lam_type, list_case_type, drop_type, map_type,
1.76 + apply_type, rec_type]"
1.77 end
1.78 \end{ttbox}
1.79 \hrule
1.80 @@ -937,7 +941,7 @@
1.81 $\QInl(a)$ and $\QInr(b)$ for $a$, $b\in\quniv(A)$. In a typical codatatype
1.82 definition with set parameters $A_1$, \ldots, $A_k$, a suitable domain is
1.83 $\quniv(A_1\un\cdots\un A_k)$. Details are published
1.84 -elsewhere~\cite{paulson-final}.
1.85 +elsewhere~\cite{paulson-mscs}.
1.86
1.87 \subsection{The case analysis operator}
1.88 The (co)datatype package automatically defines a case analysis operator,
1.89 @@ -1000,7 +1004,7 @@
1.90 \ifshort
1.91 Now $\lst(A)$ is a datatype and enjoys the usual induction rule.
1.92 \else
1.93 -Since $\lst(A)$ is a datatype, it enjoys a structural induction rule, {\tt
1.94 +Since $\lst(A)$ is a datatype, it has a structural induction rule, {\tt
1.95 list.induct}:
1.96 \[ \infer{P(x)}{x\in\lst(A) & P(\Nil)
1.97 & \infer*{P(\Cons(a,l))}{[a\in A & l\in\lst(A) & P(l)]_{a,l}} }
1.98 @@ -1079,7 +1083,7 @@
1.99 \right]_{t,f}} }
1.100 \]
1.101 This rule establishes a single predicate for $\TF(A)$, the union of the
1.102 -recursive sets. Although such reasoning is sometimes useful
1.103 +recursive sets. Although such reasoning can be useful
1.104 \cite[\S4.5]{paulson-set-II}, a proper mutual induction rule should establish
1.105 separate predicates for $\tree(A)$ and $\forest(A)$. The package calls this
1.106 rule {\tt tree\_forest.mutual\_induct}. Observe the usage of $P$ and $Q$ in
1.107 @@ -1292,7 +1296,7 @@
1.108 Isabelle/\textsc{zf} instead uses a variant notion of ordered pairing, which
1.109 can be generalized to a variant notion of function. Elsewhere I have
1.110 proved that this simple approach works (yielding final coalgebras) for a broad
1.111 -class of definitions~\cite{paulson-final}.
1.112 +class of definitions~\cite{paulson-mscs}.
1.113
1.114 Several large studies make heavy use of inductive definitions. L\"otzbeyer
1.115 and Sandner have formalized two chapters of a semantics book~\cite{winskel93},
1.116 @@ -1318,15 +1322,12 @@
1.117 The approach is not restricted to set theory. It should be suitable for any
1.118 logic that has some notion of set and the Knaster-Tarski theorem. I have
1.119 ported the (co)inductive definition package from Isabelle/\textsc{zf} to
1.120 -Isabelle/\textsc{hol} (higher-order logic). V\"olker~\cite{voelker95}
1.121 -is investigating how to port the (co)datatype package. \textsc{hol}
1.122 -represents sets by unary predicates; defining the corresponding types may
1.123 -cause complications.
1.124 +Isabelle/\textsc{hol} (higher-order logic).
1.125
1.126
1.127 \begin{footnotesize}
1.128 \bibliographystyle{springer}
1.129 -\bibliography{string-abbrv,atp,theory,funprog,isabelle,crossref}
1.130 +\bibliography{../manual}
1.131 \end{footnotesize}
1.132 %%%%%\doendnotes
1.133