# Theory Example_Three

    (*  File:       Example_Three.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 ‹Specification Three: Message Bus›

    theory Example_Three
      imports Message_Bus
    begin

    (* TODO: this fixes a bug in OCL, go bother Achim Brucker about it & send him a patch *)
    notation   OclFirst   ("_->first⇩S⇩e⇩q'(')")

    subsection ‹Consistency Notion: The meaning of the ‹∼› operator›

    definition correspondences⇩c⇩a⇩r :: "(𝒯⇩C⇩a⇩r⇩1 × 𝒯⇩C⇩a⇩r⇩2) set"
            ("∼⇩c⇩a⇩r" 100) where
      "correspondences⇩c⇩a⇩r ≡ {(car1⇩1, car2⇩1), (car1⇩2, car2⇩2)}"

    definition correspondences⇩m⇩b :: "(𝒯⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1 × 𝒯⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2) set"
            ("∼⇩m⇩b" 100) where
      "correspondences⇩m⇩b ≡ {(mb1⇩1, mb2⇩1), (mb1⇩2, mb2⇩2)}"

    consts squiggle :: "[(𝔄, 'α option option) val,(𝔄, 'β option option) val] ⇒ Boolean"
            (infixl "∼" 100)

    definition squiggle⇩c⇩a⇩r :: "[Car1, Car2] ⇒ Boolean" (infixl "∼⇩c⇩a⇩r" 100) where
      [code_unfold]: "a ∼⇩c⇩a⇩r b ≡ (λ τ :: 𝔄 st.
                          ⌊⌊ (⌈⌈a τ⌉⌉, ⌈⌈b τ⌉⌉) ∈ correspondences⇩c⇩a⇩r ⌋⌋)"

    definition squiggle⇩m⇩b :: "[MessageBus1, MessageBus2] ⇒ Boolean" (infixl "∼⇩m⇩b" 100) where
      [code_unfold]: "a ∼⇩m⇩b b ≡ (λ τ :: 𝔄 st. ⌊⌊ (⌈⌈a τ⌉⌉, ⌈⌈b τ⌉⌉) ∈ ∼⇩m⇩b ⌋⌋)"

    overloading squiggle ≡ "squiggle :: [Car1, Car2] ⇒ Boolean"
    begin
      definition squiggle⇩c⇩a⇩r [code_unfold]: "(a::Car1) ∼ (b::Car2) ≡ a ∼⇩c⇩a⇩r b"
    end
    overloading squiggle ≡ "squiggle :: [MessageBus1, MessageBus2] ⇒ Boolean"
    begin
      definition squiggle⇩m⇩b[code_unfold]:
        "(a::MessageBus1) ∼ (b::MessageBus2) ≡ a ∼⇩m⇩b b"
    end

    text ‹Squiggle behaves as expected›

    Assert "⋀ σ':: 𝔄 state. (σ', σ') ⊨ x⇩c⇩a⇩r⇩1⇩_⇩1 ∼ x⇩c⇩a⇩r⇩2⇩_⇩1"
    Assert "⋀ σ':: 𝔄 state. (σ', σ') ⊨ x⇩c⇩a⇩r⇩1⇩_⇩2 ∼ x⇩c⇩a⇩r⇩2⇩_⇩2"
    Assert "⋀ σ':: 𝔄 state. (σ', σ') ⊨ not (x⇩c⇩a⇩r⇩1⇩_⇩1 ∼ x⇩c⇩a⇩r⇩2⇩_⇩2)"
    Assert "⋀ σ':: 𝔄 state. (σ', σ') ⊨ not (x⇩c⇩a⇩r⇩1⇩_⇩2 ∼ x⇩c⇩a⇩r⇩2⇩_⇩1)"

    subsection ‹Invariant›

    text ‹
      The following concerns Figure 6 captioned
        ‹The \<^latex>‹\emph{MessageBus}› is modeled explicitly,
        as it is too complex to be described by a simple type like
        String (1-n on model)›.
    ›

    text ‹\<^latex>‹
    \begin{lstlisting}[language=myOCL, mathescape, caption={\mapping{1}{n} consisteny specification}]
    context manufacturer::MessageBus
    inv: let mb:Supplier::MessageBus
        = self.select($\sim$) in mb.ecu
        -> forAll(e|e.prot = self.prot)
    \end{lstlisting}
    ››

    definition One_to_N⇩i⇩n⇩v :: "MessageBus1 ⇒ Boolean" where
      "One_to_N⇩i⇩n⇩v (self) ≡
        let mb = MessageBus2 .allInstances()
                  ->select⇩S⇩e⇩t(m| self ∼ m)
                  ->asSequence⇩S⇩e⇩t()->first⇩S⇩e⇩q()
        in (mb .ecu⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2 ->forAll⇩S⇩e⇩t(e|
          e .prot⇩E⇩C⇩U⇩2 ≜ (self .prot⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1)))"

    subsection ‹Proof Skeleton›

    (* Skeleton for showing it for arbitrary message buses *)
    lemma one_to_n⇩l⇩e⇩m⇩m⇩a:
      fixes a :: "MessageBus1"
      shows "τ ⊨ One_to_N⇩i⇩n⇩v a"
    proof -
      obtain b :: MessageBus2 where
        "τ ⊨ (MessageBus2 .allInstances()
                   ->includes⇩S⇩e⇩t(b))" and
          "τ ⊨ a ∼⇩m⇩b b"
        sorry (*\<proof>*) ✐‹tag invisible›
      from ‹τ ⊨ a ∼⇩m⇩b b› have "τ ⊨ a ∼ b"
        by (simp add: squiggle⇩m⇩b)
      moreover {
        have "∀ e. (τ ⊨ (b .ecu⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2->includes⇩S⇩e⇩t(e)))
              ⟶ (τ ⊨ (e .prot⇩E⇩C⇩U⇩2 ≜ (a .prot⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1)))"
          sorry (*\<proof>*) ✐‹tag invisible›
        hence "τ ⊨ (b .ecu⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2->forAll⇩S⇩e⇩t(e |
                  e .prot⇩E⇩C⇩U⇩2 ≜ (a .prot⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1)))"
          sorry (*\<proof>*) ✐‹tag invisible›
      }
      ultimately show ?thesis
        sorry (*\<proof>*) ✐‹tag invisible›
    qed

    end