summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | paulson |

Thu, 10 Apr 1997 18:07:27 +0200 | |

changeset 2933 | f842a75d9624 |

parent 2932 | 9c4d5fd41c9b |

child 2934 | bd922fc9001b |

Updated discussion and references for inductive definitions

--- a/doc-src/Logics/HOL.tex Thu Apr 10 14:26:01 1997 +0200 +++ b/doc-src/Logics/HOL.tex Thu Apr 10 18:07:27 1997 +0200 @@ -1864,7 +1864,7 @@ This package is derived from the ZF one, described in a separate paper,\footnote{It appeared in CADE~\cite{paulson-CADE} and a longer version is distributed with Isabelle.} which you should refer to -in case of difficulties. The package is simpler than ZF's, thanks to HOL's +in case of difficulties. The package is simpler than ZF's thanks to HOL's automatic type-checking. The type of the (co)inductive determines the domain of the fixedpoint definition, and the package does not use inference rules for type-checking. @@ -1893,9 +1893,10 @@ elim}, using freeness reasoning on some underlying datatype. \end{description} -For an inductive definition, the result structure contains two induction rules, -{\tt induct} and \verb|mutual_induct|. For a coinductive definition, it -contains the rule \verb|coinduct|. +For an inductive definition, the result structure contains two induction +rules, {\tt induct} and \verb|mutual_induct|. (To save storage, the latter +rule is just {\tt True} unless more than one set is being defined.) For a +coinductive definition, it contains the rule \verb|coinduct|. Figure~\ref{def-result-fig} summarizes the two result signatures, specifying the types of all these components. @@ -2003,8 +2004,9 @@ end \end{ttbox} The HOL distribution contains many other inductive definitions, such as the -theory {\tt HOL/ex/PropLog.thy} and the directory {\tt HOL/IMP}. The -theory {\tt HOL/ex/LList.thy} contains coinductive definitions. +theory {\tt HOL/ex/PropLog.thy} and the subdirectories {\tt IMP}, {\tt Lambda} +and {\tt Auth}. The theory {\tt HOL/ex/LList.thy} contains coinductive +definitions. \index{*coinductive|)} \index{*inductive|)} @@ -2023,7 +2025,7 @@ equivalence proofs, soundness and completeness of the Hoare rules w.r.t.\ the denotational semantics, and soundness and completeness of a verification condition generator. Much of development is taken from -Winskel~\cite{winskel93}. For details see~\cite{Nipkow-FSTTCS-96}. +Winskel~\cite{winskel93}. For details see~\cite{nipkow-IMP}. Directory {\tt HOL/Hoare} contains a user friendly surface syntax for Hoare logic, including a tactic for generating verification-conditions.

--- a/doc-src/Logics/logics.bbl Thu Apr 10 14:26:01 1997 +0200 +++ b/doc-src/Logics/logics.bbl Thu Apr 10 18:07:27 1997 +0200 @@ -126,11 +126,37 @@ \newblock {\em Intuitionistic type theory}. \newblock Bibliopolis, 1984. +\bibitem{milner78} +Robin Milner. +\newblock A theory of type polymorphism in programming. +\newblock {\em Journal of Computer and System Sciences}, 17:348--375, 1978. + \bibitem{milner-coind} Robin Milner and Mads Tofte. \newblock Co-induction in relational semantics. \newblock {\em Theoretical Computer Science}, 87:209--220, 1991. +\bibitem{nazareth-nipkow} +Dieter Nazareth and Tobias Nipkow. +\newblock Formal verification of algorithm {W}: The monomorphic case. +\newblock In J.~von Wright, J.~Grundy, and J.~Harrison, editors, {\em Theorem + Proving in Higher Order Logics: {TPHOLs} '96}, LNCS 1125, pages 331--345, + 1996. + +\bibitem{Nipkow-CR} +Tobias Nipkow. +\newblock More {Church-Rosser} proofs (in {Isabelle/HOL}). +\newblock In Michael McRobbie and John~K. Slaney, editors, {\em Automated + Deduction --- {CADE}-13 International Conference}, LNAI 1104, pages 733--747. + Springer, 1996. + +\bibitem{nipkow-IMP} +Tobias Nipkow. +\newblock Winskel is (almost) right: Towards a mechanized semantics textbook. +\newblock In V.~Chandru and V.~Vinay, editors, {\em Foundations of Software + Technology and Theoretical Computer Science}, volume 1180 of {\em LNCS}, + pages 180--192. Springer, 1996. + \bibitem{noel} Philippe No{\"e}l. \newblock Experimenting with {Isabelle} in {ZF} set theory. @@ -173,10 +199,23 @@ \newblock Set theory for verification: {II}. {Induction} and recursion. \newblock {\em Journal of Automated Reasoning}, 15(2):167--215, 1995. +\bibitem{paulson-ns} +Lawrence~C. Paulson. +\newblock Mechanized proofs of security protocols: {Needham-Schroeder} with + public keys. +\newblock Technical Report 413, Computer Laboratory, University of Cambridge, + January 1997. + \bibitem{paulson-coind} Lawrence~C. Paulson. \newblock Mechanizing coinduction and corecursion in higher-order logic. -\newblock {\em Journal of Logic and Computation}, 7(2), March 1997. +\newblock {\em Journal of Logic and Computation}, 7(2):175--204, March 1997. + +\bibitem{paulson-security} +Lawrence~C. Paulson. +\newblock Proving properties of security protocols by induction. +\newblock In {\em 10th Computer Security Foundations Workshop}. IEEE Computer + Society Press, 1997. \newblock In press. \bibitem{paulson-COLOG} @@ -197,7 +236,7 @@ F.~J. Pelletier. \newblock Seventy-five problems for testing automatic theorem provers. \newblock {\em Journal of Automated Reasoning}, 2:191--216, 1986. -\newblock Errata, JAR 4 (1988), 235--236. +\newblock Errata, JAR 4 (1988), 235--236 and JAR 18 (1997), 135. \bibitem{plaisted90} David~A. Plaisted.

--- a/doc-src/Logics/logics.tex Thu Apr 10 14:26:01 1997 +0200 +++ b/doc-src/Logics/logics.tex Thu Apr 10 18:07:27 1997 +0200 @@ -61,6 +61,6 @@ %%\include{Cube} %%\include{LCF} \bibliographystyle{plain} -\bibliography{string,atp,theory,funprog,logicprog,isabelle,crossref} +\bibliography{string,general,atp,theory,funprog,logicprog,isabelle,crossref} \input{logics.ind} \end{document}