Theory Psi_Calculi.Chain

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

lemma pt_set_nil: 
  fixes Xs :: "'a set"
  assumes pt: "pt TYPE('a) TYPE ('x)"
  and     at: "at TYPE('x)"

  shows "([]::'x prm)∙Xs = Xs"
by(auto simp add: perm_set_def pt1[OF pt])

lemma pt_set_append: 
  fixes pi1 :: "'x prm"
  and   pi2 :: "'x prm"
  and   Xs  :: "'a set"
  assumes pt: "pt TYPE('a) TYPE ('x)"
  and     at: "at TYPE('x)"

  shows "(pi1@pi2)∙Xs = pi1∙(pi2∙Xs)"
by(auto simp add: perm_set_def pt2[OF pt])

lemma pt_set_prm_eq: 
  fixes pi1 :: "'x prm"
  and   pi2 :: "'x prm"
  and   Xs  :: "'a set"
  assumes pt: "pt TYPE('a) TYPE ('x)"
  and     at: "at TYPE('x)"

  shows "pi1 ≜ pi2  ⟹ pi1∙Xs = pi2∙Xs"
by(auto simp add: perm_set_def pt3[OF pt])

lemma pt_set_inst:
  assumes pt: "pt TYPE('a) TYPE ('x)"
  and     at: "at TYPE('x)"

  shows "pt TYPE('a set) TYPE('x)"
apply(simp add: pt_def pt_set_nil[OF pt, OF at] pt_set_append[OF pt, OF at])
apply(clarify)
by(rule pt_set_prm_eq[OF pt, OF at])

lemma pt_ball_eqvt:
  fixes pi :: "'a prm"
  and   Xs :: "'b set"
  and   P :: "'b ⇒ bool"

  assumes pt: "pt TYPE('b) TYPE('a)"
  and     at: "at TYPE('a)"

  shows "(pi ∙ (∀x ∈ Xs. P x)) = (∀x ∈ (pi ∙ Xs). pi ∙ P (rev pi ∙ x))"
apply(auto simp add: perm_bool)
apply(drule_tac pi="rev pi" in pt_set_bij2[OF pt, OF at])
apply(simp add: pt_rev_pi[OF pt_set_inst[OF pt, OF at], OF at])
apply(drule_tac pi="pi" in pt_set_bij2[OF pt, OF at])
apply(erule_tac x="pi ∙ x" in ballE)
apply(simp add: pt_rev_pi[OF pt, OF at])
by simp

lemma perm_cart_prod:
  fixes Xs :: "'b set"
  and   Ys :: "'c set"
  and   p  :: "'a prm"

  assumes pt1: "pt TYPE('b) TYPE('a)"
  and     pt2: "pt TYPE('c) TYPE('a)"
  and     at:  "at TYPE('a)"

  shows "(p ∙ (Xs × Ys)) = (((p ∙ Xs) × (p ∙ Ys))::(('b × 'c) set))"
by(auto simp add: perm_set_def)

lemma supp_member:
  fixes Xs :: "'b set"
  and   x  :: 'a

  assumes pt: "pt TYPE('b) TYPE('a)"
  and     at: "at TYPE('a)"
  and     fs: "fs TYPE('b) TYPE('a)"
  and     "finite Xs"
  and     "x ∈ ((supp Xs)::'a set)"

  obtains X where "(X::'b) ∈ Xs" and "x ∈ supp X"
proof -
  from ‹finite Xs› ‹x ∈ supp Xs› have "∃X::'b. (X ∈ Xs) ∧ (x ∈ (supp X))"
  proof(induct rule: finite_induct)
    case empty
    from ‹x ∈ ((supp {})::'a set)› have False
      by(simp add: supp_set_empty)
    thus ?case by simp
  next
    case(insert y Xs)
    show ?case
    proof(case_tac "x ∈ supp y")
      assume "x ∈ supp y"
      thus ?case by force
    next
      assume "x ∉ supp y"
      with ‹x ∈ supp(insert y Xs)› have "x ∈ supp Xs"
        by(simp add: supp_fin_insert[OF pt, OF at, OF fs, OF ‹finite Xs›])
      with ‹x ∈ supp Xs ⟹ ∃X. X ∈ Xs ∧ x ∈ supp X›
      show ?case by force
    qed
  qed
  with that show ?thesis by blast
qed

lemma supp_cart_prod_empty[simp]:
  fixes Xs :: "'b set"

  shows "supp (Xs × {}) = ({}::'a set)"
  and   "supp ({} × Xs) = ({}::'a set)"
by(auto simp add: supp_set_empty)

lemma supp_cart_prod:
  fixes Xs :: "'b set"
  and   Ys :: "'c set"

  assumes pt1: "pt TYPE('b) TYPE('a)"
  and     pt2: "pt TYPE('c) TYPE('a)"
  and     fs1: "fs TYPE('b) TYPE('a)"
  and     fs2: "fs TYPE('c) TYPE('a)"
  and     at:  "at TYPE('a)"
  and     f1:  "finite Xs"
  and     f2:  "finite Ys"
  and     a:   "Xs ≠ {}"
  and     b:   "Ys ≠ {}"

  shows "((supp (Xs × Ys))::'a set) = ((supp Xs) ∪ (supp Ys))"
proof -
  from f1 f2 have f3: "finite(Xs × Ys)" by simp
  show ?thesis
    apply(simp add: supp_of_fin_sets[OF pt_prod_inst[OF pt1, OF pt2], OF at, OF fs_prod_inst[OF fs1, OF fs2], OF f3] supp_prod)
    apply(rule equalityI)
    using Union_included_in_supp[OF pt1, OF at, OF fs1, OF f1] Union_included_in_supp[OF pt2, OF at, OF fs2, OF f2]
    apply(force simp add: supp_prod)
    using a b
    apply(auto simp add: supp_prod)
    using supp_member[OF pt1, OF at, OF fs1, OF f1]
    apply blast
    using supp_member[OF pt2, OF at, OF fs2, OF f2]
    by blast
qed

lemma fresh_cart_prod:
  fixes x  :: 'a
  and   Xs :: "'b set"
  and   Ys :: "'c set"

  assumes pt1: "pt TYPE('b) TYPE('a)"
  and     pt2: "pt TYPE('c) TYPE('a)"
  and     fs1: "fs TYPE('b) TYPE('a)"
  and     fs2: "fs TYPE('c) TYPE('a)"
  and     at:  "at TYPE('a)"
  and     f1:  "finite Xs"
  and     f2:  "finite Ys"
  and     a:   "Xs ≠ {}"
  and     b:   "Ys ≠ {}"

  shows "(x ♯ (Xs × Ys)) = (x ♯ Xs ∧ x ♯ Ys)"
using assms
by(simp add: supp_cart_prod fresh_def)

lemma fresh_star_cart_prod:
  fixes Zs   :: "'a set"
  and   xvec :: "'a list"
  and   Xs   :: "'b set"
  and   Ys   :: "'c set"

  assumes pt1: "pt TYPE('b) TYPE('a)"
  and     pt2: "pt TYPE('c) TYPE('a)"
  and     fs1: "fs TYPE('b) TYPE('a)"
  and     fs2: "fs TYPE('c) TYPE('a)"
  and     at:  "at TYPE('a)"
  and     f1:  "finite Xs"
  and     f2:  "finite Ys"
  and     a:   "Xs ≠ {}"
  and     b:   "Ys ≠ {}"

  shows "(Zs ♯* (Xs × Ys)) = (Zs ♯* Xs ∧ Zs ♯* Ys)"
  and   "(xvec ♯* (Xs × Ys)) = (xvec ♯* Xs ∧ xvec ♯* Ys)"
using assms
by(force simp add: fresh_cart_prod fresh_star_def)+

lemma permCommute:
  fixes p  :: "'a prm"
  and   q  :: "'a prm"
  and   P  :: 'x
  and   Xs :: "'a set"
  and   Ys :: "'a set"

  assumes pt: "pt TYPE('x) TYPE('a)"
  and     at: "at TYPE('a)"
  and     a: "(set p) ⊆ Xs × Ys"
  and     b: "Xs ♯* q"
  and     c: "Ys ♯* q"

  shows "p ∙ q ∙ P = q ∙ p ∙ P"
proof -
  have "p ∙ q ∙ P = (p ∙ q) ∙ p ∙ P"
    by(rule pt_perm_compose[OF pt, OF at])
  moreover from at have "pt TYPE('a) TYPE('a)"
    by(rule at_pt_inst)
  hence "pt TYPE(('a × 'a) list) TYPE('a)"
    by(force intro: pt_prod_inst pt_list_inst)
  hence "p ∙ q = q" using at a b c
    by(rule pt_freshs_freshs)
  ultimately show ?thesis by simp
qed


definition
  distinctPerm :: "'a prm ⇒ bool" where
  "distinctPerm p ≡ distinct((map fst p)@(map snd p))"

lemma at_set_avoiding_aux':
  fixes Xs::"'a set"
  and   As::"'a set"
  assumes at: "at TYPE('a)"
  and     a: "finite Xs"
  and     b: "Xs ⊆ As"
  and     c: "finite As"
  and     d: "finite ((supp c)::'a set)"
  shows "∃(Ys::'a set) (pi::'a prm). Ys♯*c ∧ Ys ∩ As = {} ∧ (pi∙Xs=Ys) ∧ 
          set pi ⊆ Xs × Ys ∧ finite Ys ∧ (distinctPerm pi)"
using a b c
proof (induct)
  case empty
  have "({}::'a set)♯*c" by (simp add: fresh_star_def)
  moreover
  have "({}::'a set) ∩ As = {}" by simp
  moreover
  have "([]::'a prm)∙{} = ({}::'a set)"
    by(rule pt1) (metis Nominal.pt_set_inst at at_pt_inst)
  moreover
  have "set ([]::'a prm) ⊆ {} × {}" by simp
  moreover 
  have "finite ({}::'a set)" by simp
  moreover have "distinctPerm([]::'a prm)"
    by(simp add: distinctPerm_def)
  ultimately show ?case by blast
next
  case (insert x Xs)
  then have ih: "∃Ys pi. Ys♯*c ∧ Ys ∩ As = {} ∧ pi∙Xs = Ys ∧ set pi ⊆ Xs × Ys ∧ finite Ys ∧ distinctPerm pi" by simp
  then obtain Ys pi where a1: "Ys♯*c" and a2: "Ys ∩ As = {}" and a3: "(pi::'a prm)∙Xs = Ys" and 
                          a4: "set pi ⊆ Xs × Ys" and a5: "finite Ys" 
                      and a6: "distinctPerm pi" by blast
  have b: "x∉Xs" by fact
  have d1: "finite As" by fact
  have d2: "finite Xs" by fact
  have d3: "insert x Xs ⊆ As" by fact
  have d4: "finite((supp pi)::'a set)"
    by(induct pi)
      (auto simp add: supp_list_nil supp_prod at_fin_set_supp[OF at]
                      supp_list_cons at_supp[OF at])
  have "∃y::'a. y♯(c,x,Ys,As,pi)" using d d1 a5 d4
    by (rule_tac at_exists_fresh'[OF at])
       (simp add: supp_prod at_supp[OF at] at_fin_set_supp[OF at])
  then obtain y::"'a" where  e: "y♯(c,x,Ys,As,pi)" by blast
  have "({y}∪Ys)♯*c" using a1 e by (simp add: fresh_star_def)
  moreover
  have "({y}∪Ys)∩As = {}" using a2 d1 e by (simp add: fresh_prod at_fin_set_fresh[OF at])
  moreover
  have "(((pi∙x,y)#pi)∙(insert x Xs)) = {y}∪Ys"
  proof -
    have eq: "[(pi∙x,y)]∙Ys = Ys" 
    proof -
      have "(pi∙x)♯Ys" using a3[symmetric] b d2
        by(simp add: pt_fresh_bij[OF pt_set_inst, OF at_pt_inst[OF at], OF at, OF at]
                     at_fin_set_fresh[OF at d2])
      moreover
      have "y♯Ys" using e by simp
      ultimately show "[(pi∙x,y)]∙Ys = Ys" 
        by (simp add: pt_fresh_fresh[OF pt_set_inst, OF at_pt_inst[OF at], OF at, OF at])
    qed
    have "(((pi∙x,y)#pi)∙({x}∪Xs)) = ([(pi∙x,y)]∙(pi∙({x}∪Xs)))"
      by (simp add: pt2[symmetric, OF pt_set_inst, OF at_pt_inst[OF at], OF at])
    also have "… = {y}∪([(pi∙x,y)]∙(pi∙Xs))" 
      by (simp only: union_eqvt perm_set_def at_calc[OF at])(auto)
    also have "… = {y}∪([(pi∙x,y)]∙Ys)" using a3 by simp
    also have "… = {y}∪Ys" using eq by simp
    finally show "(((pi∙x,y)#pi)∙(insert x Xs)) = {y}∪Ys" by auto
  qed
  moreover
  have "pi∙x=x" using a4 b a2 a3 d3 by (rule_tac at_prm_fresh2[OF at]) (auto)
  then have "set ((pi∙x,y)#pi) ⊆ (insert x Xs) × ({y}∪Ys)" using a4 by auto
  moreover 
  have "finite ({y}∪Ys)" using a5 by simp
  moreover from ‹Ys ∩ As = {}› ‹(insert x Xs) ⊆ As› ‹finite Ys› have "x ∉ Ys"
    by(auto simp add: fresh_def at_fin_set_supp[OF at])
  with a6 ‹pi ∙ x = x› ‹x ∉ Xs› ‹(set pi) ⊆ Xs × Ys› e have "distinctPerm((pi ∙ x, y)#pi)"
    apply(auto simp add: distinctPerm_def fresh_prod at_fresh[OF at])
    proof -
      fix a b
      assume "b ♯ pi" and "(a, b) ∈ set pi"
      thus False
        by(induct pi)
          (auto simp add: supp_list_cons supp_prod at_supp[OF at] fresh_list_cons fresh_prod at_fresh[OF at])
    next
      fix a b
      assume "a ♯ pi" and "(a, b) ∈ set pi"
      thus False
        by(induct pi)
          (auto simp add: supp_list_cons supp_prod at_supp[OF at] fresh_list_cons fresh_prod at_fresh[OF at])
    qed
  ultimately 
  show ?case by blast
qed

lemma at_set_avoiding:
  fixes Xs::"'a set"
  assumes at: "at TYPE('a)"
  and     a: "finite Xs"
  and     b: "finite ((supp c)::'a set)"
  obtains pi::"'a prm" where "(pi ∙ Xs) ♯* c" and "set pi ⊆ Xs × (pi ∙ Xs)" and "distinctPerm pi"
  using a b
  by (frule_tac As="Xs" in at_set_avoiding_aux'[OF at]) auto

lemma pt_swap:
  fixes x :: 'a
  and a :: 'x
  and b :: 'x

  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE('x)"

  shows "[(a, b)] ∙ x = [(b, a)] ∙ x"
proof -
  show ?thesis by(simp add: pt3[OF pt] at_ds5[OF at])
qed


atom_decl name

lemma supp_subset:
  fixes Xs :: "'a::fs_name set"
  and   Ys :: "'a::fs_name set"

  assumes "Xs ⊆ Ys"
  and     "finite Xs"
  and     "finite Ys"

  shows "(supp Xs) ⊆ ((supp Ys)::name set)"
proof(rule subsetI)
  fix x
  assume "x ∈ ((supp Xs)::name set)"
  with ‹finite Xs› obtain X where "X ∈ Xs" and "x ∈ supp X"
    by(rule supp_member[OF pt_name_inst, OF at_name_inst, OF fs_name_inst])
  from ‹X ∈ Xs› ‹Xs ⊆ Ys› have "X ∈ Ys" by auto
  with ‹finite Ys› ‹x ∈ supp X› show "x ∈ supp Ys"
    by(induct rule: finite_induct)
      (auto simp add: supp_fin_insert[OF pt_name_inst, OF at_name_inst, OF fs_name_inst])
qed

abbreviation mem_def :: "'a ⇒ 'a list ⇒ bool" (‹_ mem _› [80, 80] 80)  where
  "x mem xs ≡ x ∈ set xs"

lemma memFresh:
  fixes x :: name
  and   p :: "'a::fs_name"
  and   l :: "('a::fs_name) list"

  assumes "x ♯ l"
  and     "p mem l"
  
  shows "x ♯ p"
using assms
by(induct l, auto simp add: fresh_list_cons)

lemma memFreshChain:
  fixes xvec :: "name list"
  and   p    :: "'a::fs_name"
  and   l    :: "'a::fs_name list"
  and   Xs   :: "name set"

  assumes "p mem l"
  
  shows "xvec ♯* l ⟹ xvec ♯* p"
  and   "Xs ♯* l ⟹ Xs ♯* p"
using assms
by(auto simp add: fresh_star_def intro: memFresh)

lemma fresh_star_list_append[simp]:
  fixes A :: "name list"
  and   B :: "name list"
  and   C :: "name list"

  shows "(A ♯* (B @ C)) = ((A ♯* B) ∧ (A ♯* C))"
by(auto simp add: fresh_star_def fresh_list_append)

lemma unionSimps[simp]:
  fixes Xs :: "name set"
  and   Ys :: "name set"
  and   C  :: "'a::fs_name"

  shows "((Xs ∪ Ys) ♯* C) = ((Xs ♯* C) ∧ (Ys ♯* C))"
by(auto simp add: fresh_star_def)

lemma substFreshAux[simp]:
  fixes C    :: "'a::fs_name"
  and   xvec :: "name list"

  shows "xvec ♯* (supp C - set xvec)"
by(auto simp add: fresh_star_def fresh_def at_fin_set_supp[OF at_name_inst] fs_name1)

lemma fresh_star_perm_app[simp]:
  fixes Xs :: "name set"
  and   xvec :: "name list"
  and   p  :: "name prm"
  and   C  :: "'d::fs_name"

  shows "⟦Xs ♯* p; Xs ♯* C⟧ ⟹ Xs ♯* (p ∙ C)"
  and   "⟦xvec ♯* p; xvec ♯* C⟧ ⟹ xvec ♯* (p ∙ C)"
by(auto simp add: fresh_star_def fresh_perm_app)

lemma freshSets[simp]:
  fixes x    :: name
  and   y    :: name
  and   xvec :: "name list"
  and   X    :: "name set"
  and   C    :: 'a

  shows "([]::name list) ♯* C"
  and   "([]::name list) ♯* [y].C"
  and   "({}::name set) ♯* C"
  and   "({}::name set) ♯* [y].C"
  and   "((x#xvec) ♯* C) = (x ♯ C ∧ xvec ♯* C)"
  and   "((x#xvec) ♯* ([y].C)) = (x ♯ ([y].C) ∧ xvec ♯* ([y].C))"
  and   "((insert x X) ♯* C) = (x ♯ C ∧ X ♯* C)"
  and   "((insert x X) ♯* ([y].C)) = (x ♯ ([y].C) ∧ X ♯* ([y].C))"
by(auto simp add: fresh_star_def)

lemma freshStarAtom[simp]: "(xvec::name list) ♯* (x::name) = x ♯ xvec"
by(induct xvec)
  (auto simp add: fresh_list_nil fresh_list_cons fresh_atm)

lemma name_list_set_fresh[simp]:
  fixes xvec :: "name list"
  and   x    :: "'a::fs_name"

  shows "(set xvec) ♯* x = xvec ♯* x"
by(auto simp add: fresh_star_def)

lemma name_list_supp:
  fixes xvec :: "name list"

  shows "set xvec = supp xvec"
proof -
  have "set xvec = supp(set xvec)"
    by(simp add: at_fin_set_supp[OF at_name_inst])
  moreover have "… = supp xvec"
    by(simp add: pt_list_set_supp[OF pt_name_inst, OF at_name_inst, OF fs_name_inst])
  ultimately show ?thesis
    by simp
qed

lemma abs_fresh_list_star:
  fixes xvec :: "name list"
  and   a    :: name
  and   P    :: "'a::fs_name"

  shows "(xvec ♯* [a].P) = ((set xvec) - {a}) ♯* P"
by(induct xvec) (auto simp add: fresh_star_def abs_fresh)

lemma abs_fresh_set_star:
  fixes X :: "name set"
  and   a :: name
  and   P :: "'a::fs_name"

  shows "(X ♯* [a].P) = (X - {a}) ♯* P"
by(auto simp add: fresh_star_def abs_fresh)

lemmas abs_fresh_star = abs_fresh_list_star abs_fresh_set_star

lemma abs_fresh_list_star'[simp]:
  fixes xvec :: "name list"
  and   a    :: name
  and   P    :: "'a::fs_name"

  assumes "a ♯ xvec"

  shows "xvec ♯* [a].P = xvec ♯* P"
using assms
by(induct xvec) (auto simp add: abs_fresh fresh_list_cons fresh_atm)

lemma freshChainSym[simp]:
  fixes xvec :: "name list"
  and   yvec :: "name list"
  
  shows   "xvec ♯* yvec = yvec ♯* xvec"
by(auto simp add: fresh_star_def fresh_def name_list_supp)

lemmas [eqvt] = perm_cart_prod[OF pt_name_inst, OF pt_name_inst, OF at_name_inst]

lemma name_set_avoiding:
  fixes c :: "'a::fs_name"
  and   X :: "name set"
  
  assumes "finite X"
  and     "⋀pi::name prm. ⟦(pi ∙ X) ♯* c; distinctPerm pi; set pi ⊆ X × (pi ∙ X)⟧ ⟹ thesis"

  shows thesis
using assms
by(rule_tac c=c in at_set_avoiding[OF at_name_inst]) (simp_all add: fs_name1)

lemmas simps[simp] = fresh_atm fresh_prod
                     pt3[OF pt_name_inst, OF at_ds1, OF at_name_inst]
                     pt_fresh_fresh[OF pt_name_inst, OF at_name_inst]
                     pt_rev_pi[OF pt_name_inst, OF at_name_inst]
                     pt_pi_rev[OF pt_name_inst, OF at_name_inst]

lemmas name_supp_cart_prod = supp_cart_prod[OF pt_name_inst, OF pt_name_inst, OF fs_name_inst, OF fs_name_inst, OF at_name_inst]
lemmas name_fresh_cart_prod = fresh_cart_prod[OF pt_name_inst, OF pt_name_inst, OF fs_name_inst, OF fs_name_inst, OF at_name_inst]
lemmas name_fresh_star_cart_prod = fresh_star_cart_prod[OF pt_name_inst, OF pt_name_inst, OF fs_name_inst, OF fs_name_inst, OF at_name_inst]


lemmas name_swap_bij[simp] = pt_swap_bij[OF pt_name_inst, OF at_name_inst]
lemmas name_swap = pt_swap[OF pt_name_inst, OF at_name_inst]
lemmas name_set_fresh_fresh[simp] = pt_freshs_freshs[OF pt_name_inst, OF at_name_inst]
lemmas list_fresh[simp] = fresh_list_nil fresh_list_cons fresh_list_append

definition  eqvt :: "'a::fs_name set ⇒ bool" where
                  "eqvt X ≡ ∀x ∈ X. ∀p::name prm. p ∙ x ∈ X"

lemma eqvtUnion[intro]:
  fixes Rel  :: "('d::fs_name) set"
  and   Rel' :: "'d set"

  assumes EqvtRel:  "eqvt Rel"
  and     EqvtRel': "eqvt Rel'"

  shows "eqvt (Rel ∪ Rel')"
using assms
by(force simp add: eqvt_def)

lemma eqvtPerm[simp]: 
  fixes X :: "('d::fs_name) set"
  and   x :: name
  and   y :: name

  assumes "eqvt X"

  shows "([(x, y)] ∙ X) = X"
using assms
apply(auto simp add: eqvt_def)
apply(erule_tac x="[(x, y)] ∙ xa" in ballE)
apply(erule_tac x="[(x, y)]" in allE)
apply simp
apply(drule_tac pi="[(x, y)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply simp
apply(erule_tac x=xa in ballE)
apply(erule_tac x="[(x, y)]" in allE)
apply(drule_tac pi="[(x, y)]" and x="[(x, y)] ∙ xa" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply simp
by simp

lemma eqvtI:
  fixes X :: "'d::fs_name set"
  and   x :: 'd
  and   p :: "name prm"
  
  assumes "eqvt X"
  and     "x ∈ X"
 
  shows "(p ∙ x) ∈ X"
using assms
by(unfold eqvt_def) auto

lemma fresh_star_list_nil[simp]:
  fixes xvec :: "name list"
  and   Xs   :: "name set"
  
  shows "xvec ♯* []"
  and   "Xs ♯* []"
by(auto simp add: fresh_star_def)

lemma fresh_star_list_cons[simp]:
  fixes xvec :: "name list"
  and   Xs   :: "name set"
  and   x    :: "'a::fs_name"
  and   xs   :: "'a list"

  shows "(xvec ♯* (x#xs)) = ((xvec ♯* x) ∧ xvec ♯* xs)"
  and   "(Xs ♯* (x#xs)) = ((Xs ♯* x) ∧ (Xs ♯* xs))"
by(auto simp add: fresh_star_def)

lemma freshStarPair[simp]:
  fixes X    :: "name set"
  and   xvec :: "name list"
  and   x    :: "'a::fs_name"
  and   y    :: "'b::fs_name"

  shows "(X ♯* (x, y)) = (X ♯* x ∧ X ♯* y)"
  and   "(xvec ♯* (x, y)) = (xvec ♯* x ∧ xvec ♯* y)"
by(auto simp add: fresh_star_def)
lemma name_list_avoiding:
  fixes c    :: "'a::fs_name"
  and   xvec :: "name list"
  
  assumes "⋀pi::name prm. ⟦(pi ∙ xvec) ♯* c; distinctPerm pi; set pi ⊆ (set xvec) × (set (pi ∙ xvec))⟧ ⟹ thesis"

  shows thesis
proof -
  have "finite(set xvec)" by simp
  thus ?thesis using assms
    by(rule name_set_avoiding) (auto simp add: eqvts fresh_star_def)
qed

lemma distinctPermSimps[simp]:
  fixes p :: "name prm"
  and   a :: name
  and   b :: name

  shows "distinctPerm([]::name prm)"
  and   "(distinctPerm((a, b)#p)) = (distinctPerm p ∧ a ≠ b ∧ a ♯ p ∧ b ♯ p)"
apply(simp add: distinctPerm_def)
apply(induct p)
apply(unfold distinctPerm_def)
apply(clarsimp)
apply(rule iffI, erule iffE)
by(clarsimp)+

lemma map_eqvt[eqvt]:
  fixes p   :: "name prm"
  and   lst :: "'a::pt_name list"

  shows "(p ∙ (map f lst)) = map (p ∙ f) (p ∙ lst)"
apply(induct lst, auto) 
by(simp add: pt_fun_app_eq[OF pt_name_inst, OF at_name_inst])

lemma consPerm:
  fixes x :: name
  and   y :: name
  and   p :: "name prm"
  and   C :: "'a::pt_name"

  shows "((x, y)#p) ∙ C = [(x, y)] ∙ p ∙ C"
by(simp add: pt2[OF pt_name_inst, THEN sym])

simproc_setup consPerm ("((x, y)#p) ∙ C") = ‹
  fn _ => fn _ => fn ct => 
    case Thm.term_of ct of 
      Const (@{const_name perm}, _ ) $ (Const (@{const_name Cons}, _) $ _ $ p) $ _ =>
        (case p of
          Const (@{const_name Nil}, _) => NONE
        | _ => SOME(mk_meta_eq @{thm consPerm}))
    | _ => NONE
›

lemma distinctEqvt[eqvt]:
  fixes p  :: "name prm"
  and   xs :: "'a::pt_name list"

  shows "(p ∙ (distinct xs)) = distinct (p ∙ xs)"
by(induct xs) (auto simp add: eqvts)

lemma distinctClosed[simp]:
  fixes p  :: "name prm"
  and   xs :: "'a::pt_name list"

  shows "distinct (p ∙ xs) = distinct xs"
apply(induct xs)
apply(auto simp add: eqvts)
apply(drule_tac pi=p in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: eqvts)
apply(drule_tac pi="rev p" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
by(simp add: eqvts)

lemma lengthEqvt[eqvt]:
  fixes p  :: "name prm"
  and   xs :: "'a::pt_name list"
  
  shows "p ∙ (length xs) = length (p ∙ xs)"
by(induct xs) (auto simp add: eqvts)

lemma lengthClosed[simp]:
  fixes p  :: "name prm"
  and   xs :: "'a::pt_name list"
  
  shows "length (p ∙ xs) = length xs"
by(induct xs) (auto simp add: eqvts)

lemma subsetEqvt[eqvt]:
  fixes p :: "name prm"
  and   S :: "('a::pt_name) set"
  and   T :: "('a::pt_name) set"

  shows "(p ∙ (S ⊆ T)) = ((p ∙ S) ⊆ (p ∙ T))"
by(rule pt_subseteq_eqvt[OF pt_name_inst, OF at_name_inst])

lemma subsetClosed[simp]:
  fixes p :: "name prm"
  and   S :: "('a::pt_name) set"
  and   T :: "('a::pt_name) set"

  shows "((p ∙ S) ⊆ (p ∙ T)) = (S ⊆ T)"
apply auto
apply(drule_tac pi=p in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(insert pt_set_bij[OF pt_name_inst, OF at_name_inst])
apply auto
apply(drule_tac pi="rev p" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply auto
apply(subgoal_tac "rev p ∙ x ∈ T")
apply auto
apply(drule_tac pi="p" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply auto
apply(drule_tac pi="p" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
by auto

lemma subsetClosed'[simp]:
  fixes p    :: "name prm"
  and   xvec :: "name list"
  and   P    :: "'a::fs_name"

  shows "(set (p ∙ xvec) ⊆ supp (p ∙ P)) = (set xvec ⊆ supp P)"
by(simp add: eqvts[THEN sym])

lemma memEqvt[eqvt]:
  fixes p  :: "name prm"
  and   x  :: "'a::pt_name"
  and   xs :: "('a::pt_name) list"

  shows "(p ∙ (x mem xs)) = ((p ∙ x) mem (p ∙ xs))"
by(induct xs)
  (auto simp add: pt_bij[OF pt_name_inst, OF at_name_inst] eqvts)

lemma memClosed[simp]:
  fixes p  :: "name prm"
  and   x  :: "'a::pt_name"
  and   xs :: "('a::pt_name) list"

  shows "(p ∙ x) mem (p ∙ xs) = (x mem xs)"
proof -
  have "x mem xs = p ∙ (x mem xs)"
    by(case_tac "x mem xs") auto
  thus ?thesis by(simp add: eqvts)
qed

lemma memClosed'[simp]:
  fixes p  :: "name prm"
  and   x  :: "'a::pt_name"
  and   y  :: "'b::pt_name"
  and   xs :: "('a ×  'b) list" 

  shows "((p ∙ x, p ∙ y) mem (p ∙ xs)) = ((x, y) mem xs)"
apply(subgoal_tac "((x, y) mem xs) = (p ∙ (x, y)) mem (p ∙ xs)")
apply force
by(force simp del: eqvts)


lemma freshPerm:
  fixes x :: name
  and   p :: "name prm"

  assumes "x ♯ p"

  shows "p ∙ x = x"
using assms
apply(rule_tac pt_pi_fresh_fresh[OF pt_name_inst, OF at_name_inst])
by(induct p, auto simp add: fresh_list_cons fresh_prod)

lemma freshChainPermSimp:
  fixes xvec :: "name list"
  and   p    :: "name prm"

  assumes "xvec ♯* p"

  shows "p ∙ xvec = xvec"
  and   "rev p ∙ xvec = xvec"
using assms
by(induct xvec) (auto simp add: freshPerm pt_bij1[OF pt_name_inst, OF at_name_inst, THEN sym])

lemma freshChainAppend[simp]:
  fixes xvec :: "name list"
  and   yvec :: "name list"
  and   C    :: "'a::fs_name"
  
  shows "(xvec@yvec) ♯* C = ((xvec ♯* C) ∧ (yvec ♯* C))"
by(force simp add: fresh_star_def)

lemma subsetFresh:
  fixes xvec :: "name list"
  and   yvec :: "name list"
  and   C    :: "'d::fs_name"

  assumes "set xvec ⊆ set yvec"
  and     "yvec ♯* C"

  shows "xvec ♯* C"
using assms
by(auto simp add: fresh_star_def)

lemma distinctPermCancel[simp]:
  fixes p :: "name prm"
  and   T :: "'a::pt_name"

  assumes "distinctPerm p"

  shows "(p ∙ (p ∙ T)) = T"
using assms
proof(induct p)
  case Nil
  show ?case by simp
next
  case(Cons a p)
  thus ?case
  proof(case_tac a, auto)
    fix a b
    assume "(a::name) ♯ (p::name prm)" "b ♯ p" "p ∙ p ∙ T = T" "a ≠ b"
    thus "[(a, b)] ∙ p ∙ [(a, b)] ∙ p ∙ T = T"
      by(subst pt_perm_compose[OF pt_name_inst, OF at_name_inst]) simp
  qed
qed

fun composePerm :: "name list ⇒ name list ⇒ name prm"
where
  Base:  "composePerm [] [] = []"
| Step:  "composePerm (x#xs) (y#ys) = (x, y)#(composePerm xs ys)"
| Empty: "composePerm _ _= []"

lemma composePermInduct[consumes 1, case_names cBase cStep]:
  fixes xvec :: "name list"
  and   yvec :: "name list"
  and   P    :: "name list ⇒ name list ⇒ bool"

  assumes L: "length xvec = length yvec"
  and     rBase: "P [] []"
  and     rStep: "⋀x xvec y yvec. ⟦length xvec = length yvec; P xvec yvec⟧ ⟹ P (x # xvec) (y # yvec)"

  shows "P xvec yvec"
using assms
by(induct rule: composePerm.induct) auto

lemma composePermEqvt[eqvt]:
  fixes p    :: "name prm"
  and   xvec :: "name list"
  and   yvec :: "name list"

  shows "(p ∙ (composePerm xvec yvec)) = composePerm (p ∙ xvec) (p ∙ yvec)"
by(induct xvec yvec rule: composePerm.induct) auto

abbreviation
  composePermJudge (‹[_ _] ∙⇩v _› [80, 80, 80] 80) where "[xvec yvec] ∙⇩v p ≡ (composePerm xvec yvec) ∙ p"

abbreviation
  composePermInvJudge (‹[_ _]⇧- ∙⇩v _› [80, 80, 80] 80) where "[xvec yvec]⇧- ∙⇩v p ≡ (rev (composePerm xvec yvec)) ∙ p"

lemma permChainSimps[simp]:
  fixes xvec :: "name list"
  and   yvec :: "name list"
  and   perm :: "name prm"
  and   p    :: "'a::pt_name"

  shows "((composePerm xvec yvec) @ perm) ∙ p = [xvec yvec] ∙⇩v (perm ∙ p)"
by(simp add: pt2[OF pt_name_inst])

lemma permChainEqvt[eqvt]:
  fixes p    :: "name prm"
  and   xvec :: "name list"
  and   yvec :: "name list"
  and   x    :: "'a::pt_name"

  shows "(p ∙ ([xvec yvec] ∙⇩v x)) = [(p ∙ xvec) (p ∙ yvec)] ∙⇩v (p ∙ x)"
  and   "(p ∙ ([xvec yvec]⇧- ∙⇩v x)) = [(p ∙ xvec) (p ∙ yvec)]⇧- ∙⇩v (p ∙ x)"
by(subst pt_perm_compose[OF pt_name_inst, OF at_name_inst], simp add: eqvts rev_eqvt)+

lemma permChainBij:
  fixes xvec :: "name list"
  and   yvec :: "name list"
  and   p    :: "'a::pt_name"
  and   q    :: "'a::pt_name"

  assumes "length xvec = length yvec"

  shows "(([xvec yvec] ∙⇩v p) = ([xvec yvec] ∙⇩v q)) = (p = q)"
  and   "(([xvec yvec]⇧- ∙⇩v p) = ([xvec yvec]⇧- ∙⇩v q)) = (p = q)"
using assms
by(induct rule: composePermInduct)
  (auto simp add: pt_bij[OF pt_name_inst, OF at_name_inst])

lemma permChainAppend:
  fixes xvec1 :: "name list"
  and   yvec1 :: "name list"
  and   xvec2 :: "name list"
  and   yvec2 :: "name list"
  and   p     :: "'a::pt_name"
  
  assumes "length xvec1 = length yvec1"

  shows "([(xvec1@xvec2) (yvec1@yvec2)] ∙⇩v p) = [xvec1 yvec1] ∙⇩v [xvec2 yvec2] ∙⇩v p"
  and   "([(xvec1@xvec2) (yvec1@yvec2)]⇧- ∙⇩v p) = [xvec2 yvec2]⇧- ∙⇩v [xvec1 yvec1]⇧- ∙⇩v p"
using assms
by(induct arbitrary: p rule: composePermInduct, auto) (simp add: pt2[OF pt_name_inst])

lemma calcChainAtom:
  fixes xvec :: "name list"
  and   yvec :: "name list"
  and   x    :: name

  assumes "length xvec = length yvec"
  and     "x ♯ xvec"
  and     "x ♯ yvec"

  shows "[xvec yvec] ∙⇩v x = x"
using assms
by(induct rule: composePermInduct, auto)

lemma calcChainAtomRev:
  fixes xvec :: "name list"
  and   yvec :: "name list"
  and   x    :: name

  assumes "length xvec = length yvec"
  and     "x ♯ xvec"
  and     "x ♯ yvec"

  shows "[xvec yvec]⇧- ∙⇩v x = x"
using assms
by(induct rule: composePermInduct, auto)
  (auto simp add: pt2[OF pt_name_inst] fresh_list_cons calc_atm)

lemma permChainFresh[simp]:
  fixes x    :: name
  and   xvec :: "name list"
  and   yvec :: "name list"
  and   p    :: "'a::pt_name"

  assumes "x ♯ xvec"
  and     "x ♯ yvec"
  and     "length xvec = length yvec"

  shows "x ♯ [xvec yvec] ∙⇩v p = x ♯ p"
  and   "x ♯ [xvec yvec]⇧- ∙⇩v p = x ♯ p"
using assms
by(auto simp add: fresh_left calcChainAtomRev calcChainAtom)

lemma chainFreshFresh:
  fixes x    :: name
  and   y    :: name
  and   xvec :: "name list"
  and   p    :: "'a::pt_name"

  assumes "x ♯ xvec"
  and     "y ♯ xvec"

  shows "xvec ♯* ([(x, y)] ∙ p) = (xvec ♯* p)"
using assms
by(induct xvec) (auto simp add: fresh_list_cons fresh_left)

lemma permChainFreshFresh:
  fixes xvec :: "name list"
  and   yvec :: "name list"
  and   p    :: "'a::pt_name"

  assumes "xvec ♯* p"
  and     "yvec ♯* p"
  and     "length xvec = length yvec"

  shows "[xvec yvec] ∙⇩v p = p"
  and   "[xvec yvec]⇧- ∙⇩v p = p"
using assms
by(induct rule: composePerm.induct, auto) (simp add: pt2[OF pt_name_inst])

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

  shows "x ∉ set xvec = x ♯ xvec"
by(simp add: name_list_supp fresh_def)
  
lemma calcChain:
  fixes xvec :: "name list"
  and   yvec :: "name list"
  
  assumes "yvec ♯* xvec"
  and     "length xvec = length yvec"
  and     "distinct xvec"
  and     "distinct yvec"

  shows "[xvec yvec] ∙⇩v xvec = yvec"
using assms
by(induct xvec yvec rule: composePerm.induct, auto)
  (subst consPerm, simp add: calcChainAtom calc_atm name_list_supp fresh_def[symmetric])+

lemma freshChainPerm:
  fixes xvec :: "name list"
  and   yvec :: "name list"
  and   x    :: name
  and   C    :: "'a::pt_name"

  assumes "length xvec = length yvec"
  and     "yvec ♯* C"
  and     "xvec ♯* yvec"
  and     "x mem xvec"
  and     "distinct yvec"

  shows "x ♯ [xvec yvec] ∙⇩v C"
using assms
proof(induct rule: composePermInduct)
  case cBase
  have "x mem []" by fact
  hence False by simp
  thus ?case by simp
next
  case(cStep x' xvec y yvec)
  have "(y # yvec) ♯* C" by fact
  hence yFreshC: "y ♯ C" and yvecFreshp: "yvec ♯* C" by simp+
  have "(x' # xvec) ♯* (y # yvec)" by fact
  hence x'ineqy: "x' ≠ y" and xvecFreshyvec: "xvec ♯* yvec"
    and x'Freshyvec: "x' ♯ yvec" and yFreshxvec: "y ♯ xvec"
    by(auto simp add: fresh_list_cons)
  have "distinct (y#yvec)" by fact
  hence yFreshyvec: "y ♯ yvec" and yvecDist: "distinct yvec"
    by simp+
  have L: "length xvec = length yvec" by fact
  have "x ♯ [(x', y)] ∙ [xvec yvec] ∙⇩v C"
  proof(case_tac "x = x'")
    assume xeqx': "x = x'"
    moreover from yFreshxvec yFreshyvec yFreshC L have "y ♯ [xvec yvec] ∙⇩v C"
      by simp
    hence "([(x, y)] ∙ y) ♯ [(x, y)] ∙ [xvec yvec] ∙⇩v C"
      by(rule pt_fresh_bij1[OF pt_name_inst, OF at_name_inst])
    with x'ineqy xeqx' show ?thesis by(simp add: calc_atm)
  next
    assume xineqx': "x ≠ x'"
    have "x mem (x' # xvec)" by fact
    with xineqx' have xmemxvec: "x mem xvec" by simp
    moreover have "⟦yvec ♯* C; xvec ♯* yvec; x mem xvec; distinct yvec⟧ ⟹ x ♯ [xvec yvec] ∙⇩v C" by fact
    ultimately have "x ♯ [xvec yvec] ∙⇩v C" using yvecFreshp xvecFreshyvec yvecDist
      by simp
    hence "([(x', y)] ∙ x) ♯ [(x', y)] ∙ [xvec yvec] ∙⇩v C"
      by(rule pt_fresh_bij1[OF pt_name_inst, OF at_name_inst])
    moreover from xmemxvec yFreshxvec have "x ≠ y"
      by(induct xvec) (auto simp add: fresh_list_cons)
    ultimately show ?thesis using xineqx' x'ineqy by(simp add: calc_atm)
  qed
  thus ?case by simp
qed

lemma memFreshSimp[simp]:
  fixes y    :: name
  and   yvec :: "name list"

  shows "(¬(y mem yvec)) = y ♯ yvec"
by(induct yvec)
  (auto simp add: fresh_list_nil fresh_list_cons)

lemma freshChainPerm':
  fixes xvec :: "name list"
  and   yvec :: "name list"
  and   p    :: "'a::pt_name"

  assumes "length xvec = length yvec"
  and     "yvec ♯* p"
  and     "xvec ♯* yvec"
  and     "distinct yvec"

  shows "xvec ♯* ([xvec yvec] ∙⇩v p)"
using assms
proof(induct rule: composePermInduct)
  case cBase
  show ?case by simp
next
  case(cStep x xvec y yvec)
  have "(y # yvec) ♯* p" by fact
  hence yFreshp: "y ♯ p" and yvecFreshp: "yvec ♯* p"
    by simp+
  moreover have "(x # xvec) ♯* (y # yvec)" by fact
  hence xineqy: "x ≠ y" and xvecFreshyvec: "xvec ♯* yvec"
    and xFreshyvec: "x ♯ yvec" and yFreshxvec: "y ♯ xvec"
    by(auto simp add: fresh_list_cons)
  have "distinct (y # yvec)" by fact
  hence yFreshyvec: "y ♯ yvec" and yvecDist: "distinct yvec"
    by simp+
  have L: "length xvec = length yvec" by fact
  have "⟦yvec ♯* p; xvec ♯* yvec; distinct yvec⟧ ⟹ xvec ♯* ([xvec yvec] ∙⇩v p)" by fact
  with yvecFreshp xvecFreshyvec yvecDist have IH: "xvec ♯* ([xvec yvec] ∙⇩v p)" by simp
  show ?case
  proof(auto)
    from L yFreshp yvecFreshp xineqy xvecFreshyvec yvecDist yFreshyvec yFreshxvec xFreshyvec
    have "x ♯ [(x # xvec) (y # yvec)] ∙⇩v p"
      by(rule_tac freshChainPerm) (auto simp add: fresh_list_cons)
    thus "x ♯ [(x, y)] ∙ [xvec yvec] ∙⇩v p" by simp
  next
    show "xvec ♯* ([(x, y)] ∙ [xvec yvec] ∙⇩v p)"
    proof(case_tac "x mem xvec")
      assume "x mem xvec"
      with L yvecFreshp xvecFreshyvec yvecDist xFreshyvec
      have"x ♯ [xvec yvec] ∙⇩v p"
        by(rule_tac freshChainPerm) (auto simp add: fresh_list_cons)
      moreover from yFreshxvec yFreshyvec yFreshp L
      have "y ♯ [xvec yvec] ∙⇩v p" by simp
      ultimately show ?thesis using IH
        by(subst consPerm) (simp add: perm_fresh_fresh)
    next
      assume "¬(x mem xvec)"
      hence xFreshxvec: "x ♯ xvec" by simp
      from IH have "([(x, y)] ∙ xvec) ♯* ([(x, y)] ∙ [xvec yvec] ∙⇩v p)"
        by(simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
      with xFreshxvec yFreshxvec show ?thesis by simp
    qed
  qed
qed

lemma permSym:
  fixes x    :: name
  and   y    :: name
  and   xvec :: "name list"
  and   yvec :: "name list"
  and   p    :: "'a::pt_name"
  
  assumes "x ♯ xvec"
  and     "x ♯ yvec"
  and     "y ♯ xvec"
  and     "y ♯ yvec"
  and     "length xvec = length yvec"

  shows "([(x, y)] ∙ [xvec yvec] ∙⇩v p) = [xvec yvec] ∙⇩v [(x, y)] ∙ p"
using assms
apply(induct rule: composePerm.induct, auto)
by(subst pt_perm_compose[OF pt_name_inst, OF at_name_inst]) simp

lemma distinctPermClosed[simp]:
  fixes p :: "name prm"
  and   q :: "name prm"

  assumes "distinctPerm p"

  shows "distinctPerm(q ∙ p)"
using assms
by(induct p) (auto simp add: pt_fresh_bij[OF pt_name_inst, OF at_name_inst] dest: pt_bij4[OF pt_name_inst, OF at_name_inst])

lemma freshStarSimps:
  fixes x  :: name
  and   Xs :: "name set"
  and   Ys :: "name set"
  and   C  :: "'a::fs_name"
  and   p  :: "name prm"
  
  assumes "set p ⊆ Xs × Ys"
  and     "Xs ♯* x"
  and     "Ys ♯* x"

  shows "x ♯ (p ∙ C) = x ♯ C"
using assms
by(subst  pt_fresh_bij[OF pt_name_inst, OF at_name_inst, symmetric, of _ C p]) simp

lemma freshStarChainSimps:
  fixes xvec :: "name list"
  and   Xs   :: "name set"
  and   Ys   :: "name set"
  and   C    :: "'a::fs_name"
  and   p    :: "name prm"

  assumes "set p ⊆ Xs × Ys"
  and     "Xs ♯* xvec"
  and     "Ys ♯* xvec"

  shows   "xvec ♯* (p ∙ C) = xvec ♯* C"
using assms
by(induct xvec) (auto simp add: freshStarSimps)

lemma permStarFresh:
  fixes xvec :: "name list"
  and   p    :: "name prm"
  and   T    :: "'a::pt_name"

  assumes "xvec ♯* p"

  shows "xvec ♯* (p ∙ T) = xvec ♯* T"
using assms
by(induct p) (auto simp add: chainFreshFresh)

lemma swapStarFresh:
  fixes x :: name
  and   p :: "name prm"
  and   T :: "'a::pt_name"

  assumes "x ♯ p"

  shows "x ♯ (p ∙ T) = x ♯ T"
proof -
  from assms have "[x] ♯* (p ∙ T) = [x] ♯* T"
    by(rule_tac permStarFresh) auto
  thus ?thesis by simp
qed

lemmas freshChainSimps = freshStarSimps freshStarChainSimps permStarFresh swapStarFresh chainFreshFresh freshPerm subsetFresh

lemma freshAlphaPerm:
  fixes xvec :: "name list"
  and   Xs   :: "name set"
  and   Ys   :: "name set"
  and   p    :: "name prm"

  assumes S: "set p ⊆ Xs × Ys"
  and     "Xs ♯* xvec"
  and     "Ys ♯* xvec"

  shows "xvec ♯* p"
using assms
apply(induct p)
by auto (simp add: fresh_star_def fresh_def name_list_supp supp_list_nil)+

lemma freshAlphaSwap:
  fixes x  :: name
  and   Xs :: "name set"
  and   Ys :: "name set"
  and   p  :: "name prm"

  assumes S: "set p ⊆ Xs × Ys"
  and     "Xs ♯* x"
  and     "Ys ♯* x"

  shows "x ♯ p"
proof -
  from assms have "[x] ♯* p" 
    apply(rule_tac freshAlphaPerm)
    apply assumption
    by auto
  thus ?thesis by simp
qed

lemma setToListFresh[simp]:
  fixes xvec :: "name list"
  and   C    :: "'a::fs_name"
  and   yvec :: "name list"
  and   Xs   :: "name set"
  and   x    :: name

  shows "xvec ♯* (set yvec) = xvec ♯* yvec"
  and   "Xs ♯* (set yvec) = Xs ♯* yvec"
  and   "x ♯ (set yvec) = x ♯ yvec"
  and   "set xvec ♯* Xs = xvec ♯* Xs"
by(auto simp add: fresh_star_def name_list_supp fresh_def fs_name1 at_fin_set_supp[OF at_name_inst])

end