Theory ProcessCalculi

(* Kirstin Peters, TU Berlin, 2015 *)

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

(* Kirstin Peters, University of Augsburg, 2026 *)

subsection ‹Labelled Semantics›

text ‹Alternatively, a process calculus is defined by a set of process terms and a relation on a
      term, a label, and a term (called labelled semantics). Moreover, we assume that in this case
      there exists a special label to denote an internal action.›

record ('proc, 'lab) labelledProcessCalculus =
  LabelledSemantics :: "'proc ⇒ 'lab ⇒ 'proc ⇒ bool"
  InternalAction    :: "'lab"

text ‹A triple of the labelled semantics is called a labelled step. To avoid confusion we disable
      some syntactic sugar for Limes in Topological Spaces.›

no_notation Topological_Spaces.LIM (‹(‹notation=‹infix LIM››(_)/ ─(_)/→ (_))› [60, 0, 60] 60)

abbreviation labelledStep
  :: "'proc ⇒ 'lab ⇒ ('proc, 'lab) labelledProcessCalculus ⇒ 'proc ⇒ bool"
  (‹_ ─_→_ _› [70, 70, 70, 70] 80) where
  "P ─α→Cal Q ≡ LabelledSemantics Cal P α Q"

text ‹The internal action is denoted by tau, where we add the respective calculus, since different
      calculi may have a different internal action label.›

abbreviation internal :: "('proc, 'lab) labelledProcessCalculus ⇒ 'lab"  (‹τ-_› [70] 90) where
  "τ-Cal ≡ InternalAction Cal"

text ‹A weak internal step is the reflexive and transitive closure of a labelled step on the
      internal action label.›

inductive weakTauStep :: "'proc ⇒ ('proc, 'lab) labelledProcessCalculus ⇒ 'proc ⇒ bool"
  (‹_ →_* _› [70, 70, 70] 80) where
  WTS_refl:  "P →Cal* P"
| WTS_trans: "⟦P →Cal* Q; Q ─τ-Cal→Cal R⟧ ⟹ P →Cal* R"

lemma weakTauStep_decompose:
  fixes P Q :: "'proc"
    and Cal :: "('proc, 'lab) labelledProcessCalculus"
  assumes "P →Cal* Q"
  shows "P = Q ∨ (∃R. P →Cal* R ∧ R ─τ-Cal→Cal Q)"
  using assms
  by (induct, auto)

lemma weakTauSteps_trans:
  fixes P Q R :: "'proc"
    and Cal   :: "('proc, 'lab) labelledProcessCalculus"
  assumes "P →Cal* Q"
      and "Q →Cal* R"
    shows "P →Cal* R"
  using assms(2) assms(1)
proof induct
  case (WTS_refl Q Cal)
  assume "P →Cal* Q"
  thus "P →Cal* Q" .
next
  case (WTS_trans Q Cal S R)
  assume "P →Cal* Q ⟹ P →Cal* S" and "P →Cal* Q"
  hence "P →Cal* S"
    by simp
  moreover assume "S ─τ-Cal→Cal R"
  ultimately show "P →Cal* R"
    using weakTauStep.WTS_trans[of P Cal S R]
    by simp
qed

text ‹A weak labelled step is a labelled step surrounded by an arbitrary number of steps on the
      internal action.›

definition weakLabelledActionStep
  :: "'proc ⇒ 'lab ⇒ ('proc, 'lab) labelledProcessCalculus ⇒ 'proc ⇒ bool"
  (‹_ ─_→_* _› [70, 70, 70, 70] 80) where
  "P ─α→Cal* Q ≡ α ≠ τ-Cal ∧ (∃R S. P →Cal* R ∧ R ─α→Cal S ∧ S →Cal* Q)"

definition weakLabelledStep
  :: "'proc ⇒ 'lab ⇒ ('proc, 'lab) labelledProcessCalculus ⇒ 'proc ⇒ bool"
  (‹_ ─⁀_→_* _› [70, 70, 70, 70] 80) where
  "P ─⁀α→Cal* Q ≡ if α = τ-Cal then P →Cal* Q else P ─α→Cal* Q"

text ‹A weak labelled step can be extended by any number of internal steps.›

lemma weakLabelledActionStep_extend_by_internal:
  fixes P P' P'' :: "'proc"
    and α        :: "'lab"
    and Cal      :: "('proc, 'lab) labelledProcessCalculus"
  assumes action:   "P ─α→Cal* P'"
      and internal: "P' →Cal* P''"
    shows "P ─α→Cal* P''"
proof -
  from action obtain R S where A1: "α ≠ τ-Cal" and A2: "P →Cal* R" and A3: "R ─α→Cal S"
                           and A4: "S →Cal* P'"
    unfolding weakLabelledActionStep_def
    by blast
  from internal A4 have "S →Cal* P''"
    using weakTauSteps_trans[of S Cal P' P'']
    by simp
  with A1 A2 A3 show "P ─α→Cal* P''"
    unfolding weakLabelledActionStep_def
    by blast
qed

lemma weakLabelledActionStep_preceeded_by_internal:
  fixes P P' P'' :: "'proc"
    and α        :: "'lab"
    and Cal      :: "('proc, 'lab) labelledProcessCalculus"
  assumes internal: "P →Cal* P'"
      and action:   "P' ─α→Cal* P''"
    shows "P ─α→Cal* P''"
proof -
  from action obtain R S where A1: "α ≠ τ-Cal" and A2: "P' →Cal* R" and A3: "R ─α→Cal S"
                           and A4: "S →Cal* P''"
    unfolding weakLabelledActionStep_def
    by blast
  from internal A2 have "P →Cal* R"
    using weakTauSteps_trans[of P Cal P' R]
    by simp
  with A1 A3 A4 show "P ─α→Cal* P''"
    unfolding weakLabelledActionStep_def
    by blast
qed

lemma weakLabelledStep_extend_by_internal:
  fixes P P' P'' :: "'proc"
    and α        :: "'lab"
    and Cal      :: "('proc, 'lab) labelledProcessCalculus"
  assumes action:   "P ─⁀α→Cal* P'"
      and internal: "P' →Cal* P''"
    shows "P ─⁀α→Cal* P''"
  unfolding weakLabelledStep_def
proof auto
  assume "α = τ-Cal"
  with action have "P →Cal* P'"
    unfolding weakLabelledStep_def
    by simp
  with internal show "P →Cal* P''"
    using weakTauSteps_trans[of P Cal P' P'']
    by simp
next
  assume "α ≠ τ-Cal"
  with action have "P ─α→Cal* P'"
    unfolding weakLabelledStep_def
    by simp
  with internal show "P ─α→Cal* P''"
    using weakLabelledActionStep_extend_by_internal[of P α Cal P' P'']
    by simp
qed

lemma weakLabelledStep_preceeded_by_internal:
  fixes P P' P'' :: "'proc"
    and α        :: "'lab"
    and Cal      :: "('proc, 'lab) labelledProcessCalculus"
  assumes internal: "P →Cal* P'"
      and action:   "P' ─⁀α→Cal* P''"
    shows "P ─⁀α→Cal* P''"
  unfolding weakLabelledStep_def
proof auto
  assume "α = τ-Cal"
  with action have "P' →Cal* P''"
    unfolding weakLabelledStep_def
    by simp
  with internal show "P →Cal* P''"
    using weakTauSteps_trans[of P Cal P' P'']
    by simp
next
  assume "α ≠ τ-Cal"
  with action have "P' ─α→Cal* P''"
    unfolding weakLabelledStep_def
    by simp
  with internal show "P ─α→Cal* P''"
    using weakLabelledActionStep_preceeded_by_internal[of P Cal P' α P'']
    by simp
qed

text ‹A sequence of weak labelled steps is called a weak labelled sequence. Note that for each
      internal action in the sequence an arbitrary number of internal steps can be performed even 0
      and similarly for each other label. Also note that we deliberately do not forbid internal
      labels in the considered word.›

inductive weakLabelledSequence
  :: "'proc ⇒ 'lab list ⇒ ('proc, 'lab) labelledProcessCalculus ⇒ 'proc ⇒ bool"
  (‹_ ─⌢_→_* _› [70, 70, 70, 70] 80) where
  WLS_Nil:  "P →Cal* P' ⟹ P ─⌢[]→Cal* P'"
| WLS_Cons: "⟦P ─⌢w→Cal* P'; P' ─⁀α→Cal* P''⟧ ⟹ P ─⌢(w@[α])→Cal* P''"

lemma internal_weakLabelledSequence:
  fixes P P' :: "'proc"
    and Cal  :: "('proc, 'lab) labelledProcessCalculus"
  assumes "P ─⌢[]→Cal* P'"
  shows "P →Cal * P'"
proof -
  define w where def_w: "w = ([]::'lab list)"
  with assms have "P ─⌢w→Cal* P'"
    by simp
  from this def_w show "P →Cal * P'"
    by (induct, simp_all)
qed

text ‹A weak labelled sequence can be extended by any number of internal steps.›

lemma weakLabelledSequence_extend_by_internal:
  fixes P P' P'' :: "'proc"
    and w        :: "'lab list"
    and Cal      :: "('proc, 'lab) labelledProcessCalculus"
  assumes word:     "P ─⌢w→Cal* P'"
      and internal: "P' →Cal* P''"
    shows "P ─⌢w→Cal* P''"
  using assms
proof (induct arbitrary: P'')
  case (WLS_Nil P Cal P')
  assume "P →Cal* P'" and "P' →Cal* P''"
  hence "P →Cal* P''"
    using weakTauSteps_trans[of P Cal P' P'']
    by simp
  thus "P ─⌢[]→Cal* P''"
    using weakLabelledSequence.WLS_Nil[of P Cal P'']
    by simp
next
  case (WLS_Cons P w Cal P' α R)
  assume "P ─⌢w→Cal* P'"
  moreover assume "P' ─⁀α→Cal* R" and "R →Cal* P''"
  hence "P' ─⁀α→Cal* P''"
    using weakLabelledStep_extend_by_internal[of P' α Cal R P'']
    by simp
  ultimately show "P ─⌢(w@[α])→Cal* P''"
    using weakLabelledSequence.WLS_Cons[of P w Cal P' α P'']
    by simp
qed

lemma weakLabelledSequence_preceeded_by_internal:
  fixes P P' P'' :: "'proc"
    and w        :: "'lab list"
    and Cal      :: "('proc, 'lab) labelledProcessCalculus"
  assumes internal: "P →Cal* P'"
      and word:     "P' ─⌢w→Cal* P''"
    shows "P ─⌢w→Cal* P''"
  using word internal
proof (induct)
  case (WLS_Nil P' Cal P'')
  assume "P →Cal* P'" and "P' →Cal* P''"
  hence "P →Cal* P''"
    using weakTauSteps_trans[of P Cal P' P'']
    by simp
  thus "P ─⌢[]→Cal* P''"
    using weakLabelledSequence.WLS_Nil[of P Cal P'']
    by simp
next
  case (WLS_Cons P' w Cal P'' α P''')
  assume "P →Cal* P' ⟹ P ─⌢w→Cal* P''" and "P →Cal* P'"
  hence "P ─⌢w→Cal* P''"
    by simp
  moreover assume "P'' ─⁀α→Cal* P'''"
  ultimately show "P ─⌢(w@[α])→Cal* P'''"
    using weakLabelledSequence.WLS_Cons[of P w Cal P'' α P''']
    by simp
qed

lemma weakLabelledSequence_single:
  fixes P P' :: "'proc"
    and α    :: "'lab"
    and Cal  :: "('proc, 'lab) labelledProcessCalculus"
  assumes step: "P ─⁀α→Cal* P'"
  shows "P ─⌢[α]→Cal* P'"
proof -
  have "P →Cal* P"
    using WTS_refl[of P Cal]
    by simp
  hence "P ─⌢[]→Cal* P"
    using WLS_Nil[of P Cal P]
    by simp
  with step show "P ─⌢[α]→Cal* P'"
    using WLS_Cons[of P "[]" Cal P α P']
    by simp
qed

lemma weakLabelledSequence_decompose:
  fixes P P' :: "'proc"
    and w    :: "'lab list"
    and Cal  :: "('proc, 'lab) labelledProcessCalculus"
  assumes step: "P ─⌢w→Cal* P'"
  shows "w = [] ⟹ P →Cal* P'"
    and "w ≠ [] ⟹ ∃w' α P''. w = w'@[α] ∧ P ─⌢w'→Cal* P'' ∧ P'' ─⁀α→Cal* P'"
  using step
proof induct
  case (WLS_Nil P Cal P')
  {
    assume "P →Cal* P'"
    thus "P →Cal* P'" .
  next
    assume "[] ≠ []"
    hence False
      by simp
    thus "∃w' α P''. [] = w'@[α] ∧ P ─⌢w'→Cal* P'' ∧ P'' ─⁀α→Cal* P'"
      by simp
  }
next
  case (WLS_Cons P w Cal P' α P'')
  {
    assume "w@[α] = []"
    hence False
      by simp
    thus "P →Cal* P''"
      by simp
  next
    assume "P ─⌢w→Cal* P'" and "P' ─⁀α→Cal* P''"
    thus "∃w' α' P'''. w@[α] = w'@[α'] ∧ P ─⌢w'→Cal* P''' ∧ P''' ─⁀α'→Cal* P''"
      by blast
  }
qed

lemma weakLabelledSequence_single_rev:
  fixes P P' :: "'proc"
    and α    :: "'lab"
    and Cal  :: "('proc, 'lab) labelledProcessCalculus"
  assumes step: "P ─⌢[α]→Cal* P'"
  shows "P ─⁀α→Cal* P'"
proof -
  from step obtain P'' where A1: "P ─⌢[]→Cal* P''" and A2: "P'' ─⁀α→Cal* P'"
    using weakLabelledSequence_decompose(2)[of P "[α]" Cal P']
    by auto
  from A1 have "P →Cal* P''"
    using weakLabelledSequence_decompose(1)[of P "[]" Cal P'']
    by simp
  with A2 show "P ─⁀α→Cal* P'"
    using weakLabelledStep_preceeded_by_internal[of P Cal P'' α P']
    by simp
qed

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

definition divergentLS
  :: "'proc ⇒ ('proc, 'lab) labelledProcessCalculus ⇒ bool" (‹_ →_ω› [70, 70] 80) where
  "P →(Cal)ω ≡ ∀P'. P →Cal* P' ⟶ (∃P''. P' ─τ-Cal→Cal P'')"

end