47 \item abandoning a theory, \bold{14} |
47 \item abandoning a theory, \bold{14} |
48 \item \isa {abs} (constant), 135 |
48 \item \isa {abs} (constant), 135 |
49 \item \texttt {abs}, \bold{189} |
49 \item \texttt {abs}, \bold{189} |
50 \item absolute value, 135 |
50 \item absolute value, 135 |
51 \item \isa {add} (modifier), 27 |
51 \item \isa {add} (modifier), 27 |
|
52 \item \isa {add_ac} (theorems), 134 |
52 \item \isa {add_assoc} (theorem), \bold{134} |
53 \item \isa {add_assoc} (theorem), \bold{134} |
53 \item \isa {add_commute} (theorem), \bold{134} |
54 \item \isa {add_commute} (theorem), \bold{134} |
54 \item \isa {add_mult_distrib} (theorem), \bold{133} |
55 \item \isa {add_mult_distrib} (theorem), \bold{133} |
55 \item \texttt {ALL}, \bold{189} |
56 \item \texttt {ALL}, \bold{189} |
56 \item \isa {All} (constant), 93 |
57 \item \isa {All} (constant), 93 |
131 \item \isacommand {consts} (command), 8 |
132 \item \isacommand {consts} (command), 8 |
132 \item contrapositives, 57 |
133 \item contrapositives, 57 |
133 \item converse |
134 \item converse |
134 \subitem of a relation, \bold{96} |
135 \subitem of a relation, \bold{96} |
135 \item \isa {converse_iff} (theorem), \bold{96} |
136 \item \isa {converse_iff} (theorem), \bold{96} |
136 \item CTL, 100--110 |
|
137 |
137 |
138 \indexspace |
138 \indexspace |
139 |
139 |
140 \item \isacommand {datatype} (command), 7, 36--41 |
140 \item \isacommand {datatype} (command), 7, 36--41 |
141 \item datatypes, 15--20 |
141 \item datatypes, 15--20 |
142 \subitem and nested recursion, 38 |
142 \subitem and nested recursion, 38, 42 |
143 \subitem mutually recursive, 36 |
143 \subitem mutually recursive, 36 |
144 \item \isacommand {defer} (command), 14, 84 |
144 \item \isacommand {defer} (command), 14, 84 |
145 \item Definitional Approach, 24 |
145 \item Definitional Approach, 24 |
146 \item definitions, \bold{23} |
146 \item definitions, \bold{23} |
147 \subitem unfolding, \bold{28} |
147 \subitem unfolding, \bold{28} |
202 \item \ttEXU, \bold{189} |
202 \item \ttEXU, \bold{189} |
203 |
203 |
204 \indexspace |
204 \indexspace |
205 |
205 |
206 \item \isa {False} (constant), 3 |
206 \item \isa {False} (constant), 3 |
207 \item \isa {fast} (method), 76 |
207 \item \isa {fast} (method), 76, 108 |
208 \item Fibonacci function, 44 |
208 \item Fibonacci function, 44 |
209 \item \isa {finite} (symbol), 93 |
209 \item \isa {finite} (symbol), 93 |
210 \item \isa {Finites} (constant), 93 |
210 \item \isa {Finites} (constant), 93 |
211 \item fixed points, 100 |
211 \item fixed points, 100 |
212 \item flags, 3, 4, 31 |
212 \item flags, 3, 4, 31 |
227 \item \isa {gcd} (constant), 77--78, 85--88 |
227 \item \isa {gcd} (constant), 77--78, 85--88 |
228 \item generalizing for induction, 113 |
228 \item generalizing for induction, 113 |
229 \item generalizing induction formulae, 32 |
229 \item generalizing induction formulae, 32 |
230 \item Girard, Jean-Yves, \fnote{55} |
230 \item Girard, Jean-Yves, \fnote{55} |
231 \item Gordon, Mike, 1 |
231 \item Gordon, Mike, 1 |
|
232 \item grammars |
|
233 \subitem defining inductively, 124--129 |
232 \item ground terms example, 119--124 |
234 \item ground terms example, 119--124 |
233 |
235 |
234 \indexspace |
236 \indexspace |
235 |
237 |
236 \item \isa {hd} (constant), 15, 35 |
238 \item \isa {hd} (constant), 15, 35 |
237 \item higher-order pattern, \bold{159} |
239 \item higher-order pattern, \bold{159} |
238 \item Hilbert's $\varepsilon$-operator, 70 |
240 \item Hilbert's $\varepsilon$-operator, 70 |
239 \item HOLCF, 41 |
241 \item HOLCF, 41 |
|
242 \item Hopcroft, J. E., 129 |
240 \item \isa {hypreal} (type), 137 |
243 \item \isa {hypreal} (type), 137 |
241 |
244 |
242 \indexspace |
245 \indexspace |
243 |
246 |
244 \item \isa {Id_def} (theorem), \bold{96} |
247 \item \isa {Id_def} (theorem), \bold{96} |
247 \subitem qualified, \bold{2} |
250 \subitem qualified, \bold{2} |
248 \item identity function, \bold{94} |
251 \item identity function, \bold{94} |
249 \item identity relation, \bold{96} |
252 \item identity relation, \bold{96} |
250 \item \isa {if} expressions, 3, 4 |
253 \item \isa {if} expressions, 3, 4 |
251 \subitem simplification of, 31 |
254 \subitem simplification of, 31 |
252 \subitem splitting of, 29 |
255 \subitem splitting of, 29, 47 |
253 \item if-and-only-if, 3 |
256 \item if-and-only-if, 3 |
254 \item \isa {iff} (attribute), 74, 86, 114 |
257 \item \isa {iff} (attribute), 74, 86, 114 |
255 \item \isa {iffD1} (theorem), \bold{78} |
258 \item \isa {iffD1} (theorem), \bold{78} |
256 \item \isa {iffD2} (theorem), \bold{78} |
259 \item \isa {iffD2} (theorem), \bold{78} |
257 \item image |
260 \item image |
259 \subitem under a relation, \bold{96} |
262 \subitem under a relation, \bold{96} |
260 \item \isa {image_def} (theorem), \bold{95} |
263 \item \isa {image_def} (theorem), \bold{95} |
261 \item \isa {Image_iff} (theorem), \bold{96} |
264 \item \isa {Image_iff} (theorem), \bold{96} |
262 \item \isa {impI} (theorem), \bold{56} |
265 \item \isa {impI} (theorem), \bold{56} |
263 \item implication, 56--57 |
266 \item implication, 56--57 |
|
267 \item \isa {ind_cases} (method), 115 |
264 \item \isa {induct_tac} (method), 10, 17, 50, 172 |
268 \item \isa {induct_tac} (method), 10, 17, 50, 172 |
265 \item induction, 168--175 |
269 \item induction, 168--175 |
266 \subitem recursion, 49--50 |
270 \subitem recursion, 49--50 |
267 \subitem structural, 17 |
271 \subitem structural, 17 |
268 \subitem well-founded, 99 |
272 \subitem well-founded, 99 |
337 \indexspace |
341 \indexspace |
338 |
342 |
339 \item \isa {Main} (theory), 2 |
343 \item \isa {Main} (theory), 2 |
340 \item major premise, \bold{59} |
344 \item major premise, \bold{59} |
341 \item \isa {max} (constant), 21, 22 |
345 \item \isa {max} (constant), 21, 22 |
342 \item measure function, \bold{45}, \bold{98} |
346 \item measure functions, 45, 98 |
343 \item \isa {measure_def} (theorem), \bold{99} |
347 \item \isa {measure_def} (theorem), \bold{99} |
344 \item meta-logic, \bold{64} |
348 \item meta-logic, \bold{64} |
345 \item methods, \bold{14} |
349 \item methods, \bold{14} |
346 \item \isa {min} (constant), 21, 22 |
350 \item \isa {min} (constant), 21, 22 |
347 \item \isa {mod} (symbol), 21 |
351 \item \isa {mod} (symbol), 21 |
348 \item \isa {mod_div_equality} (theorem), \bold{133} |
352 \item \isa {mod_div_equality} (theorem), \bold{133} |
349 \item \isa {mod_mult_distrib} (theorem), \bold{133} |
353 \item \isa {mod_mult_distrib} (theorem), \bold{133} |
|
354 \item model checking example, 100--110 |
350 \item \emph{modus ponens}, 51, 56 |
355 \item \emph{modus ponens}, 51, 56 |
351 \item \isa {mono_def} (theorem), \bold{100} |
356 \item \isa {mono_def} (theorem), \bold{100} |
352 \item monotone functions, \bold{100}, 123 |
357 \item monotone functions, \bold{100}, 123 |
353 \subitem and inductive definitions, 121--122 |
358 \subitem and inductive definitions, 121--122 |
354 \item \isa {more} (constant), 140--142 |
359 \item \isa {more} (constant), 140--142 |
355 \item \isa {mp} (theorem), \bold{56} |
360 \item \isa {mp} (theorem), \bold{56} |
|
361 \item \isa {mult_ac} (theorems), 134 |
356 \item multiset ordering, \bold{99} |
362 \item multiset ordering, \bold{99} |
357 |
363 |
358 \indexspace |
364 \indexspace |
359 |
365 |
360 \item \isa {nat} (type), 2, 20, 133--134 |
366 \item \isa {nat} (type), 2, 20, 133--134 |
368 \item \isa {no_asm_use} (modifier), 27 |
374 \item \isa {no_asm_use} (modifier), 27 |
369 \item non-standard reals, 137 |
375 \item non-standard reals, 137 |
370 \item \isa {None} (constant), \bold{22} |
376 \item \isa {None} (constant), \bold{22} |
371 \item \isa {notE} (theorem), \bold{57} |
377 \item \isa {notE} (theorem), \bold{57} |
372 \item \isa {notI} (theorem), \bold{57} |
378 \item \isa {notI} (theorem), \bold{57} |
|
379 \item numbers, 131--137 |
373 \item numeric literals, 132 |
380 \item numeric literals, 132 |
374 \subitem for type \protect\isa{nat}, 133 |
381 \subitem for type \protect\isa{nat}, 133 |
375 \subitem for type \protect\isa{real}, 136 |
382 \subitem for type \protect\isa{real}, 136 |
376 |
383 |
377 \indexspace |
384 \indexspace |
391 \indexspace |
398 \indexspace |
392 |
399 |
393 \item pairs and tuples, 22, 137--140 |
400 \item pairs and tuples, 22, 137--140 |
394 \item parent theories, \bold{2} |
401 \item parent theories, \bold{2} |
395 \item partial function, 164 |
402 \item partial function, 164 |
|
403 \item pattern matching |
|
404 \subitem and \isacommand{recdef}, 45 |
396 \item pattern, higher-order, \bold{159} |
405 \item pattern, higher-order, \bold{159} |
397 \item PDL, 102--105 |
406 \item PDL, 102--104 |
398 \item permutative rewrite rule, \bold{158} |
407 \item permutative rewrite rule, \bold{158} |
399 \item \isacommand {pr} (command), 14, 84 |
408 \item \isacommand {pr} (command), 14, 84 |
400 \item \isacommand {prefer} (command), 14, 84 |
409 \item \isacommand {prefer} (command), 14, 84 |
401 \item primitive recursion, \see{recursion, primitive}{1} |
410 \item primitive recursion, \see{recursion, primitive}{1} |
402 \item \isacommand {primrec} (command), 8, 16, 36--41 |
411 \item \isacommand {primrec} (command), 8, 16, 36--41 |
443 \subitem primitive, 16 |
452 \subitem primitive, 16 |
444 \subitem well-founded, \bold{161} |
453 \subitem well-founded, \bold{161} |
445 \item recursion induction, 49--50 |
454 \item recursion induction, 49--50 |
446 \item \isacommand {redo} (command), 14 |
455 \item \isacommand {redo} (command), 14 |
447 \item reflexive and transitive closure, 96--98 |
456 \item reflexive and transitive closure, 96--98 |
|
457 \item reflexive transitive closure |
|
458 \subitem defining inductively, 116--119 |
448 \item relations, 95--98 |
459 \item relations, 95--98 |
449 \subitem well-founded, 98--99 |
460 \subitem well-founded, 98--99 |
450 \item \isa {rename_tac} (method), 66--67 |
461 \item \isa {rename_tac} (method), 66--67 |
451 \item \isa {rev} (constant), 8--12, 32 |
462 \item \isa {rev} (constant), 8--12, 32 |
452 \item rewrite rule |
463 \item rewrite rule |
498 \item \isa {someI2} (theorem), \bold{70} |
509 \item \isa {someI2} (theorem), \bold{70} |
499 \item \isa {someI_ex} (theorem), \bold{71} |
510 \item \isa {someI_ex} (theorem), \bold{71} |
500 \item sorts, 150 |
511 \item sorts, 150 |
501 \item \isa {spec} (theorem), \bold{64} |
512 \item \isa {spec} (theorem), \bold{64} |
502 \item \isa {split} (attribute), 30 |
513 \item \isa {split} (attribute), 30 |
503 \item \isa {split} (constant), \bold{137} |
514 \item \isa {split} (constant), 137 |
504 \item \isa {split} (method), 29 |
515 \item \isa {split} (method), 29, 138 |
505 \item \isa {split} (method, attr.), 29--31 |
516 \item \isa {split} (modifier), 30 |
506 \item \isa {split} (modified), 30 |
|
507 \item split rule, \bold{30} |
517 \item split rule, \bold{30} |
508 \item \isa {split_if} (theorem), 30 |
518 \item \isa {split_if} (theorem), 30 |
509 \item \isa {split_if_asm} (theorem), 30 |
519 \item \isa {split_if_asm} (theorem), 30 |
510 \item \isa {ssubst} (theorem), \bold{61} |
520 \item \isa {ssubst} (theorem), \bold{61} |
511 \item structural induction, \see{induction, structural}{1} |
521 \item structural induction, \see{induction, structural}{1} |
|
522 \item subgoal numbering, 44 |
512 \item \isa {subgoal_tac} (method), 82 |
523 \item \isa {subgoal_tac} (method), 82 |
513 \item subgoals, 10 |
524 \item subgoals, 10 |
514 \item subset relation, \bold{90} |
525 \item subset relation, \bold{90} |
515 \item \isa {subsetD} (theorem), \bold{90} |
526 \item \isa {subsetD} (theorem), \bold{90} |
516 \item \isa {subsetI} (theorem), \bold{90} |
527 \item \isa {subsetI} (theorem), \bold{90} |
543 \item \isa {tl} (constant), 15 |
554 \item \isa {tl} (constant), 15 |
544 \item \isa {ToyList} example, 7--13 |
555 \item \isa {ToyList} example, 7--13 |
545 \item \isa {trace_simp} (flag), 31 |
556 \item \isa {trace_simp} (flag), 31 |
546 \item tracing the simplifier, \bold{31} |
557 \item tracing the simplifier, \bold{31} |
547 \item \isa {trancl_trans} (theorem), \bold{97} |
558 \item \isa {trancl_trans} (theorem), \bold{97} |
|
559 \item transition systems, 101 |
548 \item \isacommand {translations} (command), 24 |
560 \item \isacommand {translations} (command), 24 |
549 \item tries, 41--44 |
561 \item tries, 41--44 |
550 \item \isa {True} (constant), 3 |
562 \item \isa {True} (constant), 3 |
551 \item tuples, \see{pairs and tuples}{1} |
563 \item tuples, \see{pairs and tuples}{1} |
552 \item \isacommand {typ} (command), 14 |
564 \item \isacommand {typ} (command), 14 |
553 \item type constraints, \bold{4} |
565 \item type constraints, \bold{4} |
554 \item type constructors, 2 |
566 \item type constructors, 2 |
555 \item type inference, \bold{3} |
567 \item type inference, \bold{3} |
556 \item type synonyms, 23 |
568 \item type synonyms, 23 |
557 \item type variables, 3 |
569 \item type variables, 3 |
558 \item \isacommand {typedecl} (command), 150 |
570 \item \isacommand {typedecl} (command), 101, 150 |
559 \item \isacommand {typedef} (command), 151--155 |
571 \item \isacommand {typedef} (command), 151--155 |
560 \item types, 2--3 |
572 \item types, 2--3 |
561 \subitem declaring, 150--151 |
573 \subitem declaring, 150--151 |
562 \subitem defining, 151--155 |
574 \subitem defining, 151--155 |
563 \item \isacommand {types} (command), 23 |
575 \item \isacommand {types} (command), 23 |
564 |
576 |
565 \indexspace |
577 \indexspace |
566 |
578 |
|
579 \item Ullman, J. D., 129 |
567 \item \texttt {UN}, \bold{189} |
580 \item \texttt {UN}, \bold{189} |
568 \item \texttt {Un}, \bold{189} |
581 \item \texttt {Un}, \bold{189} |
569 \item \isa {UN_E} (theorem), \bold{92} |
582 \item \isa {UN_E} (theorem), \bold{92} |
570 \item \isa {UN_I} (theorem), \bold{92} |
583 \item \isa {UN_I} (theorem), \bold{92} |
571 \item \isa {UN_iff} (theorem), \bold{92} |
584 \item \isa {UN_iff} (theorem), \bold{92} |
591 |
604 |
592 \indexspace |
605 \indexspace |
593 |
606 |
594 \item Wenzel, Markus, v |
607 \item Wenzel, Markus, v |
595 \item \isa {wf_induct} (theorem), \bold{99} |
608 \item \isa {wf_induct} (theorem), \bold{99} |
|
609 \item \isa {wf_inv_image} (theorem), \bold{99} |
|
610 \item \isa {wf_less_than} (theorem), \bold{98} |
|
611 \item \isa {wf_lex_prod} (theorem), \bold{99} |
|
612 \item \isa {wf_measure} (theorem), \bold{99} |
596 \item \isa {while} (constant), 167 |
613 \item \isa {while} (constant), 167 |
597 \item \isa {While_Combinator} (theory), 167 |
614 \item \isa {While_Combinator} (theory), 167 |
598 |
615 |
|
616 \indexspace |
|
617 |
|
618 \item \isa {zadd_ac} (theorems), 135 |
|
619 \item \isa {zmult_ac} (theorems), 135 |
|
620 |
599 \end{theindex} |
621 \end{theindex} |