1219 The simpset \ttindex{list_ss} contains, along with additional useful lemmas, 
1219 The simpset \ttindex{list_ss} contains, along with additional useful lemmas, 
1220 the basic rewrite rules that appear in Fig.\ts\ref{hollistsimps}. 
1220 the basic rewrite rules that appear in Fig.\ts\ref{hollistsimps}. 
1221 
1221 
1222 The tactic {\tt\ttindex{list_ind_tac} "$xs$" $i$} performs induction over the 
1222 The tactic {\tt\ttindex{list_ind_tac} "$xs$" $i$} performs induction over the 
1223 variable~$xs$ in subgoal~$i$. 
1223 variable~$xs$ in subgoal~$i$. 
1224 

1225 

1226 \subsection{The type constructor for lazy lists, {\tt llist}} 

1227 \index{*llist type} 

1228 

1229 The definition of lazy lists demonstrates methods for handling infinite 

1230 data structures and coinduction in higherorder logic. Theory 

1231 \thydx{LList} defines an operator for corecursion on lazy lists, which is 

1232 used to define a few simple functions such as map and append. Corecursion 

1233 cannot easily define operations such as filter, which can compute 

1234 indefinitely before yielding the next element (if any!) of the lazy list. 

1235 A coinduction principle is defined for proving equations on lazy lists. 

1236 

1237 I have written a paper discussing the treatment of lazy lists; it also 

1238 covers finite lists~\cite{paulsoncoind}. 

1239 
1224 
1240 
1225 
1241 \section{Datatype declarations} 
1226 \section{Datatype declarations} 
1242 \index{*datatype(} 
1227 \index{*datatype(} 
1243 
1228 
1743 monos "[Pow_mono]" 
1728 monos "[Pow_mono]" 
1744 end 
1729 end 
1745 \end{ttbox} 
1730 \end{ttbox} 
1746 The HOL distribution contains many other inductive definitions, such as the 
1731 The HOL distribution contains many other inductive definitions, such as the 
1747 theory {\tt HOL/ex/PropLog.thy} and the directory {\tt HOL/IMP}. The 
1732 theory {\tt HOL/ex/PropLog.thy} and the directory {\tt HOL/IMP}. The 
1748 theory {\tt HOL/LList.thy} contains coinductive definitions. 
1733 theory {\tt HOL/ex/LList.thy} contains coinductive definitions. 
1749 
1734 
1750 \index{*coinductive)} \index{*inductive)} \underscoreoff 
1735 \index{*coinductive)} \index{*inductive)} \underscoreoff 
1751 
1736 
1752 
1737 
1753 \section{The examples directories} 
1738 \section{The examples directories} 
1781 \item File {\tt set.ML} proves Cantor's Theorem, which is presented in 
1766 \item File {\tt set.ML} proves Cantor's Theorem, which is presented in 
1782 \S\ref{sec:holcantor} below, and the Schr\"oderBernstein Theorem. 
1767 \S\ref{sec:holcantor} below, and the Schr\"oderBernstein Theorem. 
1783 
1768 
1784 \item Theories {\tt InSort} and {\tt Qsort} prove correctness properties of 
1769 \item Theories {\tt InSort} and {\tt Qsort} prove correctness properties of 
1785 insertion sort and quick sort. 
1770 insertion sort and quick sort. 

1771 

1772 \item The definition of lazy lists demonstrates methods for handling 

1773 infinite data structures and coinduction in higherorder 

1774 logic~\cite{paulsoncoind}. Theory \thydx{LList} defines an operator for 

1775 corecursion on lazy lists, which is used to define a few simple functions 

1776 such as map and append. Corecursion cannot easily define operations such 

1777 as filter, which can compute indefinitely before yielding the next 

1778 element (if any!) of the lazy list. A coinduction principle is defined 

1779 for proving equations on lazy lists. 
1786 
1780 
1787 \item Theory {\tt PropLog} proves the soundness and completeness of 
1781 \item Theory {\tt PropLog} proves the soundness and completeness of 
1788 classical propositional logic, given a truth table semantics. The only 
1782 classical propositional logic, given a truth table semantics. The only 
1789 connective is $\imp$. A Hilbertstyle axiom system is specified, and its 
1783 connective is $\imp$. A Hilbertstyle axiom system is specified, and its 
1790 set of theorems defined inductively. A similar proof in \ZF{} is 
1784 set of theorems defined inductively. A similar proof in \ZF{} is 