Theory Strong_Late_Expansion_Law

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

nominal_primrec summands :: "pi ⇒ pi set" where 
  "summands 𝟬 = {}"
| "summands (τ.(P)) = {τ.(P)}"
| "x ♯ a ⟹ summands (a<x>.P) = {a<x>.P}"
| "summands (a{b}.P) = {a{b}.P}"
| "summands ([a⌢b]P) = {}"
| "summands ([a≠b]P) = {}"
| "summands (P ⊕ Q) = (summands P) ∪ (summands Q)"
| "summands (P ∥ Q) = {}"
| "summands (<νx>P) = (if (∃a P'. a ≠ x ∧ P = a{x}.P') then ({<νx>P}) else {})"
| "summands (!P) = {}"
apply(auto simp add: fresh_singleton name_fresh_abs fresh_set_empty fresh_singleton pi.fresh)
apply(finite_guess)+
by(fresh_guess)+

lemma summandsInput[simp]:
  fixes a :: name
  and   x :: name
  and   P :: pi

  shows "summands (a<x>.P) = {a<x>.P}"
proof -
  obtain y where yineqa: "y ≠ a" and yFreshP: "y ♯ P"
    by(force intro: name_exists_fresh[of "(a, P)"] simp add: fresh_prod)
  from yFreshP have "a<x>.P = a<y>.([(x, y)] ∙ P)" by(simp add: alphaInput)
  with yineqa show ?thesis by simp
qed

lemma finiteSummands:
  fixes P :: pi
  
  shows "finite(summands P)"
by(induct P rule: pi.induct) auto

lemma boundSummandDest[dest]:
  fixes x  :: name
  and   y  :: name
  and   P' :: pi
  and   P  :: pi

  assumes "<νx>x{y}.P' ∈ summands P"
  
  shows False
using assms
by(induct P rule: pi.induct, auto simp add: if_split pi.inject name_abs_eq name_calc)

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

  assumes "P ∈ summands Q"
  and     "x ♯ Q"
  
  shows "x ♯ P"
using assms
by(nominal_induct Q avoiding: P rule: pi.strong_induct, auto simp add: if_split)

nominal_primrec hnf :: "pi ⇒ bool" where
  "hnf 𝟬 = True"
| "hnf (τ.(P)) = True"
| "x ♯ a ⟹ hnf (a<x>.P) = True"
| "hnf (a{b}.P) = True"
| "hnf ([a⌢b]P) = False"
| "hnf ([a≠b]P) = False"
| "hnf (P ⊕ Q) = ((hnf P) ∧ (hnf Q) ∧ P ≠ 𝟬 ∧ Q ≠ 𝟬)"
| "hnf (P ∥ Q) = False"
| "hnf (<νx>P) = (∃a P'. a ≠ x ∧ P = a{x}.P')"
| "hnf (!P) = False"
apply(auto simp add: fresh_bool)
apply(finite_guess)+
by(fresh_guess)+

lemma hnfInput[simp]:
  fixes a :: name
  and   x :: name
  and   P :: pi

  shows "hnf (a<x>.P)"
proof -
  obtain y where yineqa: "y ≠ a" and yFreshP: "y ♯ P"
    by(force intro: name_exists_fresh[of "(a, P)"] simp add: fresh_prod)
  from yFreshP have "a<x>.P = a<y>.([(x, y)] ∙ P)" by(simp add: alphaInput)
  with yineqa show ?thesis by simp
qed

lemma summandTransition:
  fixes P  :: pi
  and   a  :: name
  and   x  :: name
  and   b  :: name
  and   P' :: pi

  assumes "hnf P"

  shows "P ⟼τ ≺ P' = (τ.(P') ∈ summands P)"
  and   "P ⟼a<x> ≺ P' = (a<x>.P' ∈ summands P)"
  and   "P ⟼a[b] ≺ P' = (a{b}.P' ∈ summands P)"
  and   "a ≠ x ⟹ P ⟼a<νx> ≺ P' = (<νx>a{x}.P' ∈ summands P)"
proof -
  from assms show "P ⟼τ ≺ P' = (τ.(P') ∈ summands P)"
  proof(induct P rule: pi.induct)
    case PiNil
    show ?case by auto
  next
    case(Output a b P)
    show ?case by auto
  next
    case(Tau P)
    have "τ.(P) ⟼τ ≺ P' ⟹ τ.(P') ∈ summands (τ.(P))"
      by(auto elim: tauCases simp add: pi.inject residual.inject)
    moreover have "τ.(P') ∈ summands (τ.(P)) ⟹ τ.(P) ⟼τ ≺ P'"
      by(auto simp add: pi.inject intro: transitions.Tau)
    ultimately show ?case by blast
  next
    case(Input a x P)
    show ?case by auto
  next
    case(Match a b P)
    have "hnf ([a⌢b]P)" by fact
    hence False by simp
    thus ?case by simp
  next
    case(Mismatch a b P)
    have "hnf ([a≠b]P)" by fact
    hence False by simp
    thus ?case by simp
  next
    case(Sum P Q) 
    have "hnf (P ⊕ Q)" by fact
    hence Phnf: "hnf P" and Qhnf: "hnf Q" by simp+
    
    have IHP: "P ⟼τ ≺ P' = (τ.(P') ∈ summands P)"
    proof -
      have "hnf P ⟹ P ⟼τ ≺ P' = (τ.(P') ∈ summands P)" by fact
      with Phnf show ?thesis by simp
    qed
    
    have IHQ: "Q ⟼τ ≺ P' = (τ.(P') ∈ summands Q)"
    proof -
      have "hnf Q ⟹ Q ⟼τ ≺ P' = (τ.(P') ∈ summands Q)" by fact
      with Qhnf show ?thesis by simp
    qed

    from IHP IHQ have "P ⊕ Q ⟼τ ≺ P' ⟹ τ.(P') ∈ summands (P ⊕ Q)"
      by(erule_tac sumCases, auto)
    moreover from IHP IHQ have "τ.(P') ∈ summands (P ⊕ Q) ⟹ P ⊕ Q ⟼τ ≺ P'"
      by(auto dest: Sum1 Sum2)
    ultimately show ?case by blast
  next
    case(Par P Q)
    have "hnf (P ∥ Q)" by fact
    hence False by simp
    thus ?case by simp
  next
    case(Res x P)
    thus ?case by(auto elim: resCasesF)
  next
    case(Bang P)
    have "hnf (!P)" by fact
    hence False by simp
    thus ?case by simp
  qed
next
  from assms show "P ⟼a<x> ≺ P' = (a<x>.P' ∈ summands P)"
  proof(induct P rule: pi.induct)
    case PiNil
    show ?case by auto
  next
    case(Output c b P)
    show ?case by auto
  next
    case(Tau P)
    show ?case by auto
  next
    case(Input b y P)
    have "b<y>.P ⟼a<x> ≺ P' ⟹ a<x>.P' ∈ summands (b<y>.P)"
      by(auto elim: inputCases' simp add: pi.inject residual.inject)
    moreover have "a<x>.P' ∈ summands (b<y>.P) ⟹ b<y>.P ⟼a<x> ≺ P'"
      apply(auto simp add: pi.inject name_abs_eq intro: Late_Semantics.Input)
      apply(subgoal_tac "b<x> ≺ [(x, y)] ∙ P = (b<y> ≺ [(x, y)] ∙ [(x, y)] ∙ P)")
      apply(auto intro: Late_Semantics.Input)
      by(simp add: alphaBoundResidual name_swap)
    ultimately show ?case by blast
  next
    case(Match a b P)
    have "hnf ([a⌢b]P)" by fact
    hence False by simp
    thus ?case by simp
  next
    case(Mismatch a b P)
    have "hnf ([a≠b]P)" by fact
    hence False by simp
    thus ?case by simp
  next
    case(Sum P Q) 
    have "hnf (P ⊕ Q)" by fact
    hence Phnf: "hnf P" and Qhnf: "hnf Q" by simp+
    
    have IHP: "P ⟼a<x> ≺ P' = (a<x>.P' ∈ summands P)"
    proof -
      have "hnf P ⟹ P ⟼a<x> ≺ P' = (a<x>.P' ∈ summands P)" by fact
      with Phnf show ?thesis by simp
    qed
    
    have IHQ: "Q ⟼a<x> ≺ P' = (a<x>.P' ∈ summands Q)"
    proof -
      have "hnf Q ⟹ Q ⟼a<x> ≺ P' = (a<x>.P' ∈ summands Q)" by fact
      with Qhnf show ?thesis by simp
    qed

    from IHP IHQ have "P ⊕ Q ⟼a<x> ≺ P' ⟹ a<x>.P' ∈ summands (P ⊕ Q)"
      by(erule_tac sumCases, auto)
    moreover from IHP IHQ have "a<x>.P' ∈ summands (P ⊕ Q) ⟹ P ⊕ Q ⟼a<x> ≺ P'"
      by(auto dest: Sum1 Sum2)
    ultimately show ?case by blast
  next
    case(Par P Q)
    have "hnf (P ∥ Q)" by fact
    hence False by simp
    thus ?case by simp
  next
    case(Res y P)
    have "hnf(<νy>P)" by fact
    thus ?case by(auto simp add: if_split)
  next
    case(Bang P)
    have "hnf (!P)" by fact
    hence False by simp
    thus ?case by simp
  qed
next
  from assms show "P ⟼a[b] ≺ P' = (a{b}.P' ∈ summands P)"
  proof(induct P rule: pi.induct)
    case PiNil
    show ?case by auto
  next
    case(Output c d P)
    have "c{d}.P ⟼a[b] ≺ P' ⟹ a{b}.P' ∈ summands (c{d}.P)"
      by(auto elim: outputCases simp add: residual.inject pi.inject)
    moreover have "a{b}.P' ∈ summands (c{d}.P) ⟹ c{d}.P ⟼a[b] ≺ P'"
      by(auto simp add: pi.inject intro: transitions.Output)
    ultimately show ?case by blast
  next
    case(Tau P)
    show ?case by auto
  next
    case(Input c x P)
    show ?case by auto
  next
    case(Match a b P)
    have "hnf ([a⌢b]P)" by fact
    hence False by simp
    thus ?case by simp
  next
    case(Mismatch a b P)
    have "hnf ([a≠b]P)" by fact
    hence False by simp
    thus ?case by simp
  next
    case(Sum P Q) 
    have "hnf (P ⊕ Q)" by fact
    hence Phnf: "hnf P" and Qhnf: "hnf Q" by simp+
    
    have IHP: "P ⟼a[b] ≺ P' = (a{b}.P' ∈ summands P)"
    proof -
      have "hnf P ⟹ P ⟼a[b] ≺ P' = (a{b}.P' ∈ summands P)" by fact
      with Phnf show ?thesis by simp
    qed
    
    have IHQ: "Q ⟼a[b] ≺ P' = (a{b}.P' ∈ summands Q)"
    proof -
      have "hnf Q ⟹ Q ⟼a[b] ≺ P' = (a{b}.P' ∈ summands Q)" by fact
      with Qhnf show ?thesis by simp
    qed

    from IHP IHQ have "P ⊕ Q ⟼a[b] ≺ P' ⟹ a{b}.P' ∈ summands (P ⊕ Q)"
      by(erule_tac sumCases, auto)
    moreover from IHP IHQ have "a{b}.P' ∈ summands (P ⊕ Q) ⟹ P ⊕ Q ⟼a[b] ≺ P'"
      by(auto dest: Sum1 Sum2)
    ultimately show ?case by blast
  next
    case(Par P Q)
    have "hnf (P ∥ Q)" by fact
    hence False by simp
    thus ?case by simp
  next
    case(Res x P)
    have "hnf (<νx>P)" by fact
    thus ?case by(force elim: resCasesF outputCases simp add: if_split residual.inject)
  next
    case(Bang P)
    have "hnf (!P)" by fact
    hence False by simp
    thus ?case by simp
  qed
next
  assume "a≠x"
  with assms show "P ⟼a<νx> ≺ P' = (<νx>a{x}.P' ∈ summands P)"
  proof(nominal_induct P avoiding: x P' rule: pi.strong_induct)
    case PiNil
    show ?case by auto
  next
    case(Output a b P)
    show ?case by auto 
  next
    case(Tau P)
    show ?case by auto
  next
    case(Input a x P)
    show ?case by auto
  next
    case(Match a b P)
    have "hnf ([a⌢b]P)" by fact
    hence False by simp
    thus ?case by simp
  next
    case(Mismatch a b P)
    have "hnf ([a≠b]P)" by fact
    hence False by simp
    thus ?case by simp
  next
    case(Sum P Q) 
    have "hnf (P ⊕ Q)" by fact
    hence Phnf: "hnf P" and Qhnf: "hnf Q" by simp+
    have aineqx: "a ≠ x" by fact

    have IHP: "P ⟼a<νx> ≺ P' = (<νx>a{x}.P' ∈ summands P)"
    proof -
      have "⋀x P'. ⟦hnf P; a ≠ x⟧ ⟹ P ⟼a<νx> ≺ P' = (<νx>a{x}.P' ∈ summands P)" by fact
      with Phnf aineqx show ?thesis by simp
    qed
    
    have IHQ: "Q ⟼a<νx> ≺ P' = (<νx>a{x}.P' ∈ summands Q)"
    proof -
      have "⋀x Q'. ⟦hnf Q; a ≠ x⟧ ⟹ Q ⟼a<νx> ≺ P' = (<νx>a{x}.P' ∈ summands Q)" by fact
      with Qhnf aineqx show ?thesis by simp
    qed

    from IHP IHQ have "P ⊕ Q ⟼a<νx> ≺ P' ⟹ <νx>a{x}.P' ∈ summands (P ⊕ Q)"
      by(erule_tac sumCases, auto)
    moreover from IHP IHQ have "<νx>a{x}.P' ∈ summands (P ⊕ Q) ⟹ P ⊕ Q ⟼a<νx> ≺ P'"
      by(auto dest: Sum1 Sum2)
    ultimately show ?case by blast
  next
    case(Par P Q)
    have "hnf (P ∥ Q)" by fact
    hence False by simp
    thus ?case by simp
  next
    case(Res y P)
    have Phnf: "hnf (<νy>P)" by fact
    then obtain b P'' where bineqy: "b ≠ y" and PeqP'': "P = b{y}.P''"
      by auto
    have "y ♯ x" by fact hence xineqy:  "x ≠ y" by simp
    have yFreshP': "y ♯ P'" by fact
    have aineqx: "a≠x" by fact
    have "<νy>P ⟼a<νx> ≺ P' ⟹ (<νx>a{x}.P' ∈ summands (<νy>P))"
    proof -
      assume Trans: "<νy>P ⟼a<νx> ≺ P'"
      hence  aeqb: "a = b" using xineqy bineqy PeqP''
        by(induct rule: resCasesB', auto elim: outputCases simp add: residual.inject alpha' abs_fresh pi.inject)

      have Goal: "⋀x P'. ⟦<νy>b{y}.P'' ⟼b<νx> ≺ P'; x ≠ y; x ≠ b; x ♯ P''⟧ ⟹
                           <νx>b{x}.P' ∈ summands(<νy>b{y}.P'')"
      proof -
        fix x P'
        assume xFreshP'': "(x::name) ♯ P''" and xineqb: "x ≠ b"
        assume "<νy>b{y}.P'' ⟼b<νx> ≺ P'" and xineqy: "x ≠ y"
        moreover from ‹x ≠ b› ‹x ♯ P''› ‹x ≠ y› have "x ♯ b{y}.P''" by simp
        ultimately show "<νx>b{x}.P' ∈ summands (<νy>b{y}.P'')"
        proof(induct rule: resCasesB)
          case(cOpen a P''')
          have "BoundOutputS b = BoundOutputS a" by fact hence beqa: "b = a" by simp
          have Trans: "b{y}.P'' ⟼a[y] ≺ P'''" by fact
          with PeqP'' have P''eqP''': "P'' = P'''"
            by(force elim: outputCases simp add: residual.inject)
          with bineqy xineqy xFreshP'' have "y ♯ b{x}.([(x, y)] ∙ P''')"
            by(simp add: name_fresh_abs name_calc name_fresh_left)
          with bineqy Phnf PeqP'' P''eqP''' xineqb show ?case 
            by(simp only: alphaRes, simp add: name_calc)
        next
          case(cRes P''')
          have "b{y}.P'' ⟼b<νx> ≺ P'''" by fact
          hence False by auto
          thus ?case by simp
        qed     
      qed
      obtain z where zineqx: "z ≠ x" and zineqy: "z ≠ y" and zFreshP'': "z ♯ P''" 
                 and zineqb: "z ≠ b" and zFreshP': "z ♯ P'"
        by(force intro: name_exists_fresh[of "(x, y, b, P'', P')"] simp add: fresh_prod)

      from zFreshP' aeqb PeqP'' Trans have Trans': "<νy>b{y}.P'' ⟼b<νz> ≺ [(z, x)] ∙ P'"
        by(simp add: alphaBoundResidual name_swap)
      hence "<νz>b{z}.([(z, x)] ∙ P') ∈ summands (<νy>b{y}.P'')" using zineqy zineqb zFreshP''
        by(rule Goal)
      moreover from bineqy zineqx zFreshP' aineqx aeqb have "x ♯ b{z}.([(z, x)] ∙ P')"
        by(simp add: name_fresh_left name_calc)
      ultimately have "<νx>b{x}.P' ∈ summands (<νy>b{y}.P'')" using zineqb
        by(simp add: alphaRes name_calc)
      with aeqb PeqP'' show ?thesis by blast
    qed
    moreover have "<νx>a{x}.P' ∈ summands(<νy>P) ⟹ <νy>P ⟼a<νx> ≺ P'"
    proof -
      assume "<νx>a{x}.P' ∈ summands(<νy>P)"
      with PeqP'' have Summ: "<νx>a{x}.P' ∈ summands(<νy>b{y}.P'')" by simp
      moreover with bineqy xineqy have aeqb: "a = b" 
        by(auto simp add: if_split pi.inject name_abs_eq name_fresh_fresh)
      from bineqy xineqy yFreshP' have "y ♯ b{x}.P'" by(simp add: name_calc)
      with Summ aeqb bineqy aineqx have "<νy>b{y}.([(x, y)] ∙ P') ∈ summands(<νy>b{y}.P'')"
        by(simp only: alphaRes, simp add: name_calc)
      with aeqb PeqP'' have "<νy>P ⟼a<νy> ≺ [(x, y)] ∙ P'"
        by(auto intro: Open Output simp add: if_split pi.inject name_abs_eq)
      moreover from yFreshP' have "x ♯ [(x, y)] ∙ P'" by(simp add: name_fresh_left name_calc)
      ultimately show ?thesis by(simp add: alphaBoundResidual name_swap)
    qed
    ultimately show ?case by blast
  next
    case(Bang P)
    have "hnf (!P)" by fact
    hence False by simp
    thus ?case by simp
  qed
qed

definition "expandSet" :: "pi ⇒ pi ⇒ pi set" where
          "expandSet P Q ≡ {τ.(P' ∥ Q) | P'. τ.(P') ∈ summands P} ∪ 
                           {τ.(P ∥ Q') | Q'. τ.(Q') ∈ summands Q} ∪ 
                           {a{b}.(P' ∥ Q) | a b P'. a{b}.P' ∈ summands P} ∪
                           {a{b}.(P ∥ Q') | a b Q'. a{b}.Q' ∈ summands Q} ∪
                           {a<x>.(P' ∥ Q) | a x P'. a<x>.P' ∈ summands P ∧ x ♯ Q} ∪
                           {a<x>.(P ∥ Q') | a x Q'. a<x>.Q' ∈ summands Q ∧ x ♯ P} ∪
                           {<νx>a{x}.(P' ∥ Q) | a x P'. <νx>a{x}.P' ∈ summands P ∧ x ♯ Q} ∪ 
                           {<νx>a{x}.(P ∥ Q') | a x Q'. <νx>a{x}.Q' ∈ summands Q ∧ x ♯ P} ∪ 
                           {τ.(P'[x::=b] ∥ Q') | x P' b Q'. ∃a. a<x>.P' ∈ summands P ∧ a{b}.Q' ∈ summands Q} ∪ 
                           {τ.(P' ∥ (Q'[x::=b])) | b P' x Q'. ∃a. a{b}.P' ∈ summands P ∧ a<x>.Q' ∈ summands Q} ∪ 
                           {τ.(<νy>(P'[x::=y] ∥ Q')) | x P' y Q'. ∃a. a<x>.P' ∈ summands P ∧ <νy>a{y}.Q' ∈ summands Q ∧ y ♯ P} ∪
                           {τ.(<νy>(P' ∥ (Q'[x::=y]))) | y P' x Q'. ∃a. <νy>a{y}.P' ∈ summands P ∧ a<x>.Q' ∈ summands Q ∧ y ♯ Q}"

lemma finiteExpand:
  fixes P :: pi
  and   Q :: pi

  shows "finite(expandSet P Q)"
proof -
  have "finite {τ.(P' ∥ Q) | P'. τ.(P') ∈ summands P}"
    by(induct P rule: pi.induct, auto simp add: pi.inject Collect_ex_eq conj_disj_distribL
                                                           Collect_disj_eq UN_Un_distrib)
  moreover have "finite {τ.(P ∥ Q') | Q'. τ.(Q') ∈ summands Q}"
    by(induct Q rule: pi.induct, auto simp add: pi.inject Collect_ex_eq conj_disj_distribL
                                                           Collect_disj_eq UN_Un_distrib)
  moreover have "finite {a{b}.(P' ∥ Q) | a b P'. a{b}.P' ∈ summands P}"
    by(induct P rule: pi.induct, auto simp add: pi.inject Collect_ex_eq conj_disj_distribL
                                                           Collect_disj_eq UN_Un_distrib)
  moreover have "finite {a{b}.(P ∥ Q') | a b Q'. a{b}.Q' ∈ summands Q}"
    by(induct Q rule: pi.induct, auto simp add: pi.inject Collect_ex_eq conj_disj_distribL
                                                           Collect_disj_eq UN_Un_distrib)
  moreover have "finite {a<x>.(P' ∥ Q) | a x P'. a<x>.P' ∈ summands P ∧ x ♯ Q}"
  proof -
    have Aux: "⋀a x P Q. (x::name) ♯ Q ⟹ {a'<x'>.(P' ∥ Q) |a' x' P'. a'<x'>.P' = a<x>.P ∧ x' ♯ Q} = {a<x>.(P ∥ Q)}"
      by(auto simp add: pi.inject name_abs_eq name_fresh_fresh)
    thus ?thesis
      by(nominal_induct P avoiding: Q rule: pi.strong_induct,
         auto simp add: Collect_ex_eq conj_disj_distribL conj_disj_distribR
                        Collect_disj_eq UN_Un_distrib)
  qed
  moreover have "finite {a<x>.(P ∥ Q') | a x Q'. a<x>.Q' ∈ summands Q ∧ x ♯ P}"
  proof -
    have Aux: "⋀a x P Q. (x::name) ♯ P ⟹ {a'<x'>.(P ∥ Q') |a' x' Q'. a'<x'>.Q' = a<x>.Q ∧ x' ♯ P} = {a<x>.(P ∥ Q)}"
      by(auto simp add: pi.inject name_abs_eq name_fresh_fresh)
    thus ?thesis
      by(nominal_induct Q avoiding: P rule: pi.strong_induct,
         auto simp add: Collect_ex_eq conj_disj_distribL conj_disj_distribR
                        Collect_disj_eq UN_Un_distrib)
  qed
  moreover have "finite {<νx>a{x}.(P' ∥ Q) | a x P'. <νx>a{x}.P' ∈ summands P ∧ x ♯ Q}"
  proof -
    have Aux: "⋀a x P Q. ⟦x ♯ Q; a ≠ x⟧ ⟹ {<νx'>a'{x'}.(P' ∥ Q) |a' x' P'. <νx'>a'{x'}.P' = <νx>a{x}.P ∧ x' ♯ Q} = 
                                             {<νx>a{x}.(P ∥ Q)}"
      by(auto simp add: pi.inject name_abs_eq name_fresh_fresh)
    thus ?thesis
      by(nominal_induct P avoiding: Q rule: pi.strong_induct, 
         auto simp add: Collect_ex_eq conj_disj_distribL conj_disj_distribR
                        Collect_disj_eq UN_Un_distrib)
  qed
  moreover have "finite {<νx>a{x}.(P ∥ Q') | a x Q'. <νx>a{x}.Q' ∈ summands Q ∧ x ♯ P}"
  proof -
    have Aux: "⋀a x P Q. ⟦x ♯ P; a ≠ x⟧ ⟹ {<νx'>a'{x'}.(P ∥ Q') |a' x' Q'. <νx'>a'{x'}.Q' = <νx>a{x}.Q ∧ x' ♯ P} = 
                                             {<νx>a{x}.(P ∥ Q)}"
      by(auto simp add: pi.inject name_abs_eq name_fresh_fresh)
    thus ?thesis
      by(nominal_induct Q avoiding: P rule: pi.strong_induct, 
         auto simp add: Collect_ex_eq conj_disj_distribL conj_disj_distribR
                        Collect_disj_eq UN_Un_distrib)
  qed
  moreover have "finite {τ.(P'[x::=b] ∥ Q') | x P' b Q'. ∃a. a<x>.P' ∈ summands P ∧ a{b}.Q' ∈ summands Q}"
  proof -
    have Aux: "⋀a x P b Q. {τ.(P'[x'::=b'] ∥ Q') | a' x' P' b' Q'. a'<x'>.P' = a<x>.P ∧ a'{b'}.Q' = a{b}.Q} = {τ.(P[x::=b] ∥ Q)}"
      by(auto simp add: name_abs_eq pi.inject renaming)
    have "⋀a x P Q b::'a::{}. finite {τ.(P'[x'::=b] ∥ Q') | a' x' P' b Q'. a'<x'>.P' = a<x>.P ∧ a'{b}.Q' ∈ summands Q}"
      apply(induct rule: pi.induct, simp_all)
      apply(case_tac "a=name1")
      apply(simp add: Aux)
      apply(simp add: pi.inject)
      by(simp add: Collect_ex_eq conj_disj_distribL conj_disj_distribR
                   Collect_disj_eq UN_Un_distrib)
    hence "finite {τ.(P'[x::=b] ∥ Q') | a x P' b Q'. a<x>.P' ∈ summands P ∧ a{b}.Q' ∈ summands Q}"
      by(nominal_induct P avoiding: Q rule: pi.strong_induct,
         auto simp add: Collect_ex_eq conj_disj_distribL conj_disj_distribR
                        Collect_disj_eq UN_Un_distrib name_abs_eq)
    thus ?thesis 
      apply(rule_tac finite_subset)
      defer
      by blast+
  qed
  moreover have "finite {τ.(P' ∥ (Q'[x::=b])) | b P' x Q'. ∃a. a{b}.P' ∈ summands P ∧ a<x>.Q' ∈ summands Q}"
  proof -
      have Aux: "⋀a x P b Q. {τ.(P' ∥ (Q'[x'::=b'])) | a' b' P' x' Q'. a'{b'}.P' = a{b}.P ∧ a'<x'>.Q' = a<x>.Q} = {τ.(P ∥ (Q[x::=b]))}"
        by(auto simp add: name_abs_eq pi.inject renaming)
      have "⋀a b P Q x::'a::{}. finite {τ.(P' ∥ (Q'[x::=b'])) | a' b' P' x Q'. a'{b'}.P' = a{b}.P ∧ a'<x>.Q' ∈ summands Q}"
      apply(induct rule: pi.induct, simp_all)
      apply(case_tac "a=name1")
      apply(simp add: Aux)
      apply(simp add: pi.inject)
      by(simp add: Collect_ex_eq conj_disj_distribL conj_disj_distribR
                     Collect_disj_eq UN_Un_distrib)
    hence "finite {τ.(P' ∥ (Q'[x::=b])) | a b P' x Q'. a{b}.P' ∈ summands P ∧ a<x>.Q' ∈ summands Q}"
      by(nominal_induct P avoiding: Q rule: pi.strong_induct,
         auto simp add: Collect_ex_eq conj_disj_distribL conj_disj_distribR
                        Collect_disj_eq UN_Un_distrib name_abs_eq)
    thus ?thesis
      apply(rule_tac finite_subset) defer by blast+
  qed
  moreover have "finite {τ.(<νy>(P'[x::=y] ∥ Q')) | x P' y Q'. ∃a. a<x>.P' ∈ summands P ∧ <νy>a{y}.Q' ∈ summands Q ∧ y ♯ P}"
  proof -
    have Aux: "⋀a x P y Q. y ♯ P ∧ y ≠ a ⟹ {τ.(<νy'>(P'[x'::=y'] ∥ Q')) | a' x' P' y' Q'. a'<x'>.P' = a<x>.P ∧ <νy'>a'{y'}.Q' = <νy>a{y}.Q ∧ y' ♯ a<x>.P} = {τ.(<νy>(P[x::=y] ∥ Q))}"
      apply(auto simp add: pi.inject name_abs_eq name_fresh_abs name_calc fresh_fact2 fresh_fact1 eqvts forget)
      apply(subst name_swap, simp add: injPermSubst fresh_fact1 fresh_fact2)+
      by(simp add: name_swap injPermSubst)+

    have BC: "⋀a x P Q. finite {τ.(<νy>(P'[x'::=y] ∥ Q')) | a' x' P' y Q'. a'<x'>.P' = a<x>.P ∧ <νy>a'{y}.Q' ∈ summands Q ∧ y ♯ a<x>.P}"
    proof -
      fix a x P Q
      show "finite {τ.(<νy>(P'[x'::=y] ∥ Q')) | a' x' P' y Q'. a'<x'>.P' = a<x>.P ∧ <νy>a'{y}.Q' ∈ summands Q ∧ y ♯ a<x>.P}"
        apply(nominal_induct Q avoiding: a P rule: pi.strong_induct, simp_all)
        apply(simp add: Collect_ex_eq conj_disj_distribL conj_disj_distribR
                        Collect_disj_eq UN_Un_distrib)
        apply(clarsimp)
        apply(case_tac "a=aa")
        apply(insert Aux, auto)
        by(simp add: pi.inject name_abs_eq name_calc)
    qed

    have IH: "⋀P P' Q. {τ.(<νy>(P''[x::=y] ∥ Q')) | a x P'' y Q'. (a<x>.P'' ∈ summands P ∨ a<x>.P'' ∈ summands P') ∧ <νy>a{y}.Q' ∈ summands Q ∧ y ♯ P ∧ y ♯ P'} = {τ.(<νy>(P''[x::=y] ∥ Q')) | a x P'' y Q'. a<x>.P'' ∈ summands P ∧ <νy>a{y}.Q' ∈ summands Q ∧ y ♯ P ∧ y ♯ P'} ∪ {τ.(<νy>(P''[x::=y] ∥ Q')) | a x P'' y Q'. a<x>.P'' ∈ summands P' ∧ <νy>a{y}.Q' ∈ summands Q ∧ y ♯ P ∧ y ♯ P'}"
      by blast
    have IH': "⋀P Q P'. {τ.(<νy>(P''[x::=y] ∥ Q')) | a x P'' y Q'. a<x>.P'' ∈ summands P ∧ <νy>a{y}.Q' ∈ summands Q ∧ y ♯ P ∧ y ♯ P'} ⊆ {τ.(<νy>(P''[x::=y] ∥ Q')) | a x P'' y Q'. a<x>.P'' ∈ summands P ∧ <νy>a{y}.Q' ∈ summands Q ∧ y ♯ P}"
      by blast
    have IH'': "⋀P Q P'. {τ.(<νy>(P''[x::=y] ∥ Q')) | a x P'' y Q'. a<x>.P'' ∈ summands P' ∧ <νy>a{y}.Q' ∈ summands Q ∧ y ♯ P ∧ y ♯ P'} ⊆ {τ.(<νy>(P''[x::=y] ∥ Q')) | a x P'' y Q'. a<x>.P'' ∈ summands P' ∧ <νy>a{y}.Q' ∈ summands Q ∧ y ♯ P'}"
      by blast
    have "finite {τ.(<νy>(P'[x::=y] ∥ Q')) | a x P' y Q'. a<x>.P' ∈ summands P ∧ <νy>a{y}.Q' ∈ summands Q ∧ y ♯ P}"
      apply(nominal_induct P avoiding: Q rule: pi.strong_induct, simp_all)
      apply(insert BC, force)
      apply(insert IH, auto)
      apply(blast intro: finite_subset[OF IH'])
      by(blast intro: finite_subset[OF IH''])
    thus ?thesis
      apply(rule_tac finite_subset) defer by(blast)+
  qed
  moreover have "finite {τ.(<νy>(P' ∥ (Q'[x::=y]))) | y P' x Q'. ∃a. <νy>a{y}.P' ∈ summands P ∧ a<x>.Q' ∈ summands Q ∧ y ♯ Q}"
  proof -
    have Aux: "⋀a y P x Q. ⟦y ♯ Q; y ≠ a⟧ ⟹ {τ.(<νy'>(P' ∥ (Q'[x'::=y']))) | a' y' P' x' Q'. <νy'>a'{y'}.P' = <νy>a{y}.P ∧ a'<x'>.Q' = a<x>.Q ∧ y' ♯ a<x>.Q} = {τ.(<νy>(P ∥ (Q[x::=y])))}"
      apply(auto simp add: pi.inject name_abs_eq name_fresh_abs name_calc fresh_fact2 fresh_fact1 forget eqvts fresh_left renaming[symmetric])
      apply(subst name_swap, simp add: injPermSubst fresh_fact1 fresh_fact2)+
      by(simp add: name_swap injPermSubst)+

    have IH: "⋀P y a Q Q'. {τ.(<νy'>(P' ∥ (Q''[x::=y']))) | a' y' P' x Q''. <νy'>a'{y'}.P' = <νy>a{y}.P ∧ (a'<x>.Q'' ∈ summands Q ∨ a'<x>.Q'' ∈ summands Q') ∧ y' ♯ Q ∧ y' ♯ Q'} = {τ.(<νy'>(P' ∥ (Q''[x::=y']))) | a' y' P' x Q''. <νy'>a'{y'}.P' = <νy>a{y}.P ∧ a'<x>.Q'' ∈ summands Q ∧ y' ♯ Q ∧ y' ♯ Q'} ∪ {τ.(<νy'>(P' ∥ (Q''[x::=y']))) | a' y' P' x Q''. <νy'>a'{y'}.P' = <νy>a{y}.P ∧ a'<x>.Q'' ∈ summands Q' ∧ y' ♯ Q ∧ y' ♯ Q'}"
      by blast
    have IH': "⋀a y P Q Q'. {τ.(<νy'>(P' ∥ (Q''[x::=y']))) | a' y' P' x Q''. <νy'>a'{y'}.P' = <νy>a{y}.P ∧ a'<x>.Q'' ∈ summands Q ∧ y' ♯ Q ∧ y' ♯ Q'} ⊆ {τ.(<νy'>(P' ∥ (Q''[x::=y']))) | a' y' P' x Q''. <νy'>a'{y'}.P' = <νy>a{y}.P ∧ a'<x>.Q'' ∈ summands Q ∧ y' ♯ Q}"
      by blast
    have IH'': "⋀a y P Q Q'. {τ.(<νy'>(P' ∥ (Q''[x::=y']))) | a' y' P' x Q''. <νy'>a'{y'}.P' = <νy>a{y}.P ∧ a'<x>.Q'' ∈ summands Q' ∧ y' ♯ Q ∧ y' ♯ Q'} ⊆ {τ.(<νy'>(P' ∥ (Q''[x::=y']))) | a' y' P' x Q''. <νy'>a'{y'}.P' = <νy>a{y}.P ∧ a'<x>.Q'' ∈ summands Q' ∧ y' ♯ Q'}"
      by blast

    have BC: "⋀a y P Q. ⟦y ♯ Q; y ≠ a⟧ ⟹ finite {τ.(<νy'>(P' ∥ (Q'[x::=y']))) | a' y' P' x Q'. <νy'>a'{y'}.P' = <νy>a{y}.P ∧ a'<x>.Q' ∈ summands Q ∧ y' ♯ Q}"
    proof -
      fix a y P Q
      assume "(y::name) ♯ (Q::pi)" and "y ≠ a"
      thus "finite {τ.(<νy'>(P' ∥ (Q'[x::=y']))) | a' y' P' x Q'. <νy'>a'{y'}.P' = <νy>a{y}.P ∧ a'<x>.Q' ∈ summands Q ∧ y' ♯ Q}"
        apply(nominal_induct Q avoiding: y rule: pi.strong_induct, simp_all)
        apply(case_tac "a=name1")
        apply auto
        apply(subgoal_tac "ya ♯ (pi::pi)")
        apply(insert Aux)
        apply auto
        apply(simp add: name_fresh_abs)
        apply(simp add: pi.inject name_abs_eq name_calc)
        apply(insert IH)
        apply auto
        apply(blast intro: finite_subset[OF IH'])
        by(blast intro: finite_subset[OF IH''])
    qed
    have "finite {τ.(<νy>(P' ∥ (Q'[x::=y]))) | a y P' x Q'. <νy>a{y}.P' ∈ summands P ∧ a<x>.Q' ∈ summands Q ∧ y ♯ Q}"

      apply(nominal_induct P avoiding: Q rule: pi.strong_induct, simp_all)
      apply(simp add: Collect_ex_eq conj_disj_distribL conj_disj_distribR name_fresh_abs
                      Collect_disj_eq UN_Un_distrib)
      by(auto intro: BC)
    thus ?thesis
      apply(rule_tac finite_subset) defer by blast+
  qed

  ultimately show ?thesis
    by(simp add: expandSet_def)
qed

lemma expandHnf:
  fixes P :: pi
  and   Q :: pi

  shows "∀R ∈ (expandSet P Q). hnf R"
by(force simp add: expandSet_def)

inductive_set sumComposeSet :: "(pi × pi set) set"
where
  empty:  "(𝟬, {}) ∈ sumComposeSet"
| insert: "⟦Q ∈ S; (P, S - {Q}) ∈ sumComposeSet⟧ ⟹ (P ⊕ Q, S) ∈ sumComposeSet"

lemma expandAction:
  fixes P :: pi
  and   Q :: pi
  and   S :: "pi set"

  assumes "(P, S) ∈ sumComposeSet"
  and     "Q ∈ S"
  and     "Q ⟼ Rs"

  shows "P ⟼ Rs"
using assms
proof(induct arbitrary: Q rule: sumComposeSet.induct)
  case empty
  have "Q ∈ {}" by fact
  hence False by simp
  thus ?case by simp
next
  case(insert Q' S P Q)
  have QTrans: "Q ⟼ Rs" by fact
  show ?case
  proof(case_tac "Q = Q'")
    assume "Q = Q'"
    with QTrans show "P ⊕ Q' ⟼ Rs" by(blast intro: Sum2)
  next
    assume QineqQ': "Q ≠ Q'"
    have IH: "⋀Q. ⟦Q ∈ S - {Q'}; Q ⟼ Rs⟧ ⟹ P ⟼ Rs" by fact
    have QinS: "Q ∈ S" by fact
    with QineqQ' have "Q ∈ S - {Q'}" by simp
    hence "P ⟼ Rs" using QTrans by(rule IH)
    thus ?case by(rule Sum1)
  qed
qed

lemma expandAction':
  fixes P :: pi
  and   Q :: pi
  and   R :: pi

  assumes "(R, S) ∈ sumComposeSet"
  and     "R ⟼ Rs"

  shows "∃P ∈ S. P ⟼ Rs"
using assms
proof(induct rule: sumComposeSet.induct)
  case empty
  have "𝟬 ⟼ Rs" by fact
  hence False by blast
  thus ?case by simp
next
  case(insert Q S P)
  have QinS: "Q ∈ S" by fact
  have "P ⊕ Q ⟼ Rs" by fact
  thus ?case
  proof(induct rule: sumCases)
    case cSum1
    have "P ⟼ Rs" by fact
    moreover have "P ⟼ Rs ⟹ ∃P ∈ (S - {Q}). P ⟼ Rs" by fact
    ultimately obtain P where PinS: "P ∈ (S - {Q})" and PTrans: "P ⟼ Rs" by blast
    show ?case
    proof(case_tac "P = Q")
      assume "P = Q"
      with PTrans QinS show ?case by blast
    next
      assume PineqQ: "P ≠ Q"
      from PinS have "P ∈ S" by simp
      with PTrans show ?thesis by blast
    qed
  next
    case cSum2
    have "Q ⟼ Rs" by fact
    with QinS show ?case by blast
  qed
qed

lemma expandTrans:
  fixes P :: pi
  and   Q :: pi
  and   R :: pi
  and   a :: name
  and   b :: name
  and   x :: name

  assumes Exp: "(R, expandSet P Q) ∈ sumComposeSet"
  and     Phnf: "hnf P"
  and     Qhnf: "hnf Q"

  shows "(P ∥ Q ⟼τ ≺ P') = (R ⟼τ ≺ P')"
  and   "(P ∥ Q ⟼a[b] ≺ P') = (R ⟼a[b] ≺ P')"
  and   "(P ∥ Q ⟼a<x> ≺ P') = (R ⟼a<x> ≺ P')"
  and   "(P ∥ Q ⟼a<νx> ≺ P') = (R ⟼a<νx> ≺ P')"
proof -
  show "P ∥ Q ⟼ τ ≺ P' = R ⟼ τ ≺ P'"
  proof(rule iffI)
    assume "P ∥ Q ⟼τ ≺ P'"
    thus "R ⟼τ ≺ P'"
    proof(induct rule: parCasesF[of _ _ _ _ _ "(P, Q)"])
      case(cPar1 P')
      have "P ⟼τ ≺ P'" by fact
      with Phnf have "τ.(P') ∈ summands P" by(simp add: summandTransition)
      hence "τ.(P' ∥ Q) ∈ expandSet P Q" by(auto simp add: expandSet_def)
      moreover have "τ.(P' ∥ Q) ⟼τ ≺ (P' ∥ Q)" by(rule Tau)
      ultimately show ?case using Exp by(blast intro: expandAction)
    next
      case(cPar2 Q')
      have "Q ⟼τ ≺ Q'" by fact
      with Qhnf have "τ.(Q') ∈ summands Q" by(simp add: summandTransition)
      hence "τ.(P ∥ Q') ∈ expandSet P Q" by(auto simp add: expandSet_def)
      moreover have "τ.(P ∥ Q') ⟼τ ≺ (P ∥ Q')" by(rule Tau)
      ultimately show ?case using Exp by(blast intro: expandAction)
    next
      case(cComm1 P' Q' a b x)
      have "P ⟼a<x> ≺ P'" and "Q ⟼a[b] ≺ Q'" by fact+
      with Phnf Qhnf have "a<x>.P' ∈ summands P" and "a{b}.Q' ∈ summands Q" by(simp add: summandTransition)+
      hence "τ.(P'[x::=b] ∥ Q') ∈ expandSet P Q" by(simp add: expandSet_def, blast)
      moreover have "τ.(P'[x::=b] ∥ Q') ⟼τ ≺ (P'[x::=b] ∥ Q')" by(rule Tau)
      ultimately show ?case using Exp by(blast intro: expandAction)
    next
      case(cComm2 P' Q' a b x)
      have "P ⟼a[b] ≺ P'" and "Q ⟼a<x> ≺ Q'" by fact+
      with Phnf Qhnf have "a{b}.P' ∈ summands P" and "a<x>.Q' ∈ summands Q" by(simp add: summandTransition)+
      hence "τ.(P' ∥ (Q'[x::=b])) ∈ expandSet P Q" by(simp add: expandSet_def, blast)
      moreover have "τ.(P' ∥ (Q'[x::=b])) ⟼τ ≺ (P' ∥ (Q'[x::=b]))" by(rule Tau)
      ultimately show ?case using Exp by(blast intro: expandAction)
    next
      case(cClose1 P' Q' a x y)
      have "y ♯ (P, Q)" by fact
      hence yFreshP: "y ♯ P" by(simp add: fresh_prod)
      have PTrans: "P ⟼a<x> ≺ P'" by fact
      with Phnf have PSumm: "a<x>.P' ∈ summands P" by(simp add: summandTransition)
      have "Q ⟼a<νy> ≺ Q'" by fact
      moreover from PTrans yFreshP have "y ≠ a" by(force dest: freshBoundDerivative)
      ultimately have "<νy>a{y}.Q' ∈ summands Q" using Qhnf by(simp add: summandTransition)
      with PSumm yFreshP have "τ.(<νy>(P'[x::=y] ∥ Q')) ∈ expandSet P Q"
        by(auto simp add: expandSet_def)
      moreover have "τ.(<νy>(P'[x::=y] ∥ Q')) ⟼τ ≺ <νy>(P'[x::=y] ∥ Q')" by(rule Tau)
      ultimately show ?case using Exp by(blast intro: expandAction)
    next
      case(cClose2 P' Q' a x y)
      have "y ♯ (P, Q)" by fact
      hence yFreshQ: "y ♯ Q" by(simp add: fresh_prod)
      have QTrans: "Q ⟼a<x> ≺ Q'" by fact
      with Qhnf have QSumm: "a<x>.Q' ∈ summands Q" by(simp add: summandTransition)
      have "P ⟼a<νy> ≺ P'" by fact
      moreover from QTrans yFreshQ have "y ≠ a" by(force dest: freshBoundDerivative)
      ultimately have "<νy>a{y}.P' ∈ summands P" using Phnf by(simp add: summandTransition)
      with QSumm yFreshQ have "τ.(<νy>(P' ∥ (Q'[x::=y]))) ∈ expandSet P Q"
        by(simp add: expandSet_def, blast)
      moreover have "τ.(<νy>(P' ∥ (Q'[x::=y]))) ⟼τ ≺ <νy>(P' ∥ (Q'[x::=y]))" by(rule Tau)
      ultimately show ?case using Exp by(blast intro: expandAction)
    qed
  next
    assume "R ⟼τ ≺ P'"
    with Exp obtain R where "R ∈ expandSet P Q" and "R ⟼τ ≺ P'" by(blast dest: expandAction')
    thus "P ∥ Q ⟼τ ≺ P'"
    proof(auto simp add: expandSet_def)
      fix P''
      assume "τ.(P'') ∈ summands P"
      with Phnf have "P ⟼τ ≺ P''" by(simp add: summandTransition)
      hence PQTrans: "P ∥ Q ⟼τ ≺ P'' ∥ Q" by(rule Par1F)
      assume "τ.(P'' ∥ Q) ⟼τ ≺ P'"
      hence "P' = P'' ∥ Q" by(erule_tac tauCases, auto simp add: pi.inject residual.inject)
      with PQTrans show ?thesis by simp
    next
      fix Q'
      assume "τ.(Q') ∈ summands Q"
      with Qhnf have "Q ⟼τ ≺ Q'" by(simp add: summandTransition)
      hence PQTrans: "P ∥ Q ⟼τ ≺ P ∥ Q'" by(rule Par2F)
      assume "τ.(P ∥ Q') ⟼τ ≺ P'"
      hence "P' = P ∥ Q'" by(erule_tac tauCases, auto simp add: pi.inject residual.inject)
      with PQTrans show ?thesis by simp
    next
      fix a x P'' b Q'
      assume "a<x>.P'' ∈ summands P" and "a{b}.Q' ∈ summands Q"
      with Phnf Qhnf have "P ⟼a<x> ≺ P''" and "Q ⟼a[b] ≺ Q'" by(simp add: summandTransition)+
      hence PQTrans: "P ∥ Q ⟼τ ≺ P''[x::=b] ∥ Q'" by(rule Comm1)
      assume "τ.(P''[x::=b] ∥ Q') ⟼τ ≺ P'"
      hence "P' = P''[x::=b] ∥ Q'" by(erule_tac tauCases, auto simp add: pi.inject residual.inject)
      with PQTrans show ?thesis by simp
    next
      fix a b P'' x Q'
      assume "a{b}.P'' ∈ summands P" and "a<x>.Q' ∈ summands Q"
      with Phnf Qhnf have "P ⟼a[b] ≺ P''" and "Q ⟼a<x> ≺ Q'" by(simp add: summandTransition)+
      hence PQTrans: "P ∥ Q ⟼τ ≺ P'' ∥ (Q'[x::=b])" by(rule Comm2)
      assume "τ.(P'' ∥ (Q'[x::=b])) ⟼τ ≺ P'"
      hence "P' = P'' ∥ (Q'[x::=b])" by(erule_tac tauCases, auto simp add: pi.inject residual.inject)
      with PQTrans show ?thesis by simp
    next
      fix a x P'' y Q'
      assume yFreshP: "(y::name) ♯ P"
      assume "a<x>.P'' ∈ summands P" 
      with Phnf have PTrans: "P ⟼a<x> ≺ P''" by(simp add: summandTransition)
      assume "<νy>a{y}.Q' ∈ summands Q"
      moreover from yFreshP PTrans have "y ≠ a" by(force dest: freshBoundDerivative)
      ultimately have "Q ⟼a<νy> ≺ Q'" using Qhnf by(simp add: summandTransition)
      with PTrans have PQTrans: "P ∥ Q ⟼τ ≺ <νy>(P''[x::=y] ∥ Q')" using yFreshP by(rule Close1)
      assume "τ.(<νy>(P''[x::=y] ∥ Q')) ⟼τ ≺ P'"
      hence "P' = <νy>(P''[x::=y] ∥ Q')" by(erule_tac tauCases, auto simp add: pi.inject residual.inject)
      with PQTrans show ?thesis by simp
    next
      fix a y P'' x Q'
      assume yFreshQ: "(y::name) ♯ Q"
      assume "a<x>.Q' ∈ summands Q" 
      with Qhnf have QTrans: "Q ⟼a<x> ≺ Q'" by(simp add: summandTransition)
      assume "<νy>a{y}.P'' ∈ summands P"
      moreover from yFreshQ QTrans have "y ≠ a" by(force dest: freshBoundDerivative)
      ultimately have "P ⟼a<νy> ≺ P''" using Phnf by(simp add: summandTransition)
      hence PQTrans: "P ∥ Q ⟼τ ≺ <νy>(P'' ∥ Q'[x::=y])" using QTrans yFreshQ by(rule Close2)
      assume "τ.(<νy>(P'' ∥ Q'[x::=y])) ⟼τ ≺ P'"
      hence "P' = <νy>(P'' ∥ Q'[x::=y])" by(erule_tac tauCases, auto simp add: pi.inject residual.inject)
      with PQTrans show ?thesis by simp
    qed
  qed
next
  show "P ∥ Q ⟼ a[b] ≺ P' = R ⟼ a[b] ≺ P'"
  proof(rule iffI)
    assume "P ∥ Q ⟼a[b] ≺ P'"
    thus "R ⟼a[b] ≺ P'"
    proof(induct rule: parCasesF[where C="()"])
      case(cPar1 P')
      have "P ⟼a[b] ≺ P'" by fact
      with Phnf have "a{b}.P' ∈ summands P" by(simp add: summandTransition)
      hence "a{b}.(P' ∥ Q) ∈ expandSet P Q" by(auto simp add: expandSet_def)
      moreover have "a{b}.(P' ∥ Q) ⟼a[b] ≺ (P' ∥ Q)" by(rule Output)
      ultimately show ?case using Exp by(blast intro: expandAction)
    next
      case(cPar2 Q')
      have "Q ⟼a[b] ≺ Q'" by fact
      with Qhnf have "a{b}.Q' ∈ summands Q" by(simp add: summandTransition)
      hence "a{b}.(P ∥ Q') ∈ expandSet P Q" by(simp add: expandSet_def, blast)
      moreover have "a{b}.(P ∥ Q') ⟼a[b] ≺ (P ∥ Q')" by(rule Output)
      ultimately show ?case using Exp by(blast intro: expandAction)
    next 
      case cComm1
      thus ?case by auto
    next 
      case cComm2
      thus ?case by auto
    next 
      case cClose1
      thus ?case by auto
    next 
      case cClose2
      thus ?case by auto
    qed
  next
    assume "R ⟼a[b] ≺ P'"
    with Exp obtain R where "R ∈ expandSet P Q" and "R ⟼a[b] ≺ P'" by(blast dest: expandAction')
    thus "P ∥ Q ⟼a[b] ≺ P'"
    proof(auto simp add: expandSet_def)
      fix a' b' P''
      assume "a'{b'}.P'' ∈ summands P"
      with Phnf have "P ⟼a'[b'] ≺ P''" by(simp add: summandTransition)
      hence PQTrans: "P ∥ Q ⟼a'[b'] ≺ P'' ∥ Q" by(rule Par1F)
      assume "a'{b'}.(P'' ∥ Q) ⟼a[b] ≺ P'"
      hence "P' = P'' ∥ Q" and "a = a'" and "b = b'"
        by(erule_tac outputCases, auto simp add: pi.inject residual.inject)+
      with PQTrans show ?thesis by simp
    next
      fix a' b' Q'
      assume "a'{b'}.Q' ∈ summands Q"
      with Qhnf have "Q ⟼a'[b'] ≺ Q'" by(simp add: summandTransition)
      hence PQTrans: "P ∥ Q ⟼a'[b'] ≺ P ∥ Q'" by(rule Par2F)
      assume "a'{b'}.(P ∥ Q') ⟼a[b] ≺ P'"
      hence "P' = P ∥ Q'" and "a = a'" and "b = b'"
        by(erule_tac outputCases, auto simp add: pi.inject residual.inject)+
      with PQTrans show ?thesis by simp
    qed
  qed
next
  show "P ∥ Q ⟼ a<x> ≺ P' = R ⟼ a<x> ≺ P'"
  proof(rule iffI)
    {
      fix x P'
      assume "P ∥ Q ⟼a<x> ≺ P'" and "x ♯ P" and "x ♯ Q"
      hence "R ⟼a<x> ≺ P'"
      proof(induct rule: parCasesB)
        case(cPar1 P')
        have "P ⟼a<x> ≺ P'" by fact
        with Phnf have "a<x>.P' ∈ summands P" by(simp add: summandTransition)
        moreover have "x ♯ Q" by fact
        ultimately have "a<x>.(P' ∥ Q) ∈ expandSet P Q" by(auto simp add: expandSet_def)
        moreover have "a<x>.(P' ∥ Q) ⟼a<x> ≺ (P' ∥ Q)" by(rule Input)
        ultimately show ?case using Exp by(blast intro: expandAction)
      next
        case(cPar2 Q')
        have "Q ⟼a<x> ≺ Q'" by fact
        with Qhnf have "a<x>.Q' ∈ summands Q" by(simp add: summandTransition)
        moreover have "x ♯ P" by fact
        ultimately have "a<x>.(P ∥ Q') ∈ expandSet P Q" by(simp add: expandSet_def, blast)
        moreover have "a<x>.(P ∥ Q') ⟼a<x> ≺ (P ∥ Q')" by(rule Input)
        ultimately show ?case using Exp by(blast intro: expandAction)
      qed
    }
    moreover obtain y::name where "y ♯ P" and "y ♯ Q" and "y ♯ P'"
      by(generate_fresh "name") auto
    assume "P ∥ Q ⟼a<x> ≺ P'"
    with ‹y ♯ P'› have "P ∥ Q ⟼a<y> ≺ ([(x, y)] ∙ P')"
      by(simp add: alphaBoundResidual)
    ultimately have "R ⟼a<y> ≺ ([(x, y)] ∙ P')" using ‹y ♯ P› ‹y ♯ Q›
      by auto
    thus "R ⟼a<x> ≺ P'" using ‹y ♯ P'› by(simp add: alphaBoundResidual)
  next
    assume "R ⟼a<x> ≺ P'"
    with Exp obtain R where "R ∈ expandSet P Q" and "R ⟼a<x> ≺ P'" by(blast dest: expandAction')
    thus "P ∥ Q ⟼a<x> ≺ P'"
    proof(auto simp add: expandSet_def)
      fix a' y P''
      assume "a'<y>.P'' ∈ summands P"
      with Phnf have "P ⟼a'<y> ≺ P''" by(simp add: summandTransition)
      moreover assume "y ♯ Q"
      ultimately have PQTrans: "P ∥ Q ⟼a'<y> ≺ P'' ∥ Q" by(rule Par1B)
      assume "a'<y>.(P'' ∥ Q) ⟼a<x> ≺ P'"
      hence "a<x> ≺ P' = a'<y> ≺ P'' ∥ Q" and "a = a'"
        by(erule_tac inputCases', auto simp add: pi.inject residual.inject)+
      with PQTrans show ?thesis by simp
    next
      fix a' y Q'
      assume "a'<y>.Q' ∈ summands Q"
      with Qhnf have "Q ⟼(a'::name)<y> ≺ Q'" by(simp add: summandTransition)
      moreover assume "y ♯ P"
      ultimately have PQTrans: "P ∥ Q ⟼a'<y> ≺ P ∥ Q'" by(rule Par2B)
      assume "a'<y>.(P ∥ Q') ⟼a<x> ≺ P'"
      hence "a<x> ≺ P' = a'<y> ≺ P ∥ Q'" and "a = a'"
        by(erule_tac inputCases', auto simp add: pi.inject residual.inject)+
      with PQTrans show ?thesis by simp
    qed
  qed
next
  have Goal: "⋀P Q a x P' R. ⟦(R, expandSet P Q) ∈ sumComposeSet; hnf P; hnf Q; a ≠ x⟧ ⟹ P ∥ Q ⟼a<νx> ≺ P' = R ⟼a<νx> ≺ P'"
  proof -
    fix P Q a x P' R
    assume aineqx: "(a::name) ≠ x"
    assume Exp: "(R, expandSet P Q) ∈ sumComposeSet"
    assume Phnf: "hnf P"
    assume Qhnf: "hnf Q"
    show "P ∥ Q ⟼a<νx> ≺ P' = R ⟼ a<νx> ≺ P'"
    proof(rule iffI)
      {
        fix x P'
        assume "P ∥ Q ⟼a<νx> ≺ P'" and "x ♯ P" and "x ♯ Q" and "a ≠ x"
        hence "R ⟼a<νx> ≺ P'"
        proof(induct rule: parCasesB)
          case(cPar1 P')
          have "P ⟼a<νx> ≺ P'" by fact
          with Phnf ‹a ≠ x› have "<νx>a{x}.P' ∈ summands P" by(simp add: summandTransition)
          moreover have "x ♯ Q" by fact
          ultimately have "<νx>a{x}.(P' ∥ Q) ∈ expandSet P Q" by(auto simp add: expandSet_def)
          moreover have "<νx>a{x}.(P' ∥ Q) ⟼a<νx> ≺ (P' ∥ Q)" using ‹a ≠ x›
            by(blast intro: Open Output)
          ultimately show ?case using Exp by(blast intro: expandAction)
        next
          case(cPar2 Q')
          have "Q ⟼a<νx> ≺ Q'" by fact
          with Qhnf ‹a ≠ x› have "<νx>a{x}.Q' ∈ summands Q" by(simp add: summandTransition)
          moreover have "x ♯ P" by fact
          ultimately have "<νx>a{x}.(P ∥ Q') ∈ expandSet P Q" by(simp add: expandSet_def, blast)
          moreover have "<νx>a{x}.(P ∥ Q') ⟼a<νx> ≺ (P ∥ Q')" using ‹a ≠ x›
            by(blast intro: Open Output)
          ultimately show ?case using Exp by(blast intro: expandAction)
        qed
      }
      moreover obtain y::name where "y ♯ P" and "y ♯ Q" and "y ♯ P'" and "y ≠ a"
        by(generate_fresh "name") auto
      assume "P ∥ Q ⟼a<νx> ≺ P'"
      with ‹y ♯ P'› have "P ∥ Q ⟼a<νy> ≺ ([(x, y)] ∙ P')"
        by(simp add: alphaBoundResidual)
      ultimately have "R ⟼a<νy> ≺ ([(x, y)] ∙ P')" using ‹y ♯ P› ‹y ♯ Q› ‹y ≠ a›
        by auto
      thus "R ⟼a<νx> ≺ P'" using ‹y ♯ P'› by(simp add: alphaBoundResidual)
    next
      {
        fix R x P'
        assume "R ⟼a<νx> ≺ P'" and "R ∈ expandSet P Q" and "x ♯ R" and "x ♯ P" and "x ♯ Q"
        hence "P ∥ Q ⟼a<νx> ≺ P'" 
        proof(auto simp add: expandSet_def)
          fix a' y P''
          assume "<νy>a'{y}.P'' ∈ summands P"
          moreover hence "a' ≠ y" by auto
          ultimately have "P ⟼a'<νy> ≺ P''" using Phnf by(simp add: summandTransition)
          moreover assume "y ♯ Q"
          ultimately have PQTrans: "P ∥ Q ⟼a'<νy> ≺ P'' ∥ Q" by(rule Par1B)
          assume ResTrans: "<νy>a'{y}.(P'' ∥ Q) ⟼a<νx> ≺ P'" and "x ♯ [y].a'{y}.(P'' ∥ Q)"
          with ResTrans ‹a' ≠ y› ‹x ♯ P› ‹x ♯ Q› have "a<νx> ≺ P' = a'<νy> ≺ P'' ∥ Q"
            apply(case_tac "x=y")
            defer
            apply(erule_tac resCasesB)
            apply simp
            apply(simp add: abs_fresh)
            apply(auto simp add: residual.inject alpha' calc_atm fresh_left abs_fresh elim: outputCases)
            apply(ind_cases "<νy>a'{y}.(P'' ∥ Q) ⟼ a<νy> ≺ P'")
            apply(simp add: pi.inject alpha' residual.inject abs_fresh eqvts calc_atm)
            apply(auto elim: outputCases)
            apply(simp add: pi.inject residual.inject alpha' calc_atm)
            apply auto
            apply(ind_cases "<νy>a'{y}.(P'' ∥ Q) ⟼ a<νy> ≺ P'")
            apply(auto simp add: pi.inject alpha' residual.inject abs_fresh eqvts calc_atm)
            apply(auto elim: outputCases)
            apply(erule_tac outputCases)
            apply(auto simp add: freeRes.inject)
            apply hypsubst_thin
            apply(drule_tac pi="[(b, y)]" in pt_bij3)
            by simp
        with PQTrans show ?thesis by simp
      next
        fix a' y Q'
        assume "<νy>a'{y}.Q' ∈ summands Q"
        moreover hence "a' ≠ y" by auto
        ultimately have "Q ⟼a'<νy> ≺ Q'" using Qhnf by(simp add: summandTransition)
        moreover assume "y ♯ P"
        ultimately have PQTrans: "P ∥ Q ⟼a'<νy> ≺ P ∥ Q'" by(rule Par2B)
        assume ResTrans: "<νy>a'{y}.(P ∥ Q') ⟼a<νx> ≺ P'" and "x ♯ [y].a'{y}.(P ∥ Q')"
        with ResTrans ‹a' ≠ y› have "a<νx> ≺ P' = a'<νy> ≺ P ∥ Q'"
          apply(case_tac "x=y")
          defer
          apply(erule_tac resCasesB)
            apply simp
            apply(simp add: abs_fresh)
            apply(auto simp add: residual.inject alpha' calc_atm fresh_left abs_fresh elim: outputCases)
            apply(ind_cases "<νy>a'{y}.(P ∥ Q') ⟼ a<νy> ≺ P'")
            apply(simp add: pi.inject alpha' residual.inject abs_fresh eqvts calc_atm)
            apply(auto elim: outputCases)
            apply(simp add: pi.inject residual.inject alpha' calc_atm)
            apply auto
            apply(ind_cases "<νy>a'{y}.(P ∥ Q') ⟼ a<νy> ≺ P'")
            apply(auto simp add: pi.inject alpha' residual.inject abs_fresh eqvts calc_atm)
            apply(auto elim: outputCases)
            apply(erule_tac outputCases)
            apply(auto simp add: freeRes.inject)
            apply hypsubst_thin
            apply(drule_tac pi="[(b, y)]" in pt_bij3)
            by simp
        with PQTrans show ?thesis by simp
      qed
    }
    moreover assume "R ⟼a<νx> ≺ P'"
    with Exp obtain R where "R ∈ expandSet P Q" and "R ⟼a<νx> ≺ P'" 
      apply(drule_tac expandAction') by auto
    moreover obtain y::name where "y ♯ P" and "y ♯ Q" and "y ♯ R" and "y ♯ P'"
      by(generate_fresh "name") auto
    moreover with ‹y ♯ P'› ‹R ⟼a<νx> ≺ P'› have "R ⟼a<νy> ≺ ([(x, y)] ∙ P')" by(simp add: alphaBoundResidual)
    ultimately have "P ∥ Q ⟼a<νy> ≺ ([(x, y)] ∙ P')" by auto
    thus "P ∥ Q ⟼a<νx> ≺ P'" using ‹y ♯ P'› by(simp add: alphaBoundResidual)
    qed
  qed

  obtain y where yineqx: "a ≠ y" and yFreshP': "y ♯ P'"
    by(force intro: name_exists_fresh[of "(a, P')"] simp add: fresh_prod)
  from Exp Phnf Qhnf yineqx have "(P ∥ Q ⟼a<νy> ≺ [(x, y)] ∙ P') = (R ⟼a<νy> ≺ [(x, y)] ∙ P')"
    by(rule Goal)
  moreover with yFreshP' have "x ♯ [(x, y)] ∙ P'" by(simp add: name_fresh_left name_calc)
  ultimately show "(P ∥ Q ⟼a<νx> ≺ P') = (R ⟼a<νx> ≺ P')"
    by(simp add: alphaBoundResidual name_swap)
qed

lemma expandLeft:
  fixes P   :: pi
  and   Q   :: pi
  and   R   :: pi
  and   Rel :: "(pi × pi) set"

  assumes Exp: "(R, expandSet P Q) ∈ sumComposeSet"
  and     Phnf: "hnf P"
  and     Qhnf: "hnf Q"
  and     Id: "Id ⊆ Rel"

  shows "P ∥ Q ↝[Rel] R"
proof(induct rule: simCases)
  case(Bound a x R')
  have "R ⟼a«x» ≺ R'" by fact
  with Exp Phnf Qhnf have "P ∥ Q ⟼a«x» ≺ R'" by(cases a, auto simp add: expandTrans)
  moreover from Id have "derivative R' R' a x Rel" by(cases a, auto simp add: derivative_def)
  ultimately show ?case by blast
next
  case(Free α R')
  have "R ⟼α ≺ R'" by fact
  with Exp Phnf Qhnf have "P ∥ Q ⟼α ≺ R'" by(cases α, auto simp add: expandTrans)
  moreover from Id have "(R', R') ∈ Rel" by blast
  ultimately show ?case by blast
qed

lemma expandRight:
  fixes P   :: pi
  and   Q   :: pi
  and   R   :: pi
  and   Rel :: "(pi × pi) set"

  assumes Exp: "(R, expandSet P Q) ∈ sumComposeSet"
  and     Phnf: "hnf P"
  and     Qhnf: "hnf Q"
  and     Id: "Id ⊆ Rel"

  shows "R ↝[Rel] P ∥ Q"
proof(induct rule: simCases)
  case(Bound a x R')
  have "P ∥ Q ⟼a«x» ≺ R'" by fact
  with Exp Phnf Qhnf have "R ⟼a«x» ≺ R'" by(cases a, auto simp add: expandTrans)
  moreover from Id have "derivative R' R' a x Rel" by(cases a, auto simp add: derivative_def)
  ultimately show ?case by blast
next
  case(Free α R')
  have "P ∥ Q ⟼α ≺ R'" by fact
  with Exp Phnf Qhnf have "R ⟼α ≺ R'" by(cases α, auto simp add: expandTrans)
  moreover from Id have "(R', R') ∈ Rel" by blast
  ultimately show ?case by blast
qed

lemma expandSC: 
  fixes P :: pi
  and   Q :: pi
  and   R :: pi
  
  assumes "(R, expandSet P Q) ∈ sumComposeSet"
  and     "hnf P"
  and     "hnf Q"

  shows "P ∥ Q ∼ R"
proof -
  let ?X = "{(P ∥ Q, R) | P Q R. (R, expandSet P Q) ∈ sumComposeSet ∧ hnf P ∧ hnf Q} ∪ {(R, P ∥ Q) | P Q R. (R, expandSet P Q) ∈ sumComposeSet ∧ hnf P ∧ hnf Q}"
  from assms have "(P ∥ Q, R) ∈ ?X" by auto
  thus ?thesis
  proof(coinduct rule: bisimCoinduct)
    case(cSim P Q)
    thus ?case
      by(blast intro: reflexive expandLeft expandRight)
  next
    case(cSym P Q)
     thus ?case by auto
   qed
 qed

end