Theory Psi_Calculi.Frame

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

  assumes "y  F"

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

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

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

  assumes "xvec, Ψ = yvec, Ψ'"

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

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

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

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

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

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

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

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

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

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

  obtains p where "(set p)  (set xvec) × set (yvec)" and "distinctPerm p" and "Ψ' = p  Ψ"
proof -
  assume "p. set p  set xvec × set yvec; distinctPerm p; Ψ' = p  Ψ  thesis"
  moreover obtain n where "n = length xvec" by auto
  with assms have "p. (set p)  (set xvec) × set (yvec)  distinctPerm p   Ψ' = p  Ψ"
  proof(induct n arbitrary: xvec yvec Ψ Ψ')
    case(0 xvec yvec Ψ Ψ')
    have Eq: "xvec, Ψ = yvec, Ψ'" by fact
    from 0 = length xvec have "xvec = []" by auto
    moreover with Eq have "yvec = []"
      by(case_tac yvec) auto
    ultimately show ?case using Eq
      by(simp add: frame.inject)
  next
    case(Suc n xvec yvec Ψ Ψ')
    from Suc n = length xvec
    obtain x xvec' where "xvec = x#xvec'" and "length xvec' = n"
      by(case_tac xvec) auto
    from xvec, Ψ = yvec, Ψ' xvec = x # xvec'
    obtain y yvec' where "(x#xvec'), Ψ = (y#yvec'), Ψ'"
      and "yvec = y#yvec'"
      by(case_tac yvec) auto
    hence EQ: "⦇νx⦇ν*xvec'(FAssert Ψ) = ⦇νy⦇ν*yvec'(FAssert Ψ')"
      by simp
    from xvec = x#xvec' yvec=y#yvec' xvec ♯* yvec
    have "x  y" and "xvec' ♯* yvec'" and "x  yvec'" and "y  xvec'"
      by auto
    have IH: "xvec yvec Ψ Ψ'. xvec, (Ψ::'a) = yvec, (Ψ'::'a); xvec ♯* yvec; n = length xvec 
                                 p. (set p)  (set xvec) × (set yvec)  distinctPerm p   Ψ' = p  Ψ"
      by fact

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

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

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

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

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

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

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

  obtains p where "(set p)  (set xvec) × set (p  xvec)" and "distinctPerm p" and "yvec = p  xvec" and "Ψ' = p  Ψ"
proof -
  assume "p. set p  set xvec × set (p  xvec); distinctPerm p; yvec = p  xvec; Ψ' = p  Ψ  thesis"
  moreover obtain n where "n = length xvec" by auto
  with assms have "p. (set p)  (set xvec) × set (yvec)  distinctPerm p   yvec = p  xvec  Ψ' = p  Ψ"
  proof(induct n arbitrary: xvec yvec Ψ Ψ')
    case(0 xvec yvec Ψ Ψ')
    have Eq: "xvec, Ψ = yvec, Ψ'" by fact
    from 0 = length xvec have "xvec = []" by auto
    moreover with Eq have "yvec = []"
      by(case_tac yvec) auto
    ultimately show ?case using Eq
      by(simp add: frame.inject)
  next
    case(Suc n xvec yvec Ψ Ψ')
    from Suc n = length xvec
    obtain x xvec' where "xvec = x#xvec'" and "length xvec' = n"
      by(case_tac xvec) auto
    from xvec, Ψ = yvec, Ψ' xvec = x # xvec'
    obtain y yvec' where "(x#xvec'), Ψ = (y#yvec'), Ψ'"
      and "yvec = y#yvec'"
      by(case_tac yvec) auto
    hence EQ: "⦇νx⦇ν*xvec'(FAssert Ψ) = ⦇νy⦇ν*yvec'(FAssert Ψ')"
      by simp
    from xvec = x#xvec' yvec=y#yvec' xvec ♯* yvec
    have "x  y" and "xvec' ♯* yvec'" and "x  yvec'" and "y  xvec'"
      by auto
    from distinct xvec distinct yvec xvec=x#xvec' yvec=y#yvec' have "x  xvec'" and "y  yvec'" and "distinct xvec'" and "distinct yvec'"
      by simp+
    have IH: "xvec yvec Ψ Ψ'. xvec, (Ψ::'a) = yvec, (Ψ'::'a); xvec ♯* yvec; distinct xvec; distinct yvec; n = length xvec  p. (set p)  (set xvec) × (set yvec)  distinctPerm p   yvec = p  xvec  Ψ' = p  Ψ"
      by fact
    from EQ x  y  x  yvec' y  yvec' have "xvec', Ψ = yvec', ([(x, y)]  Ψ')"
      by(simp add: frame.inject alpha eqvts)
    with xvec' ♯* yvec' distinct xvec' distinct yvec' length xvec' = n IH
    obtain p where S: "(set p)  (set xvec') × (set yvec')" and "distinctPerm p" and "yvec' = p  xvec'" and "[(x, y)]  Ψ' = p  Ψ"
      by metis
    from S have "set((x, y)#p)  set(x#xvec') × set(y#yvec')" by auto
    moreover from x  xvec' x  yvec' y  xvec' y  yvec' S have "x  p" and "y  p"
      apply(induct p)
      by(auto simp add: name_list_supp) (auto simp add: fresh_def) 

    with S distinctPerm p x  y have "distinctPerm((x, y)#p)" by auto
    moreover from yvec' = p  xvec' x  p y  p x  xvec' y  xvec' have "(y#yvec') = ((x, y)#p)  (x#xvec')"
      by(simp add: freshChainSimps calc_atm)
    moreover from ([(x, y)]  Ψ') = p  Ψ
    have "([(x, y)]  [(x, y)]  Ψ') = [(x, y)]  p  Ψ"
      by(simp add: pt_bij)
    hence "Ψ' = ((x, y)#p)  Ψ"
      by simp
    ultimately show ?case using xvec=x#xvec' yvec=y#yvec'
      by blast
  qed
  ultimately show ?thesis by blast
qed

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

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

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

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

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

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

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

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

begin

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

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

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

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

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

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

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

  assumes "x  Ψ"
  and     "x  Ψ'"

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

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

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

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

  assumes "x  M"
  and     "x  N"

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

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

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

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

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

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

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

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

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

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

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

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

  assumes "Ψ  Ψ'"
  and     "Ψ  Φ"

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

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

  assumes "Ψ  Ψ'"
  and     "Ψ  Φ"

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

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

  assumes "Ψ  Ψ'"

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

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

  assumes "Ψ  Ψ'"

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

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

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

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

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

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

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

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

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

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

  assumes "Ψ  Ψ'"

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

  assumes "F F Φ"

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

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

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

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

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

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

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

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

  assumes "F F G"

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

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

  assumes "F F G"

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

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

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

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

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

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

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

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

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

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

  assumes "F F G"

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

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

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

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

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

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

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

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

nominal_primrec 
   insertAssertion :: "'b frame  'b  'b frame"
where
  "insertAssertion (FAssert Ψ) Ψ' = FAssert (Ψ'  Ψ)"
| "x  Ψ'  insertAssertion (⦇νxF) Ψ' = ⦇νx(insertAssertion F Ψ')"
apply(finite_guess add: fsCompose)+
apply(rule TrueI)+
apply(simp add: abs_fresh)
apply(rule supports_fresh[of "supp Ψ'"])
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 (⦇νxF) 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 (MI) = ⟨ε, "
| "extractFrame (MN⟩.P) = ⟨ε, "
| "extractFrame (Case C) = ⟨ε, "
| "extractFrame (P  Q) = (extractFrame P) F (extractFrame Q)"
| "extractFrame ((Ψ::('a, 'b, 'c) psi)) = ⟨ε, Ψ" 

| "extractFrame (⦇νxP) = ⦇ν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 ♯* (⦇ν*yvecF)) = (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 ♯* (⦇ν*yvecF) = 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  (⦇ν*xvecF) = 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 AF    :: "name list"
  and   ΨF   :: 'b
  and   xvec  :: "name list"

  assumes "xvec ♯* (AF, ΨF)"

  shows "xvec ♯* AF  xvec ♯* ΨF"
  and   "AF ♯* xvec  xvec ♯* ΨF"
proof -
  from assms have "(set xvec) ♯* (AF, ΨF)"
    by(simp add: fresh_star_def)
  moreover assume "xvec ♯* AF"
  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) ♯* (AF, ΨF)"
    by(simp add: fresh_star_def)
  moreover assume "AF ♯* 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 AF :: "name list"
  and   ΨF :: 'b
  and   Ψ  :: 'b
  
  assumes "AF ♯* Ψ"

  shows "insertAssertion (AF, ΨF) Ψ = AF, Ψ  ΨF"
using assms
by(induct AF arbitrary: F) auto

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

  assumes "AF ♯* Ψ"

  shows "(AF, ΨF) F ⟨ε, Ψ = AF, ΨF  Ψ"
using assms
by(induct AF arbitrary: F) auto

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

  assumes "AF ♯* AG"
  and     "AF ♯* ΨG"
  and     "AG ♯* ΨF"

  shows "(AF, ΨF) F (AG, ΨG) = ((AF@AG), ΨF  ΨG)"
using assms
by(induct AF) auto

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

  shows "⦇νxF F F"
proof(auto simp add: FrameStatImp_def)
  fix φ::'c
  obtain AF ΨF where Feq: "F = AF, ΨF" and "AF ♯* (x, φ)"
    by(rule freshFrame)
  from AF ♯* (x, φ) have "x  AF" and "AF ♯* φ" by simp+
  obtain y where "y  φ" and "y  F" and "x  y"
    by(generate_fresh "name", auto)
  
  assume "⦇νxF F φ"
  with y  F have "⦇νy([(x, y)]  F) F φ" by(simp add: alphaFrameRes)
  with x  F y  F have "⦇νyF F φ" by simp
  with Feq have "(y#AF), ΨF F φ" by simp
  with Feq AF ♯* φ 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 ⦇νxF"
proof(auto simp add: FrameStatImp_def)
  fix φ::'c
  obtain AF ΨF where Feq: "F = AF, ΨF" and "AF ♯* (x, φ)"
    by(rule freshFrame)
  from AF ♯* (x, φ) have "x  AF" and "AF ♯* φ" by simp+
  obtain y where "y  φ" and "y  F" and "x  y"
    by(generate_fresh "name", auto)
  
  assume "F F φ"
  with Feq AF ♯* φ y  φ have "(y#AF), ΨF F φ"
    by(force intro: frameImpI dest: frameImpE simp del: frameResChain.simps)
  moreover with y  F x  F Feq show "⦇νxF F φ"
    by(subst alphaFrameRes) auto
qed

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

  shows "⦇νxF 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 "⦇νxF F ⦇νxG"
proof(auto simp add: FrameStatImp_def)
  fix φ::'c
  obtain AF ΨF where Feq: "F = AF, ΨF" and "AF ♯* (x, φ)"
    by(rule freshFrame)
  from AF ♯* (x, φ) have "x  AF" and "AF ♯* φ" by simp+
  obtain y where "y  AF" and "y  F" and "y  G"
             and "x  y" and "y  φ"
    by(generate_fresh "name", auto)
  assume "⦇νxF F φ"
  with y  F have "⦇νy([(x, y)]  F) F φ" by(simp add: alphaFrameRes)
  with Feq x  AF y  AF have "(y#AF), [(x, y)]  ΨF F φ" by(simp add: eqvts)
  with y  φ AF ♯* φ have "AF, [(x, y)]  ΨF F φ"
    by(force intro: frameImpI dest: frameImpE simp del: frameResChain.simps)
  hence "([(x, y)]  AF, [(x, y)]  ΨF) F ([(x, y)]  φ)"
    by(rule frameImpClosed)
  with x  AF y  AF 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 AG ΨG where Geq: "G = AG, ΨG" and "AG ♯* (x, y, φ)"
    by(rule freshFrame)
  from AG ♯* (x, y, φ) have "x  AG" and "y  AG" and "AG ♯* φ" by simp+
  from G F [(x, y)]  φ have "([(x, y)]  G) F [(x, y)]  [(x, y)]  φ"
    by(rule frameImpClosed)
  with Geq x  AG y  AG have "AG, [(x, y)]  ΨG F φ" by(simp add: eqvts)
  with y  φ AG ♯* φ have "(y#AG), [(x, y)]  ΨG F φ"
    by(force intro: frameImpI dest: frameImpE simp del: frameResChain.simps)
  with y  G x  AG y  AG Geq show "⦇νxG 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 "⦇νxF F ⦇νxG"
using assms
by(auto simp add: FrameStatEq_def intro: frameImpResPres)

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

  shows "⦇νx(⦇νyF) F ⦇νy(⦇νxF)"
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 AF ΨF where Feq: "F = AF, ΨF" and "AF ♯* (x, y, φ)"
      by(rule freshFrame)
    then have "x  AF" and "y  AF" and "AF ♯* φ" by simp+

    obtain x'::name where "x'  x" and "x'  y" and "x'  F" and "x'  φ" and "x'  AF"
      by(generate_fresh "name") auto
    obtain y'::name where "y'  x" and "y'  y" and "y'  x'" and "y'  F" and "y'  φ" and "y'  AF"
      by(generate_fresh "name") auto
  
    from y'  F have "⦇νx(⦇νyF) = ⦇ν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(⦇νyF)= ⦇νx'(⦇νy'(⦇ν*AF(FAssert([(x, x')]  [(y, y')]  ΨF))))"
      using  Feq x  AF x'  AF y  AF y'  AF
      by(simp add: eqvts)

    from x'  F have "⦇νy(⦇νxF) = ⦇ν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(⦇νxF)= ⦇νy'(⦇νx'(⦇ν*AF(FAssert([(x, x')]  [(y, y')]  ΨF))))"
      using  Feq x  AF x'  AF y  AF y'  AF
      by(simp add: eqvts)

    from x'  φ y'  φ AF ♯* φ
    have "(x'#y'#AF), [(x, x')]  [(y, y')]  ΨF F φ = (y'#x'#AF), [(x, x')]  [(y, y')]  ΨF F φ"
      by(force dest: frameImpE intro: frameImpI simp del: frameResChain.simps)
    with A B have "(⦇νx(⦇νyF)) F φ = (⦇νy(⦇νxF)) F φ"
      by simp
    moreover assume "(⦇νx(⦇νyF)) F φ"
    ultimately show "(⦇νy(⦇νxF)) F φ" by simp
  qed
qed

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

  shows "⦇νx(⦇νyF) F ⦇νy(⦇νxF)"
by(auto simp add: FrameStatEq_def intro: frameImpResComm)

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

  shows "⦇νx(⦇ν*xvecF) F ⦇ν*xvec(⦇νxF)"
by(induct xvec) (auto intro: frameImpResComm FrameStatImpTrans frameImpResPres)

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

  shows "⦇ν*xvec(⦇νxF) F ⦇νx(⦇ν*xvecF)"
by(induct xvec) (auto intro: frameImpResComm FrameStatImpTrans frameImpResPres)

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

  shows "⦇νx(⦇ν*xvecF) F ⦇ν*xvec(⦇νxF)"
by(induct xvec) (auto intro: frameResComm FrameStatEqTrans frameResPres)

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

  shows "⦇ν*xvec(⦇ν*yvecF) F ⦇ν*yvec(⦇ν*xvecF)"
by(induct xvec) (auto intro: frameImpResCommLeft' FrameStatImpTrans frameImpResPres)

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

  shows "⦇ν*xvec(⦇ν*yvecF) F ⦇ν*yvec(⦇ν*xvecF)"
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(⦇ν*xvecP) F ⦇ν*xvec(extractFrame P)"
by(induct xvec) (auto intro: frameImpResPres)

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

  shows "extractFrame(⦇ν*xvecP) 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(⦇ν*xvecP)) Ψ 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(⦇ν*xvecP)) Ψ 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 "⦇ν*xvecF F ⦇ν*xvecG"
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 "⦇ν*xvecF F ⦇ν*xvecG"
using assms
by(induct xvec) (auto intro: frameResPres)

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

  assumes "insertAssertion F Ψ = AF, Ψ'"
  and     "AF ♯* F"
  and     "AF ♯* Ψ"
  and     "distinct AF"

  obtains ΨF where "F = AF, ΨF" and "Ψ' = Ψ  ΨF"
proof -
  assume A: "ΨF. F = AF, ΨF; Ψ' = Ψ  ΨF  thesis"
  from assms have "ΨF. F = AF, ΨF  Ψ' = Ψ  ΨF"
  proof(nominal_induct F avoiding: Ψ AF Ψ' rule: frame.strong_induct)
    case(FAssert Ψ AF Ψ')
    thus ?case by auto
  next
    case(FRes x F Ψ AF Ψ')
    from insertAssertion (⦇νxF) Ψ = AF, Ψ' x  Ψ
    obtain y AF' where "AF = y#AF'" by(induct AF) auto
    with insertAssertion (⦇νxF) Ψ = AF, Ψ' x  Ψ x  AF
    have A: "insertAssertion F Ψ = ([(x, y)]  AF'), [(x, y)]  Ψ'"
      by(simp add: frame.inject alpha eqvts)
    from AF = y#AF' AF ♯* Ψ have "y  Ψ" and "AF' ♯* Ψ" by simp+
    from distinct AF AF = y#AF' have "y  AF'" and "distinct AF'" by auto
    from AF ♯* (⦇νxF) x  AF AF = y#AF' have "y  F" and "AF' ♯* F" and "x  AF'"
      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  AF' y  AF' have "([(x, y)]  AF') ♯* F" by simp
    from AF' ♯* Ψ have "([(x, y)]  AF') ♯* ([(x, y)]  Ψ)" by(simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
    with x  Ψ y  Ψ have "([(x, y)]  AF') ♯* Ψ" by simp
    with Ψ AF Ψ'. insertAssertion F Ψ = AF, Ψ'; AF ♯* F; AF ♯* Ψ; distinct AF  ΨF. F = AF, ΨF  Ψ' = Ψ  ΨF A 
         ([(x, y)]  AF') ♯* F distinct AF' x  AF' y  AF'
    obtain ΨF where Feq: "F = AF', ΨF" and Ψeq: "([(x, y)]  Ψ') = Ψ  ΨF"
      by force
    
    from Feq have "⦇νxF =  (x#AF'), ΨF" by(simp add: frame.inject)
    hence "([(x, y)]  ⦇νxF) = [(x, y)]  (x#AF'), ΨF" by simp
    hence "⦇νxF = AF, [(x, y)]  ΨF" using y  F AF = y#AF' x  AF y  AF'
      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   AFG :: "name list"
  and   ΨFG :: 'b

  assumes "mergeFrame F G = AFG, ΨFG"
  and     "distinct AFG"
  and     "AFG ♯* F"
  and     "AFG ♯* G"

  obtains AF ΨF AG ΨG where "AFG = AF@AG" and "ΨFG = ΨF  ΨG" and "F = AF, ΨF" and "G = AG, ΨG" and "AF ♯* ΨG" and "AG ♯* ΨF"
proof -
  assume A: "AF AG ΨF ΨG. AFG = AF@AG; ΨFG = ΨF  ΨG; F = AF, ΨF; G = AG, ΨG; AF ♯* ΨG; AG ♯* ΨF  thesis"
  from assms have "AF ΨF AG ΨG. AFG = AF@AG  ΨFG = ΨF  ΨG  F = AF, ΨF  G = AG, ΨG  AF ♯* ΨG  AG ♯* ΨF"
  proof(nominal_induct F avoiding: G AFG ΨFG rule: frame.strong_induct)
    case(FAssert Ψ G AFG ΨFG)
    thus ?case
      apply auto
      apply(rule_tac x="[]" in exI) 
      by(drule_tac insertAssertionE) auto
  next
    case(FRes x F G AFG ΨFG)
    from mergeFrame (⦇νxF) G = AFG, ΨFG x  G
    obtain y AFG' where "AFG = y#AFG'" by(induct AFG) auto
    with AFG ♯* (⦇νxF) x  AFG have "AFG' ♯* F" and "x  AFG'"
      by(auto simp add: supp_list_cons fresh_star_def fresh_def name_list_supp abs_supp frame.supp)
    from AFG = y#AFG' AFG ♯* G have "y  G" and "AFG' ♯* G" by simp+
    from AFG = y#AFG' AFG ♯* (⦇νxF) x  AFG have "y  F" and "AFG' ♯* F"
      apply(auto simp add: abs_fresh frameResChainFreshSet)
      apply(hypsubst_thin)
      by(induct AFG') (auto simp add: abs_fresh)
    from distinct AFG AFG = y#AFG' have "y  AFG'" and "distinct AFG'" by auto
    
    with AFG = y#AFG' mergeFrame (⦇νxF) G = AFG, ΨFG x  G x  AFG y  AFG'
    have "mergeFrame F G = AFG', [(x, y)]  ΨFG"
      by(simp add: frame.inject alpha eqvts)
    with distinct AFG' AFG' ♯* F AFG' ♯* G
         G AFG ΨFG. mergeFrame F G = AFG, ΨFG; distinct AFG; AFG ♯* F; AFG ♯* G  AF ΨF AG ΨG. AFG = AF@AG  ΨFG = ΨF  ΨG  F = AF, ΨF  G = AG, ΨG  AF ♯* ΨG  AG ♯* ΨF
    obtain AF ΨF AG ΨG where "AFG' = AF@AG" and "([(x, y)]  ΨFG) = ΨF  ΨG" and FrF: "F = AF, ΨF" and FrG: "G = AG, ΨG" and "AF ♯* ΨG" and "AG ♯* ΨF"
      by metis

    from AFG' = AF@AG AFG = y#AFG' have  "AFG = (y#AF)@AG" by simp
    moreover from AFG' = AF@AG y  AFG' x  AFG' have "x  AF" and "y  AF" and "x  AG" and "y  AG" by simp+
    with y  G x  G x  AFG 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)]  AF, ΨF" by simp
    with x  AF y  AF have "([(x, y)]  F) = AF, [(x, y)]  ΨF" by(simp add: eqvts)
    hence "⦇νy([(x, y)]  F) = (y#AF), [(x, y)]  ΨF" by(simp add: frame.inject)
    with y  F have "⦇νxF = (y#AF), [(x, y)]  ΨF" by(simp add: alphaFrameRes)
    moreover with AG ♯* ΨF have "([(x, y)]  AG) ♯* ([(x, y)]  ΨF)" by(simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
    with x  AG y  AG have "AG ♯* ([(x, y)]  ΨF)" by simp
    moreover from AF ♯* ΨG y  ΨG have "(y#AF) ♯* ΨG" by simp
    ultimately show ?case using FrG 
      by blast
  qed
  with A show ?thesis by blast
qed

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

lemma mergeFrameRes2[simp]:
  fixes AF :: "name list"
  and   ΨF :: 'b
  and   x   :: name
  and   AG :: "name list"
  and   ΨG :: 'b
  
  assumes "AF ♯* ΨG"
  and     "AG ♯* AF"
  and     "x  AF"
  and     "x  ΨF"
  and     "AG ♯* ΨF"
  
  shows "(AF, ΨF) F (⦇νx(AG, ΨG)) = ((AF@x#AG), Ψ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 (⦇ν*xvecF) Ψ = ⦇ν*xvec(insertAssertion F Ψ)"
using assms
by(induct xvec) auto

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

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

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

  assumes "xvec ♯* F"

  shows "⦇ν*xvecF 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 AF ΨF where "F = ⟨AF, ΨF⟩" and "AF ♯* (M, N, L)"
    by(rule freshFrame)
  with assms show ?thesis
    by(force dest: frameImpE intro: frameImpI chanEqTrans)
qed
*)
lemma frameIntAssociativity:
  fixes AF  :: "name list"
  and   Ψ   :: 'b
  and   Ψ'  :: 'b
  and   Ψ'' :: 'b

  shows "AF, (Ψ  Ψ')  Ψ'' F AF, Ψ  (Ψ'  Ψ'')"
by(induct AF) (auto intro: Associativity frameResPres)

lemma frameIntCommutativity:
  fixes AF  :: "name list"
  and   Ψ   :: 'b
  and   Ψ'  :: 'b

  shows "AF, Ψ  Ψ' F AF, Ψ'  Ψ"
by(induct AF) (auto intro: Commutativity frameResPres)

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

  shows "AF, ΨF  SBottom F AF, ΨF"
by(induct AF) (auto intro: Identity frameResPres)

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

  assumes "Ψ  Ψ'"

  shows "AF, Ψ  ΨF F AF, Ψ'  ΨF"
using assms
by(induct AF) (auto intro: Composition frameResPres)

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

  assumes "Ψ  Ψ'"

  shows "AF, ΨF  Ψ F AF, ΨF  Ψ'"
using assms
by(induct AF) (auto intro: compositionSym frameResPres)

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

  shows "F F G F G F F"
proof -
  obtain AF ΨF where "F = AF, ΨF" and "AF ♯* G"
    by(rule freshFrame)
  moreover obtain AG ΨG where "G = AG, ΨG" and "AG ♯* ΨF" and "AG ♯* AF"
    by(rule_tac C="(AF, ΨF)" in freshFrame) auto
  moreover from AF ♯* G G = AG, ΨG AG ♯* AF have "AF ♯* Ψ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 (⦇νxG)"
proof -
  have "⦇νx(F F G) F ⦇νx(G F F)"
    by(metis frameResPres frameCommutativity)
  with x  F have "⦇νx(F F G) F (⦇νxG) F F"
    by simp
  moreover have "(⦇νxG) F F F F F (⦇νxG)"
    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 AF ΨF where "F = AF, ΨF" and "AF ♯* Ψ" and "AF ♯* Ψ'" and "AF ♯* (Ψ  Ψ')"
    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   AP :: "name list"
  and   ΨP :: 'b

  shows "guarded P; extractFrame P = AP, ΨP  ΨP    supp ΨP = ({}::name set)"
  and   "guarded' I; extractFrame' I = AP, ΨP  ΨP    supp ΨP = ({}::name set)"
  and   "guarded'' C; extractFrame'' C = AP, ΨP  ΨP    supp ΨP = ({}::name set)"
proof(nominal_induct P and I and C arbitrary: AP ΨP rule: psi_input_psiCase.strong_inducts)
  case(PsiNil AP ΨP)
  thus ?case by simp
next
  case(Output M N P AP ΨP)
  thus ?case by simp
next
  case(Input M In  AP ΨP)
  thus ?case by simp
next
  case(Case psiCase AP ΨP)
  thus ?case by simp
next
  case(Par P Q APQ ΨPQ)
  from guarded(P  Q) have "guarded P" and "guarded Q" by simp+
  obtain AP ΨP where FrP: "extractFrame P = AP, ΨP" and "AP ♯* Q" by(rule freshFrame)
  obtain AQ ΨQ where FrQ: "extractFrame Q = AQ, ΨQ" and "AQ ♯* AP" and "AQ ♯* ΨP" 
    by(rule_tac C="(AP, ΨP)" in freshFrame) auto
  
  from AP ΨP. guarded P; extractFrame P = AP, ΨP  ΨP    (supp ΨP = ({}::name set)) guarded P FrP
  have "ΨP  " and "supp ΨP = ({}::name set)" by simp+
  from AQ ΨQ. guarded Q; extractFrame Q = AQ, ΨQ  ΨQ    (supp ΨQ = ({}::name set)) guarded Q FrQ
  have "ΨQ  " and "supp ΨQ = ({}::name set)" by simp+
  
  from AP ♯* Q FrQ AQ ♯* AP have "AP ♯* ΨQ" by(drule_tac extractFrameFreshChain) auto
  with AQ ♯* AP AQ ♯* ΨP FrP FrQ extractFrame(P  Q) = APQ, ΨPQ have "(AP@AQ), ΨP  ΨQ = APQ, Ψ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 AxP ΨxP)
  from guarded(⦇νxP) have "guarded P" by simp
  moreover obtain AP ΨP where FrP: "extractFrame P = AP, ΨP" by(rule freshFrame)
  moreover note AP ΨP. guarded P; extractFrame P = AP, ΨP  ΨP    (supp ΨP = ({}::name set))
  ultimately have "ΨP  " and "supp ΨP = ({}::name set)" by auto
  from FrP extractFrame(⦇νxP) = AxP, ΨxP have "(x#AP), ΨP = AxP, Ψ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 Ψ AP ΨP)
  thus ?case by simp
next
  case(Bang P AP Ψ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