# 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∙(pi2∙Xs)"
by(auto simp add: perm_set_def pt2[OF pt])

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

atom_decl name

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

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

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

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

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

assumes "x ♯ l"
and     "p mem l"

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

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

assumes "p mem l"

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

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

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

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

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

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

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

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

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

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

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

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

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

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

lemma name_list_supp:
fixes xvec :: "name list"

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

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

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

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

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

lemmas abs_fresh_star = abs_fresh_list_star abs_fresh_set_star

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

assumes "a ♯ xvec"

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

lemma freshChainSym[simp]:
fixes xvec :: "name list"
and   yvec :: "name list"

shows   "xvec ♯* yvec = yvec ♯* xvec"
by(auto simp add: fresh_star_def fresh_def name_list_supp)

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

lemma name_set_avoiding:
fixes c :: "'a::fs_name"
and   X :: "name set"

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

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

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

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

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

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

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

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

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

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

assumes "eqvt X"

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

lemma eqvtI:
fixes X :: "'d::fs_name set"
and   x :: 'd
and   p :: "name prm"

assumes "eqvt X"
and     "x ∈ X"

shows "(p ∙ x) ∈ X"
using assms
by(unfold eqvt_def) auto

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

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

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

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

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

shows "(X ♯* (x, y)) = (X ♯* x ∧ X ♯* y)"
and   "(xvec ♯* (x, y)) = (xvec ♯* x ∧ xvec ♯* y)"
by(auto simp add: fresh_star_def)
lemma name_list_avoiding:
fixes c    :: "'a::fs_name"
and   xvec :: "name list"

assumes "⋀pi::name prm. ⟦(pi ∙ xvec) ♯* c; distinctPerm pi; set pi ⊆ (set xvec) × (set (pi ∙ xvec))⟧ ⟹ thesis"

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

assumes "x ♯ p"

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

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

assumes "xvec ♯* p"

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

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

shows "(xvec@yvec) ♯* C = ((xvec ♯* C) ∧ (yvec ♯* C))"
by(force simp add: fresh_star_def)

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

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

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

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

assumes "distinctPerm p"

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

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

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

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

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

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

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

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

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

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

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

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

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

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

assumes "length xvec = length yvec"

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

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

assumes "length xvec1 = length yvec1"

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

shows "x ∉ set xvec = x ♯ xvec"
by(simp add: name_list_supp fresh_def)

lemma calcChain:
fixes xvec :: "name list"
and   yvec :: "name list"

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

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

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

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

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

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

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

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

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

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

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

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

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

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

assumes "distinctPerm p"

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

lemma freshStarSimps:
fixes x  :: name
and   Xs :: "name set"
and   Ys :: "name set"
and   C  :: "'a::fs_name"
and   p  :: "name prm"

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

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

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

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

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

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

assumes "xvec ♯* p"

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

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

assumes "x ♯ p"

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

lemmas freshChainSimps = freshStarSimps freshStarChainSimps permStarFresh swapStarFresh chainFreshFresh freshPerm subsetFresh

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

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

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

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

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

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

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

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

end


# 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 ♯* (M⟨N⟩.P) = (X ♯* M ∧ X ♯* N ∧ X ♯* P)"
and   "X ♯* M⦇I = (X ♯* M ∧ X ♯* I)"
and   "X ♯* Case C = X ♯* C"
and   "X ♯* (P ∥ Q) = (X ♯* P ∧ X ♯* Q)"
and   "X ♯* ⦇νx⦈P = (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 ♯* (M⟨N⟩.P) = (xvec ♯* M ∧ xvec ♯* N ∧ xvec ♯* P)"
and   "xvec ♯* M⦇I = (xvec ♯* M ∧ xvec ♯* I)"
and   "xvec ♯* Case C = xvec ♯* C"
and   "xvec ♯* (P ∥ Q) = (xvec ♯* P ∧ xvec ♯* Q)"
and   "xvec ♯* ⦇νx⦈P = (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 ∙ (⦇ν*xvec⦈P) = ⦇ν*(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(⦇ν*xvec⦈P) = (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 ♯ ⦇ν*xvec⦈P = (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 ♯* (⦇ν*xvec⦈P) = (∀x∈Xs. x ∈ set xvec ∨ x ♯ P)"
and   "yvec ♯* (⦇ν*xvec⦈P) = (∀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 ♯* (⦇ν*xvec⦈P) = (Xs ♯* P)"
and   "yvec ♯* xvec ⟹ yvec ♯* (⦇ν*xvec⦈P) = (yvec ♯* P)"
and   "xvec ♯* (⦇ν*xvec⦈P)"
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 "⦇ν*xvec⦈P = ⦇ν*(p ∙ xvec)⦈(p ∙ P)"
proof -
note pt_name_inst at_name_inst S
moreover have "set xvec ♯* (⦇ν*xvec⦈P)"
by (simp add: resChainFreshSet)
moreover from xvecFreshP have "set (p ∙ xvec) ♯* (⦇ν*xvec⦈P)"
by (simp add: resChainFreshSet) (simp add: fresh_star_def)
ultimately have "⦇ν*xvec⦈P = p ∙ (⦇ν*xvec⦈P)"
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⦈(⦇ν*yvec⦈P)"
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) = (∀x∈Xs. 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 "⦇νx⦈P = ⦇ν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 (M⟨N⟩.P) = True"
| "guarded (M⦇I) = True"
| "guarded (Case C) = guarded'' C"
| "guarded (P ∥ Q) = ((guarded P) ∧ (guarded Q))"
| "guarded (⦇νx⦈P) = (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 (M⟨N⟩.P) xvec Tvec) = (substTerm M xvec Tvec)⟨(substTerm N xvec Tvec)⟩.(subs P xvec Tvec)"
| "(subs (M⦇I) 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 (⦇νy⦈P) 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 (M⟨N⟩.P) σ) = (substTerm.seqSubst M σ)⟨(substTerm.seqSubst N σ)⟩.(seqSubs P σ)"
and   "(seqSubs (M⦇I) σ) = (substTerm.seqSubst M σ)⦇(seqSubs' I σ)"

and   "(seqSubs (Case C) σ) = (Case (seqSubs'' C σ))"
and   "(seqSubs (P ∥ Q) σ) = (seqSubs P σ) ∥ (seqSubs Q σ)"
and   "⟦y ♯ σ⟧ ⟹ (seqSubs (⦇νy⦈P) σ) = ⦇ν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 "⟨A⇩F, Ψ⇩F⟩ ≡ frameResChain A⇩F (FAssert Ψ⇩F)"

lemma frameResChainEqvt[eqvt]:
fixes perm :: "name prm"
and   lst  :: "name list"
and   F    :: "'a::fs_name frame"

shows "perm ∙ (⦇ν*xvec⦈F) = ⦇ν*(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 ♯ ⦇ν*xvec⦈F = (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 ♯* (⦇ν*xvec⦈F) = (∀x∈Xs. 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 "⦇ν*xvec⦈F = ⦇ν*(p ∙ xvec)⦈(p ∙ F)"
proof -
note pt_name_inst at_name_inst S
moreover have "set xvec ♯* (⦇ν*xvec⦈F)"
by (simp add: frameResChainFreshSet)
moreover from xvecFreshF have "set (p ∙ xvec) ♯* (⦇ν*xvec⦈F)"
by (simp add: frameResChainFreshSet) (simp add: fresh_star_def)
ultimately have "⦇ν*xvec⦈F = p ∙ (⦇ν*xvec⦈F)"
by (rule_tac pt_freshs_freshs [symmetric])
then show ?thesis by(simp add: eqvts)
qed

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

assumes "(p ∙ A⇩P) ♯* Ψ⇩P"
and     S: "set p ⊆ set A⇩P × set (p ∙ A⇩P)"

shows "⟨A⇩P, Ψ⇩P⟩ = ⟨(p ∙ A⇩P), 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 "⦇νx⦈F = ⦇ν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⦈(⦇ν*yvec⦈F)"
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 "⦇νx⦈F = ⦇νy⦈G"
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 "⦇νx⦈F = ⦇νy⦈G"
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 A⇩F :: "name list"
and   Ψ  :: "'a::fs_name"
and   Ψ'  :: 'a

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

lemma distinctFrame:
fixes A⇩F :: "name list"
and   Ψ⇩F :: "'a::fs_name"
and   C  :: "'b::fs_name"

assumes "A⇩F ♯* C"

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

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

obtains A⇩F Ψ⇩F where "F = ⟨A⇩F, Ψ⇩F⟩" and "distinct A⇩F" and "A⇩F ♯* C"
proof -
assume "⋀A⇩F Ψ⇩F. ⟦F = ⟨A⇩F, Ψ⇩F⟩; distinct A⇩F; A⇩F ♯* C⟧ ⟹ thesis"
moreover have "∃A⇩F Ψ⇩F. F = ⟨A⇩F, Ψ⇩F⟩ ∧ A⇩F ♯* 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. ∃A⇩F Ψ⇩F. F = ⟨A⇩F, Ψ⇩F⟩ ∧ A⇩F ♯* C›
obtain A⇩F Ψ⇩F  where "F = ⟨A⇩F, Ψ⇩F⟩" and "A⇩F ♯* C"
by blast
with ‹a ♯ C› have "⦇νa⦈F = ⦇ν*(a#A⇩F)⦈(FAssert Ψ⇩F)" and "(a#A⇩F) ♯* 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 Φ) = (∃A⇩F Ψ⇩F. F = ⟨A⇩F, Ψ⇩F⟩ ∧ A⇩F ♯* Φ ∧ (Ψ⇩F ⊢ Φ))"

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

assumes "F = ⟨A⇩F, Ψ⇩F⟩"
and     "A⇩F ♯* φ"
and     "Ψ⇩F ⊢ φ"

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

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

assumes "⟨A⇩F, Ψ⇩F⟩ = ⟨A⇩F', Ψ⇩F'⟩"
and     "A⇩F ♯* φ"
and     "A⇩F' ♯* φ"
and     "Ψ⇩F' ⊢ φ"

shows "Ψ⇩F ⊢ φ"
proof -
from ‹⟨A⇩F, Ψ⇩F⟩ = ⟨A⇩F', Ψ⇩F'⟩›
obtain n where "n = length A⇩F" by blast
moreover from ‹⟨A⇩F, Ψ⇩F⟩ = ⟨A⇩F', Ψ⇩F'⟩›
have "length A⇩F = length A⇩F'"
by(rule frameChainEqLength)
ultimately show ?thesis using assms
proof(induct n arbitrary: A⇩F A⇩F' Ψ⇩F' rule: nat.induct)
case(zero A⇩F A⇩F' Ψ⇩F')
thus ?case by(auto simp add: frame.inject)
next
case(Suc n A⇩F A⇩F' Ψ⇩F')
from ‹Suc n = length A⇩F›
obtain x xs where "A⇩F = x#xs" and "n = length xs"
by(case_tac A⇩F) auto
from ‹⟨A⇩F, Ψ⇩F⟩ = ⟨A⇩F', Ψ⇩F'⟩› ‹A⇩F = x # xs›
obtain y ys where "⟨(x#xs), Ψ⇩F⟩ = ⟨(y#ys), Ψ⇩F'⟩" and "A⇩F' = y#ys"
by(case_tac A⇩F') auto
hence EQ: "⦇νx⦈⦇ν*xs⦈(FAssert Ψ⇩F) = ⦇νy⦈⦇ν*ys⦈(FAssert Ψ⇩F')"
by simp
from ‹A⇩F = x # xs› ‹A⇩F' = y # ys› ‹length A⇩F = length A⇩F'› ‹A⇩F ♯* φ› ‹A⇩F' ♯* φ›
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 = ⟨A⇩F, Ψ⇩F⟩"
and      "A⇩F ♯* Φ"

shows "Ψ⇩F ⊢ Φ"
using assms
by(auto simp add: FrameImp_def dest: frameImpAlphaEnt)

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

assumes  "⟨A⇩F, Ψ⇩F⟩ ⊢⇩F Φ"
and      "A⇩F ♯* Φ"

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 (⦇νx⦈F) Ψ' = ⦇νx⦈(insertAssertion F Ψ')"
apply(finite_guess add: fsCompose)+
apply(rule TrueI)+
apply(simp add: abs_fresh)
apply(rule supports_fresh[of "supp