1 \contentsline {part}{\uppercase {i}\phspace {1em}Foundations}{1} |
1 \contentsline {part}{\uppercase {i}\phspace {1em}Foundations}{1} |
2 \contentsline {section}{\numberline {1}Formalizing logical syntax in Isabelle}{1} |
2 \contentsline {section}{\numberline {1}Formalizing logical syntax in Isabelle}{1} |
3 \contentsline {subsection}{\numberline {1.1}Simple types and constants}{1} |
3 \contentsline {subsection}{\numberline {1.1}Simple types and constants}{1} |
4 \contentsline {subsection}{\numberline {1.2}Polymorphic types and constants}{3} |
4 \contentsline {subsection}{\numberline {1.2}Polymorphic types and constants}{3} |
5 \contentsline {subsection}{\numberline {1.3}Higher types and quantifiers}{4} |
5 \contentsline {subsection}{\numberline {1.3}Higher types and quantifiers}{5} |
6 \contentsline {section}{\numberline {2}Formalizing logical rules in Isabelle}{5} |
6 \contentsline {section}{\numberline {2}Formalizing logical rules in Isabelle}{5} |
7 \contentsline {subsection}{\numberline {2.1}Expressing propositional rules}{6} |
7 \contentsline {subsection}{\numberline {2.1}Expressing propositional rules}{6} |
8 \contentsline {subsection}{\numberline {2.2}Quantifier rules and substitution}{7} |
8 \contentsline {subsection}{\numberline {2.2}Quantifier rules and substitution}{7} |
9 \contentsline {subsection}{\numberline {2.3}Signatures and theories}{8} |
9 \contentsline {subsection}{\numberline {2.3}Signatures and theories}{8} |
10 \contentsline {section}{\numberline {3}Proof construction in Isabelle}{9} |
10 \contentsline {section}{\numberline {3}Proof construction in Isabelle}{9} |
11 \contentsline {subsection}{\numberline {3.1}Higher-order unification}{10} |
11 \contentsline {subsection}{\numberline {3.1}Higher-order unification}{10} |
12 \contentsline {subsection}{\numberline {3.2}Joining rules by resolution}{11} |
12 \contentsline {subsection}{\numberline {3.2}Joining rules by resolution}{11} |
13 \contentsline {subsection}{\numberline {3.3}Lifting a rule into a context}{13} |
13 \contentsline {section}{\numberline {4}Lifting a rule into a context}{13} |
14 \contentsline {subsubsection}{Lifting over assumptions}{13} |
14 \contentsline {subsection}{\numberline {4.1}Lifting over assumptions}{13} |
15 \contentsline {subsubsection}{Lifting over parameters}{13} |
15 \contentsline {subsection}{\numberline {4.2}Lifting over parameters}{14} |
16 \contentsline {section}{\numberline {4}Backward proof by resolution}{14} |
16 \contentsline {section}{\numberline {5}Backward proof by resolution}{15} |
17 \contentsline {subsection}{\numberline {4.1}Refinement by resolution}{15} |
17 \contentsline {subsection}{\numberline {5.1}Refinement by resolution}{15} |
18 \contentsline {subsection}{\numberline {4.2}Proof by assumption}{15} |
18 \contentsline {subsection}{\numberline {5.2}Proof by assumption}{16} |
19 \contentsline {subsection}{\numberline {4.3}A propositional proof}{16} |
19 \contentsline {subsection}{\numberline {5.3}A propositional proof}{16} |
20 \contentsline {subsection}{\numberline {4.4}A quantifier proof}{17} |
20 \contentsline {subsection}{\numberline {5.4}A quantifier proof}{17} |
21 \contentsline {subsection}{\numberline {4.5}Tactics and tacticals}{17} |
21 \contentsline {subsection}{\numberline {5.5}Tactics and tacticals}{18} |
22 \contentsline {section}{\numberline {5}Variations on resolution}{18} |
22 \contentsline {section}{\numberline {6}Variations on resolution}{18} |
23 \contentsline {subsection}{\numberline {5.1}Elim-resolution}{18} |
23 \contentsline {subsection}{\numberline {6.1}Elim-resolution}{19} |
24 \contentsline {subsection}{\numberline {5.2}Destruction rules}{20} |
24 \contentsline {subsection}{\numberline {6.2}Destruction rules}{20} |
25 \contentsline {subsection}{\numberline {5.3}Deriving rules by resolution}{20} |
25 \contentsline {subsection}{\numberline {6.3}Deriving rules by resolution}{21} |
26 \contentsline {part}{\uppercase {ii}\phspace {1em}Getting started with Isabelle}{22} |
26 \contentsline {part}{\uppercase {ii}\phspace {1em}Getting Started with Isabelle}{23} |
27 \contentsline {section}{\numberline {6}Forward proof}{22} |
27 \contentsline {section}{\numberline {7}Forward proof}{23} |
28 \contentsline {subsection}{\numberline {6.1}Lexical matters}{22} |
28 \contentsline {subsection}{\numberline {7.1}Lexical matters}{23} |
29 \contentsline {subsection}{\numberline {6.2}Syntax of types and terms}{23} |
29 \contentsline {subsection}{\numberline {7.2}Syntax of types and terms}{24} |
30 \contentsline {subsection}{\numberline {6.3}Basic operations on theorems}{24} |
30 \contentsline {subsection}{\numberline {7.3}Basic operations on theorems}{25} |
31 \contentsline {subsection}{\numberline {6.4}Flex-flex equations}{26} |
31 \contentsline {subsection}{\numberline {7.4}*Flex-flex constraints}{27} |
32 \contentsline {section}{\numberline {7}Backward proof}{27} |
32 \contentsline {section}{\numberline {8}Backward proof}{28} |
33 \contentsline {subsection}{\numberline {7.1}The basic tactics}{27} |
33 \contentsline {subsection}{\numberline {8.1}The basic tactics}{28} |
34 \contentsline {subsection}{\numberline {7.2}Commands for backward proof}{28} |
34 \contentsline {subsection}{\numberline {8.2}Commands for backward proof}{29} |
35 \contentsline {subsection}{\numberline {7.3}A trivial example in propositional logic}{28} |
35 \contentsline {subsection}{\numberline {8.3}A trivial example in propositional logic}{29} |
36 \contentsline {subsection}{\numberline {7.4}Proving a distributive law}{30} |
36 \contentsline {subsection}{\numberline {8.4}Part of a distributive law}{31} |
37 \contentsline {section}{\numberline {8}Quantifier reasoning}{31} |
37 \contentsline {section}{\numberline {9}Quantifier reasoning}{32} |
38 \contentsline {subsection}{\numberline {8.1}Two quantifier proofs, successful and not}{31} |
38 \contentsline {subsection}{\numberline {9.1}Two quantifier proofs: a success and a failure}{32} |
39 \contentsline {subsubsection}{The successful proof}{31} |
39 \contentsline {paragraph}{The successful proof.}{32} |
40 \contentsline {subsubsection}{The unsuccessful proof}{32} |
40 \contentsline {paragraph}{The unsuccessful proof.}{33} |
41 \contentsline {subsection}{\numberline {8.2}Nested quantifiers}{33} |
41 \contentsline {subsection}{\numberline {9.2}Nested quantifiers}{33} |
42 \contentsline {subsubsection}{The wrong approach}{33} |
42 \contentsline {paragraph}{The wrong approach.}{34} |
43 \contentsline {subsubsection}{The right approach}{34} |
43 \contentsline {paragraph}{The right approach.}{34} |
44 \contentsline {subsubsection}{A one-step proof using tacticals}{35} |
44 \contentsline {paragraph}{A one-step proof using tacticals.}{35} |
45 \contentsline {subsection}{\numberline {8.3}A realistic quantifier proof}{35} |
45 \contentsline {subsection}{\numberline {9.3}A realistic quantifier proof}{36} |
46 \contentsline {subsection}{\numberline {8.4}The classical reasoning package}{36} |
46 \contentsline {subsection}{\numberline {9.4}The classical reasoner}{37} |
47 \contentsline {part}{\uppercase {iii}\phspace {1em}Advanced methods}{38} |
47 \contentsline {part}{\uppercase {iii}\phspace {1em}Advanced Methods}{39} |
48 \contentsline {section}{\numberline {9}Deriving rules in Isabelle}{38} |
48 \contentsline {section}{\numberline {10}Deriving rules in Isabelle}{39} |
49 \contentsline {subsection}{\numberline {9.1}Deriving a rule using tactics}{38} |
49 \contentsline {subsection}{\numberline {10.1}Deriving a rule using tactics and meta-level assumptions}{39} |
50 \contentsline {subsection}{\numberline {9.2}Definitions and derived rules}{40} |
50 \contentsline {subsection}{\numberline {10.2}Definitions and derived rules}{41} |
51 \contentsline {subsubsection}{Deriving the introduction rule}{41} |
51 \contentsline {subsection}{\numberline {10.3}Deriving the $\neg $ introduction rule}{41} |
52 \contentsline {subsubsection}{Deriving the elimination rule}{42} |
52 \contentsline {subsection}{\numberline {10.4}Deriving the $\neg $ elimination rule}{42} |
53 \contentsline {section}{\numberline {10}Defining theories}{44} |
53 \contentsline {section}{\numberline {11}Defining theories}{44} |
54 \contentsline {subsection}{\numberline {10.1}Declaring constants and rules}{45} |
54 \contentsline {subsection}{\numberline {11.1}Declaring constants and rules}{46} |
55 \contentsline {subsection}{\numberline {10.2}Declaring type constructors}{46} |
55 \contentsline {subsection}{\numberline {11.2}Declaring type constructors}{46} |
56 \contentsline {subsection}{\numberline {10.3}Infixes and Mixfixes}{47} |
56 \contentsline {subsection}{\numberline {11.3}Type synonyms}{48} |
57 \contentsline {subsection}{\numberline {10.4}Overloading}{48} |
57 \contentsline {subsection}{\numberline {11.4}Infix and mixfix operators}{48} |
58 \contentsline {subsection}{\numberline {10.5}Extending first-order logic with the natural numbers}{50} |
58 \contentsline {subsection}{\numberline {11.5}Overloading}{50} |
59 \contentsline {subsection}{\numberline {10.6}Declaring the theory to Isabelle}{51} |
59 \contentsline {section}{\numberline {12}Theory example: the natural numbers}{51} |
60 \contentsline {section}{\numberline {11}Refinement with explicit instantiation}{52} |
60 \contentsline {subsection}{\numberline {12.1}Extending first-order logic with the natural numbers}{51} |
61 \contentsline {subsection}{\numberline {11.1}A simple proof by induction}{52} |
61 \contentsline {subsection}{\numberline {12.2}Declaring the theory to Isabelle}{52} |
62 \contentsline {subsection}{\numberline {11.2}An example of ambiguity in {\ptt resolve_tac}}{53} |
62 \contentsline {subsection}{\numberline {12.3}Proving some recursion equations}{52} |
63 \contentsline {subsection}{\numberline {11.3}Proving that addition is associative}{54} |
63 \contentsline {section}{\numberline {13}Refinement with explicit instantiation}{53} |
64 \contentsline {section}{\numberline {12}A {\psc Prolog} interpreter}{55} |
64 \contentsline {subsection}{\numberline {13.1}A simple proof by induction}{53} |
65 \contentsline {subsection}{\numberline {12.1}Simple executions}{56} |
65 \contentsline {subsection}{\numberline {13.2}An example of ambiguity in {\ptt resolve_tac}}{54} |
66 \contentsline {subsection}{\numberline {12.2}Backtracking}{57} |
66 \contentsline {subsection}{\numberline {13.3}Proving that addition is associative}{55} |
67 \contentsline {subsection}{\numberline {12.3}Depth-first search}{58} |
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}Depth-first search}{59} |