Theory Tau

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

locale tau = env +
  fixes nameTerm :: "name ⇒ 'a"

  assumes ntEqvt[eqvt]: "(p::name prm) ∙ (nameTerm x) = nameTerm(p ∙ x)"
  and     ntSupp: "supp(nameTerm x) = {x}"
  and     ntEq: "Ψ ⊢ (nameTerm x) ↔ M = (M = nameTerm x)"
  and     subst4: "⟦length xvec = length Tvec; distinct xvec; xvec ♯* (M::'a)⟧ ⟹ M[xvec::=Tvec] = M"
begin

lemma ntChanEq[simp]:
  fixes Ψ :: 'b
  and   x :: name

  shows "Ψ ⊢ (nameTerm x) ↔ (nameTerm x)"
using ntEq
by auto

lemma nameTermFresh[simp]:
  fixes x :: name
  and   y :: name
  
  shows "x ♯ (nameTerm y) = (x ≠ y)"
using ntSupp
by(auto simp add: fresh_def)

lemma nameTermFreshChain[simp]:
  fixes xvec :: "name list"
  and   x    :: name

  shows "xvec ♯* (nameTerm x) = x ♯ xvec"
by(induct xvec) auto

definition tauPrefix :: "('a, 'b, 'c) psi ⇒ ('a, 'b, 'c) psi" (‹τ._› [85] 85)
  where "tauPrefix P ≡ THE P'. ∃x::name. x ♯ P ∧ P' = ⦇νx⦈(((nameTerm x)⦇λ*([]) (nameTerm x)⦈.𝟬) ∥ ((nameTerm x)⟨(nameTerm x)⟩.P))"

lemma tauActionUnfold:
  fixes P :: "('a, 'b, 'c) psi"
  and   C :: "'d::fs_name"

  obtains x::name where "x ♯ P" and "x ♯ C" and "τ.(P) = ⦇νx⦈(((nameTerm x)⦇λ*([]) (nameTerm x)⦈.𝟬) ∥ ((nameTerm x)⟨(nameTerm x)⟩.P))"
proof -
  obtain x::name where "x ♯ P" and "x ♯ C" by(generate_fresh "name") auto
  hence "∃x::name. x ♯ P ∧ x ♯ C ∧ τ.(P) = ⦇νx⦈(((nameTerm x)⦇λ*([]) (nameTerm x)⦈.𝟬) ∥ ((nameTerm x)⟨(nameTerm x)⟩.P))"
    apply(simp add: tauPrefix_def)
    apply(subst the_equality)
    apply(rule_tac x=x in exI)
    apply simp
    apply(clarify)
    apply(simp add: psi.inject alpha)
    by(auto simp add: calc_atm eqvts abs_fresh)
  moreover assume "⋀x. ⟦x ♯ P; x ♯ C;
          τ.(P) =
          ⦇νx⦈((nameTerm x⦇λ*[] nameTerm x⦈.𝟬) ∥ nameTerm x⟨nameTerm x⟩.P)⟧
         ⟹ thesis"
  ultimately show ?thesis by blast
qed

lemma tauActionI:
  fixes P :: "('a, 'b, 'c) psi"

  shows "∃P'. Ψ ⊳ τ.(P) ⟼τ ≺ P' ∧ Ψ ⊳ P ∼ P'"
proof -
  obtain x:: name where "x ♯ Ψ" and "x ♯ P" and "τ.(P) = ⦇νx⦈(((nameTerm x)⦇λ*([]) (nameTerm x)⦈.𝟬) ∥ ((nameTerm x)⟨(nameTerm x)⟩.P))"
    by(rule tauActionUnfold)
  
  then have "Ψ ⊳ τ.(P) ⟼τ ≺ ⦇νx⦈(𝟬 ∥ P)"
    apply simp
    apply(rule Scope)
    apply auto
    apply(subgoal_tac "Ψ ⊳ ((nameTerm x)⦇λ*([]) (nameTerm x)⦈.𝟬) ∥ ((nameTerm x)⟨(nameTerm x)⟩.P) ⟼τ ≺ ⦇ν*[]⦈(𝟬 ∥ P)")
    apply simp
    apply(rule_tac M="(nameTerm x)" and N="(nameTerm x)" and K="(nameTerm x)" in Comm1)
    apply(auto intro: ntChanEq Output Input)
    apply(subgoal_tac "Ψ ⊗ 𝟭 ⊳ (nameTerm x)⦇λ*([]) (nameTerm x)⦈.𝟬 ⟼(nameTerm x)⦇((nameTerm x)[([])::=[]])⦈ ≺ (𝟬[[]::=[]])")
    apply(simp add: subst4)
    by(rule_tac Input) auto
  moreover from ‹x ♯ Ψ› ‹x ♯ P› have "Ψ ⊳ P ∼ ⦇νx⦈(𝟬 ∥ P)"
    by(metis bisimTransitive bisimParNil bisimScopeExtSym bisimResNil bisimParPresSym bisimParComm bisimE(4))
  ultimately show ?thesis by blast
qed

lemma outputEmpy[dest]:
  assumes "Ψ ⊳ M⟨N⟩.P ⟼K⦇ν*xvec⦈⟨N'⟩ ≺ P'"

  shows "xvec = []"
using assms
apply -
by(ind_cases "Ψ ⊳ M⟨N⟩.P ⟼K⦇ν*xvec⦈⟨N'⟩ ≺ P'") (auto simp add: psi.inject residualInject)

lemma tauActionE:
  fixes P :: "('a, 'b, 'c) psi"

  assumes "Ψ ⊳ τ.(P) ⟼τ ≺ P'"

  shows "Ψ ⊳ P ∼ P'" and "supp P' = ((supp P)::name set)"
proof -
  obtain x:: name where "x ♯ (Ψ, P')" and "x ♯ P" and "τ.(P) = ⦇νx⦈(((nameTerm x)⦇λ*([]) (nameTerm x)⦈.𝟬) ∥ ((nameTerm x)⟨(nameTerm x)⟩.P))"
    by(rule tauActionUnfold)
  with assms have "Ψ ⊳ P ∼ P' ∧ supp P' = ((supp P)::name set)"
    apply simp
    apply(erule_tac resTauCases)
    apply simp+
    apply(erule_tac C="x" in parCases)
    apply simp+
    apply(drule_tac nilTrans(3)[where xvec="[]", simplified])
    apply simp
    apply force
    apply simp
    apply(subgoal_tac "Ψ ⊗ 𝟭 ⊳ (nameTerm x)⦇λ*[] (nameTerm x)⦈.𝟬 ⟼M⦇N⦈ ≺ P'a")
    apply(erule_tac inputCases)
    apply simp
    apply(subgoal_tac "xvec = []")
    apply(erule_tac outputCases)
    apply simp
    apply(clarsimp)
    apply(rule conjI)
    apply(metis bisimTransitive bisimParNil bisimScopeExtSym bisimResNil bisimParPresSym bisimParComm bisimE(4))
    apply(auto simp add: psi.supp abs_supp suppBottom)
    by(simp add: fresh_def)
  thus "Ψ ⊳ P ∼ P'" and "supp P' = ((supp P)::name set)"
    by auto
qed

lemma tauActionEqvt[eqvt]:
  fixes P :: "('a, 'b, 'c) psi"
  and   p :: "name prm"

  shows "(p ∙ τ.(P)) = τ.(p ∙ P)"
proof -
  obtain x::name where "x ♯ P" and "x ♯ p" and "τ.(P) = ⦇νx⦈(((nameTerm x)⦇λ*([]) (nameTerm x)⦈.𝟬) ∥ ((nameTerm x)⟨(nameTerm x)⟩.P))"
    by(rule tauActionUnfold)
  moreover obtain y::name where "y ♯ p ∙ P" and "y ♯ (p, x)" and "τ.(p ∙ P) = ⦇νy⦈(((nameTerm y)⦇λ*([]) (nameTerm y)⦈.𝟬) ∥ ((nameTerm y)⟨(nameTerm y)⟩.(p ∙ P)))"
    by(rule tauActionUnfold)
  ultimately show ?thesis
    by(simp add: eqvts calc_atm at_prm_fresh[OF at_name_inst] psi.inject alpha pt_fresh_perm_app[OF pt_name_inst, OF at_name_inst])
qed

lemma resCases'[consumes 7, case_names cOpen cRes]:
  fixes Ψ    :: 'b
  and   x    :: name
  and   P    :: "('a, 'b, 'c) psi"
  and   α    :: "'a action"
  and   P'   :: "('a, 'b, 'c) psi"
  and   C    :: "'d::fs_name"

  assumes Trans: "Ψ ⊳ ⦇νx⦈P ⟼xα ≺ xP'"
  and     "x ♯ Ψ"
  and     "x ♯ xα"
  and     "x ♯ xP'"
  and     "bn xα ♯* Ψ"
  and     "bn xα ♯* P"
  and     "bn xα ♯* subject xα"
  and     rOpen: "⋀M xvec yvec y N P'. ⟦Ψ ⊳ P ⟼M⦇ν*(xvec@yvec)⦈⟨([(x, y)] ∙ N)⟩ ≺ ([(x, y)] ∙ P'); y ∈ supp N;
                                         x ♯ N; x ♯ P'; x ≠ y; y ♯ xvec; y ♯ yvec; y ♯ M; distinct xvec; distinct yvec;
                                         xvec ♯* Ψ; y ♯ Ψ; yvec ♯* Ψ; xvec ♯* P; y ♯ P; yvec ♯* P; xvec ♯* M; y ♯ M;
                                         yvec ♯* M; xvec ♯* yvec; xα = M⦇ν*(xvec@y#yvec)⦈⟨N⟩; xP' = P'⟧ ⟹
                                         Prop"
  and     rScope:  "⋀P'. ⟦Ψ ⊳ P ⟼xα ≺ P'; xP' = ⦇νx⦈P'⟧ ⟹ Prop"

  shows "Prop"
proof -
  from Trans have "distinct(bn xα)" by(auto dest: boundOutputDistinct)
  have "length(bn xα) = residualLength(xα ≺ xP')" by simp
  note Trans
  moreover have "length [] = inputLength(⦇νx⦈P)" and "distinct []"
    by(auto simp add: inputLength_inputLength'_inputLength''.simps)
  moreover note ‹length(bn xα) = residualLength(xα ≺ xP')› ‹distinct(bn xα)›
  moreover note ‹length(bn xα) = residualLength(xα ≺ xP')› ‹distinct(bn xα)›
  moreover note ‹length(bn xα) = residualLength(xα ≺ xP')› ‹distinct(bn xα)›
  moreover note ‹length(bn xα) = residualLength(xα ≺ xP')› ‹distinct(bn xα)›
  ultimately show ?thesis using ‹bn xα ♯* Ψ› ‹bn xα ♯* P› ‹bn xα ♯* subject xα› ‹x ♯ Ψ› ‹x ♯ xα› ‹x ♯ xP'› ‹distinct(bn xα)› rScope rOpen
    apply(cases rule: semanticsCases[of _ _ _ _ _ _ _ _ _ _ x x]) 
    apply(auto simp add: psi.inject alpha abs_fresh residualInject boundOutputApp boundOutput.inject eqvts)
    apply(subgoal_tac "y ∈ supp Na")
    apply(auto simp add: residualInject boundOutputApp)
    apply(drule_tac pi="[(x, y)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
    by(simp add: calc_atm eqvts)
qed

lemma parCases'[consumes 5, case_names cPar1 cPar2 cComm1 cComm2]:
  fixes Ψ    :: 'b
  and   P    :: "('a, 'b, 'c) psi"
  and   Q    :: "('a, 'b, 'c) psi"
  and   α    :: "'a action"
  and   T    :: "('a, 'b, 'c) psi"
  and   C    :: "'d::fs_name"

  assumes Trans: "Ψ ⊳ P ∥ Q ⟼xα ≺ xT"
  and     "bn xα ♯* Ψ"
  and     "bn xα ♯* P"
  and     "bn xα ♯* Q"
  and     "bn xα ♯* subject xα"
  and     rPar1: "⋀P' A⇩Q Ψ⇩Q. ⟦Ψ ⊗ Ψ⇩Q ⊳ P ⟼xα ≺ P';  extractFrame Q = ⟨A⇩Q, Ψ⇩Q⟩; distinct A⇩Q;
                                  A⇩Q ♯* Ψ; A⇩Q ♯* P; A⇩Q ♯* Q; A⇩Q ♯* xα; A⇩Q ♯* P'; A⇩Q ♯* C; xT = P' ∥ Q⟧ ⟹ Prop"
  and     rPar2: "⋀Q' A⇩P Ψ⇩P. ⟦Ψ ⊗ Ψ⇩P ⊳ Q ⟼xα ≺ Q';  extractFrame P = ⟨A⇩P, Ψ⇩P⟩; distinct A⇩P;
                                 A⇩P ♯* Ψ; A⇩P ♯* P; A⇩P ♯* Q; A⇩P ♯* xα; A⇩P ♯* Q'; A⇩P ♯* C; xT = P ∥ Q'⟧ ⟹ Prop"
  and     rComm1: "⋀Ψ⇩Q M N P' A⇩P Ψ⇩P K xvec Q' A⇩Q.
           ⟦Ψ ⊗ Ψ⇩Q ⊳ P ⟼M⦇N⦈ ≺ P'; extractFrame P = ⟨A⇩P, Ψ⇩P⟩; distinct A⇩P;
            Ψ ⊗ Ψ⇩P ⊳ Q ⟼K⦇ν*xvec⦈⟨N⟩ ≺ Q'; extractFrame Q = ⟨A⇩Q, Ψ⇩Q⟩; distinct A⇩Q;
            Ψ ⊗ Ψ⇩P ⊗ Ψ⇩Q ⊢ M ↔ K; distinct xvec;
            A⇩P ♯* Ψ;  A⇩P ♯* Ψ⇩Q;  A⇩P ♯* P;  A⇩P ♯* M;  A⇩P ♯* N;  A⇩P ♯* P';  A⇩P ♯* Q;  A⇩P ♯* xvec;  A⇩P ♯* Q'; A⇩P ♯* A⇩Q;  A⇩P ♯* C; 
            A⇩Q ♯* Ψ;  A⇩Q ♯* Ψ⇩P; A⇩Q ♯* P;  A⇩Q ♯* K;  A⇩Q ♯* N;  A⇩Q ♯* P';  A⇩Q ♯* Q;  A⇩Q ♯* xvec;  A⇩Q ♯* Q'; A⇩Q ♯* C; 
            xvec ♯* Ψ;  xvec ♯* Ψ⇩P; xvec ♯* P;  xvec ♯* M;  xvec ♯* K; xvec ♯* Q;  xvec ♯* Ψ⇩Q;  xvec ♯* C; xα=τ; xT = ⦇ν*xvec⦈(P' ∥ Q')⟧ ⟹ Prop"
  and     rComm2: "⋀Ψ⇩Q M xvec N P' A⇩P Ψ⇩P K Q' A⇩Q.
           ⟦Ψ ⊗ Ψ⇩Q ⊳ P ⟼M⦇ν*xvec⦈⟨N⟩ ≺ P'; extractFrame P = ⟨A⇩P, Ψ⇩P⟩; distinct A⇩P;
            Ψ ⊗ Ψ⇩P ⊳ Q ⟼K⦇N⦈ ≺ Q'; extractFrame Q = ⟨A⇩Q, Ψ⇩Q⟩; distinct A⇩Q;
            Ψ ⊗ Ψ⇩P ⊗ Ψ⇩Q ⊢ M ↔ K; distinct xvec;
            A⇩P ♯* Ψ;  A⇩P ♯* Ψ⇩Q;  A⇩P ♯* P;  A⇩P ♯* M;  A⇩P ♯* N;  A⇩P ♯* P';  A⇩P ♯* Q;  A⇩P ♯* xvec;  A⇩P ♯* Q'; A⇩P ♯* A⇩Q;  A⇩P ♯* C; 
            A⇩Q ♯* Ψ;  A⇩Q ♯* Ψ⇩P; A⇩Q ♯* P;  A⇩Q ♯* K;  A⇩Q ♯* N;  A⇩Q ♯* P';  A⇩Q ♯* Q;  A⇩Q ♯* xvec;  A⇩Q ♯* Q'; A⇩Q ♯* C; 
            xvec ♯* Ψ;  xvec ♯* Ψ⇩P; xvec ♯* P;  xvec ♯* M;  xvec ♯* K;  xvec ♯* Q;  xvec ♯* Ψ⇩Q;  xvec ♯* C; xα=τ; xT = ⦇ν*xvec⦈(P' ∥ Q')⟧ ⟹ Prop"

  shows "Prop"
proof -
  from Trans have "distinct(bn xα)" by(auto dest: boundOutputDistinct)
  have "length(bn xα) = residualLength(xα ≺ xT)" by simp
  note Trans
  moreover have "length [] = inputLength(P ∥ Q)" and "distinct []"
    by(auto simp add: inputLength_inputLength'_inputLength''.simps)
  moreover note ‹length(bn xα) = residualLength(xα ≺ xT)› ‹distinct(bn xα)›
  moreover note ‹length(bn xα) = residualLength(xα ≺ xT)› ‹distinct(bn xα)›
  moreover note ‹length(bn xα) = residualLength(xα ≺ xT)› ‹distinct(bn xα)›
  moreover note ‹length(bn xα) = residualLength(xα ≺ xT)› ‹distinct(bn xα)›
  moreover obtain x::name where "x ♯ Ψ" and "x ♯ P" and "x ♯ Q" and "x ♯ xα" and "x ♯ xT"
    by(generate_fresh "name") auto
  ultimately show ?thesis using ‹bn xα ♯* Ψ› ‹bn xα ♯* P› ‹bn xα ♯* Q› ‹bn xα ♯* subject xα› using rPar1 rPar2 rComm1 rComm2
    by(cases rule: semanticsCases[of _ _ _ _ _ _ _ _ _ C x x]) (auto simp add: psi.inject residualInject residualInject')
qed

lemma inputCases'[consumes 1, case_names cInput]:
  fixes Ψ   :: 'b
  and   M    :: 'a
  and   xvec :: "name list"
  and   N    :: 'a
  and   P    :: "('a, 'b, 'c) psi"  
  and   α    :: "'a action"
  and   P'   :: "('a, 'b, 'c) psi"
  
  assumes Trans: "Ψ ⊳ M⦇λ*xvec N⦈.P ⟼α ≺ P'"  
  and     rInput: "⋀K Tvec. ⟦Ψ ⊢ M ↔ K; set xvec ⊆ supp N; length xvec = length Tvec; distinct xvec; α=K⦇N[xvec::=Tvec]⦈; P' = P[xvec::=Tvec]⟧ ⟹ Prop (K⦇N[xvec::=Tvec]⦈) (P[xvec::=Tvec])"

  shows "Prop α P'"
proof -
  {
    fix xvec N P
    assume Trans: "Ψ ⊳ M⦇λ*xvec N⦈.P ⟼α ≺ P'"
       and "xvec ♯* Ψ" and "xvec ♯* M" and "xvec ♯* α" and "xvec ♯* P'" and "distinct xvec"
       and rInput: "⋀K Tvec. ⟦Ψ ⊢ M ↔ K; set xvec ⊆ supp N; length xvec = length Tvec; distinct xvec; α=K⦇N[xvec::=Tvec]⦈; P'=P[xvec::=Tvec]⟧ ⟹ Prop (K⦇N[xvec::=Tvec]⦈) (P[xvec::=Tvec])"

    from Trans have "bn α = []"
      apply -
      by(ind_cases "Ψ ⊳ M⦇λ*xvec N⦈.P ⟼α ≺ P'") (auto simp add: residualInject)
    from Trans have "distinct(bn α)" by(auto dest: boundOutputDistinct)
    have "length(bn α) = residualLength(α ≺ P')" by simp
    note Trans
    moreover have "length xvec = inputLength(M⦇λ*xvec N⦈.P)" by auto
    moreover note ‹distinct xvec›
    moreover note ‹length(bn α) = residualLength(α ≺ P')› ‹distinct(bn α)›
    moreover note ‹length(bn α) = residualLength(α ≺ P')› ‹distinct(bn α)›
    moreover note ‹length(bn α) = residualLength(α ≺ P')› ‹distinct(bn α)›
    moreover note ‹length(bn α) = residualLength(α ≺ P')› ‹distinct(bn α)›
    moreover note ‹length(bn α) = residualLength(α ≺ P')› ‹distinct(bn α)›
    moreover obtain x::name where "x ♯ Ψ" and "x ♯ P" and "x ♯ M" and "x ♯ xvec" and "x ♯ α" and "x ♯ P'" and "x ♯ N"
      by(generate_fresh "name") auto
    ultimately have "Prop α P'" using ‹bn α = []› ‹xvec ♯* Ψ›‹xvec ♯* M› ‹xvec ♯* α› ‹xvec ♯* P'› rInput
      apply(cases rule: semanticsCases[of _ _ _ _ _ _ _ _ _ C x])  
      by(fastforce simp add: residualInject psi.inject inputChainFresh)+
  }
  note Goal = this
  moreover obtain p :: "name prm" where "(p ∙ xvec) ♯* Ψ" and "(p ∙ xvec) ♯* M" and "(p ∙ xvec) ♯* N" and "(p ∙ xvec) ♯* P"
                                    and "(p ∙ xvec) ♯* α" and "(p ∙ xvec) ♯* P'" and S: "set p ⊆ set xvec × set(p ∙ xvec)"
                                    and "distinctPerm p"
    by(rule_tac xvec=xvec and c="(Ψ, M, N, P, α, P')" in name_list_avoiding) auto
  from Trans ‹(p ∙ xvec) ♯* N› ‹(p ∙ xvec) ♯* P› S have "Ψ ⊳ M⦇λ*(p ∙ xvec) (p ∙ N)⦈.(p ∙ P) ⟼α ≺ P'"
    by(simp add: inputChainAlpha')
  moreover {
    fix K Tvec
    assume "Ψ ⊢ M ↔ K"
    moreover assume "set(p ∙ xvec) ⊆ supp(p ∙ N)"
    hence "(p ∙ set(p ∙ xvec)) ⊆ (p ∙ supp(p ∙ N))" by simp
    with ‹distinctPerm p› have "set xvec ⊆ supp N" by(simp add: eqvts)
    moreover assume "length(p ∙ xvec) = length(Tvec::'a list)"
    hence "length xvec = length Tvec" by simp
    moreover assume "distinct xvec"
    moreover assume "α=K⦇(p ∙ N)[(p ∙ xvec)::=Tvec]⦈" and "P' = (p ∙ P)[(p ∙ xvec)::=Tvec]"
    with ‹(p ∙ xvec) ♯* P› ‹(p ∙ xvec) ♯* N› ‹distinctPerm p› ‹length xvec = length Tvec› S
    have "α=K⦇(N[xvec::=Tvec])⦈" and "P' = P[xvec::=Tvec]"
      by(simp add: renaming substTerm.renaming)+
    ultimately have "Prop (K⦇N[xvec::=Tvec]⦈) (P[xvec::=Tvec])" 
      by(rule rInput)
    with ‹length xvec = length Tvec› S ‹distinctPerm p› ‹(p ∙ xvec) ♯* N› ‹(p ∙ xvec) ♯* P›
    have "Prop (K⦇(p ∙ N)[(p ∙ xvec)::=Tvec]⦈) ((p ∙ P)[(p ∙ xvec)::=Tvec])"
      by(simp add: renaming substTerm.renaming)
  }
  moreover from Trans have "distinct xvec" by(rule inputDistinct)
  hence "distinct(p ∙ xvec)" by simp
  ultimately show ?thesis using ‹(p ∙ xvec) ♯* Ψ› ‹(p ∙ xvec) ♯* M› ‹(p ∙ xvec) ♯* α› ‹(p ∙ xvec) ♯* P'› ‹distinct xvec›
    by(rule_tac Goal) assumption+
qed

lemma outputCases'[consumes 1, case_names cOutput]:
  fixes Ψ :: 'b
  and   M  :: 'a
  and   N  :: 'a
  and   P  :: "('a, 'b, 'c) psi"  
  and   α  :: "'a action"
  and   P' :: "('a, 'b, 'c) psi"
  
  assumes "Ψ ⊳ M⟨N⟩.P ⟼α ≺ P'"
  and     "⋀K. ⟦Ψ ⊢ M ↔ K; subject α=Some K⟧ ⟹ Prop (K⟨N⟩) P"

  shows "Prop α P'"
using assms
by(cases rule: semantics.cases) (auto simp add: residualInject psi.inject)

lemma tauOutput[dest]:
  fixes Ψ   :: 'b
  and   P    :: "('a, 'b, 'c) psi"
  and   M    :: 'a
  and   xvec :: "name list"
  and   N    :: 'a
  and   P'   :: "('a, 'b, 'c) psi"

  assumes "Ψ ⊳ τ.(P) ⟼M⦇ν*xvec⦈⟨N⟩ ≺ P'"
  
  shows False
proof -
  {
    fix xvec N P'

    assume "Ψ ⊳ τ.(P) ⟼M⦇ν*xvec⦈⟨N⟩ ≺ P'"
    and    "xvec ♯* Ψ"
    and    "xvec ♯* P"
    and    "xvec ♯* M"

    moreover obtain x:: name where "x ♯ Ψ" and "x ♯ P" and "x ♯ xvec" and "x ♯ M" and "x ♯ N" and "x ♯ P'"
                               and "τ.(P) = ⦇νx⦈(((nameTerm x)⦇λ*([]) (nameTerm x)⦈.𝟬) ∥ ((nameTerm x)⟨(nameTerm x)⟩.P))"
      by(rule_tac C="(Ψ, M, xvec, N, P')" in tauActionUnfold) auto
    ultimately have False
      apply simp
      apply(erule_tac resCases')
      apply simp+
      apply(erule_tac parOutputCases)
      apply(simp add: action.inject psi.inject)+
      apply(drule_tac nilTrans(2)[where xvec="[]", simplified])
      apply simp+
      apply(simp add: action.inject)
      apply(clarify)
      apply(erule outputCases')
      apply(auto simp add: ntEq)
      apply(erule_tac parCases')
      apply(auto simp add: abs_fresh)
      apply(drule_tac nilTrans(2)[where xvec="[]", simplified])
      apply simp
      apply(erule_tac outputCases')
      apply auto
      by(simp add: ntEq)
  }
  moreover obtain p where "set p ⊆ set xvec × set(p ∙ xvec)" and "(p ∙ xvec) ♯* N" and  "(p ∙ xvec) ♯* P'" 
                      and "(p ∙ xvec) ♯* Ψ" and "(p ∙ xvec) ♯* P" and "(p ∙ xvec) ♯* M"
    by(rule_tac c="(N, P', Ψ, P, M)" and xvec=xvec in name_list_avoiding) auto
    ultimately show False using assms by(simp add: boundOutputChainAlpha'' residualInject) auto
qed

lemma tauInput[dest]:
  fixes Ψ :: 'b
  and   P  :: "('a, 'b, 'c) psi"
  and   M  :: 'a
  and   N  :: 'a
  and   P' :: "('a, 'b, 'c) psi"

  assumes "Ψ ⊳ τ.(P) ⟼M⦇N⦈ ≺ P'"

  shows False
proof -
  obtain x:: name where "x ♯ Ψ" and "x ♯ P" and "x ♯ M" and "x ♯ N" and "x ♯ P'"
                    and "τ.(P) = ⦇νx⦈(((nameTerm x)⦇λ*([]) (nameTerm x)⦈.𝟬) ∥ ((nameTerm x)⟨(nameTerm x)⟩.P))"
    by(rule_tac C="(Ψ, M, N, P')" in tauActionUnfold) auto
  with assms show False
    apply simp
    apply(erule_tac resCases')
    apply auto
    apply(drule_tac  parCases')
    apply(auto simp add: abs_fresh)
    apply(subgoal_tac "Ψ ⊗ 𝟭 ⊳ (nameTerm x)⦇λ*[] (nameTerm x)⦈.𝟬 ⟼M⦇N⦈ ≺ P'a")
    apply(erule_tac inputCases')
    by(auto simp add: action.inject subst4)
qed

lemma tauPrefixFrame:
  fixes P :: "('a, 'b, 'c) psi"

  shows "extractFrame(τ.(P)) ≃⇩F ⟨ε, 𝟭⟩"
proof -
  obtain x:: name where "x ♯ P"
                    and "τ.(P) = ⦇νx⦈(((nameTerm x)⦇λ*([]) (nameTerm x)⦈.𝟬) ∥ ((nameTerm x)⟨(nameTerm x)⟩.P))"
    by(rule_tac C="()" in tauActionUnfold) auto
  thus ?thesis
    by(force intro: frameResFresh Identity FrameStatEqTrans)
qed

lemma insertTauAssertion:
  fixes P :: "('a, 'b, 'c) psi"
  and   Ψ :: 'b

  shows "insertAssertion (extractFrame(τ.(P))) Ψ ≃⇩F ⟨ε, Ψ⟩"
proof -
  obtain x:: name where "x ♯ P" and "x ♯ Ψ"
                    and "τ.(P) = ⦇νx⦈(((nameTerm x)⦇λ*([]) (nameTerm x)⦈.𝟬) ∥ ((nameTerm x)⟨(nameTerm x)⟩.P))"
    by(rule_tac C=Ψ in tauActionUnfold) auto
  thus ?thesis
    apply auto
    apply(rule_tac G="⟨ε, Ψ ⊗ 𝟭 ⊗ 𝟭⟩" in FrameStatEqTrans)
    apply(rule_tac frameResFresh) apply auto
    apply(subgoal_tac "x ♯ 𝟭 ⊗ 𝟭")
    apply auto
    by(metis Identity AssertionStatEqTrans AssertionStatEqSym Associativity)
qed

lemma seqSubst4:
  assumes "y ♯ σ"
  and     "wellFormedSubst σ"

  shows "substTerm.seqSubst (nameTerm y) σ = nameTerm y"
using assms
by(induct σ) (auto simp add: subst4)

lemma tauSeqSubst[simp]:
  fixes P :: "('a, 'b, 'c) psi"
  and   σ :: "(name list × 'a list) list"
  
  assumes "wellFormedSubst σ"

  shows "(τ.(P))[<σ>] = τ.(P[<σ>])"
proof -
  obtain x:: name where "x ♯ P[<σ>]" and "x ♯ σ" and "x ♯ P"
                    and "τ.(P[<σ>]) = ⦇νx⦈(((nameTerm x)⦇λ*([]) (nameTerm x)⦈.𝟬) ∥ ((nameTerm x)⟨(nameTerm x)⟩.(P[<σ>])))"
    by(rule_tac C="(σ, P)" in tauActionUnfold) auto
  moreover obtain y:: name where "y ♯ P[<σ>]" and "y ♯ σ" and "y ♯ P" and "x ≠ y"
                    and "τ.(P) = ⦇νy⦈(((nameTerm y)⦇λ*([]) (nameTerm y)⦈.𝟬) ∥ ((nameTerm y)⟨(nameTerm y)⟩.(P)))"
    by(rule_tac C="(σ, P[<σ>], x)" in tauActionUnfold) auto
  ultimately show ?thesis using assms
    by(auto simp add: psi.inject alpha eqvts calc_atm psi.inject input.inject seqSubst4)
qed

lemma tauSubst[simp]:
  fixes P    :: "('a, 'b, 'c) psi"
  and   xvec :: "name list"
  and   Tvec :: "'a list"
  
  assumes "distinct xvec"
  and     "length xvec = length Tvec"

  shows "(τ.(P))[xvec::=Tvec] = τ.(P[xvec::=Tvec])"
proof -
  obtain x:: name where "x ♯ P[xvec::=Tvec]" and "x ♯ xvec" and "x ♯ Tvec" and "x ♯ P"
                    and "τ.(P[xvec::=Tvec]) = ⦇νx⦈(((nameTerm x)⦇λ*([]) (nameTerm x)⦈.𝟬) ∥ ((nameTerm x)⟨(nameTerm x)⟩.(P[xvec::=Tvec])))"
    by(rule_tac C="(xvec, Tvec, P)" in tauActionUnfold) auto
  moreover obtain y:: name where "y ♯ P[xvec::=Tvec]" and "y ♯ xvec" and "y ♯ Tvec" and "y ♯ P" and "x ≠ y"
                    and "τ.(P) = ⦇νy⦈(((nameTerm y)⦇λ*([]) (nameTerm y)⦈.𝟬) ∥ ((nameTerm y)⟨(nameTerm y)⟩.(P)))"
    by(rule_tac C="(xvec, Tvec, P[xvec::=Tvec], x)" in tauActionUnfold) auto
  ultimately show ?thesis using assms
    by(auto simp add: psi.inject alpha eqvts calc_atm psi.inject input.inject subst4)
qed

lemma tauFresh[simp]:
  fixes P :: "('a, 'b, 'c) psi"
  and   x :: name

  shows "x ♯ τ.(P) = x ♯ P"
proof -
  obtain y::name where "y ≠ x" and "y ♯ P" and "τ.(P) = ⦇νy⦈(((nameTerm y)⦇λ*([]) (nameTerm y)⦈.𝟬) ∥ ((nameTerm y)⟨(nameTerm y)⟩.P))"
    by(rule_tac C=x in tauActionUnfold) auto

  thus ?thesis by(auto simp add: abs_fresh)
qed

lemma tauFreshChain[simp]:
  fixes P    :: "('a, 'b, 'c) psi"
  and   xvec :: "name list"

  shows "xvec ♯* (τ.(P)) = (xvec ♯* P)"
by(induct xvec) auto

lemma guardedTau:
  fixes P :: "('a, 'b, 'c) psi"

  shows "guarded(τ.(P))"
proof -
  obtain x::name where "x ♯ P" and "τ.(P) = ⦇νx⦈(((nameTerm x)⦇λ*([]) (nameTerm x)⦈.𝟬) ∥ ((nameTerm x)⟨(nameTerm x)⟩.P))"
    by(rule_tac C="()" in tauActionUnfold) auto

  thus ?thesis by auto
qed

lemma tauChainBisim:
  fixes Ψ  :: 'b
  and   P   :: "('a, 'b, 'c) psi"
  and   P'  :: "('a, 'b, 'c) psi"
  and   P'' :: "('a, 'b, 'c) psi"
  
  assumes "Ψ ⊳ P ⟹⇧^⇩τ P'"
  and     "Ψ ⊳ P ∼ P''"

  obtains P''' where "Ψ ⊳ P'' ⟹⇧^⇩τ P'''" and "Ψ ⊳ P' ∼ P'''"
using assms
proof(induct arbitrary: thesis rule: tauChainInduct)
  case(TauBase P)
  thus ?case by auto
next
  case(TauStep P P' P''')
  from ‹Ψ ⊳ P ∼ P''› obtain P'''' where P''Chain: "Ψ ⊳ P'' ⟹⇧^⇩τ P''''" and "Ψ ⊳ P' ∼ P''''"
    by(rule_tac TauStep) auto
  from ‹Ψ ⊳ P' ∼ P''''› ‹Ψ ⊳ P' ⟼τ ≺ P'''› 
  obtain P''''' where P''''Trans: "Ψ ⊳ P'''' ⟼τ ≺ P'''''" and "Ψ ⊳ P''' ∼ P'''''"
    apply(drule_tac bisimE(4))
    apply(drule_tac bisimE(2))
    apply(drule_tac simE)
    apply auto
    apply(drule_tac bisimE(4))
    by blast
  from P''Chain P''''Trans have "Ψ ⊳ P'' ⟹⇧^⇩τ P'''''" by(drule_tac tauActTauChain) auto
  with ‹Ψ ⊳ P''' ∼ P'''''› show ?case
    by(metis TauStep)
qed

lemma tauChainStepCons:
  fixes Ψ :: 'b
  and   P  :: "('a, 'b, 'c) psi"
  and   P' :: "('a, 'b, 'c) psi"
  
  assumes PChain: "Ψ ⊳ P ⟹⇧^⇩τ P'"

  obtains P'' where "Ψ ⊳ τ.(P) ⟹⇩τ P''" and "Ψ ⊳ P' ∼ P''"
proof -
  assume Goal: "⋀P''. ⟦Ψ ⊳ τ.(P) ⟹⇩τ P''; Ψ ⊳ P' ∼ P''⟧ ⟹ thesis"
  obtain P'' where PTrans: "Ψ ⊳ τ.(P) ⟼τ ≺ P''" and "Ψ ⊳ P ∼ P''" using tauActionI
    by auto
  from PChain ‹Ψ ⊳ P ∼ P''› obtain P''' where P''Chain: "Ψ ⊳ P'' ⟹⇧^⇩τ P'''" and "Ψ ⊳ P' ∼ P'''"
    by(rule tauChainBisim)
  from PTrans P''Chain have "Ψ ⊳ τ.(P) ⟹⇩τ P'''" by(drule_tac tauActTauStepChain) auto
  thus ?thesis using ‹Ψ ⊳ P' ∼ P'''›
    by(rule Goal)
qed

lemma tauChainCons:
  fixes Ψ :: 'b
  and   P  :: "('a, 'b, 'c) psi"
  and   P' :: "('a, 'b, 'c) psi"
  
  assumes "Ψ ⊳ P ⟹⇧^⇩τ P'"

  obtains P'' where "Ψ ⊳ τ.(P) ⟹⇧^⇩τ P''" and "Ψ ⊳ P' ∼ P''"
proof -
  assume Goal: "⋀P''. ⟦Ψ ⊳ τ.(P) ⟹⇧^⇩τ P''; Ψ ⊳ P' ∼ P''⟧ ⟹ thesis"  
  from assms obtain P'' where "Ψ ⊳ τ.(P) ⟹⇩τ P''" and "Ψ ⊳ P' ∼ P''"
    by(rule tauChainStepCons)
  thus ?thesis by(rule_tac Goal) auto
qed
  
lemma weakTransitionTau:
  fixes Ψ   :: 'b
  and   Q    :: "('a, 'b, 'c) psi"
  and   P    :: "('a, 'b, 'c) psi"
  and   α    :: "'a action"
  and   P'   :: "('a, 'b, 'c) psi"

  assumes PTrans: "Ψ : Q ⊳ P ⟹α ≺ P'"
  and     "bn α ♯* Ψ"
  and     "bn α ♯* P"

  obtains P'' where "Ψ : Q ⊳ τ.(P) ⟹α ≺ P''" and "Ψ ⊳ P' ∼ P''"
proof -
  assume Goal: "⋀P''. ⟦Ψ : Q ⊳ τ.(P) ⟹α ≺ P''; Ψ ⊳ P' ∼ P''⟧ ⟹ thesis"
  from PTrans obtain P'' where PChain: "Ψ ⊳ P ⟹⇧^⇩τ P''"
                           and QimpP'': "insertAssertion (extractFrame Q) Ψ ↪⇩F insertAssertion(extractFrame P'') Ψ"
                           and P''Trans: "Ψ ⊳ P'' ⟼α ≺ P'"
    by(blast dest: weakTransitionE)

  from PChain obtain P''' where tPChain: "Ψ ⊳ τ.(P) ⟹⇧^⇩τ P'''" and "Ψ ⊳ P'' ∼ P'''" by(rule tauChainCons)
  moreover from QimpP'' ‹Ψ ⊳ P'' ∼ P'''› have "insertAssertion (extractFrame Q) Ψ ↪⇩F insertAssertion(extractFrame P''') Ψ"
    by(metis bisimE FrameStatEq_def FrameStatImpTrans)
  moreover from tPChain ‹bn α ♯* P› have "bn α ♯* P'''" by(force intro: tauChainFreshChain)
  with ‹Ψ ⊳ P'' ∼ P'''› P''Trans ‹bn α ♯* Ψ› obtain P'''' where "Ψ ⊳ P''' ⟼α ≺ P''''" and "Ψ ⊳ P' ∼ P''''"
    by(metis bisimE simE)
  ultimately show ?thesis
    by(rule_tac Goal) (blast intro: weakTransitionI)
qed                          

end

end