Documentation

Cslib.Languages.CCS.Basic

Calculus of Communicating Systems (CCS) #

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

Main definitions #

Main results #

References #

source
🔶 coverage
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
    🔸 coverage
    instance Cslib.CCS.instDecidableEqAct {Name✝ : Type u_1} [DecidableEq Name✝] :
    DecidableEq (Act Name✝)
    Equations
    source
    🔸 coverage
    def Cslib.CCS.instDecidableEqAct.decEq {Name✝ : Type u_1} [DecidableEq Name✝] (x✝ x✝¹ : Act Name✝) :
    Decidable (x✝ = x✝¹)
    Equations
    Instances For
      source
      🔶 coverage
      inductive Cslib.CCS.Process (Name : Type u) (Constant : Type v) :
      Type (max u v)

      Processes.

      Instances For
        source
        🔸 coverage
        instance Cslib.CCS.instDecidableEqProcess {Name✝ : Type u_1} {Constant✝ : Type u_2} [DecidableEq Name✝] [DecidableEq Constant✝] :
        DecidableEq (Process Name✝ Constant✝)
        Equations
        source
        🔸 coverage
        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
          🔶 coverage
          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
            🔶 coverage
            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
              📐 coverage
              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
              🔸 coverage
              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
                ⇕ coverage
                theorem Cslib.CCS.Act.isCo_iff {Name : Type u_1} [DecidableEq Name] {μ μ' : Act Name} :
                μ.isCo μ' = true ↔ μ.Co μ'
                source
                🔸 coverage
                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
                🔶 coverage
                inductive Cslib.CCS.Context (Name : Type u) (Constant : Type v) :
                Type (max u v)

                Contexts.

                Instances For
                  source
                  🔸 coverage
                  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
                    🔸 coverage
                    instance Cslib.CCS.instDecidableEqContext {Name✝ : Type u_1} {Constant✝ : Type u_2} [DecidableEq Name✝] [DecidableEq Constant✝] :
                    DecidableEq (Context Name✝ Constant✝)
                    Equations
                    source
                    🔸 coverage
                    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
                      🔸 coverage
                      instance Cslib.CCS.instHasContextProcess {Name : Type u_1} {Constant : Type u_2} :
                      HasContext (Process Name Constant)
                      Equations
                      source
                      📐 coverage
                      theorem Cslib.CCS.isContext_def {Name : Type u_1} {Constant : Type u_2} (c : Context Name Constant) (p : Process Name Constant) :
                      c[p] = c.fill p

                      Definition of context filling.

                      source
                      📐 coverage
                      theorem Cslib.CCS.Context.complete {Name : Type u_1} {Constant : Type u_2} (p : Process Name Constant) :
                      ∃ (c : Context Name Constant), p = c[Process.nil] ∨ ∃ (k : Constant), p = c[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.