104

1 
\contentsline {chapter}{\numberline {1}Introduction}{1}


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


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


4 
\contentsline {chapter}{\numberline {2}Firstorder logic}{4}


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}


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


13 
\contentsline {subsection}{Deriving the introduction rule}{17}


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


15 
\contentsline {subsection}{Using the derived rules}{18}


16 
\contentsline {subsection}{Derived rules versus definitions}{20}


17 
\contentsline {chapter}{\numberline {3}ZermeloFraenkel set theory}{23}


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


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


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


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


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


23 
\contentsline {subsection}{Fundamental lemmas}{33}


24 
\contentsline {subsection}{Unordered pairs and finite sets}{36}


25 
\contentsline {subsection}{Subset and lattice properties}{36}


26 
\contentsline {subsection}{Ordered pairs}{37}


27 
\contentsline {subsection}{Relations}{37}


28 
\contentsline {subsection}{Functions}{40}


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


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


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


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


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}


37 
\contentsline {subsection}{Types}{55}


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


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


40 
\contentsline {section}{\numberline {4.3}Generic packages}{62}


41 
\contentsline {section}{\numberline {4.4}A formulation of set theory}{63}


42 
\contentsline {subsection}{Syntax of set theory}{63}


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


44 
\contentsline {subsection}{Derived rules for sets}{69}


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


46 
\contentsline {subsection}{Product and sum types}{74}


47 
\contentsline {subsection}{The type of natural numbers, $nat$}{74}


48 
\contentsline {subsection}{The type constructor for lists, $\alpha \pcomma list$}{74}


49 
\contentsline {subsection}{The type constructor for lazy lists, $\alpha \pcomma llist$}{78}


50 
\contentsline {section}{\numberline {4.6}Classical proof procedures}{78}


51 
\contentsline {section}{\numberline {4.7}The examples directory}{78}


52 
\contentsline {section}{\numberline {4.8}Example: deriving the conjunction rules}{79}


53 
\contentsline {subsection}{The introduction rule}{79}


54 
\contentsline {subsection}{The elimination rule}{80}


55 
\contentsline {section}{\numberline {4.9}Example: Cantor's Theorem}{81}


56 
\contentsline {chapter}{\numberline {5}Firstorder sequent calculus}{83}


57 
\contentsline {section}{\numberline {5.1}Unification for lists}{83}


58 
\contentsline {section}{\numberline {5.2}Syntax and rules of inference}{84}


59 
\contentsline {section}{\numberline {5.3}Tactics for the cut rule}{84}


60 
\contentsline {section}{\numberline {5.4}Tactics for sequents}{88}


61 
\contentsline {section}{\numberline {5.5}Packaging sequent rules}{89}


62 
\contentsline {section}{\numberline {5.6}Proof procedures}{89}


63 
\contentsline {subsection}{Method A}{90}


64 
\contentsline {subsection}{Method B}{90}


65 
\contentsline {section}{\numberline {5.7}A simple example of classical reasoning}{91}


66 
\contentsline {section}{\numberline {5.8}A more complex proof}{92}


67 
\contentsline {chapter}{\numberline {6}Constructive Type Theory}{95}


68 
\contentsline {section}{\numberline {6.1}Syntax}{96}


69 
\contentsline {section}{\numberline {6.2}Rules of inference}{96}


70 
\contentsline {section}{\numberline {6.3}Rule lists}{101}


71 
\contentsline {section}{\numberline {6.4}Tactics for subgoal reordering}{104}


72 
\contentsline {section}{\numberline {6.5}Rewriting tactics}{105}


73 
\contentsline {section}{\numberline {6.6}Tactics for logical reasoning}{105}


74 
\contentsline {section}{\numberline {6.7}A theory of arithmetic}{106}


75 
\contentsline {section}{\numberline {6.8}The examples directory}{106}


76 
\contentsline {section}{\numberline {6.9}Example: type inference}{108}


77 
\contentsline {section}{\numberline {6.10}An example of logical reasoning}{109}


78 
\contentsline {section}{\numberline {6.11}Example: deriving a currying functional}{112}


79 
\contentsline {section}{\numberline {6.12}Example: proving the Axiom of Choice}{113}


80 
\contentsline {chapter}{\numberline {7}Defining Logics}{118}


81 
\contentsline {section}{\numberline {7.1}Precedence grammars}{118}


82 
\contentsline {section}{\numberline {7.2}Basic syntax}{119}


83 
\contentsline {subsection}{Logical types and default syntax}{120}


84 
\contentsline {subsection}{Lexical matters *}{121}


85 
\contentsline {subsection}{Inspecting syntax *}{121}


86 
\contentsline {section}{\numberline {7.3}Abstract syntax trees}{123}


87 
\contentsline {subsection}{Parse trees to asts}{125}


88 
\contentsline {subsection}{Asts to terms *}{126}


89 
\contentsline {subsection}{Printing of terms *}{126}


90 
\contentsline {section}{\numberline {7.4}Mixfix declarations}{128}


91 
\contentsline {subsection}{Infixes}{130}


92 
\contentsline {subsection}{Binders}{130}


93 
\contentsline {section}{\numberline {7.5}Syntactic translations (macros)}{131}


94 
\contentsline {subsection}{Specifying macros}{132}


95 
\contentsline {subsection}{Applying rules}{133}


96 
\contentsline {subsection}{Rewriting strategy}{135}


97 
\contentsline {subsection}{More examples}{135}


98 
\contentsline {section}{\numberline {7.6}Translation functions *}{138}


99 
\contentsline {subsection}{A simple example *}{139}


100 
\contentsline {section}{\numberline {7.7}Example: some minimal logics}{140}
