Theory Weak_Cong_Sim

(* 
   Title: The Calculus of Communicating Systems   
   Author/Maintainer: Jesper Bengtson (jebe@itu.dk), 2012
*)
theory Weak_Cong_Sim
  imports Weak_Cong_Semantics Weak_Sim Strong_Sim
begin

definition weakCongSimulation :: "ccs ⇒ (ccs × ccs) set ⇒ ccs ⇒ bool"   ("_ ↝<_> _" [80, 80, 80] 80)
where
  "P ↝<Rel> Q ≡ ∀a Q'. Q ⟼a ≺ Q' ⟶ (∃P'. P ⟹a ≺ P' ∧ (P', Q') ∈ Rel)"

lemma weakSimI[case_names Sim]:
  fixes P   :: ccs
  and   Rel :: "(ccs × ccs) set"
  and   Q   :: ccs

  assumes "⋀α Q'. Q ⟼α ≺ Q' ⟹ ∃P'. P ⟹α ≺ P' ∧ (P', Q') ∈ Rel"

  shows "P ↝<Rel> Q"
using assms
by(auto simp add: weakCongSimulation_def)

lemma weakSimE:
  fixes P   :: ccs
  and   Rel :: "(ccs × ccs) set"
  and   Q   :: ccs
  and   α   :: act
  and   Q'  :: ccs

  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 simWeakSim:
  fixes P   :: ccs
  and   Rel :: "(ccs × ccs) set"
  and   Q   :: ccs

  assumes "P ↝[Rel] Q"
  
  shows "P ↝<Rel> Q"
using assms
by(rule_tac weakSimI, auto)
  (blast dest: simE transitionWeakCongTransition)

lemma weakCongSimWeakSim:
  fixes P   :: ccs
  and   Rel :: "(ccs × ccs) set"
  and   Q   :: ccs

  assumes "P ↝<Rel> Q"
  
  shows "P ↝⇧^<Rel> Q"
using assms
by(rule_tac Weak_Sim.weakSimI, auto)
  (blast dest: weakSimE weakCongTransitionWeakTransition)

lemma test:
  assumes "P ⟹⇩τ P'"

  shows "P = P' ∨ (∃P''. P ⟼τ ≺ P'' ∧ P'' ⟹⇩τ P')"
using assms
by(induct rule: tauChainInduct) auto

lemma tauChainCasesSym[consumes 1, case_names cTauNil cTauStep]:
  assumes "P ⟹⇩τ P'"
  and     "Prop P"
  and     "⋀P''. ⟦P ⟼τ ≺ P''; P'' ⟹⇩τ P'⟧ ⟹ Prop P'"

  shows "Prop P'"
using assms
by(blast dest: test)

lemma simE2:
  fixes P   :: ccs
  and   Rel :: "(ccs × ccs) set"
  and   Q   :: ccs
  and   α   :: act
  and   Q'  :: ccs

  assumes "P ↝<Rel> Q"
  and     "Q ⟹α ≺ Q'"
  and     Sim: "⋀R S. (R, S) ∈ Rel ⟹ R ↝⇧^<Rel> S"
  
  obtains P' where "P ⟹α ≺ P'" and "(P', Q') ∈ Rel"
proof -
  assume Goal: "⋀P'. ⟦P ⟹α ≺ P'; (P', Q') ∈ Rel⟧ ⟹ thesis"
  from ‹Q ⟹α ≺ Q'› obtain Q''' Q''
    where QChain: "Q ⟹⇩τ Q'''" and Q'''Trans: "Q''' ⟼α ≺ Q''" and Q''Chain: "Q'' ⟹⇩τ Q'"
    by(rule weakCongTransE)
  from QChain Q'''Trans show ?thesis
  proof(induct rule: tauChainCasesSym)
    case cTauNil
    from ‹P ↝<Rel> Q› ‹Q ⟼α ≺ Q''› obtain P''' where PTrans: "P ⟹α ≺ P'''" and "(P''', Q'') ∈ Rel"
      by(blast dest: weakSimE)
    moreover from Q''Chain ‹(P''', Q'') ∈ Rel› Sim obtain P' where P''Chain: "P''' ⟹⇩τ P'" and "(P', Q') ∈ Rel"
      by(rule simTauChain)
    with PTrans P''Chain show ?thesis
      by(force intro: Goal simp add: weakCongTrans_def weakTrans_def)
  next
    case(cTauStep Q'''')
    from ‹P ↝<Rel> Q› ‹Q ⟼τ ≺ Q''''› obtain P'''' where  PChain: "P ⟹τ ≺ P''''" and "(P'''', Q'''') ∈ Rel"
      by(drule_tac weakSimE) auto
    from ‹Q'''' ⟹⇩τ Q'''› ‹(P'''', Q'''') ∈ Rel› Sim obtain P''' where P''''Chain: "P'''' ⟹⇩τ P'''" and "(P''', Q''') ∈ Rel"
      by(rule simTauChain)
    from ‹(P''', Q''') ∈ Rel› have "P''' ↝⇧^<Rel> Q'''" by(rule Sim)
    then obtain P'' where P'''Trans: "P''' ⟹⇧^α ≺ P''" and "(P'', Q'') ∈ Rel" using Q'''Trans by(rule Weak_Sim.weakSimE)
    from Q''Chain ‹(P'', Q'') ∈ Rel› Sim obtain P' where P''Chain: "P'' ⟹⇩τ P'" and "(P', Q') ∈ Rel"
      by(rule simTauChain)
    from PChain P''''Chain P'''Trans P''Chain
    have "P ⟹α ≺ P'"
      apply(auto simp add: weakCongTrans_def weakTrans_def)
      apply(rule_tac x=P''aa in exI)
      apply auto
      defer
      apply blast
      by(auto simp add: tauChain_def)

    with ‹(P', Q') ∈ Rel› show ?thesis
      by(force intro: Goal simp add: weakCongTrans_def weakTrans_def)
  qed
qed

lemma reflexive:
  fixes P   :: ccs
  and   Rel :: "(ccs × ccs) set"
  
  assumes "Id ⊆ Rel"

  shows "P ↝<Rel> P"
using assms
by(auto simp add: weakCongSimulation_def intro: transitionWeakCongTransition)
  
lemma transitive:
  fixes P     :: ccs
  and   Rel   :: "(ccs × ccs) set"
  and   Q     :: ccs
  and   Rel'  :: "(ccs × ccs) set"
  and   R     :: ccs
  and   Rel'' :: "(ccs × ccs) set"
  
  assumes "P ↝<Rel> Q"
  and     "Q ↝<Rel'> R"
  and     "Rel O Rel' ⊆ Rel''"
  and     "⋀S T. (S, T) ∈ Rel ⟹ S ↝⇧^<Rel> T"
  
  shows "P ↝<Rel''> R"
proof(induct rule: weakSimI)
  case(Sim α R')
  thus ?case using assms
    apply(drule_tac Q=R in weakSimE, auto)
    by(drule_tac Q=Q in simE2) auto
qed

lemma weakMonotonic:
  fixes P :: ccs
  and   A :: "(ccs × ccs) set"
  and   Q :: ccs
  and   B :: "(ccs × ccs) set"

  assumes "P ↝<A> Q"
  and     "A ⊆ B"

  shows "P ↝<B> Q"
using assms
by(fastforce simp add: weakCongSimulation_def)

end