Reasoning

[View ccs_ctx.thm]

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]

%%% Substitutivity

Define inv : proc -> proc -> prop by
  inv P Q := bisim_up_to refl_t P Q
; inv (par P1 Q1) (par P2 Q2) := inv P1 P2 /\ inv Q1 Q2.

Define bisim_inv : proc -> proc -> prop by
   bisim_inv P Q :=
      (forall A P1, one P A P1 ->
         exists Q1, one Q A Q1 /\
           inv P1 Q1)
   /\ (forall A Q1, one Q A Q1 ->
         exists P1, one P A P1 /\
           inv P1 Q1).

Theorem inv_bisim_inv : forall P Q, inv P Q -> bisim_inv P Q.

Theorem bisim_inv_bisim : forall P Q, bisim_inv P Q -> bisim_up_to refl_t P Q.

Theorem bisim_par_subst_1 : forall P Q R,
  bisim_up_to refl_t P Q -> bisim_up_to refl_t (par P R) (par Q R).

Theorem bisim_par_subst_2 : forall P Q R,
  bisim_up_to refl_t P Q -> bisim_up_to refl_t (par R P) (par R Q).

Theorem bisim_plus_subst_1 : forall P Q R,
  bisim_up_to refl_t P Q -> bisim_up_to refl_t (plus P R) (plus Q R).

Theorem bisim_plus_subst_2 : forall P Q R,
  bisim_up_to refl_t P Q -> bisim_up_to refl_t (plus R P) (plus R Q).

Theorem bisim_act_subst : forall P Q A,
  bisim_up_to refl_t P Q -> bisim_up_to refl_t (act A P) (act A Q).

%%% Process contexts

Kind ctx type.

Type hole           ctx.
Type plus_l,par_l   ctx -> proc -> ctx.
Type plus_r,par_r   proc -> ctx -> ctx.
Type act_d          action -> ctx -> ctx.

%%% at C P Q   means  C[P] = Q.
Define at : ctx -> proc -> proc -> prop by
  at hole P P
; at (plus_l C R) P (plus Q R) := at C P Q
; at (plus_r R C) P (plus R Q) := at C P Q
; at (par_l C R) P (par Q R) := at C P Q
; at (par_r R C) P (par R Q) := at C P Q
; at (act_d A C) P (act A Q) := at C P Q.

Define substitutive_rel : (proc -> proc -> prop) -> prop by
  substitutive_rel Rel :=
    forall P1 P2 C Q1 Q2,
      at C P1 Q1 -> at C P2 Q2 ->
      Rel P1 P2 -> Rel Q1 Q2.

Theorem bisim_substitutive : substitutive_rel (bisim_up_to refl_t).

Theorem at_det3 : forall C P Q1 Q2,
  at C P Q1 -> at C P Q2 -> Q1 = Q2.

Theorem at_det2 : forall C P1 P2 Q,
  at C P1 Q -> at C P2 Q -> P1 = P2.

%%% Context concatenation

Theorem concat_ctx : forall C1 P1 C2 P2 P3,
  at C1 P1 P2 -> at C2 P2 P3 -> exists C3, at C3 P1 P3.

%%% Faithful contexts

Theorem ctx_faithful : forall C P P0 A R,
  at C P P0 -> one P0 A R ->
     (exists CC, at CC P R /\
        (forall Q Q0, at C Q Q0 -> exists RR, one Q0 A RR /\ at CC Q RR))
  \/ (exists CC PBP B, one P B PBP /\ at CC PBP R /\
        (forall Q QBQ, one Q B QBQ ->
          (forall Q0, at C Q Q0 -> exists RR, one Q0 A RR /\ at CC QBQ RR)))
  \/ (forall Q Q0, at C Q Q0 -> one Q0 A R).
induction on 1. intros. case H1 (keep). % empty context left. right. witness hole. witness R. witness A. split. search. search. intros. case H4. witness QBQ. search. % plus_l case H2. apply IH to H3 H4. case H5. left. left. witness CC. split. search. intros. case H8. apply H7 to H9. search. left. right. witness CC. witness PBP. witness B. split. search. search. intros. apply H8 to H9. case H10. apply H11 to H12. search. right. intros. case H7. apply H6 to H8. search. right. intros. case H5. search. % plus_r case H2. right. intros. case H5. search. apply IH to H3 H4. case H5. left. left. witness CC. split. search. intros. case H8. apply H7 to H9. search. left. right. witness CC. witness PBP. witness B. split. search. search. intros. apply H8 to H9. case H10. apply H11 to H12. search. right. intros. case H7. apply H6 to H8. search. % par_l case H2. apply IH to H3 H4. case H5. left. left. witness par_l CC R1. split. search. intros. case H8. apply H7 to H9. witness par RR R1. search. left. right. witness par_l CC R1. witness PBP. witness B. split. search. search. intros. case H10. apply H8 to H9. apply H12 to H11. witness par RR R1. search. right. intros. case H7. apply H6 to H8. search. left. left. witness par_l C1 Q2. split. search. intros. case H5. witness par Q3 Q2. search. apply IH to H3 H4. case H6. left. left. witness par_l CC Q2. split. search. intros. case H9. apply H8 to H10. witness par RR Q2. search. left. right. witness par_l CC Q2. witness PBP. witness B. split. search. search. intros. case H11. apply H9 to H10. apply H13 to H12. witness par RR Q2. search. right. intros. case H8. apply H7 to H9. search. apply IH to H3 H4. case H6. left. left. witness par_l CC Q2. split. search. intros. case H9. apply H8 to H10. witness par RR Q2. search. left. right. witness par_l CC Q2. witness PBP. witness B. split. search. search. intros. case H11. apply H9 to H10. apply H13 to H12. witness par RR Q2. search. right. intros. case H8. apply H7 to H9. search. % par_r case H2. left. left. witness par_r P2 C1. split. search. intros. case H5. witness par P2 Q2. search. apply IH to H3 H4. case H5. left. left. witness par_r R1 CC. split. search. intros. case H8. apply H7 to H9. witness par R1 RR. search. left. right. witness par_r R1 CC. witness PBP. witness B. split. search. search. intros. case H10. apply H8 to H9. apply H12 to H11. search. right. intros. case H7. apply H6 to H8. search. apply IH to H3 H5. case H6. left. left. witness par_r P2 CC. split. search. intros. case H9. apply H8 to H10. search. left. right. witness par_r P2 CC. witness PBP. witness B. split. search. search. intros. case H11. apply H9 to H10. apply H13 to H12. search. right. intros. case H8. apply H7 to H9. search. apply IH to H3 H5. case H6. left. left. witness par_r P2 CC. split. search. intros. case H9. apply H8 to H10. search. left. right. witness par_r P2 CC. witness PBP. witness B. split. search. search. intros. case H11. apply H9 to H10. apply H13 to H12. search. right. intros. case H8. apply H7 to H9. search. % act_d case H2. left. left. witness C1. split. search. intros. case H4. search.