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|)),\<zero> \<leadsto>[Rel] \<zero>"
by(auto simp add: simulation_def)

lemma resNilRight:
  fixes x :: name

  shows "\<zero> \<leadsto>[Rel] (|νx|)),\<zero>"
by(auto simp add: simulation_def elim: resCases)

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

  shows "x \<sharp> [x].P"
by(auto simp add: abs_fresh)

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

  assumes "x \<sharp> P"
  and     C1: "!!y R. y \<sharp> R ==> ((|νy|)),R, R) ∈ Rel"
  and     "Id ⊆ Rel"

  shows "(|νx|)),(P ⊕ Q) \<leadsto>[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 \<sharp> P"
  and     C1: "!!y R. y \<sharp> R ==> (R, (|νy|)),R) ∈ Rel"
  and     "Id ⊆ Rel"

  shows "P ⊕ (|νx|)),Q \<leadsto>[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 \<sharp> P"
  and     C1: "!!y R T. y \<sharp> R ==> ((|νy|)),(R \<parallel> T), R \<parallel> (|νy|)),T) ∈ Rel"

  shows "(|νx|)),(P \<parallel> Q) \<leadsto>[Rel] P \<parallel> (|νx|)),Q"
using assms
by(fastsimp 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 \<sharp> P"
  and     C1: "!!y R T. y \<sharp> R ==> (R \<parallel> (|νy|)),T, (|νy|)),(R \<parallel> T)) ∈ Rel"

  shows "P \<parallel> (|νx|)),Q \<leadsto>[Rel] (|νx|)),(P \<parallel> Q)"
using assms
by(fastsimp 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 \<leadsto>[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 \<leadsto>[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) \<leadsto>[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 ⊕ \<zero> \<leadsto>[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 \<leadsto>[Rel] P ⊕ \<zero>"
using assms
by(fastsimp simp add: simulation_def elim: sumCases)

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

  assumes C1: "!!R T. (R \<parallel> T, T \<parallel> R) ∈ Rel"

  shows "P \<parallel> Q \<leadsto>[Rel] Q \<parallel> P"
by(fastsimp 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 \<parallel> T) \<parallel> U, S \<parallel> (T \<parallel> U)) ∈ Rel"

  shows "(P \<parallel> Q) \<parallel> R \<leadsto>[Rel] P \<parallel> (Q \<parallel> R)"
by(fastsimp 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 \<parallel> (T \<parallel> U), (S \<parallel> T) \<parallel> U) ∈ Rel"

  shows "P \<parallel> (Q \<parallel> R) \<leadsto>[Rel] (P \<parallel> Q) \<parallel> R"
by(fastsimp simp add: simulation_def elim: parCases intro: Par1 Par2 Comm C1)

lemma parIdLeft:
  fixes P   :: ccs
  and   Rel :: "(ccs × ccs) set"
  
  assumes "!!Q. (Q \<parallel> \<zero>, Q) ∈ Rel"

  shows "P \<parallel> \<zero> \<leadsto>[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 \<parallel> \<zero>) ∈ Rel"

  shows "P \<leadsto>[Rel] P \<parallel> \<zero>"
using assms
by(fastsimp simp add: simulation_def elim: parCases)

declare fresh_atm[simp]

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

  assumes "x \<sharp> α"
  and     "Id ⊆ Rel"

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

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

  assumes "x \<sharp> α"
  and     "Id ⊆ Rel"

  shows "α.((|νx|)),P) \<leadsto>[Rel] (|νx|)),(α.(P))"
using assms
by(fastsimp 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) \<leadsto>[Rel] (|νy|)),((|νx|)),P)"
using assms
by(fastsimp simp add: simulation_def elim: resCases intro: Res)

inductive_cases bangCases[simplified ccs.distinct act.distinct]: "!P \<longmapsto>α \<prec> P'"

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

  shows "P \<parallel> !P \<leadsto>[Rel] !P"
using assms
by(fastsimp simp add: simulation_def ccs.inject elim: bangCases)

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

  shows "!P \<leadsto>[Rel] P \<parallel> !P"
using assms
by(fastsimp simp add: simulation_def ccs.inject intro: Bang)

end