# Theory Example_One

    (*  File:       Example_One.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 One: Car Identity›

    theory Example_One
      imports Car_Identity
    begin

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

    text ‹
      For now squiggle will just identify some arbitrarily-chosen pairs; TODO: some semantic
      backing for this?
    ›

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

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

    definition coext⇩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 ⌋⌋)"

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

    text ‹Co-extension 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 1 captioned
        ‹The Car manufacturer and Supplier both want to build the same car,
         thus their respective modeling starts with the most basic abstraction,
         i.e., a \<^latex>‹\emph{Car}››.
    ›

    text ‹\<^latex>‹
    \begin{lstlisting}[language=myOCL, mathescape,
      caption={\mapping{1}{1} consistency specification}]
    context manufacturer::Car
    inv: Supplier::Car.allInstances()
        -> select(c|c $\sim$ self)
        -> size() = 1
    \end{lstlisting}
    ››

    definition One_to_One⇩i⇩n⇩v :: "Car2 ⇒ Boolean" where
      "One_to_One⇩i⇩n⇩v (self) ≡ Car1
        .allInstances()->select⇩S⇩e⇩t(c | c ∼ self)
               ->size⇩S⇩e⇩t() ≜ 𝟭"

    subsection ‹Proof Skeleton›

    (* Skeleton for showing it for arbitrary cars *)
    lemma one_to_one⇩l⇩e⇩m⇩m⇩a:
      fixes a :: "Car2"
      shows "τ ⊨ One_to_One⇩i⇩n⇩v a"
    proof -
      obtain b :: "Car1" where "{b} =
        {x. (τ ⊨ (Car1 .allInstances()->includes⇩S⇩e⇩t(x)))
                ∧ (τ ⊨ (x ∼⇩c⇩a⇩r a))}"
        sorry (*\<proof>*) ✐‹tag invisible›
      hence "τ ⊨ (Car1 .allInstances()
                 ->select⇩S⇩e⇩t(c | c ∼ a) ≐ Set{b})"
        unfolding UML_Set.OclSelect_def
        sorry (*\<proof>*) ✐‹tag invisible›
      moreover have "τ ⊨ (Set{b}->size⇩S⇩e⇩t() ≜ 𝟭)"
        sorry (*\<proof>*) ✐‹tag invisible›
      ultimately have
        "τ ⊨ (Car1 .allInstances()->select⇩S⇩e⇩t(c | c ∼ a)
                    ->size⇩S⇩e⇩t() ≜ 𝟭)"
        using UML_Set.cp_OclSize
        sorry (*\<proof>*) ✐‹tag invisible›
      thus ?thesis unfolding One_to_One⇩i⇩n⇩v_def
        by simp
    qed

    end