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     .   (<