1open HolKernel Parse bossLib boolLib boolSimps categoryTheory functorTheory nat_transTheory pairTheory lcsymtacs SatisfySimps; 2 3val _ = new_theory "limit"; 4 5val is_terminal_def = Define` 6 is_terminal c y = y ��� c.obj ��� ���x. x ��� c.obj ��� ���!f. f :- x ��� y-:c`; 7 8val is_initial_def = Define` 9 is_initial c x = is_terminal (op_cat c) x`; 10 11val is_initial_thm = Q.store_thm( 12"is_initial_thm", 13`���c x. is_category c ��� (is_initial c x = x ��� c.obj ��� ���y. y ��� c.obj ��� ���!f. f :- x ��� y-:c)`, 14metis_tac [is_initial_def,is_terminal_def,op_cat_maps_to_in,op_cat_idem,op_cat_obj,op_mor_idem]) 15 16val terminal_unique = Q.store_thm( 17"terminal_unique", 18`���c x y. is_category c ��� is_terminal c x ��� is_terminal c y ��� uiso_objs c x y`, 19srw_tac [][uiso_objs_thm] >> 20simp_tac (srw_ss()) [EXISTS_UNIQUE_THM] >> 21reverse conj_tac >- metis_tac [is_terminal_def] >> 22`���f. f :- x ��� y-:c` by metis_tac [is_terminal_def] >> 23qexists_tac `f` >> srw_tac [][iso_def] >> 24`���g. g :- y ��� x-:c` by metis_tac [is_terminal_def] >> 25qexists_tac `g` >> srw_tac [][iso_pair_def] 26>- metis_tac [maps_to_composable,FST,SND] 27>> PROVE_TAC [is_terminal_def,id_maps_to,maps_to_comp,maps_to_def,maps_to_in_def,mor_obj]); 28 29val initial_unique = Q.store_thm( 30"initial_unique", 31`���c x y. is_category c ��� is_initial c x ��� is_initial c y ��� uiso_objs c x y`, 32metis_tac [terminal_unique,is_initial_def,is_category_op_cat,op_cat_uiso_objs]); 33 34val is_terminal_cat_iso = Q.store_thm( 35"is_terminal_cat_iso", (* actually should work for just an equivalence *) 36`���f c d x. cat_iso f ��� (f :- c ��� d) ��� is_terminal c x ��� is_terminal d (f@@x)`, 37srw_tac [][cat_iso_def] >> 38imp_res_tac cat_iso_pair_sym >> 39`is_functor f ��� is_functor g` by fsrw_tac [][cat_iso_pair_def] >> 40`(f ���> g) ��� (g ���> f)` by fsrw_tac [][cat_iso_pair_def] >> 41`faithful g` by metis_tac [cat_iso_embedding,embedding_def,cat_iso_def] >> 42fsrw_tac [][is_terminal_def,objf_in_obj] >> 43qx_gen_tac `y` >> strip_tac >> 44`g@@y ��� f.dom.obj` by metis_tac [objf_in_obj,composable_def] >> 45first_x_assum (qspec_then `g@@y` mp_tac) >> 46srw_tac [][] >> 47imp_res_tac is_functor_is_category >> 48fsrw_tac [][EXISTS_UNIQUE_THM] >> 49qmatch_assum_rename_tac `h :- g@@y ��� x -:f.dom` >> 50`f##h :- f@@(g@@y) ��� f@@x -:f.cod` by metis_tac [morf_maps_to,maps_to_def] >> 51conj_tac >- metis_tac [functor_comp_objf,cat_iso_pair_def,id_functor_objf,composable_def] >> 52qx_gen_tac `h1` >> qx_gen_tac `h2` >> strip_tac >> 53fsrw_tac [][faithful_def,cat_iso_pair_def] >> 54metis_tac [morf_maps_to,functor_comp_objf,id_functor_objf,composable_def,maps_to_def]); 55 56val cone_cat_def = Define` 57 cone_cat f = comma_cat (diagonal_functor f.dom f.cod) (itself_functor f)`; 58 59val is_category_cone_cat = Q.store_thm( 60"is_category_cone_cat", 61`���f. is_functor f ��� is_category (cone_cat f)`, 62srw_tac [][cone_cat_def] >> 63imp_res_tac is_functor_is_category >> 64match_mp_tac is_category_comma_cat >> 65srw_tac [][] >- ( 66 match_mp_tac is_functor_diagonal_functor >> 67 srw_tac [][] ) >> 68match_mp_tac is_functor_itself_functor >> 69srw_tac [][]); 70val _ = export_rewrites["is_category_cone_cat"]; 71 72val _ = type_abbrev("cone",``:(��,unit,(��,��,��,��) nat_trans) morphism``); 73val _ = type_abbrev("cone_mor",``:((��,��,��,��) cone, (��,��) mor # (unit, unit) mor) mor``); 74val _ = overload_on("vertex",``��(c:(��,��,��,��)cone). c.dom``); 75val _ = overload_on("proj",``��(c:(��,��,��,��)cone) x. c.map@+x``); 76val _ = overload_on("is_cone",``��d c. c ��� (cone_cat d).obj``); 77val _ = overload_on("is_cone_mor",``��d f. f ��� (cone_cat d).mor``); 78 79val vertex_obj = Q.store_thm( 80"vertex_obj", 81`���d l c. is_cone d l ��� (c = d.cod) ��� vertex l ��� c.obj`, 82srw_tac [][cone_cat_def,is_comma_cat_obj_def]); 83val _ = export_rewrites["vertex_obj"]; 84 85val proj_maps_to = Q.store_thm( 86"proj_maps_to", 87`���d l x a b c. is_functor d ��� l ��� (cone_cat d).obj ��� x ��� d.dom.obj ��� 88 (a = vertex l) ��� (b = d@@x) ��� (c = d.cod) 89 ��� proj l x :- a ��� b -:c`, 90srw_tac [][cone_cat_def] >> 91fsrw_tac [][is_comma_cat_obj_def] >> 92match_mp_tac nt_at_maps_to >> 93imp_res_tac is_functor_is_category >> 94fsrw_tac [][]); 95 96val is_cone_thm = Q.store_thm( 97"is_cone_thm", 98`���d c. is_functor d ��� 99(is_cone d c = 100 vertex c ��� d.cod.obj ��� extensional (proj c) d.dom.obj ��� 101 (c.map :- (K_functor d.dom d.cod (vertex c)) ��� d) ��� 102 (���x. x ��� d.dom.obj ��� proj c x :- vertex c ��� d@@x -:d.cod) ��� 103 (���f. f ��� d.dom.mor ��� ((d##f) o proj c f.dom -:d.cod = proj c f.cod)))`, 104srw_tac [][cone_cat_def] >> 105fsrw_tac [][is_comma_cat_obj_def] >> 106imp_res_tac is_functor_is_category >> 107EQ_TAC >> strip_tac >- ( 108 fsrw_tac [][] >> 109 imp_res_tac is_nat_trans_def >> 110 fsrw_tac [][extensional_def,extensional_nat_trans_def] >> 111 qpat_x_assum `c.map.dom = X` mp_tac >> 112 fsrw_tac [][nat_trans_axioms_def] >> 113 strip_tac >> 114 conj_tac >- ( 115 srw_tac [][] >> 116 first_x_assum (qspec_then `x` mp_tac) >> 117 fsrw_tac [][] ) >> 118 srw_tac [][] >> 119 first_x_assum (qspecl_then [`f`,`f.dom`,`f.cod`] mp_tac) >> 120 fsrw_tac [][] >> 121 first_x_assum (qspec_then `f.cod` mp_tac) >> 122 srw_tac [][maps_to_in_def]) >> 123fsrw_tac [][] >> 124srw_tac [][is_nat_trans_def] >- ( 125 srw_tac [][extensional_nat_trans_def] >> 126 fsrw_tac [][extensional_def] ) >> 127srw_tac [][nat_trans_axioms_def] >> 128`x ��� c.map.cod.dom.obj ��� y ��� c.map.cod.dom.obj` by metis_tac[maps_to_obj] >> 129res_tac >> 130imp_res_tac maps_to_in_def >> 131fsrw_tac [][] >> 132metis_tac []); 133 134val mk_cone_def = Define` 135 (mk_cone d v ps : (��,��,��,��) cone) = 136 <| dom := v; cod := (); 137 map := mk_nt <| dom := K_functor d.dom d.cod v; 138 cod := d; 139 map := ps |> |>`; 140 141val mk_cone_dom_cod = Q.store_thm( 142"mk_cone_dom_cod", 143`���d v ps. ((mk_cone d v ps).dom = v) ��� 144 ((mk_cone d v ps).cod = ())`, 145srw_tac [][mk_cone_def]); 146val _ = export_rewrites["mk_cone_dom_cod"]; 147 148val mk_cone_proj = Q.store_thm( 149"mk_cone_proj", 150`���d v ps. (proj (mk_cone d v ps) = restrict ps d.dom.obj)`, 151srw_tac [][mk_cone_def,FUN_EQ_THM,mk_nt_def]); 152 153val mk_cone_proj_ext = save_thm( 154"mk_cone_proj_ext", 155GEN_ALL(SIMP_RULE std_ss [FUN_EQ_THM] (SPEC_ALL mk_cone_proj))); 156 157val is_cone_mk_cone = Q.store_thm( 158"is_cone_mk_cone", 159`���d v ps. is_functor d ��� 160(is_cone d (mk_cone d v ps) = v ��� d.cod.obj ��� 161 (���x. x ��� d.dom.obj ��� ps x :- v ��� d@@x -:d.cod) ��� 162 (���f. f ��� d.dom.mor ��� (ps f.cod = (d##f) o ps f.dom -:d.cod)))`, 163srw_tac [][is_cone_thm,mk_cone_proj,EQ_IMP_THM] >> 164fsrw_tac [][mk_cone_def,mk_nt_def,restrict_def] >> 165imp_res_tac is_functor_is_category >> 166imp_res_tac mor_obj >> 167srw_tac [][] >> 168first_x_assum (qspec_then `f` mp_tac) >> 169srw_tac [][]); 170 171val is_cone_mor_thm = Q.store_thm( 172"is_cone_mor_thm", 173`���d f. is_functor d ��� 174(is_cone_mor d f = 175 is_cone d f.dom ��� is_cone d f.cod ��� 176 (FST f.map) :- (vertex f.dom) ��� (vertex f.cod) -:d.cod ��� 177 ���x. x ��� d.dom.obj ��� (proj f.dom x = proj f.cod x o (FST f.map) -:d.cod))`, 178srw_tac [][] >> 179EQ_TAC >> strip_tac >- ( 180 Q.ISPECL_THEN [`cone_cat d`,`f`] mp_tac mor_obj >> 181 fsrw_tac [][cone_cat_def] >> 182 fsrw_tac [][is_comma_cat_mor_def] >> 183 qpat_x_assum `nt1 = nt2` mp_tac >> 184 qpat_x_assum `X ������> f.cod.map` mp_tac >> 185 `(d = f.dom.map.cod) ��� (is_nat_trans f.dom.map)` by ( 186 fsrw_tac [][composable_nts_def] ) >> 187 fsrw_tac [][maps_to_in_def] >> 188 srw_tac [][] >> 189 qmatch_assum_abbrev_tac `kk ������> f.cod.map` >> 190 `kk ���> f.cod.map` by fsrw_tac [][composable_nts_def] >> 191 qmatch_assum_abbrev_tac `f.dom.map = nt2` >> 192 `f.dom.map@+x = nt2@+x` by srw_tac [][] >> 193 srw_tac [][Abbr`nt2`,Abbr`kk`]) >> 194imp_res_tac is_cone_thm >> 195imp_res_tac is_functor_is_category >> 196fsrw_tac [][cone_cat_def] >> 197fsrw_tac [][is_comma_cat_mor_def,maps_to_in_def] >> 198fsrw_tac [][oneTheory.one] >> 199conj_asm1_tac >- ( 200 fsrw_tac [][composable_nts_def] >> 201 fsrw_tac [][is_comma_cat_obj_def] ) >> 202conj_asm1_tac >- ( 203 fsrw_tac [][composable_nts_def] >> 204 fsrw_tac [][is_comma_cat_obj_def] ) >> 205fsrw_tac [][] >> 206qpat_x_assum `f.dom.map.cod = d` (assume_tac o SYM) >> 207`(is_nat_trans f.dom.map)` by ( 208 full_simp_tac std_ss [composable_nts_def] ) >> 209fsrw_tac [][] >> 210match_mp_tac nt_eq_thm >> 211fsrw_tac [][]); 212 213val mk_cone_mor_def = Define` 214 (mk_cone_mor c1 c2 m : (��,��,��,��) cone_mor) = 215 <| dom := c1; cod := c2; map := (m,ARB) |>`; 216 217val mk_cone_mor_dom_cod = Q.store_thm( 218"mk_cone_mor_dom_cod", 219`���c1 c2 m. ((mk_cone_mor c1 c2 m).dom = c1) ��� 220 ((mk_cone_mor c1 c2 m).cod = c2)`, 221srw_tac [][mk_cone_mor_def]); 222val _ = export_rewrites["mk_cone_mor_dom_cod"]; 223 224val FST_mk_cone_mor_map = Q.store_thm( 225"FST_mk_cone_mor_map", 226`���c1 c2 m. (FST (mk_cone_mor c1 c2 m).map = m)`, 227srw_tac [][mk_cone_mor_def]); 228val _ = export_rewrites["FST_mk_cone_mor_map"]; 229 230val is_cone_mor_mk_cone_mor = Q.store_thm( 231"is_cone_mor_mk_cone_mor", 232`���d c1 c2 f. is_functor d ��� ( 233 is_cone_mor d (mk_cone_mor c1 c2 f) = 234 is_cone d c1 ��� is_cone d c2 ��� 235 f :- c1.dom ��� c2.dom -:d.cod ��� 236 (���x. x ��� d.dom.obj ��� (proj c1 x = proj c2 x o f -:d.cod)))`, 237srw_tac [][is_cone_mor_thm] >> 238srw_tac [][mk_cone_mor_def]); 239 240val is_limit_def = Define` 241 is_limit d l = is_functor d ��� is_terminal (cone_cat d) l`; 242 243val is_limit_is_cone = Q.store_thm( 244"is_limit_is_cone", 245`���d l. is_limit d l ��� is_cone d l`, 246srw_tac [][is_limit_def,is_terminal_def]); 247val _ = export_rewrites["is_limit_is_cone"]; 248 249val limit_universal = Q.store_thm( 250"limit_universal", 251`���d l c. is_limit d l ��� c ��� (cone_cat d).obj ��� 252 ���!m. m :- c ��� l -:(cone_cat d)`, 253srw_tac [][is_limit_def,is_terminal_def]); 254 255val cone_cat_maps_to = Q.store_thm( 256"cone_cat_maps_to", 257`���m c1 c2 d. is_functor d ��� 258(m :- c1 ��� c2 -:cone_cat d = 259 (m :- c1 ��� c2) ��� (is_cone d c1) ��� (is_cone d c2) ��� 260 (FST m.map) :- vertex c1 ��� vertex c2 -:d.cod ��� 261 (���x. x ��� d.dom.obj ��� (proj m.dom x = proj m.cod x o (FST m.map) -:d.cod)) ��� 262 (���f. f ��� d.dom.mor ��� 263 (((d##f) o proj c2 f.dom -:d.cod) o (FST m.map) -:d.cod = 264 proj c2 f.cod o (FST m.map) -:d.cod)))`, 265rpt strip_tac >> EQ_TAC >- ( 266 strip_tac >> 267 imp_res_tac maps_to_in_def >> 268 imp_res_tac is_cone_mor_thm >> 269 fsrw_tac [][] >> srw_tac [][] >> 270 qabbrev_tac `co = m.cod` >> 271 qabbrev_tac `n = co.map` >> 272 qabbrev_tac `h = FST m.map` >> 273 AP_TERM_TAC >> 274 Q.ISPECL_THEN [`n`,`n.dom`,`n.cod`,`d.cod`,`f`,`f.dom`,`f.cod`] 275 mp_tac (GSYM naturality) >> 276 fsrw_tac [][cone_cat_def] >> 277 fsrw_tac [][maps_to_in_def,is_comma_cat_obj_def] >> 278 srw_tac [][] >> 279 imp_res_tac is_functor_is_category >> 280 srw_tac [][] >> 281 match_mp_tac id_comp1 >> 282 `n @+ f.cod :- n.dom@@f.cod ��� d@@f.cod -:d.cod` by ( 283 match_mp_tac nt_at_maps_to >> 284 map_every qexists_tac [`n.dom`,`d`] >> 285 srw_tac [][] ) >> 286 fsrw_tac [][maps_to_in_def]) >> 287strip_tac >> 288srw_tac [][maps_to_in_def] >> 289fsrw_tac [][is_cone_mor_thm]); 290 291(* stylistic decision to be made: should predicates be defined to include all 292of their assumptions, e.g. is_category of the appropriate fields of a record? 293composability of functors/nat_trans would be an exception, unless you overload 294notation on those types... 295is_functor_is_category (etc.) should probably be made a rewrite. 296 297alternatively: remove all these assumptions from definitions, possibly renaming 298the definitions with a "pre_", and add separate stronger predicates (without the "pre_") 299that add the extra assumptions. 300*) 301 302val has_limits_def = Define` 303 has_limits s c = ���d. is_functor d ��� (d :- s ��� c) ��� ���l. is_limit d l`; 304 305(* 306val functor_cat_pointwise_limits = Q.store_thm( 307"functor_cat_pointwise_limits", (* Mac Lane p 111*) 308`���D J P X ��. is_functor D ��� (D :- J ��� [P���X]) ��� 309 (���p. p ��� P.obj ��� is_limit ((eval_functor P X p) ��� D) (�� p)) ��� 310 (���L. is_functor L ��� (L :- P ��� X) ��� 311 (���p. p ��� P.obj ��� (L@@p = vertex (�� p))) ��� 312 let t = ��L. (mk_nt <|dom := (diagonal_functor J [P���X])@@L; cod := D; 313 map := ��j. mk_nt <|dom := ((diagonal_functor J [P���X])@@L)@@j; cod := D@@j; 314 map := ��p. proj (�� p) j|> |>) in 315 (is_nat_trans (t L)) ��� 316 (���L'. is_functor L' ��� (L' :- P ��� X) ��� (���p. p ��� P.obj ��� (L'@@p = vertex (�� p))) ��� is_nat_trans (t L') ��� (L' = L)) ��� 317 (is_limit D (mk_cone D L ((t L).map))))`, 318srw_tac [][] >> 319limit_universal 320qexists_tac `mk_functor <|dom:=P; cod:=X; map:= use the unique maps |>` 321); 322 323val functor_cat_has_limits = Q.store_thm( 324"functor_cat_has_limits", 325`���c j v. is_category c ��� is_category j ��� is_category v ��� 326 has_limits j v ��� has_limits j [c���v]`, 327srw_tac [][has_limits_def] >> 328fsrw_tac [][GSYM RIGHT_EXISTS_IMP_THM,SKOLEM_THM] >> 329qabbrev_tac `j = d.dom` >> 330qabbrev_tac `�� = ��p. f (eval_functor c v p ��� d)` >> 331`���p. p ��� c.obj ��� is_limit (eval_functor c v p ��� d) (�� p)` by 332 srw_tac [][Abbr`��`] >> 333Q.ISPECL_THEN [`d`,`j`,`c`,`v`,`��`] mp_tac functor_cat_pointwise_limits >> 334srw_tac [][LET_THM] >> 335metis_tac []); 336*) 337 338(* 339val _ = overload_on("empty_diagram",``��c. discrete_functor {} c ARB``); 340 341val is_functor_empty_diagram = Q.store_thm( 342"is_functor_empty_diagram", 343`���c. is_category c ��� is_functor (empty_diagram c)`, 344srw_tac [][is_functor_discrete_functor]); 345val _ = export_rewrites["is_functor_empty_diagram"]; 346 347val limit_empty_diagram_terminal = Q.store_thm( 348"limit_empty_diagram_terminal", 349`���c. is_category c ��� (is_limit (empty_diagram c) = is_terminal c o vertex)`, 350srw_tac [][FUN_EQ_THM,is_limit_def] >> 351srw_tac [][is_terminal_def,is_cone_thm,EQ_IMP_THM] >- ( 352 fsrw_tac [][is_cone_thm] 353why bother proving this? 354*) 355 356val _ = overload_on("product_diagram",``��c a b. discrete_functor {1;2} c (��n. if n = 1 then a else b)``); 357 358val is_functor_product_diagram = Q.store_thm( 359"is_functor_product_diagram", 360`���c a b. is_category c ��� a ��� c.obj ��� b ��� c.obj ��� is_functor (product_diagram c a b)`, 361srw_tac [][] >> 362match_mp_tac is_functor_discrete_functor >> 363srw_tac [][]); 364 365val is_binary_product_thm = Q.store_thm( 366"is_binary_product_thm", 367`���c a b l. is_category c ��� a ��� c.obj ��� b ��� c.obj ��� 368 (is_limit (product_diagram c a b) l = 369 ���ab ��1 ��2. 370 (l = mk_cone (product_diagram c a b) ab (��n. if n = 1 then ��1 else ��2)) ��� 371 ��1 :- ab ��� a -:c ��� 372 ��2 :- ab ��� b -:c ��� 373 ���p p1 p2. 374 p1 :- p ��� a -:c ��� 375 p2 :- p ��� b -:c ��� 376 ���!m. m :- p ��� ab -:c ��� 377 (��1 o m -:c = p1) ��� 378 (��2 o m -:c = p2))`, 379rpt strip_tac >> 380qabbrev_tac `d = product_diagram c a b` >> 381`is_functor d` by (srw_tac [][is_functor_product_diagram,Abbr`d`]) >> 382EQ_TAC >- ( 383 strip_tac >> 384 map_every qexists_tac [`vertex l`,`proj l 1`,`proj l 2`] >> 385 conj_tac >- ( 386 fsrw_tac [][is_limit_def,mk_cone_def,is_terminal_def] >> 387 pop_assum (K ALL_TAC) >> 388 pop_assum mp_tac >> 389 srw_tac [][is_cone_thm] >> 390 fsrw_tac [][morphism_component_equality,oneTheory.one] >> 391 srw_tac [][mk_nt_def,restrict_def,FUN_EQ_THM] >> 392 fsrw_tac [][extensional_def] >> 393 unabbrev_all_tac >> 394 srw_tac [][] ) >> 395 ntac 2 (conj_asm1_tac >- ( 396 match_mp_tac proj_maps_to >> 397 qexists_tac `d` >> 398 srw_tac [][Abbr`d`] )) >> 399 srw_tac [][] >> 400 qabbrev_tac `co = mk_cone d p (��n. if n = 1 then p1 else p2)` >> 401 `co ��� (cone_cat d).obj` by ( 402 qunabbrev_tac `co` >> 403 fsrw_tac [][is_cone_mk_cone] >> 404 imp_res_tac maps_to_obj >> 405 qunabbrev_tac `d` >> 406 fsrw_tac [][maps_to_in_def] >> 407 srw_tac [][] >> fsrw_tac [][] ) >> 408 Q.ISPECL_THEN [`d`,`l`,`co`] mp_tac limit_universal >> 409 srw_tac [][EXISTS_UNIQUE_THM] >- ( 410 pop_assum (K ALL_TAC) >> 411 pop_assum mp_tac >> 412 srw_tac [][cone_cat_maps_to] >> 413 qexists_tac `FST m.map` >> 414 pop_assum (K ALL_TAC) >> 415 pop_assum mp_tac >> 416 unabbrev_all_tac >> 417 fsrw_tac [][mk_cone_proj_ext] >> 418 srw_tac [][restrict_def] >|[ 419 pop_assum (qspec_then `1` mp_tac), 420 pop_assum (qspec_then `2` mp_tac)] >> 421 srw_tac [][] ) >> 422 qmatch_rename_tac `ma = mb` >> 423 qabbrev_tac `mma = mk_cone_mor co l ma` >> 424 qabbrev_tac `mmb = mk_cone_mor co l mb` >> 425 `mma :- co ��� l -:cone_cat d` by ( 426 srw_tac [][maps_to_in_def,Abbr`mma`] >> 427 srw_tac [][is_cone_mor_mk_cone_mor] >- ( 428 srw_tac [][Abbr`co`,Abbr`d`] ) >> 429 pop_assum mp_tac >> 430 srw_tac [][Abbr`d`,Abbr`co`,mk_cone_proj_ext,restrict_def] ) >> 431 `mmb :- co ��� l -:cone_cat d` by ( 432 srw_tac [][maps_to_in_def,Abbr`mmb`] >> 433 srw_tac [][is_cone_mor_mk_cone_mor] >- ( 434 srw_tac [][Abbr`co`,Abbr`d`] ) >> 435 pop_assum mp_tac >> 436 srw_tac [][Abbr`d`,Abbr`co`,mk_cone_proj_ext,restrict_def] ) >> 437 `mma = mmb` by res_tac >> 438 fsrw_tac [][Abbr`mma`,Abbr`mmb`,mk_cone_mor_def]) >> 439srw_tac [][is_limit_def] >> 440fsrw_tac [][is_terminal_def] >> 441conj_asm1_tac >- ( 442 imp_res_tac maps_to_obj >> 443 srw_tac [][is_cone_mk_cone,Abbr`d`] >> srw_tac [][] >> 444 fsrw_tac [][maps_to_in_def] ) >> 445qmatch_assum_abbrev_tac `is_cone d co` >> 446qx_gen_tac `c2` >> strip_tac >> 447Q.ISPECL_THEN [`d`,`c2`] mp_tac is_cone_thm >> 448srw_tac [DNF_ss][Abbr`d`] >> 449first_x_assum (qspecl_then [`c2.dom`,`proj c2 1`,`proj c2 2`] mp_tac) >> 450srw_tac [][EXISTS_UNIQUE_THM] >- ( 451 pop_assum (K ALL_TAC) >> 452 qexists_tac `mk_cone_mor c2 co m` >> 453 srw_tac [][cone_cat_maps_to,Abbr`co`,mk_cone_proj_ext,restrict_def] >> 454 srw_tac [][] >> fsrw_tac [][maps_to_in_def] ) >> 455qmatch_rename_tac `f1 = f2` >> 456first_x_assum (qspecl_then [`FST f1.map`,`FST f2.map`] assume_tac) >> 457qsuff_tac `FST f1.map = FST f2.map` >- ( 458 simp_tac std_ss [morphism_component_equality] >> 459 fsrw_tac [][maps_to_in_def] >> 460 Cases_on `f1.map` >> Cases_on `f2.map` >> srw_tac [][] >> 461 srw_tac [][morphism_component_equality] ) >> 462first_x_assum match_mp_tac >> 463unabbrev_all_tac >> 464ntac 2 (pop_assum mp_tac) >> 465fsrw_tac [][maps_to_in_def,is_cone_mor_thm] >> 466strip_tac >> strip_tac >> 467first_assum (qspec_then `1` mp_tac) >> 468first_x_assum (qspec_then `2` mp_tac) >> 469first_assum (qspec_then `1` mp_tac) >> 470first_x_assum (qspec_then `2` mp_tac) >> 471fsrw_tac [][mk_cone_proj_ext,restrict_def]); 472 473val has_binary_products_def = Define` 474 has_binary_products c = has_limits (discrete_cat {1;2}) c`; 475 476val has_binary_products_thm = Q.store_thm( 477"has_binary_products_thm", 478`���c. is_category c ��� 479(has_binary_products c = 480 ���a b. a ��� c.obj ��� b ��� c.obj ��� 481 ���l. is_limit (product_diagram c a b) l)`, 482srw_tac [][has_binary_products_def,has_limits_def,EQ_IMP_THM] >- ( 483 first_x_assum match_mp_tac >> 484 srw_tac [][is_functor_product_diagram] ) >> 485first_x_assum (qspecl_then [`d@@1`,`d@@2`] mp_tac) >> 486`d@@1 ��� d.cod.obj ��� d@@2 ��� d.cod.obj` by srw_tac [][objf_in_obj] >> 487srw_tac [][] >> 488qmatch_assum_abbrev_tac `is_limit d' l` >> 489qsuff_tac `d' = d` >- metis_tac [] >> 490match_mp_tac functor_eq_thm >> 491srw_tac [][Abbr`d'`,is_functor_product_diagram] >> 492fsrw_tac [][] >> 493match_mp_tac (GSYM morf_discrete_mor) >> 494qexists_tac `{1;2}` >> srw_tac [][]); 495 496val binary_product_projections_exist_thm = Q.store_thm( 497"binary_product_projections_exist_thm", 498`���f1 f2 f3. ���c a b. is_category c ��� a ��� c.obj ��� b ��� c.obj ��� (���l. is_limit (product_diagram c a b) l) ��� 499 f2 c a b :- f1 c a b ��� a -:c ��� 500 f3 c a b :- f1 c a b ��� b -:c ��� 501 ���p p1 p2. 502 p1 :- p ��� a -:c ��� p2 :- p ��� b -:c ��� 503 ���!m. m :- p ��� f1 c a b -:c ��� (f2 c a b o m -:c = p1) ��� (f3 c a b o m -:c = p2)`, 504srw_tac [][GSYM SKOLEM_THM,RIGHT_EXISTS_IMP_THM] >> 505pop_assum mp_tac >> srw_tac [][is_binary_product_thm] >> 506map_every qexists_tac [`ab`,`��1`,`��2`] >> 507srw_tac [][]); 508 509val binary_product_projections_def = new_specification( 510"binary_product_projections_def", 511["binary_product","binary_product_proj1","binary_product_proj2"], 512binary_product_projections_exist_thm); 513 514val pair_morphism_def = new_specification( 515"pair_morphism_def", 516["pair_morphism"], 517binary_product_projections_def |> SPEC_ALL |> UNDISCH_ALL |> CONJUNCT2 |> CONJUNCT2 518|> SIMP_RULE std_ss [EXISTS_UNIQUE_THM,GSYM LEFT_EXISTS_AND_THM] |> DISCH_ALL 519|> Q.GEN `b` |> Q.GEN `a` |> Q.GEN `c` 520|> SIMP_RULE std_ss [GSYM RIGHT_FORALL_IMP_THM,GSYM RIGHT_EXISTS_IMP_THM,SKOLEM_THM]); 521 522val HS = HardSpace 1 523 524val _ = add_rule { 525 term_name = "binary_product_syntax", 526 fixity = Infixr 800, 527 pp_elements = [HS, TOK "\195\151", HS, TM, HS, TOK "-:"], 528 paren_style = OnlyIfNecessary, 529 block_style = (AroundSameName, (PP.INCONSISTENT, 0)) 530}; 531 532val _ = add_rule { 533 term_name = "binary_product_proj1_syntax", 534 fixity = Prefix 625, 535 pp_elements = [TOK "\207\1281", HS, TM, TOK"\195\151", TM, HS, TOK "-:"], 536 paren_style = OnlyIfNecessary, 537 block_style = (AroundSameName, (PP.INCONSISTENT, 0)) 538}; 539 540val _ = add_rule { 541 term_name = "binary_product_proj2_syntax", 542 fixity = Prefix 625, 543 pp_elements = [TOK "\207\1282", HS, TM, TOK"\195\151", TM, HS, TOK "-:"], 544 paren_style = OnlyIfNecessary, 545 block_style = (AroundSameName, (PP.INCONSISTENT, 0)) 546}; 547 548val _ = add_rule { 549 term_name = "pair_morphism_syntax", 550 fixity = Prefix 625, 551 pp_elements = [TOK "\226\159\168", TM, TOK ",", TM, TOK "\226\159\169-:"], 552 paren_style = OnlyIfNecessary, 553 block_style = (AroundSameName, (PP.INCONSISTENT, 0)) 554}; 555 556val _ = overload_on("binary_product_syntax",``��a b c. binary_product c a b``); 557val _ = overload_on("binary_product_proj1_syntax",``��a b c. binary_product_proj1 c a b``); 558val _ = overload_on("binary_product_proj2_syntax",``��a b c. binary_product_proj2 c a b``); 559val _ = overload_on("pair_morphism_syntax",``��f g c. pair_morphism c f.cod g.cod f.dom f g``); 560val _ = overload_on("binary_product_syntax", ``��f g c. pair_morphism_syntax (f o (��1 f.dom �� g.dom -:c) -:c) (g o (��2 f.dom �� g.dom -:c) -:c) c``); 561 562val binary_product_obj = Q.store_thm( 563"binary_product_obj", 564`���c x y. is_category c ��� (���l. is_limit (product_diagram c x y) l) ��� x ��� c.obj ��� y ��� c.obj ��� x �� y -:c ��� c.obj`, 565metis_tac [binary_product_projections_def,maps_to_obj]); 566val _ = export_rewrites["binary_product_obj"]; 567 568val pi_maps_to = Q.store_thm( 569"pi_maps_to", 570`���c a b. is_category c ��� (���l. is_limit (product_diagram c a b) l) ��� a ��� c.obj ��� b ��� c.obj ��� 571 ��1 a��b -:c :- a �� b -:c ��� a -:c ��� 572 ��2 a��b -:c :- a �� b -:c ��� b -:c`, 573metis_tac [binary_product_projections_def]); 574 575val pair_morphism_unique = Q.store_thm( 576"pair_morphism_unique", 577`���c a b p p1 p2 m. is_category c ��� (���l. is_limit (product_diagram c a b) l) ��� a ��� c.obj ��� b ��� c.obj ��� 578 p1 :- p ��� a -:c ��� p2 :- p ��� b -:c ��� 579 m :- p ��� a �� b -:c -:c ��� 580 ((��1 a��b -:c) o m -:c = p1) ��� 581 ((��2 a��b -:c) o m -:c = p2) ��� 582 (m = pair_morphism c a b p p1 p2)`, 583metis_tac [pair_morphism_def]); 584 585val binary_product_id = Q.store_thm( 586"binary_product_id", 587`���c a b. is_category c ��� (���l. is_limit (product_diagram c a b) l) ��� a ��� c.obj ��� b ��� c.obj ��� 588 (id a �� b -:c -:c = (id a -:c) �� id b -:c -:c)`, 589srw_tac [][] >> 590qspecl_then [`c`,`a`,`b`] mp_tac pi_maps_to >> srw_tac [SATISFY_ss][] >> 591imp_res_tac maps_to_in_def >> 592imp_res_tac maps_to_obj >> 593match_mp_tac pair_morphism_unique >> 594fsrw_tac [SATISFY_ss][]); 595 596val pair_morphism_maps_to = Q.store_thm( 597"pair_morphism_maps_to", 598`���c a b p p1 p2 x y. is_category c ��� (���l. is_limit (product_diagram c a b) l) ��� a ��� c.obj ��� b ��� c.obj ��� 599 p1 :- p ��� a -:c ��� p2 :- p ��� b -:c ��� (x = p) ��� (y = a �� b -:c) ��� 600 pair_morphism c a b p p1 p2 :- x ��� y -:c`, 601metis_tac [pair_morphism_def]); 602 603val pair_pi_id = Q.store_thm( 604"pair_pi_id", 605`���c a b. is_category c ��� (���l. is_limit (product_diagram c a b) l) ��� a ��� c.obj ��� b ��� c.obj 606 ��� (pair_morphism c a b (a �� b -:c) (��1 a��b -:c) (��2 a��b -:c) = id a �� b -:c -:c)`, 607srw_tac [][] >> 608match_mp_tac EQ_SYM >> 609match_mp_tac pair_morphism_unique >> 610fsrw_tac [SATISFY_ss][] >> 611conj_asm1_tac >- srw_tac [SATISFY_ss][pi_maps_to] >> 612conj_asm1_tac >- srw_tac [SATISFY_ss][pi_maps_to] >> 613fsrw_tac [][maps_to_in_def]); 614 615val pi1_comp_pair = Q.store_thm( 616"pi1_comp_pair", 617`���c f g p a b. is_category c ��� a ��� c.obj ��� b ��� c.obj ��� 618 (���l. is_limit (product_diagram c a b) l) ��� 619 f :- p ��� a -:c ��� g :- p ��� b -:c 620 ��� ((��1 a��b -:c) o ���f,g���-:c -:c = f)`, 621metis_tac [pair_morphism_def,maps_to_in_def,maps_to_def]) 622 623val pi2_comp_pair = Q.store_thm( 624"pi2_comp_pair", 625`���c f g p a b. is_category c ��� a ��� c.obj ��� b ��� c.obj ��� 626 (���l. is_limit (product_diagram c a b) l) ��� 627 f :- p ��� a -:c ��� g :- p ��� b -:c 628 ��� ((��2 a��b -:c) o ���f,g���-:c -:c = g)`, 629metis_tac [pair_morphism_def,maps_to_in_def,maps_to_def]) 630 631val pair_morphism_comp = Q.store_thm( 632"pair_morphism_comp", 633`���c f g h. is_category c ��� h ���> f -:c ��� h ���> g -:c ��� (���l. is_limit (product_diagram c f.cod g.cod) l) 634 ��� ((���f,g���-:c) o h -:c = ���f o h -:c,g o h -:c���-:c)`, 635srw_tac [][] >> 636match_mp_tac pair_morphism_unique >> 637qspecl_then [`c`,`h`,`f`,`h.dom`,`f.cod`] mp_tac composable_maps_to >> 638qspecl_then [`c`,`h`,`g`,`h.dom`,`g.cod`] mp_tac composable_maps_to >> 639fsrw_tac [][] >> ntac 2 strip_tac >> 640imp_res_tac maps_to_in_def >> 641fsrw_tac [SATISFY_ss][] >> 642`���f,g���-:c :- f.dom ��� f.cod �� g.cod -:c -:c` by ( 643 match_mp_tac pair_morphism_maps_to >> 644 fsrw_tac [SATISFY_ss][] >> 645 imp_res_tac maps_to_obj >> 646 fsrw_tac [][maps_to_in_def,composable_in_def] ) >> 647`h ���> ���f,g���-:c -:c` by fsrw_tac [][composable_in_def,maps_to_in_def] >> 648qspecl_then [`c`,`f.cod`,`g.cod`] mp_tac pi_maps_to >> 649fsrw_tac [SATISFY_ss][maps_to_obj] >> strip_tac >> 650`���f,g���-:c ���> ��2 f.cod��g.cod -:c -:c` by fsrw_tac [][composable_in_def,maps_to_in_def] >> 651`���f,g���-:c ���> ��1 f.cod��g.cod -:c -:c` by fsrw_tac [][composable_in_def,maps_to_in_def] >> 652conj_tac >- ( match_mp_tac composable_maps_to >> fsrw_tac [][maps_to_in_def,composable_in_def] ) >> 653qspecl_then [`c`,`h`,`���f,g���-:c`,`��1 f.cod��g.cod -:c`] mp_tac (GSYM comp_assoc) >> 654qspecl_then [`c`,`h`,`���f,g���-:c`,`��2 f.cod��g.cod -:c`] mp_tac (GSYM comp_assoc) >> 655srw_tac [][] >> 656AP_TERM_TAC >|[ 657 match_mp_tac pi1_comp_pair, 658 match_mp_tac pi2_comp_pair 659] >> qexists_tac `f.dom` >> 660fsrw_tac [SATISFY_ss][maps_to_in_def,maps_to_obj,composable_in_def]); 661 662val pre_product_functor_def = Define` 663 pre_product_functor c y = <| 664 dom := c; cod := c; map := ��f. f �� id y -:c -:c |>`; 665 666val pre_product_functor_components = Q.store_thm( 667"pre_product_functor_components", 668`���c x. ((pre_product_functor c x).dom = c) ��� 669 ((pre_product_functor c x).cod = c) ��� 670 (���f. (pre_product_functor c x)##f = f �� id x-:c -:c)`, 671srw_tac [][pre_product_functor_def,morf_def]) 672val _ = export_rewrites["pre_product_functor_components"]; 673 674val pre_product_functor_objf = Q.store_thm( 675"pre_product_functor_objf", 676`���c x y. is_category c ��� (���l. is_limit (product_diagram c x y) l) ��� x ��� c.obj ��� y ��� c.obj 677��� ((pre_product_functor c y)@@x = x �� y -:c)`, 678srw_tac [][objf_def] >> 679SELECT_ELIM_TAC >> 680srw_tac [][] >- ( 681 qexists_tac `x �� y -:c` >> 682 srw_tac [SATISFY_ss][binary_product_obj,binary_product_id] ) >> 683qmatch_assum_abbrev_tac `pair_morphism c a b p p1 p2 = id z -:c` >> 684qspecl_then [`c`,`a`,`b`,`p`,`p1`,`p2`] mp_tac pair_morphism_maps_to >> 685qspecl_then [`c`,`x`,`y`] mp_tac pi_maps_to >> 686fsrw_tac [SATISFY_ss][] >> 687strip_tac >> 688imp_res_tac maps_to_in_def >> 689unabbrev_all_tac >> 690fsrw_tac [SATISFY_ss][] >> 691srw_tac [][maps_to_in_def]); 692 693val product_functor_def = Define` 694 product_functor c x = mk_functor (pre_product_functor c x)`; 695 696val is_functor_product_functor = Q.store_thm( 697"is_functor_product_functor", 698`���c y. is_category c ��� has_binary_products c ��� y ��� c.obj ��� is_functor (product_functor c y)`, 699srw_tac [][product_functor_def] >> 700qpat_x_assum `has_binary_products c` mp_tac >> srw_tac [][has_binary_products_thm] >> 701srw_tac [][functor_axioms_def] >- ( 702 imp_res_tac maps_to_obj >> 703 imp_res_tac maps_to_in_def >> 704 srw_tac [][pre_product_functor_objf] >> 705 match_mp_tac pair_morphism_maps_to >> 706 qspecl_then [`c`,`f.dom`,`y`] mp_tac pi_maps_to >> 707 fsrw_tac [][] >> 708 strip_tac >> 709 qmatch_assum_rename_tac `f :- x ��� w -:c` >> 710 qspecl_then [`c`,`��1 x��y -:c`,`f`,`x �� y-:c`,`x`,`w`] mp_tac maps_to_comp >> 711 fsrw_tac [][] >> strip_tac >> 712 imp_res_tac maps_to_in_def >> 713 fsrw_tac [][]) 714>- ( 715 qexists_tac `x �� y-:c` >> 716 srw_tac [][] >> 717 qspecl_then [`c`,`x`,`y`] mp_tac pi_maps_to >> 718 fsrw_tac [][] >> strip_tac >> 719 fsrw_tac [][maps_to_in_def,pair_pi_id]) >> 720qmatch_abbrev_tac `���p o q-:c, r o s-:c���-:c = (���t,u���-:c) o (���v,w���-:c) -:c` >> 721`p.dom = f.dom` by ( 722 unabbrev_all_tac >> 723 qspecl_then [`c`,`f`,`g`,`f.dom`,`g.cod`] mp_tac composable_maps_to >> 724 srw_tac [][maps_to_in_def] ) >> 725srw_tac [][Abbr`r`] >> 726qabbrev_tac `a = f.dom` >> 727qabbrev_tac `b = g.dom` >> 728qpat_x_assum `Abbrev (p = X)` assume_tac >> 729fsrw_tac [][] >> 730qspecl_then [`c`,`a`,`y`] mp_tac pi_maps_to >> 731qspecl_then [`c`,`b`,`y`] mp_tac pi_maps_to >> 732`a ��� c.obj ��� b ��� c.obj` by metis_tac [composable_obj] >> 733fsrw_tac [SATISFY_ss][] >> ntac 2 strip_tac >> 734`t :- b��y-:c ��� g.cod -:c` by ( 735 qunabbrev_tac `t` >> 736 match_mp_tac maps_to_comp >> 737 qexists_tac `b` >> 738 fsrw_tac [][Abbr`b`,composable_in_def] ) >> 739`v :- a��y-:c ��� f.cod -:c` by ( 740 qunabbrev_tac `v` >> 741 match_mp_tac maps_to_comp >> 742 qexists_tac `a` >> 743 fsrw_tac [][Abbr`a`,composable_in_def] ) >> 744`u :- b��y-:c ��� y -:c` by ( 745 qunabbrev_tac `u` >> 746 match_mp_tac maps_to_comp >> 747 qexists_tac `y` >> 748 fsrw_tac [][] ) >> 749`w :- a��y-:c ��� y -:c` by ( 750 qunabbrev_tac `w` >> 751 match_mp_tac maps_to_comp >> 752 qexists_tac `y` >> 753 fsrw_tac [][]) >> 754`���v,w���-:c :- a��y-:c ��� b��y-:c -:c` by ( 755 match_mp_tac pair_morphism_maps_to >> 756 fsrw_tac [][maps_to_in_def,composable_in_def] ) >> 757`t o ���v,w���-:c -:c = p o q -:c` by ( 758 qunabbrev_tac `t` >> 759 qspecl_then [`c`,`���v,w���-:c`,`��1 b��y -:c`,`g`] mp_tac comp_assoc >> 760 `���v,w���-:c ���> ��1 b��y -:c -:c` by metis_tac [maps_to_composable] >> 761 `��1 b��y-:c ���> g -:c` by metis_tac [maps_to_composable,maps_to_in_def,maps_to_def,composable_in_def] >> 762 srw_tac [][] >> 763 `(��1 b��y -:c) o ���v,w���-:c -:c = v` by ( 764 match_mp_tac pi1_comp_pair >> 765 qexists_tac `p.dom �� y-:c` >> fsrw_tac [][] >> 766 metis_tac [composable_in_def,composable_def] ) >> 767 fsrw_tac [][Abbr`p`,Abbr`v`] >> 768 match_mp_tac (GSYM comp_assoc) >> 769 fsrw_tac [][] >> 770 match_mp_tac maps_to_composable >> 771 unabbrev_all_tac >> 772 metis_tac [maps_to_in_def,maps_to_def,composable_in_def] ) >> 773`u o ���v,w���-:c -:c = w` by ( 774 qunabbrev_tac `u` >> 775 qspecl_then [`c`,`���v,w���-:c`,`��2 b��y -:c`,`id y -:c`] mp_tac comp_assoc >> 776 `���v,w���-:c ���> ��2 b��y-:c -:c` by metis_tac [maps_to_composable] >> 777 `��2 b��y -:c ���> id y -:c -:c` by metis_tac [maps_to_composable,id_maps_to] >> 778 srw_tac [][] >> 779 `(��2 b��y -:c) o ���v,w���-:c -:c = w` by ( 780 match_mp_tac pi2_comp_pair >> 781 qexists_tac `p.dom �� y-:c` >> fsrw_tac [][] >> 782 metis_tac [composable_in_def,composable_def] ) >> 783 fsrw_tac [][maps_to_in_def] ) >> 784ntac 2 (pop_assum (mp_tac o SYM)) >> 785qabbrev_tac `h = ���v,w���-:c` >> 786srw_tac [][] >> 787match_mp_tac (GSYM pair_morphism_comp) >> 788fsrw_tac [][] >> 789conj_tac >- metis_tac [maps_to_composable] >> 790conj_tac >- metis_tac [maps_to_composable] >> 791srw_tac [][DECIDE ``(1 = n) = (n = 1)``] >> 792first_x_assum match_mp_tac >> 793fsrw_tac [][maps_to_in_def]); 794 795val _ = export_theory (); 796