|
1 (* Title: HOL/ex/PiSets.thy |
|
2 ID: $Id$ |
|
3 Author: Florian Kammueller, University of Cambridge |
|
4 |
|
5 Pi sets and their application. |
|
6 *) |
|
7 |
|
8 (* One abbreviation for my major simp application *) |
|
9 fun afs thms = (asm_full_simp_tac (simpset() addsimps thms)); |
|
10 (* strip outer quantifiers and lift implication *) |
|
11 fun strip i = (REPEAT ((rtac ballI i) |
|
12 ORELSE (rtac allI i) |
|
13 ORELSE (rtac impI i))); |
|
14 (* eresolve but leave the eliminated assumptions (improves unification) *) |
|
15 goal HOL.thy "!! P. [| P |] ==> P & P"; |
|
16 by (Fast_tac 1); |
|
17 val double = result(); |
|
18 |
|
19 fun re_tac rule r i = ((rotate_tac (r - 1) i) |
|
20 THEN (dtac double i) |
|
21 THEN (rotate_tac ~1 i) |
|
22 THEN (etac conjE i) |
|
23 THEN (rotate_tac ~1 i) |
|
24 THEN (etac rule i)); |
|
25 |
|
26 (* individual theorems for convenient use *) |
|
27 val [p1,p2] = goal HOL.thy "[|P == Q; P|] ==> Q"; |
|
28 by (fold_goals_tac [p1]); |
|
29 br p2 1; |
|
30 val apply_def = result(); |
|
31 |
|
32 goal HOL.thy "!! P x y. x = y ==> P(x) = P(y)"; |
|
33 be ssubst 1; |
|
34 br refl 1; |
|
35 val extend = result(); |
|
36 |
|
37 val [p1] = goal HOL.thy "P ==> ~~P"; |
|
38 br notI 1; |
|
39 br (p1 RSN(2, notE)) 1; |
|
40 ba 1; |
|
41 val notnotI = result(); |
|
42 |
|
43 val [p1] = goal Set.thy "? x. x: S ==> S ~= {}"; |
|
44 br contrapos 1; |
|
45 br (p1 RS notnotI) 1; |
|
46 be ssubst 1; |
|
47 br notI 1; |
|
48 be exE 1; |
|
49 be emptyE 1; |
|
50 val ExEl_NotEmpty = result(); |
|
51 |
|
52 |
|
53 val [p1] = goal HOL.thy "~x ==> x = False"; |
|
54 val l1 = (p1 RS (not_def RS apply_def)) RS mp; |
|
55 val l2 = read_instantiate [("P","x")] FalseE; |
|
56 br iffI 1; |
|
57 br l1 1; |
|
58 br l2 2; |
|
59 ba 1; |
|
60 ba 1; |
|
61 val NoteqFalseEq = result(); |
|
62 |
|
63 val [p1] = goal HOL.thy "~ (! x. ~P(x)) ==> ? x. P(x)"; |
|
64 br exCI 1; |
|
65 (* 1. ! x. ~ P x ==> P ?a *) |
|
66 val l1 = p1 RS NoteqFalseEq; |
|
67 (* l1 = (! x. ~ P x) = False *) |
|
68 val l2 = l1 RS iffD1; |
|
69 val l3 = l1 RS iffD2; |
|
70 val l4 = read_instantiate [("P", "P ?a")] FalseE; |
|
71 br (l2 RS l4) 1; |
|
72 ba 1; |
|
73 val NotAllNot_Ex = result(); |
|
74 |
|
75 val [p1] = goal HOL.thy "~(? x. P(x)) ==> ! x. ~ P(x)"; |
|
76 br notnotD 1; |
|
77 br (p1 RS contrapos) 1; |
|
78 br NotAllNot_Ex 1; |
|
79 ba 1; |
|
80 val NotEx_AllNot = result(); |
|
81 |
|
82 goal Set.thy "!!S. ~ (? x. x : S) ==> S = {}"; |
|
83 by (Fast_tac 1); |
|
84 val NoEl_Empty = result(); |
|
85 |
|
86 goal Set.thy "!!S. S ~= {} ==> ? x. x : S"; |
|
87 by (Fast_tac 1); |
|
88 val NotEmpty_ExEl = result(); |
|
89 |
|
90 goal PiSets.thy "!!S. S = {} ==> ! x. x ~: S"; |
|
91 by (Fast_tac 1); |
|
92 val Empty_NoElem = result(); |
|
93 |
|
94 |
|
95 val [q1,q2] = goal HOL.thy "[| b = a ; (P a) |] ==> (P b)"; |
|
96 br (q1 RS ssubst) 1; |
|
97 br q2 1; |
|
98 val forw_subst = result(); |
|
99 |
|
100 val [q1,q2] = goal HOL.thy "[| a = b ; (P a) |] ==> (P b)"; |
|
101 br (q1 RS subst) 1; |
|
102 br q2 1; |
|
103 val forw_ssubst = result(); |
|
104 |
|
105 goal Prod.thy "((fst A),(fst(snd A)),(fst (snd (snd A))),(snd(snd(snd A)))) = A"; |
|
106 br (surjective_pairing RS subst) 1; |
|
107 br (surjective_pairing RS subst) 1; |
|
108 br (surjective_pairing RS subst) 1; |
|
109 br refl 1; |
|
110 val blow4 = result(); |
|
111 |
|
112 goal Prod.thy "!! P a b. (%(a,b). P a b) A ==> P (fst A)(snd A)"; |
|
113 by (Step_tac 1); |
|
114 by (afs [fst_conv,snd_conv] 1); |
|
115 val apply_pair = result(); |
|
116 |
|
117 goal Prod.thy "!! P a b c d. (%(a,b,c,d). P a b c d) A \ |
|
118 \ ==> P (fst A)(fst(snd A))(fst (snd (snd A)))(snd(snd(snd A)))"; |
|
119 bd (blow4 RS forw_subst) 1; |
|
120 by (afs [split_def] 1); |
|
121 val apply_quadr = result(); |
|
122 |
|
123 goal Prod.thy "!! A B x. x: A Times B ==> x = (fst x, snd x)"; |
|
124 br (surjective_pairing RS subst) 1; |
|
125 br refl 1; |
|
126 val surj_pair_forw = result(); |
|
127 |
|
128 goal Prod.thy "!! A B x. x: A Times B ==> fst x: A"; |
|
129 by (forward_tac [surj_pair_forw] 1); |
|
130 bd forw_ssubst 1; |
|
131 ba 1; |
|
132 be SigmaD1 1; |
|
133 val TimesE1 = result(); |
|
134 |
|
135 goal Prod.thy "!! A B x. x: A Times B ==> snd x: B"; |
|
136 by (forward_tac [surj_pair_forw] 1); |
|
137 bd forw_ssubst 1; |
|
138 ba 1; |
|
139 be SigmaD2 1; |
|
140 val TimesE2 = result(); |
|
141 |
|
142 (* -> and Pi *) |
|
143 |
|
144 goal PiSets.thy "!! A B. A -> B == {f. ! x. if x: A then f(x) : B else f(x) = (@ y. True)}"; |
|
145 by (simp_tac (simpset() addsimps [Pi_def]) 1); |
|
146 val funcset_def = result(); |
|
147 |
|
148 |
|
149 val [q1,q2] = goal PiSets.thy |
|
150 "[| !!x. x: A ==> f x: B x; !!x. x ~: A ==> f(x) = (@ y. True)|] ==> f: Pi A B"; |
|
151 by (rewrite_goals_tac [Pi_def]); |
|
152 br CollectI 1; |
|
153 br allI 1; |
|
154 by (case_tac "x : A" 1); |
|
155 br (if_P RS ssubst) 1; |
|
156 ba 1; |
|
157 be q1 1; |
|
158 br (if_not_P RS ssubst) 1; |
|
159 ba 1; |
|
160 be q2 1; |
|
161 val Pi_I = result(); |
|
162 |
|
163 goal PiSets.thy |
|
164 "!! A f. [| !!x. x: A ==> f x: B; !!x. x ~: A ==> f(x) = (@ y. True)|] ==> f: A -> B"; |
|
165 by (afs [Pi_I] 1); |
|
166 val funcsetI = result(); |
|
167 |
|
168 val [q1,q2,q3] = goal PiSets.thy |
|
169 "[| !! x y. [| x: A; y: B |] ==> f x y: C; \ |
|
170 \ !! x. [| x ~: A |] ==> f x = (@ y. True);\ |
|
171 \ !! x y. [| x : A; y ~: B |] ==> f x y = (@ y. True) |] ==> f: A -> B -> C"; |
|
172 by (simp_tac (simpset() addsimps [q1,q2,q3,funcsetI]) 1); |
|
173 val funcsetI2 = result(); |
|
174 |
|
175 goal PiSets.thy "!! f A B. [|f: A -> B; x: A|] ==> f x: B"; |
|
176 by (afs [funcset_def] 1); |
|
177 val funcsetE1 = result(); |
|
178 |
|
179 goal PiSets.thy "!! f A B. [|f: Pi A B; x: A|] ==> f x: B x"; |
|
180 by (afs [Pi_def] 1); |
|
181 val PiE1 = result(); |
|
182 |
|
183 goal PiSets.thy "!! f A B. [|f: A -> B; x~: A|] ==> f x = (@ y. True)"; |
|
184 by (afs [funcset_def] 1); |
|
185 val funcsetE2 = result(); |
|
186 |
|
187 goal PiSets.thy "!! f A B. [|f: Pi A B; x~: A|] ==> f x = (@ y. True)"; |
|
188 by (afs [Pi_def] 1); |
|
189 val PiE2 = result(); |
|
190 |
|
191 goal PiSets.thy "!! f A B. [|f: A -> B -> C; x : A; y ~: B|] ==> f x y = (@ y. True)"; |
|
192 by (afs [funcset_def] 1); |
|
193 val funcset2E2 = result(); |
|
194 |
|
195 |
|
196 goal PiSets.thy "!! f A B C. [| f: A -> B -> C; x: A; y: B |] ==> f x y: C"; |
|
197 by (afs [funcset_def] 1); |
|
198 val funcset2E1 = result(); |
|
199 |
|
200 goal PiSets.thy "!! f g A B. [| f: A -> B; g: A -> B; ! x: A. f x = g x |]\ |
|
201 \ ==> f = g"; |
|
202 br ext 1; |
|
203 by (case_tac "x : A" 1); |
|
204 by (Fast_tac 1); |
|
205 by (fast_tac (claset() addSDs [funcsetE2] addEs [ssubst]) 1); |
|
206 val function_extensionality = result(); |
|
207 |
|
208 goal PiSets.thy "!! f g A B. [| f: Pi A B; g: Pi A B; ! x: A. f x = g x |]\ |
|
209 \ ==> f = g"; |
|
210 br ext 1; |
|
211 by (case_tac "x : A" 1); |
|
212 by (Fast_tac 1); |
|
213 by (fast_tac (claset() addSDs [PiE2] addEs [ssubst]) 1); |
|
214 val Pi_extensionality = result(); |
|
215 |
|
216 (* compose *) |
|
217 goal PiSets.thy "!! A B C f g. [| f: A -> B; g: B -> C |]==> compose A g f: A -> C"; |
|
218 br funcsetI 1; |
|
219 by (rewrite_goals_tac [compose_def,restrict_def]); |
|
220 by (afs [funcsetE1] 1); |
|
221 br (if_not_P RS ssubst) 1; |
|
222 ba 1; |
|
223 br refl 1; |
|
224 val funcset_compose = result(); |
|
225 |
|
226 goal PiSets.thy "!! A B C f g h. [| f: A -> B; g: B -> C; h: C -> D |]\ |
|
227 \ ==> compose A h (compose A g f) = compose A (compose B h g) f"; |
|
228 by (res_inst_tac [("A","A")] function_extensionality 1); |
|
229 br funcset_compose 1; |
|
230 br funcset_compose 1; |
|
231 ba 1; |
|
232 ba 1; |
|
233 ba 1; |
|
234 br funcset_compose 1; |
|
235 ba 1; |
|
236 br funcset_compose 1; |
|
237 ba 1; |
|
238 ba 1; |
|
239 br ballI 1; |
|
240 by (rewrite_goals_tac [compose_def,restrict_def]); |
|
241 by (afs [funcsetE1,if_P RS ssubst] 1); |
|
242 val compose_assoc = result(); |
|
243 |
|
244 goal PiSets.thy "!! A B C f g x. [| f: A -> B; g: B -> C; x: A |]==> compose A g f x = g(f(x))"; |
|
245 by (afs [compose_def, restrict_def, if_P RS ssubst] 1); |
|
246 val composeE1 = result(); |
|
247 |
|
248 goal PiSets.thy "!! A B C g f.[| f : A -> B; f `` A = B; g: B -> C; g `` B = C |]\ |
|
249 \ ==> compose A g f `` A = C"; |
|
250 br equalityI 1; |
|
251 br subsetI 1; |
|
252 be imageE 1; |
|
253 by (rotate_tac 4 1); |
|
254 be ssubst 1; |
|
255 br (funcset_compose RS funcsetE1) 1; |
|
256 ba 1; |
|
257 ba 1; |
|
258 ba 1; |
|
259 br subsetI 1; |
|
260 by (hyp_subst_tac 1); |
|
261 be imageE 1; |
|
262 by (rotate_tac 3 1); |
|
263 be ssubst 1; |
|
264 be imageE 1; |
|
265 by (rotate_tac 3 1); |
|
266 be ssubst 1; |
|
267 be (composeE1 RS subst) 1; |
|
268 ba 1; |
|
269 ba 1; |
|
270 br imageI 1; |
|
271 ba 1; |
|
272 val surj_compose = result(); |
|
273 |
|
274 |
|
275 goal PiSets.thy "!! A B C g f.[| f : A -> B; g: B -> C; f `` A = B; inj_on f A; inj_on g B |]\ |
|
276 \ ==> inj_on (compose A g f) A"; |
|
277 br inj_onI 1; |
|
278 by (forward_tac [composeE1] 1); |
|
279 ba 1; |
|
280 ba 1; |
|
281 by (forward_tac [composeE1] 1); |
|
282 ba 1; |
|
283 by (rotate_tac 7 1); |
|
284 ba 1; |
|
285 by (step_tac (claset() addSEs [inj_onD]) 1); |
|
286 by (rotate_tac 5 1); |
|
287 be subst 1; |
|
288 be subst 1; |
|
289 ba 1; |
|
290 be imageI 1; |
|
291 be imageI 1; |
|
292 val inj_on_compose = result(); |
|
293 |
|
294 |
|
295 (* restrict / lam *) |
|
296 goal PiSets.thy "!! f A B. [| f `` A <= B |] ==> (lam x: A. f x) : A -> B"; |
|
297 by (rewrite_goals_tac [restrict_def]); |
|
298 br funcsetI 1; |
|
299 by (afs [if_P RS ssubst] 1); |
|
300 be subsetD 1; |
|
301 be imageI 1; |
|
302 by (afs [if_not_P RS ssubst] 1); |
|
303 val restrict_in_funcset = result(); |
|
304 |
|
305 goal PiSets.thy "!! f A B. [| ! x: A. f x: B |] ==> (lam x: A. f x) : A -> B"; |
|
306 br restrict_in_funcset 1; |
|
307 by (afs [image_def] 1); |
|
308 by (Step_tac 1); |
|
309 by (Fast_tac 1); |
|
310 val restrictI = result(); |
|
311 |
|
312 goal PiSets.thy "!! f A B. [| ! x: A. f x: B x |] ==> (lam x: A. f x) : Pi A B"; |
|
313 by (rewrite_goals_tac [restrict_def]); |
|
314 br Pi_I 1; |
|
315 by (afs [if_P RS ssubst] 1); |
|
316 by (Asm_full_simp_tac 1); |
|
317 val restrictI_Pi = result(); |
|
318 |
|
319 (* The following proof has to be redone *) |
|
320 goal PiSets.thy "!! f A B C.[| f `` A <= B -> C |] ==> (lam x: A. lam y: B. f x y) : A -> B -> C"; |
|
321 br restrict_in_funcset 1; |
|
322 by (afs [image_def] 1); |
|
323 by (afs [Pi_def,subset_def] 1); |
|
324 by (afs [restrict_def] 1); |
|
325 by (Step_tac 1); |
|
326 by (Asm_full_simp_tac 1); |
|
327 by (dres_inst_tac [("x","f xa")] spec 1); |
|
328 bd mp 1; |
|
329 br bexI 1; |
|
330 br refl 1; |
|
331 ba 1; |
|
332 by (dres_inst_tac [("x","xb")] spec 1); |
|
333 by (Asm_full_simp_tac 1); |
|
334 (* fini 1 *) |
|
335 by (Asm_full_simp_tac 1); |
|
336 val restrict_in_funcset2 = result(); |
|
337 |
|
338 goal PiSets.thy "!! f A B C.[| !x: A. ! y: B. f x y: C |] ==> (lam x: A. lam y: B. f x y) : A -> B -> C"; |
|
339 br restrict_in_funcset 1; |
|
340 by (afs [image_def] 1); |
|
341 by (afs [Pi_def,subset_def] 1); |
|
342 by (afs [restrict_def] 1); |
|
343 by (Step_tac 1); |
|
344 by (Asm_full_simp_tac 1); |
|
345 by (Asm_full_simp_tac 1); |
|
346 val restrictI2 = result(); |
|
347 |
|
348 |
|
349 (* goal PiSets.thy "!! f A B. [| f `` A <= UNION A B |] ==> (lam x: A. f x) : Pi A B"; *) |
|
350 |
|
351 goal PiSets.thy "!! f A B. [| x: A |] ==> (lam y: A. f y) x = f x"; |
|
352 by (afs [restrict_def] 1); |
|
353 val restrictE1 = result(); |
|
354 |
|
355 goal PiSets.thy "!! f A B. [| x: A; f : A -> B |] ==> (lam y: A. f y) x : B"; |
|
356 by (afs [restrictE1,funcsetE1] 1); |
|
357 val restrictE1a = result(); |
|
358 |
|
359 goal PiSets.thy "!! f A B. [| x ~: A |] ==> (lam y: A. f y) x = (@ y. True)"; |
|
360 by (afs [restrict_def] 1); |
|
361 val restrictE2 = result(); |
|
362 |
|
363 (* It would be nice to have this, but this doesn't work unfortunately |
|
364 see PiSets.ML: Pi_subset1 |
|
365 goal PiSets.thy "!! A B. [| A <= B ; ! x: A. f x : C|] ==> (lam x: B. f(x)): A -> C"; *) |
|
366 |
|
367 goal PiSets.thy "!! f A B x y. [| x: A; y: B |] ==> \ |
|
368 \ (lam a: A. lam b: B. f a b) x y = f x y"; |
|
369 by (afs [restrictE1] 1); |
|
370 val restrict2E1 = result(); |
|
371 |
|
372 (* New restrict2E1: *) |
|
373 goal PiSets.thy "!! A B. [| x : A; y : B x|] ==> (lam a:A. lam b: (B a). f a b) x y = f x y" ; |
|
374 by (afs [restrictE1] 1); |
|
375 val restrict2E1a = result(); |
|
376 |
|
377 goal PiSets.thy "!! f A B x y. [| x: A; y: B; z: C |] ==> \ |
|
378 \ (lam a: A. lam b: B. lam c: C. f a b c) x y z = f x y z"; |
|
379 by (afs [restrictE1] 1); |
|
380 val restrict3E1 = result(); |
|
381 |
|
382 goal PiSets.thy "!! f A B x y. [| x: A; y ~: B |] ==> \ |
|
383 \ (lam a: A. lam b: B. f a b) x y = (@ y. True)"; |
|
384 by (afs [restrictE1,restrictE2] 1); |
|
385 val restrict2E2 = result(); |
|
386 |
|
387 |
|
388 goal PiSets.thy "!! f g A B. [| ! x: A. f x = g x |]\ |
|
389 \ ==> (lam x: A. f x) = (lam x: A. g x)"; |
|
390 br ext 1; |
|
391 by (case_tac "x: A" 1); |
|
392 by (afs [restrictE1] 1); |
|
393 by (afs [restrictE2] 1); |
|
394 val restrict_ext = result(); |
|
395 |
|
396 (* Invers *) |
|
397 |
|
398 goal PiSets.thy "!! f A B.[|f `` A = B; x: B |] ==> ? y: A. f y = x"; |
|
399 by (rewrite_goals_tac [image_def]); |
|
400 bd equalityD2 1; |
|
401 bd subsetD 1; |
|
402 ba 1; |
|
403 bd CollectD 1; |
|
404 be bexE 1; |
|
405 bd sym 1; |
|
406 be bexI 1; |
|
407 ba 1; |
|
408 val surj_image = result(); |
|
409 |
|
410 val [q1,q2] = goal PiSets.thy "[| f `` A = B; f : A -> B |] \ |
|
411 \ ==> (lam x: B. (Inv A f) x) : B -> A"; |
|
412 br restrict_in_funcset 1; |
|
413 by (rewrite_goals_tac [image_def]); |
|
414 br subsetI 1; |
|
415 bd CollectD 1; |
|
416 be bexE 1; |
|
417 be ssubst 1; |
|
418 bd (q1 RS surj_image) 1; |
|
419 be bexE 1; |
|
420 be subst 1; |
|
421 by (rewrite_goals_tac [Inv_def]); |
|
422 by (res_inst_tac [("Q","f(@ ya. ya : A & f ya = f y) = f y")] conjunct1 1); |
|
423 br (q1 RS surj_image RS (Bex_def RS apply_def) RS (Ex_def RS apply_def)) 1; |
|
424 be (q2 RS funcsetE1) 1; |
|
425 val Inv_funcset = result(); |
|
426 |
|
427 |
|
428 val [q1,q2,q3] = goal PiSets.thy "[| f: A -> B; inj_on f A; f `` A = B |]\ |
|
429 \ ==> ! x: A. (lam y: B. (Inv A f) y)(f x) = x"; |
|
430 br ballI 1; |
|
431 br (restrictE1 RS ssubst) 1; |
|
432 be (q1 RS funcsetE1) 1; |
|
433 by (rewrite_goals_tac [Inv_def]); |
|
434 br (q2 RS inj_onD) 1; |
|
435 ba 3; |
|
436 by (res_inst_tac [("P","(@ y. y : A & f y = f x) : A")] conjunct2 1); |
|
437 br (q3 RS surj_image RS (Bex_def RS apply_def) RS (Ex_def RS apply_def)) 1; |
|
438 be (q1 RS funcsetE1) 1; |
|
439 by (res_inst_tac [("Q","f (@ y. y : A & f y = f x) = f x")] conjunct1 1); |
|
440 br (q3 RS surj_image RS (Bex_def RS apply_def) RS (Ex_def RS apply_def)) 1; |
|
441 be (q1 RS funcsetE1) 1; |
|
442 val Inv_f_f = result(); |
|
443 |
|
444 val [q1,q2] = goal PiSets.thy "[| f: A -> B; f `` A = B |]\ |
|
445 \ ==> ! x: B. f ((lam y: B. (Inv A f y)) x) = x"; |
|
446 br ballI 1; |
|
447 br (restrictE1 RS ssubst) 1; |
|
448 ba 1; |
|
449 by (rewrite_goals_tac [Inv_def]); |
|
450 by (res_inst_tac [("P","(@ y. y : A & f y = x) : A")] conjunct2 1); |
|
451 br (q2 RS surj_image RS (Bex_def RS apply_def) RS (Ex_def RS apply_def)) 1; |
|
452 ba 1; |
|
453 val f_Inv_f = result(); |
|
454 |
|
455 val [q1,q2,q3] = goal PiSets.thy "[| f: A -> B; inj_on f A; f `` A = B |]\ |
|
456 \ ==> compose A (lam y:B. (Inv A f) y) f = (lam x: A. x)"; |
|
457 br function_extensionality 1; |
|
458 br funcset_compose 1; |
|
459 br q1 1; |
|
460 br (q1 RS (q3 RS Inv_funcset)) 1; |
|
461 br restrict_in_funcset 1; |
|
462 by (Fast_tac 1); |
|
463 br ballI 1; |
|
464 by (afs [compose_def] 1); |
|
465 br (restrictE1 RS ssubst) 1; |
|
466 ba 1; |
|
467 br (restrictE1 RS ssubst) 1; |
|
468 ba 1; |
|
469 be (q3 RS (q2 RS (q1 RS Inv_f_f)) RS bspec) 1; |
|
470 val comp_Inv_id = result(); |
|
471 |
|
472 |
|
473 (* Pi and its application @@ *) |
|
474 |
|
475 goal PiSets.thy "!! A B. (PI x: A. B x) ~= {} ==> ! x: A. B(x) ~= {}"; |
|
476 bd NotEmpty_ExEl 1; |
|
477 be exE 1; |
|
478 by (rewrite_goals_tac [Pi_def]); |
|
479 bd CollectD 1; |
|
480 br ballI 1; |
|
481 br ExEl_NotEmpty 1; |
|
482 by (res_inst_tac [("x","x xa")] exI 1); |
|
483 by (afs [if_P RS subst] 1); |
|
484 val Pi_total1 = result(); |
|
485 |
|
486 goal Set.thy "!! M P. ? x: M . P x ==> (~ (! x: M. ~ P x))"; |
|
487 by (Fast_tac 1); |
|
488 val SetEx_NotNotAll = result(); |
|
489 |
|
490 goal PiSets.thy "!! A B. ? x: A. B(x) = {} ==> (PI x: A. B x) = {}"; |
|
491 br notnotD 1; |
|
492 br (Pi_total1 RSN(2,contrapos)) 1; |
|
493 ba 2; |
|
494 be SetEx_NotNotAll 1; |
|
495 val Pi_total2 = result(); |
|
496 |
|
497 val [q1,q2] = goal PiSets.thy "[|a : A; Pi A B ~= {} |] ==> (Pi A B) @@ a = B(a)"; |
|
498 by (rewrite_goals_tac [Fset_apply_def]); |
|
499 br equalityI 1; |
|
500 br subsetI 1; |
|
501 be imageE 1; |
|
502 be ssubst 1; |
|
503 by (rewrite_goals_tac [Pi_def]); |
|
504 bd CollectD 1; |
|
505 bd spec 1; |
|
506 br (q1 RS if_P RS subst) 1; |
|
507 ba 1; |
|
508 br subsetI 1; |
|
509 by (rewrite_goals_tac [image_def]); |
|
510 br CollectI 1; |
|
511 br exE 1; |
|
512 br (q2 RS NotEmpty_ExEl) 1; |
|
513 by (res_inst_tac [("x","%y. if (y = a) then x else xa y")] bexI 1); |
|
514 by (Simp_tac 1); |
|
515 by (Simp_tac 1); |
|
516 br allI 1; |
|
517 by (case_tac "xb: A" 1); |
|
518 by (afs [if_P RS ssubst] 1); |
|
519 by (case_tac "xb = a" 1); |
|
520 by (afs [if_P RS ssubst] 1); |
|
521 by (afs [if_not_P RS ssubst] 1); |
|
522 by (rewrite_goals_tac [Pi_def]); |
|
523 by (afs [if_P RS ssubst] 1); |
|
524 by (afs [if_not_P RS ssubst] 1); |
|
525 by (case_tac "xb = a" 1); |
|
526 by (afs [if_P RS ssubst] 1); |
|
527 by (hyp_subst_tac 1); |
|
528 by (afs [q1] 1); |
|
529 by (afs [if_not_P RS ssubst] 1); |
|
530 val Pi_app_def = result(); |
|
531 |
|
532 goal PiSets.thy "!! a A B C. [| a: A; (PI x: A. PI y: B x. C x y) ~= {} |] ==> (PI y: B a. C a y) ~= {}"; |
|
533 bd NotEmpty_ExEl 1; |
|
534 be exE 1; |
|
535 by (rewrite_goals_tac [Pi_def]); |
|
536 bd CollectD 1; |
|
537 bd spec 1; |
|
538 br ExEl_NotEmpty 1; |
|
539 br exI 1; |
|
540 be (if_P RS eq_reflection RS apply_def) 1; |
|
541 ba 1; |
|
542 val NotEmptyPiStep = result(); |
|
543 |
|
544 val [q1,q2,q3] = goal PiSets.thy |
|
545 "[|a : A; b: B a; (PI x: A. PI y: B x. C x y) ~= {} |] ==> (PI x: A. PI y: B x. C x y) @@ a @@ b = C a b"; |
|
546 by (fold_goals_tac [q3 RS (q1 RS NotEmptyPiStep) RS (q2 RS Pi_app_def) RS eq_reflection]); |
|
547 by (fold_goals_tac [q3 RS (q1 RS Pi_app_def) RS eq_reflection]); |
|
548 br refl 1; |
|
549 val Pi_app2_def = result(); |
|
550 |
|
551 (* Sigma does a better job ( the following is from PiSig.ML) *) |
|
552 goal PiSets.thy "!! A b a. [| a: A; Pi A B ~= {} |]\ |
|
553 \ ==> Sigma A B ^^ {a} = Pi A B @@ a"; |
|
554 br (Pi_app_def RS ssubst) 1; |
|
555 ba 1; |
|
556 ba 1; |
|
557 by (afs [Sigma_def,Domain_def,converse_def,Range_def,Image_def] 1); |
|
558 by (rewrite_goals_tac [Bex_def]); |
|
559 by (Fast_tac 1); |
|
560 val PiSig_image_eq = result(); |
|
561 |
|
562 goal PiSets.thy "!! A b a. [| a: A |]\ |
|
563 \ ==> Sigma A B ^^ {a} = B a"; |
|
564 by (Fast_tac 1); |
|
565 val Sigma_app_def = result(); |
|
566 |
|
567 (* Bijection between Pi in terms of => and Pi in terms of Sigma *) |
|
568 goal PiSets.thy "!! f. f: Pi A B ==> PiBij A B f <= Sigma A B"; |
|
569 by (afs [PiBij_def,Pi_def,restrictE1] 1); |
|
570 br subsetI 1; |
|
571 by (split_all_tac 1); |
|
572 bd CollectD 1; |
|
573 by (Asm_full_simp_tac 1); |
|
574 val PiBij_subset_Sigma = result(); |
|
575 |
|
576 goal PiSets.thy "!! f. f: Pi A B ==> (! x: A. (?! y. (x, y): (PiBij A B f)))"; |
|
577 by (afs [PiBij_def,restrictE1] 1); |
|
578 br ballI 1; |
|
579 br ex1I 1; |
|
580 ba 2; |
|
581 br refl 1; |
|
582 val PiBij_unique = result(); |
|
583 |
|
584 goal PiSets.thy "!! f. f: Pi A B ==> (! x: A. (?! y. y: B x & (x, y): (PiBij A B f)))"; |
|
585 by (afs [PiBij_def,restrictE1] 1); |
|
586 br ballI 1; |
|
587 br ex1I 1; |
|
588 be conjunct2 2; |
|
589 by (afs [PiE1] 1); |
|
590 val PiBij_unique2 = result(); |
|
591 |
|
592 goal PiSets.thy "!! f. f: Pi A B ==> PiBij A B f : Graph A B"; |
|
593 by (afs [Graph_def,PiBij_unique,PiBij_subset_Sigma] 1); |
|
594 val PiBij_in_Graph = result(); |
|
595 |
|
596 goal PiSets.thy "!! A B. PiBij A B: Pi A B -> Graph A B"; |
|
597 by (afs [PiBij_def] 1); |
|
598 br restrictI 1; |
|
599 by (strip 1); |
|
600 by (afs [Graph_def] 1); |
|
601 br conjI 1; |
|
602 br subsetI 1; |
|
603 by (strip 2); |
|
604 br ex1I 2; |
|
605 br refl 2; |
|
606 ba 2; |
|
607 by (split_all_tac 1); |
|
608 by (afs [Pi_def] 1); |
|
609 val PiBij_func = result(); |
|
610 |
|
611 goal PiSets.thy "!! A f g x. [| f: Pi A B; g: Pi A B; \ |
|
612 \ {(x, y). x: A & y = f x} = {(x, y). x: A & y = g x}; x: A |]\ |
|
613 \ ==> f x = g x"; |
|
614 be equalityE 1; |
|
615 by (rewrite_goals_tac [subset_def]); |
|
616 by (dres_inst_tac [("x","(x, f x)")] bspec 1); |
|
617 by (Fast_tac 1); |
|
618 by (Fast_tac 1); |
|
619 val set_eq_lemma = result(); |
|
620 |
|
621 goal PiSets.thy "!! A B. inj_on (PiBij A B) (Pi A B)"; |
|
622 br inj_onI 1; |
|
623 br Pi_extensionality 1; |
|
624 ba 1; |
|
625 ba 1; |
|
626 by (strip 1); |
|
627 by (afs [PiBij_def,restrictE1] 1); |
|
628 by (re_tac set_eq_lemma 2 1); |
|
629 ba 1; |
|
630 ba 2; |
|
631 by (afs [restrictE1] 1); |
|
632 be subst 1; |
|
633 by (afs [restrictE1] 1); |
|
634 val inj_PiBij = result(); |
|
635 |
|
636 goal HOL.thy "!! P . ?! x. P x ==> ? x. P x"; |
|
637 by (Blast_tac 1); |
|
638 val Ex1_Ex = result(); |
|
639 |
|
640 goal PiSets.thy "!!A B. PiBij A B `` (Pi A B) = Graph A B"; |
|
641 br equalityI 1; |
|
642 by (afs [image_def] 1); |
|
643 br subsetI 1; |
|
644 by (Asm_full_simp_tac 1); |
|
645 be bexE 1; |
|
646 be ssubst 1; |
|
647 by (afs [PiBij_in_Graph] 1); |
|
648 br subsetI 1; |
|
649 by (afs [image_def] 1); |
|
650 by (res_inst_tac [("x","lam a: A. @ y. (a, y): x")] bexI 1); |
|
651 br restrictI_Pi 2; |
|
652 by (strip 2); |
|
653 br ex1E 2; |
|
654 by (afs [Graph_def] 2); |
|
655 be conjE 2; |
|
656 bd bspec 2; |
|
657 ba 2; |
|
658 ba 2; |
|
659 br (select_equality RS ssubst) 2; |
|
660 ba 2; |
|
661 by (Blast_tac 2); |
|
662 (* gets hung up on by (afs [Graph_def] 2); *) |
|
663 by (SELECT_GOAL (rewrite_goals_tac [Graph_def]) 2); |
|
664 by (Blast_tac 2); |
|
665 (* x = PiBij A B (lam a:A. @ y. (a, y) : x) *) |
|
666 by (afs [PiBij_def,Graph_def] 1); |
|
667 br (restrictE1 RS ssubst) 1; |
|
668 br restrictI_Pi 1; |
|
669 (* again like the old 2. subgoal *) |
|
670 by (strip 1); |
|
671 br ex1E 1; |
|
672 be conjE 1; |
|
673 bd bspec 1; |
|
674 ba 1; |
|
675 ba 1; |
|
676 br (select_equality RS ssubst) 1; |
|
677 ba 1; |
|
678 by (Blast_tac 1); |
|
679 by (Blast_tac 1); |
|
680 (* *) |
|
681 br equalityI 1; |
|
682 br subsetI 1; |
|
683 br CollectI 1; |
|
684 by (split_all_tac 1); |
|
685 by (Simp_tac 1); |
|
686 br conjI 1; |
|
687 by (Blast_tac 1); |
|
688 be conjE 1; |
|
689 bd subsetD 1; |
|
690 ba 1; |
|
691 bd SigmaD1 1; |
|
692 bd bspec 1; |
|
693 ba 1; |
|
694 br (restrictE1 RS ssubst) 1; |
|
695 ba 1; |
|
696 br sym 1; |
|
697 br select_equality 1; |
|
698 ba 1; |
|
699 by (Blast_tac 1); |
|
700 (* {(xa,y). xa : A & y = (lam a:A. @ y. (a, y) : x) xa} <= x *) |
|
701 br subsetI 1; |
|
702 by (Asm_full_simp_tac 1); |
|
703 by (split_all_tac 1); |
|
704 by (Asm_full_simp_tac 1); |
|
705 be conjE 1; |
|
706 be conjE 1; |
|
707 by (afs [restrictE1] 1); |
|
708 bd bspec 1; |
|
709 ba 1; |
|
710 bd Ex1_Ex 1; |
|
711 by (rewrite_goals_tac [Ex_def]); |
|
712 ba 1; |
|
713 val surj_PiBij = result(); |
|
714 |
|
715 |
|
716 goal PiSets.thy "!! A B. [| f: Pi A B |] ==> \ |
|
717 \ (lam y: Graph A B. (Inv (Pi A B)(PiBij A B)) y)(PiBij A B f) = f"; |
|
718 br (Inv_f_f RS bspec) 1; |
|
719 ba 4; |
|
720 by (afs [PiBij_func] 1); |
|
721 by (afs [inj_PiBij] 1); |
|
722 by (afs [surj_PiBij] 1); |
|
723 val PiBij_bij1 = result(); |
|
724 |
|
725 goal PiSets.thy "!! A B. [| f: Graph A B |] ==> \ |
|
726 \ (PiBij A B) ((lam y: (Graph A B). (Inv (Pi A B)(PiBij A B)) y) f) = f"; |
|
727 br (PiBij_func RS (f_Inv_f RS bspec)) 1; |
|
728 by (afs [surj_PiBij] 1); |
|
729 ba 1; |
|
730 val PiBij_bij2 = result(); |
|
731 |
|
732 goal PiSets.thy "!! g f. [| ! x. g( f x) = x |] ==> inj f"; |
|
733 br injI 1; |
|
734 by (dres_inst_tac [("f","g")] arg_cong 1); |
|
735 by (forw_inst_tac [("x","x")] spec 1); |
|
736 by (rotate_tac 2 1); |
|
737 be subst 1; |
|
738 by (forw_inst_tac [("x","y")] spec 1); |
|
739 by (rotate_tac 2 1); |
|
740 be subst 1; |
|
741 ba 1; |
|
742 val inj_lemma = result(); |
|
743 |
|
744 goal PiSets.thy "!! g f. [| ! x. g( f x) = x |] ==> surj g"; |
|
745 by (afs [surj_def] 1); |
|
746 br allI 1; |
|
747 by (res_inst_tac [("x","f y")] exI 1); |
|
748 bd spec 1; |
|
749 be sym 1; |
|
750 val surj_lemma = result(); |
|
751 |
|
752 goal PiSets.thy "Pi {} B == {f. !x. f x = (@ y. True)}"; |
|
753 by (afs [Pi_def] 1); |
|
754 val empty_Pi = result(); |
|
755 |
|
756 goal PiSets.thy "(% x. (@ y. True)) : Pi {} B"; |
|
757 by (afs [empty_Pi] 1); |
|
758 val empty_Pi_func = result(); |
|
759 |
|
760 goal Set.thy "!! A B. [| A <= B; x ~: B |] ==> x ~: A"; |
|
761 by (Blast_tac 1); |
|
762 val subsetND = result(); |
|
763 |
|
764 |
|
765 goal PiSets.thy "!! A B C . [| ! x: A. B x <= C x |] ==> Pi A B <= Pi A C"; |
|
766 br subsetI 1; |
|
767 br Pi_I 1; |
|
768 by (afs [Pi_def] 2); |
|
769 bd bspec 1; |
|
770 ba 1; |
|
771 be subsetD 1; |
|
772 by (afs [PiE1] 1); |
|
773 val Pi_subset1 = result(); |