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(pi2Xs)"
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   pi1Xs = pi2Xs"
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 = {}  (piXs=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 = {}  piXs = 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: "xXs" 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 "(((pix,y)#pi)(insert x Xs)) = {y}Ys"
  proof -
    have eq: "[(pix,y)]Ys = Ys" 
    proof -
      have "(pix)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 "yYs" using e by simp
      ultimately show "[(pix,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 "(((pix,y)#pi)({x}Xs)) = ([(pix,y)](pi({x}Xs)))"
      by (simp add: pt2[symmetric, OF pt_set_inst, OF at_pt_inst[OF at], OF at])
    also have " = {y}([(pix,y)](piXs))" 
      by (simp only: union_eqvt perm_set_def at_calc[OF at])(auto)
    also have " = {y}([(pix,y)]Ys)" using a3 by simp
    also have " = {y}Ys" using eq by simp
    finally show "(((pix,y)#pi)(insert x Xs)) = {y}Ys" by auto
  qed
  moreover
  have "pix=x" using a4 b a2 a3 d3 by (rule_tac at_prm_fresh2[OF at]) (auto)
  then have "set ((pix,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