--- a/doc-src/Inductive/ind-defs.bbl Mon May 10 17:45:16 1999 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,214 +0,0 @@
-\begin{thebibliography}{10}
-
-\bibitem{abramsky90}
-Abramsky, S.,
-\newblock The lazy lambda calculus,
-\newblock In {\em Research Topics in Functional Programming}, D.~A. Turner, Ed.
- Addison-Wesley, 1977, pp.~65--116
-
-\bibitem{aczel77}
-Aczel, P.,
-\newblock An introduction to inductive definitions,
-\newblock In {\em Handbook of Mathematical Logic}, J.~Barwise, Ed.
- North-Holland, 1977, pp.~739--782
-
-\bibitem{aczel88}
-Aczel, P.,
-\newblock {\em Non-Well-Founded Sets},
-\newblock CSLI, 1988
-
-\bibitem{bm79}
-Boyer, R.~S., Moore, J.~S.,
-\newblock {\em A Computational Logic},
-\newblock Academic Press, 1979
-
-\bibitem{camilleri92}
-Camilleri, J., Melham, T.~F.,
-\newblock Reasoning with inductively defined relations in the {HOL} theorem
- prover,
-\newblock Tech. Rep. 265, Comp. Lab., Univ. Cambridge, Aug. 1992
-
-\bibitem{davey&priestley}
-Davey, B.~A., Priestley, H.~A.,
-\newblock {\em Introduction to Lattices and Order},
-\newblock Cambridge Univ. Press, 1990
-
-\bibitem{dybjer91}
-Dybjer, P.,
-\newblock Inductive sets and families in {Martin-L\"of's} type theory and their
- set-theoretic semantics,
-\newblock In {\em Logical Frameworks}, G.~Huet G.~Plotkin, Eds. Cambridge Univ.
- Press, 1991, pp.~280--306
-
-\bibitem{types94}
-Dybjer, P., Nordstr{\"om}, B., Smith, J., Eds.,
-\newblock {\em Types for Proofs and Programs: International Workshop {TYPES
- '94}},
-\newblock LNCS 996. Springer, 1995
-
-\bibitem{IMPS}
-Farmer, W.~M., Guttman, J.~D., Thayer, F.~J.,
-\newblock {IMPS}: An interactive mathematical proof system,
-\newblock {\em J. Auto. Reas. {\bf 11}}, 2 (1993), 213--248
-
-\bibitem{frost95}
-Frost, J.,
-\newblock A case study of co-induction in {Isabelle},
-\newblock Tech. Rep. 359, Comp. Lab., Univ. Cambridge, Feb. 1995
-
-\bibitem{gimenez-codifying}
-Gim{\'e}nez, E.,
-\newblock Codifying guarded definitions with recursive schemes,
-\newblock In Dybjer et~al. \cite{types94}, pp.~39--59
-
-\bibitem{gunter-trees}
-Gunter, E.~L.,
-\newblock A broader class of trees for recursive type definitions for {HOL},
-\newblock In {\em Higher Order Logic Theorem Proving and Its Applications: HUG
- '93\/} (Published 1994), J.~Joyce C.~Seger, Eds., LNCS 780, Springer,
- pp.~141--154
-
-\bibitem{hennessy90}
-Hennessy, M.,
-\newblock {\em The Semantics of Programming Languages: An Elementary
- Introduction Using Structural Operational Semantics},
-\newblock Wiley, 1990
-
-\bibitem{huet88}
-Huet, G.,
-\newblock Induction principles formalized in the {Calculus of Constructions},
-\newblock In {\em Programming of Future Generation Computers\/} (1988),
- K.~Fuchi M.~Nivat, Eds., Elsevier, pp.~205--216
-
-\bibitem{melham89}
-Melham, T.~F.,
-\newblock Automating recursive type definitions in higher order logic,
-\newblock In {\em Current Trends in Hardware Verification and Automated Theorem
- Proving}, G.~Birtwistle P.~A. Subrahmanyam, Eds. Springer, 1989, pp.~341--386
-
-\bibitem{milner-ind}
-Milner, R.,
-\newblock How to derive inductions in {LCF},
-\newblock note, Dept. Comp. Sci., Univ. Edinburgh, 1980
-
-\bibitem{milner89}
-Milner, R.,
-\newblock {\em Communication and Concurrency},
-\newblock Prentice-Hall, 1989
-
-\bibitem{milner-coind}
-Milner, R., Tofte, M.,
-\newblock Co-induction in relational semantics,
-\newblock {\em Theoretical Comput. Sci. {\bf 87}\/} (1991), 209--220
-
-\bibitem{monahan84}
-Monahan, B.~Q.,
-\newblock {\em Data Type Proofs using Edinburgh {LCF}},
-\newblock PhD thesis, University of Edinburgh, 1984
-
-\bibitem{nipkow-CR}
-Nipkow, T.,
-\newblock More {Church-Rosser} proofs (in {Isabelle/HOL}),
-\newblock In {\em Automated Deduction --- {CADE}-13 International Conference\/}
- (1996), M.~McRobbie J.~K. Slaney, Eds., LNAI 1104, Springer, pp.~733--747
-
-\bibitem{pvs-language}
-Owre, S., Shankar, N., Rushby, J.~M.,
-\newblock {\em The {PVS} specification language},
-\newblock Computer Science Laboratory, SRI International, Menlo Park, CA, Apr.
- 1993,
-\newblock Beta release
-
-\bibitem{paulin-tlca}
-Paulin-Mohring, C.,
-\newblock Inductive definitions in the system {Coq}: Rules and properties,
-\newblock In {\em Typed Lambda Calculi and Applications\/} (1993), M.~Bezem
- J.~Groote, Eds., LNCS 664, Springer, pp.~328--345
-
-\bibitem{paulson87}
-Paulson, L.~C.,
-\newblock {\em Logic and Computation: Interactive proof with Cambridge LCF},
-\newblock Cambridge Univ. Press, 1987
-
-\bibitem{paulson-set-I}
-Paulson, L.~C.,
-\newblock Set theory for verification: {I}. {From} foundations to functions,
-\newblock {\em J. Auto. Reas. {\bf 11}}, 3 (1993), 353--389
-
-\bibitem{paulson-isa-book}
-Paulson, L.~C.,
-\newblock {\em Isabelle: A Generic Theorem Prover},
-\newblock Springer, 1994,
-\newblock LNCS 828
-
-\bibitem{paulson-final}
-Paulson, L.~C.,
-\newblock A concrete final coalgebra theorem for {ZF} set theory,
-\newblock In Dybjer et~al. \cite{types94}, pp.~120--139
-
-\bibitem{paulson-set-II}
-Paulson, L.~C.,
-\newblock Set theory for verification: {II}. {Induction} and recursion,
-\newblock {\em J. Auto. Reas. {\bf 15}}, 2 (1995), 167--215
-
-\bibitem{paulson-coind}
-Paulson, L.~C.,
-\newblock Mechanizing coinduction and corecursion in higher-order logic,
-\newblock {\em J. Logic and Comput. {\bf 7}}, 2 (Mar. 1997), 175--204
-
-\bibitem{paulson-markt}
-Paulson, L.~C.,
-\newblock Tool support for logics of programs,
-\newblock In {\em Mathematical Methods in Program Development: Summer School
- Marktoberdorf 1996}, M.~Broy, Ed., NATO ASI Series F. Springer, Published
- 1997, pp.~461--498
-
-\bibitem{paulson-gr}
-Paulson, L.~C., Gr\c{a}bczewski, K.,
-\newblock Mechanizing set theory: Cardinal arithmetic and the axiom of choice,
-\newblock {\em J. Auto. Reas. {\bf 17}}, 3 (Dec. 1996), 291--323
-
-\bibitem{pitts94}
-Pitts, A.~M.,
-\newblock A co-induction principle for recursively defined domains,
-\newblock {\em Theoretical Comput. Sci. {\bf 124}\/} (1994), 195--219
-
-\bibitem{rasmussen95}
-Rasmussen, O.,
-\newblock The {Church-Rosser} theorem in {Isabelle}: A proof porting
- experiment,
-\newblock Tech. Rep. 364, Computer Laboratory, University of Cambridge, May
- 1995
-
-\bibitem{saaltink-fme}
-Saaltink, M., Kromodimoeljo, S., Pase, B., Craigen, D., Meisels, I.,
-\newblock An {EVES} data abstraction example,
-\newblock In {\em FME '93: Industrial-Strength Formal Methods\/} (1993),
- J.~C.~P. Woodcock P.~G. Larsen, Eds., LNCS 670, Springer, pp.~578--596
-
-\bibitem{slind-tfl}
-Slind, K.,
-\newblock Function definition in higher-order logic,
-\newblock In {\em Theorem Proving in Higher Order Logics: {TPHOLs} '96\/}
- (1996), J.~von Wright, J.~Grundy, J.~Harrison, Eds., LNCS 1125
-
-\bibitem{szasz93}
-Szasz, N.,
-\newblock A machine checked proof that {Ackermann's} function is not primitive
- recursive,
-\newblock In {\em Logical Environments}, G.~Huet G.~Plotkin, Eds. Cambridge
- Univ. Press, 1993, pp.~317--338
-
-\bibitem{voelker95}
-V\"olker, N.,
-\newblock On the representation of datatypes in {Isabelle/HOL},
-\newblock In {\em Proceedings of the First Isabelle Users Workshop\/} (Sept.
- 1995), L.~C. Paulson, Ed., Technical Report 379, Comp. Lab., Univ. Cambridge,
- pp.~206--218
-
-\bibitem{winskel93}
-Winskel, G.,
-\newblock {\em The Formal Semantics of Programming Languages},
-\newblock MIT Press, 1993
-
-\end{thebibliography}
--- 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