1 \begin{theindex} |
1 \begin{theindex} |
2 |
2 |
3 \item {\tt !} symbol, 60, 62, 69, 70, 82 |
3 \item {\tt !} symbol, 6, 8, 15, 16, 28 |
4 \item {\tt[]} symbol, 82 |
4 \item {\tt[]} symbol, 28 |
5 \item {\tt\#} symbol, 82 |
5 \item {\tt\#} symbol, 28 |
6 \item {\tt\#*} symbol, 48, 137 |
6 \item {\tt\#*} symbol, 84 |
7 \item {\tt\#+} symbol, 48, 137 |
7 \item {\tt\#+} symbol, 84 |
8 \item {\tt\#-} symbol, 48 |
8 \item {\tt\&} symbol, 6, 60 |
9 \item {\tt\&} symbol, 7, 60, 114 |
9 \item {\tt *} symbol, 7, 25, 75 |
10 \item {\tt *} symbol, 27, 61, 79, 128 |
10 \item {\tt *} type, 23 |
11 \item {\tt *} type, 77 |
11 \item {\tt +} symbol, 7, 25, 75 |
12 \item {\tt +} symbol, 44, 61, 79, 128 |
12 \item {\tt +} type, 23 |
13 \item {\tt +} type, 77 |
13 \item {\tt -} symbol, 7, 25, 84 |
14 \item {\tt -} symbol, 26, 61, 79, 137 |
14 \item {\tt -->} symbol, 6, 60, 75 |
15 \item {\tt -->} symbol, 7, 60, 114, 128 |
15 \item {\tt :} symbol, 14 |
16 \item {\tt ->} symbol, 27 |
16 \item {\tt <} constant, 26 |
17 \item {\tt -``} symbol, 26 |
17 \item {\tt <} symbol, 25 |
18 \item {\tt :} symbol, 26, 68 |
18 \item {\tt <->} symbol, 60 |
19 \item {\tt <} constant, 80 |
19 \item {\tt <=} constant, 26 |
20 \item {\tt <} symbol, 79 |
20 \item {\tt <=} symbol, 14 |
21 \item {\tt <->} symbol, 7, 114 |
21 \item {\tt =} symbol, 6, 60, 75 |
22 \item {\tt <=} constant, 80 |
22 \item {\tt ?} symbol, 6, 8, 15, 16 |
23 \item {\tt <=} symbol, 26, 68 |
23 \item {\tt ?!} symbol, 6 |
24 \item {\tt =} symbol, 7, 60, 114, 128 |
24 \item {\tt\at} symbol, 6, 28 |
25 \item {\tt ?} symbol, 60, 62, 69, 70 |
25 \item {\tt `} symbol, 75 |
26 \item {\tt ?!} symbol, 60 |
26 \item {\tt ``} symbol, 14 |
27 \item {\tt\at} symbol, 60, 82 |
27 \item \verb'{}' symbol, 14 |
28 \item {\tt `} symbol, 26, 128 |
28 \item {\tt |} symbol, 6, 60 |
29 \item {\tt ``} symbol, 26, 68 |
29 \item {\tt |-|} symbol, 84 |
30 \item \verb'{}' symbol, 68 |
30 |
31 \item {\tt |} symbol, 7, 60, 114 |
31 \indexspace |
32 \item {\tt |-|} symbol, 137 |
32 |
33 |
33 \item {\tt 0} constant, 25, 73 |
34 \indexspace |
34 |
35 |
35 \indexspace |
36 \item {\tt 0} constant, 26, 79, 126 |
36 |
37 |
37 \item {\tt absdiff_def} theorem, 84 |
38 \indexspace |
38 \item {\tt add_assoc} theorem, 84 |
39 |
39 \item {\tt add_commute} theorem, 84 |
40 \item {\tt absdiff_def} theorem, 137 |
40 \item {\tt add_def} theorem, 84 |
41 \item {\tt add_assoc} theorem, 137 |
41 \item {\tt add_inverse_diff} theorem, 84 |
42 \item {\tt add_commute} theorem, 137 |
42 \item {\tt add_mp_tac}, \bold{82} |
43 \item {\tt add_def} theorem, 48, 137 |
43 \item {\tt add_mult_dist} theorem, 84 |
44 \item {\tt add_inverse_diff} theorem, 137 |
44 \item {\tt add_safes}, \bold{66} |
45 \item {\tt add_mp_tac}, \bold{135} |
45 \item {\tt add_typing} theorem, 84 |
46 \item {\tt add_mult_dist} theorem, 48, 137 |
46 \item {\tt add_unsafes}, \bold{66} |
47 \item {\tt add_safes}, \bold{120} |
47 \item {\tt addC0} theorem, 84 |
48 \item {\tt add_typing} theorem, 137 |
48 \item {\tt addC_succ} theorem, 84 |
49 \item {\tt add_unsafes}, \bold{120} |
49 \item {\tt Addsplits}, \bold{22} |
50 \item {\tt addC0} theorem, 137 |
50 \item {\tt addsplits}, \bold{22}, 27, 39 |
51 \item {\tt addC_succ} theorem, 137 |
51 \item {\tt ALL} symbol, 6, 8, 15, 16, 60 |
52 \item {\tt Addsplits}, \bold{76} |
52 \item {\tt All} constant, 6, 60 |
53 \item {\tt addsplits}, \bold{76}, 81, 93 |
53 \item {\tt All_def} theorem, 10 |
54 \item {\tt ALL} symbol, 7, 27, 60, 62, 69, 70, 114 |
54 \item {\tt all_dupE} theorem, 12 |
55 \item {\tt All} constant, 7, 60, 114 |
55 \item {\tt allE} theorem, 12 |
56 \item {\tt All_def} theorem, 64 |
56 \item {\tt allI} theorem, 12 |
57 \item {\tt all_dupE} theorem, 5, 9, 66 |
57 \item {\tt allL} theorem, 62, 66 |
58 \item {\tt all_impE} theorem, 9 |
58 \item {\tt allL_thin} theorem, 63 |
59 \item {\tt allE} theorem, 5, 9, 66 |
59 \item {\tt allR} theorem, 62 |
60 \item {\tt allI} theorem, 8, 66 |
60 \item {\tt and_def} theorem, 10 |
61 \item {\tt allL} theorem, 116, 120 |
61 \item {\tt arg_cong} theorem, 11 |
62 \item {\tt allL_thin} theorem, 117 |
62 \item {\tt Arith} theory, 26, 83 |
63 \item {\tt allR} theorem, 116 |
|
64 \item {\tt and_def} theorem, 43, 64 |
|
65 \item {\tt app_def} theorem, 50 |
|
66 \item {\tt apply_def} theorem, 32 |
|
67 \item {\tt apply_equality} theorem, 40, 41, 57, 58 |
|
68 \item {\tt apply_equality2} theorem, 40 |
|
69 \item {\tt apply_iff} theorem, 40 |
|
70 \item {\tt apply_Pair} theorem, 40, 58 |
|
71 \item {\tt apply_type} theorem, 40 |
|
72 \item {\tt arg_cong} theorem, 65 |
|
73 \item {\tt Arith} theory, 47, 80, 136 |
|
74 \item assumptions |
63 \item assumptions |
75 \subitem contradictory, 16 |
64 \subitem in {\CTT}, 72, 82 |
76 \subitem in {\CTT}, 125, 135 |
65 |
77 |
66 \indexspace |
78 \indexspace |
67 |
79 |
68 \item {\tt Ball} constant, 14, 16 |
80 \item {\tt Ball} constant, 26, 30, 68, 70 |
69 \item {\tt Ball_def} theorem, 17 |
81 \item {\tt ball_cong} theorem, 33, 34 |
70 \item {\tt ballE} theorem, 18 |
82 \item {\tt Ball_def} theorem, 31, 71 |
71 \item {\tt ballI} theorem, 18 |
83 \item {\tt ballE} theorem, 33, 34, 72 |
72 \item {\tt basic} theorem, 62 |
84 \item {\tt ballI} theorem, 34, 72 |
73 \item {\tt basic_defs}, \bold{80} |
85 \item {\tt basic} theorem, 116 |
74 \item {\tt best_tac}, \bold{67} |
86 \item {\tt basic_defs}, \bold{133} |
75 \item {\tt Bex} constant, 14, 16 |
87 \item {\tt best_tac}, \bold{121} |
76 \item {\tt Bex_def} theorem, 17 |
88 \item {\tt beta} theorem, 40, 41 |
77 \item {\tt bexCI} theorem, 16, 18 |
89 \item {\tt Bex} constant, 26, 30, 68, 70 |
78 \item {\tt bexE} theorem, 18 |
90 \item {\tt bex_cong} theorem, 33, 34 |
79 \item {\tt bexI} theorem, 16, 18 |
91 \item {\tt Bex_def} theorem, 31, 71 |
80 \item {\textit {bool}} type, 7 |
92 \item {\tt bexCI} theorem, 34, 70, 72 |
81 \item {\tt box_equals} theorem, 11, 13 |
93 \item {\tt bexE} theorem, 34, 72 |
82 \item {\tt bspec} theorem, 18 |
94 \item {\tt bexI} theorem, 34, 70, 72 |
83 \item {\tt butlast} constant, 28 |
95 \item {\tt bij} constant, 46 |
84 |
96 \item {\tt bij_converse_bij} theorem, 46 |
85 \indexspace |
97 \item {\tt bij_def} theorem, 46 |
86 |
98 \item {\tt bij_disjoint_Un} theorem, 46 |
87 \item {\tt case} symbol, 9, 26, 27, 39 |
99 \item {\tt Blast_tac}, 17, 55, 56 |
88 \item {\tt case_tac}, \bold{13} |
100 \item {\tt blast_tac}, 18, 19, 21 |
|
101 \item {\tt bnd_mono_def} theorem, 45 |
|
102 \item {\tt Bool} theory, 41 |
|
103 \item {\textit {bool}} type, 61 |
|
104 \item {\tt bool_0I} theorem, 43 |
|
105 \item {\tt bool_1I} theorem, 43 |
|
106 \item {\tt bool_def} theorem, 43 |
|
107 \item {\tt boolE} theorem, 43 |
|
108 \item {\tt box_equals} theorem, 65, 67 |
|
109 \item {\tt bspec} theorem, 34, 72 |
|
110 \item {\tt butlast} constant, 82 |
|
111 |
|
112 \indexspace |
|
113 |
|
114 \item {\tt case} constant, 44 |
|
115 \item {\tt case} symbol, 63, 80, 81, 93 |
|
116 \item {\tt case_def} theorem, 44 |
|
117 \item {\tt case_Inl} theorem, 44 |
|
118 \item {\tt case_Inr} theorem, 44 |
|
119 \item {\tt case_tac}, \bold{67} |
|
120 \item {\tt CCL} theory, 1 |
89 \item {\tt CCL} theory, 1 |
121 \item {\tt ccontr} theorem, 66 |
90 \item {\tt ccontr} theorem, 12 |
122 \item {\tt classical} theorem, 66 |
91 \item {\tt classical} theorem, 12 |
123 \item {\tt coinduct} theorem, 45 |
92 \item {\tt coinductive}, 51--54 |
124 \item {\tt coinductive}, 105--108 |
93 \item {\tt Collect} constant, 14, 16 |
125 \item {\tt Collect} constant, 26, 27, 30, 68, 70 |
94 \item {\tt Collect_mem_eq} theorem, 16, 17 |
126 \item {\tt Collect_def} theorem, 31 |
95 \item {\tt CollectD} theorem, 18, 57 |
127 \item {\tt Collect_mem_eq} theorem, 70, 71 |
96 \item {\tt CollectE} theorem, 18 |
128 \item {\tt Collect_subset} theorem, 37 |
97 \item {\tt CollectI} theorem, 18, 57 |
129 \item {\tt CollectD} theorem, 72, 111 |
98 \item {\tt comp_rls}, \bold{80} |
130 \item {\tt CollectD1} theorem, 33, 35 |
99 \item {\tt Compl} constant, 14 |
131 \item {\tt CollectD2} theorem, 33, 35 |
100 \item {\tt Compl_def} theorem, 17 |
132 \item {\tt CollectE} theorem, 33, 35, 72 |
101 \item {\tt Compl_disjoint} theorem, 20 |
133 \item {\tt CollectI} theorem, 35, 72, 111 |
102 \item {\tt Compl_Int} theorem, 20 |
134 \item {\tt comp_assoc} theorem, 46 |
103 \item {\tt Compl_partition} theorem, 20 |
135 \item {\tt comp_bij} theorem, 46 |
104 \item {\tt Compl_Un} theorem, 20 |
136 \item {\tt comp_def} theorem, 46 |
105 \item {\tt ComplD} theorem, 19 |
137 \item {\tt comp_func} theorem, 46 |
106 \item {\tt ComplI} theorem, 19 |
138 \item {\tt comp_func_apply} theorem, 46 |
107 \item {\tt concat} constant, 28 |
139 \item {\tt comp_inj} theorem, 46 |
108 \item {\tt cong} theorem, 11 |
140 \item {\tt comp_rls}, \bold{133} |
109 \item {\tt conj_cong}, 21 |
141 \item {\tt comp_surj} theorem, 46 |
110 \item {\tt conjE} theorem, 11 |
142 \item {\tt comp_type} theorem, 46 |
111 \item {\tt conjI} theorem, 11 |
143 \item {\tt Compl} constant, 68 |
112 \item {\tt conjL} theorem, 62 |
144 \item {\tt Compl_def} theorem, 71 |
113 \item {\tt conjR} theorem, 62 |
145 \item {\tt Compl_disjoint} theorem, 74 |
114 \item {\tt conjunct1} theorem, 11 |
146 \item {\tt Compl_Int} theorem, 74 |
115 \item {\tt conjunct2} theorem, 11 |
147 \item {\tt Compl_partition} theorem, 74 |
116 \item {\tt conL} theorem, 63 |
148 \item {\tt Compl_Un} theorem, 74 |
117 \item {\tt conR} theorem, 63 |
149 \item {\tt ComplD} theorem, 73 |
118 \item Constructive Type Theory, 72--94 |
150 \item {\tt ComplI} theorem, 73 |
119 \item {\tt contr} constant, 73 |
151 \item {\tt concat} constant, 82 |
120 \item {\tt could_res}, \bold{65} |
152 \item {\tt cond_0} theorem, 43 |
121 \item {\tt could_resolve_seq}, \bold{65} |
153 \item {\tt cond_1} theorem, 43 |
122 \item {\tt CTT} theory, 1, 72 |
154 \item {\tt cond_def} theorem, 43 |
|
155 \item {\tt cong} theorem, 65 |
|
156 \item congruence rules, 33 |
|
157 \item {\tt conj_cong}, 6, 75 |
|
158 \item {\tt conj_impE} theorem, 9, 10 |
|
159 \item {\tt conjE} theorem, 9, 65 |
|
160 \item {\tt conjI} theorem, 8, 65 |
|
161 \item {\tt conjL} theorem, 116 |
|
162 \item {\tt conjR} theorem, 116 |
|
163 \item {\tt conjunct1} theorem, 8, 65 |
|
164 \item {\tt conjunct2} theorem, 8, 65 |
|
165 \item {\tt conL} theorem, 117 |
|
166 \item {\tt conR} theorem, 117 |
|
167 \item {\tt cons} constant, 26, 27 |
|
168 \item {\tt cons_def} theorem, 32 |
|
169 \item {\tt Cons_iff} theorem, 50 |
|
170 \item {\tt consCI} theorem, 36 |
|
171 \item {\tt consE} theorem, 36 |
|
172 \item {\tt ConsI} theorem, 50 |
|
173 \item {\tt consI1} theorem, 36 |
|
174 \item {\tt consI2} theorem, 36 |
|
175 \item Constructive Type Theory, 125--147 |
|
176 \item {\tt contr} constant, 126 |
|
177 \item {\tt converse} constant, 26, 40 |
|
178 \item {\tt converse_def} theorem, 32 |
|
179 \item {\tt could_res}, \bold{119} |
|
180 \item {\tt could_resolve_seq}, \bold{119} |
|
181 \item {\tt CTT} theory, 1, 125 |
|
182 \item {\tt Cube} theory, 1 |
123 \item {\tt Cube} theory, 1 |
183 \item {\tt cut} theorem, 116 |
124 \item {\tt cut} theorem, 62 |
184 \item {\tt cut_facts_tac}, 19 |
125 \item {\tt cutL_tac}, \bold{64} |
185 \item {\tt cutL_tac}, \bold{118} |
126 \item {\tt cutR_tac}, \bold{64} |
186 \item {\tt cutR_tac}, \bold{118} |
127 |
187 |
128 \indexspace |
188 \indexspace |
129 |
189 |
130 \item {\tt datatype}, 36--44 |
190 \item {\tt datatype}, 90--98 |
131 \item {\tt Delsplits}, \bold{22} |
191 \item {\tt Delsplits}, \bold{76} |
132 \item {\tt delsplits}, \bold{22} |
192 \item {\tt delsplits}, \bold{76} |
133 \item {\tt diff_0_eq_0} theorem, 84 |
193 \item {\tt diff_0_eq_0} theorem, 137 |
134 \item {\tt diff_def} theorem, 84 |
194 \item {\tt Diff_cancel} theorem, 42 |
135 \item {\tt diff_self_eq_0} theorem, 84 |
195 \item {\tt Diff_contains} theorem, 37 |
136 \item {\tt diff_succ_succ} theorem, 84 |
196 \item {\tt Diff_def} theorem, 31 |
137 \item {\tt diff_typing} theorem, 84 |
197 \item {\tt diff_def} theorem, 48, 137 |
138 \item {\tt diffC0} theorem, 84 |
198 \item {\tt Diff_disjoint} theorem, 42 |
139 \item {\tt disjCI} theorem, 12 |
199 \item {\tt Diff_Int} theorem, 42 |
140 \item {\tt disjE} theorem, 11 |
200 \item {\tt Diff_partition} theorem, 42 |
141 \item {\tt disjI1} theorem, 11 |
201 \item {\tt diff_self_eq_0} theorem, 137 |
142 \item {\tt disjI2} theorem, 11 |
202 \item {\tt Diff_subset} theorem, 37 |
143 \item {\tt disjL} theorem, 62 |
203 \item {\tt diff_succ_succ} theorem, 137 |
144 \item {\tt disjR} theorem, 62 |
204 \item {\tt diff_typing} theorem, 137 |
145 \item {\tt div} symbol, 25, 84 |
205 \item {\tt Diff_Un} theorem, 42 |
146 \item {\tt div_def} theorem, 84 |
206 \item {\tt diffC0} theorem, 137 |
147 \item {\tt div_geq} theorem, 26 |
207 \item {\tt DiffD1} theorem, 36 |
148 \item {\tt div_less} theorem, 26 |
208 \item {\tt DiffD2} theorem, 36 |
149 \item {\tt Divides} theory, 26 |
209 \item {\tt DiffE} theorem, 36 |
150 \item {\tt double_complement} theorem, 20 |
210 \item {\tt DiffI} theorem, 36 |
151 \item {\tt drop} constant, 28 |
211 \item {\tt disj_impE} theorem, 9, 10, 14 |
152 \item {\tt dropWhile} constant, 28 |
212 \item {\tt disjCI} theorem, 11, 66 |
153 |
213 \item {\tt disjE} theorem, 8, 65 |
154 \indexspace |
214 \item {\tt disjI1} theorem, 8, 65 |
155 |
215 \item {\tt disjI2} theorem, 8, 65 |
156 \item {\tt Elem} constant, 73 |
216 \item {\tt disjL} theorem, 116 |
157 \item {\tt elim_rls}, \bold{80} |
217 \item {\tt disjR} theorem, 116 |
158 \item {\tt elimL_rls}, \bold{80} |
218 \item {\tt div} symbol, 48, 79, 137 |
159 \item {\tt empty_def} theorem, 17 |
219 \item {\tt div_def} theorem, 48, 137 |
160 \item {\tt empty_pack}, \bold{66} |
220 \item {\tt div_geq} theorem, 80 |
161 \item {\tt emptyE} theorem, 19 |
221 \item {\tt div_less} theorem, 80 |
162 \item {\tt Eps} constant, 6, 8 |
222 \item {\tt Divides} theory, 80 |
163 \item {\tt Eq} constant, 73 |
223 \item {\tt domain} constant, 26, 40 |
164 \item {\tt eq} constant, 73, 78 |
224 \item {\tt domain_def} theorem, 32 |
165 \item {\tt EqC} theorem, 79 |
225 \item {\tt domain_of_fun} theorem, 40 |
166 \item {\tt EqE} theorem, 79 |
226 \item {\tt domain_subset} theorem, 39 |
167 \item {\tt Eqelem} constant, 73 |
227 \item {\tt domain_type} theorem, 40 |
168 \item {\tt EqF} theorem, 79 |
228 \item {\tt domainE} theorem, 39, 40 |
169 \item {\tt EqFL} theorem, 79 |
229 \item {\tt domainI} theorem, 39, 40 |
170 \item {\tt EqI} theorem, 79 |
230 \item {\tt double_complement} theorem, 42, 74 |
171 \item {\tt Eqtype} constant, 73 |
231 \item {\tt dresolve_tac}, 54 |
172 \item {\tt equal_tac}, \bold{81} |
232 \item {\tt drop} constant, 82 |
173 \item {\tt equal_types} theorem, 76 |
233 \item {\tt dropWhile} constant, 82 |
174 \item {\tt equal_typesL} theorem, 76 |
234 |
175 \item {\tt equalityCE} theorem, 16, 18, 57, 58 |
235 \indexspace |
176 \item {\tt equalityD1} theorem, 18 |
236 |
177 \item {\tt equalityD2} theorem, 18 |
237 \item {\tt Elem} constant, 126 |
178 \item {\tt equalityE} theorem, 18 |
238 \item {\tt elim_rls}, \bold{133} |
179 \item {\tt equalityI} theorem, 18 |
239 \item {\tt elimL_rls}, \bold{133} |
180 \item {\tt EX} symbol, 6, 8, 15, 16, 60 |
240 \item {\tt empty_def} theorem, 71 |
181 \item {\tt Ex} constant, 6, 60 |
241 \item {\tt empty_pack}, \bold{119} |
182 \item {\tt EX!} symbol, 6 |
242 \item {\tt empty_subsetI} theorem, 34 |
183 \item {\tt Ex1} constant, 6 |
243 \item {\tt emptyE} theorem, 34, 73 |
184 \item {\tt Ex1_def} theorem, 10 |
244 \item {\tt Eps} constant, 60, 62 |
185 \item {\tt ex1E} theorem, 12 |
245 \item {\tt Eq} constant, 126 |
186 \item {\tt ex1I} theorem, 12 |
246 \item {\tt eq} constant, 126, 131 |
187 \item {\tt Ex_def} theorem, 10 |
247 \item {\tt eq_mp_tac}, \bold{10} |
188 \item {\tt exCI} theorem, 12 |
248 \item {\tt EqC} theorem, 132 |
189 \item {\tt excluded_middle} theorem, 12 |
249 \item {\tt EqE} theorem, 132 |
190 \item {\tt exE} theorem, 12 |
250 \item {\tt Eqelem} constant, 126 |
191 \item {\tt exhaust_tac}, \bold{40} |
251 \item {\tt EqF} theorem, 132 |
192 \item {\tt exI} theorem, 12 |
252 \item {\tt EqFL} theorem, 132 |
193 \item {\tt exL} theorem, 62 |
253 \item {\tt EqI} theorem, 132 |
194 \item {\tt Exp} theory, 55 |
254 \item {\tt Eqtype} constant, 126 |
195 \item {\tt exR} theorem, 62, 66, 68 |
255 \item {\tt equal_tac}, \bold{134} |
196 \item {\tt exR_thin} theorem, 63, 68, 69 |
256 \item {\tt equal_types} theorem, 129 |
197 \item {\tt ext} theorem, 9, 10 |
257 \item {\tt equal_typesL} theorem, 129 |
198 |
258 \item {\tt equalityCE} theorem, 70, 72, 111, 112 |
199 \indexspace |
259 \item {\tt equalityD1} theorem, 34, 72 |
200 |
260 \item {\tt equalityD2} theorem, 34, 72 |
201 \item {\tt F} constant, 73 |
261 \item {\tt equalityE} theorem, 34, 72 |
202 \item {\tt False} constant, 6, 60 |
262 \item {\tt equalityI} theorem, 34, 53, 72 |
203 \item {\tt False_def} theorem, 10 |
263 \item {\tt equals0D} theorem, 34 |
204 \item {\tt FalseE} theorem, 11 |
264 \item {\tt equals0I} theorem, 34 |
205 \item {\tt FalseL} theorem, 62 |
265 \item {\tt eresolve_tac}, 16 |
206 \item {\tt fast_tac}, \bold{67} |
266 \item {\tt eta} theorem, 40, 41 |
207 \item {\tt FE} theorem, 79, 83 |
267 \item {\tt EX} symbol, 7, 27, 60, 62, 69, 70, 114 |
208 \item {\tt FEL} theorem, 79 |
268 \item {\tt Ex} constant, 7, 60, 114 |
209 \item {\tt FF} theorem, 79 |
269 \item {\tt EX!} symbol, 7, 60 |
210 \item {\tt filseq_resolve_tac}, \bold{65} |
270 \item {\tt Ex1} constant, 7, 60 |
211 \item {\tt filt_resolve_tac}, 65, 81 |
271 \item {\tt Ex1_def} theorem, 64 |
212 \item {\tt filter} constant, 28 |
272 \item {\tt ex1_def} theorem, 8 |
213 \item flex-flex constraints, 61 |
273 \item {\tt ex1E} theorem, 9, 66 |
214 \item {\tt FOL} theory, 82 |
274 \item {\tt ex1I} theorem, 9, 66 |
215 \item {\tt foldl} constant, 28 |
275 \item {\tt Ex_def} theorem, 64 |
216 \item {\tt form_rls}, \bold{80} |
276 \item {\tt ex_impE} theorem, 9 |
217 \item {\tt formL_rls}, \bold{80} |
277 \item {\tt exCI} theorem, 11, 15, 66 |
218 \item {\tt forms_of_seq}, \bold{64} |
278 \item {\tt excluded_middle} theorem, 11, 66 |
219 \item {\tt fst} constant, 23, 73, 78 |
279 \item {\tt exE} theorem, 8, 66 |
220 \item {\tt fst_conv} theorem, 23 |
280 \item {\tt exhaust_tac}, \bold{94} |
221 \item {\tt fst_def} theorem, 78 |
281 \item {\tt exI} theorem, 8, 66 |
222 \item {\tt Fun} theory, 21 |
282 \item {\tt exL} theorem, 116 |
223 \item {\textit {fun}} type, 7 |
283 \item {\tt Exp} theory, 109 |
224 \item {\tt fun_cong} theorem, 11 |
284 \item {\tt exR} theorem, 116, 120, 121 |
|
285 \item {\tt exR_thin} theorem, 117, 121, 122 |
|
286 \item {\tt ext} theorem, 63, 64 |
|
287 \item {\tt extension} theorem, 31 |
|
288 |
|
289 \indexspace |
|
290 |
|
291 \item {\tt F} constant, 126 |
|
292 \item {\tt False} constant, 7, 60, 114 |
|
293 \item {\tt False_def} theorem, 64 |
|
294 \item {\tt FalseE} theorem, 8, 65 |
|
295 \item {\tt FalseL} theorem, 116 |
|
296 \item {\tt fast_tac}, \bold{121} |
|
297 \item {\tt FE} theorem, 132, 136 |
|
298 \item {\tt FEL} theorem, 132 |
|
299 \item {\tt FF} theorem, 132 |
|
300 \item {\tt field} constant, 26 |
|
301 \item {\tt field_def} theorem, 32 |
|
302 \item {\tt field_subset} theorem, 39 |
|
303 \item {\tt fieldCI} theorem, 39 |
|
304 \item {\tt fieldE} theorem, 39 |
|
305 \item {\tt fieldI1} theorem, 39 |
|
306 \item {\tt fieldI2} theorem, 39 |
|
307 \item {\tt filseq_resolve_tac}, \bold{119} |
|
308 \item {\tt filt_resolve_tac}, 119, 134 |
|
309 \item {\tt filter} constant, 82 |
|
310 \item {\tt Fin.consI} theorem, 49 |
|
311 \item {\tt Fin.emptyI} theorem, 49 |
|
312 \item {\tt Fin_induct} theorem, 49 |
|
313 \item {\tt Fin_mono} theorem, 49 |
|
314 \item {\tt Fin_subset} theorem, 49 |
|
315 \item {\tt Fin_UnI} theorem, 49 |
|
316 \item {\tt Fin_UnionI} theorem, 49 |
|
317 \item first-order logic, 5--23 |
|
318 \item {\tt Fixedpt} theory, 43 |
|
319 \item {\tt flat} constant, 50 |
|
320 \item {\tt flat_def} theorem, 50 |
|
321 \item flex-flex constraints, 115 |
|
322 \item {\tt FOL} theory, 1, 5, 11, 135 |
|
323 \item {\tt FOL_cs}, \bold{11} |
|
324 \item {\tt FOL_ss}, \bold{6} |
|
325 \item {\tt foldl} constant, 82 |
|
326 \item {\tt form_rls}, \bold{133} |
|
327 \item {\tt formL_rls}, \bold{133} |
|
328 \item {\tt forms_of_seq}, \bold{118} |
|
329 \item {\tt foundation} theorem, 31 |
|
330 \item {\tt fst} constant, 26, 33, 77, 126, 131 |
|
331 \item {\tt fst_conv} theorem, 38, 77 |
|
332 \item {\tt fst_def} theorem, 32, 131 |
|
333 \item {\tt Fun} theory, 75 |
|
334 \item {\textit {fun}} type, 61 |
|
335 \item {\tt fun_cong} theorem, 65 |
|
336 \item {\tt fun_disjoint_apply1} theorem, 41, 57 |
|
337 \item {\tt fun_disjoint_apply2} theorem, 41 |
|
338 \item {\tt fun_disjoint_Un} theorem, 41, 58 |
|
339 \item {\tt fun_empty} theorem, 41 |
|
340 \item {\tt fun_extension} theorem, 40, 41 |
|
341 \item {\tt fun_is_rel} theorem, 40 |
|
342 \item {\tt fun_single} theorem, 41 |
|
343 \item function applications |
225 \item function applications |
344 \subitem in \CTT, 128 |
226 \subitem in \CTT, 75 |
345 \subitem in \ZF, 26 |
227 |
346 |
228 \indexspace |
347 \indexspace |
229 |
348 |
230 \item {\tt hd} constant, 28 |
349 \item {\tt gfp_def} theorem, 45 |
231 \item higher-order logic, 5--58 |
350 \item {\tt gfp_least} theorem, 45 |
232 \item {\tt HOL} theory, 1, 5 |
351 \item {\tt gfp_mono} theorem, 45 |
233 \item {\sc hol} system, 5, 8 |
352 \item {\tt gfp_subset} theorem, 45 |
234 \item {\tt HOL_basic_ss}, \bold{21} |
353 \item {\tt gfp_Tarski} theorem, 45 |
235 \item {\tt HOL_cs}, \bold{22} |
354 \item {\tt gfp_upperbound} theorem, 45 |
236 \item {\tt HOL_quantifiers}, \bold{8}, 16 |
355 \item {\tt Goalw}, 18, 19 |
237 \item {\tt HOL_ss}, \bold{21} |
356 |
|
357 \indexspace |
|
358 |
|
359 \item {\tt hd} constant, 82 |
|
360 \item higher-order logic, 59--112 |
|
361 \item {\tt HOL} theory, 1, 59 |
|
362 \item {\sc hol} system, 59, 62 |
|
363 \item {\tt HOL_basic_ss}, \bold{75} |
|
364 \item {\tt HOL_cs}, \bold{76} |
|
365 \item {\tt HOL_quantifiers}, \bold{62}, 70 |
|
366 \item {\tt HOL_ss}, \bold{75} |
|
367 \item {\tt HOLCF} theory, 1 |
238 \item {\tt HOLCF} theory, 1 |
368 \item {\tt hyp_rew_tac}, \bold{135} |
239 \item {\tt hyp_rew_tac}, \bold{82} |
369 \item {\tt hyp_subst_tac}, 6, 75 |
240 \item {\tt hyp_subst_tac}, 21 |
370 |
241 |
371 \indexspace |
242 \indexspace |
372 |
243 |
373 \item {\textit {i}} type, 25, 125 |
244 \item {\textit {i}} type, 72 |
374 \item {\tt id} constant, 46 |
245 \item {\tt If} constant, 6 |
375 \item {\tt id_def} theorem, 46 |
246 \item {\tt if_def} theorem, 10 |
376 \item {\tt If} constant, 60 |
247 \item {\tt if_not_P} theorem, 12 |
377 \item {\tt if} constant, 26 |
248 \item {\tt if_P} theorem, 12 |
378 \item {\tt if_def} theorem, 18, 31, 64 |
249 \item {\tt iff} theorem, 9, 10 |
379 \item {\tt if_not_P} theorem, 36, 66 |
250 \item {\tt iff_def} theorem, 62 |
380 \item {\tt if_P} theorem, 36, 66 |
251 \item {\tt iffCE} theorem, 12, 16 |
381 \item {\tt ifE} theorem, 19 |
252 \item {\tt iffD1} theorem, 11 |
382 \item {\tt iff} theorem, 63, 64 |
253 \item {\tt iffD2} theorem, 11 |
383 \item {\tt iff_def} theorem, 8, 116 |
254 \item {\tt iffE} theorem, 11 |
384 \item {\tt iff_impE} theorem, 9 |
255 \item {\tt iffI} theorem, 11 |
385 \item {\tt iffCE} theorem, 11, 66, 70 |
256 \item {\tt iffL} theorem, 63, 70 |
386 \item {\tt iffD1} theorem, 9, 65 |
257 \item {\tt iffR} theorem, 63 |
387 \item {\tt iffD2} theorem, 9, 65 |
258 \item {\tt ILL} theory, 1 |
388 \item {\tt iffE} theorem, 9, 65 |
259 \item {\tt image_def} theorem, 17 |
389 \item {\tt iffI} theorem, 9, 19, 65 |
260 \item {\tt imageE} theorem, 19 |
390 \item {\tt iffL} theorem, 117, 123 |
261 \item {\tt imageI} theorem, 19 |
391 \item {\tt iffR} theorem, 117 |
262 \item {\tt impCE} theorem, 12 |
392 \item {\tt ifI} theorem, 19 |
263 \item {\tt impE} theorem, 11 |
393 \item {\tt IFOL} theory, 5 |
264 \item {\tt impI} theorem, 9 |
394 \item {\tt IFOL_ss}, \bold{6} |
265 \item {\tt impL} theorem, 62 |
395 \item {\tt image_def} theorem, 32, 71 |
266 \item {\tt impR} theorem, 62 |
396 \item {\tt imageE} theorem, 39, 73 |
267 \item {\tt in} symbol, 7 |
397 \item {\tt imageI} theorem, 39, 73 |
268 \item {\textit {ind}} type, 24 |
398 \item {\tt imp_impE} theorem, 9, 14 |
269 \item {\tt induct_tac}, 26, \bold{40} |
399 \item {\tt impCE} theorem, 11, 66 |
270 \item {\tt inductive}, 51--54 |
400 \item {\tt impE} theorem, 9, 10, 65 |
271 \item {\tt inj} constant, 21 |
401 \item {\tt impI} theorem, 8, 63 |
272 \item {\tt inj_def} theorem, 21 |
402 \item {\tt impL} theorem, 116 |
273 \item {\tt inj_Inl} theorem, 25 |
403 \item {\tt impR} theorem, 116 |
274 \item {\tt inj_Inr} theorem, 25 |
404 \item {\tt in} symbol, 28, 61 |
275 \item {\tt inj_on} constant, 21 |
405 \item {\textit {ind}} type, 78 |
276 \item {\tt inj_on_def} theorem, 21 |
406 \item {\tt induct} theorem, 45 |
277 \item {\tt inj_Suc} theorem, 25 |
407 \item {\tt induct_tac}, 80, \bold{94} |
278 \item {\tt Inl} constant, 25 |
408 \item {\tt inductive}, 105--108 |
279 \item {\tt inl} constant, 73, 78, 88 |
409 \item {\tt Inf} constant, 26, 30 |
280 \item {\tt Inl_not_Inr} theorem, 25 |
410 \item {\tt infinity} theorem, 32 |
281 \item {\tt Inr} constant, 25 |
411 \item {\tt inj} constant, 46, 75 |
282 \item {\tt inr} constant, 73, 78 |
412 \item {\tt inj_converse_inj} theorem, 46 |
283 \item {\tt insert} constant, 14 |
413 \item {\tt inj_def} theorem, 46, 75 |
284 \item {\tt insert_def} theorem, 17 |
414 \item {\tt inj_Inl} theorem, 79 |
285 \item {\tt insertE} theorem, 19 |
415 \item {\tt inj_Inr} theorem, 79 |
286 \item {\tt insertI1} theorem, 19 |
416 \item {\tt inj_on} constant, 75 |
287 \item {\tt insertI2} theorem, 19 |
417 \item {\tt inj_on_def} theorem, 75 |
288 \item {\tt INT} symbol, 14--16 |
418 \item {\tt inj_Suc} theorem, 79 |
289 \item {\tt Int} symbol, 14 |
419 \item {\tt Inl} constant, 44, 79 |
290 \item {\tt Int_absorb} theorem, 20 |
420 \item {\tt inl} constant, 126, 131, 141 |
291 \item {\tt Int_assoc} theorem, 20 |
421 \item {\tt Inl_def} theorem, 44 |
292 \item {\tt Int_commute} theorem, 20 |
422 \item {\tt Inl_inject} theorem, 44 |
293 \item {\tt INT_D} theorem, 19 |
423 \item {\tt Inl_neq_Inr} theorem, 44 |
294 \item {\tt Int_def} theorem, 17 |
424 \item {\tt Inl_not_Inr} theorem, 79 |
295 \item {\tt INT_E} theorem, 19 |
425 \item {\tt Inr} constant, 44, 79 |
296 \item {\tt Int_greatest} theorem, 20 |
426 \item {\tt inr} constant, 126, 131 |
297 \item {\tt INT_I} theorem, 19 |
427 \item {\tt Inr_def} theorem, 44 |
298 \item {\tt Int_Inter_image} theorem, 20 |
428 \item {\tt Inr_inject} theorem, 44 |
299 \item {\tt Int_lower1} theorem, 20 |
429 \item {\tt insert} constant, 68 |
300 \item {\tt Int_lower2} theorem, 20 |
430 \item {\tt insert_def} theorem, 71 |
301 \item {\tt Int_Un_distrib} theorem, 20 |
431 \item {\tt insertE} theorem, 73 |
302 \item {\tt Int_Union} theorem, 20 |
432 \item {\tt insertI1} theorem, 73 |
303 \item {\tt IntD1} theorem, 19 |
433 \item {\tt insertI2} theorem, 73 |
304 \item {\tt IntD2} theorem, 19 |
434 \item {\tt INT} symbol, 27, 29, 68--70 |
305 \item {\tt IntE} theorem, 19 |
435 \item {\tt Int} symbol, 26, 68 |
306 \item {\tt INTER} constant, 14 |
436 \item {\tt Int_absorb} theorem, 42, 74 |
307 \item {\tt Inter} constant, 14 |
437 \item {\tt Int_assoc} theorem, 42, 74 |
308 \item {\tt INTER1} constant, 14 |
438 \item {\tt Int_commute} theorem, 42, 74 |
309 \item {\tt INTER1_def} theorem, 17 |
439 \item {\tt INT_D} theorem, 73 |
310 \item {\tt INTER_def} theorem, 17 |
440 \item {\tt Int_def} theorem, 31, 71 |
311 \item {\tt Inter_def} theorem, 17 |
441 \item {\tt INT_E} theorem, 35, 73 |
312 \item {\tt Inter_greatest} theorem, 20 |
442 \item {\tt Int_greatest} theorem, 37, 53, 55, 74 |
313 \item {\tt Inter_lower} theorem, 20 |
443 \item {\tt INT_I} theorem, 35, 73 |
314 \item {\tt Inter_Un_distrib} theorem, 20 |
444 \item {\tt Int_Inter_image} theorem, 74 |
315 \item {\tt InterD} theorem, 19 |
445 \item {\tt Int_lower1} theorem, 37, 54, 74 |
316 \item {\tt InterE} theorem, 19 |
446 \item {\tt Int_lower2} theorem, 37, 54, 74 |
317 \item {\tt InterI} theorem, 19 |
447 \item {\tt Int_Un_distrib} theorem, 42, 74 |
318 \item {\tt IntI} theorem, 19 |
448 \item {\tt Int_Union} theorem, 74 |
319 \item {\tt intr_rls}, \bold{80} |
449 \item {\tt Int_Union_RepFun} theorem, 42 |
320 \item {\tt intr_tac}, \bold{81}, 90, 91 |
450 \item {\tt IntD1} theorem, 36, 73 |
321 \item {\tt intrL_rls}, \bold{80} |
451 \item {\tt IntD2} theorem, 36, 73 |
322 \item {\tt inv} constant, 21 |
452 \item {\tt IntE} theorem, 36, 54, 73 |
323 \item {\tt inv_def} theorem, 21 |
453 \item {\tt INTER} constant, 68 |
324 |
454 \item {\tt Inter} constant, 26, 68 |
325 \indexspace |
455 \item {\tt INTER1} constant, 68 |
326 |
456 \item {\tt INTER1_def} theorem, 71 |
327 \item {\tt lam} symbol, 75 |
457 \item {\tt INTER_def} theorem, 71 |
328 \item {\tt lambda} constant, 73, 75 |
458 \item {\tt Inter_def} theorem, 31, 71 |
|
459 \item {\tt Inter_greatest} theorem, 37, 74 |
|
460 \item {\tt Inter_lower} theorem, 37, 74 |
|
461 \item {\tt Inter_Un_distrib} theorem, 42, 74 |
|
462 \item {\tt InterD} theorem, 35, 73 |
|
463 \item {\tt InterE} theorem, 35, 73 |
|
464 \item {\tt InterI} theorem, 33, 35, 73 |
|
465 \item {\tt IntI} theorem, 36, 73 |
|
466 \item {\tt IntPr.best_tac}, \bold{11} |
|
467 \item {\tt IntPr.fast_tac}, \bold{10}, 13 |
|
468 \item {\tt IntPr.inst_step_tac}, \bold{10} |
|
469 \item {\tt IntPr.safe_step_tac}, \bold{10} |
|
470 \item {\tt IntPr.safe_tac}, \bold{10} |
|
471 \item {\tt IntPr.step_tac}, \bold{10} |
|
472 \item {\tt intr_rls}, \bold{133} |
|
473 \item {\tt intr_tac}, \bold{134}, 143, 144 |
|
474 \item {\tt intrL_rls}, \bold{133} |
|
475 \item {\tt inv} constant, 75 |
|
476 \item {\tt inv_def} theorem, 75 |
|
477 |
|
478 \indexspace |
|
479 |
|
480 \item {\tt lam} symbol, 27, 29, 128 |
|
481 \item {\tt lam_def} theorem, 32 |
|
482 \item {\tt lam_type} theorem, 40 |
|
483 \item {\tt Lambda} constant, 26, 30 |
|
484 \item {\tt lambda} constant, 126, 128 |
|
485 \item $\lambda$-abstractions |
329 \item $\lambda$-abstractions |
486 \subitem in \CTT, 128 |
330 \subitem in \CTT, 75 |
487 \subitem in \ZF, 27 |
331 \item {\tt last} constant, 28 |
488 \item {\tt lamE} theorem, 40, 41 |
|
489 \item {\tt lamI} theorem, 40, 41 |
|
490 \item {\tt last} constant, 82 |
|
491 \item {\tt LCF} theory, 1 |
332 \item {\tt LCF} theory, 1 |
492 \item {\tt le_cs}, \bold{24} |
333 \item {\tt LEAST} constant, 7, 8, 26 |
493 \item {\tt LEAST} constant, 61, 62, 80 |
334 \item {\tt Least} constant, 6 |
494 \item {\tt Least} constant, 60 |
335 \item {\tt Least_def} theorem, 10 |
495 \item {\tt Least_def} theorem, 64 |
336 \item {\tt length} constant, 28 |
496 \item {\tt left_comp_id} theorem, 46 |
337 \item {\tt less_induct} theorem, 27 |
497 \item {\tt left_comp_inverse} theorem, 46 |
338 \item {\tt Let} constant, 6, 9 |
498 \item {\tt left_inverse} theorem, 46 |
339 \item {\tt let} symbol, 7, 9 |
499 \item {\tt length} constant, 50, 82 |
340 \item {\tt Let_def} theorem, 9, 10 |
500 \item {\tt length_def} theorem, 50 |
341 \item {\tt LFilter} theory, 55 |
501 \item {\tt less_induct} theorem, 81 |
342 \item {\tt List} theory, 27, 28 |
502 \item {\tt Let} constant, 25, 26, 60, 63 |
343 \item {\textit{list}} type, 27 |
503 \item {\tt let} symbol, 28, 61, 63 |
344 \item {\tt LK} theory, 1, 59, 63 |
504 \item {\tt Let_def} theorem, 25, 31, 63, 64 |
345 \item {\tt LK_dup_pack}, \bold{66}, 67 |
505 \item {\tt LFilter} theory, 109 |
346 \item {\tt LK_pack}, \bold{66} |
506 \item {\tt lfp_def} theorem, 45 |
347 \item {\tt LList} theory, 55 |
507 \item {\tt lfp_greatest} theorem, 45 |
348 |
508 \item {\tt lfp_lowerbound} theorem, 45 |
349 \indexspace |
509 \item {\tt lfp_mono} theorem, 45 |
350 |
510 \item {\tt lfp_subset} theorem, 45 |
351 \item {\tt map} constant, 28 |
511 \item {\tt lfp_Tarski} theorem, 45 |
352 \item {\tt max} constant, 7, 26 |
512 \item {\tt List} theory, 81, 82 |
353 \item {\tt mem} symbol, 28 |
513 \item {\textit{list}} type, 81 |
354 \item {\tt mem_Collect_eq} theorem, 16, 17 |
514 \item {\tt list} constant, 50 |
355 \item {\tt min} constant, 7, 26 |
515 \item {\tt List.induct} theorem, 50 |
356 \item {\tt minus} class, 7 |
516 \item {\tt list_case} constant, 50 |
357 \item {\tt mod} symbol, 25, 84 |
517 \item {\tt list_mono} theorem, 50 |
358 \item {\tt mod_def} theorem, 84 |
518 \item {\tt list_rec} constant, 50 |
359 \item {\tt mod_geq} theorem, 26 |
519 \item {\tt list_rec_Cons} theorem, 50 |
360 \item {\tt mod_less} theorem, 26 |
520 \item {\tt list_rec_def} theorem, 50 |
|
521 \item {\tt list_rec_Nil} theorem, 50 |
|
522 \item {\tt LK} theory, 1, 113, 117 |
|
523 \item {\tt LK_dup_pack}, \bold{120}, 121 |
|
524 \item {\tt LK_pack}, \bold{120} |
|
525 \item {\tt LList} theory, 109 |
|
526 \item {\tt logic} class, 5 |
|
527 |
|
528 \indexspace |
|
529 |
|
530 \item {\tt map} constant, 50, 82 |
|
531 \item {\tt map_app_distrib} theorem, 50 |
|
532 \item {\tt map_compose} theorem, 50 |
|
533 \item {\tt map_def} theorem, 50 |
|
534 \item {\tt map_flat} theorem, 50 |
|
535 \item {\tt map_ident} theorem, 50 |
|
536 \item {\tt map_type} theorem, 50 |
|
537 \item {\tt max} constant, 61, 80 |
|
538 \item {\tt mem} symbol, 82 |
|
539 \item {\tt mem_asym} theorem, 36, 37 |
|
540 \item {\tt mem_Collect_eq} theorem, 70, 71 |
|
541 \item {\tt mem_irrefl} theorem, 36 |
|
542 \item {\tt min} constant, 61, 80 |
|
543 \item {\tt minus} class, 61 |
|
544 \item {\tt mod} symbol, 48, 79, 137 |
|
545 \item {\tt mod_def} theorem, 48, 137 |
|
546 \item {\tt mod_geq} theorem, 80 |
|
547 \item {\tt mod_less} theorem, 80 |
|
548 \item {\tt mod_quo_equality} theorem, 48 |
|
549 \item {\tt Modal} theory, 1 |
361 \item {\tt Modal} theory, 1 |
550 \item {\tt mono} constant, 61 |
362 \item {\tt mono} constant, 7 |
551 \item {\tt mp} theorem, 8, 63 |
363 \item {\tt mp} theorem, 9 |
552 \item {\tt mp_tac}, \bold{10}, \bold{135} |
364 \item {\tt mp_tac}, \bold{82} |
553 \item {\tt mult_0} theorem, 48 |
365 \item {\tt mult_assoc} theorem, 84 |
554 \item {\tt mult_assoc} theorem, 48, 137 |
366 \item {\tt mult_commute} theorem, 84 |
555 \item {\tt mult_commute} theorem, 48, 137 |
367 \item {\tt mult_def} theorem, 84 |
556 \item {\tt mult_def} theorem, 48, 137 |
368 \item {\tt mult_typing} theorem, 84 |
557 \item {\tt mult_succ} theorem, 48 |
369 \item {\tt multC0} theorem, 84 |
558 \item {\tt mult_type} theorem, 48 |
370 \item {\tt multC_succ} theorem, 84 |
559 \item {\tt mult_typing} theorem, 137 |
371 \item {\tt mutual_induct_tac}, \bold{40} |
560 \item {\tt multC0} theorem, 137 |
372 |
561 \item {\tt multC_succ} theorem, 137 |
373 \indexspace |
562 \item {\tt mutual_induct_tac}, \bold{94} |
374 |
563 |
375 \item {\tt N} constant, 73 |
564 \indexspace |
376 \item {\tt n_not_Suc_n} theorem, 25 |
565 |
377 \item {\tt Nat} theory, 26 |
566 \item {\tt N} constant, 126 |
378 \item {\textit {nat}} type, 25, 26 |
567 \item {\tt n_not_Suc_n} theorem, 79 |
379 \item {\textit{nat}} type, 24--27 |
568 \item {\tt Nat} theory, 47, 80 |
380 \item {\tt nat_induct} theorem, 25 |
569 \item {\textit {nat}} type, 79, 80 |
381 \item {\tt nat_rec} constant, 26 |
570 \item {\textit{nat}} type, 78--81 |
382 \item {\tt NatDef} theory, 24 |
571 \item {\tt nat} constant, 48 |
383 \item {\tt NC0} theorem, 77 |
572 \item {\tt nat_0I} theorem, 48 |
384 \item {\tt NC_succ} theorem, 77 |
573 \item {\tt nat_case} constant, 48 |
385 \item {\tt NE} theorem, 76, 77, 85 |
574 \item {\tt nat_case_0} theorem, 48 |
386 \item {\tt NEL} theorem, 77 |
575 \item {\tt nat_case_def} theorem, 48 |
387 \item {\tt NF} theorem, 77, 86 |
576 \item {\tt nat_case_succ} theorem, 48 |
388 \item {\tt NI0} theorem, 77 |
577 \item {\tt nat_def} theorem, 48 |
389 \item {\tt NI_succ} theorem, 77 |
578 \item {\tt nat_induct} theorem, 48, 79 |
390 \item {\tt NI_succL} theorem, 77 |
579 \item {\tt nat_rec} constant, 80 |
391 \item {\tt NIO} theorem, 85 |
580 \item {\tt nat_succI} theorem, 48 |
392 \item {\tt Not} constant, 6, 60 |
581 \item {\tt NatDef} theory, 78 |
393 \item {\tt not_def} theorem, 10 |
582 \item {\tt NC0} theorem, 130 |
394 \item {\tt not_sym} theorem, 11 |
583 \item {\tt NC_succ} theorem, 130 |
395 \item {\tt notE} theorem, 11 |
584 \item {\tt NE} theorem, 129, 130, 138 |
396 \item {\tt notI} theorem, 11 |
585 \item {\tt NEL} theorem, 130 |
397 \item {\tt notL} theorem, 62 |
586 \item {\tt NF} theorem, 130, 139 |
398 \item {\tt notnotD} theorem, 12 |
587 \item {\tt NI0} theorem, 130 |
399 \item {\tt notR} theorem, 62 |
588 \item {\tt NI_succ} theorem, 130 |
400 \item {\tt null} constant, 28 |
589 \item {\tt NI_succL} theorem, 130 |
401 |
590 \item {\tt Nil_Cons_iff} theorem, 50 |
402 \indexspace |
591 \item {\tt NilI} theorem, 50 |
403 |
592 \item {\tt NIO} theorem, 138 |
404 \item {\textit {o}} type, 59 |
593 \item {\tt Not} constant, 7, 60, 114 |
405 \item {\tt o} symbol, 6, 17 |
594 \item {\tt not_def} theorem, 8, 43, 64 |
406 \item {\tt o_def} theorem, 10 |
595 \item {\tt not_impE} theorem, 9 |
407 \item {\tt of} symbol, 9 |
596 \item {\tt not_sym} theorem, 65 |
408 \item {\tt or_def} theorem, 10 |
597 \item {\tt notE} theorem, 9, 10, 65 |
409 \item {\tt Ord} theory, 7 |
598 \item {\tt notI} theorem, 9, 65 |
410 \item {\tt ord} class, 7, 8, 26 |
599 \item {\tt notL} theorem, 116 |
411 \item {\tt order} class, 7, 26 |
600 \item {\tt notnotD} theorem, 11, 66 |
412 |
601 \item {\tt notR} theorem, 116 |
413 \indexspace |
602 \item {\tt null} constant, 82 |
414 |
603 |
415 \item {\tt pack} ML type, 65 |
604 \indexspace |
416 \item {\tt Pair} constant, 23 |
605 |
417 \item {\tt pair} constant, 73 |
606 \item {\tt O} symbol, 46 |
418 \item {\tt Pair_eq} theorem, 23 |
607 \item {\textit {o}} type, 5, 113 |
419 \item {\tt Pair_inject} theorem, 23 |
608 \item {\tt o} symbol, 60, 71 |
420 \item {\tt PairE} theorem, 23 |
609 \item {\tt o_def} theorem, 64 |
421 \item {\tt pc_tac}, \bold{67}, \bold{83}, 89, 90 |
610 \item {\tt of} symbol, 63 |
422 \item {\tt plus} class, 7 |
611 \item {\tt or_def} theorem, 43, 64 |
423 \item {\tt PlusC_inl} theorem, 79 |
612 \item {\tt Ord} theory, 61 |
424 \item {\tt PlusC_inr} theorem, 79 |
613 \item {\tt ord} class, 61, 62, 80 |
425 \item {\tt PlusE} theorem, 79, 83, 87 |
614 \item {\tt order} class, 61, 80 |
426 \item {\tt PlusEL} theorem, 79 |
615 |
427 \item {\tt PlusF} theorem, 79 |
616 \indexspace |
428 \item {\tt PlusFL} theorem, 79 |
617 |
429 \item {\tt PlusI_inl} theorem, 79, 88 |
618 \item {\tt pack} ML type, 119 |
430 \item {\tt PlusI_inlL} theorem, 79 |
619 \item {\tt Pair} constant, 26, 27, 77 |
431 \item {\tt PlusI_inr} theorem, 79 |
620 \item {\tt pair} constant, 126 |
432 \item {\tt PlusI_inrL} theorem, 79 |
621 \item {\tt Pair_def} theorem, 32 |
433 \item {\tt Pow} constant, 14 |
622 \item {\tt Pair_eq} theorem, 77 |
434 \item {\tt Pow_def} theorem, 17 |
623 \item {\tt Pair_inject} theorem, 38, 77 |
435 \item {\tt PowD} theorem, 19 |
624 \item {\tt Pair_inject1} theorem, 38 |
436 \item {\tt PowI} theorem, 19 |
625 \item {\tt Pair_inject2} theorem, 38 |
437 \item {\tt primrec}, 45--48 |
626 \item {\tt Pair_neq_0} theorem, 38 |
438 \item {\tt primrec} symbol, 26 |
627 \item {\tt PairE} theorem, 77 |
439 \item priorities, 3 |
628 \item {\tt pairing} theorem, 35 |
440 \item {\tt PROD} symbol, 74, 75 |
629 \item {\tt pc_tac}, \bold{121}, \bold{136}, 142, 143 |
441 \item {\tt Prod} constant, 73 |
630 \item {\tt Perm} theory, 43 |
442 \item {\tt Prod} theory, 23 |
631 \item {\tt Pi} constant, 26, 29, 41 |
443 \item {\tt ProdC} theorem, 77, 93 |
632 \item {\tt Pi_def} theorem, 32 |
444 \item {\tt ProdC2} theorem, 77 |
633 \item {\tt Pi_type} theorem, 40, 41 |
445 \item {\tt ProdE} theorem, 77, 90, 92, 94 |
634 \item {\tt plus} class, 61 |
446 \item {\tt ProdEL} theorem, 77 |
635 \item {\tt PlusC_inl} theorem, 132 |
447 \item {\tt ProdF} theorem, 77 |
636 \item {\tt PlusC_inr} theorem, 132 |
448 \item {\tt ProdFL} theorem, 77 |
637 \item {\tt PlusE} theorem, 132, 136, 140 |
449 \item {\tt ProdI} theorem, 77, 83, 85 |
638 \item {\tt PlusEL} theorem, 132 |
450 \item {\tt ProdIL} theorem, 77 |
639 \item {\tt PlusF} theorem, 132 |
451 \item {\tt prop_cs}, \bold{22} |
640 \item {\tt PlusFL} theorem, 132 |
452 \item {\tt prop_pack}, \bold{66} |
641 \item {\tt PlusI_inl} theorem, 132, 141 |
453 |
642 \item {\tt PlusI_inlL} theorem, 132 |
454 \indexspace |
643 \item {\tt PlusI_inr} theorem, 132 |
455 |
644 \item {\tt PlusI_inrL} theorem, 132 |
456 \item {\tt qed_spec_mp}, 43 |
645 \item {\tt Pow} constant, 26, 68 |
457 |
646 \item {\tt Pow_def} theorem, 71 |
458 \indexspace |
647 \item {\tt Pow_iff} theorem, 31 |
459 |
648 \item {\tt Pow_mono} theorem, 53 |
460 \item {\tt range} constant, 14, 56 |
649 \item {\tt PowD} theorem, 34, 54, 73 |
461 \item {\tt range_def} theorem, 17 |
650 \item {\tt PowI} theorem, 34, 54, 73 |
462 \item {\tt rangeE} theorem, 19, 57 |
651 \item {\tt primrec}, 99--102 |
463 \item {\tt rangeI} theorem, 19 |
652 \item {\tt primrec} symbol, 80 |
464 \item {\tt rec} constant, 73, 76 |
653 \item {\tt PrimReplace} constant, 26, 30 |
465 \item {\tt recdef}, 48--51 |
654 \item priorities, 2 |
466 \item {\tt record}, 33 |
655 \item {\tt PROD} symbol, 27, 29, 127, 128 |
467 \item {\tt record_split_tac}, 35, 36 |
656 \item {\tt Prod} constant, 126 |
|
657 \item {\tt Prod} theory, 77 |
|
658 \item {\tt ProdC} theorem, 130, 146 |
|
659 \item {\tt ProdC2} theorem, 130 |
|
660 \item {\tt ProdE} theorem, 130, 143, 145, 147 |
|
661 \item {\tt ProdEL} theorem, 130 |
|
662 \item {\tt ProdF} theorem, 130 |
|
663 \item {\tt ProdFL} theorem, 130 |
|
664 \item {\tt ProdI} theorem, 130, 136, 138 |
|
665 \item {\tt ProdIL} theorem, 130 |
|
666 \item {\tt prop_cs}, \bold{11}, \bold{76} |
|
667 \item {\tt prop_pack}, \bold{119} |
|
668 |
|
669 \indexspace |
|
670 |
|
671 \item {\tt qcase_def} theorem, 44 |
|
672 \item {\tt qconverse} constant, 43 |
|
673 \item {\tt qconverse_def} theorem, 44 |
|
674 \item {\tt qed_spec_mp}, 97 |
|
675 \item {\tt qfsplit_def} theorem, 44 |
|
676 \item {\tt QInl_def} theorem, 44 |
|
677 \item {\tt QInr_def} theorem, 44 |
|
678 \item {\tt QPair} theory, 43 |
|
679 \item {\tt QPair_def} theorem, 44 |
|
680 \item {\tt QSigma} constant, 43 |
|
681 \item {\tt QSigma_def} theorem, 44 |
|
682 \item {\tt qsplit} constant, 43 |
|
683 \item {\tt qsplit_def} theorem, 44 |
|
684 \item {\tt qsum_def} theorem, 44 |
|
685 \item {\tt QUniv} theory, 47 |
|
686 |
|
687 \indexspace |
|
688 |
|
689 \item {\tt range} constant, 26, 68, 110 |
|
690 \item {\tt range_def} theorem, 32, 71 |
|
691 \item {\tt range_of_fun} theorem, 40, 41 |
|
692 \item {\tt range_subset} theorem, 39 |
|
693 \item {\tt range_type} theorem, 40 |
|
694 \item {\tt rangeE} theorem, 39, 73, 111 |
|
695 \item {\tt rangeI} theorem, 39, 73 |
|
696 \item {\tt rank} constant, 49 |
|
697 \item {\tt rank_ss}, \bold{24} |
|
698 \item {\tt rec} constant, 48, 126, 129 |
|
699 \item {\tt rec_0} theorem, 48 |
|
700 \item {\tt rec_def} theorem, 48 |
|
701 \item {\tt rec_succ} theorem, 48 |
|
702 \item {\tt recdef}, 102--105 |
|
703 \item {\tt record}, 87 |
|
704 \item {\tt record_split_tac}, 89, 90 |
|
705 \item recursion |
468 \item recursion |
706 \subitem general, 102--105 |
469 \subitem general, 48--51 |
707 \subitem primitive, 99--102 |
470 \subitem primitive, 45--48 |
708 \item recursive functions, \see{recursion}{98} |
471 \item recursive functions, \see{recursion}{44} |
709 \item {\tt red_if_equal} theorem, 129 |
472 \item {\tt red_if_equal} theorem, 76 |
710 \item {\tt Reduce} constant, 126, 129, 135 |
473 \item {\tt Reduce} constant, 73, 76, 82 |
711 \item {\tt refl} theorem, 8, 63, 116 |
474 \item {\tt refl} theorem, 9, 62 |
712 \item {\tt refl_elem} theorem, 129, 133 |
475 \item {\tt refl_elem} theorem, 76, 80 |
713 \item {\tt refl_red} theorem, 129 |
476 \item {\tt refl_red} theorem, 76 |
714 \item {\tt refl_type} theorem, 129, 133 |
477 \item {\tt refl_type} theorem, 76, 80 |
715 \item {\tt REPEAT_FIRST}, 134 |
478 \item {\tt REPEAT_FIRST}, 81 |
716 \item {\tt repeat_goal_tac}, \bold{121} |
479 \item {\tt repeat_goal_tac}, \bold{67} |
717 \item {\tt RepFun} constant, 26, 29, 30, 33 |
480 \item {\tt replace_type} theorem, 80, 92 |
718 \item {\tt RepFun_def} theorem, 31 |
481 \item {\tt reresolve_tac}, \bold{67} |
719 \item {\tt RepFunE} theorem, 35 |
482 \item {\tt res_inst_tac}, 8 |
720 \item {\tt RepFunI} theorem, 35 |
483 \item {\tt rev} constant, 28 |
721 \item {\tt Replace} constant, 26, 29, 30, 33 |
484 \item {\tt rew_tac}, \bold{82} |
722 \item {\tt Replace_def} theorem, 31 |
485 \item {\tt RL}, 87 |
723 \item {\tt replace_type} theorem, 133, 145 |
486 \item {\tt RS}, 92, 94 |
724 \item {\tt ReplaceE} theorem, 35 |
487 |
725 \item {\tt ReplaceI} theorem, 35 |
488 \indexspace |
726 \item {\tt replacement} theorem, 31 |
489 |
727 \item {\tt reresolve_tac}, \bold{121} |
490 \item {\tt safe_goal_tac}, \bold{67} |
728 \item {\tt res_inst_tac}, 62 |
491 \item {\tt safe_tac}, \bold{83} |
729 \item {\tt restrict} constant, 26, 33 |
492 \item {\tt safestep_tac}, \bold{83} |
730 \item {\tt restrict} theorem, 40 |
|
731 \item {\tt restrict_bij} theorem, 46 |
|
732 \item {\tt restrict_def} theorem, 32 |
|
733 \item {\tt restrict_type} theorem, 40 |
|
734 \item {\tt rev} constant, 50, 82 |
|
735 \item {\tt rev_def} theorem, 50 |
|
736 \item {\tt rew_tac}, 19, \bold{135} |
|
737 \item {\tt rewrite_rule}, 19 |
|
738 \item {\tt right_comp_id} theorem, 46 |
|
739 \item {\tt right_comp_inverse} theorem, 46 |
|
740 \item {\tt right_inverse} theorem, 46 |
|
741 \item {\tt RL}, 140 |
|
742 \item {\tt RS}, 145, 147 |
|
743 |
|
744 \indexspace |
|
745 |
|
746 \item {\tt safe_goal_tac}, \bold{121} |
|
747 \item {\tt safe_tac}, \bold{136} |
|
748 \item {\tt safestep_tac}, \bold{136} |
|
749 \item search |
493 \item search |
750 \subitem best-first, 112 |
494 \subitem best-first, 58 |
751 \item {\tt select_equality} theorem, 64, 66 |
495 \item {\tt select_equality} theorem, 10, 12 |
752 \item {\tt selectI} theorem, 63, 64 |
496 \item {\tt selectI} theorem, 9, 10 |
753 \item {\tt separation} theorem, 35 |
497 \item {\tt Seqof} constant, 60 |
754 \item {\tt Seqof} constant, 114 |
498 \item sequent calculus, 59--71 |
755 \item sequent calculus, 113--124 |
499 \item {\tt Set} theory, 13, 16 |
756 \item {\tt Set} theory, 67, 70 |
500 \item {\tt set} constant, 28 |
757 \item {\tt set} constant, 82 |
501 \item {\tt set} type, 13 |
758 \item {\tt set} type, 67 |
502 \item {\tt set_current_thy}, 58 |
759 \item set theory, 24--58 |
503 \item {\tt set_diff_def} theorem, 17 |
760 \item {\tt set_current_thy}, 112 |
504 \item {\tt show_sorts}, 8 |
761 \item {\tt set_diff_def} theorem, 71 |
505 \item {\tt show_types}, 8 |
762 \item {\tt show_sorts}, 62 |
506 \item {\tt Sigma} constant, 23 |
763 \item {\tt show_types}, 62 |
507 \item {\tt Sigma_def} theorem, 23 |
764 \item {\tt Sigma} constant, 26, 29, 30, 38, 77 |
508 \item {\tt SigmaE} theorem, 23 |
765 \item {\tt Sigma_def} theorem, 32, 77 |
509 \item {\tt SigmaI} theorem, 23 |
766 \item {\tt SigmaE} theorem, 38, 77 |
|
767 \item {\tt SigmaE2} theorem, 38 |
|
768 \item {\tt SigmaI} theorem, 38, 77 |
|
769 \item simplification |
510 \item simplification |
770 \subitem of conjunctions, 6, 75 |
511 \subitem of conjunctions, 21 |
771 \item {\tt singletonE} theorem, 36 |
512 \item {\tt size} constant, 39 |
772 \item {\tt singletonI} theorem, 36 |
513 \item {\tt snd} constant, 23, 73, 78 |
773 \item {\tt size} constant, 93 |
514 \item {\tt snd_conv} theorem, 23 |
774 \item {\tt snd} constant, 26, 33, 77, 126, 131 |
515 \item {\tt snd_def} theorem, 78 |
775 \item {\tt snd_conv} theorem, 38, 77 |
516 \item {\tt sobj} type, 63 |
776 \item {\tt snd_def} theorem, 32, 131 |
517 \item {\tt spec} theorem, 12 |
777 \item {\tt sobj} type, 117 |
518 \item {\tt split} constant, 23, 73, 87 |
778 \item {\tt spec} theorem, 8, 66 |
519 \item {\tt split} theorem, 23 |
779 \item {\tt split} constant, 26, 33, 77, 126, 140 |
520 \item {\tt split_all_tac}, \bold{24} |
780 \item {\tt split} theorem, 38, 77 |
521 \item {\tt split_if} theorem, 12, 22 |
781 \item {\tt split_all_tac}, \bold{78} |
522 \item {\tt split_list_case} theorem, 27 |
782 \item {\tt split_def} theorem, 32 |
523 \item {\tt split_split} theorem, 23 |
783 \item {\tt split_if} theorem, 66, 76 |
524 \item {\tt split_sum_case} theorem, 25 |
784 \item {\tt split_list_case} theorem, 81 |
525 \item {\tt ssubst} theorem, 11, 13 |
785 \item {\tt split_split} theorem, 77 |
526 \item {\tt stac}, \bold{21} |
786 \item {\tt split_sum_case} theorem, 79 |
527 \item {\tt step_tac}, \bold{67}, \bold{83} |
787 \item {\tt ssubst} theorem, 9, 65, 67 |
528 \item {\tt strip_tac}, \bold{13} |
788 \item {\tt stac}, \bold{75} |
529 \item {\tt subset_def} theorem, 17 |
789 \item {\tt Step_tac}, 22 |
530 \item {\tt subset_refl} theorem, 18 |
790 \item {\tt step_tac}, 23, \bold{121}, \bold{136} |
531 \item {\tt subset_trans} theorem, 18 |
791 \item {\tt strip_tac}, \bold{67} |
532 \item {\tt subsetCE} theorem, 16, 18 |
792 \item {\tt subset_def} theorem, 31, 71 |
533 \item {\tt subsetD} theorem, 16, 18 |
793 \item {\tt subset_refl} theorem, 34, 72 |
534 \item {\tt subsetI} theorem, 18 |
794 \item {\tt subset_trans} theorem, 34, 72 |
535 \item {\tt subst} theorem, 9 |
795 \item {\tt subsetCE} theorem, 34, 70, 72 |
536 \item {\tt subst_elem} theorem, 76 |
796 \item {\tt subsetD} theorem, 34, 56, 70, 72 |
537 \item {\tt subst_elemL} theorem, 76 |
797 \item {\tt subsetI} theorem, 34, 54, 55, 72 |
538 \item {\tt subst_eqtyparg} theorem, 80, 92 |
798 \item {\tt subst} theorem, 8, 63 |
539 \item {\tt subst_prodE} theorem, 78, 80 |
799 \item {\tt subst_elem} theorem, 129 |
540 \item {\tt subst_type} theorem, 76 |
800 \item {\tt subst_elemL} theorem, 129 |
541 \item {\tt subst_typeL} theorem, 76 |
801 \item {\tt subst_eqtyparg} theorem, 133, 145 |
542 \item {\tt Suc} constant, 25 |
802 \item {\tt subst_prodE} theorem, 131, 133 |
543 \item {\tt Suc_not_Zero} theorem, 25 |
803 \item {\tt subst_type} theorem, 129 |
544 \item {\tt succ} constant, 73 |
804 \item {\tt subst_typeL} theorem, 129 |
545 \item {\tt SUM} symbol, 74, 75 |
805 \item {\tt Suc} constant, 79 |
546 \item {\tt Sum} constant, 73 |
806 \item {\tt Suc_not_Zero} theorem, 79 |
547 \item {\tt Sum} theory, 24 |
807 \item {\tt succ} constant, 26, 30, 126 |
548 \item {\tt sum_case} constant, 25 |
808 \item {\tt succ_def} theorem, 32 |
549 \item {\tt sum_case_Inl} theorem, 25 |
809 \item {\tt succ_inject} theorem, 36 |
550 \item {\tt sum_case_Inr} theorem, 25 |
810 \item {\tt succ_neq_0} theorem, 36 |
551 \item {\tt SumC} theorem, 78 |
811 \item {\tt succCI} theorem, 36 |
552 \item {\tt SumE} theorem, 78, 83, 87 |
812 \item {\tt succE} theorem, 36 |
553 \item {\tt sumE} theorem, 25 |
813 \item {\tt succI1} theorem, 36 |
554 \item {\tt SumE_fst} theorem, 78, 80, 92, 93 |
814 \item {\tt succI2} theorem, 36 |
555 \item {\tt SumE_snd} theorem, 78, 80, 94 |
815 \item {\tt SUM} symbol, 27, 29, 127, 128 |
556 \item {\tt SumEL} theorem, 78 |
816 \item {\tt Sum} constant, 126 |
557 \item {\tt SumF} theorem, 78 |
817 \item {\tt Sum} theory, 43, 78 |
558 \item {\tt SumFL} theorem, 78 |
818 \item {\tt sum_case} constant, 79 |
559 \item {\tt SumI} theorem, 78, 88 |
819 \item {\tt sum_case_Inl} theorem, 79 |
560 \item {\tt SumIL} theorem, 78 |
820 \item {\tt sum_case_Inr} theorem, 79 |
561 \item {\tt SumIL2} theorem, 80 |
821 \item {\tt sum_def} theorem, 44 |
562 \item {\tt surj} constant, 17, 21 |
822 \item {\tt sum_InlI} theorem, 44 |
563 \item {\tt surj_def} theorem, 21 |
823 \item {\tt sum_InrI} theorem, 44 |
564 \item {\tt surjective_pairing} theorem, 23 |
824 \item {\tt SUM_Int_distrib1} theorem, 42 |
565 \item {\tt surjective_sum} theorem, 25 |
825 \item {\tt SUM_Int_distrib2} theorem, 42 |
566 \item {\tt swap} theorem, 12 |
826 \item {\tt SUM_Un_distrib1} theorem, 42 |
567 \item {\tt swap_res_tac}, 57 |
827 \item {\tt SUM_Un_distrib2} theorem, 42 |
568 \item {\tt sym} theorem, 11, 62 |
828 \item {\tt SumC} theorem, 131 |
569 \item {\tt sym_elem} theorem, 76 |
829 \item {\tt SumE} theorem, 131, 136, 140 |
570 \item {\tt sym_type} theorem, 76 |
830 \item {\tt sumE} theorem, 79 |
571 \item {\tt symL} theorem, 63 |
831 \item {\tt sumE2} theorem, 44 |
572 |
832 \item {\tt SumE_fst} theorem, 131, 133, 145, 146 |
573 \indexspace |
833 \item {\tt SumE_snd} theorem, 131, 133, 147 |
574 |
834 \item {\tt SumEL} theorem, 131 |
575 \item {\tt T} constant, 73 |
835 \item {\tt SumF} theorem, 131 |
576 \item {\textit {t}} type, 72 |
836 \item {\tt SumFL} theorem, 131 |
577 \item {\tt take} constant, 28 |
837 \item {\tt SumI} theorem, 131, 141 |
578 \item {\tt takeWhile} constant, 28 |
838 \item {\tt SumIL} theorem, 131 |
579 \item {\tt TC} theorem, 79 |
839 \item {\tt SumIL2} theorem, 133 |
580 \item {\tt TE} theorem, 79 |
840 \item {\tt surj} constant, 46, 71, 75 |
581 \item {\tt TEL} theorem, 79 |
841 \item {\tt surj_def} theorem, 46, 75 |
582 \item {\tt term} class, 7, 59 |
842 \item {\tt surjective_pairing} theorem, 77 |
583 \item {\tt test_assume_tac}, \bold{81} |
843 \item {\tt surjective_sum} theorem, 79 |
584 \item {\tt TF} theorem, 79 |
844 \item {\tt swap} theorem, 11, 66 |
585 \item {\tt THE} symbol, 60 |
845 \item {\tt swap_res_tac}, 16, 111 |
586 \item {\tt The} constant, 60 |
846 \item {\tt sym} theorem, 9, 65, 116 |
587 \item {\tt The} theorem, 62 |
847 \item {\tt sym_elem} theorem, 129 |
588 \item {\tt thinL} theorem, 62 |
848 \item {\tt sym_type} theorem, 129 |
589 \item {\tt thinR} theorem, 62 |
849 \item {\tt symL} theorem, 117 |
590 \item {\tt TI} theorem, 79 |
850 |
591 \item {\tt times} class, 7 |
851 \indexspace |
592 \item {\tt tl} constant, 28 |
852 |
|
853 \item {\tt T} constant, 126 |
|
854 \item {\textit {t}} type, 125 |
|
855 \item {\tt take} constant, 82 |
|
856 \item {\tt takeWhile} constant, 82 |
|
857 \item {\tt TC} theorem, 132 |
|
858 \item {\tt TE} theorem, 132 |
|
859 \item {\tt TEL} theorem, 132 |
|
860 \item {\tt term} class, 5, 61, 113 |
|
861 \item {\tt test_assume_tac}, \bold{134} |
|
862 \item {\tt TF} theorem, 132 |
|
863 \item {\tt THE} symbol, 27, 29, 37, 114 |
|
864 \item {\tt The} constant, 26, 29, 30, 114 |
|
865 \item {\tt The} theorem, 116 |
|
866 \item {\tt the_def} theorem, 31 |
|
867 \item {\tt the_equality} theorem, 36, 37 |
|
868 \item {\tt theI} theorem, 36, 37 |
|
869 \item {\tt thinL} theorem, 116 |
|
870 \item {\tt thinR} theorem, 116 |
|
871 \item {\tt TI} theorem, 132 |
|
872 \item {\tt times} class, 61 |
|
873 \item {\tt tl} constant, 82 |
|
874 \item tracing |
593 \item tracing |
875 \subitem of unification, 62 |
594 \subitem of unification, 8 |
876 \item {\tt trans} theorem, 9, 65, 116 |
595 \item {\tt trans} theorem, 11, 62 |
877 \item {\tt trans_elem} theorem, 129 |
596 \item {\tt trans_elem} theorem, 76 |
878 \item {\tt trans_red} theorem, 129 |
597 \item {\tt trans_red} theorem, 76 |
879 \item {\tt trans_tac}, 81 |
598 \item {\tt trans_tac}, 27 |
880 \item {\tt trans_type} theorem, 129 |
599 \item {\tt trans_type} theorem, 76 |
881 \item {\tt True} constant, 7, 60, 114 |
600 \item {\tt True} constant, 6, 60 |
882 \item {\tt True_def} theorem, 8, 64, 116 |
601 \item {\tt True_def} theorem, 10, 62 |
883 \item {\tt True_or_False} theorem, 63, 64 |
602 \item {\tt True_or_False} theorem, 9, 10 |
884 \item {\tt TrueI} theorem, 9, 65 |
603 \item {\tt TrueI} theorem, 11 |
885 \item {\tt Trueprop} constant, 7, 60, 114 |
604 \item {\tt Trueprop} constant, 6, 60 |
886 \item {\tt TrueR} theorem, 117 |
605 \item {\tt TrueR} theorem, 63 |
887 \item {\tt tt} constant, 126 |
606 \item {\tt tt} constant, 73 |
888 \item {\tt Type} constant, 126 |
607 \item {\tt Type} constant, 73 |
889 \item type definition, \bold{84} |
608 \item type definition, \bold{30} |
890 \item {\tt typechk_tac}, \bold{134}, 139, 142, 146, 147 |
609 \item {\tt typechk_tac}, \bold{81}, 86, 89, 93, 94 |
891 \item {\tt typedef}, 81 |
610 \item {\tt typedef}, 27 |
892 |
611 |
893 \indexspace |
612 \indexspace |
894 |
613 |
895 \item {\tt UN} symbol, 27, 29, 68--70 |
614 \item {\tt UN} symbol, 14--16 |
896 \item {\tt Un} symbol, 26, 68 |
615 \item {\tt Un} symbol, 14 |
897 \item {\tt Un1} theorem, 70 |
616 \item {\tt Un1} theorem, 16 |
898 \item {\tt Un2} theorem, 70 |
617 \item {\tt Un2} theorem, 16 |
899 \item {\tt Un_absorb} theorem, 42, 74 |
618 \item {\tt Un_absorb} theorem, 20 |
900 \item {\tt Un_assoc} theorem, 42, 74 |
619 \item {\tt Un_assoc} theorem, 20 |
901 \item {\tt Un_commute} theorem, 42, 74 |
620 \item {\tt Un_commute} theorem, 20 |
902 \item {\tt Un_def} theorem, 31, 71 |
621 \item {\tt Un_def} theorem, 17 |
903 \item {\tt UN_E} theorem, 35, 73 |
622 \item {\tt UN_E} theorem, 19 |
904 \item {\tt UN_I} theorem, 35, 73 |
623 \item {\tt UN_I} theorem, 19 |
905 \item {\tt Un_Int_distrib} theorem, 42, 74 |
624 \item {\tt Un_Int_distrib} theorem, 20 |
906 \item {\tt Un_Inter} theorem, 74 |
625 \item {\tt Un_Inter} theorem, 20 |
907 \item {\tt Un_Inter_RepFun} theorem, 42 |
626 \item {\tt Un_least} theorem, 20 |
908 \item {\tt Un_least} theorem, 37, 74 |
627 \item {\tt Un_Union_image} theorem, 20 |
909 \item {\tt Un_Union_image} theorem, 74 |
628 \item {\tt Un_upper1} theorem, 20 |
910 \item {\tt Un_upper1} theorem, 37, 74 |
629 \item {\tt Un_upper2} theorem, 20 |
911 \item {\tt Un_upper2} theorem, 37, 74 |
630 \item {\tt UnCI} theorem, 16, 19 |
912 \item {\tt UnCI} theorem, 36, 37, 70, 73 |
631 \item {\tt UnE} theorem, 19 |
913 \item {\tt UnE} theorem, 36, 73 |
632 \item {\tt UnI1} theorem, 19 |
914 \item {\tt UnI1} theorem, 36, 37, 57, 73 |
633 \item {\tt UnI2} theorem, 19 |
915 \item {\tt UnI2} theorem, 36, 37, 73 |
|
916 \item unification |
634 \item unification |
917 \subitem incompleteness of, 62 |
635 \subitem incompleteness of, 8 |
918 \item {\tt Unify.trace_types}, 62 |
636 \item {\tt Unify.trace_types}, 8 |
919 \item {\tt UNION} constant, 68 |
637 \item {\tt UNION} constant, 14 |
920 \item {\tt Union} constant, 26, 68 |
638 \item {\tt Union} constant, 14 |
921 \item {\tt UNION1} constant, 68 |
639 \item {\tt UNION1} constant, 14 |
922 \item {\tt UNION1_def} theorem, 71 |
640 \item {\tt UNION1_def} theorem, 17 |
923 \item {\tt UNION_def} theorem, 71 |
641 \item {\tt UNION_def} theorem, 17 |
924 \item {\tt Union_def} theorem, 71 |
642 \item {\tt Union_def} theorem, 17 |
925 \item {\tt Union_iff} theorem, 31 |
643 \item {\tt Union_least} theorem, 20 |
926 \item {\tt Union_least} theorem, 37, 74 |
644 \item {\tt Union_Un_distrib} theorem, 20 |
927 \item {\tt Union_Un_distrib} theorem, 42, 74 |
645 \item {\tt Union_upper} theorem, 20 |
928 \item {\tt Union_upper} theorem, 37, 74 |
646 \item {\tt UnionE} theorem, 19 |
929 \item {\tt UnionE} theorem, 35, 56, 73 |
647 \item {\tt UnionI} theorem, 19 |
930 \item {\tt UnionI} theorem, 35, 56, 73 |
648 \item {\tt unit_eq} theorem, 24 |
931 \item {\tt unit_eq} theorem, 78 |
649 |
932 \item {\tt Univ} theory, 47 |
650 \indexspace |
933 \item {\tt Upair} constant, 25, 26, 30 |
651 |
934 \item {\tt Upair_def} theorem, 31 |
652 \item {\tt when} constant, 73, 78, 87 |
935 \item {\tt UpairE} theorem, 35 |
653 |
936 \item {\tt UpairI1} theorem, 35 |
654 \indexspace |
937 \item {\tt UpairI2} theorem, 35 |
655 |
938 |
656 \item {\tt zero_ne_succ} theorem, 76, 77 |
939 \indexspace |
657 \item {\tt ZF} theory, 5 |
940 |
|
941 \item {\tt vimage_def} theorem, 32 |
|
942 \item {\tt vimageE} theorem, 39 |
|
943 \item {\tt vimageI} theorem, 39 |
|
944 |
|
945 \indexspace |
|
946 |
|
947 \item {\tt when} constant, 126, 131, 140 |
|
948 |
|
949 \indexspace |
|
950 |
|
951 \item {\tt xor_def} theorem, 43 |
|
952 |
|
953 \indexspace |
|
954 |
|
955 \item {\tt zero_ne_succ} theorem, 129, 130 |
|
956 \item {\tt ZF} theory, 1, 24, 59 |
|
957 \item {\tt ZF_cs}, \bold{24} |
|
958 \item {\tt ZF_ss}, \bold{24} |
|
959 |
658 |
960 \end{theindex} |
659 \end{theindex} |