(* 
   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   \<Psi>    :: "'a::fs_name"
  and   yvec :: "name list"
  and   \<Psi>'   :: "'a::fs_name"

  assumes "\<langle>xvec, \<Psi>\<rangle> = \<langle>yvec, \<Psi>'\<rangle>"

  obtains p where "(set p) \<subseteq> (set xvec) \<times> set (yvec)" and "\<Psi>' = p \<bullet> \<Psi>"
proof -
  assume "\<And>p. \<lbrakk>set p \<subseteq> set xvec \<times> set yvec; \<Psi>' = p \<bullet> \<Psi>\<rbrakk> \<Longrightarrow> thesis"
  moreover obtain n where "n = length xvec" by auto
  with assms have "\<exists>p. (set p) \<subseteq> (set xvec) \<times> set (yvec) \<and> \<Psi>' = p \<bullet> \<Psi>"
  proof(induct n arbitrary: xvec yvec \<Psi> \<Psi>')
    case(0 xvec yvec \<Psi> \<Psi>')
    have Eq: "\<langle>xvec, \<Psi>\<rangle> = \<langle>yvec, \<Psi>'\<rangle>" 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 \<Psi> \<Psi>')
    from `Suc n = length xvec`
    obtain x xvec' where "xvec = x#xvec'" and "length xvec' = n"
      by(case_tac xvec) auto
    from `\<langle>xvec, \<Psi>\<rangle> = \<langle>yvec, \<Psi>'\<rangle>` `xvec = x # xvec'`
    obtain y yvec' where "\<langle>(x#xvec'), \<Psi>\<rangle> = \<langle>(y#yvec'), \<Psi>'\<rangle>"
      and "yvec = y#yvec'"
      by(case_tac yvec) auto
    hence EQ: "\<lparr>\<nu>x\<rparr>\<lparr>\<nu>*xvec'\<rparr>(FAssert \<Psi>) = \<lparr>\<nu>y\<rparr>\<lparr>\<nu>*yvec'\<rparr>(FAssert \<Psi>')"
      by simp
    have IH: "\<And>xvec yvec \<Psi> \<Psi>'. \<lbrakk>\<langle>xvec, (\<Psi>::'a)\<rangle> = \<langle>yvec, (\<Psi>'::'a)\<rangle>; n = length xvec\<rbrakk> \<Longrightarrow>
                                 \<exists>p. (set p) \<subseteq> (set xvec) \<times> (set yvec) \<and> \<Psi>' = p \<bullet> \<Psi>"
      by fact
    show ?case
    proof(cases "x=y")
      case True
      from EQ `x = y` have "\<langle>xvec', \<Psi>\<rangle> = \<langle>yvec', \<Psi>'\<rangle>" by(simp add: alpha frame.inject)
      then obtain p where S: "set p \<subseteq> set xvec' \<times> set yvec'" and "\<Psi>' = p \<bullet> \<Psi>" using `length xvec' = n` IH
        by blast
      from S have "set((x, y)#p) \<subseteq> set(x#xvec') \<times> set (y#yvec')" by auto
      moreover from `x = y` `\<Psi>' = p \<bullet> \<Psi>` have "\<Psi>' = ((x, y)#p) \<bullet> \<Psi>" by auto
      ultimately show ?thesis using `xvec = x#xvec'` `yvec = y#yvec'` by blast
    next
      case False
      from EQ `x \<noteq> y` have EQ': "\<langle>xvec', \<Psi>\<rangle> = ([(x, y)] \<bullet> \<langle>yvec', \<Psi>'\<rangle>)" 
                       and xFresh\<Psi>': "x \<sharp> \<lparr>\<nu>*yvec'\<rparr>(FAssert \<Psi>')"
        by(simp add: frame.inject alpha)+
    
      show ?thesis
      proof(cases "x \<sharp> \<langle>xvec', \<Psi>\<rangle>")
        case True
        from EQ `x \<sharp> \<langle>xvec', \<Psi>\<rangle>` have "y \<sharp> \<langle>yvec', \<Psi>'\<rangle>"
          by(rule frameEqFresh)
        with xFresh\<Psi>' EQ' have "\<langle>xvec', \<Psi>\<rangle> = \<langle>yvec', \<Psi>'\<rangle>" 
          by(simp)
        with `length xvec' = n` IH
        obtain p where S: "(set p) \<subseteq> (set xvec') \<times> (set yvec')" and "\<Psi>' = p \<bullet> \<Psi>"
          by blast
        from S have "(set p) \<subseteq> set(x#xvec') \<times> set(y#yvec')" by auto
        with `xvec = x#xvec'` `yvec=y#yvec'` `\<Psi>' = p \<bullet> \<Psi>`
        show ?thesis by blast
      next
        case False
        from `\<not>(x \<sharp> \<lparr>\<nu>*xvec'\<rparr>(FAssert \<Psi>))` have xSupp\<Psi>: "x \<in> supp(\<langle>xvec', \<Psi>\<rangle>)"
          by(simp add: fresh_def)
        with EQ have "y \<in> supp (\<langle>yvec', \<Psi>'\<rangle>)"
          by(rule frameEqSupp)
        hence "y \<sharp> yvec'"
          by(induct yvec') (auto simp add: frame.supp abs_supp)

        with `x \<sharp> yvec'` EQ' have "\<langle>xvec', \<Psi>\<rangle> = \<langle>yvec', ([(x, y)] \<bullet> \<Psi>')\<rangle>"
          by(simp add: eqvts)
        with  `xvec' \<sharp>* yvec'` `length xvec' = n` IH
        obtain p where S: "(set p) \<subseteq> (set xvec') \<times> (set yvec')" and "distinctPerm p" and "([(x, y)] \<bullet> \<Psi>') = p \<bullet> \<Psi>"
          by blast
        
        from xSupp\<Psi> have "x \<sharp> xvec'"
          by(induct xvec') (auto simp add: frame.supp abs_supp)      
        with `x \<sharp> yvec'` `y \<sharp> xvec'` `y \<sharp> yvec'` S have "x \<sharp> p" and "y \<sharp> p"
          apply(induct p)
          by(auto simp add: name_list_supp) (auto simp add: fresh_def) 
        from S have "(set ((x, y)#p)) \<subseteq> (set(x#xvec')) \<times> (set(y#yvec'))"
          by force
        moreover from `x \<noteq> y` `x \<sharp> p` `y \<sharp> p` S `distinctPerm p`
        have "distinctPerm((x,y)#p)" by simp
        moreover from `x \<sharp> p` `y \<sharp> p` `x \<sharp> xvec'` `y \<sharp> xvec'` have "y#(p \<bullet> xvec') = ((x, y)#p) \<bullet> (x#xvec')" 
          by(simp add: eqvts calc_atm freshChainSimps)
        moreover from `([(x, y)] \<bullet> \<Psi>') = p \<bullet> \<Psi>`
        have "([(x, y)] \<bullet> [(x, y)] \<bullet> \<Psi>') = [(x, y)] \<bullet> p \<bullet> \<Psi>"
          by(simp add: pt_bij)
        hence "\<Psi>' = ((x, y)#p) \<bullet> \<Psi>" 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 (0) = ⟨ε, ⊥⟩"
| "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   \<Psi>    :: 'b
  and   \<Psi>'   :: 'b

  shows "xvec \<sharp>* (\<Psi> \<otimes> \<Psi>') = ((xvec \<sharp>* \<Psi>) \<and> xvec \<sharp>* \<Psi>')"
  and   "Xs \<sharp>* (\<Psi> \<otimes> \<Psi>') = ((Xs \<sharp>* \<Psi>) \<and> Xs \<sharp>* \<Psi>')"
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_FG :: "name list"
  and   Ψ_FG :: 'b

  assumes "mergeFrame F G = ⟨A_FG, Ψ_FG⟩"
  and     "distinct A_FG"
  and     "A_FG ♯* F"
  and     "A_FG ♯* G"

  obtains A_F Ψ_F A_G Ψ_G where "A_FG = A_F@A_G" and "Ψ_FG = Ψ_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_FG = A_F@A_G; Ψ_FG = Ψ_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_FG = A_F@A_G ∧ Ψ_FG = Ψ_F ⊗ Ψ_G ∧ F = ⟨A_F, Ψ_F⟩ ∧ G = ⟨A_G, Ψ_G⟩ ∧ A_F ♯* Ψ_G ∧ A_G ♯* Ψ_F"
  proof(nominal_induct F avoiding: G A_FG Ψ_FG rule: frame.strong_induct)
    case(FAssert Ψ G A_FG Ψ_FG)
    thus ?case
      apply auto
      apply(rule_tac x="[]" in exI) 
      by(drule_tac insertAssertionE) auto
  next
    case(FRes x F G A_FG Ψ_FG)
    from ‹mergeFrame ((νx)F) G = ⟨A_FG, Ψ_FG⟩› ‹x ♯ G›
    obtain y A_FG' where "A_FG = y#A_FG'" by(induct A_FG) auto
    with ‹A_FG ♯* ((νx)F)› ‹x ♯ A_FG› have "A_FG' ♯* F" and "x ♯ A_FG'"
      by(auto simp add: supp_list_cons fresh_star_def fresh_def name_list_supp abs_supp frame.supp)
    from ‹A_FG = y#A_FG'› ‹A_FG ♯* G› have "y ♯ G" and "A_FG' ♯* G" by simp+
    from ‹A_FG = y#A_FG'› ‹A_FG ♯* ((νx)F)› ‹x ♯ A_FG› have "y ♯ F" and "A_FG' ♯* F"
      apply(auto simp add: abs_fresh frameResChainFreshSet)
      apply(hypsubst_thin)
      by(induct A_FG') (auto simp add: abs_fresh)
    from ‹distinct A_FG› ‹A_FG = y#A_FG'› have "y ♯ A_FG'" and "distinct A_FG'" by auto
    
    with ‹A_FG = y#A_FG'› ‹mergeFrame ((νx)F) G = ⟨A_FG, Ψ_FG⟩› ‹x ♯ G› ‹x ♯ A_FG› ‹y ♯ A_FG'›
    have "mergeFrame F G = ⟨A_FG', [(x, y)] ∙ Ψ_FG⟩"
      by(simp add: frame.inject alpha eqvts)
    with ‹distinct A_FG'› ‹A_FG' ♯* F› ‹A_FG' ♯* G›
         ‹∧G A_FG Ψ_FG. [mergeFrame F G = ⟨A_FG, Ψ_FG⟩; distinct A_FG; A_FG ♯* F; A_FG ♯* G] ==> ∃A_F Ψ_F A_G Ψ_G. A_FG = A_F@A_G ∧ Ψ_FG = Ψ_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_FG' = A_F@A_G" and "([(x, y)] ∙ Ψ_FG) = Ψ_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_FG' = A_F@A_G› ‹A_FG = y#A_FG'› have  "A_FG = (y#A_F)@A_G" by simp
    moreover from ‹A_FG' = A_F@A_G› ‹y ♯ A_FG'› ‹x ♯ A_FG'› 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_FG› FrG have "y ♯ Ψ_G" and "x ♯ Ψ_G" 
      by auto
    from ‹([(x, y)] ∙ Ψ_FG) = Ψ_F ⊗ Ψ_G› have "([(x, y)] ∙ [(x, y)] ∙ Ψ_FG) = [(x, y)] ∙ (Ψ_F ⊗ Ψ_G)"
      by simp
    with ‹x ♯ Ψ_G› ‹y ♯ Ψ_G› have "Ψ_FG = ([(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 \<turnstile>\<^sub>F M \<leftrightarrow> N"
  
  shows "F \<turnstile>\<^sub>F N \<leftrightarrow> 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 \<turnstile>\<^sub>F M \<leftrightarrow> N"
  and     "F \<turnstile>\<^sub>F N \<leftrightarrow> L"
  
  shows "F \<turnstile>\<^sub>F M \<leftrightarrow> L"
proof -
  obtain A\<^sub>F \<Psi>\<^sub>F where "F = \<langle>A\<^sub>F, \<Psi>\<^sub>F\<rangle>" and "A\<^sub>F \<sharp>* (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_PQ Ψ_PQ)
  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_PQ, Ψ_PQ⟩› have "⟨(A_P@A_Q), Ψ_P ⊗ Ψ_Q⟩ = ⟨A_PQ, Ψ_PQ⟩"
    by auto
  with ‹supp Ψ_P = {}› ‹supp Ψ_Q = {}› compSupp have "Ψ_PQ = Ψ_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_xP Ψ_xP)
  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_xP, Ψ_xP⟩› have "⟨(x#A_P), Ψ_P⟩ = ⟨A_xP, Ψ_xP⟩" by simp
  with ‹supp Ψ_P = {}› have "Ψ_P = Ψ_xP" 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