Theory Weak_Cong_Simulation

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

context env begin

definition
  "weakCongSimulation" :: "'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' ⟶ (∃P'. Ψ ⊳ P ⟹⇩τ P' ∧ (Ψ, P', Q') ∈ Rel)"

abbreviation
  weakCongSimulationNilJudge ("_ ↝«_» _" [80, 80, 80] 80) where "P ↝«Rel» Q ≡ SBottom' ⊳ P ↝«Rel» Q"

lemma weakCongSimI[case_names cTau]:
  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 rTau:  "⋀Q'. Ψ ⊳ Q ⟼τ ≺ Q' ⟹ ∃P'. Ψ ⊳ P ⟹⇩τ P' ∧ (Ψ, P', Q') ∈ Rel"

  shows "Ψ ⊳ P ↝«Rel» Q"
using assms
by(auto simp add: weakCongSimulation_def)


lemma weakCongSimE:
  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 ↝«Rel» Q"
  and "Ψ ⊳ Q ⟼τ ≺ Q'"

  obtains P' where "Ψ ⊳ P ⟹⇩τ P'" and "(Ψ, P', Q') ∈ Rel"
using assms
by(auto simp add: weakCongSimulation_def)

lemma weakCongSimClosedAux:
  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     PSimQ: "Ψ ⊳ P ↝«Rel» Q"

  shows "(p ∙ Ψ) ⊳ (p ∙ P) ↝«Rel» (p ∙ Q)"
proof(induct rule: weakCongSimI)
  case(cTau Q')
  from ‹p ∙ Ψ ⊳ p ∙ Q ⟼τ ≺ Q'› 
  have "(rev p ∙ p ∙ Ψ) ⊳ (rev p ∙ p ∙ Q) ⟼(rev p ∙ (τ ≺ Q'))"
    by(blast dest: semantics.eqvt)
  hence "Ψ ⊳ Q ⟼τ ≺ (rev p ∙ Q')" by(simp add: eqvts)
  with PSimQ obtain P' where PChain: "Ψ ⊳ P ⟹⇩τ P'" and P'RelQ': "(Ψ, P', rev p ∙ Q') ∈ Rel"
    by(blast dest: weakCongSimE)
  from PChain have "(p ∙ Ψ) ⊳ (p ∙ P) ⟹⇩τ (p ∙ P')" by(rule tauStepChainEqvt)
  moreover from P'RelQ' EqvtRel have "(p ∙ (Ψ,  P', rev p ∙ Q')) ∈ Rel"
    by(simp only: eqvt_def)
  hence "(p ∙ Ψ, p ∙ P', Q') ∈ Rel" by(simp add: eqvts)
  ultimately show ?case
    by blast
qed

lemma weakCongSimClosed:
  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"

  shows "Ψ ⊳ P ↝«Rel» Q ⟹ (p ∙ Ψ) ⊳ (p ∙ P) ↝«Rel» (p ∙ Q)"
  and   "P ↝«Rel» Q ⟹ (p ∙ P) ↝«Rel» (p ∙ Q)"
using EqvtRel
by(force dest: weakCongSimClosedAux simp add: permBottom)+

lemma weakCongSimReflexive:
  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: weakCongSimulation_def dest: rtrancl_into_rtrancl)

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

  assumes "Ψ ⊳ Q ⟹⇩τ Q'"
  and     "Ψ ⊳ P ↝«Rel» Q"
  and     Sim: "⋀Ψ P Q. (Ψ, P, Q) ∈ Rel ⟹ Ψ ⊳ P ↝<Rel> Q"
  
  obtains P' where "Ψ ⊳ P ⟹⇩τ P'" and "(Ψ, P', Q') ∈ Rel"
proof -
  assume A: "⋀P'. ⟦Ψ ⊳ P ⟹⇩τ P'; (Ψ, P', Q') ∈ Rel⟧ ⟹ thesis"
  from ‹Ψ ⊳ Q ⟹⇩τ Q'› ‹Ψ ⊳ P ↝«Rel» Q› A show ?thesis
  proof(induct arbitrary: P thesis rule: tauStepChainInduct)
    case(TauBase Q Q' P)
    with ‹Ψ ⊳ P ↝«Rel» Q› ‹Ψ ⊳ Q ⟼τ ≺ Q'› obtain P' where PChain: "Ψ ⊳ P ⟹⇩τ P'" and P'RelQ': "(Ψ, P', Q') ∈ Rel"
      by(rule_tac weakCongSimE)
    thus ?case by(rule TauBase)
  next
    case(TauStep Q Q' Q'' P)
    from ‹Ψ ⊳ P ↝«Rel» Q› obtain P' where PChain: "Ψ ⊳ P ⟹⇩τ P'" and "(Ψ, P', Q') ∈ Rel"
      by(rule TauStep)
    from ‹(Ψ, P', Q') ∈ Rel› have "Ψ ⊳ P' ↝<Rel> Q'" by(rule Sim)
    then obtain P'' where P'Chain: "Ψ ⊳ P' ⟹⇧^⇩τ P''" and "(Ψ, P'', Q'') ∈ Rel"
      using ‹Ψ ⊳ Q' ⟼τ ≺ Q''› by(blast dest: weakSimE)
    from PChain P'Chain have "Ψ ⊳ P ⟹⇩τ P''" by simp
    thus ?case using ‹(Ψ, P'', Q'') ∈ Rel› by(rule TauStep)
  qed
qed

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

  assumes PRelQ: "(Ψ, P, Q) ∈ Rel"
  and     PSimQ: "Ψ ⊳ P ↝«Rel» Q"
  and     QSimR: "Ψ ⊳ Q ↝«Rel'» R"
  and     Set: "{(Ψ, P, R) | Ψ P R. ∃Q. (Ψ, P, Q) ∈ Rel ∧ (Ψ, Q, R) ∈ Rel'} ⊆ Rel''"
  and     Sim: "⋀Ψ P Q. (Ψ, P, Q) ∈ Rel ⟹ Ψ ⊳ P ↝<Rel> Q"

  shows "Ψ ⊳ P ↝«Rel''» R"
proof(induct rule: weakCongSimI)
  case(cTau R')
  from QSimR ‹Ψ ⊳ R ⟼τ ≺ R'› obtain Q' where QChain: "Ψ ⊳ Q ⟹⇩τ Q'" and Q'RelR': "(Ψ, Q', R') ∈ Rel'" 
    by(blast dest: weakCongSimE)
  from QChain PSimQ Sim obtain P' where PChain: "Ψ ⊳ P ⟹⇩τ P'" and P'RelQ': "(Ψ, P', Q') ∈ Rel"
    by(rule weakStepSimTauChain)
  moreover from P'RelQ' Q'RelR' Set have "(Ψ, P', R') ∈ Rel''" by blast
  ultimately show ?case by blast
qed

lemma weakCongSimStatEq:
  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: "⋀Ψ P Q Ψ'. ⟦(Ψ, P, Q) ∈ Rel; Ψ ≃ Ψ'⟧ ⟹ (Ψ', P, Q) ∈ Rel'"

  shows "Ψ' ⊳ P ↝«Rel'» Q"
proof(induct rule: weakCongSimI)
  case(cTau Q')
  from ‹Ψ' ⊳ Q ⟼τ ≺ Q'› ‹Ψ ≃ Ψ'›
  have "Ψ ⊳ Q ⟼τ ≺ Q'" by(metis statEqTransition AssertionStatEqSym)
  with PSimQ obtain P' where PChain: "Ψ ⊳ P ⟹⇩τ P'" and P'RelQ': "(Ψ, P', Q') ∈ Rel"
    by(blast dest: weakCongSimE)
  
  from PChain ‹Ψ ≃ Ψ'› have "Ψ' ⊳ P ⟹⇩τ P'" by(rule tauStepChainStatEq)
  moreover from ‹(Ψ, P', Q') ∈ Rel› ‹Ψ ≃ Ψ'› have "(Ψ', P', Q') ∈ Rel'"
    by(rule C1)
  ultimately show ?case by blast
qed

lemma weakCongSimMonotonic: 
  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(simp (no_asm) add: weakCongSimulation_def) (blast dest: weakCongSimE)+

lemma strongSimWeakCongSim:
  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 ↝[Rel] Q"
  and     "Rel ⊆ Rel'"
  
  shows "Ψ ⊳ P ↝«Rel'» Q"
using assms
apply(auto simp add: simulation_def weakCongSimulation_def)
by(erule_tac x=τ in allE) fastforce

end

end