104
|
1 |
\contentsline {chapter}{\numberline {1}Introduction}{1}
|
|
2 |
\contentsline {section}{\numberline {1.1}Basic interaction with Isabelle}{1}
|
|
3 |
\contentsline {section}{\numberline {1.2}Ending a session}{2}
|
|
4 |
\contentsline {section}{\numberline {1.3}Reading files of proofs and theories}{2}
|
|
5 |
\contentsline {section}{\numberline {1.4}Printing of terms and theorems}{2}
|
|
6 |
\contentsline {subsection}{Printing limits}{3}
|
|
7 |
\contentsline {subsection}{Printing of meta-level hypotheses}{3}
|
|
8 |
\contentsline {subsection}{Printing of types and sorts}{3}
|
|
9 |
\contentsline {subsection}{$\eta $-contraction before printing}{3}
|
|
10 |
\contentsline {section}{\numberline {1.5}Displaying exceptions as error messages}{4}
|
|
11 |
\contentsline {section}{\numberline {1.6}Shell scripts}{4}
|
|
12 |
\contentsline {chapter}{\numberline {2}Proof Management: The Subgoal Module}{6}
|
|
13 |
\contentsline {section}{\numberline {2.1}Basic commands}{6}
|
|
14 |
\contentsline {subsection}{Starting a backward proof}{6}
|
|
15 |
\contentsline {subsection}{Applying a tactic}{7}
|
|
16 |
\contentsline {subsection}{Extracting the proved theorem}{8}
|
|
17 |
\contentsline {subsection}{Undoing and backtracking}{8}
|
|
18 |
\contentsline {subsection}{Printing the proof state}{9}
|
|
19 |
\contentsline {subsection}{Timing}{9}
|
|
20 |
\contentsline {section}{\numberline {2.2}Shortcuts for applying tactics}{9}
|
|
21 |
\contentsline {subsection}{Refining a given subgoal}{9}
|
|
22 |
\contentsline {subsubsection}{Resolution with a list of theorems}{9}
|
|
23 |
\contentsline {subsection}{Scanning shortcuts}{10}
|
|
24 |
\contentsline {subsubsection}{Proof by assumption and resolution}{10}
|
|
25 |
\contentsline {subsubsection}{Resolution with a list of theorems}{10}
|
|
26 |
\contentsline {subsection}{Other shortcuts}{10}
|
|
27 |
\contentsline {section}{\numberline {2.3}Advanced features}{11}
|
|
28 |
\contentsline {subsection}{Executing batch proofs}{11}
|
|
29 |
\contentsline {subsection}{Managing multiple proofs}{11}
|
|
30 |
\contentsline {subsubsection}{The stack of proof states}{12}
|
|
31 |
\contentsline {subsubsection}{Saving and restoring proof states}{12}
|
|
32 |
\contentsline {subsection}{Debugging and inspecting}{12}
|
|
33 |
\contentsline {subsubsection}{Reading and printing terms}{13}
|
|
34 |
\contentsline {subsubsection}{Inspecting the proof state}{13}
|
|
35 |
\contentsline {subsubsection}{Filtering lists of rules}{13}
|
|
36 |
\contentsline {chapter}{\numberline {3}Tactics}{14}
|
|
37 |
\contentsline {section}{\numberline {3.1}Resolution and assumption tactics}{14}
|
|
38 |
\contentsline {subsection}{Resolution tactics}{14}
|
|
39 |
\contentsline {subsection}{Assumption tactics}{15}
|
|
40 |
\contentsline {subsection}{Matching tactics}{15}
|
|
41 |
\contentsline {subsection}{Resolution with instantiation}{15}
|
|
42 |
\contentsline {section}{\numberline {3.2}Other basic tactics}{16}
|
|
43 |
\contentsline {subsection}{Definitions and meta-level rewriting}{16}
|
|
44 |
\contentsline {subsection}{Tactic shortcuts}{17}
|
|
45 |
\contentsline {subsection}{Inserting premises and facts}{17}
|
|
46 |
\contentsline {subsection}{Theorems useful with tactics}{18}
|
|
47 |
\contentsline {section}{\numberline {3.3}Obscure tactics}{18}
|
|
48 |
\contentsline {subsection}{Tidying the proof state}{18}
|
|
49 |
\contentsline {subsection}{Renaming parameters in a goal}{18}
|
|
50 |
\contentsline {subsection}{Composition: resolution without lifting}{19}
|
|
51 |
\contentsline {section}{\numberline {3.4}Managing lots of rules}{19}
|
|
52 |
\contentsline {subsection}{Combined resolution and elim-resolution}{20}
|
|
53 |
\contentsline {subsection}{Discrimination nets for fast resolution}{20}
|
|
54 |
\contentsline {section}{\numberline {3.5}Programming tools for proof strategies}{21}
|
|
55 |
\contentsline {subsection}{Operations on type {\ptt tactic}}{22}
|
|
56 |
\contentsline {subsection}{Tracing}{22}
|
|
57 |
\contentsline {subsection}{Sequences}{23}
|
|
58 |
\contentsline {subsubsection}{Basic operations on sequences}{23}
|
|
59 |
\contentsline {subsubsection}{Converting between sequences and lists}{23}
|
|
60 |
\contentsline {subsubsection}{Combining sequences}{23}
|
|
61 |
\contentsline {chapter}{\numberline {4}Tacticals}{25}
|
|
62 |
\contentsline {section}{\numberline {4.1}The basic tacticals}{25}
|
|
63 |
\contentsline {subsection}{Joining two tactics}{25}
|
|
64 |
\contentsline {subsection}{Joining a list of tactics}{25}
|
|
65 |
\contentsline {subsection}{Repetition tacticals}{26}
|
|
66 |
\contentsline {subsection}{Identities for tacticals}{26}
|
|
67 |
\contentsline {section}{\numberline {4.2}Control and search tacticals}{27}
|
|
68 |
\contentsline {subsection}{Filtering a tactic's results}{27}
|
|
69 |
\contentsline {subsection}{Depth-first search}{28}
|
|
70 |
\contentsline {subsection}{Other search strategies}{28}
|
|
71 |
\contentsline {subsection}{Auxiliary tacticals for searching}{29}
|
|
72 |
\contentsline {subsection}{Predicates and functions useful for searching}{29}
|
|
73 |
\contentsline {section}{\numberline {4.3}Tacticals for subgoal numbering}{29}
|
|
74 |
\contentsline {subsection}{Restricting a tactic to one subgoal}{30}
|
|
75 |
\contentsline {subsection}{Scanning for a subgoal by number}{31}
|
|
76 |
\contentsline {subsection}{Joining tactic functions}{32}
|
|
77 |
\contentsline {subsection}{Applying a list of tactics to 1}{32}
|
|
78 |
\contentsline {chapter}{\numberline {5}Theorems and Forward Proof}{33}
|
|
79 |
\contentsline {section}{\numberline {5.1}Basic operations on theorems}{33}
|
|
80 |
\contentsline {subsection}{Pretty-printing a theorem}{33}
|
|
81 |
\contentsline {subsubsection}{Top-level commands}{33}
|
|
82 |
\contentsline {subsubsection}{Operations for programming}{34}
|
|
83 |
\contentsline {subsection}{Forwards proof: joining rules by resolution}{34}
|
|
84 |
\contentsline {subsection}{Expanding definitions in theorems}{35}
|
|
85 |
\contentsline {subsection}{Instantiating a theorem}{35}
|
|
86 |
\contentsline {subsection}{Miscellaneous forward rules}{35}
|
|
87 |
\contentsline {subsection}{Taking a theorem apart}{36}
|
|
88 |
\contentsline {subsection}{Tracing flags for unification}{36}
|
|
89 |
\contentsline {section}{\numberline {5.2}Primitive meta-level inference rules}{37}
|
|
90 |
\contentsline {subsection}{Propositional rules}{38}
|
|
91 |
\contentsline {subsubsection}{Assumption}{38}
|
|
92 |
\contentsline {subsubsection}{Implication}{38}
|
|
93 |
\contentsline {subsubsection}{Logical equivalence (equality)}{39}
|
|
94 |
\contentsline {subsection}{Equality rules}{39}
|
|
95 |
\contentsline {subsection}{The $\lambda $-conversion rules}{39}
|
|
96 |
\contentsline {subsection}{Universal quantifier rules}{40}
|
|
97 |
\contentsline {subsubsection}{Forall introduction}{40}
|
|
98 |
\contentsline {subsubsection}{Forall elimination}{40}
|
|
99 |
\contentsline {subsubsection}{Instantiation of unknowns}{41}
|
|
100 |
\contentsline {subsection}{Freezing/thawing type variables}{41}
|
|
101 |
\contentsline {section}{\numberline {5.3}Derived rules for goal-directed proof}{41}
|
|
102 |
\contentsline {subsection}{Proof by assumption}{41}
|
|
103 |
\contentsline {subsection}{Resolution}{41}
|
|
104 |
\contentsline {subsection}{Composition: resolution without lifting}{42}
|
|
105 |
\contentsline {subsection}{Other meta-rules}{42}
|
|
106 |
\contentsline {chapter}{\numberline {6}Theories, Terms and Types}{44}
|
|
107 |
\contentsline {section}{\numberline {6.1}Defining Theories}{44}
|
|
108 |
\contentsline {section}{\numberline {6.2}Basic operations on theories}{47}
|
|
109 |
\contentsline {subsection}{Extracting an axiom from a theory}{47}
|
|
110 |
\contentsline {subsection}{Building a theory}{47}
|
|
111 |
\contentsline {subsection}{Inspecting a theory}{48}
|
|
112 |
\contentsline {section}{\numberline {6.3}Terms}{49}
|
|
113 |
\contentsline {section}{\numberline {6.4}Certified terms}{50}
|
|
114 |
\contentsline {subsection}{Printing terms}{50}
|
|
115 |
\contentsline {subsection}{Making and inspecting certified terms}{50}
|
|
116 |
\contentsline {section}{\numberline {6.5}Types}{51}
|
|
117 |
\contentsline {section}{\numberline {6.6}Certified types}{51}
|
|
118 |
\contentsline {subsection}{Printing types}{51}
|
|
119 |
\contentsline {subsection}{Making and inspecting certified types}{51}
|
|
120 |
\contentsline {chapter}{\numberline {7}Substitution Tactics}{53}
|
|
121 |
\contentsline {section}{\numberline {7.1}Simple substitution}{53}
|
|
122 |
\contentsline {section}{\numberline {7.2}Substitution in the hypotheses}{54}
|
|
123 |
\contentsline {section}{\numberline {7.3}Setting up {\ptt hyp_subst_tac}}{54}
|
|
124 |
\contentsline {chapter}{\numberline {8}Simplification}{57}
|
|
125 |
\contentsline {section}{\numberline {8.1}Simplification sets}{57}
|
|
126 |
\contentsline {subsection}{Rewrite rules}{57}
|
|
127 |
\contentsline {subsection}{Congruence rules}{58}
|
|
128 |
\contentsline {subsection}{The subgoaler}{58}
|
|
129 |
\contentsline {subsection}{The solver}{59}
|
|
130 |
\contentsline {subsection}{The looper}{59}
|
|
131 |
\contentsline {section}{\numberline {8.2}The simplification tactics}{59}
|
|
132 |
\contentsline {section}{\numberline {8.3}Example: using the simplifier}{60}
|
|
133 |
\contentsline {chapter}{\numberline {9}The classical theorem prover}{64}
|
|
134 |
\contentsline {section}{\numberline {9.1}The sequent calculus}{64}
|
|
135 |
\contentsline {section}{\numberline {9.2}Simulating sequents by natural deduction}{65}
|
|
136 |
\contentsline {section}{\numberline {9.3}Extra rules for the sequent calculus}{66}
|
|
137 |
\contentsline {section}{\numberline {9.4}Classical rule sets}{67}
|
|
138 |
\contentsline {section}{\numberline {9.5}The classical tactics}{68}
|
|
139 |
\contentsline {subsection}{Single-step tactics}{69}
|
|
140 |
\contentsline {subsection}{The automatic tactics}{69}
|
|
141 |
\contentsline {subsection}{Other useful tactics}{69}
|
|
142 |
\contentsline {subsection}{Creating swapped rules}{70}
|
|
143 |
\contentsline {section}{\numberline {9.6}Setting up the classical prover}{70}
|