doc-src/Intro/intro.toc
changeset 105 216d6ed87399
child 359 b5a2e9503a7a
equal deleted inserted replaced
104:d8205bb279a7 105:216d6ed87399
       
     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}Higher-order 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}Elim-resolution}{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}Flex-flex 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 one-step 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 first-order 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}Depth-first search}{58}