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