# Theory Example_Two

    (*  File:       Example_Two.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 Two: Car Component›

    theory Example_Two
      imports Car_Component
    begin

    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)}"

    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 ⌋⌋)"

    text ‹Here we can now make squiggle more concrete, by depending on the car's fields:›

    overloading squiggle ≡ "squiggle :: [Car1, Car2] ⇒ Boolean"
    begin
      definition squiggle⇩c⇩a⇩r[code_unfold]: "(a::Car1) ∼ (b::Car2) ≡
          (λ τ :: 𝔄 st. ⌊⌊ car1⇩V⇩I⇩N ⌈⌈a τ⌉⌉ = car2⇩V⇩I⇩N ⌈⌈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 2 captioned
        ‹Cars with structural features, like \<^latex>‹\emph{VIN}›.›
    ›

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

    definition One_to_One_Refined⇩i⇩n⇩v :: "Car2 ⇒ Boolean" where
      "One_to_One_Refined⇩i⇩n⇩v (self) ≡
         Car1 .allInstances()
          ->select⇩S⇩e⇩t(c | c .vin⇩C⇩a⇩r⇩1 ≜ (self .vin⇩C⇩a⇩r⇩2))
          ->size⇩S⇩e⇩t() ≜ 𝟭"

    subsection ‹Proof Skeleton›

    lemma one_to_one_refined⇩l⇩e⇩m⇩m⇩a:
      fixes a :: "Car2"
      shows "τ ⊨ One_to_One_Refined⇩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 "τ ⊨ b ∼ a"
        sorry (*\<proof>*) ✐‹tag invisible›
      hence "τ ⊨ (b .vin⇩C⇩a⇩r⇩1 ≜ (a .vin⇩C⇩a⇩r⇩2))"
        sorry (*\<proof>*) ✐‹tag invisible›
      hence "τ ⊨ (Car1 .allInstances()
                ->select⇩S⇩e⇩t(c | c .vin⇩C⇩a⇩r⇩1 ≜ (a .vin⇩C⇩a⇩r⇩2))
                ≐ Set{b})"
        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 .vin⇩C⇩a⇩r⇩1 ≜ (a .vin⇩C⇩a⇩r⇩2))
            ->size⇩S⇩e⇩t() ≜ 𝟭)"
        sorry (*\<proof>*) ✐‹tag invisible›
      thus ?thesis unfolding One_to_One_Refined⇩i⇩n⇩v_def
        by simp
    qed

    end