Theory Psi_Calculi.Agent

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

nominal_datatype ('term, 'assertion, 'condition) psi = 
  PsiNil (‹𝟬› 190)


| Output "'term::fs_name" 'term "('term, 'assertion::fs_name, 'condition::fs_name) psi"    (‹_⟨_⟩._› [120, 120, 110] 110)
| Input 'term "('term, 'assertion, 'condition) input"                                      (‹_⦇_› [120, 120] 110)
| Case "(('term, 'assertion, 'condition) psiCase)"                                         (‹Case _› [120] 120)
| Par "('term, 'assertion, 'condition) psi" "('term, 'assertion, 'condition) psi"          (infixl ‹∥› 90)
| Res "«name»(('term, 'assertion, 'condition) psi)"                                        (‹⦇ν_⦈_› [120, 120] 110)
| Assert 'assertion                                                                        (‹⦃_⦄› [120] 120)
| Bang "('term, 'assertion, 'condition) psi"                                               (‹!_› [110] 110)

and ('term, 'assertion, 'condition) input = 
  Trm 'term "(('term, 'assertion, 'condition) psi)"                                        (‹⦈_._› [130, 130] 130)
| Bind "«name»(('term, 'assertion, 'condition) input)"                                     (‹ν__› [120, 120] 120)

and ('term, 'assertion, 'condition) psiCase = 
  EmptyCase                                                                                (‹⊥c› 120)
| Cond 'condition "(('term, 'assertion, 'condition) psi)"
                  "(('term, 'assertion, 'condition) psiCase)"                              (‹□ _ ⇒ _ _ › [120, 120, 120] 120)

lemma psiFreshSet[simp]:
  fixes X :: "name set"
  and   M :: "'a::fs_name"
  and   N :: 'a
  and   P :: "('a, 'b::fs_name, 'c::fs_name) psi"
  and   I :: "('a, 'b, 'c) input"
  and   C :: "('a, 'b, 'c) psiCase"
  and   Q :: "('a, 'b, 'c) psi"
  and   x :: name
  and   Ψ :: 'b
  and   Φ :: 'c

  shows "X ♯* (M⟨N⟩.P) = (X ♯* M ∧ X ♯* N ∧ X ♯* P)"
  and   "X ♯* M⦇I = (X ♯* M ∧ X ♯* I)"
  and   "X ♯* Case C = X ♯* C"
  and   "X ♯* (P ∥ Q) = (X ♯* P ∧ X ♯* Q)"
  and   "X ♯* ⦇νx⦈P = (X ♯* [x].P)"
  and   "X ♯* ⦃Ψ⦄ = X ♯* Ψ"
  and   "X ♯* !P = X ♯* P"
  and   "X ♯* 𝟬"
  and   "X ♯* Trm N P = (X ♯* N ∧ X ♯* P)"
  and   "X ♯* Bind x I = X ♯* ([x].I)"

  and   "X ♯* ⊥c"
  and   "X ♯* □ Φ ⇒ P C = (X ♯* Φ ∧ X ♯* P ∧ X ♯* C)"
by(auto simp add: fresh_star_def psi.fresh)+

lemma psiFreshVec[simp]:
  fixes xvec :: "name list"

  shows "xvec ♯* (M⟨N⟩.P) = (xvec ♯* M ∧ xvec ♯* N ∧ xvec ♯* P)"
  and   "xvec ♯* M⦇I = (xvec ♯* M ∧ xvec ♯* I)"
  and   "xvec ♯* Case C = xvec ♯* C"
  and   "xvec ♯* (P ∥ Q) = (xvec ♯* P ∧ xvec ♯* Q)"
  and   "xvec ♯* ⦇νx⦈P = (xvec ♯* [x].P)"
  and   "xvec ♯* ⦃Ψ⦄ = xvec ♯* Ψ"
  and   "xvec ♯* !P = xvec ♯* P"
  and   "xvec ♯* 𝟬"

  and   "xvec ♯* Trm N P = (xvec ♯* N ∧ xvec ♯* P)"
  and   "xvec ♯* Bind x I = xvec ♯* ([x].I)"

  and   "xvec ♯* ⊥c"
  and   "xvec ♯* □ Φ ⇒ P C = (xvec ♯* Φ ∧ xvec ♯* P ∧ xvec ♯* C)"
by(auto simp add: fresh_star_def)

fun psiCases :: "('c::fs_name × ('a::fs_name, 'b::fs_name, 'c) psi) list ⇒ ('a, 'b, 'c) psiCase"
where 
  base: "psiCases [] = ⊥c"
| step: "psiCases ((Φ, P)#xs) = Cond Φ P (psiCases xs)"

lemma psiCasesEqvt[eqvt]:
  fixes p  :: "name prm"
  and   Cs :: "('c::fs_name × ('a::fs_name, 'b::fs_name, 'c) psi) list"

  shows "(p ∙ (psiCases Cs)) = psiCases(p ∙ Cs)"
by(induct Cs) auto

lemma psiCasesFresh[simp]:
  fixes x  :: name
  and   Cs :: "('c::fs_name × ('a::fs_name, 'b::fs_name, 'c) psi) list"
  
  shows "x ♯ psiCases Cs = x ♯ Cs"
by(induct Cs)
  (auto simp add: fresh_list_nil fresh_list_cons)

lemma psiCasesFreshChain[simp]:
  fixes xvec :: "name list"
  and   Cs :: "('c::fs_name × ('a::fs_name, 'b::fs_name, 'c) psi) list"
  and   Xs   :: "name set"
  
  shows "(xvec ♯* psiCases Cs) = xvec ♯* Cs"
  and   "(Xs ♯* psiCases Cs) = Xs ♯* Cs"
by(auto simp add: fresh_star_def)

abbreviation
  psiCasesJudge (‹Cases _› [80] 80) where "Cases Cs ≡ Case(psiCases Cs)"

primrec resChain :: "name list ⇒ ('a::fs_name, 'b::fs_name, 'c::fs_name) psi ⇒ ('a, 'b, 'c) psi" where
  base: "resChain [] P = P"
| step: "resChain (x#xs) P = ⦇νx⦈(resChain xs P)"

notation resChain (‹⦇ν*_⦈_› [80, 80] 80)

lemma resChainEqvt[eqvt]:
  fixes perm :: "name prm"
  and   lst  :: "name list"
  and   P    :: "('a::fs_name, 'b::fs_name, 'c::fs_name) psi"
  
  shows "perm ∙ (⦇ν*xvec⦈P) = ⦇ν*(perm ∙ xvec)⦈(perm ∙ P)"
by(induct_tac xvec, auto)

lemma resChainSupp:
  fixes xvec :: "name list"
  and   P    :: "('a::fs_name, 'b::fs_name, 'c::fs_name) psi"

  shows "supp(⦇ν*xvec⦈P) = (supp P) - set xvec"
by(induct xvec) (auto simp add: psi.supp abs_supp)

lemma resChainFresh: 
  fixes x    :: name
  and   xvec :: "name list"
  and   P    :: "('a::fs_name, 'b::fs_name, 'c::fs_name) psi"

  shows "x ♯ ⦇ν*xvec⦈P = (x ∈ set xvec ∨ x ♯ P)"
by (induct xvec) (simp_all add: abs_fresh)

lemma resChainFreshSet: 
  fixes Xs   :: "name set"
  and   xvec :: "name list"
  and   yvec :: "name list"
  and   P    :: "('a::fs_name, 'b::fs_name, 'c::fs_name) psi"

  shows "Xs ♯* (⦇ν*xvec⦈P) = (∀x∈Xs. x ∈ set xvec ∨ x ♯ P)"
  and   "yvec ♯* (⦇ν*xvec⦈P) = (∀x∈(set yvec). x ∈ set xvec ∨ x ♯ P)"
by (simp add: fresh_star_def resChainFresh)+

lemma resChainFreshSimps[simp]:
  fixes Xs   :: "name set"
  and   xvec :: "name list"
  and   P    :: "('a::fs_name, 'b::fs_name, 'c::fs_name) psi"
  and   yvec :: "name list"

  shows "Xs ♯* xvec ⟹ Xs ♯* (⦇ν*xvec⦈P) = (Xs ♯* P)"
  and   "yvec ♯* xvec ⟹ yvec ♯* (⦇ν*xvec⦈P) = (yvec ♯* P)"
  and   "xvec ♯* (⦇ν*xvec⦈P)"
apply(simp add: resChainFreshSet) apply(force simp add: fresh_star_def name_list_supp fresh_def)
apply(simp add: resChainFreshSet) apply(force simp add: fresh_star_def name_list_supp fresh_def)
by(simp add: resChainFreshSet)
  
lemma resChainAlpha:
  fixes p    :: "name prm"
  and   xvec :: "name list"
  and   P    :: "('a::fs_name, 'b::fs_name, 'c::fs_name) psi"

  assumes xvecFreshP: "(p ∙ xvec) ♯* P"
  and     S: "set p ⊆ set xvec × set (p ∙ xvec)"

  shows "⦇ν*xvec⦈P = ⦇ν*(p ∙ xvec)⦈(p ∙ P)"
proof -
  note pt_name_inst at_name_inst S
  moreover have "set xvec ♯* (⦇ν*xvec⦈P)"
    by (simp add: resChainFreshSet)
  moreover from xvecFreshP have "set (p ∙ xvec) ♯* (⦇ν*xvec⦈P)"
    by (simp add: resChainFreshSet) (simp add: fresh_star_def)
  ultimately have "⦇ν*xvec⦈P = p ∙ (⦇ν*xvec⦈P)"
    by (rule_tac pt_freshs_freshs [symmetric])
  then show ?thesis by(simp add: eqvts)
qed

lemma resChainAppend:
  fixes xvec :: "name list"
  and   yvec :: "name list"
  and   P    :: "('a::fs_name, 'b::fs_name, 'c::fs_name) psi"
  
  shows "⦇ν*(xvec@yvec)⦈P = ⦇ν*xvec⦈(⦇ν*yvec⦈P)"
by(induct xvec) auto

lemma resChainSimps[dest]:
  fixes xvec :: "name list"
  and   P    :: "('a::fs_name, 'b::fs_name, 'c::fs_name) psi"
  and   Q    :: "('a, 'b, 'c) psi"
  and   P'   :: "('a, 'b, 'c) psi"
  and   Q'   :: "('a, 'b, 'c) psi"

  shows "((⦇ν*xvec⦈(P ∥ Q)) = P' ∥ Q') ⟹ (P = P' ∧ Q = Q')"
  and   "(P ∥ Q = ⦇ν*xvec⦈(P' ∥ Q')) ⟹ (P = P' ∧ Q = Q')"
by(case_tac xvec, simp_all add: psi.inject)+

primrec inputChain :: "name list ⇒ 'a::fs_name ⇒ ('a, 'b::fs_name, 'c::fs_name) psi ⇒ ('a, 'b, 'c) input" where
  base: "inputChain [] N P = ⦈(N).P"
| step: "inputChain (x#xs) N P = ν x (inputChain xs N P)"

abbreviation
  inputChainJudge (‹_⦇λ*_ _⦈._› [80, 80, 80, 80] 80) where "M⦇λ*xvec N⦈.P ≡ M⦇(inputChain xvec N P)"

lemma inputChainEqvt[eqvt]:
  fixes p    :: "name prm"
  and   xvec :: "name list"
  and   N    :: "'a::fs_name"
  and   P    :: "('a, 'b::fs_name, 'c::fs_name) psi"
  
  shows "p ∙ (inputChain xvec N P) = inputChain (p ∙ xvec) (p ∙ N) (p ∙ P)"
by(induct_tac xvec) auto

lemma inputChainFresh: 
  fixes x    :: name
  and   xvec :: "name list"
  and   N    :: "'a::fs_name"
  and   P    :: "('a, 'b::fs_name, 'c::fs_name) psi"

  shows "x ♯ (inputChain xvec N P) = (x ∈ set xvec ∨ (x ♯ N ∧ x ♯ P))"
by (induct xvec) (simp_all add: abs_fresh)

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

  shows "xvec ♯* (inputChain xvec N P)"
by(induct xvec) (auto simp add: abs_fresh abs_fresh_star fresh_star_def)

lemma inputChainFreshSet: 
  fixes Xs   :: "name set"
  and   xvec :: "name list"
  and   N    :: "'a::fs_name"
  and   P    :: "('a, 'b::fs_name, 'c::fs_name) psi"

  shows "Xs ♯* (inputChain xvec N P) = (∀x∈Xs. x ∈ set xvec ∨ (x ♯ N ∧ x ♯ P))"
by (simp add: fresh_star_def inputChainFresh)

lemma inputChainAlpha:
  fixes p  :: "name prm"
  and   Xs :: "name set"
  and   Ys :: "name set"

  assumes XsFreshP: "Xs ♯* (inputChain xvec N P)"
  and     YsFreshN: "Ys ♯* N"
  and     YsFreshP: "Ys ♯* P"
  and     S: "set p ⊆ Xs × Ys"

  shows "(inputChain xvec N P) = (inputChain (p ∙ xvec) (p ∙ N) (p ∙ P))"
proof -
  note pt_name_inst at_name_inst XsFreshP S
  moreover from YsFreshN YsFreshP have "Ys ♯* (inputChain xvec N P)"
    by (simp add: inputChainFreshSet) (simp add: fresh_star_def)
  ultimately have "(inputChain xvec N P) = p ∙ (inputChain xvec N P)"
    by (rule_tac pt_freshs_freshs [symmetric])
  then show ?thesis by(simp add: eqvts)
qed

lemma inputChainAlpha':
  fixes p    :: "name prm"
  and   xvec :: "name list"
  and   N    :: "'a::fs_name"
  and   P    :: "('a, 'b::fs_name, 'c::fs_name) psi"

  assumes xvecFreshP: "(p ∙ xvec) ♯* P"
  and     xvecFreshN: "(p ∙ xvec) ♯* N"
  and     S: "set p ⊆ set xvec × set (p ∙ xvec)"

  shows "(inputChain xvec N P) = (inputChain (p ∙ xvec) (p ∙ N) (p ∙ P))"
proof -
  note pt_name_inst at_name_inst S
  moreover have "set xvec ♯* (inputChain xvec N P)"
    by (simp add: inputChainFreshSet)
  ultimately show ?thesis using xvecFreshN xvecFreshP 
    by(rule_tac inputChainAlpha) (simp add: fresh_star_def)+
qed

lemma alphaRes:
  fixes M :: "'a::fs_name"
  and   x :: name
  and   P :: "('a, 'b::fs_name, 'c::fs_name) psi"
  and   y :: name

  assumes yFreshP: "y ♯ P"

  shows "⦇νx⦈P = ⦇νy⦈([(x, y)] ∙ P)"
proof(cases "x = y")
  assume "x=y"
  thus ?thesis by simp
next
  assume "x ≠ y"
  with yFreshP show ?thesis
    by(perm_simp add: psi.inject alpha calc_atm fresh_left)
qed

lemma alphaInput:
  fixes x :: name
  and   I :: "('a::fs_name, 'b::fs_name, 'c::fs_name) input"
  and   c :: name

  assumes A1: "c ♯ I"

  shows "ν x I = ν c([(x, c)] ∙ I)"
proof(cases "x = c")
  assume "x=c"
  thus ?thesis by simp
next
  assume "x ≠ c"
  with A1 show ?thesis
    by(perm_simp add: input.inject alpha calc_atm fresh_left)
qed

lemma inputChainLengthEq:
  fixes xvec :: "name list"
  and   yvec :: "name list"
  and   M    :: "'a::fs_name"
  and   P    :: "('a, 'b::fs_name, 'c::fs_name) psi"

  assumes "length xvec = length yvec"
  and     "xvec ♯* yvec"
  and     "distinct yvec"
  and     "yvec ♯* M"
  and     "yvec ♯* P"

  obtains N Q where "inputChain xvec M P = inputChain yvec N Q"
proof -
  assume "⋀N Q. inputChain xvec M P = inputChain yvec N Q ⟹ thesis"
  moreover obtain n where "n = length xvec" by auto
  with assms have "∃N Q. inputChain xvec M P = inputChain yvec N Q"
  proof(induct n arbitrary: xvec yvec M P)
    case 0
    thus ?case by auto
  next
    case(Suc n xvec yvec M P)
    from ‹Suc n = length xvec›
    obtain x xvec' where "xvec = x#xvec'" and "length xvec' = n"
      by(case_tac xvec) auto
    with ‹length xvec = length yvec›
    obtain y yvec' where "yvec = y#yvec'" by(case_tac yvec) auto
    from ‹yvec = y#yvec'› ‹xvec=x#xvec'› ‹xvec ♯* yvec› ‹distinct yvec› ‹length xvec = length yvec› ‹yvec ♯* M› ‹yvec ♯* P›
    have "length xvec' = length yvec'" and "xvec' ♯* yvec'" and "distinct yvec'" and "yvec' ♯* M" and "yvec' ♯* P"
      by simp+
    then obtain N Q where Eq: "inputChain xvec' M P = inputChain yvec' N Q" using ‹length xvec' = n›
      by(drule_tac Suc) auto
    moreover from ‹distinct yvec› ‹yvec = y#yvec'› have "y ♯ yvec'" by auto
    moreover from ‹xvec ♯* yvec› ‹xvec = x#xvec'› ‹yvec=y#yvec'› have "x ≠ y" and "x ♯ yvec'"
      by auto
    moreover from ‹yvec ♯* M› ‹yvec ♯* P› ‹yvec = y#yvec'› have "y ♯ M" and "y ♯ P" by auto
    hence "y ♯ inputChain xvec' M P" by(simp add: inputChainFresh)
    with Eq have "y ♯ inputChain yvec' N Q" by(simp add: inputChainFresh)
    ultimately have "ν x (inputChain xvec' M P) = ν y (inputChain yvec' ([(x, y)] ∙ N) ([(x, y)] ∙ Q))"
      by(simp add: input.inject alpha' eqvts name_swap)
    thus ?case using ‹xvec = x#xvec'› ‹yvec=y#yvec'› by force
  qed
  ultimately show ?thesis
    by blast
qed

lemma inputChainEq:
  fixes xvec :: "name list"
  and   M    :: "'a::fs_name"
  and   P    :: "('a, 'b::fs_name, 'c::fs_name) psi"
  and   yvec :: "name list"
  and   N    :: 'a
  and   Q    :: "('a, 'b, 'c) psi"

  assumes "inputChain xvec M P = inputChain yvec N Q"
  and     "xvec ♯* yvec"
  and     "distinct xvec"
  and     "distinct yvec"

  obtains p where "(set p) ⊆ (set xvec) × set (p ∙ xvec)" and "distinctPerm p" and "yvec = p ∙ xvec" and "N = p ∙ M" and "Q = p ∙ P"
proof -
  assume "⋀p. ⟦set p ⊆ set xvec × set (p ∙ xvec); distinctPerm p; yvec = p ∙ xvec; N = p ∙ M; Q = p ∙ P⟧ ⟹ thesis"
  moreover obtain n where "n = length xvec" by auto
  with assms have "∃p. (set p) ⊆ (set xvec) × set (yvec) ∧ distinctPerm p ∧  yvec = p ∙ xvec ∧ N = p ∙ M ∧ Q = p ∙ P"
  proof(induct n arbitrary: xvec yvec M N P Q)
    case(0 xvec yvec M N P Q)
    have Eq: "inputChain xvec M P = inputChain yvec N Q" by fact
    from ‹0 = length xvec› have "xvec = []" by auto
    moreover with Eq have "yvec = []"
      by(case_tac yvec) auto
    ultimately show ?case using Eq
      by(simp add: input.inject)
  next
    case(Suc n xvec yvec M N P Q)
    from ‹Suc n = length xvec›
    obtain x xvec' where "xvec = x#xvec'" and "length xvec' = n"
      by(case_tac xvec) auto
    from ‹inputChain xvec M P = inputChain yvec N Q› ‹xvec = x # xvec'›
    obtain y yvec' where "inputChain (x#xvec') M P = inputChain (y#yvec') N Q"
      and "yvec = y#yvec'"
      by(case_tac yvec) auto
    hence EQ: "ν x (inputChain xvec' M P) = ν y (inputChain yvec' N Q)"
      by simp
    from ‹xvec = x#xvec'› ‹yvec=y#yvec'› ‹xvec ♯* yvec›
    have "x ≠ y" and "xvec' ♯* yvec'" and "x ♯ yvec'" and "y ♯ xvec'"
      by(auto simp add: fresh_list_cons)
    from ‹distinct xvec› ‹distinct yvec› ‹xvec=x#xvec'› ‹yvec=y#yvec'› have "x ♯ xvec'" and "y ♯ yvec'" and "distinct xvec'" and "distinct yvec'"
      by simp+
    have IH: "⋀xvec yvec M N P Q. ⟦inputChain xvec (M::'a) (P::('a, 'b, 'c) psi) = inputChain yvec (N::'a) (Q::('a, 'b, 'c) psi); xvec ♯* yvec; distinct xvec; distinct yvec; n = length xvec⟧ ⟹ ∃p. (set p) ⊆ (set xvec) × (set yvec) ∧ distinctPerm p ∧  yvec = p ∙ xvec ∧ N = p ∙ M ∧ Q = p ∙ P"
      by fact
    from EQ ‹x ≠ y›  ‹x ♯ yvec'› ‹y ♯ yvec'› have "inputChain xvec' M P = inputChain yvec' ([(x, y)] ∙ N) ([(x, y)] ∙ Q)"
      by(simp add: input.inject alpha eqvts)
    with ‹xvec' ♯* yvec'› ‹distinct xvec'› ‹distinct yvec'› ‹length xvec' = n› IH
    obtain p where S: "(set p) ⊆ (set xvec') × (set yvec')" and "distinctPerm p" and "yvec' = p ∙ xvec'" and "([(x, y)] ∙ N) = p ∙ M" and "([(x, y)] ∙ Q) = p ∙ P"
      by metis
    from S have "set((x, y)#p) ⊆ set(x#xvec') × set(y#yvec')" by auto
    moreover from ‹x ♯ xvec'› ‹x ♯ yvec'› ‹y ♯ xvec'› ‹y ♯ yvec'› S have "x ♯ p" and "y ♯ p"
      apply(induct p)
      by(auto simp add: fresh_list_nil fresh_list_cons fresh_prod name_list_supp) (auto simp add: fresh_def) 

    with S ‹distinctPerm p› ‹x ≠ y› have "distinctPerm((x, y)#p)" by auto
    moreover from ‹yvec' = p ∙ xvec'› ‹x ♯ p› ‹y ♯ p› ‹x ♯ xvec'› ‹y ♯ xvec'› have "(y#yvec') = ((x, y)#p) ∙ (x#xvec')"
      by(simp add: calc_atm freshChainSimps)
    moreover from ‹([(x, y)] ∙ N) = p ∙ M› have "([(x, y)] ∙ [(x, y)] ∙ N) = [(x, y)] ∙ p ∙ M"
      by(simp add: pt_bij)
    hence "N = ((x, y)#p) ∙ M" by simp
    moreover from ‹([(x, y)] ∙ Q) = p ∙ P› have "([(x, y)] ∙ [(x, y)] ∙ Q) = [(x, y)] ∙ p ∙ P"
      by(simp add: pt_bij)
    hence "Q = ((x, y)#p) ∙ P" by simp
    ultimately show ?case using ‹xvec=x#xvec'› ‹yvec=y#yvec'›
      by blast
  qed
  ultimately show ?thesis by blast
qed

lemma inputChainEqLength:
  fixes xvec :: "name list"
  and   M    :: "'a::fs_name"
  and   P    :: "('a, 'b::fs_name, 'c::fs_name) psi"
  and   yvec :: "name list"
  and   N    :: 'a
  and   Q    :: "('a, 'b, 'c) psi"

  assumes "inputChain xvec M P = inputChain yvec N Q"

  shows "length xvec = length yvec"
proof -
  obtain n where "n = length xvec" by auto
  with assms show ?thesis
  proof(induct n arbitrary: xvec yvec M P N Q)
    case(0 xvec yvec M P N Q)
    from ‹0 = length xvec› have "xvec = []" by auto
    moreover with ‹inputChain xvec M P = inputChain yvec N Q› have "yvec = []"
      by(case_tac yvec) auto
    ultimately show ?case by simp
  next
    case(Suc n xvec yvec M P N Q)
    from ‹Suc n = length xvec›
    obtain x xvec' where "xvec = x#xvec'" and "length xvec' = n"
      by(case_tac xvec) auto
    from ‹inputChain xvec M P = inputChain yvec N Q› ‹xvec = x # xvec'›
    obtain y yvec' where "inputChain (x#xvec') M P = inputChain (y#yvec') N Q"
      and "yvec = y#yvec'"
      by(case_tac yvec) auto
    hence EQ: "ν x (inputChain xvec' M P) = ν y (inputChain yvec' N Q)"
      by simp
    have IH: "⋀xvec yvec M P N Q. ⟦inputChain xvec (M::'a) (P::('a, 'b, 'c) psi) = inputChain yvec N Q; n = length xvec⟧ ⟹ length xvec = length yvec"
      by fact
    show ?case
    proof(case_tac "x = y")
      assume "x = y"
      with EQ have "inputChain xvec' M P = inputChain yvec' N Q"
        by(simp add: alpha input.inject)
      with IH ‹length xvec' = n› have "length xvec' = length yvec'"
        by blast
      with ‹xvec = x#xvec'› ‹yvec=y#yvec'›
      show ?case by simp
    next
      assume "x ≠ y"
      with EQ have "inputChain xvec' M P = inputChain ([(x, y)] ∙ yvec') ([(x, y)] ∙ N) ([(x, y)] ∙ Q)"
        by(simp add: alpha input.inject eqvts)
      with IH ‹length xvec' = n› have "length xvec' = length ([(x, y)] ∙ yvec')"
        by blast
      hence "length xvec' = length yvec'"
        by simp
      with ‹xvec = x#xvec'› ‹yvec=y#yvec'›
      show ?case by simp
    qed
  qed
qed

lemma alphaInputChain:
  fixes yvec :: "name list"
  and   xvec :: "name list"
  and   M    :: "'a::fs_name"
  and   P    :: "('a, 'b::fs_name, 'c::fs_name) psi"

  assumes "length xvec = length yvec"
  and     "yvec ♯* M"
  and     "yvec ♯* P"
  and     "yvec ♯* xvec"
  and     "distinct yvec"

  shows "inputChain xvec M P = inputChain yvec ([xvec yvec] ∙v M) ([xvec yvec] ∙v P)"
using assms
proof(induct rule: composePermInduct)
  case cBase
  show ?case by simp
next
  case(cStep x xvec y yvec)
  thus ?case 
    apply auto
    by(subst alphaInput[of y]) (auto simp add: inputChainFresh eqvts)
qed

lemma inputChainInject[simp]:

  shows "(inputChain xvec M P = inputChain xvec N Q) = ((M = N) ∧ (P = Q))"
by(induct xvec) (auto simp add: input.inject alpha)

lemma alphaInputDistinct:
  fixes xvec :: "name list"
  and   M    :: "'a::fs_name"
  and   P    :: "('a, 'b::fs_name, 'c::fs_name) psi"
  and   yvec :: "name list"
  and   N    :: 'a
  and   Q    :: "('a, 'b, 'c) psi"

  assumes Eq: "inputChain xvec M P = inputChain yvec N Q"
  and     xvecDist: "distinct xvec"
  and     Mem: "⋀x. x ∈ set xvec ⟹ x ∈ supp M"
  and     xvecFreshyvec: "xvec ♯* yvec"
  and     xvecFreshN: "xvec ♯* N"
  and     xvecFreshQ: "xvec ♯* Q"

  shows "distinct yvec"
proof -
  from Eq have "length xvec = length yvec"
    by(rule inputChainEqLength)
  with assms show ?thesis
  proof(induct n=="length xvec" arbitrary: xvec yvec N Q rule: nat.induct)
    case(zero xvec yvec N Q)
    thus ?case by simp
  next
    case(Suc n xvec yvec N Q)
    have L: "length xvec = length yvec" and "Suc n = length xvec" by fact+
    then obtain x xvec' y yvec' where xEq: "xvec = x#xvec'" and yEq: "yvec = y#yvec'"
                                  and L': "length xvec' = length yvec'"
      by(cases xvec, auto, cases yvec, auto)
    have xvecFreshyvec: "xvec ♯* yvec" and xvecDist: "distinct xvec" by fact+
    with xEq yEq have xineqy: "x ≠ y" and xvec'Freshyvec': "xvec' ♯* yvec'"
                  and xvec'Dist: "distinct xvec'" and xFreshxvec': "x ♯ xvec'"
                  and xFreshyvec': "x ♯ yvec'" and yFreshxvec': "y ♯ xvec'"
      by(auto simp add: fresh_list_cons)
    have Eq: "inputChain xvec M P = inputChain yvec N Q" by fact
    with xEq yEq xineqy have Eq': "inputChain xvec' M P = inputChain ([(x, y)] ∙ yvec') ([(x, y)] ∙ N) ([(x, y)] ∙ Q)"
      by(simp add: input.inject alpha eqvts) 
    moreover have Mem:"⋀x. x ∈ set xvec ⟹ x ∈ supp M" by fact
    with xEq have "⋀x. x ∈ set xvec' ⟹ x ∈ supp M" by simp
    moreover have xvecFreshN: "xvec ♯* N" by fact
    with xEq xFreshxvec' yFreshxvec' have "xvec' ♯* ([(x, y)] ∙ N)" by simp
    moreover have xvecFreshQ: "xvec ♯* Q" by fact
    with xEq xFreshxvec' yFreshxvec' have "xvec' ♯* ([(x, y)] ∙ Q)" by simp
    moreover have "Suc n = length xvec" by fact
    with xEq have "n = length xvec'" by simp
    moreover from xvec'Freshyvec' xFreshxvec' yFreshxvec' have "xvec' ♯* ([(x, y)] ∙ yvec')"
      by simp
    moreover from L' have "length xvec' = length([(x, y)] ∙ yvec')" by simp
    ultimately have "distinct([(x, y)] ∙ yvec')" using xvec'Dist
      by(rule_tac Suc)
    hence "distinct yvec'" by simp
    from Mem xEq have xSuppM: "x ∈ supp M" by simp
    from L xvecFreshyvec xvecDist xvecFreshN xvecFreshQ
    have "inputChain yvec N Q = inputChain xvec ([yvec xvec] ∙v N) ([yvec xvec] ∙v Q)"
      by(simp add: alphaInputChain)
    with Eq have "M = [yvec xvec] ∙v N"  by auto
    with xEq yEq have "M = [(y, x)] ∙ [yvec' xvec'] ∙v N"
      by simp
    with xSuppM have ySuppN: "y ∈ supp([yvec' xvec'] ∙v N)"
      by(drule_tac pi="[(x, y)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
        (simp add: calc_atm eqvts name_swap)
    have "y ♯ yvec'"
    proof(simp add: fresh_def, rule notI)
      assume "y ∈ supp yvec'"
      hence "y mem yvec'"
        by(induct yvec') (auto simp add: supp_list_nil supp_list_cons supp_atm)
      moreover from xvecFreshN xEq xFreshxvec' have "xvec' ♯* N" by simp
      ultimately have "y ♯ [yvec' xvec'] ∙v  N" using L' xvec'Freshyvec' xvec'Dist
        by(force intro: freshChainPerm simp add: freshChainSym)
      with ySuppN show "False" by(simp add: fresh_def)
    qed
    with ‹distinct yvec'›  yEq show ?case by simp
  qed
qed

lemma psiCasesInject[simp]:
  fixes CsP  :: "('c::fs_name × ('a::fs_name, 'b::fs_name, 'c) psi) list"
  and   CsQ  :: "('c × ('a, 'b, 'c) psi) list"

  shows "(psiCases CsP = psiCases CsQ) = (CsP = CsQ)"
proof(induct CsP arbitrary: CsQ)
  case(Nil CsQ)
  thus ?case by(case_tac CsQ) (auto)
next
  case(Cons a CsP CsQ)
  thus ?case
    by(case_tac a, case_tac CsQ) (clarsimp simp add: psiCase.inject)+
qed

lemma casesInject[simp]:
  fixes CsP :: "('c::fs_name × ('a::fs_name, 'b::fs_name, 'c) psi) list"
  and   CsQ :: "('c × ('a, 'b, 'c) psi) list"

  shows "(Cases CsP = Cases CsQ) = (CsP = CsQ)"
apply(induct CsP)
apply(auto simp add: psiCase.inject)
apply(case_tac CsQ)
apply(simp add: psiCase.inject psi.inject)
apply(force simp add: psiCase.inject psi.inject)
apply(case_tac CsQ)
apply(force simp add: psiCase.inject psi.inject)
apply(auto simp add: psiCase.inject psi.inject)
apply(simp only: psiCases.simps[symmetric])
apply(simp only: psiCasesInject)
apply simp
apply(case_tac CsQ)
by(auto simp add: psiCase.inject psi.inject)

nominal_primrec
  guarded :: "('a::fs_name, 'b::fs_name, 'c::fs_name) psi ⇒ bool"
  and guarded'  :: "('a::fs_name, 'b::fs_name, 'c::fs_name) input ⇒ bool"
  and guarded'' :: "('a::fs_name, 'b::fs_name, 'c::fs_name) psiCase ⇒ bool"

where
  "guarded (𝟬) = True"
| "guarded (M⟨N⟩.P) = True"
| "guarded (M⦇I) = True"
| "guarded (Case C) = guarded'' C"
| "guarded (P ∥ Q) = ((guarded P) ∧ (guarded Q))"
| "guarded (⦇νx⦈P) = (guarded P)"
| "guarded (⦃Ψ⦄) = False"
| "guarded (!P) = guarded P"

| "guarded' (Trm M P) = False"
| "guarded' (ν y I) = False"

| "guarded'' (⊥c) = True"
| "guarded'' (□φ ⇒ P C) = (guarded P ∧ guarded'' C)"
apply(finite_guess)+
apply(rule TrueI)+
by(fresh_guess add: fresh_bool)+

lemma guardedEqvt[eqvt]:
  fixes p    :: "name prm"
  and   P    :: "('a::fs_name, 'b::fs_name, 'c::fs_name) psi"
  and   I    :: "('a, 'b, 'c) input"
  and   C    :: "('a, 'b, 'c) psiCase"

  shows "(p ∙ (guarded P)) = guarded (p ∙ P)"
  and   "(p ∙ (guarded' I)) = guarded' (p ∙ I)"
  and   "(p ∙ (guarded'' C)) = guarded'' (p ∙ C)"
by(nominal_induct P and I and C rule: psi_input_psiCase.strong_inducts)
  (simp add: eqvts)+

lemma guardedClosed[simp]:
  fixes P :: "('a::fs_name, 'b::fs_name, 'c::fs_name) psi"
  and   p :: "name prm"

  assumes "guarded P"

  shows "guarded(p ∙ P)"
proof -
  from ‹guarded P› have "p ∙ (guarded P)"
    by(simp add: perm_bool)
  thus ?thesis by(simp add: eqvts)
qed

locale substPsi =
  substTerm?: substType substTerm +
  substAssert?: substType substAssert +
  substCond?: substType substCond

  for substTerm :: "('a::fs_name) ⇒ name list ⇒ 'a::fs_name list ⇒ 'a"
  and substAssert :: "('b::fs_name) ⇒ name list ⇒ 'a::fs_name list ⇒ 'b"
  and substCond :: "('c::fs_name) ⇒ name list ⇒ 'a::fs_name list ⇒ 'c"
begin

nominal_primrec 
    subs   :: "('a::fs_name, 'b::fs_name, 'c::fs_name) psi ⇒ name list ⇒ 'a list ⇒ ('a, 'b, 'c) psi"
and subs'  :: "('a::fs_name, 'b::fs_name, 'c::fs_name) input ⇒ name list ⇒ 'a list ⇒ ('a, 'b, 'c) input"
and subs'' :: "('a::fs_name, 'b::fs_name, 'c::fs_name) psiCase ⇒ name list ⇒ 'a list  ⇒ ('a, 'b, 'c) psiCase"

where
  "subs (𝟬) xvec Tvec = 𝟬"
| "(subs (M⟨N⟩.P) xvec Tvec) = (substTerm M xvec Tvec)⟨(substTerm N xvec Tvec)⟩.(subs P xvec Tvec)"
| "(subs (M⦇I) xvec Tvec) = (substTerm M xvec Tvec)⦇(subs' I xvec Tvec)"

| "(subs (Case C) xvec Tvec) = (Case (subs'' C xvec Tvec))"
| "(subs (P ∥ Q) xvec Tvec) = (subs P xvec Tvec) ∥ (subs Q xvec Tvec)"
| "⟦y ♯ xvec; y ♯ Tvec⟧ ⟹ (subs (⦇νy⦈P) xvec Tvec) = ⦇νy⦈(subs P xvec Tvec)"
| "(subs (⦃Ψ⦄) xvec Tvec) = ⦃(substAssert Ψ xvec Tvec)⦄"
| "(subs (!P) xvec Tvec) = !(subs P xvec Tvec)"

| "(subs' ((Trm M P)::('a::fs_name, 'b::fs_name, 'c::fs_name) input) xvec Tvec) = (⦈(substTerm M xvec Tvec).(subs P xvec Tvec))"
| "⟦y ♯ xvec; y ♯ Tvec⟧ ⟹ (subs' (ν y I) xvec Tvec) = (ν y (subs' I xvec Tvec))"

| "(subs'' (⊥c::('a::fs_name, 'b::fs_name, 'c::fs_name) psiCase) xvec Tvec) = ⊥c"
| "(subs'' (□Φ ⇒ P C) xvec Tvec) = (□(substCond Φ xvec Tvec) ⇒ (subs P xvec Tvec) (subs'' C xvec Tvec))"
apply(finite_guess add: substTerm.fs substAssert.fs substCond.fs)+
apply(rule TrueI)+
apply(simp add: abs_fresh)
apply(simp add: abs_fresh)
apply(simp add: abs_fresh)
apply(rule supports_fresh[of "supp(xvec, Tvec)"])
apply(force simp add: perm_fun_def eqvts fresh_def[symmetric] supports_def)
apply(simp add: fs_name1)
apply(simp add: fresh_def[symmetric])
apply(rule supports_fresh[of "supp(xvec, Tvec)"])
apply(force simp add: perm_fun_def eqvts fresh_def[symmetric] supports_def)
apply(simp add: fs_name1)
apply(simp add: fresh_def[symmetric])
apply(fresh_guess)+
apply(rule supports_fresh[of "supp(xvec, Tvec)"])
apply(force simp add: perm_fun_def eqvts fresh_def[symmetric] supports_def)
apply(simp add: fs_name1)
apply(simp add: fresh_def[symmetric])
apply(fresh_guess)+
apply(rule supports_fresh[of "supp(xvec, Tvec)"])
apply(force simp add: perm_fun_def eqvts fresh_def[symmetric] supports_def)
apply(simp add: fs_name1)
apply(simp add: fresh_def[symmetric])
apply(fresh_guess)+
apply(rule supports_fresh[of "supp(xvec, Tvec)"])
apply(force simp add: perm_fun_def eqvts fresh_def[symmetric] supports_def)
apply(simp add: fs_name1)
apply(simp add: fresh_def[symmetric])
apply(fresh_guess)
apply(rule supports_fresh[of "supp(xvec, Tvec)"])
apply(force simp add: perm_fun_def eqvts fresh_def[symmetric] supports_def)
apply(simp add: fs_name1)
apply(simp add: fresh_def[symmetric])
apply(rule supports_fresh[of "supp(xvec, Tvec)"])
apply(force simp add: perm_fun_def eqvts fresh_def[symmetric] supports_def)
apply(simp add: fs_name1)
apply(simp add: fresh_def[symmetric])
apply(fresh_guess)+
apply(rule supports_fresh[of "supp(xvec, Tvec)"])
apply(force simp add: perm_fun_def eqvts fresh_def[symmetric] supports_def)
apply(simp add: fs_name1)
apply(simp add: fresh_def[symmetric])
apply(fresh_guess)+
apply(rule supports_fresh[of "supp(xvec, Tvec)"])
apply(force simp add: perm_fun_def eqvts fresh_def[symmetric] supports_def)
apply(simp add: fs_name1)
apply(simp add: fresh_def[symmetric])
apply(fresh_guess)+
apply(rule supports_fresh[of "supp(xvec, Tvec)"])
apply(force simp add: perm_fun_def eqvts fresh_def[symmetric] supports_def)
apply(simp add: fs_name1)
apply(simp add: fresh_def[symmetric])
done

lemma substEqvt[eqvt]:
  fixes p    :: "name prm"
  and   P    :: "('a, 'b, 'c) psi"
  and   xvec :: "name list"
  and   Tvec :: "'a list"
  and   I    :: "('a, 'b, 'c) input"
  and   C    :: "('a, 'b, 'c) psiCase"

  shows "(p ∙ (subs P xvec Tvec)) = subs (p ∙ P) (p ∙ xvec) (p ∙ Tvec)"
  and   "(p ∙ (subs' I xvec Tvec)) = subs' (p ∙ I) (p ∙ xvec) (p ∙ Tvec)"
  and   "(p ∙ (subs'' C xvec Tvec)) = subs'' (p ∙ C) (p ∙ xvec) (p ∙ Tvec)"
apply(nominal_induct P and I and C avoiding: xvec Tvec rule: psi_input_psiCase.strong_inducts)
apply(auto simp add: eqvts)
apply(drule_tac pi=p in pt_fresh_bij1[OF pt_name_inst, OF at_name_inst])
apply(drule_tac pi=p in pt_fresh_bij1[OF pt_name_inst, OF at_name_inst])
apply simp
apply(drule_tac pi=p in pt_fresh_bij1[OF pt_name_inst, OF at_name_inst])
apply(drule_tac pi=p in pt_fresh_bij1[OF pt_name_inst, OF at_name_inst])
by simp

lemma subst2[intro]:
  fixes xvec :: "name list"
  and   Tvec :: "'a list"
  and   x    :: name
  and   P    :: "('a, 'b, 'c) psi"
  and   I    :: "('a, 'b, 'c) input"
  and   C    :: "('a, 'b, 'c) psiCase"

  assumes "x ♯ Tvec"
  and     "x ♯ xvec"

  shows "x ♯ P ⟹ x ♯ (subs P xvec Tvec)"
  and   "x ♯ I ⟹ x ♯ (subs' I xvec Tvec)"
  and   "x ♯ C ⟹ x ♯ (subs'' C xvec Tvec)"
using assms
by(nominal_induct P and I and C avoiding: xvec Tvec rule: psi_input_psiCase.strong_inducts)
  (auto intro: substTerm.subst2 substCond.subst2 substAssert.subst2 simp add: abs_fresh)

lemma subst2Chain[intro]:
  fixes xvec :: "name list"
  and   Tvec :: "'a list"
  and   Xs   :: "name set"
  and   P    :: "('a, 'b, 'c) psi"
  and   I    :: "('a, 'b, 'c) input"
  and   C    :: "('a, 'b, 'c) psiCase"

  assumes "Xs ♯* xvec"
  and     "Xs ♯* Tvec"

  shows "Xs ♯* P ⟹ Xs ♯* (subs P xvec Tvec)"
  and   "Xs ♯* I ⟹ Xs ♯* (subs' I xvec Tvec)"
  and   "Xs ♯* C ⟹ Xs ♯* (subs'' C xvec Tvec)"
using assms
by(auto intro: subst2 simp add: fresh_star_def)

lemma renaming:
  fixes xvec :: "name list"
  and   Tvec :: "'a list"
  and   p    :: "name prm"
  and   P    :: "('a, 'b, 'c) psi"
  and   I    :: "('a ,'b, 'c) input"
  and   C    :: "('a, 'b, 'c) psiCase"

  assumes "length xvec = length Tvec"
  and     "set p ⊆ set xvec × set (p ∙ xvec)"
  and     "distinctPerm p"

  shows "⟦(p ∙ xvec) ♯* P⟧ ⟹ (subs P xvec Tvec) = subs (p ∙ P) (p ∙ xvec) Tvec"
  and   "⟦(p ∙ xvec) ♯* I⟧ ⟹ (subs' I xvec Tvec) = subs' (p ∙ I) (p ∙ xvec) Tvec"
  and   "⟦(p ∙ xvec) ♯* C⟧ ⟹ (subs'' C xvec Tvec) = subs'' (p ∙ C) (p ∙ xvec) Tvec"
using assms
by(nominal_induct P and I and C avoiding: xvec p Tvec rule: psi_input_psiCase.strong_inducts)
  (auto intro: substTerm.renaming substCond.renaming substAssert.renaming simp add: freshChainSimps psi.inject input.inject psiCase.inject)

lemma subst4Chain:
  fixes xvec :: "name list"
  and   Tvec :: "'a list"
  and   P    :: "('a, 'b, 'c) psi"
  and   I    :: "('a, 'b, 'c) input"
  and   C    :: "('a, 'b, 'c) psiCase"

  assumes "length xvec = length Tvec"
  and     "distinct xvec"
  and     "xvec ♯* Tvec"

  shows "xvec ♯* (subs P xvec Tvec)"
  and   "xvec ♯* (subs' I xvec Tvec)"
  and   "xvec ♯* (subs'' C xvec Tvec)"
using assms
by(nominal_induct P and I and C avoiding: xvec Tvec rule: psi_input_psiCase.strong_inducts)
  (auto intro: substTerm.subst4Chain substCond.subst4Chain substAssert.subst4Chain simp add: abs_fresh)

lemma guardedSubst[simp]:
  fixes P    :: "('a, 'b, 'c) psi"
  and   I    :: "('a, 'b, 'c) input"
  and   C    :: "('a, 'b, 'c) psiCase"
  and   xvec :: "name list"
  and   Tvec :: "'a list"

  assumes "length xvec = length Tvec"
  and     "distinct xvec"

  shows "guarded P ⟹ guarded(subs P xvec Tvec)"
  and   "guarded' I ⟹ guarded'(subs' I xvec Tvec)"
  and   "guarded'' C ⟹ guarded''(subs'' C xvec Tvec)"
using assms
by(nominal_induct P and I and C avoiding: xvec Tvec rule: psi_input_psiCase.strong_inducts) auto

definition seqSubs :: "('a, 'b, 'c) psi ⇒ (name list × 'a list) list ⇒ ('a, 'b, 'c) psi" (‹_[<_>]› [80, 80] 130)
  where "P[<σ>] ≡ foldl (λQ. λ(xvec, Tvec). subs Q xvec Tvec) P σ"

definition seqSubs' :: "('a, 'b, 'c) input ⇒ (name list × 'a list) list ⇒ ('a, 'b, 'c) input" 
  where "seqSubs' I σ ≡ foldl (λQ. λ(xvec, Tvec). subs' Q xvec Tvec) I σ"

definition seqSubs'' :: "('a, 'b, 'c) psiCase ⇒ (name list × 'a list) list ⇒ ('a, 'b, 'c) psiCase"
  where "seqSubs'' C σ ≡ foldl (λQ. λ(xvec, Tvec). subs'' Q xvec Tvec) C σ"

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

  assumes "xvec ♯* yvec"
  and     "xvec ♯* Tvec"

  shows "subs' (inputChain xvec N P) yvec Tvec = inputChain xvec (substTerm N yvec Tvec) (subs P yvec Tvec)"
using assms
by(induct xvec) (auto simp add: psi.inject)

fun caseListSubst :: "('c × ('a, 'b, 'c) psi) list ⇒ name list ⇒ 'a list ⇒ ('c × ('a, 'b, 'c) psi) list"
where
  "caseListSubst [] _ _ = []"
| "caseListSubst ((φ, P)#Cs) xvec Tvec = (substCond φ xvec Tvec, (subs P xvec Tvec))#(caseListSubst Cs xvec Tvec)"

lemma substCases[simp]:
  fixes Cs   :: "('c × ('a, 'b, 'c) psi) list"
  and   xvec :: "name list"
  and   Tvec :: "'a list"

  shows "subs (Cases Cs) xvec Tvec = Cases(caseListSubst Cs xvec Tvec)"
by(induct Cs) (auto simp add: psi.inject)

lemma substCases'[simp]:
  fixes Cs   :: "('c × ('a, 'b, 'c) psi) list"
  and   xvec :: "name list"
  and   Tvec :: "'a list"

  shows "(subs'' (psiCases Cs) xvec Tvec) = psiCases(caseListSubst Cs xvec Tvec)"
by(induct Cs) auto

lemma seqSubstSimps[simp]:
  shows "seqSubs (𝟬) σ = 𝟬"
  and   "(seqSubs (M⟨N⟩.P) σ) = (substTerm.seqSubst M σ)⟨(substTerm.seqSubst N σ)⟩.(seqSubs P σ)"
  and   "(seqSubs (M⦇I) σ) = (substTerm.seqSubst M σ)⦇(seqSubs' I σ)"

  and   "(seqSubs (Case C) σ) = (Case (seqSubs'' C σ))"
  and   "(seqSubs (P ∥ Q) σ) = (seqSubs P σ) ∥ (seqSubs Q σ)"
  and   "⟦y ♯ σ⟧ ⟹ (seqSubs (⦇νy⦈P) σ) = ⦇νy⦈(seqSubs P σ)"
  and   "(seqSubs (⦃Ψ⦄) σ) = ⦃(substAssert.seqSubst Ψ σ)⦄"
  and   "(seqSubs (!P) σ) = !(seqSubs P σ)"
  
  and   "(seqSubs' ((Trm M P)::('a::fs_name, 'b::fs_name, 'c::fs_name) input) σ) = (⦈(substTerm.seqSubst M σ).(seqSubs P σ))"
  and   "⟦y ♯ σ⟧ ⟹ (seqSubs' (ν y I) σ) = (ν y (seqSubs' I σ))"
  
  and   "(seqSubs'' (⊥c::('a::fs_name, 'b::fs_name, 'c::fs_name) psiCase) σ) = ⊥c"
  and   "(seqSubs'' (□Φ ⇒ P C) σ) = (□(substCond.seqSubst Φ σ) ⇒ (seqSubs P σ) (seqSubs'' C σ))"
by(induct σ arbitrary: M N P I C Q Ψ Φ, auto simp add: seqSubs_def seqSubs'_def seqSubs''_def)

lemma seqSubsNil[simp]:
  "seqSubs P [] = P"
by(simp add: seqSubs_def)

lemma seqSubsCons[simp]:
  shows "seqSubs P ((xvec, Tvec)#σ) = seqSubs(subs P xvec Tvec) σ"
  by(simp add: seqSubs_def)

lemma seqSubsTermAppend[simp]:
  shows "seqSubs P (σ@σ') = seqSubs (seqSubs P σ) σ'"
by(induct σ) (auto simp add: seqSubs_def)

fun caseListSeqSubst :: "('c × ('a, 'b, 'c) psi) list ⇒ (name list × 'a list) list ⇒ ('c × ('a, 'b, 'c) psi) list"
where
  "caseListSeqSubst [] _ = []"
| "caseListSeqSubst ((φ, P)#Cs) σ = (substCond.seqSubst φ σ, (seqSubs P σ))#(caseListSeqSubst Cs σ)"

lemma seqSubstCases[simp]:
  fixes Cs :: "('c × ('a, 'b, 'c) psi) list"
  and   σ  :: "(name list × 'a list) list"

  shows "seqSubs (Cases Cs) σ = Cases(caseListSeqSubst Cs σ)"
by(induct Cs) (auto simp add: psi.inject)

lemma seqSubstCases'[simp]:
  fixes Cs :: "('c × ('a, 'b, 'c) psi) list"
  and   σ  :: "(name list × 'a list) list"

  shows "(seqSubs'' (psiCases Cs) σ) = psiCases(caseListSeqSubst Cs σ)"
by(induct Cs) auto

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

  shows "(p ∙ (P[<σ>])) = (p ∙ P)[<(p ∙ σ)>]"
by(induct σ arbitrary: P) (auto simp add: eqvts seqSubs_def)

lemma guardedSeqSubst:
  assumes "guarded P"
  and     "wellFormedSubst σ"

  shows "guarded(seqSubs P σ)"
using assms
by(induct σ arbitrary: P) (auto dest: guardedSubst)

end

lemma inter_eqvt:
  shows "(pi::name prm) ∙ ((X::name set) ∩ Y) = (pi ∙ X) ∩ (pi ∙ Y)"
by(auto simp add: perm_set_def perm_bij)

lemma delete_eqvt:
  fixes p :: "name prm"
  and   X :: "name set"
  and   Y :: "name set"

  shows "p ∙ (X - Y) = (p ∙ X) - (p ∙ Y)"
by(auto simp add: perm_set_def perm_bij)

lemma perm_singleton[simp]:
  shows "(p::name prm) ∙ {(x::name)} = {p ∙ x}"
by(auto simp add: perm_set_def)

end