105

1 
\contentsline {part}{\uppercase {i}\phspace {1em}Foundations}{1}


2 
\contentsline {section}{\numberline {1}Formalizing logical syntax in Isabelle}{1}


3 
\contentsline {subsection}{\numberline {1.1}Simple types and constants}{1}


4 
\contentsline {subsection}{\numberline {1.2}Polymorphic types and constants}{3}

359

5 
\contentsline {subsection}{\numberline {1.3}Higher types and quantifiers}{5}

105

6 
\contentsline {section}{\numberline {2}Formalizing logical rules in Isabelle}{5}


7 
\contentsline {subsection}{\numberline {2.1}Expressing propositional rules}{6}


8 
\contentsline {subsection}{\numberline {2.2}Quantifier rules and substitution}{7}


9 
\contentsline {subsection}{\numberline {2.3}Signatures and theories}{8}


10 
\contentsline {section}{\numberline {3}Proof construction in Isabelle}{9}


11 
\contentsline {subsection}{\numberline {3.1}Higherorder unification}{10}


12 
\contentsline {subsection}{\numberline {3.2}Joining rules by resolution}{11}

359

13 
\contentsline {section}{\numberline {4}Lifting a rule into a context}{13}


14 
\contentsline {subsection}{\numberline {4.1}Lifting over assumptions}{13}


15 
\contentsline {subsection}{\numberline {4.2}Lifting over parameters}{14}


16 
\contentsline {section}{\numberline {5}Backward proof by resolution}{15}


17 
\contentsline {subsection}{\numberline {5.1}Refinement by resolution}{15}


18 
\contentsline {subsection}{\numberline {5.2}Proof by assumption}{16}


19 
\contentsline {subsection}{\numberline {5.3}A propositional proof}{16}


20 
\contentsline {subsection}{\numberline {5.4}A quantifier proof}{17}


21 
\contentsline {subsection}{\numberline {5.5}Tactics and tacticals}{18}


22 
\contentsline {section}{\numberline {6}Variations on resolution}{18}


23 
\contentsline {subsection}{\numberline {6.1}Elimresolution}{19}


24 
\contentsline {subsection}{\numberline {6.2}Destruction rules}{20}


25 
\contentsline {subsection}{\numberline {6.3}Deriving rules by resolution}{21}


26 
\contentsline {part}{\uppercase {ii}\phspace {1em}Getting Started with Isabelle}{23}


27 
\contentsline {section}{\numberline {7}Forward proof}{23}


28 
\contentsline {subsection}{\numberline {7.1}Lexical matters}{23}


29 
\contentsline {subsection}{\numberline {7.2}Syntax of types and terms}{24}


30 
\contentsline {subsection}{\numberline {7.3}Basic operations on theorems}{25}


31 
\contentsline {subsection}{\numberline {7.4}*Flexflex constraints}{27}


32 
\contentsline {section}{\numberline {8}Backward proof}{28}


33 
\contentsline {subsection}{\numberline {8.1}The basic tactics}{28}


34 
\contentsline {subsection}{\numberline {8.2}Commands for backward proof}{29}


35 
\contentsline {subsection}{\numberline {8.3}A trivial example in propositional logic}{29}


36 
\contentsline {subsection}{\numberline {8.4}Part of a distributive law}{31}


37 
\contentsline {section}{\numberline {9}Quantifier reasoning}{32}


38 
\contentsline {subsection}{\numberline {9.1}Two quantifier proofs: a success and a failure}{32}


39 
\contentsline {paragraph}{The successful proof.}{32}


40 
\contentsline {paragraph}{The unsuccessful proof.}{33}


41 
\contentsline {subsection}{\numberline {9.2}Nested quantifiers}{33}


42 
\contentsline {paragraph}{The wrong approach.}{34}


43 
\contentsline {paragraph}{The right approach.}{34}


44 
\contentsline {paragraph}{A onestep proof using tacticals.}{35}


45 
\contentsline {subsection}{\numberline {9.3}A realistic quantifier proof}{36}


46 
\contentsline {subsection}{\numberline {9.4}The classical reasoner}{37}


47 
\contentsline {part}{\uppercase {iii}\phspace {1em}Advanced Methods}{39}


48 
\contentsline {section}{\numberline {10}Deriving rules in Isabelle}{39}


49 
\contentsline {subsection}{\numberline {10.1}Deriving a rule using tactics and metalevel assumptions}{39}


50 
\contentsline {subsection}{\numberline {10.2}Definitions and derived rules}{41}


51 
\contentsline {subsection}{\numberline {10.3}Deriving the $\neg $ introduction rule}{41}


52 
\contentsline {subsection}{\numberline {10.4}Deriving the $\neg $ elimination rule}{42}


53 
\contentsline {section}{\numberline {11}Defining theories}{44}

1085

54 
\contentsline {subsection}{\numberline {11.1}Declaring constants, definitions and rules}{46}

359

55 
\contentsline {subsection}{\numberline {11.2}Declaring type constructors}{46}


56 
\contentsline {subsection}{\numberline {11.3}Type synonyms}{48}


57 
\contentsline {subsection}{\numberline {11.4}Infix and mixfix operators}{48}


58 
\contentsline {subsection}{\numberline {11.5}Overloading}{50}


59 
\contentsline {section}{\numberline {12}Theory example: the natural numbers}{51}


60 
\contentsline {subsection}{\numberline {12.1}Extending firstorder logic with the natural numbers}{51}


61 
\contentsline {subsection}{\numberline {12.2}Declaring the theory to Isabelle}{52}


62 
\contentsline {subsection}{\numberline {12.3}Proving some recursion equations}{52}


63 
\contentsline {section}{\numberline {13}Refinement with explicit instantiation}{53}


64 
\contentsline {subsection}{\numberline {13.1}A simple proof by induction}{53}


65 
\contentsline {subsection}{\numberline {13.2}An example of ambiguity in {\ptt resolve_tac}}{54}


66 
\contentsline {subsection}{\numberline {13.3}Proving that addition is associative}{55}


67 
\contentsline {section}{\numberline {14}A Prolog interpreter}{56}


68 
\contentsline {subsection}{\numberline {14.1}Simple executions}{57}


69 
\contentsline {subsection}{\numberline {14.2}Backtracking}{58}


70 
\contentsline {subsection}{\numberline {14.3}Depthfirst search}{59}
