1open HolKernel Parse boolLib bossLib; 2 3open relationTheory pairTheory pred_setTheory combinTheory 4open cardinalTheory simpleSetCatTheory 5 6(* Abstract development of existence of final co-algebras, using new_type, 7 new_constant and axioms to emulate a locale. If this can be carried out 8 generically, the concrete approach for any given instance should be clear. 9 *) 10 11 12(* Mostly based on Rutten (TCS, 2000): 13 "Universal coalgebra: a theory of systems", 14 but with use of relators and choice of axioms from 15 Blanchette et al (ITP, 2014): 16 "Truly Modular (Co)datatypes for Isabelle/HOL" 17 *) 18 19val _ = new_theory "coalgAxioms"; 20 21val _ = app (ignore o hide) ["S", "W"] 22 23val IRULE = goal_assum o resolve_then.resolve_then resolve_then.Any mp_tac 24 25val _ = new_type("F", 1) 26val _ = new_constant("mapF", ���:('a -> 'b) -> 'a F -> 'b F���) 27val _ = new_constant("setF", ���:'a F -> 'a set���) 28 29val mapID = new_axiom("mapID", ���mapF (\x. x) = (\a. a)���) 30val mapO = new_axiom ("mapO", ���mapF f o mapF g = mapF (f o g)���) 31Theorem mapO' = SIMP_RULE (srw_ss()) [FUN_EQ_THM] mapO 32val set_map = new_axiom ("set_map", ���setF o mapF f = IMAGE f o setF ���) 33Theorem set_map' = SIMP_RULE (srw_ss()) [Once FUN_EQ_THM, EXTENSION] set_map 34val map_CONG = new_axiom ( 35 "map_CONG", 36 ���!f g y. (!x. x IN setF y ==> f x = g x) ==> mapF f y = mapF g y���) 37 38val _ = add_rule{block_style = (AroundEachPhrase, (PP.CONSISTENT, 0)), 39 fixity = Suffix 2100, paren_style = OnlyIfNecessary, 40 pp_elements = [TOK "���"], term_name = "UNCURRY"} (* UOK *) 41 42val _ = add_rule {block_style = (AroundEachPhrase, (PP.CONSISTENT, 0)), 43 fixity = Suffix 2100, paren_style = OnlyIfNecessary, 44 pp_elements = [TOK "���",TM,TOK"���"], term_name = "restr"}(* UOK*) 45 46Definition relF_def: 47 relF R x y <=> ?z. setF z SUBSET UNCURRY R /\ mapF FST z = x /\ mapF SND z = y 48End 49 50val relO = new_axiom ("relO", ���relF R O relF S RSUBSET relF (R O S)���) 51 52Theorem relO_EQ : 53 relF R O relF S = relF (R O S) 54Proof 55 irule RSUBSET_ANTISYM >> simp[relO] >> 56 simp[relF_def, FUN_EQ_THM, RSUBSET, O_DEF, SUBSET_DEF, FORALL_PROD] >> 57 rw[PULL_EXISTS] >> 58 fs[GSYM RIGHT_EXISTS_IMP_THM, SKOLEM_THM] >> 59 map_every qexists_tac [���mapF (\ (a,b). (a, f a b)) z���, 60 ���mapF (\ (a,b). (f a b, b)) z���] >> 61 simp[mapO', o_UNCURRY_R, o_ABS_R, set_map', EXISTS_PROD, PULL_EXISTS] >> 62 conj_tac >> irule map_CONG >> simp[FORALL_PROD] 63QED 64 65Theorem relEQ: 66 relF (=) = (=) 67Proof 68 simp[FUN_EQ_THM, relF_def, EQ_IMP_THM, FORALL_AND_THM, 69 SUBSET_DEF, FORALL_PROD] >> conj_tac 70 >- (simp[PULL_EXISTS] >> rpt strip_tac >> irule map_CONG>> 71 simp[FORALL_PROD]) >> 72 qx_gen_tac ���a��� >> qexists_tac ���mapF (\a. (a,a)) a��� >> 73 simp[mapO', o_ABS_R, mapID, set_map'] 74QED 75 76Theorem relF_inv[simp]: 77 relF (inv R) x y = relF R y x 78Proof 79 simp[relF_def, SUBSET_DEF, FORALL_PROD, EQ_IMP_THM, PULL_EXISTS] >> rw[] >> 80 qexists_tac ���mapF (\ (a,b). (b,a)) z���>> 81 simp[mapO', o_UNCURRY_R, o_ABS_R, set_map', EXISTS_PROD] >> rw[] >> 82 irule map_CONG >> simp[FORALL_PROD] 83QED 84 85Theorem rel_monotone: 86 (!a b. R a b ==> S a b) ==> (!A B. relF R A B ==> relF S A B) 87Proof 88 simp[relF_def, EXISTS_PROD, SUBSET_DEF, PULL_EXISTS, FORALL_PROD] >> 89 metis_tac[] 90QED 91 92Type system[pp] = ���:('a -> bool) # ('a -> 'a F)��� 93 94(* same as an "all" test *) 95Definition Fset_def: 96 Fset (A : 'a set) = { af | setF af SUBSET A } 97End 98 99Theorem map_preserves_INJ: 100 INJ f A B ==> INJ (mapF f) (Fset A) (Fset B) 101Proof 102 strip_tac >> drule_then assume_tac LINV_DEF >> 103 fs[INJ_IFF] >> simp[Fset_def, set_map', PULL_EXISTS, SUBSET_DEF] >> 104 simp[EQ_IMP_THM] >> rw[] >> 105 rename [���mapF f x = mapF f y���] >> 106 ���mapF (LINV f A) (mapF f x) = mapF (LINV f A) (mapF f y)��� by simp[] >> 107 fs[mapO'] >> 108 ���mapF (LINV f A o f) x = mapF (\x. x) x /\ 109 mapF (LINV f A o f) y = mapF (\x. x) y��� 110 by (conj_tac >> irule map_CONG >> simp[]) >> 111 fs[mapID] 112QED 113 114Theorem map_preserves_funs: 115 (!a. a IN A ==> f a IN B) ==> (!af. af IN Fset A ==> mapF f af IN Fset B) 116Proof 117 simp[Fset_def, SUBSET_DEF, set_map', PULL_EXISTS] 118QED 119 120Definition system_def: 121 system ((A,af) : 'a system) <=> 122 (!a. a IN A ==> af a IN Fset A) /\ !a. a NOTIN A ==> af a = ARB 123End 124 125Theorem UNIV_system[simp]: 126 system (UNIV,af) 127Proof 128 simp[system_def, Fset_def] 129QED 130 131Theorem system_members: 132 system (A,af) ==> !a b. a IN A /\ b IN setF (af a) ==> b IN A 133Proof 134 metis_tac[system_def |> SIMP_RULE (srw_ss()) [Fset_def, SUBSET_DEF]] 135QED 136 137Definition hom_def: 138 hom h (A,af) (B,bf) <=> 139 system (A,af) /\ system (B,bf) /\ 140 (!a. a IN A ==> h a IN B /\ bf (h a) = mapF h (af a)) /\ 141 (!a. a NOTIN A ==> h a = ARB) 142End 143 144Theorem homs_compose: 145 hom f As Bs /\ hom g Bs Cs ==> hom (restr (g o f) (FST As)) As Cs 146Proof 147 map_every PairCases_on [���As���, ���Bs���, ���Cs���] >> 148 simp[hom_def, restr_def, mapO'] >> rw[] >> 149 irule map_CONG >> rpt (dxrule_then strip_assume_tac system_members) >> 150 simp[] >> metis_tac[] 151QED 152 153Theorem hom_ID: 154 system (A, af) ==> 155 hom (restr (\x. x) A) (A,af) (A,af) 156Proof 157 csimp[hom_def, restr_def, system_def, Fset_def, SUBSET_DEF] >> rw[] 158 >- metis_tac[] >> 159 ���!x. x IN setF (af a) ==> (\x. if x IN A then x else ARB) x = (\x.x) x��� 160 by metis_tac[] >> 161 drule map_CONG >> simp[mapID] 162QED 163 164Definition epi_def: 165 epi f ((A,af):'a system) ((B,bf):'b system) (:'c) <=> 166 hom f (A,af) (B,bf) /\ 167 !C cf g h. hom g (B,bf) ((C,cf):'c system) /\ hom h (B,bf) (C,cf) /\ 168 restr (g o f) A = restr (h o f) A ==> g = h 169End 170 171Definition iso_def: 172 iso (A,af) (B,bf) <=> 173 ?f g. hom f (A,af) (B,bf) /\ hom g (B,bf) (A,af) /\ 174 (!a. a IN A ==> g (f a) = a) /\ 175 (!b. b IN B ==> f (g b) = b) 176End 177 178Theorem iso_SYM: 179 iso As Bs <=> iso Bs As 180Proof 181 map_every Cases_on [���As���, ���Bs���] >> simp[iso_def] >> metis_tac[] 182QED 183 184Theorem INJ_homs_mono: 185 hom f (A,af) (B,bf) /\ INJ f A B ==> 186 !C cf g h. 187 hom g (C,cf) (A,af) /\ hom h (C,cf) (A,af) /\ 188 f o g = f o h ==> g = h 189Proof 190 simp[INJ_IFF, hom_def] >> rw[FUN_EQ_THM] >> metis_tac[] 191QED 192 193Theorem SURJ_homs_epi: 194 hom f ((A,af):'a system) ((B,bf):'b system) /\ SURJ f A B ==> 195 epi f (A,af) (B,bf) (:'c) 196Proof 197 simp[SURJ_DEF, hom_def, FUN_EQ_THM, epi_def] >> rw[] >> 198 Cases_on ���x IN B��� >> simp[] >> 199 ���?a. a IN A /\ f a = x��� by metis_tac[] >> 200 fs[restr_def] >> metis_tac[] 201QED 202 203Definition Fpushout_def: 204 Fpushout ((A,af):'a system) ((B,bf):'b system) ((C,cf):'c system) f g 205 ((P,pf):'p system,i1,i2) (:'d) 206 <=> 207 hom f (A,af) (B,bf) /\ hom g (A,af) (C,cf) /\ hom i1 (B,bf) (P,pf) /\ 208 hom i2 (C,cf) (P,pf) /\ restr (i1 o f) A = restr (i2 o g) A /\ 209 !Q qf j1 j2. 210 hom j1 (B,bf) ((Q,qf):'d system) /\ hom j2 (C,cf) (Q,qf) /\ 211 restr (j1 o f) A = restr (j2 o g) A ==> 212 ?!u. hom u (P,pf) (Q,qf) /\ 213 restr (u o i1) B = j1 /\ 214 restr (u o i2) C = j2 215End 216 217Theorem hom_implies_restr: 218 hom f (A,af) Bs ==> restr f A = f 219Proof 220 Cases_on ���Bs��� >> simp[hom_def, restr_def, FUN_EQ_THM] >> metis_tac[] 221QED 222 223Theorem epi_Fpushout: 224 epi f (A,af) (B,bf) (:'c) <=> 225 Fpushout (A,af) (B,bf) (B,bf) f f ((B,bf),restr (\x.x) B,restr (\x.x) B) (:'c) 226Proof 227 simp[epi_def, Fpushout_def] >> Cases_on ���hom f (A,af) (B,bf)��� >> 228 simp[] >> ���system (A,af) /\ system (B,bf)��� by fs[hom_def] >> simp[hom_ID] >> 229 simp_tac (srw_ss() ++ boolSimps.CONJ_ss ++ SatisfySimps.SATISFY_ss) 230 [hom_implies_restr] >> 231 simp[EXISTS_UNIQUE_THM] >> metis_tac[] 232QED 233 234Theorem hom_shom: 235 hom f (A,af) (B,bf) ==> shom f A B 236Proof 237 simp[hom_def, shom_def] 238QED 239 240 241(* 242Theorem Spushout_Fpushout_IMP: 243 hom f (A,af) (B,bf) /\ hom g (A,af) (C,cf) /\ 244 Spushout A B C f g (P,i1,i2) (:'d) ==> 245 ?pf. Fpushout (A,af) (B,bf) (C,cf) f g ((P,pf),i1,i2) (:'d) 246Proof 247 rpt strip_tac >> 248 ���Spushout A B C f g (SPO A B C f g) (:'d)��� by metis_tac[hom_shom,Spushout_quotient] >> 249 fs[SPO_def] >> pop_assum mp_tac >> 250 qmatch_abbrev_tac ���Spushout _ _ _ _ _ (SPOq, SPOi1, SPOi2) _ ==> _��� >> strip_tac >> 251 252 simp[Fpushout_def, Spushout_def] >> rpt strip_tac >> 253 ���shom f A B /\ shom g A C /\ shom i1 B P /\ shom i2 C P��� 254 by metis_tac[hom_shom] >> simp[] >> 255 Cases_on ���restr (i1 o f) A = restr (i2 o g) A��� >> simp[] >> reverse eq_tac 256 >- (rw[] >> 257 ���shom j1 B Q /\ shom j2 C Q��� by metis_tac[hom_shom] >> 258 first_x_assum drule_all >> 259 CONV_TAC (LAND_CONV (SIMP_CONV (srw_ss()) [EXISTS_UNIQUE_THM])) >> 260 rw[] 261 reverse (Cases_on ���hom f (A,af) (B,bf)���) >> simp[] 262 >- (Cases_on ���shom f A B��� >> simp[] >> 263*) 264 265Theorem BIJ_homs_iso: 266 hom f (A,af) (B,bf) /\ BIJ f A B ==> iso (A,af) (B,bf) 267Proof 268 simp[hom_def, iso_def, BIJ_IFF_INV] >> rw[] >> 269 qexistsl_tac [���f���, ���restr g B���] >> simp[restr_applies] >> 270 reverse conj_tac >- simp[restr_def] >> 271 qx_gen_tac ���b��� >> strip_tac >> 272 ���bf b = bf (f (g b))��� by metis_tac[] >> pop_assum SUBST1_TAC >> 273 simp[mapO'] >> 274 ���mapF (restr g B o f) (af (g b)) = mapF (\x. x) (af (g b))��� 275 suffices_by simp[mapID] >> 276 irule map_CONG >> simp[restr_def] >> ���g b IN A��� by simp[] >> 277 metis_tac[system_members] 278QED 279 280 281 282Definition bisim_def: 283 bisim R (A,af) (B,bf) <=> 284 system (A,af) /\ system (B,bf) /\ 285 !a b. R a b ==> a IN A /\ b IN B /\ relF R (af a) (bf b) 286End 287 288Theorem bisim_system: 289 bisim R As Bs ==> system As /\ system Bs 290Proof 291 map_every Cases_on [���As���, ���Bs���] >> simp[bisim_def] 292QED 293 294Definition bisimilar_def: 295 bisimilar As Bs <=> ?R. bisim R As Bs 296End 297 298Theorem sbisimulation_projns_homo: 299 bisim R (A,af) (B,bf) <=> 300 ?Rf. 301 hom (restr FST (UNCURRY R)) (UNCURRY R, Rf) (A, af) /\ 302 hom (restr SND (UNCURRY R)) (UNCURRY R, Rf) (B, bf) 303Proof 304 rw[bisim_def, hom_def, EQ_IMP_THM, restr_applies, FORALL_PROD] >> simp[] 305 >- (fs[relF_def, GSYM RIGHT_EXISTS_IMP_THM, SKOLEM_THM, PULL_EXISTS, 306 SUBSET_DEF] >> 307 rename [���_ IN setF (RF _ _) ==> _ IN UNCURRY R���] >> 308 qexists_tac ���restr (UNCURRY RF) (UNCURRY R)��� >> csimp[restr_def] >> rw[] 309 >- metis_tac[] 310 >- (first_x_assum $ drule_then (strip_assume_tac o GSYM) >> 311 simp[] >> irule map_CONG >> simp[]) 312 >- (simp[system_def, SUBSET_DEF, Fset_def, FORALL_PROD] >> 313 fs[FORALL_PROD] >> metis_tac[]) 314 >- metis_tac[] >> 315 first_x_assum $ drule_then (strip_assume_tac o GSYM) >> 316 simp[] >> irule map_CONG >> simp[]) 317 >- metis_tac[] 318 >- metis_tac[] >> 319 simp[relF_def, SUBSET_DEF, FORALL_PROD] >> 320 qexists_tac ���Rf (a, b)��� >> rpt (first_x_assum drule) >> simp[] >> rw[] >> 321 fs[system_def, SUBSET_DEF, Fset_def, FORALL_PROD] 322 >- metis_tac[] 323 >- (irule map_CONG>> simp[restr_def,FORALL_PROD] >> metis_tac[]) 324 >- (irule map_CONG>> simp[restr_def,FORALL_PROD] >> metis_tac[]) 325QED 326 327Theorem lemma2_4_1: 328 hom (h o g) (A,af) (C,cf) /\ hom g (A,af) (B,bf) /\ SURJ g A B /\ 329 (!b. b NOTIN B ==> h b = ARB) ==> 330 hom h (B,bf) (C,cf) 331Proof 332 simp[hom_def] >> strip_tac >> qx_gen_tac ���b��� >> strip_tac >> 333 ���?a. a IN A /\ g a = b��� by metis_tac[SURJ_DEF] >> 334 rw[mapO'] 335QED 336 337Theorem lemma2_4_2: 338 hom (h o g) (A,af) (C,cf) /\ hom h (B,bf) (C,cf) /\ 339 (!a. a IN A ==> g a IN B) /\ (!a. a NOTIN A ==> g a = ARB) /\ 340 INJ h B C ==> 341 hom g (A,af) (B,bf) 342Proof 343 simp[hom_def] >> strip_tac >> qx_gen_tac ���a��� >> strip_tac >> 344 fs[GSYM mapO'] >> 345 last_assum (first_assum o mp_then (Pos hd) mp_tac) >> 346 ���bf (g a) IN Fset B /\ mapF g (af a) IN Fset B��� 347 suffices_by metis_tac[INJ_IFF, map_preserves_INJ] >> 348 simp[Fset_def, SUBSET_DEF, set_map', PULL_EXISTS] >> metis_tac[system_members] 349QED 350 351Theorem thm2_5: 352 hom h (A,af) (B,bf) <=> 353 (!a. a IN A ==> h a IN B) /\ (!a. a NOTIN A ==> h a = ARB) /\ 354 bisim (Gr h A) (A,af) (B,bf) 355Proof 356 simp[hom_def, bisim_def] >> 357 map_every Cases_on [���system (A,af)���, ���system(B,bf)���] >> simp[] >> 358 Cases_on ���!a. a NOTIN A ==> h a = ARB��� >> simp[] >> 359 reverse (Cases_on ���!a. a IN A ==> h a IN B��� >> simp[]) 360 >- metis_tac[] >> 361 simp[relF_def, SUBSET_DEF, FORALL_PROD] >> eq_tac 362 >- (rw[] >> qexists_tac ���mapF (\a. (a, h a)) (af a)��� >> 363 simp[mapO', o_ABS_R, mapID, set_map'] >> rw[] 364 >- metis_tac[system_members] >> 365 irule map_CONG >> simp[]) >> 366 rw[] >> first_x_assum (drule_then (strip_assume_tac o GSYM)) >> 367 simp[mapO'] >> irule map_CONG >> simp[FORALL_PROD] 368QED 369 370 371Theorem prop5_1: 372 system (A,af) ==> bisim (Delta A) (A,af) (A,af) 373Proof 374 strip_tac >> drule hom_ID >> simp[thm2_5, restr_applies] 375QED 376 377Theorem thm5_2[simp]: 378 bisim (inv R) Bs As <=> bisim R As Bs 379Proof 380 map_every PairCases_on [���As���, ���Bs���] >> simp[bisim_def] >> metis_tac[] 381QED 382 383Theorem lemma5_3: 384 hom f (A,af) (B,bf) /\ hom g (A,af) (C,cf) ==> 385 bisim (span A f g) (B,bf) (C,cf) 386Proof 387 csimp[hom_def, bisim_def, PULL_EXISTS] >> 388 rw[relF_def, SUBSET_DEF, FORALL_PROD] >> 389 rename [���a IN A���, ���mapF FST _ = mapF f (af a)���] >> 390 qexists_tac ���mapF (\a. (f a, g a)) (af a)���>> 391 simp[mapO', set_map', PULL_EXISTS, o_ABS_R] >> 392 simp_tac (bool_ss ++ boolSimps.ETA_ss) [] >> 393 metis_tac[system_members] 394QED 395 396(* Rutten, Thm 5.4 *) 397Theorem bisimulations_compose: 398 bisim R (A,af) (B,bf) /\ bisim Q (B,bf) (C,cf) ==> 399 bisim (Q O R) (A,af) (C,cf) 400Proof 401 rw[bisim_def] >> fs[O_DEF, GSYM relO_EQ] >> metis_tac[] 402QED 403 404Theorem thm5_4 = bisimulations_compose 405 406Theorem thm5_5: 407 (!R. R IN Rs ==> bisim R As Bs) /\ 408 system (As:'a system) /\ system (Bs:'b system) ==> 409 bisim (\a b. ?R. R IN Rs /\ R a b) As Bs 410Proof 411 tmCases_on ���As : 'a system��� ["A af"] >> 412 tmCases_on ���Bs : 'b system��� ["B bf"] >> 413 rw[bisim_def] >- metis_tac[] >- metis_tac[] >> 414 ntac 2 (first_x_assum $ drule_then strip_assume_tac) >> 415 irule rel_monotone >> simp[] >> metis_tac[] 416QED 417 418Theorem bisim_RUNION: 419 bisim R1 As Bs /\ bisim R2 As Bs ==> bisim (R1 RUNION R2) As Bs 420Proof 421 strip_tac >> 422 ���R1 RUNION R2 = (\a b. ?R. R IN {R1;R2} /\ R a b)��� 423 by dsimp[Ntimes FUN_EQ_THM 2, RUNION] >> 424 pop_assum SUBST1_TAC >> irule thm5_5 >> simp[DISJ_IMP_THM] >> 425 drule bisim_system >> simp[] 426QED 427 428Theorem prop5_7: 429 hom f (A,af) (B,bf) ==> 430 bisim (kernel A f) (A,af) (A,af) /\ kernel A f equiv_on A 431Proof 432 rpt strip_tac 433 >- (simp[kernel_graph]>> irule bisimulations_compose >> 434 simp[] >> metis_tac[thm2_5]) >> 435 simp[equiv_on_def] >> metis_tac[] 436QED 437 438 439Definition bquot_def: 440 bquot ((A,af):'a system) R : 'a set system = 441 (partition R A, 442 restr (\ap. mapF (eps R A) (af (CHOICE ap))) (partition R A)) 443End 444 445 446Theorem bquot_correct: 447 system (A,af) /\ bisim R (A,af) (A,af) /\ R equiv_on A ==> 448 system (bquot (A,af) R) /\ hom (eps R A) (A,af) (bquot (A,af) R) 449Proof 450 csimp[hom_def, bquot_def, restr_applies] >> rw[eps_partition] 451 >- (simp[system_def, Fset_def, SUBSET_DEF, restr_applies, set_map', 452 PULL_EXISTS] >>reverse conj_tac 453 >- simp[restr_def] >> 454 qx_gen_tac ���ap��� >> strip_tac >> qx_gen_tac ���a��� >> 455 DEEP_INTRO_TAC CHOICE_INTRO >> conj_tac 456 >- metis_tac[EMPTY_NOT_IN_partition, MEMBER_NOT_EMPTY] >> 457 qx_gen_tac ���a0��� >> rpt strip_tac >> irule eps_partition >> 458 metis_tac[system_members, partition_SUBSET, SUBSET_DEF]) 459 >- (DEEP_INTRO_TAC CHOICE_INTRO >> conj_tac 460 >- metis_tac[eps_partition, EMPTY_NOT_IN_partition, MEMBER_NOT_EMPTY] >> 461 qx_gen_tac ���a'��� >> simp[eps_def] >> strip_tac >> 462 fs[sbisimulation_projns_homo] >> rpt (qpat_x_assum ���hom _ _ _ ��� mp_tac) >> 463 simp[hom_def, FORALL_PROD, restr_applies] >> rw[] >> 464 ���af a = mapF (restr FST (UNCURRY R)) (Rf (a, a')) /\ 465 af a' = mapF (restr SND (UNCURRY R)) (Rf (a, a'))��� by simp[] >> 466 simp[mapO'] >> irule map_CONG >> simp[FORALL_PROD] >> 467 qx_genl_tac [���a1���, ���a2���] >> strip_tac >> ���(a,a') IN UNCURRY R��� by simp[]>> 468 ���(a1,a2) IN UNCURRY R��� by metis_tac[system_members] >> 469 pop_assum mp_tac >> simp[restr_applies, eps_def] >> 470 strip_tac >> ���a1 IN A /\ a2 IN A��� by metis_tac[] >> 471 simp[EXTENSION] >> qx_gen_tac ���aa��� >> Cases_on ���aa IN A��� >> simp[] >> 472 prove_tac[equiv_on_def]) >> 473 simp[eps_def] 474QED 475 476Theorem prop5_8 = bquot_correct 477 478Definition coequalizer_def: 479 coequalizer ((A,af):'a system) ((B,bf):'b system) f1 f2 ((C,cf), g) (:'d) <=> 480 hom f1 (A,af) (B,bf) /\ hom f2 (A,af) (B,bf) /\ 481 hom g (B,bf) ((C,cf):'c system) /\ restr (g o f1) A = restr (g o f2) A /\ 482 !h D df. 483 hom h (B,bf) ((D,df):'d system) /\ restr (h o f1) A = restr (h o f2) A ==> 484 ?!u. hom u (C,cf) (D,df) /\ h = restr (u o g) B 485End 486 487Theorem coequalizer_thm = 488 coequalizer_def |> SPEC_ALL 489 |> Q.INST [���C'��� |-> ���FST (Cs : 'c system)���, 490 ���cf��� |-> ���SND (Cs : 'c system)���] 491 |> SIMP_RULE (srw_ss()) [] 492 493Theorem bquot_coequalizer: 494 system (A,af) /\ bisim R (A,af) (A,af) /\ R equiv_on A ==> 495 ?Rf. 496 coequalizer (UNCURRY R, Rf) 497 (A,af) 498 (restr FST (UNCURRY R)) 499 (restr SND (UNCURRY R)) 500 (bquot (A,af) R, eps R A) 501 (:'d) 502Proof 503 Cases_on ���bquot (A,af) R��� >> 504 simp[coequalizer_def, sbisimulation_projns_homo] >> rw[] >> 505 first_assum IRULE >> rw[] 506 >- metis_tac[bquot_correct,sbisimulation_projns_homo] 507 >- (simp[Once FUN_EQ_THM, restr_def, FORALL_PROD] >> 508 rw[EXTENSION] >> simp[eps_def] >> rw[] 509 >- (fs[equiv_on_def] >> metis_tac[]) 510 >- (fs[hom_def, FORALL_PROD, restr_def] >> metis_tac[]) 511 >- (fs[hom_def, FORALL_PROD, restr_def] >> metis_tac[])) 512 >- (fs[bquot_def] >> rw[] >> 513 fs[FUN_EQ_THM, restr_def, FORALL_PROD, EXISTS_UNIQUE_THM] >> 514 conj_tac 515 >- (qexists_tac ���restr (\p. h (CHOICE p)) (partition R A)��� >> conj_tac 516 >- (simp[hom_def, restr_def, mapO', o_ABS_L] >> rw[] 517 >- (simp[system_def] >> rw[] >> 518 irule map_preserves_funs >> qexists_tac ���A��� >> 519 simp[eps_partition] >> DEEP_INTRO_TAC CHOICE_INTRO >> rw[] 520 >- (rename [���A0 IN partition R A���] >> 521 ���A0 <> {}��� suffices_by metis_tac[MEMBER_NOT_EMPTY] >> 522 metis_tac[EMPTY_NOT_IN_partition]) >> 523 rename [���a0 IN A0���, ���A0 IN partition _ _���] >> 524 ���a0 IN A��� suffices_by metis_tac[system_def] >> 525 metis_tac[partition_SUBSET, SUBSET_DEF]) 526 >- fs[hom_def] 527 >- (���CHOICE ap IN A��� suffices_by metis_tac[hom_def] >> 528 DEEP_INTRO_TAC CHOICE_INTRO >> rw[] 529 >- (rename [���A0 IN partition R A���] >> 530 ���A0 <> {}��� suffices_by metis_tac[MEMBER_NOT_EMPTY] >> 531 metis_tac[EMPTY_NOT_IN_partition]) >> 532 rename [���a0 IN A0���, ���A0 IN partition _ _���] >> 533 ���a0 IN A��� suffices_by metis_tac[system_def] >> 534 metis_tac[partition_SUBSET, SUBSET_DEF]) >> 535 DEEP_INTRO_TAC CHOICE_INTRO >> rw[] 536 >- (rename [���A0 IN partition R A���] >> 537 ���A0 <> {}��� suffices_by metis_tac[MEMBER_NOT_EMPTY] >> 538 metis_tac[EMPTY_NOT_IN_partition]) >> 539 rename [���a0 IN A0���, ���A0 IN partition R A���] >> 540 ���a0 IN A��� by metis_tac[SUBSET_DEF, partition_SUBSET] >> 541 fs[hom_def] >> irule map_CONG >> qx_gen_tac ���a1��� >> strip_tac >> 542 ���a1 IN A��� by metis_tac[system_members] >> 543 simp[eps_partition] >> simp[eps_def] >> 544 DEEP_INTRO_TAC CHOICE_INTRO >> conj_tac 545 >- (simp[] >> metis_tac[equiv_on_def]) >> 546 simp[] >> metis_tac[]) >> 547 reverse (rw[]) >- fs[hom_def] >> 548 simp[eps_partition, restr_def] >> simp[eps_def] >> 549 DEEP_INTRO_TAC CHOICE_INTRO >> conj_tac 550 >- (simp[] >> metis_tac[equiv_on_def]) >> 551 simp[] >> metis_tac[]) >> 552 qx_genl_tac [���u1���, ���u2���] >> strip_tac >> qx_gen_tac ���ap��� >> 553 CCONTR_TAC >> reverse (Cases_on ���ap IN partition R A���) 554 >- (qpat_x_assum ���_ <> _��� mp_tac >> fs[hom_def]) >> 555 ���?a. a IN ap��� 556 by metis_tac[MEMBER_NOT_EMPTY, EMPTY_NOT_IN_partition] >> 557 ���a IN A��� by metis_tac[partition_SUBSET, SUBSET_DEF] >> 558 ���eps R A a = ap��� 559 by (simp[eps_def] >> simp[EXTENSION] >> 560 fs[partition_def] >> rw[] >> fs[] >> fs[equiv_on_def] >> 561 metis_tac[]) >> 562 metis_tac[]) 563QED 564 565Theorem prop5_9_1: 566 hom (restr f A) (A,af) (B,bf) /\ bisim R (A,af) (A,af) ==> 567 bisim (RIMAGE f A R) (B,bf) (B,bf) 568Proof 569 simp[RIMAGE_Gr] >> strip_tac >> IRULE bisimulations_compose >> 570 IRULE bisimulations_compose >> 571 simp[] >> goal_assum (drule_at (Pos (el 2))) >> fs[thm2_5] 572QED 573 574Theorem prop5_9_2: 575 hom (restr f A) (A,af) (B,bf) /\ bisim Q (B,bf) (B,bf) ==> 576 bisim (RINV_IMAGE f A Q) (A,af) (A,af) 577Proof 578 simp[RINV_IMAGE_Gr] >> strip_tac >> IRULE bisimulations_compose >> 579 IRULE bisimulations_compose >> simp[] >> first_assum IRULE >> 580 fs[thm2_5] 581QED 582 583(* Section 6: Subsystems *) 584 585Definition subsystem_def: 586 subsystem V (A,af) <=> 587 system (A,af) /\ V SUBSET A /\ ?vf. hom (restr (\x.x) V) (V,vf) (A,af) 588End 589 590Theorem subsystem_refl[simp]: 591 system (A,af) ==> subsystem A (A,af) 592Proof 593 simp[subsystem_def] >> strip_tac >> IRULE hom_ID >> simp[] 594QED 595 596Theorem prop6_1: 597 V SUBSET A /\ hom (restr (\x.x) V) (V,kf) (A,af) /\ 598 hom (restr (\x.x) V) (V,lf) (A,af) ==> 599 kf = lf 600Proof 601 simp[hom_def, restr_def] >> rw[] >> simp[FUN_EQ_THM] >> qx_gen_tac ���v��� >> 602 reverse (Cases_on ���v IN V���) >- fs[system_def] >> 603 ���(!a. a IN V ==> 604 mapF (\x. if x IN V then x else ARB) (kf a) = mapF (\x. x) (kf a)) /\ 605 !a. a IN V ==> 606 mapF (\x. if x IN V then x else ARB) (lf a) = mapF (\x. x) (lf a)��� 607 by (rw[] >> irule map_CONG >> simp[] >> metis_tac[system_members]) >> 608 fs[mapID] 609QED 610 611Theorem prop6_2: 612 system (A,af) ==> 613 (subsystem V (A,af) <=> V SUBSET A /\ bisim (Delta V) (A,af) (A,af)) 614Proof 615 simp[subsystem_def] >> strip_tac >> eq_tac 616 >- (csimp[PULL_EXISTS] >> rpt strip_tac >> 617 ���hom (restr (\x.x) V) (V,restr af V) (A,af)��� 618 by (fs[hom_def, restr_def] >> fs[system_def, Fset_def, SUBSET_DEF] >> 619 rw[] >- (fs[set_map'] >> metis_tac[]) >> 620 simp[mapO', o_ABS_R] >> irule map_CONG >> simp[] >> rw[]>> fs[]) >> 621 ���vf = restr af V��� by metis_tac[prop6_1] >> 622 qpat_x_assum ���hom _ _ _ ��� mp_tac >> 623 csimp[bisim_def, thm2_5, restr_def]) >> 624 csimp[bisim_def, SUBSET_DEF] >> strip_tac >> 625 qexists_tac ���restr af V��� >> 626 simp[hom_def, restr_applies] >> 627 conj_asm1_tac 628 >- (fs[system_def, Fset_def, relF_def, SUBSET_DEF, FORALL_PROD, restr_def] >> 629 rw[] >> 630 first_x_assum $ drule_then strip_assume_tac >> 631 rename [���mapF FST z = af a���]>> 632 ���setF (mapF FST z) = setF (af a)��� by simp[] >> 633 pop_assum mp_tac >> REWRITE_TAC [EXTENSION, set_map'] >> 634 simp[EXISTS_PROD]) >> 635 reverse conj_tac >- simp[restr_def] >> 636 qx_gen_tac ���a��� >> strip_tac >> 637 ���mapF (restr (\x. x) V) (af a) = mapF (\x. x) (af a)��� 638 suffices_by simp[mapID] >> 639 irule map_CONG >> drule system_members >> csimp[restr_def] >> metis_tac[] 640QED 641 642Theorem subsystem_system: 643 subsystem V (A,af) ==> system (V, restr af V) 644Proof 645 strip_tac >> ���system (A,af)��� by fs[subsystem_def] >> 646 fs[prop6_2, bisim_def] >> 647 fs[system_def, SUBSET_DEF, Fset_def, restr_def] >> 648 rpt strip_tac >> first_x_assum drule >> 649 csimp[relF_def, PULL_EXISTS, SUBSET_DEF, FORALL_PROD] >> rw[] >> 650 rename [���mapF FST rr = af a���] >> 651 ���setF (mapF FST rr) = setF (af a)��� by simp[] >> pop_assum mp_tac >> 652 simp[EXTENSION, set_map', EXISTS_PROD] >> rename [���x IN setF (af a)���] >> 653 disch_then (qspec_then ���x��� mp_tac) >> simp[] >> metis_tac[] 654QED 655 656Theorem thm6_3_1: 657 hom f (A,af) (B,bf) /\ subsystem V (A,af) ==> 658 subsystem (IMAGE f V) (B, bf) 659Proof 660 strip_tac >> 661 ���system (A, af) /\ system (B,bf)��� by fs[hom_def] >> 662 ���system (V, restr af V)��� by metis_tac[subsystem_system] >> 663 simp[prop6_2, Delta_IMAGE] >> conj_tac 664 >- fs[hom_def, subsystem_def, SUBSET_DEF, PULL_EXISTS] >> 665 irule prop5_9_1 >> qexists_tac ���restr af V��� >> fs[prop6_2] >> 666 conj_tac >- (fs[bisim_def] >> simp[restr_def]) >> 667 fs[hom_def] >> simp[restr_def] >> fs[SUBSET_DEF] >> 668 rpt strip_tac >> irule map_CONG >> simp[] >> 669 metis_tac[system_members, restr_def] 670QED 671 672Theorem thm6_3_2: 673 hom f (A,af) (B,bf) /\ subsystem W (B,bf) ==> 674 subsystem (PREIMAGE f W INTER A) (A, af) 675Proof 676 strip_tac >> 677 ���system (A, af) /\ system (B, bf) /\ system (W,restr bf W)��� 678 by metis_tac[hom_def, subsystem_system] >> 679 simp[prop6_2, Delta_INTER] >> 680 csimp[bisim_def, RINTER, relF_def, SUBSET_DEF, FORALL_PROD] >> 681 qx_gen_tac ���a0��� >> strip_tac >> 682 qexists_tac ���mapF (\a. (a,a)) (af a0)��� >> 683 simp[mapO', o_ABS_R, mapID, set_map'] >> 684 qx_gen_tac ���a'��� >> strip_tac >> reverse conj_tac 685 >- metis_tac[system_members] >> 686 fs[hom_def] >> 687 ���bf (f a0) = mapF f (af a0)��� by metis_tac[] >> 688 ���restr bf W (f a0) = mapF f (af a0)��� by simp[restr_def] >> 689 pop_assum (mp_tac o Q.AP_TERM ���setF���) >> 690 simp[EXTENSION, set_map'] >> 691 ���setF (restr bf W (f a0)) SUBSET W��� 692 by (simp[SUBSET_DEF] >> metis_tac[system_members]) >> 693 strip_tac >> 694 ���f a' IN setF (restr bf W (f a0))��� suffices_by metis_tac[SUBSET_DEF] >> 695 simp[] >> metis_tac[] 696QED 697 698Theorem subsystem_UNION: 699 system (A,af) /\ (!V. V IN VS ==> subsystem V (A,af)) ==> 700 subsystem (BIGUNION VS) (A, af) 701Proof 702 csimp[prop6_2, BIGUNION_SUBSET] >> strip_tac >> 703 ���Delta (BIGUNION VS) = (\a b. ?V. V IN (IMAGE Delta VS) /\ V a b)��� 704 by (simp[Ntimes FUN_EQ_THM 2, PULL_EXISTS] >> metis_tac[]) >> 705 pop_assum SUBST1_TAC >> irule thm5_5 >> simp[PULL_EXISTS] 706QED 707 708Theorem subsystem_ALT: 709 subsystem V (A,af) <=> 710 V SUBSET A /\ system(A,af) /\ hom (restr (\x.x) V) (V, restr af V) (A,af) 711Proof 712 eq_tac 713 >- (strip_tac >> drule_then assume_tac subsystem_system >> 714 ���system (A,af) /\ V SUBSET A��� by fs[subsystem_def] >> simp[] >> 715 simp[hom_def] >> reverse conj_tac >- simp[restr_def] >> 716 simp[restr_applies] >> 717 ���!a. a IN V ==> mapF (restr (\x.x) V) (af a) = mapF (\x.x) (af a)��� 718 suffices_by (simp[mapID] >> fs[subsystem_def, SUBSET_DEF]) >> 719 rw[] >> irule map_CONG >> simp[restr_def] >> 720 metis_tac[system_members, restr_def]) >> 721 simp[subsystem_def] >> metis_tac[] 722QED 723 724Theorem subsystem_INTER: 725 system (A,af) /\ (!V. V IN VS ==> subsystem V (A,af)) /\ VS <> {} ==> 726 subsystem (BIGINTER VS) (A, af) 727Proof 728 strip_tac >> simp[subsystem_ALT] >> rw[] 729 >- fs[BIGINTER_SUBSET, subsystem_def] >> 730 rw[hom_def, restr_applies] 731 >- (simp[system_def, PULL_EXISTS, restr_def, Fset_def, SUBSET_DEF, 732 AllCaseEqs()] >> rw[] 733 >- (rename [���V IN VS���, ���v IN V���, ���v IN setF (af v0)���] >> 734 ���system (V,restr af V)��� by metis_tac[subsystem_system] >> 735 metis_tac[system_members, restr_def]) >> 736 metis_tac[]) 737 >- metis_tac [MEMBER_NOT_EMPTY, subsystem_def, SUBSET_DEF] 738 >- (���mapF (restr (\x.x) (BIGINTER VS)) (af a) = mapF (\x.x) (af a)��� 739 suffices_by simp[mapID] >> 740 irule map_CONG >> 741 ���!x. x IN setF (af a) ==> x IN BIGINTER VS��� 742 suffices_by simp[restr_applies] >> rw[] >> 743 rename [���V IN VS���, ���v IN V���, ���v IN setF (af v0)���] >> 744 ���v0 IN V��� by simp[] >> 745 metis_tac[system_members, restr_def, subsystem_system]) >> 746 simp[restr_def] >> metis_tac[] 747QED 748 749Theorem subsystem_INTER2 = 750 subsystem_INTER |> Q.INST [���VS��� |-> ���{V1;V2}���] 751 |> SIMP_RULE (srw_ss()) [DISJ_IMP_THM, FORALL_AND_THM] 752 753Definition genS_def: 754 genS As X = BIGINTER { V | subsystem V As /\ X SUBSET V } 755End 756 757Theorem genS_correct: 758 system (A,af) /\ X SUBSET A ==> subsystem (genS (A,af) X) (A,af) 759Proof 760 simp[genS_def] >> strip_tac >> 761 irule subsystem_INTER >> simp[EXTENSION] >> IRULE subsystem_refl >> 762 simp[] 763QED 764 765Definition bounded_def: 766 bounded (:'a) (:'b) = 767 !a A af. system ((A,af):'a system) /\ a IN A ==> 768 ?f V:'b set. INJ f (genS (A,af) {a}) V 769End 770 771(* Section 7 *) 772Theorem iso_inj_hom: 773 iso (A,af) (B,bf) /\ hom h (A,af) (C,cf) /\ INJ h A C ==> 774 ?j. hom j (B,bf) (C,cf) /\ INJ j B C 775Proof 776 rw[iso_def] >> 777 rename [���hom f (A,af) (B,bf)���, ���hom invf (B,bf) (A,af)���, ���INJ h A C���] >> 778 qexists_tac ���restr (h o invf) B��� >> fs[hom_def, mapO', restr_applies] >> 779 rpt conj_tac 780 >- (rpt strip_tac >> irule map_CONG >> 781 metis_tac[system_members, restr_applies]) 782 >- simp[restr_def] >> 783 fs[INJ_IFF, restr_def] >> metis_tac[] 784QED 785 786Theorem thm7_1: 787 hom f (A,af) (B,bf) ==> 788 hom f (A,af) (IMAGE f A,restr bf (IMAGE f A)) /\ 789 (!g h C cf. hom g (IMAGE f A,restr bf (IMAGE f A)) (C,cf) /\ 790 hom h (IMAGE f A,restr bf (IMAGE f A)) (C,cf) /\ 791 restr (h o f) A = restr (g o f) A ==> h = g) /\ 792 hom (eps (kernel A f) A) (A,af) (bquot (A,af) (kernel A f)) /\ 793 hom (restr (\x.x) (IMAGE f A)) 794 (IMAGE f A, restr bf (IMAGE f A)) 795 (B,bf) /\ 796 iso (IMAGE f A, restr bf (IMAGE f A)) 797 (bquot (A,af) (kernel A f)) /\ 798 ?mu. hom mu (bquot (A,af) (kernel A f)) (B,bf) /\ 799 INJ mu (FST (bquot (A,af) (kernel A f))) B 800Proof 801 strip_tac >> ���system (A,af) /\ system (B,bf)��� by fs[hom_def] >> 802 drule_then (qspec_then ���A��� mp_tac) thm6_3_1 >> simp[] >> 803 simp[subsystem_ALT] >> strip_tac >> 804 conj_asm1_tac 805 >- (irule lemma2_4_2 >> rw[] >- fs[hom_def] >> 806 qexistsl_tac [���B���, ���bf���, ���restr (\x.x) (IMAGE f A)���] >> 807 qabbrev_tac ���ss = IMAGE f A��� >> 808 ���!a. a IN A ==> f a IN ss��� by metis_tac[IN_IMAGE] >> 809 rw[] 810 >- (simp[INJ_IFF, PULL_EXISTS, restr_def] >> fs[SUBSET_DEF]) 811 >- (simp[hom_def, restr_def] >> reverse conj_tac >- fs[hom_def] >> 812 fs[hom_def] >> rw[] >> irule map_CONG >> simp[] >> rw[] >> 813 metis_tac[system_members, IN_IMAGE])) >> 814 conj_asm1_tac 815 >- (���SURJ f A (IMAGE f A)��� suffices_by metis_tac[SURJ_homs_epi, epi_def] >> 816 simp[SURJ_DEF]) >> 817 conj_asm1_tac >- metis_tac[bquot_correct, prop5_7] >> 818 conj_asm1_tac 819 >- (drule_then strip_assume_tac prop5_7 >> 820 drule_all_then strip_assume_tac 821 (INST_TYPE [delta |-> beta] bquot_coequalizer) >> 822 drule_then drule (cj 5 (iffLR coequalizer_thm)) >> 823 impl_tac >- simp[FUN_EQ_THM, restr_def, FORALL_PROD] >> 824 simp[EXISTS_UNIQUE_THM] >> 825 disch_then (CONJUNCTS_THEN2 (qx_choose_then ���u��� strip_assume_tac) 826 strip_assume_tac) >> 827 ���?Qt qf. bquot (A,af) (kernel A f) = (Qt,qf)��� 828 by metis_tac[pair_CASES] >> 829 ���SURJ u Qt (IMAGE f A)��� 830 by (qabbrev_tac ���imgfA = IMAGE f A��� >> simp[SURJ_DEF, PULL_EXISTS] >> 831 conj_tac >- fs[hom_def] >> 832 qx_gen_tac ���b��� >> strip_tac >> 833 ���?a. a IN A /\ f a = b��� by metis_tac[IN_IMAGE] >> 834 pop_assum (SUBST1_TAC o SYM) >> 835 qpat_x_assum ���f = restr _ A��� 836 (assume_tac o SIMP_RULE (srw_ss()) [FUN_EQ_THM]) >> 837 simp[] >> simp[restr_def] >> metis_tac[hom_def, FST]) >> 838 ���INJ u Qt (IMAGE f A)��� 839 by (qabbrev_tac ���imgfA = IMAGE f A��� >> simp[INJ_DEF] >> 840 conj_tac >- fs[hom_def] >> qx_genl_tac [���ap1���, ���ap2���]>> 841 rpt strip_tac >> CCONTR_TAC >> 842 fs[bquot_def] >> 843 ���(?a1. a1 IN ap1) /\ ?a2. a2 IN ap2��� 844 by metis_tac[MEMBER_NOT_EMPTY, EMPTY_NOT_IN_partition] >> 845 ���a1 IN A /\ a2 IN A��� by metis_tac[partition_SUBSET, SUBSET_DEF] >> 846 rw[] >> fs[partition_def] >> rw[] >> fs[] >> 847 ���a1 <> a2 /\ f a1 <> f a2��� by (rpt strip_tac >> fs[]) >> 848 full_simp_tac (bool_ss ++ boolSimps.CONJ_ss)[] >> 849 qpat_x_assum ���f = restr _ _ ��� 850 (ASSUME_TAC o SIMP_RULE (srw_ss()) [FUN_EQ_THM]) >> 851 pop_assum (fn th => qspec_then ���a1��� mp_tac th >> 852 qspec_then ���a2��� mp_tac th) >> 853 csimp[restr_def, eps_def] >> 854 fs[AC CONJ_ASSOC CONJ_COMM] >> metis_tac[]) >> 855 simp[] >> 856 irule (iffLR iso_SYM) >> irule BIJ_homs_iso >> 857 fs[] >> qexists_tac ���u��� >> simp[BIJ_DEF]) >> 858 Cases_on ���bquot (A,af) (kernel A f)��� >> simp[] >> 859 drule_then (drule_then irule) iso_inj_hom >> 860 simp[INJ_IFF, restr_applies, PULL_EXISTS] >> fs[hom_def] 861QED 862 863Theorem thm7_2: 864 hom f (A,af) (B,bf) /\ bisim R (A,af) (A,af) /\ R RSUBSET kernel A f /\ 865 R equiv_on A ==> 866 ?!fbar. 867 hom fbar (bquot (A,af) R) (B,bf) /\ f = restr (fbar o eps R A) A 868Proof 869 strip_tac >> 870 ���system (A,af)��� by fs[hom_def] >> 871 drule_all_then (qx_choose_then ���Rf��� strip_assume_tac) 872 (INST_TYPE [delta |-> beta] bquot_coequalizer) >> 873 fs[coequalizer_thm] >> first_x_assum irule >> simp[] >> 874 fs[restr_def, FUN_EQ_THM, RSUBSET, FORALL_PROD] >> metis_tac[] 875QED 876 877Theorem thm7_3: 878 system (A,af) /\ subsystem B (A,af) /\ bisim R (A,af) (A,af) /\ 879 R equiv_on A /\ 880 Abbrev(TR = { a | a IN A /\ ?b. b IN B /\ R a b }) 881 ==> 882 subsystem TR (A,af) /\ 883 let Q = CURRY (UNCURRY R INTER (B CROSS B)) 884 in 885 bisim Q (B,restr af B) (B,restr af B) /\ Q equiv_on B /\ 886 iso (bquot (B,restr af B) Q) (bquot (TR,restr af TR) R) 887Proof 888 strip_tac >> conj_asm1_tac 889 >- (���TR = IMAGE (restr FST (UNCURRY R)) 890 (PREIMAGE (restr SND (UNCURRY R)) B INTER UNCURRY R)��� 891 by (simp[EXTENSION, Abbr���TR���, EXISTS_PROD, restr_def] >> csimp[] >> 892 metis_tac[bisim_def]) >> 893 simp[] >> irule thm6_3_1 >> fs[sbisimulation_projns_homo] >> 894 first_assum (goal_assum o resolve_then Any mp_tac) >> 895 irule thm6_3_2 >> metis_tac[]) >> 896 REWRITE_TAC[LET_FORALL_ELIM] >> simp_tac std_ss [S_ABS_R] >> 897 ntac 2 strip_tac >> conj_asm1_tac 898 >- (fs[sbisimulation_projns_homo] >> 899 simp[GSYM sbisimulation_projns_homo] >> 900 ���Q = RINV_IMAGE (��x.x) B R��� 901 by (simp[FUN_EQ_THM, RINV_IMAGE_def, Abbr���Q���] >> metis_tac[]) >> 902 simp[] >> irule prop5_9_2 >> simp[sbisimulation_projns_homo] >> 903 fs[subsystem_ALT] >> metis_tac[]) >> 904 conj_asm1_tac 905 >- (fs[equiv_on_def, Abbr���Q���, subsystem_def] >> metis_tac[SUBSET_DEF]) >> 906 qabbrev_tac ���epsR = eps R A ��� >> 907 ���!a. a IN B ==> a IN A��� by fs[subsystem_def, SUBSET_DEF] >> 908 ���IMAGE (restr epsR B) B = IMAGE epsR TR��� 909 by (simp[Abbr���TR���, Once EXTENSION] >> csimp[restr_applies] >> 910 qx_gen_tac ���qt��� >> csimp[eps_def, Abbr���epsR���] >> 911 csimp[] >> eq_tac >> rw[] >> 912 simp[Once EXTENSION, PULL_EXISTS] >> 913 fs[equiv_on_def] >> metis_tac[]) >> 914 ���_ = partition R TR��� 915 by (simp[Once EXTENSION, Abbr���epsR���, Abbr���TR���, eps_def] >> 916 csimp[PULL_EXISTS, partition_def] >> qx_gen_tac ���qt��� >> 917 eq_tac >> rw[] >> 918 ntac 3 (first_assum (goal_assum o resolve_then Any mp_tac)) >> 919 simp[Once EXTENSION] >> fs[equiv_on_def] >> metis_tac[]) >> 920 pop_assum (assume_tac o SYM) >> 921 ���kernel B (restr epsR B) = Q��� 922 by (simp[Abbr���epsR���, Abbr���Q���, Once FUN_EQ_THM] >> 923 csimp[Once FUN_EQ_THM, kernel_def, restr_applies] >> 924 csimp[eps_def] >> fs[equiv_on_def] >> simp[Once EXTENSION] >> 925 metis_tac[]) >> 926 pop_assum (SUBST1_TAC o SYM) >> 927 irule (iffLR iso_SYM) >> 928 Cases_on ���bquot (TR, restr af TR) R ��� >> 929 rename [���bquot (TR, restr af TR) R = (qt,qtf)���] >> 930 ���qt = IMAGE (restr epsR B) B��� by fs[bquot_def] >> pop_assum SUBST_ALL_TAC >> 931 ���restr qtf (IMAGE (restr epsR B) B) = qtf��� 932 by (fs[bquot_def] >> rw[] >> simp[Once FUN_EQ_THM] >> 933 qx_gen_tac ���aF��� >> reverse (Cases_on ���aF IN IMAGE (restr epsR B) B���) 934 >- (ONCE_REWRITE_TAC[restr_def] >> simp_tac bool_ss [] >> 935 ASM_REWRITE_TAC[]) >> 936 simp[restr_applies]) >> 937 first_assum (ONCE_REWRITE_TAC o single o SYM) >> irule (cj 5 thm7_1) >> 938 qexists_tac ���IMAGE (restr epsR B) B��� >> 939 qpat_assum ���bquot _ _ = (_, _)��� (REWRITE_TAC o single o SYM) >> 940 simp_tac (srw_ss())[hom_def,bquot_def, restr_applies] >> 941 simp[] >> rw[] 942 >- metis_tac[subsystem_system] 943 >- (csimp[system_def, restr_applies, PULL_EXISTS] >> rw[] 944 >- (irule map_preserves_funs >> 945 csimp[eps_def, Abbr���epsR���, restr_applies] >> 946 qexists_tac ���TR��� >> simp[] >> rw[] 947 >- (fs[Abbr���TR���, equiv_on_def] >> simp[Once EXTENSION] >> 948 metis_tac[]) >> 949 ���system (TR,restr af TR)��� by metis_tac[subsystem_system] >> 950 fs[system_def] >> first_x_assum irule >> 951 simp[Abbr���TR���] >> DEEP_INTRO_TAC CHOICE_INTRO >> simp[] >> 952 fs[equiv_on_def] >> metis_tac[]) >> 953 csimp[restr_def] >> metis_tac[]) 954 >- (csimp[Abbr���epsR���, restr_applies] >> metis_tac[]) 955 >- (rename [���partition R _ = IMAGE _ B���, ���b IN B���] >> 956 ���epsR b IN IMAGE (restr epsR B) B��� 957 by (csimp[restr_applies] >> metis_tac[]) >> 958 simp[restr_applies] >> 959 ���CHOICE (epsR b) IN TR��� 960 by (DEEP_INTRO_TAC CHOICE_INTRO >> 961 simp[Abbr���epsR���, Abbr���TR���, eps_def] >> 962 fs[equiv_on_def] >> metis_tac[]) >> simp[restr_applies] >> 963 ���mapF (restr epsR B) (af b) = mapF (eps R A) (af b)��� 964 by (irule map_CONG >> qx_gen_tac ���b0��� >> strip_tac >> 965 ���b0 IN B��� suffices_by simp[restr_applies] >> 966 rev_drule subsystem_system >> 967 ���af b = restr af B b��� by simp[restr_applies] >> 968 metis_tac[system_members]) >> simp[]>> 969 ���mapF (eps R TR) (af (CHOICE (epsR b))) = 970 mapF epsR (af (CHOICE (epsR b)))��� 971 by (irule map_CONG >> qx_gen_tac ���t��� >> DEEP_INTRO_TAC CHOICE_INTRO >> 972 simp[Abbr���epsR���, eps_def] >> conj_tac 973 >- (fs[equiv_on_def] >> metis_tac[]) >> 974 qx_gen_tac ���a��� >> rpt strip_tac >> 975 ���a IN TR��� by (simp[Abbr���TR���] >> fs[equiv_on_def] >> metis_tac[]) >> 976 ���af a = restr af TR a��� by simp[restr_applies] >> 977 ���t IN TR��� by metis_tac[system_members, subsystem_system] >> 978 ���t IN A��� by fs[Abbr���TR���] >> simp[] >> 979 fs[Abbr���TR���] >> simp[Once EXTENSION] >> 980 fs[equiv_on_def] >> metis_tac[]) >> 981 simp[] >> ntac 2 (pop_assum (K ALL_TAC)) >> 982 pop_assum mp_tac >> DEEP_INTRO_TAC CHOICE_INTRO >> 983 simp[Abbr���epsR���, Abbr���TR���, eps_def] >> conj_tac 984 >- (fs[equiv_on_def] >> metis_tac[]) >> 985 qx_gen_tac ���a��� >> strip_tac >> 986 disch_then $ qx_choose_then ���b'��� strip_assume_tac >> 987 qpat_x_assum ���bisim R _ _ ��� mp_tac >> 988 csimp[sbisimulation_projns_homo, hom_def, FORALL_PROD, restr_applies] >> 989 disch_then $ qx_choose_then ���Rf��� strip_assume_tac >> 990 ���af a = mapF (restr SND (UNCURRY R)) (Rf (b, a)) /\ 991 af b = mapF (restr FST (UNCURRY R)) (Rf (b, a))��� by simp[] >> 992 simp[mapO'] >> irule map_CONG >> simp[FORALL_PROD] >> 993 qx_genl_tac [���a1���, ���a2���] >> strip_tac >> ���(b,a) IN UNCURRY R��� by simp[]>> 994 ���(a1,a2) IN UNCURRY R��� by metis_tac[system_members] >> 995 pop_assum mp_tac >> simp[restr_applies, eps_def] >> 996 strip_tac >> ���a1 IN A /\ a2 IN A��� by metis_tac[] >> 997 simp[EXTENSION, restr_applies] >> fs[equiv_on_def] >> metis_tac[]) 998 >- (simp[restr_def]) 999QED 1000 1001Theorem bisimilar_equivalence: 1002 bisimilar equiv_on system 1003Proof 1004 simp[equiv_on_def, FORALL_PROD, IN_DEF] >> rw[] 1005 >- (simp[bisimilar_def, bisim_def] >> rename [���system (A,af)���] >> 1006 qexists_tac ���Delta A��� >> simp[relF_def, SUBSET_DEF, FORALL_PROD] >> 1007 qx_gen_tac ���a��� >> strip_tac >> qexists_tac ���mapF (\x. (x,x)) (af a)��� >> 1008 simp[set_map', mapO', o_ABS_R, mapID] >> 1009 metis_tac[system_members]) 1010 >- (rpt (pop_assum mp_tac) >> 1011 ���!A af B bf. 1012 system ((A,af):'a system) /\ system((B,bf):'a system) /\ 1013 bisimilar (A,af) (B,bf) ==> 1014 bisimilar (B,bf) (A,af)��� suffices_by metis_tac[] >> 1015 simp[bisimilar_def, PULL_EXISTS] >> rw[] >> 1016 rename [���bisim R _ _���] >> qexists_tac ���inv R��� >> simp[]) >> 1017 fs[bisimilar_def] >> 1018 rename [���bisim R1 (A,af) (B,bf)���, ���bisim R2 (B,bf) (C,cf)���, 1019 ���bisim _ (A,af) (C,cf)���] >> 1020 fs[bisim_def] >> qexists_tac ���R2 O R1��� >> 1021 simp[O_DEF, PULL_EXISTS, GSYM relO_EQ] >> metis_tac[] 1022QED 1023 1024Definition gbisim_def: 1025 gbisim (A,af) x y <=> ?R. bisim R (A,af) (A,af) /\ R x y 1026End 1027 1028Theorem gbisim_equivalence: 1029 system (A,af) ==> gbisim (A,af) equiv_on A 1030Proof 1031 simp[equiv_on_def, gbisim_def] >> rw[] 1032 >- (qexists_tac ���Delta A��� >> simp[prop5_1]) 1033 >- metis_tac[inv_DEF, thm5_2] >> 1034 rename [���bisim R1 _ _ ���, ���R1 a b���, ���bisim R2 _ _���, ���R2 b c���] >> 1035 qexists_tac ���R2 O R1��� >> simp[O_DEF] >> metis_tac[thm5_4] 1036QED 1037 1038Theorem bisim_gbisim: 1039 system (A,af) ==> bisim (gbisim (A,af)) (A,af) (A,af) 1040Proof 1041 simp[bisim_def,gbisim_def, PULL_EXISTS] >> rw[] >> 1042 first_assum drule >> simp_tac (srw_ss()) [relF_def] >> 1043 simp[relF_def, SUBSET_DEF, FORALL_PROD, PULL_EXISTS, gbisim_def] >> rw[] >> 1044 rename [���mapF FST z = _���, ���mapF SND z = _���, ���_ IN setF z ==> R _ _���] >> 1045 qexists_tac ���z��� >> 1046 rw[] >> qexists_tac ���R���>> simp[bisim_def] >> metis_tac[] 1047QED 1048 1049Definition simple_def: 1050 simple (A : 'a system) <=> 1051 !R. bisim R A A ==> !x y. R x y ==> x = y 1052End 1053 1054Theorem simple_imp4: 1055 simple (As:'a system) ==> 1056 !Bs:'b system f g. hom f Bs As /\ hom g Bs As ==> f = g 1057Proof 1058 tmCases_on ���As:'a system��� ["A af"] >> rw[simple_def] >> 1059 tmCases_on ���Bs:'b system��� ["B bf"] >> 1060 ���bisim (span B f g) (A,af) (A,af)��� 1061 suffices_by (strip_tac >> first_x_assum drule >> 1062 simp[PULL_EXISTS, FUN_EQ_THM] >> fs[hom_def] >> 1063 metis_tac[]) >> 1064 irule lemma5_3 >> metis_tac[] 1065QED 1066 1067Theorem simple_eq3: 1068 simple As <=> !R. bisim R As As /\ R equiv_on (FST As) ==> R = Delta (FST As) 1069Proof 1070 tmCases_on ���As : 'a system��� ["A af"] >> 1071 simp[simple_def] >> eq_tac >> rw[] 1072 >- (simp[FUN_EQ_THM, EQ_IMP_THM, FORALL_AND_THM] >> 1073 metis_tac[equiv_on_def, bisim_def]) >> 1074 ���system (A,af)��� by metis_tac[bisim_def] >> 1075 ���bisim (gbisim (A,af)) (A,af) (A,af)��� by simp[bisim_gbisim] >> 1076 first_x_assum drule >> simp[gbisim_equivalence] >> 1077 simp[FUN_EQ_THM, gbisim_def] >> metis_tac[] 1078QED 1079 1080 1081 1082 1083val _ = export_theory(); 1084