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

      Processes.

      • nil {Name : Type u} {Constant : Type v} : Process Name Constant

        Terminated process.

      • pre {Name : Type u} {Constant : Type v} (μ : Act Name) (p : Process Name Constant) : Process Name Constant

        Do μ and proceed as p.

      • par {Name : Type u} {Constant : Type v} (p q : Process Name Constant) : Process Name Constant

        p parallel q.

      • choice {Name : Type u} {Constant : Type v} (p q : Process Name Constant) : Process Name Constant

        Do p or q (nondeterministically).

      • res {Name : Type u} {Constant : Type v} (a : Name) (p : Process Name Constant) : Process Name Constant

        Restriction.

      • const {Name : Type u} {Constant : Type v} (c : Constant) : Process Name Constant

        Constant.

      Instances For
        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
          @[instance_reducible]
          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.ccsProc.quot :
          Lean.ParserDescr
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Lean.Parser.Category.ccsProc :
            Category

            Syntactic category for processes.

            Equations
            Instances For
              source
              def Cslib.CCS.ccsProc_ :
              Lean.ParserDescr

              Terminated process.

              Equations
              Instances For
                source
                def Cslib.CCS.«ccsProc_._» :
                Lean.ParserDescr

                Do μ and proceed as p.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  def Cslib.CCS.«ccsProc(_)._» :
                  Lean.ParserDescr

                  Do μ and proceed as p.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    def Cslib.CCS.«ccsProc_+_» :
                    Lean.TrailingParserDescr

                    Do p or q (nondeterministically).

                    Equations
                    Instances For
                      source
                      def Cslib.CCS.«ccsProc_|_» :
                      Lean.TrailingParserDescr

                      p parallel q.

                      Equations
                      Instances For
                        source
                        def Cslib.CCS.ccsProcν__ :
                        Lean.ParserDescr

                        Restriction.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          source
                          def Cslib.CCS.ccsProcConst_ :
                          Lean.ParserDescr

                          Constant.

                          Equations
                          Instances For
                            source
                            def Cslib.CCS.«ccsProc(_)» :
                            Lean.ParserDescr

                            Processes.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              source
                              def Cslib.CCS.«term`(CCS|_)» :
                              Lean.ParserDescr

                              Processes.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              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_reducible]
                                      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_reducible]
                                          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
                                            @[instance_reducible]
                                            instance Cslib.CCS.instHasContextProcess {Name : Type u_1} {Constant : Type u_2} :
                                            HasContext (Process Name Constant)
                                            Equations
                                            source
                                            theorem Cslib.CCS.context_fill_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
                                            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.