Revising the Client proof as suggested by Michel Charpentier. New lemmas
about composition (in Union.ML), etc. Also changed "length" to "size"
because it is displayed as "size" in any event.
\contentsline {chapter}{\numberline {1}Basic Concepts}{1}
\contentsline {section}{\numberline {1.1}Syntax definitions}{2}
\contentsline {section}{\numberline {1.2}Proof procedures}{3}
\contentsline {chapter}{\numberline {2}First-Order Logic}{4}
\contentsline {section}{\numberline {2.1}Syntax and rules of inference}{4}
\contentsline {section}{\numberline {2.2}Generic packages}{8}
\contentsline {section}{\numberline {2.3}Intuitionistic proof procedures}{8}
\contentsline {section}{\numberline {2.4}Classical proof procedures}{10}
\contentsline {section}{\numberline {2.5}An intuitionistic example}{11}
\contentsline {section}{\numberline {2.6}An example of intuitionistic negation}{12}
\contentsline {section}{\numberline {2.7}A classical example}{14}
\contentsline {section}{\numberline {2.8}Derived rules and the classical tactics}{15}
\contentsline {subsection}{\numberline {2.8.1}Deriving the introduction rule}{16}
\contentsline {subsection}{\numberline {2.8.2}Deriving the elimination rule}{17}
\contentsline {subsection}{\numberline {2.8.3}Using the derived rules}{17}
\contentsline {subsection}{\numberline {2.8.4}Derived rules versus definitions}{19}
\contentsline {chapter}{\numberline {3}Zermelo-Fraenkel Set Theory}{22}
\contentsline {section}{\numberline {3.1}Which version of axiomatic set theory?}{22}
\contentsline {section}{\numberline {3.2}The syntax of set theory}{23}
\contentsline {section}{\numberline {3.3}Binding operators}{25}
\contentsline {section}{\numberline {3.4}The Zermelo-Fraenkel axioms}{27}
\contentsline {section}{\numberline {3.5}From basic lemmas to function spaces}{30}
\contentsline {subsection}{\numberline {3.5.1}Fundamental lemmas}{30}
\contentsline {subsection}{\numberline {3.5.2}Unordered pairs and finite sets}{32}
\contentsline {subsection}{\numberline {3.5.3}Subset and lattice properties}{32}
\contentsline {subsection}{\numberline {3.5.4}Ordered pairs}{36}
\contentsline {subsection}{\numberline {3.5.5}Relations}{36}
\contentsline {subsection}{\numberline {3.5.6}Functions}{37}
\contentsline {section}{\numberline {3.6}Further developments}{38}
\contentsline {section}{\numberline {3.7}Simplification rules}{47}
\contentsline {section}{\numberline {3.8}The examples directory}{47}
\contentsline {section}{\numberline {3.9}A proof about powersets}{48}
\contentsline {section}{\numberline {3.10}Monotonicity of the union operator}{51}
\contentsline {section}{\numberline {3.11}Low-level reasoning about functions}{52}
\contentsline {chapter}{\numberline {4}Higher-Order Logic}{55}
\contentsline {section}{\numberline {4.1}Syntax}{55}
\contentsline {subsection}{\numberline {4.1.1}Types}{57}
\contentsline {subsection}{\numberline {4.1.2}Binders}{58}
\contentsline {subsection}{\numberline {4.1.3}The {\ptt let} and {\ptt case} constructions}{58}
\contentsline {section}{\numberline {4.2}Rules of inference}{58}
\contentsline {section}{\numberline {4.3}A formulation of set theory}{60}
\contentsline {subsection}{\numberline {4.3.1}Syntax of set theory}{65}
\contentsline {subsection}{\numberline {4.3.2}Axioms and rules of set theory}{69}
\contentsline {section}{\numberline {4.4}Generic packages and classical reasoning}{71}
\contentsline {section}{\numberline {4.5}Types}{73}
\contentsline {subsection}{\numberline {4.5.1}Product and sum types}{73}
\contentsline {subsection}{\numberline {4.5.2}The type of natural numbers, {\ptt nat}}{73}
\contentsline {subsection}{\numberline {4.5.3}The type constructor for lists, {\ptt list}}{76}
\contentsline {subsection}{\numberline {4.5.4}The type constructor for lazy lists, {\ptt llist}}{76}
\contentsline {section}{\numberline {4.6}Datatype declarations}{79}
\contentsline {subsection}{\numberline {4.6.1}Foundations}{79}
\contentsline {subsection}{\numberline {4.6.2}Defining datatypes}{80}
\contentsline {subsection}{\numberline {4.6.3}Examples}{82}
\contentsline {subsubsection}{The datatype $\alpha \penalty \@M \ list$}{82}
\contentsline {subsubsection}{The datatype $\alpha \penalty \@M \ list$ with mixfix syntax}{83}
\contentsline {subsubsection}{Defining functions on datatypes}{83}
\contentsline {subsubsection}{A datatype for weekdays}{84}
\contentsline {section}{\numberline {4.7}The examples directories}{84}
\contentsline {section}{\numberline {4.8}Example: Cantor's Theorem}{85}
\contentsline {chapter}{\numberline {5}First-Order Sequent Calculus}{88}
\contentsline {section}{\numberline {5.1}Unification for lists}{88}
\contentsline {section}{\numberline {5.2}Syntax and rules of inference}{90}
\contentsline {section}{\numberline {5.3}Tactics for the cut rule}{92}
\contentsline {section}{\numberline {5.4}Tactics for sequents}{93}
\contentsline {section}{\numberline {5.5}Packaging sequent rules}{94}
\contentsline {section}{\numberline {5.6}Proof procedures}{94}
\contentsline {subsection}{\numberline {5.6.1}Method A}{95}
\contentsline {subsection}{\numberline {5.6.2}Method B}{95}
\contentsline {section}{\numberline {5.7}A simple example of classical reasoning}{96}
\contentsline {section}{\numberline {5.8}A more complex proof}{97}
\contentsline {chapter}{\numberline {6}Constructive Type Theory}{99}
\contentsline {section}{\numberline {6.1}Syntax}{101}
\contentsline {section}{\numberline {6.2}Rules of inference}{101}
\contentsline {section}{\numberline {6.3}Rule lists}{107}
\contentsline {section}{\numberline {6.4}Tactics for subgoal reordering}{107}
\contentsline {section}{\numberline {6.5}Rewriting tactics}{108}
\contentsline {section}{\numberline {6.6}Tactics for logical reasoning}{109}
\contentsline {section}{\numberline {6.7}A theory of arithmetic}{111}
\contentsline {section}{\numberline {6.8}The examples directory}{111}
\contentsline {section}{\numberline {6.9}Example: type inference}{111}
\contentsline {section}{\numberline {6.10}An example of logical reasoning}{113}
\contentsline {section}{\numberline {6.11}Example: deriving a currying functional}{116}
\contentsline {section}{\numberline {6.12}Example: proving the Axiom of Choice}{117}