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