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