Theory Broadcast_Frame

theory Broadcast_Frame
  imports "Psi_Calculi.Frame"
begin

locale assertionAux = Frame.assertionAux SCompose SImp SBottom SChanEq
  for 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)
  +
  fixes SOutCon  :: "'a::fs_name ⇒ 'a ⇒ 'c"   ("_ ≼ _" [80, 80] 80)
    and SInCon   :: "'a::fs_name ⇒ 'a ⇒ 'c"   ("_ ≽ _" [80, 80] 80)

assumes statEqvt'''[eqvt]: "⋀p::name prm. p ∙ (M ≼ N) = (p ∙ M) ≼ (p ∙ N)"
  and   statEqvt''''[eqvt]: "⋀p::name prm. p ∙ (M ≽ N) = (p ∙ M) ≽ (p ∙ N)"

begin

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

shows "(supp(M ≽ N)::name set) ⊆ ((supp M) ∪ (supp N))"
proof -
  {
    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)}"
    then have "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)
    then have "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(blast dest: Infinite_cong)
    then have False by simp
  }
  then show ?thesis by(auto simp add: eqvts supp_def)
qed

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

shows "(supp(M ≼ N)::name set) ⊆ ((supp M) ∪ (supp N))"
proof -
  {
    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)}"
    then have "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)
    then have "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(blast dest: Infinite_cong)
    then have False by simp
  }
  then show ?thesis by (auto simp add: eqvts supp_def)
qed

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

assumes "x ♯ M"
  and   "x ♯ N"

shows "x ♯ M ≽ N"
  using assms chanInConSupp
  by(auto simp add: fresh_def)

lemma freshInConChain[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 freshOutCon[intro]:
  fixes x :: name
    and M :: 'a
    and N :: 'a

assumes "x ♯ M"
  and   "x ♯ N"

shows "x ♯ M ≼ N"
  using assms chanOutConSupp
  by(auto simp add: fresh_def)

lemma freshOutConChain[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 chanOutConClosed:
  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)
  then show ?thesis by(auto simp add: eqvts)
qed

lemma chanInConClosed:
  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)
  then show ?thesis by(auto simp add: eqvts)
qed

end

locale assertion = assertionAux SCompose SImp SBottom SChanEq SOutCon SInCon + assertion 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"
  and SOutCon  :: "'a::fs_name ⇒ 'a ⇒ 'c"
  and SInCon   :: "'a::fs_name ⇒ 'a ⇒ 'c" +

  assumes chanOutConSupp: "SImp Ψ (SOutCon M N) ⟹ (((supp N)::name set) ⊆ ((supp M)::name set))"
    and   chanInConSupp:  "SImp Ψ (SInCon N M) ⟹ (((supp N)::name set) ⊆ ((supp M)::name set))"

begin

notation SOutCon ("_ ≼ _" [90, 90] 90)
notation SInCon ("_ ≽ _" [90, 90] 90)

end

end