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}


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


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}


13 
\contentsline {subsection}{\numberline {3.3}Lifting a rule into a context}{13}


14 
\contentsline {subsubsection}{Lifting over assumptions}{13}


15 
\contentsline {subsubsection}{Lifting over parameters}{13}


16 
\contentsline {section}{\numberline {4}Backward proof by resolution}{14}


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


18 
\contentsline {subsection}{\numberline {4.2}Proof by assumption}{15}


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


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


21 
\contentsline {subsection}{\numberline {4.5}Tactics and tacticals}{17}


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


23 
\contentsline {subsection}{\numberline {5.1}Elimresolution}{18}


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


25 
\contentsline {subsection}{\numberline {5.3}Deriving rules by resolution}{20}


26 
\contentsline {part}{\uppercase {ii}\phspace {1em}Getting started with Isabelle}{22}


27 
\contentsline {section}{\numberline {6}Forward proof}{22}


28 
\contentsline {subsection}{\numberline {6.1}Lexical matters}{22}


29 
\contentsline {subsection}{\numberline {6.2}Syntax of types and terms}{23}


30 
\contentsline {subsection}{\numberline {6.3}Basic operations on theorems}{24}


31 
\contentsline {subsection}{\numberline {6.4}Flexflex equations}{26}


32 
\contentsline {section}{\numberline {7}Backward proof}{27}


33 
\contentsline {subsection}{\numberline {7.1}The basic tactics}{27}


34 
\contentsline {subsection}{\numberline {7.2}Commands for backward proof}{28}


35 
\contentsline {subsection}{\numberline {7.3}A trivial example in propositional logic}{28}


36 
\contentsline {subsection}{\numberline {7.4}Proving a distributive law}{30}


37 
\contentsline {section}{\numberline {8}Quantifier reasoning}{31}


38 
\contentsline {subsection}{\numberline {8.1}Two quantifier proofs, successful and not}{31}


39 
\contentsline {subsubsection}{The successful proof}{31}


40 
\contentsline {subsubsection}{The unsuccessful proof}{32}


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


42 
\contentsline {subsubsection}{The wrong approach}{33}


43 
\contentsline {subsubsection}{The right approach}{34}


44 
\contentsline {subsubsection}{A onestep proof using tacticals}{35}


45 
\contentsline {subsection}{\numberline {8.3}A realistic quantifier proof}{35}


46 
\contentsline {subsection}{\numberline {8.4}The classical reasoning package}{36}


47 
\contentsline {part}{\uppercase {iii}\phspace {1em}Advanced methods}{38}


48 
\contentsline {section}{\numberline {9}Deriving rules in Isabelle}{38}


49 
\contentsline {subsection}{\numberline {9.1}Deriving a rule using tactics}{38}


50 
\contentsline {subsection}{\numberline {9.2}Definitions and derived rules}{40}


51 
\contentsline {subsubsection}{Deriving the introduction rule}{41}


52 
\contentsline {subsubsection}{Deriving the elimination rule}{42}


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


54 
\contentsline {subsection}{\numberline {10.1}Declaring constants and rules}{45}


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


56 
\contentsline {subsection}{\numberline {10.3}Infixes and Mixfixes}{47}


57 
\contentsline {subsection}{\numberline {10.4}Overloading}{48}


58 
\contentsline {subsection}{\numberline {10.5}Extending firstorder logic with the natural numbers}{50}


59 
\contentsline {subsection}{\numberline {10.6}Declaring the theory to Isabelle}{51}


60 
\contentsline {section}{\numberline {11}Refinement with explicit instantiation}{52}


61 
\contentsline {subsection}{\numberline {11.1}A simple proof by induction}{52}


62 
\contentsline {subsection}{\numberline {11.2}An example of ambiguity in {\ptt resolve_tac}}{53}


63 
\contentsline {subsection}{\numberline {11.3}Proving that addition is associative}{54}


64 
\contentsline {section}{\numberline {12}A {\psc Prolog} interpreter}{55}


65 
\contentsline {subsection}{\numberline {12.1}Simple executions}{56}


66 
\contentsline {subsection}{\numberline {12.2}Backtracking}{57}


67 
\contentsline {subsection}{\numberline {12.3}Depthfirst search}{58}
