6156
|
1 |
\begin{theindex}
|
|
2 |
|
|
3 |
\item {\tt\#*} symbol, 45
|
|
4 |
\item {\tt\#+} symbol, 45
|
|
5 |
\item {\tt\#-} symbol, 45
|
|
6 |
\item {\tt\&} symbol, 5
|
|
7 |
\item {\tt *} symbol, 25
|
|
8 |
\item {\tt +} symbol, 41
|
|
9 |
\item {\tt -} symbol, 24
|
|
10 |
\item {\tt -->} symbol, 5
|
|
11 |
\item {\tt ->} symbol, 25
|
|
12 |
\item {\tt -``} symbol, 24
|
|
13 |
\item {\tt :} symbol, 24
|
|
14 |
\item {\tt <->} symbol, 5
|
|
15 |
\item {\tt <=} symbol, 24
|
|
16 |
\item {\tt =} symbol, 5
|
|
17 |
\item {\tt `} symbol, 24
|
|
18 |
\item {\tt ``} symbol, 24
|
|
19 |
\item {\tt |} symbol, 5
|
|
20 |
|
|
21 |
\indexspace
|
|
22 |
|
|
23 |
\item {\tt 0} constant, 24
|
|
24 |
|
|
25 |
\indexspace
|
|
26 |
|
|
27 |
\item {\tt add_0} theorem, 45
|
|
28 |
\item {\tt add_mult_dist} theorem, 45
|
|
29 |
\item {\tt add_succ} theorem, 45
|
|
30 |
\item {\tt ALL} symbol, 5, 25
|
|
31 |
\item {\tt All} constant, 5
|
|
32 |
\item {\tt all_dupE} theorem, 3, 7
|
|
33 |
\item {\tt all_impE} theorem, 7
|
|
34 |
\item {\tt allE} theorem, 3, 7
|
|
35 |
\item {\tt allI} theorem, 6
|
|
36 |
\item {\tt and_def} theorem, 41
|
|
37 |
\item {\tt apply_def} theorem, 29
|
|
38 |
\item {\tt apply_equality} theorem, 38, 39, 69
|
|
39 |
\item {\tt apply_equality2} theorem, 38
|
|
40 |
\item {\tt apply_iff} theorem, 38
|
|
41 |
\item {\tt apply_Pair} theorem, 38, 69
|
|
42 |
\item {\tt apply_type} theorem, 38
|
|
43 |
\item {\tt Arith} theory, 42
|
|
44 |
\item assumptions
|
|
45 |
\subitem contradictory, 14
|
|
46 |
|
|
47 |
\indexspace
|
|
48 |
|
|
49 |
\item {\tt Ball} constant, 24, 27
|
|
50 |
\item {\tt ball_cong} theorem, 31, 32
|
|
51 |
\item {\tt Ball_def} theorem, 28
|
|
52 |
\item {\tt ballE} theorem, 31, 32
|
|
53 |
\item {\tt ballI} theorem, 31
|
|
54 |
\item {\tt beta} theorem, 38, 39
|
|
55 |
\item {\tt Bex} constant, 24, 27
|
|
56 |
\item {\tt bex_cong} theorem, 31, 32
|
|
57 |
\item {\tt Bex_def} theorem, 28
|
|
58 |
\item {\tt bexCI} theorem, 31
|
|
59 |
\item {\tt bexE} theorem, 31
|
|
60 |
\item {\tt bexI} theorem, 31
|
|
61 |
\item {\tt bij} constant, 44
|
|
62 |
\item {\tt bij_converse_bij} theorem, 44
|
|
63 |
\item {\tt bij_def} theorem, 44
|
|
64 |
\item {\tt bij_disjoint_Un} theorem, 44
|
|
65 |
\item {\tt Blast_tac}, 15, 67, 68
|
|
66 |
\item {\tt blast_tac}, 16, 17, 19
|
|
67 |
\item {\tt bnd_mono_def} theorem, 43
|
|
68 |
\item {\tt Bool} theory, 39
|
|
69 |
\item {\tt bool_0I} theorem, 41
|
|
70 |
\item {\tt bool_1I} theorem, 41
|
|
71 |
\item {\tt bool_def} theorem, 41
|
|
72 |
\item {\tt boolE} theorem, 41
|
|
73 |
\item {\tt bspec} theorem, 31
|
|
74 |
|
|
75 |
\indexspace
|
|
76 |
|
|
77 |
\item {\tt case} constant, 41
|
|
78 |
\item {\tt case_def} theorem, 41
|
|
79 |
\item {\tt case_Inl} theorem, 41
|
|
80 |
\item {\tt case_Inr} theorem, 41
|
|
81 |
\item {\tt coinduct} theorem, 43
|
|
82 |
\item {\tt coinductive}, 57--62
|
|
83 |
\item {\tt Collect} constant, 24, 25, 30
|
|
84 |
\item {\tt Collect_def} theorem, 28
|
|
85 |
\item {\tt Collect_subset} theorem, 35
|
|
86 |
\item {\tt CollectD1} theorem, 32, 33
|
|
87 |
\item {\tt CollectD2} theorem, 32, 33
|
|
88 |
\item {\tt CollectE} theorem, 32, 33
|
|
89 |
\item {\tt CollectI} theorem, 33
|
|
90 |
\item {\tt comp_assoc} theorem, 44
|
|
91 |
\item {\tt comp_bij} theorem, 44
|
|
92 |
\item {\tt comp_def} theorem, 44
|
|
93 |
\item {\tt comp_func} theorem, 44
|
|
94 |
\item {\tt comp_func_apply} theorem, 44
|
|
95 |
\item {\tt comp_inj} theorem, 44
|
|
96 |
\item {\tt comp_surj} theorem, 44
|
|
97 |
\item {\tt comp_type} theorem, 44
|
|
98 |
\item {\tt cond_0} theorem, 41
|
|
99 |
\item {\tt cond_1} theorem, 41
|
|
100 |
\item {\tt cond_def} theorem, 41
|
|
101 |
\item congruence rules, 32
|
|
102 |
\item {\tt conj_cong}, 4
|
|
103 |
\item {\tt conj_impE} theorem, 7, 8
|
|
104 |
\item {\tt conjE} theorem, 7
|
|
105 |
\item {\tt conjI} theorem, 6
|
|
106 |
\item {\tt conjunct1} theorem, 6
|
|
107 |
\item {\tt conjunct2} theorem, 6
|
|
108 |
\item {\tt cons} constant, 23, 24
|
|
109 |
\item {\tt cons_def} theorem, 29
|
|
110 |
\item {\tt Cons_iff} theorem, 47
|
|
111 |
\item {\tt consCI} theorem, 34
|
|
112 |
\item {\tt consE} theorem, 34
|
|
113 |
\item {\tt ConsI} theorem, 47
|
|
114 |
\item {\tt consI1} theorem, 34
|
|
115 |
\item {\tt consI2} theorem, 34
|
|
116 |
\item {\tt converse} constant, 24, 37
|
|
117 |
\item {\tt converse_def} theorem, 29
|
|
118 |
\item {\tt cut_facts_tac}, 17
|
|
119 |
|
|
120 |
\indexspace
|
|
121 |
|
|
122 |
\item {\tt datatype}, 48--55
|
|
123 |
\item {\tt Diff_cancel} theorem, 40
|
|
124 |
\item {\tt Diff_contains} theorem, 35
|
|
125 |
\item {\tt Diff_def} theorem, 28
|
|
126 |
\item {\tt Diff_disjoint} theorem, 40
|
|
127 |
\item {\tt Diff_Int} theorem, 40
|
|
128 |
\item {\tt Diff_partition} theorem, 40
|
|
129 |
\item {\tt Diff_subset} theorem, 35
|
|
130 |
\item {\tt Diff_Un} theorem, 40
|
|
131 |
\item {\tt DiffD1} theorem, 34
|
|
132 |
\item {\tt DiffD2} theorem, 34
|
|
133 |
\item {\tt DiffE} theorem, 34
|
|
134 |
\item {\tt DiffI} theorem, 34
|
|
135 |
\item {\tt disj_impE} theorem, 7, 8, 12
|
|
136 |
\item {\tt disjCI} theorem, 9
|
|
137 |
\item {\tt disjE} theorem, 6
|
|
138 |
\item {\tt disjI1} theorem, 6
|
|
139 |
\item {\tt disjI2} theorem, 6
|
|
140 |
\item {\tt div} symbol, 45
|
|
141 |
\item {\tt div_def} theorem, 45
|
|
142 |
\item {\tt domain} constant, 24, 37
|
|
143 |
\item {\tt domain_def} theorem, 29
|
|
144 |
\item {\tt domain_of_fun} theorem, 38
|
|
145 |
\item {\tt domain_subset} theorem, 37
|
|
146 |
\item {\tt domain_type} theorem, 38
|
|
147 |
\item {\tt domainE} theorem, 37
|
|
148 |
\item {\tt domainI} theorem, 37
|
|
149 |
\item {\tt double_complement} theorem, 40
|
|
150 |
\item {\tt dresolve_tac}, 66
|
|
151 |
|
|
152 |
\indexspace
|
|
153 |
|
|
154 |
\item {\tt empty_subsetI} theorem, 31
|
|
155 |
\item {\tt emptyE} theorem, 31
|
|
156 |
\item {\tt eq_mp_tac}, \bold{8}
|
|
157 |
\item {\tt equalityD1} theorem, 31
|
|
158 |
\item {\tt equalityD2} theorem, 31
|
|
159 |
\item {\tt equalityE} theorem, 31
|
|
160 |
\item {\tt equalityI} theorem, 31, 65
|
|
161 |
\item {\tt equals0D} theorem, 31
|
|
162 |
\item {\tt equals0I} theorem, 31
|
|
163 |
\item {\tt eresolve_tac}, 14
|
|
164 |
\item {\tt eta} theorem, 38, 39
|
|
165 |
\item {\tt EX} symbol, 5, 25
|
|
166 |
\item {\tt Ex} constant, 5
|
|
167 |
\item {\tt EX!} symbol, 5
|
|
168 |
\item {\tt ex/Term} theory, 49
|
|
169 |
\item {\tt Ex1} constant, 5
|
|
170 |
\item {\tt ex1_def} theorem, 6
|
|
171 |
\item {\tt ex1E} theorem, 7
|
|
172 |
\item {\tt ex1I} theorem, 7
|
|
173 |
\item {\tt ex_impE} theorem, 7
|
|
174 |
\item {\tt exCI} theorem, 9, 13
|
|
175 |
\item {\tt excluded_middle} theorem, 9
|
|
176 |
\item {\tt exE} theorem, 6
|
|
177 |
\item {\tt exhaust_tac}, \bold{51}
|
|
178 |
\item {\tt exI} theorem, 6
|
|
179 |
\item {\tt extension} theorem, 28
|
|
180 |
|
|
181 |
\indexspace
|
|
182 |
|
|
183 |
\item {\tt False} constant, 5
|
|
184 |
\item {\tt FalseE} theorem, 6
|
|
185 |
\item {\tt field} constant, 24
|
|
186 |
\item {\tt field_def} theorem, 29
|
|
187 |
\item {\tt field_subset} theorem, 37
|
|
188 |
\item {\tt fieldCI} theorem, 37
|
|
189 |
\item {\tt fieldE} theorem, 37
|
|
190 |
\item {\tt fieldI1} theorem, 37
|
|
191 |
\item {\tt fieldI2} theorem, 37
|
|
192 |
\item {\tt Fin.consI} theorem, 46
|
|
193 |
\item {\tt Fin.emptyI} theorem, 46
|
|
194 |
\item {\tt Fin_induct} theorem, 46
|
|
195 |
\item {\tt Fin_mono} theorem, 46
|
|
196 |
\item {\tt Fin_subset} theorem, 46
|
|
197 |
\item {\tt Fin_UnI} theorem, 46
|
|
198 |
\item {\tt Fin_UnionI} theorem, 46
|
|
199 |
\item first-order logic, 3--21
|
|
200 |
\item {\tt Fixedpt} theory, 42
|
|
201 |
\item {\tt flat} constant, 47
|
|
202 |
\item {\tt FOL} theory, 3, 9
|
|
203 |
\item {\tt FOL_cs}, \bold{9}, 48
|
|
204 |
\item {\tt FOL_ss}, \bold{4}, 46
|
|
205 |
\item {\tt foundation} theorem, 28
|
|
206 |
\item {\tt fst} constant, 24, 30
|
|
207 |
\item {\tt fst_conv} theorem, 36
|
|
208 |
\item {\tt fst_def} theorem, 29
|
|
209 |
\item {\tt fun_disjoint_apply1} theorem, 38, 69
|
|
210 |
\item {\tt fun_disjoint_apply2} theorem, 38
|
|
211 |
\item {\tt fun_disjoint_Un} theorem, 38, 70
|
|
212 |
\item {\tt fun_empty} theorem, 38
|
|
213 |
\item {\tt fun_extension} theorem, 38, 39
|
|
214 |
\item {\tt fun_is_rel} theorem, 38
|
|
215 |
\item {\tt fun_single} theorem, 38
|
|
216 |
\item function applications
|
|
217 |
\subitem in \ZF, 24
|
|
218 |
|
|
219 |
\indexspace
|
|
220 |
|
|
221 |
\item {\tt gfp_def} theorem, 43
|
|
222 |
\item {\tt gfp_least} theorem, 43
|
|
223 |
\item {\tt gfp_mono} theorem, 43
|
|
224 |
\item {\tt gfp_subset} theorem, 43
|
|
225 |
\item {\tt gfp_Tarski} theorem, 43
|
|
226 |
\item {\tt gfp_upperbound} theorem, 43
|
|
227 |
\item {\tt Goalw}, 16, 17
|
|
228 |
|
|
229 |
\indexspace
|
|
230 |
|
|
231 |
\item {\tt hyp_subst_tac}, 4
|
|
232 |
|
|
233 |
\indexspace
|
|
234 |
|
|
235 |
\item {\textit {i}} type, 23
|
|
236 |
\item {\tt id} constant, 44
|
|
237 |
\item {\tt id_def} theorem, 44
|
|
238 |
\item {\tt if} constant, 24
|
|
239 |
\item {\tt if_def} theorem, 16, 28
|
|
240 |
\item {\tt if_not_P} theorem, 34
|
|
241 |
\item {\tt if_P} theorem, 34
|
|
242 |
\item {\tt ifE} theorem, 17
|
|
243 |
\item {\tt iff_def} theorem, 6
|
|
244 |
\item {\tt iff_impE} theorem, 7
|
|
245 |
\item {\tt iffCE} theorem, 9
|
|
246 |
\item {\tt iffD1} theorem, 7
|
|
247 |
\item {\tt iffD2} theorem, 7
|
|
248 |
\item {\tt iffE} theorem, 7
|
|
249 |
\item {\tt iffI} theorem, 7, 17
|
|
250 |
\item {\tt ifI} theorem, 17
|
|
251 |
\item {\tt IFOL} theory, 3
|
|
252 |
\item {\tt IFOL_ss}, \bold{4}
|
|
253 |
\item {\tt image_def} theorem, 29
|
|
254 |
\item {\tt imageE} theorem, 37
|
|
255 |
\item {\tt imageI} theorem, 37
|
|
256 |
\item {\tt imp_impE} theorem, 7, 12
|
|
257 |
\item {\tt impCE} theorem, 9
|
|
258 |
\item {\tt impE} theorem, 7, 8
|
|
259 |
\item {\tt impI} theorem, 6
|
|
260 |
\item {\tt in} symbol, 26
|
|
261 |
\item {\tt induct} theorem, 43
|
|
262 |
\item {\tt induct_tac}, \bold{51}
|
|
263 |
\item {\tt inductive}, 57--62
|
|
264 |
\item {\tt Inf} constant, 24, 30
|
|
265 |
\item {\tt infinity} theorem, 29
|
|
266 |
\item {\tt inj} constant, 44
|
|
267 |
\item {\tt inj_converse_inj} theorem, 44
|
|
268 |
\item {\tt inj_def} theorem, 44
|
|
269 |
\item {\tt Inl} constant, 41
|
|
270 |
\item {\tt Inl_def} theorem, 41
|
|
271 |
\item {\tt Inl_inject} theorem, 41
|
|
272 |
\item {\tt Inl_neq_Inr} theorem, 41
|
|
273 |
\item {\tt Inr} constant, 41
|
|
274 |
\item {\tt Inr_def} theorem, 41
|
|
275 |
\item {\tt Inr_inject} theorem, 41
|
|
276 |
\item {\tt INT} symbol, 25, 27
|
|
277 |
\item {\tt Int} symbol, 24
|
|
278 |
\item {\tt Int_absorb} theorem, 40
|
|
279 |
\item {\tt Int_assoc} theorem, 40
|
|
280 |
\item {\tt Int_commute} theorem, 40
|
|
281 |
\item {\tt Int_def} theorem, 28
|
|
282 |
\item {\tt INT_E} theorem, 33
|
|
283 |
\item {\tt Int_greatest} theorem, 35, 65, 66
|
|
284 |
\item {\tt INT_I} theorem, 33
|
|
285 |
\item {\tt Int_lower1} theorem, 35, 65
|
|
286 |
\item {\tt Int_lower2} theorem, 35, 65
|
|
287 |
\item {\tt Int_Un_distrib} theorem, 40
|
|
288 |
\item {\tt Int_Union_RepFun} theorem, 40
|
|
289 |
\item {\tt IntD1} theorem, 34
|
|
290 |
\item {\tt IntD2} theorem, 34
|
|
291 |
\item {\tt IntE} theorem, 34, 66
|
|
292 |
\item {\tt Inter} constant, 24
|
|
293 |
\item {\tt Inter_def} theorem, 28
|
|
294 |
\item {\tt Inter_greatest} theorem, 35
|
|
295 |
\item {\tt Inter_lower} theorem, 35
|
|
296 |
\item {\tt Inter_Un_distrib} theorem, 40
|
|
297 |
\item {\tt InterD} theorem, 33
|
|
298 |
\item {\tt InterE} theorem, 33
|
|
299 |
\item {\tt InterI} theorem, 32, 33
|
|
300 |
\item {\tt IntI} theorem, 34
|
|
301 |
\item {\tt IntPr.best_tac}, \bold{9}
|
|
302 |
\item {\tt IntPr.fast_tac}, \bold{8}, 11
|
|
303 |
\item {\tt IntPr.inst_step_tac}, \bold{8}
|
|
304 |
\item {\tt IntPr.safe_step_tac}, \bold{8}
|
|
305 |
\item {\tt IntPr.safe_tac}, \bold{8}
|
|
306 |
\item {\tt IntPr.step_tac}, \bold{8}
|
|
307 |
|
|
308 |
\indexspace
|
|
309 |
|
|
310 |
\item {\tt lam} symbol, 25, 27
|
|
311 |
\item {\tt lam_def} theorem, 29
|
|
312 |
\item {\tt lam_type} theorem, 38
|
|
313 |
\item {\tt Lambda} constant, 24, 27
|
|
314 |
\item $\lambda$-abstractions
|
|
315 |
\subitem in \ZF, 25
|
|
316 |
\item {\tt lamE} theorem, 38, 39
|
|
317 |
\item {\tt lamI} theorem, 38, 39
|
|
318 |
\item {\tt le_cs}, \bold{48}
|
|
319 |
\item {\tt left_comp_id} theorem, 44
|
|
320 |
\item {\tt left_comp_inverse} theorem, 44
|
|
321 |
\item {\tt left_inverse} theorem, 44
|
|
322 |
\item {\tt length} constant, 47
|
|
323 |
\item {\tt Let} constant, 23, 24
|
|
324 |
\item {\tt let} symbol, 26
|
|
325 |
\item {\tt Let_def} theorem, 23, 28
|
|
326 |
\item {\tt lfp_def} theorem, 43
|
|
327 |
\item {\tt lfp_greatest} theorem, 43
|
|
328 |
\item {\tt lfp_lowerbound} theorem, 43
|
|
329 |
\item {\tt lfp_mono} theorem, 43
|
|
330 |
\item {\tt lfp_subset} theorem, 43
|
|
331 |
\item {\tt lfp_Tarski} theorem, 43
|
|
332 |
\item {\tt list} constant, 47
|
|
333 |
\item {\tt List.induct} theorem, 47
|
|
334 |
\item {\tt list_case} constant, 47
|
|
335 |
\item {\tt list_mono} theorem, 47
|
|
336 |
\item {\tt logic} class, 3
|
|
337 |
|
|
338 |
\indexspace
|
|
339 |
|
|
340 |
\item {\tt map} constant, 47
|
|
341 |
\item {\tt map_app_distrib} theorem, 47
|
|
342 |
\item {\tt map_compose} theorem, 47
|
|
343 |
\item {\tt map_flat} theorem, 47
|
|
344 |
\item {\tt map_ident} theorem, 47
|
|
345 |
\item {\tt map_type} theorem, 47
|
|
346 |
\item {\tt mem_asym} theorem, 34, 35
|
|
347 |
\item {\tt mem_irrefl} theorem, 34
|
|
348 |
\item {\tt mk_cases}, 54, 61
|
|
349 |
\item {\tt mod} symbol, 45
|
|
350 |
\item {\tt mod_def} theorem, 45
|
|
351 |
\item {\tt mod_quo_equality} theorem, 45
|
|
352 |
\item {\tt mp} theorem, 6
|
|
353 |
\item {\tt mp_tac}, \bold{8}
|
|
354 |
\item {\tt mult_0} theorem, 45
|
|
355 |
\item {\tt mult_assoc} theorem, 45
|
|
356 |
\item {\tt mult_commute} theorem, 45
|
|
357 |
\item {\tt mult_succ} theorem, 45
|
|
358 |
\item {\tt mult_type} theorem, 45
|
|
359 |
|
|
360 |
\indexspace
|
|
361 |
|
|
362 |
\item {\tt Nat} theory, 42
|
|
363 |
\item {\tt nat} constant, 45
|
|
364 |
\item {\tt nat_0I} theorem, 45
|
|
365 |
\item {\tt nat_case} constant, 45
|
|
366 |
\item {\tt nat_case_0} theorem, 45
|
|
367 |
\item {\tt nat_case_def} theorem, 45
|
|
368 |
\item {\tt nat_case_succ} theorem, 45
|
|
369 |
\item {\tt nat_def} theorem, 45
|
|
370 |
\item {\tt nat_induct} theorem, 45
|
|
371 |
\item {\tt nat_succI} theorem, 45
|
|
372 |
\item {\tt Nil_Cons_iff} theorem, 47
|
|
373 |
\item {\tt NilI} theorem, 47
|
|
374 |
\item {\tt Not} constant, 5
|
|
375 |
\item {\tt not_def} theorem, 6, 41
|
|
376 |
\item {\tt not_impE} theorem, 7
|
|
377 |
\item {\tt notE} theorem, 7, 8
|
|
378 |
\item {\tt notI} theorem, 7
|
|
379 |
\item {\tt notnotD} theorem, 9
|
|
380 |
|
|
381 |
\indexspace
|
|
382 |
|
|
383 |
\item {\tt O} symbol, 44
|
|
384 |
\item {\textit {o}} type, 3
|
|
385 |
\item {\tt or_def} theorem, 41
|
|
386 |
|
|
387 |
\indexspace
|
|
388 |
|
|
389 |
\item {\tt Pair} constant, 24, 25
|
|
390 |
\item {\tt Pair_def} theorem, 29
|
|
391 |
\item {\tt Pair_inject} theorem, 36
|
|
392 |
\item {\tt Pair_inject1} theorem, 36
|
|
393 |
\item {\tt Pair_inject2} theorem, 36
|
|
394 |
\item {\tt Pair_neq_0} theorem, 36
|
|
395 |
\item {\tt pairing} theorem, 33
|
|
396 |
\item {\tt Perm} theory, 42
|
|
397 |
\item {\tt Pi} constant, 24, 27, 39
|
|
398 |
\item {\tt Pi_def} theorem, 29
|
|
399 |
\item {\tt Pi_type} theorem, 38, 39
|
|
400 |
\item {\tt Pow} constant, 24
|
|
401 |
\item {\tt Pow_iff} theorem, 28
|
|
402 |
\item {\tt Pow_mono} theorem, 65
|
|
403 |
\item {\tt PowD} theorem, 31, 66
|
|
404 |
\item {\tt PowI} theorem, 31, 66
|
|
405 |
\item {\tt primrec}, 55--57
|
|
406 |
\item {\tt PrimReplace} constant, 24, 30
|
|
407 |
\item priorities, 1
|
|
408 |
\item {\tt PROD} symbol, 25, 27
|
|
409 |
\item {\tt prop_cs}, \bold{9}
|
|
410 |
|
|
411 |
\indexspace
|
|
412 |
|
|
413 |
\item {\tt qcase_def} theorem, 42
|
|
414 |
\item {\tt qconverse} constant, 39
|
|
415 |
\item {\tt qconverse_def} theorem, 42
|
|
416 |
\item {\tt qed_spec_mp}, 54
|
|
417 |
\item {\tt qfsplit_def} theorem, 42
|
|
418 |
\item {\tt QInl_def} theorem, 42
|
|
419 |
\item {\tt QInr_def} theorem, 42
|
|
420 |
\item {\tt QPair} theory, 39
|
|
421 |
\item {\tt QPair_def} theorem, 42
|
|
422 |
\item {\tt QSigma} constant, 39
|
|
423 |
\item {\tt QSigma_def} theorem, 42
|
|
424 |
\item {\tt qsplit} constant, 39
|
|
425 |
\item {\tt qsplit_def} theorem, 42
|
|
426 |
\item {\tt qsum_def} theorem, 42
|
|
427 |
\item {\tt QUniv} theory, 46
|
|
428 |
|
|
429 |
\indexspace
|
|
430 |
|
|
431 |
\item {\tt range} constant, 24
|
|
432 |
\item {\tt range_def} theorem, 29
|
|
433 |
\item {\tt range_of_fun} theorem, 38, 39
|
|
434 |
\item {\tt range_subset} theorem, 37
|
|
435 |
\item {\tt range_type} theorem, 38
|
|
436 |
\item {\tt rangeE} theorem, 37
|
|
437 |
\item {\tt rangeI} theorem, 37
|
|
438 |
\item {\tt rank} constant, 62
|
|
439 |
\item recursion
|
|
440 |
\subitem primitive, 57
|
|
441 |
\item recursive functions, \see{recursion}{55}
|
|
442 |
\item {\tt refl} theorem, 6
|
|
443 |
\item {\tt RepFun} constant, 24, 27, 30, 32
|
|
444 |
\item {\tt RepFun_def} theorem, 28
|
|
445 |
\item {\tt RepFunE} theorem, 33
|
|
446 |
\item {\tt RepFunI} theorem, 33
|
|
447 |
\item {\tt Replace} constant, 24, 25, 30, 32
|
|
448 |
\item {\tt Replace_def} theorem, 28
|
|
449 |
\item {\tt ReplaceE} theorem, 33
|
|
450 |
\item {\tt ReplaceI} theorem, 33
|
|
451 |
\item {\tt replacement} theorem, 28
|
|
452 |
\item {\tt restrict} constant, 24, 30
|
|
453 |
\item {\tt restrict} theorem, 38
|
|
454 |
\item {\tt restrict_bij} theorem, 44
|
|
455 |
\item {\tt restrict_def} theorem, 29
|
|
456 |
\item {\tt restrict_type} theorem, 38
|
|
457 |
\item {\tt rev} constant, 47
|
|
458 |
\item {\tt rew_tac}, 17
|
|
459 |
\item {\tt rewrite_rule}, 17
|
|
460 |
\item {\tt right_comp_id} theorem, 44
|
|
461 |
\item {\tt right_comp_inverse} theorem, 44
|
|
462 |
\item {\tt right_inverse} theorem, 44
|
|
463 |
|
|
464 |
\indexspace
|
|
465 |
|
|
466 |
\item {\tt separation} theorem, 33
|
|
467 |
\item set theory, 22--70
|
|
468 |
\item {\tt Sigma} constant, 24, 27, 30, 36
|
|
469 |
\item {\tt Sigma_def} theorem, 29
|
|
470 |
\item {\tt SigmaE} theorem, 36
|
|
471 |
\item {\tt SigmaE2} theorem, 36
|
|
472 |
\item {\tt SigmaI} theorem, 36
|
|
473 |
\item simplification
|
|
474 |
\subitem of conjunctions, 4
|
|
475 |
\item {\tt singletonE} theorem, 34
|
|
476 |
\item {\tt singletonI} theorem, 34
|
|
477 |
\item {\tt snd} constant, 24, 30
|
|
478 |
\item {\tt snd_conv} theorem, 36
|
|
479 |
\item {\tt snd_def} theorem, 29
|
|
480 |
\item {\tt spec} theorem, 6
|
|
481 |
\item {\tt split} constant, 24, 30
|
|
482 |
\item {\tt split} theorem, 36
|
|
483 |
\item {\tt split_def} theorem, 29
|
|
484 |
\item {\tt ssubst} theorem, 7
|
|
485 |
\item {\tt Step_tac}, 20
|
|
486 |
\item {\tt step_tac}, 21
|
|
487 |
\item {\tt subset_def} theorem, 28
|
|
488 |
\item {\tt subset_refl} theorem, 31
|
|
489 |
\item {\tt subset_trans} theorem, 31
|
|
490 |
\item {\tt subsetCE} theorem, 31
|
|
491 |
\item {\tt subsetD} theorem, 31, 68
|
|
492 |
\item {\tt subsetI} theorem, 31, 66, 67
|
|
493 |
\item {\tt subst} theorem, 6
|
|
494 |
\item {\tt succ} constant, 24, 30
|
|
495 |
\item {\tt succ_def} theorem, 29
|
|
496 |
\item {\tt succ_inject} theorem, 34
|
|
497 |
\item {\tt succ_neq_0} theorem, 34
|
|
498 |
\item {\tt succCI} theorem, 34
|
|
499 |
\item {\tt succE} theorem, 34
|
|
500 |
\item {\tt succI1} theorem, 34
|
|
501 |
\item {\tt succI2} theorem, 34
|
|
502 |
\item {\tt SUM} symbol, 25, 27
|
|
503 |
\item {\tt Sum} theory, 39
|
|
504 |
\item {\tt sum_def} theorem, 41
|
|
505 |
\item {\tt sum_InlI} theorem, 41
|
|
506 |
\item {\tt sum_InrI} theorem, 41
|
|
507 |
\item {\tt SUM_Int_distrib1} theorem, 40
|
|
508 |
\item {\tt SUM_Int_distrib2} theorem, 40
|
|
509 |
\item {\tt SUM_Un_distrib1} theorem, 40
|
|
510 |
\item {\tt SUM_Un_distrib2} theorem, 40
|
|
511 |
\item {\tt sumE2} theorem, 41
|
|
512 |
\item {\tt surj} constant, 44
|
|
513 |
\item {\tt surj_def} theorem, 44
|
|
514 |
\item {\tt swap} theorem, 9
|
|
515 |
\item {\tt swap_res_tac}, 14
|
|
516 |
\item {\tt sym} theorem, 7
|
|
517 |
|
|
518 |
\indexspace
|
|
519 |
|
|
520 |
\item {\tt term} class, 3
|
|
521 |
\item {\tt THE} symbol, 25, 27, 35
|
|
522 |
\item {\tt The} constant, 24, 27, 30
|
|
523 |
\item {\tt the_def} theorem, 28
|
|
524 |
\item {\tt the_equality} theorem, 34, 35
|
|
525 |
\item {\tt theI} theorem, 34, 35
|
|
526 |
\item {\tt trace_induct}, \bold{59}
|
|
527 |
\item {\tt trans} theorem, 7
|
|
528 |
\item {\tt True} constant, 5
|
|
529 |
\item {\tt True_def} theorem, 6
|
|
530 |
\item {\tt TrueI} theorem, 7
|
|
531 |
\item {\tt Trueprop} constant, 5
|
|
532 |
|
|
533 |
\indexspace
|
|
534 |
|
|
535 |
\item {\tt UN} symbol, 25, 27
|
|
536 |
\item {\tt Un} symbol, 24
|
|
537 |
\item {\tt Un_absorb} theorem, 40
|
|
538 |
\item {\tt Un_assoc} theorem, 40
|
|
539 |
\item {\tt Un_commute} theorem, 40
|
|
540 |
\item {\tt Un_def} theorem, 28
|
|
541 |
\item {\tt UN_E} theorem, 33
|
|
542 |
\item {\tt UN_I} theorem, 33
|
|
543 |
\item {\tt Un_Int_distrib} theorem, 40
|
|
544 |
\item {\tt Un_Inter_RepFun} theorem, 40
|
|
545 |
\item {\tt Un_least} theorem, 35
|
|
546 |
\item {\tt Un_upper1} theorem, 35
|
|
547 |
\item {\tt Un_upper2} theorem, 35
|
|
548 |
\item {\tt UnCI} theorem, 32, 34
|
|
549 |
\item {\tt UnE} theorem, 34
|
|
550 |
\item {\tt UnI1} theorem, 32, 34, 69
|
|
551 |
\item {\tt UnI2} theorem, 32, 34
|
|
552 |
\item {\tt Union} constant, 24
|
|
553 |
\item {\tt Union_iff} theorem, 28
|
|
554 |
\item {\tt Union_least} theorem, 35
|
|
555 |
\item {\tt Union_Un_distrib} theorem, 40
|
|
556 |
\item {\tt Union_upper} theorem, 35
|
|
557 |
\item {\tt UnionE} theorem, 33, 67
|
|
558 |
\item {\tt UnionI} theorem, 33, 67
|
|
559 |
\item {\tt Univ} theory, 42
|
|
560 |
\item {\tt Upair} constant, 23, 24, 30
|
|
561 |
\item {\tt Upair_def} theorem, 28
|
|
562 |
\item {\tt UpairE} theorem, 33
|
|
563 |
\item {\tt UpairI1} theorem, 33
|
|
564 |
\item {\tt UpairI2} theorem, 33
|
|
565 |
|
|
566 |
\indexspace
|
|
567 |
|
|
568 |
\item {\tt vimage_def} theorem, 29
|
|
569 |
\item {\tt vimageE} theorem, 37
|
|
570 |
\item {\tt vimageI} theorem, 37
|
|
571 |
|
|
572 |
\indexspace
|
|
573 |
|
|
574 |
\item {\tt xor_def} theorem, 41
|
|
575 |
|
|
576 |
\indexspace
|
|
577 |
|
|
578 |
\item {\tt ZF} theory, 22
|
|
579 |
\item {\tt ZF_cs}, \bold{48}
|
|
580 |
\item {\tt ZF_ss}, \bold{46}
|
|
581 |
|
|
582 |
\end{theindex}
|