Theory Early_Semantics

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

declare name_fresh[simp del]

nominal_datatype freeRes = InputR name name              (‹_<_> [110, 110] 110)
                         | OutputR name name             (‹_[_] [110, 110] 110)
                         | TauR                          (τ 110)

nominal_datatype residual = BoundOutputR name "«name» pi" (‹__>  _› [110, 110, 110] 110)
                          | FreeR freeRes pi

lemma alphaBoundOutput:
  fixes a  :: name
  and   x  :: name
  and   P  :: pi
  and   x' :: name

  assumes A1: "x'  P"

  shows "ax>  P = ax'>  ([(x, x')]  P)"
proof(cases "x=x'")
  assume "x=x'"
  thus ?thesis by simp
next
  assume "x  x'"
  with A1 show ?thesis
    by(simp add: residual.inject alpha name_fresh_left name_calc)
qed

declare name_fresh[simp]

abbreviation Transitions_Freejudge (‹_  _› [80, 80] 80) where "α  P'  (FreeR α P')"

inductive "TransitionsEarly" :: "pi  residual  bool" (‹_  _› [80, 80] 80)
where
  Tau:               "τ.(P)  τ  P"
| Input:             "x  a; x  u  a<x>.P  a<u>  (P[x::=u])"
| Output:            "a{b}.P  a[b]   P"

| Match:             "P  V  [bb]P  V"
| Mismatch:          "P  V; a  b  [ab]P  V"

| Open:              "P  a[b]  P'; a  b  b>P  ab>  P'"
| Sum1:              "P  V  (P  Q)  V"
| Sum2:              "Q  V  (P  Q)  V"

| Par1B:             "P  ax>  P'; x  P; x  Q; x  a  P  Q  ax>  (P'  Q)"
| Par1F:             "P  α  P'  P  Q  α  (P'  Q)"
| Par2B:             "Q  ax>  Q'; x  P; x  Q; x  a  P  Q  ax>  (P  Q')"
| Par2F:             "Q  α  Q'  P  Q  α  (P  Q')"

| Comm1:             "P  a<b>  P'; Q  a[b]  Q'  P  Q  τ  P'  Q'"
| Comm2:             "P  a[b]  P'; Q  a<b>  Q'  P  Q  τ  P'  Q'"
| Close1:            "P  a<x>  P'; Q  ax>  Q'; x  P; x  Q; x  a  P  Q  τ  x>(P'  Q')"
| Close2:            "P  ax>  P'; Q  a<x>  Q'; x  P; x  Q; x  a  P  Q  τ  x>(P'  Q')"

| ResB:              "P  ax>  P'; y  a; y  x; x  P; x  a  y>P  ax>  (y>P')"
| ResF:              "P  α  P'; y  α  y>P  α  y>P'"

| Bang:              "P  !P  V  !P  V"

equivariance TransitionsEarly
nominal_inductive TransitionsEarly
by(auto simp add: abs_fresh fresh_fact2)

lemmas [simp] = freeRes.inject

lemma freshOutputAction:
  fixes P  :: pi
  and   a  :: name
  and   b  :: name
  and   P' :: pi
  and   c  :: name

  assumes "P  a[b]  P'"
  and     "c  P"

  shows "c  a" and "c  b" and "c  P'"
proof -
  from assms have "c  a  c  b  c  P'"
    by(nominal_induct x2=="a[b]  P'" arbitrary: P' rule: TransitionsEarly.strong_induct) (fastforce simp add: residual.inject abs_fresh freeRes.inject)+
  thus "c  a" and "c  b" and "c  P'"
    by blast+
qed

lemma freshInputAction:
  fixes P  :: pi
  and   a  :: name
  and   b  :: name
  and   P' :: pi
  and   c  :: name

  assumes "P  a<b>  P'"
  and     "c  P"

  shows "c  a"
using assms
by(nominal_induct x2=="a<b>  P'" arbitrary: P' rule: TransitionsEarly.strong_induct) (auto simp add: residual.inject abs_fresh)

lemma freshBoundOutputAction:
  fixes P  :: pi
  and   a  :: name
  and   x  :: name
  and   P' :: pi
  and   c  :: name
  
  assumes "P  ax>  P'"
  and     "c  P"

  shows "c  a"
using assms
by(nominal_induct x2=="ax>  P'" avoiding: x arbitrary: P' rule: TransitionsEarly.strong_induct) (auto simp add: residual.inject abs_fresh fresh_left calc_atm dest: freshOutputAction)

lemmas freshAction = freshOutputAction freshInputAction freshBoundOutputAction

lemma freshInputTransition:
  fixes P  :: pi
  and   a  :: name
  and   u  :: name
  and   P' :: pi
  and   c  :: name

  assumes "P  a<u>  P'"
  and     "c  P"
  and     "c  u"

  shows "c  P'"
using assms
by(nominal_induct x2=="a<u>  P'" arbitrary: P' rule: TransitionsEarly.strong_induct)
  (fastforce simp add: residual.inject name_fresh_abs fresh_fact1 fresh_fact2)+
   
lemma freshBoundOutputTransition:
  fixes P  :: pi
  and   a  :: name
  and   x  :: name
  and   P' :: pi
  and   c  :: name

  assumes "P  ax>  P'"
  and     "c  P"
  and     "c  x"

  shows "c  P'"
using assms
apply(nominal_induct x2=="ax>  P'" avoiding: x arbitrary: P' rule: TransitionsEarly.strong_induct)
apply(fastforce simp add: residual.inject name_fresh_abs alpha' fresh_left calc_atm dest: freshOutputAction | simp | auto simp add: abs_fresh residual.inject alpha' calc_atm)
apply(fastforce simp add: residual.inject name_fresh_abs alpha' fresh_left calc_atm dest: freshOutputAction | simp | auto simp add: abs_fresh residual.inject alpha' calc_atm)
apply(fastforce simp add: residual.inject name_fresh_abs alpha' fresh_left calc_atm dest: freshOutputAction | simp | auto simp add: abs_fresh residual.inject alpha' calc_atm)
apply(force simp add: residual.inject name_fresh_abs alpha' fresh_left calc_atm dest: freshOutputAction | simp | auto simp add: abs_fresh residual.inject alpha' calc_atm)
apply(force simp add: residual.inject name_fresh_abs alpha' fresh_left calc_atm dest: freshOutputAction | simp | auto simp add: abs_fresh residual.inject alpha' calc_atm)
apply(force simp add: residual.inject name_fresh_abs alpha' fresh_left calc_atm dest: freshOutputAction | simp | auto simp add: abs_fresh residual.inject alpha' calc_atm)
apply(force simp add: residual.inject name_fresh_abs alpha' fresh_left calc_atm dest: freshOutputAction | simp | auto simp add: abs_fresh residual.inject alpha' calc_atm)
apply(force simp add: residual.inject name_fresh_abs alpha' fresh_left calc_atm dest: freshOutputAction | simp | auto simp add: abs_fresh residual.inject alpha' calc_atm)
apply(force simp add: residual.inject name_fresh_abs alpha' fresh_left calc_atm dest: freshOutputAction | simp | auto simp add: abs_fresh residual.inject alpha' calc_atm)
apply(force simp add: residual.inject name_fresh_abs alpha' fresh_left calc_atm dest: freshOutputAction | simp | auto simp add: abs_fresh residual.inject alpha' calc_atm)
apply(force simp add: residual.inject name_fresh_abs alpha' fresh_left calc_atm dest: freshOutputAction | simp | auto simp add: abs_fresh residual.inject alpha' calc_atm)
apply(force simp add: residual.inject name_fresh_abs alpha' fresh_left calc_atm dest: freshOutputAction | simp | auto simp add: abs_fresh residual.inject alpha' calc_atm)
apply(fastforce simp add: residual.inject name_fresh_abs alpha' fresh_left calc_atm dest: freshOutputAction)
apply(fastforce simp add: residual.inject name_fresh_abs alpha' fresh_left calc_atm dest: freshOutputAction)
apply(fastforce simp add: residual.inject name_fresh_abs alpha' fresh_left calc_atm dest: freshOutputAction)
apply(fastforce simp add: residual.inject name_fresh_abs alpha' fresh_left calc_atm dest: freshOutputAction)
apply(auto simp add: residual.inject name_fresh_abs alpha' fresh_left calc_atm dest: freshOutputAction)
done

lemma freshTauTransition:
  fixes P  :: pi
  and   P' :: pi
  and   c  :: name

  assumes "P  τ  P'"
  and     "c  P"

  shows "c  P'"
using assms
apply(nominal_induct x2=="τ  P'" arbitrary: P' rule: TransitionsEarly.strong_induct)
by(fastforce simp add: residual.inject abs_fresh dest: freshOutputAction freshInputTransition freshBoundOutputTransition)+

lemma freshFreeTransition:
  fixes P  :: pi
  and   α  :: freeRes
  and   P' :: pi
  and   c  :: name

  assumes "P α  P'"
  and     "c  P"
  and     "c  α"

  shows "c  P'"
using assms
by(nominal_induct α rule: freeRes.strong_inducts)
  (auto dest: freshInputTransition freshOutputAction freshTauTransition)

lemmas freshTransition = freshInputTransition freshOutputAction freshFreeTransition
                         freshBoundOutputTransition freshTauTransition

lemma substTrans[simp]: "b  P  ((P::pi)[a::=b])[b::=c] = P[a::=c]"
apply(simp add: injPermSubst[THEN sym])
apply(simp add: renaming)
by(simp add: pt_swap[OF pt_name_inst, OF at_name_inst])

lemma Input:
  fixes a :: name
  and   x :: name
  and   u :: name
  and   P :: pi

  shows "a<x>.P a<u>  P[x::=u]"
proof -
  obtain y::name where "y  a" and "y  u" and "y  P"
    by(generate_fresh "name") (auto simp add: fresh_prod)
  from y  a y  u have "a<y>.([(x, y)]  P) a<u>  ([(x, y)]  P)[y::=u]"
    by(rule Input)
  with y  P show ?thesis by(simp add: alphaInput renaming name_swap) 
qed

lemma Par1B:
  fixes P  :: pi
  and   a  :: name
  and   x  :: name
  and   P' :: pi
  and   Q  :: pi

  assumes "P ax>  P'"
  and     "x  Q"

  shows "P  Q  ax>  (P'  Q)"
proof -
  obtain y::name where "y  P" and "y  Q" and "y  a" and "y  P'"
    by(generate_fresh "name") (auto simp add: fresh_prod)
  from P ax>  P' y  P' have "P ay>  ([(x, y)]  P')"
    by(simp add: alphaBoundOutput)
  hence "P  Q ay>  (([(x, y)]  P')  Q)" using y  P y  Q y  a
    by(rule Par1B)
  with x  Q y  Q y  P' show ?thesis
    by(subst alphaBoundOutput) (auto simp add: name_fresh_fresh)
qed

lemma Par2B:
  fixes Q  :: pi
  and   a  :: name
  and   x  :: name
  and   Q' :: pi
  and   P  :: pi

  assumes "Q ax>  Q'"
  and     "x  P"

  shows "P  Q  ax>  (P  Q')"
proof -
  obtain y::name where "y  P" and "y  Q" and "y  a" and "y  Q'"
    by(generate_fresh "name") (auto simp add: fresh_prod)
  from Q ax>  Q' y  Q' have "Q ay>  ([(x, y)]  Q')"
    by(simp add: alphaBoundOutput)
  hence "P  Q ay>  (P  ([(x, y)]  Q'))" using y  P y  Q y  a
    by(rule Par2B)
  with x  P y  P y  Q' show ?thesis
    by(subst alphaBoundOutput[of y]) (auto simp add: name_fresh_fresh)
qed

lemma inputInduct[consumes 1, case_names cInput cMatch cMismatch cSum1 cSum2 cPar1 cPar2 cRes cBang]:
  fixes P  :: pi
  and   a  :: name
  and   u  :: name
  and   P' :: pi
  and   F  :: "'a::fs_name  pi  name  name  pi  bool"
  and   C  :: "'a::fs_name"

  assumes Trans:  "P a<u>  P'"
  and     "a x P u C. x  C; x  u; x  a  F C (a<x>.P) a u (P[x::=u])"
  and     "P a u P' b C. P a<u>  P'; C. F C P a u P'  F C ([bb]P) a u P'"
  and     "P a u P' b c C. P a<u>  P'; C. F C P a u P'; bc  F C ([bc]P) a u P'"
  and     "P a u P' Q C. P a<u>  P'; C. F C P a u P'  F C (P  Q) a u P'"
  and     "Q a u Q' P C. Q a<u>  Q'; C. F C Q a u Q'  F C (P  Q) a u Q'"
  and     "P a u P' Q C. P a<u>  P'; C. F C P a u P'  F C (P  Q) a u (P'  Q)"
  and     "Q a u Q' P C. Q a<u>  Q'; C. F C Q a u Q'  F C (P  Q) a u (P  Q')"
  and     "P a u P' x C. P a<u>  P'; x  a; x  u; x  C; C. F C P a u P'  F C (x>P) a u (x>P')"
  and     "P a u P' C. P  !P a<u>  P'; C. F C (P  !P) a u P'  F C (!P) a u P'"

  shows "F C P a u P'"
using assms
by(nominal_induct x2=="a<u>  P'" avoiding: C arbitrary: P' rule: TransitionsEarly.strong_induct)
  (auto simp add: residual.inject)

lemma inputAlpha:
  assumes "P a<u>  P'"
  and     "u  P"
  and     "r  P'"

  shows "P a<r>  ([(u, r)]  P')"
using assms
proof(nominal_induct avoiding: r rule: inputInduct)
  case(cInput a x P u r)
  from x  u u  a<x>.Phave "u  a" and "u  P" by(simp add: abs_fresh)+
  have "a<x>.P a<r>  P[x::=r]"
    by(rule Input)
  thus ?case using r  P[x::=u] u  P
    by(simp add: injPermSubst substTrans)
next
  case(cMatch P a u P' b r)
  thus ?case by(force intro: Match) 
next
  case(cMismatch P a u P' b c r)
  thus ?case by(force intro: Mismatch)
next
  case(cSum1 P a u P' Q r)
  thus ?case by(force intro: Sum1)
next
  case(cSum2 Q a u Q' P r)
  thus ?case by(force intro: Sum2)
next
  case(cPar1 P a u P' Q r)
  thus ?case by(force intro: Par1F simp add: eqvts name_fresh_fresh) 
next
  case(cPar2 Q a u Q' P r)
  thus ?case by(force intro: Par2F simp add: eqvts name_fresh_fresh) 
next
  case(cRes P a u P' x r)
  thus ?case by(force intro: ResF simp add: eqvts calc_atm abs_fresh) 
next
  case(cBang P a u P' R)
  thus ?case by(force intro: Bang)
qed

lemma Close1:
  fixes P  :: pi
  and   a  :: name
  and   x  :: name
  and   P' :: pi
  and   Q  :: pi
  and   Q' :: pi

  assumes "P a<x>  P'"
  and     "Q ax>  Q'"
  and     "x  P"

  shows "P  Q τ  x>(P'  Q')"
proof -
  obtain y::name where "y  P" and "y  Q" and "y  a" and "y  Q'" and "y  P'"
    by(generate_fresh "name") (auto simp add: fresh_prod)
  from P a<x>  P' x  P y  P' have "P a<y>  ([(x, y)]  P')"
    by(rule inputAlpha)
  moreover from Q ax>  Q' y  Q' have "Q ay>  ([(x, y)]  Q')"
    by(simp add: alphaBoundOutput)
  
  ultimately have "P  Q τ  y>(([(x, y)]  P')  ([(x, y)]  Q'))" using y  P y  Q y  a
    by(rule Close1)
  with y  P' y  Q' show ?thesis by(subst alphaRes) (auto simp add: name_fresh_fresh)
qed

lemma Close2:
  fixes P  :: pi
  and   a  :: name
  and   x  :: name
  and   P' :: pi
  and   Q  :: pi
  and   Q' :: pi

  assumes "P ax>  P'"
  and     "Q a<x>  Q'"
  and     "x  Q"

  shows "P  Q τ  x>(P'  Q')"
proof -
  obtain y::name where "y  P" and "y  Q" and "y  a" and "y  Q'" and "y  P'"
    by(generate_fresh "name") (auto simp add: fresh_prod)
  from P ax>  P' y  P' have "P ay>  ([(x, y)]  P')"
    by(simp add: alphaBoundOutput)
  moreover from Q a<x>  Q' x  Q y  Q' have "Q a<y>  ([(x, y)]  Q')"
    by(rule inputAlpha)
  
  ultimately have "P  Q τ  y>(([(x, y)]  P')  ([(x, y)]  Q'))" using y  P y  Q y  a
    by(rule Close2)
  with y  P' y  Q' show ?thesis by(subst alphaRes) (auto simp add: name_fresh_fresh)
qed

lemma ResB:
  fixes P  :: pi
  and   a  :: name
  and   x  :: name
  and   P' :: pi
  and   y  :: name

  assumes "P ax>  P'"
  and     "y  a"
  and     "y  x"

  shows "y>P ax>  (y>P')"
proof -
  obtain z :: name where "z  P" and "z  P'" and "z  a" and "z  y"
    by(generate_fresh "name") (auto simp add: fresh_prod)
  from P ax>  P' z  P' have "P az>  ([(x, z)]  P')"
    by(simp add: alphaBoundOutput)
  hence "y>P az>  (y>([(x, z)]  P'))" using y  a z  y z  P z  a
    by(rule_tac ResB) auto
  thus ?thesis using z  y y  x z  P'
    by(subst alphaBoundOutput[where x'=z]) (auto simp add: eqvts calc_atm abs_fresh)
qed

lemma outputInduct[consumes 1, case_names Output Match Mismatch Sum1 Sum2 Par1 Par2 Res Bang]:
  fixes P  :: pi
  and   a  :: name
  and   b  :: name
  and   P' :: pi
  and   F  :: "'a::fs_name  pi  name  name  pi  bool"
  and   C  :: "'a::fs_name"

  assumes Trans:  "P a[b]  P'"
  and     "a b P C. F C (a{b}.P) a b P"
  and     "P a b P' c C. P OutputR a b  P'; C. F C P a b P'  F C ([cc]P) a b P'"
  and     "P a b P' c d C. P OutputR a b  P'; C. F C P a b P'; cd  F C ([cd]P) a b P'"
  and     "P a b P' Q C. P OutputR a b  P'; C. F C P a b P'  F C (P  Q) a b P'"
  and     "Q a b Q' P C. Q OutputR a b  Q'; C. F C Q a b Q'  F C (P  Q) a b Q'"
  and     "P a b P' Q C. P OutputR a b  P'; C. F C P a b P'  F C (P  Q) a b (P'  Q)"
  and     "Q a b Q' P C. Q OutputR a b  Q'; C. F C Q a b Q'  F C (P  Q) a b (P  Q')"
  and     "P a b P' x C. P OutputR a b  P'; x  a; x  b; x  C; C. F C P a b P' 
                            F C (x>P) a b (x>P')"
  and     "P a b P' C. P  !P OutputR a b  P'; C. F C (P  !P) a b P'  F C (!P) a b P'"

  shows "F C P a b P'"
using assms
by(nominal_induct x2=="a[b]  P'" avoiding: C arbitrary: P' rule: TransitionsEarly.strong_induct)
  (auto simp add: residual.inject)

lemma boundOutputInduct[consumes 2, case_names Match Mismatch Open Sum1 Sum2 Par1 Par2 Res Bang]:
  fixes P  :: pi
  and   a  :: name
  and   x  :: name
  and   P' :: pi
  and   F  :: "('a::fs_name)  pi  name  name  pi  bool"
  and   C  :: "'a::fs_name"

  assumes a: "P ax>  P'"
  and     xFreshP:  "x  P"
  and     cMatch:   "P a x P' b C. P ax>  P'; C. F C P a x P'  F C ([bb]P) a x P'"
  and     cMismatch:   "P a x P' b c C. P ax>  P'; C. F C P a x P'; b  c  F C ([bc]P) a x P'"
  and     cOpen:    "P a x P' C.   P (OutputR a x)  P'; a  x  F C (x>P) a x P'"
  and     cSum1:    "P Q a x P' C. P ax>  P'; C. F C P a x P'  F C (P  Q) a x P'" 
  and     cSum2:    "P Q a x Q' C. Q ax>  Q'; C. F C Q a x Q'  F C (P  Q) a x Q'" 
  and     cPar1B:   "P P' Q a x C. P ax>  P'; x  Q; C. F C P a x P' 
                                  F C (P  Q) a x (P'  Q)" 
  and     cPar2B:   "P Q Q' a x C. Q ax>  Q'; x  P; C. F C Q a x Q' 
                                  F C (P  Q) a x (P  Q')"
  and     cResB:    "P P' a x y C. P ax>  P'; y  a; y  x; y  C;
                                      C. F C P a x P'  F C (y>P) a x (y>P')"
  and     cBang:    "P a x P' C. P  !P ax>  P'; C. F C (P  !P) a x P' 
                                    F C (!P) a x P'"
  shows "F C P a x P'"
using assms
proof -
  have Goal: "P Rs a x P' C. P  Rs; Rs = ax>  P'; x  P  F C P a x P'"
  proof -
    fix P Rs a x P' C
    assume "P  Rs" and "Rs = ax>  P'" and "x  P"
    thus "F C P a x P'"
    proof(nominal_induct avoiding: C a x P' rule: TransitionsEarly.strong_induct)
      case(Tau P)
      thus ?case by(simp add: residual.inject)
    next
      case(Input P a x)
      thus ?case by(simp add: residual.inject)
    next
      case(Output P a b)
      thus ?case by(simp add: residual.inject)
    next
      case(Match P Rs b C a x P')
      thus ?case 
        by(force intro: cMatch simp add: residual.inject) 
    next
      case(Mismatch P Rs b c C a x P')
      thus ?case 
        by(force intro: cMismatch simp add: residual.inject) 
    next
      case(Sum1 P Q Rs C)
      thus ?case by(force intro: cSum1)
    next
      case(Sum2 P Q Rs C)
      thus ?case by(force intro: cSum2)
    next
      case(Open P a b P' C a' x P'')
      have "b  x" by fact hence bineqx: "b  x" by simp
      moreover have "ab>  P' = a'x>  P''" by fact
      ultimately have aeqa': "a=a'" and P'eqP'': "P'' = [(b, x)]  P'"
        by(simp add: residual.inject name_abs_eq)+
      have "x  b>P" by fact 
      with bineqx have xFreshP: "x  P" by(simp add: name_fresh_abs)
      have aineqb: "a  b" by fact

      have PTrans: "P a[b]  P'" by fact
      with xFreshP have xineqa: "x  a" by(force dest: freshAction)
      from PTrans have "([(b, x)]  P) [(b, x)]  (a[b]  P')" by(rule TransitionsEarly.eqvt)
      with P'eqP'' xineqa aineqb have Trans: "([(b, x)]  P) a[x]  P''"
        by(auto simp add: name_calc)
      hence "F C (x>([(b, x)]  P)) a x P''" using xineqa by(blast intro: cOpen)
      with xFreshP aeqa' show ?case by(simp add: alphaRes)
    next
      case(Par1B P  a x P' Q C a' x' P'')
      have "x  x'" by fact hence xineqx': "x  x'" by simp
      moreover have Eq: "ax>  (P'  Q) = a'x'>  P''" by fact
      hence aeqa': "a = a'" by(simp add: residual.inject)
      have xFreshQ: "x  Q" by fact
      have "x'  P  Q" by fact
      hence x'FreshP: "x'  P" and x'FreshQ: "x'  Q" by simp+
      have P''eq: "P'' = ([(x, x')]  P')  Q"
      proof -
        from Eq xineqx' have "(P'  Q) = [(x, x')]  P''"
          by(simp add: residual.inject name_abs_eq)
        hence "([(x, x')]  (P'  Q)) = P''" by simp
        with x'FreshQ xFreshQ show ?thesis by(simp add: name_fresh_fresh)
      qed

      have "x  P''" by fact
      with P''eq have x'FreshP': "x'  P'" by(simp add: name_fresh_left name_calc)

      have "P ax>  P'" by fact
      with x'FreshP' aeqa' have "P a'x'>  ([(x, x')]  P')"
        by(simp add: alphaBoundOutput)
      moreover have "C. F C P a x' ([(x, x')]  P')"
      proof -
        fix C
        have "C a' x' P''. ax>  P' = a'x'>  P''; x'  P  F C P a' x' P''" by fact
        moreover with aeqa' xineqx' x'FreshP' have "ax>  P' = a'x'>  ([(x, x')]  P')"
          by(simp add: residual.inject name_abs_eq name_fresh_left name_calc)
        ultimately show "F C P a x' ([(x, x')]  P')" using x'FreshP aeqa' by blast 
      qed
      ultimately have "F C (P  Q) a' x' (([(x, x')]  P')  Q)" using x'FreshQ aeqa'
        by(blast intro: cPar1B)
      with P''eq show ?case by simp
    next
      case(Par1F P P' Q α)
      thus ?case by(simp add: residual.inject)
    next
      case(Par2B Q a x Q' P C a' x' Q'')
      have "x  x'" by fact hence xineqx': "x  x'" by simp
      moreover have Eq: "ax>  (P  Q') = a'x'>  Q''" by fact
      hence aeqa': "a = a'" by(simp add: residual.inject)
      have xFreshP: "x  P" by fact
      have "x'  P  Q" by fact
      hence x'FreshP: "x'  P" and x'FreshQ: "x'  Q" by simp+
      have Q''eq: "Q'' = P  ([(x, x')]  Q')"
      proof -
        from Eq xineqx' have "(P  Q') = [(x, x')]  Q''"
          by(simp add: residual.inject name_abs_eq)
        hence "([(x, x')]  (P  Q')) = Q''" by simp
        with x'FreshP xFreshP show ?thesis by(simp add: name_fresh_fresh)
      qed

      have "x  Q''" by fact
      with Q''eq have x'FreshQ': "x'  Q'" by(simp add: name_fresh_left name_calc)

      have "Q ax>  Q'" by fact
      with x'FreshQ' aeqa' have "Q a'x'>  ([(x, x')]  Q')"
        by(simp add: alphaBoundOutput)
      moreover have "C. F C Q a x' ([(x, x')]  Q')"
      proof -
        fix C
        have "C a' x' Q''. ax>  Q' = a'x'>  Q''; x'  Q  F C Q a' x' Q''" by fact
        moreover with aeqa' xineqx' x'FreshQ' have "ax>  Q' = a'x'>  ([(x, x')]  Q')"
          by(simp add: residual.inject name_abs_eq name_fresh_left name_calc)
        ultimately show "F C Q a x' ([(x, x')]  Q')" using x'FreshQ aeqa' by blast 
      qed
      ultimately have "F C (P  Q) a' x' (P  ([(x, x')]  Q'))" using x'FreshP aeqa'
        by(blast intro: cPar2B)
      with Q''eq show ?case by simp
    next
      case(Par2F P P' Q α)
      thus ?case by(simp add: residual.inject)
    next
      case(Comm1 P P' Q Q' a b x)
      thus ?case by(simp add: residual.inject)
    next
      case(Comm2 P P' Q Q' a b x)
      thus ?case by(simp add: residual.inject)
    next
      case(Close1 P P' Q Q' a x y)
      thus ?case by(simp add: residual.inject)
    next
      case(Close2 P P' Q Q' a x y)
      thus ?case by(simp add: residual.inject)
    next
      case(ResB P a x P' y C a' x' P'')
      have "x  x'" by fact hence xineqx': "x  x'" by simp
      moreover have Eq: "ax>  (y>P') = a'x'>  P''" by fact
      hence aeqa': "a = a'" by(simp add: residual.inject)
      have "y  x'" by fact hence yineqx': "y  x'" by simp
      moreover have "x'  y>P" by fact
      ultimately have x'FreshP: "x'  P" by(simp add: name_fresh_abs)
      have yineqx: "y  x" and yineqa: "y  a" and yFreshC: "y  C" by fact+

      have P''eq: "P'' = y>([(x, x')]  P')"
      proof -
        from Eq xineqx' have "y>P' = [(x, x')]  P''"
          by(simp add: residual.inject name_abs_eq)
        hence "([(x, x')]  (y>P')) = P''" by simp
        with yineqx' yineqx show ?thesis by(simp add: name_fresh_fresh)
      qed

      have "x  P''" by fact
      with P''eq yineqx  have x'FreshP': "x'  P'" by(simp add: name_fresh_left name_calc name_fresh_abs)

      have "P ax>  P'" by fact
      with x'FreshP' aeqa' have "P a'x'>  ([(x, x')]  P')"
        by(simp add: alphaBoundOutput)
      moreover have "C. F C P a x' ([(x, x')]  P')"
      proof -
        fix C
        have "C a' x' P''. ax>  P' = a'x'>  P''; x'  P  F C P a' x' P''" by fact
        moreover with aeqa' xineqx' x'FreshP' have "ax>  P' = a'x'>  ([(x, x')]  P')"
          by(simp add: residual.inject name_abs_eq name_fresh_left name_calc)
        ultimately show "F C P a x' ([(x, x')]  P')" using x'FreshP aeqa' by blast 
      qed
      ultimately have "F C (y>P) a' x' (y>([(x, x')]  P'))" using yineqx' yineqa yFreshC aeqa'
        by(force intro: cResB)
      with P''eq show ?case by simp
    next
      case(ResF P P' α y)
      thus ?case by(simp add: residual.inject)
    next
      case(Bang P Rs)
      thus ?case by(force intro: cBang)
    qed
  qed
    
  with a xFreshP show ?thesis by simp
qed

lemma tauInduct[consumes 1, case_names Tau Match Mismatch Sum1 Sum2 Par1 Par2 Comm1 Comm2 Close1 Close2 Res Bang]:
  fixes P  :: pi
  and   P' :: pi
  and   F  :: "'a::fs_name  pi  pi  bool"
  and   C  :: "'a::fs_name"

  assumes Trans:  "P τ  P'"
  and     "P C. F C (τ.(P)) P"
  and     "P P' a C. P τ  P'; C. F C P P'  F C ([aa]P) P'"
  and     "P P' a b C. P τ  P'; C. F C P P'; a  b  F C ([ab]P) P'"
  and     "P P' Q C. P τ  P'; C. F C P P'  F C (P  Q) P'"
  and     "Q Q' P C. Q τ  Q'; C. F C Q Q'  F C (P  Q) Q'"
  and     "P P' Q C. P τ  P'; C. F C P P'  F C (P  Q) (P'  Q)"
  and     "Q Q' P C. Q τ  Q'; C. F C Q Q'  F C (P  Q) (P  Q')"
  and     "P a b P' Q Q' C. P a<b>  P'; Q OutputR a b  Q'  F C (P  Q) (P'  Q')"
  and     "P a b P' Q Q' C. P OutputR a b  P'; Q a<b>  Q'  F C (P  Q) (P'  Q')"
  and     "P a x P' Q Q' C. P a<x>  P'; Q ax>  Q'; x  P; x  Q; x  a; x  C  F C (P  Q) (x>(P'  Q'))"
  and     "P a x P' Q Q' C. P ax>  P'; Q a<x>  Q'; x  P; x  Q; x  a; x  C  F C (P  Q) (x>(P'  Q'))"
  and     "P P' x C. P τ  P'; x  C; C. F C P P' 
                        F C (x>P) (x>P')"
  and     "P P' C. P  !P τ  P'; C. F C (P  !P) P'  F C (!P) P'"

  shows "F C P P'"
using P τ  P'
by(nominal_induct x2=="τ  P'" avoiding: C arbitrary: P' rule: TransitionsEarly.strong_induct)
  (auto simp add: residual.inject intro: assms)+

inductive bangPred :: "pi  pi  bool"
where
  aux1: "bangPred P (!P)"
| aux2: "bangPred P (P  !P)"

inductive_cases tauCases'[simplified pi.distinct residual.distinct]: "τ.(P)  Rs"
inductive_cases inputCases'[simplified pi.inject residual.inject]: "a<b>.P  Rs"
inductive_cases outputCases'[simplified pi.inject residual.inject]: "a{b}.P  Rs"
inductive_cases matchCases'[simplified pi.inject residual.inject]: "[ab]P  Rs"
inductive_cases mismatchCases'[simplified pi.inject residual.inject]: "[ab]P  Rs"
inductive_cases sumCases'[simplified pi.inject residual.inject]: "P  Q  Rs"
inductive_cases parCasesB'[simplified pi.distinct residual.distinct]: "A  B  by>  A'"
inductive_cases parCasesF'[simplified pi.distinct residual.distinct]: "P  Q  α  P'"
inductive_cases resCasesB'[simplified pi.distinct residual.distinct]: "x'>A  ay'>  A'"
inductive_cases resCasesF'[simplified pi.distinct residual.distinct]: "x>A  α  A'"

lemma tauCases:
  fixes P  :: pi
  and   α  :: freeRes
  and   P' :: pi

  assumes "τ.(P) α  P'"
  and     "Prop (τ) P"

  shows "Prop α P'"
using assms
by(cases rule: tauCases') (auto simp add: pi.inject residual.inject)

lemma inputCases[consumes 1, case_names cInput]:
  fixes a  :: name
  and   x  :: name
  and   P  :: pi
  and   P' :: pi

  assumes Input: "a<x>.P α  P'"
  and     A: "u. Prop (a<u>) (P[x::=u])"

  shows "Prop α P'"
proof -
  {
    fix x P
    assume "a<x>.P α  P'"
    moreover assume "(x::name)  α" and "x  P'" and "x  a"
    moreover assume "u. Prop (a<u>) (P[x::=u])"
    moreover obtain z::name where "z  x" and "z  P" and "z  α" and "z  P'"  and "z  a"
      by(generate_fresh "name", auto simp add: fresh_prod)
    moreover obtain z'::name where "z'  x" and "z'  z" and "z'  P" and "z'  α" and "z'  P'" and "z'  a"
      by(generate_fresh "name", auto simp add: fresh_prod)
    ultimately have "Prop α P'"
      by(cases rule: TransitionsEarly.strong_cases[where x=x and b=z and xa=z and xb=z and xc=z and xd=z and xe=z
                                                   and y=z' and ya=z'])
        (auto simp add: pi.inject residual.inject abs_fresh alpha)
   }
   note Goal = this
   obtain y::name where "y  P" and "y  α" and "y  P'" and "y  a"
     by(generate_fresh "name") (auto simp add: fresh_prod)
   from Input y  P have "a<y>.([(x, y)]  P) α  P'" by(simp add: alphaInput)
   moreover note y  α y  P' y  a
   moreover from A y  P have "u. Prop (a<u>) (([(x, y)]  P)[y::=u])"
     by(simp add: renaming name_swap)
   ultimately show ?thesis by(rule Goal)
qed

lemma outputCases:
  fixes P  :: pi
  and   α  :: freeRes
  and   P' :: pi

  assumes "a{b}.P α  P'"
  and     "Prop (OutputR a b) P"

  shows "Prop α P'"
using assms
by(cases rule: outputCases') (auto simp add: pi.inject residual.inject)

lemma zeroTrans[dest]:
  fixes Rs :: residual

  assumes "𝟬  e Rs"

  shows "False"
using assms
by - (ind_cases "𝟬  e Rs")

lemma mismatchTrans[dest]:
  fixes a   :: name
  and   P   :: pi
  and   Rs  :: residual

  assumes "[aa]P  Rs"

  shows "False"
using assms
by(erule_tac mismatchCases') auto

lemma matchCases[consumes 1, case_names Match]:
  fixes a  :: name
  and   b  :: name
  and   P  :: pi
  and   Rs :: residual
  and   F  :: "name  name  bool"

  assumes Trans:  "[ab]P  Rs"
  and     cMatch: "P  Rs  F a a"

  shows "F a b"
using assms
by(erule_tac matchCases', auto)

lemma mismatchCases[consumes 1, case_names Mismatch]:
  fixes a  :: name
  and   b  :: name
  and   P  :: pi
  and   Rs :: residual
  and   F  :: "name  name  bool"

  assumes Trans:  "[ab]P  Rs"
  and     cMatch: "P  Rs; a  b  F a b"

  shows "F a b"
using assms  
by(erule_tac mismatchCases') auto

lemma sumCases[consumes 1, case_names Sum1 Sum2]:
  fixes P  :: pi
  and   Q  :: pi
  and   Rs :: residual

  assumes Trans: "P  Q  Rs"
  and     cSum1: "P  Rs  F"
  and     cSum2: "Q  Rs  F"

  shows F
using assms
by(erule_tac sumCases') auto

lemma parCasesB[consumes 1, case_names cPar1 cPar2]:
  fixes P   :: pi
  and   Q   :: pi
  and   a   :: name
  and   x   :: name
  and   PQ' :: pi
  
  assumes Trans: "P  Q  ax>  PQ'"
  and     icPar1B: "P'. P  ax>  P'; x  Q  F (P'  Q)"
  and     icPar2B: "Q'. Q  ax>  Q'; x  P  F (P  Q')"

  shows "F PQ'"
proof -
  from Trans show ?thesis
  proof(induct rule: parCasesB', auto simp add: pi.inject residual.inject)
    fix P' y
    assume PTrans: "P  ay>  P'"
    assume yFreshQ: "y  (Q::pi)"
    assume absEq: "[x].PQ' = [y].(P'  Q)"

    have "c::name. c  (P', x, y, Q)" by(blast intro: name_exists_fresh)
    then obtain c where cFreshP': "c  P'" and cineqx: "x  c" and cineqy: "c  y" and cFreshQ: "c  Q"
      by(force simp add: fresh_prod name_fresh)

    from cFreshP' PTrans have Trans: "P  ac>  ([(y, c)]  P')" by(simp add: alphaBoundOutput)

    from cFreshP' cFreshQ have "c  P'  Q" by simp
    hence "[y].(P'  Q) = [c].([(y, c)]  (P'  Q))"
      by(auto simp add: alpha fresh_left calc_atm)
    with yFreshQ cFreshQ have "[y].(P'  Q) = [c].(([(y, c)]  P')  Q)"
      by(simp add: name_fresh_fresh)

    with cineqx absEq have L1: "PQ' = [(x, c)]  (([(y, c)]  P')  Q)" and L2: "x  ([(y, c)]  P')  Q"
      by(simp add: name_abs_eq)+
    
    from L2 have xFreshQ: "x  Q" and xFreshP': "x  [(y, c)]  P'" by simp+
    with cFreshQ L1 have L3: "PQ' = ([(x, c)]  [(y, c)]  P')  Q" by(simp add: name_fresh_fresh)

    from Trans xFreshP' have "P  ax>  ([(x, c)]  [(y, c)]  P')" by(simp add: alphaBoundOutput name_swap)

    thus ?thesis using xFreshQ L3
      by(blast intro: icPar1B)
  next
    fix Q' y
    assume QTrans: "Q  ay>  Q'"
    assume yFreshP: "y  (P::pi)"
    assume absEq: "[x].PQ' = [y].(P  Q')"

    have "c::name. c  (Q', x, y, P)" by(blast intro: name_exists_fresh)
    then obtain c where cFreshQ': "c  Q'" and cineqx: "x  c" and cineqy: "c  y" and cFreshP: "c  P"
      by(force simp add: fresh_prod name_fresh)

    from cFreshQ' QTrans have Trans: "Q  ac>  ([(y, c)]  Q')" by(simp add: alphaBoundOutput)

    from cFreshQ' cFreshP have "c  P  Q'" by simp
    hence "[y].(P  Q') = [c].([(y, c)]  (P  Q'))"
      by(auto simp add: alpha fresh_left calc_atm)
    with yFreshP cFreshP have "[y].(P  Q') = [c].(P  ([(y, c)]  Q'))"
      by(simp add: name_fresh_fresh)

    with cineqx absEq have L1: "PQ' = [(x, c)]  (P  ([(y, c)]  Q'))" and L2: "x  P  ([(y, c)]  Q')"
      by(simp add: name_abs_eq)+
    
    from L2 have xFreshP: "x  P" and xFreshQ': "x  [(y, c)]  Q'" by simp+
    with cFreshP L1 have L3: "PQ' = P  ([(x, c)]  [(y, c)]  Q')" by(simp add: name_fresh_fresh)

    from Trans xFreshQ' have "Q  ax>  ([(x, c)]  [(y, c)]  Q')" by(simp add: alphaBoundOutput name_swap)

    thus ?thesis using xFreshP L3
      by(blast intro: icPar2B)
  qed
qed

lemma parCasesOutput[consumes 1, case_names Par1 Par2]:
  fixes P  :: pi
  and   Q  :: pi
  and   a  :: name
  and   b  :: name
  and   P' :: pi

  assumes "P  Q a[b]  PQ'"
  and     "P'. P a[b]  P'  F (P'  Q)"
  and     "Q'. Q a[b]  Q'  F (P  Q')"

  shows "F PQ'"
using assms
by(erule_tac parCasesF', auto simp add: pi.inject residual.inject)

lemma parCasesInput[consumes 1, case_names Par1 Par2]:
  fixes P  :: pi
  and   Q  :: pi
  and   a  :: name
  and   b  :: name
  and   P' :: pi

  assumes Trans: "P  Q a<b>  PQ'"
  and     icPar1F: "P'. P a<b>  P'  F (P'  Q)"
  and     icPar2F: "Q'. Q a<b>  Q'  F (P  Q')"

  shows "F PQ'"
using assms
by(erule_tac parCasesF') (auto simp add: pi.inject residual.inject)

lemma parCasesF[consumes 1, case_names cPar1 cPar2 cComm1 cComm2 cClose1 cClose2]:
  fixes P  :: pi
  and   Q  :: pi
  and   α  :: freeRes
  and   P' :: pi
  and   C  :: "'a::fs_name"

  assumes Trans: "P  Q  α  PQ'"
  and     icPar1F: "P'. P  α  P'  F α (P'  Q)"
  and     icPar2F: "Q'. Q  α  Q'  F α (P  Q')"
  and     icComm1: "P' Q' a b. P  a<b>  P'; Q  a[b]  Q'  F (τ) (P'  Q')"
  and     icComm2: "P' Q' a b. P  a[b]  P'; Q  a<b>  Q'  F (τ) (P'  Q')"
  and     icClose1: "P' Q' a x. P  a<x>  P'; Q  ax>  Q'; x  P; x  C  F (τ) (x>(P'  Q'))"
  and     icClose2: "P' Q' a x. P  ax>  P'; Q  a<x>  Q'; x  Q; x  C  F (τ) (x>(P'  Q'))"

  shows "F α PQ'"
proof -
  from Trans show ?thesis
  proof(rule parCasesF', auto)
    fix Pa Pa' Qa α'
    assume Trans': "Pa  α'  Pa'"
    assume Eq: "P  Q = Pa  Qa"
    assume Eq': "α  PQ' = α'  Pa'  Qa"

    from Eq have "P = Pa" and "Q = Qa"
      by(simp add: pi.inject)+
    
    moreover with Eq' have "α = α'" and "PQ' = Pa'  Q"
      by(simp add: residual.inject)+

    ultimately show ?thesis using icPar1F Trans'
      by simp
  next
    fix Pa Qa Qa' α'
    assume Trans': "Qa  α'  Qa'"
    assume Eq: "P  Q = Pa  Qa"
    assume Eq': "α  PQ' = α'  Pa  Qa'"

    from Eq have "P = Pa" and "Q = Qa"
      by(simp add: pi.inject)+
    
    moreover with Eq' have "α = α'" and "PQ' = P  Qa'"
      by(simp add: residual.inject)+

    ultimately show ?thesis using icPar2F Trans'
      by simp
  next
    fix Pa Pa' Qa Qa' a b
    assume TransP: "Pa  a<b>  Pa'"
    assume TransQ: "Qa  a[b]  Qa'"
    assume Eq: "P  Q = Pa  Qa"
    assume Eq': "α  PQ' = τ  Pa'  Qa'"

    from TransP TransQ Eq Eq' icComm1 show ?thesis
      by(simp add: pi.inject residual.inject)
  next
    fix Pa Pa' Qa Qa' a b x
    assume TransP: "Pa  (a::name)[b]  Pa'"
    assume TransQ: "Qa  a<b>  Qa'"
    assume Eq: "P  Q = Pa  Qa"
    assume Eq': "α  PQ' = τ  Pa'  Qa'"

    from TransP TransQ Eq Eq' icComm2 show ?thesis
      by(simp add: pi.inject residual.inject)
  next
    fix Pa Pa' Qa Qa' a x
    assume TransP: "Pa  a<x>  Pa'"
    assume TransQ: "Qa  ax>  Qa'"
    assume xFreshPa: "x  Pa"
    assume Eq: "P  Q = Pa  Qa"
    assume Eq': "α  PQ' = τ  x>(Pa'  Qa')"

    have "(c::name). c  (Pa, Pa', x, Qa', a, C)"
      by(blast intro: name_exists_fresh)
    then obtain c::name where cFreshPa: "c  Pa" and cFreshPa': "c  Pa'" and cineqy: "c  x" and cFreshQa': "c  Qa'" and cFreshC: "c  C" and cineqa: "c  a"
      by(force simp add: fresh_prod name_fresh)

    from cFreshQa' have L1: "ax>  Qa' = ac>  ([(x, c)]  Qa')"
      by(simp add: alphaBoundOutput)
    with cFreshQa' cFreshPa' have "c  (Pa'  Qa')"
      by simp
    then have L4: "x>(Pa'  Qa') = c>(([(x, c)]  Pa')  ([(x, c)]  Qa'))"
      by(simp add: alphaRes)

    have TransP: "Pa  a<c>  [(x, c)]  Pa'"
    proof -
      from xFreshPa TransP have xineqa: "xa" by(force dest: freshAction)
      from TransP have "([(x, c)]  Pa)  [(x, c)]  (a<x>  Pa')"
        by(rule TransitionsEarly.eqvt)
      with xineqa xFreshPa cFreshPa cineqa show ?thesis
        by(simp add: name_fresh_fresh name_calc)
    qed

    with TransQ L1 L4 icClose1 Eq Eq' cFreshPa cFreshC show ?thesis
      by(simp add: residual.inject, simp add: pi.inject)
  next
    fix Pa Pa' Qa Qa' a x
    assume TransP: "Pa  ax>  Pa'"
    assume TransQ: "Qa  a<x>  Qa'"
    assume xFreshQa: "x  Qa"
    assume Eq: "P  Q = Pa  Qa"
    assume Eq': "α  PQ' = τ  x>(Pa'  Qa')"

    have "(c::name). c  (Qa, Pa', x, Qa', a, C)"
      by(blast intro: name_exists_fresh)
    then obtain c::name where cFreshQa: "c  Qa" and cFreshPa': "c  Pa'" and cineqy: "c  x" and cFreshQa': "c  Qa'" and cFreshC: "c  C" and cineqa: "c  a"
      by(force simp add: fresh_prod name_fresh)

    from cFreshPa' have L1: "ax>  Pa' = ac>  ([(x, c)]  Pa')"
      by(simp add: alphaBoundOutput)
    with cFreshQa' cFreshPa' have "c  (Pa'  Qa')"
      by simp
    then have L4: "x>(Pa'  Qa') = c>(([(x, c)]  Pa')  ([(x, c)]  Qa'))"
      by(simp add: alphaRes)

    have TransQ: "Qa  a<c>  [(x, c)]  Qa'"
    proof -
      from xFreshQa TransQ have xineqa: "xa" by(force dest: freshAction)
      from TransQ have "([(x, c)]  Qa)  [(x, c)]  (a<x>  Qa')"
        by(rule TransitionsEarly.eqvt)
      with xineqa xFreshQa cFreshQa cineqa show ?thesis
        by(simp add: name_fresh_fresh name_calc)
    qed

    with TransP L1 L4 icClose2 Eq Eq' cFreshQa cFreshC show ?thesis
      by(simp add: residual.inject, simp add: pi.inject)
  qed
qed

lemma resCasesF[consumes 2, case_names Res]:
  fixes x :: name
  and   P  :: pi
  and   α  :: freeRes
  and   P' :: pi

  assumes Trans: "x>P  α  RP'"
  and     xFreshAlpha: "x  α"
  and     rcResF: " P'. P  α  P'  F (x>P')"

  shows "F RP'"
proof -
  from Trans show ?thesis
  proof(induct rule: resCasesF', auto)
    fix Pa Pa' β y
    assume PTrans: "Pa  β  Pa'"
    assume yFreshBeta: "(y::name)  β"
    assume TermEq: "x>P = y>Pa"
    assume ResEq: "α  RP' = β  y>Pa'"

    hence alphaeqbeta: "α = β" and L2: "RP' = y>Pa'" by(simp add: residual.inject)+

    have "(c::name). c  (Pa, α, Pa', x, y)" by(blast intro: name_exists_fresh)
    then obtain c::name where cFreshPa: "c  Pa" and cFreshAlpha: "c  α" and cFreshPa': "c  Pa'" and cineqx: "x  c" and cineqy: "c  y"
      by(force simp add: fresh_prod name_fresh)

    from cFreshPa have "y>Pa = c>([(y, c)]  Pa)" by(rule alphaRes)
    with TermEq cineqx have Peq: "P = [(x, c)]  [(y, c)]  Pa" and xeq: "x  [(y, c)]  Pa"
      by(simp add: pi.inject name_abs_eq)+

    from PTrans have "([(y, c)]  Pa)  [(y, c)]  (β  Pa')" by(rule TransitionsEarly.eqvt)
    with yFreshBeta cFreshAlpha alphaeqbeta have PTrans': "([(y, c)]  Pa)  α  ([(y, c)]  Pa')" 
      by(simp add: name_fresh_fresh)

    from PTrans' have "([(x, c)]  [(y, c)]  Pa)  [(x, c)]  (α  [(y, c)]  Pa')"
      by(rule TransitionsEarly.eqvt)
    with xFreshAlpha cFreshAlpha Peq have PTrans'': "P  α  [(x, c)]  [(y, c)]  Pa'"
      by(simp add: name_fresh_fresh)

    from PTrans' xeq xFreshAlpha have xeq': "x  [(y, c)]  Pa'"
      by(nominal_induct α rule: freeRes.strong_induct)
        (auto simp add: fresh_left calc_atm eqvts dest: freshTransition)

    from cFreshPa' have "y>Pa' = c>([(y, c)]  Pa')" by(rule alphaRes)
    moreover from xeq' have "c>([(y, c)]  Pa') = x>([(c, x)]  [(y, c)]  Pa')"
      by(rule alphaRes)
    ultimately have "RP' = x>([(x, c)]  [(y, c)]  Pa')" using ResEq
      by(simp add: residual.inject name_swap)

    with PTrans'' xFreshAlpha show ?thesis
      by(blast intro: rcResF)
  qed
qed

lemma resCasesB[consumes 2, case_names Open Res]:
  fixes x :: name
  and   P  :: pi
  and   a  :: name
  and   y :: name
  and   RP' :: pi

  assumes Trans:  "y>P  ax>  RP'"
  and     xineqy: "x  y"
  and     rcOpen: "P'. P (OutputR a y)  P'; a  y  F ([(x, y)]  P')"
  and     rcResB: "P'. P ax>  P'; y  a  F (y>P')"

  shows "F RP'"
proof -
  from Trans show ?thesis
  proof(induct rule: resCasesB', auto)
    fix Pa Pa' aa b
    assume PTrans: "Pa  (aa::name)[b]  Pa'"
    assume aaineqb: "aab"
    assume TermEq: "y>P = b>Pa"
    assume ResEq: "ax>  RP' = aab>  Pa'"

    have "(c::name). c  (x, a, aa, y, Pa, Pa', b)" by(blast intro: name_exists_fresh)
    then obtain c where cineqx: "cx" and cFresha: "c  a" and cineqy: "c  y" and cineqaa: "c  aa" and cFreshPa: "c  Pa" and cFreshPa': "c  Pa'" and cineqb: "c  b"
      by(force simp add: fresh_prod name_fresh)

    from cFreshPa have "b>Pa = c>([(b, c)]  Pa)" by(rule alphaRes)
    with cineqy TermEq have PEq: "P = [(y, c)]  [(b, c)]  Pa" and yFreshPa: "y  [(b, c)]  Pa"
      by(simp add: pi.inject name_abs_eq)+

    from PTrans have "([(b, c)]  Pa)  ([(b, c)]  (aa[b]  Pa'))" by(rule TransitionsEarly.eqvt)
    with aaineqb cineqaa have L1: "([(b, c)]  Pa)  aa[c]  [(b, c)]  Pa'" by(simp add: name_calc)
    with yFreshPa have yineqaa: "y  aa" by(force dest: freshAction)
    from L1 yFreshPa