Theory Weaken_Simulation

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

context weak
begin

definition
  "weakenSimulation" :: "'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' ⟶ bn α ♯* Ψ ⟶ bn α ♯* P ⟶ (∃P'. Ψ ⊳ P ⟹α ≺ P' ∧ (Ψ, P', Q') ∈ Rel)"

lemma weakenSimI[case_names cAct]:
  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   C   :: "'d::fs_name"

  assumes rOutput: "⋀α Q'. ⟦Ψ ⊳ Q ⟼α ≺ Q'; bn α ♯* Ψ; bn α ♯* P⟧ ⟹
                             ∃P'. Ψ ⊳ P ⟹α ≺ P' ∧ (Ψ, P', Q') ∈ Rel"
                                             
  shows "Ψ ⊳ P ↝⇩w<Rel> Q"
using assms
by(auto simp add: weakenSimulation_def)

lemma weakenSimWeakSim:
  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, Q) ∈ Rel"
  and     cStatImp: "⋀Ψ' R S. (Ψ, R, S) ∈ Rel ⟹ Ψ ⊳ R ⪅⇩w<Rel> S"
  and     cSim: "⋀Ψ' R S. (Ψ, R, S) ∈ Rel ⟹ Ψ ⊳ R ↝⇩w<Rel'> S"
  and     cExt: "⋀Ψ' R S Ψ'. (Ψ, R, S) ∈ Rel' ⟹ (Ψ ⊗ Ψ', R, S) ∈ Rel'"
  and     cSym: "⋀Ψ' R S. (Ψ, R, S) ∈ Rel ⟹ (Ψ, S, R) ∈ Rel"

  shows "Ψ ⊳ P ↝<Rel'> Q"
proof(induct rule: weakSimI2)
  case(cAct Ψ' α Q')
  from ‹(Ψ, P, Q) ∈ Rel› obtain P''''
    where PChain: "Ψ ⊳ P ⟹⇧^⇩τ P''''" 
      and QImpP'''': "insertAssertion (extractFrame Q) Ψ ↪⇩F insertAssertion (extractFrame P'''') Ψ"
      and "(Ψ, P'''', Q) ∈ Rel" using weakenStatImp_def
    by(metis cStatImp cSym)
    
  from ‹(Ψ, P'''', Q) ∈ Rel› have "Ψ ⊳ P'''' ↝⇩w<Rel'> Q" by(rule cSim)
  moreover from PChain ‹bn α ♯* P› have "bn α ♯* P''''" by(rule tauChainFreshChain)
  ultimately obtain P' where P''''Trans: "Ψ ⊳ P'''' ⟹α ≺ P'" and "(Ψ, P', Q') ∈ Rel'"
    using ‹Ψ ⊳ Q ⟼α ≺ Q'› ‹bn α ♯* Ψ›
    by(unfold weakenSimulation_def, auto)

  from P''''Trans ‹α ≠ τ› obtain P''' P'' where P''''Chain: "Ψ ⊳ P'''' ⟹⇧^⇩τ P'''" and P'''Trans: "Ψ ⊳ P''' ⟼α ≺ P''" and P''Chain: "Ψ ⊳ P'' ⟹⇧^⇩τ P'" 
    by(force simp add: weakenTransition_def)
  from P''''Chain QImpP'''' have "insertAssertion (extractFrame Q) Ψ ↪⇩F insertAssertion (extractFrame P''') Ψ"
    by(blast intro: statImpTauChainDerivative FrameStatImpTrans)
  with PChain P''''Chain have "Ψ : Q ⊳ P ⟹α ≺ P''" using P'''Trans by(rule_tac weakTransitionI) auto
  moreover from P''Chain have "Ψ ⊗ Ψ' ⊳ P'' ⟹⇧^⇩τ P'" by(rule weakenTauChain) 
  moreover from ‹(Ψ, P', Q') ∈ Rel'› have "(Ψ ⊗ Ψ', P', Q') ∈ Rel'" by(rule cExt)
  ultimately show ?case by blast
next
  case(cTau Q')
  from ‹(Ψ, P, Q) ∈ Rel› have "Ψ ⊳ P ↝⇩w<Rel'> Q" by(rule cSim)
  then obtain P' where "Ψ ⊳ P ⟹τ ≺ P'" and "(Ψ, P', Q') ∈ Rel'" using ‹Ψ ⊳ Q ⟼τ ≺ Q'›
    by(unfold weakenSimulation_def, fastforce)
  from ‹Ψ ⊳ P ⟹τ ≺ P'› have "Ψ ⊳ P ⟹⇧^⇩τ P'" by(auto simp add: weakenTransition_def dest: tauActTauChain)
  with ‹(Ψ, P', Q') ∈ Rel'› show ?case by blast
qed

lemma weakSimWeakenSim:
  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(induct rule: weakenSimI)
  case(cAct α Q')
  show ?case
  proof(cases "α=τ")
    case True
    from ‹Ψ ⊳ P ↝<Rel> Q› ‹Ψ ⊳ Q ⟼α ≺ Q'› ‹α = τ› 
    obtain P' where "Ψ ⊳ P ⟹⇧^⇩τ P'" and "(Ψ, P', Q') ∈ Rel"
      by(blast dest: weakSimE)
    from ‹Ψ ⊳ P ⟹⇧^⇩τ P'› have "Ψ ⊳ P ⟹τ ≺ P'"
      by(induct rule: tauChainInduct) (auto simp add: weakenTransition_def)
    thus ?thesis using ‹(Ψ, P', Q') ∈ Rel› ‹α = τ› by blast
  next
    case False
    from ‹Ψ ⊳ P ↝<Rel> Q› ‹Ψ ⊳ Q ⟼α ≺ Q'› ‹bn α ♯* Ψ› ‹bn α ♯* P› ‹α ≠ τ›
    obtain P'' P' where PTrans: "Ψ : Q ⊳ P ⟹α ≺ P''" and P''Chain: "Ψ ⊗ 𝟭 ⊳ P'' ⟹⇧^⇩τ P'" and "(Ψ ⊗ 𝟭, P', Q') ∈ Rel"
      by(blast dest: weakSimE)
    from PTrans have "Ψ ⊳ P ⟹α ≺ P''" by(auto simp add: weakTransition_def weakenTransition_def)
    moreover from P''Chain have "Ψ ⊳ P'' ⟹⇧^⇩τ P'" by(metis tauChainStatEq Identity)
    moreover from ‹(Ψ ⊗ 𝟭, P', Q') ∈ Rel› have "(Ψ, P', Q') ∈ Rel" by(metis cStatEq Identity)
    ultimately show ?thesis
    proof(induct rule: weakenTransitionCases)
      case cBase 
      from ‹Ψ ⊳ P ⟹⇧^⇩τ P'› have "Ψ ⊳ P ⟹τ ≺ P'"
        by(induct rule: tauChainInduct) (auto simp add: weakenTransition_def)
      with ‹(Ψ, P', Q') ∈ Rel› show ?case by blast
    next
      case(cStep P'''' P''')
      thus ?case 
        apply(unfold weakenTransition_def)
        by(rule_tac x=P' in exI) fastforce
    qed
  qed
qed

lemma weakenSimE:
  fixes F   :: '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"

  shows "⋀α  Q'. ⟦Ψ ⊳ Q ⟼α ≺ Q'; bn α ♯* Ψ; bn α ♯* P⟧ ⟹ 
                   ∃P'. Ψ ⊳ P ⟹α ≺ P' ∧ (Ψ, P', Q') ∈ Rel"
using assms
by(auto simp add: weakenSimulation_def)

lemma weakenSimMonotonic: 
  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(simp (no_asm) add: weakenSimulation_def) (blast dest: weakenSimE)

end

end