Theory Strong_Sim_SC

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

lemma resNilLeft:
  fixes x :: name

  shows "⦇νx⦈𝟬 ↝[Rel] 𝟬"
by(auto simp add: simulation_def)

lemma resNilRight:
  fixes x :: name

  shows "𝟬 ↝[Rel] ⦇νx⦈𝟬"
by(auto simp add: simulation_def elim: resCases)

lemma test[simp]:
  fixes x :: name
  and   P :: ccs

  shows "x ♯ [x].P"
by(auto simp add: abs_fresh)

lemma scopeExtSumLeft:
  fixes x :: name
  and   P :: ccs
  and   Q :: ccs

  assumes "x ♯ P"
  and     C1: "⋀y R. y ♯ R ⟹ (⦇νy⦈R, R) ∈ Rel"
  and     "Id ⊆ Rel"

  shows "⦇νx⦈(P ⊕ Q) ↝[Rel] P ⊕ ⦇νx⦈Q"
using assms
apply(auto simp add: simulation_def)
by(elim sumCases resCases) (blast intro: Res Sum1 Sum2 C1 dest: freshDerivative)+

lemma scopeExtSumRight:
  fixes x :: name
  and   P :: ccs
  and   Q :: ccs

  assumes "x ♯ P"
  and     C1: "⋀y R. y ♯ R ⟹ (R, ⦇νy⦈R) ∈ Rel"
  and     "Id ⊆ Rel"

  shows "P ⊕ ⦇νx⦈Q ↝[Rel] ⦇νx⦈(P ⊕ Q)"
using assms
apply(auto simp add: simulation_def)
by(elim sumCases resCases) (blast intro: Res Sum1 Sum2 C1 dest: freshDerivative)+

lemma scopeExtLeft:
  fixes x :: name
  and   P :: ccs
  and   Q :: ccs

  assumes "x ♯ P"
  and     C1: "⋀y R T. y ♯ R ⟹ (⦇νy⦈(R ∥ T), R ∥ ⦇νy⦈T) ∈ Rel"

  shows "⦇νx⦈(P ∥ Q) ↝[Rel] P ∥ ⦇νx⦈Q"
using assms
by(fastforce elim: parCases resCases intro: Res C1 Par1 Par2 Comm dest: freshDerivative simp add: simulation_def)

lemma scopeExtRight:
  fixes x :: name
  and   P :: ccs
  and   Q :: ccs

  assumes "x ♯ P"
  and     C1: "⋀y R T. y ♯ R ⟹ (R ∥ ⦇νy⦈T, ⦇νy⦈(R ∥ T)) ∈ Rel"

  shows "P ∥ ⦇νx⦈Q ↝[Rel] ⦇νx⦈(P ∥ Q)"
using assms
by(fastforce elim: parCases resCases intro: Res C1 Par1 Par2 Comm dest: freshDerivative simp add: simulation_def)

lemma sumComm:
  fixes P :: ccs
  and   Q :: ccs

  assumes "Id ⊆ Rel"

  shows "P ⊕ Q ↝[Rel] Q ⊕ P"
using assms
by(force simp add: simulation_def elim: sumCases intro: Sum1 Sum2)

lemma sumAssocLeft:
  fixes P :: ccs
  and   Q :: ccs
  and   R :: ccs

  assumes "Id ⊆ Rel"

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

lemma sumAssocRight:
  fixes P :: ccs
  and   Q :: ccs
  and   R :: ccs

  assumes "Id ⊆ Rel"

  shows " P ⊕ (Q ⊕ R) ↝[Rel] (P ⊕ Q) ⊕ R"
using assms
by(intro simI, elim sumCases) (blast intro: Sum1 Sum2)+

lemma sumIdLeft:
  fixes P   :: ccs
  and   Rel :: "(ccs × ccs) set"
  
  assumes "Id ⊆ Rel"

  shows "P ⊕ 𝟬 ↝[Rel] P"
using assms
by(auto simp add: simulation_def intro: Sum1)

lemma sumIdRight:
  fixes P   :: ccs
  and   Rel :: "(ccs × ccs) set"
  
  assumes "Id ⊆ Rel"

  shows "P ↝[Rel] P ⊕ 𝟬"
using assms
by(fastforce simp add: simulation_def elim: sumCases)

lemma parComm:
  fixes P :: ccs
  and   Q :: ccs

  assumes C1: "⋀R T. (R ∥ T, T ∥ R) ∈ Rel"

  shows "P ∥ Q ↝[Rel] Q ∥ P"
by(fastforce simp add: simulation_def elim: parCases intro: Par1 Par2 Comm C1)

lemma parAssocLeft:
  fixes P :: ccs
  and   Q :: ccs
  and   R :: ccs

  assumes C1: "⋀S T U. ((S ∥ T) ∥ U, S ∥ (T ∥ U)) ∈ Rel"

  shows "(P ∥ Q) ∥ R ↝[Rel] P ∥ (Q ∥ R)"
by(fastforce simp add: simulation_def elim: parCases intro: Par1 Par2 Comm C1)

lemma parAssocRight:
  fixes P :: ccs
  and   Q :: ccs
  and   R :: ccs

  assumes C1: "⋀S T U. (S ∥ (T ∥ U), (S ∥ T) ∥ U) ∈ Rel"

  shows "P ∥ (Q ∥ R) ↝[Rel] (P ∥ Q) ∥ R"
by(fastforce simp add: simulation_def elim: parCases intro: Par1 Par2 Comm C1)

lemma parIdLeft:
  fixes P   :: ccs
  and   Rel :: "(ccs × ccs) set"
  
  assumes "⋀Q. (Q ∥ 𝟬, Q) ∈ Rel"

  shows "P ∥ 𝟬 ↝[Rel] P"
using assms
by(auto simp add: simulation_def intro: Par1)

lemma parIdRight:
  fixes P   :: ccs
  and   Rel :: "(ccs × ccs) set"
  
  assumes "⋀Q. (Q, Q ∥ 𝟬) ∈ Rel"

  shows "P ↝[Rel] P ∥ 𝟬"
using assms
by(fastforce simp add: simulation_def elim: parCases)

declare fresh_atm[simp]

lemma resActLeft:
  fixes x :: name
  and   α :: act
  and   P :: ccs

  assumes "x ♯ α"
  and     "Id ⊆ Rel"

  shows "⦇νx⦈(α.(P)) ↝[Rel] (α.(⦇νx⦈P))"
using assms
by(fastforce simp add: simulation_def elim: actCases intro: Res Action) 

lemma resActRight:
  fixes x :: name
  and   α :: act
  and   P :: ccs

  assumes "x ♯ α"
  and     "Id ⊆ Rel"

  shows "α.(⦇νx⦈P) ↝[Rel] ⦇νx⦈(α.(P))"
using assms
by(fastforce simp add: simulation_def elim: resCases actCases intro: Action) 

lemma resComm:
  fixes x :: name
  and   y :: name 
  and   P :: ccs

  assumes "⋀Q. (⦇νx⦈(⦇νy⦈Q), ⦇νy⦈(⦇νx⦈Q)) ∈ Rel"

  shows "⦇νx⦈(⦇νy⦈P) ↝[Rel] ⦇νy⦈(⦇νx⦈P)"
using assms
by(fastforce simp add: simulation_def elim: resCases intro: Res)

inductive_cases bangCases[simplified ccs.distinct act.distinct]: "!P ⟼α ≺ P'"

lemma bangUnfoldLeft:
  fixes P :: ccs
  
  assumes "Id ⊆ Rel"

  shows "P ∥ !P ↝[Rel] !P"
using assms
by(fastforce simp add: simulation_def ccs.inject elim: bangCases)

lemma bangUnfoldRight:
  fixes P :: ccs
  
  assumes "Id ⊆ Rel"

  shows "!P ↝[Rel] P ∥ !P"
using assms
by(fastforce simp add: simulation_def ccs.inject intro: Bang)

end