Theory Late_Tau_Chain

(* 
   Title: The pi-calculus   
   Author/Maintainer: Jesper Bengtson (jebe.dk), 2012
*)
theory Late_Tau_Chain
  imports Late_Semantics1
begin

abbreviation "tauChain_judge" :: "pi ⇒ pi ⇒ bool" ("_ ⟹⇩τ _" [80, 80] 80)
where "P ⟹⇩τ P' ≡ (P, P') ∈ {(P, P') | P P'. P ⟼τ ≺ P'}^*"

lemma singleTauChain:
  fixes P  :: pi
  and   P' :: pi

  assumes "P ⟼τ ≺ P'"

  shows "P ⟹⇩τ P'"
using assms by(simp add: r_into_rtrancl)

lemma tauChainAddTau[dest]:
  fixes P   :: pi
  and   P'  :: pi
  and   P'' :: pi

  shows "P ⟹⇩τ P' ⟹ P' ⟼τ ≺ P'' ⟹ P ⟹⇩τ P''" 
  and "P ⟼τ ≺ P' ⟹ P' ⟹⇩τ P'' ⟹ P ⟹⇩τ P''"
by(auto dest: singleTauChain)

lemma tauChainInduct[consumes 1, case_names id ih]:
  fixes P  :: pi
  and   P' :: pi

  assumes "P ⟹⇩τ P'"
  and     "F P"
  and     "⋀P' P''. ⟦P ⟹⇩τ P'; P' ⟼τ ≺ P''; F P'⟧ ⟹ F P''"

  shows "F P'"
using assms  
by(drule_tac rtrancl_induct) auto

lemma eqvtChainI[eqvt]:
  fixes P    :: pi
  and   P'   :: pi
  and   perm :: "name prm"

  assumes "P ⟹⇩τ P'"

  shows "(perm ∙ P) ⟹⇩τ (perm ∙ P')"
using assms
proof(induct rule: tauChainInduct)
  case id
  thus ?case by simp
next
  case(ih P'' P''')
  have "P ⟹⇩τ P''" and "P'' ⟼ τ ≺ P'''" by fact+
  hence "(perm ∙ P'') ⟼τ ≺ (perm ∙ P''')" by(force dest: transitions.eqvt)
  moreover have "(perm ∙ P) ⟹⇩τ (perm ∙ P'')" by fact
  ultimately show ?case by auto
qed


lemma eqvtChainE:
  fixes perm :: "name prm"
  and   P    :: pi
  and   P'   :: pi

  assumes Trans: "(perm ∙ P) ⟹⇩τ (perm ∙ P')"

  shows   "P ⟹⇩τ P'"
proof -
  have "rev perm ∙ (perm ∙ P) = P" by(simp add: pt_rev_pi[OF pt_name_inst, OF at_name_inst])
  moreover have "rev perm ∙ (perm ∙ P') = P'" by(simp add: pt_rev_pi[OF pt_name_inst, OF at_name_inst])
  ultimately show ?thesis using assms
    by(drule_tac perm="rev perm" in eqvtChainI, simp)
qed

lemma eqvtChainEq:
  fixes P    :: pi
  and   P'   :: pi
  and   perm :: "name prm"

  shows   "P ⟹⇩τ P' = (perm ∙ P) ⟹⇩τ (perm ∙ P')"
by(blast intro: eqvtChainE eqvtChainI)

lemma freshChain:
  fixes P  :: pi
  and   P' :: pi
  and   x  :: name
  
  assumes "P ⟹⇩τ P'"
  and     "x ♯ P"
 
  shows   "x ♯ P'"
using assms
proof(induct rule: tauChainInduct)
  case id
  thus ?case by simp
next
  case(ih P' P'')
  have "x ♯ P" and "x ♯ P ⟹ x ♯ P'" by fact+
  hence "x ♯ P'" by simp
  moreover have "P' ⟼ τ ≺ P''" by fact
  ultimately show ?case by(force intro: freshFreeDerivative)
qed

lemma matchChain:
  fixes b :: name
  and   P :: pi
  and   P' :: pi
  
  assumes "P ⟹⇩τ P'"
  and     "P ≠ P'"
 
  shows "[b⌢b]P ⟹⇩τ P'"
using assms
proof(induct rule: tauChainInduct)
  case id
  thus ?case by simp
next
  case(ih P'' P''')
  have P''TransP''':  "P'' ⟼τ ≺ P'''"  by fact
  show "[b⌢b]P ⟹⇩τ P'''" 
  proof(cases "P = P''")
    assume "P=P''"
    moreover with P''TransP''' have "[b⌢b]P ⟼τ ≺ P'''" by(force intro: Match)
    thus "[b⌢b]P ⟹⇩τ P'''" by(rule singleTauChain)
  next
    assume "P ≠ P''"
    moreover have "P ≠ P'' ⟹ [b⌢b]P ⟹⇩τ P''" by fact
    ultimately show "[b⌢b]P ⟹⇩τ P'''" using P''TransP''' by(blast)
  qed
qed

lemma mismatchChain:
  fixes a :: name
  and   b :: name
  and   P :: pi
  and   P' :: pi
  
  assumes PChain: "P ⟹⇩τ P'"
  and     aineqb: "a ≠ b"
  and     PineqP': "P ≠ P'"
 
  shows "[a≠b]P ⟹⇩τ P'"
using PChain PineqP'
proof(induct rule: tauChainInduct)
  case id
  thus ?case by simp
next
  case(ih P'' P''')
  have P''TransP''':  "P'' ⟼τ ≺ P'''"  by fact
  show "[a≠b]P ⟹⇩τ P'''" 
  proof(cases "P = P''")
    assume "P=P''"
    moreover with aineqb P''TransP''' have "[a≠b]P ⟼τ ≺ P'''" by(force intro: Mismatch)
    thus "[a≠b]P ⟹⇩τ P'''" by(rule singleTauChain)
  next
    assume "P ≠ P''"
    moreover have "P ≠ P'' ⟹ [a≠b]P ⟹⇩τ P''" by fact+
    ultimately show "[a≠b]P ⟹⇩τ P'''" using P''TransP''' by(blast)
  qed
qed

lemma sum1Chain[rule_format]:
  fixes P  :: pi
  and   P' :: pi
  and   Q  :: pi

  assumes "P ⟹⇩τ P'"
  and     "P ≠ P'"
 
  shows "P ⊕ Q ⟹⇩τ P'"
using assms
proof(induct rule: tauChainInduct)
  case id
  thus ?case by simp
next
  case(ih P'' P''')
  have P''TransP''':  "P'' ⟼τ ≺ P'''" by fact
  show "P ⊕ Q ⟹⇩τ P'''"
  proof(cases "P = P''")
    assume "P=P''"
    moreover with P''TransP''' have "P ⊕ Q ⟼τ ≺ P'''" by(force intro: Sum1)
    thus "P ⊕ Q ⟹⇩τ P'''" by(force intro: singleTauChain)
  next
    assume "P ≠ P''"
    moreover have "P ≠ P'' ⟹ P ⊕ Q ⟹⇩τ P''" by fact
    ultimately show "P ⊕ Q ⟹⇩τ P'''" using P''TransP''' by(force)
  qed
qed


lemma sum2Chain[rule_format]:
  fixes P  :: pi
  and   Q :: pi
  and   Q'  :: pi

  assumes "Q ⟹⇩τ Q'"
  and     "Q ≠ Q'"
 
  shows "P ⊕ Q ⟹⇩τ Q'"
using assms
proof(induct rule: tauChainInduct)
  case id
  thus ?case by simp
next
  case(ih Q'' Q''')
  have Q''TransQ''':  "Q'' ⟼τ ≺ Q'''" by fact
  show "P ⊕ Q ⟹⇩τ Q'''"
  proof(cases "Q = Q''")
    assume "Q=Q''"
    moreover with Q''TransQ''' have "P ⊕ Q ⟼τ ≺ Q'''" by(force intro: Sum2)
    thus "P ⊕ Q ⟹⇩τ Q'''" by(force intro: singleTauChain)
  next
    assume "Q ≠ Q''"
    moreover have "Q ≠ Q'' ⟹ P ⊕ Q ⟹⇩τ Q''" by fact
    ultimately show "P ⊕ Q ⟹⇩τ Q'''" using Q''TransQ''' by blast
  qed
qed

lemma Par1Chain:
  fixes P  :: pi
  and   P' :: pi
  and   Q  :: pi

  assumes "P ⟹⇩τ P'"

  shows "P ∥ Q ⟹⇩τ P' ∥ Q"
using assms
proof(induct rule: tauChainInduct)
  case id
  thus ?case by simp
next
  case(ih P'' P')
  have P''TransP':  "P'' ⟼τ ≺ P'" by fact
  have IH: "P ∥ Q ⟹⇩τ P'' ∥ Q" by fact
  
  have "P'' ∥ Q ⟼τ ≺ P' ∥ Q" using P''TransP' by(force intro: Par1F)
  thus "P ∥ Q ⟹⇩τ P' ∥ Q" using IH by(force)
qed

lemma Par2Chain:
  fixes P  :: pi
  and   Q  :: pi
  and   Q' :: pi

  assumes "Q ⟹⇩τ Q'"

  shows "P ∥ Q ⟹⇩τ P ∥ Q'"
using assms
proof(induct rule: tauChainInduct)
  case id
  thus ?case by simp
next
  case(ih Q'' Q')
  have Q''TransQ':  "Q'' ⟼τ ≺ Q'" by fact
  have IH: "P ∥ Q ⟹⇩τ P ∥ Q''" by fact
  
  have "P ∥ Q'' ⟼τ ≺ P ∥ Q'" using Q''TransQ' by(force intro: Par2F)
  thus "P ∥ Q ⟹⇩τ P ∥ Q'" using IH by(force)
qed

lemma chainPar:
  fixes P  :: pi
  and   P' :: pi
  and   Q  :: pi
  and   Q' :: pi
  
  assumes "P ⟹⇩τ P'"
  and     "Q ⟹⇩τ Q'"

  shows "P ∥ Q ⟹⇩τ P' ∥ Q'"
proof -
  from ‹P ⟹⇩τ P'› have "P ∥ Q ⟹⇩τ P' ∥ Q" by(rule Par1Chain)
  moreover from ‹Q ⟹⇩τ Q'› have "P' ∥ Q ⟹⇩τ P' ∥ Q'" by(rule Par2Chain)
  ultimately show ?thesis by auto
qed

lemma ResChain:
  fixes P  :: pi
  and   P' :: pi
  and   a  :: name

  assumes "P ⟹⇩τ P'"

  shows "<νa>P ⟹⇩τ <νa>P'"
using assms
proof(induct rule: tauChainInduct)
  case id
  thus ?case by simp
next
  case(ih P'' P''')
  have "P'' ⟼τ ≺ P'''" by fact
  hence "<νa>P'' ⟼τ ≺ <νa>P'''" by(force intro: ResF)
  moreover have "<νa>P ⟹⇩τ <νa>P''" by fact
  ultimately show ?case by force
qed

lemma substChain:
  fixes P  :: pi
  and   x  :: name
  and   b  :: name
  and   P' :: pi

  assumes PTrans: "P[x::=b] ⟹⇩τ P'"

  shows "P[x::=b] ⟹⇩τ P'[x::=b]"
proof(cases "x=b")
  assume "x = b"
  with PTrans show ?thesis by simp
next
  assume "x ≠ b"
  hence "x ♯ P[x::=b]" by(simp add: fresh_fact2)
  with PTrans have "x ♯ P'" by(force intro: freshChain)
  hence "P' = P'[x::=b]" by(simp add: forget)
  with PTrans show ?thesis by simp
qed

lemma bangChain:
  fixes P  :: pi
  and   P' :: pi

  assumes PTrans: "P ∥ !P ⟹⇩τ P'"
  and     P'ineq: "P' ≠ P ∥ !P"

  shows "!P ⟹⇩τ P'"
using assms
proof(induct rule: tauChainInduct)
  case id
  thus ?case by simp
next
  case(ih P' P'')
  show ?case
  proof(cases "P' = P ∥ !P")
    case True
    from ‹P' ⟼τ ≺ P''› ‹P' = P ∥ !P› have "!P ⟼τ ≺ P''" by(blast intro: Bang)
    thus ?thesis by auto
  next
    case False
    from ‹P' ≠ P ∥ !P› have "!P ⟹⇩τ P'" by(rule ih)
    with ‹P' ⟼τ ≺ P''› show ?thesis by auto
  qed
qed

end