summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

doc-src/Logics/Old_HOL.tex

changeset 629 | c97f5a7cf763 |

parent 600 | d9133e7ed38a |

child 705 | 9fb068497df4 |

--- a/doc-src/Logics/Old_HOL.tex Mon Oct 10 18:09:58 1994 +0100 +++ b/doc-src/Logics/Old_HOL.tex Wed Oct 12 09:20:17 1994 +0100 @@ -1223,21 +1223,6 @@ variable~$xs$ in subgoal~$i$. -\subsection{The type constructor for lazy lists, {\tt llist}} -\index{*llist type} - -The definition of lazy lists demonstrates methods for handling infinite -data structures and coinduction in higher-order logic. Theory -\thydx{LList} defines an operator for corecursion on lazy lists, which is -used to define a few simple functions such as map and append. Corecursion -cannot easily define operations such as filter, which can compute -indefinitely before yielding the next element (if any!) of the lazy list. -A coinduction principle is defined for proving equations on lazy lists. - -I have written a paper discussing the treatment of lazy lists; it also -covers finite lists~\cite{paulson-coind}. - - \section{Datatype declarations} \index{*datatype|(} @@ -1745,7 +1730,7 @@ \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/LList.thy} contains coinductive definitions. +theory {\tt HOL/ex/LList.thy} contains coinductive definitions. \index{*coinductive|)} \index{*inductive|)} \underscoreoff @@ -1784,6 +1769,15 @@ \item Theories {\tt InSort} and {\tt Qsort} prove correctness properties of insertion sort and quick sort. +\item The definition of lazy lists demonstrates methods for handling + infinite data structures and coinduction in higher-order + logic~\cite{paulson-coind}. Theory \thydx{LList} defines an operator for + corecursion on lazy lists, which is used to define a few simple functions + such as map and append. Corecursion cannot easily define operations such + as filter, which can compute indefinitely before yielding the next + element (if any!) of the lazy list. A coinduction principle is defined + for proving equations on lazy lists. + \item Theory {\tt PropLog} proves the soundness and completeness of classical propositional logic, given a truth table semantics. The only connective is $\imp$. A Hilbert-style axiom system is specified, and its