1.1 --- a/doc-src/Logics/HOL.tex Thu Apr 10 14:26:01 1997 +0200
1.2 +++ b/doc-src/Logics/HOL.tex Thu Apr 10 18:07:27 1997 +0200
1.3 @@ -1864,7 +1864,7 @@
1.4 This package is derived from the ZF one, described in a
1.5 separate paper,\footnote{It appeared in CADE~\cite{paulson-CADE} and a
1.6 longer version is distributed with Isabelle.} which you should refer to
1.7 -in case of difficulties. The package is simpler than ZF's, thanks to HOL's
1.8 +in case of difficulties. The package is simpler than ZF's thanks to HOL's
1.9 automatic type-checking. The type of the (co)inductive determines the
1.10 domain of the fixedpoint definition, and the package does not use inference
1.11 rules for type-checking.
1.12 @@ -1893,9 +1893,10 @@
1.13 elim}, using freeness reasoning on some underlying datatype.
1.14 \end{description}
1.15
1.16 -For an inductive definition, the result structure contains two induction rules,
1.17 -{\tt induct} and \verb|mutual_induct|. For a coinductive definition, it
1.18 -contains the rule \verb|coinduct|.
1.19 +For an inductive definition, the result structure contains two induction
1.20 +rules, {\tt induct} and \verb|mutual_induct|. (To save storage, the latter
1.21 +rule is just {\tt True} unless more than one set is being defined.) For a
1.22 +coinductive definition, it contains the rule \verb|coinduct|.
1.23
1.24 Figure~\ref{def-result-fig} summarizes the two result signatures,
1.25 specifying the types of all these components.
1.26 @@ -2003,8 +2004,9 @@
1.27 end
1.28 \end{ttbox}
1.29 The HOL distribution contains many other inductive definitions, such as the
1.30 -theory {\tt HOL/ex/PropLog.thy} and the directory {\tt HOL/IMP}. The
1.31 -theory {\tt HOL/ex/LList.thy} contains coinductive definitions.
1.32 +theory {\tt HOL/ex/PropLog.thy} and the subdirectories {\tt IMP}, {\tt Lambda}
1.33 +and {\tt Auth}. The theory {\tt HOL/ex/LList.thy} contains coinductive
1.34 +definitions.
1.35
1.36 \index{*coinductive|)} \index{*inductive|)}
1.37
1.38 @@ -2023,7 +2025,7 @@
1.39 equivalence proofs, soundness and completeness of the Hoare rules w.r.t.\ the
1.40 denotational semantics, and soundness and completeness of a verification
1.41 condition generator. Much of development is taken from
1.42 -Winskel~\cite{winskel93}. For details see~\cite{Nipkow-FSTTCS-96}.
1.43 +Winskel~\cite{winskel93}. For details see~\cite{nipkow-IMP}.
1.44
1.45 Directory {\tt HOL/Hoare} contains a user friendly surface syntax for Hoare
1.46 logic, including a tactic for generating verification-conditions.
2.1 --- a/doc-src/Logics/logics.bbl Thu Apr 10 14:26:01 1997 +0200
2.2 +++ b/doc-src/Logics/logics.bbl Thu Apr 10 18:07:27 1997 +0200
2.3 @@ -126,11 +126,37 @@
2.4 \newblock {\em Intuitionistic type theory}.
2.5 \newblock Bibliopolis, 1984.
2.6
2.7 +\bibitem{milner78}
2.8 +Robin Milner.
2.9 +\newblock A theory of type polymorphism in programming.
2.10 +\newblock {\em Journal of Computer and System Sciences}, 17:348--375, 1978.
2.11 +
2.12 \bibitem{milner-coind}
2.13 Robin Milner and Mads Tofte.
2.14 \newblock Co-induction in relational semantics.
2.15 \newblock {\em Theoretical Computer Science}, 87:209--220, 1991.
2.16
2.17 +\bibitem{nazareth-nipkow}
2.18 +Dieter Nazareth and Tobias Nipkow.
2.19 +\newblock Formal verification of algorithm {W}: The monomorphic case.
2.20 +\newblock In J.~von Wright, J.~Grundy, and J.~Harrison, editors, {\em Theorem
2.21 + Proving in Higher Order Logics: {TPHOLs} '96}, LNCS 1125, pages 331--345,
2.22 + 1996.
2.23 +
2.24 +\bibitem{Nipkow-CR}
2.25 +Tobias Nipkow.
2.26 +\newblock More {Church-Rosser} proofs (in {Isabelle/HOL}).
2.27 +\newblock In Michael McRobbie and John~K. Slaney, editors, {\em Automated
2.28 + Deduction --- {CADE}-13 International Conference}, LNAI 1104, pages 733--747.
2.29 + Springer, 1996.
2.30 +
2.31 +\bibitem{nipkow-IMP}
2.32 +Tobias Nipkow.
2.33 +\newblock Winskel is (almost) right: Towards a mechanized semantics textbook.
2.34 +\newblock In V.~Chandru and V.~Vinay, editors, {\em Foundations of Software
2.35 + Technology and Theoretical Computer Science}, volume 1180 of {\em LNCS},
2.36 + pages 180--192. Springer, 1996.
2.37 +
2.38 \bibitem{noel}
2.39 Philippe No{\"e}l.
2.40 \newblock Experimenting with {Isabelle} in {ZF} set theory.
2.41 @@ -173,10 +199,23 @@
2.42 \newblock Set theory for verification: {II}. {Induction} and recursion.
2.43 \newblock {\em Journal of Automated Reasoning}, 15(2):167--215, 1995.
2.44
2.45 +\bibitem{paulson-ns}
2.46 +Lawrence~C. Paulson.
2.47 +\newblock Mechanized proofs of security protocols: {Needham-Schroeder} with
2.48 + public keys.
2.49 +\newblock Technical Report 413, Computer Laboratory, University of Cambridge,
2.50 + January 1997.
2.51 +
2.52 \bibitem{paulson-coind}
2.53 Lawrence~C. Paulson.
2.54 \newblock Mechanizing coinduction and corecursion in higher-order logic.
2.55 -\newblock {\em Journal of Logic and Computation}, 7(2), March 1997.
2.56 +\newblock {\em Journal of Logic and Computation}, 7(2):175--204, March 1997.
2.57 +
2.58 +\bibitem{paulson-security}
2.59 +Lawrence~C. Paulson.
2.60 +\newblock Proving properties of security protocols by induction.
2.61 +\newblock In {\em 10th Computer Security Foundations Workshop}. IEEE Computer
2.62 + Society Press, 1997.
2.63 \newblock In press.
2.64
2.65 \bibitem{paulson-COLOG}
2.66 @@ -197,7 +236,7 @@
2.67 F.~J. Pelletier.
2.68 \newblock Seventy-five problems for testing automatic theorem provers.
2.69 \newblock {\em Journal of Automated Reasoning}, 2:191--216, 1986.
2.70 -\newblock Errata, JAR 4 (1988), 235--236.
2.71 +\newblock Errata, JAR 4 (1988), 235--236 and JAR 18 (1997), 135.
2.72
2.73 \bibitem{plaisted90}
2.74 David~A. Plaisted.
3.1 --- a/doc-src/Logics/logics.tex Thu Apr 10 14:26:01 1997 +0200
3.2 +++ b/doc-src/Logics/logics.tex Thu Apr 10 18:07:27 1997 +0200
3.3 @@ -61,6 +61,6 @@
3.4 %%\include{Cube}
3.5 %%\include{LCF}
3.6 \bibliographystyle{plain}
3.7 -\bibliography{string,atp,theory,funprog,logicprog,isabelle,crossref}
3.8 +\bibliography{string,general,atp,theory,funprog,logicprog,isabelle,crossref}
3.9 \input{logics.ind}
3.10 \end{document}