Theory Weakening

(* 
   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 AF ΨF where FrF: "F = ⟨AF, ΨF⟩" and "AF ♯* F" and  "AF ♯* G"
    by(rule_tac F=F and C="(F, G)" in freshFrame) auto
  obtain AG ΨG where FrG: "G = ⟨AG, ΨG⟩" and "AG ♯* F" and  "AG ♯* G" and "AG ♯* AF" and "AG ♯* ΨF"
    by(rule_tac F=G and C="(F, G, AF, ΨF)" in freshFrame) auto
  from FrG ‹AF ♯* G› ‹AG ♯* AF› have "AF ♯* ΨG" by auto
  have "ΨF ↪ ΨF ⊗ ΨG" by(rule weaken)
  hence "⟨AG, ΨF⟩ ↪F ⟨AG, ΨF ⊗ ΨG⟩" by(rule_tac frameImpResChainPres) auto
  with ‹AG ♯* ΨF› have "⟨ε, ΨF⟩ ↪F ⟨AG, ΨF ⊗ ΨG⟩" using frameResFreshChain
    by(rule_tac FrameStatImpTrans) (auto simp add: FrameStatEq_def)
  with FrF FrG ‹AG ♯* AF› ‹AG ♯* ΨF› ‹AF ♯* ΨG› show ?thesis
    by(force simp add: frameChainAppend intro: frameImpResChainPres)
qed

lemma unitAssertWeaken:
  fixes Ψ :: 'b

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

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

  shows "⟨ε, 𝟭⟩ ↪F F"
proof -
  have "⟨ε, 𝟭⟩ ↪F ((⟨ε, 𝟭⟩) ⊗F F)" by(rule frameWeaken)
  moreover obtain AF ΨF where FrF: "F = ⟨AF, ΨF⟩"
    by(rule_tac F=F and C="()" in freshFrame) auto
  hence "(⟨ε, 𝟭⟩) ⊗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 AF  :: "name list"
  and   Ψ  :: 'b
  and   Ψ' :: 'b
  and   φ  :: 'c

  assumes "(⟨AF, Ψ⟩) ⊢F φ"
  and     "Ψ ≃ Ψ'"

  shows "(⟨AF, Ψ'⟩) ⊢F φ"
proof -
  obtain p::"name prm" where "(p ∙ AF) ♯* φ" and "(p ∙ AF) ♯* Ψ" and "(p ∙ AF) ♯* Ψ'"
                         and "distinctPerm p" and S: "set p ⊆ set AF × set(p ∙ AF)"
    by(rule_tac c="(φ, Ψ, Ψ')" in name_list_avoiding) auto
  from ‹(⟨AF, Ψ⟩) ⊢F φ› ‹(p ∙ AF) ♯* Ψ› S have "(⟨(p ∙ AF), p ∙ Ψ⟩) ⊢F φ" by(simp add: frameChainAlpha)
  hence "(p ∙ Ψ) ⊢ φ" using ‹(p ∙ AF) ♯* φ› by(rule frameImpE)
  moreover from ‹Ψ ≃ Ψ'› have "(p ∙ Ψ) ≃ (p ∙ Ψ')" by(rule AssertionStatEqClosed)
  ultimately have "(p ∙ Ψ') ⊢ φ" by(simp add: AssertionStatEq_def AssertionStatImp_def)
  hence "(⟨(p ∙ AF), p ∙ Ψ'⟩) ⊢F φ" using ‹(p ∙ AF) ♯* φ› 
    by(rule_tac frameImpI) auto
  with ‹(p ∙ AF) ♯* Ψ'› 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 AP ΨP where FrP: "extractFrame P = ⟨AP, ΨP⟩" and "AP ♯* P" and "AP ♯* φ" and "AP ♯* Ψ" and "distinct AP" 
    by(rule_tac C="(P, φ, Ψ)" in freshFrame) auto
  with ‹Ψ ⊳ P ⟼τ ≺ P'› obtain Ψ' AP' ΨP' where FrP': "extractFrame P' = ⟨AP', ΨP'⟩" and "ΨP ⊗ Ψ' ≃ ΨP'" 
                                              and "AP' ♯* P'" and "AP' ♯* φ"  and "AP' ♯* Ψ" 
    by(rule_tac C="(Ψ, φ)" in expandTauFrame) auto
  assume "insertAssertion (extractFrame P) Ψ ⊢F φ"
  with FrP ‹AP ♯* φ› ‹AP ♯* Ψ› 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 ‹AP' ♯* φ› ‹AP' ♯* Ψ› 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 AQ Ψ')
  have "(Ψ ⊗ ΨQ) ⊗ Ψ' ⊳ P ⟼α ≺ P'" by(rule cPar1)
  hence "(Ψ ⊗ Ψ') ⊗ ΨQ ⊳ P ⟼α ≺ P'"
    by(metis statEqTransition Composition Associativity Commutativity AssertionStatEqTrans)
  thus ?case using ‹extractFrame Q = ⟨AQ, ΨQ⟩› ‹bn α ♯* Q› ‹AQ ♯* Ψ› ‹AQ ♯* Ψ'› ‹AQ ♯* P› ‹AQ ♯* α›
    by(rule_tac Par1) auto
next
  case(cPar2 Ψ ΨP Q α Q' P AP Ψ')
  have "(Ψ ⊗ ΨP) ⊗ Ψ' ⊳ Q ⟼α ≺ Q'" by(rule cPar2)
  hence "(Ψ ⊗ Ψ') ⊗ ΨP ⊳ Q ⟼α ≺ Q'"
    by(metis statEqTransition Composition Associativity Commutativity AssertionStatEqTrans)
  thus ?case using ‹extractFrame P = ⟨AP, ΨP⟩› ‹bn α ♯* P› ‹AP ♯* Ψ› ‹AP ♯* Ψ'› ‹AP ♯* Q› ‹AP ♯* α›
    by(rule_tac Par2) auto
next
  case(cComm1 Ψ ΨQ P M N P' AP ΨP Q K xvec Q' AQ Ψ')
  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 = ⟨AP, Ψ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 = ⟨AQ, Ψ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 ‹AP ♯* Ψ› ‹AP ♯* Ψ'› ‹AP ♯* P› ‹AP ♯* Q› ‹AP ♯* M› ‹AP ♯* AQ›
                              ‹AQ ♯* Ψ› ‹AQ ♯* Ψ'› ‹AQ ♯* P› ‹AQ ♯* Q› ‹AQ ♯* K› ‹xvec ♯* P›
    by(rule_tac Comm1) (assumption | auto)+
next
  case(cComm2 Ψ ΨQ P M xvec N P' AP ΨP Q K Q' AQ Ψ')
  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 = ⟨AP, Ψ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 = ⟨AQ, Ψ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 ‹AP ♯* Ψ› ‹AP ♯* Ψ'› ‹AP ♯* P› ‹AP ♯* Q› ‹AP ♯* M› ‹AP ♯* AQ›
                              ‹AQ ♯* Ψ› ‹AQ ♯* Ψ'› ‹AQ ♯* P› ‹AQ ♯* Q› ‹AQ ♯* 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