Theory Strong_Sim_Pres

(* 
   Title: The Calculus of Communicating Systems   
   Author/Maintainer: Jesper Bengtson (jebe@itu.dk), 2012
*)
theory Strong_Sim_Pres
  imports Strong_Sim
begin

lemma actPres:
  fixes P    :: ccs
  and   Q    :: ccs
  and   Rel  :: "(ccs × ccs) set"
  and   a    :: name
  and   Rel' :: "(ccs × ccs) set"

  assumes "(P, Q) ∈ Rel"

  shows "α.(P) \<leadsto>[Rel] α.(Q)"
using assms
by(fastsimp simp add: simulation_def elim: actCases intro: Action)

lemma sumPres:
  fixes P   :: ccs
  and   Q   :: ccs
  and   Rel :: "(ccs × ccs) set"

  assumes "P \<leadsto>[Rel] Q"
  and     "Rel ⊆ Rel'"
  and     "Id ⊆ Rel'"

  shows "P ⊕ R \<leadsto>[Rel'] Q ⊕ R"
using assms
by(force simp add: simulation_def elim: sumCases intro: Sum1 Sum2)

lemma parPresAux:
  fixes P   :: ccs
  and   Q   :: ccs
  and   Rel :: "(ccs × ccs) set"

  assumes "P \<leadsto>[Rel] Q"
  and     "(P, Q) ∈ Rel"
  and     "R \<leadsto>[Rel'] T"
  and     "(R, T) ∈ Rel'"
  and     C1: "!!P' Q' R' T'. [|(P', Q') ∈ Rel; (R', T') ∈ Rel'|] ==> (P' \<parallel> R', Q' \<parallel> T') ∈ Rel''"

  shows "P \<parallel> R \<leadsto>[Rel''] Q \<parallel> T"
proof(induct rule: simI)
  case(Sim a QT)
  from `Q \<parallel> T \<longmapsto>a \<prec> QT`
  show ?case
  proof(induct rule: parCases)
    case(cPar1 Q')
    from `P \<leadsto>[Rel] Q` `Q \<longmapsto>a \<prec> Q'` obtain P' where "P \<longmapsto>a \<prec> P'" and "(P', Q') ∈ Rel" 
      by(rule simE)
    from `P \<longmapsto>a \<prec> P'` have "P \<parallel> R \<longmapsto>a \<prec> P' \<parallel> R" by(rule Par1)
    moreover from `(P', Q') ∈ Rel` `(R, T) ∈ Rel'` have "(P' \<parallel> R, Q' \<parallel> T) ∈ Rel''" by(rule C1)
    ultimately show ?case by blast
  next
    case(cPar2 T')
    from `R \<leadsto>[Rel'] T` `T \<longmapsto>a \<prec> T'` obtain R' where "R \<longmapsto>a \<prec> R'" and "(R', T') ∈ Rel'" 
      by(rule simE)
    from `R \<longmapsto>a \<prec> R'` have "P \<parallel> R \<longmapsto>a \<prec> P \<parallel> R'" by(rule Par2)
    moreover from `(P, Q) ∈ Rel` `(R', T') ∈ Rel'` have "(P \<parallel> R', Q \<parallel> T') ∈ Rel''" by(rule C1)
    ultimately show ?case by blast
  next
    case(cComm Q' T' a)
    from `P \<leadsto>[Rel] Q` `Q \<longmapsto>a \<prec> Q'` obtain P' where "P \<longmapsto>a \<prec> P'" and "(P', Q') ∈ Rel" 
      by(rule simE)
    from `R \<leadsto>[Rel'] T` `T \<longmapsto>(coAction a) \<prec> T'` obtain R' where "R \<longmapsto>(coAction a) \<prec> R'" and "(R', T') ∈ Rel'" 
      by(rule simE)
    from `P \<longmapsto>a \<prec> P'` `R \<longmapsto>(coAction a) \<prec> R'` `a ≠ τ` have "P \<parallel> R \<longmapsto>τ \<prec> P' \<parallel> R'" by(rule Comm)
    moreover from `(P', Q') ∈ Rel` `(R', T') ∈ Rel'` have "(P' \<parallel> R', Q' \<parallel> T') ∈ Rel''" by(rule C1)
    ultimately show ?case by blast
  qed
qed

lemma parPres:
  fixes P   :: ccs
  and   Q   :: ccs
  and   Rel :: "(ccs × ccs) set"

  assumes "P \<leadsto>[Rel] Q"
  and     "(P, Q) ∈ Rel"
  and     C1: "!!S T U. (S, T) ∈ Rel ==> (S \<parallel> U, T \<parallel> U) ∈ Rel'"

  shows "P \<parallel> R \<leadsto>[Rel'] Q \<parallel> R"
using assms
by(rule_tac parPresAux[where Rel''=Rel' and Rel'=Id]) (auto intro: reflexive)

lemma resPres:
  fixes P   :: ccs
  and   Rel :: "(ccs × ccs) set"
  and   Q   :: ccs
  and   x   :: name

  assumes "P \<leadsto>[Rel] Q"
  and     "!!R S y. (R, S) ∈ Rel ==> ((|νy|)),R, (|νy|)),S) ∈ Rel'"

  shows "(|νx|)),P \<leadsto>[Rel'] (|νx|)),Q"
using assms
by(fastsimp simp add: simulation_def elim: resCases intro: Res)

lemma bangPres:
  fixes P   :: ccs
  and   Rel :: "(ccs × ccs) set"
  and   Q   :: ccs

  assumes "(P, Q) ∈ Rel"
  and     C1: "!!R S. (R, S) ∈ Rel ==> R \<leadsto>[Rel] S"

  shows "!P \<leadsto>[bangRel Rel] !Q"
proof(induct rule: simI)
  case(Sim α Q')
  {
    fix Pa α Q'
    assume "!Q \<longmapsto>α \<prec> Q'" and "(Pa, !Q) ∈ bangRel Rel"
    hence "∃P'. Pa \<longmapsto>α \<prec> P' ∧ (P', Q') ∈ bangRel Rel"
    proof(nominal_induct arbitrary: Pa rule: bangInduct)
      case(cPar1 α Q')
      from `(Pa, Q \<parallel> !Q) ∈ bangRel Rel` 
      show ?case
      proof(induct rule: BRParCases)
        case(BRPar P R)
        from `(P, Q) ∈ Rel` have "P \<leadsto>[Rel] Q" by(rule C1)
        with `Q \<longmapsto>α \<prec> Q'` obtain P' where "P \<longmapsto>α \<prec> P'" and "(P', Q') ∈ Rel"
          by(blast dest: simE)
        from `P \<longmapsto>α \<prec> P'` have "P \<parallel> R \<longmapsto>α \<prec> P' \<parallel> R" by(rule Par1)
        moreover from `(P', Q') ∈ Rel` `(R, !Q) ∈ bangRel Rel` have "(P' \<parallel> R, Q' \<parallel> !Q) ∈ bangRel Rel"
          by(rule bangRel.BRPar)
        ultimately show ?case by blast
      qed
    next
      case(cPar2 α Q')
      from `(Pa, Q \<parallel> !Q) ∈ bangRel Rel`
      show ?case
      proof(induct rule: BRParCases)
        case(BRPar P R)
        from `(R, !Q) ∈ bangRel Rel` obtain R' where "R \<longmapsto>α \<prec> R'" and "(R', Q') ∈ bangRel Rel" using cPar2
          by blast
        from `R \<longmapsto>α \<prec> R'` have "P \<parallel> R \<longmapsto>α \<prec> P \<parallel> R'" by(rule Par2)
        moreover from `(P, Q) ∈ Rel` `(R', Q') ∈ bangRel Rel` have "(P \<parallel> R', Q \<parallel> Q') ∈ bangRel Rel" by(rule bangRel.BRPar)
        ultimately show ?case by blast
      qed
    next
      case(cComm a Q' Q'' Pa)
      from `(Pa, Q \<parallel> !Q) ∈ bangRel Rel`
      show ?case
      proof(induct rule: BRParCases)
        case(BRPar P R)
        from `(P, Q) ∈ Rel` have "P \<leadsto>[Rel] Q" by(rule C1)
        with `Q \<longmapsto>a \<prec> Q'` obtain P' where "P \<longmapsto>a \<prec> P'" and "(P', Q') ∈ Rel"
          by(blast dest: simE)
        from `(R, !Q) ∈ bangRel Rel` obtain R' where "R \<longmapsto>(coAction a) \<prec> R'" and "(R', Q'') ∈ bangRel Rel" using cComm
          by blast
        from `P \<longmapsto>a \<prec> P'` `R \<longmapsto>(coAction a) \<prec> R'` `a ≠ τ` have "P \<parallel> R \<longmapsto>τ \<prec> P' \<parallel> R'" by(rule Comm)
        moreover from `(P', Q') ∈ Rel` `(R', Q'') ∈ bangRel Rel` have "(P' \<parallel> R', Q' \<parallel> Q'') ∈ bangRel Rel" by(rule bangRel.BRPar)
        ultimately show ?case by blast
      qed
    next
      case(cBang α Q' Pa)
      from `(Pa, !Q) ∈ bangRel Rel`
      show ?case
      proof(induct rule: BRBangCases)
        case(BRBang P)
        from `(P, Q) ∈ Rel` have "(!P, !Q) ∈ bangRel Rel" by(rule bangRel.BRBang)
        with `(P, Q) ∈ Rel` have "(P \<parallel> !P, Q \<parallel> !Q) ∈ bangRel Rel" by(rule bangRel.BRPar)
        then obtain P' where "P \<parallel> !P \<longmapsto>α \<prec> P'" and "(P', Q') ∈ bangRel Rel" using cBang
          by blast
        from `P \<parallel> !P \<longmapsto>α \<prec> P'` have "!P \<longmapsto>α \<prec> P'" by(rule Bang)
        thus ?case using `(P', Q') ∈ bangRel Rel` by blast
      qed
    qed
  }

  moreover from `(P, Q) ∈ Rel` have "(!P, !Q) ∈ bangRel Rel" by(rule BRBang) 
  ultimately show ?case using `!Q \<longmapsto> α \<prec> Q'` by blast
qed

end