1 \begin{theindex} |
|
2 |
|
3 \item {\tt !!} symbol, 71 |
|
4 \item {\tt\$}, \bold{62}, 88 |
|
5 \item {\tt\%} symbol, 71 |
|
6 \item * SplitterFun, 129 |
|
7 \item {\tt ::} symbol, 71, 72 |
|
8 \item {\tt ==} symbol, 71 |
|
9 \item {\tt ==>} symbol, 71 |
|
10 \item {\tt =>} symbol, 71 |
|
11 \item {\tt =?=} symbol, 71 |
|
12 \item {\tt\at Enum} constant, 94 |
|
13 \item {\tt\at Finset} constant, 94, 95 |
|
14 \item {\tt [} symbol, 71 |
|
15 \item {\tt [|} symbol, 71 |
|
16 \item {\tt \$ISABELLE_HOME}, 3 |
|
17 \item {\tt ]} symbol, 71 |
|
18 \item {\tt _K} constant, 96, 98 |
|
19 \item \verb'{}' symbol, 94 |
|
20 \item {\tt\ttlbrace} symbol, 71 |
|
21 \item {\tt\ttrbrace} symbol, 71 |
|
22 \item {\tt |]} symbol, 71 |
|
23 |
|
24 \indexspace |
|
25 |
|
26 \item {\tt Abs}, \bold{62}, 88 |
|
27 \item {\tt abstract_over}, \bold{63} |
|
28 \item {\tt abstract_rule}, \bold{49} |
|
29 \item {\tt aconv}, \bold{63} |
|
30 \item {\tt add_path}, \bold{60} |
|
31 \item {\tt addaltern}, \bold{137} |
|
32 \item {\tt addbefore}, \bold{137} |
|
33 \item {\tt Addcongs}, \bold{107} |
|
34 \item {\tt addcongs}, \bold{112}, 127, 128 |
|
35 \item {\tt addD2}, \bold{136} |
|
36 \item {\tt AddDs}, \bold{142} |
|
37 \item {\tt addDs}, \bold{135} |
|
38 \item {\tt addE2}, \bold{136} |
|
39 \item {\tt addeqcongs}, \bold{112}, 128 |
|
40 \item {\tt AddEs}, \bold{142} |
|
41 \item {\tt addEs}, \bold{135} |
|
42 \item {\tt AddIs}, \bold{142} |
|
43 \item {\tt addIs}, \bold{135} |
|
44 \item {\tt addloop}, \bold{114} |
|
45 \item {\tt addSaltern}, \bold{137} |
|
46 \item {\tt addSbefore}, \bold{137} |
|
47 \item {\tt addSD2}, \bold{136} |
|
48 \item {\tt AddSDs}, \bold{142} |
|
49 \item {\tt addSDs}, \bold{135} |
|
50 \item {\tt addSE2}, \bold{136} |
|
51 \item {\tt AddSEs}, \bold{142} |
|
52 \item {\tt addSEs}, \bold{135} |
|
53 \item {\tt Addsimprocs}, \bold{107} |
|
54 \item {\tt addsimprocs}, \bold{111} |
|
55 \item {\tt Addsimps}, \bold{107} |
|
56 \item {\tt addsimps}, \bold{110}, 128 |
|
57 \item {\tt AddSIs}, \bold{142} |
|
58 \item {\tt addSIs}, \bold{135} |
|
59 \item {\tt addSolver}, \bold{113} |
|
60 \item {\tt Addsplits}, \bold{107} |
|
61 \item {\tt addsplits}, \bold{115} |
|
62 \item {\tt addss}, \bold{137}, 138 |
|
63 \item {\tt addSSolver}, \bold{113} |
|
64 \item {\tt addSWrapper}, \bold{137} |
|
65 \item {\tt addWrapper}, \bold{137} |
|
66 \item {\tt all_tac}, \bold{34} |
|
67 \item {\tt ALLGOALS}, \bold{38}, 119, 122 |
|
68 \item ambiguity |
|
69 \subitem of parsed expressions, 81 |
|
70 \item {\tt ancestors_of}, \bold{61} |
|
71 \item {\tt any} nonterminal, \bold{70} |
|
72 \item {\tt APPEND}, \bold{32}, 34 |
|
73 \item {\tt APPEND'}, 39 |
|
74 \item {\tt Appl}, 85 |
|
75 \item {\tt aprop} nonterminal, \bold{72} |
|
76 \item {\tt ares_tac}, \bold{23} |
|
77 \item {\tt args} nonterminal, 95 |
|
78 \item {\tt Arith} theory, 121 |
|
79 \item arities |
|
80 \subitem context conditions, 58 |
|
81 \item {\tt Asm_full_simp_tac}, \bold{106} |
|
82 \item {\tt asm_full_simp_tac}, 26, \bold{116}, 120 |
|
83 \item {\tt asm_full_simplify}, 116 |
|
84 \item {\tt asm_rl} theorem, 25 |
|
85 \item {\tt Asm_simp_tac}, \bold{105}, 118 |
|
86 \item {\tt asm_simp_tac}, \bold{116}, 128 |
|
87 \item {\tt asm_simplify}, 116 |
|
88 \item associative-commutative operators, 121 |
|
89 \item {\tt assume}, \bold{48} |
|
90 \item {\tt assume_ax}, 10, \bold{12} |
|
91 \item {\tt assume_tac}, \bold{21}, 134 |
|
92 \item {\tt assumption}, \bold{51} |
|
93 \item assumptions |
|
94 \subitem contradictory, 142 |
|
95 \subitem deleting, 26 |
|
96 \subitem in simplification, 105, 114 |
|
97 \subitem inserting, 23 |
|
98 \subitem negated, 132 |
|
99 \subitem of main goal, 9, 10, 12, 17, 18 |
|
100 \subitem reordering, 120 |
|
101 \subitem rotating, 26 |
|
102 \subitem substitution in, 102 |
|
103 \subitem tactics for, 21 |
|
104 \item ASTs, 85--90 |
|
105 \subitem made from parse trees, 86 |
|
106 \subitem made from terms, 88 |
|
107 \item {\tt atac}, \bold{23} |
|
108 \item {\tt Auto_tac}, \bold{142} |
|
109 \item {\tt auto_tac} $(cs,ss)$, \bold{139} |
|
110 \item {\tt axclass} section, 57 |
|
111 \item axiomatic type class, 57 |
|
112 \item axioms |
|
113 \subitem extracting, 11 |
|
114 \item {\tt axioms_of}, \bold{11} |
|
115 |
|
116 \indexspace |
|
117 |
|
118 \item {\tt ba}, \bold{14} |
|
119 \item {\tt back}, \bold{13} |
|
120 \item batch execution, 16 |
|
121 \item {\tt bd}, \bold{14} |
|
122 \item {\tt bds}, \bold{14} |
|
123 \item {\tt be}, \bold{14} |
|
124 \item {\tt bes}, \bold{14} |
|
125 \item {\tt BEST_FIRST}, \bold{35}, 36 |
|
126 \item {\tt Best_tac}, \bold{142} |
|
127 \item {\tt best_tac}, \bold{140} |
|
128 \item {\tt beta_conversion}, \bold{49} |
|
129 \item {\tt bicompose}, \bold{52} |
|
130 \item {\tt bimatch_tac}, \bold{27} |
|
131 \item {\tt bind_thm}, \bold{11}, 12, 42 |
|
132 \item binders, \bold{80} |
|
133 \item {\tt biresolution}, \bold{51} |
|
134 \item {\tt biresolve_tac}, \bold{27}, 143 |
|
135 \item {\tt Blast.depth_tac}, \bold{139} |
|
136 \item {\tt Blast.trace}, \bold{139} |
|
137 \item {\tt Blast_tac}, \bold{142} |
|
138 \item {\tt blast_tac}, \bold{138} |
|
139 \item {\tt Bound}, \bold{62}, 86, 88, 89 |
|
140 \item {\tt bound_hyp_subst_tac}, \bold{102} |
|
141 \item {\tt br}, \bold{14} |
|
142 \item {\tt BREADTH_FIRST}, \bold{35} |
|
143 \item {\tt brs}, \bold{14} |
|
144 \item {\tt bw}, \bold{15} |
|
145 \item {\tt bws}, \bold{15} |
|
146 \item {\tt by}, \bold{9}, 12--14, 18 |
|
147 \item {\tt byev}, \bold{10} |
|
148 |
|
149 \indexspace |
|
150 |
|
151 \item {\tt cd}, \bold{3} |
|
152 \item {\tt cert_axm}, \bold{64} |
|
153 \item {\tt CHANGED}, \bold{34} |
|
154 \item {\tt chop}, \bold{12}, 17 |
|
155 \item {\tt choplev}, \bold{13} |
|
156 \item {\tt Clarify_step_tac}, \bold{142} |
|
157 \item {\tt clarify_step_tac}, \bold{139} |
|
158 \item {\tt Clarify_tac}, \bold{142} |
|
159 \item {\tt clarify_tac}, \bold{139} |
|
160 \item {\tt Clarsimp_tac}, \bold{142} |
|
161 \item {\tt clarsimp_tac}, \bold{140} |
|
162 \item claset |
|
163 \subitem current, 141 |
|
164 \item {\tt claset} ML type, 135 |
|
165 \item {\tt ClasimpFun}, 144 |
|
166 \item classes |
|
167 \subitem context conditions, 58 |
|
168 \item classical reasoner, 130--144 |
|
169 \subitem setting up, 143 |
|
170 \subitem tactics, 138 |
|
171 \item classical sets, 134 |
|
172 \item {\tt ClassicalFun}, 143 |
|
173 \item {\tt combination}, \bold{49} |
|
174 \item {\tt commit}, \bold{3} |
|
175 \item {\tt COMP}, \bold{51} |
|
176 \item {\tt compose}, \bold{51} |
|
177 \item {\tt compose_tac}, \bold{27} |
|
178 \item {\tt concl_of}, \bold{45} |
|
179 \item {\tt COND}, \bold{36} |
|
180 \item congruence rules, 111 |
|
181 \item {\tt Const}, \bold{62}, 88, 98 |
|
182 \item {\tt Constant}, 85, 98 |
|
183 \item constants, \bold{62} |
|
184 \subitem for translations, 75 |
|
185 \subitem syntactic, 90 |
|
186 \item {\tt context}, \bold{4}, 105 |
|
187 \item {\tt contr_tac}, \bold{142} |
|
188 \item {\tt could_unify}, \bold{29} |
|
189 \item {\tt cprems_of}, \bold{45} |
|
190 \item {\tt cprop_of}, \bold{44} |
|
191 \item {\tt CPure} theory, 55 |
|
192 \item {\tt CPure.thy}, \bold{61} |
|
193 \item {\tt crep_thm}, \bold{45} |
|
194 \item {\tt cterm} ML type, 64 |
|
195 \item {\tt cterm_instantiate}, \bold{43} |
|
196 \item {\tt cterm_of}, 9, 17, \bold{64} |
|
197 \item {\tt ctyp}, \bold{65} |
|
198 \item {\tt ctyp_of}, \bold{66} |
|
199 \item {\tt cut_facts_tac}, \bold{23}, 103 |
|
200 \item {\tt cut_inst_tac}, \bold{23} |
|
201 \item {\tt cut_rl} theorem, 25 |
|
202 |
|
203 \indexspace |
|
204 |
|
205 \item {\tt datatype}, 107 |
|
206 \item {\tt Deepen_tac}, \bold{142} |
|
207 \item {\tt deepen_tac}, \bold{140} |
|
208 \item {\tt defer_tac}, \bold{24} |
|
209 \item definitions, \see{rewriting, meta-level}{1}, 24, \bold{58} |
|
210 \subitem unfolding, 9, 10 |
|
211 \item {\tt del_path}, \bold{60} |
|
212 \item {\tt Delcongs}, \bold{107} |
|
213 \item {\tt delcongs}, \bold{112} |
|
214 \item {\tt deleqcongs}, \bold{112} |
|
215 \item {\tt delete_tmpfiles}, \bold{59} |
|
216 \item delimiters, \bold{72}, 75, 76, 78 |
|
217 \item {\tt delloop}, \bold{114} |
|
218 \item {\tt delrules}, \bold{135} |
|
219 \item {\tt Delsimprocs}, \bold{107} |
|
220 \item {\tt delsimprocs}, \bold{111} |
|
221 \item {\tt Delsimps}, \bold{107} |
|
222 \item {\tt delsimps}, \bold{110} |
|
223 \item {\tt Delsplits}, \bold{107} |
|
224 \item {\tt delSWrapper}, \bold{137} |
|
225 \item {\tt delWrapper}, \bold{137} |
|
226 \item {\tt dependent_tr'}, 96, \bold{98} |
|
227 \item {\tt DEPTH_FIRST}, \bold{35} |
|
228 \item {\tt DEPTH_SOLVE}, \bold{35} |
|
229 \item {\tt DEPTH_SOLVE_1}, \bold{35} |
|
230 \item {\tt depth_tac}, \bold{140} |
|
231 \item {\tt Deriv.drop}, \bold{53} |
|
232 \item {\tt Deriv.linear}, \bold{53} |
|
233 \item {\tt Deriv.size}, \bold{53} |
|
234 \item {\tt Deriv.tree}, \bold{53} |
|
235 \item {\tt dest_eq}, \bold{103} |
|
236 \item {\tt dest_imp}, \bold{103} |
|
237 \item {\tt dest_state}, \bold{45} |
|
238 \item {\tt dest_Trueprop}, \bold{103} |
|
239 \item destruct-resolution, 21 |
|
240 \item {\tt DETERM}, \bold{36} |
|
241 \item discrimination nets, \bold{28} |
|
242 \item {\tt distinct_subgoals_tac}, \bold{26} |
|
243 \item {\tt dmatch_tac}, \bold{21} |
|
244 \item {\tt domain_type}, \bold{104} |
|
245 \item {\tt dres_inst_tac}, \bold{22} |
|
246 \item {\tt dresolve_tac}, \bold{21} |
|
247 \item {\tt dtac}, \bold{23} |
|
248 \item {\tt dummyT}, 88, 89, 99 |
|
249 \item duplicate subgoals |
|
250 \subitem removing, 26 |
|
251 |
|
252 \indexspace |
|
253 |
|
254 \item elim-resolution, 20 |
|
255 \item {\tt ematch_tac}, \bold{21} |
|
256 \item {\tt empty} constant, 94 |
|
257 \item {\tt empty_cs}, \bold{135} |
|
258 \item {\tt empty_ss}, \bold{109} |
|
259 \item {\tt eq_assume_tac}, \bold{21}, 134 |
|
260 \item {\tt eq_assumption}, \bold{51} |
|
261 \item {\tt eq_mp_tac}, \bold{142} |
|
262 \item {\tt eq_reflection} theorem, \bold{104}, 125 |
|
263 \item {\tt eq_thm}, \bold{36} |
|
264 \item {\tt eq_thy}, \bold{60} |
|
265 \item {\tt equal_elim}, \bold{48} |
|
266 \item {\tt equal_intr}, \bold{48} |
|
267 \item equality, 101--104 |
|
268 \item {\tt eres_inst_tac}, \bold{22} |
|
269 \item {\tt eresolve_tac}, \bold{20} |
|
270 \subitem on other than first premise, 44 |
|
271 \item {\tt ERROR}, 6 |
|
272 \item {\tt error}, 6 |
|
273 \item error messages, 6 |
|
274 \item {\tt eta_contract}, \bold{6}, 92 |
|
275 \item {\tt etac}, \bold{23} |
|
276 \item {\tt EVERY}, \bold{33} |
|
277 \item {\tt EVERY'}, 39 |
|
278 \item {\tt EVERY1}, \bold{40} |
|
279 \item examples |
|
280 \subitem of logic definitions, 82 |
|
281 \subitem of macros, 94, 95 |
|
282 \subitem of mixfix declarations, 77 |
|
283 \subitem of simplification, 117 |
|
284 \subitem of translations, 98 |
|
285 \item exceptions |
|
286 \subitem printing of, 7 |
|
287 \item {\tt exit}, \bold{3} |
|
288 \item {\tt extensional}, \bold{49} |
|
289 |
|
290 \indexspace |
|
291 |
|
292 \item {\tt fa}, \bold{15} |
|
293 \item {\tt Fast_tac}, \bold{142} |
|
294 \item {\tt fast_tac}, \bold{140} |
|
295 \item {\tt fd}, \bold{15} |
|
296 \item {\tt fds}, \bold{15} |
|
297 \item {\tt fe}, \bold{15} |
|
298 \item {\tt fes}, \bold{15} |
|
299 \item files |
|
300 \subitem reading, 3, 59 |
|
301 \item {\tt filt_resolve_tac}, \bold{29} |
|
302 \item {\tt FILTER}, \bold{34} |
|
303 \item {\tt filter_goal}, \bold{19} |
|
304 \item {\tt filter_thms}, \bold{29} |
|
305 \item {\tt findE}, \bold{12} |
|
306 \item {\tt findEs}, \bold{12} |
|
307 \item {\tt findI}, \bold{12} |
|
308 \item {\tt FIRST}, \bold{33} |
|
309 \item {\tt FIRST'}, 39 |
|
310 \item {\tt FIRST1}, \bold{40} |
|
311 \item {\tt FIRSTGOAL}, \bold{38} |
|
312 \item flex-flex constraints, 26, 44, 52 |
|
313 \item {\tt flexflex_rule}, \bold{52} |
|
314 \item {\tt flexflex_tac}, \bold{26} |
|
315 \item {\tt FOL_basic_ss}, \bold{128} |
|
316 \item {\tt FOL_ss}, \bold{128} |
|
317 \item {\tt fold_goals_tac}, \bold{24} |
|
318 \item {\tt fold_tac}, \bold{24} |
|
319 \item {\tt forall_elim}, \bold{50} |
|
320 \item {\tt forall_elim_list}, \bold{50} |
|
321 \item {\tt forall_elim_var}, \bold{50} |
|
322 \item {\tt forall_elim_vars}, \bold{50} |
|
323 \item {\tt forall_intr}, \bold{49} |
|
324 \item {\tt forall_intr_frees}, \bold{50} |
|
325 \item {\tt forall_intr_list}, \bold{50} |
|
326 \item {\tt force_strip_shyps}, \bold{45} |
|
327 \item {\tt Force_tac}, \bold{142} |
|
328 \item {\tt force_tac}, \bold{139} |
|
329 \item {\tt forw_inst_tac}, \bold{22} |
|
330 \item forward proof, 21, 42 |
|
331 \item {\tt forward_tac}, \bold{21} |
|
332 \item {\tt fr}, \bold{15} |
|
333 \item {\tt Free}, \bold{62}, 88 |
|
334 \item {\tt freezeT}, \bold{50} |
|
335 \item {\tt frs}, \bold{15} |
|
336 \item {\tt Full_simp_tac}, \bold{105} |
|
337 \item {\tt full_simp_tac}, \bold{116} |
|
338 \item {\tt full_simplify}, 116 |
|
339 \item {\textit {fun}} type, 65 |
|
340 \item function applications, \bold{62} |
|
341 |
|
342 \indexspace |
|
343 |
|
344 \item {\tt get_axiom}, \bold{11} |
|
345 \item {\tt get_thm}, \bold{11} |
|
346 \item {\tt get_thms}, \bold{11} |
|
347 \item {\tt getenv}, 59 |
|
348 \item {\tt getgoal}, \bold{18} |
|
349 \item {\tt gethyps}, \bold{19}, 38 |
|
350 \item {\tt Goal}, \bold{9}, 17 |
|
351 \item {\tt goal}, \bold{9} |
|
352 \item {\tt goals_limit}, \bold{13} |
|
353 \item {\tt Goalw}, \bold{9} |
|
354 \item {\tt goalw}, \bold{9} |
|
355 \item {\tt goalw_cterm}, \bold{9} |
|
356 |
|
357 \indexspace |
|
358 |
|
359 \item {\tt has_fewer_prems}, \bold{36} |
|
360 \item higher-order pattern, \bold{110} |
|
361 \item {\tt HOL_basic_ss}, \bold{109} |
|
362 \item {\tt hyp_subst_tac}, \bold{102} |
|
363 \item {\tt hyp_subst_tacs}, \bold{144} |
|
364 \item {\tt HypsubstFun}, 103, 144 |
|
365 |
|
366 \indexspace |
|
367 |
|
368 \item {\tt id} nonterminal, \bold{72}, 86, 93 |
|
369 \item identifiers, 72 |
|
370 \item {\tt idt} nonterminal, 92 |
|
371 \item {\tt idts} nonterminal, \bold{72}, 80 |
|
372 \item {\tt IF_UNSOLVED}, \bold{36} |
|
373 \item {\tt iff_reflection} theorem, 125 |
|
374 \item {\tt IFOL_ss}, \bold{128} |
|
375 \item {\tt imp_intr} theorem, \bold{104} |
|
376 \item {\tt implies_elim}, \bold{48} |
|
377 \item {\tt implies_elim_list}, \bold{48} |
|
378 \item {\tt implies_intr}, \bold{48} |
|
379 \item {\tt implies_intr_hyps}, \bold{48} |
|
380 \item {\tt implies_intr_list}, \bold{48} |
|
381 \item {\tt incr_boundvars}, \bold{63}, 98 |
|
382 \item {\tt indexname} ML type, 62, 73 |
|
383 \item infixes, \bold{79} |
|
384 \item {\tt insert} constant, 94 |
|
385 \item {\tt inst_step_tac}, \bold{141} |
|
386 \item {\tt instance} section, 57 |
|
387 \item {\tt instantiate}, \bold{50} |
|
388 \item {\tt instantiate'}, \bold{43}, 50 |
|
389 \item instantiation, 22, 43, 50 |
|
390 \item {\tt INTLEAVE}, \bold{32}, 34 |
|
391 \item {\tt INTLEAVE'}, 39 |
|
392 \item {\tt invoke_oracle}, \bold{66} |
|
393 \item {\tt is} nonterminal, 94 |
|
394 |
|
395 \indexspace |
|
396 |
|
397 \item {\tt joinrules}, \bold{143} |
|
398 |
|
399 \indexspace |
|
400 |
|
401 \item {\tt keep_derivs}, \bold{53} |
|
402 |
|
403 \indexspace |
|
404 |
|
405 \item $\lambda$-abstractions, 28, \bold{62} |
|
406 \item $\lambda$-calculus, 47, 49, 72 |
|
407 \item {\tt lessb}, \bold{28} |
|
408 \item lexer, \bold{72} |
|
409 \item {\tt lift_rule}, \bold{52} |
|
410 \item lifting, 52 |
|
411 \item {\tt logic} class, 72, 77 |
|
412 \item {\tt logic} nonterminal, \bold{72} |
|
413 \item {\tt Logic.auto_rename}, \bold{26} |
|
414 \item {\tt Logic.set_rename_prefix}, \bold{25} |
|
415 \item {\tt long_names}, \bold{6} |
|
416 \item {\tt loose_bnos}, \bold{63}, 99 |
|
417 |
|
418 \indexspace |
|
419 |
|
420 \item macros, 90--96 |
|
421 \item {\tt make_elim}, \bold{44}, 136 |
|
422 \item {\tt Match} exception, 97 |
|
423 \item {\tt match_tac}, \bold{21}, 134 |
|
424 \item {\tt max_pri}, 70, \bold{76} |
|
425 \item {\tt merge_ss}, \bold{109} |
|
426 \item meta-assumptions, 37, 46, 48, 51 |
|
427 \subitem printing of, 5 |
|
428 \item meta-equality, 47--49 |
|
429 \item meta-implication, 47, 48 |
|
430 \item meta-quantifiers, 47, 49 |
|
431 \item meta-rewriting, 9, 15, 16, \bold{24}, |
|
432 \seealso{tactics, theorems}{145} |
|
433 \subitem in theorems, 43 |
|
434 \item meta-rules, \see{meta-rules}{1}, 46--52 |
|
435 \item {\tt METAHYPS}, 19, \bold{37} |
|
436 \item mixfix declarations, 57, 75--80 |
|
437 \item {\tt mk_atomize}, \bold{127} |
|
438 \item {\tt mk_simproc}, \bold{123} |
|
439 \item {\tt ML} section, 58, 97, 99 |
|
440 \item model checkers, 81 |
|
441 \item {\tt mp} theorem, \bold{143} |
|
442 \item {\tt mp_tac}, \bold{142} |
|
443 \item {\tt MRL}, \bold{42} |
|
444 \item {\tt MRS}, \bold{42} |
|
445 |
|
446 \indexspace |
|
447 |
|
448 \item name tokens, \bold{72} |
|
449 \item {\tt nat_cancel}, \bold{111} |
|
450 \item {\tt net_bimatch_tac}, \bold{28} |
|
451 \item {\tt net_biresolve_tac}, \bold{28} |
|
452 \item {\tt net_match_tac}, \bold{28} |
|
453 \item {\tt net_resolve_tac}, \bold{28} |
|
454 \item {\tt no_tac}, \bold{34} |
|
455 \item {\tt None}, \bold{30} |
|
456 \item {\tt nonterminal} symbols, 56 |
|
457 \item {\tt not_elim} theorem, \bold{143} |
|
458 \item {\tt nprems_of}, \bold{45} |
|
459 \item numerals, 72 |
|
460 |
|
461 \indexspace |
|
462 |
|
463 \item {\textit {o}} type, 82 |
|
464 \item {\tt object}, 66 |
|
465 \item {\tt op} symbol, 79 |
|
466 \item {\tt option} ML type, 30 |
|
467 \item oracles, 66--68 |
|
468 \item {\tt ORELSE}, \bold{32}, 34, 38 |
|
469 \item {\tt ORELSE'}, 39 |
|
470 |
|
471 \indexspace |
|
472 |
|
473 \item parameters |
|
474 \subitem removing unused, 26 |
|
475 \subitem renaming, 15, 25, 52 |
|
476 \item {\tt parents_of}, \bold{61} |
|
477 \item parse trees, 85 |
|
478 \item {\tt parse_rules}, 92 |
|
479 \item pattern, higher-order, \bold{110} |
|
480 \item {\tt pause_tac}, \bold{30} |
|
481 \item Poly/{\ML} compiler, 7 |
|
482 \item {\tt pop_proof}, \bold{17} |
|
483 \item {\tt pr}, \bold{13} |
|
484 \item {\tt premises}, \bold{9}, 17 |
|
485 \item {\tt prems_of}, \bold{45} |
|
486 \item {\tt prems_of_ss}, \bold{113} |
|
487 \item pretty printing, 76, 78--79, 95 |
|
488 \item {\tt Pretty.setdepth}, \bold{5} |
|
489 \item {\tt Pretty.setmargin}, \bold{5} |
|
490 \item {\tt PRIMITIVE}, \bold{29} |
|
491 \item {\tt primrec}, 107 |
|
492 \item {\tt prin}, 7, \bold{18} |
|
493 \item print mode, 56, 99 |
|
494 \item print modes, 80--81 |
|
495 \item {\tt print_cs}, \bold{135} |
|
496 \item {\tt print_depth}, \bold{5} |
|
497 \item {\tt print_exn}, \bold{7}, 41 |
|
498 \item {\tt print_goals}, \bold{42} |
|
499 \item {\tt print_mode}, 80 |
|
500 \item {\tt print_modes}, 75 |
|
501 \item {\tt print_rules}, 92 |
|
502 \item {\tt print_simpset}, \bold{109} |
|
503 \item {\tt print_ss}, \bold{108} |
|
504 \item {\tt print_syntax}, \bold{61}, \bold{74} |
|
505 \item {\tt print_tac}, \bold{30} |
|
506 \item {\tt print_theory}, \bold{61} |
|
507 \item {\tt print_thm}, \bold{42} |
|
508 \item printing control, 4--6 |
|
509 \item {\tt printyp}, \bold{18} |
|
510 \item priorities, 69, \bold{76} |
|
511 \item priority grammars, 69--70 |
|
512 \item {\tt prlev}, \bold{13} |
|
513 \item {\tt prlim}, \bold{13} |
|
514 \item productions, 69, 75, 76 |
|
515 \subitem copy, \bold{75}, 76, 87 |
|
516 \item {\tt proof} ML type, 18 |
|
517 \item proof objects, 52--54 |
|
518 \item proof state, 8 |
|
519 \subitem printing of, 13 |
|
520 \item {\tt proof_timing}, \bold{14} |
|
521 \item proofs, 8--19 |
|
522 \subitem inspecting the state, 18 |
|
523 \subitem managing multiple, 17 |
|
524 \subitem saving and restoring, 18 |
|
525 \subitem stacking, 17 |
|
526 \subitem starting, 8 |
|
527 \subitem timing, 14 |
|
528 \item {\tt PROP} symbol, 71 |
|
529 \item {\textit {prop}} type, 65, 72 |
|
530 \item {\tt prop} nonterminal, \bold{70}, 82 |
|
531 \item {\tt ProtoPure.thy}, \bold{61} |
|
532 \item {\tt prove_goal}, 14, \bold{16} |
|
533 \item {\tt prove_goalw}, \bold{16} |
|
534 \item {\tt prove_goalw_cterm}, \bold{16} |
|
535 \item {\tt prth}, \bold{41} |
|
536 \item {\tt prthq}, \bold{42} |
|
537 \item {\tt prths}, \bold{42} |
|
538 \item {\tt prune_params_tac}, \bold{26} |
|
539 \item {\tt pttrn} nonterminal, \bold{72} |
|
540 \item {\tt pttrns} nonterminal, \bold{72} |
|
541 \item {\tt Pure} theory, 55, 70, 74 |
|
542 \item {\tt Pure.thy}, \bold{61} |
|
543 \item {\tt push_proof}, \bold{17} |
|
544 \item {\tt pwd}, \bold{3} |
|
545 |
|
546 \indexspace |
|
547 |
|
548 \item {\tt qed}, \bold{10}, 12 |
|
549 \item {\tt qed_goal}, \bold{16} |
|
550 \item {\tt qed_goalw}, \bold{16} |
|
551 \item quantifiers, 80 |
|
552 \item {\tt quit}, \bold{3} |
|
553 |
|
554 \indexspace |
|
555 |
|
556 \item {\tt read}, \bold{18} |
|
557 \item {\tt read_axm}, \bold{64} |
|
558 \item {\tt read_cterm}, \bold{64} |
|
559 \item {\tt read_instantiate}, \bold{43} |
|
560 \item {\tt read_instantiate_sg}, \bold{43} |
|
561 \item reading |
|
562 \subitem axioms, \see{{\tt assume_ax}}{55} |
|
563 \subitem goals, \see{proofs, starting}{8} |
|
564 \item {\tt reflexive}, \bold{49} |
|
565 \item {\tt ren}, \bold{15} |
|
566 \item {\tt rename_last_tac}, \bold{25} |
|
567 \item {\tt rename_params_rule}, \bold{52} |
|
568 \item {\tt rename_tac}, \bold{25} |
|
569 \item {\tt rep_cs}, \bold{135} |
|
570 \item {\tt rep_cterm}, \bold{64} |
|
571 \item {\tt rep_ctyp}, \bold{66} |
|
572 \item {\tt rep_ss}, \bold{108} |
|
573 \item {\tt rep_thm}, \bold{45} |
|
574 \item {\tt REPEAT}, \bold{33, 34} |
|
575 \item {\tt REPEAT1}, \bold{33} |
|
576 \item {\tt REPEAT_DETERM}, \bold{33} |
|
577 \item {\tt REPEAT_FIRST}, \bold{39} |
|
578 \item {\tt REPEAT_SOME}, \bold{38} |
|
579 \item {\tt res_inst_tac}, \bold{22}, 26, 27 |
|
580 \item reserved words, 72, 95 |
|
581 \item {\tt reset}, 4 |
|
582 \item {\tt reset_path}, \bold{60} |
|
583 \item resolution, 42, 51 |
|
584 \subitem tactics, 20 |
|
585 \subitem without lifting, 51 |
|
586 \item {\tt resolve_tac}, \bold{20}, 134 |
|
587 \item {\tt restore_proof}, \bold{18} |
|
588 \item {\tt result}, \bold{10}, 12, 18 |
|
589 \item {\tt rev_mp} theorem, \bold{104} |
|
590 \item rewrite rules, 110 |
|
591 \subitem permutative, 120--123 |
|
592 \item {\tt rewrite_goals_rule}, \bold{43} |
|
593 \item {\tt rewrite_goals_tac}, \bold{24}, 43 |
|
594 \item {\tt rewrite_rule}, \bold{43} |
|
595 \item {\tt rewrite_tac}, 10, \bold{24} |
|
596 \item rewriting |
|
597 \subitem object-level, \see{simplification}{1} |
|
598 \subitem ordered, 121 |
|
599 \subitem syntactic, 90--96 |
|
600 \item {\tt rewtac}, \bold{23} |
|
601 \item {\tt RL}, \bold{42} |
|
602 \item {\tt RLN}, \bold{42} |
|
603 \item {\tt rotate_prems}, \bold{44} |
|
604 \item {\tt rotate_proof}, \bold{17} |
|
605 \item {\tt rotate_tac}, \bold{26} |
|
606 \item {\tt RS}, \bold{42} |
|
607 \item {\tt RSN}, \bold{42} |
|
608 \item {\tt rtac}, \bold{23} |
|
609 \item {\tt rule_by_tactic}, 26, \bold{44} |
|
610 \item rules |
|
611 \subitem converting destruction to elimination, 44 |
|
612 |
|
613 \indexspace |
|
614 |
|
615 \item {\tt safe_asm_full_simp_tac}, \bold{116} |
|
616 \item {\tt Safe_step_tac}, \bold{142} |
|
617 \item {\tt safe_step_tac}, 136, \bold{141} |
|
618 \item {\tt Safe_tac}, \bold{142} |
|
619 \item {\tt safe_tac}, \bold{141} |
|
620 \item {\tt save_proof}, \bold{18} |
|
621 \item saving your session, \bold{2} |
|
622 \item search, 32 |
|
623 \subitem tacticals, 34--36 |
|
624 \item {\tt SELECT_GOAL}, 24, \bold{37} |
|
625 \item {\tt Seq.seq} ML type, 29 |
|
626 \item sequences (lazy lists), \bold{30} |
|
627 \item sequent calculus, 131 |
|
628 \item sessions, 1--7 |
|
629 \item {\tt set}, 4 |
|
630 \item {\tt setloop}, \bold{114} |
|
631 \item {\tt setmksimps}, 110, \bold{126}, 128 |
|
632 \item {\tt setSolver}, \bold{113}, 128 |
|
633 \item {\tt setSSolver}, \bold{113}, 128 |
|
634 \item {\tt setsubgoaler}, \bold{112}, 128 |
|
635 \item {\tt settermless}, \bold{121} |
|
636 \item {\tt setup} |
|
637 \subitem simplifier, 129 |
|
638 \subitem theory, 58 |
|
639 \item shortcuts |
|
640 \subitem for \texttt{by} commands, 14 |
|
641 \subitem for tactics, 23 |
|
642 \item {\tt show_brackets}, \bold{5} |
|
643 \item {\tt show_consts}, \bold{6} |
|
644 \item {\tt show_hyps}, \bold{5} |
|
645 \item {\tt show_path}, \bold{60} |
|
646 \item {\tt show_sorts}, \bold{5}, 89, 97 |
|
647 \item {\tt show_tags}, \bold{5} |
|
648 \item {\tt show_types}, \bold{5}, 89, 92, 99 |
|
649 \item {\tt Sign.certify_term}, \bold{64} |
|
650 \item {\tt Sign.certify_typ}, \bold{66} |
|
651 \item {\tt Sign.sg} ML type, 55 |
|
652 \item {\tt Sign.stamp_names_of}, \bold{61} |
|
653 \item {\tt Sign.string_of_term}, \bold{64} |
|
654 \item {\tt Sign.string_of_typ}, \bold{65} |
|
655 \item {\tt sign_of}, 9, 17, \bold{61} |
|
656 \item {\tt sign_of_thm}, \bold{45} |
|
657 \item signatures, \bold{55}, 61, 63, 64, 66 |
|
658 \item {\tt Simp_tac}, \bold{105} |
|
659 \item {\tt simp_tac}, \bold{116} |
|
660 \item simplification, 105--129 |
|
661 \subitem conversions, 116 |
|
662 \subitem forward rules, 116 |
|
663 \subitem from classical reasoner, 137 |
|
664 \subitem setting up, 125 |
|
665 \subitem setting up the splitter, 129 |
|
666 \subitem setting up the theory, 129 |
|
667 \subitem tactics, 115 |
|
668 \item simplification sets, 108 |
|
669 \item {\tt Simplifier.asm_full_rewrite}, 116 |
|
670 \item {\tt Simplifier.asm_rewrite}, 116 |
|
671 \item {\tt Simplifier.full_rewrite}, 116 |
|
672 \item {\tt Simplifier.rewrite}, 116 |
|
673 \item {\tt Simplifier.setup}, \bold{129} |
|
674 \item {\tt simplify}, 116 |
|
675 \item {\tt SIMPSET}, \bold{109} |
|
676 \item simpset |
|
677 \subitem current, 105, 109 |
|
678 \item {\tt simpset}, \bold{109} |
|
679 \item {\tt SIMPSET'}, \bold{109} |
|
680 \item {\tt simpset_of}, \bold{109} |
|
681 \item {\tt simpset_ref}, \bold{109} |
|
682 \item {\tt simpset_ref_of}, \bold{109} |
|
683 \item {\tt size_of_thm}, 35, \bold{36}, 143 |
|
684 \item {\tt sizef}, \bold{143} |
|
685 \item {\tt slow_best_tac}, \bold{140} |
|
686 \item {\tt slow_step_tac}, 136, \bold{141} |
|
687 \item {\tt slow_tac}, \bold{140} |
|
688 \item {\tt SOLVE}, \bold{36} |
|
689 \item {\tt Some}, \bold{30} |
|
690 \item {\tt SOMEGOAL}, \bold{38} |
|
691 \item {\tt sort} nonterminal, \bold{72} |
|
692 \item sort constraints, 71 |
|
693 \item sort hypotheses, 45, 47 |
|
694 \item sorts |
|
695 \subitem printing of, 5 |
|
696 \item {\tt ssubst} theorem, \bold{101} |
|
697 \item {\tt stac}, \bold{102} |
|
698 \item stamps, \bold{55}, 61 |
|
699 \item {\tt standard}, \bold{44} |
|
700 \item starting up, \bold{1} |
|
701 \item {\tt Step_tac}, \bold{142} |
|
702 \item {\tt step_tac}, 136, \bold{141} |
|
703 \item {\tt store_thm}, \bold{11} |
|
704 \item {\tt string_of_cterm}, \bold{64} |
|
705 \item {\tt string_of_ctyp}, \bold{65} |
|
706 \item {\tt string_of_thm}, \bold{42} |
|
707 \item strings, 72 |
|
708 \item {\tt SUBGOAL}, \bold{29} |
|
709 \item subgoal module, 8--19 |
|
710 \item {\tt subgoal_tac}, \bold{23} |
|
711 \item {\tt subgoals_of_brl}, \bold{27} |
|
712 \item {\tt subgoals_tac}, \bold{24} |
|
713 \item {\tt subst} theorem, 101, \bold{104} |
|
714 \item substitution |
|
715 \subitem rules, 101 |
|
716 \item {\tt subthy}, \bold{60} |
|
717 \item {\tt swap} theorem, \bold{143} |
|
718 \item {\tt swap_res_tac}, \bold{143} |
|
719 \item {\tt swapify}, \bold{143} |
|
720 \item {\tt sym} theorem, 102, \bold{104} |
|
721 \item {\tt symmetric}, \bold{49} |
|
722 \item {\tt syn_of}, \bold{74} |
|
723 \item syntax |
|
724 \subitem Pure, 70--75 |
|
725 \subitem transformations, 85--99 |
|
726 \item {\tt syntax} section, 56 |
|
727 \item {\tt Syntax.ast} ML type, 85 |
|
728 \item {\tt Syntax.mark_boundT}, 99 |
|
729 \item {\tt Syntax.print_gram}, \bold{74} |
|
730 \item {\tt Syntax.print_syntax}, \bold{74} |
|
731 \item {\tt Syntax.print_trans}, \bold{74} |
|
732 \item {\tt Syntax.stat_norm_ast}, 94 |
|
733 \item {\tt Syntax.syntax} ML type, 74 |
|
734 \item {\tt Syntax.test_read}, 78, 94 |
|
735 \item {\tt Syntax.trace_norm_ast}, 94 |
|
736 \item {\tt Syntax.variant_abs'}, 99 |
|
737 |
|
738 \indexspace |
|
739 |
|
740 \item {\tt tactic} ML type, 20 |
|
741 \item tacticals, 32--40 |
|
742 \subitem conditional, 36 |
|
743 \subitem deterministic, 36 |
|
744 \subitem for filtering, 34 |
|
745 \subitem for restriction to a subgoal, 37 |
|
746 \subitem identities for, 33 |
|
747 \subitem joining a list of tactics, 33 |
|
748 \subitem joining tactic functions, 39 |
|
749 \subitem joining two tactics, 32 |
|
750 \subitem repetition, 33 |
|
751 \subitem scanning for subgoals, 38 |
|
752 \subitem searching, 35 |
|
753 \item tactics, 20--31 |
|
754 \subitem assumption, \bold{21}, 23 |
|
755 \subitem commands for applying, 9 |
|
756 \subitem debugging, 18 |
|
757 \subitem filtering results of, 34 |
|
758 \subitem for composition, 27 |
|
759 \subitem for contradiction, 142 |
|
760 \subitem for inserting facts, 23 |
|
761 \subitem for Modus Ponens, 142 |
|
762 \subitem instantiation, 22 |
|
763 \subitem matching, 21 |
|
764 \subitem meta-rewriting, 23, \bold{24} |
|
765 \subitem primitives for coding, 29 |
|
766 \subitem resolution, \bold{20}, 23, 27, 28 |
|
767 \subitem restricting to a subgoal, 37 |
|
768 \subitem simplification, 115 |
|
769 \subitem substitution, 101--104 |
|
770 \subitem tracing, 30 |
|
771 \item {\tt TERM}, 64 |
|
772 \item {\tt term} ML type, 62, 88 |
|
773 \item terms, \bold{62} |
|
774 \subitem certified, \bold{63} |
|
775 \subitem made from ASTs, 88 |
|
776 \subitem printing of, 18, 64 |
|
777 \subitem reading of, 18 |
|
778 \item {\tt TFree}, \bold{65} |
|
779 \item {\tt the_context}, \bold{4} |
|
780 \item {\tt THEN}, \bold{32}, 34, 38 |
|
781 \item {\tt THEN'}, 39 |
|
782 \item {\tt THEN_BEST_FIRST}, \bold{35} |
|
783 \item theorems, 41--54 |
|
784 \subitem equality of, 36 |
|
785 \subitem extracting, 11 |
|
786 \subitem extracting proved, 10 |
|
787 \subitem joining by resolution, 42 |
|
788 \subitem of pure theory, 25 |
|
789 \subitem printing of, 41 |
|
790 \subitem retrieving, 12 |
|
791 \subitem size of, 36 |
|
792 \subitem standardizing, 44 |
|
793 \subitem storing, 11 |
|
794 \subitem taking apart, 44 |
|
795 \item theories, 55--68 |
|
796 \subitem axioms of, 11 |
|
797 \subitem inspecting, \bold{61} |
|
798 \subitem parent, \bold{55} |
|
799 \subitem reading, 3, 59 |
|
800 \subitem theorems of, 11 |
|
801 \item {\tt THEORY} exception, 11, 55 |
|
802 \item {\tt theory}, \bold{4} |
|
803 \item {\tt theory} ML type, 55 |
|
804 \item {\tt Theory.add_oracle}, \bold{66} |
|
805 \item {\tt theory_of_thm}, \bold{45} |
|
806 \item {\tt thin_refl} theorem, \bold{104} |
|
807 \item {\tt thin_tac}, \bold{26} |
|
808 \item {\tt THM} exception, 41, 42, 46, 51 |
|
809 \item {\tt thm}, \bold{11} |
|
810 \item {\tt thm} ML type, 41 |
|
811 \item {\tt thms}, \bold{11} |
|
812 \item {\tt thms_containing}, \bold{12} |
|
813 \item {\tt thms_of}, \bold{11} |
|
814 \item {\tt tid} nonterminal, \bold{72}, 86, 93 |
|
815 \item {\tt time_use}, \bold{3} |
|
816 \item {\tt time_use_thy}, \bold{4} |
|
817 \item timing statistics, 14 |
|
818 \item {\tt toggle}, 4 |
|
819 \item token class, 99 |
|
820 \item token translations, 99--100 |
|
821 \item token_translation, 100 |
|
822 \item {\tt token_translation}, 100 |
|
823 \item {\tt topthm}, \bold{18} |
|
824 \item {\tt touch_thy}, \bold{59} |
|
825 \item {\tt tpairs_of}, \bold{45} |
|
826 \item {\tt trace_BEST_FIRST}, \bold{35} |
|
827 \item {\tt trace_DEPTH_FIRST}, \bold{35} |
|
828 \item {\tt trace_goalno_tac}, \bold{39} |
|
829 \item {\tt trace_REPEAT}, \bold{33} |
|
830 \item {\tt trace_simp}, \bold{106}, 118 |
|
831 \item tracing |
|
832 \subitem of classical prover, 139 |
|
833 \subitem of macros, 94 |
|
834 \subitem of searching tacticals, 35 |
|
835 \subitem of simplification, 107, 118--119 |
|
836 \subitem of tactics, 30 |
|
837 \subitem of unification, 46 |
|
838 \item {\tt transfer}, \bold{60} |
|
839 \item {\tt transfer_sg}, \bold{61} |
|
840 \item {\tt transitive}, \bold{49} |
|
841 \item translations, 96--99 |
|
842 \subitem parse, 80, 88 |
|
843 \subitem parse AST, \bold{86}, 87 |
|
844 \subitem print, 80 |
|
845 \subitem print AST, \bold{89} |
|
846 \item {\tt translations} section, 91 |
|
847 \item {\tt trivial}, \bold{52} |
|
848 \item {\tt Trueprop} constant, 82 |
|
849 \item {\tt TRY}, \bold{33, 34} |
|
850 \item {\tt TRYALL}, \bold{38} |
|
851 \item {\tt TVar}, \bold{65} |
|
852 \item {\tt tvar} nonterminal, \bold{72, 73}, 86, 93 |
|
853 \item {\tt typ} ML type, 65 |
|
854 \item {\tt Type}, \bold{65} |
|
855 \item {\textit {type}} type, 77 |
|
856 \item {\tt type} nonterminal, \bold{72} |
|
857 \item type constraints, 72, 80, 89 |
|
858 \item type constructors, \bold{65} |
|
859 \item type identifiers, 72 |
|
860 \item type synonyms, \bold{56} |
|
861 \item type unknowns, \bold{65}, 72 |
|
862 \subitem freezing/thawing of, 50 |
|
863 \item type variables, \bold{65} |
|
864 \item types, \bold{65} |
|
865 \subitem certified, \bold{65} |
|
866 \subitem printing of, 5, 18, 65 |
|
867 |
|
868 \indexspace |
|
869 |
|
870 \item {\tt undo}, 8, \bold{13}, 17 |
|
871 \item unknowns, \bold{62}, 72 |
|
872 \item {\tt update_thy}, \bold{59} |
|
873 \item {\tt uresult}, \bold{10}, 12, 18 |
|
874 \item {\tt use}, \bold{3} |
|
875 \item {\tt use_thy}, \bold{4} |
|
876 \item {\tt use_thy_only}, \bold{59} |
|
877 |
|
878 \indexspace |
|
879 |
|
880 \item {\tt Var}, \bold{62}, 88 |
|
881 \item {\tt var} nonterminal, \bold{72, 73}, 86, 93 |
|
882 \item {\tt Variable}, 85 |
|
883 \item variables |
|
884 \subitem bound, \bold{62} |
|
885 \subitem free, \bold{62} |
|
886 \item {\tt variant_abs}, \bold{63} |
|
887 \item {\tt varifyT}, \bold{50} |
|
888 |
|
889 \indexspace |
|
890 |
|
891 \item {\tt warning}, 6 |
|
892 \item warnings, 6 |
|
893 \item {\tt writeln}, 6 |
|
894 |
|
895 \indexspace |
|
896 |
|
897 \item {\tt xnum} nonterminal, \bold{72}, 86, 93 |
|
898 \item {\tt xstr} nonterminal, \bold{72}, 86, 93 |
|
899 |
|
900 \indexspace |
|
901 |
|
902 \item {\tt zero_var_indexes}, \bold{44} |
|
903 |
|
904 \end{theindex} |
|