Theory UML_Logic
chapter‹Formalization II: OCL Terms and Library Operations›
theory UML_Logic
imports UML_Types
begin
section‹The Operations of the Boolean Type and the OCL Logic›
subsection‹Basic Constants›
lemma bot_Boolean_def : "(bot::('𝔄)Boolean) = (λ τ. ⊥)"
by(simp add: bot_fun_def bot_option_def)
lemma null_Boolean_def : "(null::('𝔄)Boolean) = (λ τ. ⌊⊥⌋)"
by(simp add: null_fun_def null_option_def bot_option_def)
definition true :: "('𝔄)Boolean"
where "true ≡ λ τ. ⌊⌊True⌋⌋"
definition false :: "('𝔄)Boolean"
where "false ≡ λ τ. ⌊⌊False⌋⌋"
lemma bool_split_0: "X τ = invalid τ ∨ X τ = null τ ∨
X τ = true τ ∨ X τ = false τ"
apply(simp add: invalid_def null_def true_def false_def)
apply(case_tac "X τ",simp_all add: null_fun_def null_option_def bot_option_def)
apply(case_tac "a",simp)
apply(case_tac "aa",simp)
apply auto
done
lemma [simp]: "false (a, b) = ⌊⌊False⌋⌋"
by(simp add:false_def)
lemma [simp]: "true (a, b) = ⌊⌊True⌋⌋"
by(simp add:true_def)
lemma textbook_true: "I⟦true⟧ τ = ⌊⌊True⌋⌋"
by(simp add: Sem_def true_def)
lemma textbook_false: "I⟦false⟧ τ = ⌊⌊False⌋⌋"
by(simp add: Sem_def false_def)
text ‹
\begin{table}[htbp]
\centering
\begin{tabu}{lX[,c,]}
\toprule
Name & Theorem \\
\midrule
@{thm [source] textbook_invalid} & @{thm [display=false] textbook_invalid} \\
@{thm [source] textbook_null_fun} & @{thm [display=false] textbook_null_fun} \\
@{thm [source] textbook_true} & @{thm [display=false] textbook_true} \\
@{thm [source] textbook_false} & @{thm [display=false] textbook_false} \\
\bottomrule
\end{tabu}
\caption{Basic semantic constant definitions of the logic}
\label{tab:sem_basic_constants}
\end{table}
›
subsection‹Validity and Definedness›
text‹However, this has also the consequence that core concepts like definedness,
validity and even cp have to be redefined on this type class:›
definition valid :: "('𝔄,'a::null)val ⇒ ('𝔄)Boolean" (‹υ _› [100]100)
where "υ X ≡ λ τ . if X τ = bot τ then false τ else true τ"
lemma valid1[simp]: "υ invalid = false"
by(rule ext,simp add: valid_def bot_fun_def bot_option_def
invalid_def true_def false_def)
lemma valid2[simp]: "υ null = true"
by(rule ext,simp add: valid_def bot_fun_def bot_option_def null_is_valid
null_fun_def invalid_def true_def false_def)
lemma valid3[simp]: "υ true = true"
by(rule ext,simp add: valid_def bot_fun_def bot_option_def null_is_valid
null_fun_def invalid_def true_def false_def)
lemma valid4[simp]: "υ false = true"
by(rule ext,simp add: valid_def bot_fun_def bot_option_def null_is_valid
null_fun_def invalid_def true_def false_def)
text_raw‹\isatagafp›
lemma cp_valid: "(υ X) τ = (υ (λ _. X τ)) τ"
by(simp add: valid_def)
text_raw‹\endisatagafp›
definition defined :: "('𝔄,'a::null)val ⇒ ('𝔄)Boolean" (‹δ _› [100]100)
where "δ X ≡ λ τ . if X τ = bot τ ∨ X τ = null τ then false τ else true τ"
text‹The generalized definitions of invalid and definedness have the same
properties as the old ones :›
lemma defined1[simp]: "δ invalid = false"
by(rule ext,simp add: defined_def bot_fun_def bot_option_def
null_def invalid_def true_def false_def)
lemma defined2[simp]: "δ null = false"
by(rule ext,simp add: defined_def bot_fun_def bot_option_def
null_def null_option_def null_fun_def invalid_def true_def false_def)
lemma defined3[simp]: "δ true = true"
by(rule ext,simp add: defined_def bot_fun_def bot_option_def null_is_valid null_option_def
null_fun_def invalid_def true_def false_def)
lemma defined4[simp]: "δ false = true"
by(rule ext,simp add: defined_def bot_fun_def bot_option_def null_is_valid null_option_def
null_fun_def invalid_def true_def false_def)
lemma defined5[simp]: "δ δ X = true"
by(rule ext,
auto simp: defined_def true_def false_def
bot_fun_def bot_option_def null_option_def null_fun_def)
lemma defined6[simp]: "δ υ X = true"
by(rule ext,
auto simp: valid_def defined_def true_def false_def
bot_fun_def bot_option_def null_option_def null_fun_def)
lemma valid5[simp]: "υ υ X = true"
by(rule ext,
auto simp: valid_def true_def false_def
bot_fun_def bot_option_def null_option_def null_fun_def)
lemma valid6[simp]: "υ δ X = true"
by(rule ext,
auto simp: valid_def defined_def true_def false_def
bot_fun_def bot_option_def null_option_def null_fun_def)
text_raw‹\isatagafp›
lemma cp_defined:"(δ X)τ = (δ (λ _. X τ)) τ"
by(simp add: defined_def)
text_raw‹\endisatagafp›
text‹The definitions above for the constants @{const defined} and @{const valid}
can be rewritten into the conventional semantic "textbook" format as follows:›
lemma textbook_defined: "I⟦δ(X)⟧ τ = (if I⟦X⟧ τ = I⟦bot⟧ τ ∨ I⟦X⟧ τ = I⟦null⟧ τ
then I⟦false⟧ τ
else I⟦true⟧ τ)"
by(simp add: Sem_def defined_def)
lemma textbook_valid: "I⟦υ(X)⟧ τ = (if I⟦X⟧ τ = I⟦bot⟧ τ
then I⟦false⟧ τ
else I⟦true⟧ τ)"
by(simp add: Sem_def valid_def)
text ‹
\autoref{tab:sem_definedness} and \autoref{tab:alglaws_definedness}
summarize the results of this section.
\begin{table}[htbp]
\centering
\begin{tabu}{lX[,c,]}
\toprule
Name & Theorem \\
\midrule
@{thm [source] textbook_defined} & @{thm [show_question_marks=false,display=false,margin=45] textbook_defined} \\
@{thm [source] textbook_valid} & @{thm [show_question_marks=false,display=false,margin=45] textbook_valid} \\
\bottomrule
\end{tabu}
\caption{Basic predicate definitions of the logic.}
\label{tab:sem_definedness}
\end{table}
\begin{table}[htbp]
\centering
\begin{tabu}{lX[,c,]}
\toprule
Name & Theorem \\
\midrule
@{thm [source] defined1} & @{thm defined1} \\
@{thm [source] defined2} & @{thm [display=false,margin=35] defined2} \\
@{thm [source] defined3} & @{thm [display=false,margin=35] defined3} \\
@{thm [source] defined4} & @{thm [display=false,margin=35] defined4} \\
@{thm [source] defined5} & @{thm [display=false,margin=35] defined5} \\
@{thm [source] defined6} & @{thm [display=false,margin=35] defined6} \\
\bottomrule
\end{tabu}
\caption{Laws of the basic predicates of the logic.}
\label{tab:alglaws_definedness}
\end{table}
›
subsection‹The Equalities of OCL \label{sec:equality}›
text‹
The OCL contains a particular version of equality, written in
Standard documents \inlineocl+_ = _+ and \inlineocl+_ <> _+ for its
negation, which is referred as \emph{weak referential equality}
hereafter and for which we use the symbol \inlineisar+_ ≐ _+
throughout the formal part of this document. Its semantics is
motivated by the desire of fast execution, and similarity to
languages like Java and C, but does not satisfy the needs of logical
reasoning over OCL expressions and specifications. We therefore
introduce a second equality, referred as \emph{strong equality} or
\emph{logical equality} and written \inlineisar+_ ≜ _+
which is not present in the current standard but was discussed in
prior texts on OCL like the Amsterdam
Manifesto~\<^cite>‹"cook.ea::amsterdam:2002"› and was identified as
desirable extension of OCL in the Aachen
Meeting~\<^cite>‹"brucker.ea:summary-aachen:2013"› in the future 2.5 OCL
Standard. The purpose of strong equality is to define and reason
over OCL. It is therefore a natural task in Featherweight OCL to
formally investigate the somewhat quite complex relationship between
these two.› text‹Strong equality has two motivations: a
pragmatic one and a fundamental one.
\begin{enumerate}
\item The pragmatic reason is fairly simple: users of object-oriented languages want
something like a ``shallow object value equality''.
You will want to say
\inlineisar+ a.boss ≜ b.boss@pre +
instead of
\begin{isar}
a.boss ≐ b.boss@pre and (* just the pointers are equal! *)
a.boss.name ≐ b.boss@pre.name@pre and
a.boss.age ≐ b.boss@pre.age@pre
\end{isar}
Breaking a shallow-object equality down to referential equality
of attributes is cumbersome, error-prone, and makes
specifications difficult to extend (add for example an attribute
sex to your class, and check in your OCL specification
everywhere that you did it right with your simulation of strong
equality). Therefore, languages like Java offer facilities
to handle two different equalities, and it is problematic even
in an execution oriented specification language to ignore
shallow object equality because it is so common in the code.
\item The fundamental reason goes as follows: whatever you do to
reason consistently over a language, you need the concept of
equality: you need to know what expressions can be replaced by
others because they \emph{mean the same thing.} People call
this also ``Leibniz Equality'' because this philosopher brought
this principle first explicitly to paper and shed some light
over it. It is the theoretic foundation of what you do in an
optimizing compiler: you replace expressions by \emph{equal}
ones, which you hope are easier to evaluate. In a typed
language, strong equality exists uniformly over all types, it is
``polymorphic'' $\_ = \_ :: \alpha * \alpha \rightarrow
bool$---this is the way that equality is defined in HOL itself.
We can express Leibniz principle as one logical rule of
surprising simplicity and beauty:
\begin{gather}
s = t \Longrightarrow P(s) = P(t)
\end{gather}
``Whenever we know, that $s$ is equal to $t$, we can replace the
sub-expression $s$ in a term $P$ by $t$ and we have that the
replacement is equal to the original.''
\end{enumerate}
›
text‹
While weak referential equality is defined to be strict in the OCL
standard, we will define strong equality as non-strict. It is quite
nasty (but not impossible) to define the logical equality in a
strict way (the substitutivity rule above would look more complex),
however, whenever references were used, strong equality is needed
since references refer to particular states (pre or post), and that
they mean the same thing can therefore not be taken for granted.
›
subsubsection‹Definition›
text‹
The strict equality on basic types (actually on all types) must be
exceptionally defined on @{term "null"}---otherwise the entire
concept of null in the language does not make much sense. This is an
important exception from the general rule that null
arguments---especially if passed as ``self''-argument---lead to
invalid results.
›
text‹
We define strong equality extremely generic, even for types that
contain a ‹null› or ‹⊥› element. Strong
equality is simply polymorphic in Featherweight OCL, \ie, is
defined identical for all types in OCL and HOL.
›
definition StrongEq::"['𝔄 st ⇒ 'α,'𝔄 st ⇒ 'α] ⇒ ('𝔄)Boolean" (infixl ‹≜› 30)
where "X ≜ Y ≡ λ τ. ⌊⌊X τ = Y τ ⌋⌋"
text‹
From this follow already elementary properties like:
›
lemma [simp,code_unfold]: "(true ≜ false) = false"
by(rule ext, auto simp: StrongEq_def)
lemma [simp,code_unfold]: "(false ≜ true) = false"
by(rule ext, auto simp: StrongEq_def)
subsubsection‹Fundamental Predicates on Strong Equality›
text‹Equality reasoning in OCL is not humpty dumpty. While strong equality
is clearly an equivalence:›
lemma StrongEq_refl [simp]: "(X ≜ X) = true"
by(rule ext, simp add: null_def invalid_def true_def false_def StrongEq_def)
lemma StrongEq_sym: "(X ≜ Y) = (Y ≜ X)"
by(rule ext, simp add: eq_sym_conv invalid_def true_def false_def StrongEq_def)
lemma StrongEq_trans_strong [simp]:
assumes A: "(X ≜ Y) = true"
and B: "(Y ≜ Z) = true"
shows "(X ≜ Z) = true"
apply(insert A B) apply(rule ext)
apply(simp add: null_def invalid_def true_def false_def StrongEq_def)
apply(drule_tac x=x in fun_cong)+
by auto
text‹
it is only in a limited sense a congruence, at least from the
point of view of this semantic theory. The point is that it is
only a congruence on OCL expressions, not arbitrary HOL
expressions (with which we can mix Featherweight OCL expressions). A
semantic---not syntactic---characterization of OCL expressions is
that they are \emph{context-passing} or \emph{context-invariant},
\ie, the context of an entire OCL expression, \ie the pre and
post state it referes to, is passed constantly and unmodified to
the sub-expressions, \ie, all sub-expressions inside an OCL
expression refer to the same context. Expressed formally, this
boils down to:
›
lemma StrongEq_subst :
assumes cp: "⋀X. P(X)τ = P(λ _. X τ)τ"
and eq: "(X ≜ Y)τ = true τ"
shows "(P X ≜ P Y)τ = true τ"
apply(insert cp eq)
apply(simp add: null_def invalid_def true_def false_def StrongEq_def)
apply(subst cp[of X])
apply(subst cp[of Y])
by simp
lemma defined7[simp]: "δ (X ≜ Y) = true"
by(rule ext,
auto simp: defined_def true_def false_def StrongEq_def
bot_fun_def bot_option_def null_option_def null_fun_def)
lemma valid7[simp]: "υ (X ≜ Y) = true"
by(rule ext,
auto simp: valid_def true_def false_def StrongEq_def
bot_fun_def bot_option_def null_option_def null_fun_def)
lemma cp_StrongEq: "(X ≜ Y) τ = ((λ _. X τ) ≜ (λ _. Y τ)) τ"
by(simp add: StrongEq_def)
subsection‹Logical Connectives and their Universal Properties›
text‹
It is a design goal to give OCL a semantics that is as closely as
possible to a ``logical system'' in a known sense; a specification
logic where the logical connectives can not be understood other that
having the truth-table aside when reading fails its purpose in our
view.
Practically, this means that we want to give a definition to the
core operations to be as close as possible to the lattice laws; this
makes also powerful symbolic normalization of OCL specifications
possible as a pre-requisite for automated theorem provers. For
example, it is still possible to compute without any definedness
and validity reasoning the DNF of an OCL specification; be it for
test-case generations or for a smooth transition to a two-valued
representation of the specification amenable to fast standard
SMT-solvers, for example.
Thus, our representation of the OCL is merely a 4-valued
Kleene-Logics with @{term "invalid"} as least, @{term "null"} as
middle and @{term "true"} resp. @{term "false"} as unrelated
top-elements.
›
definition OclNot :: "('𝔄)Boolean ⇒ ('𝔄)Boolean" (‹not›)
where "not X ≡ λ τ . case X τ of
⊥ ⇒ ⊥
| ⌊ ⊥ ⌋ ⇒ ⌊ ⊥ ⌋
| ⌊⌊ x ⌋⌋ ⇒ ⌊⌊ ¬ x ⌋⌋"
lemma cp_OclNot: "(not X)τ = (not (λ _. X τ)) τ"
by(simp add: OclNot_def)
lemma OclNot1[simp]: "not invalid = invalid"
by(rule ext,simp add: OclNot_def null_def invalid_def true_def false_def bot_option_def)
lemma OclNot2[simp]: "not null = null"
by(rule ext,simp add: OclNot_def null_def invalid_def true_def false_def
bot_option_def null_fun_def null_option_def )
lemma OclNot3[simp]: "not true = false"
by(rule ext,simp add: OclNot_def null_def invalid_def true_def false_def)
lemma OclNot4[simp]: "not false = true"
by(rule ext,simp add: OclNot_def null_def invalid_def true_def false_def)
lemma OclNot_not[simp]: "not (not X) = X"
apply(rule ext,simp add: OclNot_def null_def invalid_def true_def false_def)
apply(case_tac "X x", simp_all)
apply(case_tac "a", simp_all)
done
lemma OclNot_inject: "⋀ x y. not x = not y ⟹ x = y"
by(subst OclNot_not[THEN sym], simp)
definition OclAnd :: "[('𝔄)Boolean, ('𝔄)Boolean] ⇒ ('𝔄)Boolean" (infixl ‹and› 30)
where "X and Y ≡ (λ τ . case X τ of
⌊⌊False⌋⌋ ⇒ ⌊⌊False⌋⌋
| ⊥ ⇒ (case Y τ of
⌊⌊False⌋⌋ ⇒ ⌊⌊False⌋⌋
| _ ⇒ ⊥)
| ⌊⊥⌋ ⇒ (case Y τ of
⌊⌊False⌋⌋ ⇒ ⌊⌊False⌋⌋
| ⊥ ⇒ ⊥
| _ ⇒ ⌊⊥⌋)
| ⌊⌊True⌋⌋ ⇒ Y τ)"
text‹
Note that @{term "not"} is \emph{not} defined as a strict function;
proximity to lattice laws implies that we \emph{need} a definition
of @{term "not"} that satisfies ‹not(not(x))=x›.
›
text‹
In textbook notation, the logical core constructs @{const
"OclNot"} and @{const "OclAnd"} were represented as follows:
›
lemma textbook_OclNot:
"I⟦not(X)⟧ τ = (case I⟦X⟧ τ of ⊥ ⇒ ⊥
| ⌊ ⊥ ⌋ ⇒ ⌊ ⊥ ⌋
| ⌊⌊ x ⌋⌋ ⇒ ⌊⌊ ¬ x ⌋⌋)"
by(simp add: Sem_def OclNot_def)
lemma textbook_OclAnd:
"I⟦X and Y⟧ τ = (case I⟦X⟧ τ of
⊥ ⇒ (case I⟦Y⟧ τ of
⊥ ⇒ ⊥
| ⌊⊥⌋ ⇒ ⊥
| ⌊⌊True⌋⌋ ⇒ ⊥
| ⌊⌊False⌋⌋ ⇒ ⌊⌊False⌋⌋)
| ⌊ ⊥ ⌋ ⇒ (case I⟦Y⟧ τ of
⊥ ⇒ ⊥
| ⌊⊥⌋ ⇒ ⌊⊥⌋
| ⌊⌊True⌋⌋ ⇒ ⌊⊥⌋
| ⌊⌊False⌋⌋ ⇒ ⌊⌊False⌋⌋)
| ⌊⌊True⌋⌋ ⇒ (case I⟦Y⟧ τ of
⊥ ⇒ ⊥
| ⌊⊥⌋ ⇒ ⌊⊥⌋
| ⌊⌊y⌋⌋ ⇒ ⌊⌊y⌋⌋)
| ⌊⌊False⌋⌋ ⇒ ⌊⌊ False ⌋⌋)"
by(simp add: OclAnd_def Sem_def split: option.split bool.split)
definition OclOr :: "[('𝔄)Boolean, ('𝔄)Boolean] ⇒ ('𝔄)Boolean" (infixl ‹or› 25)
where "X or Y ≡ not(not X and not Y)"
definition OclImplies :: "[('𝔄)Boolean, ('𝔄)Boolean] ⇒ ('𝔄)Boolean" (infixl ‹implies› 25)
where "X implies Y ≡ not X or Y"
lemma cp_OclAnd:"(X and Y) τ = ((λ _. X τ) and (λ _. Y τ)) τ"
by(simp add: OclAnd_def)
lemma cp_OclOr:"((X::('𝔄)Boolean) or Y) τ = ((λ _. X τ) or (λ _. Y τ)) τ"
apply(simp add: OclOr_def)
apply(subst cp_OclNot[of "not (λ_. X τ) and not (λ_. Y τ)"])
apply(subst cp_OclAnd[of "not (λ_. X τ)" "not (λ_. Y τ)"])
by(simp add: cp_OclNot[symmetric] cp_OclAnd[symmetric] )
lemma cp_OclImplies:"(X implies Y) τ = ((λ _. X τ) implies (λ _. Y τ)) τ"
apply(simp add: OclImplies_def)
apply(subst cp_OclOr[of "not (λ_. X τ)" "(λ_. Y τ)"])
by(simp add: cp_OclNot[symmetric] cp_OclOr[symmetric] )
lemma OclAnd1[simp]: "(invalid and true) = invalid"
by(rule ext,simp add: OclAnd_def null_def invalid_def true_def false_def bot_option_def)
lemma OclAnd2[simp]: "(invalid and false) = false"
by(rule ext,simp add: OclAnd_def null_def invalid_def true_def false_def bot_option_def)
lemma OclAnd3[simp]: "(invalid and null) = invalid"
by(rule ext,simp add: OclAnd_def null_def invalid_def true_def false_def bot_option_def
null_fun_def null_option_def)
lemma OclAnd4[simp]: "(invalid and invalid) = invalid"
by(rule ext,simp add: OclAnd_def null_def invalid_def true_def false_def bot_option_def)
lemma OclAnd5[simp]: "(null and true) = null"
by(rule ext,simp add: OclAnd_def null_def invalid_def true_def false_def bot_option_def
null_fun_def null_option_def)
lemma OclAnd6[simp]: "(null and false) = false"
by(rule ext,simp add: OclAnd_def null_def invalid_def true_def false_def bot_option_def
null_fun_def null_option_def)
lemma OclAnd7[simp]: "(null and null) = null"
by(rule ext,simp add: OclAnd_def null_def invalid_def true_def false_def bot_option_def
null_fun_def null_option_def)
lemma OclAnd8[simp]: "(null and invalid) = invalid"
by(rule ext,simp add: OclAnd_def null_def invalid_def true_def false_def bot_option_def
null_fun_def null_option_def)
lemma OclAnd9[simp]: "(false and true) = false"
by(rule ext,simp add: OclAnd_def null_def invalid_def true_def false_def)
lemma OclAnd10[simp]: "(false and false) = false"
by(rule ext,simp add: OclAnd_def null_def invalid_def true_def false_def)
lemma OclAnd11[simp]: "(false and null) = false"
by(rule ext,simp add: OclAnd_def null_def invalid_def true_def false_def)
lemma OclAnd12[simp]: "(false and invalid) = false"
by(rule ext,simp add: OclAnd_def null_def invalid_def true_def false_def)
lemma OclAnd13[simp]: "(true and true) = true"
by(rule ext,simp add: OclAnd_def null_def invalid_def true_def false_def)
lemma OclAnd14[simp]: "(true and false) = false"
by(rule ext,simp add: OclAnd_def null_def invalid_def true_def false_def)
lemma OclAnd15[simp]: "(true and null) = null"
by(rule ext,simp add: OclAnd_def null_def invalid_def true_def false_def bot_option_def
null_fun_def null_option_def)
lemma OclAnd16[simp]: "(true and invalid) = invalid"
by(rule ext,simp add: OclAnd_def null_def invalid_def true_def false_def bot_option_def
null_fun_def null_option_def)
lemma OclAnd_idem[simp]: "(X and X) = X"
apply(rule ext,simp add: OclAnd_def null_def invalid_def true_def false_def)
apply(case_tac "X x", simp_all)
apply(case_tac "a", simp_all)
apply(case_tac "aa", simp_all)
done
lemma OclAnd_commute: "(X and Y) = (Y and X)"
by(rule ext,auto simp:true_def false_def OclAnd_def invalid_def
split: option.split option.split_asm
bool.split bool.split_asm)
lemma OclAnd_false1[simp]: "(false and X) = false"
apply(rule ext, simp add: OclAnd_def)
apply(auto simp:true_def false_def invalid_def
split: option.split option.split_asm)
done
lemma OclAnd_false2[simp]: "(X and false) = false"
by(simp add: OclAnd_commute)
lemma OclAnd_true1[simp]: "(true and X) = X"
apply(rule ext, simp add: OclAnd_def)
apply(auto simp:true_def false_def invalid_def
split: option.split option.split_asm)
done
lemma OclAnd_true2[simp]: "(X and true) = X"
by(simp add: OclAnd_commute)
lemma OclAnd_bot1[simp]: "⋀τ. X τ ≠ false τ ⟹ (bot and X) τ = bot τ"
apply(simp add: OclAnd_def)
apply(auto simp:true_def false_def bot_fun_def bot_option_def
split: option.split option.split_asm)
done
lemma OclAnd_bot2[simp]: "⋀τ. X τ ≠ false τ ⟹ (X and bot) τ = bot τ"
by(simp add: OclAnd_commute)
lemma OclAnd_null1[simp]: "⋀τ. X τ ≠ false τ ⟹ X τ ≠ bot τ ⟹ (null and X) τ = null τ"
apply(simp add: OclAnd_def)
apply(auto simp:true_def false_def bot_fun_def bot_option_def null_fun_def null_option_def
split: option.split option.split_asm)
done
lemma OclAnd_null2[simp]: "⋀τ. X τ ≠ false τ ⟹ X τ ≠ bot τ ⟹ (X and null) τ = null τ"
by(simp add: OclAnd_commute)
lemma OclAnd_assoc: "(X and (Y and Z)) = (X and Y and Z)"
apply(rule ext, simp add: OclAnd_def)
apply(auto simp:true_def false_def null_def invalid_def
split: option.split option.split_asm
bool.split bool.split_asm)
done
lemma OclOr1[simp]: "(invalid or true) = true"
by(rule ext, simp add: OclOr_def OclNot_def OclAnd_def null_def invalid_def true_def false_def
bot_option_def)
lemma OclOr2[simp]: "(invalid or false) = invalid"
by(rule ext, simp add: OclOr_def OclNot_def OclAnd_def null_def invalid_def true_def false_def
bot_option_def)
lemma OclOr3[simp]: "(invalid or null) = invalid"
by(rule ext, simp add: OclOr_def OclNot_def OclAnd_def null_def invalid_def true_def false_def
bot_option_def null_fun_def null_option_def)
lemma OclOr4[simp]: "(invalid or invalid) = invalid"
by(rule ext, simp add: OclOr_def OclNot_def OclAnd_def null_def invalid_def true_def false_def
bot_option_def)
lemma OclOr5[simp]: "(null or true) = true"
by(rule ext, simp add: OclOr_def OclNot_def OclAnd_def null_def invalid_def true_def false_def
bot_option_def null_fun_def null_option_def)
lemma OclOr6[simp]: "(null or false) = null"
by(rule ext, simp add: OclOr_def OclNot_def OclAnd_def null_def invalid_def true_def false_def
bot_option_def null_fun_def null_option_def)
lemma OclOr7[simp]: "(null or null) = null"
by(rule ext, simp add: OclOr_def OclNot_def OclAnd_def null_def invalid_def true_def false_def
bot_option_def null_fun_def null_option_def)
lemma OclOr8[simp]: "(null or invalid) = invalid"
by(rule ext, simp add: OclOr_def OclNot_def OclAnd_def null_def invalid_def true_def false_def
bot_option_def null_fun_def null_option_def)
lemma OclOr_idem[simp]: "(X or X) = X"
by(simp add: OclOr_def)
lemma OclOr_commute: "(X or Y) = (Y or X)"
by(simp add: OclOr_def OclAnd_commute)
lemma OclOr_false1[simp]: "(false or Y) = Y"
by(simp add: OclOr_def)
lemma OclOr_false2[simp]: "(Y or false) = Y"
by(simp add: OclOr_def)
lemma OclOr_true1[simp]: "(true or Y) = true"
by(simp add: OclOr_def)
lemma OclOr_true2: "(Y or true) = true"
by(simp add: OclOr_def)
lemma OclOr_bot1[simp]: "⋀τ. X τ ≠ true τ ⟹ (bot or X) τ = bot τ"
apply(simp add: OclOr_def OclAnd_def OclNot_def)
apply(auto simp:true_def false_def bot_fun_def bot_option_def
split: option.split option.split_asm)
done
lemma OclOr_bot2[simp]: "⋀τ. X τ ≠ true τ ⟹ (X or bot) τ = bot τ"
by(simp add: OclOr_commute)
lemma OclOr_null1[simp]: "⋀τ. X τ ≠ true τ ⟹ X τ ≠ bot τ ⟹ (null or X) τ = null τ"
apply(simp add: OclOr_def OclAnd_def OclNot_def)
apply(auto simp:true_def false_def bot_fun_def bot_option_def null_fun_def null_option_def
split: option.split option.split_asm)
apply (metis (full_types) bool.simps(3) bot_option_def null_is_valid null_option_def)
by (metis (full_types) bool.simps(3) option.distinct(1) option.sel)
lemma OclOr_null2[simp]: "⋀τ. X τ ≠ true τ ⟹ X τ ≠ bot τ ⟹ (X or null) τ = null τ"
by(simp add: OclOr_commute)
lemma OclOr_assoc: "(X or (Y or Z)) = (X or Y or Z)"
by(simp add: OclOr_def OclAnd_assoc)
lemma deMorgan1: "not(X and Y) = ((not X) or (not Y))"
by(simp add: OclOr_def)
lemma deMorgan2: "not(X or Y) = ((not X) and (not Y))"
by(simp add: OclOr_def)
lemma OclImplies_true1[simp]:"(true implies X) = X"
by(simp add: OclImplies_def)
lemma OclImplies_true2[simp]: "(X implies true) = true"
by(simp add: OclImplies_def OclOr_true2)
lemma OclImplies_false1[simp]:"(false implies X) = true"
by(simp add: OclImplies_def)
subsection‹A Standard Logical Calculus for OCL›
definition OclValid :: "[('𝔄)st, ('𝔄)Boolean] ⇒ bool" (‹(1(_)/ ⊨ (_))› 50)
where "τ ⊨ P ≡ ((P τ) = true τ)"
syntax OclNonValid :: "[('𝔄)st, ('𝔄)Boolean] ⇒ bool" (‹(1(_)/ |≠ (_))› 50)
syntax_consts OclNonValid == Not
translations "τ |≠ P" == "¬(τ ⊨ P)"
subsubsection‹Global vs. Local Judgements›
lemma transform1: "P = true ⟹ τ ⊨ P"
by(simp add: OclValid_def)
lemma transform1_rev: "∀ τ. τ ⊨ P ⟹ P = true"
by(rule ext, auto simp: OclValid_def true_def)
lemma transform2: "(P = Q) ⟹ ((τ ⊨ P) = (τ ⊨ Q))"
by(auto simp: OclValid_def)
lemma transform2_rev: "∀ τ. (τ ⊨ δ P) ∧ (τ ⊨ δ Q) ∧ (τ ⊨ P) = (τ ⊨ Q) ⟹ P = Q"
apply(rule ext,auto simp: OclValid_def true_def defined_def)
apply(erule_tac x=a in allE)
apply(erule_tac x=b in allE)
apply(auto simp: false_def true_def defined_def bot_Boolean_def null_Boolean_def
split: option.split_asm HOL.if_split_asm)
done
text‹However, certain properties (like transitivity) can not
be \emph{transformed} from the global level to the local one,
they have to be re-proven on the local level.›
lemma
assumes H : "P = true ⟹ Q = true"
shows "τ ⊨ P ⟹ τ ⊨ Q"
apply(simp add: OclValid_def)
apply(rule H[THEN fun_cong])
apply(rule ext)
oops
subsubsection‹Local Validity and Meta-logic›
text‹\label{sec:localVal}›
lemma foundation1[simp]: "τ ⊨ true"
by(auto simp: OclValid_def)
lemma foundation2[simp]: "¬(τ ⊨ false)"
by(auto simp: OclValid_def true_def false_def)
lemma foundation3[simp]: "¬(τ ⊨ invalid)"
by(auto simp: OclValid_def true_def false_def invalid_def bot_option_def)
lemma foundation4[simp]: "¬(τ ⊨ null)"
by(auto simp: OclValid_def true_def false_def null_def null_fun_def null_option_def bot_option_def)
lemma bool_split[simp]:
"(τ ⊨ (x ≜ invalid)) ∨ (τ ⊨ (x ≜ null)) ∨ (τ ⊨ (x ≜ true)) ∨ (τ ⊨ (x ≜ false))"
apply(insert bool_split_0[of x τ], auto)
apply(simp_all add: OclValid_def StrongEq_def true_def null_def invalid_def)
done
lemma defined_split:
"(τ ⊨ δ x) = ((¬(τ ⊨ (x ≜ invalid))) ∧ (¬ (τ ⊨ (x ≜ null))))"
by(simp add:defined_def true_def false_def invalid_def null_def
StrongEq_def OclValid_def bot_fun_def null_fun_def)
lemma valid_bool_split: "(τ ⊨ υ A) = ((τ ⊨ A ≜ null) ∨ (τ ⊨ A) ∨ (τ ⊨ not A)) "
by(auto simp:valid_def true_def false_def invalid_def null_def OclNot_def
StrongEq_def OclValid_def bot_fun_def bot_option_def null_option_def null_fun_def)
lemma defined_bool_split: "(τ ⊨ δ A) = ((τ ⊨ A) ∨ (τ ⊨ not A))"
by(auto simp:defined_def true_def false_def invalid_def null_def OclNot_def
StrongEq_def OclValid_def bot_fun_def bot_option_def null_option_def null_fun_def)
lemma foundation5:
"τ ⊨ (P and Q) ⟹ (τ ⊨ P) ∧ (τ ⊨ Q)"
by(simp add: OclAnd_def OclValid_def true_def false_def defined_def
split: option.split option.split_asm bool.split bool.split_asm)
lemma foundation6:
"τ ⊨ P ⟹ τ ⊨ δ P"
by(simp add: OclNot_def OclValid_def true_def false_def defined_def
null_option_def null_fun_def bot_option_def bot_fun_def
split: option.split option.split_asm)
lemma foundation7[simp]:
"(τ ⊨ not (δ x)) = (¬ (τ ⊨ δ x))"
by(simp add: OclNot_def OclValid_def true_def false_def defined_def
split: option.split option.split_asm)
lemma foundation7'[simp]:
"(τ ⊨ not (υ x)) = (¬ (τ ⊨ υ x))"
by(simp add: OclNot_def OclValid_def true_def false_def valid_def
split: option.split option.split_asm)
text‹
Key theorem for the $\delta$-closure: either an expression is
defined, or it can be replaced (substituted via ‹StrongEq_L_subst2›;
see below) by ‹invalid› or ‹null›. Strictness-reduction rules will
usually reduce these substituted terms drastically.
›
lemma foundation8:
"(τ ⊨ δ x) ∨ (τ ⊨ (x ≜ invalid)) ∨ (τ ⊨ (x ≜ null))"
proof -
have 1 : "(τ ⊨ δ x) ∨ (¬(τ ⊨ δ x))" by auto
have 2 : "(¬(τ ⊨ δ x)) = ((τ ⊨ (x ≜ invalid)) ∨ (τ ⊨ (x ≜ null)))"
by(simp only: defined_split, simp)
show ?thesis by(insert 1, simp add:2)
qed
lemma foundation9:
"τ ⊨ δ x ⟹ (τ ⊨ not x) = (¬ (τ ⊨ x))"
apply(simp add: defined_split )
by(auto simp: OclNot_def null_fun_def null_option_def bot_option_def
OclValid_def invalid_def true_def null_def StrongEq_def)
lemma foundation9':
"τ ⊨ not x ⟹ ¬ (τ ⊨ x)"
by(auto simp: foundation6 foundation9)
lemma foundation9'':
" τ ⊨ not x ⟹ τ ⊨ δ x"
by(metis OclNot3 OclNot_not OclValid_def cp_OclNot cp_defined defined4)
lemma foundation10:
"τ ⊨ δ x ⟹ τ ⊨ δ y ⟹ (τ ⊨ (x and y)) = ( (τ ⊨ x) ∧ (τ ⊨ y))"
apply(simp add: defined_split)
by(auto simp: OclAnd_def OclValid_def invalid_def
true_def null_def StrongEq_def null_fun_def null_option_def bot_option_def
split:bool.split_asm)
lemma foundation10': "(τ ⊨ (A and B)) = ((τ ⊨ A) ∧ (τ ⊨ B))"
by(auto dest:foundation5 simp:foundation6 foundation10)
lemma foundation11:
"τ ⊨ δ x ⟹ τ ⊨ δ y ⟹ (τ ⊨ (x or y)) = ( (τ ⊨ x) ∨ (τ ⊨ y))"
apply(simp add: defined_split)
by(auto simp: OclNot_def OclOr_def OclAnd_def OclValid_def invalid_def
true_def null_def StrongEq_def null_fun_def null_option_def bot_option_def
split:bool.split_asm bool.split)
lemma foundation12:
"τ ⊨ δ x ⟹ (τ ⊨ (x implies y)) = ( (τ ⊨ x) ⟶ (τ ⊨ y))"
apply(simp add: defined_split)
by(auto simp: OclNot_def OclOr_def OclAnd_def OclImplies_def bot_option_def
OclValid_def invalid_def true_def null_def StrongEq_def null_fun_def null_option_def
split:bool.split_asm bool.split option.split_asm)
lemma foundation13:"(τ ⊨ A ≜ true) = (τ ⊨ A)"
by(auto simp: OclNot_def OclValid_def invalid_def true_def null_def StrongEq_def
split:bool.split_asm bool.split)
lemma foundation14:"(τ ⊨ A ≜ false) = (τ ⊨ not A)"
by(auto simp: OclNot_def OclValid_def invalid_def false_def true_def null_def StrongEq_def
split:bool.split_asm bool.split option.split)
lemma foundation15:"(τ ⊨ A ≜ invalid) = (τ ⊨ not(υ A))"
by(auto simp: OclNot_def OclValid_def valid_def invalid_def false_def true_def null_def
StrongEq_def bot_option_def null_fun_def null_option_def bot_option_def bot_fun_def
split:bool.split_asm bool.split option.split)
lemma foundation16: "τ ⊨ (δ X) = (X τ ≠ bot ∧ X τ ≠ null)"
by(auto simp: OclValid_def defined_def false_def true_def bot_fun_def null_fun_def
split:if_split_asm)
lemma foundation16'': "¬(τ ⊨ (δ X)) = ((τ ⊨ (X ≜ invalid)) ∨ (τ ⊨ (X ≜ null)))"
apply(simp add: foundation16)
by(auto simp:defined_def false_def true_def bot_fun_def null_fun_def OclValid_def StrongEq_def invalid_def)
lemma foundation16': "(τ ⊨ (δ X)) = (X τ ≠ invalid τ ∧ X τ ≠ null τ)"
apply(simp add:invalid_def null_def null_fun_def)
by(auto simp: OclValid_def defined_def false_def true_def bot_fun_def null_fun_def
split:if_split_asm)
lemma foundation18: "(τ ⊨ (υ X)) = (X τ ≠ invalid τ)"
by(auto simp: OclValid_def valid_def false_def true_def bot_fun_def invalid_def
split:if_split_asm)
lemma foundation18': "(τ ⊨ (υ X)) = (X τ ≠ bot)"
by(auto simp: OclValid_def valid_def false_def true_def bot_fun_def
split:if_split_asm)
lemma foundation18'': "(τ ⊨ (υ X) )= (¬(τ ⊨ (X ≜ invalid)))"
by(auto simp:foundation15)
lemma foundation20 : "τ ⊨ (δ X) ⟹ τ ⊨ υ X"
by(simp add: foundation18 foundation16 invalid_def)
lemma foundation21: "(not A ≜ not B) = (A ≜ B)"
by(rule ext, auto simp: OclNot_def StrongEq_def
split: bool.split_asm HOL.if_split_asm option.split)
lemma foundation22: "(τ ⊨ (X ≜ Y)) = (X τ = Y τ)"
by(auto simp: StrongEq_def OclValid_def true_def)
lemma foundation23: "(τ ⊨ P) = (τ ⊨ (λ _ . P τ))"
by(auto simp: OclValid_def true_def)
lemma foundation24:"(τ ⊨ not(X ≜ Y)) = (X τ ≠ Y τ)"
by(simp add: StrongEq_def OclValid_def OclNot_def true_def)
lemma foundation25: "τ ⊨ P ⟹ τ ⊨ (P or Q)"
by(simp add: OclOr_def OclNot_def OclAnd_def OclValid_def true_def)
lemma foundation25': "τ ⊨ Q ⟹ τ ⊨ (P or Q)"
by(subst OclOr_commute, simp add: foundation25)
lemma foundation26:
assumes defP: "τ ⊨ δ P"
assumes defQ: "τ ⊨ δ Q"
assumes H: "τ ⊨ (P or Q)"
assumes P: "τ ⊨ P ⟹ R"
assumes Q: "τ ⊨ Q ⟹ R"
shows "R"
by(insert H, subst (asm) foundation11[OF defP defQ], erule disjE, simp_all add: P Q)
lemma foundation27: "τ ⊨ A ⟹ (τ ⊨ A implies B) = (τ ⊨ B)"
by (simp add: foundation12 foundation6)
lemma defined_not_I : "τ ⊨ δ (x) ⟹ τ ⊨ δ (not x)"
by(auto simp: OclNot_def null_def invalid_def defined_def valid_def OclValid_def
true_def false_def bot_option_def null_option_def null_fun_def bot_fun_def
split: option.split_asm HOL.if_split_asm)
lemma valid_not_I : "τ ⊨ υ (x) ⟹ τ ⊨ υ (not x)"
by(auto simp: OclNot_def null_def invalid_def defined_def valid_def OclValid_def
true_def false_def bot_option_def null_option_def null_fun_def bot_fun_def
split: option.split_asm option.split HOL.if_split_asm)
lemma defined_and_I : "τ ⊨ δ (x) ⟹ τ ⊨ δ (y) ⟹ τ ⊨ δ (x and y)"
apply(simp add: OclAnd_def null_def invalid_def defined_def valid_def OclValid_def
true_def false_def bot_option_def null_option_def null_fun_def bot_fun_def
split: option.split_asm HOL.if_split_asm)
apply(auto simp: null_option_def split: bool.split)
by(case_tac "ya",simp_all)
lemma valid_and_I : "τ ⊨ υ (x) ⟹ τ ⊨ υ (y) ⟹ τ ⊨ υ (x and y)"
apply(simp add: OclAnd_def null_def invalid_def defined_def valid_def OclValid_def
true_def false_def bot_option_def null_option_def null_fun_def bot_fun_def
split: option.split_asm HOL.if_split_asm)
by(auto simp: null_option_def split: option.split bool.split)
lemma defined_or_I : "τ ⊨ δ (x) ⟹ τ ⊨ δ (y) ⟹ τ ⊨ δ (x or y)"
by(simp add: OclOr_def defined_and_I defined_not_I)
lemma valid_or_I : "τ ⊨ υ (x) ⟹ τ ⊨ υ (y) ⟹ τ ⊨ υ (x or y)"
by(simp add: OclOr_def valid_and_I valid_not_I)
subsubsection‹Local Judgements and Strong Equality›
lemma StrongEq_L_refl: "τ ⊨ (x ≜ x)"
by(simp add: OclValid_def StrongEq_def)
lemma StrongEq_L_sym: "τ ⊨ (x ≜ y) ⟹ τ ⊨ (y ≜ x)"
by(simp add: StrongEq_sym)
lemma StrongEq_L_trans: "τ ⊨ (x ≜ y) ⟹ τ ⊨ (y ≜ z) ⟹ τ ⊨ (x ≜ z)"
by(simp add: OclValid_def StrongEq_def true_def)
text‹In order to establish substitutivity (which does not
hold in general HOL formulas) we introduce the following
predicate that allows for a calculus of the necessary side-conditions.›
definition cp :: "(('𝔄,'α) val ⇒ ('𝔄,'β) val) ⇒ bool"
where "cp P ≡ (∃ f. ∀ X τ. P X τ = f (X τ) τ)"
text‹The rule of substitutivity in Featherweight OCL holds only
for context-passing expressions, \ie those that pass
the context ‹τ› without changing it. Fortunately, all
operators of the OCL language satisfy this property
(but not all HOL operators).›
lemma StrongEq_L_subst1: "⋀ τ. cp P ⟹ τ ⊨ (x ≜ y) ⟹ τ ⊨ (P x ≜ P y)"
by(auto simp: OclValid_def StrongEq_def true_def cp_def)
lemma StrongEq_L_subst2:
"⋀ τ. cp P ⟹ τ ⊨ (x ≜ y) ⟹ τ ⊨ (P x) ⟹ τ ⊨ (P y)"
by(auto simp: OclValid_def StrongEq_def true_def cp_def)
lemma StrongEq_L_subst2_rev: "τ ⊨ y ≜ x ⟹ cp P ⟹ τ ⊨ P x ⟹ τ ⊨ P y"
apply(erule StrongEq_L_subst2)
apply(erule StrongEq_L_sym)
by assumption
lemma StrongEq_L_subst3:
assumes cp: "cp P"
and eq: "τ ⊨ (x ≜ y)"
shows "(τ ⊨ P x) = (τ ⊨ P y)"
apply(rule iffI)
apply(rule StrongEq_L_subst2[OF cp,OF eq],simp)
apply(rule StrongEq_L_subst2[OF cp,OF eq[THEN StrongEq_L_sym]],simp)
done
lemma StrongEq_L_subst3_rev:
assumes eq: "τ ⊨ (x ≜ y)"
and cp: "cp P"
shows "(τ ⊨ P x) = (τ ⊨ P y)"
by(insert cp, erule StrongEq_L_subst3, rule eq)
lemma StrongEq_L_subst4_rev:
assumes eq: "τ ⊨ (x ≜ y)"
and cp: "cp P"
shows "(¬(τ ⊨ P x)) = (¬(τ ⊨ P y))"
thm arg_cong[of _ _ "Not"]
apply(rule arg_cong[of _ _ "Not"])
by(insert cp, erule StrongEq_L_subst3, rule eq)
lemma cpI1:
"(∀ X τ. f X τ = f(λ_. X τ) τ) ⟹ cp P ⟹ cp(λX. f (P X))"
apply(auto simp: true_def cp_def)
apply(rule exI, (rule allI)+)
by(erule_tac x="P X" in allE, auto)
lemma cpI2:
"(∀ X Y τ. f X Y τ = f(λ_. X τ)(λ_. Y τ) τ) ⟹
cp P ⟹ cp Q ⟹ cp(λX. f (P X) (Q X))"
apply(auto simp: true_def cp_def)
apply(rule exI, (rule allI)+)
by(erule_tac x="P X" in allE, auto)
lemma cpI3:
"(∀ X Y Z τ. f X Y Z τ = f(λ_. X τ)(λ_. Y τ)(λ_. Z τ) τ) ⟹
cp P ⟹ cp Q ⟹ cp R ⟹ cp(λX. f (P X) (Q X) (R X))"
apply(auto simp: cp_def)
apply(rule exI, (rule allI)+)
by(erule_tac x="P X" in allE, auto)
lemma cpI4:
"(∀ W X Y Z τ. f W X Y Z τ = f(λ_. W τ)(λ_. X τ)(λ_. Y τ)(λ_. Z τ) τ) ⟹
cp P ⟹ cp Q ⟹ cp R ⟹ cp S ⟹ cp(λX. f (P X) (Q X) (R X) (S X))"
apply(auto simp: cp_def)
apply(rule exI, (rule allI)+)
by(erule_tac x="P X" in allE, auto)
lemma cpI5:
"(∀ V W X Y Z τ. f V W X Y Z τ = f(λ_. V τ) (λ_. W τ)(λ_. X τ)(λ_. Y τ)(λ_. Z τ) τ) ⟹
cp N ⟹ cp P ⟹ cp Q ⟹ cp R ⟹ cp S ⟹ cp(λX. f (N X) (P X) (Q X) (R X) (S X))"
apply(auto simp: cp_def)
apply(rule exI, (rule allI)+)
by(erule_tac x="N X" in allE, auto)
lemma cp_const : "cp(λ_. c)"
by (simp add: cp_def, fast)
lemma cp_id : "cp(λX. X)"
by (simp add: cp_def, fast)
text_raw‹\isatagafp›
lemmas cp_intro[intro!,simp,code_unfold] =
cp_const
cp_id
cp_defined[THEN allI[THEN allI[THEN cpI1], of defined]]
cp_valid[THEN allI[THEN allI[THEN cpI1], of valid]]
cp_OclNot[THEN allI[THEN allI[THEN cpI1], of not]]
cp_OclAnd[THEN allI[THEN allI[THEN allI[THEN cpI2]], of "(and)"]]
cp_OclOr[THEN allI[THEN allI[THEN allI[THEN cpI2]], of "(or)"]]
cp_OclImplies[THEN allI[THEN allI[THEN allI[THEN cpI2]], of "(implies)"]]
cp_StrongEq[THEN allI[THEN allI[THEN allI[THEN cpI2]],
of "StrongEq"]]
text_raw‹\endisatagafp›
subsection‹OCL's if then else endif›
definition OclIf :: "[('𝔄)Boolean , ('𝔄,'α::null) val, ('𝔄,'α) val] ⇒ ('𝔄,'α) val"
(‹if (_) then (_) else (_) endif› [10,10,10]50)
where "(if C then B⇩1 else B⇩2 endif) = (λ τ. if (δ C) τ = true τ
then (if (C τ) = true τ
then B⇩1 τ
else B⇩2 τ)
else invalid τ)"
lemma cp_OclIf:"((if C then B⇩1 else B⇩2 endif) τ =
(if (λ _. C τ) then (λ _. B⇩1 τ) else (λ _. B⇩2 τ) endif) τ)"
by(simp only: OclIf_def, subst cp_defined, rule refl)
text_raw‹\isatagafp›
lemmas cp_intro'[intro!,simp,code_unfold] =
cp_intro
cp_OclIf[THEN allI[THEN allI[THEN allI[THEN allI[THEN cpI3]]], of "OclIf"]]
text_raw‹\endisatagafp›
lemma OclIf_invalid [simp]: "(if invalid then B⇩1 else B⇩2 endif) = invalid"
by(rule ext, auto simp: OclIf_def)
lemma OclIf_null [simp]: "(if null then B⇩1 else B⇩2 endif) = invalid"
by(rule ext, auto simp: OclIf_def)
lemma OclIf_true [simp]: "(if true then B⇩1 else B⇩2 endif) = B⇩1"
by(rule ext, auto simp: OclIf_def)
lemma OclIf_true' [simp]: "τ ⊨ P ⟹ (if P then B⇩1 else B⇩2 endif)τ = B⇩1 τ"
apply(subst cp_OclIf,auto simp: OclValid_def)
by(simp add:cp_OclIf[symmetric])
lemma OclIf_true'' [simp]: "τ ⊨ P ⟹ τ ⊨ (if P then B⇩1 else B⇩2 endif) ≜ B⇩1"
by(subst OclValid_def, simp add: StrongEq_def true_def)
lemma OclIf_false [simp]: "(if false then B⇩1 else B⇩2 endif) = B⇩2"
by(rule ext, auto simp: OclIf_def)
lemma OclIf_false' [simp]: "τ ⊨ not P ⟹ (if P then B⇩1 else B⇩2 endif)τ = B⇩2 τ"
apply(subst cp_OclIf)
apply(auto simp: foundation14[symmetric] foundation22)
by(auto simp: cp_OclIf[symmetric])
lemma OclIf_idem1[simp]:"(if δ X then A else A endif) = A"
by(rule ext, auto simp: OclIf_def)
lemma OclIf_idem2[simp]:"(if υ X then A else A endif) = A"
by(rule ext, auto simp: OclIf_def)
lemma OclNot_if[simp]:
"not(if P then C else E endif) = (if P then not C else not E endif)"
apply(rule OclNot_inject, simp)
apply(rule ext)
apply(subst cp_OclNot, simp add: OclIf_def)
apply(subst cp_OclNot[symmetric])+
by simp
subsection‹Fundamental Predicates on Basic Types: Strict (Referential) Equality›
text‹
In contrast to logical equality, the OCL standard defines an equality operation
which we call ``strict referential equality''. It behaves differently for all
types---on value types, it is basically a strict version of strong equality,
for defined values it behaves identical. But on object types it will compare
their references within the store. We introduce strict referential equality
as an \emph{overloaded} concept and will handle it for
each type instance individually.
›
consts StrictRefEq :: "[('𝔄,'a)val,('𝔄,'a)val] ⇒ ('𝔄)Boolean" (infixl ‹≐› 30)
text‹with {term "not"} we can express the notation:›
syntax
"notequal" :: "('𝔄)Boolean ⇒ ('𝔄)Boolean ⇒ ('𝔄)Boolean" (infix ‹<>› 40)
syntax_consts
notequal == OclNot
translations
"a <> b" == "CONST OclNot(a ≐ b)"
text‹We will define instances of this equality in a case-by-case basis.›
subsection‹Laws to Establish Definedness (\texorpdfstring{$\delta$}{d}-closure)›
text‹For the logical connectives, we have --- beyond
@{thm foundation6} --- the following facts:›
lemma OclNot_defargs:
"τ ⊨ (not P) ⟹ τ ⊨ δ P"
by(auto simp: OclNot_def OclValid_def true_def invalid_def defined_def false_def
bot_fun_def bot_option_def null_fun_def null_option_def
split: bool.split_asm HOL.if_split_asm option.split option.split_asm)
lemma OclNot_contrapos_nn:
assumes A: "τ ⊨ δ A"
assumes B: "τ ⊨ not B"
assumes C: "τ ⊨ A ⟹ τ ⊨ B"
shows "τ ⊨ not A"
proof -
have D : "τ ⊨ δ B" by(rule B[THEN OclNot_defargs])
show ?thesis
apply(insert B,simp add: A D foundation9)
by(erule contrapos_nn, auto intro: C)
qed
subsection‹A Side-calculus for Constant Terms›
definition "const X ≡ ∀ τ τ'. X τ = X τ'"
lemma const_charn: "const X ⟹ X τ = X τ'"
by(auto simp: const_def)
lemma const_subst:
assumes const_X: "const X"
and const_Y: "const Y"
and eq : "X τ = Y τ"
and cp_P: "cp P"
and pp : "P Y τ = P Y τ'"
shows "P X τ = P X τ'"
proof -
have A: "⋀Y. P Y τ = P (λ_. Y τ) τ"
apply(insert cp_P, unfold cp_def)
apply(elim exE, erule_tac x=Y in allE', erule_tac x=τ in allE)
apply(erule_tac x="(λ_. Y τ)" in allE, erule_tac x=τ in allE)
by simp
have B: "⋀Y. P Y τ' = P (λ_. Y τ') τ'"
apply(insert cp_P, unfold cp_def)
apply(elim exE, erule_tac x=Y in allE', erule_tac x=τ' in allE)
apply(erule_tac x="(λ_. Y τ')" in allE, erule_tac x=τ' in allE)
by simp
have C: "X τ' = Y τ'"
apply(rule trans, subst const_charn[OF const_X],rule eq)
by(rule const_charn[OF const_Y])
show ?thesis
apply(subst A, subst B, simp add: eq C)
apply(subst A[symmetric],subst B[symmetric])
by(simp add:pp)
qed
lemma const_imply2 :
assumes "⋀τ τ'. P τ = P τ' ⟹ Q τ = Q τ'"
shows "const P ⟹ const Q"
by(simp add: const_def, insert assms, blast)
lemma const_imply3 :
assumes "⋀τ τ'. P τ = P τ' ⟹ Q τ = Q τ' ⟹ R τ = R τ'"
shows "const P ⟹ const Q ⟹ const R"
by(simp add: const_def, insert assms, blast)
lemma const_imply4 :
assumes "⋀τ τ'. P τ = P τ' ⟹ Q τ = Q τ' ⟹ R τ = R τ' ⟹ S τ = S τ'"
shows "const P ⟹ const Q ⟹ const R ⟹ const S"
by(simp add: const_def, insert assms, blast)
lemma const_lam : "const (λ_. e)"
by(simp add: const_def)
lemma const_true[simp] : "const true"
by(simp add: const_def true_def)
lemma const_false[simp] : "const false"
by(simp add: const_def false_def)
lemma const_null[simp] : "const null"
by(simp add: const_def null_fun_def)
lemma const_invalid [simp]: "const invalid"
by(simp add: const_def invalid_def)
lemma const_bot[simp] : "const bot"
by(simp add: const_def bot_fun_def)
lemma const_defined :
assumes "const X"
shows "const (δ X)"
by(rule const_imply2[OF _ assms],
simp add: defined_def false_def true_def bot_fun_def bot_option_def null_fun_def null_option_def)
lemma const_valid :
assumes "const X"
shows "const (υ X)"
by(rule const_imply2[OF _ assms],
simp add: valid_def false_def true_def bot_fun_def null_fun_def assms)
lemma const_OclAnd :
assumes "const X"
assumes "const X'"
shows "const (X and X')"
by(rule const_imply3[OF _ assms], subst (1 2) cp_OclAnd, simp add: assms OclAnd_def)
lemma const_OclNot :
assumes "const X"
shows "const (not X)"
by(rule const_imply2[OF _ assms],subst cp_OclNot,simp add: assms OclNot_def)
lemma const_OclOr :
assumes "const X"
assumes "const X'"
shows "const (X or X')"
by(simp add: assms OclOr_def const_OclNot const_OclAnd)
lemma const_OclImplies :
assumes "const X"
assumes "const X'"
shows "const (X implies X')"
by(simp add: assms OclImplies_def const_OclNot const_OclOr)
lemma const_StrongEq:
assumes "const X"
assumes "const X'"
shows "const(X ≜ X')"
apply(simp only: StrongEq_def const_def, intro allI)
apply(subst assms(1)[THEN const_charn])
apply(subst assms(2)[THEN const_charn])
by simp
lemma const_OclIf :
assumes "const B"
and "const C1"
and "const C2"
shows "const (if B then C1 else C2 endif)"
apply(rule const_imply4[OF _ assms],
subst (1 2) cp_OclIf, simp only: OclIf_def cp_defined[symmetric])
apply(simp add: const_defined[OF assms(1), simplified const_def, THEN spec, THEN spec]
const_true[simplified const_def, THEN spec, THEN spec]
assms[simplified const_def, THEN spec, THEN spec]
const_invalid[simplified const_def, THEN spec, THEN spec])
by (metis (no_types) bot_fun_def OclValid_def const_def const_true defined_def
foundation16[THEN iffD1] null_fun_def)
lemma const_OclValid1:
assumes "const x"
shows "(τ ⊨ δ x) = (τ' ⊨ δ x)"
apply(simp add: OclValid_def)
apply(subst const_defined[OF assms, THEN const_charn])
by(simp add: true_def)
lemma const_OclValid2:
assumes "const x"
shows "(τ ⊨ υ x) = (τ' ⊨ υ x)"
apply(simp add: OclValid_def)
apply(subst const_valid[OF assms, THEN const_charn])
by(simp add: true_def)
lemma const_HOL_if : "const C ⟹ const D ⟹ const F ⟹ const (λτ. if C τ then D τ else F τ)"
by(auto simp: const_def)
lemma const_HOL_and: "const C ⟹ const D ⟹ const (λτ. C τ ∧ D τ)"
by(auto simp: const_def)
lemma const_HOL_eq : "const C ⟹ const D ⟹ const (λτ. C τ = D τ)"
apply(auto simp: const_def)
apply(erule_tac x=τ in allE)
apply(erule_tac x=τ in allE)
apply(erule_tac x=τ' in allE)
apply(erule_tac x=τ' in allE)
apply simp
apply(erule_tac x=τ in allE)
apply(erule_tac x=τ in allE)
apply(erule_tac x=τ' in allE)
apply(erule_tac x=τ' in allE)
by simp
lemmas const_ss = const_bot const_null const_invalid const_false const_true const_lam
const_defined const_valid const_StrongEq const_OclNot const_OclAnd
const_OclOr const_OclImplies const_OclIf
const_HOL_if const_HOL_and const_HOL_eq
text‹Miscellaneous: Overloading the syntax of ``bottom''›
notation bot (‹⊥›)
end