Kind name,action,proc type.
Import "ccs_core".
Define bisim_t : proc -> proc -> proc -> proc -> prop by
bisim_t P1 P2 Q1 Q2 :=
bisim_up_to refl_t P1 P2 /\ bisim_up_to refl_t Q1 Q2.
Define is_sound_fst : (proc -> proc -> proc -> proc -> prop) -> prop by
is_sound_fst Tech := forall P Q,
(exists R S, bisim_up_to refl_t P R /\ bisim_up_to Tech R S /\ bisim_up_to refl_t S Q)
-> bisim_up_to refl_t P Q.
Define is_sound_snd : (proc -> proc -> proc -> proc -> prop) -> prop by
is_sound_snd Tech := forall P Q, bisim_up_to Tech P Q ->
exists R S, bisim_up_to refl_t P R /\ bisim_up_to Tech R S /\ bisim_up_to refl_t S Q.
Theorem bisim_t_reflexive : forall P, bisim_t P P P P.
intros. unfold. backchain bisim_reflexive_. backchain bisim_reflexive_.
Theorem bisim_sound_fst : is_sound_fst bisim_t.
unfold. coinduction. intros. case H1.
rename H2 to Left. rename H3 to Middle. rename H4 to Right.
unfold.
intros Pstep.
Left : case Left. clear Left1. Left : apply Left to Pstep. clear Left. rename Left1 to PPstep.
Middle : case Middle. clear Middle1. Middle : apply Middle to PPstep. clear Middle. rename Middle1 to QQstep.
Right : case Right. clear Right1. Right : apply Right to QQstep. clear Right. rename Right1 to Qstep.
witness Q5. split. search.
witness P1. witness Q5. split. search.
case Left2. case Right2.
Bisim : case Middle2.
Link : apply bisim_transitive_ to Left3 Bisim.
Link : apply bisim_symmetric_ to Bisim1.
Link : apply bisim_transitive_ to Link1 Right3.
backchain 1 CH.
intros Qstep.
Right : case Right. Right : apply Right1 to Qstep. clear Right Right1. rename Right2 to Pstep.
Middle : case Middle. Middle : apply Middle1 to Pstep. clear Middle Middle1. rename Middle2 to PPstep.
Left : case Left. Left : apply Left1 to PPstep. clear Left Left1. rename Left2 to QQstep.
witness P5. split. search.
witness P5. witness Q1. split. search.
case Left3. case Right3.
Link : case Middle3.
Link : apply bisim_transitive_ to Left4 Link.
Link : apply bisim_symmetric_ to Link1.
Link : apply bisim_transitive_ to Link3 Right4.
backchain 1 CH.
Theorem bisim_sound_snd : is_sound_snd bisim_t.
unfold. intros.
witness P. witness Q. split.
backchain bisim_reflexive_.
search.
backchain bisim_reflexive_.
Theorem bisim_sound : is_sound bisim_t.
unfold. intros.
apply bisim_sound_snd. case H2. apply H3 to H1.
apply bisim_sound_fst. case H7. backchain H8.
