Theory Strong_Late_Bisim_Subst_SC

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

lemma matchId:
  fixes a :: name
  and   P :: pi

  shows "[a⌢a]P ∼⇧s P"
by(auto simp add: substClosed_def intro: Strong_Late_Bisim_SC.matchId)

lemma mismatchNil:
  fixes a :: name
  and   P :: pi
  
  shows "[a≠a]P ∼⇧s 𝟬"
by(auto simp add: substClosed_def intro: Strong_Late_Bisim_SC.mismatchNil)

lemma scopeFresh:
  fixes P :: pi
  and   x :: name

  assumes xFreshP: "x ♯ P"

  shows "<νx>P ∼⇧s P"
proof(auto simp add: substClosed_def)
  fix s :: "(name × name) list"

  have "∃c::name. c ♯ (P, s)" by(blast intro: name_exists_fresh)
  then obtain c::name where cFreshP: "c ♯ P" and cFreshs: "c ♯ s" by(force simp add: fresh_prod)

  have "<νx>P = <νc>P"
  proof -
    from cFreshP have "<νx>P = <νc>([(x, c)] ∙ P)" by(simp add: alphaRes)
    with cFreshP xFreshP show ?thesis by(simp add: name_fresh_fresh)
  qed

  with cFreshP cFreshs show "(<νx>P)[<s>] ∼ P[<s>]"
    by(force intro: Strong_Late_Bisim_SC.scopeFresh)
qed

lemma resComm:
  fixes P :: pi
  and   x :: name
  and   y :: name

  shows "<νx><νy>P ∼⇧s <νy><νx>P"
proof(cases "x=y")
  assume xeqy: "x=y"
  have "P ∼⇧s P" by(rule Strong_Late_Bisim_Subst.reflexive)
  hence "<νx>P ∼⇧s <νx>P" by(rule resPres)
  hence "<νx><νx>P ∼⇧s <νx><νx>P" by(rule resPres)
  with xeqy show ?thesis by simp
next
  assume xineqy: "x ≠ y"
  show ?thesis
  proof(auto simp add: substClosed_def)
    fix s::"(name × name) list"
    
    have "∃c::name. c ♯ (P, s, y)" by(blast intro: name_exists_fresh)
    then obtain c::name where cFreshP: "c ♯ P" and cFreshs: "c ♯ s" and cineqy: "c ≠ y"
      by(force simp add: fresh_prod)
    
    have "∃d::name. d ♯ (P, s, c, x, y)" by (blast intro: name_exists_fresh)
    then obtain d::name where dFreshP: "d ♯ P" and dFreshs: "d ♯ s" and dineqc: "d ≠ c"
                          and dineqx: "d ≠ x" and dineqy: "d ≠ y"
      by(force simp add: fresh_prod)

    have "<νx><νy>P = <νc><νd>([(x, c)] ∙ [(y, d)] ∙ P)"
    proof -
      from cineqy cFreshP have cFreshyP: "c ♯ <νy>P" by(simp add: name_fresh_abs)
      from dFreshP have "<νy>P = <νd>([(y, d)] ∙ P)" by(rule alphaRes)
      moreover from cFreshyP have "<νx><νy>P = <νc>([(x, c)] ∙ (<νy>P))" by(rule alphaRes)
      ultimately show ?thesis using dineqc dineqx by(simp add: name_calc)
    qed
    moreover have "<νy><νx>P = <νd><νc>([(x, c)] ∙ [(y, d)] ∙ P)"
    proof -
      from dineqx dFreshP have dFreshxP: "d ♯ <νx>P" by(simp add: name_fresh_abs)
      from cFreshP have "<νx>P = <νc>([(x, c)] ∙ P)" by(rule alphaRes)
      moreover from dFreshxP have "<νy><νx>P = <νd>([(y, d)] ∙ (<νx>P))" by(rule alphaRes)
      ultimately have "<νy><νx>P = <νd><νc>([(y, d)] ∙ [(x, c)] ∙ P)" using dineqc cineqy
        by(simp add: name_calc)
      thus ?thesis using dineqx dineqc cineqy xineqy
        by(subst name_perm_compose, simp add: name_calc)
    qed

    ultimately show "(<νx><νy>P)[<s>] ∼ (<νy><νx>P)[<s>]" using cFreshs dFreshs
      by(force intro: Strong_Late_Bisim_SC.resComm)
  qed
qed

lemma sumZero:
  fixes P :: pi
  
  shows "P ⊕ 𝟬 ∼⇧s P"
by(force simp add: substClosed_def intro: Strong_Late_Bisim_SC.sumZero)
    
lemma sumSym:
  fixes P :: pi
  and   Q :: pi

  shows "P ⊕ Q ∼⇧s Q ⊕ P"
by(force simp add: substClosed_def intro: Strong_Late_Bisim_SC.sumSym)

lemma sumAssoc:
  fixes P :: pi
  and   Q :: pi
  and   R :: pi
  
  shows "(P ⊕ Q) ⊕ R ∼⇧s P ⊕ (Q ⊕ R)"
by(force simp add: substClosed_def intro: Strong_Late_Bisim_SC.sumAssoc)

lemma sumRes:
  fixes P :: pi
  and   Q :: pi
  and   x :: name

  shows "<νx>(P ⊕ Q) ∼⇧s <νx>P ⊕ <νx>Q"
proof(auto simp add: substClosed_def)
  fix s :: "(name × name) list"

  have "∃c::name. c ♯ (P, Q, s)" by(blast intro: name_exists_fresh)
  then obtain c::name where cFreshP: "c ♯ P" and cFreshQ: "c ♯ Q" and cFreshs: "c ♯ s"
    by(force simp add: fresh_prod)

  have "<νx>(P ⊕ Q) = <νc>(([(x, c)] ∙ P) ⊕ ([(x, c)] ∙ Q))"
  proof -
    from cFreshP cFreshQ have "c ♯ P ⊕ Q" by simp
    hence "<νx>(P ⊕ Q) = <νc>([(x, c)] ∙ (P ⊕ Q))" by(simp add: alphaRes)
    thus ?thesis by(simp add: name_fresh_fresh)
  qed

  moreover from cFreshP have "<νx>P = <νc>([(x, c)] ∙ P)" by(simp add: alphaRes)
  moreover from cFreshQ have "<νx>Q = <νc>([(x, c)] ∙ Q)" by(simp add: alphaRes)
  
  ultimately show "(<νx>(P ⊕ Q))[<s>] ∼ (<νx>P)[<s>] ⊕ (<νx>Q)[<s>]" using cFreshs
    by(force intro: Strong_Late_Bisim_SC.sumRes)
qed

lemma scopeExtSum:
  fixes P :: pi
  and   Q :: pi
  and   x :: name

  assumes xFreshP: "x ♯ P"

  shows "<νx>(P ⊕ Q) ∼⇧s P ⊕ <νx>Q"
proof(auto simp add: substClosed_def)
  fix s :: "(name × name) list"

  have "∃c::name. c ♯ (P, Q, s)" by(blast intro: name_exists_fresh)
  then obtain c::name where cFreshP: "c ♯ P" and cFreshQ: "c ♯ Q" and cFreshs: "c ♯ s"
    by(force simp add: fresh_prod)

  have "<νx>(P ⊕ Q) = <νc>(P ⊕ ([(x, c)] ∙ Q))"
  proof -
    from cFreshP cFreshQ have "c ♯ P ⊕ Q" by simp
    hence "<νx>(P ⊕ Q) = <νc>([(x, c)] ∙ (P ⊕ Q))" by(simp add: alphaRes)
    with xFreshP cFreshP show ?thesis by(simp add: name_fresh_fresh)
  qed

  moreover from cFreshQ have "<νx>Q = <νc>([(x, c)] ∙ Q)" by(simp add: alphaRes)
  
  ultimately show "(<νx>(P ⊕ Q))[<s>] ∼ P[<s>] ⊕ (<νx>Q)[<s>]" using cFreshs cFreshP
    by(force intro: Strong_Late_Bisim_SC.scopeExtSum)
qed

lemma parZero:
  fixes P :: pi
  
  shows "P ∥ 𝟬 ∼⇧s P"
by(force simp add: substClosed_def intro: Strong_Late_Bisim_SC.parZero)

lemma parSym:
  fixes P :: pi
  and   Q :: pi

  shows "P ∥ Q ∼⇧s Q ∥ P"
by(force simp add: substClosed_def intro: Strong_Late_Bisim_SC.parSym)

lemma parAssoc:
  fixes P :: pi
  and   Q :: pi
  and   R :: pi
  
  shows "(P ∥ Q) ∥ R ∼⇧s P ∥ (Q ∥ R)"
  by(force simp add: substClosed_def intro: Strong_Late_Bisim_SC.parAssoc)

lemma scopeExtPar:
  fixes P :: pi
  and   Q :: pi
  and   x :: name

  assumes xFreshP: "x ♯ P"

  shows "<νx>(P ∥ Q) ∼⇧s P ∥ <νx>Q"
proof(auto simp add: substClosed_def)
  fix s :: "(name × name) list"

  have "∃c::name. c ♯ (P, Q, s)" by(blast intro: name_exists_fresh)
  then obtain c::name where cFreshP: "c ♯ P" and cFreshQ: "c ♯ Q" and cFreshs: "c ♯ s"
    by(force simp add: fresh_prod)

  have "<νx>(P ∥ Q) = <νc>(P ∥ ([(x, c)] ∙ Q))"
  proof -
    from cFreshP cFreshQ have "c ♯ P ∥ Q" by simp
    hence "<νx>(P ∥ Q) = <νc>([(x, c)] ∙ (P ∥ Q))" by(simp add: alphaRes)
    with xFreshP cFreshP show ?thesis by(simp add: name_fresh_fresh)
  qed

  moreover from cFreshQ have "<νx>Q = <νc>([(x, c)] ∙ Q)" by(simp add: alphaRes)
  
  ultimately show "(<νx>(P ∥ Q))[<s>] ∼ P[<s>] ∥ (<νx>Q)[<s>]" using cFreshs cFreshP
    by(force intro: Strong_Late_Bisim_SC.scopeExtPar)
qed

lemma scopeExtPar':
  fixes P :: pi
  and   Q :: pi
  and   x :: name

  assumes xFreshP: "x ♯ Q"

  shows "<νx>(P ∥ Q) ∼⇧s (<νx>P) ∥ Q"
proof -
  have "<νx>(P ∥ Q) ∼⇧s <νx>(Q ∥ P)" by(blast intro: parSym resPres)
  moreover from xFreshP have "<νx>(Q ∥ P) ∼⇧s Q ∥ <νx>P" by(rule scopeExtPar)
  moreover have "Q ∥ <νx>P ∼⇧s (<νx>P) ∥ Q" by(rule parSym)
  ultimately show ?thesis by (blast intro: transitive)
qed

lemma bangSC:
  fixes P :: pi

  shows "!P ∼⇧s P ∥ !P"
by(auto simp add: substClosed_def intro: Strong_Late_Bisim_SC.bangSC)

lemma nilRes:
  fixes x :: name
  
  shows "<νx>𝟬 ∼⇧s 𝟬"
proof(auto simp add: substClosed_def)
  fix σ::"(name × name) list"
  obtain y::name where "y ♯ σ"
    by(generate_fresh "name") auto
  have "<νy>𝟬 ∼ 𝟬" by (rule Strong_Late_Bisim_SC.nilRes)
  with ‹y ♯ σ› have "(<νy>𝟬)[<σ>] ∼ 𝟬" by simp
  thus "(<νx>𝟬)[<σ>] ∼ 𝟬"
    by(subst alphaRes[where c=y]) auto
qed

lemma resTau:
  fixes x :: name
  and   P :: pi

  shows "<νx>(τ.(P)) ∼⇧s τ.(<νx>P)"
proof(auto simp add: substClosed_def)
  fix σ::"(name × name) list"
  obtain y::name where "y ♯ P" and "y ♯ σ"
    by(generate_fresh "name", auto)
  have "<νy>(τ.(([(x, y)] ∙ P)[<σ>])) ∼ τ.(<νy>(([(x, y)] ∙ P)[<σ>]))"
    by(rule resTau)
  with ‹y ♯ σ› have "(<νy>(τ.([(x, y)] ∙ P)))[<σ>] ∼ (τ.(<νy>([(x, y)] ∙ P)))[<σ>]"
    by simp
  with ‹y ♯ P› show "(<νx>τ.(P))[<σ>] ∼ τ.((<νx>P)[<σ>])"
    apply(subst alphaRes[where c=y])
    apply simp
    apply(subst alphaRes[where c=y and a=x])
    by simp+
qed

lemma resOutput:
  fixes x :: name
  and   a :: name
  and   b :: name
  and   P :: pi

  assumes "x ≠ a"
  and     "x ≠ b"

  shows "<νx>(a{b}.(P)) ∼⇧s a{b}.(<νx>P)"
proof(auto simp add: substClosed_def)
  fix σ::"(name × name) list"
  obtain y::name where "y ♯ P" and "y ♯ σ" and "y ≠ a" and "y ≠ b"
    by(generate_fresh "name", auto)
  have "<νy>((seq_subst_name a σ){seq_subst_name b σ}.(([(x, y)] ∙ P)[<σ>])) ∼ seq_subst_name a σ{seq_subst_name b σ}.(<νy>(([(x, y)] ∙ P)[<σ>]))"
    using ‹y ≠ a› ‹y ≠ b› ‹y ♯ σ› freshSeqSubstName
    by(rule_tac resOutput) auto
  with ‹y ♯ σ› have "(<νy>(a{b}.([(x, y)] ∙ P)))[<σ>] ∼ (a{b}.(<νy>([(x, y)] ∙ P)))[<σ>]"
    by simp
  with ‹y ♯ P› ‹y ≠ a› ‹y ≠ b› ‹x ≠ a› ‹x ≠ b› show "(<νx>a{b}.(P))[<σ>] ∼ seq_subst_name a σ{seq_subst_name b σ}.((<νx>P)[<σ>])"
    apply(subst alphaRes[where c=y])
    apply simp
    apply(subst alphaRes[where c=y and a=x])
    by simp+
qed

lemma resInput:
  fixes x :: name
  and   a :: name
  and   b :: name
  and   P :: pi

  assumes "x ≠ a"
  and     "x ≠ y"

  shows "<νx>(a<y>.(P)) ∼⇧s a<y>.(<νx>P)"
proof(auto simp add: substClosed_def)
  fix σ::"(name × name) list"
  obtain x'::name where "x' ♯ P" and "x' ♯ σ" and "x' ≠ a" and "x' ≠ x" and "x' ≠ y"
    by(generate_fresh "name", auto)
  obtain y'::name where "y' ♯ P" and "y' ♯ σ" and "y' ≠ a" and "y' ≠ x" and "y' ≠ y" and "x' ≠ y'"
    by(generate_fresh "name", auto)
  have "<νx'>((seq_subst_name a σ)<y'>.(([(y, y')] ∙ [(x, x')] ∙ P)[<σ>])) ∼ seq_subst_name a σ<y'>.(<νx'>(([(y, y')] ∙ [(x, x')] ∙ P)[<σ>]))"
    using ‹x' ≠ a› ‹x' ≠ y'› ‹x' ♯ σ› ‹y' ♯ σ› freshSeqSubstName
    by(rule_tac resInput) auto
  with ‹x' ♯ σ› ‹y' ♯ σ› have "(<νx'>(a<y'>.([(y, y')] ∙ [(x, x')] ∙ P)))[<σ>] ∼ (a<y'>.(<νx'>([(y, y')] ∙ [(x, x')] ∙ P)))[<σ>]"
    by simp
  with ‹x' ♯ P› ‹y' ≠ x› ‹x' ≠ y› ‹y' ♯ P› ‹x' ≠ y'› ‹x' ≠ a› ‹y' ≠ a› ‹x ≠ a› ‹x ≠ y› show "(<νx>a<y>.(P))[<σ>] ∼ a<y>.(<νx>P)[<σ>]"
    apply(subst alphaInput[where c=y'])
    apply simp
    apply(subst alphaRes[where c=x'])
    apply(simp add: abs_fresh fresh_left calc_atm)
    apply(simp add: eqvts calc_atm)
    apply(subst alphaRes[where c=x' and a=x])
    apply simp
    apply(subst alphaInput[where c=y' and x=y])
    apply(simp add: abs_fresh fresh_left calc_atm)
    apply(simp add: eqvts calc_atm)
    apply(subst perm_compose)
    by(simp add: eqvts calc_atm)
qed

lemma bisimSubstStructCong:
  fixes P :: pi
  and   Q :: pi

  assumes "P ≡⇩s Q"
  shows "P ∼⇧s Q"

using assms
apply(induct rule: structCong.induct)
by(auto intro: reflexive symmetric transitive sumSym sumAssoc sumZero parSym parAssoc parZero
               nilRes resComm resInput resOutput resTau sumRes scopeExtPar bangSC matchId mismatchId)


end