simpleSetCatScript.sml
1Theory simpleSetCat
2Ancestors
3 relation combin pred_set cardinal
4
5val _ = app (ignore o hide) ["S", "W"]
6
7
8Definition restr_def:
9 restr f s = \x. if x IN s then f x else ARB
10End
11
12Theorem restr_applies:
13 x IN A ==> (restr f A x = f x)
14Proof
15 simp[restr_def]
16QED
17
18Theorem IN_UNCURRY[simp]:
19 (a,b) IN UNCURRY R <=> R a b
20Proof
21 simp[IN_DEF]
22QED
23Definition Delta_def[simp]:
24 Delta V a b <=> a = b /\ a IN V
25End
26Overload "Δ" = “Delta”
27
28Theorem Delta_INTER:
29 Delta (s INTER t) = Delta s RINTER Delta t
30Proof
31 simp[FUN_EQ_THM, RINTER] >> metis_tac[]
32QED
33
34
35Definition Gr_def[simp]:
36 Gr h A a b <=> a IN A /\ b = h a
37End
38
39Theorem Gr_Id[simp]:
40 Gr (\x. x) A = Delta A
41Proof
42 csimp[FUN_EQ_THM] >> metis_tac[]
43QED
44
45Theorem Gr_restr[simp]:
46 Gr (restr f A) A = Gr f A
47Proof
48 csimp[FUN_EQ_THM, restr_def]
49QED
50
51
52Definition span_def[simp]:
53 span A f g b d <=> ?a. a IN A /\ b = f a /\ d = g a
54End
55
56Definition kernel_def[simp]:
57 kernel A f x y <=> x IN A /\ y IN A /\ f x = f y
58End
59
60Theorem kernel_graph:
61 kernel A f = inv (Gr f A) O Gr f A
62Proof
63 simp[FUN_EQ_THM, O_DEF]
64QED
65
66
67Definition RIMAGE_def:
68 RIMAGE f A R x y <=>
69 ?x0 y0. x = f x0 /\ y = f y0 /\ R x0 y0 /\ x0 IN A /\ y0 IN A
70End
71
72Definition RINV_IMAGE_def:
73 RINV_IMAGE f A R x y <=> x IN A /\ y IN A /\ R (f x) (f y)
74End
75
76Theorem RIMAGE_Gr:
77 RIMAGE f A R = Gr f A O R O inv (Gr f A)
78Proof
79 dsimp[FUN_EQ_THM, O_DEF, IN_DEF, PULL_EXISTS, RIMAGE_def] >>
80 metis_tac[]
81QED
82
83Theorem Delta_IMAGE:
84 Delta (IMAGE f A) = RIMAGE f A (Delta A)
85Proof
86 simp[FUN_EQ_THM, PULL_EXISTS, RIMAGE_def] >> metis_tac[]
87QED
88
89Theorem RINV_IMAGE_Gr:
90 RINV_IMAGE f A R = inv (Gr f A) O R O Gr f A
91Proof
92 dsimp[FUN_EQ_THM, O_DEF, RINV_IMAGE_def] >> metis_tac[]
93QED
94
95Theorem restr_restr_o[simp]:
96 restr (f o restr g A) A = restr (f o g) A
97Proof
98 simp[restr_def, FUN_EQ_THM]
99QED
100
101Theorem restr_cases:
102 restr f A x = g x <=> x IN A /\ f x = g x \/ x NOTIN A /\ g x = ARB
103Proof
104 simp[restr_def] >> metis_tac[]
105QED
106
107
108Theorem oID[simp]:
109 f o (\x.x) = f /\ (\x.x) o f = f
110Proof
111 simp[FUN_EQ_THM]
112QED
113
114Definition shom_def:
115 shom f A B <=> (!a. a IN A ==> f a IN B) /\ !a. a NOTIN A ==> f a = ARB
116End
117
118(* pushouts in Set *)
119
120Definition Spushout_def:
121 Spushout (A:'a set) (B:'b set) (C:'c set) f g (P:'p set,i1,i2) (:'d) <=>
122 shom f A B /\ shom g A C /\ shom i1 B P /\ shom i2 C P /\
123 restr (i1 o f) A = restr (i2 o g) A /\
124 !(Q:'d set) j1 j2.
125 shom j1 B Q /\ shom j2 C Q /\ restr (j1 o f) A = restr (j2 o g) A ==>
126 ?!u. shom u P Q /\ restr (u o i1) B = j1 /\ restr (u o i2) C = j2
127End
128
129Definition SPO_pimg_def[simp]:
130 SPO_pimg A f g (INL x) = PREIMAGE f {x} INTER A /\
131 SPO_pimg A f g (INR y) = PREIMAGE g {y} INTER A
132End
133
134Definition SPOr_def:
135 SPOr A f g = EQC (\x y. (?a. a IN A /\ x = INL (f a) /\ y = INR (g a)) \/
136 x = y)
137End
138
139Definition SPO_def:
140 SPO A B C f g =
141 (partition (SPOr A f g) (B <+> C),
142 restr (\b. { a | a IN B <+> C /\ SPOr A f g (INL b) a }) B,
143 restr (\c. { a | a IN B <+> C /\ SPOr A f g (INR c) a }) C)
144End
145
146Theorem symmetric_SPOr[simp]:
147 symmetric (SPOr A f g)
148Proof
149 rw[SPOr_def, symmetric_EQC]
150QED
151
152Theorem transitive_SPOr[simp]:
153 transitive (SPOr A f g)
154Proof
155 simp[SPOr_def, transitive_EQC]
156QED
157
158Theorem SPOr_lemma0[local]:
159 restr (j1 o f) A = restr (j2 o g) A ==>
160 !s1 s2. SPOr A f g s1 s2 ==>
161 (!b1 b2. s1 = INL b1 /\ s2 = INL b2 ==> j1 b1 = j1 b2) /\
162 (!b c. s1 = INL b /\ s2 = INR c ==> j1 b = j2 c) /\
163 (!b c. s1 = INR c /\ s2 = INL b ==> j1 b = j2 c) /\
164 (!c1 c2. s1 = INR c1 /\ s2 = INR c2 ==> j2 c1 = j2 c2)
165Proof
166 strip_tac >> simp[SPOr_def] >> Induct_on ‘EQC’ >> rw[]
167 >- (fs[restr_def, FUN_EQ_THM] >> metis_tac[])
168 >- (rename [‘EQC _ (INL b1) s’, ‘EQC _ s (INL b2)’] >>
169 Cases_on ‘s’ >> fs[])
170 >- (rename [‘EQC _ (INL b) s’, ‘EQC _ s (INR c)’] >>
171 Cases_on ‘s’ >> fs[])
172 >- (rename [‘EQC _ (INR c) s’, ‘EQC _ s (INL b)’] >>
173 Cases_on ‘s’ >> fs[])
174 >- (rename [‘EQC _ (INR c1) s’, ‘EQC _ s (INR c2)’] >>
175 Cases_on ‘s’ >> fs[])
176QED
177
178Theorem SPOr_lemma =
179 SPOr_lemma0 |> UNDISCH
180 |> SIMP_RULE (srw_ss()) [IMP_CONJ_THM, PULL_FORALL]
181 |> SIMP_RULE (srw_ss()) [FORALL_AND_THM]
182 |> DISCH_ALL
183
184Theorem SPOr_REFL[simp]:
185 SPOr A f g x x
186Proof
187 simp[SPOr_def]
188QED
189
190Theorem Spushout_quotient:
191 shom f A B /\ shom g A C ==>
192 Spushout (A:'a set) (B:'b set) (C:'c set) f g (SPO A B C f g) (:'d)
193Proof
194 simp[Spushout_def, SPO_def] >> rw[]
195 >- (simp[shom_def] >> reverse conj_tac >- simp[restr_def] >>
196 dsimp[restr_applies, partition_def] >> csimp[] >>
197 qx_gen_tac ‘b’ >> strip_tac >> qexists_tac ‘INL b’ >> simp[] >>
198 simp[EXTENSION] >>
199 ‘symmetric (SPOr A f g)’ suffices_by metis_tac[symmetric_def] >>
200 simp[])
201 >- (simp[shom_def] >> reverse conj_tac >- simp[restr_def] >>
202 dsimp[restr_applies, partition_def] >> csimp[] >>
203 qx_gen_tac ‘c’ >> strip_tac >>
204 qexists_tac ‘INR c’ >> simp[EXTENSION] >>
205 ‘symmetric (SPOr A f g)’ suffices_by metis_tac[symmetric_def] >>
206 simp[])
207 >- (simp[Once FUN_EQ_THM, restr_def] >> qx_gen_tac ‘a’ >> rw[]
208 >- (simp[Once EXTENSION] >> qx_gen_tac ‘s’ >>
209 ‘SPOr A f g (INL (f a)) (INR (g a)) /\ symmetric (SPOr A f g) /\
210 transitive (SPOr A f g)’
211 suffices_by metis_tac[symmetric_def, transitive_def] >>
212 simp[] >> simp[SPOr_def] >> irule EQC_R >> simp[] >> metis_tac[]) >>
213 metis_tac[shom_def]) >>
214 ONCE_REWRITE_TAC[FUN_EQ_THM] >>
215 simp[o_ABS_R] >> simp[EXISTS_UNIQUE_ALT] >>
216 qexists_tac ‘restr (\p. case some a. INL a IN p of
217 SOME a => j1 a
218 | NONE => j2 (CHOICE {b | INR b IN p}))
219 (partition (SPOr A f g) (B <+> C))’ >>
220 qx_gen_tac ‘u’ >>
221 reverse (Cases_on ‘shom u (partition (SPOr A f g) (B <+> C)) Q’)
222 >- (simp[] >> pop_assum mp_tac >> simp[shom_def] >> strip_tac
223 >- (ONCE_REWRITE_TAC [FUN_EQ_THM] >> simp[] >>
224 rename [‘a IN partition _ _’, ‘u a NOTIN Q’] >>
225 qexists_tac ‘a’ >> simp[restr_applies] >>
226 disch_then (assume_tac o SYM) >> fs[] >>
227 qpat_x_assum ‘_ NOTIN Q’ mp_tac >> simp[] >>
228 DEEP_INTRO_TAC optionTheory.some_intro >> simp[] >>
229 qpat_x_assum ‘_ IN partition _ _’ mp_tac >>
230 simp[partition_def, sumTheory.EXISTS_SUM] >> strip_tac >> rw[]
231 >- metis_tac[shom_def]
232 >- metis_tac[SPOr_REFL]
233 >- metis_tac[shom_def] >>
234 DEEP_INTRO_TAC CHOICE_INTRO >> simp[] >> conj_tac
235 >- metis_tac[SPOr_REFL] >>
236 metis_tac[shom_def]) >>
237 ONCE_REWRITE_TAC [FUN_EQ_THM] >> simp[]>> rename [‘u a <> ARB’] >>
238 qexists_tac ‘a’ >> simp[restr_def]) >>
239 ONCE_REWRITE_TAC [FUN_EQ_THM] >> simp[restr_cases] >>
240 ‘(!b. b NOTIN B ==> j1 b = ARB) /\ (!c. c NOTIN C ==> j2 c = ARB) /\
241 (!p. p NOTIN partition (SPOr A f g) (B <+> C) ==> u p = ARB)’
242 by metis_tac[shom_def] >> csimp[] >>
243 simp[DECIDE “p /\ q \/ ~p <=> q \/ ~p”] >>
244 simp[DECIDE “p \/ ~q <=> q ==> p”] >> eq_tac
245 >- (simp[partition_def, PULL_EXISTS, sumTheory.FORALL_SUM] >>
246 strip_tac >> qx_gen_tac ‘p’ >> conj_tac
247 >- (qx_gen_tac ‘b’>> rw[] >>
248 DEEP_INTRO_TAC optionTheory.some_intro >> reverse (rw[])
249 >- metis_tac[SPOr_REFL] >>
250 rename [‘SPOr _ _ _ (INL b1) (INL b2)’] >> Cases_on ‘b1 = b2’ >>
251 simp[] >> metis_tac[SPOr_lemma]) >>
252 qx_gen_tac ‘c’ >> rw[] >> DEEP_INTRO_TAC optionTheory.some_intro >> rw[]
253 >- metis_tac[SPOr_lemma] >>
254 DEEP_INTRO_TAC CHOICE_INTRO >> simp[] >>
255 metis_tac[SPOr_REFL, SPOr_lemma]) >>
256 simp[partition_def, PULL_EXISTS, sumTheory.FORALL_SUM, FORALL_AND_THM] >>
257 CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [EQ_SYM_EQ])) >> simp[] >>
258 disch_then (K ALL_TAC) >> rw[]
259 >- (DEEP_INTRO_TAC optionTheory.some_intro >> reverse (rw[])
260 >- metis_tac[SPOr_REFL] >> metis_tac[SPOr_lemma]) >>
261 DEEP_INTRO_TAC optionTheory.some_intro >> simp[] >> conj_tac
262 >- metis_tac[SPOr_lemma] >> strip_tac >>
263 DEEP_INTRO_TAC CHOICE_INTRO >> simp[] >> metis_tac[SPOr_REFL, SPOr_lemma]
264QED
265
266(* pushouts in Set into universe delta are pushouts into universe epsilon if
267 epsilon is no bigger than delta *)
268Theorem Spushout_transfer:
269 Spushout A B C f g (P,i1,i2) (:'d) /\ INJ h univ(:'e) univ(:'d) ==>
270 Spushout A B C f g (P,i1,i2) (:'e)
271Proof
272 rw[Spushout_def] >>
273 first_x_assum $ qspecl_then [‘IMAGE h Q’, ‘restr (h o j1) B’,
274 ‘restr (h o j2) C’] mp_tac >>
275 impl_tac
276 >- (fs[shom_def, restr_def, FUN_EQ_THM] >> metis_tac[INJ_IFF, IN_UNIV]) >>
277 simp[EXISTS_UNIQUE_THM] >> rw[]
278 >- (drule_then assume_tac LINV_DEF >> fs[] >>
279 qexists_tac ‘restr (LINV h univ(:'e) o u) P’>>
280 first_x_assum $ qspecl_then [‘ARB’, ‘ARB’] (K ALL_TAC) >>
281 fs[shom_def, FUN_EQ_THM, restr_def] >> rw[] >> metis_tac[]) >>
282 Q.MATCH_RENAME_TAC ‘u1 = u2’ >>
283 first_x_assum $ qspecl_then [‘restr (h o u1) P’, ‘restr (h o u2) P’] mp_tac >>
284 impl_tac
285 >- (fs[shom_def, FUN_EQ_THM, restr_def] >> rw[] >> metis_tac[]) >>
286 rw[FUN_EQ_THM, restr_def] >> metis_tac[shom_def, INJ_IFF, IN_UNIV]
287QED
288
289Theorem shoms_exist:
290 !(A:'a set) (B:'b set). B <> {} ==> ?h. shom h A B
291Proof
292 rw[shom_def] >> qexists_tac ‘restr (K (CHOICE B)) A’ >>
293 rw[restr_def, CHOICE_DEF]
294QED
295
296Theorem unit_pushout:
297 shom f A B /\ shom g A C /\ A <> {} ==>
298 Spushout A B C f g ({()}, restr (K ()) B, restr (K ()) C) (:unit)
299Proof
300 simp[shom_def, Spushout_def, FUN_EQ_THM] >> rw[] >>
301 simp[EXISTS_UNIQUE_DEF, FUN_EQ_THM]>> fs[IN_DEF] >> metis_tac[]
302QED
303
304Theorem Spushout_sym:
305 Spushout A B C f g (P,p1,p2) (:'d) ==>
306 Spushout A C B g f (P,p2,p1) (:'d)
307Proof
308 simp[Spushout_def] >> metis_tac[]
309QED
310
311Theorem shom_into_EMPTY[simp]:
312 shom f A {} <=> A = {} /\ f = K ARB
313Proof
314 csimp[shom_def] >> simp[FUN_EQ_THM, IN_DEF]
315QED
316
317Theorem shom_outof_EMPTY[simp]:
318 shom f {} A <=> f = K ARB
319Proof
320 simp[shom_def, FUN_EQ_THM]
321QED
322
323Theorem restr_EMPTY[simp]:
324 restr f {} = K ARB
325Proof
326 simp[FUN_EQ_THM, restr_def]
327QED
328
329Definition cardgt_def:
330 cardgt (:'a) n <=> FINITE univ(:'a) ==> n < CARD univ(:'a)
331End
332
333Theorem cardgt0[simp]:
334 cardgt (:'a) 0
335Proof
336 simp[cardgt_def] >> CCONTR_TAC >> fs[] >> rfs[]
337QED
338
339Theorem cardgt1_INJ_bool:
340 cardgt (:'a) 1 <=> ?bf. INJ bf {T;F} univ(:'a)
341Proof
342 simp[cardgt_def] >> eq_tac >> strip_tac >> fs[INJ_IFF]
343 >- (‘?x. x IN univ(:'a)’ by simp[] >>
344 ‘?y. y IN univ(:'a) /\ x <> y’
345 by (CCONTR_TAC >> fs[] >>
346 ‘univ(:'a) = {x}’ by simp[EXTENSION] >>
347 pop_assum SUBST_ALL_TAC >>
348 fs[]) >>
349 qexists_tac ‘\b. if b then x else y’ >> rw[]) >>
350 rw[] >> irule arithmeticTheory.LESS_LESS_EQ_TRANS >>
351 qexists_tac ‘CARD {bf T; bf F}’ >> conj_tac >- simp[] >>
352 irule CARD_SUBSET >> simp[]
353QED
354
355Theorem Spushouts_iso:
356 Spushout (A:'a set) (B:'b set) (C:'c set) f g (P : 'd set,i1,i2) (:'e) /\
357 Spushout A B C f g (Q : 'e set,j1,j2) (:'d) /\
358 cardgt (:'d) 1 /\ cardgt (:'e) 1 ==>
359 ?H. BIJ H P Q /\ restr (H o i1) B = j1 /\ restr (H o i2) C = j2
360Proof
361 rw[Spushout_def] >>
362 first_assum $ drule_all >>
363 last_assum $ drule_all >>
364 REWRITE_TAC[EXISTS_UNIQUE_DEF] >> simp[] >>
365 disch_then $ CONJUNCTS_THEN2 (qx_choose_then ‘pq’ strip_assume_tac)
366 strip_assume_tac >>
367 disch_then $ CONJUNCTS_THEN2 (qx_choose_then ‘qp’ strip_assume_tac)
368 strip_assume_tac >>
369 Cases_on ‘P = {}’ >> fs[] >> Cases_on ‘Q = {}’ >> fs[] >>
370 ‘SURJ pq P Q’
371 by (CCONTR_TAC >>
372 ‘?q. q IN Q /\ !p. p IN P ==> pq p <> q’
373 by (fs[SURJ_DEF, shom_def] >> metis_tac[]) >>
374 ‘(!b. b IN B ==> j1 b <> q) /\ (!c. c IN C ==> j2 c <> q)’
375 by (qpat_x_assum ‘_ = j1’ (SUBST_ALL_TAC o SYM) >>
376 qpat_x_assum ‘_ = j2’ (SUBST_ALL_TAC o SYM) >>
377 simp[restr_applies] >> metis_tac[shom_def]) >>
378 ‘qp q IN P’ by metis_tac[shom_def] >>
379 Cases_on ‘?p. p IN P /\ p <> qp q’
380 >- (fs[] >>
381 qabbrev_tac ‘qp' = \q0. if q0 = q then p else qp q0’ >>
382 ‘shom qp' Q P’ by (fs[shom_def, Abbr‘qp'’] >> metis_tac[]) >>
383 ‘restr (qp' o j1) B = i1 /\ restr (qp' o j2) C = i2’
384 by (simp[FUN_EQ_THM, restr_def, Abbr‘qp'’] >>
385 qpat_x_assum ‘_ = i1’ (SUBST_ALL_TAC o SYM) >>
386 qpat_x_assum ‘_ = i2’ (SUBST_ALL_TAC o SYM) >>
387 simp[restr_def]) >>
388 ‘qp' = qp’ by metis_tac[] >>
389 pop_assum mp_tac >>
390 simp_tac (srw_ss()) [Abbr‘qp'’, FUN_EQ_THM] >> metis_tac[]) >>
391 fs[] >>
392 ‘P = {qp q}’ by (simp[EXTENSION] >> metis_tac[]) >>
393 ‘?p. p NOTIN P’
394 by (‘?bf. INJ bf {T;F} univ(:'d)’ by metis_tac[cardgt1_INJ_bool] >>
395 Cases_on ‘bf T = qp q’
396 >- (qexists_tac‘bf F’ >> simp[] >> fs[INJ_IFF] >>
397 disch_then (assume_tac o SYM) >> fs[] >> rfs[]) >>
398 qexists_tac ‘bf T’ >> simp[]) >>
399 first_x_assum $ qspecl_then [‘{qp q; p}’, ‘i1’, ‘i2’] mp_tac >>
400 impl_tac >- (simp[] >> fs[shom_def]) >>
401 strip_tac >> fs[EXISTS_UNIQUE_DEF] >>
402 ‘?v. shom v Q {qp q; p} /\ restr (v o j1) B = i1 /\
403 restr (v o j2) C = i2 /\ v <> u’ suffices_by metis_tac[] >>
404 qexists_tac
405 ‘\q0. if q0 = q then if u q = p then qp q else p else u q0’ >>
406 simp[FUN_EQ_THM, restr_def] >> rpt strip_tac
407 >- (fs[shom_def, AllCaseEqs()] >> metis_tac[])
408 >- (qpat_x_assum ‘_ = i1’ (SUBST_ALL_TAC o SYM) >> simp[restr_def])
409 >- (qpat_x_assum ‘_ = i2’ (SUBST_ALL_TAC o SYM) >> simp[restr_def])
410 >- (qexists_tac ‘q’ >> rw[] >> fs[])) >>
411 ‘!p. p IN P ==> (?b. b IN B /\ i1 b = p) \/ (?c. c IN C /\ i2 c = p)’
412 by (CCONTR_TAC >> fs[] >>
413 Cases_on ‘?q. q IN Q /\ pq p <> q’ >> fs[]
414 >- (qabbrev_tac ‘v = \p0. if p0 = p then q else pq p0’ >>
415 ‘shom v P Q’ by (fs[shom_def, Abbr‘v’] >> metis_tac[]) >>
416 ‘v <> pq’ by (simp[Abbr‘v’, FUN_EQ_THM] >> metis_tac[]) >>
417 ‘restr (v o i1) B = j1 /\ restr (v o i2) C = j2’
418 suffices_by metis_tac[] >>
419 qpat_x_assum ‘_ = j1’ (SUBST_ALL_TAC o SYM) >>
420 qpat_x_assum ‘_ = j2’ (SUBST_ALL_TAC o SYM) >>
421 simp[FUN_EQ_THM, Abbr‘v’, restr_def] >> metis_tac[]) >>
422 ‘Q = {pq p}’ by (simp[EXTENSION] >> metis_tac[SURJ_DEF]) >>
423 ‘?q. q NOTIN Q’
424 by (‘?bf. INJ bf {T;F} univ(:'e)’ by metis_tac[cardgt1_INJ_bool] >>
425 Cases_on ‘bf T = pq p’
426 >- (qexists_tac‘bf F’ >> simp[] >> fs[INJ_IFF] >>
427 disch_then (assume_tac o SYM) >> fs[] >> rfs[]) >>
428 qexists_tac ‘bf T’ >> simp[]) >>
429 first_x_assum $ qspecl_then [‘{pq p; q}’, ‘j1’, ‘j2’] mp_tac >>
430 impl_tac >- (simp[] >> fs[shom_def]) >>
431 strip_tac >> fs[EXISTS_UNIQUE_DEF] >>
432 ‘?v. shom v P {pq p; q} /\ restr (v o i1) B = j1 /\
433 restr (v o i2) C = j2 /\ v <> u’ suffices_by metis_tac[] >>
434 qexists_tac
435 ‘\p0. if p0 = p then if u p = q then pq p else q else u p0’ >>
436 simp[FUN_EQ_THM, restr_def] >> rpt strip_tac
437 >- (fs[shom_def, AllCaseEqs()] >> metis_tac[])
438 >- (qpat_x_assum ‘_ = j1’ (SUBST_ALL_TAC o SYM) >> simp[restr_def] >>
439 metis_tac[])
440 >- (qpat_x_assum ‘_ = j2’ (SUBST_ALL_TAC o SYM) >> simp[restr_def] >>
441 metis_tac[])
442 >- (qexists_tac ‘p’ >> rw[] >> fs[])) >>
443 qexists_tac ‘pq’ >> simp[BIJ_DEF] >>
444 simp[INJ_IFF] >> conj_tac >- metis_tac[shom_def] >>
445 ‘!p. p IN P ==> qp (pq p) = p’ suffices_by metis_tac[] >>
446 qx_gen_tac ‘p’ >> strip_tac >> first_x_assum drule >> strip_tac
447 >- (pop_assum (SUBST_ALL_TAC o SYM) >>
448 qpat_x_assum ‘_ = i1’ (fn th => simp[SYM th, SimpRHS]) >>
449 qpat_x_assum ‘_ = j1’ (SUBST_ALL_TAC o SYM)>>
450 simp[restr_applies]) >>
451 pop_assum (SUBST_ALL_TAC o SYM) >>
452 qpat_x_assum ‘_ = i2’ (fn th => simp[SYM th, SimpRHS]) >>
453 qpat_x_assum ‘_ = j2’ (SUBST_ALL_TAC o SYM)>>
454 simp[restr_applies]
455QED
456
457(* eps R A a, injects a (from set A) into a's equivalence class with
458 respect to relation R
459*)
460Definition eps_def:
461 eps R A a = if a IN A then {b | R a b /\ b IN A} else ARB
462End
463
464Theorem eps_partition:
465 a IN A ==> eps R A a IN partition R A
466Proof
467 simp[eps_def, partition_def] >> strip_tac >>
468 qexists_tac ‘a’ >> simp[EXTENSION] >> metis_tac[]
469QED