1open HolKernel Parse boolLib
2
3open relationTheory bossLib boolSimps
4
5open pred_setTheory
6
7val _ = new_theory "diags"
8
9(* Diagram evaluation *)
10val _ = Hol_datatype `reltype = Atomic | TC`
11
12val liftrel_def = Define`
13  liftrel b ty R x y = (if b then I else (~))
14                         ((case ty of Atomic => I | TC => TC)
15                          R x y)
16`;
17
18
19val eval_def = Define`
20  eval (Fa : ('n # 'a # 'a # bool # reltype) -> bool)
21       (G : ('n # ('a + 'b) # ('a + 'b) # bool # reltype) -> bool)
22       (R : 'n -> 'c -> 'c -> bool) =
23    ! (f : 'a -> 'c).
24         (!a1 a2 n b ty. (n, a1, a2, b, ty) IN Fa ==>
25                         liftrel b ty (R n) (f a1) (f a2)) ==>
26         ? (g : 'b -> 'c).
27             (!a1 a2 n b ty. (n, INL a1, INL a2, b, ty) IN G ==>
28                             liftrel b ty (R n) (f a1) (f a2)) /\
29             (!a b n p ty. (n, INL a, INR b, p, ty) IN G ==>
30                           liftrel p ty (R n) (f a) (g b)) /\
31             (!a b n p ty. (n, INR b, INL a, p, ty) IN G ==>
32                           liftrel p ty (R n) (g b) (f a)) /\
33             (!b1 b2 n b ty. (n, INR b1, INR b2, b, ty) IN G ==>
34                             liftrel b ty (R n) (g b1) (g b2))
35`;
36
37(* Some example diagrams *)
38
39val diamond_eval = store_thm(
40  "diamond_eval",
41  ``eval {(0,0,1,T,Atomic); (0,0,2,T,Atomic)}
42         {(0,INL 1,INR 0,T,Atomic); (0,INL 2,INR 0,T,Atomic)}
43         R
44     = diamond (R 0)``,
45  SRW_TAC [DNF_ss] [diamond_def, eval_def, EQ_IMP_THM, liftrel_def] THENL [
46    FIRST_X_ASSUM (Q.SPEC_THEN `\n. if n = 0 then x
47                                    else if n = 1 then y
48                                    else z`
49                   MP_TAC) THEN
50    SRW_TAC [DNF_ss][] THEN METIS_TAC [],
51    `?u. R 0 (f 1) u /\ R 0 (f 2) u` by METIS_TAC [] THEN
52    Q.EXISTS_TAC `K u` THEN SRW_TAC [][]
53  ]);
54
55val totality_eval = store_thm(
56  "totality_eval",
57  ``eval {} {(0, INL 0, INL 1, T, Atomic)} R = !x y. R 0 x y``,
58  SRW_TAC [DNF_ss][eval_def, EQ_IMP_THM, liftrel_def] THEN
59  FIRST_X_ASSUM (Q.SPEC_THEN `\i. if i = 0 then x else y` MP_TAC) THEN
60  SRW_TAC [][]);
61
62val lopsided_TC_diamond = store_thm(
63  "lopsided_TC_diamond",
64  ``eval {(0,0,1,T,Atomic); (0,0,2,T,TC)}
65         {(0,INL 1,INR 0,T,TC); (0,INL 2,INR 0,T,TC)} R =
66    !x y z. R 0 x y /\ TC (R 0) x z ==>
67            ?u. TC (R 0) y u /\ TC (R 0) z u``,
68  SRW_TAC [DNF_ss][eval_def, EQ_IMP_THM, liftrel_def] THENL [
69    FIRST_X_ASSUM (Q.SPEC_THEN `\n. if n = 0 then x
70                                    else if n = 1 then y
71                                    else z`
72                   MP_TAC) THEN
73    SRW_TAC [DNF_ss][] THEN METIS_TAC [],
74    `?u. TC (R 0) (f 1) u /\ TC (R 0) (f 2) u` by METIS_TAC [] THEN
75    Q.EXISTS_TAC `K u` THEN SRW_TAC [][]
76  ]);
77
78val sequentialisation_eval = store_thm(
79  "sequentialisation_eval",
80  ``eval {(0,0,1,T,Atomic)}
81         {(1,INL 0,INR 0,T,Atomic); (2,INR 0,INL 1,T,Atomic)}
82         R =
83    (!x y. R 0 x y ==> ?z. R 1 x z /\ R 2 z y)``,
84  SRW_TAC [DNF_ss][eval_def, EQ_IMP_THM,liftrel_def] THENL [
85    FIRST_X_ASSUM (Q.SPEC_THEN `\n. if n = 0 then x else y` MP_TAC) THEN
86    SRW_TAC [DNF_ss][] THEN METIS_TAC [],
87    `?z. R 1 (f 0) z /\ R 2 z (f 1)` by METIS_TAC [] THEN
88    Q.EXISTS_TAC `K z` THEN SRW_TAC [][]
89  ]);
90
91val only_black_eq_T = prove(
92  ``eval Fa {} R' = T``,
93  SRW_TAC [DNF_ss][eval_def]);
94
95val relationally_reflected = store_thm(
96  "relationally_reflected",
97  ``eval {(0,0,1,T,Atomic)}
98         {(1,INR 0,INL 0,T,Atomic); (1,INR 1,INL 1,T,Atomic);
99          (2,INR 0,INR 1,T,Atomic)}
100         R =
101    (!x y. R 0 x y ==> ?u v. R 1 u x /\ R 1 v y /\ R 2 u v)``,
102  SRW_TAC [DNF_ss][eval_def, EQ_IMP_THM, liftrel_def] THENL [
103    FIRST_X_ASSUM (Q.SPEC_THEN `\n. if n = 0 then x else y` MP_TAC) THEN
104    SRW_TAC [DNF_ss][] THEN METIS_TAC [],
105    `?u v. R 1 u (f 0) /\ R 1 v (f 1) /\ R 2 u v` by METIS_TAC [] THEN
106    Q.EXISTS_TAC `\n. if n = 0 then u else v` THEN
107    SRW_TAC [][]
108  ]);
109
110val no_1step_join = store_thm(
111  "no_1step_join",
112  ``eval {(0,0,1,T,Atomic); (0,0,2,T,Atomic)}
113         {(0,INL 1,INL 2,F,Atomic)} R =
114    (!x y z. R 0 x y /\ R 0 x z ==> ~R 0 y z)``,
115  SRW_TAC [DNF_ss][eval_def, EQ_IMP_THM, liftrel_def] THENL [
116    FIRST_X_ASSUM (Q.SPEC_THEN `\n. if n = 0 then x
117                                    else if n = 1 then y else z` MP_TAC) THEN
118    SRW_TAC [DNF_ss][],
119    METIS_TAC []
120  ]);
121
122val no_terminal_object = store_thm(
123  "no_terminal_object",
124  ``eval {} {(0,INR 0,INL 0,F,Atomic)} R  = !y. ?x. ~R 0 x y``,
125  SRW_TAC [DNF_ss][eval_def, EQ_IMP_THM, liftrel_def] THENL [
126    FIRST_X_ASSUM (Q.SPEC_THEN `\n. y` MP_TAC) THEN SRW_TAC [][] THEN
127    METIS_TAC [],
128    `?u. ~R 0 u (f 0)` by METIS_TAC [] THEN
129    Q.EXISTS_TAC `\n. u` THEN SRW_TAC [][]
130  ]);
131
132
133(* ----------------------------------------------------------------------
134    Propositional Diagrams
135   ---------------------------------------------------------------------- *)
136
137val _ = Hol_datatype`
138  diaform = Lf of (('n # 'a # 'a # bool # reltype) -> bool) =>
139                  (('n # ('a + 'b) # ('a + 'b) # bool # reltype) -> bool)
140          | /\ of diaform => diaform
141          | ~ of diaform
142`
143
144val evalform_def = Define`
145  (evalform (Lf fa ex) R <=> eval fa ex R) /\
146  (evalform (f1 /\ f2) R <=> evalform f1 R /\ evalform f2 R) /\
147  (evalform (~f) R <=> ~evalform f R)
148`;
149
150val R0_refl_def = Define`
151  R0_refl = Lf {} {(0,INL 0,INL 0,T,Atomic)}
152`
153
154val R0_refl_thm = store_thm(
155  "R0_refl_thm",
156  ``evalform R0_refl R = !x. R 0 x x``,
157  SRW_TAC [][evalform_def, eval_def, R0_refl_def, liftrel_def, EQ_IMP_THM])
158
159val R0_sym_def = Define`
160  R0_sym = Lf {(0,0,1,T,Atomic)} {(0,INL 1, INL 0,T,Atomic)}
161`;
162
163val R0_sym_thm = store_thm(
164  "R0_sym_thm",
165  ``evalform R0_sym R = !x y. R 0 x y ==> R 0 y x``,
166  SRW_TAC [][evalform_def, eval_def, R0_sym_def, liftrel_def, EQ_IMP_THM] THEN
167  FIRST_X_ASSUM (Q.SPEC_THEN `\n. if n = 0 then x else y` MP_TAC) THEN
168  SRW_TAC [][])
169
170val R0_trans_def = Define`
171  R0_trans = Lf {(0,0,1,T,Atomic); (0,1,2,T,Atomic)}
172                {(0,INL 0, INL 2,T,Atomic)}
173`;
174val R0_trans_thm = store_thm(
175 "R0_trans_thm",
176  ``evalform R0_trans R = !x y z. R 0 x y /\ R 0 y z ==> R 0 x z``,
177  SRW_TAC [][evalform_def, eval_def, R0_trans_def, liftrel_def,
178             EQ_IMP_THM, DISJ_IMP_THM, FORALL_AND_THM]
179  THENL [
180    FIRST_X_ASSUM (Q.SPEC_THEN `\n. if n = 0 then x
181                                    else if n = 1 then y
182                                    else z` MP_TAC) THEN
183    SRW_TAC [][],
184    METIS_TAC []
185  ]);
186
187
188val R0_cong_def = Define`
189  R0_cong n <=> Lf {(0,0,1,T,Atomic); (n,0,2,T,Atomic)}
190                   {(n,INL 1,INL 2,T,Atomic)} /\
191                Lf {(0,1,2,T,Atomic); (n,0,1,T,Atomic)}
192                   {(n,INL 0, INL 2,T,Atomic)}
193`
194val R0_cong_thm = store_thm(
195  "R0_cong_thm",
196  ``evalform (R0_cong n) R <=> (!x y z. R 0 x y /\ R n x z ==> R n y z) /\
197                               (!x y z. R n x y /\ R 0 y z ==> R n x z)``,
198  SRW_TAC [][evalform_def, eval_def, R0_cong_def, liftrel_def,
199             EQ_IMP_THM, DISJ_IMP_THM, FORALL_AND_THM]
200  THENL [
201    FIRST_X_ASSUM (fn th =>
202       Q.SPEC_THEN `\n. if n = 0 then x
203                        else if n = 1 then y else z` MP_TAC th THEN
204       SRW_TAC [][] THEN NO_TAC),
205    FIRST_X_ASSUM (fn th =>
206       Q.SPEC_THEN `\n. if n = 0 then x
207                        else if n = 1 then y else z` MP_TAC th THEN
208       SRW_TAC [][] THEN NO_TAC),
209    METIS_TAC [],
210    METIS_TAC []
211  ]);
212
213val imp_def = xDefine "imp" `
214  (f1:('a,'b,'c)diaform) ==> f2 <=> ~(f1 /\ ~f2)
215`
216val imp_thm = store_thm(
217  "imp_thm",
218  ``evalform (f ==> g) R <=> evalform f R ==> evalform g R``,
219  SRW_TAC [][imp_def, evalform_def] THEN METIS_TAC []);
220
221
222val R0_refl_cong_sym = store_thm(
223  "R0_refl_cong_sym",
224  ``evalform (R0_cong 0 /\ R0_refl ==> R0_sym) R``,
225  SRW_TAC [][imp_thm, R0_cong_thm, evalform_def, R0_refl_thm, R0_sym_thm] THEN
226  METIS_TAC [])
227
228val R0_cong_trans = store_thm(
229  "R0_cong_trans",
230  ``evalform (R0_cong 0 ==> R0_trans) R``,
231  METIS_TAC [imp_thm, R0_cong_thm, R0_trans_thm])
232
233(* ----------------------------------------------------------------------
234    Theory of diagram equivalence
235   ---------------------------------------------------------------------- *)
236
237
238(* basic concepts *)
239val Pres_def = Define`
240  Pres f R1 R2 = !x y. R1 x y ==> R2 (f x) (f y)
241`;
242
243val onto_def = Define`
244  onto f = !x. ?y. f y = x
245`;
246
247val sRefl_def = Define`
248  sRefl f R1 R2 = !b1 b2. R2 b1 b2 ==>
249                         ?a1 a2. R1 a1 a2 /\ (b1 = f a1) /\ (b2 = f a2)
250`;
251
252val aRefl_def = Define`
253  aRefl f R1 R2 = !x y. R2 (f x) (f y) ==> R1 x y
254`;
255
256val kCompl_def = Define`
257  kCompl s f = !x y. (f x = f y) ==> EQC s x y
258`;
259
260val kSound_def = Define`
261  kSound s f = !x y. s x y ==> (f x = f y)
262`;
263
264val ofree_def = Define`
265  ofree s = !x y. EQC s x y ==> RTC s x y
266`;
267
268val presrefl_atomic = store_thm(
269  "presrefl_atomic",
270  ``Pres f R1 R2 /\ aRefl f R1 R2 ==> !x y. R1 x y = R2 (f x) (f y)``,
271  SRW_TAC [][Pres_def, aRefl_def] THEN METIS_TAC []);
272
273val presrefl_TC = store_thm(
274  "presrefl_TC",
275  ``onto f /\ Pres f R1 R2 /\ aRefl f R1 R2 ==>
276    (!x y. TC R1 x y = TC R2 (f x) (f y))``,
277  SIMP_TAC (srw_ss()) [onto_def] THEN STRIP_TAC THEN
278  `!x y. R1 x y = R2 (f x) (f y)` by METIS_TAC [presrefl_atomic] THEN
279  SIMP_TAC (srw_ss() ++ DNF_ss) [EQ_IMP_THM] THEN CONJ_TAC THENL [
280    HO_MATCH_MP_TAC TC_INDUCT THEN METIS_TAC [TC_RULES],
281    Q_TAC SUFF_TAC `!a b. TC R2 a b ==> !x y. (a = f x) /\ (b = f y) ==>
282                                              TC R1 x y`
283          THEN1 METIS_TAC [] THEN
284    HO_MATCH_MP_TAC TC_INDUCT THEN
285    SRW_TAC [][] THENL [
286      METIS_TAC [TC_RULES],
287      `?a0. f a0 = a'` by METIS_TAC [] THEN
288      METIS_TAC [TC_RULES]
289    ]
290  ]);
291
292val presrefl_liftrel = store_thm(
293  "presrefl_liftrel",
294  ``onto f /\ Pres f R1 R2 /\ aRefl f R1 R2 ==>
295    !x y b ty. liftrel b ty R1 x y = liftrel b ty R2 (f x) (f y)``,
296  SRW_TAC [][liftrel_def] THEN
297  Cases_on `ty` THEN SRW_TAC [][presrefl_TC, presrefl_atomic]);
298
299val aRefl_TC = store_thm(
300  "aRefl_TC",
301  ``aRefl f R1 R2 /\ onto f ==> aRefl f (TC R1) (TC R2)``,
302  SIMP_TAC (srw_ss()) [aRefl_def, onto_def] THEN STRIP_TAC THEN
303  Q_TAC SUFF_TAC `!a b. TC R2 a b ==> !x y. (a = f x) /\ (b = f y) ==>
304                                            TC R1 x y`
305        THEN1 METIS_TAC [] THEN
306  HO_MATCH_MP_TAC TC_INDUCT THEN SRW_TAC [][] THEN
307  METIS_TAC [TC_RULES]);
308
309
310(* important theorem *)
311val diagram_preservation = store_thm(
312  "diagram_preservation",
313  ``!R1 R2 h.
314       onto h /\ (!n. Pres h (R1 n) (R2 n) /\ aRefl h (R1 n) (R2 n)) ==>
315       !Fa G. eval Fa G R1 = eval Fa G R2``,
316  REPEAT STRIP_TAC THEN
317  `!n a1 a2 b ty. liftrel b ty (R1 n) a1 a2 =
318                  liftrel b ty (R2 n) (h a1) (h a2)`
319     by METIS_TAC [presrefl_liftrel] THEN
320  `?invh. !b. h (invh b) = b` by METIS_TAC [SKOLEM_THM, onto_def] THEN
321  ASM_SIMP_TAC (srw_ss()) [eval_def] THEN EQ_TAC THEN REPEAT STRIP_TAC THENL [
322    FIRST_X_ASSUM (MP_TAC o SPEC ``(invh : 'c -> 'b) o (f : 'd -> 'c)``) THEN
323    SRW_TAC [][] THEN
324    Q.EXISTS_TAC `h o g` THEN SRW_TAC [][],
325
326    FIRST_X_ASSUM (MP_TAC o SPEC ``(h : 'b -> 'c) o (f : 'd -> 'b)``) THEN
327    SRW_TAC [][] THEN
328    Q.EXISTS_TAC `invh o g` THEN SRW_TAC [][]
329  ]);
330
331(* can prove that diagram formulas are also preserved *)
332val diaform_preservation = store_thm(
333  "diaform_preservation",
334  ``!R1 R2 h.
335       onto h /\ (!n. Pres h (R1 n) (R2 n) /\ aRefl h (R1 n) (R2 n)) ==>
336       !f. evalform f R1 = evalform f R2``,
337  REPEAT GEN_TAC THEN STRIP_TAC THEN
338  Induct THEN SRW_TAC [][evalform_def] THEN
339  METIS_TAC [diagram_preservation])
340
341(* but aRefl is a strong requirement to make of a homomorphism...
342     (some might argue that onto is as well)
343   so let's try to weaken aRefl to sRefl.  We can do so by adding
344   structure *)
345
346val Refl_is_someany_with_structure = store_thm(
347  "Refl_is_someany_with_structure",
348  ``kSound s f /\ kCompl s f /\ onto f ==>
349    (sRefl f R1 R2 = aRefl f (EQC s O R1 O EQC s) R2)``,
350  SRW_TAC [][EQ_IMP_THM, kSound_def, kCompl_def, onto_def, sRefl_def,
351             aRefl_def]
352  THENL [
353    RES_TAC THEN SRW_TAC [][O_DEF] THEN METIS_TAC [],
354    `?a1 a2. (b1 = f a1) /\ (b2 = f a2)` by METIS_TAC [] THEN
355    SRW_TAC [][] THEN RES_TAC THEN
356    FULL_SIMP_TAC (srw_ss()) [O_DEF] THEN
357    Q_TAC SUFF_TAC `!x y. EQC s x y ==> (f x = f y)`
358          THEN1 METIS_TAC [] THEN
359    HO_MATCH_MP_TAC EQC_INDUCTION THEN METIS_TAC []
360  ]);
361
362val Pres_ok_with_structure = store_thm(
363  "Pres_ok_with_structure",
364  ``kSound s f /\ Pres f R1 R2 ==> Pres f (EQC s O R1 O EQC s) R2``,
365  SRW_TAC [][Pres_def, kSound_def, O_DEF] THEN
366  Q_TAC SUFF_TAC `!x y. EQC s x y ==> (f x = f y)` THEN1
367        METIS_TAC [] THEN
368  HO_MATCH_MP_TAC EQC_INDUCTION THEN METIS_TAC []);
369
370
371(* pre-order reduction *)
372
373(* paper's name for this theorem is
374     "Pre-ordered structural reflection is some/any"
375*)
376val note_lemma9 = store_thm(
377  "note_lemma9",
378  ``onto f  /\ kCompl s f /\ ofree s ==>
379    (sRefl f (RTC (x RUNION s)) (RTC y) =
380     aRefl f (RTC (x RUNION s)) (RTC y))``,
381  SIMP_TAC (srw_ss()) [onto_def, kCompl_def, ofree_def, sRefl_def,
382                       aRefl_def] THEN STRIP_TAC THEN EQ_TAC
383  THENL [
384    STRIP_TAC THEN MAP_EVERY Q.X_GEN_TAC [`a1`, `a2`] THEN STRIP_TAC THEN
385    `?a1' a2'. RTC (x RUNION s) a1' a2' /\ (f a1' = f a1) /\ (f a2' = f a2)`
386       by METIS_TAC [] THEN
387    `RTC s a1 a1' /\ RTC s a2' a2` by METIS_TAC [] THEN
388    `RTC (x RUNION s) a1 a1' /\ RTC (x RUNION s) a2' a2`
389       by METIS_TAC [chap3Theory.RUNION_RTC_MONOTONE, RUNION_COMM] THEN
390    METIS_TAC [RTC_RTC],
391    METIS_TAC []
392  ]);
393
394(* paper's name for this theorem is
395     "Some-Reflection is Structurally Pre-ordered"
396*)
397val note_prop10_1 = store_thm(
398  "note_prop10_1",
399  ``onto f /\ kCompl s f /\ ofree s /\ sRefl f x y ==>
400    sRefl f (RTC (x RUNION s)) (RTC y)``,
401  SIMP_TAC (srw_ss()) [sRefl_def, onto_def, ofree_def, kCompl_def] THEN
402  STRIP_TAC THEN
403  HO_MATCH_MP_TAC RTC_INDUCT THEN CONJ_TAC THENL [
404    METIS_TAC [chap3Theory.RUNION_RTC_MONOTONE, RUNION_COMM],
405    REPEAT STRIP_TAC THEN
406    `?a0 a1'. x a0 a1' /\ (b1 = f a0) /\ (b1' = f a1')` by METIS_TAC [] THEN
407    `RTC s a1' a1` by METIS_TAC [] THEN
408    `RTC (x RUNION s) a1' a1`
409      by METIS_TAC [chap3Theory.RUNION_RTC_MONOTONE, RUNION_COMM] THEN
410    `RTC (x RUNION s) a0 a1'` by METIS_TAC [chap3Theory.RUNION_RTC_MONOTONE,
411                                            RTC_RULES] THEN
412    METIS_TAC [RTC_RTC]
413  ]);
414
415(* "structural pre-ordered preservation" *)
416val Pres_structure_RTC = store_thm(
417  "Pres_structure_RTC",
418  ``Pres f R1 R2 /\ kSound s f ==>
419    Pres f (RTC (R1 RUNION s)) (RTC R2)``,
420  SIMP_TAC (srw_ss()) [Pres_def, kSound_def] THEN STRIP_TAC THEN
421  HO_MATCH_MP_TAC RTC_INDUCT THEN SRW_TAC [][RTC_RULES, RUNION] THEN
422  METIS_TAC [RTC_RULES]);
423
424val _ = export_theory()
425