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 \<longmapsto>τ \<prec> P'}^*"

lemma tauChainInduct[consumes 1, case_names Base Step]:
  assumes "P ==>⇩τ P'"
  and     "Prop P"
  and     "!!P' P''. [|P ==>⇩τ P'; P' \<longmapsto>τ \<prec> 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' \<longmapsto>τ \<prec> 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' \<longmapsto>τ \<prec> 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 \<parallel> Q ==>⇩τ P' \<parallel> 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 \<parallel> Q ==>⇩τ P \<parallel> 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 \<parallel> !P ==>⇩τ P'"
  and     "P' ≠ P \<parallel> !P"

  shows "!P ==>⇩τ P'"
using assms
apply(induct rule: tauChainInduct)
apply auto
apply(case_tac "P' ≠ P \<parallel> !P")
apply auto
apply(drule Bang)
apply(simp add: tauChain_def)
by auto

end