Theory Sim_Struct_Cong

(* 
   Title: Psi-calculi   
   Author/Maintainer: Jesper Bengtson (jebe@itu.dk), 2012
*)
theory Sim_Struct_Cong
  imports Simulation
begin

lemma partitionListLeft:
  assumes "xs@ys=xs'@y#ys'"
  and     "y mem xs"
  and     "distinct(xs@ys)"

  obtains zs where "xs = xs'@y#zs" and "ys'=zs@ys"
using assms
by(auto simp add: append_eq_append_conv2 append_eq_Cons_conv)

lemma partitionListRight: 
  assumes "xs@ys=xs'@y#ys'"
  and     "y mem ys"
  and     "distinct(xs@ys)"

  obtains zs where "xs' = xs@zs" and "ys=zs@y#ys'"
using assms
by(force simp add: append_eq_append_conv2 append_eq_Cons_conv)

context env begin

lemma resComm:
  fixes Ψ   :: 'b
  and   x   :: name
  and   y   :: name
  and   Rel :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"
  and   P   :: "('a, 'b, 'c) psi"
  
  assumes "x  Ψ"
  and     "y  Ψ"
  and     "eqvt Rel"
  and     R1: "Ψ' Q. (Ψ', Q, Q)  Rel"
  and     R2: "Ψ' a b Q. a  Ψ'; b  Ψ'  (Ψ', ⦇νa(⦇νbQ), ⦇νb(⦇νaQ))  Rel"

  shows "Ψ  ⦇νx(⦇νyP) ↝[Rel] ⦇νy(⦇νxP)"
proof(case_tac "x=y")
  assume "x = y"
  thus ?thesis using R1
    by(force intro: reflexive)
next
  assume "x  y"
  note eqvt Rel
  moreover from x  Ψ y  Ψ have "[x, y] ♯* Ψ" by(simp add: fresh_star_def)
  moreover have "[x, y] ♯* ⦇νx(⦇νyP)" by(simp add: abs_fresh)
  moreover have "[x, y] ♯* ⦇νy(⦇νxP)" by(simp add: abs_fresh)
  ultimately show ?thesis
  proof(induct rule: simIChainFresh[where C="(x, y)"])
    case(cSim α P')
    from bn α ♯* (x, y) bn α ♯* (⦇νx(⦇νyP)) have "x  bn α" and "y  bn α" and "bn α ♯* P" by simp+
    from [x, y] ♯* α have "x  α" and "y  α" by simp+
    from [x, y] ♯* P' have "x  P'" and "y  P'" by simp+
    from bn α ♯* P x  α have "bn α ♯* ⦇νxP" by(simp add: abs_fresh)
    with Ψ  ⦇νy(⦇νxP) α  P' y  Ψ y  α y  P' bn α ♯* Ψ
    show ?case using bn α ♯* subject α x  α x  P' bn α ♯* Ψ bn α ♯* P bn α ♯* subject α y  α
    proof(induct rule: resCases')
      case(cOpen M yvec1 yvec2 y' N P')
      from yvec1 ♯* yvec2 distinct yvec1 distinct yvec2 have "distinct(yvec1@yvec2)" by auto
      from x  M⦇ν*(yvec1 @ y' # yvec2)⦈⟨N have "x  M" and "x  yvec1" and "x  y'" and "x  yvec2" and "x  N"
        by simp+
      from y  M⦇ν*(yvec1 @ y' # yvec2)⦈⟨N have "y  M" and "y  yvec1" and "y  yvec2"
        by simp+
      from Ψ  ([(y, y')]  ⦇νxP) M⦇ν*(yvec1@yvec2)⦈⟨N  P' x  y x  y'
      have "Ψ  ⦇νx([(y, y')]  P) M⦇ν*(yvec1@yvec2)⦈⟨N  P'" by(simp add: eqvts)
      moreover note x  Ψ
      moreover from x  N x  yvec1 x  yvec2 x  M have "x  M⦇ν*(yvec1@yvec2)⦈⟨N" by simp
      moreover note x  P'
      moreover from yvec1 ♯* Ψ yvec2 ♯* Ψ have "bn(M⦇ν*(yvec1@yvec2)⦈⟨N) ♯* Ψ" by simp
      moreover from yvec1 ♯* ⦇νxP yvec2 ♯* ⦇νxP y  yvec1 y'  yvec1 y  yvec2 y'  yvec2 x  yvec1 x  yvec2
      have "bn(M⦇ν*(yvec1@yvec2)⦈⟨N) ♯* ([(y, y')]  P)" by simp
      moreover from yvec1 ♯* M yvec2 ♯* M have "bn(M⦇ν*(yvec1 @ yvec2)⦈⟨N) ♯* subject(M⦇ν*(yvec1 @ yvec2)⦈⟨N)"
        by simp
      moreover have "bn(M⦇ν*(yvec1 @ yvec2)⦈⟨N) = yvec1@yvec2" by simp
      moreover have "subject(M⦇ν*(yvec1 @ yvec2)⦈⟨N) = Some M" by simp
      moreover have "object(M⦇ν*(yvec1 @ yvec2)⦈⟨N) = Some N" by simp
      ultimately show ?case 
      proof(induct rule: resCases')
        case(cOpen M' xvec1 xvec2 x' N' P')
        from bn(M'⦇ν*(xvec1 @ x' # xvec2)⦈⟨N') = yvec1 @ yvec2 have "yvec1@yvec2 = xvec1@x'#xvec2" by simp
        from subject(M'⦇ν*(xvec1 @ x' # xvec2)⦈⟨N') = Some M have "M = M'" by simp
        from object(M'⦇ν*(xvec1 @ x' # xvec2)⦈⟨N') = Some N have "N = N'" by simp
        from x  yvec1 x  yvec2 y'  yvec1 y'  yvec2 y  yvec1 y  yvec2
        have "x  (yvec1@yvec2)" and "y  (yvec1@yvec2)" and "y'  (yvec1@yvec2)" by simp+
        with yvec1@yvec2 = xvec1@x'#xvec2
        have "x  xvec1" and "x  x'" and "x  xvec2" and "y  xvec1" and "y  x'" and "y  xvec2"
          and "y'  xvec1" and "x'  y'" and "y'  xvec2"
          by auto

        show ?case
        proof(case_tac "x' mem yvec1")
          assume "x' mem yvec1"
        
          with yvec1@yvec2 = xvec1@x'#xvec2 distinct (yvec1@yvec2)
          obtain xvec2' where Eq1: "yvec1=xvec1@x'#xvec2'"
                          and Eq: "xvec2=xvec2'@yvec2"
            by(rule_tac partitionListLeft)
          from Ψ  ([(x, x')]  [(y, y')]  P) M'⦇ν*(xvec1@xvec2)⦈⟨N'  P' y'  supp N y'  Ψ y'  M y'  xvec1 y'  xvec2 Eq M=M' N = N'
          have "Ψ  ⦇νy'([(x, x')]  [(y, y')]  P) M'⦇ν*((xvec1@xvec2')@y'#yvec2)⦈⟨N'  P'" 
            by(rule_tac Open) auto
          then have "Ψ  ⦇νx'(⦇νy'([(x, x')]  [(y, y')]  P)) M⦇ν*(xvec1@x'#xvec2'@y'#yvec2)⦈⟨N  P'" 
            using x'  supp N' x'  Ψ x'  M' x'  xvec1 x'  xvec2 x'  y' Eq M=M' N=N'
            by(rule_tac Open) auto
          with x'  y' x  y' x'  [(y, y')]  P
          have "Ψ  ⦇νx(⦇νy'([(y, y')]  P)) M⦇ν*(xvec1@x'#xvec2'@y'#yvec2)⦈⟨N  P'"
            by(subst alphaRes[where y=x']) (simp add: calc_atm eqvts abs_fresh)+
          with Eq1 y'  ⦇νxP x  y' R1 show ?case
            by(fastforce simp add: alphaRes abs_fresh)
        next
          assume "¬x' mem yvec1"
          hence "x'  yvec1" by(simp add: fresh_def)
          from ¬x' mem yvec1 yvec1@yvec2 = xvec1@x'#xvec2
          have "x' mem yvec2"
            by(fastforce simp add: append_eq_append_conv2 append_eq_Cons_conv
                                  fresh_list_append fresh_list_cons)
          with yvec1@yvec2 = xvec1@x'#xvec2 distinct (yvec1@yvec2)
          obtain xvec2' where Eq: "xvec1=yvec1@xvec2'"
                          and Eq1: "yvec2=xvec2'@x'#xvec2"
            by(rule_tac partitionListRight)
          from Ψ  ([(x, x')]  [(y, y')]  P) M'⦇ν*(xvec1@xvec2)⦈⟨N'  P' y'  supp N y'  Ψ y'  M y'  xvec1 y'  xvec2 Eq M=M' N = N'
          have "Ψ  ⦇νy'([(x, x')]  [(y, y')]  P) M'⦇ν*(yvec1@y'#xvec2'@xvec2)⦈⟨N'  P'" 
            by(rule_tac Open) (assumption | simp)+
          then have "Ψ  ⦇νx'(⦇νy'([(x, x')]  [(y, y')]  P)) M⦇ν*((yvec1@y'#xvec2')@x'#xvec2)⦈⟨N  P'" 
            using x'  supp N' x'  Ψ x'  M' x'  xvec1 x'  xvec2 x'  y' Eq M=M' N=N'
            by(rule_tac Open) auto
          with x'  y' x  y' x'  [(y, y')]  P
          have "Ψ  ⦇νx(⦇νy'([(y, y')]  P)) M⦇ν*((yvec1@y'#xvec2')@x'#xvec2)⦈⟨N  P'"
            by(subst alphaRes[where y=x']) (simp add: calc_atm eqvts abs_fresh)+
          with Eq1 y'  ⦇νxP x  y' R1 show ?case
            by(fastforce simp add: alphaRes abs_fresh)
        qed
      next
        case(cRes P')
        from Ψ  ([(y, y')]  P) M⦇ν*(yvec1@yvec2)⦈⟨N  P' y'  supp N y'  Ψ y'  M y'  yvec1 y'  yvec2
        have "Ψ  ⦇νy'([(y, y')]  P) M⦇ν*(yvec1@y'#yvec2)⦈⟨N  P'" by(rule Open)
        with y'  ⦇νxP x  y'have "Ψ  ⦇νyP M⦇ν*(yvec1@y'#yvec2)⦈⟨N  P'" by(simp add: alphaRes abs_fresh)
        hence "Ψ  ⦇νx(⦇νyP) M⦇ν*(yvec1@y'#yvec2)⦈⟨N  ⦇νxP'" using x  Ψ x  M x  yvec1 x  y' x  yvec2 x  N
          by(rule_tac Scope) auto
        moreover have "(Ψ, ⦇νxP', ⦇νxP')  Rel" by(rule R1)
        ultimately show ?case by blast
      qed
    next
      case(cRes P')
      from x  ⦇νyP' x  y have "x  P'" by(simp add: abs_fresh)
      with Ψ  ⦇νxP α  P' x  Ψ x  α
      show ?case using bn α ♯* Ψ bn α ♯* P bn α ♯* subject α y  α
      proof(induct rule: resCases')
        case(cOpen M xvec1 xvec2 x' N P')
        from y  M⦇ν*(xvec1@x'#xvec2)⦈⟨N have "y  x'" and "y  M⦇ν*(xvec1@xvec2)⦈⟨N" by simp+
        from Ψ  ([(x, x')]  P) M⦇ν*(xvec1@xvec2)⦈⟨N  P' y  Ψ y  M⦇ν*(xvec1@xvec2)⦈⟨N
        have "Ψ  ⦇νy([(x, x')]  P) M⦇ν*(xvec1@xvec2)⦈⟨N  ⦇νyP'" 
          by(rule Scope)
        hence "Ψ  ⦇νx'(⦇νy([(x, x')]  P)) M⦇ν*(xvec1@x'#xvec2)⦈⟨N  ⦇νyP'" 
          using x'  supp N x'  Ψ x'  M x'  xvec1 x'  xvec2
          by(rule Open)
        with y  x' x  y x'  P have "Ψ  ⦇νx(⦇νyP) M⦇ν*(xvec1@x'#xvec2)⦈⟨N  ⦇νyP'"
          by(subst alphaRes[where y=x']) (simp add: abs_fresh eqvts calc_atm)+
        moreover have "(Ψ, ⦇νyP', ⦇νyP')  Rel" by(rule R1)
        ultimately show ?case by blast
      next
        case(cRes P')
        from Ψ  P α  P' y  Ψ y  α
        have "Ψ  ⦇νyP α  ⦇νyP'" by(rule Scope)
        hence "Ψ  ⦇νx(⦇νyP) α  ⦇νx(⦇νyP')" using x  Ψ x  α
          by(rule Scope)
        moreover from x  Ψ y  Ψ have "(Ψ, ⦇νx(⦇νyP'), ⦇νy(⦇νxP'))  Rel"
          by(rule R2)
        ultimately show ?case by blast
      qed
    qed
  qed
qed

lemma parAssocLeft:
  fixes Ψ   :: 'b
  and   P   :: "('a, 'b, 'c) psi"
  and   Q   :: "('a, 'b, 'c) psi"
  and   R   :: "('a, 'b, 'c) psi"
  and   Rel :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"

  assumes "eqvt Rel"
  and     C1: "Ψ' S T U. (Ψ, (S  T)  U, S  (T  U))  Rel"
  and     C2: "xvec Ψ' S T U. xvec ♯* Ψ'; xvec ♯* S  (Ψ', ⦇ν*xvec((S  T)  U), S  (⦇ν*xvec(T  U)))  Rel"
  and     C3: "xvec Ψ' S T U. xvec ♯* Ψ'; xvec ♯* U  (Ψ', (⦇ν*xvec(S  T))  U, ⦇ν*xvec(S  (T  U)))  Rel"
  and     C4: "Ψ' S T xvec. (Ψ', S, T)  Rel; xvec ♯* Ψ'  (Ψ', ⦇ν*xvecS, ⦇ν*xvecT)  Rel"

  shows "Ψ  (P  Q)  R ↝[Rel] P  (Q  R)"
using eqvt Rel
proof(induct rule: simI[of _ _ _ _ "()"])
  case(cSim α PQR) 
  from bn α ♯* (P  Q  R) have "bn α ♯* P" and "bn α ♯* Q" and "bn α ♯* R" by simp+
  hence "bn α ♯* (Q  R)" by simp
  with Ψ  P  (Q  R) α  PQR bn α ♯* Ψ bn α ♯* P
  show ?case using bn α ♯* subject α
  proof(induct rule: parCases[where C = "(Ψ, P, Q, R, α)"])
    case(cPar1 P' AQR ΨQR)
    from AQR ♯* (Ψ, P, Q, R, α) have "AQR ♯* Q" and  "AQR ♯* R"
      by simp+
    with extractFrame(Q  R) = AQR, ΨQR distinct AQR
    obtain AQ ΨQ AR ΨR where "AQR = AQ@AR" and "ΨQR = ΨQ  ΨR" and FrQ: "extractFrame Q = AQ, ΨQ" and  FrR: "extractFrame R = AR, ΨR"
                           and "AQ ♯* ΨR" and "AR ♯* ΨQ"
      by(rule_tac mergeFrameE) (auto dest: extractFrameFreshChain)

    from AQR = AQ@AR AQR ♯* Ψ AQR ♯* P AQR ♯* Q AQR ♯* α
    have "AQ ♯* Ψ" and "AR ♯* Ψ" and "AQ ♯* P" and "AR ♯* P" and "AQ ♯* Q" and "AR ♯* Q" and "AQ ♯* α" and "AR ♯* α"
      by simp+

    from Ψ  ΨQR  P α  P' ΨQR = ΨQ  ΨR have "(Ψ  ΨR)  ΨQ  P α  P'"
      by(metis statEqTransition Associativity Commutativity Composition)
    hence "Ψ  ΨR  P  Q α  (P'  Q)" using FrQ bn α ♯* Q AQ ♯* Ψ AQ ♯* ΨR AQ ♯* P AQ ♯* α
      by(rule_tac Par1) auto
    hence "Ψ  (P  Q)  R α  ((P'  Q)  R)" using FrR bn α ♯* R AR ♯* Ψ AR ♯* P AR ♯* Q AR ♯* α
      by(rule_tac Par1) auto
    moreover have "(Ψ, (P'  Q)  R, P'  (Q  R))  Rel" by(rule C1)
    ultimately show ?case by blast
  next
    case(cPar2 QR AP ΨP)
    from AP ♯* (Ψ, P, Q, R, α) have "AP ♯* Q" and "AP ♯* R" and "AP ♯* α"
      by simp+
    have FrP: "extractFrame P = AP, ΨP" by fact
    with bn α ♯* P AP ♯* α have "bn α ♯* ΨP" by(auto dest: extractFrameFreshChain)
    with bn α ♯* Ψ have "bn α ♯* (Ψ  ΨP)" by force
    with Ψ  ΨP  Q  R α  QR
    show ?case using bn α ♯* Q bn α ♯* R bn α ♯* subject α AP ♯* Q AP ♯* R
    proof(induct rule: parCasesSubject[where C = "(AP, ΨP, P, Q, R, Ψ)"])
      case(cPar1 Q' AR ΨR)
      from AR ♯* (AP, ΨP, P, Q, R, Ψ) have "AR ♯* AP" and "AR ♯* P" and "AR ♯* Q" and "AR ♯* ΨP" and "AR ♯* Ψ"
        by simp+
      from AP ♯* R extractFrame R = AR, ΨR AR ♯* AP have "AP ♯* ΨR"
        by(drule_tac extractFrameFreshChain) auto
      from (Ψ  ΨP)  ΨR  Q α  Q' have "(Ψ  ΨR)  ΨP  Q α  Q'" 
        by(metis statEqTransition Associativity Commutativity Composition)
      hence "Ψ  ΨR  P  Q α  (P  Q')"
        using FrP bn α ♯* P AP ♯* Ψ AP ♯* ΨR AP ♯* Q AP ♯* α
        by(rule_tac Par2) (assumption | force)+
      hence "Ψ  (P  Q)  R α  ((P  Q')  R)"
        using extractFrame R = AR, ΨR bn α ♯* R AR ♯* Ψ AR ♯* P AR ♯* Q AR ♯* α
        by(rule_tac Par1) (assumption | simp)+
      moreover have "(Ψ, (P  Q')  R, P  (Q'  R))  Rel" by(rule C1)
      ultimately show ?case by blast
    next
      case(cPar2 R' AQ ΨQ)
      from AQ ♯* (AP, ΨP, P, Q, R, Ψ) have "AQ ♯* AP" and "AQ ♯* R" and "AQ ♯* ΨP" and "AQ ♯* Ψ"
        by simp+
      have FrQ: "extractFrame Q = AQ, ΨQ" by fact
      from AP ♯* Q FrQ AQ ♯* AP have "AP ♯* ΨQ"
        by(drule_tac extractFrameFreshChain) auto
      from (Ψ  ΨP)  ΨQ  R α  R'
      have "Ψ  (ΨP  ΨQ)  R α  R'"
        by(blast intro: statEqTransition Associativity)
      moreover from FrP FrQ AQ ♯* AP AP ♯* ΨQ  AQ ♯* ΨP 
      have "extractFrame(P  Q) = (AP@AQ), ΨP  ΨQ " by simp
      moreover from bn α ♯* P bn α ♯* Q have "bn α ♯* (P  Q)" by simp
      moreover from AP ♯* Ψ AQ ♯* Ψ have "(AP@AQ) ♯* Ψ" by simp
      moreover from AP ♯* R AQ ♯* R have "(AP@AQ) ♯* R" by simp
      moreover from AP ♯* α AQ ♯* α have "(AP@AQ) ♯* α" by simp
      ultimately have "Ψ  (P  Q)  R α  ((P  Q)  R')"
        by(rule Par2) 
      moreover have "(Ψ, (P  Q)  R', P  (Q  R'))  Rel" by(rule C1)
      ultimately show ?case by blast
    next
      case(cComm1 ΨR M N Q' AQ ΨQ K xvec R' AR) 
      from AQ ♯* (AP, ΨP, P, Q, R, Ψ)
      have "AQ ♯* P" and "AQ ♯* Q" and "AQ ♯* R" and "AQ ♯* AP" and "AQ ♯* ΨP"  and "AQ ♯* Ψ" by simp+
      from AR ♯* (AP, ΨP, P, Q, R, Ψ) have "AR ♯* P" and "AR ♯* Q" and "AR ♯* R" and "AR ♯* AP"  and "AR ♯* Ψ" by simp+
      from xvec ♯* (AP,  ΨP, P, Q, R, Ψ) have "xvec ♯* AP" and "xvec ♯* P" and "xvec ♯* Q" and "xvec ♯* Ψ" by simp+

      have FrQ: "extractFrame Q = AQ, ΨQ" by fact
      with AP ♯* Q AQ ♯* AP have "AP ♯* ΨQ"
        by(drule_tac extractFrameFreshChain) auto
      have FrR: "extractFrame R = AR, ΨR" by fact
      with AP ♯* R AR ♯* AP have "AP ♯* ΨR"
        by(drule_tac extractFrameFreshChain) auto
      from (Ψ  ΨP)  ΨQ  R K⦇ν*xvec⦈⟨N  R' AP ♯* R xvec ♯* AP xvec ♯* K distinct xvec have "AP ♯* N" 
        by(rule_tac outputFreshChainDerivative) auto

      from (Ψ  ΨP)  ΨR  Q MN  Q' have "(Ψ  ΨR)  ΨP  Q MN  Q'"
        by(metis statEqTransition Associativity Commutativity Composition)
      hence "Ψ  ΨR  P  Q MN  (P  Q')" using FrP AP ♯* Ψ AP ♯* ΨR AP ♯* Q AP ♯* M AP ♯* N
        by(rule_tac Par2) auto
      moreover from FrP FrQ AP ♯* ΨQ AQ ♯* AP AQ ♯* ΨP have "extractFrame(P  Q) = (AP@AQ), ΨP  ΨQ"
        by simp
      moreover from  (Ψ  ΨP)  ΨQ  R K⦇ν*xvec⦈⟨N  R' have "Ψ  ΨP  ΨQ  R K⦇ν*xvec⦈⟨N  R'"
        by(metis statEqTransition Associativity)
      moreover note extractFrame R = AR, ΨR
      moreover from (Ψ  ΨP)  ΨQ  ΨR  M  K have "Ψ  (ΨP  ΨQ)  ΨR  M  K"
        by(metis statEqEnt Associativity Commutativity Composition)
      ultimately have "Ψ  (P  Q)  R τ  ⦇ν*xvec((P  Q')  R')"
        using AP ♯* Ψ AQ ♯* Ψ AR ♯* Ψ AP ♯* P AQ ♯* P AR ♯* P AP ♯* Q AQ ♯* Q AR ♯* Q AP ♯* R AQ ♯* R AR ♯* R
              AP ♯* M AQ ♯* M AR ♯* K AR ♯* AP AQ ♯* AR xvec ♯* P xvec ♯* Q
        by(rule_tac Comm1) (assumption | simp)+
      moreover from xvec ♯* Ψ xvec ♯* P have "(Ψ, ⦇ν*xvec((P  Q')  R'), P  (⦇ν*xvec(Q'  R')))  Rel"
        by(rule C2)
      ultimately show ?case by blast
    next
      case(cComm2 ΨR M xvec N Q' AQ ΨQ K R' AR) 
      from AQ ♯* (AP,  ΨP, P, Q, R, Ψ)
      have "AQ ♯* P" and "AQ ♯* Q" and "AQ ♯* R" and "AQ ♯* AP" and "AQ ♯* Ψ" and "AQ ♯* ΨP" by simp+
      from AR ♯* (AP,  ΨP, P, Q, R, Ψ) have "AR ♯* P" and "AR ♯* Q" and "AR ♯* R" and "AR ♯* AP"and "AR ♯* Ψ" by simp+
      from xvec ♯* (AP,  ΨP, P, Q, R, Ψ) have "xvec ♯* AP" and "xvec ♯* P" and "xvec ♯* Q" and "xvec ♯* Ψ" by simp+

      have FrQ: "extractFrame Q = AQ, ΨQ" by fact
      with AP ♯* Q AQ ♯* AP have "AP ♯* ΨQ"
        by(drule_tac extractFrameFreshChain) auto
      have FrR: "extractFrame R = AR, ΨR" by fact
      with AP ♯* R AR ♯* AP have "AP ♯* ΨR"
        by(drule_tac extractFrameFreshChain) auto

      from (Ψ  ΨP)  ΨR  Q M⦇ν*xvec⦈⟨N  Q' AP ♯* Q xvec ♯* AP xvec ♯* M distinct xvec have "AP ♯* N" 
        by(rule_tac outputFreshChainDerivative) auto

      from (Ψ  ΨP)  ΨR  Q M⦇ν*xvec⦈⟨N  Q' have "(Ψ  ΨR)  ΨP  Q M⦇ν*xvec⦈⟨N  Q'"
        by(metis statEqTransition Associativity Commutativity Composition)
      hence "Ψ  ΨR  P  Q M⦇ν*xvec⦈⟨N  (P  Q')" using FrP AP ♯* Ψ AP ♯* ΨR AP ♯* Q AP ♯* M AP ♯* N xvec ♯* P xvec ♯* AP
        by(rule_tac Par2) auto
      moreover from FrP FrQ AP ♯* ΨQ AQ ♯* AP AQ ♯* ΨP have "extractFrame(P  Q) = (AP@AQ), ΨP  ΨQ"
        by simp+
      moreover from  (Ψ  ΨP)  ΨQ  R KN  R' have "Ψ  ΨP  ΨQ  R KN  R'"
        by(metis statEqTransition Associativity)
      moreover note extractFrame R = AR, ΨR
      moreover from (Ψ  ΨP)  ΨQ  ΨR  M  K have "Ψ  (ΨP  ΨQ)  ΨR  M  K"
        by(metis statEqEnt Associativity Commutativity Composition)
      ultimately have "Ψ  (P  Q)  R τ  ⦇ν*xvec((P  Q')  R')"
        using AP ♯* Ψ AQ ♯* Ψ AR ♯* Ψ AP ♯* P AQ ♯* P AR ♯* P AP ♯* Q AQ ♯* Q AR ♯* Q AP ♯* R AQ ♯* R AR ♯* R
              AP ♯* M AQ ♯* M AR ♯* K AR ♯* AP AQ ♯* AR xvec ♯* R
        by(rule_tac Comm2) (assumption | simp)+
      moreover from xvec ♯* Ψ xvec ♯* P have "(Ψ, ⦇ν*xvec((P  Q')  R'), P  (⦇ν*xvec(Q'  R')))  Rel"
        by(rule C2)
      ultimately show ?case by blast
    qed
  next
    case(cComm1 ΨQR M N P' AP ΨP K xvec QR' AQR)
    from xvec ♯* (Ψ, P, Q, R, α) have "xvec ♯* Q" and "xvec ♯* R" by simp+
    from AQR ♯* (Ψ, P, Q, R, α) have "AQR ♯* Q" and "AQR ♯* R" and "AQR ♯* Ψ" by simp+
    from AP ♯* (Q  R) have "AP ♯* Q" and "AP ♯* R" by simp+
    have PTrans: "Ψ  ΨQR  P MN  P'" and FrP: "extractFrame P = AP, ΨP" and MeqK: "Ψ  ΨP  ΨQR  M  K" by fact+
    note Ψ  ΨP  Q  R K⦇ν*xvec⦈⟨N  QR'  
    moreover from xvec ♯* Ψ xvec ♯* ΨP have "xvec ♯* (Ψ  ΨP)" by force
    moreover note xvec ♯* Qxvec ♯* R xvec ♯* K
         extractFrame(Q  R) = AQR, ΨQR distinct AQR 
    moreover from AQR ♯* Ψ AQR ♯* ΨP have "AQR ♯* (Ψ  ΨP)" by force
    ultimately show ?case using AQR ♯* Q AQR ♯* R AQR ♯* K
    proof(induct rule: parCasesOutputFrame)
      case(cPar1 Q' AQ ΨQ AR ΨR)
      have Aeq: "AQR = AQ@AR" and Ψeq: "ΨQR = ΨQ  ΨR" by fact+
      from PTrans Ψeq have "(Ψ  ΨR)  ΨQ  P MN  P'"
        by(metis statEqTransition Associativity Commutativity Composition)
      moreover note FrP
      moreover from (Ψ  ΨP)  ΨR  Q K⦇ν*xvec⦈⟨N  Q' have "(Ψ  ΨR)  ΨP  Q K⦇ν*xvec⦈⟨N  Q'"
        by(metis statEqTransition Associativity Commutativity Composition)
      moreover note extractFrame Q = AQ, ΨQ
      moreover from MeqK Ψeq have "(Ψ  ΨR)  ΨP  ΨQ  M  K"
        by(metis statEqEnt Associativity Commutativity Composition)
      moreover from AP ♯* R AP ♯* AQR Aeq extractFrame R = AR, ΨR have "AP ♯* AQ" and "AP ♯* ΨR"
        by(auto dest:  extractFrameFreshChain)
      moreover from AQR ♯* P AQR ♯* Ψ Aeq have "AQ ♯* P" and "AQ ♯* Ψ" by simp+
      ultimately have "Ψ  ΨR  P  Q τ  ⦇ν*xvec(P'  Q')"
        using AP ♯* Ψ AP ♯* P AP ♯* Q AP ♯* M AP ♯* AQ AQ ♯* Ψ AQ ♯* ΨR AQ ♯* P AQ ♯* Q AQ ♯* K xvec ♯* P
        by(rule_tac Comm1) (assumption | force)+
      moreover from AQR ♯* Ψ Aeq have "AR ♯* Ψ" by simp
      moreover from AQR ♯* P Aeq have "AR ♯* P" by simp
      ultimately have "Ψ  (P  Q)  R τ  (⦇ν*xvec(P'  Q'))  R" using extractFrame R = AR, ΨR AR ♯* Q
        by(rule_tac Par1) (assumption | simp)+
      moreover from xvec ♯* Ψ xvec ♯* R have "(Ψ, (⦇ν*xvec(P'  Q'))  R, ⦇ν*xvec(P'  (Q'  R)))  Rel"
        by(rule C3)
      ultimately show ?case by blast
    next
      case(cPar2 R' AQ ΨQ AR ΨR)
      have Aeq: "AQR = AQ@AR" and Ψeq: "ΨQR = ΨQ  ΨR" by fact+
      from AQR ♯* Ψ AQR ♯* P AQR ♯* ΨP AP ♯* AQR Aeq have "AR ♯* Ψ" and "AR ♯* ΨP" and "AP ♯* AR" and "AP ♯* AQ" and "AR ♯* P" by simp+
      from AQR ♯* Ψ Aeq have "AQ ♯* Ψ" by simp
      from AQR ♯* P AP ♯* AQR Aeq FrP have "AQ ♯* ΨP" by(auto dest: extractFrameFreshChain)
      from AP ♯* AQR extractFrame R = AR, ΨR extractFrame Q = AQ, ΨQ Aeq AP ♯* Q AP ♯* R have "AP ♯* ΨQ" and  "AP ♯* ΨR" by(auto dest: extractFrameFreshChain)
      have RTrans: "(Ψ  ΨP)  ΨQ  R K⦇ν*xvec⦈⟨N  R'" and FrR: "extractFrame R = AR, ΨR" by fact+
      then obtain K' where KeqK': "((Ψ  ΨP)  ΨQ)  ΨR  K  K'" and "AP ♯* K'" and "AQ ♯* K'"
      using AP ♯* R AQ ♯* R AR ♯* Ψ AR ♯* ΨP AR ♯* ΨQ AQ ♯* AR AP ♯* AR AR ♯* R AR ♯* R AR ♯* K distinct AR xvec ♯* K distinct xvec
        by(rule_tac B="AP@AQ" in obtainPrefix) (assumption | force)+
      from PTrans Ψeq have "(Ψ  ΨR)  ΨQ  P MN  P'"
        by(metis statEqTransition Associativity Commutativity Composition)
      moreover from MeqK KeqK' Ψeq have MeqK': "((Ψ  ΨR)  ΨQ)  ΨP  M  K'"
        by(metis statEqEnt Associativity Commutativity Composition chanEqTrans)
      ultimately have "(Ψ  ΨR)  ΨQ  P K'N  P'" using FrP distinct AP AP ♯* Ψ AP ♯* P AP ♯* M AP ♯* K' AP ♯* ΨQ AP ♯* ΨR
        by(rule_tac inputRenameSubject) auto
      moreover from AQR ♯* P AQR ♯* N Aeq have "AQ ♯* P" and "AQ ♯* N" by simp+
      ultimately have "Ψ  ΨR  P  Q K'N  P'  Q" using extractFrame Q = AQ, ΨQ AQ ♯* ΨR AQ ♯* K' AQ ♯* Ψ
        by(rule_tac Par1) (assumption | force)+
      moreover from FrP extractFrame Q = AQ, ΨQ AP ♯* AQ AP ♯* ΨQ AQ ♯* ΨP
      have "extractFrame(P  Q) = (AP@AQ), ΨP  ΨQ" by simp+
      moreover from RTrans have "Ψ  (ΨP  ΨQ)  R K⦇ν*xvec⦈⟨N  R'" by(metis Associativity statEqTransition)
      moreover note FrR
      moreover from MeqK' KeqK' have "Ψ  (ΨP  ΨQ)  ΨR  K'  K"
        by(metis statEqEnt Associativity Commutativity Composition chanEqTrans chanEqSym)
      ultimately have "Ψ  (P  Q)  R τ  ⦇ν*xvec((P'  Q)  R')"
        using AP ♯* Ψ AQ ♯* Ψ AP ♯* P AQ ♯* P AP ♯* Q AQ ♯* Q AP ♯* R AQ ♯* R AP ♯* K' AQ ♯* K' AP ♯* AR AQ ♯* AR
              AR ♯* Ψ AR ♯* P AR ♯* Q AR ♯* R AR ♯* K xvec ♯* P xvec ♯* Q
        by(rule_tac Comm1) (assumption | simp)+
      moreover from xvec ♯* Ψ have "(Ψ, ⦇ν*xvec((P'  Q)  R'), ⦇ν*xvec(P'  (Q  R')))  Rel"
        by(metis C1 C4)
      ultimately show ?case by blast
    qed
  next
    case(cComm2 ΨQR M xvec N P' AP ΨP K QR' AQR)
    from AQR ♯* (Ψ, P, Q, R, α) have "AQR ♯* Q" and "AQR ♯* R" and "AQR ♯* Ψ" by simp+
    from AP ♯* (Q  R) xvec ♯* (Q  R) have "AP ♯* Q" and "AP ♯* R" and "xvec ♯* Q" and "xvec ♯* R" by simp+
    have PTrans: "Ψ  ΨQR  P M⦇ν*xvec⦈⟨N  P'" and FrP: "extractFrame P = AP, ΨP" and MeqK: "Ψ  ΨP  ΨQR  M  K" by fact+
    note Ψ  ΨP  Q  R KN  QR' extractFrame(Q  R) = AQR, ΨQR distinct AQR 
    moreover from AQR ♯* Ψ AQR ♯* ΨP have "AQR ♯* (Ψ  ΨP)" by force
    ultimately show ?case using AQR ♯* Q AQR ♯* R AQR ♯* K
    proof(induct rule: parCasesInputFrame)
      case(cPar1 Q' AQ ΨQ AR ΨR)
      have Aeq: "AQR = AQ@AR" and Ψeq: "ΨQR = ΨQ  ΨR" by fact+
      from PTrans Ψeq have "(Ψ  ΨR)  ΨQ  P M⦇ν*xvec⦈⟨N  P'"
        by(metis statEqTransition Associativity Commutativity Composition)
      moreover note FrP
      moreover from (Ψ  ΨP)  ΨR  Q KN  Q' have "(Ψ  ΨR)  ΨP  Q KN  Q'"
        by(metis statEqTransition Associativity Commutativity Composition)
      moreover note extractFrame Q = AQ, ΨQ
      moreover from MeqK Ψeq have "(Ψ  ΨR)  ΨP  ΨQ  M  K"
        by(metis statEqEnt Associativity Commutativity Composition)
      moreover from AP ♯* Q AP ♯* R AP ♯* AQR Aeq extractFrame Q = AQ, ΨQ extractFrame R = AR, ΨR
      have "AP ♯* AQ" and "AP ♯* ΨR" by(auto dest: extractFrameFreshChain)
      moreover from AQR ♯* Ψ  AQR ♯* P Aeq have "AQ ♯* Ψ" and "AQ ♯* P" by simp+
      ultimately have "Ψ  ΨR  P  Q τ  ⦇ν*xvec(P'  Q')"
        using AP ♯* Ψ AP ♯* P AP ♯* Q AP ♯* M AP ♯* AQ AQ ♯* Ψ AQ ♯* ΨR AQ ♯* P AQ ♯* Q AQ ♯* K xvec ♯* Q
        by(rule_tac Comm2) (assumption | force)+
      moreover from AQR ♯* Ψ AQR ♯* P Aeq have "AR ♯* Ψ" and "AR ♯* P" by simp+
      ultimately have "Ψ  (P  Q)  R τ  (⦇ν*xvec(P'  Q'))  R" using extractFrame R = AR, ΨR AR ♯* Q
        by(rule_tac Par1) (assumption | simp)+
      moreover from xvec ♯* Ψ xvec ♯* R have "(Ψ, (⦇ν*xvec(P'  Q'))  R, ⦇ν*xvec(P'  (Q'  R)))  Rel"
        by(rule C3)
      ultimately show ?case by blast
    next
      case(cPar2 R' AQ ΨQ AR ΨR)
      have Aeq: "AQR = AQ@AR" and Ψeq: "ΨQR = ΨQ  ΨR" by fact+
      from AQR ♯* Ψ AQR ♯* P AQR ♯* ΨP AP ♯* AQR Aeq 
      have "AR ♯* Ψ" and "AR ♯* ΨP" and "AP ♯* AR" and "AP ♯* AQ" and "AR ♯* P" and "AQ ♯* Ψ" and "AQ ♯* ΨP" by simp+
      have RTrans: "(Ψ  ΨP)  ΨQ  R KN  R'" and FrR: "extractFrame R = AR, ΨR" by fact+
      then obtain K' where KeqK': "((Ψ  ΨP)  ΨQ)  ΨR  K  K'" and "AP ♯* K'" and "AQ ♯* K'"
      using AP ♯* R AQ ♯* R AR ♯* Ψ AR ♯* ΨP AR ♯* ΨQ AQ ♯* AR AP ♯* AR AR ♯* R AR ♯* R AR ♯* K distinct AR
        by(rule_tac B="AP@AQ" in obtainPrefix) (assumption | force)+
      from PTrans Ψeq have "(Ψ  ΨR)  ΨQ  P M⦇ν*xvec⦈⟨N  P'"
        by(metis statEqTransition Associativity Commutativity Composition)
      moreover from MeqK KeqK' Ψeq have MeqK': "((Ψ  ΨR)  ΨQ)  ΨP  M  K'"
        by(metis statEqEnt Associativity Commutativity Composition chanEqTrans)
      moreover from AP ♯* R AP ♯* Q AP ♯* AQR FrR extractFrame Q = AQ, ΨQ Aeq have "AP ♯* ΨQ" and "AP ♯* ΨR"
        by(auto dest: extractFrameFreshChain)
      ultimately have "(Ψ  ΨR)  ΨQ  P K'⦇ν*xvec⦈⟨N  P'" using FrP distinct AP AP ♯* Ψ AP ♯* P AP ♯* M AP ♯* K'
        by(rule_tac outputRenameSubject) auto
      moreover from AQR ♯* P AQR ♯* N AQR ♯* xvec Aeq have "AQ ♯* P" and "AQ ♯* N" and "AQ ♯* xvec" by simp+
      ultimately have "Ψ  ΨR  P  Q K'⦇ν*xvec⦈⟨N  (P'  Q)" using extractFrame Q = AQ, ΨQ AQ ♯* ΨR AQ ♯* K' xvec ♯* Q AQ ♯* Ψ
        by(rule_tac Par1) (assumption | force)+
      moreover from FrP extractFrame Q = AQ, ΨQ AP ♯* AQ AP ♯* ΨQ AQ ♯* ΨP
      have "extractFrame(P  Q) = (AP@AQ), ΨP  ΨQ" by simp+
      moreover from RTrans have "Ψ  (ΨP  ΨQ)  R KN  R'" by(metis Associativity statEqTransition)
      moreover note FrR
      moreover from MeqK' KeqK' have "Ψ  (ΨP  ΨQ)  ΨR  K'  K"
        by(metis statEqEnt Associativity Commutativity Composition chanEqTrans chanEqSym)
      ultimately have "Ψ  (P  Q)  R τ  ⦇ν*xvec((P'  Q)  R')"
        using AP ♯* Ψ AQ ♯* Ψ AP ♯* P AQ ♯* P AP ♯* Q AQ ♯* Q AP ♯* R AQ ♯* R AP ♯* K' AQ ♯* K' AP ♯* AR AQ ♯* AR
              AR ♯* Ψ AR ♯* P AR ♯* Q AR ♯* R AR ♯* K xvec ♯* R
        by(rule_tac Comm2) (assumption | simp)+
      moreover from xvec ♯* Ψ have "(Ψ, ⦇ν*xvec((P'  Q)  R'), ⦇ν*xvec(P'  (Q  R')))  Rel"
        by(metis C1 C4)
      ultimately show ?case by blast
    qed
  qed
qed

lemma parNilLeft:
  fixes Ψ :: 'b
  and   P   :: "('a, 'b, 'c) psi"
  and   Rel :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"  

  assumes "eqvt Rel"
  and     C1: "Q. (Ψ, Q  𝟬, Q)  Rel"

  shows "Ψ  (P  𝟬) ↝[Rel] P"
using eqvt Rel
proof(induct rule: simI[of _ _ _ _ "()"])
  case(cSim α P')
  from Ψ  P α  P' have "Ψ  SBottom'  P α  P'"
    by(metis statEqTransition Identity AssertionStatEqSym)
  hence "Ψ  (P  𝟬) α  (P'  𝟬)"
    by(rule_tac Par1) auto
  moreover have "(Ψ, P'  𝟬, P')  Rel" by(rule C1)
  ultimately show ?case by blast
qed

lemma parNilRight:
  fixes Ψ :: 'b
  and   P   :: "('a, 'b, 'c) psi"
  and   Rel :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"  

  assumes "eqvt Rel"
  and     C1: "Q. (Ψ, Q, (Q  𝟬))  Rel"

  shows "Ψ  P ↝[Rel] (P  𝟬)"
using eqvt Rel
proof(induct rule: simI[of _ _ _ _ "()"])
  case(cSim α P')
  note Ψ  P  𝟬 α  P' bn α ♯* Ψ bn α ♯* P
  moreover have "bn α ♯* 𝟬" by simp
  ultimately show ?case using bn α ♯* subject α
  proof(induct rule: parCases[where C="()"])
    case(cPar1 P' AQ ΨQ)
    from extractFrame(𝟬) = AQ, ΨQ have "ΨQ = SBottom'" by auto
    with Ψ  ΨQ  P α  P' have "Ψ  P α  P'"
      by(metis statEqTransition Identity)
    moreover have "(Ψ, P', P'  𝟬)  Rel" by(rule C1)
    ultimately show ?case by blast
  next
    case(cPar2 Q' AP ΨP)
    from Ψ  ΨP  𝟬 α  Q' have False
      by auto
    thus ?case by simp
  next
    case(cComm1 ΨQ M N P' AP ΨP K xvec Q' AQ)
    from Ψ  ΨP  𝟬 K⦇ν*xvec⦈⟨N  Q' have False by auto
    thus ?case by simp
  next
    case(cComm2 ΨQ M xvec N P' AP ΨP K Q' AQ)
    from Ψ  ΨP  𝟬 KN  Q' have False
      by auto
    thus ?case by simp
  qed
qed

lemma resNilLeft:
  fixes x   :: name
  and   Ψ   :: 'b
  and   Rel :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"

  shows "Ψ  ⦇νx𝟬 ↝[Rel] 𝟬"
by(auto simp add: simulation_def)

lemma resNilRight:
  fixes x   :: name
  and   Ψ   :: 'b
  and   Rel :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"

  shows "Ψ  𝟬 ↝[Rel] ⦇νx𝟬"
apply(auto simp add: simulation_def)
by(cases rule: semantics.cases) (auto simp add: psi.inject alpha')

lemma inputPushResLeft:
  fixes Ψ   :: 'b
  and   x    :: name
  and   M    :: 'a
  and   xvec :: "name list"
  and   N    :: 'a
  and   P    :: "('a, 'b, 'c) psi"

  assumes "eqvt Rel"
  and     "x  Ψ"
  and     "x  M"
  and     "x  xvec"
  and     "x  N"
  and     C1: "Q. (Ψ, Q, Q)  Rel"

  shows "Ψ  ⦇νx(M⦇λ*xvec N⦈.P) ↝[Rel] M⦇λ*xvec N⦈.⦇νxP"
proof -
  note eqvt Rel x  Ψ
  moreover have "x  ⦇νx(M⦇λ*xvec N⦈.P)" by(simp add: abs_fresh)
  moreover from x  M x  N have "x  M⦇λ*xvec N⦈.⦇νxP"
    by(auto simp add: inputChainFresh abs_fresh)
  ultimately show ?thesis
  proof(induct rule: simIFresh[of _ _ _ _ _ "()"])
    case(cSim α P')
    from Ψ  M⦇λ*xvec N⦈.⦇νxP α  P' x  α show ?case
    proof(induct rule: inputCases)
      case(cInput K Tvec)
      from x  KN[xvec::=Tvec] have "x  K" and "x  N[xvec::=Tvec]" by simp+
      from Ψ  M  K distinct xvec set xvec  supp N length xvec = length Tvec
      have "Ψ  M⦇λ*xvec N⦈.P K(N[xvec::=Tvec])  P[xvec::=Tvec]"
        by(rule Input)
      hence "Ψ  ⦇νx(M⦇λ*xvec N⦈.P) K(N[xvec::=Tvec])  ⦇νx(P[xvec::=Tvec])" using x  Ψ x  K x  N[xvec::=Tvec]
        by(rule_tac Scope) auto
      moreover from length xvec = length Tvec distinct xvec set xvec  supp N x  N[xvec::=Tvec] have "x  Tvec"
        by(rule substTerm.subst3)
      with x  xvec have "(Ψ, ⦇νx(P[xvec::=Tvec]), (⦇νxP)[xvec::=Tvec])  Rel"
        by(force intro: C1)
      ultimately show ?case by blast
    qed
  qed
qed
 
lemma inputPushResRight:
  fixes Ψ   :: 'b
  and   x    :: name
  and   M    :: 'a
  and   xvec :: "name list"
  and   N    :: 'a
  and   P    :: "('a, 'b, 'c) psi"

  assumes "eqvt Rel"
  and     "x  Ψ"
  and     "x  M"
  and     "x  xvec"
  and     "x  N"
  and     C1: "Q. (Ψ, Q, Q)  Rel"

  shows "Ψ  M⦇λ*xvec N⦈.⦇νxP ↝[Rel] ⦇νx(M⦇λ*xvec N⦈.P)"
proof -
  note eqvt Rel x  Ψ
  moreover from x  M x  N have "x  M⦇λ*xvec N⦈.⦇νxP"
    by(auto simp add: inputChainFresh abs_fresh)
  moreover have "x  ⦇νx(M⦇λ*xvec N⦈.P)" by(simp add: abs_fresh)
  ultimately show ?thesis
  proof(induct rule: simIFresh[of _ _ _ _ _ "()"])
    case(cSim α P')
    note Ψ  ⦇νx(M⦇λ*xvec N⦈.P) α  P' x  Ψ x  α x  P' bn α ♯* Ψ 
    moreover from bn α ♯* (⦇νx(M⦇λ*xvec N⦈.P)) x  α have  "bn α ♯* (M⦇λ*xvec N⦈.P)"
      by simp
    ultimately show ?case using bn α ♯* subject α
    proof(induct rule: resCases)
      case(cRes P')
      from Ψ  M⦇λ*xvec N⦈.P α  P' x  α show ?case
      proof(induct rule: inputCases)
        case(cInput K Tvec)
        from x  KN[xvec::=Tvec] have "x  K" and "x  N[xvec::=Tvec]" by simp+
        from Ψ  M  K distinct xvec set xvec  supp N length xvec = length Tvec
        have "Ψ  M⦇λ*xvec N⦈.(⦇νxP) K(N[xvec::=Tvec])  (⦇νxP)[xvec::=Tvec]"
          by(rule Input)
        moreover from length xvec = length Tvec distinct xvec set xvec  supp N x  N[xvec::=Tvec] have "x  Tvec"
          by(rule substTerm.subst3)
        with x  xvec have "(Ψ, (⦇νxP)[xvec::=Tvec], ⦇νx(P[xvec::=Tvec]))  Rel"
          by(force intro: C1)
        ultimately show ?case by blast
      qed
    next
      case cOpen
      then have False by auto
      thus ?case by simp
    qed
  qed
qed

lemma outputPushResLeft:
  fixes Ψ   :: 'b
  and   x    :: name
  and   M    :: 'a
  and   N    :: 'a
  and   P    :: "('a, 'b, 'c) psi"

  assumes "eqvt Rel"
  and     "x  Ψ"
  and     "x  M"
  and     "x  N"
  and     C1: "Q. (Ψ, Q, Q)  Rel"

  shows "Ψ  ⦇νx(MN⟩.P) ↝[Rel] MN⟩.⦇νxP"
proof -
  note eqvt Rel x  Ψ
  moreover have "x  ⦇νx(MN⟩.P)" by(simp add: abs_fresh)
  moreover from x  M x  N have "x  MN⟩.⦇νxP"
    by(auto simp add: abs_fresh)
  ultimately show ?thesis
  proof(induct rule: simIFresh[of _ _ _ _ _ "()"])
    case(cSim α P')
    from Ψ  MN⟩.⦇νxP α  P' x  α
    show ?case
    proof(induct rule: outputCases)
      case(cOutput K)
      from Ψ  M  K have "Ψ  MN⟩.P KN  P"
        by(rule Output)
      hence "Ψ  ⦇νx(MN⟩.P) KN  ⦇νxP" using x  Ψ x  KN
        by(rule Scope)
      moreover have "(Ψ, ⦇νxP, ⦇νxP)  Rel" by(rule C1)
      ultimately show ?case by blast
    qed
  qed
qed
 
lemma outputPushResRight:
  fixes Ψ   :: 'b
  and   x    :: name
  and   M    :: 'a
  and   N    :: 'a
  and   P    :: "('a, 'b, 'c) psi"

  assumes "eqvt Rel"
  and     "x  Ψ"
  and     "x  M"
  and     "x  N"
  and     C1: "Q. (Ψ, Q, Q)  Rel"

  shows "Ψ  MN⟩.⦇νxP ↝[Rel] ⦇νx(MN⟩.P)"
proof -
  note eqvt Rel x  Ψ
  moreover from x  M x  N have "x  MN⟩.⦇νxP"
    by(auto simp add: abs_fresh)
  moreover have "x  ⦇νx(MN⟩.P)" by(simp add: abs_fresh)
  ultimately show ?thesis
  proof(induct rule: simIFresh[of _ _ _ _ _ "(M, N)"])
    case(cSim α P')
    note Ψ  ⦇νx(MN⟩.P) α  P' x  Ψ x  α x  P' bn α ♯* Ψ
    moreover from bn α ♯* (⦇νx(MN⟩.P)) x  α have "bn α ♯* (MN⟩.P)" by simp
    ultimately show ?case using bn α ♯* subject α bn α ♯* (M, N) x  α
    proof(induct rule: resCases)
      case(cOpen K xvec1 xvec2 y N' P')
      from bn(K⦇ν*(xvec1@y#xvec2)⦈⟨N') ♯* (M, N) have "y  N" by simp+
      from Ψ  MN⟩.P K⦇ν*(xvec1@xvec2)⦈⟨([(x, y)]  N')  ([(x, y)]  P')
      have "N = ([(x, y)]  N')"
        apply -
        by(ind_cases "Ψ  MN⟩.P K⦇ν*(xvec1@xvec2)⦈⟨([(x, y)]  N')  ([(x, y)]  P')")
          (auto simp add: residualInject psi.inject)
      with x  N y  N x  y have "N = N'"
        by(subst pt_bij[OF pt_name_inst, OF at_name_inst, symmetric, where pi="[(x, y)]"])
          (simp add: fresh_left calc_atm)
      with y  supp N' y  N have False by(simp add: fresh_def)
      thus ?case by simp
    next
      case(cRes P')
      from Ψ  MN⟩.P α  P' show ?case
      proof(induct rule: outputCases)
        case(cOutput K)
        from Ψ  M  K have "Ψ  MN⟩.(⦇νxP) KN  ⦇νxP"
          by(rule Output)
        moreover have "(Ψ, ⦇νxP, ⦇νxP)  Rel" by(rule C1)
        ultimately show ?case by force
      qed
    qed
  qed
qed

lemma casePushResLeft:
  fixes Ψ  :: 'b
  and   x  :: name
  and   Cs :: "('c × ('a, 'b, 'c) psi) list"

  assumes "eqvt Rel"
  and     "x  Ψ"
  and     "x  map fst Cs"
  and     C1: "Q. (Ψ, Q, Q)  Rel"

  shows "Ψ  ⦇νx(Cases Cs) ↝[Rel] Cases (map (λ(φ, P). (φ, ⦇νxP)) Cs)"
proof -
  note eqvt Rel x  Ψ
  moreover have "x  ⦇νx(Cases Cs)" by(simp add: abs_fresh)
  moreover from x  map fst Cs have "x  Cases (map (λ(φ, P). (φ, ⦇νxP)) Cs)"
    by(induct Cs) (auto simp add: abs_fresh)
  ultimately show ?thesis
  proof(induct rule: simIFresh[of _ _ _ _ _ Cs])
    case(cSim α P'')
    from Ψ  Cases (map (λ(φ, P). (φ, ⦇νxP)) Cs) α  P'' 
    show ?case
    proof(induct rule: caseCases)
      case(cCase φ P')
      from (φ, P') mem (map (λ(φ, P). (φ, ⦇νxP)) Cs) 
      obtain P where "(φ, P) mem Cs" and "P' = ⦇νxP" 
        by(induct Cs) auto
      from guarded P' P' = ⦇νxP have "guarded P" by simp
      from Ψ  P' α  P'' P' = ⦇νxP have "Ψ  ⦇νxP α  P''"
        by simp
      moreover note x  Ψ x  α x  P'' bn α ♯* Ψ 
      moreover from bn α ♯* Cs (φ, P) mem Cs
      have "bn α ♯* P" by(auto dest: memFreshChain)
      ultimately show ?case using bn α ♯* subject α x  α bn α ♯* Cs
      proof(induct rule: resCases)
        case(cOpen M xvec1 xvec2 y N P')
        from x  M⦇ν*(xvec1@y#xvec2)⦈⟨N have "x  xvec1" and "x  xvec2" and "x  M" by simp+
        from bn(M⦇ν*(xvec1@y#xvec2)⦈⟨N) ♯* Cs have "y  Cs" by simp
        from Ψ  P M⦇ν*(xvec1@xvec2)⦈⟨([(x, y)]  N)  ([(x, y)]  P') (φ, P) mem Cs Ψ  φ guarded P
        have "Ψ  Cases Cs M⦇ν*(xvec1@xvec2)⦈⟨([(x, y)]  N)  ([(x, y)]  P')" by(rule Case)
        hence "([(x, y)]  Ψ)  ([(x, y)]  (Cases Cs))  ([(x, y)]  (M⦇ν*(xvec1@xvec2)⦈⟨([(x, y)]  N)  ([(x, y)]  P')))"
          by(rule semantics.eqvt)
        with x  Ψ x  M y  xvec1 y  xvec2 y  Ψ y  M x  xvec1 x  xvec2
        have "Ψ  ([(x, y)]  (Cases Cs))  M⦇ν*(xvec1@xvec2)⦈⟨N  P'" by(simp add: eqvts)
        hence "Ψ  ⦇νy([(x, y)]  (Cases Cs))  M⦇ν*(xvec1@y#xvec2)⦈⟨N  P'" using y  supp N y  Ψ y  M y  xvec1 y  xvec2
          by(rule Open)
        hence "Ψ  ⦇νx(Cases Cs)  M⦇ν*(xvec1@y#xvec2)⦈⟨N  P'" using y  Cs
          by(simp add: alphaRes)
        moreover have "(Ψ, P', P')  Rel" by(rule C1)
        ultimately show ?case by blast
      next
        case(cRes P')
        from Ψ  P α  P' (φ, P) mem Cs Ψ  φ guarded P
        have "Ψ  Cases Cs α  P'" by(rule Case)
        hence "Ψ  ⦇νx(Cases Cs) α  ⦇νxP'" using x  Ψ x  α
          by(rule Scope)
        moreover have "(Ψ, ⦇νxP', ⦇νxP')  Rel" by(rule C1)
        ultimately show ?case by blast
      qed
    qed
  qed
qed
 
lemma casePushResRight:
  fixes Ψ  :: 'b
  and   x  :: name
  and   Cs :: "('c × ('a, 'b, 'c) psi) list"

  assumes "eqvt Rel"
  and     "x  Ψ"
  and     "x  map fst Cs"
  and     C1: "Q. (Ψ, Q, Q)  Rel"

  shows "Ψ  Cases (map (λ(φ, P). (φ, ⦇νxP)) Cs) ↝[Rel] ⦇νx(Cases Cs)"
proof -
  note eqvt Rel x  Ψ
  moreover from x  map fst Cs have "x  Cases (map (λ(φ, P). (φ, ⦇νxP)) Cs)"
    by(induct Cs) (auto simp add: abs_fresh)
  moreover have "x  ⦇νx(Cases Cs)" by(simp add: abs_fresh)
  ultimately show ?thesis
  proof(induct rule: simIFresh[of _ _ _ _ _ Cs])
    case(cSim α P'')
    note Ψ  ⦇νx(Cases Cs) α  P'' x  Ψ x  α x  P'' bn α ♯* Ψ
    moreover from bn α ♯* ⦇νx(Cases Cs) x  α have "bn α ♯* (Cases Cs)" by simp
    ultimately show ?case using bn α ♯* subject α x  α bn α ♯* Cs
    proof(induct rule: resCases)
      case(cOpen M xvec1 xvec2 y N P')
      from x  M⦇ν*(xvec1@y#xvec2)⦈⟨N have "x  xvec1" and "x  xvec2" and "x  M" by simp+
      from bn(M⦇ν*(xvec1@y#xvec2)⦈⟨N) ♯* Cs have "y  Cs" by simp
      from Ψ  Cases Cs M⦇ν*(xvec1@xvec2)⦈⟨([(x, y)]  N)  ([(x, y)]  P')
      show ?case
      proof(induct rule: caseCases)
        case(cCase φ P)
        from Ψ  P M⦇ν*(xvec1@xvec2)⦈⟨([(x, y)]  N)  ([(x, y)]  P')
        have "([(x, y)]  Ψ)  ([(x, y)]  P)  ([(x, y)]  (M⦇ν*(xvec1@xvec2)⦈⟨([(x, y)]  N)  ([(x, y)]  P')))"
          by(rule semantics.eqvt)
        with x  Ψ x  M y  xvec1 y  xvec2 y  Ψ y  M x  xvec1 x  xvec2
        have "Ψ  ([(x, y)]  P)  M⦇ν*(xvec1@xvec2)⦈⟨N  P'" by(simp add: eqvts)
        hence "Ψ  ⦇νy([(x, y)]  P)  M⦇ν*(xvec1@y#xvec2)⦈⟨N  P'" using y  supp N y  Ψ y  M y  xvec1 y  xvec2
          by(rule Open)
        hence "Ψ  ⦇νxP  M⦇ν*(xvec1@y#xvec2)⦈⟨N  P'" using y  Cs (φ, P) mem Cs
          by(subst alphaRes, auto dest: memFresh)
        moreover from (φ, P) mem Cs have "(φ, ⦇νxP) mem (map (λ(φ, P). (φ, ⦇νxP)) Cs)"
          by(induct Cs) auto
        moreover note Ψ  φ
        moreover from guarded P have "guarded(⦇νxP)" by simp
        ultimately have "Ψ  (Cases (map (λ(φ, P). (φ, ⦇νxP)) Cs)) M⦇ν*(xvec1@y#xvec2)⦈⟨N  P'"
          by(rule Case)
        moreover have "(Ψ, P', P')  Rel" by(rule C1)
        ultimately show ?case by blast
      qed
    next
      case(cRes P')
      from Ψ  Cases Cs α  P'
      show ?case
      proof(induct rule: caseCases)
        case(cCase φ P)
        from Ψ  P α  P' x  Ψ x  α
        have "Ψ  ⦇νxP α  ⦇νxP'" by(rule Scope)
        moreover from (φ, P) mem Cs have "(φ, ⦇νxP) mem (map (λ(φ, P). (φ, ⦇νxP)) Cs)"
          by(induct Cs) auto
        moreover note Ψ  φ
        moreover from guarded P have "guarded(⦇νxP)" by simp
        ultimately have "Ψ  (Cases (map (λ(φ, P). (φ, ⦇νxP)) Cs)) α  ⦇νxP'"
          by(rule Case)
        moreover have "(Ψ, ⦇νxP', ⦇νxP')  Rel" by(rule C1)
        ultimately show ?case by blast
      qed
    qed
  qed
qed

lemma resInputCases[consumes 5, case_names cRes]:
  fixes Ψ    :: 'b
  and   x    :: name
  and   P    :: "('a, 'b, 'c) psi"
  and   M    :: 'a
  and   N    :: 'a
  and   P'   :: "('a, 'b, 'c) psi"
  and   C    :: "'d::fs_name"

  assumes Trans: "Ψ  ⦇νxP MN  P'"
  and     "x  Ψ"
  and     "x  M"
  and     "x  N"
  and     "x  P'"
  and     rScope:  "P'.