Theory Bisimilarity

Up to index of Isabelle/HOL/PI

theory Bisimilarity = Congruence + WkTrans
files [Bisimilarity.ML]:
```Bisimilarity = Congruence + WkTrans +

consts
sim :: "(('a::inf_class) procs * 'a procs) set"
bisim :: "(('a::inf_class) procs * 'a procs) set"

syntax
"@sim" :: "[('a::inf_class) procs, 'a procs] => bool"
(infixl ".<" 60)
"@bisim" :: "[('a::inf_class) procs, 'a procs] => bool"
(infixl ".=" 60)

translations
"P .< Q" == "(P, Q) : sim"
"P .= Q" == "(P, Q) : bisim"

coinductive "bisim"
intrs
intr   "[| ALL a b P'. P -a<b>-> P' --> (EX Q' P'' Q''. Q =a<b>=> Q' & \
\     P' .> P'' & Q' .> Q'' & P'' .= Q'') ; \
\ ALL a fP'. P -a<>-> fP' --> (EX fQ'. Q =a<>=> fQ' & \
\     (ALL c. fresha c fP' & fresha c fQ' --> \
\             (EX P'' Q''. fP' c .> P'' & fQ' c .> Q'' & P'' .= Q''))) ; \
\ ALL a fP'. P -a[]-> fP' --> (EX fQ'. Q =a[]=> fQ' & \
\     (ALL c. EX P'' Q''. fP' c .> P'' & fQ' c .> Q'' & P'' .= Q'')) ;\
\ ALL P'. P -tau-> P' --> (EX Q' P'' Q''. Q =eps=> Q' & \
\     P' .> P'' & Q' .> Q'' & P'' .= Q'') ; \
\ ALL a b Q'. Q -a<b>-> Q' --> (EX P' P'' Q''. P =a<b>=> P' & \
\     P' .> P'' & Q' .> Q'' & P'' .= Q'') ; \
\ ALL a fQ'. Q -a<>-> fQ' --> (EX fP'. P =a<>=> fP' & \
\     (ALL c. fresha c fP' & fresha c fQ' --> \
\             (EX P'' Q''. fP' c .> P'' & fQ' c .> Q'' & P'' .= Q''))) ;\
\ ALL a fQ'. Q -a[]-> fQ' --> (EX fP'. P =a[]=> fP' & \
\     (ALL c. EX P'' Q''. fP' c .> P'' & fQ' c .> Q'' & P'' .= Q'')) ; \
\ ALL Q'. Q -tau-> Q' --> (EX P' P'' Q''. P =eps=> P' & \
\     P' .> P'' & Q' .> Q'' & P'' .= Q'') |] ==> P .= Q"

end
```

theorem bisimI:

```  [| (P, Q) : X;
!!P Q a b P'.
[| (P, Q) : X; P -a<b>-> P' |]
==> EX Q' P'' Q''.
Q =a<b>=> Q' & P' .> P'' & Q' .> Q'' & (P'', Q'') : X Un bisim;
!!P Q a fP'.
[| (P, Q) : X; P -a<>-> fP' |]
==> EX fQ'.
Q =a<>=> fQ' &
(ALL c. fresha c fP' & fresha c fQ' -->
(EX P'' Q''.
fP' c .> P'' &
fQ' c .> Q'' & (P'', Q'') : X Un bisim));
!!P Q a fP'.
[| (P, Q) : X; P -a[]-> fP' |]
==> EX fQ'.
Q =a[]=> fQ' &
(ALL c. EX P'' Q''.
fP' c .> P'' & fQ' c .> Q'' & (P'', Q'') : X Un bisim);
!!P Q P'.
[| (P, Q) : X; P -tau-> P' |]
==> EX Q' P'' Q''.
Q =eps=> Q' & P' .> P'' & Q' .> Q'' & (P'', Q'') : X Un bisim;
!!P Q a b Q'.
[| (P, Q) : X; Q -a<b>-> Q' |]
==> EX P' P'' Q''.
P =a<b>=> P' & P' .> P'' & Q' .> Q'' & (P'', Q'') : X Un bisim;
!!P Q a fQ'.
[| (P, Q) : X; Q -a<>-> fQ' |]
==> EX fP'.
P =a<>=> fP' &
(ALL c. fresha c fP' & fresha c fQ' -->
(EX P'' Q''.
fP' c .> P'' &
fQ' c .> Q'' & (P'', Q'') : X Un bisim));
!!P Q a fQ'.
[| (P, Q) : X; Q -a[]-> fQ' |]
==> EX fP'.
P =a[]=> fP' &
(ALL c. EX P'' Q''.
fP' c .> P'' & fQ' c .> Q'' & (P'', Q'') : X Un bisim);
!!P Q Q'.
[| (P, Q) : X; Q -tau-> Q' |]
==> EX P' P'' Q''.
P =eps=> P' & P' .> P'' & Q' .> Q'' & (P'', Q'') : X Un bisim |]
==> P .= Q```

theorem plain_bisimI:

```  [| (P, Q) : X;
!!P Q a b P'.
[| (P, Q) : X; P -a<b>-> P' |]
==> EX Q' P'' Q''. Q =a<b>=> Q' & (P', Q') : X Un bisim;
!!P Q a fP'.
[| (P, Q) : X; P -a<>-> fP' |]
==> EX fQ'.
Q =a<>=> fQ' &
(ALL c. fresha c fP' & fresha c fQ' -->
(fP' c, fQ' c) : X Un bisim);
!!P Q a fP'.
[| (P, Q) : X; P -a[]-> fP' |]
==> EX fQ'. Q =a[]=> fQ' & (ALL c. (fP' c, fQ' c) : X Un bisim);
!!P Q P'.
[| (P, Q) : X; P -tau-> P' |]
==> EX Q' P'' Q''. Q =eps=> Q' & (P', Q') : X Un bisim;
!!P Q a b Q'.
[| (P, Q) : X; Q -a<b>-> Q' |]
==> EX P' P'' Q''. P =a<b>=> P' & (P', Q') : X Un bisim;
!!P Q a fQ'.
[| (P, Q) : X; Q -a<>-> fQ' |]
==> EX fP'.
P =a<>=> fP' &
(ALL c. fresha c fP' & fresha c fQ' -->
(fP' c, fQ' c) : X Un bisim);
!!P Q a fQ'.
[| (P, Q) : X; Q -a[]-> fQ' |]
==> EX fP'. P =a[]=> fP' & (ALL c. (fP' c, fQ' c) : X Un bisim);
!!P Q Q'.
[| (P, Q) : X; Q -tau-> Q' |]
==> EX P' P'' Q''. P =eps=> P' & (P', Q') : X Un bisim |]
==> P .= Q```

theorem RstrIdD1:

`  (P, Q) : RstrId ==> P = Q`

theorem RstrIdI:

`  rstr P ==> (P, P) : RstrId`

theorem bisim_refl:

`  rstr P ==> P .= P`