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