88 \item binary trees, 18 |
88 \item binary trees, 18 |
89 \item binomial coefficients, 99 |
89 \item binomial coefficients, 99 |
90 \item bisimulations, 106 |
90 \item bisimulations, 106 |
91 \item \isa {blast} (method), 79--80, 82 |
91 \item \isa {blast} (method), 79--80, 82 |
92 \item \isa {bool} (type), 4, 5 |
92 \item \isa {bool} (type), 4, 5 |
93 \item boolean expressions example, 19--22 |
93 \item boolean expressions example, 20--22 |
94 \item \isa {bspec} (theorem), \bold{98} |
94 \item \isa {bspec} (theorem), \bold{98} |
95 \item \isacommand{by} (command), 63 |
95 \item \isacommand{by} (command), 63 |
96 |
96 |
97 \indexspace |
97 \indexspace |
98 |
98 |
211 \item \isa {Finites} (constant), 99 |
211 \item \isa {Finites} (constant), 99 |
212 \item fixed points, 106 |
212 \item fixed points, 106 |
213 \item flags, 5, 6, 33 |
213 \item flags, 5, 6, 33 |
214 \subitem setting and resetting, 5 |
214 \subitem setting and resetting, 5 |
215 \item \isa {force} (method), 81, 82 |
215 \item \isa {force} (method), 81, 82 |
216 \item formulae, 5 |
216 \item formulae, 5--6 |
217 \item forward proof, 82--88 |
217 \item forward proof, 82--88 |
218 \item \isa {frule} (method), 73 |
218 \item \isa {frule} (method), 73 |
219 \item \isa {frule_tac} (method), 66 |
219 \item \isa {frule_tac} (method), 66 |
220 \item \isa {fst} (constant), 24 |
220 \item \isa {fst} (constant), 24 |
221 \item function types, 5 |
221 \item function types, 5 |
252 \item identity function, \bold{100} |
252 \item identity function, \bold{100} |
253 \item identity relation, \bold{102} |
253 \item identity relation, \bold{102} |
254 \item \isa {if} expressions, 5, 6 |
254 \item \isa {if} expressions, 5, 6 |
255 \subitem simplification of, 33 |
255 \subitem simplification of, 33 |
256 \subitem splitting of, 31, 49 |
256 \subitem splitting of, 31, 49 |
257 \item if-and-only-if, 5 |
257 \item if-and-only-if, 6 |
258 \item \isa {iff} (attribute), 80, 92, 120 |
258 \item \isa {iff} (attribute), 80, 92, 120 |
259 \item \isa {iffD1} (theorem), \bold{84} |
259 \item \isa {iffD1} (theorem), \bold{84} |
260 \item \isa {iffD2} (theorem), \bold{84} |
260 \item \isa {iffD2} (theorem), \bold{84} |
261 \item image |
261 \item image |
262 \subitem under a function, \bold{101} |
262 \subitem under a function, \bold{101} |
264 \item \isa {image_def} (theorem), \bold{101} |
264 \item \isa {image_def} (theorem), \bold{101} |
265 \item \isa {Image_iff} (theorem), \bold{102} |
265 \item \isa {Image_iff} (theorem), \bold{102} |
266 \item \isa {impI} (theorem), \bold{62} |
266 \item \isa {impI} (theorem), \bold{62} |
267 \item implication, 62--63 |
267 \item implication, 62--63 |
268 \item \isa {ind_cases} (method), 121 |
268 \item \isa {ind_cases} (method), 121 |
269 \item \isa {induct_tac} (method), 12, 19, 52, 178 |
269 \item \isa {induct_tac} (method), 12, 19, 51, 178 |
270 \item induction, 174--181 |
270 \item induction, 174--181 |
271 \subitem complete, 176 |
271 \subitem complete, 176 |
272 \subitem deriving new schemas, 178 |
272 \subitem deriving new schemas, 178 |
273 \subitem on a term, 175 |
273 \subitem on a term, 175 |
274 \subitem recursion, 51--52 |
274 \subitem recursion, 51--52 |
324 \item LCF, 43 |
324 \item LCF, 43 |
325 \item \isa {LEAST} (symbol), 23, 75 |
325 \item \isa {LEAST} (symbol), 23, 75 |
326 \item least number operator, \see{\protect\isa{LEAST}}{75} |
326 \item least number operator, \see{\protect\isa{LEAST}}{75} |
327 \item \isacommand {lemma} (command), 13 |
327 \item \isacommand {lemma} (command), 13 |
328 \item \isacommand {lemmas} (command), 83, 92 |
328 \item \isacommand {lemmas} (command), 83, 92 |
329 \item \isa {length} (symbol), 17 |
329 \item \isa {length} (symbol), 18 |
330 \item \isa {length_induct}, \bold{178} |
330 \item \isa {length_induct}, \bold{178} |
331 \item \isa {less_than} (constant), 104 |
331 \item \isa {less_than} (constant), 104 |
332 \item \isa {less_than_iff} (theorem), \bold{104} |
332 \item \isa {less_than_iff} (theorem), \bold{104} |
333 \item \isa {let} expressions, 5, 6, 31 |
333 \item \isa {let} expressions, 5, 6, 31 |
334 \item \isa {Let_def} (theorem), 31 |
334 \item \isa {Let_def} (theorem), 31 |
335 \item \isa {lex_prod_def} (theorem), \bold{105} |
335 \item \isa {lex_prod_def} (theorem), \bold{105} |
336 \item lexicographic product, \bold{105}, 166 |
336 \item lexicographic product, \bold{105}, 166 |
337 \item {\texttt{lfp}} |
337 \item {\texttt{lfp}} |
338 \subitem applications of, \see{CTL}{106} |
338 \subitem applications of, \see{CTL}{106} |
|
339 \item Library, 4 |
339 \item linear arithmetic, 22--24, 139 |
340 \item linear arithmetic, 22--24, 139 |
340 \item \isa {List} (theory), 17 |
341 \item \isa {List} (theory), 17 |
341 \item \isa {list} (type), 4, 9, 17 |
342 \item \isa {list} (type), 5, 9, 17 |
342 \item \isa {list.split} (theorem), 32 |
343 \item \isa {list.split} (theorem), 32 |
343 \item \isa {lists_mono} (theorem), \bold{127} |
344 \item \isa {lists_mono} (theorem), \bold{127} |
344 \item Lowe, Gavin, 184--185 |
345 \item Lowe, Gavin, 184--185 |
345 |
346 |
346 \indexspace |
347 \indexspace |
349 \item major premise, \bold{65} |
350 \item major premise, \bold{65} |
350 \item \isa {max} (constant), 23, 24 |
351 \item \isa {max} (constant), 23, 24 |
351 \item measure functions, 47, 104 |
352 \item measure functions, 47, 104 |
352 \item \isa {measure_def} (theorem), \bold{105} |
353 \item \isa {measure_def} (theorem), \bold{105} |
353 \item meta-logic, \bold{70} |
354 \item meta-logic, \bold{70} |
354 \item methods, \bold{15} |
355 \item methods, \bold{16} |
355 \item \isa {min} (constant), 23, 24 |
356 \item \isa {min} (constant), 23, 24 |
356 \item \isa {mod} (symbol), 23 |
357 \item \isa {mod} (symbol), 23 |
357 \item \isa {mod_div_equality} (theorem), \bold{141} |
358 \item \isa {mod_div_equality} (theorem), \bold{141} |
358 \item \isa {mod_mult_distrib} (theorem), \bold{141} |
359 \item \isa {mod_mult_distrib} (theorem), \bold{141} |
359 \item model checking example, 106--116 |
360 \item model checking example, 106--116 |
375 \item natural numbers, 22, 141--143 |
376 \item natural numbers, 22, 141--143 |
376 \item Needham-Schroeder protocol, 183--185 |
377 \item Needham-Schroeder protocol, 183--185 |
377 \item negation, 63--65 |
378 \item negation, 63--65 |
378 \item \isa {Nil} (constant), 9 |
379 \item \isa {Nil} (constant), 9 |
379 \item \isa {no_asm} (modifier), 29 |
380 \item \isa {no_asm} (modifier), 29 |
380 \item \isa {no_asm_simp} (modifier), 29 |
381 \item \isa {no_asm_simp} (modifier), 30 |
381 \item \isa {no_asm_use} (modifier), 29 |
382 \item \isa {no_asm_use} (modifier), 30 |
382 \item non-standard reals, 145 |
383 \item non-standard reals, 145 |
383 \item \isa {None} (constant), \bold{24} |
384 \item \isa {None} (constant), \bold{24} |
384 \item \isa {notE} (theorem), \bold{63} |
385 \item \isa {notE} (theorem), \bold{63} |
385 \item \isa {notI} (theorem), \bold{63} |
386 \item \isa {notI} (theorem), \bold{63} |
386 \item numbers, 139--145 |
387 \item numbers, 139--145 |
424 \item protocols |
425 \item protocols |
425 \subitem security, 183--193 |
426 \subitem security, 183--193 |
426 |
427 |
427 \indexspace |
428 \indexspace |
428 |
429 |
429 \item quantifiers, 5 |
430 \item quantifiers, 6 |
430 \subitem and inductive definitions, 125--127 |
431 \subitem and inductive definitions, 125--127 |
431 \subitem existential, 72 |
432 \subitem existential, 72 |
432 \subitem for sets, 98 |
433 \subitem for sets, 98 |
433 \subitem instantiating, 74 |
434 \subitem instantiating, 74 |
434 \subitem universal, 69--72 |
435 \subitem universal, 69--72 |
481 |
482 |
482 \indexspace |
483 \indexspace |
483 |
484 |
484 \item \isa {safe} (method), 81, 82 |
485 \item \isa {safe} (method), 81, 82 |
485 \item safe rules, \bold{80} |
486 \item safe rules, \bold{80} |
486 \item \isa {set} (type), 4, 95 |
487 \item \isa {set} (type), 5, 95 |
487 \item set comprehensions, 97--98 |
488 \item set comprehensions, 97--98 |
488 \item \isa {set_ext} (theorem), \bold{96} |
489 \item \isa {set_ext} (theorem), \bold{96} |
489 \item sets, 95--99 |
490 \item sets, 95--99 |
490 \subitem finite, 99 |
491 \subitem finite, 99 |
491 \subitem notation for finite, \bold{97} |
492 \subitem notation for finite, \bold{97} |
493 \item \isa {show_brackets} (flag), 6 |
494 \item \isa {show_brackets} (flag), 6 |
494 \item \isa {show_types} (flag), 5, 16 |
495 \item \isa {show_types} (flag), 5, 16 |
495 \item \isa {simp} (attribute), 11, 28 |
496 \item \isa {simp} (attribute), 11, 28 |
496 \item \isa {simp} (method), \bold{28} |
497 \item \isa {simp} (method), \bold{28} |
497 \item \isa {simp} del (attribute), 28 |
498 \item \isa {simp} del (attribute), 28 |
498 \item \isa {simp_all} (method), 28, 37 |
499 \item \isa {simp_all} (method), 29, 37 |
499 \item simplification, 27--33, 163--166 |
500 \item simplification, 27--33, 163--166 |
500 \subitem of \isa{let}-expressions, 31 |
501 \subitem of \isa{let}-expressions, 31 |
501 \subitem with definitions, 30 |
502 \subitem with definitions, 30 |
502 \subitem with/of assumptions, 29 |
503 \subitem with/of assumptions, 29 |
503 \item simplification rule, 165--166 |
504 \item simplification rule, 165--166 |
567 \item tries, 43--46 |
568 \item tries, 43--46 |
568 \item \isa {True} (constant), 5 |
569 \item \isa {True} (constant), 5 |
569 \item tuples, \see{pairs and tuples}{1} |
570 \item tuples, \see{pairs and tuples}{1} |
570 \item \isacommand {typ} (command), 16 |
571 \item \isacommand {typ} (command), 16 |
571 \item type constraints, \bold{6} |
572 \item type constraints, \bold{6} |
572 \item type constructors, 4 |
573 \item type constructors, 5 |
573 \item type inference, \bold{5} |
574 \item type inference, \bold{5} |
574 \item type synonyms, 25 |
575 \item type synonyms, 25 |
575 \item type variables, 5 |
576 \item type variables, 5 |
576 \item \isacommand {typedecl} (command), 107, 158 |
577 \item \isacommand {typedecl} (command), 107, 158 |
577 \item \isacommand {typedef} (command), 159--162 |
578 \item \isacommand {typedef} (command), 159--162 |
595 \item \texttt {Union}, \bold{195} |
596 \item \texttt {Union}, \bold{195} |
596 \item union |
597 \item union |
597 \subitem indexed, 98 |
598 \subitem indexed, 98 |
598 \item \isa {Union_iff} (theorem), \bold{98} |
599 \item \isa {Union_iff} (theorem), \bold{98} |
599 \item \isa {unit} (type), 24 |
600 \item \isa {unit} (type), 24 |
600 \item unknowns, 6, \bold{58} |
601 \item unknowns, 7, \bold{58} |
601 \item unsafe rules, \bold{80} |
602 \item unsafe rules, \bold{80} |
602 \item updating a function, \bold{99} |
603 \item updating a function, \bold{99} |
603 |
604 |
604 \indexspace |
605 \indexspace |
605 |
606 |
606 \item variables, 6--7 |
607 \item variables, 7 |
607 \subitem schematic, 6 |
608 \subitem schematic, 7 |
608 \subitem type, 5 |
609 \subitem type, 5 |
609 \item \isa {vimage_def} (theorem), \bold{101} |
610 \item \isa {vimage_def} (theorem), \bold{101} |
610 |
611 |
611 \indexspace |
612 \indexspace |
612 |
613 |