doc-src/Logics/Old_HOL.tex
 changeset 629 c97f5a7cf763 parent 600 d9133e7ed38a child 705 9fb068497df4
equal inserted replaced
628:bb3f87f9cafe 629:c97f5a7cf763
  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{hol-list-simps}.
  1220 the basic rewrite rules that appear in Fig.\ts\ref{hol-list-simps}.
  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$.
  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:hol-cantor} below, and the Schr\"oder-Bernstein Theorem.
  1767   \S\ref{sec:hol-cantor} below, and the Schr\"oder-Bernstein 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 higher-order

  1774   logic~\cite{paulson-coind}.  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 Hilbert-style axiom system is specified, and its
  1783   connective is $\imp$.  A Hilbert-style 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