Theory Strong_Late_Sim_Pres

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

lemma tauPres:
  fixes P    :: pi
  and   Q    :: pi
  and   Rel  :: "(pi × pi) set"
  and   Rel' :: "(pi × pi) set"

  assumes PRelQ: "(P, Q) ∈ Rel"

  shows "τ.(P) ↝[Rel] τ.(Q)"
proof -
  show "τ.(P) ↝[Rel] τ.(Q)"
  proof(induct rule: simCases)
    case(Bound a x Q')
    have "τ.(Q) ⟼ a«x» ≺ Q'" by fact
    hence False by auto
    thus ?case by simp
  next
    case(Free α Q')
    have "τ.(Q) ⟼ α ≺ Q'" by fact
    thus ?case
    proof(induct rule: tauCases)
      case cTau
      have "τ.(P) ⟼ τ ≺ P" by(rule Late_Semantics.Tau)
      with PRelQ show ?case by blast
    qed
  qed
qed

lemma inputPres:
  fixes P    :: pi
  and   x    :: name
  and   Q    :: pi
  and   a    :: name
  and   Rel  :: "(pi × pi) set"

  assumes PRelQ: "∀y. (P[x::=y], Q[x::=y]) ∈ Rel"
  and     Eqvt: "eqvt Rel"

  shows "a<x>.P ↝[Rel] a<x>.Q"
using Eqvt
proof(induct rule: simCasesCont[where C="(x, a, P, Q)"])
  case(Bound b y Q')
  from ‹y ♯ (x, a, P, Q)› have "y ≠ x" "y ≠ a" "y ♯ P" "y ♯ Q" by simp+
  from ‹a<x>.Q ⟼b«y» ≺ Q'› ‹y ≠ a› ‹y ≠ x› ‹y ♯ Q› show ?case
  proof(induct rule: inputCases)
    case cInput
    
    have "a<x>.P ⟼ a<x> ≺ P" by(rule Input) 
    hence "a<x>.P ⟼ a<y> ≺ ([(x, y)] ∙ P)" using ‹y ♯ P›
      by(simp add: alphaBoundResidual)

    moreover have "derivative ([(x, y)] ∙ P) ([(x, y)] ∙ Q) (InputS a) y Rel"
    proof(auto simp add: derivative_def)
      fix u
      show "(([(x, y)] ∙ P)[y::=u], ([(x, y)] ∙ Q)[y::=u]) ∈ Rel"
      proof(cases "y=u")
        assume "y = u"
        moreover have "([(y, x)] ∙ P, [(y, x)] ∙ Q) ∈ Rel"
        proof -
          from PRelQ have "(P[x::=x], Q[x::=x]) ∈ Rel" by blast
          hence "(P, Q) ∈ Rel" by simp
          with Eqvt show ?thesis by(rule eqvtRelI)
        qed
        ultimately show ?thesis by simp
      next
        assume yinequ: "y ≠ u"
        show ?thesis
        proof(cases "x = u")
          assume "x = u"
          moreover have "(([(y, x)] ∙ P)[y::=x], ([(y, x)] ∙ Q)[y::=x]) ∈ Rel"
          proof -
            from PRelQ have "(P[x::=y], Q[x::=y]) ∈ Rel" by blast
            with Eqvt have "([(y, x)] ∙ (P[x::=y]), [(y, x)] ∙ (Q[x::=y])) ∈ Rel"
              by(rule eqvtRelI)
            with ‹y ≠ x› show ?thesis
              by(simp add: eqvt_subs name_calc)
          qed
          ultimately show ?thesis by simp
        next
          assume xinequ: "x ≠ u"
          hence "(([(y, x)] ∙ P)[y::=u], ([(y, x)] ∙ Q)[y::=u]) ∈ Rel"
          proof -
            from PRelQ have "(P[x::=u], Q[x::=u]) ∈ Rel" by blast
            with Eqvt have "([(y, x)] ∙ (P[x::=u]), [(y, x)] ∙ (Q[x::=u])) ∈ Rel"
              by(rule eqvtRelI)
            with ‹y ≠ x›  xinequ yinequ show ?thesis
              by(simp add: eqvt_subs name_calc)
          qed
          thus ?thesis by simp
        qed
      qed
    qed
    
    ultimately show ?case by blast
  qed
next
  case(Free α Q')
  have "a<x>.Q ⟼ α ≺ Q'" by fact
  hence False by auto
  thus ?case by blast
qed

lemma outputPres:
  fixes P    :: pi
  and   Q    :: pi
  and   a    :: name
  and   b    :: name
  and   Rel  :: "(pi × pi) set"
  and   Rel' :: "(pi × pi) set"

  assumes PRelQ: "(P, Q) ∈ Rel"

  shows "a{b}.P ↝[Rel] a{b}.Q"
proof -
  show ?thesis
  proof(induct rule: simCases)
    case(Bound c x Q')
    have "a{b}.Q ⟼ c«x» ≺ Q'" by fact
    hence False by auto
    thus ?case by simp
  next
    case(Free α Q')
    have "a{b}.Q ⟼ α ≺ Q'" by fact
    thus ?case
    proof(induct rule: outputCases)
      case cOutput
      have "a{b}.P ⟼ a[b] ≺ P" by(rule Late_Semantics.Output)
      with PRelQ show ?case by blast
    qed
  qed
qed

lemma matchPres:
  fixes P    :: pi
  and   Q    :: pi
  and   a    :: name
  and   b    :: name
  and   Rel  :: "(pi × pi) set"
  and   Rel' :: "(pi × pi) set"

  assumes PSimQ: "P ↝[Rel] Q"
  and     "Rel ⊆ Rel'"

  shows "[a⌢b]P ↝[Rel'] [a⌢b]Q"
proof -
  show ?thesis
  proof(induct rule: simCases)
    case(Bound c x Q')
    have "x ♯  [a⌢b]P" by fact
    hence xFreshP: "x ♯ P" by simp
    have "[a⌢b]Q ⟼ c«x» ≺ Q'" by fact
    thus ?case
    proof(induct rule: matchCases)
      case cMatch
      have "Q ⟼c«x» ≺ Q'" by fact
      with PSimQ xFreshP obtain P' where PTrans: "P ⟼c«x» ≺ P'"
                                     and Pderivative: "derivative P' Q' c x Rel"
        by(blast dest: simE)

      from PTrans have "[a⌢a]P ⟼ c«x» ≺ P'" by(rule Late_Semantics.Match)
      moreover from Pderivative ‹Rel ⊆ Rel'› have "derivative P' Q' c x Rel'"
        by(cases c) (auto simp add: derivative_def)
      ultimately show ?case by blast
    qed
  next
    case(Free α Q')
    have "[a⌢b]Q ⟼α ≺ Q'" by fact
    thus ?case
    proof(induct rule: matchCases)
      case cMatch
      have "Q ⟼ α ≺ Q'" by fact
      with PSimQ obtain P' where PTrans: "P ⟼ α ≺ P'"
                             and PRel: "(P', Q') ∈ Rel"
          by(blast dest: simE)
      from PTrans have "[a⌢a]P ⟼α ≺ P'" by(rule Late_Semantics.Match)
      with PRel ‹Rel ⊆ Rel'› show ?case by blast
    qed
  qed
qed

lemma mismatchPres:
  fixes P    :: pi
  and   Q    :: pi
  and   a    :: name
  and   b    :: name
  and   Rel  :: "(pi × pi) set"
  and   Rel' :: "(pi × pi) set"

  assumes PSimQ: "P ↝[Rel] Q"
  and     "Rel ⊆ Rel'"

  shows "[a≠b]P ↝[Rel'] [a≠b]Q"
proof(induct rule: simCases)
  case(Bound c x Q')
  have "x ♯ [a≠b]P" by fact
  hence xFreshP: "x ♯ P" by simp
  from ‹[a≠b]Q ⟼ c«x» ≺ Q'› show ?case
  proof(induct rule: mismatchCases)
    case cMismatch
    have "Q ⟼c«x» ≺ Q'" by fact
    with PSimQ xFreshP obtain P' where PTrans: "P ⟼c«x» ≺ P'"
                                   and Pderivative: "derivative P' Q' c x Rel"
      by(blast dest: simE)

    from PTrans ‹a ≠ b› have "[a≠b]P ⟼ c«x» ≺ P'" by(rule Late_Semantics.Mismatch)
    moreover from Pderivative ‹Rel ⊆ Rel'› have "derivative P' Q' c x Rel'"
      by(cases c) (auto simp add: derivative_def)
    ultimately show ?case by blast
  qed
next
  case(Free α Q')
  have "[a≠b]Q ⟼α ≺ Q'" by fact
  thus ?case
  proof(induct rule: mismatchCases)
    case cMismatch
    have "Q ⟼ α ≺ Q'" by fact
    with PSimQ obtain P' where PTrans: "P ⟼ α ≺ P'"
                           and PRel: "(P', Q') ∈ Rel"
      by(blast dest: simE)
    from PTrans ‹a ≠ b› have "[a≠b]P ⟼α ≺ P'" by(rule Late_Semantics.Mismatch)
    with PRel ‹Rel ⊆ Rel'› show ?case by blast
  qed
qed

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

  assumes PSimQ: "P ↝[Rel] Q"
  and     "Id ⊆ Rel'"
  and     "Rel ⊆ Rel'"

  shows "P ⊕ R ↝[Rel'] Q ⊕ R"
proof -
  show ?thesis
  proof(induct rule: simCases)
    case(Bound a x QR)
    have "x ♯ P ⊕ R" by fact
    hence xFreshP: "x ♯ P" and xFreshR: "x ♯ R" by simp+
    have "Q ⊕ R ⟼a«x» ≺ QR" by fact
    thus ?case
    proof(induct rule: sumCases)
      case cSum1
      have "Q ⟼a«x» ≺ QR" by fact
      with xFreshP PSimQ obtain P' where PTrans: "P ⟼a«x» ≺ P'"
                                     and Pderivative: "derivative P' QR a x Rel"
        by(blast dest: simE)

      from PTrans have "P ⊕ R ⟼a«x» ≺ P'" by(rule Late_Semantics.Sum1)
      moreover from Pderivative ‹Rel ⊆ Rel'› have "derivative P' QR a x Rel'"
        by(cases a) (auto simp add: derivative_def)
      ultimately show ?case by blast
    next
      case cSum2
      from ‹R ⟼a«x» ≺ QR› have "P ⊕ R ⟼a«x» ≺ QR" by(rule Sum2)
      thus ?case using ‹Id ⊆ Rel'› by(blast intro: derivativeReflexive)
    qed
  next
    case(Free α QR)
    have "Q ⊕ R ⟼α ≺ QR" by fact
    thus ?case
    proof(induct rule: sumCases)
      case cSum1
      have "Q ⟼α ≺ QR" by fact
      with PSimQ obtain P' where PTrans: "P ⟼α ≺ P'" and PRel: "(P', QR) ∈ Rel" 
        by(blast dest: simE)
      from PTrans have "P ⊕ R ⟼α ≺ P'" by(rule Late_Semantics.Sum1)
      with PRel ‹Rel ⊆ Rel'› show ?case by blast
    next
      case cSum2
      from ‹R ⟼α ≺ QR› have "P ⊕ R ⟼α ≺ QR" by(rule Sum2)
      thus ?case using ‹Id ⊆ Rel'› by(blast intro: derivativeReflexive)
    qed
  qed
qed
      
lemma parCompose:
  fixes P     :: pi
  and   Q     :: pi
  and   R     :: pi
  and   T     :: pi
  and   Rel   :: "(pi × pi) set"
  and   Rel'  :: "(pi × pi) set"
  and   Rel'' :: "(pi × pi) set"
  
  assumes PSimQ:    "P ↝[Rel] Q"
  and     RSimT:    "R ↝[Rel'] T"
  and     PRelQ:    "(P, Q) ∈ Rel"
  and     RRel'T:   "(R, T) ∈ Rel'"
  and     Par:      "⋀P Q R T. ⟦(P, Q) ∈ Rel; (R, T) ∈ Rel'⟧ ⟹ (P ∥ R, Q ∥ T) ∈ Rel''"
  and     Res:      "⋀P Q a. (P, Q) ∈ Rel'' ⟹ (<νa>P, <νa>Q) ∈ Rel''"
  and     EqvtRel:  "eqvt Rel"
  and     EqvtRel': "eqvt Rel'"
  and     EqvtRel'': "eqvt Rel''"

  shows "P ∥ R ↝[Rel''] Q ∥ T"
using EqvtRel''
proof(induct rule: simCasesCont[where C="()"])
  case(Bound a x Q')
  have "x ♯ P ∥ R" and "x ♯ Q ∥ T" by fact+
  hence xFreshP: "x ♯ P" and xFreshR: "x ♯ R" and "x ♯ Q" and "x ♯ T" by simp+
  have QTTrans: "Q ∥ T ⟼ a«x» ≺ Q'" by fact
  thus ?case using ‹x ♯ Q› ‹x ♯ T›
  proof(induct rule: parCasesB)
    case(cPar1 Q')
    have QTrans: "Q ⟼ a«x» ≺ Q'" and xFreshT: "x ♯ T" by fact+
      
    from xFreshP PSimQ QTrans obtain P' where PTrans:"P ⟼ a«x» ≺ P'"
                                          and Pderivative: "derivative P' Q' a x Rel"
      by(blast dest: simE)
    from PTrans xFreshR have "P ∥ R ⟼ a«x» ≺ P' ∥ R" by(rule Late_Semantics.Par1B)
    moreover from Pderivative xFreshR xFreshT RRel'T have "derivative (P' ∥ R) (Q' ∥ T) a x Rel''"
      by(cases a, auto intro: Par simp add: derivative_def forget)
    ultimately show ?case by blast
  next
    case(cPar2 T')
    have TTrans: "T ⟼ a«x» ≺ T'" and xFreshQ: "x ♯ Q" by fact+
    
    from xFreshR RSimT TTrans obtain R' where RTrans:"R ⟼ a«x» ≺ R'"
                                          and Rderivative: "derivative R' T' a x Rel'"
      by(blast dest: simE)
    from RTrans xFreshP have ParTrans: "P ∥ R ⟼ a«x» ≺ P ∥ R'" by(rule Late_Semantics.Par2B)      
    moreover from Rderivative xFreshP xFreshQ PRelQ have "derivative (P ∥ R') (Q ∥  T') a x Rel''"
      by(cases a, auto intro: Par simp add: derivative_def forget)
    ultimately show ?case by blast
  qed
next
  case(Free α QT')
  have QTTrans: "Q ∥ T ⟼ α ≺ QT'" by fact
  thus ?case using PSimQ RSimT PRelQ RRel'T
  proof(induct rule: parCasesF[where C="(P, R)"])
    case(cPar1 Q')
    have RRel'T: "(R, T) ∈ Rel'" by fact
    have "P ↝[Rel] Q" and "Q ⟼ α ≺ Q'" by fact+
    then obtain P' where PTrans: "P ⟼ α ≺ P'" and PRel: "(P', Q') ∈ Rel"
      by(blast dest: simE)
    from PTrans have Trans: "P ∥ R ⟼ α ≺ P' ∥ R" by(rule Late_Semantics.Par1F)
    moreover from PRel RRel'T have "(P' ∥ R, Q' ∥ T) ∈ Rel''" by(blast intro: Par)
    ultimately show ?case by blast
  next
    case(cPar2 T')
    have PRelQ: "(P, Q) ∈ Rel" by fact
    have "R ↝[Rel'] T" and "T ⟼ α ≺ T'" by fact+
    then obtain R' where RTrans: "R ⟼ α ≺ R'" and RRel: "(R', T') ∈ Rel'"
      by(blast dest: simE)
    from RTrans have Trans: "P ∥ R ⟼ α ≺ P ∥ R'" by(rule Late_Semantics.Par2F)
    moreover from PRelQ RRel have "(P ∥ R', Q ∥ T') ∈ Rel''" by(blast intro: Par)
    ultimately show ?case by blast
  next
    case(cComm1 Q' T' a b x)
    from ‹x ♯ (P, R)› have "x ♯ P" by simp
    with ‹P ↝[Rel] Q› ‹Q ⟼ a<x> ≺ Q'› ‹x ♯ P›
    obtain P' where PTrans: "P ⟼a<x> ≺ P'" 
                and Pderivative: "derivative P' Q' (InputS a) x Rel"
      by(blast dest: simE)
    from Pderivative have PRel: "(P'[x::=b], Q'[x::=b]) ∈ Rel" by(simp add: derivative_def)
      
    have "R ↝[Rel'] T" and "T ⟼ a[b] ≺ T'" by fact+
    then obtain R' where RTrans: "R ⟼a[b] ≺ R'" and RRel: "(R', T') ∈ Rel'"
      by(blast dest: simE)
      
    from PTrans RTrans have "P ∥ R ⟼ τ ≺ P'[x::=b] ∥ R'" by(rule Late_Semantics.Comm1)
    moreover from PRel RRel have "(P'[x::=b] ∥ R', Q'[x::=b] ∥ T') ∈ Rel''" by(blast intro: Par)
    ultimately show ?case by blast
  next
    case(cComm2 Q' T' a b x)
    have "P ↝[Rel] Q" and "Q ⟼a[b] ≺ Q'" by fact+
    then obtain P' where PTrans: "P ⟼a[b] ≺ P'" and PRel: "(P', Q') ∈ Rel"
      by(blast dest: simE)
    
    from ‹x ♯ (P, R)› have "x ♯ R" by simp
    with ‹R ↝[Rel'] T› ‹T ⟼a<x> ≺ T'›
    obtain R' where RTrans: "R ⟼a<x> ≺ R'"
                and Rderivative: "derivative R' T' (InputS a) x Rel'"
      by(blast dest: simE)
    from Rderivative have RRel: "(R'[x::=b], T'[x::=b]) ∈ Rel'" by(simp add: derivative_def)
      
    from PTrans RTrans have "P ∥ R ⟼ τ ≺ P' ∥ R'[x::=b]" by(rule Late_Semantics.Comm2)
    moreover from PRel RRel have "(P' ∥ R'[x::=b], Q' ∥ T'[x::=b]) ∈ Rel''" by(blast intro: Par)
    ultimately show "∃P'. P ∥ R ⟼ τ ≺ P' ∧ (P', Q' ∥ T'[x::=b]) ∈ Rel''" by blast
  next
    case(cClose1 Q' T' a x y)
    from ‹x ♯ (P, R)› have "x ♯ P" by simp
    with ‹P ↝[Rel] Q› ‹Q ⟼a<x> ≺ Q'›
    obtain P' where PTrans: "P ⟼a<x> ≺ P'"
                and Pderivative: "derivative P' Q' (InputS a) x Rel"
      by(blast dest: simE)
    from Pderivative have PRel: "(P'[x::=y], Q'[x::=y]) ∈ Rel" by(simp add: derivative_def)
      
    from ‹y ♯ (P, R)› have "y ♯ R" and "y ♯ P" by simp+
    from ‹R ↝[Rel'] T› ‹T ⟼a<νy> ≺ T'› ‹y ♯ R›
    obtain R' where RTrans: "R ⟼a<νy> ≺ R'"
                and Rderivative: "derivative R' T' (BoundOutputS a) y Rel'"
      by(blast dest: simE)
    from Rderivative have RRel: "(R', T') ∈ Rel'" by(simp add: derivative_def)
    
    from PTrans RTrans ‹y ♯ P› have Trans: "P ∥ R ⟼ τ ≺ <νy>(P'[x::=y] ∥ R')"
      by(rule Late_Semantics.Close1)
    moreover from PRel RRel have "(<νy>(P'[x::=y] ∥ R'), <νy>(Q'[x::=y] ∥ T')) ∈ Rel''"
      by(blast intro: Par Res)
    ultimately show ?case by blast
  next
    case(cClose2 Q' T' a x y)
    from ‹y ♯ (P, R)› have "y ♯ P" and "y ♯ R" by simp+
    from ‹P ↝[Rel] Q› ‹Q ⟼a<νy> ≺ Q'› ‹y ♯ P›
    obtain P' where PTrans: "P ⟼a<νy> ≺ P'" and P'RelQ': "(P', Q') ∈ Rel"
      by(force dest: simE simp add: derivative_def)
    
    from ‹x ♯ (P, R)› have "x ♯ R" by simp+
    with ‹R ↝[Rel'] T› ‹T ⟼a<x> ≺ T'›
    obtain R' where RTrans: "R ⟼a<x> ≺ R'"
                and R'Rel'T': "(R'[x::=y], T'[x::=y]) ∈ Rel'" 
      by(force dest: simE simp add: derivative_def)
      
    from PTrans RTrans ‹y ♯ R› have Trans: "P ∥ R ⟼ τ ≺ <νy>(P' ∥ R'[x::=y])"
      by(rule Close2)
    moreover from P'RelQ' R'Rel'T' have "(<νy>(P' ∥ R'[x::=y]), <νy>(Q' ∥ T'[x::=y])) ∈ Rel''"
      by(blast intro: Par Res)
    ultimately show ?case by blast
  qed
qed

lemma parPres:
  fixes P   :: pi
  and   Q   :: pi
  and   R   :: pi
  and   a   :: name
  and   b   :: name
  and   Rel :: "(pi × pi) set"
  and   Rel' :: "(pi × pi) set"
  
  assumes PSimQ:    "P ↝[Rel] Q"
  and     PRelQ:    "(P, Q) ∈ Rel"
  and     Par:      "⋀P Q R. (P, Q) ∈ Rel ⟹ (P ∥ R, Q ∥ R) ∈ Rel'"
  and     Res:      "⋀P Q a. (P, Q) ∈ Rel' ⟹ (<νa>P, <νa>Q) ∈ Rel'"
  and     EqvtRel:  "eqvt Rel"
  and     EqvtRel': "eqvt Rel'"

  shows "P ∥ R ↝[Rel'] Q ∥ R"
proof -
  note PSimQ 
  moreover have RSimR: "R ↝[Id] R" by(auto intro: reflexive)
  moreover note PRelQ moreover have "(R, R) ∈ Id" by auto
  moreover from Par have "⋀P Q R T. ⟦(P, Q) ∈ Rel; (R, T) ∈ Id⟧ ⟹ (P ∥ R, Q ∥ T) ∈ Rel'"
    by auto
  moreover note Res ‹eqvt Rel›
  moreover have "eqvt Id" by(auto simp add: eqvt_def)
  ultimately show ?thesis using EqvtRel' by(rule parCompose)
qed

lemma resDerivative:
  fixes P    :: pi
  and   Q    :: pi
  and   a    :: subject
  and   x    :: name
  and   y    :: name
  and   Rel  :: "(pi × pi) set"
  and   Rel' :: "(pi × pi) set"
  
  assumes Der: "derivative P Q a x Rel"
  and     Rel: "⋀(P::pi) (Q::pi) (x::name). (P, Q) ∈ Rel ⟹ (<νx>P, <νx>Q) ∈ Rel'"
  and     Eqv: "eqvt Rel"

  shows "derivative (<νy>P) (<νy>Q) a x Rel'"
proof -
  from Der Rel show ?thesis
  proof(cases a, auto simp add: derivative_def)
    fix u
    assume A1: "∀u. (P[x::=u], Q[x::=u]) ∈ Rel"
    show "((<νy>P)[x::=u], (<νy>Q)[x::=u]) ∈ Rel'" 
    proof(cases "x=y")
      assume xeqy: "x=y"

      from A1 have "(P[x::=x], Q[x::=x]) ∈ Rel" by blast
      hence L1: "(<νy>P, <νy>Q) ∈ Rel'" by(force intro: Rel)

      have "y ♯ <νy>P" and "y ♯ <νy>Q" by(simp only: freshRes)+
      hence "(<νy>P)[y::=u] = <νy>P" and "(<νy>Q)[y::=u] = <νy>Q" by(simp add: forget)+

      with L1 xeqy show ?thesis by simp
    next
      assume xineqy: "x≠y"

      show ?thesis
      proof(cases "y=u")
        assume yequ: "y=u"
      
        have "∃(c::name). c ♯ (P, Q, x, y)" by(blast intro: name_exists_fresh)
        then obtain c where cFreshP: "c ♯ P" and cFreshQ: "c ♯ Q" and cineqx: "c ≠ x" and cineqy: "y ≠ c"
          by(force simp add: fresh_prod name_fresh)
        
        from A1 have "(P[x::=c], Q[x::=c]) ∈ Rel" by blast
        with Eqv have "([(y, c)] ∙ (P[x::=c]), [(y, c)] ∙ (Q[x::=c])) ∈ Rel" by(rule eqvtRelI)
        with xineqy cineqx cineqy have "(([(y, c)] ∙ P)[x::=y], ([(y, c)] ∙ Q)[x::=y]) ∈ Rel"
          by(simp add: eqvt_subs name_calc)
        hence "(<νc>(([(y, c)] ∙ P)[x::=y]), <νc>(([(y, c)] ∙ Q)[x::=y])) ∈ Rel'" by(rule Rel)
        with cineqx cineqy have "((<νc>(([(y, c)] ∙ P)))[x::=y], (<νc>(([(y, c)] ∙ Q)))[x::=y])∈ Rel'" by simp
        moreover from cFreshP cFreshQ have "<νc>([(y, c)] ∙ P) = <νy>P" and "<νc>([(y, c)] ∙ Q) = <νy>Q"
          by(simp add: alphaRes)+
        ultimately show ?thesis using yequ by simp
      next
        assume yinequ: "y ≠ u"
        from A1 have "(P[x::=u], Q[x::=u]) ∈ Rel" by blast
        hence "(<νy>(P[x::=u]), <νy>(Q[x::=u])) ∈ Rel'" by(rule Rel)
        with xineqy yinequ show ?thesis by simp
      qed
    qed
  qed
qed

lemma resPres:
  fixes P    :: pi
  and   Q    :: pi
  and   Rel  :: "(pi × pi) set"
  and   x    :: name
  and   Rel' :: "(pi × pi) set"

  assumes PSimQ: "P ↝[Rel] Q"
  and     ResRel: "⋀(P::pi) (Q::pi) (x::name). (P, Q) ∈ Rel ⟹ (<νx>P, <νx>Q) ∈ Rel'"
  and     RelRel': "Rel ⊆ Rel'"
  and     EqvtRel: "eqvt Rel"
  and     EqvtRel': "eqvt Rel'"

  shows "<νx>P ↝[Rel'] <νx>Q"
using EqvtRel'
proof(induct rule: resSimCases[of _ _ _ _ "(P, x)"])
  case(BoundOutput Q' a)
  have QTrans: "Q ⟼a[x] ≺ Q'" and aineqx: "a ≠ x" by fact+
  
  from PSimQ QTrans obtain P' where PTrans: "P ⟼ a[x] ≺ P'"
                                and P'RelQ': "(P', Q') ∈ Rel"
    by(blast dest: simE)
  
  from PTrans aineqx have "<νx>P ⟼a<νx> ≺ P'" by(rule Late_Semantics.Open)
  moreover from P'RelQ' RelRel' have "(P', Q') ∈ Rel'" by force
  ultimately show ?case by blast
next
  case(BoundR Q' a y)
  have QTrans: "Q ⟼a«y» ≺ Q'" and xFresha: "x ♯ a" by fact+
  have "y ♯ (P, x)" by fact 
  hence yFreshP: "y ♯ P" and yineqx: "y ≠ x" by(simp add: fresh_prod)+
  
  from PSimQ yFreshP QTrans  obtain P' where PTrans: "P ⟼a«y» ≺ P'"
                                         and Pderivative: "derivative P' Q' a y Rel"
    by(blast dest: simE)
  from PTrans xFresha yineqx have ResTrans: "<νx>P ⟼a«y» ≺ <νx>P'"
    by(blast intro: Late_Semantics.ResB)
  moreover from Pderivative ResRel EqvtRel have "derivative (<νx>P') (<νx>Q') a y Rel'"
    by(rule resDerivative)
  
  ultimately show ?case by blast
next
  case(FreeR Q' α)
  have QTrans: "Q ⟼ α ≺ Q'" and xFreshAlpha: "(x::name) ♯ α" by fact+
      
  from QTrans PSimQ obtain P' where PTrans: "P ⟼ α ≺ P'"
                                and P'RelQ': "(P', Q') ∈ Rel"
    by(blast dest: simE)

  from PTrans xFreshAlpha have "<νx>P ⟼α ≺ <νx>P'" by(rule Late_Semantics.ResF)
  moreover from P'RelQ' have "(<νx>P', <νx>Q') ∈ Rel'" by(rule ResRel)
  ultimately show ?case by blast
qed

lemma resChainI:
  fixes P   :: pi
  and   Q   :: pi
  and   Rel :: "(pi × pi) set"
  and   xs  :: "name list"

  assumes PRelQ:   "P ↝[Rel] Q"
  and     eqvtRel: "eqvt Rel"
  and     Res:     "⋀P Q x. (P, Q) ∈ Rel ⟹ (<νx>P, <νx>Q) ∈ Rel"

  shows "(resChain xs) P ↝[Rel] (resChain xs) Q"
proof(induct xs) (* Base case *)
  from PRelQ show "resChain [] P ↝[Rel] resChain [] Q" by simp
next (* Inductive step *)
  fix x xs
  assume IH: "(resChain xs P) ↝[Rel] (resChain xs Q)"
  moreover note Res
  moreover have "Rel ⊆ Rel" by simp
  ultimately have "<νx>(resChain xs P) ↝[Rel] <νx>(resChain xs Q)" using eqvtRel
    by(rule_tac resPres) 
  
  thus "resChain (x # xs) P ↝[Rel] resChain (x # xs) Q"
    by simp
qed

lemma bangPres:
  fixes P    :: pi
  and   Q    :: pi
  and   Rel  :: "(pi × pi) set"
 
  assumes PRelQ:    "(P, Q) ∈ Rel"
  and     Sim:      "⋀P Q. (P, Q) ∈ Rel ⟹ P ↝[Rel] Q"
  and     eqvtRel:  "eqvt Rel"

  shows "!P ↝[bangRel Rel] !Q"
proof -
  let ?Sim = "λP Rs. (∀a x Q'. Rs = a«x» ≺ Q' ⟶ x ♯ P ⟶ (∃P'. P ⟼a«x» ≺ P' ∧ derivative P' Q' a x (bangRel Rel))) ∧
                     (∀α Q'. Rs = α ≺ Q' ⟶ (∃P'. P ⟼α ≺ P' ∧ (P', Q') ∈ bangRel Rel))"
  from eqvtRel have EqvtBangRel: "eqvt(bangRel Rel)" by(rule eqvtBangRel)

  {
    fix Pa Rs
    assume "!Q ⟼ Rs" and "(Pa, !Q) ∈ bangRel Rel"
    hence "?Sim Pa Rs" using PRelQ
    proof(nominal_induct avoiding: Pa P rule: bangInduct)
      case(cPar1B a x Q' Pa P)
      have QTrans: "Q ⟼ a«x» ≺ Q'" by fact
      have "(Pa, Q ∥ !Q) ∈ bangRel Rel" and "x ♯ Pa" by fact+
      thus "?Sim Pa (a«x» ≺ (Q' ∥ !Q))"
      proof(induct rule: BRParCases)
        case(BRPar P R)
        have PRelQ: "(P, Q) ∈ Rel" by fact
        have PBRQ: "(R, !Q) ∈ bangRel Rel" by fact
        have "x ♯ P ∥ R" by fact
        hence xFreshP: "x ♯ P" and xFreshR: "x ♯ R" by simp+
        show ?case 
        proof(auto simp add: residual.inject alpha')
          from PRelQ have "P ↝[Rel] Q" by(rule Sim)

          with QTrans xFreshP obtain P' where PTrans: "P ⟼ a«x» ≺ P'" and P'RelQ': "derivative P' Q' a x Rel"
            by(blast dest: simE)

          from PTrans xFreshR have "P ∥ R ⟼ a«x» ≺ (P' ∥ R)"
            by(force intro: Late_Semantics.Par1B)
          moreover from P'RelQ' PBRQ ‹x ♯ Q› ‹x ♯ R› have "derivative (P' ∥ R) (Q' ∥ !Q) a x (bangRel Rel)"
            by(cases a) (auto simp add: derivative_def forget intro: Rel.BRPar)
          ultimately show "∃P'. P ∥ R ⟼a«x» ≺ P' ∧ derivative P' (Q' ∥ !Q) a x (bangRel Rel)" by blast
        next
          fix y
          assume "(y::name) ♯ Q'" and "y ♯ P" and "y ♯ R" and "y ♯ Q"
          from QTrans ‹y ♯ Q'› have "Q ⟼a«y» ≺ ([(x, y)] ∙ Q')"
            by(simp add: alphaBoundResidual)
          moreover from PRelQ have "P ↝[Rel] Q" by(rule Sim)
          ultimately obtain P' where PTrans: "P ⟼a«y» ≺ P'" and P'RelQ': "derivative P' ([(x, y)] ∙ Q') a y Rel"
            using ‹y ♯ P›
            by(blast dest: simE)
          from PTrans ‹y ♯ R› have "P ∥ R ⟼a«y» ≺ (P' ∥ R)" by(force intro: Late_Semantics.Par1B)
          moreover from P'RelQ' PBRQ ‹y ♯ Q› ‹y ♯ R› have "derivative (P' ∥ R) (([(x, y)] ∙ Q') ∥ !Q) a y (bangRel Rel)"
            by(cases a) (auto simp add: derivative_def forget intro: Rel.BRPar)
          with ‹x ♯ Q› ‹y ♯ Q› have "derivative (P' ∥ R) (([(y, x)] ∙ Q') ∥ !([(y, x)] ∙ Q)) a y (bangRel Rel)"
            by(simp add: name_fresh_fresh name_swap)
          ultimately show "∃P'. P ∥ R ⟼a«y» ≺ P' ∧ derivative P' (([(y, x)] ∙ Q') ∥ !([(y, x)] ∙ Q)) a y (bangRel Rel)"
            by blast
        qed
      qed
    next
      case(cPar1F α Q' Pa P)
      have QTrans: "Q ⟼α ≺ Q'" by fact
      have "(Pa, Q ∥ !Q) ∈ bangRel Rel" by fact
      thus ?case
      proof(induct rule: BRParCases)
        case(BRPar P R)
        have PRelQ: "(P, Q) ∈ Rel" and BR: "(R, !Q) ∈ bangRel Rel" by fact+
        show ?case
        proof(auto simp add: residual.inject)
          from PRelQ have "P ↝[Rel] Q" by(rule Sim)
          with QTrans obtain P' where PTrans: "P ⟼ α ≺ P'" and RRel: "(P', Q') ∈ Rel"
            by(blast dest: simE)
          
          from PTrans have "P ∥ R ⟼ α ≺ P' ∥ R" by(rule Par1F)
          moreover from RRel BR have "(P' ∥ R, Q' ∥ !Q) ∈ bangRel Rel" by(rule Rel.BRPar)
          ultimately show "∃P'. P ∥ R ⟼ α ≺ P' ∧ (P', Q' ∥ !Q) ∈ bangRel Rel" by blast
        qed
      qed
    next
      case(cPar2B a x Q' Pa P)
      hence IH: "⋀Pa. (Pa, !Q) ∈ bangRel Rel ⟹ ?Sim Pa (a«x» ≺ Q')" by simp
      have "(Pa, Q ∥ !Q) ∈ bangRel Rel" and "x ♯ Pa" by fact+
      thus "?Sim Pa (a«x» ≺ (Q ∥ Q'))"
      proof(induct rule: BRParCases)
        case(BRPar P R)
        have PRelQ: "(P, Q) ∈ Rel" and RBRQ: "(R, !Q) ∈ bangRel Rel" by fact+
        have "x ♯ P ∥ R" by fact
        hence xFreshP: "x ♯ P" and xFreshR: "x ♯ R" by simp+

        from EqvtBangRel ‹x ♯ Q› show "?Sim (P ∥ R) (a«x» ≺ (Q ∥ Q'))"
        proof(auto simp add: residual.inject alpha' name_fresh_fresh)
          from RBRQ have "?Sim R (a«x» ≺ Q')" by(rule IH)
          with xFreshR obtain R' where RTrans: "R ⟼ a«x» ≺ R'" and R'BRQ': "derivative R' Q' a x (bangRel Rel)"
            by(auto simp add: residual.inject)
          from RTrans xFreshP have "P ∥ R ⟼ a«x» ≺ (P ∥ R')" by(auto intro: Par2B)
          moreover from PRelQ R'BRQ' ‹x ♯ Q› ‹x ♯ P› have "derivative (P ∥ R') (Q ∥ Q') a x (bangRel Rel)" 
            by(cases a) (auto simp add: derivative_def forget intro: Rel.BRPar)
          ultimately show "∃P'. P ∥ R ⟼ a«x» ≺ P' ∧ derivative P' (Q ∥ Q') a x (bangRel Rel)" by blast
        next
          fix y
          assume "(y::name) ♯ Q" and "y ♯ Q'" and "y ♯ P" and "y ♯ R"
          from RBRQ have "?Sim R (a«x» ≺ Q')" by(rule IH)
          with ‹y ♯ Q'› have "?Sim R (a«y» ≺ ([(x, y)] ∙ Q'))" by(simp add: alphaBoundResidual)
          with ‹y ♯ R› obtain R' where RTrans: "R ⟼ a«y» ≺ R'" and R'BRQ': "derivative R' ([(x, y)] ∙ Q') a y (bangRel Rel)"
            by(auto simp add: residual.inject)
          from RTrans ‹y ♯ P› have "P ∥ R ⟼ a«y» ≺ (P ∥ R')" by(auto intro: Par2B)
          moreover from PRelQ R'BRQ' ‹y ♯ P› ‹y ♯ Q› have "derivative (P ∥ R') (Q ∥ ([(x, y)] ∙ Q')) a y (bangRel Rel)" 
            by(cases a) (auto simp add: derivative_def forget intro: Rel.BRPar)
          hence "derivative (P ∥ R') (Q ∥ ([(y, x)] ∙ Q')) a y (bangRel Rel)"
            by(simp add: name_swap)
          ultimately show "∃P'. P ∥ R ⟼ a«y» ≺ P' ∧ derivative P' (Q ∥ ([(y, x)] ∙ Q')) a y (bangRel Rel)" by blast
        qed
      qed
    next
      case(cPar2F α Q' Pa P)
      hence IH: "⋀Pa. (Pa, !Q) ∈ bangRel Rel ⟹ ?Sim Pa (α ≺ Q')" by simp
      have "(Pa, Q ∥ !Q) ∈ bangRel Rel" by fact
      thus ?case
      proof(induct rule: BRParCases)
        case(BRPar P R)
        have PRelQ: "(P, Q) ∈ Rel" and RBRQ: "(R, !Q) ∈ bangRel Rel" by fact+
        show ?case
        proof(auto simp add: residual.inject)
          from RBRQ IH have "∃R'. R ⟼ α ≺ R' ∧ (R', Q') ∈ bangRel Rel"
            by(metis simE)
          then obtain R' where RTrans: "R ⟼ α ≺ R'" and R'RelQ': "(R', Q') ∈ bangRel Rel"
            by blast

          from RTrans have "P ∥ R ⟼ α ≺ P ∥ R'" by(rule Par2F)
          moreover from PRelQ R'RelQ' have "(P ∥ R', Q ∥ Q') ∈ bangRel Rel" by(rule Rel.BRPar)
          ultimately show " ∃P'. P ∥ R ⟼ α ≺ P' ∧ (P', Q ∥ Q') ∈ bangRel Rel" by blast
        qed
      qed
    next
      case(cComm1 a x Q' b Q'' Pa P)
      hence IH: "⋀Pa. (Pa, !Q) ∈ bangRel Rel ⟹ ?Sim Pa (a[b] ≺ Q'')" by simp
      have QTrans: "Q ⟼a<x> ≺ Q'" by fact
      have "(Pa, Q ∥ !Q) ∈ bangRel Rel" by fact
      thus ?case using ‹x ♯ Pa›
      proof(induct rule: BRParCases)
        case(BRPar P R)
        have PRelQ: "(P, Q) ∈ Rel" and RBRQ: "(R, !Q) ∈ bangRel Rel" by fact+
        from ‹x ♯ P ∥ R› have "x ♯ P" and "x ♯ R" by simp+
        show ?case
        proof(auto simp add: residual.inject)
          from PRelQ have "P ↝[Rel] Q" by(rule Sim)
          with QTrans ‹x ♯ P› obtain P' where PTrans: "P ⟼ a<x> ≺ P'" and P'RelQ': "(P'[x::=b], Q'[x::=b]) ∈ Rel"
            by(drule_tac simE) (auto simp add: derivative_def)
          
          from IH RBRQ have RTrans: "∃R'. R ⟼ a[b] ≺ R' ∧ (R', Q'') ∈ bangRel Rel"
            by(auto simp add: derivative_def)
          then obtain R' where RTrans: "R ⟼ a[b] ≺ R'" and R'RelQ'': "(R', Q'') ∈ bangRel Rel"
            by blast
          
          from PTrans RTrans have "P ∥ R ⟼τ ≺ P'[x::=b] ∥ R'" by(rule Comm1)
          moreover from P'RelQ' R'RelQ'' have "(P'[x::=b] ∥ R', Q'[x::=b] ∥ Q'') ∈ bangRel Rel" by(rule Rel.BRPar)
          ultimately show "∃P'. P ∥ R ⟼ τ ≺ P' ∧ (P', Q'[x::=b] ∥ Q'') ∈ bangRel Rel" by blast
        qed
      qed
    next
      case(cComm2 a b Q' x Q'' Pa P)
      hence IH: "⋀Pa. (Pa, !Q) ∈ bangRel Rel ⟹ ?Sim Pa (a<x> ≺ Q'')" by simp
      have QTrans: "Q ⟼ a[b] ≺ Q'" by fact
      have "(Pa, Q ∥ !Q) ∈ bangRel Rel" by fact
      thus ?case using ‹x ♯ Pa›
      proof(induct rule: BRParCases)
        case(BRPar P R)
        have PRelQ: "(P, Q) ∈ Rel" and RBRQ: "(R, !Q) ∈ bangRel Rel" by fact+
        from ‹x ♯ P ∥ R› have "x ♯ P" and "x ♯ R" by simp+
        show ?case
        proof(auto simp add: residual.inject)
          from PRelQ have "P ↝[Rel] Q" by(rule Sim)
          with QTrans obtain P' where PTrans: "P ⟼ a[b] ≺ P'" and P'RelQ': "(P', Q') ∈ Rel"
            by(blast dest: simE)

          from IH RBRQ ‹x ♯ R› have RTrans: "∃R'. R ⟼ a<x> ≺ R' ∧ (R'[x::=b], Q''[x::=b]) ∈ bangRel Rel"
            by(fastforce simp add: derivative_def residual.inject)
          then obtain R' where RTrans: "R ⟼ a<x> ≺ R'" and R'RelQ'': "(R'[x::=b], Q''[x::=b]) ∈ bangRel Rel"
            by blast

          from PTrans RTrans have "P ∥ R ⟼ τ ≺ P' ∥ R'[x::=b]" by(rule Comm2)
          moreover from P'RelQ' R'RelQ'' have "(P' ∥ R'[x::=b], Q' ∥ Q''[x::=b]) ∈ bangRel Rel" by(rule Rel.BRPar)
          ultimately show "∃P'. P ∥ R ⟼ τ ≺ P' ∧ (P', Q' ∥ (Q''[x::=b])) ∈ bangRel Rel" by blast
        qed
      qed
    next
      case(cClose1 a x Q' y Q'' Pa P)
      hence IH: "⋀Pa. (Pa, !Q) ∈ bangRel Rel ⟶ ?Sim Pa (a<νy> ≺ Q'')" by simp
      have QTrans: "Q ⟼ a<x> ≺ Q'" by fact
      have "(Pa, Q ∥ !Q) ∈ bangRel Rel" by fact
      moreover have xFreshPa: "x ♯ Pa" by fact
      ultimately show ?case using ‹y ♯ Pa›
      proof(induct rule: BRParCases)
        case(BRPar P R)
        have PRelQ: "(P, Q) ∈ Rel" and RBRQ: "(R, !Q) ∈ bangRel Rel" by fact+
        have "x ♯ P ∥ R" and "y ♯ P ∥ R" by fact+
        hence xFreshP: "x ♯ P" and xFreshR: "x ♯ R" and "y ♯ R" and "y ♯ P" by simp+
        show ?case
        proof(auto simp add: residual.inject)
          from PRelQ have "P ↝[Rel] Q" by(rule Sim)
          with QTrans xFreshP obtain P' where PTrans: "P ⟼a<x> ≺ P'" and P'RelQ': "(P'[x::=y], Q'[x::=y]) ∈ Rel"
            by(fastforce dest: simE simp add: derivative_def)

           from RBRQ ‹y ♯ R› IH have "∃R'. R ⟼a<νy> ≺ R' ∧ (R', Q'') ∈ bangRel Rel"
             by(auto simp add: residual.inject derivative_def)
           then obtain R' where RTrans: "R ⟼a<νy> ≺ R'" and R'RelQ'': "(R', Q'') ∈ bangRel Rel"
             by blast

           from PTrans RTrans ‹y ♯ P› have "P ∥ R ⟼τ ≺ <νy>(P'[x::=y] ∥ R')"
             by(rule Close1)     
           moreover from P'RelQ' R'RelQ'' have "(<νy>(P'[x::=y] ∥ R'), <νy>(Q'[x::=y] ∥ Q'')) ∈ bangRel Rel"
             by(force intro: Rel.BRPar BRRes)
           ultimately show "∃P'. P ∥ R ⟼ τ ≺ P' ∧ (P', <νy>(Q'[x::=y] ∥ Q'')) ∈ bangRel Rel" by blast
         qed
      qed
    next
      case(cClose2 a x Q' y Q'' Pa P)
      hence IH: "⋀Pa. (Pa, !Q) ∈ bangRel Rel ⟹ ?Sim Pa (a<y> ≺ Q'')" by simp
      have QTrans: "Q ⟼ a<νx> ≺ Q'" by fact
      have "(Pa, Q ∥ !Q) ∈ bangRel Rel" and "x ♯ Pa" and "y ♯ Pa" by fact+
      thus ?case
      proof(induct rule: BRParCases)
        case(BRPar P R)
        have PRelQ: "(P, Q) ∈ Rel" and RBRQ: "(R, !Q) ∈ bangRel Rel" by fact+
        have "x ♯ P ∥ R" and "y ♯ P ∥ R" by fact+
        hence xFreshP: "x ♯ P" and xFreshR: "x ♯ R" and "y ♯ R" by simp+
        show ?case
        proof(auto simp add: residual.inject)
          from PRelQ have "P ↝[Rel] Q" by(rule Sim)
          with QTrans xFreshP obtain P' where PTrans: "P ⟼a<νx> ≺ P'" and P'RelQ': "(P', Q') ∈ Rel"
            by(fastforce dest: simE simp add: derivative_def)

          from RBRQ IH ‹y ♯ R› have "∃R'.  R ⟼a<y> ≺ R' ∧ (R'[y::=x], Q''[y::=x]) ∈ bangRel Rel"
            by(fastforce simp add: derivative_def residual.inject)
          then obtain R' where RTrans: "R ⟼a<y> ≺ R'" and R'RelQ'': "(R'[y::=x], Q''[y::=x]) ∈ bangRel Rel"
            by blast

          from PTrans RTrans xFreshR have "P ∥ R ⟼ τ ≺ <νx>(P' ∥ R'[y::=x])"
            by(rule Close2)
          moreover from P'RelQ' R'RelQ'' have "(<νx>(P' ∥ R'[y::=x]), <νx>(Q' ∥ Q''[y::=x])) ∈ bangRel Rel"
            by(force intro: Rel.BRPar BRRes)
          ultimately show "∃P'. P ∥ R ⟼ τ ≺ P' ∧ (P', <νx>(Q' ∥ Q''[y::=x])) ∈ bangRel Rel" by blast
        qed
      qed
    next
      case(cBang Rs Pa P)
      hence IH: "⋀Pa. (Pa, Q ∥ !Q) ∈ bangRel Rel ⟹ ?Sim Pa Rs" by simp
      have "(Pa, !Q) ∈ bangRel Rel" by fact
      thus ?case
      proof(induct rule: BRBangCases)
        case(BRBang P)
        have PRelQ: "(P, Q) ∈ Rel" by fact
        hence "(!P, !Q) ∈ bangRel Rel" by(rule Rel.BRBang)
        with PRelQ have "(P ∥ !P, Q ∥ !Q) ∈ bangRel Rel" by(rule BRPar)
        with IH have "?Sim (P ∥ !P) Rs" by simp
        thus ?case by(force intro: Bang)
      qed
    qed
  }

  moreover from PRelQ have "(!P, !Q) ∈ bangRel Rel" by(rule BRBang) 
  ultimately show ?thesis by(auto simp add: simulation_def)
qed

end