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

locale weak = env + 
  assumes weaken: "Ψ ↪ Ψ ⊗ Ψ'"
begin

lemma entWeaken:
  fixes Ψ :: 'b
  and   φ :: 'c

  assumes "Ψ ⊨ φ"

  shows "Ψ ⊗ Ψ' ⊨ φ"
using assms weaken
by(auto simp add: AssertionStatImp_def)

lemma assertWeaken:
  fixes Ψ  :: 'b
  and   Ψ' :: 'b

  shows "Ψ ↪ Ψ ⊗ Ψ'"
by(auto simp add: AssertionStatImp_def entWeaken)

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

  shows "F ↪_F F ⊗_F G"
proof -
  obtain A_F Ψ_F where FrF: "F = ⟨A_F, Ψ_F⟩" and "A_F ♯* F" and  "A_F ♯* G"
    by(rule_tac F=F and C="(F, G)" in freshFrame) auto
  obtain A_G Ψ_G where FrG: "G = ⟨A_G, Ψ_G⟩" and "A_G ♯* F" and  "A_G ♯* G" and "A_G ♯* A_F" and "A_G ♯* Ψ_F"
    by(rule_tac F=G and C="(F, G, A_F, Ψ_F)" in freshFrame) auto
  from FrG ‹A_F ♯* G› ‹A_G ♯* A_F› have "A_F ♯* Ψ_G" by auto
  have "Ψ_F ↪ Ψ_F ⊗ Ψ_G" by(rule weaken)
  hence "⟨A_G, Ψ_F⟩ ↪_F ⟨A_G, Ψ_F ⊗ Ψ_G⟩" by(rule_tac frameImpResChainPres) auto
  with ‹A_G ♯* Ψ_F› have "⟨ε, Ψ_F⟩ ↪_F ⟨A_G, Ψ_F ⊗ Ψ_G⟩" using frameResFreshChain
    by(rule_tac FrameStatImpTrans) (auto simp add: FrameStatEq_def)
  with FrF FrG ‹A_G ♯* A_F› ‹A_G ♯* Ψ_F› ‹A_F ♯* Ψ_G› show ?thesis
    by(force simp add: frameChainAppend intro: frameImpResChainPres)
qed

lemma unitAssertWeaken:
  fixes Ψ :: 'b

  shows "1 ↪ Ψ"
proof -
  have "1 ↪ 1 ⊗ Ψ" by(rule assertWeaken)
  moreover have "1 ⊗ Ψ ↪ Ψ" by(metis Identity AssertionStatEq_def Commutativity AssertionStatEqTrans)
  ultimately show ?thesis by(rule AssertionStatImpTrans)
qed

lemma unitFrameWeaken:
  fixes F :: "'b frame"

  shows "⟨ε, 1⟩ ↪_F F"
proof -
  have "⟨ε, 1⟩ ↪_F ((⟨ε, 1⟩) ⊗_F F)" by(rule frameWeaken)
  moreover obtain A_F Ψ_F where FrF: "F = ⟨A_F, Ψ_F⟩"
    by(rule_tac F=F and C="()" in freshFrame) auto
  hence "(⟨ε, 1⟩) ⊗_F F ≃_F F" 
    by simp (metis frameIntIdentity frameIntCommutativity FrameStatEqTrans FrameStatEqSym)
  ultimately show ?thesis by(metis FrameStatImpTrans FrameStatEq_def)
qed

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

  shows "⟨ε, Ψ⟩ ↪_F insertAssertion F Ψ"
proof -
  have "⟨ε, Ψ⟩ ↪_F (⟨ε, Ψ⟩) ⊗_F F" by(rule frameWeaken)
  thus ?thesis by simp
qed

lemma frameImpStatEq:
  fixes A_F  :: "name list"
  and   Ψ  :: 'b
  and   Ψ' :: 'b
  and   φ  :: 'c

  assumes "(⟨A_F, Ψ⟩) ⊨_F φ"
  and     "Ψ ≃ Ψ'"

  shows "(⟨A_F, Ψ'⟩) ⊨_F φ"
proof -
  obtain p::"name prm" where "(p ∙ A_F) ♯* φ" and "(p ∙ A_F) ♯* Ψ" and "(p ∙ A_F) ♯* Ψ'"
                         and "distinctPerm p" and S: "set p ⊆ set A_F × set(p ∙ A_F)"
    by(rule_tac c="(φ, Ψ, Ψ')" in name_list_avoiding) auto
  from ‹(⟨A_F, Ψ⟩) ⊨_F φ› ‹(p ∙ A_F) ♯* Ψ› S have "(⟨(p ∙ A_F), p ∙ Ψ⟩) ⊨_F φ" by(simp add: frameChainAlpha)
  hence "(p ∙ Ψ) ⊨ φ" using ‹(p ∙ A_F) ♯* φ› by(rule frameImpE)
  moreover from ‹Ψ ≃ Ψ'› have "(p ∙ Ψ) ≃ (p ∙ Ψ')" by(rule AssertionStatEqClosed)
  ultimately have "(p ∙ Ψ') ⊨ φ" by(simp add: AssertionStatEq_def AssertionStatImp_def)
  hence "(⟨(p ∙ A_F), p ∙ Ψ'⟩) ⊨_F φ" using ‹(p ∙ A_F) ♯* φ›
    by(rule_tac frameImpI) auto
  with ‹(p ∙ A_F) ♯* Ψ'› S show ?thesis by(simp add: frameChainAlpha)
qed

lemma statImpTauDerivative:
  fixes Ψ   :: 'b
  and   P    :: "('a, 'b, 'c) psi"
  and   P'   :: "('a, 'b, 'c) psi"

  assumes "Ψ ⊳ P ⟼τ ≺ P'"

  shows "insertAssertion (extractFrame P) Ψ ↪_F insertAssertion (extractFrame P') Ψ"
proof(auto simp add: FrameStatImp_def)
  fix φ :: 'c
  obtain A_P Ψ_P where FrP: "extractFrame P = ⟨A_P, Ψ_P⟩" and "A_P ♯* P" and "A_P ♯* φ" and "A_P ♯* Ψ" and "distinct A_P" 
    by(rule_tac C="(P, φ, Ψ)" in freshFrame) auto
  with ‹Ψ ⊳ P ⟼τ ≺ P'› obtain Ψ' A_P' Ψ_P' where FrP': "extractFrame P' = ⟨A_P', Ψ_P'⟩" and "Ψ_P ⊗ Ψ' ≃ Ψ_P'" 
                                              and "A_P' ♯* P'" and "A_P' ♯* φ"  and "A_P' ♯* Ψ" 
    by(rule_tac C="(Ψ, φ)" in expandTauFrame) auto
  assume "insertAssertion (extractFrame P) Ψ ⊨_F φ"
  with FrP ‹A_P ♯* φ› ‹A_P ♯* Ψ› have "Ψ ⊗ Ψ_P ⊨ φ" by(auto dest: frameImpE)
  hence "(Ψ ⊗ Ψ_P) ⊗ Ψ' ⊨ φ" by(rule entWeaken)
  hence "Ψ ⊗ Ψ_P' ⊨ φ" using ‹Ψ_P ⊗ Ψ' ≃ Ψ_P'›
    by(rule_tac statEqEnt, auto) (metis Associativity compositionSym AssertionStatEqTrans AssertionStatEqSym Commutativity)
  with ‹A_P' ♯* φ› ‹A_P' ♯* Ψ› FrP' show "insertAssertion (extractFrame P') Ψ ⊨_F φ"
    by(force intro: frameImpI)
qed

lemma weakenTransition:
  fixes Ψ  :: 'b
  and   P  :: "('a, 'b, 'c) psi"
  and   Rs :: "('a, 'b, 'c) residual"
  and   Ψ' :: 'b

  assumes "Ψ ⊳ P ⟼ Rs"

  shows "Ψ ⊗ Ψ' ⊳ P ⟼ Rs"
using assms
proof(nominal_induct avoiding: Ψ' rule: semantics.strong_induct)
  case(cInput Ψ M K xvec N Tvec P Ψ')
  from ‹Ψ ⊨ M ↔ K› have "Ψ ⊗ Ψ' ⊨ M ↔ K" by(rule entWeaken)
  thus ?case using ‹distinct xvec› ‹set xvec ⊆ (supp N)› ‹length xvec = length Tvec›
    by(rule Input)
next
  case(Output Ψ M K N P Ψ')
  from ‹Ψ ⊨ M ↔ K› have "Ψ ⊗ Ψ' ⊨ M ↔ K" by(rule entWeaken)
  thus ?case by(rule semantics.Output)
next
  case(Case Ψ P Rs φ Cs Ψ')
  have "Ψ ⊗ Ψ' ⊳ P ⟼ Rs" by(rule Case)
  moreover note ‹(φ, P) mem Cs›
  moreover from ‹Ψ ⊨ φ› have "Ψ ⊗ Ψ' ⊨ φ" by(rule entWeaken)
  ultimately show ?case using ‹guarded P›
    by(rule semantics.Case)
next
  case(cPar1 Ψ Ψ_Q P α P' Q A_Q Ψ')
  have "(Ψ ⊗ Ψ_Q) ⊗ Ψ' ⊳ P ⟼α ≺ P'" by(rule cPar1)
  hence "(Ψ ⊗ Ψ') ⊗ Ψ_Q ⊳ P ⟼α ≺ P'"
    by(metis statEqTransition Composition Associativity Commutativity AssertionStatEqTrans)
  thus ?case using ‹extractFrame Q = ⟨A_Q, Ψ_Q⟩› ‹bn α ♯* Q› ‹A_Q ♯* Ψ› ‹A_Q ♯* Ψ'› ‹A_Q ♯* P› ‹A_Q ♯* α›
    by(rule_tac Par1) auto
next
  case(cPar2 Ψ Ψ_P Q α Q' P A_P Ψ')
  have "(Ψ ⊗ Ψ_P) ⊗ Ψ' ⊳ Q ⟼α ≺ Q'" by(rule cPar2)
  hence "(Ψ ⊗ Ψ') ⊗ Ψ_P ⊳ Q ⟼α ≺ Q'"
    by(metis statEqTransition Composition Associativity Commutativity AssertionStatEqTrans)
  thus ?case using ‹extractFrame P = ⟨A_P, Ψ_P⟩› ‹bn α ♯* P› ‹A_P ♯* Ψ› ‹A_P ♯* Ψ'› ‹A_P ♯* Q› ‹A_P ♯* α›
    by(rule_tac Par2) auto
next
  case(cComm1 Ψ Ψ_Q P M N P' A_P Ψ_P Q K xvec Q' A_Q Ψ')
  have "(Ψ ⊗ Ψ_Q) ⊗ Ψ' ⊳ P ⟼M(N) ≺ P'" by(rule cComm1)
  hence "(Ψ ⊗ Ψ') ⊗ Ψ_Q ⊳ P ⟼M(N) ≺ P'"
    by(metis statEqTransition Composition Associativity Commutativity AssertionStatEqTrans)
  moreover note ‹extractFrame P = ⟨A_P, Ψ_P⟩›
  moreover have "(Ψ ⊗ Ψ_P) ⊗ Ψ' ⊳ Q ⟼K(ν*xvec)⟨N⟩ ≺ Q'" by(rule cComm1)
  hence "(Ψ ⊗ Ψ') ⊗ Ψ_P ⊳ Q ⟼K(ν*xvec)⟨N⟩ ≺ Q'"
    by(metis statEqTransition Composition Associativity Commutativity AssertionStatEqTrans)
  moreover note ‹extractFrame Q = ⟨A_Q, Ψ_Q⟩›
  moreover from ‹Ψ ⊗ Ψ_P ⊗ Ψ_Q ⊨ M ↔ K› have "(Ψ ⊗ Ψ_P ⊗ Ψ_Q) ⊗ Ψ' ⊨ M ↔ K" by(rule entWeaken)
  hence "(Ψ ⊗ Ψ') ⊗ Ψ_P ⊗ Ψ_Q ⊨ M ↔ K" by(metis statEqEnt Composition Associativity Commutativity AssertionStatEqTrans)
  ultimately show ?case using ‹A_P ♯* Ψ› ‹A_P ♯* Ψ'› ‹A_P ♯* P› ‹A_P ♯* Q› ‹A_P ♯* M› ‹A_P ♯* A_Q›
                              ‹A_Q ♯* Ψ› ‹A_Q ♯* Ψ'› ‹A_Q ♯* P› ‹A_Q ♯* Q› ‹A_Q ♯* K› ‹xvec ♯* P›
    by(rule_tac Comm1) (assumption | auto)+
next
  case(cComm2 Ψ Ψ_Q P M xvec N P' A_P Ψ_P Q K Q' A_Q Ψ')
  have "(Ψ ⊗ Ψ_Q) ⊗ Ψ' ⊳ P ⟼M(ν*xvec)⟨N⟩ ≺ P'" by(rule cComm2)
  hence "(Ψ ⊗ Ψ') ⊗ Ψ_Q ⊳ P ⟼M(ν*xvec)⟨N⟩ ≺ P'"
    by(metis statEqTransition Composition Associativity Commutativity AssertionStatEqTrans)
  moreover note ‹extractFrame P = ⟨A_P, Ψ_P⟩›
  moreover have "(Ψ ⊗ Ψ_P) ⊗ Ψ' ⊳ Q ⟼K(N) ≺ Q'" by(rule cComm2)
  hence "(Ψ ⊗ Ψ') ⊗ Ψ_P ⊳ Q ⟼K(N) ≺ Q'"
    by(metis statEqTransition Composition Associativity Commutativity AssertionStatEqTrans)
  moreover note ‹extractFrame Q = ⟨A_Q, Ψ_Q⟩›
  moreover from ‹Ψ ⊗ Ψ_P ⊗ Ψ_Q ⊨ M ↔ K› have "(Ψ ⊗ Ψ_P ⊗ Ψ_Q) ⊗ Ψ' ⊨ M ↔ K" by(rule entWeaken)
  hence "(Ψ ⊗ Ψ') ⊗ Ψ_P ⊗ Ψ_Q ⊨ M ↔ K" by(metis statEqEnt Composition Associativity Commutativity AssertionStatEqTrans)
  ultimately show ?case using ‹A_P ♯* Ψ› ‹A_P ♯* Ψ'› ‹A_P ♯* P› ‹A_P ♯* Q› ‹A_P ♯* M› ‹A_P ♯* A_Q›
                              ‹A_Q ♯* Ψ› ‹A_Q ♯* Ψ'› ‹A_Q ♯* P› ‹A_Q ♯* Q› ‹A_Q ♯* K› ‹xvec ♯* Q›
    by(rule_tac Comm2) (assumption | auto)+
next
  case(cOpen Ψ P M xvec yvec N P' x Ψ')
  have "Ψ ⊗ Ψ' ⊳ P ⟼M(ν*(xvec@yvec))⟨N⟩ ≺ P'" by(rule cOpen)
  thus ?case using ‹x ∈ supp N› ‹x ♯ Ψ› ‹x ♯ Ψ'› ‹x ♯ M› ‹x ♯ xvec› ‹x ♯ yvec›
    by(rule_tac Open) auto
next  
  case(cScope Ψ P α P' x Ψ')
  have "Ψ ⊗ Ψ' ⊳ P ⟼α ≺ P'" by(rule cScope)
  thus ?case using ‹x ♯ Ψ› ‹x ♯ Ψ'› ‹x ♯ α› by(rule_tac Scope) auto
next
  case(Bang Ψ P Rs Ψ')
  have "Ψ ⊗ Ψ' ⊳ P ∥ !P⟼ Rs" by(rule Bang)
  thus ?case using ‹guarded P› by(rule semantics.Bang)
qed

end

end