Theory Weak_Stat_Imp

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

context env begin

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

lemma weakStatImpMonotonic:
  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 ⪅<A> Q"
  and     "A ⊆ B"

  shows "Ψ ⊳ P ⪅<B> Q"
using assms
by(auto simp add: weakStatImp_def) blast

lemma weakStatImpI[case_names cStatImp]:
  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''. Ψ ⊳ Q ⟹⇧^⇩τ Q' ∧ insertAssertion(extractFrame P) Ψ ↪⇩F insertAssertion(extractFrame Q') Ψ ∧ Ψ ⊗ Ψ' ⊳ Q' ⟹⇧^⇩τ Q'' ∧ (Ψ ⊗ Ψ', P, Q'') ∈ Rel"

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

lemma weakStatImpE:
  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 ⪅<Rel> Q"

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

using assms
by(auto simp add: weakStatImp_def) blast

lemma weakStatImpClosed:
  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   p   :: "name prm"

  assumes EqvtRel: "eqvt Rel"
  and     PStatImpQ: "Ψ ⊳ P ⪅<Rel> Q"

  shows "(p ∙ Ψ) ⊳ (p ∙ P) ⪅<Rel> (p ∙ Q)"
proof(induct rule: weakStatImpI)
  case(cStatImp Ψ')
  from PStatImpQ obtain Q' Q'' where QChain: "Ψ ⊳ Q ⟹⇧^⇩τ Q'"
                                 and PimpQ': "insertAssertion (extractFrame P) Ψ ↪⇩F insertAssertion (extractFrame Q') Ψ"
                                 and Q'Chain: "Ψ ⊗ (rev(p::name prm) ∙ Ψ') ⊳ Q' ⟹⇧^⇩τ Q''" and "(Ψ ⊗ (rev p ∙ Ψ'), P,  Q'') ∈ Rel"
    by(rule weakStatImpE)
  from QChain have "(p ∙ Ψ) ⊳ (p ∙ Q) ⟹⇧^⇩τ (p ∙ Q')" by(rule tauChainEqvt)
  moreover from PimpQ' have "insertAssertion (extractFrame (p ∙ P)) (p ∙ Ψ) ↪⇩F insertAssertion (extractFrame(p ∙ Q')) (p ∙ Ψ)"
    by(drule_tac p=p in FrameStatImpClosed) (simp add: eqvts)
  moreover from Q'Chain have "(p ∙ Ψ) ⊗ Ψ' ⊳ (p ∙ Q') ⟹⇧^⇩τ (p ∙ Q'')" by(drule_tac p=p in tauChainEqvt) (simp add: eqvts)
  moreover from ‹(Ψ ⊗ (rev p ∙ Ψ'), P, Q'') ∈ Rel› EqvtRel have "((p ∙ Ψ) ⊗ Ψ', (p ∙ P), (p ∙ Q'')) ∈ Rel"
    by(drule_tac p=p in eqvtI) (auto simp add: eqvts)
  ultimately show ?case
    by blast
qed

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

  assumes "{(Ψ, P, P) | Ψ P. True} ⊆ Rel"

  shows "Ψ ⊳ P ⪅<Rel> P"
using assms
by(auto simp add: weakStatImp_def weakTransition_def dest: rtrancl_into_rtrancl) force+

lemma weakStatImpTransitive:
  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   Rel'  :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"
  and   R     :: "('a, 'b, 'c) psi"
  and   Rel'' :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"

  assumes PStatImpQ: "Ψ ⊳ P ⪅<Rel> Q"
  and     QRelR: "(Ψ, Q, R) ∈ Rel'"
  and     Set: "{(Ψ', S, U) | Ψ' S U. ∃T. (Ψ', S, T) ∈ Rel ∧ (Ψ', T, U) ∈ Rel'} ⊆ Rel''"
  and     C1: "⋀Ψ' S T. (Ψ', S, T) ∈ Rel' ⟹ Ψ' ⊳ S ⪅<Rel'> T"
  and     C2: "⋀Ψ' S T S'. ⟦(Ψ', S, T) ∈ Rel'; Ψ' ⊳ S ⟹⇧^⇩τ S'⟧ ⟹ ∃T'. Ψ' ⊳ T ⟹⇧^⇩τ T' ∧ (Ψ', S', T') ∈ Rel'"

  shows "Ψ ⊳ P ⪅<Rel''> R"
proof(induct rule: weakStatImpI)
  case(cStatImp Ψ')
  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 QChain ‹(Ψ, Q, R) ∈ Rel'› obtain R' where RChain: "Ψ ⊳ R ⟹⇧^⇩τ R'" and "(Ψ, Q', R') ∈ Rel'"
    by(metis C2)
  from ‹(Ψ, Q', R') ∈ Rel'› obtain R'' R''' where R'Chain: "Ψ ⊳ R' ⟹⇧^⇩τ R''"
                                              and Q'impR'': "insertAssertion (extractFrame Q') Ψ ↪⇩F insertAssertion (extractFrame R'') Ψ"
                                              and R''Chain: "Ψ ⊗ Ψ' ⊳ R'' ⟹⇧^⇩τ R'''" and "(Ψ ⊗ Ψ', Q', R''') ∈ Rel'"
    by(blast dest: C1 weakStatImpE)
  from RChain R'Chain have "Ψ ⊳ R ⟹⇧^⇩τ R''" by auto
  moreover from PimpQ' Q'impR'' have "insertAssertion (extractFrame P) Ψ ↪⇩F insertAssertion (extractFrame R'') Ψ"
    by(rule FrameStatImpTrans)
  moreover from Q'Chain ‹(Ψ ⊗ Ψ', Q',  R''') ∈ Rel'› obtain R'''' where R'''Chain: "Ψ ⊗ Ψ' ⊳ R''' ⟹⇧^⇩τ R''''" and "(Ψ ⊗ Ψ', Q'', R'''') ∈ Rel'"
    by(metis C2)
  from R''Chain R'''Chain have "Ψ ⊗ Ψ' ⊳ R'' ⟹⇧^⇩τ R''''" by auto
  moreover from ‹(Ψ ⊗ Ψ', P,  Q'') ∈ Rel› ‹(Ψ ⊗ Ψ', Q'', R'''') ∈ Rel'› Set have "(Ψ ⊗ Ψ', P, R'''') ∈ Rel''" by blast
  ultimately show ?case
    by blast
qed

lemma weakStatImpStatEq:
  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 PSimQ: "Ψ ⊳ P ⪅<Rel> Q"
  and     "Ψ ≃ Ψ'"
  and     C1: "⋀Ψ' R S Ψ''. ⟦(Ψ', R, S) ∈ Rel; Ψ' ≃ Ψ''⟧ ⟹ (Ψ'', R, S) ∈ Rel'"

  shows "Ψ' ⊳ P ⪅<Rel'> Q"
proof(induct rule: weakStatImpI)
  case(cStatImp Ψ'')
  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 QChain ‹Ψ ≃ Ψ'› have "Ψ' ⊳ Q ⟹⇧^⇩τ Q'" by(rule tauChainStatEq)
  moreover from PimpQ ‹Ψ ≃ Ψ'› have "insertAssertion (extractFrame P) Ψ' ↪⇩F insertAssertion (extractFrame Q') Ψ'"
    by(rule insertAssertionStatImp)
  moreover from Q'Chain ‹Ψ ≃ Ψ'› have "Ψ' ⊗ Ψ'' ⊳ Q' ⟹⇧^⇩τ Q''" by(metis tauChainStatEq Composition)
  moreover from ‹(Ψ ⊗ Ψ'', P, Q'') ∈ Rel› ‹Ψ ≃ Ψ'›  have "(Ψ' ⊗ Ψ'', P, Q'') ∈ Rel'" by(blast intro: Composition C1)
  ultimately show ?case
    by blast
qed

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

  assumes PImpQ: "insertAssertion(extractFrame P) Ψ ↪⇩F insertAssertion(extractFrame Q) Ψ"
  and     C1: "⋀Ψ'. (Ψ ⊗ Ψ', P, Q) ∈ Rel"

  shows "Ψ ⊳ P ⪅<Rel> Q"
proof(induct rule: weakStatImpI)
  case(cStatImp Ψ')
  have "Ψ ⊳ Q ⟹⇧^⇩τ Q" by simp
  moreover note PImpQ
  moreover have "Ψ ⊗ Ψ' ⊳ Q ⟹⇧^⇩τ Q" by simp
  moreover have "(Ψ ⊗ Ψ', P, Q) ∈ Rel" by(rule C1)
  ultimately show ?case
    by blast
qed

end

end