1(* ------------------------------------------------------------------------ *) 2(* Bisimulations defined on general labeled transition ('a->'b->'a->bool) *) 3(* ------------------------------------------------------------------------ *) 4 5open HolKernel Parse boolLib simpLib metisLib BasicProvers; 6open relationTheory; 7 8val _ = new_theory "bisimulation"; 9 10(*---------------------------------------------------------------------------*) 11(* (Strong) bisimulation *) 12(*---------------------------------------------------------------------------*) 13 14val BISIM_def = new_definition ("BISIM_def", 15 ``BISIM ts R = !p q. 16 R p q ==> !l. 17 (!p'. ts p l p' ==> ?q'. ts q l q' /\ R p' q') /\ 18 (!q'. ts q l q' ==> ?p'. ts p l p' /\ R p' q')``); 19 20(* (Strong) bisimilarity, see BISIM_REL_def for an alternative definition *) 21CoInductive BISIM_REL : 22 !p q. (!l. 23 (!p'. ts p l p' ==> ?q'. ts q l q' /\ (BISIM_REL ts) p' q') /\ 24 (!q'. ts q l q' ==> ?p'. ts p l p' /\ (BISIM_REL ts) p' q')) 25 ==> (BISIM_REL ts) p q 26End 27 28Theorem BISIM_ID : 29 !ts. BISIM ts Id 30Proof 31 SRW_TAC[][BISIM_def] 32QED 33 34Theorem BISIM_INV : 35 !ts R. BISIM ts R ==> BISIM ts (inv R) 36Proof 37 SRW_TAC[][BISIM_def, inv_DEF] >> METIS_TAC [] 38QED 39 40Theorem BISIM_O : 41 !ts R R'. BISIM ts R /\ BISIM ts R' ==> BISIM ts (R' O R) 42Proof 43 rpt STRIP_TAC 44 >> PURE_ONCE_REWRITE_TAC [BISIM_def] 45 >> SRW_TAC[][O_DEF] 46 >> METIS_TAC[BISIM_def] 47QED 48 49Theorem BISIM_RUNION : 50 !ts R R'. BISIM ts R /\ BISIM ts R' ==> BISIM ts (R RUNION R') 51Proof 52 rpt GEN_TAC 53 >> PURE_ONCE_REWRITE_TAC [BISIM_def] 54 >> SRW_TAC[][RUNION] 55 >> METIS_TAC[] 56QED 57 58Theorem BISIM_REL_IS_BISIM : 59 !ts. BISIM ts (BISIM_REL ts) 60Proof 61 PURE_ONCE_REWRITE_TAC [BISIM_def] 62 >> rpt GEN_TAC >> DISCH_TAC 63 >> Q.SPEC_TAC (`l`, `l`) 64 >> PURE_ONCE_REWRITE_TAC [GSYM BISIM_REL_cases] 65 >> ASM_REWRITE_TAC [] 66QED 67 68(* (Strong) bisimilarity, the original definition *) 69Theorem BISIM_REL_def : 70 !ts. BISIM_REL ts = \p q. ?R. BISIM ts R /\ R p q 71Proof 72 SRW_TAC[][FUN_EQ_THM] 73 >> EQ_TAC 74 >| [ (* goal 1 (of 2) *) 75 DISCH_TAC >> Q.EXISTS_TAC `BISIM_REL ts` \\ 76 ASM_REWRITE_TAC [BISIM_REL_IS_BISIM], 77 (* goal 2 (of 2) *) 78 Q.SPEC_TAC (`q`, `q`) \\ 79 Q.SPEC_TAC (`p`, `p`) \\ 80 HO_MATCH_MP_TAC BISIM_REL_coind \\ (* co-induction used here! *) 81 PROVE_TAC [BISIM_def] ] 82QED 83 84Theorem BISIM_REL_IS_EQUIV_REL : 85 !ts. equivalence (BISIM_REL ts) 86Proof 87 SRW_TAC[][equivalence_def] 88 >- (SRW_TAC[][reflexive_def, BISIM_REL_def] \\ 89 Q.EXISTS_TAC `Id` \\ 90 REWRITE_TAC [BISIM_ID]) 91 >- (SRW_TAC[][symmetric_def, BISIM_REL_def] \\ 92 SRW_TAC[][EQ_IMP_THM] \\ 93 Q.EXISTS_TAC `SC R` \\ 94 FULL_SIMP_TAC (srw_ss ()) [BISIM_def, SC_DEF] \\ 95 METIS_TAC[]) 96 >- (SRW_TAC[][transitive_def, BISIM_REL_def] \\ 97 Q.EXISTS_TAC `R' O R` \\ 98 METIS_TAC [O_DEF, BISIM_O]) 99QED 100 101 102(*---------------------------------------------------------------------------*) 103(* Weak bisimulation *) 104(*---------------------------------------------------------------------------*) 105 106(* Empty transition: zero or more invisible actions *) 107val ETS_def = new_definition ("ETS_def", (* was: EPS *) 108 ``ETS ts tau = RTC (\x y. ts x tau y)``); 109 110(* Weak transition *) 111val WTS_def = new_definition ("WTS_def", 112 ``WTS ts tau = 113 \p l q. ?p' q'. (ETS ts tau) p p' /\ ts p' l q' /\ (ETS ts tau) q' q``); 114 115(* Weak bisimulation *) 116val WBISIM_def = new_definition ("WBISIM_def", 117 ``WBISIM ts tau R = 118 !p q. R p q ==> 119 (!l. l <> tau ==> 120 (!p'. ts p l p' ==> ?q'. (WTS ts tau) q l q' /\ R p' q') /\ 121 (!q'. ts q l q' ==> ?p'. (WTS ts tau) p l p' /\ R p' q')) /\ 122 (!p'. ts p tau p' ==> ?q'. (ETS ts tau) q q' /\ R p' q') /\ 123 (!q'. ts q tau q' ==> ?p'. (ETS ts tau) p p' /\ R p' q')``); 124 125(* Weak bisimilarity, see WBISIM_REL_def for an alternative definition *) 126CoInductive WBISIM_REL : 127 !p q. 128 (!l. l <> tau ==> 129 (!p'. ts p l p' ==> ?q'. WTS ts tau q l q' /\ WBISIM_REL ts tau p' q') /\ 130 (!q'. ts q l q' ==> ?p'. WTS ts tau p l p' /\ WBISIM_REL ts tau p' q')) /\ 131 (!p'. ts p tau p' ==> ?q'. ETS ts tau q q' /\ WBISIM_REL ts tau p' q') /\ 132 (!q'. ts q tau q' ==> ?p'. ETS ts tau p p' /\ WBISIM_REL ts tau p' q') 133 ==> 134 WBISIM_REL ts tau p q 135End 136 137Theorem TS_IMP_ETS : 138 !ts tau p q. ts p tau q ==> (ETS ts tau) p q 139Proof 140 SRW_TAC[][ETS_def] 141 >> MATCH_MP_TAC RTC_SINGLE 142 >> BETA_TAC >> ASM_REWRITE_TAC [] 143QED 144 145Theorem ETS_REFL : 146 !ts tau p. (ETS ts tau) p p 147Proof 148 SRW_TAC[][ETS_def, RTC_REFL] 149QED 150 151Theorem TS_IMP_WTS : 152 !ts tau p l q. ts p l q ==> WTS ts tau p l q 153Proof 154 SRW_TAC[][WTS_def] 155 >> Q.EXISTS_TAC `p` 156 >> Q.EXISTS_TAC `q` 157 >> ASM_REWRITE_TAC [ETS_REFL] 158QED 159 160Theorem ETS_TRANS : 161 !ts tau x y z. (ETS ts tau) x y /\ (ETS ts tau) y z 162 ==> (ETS ts tau) x z 163Proof 164 SRW_TAC[][ETS_def] 165 >> MATCH_MP_TAC (REWRITE_RULE [transitive_def] RTC_TRANSITIVE) 166 >> Q.EXISTS_TAC `y` 167 >> ASM_REWRITE_TAC [] 168QED 169 170val lemma1 = prove ( 171 ``!R. (!p q. ts p tau q ==> R p q) /\ 172 (!p. R p p) /\ 173 (!p q r. R p q /\ R q r ==> R p r) 174 ==> !p q. (ETS ts tau) p q ==> R p q``, 175 GEN_TAC >> STRIP_TAC 176 >> REWRITE_TAC [ETS_def] 177 >> HO_MATCH_MP_TAC RTC_INDUCT 178 >> METIS_TAC []); 179 180Theorem ETS_WTS_ETS : 181 !ts tau p p1 l p2 p'. 182 (ETS ts tau) p p1 /\ (WTS ts tau) p1 l p2 /\ (ETS ts tau) p2 p' 183 ==> (WTS ts tau) p l p' 184Proof 185 SRW_TAC[][WTS_def] 186 >> Q.EXISTS_TAC `p''` 187 >> Q.EXISTS_TAC `q'` 188 >> ASM_REWRITE_TAC [] 189 >> METIS_TAC [ETS_TRANS] 190QED 191 192Theorem WBISIM_INV : 193 !ts tau R. WBISIM ts tau R ==> WBISIM ts tau (inv R) 194Proof 195 SRW_TAC[][WBISIM_def, inv_DEF] >> METIS_TAC [] 196QED 197 198Theorem lemma2[local]: 199 !p p'. (ETS ts tau) p p' ==> 200 !R q. WBISIM ts tau R /\ R p q ==> ?q'. (ETS ts tau) q q' /\ R p' q' 201Proof 202 HO_MATCH_MP_TAC lemma1 203 >> SRW_TAC[][] 204 >| [ (* goal 1 (of 3) *) 205 FULL_SIMP_TAC (srw_ss()) [WBISIM_def] \\ 206 RES_TAC >> Q.EXISTS_TAC `q'` >> ASM_REWRITE_TAC [], 207 (* goal 2 (of 3) *) 208 FULL_SIMP_TAC (srw_ss()) [WBISIM_def] \\ 209 RES_TAC >> Q.EXISTS_TAC `q` \\ 210 ASM_REWRITE_TAC [ETS_def, RTC_REFL], 211 (* goal 3 (of 3) *) 212 `?q'. ETS ts tau q q' /\ R p' q'` by PROVE_TAC [] \\ 213 `?q''. ETS ts tau q' q'' /\ R p'' q''` by PROVE_TAC [] \\ 214 Q.EXISTS_TAC `q''` >> ASM_REWRITE_TAC [] \\ 215 FULL_SIMP_TAC (srw_ss()) [ETS_def] \\ 216 MATCH_MP_TAC (REWRITE_RULE [transitive_def] RTC_TRANSITIVE) \\ 217 Q.EXISTS_TAC `q'` >> ASM_REWRITE_TAC [] ] 218QED 219 220val lemma2' = prove ( 221 ``!q q'. (ETS ts tau) q q' ==> 222 !R p. WBISIM ts tau R /\ R p q ==> 223 ?p'. (ETS ts tau) p p' /\ R p' q'``, 224 rpt STRIP_TAC 225 >> MP_TAC (Q.SPECL [`q`, `q'`] lemma2) >> SRW_TAC[][] 226 >> POP_ASSUM (MP_TAC o (REWRITE_RULE [inv_DEF]) o (Q.SPECL [`inv R`, `p`])) 227 >> IMP_RES_TAC WBISIM_INV 228 >> SRW_TAC[][]); 229 230(* p ==> p1 -l-> p2 ==> p' 231 R R R R 232 q ==> q1 =l=> q2 ==> q' 233 *) 234val lemma3 = prove ( 235 ``!p l p'. (WTS ts tau) p l p' /\ l <> tau ==> 236 !R q. WBISIM ts tau R /\ R p q ==> 237 ?q'. (WTS ts tau) q l q' /\ R p' q'``, 238 rpt STRIP_TAC 239 >> `?p1 p2. (ETS ts tau) p p1 /\ ts p1 l p2 /\ (ETS ts tau) p2 p'` 240 by PROVE_TAC [WTS_def] 241 >> `?q1. (ETS ts tau) q q1 /\ R p1 q1` by PROVE_TAC [lemma2] 242 >> `?q2. (WTS ts tau) q1 l q2 /\ R p2 q2` by PROVE_TAC [WBISIM_def] 243 >> `?q'. (ETS ts tau) q2 q' /\ R p' q'` by PROVE_TAC [lemma2] 244 >> Q.EXISTS_TAC `q'` >> ASM_REWRITE_TAC [] 245 >> MATCH_MP_TAC ETS_WTS_ETS 246 >> Q.EXISTS_TAC `q1` 247 >> Q.EXISTS_TAC `q2` 248 >> ASM_REWRITE_TAC []); 249 250val lemma3' = prove ( 251 ``!q l q'. (WTS ts tau) q l q' /\ l <> tau ==> 252 !R p. WBISIM ts tau R /\ R p q ==> 253 ?p'. (WTS ts tau) p l p' /\ R p' q'``, 254 rpt STRIP_TAC 255 >> MP_TAC (Q.SPECL [`q`, `l`, `q'`] lemma3) >> SRW_TAC[][] 256 >> POP_ASSUM (MP_TAC o (REWRITE_RULE [inv_DEF]) o (Q.SPECL [`inv R`, `p`])) 257 >> IMP_RES_TAC WBISIM_INV 258 >> SRW_TAC[][]); 259 260Theorem WBISIM_ID : 261 !ts tau. WBISIM ts tau Id 262Proof 263 SRW_TAC[][WBISIM_def] 264 >- (MATCH_MP_TAC TS_IMP_WTS >> ASM_REWRITE_TAC []) 265 >> MATCH_MP_TAC TS_IMP_ETS >> ASM_REWRITE_TAC [] 266QED 267 268Theorem WBISIM_INV : 269 !ts tau R. WBISIM ts tau R ==> WBISIM ts tau (inv R) 270Proof 271 SRW_TAC[][WBISIM_def, inv_DEF] >> METIS_TAC [] 272QED 273 274Theorem WBISIM_O : 275 !ts tau R R'. WBISIM ts tau R /\ WBISIM ts tau R' ==> 276 WBISIM ts tau (R' O R) 277Proof 278 rpt STRIP_TAC 279 >> PURE_ONCE_REWRITE_TAC [WBISIM_def] 280 >> SRW_TAC[][O_DEF] 281 >| [ METIS_TAC [WBISIM_def, lemma3], 282 METIS_TAC [WBISIM_def, lemma3'], 283 METIS_TAC [WBISIM_def, lemma2], 284 METIS_TAC [WBISIM_def, lemma2'] ] 285QED 286 287Theorem WBISIM_RUNION : 288 !ts tau R R'. WBISIM ts tau R /\ WBISIM ts tau R' ==> 289 WBISIM ts tau (R RUNION R') 290Proof 291 rpt GEN_TAC 292 >> PURE_ONCE_REWRITE_TAC [WBISIM_def] 293 >> REWRITE_TAC [RUNION] >> BETA_TAC 294 >> rpt STRIP_TAC 295 >> RES_TAC (* 8 sub-goals here, the same last tactic *) 296 >| [ Q.EXISTS_TAC `q'`, Q.EXISTS_TAC `p'`, 297 Q.EXISTS_TAC `q'`, Q.EXISTS_TAC `p'`, 298 Q.EXISTS_TAC `q'`, Q.EXISTS_TAC `p'`, 299 Q.EXISTS_TAC `q'`, Q.EXISTS_TAC `p'` ] 300 >> ASM_REWRITE_TAC [] 301QED 302 303Theorem WBISIM_REL_IS_WBISIM : 304 !ts tau. WBISIM ts tau (WBISIM_REL ts tau) 305Proof 306 PURE_ONCE_REWRITE_TAC [WBISIM_def] 307 >> rpt GEN_TAC >> DISCH_TAC 308 >> PURE_ONCE_REWRITE_TAC [GSYM WBISIM_REL_cases] 309 >> ASM_REWRITE_TAC [] 310QED 311 312(* Weak bisimilarity, the original definition *) 313Theorem WBISIM_REL_def : 314 !ts tau. WBISIM_REL ts tau = \p q. ?R. WBISIM ts tau R /\ R p q 315Proof 316 SRW_TAC[][FUN_EQ_THM] 317 >> EQ_TAC 318 >| [ (* goal 1 (of 2) *) 319 DISCH_TAC >> Q.EXISTS_TAC `WBISIM_REL ts tau` \\ 320 ASM_REWRITE_TAC [WBISIM_REL_IS_WBISIM], 321 (* goal 2 (of 2) *) 322 Q.SPEC_TAC (`q`, `q`) \\ 323 Q.SPEC_TAC (`p`, `p`) \\ 324 HO_MATCH_MP_TAC WBISIM_REL_coind \\ (* co-induction used here! *) 325 PROVE_TAC [WBISIM_def] ] 326QED 327 328Theorem WBISIM_REL_IS_EQUIV_REL : 329 !ts tau. equivalence (WBISIM_REL ts tau) 330Proof 331 SRW_TAC[][equivalence_def] 332 >- (SRW_TAC[][reflexive_def, WBISIM_REL_def] \\ 333 Q.EXISTS_TAC `Id` \\ 334 SRW_TAC[][WBISIM_def, WBISIM_ID]) 335 >- (SRW_TAC[][symmetric_def, WBISIM_REL_def] \\ 336 SRW_TAC[][EQ_IMP_THM] \\ 337 Q.EXISTS_TAC `SC R` \\ 338 FULL_SIMP_TAC (srw_ss ()) [WBISIM_def, SC_DEF] \\ 339 METIS_TAC []) 340 >- (SRW_TAC[][transitive_def, WBISIM_REL_def] >> 341 Q.EXISTS_TAC `R' O R` \\ 342 METIS_TAC [WBISIM_O, O_DEF]) 343QED 344 345 346(*---------------------------------------------------------------------------*) 347(* Relations between strong and weak bisimulations *) 348(*---------------------------------------------------------------------------*) 349 350Theorem BISIM_IMP_WBISIM : 351 !ts tau R. BISIM ts R ==> WBISIM ts tau R 352Proof 353 SRW_TAC[][WBISIM_def] (* 4 goals *) 354 >> IMP_RES_TAC BISIM_def 355 >| [ (* goal 1 (of 4) *) 356 Q.EXISTS_TAC `q'` >> ASM_REWRITE_TAC [] \\ 357 MATCH_MP_TAC TS_IMP_WTS, 358 (* goal 2 (of 4) *) 359 Q.EXISTS_TAC `p'` >> ASM_REWRITE_TAC [] \\ 360 MATCH_MP_TAC TS_IMP_WTS, 361 (* goal 3 (of 4) *) 362 Q.EXISTS_TAC `q'` >> ASM_REWRITE_TAC [] \\ 363 MATCH_MP_TAC TS_IMP_ETS, 364 (* goal 4 (of 4) *) 365 Q.EXISTS_TAC `p'` >> ASM_REWRITE_TAC [] \\ 366 MATCH_MP_TAC TS_IMP_ETS ] 367 >> ASM_REWRITE_TAC [] 368QED 369 370Theorem BISIM_REL_RSUBSET_WBISIM_REL : 371 !ts tau. (BISIM_REL ts) RSUBSET (WBISIM_REL ts tau) 372Proof 373 SRW_TAC[][RSUBSET, BISIM_REL_def, WBISIM_REL_def] 374 >> Q.EXISTS_TAC `R` >> ASM_REWRITE_TAC [] 375 >> MATCH_MP_TAC BISIM_IMP_WBISIM 376 >> ASM_REWRITE_TAC [] 377QED 378 379Theorem BISIM_REL_IMP_WBISIM_REL : 380 !ts tau p q. (BISIM_REL ts) p q ==> (WBISIM_REL ts tau) p q 381Proof 382 REWRITE_TAC [GSYM RSUBSET, BISIM_REL_RSUBSET_WBISIM_REL] 383QED 384 385val _ = export_theory (); 386