Theory Weak_Late_Cong_Subst

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

definition congruenceSubst :: "pi ⇒ pi⇒ bool" (infixr ‹≃⇧s› 65) where
  "P ≃⇧s Q ≡ (P, Q) ∈ (substClosed congruence)"

lemmas congruenceSubstDef = congruenceSubst_def congruence_def substClosed_def

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(force simp add: congruenceSubstDef)
next
  from assms show "Q[<s>] ↝<weakBisim> P[<s>]" by(force simp add: congruenceSubstDef)
qed

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

  assumes "∀s. P[<s>] ↝<weakBisim> Q[<s>] ∧ Q[<s>] ↝<weakBisim> P[<s>]"

  shows "P ≃⇧s Q"
proof -
  from assms show ?thesis by(force simp add: congruenceSubstDef)
qed

lemma weakEqSubset:
  shows "substClosed congruence ⊆ weakBisim"
proof(auto simp add: substClosed_def)
  fix P Q
  assume "∀s. P[<s>] ≃ Q[<s>]"
  hence "P[<[]>] ≃ Q[<[]>]" by blast
  thus "P ≈ Q"
    by(force dest: congruenceWeakBisim intro: Weak_Late_Bisim.unfoldI)
qed


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

  assumes "P ≃⇧s Q"

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

lemma eqvt:
  shows "eqvt (substClosed congruence)"
by(rule eqvtSubstClosed[OF Weak_Late_Cong.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(simp add: congruenceSubst_def) (rule eqvtRelI[OF eqvt])

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

  shows "P ≃⇧s Q"
using assms
by(force intro: strongBisimWeakEq simp add: substClosed_def congruenceSubst_def)

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

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


lemma reflexive:
  fixes P :: pi
  
  shows "P ≃⇧s P"
proof -
  from Weak_Late_Bisim.reflexive have "⋀P. P ↝<weakBisim> P"
    by(blast intro: Weak_Late_Step_Sim.reflexive)
  thus ?thesis
    by(force simp add: congruenceSubstDef)
qed

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

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: congruenceSubst_def substClosed_def intro: Weak_Late_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: congruenceSubst_def substClosed_def)
  fix s'
  assume "∀s. (P[<s>], Q[<s>]) ∈ congruence"
  hence "(P[<(s@s')>], Q[<(s@s')>]) ∈ congruence" 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'>]) ∈ congruence"
    by simp
qed

end