4.3. Derived operators on concrete bigraphs🔗

Parallel product, merge and closure on concrete link graphs and bigraphs, with the laws relating them to the tensor product \otimes of Tensor.lean, which is defined when the supports are disjoint and the inner and the outer names are disjoint.

Definition4.3.1

uses 1used by 1✓L∃∀N

Tagsfrom sourcenot audited

The parallel product (TR-580 Defs 8.6, 9.13) takes the union of the link maps, so that an outer name shared by the two factors is one name, and keeps the places side by side. For link graphs A : X \to Y, A' : X' \to Y' and bigraphs G : \langle m, X \rangle \to \langle n, Y \rangle, G' : \langle m', X' \rangle \to \langle n', Y' \rangle, writing \mid_{\ell} for the parallel product of link graphs (TR-580 writes \mid, Def 8.6),

A \mid_{\ell} A' : X \cup X' \to Y \cup Y', \qquad G \parallel G' = \langle G^{\mathsf P} \otimes G'^{\mathsf P},\; G^{\mathsf L} \mid_{\ell} G'^{\mathsf L} \rangle : \langle m + m', X \cup X' \rangle \to \langle n + n', Y \cup Y' \rangle ,

defined when X \cap X' = \emptyset and the link graphs are disjoint: no natural number is a node or an edge of both. The parallel product of hard bigraphs is hard. The domain is smaller than the source's, which asks of bigraphs only that the node sets be disjoint: here the edges are disjoint too, and no number is a node of one factor and an edge of the other.

Class: LiG.par, Big.par, BigH.par FROM SOURCE; LiG.Disjoint not audited.

Lean code for Definition4.3.1●4 definitions

defdefined in Bigraph/Concrete/Par.lean

complete

def par {Ctrl : Type} {S : Bigraph.Sig Ctrl} {X Y X' Y' : NSet}
  (A : LiG S X Y) (A' : LiG S X' Y') (h : A.Disjoint A')
  (_hX : X.Disjoint X') : LiG S (X.union X') (Y.union Y')

def par {Ctrl : Type} {S : Bigraph.Sig Ctrl}
  {X Y X' Y' : NSet} (A : LiG S X Y)
  (A' : LiG S X' Y') (h : A.Disjoint A')
  (_hX : X.Disjoint X') :
  LiG S (X.union X') (Y.union Y')

**The parallel product of link graphs** `A | A' : X ∪ X' → Y ∪ Y'`: the
construction of TR-580 Def 8.6 (the union of the link maps; the inner
names disjoint, as the Def asks; the outer names may be shared, and a
shared outer name is one name). The link map is the tensor's
(`tensorLink`).

DOMAIN RESTRICTION (the library's, not the text's). Def 8.6 states no
support condition. Here the supports must be disjoint in one supply:
`(V ∪ E) ∩ (V' ∪ E') = ∅`. So this rejects pairs that share an edge
number (which the text of 8.6 and 9.13 does not exclude, though Prop
9.14 implies it must) and pairs in which one number is a node of one and
an edge of the other (never excluded by the source, where nodes and
edges are separate sets). Every source-admissible pair with disjoint
edge sets is admitted after a support translation. The library's
composition and tensor carry the same restriction.

defdefined in Bigraph/Concrete/Par.lean

complete

def par {Ctrl : Type} {S : Bigraph.Sig Ctrl} {I J I' J' : Face}
  (A : Big S I J) (A' : Big S I' J') (h : A.L.Disjoint A'.L)
  (hX : I.names.Disjoint I'.names) : Big S (I.tensor I') (J.tensor J')

def par {Ctrl : Type} {S : Bigraph.Sig Ctrl}
  {I J I' J' : Face} (A : Big S I J)
  (A' : Big S I' J')
  (h : A.L.Disjoint A'.L)
  (hX : I.names.Disjoint I'.names) :
  Big S (I.tensor I') (J.tensor J')

**The parallel product of bigraphs** `A ‖ A' : I ⊗ I' → J ‖ J'`: the
construction of TR-580 Def 9.13, `⟨A^P ⊗ A'^P, A^L | A'^L⟩`, with the inner
names disjoint. It keeps the regions of `A` and `A'` separate and
identifies shared outer names. DOMAIN RESTRICTION: Def 9.13 asks that
"the node sets are disjoint"; here the supports must be disjoint in one
supply, which is stricter (see `LiG.par`).

defdefined in Bigraph/Concrete/Par.lean

complete

def par {Ctrl : Type} {S : Bigraph.Sig Ctrl} {I J I' J' : Face}
  (A : BigH S I J) (A' : BigH S I' J') (h : A.big.L.Disjoint A'.big.L)
  (hX : I.names.Disjoint I'.names) : BigH S (I.tensor I') (J.tensor J')

def par {Ctrl : Type} {S : Bigraph.Sig Ctrl}
  {I J I' J' : Face} (A : BigH S I J)
  (A' : BigH S I' J')
  (h : A.big.L.Disjoint A'.big.L)
  (hX : I.names.Disjoint I'.names) :
  BigH S (I.tensor I') (J.tensor J')

**The parallel product of hard bigraphs** (TR-580 Def 9.13 in ´BIG_h):
hard because the tensor of hard place graphs is hard.

defdefined in Bigraph/Concrete/Link.lean

complete

def Disjoint {Ctrl : Type} {S : Bigraph.Sig Ctrl} {X Y X' Y' : NSet}
  (A : LiG S X Y) (B : LiG S X' Y') : Prop

def Disjoint {Ctrl : Type}
  {S : Bigraph.Sig Ctrl}
  {X Y X' Y' : NSet} (A : LiG S X Y)
  (B : LiG S X' Y') : Prop

No node or edge in common.

Theorem4.3.2

uses 1used by 0✓L∃∀N

Where the tensor product is defined, the parallel product is the tensor product. For link graphs and for bigraphs with disjoint supports and X \cap X' = \emptyset,

Y \cap Y' = \emptyset \;\Longrightarrow\; A \mid_{\ell} A' = A \otimes A' \;\text{ and }\; G \parallel G' = G \otimes G' .

Rests on not audited: Big, LiG, LiG.Disjoint, NSet.Disjoint.

Lean code for Theorem4.3.2●2 theorems

theoremdefined in Bigraph/Concrete/Par.lean

complete

theorem par_eq_tensor {Ctrl : Type} {S : Bigraph.Sig Ctrl} {X Y X' Y' : NSet}
  (A : LiG S X Y) (A' : LiG S X' Y') (h : A.Disjoint A')
  (hX : X.Disjoint X') (hY : Y.Disjoint Y') :
  A.par A' h hX = A.tensor A' h hX hY

theorem par_eq_tensor {Ctrl : Type}
  {S : Bigraph.Sig Ctrl}
  {X Y X' Y' : NSet} (A : LiG S X Y)
  (A' : LiG S X' Y') (h : A.Disjoint A')
  (hX : X.Disjoint X')
  (hY : Y.Disjoint Y') :
  A.par A' h hX = A.tensor A' h hX hY

**With disjoint outer names the parallel product is the tensor product**
(TR-580 §8: `|` "does not require them to be disjoint").

theoremdefined in Bigraph/Concrete/Par.lean

complete

theorem par_eq_tensor {Ctrl : Type} {S : Bigraph.Sig Ctrl} {I J I' J' : Face}
  (A : Big S I J) (A' : Big S I' J') (h : A.L.Disjoint A'.L)
  (hX : I.names.Disjoint I'.names) (hY : J.names.Disjoint J'.names) :
  A.par A' h hX = A.tensor A' h hX hY

theorem par_eq_tensor {Ctrl : Type}
  {S : Bigraph.Sig Ctrl}
  {I J I' J' : Face} (A : Big S I J)
  (A' : Big S I' J')
  (h : A.L.Disjoint A'.L)
  (hX : I.names.Disjoint I'.names)
  (hY : J.names.Disjoint J'.names) :
  A.par A' h hX = A.tensor A' h hX hY

With disjoint outer names, `‖` is `⊗`.

Definition4.3.3

uses 0

Used by 2

Reverse dependency previews

Preview

Theorem 4.3.5

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Tagsnewnot audited

The two sides of a law may have faces, such as \emptyset \cup Y and Y, that are equal as sets of names without being the same expression. Link graphs A : X \to Y and B : X' \to Y' are the same, A \doteq B, when X and X' have the same members, so do Y and Y', and the controls, the edges and the link maps are equal. Bigraphs G : \langle m, X \rangle \to \langle n, Y \rangle and H : \langle m, X' \rangle \to \langle n, Y' \rangle are the same when their place graphs are equal and their link graphs are the same. Between graphs of the same faces this is equality:

A, B : X \to Y \;\Longrightarrow\; (A \doteq B \iff A = B) .

Class: LiG.Same, Big.Same NEW; LiG.same_iff_eq, Big.same_iff_eq not audited.

Lean code for Definition4.3.3●4 declarations

defdefined in Bigraph/Concrete/Same.lean

complete

def Same {Ctrl : Type} {S : Bigraph.Sig Ctrl} {X Y X' Y' : NSet}
  (A : LiG S X Y) (B : LiG S X' Y') : Prop

def Same {Ctrl : Type} {S : Bigraph.Sig Ctrl}
  {X Y X' Y' : NSet} (A : LiG S X Y)
  (B : LiG S X' Y') : Prop

**The same link graph, at possibly differently presented faces**: the
faces have the same names, and the controls, edges and link maps are
equal. Between link graphs of the SAME faces this is equality
(`LiG.ext`). It is used where the two sides of a law have faces such as
`∅ ∪ Y` and `Y`, which are equal as sets but are not the same Lean
expression; stating the law with `=` would need a transport, which is
avoided.

defdefined in Bigraph/Concrete/Same.lean

complete

def Same {Ctrl : Type} {S : Bigraph.Sig Ctrl} {m n : Nat} {X Y X' Y' : NSet}
  (A : Big S { width := m, names := X } { width := n, names := Y })
  (B : Big S { width := m, names := X' } { width := n, names := Y' }) :
  Prop

def Same {Ctrl : Type} {S : Bigraph.Sig Ctrl}
  {m n : Nat} {X Y X' Y' : NSet}
  (A :
    Big S { width := m, names := X }
      { width := n, names := Y })
  (B :
    Big S { width := m, names := X' }
      { width := n, names := Y' }) :
  Prop

**The same bigraph, at possibly differently presented names**: equal
widths (the same Lean expressions `m`, `n`), equal place graphs, and
link graphs that are `LiG.Same`. Between bigraphs of the same faces this
is equality (`same_iff_eq`).

theoremdefined in Bigraph/Concrete/Same.lean

complete

theorem same_iff_eq {Ctrl : Type} {S : Bigraph.Sig Ctrl} {X Y : NSet}
  (A B : LiG S X Y) : A.Same B ↔ A = B

theorem same_iff_eq {Ctrl : Type}
  {S : Bigraph.Sig Ctrl} {X Y : NSet}
  (A B : LiG S X Y) : A.Same B ↔ A = B

**`Same` identifies nothing**: between link graphs of the same faces it
is equality.

theoremdefined in Bigraph/Concrete/Same.lean

complete

theorem same_iff_eq {Ctrl : Type} {S : Bigraph.Sig Ctrl} {m n : Nat}
  {X Y : NSet}
  (A B : Big S { width := m, names := X } { width := n, names := Y }) :
  A.Same B ↔ A = B

theorem same_iff_eq {Ctrl : Type}
  {S : Bigraph.Sig Ctrl} {m n : Nat}
  {X Y : NSet}
  (A B :
    Big S { width := m, names := X }
      { width := n, names := Y }) :
  A.Same B ↔ A = B

`Big.Same` identifies nothing.

Definition4.3.4

uses 1

Used by 2

Reverse dependency previews

Preview

Theorem 4.3.5

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Tagsfrom sourcebridgednew

Merge and closure, each defined directly and with no nodes. The merge \mathrm{merge}_m^X : \langle m, X \rangle \to \langle 1, X \rangle puts every site in the one root and links every name to itself; the sources write it \mathrm{merge}_m \otimes \mathrm{id}_X. The closure /_{k}\, x : \{x\} \to \emptyset has the one edge k, to which x is linked. For X \cap Y = \emptyset and a numbering e of edges that is injective on X, the multiple closure

\mathrm{cl}_e(X; Y) : X \cup Y \to Y

has one edge e(x) for each x \in X, to which x is linked, and links each name of Y to itself; the sources write it /X \otimes \mathrm{id}_Y. On bigraphs, \mathrm{cl}^m_e(X; Y) = \langle \mathrm{id}_m, \mathrm{cl}_e(X; Y) \rangle : \langle m, X \cup Y \rangle \to \langle m, Y \rangle, and /_{k}\, x also denotes the bigraph \langle \mathrm{id}_0, /_{k}\, x \rangle : \langle 0, \{x\} \rangle \to \langle 0, \emptyset \rangle. A concrete closure must number its edges; the sources' closure has one edge for each name, without a number.

Class: Big.mergeN, LiG.closure, Big.closure BRIDGED; LiG.closure1 FROM SOURCE; Big.closure1, Big.closureW NEW.

Lean code for Definition4.3.4●6 definitions

defdefined in Bigraph/Concrete/Wiring.lean

complete

def mergeN {Ctrl : Type} {S : Bigraph.Sig Ctrl} (m : Nat) (X : NSet) :
  Big S { width := m, names := X } { width := 1, names := X }

def mergeN {Ctrl : Type}
  {S : Bigraph.Sig Ctrl} (m : Nat)
  (X : NSet) :
  Big S { width := m, names := X }
    { width := 1, names := X }

**`merge_m ⊗ id_X : ⟨m, X⟩ → ⟨1, X⟩`**: no nodes, every site in the one
root, every name linked to itself. For `X = ∅` this is BiCoq §2.2.2's
`merge_m = ⟨∅,∅,∅, s↦0, ∅⟩`, component by component. For general `X` it
is the object `merge ⊗ id_X` of TR-580 §9 p. 59 and BiCoq §6.2, which no
source defines as a primitive; the law relating the two is
`Big.mergeId` (`MergeIdStatement`). For `m = 0` and `X = ∅` this is the
barren root `1` (for general `X`, `1 ⊗ id_X`); neither is hard.

defdefined in Bigraph/Concrete/Wiring.lean

complete

def closure1 {Ctrl : Type} {S : Bigraph.Sig Ctrl} (x e : Nat) :
  LiG S (NSet.single x) NSet.empty

def closure1 {Ctrl : Type}
  {S : Bigraph.Sig Ctrl} (x e : Nat) :
  LiG S (NSet.single x) NSet.empty

**The closure `/x : {x} → ∅`** (TR-580 §9: "/x : x→ϵ, called closure"; one
of the six elementary bigraphs of §10), as a concrete link graph: no
nodes, ONE edge, numbered `e`, to which the inner name `x` is linked.
(The source's edge has no identity up to support equivalence; a concrete
link graph must number it.)

defdefined in Bigraph/Concrete/Wiring.lean

complete

def closure {Ctrl : Type} {S : Bigraph.Sig Ctrl} (X Y : NSet)
  (ed : Nat → Nat) (_hXY : X.Disjoint Y)
  (_hinj :
    ∀ (x x' : Nat),
      X.mem x = true → X.mem x' = true → ed x = ed x' → x = x') :
  LiG S (X.union Y) Y

def closure {Ctrl : Type}
  {S : Bigraph.Sig Ctrl} (X Y : NSet)
  (ed : Nat → Nat) (_hXY : X.Disjoint Y)
  (_hinj :
    ∀ (x x' : Nat),
      X.mem x = true →
        X.mem x' = true →
          ed x = ed x' → x = x') :
  LiG S (X.union Y) Y

**The multiple closure** `/X ⊗ id_Y : X ∪ Y → Y` (TR-580 §9: "/x : x→ϵ,
called closure … /X for the multiple closure /x₁⊗···⊗/xₙ"), for disjoint
`X`, `Y`: no nodes; one edge `ed x` for each name `x ∈ X`, to which `x`
is linked; each name of `Y` linked to itself. The edges are distinct
when `ed` is injective on `X` (the hypothesis `_hinj`, a definedness
condition: with a non-injective `ed` this would be a closure after a
substitution).

defdefined in Bigraph/Concrete/Wiring.lean

complete

def closure {Ctrl : Type} {S : Bigraph.Sig Ctrl} (m : Nat) (X Y : NSet)
  (ed : Nat → Nat) (hXY : X.Disjoint Y)
  (hinj :
    ∀ (x x' : Nat),
      X.mem x = true → X.mem x' = true → ed x = ed x' → x = x') :
  Big S { width := m, names := X.union Y } { width := m, names := Y }

def closure {Ctrl : Type}
  {S : Bigraph.Sig Ctrl} (m : Nat)
  (X Y : NSet) (ed : Nat → Nat)
  (hXY : X.Disjoint Y)
  (hinj :
    ∀ (x x' : Nat),
      X.mem x = true →
        X.mem x' = true →
          ed x = ed x' → x = x') :
  Big S { width := m, names := X.union Y }
    { width := m, names := Y }

**`id_m ⊗ /X ⊗ id_Y : ⟨m, X ∪ Y⟩ → ⟨m, Y⟩`**: the closure of the names
`X` of an interface of width `m`, the names `Y` kept.

defdefined in Bigraph/Concrete/Wiring.lean

complete

def closure1 {Ctrl : Type} {S : Bigraph.Sig Ctrl} (x e : Nat) :
  Big S { width := 0, names := NSet.single x }
    { width := 0, names := NSet.empty }

def closure1 {Ctrl : Type}
  {S : Bigraph.Sig Ctrl} (x e : Nat) :
  Big S
    { width := 0, names := NSet.single x }
    { width := 0, names := NSet.empty }

**The closure `/x` as a bigraph of width 0**: `⟨id_0, /x⟩ : ⟨0, {x}⟩ → ⟨0, ∅⟩`.

defdefined in Bigraph/Concrete/Wiring.lean

complete

def closureW {Ctrl : Type} {S : Bigraph.Sig Ctrl} (X Y : NSet)
  (ed : Nat → Nat) (hXY : X.Disjoint Y)
  (hinj :
    ∀ (x x' : Nat),
      X.mem x = true → X.mem x' = true → ed x = ed x' → x = x') :
  Big S { width := 0, names := X.union Y } { width := 0, names := Y }

def closureW {Ctrl : Type}
  {S : Bigraph.Sig Ctrl} (X Y : NSet)
  (ed : Nat → Nat) (hXY : X.Disjoint Y)
  (hinj :
    ∀ (x x' : Nat),
      X.mem x = true →
        X.mem x' = true →
          ed x = ed x' → x = x') :
  Big S { width := 0, names := X.union Y }
    { width := 0, names := Y }

The width-0 bigraph carrying a multiple closure: `⟨id₀, /X ⊗ id_Y⟩`.

Theorem4.3.5

Statement uses 2

Statement dependency previews

Preview

Definition 4.3.3

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 1✓L∃∀N

The multiple closure of link graphs is the tensor of the single closures with the identity on Y. For every Y and e; for every x and e; and for x \notin X, (\{x\} \cup X) \cap Y = \emptyset and e injective on \{x\} \cup X:

\mathrm{cl}_e(\emptyset; Y) \doteq \mathrm{id}_Y, \qquad \mathrm{cl}_e(\{x\}; \emptyset) \doteq /_{e(x)}\, x, \qquad \mathrm{cl}_e(\{x\} \cup X; Y) \doteq /_{e(x)}\, x \otimes \mathrm{cl}_e(X; Y) .

In the third law the right side is defined under the hypotheses given, one instance being checked on x = 0, X = \{1\}, Y = \{2\}.

Rests on NEW: LiG.Same, NSet.single; not audited: LiG.Disjoint, LiG.id, NSet.Disjoint, NSet.empty.

Lean code for Theorem4.3.5●7 declarations

theoremdefined in Bigraph/Concrete/Wiring.lean

complete

theorem closureEmpty {Ctrl : Type} {S : Bigraph.Sig Ctrl} :
  LiG.ClosureEmptyStatement S

theorem closureEmpty {Ctrl : Type}
  {S : Bigraph.Sig Ctrl} :
  LiG.ClosureEmptyStatement S

**(C-a) PROVED**: `/∅ ⊗ id_Y = id_Y`.

theoremdefined in Bigraph/Concrete/Wiring.lean

complete

theorem closureSingle {Ctrl : Type} {S : Bigraph.Sig Ctrl} :
  LiG.ClosureSingleStatement S

theorem closureSingle {Ctrl : Type}
  {S : Bigraph.Sig Ctrl} :
  LiG.ClosureSingleStatement S

**(C-b) PROVED**: `/{x} ⊗ id_∅ = /x`, the edge being `ed x`.

theoremdefined in Bigraph/Concrete/Wiring.lean

complete

theorem closureCons {Ctrl : Type} {S : Bigraph.Sig Ctrl} :
  LiG.ClosureConsStatement S

theorem closureCons {Ctrl : Type}
  {S : Bigraph.Sig Ctrl} :
  LiG.ClosureConsStatement S

**(C-c) PROVED**: for `x ∉ X`, `/({x} ∪ X) ⊗ id_Y = /x ⊗ (/X ⊗ id_Y)`.

theoremdefined in Bigraph/Concrete/Wiring.lean

complete

theorem closureCons_derived {Ctrl : Type} {S : Bigraph.Sig Ctrl} (x : Nat)
  (X Y : NSet) (ed : Nat → Nat) (hx : X.mem x = false)
  (h₁ : ((NSet.single x).union X).Disjoint Y)
  (i₁ :
    ∀ (y y' : Nat),
      ((NSet.single x).union X).mem y = true →
        ((NSet.single x).union X).mem y' = true →
          ed y = ed y' → y = y') :
  (LiG.closure ((NSet.single x).union X) Y ed h₁ i₁).Same
    ((LiG.closure1 x (ed x)).tensor (LiG.closure X Y ed ⋯ ⋯) ⋯ ⋯ ⋯)

theorem closureCons_derived {Ctrl : Type}
  {S : Bigraph.Sig Ctrl} (x : Nat)
  (X Y : NSet) (ed : Nat → Nat)
  (hx : X.mem x = false)
  (h₁ :
    ((NSet.single x).union X).Disjoint Y)
  (i₁ :
    ∀ (y y' : Nat),
      ((NSet.single x).union X).mem y =
          true →
        ((NSet.single x).union X).mem y' =
            true →
          ed y = ed y' → y = y') :
  (LiG.closure ((NSet.single x).union X) Y
        ed h₁ i₁).Same
    ((LiG.closure1 x (ed x)).tensor
      (LiG.closure X Y ed ⋯ ⋯) ⋯ ⋯ ⋯)

**(C-c) with only its three proper hypotheses** `x ∉ X`, `h₁`, `i₁`: the
other five definedness conditions are derived. PROVED.

defdefined in Bigraph/Concrete/Wiring.lean

complete

def ClosureEmptyStatement {Ctrl : Type} (S : Bigraph.Sig Ctrl) : Prop

def ClosureEmptyStatement {Ctrl : Type}
  (S : Bigraph.Sig Ctrl) : Prop

**(C-a)** `/∅ ⊗ id_Y = id_Y`. PROVED: `closureEmpty`.

defdefined in Bigraph/Concrete/Wiring.lean

complete

def ClosureSingleStatement {Ctrl : Type} (S : Bigraph.Sig Ctrl) : Prop

def ClosureSingleStatement {Ctrl : Type}
  (S : Bigraph.Sig Ctrl) : Prop

**(C-b)** `/{x} ⊗ id_∅ = /x`, the edge being `ed x`. PROVED:
`closureSingle`.

defdefined in Bigraph/Concrete/Wiring.lean

complete

def ClosureConsStatement {Ctrl : Type} (S : Bigraph.Sig Ctrl) : Prop

def ClosureConsStatement {Ctrl : Type}
  (S : Bigraph.Sig Ctrl) : Prop

**(C-c)** for `x ∉ X`: `/({x} ∪ X) ⊗ id_Y = /x ⊗ (/X ⊗ id_Y)`, the right
side the library's tensor of link graphs. Every definedness condition of
either side is a hypothesis. PROVED: `closureCons`; the hypotheses `h₂`,
`i₂`, `hd`, `hX`, `hY` follow from the first three
(`closureCons_derived`).

Theorem4.3.6

uses 1used by 0✓L∃∀N

The third closure law with the single closure on the right, for link graphs and for bigraphs of any width m: for x \notin X, (\{x\} \cup X) \cap Y = \emptyset and e injective on \{x\} \cup X,

\mathrm{cl}_e(\{x\} \cup X; Y) \doteq \mathrm{cl}_e(X; Y) \otimes /_{e(x)}\, x, \qquad \mathrm{cl}^m_e(\{x\} \cup X; Y) \doteq \mathrm{cl}^m_e(X; Y) \otimes /_{e(x)}\, x ,

and the width of a closure is a tensor with an identity: for X \cap Y = \emptyset and e injective on X,

\mathrm{cl}^m_e(X; Y) \doteq \mathrm{id}_{\langle m, \emptyset \rangle} \otimes \mathrm{cl}^0_e(X; Y) .

The law on bigraphs with the single closure on the left is OPEN: its two sides have widths 0 + m and m, and it has not been stated.

Rests on NEW: Big.Same, Big.closure1, Big.closureW, LiG.Same, NSet.single; not audited: Big, LiG.Disjoint, NSet.Disjoint, NSet.empty.

Lean code for Theorem4.3.6●4 theorems

theoremdefined in Bigraph/Concrete/Wiring.lean

complete

theorem closureSnoc {Ctrl : Type} {S : Bigraph.Sig Ctrl} (x : Nat) (X Y : NSet)
  (ed : Nat → Nat) (hx : X.mem x = false)
  (h₁ : ((NSet.single x).union X).Disjoint Y)
  (i₁ :
    ∀ (y y' : Nat),
      ((NSet.single x).union X).mem y = true →
        ((NSet.single x).union X).mem y' = true → ed y = ed y' → y = y')
  (h₂ : X.Disjoint Y)
  (i₂ :
    ∀ (y y' : Nat),
      X.mem y = true → X.mem y' = true → ed y = ed y' → y = y')
  (hd : (LiG.closure X Y ed h₂ i₂).Disjoint (LiG.closure1 x (ed x)))
  (hX : (X.union Y).Disjoint (NSet.single x))
  (hY : Y.Disjoint NSet.empty) :
  (LiG.closure ((NSet.single x).union X) Y ed h₁ i₁).Same
    ((LiG.closure X Y ed h₂ i₂).tensor (LiG.closure1 x (ed x)) hd hX hY)

theorem closureSnoc {Ctrl : Type}
  {S : Bigraph.Sig Ctrl} (x : Nat)
  (X Y : NSet) (ed : Nat → Nat)
  (hx : X.mem x = false)
  (h₁ :
    ((NSet.single x).union X).Disjoint Y)
  (i₁ :
    ∀ (y y' : Nat),
      ((NSet.single x).union X).mem y =
          true →
        ((NSet.single x).union X).mem y' =
            true →
          ed y = ed y' → y = y')
  (h₂ : X.Disjoint Y)
  (i₂ :
    ∀ (y y' : Nat),
      X.mem y = true →
        X.mem y' = true →
          ed y = ed y' → y = y')
  (hd :
    (LiG.closure X Y ed h₂ i₂).Disjoint
      (LiG.closure1 x (ed x)))
  (hX :
    (X.union Y).Disjoint (NSet.single x))
  (hY : Y.Disjoint NSet.empty) :
  (LiG.closure ((NSet.single x).union X) Y
        ed h₁ i₁).Same
    ((LiG.closure X Y ed h₂ i₂).tensor
      (LiG.closure1 x (ed x)) hd hX hY)

**(C-c) with `/x` on the right**: for `x ∉ X`,
`/({x} ∪ X) ⊗ id_Y = (/X ⊗ id_Y) ⊗ /x`. PROVED.

theoremdefined in Bigraph/Concrete/Wiring.lean

complete

theorem closureSnoc {Ctrl : Type} {S : Bigraph.Sig Ctrl} (m x : Nat)
  (X Y : NSet) (ed : Nat → Nat) (hx : X.mem x = false)
  (h₁ : ((NSet.single x).union X).Disjoint Y)
  (i₁ :
    ∀ (y y' : Nat),
      ((NSet.single x).union X).mem y = true →
        ((NSet.single x).union X).mem y' = true → ed y = ed y' → y = y')
  (h₂ : X.Disjoint Y)
  (i₂ :
    ∀ (y y' : Nat),
      X.mem y = true → X.mem y' = true → ed y = ed y' → y = y')
  (hd :
    (Big.closure m X Y ed h₂ i₂).L.Disjoint (Big.closure1 x (ed x)).L)
  (hX : (X.union Y).Disjoint (NSet.single x))
  (hY : Y.Disjoint NSet.empty) :
  (Big.closure m ((NSet.single x).union X) Y ed h₁ i₁).Same
    ((Big.closure m X Y ed h₂ i₂).tensor (Big.closure1 x (ed x)) hd hX
      hY)

theorem closureSnoc {Ctrl : Type}
  {S : Bigraph.Sig Ctrl} (m x : Nat)
  (X Y : NSet) (ed : Nat → Nat)
  (hx : X.mem x = false)
  (h₁ :
    ((NSet.single x).union X).Disjoint Y)
  (i₁ :
    ∀ (y y' : Nat),
      ((NSet.single x).union X).mem y =
          true →
        ((NSet.single x).union X).mem y' =
            true →
          ed y = ed y' → y = y')
  (h₂ : X.Disjoint Y)
  (i₂ :
    ∀ (y y' : Nat),
      X.mem y = true →
        X.mem y' = true →
          ed y = ed y' → y = y')
  (hd :
    (Big.closure m X Y ed h₂
            i₂).L.Disjoint
      (Big.closure1 x (ed x)).L)
  (hX :
    (X.union Y).Disjoint (NSet.single x))
  (hY : Y.Disjoint NSet.empty) :
  (Big.closure m ((NSet.single x).union X)
        Y ed h₁ i₁).Same
    ((Big.closure m X Y ed h₂ i₂).tensor
      (Big.closure1 x (ed x)) hd hX hY)

**(C-c) on bigraphs, `/x` on the right**: for `x ∉ X`,
`id_m ⊗ /({x} ∪ X) ⊗ id_Y = (id_m ⊗ /X ⊗ id_Y) ⊗ /x`, the right side the
library's tensor of bigraphs, of widths `m + 0`. PROVED.

theoremdefined in Bigraph/Concrete/Wiring.lean

complete

theorem closureSnoc_derived {Ctrl : Type} {S : Bigraph.Sig Ctrl} (m x : Nat)
  (X Y : NSet) (ed : Nat → Nat) (hx : X.mem x = false)
  (h₁ : ((NSet.single x).union X).Disjoint Y)
  (i₁ :
    ∀ (y y' : Nat),
      ((NSet.single x).union X).mem y = true →
        ((NSet.single x).union X).mem y' = true →
          ed y = ed y' → y = y') :
  (Big.closure m ((NSet.single x).union X) Y ed h₁ i₁).Same
    ((Big.closure m X Y ed ⋯ ⋯).tensor (Big.closure1 x (ed x)) ⋯ ⋯ ⋯)

theorem closureSnoc_derived {Ctrl : Type}
  {S : Bigraph.Sig Ctrl} (m x : Nat)
  (X Y : NSet) (ed : Nat → Nat)
  (hx : X.mem x = false)
  (h₁ :
    ((NSet.single x).union X).Disjoint Y)
  (i₁ :
    ∀ (y y' : Nat),
      ((NSet.single x).union X).mem y =
          true →
        ((NSet.single x).union X).mem y' =
            true →
          ed y = ed y' → y = y') :
  (Big.closure m ((NSet.single x).union X)
        Y ed h₁ i₁).Same
    ((Big.closure m X Y ed ⋯ ⋯).tensor
      (Big.closure1 x (ed x)) ⋯ ⋯ ⋯)

`Big.closureSnoc` with only the three proper hypotheses. PROVED.

theoremdefined in Bigraph/Concrete/Wiring.lean

complete

theorem closure_same_id_tensor {Ctrl : Type} {S : Bigraph.Sig Ctrl} (m : Nat)
  (X Y : NSet) (ed : Nat → Nat) (hXY : X.Disjoint Y)
  (hinj :
    ∀ (x x' : Nat),
      X.mem x = true → X.mem x' = true → ed x = ed x' → x = x')
  (h :
    (Big.id { width := m, names := NSet.empty }).L.Disjoint
      (Big.closureW X Y ed hXY hinj).L)
  (hX : NSet.empty.Disjoint (X.union Y)) (hY : NSet.empty.Disjoint Y) :
  (Big.closure m X Y ed hXY hinj).Same
    ((Big.id { width := m, names := NSet.empty }).tensor
      (Big.closureW X Y ed hXY hinj) h hX hY)

theorem closure_same_id_tensor {Ctrl : Type}
  {S : Bigraph.Sig Ctrl} (m : Nat)
  (X Y : NSet) (ed : Nat → Nat)
  (hXY : X.Disjoint Y)
  (hinj :
    ∀ (x x' : Nat),
      X.mem x = true →
        X.mem x' = true →
          ed x = ed x' → x = x')
  (h :
    (Big.id
            { width := m,
              names :=
                NSet.empty }).L.Disjoint
      (Big.closureW X Y ed hXY hinj).L)
  (hX : NSet.empty.Disjoint (X.union Y))
  (hY : NSet.empty.Disjoint Y) :
  (Big.closure m X Y ed hXY hinj).Same
    ((Big.id
          { width := m,
            names := NSet.empty }).tensor
      (Big.closureW X Y ed hXY hinj) h hX
      hY)

**The bigraph-level closure is `id_⟨m,∅⟩ ⊗ ⟨id₀, /X ⊗ id_Y⟩`**: the width
`m` of `Big.closure` is a tensor with an identity. Widths `m + 0` are `m`
by computation; the name sets are compared by `Big.Same`.

Theorem4.3.7

Statement uses 2

Statement dependency previews

Preview

Definition 4.3.3

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 0✓L∃∀N

The merge with names is the tensor of the merge without names and an identity. For every m and X, the right side being defined,

\mathrm{merge}_m^X \doteq \mathrm{merge}_m^{\emptyset} \otimes \mathrm{id}_{\langle 0, X \rangle} .

Rests on NEW: Big.Same; not audited: Big, LiG.Disjoint, NSet.Disjoint, NSet.empty.

Lean code for Theorem4.3.7●3 declarations

theoremdefined in Bigraph/Concrete/Wiring.lean

complete

theorem mergeId {Ctrl : Type} (S : Bigraph.Sig Ctrl) : Big.MergeIdStatement S

theorem mergeId {Ctrl : Type}
  (S : Bigraph.Sig Ctrl) :
  Big.MergeIdStatement S

**The merge law, PROVED.**

defdefined in Bigraph/Concrete/Wiring.lean

complete

def MergeIdStatement {Ctrl : Type} (S : Bigraph.Sig Ctrl) : Prop

def MergeIdStatement {Ctrl : Type}
  (S : Bigraph.Sig Ctrl) : Prop

**The merge law**: `mergeN m X ≐ mergeN m ∅ ⊗ id_⟨0,X⟩`.

theoremdefined in Bigraph/Concrete/Wiring.lean

complete

theorem mergeId_derived {Ctrl : Type} (S : Bigraph.Sig Ctrl) (m : Nat)
  (X : NSet) :
  ∃ h hX,
    (Big.mergeN m X).Same
      ((Big.mergeN m NSet.empty).tensor
        (Big.id { width := 0, names := X }) h hX hX)

theorem mergeId_derived {Ctrl : Type}
  (S : Bigraph.Sig Ctrl) (m : Nat)
  (X : NSet) :
  ∃ h hX,
    (Big.mergeN m X).Same
      ((Big.mergeN m NSet.empty).tensor
        (Big.id
          { width := 0, names := X })
        h hX hX)

The definedness conditions of the right side always hold.