Theory Weak_Early_Step_Sim_Pres

(* 
   Title: The pi-calculus   
   Author/Maintainer: Jesper Bengtson (jebe.dk), 2012
*)
theory Weak_Early_Step_Sim_Pres
  imports Weak_Early_Step_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(induct rule: simCases)
  case(Bound a x Q')
  have "τ.(Q) ⟼a<νx> ≺ Q'" by fact
  hence False by(induct rule: tauCases', auto)
  thus ?case by simp
next
  case(Free α Q')
  have "τ.(Q) ⟼(α ≺ Q')" by fact
  thus ?case
  proof(induct rule: tauCases', auto simp add: pi.inject residual.inject)
    have "τ.(P) ⟹ τ ≺ P" by(rule Weak_Early_Step_Semantics.Tau)
    with PRelQ show "∃P'. τ.(P) ⟹ τ ≺ P' ∧ (P', Q) ∈ Rel" by blast
  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
    by(erule_tac inputCases') auto
next
  case(Free α Q')
  from ‹a<x>.Q ⟼ α ≺ Q'›
  show ?case
  proof(induct rule: inputCases)
    case(cInput u)
    have "a<x>.P ⟹(a<u>) ≺ (P[x::=u])"
      by(rule Weak_Early_Step_Semantics.Input)
    moreover from PRelQ have "(P[x::=u], Q[x::=u]) ∈ Rel" by auto
    ultimately show ?case by blast
  qed
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(induct rule: simCases)
  case(Bound c x Q')
  have "a{b}.Q ⟼c<νx> ≺ Q'" by fact
  hence False by(induct rule: outputCases', auto)
  thus ?case by simp
next
  case(Free α Q')
  have "a{b}.Q ⟼α ≺ Q'" by fact
  thus "∃P'. a{b}.P ⟹ α ≺ P' ∧ (P', Q') ∈ Rel"
  proof(induct rule: outputCases', auto simp add: pi.inject residual.inject)
    have "a{b}.P ⟹ a[b] ≺ P" by(rule Weak_Early_Step_Semantics.Output)
    with PRelQ show "∃P'. a{b}.P ⟹ a[b] ≺ P' ∧ (P', Q) ∈ Rel" by blast
  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     RelRel': "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::name) ♯ P" by simp
  have "[a⌢b]Q ⟼c<νx> ≺ Q'" by fact
  thus ?case
  proof(induct rule: matchCases)
    case Match
    have "Q ⟼c<νx> ≺ Q'" by fact
    with PSimQ xFreshP obtain P' where PTrans: "P ⟹c<νx> ≺ P'"
                                   and P'RelQ': "(P', Q') ∈ Rel"
      by(blast dest: simE)
    from PTrans have "[a⌢a]P ⟹c<νx> ≺ P'" by(rule Weak_Early_Step_Semantics.Match)
    moreover from P'RelQ' RelRel' have "(P', Q') ∈ Rel'" by blast
    ultimately show ?case by blast
  qed
next
  case(Free α Q')
  have "[a⌢b]Q ⟼α ≺ Q'" by fact
  thus ?case
  proof(induct rule: matchCases)
    case Match
    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 Weak_Early_Step_Semantics.Match)
    with RelRel' PRel show ?case by blast
  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     RelRel': "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::name) ♯ P" by simp
  have "[a≠b]Q ⟼c<νx> ≺ Q'" by fact
  thus ?case
  proof(induct rule: mismatchCases)
    case Mismatch
    have aineqb: "a ≠ b" by fact
    have "Q ⟼c<νx> ≺ Q'" by fact
    with PSimQ xFreshP obtain P' where PTrans: "P ⟹c<νx> ≺ P'"
                                   and P'RelQ': "(P', Q') ∈ Rel"
      by(blast dest: simE)
    from PTrans aineqb have "[a≠b]P ⟹c<νx> ≺ P'" by(rule Weak_Early_Step_Semantics.Mismatch)
    moreover from P'RelQ' RelRel' have "(P', Q') ∈ Rel'" by blast
    ultimately show ?case by blast
  qed
next
  case(Free α Q')
  have "[a≠b]Q ⟼α ≺ Q'" by fact
  thus ?case
  proof(induct rule: mismatchCases)
    case Mismatch
    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 Weak_Early_Step_Semantics.Mismatch)
    with RelRel' PRel show ?case by blast
  qed
qed

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

  assumes PSimQ: "P ↝«Rel» Q"
  and     RelRel': "Rel ⊆ Rel'"
  and     C: "Id ⊆ Rel'"

  shows "P ⊕ R ↝«Rel'» Q ⊕ R"
proof(induct rule: simCases)
  case(Bound a x Q')
  have "x ♯ P ⊕ R" by fact
  hence xFreshP: "(x::name) ♯ P" and xFreshR: "x ♯ R" by simp+
  have "Q ⊕ R ⟼a<νx> ≺ Q'" by fact
  thus ?case
  proof(induct rule: sumCases)
    case Sum1
    have "Q ⟼a<νx> ≺ Q'" by fact
    with xFreshP PSimQ obtain P' where PTrans: "P ⟹a<νx> ≺ P'" and P'RelQ': "(P', Q') ∈ Rel"
      by(blast dest: simE)
    from PTrans have "P ⊕ R ⟹a<νx> ≺ P'" by(rule Weak_Early_Step_Semantics.Sum1)
    moreover from P'RelQ' RelRel' have "(P', Q') ∈ Rel'" by blast
    ultimately show ?case by blast
  next
    case Sum2
    from ‹R ⟼a<νx> ≺ Q'› have "P ⊕ R ⟼a<νx> ≺ Q'" by(rule Early_Semantics.Sum2)
    hence "P ⊕ R ⟹a<νx> ≺ Q'" by(rule Weak_Early_Step_Semantics.singleActionChain)
    moreover from C have "(Q', Q') ∈ Rel'" by blast
    ultimately show ?case by blast
  qed
next
  case(Free α Q')
  have "Q ⊕ R ⟼α ≺ Q'" by fact
  thus ?case
  proof(induct rule: sumCases)
    case Sum1
    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 "P ⊕ R ⟹α ≺ P'" by(rule Weak_Early_Step_Semantics.Sum1)
    with RelRel' PRel show ?case by blast
  next
    case Sum2
    from ‹R ⟼α ≺ Q'› have "P ⊕ R ⟼α ≺ Q'" by(rule Early_Semantics.Sum2)
    hence "P ⊕ R ⟹α ≺ Q'" by(rule Weak_Early_Step_Semantics.singleActionChain)
    moreover from C have "(Q', Q') ∈ Rel'" by blast
    ultimately show ?case by blast
  qed
qed
      
lemma parPres:
  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     PRelQ:    "(P, Q) ∈ Rel"
  and     Par:      "⋀S T U. (S, T) ∈ Rel ⟹ (S ∥ U, T ∥ U) ∈ Rel'"
  and     Res:      "⋀S T x. (S, T) ∈ Rel' ⟹ (<νx>S, <νx>T) ∈ Rel'"

  shows "P ∥ R ↝«Rel'» Q ∥ R"
proof -
  show ?thesis
  proof(induct rule: simCases)
    case(Bound a x Q')
    have "x ♯ P ∥ R" by fact
    hence xFreshP: "x ♯ P" and xFreshR: "x ♯ R" by simp+
    have "Q ∥ R ⟼a<νx> ≺ Q'" by fact
    thus ?case
    proof(induct rule: parCasesB)
      case(cPar1 Q')
      have QTrans: "Q ⟼ a<νx> ≺ Q'" by fact
      from xFreshP PSimQ QTrans obtain P' where PTrans:"P ⟹ a<νx> ≺ P'"
                                            and P'RelQ': "(P', Q') ∈ Rel"
        by(blast dest: simE)
      from PTrans xFreshR have "P ∥ R ⟹ a<νx> ≺ (P' ∥ R)" by(rule Weak_Early_Step_Semantics.Par1B)
      moreover from P'RelQ' have "(P' ∥ R, Q' ∥ R) ∈ Rel'" by(rule Par)
      ultimately show ?case by blast
    next
      case(cPar2 R')
      from ‹R ⟼ a<νx> ≺ R'› ‹x ♯ P› have "P ∥ R ⟼a<νx> ≺ (P ∥ R')"
        by(rule Early_Semantics.Par2B)
      hence "P ∥ R ⟹ a<νx> ≺ (P ∥ R')" by(rule Weak_Early_Step_Semantics.singleActionChain)
      moreover from PRelQ have "(P ∥ R', Q ∥  R') ∈ Rel'" by(rule Par)
      ultimately show ?case by blast
    qed
  next
    case(Free α QR')
    have "Q ∥ R ⟼ α ≺ QR'" by fact
    thus ?case
    proof(induct rule: parCasesF[of _ _ _ _ _ "(P, R)"])
      case(cPar1 Q')
      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 Trans: "P ∥ R ⟹ α ≺ P' ∥ R" by(rule Weak_Early_Step_Semantics.Par1F)
      moreover from PRel have "(P' ∥ R, Q' ∥ R) ∈ Rel'" by(blast intro: Par)
      ultimately show ?case by blast
    next
      case(cPar2 R')
      from ‹R ⟼α ≺ R'› have "P ∥ R ⟼α ≺ (P ∥ R')"
        by(rule Early_Semantics.Par2F)
      hence "P ∥ R ⟹α ≺ (P ∥ R')" by(rule Weak_Early_Step_Semantics.singleActionChain)
      moreover from PRelQ have "(P ∥ R', Q ∥  R') ∈ Rel'" by(rule Par)
      ultimately show ?case by blast
    next
      case(cComm1 Q' R' a b)
      have QTrans: "Q ⟼ a<b> ≺ Q'" and RTrans: "R ⟼ a[b] ≺ R'" by fact+

      from PSimQ QTrans obtain P' where PTrans: "P ⟹a<b> ≺ P'"
                                    and P'RelQ': "(P', Q') ∈ Rel"
        by(blast dest: simE)
      from RTrans have "R ⟹a[b] ≺ R'" by(rule Weak_Early_Step_Semantics.singleActionChain)
      with PTrans have "P ∥ R ⟹ τ ≺ P' ∥ R'" by(rule Weak_Early_Step_Semantics.Comm1)
      moreover from P'RelQ' have "(P' ∥ R', Q' ∥ R') ∈ Rel'" by(rule Par)
      ultimately show ?case by blast
    next
      case(cComm2 Q' R' a b)
      have QTrans: "Q ⟼a[b] ≺ Q'" and RTrans: "R ⟼a<b> ≺ R'" by fact+
      
      from PSimQ QTrans obtain P' where PTrans: "P ⟹a[b] ≺ P'"
                                    and P'RelQ': "(P', Q') ∈ Rel"
        by(blast dest: simE)
      
      from RTrans have "R ⟹a<b> ≺ R'" by(rule Weak_Early_Step_Semantics.singleActionChain)
      with PTrans have "P ∥ R ⟹ τ ≺ P' ∥ R'" by(rule Weak_Early_Step_Semantics.Comm2)
      moreover from P'RelQ' have "(P' ∥ R', Q' ∥ R') ∈ Rel'" by(rule Par)
      ultimately show ?case by blast
    next
      case(cClose1 Q' R' a x)
      have QTrans: "Q ⟼a<x> ≺ Q'" and RTrans: "R ⟼a<νx> ≺ R'" by fact+
      have "x ♯ (P, R)" by fact
      hence xFreshP: "x ♯ P" and xFreshR: "x ♯ R" by(simp add: fresh_prod)+
      
      from PSimQ QTrans obtain P' where PTrans: "P ⟹a<x> ≺ P'"
                                    and P'RelQ': "(P', Q') ∈ Rel"
        by(blast dest: simE)
      
      from RTrans have "R ⟹a<νx> ≺ R'" by(rule Weak_Early_Step_Semantics.singleActionChain)
      with PTrans have Trans: "P ∥ R ⟹ τ ≺ <νx>(P' ∥ R')" using ‹x ♯ P›
        by(rule Weak_Early_Step_Semantics.Close1)
      moreover from P'RelQ' have "(<νx>(P' ∥ R'), <νx>(Q' ∥ R')) ∈ Rel'"
        by(blast intro: Par Res)
      ultimately show ?case by blast
    next
      case(cClose2 Q' R' a x)
      have QTrans: "Q ⟼a<νx> ≺ Q'" and RTrans: "R ⟼a<x> ≺ R'" by fact+
      have "x ♯ (P, R)" by fact
      hence xFreshR: "x ♯ R" and xFreshP: "x ♯ P" by(simp add: fresh_prod)+

      from PSimQ QTrans xFreshP obtain P' where PTrans: "P ⟹a<νx> ≺ P'"
                                            and P'RelQ': "(P', Q') ∈ Rel"
        by(blast dest: simE)
      
      from RTrans have "R ⟹a<x> ≺ R'" by(rule Weak_Early_Step_Semantics.singleActionChain)
      with PTrans have Trans: "P ∥ R ⟹τ ≺ <νx>(P' ∥ R')" using ‹x ♯ R›
        by(rule Weak_Early_Step_Semantics.Close2)
      moreover from P'RelQ' have "(<νx>(P' ∥ R'), <νx>(Q' ∥ R')) ∈ Rel'"
        by(blast intro: Par Res)
      ultimately show ?case by blast
    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     C1: "⋀R S x. (R, S) ∈ Rel ⟹ (<νx>R, <νx>S) ∈ Rel'"
  and     RelRel': "Rel ⊆ Rel'"
  and     EqvtRel: "eqvt Rel"
  and     EqvtRel': "eqvt Rel'"

  shows "<νx>P ↝«Rel'» <νx>Q"
proof -
  from EqvtRel' show ?thesis
  proof(induct rule: simCasesCont[of _ "(P, x)"])
    case(Bound a y Q')
    have Trans: "<νx>Q ⟼a<νy> ≺ Q'" by fact
    have "y ♯ (P, x)" by fact
    hence yineqx: "y ≠ x" and yFreshP: "y ♯ P" by(simp add: fresh_prod)+
    from Trans yineqx show ?case
    proof(induct rule: resCasesB)
      case(Open Q')
      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 Weak_Early_Step_Semantics.Open)
      hence "<νx>P ⟹a<νy> ≺ ([(y, x)] ∙ P')" using ‹y ♯ P› ‹y ≠ x›
        by(force simp add: weakTransitionAlpha abs_fresh name_swap)

      moreover from EqvtRel P'RelQ' RelRel' have "([(y, x)] ∙ P', [(y, x)] ∙ Q') ∈ Rel'"
        by(blast intro: eqvtRelI)
      ultimately show ?case by blast
    next
      case(Res Q')
      have QTrans: "Q ⟼a<νy> ≺ Q'" and xineqa: "x ≠ a" by fact+

      from PSimQ yFreshP QTrans obtain P' where PTrans: "P ⟹a<νy> ≺ P'"
                                            and P'RelQ': "(P', Q') ∈ Rel"
        by(blast dest: simE)
      from PTrans xineqa yineqx yFreshP have ResTrans: "<νx>P ⟹a<νy> ≺ (<νx>P')"
        by(blast intro: Weak_Early_Step_Semantics.ResB)
      moreover from P'RelQ' have "((<νx>P'), (<νx>Q')) ∈ Rel'"
        by(rule C1)
      ultimately show ?case by blast
    qed
  next
    case(Free α Q')
    have QTrans: "<νx>Q ⟼ α ≺ Q'" by fact
    have "∃c::name. c ♯ (P, Q, Q', α)" by(blast intro: name_exists_fresh)
    then obtain c::name where cFreshQ: "c ♯ Q" and cFreshAlpha: "c ♯ α" and cFreshQ': "c ♯ Q'" and cFreshP: "c ♯ P"
      by(force simp add: fresh_prod)
    from cFreshP have "<νx>P = <νc>([(x, c)] ∙ P)" by(simp add: alphaRes)
    moreover have "∃P'.<νc>([(x, c)] ∙ P) ⟹ α ≺ P' ∧ (P', Q') ∈ Rel'"
    proof -
      from QTrans cFreshQ have "<νc>([(x, c)] ∙ Q) ⟼α ≺ Q'" by(simp add: alphaRes)
      moreover have "c ♯ α" by(rule cFreshAlpha)
      moreover from PSimQ EqvtRel have "([(x, c)] ∙ P) ↝«Rel» ([(x, c)] ∙ Q)"
        by(blast intro: eqvtI)
      ultimately show ?thesis
        apply(induct rule: resCasesF, auto simp add: residual.inject pi.inject name_abs_eq)
        by(blast intro: Weak_Early_Step_Semantics.ResF C1 dest: simE)
    qed

    ultimately show ?case by force
  qed
qed

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

  assumes eqvtRel: "eqvt Rel"
  and     Res:     "⋀R S x. (R, S) ∈ Rel ⟹ (<νx>R, <νx>S) ∈ Rel"
  and     PRelQ:   "P ↝«Rel» Q"

  shows "(resChain lst) P ↝«Rel» (resChain lst) Q"
proof -
  show ?thesis
  proof(induct lst) (* Base case *)
    from PRelQ show "resChain [] P ↝«Rel» resChain [] Q" by simp
  next (* Inductive step *)
    fix a lst
    assume IH: "(resChain lst P) ↝«Rel» (resChain lst Q)"
    moreover from Res have "⋀P Q a. (P, Q) ∈ Rel ⟹ (<νa>P, <νa>Q) ∈ Rel"
      by simp
    moreover have "Rel ⊆ Rel" by simp
    ultimately have "<νa>(resChain lst P) ↝«Rel» <νa>(resChain lst Q)" using eqvtRel
      by(rule_tac resPres)

    thus "resChain (a # lst) P ↝«Rel» resChain (a # lst) Q"
      by simp
  qed
qed

lemma bangPres:
  fixes P    :: pi
  and   Q    :: pi
  and   Rel  :: "(pi × pi) set"
 
  assumes PRelQ:    "(P, Q) ∈ Rel"
  and     Sim:      "⋀R S. (R, S) ∈ Rel ⟹ R ↝«Rel'» S"
  and     C1:       "Rel ⊆ Rel'"
  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' ∧ (P', Q') ∈ bangRel Rel')) ∧
                     (∀α Q'. Rs = α ≺ Q' ⟶ (∃P'. P ⟹α ≺ P' ∧ (P', Q') ∈ bangRel Rel'))"
  from eqvtRel have EqvtBangRel: "eqvt(bangRel Rel')" by(rule eqvtBangRel)
  from C1 have BRelRel': "⋀P Q. (P, Q) ∈ bangRel Rel ⟹ (P, Q) ∈ bangRel Rel'"
    by(auto intro: bangRelSubset)

  {
    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(Par1B 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': "(P', Q') ∈ Rel'"
            by(blast dest: simE)

          from PTrans xFreshR have "P ∥ R ⟹a<νx> ≺ (P' ∥ R)"
            by(force intro: Weak_Early_Step_Semantics.Par1B)
          moreover from P'RelQ' PBRQ BRelRel' have "(P' ∥ R, Q' ∥ !Q) ∈ bangRel Rel'" by(blast intro: Rel.BRPar)
          ultimately show "∃P'. P ∥ R ⟹a<νx> ≺ P' ∧ (P', Q' ∥ !Q) ∈ 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: alphaBoundOutput)
          moreover from PRelQ have "P ↝«Rel'» Q" by(rule Sim)
          ultimately obtain P' where PTrans: "P ⟹a<νy> ≺ P'" and P'RelQ': "(P', [(x, y)] ∙ Q') ∈ Rel'"
            using ‹y ♯ P›
            by(blast dest: simE)
          from PTrans ‹y ♯ R› have "P ∥ R ⟹a<νy> ≺ (P' ∥ R)" by(force intro: Weak_Early_Step_Semantics.Par1B)
          moreover from P'RelQ' PBRQ BRelRel' have "(P' ∥ R, ([(x, y)] ∙ Q') ∥ !Q) ∈ bangRel Rel'" by(metis Rel.BRPar)
          with ‹x ♯ Q› ‹y ♯ Q› have "(P' ∥ R, ([(y, x)] ∙ Q') ∥ !([(y, x)] ∙ Q)) ∈ bangRel Rel'"
            by(simp add: name_fresh_fresh name_swap)
          ultimately show "∃P'. P ∥ R ⟹a<νy> ≺ P' ∧ (P', ([(y, x)] ∙ Q') ∥ !([(y, x)] ∙ Q)) ∈ bangRel Rel'"
            by blast
        qed
      qed
    next
      case(Par1F α 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 Weak_Early_Step_Semantics.Par1F)
          moreover from RRel BR BRelRel' have "(P' ∥ R, Q' ∥ !Q) ∈ bangRel Rel'" by(metis Rel.BRPar)
          ultimately show "∃P'. P ∥ R ⟹α ≺ P' ∧ (P', Q' ∥ !Q) ∈ bangRel Rel'" by blast
        qed
      qed
    next
      case(Par2B 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 show "?Sim (P ∥ R) (a<νx> ≺ (Q ∥ Q'))"
        proof(auto simp add: residual.inject alpha')
          from RBRQ have "?Sim R (a<νx> ≺ Q')" by(rule IH)
          with xFreshR obtain R' where RTrans: "R ⟹a<νx> ≺ R'" and R'BRQ': "(R', Q') ∈ (bangRel Rel')"
            by(metis simE)
          from RTrans xFreshP have "P ∥ R ⟹a<νx> ≺ (P ∥ R')" by(auto intro: Weak_Early_Step_Semantics.Par2B)
          moreover from PRelQ R'BRQ' C1 have "(P ∥ R', Q ∥ Q') ∈ (bangRel Rel')" by(blast dest: Rel.BRPar)
          ultimately show "∃P'. P ∥ R ⟹a<νx> ≺ P' ∧ (P', Q ∥ Q') ∈ 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: alphaBoundOutput)
          with ‹y ♯ R› obtain R' where RTrans: "R ⟹a<νy> ≺ R'" and R'BRQ': "(R', ([(x, y)] ∙ Q')) ∈ (bangRel Rel')"
            by(metis simE)
          from RTrans ‹y ♯ P› have "P ∥ R ⟹a<νy> ≺ (P ∥ R')" by(auto intro: Weak_Early_Step_Semantics.Par2B)
          moreover from PRelQ R'BRQ' C1 have "(P ∥ R', Q ∥ ([(x, y)] ∙ Q')) ∈ (bangRel Rel')" by(blast dest: Rel.BRPar)
          with ‹y ♯ Q› ‹x ♯ Q› have "(P ∥ R', ([(y, x)] ∙ Q) ∥ ([(y, x)] ∙ Q')) ∈ (bangRel Rel')"
            by(simp add: name_swap name_fresh_fresh)
          ultimately show "∃P'. P ∥ R ⟹a<νy> ≺ P' ∧ (P', ([(y, x)] ∙ Q) ∥ ([(y, x)] ∙ Q')) ∈ bangRel Rel'" by blast
        qed
      qed
    next
      case(Par2F α 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 Weak_Early_Step_Semantics.Par2F)
          moreover from PRelQ R'RelQ' C1 have "(P ∥ R', Q ∥ Q') ∈ bangRel Rel'" by(blast dest: Rel.BRPar)
          ultimately show " ∃P'. P ∥ R ⟹α ≺ P' ∧ (P', Q ∥ Q') ∈ bangRel Rel'" by blast
        qed
      qed
    next
      case(Comm1 a Q' b Q'' Pa P)
      hence IH: "⋀Pa. (Pa, !Q) ∈ bangRel Rel ⟹ ?Sim Pa (a[b] ≺ Q'')" by simp
      have QTrans: "Q ⟼a<b> ≺ 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 RBRQ: "(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 ⟹a<b> ≺ P'" and P'RelQ': "(P', Q') ∈ Rel'"
            by(blast dest: simE)
          
          from IH RBRQ have RTrans: "∃R'. R ⟹a[b] ≺ R' ∧ (R', Q'') ∈ bangRel Rel'"
            by(metis simE)
          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' ∥ R'" by(rule Weak_Early_Step_Semantics.Comm1)
          moreover from P'RelQ' 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(Comm2 a b Q' Q'')
      hence IH: "⋀Pa. (Pa, !Q) ∈ bangRel Rel ⟹ ?Sim Pa (a<b> ≺ Q'')" by simp
      have QTrans: "Q ⟼ a[b] ≺ 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 RBRQ: "(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 ⟹a[b] ≺ P'" and P'RelQ': "(P', Q') ∈ Rel'"
            by(blast dest: simE)

          from IH RBRQ have RTrans: "∃R'. R ⟹a<b> ≺ R' ∧ (R', Q'') ∈ bangRel Rel'"
            by(metis simE)
          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' ∥ R'" by(rule Weak_Early_Step_Semantics.Comm2)
          moreover from P'RelQ' 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(Close1 a x Q' Q'' Pa P)
      hence IH: "⋀Pa. (Pa, !Q) ∈ bangRel Rel ⟶ ?Sim Pa (a<νx> ≺ Q'')" by simp
      have QTrans: "Q ⟼ a<x> ≺ Q'" by fact
      have xFreshQ: "x ♯ Q" by fact
      have "(Pa, Q ∥ !Q) ∈ bangRel Rel" by fact
      moreover have xFreshPa: "x ♯ Pa" by fact
      ultimately show ?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" by fact
        hence xFreshP: "x ♯ P" and xFreshR: "x ♯ 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(blast dest: simE)

           from RBRQ xFreshR IH have "∃R'. R ⟹a<νx> ≺ R' ∧ (R', Q'') ∈ bangRel Rel'"
             by(metis simE)
           then obtain R' where RTrans: "R ⟹a<νx> ≺ R'" and R'RelQ'': "(R', Q'') ∈ bangRel Rel'"
             by blast

           from PTrans RTrans xFreshP have "P ∥ R ⟹τ ≺ <νx>(P' ∥ R')"
             by(rule Weak_Early_Step_Semantics.Close1)   
           moreover from P'RelQ' R'RelQ'' have "(<νx>(P' ∥ R'), <νx>(Q' ∥ Q'')) ∈ bangRel Rel'"
             by(force intro: Rel.BRPar BRRes)
           ultimately show "∃P'. P ∥ R ⟹τ ≺ P' ∧ (P', <νx>(Q' ∥ Q'')) ∈ bangRel Rel'" by blast
         qed
      qed
    next
      case(Close2 a x Q' Q'' Pa P)
      hence IH: "⋀Pa. (Pa, !Q) ∈ bangRel Rel ⟹ ?Sim Pa (a<x> ≺ Q'')" by simp
      have QTrans: "Q ⟼ a<νx> ≺ Q'" by fact
      have xFreshQ: "x ♯ Q" by fact
      have "(Pa, Q ∥ !Q) ∈ bangRel Rel" and "x ♯ 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" by fact
        hence xFreshP: "x ♯ P" and xFreshR: "x ♯ 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(blast dest: simE)

          from RBRQ IH have "∃R'.  R ⟹a<x> ≺ R' ∧ (R', Q'') ∈ bangRel Rel'"
            by auto
          then obtain R' where RTrans: "R ⟹a<x> ≺ R'" and R'RelQ'': "(R', Q'') ∈ bangRel Rel'"
            by blast

          from PTrans RTrans xFreshR have "P ∥ R ⟹τ ≺ <νx>(P' ∥ R')"
            by(rule Weak_Early_Step_Semantics.Close2)    
          moreover from P'RelQ' R'RelQ'' have "(<νx>(P' ∥ R'), <νx>(Q' ∥ Q'')) ∈ bangRel Rel'"
            by(force intro: Rel.BRPar BRRes)
          ultimately show "∃P'. P ∥ R ⟹τ ≺ P' ∧ (P', <νx>(Q' ∥ Q'')) ∈ bangRel Rel'" by blast
        qed
      qed
    next
      case(Bang 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: Weak_Early_Step_Semantics.Bang)
      qed
    qed
  }

  moreover from PRelQ have "(!P, !Q) ∈ bangRel Rel" by(rule BRBang) 
  ultimately show ?thesis by(auto simp add: weakStepSimulation_def)
qed
(*
lemma bangPres:
  fixes P    :: pi
  and   Q    :: pi
  and   Rel  :: "(pi × pi) set"
  and   Rel' :: "(pi × pi) set"
 
  assumes PRelQ:      "(P, Q) ∈ Rel"
  and     Sim:        "⋀P Q. (P, Q) ∈ Rel ⟹ P ↝<Rel'> Q"
  and     RelRel':    "⋀P Q. (P, Q) ∈ Rel ⟹ (P, Q) ∈ Rel'"
  and     eqvtRel':   "eqvt Rel'"

  shows "!P ↝<bangRel Rel'> !Q"
proof -
  from eqvtRel' have EqvtBangRel': "eqvt (bangRel Rel')" by(rule eqvtBangRel)
  from RelRel' have BRelRel': "⋀P Q. (P, Q) ∈ bangRel Rel ⟹ (P, Q) ∈ bangRel Rel'"
    by(auto intro: bangRelSubset)
  have "⋀Rs P. ⟦!Q ⟼ Rs; (P, !Q) ∈ bangRel Rel⟧ ⟹ weakSimStepAct P Rs P (bangRel Rel')"
  proof -
    fix Rs P
    assume "!Q ⟼ Rs" and "(P, !Q) ∈ bangRel Rel"
    thus "weakSimStepAct P Rs P (bangRel Rel')"
    proof(nominal_induct avoiding: P rule: bangInduct)
      case(Par1B a x Q')
      have QTrans: "Q ⟼a<νx> ≺ Q'" and xFreshQ: "x ♯ Q" by fact
      have "(P, Q ∥ !Q) ∈ bangRel Rel" and "x ♯ P" by fact
      thus ?case
      proof(induct rule: BRParCases)
        case(BRPar P R)
        have PRelQ: "(P, Q) ∈ Rel" and RBangRelT: "(R, !Q) ∈ bangRel Rel" by fact
        have "x ♯ P ∥ R" by fact
        hence xFreshP: "x ♯ P" and xFreshR: "x ♯ R" by simp+
        from PRelQ have PSimQ: "P ↝<Rel'> Q" by(rule Sim)
        from EqvtBangRel' show ?case
        proof(induct rule: simActBoundCases)
          case BoundOutput
          with PSimQ QTrans xFreshP obtain P' where PTrans: "P ⟹a<νx> ≺ P'"
                                                and P'RelQ': "(P', Q') ∈ Rel'"
            by(blast dest: simE)
          from PTrans xFreshR have "P ∥ R ⟹a<νx>≺ (P' ∥ R)"
            by(rule Weak_Early_Step_Semantics.Par1B)
          moreover from P'RelQ' RBangRelT have "(P' ∥ R, Q' ∥ !Q) ∈ bangRel Rel'"
            by(blast intro: Rel.BRPar BRelRel')
          ultimately show ?case by blast
        qed
      qed
    next
      case(Par1F α Q' P)
      have QTrans: "Q ⟼α ≺ Q'" by fact
      have "(P, Q ∥ !Q) ∈ bangRel Rel" by fact
      thus ?case
      proof(induct rule: BRParCases)
        case(BRPar P R)
        have PRelQ: "(P, Q) ∈ Rel" and RBangRelQ: "(R, !Q) ∈ bangRel Rel" by fact
        show ?case
        proof(induct rule: simActFreeCases)
          case Der
          from PRelQ have "P ↝<Rel'> Q" by(rule Sim)
          with QTrans obtain P' where PTrans: "P ⟹α ≺ P'" and P'RelQ': "(P', Q') ∈ Rel'"
            by(blast dest: simE)

          from PTrans have "P ∥ R ⟹α ≺ P' ∥ R" by(rule Weak_Early_Step_Semantics.Par1F)
          moreover from P'RelQ' RBangRelQ have "(P' ∥ R, Q' ∥ !Q) ∈ bangRel Rel'"
            by(blast intro: Rel.BRPar BRelRel')
          ultimately show ?case by blast
        qed
      qed
    next
      case(Par2B a x Q' P)
      have IH: "⋀P. (P, !Q) ∈ bangRel Rel ⟹ weakSimStepAct P (a<νx> ≺ Q') P (bangRel Rel')" by fact
      have xFreshQ: "x ♯ Q" by fact
      have "(P, Q ∥ !Q) ∈ bangRel Rel" and "x ♯ P" by fact
      thus ?case
      proof(induct rule: BRParCases)
        case(BRPar P R)
        have PRelQ: "(P, Q) ∈ Rel" and RBangRelQ: "(R, !Q) ∈ bangRel Rel" by fact
        have "x ♯ P ∥ R" by fact
        hence xFreshP: "x ♯ P" and xFreshR: "x ♯ R" by simp+
        from EqvtBangRel' show ?case
        proof(induct rule: simActBoundCases)
          case BoundOutput
          with IH RBangRelQ have "weakSimStepAct R (a<νx> ≺ Q') R (bangRel Rel')" by blast
          with xFreshR obtain R' where RTrans: "R ⟹a<νx> ≺ R'"
                                   and R'BangRelQ': "(R', Q') ∈ bangRel Rel'"
            by(simp add: weakSimStepAct_def, blast)
          
          from RTrans xFreshP have "P ∥ R ⟹a<νx> ≺ (P ∥ R')"
            by(auto intro: Weak_Early_Step_Semantics.Par2B)
          moreover from PRelQ R'BangRelQ' have "(P ∥ R', Q ∥ Q') ∈ (bangRel Rel')"
            by(blast intro: Rel.BRPar RelRel')
          ultimately show ?case by blast
        qed
      qed
    next
      case(Par2F α Q' P)
      have IH: "⋀P. (P, !Q) ∈ bangRel Rel ⟹ weakSimStepAct P (α ≺ Q') P (bangRel Rel')" by fact
      have "(P, Q ∥ !Q) ∈ bangRel Rel" by fact
      thus ?case
      proof(induct rule: BRParCases)
        case(BRPar P R)
        have PRelQ: "(P, Q) ∈ Rel" and RBangRelQ: "(R, !Q) ∈ bangRel Rel" by fact
        show ?case
        proof(induct rule: simActFreeCases)
          case Der
          from RBangRelQ have "weakSimStepAct R (α ≺ Q') R (bangRel Rel')" by(rule IH)
          then obtain R' where RTrans: "R ⟹α ≺ R'" and R'RelQ': "(R', Q') ∈ (bangRel Rel')"
            by(simp add: weakSimStepAct_def, blast)

          from RTrans have "P ∥ R ⟹α ≺ P ∥ R'" by(rule Weak_Early_Step_Semantics.Par2F)
          moreover from PRelQ R'RelQ' have "(P ∥ R', Q ∥ Q') ∈ (bangRel Rel')" 
            by(blast intro: Rel.BRPar RelRel')
          ultimately show ?case by blast
        qed
      qed
    next
      case(Comm1 a Q' b Q'' P)
      have QTrans: "Q ⟼ a<b> ≺ Q'" by fact
      have IH: "⋀P. (P, !Q) ∈ bangRel Rel ⟹ weakSimStepAct P (a[b] ≺ Q'') P (bangRel Rel')" by fact
      have "(P, Q ∥ !Q) ∈ bangRel Rel" by fact
      thus ?case
      proof(induct rule: BRParCases)
        case(BRPar P R)
        have PRelQ: "(P, Q) ∈ Rel" and RBangRelQ: "(R, !Q) ∈ bangRel Rel" by fact
        show ?case
        proof(induct rule: simActFreeCases)
          case Der
          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 RBangRelQ have "weakSimStepAct R (a[b] ≺ Q'') R (bangRel Rel')" by(rule IH)
          then obtain R' where RTrans: "R ⟹a[b] ≺ R'"
                           and R'RelQ'': "(R', Q'') ∈ (bangRel Rel')"
            by(simp add: weakSimStepAct_def, blast)
        
          from PTrans RTrans have "P ∥ R ⟹τ ≺ (P' ∥ R')"
            by(rule Weak_Early_Step_Semantics.Comm1)
          moreover from P'RelQ' R'RelQ'' have "(P' ∥ R', Q' ∥ Q'') ∈ (bangRel Rel')"
            by(rule Rel.BRPar)
          ultimately show ?case by blast
        qed
      qed
    next
      case(Comm2 a b Q' Q'' P)
      have QTrans: "Q ⟼a[b] ≺ Q'" by fact
      have IH: "⋀P. (P, !Q) ∈ bangRel Rel ⟹ weakSimStepAct P (a<b> ≺ Q'') P (bangRel Rel')" by fact
      have "(P, Q ∥ !Q) ∈ bangRel Rel" by fact
      thus ?case
      proof(induct rule: BRParCases)
        case(BRPar P R)
        have PRelQ: "(P, Q) ∈ Rel" and RBangRelQ: "(R, !Q) ∈ bangRel Rel" by fact+
        show ?case
        proof(induct rule: simActFreeCases)
          case Der
          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 RBangRelQ have "weakSimStepAct R (a<b> ≺ Q'') R (bangRel Rel')" by(rule IH)
          then obtain R' where RTrans: "R ⟹a<b> ≺ R'" and R'BangRelQ'': "(R', Q'') ∈ (bangRel Rel')"
            by(simp add: weakSimStepAct_def, blast)
        
          from PTrans RTrans have "P ∥ R ⟹τ ≺ (P' ∥ R')"
            by(rule Weak_Early_Step_Semantics.Comm2)
          moreover from P'RelQ' R'BangRelQ'' have "(P' ∥ R', Q' ∥ Q'') ∈ (bangRel Rel')"
            by(rule Rel.BRPar)
          ultimately show ?case by blast
        qed
      qed
    next
      case(Close1 a x Q' Q'' P)
      have QTrans: "Q ⟼ a<x> ≺ Q'" by fact
      have IH: "⋀P. (P, !Q) ∈ bangRel Rel ⟹ weakSimStepAct P (a<νx> ≺ Q'') P (bangRel Rel')" by fact
      have "(P, Q ∥ !Q) ∈ bangRel Rel" and "x ♯ P" by fact
      thus ?case
      proof(induct rule: BRParCases)
        case(BRPar P R)
        have PRelQ: "(P, Q) ∈ Rel" and RBangRelQ: "(R, !Q) ∈ bangRel Rel" by fact
        have "x ♯ P ∥ R" by fact
        hence xFreshR: "x ♯ R" and xFreshP: "x ♯ P" by simp+
        show ?case
        proof(induct rule: simActFreeCases)
          case Der
          from PRelQ have "P ↝<Rel'> Q" by(rule Sim)
          with QTrans obtain P' where PTrans: "P ⟹a<x> ≺ P'" and P'RelQ': "(P', Q') ∈ Rel'"
            by(blast dest: simE)
          
          from RBangRelQ have "weakSimStepAct R (a<νx> ≺ Q'') R (bangRel Rel')" by(rule IH)
          with xFreshR obtain R' where RTrans: "R ⟹a<νx> ≺ R'"
                                   and R'RelQ'': "(R', Q'') ∈ (bangRel Rel')"
            by(simp add: weakSimStepAct_def, blast)
        
          from PTrans RTrans xFreshP xFreshR have "P ∥ R ⟹τ ≺ <νx>(P' ∥ R')"
            by(rule Weak_Early_Step_Semantics.Close1)
          moreover from P'RelQ' R'RelQ'' have "(<νx>(P' ∥ R'), <νx>(Q' ∥ Q'')) ∈ (bangRel Rel')"
            by(force intro: Rel.BRPar Rel.BRRes)
          ultimately show ?case by blast
        qed
      qed
    next
      case(Close2 a x Q' Q'' P)
      have QTrans: "Q ⟼ a<νx> ≺ Q'" by fact
      have IH: "⋀P. (P, !Q) ∈ bangRel Rel ⟹ weakSimStepAct P (a<x> ≺ Q'') P (bangRel Rel')" by fact
      have "(P, Q ∥ !Q) ∈ bangRel Rel" and "x ♯ P" by fact
      thus ?case
      proof(induct rule: BRParCases)
        case(BRPar P R)
        have PRelQ: "(P, Q) ∈ Rel" and RBangRelQ: "(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(induct rule: simActFreeCases)
          case Der
          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(blast dest: simE)

          from RBangRelQ have "weakSimStepAct R (a<x> ≺ Q'') R (bangRel Rel')" by(rule IH)
          with xFreshR obtain R' where RTrans: "R ⟹a<x> ≺ R'"
                                       and R'RelQ'': "(R', Q'') ∈ (bangRel Rel')"
            by(simp add: weakSimStepAct_def, blast)
        
          from PTrans RTrans xFreshP xFreshR have "P ∥ R ⟹τ ≺ <νx>(P' ∥ R')"
            by(rule Weak_Early_Step_Semantics.Close2)
          moreover from P'RelQ' R'RelQ'' have "(<νx>(P' ∥ R'), <νx>(Q' ∥ Q'')) ∈ (bangRel Rel')"
            by(force intro: Rel.BRPar Rel.BRRes)
          ultimately show ?case by blast
        qed
      qed
    next
      case(Bang Rs)
      have IH: "⋀P. (P, Q ∥ !Q) ∈ bangRel Rel ⟹ weakSimStepAct P Rs P (bangRel Rel')" by fact
      have "(P, !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 Rel.BRPar)
        hence "weakSimStepAct (P ∥ !P) Rs (P ∥ !P) (bangRel Rel')" by(rule IH)
        thus ?case
        proof(simp (no_asm) add: weakSimStepAct_def, auto)
          fix Q' a x
          assume "weakSimStepAct (P ∥ !P) (a<νx> ≺ Q') (P ∥ !P) (bangRel Rel')" and "x ♯ P"
          then obtain P' where PTrans: "(P ∥ !P) ⟹a<νx> ≺ P'"
                           and P'RelQ': "(P', Q') ∈ (bangRel Rel')"
            by(simp add: weakSimStepAct_def, blast)
          from PTrans have "!P ⟹a<νx> ≺ P'"
            by(force intro: Weak_Early_Step_Semantics.Bang simp add: weakTransition_def)
          with P'RelQ' show "∃P'. !P ⟹a<νx> ≺ P' ∧ (P', Q') ∈ (bangRel Rel')" by blast
        next
          fix Q' α
          assume "weakSimStepAct (P ∥ !P) (α ≺ Q') (P ∥ !P) (bangRel Rel')"
          then obtain P' where PTrans: "(P ∥ !P) ⟹α ≺ P'"
                           and P'RelQ': "(P', Q') ∈ (bangRel Rel')"
            by(simp add: weakSimStepAct_def, blast)
          from PTrans have "!P ⟹α ≺ P'" by(rule Weak_Early_Step_Semantics.Bang)
          with P'RelQ' show "∃P'. !P ⟹α ≺ P' ∧ (P', Q') ∈ (bangRel Rel')" by blast
        qed
      qed
    qed
  qed
  moreover from PRelQ have "(!P, !Q) ∈ bangRel Rel" by(rule Rel.BRBang)
  ultimately show ?thesis by(simp add: simDef)
qed
*)
end