Theory Weak_Cong_Pres

(* 
   Title: Psi-calculi   
   Author/Maintainer: Jesper Bengtson (jebe@itu.dk), 2012
*)
theory Weak_Cong_Pres
  imports Weak_Psi_Congruence Weak_Cong_Sim_Pres Weak_Bisim_Pres
begin

context env begin

lemma weakPsiCongInputPres:
  fixes Ψ    :: 'b
  and   P    :: "('a, 'b, 'c) psi"
  and   Q    :: "('a, 'b, 'c) psi"
  and   M    :: 'a
  and   xvec :: "name list"
  and   N    :: 'a

  assumes "⋀Tvec. length xvec = length Tvec ⟹  Ψ ⊳ P[xvec::=Tvec] ≈ Q[xvec::=Tvec]"

  shows "Ψ ⊳ M⦇λ*xvec N⦈.P ≐ M⦇λ*xvec N⦈.Q"
proof -
  from assms have "∀Tvec. length xvec = length Tvec ⟶  Ψ ⊳ P[xvec::=Tvec] ≈ Q[xvec::=Tvec]"
    by simp
  thus ?thesis
  proof(induct rule: weakPsiCongSymI)
    case(cSym P Q)
    thus ?case by(auto dest: weakBisimE)
  next
    case(cSim P Q)
    show ?case 
      by(induct rule: weakCongSimI) auto
  next
    case(cWeakBisim P Q)
    thus ?case by(rule_tac weakBisimInputPres) auto
  qed
qed
  
lemma weakPsiCongOutputPres:
  fixes Ψ    :: 'b
  and   P    :: "('a, 'b, 'c) psi"
  and   Q    :: "('a, 'b, 'c) psi"
  and   M    :: 'a
  and   xvec :: "name list"
  and   N    :: 'a

  assumes "Ψ ⊳ P ≐ Q"

  shows "Ψ ⊳ M⟨N⟩.P ≐ M⟨N⟩.Q"
using assms
proof(induct rule: weakPsiCongSymI)
  case(cSym P Q)
  thus ?case by(rule weakPsiCongSym)
next
  case(cSim P Q)
  show ?case by(induct rule: weakCongSimI) auto
next
  case(cWeakBisim P Q)
  thus ?case by(metis weakPsiCongE weakBisimOutputPres)
qed

lemma weakBisimCasePres:
  fixes Ψ   :: 'b
  and   CsP :: "('c × ('a, 'b, 'c) psi) list"
  and   CsQ :: "('c × ('a, 'b, 'c) psi) list"

  assumes A: "⋀φ P. (φ, P) mem CsP ⟹ ∃Q. (φ, Q) mem CsQ ∧ guarded Q ∧ (∀Ψ. Ψ ⊳ P ≐ Q)"
  and     B: "⋀φ Q. (φ, Q) mem CsQ ⟹ ∃P. (φ, P) mem CsP ∧ guarded P ∧ (∀Ψ. Ψ ⊳ P ≐ Q)"

  shows "Ψ ⊳ Cases CsP ≈ Cases CsQ"
proof -
  let ?X = "{(Ψ, Cases CsP, Cases CsQ) | Ψ CsP CsQ. (∀φ P. (φ, P) mem CsP ⟶ (∃Q. (φ, Q) mem CsQ ∧ guarded Q ∧ (∀Ψ. Ψ ⊳ P ≐ Q))) ∧
                                                     (∀φ Q. (φ, Q) mem CsQ ⟶ (∃P. (φ, P) mem CsP ∧ guarded P ∧ (∀Ψ. Ψ ⊳ P ≐ Q)))}"
  from assms have "(Ψ, Cases CsP, Cases CsQ) ∈ ?X" by auto
  thus ?thesis
  proof(coinduct rule: weakBisimCoinduct)
    case(cStatImp Ψ CasesP CasesQ)
    thus ?case
      apply(auto simp add: weakStatImp_def)
      by(rule_tac x="Cases CsQ" in exI, auto)
  next
    case(cSim Ψ CasesP CasesQ)
    then obtain CsP CsQ where C1: "⋀φ Q. (φ, Q) mem CsQ ⟹ ∃P. (φ, P) mem CsP ∧ guarded P ∧ (∀Ψ. Ψ ⊳ P ≐ Q)"
                          and A: "CasesP = Cases CsP" and B: "CasesQ = Cases CsQ"
      by auto
    note C1
    moreover have "⋀Ψ P Q. Ψ ⊳ P ≈ Q ⟹ Ψ ⊳ P ↝<weakBisim> Q" by(rule weakBisimE)
    moreover note weakPsiCongE(1) weakPsiCongE(2)
    ultimately have "Ψ ⊳ Cases CsP ↝<weakBisim> Cases CsQ"
      by(rule_tac caseWeakSimPres) (assumption | blast)+
    hence "Ψ ⊳ Cases CsP ↝<(?X ∪ weakBisim)> Cases CsQ"
      by(rule_tac weakSimMonotonic) auto
    with A B show ?case by blast
  next
    case(cExt Ψ P Q Ψ')
    thus ?case by auto
  next
    case(cSym Ψ P Q)
    thus ?case by auto (metis weakPsiCongSym)+
  qed
qed

lemma weakPsiCongCasePres:
  fixes Ψ   :: 'b
  and   CsP :: "('c × ('a, 'b, 'c) psi) list"
  and   CsQ :: "('c × ('a, 'b, 'c) psi) list"

  assumes A: "⋀φ P. (φ, P) mem CsP ⟹ ∃Q. (φ, Q) mem CsQ ∧ guarded Q ∧ (∀Ψ. Ψ ⊳ P ≐ Q)"
  and     B: "⋀φ Q. (φ, Q) mem CsQ ⟹ ∃P. (φ, P) mem CsP ∧ guarded P ∧ (∀Ψ. Ψ ⊳ P ≐ Q)"

  shows "Ψ ⊳ Cases CsP ≐ Cases CsQ"
proof -
  let ?Prop = "λCsP CsQ. ∀φ P. (φ, P) mem CsP ⟶ (∃Q. (φ, Q) mem CsQ ∧ guarded Q ∧ (∀Ψ. Ψ ⊳ P ≐ Q))"
  from A B have "?Prop CsP CsQ ∧ ?Prop CsQ CsP" by(metis weakPsiCongSym)
  thus ?thesis
  proof(induct rule: weakPsiCongSymI[where C="λP. Cases P"])
    case(cSym P Q)
    thus ?case by auto
  next
    case(cWeakBisim CsP CsQ)
    thus ?case
      by(rule_tac weakBisimCasePres) (metis weakPsiCongSym)+
  next
    case(cSim CsP CsQ)
    thus ?case       
      apply auto
      apply(rule_tac weakCongSimCasePres, auto)
      by(blast dest: weakPsiCongE)
  qed
qed

lemma weakPsiCongResPres:
  fixes Ψ :: 'b
  and   P :: "('a, 'b, 'c) psi"
  and   Q :: "('a, 'b, 'c) psi"
  and   x :: name
  
  assumes "Ψ ⊳ P ≐ Q"
  and     "x ♯ Ψ"

  shows "Ψ ⊳ ⦇νx⦈P ≐ ⦇νx⦈Q"
using ‹Ψ ⊳ P ≐ Q›
proof(induct rule: weakPsiCongSymI)
  case(cSym P Q)
  thus ?case by(rule weakPsiCongSym)
next
  case(cWeakBisim P Q)
  thus ?case using ‹x ♯ Ψ› by(metis weakPsiCongE weakBisimResPres)
next
  case(cSim P Q)
  obtain y::name where "y ♯ Ψ" and "y ♯ P" and "y ♯ Q"
    by(generate_fresh "name") auto
  from ‹Ψ ⊳ P ≐ Q› have "([(x, y)] ∙ Ψ) ⊳ ([(x, y)] ∙ P) ≐ ([(x, y)] ∙ Q)" by(rule weakPsiCongClosed)
  hence "([(x, y)] ∙ Ψ) ⊳ ([(x, y)] ∙ P) ↝«weakBisim» ([(x, y)] ∙ Q)" by(rule weakPsiCongE)
  with ‹x ♯ Ψ› ‹y ♯ Ψ› have "Ψ  ⊳ ([(x, y)] ∙ P) ↝«weakBisim» ([(x, y)] ∙ Q)" by simp
  moreover have "eqvt weakBisim" by simp
  moreover note ‹y ♯ Ψ›
  moreover have "weakBisim ⊆ weakBisim" by auto
  moreover note weakBisimResPres
  ultimately have "Ψ ⊳ ⦇νy⦈([(x, y)] ∙ P) ↝«weakBisim» ⦇νy⦈([(x, y)] ∙ Q)" by(rule weakCongSimResPres)
  with ‹y ♯ P› ‹y ♯ Q› show ?case by(simp add: alphaRes)
qed

lemma weakPsiCongResChainPres:
  fixes Ψ   :: 'b
  and   P    :: "('a, 'b, 'c) psi"
  and   Q    :: "('a, 'b, 'c) psi"
  and   xvec :: "name list"

  assumes "Ψ ⊳ P ≐ Q"
  and     "xvec ♯* Ψ"

  shows "Ψ ⊳ ⦇ν*xvec⦈P ≐ ⦇ν*xvec⦈Q"
using assms
by(induct xvec) (auto intro: weakPsiCongResPres)

lemma weakPsiCongParPres:
  fixes Ψ :: 'b
  and   P :: "('a, 'b, 'c) psi"
  and   Q :: "('a, 'b, 'c) psi"
  and   R :: "('a, 'b, 'c) psi"
  
  assumes "∀Ψ. Ψ ⊳ P ≐ Q"

  shows "Ψ ⊳ P ∥ R ≐ Q ∥ R"
using assms
proof(induct rule: weakPsiCongSymI[where C="λP. P ∥ R"])
  case(cSym P Q)
  thus ?case by(blast dest: weakPsiCongSym)
next
  case(cWeakBisim P Q)
  thus ?case by(metis weakBisimParPres weakPsiCongE)
next
  case(cSim P Q)
  {
    fix Ψ
    from ‹∀Ψ. Ψ ⊳ P ≐ Q› have "Ψ ⊳ P ↝«weakBisim» Q" by(auto dest: weakPsiCongE)
  }
  moreover {
    fix Ψ
    from ‹∀Ψ. Ψ ⊳ P ≐ Q› have "Ψ ⊳ P ↝<weakBisim> Q" by(auto dest: weakPsiCongE weakBisimE)
  }
  moreover {
    fix Ψ
    from ‹∀Ψ. Ψ ⊳ P ≐ Q› have "Ψ ⊳ P ≈ Q" by(auto dest: weakPsiCongE)
    hence "Ψ ⊳ Q ⪅<weakBisim> P" by(metis weakBisimE)
  }
  ultimately show ?case using weakBisimEqvt weakBisimEqvt weakBisimE(4)  weakBisimE(3) weakBisimParPresAux weakBisimResChainPres statEqWeakBisim
    by(rule_tac weakCongSimParPres)
qed

end

end