Theory Rel

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

definition eqvt :: "(('a::pt_name) × ('a::pt_name)) set ⇒ bool"
  where "eqvt Rel ≡ (∀x (perm::name prm). x ∈ Rel ⟶ perm ∙ x ∈ Rel)"

lemma eqvtRelI:
  fixes Rel  :: "('a::pt_name × 'a) set"
  and   P    :: 'a
  and   Q    :: 'a
  and   perm :: "name prm"

  assumes "eqvt Rel"
  and     "(P, Q) ∈ Rel"

  shows "(perm ∙ P, perm ∙ Q) ∈ Rel"
using assms
by(auto simp add: eqvt_def)

lemma eqvtRelE:
  fixes Rel  :: "('a::pt_name × 'a) set"
  and   P    :: 'a
  and   Q    :: 'a
  and   perm :: "name prm"

  assumes "eqvt Rel"
  and     "(perm ∙ P, perm ∙ Q) ∈ Rel"

  shows "(P, Q) ∈ Rel"
proof -
  have "rev perm ∙ (perm ∙ P) = P" and "rev perm ∙ (perm ∙ Q) = Q"
    by(simp add: pt_rev_pi[OF pt_name_inst, OF at_name_inst])+
  with assms show ?thesis
    by(force dest: eqvtRelI[of _ _ _ "rev perm"])
qed

lemma eqvtTrans[intro]:
  fixes Rel  :: "('a::pt_name × 'a) set"
  and   Rel' :: "('a × 'a) set"

  assumes EqvtRel:  "eqvt Rel"
  and     EqvtRel': "eqvt Rel'"

  shows "eqvt (Rel O Rel')"
using assms
by(force simp add: eqvt_def)

lemma eqvtUnion[intro]:
  fixes Rel  :: "('a::pt_name × 'a) set"
  and   Rel' :: "('a × 'a) set"

  assumes EqvtRel:  "eqvt Rel"
  and     EqvtRel': "eqvt Rel'"

  shows "eqvt (Rel ∪ Rel')"
using assms
by(force simp add: eqvt_def)

definition substClosed :: "(pi × pi) set ⇒ (pi × pi) set" where
  "substClosed Rel ≡ {(P, Q) | P Q. ∀σ. (P[<σ>], Q[<σ>]) ∈ Rel}"

lemma eqvtSubstClosed:
  fixes Rel :: "(pi × pi) set"

  assumes eqvtRel: "eqvt Rel"

  shows "eqvt (substClosed Rel)"
proof(simp add: eqvt_def substClosed_def, auto)
  fix P Q perm s

  assume "∀s. (P[<s>], Q[<s>]) ∈ Rel"
  hence "(P[<(rev (perm::name prm) ∙ s)>], Q[<(rev perm ∙ s)>]) ∈ Rel" by simp
  with eqvtRel have "(perm ∙ (P[<(rev perm ∙ s)>]), perm ∙ (Q[<(rev perm ∙ s)>])) ∈ Rel"
    by(rule eqvtRelI)
  thus "((perm ∙ P)[<s>], (perm ∙ Q)[<s>]) ∈ Rel"
    by(simp add: name_per_rev)
qed

lemma substClosedSubset:
  fixes Rel  :: "(pi × pi) set"

  shows "substClosed Rel ⊆ Rel"
proof(auto simp add: substClosed_def)
  fix P Q
  assume "∀s. (P[<s>], Q[<s>]) ∈ Rel"
  hence "(P[<[]>], Q[<[]>]) ∈ Rel" by blast
  thus "(P, Q) ∈ Rel" by simp
qed

lemma partUnfold:
  fixes P   :: pi
  and   Q   :: pi
  and   σ   :: "(name × name) list"
  and   Rel :: "(pi × pi) set"

  assumes "(P, Q) ∈ substClosed Rel"

  shows "(P[<σ>], Q[<σ>]) ∈ substClosed Rel"
using assms
proof(auto simp add: substClosed_def)
  fix σ'
  assume "∀σ. (P[<σ>], Q[<σ>]) ∈ Rel"
  hence "(P[<(σ@σ')>], Q[<(σ@σ')>]) ∈ Rel" by blast
  thus "((P[<σ>])[<σ'>], (Q[<σ>])[<σ'>]) ∈ Rel"
    by simp
qed

inductive_set bangRel :: "(pi × pi) set ⇒ (pi × pi) set"
for Rel :: "(pi × pi) set"
where
  BRBang: "(P, Q) ∈ Rel ⟹ (!P, !Q) ∈ bangRel Rel"
| BRPar: "(R, T) ∈ Rel ⟹ (P, Q) ∈ (bangRel Rel) ⟹ (R ∥ P, T ∥ Q) ∈ (bangRel Rel)"
| BRRes: "(P, Q) ∈ bangRel Rel ⟹ (<νa>P, <νa>Q) ∈ bangRel Rel"

inductive_cases BRBangCases': "(P, !Q) ∈ bangRel Rel"
inductive_cases BRParCases': "(P, Q ∥ !Q) ∈ bangRel Rel"
inductive_cases BRResCases': "(P, <νx>Q) ∈ bangRel Rel"

lemma eqvtBangRel:
  fixes Rel :: "(pi × pi) set"

  assumes eqvtRel: "eqvt Rel"

  shows "eqvt(bangRel Rel)"
proof(simp add: eqvt_def, auto)
  fix P Q perm
  assume "(P, Q) ∈ bangRel Rel"
  thus "((perm::name prm) ∙ P, perm ∙ Q) ∈ bangRel Rel"
  proof(induct)
    fix P Q
    assume "(P, Q) ∈ Rel"
    with eqvtRel have "(perm ∙ P, perm ∙ Q) ∈ Rel"
      by(rule eqvtRelI)
    thus "(perm ∙ !P, perm ∙ !Q) ∈ bangRel Rel"
      by(force intro: BRBang)
  next
    fix P Q R T
    assume R: "(R, T) ∈ Rel"
    assume BR: "(perm ∙ P, perm ∙ Q) ∈ bangRel Rel"

    from eqvtRel R have "(perm ∙ R, perm ∙ T) ∈ Rel"
      by(rule eqvtRelI)

    with BR show "(perm ∙ (R ∥ P), perm ∙ (T ∥ Q)) ∈ bangRel Rel"
      by(force intro: BRPar)
  next
    fix P Q a
    assume "(perm ∙ P, perm ∙ Q) ∈ bangRel Rel"
    thus "(perm ∙ <νa>P, perm ∙ <νa>Q) ∈ bangRel Rel"
      by(force intro: BRRes)
  qed
qed

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

  assumes "(P, !Q) ∈ bangRel Rel"
  and     "⋀P. (P, Q) ∈ Rel ⟹ F (!P)"
  
  shows "F P"
using assms
by(induct rule: BRBangCases', auto simp add: pi.inject)

lemma BRParCases[consumes 1, case_names BRPar]:
  fixes P   :: pi
  and   Q   :: pi
  and   Rel :: "(pi × pi) set"
  and   F   :: "pi ⇒ 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(induct rule: BRParCases', auto simp add: pi.inject)

lemma bangRelSubset:
  fixes Rel  :: "(pi × pi) set"
  and   Rel' :: "(pi × pi) 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 BRRes)

lemma bangRelSymetric: 
  fixes P   :: pi
  and   Q   :: pi
  and   Rel :: "(pi × pi) set"

  assumes A:   "(P, Q) ∈ bangRel Rel"
  and     Sym: "⋀P Q. (P, Q) ∈ Rel ⟹ (Q, P) ∈ Rel"

  shows "(Q, P) ∈ bangRel Rel"
proof -
  from A show ?thesis
  proof(induct)
    fix P Q
    assume "(P, Q) ∈ Rel"
    hence "(Q, P) ∈ Rel" by(rule Sym)
    thus "(!Q, !P) ∈ bangRel Rel" by(rule BRBang)
  next
    fix P Q R T
    assume RRelT: "(R, T) ∈ Rel"
    assume IH: "(Q, P) ∈ bangRel Rel"
    from RRelT have "(T, R) ∈ Rel" by(rule Sym)
    thus "(T ∥ Q, R ∥ P) ∈ bangRel Rel" using IH by(rule BRPar)
  next
    fix P Q a
    assume "(Q, P) ∈ bangRel Rel"
    thus "(<νa>Q, <νa>P) ∈ bangRel Rel" by(rule BRRes)
  qed
qed

primrec resChain :: "name list ⇒ pi ⇒ pi" where
   base: "resChain [] P = P"
 | step: "resChain (x#xs) P = <νx>(resChain xs P)"

lemma resChainPerm[simp]:
  fixes perm :: "name prm"
  and   lst  :: "name list"
  and   P    :: pi
  
  shows "perm ∙ (resChain lst P) = resChain (perm ∙ lst) (perm ∙ P)"
by(induct_tac lst, auto)

lemma resChainFresh:
  fixes a   :: name
  and   lst :: "name list"
  and   P   :: pi

  assumes "a ♯ (lst, P)"

  shows "a ♯ (resChain lst P)"
using assms apply(induct_tac lst)
apply(simp add: fresh_prod)
by(simp add: fresh_prod name_fresh_abs)

end