# Theory OCL_Reactions

    (*  File:       OCL_Reactions.thy
        Copyright   2026  Ludwig-Maximilians-Universität (LMU) München
    *)
    ✐‹creator "Michael Kirsten, Ludwig-Maximilians-Universität München"›
    ✐‹contributor "Terru Stübinger, Karlsruhe Institute of Technology (KIT)"›
    section ‹Brake System Specification›

    theory OCL_Reactions
      imports Brake_System
    begin

    subsection ‹Semantics of Model Correspondence›

    text ‹Notation fix for ‹Featherweight_OCL›'s operation ‹first⇩S⇩e⇩q››
    notation OclFirst (‹_->first⇩S⇩e⇩q'(')›)

    subsubsection ‹Co-Extension Operator›

    text ‹"Generic" empty co-extension›
    definition coext⇩g⇩e⇩n⇩e⇩r⇩i⇩c (infixl "∼⇩g⇩e⇩n⇩e⇩r⇩i⇩c" 100) where
      "a ∼⇩g⇩e⇩n⇩e⇩r⇩i⇩c (b::(𝔄,⟨⟨'b⟩⇩⊥⟩⇩⊥) val) ≡ (λ τ :: 𝔄 st. ⌊⌊ (⌈⌈a τ⌉⌉, ⌈⌈b τ⌉⌉) ∈ {} ⌋⌋)"

    text ‹Concrete correspondences for ‹BrakeComponent›-to-‹Namespace››
    definition correspondences⇩b⇩c⇩n⇩s :: "(𝒯⇩B⇩r⇩a⇩k⇩e⇩C⇩o⇩m⇩p⇩o⇩n⇩e⇩n⇩t × 𝒯⇩N⇩a⇩m⇩e⇩s⇩p⇩a⇩c⇩e) set"
      where "correspondences⇩b⇩c⇩n⇩s ≡ {(brakecomponent⇩1, namespace⇩1),
                                  (brakecomponent⇩2, namespace⇩2)}"

    text ‹Concrete correspondences for ‹Namespace›-to-‹BrakeComponent››
    definition correspondences⇩n⇩s⇩b⇩c :: "(𝒯⇩N⇩a⇩m⇩e⇩s⇩p⇩a⇩c⇩e × 𝒯⇩B⇩r⇩a⇩k⇩e⇩C⇩o⇩m⇩p⇩o⇩n⇩e⇩n⇩t) set"
      where "correspondences⇩n⇩s⇩b⇩c ≡ {(namespace⇩1, brakecomponent⇩1),
                                  (namespace⇩2, brakecomponent⇩2)}"

    text ‹Co-extension operators for previously defined correspondences›
    definition coext⇩b⇩c⇩n⇩s :: "[BrakeComponent, Namespace] ⇒ Boolean"
        (infixl "∼⇩b⇩c⇩n⇩s" 100) where "a ∼⇩b⇩c⇩n⇩s b ≡
            (λ τ :: 𝔄 st. ⌊⌊ (⌈⌈a τ⌉⌉, ⌈⌈b τ⌉⌉) ∈ correspondences⇩b⇩c⇩n⇩s ⌋⌋)"

    definition coext⇩n⇩s⇩b⇩c :: "[Namespace, BrakeComponent] ⇒ Boolean"
        (infixl "∼⇩n⇩s⇩b⇩c" 100) where "a ∼⇩n⇩s⇩b⇩c b ≡
            (λ τ :: 𝔄 st. ⌊⌊ (⌈⌈a τ⌉⌉, ⌈⌈b τ⌉⌉) ∈ correspondences⇩n⇩s⇩b⇩c ⌋⌋)"

    text ‹Co-extension constant for overloading›
    consts squiggle :: "[(𝔄, 'α option option) val,(𝔄, 'β option option) val]
                            ⇒ Boolean" (infixl "∼" 100)

    overloading squiggle ≡ "squiggle :: [BrakeComponent, Namespace] ⇒ Boolean"
    begin
      definition squiggle⇩b⇩c⇩n⇩s[code_unfold]:
        "(a::BrakeComponent) ∼ (b::Namespace) ≡ a ∼⇩b⇩c⇩n⇩s b"
    end
    overloading squiggle ≡ "squiggle :: [Namespace, BrakeComponent] ⇒ Boolean"
    begin
      definition squiggle⇩n⇩s⇩b⇩c[code_unfold]:
        "(a::Namespace) ∼ (b::BrakeComponent) ≡ a ∼⇩n⇩s⇩b⇩c b"
    end

    subsubsection ‹Exemplary Assertions›

    Assert "⋀ σ':: 𝔄 state. (σ', σ') ⊨ x⇩b⇩r⇩a⇩k⇩e⇩c⇩o⇩m⇩p⇩o⇩n⇩e⇩n⇩t⇩_⇩1 ∼ x⇩n⇩a⇩m⇩e⇩s⇩p⇩a⇩c⇩e⇩_⇩1"
    Assert "⋀ σ':: 𝔄 state. (σ', σ') ⊨ x⇩n⇩a⇩m⇩e⇩s⇩p⇩a⇩c⇩e⇩_⇩1 ∼ x⇩b⇩r⇩a⇩k⇩e⇩c⇩o⇩m⇩p⇩o⇩n⇩e⇩n⇩t⇩_⇩1"

    Assert "⋀ σ':: 𝔄 state. (σ', σ') ⊨ x⇩b⇩r⇩a⇩k⇩e⇩c⇩o⇩m⇩p⇩o⇩n⇩e⇩n⇩t⇩_⇩2 ∼ x⇩n⇩a⇩m⇩e⇩s⇩p⇩a⇩c⇩e⇩_⇩2"
    Assert "⋀ σ':: 𝔄 state. (σ', σ') ⊨ x⇩n⇩a⇩m⇩e⇩s⇩p⇩a⇩c⇩e⇩_⇩2 ∼ x⇩b⇩r⇩a⇩k⇩e⇩c⇩o⇩m⇩p⇩o⇩n⇩e⇩n⇩t⇩_⇩2"

    Assert "⋀ σ':: 𝔄 state. (σ', σ') ⊨ not (x⇩b⇩r⇩a⇩k⇩e⇩c⇩o⇩m⇩p⇩o⇩n⇩e⇩n⇩t⇩_⇩1 ∼ x⇩n⇩a⇩m⇩e⇩s⇩p⇩a⇩c⇩e⇩_⇩2)"
    Assert "⋀ σ':: 𝔄 state. (σ', σ') ⊨ not (x⇩n⇩a⇩m⇩e⇩s⇩p⇩a⇩c⇩e⇩_⇩2 ∼ x⇩b⇩r⇩a⇩k⇩e⇩c⇩o⇩m⇩p⇩o⇩n⇩e⇩n⇩t⇩_⇩1)"

    Assert "⋀ σ':: 𝔄 state. (σ', σ') ⊨ not (x⇩b⇩r⇩a⇩k⇩e⇩c⇩o⇩m⇩p⇩o⇩n⇩e⇩n⇩t⇩_⇩2 ∼ x⇩n⇩a⇩m⇩e⇩s⇩p⇩a⇩c⇩e⇩_⇩1)"
    Assert "⋀ σ':: 𝔄 state. (σ', σ') ⊨ not (x⇩n⇩a⇩m⇩e⇩s⇩p⇩a⇩c⇩e⇩_⇩1 ∼ x⇩b⇩r⇩a⇩k⇩e⇩c⇩o⇩m⇩p⇩o⇩n⇩e⇩n⇩t⇩_⇩2)"

    subsection ‹CAD Model One Corresponding Element (1)›

    text ‹\<^latex>‹
    \begin{lstlisting}[language=myOCL, mathescape,
      caption={CAD Model One Corresponding Element}]
    context brakesystem::Brakesystem
    inv: CAD::CADModel.allInstances()
        -> select(c | c $\sim$ self)
        -> size() = 1
    \end{lstlisting}
    ››

    definition Corr_CAD_Models⇩i⇩n⇩v :: "CAD_Model ⇒ Boolean" where
     "Corr_CAD_Models⇩i⇩n⇩v (self) ≡
        Namespace .allInstances()->select⇩S⇩e⇩t(m | self ∼ m)->size⇩S⇩e⇩t() ≜ 𝟭"

    subsection ‹Brake Component's Corresponding IDs Identical (2)›

    text ‹\<^latex>‹
    \begin{lstlisting}[language=myOCL, mathescape,
      caption={Article's Listing 7}]
    context brakesystem::BrakeComponent
    inv: self.select($\sim$) ->
        forAll (c | c.oclIsTypeOf(CAD::Namespace)
            and self.select($\sim$) -> size() = 1
            and self.id = self.select($\sim$) -> first().id
    \end{lstlisting}
    ››

    definition Id_IDs⇩i⇩n⇩v :: "BrakeComponent ⇒ Boolean" where
      "Id_IDs⇩i⇩n⇩v (self) ≡
          Namespace .allInstances()->select⇩S⇩e⇩t(m | self ∼ m)->size⇩S⇩e⇩t() ≜ 𝟭 and
            (Namespace .allInstances()->select⇩S⇩e⇩t(m | self ∼ m)->asSequence⇩S⇩e⇩t()
              ->first⇩S⇩e⇩q().id⇩N⇩a⇩m⇩e⇩s⇩p⇩a⇩c⇩e ≜ (self .id⇩B⇩r⇩a⇩k⇩e⇩C⇩o⇩m⇩p⇩o⇩n⇩e⇩n⇩t))"

    subsection ‹Brake Component One Corresponding ID (3)›

    text ‹\<^latex>‹
    \begin{lstlisting}[language=myOCL, mathescape,
      caption={Brake Component One Corresponding ID}]
    context brakesystem::BrakeComponent
    inv: self.id = self.select($\sim$) -> first().id
    \end{lstlisting}
    ››

    definition Corr_IDs⇩i⇩n⇩v :: "BrakeComponent ⇒ Boolean" where
      "Corr_IDs⇩i⇩n⇩v (self) ≡ Namespace .allInstances()->select⇩S⇩e⇩t(m | self ∼ m)
          ->asSequence⇩S⇩e⇩t()->first⇩S⇩e⇩q().id⇩N⇩a⇩m⇩e⇩s⇩p⇩a⇩c⇩e ≜ (self .id⇩B⇩r⇩a⇩k⇩e⇩C⇩o⇩m⇩p⇩o⇩n⇩e⇩n⇩t)"

    subsection ‹Brake Component's Corresponding OEM Numbers (4)›

    text ‹\<^latex>‹
    \begin{lstlisting}[language=myOCL, mathescape,
      caption={Article's Listing 8}]
    context brakesystem :: BrakeComponent
    inv: self.select($\sim$).parameters ->
        select (p | p.name = "OEM Number").value =
            self.OEM_Number
    \end{lstlisting}
    ››

    definition OEM_number_String ::"String" (‹𝗈𝖾𝗆 𝗇𝗎𝗆𝖻𝖾𝗋›) where
      "𝗈𝖾𝗆 𝗇𝗎𝗆𝖻𝖾𝗋 = (λ _ . ⌊⌊''OEM_number''⌋⌋)"

    definition Id_OEMs⇩i⇩n⇩v :: "BrakeComponent ⇒ Boolean" where
      "Id_OEMs⇩i⇩n⇩v (self) ≡
        ((Namespace .allInstances()->select⇩S⇩e⇩t(m|self ∼ m)
            ->asSequence⇩S⇩e⇩t()->first⇩S⇩e⇩q().parameters
            ->select⇩S⇩e⇩t(c | c .name⇩P⇩a⇩r⇩a⇩m⇩e⇩t⇩e⇩r ≐ 𝗈𝖾𝗆 𝗇𝗎𝗆𝖻𝖾𝗋)
            ->asSequence⇩S⇩e⇩t()->first⇩S⇩e⇩q()
            .oclAsType(NumericParameter) .value⇩N⇩u⇩m⇩e⇩r⇩i⇩c⇩P⇩a⇩r⇩a⇩m⇩e⇩t⇩e⇩r))
          ≜ ((self .OEM_number⇩B⇩r⇩a⇩k⇩e⇩C⇩o⇩m⇩p⇩o⇩n⇩e⇩n⇩t)->oclAsType⇩I⇩n⇩t(Real))"

    subsection ‹Brake Component's Corresp. Specification Types (5)›

    text ‹\<^latex>‹
    \begin{lstlisting}[language=myOCL, mathescape,
      caption={Article's Listing 9}]
    context brakesystem::BrakeComponent
    inv: self.select($\sim$).parameters ->
        select(p | p.name = "Specification Type").value =
            self.Specification_Type
    \end{lstlisting}
    ››

    definition SpecificationType_String ::"String" (‹𝗌𝗉𝖾𝖼𝗂𝖿𝗂𝖼𝖺𝗍𝗂𝗈𝗇 𝗍𝗒𝗉𝖾›) where
      "𝗌𝗉𝖾𝖼𝗂𝖿𝗂𝖼𝖺𝗍𝗂𝗈𝗇 𝗍𝗒𝗉𝖾 = (λ _ . ⌊⌊''specificationType''⌋⌋)"

    definition Id_Specs⇩i⇩n⇩v :: "BrakeComponent ⇒ Boolean" where
      "Id_Specs⇩i⇩n⇩v (self) ≡
        (Namespace .allInstances()->select⇩S⇩e⇩t(m|self ∼ m)
          ->asSequence⇩S⇩e⇩t()->first⇩S⇩e⇩q().parameters
            ->select⇩S⇩e⇩t(c | c .name⇩P⇩a⇩r⇩a⇩m⇩e⇩t⇩e⇩r ≐ 𝗌𝗉𝖾𝖼𝗂𝖿𝗂𝖼𝖺𝗍𝗂𝗈𝗇 𝗍𝗒𝗉𝖾)
              ->asSequence⇩S⇩e⇩t()->first⇩S⇩e⇩q().oclAsType(StringParameter)
              .value⇩S⇩t⇩r⇩i⇩n⇩g⇩P⇩a⇩r⇩a⇩m⇩e⇩t⇩e⇩r) ≜ (self .specificationType⇩B⇩r⇩a⇩k⇩e⇩C⇩o⇩m⇩p⇩o⇩n⇩e⇩n⇩t)"

    subsection ‹Brake Component's Corresp. Fitting Positions (6)›

    text ‹\<^latex>‹
    \begin{lstlisting}[language=myOCL, mathescape,
      caption={Article's Listing 10}]
    context brakesystem::BrakeComponent
    inv: self.select($\sim$).parameters ->
        select(p | p.name = "Fitting Position").value =
            self.Fitting_Position
    \end{lstlisting}
    ››

    definition FittingPosition_String ::"String" (‹𝖿𝗂𝗍𝗍𝗂𝗇𝗀 𝗉𝗈𝗌𝗂𝗍𝗂𝗈𝗇›) where
      "𝖿𝗂𝗍𝗍𝗂𝗇𝗀 𝗉𝗈𝗌𝗂𝗍𝗂𝗈𝗇 = (λ _ . ⌊⌊''fittingPosition''⌋⌋)"

    definition Id_Fitting⇩i⇩n⇩v :: "BrakeComponent ⇒ Boolean" where
      "Id_Fitting⇩i⇩n⇩v (self) ≡
        (Namespace .allInstances()->select⇩S⇩e⇩t(m|self ∼ m)
          ->asSequence⇩S⇩e⇩t()->first⇩S⇩e⇩q().parameters
              ->select⇩S⇩e⇩t(c | c .name⇩P⇩a⇩r⇩a⇩m⇩e⇩t⇩e⇩r ≐ 𝖿𝗂𝗍𝗍𝗂𝗇𝗀 𝗉𝗈𝗌𝗂𝗍𝗂𝗈𝗇)
              ->asSequence⇩S⇩e⇩t()->first⇩S⇩e⇩q().oclAsType(StringParameter)
              .value⇩S⇩t⇩r⇩i⇩n⇩g⇩P⇩a⇩r⇩a⇩m⇩e⇩t⇩e⇩r) ≜ (self .fittingPosition⇩B⇩r⇩a⇩k⇩e⇩C⇩o⇩m⇩p⇩o⇩n⇩e⇩n⇩t)"

    subsection ‹Proof Skeletons›

    lemma corr_cad_models⇩l⇩e⇩m⇩m⇩a:
    ― ‹Skeleton for proving the invariant (1) on arbitrary ‹CAD_Model›s›
      fixes a :: "CAD_Model"
      shows "τ ⊨ Corr_CAD_Models⇩i⇩n⇩v a"
    proof (unfold Corr_CAD_Models⇩i⇩n⇩v_def)
      obtain ms :: "Namespace set" where
        "ms = {x. (τ ⊨ (Namespace .allInstances()->includes⇩S⇩e⇩t(x)))
                        ∧ (τ ⊨ a ∼ x)}"
        by presburger
      with σ_def have "card ms = 1"
        sorry (* \<proof> *) ✐‹tag invisible›
      then obtain m :: "Namespace" where
        "τ ⊨ (Namespace .allInstances()->select⇩S⇩e⇩t(c | c ∼ a) ≐ Set{m})"
        unfolding UML_Set.OclSelect_def
        sorry (* \<proof> *) ✐‹tag invisible›
      moreover with ‹card ms = 1› have "τ ⊨ (Set{m}->size⇩S⇩e⇩t() ≜ 𝟭)"
        sorry (* \<proof> *) (* \<proof> *) ✐‹tag invisible›
      ultimately show
       "τ ⊨ (Namespace .allInstances()->select⇩S⇩e⇩t(m | a ∼ m)->size⇩S⇩e⇩t() ≜ 𝟭)"
        using UML_Set.cp_OclSize
        sorry (* \<proof> *) ✐‹tag invisible›
    qed

    lemma id_ids⇩l⇩e⇩m⇩m⇩a:
    ― ‹Skeleton for proving the invariant (3) on arbitrary ‹BrakeComponent›s›
      fixes a :: "BrakeComponent"
      shows "τ ⊨ Id_IDs⇩i⇩n⇩v a"
    proof (unfold Id_IDs⇩i⇩n⇩v_def)
      have single:
        "τ ⊨ (Namespace .allInstances()->select⇩S⇩e⇩t(m | a ∼ m)->size⇩S⇩e⇩t() ≜ 𝟭)"
      proof -
        obtain ms :: "Namespace set" where "ms =
          {x. (τ ⊨ (Namespace .allInstances()->includes⇩S⇩e⇩t(x)))
                     ∧ (τ ⊨ a ∼ x)}"
          by presburger
        with σ_def have "card ms = 1"
          sorry (* \<proof> *) ✐‹tag invisible›
        then obtain m :: "Namespace" where
          "τ ⊨ (Namespace .allInstances()->select⇩S⇩e⇩t(c | c ∼ a) ≐ Set{m})"
          unfolding UML_Set.OclSelect_def
          sorry (* \<proof> *) ✐‹tag invisible›
        moreover with ‹card ms = 1›
        have "τ ⊨ (Set{m}->size⇩S⇩e⇩t() ≜ 𝟭)"
          sorry (* \<proof> *) ✐‹tag invisible›
        ultimately show
         "τ ⊨ (Namespace .allInstances()->select⇩S⇩e⇩t(m | a ∼ m)->size⇩S⇩e⇩t() ≜ 𝟭)"
          using UML_Set.cp_OclSize
          sorry (* \<proof> *) ✐‹tag invisible›
      qed
      moreover have "τ ⊨ (Namespace .allInstances()->select⇩S⇩e⇩t(m|a ∼ m)
          ->asSequence⇩S⇩e⇩t()->first⇩S⇩e⇩q().id⇩N⇩a⇩m⇩e⇩s⇩p⇩a⇩c⇩e ≜ (a .id⇩B⇩r⇩a⇩k⇩e⇩C⇩o⇩m⇩p⇩o⇩n⇩e⇩n⇩t))"
      proof -
        from single obtain m :: "Namespace" where
          "τ ⊨ (Namespace .allInstances()->select⇩S⇩e⇩t(m | a ∼ m) ≜ Set{m})"
          sorry (* \<proof> *) ✐‹tag invisible›
        moreover have "τ ⊨ (m .id⇩N⇩a⇩m⇩e⇩s⇩p⇩a⇩c⇩e ≜ (a .id⇩B⇩r⇩a⇩k⇩e⇩C⇩o⇩m⇩p⇩o⇩n⇩e⇩n⇩t))"
          sorry (* \<proof> *) ✐‹tag invisible›
        ultimately show
          "τ ⊨ (Namespace .allInstances()->select⇩S⇩e⇩t(m | a ∼ m)->asSequence⇩S⇩e⇩t()
                  ->first⇩S⇩e⇩q().id⇩N⇩a⇩m⇩e⇩s⇩p⇩a⇩c⇩e ≜ (a .id⇩B⇩r⇩a⇩k⇩e⇩C⇩o⇩m⇩p⇩o⇩n⇩e⇩n⇩t))"
          sorry (* \<proof> *) ✐‹tag invisible›
      qed
      thus "τ ⊨ (Namespace .allInstances()->select⇩S⇩e⇩t(m | a ∼ m)->size⇩S⇩e⇩t() ≜ 𝟭
              and (Namespace .allInstances()->select⇩S⇩e⇩t(m|a ∼ m)
                  ->asSequence⇩S⇩e⇩t()->first⇩S⇩e⇩q()
                .id⇩N⇩a⇩m⇩e⇩s⇩p⇩a⇩c⇩e ≜ (a .id⇩B⇩r⇩a⇩k⇩e⇩C⇩o⇩m⇩p⇩o⇩n⇩e⇩n⇩t)))"
        sorry (* \<proof> *) ✐‹tag invisible›
    qed

    lemma corr_ids⇩l⇩e⇩m⇩m⇩a:
    ― ‹Skeleton for proving the invariant (3) on arbitrary ‹BrakeComponent›s›
      fixes a :: "BrakeComponent"
      shows "τ ⊨ Corr_IDs⇩i⇩n⇩v a"
    proof (unfold Corr_IDs⇩i⇩n⇩v_def)
      from id_ids⇩l⇩e⇩m⇩m⇩a foundation10'
      have "τ ⊨ (Namespace .allInstances()->select⇩S⇩e⇩t(m|a ∼ m)->size⇩S⇩e⇩t() ≜ 𝟭)"
        unfolding Id_IDs⇩i⇩n⇩v_def
        by metis
      then obtain m :: "Namespace" where
        "τ ⊨ (Namespace .allInstances()->select⇩S⇩e⇩t(m | a ∼ m) ≜ Set{m})"
        sorry (* \<proof> *) ✐‹tag invisible›
      hence "τ ⊨ (Namespace .allInstances()->select⇩S⇩e⇩t(m | a ∼ m)
                    ->asSequence⇩S⇩e⇩t()->first⇩S⇩e⇩q() ≜ m)"
        sorry (* \<proof> *) ✐‹tag invisible›
      have "τ ⊨ (m .id⇩N⇩a⇩m⇩e⇩s⇩p⇩a⇩c⇩e ≜ (a .id⇩B⇩r⇩a⇩k⇩e⇩C⇩o⇩m⇩p⇩o⇩n⇩e⇩n⇩t))"
        sorry (* \<proof> *) ✐‹tag invisible›
      show
       "τ ⊨ (Namespace .allInstances()->select⇩S⇩e⇩t(m | a ∼ m)
              ->asSequence⇩S⇩e⇩t()->first⇩S⇩e⇩q().id⇩N⇩a⇩m⇩e⇩s⇩p⇩a⇩c⇩e
            ≜ (a .id⇩B⇩r⇩a⇩k⇩e⇩C⇩o⇩m⇩p⇩o⇩n⇩e⇩n⇩t))"
        sorry (* \<proof> *) ✐‹tag invisible›
    qed

    lemma id_oems⇩l⇩e⇩m⇩m⇩a:
    ― ‹Skeleton for proving the invariant (4) on arbitrary ‹BrakeComponent›s›
      fixes a :: "BrakeComponent"
      shows "τ ⊨ Id_OEMs⇩i⇩n⇩v a"
    proof (unfold Id_OEMs⇩i⇩n⇩v_def)
      from id_ids⇩l⇩e⇩m⇩m⇩a foundation10'
      have "τ ⊨ (Namespace .allInstances()->select⇩S⇩e⇩t(m|a ∼ m)->size⇩S⇩e⇩t() ≜ 𝟭)"
        unfolding Id_IDs⇩i⇩n⇩v_def
        by metis
      then obtain m :: "Namespace" where
        "τ ⊨ (Namespace .allInstances()->select⇩S⇩e⇩t(m | a ∼ m)
                ->asSequence⇩S⇩e⇩t()->first⇩S⇩e⇩q() ≜ m)"
        using StrongEq_L_sym StrongEq_L_trans StrongEq_refl
        by metis
      then obtain p :: "Parameter" where
         "τ ⊨ (m .parameters
            ->select⇩S⇩e⇩t(c | c .name⇩P⇩a⇩r⇩a⇩m⇩e⇩t⇩e⇩r ≐ 𝗈𝖾𝗆 𝗇𝗎𝗆𝖻𝖾𝗋) ≜ Set{p})"
        sorry (* \<proof> *) ✐‹tag invisible›
      moreover have "τ ⊨ (p .oclAsType(NumericParameter).value⇩N⇩u⇩m⇩e⇩r⇩i⇩c⇩P⇩a⇩r⇩a⇩m⇩e⇩t⇩e⇩r
                            ≜ (a .OEM_number⇩B⇩r⇩a⇩k⇩e⇩C⇩o⇩m⇩p⇩o⇩n⇩e⇩n⇩t->oclAsType⇩I⇩n⇩t(Real)))"
        sorry (* \<proof> *) ✐‹tag invisible›
      ultimately show
        "τ ⊨ (Namespace .allInstances()->select⇩S⇩e⇩t(m|a ∼ m)
              ->asSequence⇩S⇩e⇩t()->first⇩S⇩e⇩q().parameters
                ->select⇩S⇩e⇩t(c|c .name⇩P⇩a⇩r⇩a⇩m⇩e⇩t⇩e⇩r ≐ 𝗈𝖾𝗆 𝗇𝗎𝗆𝖻𝖾𝗋)
              ->asSequence⇩S⇩e⇩t()->first⇩S⇩e⇩q().oclAsType(NumericParameter)
          .value⇩N⇩u⇩m⇩e⇩r⇩i⇩c⇩P⇩a⇩r⇩a⇩m⇩e⇩t⇩e⇩r ≜ ((a .OEM_number⇩B⇩r⇩a⇩k⇩e⇩C⇩o⇩m⇩p⇩o⇩n⇩e⇩n⇩t)
                                    ->oclAsType⇩I⇩n⇩t(Real)))"
        sorry (* \<proof> *) ✐‹tag invisible›
    qed

    lemma id_specs⇩l⇩e⇩m⇩m⇩a:
    ― ‹Skeleton for proving the invariant (5) on arbitrary ‹BrakeComponent›s›
      fixes a :: "BrakeComponent"
      shows "τ ⊨ Id_Specs⇩i⇩n⇩v a"
    proof (unfold Id_Specs⇩i⇩n⇩v_def)
      from id_ids⇩l⇩e⇩m⇩m⇩a foundation10'
      have "τ ⊨ (Namespace .allInstances()->select⇩S⇩e⇩t(m|a ∼ m)->size⇩S⇩e⇩t() ≜ 𝟭)"
        unfolding Id_IDs⇩i⇩n⇩v_def
        by metis
      then obtain m :: "Namespace" where
        "τ ⊨ (Namespace .allInstances()->select⇩S⇩e⇩t(m | a ∼ m)
                ->asSequence⇩S⇩e⇩t()->first⇩S⇩e⇩q() ≜ m)"
        using StrongEq_refl foundation1
        by metis
      then obtain p :: "Parameter" where
         "τ ⊨ (m .parameters->select⇩S⇩e⇩t(c | c .name⇩P⇩a⇩r⇩a⇩m⇩e⇩t⇩e⇩r ≐ 𝗌𝗉𝖾𝖼𝗂𝖿𝗂𝖼𝖺𝗍𝗂𝗈𝗇 𝗍𝗒𝗉𝖾)
                  ≜ Set{p})"
        sorry (* \<proof> *) ✐‹tag invisible›
      moreover have "τ ⊨ (p .oclAsType(StringParameter).value⇩S⇩t⇩r⇩i⇩n⇩g⇩P⇩a⇩r⇩a⇩m⇩e⇩t⇩e⇩r
                            ≜ (a .specificationType⇩B⇩r⇩a⇩k⇩e⇩C⇩o⇩m⇩p⇩o⇩n⇩e⇩n⇩t))"
        sorry (* \<proof> *) ✐‹tag invisible›
      ultimately show
        "τ ⊨ (Namespace .allInstances()->select⇩S⇩e⇩t(m|a ∼ m)
          ->asSequence⇩S⇩e⇩t()->first⇩S⇩e⇩q().parameters
            ->select⇩S⇩e⇩t(c | c .name⇩P⇩a⇩r⇩a⇩m⇩e⇩t⇩e⇩r ≐ 𝗌𝗉𝖾𝖼𝗂𝖿𝗂𝖼𝖺𝗍𝗂𝗈𝗇 𝗍𝗒𝗉𝖾)
            ->asSequence⇩S⇩e⇩t()->first⇩S⇩e⇩q().oclAsType(StringParameter)
              .value⇩S⇩t⇩r⇩i⇩n⇩g⇩P⇩a⇩r⇩a⇩m⇩e⇩t⇩e⇩r ≜ (a .specificationType⇩B⇩r⇩a⇩k⇩e⇩C⇩o⇩m⇩p⇩o⇩n⇩e⇩n⇩t))"
        sorry (* \<proof> *) ✐‹tag invisible›
    qed

    lemma id_fitting⇩l⇩e⇩m⇩m⇩a:
    ― ‹Skeleton for proving the invariant (6) on arbitrary ‹BrakeComponent›s›
      fixes a :: "BrakeComponent"
      shows "τ ⊨ Id_Fitting⇩i⇩n⇩v a"
    proof (unfold Id_Fitting⇩i⇩n⇩v_def)
      from id_ids⇩l⇩e⇩m⇩m⇩a foundation10'
      have "τ ⊨ (Namespace .allInstances()->select⇩S⇩e⇩t(m|a ∼ m)->size⇩S⇩e⇩t() ≜ 𝟭)"
        unfolding Id_IDs⇩i⇩n⇩v_def
        by metis
      then obtain m :: "Namespace"
        where "τ ⊨ (Namespace .allInstances()->select⇩S⇩e⇩t(m | a ∼ m)
                      ->asSequence⇩S⇩e⇩t()->first⇩S⇩e⇩q() ≜ m)"
        sorry (* \<proof> *) ✐‹tag invisible›
      then obtain p :: "Parameter" where
         "τ ⊨ (m .parameters->select⇩S⇩e⇩t(c | c .name⇩P⇩a⇩r⇩a⇩m⇩e⇩t⇩e⇩r ≐ 𝖿𝗂𝗍𝗍𝗂𝗇𝗀 𝗉𝗈𝗌𝗂𝗍𝗂𝗈𝗇)
                ≜ Set{p})"
        sorry (* \<proof> *) ✐‹tag invisible›
      moreover have "τ ⊨ (p .oclAsType(StringParameter).value⇩S⇩t⇩r⇩i⇩n⇩g⇩P⇩a⇩r⇩a⇩m⇩e⇩t⇩e⇩r
                            ≜ (a .fittingPosition⇩B⇩r⇩a⇩k⇩e⇩C⇩o⇩m⇩p⇩o⇩n⇩e⇩n⇩t))"
        sorry (* \<proof> *) ✐‹tag invisible›
      ultimately show
        "τ ⊨ (Namespace .allInstances()->select⇩S⇩e⇩t(m|a ∼ m)
            ->asSequence⇩S⇩e⇩t()->first⇩S⇩e⇩q().parameters
            ->select⇩S⇩e⇩t(c | c .name⇩P⇩a⇩r⇩a⇩m⇩e⇩t⇩e⇩r ≐ 𝖿𝗂𝗍𝗍𝗂𝗇𝗀 𝗉𝗈𝗌𝗂𝗍𝗂𝗈𝗇)
            ->asSequence⇩S⇩e⇩t()->first⇩S⇩e⇩q().oclAsType(StringParameter)
              .value⇩S⇩t⇩r⇩i⇩n⇩g⇩P⇩a⇩r⇩a⇩m⇩e⇩t⇩e⇩r ≜ (a .fittingPosition⇩B⇩r⇩a⇩k⇩e⇩C⇩o⇩m⇩p⇩o⇩n⇩e⇩n⇩t))"
        sorry (* \<proof> *) ✐‹tag invisible›
    qed

    end