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