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