1(* 2 * Copyright 1991-1995 University of Cambridge (Author: Monica Nesi) 3 * Copyright 2017 University of Bologna (Author: Chun Tian) 4 *) 5 6open HolKernel Parse boolLib bossLib; 7 8open pred_setTheory relationTheory pairTheory sumTheory listTheory; 9open prim_recTheory arithmeticTheory combinTheory; 10 11open CCSLib CCSTheory; 12open StrongEQTheory StrongEQLib StrongLawsTheory; 13open WeakEQTheory WeakEQLib WeakLawsTheory; 14open ObsCongrTheory ObsCongrLib ObsCongrLawsTheory ObsCongrConv; 15open TraceTheory CongruenceTheory; 16 17val _ = new_theory "CoarsestCongr"; 18val _ = temp_loose_equality (); 19 20(******************************************************************************) 21(* *) 22(* A derived tau-law for observation congruence *) 23(* *) 24(******************************************************************************) 25 26(* Theorem TAU_STRAT: 27 |- !E E'. OBS_CONGR (sum E (prefix tau (sum E' E))) (prefix tau (sum E' E)) 28 *) 29val TAU_STRAT = store_thm ( 30 "TAU_STRAT", 31 ``!E E'. OBS_CONGR (sum E (prefix tau (sum E' E))) (prefix tau (sum E' E))``, 32 rpt GEN_TAC 33 >> OC_LHS_SUBST1_TAC 34 (SPEC ``sum E' E`` (GEN_ALL (OC_SYM (SPEC_ALL TAU2)))) 35 >> OC_SUM_IDEMP_TAC 36 >> OC_LHS_SUBST1_TAC (SPEC ``sum E' E`` TAU2)); 37 38(******************************************************************************) 39(* *) 40(* Deng Lemma and Hennessy Lemma *) 41(* *) 42(******************************************************************************) 43 44(* Lemma 4.2. (Deng Lemma) [Den07], the weak bisimularity version *) 45val DENG_LEMMA = store_thm ((* NEW *) 46 "DENG_LEMMA", 47 ``!p q. WEAK_EQUIV p q ==> (?p'. TRANS p tau p' /\ WEAK_EQUIV p' q) \/ 48 (?q'. TRANS q tau q' /\ WEAK_EQUIV p q') \/ 49 OBS_CONGR p q``, 50 rpt STRIP_TAC 51 >> MATCH_MP_TAC (DECIDE ``(~P /\ ~Q ==> R) ==> P \/ Q \/ R``) 52 >> rpt STRIP_TAC 53 >> REWRITE_TAC [OBS_CONGR] 54 >> rpt STRIP_TAC (* 2 sub-goals here *) 55 >| [ (* goal 1 (of 2) *) 56 Cases_on `u` >| (* 2 sub-goals here *) 57 [ (* goal 1.1 (of 2) *) 58 PAT_X_ASSUM ``WEAK_EQUIV p q`` 59 (STRIP_ASSUME_TAC o (ONCE_REWRITE_RULE [WEAK_PROPERTY_STAR])) \\ 60 RES_TAC \\ 61 IMP_RES_TAC EPS_cases1 >- PROVE_TAC [] \\ 62 Q.EXISTS_TAC `E2` >> ASM_REWRITE_TAC [] \\ 63 REWRITE_TAC [WEAK_TRANS] \\ 64 take [`q`, `u`] >> ASM_REWRITE_TAC [EPS_REFL, PREFIX], 65 (* goal 1.2 (of 2) *) 66 PAT_X_ASSUM ``WEAK_EQUIV p q`` 67 (STRIP_ASSUME_TAC o (ONCE_REWRITE_RULE [WEAK_PROPERTY_STAR])) \\ 68 RES_TAC \\ 69 Q.EXISTS_TAC `E2` >> ASM_REWRITE_TAC [] ], 70 (* goal 2 (of 2) *) 71 Cases_on `u` >| (* 2 sub-goals here *) 72 [ (* goal 2.1 (of 2) *) 73 PAT_X_ASSUM ``WEAK_EQUIV p q`` 74 (STRIP_ASSUME_TAC o (ONCE_REWRITE_RULE [WEAK_PROPERTY_STAR])) \\ 75 RES_TAC \\ 76 IMP_RES_TAC EPS_cases1 >- PROVE_TAC [] \\ 77 Q.EXISTS_TAC `E1` >> ASM_REWRITE_TAC [] \\ 78 REWRITE_TAC [WEAK_TRANS] \\ 79 take [`p`, `u`] >> ASM_REWRITE_TAC [EPS_REFL, PREFIX], 80 (* goal 1.2.2 (of 2) *) 81 PAT_X_ASSUM ``WEAK_EQUIV p q`` 82 (STRIP_ASSUME_TAC o (ONCE_REWRITE_RULE [WEAK_PROPERTY_STAR])) \\ 83 RES_TAC \\ 84 Q.EXISTS_TAC `E1` >> ASM_REWRITE_TAC [] ] ]); 85 86(* Hennessy Lemma, the easy part *) 87val HENNESSY_LEMMA_RL = store_thm ((* NEW *) 88 "HENNESSY_LEMMA_RL", 89 ``!p q. (OBS_CONGR p q \/ OBS_CONGR p (prefix tau q) \/ 90 OBS_CONGR (prefix tau p) q) ==> WEAK_EQUIV p q``, 91 rpt STRIP_TAC (* 3 sub-goals here *) 92 >| [ (* goal 2.1 (of 3) *) 93 IMP_RES_TAC OBS_CONGR_IMP_WEAK_EQUIV, 94 (* goal 2.2 (of 3) *) 95 IMP_RES_TAC OBS_CONGR_IMP_WEAK_EQUIV \\ 96 ASSUME_TAC (Q.SPEC `q` TAU_WEAK) \\ 97 IMP_RES_TAC WEAK_EQUIV_TRANS, 98 (* goal 2.3 (of 3) *) 99 IMP_RES_TAC OBS_CONGR_IMP_WEAK_EQUIV \\ 100 ASSUME_TAC (Q.SPEC `p` TAU_WEAK) \\ 101 POP_ASSUM (ASSUME_TAC o (MATCH_MP WEAK_EQUIV_SYM)) \\ 102 IMP_RES_TAC WEAK_EQUIV_TRANS ]); 103 104(* Hennessy Lemma, the hard part *) 105val HENNESSY_LEMMA_LR = store_thm ((* NEW *) 106 "HENNESSY_LEMMA_LR", 107 ``!p q. WEAK_EQUIV p q ==> (OBS_CONGR p q \/ OBS_CONGR p (prefix tau q) 108 \/ OBS_CONGR (prefix tau p) q)``, 109 rpt STRIP_TAC 110 >> Cases_on `?E. TRANS p tau E /\ WEAK_EQUIV E q` (* 2 sub-goals here *) 111 >| [ (* goal 1 (of 2) *) 112 DISJ2_TAC >> DISJ1_TAC \\ (* CHOOSE ``OBS_CONGR p tau..q`` *) 113 REWRITE_TAC [OBS_CONGR] >> rpt STRIP_TAC >| (* 2 sub-goals here *) 114 [ (* goal 1.1 (of 2) *) 115 Cases_on `u` \\ (* 2 sub-goals here, sharing initial tacticals *) 116 PAT_X_ASSUM ``WEAK_EQUIV p q`` 117 (STRIP_ASSUME_TAC o (ONCE_REWRITE_RULE [WEAK_PROPERTY_STAR])) \\ 118 RES_TAC \\ 119 Q.EXISTS_TAC `E2` >> ASM_REWRITE_TAC [] >| 120 [ (* goal 1.1.1 (of 2) *) 121 REWRITE_TAC [WEAK_TRANS] \\ 122 take [`prefix tau q`, `q`] \\ 123 ASM_REWRITE_TAC [EPS_REFL, PREFIX], 124 (* goal 1.1.2 (of 2) *) 125 IMP_RES_TAC TAU_PREFIX_WEAK_TRANS ], 126 (* goal 1.2 (of 2) *) 127 IMP_RES_TAC TRANS_PREFIX >> ASM_REWRITE_TAC [] \\ 128 PAT_X_ASSUM ``?E. TRANS p tau E /\ WEAK_EQUIV E q`` STRIP_ASSUME_TAC \\ 129 Q.EXISTS_TAC `E` >> ASM_REWRITE_TAC [] \\ 130 IMP_RES_TAC TRANS_IMP_WEAK_TRANS ], 131 (* goal 2 (of 2) *) 132 Cases_on `?E. TRANS q tau E /\ WEAK_EQUIV p E` >| (* 2 sub-goals here *) 133 [ (* goal 2.1 (of 2) *) 134 NTAC 2 DISJ2_TAC \\ (* CHOOSE ``OBS_CONGR tau..p q`` *) 135 REWRITE_TAC [OBS_CONGR] >> rpt STRIP_TAC >| (* 2 sub-goals here *) 136 [ (* goal 2.1.1 (of 2) *) 137 IMP_RES_TAC TRANS_PREFIX >> ONCE_ASM_REWRITE_TAC [] \\ 138 PAT_X_ASSUM ``?E. TRANS q tau E /\ WEAK_EQUIV p E`` STRIP_ASSUME_TAC \\ 139 Q.EXISTS_TAC `E` >> ONCE_ASM_REWRITE_TAC [] \\ 140 IMP_RES_TAC TRANS_IMP_WEAK_TRANS \\ 141 ASM_REWRITE_TAC [], 142 (* goal 2.1.2 (of 2) *) 143 Cases_on `u` \\ (* 2 sub-goals here, sharing initial tacticals *) 144 PAT_X_ASSUM ``WEAK_EQUIV p q`` 145 (STRIP_ASSUME_TAC o (ONCE_REWRITE_RULE [WEAK_PROPERTY_STAR])) \\ 146 RES_TAC \\ 147 Q.EXISTS_TAC `E1` >> ASM_REWRITE_TAC [] >| 148 [ (* goal 2.1.2.1 (of 2) *) 149 REWRITE_TAC [WEAK_TRANS] \\ 150 take [`prefix tau p`, `p`] \\ 151 ASM_REWRITE_TAC [EPS_REFL, PREFIX], 152 (* goal 2.1.2.2 (of 2) *) 153 IMP_RES_TAC TAU_PREFIX_WEAK_TRANS ] ], 154 (* goal 2.2 (of 2) *) 155 DISJ1_TAC \\ (* CHOOSE ``OBS_CONGR p q``, then use Deng Lemma *) 156 IMP_RES_TAC DENG_LEMMA \\ (* 2 sub-goals here, same tactical *) 157 RES_TAC ] ]); 158 159(* Lemma 4.1. (Hennessy Lemma) [Mil89] *) 160val HENNESSY_LEMMA = store_thm ((* NEW *) 161 "HENNESSY_LEMMA", 162 ``!p q. WEAK_EQUIV p q = (OBS_CONGR p q \/ OBS_CONGR p (prefix tau q) 163 \/ OBS_CONGR (prefix tau p) q)``, 164 rpt GEN_TAC >> EQ_TAC 165 >- REWRITE_TAC [HENNESSY_LEMMA_LR] 166 >> REWRITE_TAC [HENNESSY_LEMMA_RL]); 167 168(* Definition 12: the coarsest congruence that is finer than WEAK_EQUIV is called 169 WEAK_CONGR (weak bisimulation congruence) *) 170val WEAK_CONGR = new_definition ((* NEW *) 171 "WEAK_CONGR", ``WEAK_CONGR = CC WEAK_EQUIV``); 172 173val WEAK_CONGR_THM = save_thm ( 174 "WEAK_CONGR_THM", REWRITE_RULE [CC_def] WEAK_CONGR); 175 176val WEAK_CONGR_congruence = store_thm ((* NEW *) 177 "WEAK_CONGR_congruence", ``congruence WEAK_CONGR``, 178 REWRITE_TAC [WEAK_CONGR] 179 >> MATCH_MP_TAC CC_congruence 180 >> REWRITE_TAC [WEAK_EQUIV_equivalence]); 181 182val OBS_CONGR_IMP_WEAK_CONGR = store_thm ((* NEW *) 183 "OBS_CONGR_IMP_WEAK_CONGR", ``!p q. OBS_CONGR p q ==> WEAK_CONGR p q``, 184 REWRITE_TAC [WEAK_CONGR, GSYM RSUBSET] 185 >> ASSUME_TAC OBS_CONGR_congruence 186 >> `OBS_CONGR RSUBSET WEAK_EQUIV` 187 by PROVE_TAC [OBS_CONGR_IMP_WEAK_EQUIV, RSUBSET] 188 >> IMP_RES_TAC CC_is_coarsest 189 >> ASM_REWRITE_TAC []); 190 191val SUM_EQUIV = new_definition ((* NEW *) 192 "SUM_EQUIV", ``SUM_EQUIV = (\p q. !r. WEAK_EQUIV (sum p r) (sum q r))``); 193 194val WEAK_CONGR_IMP_SUM_EQUIV = store_thm ((* NEW *) 195 "WEAK_CONGR_IMP_SUM_EQUIV", 196 ``!p q. WEAK_CONGR p q ==> SUM_EQUIV p q``, 197 REWRITE_TAC [WEAK_CONGR, SUM_EQUIV, CC_def] 198 >> BETA_TAC >> rpt STRIP_TAC 199 >> POP_ASSUM MP_TAC 200 >> Know `CONTEXT (\(t :('a, 'b) CCS). t) /\ CONTEXT (\t. r)` 201 >- REWRITE_TAC [CONTEXT1, CONTEXT2] 202 >> DISCH_TAC 203 >> POP_ASSUM (ASSUME_TAC o (MATCH_MP CONTEXT4)) 204 >> DISCH_TAC >> RES_TAC 205 >> POP_ASSUM (MP_TAC o BETA_RULE) >> Rewr); 206 207(******************************************************************************) 208(* *) 209(* Coarsest congruence contained in WEAK_EQUIV *) 210(* *) 211(******************************************************************************) 212 213val COARSEST_CONGR_LR = store_thm ((* NEW *) 214 "COARSEST_CONGR_LR", 215 ``!p q. OBS_CONGR p q ==> !r. WEAK_EQUIV (sum p r) (sum q r)``, 216 rpt STRIP_TAC 217 >> MATCH_MP_TAC OBS_CONGR_IMP_WEAK_EQUIV 218 >> RW_TAC std_ss [OBS_CONGR_SUBST_SUM_R]); 219 220(* The property as assumptions on processes in COARSEST_CONGR_THM *) 221val free_action_def = Define ` 222 free_action p = ?a. !p'. ~(WEAK_TRANS p (label a) p')`; 223 224val COARSEST_CONGR_RL = store_thm ((* NEW *) 225 "COARSEST_CONGR_RL", 226 ``!p q. free_action p /\ free_action q ==> 227 (!r. WEAK_EQUIV (sum p r) (sum q r)) ==> OBS_CONGR p q``, 228 REWRITE_TAC [free_action_def, OBS_CONGR] 229 >> rpt STRIP_TAC (* 2 sub-goals here *) 230 >| [ (* goal 1 (of 2) *) 231 ASSUME_TAC (Q.SPEC `prefix (label a) nil` 232 (ASSUME ``!r. WEAK_EQUIV (sum p r) (sum q r)``)) \\ 233 IMP_RES_TAC SUM1 \\ 234 POP_ASSUM (ASSUME_TAC o (Q.SPEC `prefix (label a) nil`)) \\ 235 Cases_on `u` >| (* 2 sub-goals here *) 236 [ (* goal 1.1 (of 2) *) 237 STRIP_ASSUME_TAC 238 (ONCE_REWRITE_RULE [WEAK_PROPERTY_STAR] 239 (ASSUME ``WEAK_EQUIV (sum p (prefix (label a) nil)) 240 (sum q (prefix (label a) nil))``)) \\ 241 RES_TAC \\ 242 IMP_RES_TAC EPS_cases1 >| (* 2 sub-goals here *) 243 [ (* goal 1.1.1 (of 2) *) 244 `TRANS E2 (label a) nil` by RW_TAC std_ss [SUM2, PREFIX] \\ 245 STRIP_ASSUME_TAC 246 (ONCE_REWRITE_RULE [WEAK_PROPERTY_STAR] (ASSUME ``WEAK_EQUIV E1 E2``)) \\ 247 RES_TAC \\ 248 IMP_RES_TAC TRANS_TAU_AND_WEAK \\ 249 RES_TAC, (* initial assumption of `p` is used here *) 250 (* goal 1.1.2 (of 2) *) 251 PAT_X_ASSUM ``TRANS (sum q (prefix (label a) nil)) tau u`` 252 (STRIP_ASSUME_TAC o (MATCH_MP TRANS_SUM)) >| (* 2 sub-goals here *) 253 [ (* goal 1.1.2.1 (of 4) *) 254 Q.EXISTS_TAC `E2` >> ASM_REWRITE_TAC [] \\ 255 REWRITE_TAC [WEAK_TRANS] \\ 256 take [`q`, `u`] >> ASM_REWRITE_TAC [EPS_REFL], 257 (* goal 1.1.2.2 (of 4) *) 258 IMP_RES_TAC TRANS_PREFIX \\ 259 RW_TAC std_ss [Action_distinct] ] ], 260 (* goal 1.2 (of 2) *) 261 STRIP_ASSUME_TAC 262 (ONCE_REWRITE_RULE [WEAK_PROPERTY_STAR] 263 (ASSUME ``WEAK_EQUIV (sum p (prefix (label a) nil)) 264 (sum q (prefix (label a) nil))``)) \\ 265 RES_TAC \\ 266 IMP_RES_TAC WEAK_TRANS_cases1 >| (* 2 sub-goals here *) 267 [ (* goal 1.2.1 (of 2) *) 268 PAT_X_ASSUM ``TRANS (sum q (prefix (label a) nil)) tau E'`` 269 (STRIP_ASSUME_TAC o (MATCH_MP TRANS_SUM)) >| (* 2 sub-goals here *) 270 [ (* goal 1.2.1.1 (of 2) *) 271 Q.EXISTS_TAC `E2` >> ASM_REWRITE_TAC [] \\ 272 IMP_RES_TAC TRANS_TAU_AND_WEAK, 273 (* goal 1.2.1.2 (of 2) *) 274 IMP_RES_TAC TRANS_PREFIX \\ 275 RW_TAC std_ss [Action_distinct] ], 276 (* goal 1.2.2 (of 2) *) 277 PAT_X_ASSUM ``TRANS (sum q (prefix (label a) nil)) (label L) E'`` 278 (STRIP_ASSUME_TAC o (MATCH_MP TRANS_SUM)) >| (* 2 sub-goals here *) 279 [ (* goal 1.2.2.1 (of 2) *) 280 Q.EXISTS_TAC `E2` >> ASM_REWRITE_TAC [] \\ 281 REWRITE_TAC [WEAK_TRANS] \\ 282 take [`q`, `E'`] >> ASM_REWRITE_TAC [EPS_REFL], 283 (* goal 1.2.2.2 (of 2) *) 284 IMP_RES_TAC TRANS_PREFIX \\ 285 PAT_X_ASSUM ``label L = label a`` 286 (ASSUME_TAC o (REWRITE_RULE [Action_11])) \\ 287 `TRANS p (label a) E1` by RW_TAC std_ss [] \\ 288 POP_ASSUM (ASSUME_TAC o (MATCH_MP TRANS_IMP_WEAK_TRANS)) \\ 289 RES_TAC ] ] ], (* initial assumption of `p` is used here *) 290 (* goal 2, completely symmetric with goal 1 *) 291 ASSUME_TAC (Q.SPEC `prefix (label a') nil` 292 (ASSUME ``!r. WEAK_EQUIV (sum p r) (sum q r)``)) \\ 293 IMP_RES_TAC SUM1 \\ 294 POP_ASSUM (ASSUME_TAC o (Q.SPEC `prefix (label a') nil`)) \\ 295 Cases_on `u` >| (* 2 sub-goals here *) 296 [ (* goal 2.1 (of 2) *) 297 STRIP_ASSUME_TAC 298 (ONCE_REWRITE_RULE [WEAK_PROPERTY_STAR] 299 (ASSUME ``WEAK_EQUIV (sum p (prefix (label a') nil)) 300 (sum q (prefix (label a') nil))``)) \\ 301 RES_TAC \\ 302 IMP_RES_TAC EPS_cases1 >| (* 2 sub-goals here *) 303 [ (* goal 2.1.1 (of 2) *) 304 `TRANS E1 (label a') nil` by RW_TAC std_ss [SUM2, PREFIX] \\ 305 STRIP_ASSUME_TAC 306 (ONCE_REWRITE_RULE [WEAK_PROPERTY_STAR] (ASSUME ``WEAK_EQUIV E1 E2``)) \\ 307 RES_TAC \\ 308 IMP_RES_TAC TRANS_TAU_AND_WEAK \\ 309 RES_TAC, (* initial assumption of `q` is used here *) 310 (* goal 2.1.2 (of 2) *) 311 PAT_X_ASSUM ``TRANS (sum p (prefix (label a') nil)) tau u`` 312 (STRIP_ASSUME_TAC o (MATCH_MP TRANS_SUM)) >| (* 2 sub-goals here *) 313 [ (* goal 2.1.2.1 (of 4) *) 314 Q.EXISTS_TAC `E1` >> ASM_REWRITE_TAC [] \\ 315 REWRITE_TAC [WEAK_TRANS] \\ 316 take [`p`, `u`] >> ASM_REWRITE_TAC [EPS_REFL], 317 (* goal 2.1.2.2 (of 4) *) 318 IMP_RES_TAC TRANS_PREFIX \\ 319 RW_TAC std_ss [Action_distinct] ] ], 320 (* goal 2.2 (of 2) *) 321 STRIP_ASSUME_TAC 322 (ONCE_REWRITE_RULE [WEAK_PROPERTY_STAR] 323 (ASSUME ``WEAK_EQUIV (sum p (prefix (label a') nil)) 324 (sum q (prefix (label a') nil))``)) \\ 325 RES_TAC \\ 326 IMP_RES_TAC WEAK_TRANS_cases1 >| (* 2 sub-goals here *) 327 [ (* goal 2.2.1 (of 2) *) 328 PAT_X_ASSUM ``TRANS (sum p (prefix (label a') nil)) tau E'`` 329 (STRIP_ASSUME_TAC o (MATCH_MP TRANS_SUM)) >| (* 2 sub-goals here *) 330 [ (* goal 2.2.1.1 (of 2) *) 331 Q.EXISTS_TAC `E1` >> ASM_REWRITE_TAC [] \\ 332 IMP_RES_TAC TRANS_TAU_AND_WEAK, 333 (* goal 2.2.1.2 (of 2) *) 334 IMP_RES_TAC TRANS_PREFIX \\ 335 RW_TAC std_ss [Action_distinct] ], 336 (* goal 2.2.2 (of 2) *) 337 PAT_X_ASSUM ``TRANS (sum p (prefix (label a') nil)) (label L) E'`` 338 (STRIP_ASSUME_TAC o (MATCH_MP TRANS_SUM)) >| (* 2 sub-goals here *) 339 [ (* goal 2.2.2.1 (of 2) *) 340 Q.EXISTS_TAC `E1` >> ASM_REWRITE_TAC [] \\ 341 REWRITE_TAC [WEAK_TRANS] \\ 342 take [`p`, `E'`] >> ASM_REWRITE_TAC [EPS_REFL], 343 (* goal 2.2.2.2 (of 2) *) 344 IMP_RES_TAC TRANS_PREFIX \\ 345 PAT_X_ASSUM ``label L = label a'`` (ASSUME_TAC o (REWRITE_RULE [Action_11])) \\ 346 `TRANS q (label a') E2` by RW_TAC std_ss [] \\ 347 POP_ASSUM (ASSUME_TAC o (MATCH_MP TRANS_IMP_WEAK_TRANS)) \\ 348 RES_TAC ] ] ] ] ); (* initial assumption of `q` is used here *) 349 350(* Theorem 4.5. (Coarsest congruence contained in WEAK_EQUIV) in Gorrieri's book. 351 OBS_CONGR congruences theorems shouldn't depend on this result. 352 *) 353val COARSEST_CONGR_THM = store_thm ((* NEW *) 354 "COARSEST_CONGR_THM", 355 ``!p q. free_action p /\ free_action q ==> 356 (OBS_CONGR p q = !r. WEAK_EQUIV (sum p r) (sum q r))``, 357 rpt STRIP_TAC 358 >> EQ_TAC >- REWRITE_TAC [COARSEST_CONGR_LR] 359 >> MATCH_MP_TAC COARSEST_CONGR_RL 360 >> ASM_REWRITE_TAC []); 361 362(******************************************************************************) 363(* *) 364(* Coarsest congruence contained in WEAK_EQUIV (finite version) *) 365(* *) 366(******************************************************************************) 367 368(* The shared core lemma used in PROP3's proof *) 369val PROP3_COMMON = store_thm ((* NEW *) 370 "PROP3_COMMON", 371 ``!p q. (?k. STABLE k /\ 372 (!p' u. WEAK_TRANS p u p' ==> ~(WEAK_EQUIV p' k)) /\ 373 (!q' u. WEAK_TRANS q u q' ==> ~(WEAK_EQUIV q' k))) ==> 374 (!r. WEAK_EQUIV (sum p r) (sum q r)) ==> OBS_CONGR p q``, 375 rpt STRIP_TAC 376 >> PAT_X_ASSUM ``!r. WEAK_EQUIV (sum p r) (sum q r)`` 377 (ASSUME_TAC o (Q.SPEC `prefix (label a) k`)) 378 >> REWRITE_TAC [OBS_CONGR] 379 >> rpt STRIP_TAC (* 2 sub-goals here *) 380 >| [ (* goal 1 (of 2) *) 381 IMP_RES_TAC SUM1 \\ 382 POP_ASSUM (ASSUME_TAC o (Q.SPEC `prefix (label a) k`)) \\ 383 PAT_X_ASSUM ``WEAK_EQUIV (sum p (prefix (label a) k)) (sum q (prefix (label a) k))`` 384 (STRIP_ASSUME_TAC o (ONCE_REWRITE_RULE [WEAK_PROPERTY_STAR])) \\ 385 Cases_on `u` >| (* 2 sub-goals here *) 386 [ (* goal 1.1 (of 2) *) 387 RES_TAC \\ 388 PAT_X_ASSUM ``EPS (sum q (prefix (label a) k)) E2`` 389 (STRIP_ASSUME_TAC o (ONCE_REWRITE_RULE [EPS_cases1])) >| (* 2 sub-goals here *) 390 [ (* goal 1.1.1 (of 2) *) 391 `TRANS E2 (label a) k` by PROVE_TAC [PREFIX, SUM2] \\ 392 PAT_X_ASSUM ``WEAK_EQUIV E1 E2`` 393 (STRIP_ASSUME_TAC o (ONCE_REWRITE_RULE [WEAK_PROPERTY_STAR])) \\ 394 RES_TAC \\ 395 IMP_RES_TAC TRANS_TAU_AND_WEAK \\ 396 PROVE_TAC [], 397 (* goal 1.1.2 (of 2) *) 398 PAT_X_ASSUM ``TRANS (sum q (prefix (label a) k)) tau u`` 399 (STRIP_ASSUME_TAC o (MATCH_MP TRANS_SUM)) >| (* 2 sub-goals here *) 400 [ (* goal 1.1.2.1 (of 2) *) 401 Q.EXISTS_TAC `E2` >> ASM_REWRITE_TAC [] \\ 402 IMP_RES_TAC TRANS_AND_EPS, 403 (* goal 1.1.2.2 (of 2) *) 404 IMP_RES_TAC TRANS_PREFIX \\ 405 RW_TAC std_ss [Action_distinct_label] ] ], 406 (* goal 1.2 (of 2) *) 407 Cases_on `x = a` >| (* 2 sub-goals here *) 408 [ (* goal 1.2.1 (of 2) *) 409 FULL_SIMP_TAC std_ss [] >> RES_TAC \\ 410 Q.EXISTS_TAC `E2` >> ASM_REWRITE_TAC [] \\ 411 IMP_RES_TAC WEAK_TRANS_cases1 >| (* 2 sub-goals here *) 412 [ (* goal 1.2.1.1 (of 2) *) 413 PAT_X_ASSUM ``TRANS (sum q (prefix (label a) k)) tau E'`` 414 (STRIP_ASSUME_TAC o (MATCH_MP TRANS_SUM)) >| (* 2 sub-goals here *) 415 [ (* goal 1.2.1.1.1 (of 2) *) 416 IMP_RES_TAC TRANS_TAU_AND_WEAK, 417 (* goal 1.2.1.1.2 (of 2) *) 418 IMP_RES_TAC TRANS_PREFIX \\ 419 RW_TAC std_ss [Action_distinct] ], 420 (* goal 1.2.1.2 (of 2) *) 421 PAT_X_ASSUM ``TRANS (sum q (prefix (label a) k)) (label a) E'`` 422 (STRIP_ASSUME_TAC o (MATCH_MP TRANS_SUM)) >| (* 2 sub-goals here *) 423 [ (* goal 1.2.1.2.1 (of 2) *) 424 IMP_RES_TAC TRANS_AND_EPS, 425 (* goal 1.2.1.2.2 (of 2) *) 426 IMP_RES_TAC TRANS_PREFIX \\ 427 `WEAK_EQUIV E1 k` by PROVE_TAC [EPS_STABLE'] \\ 428 IMP_RES_TAC TRANS_IMP_WEAK_TRANS \\ 429 RES_TAC ] ], 430 (* goal 1.2.2 (of 2) *) 431 RES_TAC \\ 432 Q.EXISTS_TAC `E2` >> ASM_REWRITE_TAC [] \\ 433 IMP_RES_TAC WEAK_TRANS_cases1 >| (* 2 sub-goals here *) 434 [ (* goal 1.2.2.1 (of 2) *) 435 PAT_X_ASSUM ``TRANS (sum q (prefix (label a) k)) tau E'`` 436 (STRIP_ASSUME_TAC o (MATCH_MP TRANS_SUM)) >| (* 2 sub-goals here *) 437 [ (* goal 1.2.2.1.1 (of 2) *) 438 IMP_RES_TAC TRANS_TAU_AND_WEAK, 439 (* goal 1.2.2.1.2 (of 2) *) 440 IMP_RES_TAC TRANS_PREFIX \\ 441 RW_TAC std_ss [Action_distinct] ], 442 (* goal 1.2.2.2 (of 2) *) 443 PAT_X_ASSUM ``TRANS (sum q (prefix (label a) k)) (label x) E'`` 444 (STRIP_ASSUME_TAC o (MATCH_MP TRANS_SUM)) >| (* 2 sub-goals here *) 445 [ (* goal 1.2.2.2.1 (of 2) *) 446 IMP_RES_TAC TRANS_AND_EPS, 447 (* goal 1.2.2.2.2 (of 2) *) 448 IMP_RES_TAC TRANS_PREFIX \\ 449 RW_TAC std_ss [Action_11] ] ] ] ], 450 (* goal 2 (of 2), almost symmetric with goal 1 *) 451 IMP_RES_TAC SUM1 \\ 452 POP_ASSUM (ASSUME_TAC o (Q.SPEC `prefix (label a) k`)) \\ 453 PAT_X_ASSUM ``WEAK_EQUIV (sum p (prefix (label a) k)) (sum h (prefix (label a) k))`` 454 (STRIP_ASSUME_TAC o (ONCE_REWRITE_RULE [WEAK_PROPERTY_STAR])) \\ 455 Cases_on `u` >| (* 2 sub-goals here *) 456 [ (* goal 2.1 (of 2) *) 457 RES_TAC \\ 458 PAT_X_ASSUM ``EPS (sum p (prefix (label a) k)) E1`` 459 (STRIP_ASSUME_TAC o (ONCE_REWRITE_RULE [EPS_cases1])) >| (* 2 sub-goals here *) 460 [ (* goal 2.1.1 (of 2) *) 461 `TRANS E1 (label a) k` by PROVE_TAC [PREFIX, SUM2] \\ 462 PAT_X_ASSUM ``WEAK_EQUIV E1 E2`` 463 (STRIP_ASSUME_TAC o (ONCE_REWRITE_RULE [WEAK_PROPERTY_STAR])) \\ 464 RES_TAC \\ 465 IMP_RES_TAC TRANS_TAU_AND_WEAK \\ 466 `WEAK_EQUIV E2' k` by PROVE_TAC [WEAK_EQUIV_SYM] \\ (* one extra step *) 467 PROVE_TAC [], 468 (* goal 2.1.2 (of 2) *) 469 PAT_X_ASSUM ``TRANS (sum p (prefix (label a) k)) tau u`` 470 (STRIP_ASSUME_TAC o (MATCH_MP TRANS_SUM)) >| (* 2 sub-goals here *) 471 [ (* goal 2.1.2.1 (of 2) *) 472 Q.EXISTS_TAC `E1` >> ASM_REWRITE_TAC [] \\ 473 IMP_RES_TAC TRANS_AND_EPS, 474 (* goal 2.1.2.2 (of 2) *) 475 IMP_RES_TAC TRANS_PREFIX \\ 476 RW_TAC std_ss [Action_distinct_label] ] ], 477 (* goal 2.2 (of 2) *) 478 Cases_on `x = a` >| (* 2 sub-goals here *) 479 [ (* goal 2.2.1 (of 2) *) 480 FULL_SIMP_TAC std_ss [] >> RES_TAC \\ 481 Q.EXISTS_TAC `E1` >> ASM_REWRITE_TAC [] \\ 482 IMP_RES_TAC WEAK_TRANS_cases1 >| (* 2 sub-goals here *) 483 [ (* goal 2.2.1.1 (of 2) *) 484 PAT_X_ASSUM ``TRANS (sum p (prefix (label a) k)) tau E'`` 485 (STRIP_ASSUME_TAC o (MATCH_MP TRANS_SUM)) >| (* 2 sub-goals here *) 486 [ (* goal 2.2.1.1.1 (of 2) *) 487 IMP_RES_TAC TRANS_TAU_AND_WEAK, 488 (* goal 2.2.1.1.2 (of 2) *) 489 IMP_RES_TAC TRANS_PREFIX \\ 490 RW_TAC std_ss [Action_distinct] ], 491 (* goal 2.2.1.2 (of 2) *) 492 PAT_X_ASSUM ``TRANS (sum p (prefix (label a) k)) (label a) E'`` 493 (STRIP_ASSUME_TAC o (MATCH_MP TRANS_SUM)) >| (* 2 sub-goals here *) 494 [ (* goal 2.2.1.2.1 (of 2) *) 495 IMP_RES_TAC TRANS_AND_EPS, 496 (* goal 2.2.1.2.2 (of 2) *) 497 IMP_RES_TAC TRANS_PREFIX \\ 498 `WEAK_EQUIV E2 k` by PROVE_TAC [EPS_STABLE', WEAK_EQUIV_SYM] \\ 499 IMP_RES_TAC TRANS_IMP_WEAK_TRANS \\ 500 RES_TAC ] ], 501 (* goal 2.2.2 (of 2) *) 502 RES_TAC \\ 503 Q.EXISTS_TAC `E1` >> ASM_REWRITE_TAC [] \\ 504 IMP_RES_TAC WEAK_TRANS_cases1 >| (* 2 sub-goals here *) 505 [ (* goal 2.2.2.1 (of 2) *) 506 PAT_X_ASSUM ``TRANS (sum p (prefix (label a) k)) tau E'`` 507 (STRIP_ASSUME_TAC o (MATCH_MP TRANS_SUM)) >| (* 2 sub-goals here *) 508 [ (* goal 2.2.2.1.1 (of 2) *) 509 IMP_RES_TAC TRANS_TAU_AND_WEAK, 510 (* goal 2.2.2.1.2 (of 2) *) 511 IMP_RES_TAC TRANS_PREFIX \\ 512 RW_TAC std_ss [Action_distinct] ], 513 (* goal 2.2.2.2 (of 2) *) 514 PAT_X_ASSUM ``TRANS (sum p (prefix (label a) k)) (label x) E'`` 515 (STRIP_ASSUME_TAC o (MATCH_MP TRANS_SUM)) >| (* 2 sub-goals here *) 516 [ (* goal 2.2.2.2.1 (of 2) *) 517 IMP_RES_TAC TRANS_AND_EPS, 518 (* goal 2.2.2.2.2 (of 2) *) 519 IMP_RES_TAC TRANS_PREFIX \\ 520 RW_TAC std_ss [Action_11] ] ] ] ] ]); 521 522(* A variant of Proposition 9 (Jan Willem Klop) from [vGl05]. In this theory, all CCS 523 processes are finitary, and this makes the lemma relatively easy. *) 524 525(* (KLOP :'b Label -> num -> ('a, 'b) CCS) *) 526val KLOP_def = Define ` 527 (KLOP (a: 'b Label) (0 :num) = nil) /\ 528 (KLOP a (SUC n) = sum (KLOP a n) (prefix (label a) (KLOP a n))) `; 529 530val K0_NO_TRANS = store_thm ( 531 "K0_NO_TRANS", ``!(a :'b Label) u E. ~(TRANS (KLOP a 0) u E)``, 532 rpt GEN_TAC 533 >> REWRITE_TAC [KLOP_def] 534 >> REWRITE_TAC [NIL_NO_TRANS]); 535 536(* Klop processes are STABLE. *) 537val KLOP_PROP0 = store_thm ((* NEW *) 538 "KLOP_PROP0", ``!(a :'b Label) n. STABLE (KLOP a n)``, 539 GEN_TAC 540 >> Induct_on `n` (* 2 sub-goals here *) 541 >- REWRITE_TAC [STABLE, KLOP_def, NIL_NO_TRANS] 542 >> POP_ASSUM MP_TAC 543 >> REWRITE_TAC [STABLE, KLOP_def] 544 >> rpt STRIP_TAC 545 >> IMP_RES_TAC TRANS_SUM (* 2 sub-goals here *) 546 >- PROVE_TAC [] 547 >> IMP_RES_TAC TRANS_PREFIX 548 >> PROVE_TAC [Action_distinct]); 549 550(* Any transition of Klop processes is still a Klop process. Together with Prop 0, 551 this also implies that Klop processes are tau-free. *) 552val KLOP_PROP1_LR = store_thm ((* NEW *) 553 "KLOP_PROP1_LR", 554 ``!(a :'b Label) n E. TRANS (KLOP a n) (label a) E ==> ?m. m < n /\ (E = KLOP a m)``, 555 GEN_TAC 556 >> Induct_on `n` (* 2 sub-goals here, first one is easy *) 557 >- PROVE_TAC [K0_NO_TRANS] 558 >> REWRITE_TAC [KLOP_def] 559 >> rpt STRIP_TAC 560 >> IMP_RES_TAC TRANS_SUM (* 2 sub-goals here *) 561 >| [ (* goal 1 (of 2) *) 562 RES_TAC \\ 563 Q.EXISTS_TAC `m` >> ASM_REWRITE_TAC [] \\ 564 IMP_RES_TAC LESS_IMP_LESS_OR_EQ \\ 565 IMP_RES_TAC LESS_EQ_IMP_LESS_SUC, 566 (* goal 2 (of 2) *) 567 IMP_RES_TAC TRANS_PREFIX \\ 568 Q.EXISTS_TAC `n` >> ASM_REWRITE_TAC [] \\ 569 ASSUME_TAC (Q.SPEC `n` LESS_EQ_REFL) \\ 570 IMP_RES_TAC LESS_EQ_IFF_LESS_SUC ]); 571 572val KLOP_PROP1_RL = store_thm ((* NEW *) 573 "KLOP_PROP1_RL", 574 ``!(a :'b Label) n E. (?m. m < n /\ (E = KLOP a m)) ==> TRANS (KLOP a n) (label a) E``, 575 GEN_TAC 576 >> Induct_on `n` (* 2 sub-goals here *) 577 >> rpt STRIP_TAC 578 >- IMP_RES_TAC NOT_LESS_0 579 >> REWRITE_TAC [KLOP_def] 580 >> IMP_RES_TAC LESS_LEMMA1 (* 2 sub-goals here *) 581 >| [ (* goal 1 (of 2) *) 582 MATCH_MP_TAC SUM2 >> ASM_REWRITE_TAC [] \\ 583 REWRITE_TAC [PREFIX], 584 (* goal 2 (of 2) *) 585 RES_TAC \\ 586 MATCH_MP_TAC SUM1 >> ASM_REWRITE_TAC [] ]); 587 588(* Klop processes are closed under transition *) 589val KLOP_PROP1 = store_thm ((* NEW *) 590 "KLOP_PROP1", 591 ``!(a :'b Label) n E. TRANS (KLOP a n) (label a) E = (?m. m < n /\ (E = KLOP a m))``, 592 rpt GEN_TAC 593 >> EQ_TAC (* 2 sub-goals here *) 594 >| [ (* goal 1 (of 2) *) 595 REWRITE_TAC [KLOP_PROP1_LR], 596 (* goal 2 (of 2) *) 597 REWRITE_TAC [KLOP_PROP1_RL] ]); 598 599(* Klop processes are closed under weak transition *) 600val KLOP_PROP1' = store_thm ((* NEW *) 601 "KLOP_PROP1'", 602 ``!(a :'b Label) n E. WEAK_TRANS (KLOP a n) (label a) E = (?m. m < n /\ (E = KLOP a m))``, 603 rpt GEN_TAC 604 >> EQ_TAC (* 2 sub-goals here *) 605 >| [ (* goal 1 (of 2) *) 606 DISCH_TAC \\ 607 IMP_RES_TAC WEAK_TRANS_cases1 >| (* 2 sub-goals here *) 608 [ (* goal 1.1 (of 2) *) 609 ASSUME_TAC (Q.SPECL [`a`, `n`] KLOP_PROP0) \\ 610 IMP_RES_TAC STABLE_NO_TRANS_TAU, 611 (* goal 1.2 (of 2) *) 612 IMP_RES_TAC KLOP_PROP1_LR \\ 613 IMP_RES_TAC EPS_cases1 >| (* 2 sub-goals here *) 614 [ (* goal 1.2.1 (of 2) *) 615 Q.EXISTS_TAC `m` >> PROVE_TAC [], 616 (* goal 1.2.2 (of 2) *) 617 ASSUME_TAC (Q.SPECL [`a`, `m`] KLOP_PROP0) \\ 618 PROVE_TAC [STABLE_NO_TRANS_TAU] ] ], 619 (* goal 2 (of 2) *) 620 DISCH_TAC \\ 621 MATCH_MP_TAC TRANS_IMP_WEAK_TRANS \\ 622 RW_TAC std_ss [Q.SPECL [`a`, `n`, `E`] KLOP_PROP1_RL] ]); 623 624(* Klop processes are strongly distinct with each other *) 625val KLOP_PROP2 = store_thm ((* NEW *) 626 "KLOP_PROP2", 627 ``!(a :'b Label) n m. m < n ==> ~(STRONG_EQUIV (KLOP a m) (KLOP a n))``, 628 GEN_TAC 629 >> completeInduct_on `n` 630 >> rpt STRIP_TAC 631 >> `TRANS (KLOP a n) (label a) (KLOP a m)` by PROVE_TAC [KLOP_PROP1] 632 >> STRIP_ASSUME_TAC 633 (((Q.SPEC `label a`) o (ONCE_REWRITE_RULE [PROPERTY_STAR])) 634 (ASSUME ``STRONG_EQUIV (KLOP (a :'b Label) m) (KLOP a n)``)) 635 >> RES_TAC 636 >> PAT_X_ASSUM ``TRANS (KLOP (a :'b Label) m) (label a) E1`` 637 (STRIP_ASSUME_TAC o (REWRITE_RULE [KLOP_PROP1])) 638 >> PROVE_TAC []); 639 640(* Klop processes are weakly distinct with each other *) 641val KLOP_PROP2' = store_thm ((* NEW *) 642 "KLOP_PROP2'", 643 ``!(a :'b Label) n m. m < n ==> ~(WEAK_EQUIV (KLOP a m) (KLOP a n))``, 644 GEN_TAC 645 >> completeInduct_on `n` 646 >> rpt STRIP_TAC 647 >> `TRANS (KLOP a n) (label a) (KLOP a m)` by PROVE_TAC [KLOP_PROP1] 648 >> STRIP_ASSUME_TAC 649 (ONCE_REWRITE_RULE [WEAK_PROPERTY_STAR] 650 (ASSUME ``WEAK_EQUIV (KLOP (a :'b Label) m) (KLOP a n)``)) 651 >> RES_TAC 652 >> PAT_X_ASSUM ``WEAK TRANS (KLOP (a :'b Label) m) (label a) E1`` 653 (STRIP_ASSUME_TAC o (REWRITE_RULE [KLOP_PROP1'])) 654 >> PROVE_TAC []); 655 656val KLOP_ONE_ONE = store_thm ((* NEW *) 657 "KLOP_ONE_ONE", ``!(a :'b Label). ONE_ONE (KLOP a)``, 658 REWRITE_TAC [ONE_ONE_DEF] 659 >> BETA_TAC 660 >> rpt STRIP_TAC 661 >> IMP_RES_TAC EQUAL_IMP_STRONG_EQUIV 662 >> CCONTR_TAC 663 >> `x1 < x2 \/ x2 < x1` by PROVE_TAC [LESS_LESS_CASES] (* 2 sub-goals here *) 664 >| [ (* goal 1 (of 2) *) 665 IMP_RES_TAC KLOP_PROP2, 666 (* goal 2 (of 2) *) 667 IMP_RES_TAC KLOP_PROP2 \\ 668 PROVE_TAC [STRONG_EQUIV_SYM] ]); 669 670(* The finite version of Klop's Lemma: 671 672 +----------------------------------- =~ ------------+ 673 | | 674+---+---+-|-+---+---+---+---+---+---+---+---+ | 675| | | n | | | | | | | | | | 676+---+---+-|-+---+---+---+---+---+---+---+---+ | 677 | (nodes) / / | 678 map / / | 679 | / / | 680 | / / | 681+---+---+-|-+---+---+---+---+---+---+---+---+---+---+---+---+-|-+---+---+---+---+-- 682| | | y | | | | | | | | | | | | | k | | | | | .... 683+---+---+---+---+---+---+---+---+---+---+---+---+---+---+---+---+---+---+---+---+-- 684 (klop0) | (klops) 685 686 Proof stretch: 687 688 1. Build nodes = (NODES g) UNION (NODES h) 689 2. Build klops = IMAGE KLOP univ(:num) 690 3. Define map x = if (?y. y IN klops /\ WEAK_EQUIV x y) THEN y ELSE (CHOICE klops) 691 4. Map nodes to klop0, which must be FINITE 692 5. Choose `k` from (klops DIFF klops0) 693 6. For all n in nodes, we prove that n =~ k can't hold. Because if it holds, 694 (y = map n) by definition has two cases: 695 696 a) y =~ n, in this case we have y =~ k, two equivalent elements in klops 697 b) there's no `y` equivalent with n in klops, but we know there is x 698 699 *) 700 701val IN_APP = Q.prove (`!x P. (x IN P) = P x`, 702 SIMP_TAC bool_ss [IN_DEF]); 703 704(* The pure Math part in the proof of KLOP_LEMMA_FINITE *) 705val INFINITE_EXISTS_LEMMA = store_thm ((* NEW *) 706 "INFINITE_EXISTS_LEMMA", 707 ``!R A B. equivalence (R :'a -> 'a -> bool) ==> 708 FINITE (A :'a -> bool) /\ INFINITE (B :'a -> bool) /\ 709 (!x y. x IN B /\ y IN B /\ x <> y ==> ~(R x y)) ==> 710 ?k. k IN B /\ (!n. n IN A ==> ~(R n k))``, 711 rpt GEN_TAC 712 >> REWRITE_TAC [equivalence_def] 713 >> rpt STRIP_TAC 714 715 >> Q.ABBREV_TAC `map = (\x. if (?y. y IN B /\ R x y) then 716 (@y. y IN B /\ R x y) else (CHOICE B))` 717 >> POP_ASSUM (ASSUME_TAC o (* GSYM o *) 718 SIMP_RULE bool_ss [FUN_EQ_THM, markerTheory.Abbrev_def]) 719 >> Know `!x. map x IN B` 720 >- ( GEN_TAC >> ASM_REWRITE_TAC [] \\ 721 RW_TAC std_ss [IN_DEF] >| (* 2 sub-goals here *) 722 [ (* goal 1 (of 2) *) 723 MATCH_MP_TAC SELECT_ELIM_THM \\ (* eliminated `Q (@P)` here *) 724 RW_TAC std_ss [] \\ 725 Q.EXISTS_TAC `y` >> ASM_REWRITE_TAC [], 726 (* goal 2 (of 2) *) 727 ONCE_REWRITE_TAC [GSYM IN_APP] \\ 728 MATCH_MP_TAC CHOICE_DEF \\ 729 PROVE_TAC [FINITE_EMPTY] ] ) >> DISCH_TAC 730 >> Q.ABBREV_TAC `B0 = IMAGE map A` 731 >> `FINITE B0` by PROVE_TAC [IMAGE_FINITE] 732 >> Know `B0 SUBSET B` 733 >- ( REWRITE_TAC [SUBSET_DEF] \\ 734 rpt STRIP_TAC \\ 735 `x IN (IMAGE map A)` by PROVE_TAC [] \\ 736 POP_ASSUM MP_TAC \\ 737 REWRITE_TAC [IN_IMAGE] >> PROVE_TAC [] ) >> DISCH_TAC 738 >> `?k. k IN B /\ k NOTIN B0` 739 by PROVE_TAC [Q.SPECL [`B`, `B0`] IN_INFINITE_NOT_FINITE] 740 >> Q.EXISTS_TAC `k` 741 >> `!n. n IN A ==> map n IN B0` by PROVE_TAC [IN_IMAGE] 742 >> Know `!n. n IN A ==> R n (map n) \/ (~?x. x IN B /\ R n x)` 743 >- ( rpt STRIP_TAC \\ 744 PAT_X_ASSUM ``!x. map x = P`` (ASSUME_TAC o (Q.SPEC `n`)) \\ 745 Cases_on `?y. y IN B /\ R n y` >| (* 2 sub-goals here *) 746 [ (* goal 1 (of 2) *) 747 FULL_SIMP_TAC std_ss [] \\ 748 DISJ1_TAC \\ 749 METIS_TAC [], (* PROVE_TAC doesn't work here *) 750 (* goal 2 (of 2) *) 751 FULL_SIMP_TAC std_ss [] ] ) >> DISCH_TAC 752 >> Know `!n. n IN A ==> ~(R n k)` 753 >- ( rpt STRIP_TAC \\ 754 `map n IN B0` by PROVE_TAC [IMAGE_IN] \\ 755 Q.ABBREV_TAC `y = map n` \\ 756 RES_TAC >| (* 2 sub-goals here *) 757 [ (* goal 1 (of 2) *) 758 `y IN B` by PROVE_TAC [SUBSET_DEF] \\ 759 `R k y` by PROVE_TAC [transitive_def, symmetric_def] \\ 760 Cases_on `k = y` >- PROVE_TAC [] \\ 761 `~(R k y)` by PROVE_TAC [], 762 (* goal 2 (of 2) *) 763 `B k /\ R n k` by PROVE_TAC [IN_DEF] \\ 764 RES_TAC ] ) >> DISCH_TAC 765 >> ASM_REWRITE_TAC []); 766 767val KLOP_LEMMA_FINITE = store_thm ((* NEW *) 768 "KLOP_LEMMA_FINITE", 769 ``!p q. finite_state p /\ finite_state q ==> 770 ?k. STABLE k /\ 771 (!p' u. WEAK_TRANS p u p' ==> ~(WEAK_EQUIV p' k)) /\ 772 (!q' u. WEAK_TRANS q u q' ==> ~(WEAK_EQUIV q' k))``, 773 rpt STRIP_TAC 774 (* Part 1: assert that the union of all nodes in g and h is finite *) 775 >> PAT_X_ASSUM ``finite_state p`` 776 (ASSUME_TAC o (REWRITE_RULE [finite_state_def])) 777 >> PAT_X_ASSUM ``finite_state q`` 778 (ASSUME_TAC o (REWRITE_RULE [finite_state_def])) 779 >> Q.ABBREV_TAC `nodes = (NODES p) UNION (NODES q)` 780 >> `FINITE nodes` by PROVE_TAC [FINITE_UNION] 781(* 782 0. FINITE (NODES g) 783 1. FINITE (NODES h) 784 2. Abbrev (nodes = NODES g ��� NODES h) 785 3. FINITE nodes 786 *) 787 (* Part 2: assert an infinite set of Klop processes *) 788 >> Q.ABBREV_TAC `a = (ARB :'b Label)` 789 >> Q.ABBREV_TAC `f = KLOP a` 790 >> `!x y. (f x = f y) ==> (x = y)` by PROVE_TAC [KLOP_ONE_ONE, ONE_ONE_DEF] 791 >> Q.ABBREV_TAC `klops = IMAGE f (UNIV :num set)` 792 >> `INFINITE klops` by PROVE_TAC [IMAGE_11_INFINITE, INFINITE_NUM_UNIV] 793(* 794 4. Abbrev (a = ARB) 795 5. Abbrev (f = KLOP a) 796 6. ���x y. f x = f y ��� x = y 797 7. Abbrev (klops = IMAGE f ����(:num)) 798 8. INFINITE klops 799*) 800 (* Part 3: assert the distincity of elements in the infinite set *) 801 >> Know `!x y. x IN klops /\ y IN klops /\ x <> y ==> ~(WEAK_EQUIV x y)` 802 >- ( rpt STRIP_TAC \\ 803 `?n. x = KLOP a n` by PROVE_TAC [IN_UNIV, IN_IMAGE] \\ 804 `?m. y = KLOP a m` by PROVE_TAC [IN_UNIV, IN_IMAGE] \\ 805 STRIP_ASSUME_TAC (Q.SPECL [`m`, `n`] LESS_LESS_CASES) >| (* 3 sub-goals here *) 806 [ (* goal 1 (of 3) *) 807 PROVE_TAC [], 808 (* goal 2 (of 3) *) 809 PROVE_TAC [KLOP_PROP2', WEAK_EQUIV_SYM], 810 (* goal 3 (of 3) *) 811 PROVE_TAC [KLOP_PROP2'] ] ) 812 >> DISCH_TAC 813 (* Part 4: assert the existence of k *) 814 >> ASSUME_TAC WEAK_EQUIV_equivalence 815 >> POP_ASSUM (MP_TAC o 816 (MATCH_MP (ISPECL [``WEAK_EQUIV :('a, 'b) simulation``, 817 ``nodes :('a, 'b) CCS -> bool``, 818 ``klops :('a, 'b) CCS -> bool``] INFINITE_EXISTS_LEMMA))) 819 >> RW_TAC std_ss [] 820(* 821 9. ���x y. x ��� klops ��� y ��� klops ��� x ��� y ��� ��(x ��� y) 822 10. k ��� klops 823 11. ���n. n ��� nodes ��� ��(n ��� k) 824 *) 825 >> Q.EXISTS_TAC `k` 826 >> CONJ_TAC (* 2 sub-goals here *) 827 >- ( `k IN IMAGE f UNIV` by PROVE_TAC [] \\ 828 POP_ASSUM (STRIP_ASSUME_TAC o (REWRITE_RULE [IN_IMAGE])) \\ 829 PROVE_TAC [KLOP_PROP0] ) 830 (* Part 5: final check *) 831 >> `!n. n IN (NODES p) ==> ~(WEAK_EQUIV n k)` by PROVE_TAC [IN_UNION] 832 >> `!n. n IN (NODES q) ==> ~(WEAK_EQUIV n k)` by PROVE_TAC [IN_UNION] 833 >> CONJ_TAC (* 2 sub-goals here *) 834 >| [ (* goal 1 (of 2) *) 835 rpt STRIP_TAC \\ 836 IMP_RES_TAC WEAK_TRANS_IN_NODES \\ 837 PROVE_TAC [], 838 (* goal 2 (of 2) *) 839 rpt STRIP_TAC \\ 840 IMP_RES_TAC WEAK_TRANS_IN_NODES \\ 841 PROVE_TAC [] ]); 842 843(* The finite version of COARSEST_CONGR_THM (PROP3) *) 844val COARSEST_CONGR_FINITE = store_thm ((* NEW *) 845 "COARSEST_CONGR_FINITE", 846 ``!p q. finite_state p /\ finite_state q ==> 847 (OBS_CONGR p q = !r. WEAK_EQUIV (sum p r) (sum q r))``, 848 rpt STRIP_TAC 849 >> EQ_TAC >- REWRITE_TAC [COARSEST_CONGR_LR] 850 >> MP_TAC (Q.SPECL [`p`, `q`] KLOP_LEMMA_FINITE) 851 >> RW_TAC std_ss [PROP3_COMMON]); 852 853(* unused *) 854val KLOP_INF_def = Define ` 855 KLOP_INF X a = rec X (sum (var X) (prefix (label a) (var X)))`; 856 857(** Bibliography: 858 859[Den07] Y. Deng, ���A simple completeness proof for the axiomatisations of weak behavioural 860 equivalences���, Bulletin of the EATCS, 93:207-219, 2007. 861 862[Mil89] R. Milner, Communication and Concurrency, Prentice-Hall, 1989. 863 864[vGl05] R.J. van Glabbeek, ���A characterisation of weak bisimulation congruence���, in Processes, 865 Terms and Cycles: Steps on the Road to Infinity, Essays dedicated to Jan Willem Klop, on the 866 occasion of his 60th birthday, LNCS 3838, 26-39. Springer-Verlag, 2005. 867 *) 868 869val _ = export_theory (); 870val _ = html_theory "CoarsestCongr"; 871 872(* last updated: Oct 14, 2017 *) 873