Session Psi_Calculi

Theory 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

Theory 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

Theory 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

Theory Frame

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

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

  shows "length(p  xvec) = length xvec"
by(induct xvec) auto

nominal_datatype 'assertion frame =
    FAssert "'assertion::fs_name"
  | FRes "«name» ('assertion frame)" ("⦇ν__" [80, 80] 80)

primrec frameResChain :: "name list  ('a::fs_name) frame  'a frame" where
  base: "frameResChain [] F = F"
| step: "frameResChain (x#xs) F = ⦇νx(frameResChain xs F)"

notation frameResChain ("⦇ν*__" [80, 80] 80)
notation FAssert  ("⟨ε, _" [80] 80)
abbreviation FAssertJudge ("_, _" [80, 80] 80) where "AF, ΨF  frameResChain AF (FAssert ΨF)"

lemma frameResChainEqvt[eqvt]:
  fixes perm :: "name prm"
  and   lst  :: "name list"
  and   F    :: "'a::fs_name frame"
  
  shows "perm  (⦇ν*xvecF) = ⦇ν*(perm  xvec)(perm  F)"
by(induct_tac xvec, auto)

lemma frameResChainFresh: 
  fixes x    :: name
  and   xvec :: "name list"
  and   F    :: "'a::fs_name frame"

  shows "x  ⦇ν*xvecF = (x  set xvec  x  F)"
by (induct xvec) (simp_all add: abs_fresh)

lemma frameResChainFreshSet: 
  fixes Xs   :: "name set"
  and   xvec :: "name list"
  and   F    :: "'a::fs_name frame"

  shows "Xs ♯* (⦇ν*xvecF) = (xXs. x  set xvec  x  F)"
by (simp add: fresh_star_def frameResChainFresh)

lemma frameChainAlpha:
  fixes p    :: "name prm"
  and   xvec :: "name list"
  and   F    :: "'a::fs_name frame"

  assumes xvecFreshF: "(p  xvec) ♯* F"
  and     S: "set p  set xvec × set (p  xvec)"

  shows "⦇ν*xvecF = ⦇ν*(p  xvec)(p  F)"
proof -
  note pt_name_inst at_name_inst S
  moreover have "set xvec ♯* (⦇ν*xvecF)"
    by (simp add: frameResChainFreshSet)
  moreover from xvecFreshF have "set (p  xvec) ♯* (⦇ν*xvecF)"
    by (simp add: frameResChainFreshSet) (simp add: fresh_star_def)
  ultimately have "⦇ν*xvecF = p  (⦇ν*xvecF)"
    by (rule_tac pt_freshs_freshs [symmetric])
  then show ?thesis by(simp add: eqvts)
qed

lemma frameChainAlpha':
  fixes p    :: "name prm"
  and   AP   :: "name list"
  and   ΨP  :: "'a::fs_name"

  assumes "(p  AP) ♯* ΨP"
  and     S: "set p  set AP × set (p  AP)"

  shows "AP, ΨP = (p  AP), p  ΨP"
using assms
by(subst frameChainAlpha) (auto simp add: fresh_star_def)

lemma alphaFrameRes:
  fixes x :: name
  and   F :: "'a::fs_name frame"
  and   y :: name

  assumes "y  F"

  shows "⦇νxF = ⦇νy([(x, y)]  F)"
proof(cases "x = y")
  assume "x=y"
  thus ?thesis by simp
next
  assume "x  y"
  with y  F show ?thesis
    by(perm_simp add: frame.inject alpha calc_atm fresh_left)
qed

lemma frameChainAppend:
  fixes xvec :: "name list"
  and   yvec :: "name list"
  and   F    :: "'a::fs_name frame"
  
  shows "⦇ν*(xvec@yvec)F = ⦇ν*xvec(⦇ν*yvecF)"
by(induct xvec) auto

lemma frameChainEqLength:
  fixes xvec :: "name list"
  and   Ψ    :: "'a::fs_name"
  and   yvec :: "name list"
  and   Ψ'   :: "'a::fs_name"

  assumes "xvec, Ψ = yvec, Ψ'"

  shows "length xvec = length yvec"
proof -
  obtain n where "n = length xvec" by auto
  with assms show ?thesis
  proof(induct n arbitrary: xvec yvec Ψ Ψ')
    case(0 xvec yvec Ψ Ψ')
    from 0 = length xvec have "xvec = []" by auto
    moreover with xvec, Ψ = yvec, Ψ' have "yvec = []"
      by(case_tac yvec) auto
    ultimately show ?case by simp
  next
    case(Suc n xvec yvec Ψ Ψ')
    from ‹Suc n = length xvec
    obtain x xvec' where "xvec = x#xvec'" and "length xvec' = n"
      by(case_tac xvec) auto
    from xvec, Ψ = yvec, Ψ' xvec = x # xvec'
    obtain y yvec' where "(x#xvec'), Ψ = (y#yvec'), Ψ'"
      and "yvec = y#yvec'"
      by(case_tac yvec) auto
    hence EQ: "⦇νx⦇ν*xvec'(FAssert Ψ) = ⦇νy⦇ν*yvec'(FAssert Ψ')"
      by simp
    have IH: "xvec yvec Ψ Ψ'. xvec, (Ψ::'a) = yvec, (Ψ'::'a); n = length xvec  length xvec = length yvec"
      by fact
    show ?case
    proof(case_tac "x = y")
      assume "x = y"
      with EQ have "xvec', Ψ = yvec', Ψ'"
        by(simp add: alpha frame.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 "xvec', Ψ = [(x, y)]  yvec', Ψ'"
        by(simp add: alpha frame.inject)
      hence "xvec', Ψ = ([(x, y)]  yvec'), ([(x, y)]  Ψ')"
        by(simp add: 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 frameEqFresh:
  fixes F :: "('a::fs_name) frame"
  and   G :: "'a frame"
  and   x :: name
  and   y :: name

  assumes "⦇νxF = ⦇νyG"
  and     "x  F"
  
  shows "y  G"
using assms
by(auto simp add: frame.inject alpha fresh_left calc_atm)  

lemma frameEqSupp:
  fixes F :: "('a::fs_name) frame"
  and   G :: "'a frame"
  and   x :: name
  and   y :: name

  assumes "⦇νxF = ⦇νyG"
  and     "x  supp F"
  
  shows "y  supp G"
using assms
apply(auto simp add: frame.inject alpha fresh_left calc_atm)
apply(drule_tac pi="[(x, y)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
by(simp add: eqvts calc_atm)

lemma frameChainEqSuppEmpty[dest]:
  fixes xvec :: "name list"
  and   Ψ    :: "'a::fs_name"
  and   yvec :: "name list"
  and   Ψ'   :: "'a::fs_name"

  assumes "xvec, Ψ = yvec, Ψ'"
  and     "supp Ψ = ({}::name set)"

  shows "Ψ = Ψ'"
proof -
  obtain n where "n = length xvec" by auto
  with assms show ?thesis
  proof(induct n arbitrary: xvec yvec Ψ Ψ')
    case(0 xvec yvec Ψ Ψ')
    from 0 = length xvec have "xvec = []" by auto
    moreover with xvec, Ψ = yvec, Ψ' have "yvec = []"
      by(case_tac yvec) auto
    ultimately show ?case  using xvec, Ψ = yvec, Ψ'
      by(simp add: frame.inject) 
  next
    case(Suc n xvec yvec Ψ Ψ')
    from ‹Suc n = length xvec
    obtain x xvec' where "xvec = x#xvec'" and "length xvec' = n"
      by(case_tac xvec) auto
    from xvec, Ψ = yvec, Ψ' xvec = x # xvec'
    obtain y yvec' where "(x#xvec'), Ψ = (y#yvec'), Ψ'"
      and "yvec = y#yvec'"
      by(case_tac yvec) auto
    hence EQ: "⦇νx⦇ν*xvec'(FAssert Ψ) = ⦇νy⦇ν*yvec'(FAssert Ψ')"
      by simp
    have IH: "xvec yvec Ψ Ψ'. xvec, (Ψ::'a) = yvec, (Ψ'::'a); supp Ψ = ({}::name set); n = length xvec  Ψ = Ψ'"
      by fact
    show ?case
    proof(case_tac "x = y")
      assume "x = y"
      with EQ have "xvec', Ψ = yvec', Ψ'"
        by(simp add: alpha frame.inject)
      with IH ‹length xvec' = n ‹supp Ψ = {} show ?case
        by simp
    next
      assume "x  y"
      with EQ have "xvec', Ψ = [(x, y)]  yvec', Ψ'"
        by(simp add: alpha frame.inject)
      hence "xvec', Ψ = ([(x, y)]  yvec'), ([(x, y)]  Ψ')"
        by(simp add: eqvts)
      with IH ‹length xvec' = n ‹supp Ψ = {} have "Ψ = [(x, y)]  Ψ'"
        by(simp add: eqvts)
      moreover with ‹supp Ψ = {} have "supp([(x, y)]  Ψ') = ({}::name set)"
        by simp
      hence "x  ([(x, y)]  Ψ')" and "y  ([(x, y)]  Ψ')"
        by(simp add: fresh_def)+
      with x  y have "x  Ψ'" and "y  Ψ'"
        by(simp add: fresh_left calc_atm)+
      ultimately show ?case by simp
    qed
  qed
qed

lemma frameChainEq:
  fixes xvec :: "name list"
  and   Ψ    :: "'a::fs_name"
  and   yvec :: "name list"
  and   Ψ'   :: "'a::fs_name"

  assumes "xvec, Ψ = yvec, Ψ'"
  and     "xvec ♯* yvec"

  obtains p where "(set p)  (set xvec) × set (yvec)" and "distinctPerm p" and "Ψ' = p  Ψ"
proof -
  assume "p. set p  set xvec × set yvec; distinctPerm p; Ψ' = p  Ψ  thesis"
  moreover obtain n where "n = length xvec" by auto
  with assms have "p. (set p)  (set xvec) × set (yvec)  distinctPerm p   Ψ' = p  Ψ"
  proof(induct n arbitrary: xvec yvec Ψ Ψ')
    case(0 xvec yvec Ψ Ψ')
    have Eq: "xvec, Ψ = yvec, Ψ'" 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: frame.inject)
  next
    case(Suc n xvec yvec Ψ Ψ')
    from ‹Suc n = length xvec
    obtain x xvec' where "xvec = x#xvec'" and "length xvec' = n"
      by(case_tac xvec) auto
    from xvec, Ψ = yvec, Ψ' xvec = x # xvec'
    obtain y yvec' where "(x#xvec'), Ψ = (y#yvec'), Ψ'"
      and "yvec = y#yvec'"
      by(case_tac yvec) auto
    hence EQ: "⦇νx⦇ν*xvec'(FAssert Ψ) = ⦇νy⦇ν*yvec'(FAssert Ψ')"
      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
    have IH: "xvec yvec Ψ Ψ'. xvec, (Ψ::'a) = yvec, (Ψ'::'a); xvec ♯* yvec; n = length xvec 
                                 p. (set p)  (set xvec) × (set yvec)  distinctPerm p   Ψ' = p  Ψ"
      by fact

    from EQ x  y have EQ': "xvec', Ψ = ([(x, y)]  yvec', Ψ')" 
                     and xFreshΨ': "x  ⦇ν*yvec'(FAssert Ψ')"
      by(simp add: frame.inject alpha)+

    show ?case
    proof(case_tac "x  xvec', Ψ")
      assume "x  xvec', Ψ"
      with EQ have "y  yvec', Ψ'"
        by(rule frameEqFresh)
      with xFreshΨ' EQ' have "xvec', Ψ = yvec', Ψ'" 
        by(simp)
      with xvec' ♯* yvec' ‹length xvec' = n IH
      obtain p where S: "(set p)  (set xvec') × (set yvec')" and "distinctPerm p"  and "Ψ' = p  Ψ"
        by blast
      from S have "(set p)  set(x#xvec') × set(y#yvec')" by auto
      with xvec = x#xvec' yvec=y#yvec' ‹distinctPerm p Ψ' = p  Ψ
      show ?case by blast
    next
      assume "¬(x  ⦇ν*xvec'(FAssert Ψ))"
      hence xSuppΨ: "x  supp(xvec', Ψ)"
        by(simp add: fresh_def)
      with EQ have "y  supp (yvec', Ψ')"
        by(rule frameEqSupp)
      hence "y  yvec'"
        by(induct yvec') (auto simp add: frame.supp abs_supp)      
      with x  yvec' EQ' have "xvec', Ψ = yvec', ([(x, y)]  Ψ')"
        by(simp add: eqvts)
      with  xvec' ♯* yvec' ‹length xvec' = n IH
      obtain p where S: "(set p)  (set xvec') × (set yvec')" and "distinctPerm p" and "([(x, y)]  Ψ') = p  Ψ"
        by blast

      from xSuppΨ have "x  xvec'"
        by(induct xvec') (auto simp add: frame.supp abs_supp)      
      with x  yvec' y  xvec' y  yvec' S have "x  p" and "y  p"
        apply(induct p)
        by(auto simp add: name_list_supp) (auto simp add: fresh_def) 
      from S have "(set ((x, y)#p))  (set(x#xvec')) × (set(y#yvec'))"
        by force
      moreover from x  y x  p y  p S ‹distinctPerm p
      have "distinctPerm((x,y)#p)" by simp
      moreover from x  p y  p x  xvec' y  xvec' have "y#(p  xvec') = ((x, y)#p)  (x#xvec')" 
        by(simp add: eqvts calc_atm freshChainSimps)
      moreover from ([(x, y)]  Ψ') = p  Ψ
      have "([(x, y)]  [(x, y)]  Ψ') = [(x, y)]  p  Ψ"
        by(simp add: pt_bij)
      hence "Ψ' = ((x, y)#p)  Ψ" by simp
      ultimately show ?case using xvec=x#xvec' yvec=y#yvec'
        by blast
    qed
  qed
  ultimately show ?thesis by blast
qed
(*
lemma frameChainEq'':
  fixes xvec :: "name list"
  and   Ψ    :: "'a::fs_name"
  and   yvec :: "name list"
  and   Ψ'   :: "'a::fs_name"

  assumes "⟨xvec, Ψ⟩ = ⟨yvec, Ψ'⟩"

  obtains p where "(set p) ⊆ (set xvec) × set (yvec)" and "Ψ' = p ∙ Ψ"
proof -
  assume "⋀p. ⟦set p ⊆ set xvec × set yvec; Ψ' = p ∙ Ψ⟧ ⟹ thesis"
  moreover obtain n where "n = length xvec" by auto
  with assms have "∃p. (set p) ⊆ (set xvec) × set (yvec) ∧ Ψ' = p ∙ Ψ"
  proof(induct n arbitrary: xvec yvec Ψ Ψ')
    case(0 xvec yvec Ψ Ψ')
    have Eq: "⟨xvec, Ψ⟩ = ⟨yvec, Ψ'⟩" 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: frame.inject)
  next
    case(Suc n xvec yvec Ψ Ψ')
    from `Suc n = length xvec`
    obtain x xvec' where "xvec = x#xvec'" and "length xvec' = n"
      by(case_tac xvec) auto
    from `⟨xvec, Ψ⟩ = ⟨yvec, Ψ'⟩` `xvec = x # xvec'`
    obtain y yvec' where "⟨(x#xvec'), Ψ⟩ = ⟨(y#yvec'), Ψ'⟩"
      and "yvec = y#yvec'"
      by(case_tac yvec) auto
    hence EQ: "⦇νx⦈⦇ν*xvec'⦈(FAssert Ψ) = ⦇νy⦈⦇ν*yvec'⦈(FAssert Ψ')"
      by simp
    have IH: "⋀xvec yvec Ψ Ψ'. ⟦⟨xvec, (Ψ::'a)⟩ = ⟨yvec, (Ψ'::'a)⟩; n = length xvec⟧ ⟹
                                 ∃p. (set p) ⊆ (set xvec) × (set yvec) ∧ Ψ' = p ∙ Ψ"
      by fact
    show ?case
    proof(cases "x=y")
      case True
      from EQ `x = y` have "⟨xvec', Ψ⟩ = ⟨yvec', Ψ'⟩" by(simp add: alpha frame.inject)
      then obtain p where S: "set p ⊆ set xvec' × set yvec'" and "Ψ' = p ∙ Ψ" using `length xvec' = n` IH
        by blast
      from S have "set((x, y)#p) ⊆ set(x#xvec') × set (y#yvec')" by auto
      moreover from `x = y` `Ψ' = p ∙ Ψ` have "Ψ' = ((x, y)#p) ∙ Ψ" by auto
      ultimately show ?thesis using `xvec = x#xvec'` `yvec = y#yvec'` by blast
    next
      case False
      from EQ `x ≠ y` have EQ': "⟨xvec', Ψ⟩ = ([(x, y)] ∙ ⟨yvec', Ψ'⟩)" 
                       and xFreshΨ': "x ♯ ⦇ν*yvec'⦈(FAssert Ψ')"
        by(simp add: frame.inject alpha)+
    
      show ?thesis
      proof(cases "x ♯ ⟨xvec', Ψ⟩")
        case True
        from EQ `x ♯ ⟨xvec', Ψ⟩` have "y ♯ ⟨yvec', Ψ'⟩"
          by(rule frameEqFresh)
        with xFreshΨ' EQ' have "⟨xvec', Ψ⟩ = ⟨yvec', Ψ'⟩" 
          by(simp)
        with `length xvec' = n` IH
        obtain p where S: "(set p) ⊆ (set xvec') × (set yvec')" and "Ψ' = p ∙ Ψ"
          by blast
        from S have "(set p) ⊆ set(x#xvec') × set(y#yvec')" by auto
        with `xvec = x#xvec'` `yvec=y#yvec'` `Ψ' = p ∙ Ψ`
        show ?thesis by blast
      next
        case False
        from `¬(x ♯ ⦇ν*xvec'⦈(FAssert Ψ))` have xSuppΨ: "x ∈ supp(⟨xvec', Ψ⟩)"
          by(simp add: fresh_def)
        with EQ have "y ∈ supp (⟨yvec', Ψ'⟩)"
          by(rule frameEqSupp)
        hence "y ♯ yvec'"
          by(induct yvec') (auto simp add: frame.supp abs_supp)

        with `x ♯ yvec'` EQ' have "⟨xvec', Ψ⟩ = ⟨yvec', ([(x, y)] ∙ Ψ')⟩"
          by(simp add: eqvts)
        with  `xvec' ♯* yvec'` `length xvec' = n` IH
        obtain p where S: "(set p) ⊆ (set xvec') × (set yvec')" and "distinctPerm p" and "([(x, y)] ∙ Ψ') = p ∙ Ψ"
          by blast
        
        from xSuppΨ have "x ♯ xvec'"
          by(induct xvec') (auto simp add: frame.supp abs_supp)      
        with `x ♯ yvec'` `y ♯ xvec'` `y ♯ yvec'` S have "x ♯ p" and "y ♯ p"
          apply(induct p)
          by(auto simp add: name_list_supp) (auto simp add: fresh_def) 
        from S have "(set ((x, y)#p)) ⊆ (set(x#xvec')) × (set(y#yvec'))"
          by force
        moreover from `x ≠ y` `x ♯ p` `y ♯ p` S `distinctPerm p`
        have "distinctPerm((x,y)#p)" by simp
        moreover from `x ♯ p` `y ♯ p` `x ♯ xvec'` `y ♯ xvec'` have "y#(p ∙ xvec') = ((x, y)#p) ∙ (x#xvec')" 
          by(simp add: eqvts calc_atm freshChainSimps)
        moreover from `([(x, y)] ∙ Ψ') = p ∙ Ψ`
        have "([(x, y)] ∙ [(x, y)] ∙ Ψ') = [(x, y)] ∙ p ∙ Ψ"
          by(simp add: pt_bij)
        hence "Ψ' = ((x, y)#p) ∙ Ψ" by simp
        ultimately show ?case using `xvec=x#xvec'` `yvec=y#yvec'`
          by blast
      qed
    qed
    ultimately show ?thesis by blast
qed
*)
lemma frameChainEq':
  fixes xvec :: "name list"
  and   Ψ    :: "'a::fs_name"
  and   yvec :: "name list"
  and   Ψ'   :: "'a::fs_name"

  assumes "xvec, Ψ = yvec, Ψ'"
  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 "Ψ' = p  Ψ"
proof -
  assume "p. set p  set xvec × set (p  xvec); distinctPerm p; yvec = p  xvec; Ψ' = 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  Ψ' = p  Ψ"
  proof(induct n arbitrary: xvec yvec Ψ Ψ')
    case(0 xvec yvec Ψ Ψ')
    have Eq: "xvec, Ψ = yvec, Ψ'" 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: frame.inject)
  next
    case(Suc n xvec yvec Ψ Ψ')
    from ‹Suc n = length xvec
    obtain x xvec' where "xvec = x#xvec'" and "length xvec' = n"
      by(case_tac xvec) auto
    from xvec, Ψ = yvec, Ψ' xvec = x # xvec'
    obtain y yvec' where "(x#xvec'), Ψ = (y#yvec'), Ψ'"
      and "yvec = y#yvec'"
      by(case_tac yvec) auto
    hence EQ: "⦇νx⦇ν*xvec'(FAssert Ψ) = ⦇νy⦇ν*yvec'(FAssert Ψ')"
      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
    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 Ψ Ψ'. xvec, (Ψ::'a) = yvec, (Ψ'::'a); xvec ♯* yvec; distinct xvec; distinct yvec; n = length xvec  p. (set p)  (set xvec) × (set yvec)  distinctPerm p   yvec = p  xvec  Ψ' = p  Ψ"
      by fact
    from EQ x  y  x  yvec' y  yvec' have "xvec', Ψ = yvec', ([(x, y)]  Ψ')"
      by(simp add: frame.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)]  Ψ' = 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: 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: freshChainSimps calc_atm)
    moreover from ([(x, y)]  Ψ') = p  Ψ
    have "([(x, y)]  [(x, y)]  Ψ') = [(x, y)]  p  Ψ"
      by(simp add: pt_bij)
    hence "Ψ' = ((x, y)#p)  Ψ"
      by simp
    ultimately show ?case using xvec=x#xvec' yvec=y#yvec'
      by blast
  qed
  ultimately show ?thesis by blast
qed

lemma frameEq[simp]:
  fixes AF :: "name list"
  and   Ψ  :: "'a::fs_name"
  and   Ψ'  :: 'a

  shows "AF, Ψ = ⟨ε, Ψ' = (AF = []  Ψ = Ψ')"
  and   "⟨ε, Ψ' = AF, Ψ  = (AF = []  Ψ = Ψ')"
proof -
  {
    assume "AF, Ψ = ⟨ε, Ψ'"
    hence A: "AF, Ψ = [], Ψ'" by simp
    hence "length AF = length ([]::name list)"
      by(rule frameChainEqLength)
    with A have "AF = []" and "Ψ = Ψ'" by(auto simp add: frame.inject)
  }
  thus "AF, Ψ = ⟨ε, Ψ' = (AF = []  Ψ = Ψ')"
  and  "⟨ε, Ψ' = AF, Ψ  = (AF = []  Ψ = Ψ')"
    by auto
qed

lemma distinctFrame:
  fixes AF :: "name list"
  and   ΨF :: "'a::fs_name"
  and   C  :: "'b::fs_name"
  
  assumes "AF ♯* C"

  obtains AF' where  "AF, ΨF = AF', ΨF" and "distinct AF'" and "AF' ♯* C"
proof -
  assume "AF'. AF, ΨF = AF', ΨF; distinct AF'; AF' ♯* C  thesis"
  moreover from assms have "AF'. AF, ΨF = AF', ΨF  distinct AF'  AF' ♯* C"
  proof(induct AF)
    case Nil
    thus ?case by simp
  next
    case(Cons a AF)
    then obtain AF' where Eq: "AF, ΨF = AF', ΨF" and "distinct AF'" and "AF' ♯* C" by force
    from (a#AF) ♯* C have "a  C" and "AF ♯* C" by simp+
    show ?case
    proof(case_tac "a  AF', ΨF")
      assume "a  AF', ΨF"
      obtain b::name where "b  AF'" and "b  ΨF" and "b  C" by(generate_fresh "name", auto)
      have "(a#AF), ΨF = (b#AF'), ΨF"
      proof -
        from Eq have "(a#AF), ΨF = (a#AF'), ΨF" by(simp add: frame.inject)
        moreover from b  ΨF have " = ⦇νb([(a, b)]  ⦇ν*AF'(FAssert ΨF))"
          by(force intro: alphaFrameRes simp add: frameResChainFresh)
        ultimately show ?thesis using a  AF', ΨF b  ΨF
          by(simp add: frameResChainFresh)
      qed
      moreover from ‹distinct AF' b  AF' have "distinct(b#AF')" by simp
      moreover from AF' ♯* C b  C have "(b#AF') ♯* C" by simp+
      ultimately show ?case by blast
    next
      from Eq have "(a#AF), ΨF = (a#AF'), ΨF" by(simp add: frame.inject)
      moreover assume "¬(a  AF', ΨF)"
      hence "a  AF'" apply(simp add: fresh_def)
        by(induct AF') (auto simp add: supp_list_nil supp_list_cons supp_atm frame.supp abs_supp)
      with ‹distinct AF' have "distinct(a#AF')" by simp
      moreover from AF' ♯* C a  C have "(a#AF') ♯* C" by simp+
      ultimately show ?case by blast
    qed
  qed
  ultimately show ?thesis using AF ♯* C
    by blast
qed

lemma freshFrame:
  fixes F  :: "('a::fs_name) frame"
  and   C  :: "'b ::fs_name"

  obtains AF ΨF where "F = AF, ΨF" and "distinct AF" and "AF ♯* C"
proof -
  assume "AF ΨF. F = AF, ΨF; distinct AF; AF ♯* C  thesis"
  moreover have "AF ΨF. F = AF, ΨF  AF ♯* C"
  proof(nominal_induct F avoiding: C rule: frame.strong_induct)
    case(FAssert ΨF)
    have "FAssert ΨF = [], ΨF" by simp
    moreover have "([]::name list) ♯* C" by simp
    ultimately show ?case by force
  next
    case(FRes a F)
    from C. AF ΨF. F = AF, ΨF  AF ♯* C
    obtain AF ΨF  where "F = AF, ΨF" and "AF ♯* C"
      by blast
    with a  C have "⦇νaF = ⦇ν*(a#AF)(FAssert ΨF)" and "(a#AF) ♯* C"
      by simp+
    thus ?case by blast
  qed
  ultimately show ?thesis
    by(auto, rule_tac distinctFrame) auto
qed

locale assertionAux = 
  fixes SCompose :: "'b::fs_name  'b  'b"   (infixr "" 80)
  and   SImp     :: "'b  'c::fs_name  bool" ("_  _" [70, 70] 70)
  and   SBottom  :: 'b                         ("" 90) 
  and   SChanEq  :: "'a::fs_name  'a  'c"   ("_  _" [80, 80] 80)

  assumes statEqvt[eqvt]:   "p::name prm. p  (Ψ  Φ) = (p  Ψ)  (p  Φ)"
  and     statEqvt'[eqvt]:  "p::name prm. p  (Ψ  Ψ') = (p  Ψ)  (p  Ψ')" 
  and     statEqvt''[eqvt]: "p::name prm. p  (M  N) = (p  M)  (p  N)"
  and     permBottom[eqvt]: "p::name prm. (p  SBottom) = SBottom"

begin

lemma statClosed:
  fixes Ψ :: 'b
  and   φ :: 'c
  and   p :: "name prm"
  
  assumes "Ψ  φ"

  shows "(p  Ψ)  (p  φ)"
using assms statEqvt
by(simp add: perm_bool)

lemma compSupp:
  fixes Ψ  :: 'b
  and   Ψ' :: 'b

  shows "(supp(Ψ  Ψ')::name set)  ((supp Ψ)  (supp Ψ'))"
proof(auto simp add: eqvts supp_def)
  fix x::name
  let ?P = "λy. ([(x, y)]  Ψ)  [(x, y)]  Ψ'  Ψ  Ψ'"
  let ?Q = "λy Ψ. ([(x, y)]  Ψ)  Ψ"
  assume "finite {y. ?Q y Ψ'}"
  moreover assume "finite {y. ?Q y Ψ}" and "infinite {y. ?P(y)}"
  hence "infinite({y. ?P(y)} - {y. ?Q y Ψ})" by(rule Diff_infinite_finite)
  ultimately have "infinite(({y. ?P(y)} - {y. ?Q y Ψ}) - {y. ?Q y Ψ'})" by(rule Diff_infinite_finite)
  hence "infinite({y. ?P(y)  ¬(?Q y Ψ)  ¬ (?Q y Ψ')})" by(simp add: set_diff_eq)
  moreover have "{y. ?P(y)  ¬(?Q y Ψ)  ¬ (?Q y Ψ')} = {}" by auto
  ultimately have "infinite {}" by(drule_tac Infinite_cong) auto
  thus False by simp
qed

lemma chanEqSupp:
  fixes M :: 'a
  and   N :: 'a

  shows "(supp(M  N)::name set)  ((supp M)  (supp N))"
proof(auto simp add: eqvts supp_def)
  fix x::name
  let ?P = "λy. ([(x, y)]  M)  [(x, y)]  N  M  N"
  let ?Q = "λy M. ([(x, y)]  M)  M"
  assume "finite {y. ?Q y N}"
  moreover assume "finite {y. ?Q y M}" and "infinite {y. ?P(y)}"
  hence "infinite({y. ?P(y)} - {y. ?Q y M})" by(rule Diff_infinite_finite)
  ultimately have "infinite(({y. ?P(y)} - {y. ?Q y M}) - {y. ?Q y N})" by(rule Diff_infinite_finite)
  hence "infinite({y. ?P(y)  ¬(?Q y M)  ¬ (?Q y N)})" by(simp add: set_diff_eq)
  moreover have "{y. ?P(y)  ¬(?Q y M)  ¬ (?Q y N)} = {}" by auto
  ultimately have "infinite {}" by(drule_tac Infinite_cong) auto
  thus False by simp
qed

lemma freshComp[intro]:
  fixes x  :: name
  and   Ψ  :: 'b
  and   Ψ' :: 'b

  assumes "x  Ψ"
  and     "x  Ψ'"

  shows "x  Ψ  Ψ'"
using assms compSupp
by(auto simp add: fresh_def)

lemma freshCompChain[intro]:
  fixes xvec  :: "name list"
  and   Xs    :: "name set"
  and   Ψ     :: 'b
  and   Ψ'    :: 'b

  shows "xvec ♯* Ψ; xvec ♯* Ψ'  xvec ♯* (Ψ  Ψ')"
  and   "Xs ♯* Ψ; Xs ♯* Ψ'  Xs ♯* (Ψ  Ψ')"
by(auto simp add: fresh_star_def)

lemma freshChanEq[intro]:
  fixes x :: name
  and   M :: 'a
  and   N :: 'a

  assumes "x  M"
  and     "x  N"

  shows "x  M  N"
using assms chanEqSupp
by(auto simp add: fresh_def)

lemma freshChanEqChain[intro]:
  fixes xvec :: "name list"
  and   Xs   :: "name set"
  and   M    :: 'a
  and   N    :: 'a

  shows "xvec ♯* M; xvec ♯* N  xvec ♯* (M  N)"
  and   "Xs ♯* M; Xs ♯* N  Xs ♯* (M  N)"
by(auto simp add: fresh_star_def)

lemma suppBottom[simp]:
  shows "((supp SBottom)::name set) = {}"
by(auto simp add: supp_def permBottom)

lemma freshBottom[simp]:
  fixes x :: name
  
  shows "x  "
by(simp add: fresh_def)

lemma freshBottoChain[simp]:
  fixes xvec :: "name list"
  and   Xs   :: "name set"

  shows "xvec ♯* ()"
  and   "Xs   ♯* ()"
by(auto simp add: fresh_star_def)

lemma chanEqClosed:
  fixes Ψ :: 'b
  and   M :: 'a
  and   N :: 'a
  and   p :: "name prm"
 
  assumes "Ψ  M  N"

  shows "(p  Ψ)  (p  M)  (p  N)"
proof -
  from Ψ  M  N have "(p  Ψ)  p  (M  N)"
    by(rule statClosed)
  thus ?thesis by(simp add: eqvts)
qed

definition
  AssertionStatImp :: "'b  'b  bool" (infix "" 70)
  where "(Ψ  Ψ')  (Φ. Ψ  Φ  Ψ'  Φ)"

definition
  AssertionStatEq :: "'b  'b  bool" (infix "" 70)
  where "(Ψ  Ψ')  Ψ  Ψ'  Ψ'  Ψ"

lemma statImpEnt:
  fixes Ψ  :: 'b
  and   Ψ' :: 'b
  and   Φ  :: 'c

  assumes "Ψ  Ψ'"
  and     "Ψ  Φ"

  shows "Ψ'  Φ"
using assms
by(simp add: AssertionStatImp_def)

lemma statEqEnt:
  fixes Ψ  :: 'b
  and   Ψ' :: 'b
  and   Φ  :: 'c

  assumes "Ψ  Ψ'"
  and     "Ψ  Φ"

  shows "Ψ'  Φ"
using assms
by(auto simp add: AssertionStatEq_def intro: statImpEnt)

lemma AssertionStatImpClosed:
  fixes Ψ  :: 'b
  and   Ψ' :: 'b
  and   p  :: "name prm"

  assumes "Ψ  Ψ'"

  shows "(p  Ψ)  (p  Ψ')"
proof(auto simp add: AssertionStatImp_def)
  fix φ
  assume "(p  Ψ)  φ"
  hence "Ψ  rev p  φ" by(drule_tac p="rev p" in statClosed) auto
  with Ψ  Ψ' have "Ψ'  rev p  φ" by(simp add: AssertionStatImp_def)
  thus "(p  Ψ')  φ" by(drule_tac p=p in statClosed) auto
qed

lemma AssertionStatEqClosed:
  fixes Ψ  :: 'b
  and   Ψ' :: 'b
  and   p  :: "name prm"

  assumes "Ψ  Ψ'"

  shows "(p  Ψ)  (p  Ψ')"
using assms
by(auto simp add: AssertionStatEq_def intro: AssertionStatImpClosed)

lemma AssertionStatImpEqvt[eqvt]:
  fixes Ψ  :: 'b
  and   Ψ' :: 'b
  and   p  :: "name prm"

  shows "(p  (Ψ  Ψ')) = ((p  Ψ)  (p  Ψ'))"
by(simp add: AssertionStatImp_def eqvts)

lemma AssertionStatEqEqvt[eqvt]:
  fixes Ψ  :: 'b
  and   Ψ' :: 'b
  and   p  :: "name prm"

  shows "(p  (Ψ  Ψ')) = ((p  Ψ)  (p  Ψ'))"
by(simp add: AssertionStatEq_def eqvts)

lemma AssertionStatImpRefl[simp]:
  fixes Ψ :: 'b

  shows "Ψ  Ψ"
by(simp add: AssertionStatImp_def)

lemma AssertionStatEqRefl[simp]:
  fixes Ψ :: 'b

  shows "Ψ  Ψ"
by(simp add: AssertionStatEq_def)

lemma AssertionStatEqSym:
  fixes Ψ   :: 'b
  and   Ψ'  :: 'b

  assumes "Ψ  Ψ'"

  shows "Ψ'  Ψ"
using assms
by(auto simp add: AssertionStatEq_def)

lemma AssertionStatImpTrans:
  fixes Ψ   :: 'b
  and   Ψ'  :: 'b
  and   Ψ'' :: 'b

  assumes "Ψ  Ψ'"
  and     "Ψ'  Ψ''"

  shows "Ψ  Ψ''"
using assms
by(simp add: AssertionStatImp_def)

lemma AssertionStatEqTrans:
  fixes Ψ   :: 'b
  and   Ψ'  :: 'b
  and   Ψ'' :: 'b

  assumes "Ψ  Ψ'"
  and     "Ψ'  Ψ''"

  shows "Ψ  Ψ''"
using assms
by(auto simp add: AssertionStatEq_def intro: AssertionStatImpTrans)

definition 
  FrameImp :: "'b::fs_name frame  'c  bool"   (infixl "F" 70)
  where "(F F Φ) = (AF ΨF. F = AF, ΨF  AF ♯* Φ  (ΨF  Φ))"

lemma frameImpI:
  fixes F  :: "'b frame"
  and   φ  :: 'c
  and   AF :: "name list"
  and   ΨF :: 'b

  assumes "F = AF, ΨF"
  and     "AF ♯* φ"
  and     "ΨF  φ"

  shows "F F φ"
using assms
by(force simp add: FrameImp_def)

lemma frameImpAlphaEnt:
  fixes AF  :: "name list"
  and   ΨF  :: 'b
  and   AF' :: "name list"
  and   ΨF' :: 'b
  and   φ   :: 'c

  assumes "AF, ΨF = AF', ΨF'" 
  and     "AF ♯* φ"
  and     "AF' ♯* φ"
  and     "ΨF'  φ"

  shows "ΨF  φ"
proof -
  from AF, ΨF = AF', ΨF'
  obtain n where "n = length AF" by blast
  moreover from AF, ΨF = AF', ΨF'
  have "length AF = length AF'"
    by(rule frameChainEqLength)
  ultimately show ?thesis using assms
  proof(induct n arbitrary: AF AF' ΨF' rule: nat.induct)
    case(zero AF AF' ΨF')
    thus ?case by(auto simp add: frame.inject)
  next
    case(Suc n AF AF' ΨF')
    from ‹Suc n = length AF
    obtain x xs where "AF = x#xs" and "n = length xs"
      by(case_tac AF) auto
    from AF, ΨF = AF', ΨF' AF = x # xs
    obtain y ys where "(x#xs), ΨF = (y#ys), ΨF'" and "AF' = y#ys"
      by(case_tac AF') auto
    hence EQ: "⦇νx⦇ν*xs(FAssert ΨF) = ⦇νy⦇ν*ys(FAssert ΨF')"
      by simp
    from AF = x # xs AF' = y # ys ‹length AF = length AF' AF ♯* φ AF' ♯* φ
    have "length xs = length ys" and "xs ♯* φ" and "ys ♯* φ" and "x  φ" and "y  φ" 
      by auto
    
    have IH: "xs ys ΨF'. n = length xs; length xs = length ys; xs, ΨF = ys, (ΨF'::'b); xs ♯* φ; ys ♯* φ; ΨF'  φ  ΨF  φ"
      by fact
    show ?case
    proof(case_tac "x = y")
      assume "x = y"
      with EQ have "xs, ΨF = ys, ΨF'" by(simp add: alpha frame.inject)
      with IH n = length xs ‹length xs = length ys xs ♯* φ  ys ♯* φ ΨF'  φ
      show ?case by blast
    next
      assume "x  y"
      with EQ have "xs, ΨF = [(x, y)]  ys, ΨF'" by(simp add: alpha frame.inject)
      hence "xs, ΨF = ([(x, y)]  ys), ([(x, y)]  ΨF')" by(simp add: eqvts)
      moreover from ‹length xs = length ys have "length xs = length([(x, y)]  ys)"
        by auto
      moreover from ys ♯* φ have "([(x, y)]  ys) ♯* ([(x, y)]  φ)"
        by(simp add: fresh_star_bij)
      with x  φ y  φ have "([(x, y)]  ys) ♯* φ"
        by simp
      moreover with ΨF'  φ have "([(x, y)]  ΨF')  ([(x, y)]  φ)"
        by(simp add: statClosed)
      with x  φ y  φ have "([(x, y)]  ΨF')  φ"
        by simp
      ultimately show ?case using IH n = length xs xs ♯* φ
        by blast
    qed
  qed
qed

lemma frameImpEAux:
  fixes F  :: "'b frame"
  and   Φ  :: 'c

  assumes  "F F Φ"
  and      "F = AF, ΨF"
  and      "AF ♯* Φ"
  
  shows "ΨF  Φ"
using assms
by(auto simp add: FrameImp_def dest: frameImpAlphaEnt)

lemma frameImpE:
  fixes F  :: "'b frame"
  and   Φ  :: 'c

  assumes  "AF, ΨF F Φ"
  and      "AF ♯* Φ"
  
  shows "ΨF  Φ"
using assms
by(auto elim: frameImpEAux)

lemma frameImpClosed:
  fixes F :: "'b frame"
  and   Φ :: 'c
  and   p :: "name prm"

  assumes "F F Φ"

  shows "(p  F) F (p  Φ)"
using assms
by(force simp add: FrameImp_def eqvts pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst]
         intro: statClosed)

lemma frameImpEqvt[eqvt]:
  fixes F :: "'b frame"
  and   Φ :: 'c
  and   p :: "name prm"

  shows "(p  (F F Φ)) = (p  F) F (p  Φ)"
proof -
  have "F F Φ  (p  F) F (p  Φ)"
    by(rule frameImpClosed)
  moreover have "(p  F) F (p  Φ)  F F Φ"
    by(drule_tac p = "rev p" in frameImpClosed) simp
  ultimately show ?thesis
    by(auto simp add: perm_bool)
qed

lemma frameImpEmpty[simp]:
  fixes Ψ :: 'b
  and   φ :: 'c

  shows "⟨ε, Ψ F φ = Ψ  φ" 
by(auto simp add: FrameImp_def)

definition
  FrameStatImp :: "'b frame  'b frame bool" (infix "F" 70)
  where "(F F G)  (φ. F F φ  G F φ)"

definition
  FrameStatEq :: "'b frame  'b frame bool" (infix "F" 70)
  where "(F F G)  F F G  G F F"

lemma FrameStatImpClosed:
  fixes F :: "'b frame"
  and   G :: "'b frame"
  and   p :: "name prm"

  assumes "F F G"

  shows "(p  F) F (p  G)"
proof(auto simp add: FrameStatImp_def)
  fix φ
  assume "(p  F) F φ"
  hence "F F rev p  φ" by(drule_tac p="rev p" in frameImpClosed) auto
  with F F G have "G F rev p  φ" by(simp add: FrameStatImp_def)
  thus "(p  G) F φ" by(drule_tac p=p in frameImpClosed) auto
qed

lemma FrameStatEqClosed:
  fixes F :: "'b frame"
  and   G :: "'b frame"
  and   p :: "name prm"

  assumes "F F G"

  shows "(p  F) F (p  G)"
using assms
by(auto simp add: FrameStatEq_def intro: FrameStatImpClosed)

lemma FrameStatImpEqvt[eqvt]:
  fixes F :: "'b frame"
  and   G :: "'b frame"
  and   p :: "name prm"

  shows "(p  (F F G)) = ((p  F) F (p  G))"
by(simp add: FrameStatImp_def eqvts)

lemma FrameStatEqEqvt[eqvt]:
  fixes F :: "'b frame"
  and   G :: "'b frame"
  and   p :: "name prm"

  shows "(p  (F F G)) = ((p  F) F (p  G))"
by(simp add: FrameStatEq_def eqvts)

lemma FrameStatImpRefl[simp]:
  fixes F :: "'b frame"

  shows "F F F"
by(simp add: FrameStatImp_def)

lemma FrameStatEqRefl[simp]:
  fixes F :: "'b frame"

  shows "F F F"
by(simp add: FrameStatEq_def)

lemma FrameStatEqSym:
  fixes F  :: "'b frame"
  and   G  :: "'b frame"

  assumes "F F G"

  shows "G F F"
using assms
by(auto simp add: FrameStatEq_def)

lemma FrameStatImpTrans:
  fixes F :: "'b frame"
  and   G :: "'b frame" 
  and   H :: "'b frame"

  assumes "F F G"
  and     "G F H"

  shows "F F H"
using assms
by(simp add: FrameStatImp_def)

lemma FrameStatEqTrans:
  fixes F :: "'b frame"
  and   G :: "'b frame"
  and   H :: "'b frame"

  assumes "F F G"
  and     "G F H"

  shows "F F H"
using assms
by(auto simp add: FrameStatEq_def intro: FrameStatImpTrans)

lemma fsCompose[simp]: "finite((supp SCompose)::name set)"
by(simp add: supp_def perm_fun_def eqvts)

nominal_primrec 
   insertAssertion :: "'b frame  'b  'b frame"
where
  "insertAssertion (FAssert Ψ) Ψ' = FAssert (Ψ'  Ψ)"
| "x  Ψ'  insertAssertion (⦇νxF) Ψ' = ⦇νx(insertAssertion F Ψ')"
apply(finite_guess add: fsCompose)+
apply(rule TrueI)+
apply(simp add: abs_fresh)
apply(rule supports_fresh[of "supp