Theory Tau_Chain

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


definition tauChain :: "ccs ⇒ ccs ⇒ bool" (‹_ ⟹⇩τ _› [80, 80] 80)
  where "P ⟹⇩τ P' ≡ (P, P') ∈ {(P, P') | P P'. P ⟼τ ≺ P'}^*"

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

  shows "Prop P'"
using assms
by(auto simp add: tauChain_def elim: rtrancl_induct)

lemma tauChainRefl[simp]:
  fixes P :: ccs

  shows "P ⟹⇩τ P"
by(auto simp add: tauChain_def)

lemma tauChainCons[dest]:
  fixes P   :: ccs
  and   P'  :: ccs
  and   P'' :: ccs

  assumes "P ⟹⇩τ P'"
  and     "P' ⟼τ ≺ P''"

  shows "P ⟹⇩τ P''"
using assms
by(auto simp add: tauChain_def) (blast dest: rtrancl_trans)

lemma tauChainCons2[dest]:
  fixes P   :: ccs
  and   P'  :: ccs
  and   P'' :: ccs

  assumes "P' ⟼τ ≺ P''"
  and     "P ⟹⇩τ P'"

  shows "P ⟹⇩τ P''"
using assms
by(auto simp add: tauChain_def) (blast dest: rtrancl_trans)

lemma tauChainAppend[dest]:
  fixes P   :: ccs
  and   P'  :: ccs
  and   P'' :: ccs

  assumes "P ⟹⇩τ P'"
  and     "P' ⟹⇩τ P''"

  shows "P ⟹⇩τ P''"
using ‹P' ⟹⇩τ P''› ‹P ⟹⇩τ P'›
by(induct rule: tauChainInduct) auto

lemma tauChainSum1:
  fixes P  :: ccs
  and   P' :: ccs
  and   Q  :: ccs

  assumes "P ⟹⇩τ P'"
  and     "P ≠ P'"

  shows "P ⊕ Q ⟹⇩τ P'"
using assms
proof(induct rule: tauChainInduct)
  case Base 
  thus ?case by simp
next
  case(Step P' P'')
  thus ?case
    by(case_tac "P=P'") (auto intro: Sum1 simp add: tauChain_def)
qed

lemma tauChainSum2:
  fixes P  :: ccs
  and   P' :: ccs
  and   Q  :: ccs

  assumes "Q ⟹⇩τ Q'"
  and     "Q ≠ Q'"

  shows "P ⊕ Q ⟹⇩τ Q'"
using assms
proof(induct rule: tauChainInduct)
  case Base 
  thus ?case by simp
next
  case(Step Q' Q'')
  thus ?case
    by(case_tac "Q=Q'") (auto intro: Sum2 simp add: tauChain_def)
qed

lemma tauChainPar1:
  fixes P  :: ccs
  and   P' :: ccs
  and   Q  :: ccs

  assumes "P ⟹⇩τ P'"

  shows "P ∥ Q ⟹⇩τ P' ∥ Q"
using assms
by(induct rule: tauChainInduct) (auto intro: Par1)

lemma tauChainPar2:
  fixes Q  :: ccs
  and   Q' :: ccs
  and   P  :: ccs

  assumes "Q ⟹⇩τ Q'"

  shows "P ∥ Q ⟹⇩τ P ∥ Q'"
using assms
by(induct rule: tauChainInduct) (auto intro: Par2)

lemma tauChainRes:
  fixes P  :: ccs
  and   P' :: ccs
  and   x  :: name

  assumes "P ⟹⇩τ P'"

  shows "⦇νx⦈P ⟹⇩τ ⦇νx⦈P'"
using assms
by(induct rule: tauChainInduct) (auto dest: Res)

lemma tauChainRepl:
  fixes P :: ccs

  assumes "P ∥ !P ⟹⇩τ P'"
  and     "P' ≠ P ∥ !P"

  shows "!P ⟹⇩τ P'"
using assms
apply(induct rule: tauChainInduct)
apply auto
apply(case_tac "P' ≠ P ∥ !P")
apply auto
apply(drule Bang)
apply(simp add: tauChain_def)
by auto

end