Theory ProcessCalculi

theory ProcessCalculi
  imports Relations
begin

section ‹Process Calculi›

text ‹A process calculus is given by a set of process terms (syntax) and a relation on terms
        (semantics). We consider reduction as well as labelled variants of the semantics.›

subsection ‹Reduction Semantics›

text ‹A set of process terms and a relation on pairs of terms (called reduction semantics) define
        a process calculus.›

record 'proc processCalculus =
  Reductions :: "'proc ⇒ 'proc ⇒ bool"

text ‹A pair of the reduction relation is called a (reduction) step.›

abbreviation step :: "'proc ⇒ 'proc processCalculus ⇒ 'proc ⇒ bool"
    ("_ ⟼_ _" [70, 70, 70] 80)
  where
  "P ⟼Cal Q ≡ Reductions Cal P Q"

text ‹We use * to indicate the reflexive and transitive closure of the reduction relation.›

primrec nSteps
  :: "'proc ⇒ 'proc processCalculus ⇒ nat ⇒ 'proc ⇒ bool"
    ("_ ⟼_⇗_⇖ _" [70, 70, 70, 70] 80)
  where
  "P ⟼Cal⇗0⇖ Q     = (P = Q)" |
  "P ⟼Cal⇗Suc n⇖ Q = (∃P'. P ⟼Cal⇗n⇖ P' ∧ P' ⟼Cal Q)"

definition steps
  :: "'proc ⇒ 'proc processCalculus ⇒ 'proc ⇒ bool"
    ("_ ⟼_* _" [70, 70, 70] 80)
  where
  "P ⟼Cal* Q ≡ ∃n. P ⟼Cal⇗n⇖ Q"

text ‹A process is divergent, if it can perform an infinite sequence of steps.›

definition divergent
  :: "'proc ⇒ 'proc processCalculus ⇒ bool"
    ("_ ⟼_ω" [70, 70] 80)
  where
  "P ⟼(Cal)ω ≡ ∀P'. P ⟼Cal* P' ⟶ (∃P''. P' ⟼Cal P'')"

text ‹Each term can perform an (empty) sequence of steps to itself.›

lemma steps_refl:
  fixes Cal :: "'proc processCalculus"
    and P   :: "'proc"
  shows "P ⟼Cal* P"
proof -
  have "P ⟼Cal⇗0⇖ P"
    by simp
  hence "∃n. P ⟼Cal⇗n⇖ P"
    by blast
  thus "P ⟼Cal* P"
    by (simp add: steps_def)
qed

text ‹A single step is a sequence of steps of length one.›

lemma step_to_steps:
  fixes Cal  :: "'proc processCalculus"
    and P P' :: "'proc"
  assumes step: "P ⟼Cal P'"
  shows "P ⟼Cal* P'"
proof -
  from step have "P ⟼Cal⇗1⇖ P'"
    by simp
  thus ?thesis
    unfolding steps_def
    by blast
qed

text ‹If there is a sequence of steps from P to Q and from Q to R, then there is also a sequence
        of steps from P to R.›

lemma nSteps_add:
  fixes Cal   :: "'proc processCalculus"
    and n1 n2 :: "nat"
  shows "∀P Q R. P ⟼Cal⇗n1⇖ Q ∧ Q ⟼Cal⇗n2⇖ R ⟶ P ⟼Cal⇗(n1 + n2)⇖ R"
proof (induct n2, simp)
  case (Suc n)
  assume IH: "∀P Q R. P ⟼Cal⇗n1⇖ Q ∧ Q ⟼Cal⇗n⇖ R ⟶ P ⟼Cal⇗(n1 + n)⇖ R"
  show ?case
  proof clarify
    fix P Q R
    assume "Q ⟼Cal⇗Suc n⇖ R"
    from this obtain Q' where A1: "Q ⟼Cal⇗n⇖ Q'" and A2: "Q' ⟼Cal R"
      by auto
    assume "P ⟼Cal⇗n1⇖ Q"
    with A1 IH have "P ⟼Cal⇗(n1 + n)⇖ Q'"
      by blast
    with A2 show "P ⟼Cal⇗(n1 + Suc n)⇖ R"
      by auto
  qed
qed

lemma steps_add:
  fixes Cal   :: "'proc processCalculus"
    and P Q R :: "'proc"
  assumes A1: "P ⟼Cal* Q"
      and A2: "Q ⟼Cal* R"
  shows "P ⟼Cal* R"
proof -
  from A1 obtain n1 where "P ⟼Cal⇗n1⇖ Q"
    by (auto simp add: steps_def)
  moreover from A2 obtain n2 where "Q ⟼Cal⇗n2⇖ R"
    by (auto simp add: steps_def)
  ultimately have "P ⟼Cal⇗(n1 + n2)⇖ R"
    using nSteps_add[where Cal="Cal"]
    by blast
  thus "P ⟼Cal* R"
    by (simp add: steps_def, blast)
qed

subsubsection ‹Observables or Barbs›

text ‹We assume a predicate that tests terms for some kind of observables. At this point we do
        not limit or restrict the kind of observables used for a calculus nor the method to check
        them.›

record ('proc, 'barbs) calculusWithBarbs =
  Calculus :: "'proc processCalculus"
  HasBarb  :: "'proc ⇒ 'barbs ⇒ bool" ("_↓_" [70, 70] 80)

abbreviation hasBarb
  :: "'proc ⇒ ('proc, 'barbs) calculusWithBarbs ⇒ 'barbs ⇒ bool"
    ("_↓<_>_" [70, 70, 70] 80)
  where
  "P↓<CWB>a ≡ HasBarb CWB P a"

text ‹A term reaches a barb if it can evolve to a term that has this barb.›

abbreviation reachesBarb
  :: "'proc ⇒ ('proc, 'barbs) calculusWithBarbs ⇒ 'barbs ⇒ bool"
    ("_⇓<_>_" [70, 70, 70] 80)
  where
  "P⇓<CWB>a ≡ ∃P'. P ⟼(Calculus CWB)* P' ∧ P'↓<CWB>a"

text ‹A relation R preserves barbs if whenever (P, Q) in R and P has a barb then also Q has this
        barb.›

abbreviation rel_preserves_barb_set
    :: "('proc × 'proc) set ⇒ ('proc, 'barbs) calculusWithBarbs ⇒ 'barbs set ⇒ bool"
  where
  "rel_preserves_barb_set Rel CWB Barbs ≡
   rel_preserves_binary_pred Rel (λP a. a ∈ Barbs ∧ P↓<CWB>a)"

abbreviation rel_preserves_barbs
    :: "('proc × 'proc) set ⇒ ('proc, 'barbs) calculusWithBarbs ⇒ bool"
  where
  "rel_preserves_barbs Rel CWB ≡ rel_preserves_binary_pred Rel (HasBarb CWB)"

lemma preservation_of_barbs_and_set_of_barbs:
  fixes Rel :: "('proc × 'proc) set"
    and CWB :: "('proc, 'barbs) calculusWithBarbs"
  shows "rel_preserves_barbs Rel CWB = (∀Barbs. rel_preserves_barb_set Rel CWB Barbs)"
    by blast

text ‹A relation R reflects barbs if whenever (P, Q) in R and Q has a barb then also P has this
        barb.›

abbreviation rel_reflects_barb_set
    :: "('proc × 'proc) set ⇒ ('proc, 'barbs) calculusWithBarbs ⇒ 'barbs set ⇒ bool"
  where
  "rel_reflects_barb_set Rel CWB Barbs ≡
   rel_reflects_binary_pred Rel (λP a. a ∈ Barbs ∧ P↓<CWB>a)"

abbreviation rel_reflects_barbs
    :: "('proc × 'proc) set ⇒ ('proc, 'barbs) calculusWithBarbs ⇒ bool"
  where
  "rel_reflects_barbs Rel CWB ≡ rel_reflects_binary_pred Rel (HasBarb CWB)"

lemma reflection_of_barbs_and_set_of_barbs:
  fixes Rel :: "('proc × 'proc) set"
    and CWB :: "('proc, 'barbs) calculusWithBarbs"
  shows "rel_reflects_barbs Rel CWB = (∀Barbs. rel_reflects_barb_set Rel CWB Barbs)"
    by blast

text ‹A relation respects barbs if it preserves and reflects barbs.›

abbreviation rel_respects_barb_set
    :: "('proc × 'proc) set ⇒ ('proc, 'barbs) calculusWithBarbs ⇒ 'barbs set ⇒ bool"
  where
  "rel_respects_barb_set Rel CWB Barbs ≡
   rel_preserves_barb_set Rel CWB Barbs ∧ rel_reflects_barb_set Rel CWB Barbs"

abbreviation rel_respects_barbs
    :: "('proc × 'proc) set ⇒ ('proc, 'barbs) calculusWithBarbs ⇒ bool"
  where
  "rel_respects_barbs Rel CWB ≡ rel_preserves_barbs Rel CWB ∧ rel_reflects_barbs Rel CWB"

lemma respection_of_barbs_and_set_of_barbs:
  fixes Rel :: "('proc × 'proc) set"
    and CWB :: "('proc, 'barbs) calculusWithBarbs"
  shows "rel_respects_barbs Rel CWB = (∀Barbs. rel_respects_barb_set Rel CWB Barbs)"
    by blast

text ‹If a relation preserves barbs then so does its reflexive or/and transitive closure.›

lemma preservation_of_barbs_and_closures:
  fixes Rel :: "('proc × 'proc) set"
    and CWB :: "('proc, 'barbs) calculusWithBarbs"
  assumes preservation: "rel_preserves_barbs Rel CWB"
  shows "rel_preserves_barbs (Rel⇧=) CWB"
    and "rel_preserves_barbs (Rel⇧+) CWB"
    and "rel_preserves_barbs (Rel⇧*) CWB"
      using preservation
            preservation_of_binary_predicates_and_closures[where Rel="Rel" and Pred="HasBarb CWB"]
    by blast+

text ‹If a relation reflects barbs then so does its reflexive or/and transitive closure.›

lemma reflection_of_barbs_and_closures:
  fixes Rel :: "('proc × 'proc) set"
    and CWB :: "('proc, 'barbs) calculusWithBarbs"
  assumes reflection: "rel_reflects_barbs Rel CWB"
  shows "rel_reflects_barbs (Rel⇧=) CWB"
    and "rel_reflects_barbs (Rel⇧+) CWB"
    and "rel_reflects_barbs (Rel⇧*) CWB"
      using reflection
            reflection_of_binary_predicates_and_closures[where Rel="Rel" and Pred="HasBarb CWB"]
    by blast+

text ‹If a relation respects barbs then so does its reflexive, symmetric, or/and transitive
        closure.›

lemma respection_of_barbs_and_closures:
  fixes Rel :: "('proc × 'proc) set"
    and CWB :: "('proc, 'barbs) calculusWithBarbs"
  assumes respection: "rel_respects_barbs Rel CWB"
  shows "rel_respects_barbs (Rel⇧=) CWB"
    and "rel_respects_barbs (symcl Rel) CWB"
    and "rel_respects_barbs (Rel⇧+) CWB"
    and "rel_respects_barbs (symcl (Rel⇧=)) CWB"
    and "rel_respects_barbs (Rel⇧*) CWB"
    and "rel_respects_barbs ((symcl (Rel⇧=))⇧+) CWB"
proof -
  from respection show "rel_respects_barbs (Rel⇧=) CWB"
      using respection_of_binary_predicates_and_closures(1)[where Rel="Rel" and Pred="HasBarb CWB"]
    by blast
next
  from respection show "rel_respects_barbs (symcl Rel) CWB"
      using respection_of_binary_predicates_and_closures(2)[where Rel="Rel" and Pred="HasBarb CWB"]
    by blast
next
  from respection show "rel_respects_barbs (Rel⇧+) CWB"
      using respection_of_binary_predicates_and_closures(3)[where Rel="Rel" and Pred="HasBarb CWB"]
    by blast
next
  from respection show "rel_respects_barbs (symcl (Rel⇧=)) CWB"
      using respection_of_binary_predicates_and_closures(4)[where Rel="Rel" and Pred="HasBarb CWB"]
    by blast
next
  from respection show "rel_respects_barbs (Rel⇧*) CWB"
      using respection_of_binary_predicates_and_closures(5)[where Rel="Rel" and Pred="HasBarb CWB"]
    by blast
next
  from respection show "rel_respects_barbs ((symcl (Rel⇧=))⇧+) CWB"
      using respection_of_binary_predicates_and_closures(6)[where Rel="Rel" and Pred="HasBarb CWB"]
    by blast
qed

text ‹A relation R weakly preserves barbs if it preserves reachability of barbs, i.e., if (P, Q)
        in R and P reaches a barb then also Q has to reach this barb.›

abbreviation rel_weakly_preserves_barb_set
    :: "('proc × 'proc) set ⇒ ('proc, 'barbs) calculusWithBarbs ⇒ 'barbs set ⇒ bool"
  where
  "rel_weakly_preserves_barb_set Rel CWB Barbs ≡
   rel_preserves_binary_pred Rel (λP a. a ∈ Barbs ∧ P⇓<CWB>a)"

abbreviation rel_weakly_preserves_barbs
    :: "('proc × 'proc) set ⇒ ('proc, 'barbs) calculusWithBarbs ⇒ bool"
  where
  "rel_weakly_preserves_barbs Rel CWB ≡ rel_preserves_binary_pred Rel (λP a. P⇓<CWB>a)"

lemma weak_preservation_of_barbs_and_set_of_barbs:
  fixes Rel :: "('proc × 'proc) set"
    and CWB :: "('proc, 'barbs) calculusWithBarbs"
  shows "rel_weakly_preserves_barbs Rel CWB
         = (∀Barbs. rel_weakly_preserves_barb_set Rel CWB Barbs)"
    by blast

text ‹A relation R weakly reflects barbs if it reflects reachability of barbs, i.e., if (P, Q) in
        R and Q reaches a barb then also P has to reach this barb.›

abbreviation rel_weakly_reflects_barb_set
    :: "('proc × 'proc) set ⇒ ('proc, 'barbs) calculusWithBarbs ⇒ 'barbs set ⇒ bool"
  where
  "rel_weakly_reflects_barb_set Rel CWB Barbs ≡
   rel_reflects_binary_pred Rel (λP a. a ∈ Barbs ∧ P⇓<CWB>a)"

abbreviation rel_weakly_reflects_barbs
    :: "('proc × 'proc) set ⇒ ('proc, 'barbs) calculusWithBarbs ⇒ bool"
  where
  "rel_weakly_reflects_barbs Rel CWB ≡ rel_reflects_binary_pred Rel (λP a. P⇓<CWB>a)"

lemma weak_reflection_of_barbs_and_set_of_barbs:
  fixes Rel :: "('proc × 'proc) set"
    and CWB :: "('proc, 'barbs) calculusWithBarbs"
  shows "rel_weakly_reflects_barbs Rel CWB = (∀Barbs. rel_weakly_reflects_barb_set Rel CWB Barbs)"
    by blast

text ‹A relation weakly respects barbs if it weakly preserves and weakly reflects barbs.›

abbreviation rel_weakly_respects_barb_set
    :: "('proc × 'proc) set ⇒ ('proc, 'barbs) calculusWithBarbs ⇒ 'barbs set ⇒ bool"
  where
  "rel_weakly_respects_barb_set Rel CWB Barbs ≡
   rel_weakly_preserves_barb_set Rel CWB Barbs ∧ rel_weakly_reflects_barb_set Rel CWB Barbs"

abbreviation rel_weakly_respects_barbs
    :: "('proc × 'proc) set ⇒ ('proc, 'barbs) calculusWithBarbs ⇒ bool"
  where
  "rel_weakly_respects_barbs Rel CWB ≡
   rel_weakly_preserves_barbs Rel CWB ∧ rel_weakly_reflects_barbs Rel CWB"

lemma weak_respection_of_barbs_and_set_of_barbs:
  fixes Rel :: "('proc × 'proc) set"
    and CWB :: "('proc, 'barbs) calculusWithBarbs"
  shows "rel_weakly_respects_barbs Rel CWB = (∀Barbs. rel_weakly_respects_barb_set Rel CWB Barbs)"
    by blast

text ‹If a relation weakly preserves barbs then so does its reflexive or/and transitive closure.
›

lemma weak_preservation_of_barbs_and_closures:
  fixes Rel :: "('proc × 'proc) set"
    and CWB :: "('proc, 'barbs) calculusWithBarbs"
  assumes preservation: "rel_weakly_preserves_barbs Rel CWB"
  shows "rel_weakly_preserves_barbs (Rel⇧=) CWB"
    and "rel_weakly_preserves_barbs (Rel⇧+) CWB"
    and "rel_weakly_preserves_barbs (Rel⇧*) CWB"
      using preservation preservation_of_binary_predicates_and_closures[where Rel="Rel"
                          and Pred="λP a. P⇓<CWB>a"]
    by blast+

text ‹If a relation weakly reflects barbs then so does its reflexive or/and transitive closure.
›

lemma weak_reflection_of_barbs_and_closures:
  fixes Rel :: "('proc × 'proc) set"
    and CWB :: "('proc, 'barbs) calculusWithBarbs"
  assumes reflection: "rel_weakly_reflects_barbs Rel CWB"
  shows "rel_weakly_reflects_barbs (Rel⇧=) CWB"
    and "rel_weakly_reflects_barbs (Rel⇧+) CWB"
    and "rel_weakly_reflects_barbs (Rel⇧*) CWB"
      using reflection reflection_of_binary_predicates_and_closures[where Rel="Rel"
                        and Pred="λP a. P⇓<CWB>a"]
    by blast+

text ‹If a relation weakly respects barbs then so does its reflexive, symmetric, or/and
        transitive closure.›

lemma weak_respection_of_barbs_and_closures:
  fixes Rel :: "('proc × 'proc) set"
    and CWB :: "('proc, 'barbs) calculusWithBarbs"
  assumes respection: "rel_weakly_respects_barbs Rel CWB"
  shows "rel_weakly_respects_barbs (Rel⇧=) CWB"
    and "rel_weakly_respects_barbs (symcl Rel) CWB"
    and "rel_weakly_respects_barbs (Rel⇧+) CWB"
    and "rel_weakly_respects_barbs (symcl (Rel⇧=)) CWB"
    and "rel_weakly_respects_barbs (Rel⇧*) CWB"
    and "rel_weakly_respects_barbs ((symcl (Rel⇧=))⇧+) CWB"
proof -
  from respection show "rel_weakly_respects_barbs (Rel⇧=) CWB"
      using respection_of_binary_predicates_and_closures(1)[where Rel="Rel"
              and Pred="λP a. P⇓<CWB>a"]
    by blast
next
  from respection show "rel_weakly_respects_barbs (symcl Rel) CWB"
      using respection_of_binary_predicates_and_closures(2)[where Rel="Rel"
              and Pred="λP a. P⇓<CWB>a"]
    by blast
next
  from respection show "rel_weakly_respects_barbs (Rel⇧+) CWB"
      using respection_of_binary_predicates_and_closures(3)[where Rel="Rel"
              and Pred="λP a. P⇓<CWB>a"]
    by blast
next
  from respection show "rel_weakly_respects_barbs (symcl (Rel⇧=)) CWB"
      using respection_of_binary_predicates_and_closures(4)[where Rel="Rel"
              and Pred="λP a. P⇓<CWB>a"]
    by blast
next
  from respection show "rel_weakly_respects_barbs (Rel⇧*) CWB"
      using respection_of_binary_predicates_and_closures(5)[where Rel="Rel"
              and Pred="λP a. P⇓<CWB>a"]
    by blast
next
  from respection show "rel_weakly_respects_barbs ((symcl (Rel⇧=))⇧+) CWB"
      using respection_of_binary_predicates_and_closures(6)[where Rel="Rel"
              and Pred="λP a. P⇓<CWB>a"]
    by blast
qed

end