1.1 --- a/doc-src/Inductive/ind-defs.bbl Mon May 10 17:45:16 1999 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,214 +0,0 @@
1.4 -\begin{thebibliography}{10}
1.5 -
1.6 -\bibitem{abramsky90}
1.7 -Abramsky, S.,
1.8 -\newblock The lazy lambda calculus,
1.9 -\newblock In {\em Research Topics in Functional Programming}, D.~A. Turner, Ed.
1.10 - Addison-Wesley, 1977, pp.~65--116
1.11 -
1.12 -\bibitem{aczel77}
1.13 -Aczel, P.,
1.14 -\newblock An introduction to inductive definitions,
1.15 -\newblock In {\em Handbook of Mathematical Logic}, J.~Barwise, Ed.
1.16 - North-Holland, 1977, pp.~739--782
1.17 -
1.18 -\bibitem{aczel88}
1.19 -Aczel, P.,
1.20 -\newblock {\em Non-Well-Founded Sets},
1.21 -\newblock CSLI, 1988
1.22 -
1.23 -\bibitem{bm79}
1.24 -Boyer, R.~S., Moore, J.~S.,
1.25 -\newblock {\em A Computational Logic},
1.26 -\newblock Academic Press, 1979
1.27 -
1.28 -\bibitem{camilleri92}
1.29 -Camilleri, J., Melham, T.~F.,
1.30 -\newblock Reasoning with inductively defined relations in the {HOL} theorem
1.31 - prover,
1.32 -\newblock Tech. Rep. 265, Comp. Lab., Univ. Cambridge, Aug. 1992
1.33 -
1.34 -\bibitem{davey&priestley}
1.35 -Davey, B.~A., Priestley, H.~A.,
1.36 -\newblock {\em Introduction to Lattices and Order},
1.37 -\newblock Cambridge Univ. Press, 1990
1.38 -
1.39 -\bibitem{dybjer91}
1.40 -Dybjer, P.,
1.41 -\newblock Inductive sets and families in {Martin-L\"of's} type theory and their
1.42 - set-theoretic semantics,
1.43 -\newblock In {\em Logical Frameworks}, G.~Huet G.~Plotkin, Eds. Cambridge Univ.
1.44 - Press, 1991, pp.~280--306
1.45 -
1.46 -\bibitem{types94}
1.47 -Dybjer, P., Nordstr{\"om}, B., Smith, J., Eds.,
1.48 -\newblock {\em Types for Proofs and Programs: International Workshop {TYPES
1.49 - '94}},
1.50 -\newblock LNCS 996. Springer, 1995
1.51 -
1.52 -\bibitem{IMPS}
1.53 -Farmer, W.~M., Guttman, J.~D., Thayer, F.~J.,
1.54 -\newblock {IMPS}: An interactive mathematical proof system,
1.55 -\newblock {\em J. Auto. Reas. {\bf 11}}, 2 (1993), 213--248
1.56 -
1.57 -\bibitem{frost95}
1.58 -Frost, J.,
1.59 -\newblock A case study of co-induction in {Isabelle},
1.60 -\newblock Tech. Rep. 359, Comp. Lab., Univ. Cambridge, Feb. 1995
1.61 -
1.62 -\bibitem{gimenez-codifying}
1.63 -Gim{\'e}nez, E.,
1.64 -\newblock Codifying guarded definitions with recursive schemes,
1.65 -\newblock In Dybjer et~al. \cite{types94}, pp.~39--59
1.66 -
1.67 -\bibitem{gunter-trees}
1.68 -Gunter, E.~L.,
1.69 -\newblock A broader class of trees for recursive type definitions for {HOL},
1.70 -\newblock In {\em Higher Order Logic Theorem Proving and Its Applications: HUG
1.71 - '93\/} (Published 1994), J.~Joyce C.~Seger, Eds., LNCS 780, Springer,
1.72 - pp.~141--154
1.73 -
1.74 -\bibitem{hennessy90}
1.75 -Hennessy, M.,
1.76 -\newblock {\em The Semantics of Programming Languages: An Elementary
1.77 - Introduction Using Structural Operational Semantics},
1.78 -\newblock Wiley, 1990
1.79 -
1.80 -\bibitem{huet88}
1.81 -Huet, G.,
1.82 -\newblock Induction principles formalized in the {Calculus of Constructions},
1.83 -\newblock In {\em Programming of Future Generation Computers\/} (1988),
1.84 - K.~Fuchi M.~Nivat, Eds., Elsevier, pp.~205--216
1.85 -
1.86 -\bibitem{melham89}
1.87 -Melham, T.~F.,
1.88 -\newblock Automating recursive type definitions in higher order logic,
1.89 -\newblock In {\em Current Trends in Hardware Verification and Automated Theorem
1.90 - Proving}, G.~Birtwistle P.~A. Subrahmanyam, Eds. Springer, 1989, pp.~341--386
1.91 -
1.92 -\bibitem{milner-ind}
1.93 -Milner, R.,
1.94 -\newblock How to derive inductions in {LCF},
1.95 -\newblock note, Dept. Comp. Sci., Univ. Edinburgh, 1980
1.96 -
1.97 -\bibitem{milner89}
1.98 -Milner, R.,
1.99 -\newblock {\em Communication and Concurrency},
1.100 -\newblock Prentice-Hall, 1989
1.101 -
1.102 -\bibitem{milner-coind}
1.103 -Milner, R., Tofte, M.,
1.104 -\newblock Co-induction in relational semantics,
1.105 -\newblock {\em Theoretical Comput. Sci. {\bf 87}\/} (1991), 209--220
1.106 -
1.107 -\bibitem{monahan84}
1.108 -Monahan, B.~Q.,
1.109 -\newblock {\em Data Type Proofs using Edinburgh {LCF}},
1.110 -\newblock PhD thesis, University of Edinburgh, 1984
1.111 -
1.112 -\bibitem{nipkow-CR}
1.113 -Nipkow, T.,
1.114 -\newblock More {Church-Rosser} proofs (in {Isabelle/HOL}),
1.115 -\newblock In {\em Automated Deduction --- {CADE}-13 International Conference\/}
1.116 - (1996), M.~McRobbie J.~K. Slaney, Eds., LNAI 1104, Springer, pp.~733--747
1.117 -
1.118 -\bibitem{pvs-language}
1.119 -Owre, S., Shankar, N., Rushby, J.~M.,
1.120 -\newblock {\em The {PVS} specification language},
1.121 -\newblock Computer Science Laboratory, SRI International, Menlo Park, CA, Apr.
1.122 - 1993,
1.123 -\newblock Beta release
1.124 -
1.125 -\bibitem{paulin-tlca}
1.126 -Paulin-Mohring, C.,
1.127 -\newblock Inductive definitions in the system {Coq}: Rules and properties,
1.128 -\newblock In {\em Typed Lambda Calculi and Applications\/} (1993), M.~Bezem
1.129 - J.~Groote, Eds., LNCS 664, Springer, pp.~328--345
1.130 -
1.131 -\bibitem{paulson87}
1.132 -Paulson, L.~C.,
1.133 -\newblock {\em Logic and Computation: Interactive proof with Cambridge LCF},
1.134 -\newblock Cambridge Univ. Press, 1987
1.135 -
1.136 -\bibitem{paulson-set-I}
1.137 -Paulson, L.~C.,
1.138 -\newblock Set theory for verification: {I}. {From} foundations to functions,
1.139 -\newblock {\em J. Auto. Reas. {\bf 11}}, 3 (1993), 353--389
1.140 -
1.141 -\bibitem{paulson-isa-book}
1.142 -Paulson, L.~C.,
1.143 -\newblock {\em Isabelle: A Generic Theorem Prover},
1.144 -\newblock Springer, 1994,
1.145 -\newblock LNCS 828
1.146 -
1.147 -\bibitem{paulson-final}
1.148 -Paulson, L.~C.,
1.149 -\newblock A concrete final coalgebra theorem for {ZF} set theory,
1.150 -\newblock In Dybjer et~al. \cite{types94}, pp.~120--139
1.151 -
1.152 -\bibitem{paulson-set-II}
1.153 -Paulson, L.~C.,
1.154 -\newblock Set theory for verification: {II}. {Induction} and recursion,
1.155 -\newblock {\em J. Auto. Reas. {\bf 15}}, 2 (1995), 167--215
1.156 -
1.157 -\bibitem{paulson-coind}
1.158 -Paulson, L.~C.,
1.159 -\newblock Mechanizing coinduction and corecursion in higher-order logic,
1.160 -\newblock {\em J. Logic and Comput. {\bf 7}}, 2 (Mar. 1997), 175--204
1.161 -
1.162 -\bibitem{paulson-markt}
1.163 -Paulson, L.~C.,
1.164 -\newblock Tool support for logics of programs,
1.165 -\newblock In {\em Mathematical Methods in Program Development: Summer School
1.166 - Marktoberdorf 1996}, M.~Broy, Ed., NATO ASI Series F. Springer, Published
1.167 - 1997, pp.~461--498
1.168 -
1.169 -\bibitem{paulson-gr}
1.170 -Paulson, L.~C., Gr\c{a}bczewski, K.,
1.171 -\newblock Mechanizing set theory: Cardinal arithmetic and the axiom of choice,
1.172 -\newblock {\em J. Auto. Reas. {\bf 17}}, 3 (Dec. 1996), 291--323
1.173 -
1.174 -\bibitem{pitts94}
1.175 -Pitts, A.~M.,
1.176 -\newblock A co-induction principle for recursively defined domains,
1.177 -\newblock {\em Theoretical Comput. Sci. {\bf 124}\/} (1994), 195--219
1.178 -
1.179 -\bibitem{rasmussen95}
1.180 -Rasmussen, O.,
1.181 -\newblock The {Church-Rosser} theorem in {Isabelle}: A proof porting
1.182 - experiment,
1.183 -\newblock Tech. Rep. 364, Computer Laboratory, University of Cambridge, May
1.184 - 1995
1.185 -
1.186 -\bibitem{saaltink-fme}
1.187 -Saaltink, M., Kromodimoeljo, S., Pase, B., Craigen, D., Meisels, I.,
1.188 -\newblock An {EVES} data abstraction example,
1.189 -\newblock In {\em FME '93: Industrial-Strength Formal Methods\/} (1993),
1.190 - J.~C.~P. Woodcock P.~G. Larsen, Eds., LNCS 670, Springer, pp.~578--596
1.191 -
1.192 -\bibitem{slind-tfl}
1.193 -Slind, K.,
1.194 -\newblock Function definition in higher-order logic,
1.195 -\newblock In {\em Theorem Proving in Higher Order Logics: {TPHOLs} '96\/}
1.196 - (1996), J.~von Wright, J.~Grundy, J.~Harrison, Eds., LNCS 1125
1.197 -
1.198 -\bibitem{szasz93}
1.199 -Szasz, N.,
1.200 -\newblock A machine checked proof that {Ackermann's} function is not primitive
1.201 - recursive,
1.202 -\newblock In {\em Logical Environments}, G.~Huet G.~Plotkin, Eds. Cambridge
1.203 - Univ. Press, 1993, pp.~317--338
1.204 -
1.205 -\bibitem{voelker95}
1.206 -V\"olker, N.,
1.207 -\newblock On the representation of datatypes in {Isabelle/HOL},
1.208 -\newblock In {\em Proceedings of the First Isabelle Users Workshop\/} (Sept.
1.209 - 1995), L.~C. Paulson, Ed., Technical Report 379, Comp. Lab., Univ. Cambridge,
1.210 - pp.~206--218
1.211 -
1.212 -\bibitem{winskel93}
1.213 -Winskel, G.,
1.214 -\newblock {\em The Formal Semantics of Programming Languages},
1.215 -\newblock MIT Press, 1993
1.216 -
1.217 -\end{thebibliography}
2.1 --- a/doc-src/Inductive/ind-defs.tex Mon May 10 17:45:16 1999 +0200
2.2 +++ b/doc-src/Inductive/ind-defs.tex Tue May 11 10:32:10 1999 +0200
2.3 @@ -582,7 +582,7 @@
2.4 domains "listn(A)" <= "nat*list(A)"
2.5 intrs
2.6 NilI "<0,Nil>: listn(A)"
2.7 - ConsI "[| a: A; <n,l>: listn(A) |] ==> <succ(n), Cons(a,l)>: listn(A)"
2.8 + ConsI "[| a:A; <n,l>:listn(A) |] ==> <succ(n), Cons(a,l)>: listn(A)"
2.9 type_intrs "nat_typechecks @ list.intrs"
2.10 end
2.11 \end{ttbox}
2.12 @@ -696,15 +696,17 @@
2.13 \]
2.14 To make this coinductive definition, the theory file includes (after the
2.15 declaration of $\llist(A)$) the following lines:
2.16 +\bgroup\leftmargini=\parindent
2.17 \begin{ttbox}
2.18 consts lleq :: i=>i
2.19 coinductive
2.20 domains "lleq(A)" <= "llist(A) * llist(A)"
2.21 intrs
2.22 LNil "<LNil,LNil> : lleq(A)"
2.23 - LCons "[| a:A; <l,l'>: lleq(A) |] ==> <LCons(a,l),LCons(a,l')>: lleq(A)"
2.24 + LCons "[| a:A; <l,l'>:lleq(A) |] ==> <LCons(a,l),LCons(a,l')>: lleq(A)"
2.25 type_intrs "llist.intrs"
2.26 \end{ttbox}
2.27 +\egroup
2.28 The domain of $\lleq(A)$ is $\llist(A)\times\llist(A)$. The type-checking
2.29 rules include the introduction rules for $\llist(A)$, whose
2.30 declaration is discussed below (\S\ref{lists-sec}).
2.31 @@ -830,27 +832,29 @@
2.32
2.33 \begin{figure}
2.34 \begin{ttbox}
2.35 -Primrec = List +
2.36 -consts
2.37 - primrec :: i
2.38 - SC :: i
2.39 - \(\vdots\)
2.40 +Primrec_defs = Main +
2.41 +consts SC :: i
2.42 + \(\vdots\)
2.43 defs
2.44 - SC_def "SC == lam l:list(nat).list_case(0, \%x xs.succ(x), l)"
2.45 - \(\vdots\)
2.46 + SC_def "SC == lam l:list(nat).list_case(0, \%x xs.succ(x), l)"
2.47 + \(\vdots\)
2.48 +end
2.49 +
2.50 +Primrec = Primrec_defs +
2.51 +consts prim_rec :: i
2.52 inductive
2.53 - domains "primrec" <= "list(nat)->nat"
2.54 - intrs
2.55 - SC "SC : primrec"
2.56 - CONST "k: nat ==> CONST(k) : primrec"
2.57 - PROJ "i: nat ==> PROJ(i) : primrec"
2.58 - COMP "[| g: primrec; fs: list(primrec) |] ==> COMP(g,fs): primrec"
2.59 - PREC "[| f: primrec; g: primrec |] ==> PREC(f,g): primrec"
2.60 - monos list_mono
2.61 - con_defs SC_def, CONST_def, PROJ_def, COMP_def, PREC_def
2.62 - type_intrs "nat_typechecks @ list.intrs @
2.63 - [lam_type, list_case_type, drop_type, map_type,
2.64 - apply_type, rec_type]"
2.65 + domains "primrec" <= "list(nat)->nat"
2.66 + intrs
2.67 + SC "SC : primrec"
2.68 + CONST "k: nat ==> CONST(k) : primrec"
2.69 + PROJ "i: nat ==> PROJ(i) : primrec"
2.70 + COMP "[| g: primrec; fs: list(primrec) |] ==> COMP(g,fs): primrec"
2.71 + PREC "[| f: primrec; g: primrec |] ==> PREC(f,g): primrec"
2.72 + monos list_mono
2.73 + con_defs SC_def, CONST_def, PROJ_def, COMP_def, PREC_def
2.74 + type_intrs "nat_typechecks @ list.intrs @
2.75 + [lam_type, list_case_type, drop_type, map_type,
2.76 + apply_type, rec_type]"
2.77 end
2.78 \end{ttbox}
2.79 \hrule
2.80 @@ -937,7 +941,7 @@
2.81 $\QInl(a)$ and $\QInr(b)$ for $a$, $b\in\quniv(A)$. In a typical codatatype
2.82 definition with set parameters $A_1$, \ldots, $A_k$, a suitable domain is
2.83 $\quniv(A_1\un\cdots\un A_k)$. Details are published
2.84 -elsewhere~\cite{paulson-final}.
2.85 +elsewhere~\cite{paulson-mscs}.
2.86
2.87 \subsection{The case analysis operator}
2.88 The (co)datatype package automatically defines a case analysis operator,
2.89 @@ -1000,7 +1004,7 @@
2.90 \ifshort
2.91 Now $\lst(A)$ is a datatype and enjoys the usual induction rule.
2.92 \else
2.93 -Since $\lst(A)$ is a datatype, it enjoys a structural induction rule, {\tt
2.94 +Since $\lst(A)$ is a datatype, it has a structural induction rule, {\tt
2.95 list.induct}:
2.96 \[ \infer{P(x)}{x\in\lst(A) & P(\Nil)
2.97 & \infer*{P(\Cons(a,l))}{[a\in A & l\in\lst(A) & P(l)]_{a,l}} }
2.98 @@ -1079,7 +1083,7 @@
2.99 \right]_{t,f}} }
2.100 \]
2.101 This rule establishes a single predicate for $\TF(A)$, the union of the
2.102 -recursive sets. Although such reasoning is sometimes useful
2.103 +recursive sets. Although such reasoning can be useful
2.104 \cite[\S4.5]{paulson-set-II}, a proper mutual induction rule should establish
2.105 separate predicates for $\tree(A)$ and $\forest(A)$. The package calls this
2.106 rule {\tt tree\_forest.mutual\_induct}. Observe the usage of $P$ and $Q$ in
2.107 @@ -1292,7 +1296,7 @@
2.108 Isabelle/\textsc{zf} instead uses a variant notion of ordered pairing, which
2.109 can be generalized to a variant notion of function. Elsewhere I have
2.110 proved that this simple approach works (yielding final coalgebras) for a broad
2.111 -class of definitions~\cite{paulson-final}.
2.112 +class of definitions~\cite{paulson-mscs}.
2.113
2.114 Several large studies make heavy use of inductive definitions. L\"otzbeyer
2.115 and Sandner have formalized two chapters of a semantics book~\cite{winskel93},
2.116 @@ -1318,15 +1322,12 @@
2.117 The approach is not restricted to set theory. It should be suitable for any
2.118 logic that has some notion of set and the Knaster-Tarski theorem. I have
2.119 ported the (co)inductive definition package from Isabelle/\textsc{zf} to
2.120 -Isabelle/\textsc{hol} (higher-order logic). V\"olker~\cite{voelker95}
2.121 -is investigating how to port the (co)datatype package. \textsc{hol}
2.122 -represents sets by unary predicates; defining the corresponding types may
2.123 -cause complications.
2.124 +Isabelle/\textsc{hol} (higher-order logic).
2.125
2.126
2.127 \begin{footnotesize}
2.128 \bibliographystyle{springer}
2.129 -\bibliography{string-abbrv,atp,theory,funprog,isabelle,crossref}
2.130 +\bibliography{../manual}
2.131 \end{footnotesize}
2.132 %%%%%\doendnotes
2.133