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 "⦇νxP = ⦇ν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  α  ⦇νxP α  ⦇νxP'"
| 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 𝒞 (⦇νxP) α (⦇νxP');
 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 "⦇νxP α  P'"
  and     "P'. P α  P'; x  α  Prop (⦇νxP')"

  shows "Prop P'"
proof -
  from ⦇νxP α  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 (⦇νxPa)") 
    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