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 Ψ'"])
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)+
done

lemma insertAssertionEqvt[eqvt]:
  fixes p :: "name prm"
  and   F :: "'b frame"
  and   Ψ :: 'b

  shows "p ∙ (insertAssertion F Ψ) = insertAssertion (p ∙ F) (p ∙ Ψ)"
by(nominal_induct F avoiding: p Ψ rule: frame.strong_induct)
  (auto simp add: at_prm_fresh[OF at_name_inst] 
                  pt_fresh_perm_app[OF pt_name_inst, OF at_name_inst] eqvts)


nominal_primrec 
   mergeFrame :: "'b frame ⇒ 'b frame ⇒ 'b frame"
where
  "mergeFrame (FAssert Ψ) G = insertAssertion G Ψ"
| "x ♯ G ⟹ mergeFrame (⦇νx⦈F) G = ⦇νx⦈(mergeFrame F G)"
apply(finite_guess add: fsCompose)+
apply(rule TrueI)+
apply(simp add: abs_fresh)
apply(simp add: fs_name1)
apply(rule supports_fresh[of "supp G"])
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)+
done

notation mergeFrame (infixr "⊗⇩F" 80)

abbreviation
  frameBottomJudge ("⊥⇩F") where "⊥⇩F ≡ (FAssert SBottom)"

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

  shows "p ∙ (mergeFrame F G) = mergeFrame (p ∙ F) (p ∙ G)"
by(nominal_induct F avoiding: p G rule: frame.strong_induct)
  (auto simp add: at_prm_fresh[OF at_name_inst] 
                  pt_fresh_perm_app[OF pt_name_inst, OF at_name_inst] eqvts)

nominal_primrec
    extractFrame   :: "('a, 'b, 'c) psi ⇒ 'b frame"
and extractFrame'  :: "('a, 'b, 'c) input ⇒ 'b frame"
and extractFrame'' :: "('a, 'b, 'c) psiCase ⇒ 'b frame"

where
  "extractFrame (𝟬) =  ⟨ε, ⊥⟩"
| "extractFrame (M⦇I) = ⟨ε, ⊥⟩"
| "extractFrame (M⟨N⟩.P) = ⟨ε, ⊥⟩"
| "extractFrame (Case C) = ⟨ε, ⊥⟩"
| "extractFrame (P ∥ Q) = (extractFrame P) ⊗⇩F (extractFrame Q)"
| "extractFrame ((⦃Ψ⦄::('a, 'b, 'c) psi)) = ⟨ε, Ψ⟩" 

| "extractFrame (⦇νx⦈P) = ⦇νx⦈(extractFrame P)"
| "extractFrame (!P) = ⟨ε, ⊥⟩" 

| "extractFrame' ((Trm M P)::('a::fs_name, 'b::fs_name, 'c::fs_name) input) = ⟨ε, ⊥⟩" 
| "extractFrame' (Bind x I) = ⟨ε, ⊥⟩" 

| "extractFrame'' (⊥⇩c::('a::fs_name, 'b::fs_name, 'c::fs_name) psiCase) = ⟨ε, ⊥⟩" 
| "extractFrame'' (□Φ ⇒ P C) = ⟨ε, ⊥⟩" 
apply(finite_guess add: fsCompose)+
apply(rule TrueI)+
apply(simp add: abs_fresh)+
apply(fresh_guess add: freshBottom)+
apply(rule supports_fresh[of "{}"])
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 add: freshBottom)+
apply(rule supports_fresh[of "{}"])
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 add: freshBottom)+
done

lemmas extractFrameSimps = extractFrame_extractFrame'_extractFrame''.simps

lemma extractFrameEqvt[eqvt]:
  fixes p :: "name prm"
  and   P :: "('a, 'b, 'c) psi"
  and   I :: "('a, 'b, 'c) input"
  and   C :: "('a, 'b, 'c) psiCase"

  shows "p ∙ (extractFrame P) = extractFrame (p ∙ P)"
  and   "p ∙ (extractFrame' I) = extractFrame' (p ∙ I)"
  and   "p ∙ (extractFrame'' C) = extractFrame'' (p ∙ C)"
by(nominal_induct P and I and C avoiding: p rule: psi_input_psiCase.strong_inducts)
   (auto simp add: at_prm_fresh[OF at_name_inst] eqvts permBottom
                  pt_fresh_perm_app[OF pt_name_inst, OF at_name_inst])

lemma insertAssertionFresh[intro]:
  fixes F :: "'b frame"
  and   Ψ :: 'b
  and   x :: name

  assumes "x ♯ F"
  and     "x ♯ Ψ"

  shows "x ♯ (insertAssertion F Ψ)"
using assms
by(nominal_induct F avoiding: x Ψ rule: frame.strong_induct)
  (auto simp add: abs_fresh)

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

  shows "⟦xvec ♯* F; xvec ♯* Ψ⟧ ⟹ xvec ♯* (insertAssertion F Ψ)"
  and   "⟦Xs ♯* F; Xs ♯* Ψ⟧ ⟹ Xs ♯* (insertAssertion F Ψ)"
by(auto simp add: fresh_star_def)

lemma mergeFrameFresh[intro]:
  fixes F :: "'b frame"
  and   G :: "'b frame"
  and   x :: name

  shows "⟦x ♯ F; x ♯ G⟧ ⟹ x ♯ (mergeFrame F G)"
by(nominal_induct F avoiding: x G rule: frame.strong_induct)
  (auto simp add: abs_fresh)

lemma mergeFrameFreshChain[intro]:
  fixes F    :: "'b frame"
  and   G    :: "'b frame"
  and   xvec :: "name list"
  and   Xs   :: "name set"

  shows "⟦xvec ♯* F; xvec ♯* G⟧ ⟹ xvec ♯* (mergeFrame F G)"
  and   "⟦Xs ♯* F; Xs ♯* G⟧ ⟹ Xs ♯* (mergeFrame F G)"
by(auto simp add: fresh_star_def)

lemma extractFrameFresh:
  fixes P :: "('a, 'b, 'c) psi"
  and   I :: "('a, 'b, 'c) input"
  and   C :: "('a, 'b, 'c) psiCase"
  and   x :: name

  shows "x ♯ P ⟹ x ♯ extractFrame P"
  and   "x ♯ I ⟹ x ♯ extractFrame' I"
  and   "x ♯ C ⟹ x ♯ extractFrame'' C"
by(nominal_induct P and I and C avoiding: x rule: psi_input_psiCase.strong_inducts)
  (auto simp add: abs_fresh)

lemma extractFrameFreshChain:
  fixes P    :: "('a, 'b, 'c) psi"
  and   I    :: "('a, 'b, 'c) input"
  and   C    :: "('a, 'b, 'c) psiCase"
  and   xvec :: "name list"
  and   Xs   :: "name set"

  shows "xvec ♯* P ⟹ xvec ♯* extractFrame P"
  and   "xvec ♯* I ⟹ xvec ♯* extractFrame' I"
  and   "xvec ♯* C ⟹ xvec ♯* extractFrame'' C"
  and   "Xs ♯* P ⟹ Xs ♯* extractFrame P"
  and   "Xs ♯* I ⟹ Xs ♯* extractFrame' I"
  and   "Xs ♯* C ⟹ Xs ♯* extractFrame'' C"
by(auto simp add: fresh_star_def intro: extractFrameFresh)


lemma guardedFrameSupp[simp]:
  fixes P :: "('a, 'b, 'c) psi"
  and   I :: "('a, 'b, 'c) input"
  and   C :: "('a, 'b, 'c) psiCase"
  and   x :: name 

  shows "guarded P ⟹ x ♯ (extractFrame P)"
  and   "guarded' I ⟹ x ♯ (extractFrame' I)"
  and   "guarded'' C ⟹ x ♯ (extractFrame'' C)"
by(nominal_induct P and I and C arbitrary: x rule: psi_input_psiCase.strong_inducts)
  (auto simp add: frameResChainFresh abs_fresh)

lemma frameResChainFresh': 
  fixes xvec :: "name list"
  and   yvec :: "name list"
  and   F    :: "'b frame"

  shows "(xvec ♯* (⦇ν*yvec⦈F)) = (∀x ∈ set xvec. x ∈ set yvec ∨ x ♯ F)"
by(simp add: frameResChainFresh fresh_star_def)

lemma frameChainFresh[simp]:
  fixes xvec :: "name list"
  and   Ψ    :: 'b
  and   Xs   :: "name set"

  shows "xvec ♯* (FAssert Ψ) = xvec ♯* Ψ"
  and   "Xs ♯* (FAssert Ψ) = Xs ♯* Ψ"
by(simp add: fresh_star_def)+

lemma frameResChainFresh''[simp]:
  fixes xvec :: "name list"
  and   yvec :: "name list"
  and   F    :: "'b frame"
  
  assumes "xvec ♯* yvec"

  shows "xvec ♯* (⦇ν*yvec⦈F) = xvec ♯* F"

using assms
by(simp_all add: frameResChainFresh')
  (auto simp add: fresh_star_def fresh_def name_list_supp)

lemma frameResChainFresh'''[simp]:
  fixes x    :: name
  and   xvec :: "name list"
  and   F    :: "'b frame"
  
  assumes "x ♯ xvec"

  shows "x ♯ (⦇ν*xvec⦈F) = x ♯ F"
using assms
by(induct xvec) (auto simp add: abs_fresh)

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

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

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

  shows "xvec ♯* (SBottom)"
  and   "Xs ♯* (SBottom)"
by(auto simp add: fresh_star_def)
(*
lemma freshChainComp[simp]:
  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 freshFrameDest[dest]:
  fixes A⇩F    :: "name list"
  and   Ψ⇩F   :: 'b
  and   xvec  :: "name list"

  assumes "xvec ♯* (⟨A⇩F, Ψ⇩F⟩)"

  shows "xvec ♯* A⇩F ⟹ xvec ♯* Ψ⇩F"
  and   "A⇩F ♯* xvec ⟹ xvec ♯* Ψ⇩F"
proof -
  from assms have "(set xvec) ♯* (⟨A⇩F, Ψ⇩F⟩)"
    by(simp add: fresh_star_def)
  moreover assume "xvec ♯* A⇩F"
  ultimately show "xvec ♯* Ψ⇩F"
    by(simp add: frameResChainFreshSet) (force simp add: fresh_def name_list_supp fresh_star_def)
next
  from assms have "(set xvec) ♯* (⟨A⇩F, Ψ⇩F⟩)"
    by(simp add: fresh_star_def)
  moreover assume "A⇩F ♯* xvec"
  ultimately show "xvec ♯* Ψ⇩F"
    by(simp add: frameResChainFreshSet) (force simp add: fresh_def name_list_supp fresh_star_def)
qed

lemma insertAssertionSimps[simp]:
  fixes A⇩F :: "name list"
  and   Ψ⇩F :: 'b
  and   Ψ  :: 'b
  
  assumes "A⇩F ♯* Ψ"

  shows "insertAssertion (⟨A⇩F, Ψ⇩F⟩) Ψ = ⟨A⇩F, Ψ ⊗ Ψ⇩F⟩"
using assms
by(induct A⇩F arbitrary: F) auto

lemma mergeFrameSimps[simp]:
  fixes A⇩F :: "name list"
  and   Ψ⇩F :: 'b
  and   Ψ  :: 'b

  assumes "A⇩F ♯* Ψ"

  shows "(⟨A⇩F, Ψ⇩F⟩) ⊗⇩F ⟨ε, Ψ⟩ = ⟨A⇩F, Ψ⇩F ⊗ Ψ⟩"
using assms
by(induct A⇩F arbitrary: F) auto

lemma mergeFrames[simp]:
  fixes A⇩F  :: "name list"
  and   Ψ⇩F :: 'b
  and   A⇩G  :: "name list"
  and   Ψ⇩G :: 'b

  assumes "A⇩F ♯* A⇩G"
  and     "A⇩F ♯* Ψ⇩G"
  and     "A⇩G ♯* Ψ⇩F"

  shows "(⟨A⇩F, Ψ⇩F⟩) ⊗⇩F (⟨A⇩G, Ψ⇩G⟩) = (⟨(A⇩F@A⇩G), Ψ⇩F ⊗ Ψ⇩G⟩)"
using assms
by(induct A⇩F) auto

lemma frameImpResFreshLeft:
  fixes F :: "'b frame"
  and   x :: name
  
  assumes "x ♯ F"

  shows "⦇νx⦈F ↪⇩F F"
proof(auto simp add: FrameStatImp_def)
  fix φ::'c
  obtain A⇩F Ψ⇩F where Feq: "F = ⟨A⇩F, Ψ⇩F⟩" and "A⇩F ♯* (x, φ)"
    by(rule freshFrame)
  from ‹A⇩F ♯* (x, φ)› have "x ♯ A⇩F" and "A⇩F ♯* φ" by simp+
  obtain y where "y ♯ φ" and "y ♯ F" and "x ≠ y"
    by(generate_fresh "name", auto)
  
  assume "⦇νx⦈F ⊢⇩F φ"
  with ‹y ♯ F› have "⦇νy⦈([(x, y)] ∙ F) ⊢⇩F φ" by(simp add: alphaFrameRes)
  with ‹x ♯ F› ‹y ♯ F› have "⦇νy⦈F ⊢⇩F φ" by simp
  with Feq have "⟨(y#A⇩F), Ψ⇩F⟩ ⊢⇩F φ" by simp
  with Feq ‹A⇩F ♯* φ› ‹y ♯ φ› show "F ⊢⇩F φ"
    by(force intro: frameImpI dest: frameImpE simp del: frameResChain.simps)
qed

lemma frameImpResFreshRight:
  fixes F :: "'b frame"
  and   x :: name
  
  assumes "x ♯ F"

  shows "F ↪⇩F ⦇νx⦈F"
proof(auto simp add: FrameStatImp_def)
  fix φ::'c
  obtain A⇩F Ψ⇩F where Feq: "F = ⟨A⇩F, Ψ⇩F⟩" and "A⇩F ♯* (x, φ)"
    by(rule freshFrame)
  from ‹A⇩F ♯* (x, φ)› have "x ♯ A⇩F" and "A⇩F ♯* φ" by simp+
  obtain y where "y ♯ φ" and "y ♯ F" and "x ≠ y"
    by(generate_fresh "name", auto)
  
  assume "F ⊢⇩F φ"
  with Feq ‹A⇩F ♯* φ› ‹y ♯ φ› have "⟨(y#A⇩F), Ψ⇩F⟩ ⊢⇩F φ"
    by(force intro: frameImpI dest: frameImpE simp del: frameResChain.simps)
  moreover with ‹y ♯ F› ‹x ♯ F› Feq show "⦇νx⦈F ⊢⇩F φ"
    by(subst alphaFrameRes) auto
qed

lemma frameResFresh:
  fixes F :: "'b frame"
  and   x :: name
  
  assumes "x ♯ F"

  shows "⦇νx⦈F ≃⇩F F"
using assms
by(auto simp add: FrameStatEq_def intro: frameImpResFreshLeft frameImpResFreshRight)

lemma frameImpResPres:
  fixes F :: "'b frame"
  and   G :: "'b frame"
  and   x :: name
  
  assumes "F ↪⇩F G"

  shows "⦇νx⦈F ↪⇩F ⦇νx⦈G"
proof(auto simp add: FrameStatImp_def)
  fix φ::'c
  obtain A⇩F Ψ⇩F where Feq: "F = ⟨A⇩F, Ψ⇩F⟩" and "A⇩F ♯* (x, φ)"
    by(rule freshFrame)
  from ‹A⇩F ♯* (x, φ)› have "x ♯ A⇩F" and "A⇩F ♯* φ" by simp+
  obtain y where "y ♯ A⇩F" and "y ♯ F" and "y ♯ G"
             and "x ≠ y" and "y ♯ φ"
    by(generate_fresh "name", auto)
  assume "⦇νx⦈F ⊢⇩F φ"
  with ‹y ♯ F› have "⦇νy⦈([(x, y)] ∙ F) ⊢⇩F φ" by(simp add: alphaFrameRes)
  with Feq ‹x ♯ A⇩F› ‹y ♯ A⇩F› have "⟨(y#A⇩F), [(x, y)] ∙ Ψ⇩F⟩ ⊢⇩F φ" by(simp add: eqvts)
  with ‹y ♯ φ› ‹A⇩F ♯* φ› have "⟨A⇩F, [(x, y)] ∙ Ψ⇩F⟩ ⊢⇩F φ"
    by(force intro: frameImpI dest: frameImpE simp del: frameResChain.simps)
  hence "([(x, y)] ∙ ⟨A⇩F, [(x, y)] ∙ Ψ⇩F⟩) ⊢⇩F ([(x, y)] ∙ φ)"
    by(rule frameImpClosed)
  with ‹x ♯ A⇩F› ‹y ♯ A⇩F› Feq have "F ⊢⇩F [(x, y)] ∙ φ"
    by(simp add: eqvts)
  with ‹F ↪⇩F G› have "G ⊢⇩F [(x, y)] ∙ φ" by(simp add: FrameStatImp_def)
  
  obtain A⇩G Ψ⇩G where Geq: "G = ⟨A⇩G, Ψ⇩G⟩" and "A⇩G ♯* (x, y, φ)"
    by(rule freshFrame)
  from ‹A⇩G ♯* (x, y, φ)› have "x ♯ A⇩G" and "y ♯ A⇩G" and "A⇩G ♯* φ" by simp+
  from ‹G ⊢⇩F [(x, y)] ∙ φ› have "([(x, y)] ∙ G) ⊢⇩F [(x, y)] ∙ [(x, y)] ∙ φ"
    by(rule frameImpClosed)
  with Geq ‹x ♯ A⇩G› ‹y ♯ A⇩G› have "⟨A⇩G, [(x, y)] ∙ Ψ⇩G⟩ ⊢⇩F φ" by(simp add: eqvts)
  with ‹y ♯ φ› ‹A⇩G ♯* φ› have "⟨(y#A⇩G), [(x, y)] ∙ Ψ⇩G⟩ ⊢⇩F φ"
    by(force intro: frameImpI dest: frameImpE simp del: frameResChain.simps)
  with ‹y ♯ G› ‹x ♯ A⇩G› ‹y ♯ A⇩G› Geq show "⦇νx⦈G ⊢⇩F φ"
    by(subst alphaFrameRes) (fastforce simp add: eqvts)+
qed

lemma frameResPres:
  fixes F :: "'b frame"
  and   G :: "'b frame"
  and   x :: name
  
  assumes "F ≃⇩F G"

  shows "⦇νx⦈F ≃⇩F ⦇νx⦈G"
using assms
by(auto simp add: FrameStatEq_def intro: frameImpResPres)

lemma frameImpResComm:
  fixes x :: name
  and   y :: name
  and   F :: "'b frame"

  shows "⦇νx⦈(⦇νy⦈F) ↪⇩F ⦇νy⦈(⦇νx⦈F)"
proof(case_tac "x = y")
  assume "x = y"
  thus ?thesis by simp
next
  assume "x ≠ y"
  show ?thesis
  proof(auto simp add: FrameStatImp_def)
    fix φ::'c
    obtain A⇩F Ψ⇩F where Feq: "F = ⟨A⇩F, Ψ⇩F⟩" and "A⇩F ♯* (x, y, φ)"
      by(rule freshFrame)
    then have "x ♯ A⇩F" and "y ♯ A⇩F" and "A⇩F ♯* φ" by simp+

    obtain x'::name where "x' ≠ x" and "x' ≠ y" and "x' ♯ F" and "x' ♯ φ" and "x' ♯ A⇩F"
      by(generate_fresh "name") auto
    obtain y'::name where "y' ≠ x" and "y' ≠ y" and "y' ≠ x'" and "y' ♯ F" and "y' ♯ φ" and "y' ♯ A⇩F"
      by(generate_fresh "name") auto
  
    from ‹y' ♯ F› have "⦇νx⦈(⦇νy⦈F) = ⦇νx⦈(⦇νy'⦈([(y, y')] ∙ F))"
      by(simp add: alphaFrameRes)
    moreover from ‹x' ♯ F› ‹x' ≠ y› ‹y' ≠ x'› have "… = ⦇νx'⦈([(x, x')] ∙ (⦇νy'⦈([(y, y')] ∙ F)))"
      by(rule_tac alphaFrameRes) (simp add: abs_fresh fresh_left)
    moreover with  ‹y' ≠ x'› ‹y' ≠ x› have "… = ⦇νx'⦈(⦇νy'⦈([(x, x')] ∙ [(y, y')] ∙ F))"
      by(simp add: eqvts calc_atm)
    ultimately have A: "⦇νx⦈(⦇νy⦈F)= ⦇νx'⦈(⦇νy'⦈(⦇ν*A⇩F⦈(FAssert([(x, x')] ∙ [(y, y')] ∙ Ψ⇩F))))"
      using  Feq ‹x ♯ A⇩F› ‹x' ♯ A⇩F› ‹y ♯ A⇩F› ‹y' ♯ A⇩F›
      by(simp add: eqvts)

    from ‹x' ♯ F› have "⦇νy⦈(⦇νx⦈F) = ⦇νy⦈(⦇νx'⦈([(x, x')] ∙ F))"
      by(simp add: alphaFrameRes)
    moreover from ‹y' ♯ F› ‹y' ≠ x› ‹y' ≠ x'› have "… = ⦇νy'⦈([(y, y')] ∙ (⦇νx'⦈([(x, x')] ∙ F)))"
      by(rule_tac alphaFrameRes) (simp add: abs_fresh fresh_left)
    moreover with  ‹y' ≠ x'› ‹x' ≠ y› have "… = ⦇νy'⦈(⦇νx'⦈([(y, y')] ∙ [(x, x')] ∙ F))"
      by(simp add: eqvts calc_atm)
    moreover with ‹x' ≠ x› ‹x' ≠ y› ‹y' ≠ x› ‹y' ≠ y› ‹y' ≠ x'› ‹x ≠ y›
      have "… = ⦇νy'⦈(⦇νx'⦈([(x, x')] ∙ [(y, y')] ∙ F))"
      apply(simp add: eqvts)
      by(subst perm_compose) (simp add: calc_atm)
    ultimately have B: "⦇νy⦈(⦇νx⦈F)= ⦇νy'⦈(⦇νx'⦈(⦇ν*A⇩F⦈(FAssert([(x, x')] ∙ [(y, y')] ∙ Ψ⇩F))))"
      using  Feq ‹x ♯ A⇩F› ‹x' ♯ A⇩F› ‹y ♯ A⇩F› ‹y' ♯ A⇩F›
      by(simp add: eqvts)

    from ‹x' ♯ φ› ‹y' ♯ φ› ‹A⇩F ♯* φ›
    have "⟨(x'#y'#A⇩F), [(x, x')] ∙ [(y, y')] ∙ Ψ⇩F⟩ ⊢⇩F φ = ⟨(y'#x'#A⇩F), [(x, x')] ∙ [(y, y')] ∙ Ψ⇩F⟩ ⊢⇩F φ"
      by(force dest: frameImpE intro: frameImpI simp del: frameResChain.simps)
    with A B have "(⦇νx⦈(⦇νy⦈F)) ⊢⇩F φ = (⦇νy⦈(⦇νx⦈F)) ⊢⇩F φ"
      by simp
    moreover assume "(⦇νx⦈(⦇νy⦈F)) ⊢⇩F φ"
    ultimately show "(⦇νy⦈(⦇νx⦈F)) ⊢⇩F φ" by simp
  qed
qed

lemma frameResComm:
  fixes x :: name
  and   y :: name
  and   F :: "'b frame"

  shows "⦇νx⦈(⦇νy⦈F) ≃⇩F ⦇νy⦈(⦇νx⦈F)"
by(auto simp add: FrameStatEq_def intro: frameImpResComm)

lemma frameImpResCommLeft':
  fixes x    :: name
  and   xvec :: "name list"
  and   F    :: "'b frame"

  shows "⦇νx⦈(⦇ν*xvec⦈F) ↪⇩F ⦇ν*xvec⦈(⦇νx⦈F)"
by(induct xvec) (auto intro: frameImpResComm FrameStatImpTrans frameImpResPres)

lemma frameImpResCommRight':
  fixes x    :: name
  and   xvec :: "name list"
  and   F    :: "'b frame"

  shows "⦇ν*xvec⦈(⦇νx⦈F) ↪⇩F ⦇νx⦈(⦇ν*xvec⦈F)"
by(induct xvec) (auto intro: frameImpResComm FrameStatImpTrans frameImpResPres)

lemma frameResComm':
  fixes x    :: name
  and   xvec :: "name list"
  and   F    :: "'b frame"

  shows "⦇νx⦈(⦇ν*xvec⦈F) ≃⇩F ⦇ν*xvec⦈(⦇νx⦈F)"
by(induct xvec) (auto intro: frameResComm FrameStatEqTrans frameResPres)

lemma frameImpChainComm:
  fixes xvec :: "name list"
  and   yvec :: "name list"
  and   F    :: "'b frame"

  shows "⦇ν*xvec⦈(⦇ν*yvec⦈F) ↪⇩F ⦇ν*yvec⦈(⦇ν*xvec⦈F)"
by(induct xvec) (auto intro: frameImpResCommLeft' FrameStatImpTrans frameImpResPres)

lemma frameResChainComm:
  fixes xvec :: "name list"
  and   yvec :: "name list"
  and   F    :: "'b frame"

  shows "⦇ν*xvec⦈(⦇ν*yvec⦈F) ≃⇩F ⦇ν*yvec⦈(⦇ν*xvec⦈F)"
by(induct xvec) (auto intro: frameResComm' FrameStatEqTrans frameResPres)

lemma frameImpNilStatEq[simp]:
  fixes Ψ  :: 'b
  and   Ψ' :: 'b

  shows "(⟨ε, Ψ⟩ ↪⇩F ⟨ε, Ψ'⟩) = (Ψ ↪ Ψ')"
by(simp add: FrameStatImp_def AssertionStatImp_def FrameImp_def)


lemma frameNilStatEq[simp]:
  fixes Ψ  :: 'b
  and   Ψ' :: 'b

  shows "(⟨ε, Ψ⟩ ≃⇩F ⟨ε, Ψ'⟩) = (Ψ ≃ Ψ')"
by(simp add: FrameStatEq_def AssertionStatEq_def FrameImp_def)

lemma extractFrameChainStatImp:
  fixes xvec :: "name list"
  and   P    :: "('a, 'b, 'c) psi"

  shows "extractFrame(⦇ν*xvec⦈P) ↪⇩F ⦇ν*xvec⦈(extractFrame P)"
by(induct xvec) (auto intro: frameImpResPres)

lemma extractFrameChainStatEq:
  fixes xvec :: "name list"
  and   P    :: "('a, 'b, 'c) psi"

  shows "extractFrame(⦇ν*xvec⦈P) ≃⇩F ⦇ν*xvec⦈(extractFrame P)"
by(induct xvec) (auto intro: frameResPres)

lemma insertAssertionExtractFrameFreshImp:
  fixes xvec :: "name list"
  and   Ψ   :: 'b
  and   P    :: "('a, 'b, 'c) psi"

  assumes "xvec ♯* Ψ"

  shows "insertAssertion(extractFrame(⦇ν*xvec⦈P)) Ψ ↪⇩F ⦇ν*xvec⦈(insertAssertion (extractFrame P) Ψ)"
using assms
by(induct xvec) (auto intro: frameImpResPres)

lemma insertAssertionExtractFrameFresh:
  fixes xvec :: "name list"
  and   Ψ   :: 'b
  and   P    :: "('a, 'b, 'c) psi"

  assumes "xvec ♯* Ψ"

  shows "insertAssertion(extractFrame(⦇ν*xvec⦈P)) Ψ ≃⇩F ⦇ν*xvec⦈(insertAssertion (extractFrame P) Ψ)"
using assms
by(induct xvec) (auto intro: frameResPres)

lemma frameImpResChainPres:
  fixes F    :: "'b frame"
  and   G    :: "'b frame"
  and   xvec :: "name list"

  assumes "F ↪⇩F G"

  shows "⦇ν*xvec⦈F ↪⇩F ⦇ν*xvec⦈G"
using assms
by(induct xvec) (auto intro: frameImpResPres)

lemma frameResChainPres:
  fixes F    :: "'b frame"
  and   G    :: "'b frame"
  and   xvec :: "name list"

  assumes "F ≃⇩F G"

  shows "⦇ν*xvec⦈F ≃⇩F ⦇ν*xvec⦈G"
using assms
by(induct xvec) (auto intro: frameResPres)

lemma insertAssertionE:
  fixes F  :: "('b::fs_name) frame"
  and   Ψ  :: 'b
  and   Ψ' :: 'b
  and   A⇩F :: "name list"

  assumes "insertAssertion F Ψ = ⟨A⇩F, Ψ'⟩"
  and     "A⇩F ♯* F"
  and     "A⇩F ♯* Ψ"
  and     "distinct A⇩F"

  obtains Ψ⇩F where "F = ⟨A⇩F, Ψ⇩F⟩" and "Ψ' = Ψ ⊗ Ψ⇩F"
proof -
  assume A: "⋀Ψ⇩F. ⟦F = ⟨A⇩F, Ψ⇩F⟩; Ψ' = Ψ ⊗ Ψ⇩F⟧ ⟹ thesis"
  from assms have "∃Ψ⇩F. F = ⟨A⇩F, Ψ⇩F⟩ ∧ Ψ' = Ψ ⊗ Ψ⇩F"
  proof(nominal_induct F avoiding: Ψ A⇩F Ψ' rule: frame.strong_induct)
    case(FAssert Ψ A⇩F Ψ')
    thus ?case by auto
  next
    case(FRes x F Ψ A⇩F Ψ')
    from ‹insertAssertion (⦇νx⦈F) Ψ = ⟨A⇩F, Ψ'⟩› ‹x ♯ Ψ›
    obtain y A⇩F' where "A⇩F = y#A⇩F'" by(induct A⇩F) auto
    with ‹insertAssertion (⦇νx⦈F) Ψ = ⟨A⇩F, Ψ'⟩› ‹x ♯ Ψ› ‹x ♯ A⇩F›
    have A: "insertAssertion F Ψ = ⟨([(x, y)] ∙ A⇩F'), [(x, y)] ∙ Ψ'⟩"
      by(simp add: frame.inject alpha eqvts)
    from ‹A⇩F = y#A⇩F'› ‹A⇩F ♯* Ψ› have "y ♯ Ψ" and "A⇩F' ♯* Ψ" by simp+
    from ‹distinct A⇩F› ‹A⇩F = y#A⇩F'› have "y ♯ A⇩F'" and "distinct A⇩F'" by auto
    from ‹A⇩F ♯* (⦇νx⦈F)› ‹x ♯ A⇩F› ‹A⇩F = y#A⇩F'› have "y ♯ F" and "A⇩F' ♯* F" and "x ♯ A⇩F'"
      apply -
      apply(auto simp add: abs_fresh)
      apply(hypsubst_thin)
      apply(subst fresh_star_def)
      apply(erule rev_mp)
      apply(subst fresh_star_def)
      apply(clarify)
      apply(erule_tac x=xa in ballE)
      apply(simp add: abs_fresh)
      apply auto
      by(simp add: fresh_def name_list_supp)
    with ‹x ♯ A⇩F'› ‹y ♯ A⇩F'› have "([(x, y)] ∙ A⇩F') ♯* F" by simp
    from ‹A⇩F' ♯* Ψ› have "([(x, y)] ∙ A⇩F') ♯* ([(x, y)] ∙ Ψ)" by(simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
    with ‹x ♯ Ψ› ‹y ♯ Ψ› have "([(x, y)] ∙ A⇩F') ♯* Ψ" by simp
    with ‹⋀Ψ A⇩F Ψ'. ⟦insertAssertion F Ψ = ⟨A⇩F, Ψ'⟩; A⇩F ♯* F; A⇩F ♯* Ψ; distinct A⇩F⟧ ⟹ ∃Ψ⇩F. F = ⟨A⇩F, Ψ⇩F⟩ ∧ Ψ' = Ψ ⊗ Ψ⇩F› A 
         ‹([(x, y)] ∙ A⇩F') ♯* F› ‹distinct A⇩F'› ‹x ♯ A⇩F'› ‹y ♯ A⇩F'›
    obtain Ψ⇩F where Feq: "F = ⟨A⇩F', Ψ⇩F⟩" and Ψeq: "([(x, y)] ∙ Ψ') = Ψ ⊗ Ψ⇩F"
      by force
    
    from Feq have "⦇νx⦈F =  ⟨(x#A⇩F'), Ψ⇩F⟩" by(simp add: frame.inject)
    hence "([(x, y)] ∙ ⦇νx⦈F) = [(x, y)] ∙ ⟨(x#A⇩F'), Ψ⇩F⟩" by simp
    hence "⦇νx⦈F = ⟨A⇩F, [(x, y)] ∙ Ψ⇩F⟩" using ‹y ♯ F› ‹A⇩F = y#A⇩F'› ‹x ♯ A⇩F› ‹y ♯ A⇩F'›
      by(simp add: eqvts calc_atm alphaFrameRes)

    moreover from Ψeq have "[(x, y)] ∙ ([(x, y)] ∙ Ψ') = [(x, y)] ∙ (Ψ ⊗ Ψ⇩F)"
      by simp
    with ‹x ♯ Ψ› ‹y ♯ Ψ› have "Ψ' = Ψ ⊗ ([(x, y)] ∙ Ψ⇩F)" by(simp add: eqvts)
    ultimately show ?case
      by blast
  qed
  with A show ?thesis
    by blast
qed

lemma mergeFrameE:
  fixes F   :: "'b frame"
  and   G   :: "'b frame"
  and   A⇩F⇩G :: "name list"
  and   Ψ⇩F⇩G :: 'b

  assumes "mergeFrame F G = ⟨A⇩F⇩G, Ψ⇩F⇩G⟩"
  and     "distinct A⇩F⇩G"
  and     "A⇩F⇩G ♯* F"
  and     "A⇩F⇩G ♯* G"

  obtains A⇩F Ψ⇩F A⇩G Ψ⇩G where "A⇩F⇩G = A⇩F@A⇩G" and "Ψ⇩F⇩G = Ψ⇩F ⊗ Ψ⇩G" and "F = ⟨A⇩F, Ψ⇩F⟩" and "G = ⟨A⇩G, Ψ⇩G⟩" and "A⇩F ♯* Ψ⇩G" and "A⇩G ♯* Ψ⇩F"
proof -
  assume A: "⋀A⇩F A⇩G Ψ⇩F Ψ⇩G. ⟦A⇩F⇩G = A⇩F@A⇩G; Ψ⇩F⇩G = Ψ⇩F ⊗ Ψ⇩G; F = ⟨A⇩F, Ψ⇩F⟩; G = ⟨A⇩G, Ψ⇩G⟩; A⇩F ♯* Ψ⇩G; A⇩G ♯* Ψ⇩F⟧ ⟹ thesis"
  from assms have "∃A⇩F Ψ⇩F A⇩G Ψ⇩G. A⇩F⇩G = A⇩F@A⇩G ∧ Ψ⇩F⇩G = Ψ⇩F ⊗ Ψ⇩G ∧ F = ⟨A⇩F, Ψ⇩F⟩ ∧ G = ⟨A⇩G, Ψ⇩G⟩ ∧ A⇩F ♯* Ψ⇩G ∧ A⇩G ♯* Ψ⇩F"
  proof(nominal_induct F avoiding: G A⇩F⇩G Ψ⇩F⇩G rule: frame.strong_induct)
    case(FAssert Ψ G A⇩F⇩G Ψ⇩F⇩G)
    thus ?case
      apply auto
      apply(rule_tac x="[]" in exI) 
      by(drule_tac insertAssertionE) auto
  next
    case(FRes x F G A⇩F⇩G Ψ⇩F⇩G)
    from ‹mergeFrame (⦇νx⦈F) G = ⟨A⇩F⇩G, Ψ⇩F⇩G⟩› ‹x ♯ G›
    obtain y A⇩F⇩G' where "A⇩F⇩G = y#A⇩F⇩G'" by(induct A⇩F⇩G) auto
    with ‹A⇩F⇩G ♯* (⦇νx⦈F)› ‹x ♯ A⇩F⇩G› have "A⇩F⇩G' ♯* F" and "x ♯ A⇩F⇩G'"
      by(auto simp add: supp_list_cons fresh_star_def fresh_def name_list_supp abs_supp frame.supp)
    from ‹A⇩F⇩G = y#A⇩F⇩G'› ‹A⇩F⇩G ♯* G› have "y ♯ G" and "A⇩F⇩G' ♯* G" by simp+
    from ‹A⇩F⇩G = y#A⇩F⇩G'› ‹A⇩F⇩G ♯* (⦇νx⦈F)› ‹x ♯ A⇩F⇩G› have "y ♯ F" and "A⇩F⇩G' ♯* F"
      apply(auto simp add: abs_fresh frameResChainFreshSet)
      apply(hypsubst_thin)
      by(induct A⇩F⇩G') (auto simp add: abs_fresh)
    from ‹distinct A⇩F⇩G› ‹A⇩F⇩G = y#A⇩F⇩G'› have "y ♯ A⇩F⇩G'" and "distinct A⇩F⇩G'" by auto
    
    with ‹A⇩F⇩G = y#A⇩F⇩G'› ‹mergeFrame (⦇νx⦈F) G = ⟨A⇩F⇩G, Ψ⇩F⇩G⟩› ‹x ♯ G› ‹x ♯ A⇩F⇩G› ‹y ♯ A⇩F⇩G'›
    have "mergeFrame F G = ⟨A⇩F⇩G', [(x, y)] ∙ Ψ⇩F⇩G⟩"
      by(simp add: frame.inject alpha eqvts)
    with ‹distinct A⇩F⇩G'› ‹A⇩F⇩G' ♯* F› ‹A⇩F⇩G' ♯* G›
         ‹⋀G A⇩F⇩G Ψ⇩F⇩G. ⟦mergeFrame F G = ⟨A⇩F⇩G, Ψ⇩F⇩G⟩; distinct A⇩F⇩G; A⇩F⇩G ♯* F; A⇩F⇩G ♯* G⟧ ⟹ ∃A⇩F Ψ⇩F A⇩G Ψ⇩G. A⇩F⇩G = A⇩F@A⇩G ∧ Ψ⇩F⇩G = Ψ⇩F ⊗ Ψ⇩G ∧ F = ⟨A⇩F, Ψ⇩F⟩ ∧ G = ⟨A⇩G, Ψ⇩G⟩ ∧ A⇩F ♯* Ψ⇩G ∧ A⇩G ♯* Ψ⇩F›
    obtain A⇩F Ψ⇩F A⇩G Ψ⇩G where "A⇩F⇩G' = A⇩F@A⇩G" and "([(x, y)] ∙ Ψ⇩F⇩G) = Ψ⇩F ⊗ Ψ⇩G" and FrF: "F = ⟨A⇩F, Ψ⇩F⟩" and FrG: "G = ⟨A⇩G, Ψ⇩G⟩" and "A⇩F ♯* Ψ⇩G" and "A⇩G ♯* Ψ⇩F"
      by metis

    from ‹A⇩F⇩G' = A⇩F@A⇩G› ‹A⇩F⇩G = y#A⇩F⇩G'› have  "A⇩F⇩G = (y#A⇩F)@A⇩G" by simp
    moreover from ‹A⇩F⇩G' = A⇩F@A⇩G› ‹y ♯ A⇩F⇩G'› ‹x ♯ A⇩F⇩G'› have "x ♯ A⇩F" and "y ♯ A⇩F" and "x ♯ A⇩G" and "y ♯ A⇩G" by simp+
    with ‹y ♯ G› ‹x ♯ G› ‹x ♯ A⇩F⇩G› FrG have "y ♯ Ψ⇩G" and "x ♯ Ψ⇩G" 
      by auto
    from ‹([(x, y)] ∙ Ψ⇩F⇩G) = Ψ⇩F ⊗ Ψ⇩G› have "([(x, y)] ∙ [(x, y)] ∙ Ψ⇩F⇩G) = [(x, y)] ∙ (Ψ⇩F ⊗ Ψ⇩G)"
      by simp
    with ‹x ♯ Ψ⇩G› ‹y ♯ Ψ⇩G› have "Ψ⇩F⇩G = ([(x, y)] ∙ Ψ⇩F) ⊗ Ψ⇩G" by(simp add: eqvts)
    moreover from FrF have "([(x, y)] ∙ F) = [(x, y)] ∙ ⟨A⇩F, Ψ⇩F⟩" by simp
    with ‹x ♯ A⇩F› ‹y ♯ A⇩F› have "([(x, y)] ∙ F) = ⟨A⇩F, [(x, y)] ∙ Ψ⇩F⟩" by(simp add: eqvts)
    hence "⦇νy⦈([(x, y)] ∙ F) = ⟨(y#A⇩F), [(x, y)] ∙ Ψ⇩F⟩" by(simp add: frame.inject)
    with ‹y ♯ F› have "⦇νx⦈F = ⟨(y#A⇩F), [(x, y)] ∙ Ψ⇩F⟩" by(simp add: alphaFrameRes)
    moreover with ‹A⇩G ♯* Ψ⇩F› have "([(x, y)] ∙ A⇩G) ♯* ([(x, y)] ∙ Ψ⇩F)" by(simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
    with ‹x ♯ A⇩G› ‹y ♯ A⇩G› have "A⇩G ♯* ([(x, y)] ∙ Ψ⇩F)" by simp
    moreover from ‹A⇩F ♯* Ψ⇩G› ‹y ♯ Ψ⇩G› have "(y#A⇩F) ♯* Ψ⇩G" by simp
    ultimately show ?case using FrG 
      by blast
  qed
  with A show ?thesis by blast
qed

lemma mergeFrameRes1[simp]:
  fixes A⇩F :: "name list"
  and   Ψ⇩F :: 'b
  and   x   :: name
  and   A⇩G :: "name list"
  and   Ψ⇩G :: 'b
  
  assumes "A⇩F ♯* Ψ⇩G"
  and     "A⇩F ♯* A⇩G"
  and     "x ♯ A⇩F"
  and     "x ♯ Ψ⇩F"
  and     "A⇩G ♯* Ψ⇩F"
  
  shows "(⟨A⇩F, Ψ⇩F⟩) ⊗⇩F (⦇νx⦈(⟨A⇩G, Ψ⇩G⟩)) = (⟨(A⇩F@x#A⇩G), Ψ⇩F ⊗ Ψ⇩G⟩)"
using assms
apply(fold frameResChain.simps)
by(rule mergeFrames) auto

lemma mergeFrameRes2[simp]:
  fixes A⇩F :: "name list"
  and   Ψ⇩F :: 'b
  and   x   :: name
  and   A⇩G :: "name list"
  and   Ψ⇩G :: 'b
  
  assumes "A⇩F ♯* Ψ⇩G"
  and     "A⇩G ♯* A⇩F"
  and     "x ♯ A⇩F"
  and     "x ♯ Ψ⇩F"
  and     "A⇩G ♯* Ψ⇩F"
  
  shows "(⟨A⇩F, Ψ⇩F⟩) ⊗⇩F (⦇νx⦈(⟨A⇩G, Ψ⇩G⟩)) = (⟨(A⇩F@x#A⇩G), Ψ⇩F ⊗ Ψ⇩G⟩)"
using assms
apply(fold frameResChain.simps)
by(rule mergeFrames) auto

lemma insertAssertionResChain[simp]:
  fixes xvec :: "name list"
  and   F    :: "'b frame"
  and   Ψ   :: 'b

  assumes "xvec ♯* Ψ"

  shows "insertAssertion (⦇ν*xvec⦈F) Ψ = ⦇ν*xvec⦈(insertAssertion F Ψ)"
using assms
by(induct xvec) auto

lemma extractFrameResChain[simp]:
  fixes xvec :: "name list"
  and   P    :: "('a, 'b, 'c) psi"

  shows "extractFrame(⦇ν*xvec⦈P) = ⦇ν*xvec⦈(extractFrame P)"
by(induct xvec) auto

lemma frameResFreshChain:
  fixes xvec :: "name list"
  and   F    :: "'b frame"

  assumes "xvec ♯* F"

  shows "⦇ν*xvec⦈F ≃⇩F F"
using assms
proof(induct xvec)
  case Nil
  thus ?case by simp
next
  case(Cons x xvec)
  thus ?case
    by auto (metis frameResPres frameResFresh FrameStatEqTrans)
qed

end

locale assertion = assertionAux SCompose SImp SBottom SChanEq
  for SCompose  :: "'b::fs_name ⇒ 'b ⇒ 'b"
  and SImp      :: "'b ⇒ 'c::fs_name ⇒ bool"
  and SBottom   :: 'b
  and SChanEq   :: "'a::fs_name ⇒ 'a ⇒ 'c" +

  assumes chanEqSym:     "SImp Ψ (SChanEq M N) ⟹ SImp Ψ (SChanEq N M)"
  and     chanEqTrans:   "⟦SImp Ψ (SChanEq M N); SImp Ψ (SChanEq N L)⟧ ⟹ SImp Ψ (SChanEq M L)"
  and     Composition:   "assertionAux.AssertionStatEq SImp Ψ Ψ' ⟹ assertionAux.AssertionStatEq SImp (SCompose Ψ Ψ'') (SCompose Ψ' Ψ'')"
  and     Identity:      "assertionAux.AssertionStatEq SImp (SCompose Ψ SBottom) Ψ"
  and     Associativity: "assertionAux.AssertionStatEq SImp (SCompose (SCompose Ψ Ψ') Ψ'') (SCompose Ψ (SCompose Ψ' Ψ''))"
  and     Commutativity: "assertionAux.AssertionStatEq SImp (SCompose Ψ Ψ') (SCompose Ψ' Ψ)"

begin

notation SCompose (infixr "⊗" 90)
notation SImp ("_ ⊢ _" [85, 85] 85)
notation SChanEq ("_ ↔ _" [90, 90] 90)
notation SBottom ("⊥" 90)

lemma compositionSym:
  fixes Ψ   :: 'b
  and   Ψ'  :: 'b
  and   Ψ'' :: 'b

  assumes "Ψ ≃ Ψ'"

  shows "Ψ'' ⊗ Ψ ≃ Ψ'' ⊗ Ψ'"
proof -
  have "Ψ'' ⊗ Ψ ≃ Ψ ⊗ Ψ''" by(rule Commutativity)
  moreover from assms have "Ψ ⊗ Ψ'' ≃ Ψ' ⊗ Ψ''" by(rule Composition)
  moreover have "Ψ' ⊗ Ψ'' ≃ Ψ'' ⊗ Ψ'" by(rule Commutativity)
  ultimately show ?thesis by(blast intro: AssertionStatEqTrans)
qed

lemma Composition':
  fixes Ψ    :: 'b
  and   Ψ'   :: 'b
  and   Ψ''  :: 'b
  and   Ψ''' :: 'b

  assumes "Ψ ≃ Ψ'"
  and     "Ψ'' ≃ Ψ'''"
  
  shows "Ψ ⊗ Ψ'' ≃ Ψ' ⊗ Ψ'''"
using assms
by(metis Composition Commutativity AssertionStatEqTrans)
  

lemma composition':
  fixes Ψ    :: 'b
  and   Ψ'   :: 'b
  and   Ψ''  :: 'b
  and   Ψ''' :: 'b

  assumes "Ψ ≃ Ψ'"

  shows "(Ψ ⊗ Ψ'') ⊗ Ψ''' ≃ (Ψ' ⊗ Ψ'') ⊗ Ψ'''"
proof -
  have "(Ψ ⊗ Ψ'') ⊗ Ψ''' ≃ Ψ ⊗ (Ψ'' ⊗ Ψ''')"
    by(rule Associativity)
  moreover from assms have "Ψ ⊗ (Ψ'' ⊗ Ψ''') ≃ Ψ' ⊗ (Ψ'' ⊗ Ψ''')"
    by(rule Composition)
  moreover have "Ψ' ⊗ (Ψ'' ⊗ Ψ''') ≃ (Ψ' ⊗ Ψ'') ⊗ Ψ'''"
    by(rule Associativity[THEN AssertionStatEqSym])
  ultimately show ?thesis by(blast dest: AssertionStatEqTrans)
qed

lemma associativitySym:
  fixes Ψ   :: 'b
  and   Ψ'  :: 'b
  and   Ψ'' :: 'b
  
  shows "(Ψ ⊗ Ψ') ⊗ Ψ'' ≃ (Ψ ⊗ Ψ'') ⊗ Ψ'"
proof -
  have "(Ψ ⊗ Ψ') ⊗ Ψ'' ≃ Ψ ⊗ (Ψ' ⊗ Ψ'')"
    by(rule Associativity)
  moreover have "Ψ ⊗ (Ψ' ⊗ Ψ'') ≃ Ψ ⊗ (Ψ'' ⊗ Ψ')"
    by(rule compositionSym[OF Commutativity])
  moreover have "Ψ ⊗ (Ψ'' ⊗ Ψ') ≃ (Ψ ⊗ Ψ'') ⊗ Ψ'"
    by(rule AssertionStatEqSym[OF Associativity])
  ultimately show ?thesis
    by(blast dest: AssertionStatEqTrans)
qed
(*
lemma frameChanEqSym:
  fixes F :: "'b frame"
  and   M :: 'a
  and   N :: 'a

  assumes "F ⊢⇩F M ↔ N"
  
  shows "F ⊢⇩F N ↔ M"
using assms
apply(auto simp add: FrameImp_def)
by(force intro: chanEqSym simp add: FrameImp_def)

lemma frameChanEqTrans:
  fixes F :: "'b frame"
  and   M :: 'a
  and   N :: 'a

  assumes "F ⊢⇩F M ↔ N"
  and     "F ⊢⇩F N ↔ L"
  
  shows "F ⊢⇩F M ↔ L"
proof -
  obtain A⇩F Ψ⇩F where "F = ⟨A⇩F, Ψ⇩F⟩" and "A⇩F ♯* (M, N, L)"
    by(rule freshFrame)
  with assms show ?thesis
    by(force dest: frameImpE intro: frameImpI chanEqTrans)
qed
*)
lemma frameIntAssociativity:
  fixes A⇩F  :: "name list"
  and   Ψ   :: 'b
  and   Ψ'  :: 'b
  and   Ψ'' :: 'b

  shows "⟨A⇩F, (Ψ ⊗ Ψ') ⊗ Ψ''⟩ ≃⇩F ⟨A⇩F, Ψ ⊗ (Ψ' ⊗ Ψ'')⟩"
by(induct A⇩F) (auto intro: Associativity frameResPres)

lemma frameIntCommutativity:
  fixes A⇩F  :: "name list"
  and   Ψ   :: 'b
  and   Ψ'  :: 'b

  shows "⟨A⇩F, Ψ ⊗ Ψ'⟩ ≃⇩F ⟨A⇩F, Ψ' ⊗ Ψ⟩"
by(induct A⇩F) (auto intro: Commutativity frameResPres)

lemma frameIntIdentity:
  fixes A⇩F :: "name list"
  and   Ψ⇩F :: 'b 

  shows "⟨A⇩F, Ψ⇩F ⊗ SBottom⟩ ≃⇩F ⟨A⇩F, Ψ⇩F⟩"
by(induct A⇩F) (auto intro: Identity frameResPres)

lemma frameIntComposition:
  fixes Ψ  :: 'b
  and   Ψ' :: 'b
  and   A⇩F :: "name list"
  and   Ψ⇩F :: 'b

  assumes "Ψ ≃ Ψ'"

  shows "⟨A⇩F, Ψ ⊗ Ψ⇩F⟩ ≃⇩F ⟨A⇩F, Ψ' ⊗ Ψ⇩F⟩"
using assms
by(induct A⇩F) (auto intro: Composition frameResPres)

lemma frameIntCompositionSym:
  fixes Ψ  :: 'b
  and   Ψ' :: 'b
  and   A⇩F :: "name list"
  and   Ψ⇩F :: 'b

  assumes "Ψ ≃ Ψ'"

  shows "⟨A⇩F, Ψ⇩F ⊗ Ψ⟩ ≃⇩F ⟨A⇩F, Ψ⇩F ⊗ Ψ'⟩"
using assms
by(induct A⇩F) (auto intro: compositionSym frameResPres)

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

  shows "F ⊗⇩F G ≃⇩F G ⊗⇩F F"
proof -
  obtain A⇩F Ψ⇩F where "F = ⟨A⇩F, Ψ⇩F⟩" and "A⇩F ♯* G"
    by(rule freshFrame)
  moreover obtain A⇩G Ψ⇩G where "G = ⟨A⇩G, Ψ⇩G⟩" and "A⇩G ♯* Ψ⇩F" and "A⇩G ♯* A⇩F"
    by(rule_tac C="(A⇩F, Ψ⇩F)" in freshFrame) auto
  moreover from ‹A⇩F ♯* G› ‹G = ⟨A⇩G, Ψ⇩G⟩› ‹A⇩G ♯* A⇩F› have "A⇩F ♯* Ψ⇩G"
    by auto
  ultimately show ?thesis
    by auto (metis FrameStatEqTrans frameChainAppend frameResChainComm frameIntCommutativity)
qed
  
lemma frameScopeExt:
  fixes x :: name
  and   F :: "'b frame"
  and   G :: "'b frame"

  assumes "x ♯ F"

  shows "⦇νx⦈(F ⊗⇩F G) ≃⇩F F ⊗⇩F (⦇νx⦈G)"
proof -
  have "⦇νx⦈(F ⊗⇩F G) ≃⇩F ⦇νx⦈(G ⊗⇩F F)"
    by(metis frameResPres frameCommutativity)
  with ‹x ♯ F› have "⦇νx⦈(F ⊗⇩F G) ≃⇩F (⦇νx⦈G) ⊗⇩F F"
    by simp
  moreover have "(⦇νx⦈G) ⊗⇩F F ≃⇩F F ⊗⇩F (⦇νx⦈G)"
    by(rule frameCommutativity)
  ultimately show ?thesis by(rule FrameStatEqTrans)
qed

lemma insertDoubleAssertionStatEq:
  fixes F  :: "'b frame"
  and   Ψ  :: 'b
  and   Ψ' :: 'b

  shows "insertAssertion(insertAssertion F Ψ) Ψ' ≃⇩F (insertAssertion F) (Ψ ⊗ Ψ')"
proof -
  obtain A⇩F Ψ⇩F where "F = ⟨A⇩F, Ψ⇩F⟩" and "A⇩F ♯* Ψ" and "A⇩F ♯* Ψ'" and "A⇩F ♯* (Ψ ⊗ Ψ')"
    by(rule_tac C="(Ψ, Ψ')" in freshFrame) auto
  thus ?thesis
    by auto (metis frameIntComposition Commutativity frameIntAssociativity FrameStatEqTrans FrameStatEqSym)
qed

lemma guardedStatEq:
  fixes P  :: "('a, 'b, 'c) psi"
  and   I  :: "('a, 'b, 'c) input"
  and   C  :: "('a, 'b, 'c) psiCase"
  and   A⇩P :: "name list"
  and   Ψ⇩P :: 'b

  shows "⟦guarded P; extractFrame P = ⟨A⇩P, Ψ⇩P⟩⟧ ⟹ Ψ⇩P ≃ ⊥ ∧ supp Ψ⇩P = ({}::name set)"
  and   "⟦guarded' I; extractFrame' I = ⟨A⇩P, Ψ⇩P⟩⟧ ⟹ Ψ⇩P ≃ ⊥ ∧ supp Ψ⇩P = ({}::name set)"
  and   "⟦guarded'' C; extractFrame'' C = ⟨A⇩P, Ψ⇩P⟩⟧ ⟹ Ψ⇩P ≃ ⊥ ∧ supp Ψ⇩P = ({}::name set)"
proof(nominal_induct P and I and C arbitrary: A⇩P Ψ⇩P rule: psi_input_psiCase.strong_inducts)
  case(PsiNil A⇩P Ψ⇩P)
  thus ?case by simp
next
  case(Output M N P A⇩P Ψ⇩P)
  thus ?case by simp
next
  case(Input M In  A⇩P Ψ⇩P)
  thus ?case by simp
next
  case(Case psiCase A⇩P Ψ⇩P)
  thus ?case by simp
next
  case(Par P Q A⇩P⇩Q Ψ⇩P⇩Q)
  from ‹guarded(P ∥ Q)› have "guarded P" and "guarded Q" by simp+
  obtain A⇩P Ψ⇩P where FrP: "extractFrame P = ⟨A⇩P, Ψ⇩P⟩" and "A⇩P ♯* Q" by(rule freshFrame)
  obtain A⇩Q Ψ⇩Q where FrQ: "extractFrame Q = ⟨A⇩Q, Ψ⇩Q⟩" and "A⇩Q ♯* A⇩P" and "A⇩Q ♯* Ψ⇩P" 
    by(rule_tac C="(A⇩P, Ψ⇩P)" in freshFrame) auto
  
  from ‹⋀A⇩P Ψ⇩P. ⟦guarded P; extractFrame P = ⟨A⇩P, Ψ⇩P⟩⟧ ⟹ Ψ⇩P ≃ ⊥ ∧ (supp Ψ⇩P = ({}::name set))› ‹guarded P› FrP
  have "Ψ⇩P ≃ ⊥" and "supp Ψ⇩P = ({}::name set)" by simp+
  from ‹⋀A⇩Q Ψ⇩Q. ⟦guarded Q; extractFrame Q = ⟨A⇩Q, Ψ⇩Q⟩⟧ ⟹ Ψ⇩Q ≃ ⊥ ∧ (supp Ψ⇩Q = ({}::name set))› ‹guarded Q› FrQ
  have "Ψ⇩Q ≃ ⊥" and "supp Ψ⇩Q = ({}::name set)" by simp+
  
  from ‹A⇩P ♯* Q› FrQ ‹A⇩Q ♯* A⇩P› have "A⇩P ♯* Ψ⇩Q" by(drule_tac extractFrameFreshChain) auto
  with ‹A⇩Q ♯* A⇩P› ‹A⇩Q ♯* Ψ⇩P› FrP FrQ ‹extractFrame(P ∥ Q) = ⟨A⇩P⇩Q, Ψ⇩P⇩Q⟩› have "⟨(A⇩P@A⇩Q), Ψ⇩P ⊗ Ψ⇩Q⟩ = ⟨A⇩P⇩Q, Ψ⇩P⇩Q⟩"
    by auto
  with ‹supp Ψ⇩P = {}› ‹supp Ψ⇩Q = {}› compSupp have "Ψ⇩P⇩Q = Ψ⇩P ⊗ Ψ⇩Q"
    by blast
  moreover from ‹Ψ⇩P ≃ ⊥› ‹Ψ⇩Q ≃ ⊥› have "Ψ⇩P ⊗ Ψ⇩Q ≃ ⊥"
    by(metis Composition Identity Associativity Commutativity AssertionStatEqTrans)
  ultimately show ?case using ‹supp Ψ⇩P = {}› ‹supp Ψ⇩Q = {}› compSupp
    by blast
next
  case(Res x P A⇩x⇩P Ψ⇩x⇩P)
  from ‹guarded(⦇νx⦈P)› have "guarded P" by simp
  moreover obtain A⇩P Ψ⇩P where FrP: "extractFrame P = ⟨A⇩P, Ψ⇩P⟩" by(rule freshFrame)
  moreover note ‹⋀A⇩P Ψ⇩P. ⟦guarded P; extractFrame P = ⟨A⇩P, Ψ⇩P⟩⟧ ⟹ Ψ⇩P ≃ ⊥ ∧ (supp Ψ⇩P = ({}::name set))›
  ultimately have "Ψ⇩P ≃ ⊥" and "supp Ψ⇩P = ({}::name set)" by auto
  from FrP ‹extractFrame(⦇νx⦈P) = ⟨A⇩x⇩P, Ψ⇩x⇩P⟩› have "⟨(x#A⇩P), Ψ⇩P⟩ = ⟨A⇩x⇩P, Ψ⇩x⇩P⟩" by simp
  with ‹supp Ψ⇩P = {}› have "Ψ⇩P = Ψ⇩x⇩P" by(auto simp del: frameResChain.simps)
  with ‹Ψ⇩P ≃ ⊥› ‹supp Ψ⇩P = {}› show ?case
    by simp
next
  case(Assert Ψ A⇩P Ψ⇩P)
  thus ?case by simp
next
  case(Bang P A⇩P Ψ⇩P)
  thus ?case by simp
next
  case(Trm M P)
  thus ?case by simp
next
  case(Bind x I)
  thus ?case by simp
next
  case EmptyCase
  thus ?case by simp
next
  case(Cond φ P psiCase)
  thus ?case by simp
qed

end

end