Quelle  Tau_Chain.thy

(* 
   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 ==>_\<tau> P' ≡ (P, P') ∈ {(P, P') | P P'. P ⟼τ ≺ P'}^*"

lemma tauChainInduct[consumes 1, case_names Base Step]:
  assumes "P ==>_\<tau> P'"
  and     "Prop P"
  and     "∧P' P''. [P ==>_\<tau> 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 ==>_\<tau> P"
by(auto simp add: tauChain_def)

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

  assumes "P ==>_\<tau> P'"
  and     "P' ⟼τ ≺ P''"

  shows "P ==>_\<tau> 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 ==>_\<tau> P'"

  shows "P ==>_\<tau> 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 ==>_\<tau> P'"
  and     "P' ==>_\<tau> P''"

  shows "P ==>_\<tau> P''"
using ‹P' ==>_\τ P''› ‹P ==>_\τ P'›
by(induct rule: tauChainInduct) auto

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

  assumes "P ==>_\<tau> P'"
  and     "P ≠ P'"

  shows "P ⊕ Q ==>_\<tau> 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 ==>_\<tau> Q'"
  and     "Q ≠ Q'"

  shows "P ⊕ Q ==>_\<tau> 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 ==>_\<tau> P'"

  shows "P ∥ Q ==>_\<tau> P' ∥ Q"
using assms
by(induct rule: tauChainInduct) (auto intro: Par1)

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

  assumes "Q ==>_\<tau> Q'"

  shows "P ∥ Q ==>_\<tau> P ∥ Q'"
using assms
by(induct rule: tauChainInduct) (auto intro: Par2)

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

  assumes "P ==>_\<tau> P'"

  shows "(νx)P ==>_\<tau> (νx)P'"
using assms
by(induct rule: tauChainInduct) (auto dest: Res)

lemma tauChainRepl:
  fixes P :: ccs

  assumes "P ∥ !P ==>_\<tau> P'"
  and     "P' ≠ P ∥ !P"

  shows "!P ==>_\<tau> 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