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