Theory Design_UML

(*****************************************************************************
 * Featherweight-OCL --- A Formal Semantics for UML-OCL Version OCL 2.5
 *                       for the OMG Standard.
 *                       http://www.brucker.ch/projects/hol-testgen/
 *
 * Design_UML.thy --- OCL Contracts and an Example.
 * This file is part of HOL-TestGen.
 *
 * Copyright (c) 2012-2015 Université Paris-Saclay, Univ. Paris-Sud, France
 *               2013-2015 IRT SystemX, France
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are
 * met:
 *
 *     * Redistributions of source code must retain the above copyright
 *       notice, this list of conditions and the following disclaimer.
 *
 *     * Redistributions in binary form must reproduce the above
 *       copyright notice, this list of conditions and the following
 *       disclaimer in the documentation and/or other materials provided
 *       with the distribution.
 *
 *     * Neither the name of the copyright holders nor the names of its
 *       contributors may be used to endorse or promote products derived
 *       from this software without specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
 * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
 * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
 * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
 * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
 * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
 * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
 * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
 * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 ******************************************************************************)

chapter‹Example: The Employee Design Model› (* UML part *)

theory
  Design_UML
imports
  "../../../UML_Main"
begin

text ‹\label{ex:employee-design:uml}›

section‹Introduction›
text‹
  For certain concepts like classes and class-types, only a generic
  definition for its resulting semantics can be given. Generic means,
  there is a function outside HOL that ``compiles'' a concrete,
  closed-world class diagram into a ``theory'' of this data model,
  consisting of a bunch of definitions for classes, accessors, method,
  casts, and tests for actual types, as well as proofs for the
  fundamental properties of these operations in this concrete data
  model.›

text‹Such generic function or ``compiler'' can be implemented in
  Isabelle on the ML level.  This has been done, for a semantics
  following the open-world assumption, for UML 2.0
  in~cite‹"brucker.ea:extensible:2008-b" and "brucker:interactive:2007"›. In
  this paper, we follow another approach for UML 2.4: we define the
  concepts of the compilation informally, and present a concrete
  example which is verified in Isabelle/HOL.›

subsection‹Outlining the Example›

text‹We are presenting here a ``design-model'' of the (slightly
modified) example Figure 7.3, page 20 of
the OCL standard~cite‹"omg:ocl:2012"›. To be precise, this theory contains the formalization of
the data-part covered by the UML class model (see \autoref{fig:person}):›

text‹
\begin{figure}
  \centering\scalebox{.3}{\includegraphics{figures/person.png}}%
  \caption{A simple UML class model drawn from Figure 7.3,
  page 20 of~cite‹"omg:ocl:2012"›. \label{fig:person}}
\end{figure}
›

text‹This means that the association (attached to the association class
\inlineocl{EmployeeRanking}) with the association ends \inlineocl+boss+ and \inlineocl+employees+ is implemented
by the attribute  \inlineocl+boss+ and the operation \inlineocl+employees+ (to be discussed in the OCL part
captured by the subsequent theory).
›

section‹Example Data-Universe and its Infrastructure›
text‹Ideally, the following is generated automatically from a UML class model.›

text‹Our data universe  consists in the concrete class diagram just of node's,
and implicitly of the class object. Each class implies the existence of a class
type defined for the corresponding object representations as follows:›

datatype typePerson = mkPerson oid          (* the oid to the person itself *)
                            "int option" (* the attribute "salary" or null *)
                            "oid option" (* the attribute "boss" or null *)


datatype typeOclAny = mkOclAny oid          (* the oid to the oclany itself *)
                            "(int option × oid option) option"
                                         (* the extensions to "person"; used to denote
                                            objects of actual type "person" casted to "oclany";
                                            in case of existence of several subclasses
                                            of oclany, sums of extensions have to be provided. *)

text‹Now, we construct a concrete ``universe of OclAny types'' by injection into a
sum type containing the class types. This type of OclAny will be used as instance
for all respective type-variables.›

datatype 𝔄 = inPerson typePerson | inOclAny typeOclAny

text‹Having fixed the object universe, we can introduce type synonyms that exactly correspond
to OCL types. Again, we exploit that our representation of OCL is a ``shallow embedding'' with a
one-to-one correspondance of OCL-types to types of the meta-language HOL.›
type_synonym Boolean     = " 𝔄 Boolean"
type_synonym Integer     = " 𝔄 Integer"
type_synonym Void        = " 𝔄 Void"
type_synonym OclAny      = "(𝔄, typeOclAny option option) val"
type_synonym Person      = "(𝔄, typePerson option option) val"
type_synonym Set_Integer = "(𝔄, int option option) Set"
type_synonym Set_Person  = "(𝔄, typePerson option option) Set"

text‹Just a little check:›
typ "Boolean"

text‹To reuse key-elements of the library like referential equality, we have
to show that the object universe belongs to the type class ``oclany,'' \ie,
 each class type has to provide a function @{term oid_of} yielding the object id (oid) of the object.›
instantiation typePerson :: object
begin
   definition oid_of_typePerson_def: "oid_of x = (case x of mkPerson oid _ _ ⇒ oid)"
   instance ..
end

instantiation typeOclAny :: object
begin
   definition oid_of_typeOclAny_def: "oid_of x = (case x of mkOclAny oid _ ⇒ oid)"
   instance ..
end

instantiation 𝔄 :: object
begin
   definition oid_of_𝔄_def: "oid_of x = (case x of
                                             inPerson person ⇒ oid_of person
                                           | inOclAny oclany ⇒ oid_of oclany)"
   instance ..
end




section‹Instantiation of the Generic Strict Equality›
text‹We instantiate the referential equality
on ‹Person› and ‹OclAny››

overloading StrictRefEq ≡ "StrictRefEq :: [Person,Person] ⇒ Boolean"
begin
  definition StrictRefEqObject_Person   : "(x::Person) ≐ y  ≡ StrictRefEqObject x y"
end

overloading StrictRefEq ≡ "StrictRefEq :: [OclAny,OclAny] ⇒ Boolean"
begin
  definition StrictRefEqObject_OclAny   : "(x::OclAny) ≐ y  ≡ StrictRefEqObject x y"
end

lemmas cps23 = 
    cp_StrictRefEqObject[of "x::Person" "y::Person" "τ",
                         simplified StrictRefEqObject_Person[symmetric]]
    cp_intro(9)         [of "P::Person ⇒Person""Q::Person ⇒Person",
                         simplified StrictRefEqObject_Person[symmetric] ]
    StrictRefEqObject_def      [of "x::Person" "y::Person",
                         simplified StrictRefEqObject_Person[symmetric]]
    StrictRefEqObject_defargs  [of _ "x::Person" "y::Person",
                         simplified StrictRefEqObject_Person[symmetric]]
    StrictRefEqObject_strict1
                        [of "x::Person",
                         simplified StrictRefEqObject_Person[symmetric]]
    StrictRefEqObject_strict2
                        [of "x::Person",
                         simplified StrictRefEqObject_Person[symmetric]]
  for x y τ P Q
text‹For each Class \emph{C}, we will have a casting operation \inlineocl{.oclAsType($C$)},
   a test on the actual type \inlineocl{.oclIsTypeOf($C$)} as well as its relaxed form
   \inlineocl{.oclIsKindOf($C$)} (corresponding exactly to Java's \verb+instanceof+-operator.
›
text‹Thus, since we have two class-types in our concrete class hierarchy, we have
two operations to declare and to provide two overloading definitions for the two static types.
›


section‹OclAsType›
subsection‹Definition›

consts OclAsTypeOclAny :: "'α ⇒ OclAny" ("(_) .oclAsType'(OclAny')")
consts OclAsTypePerson :: "'α ⇒ Person" ("(_) .oclAsType'(Person')")

definition "OclAsTypeOclAny_𝔄 = (λu. ⌊case u of inOclAny a ⇒ a
                                            | inPerson (mkPerson oid a b) ⇒ mkOclAny oid ⌊(a,b)⌋⌋)"

lemma OclAsTypeOclAny_𝔄_some: "OclAsTypeOclAny_𝔄 x ≠ None"
by(simp add: OclAsTypeOclAny_𝔄_def)

overloading OclAsTypeOclAny ≡ "OclAsTypeOclAny :: OclAny ⇒ OclAny"
begin
  definition OclAsTypeOclAny_OclAny:
        "(X::OclAny) .oclAsType(OclAny) ≡ X"
end

overloading OclAsTypeOclAny ≡ "OclAsTypeOclAny :: Person ⇒ OclAny"
begin
  definition OclAsTypeOclAny_Person:
        "(X::Person) .oclAsType(OclAny) ≡
                   (λτ. case X τ of
                              ⊥   ⇒ invalid τ
                            | ⌊⊥⌋ ⇒ null τ
                            | ⌊⌊mkPerson oid a b ⌋⌋ ⇒  ⌊⌊  (mkOclAny oid ⌊(a,b)⌋) ⌋⌋)"
end

definition "OclAsTypePerson_𝔄 = 
                   (λu. case u of inPerson p ⇒ ⌊p⌋
                            | inOclAny (mkOclAny oid ⌊(a,b)⌋) ⇒ ⌊mkPerson oid a b⌋
                            | _ ⇒ None)"

overloading OclAsTypePerson ≡ "OclAsTypePerson :: OclAny ⇒ Person"
begin
  definition OclAsTypePerson_OclAny:
        "(X::OclAny) .oclAsType(Person) ≡
                   (λτ. case X τ of
                              ⊥   ⇒ invalid τ
                            | ⌊⊥⌋ ⇒ null τ
                            | ⌊⌊mkOclAny oid ⊥ ⌋⌋ ⇒  invalid τ   ― ‹down-cast exception›
                            | ⌊⌊mkOclAny oid ⌊(a,b)⌋ ⌋⌋ ⇒  ⌊⌊mkPerson oid a b ⌋⌋)"
end

overloading OclAsTypePerson ≡ "OclAsTypePerson :: Person ⇒ Person"
begin
  definition OclAsTypePerson_Person:
        "(X::Person) .oclAsType(Person) ≡ X "  (* to avoid identity for null ? *)
end
text_raw‹\isatagafp›

lemmas [simp] =
 OclAsTypeOclAny_OclAny
 OclAsTypePerson_Person
subsection‹Context Passing›

lemma cp_OclAsTypeOclAny_Person_Person: "cp P ⟹ cp(λX. (P (X::Person)::Person) .oclAsType(OclAny))"
by(rule cpI1, simp_all add: OclAsTypeOclAny_Person)
lemma cp_OclAsTypeOclAny_OclAny_OclAny: "cp P ⟹ cp(λX. (P (X::OclAny)::OclAny) .oclAsType(OclAny))"
by(rule cpI1, simp_all add: OclAsTypeOclAny_OclAny)
lemma cp_OclAsTypePerson_Person_Person: "cp P ⟹ cp(λX. (P (X::Person)::Person) .oclAsType(Person))"
by(rule cpI1, simp_all add: OclAsTypePerson_Person)
lemma cp_OclAsTypePerson_OclAny_OclAny: "cp P ⟹ cp(λX. (P (X::OclAny)::OclAny) .oclAsType(Person))"
by(rule cpI1, simp_all add: OclAsTypePerson_OclAny)

lemma cp_OclAsTypeOclAny_Person_OclAny: "cp P ⟹ cp(λX. (P (X::Person)::OclAny) .oclAsType(OclAny))"
by(rule cpI1, simp_all add: OclAsTypeOclAny_OclAny)
lemma cp_OclAsTypeOclAny_OclAny_Person: "cp P ⟹ cp(λX. (P (X::OclAny)::Person) .oclAsType(OclAny))"
by(rule cpI1, simp_all add: OclAsTypeOclAny_Person)
lemma cp_OclAsTypePerson_Person_OclAny: "cp P ⟹ cp(λX. (P (X::Person)::OclAny) .oclAsType(Person))"
by(rule cpI1, simp_all add: OclAsTypePerson_OclAny)
lemma cp_OclAsTypePerson_OclAny_Person: "cp P ⟹ cp(λX. (P (X::OclAny)::Person) .oclAsType(Person))"
by(rule cpI1, simp_all add: OclAsTypePerson_Person)

lemmas [simp] =
 cp_OclAsTypeOclAny_Person_Person
 cp_OclAsTypeOclAny_OclAny_OclAny
 cp_OclAsTypePerson_Person_Person
 cp_OclAsTypePerson_OclAny_OclAny

 cp_OclAsTypeOclAny_Person_OclAny
 cp_OclAsTypeOclAny_OclAny_Person
 cp_OclAsTypePerson_Person_OclAny
 cp_OclAsTypePerson_OclAny_Person

text_raw‹\endisatagafp›

subsection‹Execution with Invalid or Null as Argument›

lemma OclAsTypeOclAny_OclAny_strict : "(invalid::OclAny) .oclAsType(OclAny) = invalid" by(simp)
lemma OclAsTypeOclAny_OclAny_nullstrict : "(null::OclAny) .oclAsType(OclAny) = null" by(simp)
lemma OclAsTypeOclAny_Person_strict[simp] : "(invalid::Person) .oclAsType(OclAny) = invalid"
      by(rule ext, simp add: bot_option_def invalid_def OclAsTypeOclAny_Person)
lemma OclAsTypeOclAny_Person_nullstrict[simp] : "(null::Person) .oclAsType(OclAny) = null"
      by(rule ext, simp add: null_fun_def null_option_def bot_option_def OclAsTypeOclAny_Person)
lemma OclAsTypePerson_OclAny_strict[simp] : "(invalid::OclAny) .oclAsType(Person) = invalid"
      by(rule ext, simp add: bot_option_def invalid_def  OclAsTypePerson_OclAny)
lemma OclAsTypePerson_OclAny_nullstrict[simp] : "(null::OclAny) .oclAsType(Person) = null"
      by(rule ext, simp add: null_fun_def null_option_def bot_option_def  OclAsTypePerson_OclAny)
lemma OclAsTypePerson_Person_strict : "(invalid::Person) .oclAsType(Person) = invalid"  by(simp)
lemma OclAsTypePerson_Person_nullstrict : "(null::Person) .oclAsType(Person) = null" by(simp)

section‹OclIsTypeOf›

subsection‹Definition›

consts OclIsTypeOfOclAny :: "'α ⇒ Boolean" ("(_).oclIsTypeOf'(OclAny')")
consts OclIsTypeOfPerson :: "'α ⇒ Boolean" ("(_).oclIsTypeOf'(Person')")

overloading OclIsTypeOfOclAny ≡ "OclIsTypeOfOclAny :: OclAny ⇒ Boolean"
begin
  definition OclIsTypeOfOclAny_OclAny:
        "(X::OclAny) .oclIsTypeOf(OclAny) ≡
                   (λτ. case X τ of
                              ⊥   ⇒ invalid τ
                            | ⌊⊥⌋ ⇒ true τ  ― ‹invalid ??›
                            | ⌊⌊mkOclAny oid ⊥ ⌋⌋ ⇒ true τ
                            | ⌊⌊mkOclAny oid ⌊_⌋ ⌋⌋ ⇒ false τ)"
end

lemma OclIsTypeOfOclAny_OclAny':
         "(X::OclAny) .oclIsTypeOf(OclAny) = 
                    (λ τ. if τ ⊨ υ X then (case X τ of
                                              ⌊⊥⌋ ⇒ true τ  ― ‹invalid ??›
                                           | ⌊⌊mkOclAny oid ⊥ ⌋⌋ ⇒ true τ
                                           | ⌊⌊mkOclAny oid ⌊_⌋ ⌋⌋ ⇒ false τ)
                                           else invalid τ)"
       apply(rule ext, simp add: OclIsTypeOfOclAny_OclAny)
       by(case_tac "τ ⊨ υ X", auto simp: foundation18' bot_option_def)

interpretation OclIsTypeOfOclAny_OclAny : 
       profile_mono_schemeV 
       "OclIsTypeOfOclAny::OclAny ⇒ Boolean" 
       "λ X. (case X of
                    ⌊None⌋ ⇒ ⌊⌊True⌋⌋  ― ‹invalid ??›
                  | ⌊⌊mkOclAny oid None ⌋⌋ ⇒ ⌊⌊True⌋⌋
                  | ⌊⌊mkOclAny oid ⌊_⌋ ⌋⌋ ⇒ ⌊⌊False⌋⌋)"                     
      apply(unfold_locales, simp add: atomize_eq, rule ext)
      by(auto simp:  OclIsTypeOfOclAny_OclAny' OclValid_def true_def false_def 
              split: option.split typeOclAny.split)

overloading OclIsTypeOfOclAny ≡ "OclIsTypeOfOclAny :: Person ⇒ Boolean"
begin
  definition OclIsTypeOfOclAny_Person:
        "(X::Person) .oclIsTypeOf(OclAny) ≡
                   (λτ. case X τ of
                              ⊥   ⇒ invalid τ
                            | ⌊⊥⌋ ⇒ true τ    ― ‹invalid ??›
                            | ⌊⌊ _ ⌋⌋ ⇒ false τ)  ― ‹must have actual type ‹Person› otherwise›"
end

overloading OclIsTypeOfPerson ≡ "OclIsTypeOfPerson :: OclAny ⇒ Boolean"
begin
  definition OclIsTypeOfPerson_OclAny:
        "(X::OclAny) .oclIsTypeOf(Person) ≡
                   (λτ. case X τ of
                              ⊥   ⇒ invalid τ
                            | ⌊⊥⌋ ⇒ true τ
                            | ⌊⌊mkOclAny oid ⊥ ⌋⌋ ⇒ false τ
                            | ⌊⌊mkOclAny oid ⌊_⌋ ⌋⌋ ⇒ true τ)"
end

overloading OclIsTypeOfPerson ≡ "OclIsTypeOfPerson :: Person ⇒ Boolean"
begin
  definition OclIsTypeOfPerson_Person:
        "(X::Person) .oclIsTypeOf(Person) ≡
                   (λτ. case X τ of
                              ⊥ ⇒ invalid τ
                            | _ ⇒ true τ)" (* for (* ⌊⌊ _ ⌋⌋ ⇒ true τ *) : must have actual type Node otherwise  *)
end
text_raw‹\isatagafp›
subsection‹Context Passing›

lemma cp_OclIsTypeOfOclAny_Person_Person: "cp P ⟹ cp(λX.(P(X::Person)::Person).oclIsTypeOf(OclAny))"
by(rule cpI1, simp_all add: OclIsTypeOfOclAny_Person)
lemma cp_OclIsTypeOfOclAny_OclAny_OclAny: "cp P ⟹ cp(λX.(P(X::OclAny)::OclAny).oclIsTypeOf(OclAny))"
by(rule cpI1, simp_all add: OclIsTypeOfOclAny_OclAny)
lemma cp_OclIsTypeOfPerson_Person_Person: "cp P ⟹ cp(λX.(P(X::Person)::Person).oclIsTypeOf(Person))"
by(rule cpI1, simp_all add: OclIsTypeOfPerson_Person)
lemma cp_OclIsTypeOfPerson_OclAny_OclAny: "cp P ⟹ cp(λX.(P(X::OclAny)::OclAny).oclIsTypeOf(Person))"
by(rule cpI1, simp_all add: OclIsTypeOfPerson_OclAny)


lemma cp_OclIsTypeOfOclAny_Person_OclAny: "cp P ⟹ cp(λX.(P(X::Person)::OclAny).oclIsTypeOf(OclAny))"
by(rule cpI1, simp_all add: OclIsTypeOfOclAny_OclAny)
lemma cp_OclIsTypeOfOclAny_OclAny_Person: "cp P ⟹ cp(λX.(P(X::OclAny)::Person).oclIsTypeOf(OclAny))"
by(rule cpI1, simp_all add: OclIsTypeOfOclAny_Person)
lemma cp_OclIsTypeOfPerson_Person_OclAny: "cp P ⟹ cp(λX.(P(X::Person)::OclAny).oclIsTypeOf(Person))"
by(rule cpI1, simp_all add: OclIsTypeOfPerson_OclAny)
lemma cp_OclIsTypeOfPerson_OclAny_Person: "cp P ⟹ cp(λX.(P(X::OclAny)::Person).oclIsTypeOf(Person))"
by(rule cpI1, simp_all add: OclIsTypeOfPerson_Person)

lemmas [simp] =
 cp_OclIsTypeOfOclAny_Person_Person
 cp_OclIsTypeOfOclAny_OclAny_OclAny
 cp_OclIsTypeOfPerson_Person_Person
 cp_OclIsTypeOfPerson_OclAny_OclAny

 cp_OclIsTypeOfOclAny_Person_OclAny
 cp_OclIsTypeOfOclAny_OclAny_Person
 cp_OclIsTypeOfPerson_Person_OclAny
 cp_OclIsTypeOfPerson_OclAny_Person
text_raw‹\endisatagafp›

subsection‹Execution with Invalid or Null as Argument›

lemma OclIsTypeOfOclAny_OclAny_strict1[simp]:
     "(invalid::OclAny) .oclIsTypeOf(OclAny) = invalid"
by(rule ext, simp add: null_fun_def null_option_def bot_option_def null_def invalid_def
                       OclIsTypeOfOclAny_OclAny)
lemma OclIsTypeOfOclAny_OclAny_strict2[simp]:
     "(null::OclAny) .oclIsTypeOf(OclAny) = true"
by(rule ext, simp add: null_fun_def null_option_def bot_option_def null_def invalid_def
                       OclIsTypeOfOclAny_OclAny)
lemma OclIsTypeOfOclAny_Person_strict1[simp]:
     "(invalid::Person) .oclIsTypeOf(OclAny) = invalid"
by(rule ext, simp add: null_fun_def null_option_def bot_option_def null_def invalid_def
                       OclIsTypeOfOclAny_Person)
lemma OclIsTypeOfOclAny_Person_strict2[simp]:
     "(null::Person) .oclIsTypeOf(OclAny) = true"
by(rule ext, simp add: null_fun_def null_option_def bot_option_def null_def invalid_def
                       OclIsTypeOfOclAny_Person)
lemma OclIsTypeOfPerson_OclAny_strict1[simp]:
     "(invalid::OclAny) .oclIsTypeOf(Person) = invalid"
by(rule ext, simp add: null_fun_def null_option_def bot_option_def null_def invalid_def
                       OclIsTypeOfPerson_OclAny)
lemma OclIsTypeOfPerson_OclAny_strict2[simp]:
     "(null::OclAny) .oclIsTypeOf(Person) = true"
by(rule ext, simp add: null_fun_def null_option_def bot_option_def null_def invalid_def
                       OclIsTypeOfPerson_OclAny)
lemma OclIsTypeOfPerson_Person_strict1[simp]:
     "(invalid::Person) .oclIsTypeOf(Person) = invalid"
by(rule ext, simp add: null_fun_def null_option_def bot_option_def null_def invalid_def
                       OclIsTypeOfPerson_Person)
lemma OclIsTypeOfPerson_Person_strict2[simp]:
     "(null::Person) .oclIsTypeOf(Person) = true"
by(rule ext, simp add: null_fun_def null_option_def bot_option_def null_def invalid_def
                       OclIsTypeOfPerson_Person)

subsection‹Up Down Casting›

lemma actualType_larger_staticType:
assumes isdef: "τ ⊨ (δ X)"
shows          "τ ⊨ (X::Person) .oclIsTypeOf(OclAny) ≜ false"
using isdef
by(auto simp : null_option_def bot_option_def
               OclIsTypeOfOclAny_Person foundation22 foundation16)

lemma down_cast_type:
assumes isOclAny: "τ ⊨ (X::OclAny) .oclIsTypeOf(OclAny)"
and     non_null: "τ ⊨ (δ X)"
shows             "τ ⊨ (X .oclAsType(Person)) ≜ invalid"
using isOclAny non_null
apply(auto simp : bot_fun_def null_fun_def null_option_def bot_option_def null_def invalid_def
                  OclAsTypeOclAny_Person OclAsTypePerson_OclAny foundation22 foundation16
           split: option.split typeOclAny.split typePerson.split)
by(simp add: OclIsTypeOfOclAny_OclAny  OclValid_def false_def true_def)

lemma down_cast_type':
assumes isOclAny: "τ ⊨ (X::OclAny) .oclIsTypeOf(OclAny)"
and     non_null: "τ ⊨ (δ X)"
shows             "τ ⊨ not (υ (X .oclAsType(Person)))"
by(rule foundation15[THEN iffD1], simp add: down_cast_type[OF assms])

lemma up_down_cast :
assumes isdef: "τ ⊨ (δ X)"
shows "τ ⊨ ((X::Person) .oclAsType(OclAny) .oclAsType(Person) ≜ X)"
using isdef
by(auto simp : null_fun_def null_option_def bot_option_def null_def invalid_def
               OclAsTypeOclAny_Person OclAsTypePerson_OclAny foundation22 foundation16
        split: option.split typePerson.split)


lemma up_down_cast_Person_OclAny_Person [simp]:
shows "((X::Person) .oclAsType(OclAny) .oclAsType(Person) = X)"
 apply(rule ext, rename_tac τ)
 apply(rule foundation22[THEN iffD1])
 apply(case_tac "τ ⊨ (δ X)", simp add: up_down_cast)
 apply(simp add: defined_split, elim disjE)
 apply(erule StrongEq_L_subst2_rev, simp, simp)+
done

lemma up_down_cast_Person_OclAny_Person':
assumes "τ ⊨ υ X"
shows   "τ ⊨ (((X :: Person) .oclAsType(OclAny) .oclAsType(Person)) ≐ X)"
 apply(simp only: up_down_cast_Person_OclAny_Person StrictRefEqObject_Person)
by(rule StrictRefEqObject_sym, simp add: assms)

lemma up_down_cast_Person_OclAny_Person'': 
assumes "τ ⊨ υ (X :: Person)"
shows   "τ ⊨ (X .oclIsTypeOf(Person) implies (X .oclAsType(OclAny) .oclAsType(Person)) ≐ X)"
 apply(simp add: OclValid_def)
 apply(subst cp_OclImplies)
 apply(simp add: StrictRefEqObject_Person StrictRefEqObject_sym[OF assms, simplified OclValid_def])
 apply(subst cp_OclImplies[symmetric])
by simp


section‹OclIsKindOf›
subsection‹Definition›

consts OclIsKindOfOclAny :: "'α ⇒ Boolean" ("(_).oclIsKindOf'(OclAny')")
consts OclIsKindOfPerson :: "'α ⇒ Boolean" ("(_).oclIsKindOf'(Person')")

overloading OclIsKindOfOclAny ≡ "OclIsKindOfOclAny :: OclAny ⇒ Boolean"
begin
  definition OclIsKindOfOclAny_OclAny:
        "(X::OclAny) .oclIsKindOf(OclAny) ≡
                   (λτ. case X τ of
                              ⊥ ⇒ invalid τ
                            | _ ⇒ true τ)"
end

overloading OclIsKindOfOclAny ≡ "OclIsKindOfOclAny :: Person ⇒ Boolean"
begin
  definition OclIsKindOfOclAny_Person:
        "(X::Person) .oclIsKindOf(OclAny) ≡
                   (λτ. case X τ of
                              ⊥ ⇒ invalid τ
                            | _⇒ true τ)"
(* for (* ⌊⌊mkPerson e oid _ ⌋⌋ ⇒ true τ *) :  must have actual type Person otherwise  *)
end

overloading OclIsKindOfPerson ≡ "OclIsKindOfPerson :: OclAny ⇒ Boolean"
begin
  definition OclIsKindOfPerson_OclAny:
        "(X::OclAny) .oclIsKindOf(Person) ≡
                   (λτ. case X τ of
                              ⊥   ⇒ invalid τ
                            | ⌊⊥⌋ ⇒ true τ
                            | ⌊⌊mkOclAny oid ⊥ ⌋⌋ ⇒ false τ
                            | ⌊⌊mkOclAny oid ⌊_⌋ ⌋⌋ ⇒ true τ)"
end

overloading OclIsKindOfPerson ≡ "OclIsKindOfPerson :: Person ⇒ Boolean"
begin
 definition OclIsKindOfPerson_Person:
        "(X::Person) .oclIsKindOf(Person) ≡
                   (λτ. case X τ of
                              ⊥ ⇒ invalid τ
                            | _ ⇒ true τ)"
end
text_raw‹\isatagafp›
subsection‹Context Passing›

lemma cp_OclIsKindOfOclAny_Person_Person: "cp P ⟹ cp(λX.(P(X::Person)::Person).oclIsKindOf(OclAny))"
by(rule cpI1, simp_all add: OclIsKindOfOclAny_Person)
lemma cp_OclIsKindOfOclAny_OclAny_OclAny: "cp P ⟹ cp(λX.(P(X::OclAny)::OclAny).oclIsKindOf(OclAny))"
by(rule cpI1, simp_all add: OclIsKindOfOclAny_OclAny)
lemma cp_OclIsKindOfPerson_Person_Person: "cp P ⟹ cp(λX.(P(X::Person)::Person).oclIsKindOf(Person))"
by(rule cpI1, simp_all add: OclIsKindOfPerson_Person)
lemma cp_OclIsKindOfPerson_OclAny_OclAny: "cp P ⟹ cp(λX.(P(X::OclAny)::OclAny).oclIsKindOf(Person))"
by(rule cpI1, simp_all add: OclIsKindOfPerson_OclAny)

lemma cp_OclIsKindOfOclAny_Person_OclAny: "cp P ⟹ cp(λX.(P(X::Person)::OclAny).oclIsKindOf(OclAny))"
by(rule cpI1, simp_all add: OclIsKindOfOclAny_OclAny)
lemma cp_OclIsKindOfOclAny_OclAny_Person: "cp P ⟹ cp(λX.(P(X::OclAny)::Person).oclIsKindOf(OclAny))"
by(rule cpI1, simp_all add: OclIsKindOfOclAny_Person)
lemma cp_OclIsKindOfPerson_Person_OclAny: "cp P ⟹ cp(λX.(P(X::Person)::OclAny).oclIsKindOf(Person))"
by(rule cpI1, simp_all add: OclIsKindOfPerson_OclAny)
lemma cp_OclIsKindOfPerson_OclAny_Person: "cp P ⟹ cp(λX.(P(X::OclAny)::Person).oclIsKindOf(Person))"
by(rule cpI1, simp_all add: OclIsKindOfPerson_Person)

lemmas [simp] =
 cp_OclIsKindOfOclAny_Person_Person
 cp_OclIsKindOfOclAny_OclAny_OclAny
 cp_OclIsKindOfPerson_Person_Person
 cp_OclIsKindOfPerson_OclAny_OclAny

 cp_OclIsKindOfOclAny_Person_OclAny
 cp_OclIsKindOfOclAny_OclAny_Person
 cp_OclIsKindOfPerson_Person_OclAny
 cp_OclIsKindOfPerson_OclAny_Person
text_raw‹\endisatagafp›
subsection‹Execution with Invalid or Null as Argument›

lemma OclIsKindOfOclAny_OclAny_strict1[simp] : "(invalid::OclAny) .oclIsKindOf(OclAny) = invalid"
by(rule ext, simp add: invalid_def bot_option_def
                       OclIsKindOfOclAny_OclAny)
lemma OclIsKindOfOclAny_OclAny_strict2[simp] : "(null::OclAny) .oclIsKindOf(OclAny) = true"
by(rule ext, simp add: null_fun_def null_option_def
                       OclIsKindOfOclAny_OclAny)
lemma OclIsKindOfOclAny_Person_strict1[simp] : "(invalid::Person) .oclIsKindOf(OclAny) = invalid"
by(rule ext, simp add: bot_option_def invalid_def
                       OclIsKindOfOclAny_Person)
lemma OclIsKindOfOclAny_Person_strict2[simp] : "(null::Person) .oclIsKindOf(OclAny) = true"
by(rule ext, simp add: null_fun_def null_option_def bot_option_def
                       OclIsKindOfOclAny_Person)
lemma OclIsKindOfPerson_OclAny_strict1[simp]: "(invalid::OclAny) .oclIsKindOf(Person) = invalid"
by(rule ext, simp add: null_fun_def null_option_def bot_option_def null_def invalid_def
                       OclIsKindOfPerson_OclAny)
lemma OclIsKindOfPerson_OclAny_strict2[simp]: "(null::OclAny) .oclIsKindOf(Person) = true"
by(rule ext, simp add: null_fun_def null_option_def bot_option_def null_def invalid_def
                       OclIsKindOfPerson_OclAny)
lemma OclIsKindOfPerson_Person_strict1[simp]: "(invalid::Person) .oclIsKindOf(Person) = invalid"
by(rule ext, simp add: null_fun_def null_option_def bot_option_def null_def invalid_def
                       OclIsKindOfPerson_Person)
lemma OclIsKindOfPerson_Person_strict2[simp]: "(null::Person) .oclIsKindOf(Person) = true"
by(rule ext, simp add: null_fun_def null_option_def bot_option_def null_def invalid_def
                       OclIsKindOfPerson_Person)

subsection‹Up Down Casting›

lemma actualKind_larger_staticKind:
assumes isdef: "τ ⊨ (δ X)"
shows          "τ ⊨  ((X::Person) .oclIsKindOf(OclAny) ≜ true)"
using isdef
by(auto simp : bot_option_def
               OclIsKindOfOclAny_Person foundation22 foundation16)

lemma down_cast_kind:
assumes isOclAny: "¬ (τ ⊨ ((X::OclAny).oclIsKindOf(Person)))"
and     non_null: "τ ⊨ (δ X)"
shows             "τ ⊨ ((X .oclAsType(Person)) ≜ invalid)"
using isOclAny non_null
apply(auto simp : bot_fun_def null_fun_def null_option_def bot_option_def null_def invalid_def
                  OclAsTypeOclAny_Person OclAsTypePerson_OclAny foundation22 foundation16
           split: option.split typeOclAny.split typePerson.split)
by(simp add: OclIsKindOfPerson_OclAny  OclValid_def false_def true_def)

section‹OclAllInstances›

text‹To denote OCL-types occurring in OCL expressions syntactically---as, for example,  as
``argument'' of \inlineisar{oclAllInstances()}---we use the inverses of the injection
functions into the object universes; we show that this is sufficient ``characterization.''›

definition "Person ≡ OclAsTypePerson_𝔄"
definition "OclAny ≡ OclAsTypeOclAny_𝔄"
lemmas [simp] = Person_def OclAny_def

lemma OclAllInstances_genericOclAny_exec: "OclAllInstances_generic pre_post OclAny =
             (λτ.  Abs_Setbase  ⌊⌊ Some ` OclAny ` ran (heap (pre_post τ)) ⌋⌋)"
proof -
 let ?S1 = "λτ. OclAny ` ran (heap (pre_post τ))"
 let ?S2 = "λτ. ?S1 τ - {None}"
 have B : "⋀τ. ?S2 τ ⊆ ?S1 τ" by auto
 have C : "⋀τ. ?S1 τ ⊆ ?S2 τ" by(auto simp: OclAsTypeOclAny_𝔄_some)

 show ?thesis by(insert equalityI[OF B C], simp)
qed

lemma OclAllInstances_at_postOclAny_exec: "OclAny .allInstances() =
             (λτ.  Abs_Setbase  ⌊⌊ Some ` OclAny ` ran (heap (snd τ)) ⌋⌋)"
unfolding OclAllInstances_at_post_def
by(rule OclAllInstances_genericOclAny_exec)

lemma OclAllInstances_at_preOclAny_exec: "OclAny .allInstances@pre() =
             (λτ.  Abs_Setbase  ⌊⌊ Some ` OclAny ` ran (heap (fst τ)) ⌋⌋) "
unfolding OclAllInstances_at_pre_def
by(rule OclAllInstances_genericOclAny_exec)

subsection‹OclIsTypeOf›

lemma OclAny_allInstances_generic_oclIsTypeOfOclAny1:
assumes [simp]: "⋀x. pre_post (x, x) = x"
shows "∃τ. (τ ⊨     ((OclAllInstances_generic pre_post OclAny)->forAllSet(X|X .oclIsTypeOf(OclAny))))"
 apply(rule_tac x = τ0 in exI, simp add: τ0_def OclValid_def del: OclAllInstances_generic_def)
 apply(simp only: assms UML_Set.OclForall_def refl if_True
                  OclAllInstances_generic_defined[simplified OclValid_def])
 apply(simp only: OclAllInstances_generic_def)
 apply(subst (1 2 3) Abs_Setbase_inverse, simp add: bot_option_def)
by(simp add: OclIsTypeOfOclAny_OclAny)

lemma OclAny_allInstances_at_post_oclIsTypeOfOclAny1:
"∃τ. (τ ⊨     (OclAny .allInstances()->forAllSet(X|X .oclIsTypeOf(OclAny))))"
unfolding OclAllInstances_at_post_def
by(rule OclAny_allInstances_generic_oclIsTypeOfOclAny1, simp)

lemma OclAny_allInstances_at_pre_oclIsTypeOfOclAny1:
"∃τ. (τ ⊨     (OclAny .allInstances@pre()->forAllSet(X|X .oclIsTypeOf(OclAny))))"
unfolding OclAllInstances_at_pre_def
by(rule OclAny_allInstances_generic_oclIsTypeOfOclAny1, simp)

lemma OclAny_allInstances_generic_oclIsTypeOfOclAny2:
assumes [simp]: "⋀x. pre_post (x, x) = x"
shows "∃τ. (τ ⊨ not ((OclAllInstances_generic pre_post OclAny)->forAllSet(X|X .oclIsTypeOf(OclAny))))"
proof - fix oid a let ?t0 = "⦇heap = Map.empty(oid ↦ inOclAny (mkOclAny oid ⌊a⌋)),
                              assocs = Map.empty⦈" show ?thesis
 apply(rule_tac x = "(?t0, ?t0)" in exI, simp add: OclValid_def del: OclAllInstances_generic_def)
 apply(simp only: UML_Set.OclForall_def refl if_True
                  OclAllInstances_generic_defined[simplified OclValid_def])
 apply(simp only: OclAllInstances_generic_def OclAsTypeOclAny_𝔄_def)
 apply(subst (1 2 3) Abs_Setbase_inverse, simp add: bot_option_def)
 by(simp add: OclIsTypeOfOclAny_OclAny OclNot_def OclAny_def)
qed

lemma OclAny_allInstances_at_post_oclIsTypeOfOclAny2:
"∃τ. (τ ⊨ not (OclAny .allInstances()->forAllSet(X|X .oclIsTypeOf(OclAny))))"
unfolding OclAllInstances_at_post_def
by(rule OclAny_allInstances_generic_oclIsTypeOfOclAny2, simp)

lemma OclAny_allInstances_at_pre_oclIsTypeOfOclAny2:
"∃τ. (τ ⊨ not (OclAny .allInstances@pre()->forAllSet(X|X .oclIsTypeOf(OclAny))))"
unfolding OclAllInstances_at_pre_def
by(rule OclAny_allInstances_generic_oclIsTypeOfOclAny2, simp)

lemma Person_allInstances_generic_oclIsTypeOfPerson:
"τ ⊨ ((OclAllInstances_generic pre_post Person)->forAllSet(X|X .oclIsTypeOf(Person)))"
 apply(simp add: OclValid_def del: OclAllInstances_generic_def)
 apply(simp only: UML_Set.OclForall_def refl if_True
                  OclAllInstances_generic_defined[simplified OclValid_def])
 apply(simp only: OclAllInstances_generic_def)
 apply(subst (1 2 3) Abs_Setbase_inverse, simp add: bot_option_def)
by(simp add: OclIsTypeOfPerson_Person)

lemma Person_allInstances_at_post_oclIsTypeOfPerson:
"τ ⊨ (Person .allInstances()->forAllSet(X|X .oclIsTypeOf(Person)))"
unfolding OclAllInstances_at_post_def
by(rule Person_allInstances_generic_oclIsTypeOfPerson)

lemma Person_allInstances_at_pre_oclIsTypeOfPerson:
"τ ⊨ (Person .allInstances@pre()->forAllSet(X|X .oclIsTypeOf(Person)))"
unfolding OclAllInstances_at_pre_def
by(rule Person_allInstances_generic_oclIsTypeOfPerson)

subsection‹OclIsKindOf›
lemma OclAny_allInstances_generic_oclIsKindOfOclAny:
"τ ⊨ ((OclAllInstances_generic pre_post OclAny)->forAllSet(X|X .oclIsKindOf(OclAny)))"
 apply(simp add: OclValid_def del: OclAllInstances_generic_def)
 apply(simp only: UML_Set.OclForall_def refl if_True
                  OclAllInstances_generic_defined[simplified OclValid_def])
 apply(simp only: OclAllInstances_generic_def)
 apply(subst (1 2 3) Abs_Setbase_inverse, simp add: bot_option_def)
by(simp add: OclIsKindOfOclAny_OclAny)

lemma OclAny_allInstances_at_post_oclIsKindOfOclAny:
"τ ⊨ (OclAny .allInstances()->forAllSet(X|X .oclIsKindOf(OclAny)))"
unfolding OclAllInstances_at_post_def
by(rule OclAny_allInstances_generic_oclIsKindOfOclAny)

lemma OclAny_allInstances_at_pre_oclIsKindOfOclAny:
"τ ⊨ (OclAny .allInstances@pre()->forAllSet(X|X .oclIsKindOf(OclAny)))"
unfolding OclAllInstances_at_pre_def
by(rule OclAny_allInstances_generic_oclIsKindOfOclAny)

lemma Person_allInstances_generic_oclIsKindOfOclAny:
"τ ⊨ ((OclAllInstances_generic pre_post Person)->forAllSet(X|X .oclIsKindOf(OclAny)))"
 apply(simp add: OclValid_def del: OclAllInstances_generic_def)
 apply(simp only: UML_Set.OclForall_def refl if_True
                  OclAllInstances_generic_defined[simplified OclValid_def])
 apply(simp only: OclAllInstances_generic_def)
 apply(subst (1 2 3) Abs_Setbase_inverse, simp add: bot_option_def)
by(simp add: OclIsKindOfOclAny_Person)

lemma Person_allInstances_at_post_oclIsKindOfOclAny:
"τ ⊨ (Person .allInstances()->forAllSet(X|X .oclIsKindOf(OclAny)))"
unfolding OclAllInstances_at_post_def
by(rule Person_allInstances_generic_oclIsKindOfOclAny)

lemma Person_allInstances_at_pre_oclIsKindOfOclAny:
"τ ⊨ (Person .allInstances@pre()->forAllSet(X|X .oclIsKindOf(OclAny)))"
unfolding OclAllInstances_at_pre_def
by(rule Person_allInstances_generic_oclIsKindOfOclAny)

lemma Person_allInstances_generic_oclIsKindOfPerson:
"τ ⊨ ((OclAllInstances_generic pre_post Person)->forAllSet(X|X .oclIsKindOf(Person)))"
 apply(simp add: OclValid_def del: OclAllInstances_generic_def)
 apply(simp only: UML_Set.OclForall_def refl if_True
                  OclAllInstances_generic_defined[simplified OclValid_def])
 apply(simp only: OclAllInstances_generic_def)
 apply(subst (1 2 3) Abs_Setbase_inverse, simp add: bot_option_def)
by(simp add: OclIsKindOfPerson_Person)

lemma Person_allInstances_at_post_oclIsKindOfPerson:
"τ ⊨ (Person .allInstances()->forAllSet(X|X .oclIsKindOf(Person)))"
unfolding OclAllInstances_at_post_def
by(rule Person_allInstances_generic_oclIsKindOfPerson)

lemma Person_allInstances_at_pre_oclIsKindOfPerson:
"τ ⊨ (Person .allInstances@pre()->forAllSet(X|X .oclIsKindOf(Person)))"
unfolding OclAllInstances_at_pre_def
by(rule Person_allInstances_generic_oclIsKindOfPerson)

section‹The Accessors (any, boss, salary)›
text‹\label{sec:edm-accessors}›
text‹Should be generated entirely from a class-diagram.›


subsection‹Definition›

definition eval_extract :: "('𝔄,('a::object) option option) val
                            ⇒ (oid ⇒ ('𝔄,'c::null) val)
                            ⇒ ('𝔄,'c::null) val"
where "eval_extract X f = (λ τ. case X τ of
                                    ⊥ ⇒ invalid τ   ― ‹exception propagation›
                               | ⌊  ⊥ ⌋ ⇒ invalid τ ― ‹dereferencing null pointer›
                               | ⌊⌊ obj ⌋⌋ ⇒ f (oid_of obj) τ)"


definition deref_oidPerson :: "(𝔄 state × 𝔄 state ⇒ 𝔄 state)
                             ⇒ (typePerson ⇒ (𝔄, 'c::null)val)
                             ⇒ oid
                             ⇒ (𝔄, 'c::null)val"
where "deref_oidPerson fst_snd f oid = (λτ. case (heap (fst_snd τ)) oid of
                                              ⌊ inPerson obj ⌋ ⇒ f obj τ
                                            | _              ⇒ invalid τ)"



definition deref_oidOclAny :: "(𝔄 state × 𝔄 state ⇒ 𝔄 state)
                             ⇒ (typeOclAny ⇒ (𝔄, 'c::null)val)
                             ⇒ oid
                             ⇒ (𝔄, 'c::null)val"
where "deref_oidOclAny fst_snd f oid = (λτ. case (heap (fst_snd τ)) oid of
                       ⌊ inOclAny obj ⌋ ⇒ f obj τ
                     | _       ⇒ invalid τ)"

text‹pointer undefined in state or not referencing a type conform object representation›


definition "selectOclAny𝒜𝒩𝒴 f = (λ X. case X of
                     (mkOclAny _ ⊥) ⇒ null
                   | (mkOclAny _ ⌊any⌋) ⇒ f (λx _. ⌊⌊x⌋⌋) any)"


definition "selectPersonℬ𝒪𝒮𝒮 f = (λ X. case X of
                     (mkPerson _ _ ⊥) ⇒ null  ― ‹object contains null pointer›
                   | (mkPerson _ _ ⌊boss⌋) ⇒ f (λx _. ⌊⌊x⌋⌋) boss)"


definition "selectPerson𝒮𝒜ℒ𝒜ℛ𝒴 f = (λ X. case X of
                     (mkPerson _ ⊥ _) ⇒ null
                   | (mkPerson _ ⌊salary⌋ _) ⇒ f (λx _. ⌊⌊x⌋⌋) salary)"


definition "in_pre_state = fst"
definition "in_post_state = snd"

definition "reconst_basetype = (λ convert x. convert x)"

definition dotOclAny𝒜𝒩𝒴 :: "OclAny ⇒ _"  ("(1(_).any)" 50)
  where "(X).any = eval_extract X
                     (deref_oidOclAny in_post_state
                       (selectOclAny𝒜𝒩𝒴
                         reconst_basetype))"

definition dotPersonℬ𝒪𝒮𝒮 :: "Person ⇒ Person"  ("(1(_).boss)" 50)
  where "(X).boss = eval_extract X
                      (deref_oidPerson in_post_state
                        (selectPersonℬ𝒪𝒮𝒮
                          (deref_oidPerson in_post_state)))"

definition dotPerson𝒮𝒜ℒ𝒜ℛ𝒴 :: "Person ⇒ Integer"  ("(1(_).salary)" 50)
  where "(X).salary = eval_extract X
                        (deref_oidPerson in_post_state
                          (selectPerson𝒮𝒜ℒ𝒜ℛ𝒴
                            reconst_basetype))"

definition dotOclAny𝒜𝒩𝒴_at_pre :: "OclAny ⇒ _"  ("(1(_).any@pre)" 50)
  where "(X).any@pre = eval_extract X
                         (deref_oidOclAny in_pre_state
                           (selectOclAny𝒜𝒩𝒴
                             reconst_basetype))"

definition dotPersonℬ𝒪𝒮𝒮_at_pre:: "Person ⇒ Person"  ("(1(_).boss@pre)" 50)
  where "(X).boss@pre = eval_extract X
                          (deref_oidPerson in_pre_state
                            (selectPersonℬ𝒪𝒮𝒮
                              (deref_oidPerson in_pre_state)))"

definition dotPerson𝒮𝒜ℒ𝒜ℛ𝒴_at_pre:: "Person ⇒ Integer"  ("(1(_).salary@pre)" 50)
  where "(X).salary@pre = eval_extract X
                            (deref_oidPerson in_pre_state
                              (selectPerson𝒮𝒜ℒ𝒜ℛ𝒴
                                reconst_basetype))"

lemmas dot_accessor =
  dotOclAny𝒜𝒩𝒴_def
  dotPersonℬ𝒪𝒮𝒮_def
  dotPerson𝒮𝒜ℒ𝒜ℛ𝒴_def
  dotOclAny𝒜𝒩𝒴_at_pre_def
  dotPersonℬ𝒪𝒮𝒮_at_pre_def
  dotPerson𝒮𝒜ℒ𝒜ℛ𝒴_at_pre_def

subsection‹Context Passing›

lemmas [simp] = eval_extract_def

lemma cp_dotOclAny𝒜𝒩𝒴: "((X).any) τ = ((λ_. X τ).any) τ" by (simp add: dot_accessor)
lemma cp_dotPersonℬ𝒪𝒮𝒮: "((X).boss) τ = ((λ_. X τ).boss) τ" by (simp add: dot_accessor)
lemma cp_dotPerson𝒮𝒜ℒ𝒜ℛ𝒴: "((X).salary) τ = ((λ_. X τ).salary) τ" by (simp add: dot_accessor)

lemma cp_dotOclAny𝒜𝒩𝒴_at_pre: "((X).any@pre) τ = ((λ_. X τ).any@pre) τ" by (simp add: dot_accessor)
lemma cp_dotPersonℬ𝒪𝒮𝒮_at_pre: "((X).boss@pre) τ = ((λ_. X τ).boss@pre) τ" by (simp add: dot_accessor)
lemma cp_dotPerson𝒮𝒜ℒ𝒜ℛ𝒴_at_pre: "((X).salary@pre) τ = ((λ_. X τ).salary@pre) τ" by (simp add: dot_accessor)

lemmas cp_dotOclAny𝒜𝒩𝒴_I [simp, intro!]=
       cp_dotOclAny𝒜𝒩𝒴[THEN allI[THEN allI],
                          of "λ X _. X" "λ _ τ. τ", THEN cpI1]
lemmas cp_dotOclAny𝒜𝒩𝒴_at_pre_I [simp, intro!]=
       cp_dotOclAny𝒜𝒩𝒴_at_pre[THEN allI[THEN allI],
                          of "λ X _. X" "λ _ τ. τ", THEN cpI1]

lemmas cp_dotPersonℬ𝒪𝒮𝒮_I [simp, intro!]=
       cp_dotPersonℬ𝒪𝒮𝒮[THEN allI[THEN allI],
                          of "λ X _. X" "λ _ τ. τ", THEN cpI1]
lemmas cp_dotPersonℬ𝒪𝒮𝒮_at_pre_I [simp, intro!]=
       cp_dotPersonℬ𝒪𝒮𝒮_at_pre[THEN allI[THEN allI],
                          of "λ X _. X" "λ _ τ. τ", THEN cpI1]

lemmas cp_dotPerson𝒮𝒜ℒ𝒜ℛ𝒴_I [simp, intro!]=
       cp_dotPerson𝒮𝒜ℒ𝒜ℛ𝒴[THEN allI[THEN allI],
                          of "λ X _. X" "λ _ τ. τ", THEN cpI1]
lemmas cp_dotPerson𝒮𝒜ℒ𝒜ℛ𝒴_at_pre_I [simp, intro!]=
       cp_dotPerson𝒮𝒜ℒ𝒜ℛ𝒴_at_pre[THEN allI[THEN allI],
                          of "λ X _. X" "λ _ τ. τ", THEN cpI1]

subsection‹Execution with Invalid or Null as Argument›

lemma dotOclAny𝒜𝒩𝒴_nullstrict [simp]: "(null).any = invalid"
by(rule ext, simp add: dot_accessor null_fun_def null_option_def bot_option_def null_def invalid_def)
lemma dotOclAny𝒜𝒩𝒴_at_pre_nullstrict [simp] : "(null).any@pre = invalid"
by(rule ext, simp add: dot_accessor null_fun_def null_option_def bot_option_def null_def invalid_def)
lemma dotOclAny𝒜𝒩𝒴_strict [simp] : "(invalid).any = invalid"
by(rule ext, simp add: dot_accessor null_fun_def null_option_def bot_option_def null_def invalid_def)
lemma dotOclAny𝒜𝒩𝒴_at_pre_strict [simp] : "(invalid).any@pre = invalid"
by(rule ext, simp add: dot_accessor null_fun_def null_option_def bot_option_def null_def invalid_def)


lemma dotPersonℬ𝒪𝒮𝒮_nullstrict [simp]: "(null).boss = invalid"
by(rule ext, simp add: dot_accessor null_fun_def null_option_def bot_option_def null_def invalid_def)
lemma dotPersonℬ𝒪𝒮𝒮_at_pre_nullstrict [simp] : "(null).boss@pre = invalid"
by(rule ext, simp add: dot_accessor null_fun_def null_option_def bot_option_def null_def invalid_def)
lemma dotPersonℬ𝒪𝒮𝒮_strict [simp] : "(invalid).boss = invalid"
by(rule ext, simp add: dot_accessor null_fun_def null_option_def bot_option_def null_def invalid_def)
lemma dotPersonℬ𝒪𝒮𝒮_at_pre_strict [simp] : "(invalid).boss@pre = invalid"
by(rule ext, simp add: dot_accessor null_fun_def null_option_def bot_option_def null_def invalid_def)


lemma dotPerson𝒮𝒜ℒ𝒜ℛ𝒴_nullstrict [simp]: "(null).salary = invalid"
by(rule ext, simp add: dot_accessor null_fun_def null_option_def bot_option_def null_def invalid_def)
lemma dotPerson𝒮𝒜ℒ𝒜ℛ𝒴_at_pre_nullstrict [simp] : "(null).salary@pre = invalid"
by(rule ext, simp add: dot_accessor null_fun_def null_option_def bot_option_def null_def invalid_def)
lemma dotPerson𝒮𝒜ℒ𝒜ℛ𝒴_strict [simp] : "(invalid).salary = invalid"
by(rule ext, simp add: dot_accessor null_fun_def null_option_def bot_option_def null_def invalid_def)
lemma dotPerson𝒮𝒜ℒ𝒜ℛ𝒴_at_pre_strict [simp] : "(invalid).salary@pre = invalid"
by(rule ext, simp add: dot_accessor null_fun_def null_option_def bot_option_def null_def invalid_def)

subsection‹Representation in States›

lemma dotPersonℬ𝒪𝒮𝒮_def_mono:"τ ⊨ δ(X .boss) ⟹ τ ⊨ δ(X)"
  apply(case_tac "τ ⊨ (X ≜ invalid)", insert StrongEq_L_subst2[where P = "(λx. (δ (x .boss)))" and τ = "τ" and x = "X" and y = "invalid"], simp add: foundation16')
  apply(case_tac "τ ⊨ (X ≜ null)", insert StrongEq_L_subst2[where P = "(λx. (δ (x .boss)))" and τ = "τ" and x = "X" and y = "null"], simp add: foundation16')
by(simp add: defined_split)

lemma repr_boss:  
assumes A : "τ ⊨ δ(x .boss)"
shows      "is_represented_in_state in_post_state (x .boss) Person τ"
         apply(insert A[simplified foundation16]
                      A[THEN dotPersonℬ𝒪𝒮𝒮_def_mono, simplified foundation16])
         unfolding is_represented_in_state_def
                   dotPersonℬ𝒪𝒮𝒮_def eval_extract_def selectPersonℬ𝒪𝒮𝒮_def in_post_state_def
         by(auto simp: deref_oidPerson_def bot_fun_def bot_option_def null_option_def null_fun_def invalid_def
                       OclAsTypePerson_𝔄_def image_def ran_def
                 split: typePerson.split option.split 𝔄.split)

lemma repr_bossX : 
assumes A: "τ ⊨ δ(x .boss)"
shows "τ ⊨ ((Person .allInstances()) ->includesSet(x .boss))"
proof -
  have B : "⋀S f. (x .boss) τ ∈ (Some ` f ` S) ⟹
                  (x .boss) τ ∈ (Some ` (f ` S - {None}))"
            apply(auto simp: image_def ran_def, metis)
  by(insert A[simplified foundation16], simp add: null_option_def bot_option_def)
  show ?thesis
         apply(insert repr_boss[OF A] OclAllInstances_at_post_defined[where H = Person and τ = τ])
         unfolding is_represented_in_state_def OclValid_def
                   OclAllInstances_at_post_def OclAllInstances_generic_def OclIncludes_def
                   in_post_state_def
         apply(simp add: A[THEN foundation20, simplified OclValid_def])
         apply(subst Abs_Setbase_inverse, simp, metis bot_option_def option.distinct(1))
  by(simp add: image_comp B true_def)
qed

section‹A Little Infra-structure on Example States›

text‹
The example we are defining in this section comes from the figure~\ref{fig:edm1_system-states}.
\begin{figure}
\includegraphics[width=\textwidth]{figures/pre-post.pdf}
\caption{(a) pre-state $\sigma_1$ and
  (b) post-state $\sigma_1'$.}
\label{fig:edm1_system-states}
\end{figure}
›

text_raw‹\isatagafp›

definition OclInt1000 ("𝟭𝟬𝟬𝟬") where "OclInt1000 = (λ _ . ⌊⌊1000⌋⌋)"
definition OclInt1200 ("𝟭𝟮𝟬𝟬") where "OclInt1200 = (λ _ . ⌊⌊1200⌋⌋)"
definition OclInt1300 ("𝟭𝟯𝟬𝟬") where "OclInt1300 = (λ _ . ⌊⌊1300⌋⌋)"
definition OclInt1800 ("𝟭𝟴𝟬𝟬") where "OclInt1800 = (λ _ . ⌊⌊1800⌋⌋)"
definition OclInt2600 ("𝟮𝟲𝟬𝟬") where "OclInt2600 = (λ _ . ⌊⌊2600⌋⌋)"
definition OclInt2900 ("𝟮𝟵𝟬𝟬") where "OclInt2900 = (λ _ . ⌊⌊2900⌋⌋)"
definition OclInt3200 ("𝟯𝟮𝟬𝟬") where "OclInt3200 = (λ _ . ⌊⌊3200⌋⌋)"
definition OclInt3500 ("𝟯𝟱𝟬𝟬") where "OclInt3500 = (λ _ . ⌊⌊3500⌋⌋)"

definition "oid0 ≡ 0"
definition "oid1 ≡ 1"
definition "oid2 ≡ 2"
definition "oid3 ≡ 3"
definition "oid4 ≡ 4"
definition "oid5 ≡ 5"
definition "oid6 ≡ 6"
definition "oid7 ≡ 7"
definition "oid8 ≡ 8"

definition "person1 ≡ mkPerson oid0 ⌊1300⌋ ⌊oid1⌋"
definition "person2 ≡ mkPerson oid1 ⌊1800⌋ ⌊oid1⌋"
definition "person3 ≡ mkPerson oid2 None None"
definition "person4 ≡ mkPerson oid3 ⌊2900⌋ None"
definition "person5 ≡ mkPerson oid4 ⌊3500⌋ None"
definition "person6 ≡ mkPerson oid5 ⌊2500⌋ ⌊oid6⌋"
definition "person7 ≡ mkOclAny oid6 ⌊(⌊3200⌋, ⌊oid6⌋)⌋"
definition "person8 ≡ mkOclAny oid7 None"
definition "person9 ≡ mkPerson oid8 ⌊0⌋ None"

definition
      "σ1  ≡ ⦇ heap = Map.empty(oid0 ↦ inPerson (mkPerson oid0 ⌊1000⌋ ⌊oid1⌋),
                           oid1 ↦ inPerson (mkPerson oid1 ⌊1200⌋  None),
                           ⌦‹oid2›
                           oid3 ↦ inPerson (mkPerson oid3 ⌊2600⌋ ⌊oid4⌋),
                           oid4 ↦ inPerson person5,
                           oid5 ↦ inPerson (mkPerson oid5 ⌊2300⌋ ⌊oid3⌋),
                           ⌦‹oid6›
                           ⌦‹oid7›
                           oid8 ↦ inPerson person9),
               assocs = Map.empty ⦈"

definition
      "σ1' ≡ ⦇ heap = Map.empty(oid0 ↦ inPerson person1,
                           oid1 ↦ inPerson person2,
                           oid2 ↦ inPerson person3,
                           oid3 ↦ inPerson person4,
                           ⌦‹oid4›
                           oid5 ↦ inPerson person6,
                           oid6 ↦ inOclAny person7,
                           oid7 ↦ inOclAny person8,
                           oid8 ↦ inPerson person9),
               assocs = Map.empty ⦈"

definition "σ0 ≡ ⦇ heap = Map.empty, assocs = Map.empty ⦈"


lemma basic_τ_wff: "WFF(σ1,σ1')"
by(auto simp: WFF_def σ1_def σ1'_def
              oid0_def oid1_def oid2_def oid3_def oid4_def oid5_def oid6_def oid7_def oid8_def
              oid_of_𝔄_def oid_of_typePerson_def oid_of_typeOclAny_def
              person1_def person2_def person3_def person4_def
              person5_def person6_def person7_def person8_def person9_def)

lemma [simp,code_unfold]: "dom (heap σ1) = {oid0,oid1⌦‹,oid2›,oid3,oid4,oid5⌦‹,oid6,oid7›,oid8}"
by(auto simp: σ1_def)

lemma [simp,code_unfold]: "dom (heap σ1') = {oid0,oid1,oid2,oid3⌦‹,oid4›,oid5,oid6,oid7,oid8}"
by(auto simp: σ1'_def)

text_raw‹\isatagafp›

definition "XPerson1 :: Person ≡ λ _ .⌊⌊ person1 ⌋⌋"
definition "XPerson2 :: Person ≡ λ _ .⌊⌊ person2 ⌋⌋"
definition "XPerson3 :: Person ≡ λ _ .⌊⌊ person3 ⌋⌋"
definition "XPerson4 :: Person ≡ λ _ .⌊⌊ person4 ⌋⌋"
definition "XPerson5 :: Person ≡ λ _ .⌊⌊ person5 ⌋⌋"
definition "XPerson6 :: Person ≡ λ _ .⌊⌊ person6 ⌋⌋"
definition "XPerson7 :: OclAny ≡ λ _ .⌊⌊ person7 ⌋⌋"
definition "XPerson8 :: OclAny ≡ λ _ .⌊⌊ person8 ⌋⌋"
definition "XPerson9 :: Person ≡ λ _ .⌊⌊ person9 ⌋⌋"

lemma [code_unfold]: "((x::Person) ≐ y) = StrictRefEqObject x y" by(simp only: StrictRefEqObject_Person)
lemma [code_unfold]: "((x::OclAny) ≐ y) = StrictRefEqObject x y" by(simp only: StrictRefEqObject_OclAny)

lemmas [simp,code_unfold] =
 OclAsTypeOclAny_OclAny
 OclAsTypeOclAny_Person
 OclAsTypePerson_OclAny
 OclAsTypePerson_Person

 OclIsTypeOfOclAny_OclAny
 OclIsTypeOfOclAny_Person
 OclIsTypeOfPerson_OclAny
 OclIsTypeOfPerson_Person

 OclIsKindOfOclAny_OclAny
 OclIsKindOfOclAny_Person
 OclIsKindOfPerson_OclAny
 OclIsKindOfPerson_Person
text_raw‹\endisatagafp›

Assert "⋀spre     .   (spre,σ1') ⊨      (XPerson1 .salary    <> 𝟭𝟬𝟬𝟬)"
Assert "⋀spre     .   (spre,σ1') ⊨      (XPerson1 .salary    ≐ 𝟭𝟯𝟬𝟬)"
Assert "⋀    spost.   (σ1,spost) ⊨      (XPerson1 .salary@pre     ≐ 𝟭𝟬𝟬𝟬)"
Assert "⋀    spost.   (σ1,spost) ⊨      (XPerson1 .salary@pre     <> 𝟭𝟯𝟬𝟬)"
Assert "⋀spre     .   (spre,σ1') ⊨      (XPerson1 .boss   <> XPerson1)"
Assert "⋀spre     .   (spre,σ1') ⊨      (XPerson1 .boss .salary   ≐ 𝟭𝟴𝟬𝟬)"
Assert "⋀spre     .   (spre,σ1') ⊨      (XPerson1 .boss .boss  <> XPerson1)"
Assert "⋀spre     .   (spre,σ1') ⊨      (XPerson1 .boss .boss  ≐ XPerson2)"
Assert "               (σ1,σ1') ⊨      (XPerson1 .boss@pre .salary  ≐ 𝟭𝟴𝟬𝟬)"
Assert "⋀    spost.   (σ1,spost) ⊨      (XPerson1 .boss@pre .salary@pre  ≐ 𝟭𝟮𝟬𝟬)"
Assert "⋀    spost.   (σ1,spost) ⊨      (XPerson1 .boss@pre .salary@pre  <> 𝟭𝟴𝟬𝟬)"
Assert "⋀    spost.   (σ1,spost) ⊨      (XPerson1 .boss@pre  ≐ XPerson2)"
Assert "               (σ1,σ1') ⊨      (XPerson1 .boss@pre .boss  ≐ XPerson2)"
Assert "⋀    spost.   (σ1,spost) ⊨      (XPerson1 .boss@pre .boss@pre  ≐ null)"
Assert "⋀    spost.   (σ1,spost) ⊨ not(υ(XPerson1 .boss@pre .boss@pre .boss@pre))"

lemma "               (σ1,σ1') ⊨      (XPerson1 .oclIsMaintained())"
by(simp add: OclValid_def OclIsMaintained_def
             σ1_def σ1'_def
             XPerson1_def person1_def
             oid0_def oid1_def oid2_def oid3_def oid4_def oid5_def oid6_def
             oid_of_option_def oid_of_typePerson_def)

lemma "⋀spre spost.   (spre,spost) ⊨    ((XPerson1 .oclAsType(OclAny) .oclAsType(Person)) ≐ XPerson1)"
by(rule up_down_cast_Person_OclAny_Person', simp add: XPerson1_def)
Assert "⋀spre spost.   (spre,spost) ⊨     (XPerson1 .oclIsTypeOf(Person))"
Assert "⋀spre spost.   (spre,spost) ⊨  not(XPerson1 .oclIsTypeOf(OclAny))"
Assert "⋀spre spost.   (spre,spost) ⊨     (XPerson1 .oclIsKindOf(Person))"
Assert "⋀spre spost.   (spre,spost) ⊨     (XPerson1 .oclIsKindOf(OclAny))"
Assert "⋀spre spost.   (spre,spost) ⊨  not(XPerson1 .oclAsType(OclAny) .oclIsTypeOf(OclAny))"


Assert "⋀spre     .   (spre,σ1') ⊨      (XPerson2 .salary       ≐ 𝟭𝟴𝟬𝟬)"
Assert "⋀    spost.   (σ1,spost) ⊨      (XPerson2 .salary@pre   ≐ 𝟭𝟮𝟬𝟬)"
Assert "⋀spre     .   (spre,σ1') ⊨      (XPerson2 .boss      ≐ XPerson2)"
Assert "               (σ1,σ1') ⊨      (XPerson2 .boss .salary@pre      ≐ 𝟭𝟮𝟬𝟬)"
Assert "               (σ1,σ1') ⊨      (XPerson2 .boss .boss@pre      ≐ null)"
Assert "⋀    spost.   (σ1,spost) ⊨      (XPerson2 .boss@pre  ≐ null)"
Assert "⋀    spost.   (σ1,spost) ⊨      (XPerson2 .boss@pre  <> XPerson2)"
Assert "               (σ1,σ1') ⊨      (XPerson2 .boss@pre  <> (XPerson2 .boss))"
Assert "⋀    spost.   (σ1,spost) ⊨ not(υ(XPerson2 .boss@pre .boss))"
Assert "⋀    spost.   (σ1,spost) ⊨ not(υ(XPerson2 .boss@pre .salary@pre))"
lemma "               (σ1,σ1') ⊨      (XPerson2 .oclIsMaintained())"
by(simp add: OclValid_def OclIsMaintained_def σ1_def σ1'_def XPerson2_def person2_def
             oid0_def oid1_def oid2_def oid3_def oid4_def oid5_def oid6_def
             oid_of_option_def oid_of_typePerson_def)

Assert "⋀spre     .   (spre,σ1') ⊨      (XPerson3 .salary       ≐ null)"
Assert "⋀    spost.   (σ1,spost) ⊨ not(υ(XPerson3 .salary@pre))"
Assert "⋀spre     .   (spre,σ1') ⊨      (XPerson3 .boss       ≐ null)"
Assert "⋀spre     .   (spre,σ1') ⊨ not(υ(XPerson3 .boss .salary))"
Assert "⋀    spost.   (σ1,spost) ⊨ not(υ(XPerson3 .boss@pre))"
lemma "               (σ1,σ1') ⊨      (XPerson3 .oclIsNew())"
by(simp add: OclValid_def OclIsNew_def σ1_def σ1'_def XPerson3_def person3_def
             oid0_def oid1_def oid2_def oid3_def oid4_def oid5_def oid6_def oid8_def
             oid_of_option_def oid_of_typePerson_def)


Assert "⋀    spost.   (σ1,spost) ⊨      (XPerson4 .boss@pre   ≐ XPerson5)"
Assert "               (σ1,σ1') ⊨ not(υ(XPerson4 .boss@pre .salary))"
Assert "⋀    spost.   (σ1,spost) ⊨      (XPerson4 .boss@pre .salary@pre   ≐ 𝟯𝟱𝟬𝟬)"
lemma "               (σ1,σ1') ⊨      (XPerson4 .oclIsMaintained())"
by(simp add: OclValid_def OclIsMaintained_def σ1_def σ1'_def XPerson4_def person4_def
             oid0_def oid1_def oid2_def oid3_def oid4_def oid5_def oid6_def
             oid_of_option_def oid_of_typePerson_def)

Assert "⋀spre     .   (spre,σ1') ⊨ not(υ(XPerson5 .salary))"
Assert "⋀    spost.   (σ1,spost) ⊨      (XPerson5 .salary@pre   ≐ 𝟯𝟱𝟬𝟬)"
Assert "⋀spre     .   (spre,σ1') ⊨ not(υ(XPerson5 .boss))"
lemma "               (σ1,σ1') ⊨      (XPerson5 .oclIsDeleted())"
by(simp add: OclNot_def OclValid_def OclIsDeleted_def σ1_def σ1'_def XPerson5_def person5_def
             oid0_def oid1_def oid2_def oid3_def oid4_def oid5_def oid6_def oid7_def oid8_def
             oid_of_option_def oid_of_typePerson_def)

(* (* access to an oclany object not yet supported *) Assert "  (σ1,σ1') ⊨     ((XPerson6 .boss .salary)   ≐ 𝟯𝟮𝟬𝟬 )"*)
Assert "⋀spre     .   (spre,σ1') ⊨ not(υ(XPerson6 .boss .salary@pre))"
Assert "⋀    spost.   (σ1,spost) ⊨      (XPerson6 .boss@pre   ≐ XPerson4)"
Assert "               (σ1,σ1') ⊨      (XPerson6 .boss@pre .salary   ≐ 𝟮𝟵𝟬𝟬)"
Assert "⋀    spost.   (σ1,spost) ⊨      (XPerson6 .boss@pre .salary@pre   ≐ 𝟮𝟲𝟬𝟬)"
Assert "⋀    spost.   (σ1,spost) ⊨      (XPerson6 .boss@pre .boss@pre  ≐ XPerson5)"
lemma "               (σ1,σ1') ⊨      (XPerson6 .oclIsMaintained())"
by(simp add: OclValid_def OclIsMaintained_def σ1_def σ1'_def XPerson6_def person6_def
             oid0_def oid1_def oid2_def oid3_def oid4_def oid5_def oid6_def
             oid_of_option_def oid_of_typePerson_def)

(* (* access to an oclany object not yet supported *) Assert "  (σ1,σ1') ⊨     ((XPerson7 .oclAsType(Person)   ≐  (XPerson6 .boss)))" *)
(* (* access to an oclany object not yet supported *) Assert "  (σ1,σ1') ⊨     ((XPerson7 .oclAsType(Person) .boss)   ≐ (XPerson7 .oclAsType(Person)) )" *)
(* (* access to an oclany object not yet supported *) Assert "  (σ1,σ1') ⊨     ((XPerson7 .oclAsType(Person) .boss .salary)   ≐ 𝟯𝟮𝟬𝟬 )" *)
Assert "⋀spre spost.   (spre,spost) ⊨     υ(XPerson7 .oclAsType(Person))"
Assert "⋀    spost.    (σ1,spost) ⊨ not(υ(XPerson7 .oclAsType(Person) .boss@pre))"
lemma "⋀spre spost.   (spre,spost) ⊨     ((XPerson7 .oclAsType(Person) .oclAsType(OclAny)
                                                                   .oclAsType(Person))
                                      ≐ (XPerson7 .oclAsType(Person)))"
by(rule up_down_cast_Person_OclAny_Person', simp add: XPerson7_def OclValid_def valid_def person7_def)
lemma "               (σ1,σ1') ⊨       (XPerson7 .oclIsNew())"
by(simp add: OclValid_def OclIsNew_def  σ1_def σ1'_def  XPerson7_def person7_def
             oid0_def oid1_def oid2_def oid3_def oid4_def oid5_def oid6_def oid8_def
             oid_of_option_def oid_of_typeOclAny_def)

Assert "⋀spre spost.   (spre,spost) ⊨      (XPerson8  <> XPerson7)"
Assert "⋀spre spost.   (spre,spost) ⊨ not(υ(XPerson8 .oclAsType(Person)))"
Assert "⋀spre spost.   (spre,spost) ⊨      (XPerson8 .oclIsTypeOf(OclAny))"
Assert "⋀spre spost.   (spre,spost) ⊨   not(XPerson8 .oclIsTypeOf(Person))"
Assert "⋀spre spost.   (spre,spost) ⊨   not(XPerson8 .oclIsKindOf(Person))"
Assert "⋀spre spost.   (spre,spost) ⊨      (XPerson8 .oclIsKindOf(OclAny))"

lemma σ_modifiedonly: "(σ1,σ1') ⊨ (Set{ XPerson1 .oclAsType(OclAny)
                      , XPerson2 .oclAsType(OclAny)
                      ⌦‹, XPerson3 .oclAsType(OclAny)›
                      , XPerson4 .oclAsType(OclAny)
                      ⌦‹, XPerson5 .oclAsType(OclAny)›
                      , XPerson6 .oclAsType(OclAny)
                      ⌦‹, XPerson7 .oclAsType(OclAny)›
                      ⌦‹, XPerson8 .oclAsType(OclAny)›
                      ⌦‹, XPerson9 .oclAsType(OclAny)›}->oclIsModifiedOnly())"
 apply(simp add: OclIsModifiedOnly_def OclValid_def
                 oid0_def oid1_def oid2_def oid3_def oid4_def oid5_def oid6_def oid7_def oid8_def
                 XPerson1_def XPerson2_def XPerson3_def XPerson4_def
                 XPerson5_def XPerson6_def XPerson7_def XPerson8_def XPerson9_def
                 person1_def person2_def person3_def person4_def
                 person5_def person6_def person7_def person8_def person9_def
                 image_def)
 apply(simp add: OclIncluding_rep_set mtSet_rep_set null_option_def bot_option_def)
 apply(simp add: oid_of_option_def oid_of_typeOclAny_def, clarsimp)
 apply(simp add: σ1_def σ1'_def
                 oid0_def oid1_def oid2_def oid3_def oid4_def oid5_def oid6_def oid7_def oid8_def)
done

lemma "(σ1,σ1') ⊨ ((XPerson9 @pre (λx. ⌊OclAsTypePerson_𝔄 x⌋))  ≜ XPerson9)"
by(simp add: OclSelf_at_pre_def σ1_def oid_of_option_def oid_of_typePerson_def
             XPerson9_def person9_def oid8_def OclValid_def StrongEq_def OclAsTypePerson_𝔄_def)

lemma "(σ1,σ1') ⊨ ((XPerson9 @post (λx. ⌊OclAsTypePerson_𝔄 x⌋))  ≜ XPerson9)"
by(simp add: OclSelf_at_post_def σ1'_def oid_of_option_def oid_of_typePerson_def
             XPerson9_def person9_def oid8_def OclValid_def StrongEq_def OclAsTypePerson_𝔄_def)

lemma "(σ1,σ1') ⊨ (((XPerson9 .oclAsType(OclAny)) @pre (λx. ⌊OclAsTypeOclAny_𝔄 x⌋)) ≜
                   ((XPerson9 .oclAsType(OclAny)) @post (λx. ⌊OclAsTypeOclAny_𝔄 x⌋)))"
proof -

 have including4 : "⋀a b c d τ.
        Set{λτ. ⌊⌊a⌋⌋, λτ. ⌊⌊b⌋⌋, λτ. ⌊⌊c⌋⌋, λτ. ⌊⌊d⌋⌋} τ = Abs_Setbase ⌊⌊ {⌊⌊a⌋⌋, ⌊⌊b⌋⌋, ⌊⌊c⌋⌋, ⌊⌊d⌋⌋} ⌋⌋"
  apply(subst abs_rep_simp'[symmetric], simp)
  apply(simp add: OclIncluding_rep_set mtSet_rep_set)
  by(rule arg_cong[of _ _ "λx. (Abs_Setbase(⌊⌊ x ⌋⌋))"], auto)

 have excluding1: "⋀S a b c d e τ.
                   (λ_. Abs_Setbase ⌊⌊ {⌊⌊a⌋⌋, ⌊⌊b⌋⌋, ⌊⌊c⌋⌋, ⌊⌊d⌋⌋} ⌋⌋)->excludingSet(λτ. ⌊⌊e⌋⌋) τ =
                   Abs_Setbase ⌊⌊ {⌊⌊a⌋⌋, ⌊⌊b⌋⌋, ⌊⌊c⌋⌋, ⌊⌊d⌋⌋} - {⌊⌊e⌋⌋} ⌋⌋"
  apply(simp add: UML_Set.OclExcluding_def)
  apply(simp add: defined_def OclValid_def false_def true_def
                  bot_fun_def bot_Setbase_def null_fun_def null_Setbase_def)
  apply(rule conjI)
   apply(rule impI, subst (asm) Abs_Setbase_inject) apply( simp add: bot_option_def)+
  apply(rule conjI)
   apply(rule impI, subst (asm) Abs_Setbase_inject) apply( simp add: bot_option_def null_option_def)+
  apply(subst Abs_Setbase_inverse, simp add: bot_option_def, simp)
 done

 show ?thesis
  apply(rule framing[where X = "Set{ XPerson1 .oclAsType(OclAny)
                       , XPerson2 .oclAsType(OclAny)
                       ⌦‹, XPerson3 .oclAsType(OclAny)›
                       , XPerson4 .oclAsType(OclAny)
                       ⌦‹, XPerson5 .oclAsType(OclAny)›
                       , XPerson6 .oclAsType(OclAny)
                       ⌦‹, XPerson7 .oclAsType(OclAny)›
                       ⌦‹, XPerson8 .oclAsType(OclAny)›
                       ⌦‹, XPerson9 .oclAsType(OclAny)›}"])
   apply(cut_tac σ_modifiedonly)
   apply(simp only: OclValid_def
                    XPerson1_def XPerson2_def XPerson3_def XPerson4_def
                    XPerson5_def XPerson6_def XPerson7_def XPerson8_def XPerson9_def
                    person1_def person2_def person3_def person4_def
                    person5_def person6_def person7_def person8_def person9_def
                    OclAsTypeOclAny_Person)
   apply(subst cp_OclIsModifiedOnly, subst UML_Set.OclExcluding.cp0,
     subst (asm) cp_OclIsModifiedOnly, simp add: including4 excluding1)

  apply(simp only: XPerson1_def XPerson2_def XPerson3_def XPerson4_def
                   XPerson5_def XPerson6_def XPerson7_def XPerson8_def XPerson9_def
                   person1_def person2_def person3_def person4_def
                   person5_def person6_def person7_def person8_def person9_def)
  apply(simp add: OclIncluding_rep_set mtSet_rep_set
                  oid0_def oid1_def oid2_def oid3_def oid4_def oid5_def oid6_def oid7_def oid8_def)
  apply(simp add: StrictRefEqObject_def oid_of_option_def oid_of_typeOclAny_def OclNot_def OclValid_def
                  null_option_def bot_option_def)
 done
qed

lemma perm_σ1' : "σ1' = ⦇ heap = Map.empty
                           (oid8 ↦ inPerson person9,
                           oid7 ↦ inOclAny person8,
                           oid6 ↦ inOclAny person7,
                           oid5 ↦ inPerson person6,
                           ⌦‹oid4›
                           oid3 ↦ inPerson person4,
                           oid2 ↦ inPerson person3,
                           oid1 ↦ inPerson person2,
                           oid0 ↦ inPerson person1)
                       , assocs = assocs σ1' ⦈"
proof -
 note P = fun_upd_twist
 show ?thesis
  apply(simp add: σ1'_def
                  oid0_def oid1_def oid2_def oid3_def oid4_def oid5_def oid6_def oid7_def oid8_def)
  apply(subst (1) P, simp)
  apply(subst (2) P, simp) apply(subst (1) P, simp)
  apply(subst (3) P, simp) apply(subst (2) P, simp) apply(subst (1) P, simp)
  apply(subst (4) P, simp) apply(subst (3) P, simp) apply(subst (2) P, simp) apply(subst (1) P, simp)
  apply(subst (5) P, simp) apply(subst (4) P, simp) apply(subst (3) P, simp) apply(subst (2) P, simp) apply(subst (1) P, simp)
  apply(subst (6) P, simp) apply(subst (5) P, simp) apply(subst (4) P, simp) apply(subst (3) P, simp) apply(subst (2) P, simp) apply(subst (1) P, simp)
  apply(subst (7) P, simp) apply(subst (6) P, simp) apply(subst (5) P, simp) apply(subst (4) P, simp) apply(subst (3) P, simp) apply(subst (2) P, simp) apply(subst (1) P, simp)
 by(simp)
qed

declare const_ss [simp]

lemma "⋀σ1.
 (σ1,σ1') ⊨ (Person .allInstances() ≐ Set{ XPerson1, XPerson2, XPerson3, XPerson4⌦‹, XPerson5›, XPerson6,
                                           XPerson7 .oclAsType(Person)⌦‹, XPerson8›, XPerson9 })"
 apply(subst perm_σ1')
 apply(simp only: oid0_def oid1_def oid2_def oid3_def oid4_def oid5_def oid6_def oid7_def oid8_def
                  XPerson1_def XPerson2_def XPerson3_def XPerson4_def
                  XPerson5_def XPerson6_def XPerson7_def XPerson8_def XPerson9_def
                  person7_def)
 apply(subst state_update_vs_allInstances_at_post_tc, simp, simp add: OclAsTypePerson_𝔄_def, simp, rule const_StrictRefEqSet_including, simp, simp, simp, rule OclIncluding_cong, simp, simp)
  apply(subst state_update_vs_allInstances_at_post_tc, simp, simp add: OclAsTypePerson_𝔄_def, simp, rule const_StrictRefEqSet_including, simp, simp, simp, rule OclIncluding_cong, simp, simp)
   apply(subst state_update_vs_allInstances_at_post_tc, simp, simp add: OclAsTypePerson_𝔄_def, simp, rule const_StrictRefEqSet_including, simp, simp, simp, rule OclIncluding_cong, simp, simp)
    apply(subst state_update_vs_allInstances_at_post_tc, simp, simp add: OclAsTypePerson_𝔄_def, simp, rule const_StrictRefEqSet_including, simp, simp, simp, rule OclIncluding_cong, simp, simp)
     apply(subst state_update_vs_allInstances_at_post_tc, simp, simp add: OclAsTypePerson_𝔄_def, simp, rule const_StrictRefEqSet_including, simp, simp, simp, rule OclIncluding_cong, simp, simp)
      apply(subst state_update_vs_allInstances_at_post_tc, simp, simp add: OclAsTypePerson_𝔄_def, simp, rule const_StrictRefEqSet_including, simp, simp, simp, rule OclIncluding_cong, simp, simp)
       apply(subst state_update_vs_allInstances_at_post_ntc, simp, simp add: OclAsTypePerson_𝔄_def
                                                                             person8_def, simp, rule const_StrictRefEqSet_including, simp, simp, simp)
       apply(subst state_update_vs_allInstances_at_post_tc, simp, simp add: OclAsTypePerson_𝔄_def, simp, rule const_StrictRefEqSet_including, simp, simp, simp, rule OclIncluding_cong, simp, simp)
        apply(rule state_update_vs_allInstances_at_post_empty)
by(simp_all add: OclAsTypePerson_𝔄_def)

lemma "⋀σ1.
 (σ1,σ1') ⊨ (OclAny .allInstances() ≐ Set{ XPerson1 .oclAsType(OclAny), XPerson2 .oclAsType(OclAny),
                                           XPerson3 .oclAsType(OclAny), XPerson4 .oclAsType(OclAny)
                                           ⌦‹, XPerson5›, XPerson6 .oclAsType(OclAny),
                                           XPerson7, XPerson8, XPerson9 .oclAsType(OclAny) })"
 apply(subst perm_σ1')
 apply(simp only: oid0_def oid1_def oid2_def oid3_def oid4_def oid5_def oid6_def oid7_def oid8_def
                  XPerson1_def XPerson2_def XPerson3_def XPerson4_def XPerson5_def XPerson6_def XPerson7_def XPerson8_def XPerson9_def
                  person1_def person2_def person3_def person4_def person5_def person6_def person9_def)
 apply(subst state_update_vs_allInstances_at_post_tc, simp, simp add: OclAsTypeOclAny_𝔄_def, simp, rule const_StrictRefEqSet_including, simp, simp, simp, rule OclIncluding_cong, simp, simp)+
         apply(rule state_update_vs_allInstances_at_post_empty)
by(simp_all add: OclAsTypeOclAny_𝔄_def)

end