Theory Weak_Late_Bisim_Subst

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

consts weakBisimSubst :: "(pi × pi) set"
abbreviation
  weakBisimSubstJudge (infixr "≈⇧s" 65) where "P ≈⇧s Q ≡ (P, Q) ∈ (substClosed weakBisim)"

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

  assumes "P ≈⇧s Q"

  shows "P ≈ Q"
proof -
  from assms substClosedSubset show ?thesis
    by blast
qed

lemma strongBisimWeakBisim:
  fixes P :: pi
  and   Q :: pi
  
  assumes "P ∼⇧s Q"

  shows "P ≈⇧s Q"
using assms
by(auto simp add: substClosed_def intro: strongBisimWeakBisim)

lemma eqvt:
  shows "eqvt (substClosed weakBisim)"
by(rule eqvtSubstClosed[OF Weak_Late_Bisim.eqvt])

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

  assumes "P ≈⇧s Q"

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

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

lemma symetric:
  fixes P :: pi
  and   Q :: pi
  
  assumes "P ≈⇧s Q"
  
  shows "Q ≈⇧s P"
using assms
by(force simp add: substClosed_def intro: Weak_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: Weak_Late_Bisim.transitive)


lemma partUnfold:
  fixes P :: pi
  and   Q :: pi
  and   s :: "(name × name) list"

  assumes "P ≈⇧s Q"

  shows "P[<s>] ≈⇧s Q[<s>]"
using assms
proof(auto simp add: substClosed_def)
  fix s'
  assume "∀s. P[<s>] ≈ Q[<s>]"
  hence "P[<(s@s')>] ≈ Q[<(s@s')>]" by blast
  moreover have "P[<(s@s')>] = (P[<s>])[<s'>]"
    by(induct s', auto)
  moreover have "Q[<(s@s')>] = (Q[<s>])[<s'>]"
    by(induct s', auto)
  
  ultimately show "(P[<s>])[<s'>] ≈ (Q[<s>])[<s'>]"
    by simp
qed
  
end