# Theory Car_Identity

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

    theory Car_Identity
      imports "Featherweight_OCL.UML_Main"
    begin

    text ‹
      Featherweight OCL can only reason about one meta-model at a time.
      So in the following, we will have one model containing classes Car1 and Car2,
      but pretend they are separate.

      Note: This should correspond to Figure 1 from the paper.
    ›

    subsection ‹Types›

    datatype 𝒯⇩C⇩a⇩r⇩1 = mk⇩C⇩a⇩r⇩1 (car1⇩o⇩i⇩d: oid)
    datatype 𝒯⇩C⇩a⇩r⇩2 = mk⇩C⇩a⇩r⇩2 (car2⇩o⇩i⇩d: oid)

    datatype 𝔄 = in⇩C⇩a⇩r⇩1 𝒯⇩C⇩a⇩r⇩1 | in⇩C⇩a⇩r⇩2 𝒯⇩C⇩a⇩r⇩2

    type_synonym Boolean     = "𝔄 Boolean"
    type_synonym Integer     = "𝔄 Integer"
    type_synonym Void        = "𝔄 Void"
    type_synonym Car1        = "(𝔄, 𝒯⇩C⇩a⇩r⇩1 option option) val"
    type_synonym Car2        = "(𝔄, 𝒯⇩C⇩a⇩r⇩2 option option) val"
    type_synonym Set_Integer = "(𝔄, int option option) Set"
    type_synonym Set_Car1    = "(𝔄, 𝒯⇩C⇩a⇩r⇩1 option option) Set"
    type_synonym Set_Car2    = "(𝔄, 𝒯⇩C⇩a⇩r⇩2 option option) Set"

    subsubsection ‹Some Machinery›

    instantiation 𝒯⇩C⇩a⇩r⇩1 :: object
    begin
      definition oid_of_𝒯⇩C⇩a⇩r⇩1[code_unfold]: "oid_of ≡ car1⇩o⇩i⇩d"
      instance ..
    end
    instantiation 𝒯⇩C⇩a⇩r⇩2 :: object
    begin
      definition oid_of_𝒯⇩C⇩a⇩r⇩2[code_unfold]: "oid_of ≡ car2⇩o⇩i⇩d"
      instance ..
    end

    instantiation 𝔄 :: object
    begin
      definition oid⇩𝔄[code_unfold]:
        "oid_of x ≡
            (case x of
              in⇩C⇩a⇩r⇩1 car⇩1 ⇒ car1⇩o⇩i⇩d car⇩1 |
              in⇩C⇩a⇩r⇩2 car⇩2 ⇒ car2⇩o⇩i⇩d car⇩2)"
      instance ..
    end

    lemma singleton_set_size:
      fixes
        τ :: "𝔄 st" and
        a :: "'a"
      shows "Set{λ (_ :: 𝔄 st). ⌊⌊a⌋⌋}->size⇩S⇩e⇩t() τ = 𝟭 τ"
    proof -
      let ?set = "⌈⌈Rep_Set⇩b⇩a⇩s⇩e (Set{λ (_ :: 𝔄 st). ⌊⌊a⌋⌋} τ)⌉⌉"
      have
        "?set = {⌊⌊a⌋⌋}" and
        "card ?set = 1"
        by (simp_all add: OclIncluding_rep_set mtSet_rep_set)
      thus ?thesis
        unfolding UML_Set.OclSize_def OclInt1_def
        by simp
    qed

    subsection ‹Instantiation of Strict Equality›

    overloading StrictRefEq ≡ "StrictRefEq :: [Car1, Car1] ⇒ Boolean"
    begin
      definition StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t⇩_⇩C⇩a⇩r⇩1[code_unfold]:
        "(x::Car1) ≐ y ≡ StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t x y"
    end
    overloading StrictRefEq ≡ "StrictRefEq :: [Car2, Car2] ⇒ Boolean"
    begin
      definition StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t⇩_⇩C⇩a⇩r⇩2[code_unfold]:
        "(x::Car2) ≐ y ≡ StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t x y"
    end

    lemmas cps23 =
        cp_StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t[of "x::Car1" "y::Car1" "τ::𝔄 st",
                        simplified StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t⇩_⇩C⇩a⇩r⇩1[symmetric]]
        cp_intro(9)      [of "C::Car1 ⇒ Car1" "D::Car1 ⇒ Car1",
                        simplified StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t⇩_⇩C⇩a⇩r⇩1[symmetric] ]
        StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t_def     [of "x::Car1" "y::Car1", simplified StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t⇩_⇩C⇩a⇩r⇩1[symmetric]]
        StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t_defargs [of _ "x::Car1" "y::Car1", simplified StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t⇩_⇩C⇩a⇩r⇩1[symmetric]]
        StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t_strict1 [of "x::Car1", simplified StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t⇩_⇩C⇩a⇩r⇩1[symmetric]]
        StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t_strict2 [of "x::Car1", simplified StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t⇩_⇩C⇩a⇩r⇩1[symmetric]]
        cp_StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t[of "x::Car1" "y::Car1" "τ::𝔄 st",
                        simplified StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t⇩_⇩C⇩a⇩r⇩1[symmetric]]
        cp_intro(9)      [of "C::Car2 ⇒ Car2" "D::Car2 ⇒ Car2",
                        simplified StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t⇩_⇩C⇩a⇩r⇩2[symmetric] ]
        StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t_def     [of "x::Car2" "y::Car2", simplified StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t⇩_⇩C⇩a⇩r⇩2[symmetric]]
        StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t_defargs [of _ "x::Car2" "y::Car2", simplified StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t⇩_⇩C⇩a⇩r⇩2[symmetric]]
        StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t_strict1 [of "x::Car2", simplified StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t⇩_⇩C⇩a⇩r⇩2[symmetric]]
        StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t_strict2 [of "x::Car2", simplified StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t⇩_⇩C⇩a⇩r⇩2[symmetric]]
      for x y τ C D

    subsection ‹OCL Usage: OclAsType›

    consts OclAsType⇩C⇩a⇩r⇩1 :: "'α ⇒ Car1" ("(_) .oclAsType'(Car1')")
    consts OclAsType⇩C⇩a⇩r⇩2 :: "'α ⇒ Car2" ("(_) .oclAsType'(Car2')")

    definition OclAsType⇩C⇩a⇩r⇩1_𝔄 :: "𝔄 ⇒ ⟨𝒯⇩C⇩a⇩r⇩1⟩⇩⊥" where
      "OclAsType⇩C⇩a⇩r⇩1_𝔄 ≡
        (λ u::𝔄. ⌊case u of in⇩C⇩a⇩r⇩1 (v::𝒯⇩C⇩a⇩r⇩1) ⇒ v⌋)"
    definition OclAsType⇩C⇩a⇩r⇩2_𝔄 :: "𝔄 ⇒ ⟨𝒯⇩C⇩a⇩r⇩2⟩⇩⊥" where
      "OclAsType⇩C⇩a⇩r⇩2_𝔄 ≡
        (λ u::𝔄. ⌊case u of in⇩C⇩a⇩r⇩2 (v::𝒯⇩C⇩a⇩r⇩2) ⇒ v⌋)"

    lemmas [simp] =
      OclAsType⇩C⇩a⇩r⇩1_𝔄_def
      OclAsType⇩C⇩a⇩r⇩2_𝔄_def

    lemma OclAsType⇩C⇩a⇩r⇩1_𝔄_some:
      fixes x :: "𝔄"
      shows "OclAsType⇩C⇩a⇩r⇩1_𝔄 x ≠ None"
      by simp
    lemma OclAsType⇩C⇩a⇩r⇩2_𝔄_some:
      fixes x :: "𝔄"
      shows "OclAsType⇩C⇩a⇩r⇩2_𝔄 x ≠ None"
      by simp

    overloading OclAsType⇩C⇩a⇩r⇩1 ≡ "OclAsType⇩C⇩a⇩r⇩1 :: Car1 ⇒ Car1"
    begin
      definition OclAsType⇩C⇩a⇩r⇩1_Car1[code_unfold]:
        "(X::Car1) .oclAsType(Car1) ≡ X"
    end
    overloading OclAsType⇩C⇩a⇩r⇩2 ≡ "OclAsType⇩C⇩a⇩r⇩2 :: Car2 ⇒ Car2"
    begin
      definition OclAsType⇩C⇩a⇩r⇩2_Car2[code_unfold]:
        "(X::Car2) .oclAsType(Car2) ≡ X"
    end
    lemmas [simp] =
      OclAsType⇩C⇩a⇩r⇩1_Car1
      OclAsType⇩C⇩a⇩r⇩2_Car2

    lemma OclAsType⇩C⇩a⇩r⇩1_Car1_strict: "(invalid::Car1) .oclAsType(Car1) = invalid"
      by simp
    lemma OclAsType⇩C⇩a⇩r⇩2_Car2_strict: "(invalid::Car2) .oclAsType(Car2) = invalid"
      by simp
    lemma OclAsType⇩C⇩a⇩r⇩1_Car1_nullstrict: "(null::Car1) .oclAsType(Car1) = null"
      by simp
    lemma OclAsType⇩C⇩a⇩r⇩2_Car2_nullstrict: "(null::Car2) .oclAsType(Car2) = null"
      by simp

    subsection ‹OCL Usage: OclIsTypeOf›

    consts OclIsTypeOf⇩C⇩a⇩r⇩1 :: "'α ⇒ Boolean" ("(_).oclIsTypeOf'(Car1')")
    consts OclIsTypeOf⇩C⇩a⇩r⇩2 :: "'α ⇒ Boolean" ("(_).oclIsTypeOf'(Car2')")

    overloading OclIsTypeOf⇩C⇩a⇩r⇩1 ≡ "OclIsTypeOf⇩C⇩a⇩r⇩1 :: Car1 ⇒ Boolean"
    begin
      definition OclIsTypeOf⇩C⇩a⇩r⇩1_Car1[code_unfold]:
          "(X::Car1) .oclIsTypeOf(Car1) ≡ (λ τ :: (𝔄 st).
                  case X τ of
                    ⊥ ⇒ invalid τ |
                    _ ⇒ true τ)"
    end
    overloading OclIsTypeOf⇩C⇩a⇩r⇩2 ≡ "OclIsTypeOf⇩C⇩a⇩r⇩2 :: Car2 ⇒ Boolean"
    begin
      definition OclIsTypeOf⇩C⇩a⇩r⇩2_Car2[code_unfold]:
        "(X::Car2) .oclIsTypeOf(Car2) ≡ (λ τ :: (𝔄 st).
                case X τ of
                  ⊥ ⇒ invalid τ |
                  _ ⇒ true τ)"
    end

    lemma OclIsTypeOf⇩C⇩a⇩r⇩1_Car1':
      fixes X :: "Car1"
      shows "X .oclIsTypeOf(Car1) = (λ τ :: (𝔄 st).
                if τ ⊨ υ X
                then case X τ of
                        ⊥ ⇒ invalid τ |
                        _ ⇒ true τ
                else invalid τ)"
      unfolding OclIsTypeOf⇩C⇩a⇩r⇩1_Car1 foundation18' bot_option_def
      by (rule ext, simp)
    lemma OclIsTypeOf⇩C⇩a⇩r⇩2_Car2':
      fixes X :: "Car2"
      shows "X .oclIsTypeOf(Car2) = (λ τ :: (𝔄 st).
                if τ ⊨ υ X
                then case X τ of
                        ⊥ ⇒ invalid τ |
                        _ ⇒ true τ
                else invalid τ)"
      unfolding OclIsTypeOf⇩C⇩a⇩r⇩2_Car2 foundation18' bot_option_def
      by (rule ext, simp)

    interpretation OclIsTypeOf⇩C⇩a⇩r⇩1_Car1:
        profile_mono_schemeV
        "OclIsTypeOf⇩C⇩a⇩r⇩1::Car1 ⇒ Boolean"
        "λ _::(⟨⟨𝒯⇩C⇩a⇩r⇩1⟩⇩⊥⟩⇩⊥). ⌊⌊True⌋⌋"
    proof (unfold_locales, unfold OclIsTypeOf⇩C⇩a⇩r⇩1_Car1' OclValid_def true_def,
            simp add: atomize_eq, rule ext)
      fix
        x :: "Car1" and
        τ :: "𝔄 st"
      show "(if (υ x) τ = ⌊⌊True⌋⌋
              then case x τ of ⊥ ⇒ invalid τ | ⌊a⌋ ⇒ ⌊⌊True⌋⌋
              else invalid τ) =
                  (if (υ x) τ = ⌊⌊True⌋⌋ then ⌊⌊True⌋⌋ else invalid τ)"
        by (auto split: option.split,
            metis OclValid_def bot_option_def foundation18' true_def)
    qed
    interpretation OclIsTypeOf⇩C⇩a⇩r⇩2_Car2:
        profile_mono_schemeV
        "OclIsTypeOf⇩C⇩a⇩r⇩2::Car2 ⇒ Boolean"
        "λ _::(⟨⟨𝒯⇩C⇩a⇩r⇩2⟩⇩⊥⟩⇩⊥). ⌊⌊True⌋⌋"
    proof (unfold_locales, unfold OclIsTypeOf⇩C⇩a⇩r⇩2_Car2' OclValid_def true_def false_def,
            simp add: atomize_eq, rule ext)
      fix
        x :: "Car2" and
        τ :: "𝔄 st"
      show "(if (υ x) τ = ⌊⌊True⌋⌋
              then case x τ of ⊥ ⇒ invalid τ | ⌊a⌋ ⇒ ⌊⌊True⌋⌋
              else invalid τ) =
                  (if (υ x) τ = ⌊⌊True⌋⌋ then ⌊⌊True⌋⌋ else invalid τ)"
        by (auto split: option.split,
            metis OclValid_def bot_option_def foundation18' true_def)
    qed

    lemma cp_OclIsTypeOf⇩C⇩a⇩r⇩1_Car1_Car1:
      fixes P :: "Car1 ⇒ Car1"
      shows "cp P ⟹ cp(λ X::Car1. ((P X) .oclIsTypeOf(Car1)))"
      using OclIsTypeOf⇩C⇩a⇩r⇩1_Car1.cp
      by simp
    lemma cp_OclIsTypeOf⇩C⇩a⇩r⇩2_Car2_Car2:
      fixes P :: "Car2 ⇒ Car2"
      shows "cp P ⟹ cp(λ X::Car2. ((P X) .oclIsTypeOf(Car2)))"
      using OclIsTypeOf⇩C⇩a⇩r⇩2_Car2.cp
      by simp

    lemmas [simp] =
      cp_OclIsTypeOf⇩C⇩a⇩r⇩1_Car1_Car1
      cp_OclIsTypeOf⇩C⇩a⇩r⇩2_Car2_Car2

    lemma OclIsTypeOf⇩C⇩a⇩r⇩1_Car1_strict1[simp]:
      "(invalid::Car1) .oclIsTypeOf(Car1) = invalid"
      by (rule OclIsTypeOf⇩C⇩a⇩r⇩1_Car1.strict)
    lemma OclIsTypeOf⇩C⇩a⇩r⇩2_Car2_strict1[simp]:
      "(invalid::Car2) .oclIsTypeOf(Car2) = invalid"
      by (rule OclIsTypeOf⇩C⇩a⇩r⇩2_Car2.strict)

    lemma OclIsTypeOf⇩C⇩a⇩r⇩1_Car1_strict2[simp]:
      "(null::Car1) .oclIsTypeOf(Car1) = true"
      unfolding OclIsTypeOf⇩C⇩a⇩r⇩1_Car1 null_fun_def null_option_def
      by simp
    lemma OclIsTypeOf⇩C⇩a⇩r⇩2_Car2_strict2[simp]:
      "(null::Car2) .oclIsTypeOf(Car2) = true"
      unfolding OclIsTypeOf⇩C⇩a⇩r⇩2_Car2 null_fun_def null_option_def
      by simp

    subsection ‹OCL Usage: OclIsKindOf›

    subsubsection ‹A Couple of General Heap Accessors›

    definition pre⇩s⇩t⇩a⇩t⇩e :: "'𝔄 × '𝔅 ⇒ '𝔄" where
      "pre⇩s⇩t⇩a⇩t⇩e ≡ fst"

    definition post⇩s⇩t⇩a⇩t⇩e :: "'𝔄 × '𝔅 ⇒ '𝔅" where
      "post⇩s⇩t⇩a⇩t⇩e ≡ snd"

    definition reconst⇩𝒯⇩_⇩b⇩a⇩s⇩e :: "('τ ⇒ 𝔄 st ⇒ ⟨⟨'τ⟩⇩⊥⟩⇩⊥) ⇒ 'τ ⇒
                                    𝔄 st ⇒ ⟨⟨'τ⟩⇩⊥⟩⇩⊥" where
      "reconst⇩𝒯⇩_⇩b⇩a⇩s⇩e ≡ (λ (convert :: 'τ ⇒ 𝔄 st ⇒ ⟨⟨'τ⟩⇩⊥⟩⇩⊥) (τ::'τ). convert τ)"

    definition list⇩f⇩l⇩a⇩t⇩t⇩e⇩n :: "oid list list ⇒ oid list" where
      "list⇩f⇩l⇩a⇩t⇩t⇩e⇩n ≡ (λ ls⇩1 :: oid list list.
          foldl (λ oids⇩1 :: _ list.
            (λ ls⇩2 :: _ list. foldl (λ oids⇩2 :: _ list. (λ l :: _. Cons l oids⇩2)) oids⇩1 (rev ls⇩2)))
              Nil (rev ls⇩1))"

    definition switch⇩2_1 :: "'α list ⇒ 'α × 'α" where
      "switch⇩2_1 = (λ [x, y]    ⇒ (x, y))"
    definition switch⇩2_2 :: "'α list ⇒ 'α × 'α" where
      "switch⇩2_2 = (λ [x, y]    ⇒ (y, x))"
    definition switch⇩3_1 :: "'α list ⇒ 'α × 'α" where
      "switch⇩3_1 = (λ [x, y, z] ⇒ (x, y))"
    definition switch⇩3_2 :: "'α list ⇒ 'α × 'α" where
      "switch⇩3_2 = (λ [x, y, z] ⇒ (x, z))"
    definition switch⇩3_3 :: "'α list ⇒ 'α × 'α" where
      "switch⇩3_3 = (λ [x, y, z] ⇒ (y, x))"
    definition switch⇩3_4 :: "'α list ⇒ 'α × 'α" where
      "switch⇩3_4 = (λ [x, y, z] ⇒ (y, z))"
    definition switch⇩3_5 :: "'α list ⇒ 'α × 'α" where
      "switch⇩3_5 = (λ [x, y ,z] ⇒ (z, x))"
    definition switch⇩3_6 :: "'α list ⇒ 'α × 'α" where
      "switch⇩3_6 = (λ [x, y, z] ⇒ (z, y))"

    subsubsection ‹OclIsKindOf›

    consts OclIsKindOf⇩C⇩a⇩r⇩1 :: "'α ⇒ Boolean" ("(_).oclIsKindOf'(Car1')")
    consts OclIsKindOf⇩C⇩a⇩r⇩2 :: "'α ⇒ Boolean" ("(_).oclIsKindOf'(Car2')")

    overloading OclIsKindOf⇩C⇩a⇩r⇩1 ≡ "OclIsKindOf⇩C⇩a⇩r⇩1 :: Car1 ⇒ Boolean"
    begin
      definition OclIsKindOf⇩C⇩a⇩r⇩1_Car1[code_unfold]:
          "(X::Car1) .oclIsKindOf(Car1) ≡ (λ τ :: (𝔄 st).
                case X τ of
                  ⊥ ⇒ invalid τ |
                  _ ⇒ true τ)"
    end
    overloading OclIsKindOf⇩C⇩a⇩r⇩2 ≡ "OclIsKindOf⇩C⇩a⇩r⇩2 :: Car2 ⇒ Boolean"
    begin
      definition OclIsKindOf⇩C⇩a⇩r⇩2_Car2[code_unfold]:
          "(X::Car2) .oclIsKindOf(Car2) ≡ (λ τ :: (𝔄 st).
                case X τ of
                  ⊥ ⇒ invalid τ |
                  _ ⇒ true τ)"
    end

    lemma cp_OclIsKindOf⇩C⇩a⇩r⇩1_Car1_Car1:
      fixes P :: "Car1 ⇒ Car1"
      shows "cp P ⟹ cp(λ X::Car1. ((P X) .oclIsKindOf(Car1)))"
      unfolding OclIsKindOf⇩C⇩a⇩r⇩1_Car1
      by (rule cpI1, safe)
    lemma cp_OclIsKindOf⇩C⇩a⇩r⇩2_Car2_Car2:
      fixes P :: "Car2 ⇒ Car2"
      shows "cp P ⟹ cp(λ X::Car2. ((P X) .oclIsKindOf(Car2)))"
      unfolding OclIsKindOf⇩C⇩a⇩r⇩2_Car2
      by (rule cpI1, safe)

    lemmas [simp] =
      cp_OclIsKindOf⇩C⇩a⇩r⇩1_Car1_Car1
      cp_OclIsKindOf⇩C⇩a⇩r⇩2_Car2_Car2

    lemma OclIsKindOf⇩C⇩a⇩r⇩1_Car1_strict1[simp]:
      "(invalid::Car1) .oclIsKindOf(Car1) = invalid"
      unfolding invalid_def bot_option_def OclIsKindOf⇩C⇩a⇩r⇩1_Car1
      by simp
    lemma OclIsKindOf⇩C⇩a⇩r⇩2_Car2_strict1[simp]:
      "(invalid::Car2) .oclIsKindOf(Car2) = invalid"
      unfolding invalid_def bot_option_def OclIsKindOf⇩C⇩a⇩r⇩2_Car2
      by simp

    lemma OclIsKindOf⇩C⇩a⇩r⇩1_Car1_strict2[simp]:
      "(null::Car1) .oclIsKindOf(Car1) = true"
      unfolding null_fun_def null_option_def OclIsKindOf⇩C⇩a⇩r⇩1_Car1
      by simp
    lemma OclIsKindOf⇩C⇩a⇩r⇩2_Car2_strict2[simp]:
      "(null::Car2) .oclIsKindOf(Car2) = true"
      unfolding null_fun_def null_option_def OclIsKindOf⇩C⇩a⇩r⇩2_Car2
      by simp

    subsection ‹OCL Usage: OclAllInstances›

    definition Car1 :: "𝔄 ⇒ ⟨𝒯⇩C⇩a⇩r⇩1⟩⇩⊥" where "Car1 ≡ OclAsType⇩C⇩a⇩r⇩1_𝔄"
    definition Car2 :: "𝔄 ⇒ ⟨𝒯⇩C⇩a⇩r⇩2⟩⇩⊥" where "Car2 ≡ OclAsType⇩C⇩a⇩r⇩2_𝔄"

    lemmas [simp] =
      Car1_def
      Car2_def

    lemma OclAllInstances_generic⇩C⇩a⇩r⇩1_exec:
      fixes pre_post :: "𝔄 st ⇒ 𝔄 state"
      shows "OclAllInstances_generic pre_post Car1 =
              (λ τ :: 𝔄 st. Abs_Set⇩b⇩a⇩s⇩e ⌊⌊Some ` Car1 ` ran (heap (pre_post τ))⌋⌋)"
    proof -
      let ?S1 = "λ τ :: 𝔄 st. Car1 ` ran (heap (pre_post τ))"
      let ?S2 = "λ τ :: 𝔄 st. ?S1 τ - {None}"
      have B: "⋀ τ :: 𝔄 st. ?S2 τ ⊆ ?S1 τ"
        by safe
      have "⋀ τ :: 𝔄 st. ?S1 τ ⊆ ?S2 τ"
        by force
      thus ?thesis
        by(insert equalityI [OF B], simp)
    qed
    lemma OclAllInstances_generic⇩C⇩a⇩r⇩2_exec:
      fixes pre_post :: "𝔄 st ⇒ 𝔄 state"
      shows "OclAllInstances_generic pre_post Car2 =
              (λ τ :: 𝔄 st. Abs_Set⇩b⇩a⇩s⇩e ⌊⌊Some ` Car2 ` ran (heap (pre_post τ))⌋⌋)"
    proof -
      let ?S1 = "λ τ :: 𝔄 st. Car2 ` ran (heap (pre_post τ))"
      let ?S2 = "λ τ :: 𝔄 st. ?S1 τ - {None}"
      have B: "⋀ τ :: 𝔄 st. ?S2 τ ⊆ ?S1 τ"
        by safe
      have "⋀ τ :: 𝔄 st. ?S1 τ ⊆ ?S2 τ"
        by force
      thus ?thesis
        by(insert equalityI [OF B], simp)
    qed

    lemma OclAllInstances_at_post⇩C⇩a⇩r⇩1_exec: "Car1 .allInstances() =
            (λ τ :: 𝔄 st. Abs_Set⇩b⇩a⇩s⇩e ⌊⌊Some ` Car1 ` ran (heap (post⇩s⇩t⇩a⇩t⇩e τ))⌋⌋)"
      unfolding OclAllInstances_at_post_def post⇩s⇩t⇩a⇩t⇩e_def
      by(rule OclAllInstances_generic⇩C⇩a⇩r⇩1_exec)
    lemma OclAllInstances_at_post⇩C⇩a⇩r⇩2_exec: "Car2 .allInstances() =
            (λ τ :: 𝔄 st. Abs_Set⇩b⇩a⇩s⇩e ⌊⌊Some ` Car2 ` ran (heap (post⇩s⇩t⇩a⇩t⇩e τ))⌋⌋)"
      unfolding OclAllInstances_at_post_def post⇩s⇩t⇩a⇩t⇩e_def
      by(rule OclAllInstances_generic⇩C⇩a⇩r⇩2_exec)

    lemma OclAllInstances_at_pre⇩C⇩a⇩r⇩1_exec: "Car1 .allInstances@pre() =
            (λ τ :: 𝔄 st. Abs_Set⇩b⇩a⇩s⇩e ⌊⌊Some ` Car1 ` ran (heap (pre⇩s⇩t⇩a⇩t⇩e τ))⌋⌋)"
      unfolding OclAllInstances_at_pre_def pre⇩s⇩t⇩a⇩t⇩e_def
      by(rule OclAllInstances_generic⇩C⇩a⇩r⇩1_exec)
    lemma OclAllInstances_at_pre⇩C⇩a⇩r⇩2_exec: "Car2 .allInstances@pre() =
            (λ τ :: 𝔄 st. Abs_Set⇩b⇩a⇩s⇩e ⌊⌊Some ` Car2 ` ran (heap (pre⇩s⇩t⇩a⇩t⇩e τ))⌋⌋)"
      unfolding OclAllInstances_at_pre_def pre⇩s⇩t⇩a⇩t⇩e_def
      by(rule OclAllInstances_generic⇩C⇩a⇩r⇩2_exec)

    lemma Car1_allInstances_generic_oclIsTypeOf⇩C⇩a⇩r⇩11:
      fixes pre_post :: "𝔄 st ⇒ 𝔄 state"
      assumes [simp]: "⋀ x :: 𝔄 state. pre_post (x, x) = x"
      shows "∃ τ :: 𝔄 st.
                (τ ⊨ ((OclAllInstances_generic pre_post Car1)
                          ->forAll⇩S⇩e⇩t(X | X .oclIsTypeOf(Car1))))"
      unfolding OclAllInstances_generic_defined[simplified OclValid_def] UML_Set.OclForall_def
      unfolding OclAllInstances_generic_def
      apply(rule_tac x = τ⇩0 in exI)
      unfolding τ⇩0_def OclValid_def
      apply(subst (1 2 3) Abs_Set⇩b⇩a⇩s⇩e_inverse)
      by simp_all
    lemma Car2_allInstances_generic_oclIsTypeOf⇩C⇩a⇩r⇩21:
      fixes pre_post :: "𝔄 st ⇒ 𝔄 state"
      assumes [simp]: "⋀ x :: 𝔄 state. pre_post (x, x) = x"
      shows "∃ τ :: 𝔄 st.
                (τ ⊨ ((OclAllInstances_generic pre_post Car2)
                          ->forAll⇩S⇩e⇩t(X | X .oclIsTypeOf(Car2))))"
      unfolding OclAllInstances_generic_defined[simplified OclValid_def] UML_Set.OclForall_def
      unfolding OclAllInstances_generic_def
      apply(rule_tac x = τ⇩0 in exI)
      unfolding τ⇩0_def OclValid_def
      apply(subst (1 2 3) Abs_Set⇩b⇩a⇩s⇩e_inverse)
      by simp_all

    lemma Car1_allInstances_at_post_oclIsTypeOf⇩C⇩a⇩r⇩11:
      "∃ τ :: 𝔄 st. (τ ⊨ (Car1 .allInstances()->forAll⇩S⇩e⇩t(X | X .oclIsTypeOf(Car1))))"
      unfolding OclAllInstances_at_post_def
      by(rule Car1_allInstances_generic_oclIsTypeOf⇩C⇩a⇩r⇩11, simp)
    lemma Car2_allInstances_at_post_oclIsTypeOf⇩C⇩a⇩r⇩21:
      "∃ τ :: 𝔄 st. (τ ⊨ (Car2 .allInstances()->forAll⇩S⇩e⇩t(X | X .oclIsTypeOf(Car2))))"
      unfolding OclAllInstances_at_post_def
      by(rule Car2_allInstances_generic_oclIsTypeOf⇩C⇩a⇩r⇩21, simp)

    lemma Car1_allInstances_at_pre_oclIsTypeOf⇩C⇩a⇩r⇩11:
      "∃ τ :: 𝔄 st. (τ ⊨ (Car1 .allInstances@pre()->forAll⇩S⇩e⇩t(X | X .oclIsTypeOf(Car1))))"
      unfolding OclAllInstances_at_pre_def
      by(rule Car1_allInstances_generic_oclIsTypeOf⇩C⇩a⇩r⇩11, simp)
    lemma Car2_allInstances_at_pre_oclIsTypeOf⇩C⇩a⇩r⇩21:
      "∃ τ :: 𝔄 st. (τ ⊨ (Car2 .allInstances@pre()->forAll⇩S⇩e⇩t(X | X .oclIsTypeOf(Car2))))"
      unfolding OclAllInstances_at_pre_def
      by(rule Car2_allInstances_generic_oclIsTypeOf⇩C⇩a⇩r⇩21, simp)

    lemma Car1_allInstances_generic_oclIsTypeOf⇩C⇩a⇩r⇩1:
      fixes
        τ :: "𝔄 st" and
        pre_post :: "𝔄 st ⇒ 𝔄 state"
      shows "τ ⊨ ((OclAllInstances_generic pre_post Car1)->forAll⇩S⇩e⇩t(X | X .oclIsTypeOf(Car1)))"
      unfolding OclAllInstances_generic_defined[simplified OclValid_def] UML_Set.OclForall_def
      unfolding OclAllInstances_generic_def OclValid_def OclIsTypeOf⇩C⇩a⇩r⇩1_Car1
      apply(subst (1 2 3) Abs_Set⇩b⇩a⇩s⇩e_inverse)
      by (simp add: bot_option_def, simp)
    lemma Car2_allInstances_generic_oclIsTypeOf⇩C⇩a⇩r⇩2:
      fixes
        τ :: "𝔄 st" and
        pre_post :: "𝔄 st ⇒ 𝔄 state"
      shows "τ ⊨ ((OclAllInstances_generic pre_post Car2)->forAll⇩S⇩e⇩t(X | X .oclIsTypeOf(Car2)))"
      unfolding OclAllInstances_generic_defined[simplified OclValid_def] UML_Set.OclForall_def
      unfolding OclAllInstances_generic_def OclValid_def OclIsTypeOf⇩C⇩a⇩r⇩2_Car2
      apply(subst (1 2 3) Abs_Set⇩b⇩a⇩s⇩e_inverse)
      by (simp add: bot_option_def, simp)

    lemma Car1_allInstances_at_post_oclIsTypeOf⇩C⇩a⇩r⇩1:
      fixes τ :: "𝔄 st"
      shows "τ ⊨ (Car1 .allInstances()->forAll⇩S⇩e⇩t(X | X .oclIsTypeOf(Car1)))"
      unfolding OclAllInstances_at_post_def
      by(rule Car1_allInstances_generic_oclIsTypeOf⇩C⇩a⇩r⇩1)
    lemma Car2_allInstances_at_post_oclIsTypeOf⇩C⇩a⇩r⇩2:
      fixes τ :: "𝔄 st"
      shows "τ ⊨ (Car2 .allInstances()->forAll⇩S⇩e⇩t(X | X .oclIsTypeOf(Car2)))"
      unfolding OclAllInstances_at_post_def
      by(rule Car2_allInstances_generic_oclIsTypeOf⇩C⇩a⇩r⇩2)

    lemma Car1_allInstances_at_pre_oclIsTypeOf⇩C⇩a⇩r⇩1:
      fixes τ :: "𝔄 st"
      shows "τ ⊨ (Car1 .allInstances@pre()->forAll⇩S⇩e⇩t(X | X .oclIsTypeOf(Car1)))"
      unfolding OclAllInstances_at_pre_def
      by(rule Car1_allInstances_generic_oclIsTypeOf⇩C⇩a⇩r⇩1)
    lemma Car2_allInstances_at_pre_oclIsTypeOf⇩C⇩a⇩r⇩2:
      fixes τ :: "𝔄 st"
      shows "τ ⊨ (Car2 .allInstances@pre()->forAll⇩S⇩e⇩t(X | X .oclIsTypeOf(Car2)))"
      unfolding OclAllInstances_at_pre_def
      by(rule Car2_allInstances_generic_oclIsTypeOf⇩C⇩a⇩r⇩2)

    lemma Car1_allInstances_generic_oclIsKindOf⇩C⇩a⇩r⇩1:
      fixes
        τ :: "𝔄 st" and
        pre_post :: "𝔄 st ⇒ 𝔄 state"
      shows "τ ⊨ ((OclAllInstances_generic pre_post Car1)->forAll⇩S⇩e⇩t(X | X .oclIsKindOf(Car1)))"
      unfolding OclAllInstances_generic_defined[simplified OclValid_def] UML_Set.OclForall_def
      unfolding OclValid_def OclAllInstances_generic_def OclIsKindOf⇩C⇩a⇩r⇩1_Car1
      apply(subst (1 2 3) Abs_Set⇩b⇩a⇩s⇩e_inverse)
      unfolding bot_option_def
      by simp_all
    lemma Car2_allInstances_generic_oclIsKindOf⇩C⇩a⇩r⇩2:
      fixes
        τ :: "𝔄 st" and
        pre_post :: "𝔄 st ⇒ 𝔄 state"
      shows "τ ⊨ ((OclAllInstances_generic pre_post Car2)->forAll⇩S⇩e⇩t(X | X .oclIsKindOf(Car2)))"
      unfolding OclAllInstances_generic_defined[simplified OclValid_def] UML_Set.OclForall_def
      unfolding OclValid_def OclAllInstances_generic_def OclIsKindOf⇩C⇩a⇩r⇩2_Car2
      apply(subst (1 2 3) Abs_Set⇩b⇩a⇩s⇩e_inverse)
      unfolding bot_option_def
      by simp_all

    lemma Car1_allInstances_at_post_oclIsKindOf⇩C⇩a⇩r⇩1:
      fixes τ :: "𝔄 st"
      shows "τ ⊨ (Car1 .allInstances()->forAll⇩S⇩e⇩t(X | X .oclIsKindOf(Car1)))"
      unfolding OclAllInstances_at_post_def
      by(rule Car1_allInstances_generic_oclIsKindOf⇩C⇩a⇩r⇩1)
    lemma Car2_allInstances_at_post_oclIsKindOf⇩C⇩a⇩r⇩2:
      fixes τ :: "𝔄 st"
      shows "τ ⊨ (Car2 .allInstances()->forAll⇩S⇩e⇩t(X | X .oclIsKindOf(Car2)))"
      unfolding OclAllInstances_at_post_def
      by(rule Car2_allInstances_generic_oclIsKindOf⇩C⇩a⇩r⇩2)

    lemma Car1_allInstances_at_pre_oclIsKindOf⇩C⇩a⇩r⇩1:
      fixes τ :: "𝔄 st"
      shows "τ ⊨ (Car1 .allInstances@pre()->forAll⇩S⇩e⇩t(X | X .oclIsKindOf(Car1)))"
      unfolding OclAllInstances_at_pre_def
      by(rule Car1_allInstances_generic_oclIsKindOf⇩C⇩a⇩r⇩1)
    lemma Car2_allInstances_at_pre_oclIsKindOf⇩C⇩a⇩r⇩2:
      fixes τ :: "𝔄 st"
      shows "τ ⊨ (Car2 .allInstances@pre()->forAll⇩S⇩e⇩t(X | X .oclIsKindOf(Car2)))"
      unfolding OclAllInstances_at_pre_def
      by(rule Car2_allInstances_generic_oclIsKindOf⇩C⇩a⇩r⇩2)

    subsection ‹OCL Usage: The Accessors›

    text ‹Now we also define accessors (albeit not very useful for this small example)›

    definition eval_extract :: "(𝔄, ('α::object) option option) val ⇒
                                  (oid ⇒ (𝔄, 'β::null) val) ⇒
                                  (𝔄, 'β) val" where
      "eval_extract X f ≡ (λ τ :: 𝔄 st.
          case (X :: 𝔄 st ⇒ ⟨⟨'α⟩⇩⊥⟩⇩⊥) τ of
            ⊥      ⇒ invalid τ |  ― ‹exception propagation›
            ⌊⊥⌋    ⇒ invalid τ |  ― ‹dereferencing null pointer›
            ⌊⌊obj⌋⌋ ⇒ f (oid_of obj) τ)"

    definition deref_assocs :: "(𝔄 st ⇒ 𝔄 state) ⇒
                                    (oid list list ⇒ oid list × oid list) ⇒
                                    oid ⇒ (oid list ⇒ (𝔄, 'α::null) val) ⇒
                                    oid ⇒ (𝔄, 'α) val" where
      "deref_assocs pre⇩p⇩o⇩s⇩t to⇩f⇩r⇩o⇩m assoc⇩o⇩i⇩d f oid ≡ (λ τ :: 𝔄 st.
          case (assocs (pre⇩p⇩o⇩s⇩t τ)) assoc⇩o⇩i⇩d of
            ⌊S::oid list list list⌋ ⇒
              f (list⇩f⇩l⇩a⇩t⇩t⇩e⇩n (map (post⇩s⇩t⇩a⇩t⇩e ∘ to⇩f⇩r⇩o⇩m)
                (filter (λ p :: (oid list list).
                          List.member (pre⇩s⇩t⇩a⇩t⇩e (to⇩f⇩r⇩o⇩m p)) oid) S))) τ |
            _ ⇒ invalid τ)"

    definition deref_oid⇩C⇩a⇩r⇩1 :: "(𝔄 st ⇒ 𝔄 state) ⇒
                                  (𝒯⇩C⇩a⇩r⇩1 ⇒ (𝔄, 'α::null) val) ⇒
                                  oid ⇒ (𝔄, 'α) val" where
      "deref_oid⇩C⇩a⇩r⇩1 fst⇩s⇩n⇩d f oid ≡ (λ τ :: (𝔄 st).
          case (heap (fst⇩s⇩n⇩d τ)) oid of
            ⌊in⇩C⇩a⇩r⇩1 obj⌋ ⇒ f obj τ |
            _           ⇒ invalid τ)"
    definition deref_oid⇩C⇩a⇩r⇩2 :: "(𝔄 st ⇒ 𝔄 state) ⇒
                                  (𝒯⇩C⇩a⇩r⇩2 ⇒ (𝔄, 'α::null) val) ⇒
                                  oid ⇒ (𝔄, 'α) val" where
      "deref_oid⇩C⇩a⇩r⇩2 fst⇩s⇩n⇩d f oid ≡ (λ τ :: (𝔄 st).
          case (heap (fst⇩s⇩n⇩d τ)) oid of
            ⌊ in⇩C⇩a⇩r⇩2 obj ⌋ ⇒ f obj τ |
            _             ⇒ invalid τ)"

    lemmas [simp] = eval_extract_def

    subsection ‹An Example Heap›

    text ‹We can give an example state with some concrete car1s and car2s:›

    definition oid⇩0 :: "'a::zero"    where "oid⇩0 ≡ 0"
    definition oid⇩1 :: "'a::numeral" where "oid⇩1 ≡ 1"
    definition oid⇩2 :: "'a::numeral" where "oid⇩2 ≡ 2"
    definition oid⇩3 :: "'a::numeral" where "oid⇩3 ≡ 3"
    definition oid⇩4 :: "'a::numeral" where "oid⇩4 ≡ 4"

    definition oids :: "'a::{zero,numeral} list" where
      "oids ≡ [oid⇩0, oid⇩1, oid⇩2, oid⇩3, oid⇩4]"

    definition car1⇩1 :: "𝒯⇩C⇩a⇩r⇩1" where "car1⇩1 ≡ mk⇩C⇩a⇩r⇩1 oid⇩0"
    definition car1⇩2 :: "𝒯⇩C⇩a⇩r⇩1" where "car1⇩2 ≡ mk⇩C⇩a⇩r⇩1 oid⇩1"
    definition car2⇩1 :: "𝒯⇩C⇩a⇩r⇩2" where "car2⇩1 ≡ mk⇩C⇩a⇩r⇩2 oid⇩2"
    definition car2⇩2 :: "𝒯⇩C⇩a⇩r⇩2" where "car2⇩2 ≡ mk⇩C⇩a⇩r⇩2 oid⇩3"

    definition cars⇩m⇩a⇩n :: "𝒯⇩C⇩a⇩r⇩1 list" where
      "cars⇩m⇩a⇩n ≡ [car1⇩1, car1⇩2]"
    definition cars⇩s⇩u⇩p :: "𝒯⇩C⇩a⇩r⇩2 list" where
      "cars⇩s⇩u⇩p ≡ [car2⇩1, car2⇩2]"

    definition σ :: "𝔄 state" where
      "σ ≡ ⦇heap = Map.empty(oid⇩0 ↦ in⇩C⇩a⇩r⇩1 car1⇩1, oid⇩1 ↦ in⇩C⇩a⇩r⇩1 car1⇩2,
                             oid⇩2 ↦ in⇩C⇩a⇩r⇩2 car2⇩1, oid⇩3 ↦ in⇩C⇩a⇩r⇩2 car2⇩2),
            assocs = Map.empty⦈"
    abbreviation "τ ≡ (σ, σ)"

    definition σ⇩0 :: "𝔄 state" where
      "σ⇩0 ≡ ⦇heap = Map.empty, assocs = Map.empty⦈"

    text ‹
      There is already an equivalent definition of ‹τ⇩0 ≡ (σ⇩0, σ⇩0)› in
      \<^theory>‹Featherweight_OCL.UML_State›.
    ›
    lemma τ⇩0_equiv: "τ⇩0 ≡ (σ⇩0, σ⇩0)"
      unfolding σ⇩0_def τ⇩0_def
      by argo

    lemma refl⇩0_τ_wff: "WFF τ⇩0"
      by(auto simp: WFF_def τ⇩0_equiv τ⇩0_def)
    lemma refl_τ_wff: "WFF τ"
      by(auto simp: WFF_def σ_def oid⇩0_def oid⇩1_def oid⇩2_def oid⇩3_def oid⇩𝔄
                    car1⇩1_def car1⇩2_def car2⇩1_def car2⇩2_def)
    lemma basic_τ_wff: "WFF (σ⇩0, σ)"
      by(auto simp: WFF_def σ⇩0_def σ_def oid⇩0_def oid⇩1_def oid⇩2_def oid⇩3_def oid⇩𝔄
                    car1⇩1_def car1⇩2_def car2⇩1_def car2⇩2_def)

    lemma[simp, code_unfold]: "dom (heap σ) = {oid⇩0, oid⇩1, oid⇩2, oid⇩3}"
      unfolding σ_def
      by auto
    lemma[simp, code_unfold]: "dom (heap σ⇩0) = {}"
      unfolding σ⇩0_def
      by auto

    subsubsection ‹Abbreviations for Some Constant OCL Values›

    definition x⇩c⇩a⇩r⇩1⇩_⇩1 :: "Car1" where
      "x⇩c⇩a⇩r⇩1⇩_⇩1 ≡ λ _. ⌊⌊car1⇩1⌋⌋"
    definition x⇩c⇩a⇩r⇩2⇩_⇩1 :: "Car2" where
      "x⇩c⇩a⇩r⇩2⇩_⇩1 ≡ λ _. ⌊⌊car2⇩1⌋⌋"
    definition x⇩c⇩a⇩r⇩1⇩_⇩2 :: "Car1" where
      "x⇩c⇩a⇩r⇩1⇩_⇩2 ≡ λ _. ⌊⌊car1⇩2⌋⌋"
    definition x⇩c⇩a⇩r⇩2⇩_⇩2 :: "Car2" where
      "x⇩c⇩a⇩r⇩2⇩_⇩2 ≡ λ _. ⌊⌊car2⇩2⌋⌋"

    lemmas[simp] = x⇩c⇩a⇩r⇩1⇩_⇩1_def x⇩c⇩a⇩r⇩2⇩_⇩1_def x⇩c⇩a⇩r⇩1⇩_⇩2_def x⇩c⇩a⇩r⇩2⇩_⇩2_def

    lemma[code_unfold]: "((x::Car1) ≐ y) = StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t x y"
      by(simp only: StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t⇩_⇩C⇩a⇩r⇩1)
    lemma[code_unfold]: "((x::Car2) ≐ y) = StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t x y"
      by(simp only: StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t⇩_⇩C⇩a⇩r⇩2)

    lemma[code_unfold]: "ran (heap σ) = {in⇩C⇩a⇩r⇩1 car1⇩1, in⇩C⇩a⇩r⇩1 car1⇩2, in⇩C⇩a⇩r⇩2 car2⇩1, in⇩C⇩a⇩r⇩2 car2⇩2}"
      unfolding σ_def oid⇩0_def oid⇩1_def oid⇩2_def oid⇩3_def
      by (simp add: insert_commute)

    lemma[code_unfold]: "ran (heap σ⇩0) = {}"
      unfolding σ⇩0_def
      by simp

    end