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  (⦇νyR, R)  Rel"
  and     "Id  Rel"

  shows "⦇νx(P  Q) ↝[Rel] P  ⦇νxQ"
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, ⦇νyR)  Rel"
  and     "Id  Rel"

  shows "P  ⦇νxQ ↝[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  ⦇νyT)  Rel"

  shows "⦇νx(P  Q) ↝[Rel] P  ⦇νxQ"
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  ⦇νyT, ⦇νy(R  T))  Rel"

  shows "P  ⦇νxQ ↝[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] (α.(⦇νxP))"
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 "α.(⦇νxP) ↝[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(⦇νyQ), ⦇νy(⦇νxQ))  Rel"

  shows "⦇νx(⦇νyP) ↝[Rel] ⦇νy(⦇νxP)"
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