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 ♯* (MN⟩.P) = (X ♯* M  X ♯* N  X ♯* P)"
  and   "X ♯* MI = (X ♯* M  X ♯* I)"
  and   "X ♯* Case C = X ♯* C"
  and   "X ♯* (P  Q) = (X ♯* P  X ♯* Q)"
  and   "X ♯* ⦇νxP = (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 ♯* (MN⟩.P) = (xvec ♯* M  xvec ♯* N  xvec ♯* P)"
  and   "xvec ♯* MI = (xvec ♯* M  xvec ♯* I)"
  and   "xvec ♯* Case C = xvec ♯* C"
  and   "xvec ♯* (P  Q) = (xvec ♯* P  xvec ♯* Q)"
  and   "xvec ♯* ⦇νxP = (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  (⦇ν*xvecP) = ⦇ν*(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(⦇ν*xvecP) = (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  ⦇ν*xvecP = (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 ♯* (⦇ν*xvecP) = (xXs. x  set xvec  x  P)"
  and   "yvec ♯* (⦇ν*xvecP) = (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 ♯* (⦇ν*xvecP) = (Xs ♯* P)"
  and   "yvec ♯* xvec  yvec ♯* (⦇ν*xvecP) = (yvec ♯* P)"
  and   "xvec ♯* (⦇ν*xvecP)"
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 "⦇ν*xvecP = ⦇ν*(p  xvec)(p  P)"
proof -
  note pt_name_inst at_name_inst S
  moreover have "set xvec ♯* (⦇ν*xvecP)"
    by (simp add: resChainFreshSet)
  moreover from xvecFreshP have "set (p  xvec) ♯* (⦇ν*xvecP)"
    by (simp add: resChainFreshSet) (simp add: fresh_star_def)
  ultimately have "⦇ν*xvecP = p  (⦇ν*xvecP)"
    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(⦇ν*yvecP)"
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) = (xXs. 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 "⦇νxP = ⦇ν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 (MN⟩.P) = True"
| "guarded (MI) = True"
| "guarded (Case C) = guarded'' C"
| "guarded (P  Q) = ((guarded P)  (guarded Q))"
| "guarded (⦇νxP) = (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 (MN⟩.P) xvec Tvec) = (substTerm M xvec Tvec)(substTerm N xvec Tvec)⟩.(subs P xvec Tvec)"
| "(subs (MI) 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 (⦇νyP) 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 (MN⟩.P) σ) = (substTerm.seqSubst M σ)(substTerm.seqSubst N σ)⟩.(seqSubs P σ)"
  and   "(seqSubs (MI) σ) = (substTerm.seqSubst M σ)(seqSubs' I σ)"

  and   "(seqSubs (Case C) σ) = (Case (seqSubs'' C σ))"
  and   "(seqSubs (P  Q) σ) = (seqSubs P σ)  (seqSubs Q σ)"
  and   "y  σ  (seqSubs (⦇νyP) σ) = ⦇ν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