1open HolKernel Parse boolLib bossLib pairTheory pred_setTheory SatisfySimps boolSimps; 2 3val _ = new_theory "category"; 4 5Definition extensional_def: 6 extensional f x <=> ���e. e ��� x ��� (f e = ARB) 7End 8 9val restrict_def = Define` 10 restrict f x = ��e. if e ��� x then f e else ARB`; 11 12val extensional_restrict = Q.store_thm( 13"extensional_restrict", 14`���f x. extensional (restrict f x) x`, 15srw_tac [][extensional_def,restrict_def]) 16val _ = export_rewrites["extensional_restrict"]; 17 18val restrict_idem = Q.store_thm( 19"restrict_idem", 20`���f x. restrict (restrict f x) x = restrict f x`, 21srw_tac [][restrict_def]) 22val _ = export_rewrites["restrict_idem"]; 23 24val extensional_restrict_iff = Q.store_thm( 25"extensional_restrict_iff", 26`���f x. extensional f x = (f = restrict f x)`, 27srw_tac [][EQ_IMP_THM] >- ( 28 fsrw_tac [][restrict_def,extensional_def,FUN_EQ_THM] >> 29 srw_tac [][] ) >> 30metis_tac [extensional_restrict]); 31 32val _ = Hol_datatype`morphism = <| 33 dom : ��; cod : ��; map : �� |>`; 34 35val morphism_component_equality = DB.theorem"morphism_component_equality"; 36 37val HS = HardSpace 1; 38 39val _ = add_rule { 40 term_name = "composable", 41 fixity = Infix(NONASSOC,450), 42 pp_elements = [HS, TOK "\226\137\136>", HS], 43 paren_style = OnlyIfNecessary, 44 block_style = (AroundEachPhrase, (PP.INCONSISTENT, 0)) 45}; 46 47Definition composable_def: f ���> g <=> (f.cod = g.dom) 48End 49 50val compose_def = Define` 51 compose (c:(��,��,��) morphism -> (��,��,��) morphism -> ��) = 52 CURRY (restrict 53 (��(f,g). <| dom := f.dom; cod := g.cod; map := c f g |>) 54 {(f,g) | f ���> g})`; 55 56val _ = add_rule { 57 term_name = "maps_to", 58 fixity = Infix(NONASSOC,450), 59 pp_elements = [HS, TOK ":-", HS, TM, HS, TOK "\226\134\146", HS], 60 paren_style = OnlyIfNecessary, 61 block_style = (AroundEachPhrase, (PP.INCONSISTENT, 0)) 62}; 63 64Definition maps_to_def: f :- x ��� y <=> (f.dom = x) ��� (f.cod = y) 65End 66 67val _ = type_abbrev("mor",``:(��,��,��) morphism``); 68 69val _ = Hol_datatype `category = 70 <| obj : �� set ; 71 mor : (��,��) mor set ; 72 id_map : �� -> ��; 73 comp : (��,��) mor -> (��,��) mor -> �� |>`; 74 75val category_component_equality = DB.theorem "category_component_equality"; 76 77val _ = add_rule { 78 term_name = "maps_to_in_syntax", 79 fixity = Infix(NONASSOC,450), 80 pp_elements = [HS, TOK ":-", HS, TM, HS, TOK "\226\134\146", HS, TM, HS, TOK "-:"], 81 paren_style = OnlyIfNecessary, 82 block_style = (AroundEachPhrase, (PP.INCONSISTENT, 0)) 83}; 84 85Definition maps_to_in_def: maps_to_in c f x y <=> f ��� c.mor ��� f :- x ��� y 86End 87 88val _ = overload_on("maps_to_in_syntax",``��f x y c. maps_to_in c f x y``); 89 90val maps_to_in_dom_cod = Q.store_thm( 91"maps_to_in_dom_cod", 92`���f c. f ��� c.mor ��� maps_to_in c f f.dom f.cod`, 93srw_tac [][maps_to_in_def,maps_to_def]); 94val _ = export_rewrites["maps_to_in_dom_cod"]; 95 96val _ = add_rule { 97 term_name = "id_in_syntax", 98 fixity = Prefix 625, 99 pp_elements = [TOK"id",HS,TM,HS,TOK"-:"], 100 paren_style = OnlyIfNecessary, 101 block_style = (AroundEachPhrase, (PP.INCONSISTENT, 0)) 102}; 103 104val id_in_def = Define` 105 id_in c = restrict (��x. <|dom := x; cod := x; map := c.id_map x|>) c.obj`; 106 107val _ = overload_on("id_in_syntax",``��x c. id_in c x``); 108 109val _ = add_rule { 110 term_name = "composable_in_syntax", 111 fixity = Infix(NONASSOC,450), 112 pp_elements = [HS, TOK "\226\137\136>", HS, TM, HS, TOK "-:"], 113 paren_style = OnlyIfNecessary, 114 block_style = (AroundEachPhrase, (PP.INCONSISTENT, 0)) 115}; 116 117val _ = add_rule{ 118 term_name="hom_syntax", 119 fixity=Suffix 620, 120 pp_elements=[TOK"|",TM,TOK"\226\134\146",TM,TOK"|"], 121 paren_style=OnlyIfNecessary, 122 block_style=(AroundEachPhrase,(PP.INCONSISTENT,0))}; 123 124val hom_def = Define` 125 hom c x y = {f | f :- x ��� y -:c}`; 126 127val _ = overload_on("hom_syntax",``hom``); 128 129Definition composable_in_def: 130 composable_in c f g <=> f ��� c.mor ��� g ��� c.mor ��� f ���> g 131End 132 133val _ = overload_on("composable_in_syntax",``��f g c. composable_in c f g``); 134 135val _ = add_rule { 136 term_name = "compose_in_syntax", 137 fixity = Infixr 800, 138 pp_elements = [HS, TOK "o", HS, TM, HS, TOK "-:"], 139 paren_style = OnlyIfNecessary, 140 block_style = (AroundSameName, (PP.INCONSISTENT, 0)) 141}; 142 143val compose_in_def = Define` 144 compose_in c = CURRY (restrict (UNCURRY (compose c.comp)) {(f,g) | f ���> g -: c})`; 145 146val _ = overload_on("compose_in_syntax",``��g f c. compose_in c f g``); 147 148val compose_in_thm = Q.store_thm( 149"compose_in_thm", 150`���c f g. f ���> g -:c ��� (g o f -: c = compose c.comp f g)`, 151srw_tac [][compose_in_def,restrict_def]); 152 153Definition extensional_category_def: 154 extensional_category c <=> 155 extensional c.id_map c.obj ��� 156 extensional (UNCURRY c.comp) {(f,g) | f ���> g -: c} 157End 158 159Definition category_axioms_def: 160 category_axioms c <=> 161 (���f. f ��� c.mor ��� f.dom ��� c.obj) ��� 162 (���f. f ��� c.mor ��� f.cod ��� c.obj) ��� 163 (���a. a ��� c.obj ��� (id a -:c) :- a ��� a -: c) ��� 164 (���f. f ��� c.mor ��� (f o (id f.dom -:c) -: c = f)) ��� 165 (���f. f ��� c.mor ��� ((id f.cod -:c) o f -: c = f)) ��� 166 (���f g h. f ���> g -: c ��� g ���> h -: c ��� 167 (((h o g -: c) o f -: c) = h o g o f -: c -: c)) ��� 168 (���f g x y z. f :- x ��� y -: c ��� g :- y ��� z -: c ��� 169 g o f -: c :- x ��� z -: c) 170End 171 172Definition is_category_def: 173 is_category c ��� extensional_category c ��� category_axioms c 174End 175 176val compose_thm = Q.store_thm( 177"compose_thm", 178`���c f g. (f ���> g) ��� (compose c f g = <|dom := f.dom; cod := g.cod; map := c f g|>)`, 179srw_tac [][compose_def,restrict_def]); 180 181val _ = export_rewrites["composable_def","maps_to_def","compose_thm"]; 182 183val mk_cat_def = Define` 184 mk_cat (c:(��,��) category) = <| 185 obj := c.obj; 186 mor := c.mor; 187 id_map := restrict c.id_map c.obj; 188 comp := CURRY (restrict (UNCURRY c.comp) {(f,g) | f ���> g -: c}) |>`; 189 190Theorem mk_cat_maps_to_in: 191 ���c f x y. f :- x ��� y -: (mk_cat c) <=> f :- x ��� y -: c 192Proof srw_tac [][maps_to_in_def,mk_cat_def,restrict_def] 193QED 194 195Theorem mk_cat_composable_in: 196 ���c f g. (f ���> g -: (mk_cat c)) <=> f ���> g -: c 197Proof srw_tac [][composable_in_def,mk_cat_def,restrict_def] 198QED 199 200val mk_cat_id = Q.store_thm( 201"mk_cat_id", 202`���c a. a ��� c.obj ��� (id a -:(mk_cat c) = id a -:c)`, 203srw_tac [][mk_cat_def,restrict_def,id_in_def]); 204 205val mk_cat_obj = Q.store_thm( 206"mk_cat_obj", 207`���c. (mk_cat c).obj = c.obj`, 208srw_tac [][mk_cat_def]); 209 210val mk_cat_mor = Q.store_thm( 211"mk_cat_mor", 212`���c. (mk_cat c).mor = c.mor`, 213srw_tac [][mk_cat_def]); 214 215val mk_cat_comp = Q.store_thm( 216"mk_cat_comp", 217`���c f g. f ���> g -: c ��� (g o f -: (mk_cat c) = g o f -: c)`, 218srw_tac [][mk_cat_def,restrict_def,compose_in_def,compose_def,composable_in_def]); 219 220val _ = export_rewrites 221["mk_cat_maps_to_in","mk_cat_composable_in", 222 "mk_cat_id","mk_cat_obj","mk_cat_mor","mk_cat_comp"]; 223 224val extensional_mk_cat = Q.store_thm( 225"extensional_mk_cat", 226`���c. extensional_category (mk_cat c)`, 227srw_tac [][extensional_category_def,mk_cat_def]) 228val _ = export_rewrites["extensional_mk_cat"]; 229 230val maps_to_dom_composable = Q.store_thm( 231"maps_to_dom_composable", 232`���c f g x. g ��� c.mor ��� (f :- x ��� g.dom -: c) ��� f ���> g -: c`, 233srw_tac [][composable_in_def,maps_to_in_def]); 234 235val maps_to_cod_composable = Q.store_thm( 236"maps_to_cod_composable", 237`���c f g y. f ��� c.mor ��� (g :- f.cod ��� y -: c) ��� f ���> g -: c`, 238srw_tac [][maps_to_in_def,composable_in_def]); 239 240val is_category_mk_cat = Q.store_thm( 241"is_category_mk_cat", 242`���c. is_category (mk_cat c) = category_axioms c`, 243srw_tac [][is_category_def] >> 244reverse EQ_TAC >> 245fsrw_tac [][category_axioms_def] >> 246strip_tac >- ( 247conj_tac >- ( 248 qx_gen_tac `f` >> 249 qspecl_then [`c`,`id f.dom -:c`,`f`,`f.dom`] mp_tac maps_to_dom_composable >> 250 srw_tac [][] ) >> 251conj_tac >- ( 252 qx_gen_tac `f` >> 253 qspecl_then [`c`,`f`,`id f.cod -:c`,`f.cod`] mp_tac maps_to_cod_composable >> 254 srw_tac [][] ) >> 255conj_tac >- ( 256 srw_tac [][] >> 257 `f ���> (h o g -: c) -: c` by ( 258 fsrw_tac [][composable_in_def,maps_to_in_def] ) >> 259 `(g o f -: c) ���> h -: c` by ( 260 fsrw_tac [][composable_in_def,maps_to_in_def] ) >> 261 srw_tac [][] ) >> 262srw_tac [][] >> 263`f ���> g -: c` by ( 264 fsrw_tac [][composable_in_def,maps_to_in_def] ) THEN 265fsrw_tac [][maps_to_in_def,composable_in_def]) >> 266conj_tac >- ( 267 qx_gen_tac `f` >> strip_tac >> 268 `id f.dom -:(mk_cat c) = id f.dom -:c` by srw_tac [][] >> 269 `f o (id f.dom -:(mk_cat c)) -:mk_cat c = f o (id f.dom -:c) -:c` by ( 270 pop_assum mp_tac >> 271 simp_tac (srw_ss()) [] >> 272 srw_tac [][] >> 273 match_mp_tac mk_cat_comp >> 274 srw_tac [][composable_in_def] >> 275 fsrw_tac [][maps_to_in_def] ) >> 276 pop_assum mp_tac >> srw_tac [][] >> 277 fsrw_tac [][] >> metis_tac []) >> 278conj_tac >- ( 279 qx_gen_tac `f` >> strip_tac >> 280 `id f.cod -:(mk_cat c) = id f.cod -:c` by srw_tac [][] >> 281 `(id f.cod -:(mk_cat c)) o f -: mk_cat c = (id f.cod -:c) o f -: c` by ( 282 pop_assum mp_tac >> 283 simp_tac (srw_ss()) [] >> 284 srw_tac [][] >> 285 match_mp_tac mk_cat_comp >> 286 srw_tac [][composable_in_def] >> 287 fsrw_tac [][maps_to_in_def] ) >> 288 pop_assum mp_tac >> srw_tac [][] >> 289 fsrw_tac [][] >> metis_tac []) >> 290conj_tac >- ( 291 srw_tac [][] >> 292 `f ���> (h o g -: c) -: c` by ( 293 fsrw_tac [][composable_in_def,maps_to_in_def] ) >> 294 `(g o f -: c) ���> h -: c` by ( 295 fsrw_tac [][composable_in_def,maps_to_in_def] ) >> 296 metis_tac [mk_cat_comp] ) >> 297srw_tac [][] >> 298`f ���> g -: c` by ( 299 fsrw_tac [][composable_in_def,maps_to_in_def] ) >> 300fsrw_tac [][maps_to_in_def,composable_in_def]); 301 302val _ = export_rewrites["is_category_mk_cat"]; 303 304val comp_assoc = Q.store_thm( 305"comp_assoc", 306`���c f g h. is_category c ��� f ���> g -: c ��� g ���> h -: c 307 ��� ((h o g -: c) o f -: c = h o (g o f -: c) -: c)`, 308srw_tac [][is_category_def,category_axioms_def]); 309 310val composable_maps_to = Q.store_thm( 311"composable_maps_to", 312`���c f g a b. is_category c ��� f ���> g -: c ��� (a = f.dom) ��� (b = g.cod) 313 ��� g o f -:c :- a ��� b -:c`, 314srw_tac [][composable_in_def] >> 315fsrw_tac [][is_category_def,category_axioms_def] >> 316first_assum match_mp_tac >> srw_tac [][maps_to_in_def]); 317 318val maps_to_composable = Q.store_thm( 319"maps_to_composable", 320`���c f g x y z. f :- x ��� y -:c ��� g :- y ��� z -:c ��� f ���> g -:c`, 321srw_tac [][composable_in_def,maps_to_in_def]); 322 323val maps_to_comp = Q.store_thm( 324"maps_to_comp", 325`���c f g x y z. is_category c ��� f :- x ��� y -:c ��� g :- y ��� z -:c ��� 326 g o f -:c :- x ��� z -:c`, 327srw_tac [][is_category_def,category_axioms_def] >> metis_tac []); 328 329val comp_mor_dom_cod = Q.store_thm( 330"comp_mor_dom_cod", 331`���c f g. is_category c ��� f ���> g -:c ��� 332 f ��� c.mor ��� g ��� c.mor ��� g o f -:c ��� c.mor ��� 333 ((g o f -:c).dom = f.dom) ��� 334 ((g o f -:c).cod = g.cod)`, 335rpt strip_tac >> 336imp_res_tac composable_maps_to >> 337fsrw_tac [][maps_to_in_def,composable_in_def]); 338 339val mor_obj = Q.store_thm( 340"mor_obj", 341`���c f. is_category c ��� f ��� c.mor ��� f.dom ��� c.obj ��� f.cod ��� c.obj`, 342srw_tac [][is_category_def,category_axioms_def]); 343val _ = export_rewrites["mor_obj"]; 344 345val maps_to_obj = Q.store_thm( 346"maps_to_obj", 347`���c f x y. is_category c ��� f :- x ��� y -:c 348��� x ��� c.obj ��� y ��� c.obj`, 349srw_tac [][maps_to_in_def] >> srw_tac [][]); 350 351val composable_obj = Q.store_thm( 352"composable_obj", 353`���c f g. is_category c ��� f ���> g -:c ��� 354 f.dom ��� c.obj ��� g.dom ��� c.obj ��� f.cod ��� c.obj ��� g.cod ��� c.obj`, 355srw_tac [][composable_in_def]); 356 357val id_maps_to = Q.store_thm( 358"id_maps_to", 359`���c x. is_category c ��� x ��� c.obj ��� (id x -:c) :- x ��� x -:c`, 360metis_tac [is_category_def,category_axioms_def]); 361 362val id_inj = Q.store_thm( 363"id_inj", 364`���c x y. is_category c ��� x ��� c.obj ��� y ��� c.obj ��� (id x -:c = id y -:c) ��� (x = y)`, 365srw_tac [][id_maps_to,id_in_def,restrict_def]); 366 367val composable_comp = Q.store_thm( 368"composable_comp", 369`���c f g h. is_category c ��� f ���> g -:c ��� g ���> h -:c ��� 370 f ���> h o g -:c -:c ��� g o f -:c ���> h -:c`, 371srw_tac [][] >> fsrw_tac [][composable_in_def,comp_mor_dom_cod]); 372 373val id_mor = Q.store_thm( 374"id_mor", 375`���c x. is_category c ��� x ��� c.obj ��� (id x -:c) ��� c.mor`, 376srw_tac [][] >> 377imp_res_tac id_maps_to >> 378fsrw_tac [][maps_to_in_def]); 379 380val id_composable_id = Q.store_thm( 381"id_composable_id", 382`���c x. is_category c ��� x ��� c.obj ��� 383 (id x -:c) ���> (id x -:c) -:c`, 384srw_tac [][] >> 385match_mp_tac maps_to_composable >> 386metis_tac [id_maps_to]); 387 388val id_dom_cod = Q.store_thm( 389"id_dom_cod", 390`���c x. is_category c ��� x ��� c.obj ��� 391 ((id x -:c).dom = x) ��� ((id x -:c).cod = x)`, 392srw_tac [][] >> 393imp_res_tac id_maps_to >> 394fsrw_tac [][maps_to_in_def]); 395 396val id_comp1 = Q.store_thm( 397"id_comp1", 398`���c f x. is_category c ��� f ��� c.mor ��� (x = f.dom) ��� 399 (f o (id x -:c) -:c = f)`, 400metis_tac [is_category_def,category_axioms_def]); 401 402val id_comp2 = Q.store_thm( 403"id_comp2", 404`���c f x. is_category c ��� f ��� c.mor ��� (x = f.cod) ��� 405 ((id x -:c) o f -:c = f)`, 406metis_tac [is_category_def,category_axioms_def]); 407 408val left_right_inv_unique = Q.store_thm( 409"left_right_inv_unique", 410`���c f g h. is_category c ��� h ���> f -:c ��� f ���> g -:c ��� 411 (g o f -:c = id f.dom -:c) ��� (f o h -:c = id f.cod -:c) ��� 412 (h = g)`, 413simp_tac std_ss [is_category_def,category_axioms_def] >> 414rpt strip_tac >> 415`h ��� c.mor ��� g ��� c.mor ��� 416 (f.dom = h.cod) ��� (f.cod = g.dom)` 417 by fsrw_tac [][composable_in_def] >> 418metis_tac [composable_in_def,composable_def]); 419 420val id_comp_id = Q.store_thm( 421"id_comp_id", 422`���c x. is_category c ��� x ��� c.obj ��� 423 ((id x -:c) o (id x -:c) -:c = (id x -:c))`, 424rpt strip_tac >> 425imp_res_tac id_dom_cod >> 426full_simp_tac std_ss [is_category_def,category_axioms_def,maps_to_in_def] >> 427metis_tac []); 428 429val _ = export_rewrites["id_dom_cod","id_comp1","id_comp2","id_comp_id","id_maps_to","id_mor"]; 430 431val _ = add_rule { 432 term_name = "iso_pair_syntax", 433 fixity = Infix(NONASSOC,450), 434 pp_elements = [HS, TOK "<\226\137\131>", HS, TM, HS, TOK "-:"], 435 paren_style = OnlyIfNecessary, 436 block_style = (AroundEachPhrase, (PP.INCONSISTENT, 0)) 437}; 438 439Definition iso_pair_def: 440 iso_pair c f g <=> f ���> g -:c ��� (f o g -:c = id g.dom -:c) ��� 441 (g o f -:c = id f.dom -:c) 442End 443 444val _ = overload_on("iso_pair_syntax",``��f g c. iso_pair c f g``); 445 446val iso_def = Define` 447 iso c f = ���g. f <���> g -:c`; 448 449Theorem iso_pair_sym: 450 ���c f g. is_category c ��� (f <���> g -:c <=> g <���> f -:c) 451Proof 452srw_tac [][] >> 453imp_res_tac is_category_def >> 454imp_res_tac category_axioms_def >> 455fsrw_tac [][iso_pair_def,composable_in_def,maps_to_in_def] >> 456metis_tac [] 457QED 458 459val inv_unique = Q.store_thm( 460"inv_unique", 461`���c f g h. is_category c ��� f <���> g -:c ��� f <���> h -:c ��� (g = h)`, 462rpt strip_tac >> 463match_mp_tac left_right_inv_unique >> 464imp_res_tac iso_pair_sym >> 465fsrw_tac [][iso_pair_def,composable_in_def] >> 466metis_tac []); 467 468val id_iso_pair = Q.store_thm( 469"id_iso_pair", 470`���c x. is_category c ��� x ��� c.obj ��� (id x -:c) <���> (id x -:c) -:c`, 471srw_tac [][iso_pair_def] >> 472match_mp_tac maps_to_composable >> 473imp_res_tac is_category_def >> 474imp_res_tac category_axioms_def >> 475metis_tac []); 476 477val _ = add_rule { 478 term_name = "inv_in_syntax", 479 fixity = Infix(NONASSOC,2050), 480 pp_elements = [TOK "\226\129\187\194\185", TOK "-:"], 481 paren_style = OnlyIfNecessary, 482 block_style = (AroundEachPhrase, (PP.INCONSISTENT, 0)) 483}; 484 485val inv_in_def = Define` 486 inv_in c f = @g. f <���> g -:c`; 487 488val _ = overload_on("inv_in_syntax",``��f c. inv_in c f``); 489 490val inv_elim_thm = Q.store_thm( 491"inv_elim_thm", 492`���P (c:(��,��) category) f g. is_category c ��� f <���> g -:c ��� P g ��� P f�����-:c`, 493srw_tac [][inv_in_def] >> 494SELECT_ELIM_TAC >> 495srw_tac [SATISFY_ss][] >> 496qsuff_tac `x=g` >- srw_tac [][] >> 497match_mp_tac inv_unique >> 498fsrw_tac [SATISFY_ss][]);; 499 500fun is_inv_in tm = let 501 val (inv_in,[c,f]) = strip_comb tm 502 val ("inv_in",ty) = dest_const inv_in 503in 504 can (match_type ``:(��,��) category -> (��,��) mor -> (��,��) mor``) ty 505end handle HOL_ERR _ => false | Bind => false; 506 507fun inv_elim_tac (g as (_, w)) = let 508 val t = find_term is_inv_in w 509in 510 CONV_TAC (UNBETA_CONV t) THEN 511 MATCH_MP_TAC inv_elim_thm THEN BETA_TAC 512end g; 513 514val inv_eq_iso_pair = Q.store_thm( 515"inv_eq_iso_pair", 516`���c f g. is_category c ��� f <���> g -:c ��� (f�����-:c = g)`, 517srw_tac [][] >> 518inv_elim_tac >> 519srw_tac [][]); 520 521val inv_idem = Q.store_thm( 522"inv_idem", 523`���c f. is_category c ��� iso c f ��� 524 iso c f�����-:c ��� ((f�����-:c)�����-:c = f)`, 525srw_tac [][iso_def] >> 526inv_elim_tac >> 527srw_tac [][] >> 528TRY inv_elim_tac >> 529metis_tac [iso_pair_sym]); 530 531val iso_pair_mor = Q.store_thm( 532"iso_pair_mor", 533`���c f g. is_category c ��� f <���> g -:c ��� 534 f ��� c.mor ��� g ��� c.mor`, 535srw_tac [][iso_pair_def,composable_in_def]); 536 537val iso_mor = Q.store_thm( 538"iso_mor", 539`���c f. is_category c ��� iso c f ��� f ��� c.mor`, 540srw_tac [][iso_def] >> 541imp_res_tac iso_pair_mor >> 542fsrw_tac [][]); 543 544val inv_mor_dom_cod = Q.store_thm( 545"inv_mor_dom_cod", 546`���c f. is_category c ��� iso c f ��� 547 f�����-:c ��� c.mor ��� 548 ((f�����-:c).dom = f.cod) ��� 549 ((f�����-:c).cod = f.dom)`, 550srw_tac [][iso_def] >> 551imp_res_tac inv_eq_iso_pair >> 552imp_res_tac iso_pair_mor >> 553imp_res_tac iso_pair_sym >> 554fsrw_tac [][iso_pair_def,composable_in_def]); 555 556val inv_maps_to = Q.store_thm( 557"inv_maps_to", 558`���c f a b. is_category c ��� iso c f ��� (a = f.cod) ��� (b = f.dom) ��� f����� -:c :- a ��� b -:c`, 559srw_tac [][maps_to_in_def,inv_mor_dom_cod]); 560 561val inv_composable = Q.store_thm( 562"inv_composable", 563`���c f. is_category c ��� iso c f ��� 564 f�����-:c ���> f -:c ��� 565 f ���> f�����-:c -:c`, 566srw_tac [][iso_def] >> 567imp_res_tac iso_pair_sym >> 568match_mp_tac maps_to_composable >> 569imp_res_tac inv_eq_iso_pair >> 570fsrw_tac [][iso_pair_def] >> 571srw_tac [][maps_to_in_def] >> 572fsrw_tac [][composable_in_def]); 573 574val comp_inv_id = Q.store_thm( 575"comp_inv_id", 576`���c f. is_category c ��� iso c f ��� 577 (f o (f�����-:c) -:c = id f.cod -:c) ��� 578 ((f�����-:c) o f -:c = id f.dom -:c)`, 579srw_tac [][iso_def] >> 580inv_elim_tac >> 581imp_res_tac iso_pair_sym >> 582imp_res_tac iso_pair_def >> 583fsrw_tac [][composable_in_def] >> 584metis_tac []); 585 586val invs_composable = Q.store_thm( 587"invs_composable", 588`���c f g. is_category c ��� f ���> g -:c ��� iso c f ��� iso c g ��� 589 g�����-:c ���> f�����-:c -:c`, 590srw_tac [][] >> 591imp_res_tac inv_mor_dom_cod >> 592fsrw_tac [][composable_in_def]); 593 594val iso_pair_comp = Q.store_thm( 595"iso_pair_comp", 596`���c f g. is_category c ��� f ���> g -:c ��� iso c f ��� iso c g ��� 597 g o f -:c <���> (f�����-:c) o (g�����-:c) -:c -:c`, 598srw_tac [][] >> 599`g�����-:c ���> f�����-:c -:c` by imp_res_tac invs_composable >> 600`(f�����-:c) o g�����-:c -:c ���> g o f -:c -:c` by ( 601 match_mp_tac maps_to_composable >> srw_tac [][] >> 602 imp_res_tac composable_maps_to >> 603 imp_res_tac inv_mor_dom_cod >> 604 imp_res_tac comp_mor_dom_cod >> 605 map_every qexists_tac [`g.cod`,`f.dom`,`g.cod`] >> 606 srw_tac [][] >> fsrw_tac [][maps_to_in_def] ) >> 607imp_res_tac is_category_def >> 608`(g o f -:c) o ((f����� -:c) o (g����� -:c) -:c) -:c = ((g o f -:c) o (f����� -:c) -:c) o (g����� -:c) -:c` by ( 609 fsrw_tac [][category_axioms_def] >> 610 first_assum (match_mp_tac o GSYM) >> srw_tac [][] >> 611 match_mp_tac (DISCH_ALL (CONJUNCT1 (UNDISCH_ALL (SPEC_ALL composable_comp)))) >> 612 fsrw_tac [][inv_composable] ) >> 613`(g o f -:c) o (f����� -:c) -:c = g o (f o (f����� -:c) -:c) -:c` by ( 614 fsrw_tac [][category_axioms_def] >> 615 first_assum match_mp_tac >> srw_tac [][] >> 616 fsrw_tac [][inv_composable] ) >> 617`((f����� -:c) o (g����� -:c) -:c) o (g o f -:c) -:c = (f����� -:c) o ((g����� -:c) o (g o f -:c) -:c) -:c` by ( 618 fsrw_tac [][category_axioms_def] >> 619 first_assum match_mp_tac >> srw_tac [][] >> 620 match_mp_tac (DISCH_ALL (CONJUNCT2 (UNDISCH_ALL (SPEC_ALL composable_comp)))) >> 621 fsrw_tac [][inv_composable] ) >> 622`(g����� -:c) o (g o f -:c) -:c = ((g����� -:c) o g -:c) o f -:c` by ( 623 fsrw_tac [][category_axioms_def] >> 624 first_assum (match_mp_tac o GSYM) >> srw_tac [][] >> 625 fsrw_tac [][inv_composable] ) >> 626`f.cod = g.dom` by fsrw_tac [][composable_in_def] >> 627imp_res_tac comp_inv_id >> 628imp_res_tac inv_mor_dom_cod >> 629imp_res_tac comp_mor_dom_cod >> 630fsrw_tac [][] >> 631fsrw_tac [][category_axioms_def] >> 632srw_tac [][iso_pair_def] >> 633match_mp_tac maps_to_composable >> 634metis_tac [maps_to_in_def,maps_to_def]); 635 636val _ = add_rule { 637 term_name = "iso_pair_between_objs_syntax", 638 fixity = Infix(NONASSOC,450), 639 pp_elements = [HS, TOK "<", TM, TOK "\226\137\131", TM, TOK ">", HS, TM, HS, TOK "-:"], 640 paren_style = OnlyIfNecessary, 641 block_style = (AroundEachPhrase, (PP.INCONSISTENT, 0)) 642}; 643 644Definition iso_pair_between_objs_def: 645 iso_pair_between_objs c a f g b <=> (f :- a ��� b) ��� f <���> g -:c 646End 647 648val _ = overload_on("iso_pair_between_objs_syntax", 649 ``��f a b g c. iso_pair_between_objs c a f g b``); 650 651val iso_pair_between_objs_sym = Q.store_thm( 652"iso_pair_between_objs_sym", 653`���f a b g c. is_category c ��� (f <a���b> g -:c ��� g <b���a> f -:c)`, 654qsuff_tac `���f a b g c. is_category c ��� (f <a���b> g -:c ��� g <b���a> f -:c)` 655>- metis_tac [] >> 656srw_tac [][iso_pair_between_objs_def] >> 657imp_res_tac iso_pair_sym >> 658fsrw_tac [][iso_pair_def] >> 659imp_res_tac maps_to_in_def >> 660imp_res_tac composable_in_def >> 661fsrw_tac [][]); 662 663val _ = add_rule { 664 term_name = "iso_objs_syntax", 665 fixity = Infix(NONASSOC,450), 666 pp_elements = [HS, TOK "\226\137\133", HS, TM, HS, TOK "-:"], 667 paren_style = OnlyIfNecessary, 668 block_style = (AroundEachPhrase, (PP.INCONSISTENT, 0)) 669}; 670 671val iso_objs_def = Define` 672 iso_objs c a b = ���f g. f <a���b> g -:c`; 673 674val _ = overload_on("iso_objs_syntax",``��a b c. iso_objs c a b``); 675 676val iso_objs_thm = Q.store_thm( 677"iso_objs_thm", 678`���c a b. is_category c ��� (a ��� b -:c = ���f. f :- a ��� b -:c ��� iso c f)`, 679srw_tac [][iso_objs_def,iso_pair_between_objs_def,iso_def] >> 680metis_tac [maps_to_in_def,maps_to_def,iso_pair_mor]); 681 682val _ = add_rule { 683 term_name = "uiso_objs_syntax", 684 fixity = Infix(NONASSOC,450), 685 pp_elements = [HS, TOK "\226\137\161", HS, TM, HS, TOK "-:"], 686 paren_style = OnlyIfNecessary, 687 block_style = (AroundEachPhrase, (PP.INCONSISTENT, 0)) 688}; 689 690val uiso_objs_def = Define` 691 uiso_objs c a b = ���!fg. FST fg <a���b> SND fg -:c`; 692 693val _ = overload_on("uiso_objs_syntax",``��a b c. uiso_objs c a b``); 694 695val uiso_objs_thm = Q.store_thm( 696"uiso_objs_thm", 697`���c a b. is_category c ��� (a ��� b -:c = ���!f. f :- a ��� b -:c ��� iso c f)`, 698srw_tac [][uiso_objs_def,EXISTS_UNIQUE_THM,EXISTS_PROD,FORALL_PROD, 699 iso_pair_between_objs_def,iso_def] >> 700metis_tac [inv_unique,maps_to_in_def,maps_to_def,iso_pair_mor]); 701 702val iso_objs_sym = Q.store_thm( 703"iso_objs_sym", 704`���c a b. is_category c ��� (a ��� b -:c ��� b ��� a -:c)`, 705srw_tac [][iso_objs_def] >> 706metis_tac [iso_pair_between_objs_sym]); 707 708val uiso_objs_sym = Q.store_thm( 709"uiso_objs_sym", 710`���c a b. is_category c ��� (a ��� b -:c ��� b ��� a -:c)`, 711qsuff_tac `���c a b. is_category c ��� (a ��� b -:c ��� b ��� a -:c)` 712>- metis_tac [] >> 713srw_tac [][uiso_objs_def] >> 714fsrw_tac [][EXISTS_UNIQUE_THM] >> 715fsrw_tac [][FORALL_PROD,EXISTS_PROD] >> 716Cases_on `fg` >> 717metis_tac [iso_pair_between_objs_sym]); 718 719val iso_objs_objs = Q.store_thm( 720"iso_objs_objs", 721`���c a b. is_category c ��� a ��� b -:c ��� a ��� c.obj ��� b ��� c.obj`, 722srw_tac [][] >> 723imp_res_tac iso_objs_thm >> 724imp_res_tac maps_to_obj); 725 726val unit_cat_def = Define` 727 unit_cat = mk_cat <| obj := {()}; mor := {ARB:(unit,unit) mor}; id_map := ARB; comp := ARB |>`; 728 729val is_category_unit_cat = Q.store_thm( 730"is_category_unit_cat", 731`is_category unit_cat`, 732srw_tac [] 733[unit_cat_def,category_axioms_def, 734 oneTheory.one,maps_to_in_def,compose_in_def, 735 morphism_component_equality]); 736 737val unit_cat_obj = Q.store_thm( 738"unit_cat_obj", 739`���x. x ��� unit_cat.obj`, 740srw_tac [][unit_cat_def,oneTheory.one]); 741 742val unit_cat_mor = Q.store_thm( 743"unit_cat_mor", 744`���f. f ��� unit_cat.mor`, 745srw_tac [][unit_cat_def,oneTheory.one,morphism_component_equality]); 746 747val unit_cat_mor_dom_cod_map = Q.store_thm( 748"unit_cat_mor_dom_cod_map", 749`���f. f ��� unit_cat.mor ��� (f.dom = ARB) ��� (f.cod = ARB) ��� (f.map = ARB)`, 750srw_tac [][unit_cat_def,oneTheory.one]); 751 752val unit_cat_maps_to = Q.store_thm( 753"unit_cat_maps_to", 754`���f x y. f :- x ��� y -:unit_cat`, 755srw_tac [][maps_to_in_def,unit_cat_mor, 756 unit_cat_mor_dom_cod_map,oneTheory.one]); 757 758val _ = export_rewrites 759["is_category_unit_cat","unit_cat_obj","unit_cat_mor", 760 "unit_cat_mor_dom_cod_map","unit_cat_maps_to"]; 761 762val discrete_mor_def = Define` 763 discrete_mor x = <|dom := x; cod := x; map := ()|>`; 764 765val discrete_mor_components = Q.store_thm( 766"discrete_mor_components", 767`���x. ((discrete_mor x).dom = x) ��� 768 ((discrete_mor x).cod = x) ��� 769 ((discrete_mor x).map = ())`, 770srw_tac [][discrete_mor_def]); 771val _ = export_rewrites["discrete_mor_components"]; 772 773val discrete_cat_def = Define` 774 discrete_cat s = mk_cat <| obj := s; mor := IMAGE discrete_mor s; 775 id_map := K (); comp := K (K ()) |>`; 776 777val is_category_discrete_cat = Q.store_thm( 778"is_category_discrete_cat", 779`���s. is_category (discrete_cat s)`, 780srw_tac [][discrete_cat_def] >> 781fsrw_tac [][category_axioms_def] >> 782conj_tac >- (ntac 2 (srw_tac [][])) >> 783conj_tac >- (ntac 2 (srw_tac [][])) >> 784conj_tac >- (srw_tac [][id_in_def,restrict_def,maps_to_in_def,morphism_component_equality]) >> 785conj_tac >- (srw_tac [][compose_in_def,restrict_def,id_in_def,composable_in_def] >> fsrw_tac [][morphism_component_equality]) >> 786conj_tac >- (srw_tac [][id_in_def,restrict_def,compose_in_def,composable_in_def] >> fsrw_tac [][morphism_component_equality]) >> 787conj_tac >- (srw_tac [][compose_in_def,restrict_def,composable_in_def] >> fsrw_tac [][morphism_component_equality]) >> 788srw_tac [][compose_in_def,restrict_def,maps_to_in_def,composable_in_def] >> 789fsrw_tac [][morphism_component_equality]); 790val _ = export_rewrites["is_category_discrete_cat"]; 791 792Theorem discrete_cat_obj_mor[simp]: 793 ���s. (���x. x ��� (discrete_cat s).obj ��� x ��� s) ��� 794 (���f. f ��� (discrete_cat s).mor ��� (���x. (f = discrete_mor x) ��� x ��� s)) 795Proof srw_tac [][discrete_cat_def] 796QED 797 798val discrete_cat_id = Q.store_thm( 799"discrete_cat_id", 800`���s x. x ��� s ��� (id x -:(discrete_cat s) = discrete_mor x)`, 801srw_tac [][id_in_def,restrict_def,morphism_component_equality] >> 802srw_tac [][discrete_cat_def,mk_cat_def,restrict_def]); 803val _ = export_rewrites["discrete_cat_id"]; 804 805Theorem discrete_cat_maps_to[simp]: 806 ���f x y s. f :- x ��� y -:(discrete_cat s) ��� 807 x ��� s ��� (y = x) ��� (f = id x -:(discrete_cat s)) 808Proof srw_tac [][maps_to_in_def,EQ_IMP_THM] >> srw_tac [][] >> 809 metis_tac [] 810QED 811 812Theorem discrete_cat_composable[simp]: 813 ���s f g. f ���> g -:discrete_cat s ��� ���x. x ��� s ��� (g = f) ��� (f = discrete_mor x) 814Proof 815 srw_tac [][composable_in_def,morphism_component_equality] >> metis_tac [] 816QED 817 818val discrete_cat_compose_in = Q.store_thm( 819"discrete_cat_compose_in", 820`���s f. f ��� (discrete_cat s).mor ��� ((f o f -:discrete_cat s) = f)`, 821fsrw_tac [boolSimps.DNF_ss][compose_in_def,restrict_def] >> 822srw_tac [][morphism_component_equality] >> 823srw_tac [][discrete_cat_def,mk_cat_def,restrict_def,composable_in_def] >> 824metis_tac []); 825val _ = export_rewrites["discrete_cat_compose_in"]; 826 827val unit_cat_discrete = Q.store_thm( 828"unit_cat_discrete", 829`unit_cat = discrete_cat {()}`, 830srw_tac [][unit_cat_def,discrete_cat_def,mk_cat_def,restrict_def] >> 831srw_tac [][composable_in_def] >> 832srw_tac [][pred_setTheory.EXTENSION] >> 833fsrw_tac [][oneTheory.one,morphism_component_equality,FUN_EQ_THM]); 834 835val indiscrete_cat_def = Define` 836 indiscrete_cat s = mk_cat <| 837 obj := s; mor := { <|dom := x; cod := y; map := ()|> | x ��� s ��� y ��� s }; 838 id_map := K (); 839 comp := K (K ()) |>`; 840 841val is_category_indiscrete_cat = Q.store_thm( 842"is_category_indiscrete_cat", 843`���s. is_category (indiscrete_cat s)`, 844srw_tac [][indiscrete_cat_def] >> 845fsrw_tac [DNF_ss] 846[category_axioms_def,maps_to_in_def,compose_in_def, 847 id_in_def,composable_in_def,restrict_def]); 848val _ = export_rewrites["is_category_indiscrete_cat"]; 849 850val indiscrete_cat_obj_mor = Q.store_thm( 851"indiscrete_cat_obj_mor", 852`���s. ((indiscrete_cat s).obj = s) ��� 853 ((indiscrete_cat s).mor = {f | f.dom ��� s ��� f.cod ��� s })`, 854srw_tac [][indiscrete_cat_def,morphism_component_equality,oneTheory.one,EXTENSION]); 855val _ = export_rewrites["indiscrete_cat_obj_mor"]; 856 857val indiscrete_cat_id = Q.store_thm( 858"indiscrete_cat_id", 859`���s x. x ��� s ��� (id x -:(indiscrete_cat s) = <|dom := x; cod := x; map := ()|>)`, 860srw_tac [][id_in_def,restrict_def,morphism_component_equality,oneTheory.one]); 861val _ = export_rewrites["indiscrete_cat_id"]; 862 863Theorem indiscrete_cat_maps_to[simp]: 864 ���f x y s. f :- x ��� y -:(indiscrete_cat s) ��� (f :- x ��� y) ��� x ��� s ��� y ��� s 865Proof srw_tac [][maps_to_in_def,EQ_IMP_THM] >> srw_tac [][] 866QED 867 868Theorem indiscrete_cat_composable[simp]: 869 ���s f g. f ���> g -:indiscrete_cat s ��� 870 (f ���> g) ��� f ��� (indiscrete_cat s).mor ��� g ��� (indiscrete_cat s).mor 871Proof 872 srw_tac [][composable_in_def,morphism_component_equality,EQ_IMP_THM] 873QED 874 875val indiscrete_cat_compose_in = Q.store_thm( 876"indiscrete_cat_compose_in", 877`���s f g. f ���> g -:indiscrete_cat s ��� ((g o f -:indiscrete_cat s) = compose (K (K ())) f g)`, 878fsrw_tac [][compose_in_def,restrict_def,oneTheory.one]); 879val _ = export_rewrites["indiscrete_cat_compose_in"]; 880 881val _ = add_rule { 882 term_name = "op_syntax", 883 fixity = Suffix 2100, 884 pp_elements = [TOK "\194\176"], 885 paren_style = OnlyIfNecessary, 886 block_style = (AroundSameName, (PP.INCONSISTENT, 0)) 887}; 888 889val op_mor_def = Define` 890 op_mor f = <| dom := f.cod; cod := f.dom; map := f.map |>`; 891 892val _ = overload_on("op_syntax",``op_mor``); 893 894val op_mor_dom = Q.store_thm( 895"op_mor_dom", 896`���f. (op_mor f).dom = f.cod`, 897srw_tac [][op_mor_def]); 898 899val op_mor_cod = Q.store_thm( 900"op_mor_cod", 901`���f. (op_mor f).cod = f.dom`, 902srw_tac [][op_mor_def]); 903 904val op_mor_map = Q.store_thm( 905"op_mor_map", 906`���f. (op_mor f).map = f.map`, 907srw_tac [][op_mor_def]); 908 909val op_mor_maps_to = Q.store_thm( 910"op_mor_maps_to", 911`���f x y. ((op_mor f) :- x ��� y) ��� f :- y ��� x`, 912srw_tac [][op_mor_dom,op_mor_cod,EQ_IMP_THM]); 913 914val op_mor_idem = Q.store_thm( 915"op_mor_idem", 916`���f. op_mor (op_mor f) = f`, 917srw_tac [][op_mor_def,morphism_component_equality]); 918 919val op_mor_composable = Q.store_thm( 920"op_mor_composable", 921`���f g. ((op_mor f) ���> (op_mor g)) ��� g ���> f`, 922srw_tac [][EQ_IMP_THM,op_mor_cod,op_mor_dom]); 923 924val op_mor_inj = Q.store_thm( 925"op_mor_inj", 926`���f g. (op_mor f = op_mor g) ��� (f = g)`, 927srw_tac [][morphism_component_equality] >> 928srw_tac [][op_mor_cod,op_mor_dom,op_mor_map,EQ_IMP_THM]); 929 930val _ = export_rewrites 931["op_mor_dom","op_mor_cod","op_mor_map","op_mor_inj", 932 "op_mor_maps_to","op_mor_idem","op_mor_composable"]; 933 934val BIJ_op_mor = Q.store_thm( 935"BIJ_op_mor", 936`���s. BIJ op_mor s (IMAGE op_mor s)`, 937srw_tac [][BIJ_DEF,INJ_DEF,SURJ_DEF] >> 938metis_tac []); 939 940val op_cat_def = Define` 941 op_cat c = <| obj := c.obj; mor := IMAGE op_mor c.mor; 942 id_map := c.id_map; comp := ��f g. c.comp (op_mor g) (op_mor f) |>`; 943 944val _ = overload_on("op_syntax",``op_cat``); 945 946val op_cat_idem = Q.store_thm( 947"op_cat_idem", 948`���c. op_cat (op_cat c) = c`, 949srw_tac [][op_cat_def,category_component_equality, 950 EXTENSION,FUN_EQ_THM] >> 951metis_tac [op_mor_idem]); 952 953val op_cat_maps_to_in = Q.store_thm( 954"op_cat_maps_to_in", 955`���f x y c. f :- x ��� y -:(op_cat c) ��� (op_mor f) :- y ��� x -:c`, 956simp_tac std_ss [op_cat_def,maps_to_in_def,op_mor_maps_to] >> 957srw_tac [][] >> 958metis_tac [op_mor_idem,op_mor_cod,op_mor_dom]); 959 960val op_cat_obj = Q.store_thm( 961"op_cat_obj", 962`���c. (op_cat c).obj = c.obj`, 963srw_tac [][op_cat_def]); 964 965val op_cat_mor = Q.store_thm( 966"op_cat_mor", 967`���c. (op_cat c).mor = IMAGE op_mor c.mor`, 968srw_tac [][op_cat_def]); 969 970val op_cat_comp = Q.store_thm( 971"op_cat_comp", 972`���c f g. (op_cat c).comp f g = c.comp (op_mor g) (op_mor f)`, 973srw_tac [][op_cat_def]); 974 975val op_cat_composable = Q.store_thm( 976"op_cat_composable", 977`���c f g. f ���> g -:(op_cat c) ��� (op_mor g) ���> (op_mor f) -:c`, 978srw_tac [][composable_in_def,op_cat_mor] >> metis_tac [op_mor_idem]); 979 980val op_cat_id = Q.store_thm( 981"op_cat_id", 982`���c x. id x -: (op_cat c) = id x -:c`, 983srw_tac [][op_cat_def,id_in_def]); 984 985val op_mor_id = Q.store_thm( 986"op_mor_id", 987`���c x. is_category c ��� x ��� c.obj ��� ((op_mor (id x -:c)) = id x -:c)`, 988srw_tac [][morphism_component_equality,id_in_def]); 989 990val _ = export_rewrites 991["op_cat_idem","op_cat_maps_to_in","op_cat_obj","op_cat_mor", 992 "op_cat_comp","op_cat_composable","op_cat_id","op_mor_id"]; 993 994val op_cat_compose_in = Q.store_thm( 995"op_cat_compose_in", 996`���f g c. f�� ���> g�� -:c ��� ((f o g -:op_cat c) = op_mor ((op_mor g) o (op_mor f) -:c))`, 997srw_tac [][compose_def,compose_in_def,composable_in_def,restrict_def] >> 998srw_tac [][morphism_component_equality] >> fsrw_tac [][]); 999 1000val op_cat_axioms = Q.store_thm( 1001"op_cat_axioms", 1002`���c. category_axioms c ��� category_axioms (op_cat c)`, 1003fsrw_tac [][category_axioms_def] >> 1004gen_tac >> strip_tac >> 1005conj_tac >- ( srw_tac [][op_cat_def] >> srw_tac [][] ) >> 1006conj_tac >- ( srw_tac [][op_cat_def] >> srw_tac [][] ) >> 1007conj_tac >- ( 1008 srw_tac [][] >> 1009 qsuff_tac `(id a -:c)�� = (id a -:c)` >- srw_tac [][] >> 1010 fsrw_tac [][morphism_component_equality,maps_to_in_def] ) >> 1011conj_tac >- ( 1012 srw_tac [][] >> srw_tac [][] >> 1013 match_mp_tac (fst (EQ_IMP_RULE (SPEC_ALL op_mor_inj))) >> 1014 `id x.cod -:c = (op_mor (id x.cod -:c))` by ( 1015 srw_tac [][morphism_component_equality] >> 1016 fsrw_tac [][maps_to_in_def] ) >> 1017 `x�� �� ���> (id x.cod -:c)�� -:c` by ( 1018 srw_tac [][composable_in_def] >> 1019 metis_tac [maps_to_in_def,maps_to_def] ) >> 1020 metis_tac [op_cat_compose_in,op_mor_idem] ) >> 1021conj_tac >- ( 1022 srw_tac [][] >> srw_tac [][] >> 1023 match_mp_tac (fst (EQ_IMP_RULE (SPEC_ALL op_mor_inj))) >> 1024 `id x.dom -:c = (op_mor (id x.dom -:c))` by ( 1025 srw_tac [][morphism_component_equality] >> 1026 fsrw_tac [][maps_to_in_def] ) >> 1027 `(id x.dom -:c)�� ���> x�� �� -:c` by ( 1028 srw_tac [][composable_in_def] >> 1029 metis_tac [maps_to_in_def,maps_to_def] ) >> 1030 metis_tac [op_cat_compose_in,op_mor_idem] ) >> 1031conj_tac >- ( 1032 srw_tac [][op_cat_compose_in] >> 1033 `(h�� ���> (f�� o g�� -:c)�� �� -:c)` by ( 1034 match_mp_tac maps_to_composable >> 1035 map_every qexists_tac [`h.cod`,`h.dom`,`f.dom`] >> 1036 fsrw_tac [][composable_in_def,maps_to_in_def] ) >> 1037 `((g�� o h�� -:c)�� �� ���> f�� -:c)` by ( 1038 match_mp_tac maps_to_composable >> 1039 map_every qexists_tac [`h.cod`,`f.cod`,`f.dom`] >> 1040 fsrw_tac [][composable_in_def,maps_to_in_def] ) >> 1041 srw_tac [][op_cat_compose_in]) >> 1042srw_tac [][] >> 1043`g�� ���> f�� -:c` by ( 1044 fsrw_tac [][composable_in_def] >> 1045 fsrw_tac [][maps_to_in_def] ) >> 1046srw_tac [][op_cat_compose_in,op_cat_maps_to_in] >> 1047fsrw_tac [][maps_to_in_def]); 1048 1049val op_cat_extensional = Q.store_thm( 1050"op_cat_extensional", 1051`���c. extensional_category c ��� extensional_category (op_cat c)`, 1052srw_tac [][extensional_category_def,op_cat_def] >> 1053fsrw_tac [][extensional_def,IN_DEF,UNCURRY,FORALL_PROD]); 1054 1055val is_category_op_cat = Q.store_thm( 1056"is_category_op_cat", 1057`���c. is_category (op_cat c) ��� is_category c`, 1058metis_tac [is_category_def,op_cat_axioms,op_cat_extensional,op_cat_idem]) 1059val _ = export_rewrites["is_category_op_cat"]; 1060 1061val op_cat_iso_pair = Q.store_thm( 1062"op_cat_iso_pair", 1063`���c f g. is_category c ��� (f <���> g -:(op_cat c) ��� (op_mor f) <���> (op_mor g) -:c)`, 1064qsuff_tac `���c f g. is_category c ��� (f <���> g -:c ��� (op_mor f) <���> (op_mor g) -:(op_cat c))` >- 1065metis_tac [op_cat_idem,is_category_op_cat,op_mor_idem] >> 1066srw_tac [][] >> 1067imp_res_tac iso_pair_sym >> 1068fsrw_tac [][iso_pair_def,op_cat_composable,op_cat_compose_in] >> 1069fsrw_tac [][compose_in_def,morphism_component_equality,composable_in_def]); 1070 1071val op_cat_iso_pair_between_objs = Q.store_thm( 1072"op_cat_iso_pair_between_objs", 1073`���c x f g y. is_category c ��� (f <x���y> g -:c�� ��� g�� <x���y> f�� -:c)`, 1074qsuff_tac `���c x f g y. is_category c ��� (f <x���y> g -:c�� ��� g�� <x���y> f�� -:c)` >- 1075metis_tac [op_cat_idem,is_category_op_cat,op_mor_idem] >> 1076srw_tac [][iso_pair_between_objs_def,op_cat_iso_pair,iso_pair_sym] >> 1077imp_res_tac iso_pair_sym >> 1078fsrw_tac [][iso_pair_def,maps_to_in_def,composable_in_def]); 1079 1080val op_cat_iso = Q.store_thm( 1081"op_cat_iso", 1082`���c f. is_category c ��� (iso c�� f ��� iso c f��)`, 1083metis_tac [iso_def,op_cat_iso_pair,op_mor_idem]); 1084 1085val op_cat_iso_objs = Q.store_thm( 1086"op_cat_iso_objs", 1087`���c x y. is_category c ��� (x ��� y -:c�� ��� x ��� y -:c)`, 1088qsuff_tac `���c x y. is_category c ��� (x ��� y -:c�� ��� x ��� y -:c)` >- 1089metis_tac [op_cat_idem,is_category_op_cat] >> 1090srw_tac [][iso_objs_def] >> 1091imp_res_tac iso_pair_between_objs_sym >> 1092fsrw_tac [][iso_pair_between_objs_def] >> 1093metis_tac [op_cat_maps_to_in,op_mor_dom,op_mor_cod,op_cat_iso_pair]); 1094 1095val op_cat_uiso_objs = Q.store_thm( 1096"op_cat_uiso_objs", 1097`���c x y. is_category c ��� (x ��� y -:c�� ��� x ��� y -:c)`, 1098qsuff_tac `���c x y. is_category c ��� (x ��� y -:c�� ��� x ��� y -:c)` >- 1099metis_tac [op_cat_idem,is_category_op_cat] >> 1100srw_tac [][uiso_objs_def,op_cat_iso_pair_between_objs] >> 1101fsrw_tac [][EXISTS_UNIQUE_THM,EXISTS_PROD,FORALL_PROD] >> 1102metis_tac [iso_pair_between_objs_sym,op_mor_idem]); 1103 1104val category_eq_thm = Q.store_thm( 1105"category_eq_thm", 1106`���c1 c2. is_category c1 ��� is_category c2 ��� 1107 (c1.obj = c2.obj) ��� (c1.mor = c2.mor) ��� 1108 (���x. x ��� c1.obj ��� (id x -:c1 = id x -:c2)) ��� 1109 (���f g. f ���> g -:c1 ��� (g o f -:c1 = g o f-:c2)) 1110��� (c1 = c2)`, 1111srw_tac [][category_component_equality] >> 1112srw_tac [][FUN_EQ_THM] >- ( 1113 qmatch_rename_tac `c1.id_map x = c2.id_map x` >> 1114 Cases_on `x ��� c1.obj` >- ( 1115 first_x_assum (qspec_then `x` mp_tac) >> 1116 srw_tac [][id_in_def,restrict_def] >> 1117 metis_tac [] ) >> 1118 fsrw_tac [][is_category_def,extensional_category_def,extensional_def] >> 1119 metis_tac [] ) >> 1120qmatch_rename_tac `c1.comp f g = c2.comp f g` >> 1121Cases_on `f ���> g-:c1` >- ( 1122 first_x_assum (qspecl_then [`f`,`g`] mp_tac) >> 1123 srw_tac [][compose_in_def,restrict_def,compose_def,composable_in_def] >> 1124 fsrw_tac [][composable_in_def] >> 1125 metis_tac [] ) >> 1126fsrw_tac [][is_category_def,extensional_category_def,extensional_def,FORALL_PROD] >> 1127fsrw_tac [][composable_in_def] >> metis_tac []); 1128 1129val op_discrete_cat = Q.store_thm( 1130"op_discrete_cat", 1131`���s. (discrete_cat s)�� = discrete_cat s`, 1132srw_tac [][] >> match_mp_tac category_eq_thm >> 1133srw_tac [][] >- ( 1134 srw_tac [DNF_ss][morphism_component_equality,EXTENSION] >> 1135 metis_tac [] ) >> 1136fsrw_tac [][compose_in_def,restrict_def,compose_def,op_cat_comp] >> 1137srw_tac [][] >> fsrw_tac [][morphism_component_equality] >> 1138srw_tac [][] >> metis_tac []); 1139val _ = export_rewrites["op_discrete_cat"]; 1140 1141val op_indiscrete_cat = Q.store_thm( 1142"op_indiscrete_cat", 1143`���s. (indiscrete_cat s)�� = indiscrete_cat s`, 1144srw_tac [][] >> match_mp_tac category_eq_thm >> 1145srw_tac [][] >- ( 1146 srw_tac [DNF_ss][morphism_component_equality,EXTENSION] >> 1147 srw_tac [][EQ_IMP_THM] >> 1148 fsrw_tac [][oneTheory.one] >> 1149 qexists_tac `op_mor x` >> 1150 srw_tac [][] ) >> 1151srw_tac [][compose_in_def,restrict_def,oneTheory.one]); 1152val _ = export_rewrites["op_indiscrete_cat"]; 1153 1154val product_mor_def = Define` 1155 product_mor (f,g) = 1156 <| dom := (f.dom,g.dom); cod := (f.cod,g.cod); map := (f.map,g.map) |>`; 1157 1158val product_mor_components = Q.store_thm( 1159"product_mor_components", 1160`���fg. ((product_mor fg).dom = ((FST fg).dom, (SND fg).dom)) ��� 1161 ((product_mor fg).cod = ((FST fg).cod, (SND fg).cod)) ��� 1162 ((product_mor fg).map = ((FST fg).map, (SND fg).map))`, 1163Cases >> srw_tac [][product_mor_def]); 1164val _ = export_rewrites["product_mor_components"]; 1165 1166val unproduct_mor_def = Define` 1167 unproduct_mor fg = 1168 (<|dom:= FST fg.dom; cod:= FST fg.cod; map := FST fg.map|>, 1169 <|dom:= SND fg.dom; cod:= SND fg.cod; map := SND fg.map|>)`; 1170 1171val product_mor_unproduct_mor = Q.store_thm( 1172"product_mor_unproduct_mor", 1173`(���x. product_mor (unproduct_mor x) = x) ��� 1174 (���x. unproduct_mor (product_mor x) = x)`, 1175fsrw_tac [][FORALL_PROD,product_mor_def,unproduct_mor_def, 1176 morphism_component_equality]); 1177val _ = export_rewrites["product_mor_unproduct_mor"]; 1178 1179Theorem product_mor_eq[simp]: 1180 ���f g f' g'. (product_mor (f,g) = product_mor (f',g')) ��� 1181 (f = f') ��� (g = g') 1182Proof 1183 srw_tac [][EQ_IMP_THM] >> 1184 fsrw_tac [][product_mor_def,morphism_component_equality] 1185QED 1186 1187val pre_product_cat_def = Define` 1188 pre_product_cat c1 c2 = <| 1189 obj := c1.obj �� c2.obj; 1190 mor := IMAGE product_mor (c1.mor �� c2.mor); 1191 id_map := ��ab. (c1.id_map (FST ab), c2.id_map (SND ab)); 1192 comp := ��ef gh. 1193 (c1.comp (FST (unproduct_mor ef)) (FST (unproduct_mor gh)), 1194 c2.comp (SND (unproduct_mor ef)) (SND (unproduct_mor gh)))|>`; 1195 1196val pre_product_cat_obj_mor = Q.store_thm( 1197"pre_product_cat_obj_mor", 1198`���c1 c2. ((pre_product_cat c1 c2).obj = c1.obj �� c2.obj) ��� 1199 ((pre_product_cat c1 c2).mor = 1200 IMAGE product_mor (c1.mor �� c2.mor))`, 1201srw_tac [][pre_product_cat_def]); 1202val _ = export_rewrites["pre_product_cat_obj_mor"]; 1203 1204Theorem pre_product_cat_maps_to_in: 1205 ���c1 c2 f x y. 1206 f :- x ��� y -:(pre_product_cat c1 c2) ��� 1207 (FST (unproduct_mor f)) :- (FST x) ��� (FST y) -: c1 ��� 1208 (SND (unproduct_mor f)) :- (SND x) ��� (SND y) -: c2 1209Proof 1210srw_tac [DNF_ss][maps_to_in_def,unproduct_mor_def, 1211 morphism_component_equality,EXISTS_PROD] >> 1212Cases_on `f.dom` >> Cases_on `f.cod` >> Cases_on `f.map` >> 1213Cases_on `x` >> Cases_on `y` >> 1214srw_tac [DNF_ss][EQ_IMP_THM] >|[ 1215 qmatch_abbrev_tac `x ��� c1.mor` >> 1216 qsuff_tac `x=p_1` >- srw_tac [][] >> 1217 srw_tac [][Abbr`x`,morphism_component_equality], 1218 qmatch_abbrev_tac `x ��� c2.mor` >> 1219 qsuff_tac `x=p_2` >- srw_tac [][] >> 1220 srw_tac [][Abbr`x`,morphism_component_equality], 1221 qmatch_assum_abbrev_tac `p1 ��� c1.mor` >> 1222 qmatch_assum_abbrev_tac `p2 ��� c2.mor` >> 1223 map_every qexists_tac [`p1`,`p2`] >> 1224 srw_tac [][Abbr`p1`,Abbr`p2`]] 1225QED 1226 1227val pre_product_cat_id = Q.store_thm( 1228"pre_product_cat_id", 1229`���c1 c2 x y. x ��� c1.obj ��� y ��� c2.obj ��� 1230 (id (x,y) -:(pre_product_cat c1 c2) = 1231 product_mor (id x -:c1, id y -:c2))`, 1232srw_tac [][id_in_def,restrict_def,product_mor_def,pre_product_cat_def]); 1233 1234Theorem pre_product_cat_composable_in[simp]: 1235 ���c1 c2 f g. f ���> g -:(pre_product_cat c1 c2) ��� 1236 (FST (unproduct_mor f) ���> FST (unproduct_mor g) -:c1) ��� 1237 (SND (unproduct_mor f) ���> SND (unproduct_mor g) -:c2) 1238Proof 1239 srw_tac [DNF_ss][composable_in_def,EXISTS_PROD,EQ_IMP_THM] >> 1240 fsrw_tac [][] >> 1241 map_every qexists_tac [`FST (unproduct_mor f)`,`SND (unproduct_mor f)`, 1242 `FST (unproduct_mor g)`,`SND (unproduct_mor g)`] >> 1243 fsrw_tac [][] >> 1244 Cases_on `f.cod` >> Cases_on `g.dom` >> fsrw_tac [][unproduct_mor_def] 1245QED 1246 1247val pre_product_cat_compose_in = Q.store_thm( 1248"pre_product_cat_compose_in", 1249`���c1 c2 f g. (f ���> g -:(pre_product_cat c1 c2)) ��� 1250 (g o f -:(pre_product_cat c1 c2) = 1251 product_mor (FST (unproduct_mor g) o FST (unproduct_mor f) -:c1, 1252 SND (unproduct_mor g) o SND (unproduct_mor f) -:c2))`, 1253srw_tac [][compose_in_def,restrict_def,product_mor_def,compose_def, 1254 unproduct_mor_def,pre_product_cat_def] >> 1255rpt (pop_assum mp_tac) >> srw_tac [][composable_in_def] >> 1256Cases_on `f.cod` >> Cases_on `g.dom` >> fsrw_tac [][]); 1257val _ = export_rewrites["pre_product_cat_compose_in"]; 1258 1259val product_cat_def = Define` 1260 product_cat c1 c2 = mk_cat (pre_product_cat c1 c2)`; 1261 1262val is_category_product_cat = Q.store_thm( 1263"is_category_product_cat", 1264`���c1 c2. is_category c1 ��� is_category c2 1265 ��� is_category (product_cat c1 c2)`, 1266srw_tac [][product_cat_def] >> 1267fsrw_tac [DNF_ss][category_axioms_def,FORALL_PROD] >> 1268conj_tac >- srw_tac [][pre_product_cat_id,pre_product_cat_maps_to_in] >> 1269conj_tac >- ( 1270 srw_tac [][pre_product_cat_id] >> 1271 qmatch_abbrev_tac `f o g -:(pre_product_cat c1 c2) = h` >> 1272 `g ���> f -:(pre_product_cat c1 c2)` by ( 1273 unabbrev_all_tac >> 1274 srw_tac [][composable_in_def] ) >> 1275 unabbrev_all_tac >> srw_tac [][] ) >> 1276conj_tac >- ( 1277 srw_tac [][pre_product_cat_id] >> 1278 qmatch_abbrev_tac `f o g -:(pre_product_cat c1 c2) = h` >> 1279 `g ���> f -:(pre_product_cat c1 c2)` by ( 1280 unabbrev_all_tac >> 1281 srw_tac [][composable_in_def] ) >> 1282 unabbrev_all_tac >> srw_tac [][] ) >> 1283conj_tac >- ( 1284 srw_tac [][] >> 1285 qmatch_abbrev_tac `ff o gg -:ppc = ee o hh -:ppc` >> 1286 `gg ���> ff -:ppc` by ( 1287 unabbrev_all_tac >> srw_tac [][composable_comp] ) >> 1288 `hh ���> ee -:ppc` by ( 1289 unabbrev_all_tac >> srw_tac [][composable_comp] ) >> 1290 unabbrev_all_tac >> srw_tac [][] >> 1291 match_mp_tac comp_assoc >> fsrw_tac [][] ) >> 1292srw_tac [][] >> 1293`f ���> g -:pre_product_cat c1 c2` by ( 1294 fsrw_tac [][pre_product_cat_maps_to_in] >> 1295 srw_tac [][] >> 1296 match_mp_tac maps_to_composable >> 1297 metis_tac [] ) >> 1298fsrw_tac [][pre_product_cat_maps_to_in] >> 1299srw_tac [][] >> 1300match_mp_tac composable_maps_to >> 1301fsrw_tac [][maps_to_in_def,composable_in_def]); 1302 1303val _ = export_theory (); 1304