doc-src/Intro/intro.toc
 author lcp Tue, 03 May 1994 18:38:28 +0200 changeset 359 b5a2e9503a7a parent 105 216d6ed87399 child 1085 504dad4d7843 permissions -rw-r--r--
final Springer version
```
\contentsline {part}{\uppercase {i}\phspace {1em}Foundations}{1}
\contentsline {section}{\numberline {1}Formalizing logical syntax in Isabelle}{1}
\contentsline {subsection}{\numberline {1.1}Simple types and constants}{1}
\contentsline {subsection}{\numberline {1.2}Polymorphic types and constants}{3}
\contentsline {subsection}{\numberline {1.3}Higher types and quantifiers}{5}
\contentsline {section}{\numberline {2}Formalizing logical rules in Isabelle}{5}
\contentsline {subsection}{\numberline {2.1}Expressing propositional rules}{6}
\contentsline {subsection}{\numberline {2.2}Quantifier rules and substitution}{7}
\contentsline {subsection}{\numberline {2.3}Signatures and theories}{8}
\contentsline {section}{\numberline {3}Proof construction in Isabelle}{9}
\contentsline {subsection}{\numberline {3.1}Higher-order unification}{10}
\contentsline {subsection}{\numberline {3.2}Joining rules by resolution}{11}
\contentsline {section}{\numberline {4}Lifting a rule into a context}{13}
\contentsline {subsection}{\numberline {4.1}Lifting over assumptions}{13}
\contentsline {subsection}{\numberline {4.2}Lifting over parameters}{14}
\contentsline {section}{\numberline {5}Backward proof by resolution}{15}
\contentsline {subsection}{\numberline {5.1}Refinement by resolution}{15}
\contentsline {subsection}{\numberline {5.2}Proof by assumption}{16}
\contentsline {subsection}{\numberline {5.3}A propositional proof}{16}
\contentsline {subsection}{\numberline {5.4}A quantifier proof}{17}
\contentsline {subsection}{\numberline {5.5}Tactics and tacticals}{18}
\contentsline {section}{\numberline {6}Variations on resolution}{18}
\contentsline {subsection}{\numberline {6.1}Elim-resolution}{19}
\contentsline {subsection}{\numberline {6.2}Destruction rules}{20}
\contentsline {subsection}{\numberline {6.3}Deriving rules by resolution}{21}
\contentsline {part}{\uppercase {ii}\phspace {1em}Getting Started with Isabelle}{23}
\contentsline {section}{\numberline {7}Forward proof}{23}
\contentsline {subsection}{\numberline {7.1}Lexical matters}{23}
\contentsline {subsection}{\numberline {7.2}Syntax of types and terms}{24}
\contentsline {subsection}{\numberline {7.3}Basic operations on theorems}{25}
\contentsline {subsection}{\numberline {7.4}*Flex-flex constraints}{27}
\contentsline {section}{\numberline {8}Backward proof}{28}
\contentsline {subsection}{\numberline {8.1}The basic tactics}{28}
\contentsline {subsection}{\numberline {8.2}Commands for backward proof}{29}
\contentsline {subsection}{\numberline {8.3}A trivial example in propositional logic}{29}
\contentsline {subsection}{\numberline {8.4}Part of a distributive law}{31}
\contentsline {section}{\numberline {9}Quantifier reasoning}{32}
\contentsline {subsection}{\numberline {9.1}Two quantifier proofs: a success and a failure}{32}
\contentsline {paragraph}{The successful proof.}{32}
\contentsline {paragraph}{The unsuccessful proof.}{33}
\contentsline {subsection}{\numberline {9.2}Nested quantifiers}{33}
\contentsline {paragraph}{The wrong approach.}{34}
\contentsline {paragraph}{The right approach.}{34}
\contentsline {paragraph}{A one-step proof using tacticals.}{35}
\contentsline {subsection}{\numberline {9.3}A realistic quantifier proof}{36}
\contentsline {subsection}{\numberline {9.4}The classical reasoner}{37}
\contentsline {section}{\numberline {10}Deriving rules in Isabelle}{39}
\contentsline {subsection}{\numberline {10.1}Deriving a rule using tactics and meta-level assumptions}{39}
\contentsline {subsection}{\numberline {10.2}Definitions and derived rules}{41}
\contentsline {subsection}{\numberline {10.3}Deriving the \$\neg \$ introduction rule}{41}
\contentsline {subsection}{\numberline {10.4}Deriving the \$\neg \$ elimination rule}{42}
\contentsline {section}{\numberline {11}Defining theories}{44}
\contentsline {subsection}{\numberline {11.1}Declaring constants and rules}{46}
\contentsline {subsection}{\numberline {11.2}Declaring type constructors}{46}
\contentsline {subsection}{\numberline {11.3}Type synonyms}{48}
\contentsline {subsection}{\numberline {11.4}Infix and mixfix operators}{48}