2665
|
1 |
\begin{theindex}
|
|
2 |
|
6141
|
3 |
\item {\tt !} symbol, 6, 8, 15, 16, 28
|
|
4 |
\item {\tt[]} symbol, 28
|
|
5 |
\item {\tt\#} symbol, 28
|
|
6 |
\item {\tt\#*} symbol, 83
|
|
7 |
\item {\tt\#+} symbol, 83
|
|
8 |
\item {\tt\&} symbol, 6, 59
|
|
9 |
\item {\tt *} symbol, 7, 25, 74
|
|
10 |
\item {\tt *} type, 23
|
|
11 |
\item {\tt +} symbol, 7, 25, 74
|
|
12 |
\item {\tt +} type, 23
|
|
13 |
\item {\tt -} symbol, 7, 25, 83
|
|
14 |
\item {\tt -->} symbol, 6, 59, 74
|
|
15 |
\item {\tt :} symbol, 14
|
|
16 |
\item {\tt <} constant, 26
|
|
17 |
\item {\tt <} symbol, 25
|
|
18 |
\item {\tt <->} symbol, 59
|
|
19 |
\item {\tt <=} constant, 26
|
|
20 |
\item {\tt <=} symbol, 14
|
|
21 |
\item {\tt =} symbol, 6, 59, 74
|
|
22 |
\item {\tt ?} symbol, 6, 8, 15, 16
|
|
23 |
\item {\tt ?!} symbol, 6
|
|
24 |
\item {\tt\at} symbol, 6, 28
|
|
25 |
\item {\tt `} symbol, 74
|
|
26 |
\item {\tt ``} symbol, 14
|
|
27 |
\item \verb'{}' symbol, 14
|
|
28 |
\item {\tt |} symbol, 6, 59
|
|
29 |
\item {\tt |-|} symbol, 83
|
2665
|
30 |
|
|
31 |
\indexspace
|
|
32 |
|
6141
|
33 |
\item {\tt 0} constant, 25, 72
|
2665
|
34 |
|
|
35 |
\indexspace
|
|
36 |
|
6141
|
37 |
\item {\tt absdiff_def} theorem, 83
|
|
38 |
\item {\tt add_assoc} theorem, 83
|
|
39 |
\item {\tt add_commute} theorem, 83
|
|
40 |
\item {\tt add_def} theorem, 83
|
|
41 |
\item {\tt add_inverse_diff} theorem, 83
|
|
42 |
\item {\tt add_mp_tac}, \bold{81}
|
|
43 |
\item {\tt add_mult_dist} theorem, 83
|
|
44 |
\item {\tt add_safes}, \bold{65}
|
|
45 |
\item {\tt add_typing} theorem, 83
|
|
46 |
\item {\tt add_unsafes}, \bold{65}
|
|
47 |
\item {\tt addC0} theorem, 83
|
|
48 |
\item {\tt addC_succ} theorem, 83
|
|
49 |
\item {\tt Addsplits}, \bold{22}
|
|
50 |
\item {\tt addsplits}, \bold{22}, 27, 39
|
|
51 |
\item {\tt ALL} symbol, 6, 8, 15, 16, 59
|
|
52 |
\item {\tt All} constant, 6, 59
|
|
53 |
\item {\tt All_def} theorem, 10
|
|
54 |
\item {\tt all_dupE} theorem, 12
|
|
55 |
\item {\tt allE} theorem, 12
|
|
56 |
\item {\tt allI} theorem, 12
|
|
57 |
\item {\tt allL} theorem, 61, 65
|
|
58 |
\item {\tt allL_thin} theorem, 62
|
|
59 |
\item {\tt allR} theorem, 61
|
|
60 |
\item {\tt and_def} theorem, 10
|
|
61 |
\item {\tt arg_cong} theorem, 11
|
|
62 |
\item {\tt Arith} theory, 26, 82
|
6072
|
63 |
\item assumptions
|
6141
|
64 |
\subitem in {\CTT}, 71, 81
|
2665
|
65 |
|
|
66 |
\indexspace
|
|
67 |
|
6141
|
68 |
\item {\tt Ball} constant, 14, 16
|
|
69 |
\item {\tt Ball_def} theorem, 17
|
|
70 |
\item {\tt ballE} theorem, 18
|
|
71 |
\item {\tt ballI} theorem, 18
|
|
72 |
\item {\tt basic} theorem, 61
|
|
73 |
\item {\tt basic_defs}, \bold{79}
|
|
74 |
\item {\tt best_tac}, \bold{66}
|
|
75 |
\item {\tt Bex} constant, 14, 16
|
|
76 |
\item {\tt Bex_def} theorem, 17
|
|
77 |
\item {\tt bexCI} theorem, 16, 18
|
|
78 |
\item {\tt bexE} theorem, 18
|
|
79 |
\item {\tt bexI} theorem, 16, 18
|
|
80 |
\item {\textit {bool}} type, 7
|
|
81 |
\item {\tt box_equals} theorem, 11, 13
|
|
82 |
\item {\tt bspec} theorem, 18
|
|
83 |
\item {\tt butlast} constant, 28
|
2665
|
84 |
|
|
85 |
\indexspace
|
|
86 |
|
6141
|
87 |
\item {\tt case} symbol, 9, 26, 27, 39
|
|
88 |
\item {\tt case_tac}, \bold{13}
|
|
89 |
\item {\tt CCL} theory, 1
|
|
90 |
\item {\tt ccontr} theorem, 12
|
|
91 |
\item {\tt classical} theorem, 12
|
|
92 |
\item {\tt coinductive}, 51--53
|
|
93 |
\item {\tt Collect} constant, 14, 16
|
|
94 |
\item {\tt Collect_mem_eq} theorem, 16, 17
|
|
95 |
\item {\tt CollectD} theorem, 18, 56
|
|
96 |
\item {\tt CollectE} theorem, 18
|
|
97 |
\item {\tt CollectI} theorem, 18, 57
|
|
98 |
\item {\tt comp_rls}, \bold{79}
|
|
99 |
\item {\tt Compl} constant, 14
|
|
100 |
\item {\tt Compl_def} theorem, 17
|
|
101 |
\item {\tt Compl_disjoint} theorem, 20
|
|
102 |
\item {\tt Compl_Int} theorem, 20
|
|
103 |
\item {\tt Compl_partition} theorem, 20
|
|
104 |
\item {\tt Compl_Un} theorem, 20
|
|
105 |
\item {\tt ComplD} theorem, 19
|
|
106 |
\item {\tt ComplI} theorem, 19
|
|
107 |
\item {\tt concat} constant, 28
|
|
108 |
\item {\tt cong} theorem, 11
|
|
109 |
\item {\tt conj_cong}, 21
|
|
110 |
\item {\tt conjE} theorem, 11
|
|
111 |
\item {\tt conjI} theorem, 11
|
|
112 |
\item {\tt conjL} theorem, 61
|
|
113 |
\item {\tt conjR} theorem, 61
|
|
114 |
\item {\tt conjunct1} theorem, 11
|
|
115 |
\item {\tt conjunct2} theorem, 11
|
|
116 |
\item {\tt conL} theorem, 62
|
|
117 |
\item {\tt conR} theorem, 62
|
|
118 |
\item Constructive Type Theory, 71--93
|
|
119 |
\item {\tt contr} constant, 72
|
|
120 |
\item {\tt could_res}, \bold{64}
|
|
121 |
\item {\tt could_resolve_seq}, \bold{64}
|
|
122 |
\item {\tt CTT} theory, 1, 71
|
|
123 |
\item {\tt Cube} theory, 1
|
|
124 |
\item {\tt cut} theorem, 61
|
|
125 |
\item {\tt cutL_tac}, \bold{63}
|
|
126 |
\item {\tt cutR_tac}, \bold{63}
|
6072
|
127 |
|
|
128 |
\indexspace
|
|
129 |
|
6141
|
130 |
\item {\tt datatype}, 36--44
|
|
131 |
\item {\tt Delsplits}, \bold{22}
|
|
132 |
\item {\tt delsplits}, \bold{22}
|
|
133 |
\item {\tt diff_0_eq_0} theorem, 83
|
|
134 |
\item {\tt diff_def} theorem, 83
|
|
135 |
\item {\tt diff_self_eq_0} theorem, 83
|
|
136 |
\item {\tt diff_succ_succ} theorem, 83
|
|
137 |
\item {\tt diff_typing} theorem, 83
|
|
138 |
\item {\tt diffC0} theorem, 83
|
|
139 |
\item {\tt disjCI} theorem, 12
|
|
140 |
\item {\tt disjE} theorem, 11
|
|
141 |
\item {\tt disjI1} theorem, 11
|
|
142 |
\item {\tt disjI2} theorem, 11
|
|
143 |
\item {\tt disjL} theorem, 61
|
|
144 |
\item {\tt disjR} theorem, 61
|
|
145 |
\item {\tt div} symbol, 25, 83
|
|
146 |
\item {\tt div_def} theorem, 83
|
|
147 |
\item {\tt div_geq} theorem, 26
|
|
148 |
\item {\tt div_less} theorem, 26
|
|
149 |
\item {\tt Divides} theory, 26
|
|
150 |
\item {\tt double_complement} theorem, 20
|
|
151 |
\item {\tt drop} constant, 28
|
|
152 |
\item {\tt dropWhile} constant, 28
|
2665
|
153 |
|
|
154 |
\indexspace
|
|
155 |
|
6141
|
156 |
\item {\tt Elem} constant, 72
|
|
157 |
\item {\tt elim_rls}, \bold{79}
|
|
158 |
\item {\tt elimL_rls}, \bold{79}
|
|
159 |
\item {\tt empty_def} theorem, 17
|
|
160 |
\item {\tt empty_pack}, \bold{65}
|
|
161 |
\item {\tt emptyE} theorem, 19
|
|
162 |
\item {\tt Eps} constant, 6, 8
|
|
163 |
\item {\tt Eq} constant, 72
|
|
164 |
\item {\tt eq} constant, 72, 77
|
|
165 |
\item {\tt EqC} theorem, 78
|
|
166 |
\item {\tt EqE} theorem, 78
|
|
167 |
\item {\tt Eqelem} constant, 72
|
|
168 |
\item {\tt EqF} theorem, 78
|
|
169 |
\item {\tt EqFL} theorem, 78
|
|
170 |
\item {\tt EqI} theorem, 78
|
|
171 |
\item {\tt Eqtype} constant, 72
|
|
172 |
\item {\tt equal_tac}, \bold{80}
|
|
173 |
\item {\tt equal_types} theorem, 75
|
|
174 |
\item {\tt equal_typesL} theorem, 75
|
|
175 |
\item {\tt equalityCE} theorem, 16, 18, 56, 57
|
|
176 |
\item {\tt equalityD1} theorem, 18
|
|
177 |
\item {\tt equalityD2} theorem, 18
|
|
178 |
\item {\tt equalityE} theorem, 18
|
|
179 |
\item {\tt equalityI} theorem, 18
|
|
180 |
\item {\tt EX} symbol, 6, 8, 15, 16, 59
|
|
181 |
\item {\tt Ex} constant, 6, 59
|
|
182 |
\item {\tt EX!} symbol, 6
|
|
183 |
\item {\tt Ex1} constant, 6
|
|
184 |
\item {\tt Ex1_def} theorem, 10
|
|
185 |
\item {\tt ex1E} theorem, 12
|
|
186 |
\item {\tt ex1I} theorem, 12
|
|
187 |
\item {\tt Ex_def} theorem, 10
|
|
188 |
\item {\tt exCI} theorem, 12
|
|
189 |
\item {\tt excluded_middle} theorem, 12
|
|
190 |
\item {\tt exE} theorem, 12
|
|
191 |
\item {\tt exhaust_tac}, \bold{40}
|
|
192 |
\item {\tt exI} theorem, 12
|
|
193 |
\item {\tt exL} theorem, 61
|
|
194 |
\item {\tt Exp} theory, 55
|
|
195 |
\item {\tt exR} theorem, 61, 65, 67
|
|
196 |
\item {\tt exR_thin} theorem, 62, 67, 68
|
|
197 |
\item {\tt ext} theorem, 9, 10
|
2665
|
198 |
|
|
199 |
\indexspace
|
|
200 |
|
6141
|
201 |
\item {\tt F} constant, 72
|
|
202 |
\item {\tt False} constant, 6, 59
|
|
203 |
\item {\tt False_def} theorem, 10
|
|
204 |
\item {\tt FalseE} theorem, 11
|
|
205 |
\item {\tt FalseL} theorem, 61
|
|
206 |
\item {\tt fast_tac}, \bold{66}
|
|
207 |
\item {\tt FE} theorem, 78, 82
|
|
208 |
\item {\tt FEL} theorem, 78
|
|
209 |
\item {\tt FF} theorem, 78
|
|
210 |
\item {\tt filseq_resolve_tac}, \bold{64}
|
|
211 |
\item {\tt filt_resolve_tac}, 64, 80
|
|
212 |
\item {\tt filter} constant, 28
|
|
213 |
\item flex-flex constraints, 60
|
|
214 |
\item {\tt FOL} theory, 81
|
|
215 |
\item {\tt foldl} constant, 28
|
|
216 |
\item {\tt form_rls}, \bold{79}
|
|
217 |
\item {\tt formL_rls}, \bold{79}
|
|
218 |
\item {\tt forms_of_seq}, \bold{63}
|
|
219 |
\item {\tt fst} constant, 23, 72, 77
|
|
220 |
\item {\tt fst_conv} theorem, 23
|
|
221 |
\item {\tt fst_def} theorem, 77
|
|
222 |
\item {\tt Fun} theory, 21
|
|
223 |
\item {\textit {fun}} type, 7
|
|
224 |
\item {\tt fun_cong} theorem, 11
|
2665
|
225 |
\item function applications
|
6141
|
226 |
\subitem in \CTT, 74
|
2665
|
227 |
|
|
228 |
\indexspace
|
|
229 |
|
6141
|
230 |
\item {\tt hd} constant, 28
|
|
231 |
\item higher-order logic, 5--57
|
|
232 |
\item {\tt HOL} theory, 1, 5
|
|
233 |
\item {\sc hol} system, 5, 8
|
|
234 |
\item {\tt HOL_basic_ss}, \bold{21}
|
|
235 |
\item {\tt HOL_cs}, \bold{22}
|
|
236 |
\item {\tt HOL_quantifiers}, \bold{8}, 16
|
|
237 |
\item {\tt HOL_ss}, \bold{21}
|
|
238 |
\item {\tt HOLCF} theory, 1
|
|
239 |
\item {\tt hyp_rew_tac}, \bold{81}
|
|
240 |
\item {\tt hyp_subst_tac}, 21
|
2665
|
241 |
|
|
242 |
\indexspace
|
|
243 |
|
6141
|
244 |
\item {\textit {i}} type, 71
|
|
245 |
\item {\tt If} constant, 6
|
|
246 |
\item {\tt if_def} theorem, 10
|
|
247 |
\item {\tt if_not_P} theorem, 12
|
|
248 |
\item {\tt if_P} theorem, 12
|
|
249 |
\item {\tt iff} theorem, 9, 10
|
|
250 |
\item {\tt iff_def} theorem, 61
|
|
251 |
\item {\tt iffCE} theorem, 12, 16
|
|
252 |
\item {\tt iffD1} theorem, 11
|
|
253 |
\item {\tt iffD2} theorem, 11
|
|
254 |
\item {\tt iffE} theorem, 11
|
|
255 |
\item {\tt iffI} theorem, 11
|
|
256 |
\item {\tt iffL} theorem, 62, 69
|
|
257 |
\item {\tt iffR} theorem, 62
|
|
258 |
\item {\tt ILL} theory, 1
|
|
259 |
\item {\tt image_def} theorem, 17
|
|
260 |
\item {\tt imageE} theorem, 19
|
|
261 |
\item {\tt imageI} theorem, 19
|
|
262 |
\item {\tt impCE} theorem, 12
|
|
263 |
\item {\tt impE} theorem, 11
|
|
264 |
\item {\tt impI} theorem, 9
|
|
265 |
\item {\tt impL} theorem, 61
|
|
266 |
\item {\tt impR} theorem, 61
|
|
267 |
\item {\tt in} symbol, 7
|
|
268 |
\item {\textit {ind}} type, 24
|
|
269 |
\item {\tt induct_tac}, 26, \bold{40}
|
|
270 |
\item {\tt inductive}, 51--53
|
|
271 |
\item {\tt inj} constant, 21
|
|
272 |
\item {\tt inj_def} theorem, 21
|
|
273 |
\item {\tt inj_Inl} theorem, 25
|
|
274 |
\item {\tt inj_Inr} theorem, 25
|
|
275 |
\item {\tt inj_on} constant, 21
|
|
276 |
\item {\tt inj_on_def} theorem, 21
|
|
277 |
\item {\tt inj_Suc} theorem, 25
|
|
278 |
\item {\tt Inl} constant, 25
|
|
279 |
\item {\tt inl} constant, 72, 77, 87
|
|
280 |
\item {\tt Inl_not_Inr} theorem, 25
|
|
281 |
\item {\tt Inr} constant, 25
|
|
282 |
\item {\tt inr} constant, 72, 77
|
|
283 |
\item {\tt insert} constant, 14
|
|
284 |
\item {\tt insert_def} theorem, 17
|
|
285 |
\item {\tt insertE} theorem, 19
|
|
286 |
\item {\tt insertI1} theorem, 19
|
|
287 |
\item {\tt insertI2} theorem, 19
|
|
288 |
\item {\tt INT} symbol, 14--16
|
|
289 |
\item {\tt Int} symbol, 14
|
|
290 |
\item {\tt Int_absorb} theorem, 20
|
|
291 |
\item {\tt Int_assoc} theorem, 20
|
|
292 |
\item {\tt Int_commute} theorem, 20
|
|
293 |
\item {\tt INT_D} theorem, 19
|
|
294 |
\item {\tt Int_def} theorem, 17
|
|
295 |
\item {\tt INT_E} theorem, 19
|
|
296 |
\item {\tt Int_greatest} theorem, 20
|
|
297 |
\item {\tt INT_I} theorem, 19
|
|
298 |
\item {\tt Int_Inter_image} theorem, 20
|
|
299 |
\item {\tt Int_lower1} theorem, 20
|
|
300 |
\item {\tt Int_lower2} theorem, 20
|
|
301 |
\item {\tt Int_Un_distrib} theorem, 20
|
|
302 |
\item {\tt Int_Union} theorem, 20
|
|
303 |
\item {\tt IntD1} theorem, 19
|
|
304 |
\item {\tt IntD2} theorem, 19
|
|
305 |
\item {\tt IntE} theorem, 19
|
|
306 |
\item {\tt INTER} constant, 14
|
|
307 |
\item {\tt Inter} constant, 14
|
|
308 |
\item {\tt INTER1} constant, 14
|
|
309 |
\item {\tt INTER1_def} theorem, 17
|
|
310 |
\item {\tt INTER_def} theorem, 17
|
|
311 |
\item {\tt Inter_def} theorem, 17
|
|
312 |
\item {\tt Inter_greatest} theorem, 20
|
|
313 |
\item {\tt Inter_lower} theorem, 20
|
|
314 |
\item {\tt Inter_Un_distrib} theorem, 20
|
|
315 |
\item {\tt InterD} theorem, 19
|
|
316 |
\item {\tt InterE} theorem, 19
|
|
317 |
\item {\tt InterI} theorem, 19
|
|
318 |
\item {\tt IntI} theorem, 19
|
|
319 |
\item {\tt intr_rls}, \bold{79}
|
|
320 |
\item {\tt intr_tac}, \bold{80}, 89, 90
|
|
321 |
\item {\tt intrL_rls}, \bold{79}
|
|
322 |
\item {\tt inv} constant, 21
|
|
323 |
\item {\tt inv_def} theorem, 21
|
2665
|
324 |
|
|
325 |
\indexspace
|
|
326 |
|
6141
|
327 |
\item {\tt lam} symbol, 74
|
|
328 |
\item {\tt lambda} constant, 72, 74
|
2665
|
329 |
\item $\lambda$-abstractions
|
6141
|
330 |
\subitem in \CTT, 74
|
|
331 |
\item {\tt last} constant, 28
|
|
332 |
\item {\tt LCF} theory, 1
|
|
333 |
\item {\tt LEAST} constant, 7, 8, 26
|
|
334 |
\item {\tt Least} constant, 6
|
|
335 |
\item {\tt Least_def} theorem, 10
|
|
336 |
\item {\tt length} constant, 28
|
|
337 |
\item {\tt less_induct} theorem, 27
|
|
338 |
\item {\tt Let} constant, 6, 9
|
|
339 |
\item {\tt let} symbol, 7, 9
|
|
340 |
\item {\tt Let_def} theorem, 9, 10
|
|
341 |
\item {\tt LFilter} theory, 55
|
|
342 |
\item {\tt List} theory, 27, 28
|
|
343 |
\item {\textit{list}} type, 27
|
|
344 |
\item {\tt LK} theory, 1, 58, 62
|
|
345 |
\item {\tt LK_dup_pack}, \bold{65}, 66
|
|
346 |
\item {\tt LK_pack}, \bold{65}
|
|
347 |
\item {\tt LList} theory, 54
|
2665
|
348 |
|
|
349 |
\indexspace
|
|
350 |
|
6141
|
351 |
\item {\tt map} constant, 28
|
|
352 |
\item {\tt max} constant, 7, 26
|
|
353 |
\item {\tt mem} symbol, 28
|
|
354 |
\item {\tt mem_Collect_eq} theorem, 16, 17
|
|
355 |
\item {\tt min} constant, 7, 26
|
|
356 |
\item {\tt minus} class, 7
|
|
357 |
\item {\tt mod} symbol, 25, 83
|
|
358 |
\item {\tt mod_def} theorem, 83
|
|
359 |
\item {\tt mod_geq} theorem, 26
|
|
360 |
\item {\tt mod_less} theorem, 26
|
|
361 |
\item {\tt Modal} theory, 1
|
|
362 |
\item {\tt mono} constant, 7
|
|
363 |
\item {\tt mp} theorem, 9
|
|
364 |
\item {\tt mp_tac}, \bold{81}
|
|
365 |
\item {\tt mult_assoc} theorem, 83
|
|
366 |
\item {\tt mult_commute} theorem, 83
|
|
367 |
\item {\tt mult_def} theorem, 83
|
|
368 |
\item {\tt mult_typing} theorem, 83
|
|
369 |
\item {\tt multC0} theorem, 83
|
|
370 |
\item {\tt multC_succ} theorem, 83
|
|
371 |
\item {\tt mutual_induct_tac}, \bold{40}
|
6072
|
372 |
|
|
373 |
\indexspace
|
|
374 |
|
6141
|
375 |
\item {\tt N} constant, 72
|
|
376 |
\item {\tt n_not_Suc_n} theorem, 25
|
|
377 |
\item {\tt Nat} theory, 26
|
|
378 |
\item {\textit {nat}} type, 25, 26
|
|
379 |
\item {\textit{nat}} type, 24--27
|
|
380 |
\item {\tt nat_induct} theorem, 25
|
|
381 |
\item {\tt nat_rec} constant, 26
|
|
382 |
\item {\tt NatDef} theory, 24
|
|
383 |
\item {\tt NC0} theorem, 76
|
|
384 |
\item {\tt NC_succ} theorem, 76
|
|
385 |
\item {\tt NE} theorem, 75, 76, 84
|
|
386 |
\item {\tt NEL} theorem, 76
|
|
387 |
\item {\tt NF} theorem, 76, 85
|
|
388 |
\item {\tt NI0} theorem, 76
|
|
389 |
\item {\tt NI_succ} theorem, 76
|
|
390 |
\item {\tt NI_succL} theorem, 76
|
|
391 |
\item {\tt NIO} theorem, 84
|
|
392 |
\item {\tt Not} constant, 6, 59
|
|
393 |
\item {\tt not_def} theorem, 10
|
|
394 |
\item {\tt not_sym} theorem, 11
|
|
395 |
\item {\tt notE} theorem, 11
|
|
396 |
\item {\tt notI} theorem, 11
|
|
397 |
\item {\tt notL} theorem, 61
|
|
398 |
\item {\tt notnotD} theorem, 12
|
|
399 |
\item {\tt notR} theorem, 61
|
|
400 |
\item {\tt null} constant, 28
|
2665
|
401 |
|
|
402 |
\indexspace
|
|
403 |
|
6141
|
404 |
\item {\textit {o}} type, 58
|
|
405 |
\item {\tt o} symbol, 6, 17
|
|
406 |
\item {\tt o_def} theorem, 10
|
|
407 |
\item {\tt of} symbol, 9
|
|
408 |
\item {\tt or_def} theorem, 10
|
|
409 |
\item {\tt Ord} theory, 7
|
|
410 |
\item {\tt ord} class, 7, 8, 26
|
|
411 |
\item {\tt order} class, 7, 26
|
2665
|
412 |
|
|
413 |
\indexspace
|
|
414 |
|
6141
|
415 |
\item {\tt pack} ML type, 64
|
|
416 |
\item {\tt Pair} constant, 23
|
|
417 |
\item {\tt pair} constant, 72
|
|
418 |
\item {\tt Pair_eq} theorem, 23
|
|
419 |
\item {\tt Pair_inject} theorem, 23
|
|
420 |
\item {\tt PairE} theorem, 23
|
|
421 |
\item {\tt pc_tac}, \bold{66}, \bold{82}, 88, 89
|
|
422 |
\item {\tt plus} class, 7
|
|
423 |
\item {\tt PlusC_inl} theorem, 78
|
|
424 |
\item {\tt PlusC_inr} theorem, 78
|
|
425 |
\item {\tt PlusE} theorem, 78, 82, 86
|
|
426 |
\item {\tt PlusEL} theorem, 78
|
|
427 |
\item {\tt PlusF} theorem, 78
|
|
428 |
\item {\tt PlusFL} theorem, 78
|
|
429 |
\item {\tt PlusI_inl} theorem, 78, 87
|
|
430 |
\item {\tt PlusI_inlL} theorem, 78
|
|
431 |
\item {\tt PlusI_inr} theorem, 78
|
|
432 |
\item {\tt PlusI_inrL} theorem, 78
|
|
433 |
\item {\tt Pow} constant, 14
|
|
434 |
\item {\tt Pow_def} theorem, 17
|
|
435 |
\item {\tt PowD} theorem, 19
|
|
436 |
\item {\tt PowI} theorem, 19
|
|
437 |
\item {\tt primrec}, 45--48
|
|
438 |
\item {\tt primrec} symbol, 26
|
|
439 |
\item priorities, 3
|
|
440 |
\item {\tt PROD} symbol, 73, 74
|
|
441 |
\item {\tt Prod} constant, 72
|
|
442 |
\item {\tt Prod} theory, 23
|
|
443 |
\item {\tt ProdC} theorem, 76, 92
|
|
444 |
\item {\tt ProdC2} theorem, 76
|
|
445 |
\item {\tt ProdE} theorem, 76, 89, 91, 93
|
|
446 |
\item {\tt ProdEL} theorem, 76
|
|
447 |
\item {\tt ProdF} theorem, 76
|
|
448 |
\item {\tt ProdFL} theorem, 76
|
|
449 |
\item {\tt ProdI} theorem, 76, 82, 84
|
|
450 |
\item {\tt ProdIL} theorem, 76
|
|
451 |
\item {\tt prop_cs}, \bold{22}
|
|
452 |
\item {\tt prop_pack}, \bold{65}
|
2665
|
453 |
|
|
454 |
\indexspace
|
|
455 |
|
6141
|
456 |
\item {\tt qed_spec_mp}, 43
|
6072
|
457 |
|
|
458 |
\indexspace
|
|
459 |
|
6141
|
460 |
\item {\tt range} constant, 14, 56
|
|
461 |
\item {\tt range_def} theorem, 17
|
|
462 |
\item {\tt rangeE} theorem, 19, 56
|
|
463 |
\item {\tt rangeI} theorem, 19
|
|
464 |
\item {\tt rec} constant, 72, 75
|
|
465 |
\item {\tt recdef}, 48--51
|
|
466 |
\item {\tt record}, 33
|
|
467 |
\item {\tt record_split_tac}, 35, 36
|
6072
|
468 |
\item recursion
|
6141
|
469 |
\subitem general, 48--51
|
|
470 |
\subitem primitive, 45--48
|
|
471 |
\item recursive functions, \see{recursion}{44}
|
|
472 |
\item {\tt red_if_equal} theorem, 75
|
|
473 |
\item {\tt Reduce} constant, 72, 75, 81
|
|
474 |
\item {\tt refl} theorem, 9, 61
|
|
475 |
\item {\tt refl_elem} theorem, 75, 79
|
|
476 |
\item {\tt refl_red} theorem, 75
|
|
477 |
\item {\tt refl_type} theorem, 75, 79
|
|
478 |
\item {\tt REPEAT_FIRST}, 80
|
|
479 |
\item {\tt repeat_goal_tac}, \bold{66}
|
|
480 |
\item {\tt replace_type} theorem, 79, 91
|
|
481 |
\item {\tt reresolve_tac}, \bold{66}
|
|
482 |
\item {\tt res_inst_tac}, 8
|
|
483 |
\item {\tt rev} constant, 28
|
|
484 |
\item {\tt rew_tac}, \bold{81}
|
|
485 |
\item {\tt RL}, 86
|
|
486 |
\item {\tt RS}, 91, 93
|
2665
|
487 |
|
|
488 |
\indexspace
|
|
489 |
|
6141
|
490 |
\item {\tt safe_goal_tac}, \bold{66}
|
|
491 |
\item {\tt safe_tac}, \bold{82}
|
|
492 |
\item {\tt safestep_tac}, \bold{82}
|
6072
|
493 |
\item search
|
6141
|
494 |
\subitem best-first, 57
|
|
495 |
\item {\tt select_equality} theorem, 10, 12
|
|
496 |
\item {\tt selectI} theorem, 9, 10
|
|
497 |
\item {\tt Seqof} constant, 59
|
|
498 |
\item sequent calculus, 58--70
|
|
499 |
\item {\tt Set} theory, 13, 16
|
|
500 |
\item {\tt set} constant, 28
|
|
501 |
\item {\tt set} type, 13
|
|
502 |
\item {\tt set_current_thy}, 57
|
|
503 |
\item {\tt set_diff_def} theorem, 17
|
|
504 |
\item {\tt show_sorts}, 8
|
|
505 |
\item {\tt show_types}, 8
|
|
506 |
\item {\tt Sigma} constant, 23
|
|
507 |
\item {\tt Sigma_def} theorem, 23
|
|
508 |
\item {\tt SigmaE} theorem, 23
|
|
509 |
\item {\tt SigmaI} theorem, 23
|
6072
|
510 |
\item simplification
|
6141
|
511 |
\subitem of conjunctions, 21
|
|
512 |
\item {\tt size} constant, 40
|
|
513 |
\item {\tt snd} constant, 23, 72, 77
|
|
514 |
\item {\tt snd_conv} theorem, 23
|
|
515 |
\item {\tt snd_def} theorem, 77
|
|
516 |
\item {\tt sobj} type, 62
|
|
517 |
\item {\tt spec} theorem, 12
|
|
518 |
\item {\tt split} constant, 23, 72, 86
|
|
519 |
\item {\tt split} theorem, 23
|
|
520 |
\item {\tt split_all_tac}, \bold{24}
|
|
521 |
\item {\tt split_if} theorem, 12, 22
|
|
522 |
\item {\tt split_list_case} theorem, 27
|
|
523 |
\item {\tt split_split} theorem, 23
|
|
524 |
\item {\tt split_sum_case} theorem, 25
|
|
525 |
\item {\tt ssubst} theorem, 11, 13
|
|
526 |
\item {\tt stac}, \bold{21}
|
|
527 |
\item {\tt step_tac}, \bold{66}, \bold{82}
|
|
528 |
\item {\tt strip_tac}, \bold{13}
|
|
529 |
\item {\tt subset_def} theorem, 17
|
|
530 |
\item {\tt subset_refl} theorem, 18
|
|
531 |
\item {\tt subset_trans} theorem, 18
|
|
532 |
\item {\tt subsetCE} theorem, 16, 18
|
|
533 |
\item {\tt subsetD} theorem, 16, 18
|
|
534 |
\item {\tt subsetI} theorem, 18
|
|
535 |
\item {\tt subst} theorem, 9
|
|
536 |
\item {\tt subst_elem} theorem, 75
|
|
537 |
\item {\tt subst_elemL} theorem, 75
|
|
538 |
\item {\tt subst_eqtyparg} theorem, 79, 91
|
|
539 |
\item {\tt subst_prodE} theorem, 77, 79
|
|
540 |
\item {\tt subst_type} theorem, 75
|
|
541 |
\item {\tt subst_typeL} theorem, 75
|
|
542 |
\item {\tt Suc} constant, 25
|
|
543 |
\item {\tt Suc_not_Zero} theorem, 25
|
|
544 |
\item {\tt succ} constant, 72
|
|
545 |
\item {\tt SUM} symbol, 73, 74
|
|
546 |
\item {\tt Sum} constant, 72
|
|
547 |
\item {\tt Sum} theory, 24
|
|
548 |
\item {\tt sum_case} constant, 25
|
|
549 |
\item {\tt sum_case_Inl} theorem, 25
|
|
550 |
\item {\tt sum_case_Inr} theorem, 25
|
|
551 |
\item {\tt SumC} theorem, 77
|
|
552 |
\item {\tt SumE} theorem, 77, 82, 86
|
|
553 |
\item {\tt sumE} theorem, 25
|
|
554 |
\item {\tt SumE_fst} theorem, 77, 79, 91, 92
|
|
555 |
\item {\tt SumE_snd} theorem, 77, 79, 93
|
|
556 |
\item {\tt SumEL} theorem, 77
|
|
557 |
\item {\tt SumF} theorem, 77
|
|
558 |
\item {\tt SumFL} theorem, 77
|
|
559 |
\item {\tt SumI} theorem, 77, 87
|
|
560 |
\item {\tt SumIL} theorem, 77
|
|
561 |
\item {\tt SumIL2} theorem, 79
|
|
562 |
\item {\tt surj} constant, 17, 21
|
|
563 |
\item {\tt surj_def} theorem, 21
|
|
564 |
\item {\tt surjective_pairing} theorem, 23
|
|
565 |
\item {\tt surjective_sum} theorem, 25
|
|
566 |
\item {\tt swap} theorem, 12
|
|
567 |
\item {\tt swap_res_tac}, 57
|
|
568 |
\item {\tt sym} theorem, 11, 61
|
|
569 |
\item {\tt sym_elem} theorem, 75
|
|
570 |
\item {\tt sym_type} theorem, 75
|
|
571 |
\item {\tt symL} theorem, 62
|
2665
|
572 |
|
|
573 |
\indexspace
|
|
574 |
|
6141
|
575 |
\item {\tt T} constant, 72
|
|
576 |
\item {\textit {t}} type, 71
|
|
577 |
\item {\tt take} constant, 28
|
|
578 |
\item {\tt takeWhile} constant, 28
|
|
579 |
\item {\tt TC} theorem, 78
|
|
580 |
\item {\tt TE} theorem, 78
|
|
581 |
\item {\tt TEL} theorem, 78
|
|
582 |
\item {\tt term} class, 7, 58
|
|
583 |
\item {\tt test_assume_tac}, \bold{80}
|
|
584 |
\item {\tt TF} theorem, 78
|
|
585 |
\item {\tt THE} symbol, 59
|
|
586 |
\item {\tt The} constant, 59
|
|
587 |
\item {\tt The} theorem, 61
|
|
588 |
\item {\tt thinL} theorem, 61
|
|
589 |
\item {\tt thinR} theorem, 61
|
|
590 |
\item {\tt TI} theorem, 78
|
|
591 |
\item {\tt times} class, 7
|
|
592 |
\item {\tt tl} constant, 28
|
6072
|
593 |
\item tracing
|
6141
|
594 |
\subitem of unification, 8
|
|
595 |
\item {\tt trans} theorem, 11, 61
|
|
596 |
\item {\tt trans_elem} theorem, 75
|
|
597 |
\item {\tt trans_red} theorem, 75
|
|
598 |
\item {\tt trans_tac}, 27
|
|
599 |
\item {\tt trans_type} theorem, 75
|
|
600 |
\item {\tt True} constant, 6, 59
|
|
601 |
\item {\tt True_def} theorem, 10, 61
|
|
602 |
\item {\tt True_or_False} theorem, 9, 10
|
|
603 |
\item {\tt TrueI} theorem, 11
|
|
604 |
\item {\tt Trueprop} constant, 6, 59
|
|
605 |
\item {\tt TrueR} theorem, 62
|
|
606 |
\item {\tt tt} constant, 72
|
|
607 |
\item {\tt Type} constant, 72
|
|
608 |
\item type definition, \bold{30}
|
|
609 |
\item {\tt typechk_tac}, \bold{80}, 85, 88, 92, 93
|
|
610 |
\item {\tt typedef}, 27
|
2665
|
611 |
|
|
612 |
\indexspace
|
|
613 |
|
6141
|
614 |
\item {\tt UN} symbol, 14--16
|
|
615 |
\item {\tt Un} symbol, 14
|
|
616 |
\item {\tt Un1} theorem, 16
|
|
617 |
\item {\tt Un2} theorem, 16
|
|
618 |
\item {\tt Un_absorb} theorem, 20
|
|
619 |
\item {\tt Un_assoc} theorem, 20
|
|
620 |
\item {\tt Un_commute} theorem, 20
|
|
621 |
\item {\tt Un_def} theorem, 17
|
|
622 |
\item {\tt UN_E} theorem, 19
|
|
623 |
\item {\tt UN_I} theorem, 19
|
|
624 |
\item {\tt Un_Int_distrib} theorem, 20
|
|
625 |
\item {\tt Un_Inter} theorem, 20
|
|
626 |
\item {\tt Un_least} theorem, 20
|
|
627 |
\item {\tt Un_Union_image} theorem, 20
|
|
628 |
\item {\tt Un_upper1} theorem, 20
|
|
629 |
\item {\tt Un_upper2} theorem, 20
|
|
630 |
\item {\tt UnCI} theorem, 16, 19
|
|
631 |
\item {\tt UnE} theorem, 19
|
|
632 |
\item {\tt UnI1} theorem, 19
|
|
633 |
\item {\tt UnI2} theorem, 19
|
6072
|
634 |
\item unification
|
6141
|
635 |
\subitem incompleteness of, 8
|
|
636 |
\item {\tt Unify.trace_types}, 8
|
|
637 |
\item {\tt UNION} constant, 14
|
|
638 |
\item {\tt Union} constant, 14
|
|
639 |
\item {\tt UNION1} constant, 14
|
|
640 |
\item {\tt UNION1_def} theorem, 17
|
|
641 |
\item {\tt UNION_def} theorem, 17
|
|
642 |
\item {\tt Union_def} theorem, 17
|
|
643 |
\item {\tt Union_least} theorem, 20
|
|
644 |
\item {\tt Union_Un_distrib} theorem, 20
|
|
645 |
\item {\tt Union_upper} theorem, 20
|
|
646 |
\item {\tt UnionE} theorem, 19
|
|
647 |
\item {\tt UnionI} theorem, 19
|
|
648 |
\item {\tt unit_eq} theorem, 24
|
2665
|
649 |
|
|
650 |
\indexspace
|
|
651 |
|
6141
|
652 |
\item {\tt when} constant, 72, 77, 86
|
2665
|
653 |
|
|
654 |
\indexspace
|
|
655 |
|
6141
|
656 |
\item {\tt zero_ne_succ} theorem, 75, 76
|
|
657 |
\item {\tt ZF} theory, 5
|
2665
|
658 |
|
|
659 |
\end{theindex}
|