Quelle  Strong_Sim_SC.thy

(* 
   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)0 ↝[Rel] 0"
by(auto simp add: simulation_def)

lemma resNilRight:
  fixes x :: name

  shows "0 ↝[Rel] (νx)0"
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 ⊕ 0 ↝[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 ⊕ 0"
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 ∥ 0, Q) ∈ Rel"

  shows "P ∥ 0 ↝[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 ∥ 0) ∈ Rel"

  shows "P ↝[Rel] P ∥ 0"
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