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