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