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