Theory Weak_Sim_Pres

(* 
   Title: The Calculus of Communicating Systems   
   Author/Maintainer: Jesper Bengtson (jebe@itu.dk), 2012
*)
theory Weak_Sim_Pres
  imports Weak_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) ↝⇧^<Rel> α.(Q)"
using assms
by(fastforce simp add: weakSimulation_def elim: actCases intro: weakAction)

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

  assumes "P ↝⇧^<Rel> Q"
  and     "Rel ⊆ Rel'"
  and     "Id ⊆ Rel'"
  and     C1: "⋀S T U. (S, T) ∈ Rel ⟹ (S ⊕ U, T) ∈ Rel'"

  shows "P ⊕ R ↝⇧^<Rel'> Q ⊕ R"
proof(induct rule: weakSimI)
  case(Sim α QR)
  from ‹Q ⊕ R ⟼α ≺ QR› show ?case
  proof(induct rule: sumCases)
    case(cSum1 Q')
    from ‹P ↝⇧^<Rel> Q› ‹Q ⟼α ≺ Q'› 
    obtain P' where "P ⟹⇧^α ≺ P'" and "(P', Q') ∈ Rel"
      by(blast dest: weakSimE)
    thus ?case
    proof(induct rule: weakTransCases)
      case Base
      have "P ⊕ R ⟹⇧^τ ≺ P ⊕ R" by simp
      moreover from ‹(P, Q') ∈ Rel› have "(P ⊕ R, Q') ∈ Rel'" by(rule C1)
      ultimately show ?case by blast
    next
      case Step
      from ‹P ⟹α ≺ P'› have "P ⊕ R ⟹α ≺ P'" by(rule weakCongSum1)
      hence "P ⊕ R ⟹⇧^α ≺ P'" by(simp add: weakTrans_def)
      thus ?case using ‹(P', Q') ∈ Rel› ‹Rel ⊆ Rel'› by blast
    qed
  next
    case(cSum2 R')
    from ‹R ⟼α ≺ R'› have "R ⟹α ≺ R'" by(rule transitionWeakCongTransition)
    hence "P ⊕ R ⟹α ≺ R'" by(rule weakCongSum2)
    hence "P ⊕ R ⟹⇧^α ≺ R'" by(simp add: weakTrans_def)
    thus ?case using ‹Id ⊆ Rel'› by blast
  qed
qed

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

  assumes "P ↝⇧^<Rel> Q"
  and     "(P, Q) ∈ Rel"
  and     "R ↝⇧^<Rel'> T"
  and     "(R, T) ∈ Rel'"
  and     C1: "⋀P' Q' R' T'. ⟦(P', Q') ∈ Rel; (R', T') ∈ Rel'⟧ ⟹ (P' ∥ R', Q' ∥ T') ∈ Rel''"

  shows "P ∥ R ↝⇧^<Rel''> Q ∥ T"
proof(induct rule: weakSimI)
  case(Sim α QT)
  from ‹Q ∥ T ⟼α ≺ QT›
  show ?case
  proof(induct rule: parCases)
    case(cPar1 Q')
    from ‹P ↝⇧^<Rel> Q› ‹Q ⟼α ≺ Q'› obtain P' where "P ⟹⇧^α ≺ P'" and "(P', Q') ∈ Rel" 
      by(rule weakSimE)
    from ‹P ⟹⇧^α ≺ P'› have "P ∥ R ⟹⇧^α ≺ P' ∥ R" by(rule weakPar1)
    moreover from ‹(P', Q') ∈ Rel› ‹(R, T) ∈ Rel'› have "(P' ∥ R, Q' ∥ T) ∈ Rel''" by(rule C1)
    ultimately show ?case by blast
  next
    case(cPar2 T')
    from ‹R ↝⇧^<Rel'> T› ‹T ⟼α ≺ T'› obtain R' where "R ⟹⇧^α ≺ R'" and "(R', T') ∈ Rel'" 
      by(rule weakSimE)
    from ‹R ⟹⇧^α ≺ R'› have "P ∥ R ⟹⇧^α ≺ P ∥ R'" by(rule weakPar2)
    moreover from ‹(P, Q) ∈ Rel› ‹(R', T') ∈ Rel'› have "(P ∥ R', Q ∥ T') ∈ Rel''" by(rule C1)
    ultimately show ?case by blast
  next
    case(cComm Q' T' α)
    from ‹P ↝⇧^<Rel> Q› ‹Q ⟼α ≺ Q'› obtain P' where "P ⟹⇧^α ≺ P'" and "(P', Q') ∈ Rel" 
      by(rule weakSimE)
    from ‹R ↝⇧^<Rel'> T› ‹T ⟼(coAction α) ≺ T'› obtain R' where "R ⟹⇧^(coAction α) ≺ R'" and "(R', T') ∈ Rel'" 
      by(rule weakSimE)
    from ‹P ⟹⇧^α ≺ P'› ‹R ⟹⇧^(coAction α) ≺ R'› ‹α ≠ τ› have "P ∥ R ⟹τ ≺ P' ∥ R'" 
      by(auto intro: weakCongSync simp add: weakTrans_def)
    hence "P ∥ R ⟹⇧^τ ≺ P' ∥ R'" by(simp add: weakTrans_def)
    moreover from ‹(P', Q') ∈ Rel› ‹(R', T') ∈ Rel'› have "(P' ∥ R', Q' ∥ T') ∈ Rel''" by(rule C1)
    ultimately show ?case by blast
  qed
qed

lemma parPres:
  fixes P    :: ccs
  and   Q    :: ccs
  and   R    :: ccs
  and   Rel  :: "(ccs × ccs) set"
  and   Rel' :: "(ccs × ccs) set"
  assumes "P ↝⇧^<Rel> Q"
  and     "(P, Q) ∈ Rel"
  and     C1: "⋀S T U. (S, T) ∈ Rel ⟹ (S ∥ U, T ∥ U) ∈ Rel'"

  shows "P ∥ R ↝⇧^<Rel'> Q ∥ R"
using assms
by(rule_tac parPresAux[where Rel'=Id and Rel''=Rel']) (auto intro: reflexive)

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

  assumes "P ↝⇧^<Rel> Q"
  and     "⋀R S y. (R, S) ∈ Rel ⟹ (⦇νy⦈R, ⦇νy⦈S) ∈ Rel'"

  shows "⦇νx⦈P ↝⇧^<Rel'> ⦇νx⦈Q"
using assms
by(fastforce simp add: weakSimulation_def elim: resCases intro: weakRes)

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 ↝⇧^<Rel> S"
  and     Par: "⋀R S T U. ⟦(R, S) ∈ Rel; (T, U) ∈ Rel'⟧ ⟹ (R ∥ T, S ∥ U) ∈ Rel'"
  and     C2: "bangRel Rel ⊆ Rel'"
  and     C3: "⋀R S. (R ∥ !R, S) ∈ Rel' ⟹ (!R, S) ∈ Rel'"

  shows "!P ↝⇧^<Rel'> !Q"
proof(induct rule: weakSimI)
  case(Sim α Q')
  {
    fix Pa α Q'
    assume "!Q ⟼α ≺ Q'" and "(Pa, !Q) ∈ bangRel Rel"
    hence "∃P'. Pa ⟹⇧^α ≺ P' ∧ (P', Q') ∈ Rel'"
    proof(nominal_induct arbitrary: Pa rule: bangInduct)
      case(cPar1 α Q')
      from ‹(Pa, Q ∥ !Q) ∈ bangRel Rel› 
      show ?case
      proof(induct rule: BRParCases)
        case(BRPar P R)
        from ‹(P, Q) ∈ Rel› have "P ↝⇧^<Rel> Q" by(rule C1)
        with ‹Q ⟼α ≺ Q'› obtain P' where "P ⟹⇧^α ≺ P'" and "(P', Q') ∈ Rel"
          by(blast dest: weakSimE)
        from ‹P ⟹⇧^α ≺ P'› have "P ∥ R ⟹⇧^α ≺ P' ∥ R" by(rule weakPar1)
        moreover from ‹(P', Q') ∈ Rel› ‹(R, !Q) ∈ bangRel Rel› C2 have "(P' ∥ R, Q' ∥ !Q) ∈ Rel'"
          by(blast intro: Par)
        ultimately show ?case by blast
      qed
    next
      case(cPar2 α Q')
      from ‹(Pa, Q ∥ !Q) ∈ bangRel Rel›
      show ?case
      proof(induct rule: BRParCases)
        case(BRPar P R)
        from ‹(R, !Q) ∈ bangRel Rel› obtain R' where "R ⟹⇧^α ≺ R'" and "(R', Q') ∈ Rel'" using cPar2
          by blast
        from ‹R ⟹⇧^α ≺ R'› have "P ∥ R ⟹⇧^α ≺ P ∥ R'" by(rule weakPar2)
        moreover from ‹(P, Q) ∈ Rel› ‹(R', Q') ∈ Rel'› have "(P ∥ R', Q ∥ Q') ∈ Rel'" by(rule Par)
        ultimately show ?case by blast
      qed
    next
      case(cComm a Q' Q'' Pa)
      from ‹(Pa, Q ∥ !Q) ∈ bangRel Rel›
      show ?case
      proof(induct rule: BRParCases)
        case(BRPar P R)
        from ‹(P, Q) ∈ Rel› have "P ↝⇧^<Rel> Q" by(rule C1)
        with ‹Q ⟼a ≺ Q'› obtain P' where "P ⟹⇧^a ≺ P'" and "(P', Q') ∈ Rel"
          by(blast dest: weakSimE)
        from ‹(R, !Q) ∈ bangRel Rel› obtain R' where "R ⟹⇧^(coAction a) ≺ R'" and "(R', Q'') ∈ Rel'" using cComm
          by blast
        from ‹P ⟹⇧^a ≺ P'› ‹R ⟹⇧^(coAction a) ≺ R'› ‹a ≠ τ› have "P ∥ R ⟹⇧^τ ≺ P' ∥ R'"
          by(auto intro: weakCongSync simp add: weakTrans_def)
        moreover from ‹(P', Q') ∈ Rel› ‹(R', Q'') ∈ Rel'› have "(P' ∥ R', Q' ∥ Q'') ∈ Rel'" by(rule Par)
        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 ∥ !P, Q ∥ !Q) ∈ bangRel Rel" by(rule bangRel.BRPar)
        then obtain P' where "P ∥ !P ⟹⇧^α ≺ P'" and "(P', Q') ∈ Rel'" using cBang
          by blast
        from ‹P ∥ !P ⟹⇧^α ≺ P'› 
        show ?case
        proof(induct rule: weakTransCases)
          case Base
          have "!P ⟹⇧^τ ≺ !P" by simp
          moreover from ‹(P', Q') ∈ Rel'› ‹P ∥ !P = P'› have "(!P, Q') ∈ Rel'" by(blast intro: C3)
          ultimately show ?case by blast
        next
          case Step
          from ‹P ∥ !P ⟹α ≺ P'› have "!P ⟹α ≺ P'" by(rule weakCongRepl)
          hence "!P ⟹⇧^α ≺ P'" by(simp add: weakTrans_def)
          with ‹(P', Q') ∈ Rel'› show ?case by blast
        qed
      qed
    qed
  }

  moreover from ‹(P, Q) ∈ Rel› have "(!P, !Q) ∈ bangRel Rel" by(rule BRBang) 
  ultimately show ?case using ‹!Q ⟼ α ≺ Q'› by blast
qed

end