Theory Agent

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

atom_decl name

nominal_datatype act = actAction name      ("⦇_⦈" 100)
                     | actCoAction name    ("⟨_⟩" 100)
                     | actTau              ("τ" 100)

nominal_datatype ccs = CCSNil           ("𝟬" 115)
                     | Action act ccs   ("_._" [120, 110] 110)
                     | Sum ccs ccs      (infixl "⊕" 90)
                     | Par ccs ccs      (infixl "∥" 85)
                     | Res "«name» ccs" ("⦇ν_⦈_" [105, 100] 100)
                     | Bang ccs         ("!_" [95])

nominal_primrec coAction :: "act ⇒ act"
where
  "coAction (⦇a⦈) = (⟨a⟩)"
| "coAction (⟨a⟩)= (⦇a⦈)"
| "coAction (τ) = τ"
by(rule TrueI)+

lemma coActionEqvt[eqvt]:
  fixes p :: "name prm"
  and   a :: act

  shows "(p ∙ coAction a) = coAction(p ∙ a)"
by(nominal_induct a rule: act.strong_induct) (auto simp add: eqvts)

lemma coActionSimps[simp]:
  fixes a :: act

  shows "coAction(coAction a) = a"
  and   "(coAction a = τ) = (a = τ)"
by auto (nominal_induct rule: act.strong_induct, auto)+

lemma coActSimp[simp]: shows "coAction α ≠ τ = (α ≠ τ)" and "(coAction α = τ) = (α = τ)"
by(nominal_induct α rule: act.strong_induct) auto
    
lemma coActFresh[simp]:
  fixes x :: name
  and   a :: act

  shows "x ♯ coAction a = x ♯ a"
by(nominal_induct a rule: act.strong_induct) (auto)
  
lemma alphaRes:
  fixes y :: name
  and   P :: ccs
  and   x :: name

  assumes "y ♯ P"
  
  shows "⦇νx⦈P = ⦇νy⦈([(x, y)] ∙ P)"
using assms
by(auto simp add: ccs.inject alpha fresh_left calc_atm pt_swap_bij[OF pt_name_inst, OF at_name_inst]pt3[OF pt_name_inst, OF at_ds1[OF at_name_inst]])

inductive semantics :: "ccs ⇒ act ⇒ ccs ⇒ bool"    ("_ ⟼_ ≺ _" [80, 80, 80] 80)
where
  Action:   "α.(P) ⟼α ≺ P"
| Sum1:     "P ⟼α ≺ P' ⟹ P ⊕ Q ⟼α ≺ P'"
| Sum2:     "Q ⟼α ≺ Q' ⟹ P ⊕ Q ⟼α ≺ Q'"
| Par1:     "P ⟼α ≺ P' ⟹ P ∥ Q ⟼α ≺ P' ∥ Q"
| Par2:     "Q ⟼α ≺ Q' ⟹ P ∥ Q ⟼α ≺ P ∥ Q'"
| Comm:     "⟦P ⟼a ≺ P'; Q ⟼(coAction a) ≺ Q'; a ≠ τ⟧ ⟹ P ∥ Q ⟼τ ≺ P' ∥ Q'"
| Res:      "⟦P ⟼α ≺ P'; x ♯ α⟧ ⟹ ⦇νx⦈P ⟼α ≺ ⦇νx⦈P'"
| Bang:     "P ∥ !P ⟼α ≺ P' ⟹ !P ⟼α ≺ P'"

equivariance semantics

nominal_inductive semantics
by(auto simp add: abs_fresh)

lemma semanticsInduct:
"⟦R ⟼β ≺ R'; ⋀α P 𝒞. Prop 𝒞 (α.(P)) α P;
 ⋀P α P' Q 𝒞. ⟦P ⟼α ≺ P'; ⋀𝒞. Prop 𝒞 P α P'⟧ ⟹ Prop 𝒞 (ccs.Sum P Q) α P';
 ⋀Q α Q' P 𝒞. ⟦Q ⟼α ≺ Q'; ⋀𝒞. Prop 𝒞 Q α Q'⟧ ⟹ Prop 𝒞 (ccs.Sum P Q) α Q';
 ⋀P α P' Q 𝒞. ⟦P ⟼α ≺ P'; ⋀𝒞. Prop 𝒞 P α P'⟧ ⟹ Prop 𝒞 (P ∥ Q) α (P' ∥ Q);
 ⋀Q α Q' P 𝒞. ⟦Q ⟼α ≺ Q'; ⋀𝒞. Prop 𝒞 Q α Q'⟧ ⟹ Prop 𝒞 (P ∥ Q) α (P ∥ Q');
 ⋀P a P' Q Q' 𝒞.
    ⟦P ⟼a ≺ P'; ⋀𝒞. Prop 𝒞 P a P'; Q ⟼(coAction a) ≺ Q';
     ⋀𝒞. Prop 𝒞 Q (coAction a) Q'; a ≠ τ⟧
    ⟹ Prop 𝒞 (P ∥ Q) (τ) (P' ∥ Q');
 ⋀P α P' x 𝒞.
    ⟦x ♯ 𝒞; P ⟼α ≺ P'; ⋀𝒞. Prop 𝒞 P α P'; x ♯ α⟧ ⟹ Prop 𝒞 (⦇νx⦈P) α (⦇νx⦈P');
 ⋀P α P' 𝒞. ⟦P ∥ !P ⟼α ≺ P'; ⋀𝒞. Prop 𝒞 (P ∥ !P) α P'⟧ ⟹ Prop 𝒞 !P α P'⟧

⟹ Prop (𝒞::'a::fs_name) R β R'"
by(erule_tac z=𝒞 in semantics.strong_induct) auto

lemma NilTrans[dest]:
  shows "𝟬 ⟼α ≺ P' ⟹ False"
  and   "(⦇b⦈).P ⟼⟨c⟩ ≺ P' ⟹ False"
  and   "(⦇b⦈).P ⟼τ ≺ P' ⟹ False"
  and   "(⟨b⟩).P ⟼⦇c⦈ ≺ P' ⟹ False"
  and   "(⟨b⟩).P ⟼τ ≺ P' ⟹ False"
apply(ind_cases "𝟬 ⟼α ≺ P'")
apply(ind_cases "(⦇b⦈).P ⟼⟨c⟩ ≺ P'", auto simp add: ccs.inject)
apply(ind_cases "(⦇b⦈).P ⟼τ ≺ P'", auto simp add: ccs.inject)
apply(ind_cases "(⟨b⟩).P ⟼⦇c⦈ ≺ P'", auto simp add: ccs.inject)
apply(ind_cases "(⟨b⟩).P ⟼τ ≺ P'", auto simp add: ccs.inject)
done

lemma freshDerivative:
  fixes P  :: ccs
  and   a  :: act
  and   P' :: ccs
  and   x  :: name

  assumes "P ⟼α ≺ P'"
  and     "x ♯ P"

  shows "x ♯ α" and "x ♯ P'"
using assms
by(nominal_induct rule: semantics.strong_induct)
  (auto simp add: ccs.fresh abs_fresh)
  
lemma actCases[consumes 1, case_names cAct]:
  fixes α  :: act
  and   P  :: ccs
  and   β  :: act
  and   P' :: ccs

  assumes "α.(P) ⟼β ≺ P'"
  and     "Prop α P"

  shows "Prop β P'"
using assms
by - (ind_cases "α.(P) ⟼β ≺ P'", auto simp add: ccs.inject)

lemma sumCases[consumes 1, case_names cSum1 cSum2]:
  fixes P :: ccs
  and   Q :: ccs
  and   α :: act
  and   R :: ccs

  assumes "P ⊕ Q ⟼α ≺ R"
  and     "⋀P'. P ⟼α ≺ P' ⟹ Prop P'"
  and     "⋀Q'. Q ⟼α ≺ Q' ⟹ Prop Q'"

  shows "Prop R"
using assms
by - (ind_cases "P ⊕ Q ⟼α ≺ R", auto simp add: ccs.inject)

lemma parCases[consumes 1, case_names cPar1 cPar2 cComm]:
  fixes P :: ccs
  and   Q :: ccs
  and   a :: act
  and   R :: ccs

  assumes "P ∥ Q ⟼α ≺ R"
  and     "⋀P'. P ⟼α ≺ P' ⟹ Prop α (P' ∥ Q)"
  and     "⋀Q'. Q ⟼α ≺ Q' ⟹ Prop α (P ∥ Q')"
  and     "⋀P' Q' a. ⟦P ⟼a ≺ P'; Q ⟼(coAction a) ≺ Q'; a ≠ τ; α = τ⟧ ⟹ Prop (τ) (P' ∥ Q')"

  shows "Prop α R"
using assms
by - (ind_cases "P ∥ Q ⟼α ≺ R", auto simp add: ccs.inject)

lemma resCases[consumes 1, case_names cRes]:
  fixes x  :: name
  and   P  :: ccs
  and   α  :: act
  and   P' :: ccs

  assumes "⦇νx⦈P ⟼α ≺ P'"
  and     "⋀P'. ⟦P ⟼α ≺ P'; x ♯ α⟧ ⟹ Prop (⦇νx⦈P')"

  shows "Prop P'"
proof -
  from ‹⦇νx⦈P ⟼α ≺ P'› have "x ♯ α" and "x ♯ P'"
    by(auto intro: freshDerivative simp add: abs_fresh)+
  with assms show ?thesis
    by(cases rule: semantics.strong_cases[of _ _ _ _ x])
      (auto simp add: abs_fresh ccs.inject alpha)
qed

inductive bangPred :: "ccs ⇒ ccs ⇒ bool"
where
  aux1: "bangPred P (!P)"
| aux2: "bangPred P (P ∥ !P)"

lemma bangInduct[consumes 1, case_names cPar1 cPar2 cComm cBang]:
  fixes P  :: ccs
  and   α  :: act
  and   P' :: ccs
  and   𝒞  :: "'a::fs_name"

  assumes "!P ⟼α ≺ P'"
  and     rPar1: "⋀α P' 𝒞. ⟦P ⟼α ≺ P'⟧ ⟹ Prop 𝒞 (P ∥ !P) α (P' ∥ !P)"
  and     rPar2: "⋀α P' 𝒞. ⟦!P ⟼α ≺ P'; ⋀𝒞. Prop 𝒞 (!P) α P'⟧ ⟹ Prop 𝒞 (P ∥ !P) α (P ∥ P')"
  and     rComm: "⋀a P' P'' 𝒞. ⟦P ⟼a ≺ P'; !P ⟼(coAction a) ≺ P''; ⋀𝒞. Prop 𝒞 (!P) (coAction a) P''; a ≠ τ⟧ ⟹ Prop 𝒞 (P ∥ !P) (τ) (P' ∥ P'')"
  and     rBang: "⋀α P' 𝒞. ⟦P ∥ !P ⟼α ≺ P'; ⋀𝒞. Prop 𝒞 (P ∥ !P) α P'⟧ ⟹ Prop 𝒞 (!P) α P'"


  shows "Prop 𝒞 (!P) α P'"
proof -
  {
    fix X α P'
    assume "X ⟼α ≺ P'" and "bangPred P X"
    hence "Prop 𝒞 X α P'"
    proof(nominal_induct avoiding: 𝒞 rule: semantics.strong_induct)
      case(Action α Pa)
      thus ?case 
        by - (ind_cases "bangPred P (α.(Pa))") 
    next
      case(Sum1 Pa α P' Q)
      thus ?case
        by - (ind_cases "bangPred P (Pa ⊕ Q)") 
    next
      case(Sum2 Q α Q' Pa)
      thus ?case
        by - (ind_cases "bangPred P (Pa ⊕ Q)") 
    next
      case(Par1 Pa α P' Q)
      thus ?case
        apply -
        by(ind_cases "bangPred P (Pa ∥ Q)", auto intro: rPar1 simp add: ccs.inject)
    next
      case(Par2 Q α P' Pa)
      thus ?case
        apply -
        by(ind_cases "bangPred P (Pa ∥ Q)", auto intro: rPar2 aux1 simp add: ccs.inject)
    next
      case(Comm Pa a P' Q Q' C)
      thus ?case
        apply -
        by(ind_cases "bangPred P (Pa ∥ Q)", auto intro: rComm aux1 simp add: ccs.inject)
    next
      case(Res Pa α P' x)
      thus ?case
        by - (ind_cases "bangPred P (⦇νx⦈Pa)") 
    next
      case(Bang Pa α P')
      thus ?case
        apply -
        by(ind_cases "bangPred P (!Pa)", auto intro: rBang aux2 simp add: ccs.inject)
    qed
  }
  with ‹!P ⟼α ≺ P'› show ?thesis by(force intro: bangPred.aux1)
qed

inductive_set bangRel :: "(ccs × ccs) set ⇒ (ccs × ccs) set"
for Rel :: "(ccs × ccs) set"
where
  BRBang: "(P, Q) ∈ Rel ⟹ (!P, !Q) ∈ bangRel Rel"
| BRPar: "(R, T) ∈ Rel ⟹ (P, Q) ∈ (bangRel Rel) ⟹ (R ∥ P, T ∥ Q) ∈ (bangRel Rel)"

lemma BRBangCases[consumes 1, case_names BRBang]:
  fixes P   :: ccs
  and   Q   :: ccs
  and   Rel :: "(ccs × ccs) set"
  and   F   :: "ccs ⇒ bool"

  assumes "(P, !Q) ∈ bangRel Rel"
  and     "⋀P. (P, Q) ∈ Rel ⟹ F (!P)"
  
  shows "F P"
using assms
by - (ind_cases "(P, !Q) ∈ bangRel Rel", auto simp add: ccs.inject) 

lemma BRParCases[consumes 1, case_names BRPar]:
  fixes P   :: ccs
  and   Q   :: ccs
  and   Rel :: "(ccs × ccs) set"
  and   F   :: "ccs ⇒ bool"

  assumes "(P, Q ∥ !Q) ∈ bangRel Rel"
  and     "⋀P R. ⟦(P, Q) ∈ Rel; (R, !Q) ∈ bangRel Rel⟧ ⟹ F (P ∥ R)"

  shows "F P"
using assms
by - (ind_cases "(P, Q ∥ !Q) ∈ bangRel Rel", auto simp add: ccs.inject) 

lemma bangRelSubset:
  fixes Rel  :: "(ccs × ccs) set"
  and   Rel' :: "(ccs × ccs) set"

  assumes "(P, Q) ∈ bangRel Rel"
  and     "⋀P Q. (P, Q) ∈ Rel ⟹ (P, Q) ∈ Rel'"

  shows "(P, Q) ∈ bangRel Rel'"
using assms
by(induct rule:  bangRel.induct) (auto intro: BRBang BRPar)

end