Theory Psi_Calculi.Subst_Term

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

locale substType =
  fixes subst :: "'a::fs_name  name list  'b::fs_name list  'a" ("_[_::=_]" [80, 80 ,80] 130)

  assumes eq[eqvt]: "p::name prm. (p  (M[xvec::=Tvec])) = ((p  M)[(p  xvec)::=(p  Tvec)])"
(*  and subst1:       "⋀xvec Tvec T x. ⟦length xvec = length Tvec; distinct xvec; (x::name) ♯ T[xvec::=Tvec]; x ♯ xvec⟧ ⟹ x ♯ T"
  and subst2:       "⋀xvec Tvec T x. ⟦length xvec = length Tvec; distinct xvec; (x::name) ♯ T; x ♯ Tvec⟧ ⟹ x ♯ T[xvec::=Tvec]"*)
  and subst3:       "xvec Tvec T x. length xvec = length Tvec; distinct xvec; set(xvec)  supp(T); (x::name)  T[xvec::=Tvec]  x  Tvec"
(*  and subst4:       "⋀xvec Tvec T. ⟦length xvec = length Tvec; distinct xvec; xvec ♯* T⟧ ⟹ T[xvec::=Tvec] = T"
  and subst5:       "⋀xvec Tvec yvec Tvec' T. ⟦length xvec = length Tvec; distinct xvec; length yvec = length Tvec'; distinct yvec; yvec ♯* xvec; yvec ♯* Tvec⟧ ⟹
                                                T[(xvec@yvec)::=(Tvec@Tvec')] = (T[xvec::=Tvec])[yvec::=Tvec']"*)
  and renaming:     "xvec Tvec p T. length xvec = length Tvec; (set p)  set xvec × set (p  xvec);
                                      distinctPerm p; (p  xvec) ♯* T 
                                      T[xvec::=Tvec] = (p  T)[(p  xvec)::=Tvec]"
begin

lemma suppSubst:
  fixes M    :: 'a
  and   xvec :: "name list"
  and   Tvec :: "'b list"
  
  shows "(supp(M[xvec::=Tvec])::name set)  ((supp M)  (supp xvec)  (supp Tvec))"
proof(auto simp add: eqvts supp_def)
  fix x::name
  let ?P = "λy. ([(x, y)]  M)[([(x, y)]  xvec)::=([(x, y)]  Tvec)]  M[xvec::=Tvec]"
  let ?Q = "λy M. ([(x, y)]  M)  (M::'a)"
  let ?R = "λy xvec. ([(x, y)]  xvec)  (xvec::name list)"
  let ?S = "λy Tvec. ([(x, y)]  Tvec)  (Tvec::'b list)"
  assume A: "finite {y. ?Q y M}" and B: "finite {y. ?R y xvec}" and C: "finite {y. ?S y Tvec}" and D: "infinite {y. ?P(y)}"
  hence "infinite({y. ?P(y)} - {y. ?Q y M}  - {y. ?R y xvec}  - {y. ?S y Tvec})" 
    by(auto intro: Diff_infinite_finite)
  hence "infinite({y. ?P(y)  ¬(?Q y M)  ¬ (?R y xvec)  ¬ (?S y Tvec)})" by(simp add: set_diff_eq)
  moreover have "{y. ?P(y)  ¬(?Q y M)  ¬ (?R y xvec)  ¬ (?S y Tvec)} = {}" by auto
  ultimately have "infinite {}" by(drule_tac Infinite_cong) auto
  thus False by simp
qed

lemma subst2[intro]:
  fixes x    :: name
  and   M    :: 'a
  and   xvec :: "name list"
  and   Tvec :: "'b list"
  
  assumes "x  M"
  and     "x  xvec"
  and     "x  Tvec"

  shows "x  M[xvec::=Tvec]"
using assms suppSubst
by(auto simp add: fresh_def)

lemma subst2Chain[intro]:
  fixes yvec :: "name list"
  and   M    :: 'a
  and   xvec :: "name list"
  and   Tvec :: "'b list"
  
  assumes "yvec ♯* M"
  and     "yvec ♯* xvec"
  and     "yvec ♯* Tvec"

  shows "yvec ♯* M[xvec::=Tvec]"
using assms
by(induct yvec) auto

lemma fs[simp]: "finite ((supp subst)::name set)"
by(simp add: supp_def perm_fun_def eqvts)
(*
lemma subst1Chain:
  fixes xvec :: "name list"
  and   Tvec :: "'b list"
  and   Xs   :: "name set"
  and   T    :: 'a

  assumes "length xvec = length Tvec"
  and     "distinct xvec"
  and     "Xs ♯* T[xvec::=Tvec]"
  and     "Xs ♯* xvec"

  shows "Xs ♯* T"
using assms
by(auto intro: subst1 simp add: fresh_star_def)
*)
lemma subst3Chain:
  fixes xvec :: "name list"
  and   Tvec :: "'b list"
  and   Xs   :: "name set"
  and   T    :: 'a

  assumes "length xvec = length Tvec"
  and     "distinct xvec"
  and     "set xvec  supp T"
  and     "Xs ♯* T[xvec::=Tvec]"

  shows "Xs ♯* Tvec"
using assms
by(auto intro: subst3 simp add: fresh_star_def)

lemma subst4Chain:
  fixes xvec :: "name list"
  and   Tvec :: "'b list"
  and   T    :: 'a

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

  shows "xvec ♯* T[xvec::=Tvec]"
proof -
  obtain p where "((p::name prm)  (xvec::name list)) ♯* T" and "(p  xvec) ♯* xvec"
             and S: "(set p)  set xvec × set (p  xvec)"
             and "distinctPerm p"
    by(rule_tac xvec=xvec and c="(T, xvec)" in name_list_avoiding) auto 

  from length xvec = length Tvec have "length(p  xvec) = length Tvec" by simp
  moreover from (p  xvec) ♯* T have "(p  p  xvec) ♯* (p  T)"
    by(simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
  with distinctPerm p have "xvec ♯* (p  T)" by simp
  ultimately have "(set xvec) ♯* (p  T)[(p  xvec)::=Tvec]" using xvec ♯* Tvec (p  xvec) ♯* xvec
    by auto

  thus ?thesis using length xvec = length Tvec distinct xvec S (p  xvec) ♯* T distinctPerm p
    by(simp add: renaming)
qed

definition seqSubst :: "'a  (name list × 'b list) list  'a" ("_[<_>]" [80, 80] 130)
  where "M[<σ>]  foldl (λN. λ(xvec, Tvec). N[xvec::=Tvec]) M σ"

lemma seqSubstNil[simp]:
  "seqSubst M [] = M"
by(simp add: seqSubst_def)

lemma seqSubstCons[simp]:
  shows "seqSubst M ((xvec, Tvec)#σ) = seqSubst(M[xvec::=Tvec]) σ"
  by(simp add: seqSubst_def)

lemma seqSubstTermAppend[simp]:
  shows "seqSubst M (σ@σ') = seqSubst (seqSubst M σ) σ'"
by(induct σ) (auto simp add: seqSubst_def)

definition wellFormedSubst :: "(('d::fs_name) list × ('e::fs_name) list) list  bool" where "wellFormedSubst σ = ((filter (λ(xvec, Tvec). ¬(length xvec = length Tvec  distinct xvec)) σ) = [])"

lemma wellFormedSubstEqvt[eqvt]:
  fixes σ :: "(('d::fs_name) list × ('e::fs_name) list) list"
  and   p :: "name prm"

  shows "p  (wellFormedSubst σ) = wellFormedSubst(p  σ)"
by(induct σ arbitrary: p) (auto simp add: eqvts wellFormedSubst_def)

lemma wellFormedSimp[simp]:
  fixes σ :: "(('d::fs_name) list × ('e::fs_name) list) list"
  and   p :: "name prm"
  
  shows "wellFormedSubst(p  σ) = wellFormedSubst σ"
by(induct σ) (auto simp add: eqvts wellFormedSubst_def)

lemma wellFormedNil[simp]:
  "wellFormedSubst []"
by(simp add: wellFormedSubst_def)

lemma wellFormedCons[simp]:
  shows "wellFormedSubst((xvec, Tvec)#σ) = (length xvec = length Tvec  distinct xvec  wellFormedSubst σ)"
by(simp add: wellFormedSubst_def) auto

lemma wellFormedAppend[simp]:
  fixes σ  :: "(('d::fs_name) list × ('e::fs_name) list) list"
  and   σ' :: "(('d::fs_name) list × ('e::fs_name) list) list"

  shows "wellFormedSubst(σ@σ') = (wellFormedSubst σ  wellFormedSubst σ')"
by(simp add: wellFormedSubst_def)

lemma seqSubst2[intro]:
  fixes σ :: "(name list × 'b list) list"
  and   T :: 'a
  and   x :: name

  assumes "x  σ"
  and     "x  T"

  shows "x  T[<σ>]"
using assms
by(induct σ arbitrary: T) (clarsimp |  blast)+

lemma seqSubst2Chain[intro]:
  fixes σ    :: "(name list × 'b list) list"
  and   T    :: 'a
  and   xvec :: "name list"

  assumes "xvec ♯* σ"
  and     "xvec ♯* T"

  shows "xvec ♯* T[<σ>]"
using assms
by(induct xvec) auto

end

end