1 \begin{theindex} |
1 \begin{theindex} |
2 |
2 |
3 \item {\ptt !!} symbol, 24 |
3 \item {\tt !!} symbol, 25 |
4 \subitem in main goal, 44 |
4 \subitem in main goal, 46 |
5 \item {\tt\%} symbol, 24 |
5 \item {\tt\%} symbol, 25 |
6 \item {\ptt ::} symbol, 24 |
6 \item {\tt ::} symbol, 25 |
7 \item {\ptt ==} symbol, 24 |
7 \item {\tt ==} symbol, 25 |
8 \item {\ptt ==>} symbol, 24 |
8 \item {\tt ==>} symbol, 25 |
9 \item {\ptt =>} symbol, 24 |
9 \item {\tt =>} symbol, 25 |
10 \item {\ptt =?=} symbol, 24 |
10 \item {\tt =?=} symbol, 25 |
11 \item {\ptt [} symbol, 24 |
11 \item {\tt [} symbol, 25 |
12 \item {\ptt [|} symbol, 24 |
12 \item {\tt [|} symbol, 25 |
13 \item {\ptt ]} symbol, 24 |
13 \item {\tt ]} symbol, 25 |
14 \item {\tt\ttlbrace} symbol, 24 |
14 \item {\tt\ttlbrace} symbol, 25 |
15 \item {\tt\ttrbrace} symbol, 24 |
15 \item {\tt\ttrbrace} symbol, 25 |
16 \item {\ptt |]} symbol, 24 |
16 \item {\tt |]} symbol, 25 |
17 |
17 |
18 \indexspace |
18 \indexspace |
19 |
19 |
20 \item {\ptt allI} theorem, 35 |
20 \item {\tt allI} theorem, 37 |
21 \item arities |
21 \item arities |
22 \subitem declaring, 4, \bold{47} |
22 \subitem declaring, 4, \bold{49} |
23 \item {\ptt asm_simp_tac}, 57 |
23 \item {\tt asm_simp_tac}, 60 |
24 \item {\ptt assume_tac}, 28, 30, 35, 44 |
24 \item {\tt assume_tac}, 29, 31, 37, 47 |
25 \item assumptions |
25 \item assumptions |
26 \subitem deleting, 19 |
26 \subitem deleting, 20 |
27 \subitem discharge of, 7 |
27 \subitem discharge of, 7 |
28 \subitem lifting over, 13 |
28 \subitem lifting over, 14 |
29 \subitem of main goal, 39 |
29 \subitem of main goal, 41 |
30 \subitem use of, 16, 27 |
30 \subitem use of, 16, 28 |
31 \item axioms |
31 \item axioms |
32 \subitem Peano, 52 |
32 \subitem Peano, 54 |
33 |
33 |
34 \indexspace |
34 \indexspace |
35 |
35 |
36 \item {\ptt ba}, 29 |
36 \item {\tt ba}, 30 |
37 \item {\ptt back}, 55, 56, 59 |
37 \item {\tt back}, 59, 62 |
38 \item backtracking |
38 \item backtracking |
39 \subitem Prolog style, 59 |
39 \subitem Prolog style, 62 |
40 \item {\ptt bd}, 29 |
40 \item {\tt bd}, 30 |
41 \item {\ptt be}, 29 |
41 \item {\tt be}, 30 |
42 \item {\ptt br}, 29 |
42 \item {\tt br}, 30 |
43 \item {\ptt by}, 29 |
43 \item {\tt by}, 30 |
44 |
44 |
45 \indexspace |
45 \indexspace |
46 |
46 |
47 \item {\ptt choplev}, 34, 35, 61 |
47 \item {\tt choplev}, 36, 37, 64 |
48 \item classes, 3 |
48 \item classes, 3 |
49 \subitem built-in, \bold{24} |
49 \subitem built-in, \bold{25} |
50 \item classical reasoner, 37 |
50 \item classical reasoner, 39 |
51 \item {\ptt conjunct1} theorem, 26 |
51 \item {\tt conjunct1} theorem, 27 |
52 \item constants, 1 |
52 \item constants, 1 |
53 \subitem clashes with variables, 9 |
53 \subitem clashes with variables, 9 |
54 \subitem declaring, \bold{46} |
54 \subitem declaring, \bold{48} |
55 \subitem overloaded, 51 |
55 \subitem overloaded, 53 |
56 \subitem polymorphic, 3 |
56 \subitem polymorphic, 3 |
57 |
57 |
58 \indexspace |
58 \indexspace |
59 |
59 |
60 \item definitions, 5, \bold{46} |
60 \item definitions, 6, \bold{48} |
61 \subitem and derived rules, 41--44 |
61 \subitem and derived rules, 43--46 |
62 \item {\ptt DEPTH_FIRST}, 60 |
62 \item {\tt DEPTH_FIRST}, 64 |
63 \item destruct-resolution, 21, 29 |
63 \item destruct-resolution, 22, 30 |
64 \item {\ptt disjE} theorem, 30 |
64 \item {\tt disjE} theorem, 31 |
65 \item {\ptt dres_inst_tac}, 54 |
65 \item {\tt dres_inst_tac}, 57 |
66 \item {\ptt dresolve_tac}, 29, 31, 36 |
66 \item {\tt dresolve_tac}, 30, 32, 38 |
67 |
67 |
68 \indexspace |
68 \indexspace |
69 |
69 |
70 \item eigenvariables, \see{parameters}{7} |
70 \item eigenvariables, \see{parameters}{8} |
71 \item elim-resolution, \bold{19}, 28 |
71 \item elim-resolution, \bold{20}, 30 |
72 \item equality |
72 \item equality |
73 \subitem polymorphic, 3 |
73 \subitem polymorphic, 3 |
74 \item {\ptt eres_inst_tac}, 54 |
74 \item {\tt eres_inst_tac}, 57 |
75 \item {\ptt eresolve_tac}, 28, 31, 36, 44 |
75 \item {\tt eresolve_tac}, 30, 32, 38, 47 |
76 \item examples |
76 \item examples |
77 \subitem of deriving rules, 39 |
77 \subitem of deriving rules, 41 |
78 \subitem of induction, 54, 55 |
78 \subitem of induction, 57, 58 |
79 \subitem of simplification, 56 |
79 \subitem of simplification, 59 |
80 \subitem of tacticals, 35 |
80 \subitem of tacticals, 37 |
81 \subitem of theories, 46, 48--53, 58 |
81 \subitem of theories, 48, 50--55, 61 |
82 \subitem propositional, 16, 29, 31 |
82 \subitem propositional, 17, 31, 32 |
83 \subitem with quantifiers, 17, 32, 33, 36 |
83 \subitem with quantifiers, 18, 33, 35, 37 |
84 \item {\ptt exE} theorem, 36 |
84 \item {\tt exE} theorem, 38 |
85 |
85 |
86 \indexspace |
86 \indexspace |
87 |
87 |
88 \item {\ptt FalseE} theorem, 43 |
88 \item {\tt FalseE} theorem, 45 |
89 \item {\ptt fast_tac}, 37 |
89 \item {\tt fast_tac}, 39 |
90 \item first-order logic, 1 |
90 \item first-order logic, 1 |
91 \item flex-flex constraints, 5, 24, \bold{27} |
91 \item flex-flex constraints, 6, 25, \bold{28} |
92 \item {\ptt flexflex_rule}, 27 |
92 \item {\tt flexflex_rule}, 28 |
93 \item forward proof, 20, 23--29 |
93 \item forward proof, 21, 24--30 |
94 \item {\ptt fun} type, 1, 4 |
94 \item {\tt fun} type, 1, 4 |
95 \item function applications, 1, 7 |
95 \item function applications, 1, 8 |
96 |
96 |
97 \indexspace |
97 \indexspace |
98 |
98 |
99 \item {\ptt goal}, 29, 39, 44 |
99 \item {\tt goal}, 30, 41, 46 |
100 \item {\ptt goalw}, 42--44 |
100 \item {\tt goalw}, 44--46 |
101 |
101 |
102 \indexspace |
102 \indexspace |
103 |
103 |
104 \item {\ptt has_fewer_prems}, 61 |
104 \item {\tt has_fewer_prems}, 64 |
105 \item higher-order logic, 4 |
105 \item higher-order logic, 4 |
106 |
106 |
107 \indexspace |
107 \indexspace |
108 |
108 |
109 \item identifiers, 23 |
109 \item identifiers, 24 |
110 \item {\ptt impI} theorem, 30, 42 |
110 \item {\tt impI} theorem, 31, 44 |
111 \item infixes, 49 |
111 \item infixes, 52 |
112 \item instantiation, 54--57 |
112 \item instantiation, 57--60 |
113 \item Isabelle |
113 \item Isabelle |
114 \subitem object-logics supported, i |
114 \subitem object-logics supported, i |
115 \subitem overview, i |
115 \subitem overview, i |
116 \subitem release history, i |
116 \subitem release history, i |
117 |
117 |
118 \indexspace |
118 \indexspace |
119 |
119 |
120 \item $\lambda$-abstractions, 1, 7, 24 |
120 \item $\lambda$-abstractions, 1, 8, 25 |
121 \item $\lambda$-calculus, 1 |
121 \item $\lambda$-calculus, 1 |
122 \item LCF, i |
122 \item LCF, i |
123 \item LCF system, 15, 25 |
123 \item LCF system, 15, 26 |
124 \item level of a proof, 29 |
124 \item level of a proof, 31 |
125 \item lifting, \bold{13} |
125 \item lifting, \bold{14} |
126 \item {\ptt logic} class, 3, 6, 24 |
126 \item {\tt logic} class, 3, 6, 25 |
127 |
127 |
128 \indexspace |
128 \indexspace |
129 |
129 |
130 \item major premise, \bold{20} |
130 \item major premise, \bold{21} |
131 \item {\ptt Match} exception, 40 |
131 \item {\tt Match} exception, 42 |
132 \item meta-assumptions |
132 \item meta-assumptions |
133 \subitem syntax of, 21 |
133 \subitem syntax of, 22 |
134 \item meta-equality, \bold{5}, 24 |
134 \item meta-equality, \bold{5}, 25 |
135 \item meta-implication, \bold{5}, 6, 24 |
135 \item meta-implication, \bold{5}, 7, 25 |
136 \item meta-quantifiers, \bold{5}, 7, 24 |
136 \item meta-quantifiers, \bold{5}, 8, 25 |
137 \item meta-rewriting, 41 |
137 \item meta-rewriting, 43 |
138 \item mixfix declarations, 49, 50, 53 |
138 \item mixfix declarations, 52, 53, 56 |
139 \item ML, i |
139 \item ML, i |
140 \item {\ptt ML} section, 45 |
140 \item {\tt ML} section, 47 |
141 \item {\ptt mp} theorem, 26 |
141 \item {\tt mp} theorem, 27 |
142 |
142 |
143 \indexspace |
143 \indexspace |
144 |
144 |
145 \item {\ptt Nat} theory, 53 |
145 \item {\tt Nat} theory, 55 |
146 \item {\ptt nat} type, 1, 3 |
146 \item {\tt nat} type, 1, 3 |
147 \item {\ptt not_def} theorem, 42 |
147 \item {\tt not_def} theorem, 44 |
148 \item {\ptt notE} theorem, \bold{43}, 55 |
148 \item {\tt notE} theorem, \bold{45}, 58 |
149 \item {\ptt notI} theorem, \bold{42}, 55 |
149 \item {\tt notI} theorem, \bold{44}, 58 |
150 |
150 |
151 \indexspace |
151 \indexspace |
152 |
152 |
153 \item {\ptt o} type, 1, 4 |
153 \item {\tt o} type, 1, 4 |
154 \item {\ptt ORELSE}, 35 |
154 \item {\tt ORELSE}, 37 |
155 \item overloading, \bold{4}, 51 |
155 \item overloading, \bold{4}, 53 |
156 |
156 |
157 \indexspace |
157 \indexspace |
158 |
158 |
159 \item parameters, \bold{7}, 32 |
159 \item parameters, \bold{8}, 33 |
160 \subitem lifting over, 14 |
160 \subitem lifting over, 15 |
161 \item {\ptt Prolog} theory, 58 |
161 \item {\tt Prolog} theory, 61 |
162 \item Prolog interpreter, \bold{57} |
162 \item Prolog interpreter, \bold{60} |
163 \item proof state, 15 |
163 \item proof state, 16 |
164 \item proofs |
164 \item proofs |
165 \subitem commands for, 29 |
165 \subitem commands for, 30 |
166 \item {\ptt PROP} symbol, 25 |
166 \item {\tt PROP} symbol, 26 |
167 \item {\ptt prop} type, 6, 24 |
167 \item {\tt prop} type, 6, 25, 26 |
168 \item {\ptt prth}, 26 |
168 \item {\tt prth}, 27 |
169 \item {\ptt prthq}, 26, 27 |
169 \item {\tt prthq}, 27, 28 |
170 \item {\ptt prths}, 26 |
170 \item {\tt prths}, 27 |
171 \item {\ptt Pure} theory, 45 |
171 \item {\tt Pure} theory, 47 |
172 |
172 |
173 \indexspace |
173 \indexspace |
174 |
174 |
175 \item quantifiers, 5, 7, 32 |
175 \item quantifiers, 5, 8, 33 |
176 |
176 |
177 \indexspace |
177 \indexspace |
178 |
178 |
179 \item {\ptt read_instantiate}, 28 |
179 \item {\tt read_instantiate}, 29 |
180 \item {\ptt refl} theorem, 28 |
180 \item {\tt refl} theorem, 29 |
181 \item {\ptt REPEAT}, 31, 36, 59, 60 |
181 \item {\tt REPEAT}, 33, 37, 62, 64 |
182 \item {\ptt res_inst_tac}, 54, 56 |
182 \item {\tt res_inst_tac}, 57, 60 |
183 \item reserved words, 23 |
183 \item reserved words, 24 |
184 \item resolution, 10, \bold{11} |
184 \item resolution, 10, \bold{12} |
185 \subitem in backward proof, 15 |
185 \subitem in backward proof, 15 |
186 \subitem with instantiation, 54 |
186 \subitem with instantiation, 57 |
187 \item {\ptt resolve_tac}, 28, 30, 43, 55 |
187 \item {\tt resolve_tac}, 30, 31, 46, 58 |
188 \item {\ptt result}, 29, 40, 44 |
188 \item {\tt result}, 30, 42, 46 |
189 \item {\ptt rewrite_goals_tac}, 42 |
189 \item {\tt rewrite_goals_tac}, 44 |
190 \item {\ptt rewrite_rule}, 43 |
190 \item {\tt rewrite_rule}, 45, 46 |
191 \item {\ptt RL}, 27, 28 |
191 \item {\tt RL}, 29 |
192 \item {\ptt RLN}, 27 |
192 \item {\tt RLN}, 29 |
193 \item {\ptt RS}, 26, 27, 44 |
193 \item {\tt RS}, 27, 29, 46 |
194 \item {\ptt RSN}, 26, 27 |
194 \item {\tt RSN}, 27, 29 |
195 \item rules |
195 \item rules |
196 \subitem declaring, 46 |
196 \subitem declaring, 48 |
197 \subitem derived, 12, \bold{21}, 39, 41 |
197 \subitem derived, 13, \bold{22}, 41, 43 |
198 \subitem destruction, 20 |
198 \subitem destruction, 21 |
199 \subitem elimination, 20 |
199 \subitem elimination, 21 |
200 \subitem propositional, 6 |
200 \subitem propositional, 6 |
201 \subitem quantifier, 7 |
201 \subitem quantifier, 8 |
202 |
202 |
203 \indexspace |
203 \indexspace |
204 |
204 |
205 \item search |
205 \item search |
206 \subitem depth-first, 60 |
206 \subitem depth-first, 63 |
207 \item signatures, \bold{8} |
207 \item signatures, \bold{9} |
208 \item {\ptt simp_tac}, 57 |
208 \item {\tt simp_tac}, 60 |
209 \item simplification, 56 |
209 \item simplification, 59 |
210 \item simplification sets, 56 |
210 \item simplification sets, 59 |
211 \item sort constraints, 24 |
211 \item sort constraints, 25 |
212 \item sorts, \bold{4} |
212 \item sorts, \bold{5} |
213 \item {\ptt spec} theorem, 26, 34, 35 |
213 \item {\tt spec} theorem, 28, 36, 37 |
214 \item {\ptt standard}, 26 |
214 \item {\tt standard}, 27 |
215 \item substitution, \bold{7} |
215 \item substitution, \bold{8} |
216 \item {\ptt Suc_inject}, 55 |
216 \item {\tt Suc_inject}, 58 |
217 \item {\ptt Suc_neq_0}, 55 |
217 \item {\tt Suc_neq_0}, 58 |
218 \item syntax |
218 \item syntax |
219 \subitem of types and terms, 24 |
219 \subitem of types and terms, 25 |
220 |
220 |
221 \indexspace |
221 \indexspace |
222 |
222 |
223 \item tacticals, \bold{18}, 35 |
223 \item tacticals, \bold{19}, 37 |
224 \item tactics, \bold{18} |
224 \item tactics, \bold{19} |
225 \subitem assumption, 28 |
225 \subitem assumption, 29 |
226 \subitem resolution, 28 |
226 \subitem resolution, 30 |
227 \item {\ptt term} class, 3 |
227 \item {\tt term} class, 3 |
228 \item terms |
228 \item terms |
229 \subitem syntax of, 1, \bold{24} |
229 \subitem syntax of, 1, \bold{25} |
230 \item theorems |
230 \item theorems |
231 \subitem basic operations on, \bold{25} |
231 \subitem basic operations on, \bold{26} |
232 \subitem printing of, 25 |
232 \subitem printing of, 27 |
233 \item theories, \bold{8} |
233 \item theories, \bold{9} |
234 \subitem defining, 44--54 |
234 \subitem defining, 47--57 |
235 \item {\ptt thm} ML type, 25 |
235 \item {\tt thm} ML type, 26 |
236 \item {\ptt topthm}, 40 |
236 \item {\tt topthm}, 42 |
237 \item {\ptt Trueprop} constant, 6, 24 |
237 \item {\tt Trueprop} constant, 6, 7, 25 |
238 \item type constraints, 24 |
238 \item type constraints, 25 |
239 \item type constructors, 1 |
239 \item type constructors, 1 |
240 \item type identifiers, 23 |
240 \item type identifiers, 24 |
241 \item type synonyms, \bold{49} |
241 \item type synonyms, \bold{51} |
242 \item types |
242 \item types |
243 \subitem declaring, \bold{47} |
243 \subitem declaring, \bold{49} |
244 \subitem function, 1 |
244 \subitem function, 1 |
245 \subitem higher, \bold{5} |
245 \subitem higher, \bold{5} |
246 \subitem polymorphic, \bold{3} |
246 \subitem polymorphic, \bold{3} |
247 \subitem simple, \bold{1} |
247 \subitem simple, \bold{1} |
248 \subitem syntax of, 1, \bold{24} |
248 \subitem syntax of, 1, \bold{25} |
249 |
249 |
250 \indexspace |
250 \indexspace |
251 |
251 |
252 \item {\ptt undo}, 29 |
252 \item {\tt undo}, 30 |
253 \item unification |
253 \item unification |
254 \subitem higher-order, \bold{10}, 55 |
254 \subitem higher-order, \bold{11}, 58 |
255 \subitem incompleteness of, 11 |
255 \subitem incompleteness of, 11 |
256 \item unknowns, 9, 23, 32 |
256 \item unknowns, 10, 24, 33 |
257 \subitem function, \bold{11}, 27, 32 |
257 \subitem function, \bold{11}, 28, 33 |
258 \item {\ptt use_thy}, \bold{45} |
258 \item {\tt use_thy}, \bold{47} |
259 |
259 |
260 \indexspace |
260 \indexspace |
261 |
261 |
262 \item variables |
262 \item variables |
263 \subitem bound, 7 |
263 \subitem bound, 8 |
264 |
264 |
265 \end{theindex} |
265 \end{theindex} |