1 \contentsline {chapter}{\numberline {1}Introduction}{1} |
1 \contentsline {chapter}{\numberline {1}Basic Use of Isabelle}{1} |
2 \contentsline {section}{\numberline {1.1}Basic interaction with Isabelle}{1} |
2 \contentsline {section}{\numberline {1.1}Basic interaction with Isabelle}{1} |
3 \contentsline {section}{\numberline {1.2}Ending a session}{2} |
3 \contentsline {section}{\numberline {1.2}Ending a session}{2} |
4 \contentsline {section}{\numberline {1.3}Reading files of proofs and theories}{2} |
4 \contentsline {section}{\numberline {1.3}Reading ML files}{2} |
5 \contentsline {section}{\numberline {1.4}Printing of terms and theorems}{3} |
5 \contentsline {section}{\numberline {1.4}Printing of terms and theorems}{2} |
6 \contentsline {subsection}{Printing limits}{3} |
6 \contentsline {subsection}{Printing limits}{2} |
7 \contentsline {subsection}{Printing of meta-level hypotheses}{3} |
7 \contentsline {subsection}{Printing of hypotheses, types and sorts}{3} |
8 \contentsline {subsection}{Printing of types and sorts}{3} |
8 \contentsline {subsection}{$\eta $-contraction before printing}{3} |
9 \contentsline {subsection}{$\eta $-contraction before printing}{4} |
9 \contentsline {section}{\numberline {1.5}Displaying exceptions as error messages}{3} |
10 \contentsline {section}{\numberline {1.5}Displaying exceptions as error messages}{4} |
10 \contentsline {section}{\numberline {1.6}Shell scripts}{4} |
11 \contentsline {section}{\numberline {1.6}Shell scripts}{5} |
11 \contentsline {chapter}{\numberline {2}Proof Management: The Subgoal Module}{5} |
12 \contentsline {chapter}{\numberline {2}Proof Management: The Subgoal Module}{6} |
12 \contentsline {section}{\numberline {2.1}Basic commands}{5} |
13 \contentsline {section}{\numberline {2.1}Basic commands}{6} |
13 \contentsline {subsection}{Starting a backward proof}{5} |
14 \contentsline {subsection}{Starting a backward proof}{6} |
14 \contentsline {subsection}{Applying a tactic}{6} |
15 \contentsline {subsection}{Applying a tactic}{7} |
15 \contentsline {subsection}{Extracting the proved theorem}{7} |
16 \contentsline {subsection}{Extracting the proved theorem}{8} |
16 \contentsline {subsection}{Undoing and backtracking}{7} |
17 \contentsline {subsection}{Undoing and backtracking}{8} |
17 \contentsline {subsection}{Printing the proof state}{8} |
18 \contentsline {subsection}{Printing the proof state}{9} |
18 \contentsline {subsection}{Timing}{8} |
19 \contentsline {subsection}{Timing}{9} |
19 \contentsline {section}{\numberline {2.2}Shortcuts for applying tactics}{8} |
20 \contentsline {section}{\numberline {2.2}Shortcuts for applying tactics}{9} |
20 \contentsline {subsection}{Refining a given subgoal}{8} |
21 \contentsline {subsection}{Refining a given subgoal}{9} |
21 \contentsline {subsection}{Scanning shortcuts}{9} |
22 \contentsline {subsubsection}{Resolution with a list of theorems}{9} |
22 \contentsline {subsection}{Other shortcuts}{9} |
23 \contentsline {subsection}{Scanning shortcuts}{10} |
23 \contentsline {section}{\numberline {2.3}Executing batch proofs}{9} |
24 \contentsline {subsubsection}{Proof by assumption and resolution}{10} |
24 \contentsline {section}{\numberline {2.4}Managing multiple proofs}{10} |
25 \contentsline {subsubsection}{Resolution with a list of theorems}{10} |
25 \contentsline {subsection}{The stack of proof states}{11} |
26 \contentsline {subsection}{Other shortcuts}{10} |
26 \contentsline {subsection}{Saving and restoring proof states}{11} |
27 \contentsline {section}{\numberline {2.3}Advanced features}{11} |
27 \contentsline {section}{\numberline {2.5}Debugging and inspecting}{11} |
28 \contentsline {subsection}{Executing batch proofs}{11} |
28 \contentsline {subsection}{Reading and printing terms}{11} |
29 \contentsline {subsection}{Managing multiple proofs}{11} |
29 \contentsline {subsection}{Inspecting the proof state}{12} |
30 \contentsline {subsubsection}{The stack of proof states}{12} |
30 \contentsline {subsection}{Filtering lists of rules}{12} |
31 \contentsline {subsubsection}{Saving and restoring proof states}{12} |
31 \contentsline {chapter}{\numberline {3}Tactics}{13} |
32 \contentsline {subsection}{Debugging and inspecting}{12} |
32 \contentsline {section}{\numberline {3.1}Resolution and assumption tactics}{13} |
33 \contentsline {subsubsection}{Reading and printing terms}{13} |
33 \contentsline {subsection}{Resolution tactics}{13} |
34 \contentsline {subsubsection}{Inspecting the proof state}{13} |
34 \contentsline {subsection}{Assumption tactics}{14} |
35 \contentsline {subsubsection}{Filtering lists of rules}{13} |
35 \contentsline {subsection}{Matching tactics}{14} |
36 \contentsline {chapter}{\numberline {3}Tactics}{14} |
36 \contentsline {subsection}{Resolution with instantiation}{14} |
37 \contentsline {section}{\numberline {3.1}Resolution and assumption tactics}{14} |
37 \contentsline {section}{\numberline {3.2}Other basic tactics}{15} |
38 \contentsline {subsection}{Resolution tactics}{14} |
38 \contentsline {subsection}{Definitions and meta-level rewriting}{15} |
39 \contentsline {subsection}{Assumption tactics}{15} |
39 \contentsline {subsection}{Tactic shortcuts}{16} |
40 \contentsline {subsection}{Matching tactics}{15} |
40 \contentsline {subsection}{Inserting premises and facts}{16} |
41 \contentsline {subsection}{Resolution with instantiation}{15} |
41 \contentsline {subsection}{Theorems useful with tactics}{17} |
42 \contentsline {section}{\numberline {3.2}Other basic tactics}{16} |
42 \contentsline {section}{\numberline {3.3}Obscure tactics}{17} |
43 \contentsline {subsection}{Definitions and meta-level rewriting}{16} |
43 \contentsline {subsection}{Tidying the proof state}{17} |
44 \contentsline {subsection}{Tactic shortcuts}{17} |
44 \contentsline {subsection}{Renaming parameters in a goal}{17} |
45 \contentsline {subsection}{Inserting premises and facts}{17} |
45 \contentsline {subsection}{Composition: resolution without lifting}{18} |
46 \contentsline {subsection}{Theorems useful with tactics}{18} |
46 \contentsline {section}{\numberline {3.4}Managing lots of rules}{18} |
47 \contentsline {section}{\numberline {3.3}Obscure tactics}{18} |
47 \contentsline {subsection}{Combined resolution and elim-resolution}{19} |
48 \contentsline {subsection}{Tidying the proof state}{18} |
48 \contentsline {subsection}{Discrimination nets for fast resolution}{19} |
49 \contentsline {subsection}{Renaming parameters in a goal}{18} |
49 \contentsline {section}{\numberline {3.5}Programming tools for proof strategies}{20} |
50 \contentsline {subsection}{Composition: resolution without lifting}{19} |
50 \contentsline {subsection}{Operations on type {\ptt tactic}}{21} |
51 \contentsline {section}{\numberline {3.4}Managing lots of rules}{19} |
51 \contentsline {subsection}{Tracing}{21} |
52 \contentsline {subsection}{Combined resolution and elim-resolution}{20} |
52 \contentsline {section}{\numberline {3.6}Sequences}{22} |
53 \contentsline {subsection}{Discrimination nets for fast resolution}{20} |
53 \contentsline {subsection}{Basic operations on sequences}{22} |
54 \contentsline {section}{\numberline {3.5}Programming tools for proof strategies}{21} |
54 \contentsline {subsection}{Converting between sequences and lists}{22} |
55 \contentsline {subsection}{Operations on type {\ptt tactic}}{22} |
55 \contentsline {subsection}{Combining sequences}{22} |
56 \contentsline {subsection}{Tracing}{22} |
56 \contentsline {chapter}{\numberline {4}Tacticals}{24} |
57 \contentsline {subsection}{Sequences}{23} |
57 \contentsline {section}{\numberline {4.1}The basic tacticals}{24} |
58 \contentsline {subsubsection}{Basic operations on sequences}{23} |
58 \contentsline {subsection}{Joining two tactics}{24} |
59 \contentsline {subsubsection}{Converting between sequences and lists}{23} |
59 \contentsline {subsection}{Joining a list of tactics}{24} |
60 \contentsline {subsubsection}{Combining sequences}{23} |
60 \contentsline {subsection}{Repetition tacticals}{25} |
61 \contentsline {chapter}{\numberline {4}Tacticals}{25} |
61 \contentsline {subsection}{Identities for tacticals}{25} |
62 \contentsline {section}{\numberline {4.1}The basic tacticals}{25} |
62 \contentsline {section}{\numberline {4.2}Control and search tacticals}{26} |
63 \contentsline {subsection}{Joining two tactics}{25} |
63 \contentsline {subsection}{Filtering a tactic's results}{26} |
64 \contentsline {subsection}{Joining a list of tactics}{25} |
64 \contentsline {subsection}{Depth-first search}{26} |
65 \contentsline {subsection}{Repetition tacticals}{26} |
65 \contentsline {subsection}{Other search strategies}{27} |
66 \contentsline {subsection}{Identities for tacticals}{26} |
66 \contentsline {subsection}{Auxiliary tacticals for searching}{27} |
67 \contentsline {section}{\numberline {4.2}Control and search tacticals}{27} |
67 \contentsline {subsection}{Predicates and functions useful for searching}{28} |
68 \contentsline {subsection}{Filtering a tactic's results}{27} |
68 \contentsline {section}{\numberline {4.3}Tacticals for subgoal numbering}{28} |
69 \contentsline {subsection}{Depth-first search}{28} |
69 \contentsline {subsection}{Restricting a tactic to one subgoal}{28} |
70 \contentsline {subsection}{Other search strategies}{28} |
70 \contentsline {subsection}{Scanning for a subgoal by number}{29} |
71 \contentsline {subsection}{Auxiliary tacticals for searching}{29} |
71 \contentsline {subsection}{Joining tactic functions}{30} |
72 \contentsline {subsection}{Predicates and functions useful for searching}{29} |
72 \contentsline {subsection}{Applying a list of tactics to 1}{31} |
73 \contentsline {section}{\numberline {4.3}Tacticals for subgoal numbering}{29} |
73 \contentsline {chapter}{\numberline {5}Theorems and Forward Proof}{32} |
74 \contentsline {subsection}{Restricting a tactic to one subgoal}{30} |
74 \contentsline {section}{\numberline {5.1}Basic operations on theorems}{32} |
75 \contentsline {subsection}{Scanning for a subgoal by number}{31} |
75 \contentsline {subsection}{Pretty-printing a theorem}{32} |
76 \contentsline {subsection}{Joining tactic functions}{32} |
76 \contentsline {subsection}{Forward proof: joining rules by resolution}{33} |
77 \contentsline {subsection}{Applying a list of tactics to 1}{32} |
77 \contentsline {subsection}{Expanding definitions in theorems}{33} |
78 \contentsline {chapter}{\numberline {5}Theorems and Forward Proof}{33} |
78 \contentsline {subsection}{Instantiating a theorem}{34} |
79 \contentsline {section}{\numberline {5.1}Basic operations on theorems}{33} |
79 \contentsline {subsection}{Miscellaneous forward rules}{34} |
80 \contentsline {subsection}{Pretty-printing a theorem}{33} |
80 \contentsline {subsection}{Taking a theorem apart}{35} |
81 \contentsline {subsubsection}{Top-level commands}{33} |
81 \contentsline {subsection}{Tracing flags for unification}{35} |
82 \contentsline {subsubsection}{Operations for programming}{34} |
82 \contentsline {section}{\numberline {5.2}Primitive meta-level inference rules}{36} |
83 \contentsline {subsection}{Forwards proof: joining rules by resolution}{34} |
83 \contentsline {subsection}{Assumption rule}{37} |
84 \contentsline {subsection}{Expanding definitions in theorems}{35} |
84 \contentsline {subsection}{Implication rules}{37} |
85 \contentsline {subsection}{Instantiating a theorem}{35} |
85 \contentsline {subsection}{Logical equivalence rules}{38} |
86 \contentsline {subsection}{Miscellaneous forward rules}{35} |
86 \contentsline {subsection}{Equality rules}{38} |
87 \contentsline {subsection}{Taking a theorem apart}{36} |
87 \contentsline {subsection}{The $\lambda $-conversion rules}{38} |
88 \contentsline {subsection}{Tracing flags for unification}{36} |
88 \contentsline {subsection}{Forall introduction rules}{39} |
89 \contentsline {section}{\numberline {5.2}Primitive meta-level inference rules}{37} |
89 \contentsline {subsection}{Forall elimination rules}{39} |
90 \contentsline {subsection}{Propositional rules}{38} |
90 \contentsline {subsection}{Instantiation of unknowns}{39} |
91 \contentsline {subsubsection}{Assumption}{38} |
91 \contentsline {subsection}{Freezing/thawing type unknowns}{40} |
92 \contentsline {subsubsection}{Implication}{38} |
92 \contentsline {section}{\numberline {5.3}Derived rules for goal-directed proof}{40} |
93 \contentsline {subsubsection}{Logical equivalence (equality)}{39} |
93 \contentsline {subsection}{Proof by assumption}{40} |
94 \contentsline {subsection}{Equality rules}{39} |
94 \contentsline {subsection}{Resolution}{40} |
95 \contentsline {subsection}{The $\lambda $-conversion rules}{39} |
95 \contentsline {subsection}{Composition: resolution without lifting}{40} |
96 \contentsline {subsection}{Universal quantifier rules}{40} |
96 \contentsline {subsection}{Other meta-rules}{41} |
97 \contentsline {subsubsection}{Forall introduction}{40} |
97 \contentsline {chapter}{\numberline {6}Theories, Terms and Types}{42} |
98 \contentsline {subsubsection}{Forall elimination}{40} |
98 \contentsline {section}{\numberline {6.1}Defining theories}{42} |
99 \contentsline {subsubsection}{Instantiation of unknowns}{41} |
99 \contentsline {subsection}{*Classes and arities}{44} |
100 \contentsline {subsection}{Freezing/thawing type variables}{41} |
100 \contentsline {section}{\numberline {6.2}Loading a new theory}{44} |
101 \contentsline {section}{\numberline {5.3}Derived rules for goal-directed proof}{41} |
101 \contentsline {section}{\numberline {6.3}Reloading modified theories}{45} |
102 \contentsline {subsection}{Proof by assumption}{41} |
102 \contentsline {subsection}{Important note for Poly/ML users}{45} |
103 \contentsline {subsection}{Resolution}{41} |
103 \contentsline {subsection}{*Pseudo theories}{46} |
104 \contentsline {subsection}{Composition: resolution without lifting}{42} |
104 \contentsline {section}{\numberline {6.4}Basic operations on theories}{47} |
105 \contentsline {subsection}{Other meta-rules}{42} |
105 \contentsline {subsection}{Extracting an axiom from a theory}{47} |
106 \contentsline {chapter}{\numberline {6}Theories, Terms and Types}{44} |
106 \contentsline {subsection}{Building a theory}{47} |
107 \contentsline {section}{\numberline {6.1}Defining Theories}{44} |
107 \contentsline {subsection}{Inspecting a theory}{47} |
108 \contentsline {subsection}{Classes and types}{47} |
108 \contentsline {section}{\numberline {6.5}Terms}{48} |
109 \contentsline {section}{\numberline {6.2}Loading Theories}{47} |
109 \contentsline {section}{\numberline {6.6}Variable binding}{49} |
110 \contentsline {subsection}{Reading a new theory}{47} |
110 \contentsline {section}{\numberline {6.7}Certified terms}{50} |
111 \contentsline {subsection}{Filenames and paths}{48} |
111 \contentsline {subsection}{Printing terms}{50} |
112 \contentsline {subsection}{Reloading a theory}{48} |
112 \contentsline {subsection}{Making and inspecting certified terms}{50} |
113 \contentsline {subsection}{Pseudo theories}{48} |
113 \contentsline {section}{\numberline {6.8}Types}{50} |
114 \contentsline {subsection}{Removing a theory}{49} |
114 \contentsline {section}{\numberline {6.9}Certified types}{51} |
115 \contentsline {subsection}{Using Poly/{\psc ml}}{49} |
115 \contentsline {subsection}{Printing types}{51} |
116 \contentsline {section}{\numberline {6.3}Basic operations on theories}{49} |
116 \contentsline {subsection}{Making and inspecting certified types}{51} |
117 \contentsline {subsection}{Extracting an axiom from a theory}{49} |
117 \contentsline {chapter}{\numberline {7}Defining Logics}{52} |
118 \contentsline {subsection}{Building a theory}{50} |
118 \contentsline {section}{\numberline {7.1}Priority grammars}{52} |
119 \contentsline {subsection}{Inspecting a theory}{51} |
119 \contentsline {section}{\numberline {7.2}The Pure syntax}{53} |
120 \contentsline {section}{\numberline {6.4}Terms}{52} |
120 \contentsline {subsection}{Logical types and default syntax}{55} |
121 \contentsline {section}{\numberline {6.5}Certified terms}{53} |
121 \contentsline {subsection}{Lexical matters}{55} |
122 \contentsline {subsection}{Printing terms}{53} |
122 \contentsline {subsection}{*Inspecting the syntax}{56} |
123 \contentsline {subsection}{Making and inspecting certified terms}{53} |
123 \contentsline {section}{\numberline {7.3}Mixfix declarations}{58} |
124 \contentsline {section}{\numberline {6.6}Types}{54} |
124 \contentsline {subsection}{Grammar productions}{58} |
125 \contentsline {section}{\numberline {6.7}Certified types}{54} |
125 \contentsline {subsection}{The general mixfix form}{59} |
126 \contentsline {subsection}{Printing types}{54} |
126 \contentsline {subsection}{Example: arithmetic expressions}{60} |
127 \contentsline {subsection}{Making and inspecting certified types}{54} |
127 \contentsline {subsection}{The mixfix template}{61} |
128 \contentsline {chapter}{\numberline {7}Substitution Tactics}{56} |
128 \contentsline {subsection}{Infixes}{61} |
129 \contentsline {section}{\numberline {7.1}Simple substitution}{56} |
129 \contentsline {subsection}{Binders}{62} |
130 \contentsline {section}{\numberline {7.2}Substitution in the hypotheses}{57} |
130 \contentsline {section}{\numberline {7.4}Example: some minimal logics}{62} |
131 \contentsline {section}{\numberline {7.3}Setting up {\ptt hyp_subst_tac}}{57} |
131 \contentsline {chapter}{\numberline {8}Syntax Transformations}{66} |
132 \contentsline {chapter}{\numberline {8}Simplification}{60} |
132 \contentsline {section}{\numberline {8.1}Abstract syntax trees}{66} |
133 \contentsline {section}{\numberline {8.1}Simplification sets}{60} |
133 \contentsline {section}{\numberline {8.2}Transforming parse trees to {\psc ast}{}s}{67} |
134 \contentsline {subsection}{Rewrite rules}{60} |
134 \contentsline {section}{\numberline {8.3}Transforming {\psc ast}{}s to terms}{69} |
135 \contentsline {subsection}{Congruence rules}{61} |
135 \contentsline {section}{\numberline {8.4}Printing of terms}{69} |
136 \contentsline {subsection}{The subgoaler}{61} |
136 \contentsline {section}{\numberline {8.5}Macros: Syntactic rewriting}{71} |
137 \contentsline {subsection}{The solver}{62} |
137 \contentsline {subsection}{Specifying macros}{72} |
138 \contentsline {subsection}{The looper}{62} |
138 \contentsline {subsection}{Applying rules}{73} |
139 \contentsline {section}{\numberline {8.2}The simplification tactics}{62} |
139 \contentsline {subsection}{Example: the syntax of finite sets}{75} |
140 \contentsline {section}{\numberline {8.3}Example: using the simplifier}{63} |
140 \contentsline {subsection}{Example: a parse macro for dependent types}{76} |
141 \contentsline {chapter}{\numberline {9}The classical theorem prover}{67} |
141 \contentsline {section}{\numberline {8.6}Translation functions}{76} |
142 \contentsline {section}{\numberline {9.1}The sequent calculus}{67} |
142 \contentsline {subsection}{Declaring translation functions}{77} |
143 \contentsline {section}{\numberline {9.2}Simulating sequents by natural deduction}{68} |
143 \contentsline {subsection}{The translation strategy}{77} |
144 \contentsline {section}{\numberline {9.3}Extra rules for the sequent calculus}{69} |
144 \contentsline {subsection}{Example: a print translation for dependent types}{78} |
145 \contentsline {section}{\numberline {9.4}Classical rule sets}{70} |
145 \contentsline {chapter}{\numberline {9}Substitution Tactics}{80} |
146 \contentsline {section}{\numberline {9.5}The classical tactics}{71} |
146 \contentsline {section}{\numberline {9.1}Substitution rules}{80} |
147 \contentsline {subsection}{Single-step tactics}{72} |
147 \contentsline {section}{\numberline {9.2}Substitution in the hypotheses}{81} |
148 \contentsline {subsection}{The automatic tactics}{72} |
148 \contentsline {section}{\numberline {9.3}Setting up {\ptt hyp_subst_tac}}{82} |
149 \contentsline {subsection}{Other useful tactics}{72} |
149 \contentsline {chapter}{\numberline {10}Simplification}{84} |
150 \contentsline {subsection}{Creating swapped rules}{73} |
150 \contentsline {section}{\numberline {10.1}Simplification sets}{84} |
151 \contentsline {section}{\numberline {9.6}Setting up the classical prover}{73} |
151 \contentsline {subsection}{Rewrite rules}{84} |
|
152 \contentsline {subsection}{*Congruence rules}{85} |
|
153 \contentsline {subsection}{*The subgoaler}{85} |
|
154 \contentsline {subsection}{*The solver}{86} |
|
155 \contentsline {subsection}{*The looper}{86} |
|
156 \contentsline {section}{\numberline {10.2}The simplification tactics}{87} |
|
157 \contentsline {section}{\numberline {10.3}Examples using the simplifier}{88} |
|
158 \contentsline {subsection}{A trivial example}{88} |
|
159 \contentsline {subsection}{An example of tracing}{89} |
|
160 \contentsline {subsection}{Free variables and simplification}{90} |
|
161 \contentsline {section}{\numberline {10.4}Permutative rewrite rules}{90} |
|
162 \contentsline {subsection}{Example: sums of integers}{91} |
|
163 \contentsline {subsection}{Re-orienting equalities}{93} |
|
164 \contentsline {section}{\numberline {10.5}*Setting up the simplifier}{93} |
|
165 \contentsline {subsection}{A collection of standard rewrite rules}{94} |
|
166 \contentsline {subsection}{Functions for preprocessing the rewrite rules}{94} |
|
167 \contentsline {subsection}{Making the initial simpset}{96} |
|
168 \contentsline {subsection}{Case splitting}{97} |
|
169 \contentsline {chapter}{\numberline {11}The Classical Reasoner}{98} |
|
170 \contentsline {section}{\numberline {11.1}The sequent calculus}{98} |
|
171 \contentsline {section}{\numberline {11.2}Simulating sequents by natural deduction}{99} |
|
172 \contentsline {section}{\numberline {11.3}Extra rules for the sequent calculus}{100} |
|
173 \contentsline {section}{\numberline {11.4}Classical rule sets}{101} |
|
174 \contentsline {section}{\numberline {11.5}The classical tactics}{103} |
|
175 \contentsline {subsection}{The automatic tactics}{103} |
|
176 \contentsline {subsection}{Single-step tactics}{103} |
|
177 \contentsline {subsection}{Other useful tactics}{104} |
|
178 \contentsline {subsection}{Creating swapped rules}{104} |
|
179 \contentsline {section}{\numberline {11.6}Setting up the classical reasoner}{104} |
|
180 \contentsline {chapter}{\numberline {A}Syntax of Isabelle Theories}{107} |