theory Agent
imports Nominal
begin
atom_decl name
nominal_datatype act = actAction name ("(|_|))," 100)
| actCoAction name ("⟨_⟩" 100)
| actTau ("τ" 100)
nominal_datatype ccs = CCSNil ("\<zero>" 115)
| Action act ccs ("_._" [120, 110] 110)
| Sum ccs ccs (infixl "⊕" 90)
| Par ccs ccs (infixl "\<parallel>" 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 \<sharp> coAction a = x \<sharp> a"
by(nominal_induct a rule: act.strong_induct) (auto)
lemma alphaRes:
fixes y :: name
and P :: ccs
and x :: name
assumes "y \<sharp> 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" ("_ \<longmapsto>_ \<prec> _" [80, 80, 80] 80)
where
Action: "α.(P) \<longmapsto>α \<prec> P"
| Sum1: "P \<longmapsto>α \<prec> P' ==> P ⊕ Q \<longmapsto>α \<prec> P'"
| Sum2: "Q \<longmapsto>α \<prec> Q' ==> P ⊕ Q \<longmapsto>α \<prec> Q'"
| Par1: "P \<longmapsto>α \<prec> P' ==> P \<parallel> Q \<longmapsto>α \<prec> P' \<parallel> Q"
| Par2: "Q \<longmapsto>α \<prec> Q' ==> P \<parallel> Q \<longmapsto>α \<prec> P \<parallel> Q'"
| Comm: "[|P \<longmapsto>a \<prec> P'; Q \<longmapsto>(coAction a) \<prec> Q'; a ≠ τ|] ==> P \<parallel> Q \<longmapsto>τ \<prec> P' \<parallel> Q'"
| Res: "[|P \<longmapsto>α \<prec> P'; x \<sharp> α|] ==> (|νx|)),P \<longmapsto>α \<prec> (|νx|)),P'"
| Bang: "P \<parallel> !P \<longmapsto>α \<prec> P' ==> !P \<longmapsto>α \<prec> P'"
equivariance semantics
nominal_inductive semantics
by(auto simp add: abs_fresh)
lemma semanticsInduct:
"[|R \<longmapsto>β \<prec> R'; !!α P \<C>. Prop \<C> (α.(P)) α P;
!!P α P' Q \<C>. [|P \<longmapsto>α \<prec> P'; !!\<C>. Prop \<C> P α P'|] ==> Prop \<C> (ccs.Sum P Q) α P';
!!Q α Q' P \<C>. [|Q \<longmapsto>α \<prec> Q'; !!\<C>. Prop \<C> Q α Q'|] ==> Prop \<C> (ccs.Sum P Q) α Q';
!!P α P' Q \<C>. [|P \<longmapsto>α \<prec> P'; !!\<C>. Prop \<C> P α P'|] ==> Prop \<C> (P \<parallel> Q) α (P' \<parallel> Q);
!!Q α Q' P \<C>. [|Q \<longmapsto>α \<prec> Q'; !!\<C>. Prop \<C> Q α Q'|] ==> Prop \<C> (P \<parallel> Q) α (P \<parallel> Q');
!!P a P' Q Q' \<C>.
[|P \<longmapsto>a \<prec> P'; !!\<C>. Prop \<C> P a P'; Q \<longmapsto>(coAction a) \<prec> Q';
!!\<C>. Prop \<C> Q (coAction a) Q'; a ≠ τ|]
==> Prop \<C> (P \<parallel> Q) (τ) (P' \<parallel> Q');
!!P α P' x \<C>.
[|x \<sharp> \<C>; P \<longmapsto>α \<prec> P'; !!\<C>. Prop \<C> P α P'; x \<sharp> α|] ==> Prop \<C> ((|νx|)),P) α ((|νx|)),P');
!!P α P' \<C>. [|P \<parallel> !P \<longmapsto>α \<prec> P'; !!\<C>. Prop \<C> (P \<parallel> !P) α P'|] ==> Prop \<C> !P α P'|]
==> Prop (\<C>::'a::fs_name) R β R'"
by(erule_tac z=\<C> in semantics.strong_induct) auto
lemma NilTrans[dest]:
shows "\<zero> \<longmapsto>α \<prec> P' ==> False"
and "((|b|)),).P \<longmapsto>⟨c⟩ \<prec> P' ==> False"
and "((|b|)),).P \<longmapsto>τ \<prec> P' ==> False"
and "(⟨b⟩).P \<longmapsto>(|c|)), \<prec> P' ==> False"
and "(⟨b⟩).P \<longmapsto>τ \<prec> P' ==> False"
apply(ind_cases "\<zero> \<longmapsto>α \<prec> P'")
apply(ind_cases "((|b|)),).P \<longmapsto>⟨c⟩ \<prec> P'", auto simp add: ccs.inject)
apply(ind_cases "((|b|)),).P \<longmapsto>τ \<prec> P'", auto simp add: ccs.inject)
apply(ind_cases "(⟨b⟩).P \<longmapsto>(|c|)), \<prec> P'", auto simp add: ccs.inject)
apply(ind_cases "(⟨b⟩).P \<longmapsto>τ \<prec> P'", auto simp add: ccs.inject)
done
lemma freshDerivative:
fixes P :: ccs
and a :: act
and P' :: ccs
and x :: name
assumes "P \<longmapsto>α \<prec> P'"
and "x \<sharp> P"
shows "x \<sharp> α" and "x \<sharp> 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) \<longmapsto>β \<prec> P'"
and "Prop α P"
shows "Prop β P'"
using assms
by - (ind_cases "α.(P) \<longmapsto>β \<prec> 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 \<longmapsto>α \<prec> R"
and "!!P'. P \<longmapsto>α \<prec> P' ==> Prop P'"
and "!!Q'. Q \<longmapsto>α \<prec> Q' ==> Prop Q'"
shows "Prop R"
using assms
by - (ind_cases "P ⊕ Q \<longmapsto>α \<prec> 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 \<parallel> Q \<longmapsto>α \<prec> R"
and "!!P'. P \<longmapsto>α \<prec> P' ==> Prop α (P' \<parallel> Q)"
and "!!Q'. Q \<longmapsto>α \<prec> Q' ==> Prop α (P \<parallel> Q')"
and "!!P' Q' a. [|P \<longmapsto>a \<prec> P'; Q \<longmapsto>(coAction a) \<prec> Q'; a ≠ τ; α = τ|] ==> Prop (τ) (P' \<parallel> Q')"
shows "Prop α R"
using assms
by - (ind_cases "P \<parallel> Q \<longmapsto>α \<prec> 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 \<longmapsto>α \<prec> P'"
and "!!P'. [|P \<longmapsto>α \<prec> P'; x \<sharp> α|] ==> Prop ((|νx|)),P')"
shows "Prop P'"
proof -
from `(|νx|)),P \<longmapsto>α \<prec> P'` have "x \<sharp> α" and "x \<sharp> 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 \<parallel> !P)"
lemma bangInduct[consumes 1, case_names cPar1 cPar2 cComm cBang]:
fixes P :: ccs
and α :: act
and P' :: ccs
and \<C> :: "'a::fs_name"
assumes "!P \<longmapsto>α \<prec> P'"
and rPar1: "!!α P' \<C>. [|P \<longmapsto>α \<prec> P'|] ==> Prop \<C> (P \<parallel> !P) α (P' \<parallel> !P)"
and rPar2: "!!α P' \<C>. [|!P \<longmapsto>α \<prec> P'; !!\<C>. Prop \<C> (!P) α P'|] ==> Prop \<C> (P \<parallel> !P) α (P \<parallel> P')"
and rComm: "!!a P' P'' \<C>. [|P \<longmapsto>a \<prec> P'; !P \<longmapsto>(coAction a) \<prec> P''; !!\<C>. Prop \<C> (!P) (coAction a) P''; a ≠ τ|] ==> Prop \<C> (P \<parallel> !P) (τ) (P' \<parallel> P'')"
and rBang: "!!α P' \<C>. [|P \<parallel> !P \<longmapsto>α \<prec> P'; !!\<C>. Prop \<C> (P \<parallel> !P) α P'|] ==> Prop \<C> (!P) α P'"
shows "Prop \<C> (!P) α P'"
proof -
{
fix X α P'
assume "X \<longmapsto>α \<prec> P'" and "bangPred P X"
hence "Prop \<C> X α P'"
proof(nominal_induct avoiding: \<C> 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 \<parallel> Q)", auto intro: rPar1 simp add: ccs.inject)
next
case(Par2 Q α P' Pa)
thus ?case
apply -
by(ind_cases "bangPred P (Pa \<parallel> 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 \<parallel> 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 \<longmapsto>α \<prec> 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 \<parallel> P, T \<parallel> 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 \<parallel> !Q) ∈ bangRel Rel"
and "!!P R. [|(P, Q) ∈ Rel; (R, !Q) ∈ bangRel Rel|] ==> F (P \<parallel> R)"
shows "F P"
using assms
by - (ind_cases "(P, Q \<parallel> !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