Theory Weak_Early_Cong_Subst

(* 
   Title: The pi-calculus   
   Author/Maintainer: Jesper Bengtson (jebe.dk), 2012
*)
theory Weak_Early_Cong_Subst
  imports Weak_Early_Cong Weak_Early_Bisim_Subst Strong_Early_Bisim_Subst
begin

consts congruenceSubst :: "(pi × pi) set"

definition weakCongruenceSubst (infixr "≃⇧s" 65) where "P ≃⇧s Q ≡ ∀σ. P[<σ>] ≃ Q[<σ>]"

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

  assumes "P ≃⇧s Q"

  shows "P[<s>] ↝«weakBisim» Q[<s>]"
  and   "Q[<s>] ↝«weakBisim» P[<s>]"
proof -
  from assms show "P[<s>] ↝«weakBisim» Q[<s>]" by(simp add: weakCongruenceSubst_def weakCongruence_def)
next
  from assms show "Q[<s>] ↝«weakBisim» P[<s>]" by(simp add: weakCongruenceSubst_def weakCongruence_def)
qed

lemma unfoldI:
  fixes P :: pi
  and   Q :: pi

  assumes "⋀s. P[<s>] ↝«weakBisim» Q[<s>]"
  and     "⋀s. Q[<s>] ↝«weakBisim» P[<s>]"

  shows "P ≃⇧s Q"
using assms
by(simp add: weakCongruenceSubst_def weakCongruence_def)

lemma weakCongWeakEq:
  fixes P :: pi
  and   Q :: pi

  assumes "P ≃⇧s Q"

  shows "P ≃ Q"
using assms
apply(simp add: weakCongruenceSubst_def weakCongruence_def)
apply(erule_tac x="[]" in allE)
by auto

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

  assumes "P ≃⇧s Q"

  shows "(p ∙ P) ≃⇧s (p ∙ Q)"
proof(simp add: weakCongruenceSubst_def, rule allI)
  fix s
  from assms have "P[<(rev p ∙ s)>] ≃ Q[<(rev p ∙ s)>]" by(auto simp add: weakCongruenceSubst_def)
  thus "(p ∙ P)[<s>] ≃ (p ∙ Q)[<s>]" by(drule_tac p=p in Weak_Early_Cong.eqvtI) (simp add: eqvts name_per_rev)
qed

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

  shows "P ≃⇧s Q"
using assms
by(auto intro: strongBisimWeakCong simp add: substClosed_def weakCongruenceSubst_def)

lemma congSubstBisimSubst:
  fixes P :: pi
  and   Q :: pi
  
  assumes "P ≃⇧s Q"

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

lemma reflexive:
  fixes P :: pi
  
  shows "P ≃⇧s P"
proof -
  from Weak_Early_Bisim.reflexive have "⋀P. P ↝«weakBisim» P"
    by(blast intro: Weak_Early_Step_Sim.reflexive)
  thus ?thesis
    by(force simp add: weakCongruenceSubst_def weakCongruence_def)
qed

lemma symetric:
  fixes P :: pi
  and   Q :: pi
  
  assumes "P ≃⇧s Q"
  
  shows "Q ≃⇧s P"
using assms by(auto simp add: weakCongruenceSubst_def weakCongruence_def)

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(auto simp add: weakCongruenceSubst_def intro: Weak_Early_Cong.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: weakCongruenceSubst_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