(* 
   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           (‹0› 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 C. Prop C (α.(P)) α P;
 ∧P α P' Q C. [P ⟼α ≺ P'; ∧C. Prop C P α P'] ==> Prop C (ccs.Sum P Q) α P';
 ∧Q α Q' P C. [Q ⟼α ≺ Q'; ∧C. Prop C Q α Q'] ==> Prop C (ccs.Sum P Q) α Q';
 ∧P α P' Q C. [P ⟼α ≺ P'; ∧C. Prop C P α P'] ==> Prop C (P ∥ Q) α (P' ∥ Q);
 ∧Q α Q' P C. [Q ⟼α ≺ Q'; ∧C. Prop C Q α Q'] ==> Prop C (P ∥ Q) α (P ∥ Q');
 ∧P a P' Q Q' C.
    [P ⟼a ≺ P'; ∧C. Prop C P a P'; Q ⟼(coAction a) ≺ Q';
     ∧C. Prop C Q (coAction a) Q'; a ≠ τ]
    ==> Prop C (P ∥ Q) (τ) (P' ∥ Q');
 ∧P α P' x C.
    [x ♯ C; P ⟼α ≺ P'; ∧C. Prop C P α P'; x ♯ α] ==> Prop C ((νx)P) α ((νx)P');
 ∧P α P' C. [P ∥ !P ⟼α ≺ P'; ∧C. Prop C (P ∥ !P) α P'] ==> Prop C !P α P']

\<Longrightarrow> Prop (C::'a::fs_name) R β R'"
by(erule_tac z=C in semantics.strong_induct) auto

lemma NilTrans[dest]:
  shows "0 ⟼α ≺ 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 "0 ⟼α ≺ 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   C  :: "'a::fs_name"

  assumes "!P ⟼α ≺ P'"
  and     rPar1: "∧α P' C. [P ⟼α ≺ P'] ==> Prop C (P ∥ !P) α (P' ∥ !P)"
  and     rPar2: "∧α P' C. [!P ⟼α ≺ P'; ∧C. Prop C (!P) α P'] ==> Prop C (P ∥ !P) α (P ∥ P')"
  and     rComm: "∧a P' P'' C. [P ⟼a ≺ P'; !P ⟼(coAction a) ≺ P''; ∧C. Prop C (!P) (coAction a) P''; a ≠ τ] ==> Prop C (P ∥ !P) (τ) (P' ∥ P'')"
  and     rBang: "∧α P' C. [P ∥ !P ⟼α ≺ P'; ∧C. Prop C (P ∥ !P) α P'] ==> Prop C (!P) α P'"


  shows "Prop C (!P) α P'"
proof -
  {
    fix X α P'
    assume "X ⟼α ≺ 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 ∥ 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