359

1 
\contentsline {chapter}{\numberline {1}Basic Concepts}{1}


2 
\contentsline {section}{\numberline {1.1}Syntax definitions}{2}

104

3 
\contentsline {section}{\numberline {1.2}Proof procedures}{3}

359

4 
\contentsline {chapter}{\numberline {2}FirstOrder Logic}{4}

104

5 
\contentsline {section}{\numberline {2.1}Syntax and rules of inference}{4}


6 
\contentsline {section}{\numberline {2.2}Generic packages}{8}


7 
\contentsline {section}{\numberline {2.3}Intuitionistic proof procedures}{8}


8 
\contentsline {section}{\numberline {2.4}Classical proof procedures}{10}


9 
\contentsline {section}{\numberline {2.5}An intuitionistic example}{11}


10 
\contentsline {section}{\numberline {2.6}An example of intuitionistic negation}{12}


11 
\contentsline {section}{\numberline {2.7}A classical example}{14}

359

12 
\contentsline {section}{\numberline {2.8}Derived rules and the classical tactics}{15}

465

13 
\contentsline {subsection}{\numberline {2.8.1}Deriving the introduction rule}{16}


14 
\contentsline {subsection}{\numberline {2.8.2}Deriving the elimination rule}{17}


15 
\contentsline {subsection}{\numberline {2.8.3}Using the derived rules}{17}


16 
\contentsline {subsection}{\numberline {2.8.4}Derived rules versus definitions}{19}

359

17 
\contentsline {chapter}{\numberline {3}ZermeloFraenkel Set Theory}{22}


18 
\contentsline {section}{\numberline {3.1}Which version of axiomatic set theory?}{22}


19 
\contentsline {section}{\numberline {3.2}The syntax of set theory}{23}


20 
\contentsline {section}{\numberline {3.3}Binding operators}{25}


21 
\contentsline {section}{\numberline {3.4}The ZermeloFraenkel axioms}{27}


22 
\contentsline {section}{\numberline {3.5}From basic lemmas to function spaces}{30}

465

23 
\contentsline {subsection}{\numberline {3.5.1}Fundamental lemmas}{30}


24 
\contentsline {subsection}{\numberline {3.5.2}Unordered pairs and finite sets}{32}


25 
\contentsline {subsection}{\numberline {3.5.3}Subset and lattice properties}{32}


26 
\contentsline {subsection}{\numberline {3.5.4}Ordered pairs}{36}


27 
\contentsline {subsection}{\numberline {3.5.5}Relations}{36}


28 
\contentsline {subsection}{\numberline {3.5.6}Functions}{37}

359

29 
\contentsline {section}{\numberline {3.6}Further developments}{38}


30 
\contentsline {section}{\numberline {3.7}Simplification rules}{47}


31 
\contentsline {section}{\numberline {3.8}The examples directory}{47}


32 
\contentsline {section}{\numberline {3.9}A proof about powersets}{48}


33 
\contentsline {section}{\numberline {3.10}Monotonicity of the union operator}{51}


34 
\contentsline {section}{\numberline {3.11}Lowlevel reasoning about functions}{52}


35 
\contentsline {chapter}{\numberline {4}HigherOrder Logic}{55}


36 
\contentsline {section}{\numberline {4.1}Syntax}{55}

465

37 
\contentsline {subsection}{\numberline {4.1.1}Types}{57}


38 
\contentsline {subsection}{\numberline {4.1.2}Binders}{58}


39 
\contentsline {subsection}{\numberline {4.1.3}The {\ptt let} and {\ptt case} constructions}{58}

359

40 
\contentsline {section}{\numberline {4.2}Rules of inference}{58}


41 
\contentsline {section}{\numberline {4.3}A formulation of set theory}{60}

465

42 
\contentsline {subsection}{\numberline {4.3.1}Syntax of set theory}{65}


43 
\contentsline {subsection}{\numberline {4.3.2}Axioms and rules of set theory}{69}

359

44 
\contentsline {section}{\numberline {4.4}Generic packages and classical reasoning}{71}


45 
\contentsline {section}{\numberline {4.5}Types}{73}

465

46 
\contentsline {subsection}{\numberline {4.5.1}Product and sum types}{73}


47 
\contentsline {subsection}{\numberline {4.5.2}The type of natural numbers, {\ptt nat}}{73}


48 
\contentsline {subsection}{\numberline {4.5.3}The type constructor for lists, {\ptt list}}{76}


49 
\contentsline {subsection}{\numberline {4.5.4}The type constructor for lazy lists, {\ptt llist}}{76}


50 
\contentsline {section}{\numberline {4.6}Datatype declarations}{79}


51 
\contentsline {subsection}{\numberline {4.6.1}Foundations}{79}


52 
\contentsline {subsection}{\numberline {4.6.2}Defining datatypes}{80}


53 
\contentsline {subsection}{\numberline {4.6.3}Examples}{82}


54 
\contentsline {subsubsection}{The datatype $\alpha \penalty \@M \ list$}{82}


55 
\contentsline {subsubsection}{The datatype $\alpha \penalty \@M \ list$ with mixfix syntax}{83}


56 
\contentsline {subsubsection}{Defining functions on datatypes}{83}


57 
\contentsline {subsubsection}{A datatype for weekdays}{84}


58 
\contentsline {section}{\numberline {4.7}The examples directories}{84}


59 
\contentsline {section}{\numberline {4.8}Example: Cantor's Theorem}{85}


60 
\contentsline {chapter}{\numberline {5}FirstOrder Sequent Calculus}{88}


61 
\contentsline {section}{\numberline {5.1}Unification for lists}{88}


62 
\contentsline {section}{\numberline {5.2}Syntax and rules of inference}{90}


63 
\contentsline {section}{\numberline {5.3}Tactics for the cut rule}{92}


64 
\contentsline {section}{\numberline {5.4}Tactics for sequents}{93}


65 
\contentsline {section}{\numberline {5.5}Packaging sequent rules}{94}


66 
\contentsline {section}{\numberline {5.6}Proof procedures}{94}


67 
\contentsline {subsection}{\numberline {5.6.1}Method A}{95}


68 
\contentsline {subsection}{\numberline {5.6.2}Method B}{95}


69 
\contentsline {section}{\numberline {5.7}A simple example of classical reasoning}{96}


70 
\contentsline {section}{\numberline {5.8}A more complex proof}{97}


71 
\contentsline {chapter}{\numberline {6}Constructive Type Theory}{99}


72 
\contentsline {section}{\numberline {6.1}Syntax}{101}


73 
\contentsline {section}{\numberline {6.2}Rules of inference}{101}


74 
\contentsline {section}{\numberline {6.3}Rule lists}{107}


75 
\contentsline {section}{\numberline {6.4}Tactics for subgoal reordering}{107}


76 
\contentsline {section}{\numberline {6.5}Rewriting tactics}{108}


77 
\contentsline {section}{\numberline {6.6}Tactics for logical reasoning}{109}


78 
\contentsline {section}{\numberline {6.7}A theory of arithmetic}{111}


79 
\contentsline {section}{\numberline {6.8}The examples directory}{111}


80 
\contentsline {section}{\numberline {6.9}Example: type inference}{111}


81 
\contentsline {section}{\numberline {6.10}An example of logical reasoning}{113}


82 
\contentsline {section}{\numberline {6.11}Example: deriving a currying functional}{116}


83 
\contentsline {section}{\numberline {6.12}Example: proving the Axiom of Choice}{117}
