# HG changeset patch
# User paulson
# Date 860688447 -7200
# Node ID f842a75d96246ec37c9ed6abc5d2e1b181833519
# Parent  9c4d5fd41c9b234abaebe30c11cfe1deabe04225
Updated discussion and references for inductive definitions

diff -r 9c4d5fd41c9b -r f842a75d9624 doc-src/Logics/HOL.tex
--- 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.
diff -r 9c4d5fd41c9b -r f842a75d9624 doc-src/Logics/logics.bbl
--- 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.
diff -r 9c4d5fd41c9b -r f842a75d9624 doc-src/Logics/logics.tex
--- 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}