1 \begin{theindex} |
1 \begin{theindex} |
2 |
2 |
3 \item \ttall, \bold{189} |
3 \item \ttall, \bold{187} |
4 \item \texttt{?}, \bold{189} |
4 \item \texttt{?}, \bold{187} |
5 \item \isasymuniqex, \bold{189} |
5 \item \isasymuniqex, \bold{187} |
6 \item \ttuniquex, \bold{189} |
6 \item \ttuniquex, \bold{187} |
7 \item {\texttt {\&}}, \bold{189} |
7 \item {\texttt {\&}}, \bold{187} |
8 \item \verb$~$, \bold{189} |
8 \item \verb$~$, \bold{187} |
9 \item \verb$~=$, \bold{189} |
9 \item \verb$~=$, \bold{187} |
10 \item \ttor, \bold{189} |
10 \item \ttor, \bold{187} |
11 \item \texttt{[]}, \bold{7} |
11 \item \texttt{[]}, \bold{7} |
12 \item \texttt{\#}, \bold{7} |
12 \item \texttt{\#}, \bold{7} |
13 \item \texttt{\at}, \bold{8}, 189 |
13 \item \texttt{\at}, \bold{8}, 187 |
14 \item \isasymnotin, \bold{189} |
14 \item \isasymnotin, \bold{187} |
15 \item \verb$~:$, \bold{189} |
15 \item \verb$~:$, \bold{187} |
16 \item \isasymInter, \bold{189} |
16 \item \isasymInter, \bold{187} |
17 \item \isasymUnion, \bold{189} |
17 \item \isasymUnion, \bold{187} |
18 \item \isasyminverse, \bold{189} |
18 \item \isasyminverse, \bold{187} |
19 \item \verb$^-1$, \bold{189} |
19 \item \verb$^-1$, \bold{187} |
20 \item \isactrlsup{\isacharasterisk}, \bold{189} |
20 \item \isactrlsup{\isacharasterisk}, \bold{187} |
21 \item \verb$^$\texttt{*}, \bold{189} |
21 \item \verb$^$\texttt{*}, \bold{187} |
22 \item \isasymAnd, \bold{10}, \bold{189} |
22 \item \isasymAnd, \bold{10}, \bold{187} |
23 \item \ttAnd, \bold{189} |
23 \item \ttAnd, \bold{187} |
24 \item \isasymrightleftharpoons, 24 |
24 \item \isasymrightleftharpoons, 24 |
25 \item \isasymrightharpoonup, 24 |
25 \item \isasymrightharpoonup, 24 |
26 \item \isasymleftharpoondown, 24 |
26 \item \isasymleftharpoondown, 24 |
27 \item \emph {$\Rightarrow $}, \bold{3} |
27 \item \emph {$\Rightarrow $}, \bold{3} |
28 \item \ttlbr, \bold{189} |
28 \item \ttlbr, \bold{187} |
29 \item \ttrbr, \bold{189} |
29 \item \ttrbr, \bold{187} |
30 \item \texttt {\%}, \bold{189} |
30 \item \texttt {\%}, \bold{187} |
31 \item \texttt {;}, \bold{5} |
31 \item \texttt {;}, \bold{5} |
32 \item \isa {()} (constant), 22 |
32 \item \isa {()} (constant), 22 |
33 \item \isa {+} (tactical), 83 |
33 \item \isa {+} (tactical), 83 |
34 \item \isa {<*lex*>}, \see{lexicographic product}{1} |
34 \item \isa {<*lex*>}, \see{lexicographic product}{1} |
35 \item \isa {?} (tactical), 83 |
35 \item \isa {?} (tactical), 83 |
44 \indexspace |
44 \indexspace |
45 |
45 |
46 \item abandoning a proof, \bold{11} |
46 \item abandoning a proof, \bold{11} |
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{187} |
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_ac} (theorems), 134 |
53 \item \isa {add_assoc} (theorem), \bold{134} |
53 \item \isa {add_assoc} (theorem), \bold{134} |
54 \item \isa {add_commute} (theorem), \bold{134} |
54 \item \isa {add_commute} (theorem), \bold{134} |
55 \item \isa {add_mult_distrib} (theorem), \bold{133} |
55 \item \isa {add_mult_distrib} (theorem), \bold{133} |
56 \item \texttt {ALL}, \bold{189} |
56 \item \texttt {ALL}, \bold{187} |
57 \item \isa {All} (constant), 93 |
57 \item \isa {All} (constant), 93 |
58 \item \isa {allE} (theorem), \bold{65} |
58 \item \isa {allE} (theorem), \bold{65} |
59 \item \isa {allI} (theorem), \bold{64} |
59 \item \isa {allI} (theorem), \bold{64} |
60 \item append function, 8--12 |
60 \item append function, 8--12 |
61 \item \isacommand {apply} (command), 13 |
61 \item \isacommand {apply} (command), 13 |
62 \item \isa {arg_cong} (theorem), \bold{80} |
62 \item \isa {arg_cong} (theorem), \bold{80} |
63 \item \isa {arith} (method), 21, 131 |
63 \item \isa {arith} (method), 21, 131 |
64 \item arithmetic operations |
64 \item arithmetic operations |
65 \subitem for \protect\isa{nat}, 21 |
65 \subitem for \protect\isa{nat}, 21 |
66 \item \textsc {ascii} symbols, \bold{189} |
66 \item \textsc {ascii} symbols, \bold{187} |
67 \item associative-commutative function, 158 |
67 \item associative-commutative function, 156 |
68 \item \isa {assumption} (method), 53 |
68 \item \isa {assumption} (method), 53 |
69 \item assumptions |
69 \item assumptions |
70 \subitem of subgoal, 10 |
70 \subitem of subgoal, 10 |
71 \subitem renaming, 66--67 |
71 \subitem renaming, 66--67 |
72 \subitem reusing, 67 |
72 \subitem reusing, 67 |
103 \item cardinality, 93 |
103 \item cardinality, 93 |
104 \item \isa {case} (symbol), 30, 31 |
104 \item \isa {case} (symbol), 30, 31 |
105 \item \isa {case} expressions, 3, 4, 16 |
105 \item \isa {case} expressions, 3, 4, 16 |
106 \item case distinctions, 17 |
106 \item case distinctions, 17 |
107 \item case splits, \bold{29} |
107 \item case splits, \bold{29} |
108 \item \isa {case_tac} (method), 17, 85 |
108 \item \isa {case_tac} (method), 17, 85, 139 |
109 \item \isa {clarify} (method), 75, 76 |
109 \item \isa {clarify} (method), 75, 76 |
110 \item \isa {clarsimp} (method), 75, 76 |
110 \item \isa {clarsimp} (method), 75, 76 |
111 \item \isa {classical} (theorem), \bold{57} |
111 \item \isa {classical} (theorem), \bold{57} |
112 \item coinduction, \bold{100} |
112 \item coinduction, \bold{100} |
113 \item \isa {Collect} (constant), 93 |
113 \item \isa {Collect} (constant), 93 |
121 \subitem of relations, \bold{96} |
121 \subitem of relations, \bold{96} |
122 \item conclusion |
122 \item conclusion |
123 \subitem of subgoal, 10 |
123 \subitem of subgoal, 10 |
124 \item conditional expressions, \see{\isa{if} expressions}{1} |
124 \item conditional expressions, \see{\isa{if} expressions}{1} |
125 \item conditional simplification rules, 29 |
125 \item conditional simplification rules, 29 |
126 \item \isa {cong} (attribute), 158 |
126 \item \isa {cong} (attribute), 156 |
127 \item congruence rules, \bold{157} |
127 \item congruence rules, \bold{155} |
128 \item \isa {conjE} (theorem), \bold{55} |
128 \item \isa {conjE} (theorem), \bold{55} |
129 \item \isa {conjI} (theorem), \bold{52} |
129 \item \isa {conjI} (theorem), \bold{52} |
130 \item \isa {Cons} (constant), 7 |
130 \item \isa {Cons} (constant), 7 |
131 \item \isacommand {constdefs} (command), 23 |
131 \item \isacommand {constdefs} (command), 23 |
132 \item \isacommand {consts} (command), 8 |
132 \item \isacommand {consts} (command), 8 |
133 \item contrapositives, 57 |
133 \item contrapositives, 57 |
134 \item converse |
134 \item converse |
135 \subitem of a relation, \bold{96} |
135 \subitem of a relation, \bold{96} |
136 \item \isa {converse_iff} (theorem), \bold{96} |
136 \item \isa {converse_iff} (theorem), \bold{96} |
|
137 \item CTL, 105--110, 171--173 |
137 |
138 |
138 \indexspace |
139 \indexspace |
139 |
140 |
140 \item \isacommand {datatype} (command), 7, 36--41 |
141 \item \isacommand {datatype} (command), 7, 36--41 |
141 \item datatypes, 15--20 |
142 \item datatypes, 15--20 |
142 \subitem and nested recursion, 38, 42 |
143 \subitem and nested recursion, 38, 42 |
143 \subitem mutually recursive, 36 |
144 \subitem mutually recursive, 36 |
|
145 \subitem nested, 160 |
144 \item \isacommand {defer} (command), 14, 84 |
146 \item \isacommand {defer} (command), 14, 84 |
145 \item Definitional Approach, 24 |
147 \item Definitional Approach, 24 |
146 \item definitions, \bold{23} |
148 \item definitions, \bold{23} |
147 \subitem unfolding, \bold{28} |
149 \subitem unfolding, \bold{28} |
148 \item \isacommand {defs} (command), 23 |
150 \item \isacommand {defs} (command), 23 |
188 \item \isa {erule} (method), 54 |
190 \item \isa {erule} (method), 54 |
189 \item \isa {erule_tac} (method), 60 |
191 \item \isa {erule_tac} (method), 60 |
190 \item Euclid's algorithm, 85--88 |
192 \item Euclid's algorithm, 85--88 |
191 \item even numbers |
193 \item even numbers |
192 \subitem defining inductively, 111--115 |
194 \subitem defining inductively, 111--115 |
193 \item \texttt {EX}, \bold{189} |
195 \item \texttt {EX}, \bold{187} |
194 \item \isa {Ex} (constant), 93 |
196 \item \isa {Ex} (constant), 93 |
195 \item \isa {exE} (theorem), \bold{66} |
197 \item \isa {exE} (theorem), \bold{66} |
196 \item \isa {exI} (theorem), \bold{66} |
198 \item \isa {exI} (theorem), \bold{66} |
197 \item \isa {ext} (theorem), \bold{93} |
199 \item \isa {ext} (theorem), \bold{93} |
198 \item extensionality |
200 \item extensionality |
199 \subitem for functions, \bold{93, 94} |
201 \subitem for functions, \bold{93, 94} |
200 \subitem for records, 143 |
202 \subitem for records, 143 |
201 \subitem for sets, \bold{90} |
203 \subitem for sets, \bold{90} |
202 \item \ttEXU, \bold{189} |
204 \item \ttEXU, \bold{187} |
203 |
205 |
204 \indexspace |
206 \indexspace |
205 |
207 |
206 \item \isa {False} (constant), 3 |
208 \item \isa {False} (constant), 3 |
207 \item \isa {fast} (method), 76, 108 |
209 \item \isa {fast} (method), 76, 108 |
217 \item \isa {frule} (method), 67 |
219 \item \isa {frule} (method), 67 |
218 \item \isa {frule_tac} (method), 60 |
220 \item \isa {frule_tac} (method), 60 |
219 \item \isa {fst} (constant), 22 |
221 \item \isa {fst} (constant), 22 |
220 \item function types, 3 |
222 \item function types, 3 |
221 \item functions, 93--95 |
223 \item functions, 93--95 |
|
224 \subitem partial, 162 |
222 \subitem total, 9, 44--50 |
225 \subitem total, 9, 44--50 |
223 \subitem underdefined, 165 |
226 \subitem underdefined, 163 |
224 |
227 |
225 \indexspace |
228 \indexspace |
226 |
229 |
227 \item \isa {gcd} (constant), 77--78, 85--88 |
230 \item \isa {gcd} (constant), 77--78, 85--88 |
228 \item generalizing for induction, 113 |
231 \item generalizing for induction, 113 |
263 \item \isa {image_def} (theorem), \bold{95} |
265 \item \isa {image_def} (theorem), \bold{95} |
264 \item \isa {Image_iff} (theorem), \bold{96} |
266 \item \isa {Image_iff} (theorem), \bold{96} |
265 \item \isa {impI} (theorem), \bold{56} |
267 \item \isa {impI} (theorem), \bold{56} |
266 \item implication, 56--57 |
268 \item implication, 56--57 |
267 \item \isa {ind_cases} (method), 115 |
269 \item \isa {ind_cases} (method), 115 |
268 \item \isa {induct_tac} (method), 10, 17, 50, 172 |
270 \item \isa {induct_tac} (method), 10, 17, 50, 170 |
269 \item induction, 168--175 |
271 \item induction, 166--173 |
|
272 \subitem complete, 168 |
|
273 \subitem deriving new schemas, 170 |
|
274 \subitem on a term, 167 |
270 \subitem recursion, 49--50 |
275 \subitem recursion, 49--50 |
271 \subitem structural, 17 |
276 \subitem structural, 17 |
272 \subitem well-founded, 99 |
277 \subitem well-founded, 99 |
273 \item induction heuristics, 31--33 |
278 \item induction heuristics, 31--33 |
274 \item \isacommand {inductive} (command), 111 |
279 \item \isacommand {inductive} (command), 111 |
281 \item \isa {inj_on_def} (theorem), \bold{94} |
286 \item \isa {inj_on_def} (theorem), \bold{94} |
282 \item injections, 94 |
287 \item injections, 94 |
283 \item \isa {insert} (constant), 91 |
288 \item \isa {insert} (constant), 91 |
284 \item \isa {insert} (method), 81--82 |
289 \item \isa {insert} (method), 81--82 |
285 \item instance, \bold{145} |
290 \item instance, \bold{145} |
286 \item \texttt {INT}, \bold{189} |
291 \item \texttt {INT}, \bold{187} |
287 \item \texttt {Int}, \bold{189} |
292 \item \texttt {Int}, \bold{187} |
288 \item \isa {int} (type), 135 |
293 \item \isa {int} (type), 135 |
289 \item \isa {INT_iff} (theorem), \bold{92} |
294 \item \isa {INT_iff} (theorem), \bold{92} |
290 \item \isa {IntD1} (theorem), \bold{89} |
295 \item \isa {IntD1} (theorem), \bold{89} |
291 \item \isa {IntD2} (theorem), \bold{89} |
296 \item \isa {IntD2} (theorem), \bold{89} |
292 \item integers, 135 |
297 \item integers, 135 |
293 \item \isa {INTER} (constant), 93 |
298 \item \isa {INTER} (constant), 93 |
294 \item \texttt {Inter}, \bold{189} |
299 \item \texttt {Inter}, \bold{187} |
295 \item \isa {Inter_iff} (theorem), \bold{92} |
300 \item \isa {Inter_iff} (theorem), \bold{92} |
296 \item intersection, 89 |
301 \item intersection, 89 |
297 \subitem indexed, 92 |
302 \subitem indexed, 92 |
298 \item \isa {IntI} (theorem), \bold{89} |
303 \item \isa {IntI} (theorem), \bold{89} |
299 \item \isa {intro} (method), 58 |
304 \item \isa {intro} (method), 58 |
300 \item \isa {intro!} (attribute), 112 |
305 \item \isa {intro!} (attribute), 112 |
|
306 \item \isa {intro_classes} (method), 145 |
301 \item introduction rules, 52--53 |
307 \item introduction rules, 52--53 |
302 \item \isa {inv} (constant), 70 |
308 \item \isa {inv} (constant), 70 |
303 \item \isa {inv_image_def} (theorem), \bold{99} |
309 \item \isa {inv_image_def} (theorem), \bold{99} |
304 \item inverse |
310 \item inverse |
305 \subitem of a function, \bold{94} |
311 \subitem of a function, \bold{94} |
320 \item \isa {LEAST} (symbol), 21, 69 |
326 \item \isa {LEAST} (symbol), 21, 69 |
321 \item least number operator, \see{\protect\isa{LEAST}}{69} |
327 \item least number operator, \see{\protect\isa{LEAST}}{69} |
322 \item \isacommand {lemma} (command), 11 |
328 \item \isacommand {lemma} (command), 11 |
323 \item \isacommand {lemmas} (command), 77, 86 |
329 \item \isacommand {lemmas} (command), 77, 86 |
324 \item \isa {length} (symbol), 16 |
330 \item \isa {length} (symbol), 16 |
325 \item \isa {length_induct}, \bold{172} |
331 \item \isa {length_induct}, \bold{170} |
326 \item \isa {less_than} (constant), 98 |
332 \item \isa {less_than} (constant), 98 |
327 \item \isa {less_than_iff} (theorem), \bold{98} |
333 \item \isa {less_than_iff} (theorem), \bold{98} |
328 \item \isa {let} expressions, 3, 4, 29 |
334 \item \isa {let} expressions, 3, 4, 29 |
329 \item \isa {Let_def} (theorem), 29 |
335 \item \isa {Let_def} (theorem), 29 |
330 \item \isa {lex_prod_def} (theorem), \bold{99} |
336 \item \isa {lex_prod_def} (theorem), \bold{99} |
331 \item lexicographic product, \bold{99}, 160 |
337 \item lexicographic product, \bold{99}, 158 |
332 \item {\texttt{lfp}} |
338 \item {\texttt{lfp}} |
333 \subitem applications of, \see{CTL}{100} |
339 \subitem applications of, \see{CTL}{100} |
334 \item linear arithmetic, 20--22, 131 |
340 \item linear arithmetic, 20--22, 131 |
335 \item \isa {List} (theory), 15 |
341 \item \isa {List} (theory), 15 |
336 \item \isa {list} (type), 2, 7, 15 |
342 \item \isa {list} (type), 2, 7, 15 |
337 \item \isa {list.split} (theorem), 30 |
343 \item \isa {list.split} (theorem), 30 |
338 \item \isa {lists_mono} (theorem), \bold{121} |
344 \item \isa {lists_mono} (theorem), \bold{121} |
339 \item Lowe, Gavin, 178--179 |
345 \item Lowe, Gavin, 176--177 |
340 |
346 |
341 \indexspace |
347 \indexspace |
342 |
348 |
343 \item \isa {Main} (theory), 2 |
349 \item \isa {Main} (theory), 2 |
344 \item major premise, \bold{59} |
350 \item major premise, \bold{59} |
354 \item model checking example, 100--110 |
360 \item model checking example, 100--110 |
355 \item \emph{modus ponens}, 51, 56 |
361 \item \emph{modus ponens}, 51, 56 |
356 \item \isa {mono_def} (theorem), \bold{100} |
362 \item \isa {mono_def} (theorem), \bold{100} |
357 \item monotone functions, \bold{100}, 123 |
363 \item monotone functions, \bold{100}, 123 |
358 \subitem and inductive definitions, 121--122 |
364 \subitem and inductive definitions, 121--122 |
359 \item \isa {more} (constant), 140--142 |
365 \item \isa {more} (constant), 140, 141 |
360 \item \isa {mp} (theorem), \bold{56} |
366 \item \isa {mp} (theorem), \bold{56} |
361 \item \isa {mult_ac} (theorems), 134 |
367 \item \isa {mult_ac} (theorems), 134 |
|
368 \item multiple inheritance, \bold{149} |
362 \item multiset ordering, \bold{99} |
369 \item multiset ordering, \bold{99} |
363 |
370 |
364 \indexspace |
371 \indexspace |
365 |
372 |
366 \item \isa {nat} (type), 2, 20, 133--134 |
373 \item \isa {nat} (type), 2, 20, 133--134 |
|
374 \item \isa {nat_less_induct} (theorem), 168 |
367 \item natural deduction, 51--52 |
375 \item natural deduction, 51--52 |
368 \item natural numbers, 20, 133--134 |
376 \item natural numbers, 20, 133--134 |
369 \item Needham-Schroeder protocol, 177--179 |
377 \item Needham-Schroeder protocol, 175--177 |
370 \item negation, 57--59 |
378 \item negation, 57--59 |
371 \item \isa {Nil} (constant), 7 |
379 \item \isa {Nil} (constant), 7 |
372 \item \isa {no_asm} (modifier), 27 |
380 \item \isa {no_asm} (modifier), 27 |
373 \item \isa {no_asm_simp} (modifier), 27 |
381 \item \isa {no_asm_simp} (modifier), 27 |
374 \item \isa {no_asm_use} (modifier), 27 |
382 \item \isa {no_asm_use} (modifier), 27 |
382 \subitem for type \protect\isa{real}, 136 |
390 \subitem for type \protect\isa{real}, 136 |
383 |
391 |
384 \indexspace |
392 \indexspace |
385 |
393 |
386 \item \isa {O} (symbol), 96 |
394 \item \isa {O} (symbol), 96 |
387 \item \texttt {o}, \bold{189} |
395 \item \texttt {o}, \bold{187} |
388 \item \isa {o_def} (theorem), \bold{94} |
396 \item \isa {o_def} (theorem), \bold{94} |
389 \item \isa {OF} (attribute), 79--80 |
397 \item \isa {OF} (attribute), 79--80 |
390 \item \isa {of} (attribute), 77, 80 |
398 \item \isa {of} (attribute), 77, 80 |
391 \item \isa {only} (modifier), 27 |
399 \item \isa {only} (modifier), 27 |
392 \item \isacommand {oops} (command), 11 |
400 \item \isacommand {oops} (command), 11 |
393 \item \isa {option} (type), \bold{22} |
401 \item \isa {option} (type), \bold{22} |
394 \item ordered rewriting, \bold{158} |
402 \item ordered rewriting, \bold{156} |
395 \item overloading, 21, 144--146 |
403 \item overloading, 21, 144--146 |
396 \subitem and arithmetic, 132 |
404 \subitem and arithmetic, 132 |
397 |
405 |
398 \indexspace |
406 \indexspace |
399 |
407 |
400 \item pairs and tuples, 22, 137--140 |
408 \item pairs and tuples, 22, 137--140 |
401 \item parent theories, \bold{2} |
409 \item parent theories, \bold{2} |
402 \item partial function, 164 |
|
403 \item pattern matching |
410 \item pattern matching |
404 \subitem and \isacommand{recdef}, 45 |
411 \subitem and \isacommand{recdef}, 45 |
405 \item pattern, higher-order, \bold{159} |
412 \item patterns |
|
413 \subitem higher-order, \bold{157} |
406 \item PDL, 102--104 |
414 \item PDL, 102--104 |
407 \item permutative rewrite rule, \bold{158} |
|
408 \item \isacommand {pr} (command), 14, 84 |
415 \item \isacommand {pr} (command), 14, 84 |
409 \item \isacommand {prefer} (command), 14, 84 |
416 \item \isacommand {prefer} (command), 14, 84 |
410 \item primitive recursion, \see{recursion, primitive}{1} |
417 \item primitive recursion, \see{recursion, primitive}{1} |
411 \item \isacommand {primrec} (command), 8, 16, 36--41 |
418 \item \isacommand {primrec} (command), 8, 16, 36--41 |
412 \item product type, \see{pairs and tuples}{1} |
419 \item product type, \see{pairs and tuples}{1} |
437 \item \isa {range} (symbol), 95 |
444 \item \isa {range} (symbol), 95 |
438 \item \isa {Range_iff} (theorem), \bold{96} |
445 \item \isa {Range_iff} (theorem), \bold{96} |
439 \item \isa {Real} (theory), 137 |
446 \item \isa {Real} (theory), 137 |
440 \item \isa {real} (type), 136--137 |
447 \item \isa {real} (type), 136--137 |
441 \item real numbers, 136--137 |
448 \item real numbers, 136--137 |
442 \item \isacommand {recdef} (command), 44--50, 98, 160--168 |
449 \item \isacommand {recdef} (command), 44--50, 98, 158--166 |
443 \subitem and numeric literals, 132 |
450 \subitem and numeric literals, 132 |
444 \item \isa {recdef_cong} (attribute), 164 |
451 \item \isa {recdef_cong} (attribute), 162 |
445 \item \isa {recdef_simp} (attribute), 46 |
452 \item \isa {recdef_simp} (attribute), 46 |
446 \item \isa {recdef_wf} (attribute), 162 |
453 \item \isa {recdef_wf} (attribute), 160 |
447 \item \isacommand {record} (command), 140 |
454 \item \isacommand {record} (command), 140 |
448 \item \isa {record_split} (method), 143 |
455 \item \isa {record_split} (method), 143 |
449 \item records, 140--144 |
456 \item records, 140--144 |
450 \subitem extensible, 141--142 |
457 \subitem extensible, 141--142 |
451 \item recursion |
458 \item recursion |
|
459 \subitem guarded, 163 |
452 \subitem primitive, 16 |
460 \subitem primitive, 16 |
453 \subitem well-founded, \bold{161} |
461 \subitem well-founded, \bold{159} |
454 \item recursion induction, 49--50 |
462 \item recursion induction, 49--50 |
455 \item \isacommand {redo} (command), 14 |
463 \item \isacommand {redo} (command), 14 |
456 \item reflexive and transitive closure, 96--98 |
464 \item reflexive and transitive closure, 96--98 |
457 \item reflexive transitive closure |
465 \item reflexive transitive closure |
458 \subitem defining inductively, 116--119 |
466 \subitem defining inductively, 116--119 |
459 \item relations, 95--98 |
467 \item relations, 95--98 |
460 \subitem well-founded, 98--99 |
468 \subitem well-founded, 98--99 |
461 \item \isa {rename_tac} (method), 66--67 |
469 \item \isa {rename_tac} (method), 66--67 |
462 \item \isa {rev} (constant), 8--12, 32 |
470 \item \isa {rev} (constant), 8--12, 32 |
463 \item rewrite rule |
|
464 \subitem permutative, \bold{158} |
|
465 \item rewrite rules, \bold{25} |
471 \item rewrite rules, \bold{25} |
|
472 \subitem permutative, \bold{156} |
466 \item rewriting, \bold{25} |
473 \item rewriting, \bold{25} |
467 \subitem ordered, \bold{158} |
|
468 \item \isa {rotate_tac} (method), 28 |
474 \item \isa {rotate_tac} (method), 28 |
469 \item \isa {rtrancl_refl} (theorem), \bold{96} |
475 \item \isa {rtrancl_refl} (theorem), \bold{96} |
470 \item \isa {rtrancl_trans} (theorem), \bold{96} |
476 \item \isa {rtrancl_trans} (theorem), \bold{96} |
471 \item rule induction, 112--114 |
477 \item rule induction, 112--114 |
472 \item rule inversion, 114--115, 123--124 |
478 \item rule inversion, 114--115, 123--124 |
|
479 \item \isa {rule_format} (attribute), 167 |
473 \item \isa {rule_tac} (method), 60 |
480 \item \isa {rule_tac} (method), 60 |
474 \subitem and renaming, 67 |
481 \subitem and renaming, 67 |
475 |
482 |
476 \indexspace |
483 \indexspace |
477 |
484 |
488 \item \isa {show_types} (flag), 3, 14 |
495 \item \isa {show_types} (flag), 3, 14 |
489 \item \isa {simp} (attribute), 9, 26 |
496 \item \isa {simp} (attribute), 9, 26 |
490 \item \isa {simp} (method), \bold{26} |
497 \item \isa {simp} (method), \bold{26} |
491 \item \isa {simp} del (attribute), 26 |
498 \item \isa {simp} del (attribute), 26 |
492 \item \isa {simp_all} (method), 26, 35 |
499 \item \isa {simp_all} (method), 26, 35 |
493 \item simplification, 25--31, 157--160 |
500 \item simplification, 25--31, 155--158 |
494 \subitem of \isa{let}-expressions, 29 |
501 \subitem of \isa{let}-expressions, 29 |
495 \subitem ordered, \bold{158} |
|
496 \subitem with definitions, 28 |
502 \subitem with definitions, 28 |
497 \subitem with/of assumptions, 27 |
503 \subitem with/of assumptions, 27 |
498 \item simplification rule, 159--160 |
504 \item simplification rule, 157--158 |
499 \item simplification rules, 26 |
505 \item simplification rules, 26 |
500 \subitem adding and deleting, 27 |
506 \subitem adding and deleting, 27 |
501 \item \isa {simplified} (attribute), 77, 80 |
507 \item \isa {simplified} (attribute), 77, 80 |
502 \item \isa {size} (constant), 15 |
508 \item \isa {size} (constant), 15 |
503 \item \isa {snd} (constant), 22 |
509 \item \isa {snd} (constant), 22 |
504 \item \isa {SOME} (symbol), 70 |
510 \item \isa {SOME} (symbol), 70 |
505 \item \texttt {SOME}, \bold{189} |
511 \item \texttt {SOME}, \bold{187} |
506 \item \isa {Some} (constant), \bold{22} |
512 \item \isa {Some} (constant), \bold{22} |
507 \item \isa {some_equality} (theorem), \bold{70} |
513 \item \isa {some_equality} (theorem), \bold{70} |
508 \item \isa {someI} (theorem), \bold{70} |
514 \item \isa {someI} (theorem), \bold{70} |
509 \item \isa {someI2} (theorem), \bold{70} |
515 \item \isa {someI2} (theorem), \bold{70} |
510 \item \isa {someI_ex} (theorem), \bold{71} |
516 \item \isa {someI_ex} (theorem), \bold{71} |
517 \item split rule, \bold{30} |
523 \item split rule, \bold{30} |
518 \item \isa {split_if} (theorem), 30 |
524 \item \isa {split_if} (theorem), 30 |
519 \item \isa {split_if_asm} (theorem), 30 |
525 \item \isa {split_if_asm} (theorem), 30 |
520 \item \isa {ssubst} (theorem), \bold{61} |
526 \item \isa {ssubst} (theorem), \bold{61} |
521 \item structural induction, \see{induction, structural}{1} |
527 \item structural induction, \see{induction, structural}{1} |
|
528 \item subclasses, 144, 148 |
522 \item subgoal numbering, 44 |
529 \item subgoal numbering, 44 |
523 \item \isa {subgoal_tac} (method), 82 |
530 \item \isa {subgoal_tac} (method), 82 |
524 \item subgoals, 10 |
531 \item subgoals, 10 |
525 \item subset relation, \bold{90} |
532 \item subset relation, \bold{90} |
526 \item \isa {subsetD} (theorem), \bold{90} |
533 \item \isa {subsetD} (theorem), \bold{90} |
566 \item type constructors, 2 |
573 \item type constructors, 2 |
567 \item type inference, \bold{3} |
574 \item type inference, \bold{3} |
568 \item type synonyms, 23 |
575 \item type synonyms, 23 |
569 \item type variables, 3 |
576 \item type variables, 3 |
570 \item \isacommand {typedecl} (command), 101, 150 |
577 \item \isacommand {typedecl} (command), 101, 150 |
571 \item \isacommand {typedef} (command), 151--155 |
578 \item \isacommand {typedef} (command), 151--154 |
572 \item types, 2--3 |
579 \item types, 2--3 |
573 \subitem declaring, 150--151 |
580 \subitem declaring, 150--151 |
574 \subitem defining, 151--155 |
581 \subitem defining, 151--154 |
575 \item \isacommand {types} (command), 23 |
582 \item \isacommand {types} (command), 23 |
576 |
583 |
577 \indexspace |
584 \indexspace |
578 |
585 |
579 \item Ullman, J. D., 129 |
586 \item Ullman, J. D., 129 |
580 \item \texttt {UN}, \bold{189} |
587 \item \texttt {UN}, \bold{187} |
581 \item \texttt {Un}, \bold{189} |
588 \item \texttt {Un}, \bold{187} |
582 \item \isa {UN_E} (theorem), \bold{92} |
589 \item \isa {UN_E} (theorem), \bold{92} |
583 \item \isa {UN_I} (theorem), \bold{92} |
590 \item \isa {UN_I} (theorem), \bold{92} |
584 \item \isa {UN_iff} (theorem), \bold{92} |
591 \item \isa {UN_iff} (theorem), \bold{92} |
585 \item \isa {Un_subset_iff} (theorem), \bold{90} |
592 \item \isa {Un_subset_iff} (theorem), \bold{90} |
586 \item \isacommand {undo} (command), 14 |
593 \item \isacommand {undo} (command), 14 |
587 \item unification, 60--63 |
594 \item unification, 60--63 |
588 \item \isa {UNION} (constant), 93 |
595 \item \isa {UNION} (constant), 93 |
589 \item \texttt {Union}, \bold{189} |
596 \item \texttt {Union}, \bold{187} |
590 \item union |
597 \item union |
591 \subitem indexed, 92 |
598 \subitem indexed, 92 |
592 \item \isa {Union_iff} (theorem), \bold{92} |
599 \item \isa {Union_iff} (theorem), \bold{92} |
593 \item \isa {unit} (type), 22 |
600 \item \isa {unit} (type), 22 |
594 \item unknowns, 4, \bold{52} |
601 \item unknowns, 4, \bold{52} |
602 \subitem type, 3 |
609 \subitem type, 3 |
603 \item \isa {vimage_def} (theorem), \bold{95} |
610 \item \isa {vimage_def} (theorem), \bold{95} |
604 |
611 |
605 \indexspace |
612 \indexspace |
606 |
613 |
607 \item Wenzel, Markus, v |
614 \item Wenzel, Markus, vii |
608 \item \isa {wf_induct} (theorem), \bold{99} |
615 \item \isa {wf_induct} (theorem), \bold{99} |
609 \item \isa {wf_inv_image} (theorem), \bold{99} |
616 \item \isa {wf_inv_image} (theorem), \bold{99} |
610 \item \isa {wf_less_than} (theorem), \bold{98} |
617 \item \isa {wf_less_than} (theorem), \bold{98} |
611 \item \isa {wf_lex_prod} (theorem), \bold{99} |
618 \item \isa {wf_lex_prod} (theorem), \bold{99} |
612 \item \isa {wf_measure} (theorem), \bold{99} |
619 \item \isa {wf_measure} (theorem), \bold{99} |
613 \item \isa {while} (constant), 167 |
620 \item \isa {wf_subset} (theorem), 160 |
614 \item \isa {While_Combinator} (theory), 167 |
621 \item \isa {while} (constant), 165 |
|
622 \item \isa {While_Combinator} (theory), 165 |
|
623 \item \isa {while_rule} (theorem), 165 |
615 |
624 |
616 \indexspace |
625 \indexspace |
617 |
626 |
618 \item \isa {zadd_ac} (theorems), 135 |
627 \item \isa {zadd_ac} (theorems), 135 |
619 \item \isa {zmult_ac} (theorems), 135 |
628 \item \isa {zmult_ac} (theorems), 135 |