Click on a command or tactic to see a detailed view of its use.

Kind name,action,proc type.

Import "ccs_core". [View 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 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 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.