1open HolKernel Parse boolLib boolSimps bossLib SatisfySimps categoryTheory functorTheory pred_setTheory limitTheory; 2 3val _ = new_theory "ens_cat"; 4val _ = ParseExtras.temp_loose_equality() 5 6val HasFunType_def = Define` 7 HasFunType f X Y = extensional f X ��� ���x. x ��� X ��� f x ��� Y`; 8 9val IsTypedFun_def = Define` 10 IsTypedFun f = HasFunType f.map f.dom f.cod`; 11 12val TypedFun_ext = Q.store_thm( 13"TypedFun_ext", 14`���f g. IsTypedFun f ��� IsTypedFun g ��� 15 ((f = g) = ((f.dom = g.dom) ��� (f.cod = g.cod) ��� (���x. x ��� f.dom ��� (f.map x = g.map x))))`, 16srw_tac [][morphism_component_equality,IsTypedFun_def,HasFunType_def,extensional_def] >> 17srw_tac [][EQ_IMP_THM] >> 18srw_tac [][FUN_EQ_THM] >> 19Cases_on `x ��� f.dom` >> srw_tac [][] >> 20pop_assum mp_tac >> srw_tac [][]); 21 22val TypedGraphFun_def = Define` 23 TypedGraphFun (X,Y) f = <| 24 dom := X; cod := Y; map := restrict f X |>`; 25 26val TypedGraphFun_components = Q.store_thm( 27"TypedGraphFun_components", 28`���X Y f. ((TypedGraphFun (X,Y) f).dom = X) ��� 29 ((TypedGraphFun (X,Y) f).cod = Y) ��� 30 ((TypedGraphFun (X,Y) f).map = restrict f X)`, 31srw_tac [][TypedGraphFun_def]); 32val _ = export_rewrites["TypedGraphFun_components"]; 33 34val IsTypedFunTypedGraphFun = Q.store_thm( 35"IsTypedFunTypedGraphFun", 36`���f X Y. IsTypedFun (TypedGraphFun (X,Y) f) = ���x. x ��� X ��� f x ��� Y`, 37srw_tac [][EQ_IMP_THM,IsTypedFun_def,TypedGraphFun_def,HasFunType_def,restrict_def,extensional_def]); 38val _ = export_rewrites["IsTypedFunTypedGraphFun"]; 39 40val TypedGraphFun_Ext = Q.store_thm( 41"TypedGraphFun_Ext", 42`���X Y f X' Y' f'. (TypedGraphFun (X,Y) f = TypedGraphFun (X',Y') f') ��� ((X = X') ��� (Y = Y') ��� ���x. x ��� X ��� (f x = f' x))`, 43srw_tac [][TypedGraphFun_def,restrict_def,EQ_IMP_THM] >> metis_tac []); 44 45val ComposeFun_def = Define` 46 ComposeFun (X,Y) g f = restrict ((restrict g Y) o f) X`; 47 48val ComposeTypedFun_def = Define` 49 ComposeTypedFun = compose (��f g. ComposeFun (f.dom,g.dom) g.map f.map)`; 50 51val _ = overload_on("o",``��g f. ComposeTypedFun f g``); 52val _ = overload_on("o",``��g f. (combin$o) g f``); 53 54val ComposeTypedFun_components = Q.store_thm( 55"ComposeTypedFun_components", 56`���f g. (f ���> g) ��� 57((g o f).dom = f.dom) ��� 58((g o f).cod = g.cod) ��� 59((g o f).map = ComposeFun(f.dom,g.dom) g.map f.map)`, 60srw_tac [][ComposeTypedFun_def]); 61val _ = export_rewrites["ComposeTypedFun_components"]; 62 63val IdFun_def = Define` 64 IdFun s = restrict I s`; 65 66val IdFunAp = Q.store_thm( 67"IdFunAp", 68`���x s. x ��� s ��� (IdFun s x = x)`, 69srw_tac [][IdFun_def,restrict_def]); 70val _ = export_rewrites["IdFunAp"]; 71 72val IdFunType = Q.store_thm( 73"IdFunType", 74`���s. HasFunType (IdFun s) s s`, 75srw_tac [][HasFunType_def,IdFun_def]); 76val _ = export_rewrites["IdFunType"]; 77 78val ComposeFunId = Q.store_thm( 79"ComposeFunId", 80`���X Y f. HasFunType f X Y ��� 81(ComposeFun (X,X) f (IdFun X) = f) ��� 82(ComposeFun (X,Y) (IdFun Y) f = f)`, 83srw_tac [][ComposeFun_def,IdFun_def,FUN_EQ_THM,HasFunType_def] >> 84fsrw_tac [][restrict_def,extensional_def] >> 85metis_tac []); 86val _ = export_rewrites["ComposeFunId"]; 87 88val ComposeFunAssoc = Q.store_thm( 89"ComposeFunAssoc", 90`���a f b g c h ab bc ac. 91 HasFunType f a b ��� HasFunType g b c ��� 92 (ab = (a,b)) ��� (bc = (b,c)) ��� (ac = (a,c)) ��� 93 (ComposeFun ac h (ComposeFun ab g f) = ComposeFun ab (ComposeFun bc h g) f)`, 94srw_tac [][ComposeFun_def,FUN_EQ_THM] >> 95fsrw_tac [][HasFunType_def,extensional_def,restrict_def]); 96val _ = export_rewrites["ComposeFunAssoc"]; 97 98val ComposeFunType = Q.store_thm( 99"ComposeFunType", 100`���X f Y g XY Z. HasFunType f X Y ��� HasFunType g Y Z ��� (XY = (X,Y)) ��� HasFunType (ComposeFun XY g f) X Z`, 101srw_tac [][HasFunType_def,ComposeFun_def] >> 102fsrw_tac [][extensional_def,restrict_def]); 103val _ = export_rewrites["ComposeFunType"]; 104 105val _ = overload_on("IsTypedFunIn",``��U f. f.dom ��� U ��� f.cod ��� U ��� IsTypedFun f``); 106 107val ens_cat_def = Define` 108 ens_cat U = mk_cat <| 109 obj := U ; 110 mor := {f | IsTypedFunIn U f} ; 111 id_map := IdFun ; 112 comp := ��f g. (g o f).map |>`; 113 114val is_category_ens_cat = Q.store_thm( 115"is_category_ens_cat", 116`���U. is_category (ens_cat U)`, 117srw_tac [][ens_cat_def] >> 118srw_tac [][category_axioms_def] >- ( 119 srw_tac [][maps_to_in_def,id_in_def,IsTypedFun_def,restrict_def] ) 120>- ( 121 srw_tac [][id_in_def,restrict_def] >> 122 srw_tac [][compose_in_def,restrict_def] >> 123 fsrw_tac [SATISFY_ss][IsTypedFun_def,morphism_component_equality] >> 124 fsrw_tac [][composable_in_def] >> fsrw_tac [][]) 125>- ( 126 srw_tac [][id_in_def,restrict_def] >> 127 srw_tac [][compose_in_def,restrict_def] >> 128 fsrw_tac [SATISFY_ss][IsTypedFun_def,morphism_component_equality] >> 129 fsrw_tac [][composable_in_def] >> fsrw_tac [][]) 130>- ( 131 fsrw_tac [][compose_in_def,restrict_def] >> 132 fsrw_tac [][composable_in_def] >> 133 fsrw_tac [][compose_def,restrict_def] >> 134 fsrw_tac [][IsTypedFun_def]) >> 135fsrw_tac [][maps_to_in_def] >> 136fsrw_tac [][compose_in_def,restrict_def,composable_in_def] >> 137fsrw_tac [][IsTypedFun_def]); 138val _ = export_rewrites["is_category_ens_cat"]; 139 140val ens_cat_obj = Q.store_thm( 141"ens_cat_obj", 142`���U. (ens_cat U).obj = U`, 143srw_tac [][ens_cat_def]); 144 145val ens_cat_mor = Q.store_thm( 146"ens_cat_mor", 147`���U f. f ��� (ens_cat U).mor ��� IsTypedFunIn U f`, 148srw_tac [][ens_cat_def]); 149 150val ens_cat_id = Q.store_thm( 151"ens_cat_id", 152`���U x. x ��� U ��� ((id x -:(ens_cat U)) = TypedGraphFun (x,x) (IdFun x))`, 153srw_tac [][id_in_def,ens_cat_def,mk_cat_def,restrict_def,TypedGraphFun_def,IdFun_def]); 154 155val ens_cat_composable_in = Q.store_thm( 156"ens_cat_composable_in", 157`���U f g. f ���> g -:(ens_cat U) ��� IsTypedFunIn U f ��� IsTypedFunIn U g ��� f ���> g`, 158srw_tac [][composable_in_def,ens_cat_mor]); 159 160val ens_cat_comp = Q.store_thm( 161"ens_cat_comp", 162`���U f g. f ���> g -:(ens_cat U) ��� ((ens_cat U).comp f g = ComposeFun(f.dom,g.dom) g.map f.map)`, 163srw_tac [][ens_cat_def,mk_cat_def,restrict_def,composable_in_def]); 164 165val ens_cat_compose_in = Q.store_thm( 166"ens_cat_compose_in", 167`���U f g. f ���> g -:(ens_cat U) ��� (g o f -:(ens_cat U) = g o f)`, 168srw_tac [][compose_in_def,morphism_component_equality,ens_cat_comp,ens_cat_composable_in,restrict_def]>> 169metis_tac []); 170 171val ens_cat_maps_to_in = Q.store_thm( 172"ens_cat_maps_to_in", 173`���U f x y. f :- x ��� y -:(ens_cat U) ��� IsTypedFunIn U f ��� f :- x ��� y`, 174srw_tac [][maps_to_in_def,EQ_IMP_THM,ens_cat_mor]); 175 176val _ = export_rewrites[ 177"ens_cat_obj","ens_cat_mor","ens_cat_id", 178"ens_cat_composable_in","ens_cat_comp", 179"ens_cat_compose_in","ens_cat_maps_to_in"]; 180 181val ens_cat_empty_terminal = Q.store_thm( 182"ens_cat_empty_terminal", 183`���U. is_terminal (ens_cat U) ��� = ��� ��� U ��� ���x. x ��� U ��� (x = ���)`, 184srw_tac [][is_terminal_def,EQ_IMP_THM,EXISTS_UNIQUE_THM] >- ( 185 first_x_assum (qspec_then `x` mp_tac) >> 186 srw_tac [][] >> 187 fsrw_tac [][IsTypedFun_def,HasFunType_def,EXTENSION] ) 188>- ( 189 qexists_tac `TypedGraphFun (���,���) ARB` >> 190 srw_tac [][] ) >> 191srw_tac [][TypedFun_ext]); 192 193Theorem ens_cat_terminal_objects: 194 ���U t. (���s. s ��� U ��� s ��� ���) ��� 195 (is_terminal (ens_cat U) t = ���x. (t = {x}) ��� t ��� U) 196Proof 197 srw_tac [][is_terminal_def,EQ_IMP_THM,EXISTS_UNIQUE_THM] >> 198 srw_tac [][] 199 >- (srw_tac [][EXTENSION] >> 200 Cases_on ���t = {}��� 201 >- (first_x_assum (qspec_then ���s��� mp_tac) >> 202 srw_tac [][] >> 203 disj1_tac >> 204 srw_tac [][] >> 205 Cases_on ���f.dom = s��� >> srw_tac [][] >> 206 Cases_on ���f.cod = ������ >> srw_tac [][] >> 207 srw_tac [][IsTypedFun_def,HasFunType_def,MEMBER_NOT_EMPTY] ) >> 208 qexists_tac ���CHOICE t��� >> 209 srw_tac [][EQ_IMP_THM,CHOICE_DEF] >> 210 first_x_assum (qspec_then ���t��� mp_tac) >> 211 srw_tac [][] >> 212 qmatch_assum_rename_tac ���x ��� f.cod��� >> 213 first_x_assum 214 (qspecl_then [���TypedGraphFun (f.dom,f.cod) (K x)���, 215 ���TypedGraphFun (f.dom,f.cod) (K (CHOICE f.cod))���] mp_tac) >> 216 srw_tac [][CHOICE_DEF] >> 217 fsrw_tac [][morphism_component_equality,restrict_def] >> 218 qmatch_assum_abbrev_tac ���ff = gg��� >> 219 ���ff x = gg x��� by simp[] >> 220 pop_assum mp_tac >> 221 unabbrev_all_tac >> 222 qpat_x_assum ���x ��� f.cod��� mp_tac >> 223 simp_tac std_ss [] ) 224 >- (qmatch_assum_rename_tac ���y ��� U��� >> 225 qexists_tac ���TypedGraphFun (y,{x}) (K x)��� >> 226 srw_tac [][] ) >> 227 srw_tac [][TypedFun_ext] >> 228 rpt (qpat_x_assum ���IsTypedFun X��� mp_tac) >> 229 fsrw_tac [][IsTypedFun_def,HasFunType_def] 230QED 231 232(* 233val ens_cat_has_binary_products = Q.store_thm( 234"ens_cat_has_binary_products", 235`���U J. (INJ J {{(x,y) | x ��� a ��� y ��� b} | a ��� U ��� b ��� U} U) ��� has_binary_products (ens_cat U)`, 236srw_tac [][has_binary_products_thm,is_binary_product_thm] >> 237`J {(x,y) | x ��� a ��� y ��� b} ��� U` by fsrw_tac [DNF_ss][INJ_DEF] >> 238qmatch_assum_abbrev_tac `J axb ��� U` >> 239qmatch_assum_abbrev_tac `INJ J UU U` >> 240qexists_tac `TypedGraphFun (J axb, a) (��p. (LINV J UU axb)` >> 241LINV_DEF 242srw_tac [][] 243``TypedGraphFun ((J:('a # 'a set -> 'a set)) (a,b), a)`` 244``(LINV (J:(('a # 'a) set -> 'a set)) UU)`` 245type_of it 246*) 247 248val pre_inclusion_functor_def = Define` 249 pre_inclusion_functor u1 u2 = <| 250 dom := ens_cat u1; 251 cod := ens_cat u2; 252 map := I|>`; 253 254val pre_inclusion_functor_components = Q.store_thm( 255"pre_inclusion_functor_components", 256`���u1 u2. ((pre_inclusion_functor u1 u2).dom = ens_cat u1) ��� 257 ((pre_inclusion_functor u1 u2).cod = ens_cat u2) ��� 258 (���f. f ��� (ens_cat u1).mor ��� ((pre_inclusion_functor u1 u2)##f = f)) ��� 259 (���x. x ��� u1 ��� x ��� u2 ��� ((pre_inclusion_functor u1 u2)@@x = x))`, 260srw_tac [][pre_inclusion_functor_def,morf_def,objf_def] >> 261SELECT_ELIM_TAC >> 262conj_tac >- ( qexists_tac `x` >> srw_tac [][] ) >> 263srw_tac [][] >> 264pop_assum mp_tac >> 265fsrw_tac [][morphism_component_equality]); 266val _ = export_rewrites["pre_inclusion_functor_components"]; 267 268val inclusion_functor_def = Define` 269 inclusion_functor u1 u2 = mk_functor (pre_inclusion_functor u1 u2)`; 270 271val inclusion_functor_components = Q.store_thm( 272"inclusion_functor_components", 273`���u1 u2. ((inclusion_functor u1 u2).dom = ens_cat u1) ��� 274 ((inclusion_functor u1 u2).cod = ens_cat u2) ��� 275 (���f. f ��� (ens_cat u1).mor ��� ((inclusion_functor u1 u2)##f = f)) ��� 276 (���x. x ��� u1 ��� x ��� u2 ��� ((inclusion_functor u1 u2)@@x = x))`, 277srw_tac [][inclusion_functor_def]); 278val _ = export_rewrites["inclusion_functor_components"]; 279 280val is_functor_inclusion_functor = Q.store_thm( 281"is_functor_inclusion_functor", 282`���u1 u2. u1 ��� u2 ��� is_functor (inclusion_functor u1 u2)`, 283srw_tac [][inclusion_functor_def] >> 284srw_tac [][functor_axioms_def] >> 285fsrw_tac [][SUBSET_DEF] >- ( 286 qexists_tac `x` >> srw_tac [][] ) >> 287`(g o f) ��� (ens_cat u1).mor` by ( 288 srw_tac [][] >> fsrw_tac [][IsTypedFun_def] ) >> 289srw_tac [][]); 290val _ = export_rewrites["is_functor_inclusion_functor"]; 291 292val _ = export_theory(); 293