Quelle  Agent.thy

(* 
   Title: The pi-calculus   
   Author/Maintainer: Jesper Bengtson (jebe.dk), 2012
*)
theory Agent
  imports "HOL-Nominal.Nominal"
begin

lemma pt_id:
  fixes x :: 'a
    and a :: 'x

  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE('x)"
  shows "[(a, a)] ∙ x = x"
proof -
  have "x = ([]::'x prm) ∙ x"
    by(simp add: pt1[OF pt])
  also have "[(a, a)] ∙ x = ([]::'x prm) ∙ x"
    by(simp add: pt3[OF pt] at_ds1[OF at])
  finally show ?thesis by simp
qed

lemma pt_swap:
  fixes x :: 'a
  and a :: 'x
  and b :: 'x

  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE('x)"

  shows "[(a, b)] ∙ x = [(b, a)] ∙ x"
proof -
  show ?thesis by(simp add: pt3[OF pt] at_ds5[OF at])
qed

atom_decl name

lemmas name_fresh_abs = fresh_abs_fun_iff[OF pt_name_inst, OF at_name_inst, OF fs_name1]
lemmas name_bij = at_bij[OF at_name_inst]
lemmas name_supp_abs = abs_fun_supp[OF pt_name_inst, OF at_name_inst, OF fs_name1]
lemmas name_abs_eq = abs_fun_eq[OF pt_name_inst, OF at_name_inst]
lemmas name_supp = at_supp[OF at_name_inst]
lemmas name_calc = at_calc[OF at_name_inst]
lemmas name_fresh_fresh = pt_fresh_fresh[OF pt_name_inst, OF at_name_inst]
lemmas name_fresh_left = pt_fresh_left[OF pt_name_inst, OF at_name_inst]
lemmas name_fresh_right = pt_fresh_right[OF pt_name_inst, OF at_name_inst]
lemmas name_id[simp] = pt_id[OF pt_name_inst, OF at_name_inst]
lemmas name_swap_bij[simp] = pt_swap_bij[OF pt_name_inst, OF at_name_inst]
lemmas name_swap = pt_swap[OF pt_name_inst, OF at_name_inst]
lemmas name_rev_per = pt_rev_pi[OF pt_name_inst, OF at_name_inst]
lemmas name_per_rev = pt_pi_rev[OF pt_name_inst, OF at_name_inst]
lemmas name_exists_fresh = at_exists_fresh[OF at_name_inst, OF fs_name1]
lemmas name_perm_compose = pt_perm_compose[OF pt_name_inst, OF at_name_inst]

nominal_datatype pi = PiNil                  (‹0›)
                    | Output name name pi    (‹_{_}._› [120, 120, 110] 110)
                    | Tau pi                 (‹τ._› [120] 110)
                    | Input name "«name¬ pi" (‹_🪙._› [120, 120, 110] 110)
                    | Match name name pi     (‹[_⌢_]_› [120, 120, 110] 110)
                    | Mismatch name name pi  (‹[_≠_]_› [120, 120, 110] 110)
                    | Sum pi pi              (infixr ‹⊕› 90)
                    | Par pi pi              (infixr ‹∥› 85)
                    | Res "«name¬ pi"        (‹<\<nu>_>_› [100, 100] 100)
                    | Bang pi                (‹!_› [110] 110)

lemmas name_fresh[simp] = at_fresh[OF at_name_inst]

lemma alphaInput:
  fixes a :: name
  and   x :: name
  and   P :: pi
  and   c :: name

  assumes A1: "c ♯ P"

  shows "a<x>.P = a<c>.([(x, c)] ∙ P)"
proof(cases "x = c")
  assume "x=c"
  thus ?thesis by(simp)
next
  assume "x ≠ c"
  with A1 show ?thesis
    by(simp add: pi.inject alpha name_fresh_left name_calc)
qed

lemma alphaRes:
  fixes a :: name
  and   P :: pi
  and   c :: name
  
  assumes A1: "c ♯ P"

  shows "<νa>P = <νc>([(a, c)] ∙ P)"
proof(cases "a=c")
  assume "a=c"
  thus ?thesis by simp
next
  assume "a ≠ c"
  with A1 show ?thesis
    by(simp add: pi.inject alpha fresh_left name_calc)
qed

(*Substitution*)

definition subst_name :: "name ==> name ==> name ==> name"   (‹_[_::=_]› [110, 110, 110] 110)
where
  "a[b::=c] ≡ if (a = b) then c else a"

declare subst_name_def[simp]

lemma subst_name_eqvt[eqvt]:
  fixes p :: "name prm"
  and   a :: name
  and   b :: name
  and   c :: name

  shows "p ∙ (a[b::=c]) = (p∙ a)[(p ∙ b)::=(p ∙ c)]"
by(auto simp add: at_bij[OF at_name_inst])


nominal_primrec (freshness_context: "(c::name, d::name)")
  subs :: "pi ==> name ==> name ==> pi" (‹_[_::=_]› [100,100,100] 100)
where
  "0[c::=d] = 0"
| "τ.(P)[c::=d] = τ.(P[c::=d])"
| "a{b}.P[c::=d] = (a[c::=d]){(b[c::=d])}.(P[c::=d])"
| "[x ≠ a; x ≠ c; x ≠ d] ==> (a<x>.P)[c::=d] = (a[c::=d])<x>.(P[c::=d])"
| "[a⌢b]P[c::=d] = [(a[c::=d])⌢(b[c::=d])](P[c::=d])"
| "[a≠b]P[c::=d] = [(a[c::=d])≠(b[c::=d])](P[c::=d])"
| "(P ⊕ Q)[c::=d] = (P[c::=d]) ⊕ (Q[c::=d])"
| "(P ∥ Q)[c::=d] = (P[c::=d]) ∥ (Q[c::=d])"
| "[x ≠ c; x ≠ d] ==> (<νx>P)[c::=d] = <νx>(P[c::=d])"
| "!P[c::=d] = !(P[c::=d])"
apply(simp_all add: abs_fresh)
apply(finite_guess)+
by(fresh_guess)+

lemma forget:
  fixes a :: name
  and   P :: pi
  and   b :: name

  assumes "a ♯ P"

  shows "P[a::=b] = P"
using assms
by(nominal_induct P avoiding: a b rule: pi.strong_induct)
  (auto simp add: name_fresh_abs)

lemma fresh_fact2[rule_format]:
  fixes P :: pi
  and   a :: name
  and   b :: name

  assumes "a ≠ b"

  shows "a ♯ P[a::=b]"
using assms
by(nominal_induct P avoiding: a b rule: pi.strong_induct)
  (auto simp add: name_fresh_abs)

lemma subst_identity[simp]:
  fixes P :: pi
  and   a :: name

  shows "P[a::=a] = P"
by(nominal_induct P avoiding: a rule: pi.strong_induct) auto

lemma renaming:
  fixes P :: pi
  and   a :: name
  and   b :: name
  and   c :: name

  assumes "c ♯ P"

  shows "P[a::=b] = ([(c, a)] ∙ P)[c::=b]"
using assms
by(nominal_induct P avoiding: a b c rule: pi.strong_induct)
  (auto simp add: name_calc name_fresh_abs)


lemma fresh_fact1:
  fixes P :: pi
  and   a :: name
  and   b :: name
  and   c :: name

  assumes "a ♯ P"
  and     "a ≠ c"

  shows "a ♯ P[b::=c]"
using assms
by(nominal_induct P avoiding: a b c rule: pi.strong_induct)
  (auto simp add: name_fresh_abs)


lemma eqvt_subs[eqvt]:
  fixes p :: "name prm"
  and   P :: pi
  and   a :: name
  and   b :: name

  shows "p ∙ (P[a::=b]) = (p ∙ P)[(p ∙ a)::=(p ∙ b)]"
by(nominal_induct P avoiding: a b rule: pi.strong_induct)
  (auto simp add: name_bij)


lemma substInput[simp]:
  fixes x :: name
  and   b :: name
  and   c :: name
  and   a :: name
  and   P :: pi

  assumes "x ≠ b"
  and     "x ≠ c"

  shows "(a<x>.P)[b::=c] = (a[b::=c])<x>.(P[b::=c])"
proof -
  obtain y::name where"y ≠ a" and "y ♯ P" and "y ≠ b" and "y ≠ c"
    by(generate_fresh "name") (auto simp add: fresh_prod)
  from ‹y ♯ P› have "a<x>.P = a<y>.([(x, y)] ∙ P)" by(simp add: alphaInput)
  moreover have "(a[b::=c])<x>.(P[b::=c]) = (a[b::=c])<y>.(([(x, y)] ∙ P)[b::=c])" (is "?LHS = ?RHS")
  proof -
    from ‹y ♯ P› ‹y ≠ c› have "y ♯ P[b::=c]" by(rule fresh_fact1)
    hence "?LHS = (a[b::=c])<y>.([(x, y)] ∙ (P[b::=c]))" by(simp add: alphaInput)
    moreover with ‹x ≠ b› ‹x ≠ c› ‹y ≠ b› ‹y ≠ c› have "… = ?RHS"
      by(auto simp add: eqvt_subs name_calc)
    ultimately show ?thesis by simp
  qed
  ultimately show ?thesis using ‹y ≠ a› ‹y ≠ b› ‹y ≠ c› by simp
qed

lemma injPermSubst:
  fixes P :: pi
  and   a :: name
  and   b :: name

  assumes "b ♯ P"

  shows "[(a, b)] ∙ P = P[a::=b]"
using assms
by(nominal_induct P avoiding: a b rule: pi.strong_induct)
  (auto simp add: name_calc name_fresh_abs)

lemma substRes2:
  fixes P :: pi
  and   a :: name
  and   b :: name

  assumes "b ♯ P"

  shows "<νa>P = <νb>(P[a::=b])"
proof(case_tac "a = b")
  assume "a = b"
  thus ?thesis by auto
next
  assume "a ≠ b"
  moreover with ‹b ♯ P› show ?thesis
    apply(simp add: pi.inject abs_fun_eq[OF pt_name_inst, OF at_name_inst])
    apply auto
    apply(simp add: renaming)
    apply(simp add: pt_swap[OF pt_name_inst, OF at_name_inst])
    apply(simp add: renaming)
    apply(simp add: pt_fresh_left[OF pt_name_inst, OF at_name_inst])
    by(force simp add: at_calc[OF at_name_inst])
qed

lemma freshRes:
  fixes P :: pi
  and   a :: name
  
  shows "a ♯ <νa>P"
by(simp add: name_fresh_abs)

lemma substRes3: 
  fixes P :: pi
  and   a :: name
  and   b :: name

  assumes "b ♯ P"

  shows "(<νa>P)[a::=b] = <νb>(P[a::=b])"
proof -
  have "(<νa>P)[a::=b] = <νa>P"
    using freshRes by(simp add: forget)
  thus ?thesis using ‹b ♯ P› by(simp add: substRes2)
qed

lemma suppSubst:
  fixes P :: pi
  and   a :: name
  and   b :: name

  shows "supp(P[a::=b]) ⊆ insert b ((supp P) - {a})"
apply(nominal_induct P avoiding: a b rule: pi.strong_induct,
      simp_all add: pi.supp name_supp_abs name_supp supp_prod)
by(blast)+
  
(******** Sequential substitution *******)

primrec seqSubs :: "pi ==> (name × name) list ==> pi" (‹_[🪙]› [100,100] 100) where
  "P[<[]>] = P"
| "P[<(x#σ)>] = (P[(fst x)::=(snd x)])[<σ>]"

primrec seq_subst_name :: "name ==> (name × name) list ==> name" where
  "seq_subst_name a [] = a"
| "seq_subst_name a (x#σ) = seq_subst_name (a[(fst x)::=(snd x)]) σ"

lemma freshSeqSubstName:
  fixes x :: name
  and   a :: name
  and   s :: "(name × name) list"

  assumes "x ≠ a"
  and     "x ♯ s"

  shows "x ≠ seq_subst_name a s"
using assms
apply(induct s arbitrary: a)
apply simp
apply(case_tac "aa = fst(a)")
by (force simp add: fresh_list_cons fresh_prod)+


lemma seqSubstZero[simp]:
  fixes σ :: "(name × name) list"

  shows "0[<σ>] = 0"
by(induct σ, auto)

lemma seqSubstTau[simp]:
  fixes P :: pi
  and   σ :: "(name × name) list"

  shows "(τ.(P))[<σ>] = τ.(P[<σ>])"
by(induct σ arbitrary: P, auto)

lemma seqSubstOutput[simp]:
  fixes a :: name
  and   b :: name
  and   P :: pi
  and   σ :: "(name × name) list"
  
  shows "(a{b}.P)[<σ>] = (seq_subst_name a σ){(seq_subst_name b σ)}.(P[<σ>])"
by(induct σ arbitrary: a b P, auto)

lemma seqSubstInput[simp]:
  fixes a :: name
  and   x :: name
  and   P :: pi
  and   σ :: "(name × name) list"

  assumes "x ♯ σ"
 
  shows "(a<x>.P)[<σ>] = (seq_subst_name a σ)<x>.(P[<σ>])"
using assms
by(induct σ arbitrary: a x P) (auto simp add: fresh_list_cons fresh_prod)

lemma seqSubstMatch[simp]:
  fixes a :: name
  and   b :: name
  and   P :: pi
  and   σ :: "(name × name) list"

  shows "([a⌢b]P)[<σ>] = [(seq_subst_name a σ)⌢(seq_subst_name b σ)](P[<σ>])"
by(induct σ arbitrary: a b P, auto)

lemma seqSubstMismatch[simp]:
  fixes a :: name
  and   b :: name
  and   P :: pi
  and   σ :: "(name × name) list"

  shows "([a≠b]P)[<σ>] = [(seq_subst_name a σ)≠(seq_subst_name b σ)](P[<σ>])"
by(induct σ arbitrary: a b P, auto)

lemma seqSubstSum[simp]:
  fixes P :: pi
  and   Q :: pi
  and   σ :: "(name × name) list"

  shows "(P ⊕ Q)[<σ>] = (P[<σ>]) ⊕ (Q[<σ>])"
by(induct σ arbitrary: P Q , auto)

lemma seqSubstPar[simp]:
  fixes P :: pi
  and   Q :: pi
  and   σ :: "(name × name) list"

  shows "(P ∥ Q)[<σ>] = (P[<σ>]) ∥ (Q[<σ>])"
by(induct σ arbitrary: P Q, auto)

lemma seqSubstRes[simp]:
  fixes x :: name
  and   P :: pi
  and   σ :: "(name × name) list"

  assumes "x ♯ σ"

  shows "(<νx>P)[<σ>] = <νx>(P[<σ>])"
using assms
by(induct σ arbitrary: x P) (auto simp add: fresh_list_cons fresh_prod)

lemma seqSubstBang[simp]:
  fixes P :: pi
  and   s :: "(name × name) list"

  shows "(!P)[<σ>] = !(P[<σ>])"
by(induct σ arbitrary: P, auto)

lemma seqSubstEqvt[eqvt, simp]:
  fixes P :: pi
  and   σ :: "(name × name) list"
  and   p :: "name prm"

  shows "p ∙ (P[<σ>]) = (p ∙ P)[<(p ∙ σ)>]"
by(induct σ arbitrary: P, auto simp add: eqvt_subs)

lemma seqSubstAppend[simp]:
  fixes P  :: pi
  and   σ  :: "(name × name) list"
  and   σ' :: "(name × name) list"

  shows "P[<(σ@σ')>] = (P[<σ>])[<σ'>]"
by(induct σ arbitrary: P, auto)

lemma freshSubstChain[intro]:
  fixes P :: pi
  and   σ :: "(name × name) list"
  and   a :: name

  assumes "a ♯ P"
  and     "a ♯ σ"

  shows "a ♯ P[<σ>]"
using assms
by(induct σ arbitrary: a P, auto simp add: fresh_list_cons fresh_prod fresh_fact1)

end