# HG changeset patch # User paulson # Date 926411530 -7200 # Node ID ccae8c659762c31b26ee5f3b701a9429d82583ff # Parent 5f810292c03053c209d65a4716a4781f8b6652bd changes for new manual.bib diff -r 5f810292c030 -r ccae8c659762 doc-src/Inductive/ind-defs.bbl --- 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} diff -r 5f810292c030 -r ccae8c659762 doc-src/Inductive/ind-defs.tex --- 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; : listn(A) |] ==> : listn(A)" + ConsI "[| a:A; :listn(A) |] ==> : 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 " : lleq(A)" - LCons "[| a:A; : lleq(A) |] ==> : lleq(A)" + LCons "[| a:A; :lleq(A) |] ==> : 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