Theory Weak_Late_Bisim_Pres

(* 
   Title: The pi-calculus   
   Author/Maintainer: Jesper Bengtson (jebe.dk), 2012
*)
theory Weak_Late_Bisim_Pres
  imports Weak_Late_Bisim_SC Weak_Late_Sim_Pres Strong_Late_Bisim_SC
begin

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

  assumes "P ≈ Q"

  shows "τ.(P) ≈ τ.(Q)"
proof -
  let ?X = "{(τ.(P), τ.(Q)) | P Q. P ≈ Q}"
  from assms have "(τ.(P), τ.(Q)) ∈ ?X" by auto
  thus ?thesis
    by(coinduct rule: weakBisimCoinduct)
      (auto simp add: pi.inject intro:  Weak_Late_Sim_Pres.tauPres symmetric)
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 eqvtI)
      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: inputPres)
  next
    case(cSym P Q)
    thus ?case
      by(blast dest: symmetric)
  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)) | a b P Q. P ≈ Q}"
  from assms have "(a{b}.(P), a{b}.(Q)) ∈ ?X" by auto
  thus ?thesis
    by(coinduct rule: weakBisimCoinduct)
      (auto simp add: pi.inject intro:  Weak_Late_Sim_Pres.outputPres symmetric)
qed

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

  shows "<νx>P ≈ <νx>Q"
proof -
  let ?X = "{x. ∃P Q. P ≈ Q ∧ (∃a. x = (<νa>P, <νa>Q))}"
  from PBiSimQ have "(<νx>P, <νx>Q) ∈ ?X" by blast
  moreover have "⋀P Q a. P ↝⇧^<weakBisim> Q ⟹ <νa>P ↝⇧^<(?X ∪ weakBisim)> <νa>Q"
  proof -
    fix P Q a
    assume PSimQ: "P ↝⇧^<weakBisim> Q"
    moreover have "⋀P Q a. P ≈ Q ⟹ (<νa>P, <νa>Q) ∈ ?X ∪ weakBisim" by blast
    moreover have "weakBisim ⊆ ?X ∪ weakBisim" by blast
    moreover have "eqvt weakBisim" by(rule eqvt)
    moreover have "eqvt (?X ∪ weakBisim)"
      by(auto simp add: eqvt_def dest: eqvtI)+
    ultimately show "<νa>P ↝⇧^<(?X ∪ weakBisim)> <νa>Q"
      by(rule Weak_Late_Sim_Pres.resPres)
  qed
    
  ultimately show ?thesis using PBiSimQ
    by(coinduct rule: weakBisimCoinductAux, blast dest: unfoldE)
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 assms have "([a⌢b]P, [a⌢b]Q) ∈ ?X" by auto
  thus ?thesis
  proof(coinduct rule: weakBisimCoinduct)
    case(cSim P Q)
    {
      fix P Q a b
      assume "P ≈ Q"
      hence "P ↝⇧^<weakBisim> Q" by(rule unfoldE)
      moreover {
        fix P Q a
        assume "P ≈ Q"
        moreover have "[a⌢a]P ≈ P" by(rule matchId)
        ultimately have "[a⌢a]P ≈ Q" by(blast intro: transitive)
      }
      moreover have "weakBisim ⊆ ?X ∪ weakBisim" by blast
      ultimately have "[a⌢b]P ↝⇧^<(?X ∪ weakBisim)> [a⌢b]Q"
        by(rule matchPres)
    }
    with ‹(P, Q) ∈ ?X› show ?case by auto
  next
    case(cSym P Q)
    thus ?case by(auto simp add: pi.inject dest: symmetric)
  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 assms have "([a≠b]P, [a≠b]Q) ∈ ?X" by auto
  thus ?thesis
  proof(coinduct rule: weakBisimCoinduct)
    case(cSim P Q)
    {
      fix P Q a b
      assume "P ≈ Q"
      hence "P ↝⇧^<weakBisim> Q" by(rule unfoldE)
      moreover {
        fix P Q a b
        assume "P ≈ Q" and "(a::name) ≠ b"
        note ‹P ≈ Q›
        moreover from ‹a ≠ b› have "[a≠b]P ≈ P" by(rule mismatchId)
        ultimately have "[a≠b]P ≈ Q" by(blast intro: transitive)
      }
      moreover have "weakBisim ⊆ ?X ∪ weakBisim" by blast
      ultimately have "[a≠b]P ↝⇧^<(?X ∪ weakBisim)> [a≠b]Q"
        by(rule mismatchPres)
    }
    with ‹(P, Q) ∈ ?X› show ?case by auto
  next
    case(cSym P Q)
    thus ?case by(auto simp add: pi.inject dest: symmetric)
  qed
qed

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

  assumes "P ≈ Q"

  shows "P ∥ R ≈ Q ∥ R"
proof -
  let ?ParSet = "{(resChain lst (P ∥ R), resChain lst (Q ∥ R)) | lst P Q R. P ≈ Q}"
  have BC: "⋀P Q. P ∥ Q = resChain [] (P ∥ Q)" by auto
  from assms have "(P ∥ R, Q ∥ R) ∈ ?ParSet" by(blast intro: BC)
  thus ?thesis
  proof(coinduct rule: weakBisimCoinduct)
    case(cSim PR QR)
    {
      fix P Q R lst
      assume "P ≈ Q"
    
      from eqvtI have "eqvt (?ParSet ∪ weakBisim)"
        by(auto simp add: eqvt_def, blast)
      moreover have "⋀P Q a. (P, Q) ∈ ?ParSet ∪ weakBisim ⟹ (<νa>P, <νa>Q) ∈ ?ParSet ∪ weakBisim"
        by(blast intro: resChain.step[THEN sym] resPres)
      moreover {
        from ‹P ≈ Q› have "P ↝⇧^<weakBisim> Q" by(rule unfoldE)
        moreover note ‹P ≈ Q›
        moreover {
          fix P Q R
          assume "P ≈ Q"
          moreover have "P ∥ R = resChain [] (P ∥ R)" by simp
          moreover have "Q ∥ R = resChain [] (Q ∥ R)" by simp
          ultimately have "(P ∥ R, Q ∥ R) ∈ ?ParSet ∪ weakBisim" by blast
        }
        moreover {
          fix P Q a
          assume A: "(P, Q) ∈ ?ParSet ∪ weakBisim"
          hence "(<νa>P, <νa>Q) ∈ ?ParSet ∪ weakBisim" (is "?goal")
            apply(auto intro: resPres)
            by(rule_tac x="a#lst" in exI) auto
        }
        ultimately have "(P ∥ R) ↝⇧^<(?ParSet ∪ weakBisim)> (Q ∥ R)" using eqvt ‹eqvt(?ParSet ∪ weakBisim)›
          by(rule Weak_Late_Sim_Pres.parPres)
      }

      ultimately have "resChain lst (P ∥ R) ↝⇧^<(?ParSet ∪ weakBisim)> resChain lst (Q ∥ R)"
        by(rule resChainI)
    }
    with ‹(PR, QR) ∈ ?ParSet› show ?case by blast
  next
    case(cSym PR QR)
    thus ?case by(auto dest: symmetric)
  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_Late_Bisim.bisim O (bangRel weakBisim) O Strong_Late_Bisim.bisim"

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

  have RelStay: "⋀P Q. (P ∥ !P, Q) ∈ ?Y ⟹ (!P, Q) ∈ ?Y"
  proof(auto)
    fix P Q R T
    assume PBisimQ: "P ∥ !P ∼ Q" 
       and QBRR: "(Q, R) ∈ bangRel weakBisim"
       and RBisimT: "R ∼ T"
    have "!P ∼ Q" 
    proof -
      have "!P ∼ P ∥ !P" by(rule Strong_Late_Bisim_SC.bangSC)
      thus ?thesis using PBisimQ by(rule Strong_Late_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' ∼ T" and RBisimR': "R ∼ R'"
         and R'BRT': "(R', T') ∈ bangRel weakBisim"
      have "P ∥ R ∼ P ∥ R'"
      proof -
        from RBisimR' have "R ∥ P ∼ R' ∥ P" by(rule Strong_Late_Bisim_Pres.parPres)
        moreover have "P ∥ R ∼ R ∥ P" and "R' ∥ P ∼ P ∥ R'" by(rule Strong_Late_Bisim_SC.parSym)+
        ultimately show ?thesis by(blast intro: Strong_Late_Bisim.transitive)
      qed
      moreover from PBisimQ R'BRT' have "(P ∥ R', Q ∥ T') ∈ bangRel weakBisim" by(rule BRPar)
      moreover have "Q ∥ T' ∼ Q ∥ T"
      proof -
        from T'BisimT have "T' ∥ Q ∼ T ∥ Q" by(rule Strong_Late_Bisim_Pres.parPres)
        moreover have "Q ∥ T' ∼ T' ∥ Q" and "T ∥ Q ∼ Q ∥ T" by(rule Strong_Late_Bisim_SC.parSym)+
        ultimately show ?thesis by(blast intro: Strong_Late_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_Late_Bisim_Pres.resPres transitive)

  from PBisimQ have "(!P, !Q) ∈ ?X" by(rule BRBang)
  moreover from eqvt have "eqvt (bangRel weakBisim)" by(rule eqvtBangRel)
  ultimately show ?thesis
  proof(coinduct rule: weakBisimTransitiveCoinduct)
    case(cSim P Q)
    from ‹(P, Q) ∈ ?X›
    show "P ↝⇧^<?Y> Q"
    proof(induct)
      case(BRBang P Q)
      have "P ≈ Q" by fact
      moreover hence "P ↝⇧^<weakBisim> Q" by(blast dest: unfoldE)
      moreover have "⋀P Q. P ≈ Q ⟹ P ↝⇧^<weakBisim> Q" by(blast dest: unfoldE)
      moreover from Strong_Late_Bisim.bisimEqvt eqvt have "eqvt ?Y" by(blast intro: eqvtBangRel)

      ultimately show "!P ↝⇧^<?Y> !Q" using ParCompose ResCong RelStay XsubY
        by(rule_tac Weak_Late_Sim_Pres.bangPres, simp_all)
    next
      case(BRPar P Q R T)
      have PBiSimQ: "P ≈ Q" by fact
      have RBangRelT: "(R, T) ∈ ?X" by fact
      have RSimT: "R ↝⇧^<?Y> T" by fact
      moreover from PBiSimQ  have "P ↝⇧^<weakBisim> Q" by(blast dest: unfoldE)
      moreover from RBangRelT have "(R, T) ∈ ?Y" by(blast intro: Strong_Late_Bisim.reflexive)
      ultimately show "P ∥ R ↝⇧^<?Y> Q ∥ T" using ParCompose ResCong eqvt eqvtY ‹P ≈ Q›
        by(rule_tac Weak_Late_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_Late_Sim_Pres.resPres, simp_all)
    qed
  next
    case(cSym P Q)
    thus ?case by(metis symmetric bangRelSymetric)
  qed
qed

end