Theory Weak_Early_Bisim_Pres

(* 
   Title: The pi-calculus   
   Author/Maintainer: Jesper Bengtson (jebe.dk), 2012
*)
theory Weak_Early_Bisim_Pres
  imports Strong_Early_Bisim_Pres Weak_Early_Sim_Pres Weak_Early_Bisim_SC Weak_Early_Bisim
begin

(************ Preservation rules ************)

lemma tauPres:
  fixes P :: pi
  and   Q :: pi

  assumes "P ≈ Q"

  shows "τ.(P) ≈ τ.(Q)"
proof -
  let ?X = "{(τ.(P), τ.(Q)) | P Q. P ≈ Q}"
  from ‹P ≈ Q› have "(τ.(P), τ.(Q)) ∈ ?X" by auto
  thus ?thesis
  proof(coinduct rule: weakBisimCoinduct)
    case(cSim P Q)
    thus ?case
      by(force intro: Weak_Early_Sim_Pres.tauPres)
  next
    case(cSym P Q)
    thus ?case by(force dest: Weak_Early_Bisim.symetric simp add: pi.inject)
  qed
qed

lemma outputPres:
  fixes P :: pi
  and   Q :: pi
  and   a :: name
  and   b :: name

  assumes "P ≈ Q"

  shows "a{b}.P ≈ a{b}.Q"
proof -
  let ?X = "{(a{b}.(P), a{b}.(Q)) | P Q a b. P ≈ Q}"
  from ‹P ≈ Q› have "(a{b}.(P), a{b}.(Q)) ∈ ?X" by auto
  thus ?thesis
  proof(coinduct rule: weakBisimCoinduct)
    case(cSim P Q)
    thus ?case
      by(force intro: Weak_Early_Sim_Pres.outputPres)
  next
    case(cSym P Q)
    thus ?case by(force dest: Weak_Early_Bisim.symetric simp add: pi.inject)
  qed
qed

lemma inputPres:
  fixes P :: pi
  and   Q :: pi
  and   a :: name
  and   x :: name

  assumes PSimQ: "∀y. P[x::=y] ≈ Q[x::=y]"
  
  shows "a<x>.P ≈ a<x>.Q"
proof -
  let ?X = "{(a<x>.P, a<x>.Q) | a x P Q. ∀y. P[x::=y] ≈ Q[x::=y]}"
  {
    fix axP axQ p
    assume "(axP, axQ) ∈ ?X"
    then obtain a x P Q where A: "∀y. P[x::=y] ≈ Q[x::=y]" and B: "axP = a<x>.P" and C: "axQ = a<x>.Q"
      by auto
    have "⋀y. ((p::name prm) ∙ P)[(p ∙ x)::=y] ≈ (p ∙ Q)[(p ∙ x)::=y]"
    proof -
      fix y
      from A have "P[x::=(rev p ∙ y)] ≈ Q[x::=(rev p ∙ y)]"
        by blast
      hence "(p ∙ (P[x::=(rev p ∙ y)])) ≈ p ∙ (Q[x::=(rev p ∙ y)])"
        by(rule eqvts)
      thus "(p ∙ P)[(p ∙ x)::=y] ≈ (p ∙ Q)[(p ∙ x)::=y]"
        by(simp add: eqvts pt_pi_rev[OF pt_name_inst, OF at_name_inst])
    qed
    hence "((p::name prm) ∙ axP, p ∙ axQ) ∈ ?X" using B C
      by auto
  }
  hence "eqvt ?X" by(simp add: eqvt_def)

  from PSimQ have "(a<x>.P, a<x>.Q) ∈ ?X" by auto
  thus ?thesis
  proof(coinduct rule: weakBisimCoinduct)
    case(cSim P Q)
    thus ?case using ‹eqvt ?X›
      by(force intro: Weak_Early_Sim_Pres.inputPres)
  next
    case(cSym P Q)
    thus ?case
      by(blast dest: weakBisimE)
  qed
qed

lemma resPres:
  fixes P :: pi
  and   Q :: pi
  and   x :: name
  
  assumes "P ≈ Q"

  shows "<νx>P ≈ <νx>Q"
proof -
  let ?X = "{(<νx>P, <νx>Q) | x P Q. P ≈ Q}"
  from ‹P ≈ Q› have "(<νx>P, <νx>Q) ∈ ?X" by blast
  thus ?thesis
  proof(coinduct rule: weakBisimCoinduct)
    case(cSim xP xQ)
    {
      fix P Q x
      assume "P ≈ Q"
      hence "P ↝<weakBisim> Q" by(rule weakBisimE)
      moreover have "⋀P Q x. P ≈ Q ⟹ (<νx>P, <νx>Q) ∈ ?X ∪ weakBisim" by blast
      moreover have "weakBisim ⊆ ?X ∪ weakBisim" by blast
      moreover have "eqvt weakBisim" by simp
      moreover have "eqvt (?X ∪ weakBisim)"
        by(auto simp add: eqvt_def dest: Weak_Early_Bisim.eqvtI)+
      ultimately have "<νx>P ↝<(?X ∪ weakBisim)> <νx>Q"
        by(rule Weak_Early_Sim_Pres.resPres)
    }
    with ‹(xP, xQ) ∈ ?X› show ?case by blast
  next
    case(cSym xP xQ)
    thus ?case by(blast dest: Weak_Early_Bisim.symetric)
  qed
qed

lemma matchPres:
  fixes P :: pi
  and   Q :: pi
  and   a :: name
  and   b :: name

  assumes "P ≈ Q"

  shows "[a⌢b]P ≈ [a⌢b]Q"
proof -
  let ?X = "{([a⌢b]P, [a⌢b]Q) | a b P Q. P ≈ Q}"
  from ‹P ≈ Q› have "([a⌢b]P, [a⌢b]Q) ∈ ?X" by blast
  thus ?thesis
  proof(coinduct rule: weakBisimCoinduct)
    case(cSim abP abQ)
    {
      fix P Q a b
      assume "P ≈ Q"
      hence "P ↝<weakBisim> Q" by(rule weakBisimE)
      moreover have "weakBisim ⊆ (?X ∪ weakBisim)" by blast
      moreover have "⋀P Q a. P ≈ Q ⟹ [a⌢a]P ≈ Q"
        by (metis (full_types) strongBisimWeakBisim Strong_Early_Bisim_SC.matchId Weak_Early_Bisim.transitive)
      ultimately have"[a⌢b]P ↝<(?X ∪ weakBisim)> [a⌢b]Q" 
        by(rule Weak_Early_Sim_Pres.matchPres)
    }
    with ‹(abP, abQ) ∈ ?X› show ?case by blast
  next
    case(cSym abP abQ)
    thus ?case by(blast dest: Weak_Early_Bisim.symetric)
  qed
qed

lemma mismatchPres:
  fixes P :: pi
  and   Q :: pi
  and   a :: name
  and   b :: name

  assumes "P ≈ Q"

  shows "[a≠b]P ≈ [a≠b]Q"
proof -
  let ?X = "{([a≠b]P, [a≠b]Q)| a b P Q. P ≈ Q}"
  from ‹P ≈ Q› have "([a≠b]P, [a≠b]Q) ∈ ?X" by blast
  thus ?thesis
  proof(coinduct rule: weakBisimCoinduct)
    case(cSim abP abQ)
    {
      fix P Q a b
      assume "P ≈ Q"
      hence "P ↝<weakBisim> Q" by(rule weakBisimE)
      moreover have "weakBisim ⊆ (?X ∪ weakBisim)" by blast
      moreover have "⋀P Q a b. ⟦P ≈ Q; a ≠ b⟧ ⟹ [a≠b]P ≈ Q"
        by (metis (full_types) strongBisimWeakBisim Strong_Early_Bisim_SC.mismatchId Weak_Early_Bisim.transitive)
      ultimately have "[a≠b]P ↝<(?X ∪ weakBisim)> [a≠b]Q"
        by(rule Weak_Early_Sim_Pres.mismatchPres) 
    }
    with ‹(abP, abQ) ∈ ?X› show ?case by blast
  next
    case(cSym abP abQ)
    thus ?case by(blast dest: Weak_Early_Bisim.symetric)
  qed
qed

lemma parPres:
  fixes P :: pi
  and   Q :: pi
  and   R :: pi

  assumes "P ≈ Q"

  shows "P ∥ R ≈ Q ∥ R"
proof -
  let ?X = "{(resChain lst (P ∥ R), resChain lst (Q ∥ R)) | lst P R Q. P ≈ Q}"
  have BC: "⋀P Q. P ∥ Q = resChain [] (P ∥ Q)" by auto
  from ‹P ≈ Q› have "(P ∥ R, Q ∥ R) ∈ ?X" by(blast intro: BC)
  thus ?thesis
  proof(coinduct rule: weakBisimCoinduct)
    case(cSym PR QR)
    {
      fix P Q R lst
      assume "P ≈ Q"
      moreover hence "P ↝<weakBisim> Q" by(rule weakBisimE)
      moreover have "⋀P Q R. P ≈ Q ⟹ (P ∥ R, Q ∥ R) ∈ ?X" using BC
        by blast
      moreover {
        fix PR QR x
        assume "(PR, QR) ∈ ?X"
        then obtain lst P Q R where "P ≈ Q" and A: "PR = resChain lst (P ∥ R)" and B: "QR = resChain lst (Q ∥ R)"
          by auto
        from A have "<νx>PR = resChain (x#lst) (P ∥ R)" by auto
        moreover from B have "<νx>QR = resChain (x#lst) (Q ∥ R)" by auto
        ultimately have "(<νx>PR, <νx>QR) ∈ ?X" using ‹P ≈ Q›
          by blast
      }
      note Res = this
      ultimately have "P ∥ R ↝<?X> Q ∥ R"
        by(rule_tac Weak_Early_Sim_Pres.parPres)
      moreover have "eqvt ?X"
        by(auto simp add: eqvt_def) (blast intro: eqvts)
      ultimately have "resChain lst (P ∥ R) ↝<?X> resChain lst (Q ∥ R)" using Res
        by(rule_tac Weak_Early_Sim_Pres.resChainI)
      hence "resChain lst (P ∥ R) ↝<(?X ∪ weakBisim)> resChain lst (Q ∥ R)"
        by(force intro: Weak_Early_Sim.monotonic)
    }
    with ‹(PR, QR) ∈ ?X› show "PR ↝<(?X ∪ weakBisim)> QR"
      by blast
  next
    case(cSym PR QR)
    thus ?case by(blast dest: Weak_Early_Bisim.symetric)
  qed
qed

lemma bangPres:
  fixes P :: pi
  and   Q :: pi

  assumes PBisimQ: "P ≈ Q"

  shows "!P ≈ !Q"
proof -
  let ?X = "(bangRel weakBisim)"
  let ?Y = "Strong_Early_Bisim.bisim O (bangRel weakBisim) O Strong_Early_Bisim.bisim"

  from Weak_Early_Bisim.eqvt Strong_Early_Bisim.eqvt have eqvtY: "eqvt ?Y" by(blast intro: eqvtBangRel)
  have XsubY: "?X ⊆ ?Y" by(auto intro: Strong_Early_Bisim.reflexive)

  have RelStay: "⋀P Q. (P ∥ !P, Q) ∈ ?Y ⟹ (!P, Q) ∈ ?Y"
  proof(auto)
    fix P Q R T
    assume PBisimQ: "P ∥ !P ∼⇩e Q" 
       and QBRR: "(Q, R) ∈ bangRel weakBisim"
       and RBisimT: "R ∼⇩e T"
    have "!P ∼⇩e Q" 
    proof -
      have "!P ∼⇩e P ∥ !P" by(rule Strong_Early_Bisim_SC.bangSC)
      thus ?thesis using PBisimQ by(rule Strong_Early_Bisim.transitive)
    qed
    with QBRR RBisimT show "(!P, T) ∈ ?Y" by blast
  qed
 
  have ParCompose: "⋀P Q R T. ⟦P ≈ Q; (R, T) ∈ ?Y⟧ ⟹ (P ∥ R, Q ∥ T) ∈ ?Y"
  proof -
    fix P Q R T
    assume PBisimQ: "P ≈ Q"
       and RYT:     "(R, T) ∈ ?Y"
    thus "(P ∥ R, Q ∥ T) ∈ ?Y"
    proof(auto)
      fix T' R'
      assume T'BisimT: "T' ∼⇩e T" and RBisimR': "R ∼⇩e R'"
         and R'BRT': "(R', T') ∈ bangRel weakBisim"
      have "P ∥ R ∼⇩e P ∥ R'"
      proof -
        from RBisimR' have "R ∥ P ∼⇩e R' ∥ P" by(rule Strong_Early_Bisim_Pres.parPres)
        moreover have "P ∥ R ∼⇩e R ∥ P" and "R' ∥ P ∼⇩e P ∥ R'" by(rule Strong_Early_Bisim_SC.parSym)+
        ultimately show ?thesis by(blast intro: Strong_Early_Bisim.transitive)
      qed
      moreover from PBisimQ R'BRT' have "(P ∥ R', Q ∥ T') ∈ bangRel weakBisim" by(rule BRPar)
      moreover have "Q ∥ T' ∼⇩e Q ∥ T"
      proof -
        from T'BisimT have "T' ∥ Q ∼⇩e T ∥ Q" by(rule Strong_Early_Bisim_Pres.parPres)
        moreover have "Q ∥ T' ∼⇩e T' ∥ Q" and "T ∥ Q ∼⇩e Q ∥ T" by(rule Strong_Early_Bisim_SC.parSym)+
        ultimately show ?thesis by(blast intro: Strong_Early_Bisim.transitive)
      qed
      ultimately show ?thesis by blast
    qed
  qed

  have ResCong: "⋀P Q x. (P, Q) ∈ ?Y ⟹ (<νx>P, <νx>Q) ∈ ?Y"
    by(auto intro: BRRes Strong_Early_Bisim_Pres.resPres transitive)

  have Sim: "⋀P Q. (P, Q) ∈ ?X ⟹ P ↝<?Y> Q"
  proof -
    fix P Q
    assume "(P, Q) ∈ ?X"
    thus "P ↝<?Y> Q"
    proof(induct)
      case(BRBang P Q)
      have "P ≈ Q" by fact
      moreover hence "P ↝<weakBisim> Q" by(blast dest: weakBisimE)
      moreover have "⋀P Q. P ≈ Q ⟹ P ↝<weakBisim> Q" by(blast dest: weakBisimE)
      moreover from Strong_Early_Bisim.eqvt Weak_Early_Bisim.eqvt have "eqvt ?Y" by(blast intro: eqvtBangRel)

      ultimately show "!P ↝<?Y> !Q" using ParCompose ResCong RelStay XsubY
        by(rule_tac Weak_Early_Sim_Pres.bangPres, simp_all)
    next
      case(BRPar P Q R T)
      have PBiSimQ: "P ≈ Q" by fact
      moreover have RBangRelT: "(R, T) ∈ ?X" by fact
      have RSimT: "R ↝<?Y> T" by fact
      moreover from PBiSimQ  have "P ↝<weakBisim> Q" by(blast dest: weakBisimE)
      moreover from RBangRelT have "(R, T) ∈ ?Y" by(blast intro: Strong_Early_Bisim.reflexive)
      ultimately show "P ∥ R ↝<?Y> Q ∥ T" using ParCompose ResCong eqvt eqvtY
        by(rule_tac Weak_Early_Sim_Pres.parCompose)
    next
      case(BRRes P Q x)
      have "P ↝<?Y> Q" by fact
      thus "<νx>P ↝<?Y> <νx>Q" using ResCong eqvtY XsubY
        by(rule_tac Weak_Early_Sim_Pres.resPres, simp_all)
    qed
  qed

  from PBisimQ have "(!P, !Q) ∈ ?X" by(rule BRBang)
  moreover from Weak_Early_Bisim.eqvt have "eqvt (bangRel weakBisim)" by(rule eqvtBangRel)
  ultimately show ?thesis
    apply(coinduct rule: Weak_Early_Bisim.transitive_coinduct_weak)
    apply(blast intro: Sim)
    by(blast dest: bangRelSymetric Weak_Early_Bisim.symetric intro: Strong_Early_Bisim.reflexive)
qed

lemma bangRelSubWeakBisim:
  shows "bangRel weakBisim ⊆ weakBisim"
proof(auto)
  fix a b
  assume "(a, b) ∈ bangRel weakBisim"
  thus "a ≈ b"
  proof(induct)
    fix P Q
    assume "P ≈ Q"
    thus "!P ≈ !Q" by(rule bangPres)
  next
    fix P Q R T
    assume "R ≈ T" and "P ≈ Q"
    thus "R ∥ P ≈ T ∥ Q" by(metis parPres parSym Weak_Early_Bisim.transitive)
  next
    fix P Q
    fix a::name
    assume "P ≈ Q"
    thus "<νa>P ≈ <νa>Q" by(rule resPres)
  qed
qed

end