|
1 %%%% RULES.ML |
|
2 |
|
3 \idx{empty_set} ~(x:0) |
|
4 \idx{union_iff} A:Union(C) <-> (EX B:C. A:B) |
|
5 \idx{power_set} A : Pow(B) <-> A <= B |
|
6 \idx{infinity} 0:Inf & (ALL y:Inf. succ(y): Inf) |
|
7 \idx{foundation} A=0 | (EX x:A. ALL y:x. ~ y:A) |
|
8 |
|
9 \idx{replacement} (!!x y z.[| x:A; P(x,y); P(x,z) |] ==> y=z) ==> |
|
10 y : PrimReplace(A,P) <-> (EX x:A. P(x,y)) |
|
11 |
|
12 \idx{Replace_def} Replace(A,P) == PrimReplace(A, %x y. (EX!z.P(x,z)) & P(x,y)) |
|
13 \idx{RepFun_def} RepFun(A,f) == Replace(A, %x u. u=f(x)) |
|
14 \idx{Collect_def} Collect(A,P) == \{ y . x:A, x=y & P(x)\} |
|
15 \idx{the_def} The(P) == Union(\{y . x:\{0\}, P(y)\}) |
|
16 |
|
17 \idx{Upair_def} Upair(a,b) == |
|
18 \{y. x:Pow(Pow(0)), (x=0 & y=a) | (x=Pow(0) & y=b)\} |
|
19 |
|
20 \idx{Inter_def} Inter(A) == \{ x:Union(A) . ALL y:A. x:y\} |
|
21 |
|
22 \idx{Un_def} A Un B == Union(Upair(A,B)) |
|
23 \idx{Int_def} A Int B == Inter(Upair(A,B)) |
|
24 \idx{Diff_def} A - B == \{ x:A . ~(x:B) \} |
|
25 \idx{cons_def} cons(a,A) == Upair(a,a) Un A |
|
26 \idx{succ_def} succ(i) == cons(i,i) |
|
27 |
|
28 \idx{Pair_def} <a,b> == \{\{a,a\}, \{a,b\}\} |
|
29 \idx{fst_def} fst(A) == THE x. EX y. A=<x,y> |
|
30 \idx{snd_def} snd(A) == THE y. EX x. A=<x,y> |
|
31 \idx{split_def} split(p,c) == THE y. EX a b. p=<a,b> & y=c(a,b) |
|
32 \idx{Sigma_def} Sigma(A,B) == UN x:A. UN y:B(x). \{<x,y>\} |
|
33 |
|
34 \idx{domain_def} domain(r) == \{a:Union(Union(r)) . EX b. <a,b> : r\} |
|
35 \idx{range_def} range(r) == \{b:Union(Union(r)) . EX a. <a,b> : r\} |
|
36 \idx{field_def} field(r) == domain(r) Un range(r) |
|
37 \idx{image_def} r``A == \{y : range(r) . EX x:A. <x,y> : r\} |
|
38 \idx{vimage_def} r -`` A == \{x : domain(r) . EX y:A. <x,y> : r\} |
|
39 |
|
40 \idx{lam_def} Lambda(A,f) == RepFun(A, %x. <x,f(x)>) |
|
41 \idx{apply_def} f`a == THE y. <a,y> : f |
|
42 \idx{restrict_def} restrict(f,A) == lam x:A.f`x |
|
43 \idx{Pi_def} Pi(A,B) == \{f: Pow(Sigma(A,B)). ALL x:A. EX! y. <x,y>: f\} |
|
44 |
|
45 \idx{subset_def} A <= B == ALL x:A. x:B |
|
46 \idx{strict_subset_def} A <! B == A <=B & ~(A=B) |
|
47 \idx{extension} A = B <-> A <= B & B <= A |
|
48 |
|
49 \idx{Ball_def} Ball(A,P) == ALL x. x:A --> P(x) |
|
50 \idx{Bex_def} Bex(A,P) == EX x. x:A & P(x) |
|
51 |
|
52 |
|
53 %%%% LEMMAS.ML |
|
54 |
|
55 \idx{ballI} [| !!x. x:A ==> P(x) |] ==> ALL x:A. P(x) |
|
56 \idx{bspec} [| ALL x:A. P(x); x: A |] ==> P(x) |
|
57 \idx{ballE} [| ALL x:A. P(x); P(x) ==> Q; ~ x:A ==> Q |] ==> Q |
|
58 |
|
59 \idx{ball_cong} [| A=A'; !!x. x:A' ==> P(x) <-> P'(x) |] ==> |
|
60 (ALL x:A. P(x)) <-> (ALL x:A'. P'(x)) |
|
61 |
|
62 \idx{bexI} [| P(x); x: A |] ==> EX x:A. P(x) |
|
63 \idx{bexCI} [| ALL x:A. ~P(x) ==> P(a); a: A |] ==> EX x:A.P(x) |
|
64 \idx{bexE} [| EX x:A. P(x); !!x. [| x:A; P(x) |] ==> Q |] ==> Q |
|
65 |
|
66 \idx{bex_cong} [| A=A'; !!x. x:A' ==> P(x) <-> P'(x) |] ==> |
|
67 (EX x:A. P(x)) <-> (EX x:A'. P'(x)) |
|
68 |
|
69 \idx{subsetI} (!!x.x:A ==> x:B) ==> A <= B |
|
70 \idx{subsetD} [| A <= B; c:A |] ==> c:B |
|
71 \idx{subsetCE} [| A <= B; ~(c:A) ==> P; c:B ==> P |] ==> P |
|
72 \idx{subset_refl} A <= A |
|
73 \idx{subset_trans} [| A<=B; B<=C |] ==> A<=C |
|
74 |
|
75 \idx{equalityI} [| A <= B; B <= A |] ==> A = B |
|
76 \idx{equalityD1} A = B ==> A<=B |
|
77 \idx{equalityD2} A = B ==> B<=A |
|
78 \idx{equalityE} [| A = B; [| A<=B; B<=A |] ==> P |] ==> P |
|
79 |
|
80 \idx{emptyE} a:0 ==> P |
|
81 \idx{empty_subsetI} 0 <= A |
|
82 \idx{equals0I} [| !!y. y:A ==> False |] ==> A=0 |
|
83 \idx{equals0D} [| A=0; a:A |] ==> P |
|
84 |
|
85 \idx{PowI} A <= B ==> A : Pow(B) |
|
86 \idx{PowD} A : Pow(B) ==> A<=B |
|
87 |
|
88 \idx{ReplaceI} [| x: A; P(x,b); !!y. P(x,y) ==> y=b |] ==> |
|
89 b : \{y. x:A, P(x,y)\} |
|
90 |
|
91 \idx{ReplaceE} [| b : \{y. x:A, P(x,y)\}; |
|
92 !!x. [| x: A; P(x,b); ALL y. P(x,y)-->y=b |] ==> R |
|
93 |] ==> R |
|
94 |
|
95 \idx{Replace_cong} [| A=B; !!x y. x:B ==> P(x,y) <-> Q(x,y) |] ==> |
|
96 \{y. x:A, P(x,y)\} = \{y. x:B, Q(x,y)\} |
|
97 |
|
98 \idx{RepFunI} [| a : A |] ==> f(a) : RepFun(A,f) |
|
99 \idx{RepFunE} [| b : RepFun(A, %x.f(x)); |
|
100 !!x.[| x:A; b=f(x) |] ==> P |] ==> P |
|
101 |
|
102 \idx{RepFun_cong} [| A=B; !!x. x:B ==> f(x)=g(x) |] ==> |
|
103 RepFun(A, %x.f(x)) = RepFun(B, %x.g(x)) |
|
104 |
|
105 |
|
106 \idx{separation} x : Collect(A,P) <-> x:A & P(x) |
|
107 \idx{CollectI} [| a:A; P(a) |] ==> a : \{x:A. P(x)\} |
|
108 \idx{CollectE} [| a : \{x:A. P(x)\}; [| a:A; P(a) |] ==> R |] ==> R |
|
109 \idx{CollectD1} a : \{x:A. P(x)\} ==> a:A |
|
110 \idx{CollectD2} a : \{x:A. P(x)\} ==> P(a) |
|
111 |
|
112 \idx{Collect_cong} [| A=B; !!x. x:B ==> P(x) <-> Q(x) |] ==> |
|
113 \{x:A. P(x)\} = \{x:B. Q(x)\} |
|
114 |
|
115 \idx{UnionI} [| B: C; A: B |] ==> A: Union(C) |
|
116 \idx{UnionE} [| A : Union(C); !!B.[| A: B; B: C |] ==> R |] ==> R |
|
117 |
|
118 \idx{InterI} [| !!x. x: C ==> A: x; c:C |] ==> A : Inter(C) |
|
119 \idx{InterD} [| A : Inter(C); B : C |] ==> A : B |
|
120 \idx{InterE} [| A : Inter(C); A:B ==> R; ~ B:C ==> R |] ==> R |
|
121 |
|
122 \idx{UN_I} [| a: A; b: B(a) |] ==> b: (UN x:A. B(x)) |
|
123 \idx{UN_E} [| b : (UN x:A. B(x)); !!x.[| x: A; b: B(x) |] ==> R |] ==> R |
|
124 |
|
125 \idx{INT_I} [| !!x. x: A ==> b: B(x); a: A |] ==> b: (INT x:A. B(x)) |
|
126 \idx{INT_E} [| b : (INT x:A. B(x)); a: A |] ==> b : B(a) |
|
127 |
|
128 |
|
129 %%%% UPAIR.ML |
|
130 |
|
131 \idx{pairing} a:Upair(b,c) <-> (a=b | a=c) |
|
132 \idx{UpairI1} a : Upair(a,b) |
|
133 \idx{UpairI2} b : Upair(a,b) |
|
134 \idx{UpairE} [| a : Upair(b,c); a = b ==> P; a = c ==> P |] ==> P |
|
135 |
|
136 \idx{UnI1} c : A ==> c : A Un B |
|
137 \idx{UnI2} c : B ==> c : A Un B |
|
138 \idx{UnCI} (~c : B ==> c : A) ==> c : A Un B |
|
139 \idx{UnE} [| c : A Un B; c:A ==> P; c:B ==> P |] ==> P |
|
140 |
|
141 \idx{IntI} [| c : A; c : B |] ==> c : A Int B |
|
142 \idx{IntD1} c : A Int B ==> c : A |
|
143 \idx{IntD2} c : A Int B ==> c : B |
|
144 \idx{IntE} [| c : A Int B; [| c:A; c:B |] ==> P |] ==> P |
|
145 |
|
146 \idx{DiffI} [| c : A; ~ c : B |] ==> c : A - B |
|
147 \idx{DiffD1} c : A - B ==> c : A |
|
148 \idx{DiffD2} [| c : A - B; c : B |] ==> P |
|
149 \idx{DiffE} [| c : A - B; [| c:A; ~ c:B |] ==> P |] ==> P |
|
150 |
|
151 \idx{consI1} a : cons(a,B) |
|
152 \idx{consI2} a : B ==> a : cons(b,B) |
|
153 \idx{consCI} (~ a:B ==> a=b) ==> a: cons(b,B) |
|
154 \idx{consE} [| a : cons(b,A); a=b ==> P; a:A ==> P |] ==> P |
|
155 |
|
156 \idx{singletonI} a : \{a\} |
|
157 \idx{singletonE} [| a : \{b\}; a=b ==> P |] ==> P |
|
158 |
|
159 \idx{succI1} i : succ(i) |
|
160 \idx{succI2} i : j ==> i : succ(j) |
|
161 \idx{succCI} (~ i:j ==> i=j) ==> i: succ(j) |
|
162 \idx{succE} [| i : succ(j); i=j ==> P; i:j ==> P |] ==> P |
|
163 \idx{succ_neq_0} [| succ(n)=0 |] ==> P |
|
164 \idx{succ_inject} succ(m) = succ(n) ==> m=n |
|
165 |
|
166 \idx{the_equality} [| P(a); !!x. P(x) ==> x=a |] ==> (THE x. P(x)) = a |
|
167 \idx{theI} EX! x. P(x) ==> P(THE x. P(x)) |
|
168 |
|
169 \idx{mem_anti_sym} [| a:b; b:a |] ==> P |
|
170 \idx{mem_anti_refl} a:a ==> P |
|
171 |
|
172 |
|
173 %%% SUBSET.ML |
|
174 |
|
175 \idx{Union_upper} B:A ==> B <= Union(A) |
|
176 \idx{Union_least} [| !!x. x:A ==> x<=C |] ==> Union(A) <= C |
|
177 |
|
178 \idx{Inter_lower} B:A ==> Inter(A) <= B |
|
179 \idx{Inter_greatest} [| a:A; !!x. x:A ==> C<=x |] ==> C <= Inter(A) |
|
180 |
|
181 \idx{Un_upper1} A <= A Un B |
|
182 \idx{Un_upper2} B <= A Un B |
|
183 \idx{Un_least} [| A<=C; B<=C |] ==> A Un B <= C |
|
184 |
|
185 \idx{Int_lower1} A Int B <= A |
|
186 \idx{Int_lower2} A Int B <= B |
|
187 \idx{Int_greatest} [| C<=A; C<=B |] ==> C <= A Int B |
|
188 |
|
189 \idx{Diff_subset} A-B <= A |
|
190 \idx{Diff_contains} [| C<=A; C Int B = 0 |] ==> C <= A-B |
|
191 |
|
192 \idx{Collect_subset} Collect(A,P) <= A |
|
193 |
|
194 %%% PAIR.ML |
|
195 |
|
196 \idx{Pair_inject1} <a,b> = <c,d> ==> a=c |
|
197 \idx{Pair_inject2} <a,b> = <c,d> ==> b=d |
|
198 \idx{Pair_inject} [| <a,b> = <c,d>; [| a=c; b=d |] ==> P |] ==> P |
|
199 \idx{Pair_neq_0} <a,b>=0 ==> P |
|
200 |
|
201 \idx{fst_conv} fst(<a,b>) = a |
|
202 \idx{snd_conv} snd(<a,b>) = b |
|
203 \idx{split_conv} split(<a,b>, %x y.c(x,y)) = c(a,b) |
|
204 |
|
205 \idx{SigmaI} [| a:A; b:B(a) |] ==> <a,b> : (SUM x:A. B(x)) |
|
206 |
|
207 \idx{SigmaE} [| c: (SUM x:A. B(x)); |
|
208 !!x y.[| x:A; y:B(x); c=<x,y> |] ==> P |
|
209 |] ==> P |
|
210 |
|
211 \idx{SigmaE2} [| <a,b> : (SUM x:A. B(x)); |
|
212 [| a:A; b:B(a) |] ==> P |
|
213 |] ==> P |
|
214 |
|
215 |
|
216 %%% DOMRANGE.ML |
|
217 |
|
218 \idx{domainI} <a,b>: r ==> a : domain(r) |
|
219 \idx{domainE} [| a : domain(r); !!y. <a,y>: r ==> P |] ==> P |
|
220 \idx{domain_subset} domain(Sigma(A,B)) <= A |
|
221 |
|
222 \idx{rangeI} <a,b>: r ==> b : range(r) |
|
223 \idx{rangeE} [| b : range(r); !!x. <x,b>: r ==> P |] ==> P |
|
224 \idx{range_subset} range(A*B) <= B |
|
225 |
|
226 \idx{fieldI1} <a,b>: r ==> a : field(r) |
|
227 \idx{fieldI2} <a,b>: r ==> b : field(r) |
|
228 \idx{fieldCI} (~ <c,a>:r ==> <a,b>: r) ==> a : field(r) |
|
229 |
|
230 \idx{fieldE} [| a : field(r); |
|
231 !!x. <a,x>: r ==> P; |
|
232 !!x. <x,a>: r ==> P |
|
233 |] ==> P |
|
234 |
|
235 \idx{field_subset} field(A*A) <= A |
|
236 |
|
237 \idx{imageI} [| <a,b>: r; a:A |] ==> b : r``A |
|
238 \idx{imageE} [| b: r``A; !!x.[| <x,b>: r; x:A |] ==> P |] ==> P |
|
239 |
|
240 \idx{vimageI} [| <a,b>: r; b:B |] ==> a : r-``B |
|
241 \idx{vimageE} [| a: r-``B; !!x.[| <a,x>: r; x:B |] ==> P |] ==> P |
|
242 |
|
243 |
|
244 %%% FUNC.ML |
|
245 |
|
246 \idx{fun_is_rel} f: (PROD x:A.B(x)) ==> f <= Sigma(A,B) |
|
247 |
|
248 \idx{apply_equality} [| <a,b>: f; f: (PROD x:A.B(x)) |] ==> f`a = b |
|
249 \idx{apply_equality2} [| <a,b>: f; <a,c>: f; f: (PROD x:A.B(x)) |] ==> b=c |
|
250 |
|
251 \idx{apply_type} [| f: (PROD x:A.B(x)); a:A |] ==> f`a : B(a) |
|
252 \idx{apply_Pair} [| f: (PROD x:A.B(x)); a:A |] ==> <a,f`a>: f |
|
253 \idx{apply_iff} [| f: (PROD x:A.B(x)); a:A |] ==> <a,b>: f <-> f`a = b |
|
254 |
|
255 \idx{domain_type} [| <a,b> : f; f: (PROD x:A.B(x)) |] ==> a : A |
|
256 \idx{range_type} [| <a,b> : f; f: (PROD x:A.B(x)) |] ==> b : B(a) |
|
257 |
|
258 \idx{Pi_type} [| f: A->C; !!x. x:A ==> f`x : B(x) |] ==> f: Pi(A,B) |
|
259 \idx{domain_of_fun} f : Pi(A,B) ==> domain(f)=A |
|
260 \idx{range_of_fun} f : Pi(A,B) ==> f: A->range(f) |
|
261 |
|
262 \idx{fun_extension} [| f : (PROD x:A.B(x)); g: (PROD x:A.D(x)); |
|
263 !!x. x:A ==> f`x = g`x |
|
264 |] ==> f=g |
|
265 |
|
266 \idx{lamI} a:A ==> <a,b(a)> : (lam x:A. b(x)) |
|
267 \idx{lamE} [| p: (lam x:A. b(x)); !!x.[| x:A; p=<x,b(x)> |] ==> P |
|
268 |] ==> P |
|
269 |
|
270 \idx{lam_type} [| !!x. x:A ==> b(x): B(x) |] ==> |
|
271 (lam x:A.b(x)) : (PROD x:A.B(x)) |
|
272 |
|
273 \idx{beta_conv} a : A ==> (lam x:A.b(x)) ` a = b(a) |
|
274 \idx{eta_conv} f : (PROD x:A.B(x)) ==> (lam x:A. f`x) = f |
|
275 |
|
276 \idx{lam_theI} (!!x. x:A ==> EX! y. Q(x,y)) ==> EX h. ALL x:A. Q(x, h`x) |
|
277 |
|
278 \idx{restrict_conv} a : A ==> restrict(f,A) ` a = f`a |
|
279 \idx{restrict_type} [| !!x. x:A ==> f`x: B(x) |] ==> |
|
280 restrict(f,A) : (PROD x:A.B(x)) |
|
281 |
|
282 \idx{fun_empty} 0: 0->0 |
|
283 \idx{fun_single} \{<a,b>\} : \{a\} -> \{b\} |
|
284 |
|
285 \idx{fun_disjoint_Un} [| f: A->B; g: C->D; A Int C = 0 |] ==> |
|
286 (f Un g) : (A Un C) -> (B Un D) |
|
287 |
|
288 \idx{fun_disjoint_apply1} [| a:A; f: A->B; g: C->D; A Int C = 0 |] ==> |
|
289 (f Un g)`a = f`a |
|
290 |
|
291 \idx{fun_disjoint_apply2} [| c:C; f: A->B; g: C->D; A Int C = 0 |] ==> |
|
292 (f Un g)`c = g`c |
|
293 |
|
294 |
|
295 %%% SIMPDATA.ML |
|
296 |
|
297 a\in a & \bimp & False\\ |
|
298 a\in \emptyset & \bimp & False\\ |
|
299 a \in A \union B & \bimp & a\in A \disj a\in B\\ |
|
300 a \in A \inter B & \bimp & a\in A \conj a\in B\\ |
|
301 a \in A-B & \bimp & a\in A \conj \neg (a\in B)\\ |
|
302 a \in {\tt cons}(b,B) & \bimp & a=b \disj a\in B\\ |
|
303 i \in {\tt succ}(j) & \bimp & i=j \disj i\in j\\ |
|
304 A\in \bigcup(C) & \bimp & (\exists B. B\in C \conj A\in B)\\ |
|
305 A\in \bigcap(C) & \bimp & (\forall B. B\in C \imp A\in B) |
|
306 \qquad (\exists B. B\in C)\\ |
|
307 a \in {\tt Collect}(A,P) & \bimp & a\in A \conj P(a)\\ |
|
308 b \in {\tt RepFun}(A,f) & \bimp & (\exists x. x\in A \conj b=f(x)) |
|
309 |
|
310 equalities.ML perm.ML plus.ML nat.ML |
|
311 ---------------------------------------------------------------- |
|
312 equalities.ML |
|
313 |
|
314 \idx{Int_absorb} A Int A = A |
|
315 \idx{Int_commute} A Int B = B Int A |
|
316 \idx{Int_assoc} (A Int B) Int C = A Int (B Int C) |
|
317 \idx{Int_Un_distrib} (A Un B) Int C = (A Int C) Un (B Int C) |
|
318 |
|
319 \idx{Un_absorb} A Un A = A |
|
320 \idx{Un_commute} A Un B = B Un A |
|
321 \idx{Un_assoc} (A Un B) Un C = A Un (B Un C) |
|
322 \idx{Un_Int_distrib} (A Int B) Un C = (A Un C) Int (B Un C) |
|
323 |
|
324 \idx{Diff_cancel} A-A = 0 |
|
325 \idx{Diff_disjoint} A Int (B-A) = 0 |
|
326 \idx{Diff_partition} A<=B ==> A Un (B-A) = B |
|
327 \idx{double_complement} [| A<=B; B<= C |] ==> (B - (C-A)) = A |
|
328 \idx{Diff_Un} A - (B Un C) = (A-B) Int (A-C) |
|
329 \idx{Diff_Int} A - (B Int C) = (A-B) Un (A-C) |
|
330 |
|
331 \idx{Union_Un_distrib} Union(A Un B) = Union(A) Un Union(B) |
|
332 \idx{Inter_Un_distrib} [| a:A; b:B |] ==> |
|
333 Inter(A Un B) = Inter(A) Int Inter(B) |
|
334 |
|
335 \idx{Int_Union_RepFun} A Int Union(B) = (UN C:B. A Int C) |
|
336 |
|
337 \idx{Un_Inter_RepFun} b:B ==> |
|
338 A Un Inter(B) = (INT C:B. A Un C) |
|
339 |
|
340 \idx{SUM_Un_distrib1} (SUM x:A Un B. C(x)) = |
|
341 (SUM x:A. C(x)) Un (SUM x:B. C(x)) |
|
342 |
|
343 \idx{SUM_Un_distrib2} (SUM x:C. A(x) Un B(x)) = |
|
344 (SUM x:C. A(x)) Un (SUM x:C. B(x)) |
|
345 |
|
346 \idx{SUM_Int_distrib1} (SUM x:A Int B. C(x)) = |
|
347 (SUM x:A. C(x)) Int (SUM x:B. C(x)) |
|
348 |
|
349 \idx{SUM_Int_distrib2} (SUM x:C. A(x) Int B(x)) = |
|
350 (SUM x:C. A(x)) Int (SUM x:C. B(x)) |
|
351 |
|
352 |
|
353 ---------------------------------------------------------------- |
|
354 perm.ML |
|
355 |
|
356 \idx{comp_def} |
|
357 r O s == \{xz : domain(s)*range(r) . |
|
358 EX x y z. xz=<x,z> & <x,y>:s & <y,z>:r\}), |
|
359 \idx{id_def} (*the identity function for A*) |
|
360 id(A) == (lam x:A. x)), |
|
361 \idx{inj_def} |
|
362 inj(A,B) == |
|
363 \{ f: A->B. ALL w:A. ALL x:A. f`w=f`x --> w=x\}), |
|
364 \idx{surj_def} |
|
365 surj(A,B) == \{ f: A->B . ALL y:B. EX x:A. f`x=y\}), |
|
366 \idx{bij_def} |
|
367 bij(A,B) == inj(A,B) Int surj(A,B)) |
|
368 |
|
369 |
|
370 \idx{surj_is_fun} f: surj(A,B) ==> f: A->B |
|
371 \idx{fun_is_surj} f : Pi(A,B) ==> f: surj(A,range(f)) |
|
372 |
|
373 \idx{inj_is_fun} f: inj(A,B) ==> f: A->B |
|
374 \idx{inj_equality} [| <a,b>:f; <c,b>:f; f: inj(A,B) |] ==> a=c |
|
375 |
|
376 \idx{bij_is_fun} f: bij(A,B) ==> f: A->B |
|
377 |
|
378 \idx{inj_converse_surj} f: inj(A,B) ==> converse(f): surj(range(f), A) |
|
379 |
|
380 \idx{left_inverse} [| f: inj(A,B); a: A |] ==> converse(f)`(f`a) = a |
|
381 \idx{right_inverse} [| f: inj(A,B); b: range(f) |] ==> |
|
382 f`(converse(f)`b) = b |
|
383 |
|
384 \idx{inj_converse_inj} f: inj(A,B) ==> converse(f): inj(range(f), A) |
|
385 \idx{bij_converse_bij} f: bij(A,B) ==> converse(f): bij(B,A) |
|
386 |
|
387 \idx{comp_type} [| s<=A*B; r<=B*C |] ==> (r O s) <= A*C |
|
388 \idx{comp_assoc} (r O s) O t = r O (s O t) |
|
389 |
|
390 \idx{left_comp_id} r<=A*B ==> id(B) O r = r |
|
391 \idx{right_comp_id} r<=A*B ==> r O id(A) = r |
|
392 |
|
393 \idx{comp_func} [| g: A->B; f: B->C |] ==> (f O g) : A->C |
|
394 \idx{comp_func_apply} [| g: A->B; f: B->C; a:A |] ==> (f O g)`a = f`(g`a) |
|
395 |
|
396 \idx{comp_inj} [| g: inj(A,B); f: inj(B,C) |] ==> (f O g) : inj(A,C) |
|
397 \idx{comp_surj} [| g: surj(A,B); f: surj(B,C) |] ==> (f O g) : surj(A,C) |
|
398 \idx{comp_bij} [| g: bij(A,B); f: bij(B,C) |] ==> (f O g) : bij(A,C) |
|
399 |
|
400 \idx{left_comp_inverse} f: inj(A,B) ==> converse(f) O f = id(A) |
|
401 \idx{right_comp_inverse} f: surj(A,B) ==> f O converse(f) = id(B) |
|
402 |
|
403 \idx{bij_disjoint_Un} |
|
404 [| f: bij(A,B); g: bij(C,D); A Int C = 0; B Int D = 0 |] ==> |
|
405 (f Un g) : bij(A Un C, B Un D) |
|
406 |
|
407 \idx{restrict_bij} [| f: inj(A,B); C<=A |] ==> restrict(f,C): bij(C, f``C) |
|
408 |
|
409 |
|
410 ---------------------------------------------------------------- |
|
411 plus.ML |
|
412 |
|
413 \idx{plus_def} A+B == \{0\}*A Un \{\{0\}\}*B |
|
414 \idx{Inl_def} Inl(a) == < 0 ,a> |
|
415 \idx{Inr_def} Inr(b) == <\{0\},b> |
|
416 \idx{when_def} when(u,c,d) == |
|
417 THE y. EX z.(u=Inl(z) & y=c(z)) | (u=Inr(z) & y=d(z)) |
|
418 |
|
419 \idx{plus_InlI} a : A ==> Inl(a) : A+B |
|
420 \idx{plus_InrI} b : B ==> Inr(b) : A+B |
|
421 |
|
422 \idx{Inl_inject} Inl(a) = Inl(b) ==> a=b |
|
423 \idx{Inr_inject} Inr(a) = Inr(b) ==> a=b |
|
424 \idx{Inl_neq_Inr} Inl(a)=Inr(b) ==> P |
|
425 |
|
426 \idx{plusE2} u: A+B ==> (EX x. x:A & u=Inl(x)) | (EX y. y:B & u=Inr(y)) |
|
427 |
|
428 \idx{when_Inl_conv} when(Inl(a),c,d) = c(a) |
|
429 \idx{when_Inr_conv} when(Inr(b),c,d) = d(b) |
|
430 |
|
431 \idx{when_type} [| u: A+B; |
|
432 !!x. x: A ==> c(x): C(Inl(x)); |
|
433 !!y. y: B ==> d(y): C(Inr(y)) |
|
434 |] ==> when(u,c,d) : C(u) |
|
435 |
|
436 |
|
437 ---------------------------------------------------------------- |
|
438 nat.ML |
|
439 |
|
440 |
|
441 \idx{nat_def} nat == lfp(lam r: Pow(Inf). \{0\} Un RepFun(r,succ)) |
|
442 \idx{nat_case_def} nat_case(n,a,b) == |
|
443 THE y. n=0 & y=a | (EX x. n=succ(x) & y=b(x)) |
|
444 \idx{nat_rec_def} nat_rec(k,a,b) == |
|
445 transrec(nat, k, %n f. nat_case(n, a, %m. b(m, f`m))) |
|
446 |
|
447 \idx{nat_0_I} 0 : nat |
|
448 \idx{nat_succ_I} n : nat ==> succ(n) : nat |
|
449 |
|
450 \idx{nat_induct} |
|
451 [| n: nat; P(0); !!x. [| x: nat; P(x) |] ==> P(succ(x)) |
|
452 |] ==> P(n) |
|
453 |
|
454 \idx{nat_case_0_conv} nat_case(0,a,b) = a |
|
455 \idx{nat_case_succ_conv} nat_case(succ(m),a,b) = b(m) |
|
456 |
|
457 \idx{nat_case_type} |
|
458 [| n: nat; a: C(0); !!m. m: nat ==> b(m): C(succ(m)) |
|
459 |] ==> nat_case(n,a,b) : C(n) |
|
460 |
|
461 \idx{nat_rec_0_conv} nat_rec(0,a,b) = a |
|
462 \idx{nat_rec_succ_conv} m: nat ==> nat_rec(succ(m),a,b) = b(m, nat_rec(m,a,b)) |
|
463 |
|
464 \idx{nat_rec_type} |
|
465 [| n: nat; |
|
466 a: C(0); |
|
467 !!m z. [| m: nat; z: C(m) |] ==> b(m,z): C(succ(m)) |
|
468 |] ==> nat_rec(n,a,b) : C(n) |