Theory Analysis_UML
chapter‹Example: The Employee Analysis Model›
theory
Analysis_UML
imports
"../../../UML_Main"
begin
text ‹\label{ex:employee-analysis: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 an ``analysis-model'' of the (slightly
modified) example Figure 7.3, page 20 of
the OCL standard~\<^cite>‹"omg:ocl:2012"›.
Here, analysis model means that associations
were really represented as relation on objects on the state---as is
intended by the standard---rather by pointers between objects as is
done in our ``design model''
\isatagafp
(see \autoref{ex:employee-design:uml}).
\endisatagafp
\isatagannexa
(see \url{http://isa-afp.org/entries/Featherweight_OCL.shtml}).
\endisatagannexa
To be precise, this theory contains the formalization of the data-part
covered by the UML class model (see \autoref{fig:person-ana}):›
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-ana}}
\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 type⇩P⇩e⇩r⇩s⇩o⇩n = mk⇩P⇩e⇩r⇩s⇩o⇩n oid
"int option"
datatype type⇩O⇩c⇩l⇩A⇩n⇩y = mk⇩O⇩c⇩l⇩A⇩n⇩y oid
"(int option) option"
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 𝔄 = in⇩P⇩e⇩r⇩s⇩o⇩n type⇩P⇩e⇩r⇩s⇩o⇩n | in⇩O⇩c⇩l⇩A⇩n⇩y type⇩O⇩c⇩l⇩A⇩n⇩y
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 = "(𝔄, type⇩O⇩c⇩l⇩A⇩n⇩y option option) val"
type_synonym Person = "(𝔄, type⇩P⇩e⇩r⇩s⇩o⇩n option option) val"
type_synonym Set_Integer = "(𝔄, int option option) Set"
type_synonym Set_Person = "(𝔄, type⇩P⇩e⇩r⇩s⇩o⇩n 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 type⇩P⇩e⇩r⇩s⇩o⇩n :: object
begin
definition oid_of_type⇩P⇩e⇩r⇩s⇩o⇩n_def: "oid_of x = (case x of mk⇩P⇩e⇩r⇩s⇩o⇩n oid _ ⇒ oid)"
instance ..
end
instantiation type⇩O⇩c⇩l⇩A⇩n⇩y :: object
begin
definition oid_of_type⇩O⇩c⇩l⇩A⇩n⇩y_def: "oid_of x = (case x of mk⇩O⇩c⇩l⇩A⇩n⇩y oid _ ⇒ oid)"
instance ..
end
instantiation 𝔄 :: object
begin
definition oid_of_𝔄_def: "oid_of x = (case x of
in⇩P⇩e⇩r⇩s⇩o⇩n person ⇒ oid_of person
| in⇩O⇩c⇩l⇩A⇩n⇩y 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 StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t_⇩P⇩e⇩r⇩s⇩o⇩n : "(x::Person) ≐ y ≡ StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t x y"
end
overloading StrictRefEq ≡ "StrictRefEq :: [OclAny,OclAny] ⇒ Boolean"
begin
definition StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t_⇩O⇩c⇩l⇩A⇩n⇩y : "(x::OclAny) ≐ y ≡ StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t x y"
end
lemmas cps23 =
cp_StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t[of "x::Person" "y::Person" "τ",
simplified StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t_⇩P⇩e⇩r⇩s⇩o⇩n[symmetric]]
cp_intro(9) [of "P::Person ⇒Person""Q::Person ⇒Person",
simplified StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t_⇩P⇩e⇩r⇩s⇩o⇩n[symmetric] ]
StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t_def [of "x::Person" "y::Person",
simplified StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t_⇩P⇩e⇩r⇩s⇩o⇩n[symmetric]]
StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t_defargs [of _ "x::Person" "y::Person",
simplified StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t_⇩P⇩e⇩r⇩s⇩o⇩n[symmetric]]
StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t_strict1
[of "x::Person",
simplified StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t_⇩P⇩e⇩r⇩s⇩o⇩n[symmetric]]
StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t_strict2
[of "x::Person",
simplified StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t_⇩P⇩e⇩r⇩s⇩o⇩n[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 OclAsType⇩O⇩c⇩l⇩A⇩n⇩y :: "'α ⇒ OclAny" ("(_) .oclAsType'(OclAny')")
consts OclAsType⇩P⇩e⇩r⇩s⇩o⇩n :: "'α ⇒ Person" ("(_) .oclAsType'(Person')")
definition "OclAsType⇩O⇩c⇩l⇩A⇩n⇩y_𝔄 = (λu. ⌊case u of in⇩O⇩c⇩l⇩A⇩n⇩y a ⇒ a
| in⇩P⇩e⇩r⇩s⇩o⇩n (mk⇩P⇩e⇩r⇩s⇩o⇩n oid a) ⇒ mk⇩O⇩c⇩l⇩A⇩n⇩y oid ⌊a⌋⌋)"
lemma OclAsType⇩O⇩c⇩l⇩A⇩n⇩y_𝔄_some: "OclAsType⇩O⇩c⇩l⇩A⇩n⇩y_𝔄 x ≠ None"
by(simp add: OclAsType⇩O⇩c⇩l⇩A⇩n⇩y_𝔄_def)
overloading OclAsType⇩O⇩c⇩l⇩A⇩n⇩y ≡ "OclAsType⇩O⇩c⇩l⇩A⇩n⇩y :: OclAny ⇒ OclAny"
begin
definition OclAsType⇩O⇩c⇩l⇩A⇩n⇩y_OclAny:
"(X::OclAny) .oclAsType(OclAny) ≡ X"
end
overloading OclAsType⇩O⇩c⇩l⇩A⇩n⇩y ≡ "OclAsType⇩O⇩c⇩l⇩A⇩n⇩y :: Person ⇒ OclAny"
begin
definition OclAsType⇩O⇩c⇩l⇩A⇩n⇩y_Person:
"(X::Person) .oclAsType(OclAny) ≡
(λτ. case X τ of
⊥ ⇒ invalid τ
| ⌊⊥⌋ ⇒ null τ
| ⌊⌊mk⇩P⇩e⇩r⇩s⇩o⇩n oid a ⌋⌋ ⇒ ⌊⌊ (mk⇩O⇩c⇩l⇩A⇩n⇩y oid ⌊a⌋) ⌋⌋)"
end
definition "OclAsType⇩P⇩e⇩r⇩s⇩o⇩n_𝔄 =
(λu. case u of in⇩P⇩e⇩r⇩s⇩o⇩n p ⇒ ⌊p⌋
| in⇩O⇩c⇩l⇩A⇩n⇩y (mk⇩O⇩c⇩l⇩A⇩n⇩y oid ⌊a⌋) ⇒ ⌊mk⇩P⇩e⇩r⇩s⇩o⇩n oid a⌋
| _ ⇒ None)"
overloading OclAsType⇩P⇩e⇩r⇩s⇩o⇩n ≡ "OclAsType⇩P⇩e⇩r⇩s⇩o⇩n :: OclAny ⇒ Person"
begin
definition OclAsType⇩P⇩e⇩r⇩s⇩o⇩n_OclAny:
"(X::OclAny) .oclAsType(Person) ≡
(λτ. case X τ of
⊥ ⇒ invalid τ
| ⌊⊥⌋ ⇒ null τ
| ⌊⌊mk⇩O⇩c⇩l⇩A⇩n⇩y oid ⊥ ⌋⌋ ⇒ invalid τ
| ⌊⌊mk⇩O⇩c⇩l⇩A⇩n⇩y oid ⌊a⌋ ⌋⌋ ⇒ ⌊⌊mk⇩P⇩e⇩r⇩s⇩o⇩n oid a⌋⌋)"
end
overloading OclAsType⇩P⇩e⇩r⇩s⇩o⇩n ≡ "OclAsType⇩P⇩e⇩r⇩s⇩o⇩n :: Person ⇒ Person"
begin
definition OclAsType⇩P⇩e⇩r⇩s⇩o⇩n_Person:
"(X::Person) .oclAsType(Person) ≡ X "
end
text_raw‹\isatagafp›
lemmas [simp] =
OclAsType⇩O⇩c⇩l⇩A⇩n⇩y_OclAny
OclAsType⇩P⇩e⇩r⇩s⇩o⇩n_Person
subsection‹Context Passing›
lemma cp_OclAsType⇩O⇩c⇩l⇩A⇩n⇩y_Person_Person: "cp P ⟹ cp(λX. (P (X::Person)::Person) .oclAsType(OclAny))"
by(rule cpI1, simp_all add: OclAsType⇩O⇩c⇩l⇩A⇩n⇩y_Person)
lemma cp_OclAsType⇩O⇩c⇩l⇩A⇩n⇩y_OclAny_OclAny: "cp P ⟹ cp(λX. (P (X::OclAny)::OclAny) .oclAsType(OclAny))"
by(rule cpI1, simp_all add: OclAsType⇩O⇩c⇩l⇩A⇩n⇩y_OclAny)
lemma cp_OclAsType⇩P⇩e⇩r⇩s⇩o⇩n_Person_Person: "cp P ⟹ cp(λX. (P (X::Person)::Person) .oclAsType(Person))"
by(rule cpI1, simp_all add: OclAsType⇩P⇩e⇩r⇩s⇩o⇩n_Person)
lemma cp_OclAsType⇩P⇩e⇩r⇩s⇩o⇩n_OclAny_OclAny: "cp P ⟹ cp(λX. (P (X::OclAny)::OclAny) .oclAsType(Person))"
by(rule cpI1, simp_all add: OclAsType⇩P⇩e⇩r⇩s⇩o⇩n_OclAny)
lemma cp_OclAsType⇩O⇩c⇩l⇩A⇩n⇩y_Person_OclAny: "cp P ⟹ cp(λX. (P (X::Person)::OclAny) .oclAsType(OclAny))"
by(rule cpI1, simp_all add: OclAsType⇩O⇩c⇩l⇩A⇩n⇩y_OclAny)
lemma cp_OclAsType⇩O⇩c⇩l⇩A⇩n⇩y_OclAny_Person: "cp P ⟹ cp(λX. (P (X::OclAny)::Person) .oclAsType(OclAny))"
by(rule cpI1, simp_all add: OclAsType⇩O⇩c⇩l⇩A⇩n⇩y_Person)
lemma cp_OclAsType⇩P⇩e⇩r⇩s⇩o⇩n_Person_OclAny: "cp P ⟹ cp(λX. (P (X::Person)::OclAny) .oclAsType(Person))"
by(rule cpI1, simp_all add: OclAsType⇩P⇩e⇩r⇩s⇩o⇩n_OclAny)
lemma cp_OclAsType⇩P⇩e⇩r⇩s⇩o⇩n_OclAny_Person: "cp P ⟹ cp(λX. (P (X::OclAny)::Person) .oclAsType(Person))"
by(rule cpI1, simp_all add: OclAsType⇩P⇩e⇩r⇩s⇩o⇩n_Person)
lemmas [simp] =
cp_OclAsType⇩O⇩c⇩l⇩A⇩n⇩y_Person_Person
cp_OclAsType⇩O⇩c⇩l⇩A⇩n⇩y_OclAny_OclAny
cp_OclAsType⇩P⇩e⇩r⇩s⇩o⇩n_Person_Person
cp_OclAsType⇩P⇩e⇩r⇩s⇩o⇩n_OclAny_OclAny
cp_OclAsType⇩O⇩c⇩l⇩A⇩n⇩y_Person_OclAny
cp_OclAsType⇩O⇩c⇩l⇩A⇩n⇩y_OclAny_Person
cp_OclAsType⇩P⇩e⇩r⇩s⇩o⇩n_Person_OclAny
cp_OclAsType⇩P⇩e⇩r⇩s⇩o⇩n_OclAny_Person
text_raw‹\endisatagafp›
subsection‹Execution with Invalid or Null as Argument›
lemma OclAsType⇩O⇩c⇩l⇩A⇩n⇩y_OclAny_strict : "(invalid::OclAny) .oclAsType(OclAny) = invalid" by(simp)
lemma OclAsType⇩O⇩c⇩l⇩A⇩n⇩y_OclAny_nullstrict : "(null::OclAny) .oclAsType(OclAny) = null" by(simp)
lemma OclAsType⇩O⇩c⇩l⇩A⇩n⇩y_Person_strict[simp] : "(invalid::Person) .oclAsType(OclAny) = invalid"
by(rule ext, simp add: bot_option_def invalid_def OclAsType⇩O⇩c⇩l⇩A⇩n⇩y_Person)
lemma OclAsType⇩O⇩c⇩l⇩A⇩n⇩y_Person_nullstrict[simp] : "(null::Person) .oclAsType(OclAny) = null"
by(rule ext, simp add: null_fun_def null_option_def bot_option_def OclAsType⇩O⇩c⇩l⇩A⇩n⇩y_Person)
lemma OclAsType⇩P⇩e⇩r⇩s⇩o⇩n_OclAny_strict[simp] : "(invalid::OclAny) .oclAsType(Person) = invalid"
by(rule ext, simp add: bot_option_def invalid_def OclAsType⇩P⇩e⇩r⇩s⇩o⇩n_OclAny)
lemma OclAsType⇩P⇩e⇩r⇩s⇩o⇩n_OclAny_nullstrict[simp] : "(null::OclAny) .oclAsType(Person) = null"
by(rule ext, simp add: null_fun_def null_option_def bot_option_def OclAsType⇩P⇩e⇩r⇩s⇩o⇩n_OclAny)
lemma OclAsType⇩P⇩e⇩r⇩s⇩o⇩n_Person_strict : "(invalid::Person) .oclAsType(Person) = invalid" by(simp)
lemma OclAsType⇩P⇩e⇩r⇩s⇩o⇩n_Person_nullstrict : "(null::Person) .oclAsType(Person) = null" by(simp)
section‹OclIsTypeOf›
subsection‹Definition›
consts OclIsTypeOf⇩O⇩c⇩l⇩A⇩n⇩y :: "'α ⇒ Boolean" ("(_).oclIsTypeOf'(OclAny')")
consts OclIsTypeOf⇩P⇩e⇩r⇩s⇩o⇩n :: "'α ⇒ Boolean" ("(_).oclIsTypeOf'(Person')")
overloading OclIsTypeOf⇩O⇩c⇩l⇩A⇩n⇩y ≡ "OclIsTypeOf⇩O⇩c⇩l⇩A⇩n⇩y :: OclAny ⇒ Boolean"
begin
definition OclIsTypeOf⇩O⇩c⇩l⇩A⇩n⇩y_OclAny:
"(X::OclAny) .oclIsTypeOf(OclAny) ≡
(λτ. case X τ of
⊥ ⇒ invalid τ
| ⌊⊥⌋ ⇒ true τ
| ⌊⌊mk⇩O⇩c⇩l⇩A⇩n⇩y oid ⊥ ⌋⌋ ⇒ true τ
| ⌊⌊mk⇩O⇩c⇩l⇩A⇩n⇩y oid ⌊_⌋ ⌋⌋ ⇒ false τ)"
end
lemma OclIsTypeOf⇩O⇩c⇩l⇩A⇩n⇩y_OclAny':
"(X::OclAny) .oclIsTypeOf(OclAny) =
(λ τ. if τ ⊨ υ X then (case X τ of
⌊⊥⌋ ⇒ true τ
| ⌊⌊mk⇩O⇩c⇩l⇩A⇩n⇩y oid ⊥ ⌋⌋ ⇒ true τ
| ⌊⌊mk⇩O⇩c⇩l⇩A⇩n⇩y oid ⌊_⌋ ⌋⌋ ⇒ false τ)
else invalid τ)"
apply(rule ext, simp add: OclIsTypeOf⇩O⇩c⇩l⇩A⇩n⇩y_OclAny)
by(case_tac "τ ⊨ υ X", auto simp: foundation18' bot_option_def)
interpretation OclIsTypeOf⇩O⇩c⇩l⇩A⇩n⇩y_OclAny :
profile_mono_schemeV
"OclIsTypeOf⇩O⇩c⇩l⇩A⇩n⇩y::OclAny ⇒ Boolean"
"λ X. (case X of
⌊None⌋ ⇒ ⌊⌊True⌋⌋
| ⌊⌊mk⇩O⇩c⇩l⇩A⇩n⇩y oid None ⌋⌋ ⇒ ⌊⌊True⌋⌋
| ⌊⌊mk⇩O⇩c⇩l⇩A⇩n⇩y oid ⌊_⌋ ⌋⌋ ⇒ ⌊⌊False⌋⌋)"
apply(unfold_locales, simp add: atomize_eq, rule ext)
by(auto simp: OclIsTypeOf⇩O⇩c⇩l⇩A⇩n⇩y_OclAny' OclValid_def true_def false_def
split: option.split type⇩O⇩c⇩l⇩A⇩n⇩y.split)
overloading OclIsTypeOf⇩O⇩c⇩l⇩A⇩n⇩y ≡ "OclIsTypeOf⇩O⇩c⇩l⇩A⇩n⇩y :: Person ⇒ Boolean"
begin
definition OclIsTypeOf⇩O⇩c⇩l⇩A⇩n⇩y_Person:
"(X::Person) .oclIsTypeOf(OclAny) ≡
(λτ. case X τ of
⊥ ⇒ invalid τ
| ⌊⊥⌋ ⇒ true τ
| ⌊⌊ _ ⌋⌋ ⇒ false τ) "
end
overloading OclIsTypeOf⇩P⇩e⇩r⇩s⇩o⇩n ≡ "OclIsTypeOf⇩P⇩e⇩r⇩s⇩o⇩n :: OclAny ⇒ Boolean"
begin
definition OclIsTypeOf⇩P⇩e⇩r⇩s⇩o⇩n_OclAny:
"(X::OclAny) .oclIsTypeOf(Person) ≡
(λτ. case X τ of
⊥ ⇒ invalid τ
| ⌊⊥⌋ ⇒ true τ
| ⌊⌊mk⇩O⇩c⇩l⇩A⇩n⇩y oid ⊥ ⌋⌋ ⇒ false τ
| ⌊⌊mk⇩O⇩c⇩l⇩A⇩n⇩y oid ⌊_⌋ ⌋⌋ ⇒ true τ)"
end
overloading OclIsTypeOf⇩P⇩e⇩r⇩s⇩o⇩n ≡ "OclIsTypeOf⇩P⇩e⇩r⇩s⇩o⇩n :: Person ⇒ Boolean"
begin
definition OclIsTypeOf⇩P⇩e⇩r⇩s⇩o⇩n_Person:
"(X::Person) .oclIsTypeOf(Person) ≡
(λτ. case X τ of
⊥ ⇒ invalid τ
| _ ⇒ true τ)"
end
text_raw‹\isatagafp›
subsection‹Context Passing›
lemma cp_OclIsTypeOf⇩O⇩c⇩l⇩A⇩n⇩y_Person_Person: "cp P ⟹ cp(λX.(P(X::Person)::Person).oclIsTypeOf(OclAny))"
by(rule cpI1, simp_all add: OclIsTypeOf⇩O⇩c⇩l⇩A⇩n⇩y_Person)
lemma cp_OclIsTypeOf⇩O⇩c⇩l⇩A⇩n⇩y_OclAny_OclAny: "cp P ⟹ cp(λX.(P(X::OclAny)::OclAny).oclIsTypeOf(OclAny))"
by(rule cpI1, simp_all add: OclIsTypeOf⇩O⇩c⇩l⇩A⇩n⇩y_OclAny)
lemma cp_OclIsTypeOf⇩P⇩e⇩r⇩s⇩o⇩n_Person_Person: "cp P ⟹ cp(λX.(P(X::Person)::Person).oclIsTypeOf(Person))"
by(rule cpI1, simp_all add: OclIsTypeOf⇩P⇩e⇩r⇩s⇩o⇩n_Person)
lemma cp_OclIsTypeOf⇩P⇩e⇩r⇩s⇩o⇩n_OclAny_OclAny: "cp P ⟹ cp(λX.(P(X::OclAny)::OclAny).oclIsTypeOf(Person))"
by(rule cpI1, simp_all add: OclIsTypeOf⇩P⇩e⇩r⇩s⇩o⇩n_OclAny)
lemma cp_OclIsTypeOf⇩O⇩c⇩l⇩A⇩n⇩y_Person_OclAny: "cp P ⟹ cp(λX.(P(X::Person)::OclAny).oclIsTypeOf(OclAny))"
by(rule cpI1, simp_all add: OclIsTypeOf⇩O⇩c⇩l⇩A⇩n⇩y_OclAny)
lemma cp_OclIsTypeOf⇩O⇩c⇩l⇩A⇩n⇩y_OclAny_Person: "cp P ⟹ cp(λX.(P(X::OclAny)::Person).oclIsTypeOf(OclAny))"
by(rule cpI1, simp_all add: OclIsTypeOf⇩O⇩c⇩l⇩A⇩n⇩y_Person)
lemma cp_OclIsTypeOf⇩P⇩e⇩r⇩s⇩o⇩n_Person_OclAny: "cp P ⟹ cp(λX.(P(X::Person)::OclAny).oclIsTypeOf(Person))"
by(rule cpI1, simp_all add: OclIsTypeOf⇩P⇩e⇩r⇩s⇩o⇩n_OclAny)
lemma cp_OclIsTypeOf⇩P⇩e⇩r⇩s⇩o⇩n_OclAny_Person: "cp P ⟹ cp(λX.(P(X::OclAny)::Person).oclIsTypeOf(Person))"
by(rule cpI1, simp_all add: OclIsTypeOf⇩P⇩e⇩r⇩s⇩o⇩n_Person)
lemmas [simp] =
cp_OclIsTypeOf⇩O⇩c⇩l⇩A⇩n⇩y_Person_Person
cp_OclIsTypeOf⇩O⇩c⇩l⇩A⇩n⇩y_OclAny_OclAny
cp_OclIsTypeOf⇩P⇩e⇩r⇩s⇩o⇩n_Person_Person
cp_OclIsTypeOf⇩P⇩e⇩r⇩s⇩o⇩n_OclAny_OclAny
cp_OclIsTypeOf⇩O⇩c⇩l⇩A⇩n⇩y_Person_OclAny
cp_OclIsTypeOf⇩O⇩c⇩l⇩A⇩n⇩y_OclAny_Person
cp_OclIsTypeOf⇩P⇩e⇩r⇩s⇩o⇩n_Person_OclAny
cp_OclIsTypeOf⇩P⇩e⇩r⇩s⇩o⇩n_OclAny_Person
text_raw‹\endisatagafp›
subsection‹Execution with Invalid or Null as Argument›
lemma OclIsTypeOf⇩O⇩c⇩l⇩A⇩n⇩y_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
OclIsTypeOf⇩O⇩c⇩l⇩A⇩n⇩y_OclAny)
lemma OclIsTypeOf⇩O⇩c⇩l⇩A⇩n⇩y_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
OclIsTypeOf⇩O⇩c⇩l⇩A⇩n⇩y_OclAny)
lemma OclIsTypeOf⇩O⇩c⇩l⇩A⇩n⇩y_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
OclIsTypeOf⇩O⇩c⇩l⇩A⇩n⇩y_Person)
lemma OclIsTypeOf⇩O⇩c⇩l⇩A⇩n⇩y_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
OclIsTypeOf⇩O⇩c⇩l⇩A⇩n⇩y_Person)
lemma OclIsTypeOf⇩P⇩e⇩r⇩s⇩o⇩n_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
OclIsTypeOf⇩P⇩e⇩r⇩s⇩o⇩n_OclAny)
lemma OclIsTypeOf⇩P⇩e⇩r⇩s⇩o⇩n_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
OclIsTypeOf⇩P⇩e⇩r⇩s⇩o⇩n_OclAny)
lemma OclIsTypeOf⇩P⇩e⇩r⇩s⇩o⇩n_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
OclIsTypeOf⇩P⇩e⇩r⇩s⇩o⇩n_Person)
lemma OclIsTypeOf⇩P⇩e⇩r⇩s⇩o⇩n_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
OclIsTypeOf⇩P⇩e⇩r⇩s⇩o⇩n_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
OclIsTypeOf⇩O⇩c⇩l⇩A⇩n⇩y_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
OclAsType⇩O⇩c⇩l⇩A⇩n⇩y_Person OclAsType⇩P⇩e⇩r⇩s⇩o⇩n_OclAny foundation22 foundation16
split: option.split type⇩O⇩c⇩l⇩A⇩n⇩y.split type⇩P⇩e⇩r⇩s⇩o⇩n.split)
by(simp add: OclIsTypeOf⇩O⇩c⇩l⇩A⇩n⇩y_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
OclAsType⇩O⇩c⇩l⇩A⇩n⇩y_Person OclAsType⇩P⇩e⇩r⇩s⇩o⇩n_OclAny foundation22 foundation16
split: option.split type⇩P⇩e⇩r⇩s⇩o⇩n.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 StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t_⇩P⇩e⇩r⇩s⇩o⇩n)
by(rule StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t_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: StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t_⇩P⇩e⇩r⇩s⇩o⇩n StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t_sym[OF assms, simplified OclValid_def])
apply(subst cp_OclImplies[symmetric])
by simp
section‹OclIsKindOf›
subsection‹Definition›
consts OclIsKindOf⇩O⇩c⇩l⇩A⇩n⇩y :: "'α ⇒ Boolean" ("(_).oclIsKindOf'(OclAny')")
consts OclIsKindOf⇩P⇩e⇩r⇩s⇩o⇩n :: "'α ⇒ Boolean" ("(_).oclIsKindOf'(Person')")
overloading OclIsKindOf⇩O⇩c⇩l⇩A⇩n⇩y ≡ "OclIsKindOf⇩O⇩c⇩l⇩A⇩n⇩y :: OclAny ⇒ Boolean"
begin
definition OclIsKindOf⇩O⇩c⇩l⇩A⇩n⇩y_OclAny:
"(X::OclAny) .oclIsKindOf(OclAny) ≡
(λτ. case X τ of
⊥ ⇒ invalid τ
| _ ⇒ true τ)"
end
overloading OclIsKindOf⇩O⇩c⇩l⇩A⇩n⇩y ≡ "OclIsKindOf⇩O⇩c⇩l⇩A⇩n⇩y :: Person ⇒ Boolean"
begin
definition OclIsKindOf⇩O⇩c⇩l⇩A⇩n⇩y_Person:
"(X::Person) .oclIsKindOf(OclAny) ≡
(λτ. case X τ of
⊥ ⇒ invalid τ
| _⇒ true τ)"
end
overloading OclIsKindOf⇩P⇩e⇩r⇩s⇩o⇩n ≡ "OclIsKindOf⇩P⇩e⇩r⇩s⇩o⇩n :: OclAny ⇒ Boolean"
begin
definition OclIsKindOf⇩P⇩e⇩r⇩s⇩o⇩n_OclAny:
"(X::OclAny) .oclIsKindOf(Person) ≡
(λτ. case X τ of
⊥ ⇒ invalid τ
| ⌊⊥⌋ ⇒ true τ
| ⌊⌊mk⇩O⇩c⇩l⇩A⇩n⇩y oid ⊥ ⌋⌋ ⇒ false τ
| ⌊⌊mk⇩O⇩c⇩l⇩A⇩n⇩y oid ⌊_⌋ ⌋⌋ ⇒ true τ)"
end
overloading OclIsKindOf⇩P⇩e⇩r⇩s⇩o⇩n ≡ "OclIsKindOf⇩P⇩e⇩r⇩s⇩o⇩n :: Person ⇒ Boolean"
begin
definition OclIsKindOf⇩P⇩e⇩r⇩s⇩o⇩n_Person:
"(X::Person) .oclIsKindOf(Person) ≡
(λτ. case X τ of
⊥ ⇒ invalid τ
| _ ⇒ true τ)"
end
text_raw‹\isatagafp›
subsection‹Context Passing›
lemma cp_OclIsKindOf⇩O⇩c⇩l⇩A⇩n⇩y_Person_Person: "cp P ⟹ cp(λX.(P(X::Person)::Person).oclIsKindOf(OclAny))"
by(rule cpI1, simp_all add: OclIsKindOf⇩O⇩c⇩l⇩A⇩n⇩y_Person)
lemma cp_OclIsKindOf⇩O⇩c⇩l⇩A⇩n⇩y_OclAny_OclAny: "cp P ⟹ cp(λX.(P(X::OclAny)::OclAny).oclIsKindOf(OclAny))"
by(rule cpI1, simp_all add: OclIsKindOf⇩O⇩c⇩l⇩A⇩n⇩y_OclAny)
lemma cp_OclIsKindOf⇩P⇩e⇩r⇩s⇩o⇩n_Person_Person: "cp P ⟹ cp(λX.(P(X::Person)::Person).oclIsKindOf(Person))"
by(rule cpI1, simp_all add: OclIsKindOf⇩P⇩e⇩r⇩s⇩o⇩n_Person)
lemma cp_OclIsKindOf⇩P⇩e⇩r⇩s⇩o⇩n_OclAny_OclAny: "cp P ⟹ cp(λX.(P(X::OclAny)::OclAny).oclIsKindOf(Person))"
by(rule cpI1, simp_all add: OclIsKindOf⇩P⇩e⇩r⇩s⇩o⇩n_OclAny)
lemma cp_OclIsKindOf⇩O⇩c⇩l⇩A⇩n⇩y_Person_OclAny: "cp P ⟹ cp(λX.(P(X::Person)::OclAny).oclIsKindOf(OclAny))"
by(rule cpI1, simp_all add: OclIsKindOf⇩O⇩c⇩l⇩A⇩n⇩y_OclAny)
lemma cp_OclIsKindOf⇩O⇩c⇩l⇩A⇩n⇩y_OclAny_Person: "cp P ⟹ cp(λX.(P(X::OclAny)::Person).oclIsKindOf(OclAny))"
by(rule cpI1, simp_all add: OclIsKindOf⇩O⇩c⇩l⇩A⇩n⇩y_Person)
lemma cp_OclIsKindOf⇩P⇩e⇩r⇩s⇩o⇩n_Person_OclAny: "cp P ⟹ cp(λX.(P(X::Person)::OclAny).oclIsKindOf(Person))"
by(rule cpI1, simp_all add: OclIsKindOf⇩P⇩e⇩r⇩s⇩o⇩n_OclAny)
lemma cp_OclIsKindOf⇩P⇩e⇩r⇩s⇩o⇩n_OclAny_Person: "cp P ⟹ cp(λX.(P(X::OclAny)::Person).oclIsKindOf(Person))"
by(rule cpI1, simp_all add: OclIsKindOf⇩P⇩e⇩r⇩s⇩o⇩n_Person)
lemmas [simp] =
cp_OclIsKindOf⇩O⇩c⇩l⇩A⇩n⇩y_Person_Person
cp_OclIsKindOf⇩O⇩c⇩l⇩A⇩n⇩y_OclAny_OclAny
cp_OclIsKindOf⇩P⇩e⇩r⇩s⇩o⇩n_Person_Person
cp_OclIsKindOf⇩P⇩e⇩r⇩s⇩o⇩n_OclAny_OclAny
cp_OclIsKindOf⇩O⇩c⇩l⇩A⇩n⇩y_Person_OclAny
cp_OclIsKindOf⇩O⇩c⇩l⇩A⇩n⇩y_OclAny_Person
cp_OclIsKindOf⇩P⇩e⇩r⇩s⇩o⇩n_Person_OclAny
cp_OclIsKindOf⇩P⇩e⇩r⇩s⇩o⇩n_OclAny_Person
text_raw‹\endisatagafp›
subsection‹Execution with Invalid or Null as Argument›
lemma OclIsKindOf⇩O⇩c⇩l⇩A⇩n⇩y_OclAny_strict1[simp] : "(invalid::OclAny) .oclIsKindOf(OclAny) = invalid"
by(rule ext, simp add: invalid_def bot_option_def
OclIsKindOf⇩O⇩c⇩l⇩A⇩n⇩y_OclAny)
lemma OclIsKindOf⇩O⇩c⇩l⇩A⇩n⇩y_OclAny_strict2[simp] : "(null::OclAny) .oclIsKindOf(OclAny) = true"
by(rule ext, simp add: null_fun_def null_option_def
OclIsKindOf⇩O⇩c⇩l⇩A⇩n⇩y_OclAny)
lemma OclIsKindOf⇩O⇩c⇩l⇩A⇩n⇩y_Person_strict1[simp] : "(invalid::Person) .oclIsKindOf(OclAny) = invalid"
by(rule ext, simp add: bot_option_def invalid_def
OclIsKindOf⇩O⇩c⇩l⇩A⇩n⇩y_Person)
lemma OclIsKindOf⇩O⇩c⇩l⇩A⇩n⇩y_Person_strict2[simp] : "(null::Person) .oclIsKindOf(OclAny) = true"
by(rule ext, simp add: null_fun_def null_option_def bot_option_def
OclIsKindOf⇩O⇩c⇩l⇩A⇩n⇩y_Person)
lemma OclIsKindOf⇩P⇩e⇩r⇩s⇩o⇩n_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
OclIsKindOf⇩P⇩e⇩r⇩s⇩o⇩n_OclAny)
lemma OclIsKindOf⇩P⇩e⇩r⇩s⇩o⇩n_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
OclIsKindOf⇩P⇩e⇩r⇩s⇩o⇩n_OclAny)
lemma OclIsKindOf⇩P⇩e⇩r⇩s⇩o⇩n_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
OclIsKindOf⇩P⇩e⇩r⇩s⇩o⇩n_Person)
lemma OclIsKindOf⇩P⇩e⇩r⇩s⇩o⇩n_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
OclIsKindOf⇩P⇩e⇩r⇩s⇩o⇩n_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
OclIsKindOf⇩O⇩c⇩l⇩A⇩n⇩y_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
OclAsType⇩O⇩c⇩l⇩A⇩n⇩y_Person OclAsType⇩P⇩e⇩r⇩s⇩o⇩n_OclAny foundation22 foundation16
split: option.split type⇩O⇩c⇩l⇩A⇩n⇩y.split type⇩P⇩e⇩r⇩s⇩o⇩n.split)
by(simp add: OclIsKindOf⇩P⇩e⇩r⇩s⇩o⇩n_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 ≡ OclAsType⇩P⇩e⇩r⇩s⇩o⇩n_𝔄"
definition "OclAny ≡ OclAsType⇩O⇩c⇩l⇩A⇩n⇩y_𝔄"
lemmas [simp] = Person_def OclAny_def
lemma OclAllInstances_generic⇩O⇩c⇩l⇩A⇩n⇩y_exec: "OclAllInstances_generic pre_post OclAny =
(λτ. Abs_Set⇩b⇩a⇩s⇩e ⌊⌊ 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: OclAsType⇩O⇩c⇩l⇩A⇩n⇩y_𝔄_some)
show ?thesis by(insert equalityI[OF B C], simp)
qed
lemma OclAllInstances_at_post⇩O⇩c⇩l⇩A⇩n⇩y_exec: "OclAny .allInstances() =
(λτ. Abs_Set⇩b⇩a⇩s⇩e ⌊⌊ Some ` OclAny ` ran (heap (snd τ)) ⌋⌋)"
unfolding OclAllInstances_at_post_def
by(rule OclAllInstances_generic⇩O⇩c⇩l⇩A⇩n⇩y_exec)
lemma OclAllInstances_at_pre⇩O⇩c⇩l⇩A⇩n⇩y_exec: "OclAny .allInstances@pre() =
(λτ. Abs_Set⇩b⇩a⇩s⇩e ⌊⌊ Some ` OclAny ` ran (heap (fst τ)) ⌋⌋) "
unfolding OclAllInstances_at_pre_def
by(rule OclAllInstances_generic⇩O⇩c⇩l⇩A⇩n⇩y_exec)
subsection‹OclIsTypeOf›
lemma OclAny_allInstances_generic_oclIsTypeOf⇩O⇩c⇩l⇩A⇩n⇩y1:
assumes [simp]: "⋀x. pre_post (x, x) = x"
shows "∃τ. (τ ⊨ ((OclAllInstances_generic pre_post OclAny)->forAll⇩S⇩e⇩t(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_Set⇩b⇩a⇩s⇩e_inverse, simp add: bot_option_def)
by(simp add: OclIsTypeOf⇩O⇩c⇩l⇩A⇩n⇩y_OclAny)
lemma OclAny_allInstances_at_post_oclIsTypeOf⇩O⇩c⇩l⇩A⇩n⇩y1:
"∃τ. (τ ⊨ (OclAny .allInstances()->forAll⇩S⇩e⇩t(X|X .oclIsTypeOf(OclAny))))"
unfolding OclAllInstances_at_post_def
by(rule OclAny_allInstances_generic_oclIsTypeOf⇩O⇩c⇩l⇩A⇩n⇩y1, simp)
lemma OclAny_allInstances_at_pre_oclIsTypeOf⇩O⇩c⇩l⇩A⇩n⇩y1:
"∃τ. (τ ⊨ (OclAny .allInstances@pre()->forAll⇩S⇩e⇩t(X|X .oclIsTypeOf(OclAny))))"
unfolding OclAllInstances_at_pre_def
by(rule OclAny_allInstances_generic_oclIsTypeOf⇩O⇩c⇩l⇩A⇩n⇩y1, simp)
lemma OclAny_allInstances_generic_oclIsTypeOf⇩O⇩c⇩l⇩A⇩n⇩y2:
assumes [simp]: "⋀x. pre_post (x, x) = x"
shows "∃τ. (τ ⊨ not ((OclAllInstances_generic pre_post OclAny)->forAll⇩S⇩e⇩t(X|X .oclIsTypeOf(OclAny))))"
proof - fix oid a let ?t0 = "⦇heap = Map.empty(oid ↦ in⇩O⇩c⇩l⇩A⇩n⇩y (mk⇩O⇩c⇩l⇩A⇩n⇩y 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 OclAsType⇩O⇩c⇩l⇩A⇩n⇩y_𝔄_def)
apply(subst (1 2 3) Abs_Set⇩b⇩a⇩s⇩e_inverse, simp add: bot_option_def)
by(simp add: OclIsTypeOf⇩O⇩c⇩l⇩A⇩n⇩y_OclAny OclNot_def OclAny_def)
qed
lemma OclAny_allInstances_at_post_oclIsTypeOf⇩O⇩c⇩l⇩A⇩n⇩y2:
"∃τ. (τ ⊨ not (OclAny .allInstances()->forAll⇩S⇩e⇩t(X|X .oclIsTypeOf(OclAny))))"
unfolding OclAllInstances_at_post_def
by(rule OclAny_allInstances_generic_oclIsTypeOf⇩O⇩c⇩l⇩A⇩n⇩y2, simp)
lemma OclAny_allInstances_at_pre_oclIsTypeOf⇩O⇩c⇩l⇩A⇩n⇩y2:
"∃τ. (τ ⊨ not (OclAny .allInstances@pre()->forAll⇩S⇩e⇩t(X|X .oclIsTypeOf(OclAny))))"
unfolding OclAllInstances_at_pre_def
by(rule OclAny_allInstances_generic_oclIsTypeOf⇩O⇩c⇩l⇩A⇩n⇩y2, simp)
lemma Person_allInstances_generic_oclIsTypeOf⇩P⇩e⇩r⇩s⇩o⇩n:
"τ ⊨ ((OclAllInstances_generic pre_post Person)->forAll⇩S⇩e⇩t(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_Set⇩b⇩a⇩s⇩e_inverse, simp add: bot_option_def)
by(simp add: OclIsTypeOf⇩P⇩e⇩r⇩s⇩o⇩n_Person)
lemma Person_allInstances_at_post_oclIsTypeOf⇩P⇩e⇩r⇩s⇩o⇩n:
"τ ⊨ (Person .allInstances()->forAll⇩S⇩e⇩t(X|X .oclIsTypeOf(Person)))"
unfolding OclAllInstances_at_post_def
by(rule Person_allInstances_generic_oclIsTypeOf⇩P⇩e⇩r⇩s⇩o⇩n)
lemma Person_allInstances_at_pre_oclIsTypeOf⇩P⇩e⇩r⇩s⇩o⇩n:
"τ ⊨ (Person .allInstances@pre()->forAll⇩S⇩e⇩t(X|X .oclIsTypeOf(Person)))"
unfolding OclAllInstances_at_pre_def
by(rule Person_allInstances_generic_oclIsTypeOf⇩P⇩e⇩r⇩s⇩o⇩n)
subsection‹OclIsKindOf›
lemma OclAny_allInstances_generic_oclIsKindOf⇩O⇩c⇩l⇩A⇩n⇩y:
"τ ⊨ ((OclAllInstances_generic pre_post OclAny)->forAll⇩S⇩e⇩t(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_Set⇩b⇩a⇩s⇩e_inverse, simp add: bot_option_def)
by(simp add: OclIsKindOf⇩O⇩c⇩l⇩A⇩n⇩y_OclAny)
lemma OclAny_allInstances_at_post_oclIsKindOf⇩O⇩c⇩l⇩A⇩n⇩y:
"τ ⊨ (OclAny .allInstances()->forAll⇩S⇩e⇩t(X|X .oclIsKindOf(OclAny)))"
unfolding OclAllInstances_at_post_def
by(rule OclAny_allInstances_generic_oclIsKindOf⇩O⇩c⇩l⇩A⇩n⇩y)
lemma OclAny_allInstances_at_pre_oclIsKindOf⇩O⇩c⇩l⇩A⇩n⇩y:
"τ ⊨ (OclAny .allInstances@pre()->forAll⇩S⇩e⇩t(X|X .oclIsKindOf(OclAny)))"
unfolding OclAllInstances_at_pre_def
by(rule OclAny_allInstances_generic_oclIsKindOf⇩O⇩c⇩l⇩A⇩n⇩y)
lemma Person_allInstances_generic_oclIsKindOf⇩O⇩c⇩l⇩A⇩n⇩y:
"τ ⊨ ((OclAllInstances_generic pre_post Person)->forAll⇩S⇩e⇩t(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_Set⇩b⇩a⇩s⇩e_inverse, simp add: bot_option_def)
by(simp add: OclIsKindOf⇩O⇩c⇩l⇩A⇩n⇩y_Person)
lemma Person_allInstances_at_post_oclIsKindOf⇩O⇩c⇩l⇩A⇩n⇩y:
"τ ⊨ (Person .allInstances()->forAll⇩S⇩e⇩t(X|X .oclIsKindOf(OclAny)))"
unfolding OclAllInstances_at_post_def
by(rule Person_allInstances_generic_oclIsKindOf⇩O⇩c⇩l⇩A⇩n⇩y)
lemma Person_allInstances_at_pre_oclIsKindOf⇩O⇩c⇩l⇩A⇩n⇩y:
"τ ⊨ (Person .allInstances@pre()->forAll⇩S⇩e⇩t(X|X .oclIsKindOf(OclAny)))"
unfolding OclAllInstances_at_pre_def
by(rule Person_allInstances_generic_oclIsKindOf⇩O⇩c⇩l⇩A⇩n⇩y)
lemma Person_allInstances_generic_oclIsKindOf⇩P⇩e⇩r⇩s⇩o⇩n:
"τ ⊨ ((OclAllInstances_generic pre_post Person)->forAll⇩S⇩e⇩t(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_Set⇩b⇩a⇩s⇩e_inverse, simp add: bot_option_def)
by(simp add: OclIsKindOf⇩P⇩e⇩r⇩s⇩o⇩n_Person)
lemma Person_allInstances_at_post_oclIsKindOf⇩P⇩e⇩r⇩s⇩o⇩n:
"τ ⊨ (Person .allInstances()->forAll⇩S⇩e⇩t(X|X .oclIsKindOf(Person)))"
unfolding OclAllInstances_at_post_def
by(rule Person_allInstances_generic_oclIsKindOf⇩P⇩e⇩r⇩s⇩o⇩n)
lemma Person_allInstances_at_pre_oclIsKindOf⇩P⇩e⇩r⇩s⇩o⇩n:
"τ ⊨ (Person .allInstances@pre()->forAll⇩S⇩e⇩t(X|X .oclIsKindOf(Person)))"
unfolding OclAllInstances_at_pre_def
by(rule Person_allInstances_generic_oclIsKindOf⇩P⇩e⇩r⇩s⇩o⇩n)
section‹The Accessors (any, boss, salary)›
text‹\label{sec:eam-accessors}›
text‹Should be generated entirely from a class-diagram.›
subsection‹Definition (of the association Employee-Boss)›
text‹We start with a oid for the association; this oid can be used
in presence of association classes to represent the association inside an object,
pretty much similar to the \inlineisar+Design_UML+, where we stored
an \verb+oid+ inside the class as ``pointer.''›
definition oid⇩P⇩e⇩r⇩s⇩o⇩nℬ𝒪𝒮𝒮 ::"oid" where "oid⇩P⇩e⇩r⇩s⇩o⇩nℬ𝒪𝒮𝒮 = 10"
text‹From there on, we can already define an empty state which must contain
for $\mathit{oid}_{Person}\mathcal{BOSS}$ the empty relation (encoded as association list, since there are
associations with a Sequence-like structure).›
:: "('𝔄,('a::object) option option) val
⇒ (oid ⇒ ('𝔄,'c::null) val)
⇒ ('𝔄,'c::null) val"
where "eval_extract X f = (λ τ. case X τ of
⊥ ⇒ invalid τ
| ⌊ ⊥ ⌋ ⇒ invalid τ
| ⌊⌊ obj ⌋⌋ ⇒ f (oid_of obj) τ)"
definition "choose⇩2_1 = fst"
definition "choose⇩2_2 = snd"
definition "List_flatten = (λl. (foldl ((λacc. (λl. (foldl ((λacc. (λl. (Cons (l) (acc))))) (acc) ((rev (l))))))) (Nil) ((rev (l)))))"
definition "deref_assocs⇩2" :: "('𝔄 state × '𝔄 state ⇒ '𝔄 state)
⇒ (oid list list ⇒ oid list × oid list)
⇒ oid
⇒ (oid list ⇒ ('𝔄,'f)val)
⇒ oid
⇒ ('𝔄, 'f::null)val"
where "deref_assocs⇩2 pre_post to_from assoc_oid f oid =
(λτ. case (assocs (pre_post τ)) assoc_oid of
⌊ S ⌋ ⇒ f (List_flatten (map (choose⇩2_2 ∘ to_from)
(filter (λ p. List.member (choose⇩2_1 (to_from p)) oid) S)))
τ
| _ ⇒ invalid τ)"
text‹The ‹pre_post›-parameter is configured with ‹fst› or
‹snd›, the ‹to_from›-parameter either with the identity @{term id} or
the following combinator ‹switch›:›
definition "switch⇩2_1 = (λ[x,y]⇒ (x,y))"
definition "switch⇩2_2 = (λ[x,y]⇒ (y,x))"
definition "switch⇩3_1 = (λ[x,y,z]⇒ (x,y))"
definition "switch⇩3_2 = (λ[x,y,z]⇒ (x,z))"
definition "switch⇩3_3 = (λ[x,y,z]⇒ (y,x))"
definition "switch⇩3_4 = (λ[x,y,z]⇒ (y,z))"
definition "switch⇩3_5 = (λ[x,y,z]⇒ (z,x))"
definition "switch⇩3_6 = (λ[x,y,z]⇒ (z,y))"
definition deref_oid⇩P⇩e⇩r⇩s⇩o⇩n :: "(𝔄 state × 𝔄 state ⇒ 𝔄 state)
⇒ (type⇩P⇩e⇩r⇩s⇩o⇩n ⇒ (𝔄, 'c::null)val)
⇒ oid
⇒ (𝔄, 'c::null)val"
where "deref_oid⇩P⇩e⇩r⇩s⇩o⇩n fst_snd f oid = (λτ. case (heap (fst_snd τ)) oid of
⌊ in⇩P⇩e⇩r⇩s⇩o⇩n obj ⌋ ⇒ f obj τ
| _ ⇒ invalid τ)"
definition deref_oid⇩O⇩c⇩l⇩A⇩n⇩y :: "(𝔄 state × 𝔄 state ⇒ 𝔄 state)
⇒ (type⇩O⇩c⇩l⇩A⇩n⇩y ⇒ (𝔄, 'c::null)val)
⇒ oid
⇒ (𝔄, 'c::null)val"
where "deref_oid⇩O⇩c⇩l⇩A⇩n⇩y fst_snd f oid = (λτ. case (heap (fst_snd τ)) oid of
⌊ in⇩O⇩c⇩l⇩A⇩n⇩y obj ⌋ ⇒ f obj τ
| _ ⇒ invalid τ)"
text‹pointer undefined in state or not referencing a type conform object representation›
definition "select⇩O⇩c⇩l⇩A⇩n⇩y𝒜𝒩𝒴 f = (λ X. case X of
(mk⇩O⇩c⇩l⇩A⇩n⇩y _ ⊥) ⇒ null
| (mk⇩O⇩c⇩l⇩A⇩n⇩y _ ⌊any⌋) ⇒ f (λx _. ⌊⌊x⌋⌋) any)"
definition "select⇩P⇩e⇩r⇩s⇩o⇩nℬ𝒪𝒮𝒮 f = select_object mtSet UML_Set.OclIncluding UML_Set.OclANY (f (λx _. ⌊⌊x⌋⌋))"
definition "select⇩P⇩e⇩r⇩s⇩o⇩n𝒮𝒜ℒ𝒜ℛ𝒴 f = (λ X. case X of
(mk⇩P⇩e⇩r⇩s⇩o⇩n _ ⊥) ⇒ null
| (mk⇩P⇩e⇩r⇩s⇩o⇩n _ ⌊salary⌋) ⇒ f (λx _. ⌊⌊x⌋⌋) salary)"
definition "deref_assocs⇩2ℬ𝒪𝒮𝒮 fst_snd f = (λ mk⇩P⇩e⇩r⇩s⇩o⇩n oid _ ⇒
deref_assocs⇩2 fst_snd switch⇩2_1 oid⇩P⇩e⇩r⇩s⇩o⇩nℬ𝒪𝒮𝒮 f oid)"
definition "in_pre_state = fst"
definition "in_post_state = snd"
definition "reconst_basetype = (λ convert x. convert x)"
definition dot⇩O⇩c⇩l⇩A⇩n⇩y𝒜𝒩𝒴 :: "OclAny ⇒ _" ("(1(_).any)" 50)
where "(X).any = eval_extract X
(deref_oid⇩O⇩c⇩l⇩A⇩n⇩y in_post_state
(select⇩O⇩c⇩l⇩A⇩n⇩y𝒜𝒩𝒴
reconst_basetype))"
definition dot⇩P⇩e⇩r⇩s⇩o⇩nℬ𝒪𝒮𝒮 :: "Person ⇒ Person" ("(1(_).boss)" 50)
where "(X).boss = eval_extract X
(deref_oid⇩P⇩e⇩r⇩s⇩o⇩n in_post_state
(deref_assocs⇩2ℬ𝒪𝒮𝒮 in_post_state
(select⇩P⇩e⇩r⇩s⇩o⇩nℬ𝒪𝒮𝒮
(deref_oid⇩P⇩e⇩r⇩s⇩o⇩n in_post_state))))"
definition dot⇩P⇩e⇩r⇩s⇩o⇩n𝒮𝒜ℒ𝒜ℛ𝒴 :: "Person ⇒ Integer" ("(1(_).salary)" 50)
where "(X).salary = eval_extract X
(deref_oid⇩P⇩e⇩r⇩s⇩o⇩n in_post_state
(select⇩P⇩e⇩r⇩s⇩o⇩n𝒮𝒜ℒ𝒜ℛ𝒴
reconst_basetype))"
definition dot⇩O⇩c⇩l⇩A⇩n⇩y𝒜𝒩𝒴_at_pre :: "OclAny ⇒ _" ("(1(_).any@pre)" 50)
where "(X).any@pre = eval_extract X
(deref_oid⇩O⇩c⇩l⇩A⇩n⇩y in_pre_state
(select⇩O⇩c⇩l⇩A⇩n⇩y𝒜𝒩𝒴
reconst_basetype))"
definition dot⇩P⇩e⇩r⇩s⇩o⇩nℬ𝒪𝒮𝒮_at_pre:: "Person ⇒ Person" ("(1(_).boss@pre)" 50)
where "(X).boss@pre = eval_extract X
(deref_oid⇩P⇩e⇩r⇩s⇩o⇩n in_pre_state
(deref_assocs⇩2ℬ𝒪𝒮𝒮 in_pre_state
(select⇩P⇩e⇩r⇩s⇩o⇩nℬ𝒪𝒮𝒮
(deref_oid⇩P⇩e⇩r⇩s⇩o⇩n in_pre_state))))"
definition dot⇩P⇩e⇩r⇩s⇩o⇩n𝒮𝒜ℒ𝒜ℛ𝒴_at_pre:: "Person ⇒ Integer" ("(1(_).salary@pre)" 50)
where "(X).salary@pre = eval_extract X
(deref_oid⇩P⇩e⇩r⇩s⇩o⇩n in_pre_state
(select⇩P⇩e⇩r⇩s⇩o⇩n𝒮𝒜ℒ𝒜ℛ𝒴
reconst_basetype))"
lemmas dot_accessor =
dot⇩O⇩c⇩l⇩A⇩n⇩y𝒜𝒩𝒴_def
dot⇩P⇩e⇩r⇩s⇩o⇩nℬ𝒪𝒮𝒮_def
dot⇩P⇩e⇩r⇩s⇩o⇩n𝒮𝒜ℒ𝒜ℛ𝒴_def
dot⇩O⇩c⇩l⇩A⇩n⇩y𝒜𝒩𝒴_at_pre_def
dot⇩P⇩e⇩r⇩s⇩o⇩nℬ𝒪𝒮𝒮_at_pre_def
dot⇩P⇩e⇩r⇩s⇩o⇩n𝒮𝒜ℒ𝒜ℛ𝒴_at_pre_def
subsection‹Context Passing›
lemmas [simp] = eval_extract_def
lemma cp_dot⇩O⇩c⇩l⇩A⇩n⇩y𝒜𝒩𝒴: "((X).any) τ = ((λ_. X τ).any) τ" by (simp add: dot_accessor)
lemma cp_dot⇩P⇩e⇩r⇩s⇩o⇩nℬ𝒪𝒮𝒮: "((X).boss) τ = ((λ_. X τ).boss) τ" by (simp add: dot_accessor)
lemma cp_dot⇩P⇩e⇩r⇩s⇩o⇩n𝒮𝒜ℒ𝒜ℛ𝒴: "((X).salary) τ = ((λ_. X τ).salary) τ" by (simp add: dot_accessor)
lemma cp_dot⇩O⇩c⇩l⇩A⇩n⇩y𝒜𝒩𝒴_at_pre: "((X).any@pre) τ = ((λ_. X τ).any@pre) τ" by (simp add: dot_accessor)
lemma cp_dot⇩P⇩e⇩r⇩s⇩o⇩nℬ𝒪𝒮𝒮_at_pre: "((X).boss@pre) τ = ((λ_. X τ).boss@pre) τ" by (simp add: dot_accessor)
lemma cp_dot⇩P⇩e⇩r⇩s⇩o⇩n𝒮𝒜ℒ𝒜ℛ𝒴_at_pre: "((X).salary@pre) τ = ((λ_. X τ).salary@pre) τ" by (simp add: dot_accessor)
lemmas cp_dot⇩O⇩c⇩l⇩A⇩n⇩y𝒜𝒩𝒴_I [simp, intro!]=
cp_dot⇩O⇩c⇩l⇩A⇩n⇩y𝒜𝒩𝒴[THEN allI[THEN allI],
of "λ X _. X" "λ _ τ. τ", THEN cpI1]
lemmas cp_dot⇩O⇩c⇩l⇩A⇩n⇩y𝒜𝒩𝒴_at_pre_I [simp, intro!]=
cp_dot⇩O⇩c⇩l⇩A⇩n⇩y𝒜𝒩𝒴_at_pre[THEN allI[THEN allI],
of "λ X _. X" "λ _ τ. τ", THEN cpI1]
lemmas cp_dot⇩P⇩e⇩r⇩s⇩o⇩nℬ𝒪𝒮𝒮_I [simp, intro!]=
cp_dot⇩P⇩e⇩r⇩s⇩o⇩nℬ𝒪𝒮𝒮[THEN allI[THEN allI],
of "λ X _. X" "λ _ τ. τ", THEN cpI1]
lemmas cp_dot⇩P⇩e⇩r⇩s⇩o⇩nℬ𝒪𝒮𝒮_at_pre_I [simp, intro!]=
cp_dot⇩P⇩e⇩r⇩s⇩o⇩nℬ𝒪𝒮𝒮_at_pre[THEN allI[THEN allI],
of "λ X _. X" "λ _ τ. τ", THEN cpI1]
lemmas cp_dot⇩P⇩e⇩r⇩s⇩o⇩n𝒮𝒜ℒ𝒜ℛ𝒴_I [simp, intro!]=
cp_dot⇩P⇩e⇩r⇩s⇩o⇩n𝒮𝒜ℒ𝒜ℛ𝒴[THEN allI[THEN allI],
of "λ X _. X" "λ _ τ. τ", THEN cpI1]
lemmas cp_dot⇩P⇩e⇩r⇩s⇩o⇩n𝒮𝒜ℒ𝒜ℛ𝒴_at_pre_I [simp, intro!]=
cp_dot⇩P⇩e⇩r⇩s⇩o⇩n𝒮𝒜ℒ𝒜ℛ𝒴_at_pre[THEN allI[THEN allI],
of "λ X _. X" "λ _ τ. τ", THEN cpI1]
subsection‹Execution with Invalid or Null as Argument›
lemma dot⇩O⇩c⇩l⇩A⇩n⇩y𝒜𝒩𝒴_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 dot⇩O⇩c⇩l⇩A⇩n⇩y𝒜𝒩𝒴_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 dot⇩O⇩c⇩l⇩A⇩n⇩y𝒜𝒩𝒴_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 dot⇩O⇩c⇩l⇩A⇩n⇩y𝒜𝒩𝒴_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 dot⇩P⇩e⇩r⇩s⇩o⇩nℬ𝒪𝒮𝒮_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 dot⇩P⇩e⇩r⇩s⇩o⇩nℬ𝒪𝒮𝒮_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 dot⇩P⇩e⇩r⇩s⇩o⇩nℬ𝒪𝒮𝒮_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 dot⇩P⇩e⇩r⇩s⇩o⇩nℬ𝒪𝒮𝒮_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 dot⇩P⇩e⇩r⇩s⇩o⇩n𝒮𝒜ℒ𝒜ℛ𝒴_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 dot⇩P⇩e⇩r⇩s⇩o⇩n𝒮𝒜ℒ𝒜ℛ𝒴_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 dot⇩P⇩e⇩r⇩s⇩o⇩n𝒮𝒜ℒ𝒜ℛ𝒴_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 dot⇩P⇩e⇩r⇩s⇩o⇩n𝒮𝒜ℒ𝒜ℛ𝒴_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 dot⇩P⇩e⇩r⇩s⇩o⇩nℬ𝒪𝒮𝒮_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 dot⇩P⇩e⇩r⇩s⇩o⇩nℬ𝒪𝒮𝒮_def_mono, simplified foundation16])
unfolding is_represented_in_state_def
dot⇩P⇩e⇩r⇩s⇩o⇩nℬ𝒪𝒮𝒮_def eval_extract_def select⇩P⇩e⇩r⇩s⇩o⇩nℬ𝒪𝒮𝒮_def in_post_state_def
oops
lemma repr_bossX :
assumes A: "τ ⊨ δ(x .boss)"
shows "τ ⊨ ((Person .allInstances()) ->includes⇩S⇩e⇩t(x .boss))"
oops
section‹A Little Infra-structure on Example States›
text‹
The example we are defining in this section comes from the figure~\ref{fig:eam1_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:eam1_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 ≡ mk⇩P⇩e⇩r⇩s⇩o⇩n oid0 ⌊1300⌋"
definition "person2 ≡ mk⇩P⇩e⇩r⇩s⇩o⇩n oid1 ⌊1800⌋"
definition "person3 ≡ mk⇩P⇩e⇩r⇩s⇩o⇩n oid2 None"
definition "person4 ≡ mk⇩P⇩e⇩r⇩s⇩o⇩n oid3 ⌊2900⌋"
definition "person5 ≡ mk⇩P⇩e⇩r⇩s⇩o⇩n oid4 ⌊3500⌋"
definition "person6 ≡ mk⇩P⇩e⇩r⇩s⇩o⇩n oid5 ⌊2500⌋"
definition "person7 ≡ mk⇩O⇩c⇩l⇩A⇩n⇩y oid6 ⌊⌊3200⌋⌋"
definition "person8 ≡ mk⇩O⇩c⇩l⇩A⇩n⇩y oid7 None"
definition "person9 ≡ mk⇩P⇩e⇩r⇩s⇩o⇩n oid8 ⌊0⌋"
text_raw‹\endisatagafp›
definition
"σ⇩1 ≡ ⦇ heap = Map.empty(oid0 ↦ in⇩P⇩e⇩r⇩s⇩o⇩n (mk⇩P⇩e⇩r⇩s⇩o⇩n oid0 ⌊1000⌋),
oid1 ↦ in⇩P⇩e⇩r⇩s⇩o⇩n (mk⇩P⇩e⇩r⇩s⇩o⇩n oid1 ⌊1200⌋),
oid3 ↦ in⇩P⇩e⇩r⇩s⇩o⇩n (mk⇩P⇩e⇩r⇩s⇩o⇩n oid3 ⌊2600⌋),
oid4 ↦ in⇩P⇩e⇩r⇩s⇩o⇩n person5,
oid5 ↦ in⇩P⇩e⇩r⇩s⇩o⇩n (mk⇩P⇩e⇩r⇩s⇩o⇩n oid5 ⌊2300⌋),
oid8 ↦ in⇩P⇩e⇩r⇩s⇩o⇩n person9),
assocs = Map.empty(oid⇩P⇩e⇩r⇩s⇩o⇩nℬ𝒪𝒮𝒮 ↦ [[[oid0],[oid1]],[[oid3],[oid4]],[[oid5],[oid3]]]) ⦈"
definition
"σ⇩1' ≡ ⦇ heap = Map.empty(oid0 ↦ in⇩P⇩e⇩r⇩s⇩o⇩n person1,
oid1 ↦ in⇩P⇩e⇩r⇩s⇩o⇩n person2,
oid2 ↦ in⇩P⇩e⇩r⇩s⇩o⇩n person3,
oid3 ↦ in⇩P⇩e⇩r⇩s⇩o⇩n person4,
oid5 ↦ in⇩P⇩e⇩r⇩s⇩o⇩n person6,
oid6 ↦ in⇩O⇩c⇩l⇩A⇩n⇩y person7,
oid7 ↦ in⇩O⇩c⇩l⇩A⇩n⇩y person8,
oid8 ↦ in⇩P⇩e⇩r⇩s⇩o⇩n person9),
assocs = Map.empty(oid⇩P⇩e⇩r⇩s⇩o⇩nℬ𝒪𝒮𝒮 ↦ [[[oid0],[oid1]],[[oid1],[oid1]],[[oid5],[oid6]],[[oid6],[oid6]]]) ⦈"
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_type⇩P⇩e⇩r⇩s⇩o⇩n_def oid_of_type⇩O⇩c⇩l⇩A⇩n⇩y_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,oid3,oid4,oid5,oid8}"
by(auto simp: σ⇩1_def)
lemma [simp,code_unfold]: "dom (heap σ⇩1') = {oid0,oid1,oid2,oid3,oid5,oid6,oid7,oid8}"
by(auto simp: σ⇩1'_def)
text_raw‹\isatagafp›
definition "X⇩P⇩e⇩r⇩s⇩o⇩n1 :: Person ≡ λ _ .⌊⌊ person1 ⌋⌋"
definition "X⇩P⇩e⇩r⇩s⇩o⇩n2 :: Person ≡ λ _ .⌊⌊ person2 ⌋⌋"
definition "X⇩P⇩e⇩r⇩s⇩o⇩n3 :: Person ≡ λ _ .⌊⌊ person3 ⌋⌋"
definition "X⇩P⇩e⇩r⇩s⇩o⇩n4 :: Person ≡ λ _ .⌊⌊ person4 ⌋⌋"
definition "X⇩P⇩e⇩r⇩s⇩o⇩n5 :: Person ≡ λ _ .⌊⌊ person5 ⌋⌋"
definition "X⇩P⇩e⇩r⇩s⇩o⇩n6 :: Person ≡ λ _ .⌊⌊ person6 ⌋⌋"
definition "X⇩P⇩e⇩r⇩s⇩o⇩n7 :: OclAny ≡ λ _ .⌊⌊ person7 ⌋⌋"
definition "X⇩P⇩e⇩r⇩s⇩o⇩n8 :: OclAny ≡ λ _ .⌊⌊ person8 ⌋⌋"
definition "X⇩P⇩e⇩r⇩s⇩o⇩n9 :: Person ≡ λ _ .⌊⌊ person9 ⌋⌋"
lemma [code_unfold]: "((x::Person) ≐ y) = StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t x y" by(simp only: StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t_⇩P⇩e⇩r⇩s⇩o⇩n)
lemma [code_unfold]: "((x::OclAny) ≐ y) = StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t x y" by(simp only: StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t_⇩O⇩c⇩l⇩A⇩n⇩y)
lemmas [simp,code_unfold] =
OclAsType⇩O⇩c⇩l⇩A⇩n⇩y_OclAny
OclAsType⇩O⇩c⇩l⇩A⇩n⇩y_Person
OclAsType⇩P⇩e⇩r⇩s⇩o⇩n_OclAny
OclAsType⇩P⇩e⇩r⇩s⇩o⇩n_Person
OclIsTypeOf⇩O⇩c⇩l⇩A⇩n⇩y_OclAny
OclIsTypeOf⇩O⇩c⇩l⇩A⇩n⇩y_Person
OclIsTypeOf⇩P⇩e⇩r⇩s⇩o⇩n_OclAny
OclIsTypeOf⇩P⇩e⇩r⇩s⇩o⇩n_Person
OclIsKindOf⇩O⇩c⇩l⇩A⇩n⇩y_OclAny
OclIsKindOf⇩O⇩c⇩l⇩A⇩n⇩y_Person
OclIsKindOf⇩P⇩e⇩r⇩s⇩o⇩n_OclAny
OclIsKindOf⇩P⇩e⇩r⇩s⇩o⇩n_Person
text_raw‹\endisatagafp›
Assert "⋀s⇩p⇩r⇩e . (s⇩p⇩r⇩e,σ⇩1') ⊨ (X⇩P⇩e⇩r⇩s⇩o⇩n1 .salary <> 𝟭𝟬𝟬𝟬)"
Assert "⋀s⇩p⇩r⇩e . (s⇩p⇩r⇩e,σ⇩1') ⊨ (X⇩P⇩e⇩r⇩s⇩o⇩n1 .salary ≐ 𝟭𝟯𝟬𝟬)"
Assert "⋀ s⇩p⇩o⇩s⇩t. (σ⇩1,s⇩p⇩o⇩s⇩t) ⊨ (X⇩P⇩e⇩r⇩s⇩o⇩n1 .salary@pre ≐ 𝟭𝟬𝟬𝟬)"
Assert "⋀ s⇩p⇩o⇩s⇩t. (σ⇩1,s⇩p⇩o⇩s⇩t) ⊨ (X⇩P⇩e⇩r⇩s⇩o⇩n1 .salary@pre <> 𝟭𝟯𝟬𝟬)"
lemma " (σ⇩1,σ⇩1') ⊨ (X⇩P⇩e⇩r⇩s⇩o⇩n1 .oclIsMaintained())"
by(simp add: OclValid_def OclIsMaintained_def
σ⇩1_def σ⇩1'_def
X⇩P⇩e⇩r⇩s⇩o⇩n1_def person1_def
oid0_def oid1_def oid2_def oid3_def oid4_def oid5_def oid6_def
oid_of_option_def oid_of_type⇩P⇩e⇩r⇩s⇩o⇩n_def)
lemma "⋀s⇩p⇩r⇩e s⇩p⇩o⇩s⇩t. (s⇩p⇩r⇩e,s⇩p⇩o⇩s⇩t) ⊨ ((X⇩P⇩e⇩r⇩s⇩o⇩n1 .oclAsType(OclAny) .oclAsType(Person)) ≐ X⇩P⇩e⇩r⇩s⇩o⇩n1)"
by(rule up_down_cast_Person_OclAny_Person', simp add: X⇩P⇩e⇩r⇩s⇩o⇩n1_def)
Assert "⋀s⇩p⇩r⇩e s⇩p⇩o⇩s⇩t. (s⇩p⇩r⇩e,s⇩p⇩o⇩s⇩t) ⊨ (X⇩P⇩e⇩r⇩s⇩o⇩n1 .oclIsTypeOf(Person))"
Assert "⋀s⇩p⇩r⇩e s⇩p⇩o⇩s⇩t. (s⇩p⇩r⇩e,s⇩p⇩o⇩s⇩t) ⊨ not(X⇩P⇩e⇩r⇩s⇩o⇩n1 .oclIsTypeOf(OclAny))"
Assert "⋀s⇩p⇩r⇩e s⇩p⇩o⇩s⇩t. (s⇩p⇩r⇩e,s⇩p⇩o⇩s⇩t) ⊨ (X⇩P⇩e⇩r⇩s⇩o⇩n1 .oclIsKindOf(Person))"
Assert "⋀s⇩p⇩r⇩e s⇩p⇩o⇩s⇩t. (s⇩p⇩r⇩e,s⇩p⇩o⇩s⇩t) ⊨ (X⇩P⇩e⇩r⇩s⇩o⇩n1 .oclIsKindOf(OclAny))"
Assert "⋀s⇩p⇩r⇩e s⇩p⇩o⇩s⇩t. (s⇩p⇩r⇩e,s⇩p⇩o⇩s⇩t) ⊨ not(X⇩P⇩e⇩r⇩s⇩o⇩n1 .oclAsType(OclAny) .oclIsTypeOf(OclAny))"
Assert "⋀s⇩p⇩r⇩e . (s⇩p⇩r⇩e,σ⇩1') ⊨ (X⇩P⇩e⇩r⇩s⇩o⇩n2 .salary ≐ 𝟭𝟴𝟬𝟬)"
Assert "⋀ s⇩p⇩o⇩s⇩t. (σ⇩1,s⇩p⇩o⇩s⇩t) ⊨ (X⇩P⇩e⇩r⇩s⇩o⇩n2 .salary@pre ≐ 𝟭𝟮𝟬𝟬)"
lemma " (σ⇩1,σ⇩1') ⊨ (X⇩P⇩e⇩r⇩s⇩o⇩n2 .oclIsMaintained())"
by(simp add: OclValid_def OclIsMaintained_def σ⇩1_def σ⇩1'_def X⇩P⇩e⇩r⇩s⇩o⇩n2_def person2_def
oid0_def oid1_def oid2_def oid3_def oid4_def oid5_def oid6_def
oid_of_option_def oid_of_type⇩P⇩e⇩r⇩s⇩o⇩n_def)
Assert "⋀s⇩p⇩r⇩e . (s⇩p⇩r⇩e,σ⇩1') ⊨ (X⇩P⇩e⇩r⇩s⇩o⇩n3 .salary ≐ null)"
Assert "⋀ s⇩p⇩o⇩s⇩t. (σ⇩1,s⇩p⇩o⇩s⇩t) ⊨ not(υ(X⇩P⇩e⇩r⇩s⇩o⇩n3 .salary@pre))"
lemma " (σ⇩1,σ⇩1') ⊨ (X⇩P⇩e⇩r⇩s⇩o⇩n3 .oclIsNew())"
by(simp add: OclValid_def OclIsNew_def σ⇩1_def σ⇩1'_def X⇩P⇩e⇩r⇩s⇩o⇩n3_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_type⇩P⇩e⇩r⇩s⇩o⇩n_def)
lemma " (σ⇩1,σ⇩1') ⊨ (X⇩P⇩e⇩r⇩s⇩o⇩n4 .oclIsMaintained())"
by(simp add: OclValid_def OclIsMaintained_def σ⇩1_def σ⇩1'_def X⇩P⇩e⇩r⇩s⇩o⇩n4_def person4_def
oid0_def oid1_def oid2_def oid3_def oid4_def oid5_def oid6_def
oid_of_option_def oid_of_type⇩P⇩e⇩r⇩s⇩o⇩n_def)
Assert "⋀s⇩p⇩r⇩e . (s⇩p⇩r⇩e,σ⇩1') ⊨ not(υ(X⇩P⇩e⇩r⇩s⇩o⇩n5 .salary))"
Assert "⋀ s⇩p⇩o⇩s⇩t. (σ⇩1,s⇩p⇩o⇩s⇩t) ⊨ (X⇩P⇩e⇩r⇩s⇩o⇩n5 .salary@pre ≐ 𝟯𝟱𝟬𝟬)"
lemma " (σ⇩1,σ⇩1') ⊨ (X⇩P⇩e⇩r⇩s⇩o⇩n5 .oclIsDeleted())"
by(simp add: OclNot_def OclValid_def OclIsDeleted_def σ⇩1_def σ⇩1'_def X⇩P⇩e⇩r⇩s⇩o⇩n5_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_type⇩P⇩e⇩r⇩s⇩o⇩n_def)
lemma " (σ⇩1,σ⇩1') ⊨ (X⇩P⇩e⇩r⇩s⇩o⇩n6 .oclIsMaintained())"
by(simp add: OclValid_def OclIsMaintained_def σ⇩1_def σ⇩1'_def X⇩P⇩e⇩r⇩s⇩o⇩n6_def person6_def
oid0_def oid1_def oid2_def oid3_def oid4_def oid5_def oid6_def
oid_of_option_def oid_of_type⇩P⇩e⇩r⇩s⇩o⇩n_def)
Assert "⋀s⇩p⇩r⇩e s⇩p⇩o⇩s⇩t. (s⇩p⇩r⇩e,s⇩p⇩o⇩s⇩t) ⊨ υ(X⇩P⇩e⇩r⇩s⇩o⇩n7 .oclAsType(Person))"
lemma "⋀s⇩p⇩r⇩e s⇩p⇩o⇩s⇩t. (s⇩p⇩r⇩e,s⇩p⇩o⇩s⇩t) ⊨ ((X⇩P⇩e⇩r⇩s⇩o⇩n7 .oclAsType(Person) .oclAsType(OclAny)
.oclAsType(Person))
≐ (X⇩P⇩e⇩r⇩s⇩o⇩n7 .oclAsType(Person)))"
by(rule up_down_cast_Person_OclAny_Person', simp add: X⇩P⇩e⇩r⇩s⇩o⇩n7_def OclValid_def valid_def person7_def)
lemma " (σ⇩1,σ⇩1') ⊨ (X⇩P⇩e⇩r⇩s⇩o⇩n7 .oclIsNew())"
by(simp add: OclValid_def OclIsNew_def σ⇩1_def σ⇩1'_def X⇩P⇩e⇩r⇩s⇩o⇩n7_def