Theory Strong_Late_Bisim_Subst

(* 
   Title: The pi-calculus   
   Author/Maintainer: Jesper Bengtson (jebe.dk), 2012
*)
theory Strong_Late_Bisim_Subst
  imports Strong_Late_Bisim
begin

abbreviation
  StrongEqJudge (infixr "∼⇧s" 65) where "P ∼⇧s Q ≡ (P, Q) ∈ (substClosed bisim)"


lemma congBisim:
  fixes P :: pi
  and   Q :: pi

  assumes "P ∼⇧s Q"

  shows "P ∼ Q"
using assms substClosedSubset by blast

lemma eqvt:
  shows "eqvt (substClosed bisim)"
by(rule eqvtSubstClosed[OF Strong_Late_Bisim.bisimEqvt])

lemma eqClosed:
  fixes P :: pi
  and   Q :: pi
  and   perm :: "name prm"

  assumes "P ∼⇧s Q"

  shows "(perm ∙ P) ∼⇧s (perm ∙ Q)"
using assms
by(rule eqvtRelI[OF eqvt])

lemma reflexive:
  fixes P :: pi
  
  shows "P ∼⇧s P"
by(force simp add: substClosed_def intro: Strong_Late_Bisim.reflexive)

lemma symmetric:
  fixes P :: pi
  and   Q :: pi
  
  assumes "P ∼⇧s Q"
  
  shows "Q ∼⇧s P"
using assms
by(force simp add: substClosed_def intro: Strong_Late_Bisim.symmetric)

lemma transitive:
  fixes P :: pi
  and   Q :: pi
  and   R :: pi
  
  assumes "P ∼⇧s Q"
  and     "Q ∼⇧s R"
  
  shows "P ∼⇧s R"
using assms
by(force simp add: substClosed_def intro: Strong_Late_Bisim.transitive)

end