Documentation

Cslib.Languages.CCS.Basic

Calculus of Communicating Systems (CCS) #

CCS [Mil80], as presented in [San]. In the semantics (see CCS.lts), we adopt the option of constant definitions (K = P).

Main definitions #

Main results #

References #

source
inductive Cslib.CCS.Act (Name : Type u) :
Type u

Actions.

  • name {Name : Type u} (a : Name) : Act Name
  • coname {Name : Type u} (a : Name) : Act Name
  • τ {Name : Type u} : Act Name
Instances For
    source
    instance Cslib.CCS.instDecidableEqAct {Name✝ : Type u_1} [DecidableEq Name✝] :
    DecidableEq (Act Name✝)
    Equations
    source
    def Cslib.CCS.instDecidableEqAct.decEq {Name✝ : Type u_1} [DecidableEq Name✝] (x✝ x✝¹ : Act Name✝) :
    Decidable (x✝ = x✝¹)
    Equations
    Instances For
      source
      inductive Cslib.CCS.Process (Name : Type u) (Constant : Type v) :
      Type (max u v)

      Processes.

      Instances For
        source
        instance Cslib.CCS.instDecidableEqProcess {Name✝ : Type u_1} {Constant✝ : Type u_2} [DecidableEq Name✝] [DecidableEq Constant✝] :
        DecidableEq (Process Name✝ Constant✝)
        Equations
        source
        def Cslib.CCS.instDecidableEqProcess.decEq {Name✝ : Type u_1} {Constant✝ : Type u_2} [DecidableEq Name✝] [DecidableEq Constant✝] (x✝ x✝¹ : Process Name✝ Constant✝) :
        Decidable (x✝ = x✝¹)
        Equations
        Instances For
          source
          inductive Cslib.CCS.Act.IsVisible {Name : Type u_1} :
          Act Name → Prop

          An action is visible if it a name or a coname.

          Instances For
            source
            @[simp]
            theorem Cslib.CCS.Act.isVisible_neq_τ {Name : Type u_1} {μ : Act Name} (h : μ.IsVisible) :
            μ ≠ τ

            If an action is visible, it is not τ.

            source
            inductive Cslib.CCS.Act.Co {Name : Type u} :
            Act Name → Act Name → Prop

            Checks that an action is the coaction of another.

            Instances For
              source
              theorem Cslib.CCS.Act.Co.symm {Name✝ : Type u_1} {μ μ' : Act Name✝} (h : μ.Co μ') :
              μ'.Co μ

              Act.Co is symmetric.

              source
              theorem Cslib.CCS.Act.co_isVisible {Name✝ : Type u_1} {μ μ' : Act Name✝} (h : μ.Co μ') :
              μ.IsVisible ∧ μ'.IsVisible

              If two actions are one the coaction of the other, then they are both visible.

              source
              def Cslib.CCS.Act.isCo {Name : Type u_1} [DecidableEq Name] (μ μ' : Act Name) :
              Bool

              Checks that an action is the coaction of another. This is the Boolean version of Act.Co.

              Equations
              Instances For
                source
                theorem Cslib.CCS.Act.isCo_iff {Name : Type u_1} [DecidableEq Name] {μ μ' : Act Name} :
                μ.isCo μ' = true ↔ μ.Co μ'
                source
                instance Cslib.CCS.Act.instDecidableCoOfDecidableEq {Name : Type u_1} [DecidableEq Name] {μ μ' : Act Name} :
                Decidable (μ.Co μ')

                Act.Co is decidable if Name equality is decidable.

                Equations
                source
                inductive Cslib.CCS.Context (Name : Type u) (Constant : Type v) :
                Type (max u v)

                Contexts.

                Instances For
                  source
                  def Cslib.CCS.instDecidableEqContext.decEq {Name✝ : Type u_1} {Constant✝ : Type u_2} [DecidableEq Name✝] [DecidableEq Constant✝] (x✝ x✝¹ : Context Name✝ Constant✝) :
                  Decidable (x✝ = x✝¹)
                  Equations
                  Instances For
                    source
                    instance Cslib.CCS.instDecidableEqContext {Name✝ : Type u_1} {Constant✝ : Type u_2} [DecidableEq Name✝] [DecidableEq Constant✝] :
                    DecidableEq (Context Name✝ Constant✝)
                    Equations
                    source
                    def Cslib.CCS.Context.fill {Name : Type u_1} {Constant : Type u_2} (c : Context Name Constant) (p : Process Name Constant) :
                    Process Name Constant

                    Replaces the hole in a Context with a Process.

                    Equations
                    Instances For
                      source
                      theorem Cslib.CCS.Context.complete {Name : Type u_1} {Constant : Type u_2} (p : Process Name Constant) :
                      ∃ (c : Context Name Constant), p = c.fill Process.nil ∨ ∃ (k : Constant), p = c.fill (Process.const k)

                      Any Process can be obtained by filling a Context with an atom. This proves that Context is a complete formalisation of syntactic contexts for CCS.