Theory Weaken_Stat_Imp

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

context weak begin

definition
  "weakenStatImp" :: "'b ⇒ ('a, 'b, 'c) psi ⇒
                     ('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set ⇒ 
                     ('a, 'b, 'c) psi ⇒ bool" (‹_ ⊳ _ ⪅⇩w<_> _› [80, 80, 80, 80] 80)
where "Ψ ⊳ P ⪅⇩w<Rel> Q ≡ ∃Q'. Ψ ⊳ Q ⟹⇧^⇩τ Q' ∧ insertAssertion(extractFrame P) Ψ ↪⇩F insertAssertion(extractFrame Q') Ψ ∧ (Ψ, P, Q') ∈ Rel"

lemma weakenStatImpMonotonic:
  fixes Ψ :: 'b
  and   P :: "('a, 'b, 'c) psi"
  and   A :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"
  and   Q :: "('a, 'b, 'c) psi"
  and   B :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"

  assumes "Ψ ⊳ P ⪅⇩w<A> Q"
  and     "A ⊆ B"

  shows "Ψ ⊳ P ⪅⇩w<B> Q"
using assms
by(auto simp add: weakenStatImp_def)

lemma weakenStatImpI:
  fixes Ψ :: 'b
  and   P :: "('a, 'b, 'c) psi"
  and   Rel :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"
  and   Q   :: "('a, 'b, 'c) psi"
  and   Ψ' :: 'b

  assumes "Ψ ⊳ Q ⟹⇧^⇩τ Q'"
  and     "insertAssertion(extractFrame P) Ψ ↪⇩F insertAssertion(extractFrame Q') Ψ"
  and     "(Ψ, P, Q') ∈ Rel"

  shows "Ψ ⊳ P ⪅⇩w<Rel> Q"
using assms
by(auto simp add: weakenStatImp_def)

lemma weakenStatImpE:
  fixes Ψ :: 'b
  and   P :: "('a, 'b, 'c) psi"
  and   Rel :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"
  and   Q   :: "('a, 'b, 'c) psi"
  and   Ψ' :: 'b

  assumes "Ψ ⊳ P ⪅⇩w<Rel> Q"

  obtains Q' where "Ψ ⊳ Q ⟹⇧^⇩τ Q'" and "insertAssertion(extractFrame P) Ψ ↪⇩F insertAssertion(extractFrame Q') Ψ " and "(Ψ, P, Q') ∈ Rel"
using assms
by(auto simp add: weakenStatImp_def)

lemma weakStatImpWeakenStatImp:
  fixes Ψ  :: 'b
  and   P   :: "('a, 'b, 'c) psi"
  and   Rel :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"
  and   Q   :: "('a, 'b, 'c) psi"

  assumes cSim: "Ψ ⊳ P ⪅<Rel> Q"
  and     cStatEq: "⋀Ψ' R S Ψ''. ⟦(Ψ', R, S) ∈ Rel; Ψ' ≃ Ψ''⟧ ⟹ (Ψ'', R, S) ∈ Rel"

  shows "Ψ ⊳ P ⪅⇩w<Rel> Q"
proof -
  from ‹Ψ ⊳ P ⪅<Rel> Q› 
  obtain Q' Q'' where QChain: "Ψ ⊳ Q ⟹⇧^⇩τ Q'"
                  and PImpQ': "insertAssertion(extractFrame P) Ψ ↪⇩F insertAssertion(extractFrame Q') Ψ"
                  and Q'Chain: "Ψ ⊗ 𝟭 ⊳ Q' ⟹⇧^⇩τ Q''" and "(Ψ ⊗ 𝟭, P, Q'') ∈ Rel"
    by(rule weakStatImpE)
  from Q'Chain Identity have Q'Chain: "Ψ ⊳ Q' ⟹⇧^⇩τ Q''" by(rule tauChainStatEq)
  with QChain have "Ψ ⊳ Q ⟹⇧^⇩τ Q''" by auto
  moreover from Q'Chain have "insertAssertion(extractFrame Q') Ψ ↪⇩F insertAssertion(extractFrame Q'') Ψ"
    by(rule statImpTauChainDerivative)
  with PImpQ' have "insertAssertion(extractFrame P) Ψ ↪⇩F insertAssertion(extractFrame Q'') Ψ"
    by(rule FrameStatImpTrans)
  moreover from ‹(Ψ ⊗ 𝟭, P, Q'') ∈ Rel› Identity have "(Ψ, P, Q'') ∈ Rel" by(rule cStatEq)
  ultimately show ?thesis by(rule weakenStatImpI)
qed

lemma weakenStatImpWeakStatImp:
  fixes Ψ  :: 'b
  and   P   :: "('a, 'b, 'c) psi"
  and   Rel :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"
  and   Q   :: "('a, 'b, 'c) psi"

  assumes "Ψ ⊳ P ⪅⇩w<Rel> Q"
  and     cExt: "⋀Ψ' R S Ψ''. (Ψ', R, S) ∈ Rel ⟹ (Ψ' ⊗ Ψ'', R, S) ∈ Rel"

  shows "Ψ ⊳ P ⪅<Rel> Q"
proof(induct rule: weakStatImpI)
  case(cStatImp Ψ')
     
  from ‹Ψ ⊳ P ⪅⇩w<Rel> Q› 
  obtain Q' where QChain: "Ψ ⊳ Q ⟹⇧^⇩τ Q'"
              and PImpQ': "insertAssertion(extractFrame P) Ψ ↪⇩F insertAssertion(extractFrame Q') Ψ"
              and "(Ψ, P, Q') ∈ Rel"
    by(rule weakenStatImpE)
  note QChain PImpQ'
  moreover have "Ψ ⊗ Ψ' ⊳ Q' ⟹⇧^⇩τ Q'" by simp
  moreover from ‹(Ψ, P, Q') ∈ Rel› have "(Ψ ⊗ Ψ', P, Q') ∈ Rel" by(rule cExt)
  ultimately show ?case by blast
qed

end

end