Port Definitions and Connection Compatibility

Defines PortDef (typed, directed port), Conjugation (conjugation relation), and compatible — a decidable proposition for port-to-port connection compatibility.

structure VerifiedMBSE.Core.PortDef : Type

PortDef: port definition adding a flow type to a directed feature.

• feature : DirectedFeature
• flowType : KerMLType

def VerifiedMBSE.Core.instReprPortDef.repr : PortDef → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance VerifiedMBSE.Core.instReprPortDef : Repr PortDef

Equations

• VerifiedMBSE.Core.instReprPortDef = { reprPrec := VerifiedMBSE.Core.instReprPortDef.repr }

def VerifiedMBSE.Core.PortDef.conj (p : PortDef) : PortDef

PortDef conjugation: inverts direction while preserving the flow type.

Equations

• p.conj = { feature := p.feature.conj, flowType := p.flowType }

theorem VerifiedMBSE.Core.PortDef.conj_involution (p : PortDef) : p.conj.conj = p

PortDef conjugation is an involution.

structure VerifiedMBSE.Core.Conjugation : Type

KerML Conjugation relation: A's conjugate equals B. Type-theoretically corresponds to the A and A⊥ relation in linear logic.

• original : KerMLType
• conjugated : KerMLType

@[implicit_reducible]

instance VerifiedMBSE.Core.instReprConjugation : Repr Conjugation

Equations

• VerifiedMBSE.Core.instReprConjugation = { reprPrec := VerifiedMBSE.Core.instReprConjugation.repr }

def VerifiedMBSE.Core.instReprConjugation.repr : Conjugation → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def VerifiedMBSE.Core.compatible (a b : KerMLType) : Prop

Port compatibility: A and B are connectable ⟺ B is the conjugate of A.

Equations

• VerifiedMBSE.Core.compatible a b = ∃ (c : VerifiedMBSE.Core.Conjugation), c.original = a ∧ c.conjugated = b

theorem VerifiedMBSE.Core.compatible_symm {a b : KerMLType} (h : compatible a b) : compatible b a

Compatibility is symmetric: A and B are compatible ⟺ B and A are compatible.

theorem VerifiedMBSE.Core.compatible_conj_involution (a b : KerMLType) (h : compatible a b) : compatible b a

Involutivity: compatible a b → compatible b a (alias for compatible_symm).