# File Bisimilarity.ML

```val [p0,p1,p2,p3,p4,p5,p6,p7,p8] = Goal "[| (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";
by (cut_facts_tac [p0] 1);
by (res_inst_tac [("X", "X")] bisim.coinduct 1);
by (atac 1);
by (Clarify_tac 1);
by (res_inst_tac [("x", "a")] exI 1);
by (res_inst_tac [("x", "b")] exI 1);
by (rtac conjI 1);
by (Simp_tac 1);
(* free output of first process *)
by (rtac conjI 1);
by (Clarify_tac 1);
by (dres_inst_tac [("P", "a")] p1 1);
by (atac 1);
by (Force_tac 1);
(* bound output of first process *)
by (rtac conjI 1);
by (Clarify_tac 1);
by (dres_inst_tac [("P", "a")] p2 1);
by (atac 1);
by (Force_tac 1);
(* input of first process *)
by (rtac conjI 1);
by (Clarify_tac 1);
by (dres_inst_tac [("P", "a")] p3 1);
by (atac 1);
by (Force_tac 1);
(* silent step of first process *)
by (rtac conjI 1);
by (Clarify_tac 1);
by (dres_inst_tac [("P", "a")] p4 1);
by (atac 1);
by (Force_tac 1);
(* free output of second process *)
by (rtac conjI 1);
by (Clarify_tac 1);
by (dres_inst_tac [("P", "a")] p5 1);
by (atac 1);
by (Force_tac 1);
(* bound output of second process *)
by (rtac conjI 1);
by (Clarify_tac 1);
by (dres_inst_tac [("P", "a")] p6 1);
by (atac 1);
by (Force_tac 1);
(* input of second process *)
by (rtac conjI 1);
by (Clarify_tac 1);
by (dres_inst_tac [("P", "a")] p7 1);
by (atac 1);
by (Force_tac 1);
(* silent step of second process *)
by (Clarify_tac 1);
by (dres_inst_tac [("P", "a")] p8 1);
by (atac 1);
by (Force_tac 1);
qed "bisimI";

val [p0,p1,p2,p3,p4,p5,p6,p7,p8] = Goal "[| (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";
by (cut_facts_tac [p0] 1);
by (res_inst_tac [("X", "X")] bisimI 1);
by (atac 1);
(* free output of first process *)
by (dres_inst_tac [("P", "Pa")] p1 1);
by (atac 1);
by (fast_tac (claset() addIs [PiCon.refl,AxExp.con] @ StTrans_rstr2 @ WkTrans_rstr2) 1);
(* bound output of first process *)
by (dres_inst_tac [("P", "Pa")] p2 1);
by (atac 1);
@ StTrans_rstr2 @ WkTrans_rstr2) 1);
(* input of first process *)
by (dres_inst_tac [("P", "Pa")] p3 1);
by (atac 1);
@ StTrans_rstr2 @ WkTrans_rstr2) 1);
(* silent step of first process *)
by (dres_inst_tac [("P", "Pa")] p4 1);
by (atac 1);
by (fast_tac (claset() addIs [PiCon.refl,AxExp.con] @ StTrans_rstr2 @ WkTrans_rstr2) 1);
(* free output of second process *)
by (dres_inst_tac [("P", "Pa")] p5 1);
by (atac 1);
by (fast_tac (claset() addIs [PiCon.refl,AxExp.con] @ StTrans_rstr2 @ WkTrans_rstr2) 1);
(* bound output of first process *)
by (dres_inst_tac [("P", "Pa")] p6 1);
by (atac 1);
@ StTrans_rstr2 @ WkTrans_rstr2) 1);
(* input of first process *)
by (dres_inst_tac [("P", "Pa")] p7 1);
by (atac 1);
@ StTrans_rstr2 @ WkTrans_rstr2) 1);
(* silent step of first process *)
by (dres_inst_tac [("P", "Pa")] p8 1);
by (atac 1);
by (fast_tac (claset() addIs [PiCon.refl,AxExp.con] @ StTrans_rstr2 @ WkTrans_rstr2) 1);
qed "plain_bisimI";

Goal "(P, Q) : RstrId ==> P = Q";
by (asm_full_simp_tac (simpset() addsimps [RstrId_def]) 1);
qed "RstrIdD1";

Goal "rstr P ==> (P, P) : RstrId";
by (asm_simp_tac (simpset() addsimps [RstrId_def]) 1);
qed "RstrIdI";

Goal "rstr P ==> P .= P";
by (res_inst_tac [("X", "RstrId")] plain_bisimI 1);