Theory UML_Set
theory UML_Set
imports "../basic_types/UML_Void"
"../basic_types/UML_Boolean"
"../basic_types/UML_Integer"
"../basic_types/UML_String"
"../basic_types/UML_Real"
begin
no_notation None ("⊥")
section‹Collection Type Set: Operations \label{formal-set}›
subsection‹As a Motivation for the (infinite) Type Construction: Type-Extensions as Sets
\label{sec:type-extensions}›
text‹Our notion of typed set goes beyond the usual notion of a finite executable set and
is powerful enough to capture \emph{the extension of a type} in UML and OCL. This means
we can have in Featherweight OCL Sets containing all possible elements of a type, not only
those (finite) ones representable in a state. This holds for base types as well as class types,
although the notion for class-types --- involving object id's not occurring in a state ---
requires some care.
In a world with @{term invalid} and @{term null}, there are two notions extensions possible:
\begin{enumerate}
\item the set of all \emph{defined} values of a type @{term T}
(for which we will introduce the constant @{term T})
\item the set of all \emph{valid} values of a type @{term T}, so including @{term null}
(for which we will introduce the constant @{term T⇩n⇩u⇩l⇩l}).
\end{enumerate}
›
text‹We define the set extensions for the base type @{term Integer} as follows:›
definition Integer :: "('𝔄,Integer⇩b⇩a⇩s⇩e) Set"
where "Integer ≡ (λ τ. (Abs_Set⇩b⇩a⇩s⇩e o Some o Some) ((Some o Some) ` (UNIV::int set)))"
definition Integer⇩n⇩u⇩l⇩l :: "('𝔄,Integer⇩b⇩a⇩s⇩e) Set"
where "Integer⇩n⇩u⇩l⇩l ≡ (λ τ. (Abs_Set⇩b⇩a⇩s⇩e o Some o Some) (Some ` (UNIV::int option set)))"
lemma Integer_defined : "δ Integer = true"
apply(rule ext, auto simp: Integer_def defined_def false_def true_def
bot_fun_def null_fun_def null_option_def)
by(simp_all add: Abs_Set⇩b⇩a⇩s⇩e_inject bot_option_def bot_Set⇩b⇩a⇩s⇩e_def null_Set⇩b⇩a⇩s⇩e_def null_option_def)
lemma Integer⇩n⇩u⇩l⇩l_defined : "δ Integer⇩n⇩u⇩l⇩l = true"
apply(rule ext, auto simp: Integer⇩n⇩u⇩l⇩l_def defined_def false_def true_def
bot_fun_def null_fun_def null_option_def)
by(simp_all add: Abs_Set⇩b⇩a⇩s⇩e_inject bot_option_def bot_Set⇩b⇩a⇩s⇩e_def null_Set⇩b⇩a⇩s⇩e_def null_option_def)
text‹This allows the theorems:
‹τ ⊨ δ x ⟹ τ ⊨ (Integer->includes⇩S⇩e⇩t(x))›
‹τ ⊨ δ x ⟹ τ ⊨ Integer ≜ (Integer->including⇩S⇩e⇩t(x))›
and
‹τ ⊨ υ x ⟹ τ ⊨ (Integer⇩n⇩u⇩l⇩l->includes⇩S⇩e⇩t(x))›
‹τ ⊨ υ x ⟹ τ ⊨ Integer⇩n⇩u⇩l⇩l ≜ (Integer⇩n⇩u⇩l⇩l->including⇩S⇩e⇩t(x))›
which characterize the infiniteness of these sets by a recursive property on these sets.
›
text‹In the same spirit, we proceed similarly for the remaining base types:›
definition Void⇩n⇩u⇩l⇩l :: "('𝔄,Void⇩b⇩a⇩s⇩e) Set"
where "Void⇩n⇩u⇩l⇩l ≡ (λ τ. (Abs_Set⇩b⇩a⇩s⇩e o Some o Some) {Abs_Void⇩b⇩a⇩s⇩e (Some None)})"
definition Void⇩e⇩m⇩p⇩t⇩y :: "('𝔄,Void⇩b⇩a⇩s⇩e) Set"
where "Void⇩e⇩m⇩p⇩t⇩y ≡ (λ τ. (Abs_Set⇩b⇩a⇩s⇩e o Some o Some) {})"
lemma Void⇩n⇩u⇩l⇩l_defined : "δ Void⇩n⇩u⇩l⇩l = true"
apply(rule ext, auto simp: Void⇩n⇩u⇩l⇩l_def defined_def false_def true_def
bot_fun_def null_fun_def null_option_def
bot_Set⇩b⇩a⇩s⇩e_def null_Set⇩b⇩a⇩s⇩e_def)
by((subst (asm) Abs_Set⇩b⇩a⇩s⇩e_inject, auto simp add: bot_option_def null_option_def bot_Void_def),
(subst (asm) Abs_Void⇩b⇩a⇩s⇩e_inject, auto simp add: bot_option_def null_option_def))+
lemma Void⇩e⇩m⇩p⇩t⇩y_defined : "δ Void⇩e⇩m⇩p⇩t⇩y = true"
apply(rule ext, auto simp: Void⇩e⇩m⇩p⇩t⇩y_def defined_def false_def true_def
bot_fun_def null_fun_def null_option_def
bot_Set⇩b⇩a⇩s⇩e_def null_Set⇩b⇩a⇩s⇩e_def)
by((subst (asm) Abs_Set⇩b⇩a⇩s⇩e_inject, auto simp add: bot_option_def null_option_def bot_Void_def))+
lemma assumes "τ ⊨ δ (V :: ('𝔄,Void⇩b⇩a⇩s⇩e) Set)"
shows "τ ⊨ V ≜ Void⇩n⇩u⇩l⇩l ∨ τ ⊨ V ≜ Void⇩e⇩m⇩p⇩t⇩y"
proof -
have A:"⋀x y. x ≠ {} ⟹ ∃y. y∈ x"
by (metis all_not_in_conv)
show "?thesis"
apply(case_tac "V τ")
proof - fix y show "V τ = Abs_Set⇩b⇩a⇩s⇩e y ⟹
y ∈ {X. X = ⊥ ∨ X = null ∨ (∀x∈⌈⌈X⌉⌉. x ≠ ⊥)} ⟹
τ ⊨ V ≜ Void⇩n⇩u⇩l⇩l ∨ τ ⊨ V ≜ Void⇩e⇩m⇩p⇩t⇩y"
apply(insert assms, case_tac y, simp add: bot_option_def, simp add: bot_Set⇩b⇩a⇩s⇩e_def foundation16)
apply(simp add: bot_option_def null_option_def)
apply(erule disjE, metis OclValid_def defined_def foundation2 null_Set⇩b⇩a⇩s⇩e_def null_fun_def true_def)
proof - fix a show "V τ = Abs_Set⇩b⇩a⇩s⇩e ⌊a⌋ ⟹ ∀x∈⌈a⌉. x ≠ ⊥ ⟹ τ ⊨ V ≜ Void⇩n⇩u⇩l⇩l ∨ τ ⊨ V ≜ Void⇩e⇩m⇩p⇩t⇩y"
apply(case_tac a, simp, insert assms, metis OclValid_def foundation16 null_Set⇩b⇩a⇩s⇩e_def true_def)
apply(simp)
proof - fix aa show " V τ = Abs_Set⇩b⇩a⇩s⇩e ⌊⌊aa⌋⌋ ⟹ ∀x∈aa. x ≠ ⊥ ⟹ τ ⊨ V ≜ Void⇩n⇩u⇩l⇩l ∨ τ ⊨ V ≜ Void⇩e⇩m⇩p⇩t⇩y"
apply(case_tac "aa = {}",
rule disjI2,
insert assms,
simp add: Void⇩e⇩m⇩p⇩t⇩y_def OclValid_def StrongEq_def true_def,
rule disjI1)
apply(subgoal_tac "aa = {Abs_Void⇩b⇩a⇩s⇩e ⌊None⌋}", simp add: StrongEq_def OclValid_def true_def Void⇩n⇩u⇩l⇩l_def)
apply(drule A, erule exE)
proof - fix y show "V τ = Abs_Set⇩b⇩a⇩s⇩e ⌊⌊aa⌋⌋ ⟹
∀x∈aa. x ≠ ⊥ ⟹
τ ⊨ δ V ⟹
y ∈ aa ⟹
aa = {Abs_Void⇩b⇩a⇩s⇩e ⌊None⌋}"
apply(rule equalityI, rule subsetI, simp)
proof - fix x show " V τ = Abs_Set⇩b⇩a⇩s⇩e ⌊⌊aa⌋⌋ ⟹
∀x∈aa. x ≠ ⊥ ⟹ τ ⊨ δ V ⟹ y ∈ aa ⟹ x ∈ aa ⟹ x = Abs_Void⇩b⇩a⇩s⇩e ⌊None⌋"
apply(case_tac x, simp)
by (metis bot_Void_def bot_option_def null_option_def)
apply_end(simp_all)
apply_end(erule ballE[where x = y], simp_all)
apply_end(case_tac y,
simp add: bot_option_def null_option_def OclValid_def defined_def split: if_split_asm,
simp add: false_def true_def)
qed (erule disjE, simp add: bot_Void_def, simp)
qed qed qed qed qed
definition Boolean :: "('𝔄,Boolean⇩b⇩a⇩s⇩e) Set"
where "Boolean ≡ (λ τ. (Abs_Set⇩b⇩a⇩s⇩e o Some o Some) ((Some o Some) ` (UNIV::bool set)))"
definition Boolean⇩n⇩u⇩l⇩l :: "('𝔄,Boolean⇩b⇩a⇩s⇩e) Set"
where "Boolean⇩n⇩u⇩l⇩l ≡ (λ τ. (Abs_Set⇩b⇩a⇩s⇩e o Some o Some) (Some ` (UNIV::bool option set)))"
lemma Boolean_defined : "δ Boolean = true"
apply(rule ext, auto simp: Boolean_def defined_def false_def true_def
bot_fun_def null_fun_def null_option_def)
by(simp_all add: Abs_Set⇩b⇩a⇩s⇩e_inject bot_option_def bot_Set⇩b⇩a⇩s⇩e_def null_Set⇩b⇩a⇩s⇩e_def null_option_def)
lemma Boolean⇩n⇩u⇩l⇩l_defined : "δ Boolean⇩n⇩u⇩l⇩l = true"
apply(rule ext, auto simp: Boolean⇩n⇩u⇩l⇩l_def defined_def false_def true_def
bot_fun_def null_fun_def null_option_def)
by(simp_all add: Abs_Set⇩b⇩a⇩s⇩e_inject bot_option_def bot_Set⇩b⇩a⇩s⇩e_def null_Set⇩b⇩a⇩s⇩e_def null_option_def)
definition String :: "('𝔄,String⇩b⇩a⇩s⇩e) Set"
where "String ≡ (λ τ. (Abs_Set⇩b⇩a⇩s⇩e o Some o Some) ((Some o Some) ` (UNIV::string set)))"
definition String⇩n⇩u⇩l⇩l :: "('𝔄,String⇩b⇩a⇩s⇩e) Set"
where "String⇩n⇩u⇩l⇩l ≡ (λ τ. (Abs_Set⇩b⇩a⇩s⇩e o Some o Some) (Some ` (UNIV::string option set)))"
lemma String_defined : "δ String = true"
apply(rule ext, auto simp: String_def defined_def false_def true_def
bot_fun_def null_fun_def null_option_def)
by(simp_all add: Abs_Set⇩b⇩a⇩s⇩e_inject bot_option_def bot_Set⇩b⇩a⇩s⇩e_def null_Set⇩b⇩a⇩s⇩e_def null_option_def)
lemma String⇩n⇩u⇩l⇩l_defined : "δ String⇩n⇩u⇩l⇩l = true"
apply(rule ext, auto simp: String⇩n⇩u⇩l⇩l_def defined_def false_def true_def
bot_fun_def null_fun_def null_option_def)
by(simp_all add: Abs_Set⇩b⇩a⇩s⇩e_inject bot_option_def bot_Set⇩b⇩a⇩s⇩e_def null_Set⇩b⇩a⇩s⇩e_def null_option_def)
definition Real :: "('𝔄,Real⇩b⇩a⇩s⇩e) Set"
where "Real ≡ (λ τ. (Abs_Set⇩b⇩a⇩s⇩e o Some o Some) ((Some o Some) ` (UNIV::real set)))"
definition Real⇩n⇩u⇩l⇩l :: "('𝔄,Real⇩b⇩a⇩s⇩e) Set"
where "Real⇩n⇩u⇩l⇩l ≡ (λ τ. (Abs_Set⇩b⇩a⇩s⇩e o Some o Some) (Some ` (UNIV::real option set)))"
lemma Real_defined : "δ Real = true"
apply(rule ext, auto simp: Real_def defined_def false_def true_def
bot_fun_def null_fun_def null_option_def)
by(simp_all add: Abs_Set⇩b⇩a⇩s⇩e_inject bot_option_def bot_Set⇩b⇩a⇩s⇩e_def null_Set⇩b⇩a⇩s⇩e_def null_option_def)
lemma Real⇩n⇩u⇩l⇩l_defined : "δ Real⇩n⇩u⇩l⇩l = true"
apply(rule ext, auto simp: Real⇩n⇩u⇩l⇩l_def defined_def false_def true_def
bot_fun_def null_fun_def null_option_def)
by(simp_all add: Abs_Set⇩b⇩a⇩s⇩e_inject bot_option_def bot_Set⇩b⇩a⇩s⇩e_def null_Set⇩b⇩a⇩s⇩e_def null_option_def)
subsection‹Basic Properties of the Set Type›
text‹Every element in a defined set is valid.›
lemma Set_inv_lemma: "τ ⊨ (δ X) ⟹ ∀x∈⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X τ)⌉⌉. x ≠ bot"
apply(insert Rep_Set⇩b⇩a⇩s⇩e [of "X τ"], simp)
apply(auto simp: OclValid_def defined_def false_def true_def cp_def
bot_fun_def bot_Set⇩b⇩a⇩s⇩e_def null_Set⇩b⇩a⇩s⇩e_def null_fun_def
split:if_split_asm)
apply(erule contrapos_pp [of "Rep_Set⇩b⇩a⇩s⇩e (X τ) = bot"])
apply(subst Abs_Set⇩b⇩a⇩s⇩e_inject[symmetric], rule Rep_Set⇩b⇩a⇩s⇩e, simp)
apply(simp add: Rep_Set⇩b⇩a⇩s⇩e_inverse bot_Set⇩b⇩a⇩s⇩e_def bot_option_def)
apply(erule contrapos_pp [of "Rep_Set⇩b⇩a⇩s⇩e (X τ) = null"])
apply(subst Abs_Set⇩b⇩a⇩s⇩e_inject[symmetric], rule Rep_Set⇩b⇩a⇩s⇩e, simp)
apply(simp add: Rep_Set⇩b⇩a⇩s⇩e_inverse null_option_def)
by (simp add: bot_option_def)
lemma Set_inv_lemma' :
assumes x_def : "τ ⊨ δ X"
and e_mem : "e ∈ ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X τ)⌉⌉"
shows "τ ⊨ υ (λ_. e)"
apply(rule Set_inv_lemma[OF x_def, THEN ballE[where x = e]])
apply(simp add: foundation18')
by(simp add: e_mem)
lemma abs_rep_simp' :
assumes S_all_def : "τ ⊨ δ S"
shows "Abs_Set⇩b⇩a⇩s⇩e ⌊⌊⌈⌈Rep_Set⇩b⇩a⇩s⇩e (S τ)⌉⌉⌋⌋ = S τ"
proof -
have discr_eq_false_true : "⋀τ. (false τ = true τ) = False" by(simp add: false_def true_def)
show ?thesis
apply(insert S_all_def, simp add: OclValid_def defined_def)
apply(rule mp[OF Abs_Set⇩b⇩a⇩s⇩e_induct[where P = "λS. (if S = ⊥ τ ∨ S = null τ
then false τ else true τ) = true τ ⟶
Abs_Set⇩b⇩a⇩s⇩e ⌊⌊⌈⌈Rep_Set⇩b⇩a⇩s⇩e S⌉⌉⌋⌋ = S"]],
rename_tac S')
apply(simp add: Abs_Set⇩b⇩a⇩s⇩e_inverse discr_eq_false_true)
apply(case_tac S') apply(simp add: bot_fun_def bot_Set⇩b⇩a⇩s⇩e_def)+
apply(rename_tac S'', case_tac S'') apply(simp add: null_fun_def null_Set⇩b⇩a⇩s⇩e_def)+
done
qed
lemma S_lift' :
assumes S_all_def : "(τ :: '𝔄 st) ⊨ δ S"
shows "∃S'. (λa (_::'𝔄 st). a) ` ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (S τ)⌉⌉ = (λa (_::'𝔄 st). ⌊a⌋) ` S'"
apply(rule_tac x = "(λa. ⌈a⌉) ` ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (S τ)⌉⌉" in exI)
apply(simp only: image_comp)
apply(simp add: comp_def)
apply(rule image_cong, fast)
apply(drule Set_inv_lemma'[OF S_all_def])
by(case_tac x, (simp add: bot_option_def foundation18')+)
lemma invalid_set_OclNot_defined [simp,code_unfold]:"δ(invalid::('𝔄,'α::null) Set) = false" by simp
lemma null_set_OclNot_defined [simp,code_unfold]:"δ(null::('𝔄,'α::null) Set) = false"
by(simp add: defined_def null_fun_def)
lemma invalid_set_valid [simp,code_unfold]:"υ(invalid::('𝔄,'α::null) Set) = false"
by simp
lemma null_set_valid [simp,code_unfold]:"υ(null::('𝔄,'α::null) Set) = true"
apply(simp add: valid_def null_fun_def bot_fun_def bot_Set⇩b⇩a⇩s⇩e_def null_Set⇩b⇩a⇩s⇩e_def)
apply(subst Abs_Set⇩b⇩a⇩s⇩e_inject,simp_all add: null_option_def bot_option_def)
done
text‹... which means that we can have a type ‹('𝔄,('𝔄,('𝔄) Integer) Set) Set›
corresponding exactly to Set(Set(Integer)) in OCL notation. Note that the parameter
‹'𝔄› still refers to the object universe; making the OCL semantics entirely parametric
in the object universe makes it possible to study (and prove) its properties
independently from a concrete class diagram.›
subsection‹Definition: Strict Equality \label{sec:set-strict-equality}›
text‹After the part of foundational operations on sets, we detail here equality on sets.
Strong equality is inherited from the OCL core, but we have to consider
the case of the strict equality. We decide to overload strict equality in the
same way we do for other value's in OCL:›
overloading
StrictRefEq ≡ "StrictRefEq :: [('𝔄,'α::null)Set,('𝔄,'α::null)Set] ⇒ ('𝔄)Boolean"
begin
definition StrictRefEq⇩S⇩e⇩t :
"(x::('𝔄,'α::null)Set) ≐ y ≡ λ τ. if (υ x) τ = true τ ∧ (υ y) τ = true τ
then (x ≜ y)τ
else invalid τ"
end
text‹One might object here that for the case of objects, this is an empty definition.
The answer is no, we will restrain later on states and objects such that any object
has its oid stored inside the object (so the ref, under which an object can be referenced
in the store will represented in the object itself). For such well-formed stores that satisfy
this invariant (the WFF-invariant), the referential equality and the
strong equality---and therefore the strict equality on sets in the sense above---coincides.›
text‹Property proof in terms of @{term "profile_bin⇩S⇩t⇩r⇩o⇩n⇩g⇩E⇩q_⇩v_⇩v"}›
interpretation StrictRefEq⇩S⇩e⇩t : profile_bin⇩S⇩t⇩r⇩o⇩n⇩g⇩E⇩q_⇩v_⇩v "λ x y. (x::('𝔄,'α::null)Set) ≐ y"
by unfold_locales (auto simp: StrictRefEq⇩S⇩e⇩t)
subsection‹Constants: mtSet›
definition mtSet::"('𝔄,'α::null) Set" ("Set{}")
where "Set{} ≡ (λ τ. Abs_Set⇩b⇩a⇩s⇩e ⌊⌊{}::'α set⌋⌋ )"
lemma mtSet_defined[simp,code_unfold]:"δ(Set{}) = true"
apply(rule ext, auto simp: mtSet_def defined_def null_Set⇩b⇩a⇩s⇩e_def
bot_Set⇩b⇩a⇩s⇩e_def bot_fun_def null_fun_def)
by(simp_all add: Abs_Set⇩b⇩a⇩s⇩e_inject bot_option_def null_Set⇩b⇩a⇩s⇩e_def null_option_def)
lemma mtSet_valid[simp,code_unfold]:"υ(Set{}) = true"
apply(rule ext,auto simp: mtSet_def valid_def null_Set⇩b⇩a⇩s⇩e_def
bot_Set⇩b⇩a⇩s⇩e_def bot_fun_def null_fun_def)
by(simp_all add: Abs_Set⇩b⇩a⇩s⇩e_inject bot_option_def null_Set⇩b⇩a⇩s⇩e_def null_option_def)
lemma mtSet_rep_set: "⌈⌈Rep_Set⇩b⇩a⇩s⇩e (Set{} τ)⌉⌉ = {}"
apply(simp add: mtSet_def, subst Abs_Set⇩b⇩a⇩s⇩e_inverse)
by(simp add: bot_option_def)+
lemma [simp,code_unfold]: "const Set{}"
by(simp add: const_def mtSet_def)
text‹Note that the collection types in OCL allow for null to be included;
however, there is the null-collection into which inclusion yields invalid.›
subsection‹Definition: Including›
definition OclIncluding :: "[('𝔄,'α::null) Set,('𝔄,'α) val] ⇒ ('𝔄,'α) Set"
where "OclIncluding x y = (λ τ. if (δ x) τ = true τ ∧ (υ y) τ = true τ
then Abs_Set⇩b⇩a⇩s⇩e ⌊⌊ ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (x τ)⌉⌉ ∪ {y τ} ⌋⌋
else invalid τ )"
notation OclIncluding ("_->including⇩S⇩e⇩t'(_')")
interpretation OclIncluding : profile_bin⇩d_⇩v OclIncluding "λx y. Abs_Set⇩b⇩a⇩s⇩e⌊⌊⌈⌈Rep_Set⇩b⇩a⇩s⇩e x⌉⌉ ∪ {y}⌋⌋"
proof -
have A : "None ∈ {X. X = bot ∨ X = null ∨ (∀x∈⌈⌈X⌉⌉. x ≠ bot)}" by(simp add: bot_option_def)
have B : "⌊None⌋ ∈ {X. X = bot ∨ X = null ∨ (∀x∈⌈⌈X⌉⌉. x ≠ bot)}"
by(simp add: null_option_def bot_option_def)
have C : "⋀x y. x ≠ ⊥ ⟹ x ≠ null ⟹ y ≠ ⊥ ⟹
⌊⌊insert y ⌈⌈Rep_Set⇩b⇩a⇩s⇩e x⌉⌉⌋⌋ ∈ {X. X = bot ∨ X = null ∨ (∀x∈⌈⌈X⌉⌉. x ≠ bot)}"
by(auto intro!:Set_inv_lemma[simplified OclValid_def
defined_def false_def true_def null_fun_def bot_fun_def])
show "profile_bin⇩d_⇩v OclIncluding (λx y. Abs_Set⇩b⇩a⇩s⇩e⌊⌊⌈⌈Rep_Set⇩b⇩a⇩s⇩e x⌉⌉ ∪ {y}⌋⌋)"
apply unfold_locales
apply(auto simp:OclIncluding_def bot_option_def null_option_def null_Set⇩b⇩a⇩s⇩e_def bot_Set⇩b⇩a⇩s⇩e_def)
apply(erule_tac Q="Abs_Set⇩b⇩a⇩s⇩e⌊⌊insert y ⌈⌈Rep_Set⇩b⇩a⇩s⇩e x⌉⌉⌋⌋ = Abs_Set⇩b⇩a⇩s⇩e None" in contrapos_pp)
apply(subst Abs_Set⇩b⇩a⇩s⇩e_inject[OF C A])
apply(simp_all add: null_Set⇩b⇩a⇩s⇩e_def bot_Set⇩b⇩a⇩s⇩e_def bot_option_def)
apply(erule_tac Q="Abs_Set⇩b⇩a⇩s⇩e⌊⌊insert y ⌈⌈Rep_Set⇩b⇩a⇩s⇩e x⌉⌉⌋⌋ = Abs_Set⇩b⇩a⇩s⇩e ⌊None⌋" in contrapos_pp)
apply(subst Abs_Set⇩b⇩a⇩s⇩e_inject[OF C B])
apply(simp_all add: null_Set⇩b⇩a⇩s⇩e_def bot_Set⇩b⇩a⇩s⇩e_def bot_option_def)
done
qed
syntax
"_OclFinset" :: "args => ('𝔄,'a::null) Set" ("Set{(_)}")
translations
"Set{x, xs}" == "CONST OclIncluding (Set{xs}) x"
"Set{x}" == "CONST OclIncluding (Set{}) x "
subsection‹Definition: Excluding›
definition OclExcluding :: "[('𝔄,'α::null) Set,('𝔄,'α) val] ⇒ ('𝔄,'α) Set"
where "OclExcluding x y = (λ τ. if (δ x) τ = true τ ∧ (υ y) τ = true τ
then Abs_Set⇩b⇩a⇩s⇩e ⌊⌊ ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (x τ)⌉⌉ - {y τ} ⌋⌋
else ⊥ )"
notation OclExcluding ("_->excluding⇩S⇩e⇩t'(_')")
lemma OclExcluding_inv: "(x:: Set('b::{null})) ≠ ⊥ ⟹ x ≠ null ⟹ y ≠ ⊥ ⟹
⌊⌊⌈⌈Rep_Set⇩b⇩a⇩s⇩e x⌉⌉ - {y}⌋⌋ ∈ {X. X = bot ∨ X = null ∨ (∀x∈⌈⌈X⌉⌉. x ≠ bot)}"
proof - fix X :: "'a state × 'a state ⇒ Set('b)" fix τ
show "x ≠ ⊥ ⟹ x ≠ null ⟹ y ≠ ⊥ ⟹ ?thesis"
when "x = X τ"
by(simp add: that Set_inv_lemma[simplified OclValid_def
defined_def null_fun_def bot_fun_def, of X τ])
qed simp_all
interpretation OclExcluding : profile_bin⇩d_⇩v OclExcluding "λx y. Abs_Set⇩b⇩a⇩s⇩e⌊⌊⌈⌈Rep_Set⇩b⇩a⇩s⇩e x⌉⌉ - {y}⌋⌋"
proof -
have A : "None ∈ {X. X = bot ∨ X = null ∨ (∀x∈⌈⌈X⌉⌉. x ≠ bot)}" by(simp add: bot_option_def)
have B : "⌊None⌋ ∈ {X. X = bot ∨ X = null ∨ (∀x∈⌈⌈X⌉⌉. x ≠ bot)}"
by(simp add: null_option_def bot_option_def)
show "profile_bin⇩d_⇩v OclExcluding (λx y. Abs_Set⇩b⇩a⇩s⇩e⌊⌊⌈⌈Rep_Set⇩b⇩a⇩s⇩e (x:: Set('b))⌉⌉ - {y}⌋⌋)"
apply unfold_locales
apply(auto simp:OclExcluding_def bot_option_def null_option_def null_Set⇩b⇩a⇩s⇩e_def bot_Set⇩b⇩a⇩s⇩e_def invalid_def)
apply(erule_tac Q="Abs_Set⇩b⇩a⇩s⇩e⌊⌊⌈⌈Rep_Set⇩b⇩a⇩s⇩e x⌉⌉ - {y}⌋⌋ = Abs_Set⇩b⇩a⇩s⇩e None" in contrapos_pp)
apply(subst Abs_Set⇩b⇩a⇩s⇩e_inject[OF OclExcluding_inv A])
apply(simp_all add: null_Set⇩b⇩a⇩s⇩e_def bot_Set⇩b⇩a⇩s⇩e_def bot_option_def)
apply(erule_tac Q="Abs_Set⇩b⇩a⇩s⇩e⌊⌊⌈⌈Rep_Set⇩b⇩a⇩s⇩e x⌉⌉ - {y}⌋⌋ = Abs_Set⇩b⇩a⇩s⇩e ⌊None⌋" in contrapos_pp)
apply(subst Abs_Set⇩b⇩a⇩s⇩e_inject[OF OclExcluding_inv B])
apply(simp_all add: null_Set⇩b⇩a⇩s⇩e_def bot_Set⇩b⇩a⇩s⇩e_def bot_option_def)
done
qed
subsection‹Definition: Includes›
definition OclIncludes :: "[('𝔄,'α::null) Set,('𝔄,'α) val] ⇒ '𝔄 Boolean"
where "OclIncludes x y = (λ τ. if (δ x) τ = true τ ∧ (υ y) τ = true τ
then ⌊⌊(y τ) ∈ ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (x τ)⌉⌉ ⌋⌋
else ⊥ )"
notation OclIncludes ("_->includes⇩S⇩e⇩t'(_')" )
interpretation OclIncludes : profile_bin⇩d_⇩v OclIncludes "λx y. ⌊⌊y ∈ ⌈⌈Rep_Set⇩b⇩a⇩s⇩e x⌉⌉⌋⌋"
by(unfold_locales, auto simp:OclIncludes_def bot_option_def null_option_def invalid_def)
subsection‹Definition: Excludes›
definition OclExcludes :: "[('𝔄,'α::null) Set,('𝔄,'α) val] ⇒ '𝔄 Boolean"
where "OclExcludes x y = (not(OclIncludes x y))"
notation OclExcludes ("_->excludes⇩S⇩e⇩t'(_')" )
text‹The case of the size definition is somewhat special, we admit
explicitly in Featherweight OCL the possibility of infinite sets. For
the size definition, this requires an extra condition that assures
that the cardinality of the set is actually a defined integer.›
interpretation OclExcludes : profile_bin⇩d_⇩v OclExcludes "λx y. ⌊⌊y ∉ ⌈⌈Rep_Set⇩b⇩a⇩s⇩e x⌉⌉⌋⌋"
by(unfold_locales, auto simp:OclExcludes_def OclIncludes_def OclNot_def bot_option_def null_option_def invalid_def)
subsection‹Definition: Size›
definition OclSize :: "('𝔄,'α::null)Set ⇒ '𝔄 Integer"
where "OclSize x = (λ τ. if (δ x) τ = true τ ∧ finite(⌈⌈Rep_Set⇩b⇩a⇩s⇩e (x τ)⌉⌉)
then ⌊⌊ int(card ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (x τ)⌉⌉) ⌋⌋
else ⊥ )"
notation
OclSize ("_->size⇩S⇩e⇩t'(')" )
text‹The following definition follows the requirement of the
standard to treat null as neutral element of sets. It is
a well-documented exception from the general strictness
rule and the rule that the distinguished argument self should
be non-null.›
subsection‹Definition: IsEmpty›
definition OclIsEmpty :: "('𝔄,'α::null) Set ⇒ '𝔄 Boolean"
where "OclIsEmpty x = ((υ x and not (δ x)) or ((OclSize x) ≐ 𝟬))"
notation OclIsEmpty ("_->isEmpty⇩S⇩e⇩t'(')" )
subsection‹Definition: NotEmpty›
definition OclNotEmpty :: "('𝔄,'α::null) Set ⇒ '𝔄 Boolean"
where "OclNotEmpty x = not(OclIsEmpty x)"
notation OclNotEmpty ("_->notEmpty⇩S⇩e⇩t'(')" )
subsection‹Definition: Any›
definition OclANY :: "[('𝔄,'α::null) Set] ⇒ ('𝔄,'α) val"
where "OclANY x = (λ τ. if (υ x) τ = true τ
then if (δ x and OclNotEmpty x) τ = true τ
then SOME y. y ∈ ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (x τ)⌉⌉
else null τ
else ⊥ )"
notation OclANY ("_->any⇩S⇩e⇩t'(')")
subsection‹Definition: Forall›
text‹The definition of OclForall mimics the one of @{term "OclAnd"}:
OclForall is not a strict operation.›
definition OclForall :: "[('𝔄,'α::null)Set,('𝔄,'α)val⇒('𝔄)Boolean] ⇒ '𝔄 Boolean"
where "OclForall S P = (λ τ. if (δ S) τ = true τ
then if (∃x∈⌈⌈Rep_Set⇩b⇩a⇩s⇩e (S τ)⌉⌉. P(λ _. x) τ = false τ)
then false τ
else if (∃x∈⌈⌈Rep_Set⇩b⇩a⇩s⇩e (S τ)⌉⌉. P(λ _. x) τ = invalid τ)
then invalid τ
else if (∃x∈⌈⌈Rep_Set⇩b⇩a⇩s⇩e (S τ)⌉⌉. P(λ _. x) τ = null τ)
then null τ
else true τ
else ⊥)"
syntax
"_OclForallSet" :: "[('𝔄,'α::null) Set,id,('𝔄)Boolean] ⇒ '𝔄 Boolean" ("(_)->forAll⇩S⇩e⇩t'(_|_')")
translations
"X->forAll⇩S⇩e⇩t(x | P)" == "CONST UML_Set.OclForall X (%x. P)"
subsection‹Definition: Exists›
text‹Like OclForall, OclExists is also not strict.›
definition OclExists :: "[('𝔄,'α::null) Set,('𝔄,'α)val⇒('𝔄)Boolean] ⇒ '𝔄 Boolean"
where "OclExists S P = not(UML_Set.OclForall S (λ X. not (P X)))"
syntax
"_OclExistSet" :: "[('𝔄,'α::null) Set,id,('𝔄)Boolean] ⇒ '𝔄 Boolean" ("(_)->exists⇩S⇩e⇩t'(_|_')")
translations
"X->exists⇩S⇩e⇩t(x | P)" == "CONST UML_Set.OclExists X (%x. P)"
subsection‹Definition: Iterate›
definition OclIterate :: "[('𝔄,'α::null) Set,('𝔄,'β::null)val,
('𝔄,'α)val⇒('𝔄,'β)val⇒('𝔄,'β)val] ⇒ ('𝔄,'β)val"
where "OclIterate S A F = (λ τ. if (δ S) τ = true τ ∧ (υ A) τ = true τ ∧ finite⌈⌈Rep_Set⇩b⇩a⇩s⇩e (S τ)⌉⌉
then (Finite_Set.fold (F) (A) ((λa τ. a) ` ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (S τ)⌉⌉))τ
else ⊥)"
syntax
"_OclIterateSet" :: "[('𝔄,'α::null) Set, idt, idt, 'α, 'β] => ('𝔄,'γ)val"
("_ ->iterate⇩S⇩e⇩t'(_;_=_ | _')" )
translations
"X->iterate⇩S⇩e⇩t(a; x = A | P)" == "CONST OclIterate X A (%a. (% x. P))"
subsection‹Definition: Select›
definition OclSelect :: "[('𝔄,'α::null)Set,('𝔄,'α)val⇒('𝔄)Boolean] ⇒ ('𝔄,'α)Set"
where "OclSelect S P = (λτ. if (δ S) τ = true τ
then if (∃x∈⌈⌈Rep_Set⇩b⇩a⇩s⇩e (S τ)⌉⌉. P(λ _. x) τ = invalid τ)
then invalid τ
else Abs_Set⇩b⇩a⇩s⇩e ⌊⌊{x∈⌈⌈ Rep_Set⇩b⇩a⇩s⇩e (S τ)⌉⌉. P (λ_. x) τ ≠ false τ}⌋⌋
else invalid τ)"
syntax
"_OclSelectSet" :: "[('𝔄,'α::null) Set,id,('𝔄)Boolean] ⇒ '𝔄 Boolean" ("(_)->select⇩S⇩e⇩t'(_|_')")
translations
"X->select⇩S⇩e⇩t(x | P)" == "CONST OclSelect X (% x. P)"
subsection‹Definition: Reject›
definition OclReject :: "[('𝔄,'α::null)Set,('𝔄,'α)val⇒('𝔄)Boolean] ⇒ ('𝔄,'α::null)Set"
where "OclReject S P = OclSelect S (not o P)"
syntax
"_OclRejectSet" :: "[('𝔄,'α::null) Set,id,('𝔄)Boolean] ⇒ '𝔄 Boolean" ("(_)->reject⇩S⇩e⇩t'(_|_')")
translations
"X->reject⇩S⇩e⇩t(x | P)" == "CONST OclReject X (% x. P)"
subsection‹Definition: IncludesAll›
definition OclIncludesAll :: "[('𝔄,'α::null) Set,('𝔄,'α) Set] ⇒ '𝔄 Boolean"
where "OclIncludesAll x y = (λ τ. if (δ x) τ = true τ ∧ (δ y) τ = true τ
then ⌊⌊⌈⌈Rep_Set⇩b⇩a⇩s⇩e (y τ)⌉⌉ ⊆ ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (x τ)⌉⌉ ⌋⌋
else ⊥ )"
notation OclIncludesAll ("_->includesAll⇩S⇩e⇩t'(_')" )
interpretation OclIncludesAll : profile_bin⇩d_⇩d OclIncludesAll "λx y. ⌊⌊⌈⌈Rep_Set⇩b⇩a⇩s⇩e y⌉⌉ ⊆ ⌈⌈Rep_Set⇩b⇩a⇩s⇩e x⌉⌉⌋⌋"
by(unfold_locales, auto simp:OclIncludesAll_def bot_option_def null_option_def invalid_def)
subsection‹Definition: ExcludesAll›
definition OclExcludesAll :: "[('𝔄,'α::null) Set,('𝔄,'α) Set] ⇒ '𝔄 Boolean"
where "OclExcludesAll x y = (λ τ. if (δ x) τ = true τ ∧ (δ y) τ = true τ
then ⌊⌊⌈⌈Rep_Set⇩b⇩a⇩s⇩e (y τ)⌉⌉ ∩ ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (x τ)⌉⌉ = {} ⌋⌋
else ⊥ )"
notation OclExcludesAll ("_->excludesAll⇩S⇩e⇩t'(_')" )
interpretation OclExcludesAll : profile_bin⇩d_⇩d OclExcludesAll "λx y. ⌊⌊⌈⌈Rep_Set⇩b⇩a⇩s⇩e y⌉⌉ ∩ ⌈⌈Rep_Set⇩b⇩a⇩s⇩e x⌉⌉ = {}⌋⌋"
by(unfold_locales, auto simp:OclExcludesAll_def bot_option_def null_option_def invalid_def)
subsection‹Definition: Union›
definition OclUnion :: "[('𝔄,'α::null) Set,('𝔄,'α) Set] ⇒ ('𝔄,'α) Set"
where "OclUnion x y = (λ τ. if (δ x) τ = true τ ∧ (δ y) τ = true τ
then Abs_Set⇩b⇩a⇩s⇩e⌊⌊⌈⌈Rep_Set⇩b⇩a⇩s⇩e (y τ)⌉⌉ ∪ ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (x τ)⌉⌉ ⌋⌋
else ⊥ )"
notation OclUnion ("_->union⇩S⇩e⇩t'(_')" )
lemma OclUnion_inv: "(x:: Set('b::{null})) ≠ ⊥ ⟹ x ≠ null ⟹ y ≠ ⊥ ⟹ y ≠ null ⟹
⌊⌊⌈⌈Rep_Set⇩b⇩a⇩s⇩e y⌉⌉ ∪ ⌈⌈Rep_Set⇩b⇩a⇩s⇩e x⌉⌉⌋⌋ ∈ {X. X = bot ∨ X = null ∨ (∀x∈⌈⌈X⌉⌉. x ≠ bot)}"
proof - fix X Y :: "'a state × 'a state ⇒ Set('b)" fix τ
show "x ≠ ⊥ ⟹ x ≠ null ⟹ y ≠ ⊥ ⟹ y ≠ null ⟹ ?thesis"
when "x = X τ" "y = Y τ"
by(auto simp: that,
insert
Set_inv_lemma[simplified OclValid_def
defined_def null_fun_def bot_fun_def, of Y τ]
Set_inv_lemma[simplified OclValid_def
defined_def null_fun_def bot_fun_def, of X τ],
auto)
qed simp_all
interpretation OclUnion : profile_bin⇩d_⇩d OclUnion "λx y. Abs_Set⇩b⇩a⇩s⇩e⌊⌊⌈⌈Rep_Set⇩b⇩a⇩s⇩e y⌉⌉ ∪ ⌈⌈Rep_Set⇩b⇩a⇩s⇩e x⌉⌉⌋⌋"
proof -
have A : "None ∈ {X. X = bot ∨ X = null ∨ (∀x∈⌈⌈X⌉⌉. x ≠ bot)}" by(simp add: bot_option_def)
have B : "⌊None⌋ ∈ {X. X = bot ∨ X = null ∨ (∀x∈⌈⌈X⌉⌉. x ≠ bot)}"
by(simp add: null_option_def bot_option_def)
show "profile_bin⇩d_⇩d OclUnion (λx y. Abs_Set⇩b⇩a⇩s⇩e⌊⌊⌈⌈Rep_Set⇩b⇩a⇩s⇩e y⌉⌉ ∪ ⌈⌈Rep_Set⇩b⇩a⇩s⇩e x⌉⌉⌋⌋)"
apply unfold_locales
apply(auto simp:OclUnion_def bot_option_def null_option_def null_Set⇩b⇩a⇩s⇩e_def bot_Set⇩b⇩a⇩s⇩e_def invalid_def)
apply(erule_tac Q="Abs_Set⇩b⇩a⇩s⇩e⌊⌊⌈⌈Rep_Set⇩b⇩a⇩s⇩e y⌉⌉ ∪ ⌈⌈Rep_Set⇩b⇩a⇩s⇩e x⌉⌉⌋⌋ = Abs_Set⇩b⇩a⇩s⇩e None" in contrapos_pp)
apply(subst Abs_Set⇩b⇩a⇩s⇩e_inject[OF OclUnion_inv A])
apply(simp_all add: null_Set⇩b⇩a⇩s⇩e_def bot_Set⇩b⇩a⇩s⇩e_def bot_option_def)
apply(erule_tac Q="Abs_Set⇩b⇩a⇩s⇩e⌊⌊⌈⌈Rep_Set⇩b⇩a⇩s⇩e y⌉⌉ ∪ ⌈⌈Rep_Set⇩b⇩a⇩s⇩e x⌉⌉⌋⌋ = Abs_Set⇩b⇩a⇩s⇩e ⌊None⌋" in contrapos_pp)
apply(subst Abs_Set⇩b⇩a⇩s⇩e_inject[OF OclUnion_inv B])
apply(simp_all add: null_Set⇩b⇩a⇩s⇩e_def bot_Set⇩b⇩a⇩s⇩e_def bot_option_def)
done
qed
subsection‹Definition: Intersection›
definition OclIntersection :: "[('𝔄,'α::null) Set,('𝔄,'α) Set] ⇒ ('𝔄,'α) Set"
where "OclIntersection x y = (λ τ. if (δ x) τ = true τ ∧ (δ y) τ = true τ
then Abs_Set⇩b⇩a⇩s⇩e⌊⌊⌈⌈Rep_Set⇩b⇩a⇩s⇩e (y τ)⌉⌉
∩ ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (x τ)⌉⌉⌋⌋
else ⊥ )"
notation OclIntersection("_->intersection⇩S⇩e⇩t'(_')" )
lemma OclIntersection_inv: "(x:: Set('b::{null})) ≠ ⊥ ⟹ x ≠ null ⟹ y ≠ ⊥ ⟹ y ≠ null ⟹
⌊⌊⌈⌈Rep_Set⇩b⇩a⇩s⇩e y⌉⌉ ∩ ⌈⌈Rep_Set⇩b⇩a⇩s⇩e x⌉⌉⌋⌋ ∈ {X. X = bot ∨ X = null ∨ (∀x∈⌈⌈X⌉⌉. x ≠ bot)}"
proof - fix X Y :: "'a state × 'a state ⇒ Set('b)" fix τ
show "x ≠ ⊥ ⟹ x ≠ null ⟹ y ≠ ⊥ ⟹ y ≠ null ⟹ ?thesis"
when "x = X τ" "y = Y τ"
by(auto simp: that,
insert
Set_inv_lemma[simplified OclValid_def
defined_def null_fun_def bot_fun_def, of Y τ]
Set_inv_lemma[simplified OclValid_def
defined_def null_fun_def bot_fun_def, of X τ],
auto)
qed simp_all
interpretation OclIntersection : profile_bin⇩d_⇩d OclIntersection "λx y. Abs_Set⇩b⇩a⇩s⇩e⌊⌊⌈⌈Rep_Set⇩b⇩a⇩s⇩e y⌉⌉ ∩ ⌈⌈Rep_Set⇩b⇩a⇩s⇩e x⌉⌉⌋⌋"
proof -
have A : "None ∈ {X. X = bot ∨ X = null ∨ (∀x∈⌈⌈X⌉⌉. x ≠ bot)}" by(simp add: bot_option_def)
have B : "⌊None⌋ ∈ {X. X = bot ∨ X = null ∨ (∀x∈⌈⌈X⌉⌉. x ≠ bot)}"
by(simp add: null_option_def bot_option_def)
show "profile_bin⇩d_⇩d OclIntersection (λx y. Abs_Set⇩b⇩a⇩s⇩e⌊⌊⌈⌈Rep_Set⇩b⇩a⇩s⇩e y⌉⌉ ∩ ⌈⌈Rep_Set⇩b⇩a⇩s⇩e x⌉⌉⌋⌋)"
apply unfold_locales
apply(auto simp:OclIntersection_def bot_option_def null_option_def null_Set⇩b⇩a⇩s⇩e_def bot_Set⇩b⇩a⇩s⇩e_def invalid_def)
apply(erule_tac Q="Abs_Set⇩b⇩a⇩s⇩e⌊⌊⌈⌈Rep_Set⇩b⇩a⇩s⇩e y⌉⌉ ∩ ⌈⌈Rep_Set⇩b⇩a⇩s⇩e x⌉⌉⌋⌋ = Abs_Set⇩b⇩a⇩s⇩e None" in contrapos_pp)
apply(subst Abs_Set⇩b⇩a⇩s⇩e_inject[OF OclIntersection_inv A])
apply(simp_all add: null_Set⇩b⇩a⇩s⇩e_def bot_Set⇩b⇩a⇩s⇩e_def bot_option_def)
apply(erule_tac Q="Abs_Set⇩b⇩a⇩s⇩e⌊⌊⌈⌈Rep_Set⇩b⇩a⇩s⇩e y⌉⌉ ∩ ⌈⌈Rep_Set⇩b⇩a⇩s⇩e x⌉⌉⌋⌋ = Abs_Set⇩b⇩a⇩s⇩e ⌊None⌋" in contrapos_pp)
apply(subst Abs_Set⇩b⇩a⇩s⇩e_inject[OF OclIntersection_inv B])
apply(simp_all add: null_Set⇩b⇩a⇩s⇩e_def bot_Set⇩b⇩a⇩s⇩e_def bot_option_def)
done
qed
subsection‹Definition (future operators)›
consts
OclCount :: "[('𝔄,'α::null) Set,('𝔄,'α) Set] ⇒ '𝔄 Integer"
OclSum :: " ('𝔄,'α::null) Set ⇒ '𝔄 Integer"
notation OclCount ("_->count⇩S⇩e⇩t'(_')" )
notation OclSum ("_->sum⇩S⇩e⇩t'(')" )
subsection‹Logical Properties›
text‹OclIncluding›
lemma OclIncluding_valid_args_valid:
"(τ ⊨ υ(X->including⇩S⇩e⇩t(x))) = ((τ ⊨(δ X)) ∧ (τ ⊨(υ x)))"
by (metis (opaque_lifting, no_types) OclIncluding.def_valid_then_def OclIncluding.defined_args_valid)
lemma OclIncluding_valid_args_valid''[simp,code_unfold]:
"υ(X->including⇩S⇩e⇩t(x)) = ((δ X) and (υ x))"
by (simp add: OclIncluding.def_valid_then_def)
text‹etc. etc.›
text_raw‹\isatagafp›
text‹OclExcluding›
lemma OclExcluding_valid_args_valid:
"(τ ⊨ υ(X->excluding⇩S⇩e⇩t(x))) = ((τ ⊨(δ X)) ∧ (τ ⊨(υ x)))"
by (metis OclExcluding.def_valid_then_def OclExcluding.defined_args_valid)
lemma OclExcluding_valid_args_valid''[simp,code_unfold]:
"υ(X->excluding⇩S⇩e⇩t(x)) = ((δ X) and (υ x))"
by (simp add: OclExcluding.def_valid_then_def)
text‹OclIncludes›
lemma OclIncludes_valid_args_valid:
"(τ ⊨ υ(X->includes⇩S⇩e⇩t(x))) = ((τ ⊨(δ X)) ∧ (τ ⊨(υ x)))"
by (simp add: OclIncludes.def_valid_then_def foundation10')
lemma OclIncludes_valid_args_valid''[simp,code_unfold]:
"υ(X->includes⇩S⇩e⇩t(x)) = ((δ X) and (υ x))"
by (simp add: OclIncludes.def_valid_then_def)
text‹OclExcludes›
lemma OclExcludes_valid_args_valid:
"(τ ⊨ υ(X->excludes⇩S⇩e⇩t(x))) = ((τ ⊨(δ X)) ∧ (τ ⊨(υ x)))"
by (simp add: OclExcludes.def_valid_then_def foundation10')
lemma OclExcludes_valid_args_valid''[simp,code_unfold]:
"υ(X->excludes⇩S⇩e⇩t(x)) = ((δ X) and (υ x))"
by (simp add: OclExcludes.def_valid_then_def)
text‹OclSize›
lemma OclSize_defined_args_valid: "τ ⊨ δ (X->size⇩S⇩e⇩t()) ⟹ τ ⊨ δ X"
by(auto simp: OclSize_def OclValid_def true_def valid_def false_def StrongEq_def
defined_def invalid_def bot_fun_def null_fun_def
split: bool.split_asm HOL.if_split_asm option.split)
lemma OclSize_infinite:
assumes non_finite:"τ ⊨ not(δ(S->size⇩S⇩e⇩t()))"
shows "(τ ⊨ not(δ(S))) ∨ ¬ finite ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (S τ)⌉⌉"
apply(insert non_finite, simp)
apply(rule impI)
apply(simp add: OclSize_def OclValid_def defined_def)
apply(case_tac "finite ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (S τ)⌉⌉",
simp_all add:null_fun_def null_option_def bot_fun_def bot_option_def)
done
lemma "τ ⊨ δ X ⟹ ¬ finite ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X τ)⌉⌉ ⟹ ¬ τ ⊨ δ (X->size⇩S⇩e⇩t())"
by(simp add: OclSize_def OclValid_def defined_def bot_fun_def false_def true_def)
lemma size_defined:
assumes X_finite: "⋀τ. finite ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X τ)⌉⌉"
shows "δ (X->size⇩S⇩e⇩t()) = δ X"
apply(rule ext, simp add: cp_defined[of "X->size⇩S⇩e⇩t()"] OclSize_def)
apply(simp add: defined_def bot_option_def bot_fun_def null_option_def null_fun_def X_finite)
done
lemma size_defined':
assumes X_finite: "finite ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X τ)⌉⌉"
shows "(τ ⊨ δ (X->size⇩S⇩e⇩t())) = (τ ⊨ δ X)"
apply(simp add: cp_defined[of "X->size⇩S⇩e⇩t()"] OclSize_def OclValid_def)
apply(simp add: defined_def bot_option_def bot_fun_def null_option_def null_fun_def X_finite)
done
text‹OclIsEmpty›
lemma OclIsEmpty_defined_args_valid:"τ ⊨ δ (X->isEmpty⇩S⇩e⇩t()) ⟹ τ ⊨ υ X"
apply(auto simp: OclIsEmpty_def OclValid_def defined_def valid_def false_def true_def
bot_fun_def null_fun_def OclAnd_def OclOr_def OclNot_def
split: if_split_asm)
apply(case_tac "(X->size⇩S⇩e⇩t() ≐ 𝟬) τ", simp add: bot_option_def, simp, rename_tac x)
apply(case_tac x, simp add: null_option_def bot_option_def, simp)
apply(simp add: OclSize_def StrictRefEq⇩I⇩n⇩t⇩e⇩g⇩e⇩r valid_def)
by (metis (opaque_lifting, no_types)
bot_fun_def OclValid_def defined_def foundation2 invalid_def)
lemma "τ ⊨ δ (null->isEmpty⇩S⇩e⇩t())"
by(auto simp: OclIsEmpty_def OclValid_def defined_def valid_def false_def true_def
bot_fun_def null_fun_def OclAnd_def OclOr_def OclNot_def null_is_valid
split: if_split_asm)
lemma OclIsEmpty_infinite: "τ ⊨ δ X ⟹ ¬ finite ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X τ)⌉⌉ ⟹ ¬ τ ⊨ δ (X->isEmpty⇩S⇩e⇩t())"
apply(auto simp: OclIsEmpty_def OclValid_def defined_def valid_def false_def true_def
bot_fun_def null_fun_def OclAnd_def OclOr_def OclNot_def
split: if_split_asm)
apply(case_tac "(X->size⇩S⇩e⇩t() ≐ 𝟬) τ", simp add: bot_option_def, simp, rename_tac x)
apply(case_tac x, simp add: null_option_def bot_option_def, simp)
by(simp add: OclSize_def StrictRefEq⇩I⇩n⇩t⇩e⇩g⇩e⇩r valid_def bot_fun_def false_def true_def invalid_def)
text‹OclNotEmpty›
lemma OclNotEmpty_defined_args_valid:"τ ⊨ δ (X->notEmpty⇩S⇩e⇩t()) ⟹ τ ⊨ υ X"
by (metis (opaque_lifting, no_types) OclNotEmpty_def OclNot_defargs OclNot_not foundation6 foundation9
OclIsEmpty_defined_args_valid)
lemma "τ ⊨ δ (null->notEmpty⇩S⇩e⇩t())"
by (metis (opaque_lifting, no_types) OclNotEmpty_def OclAnd_false1 OclAnd_idem OclIsEmpty_def
OclNot3 OclNot4 OclOr_def defined2 defined4 transform1 valid2)
lemma OclNotEmpty_infinite: "τ ⊨ δ X ⟹ ¬ finite ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X τ)⌉⌉ ⟹ ¬ τ ⊨ δ (X->notEmpty⇩S⇩e⇩t())"
apply(simp add: OclNotEmpty_def)
apply(drule OclIsEmpty_infinite, simp)
by (metis OclNot_defargs OclNot_not foundation6 foundation9)
lemma OclNotEmpty_has_elt : "τ ⊨ δ X ⟹
τ ⊨ X->notEmpty⇩S⇩e⇩t() ⟹
∃e. e ∈ ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X τ)⌉⌉"
apply(simp add: OclNotEmpty_def OclIsEmpty_def deMorgan1 deMorgan2, drule foundation5)
apply(subst (asm) (2) OclNot_def,
simp add: OclValid_def StrictRefEq⇩I⇩n⇩t⇩e⇩g⇩e⇩r StrongEq_def
split: if_split_asm)
prefer 2
apply(simp add: invalid_def bot_option_def true_def)
apply(simp add: OclSize_def valid_def split: if_split_asm,
simp_all add: false_def true_def bot_option_def bot_fun_def OclInt0_def)
by (metis equals0I)
text‹OclANY›
lemma OclANY_defined_args_valid: "τ ⊨ δ (X->any⇩S⇩e⇩t()) ⟹ τ ⊨ δ X"
by(auto simp: OclANY_def OclValid_def true_def valid_def false_def StrongEq_def
defined_def invalid_def bot_fun_def null_fun_def OclAnd_def
split: bool.split_asm HOL.if_split_asm option.split)
lemma "τ ⊨ δ X ⟹ τ ⊨ X->isEmpty⇩S⇩e⇩t() ⟹ ¬ τ ⊨ δ (X->any⇩S⇩e⇩t())"
apply(simp add: OclANY_def OclValid_def)
apply(subst cp_defined, subst cp_OclAnd, simp add: OclNotEmpty_def, subst (1 2) cp_OclNot,
simp add: cp_OclNot[symmetric] cp_OclAnd[symmetric] cp_defined[symmetric],
simp add: false_def true_def)
by(drule foundation20[simplified OclValid_def true_def], simp)
lemma OclANY_valid_args_valid:
"(τ ⊨ υ(X->any⇩S⇩e⇩t())) = (τ ⊨ υ X)"
proof -
have A: "(τ ⊨ υ(X->any⇩S⇩e⇩t())) ⟹ ((τ ⊨(υ X)))"
by(auto simp: OclANY_def OclValid_def true_def valid_def false_def StrongEq_def
defined_def invalid_def bot_fun_def null_fun_def
split: bool.split_asm HOL.if_split_asm option.split)
have B: "(τ ⊨(υ X)) ⟹ (τ ⊨ υ(X->any⇩S⇩e⇩t()))"
apply(auto simp: OclANY_def OclValid_def true_def false_def StrongEq_def
defined_def invalid_def valid_def bot_fun_def null_fun_def
bot_option_def null_option_def null_is_valid
OclAnd_def
split: bool.split_asm HOL.if_split_asm option.split)
apply(frule Set_inv_lemma[OF foundation16[THEN iffD2], OF conjI], simp)
apply(subgoal_tac "(δ X) τ = true τ")
prefer 2
apply (metis (opaque_lifting, no_types) OclValid_def foundation16)
apply(simp add: true_def,
drule OclNotEmpty_has_elt[simplified OclValid_def true_def], simp)
by(erule exE,
insert someI2[where Q = "λx. x ≠ ⊥" and P = "λy. y ∈ ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X τ)⌉⌉"],
simp)
show ?thesis by(auto dest:A intro:B)
qed
lemma OclANY_valid_args_valid''[simp,code_unfold]:
"υ(X->any⇩S⇩e⇩t()) = (υ X)"
by(auto intro!: OclANY_valid_args_valid transform2_rev)
text_raw‹\endisatagafp›
subsection‹Execution Laws with Invalid or Null or Infinite Set as Argument›
text‹OclIncluding›
text‹OclExcluding›
text‹OclIncludes›
text‹OclExcludes›
text‹OclSize›
lemma OclSize_invalid[simp,code_unfold]:"(invalid->size⇩S⇩e⇩t()) = invalid"
by(simp add: bot_fun_def OclSize_def invalid_def defined_def valid_def false_def true_def)
lemma OclSize_null[simp,code_unfold]:"(null->size⇩S⇩e⇩t()) = invalid"
by(rule ext,
simp add: bot_fun_def null_fun_def null_is_valid OclSize_def
invalid_def defined_def valid_def false_def true_def)
text‹OclIsEmpty›
lemma OclIsEmpty_invalid[simp,code_unfold]:"(invalid->isEmpty⇩S⇩e⇩t()) = invalid"
by(simp add: OclIsEmpty_def)
lemma OclIsEmpty_null[simp,code_unfold]:"(null->isEmpty⇩S⇩e⇩t()) = true"
by(simp add: OclIsEmpty_def)
text‹OclNotEmpty›
lemma OclNotEmpty_invalid[simp,code_unfold]:"(invalid->notEmpty⇩S⇩e⇩t()) = invalid"
by(simp add: OclNotEmpty_def)
lemma OclNotEmpty_null[simp,code_unfold]:"(null->notEmpty⇩S⇩e⇩t()) = false"
by(simp add: OclNotEmpty_def)
text‹OclANY›
lemma OclANY_invalid[simp,code_unfold]:"(invalid->any⇩S⇩e⇩t()) = invalid"
by(simp add: bot_fun_def OclANY_def invalid_def defined_def valid_def false_def true_def)
lemma OclANY_null[simp,code_unfold]:"(null->any⇩S⇩e⇩t()) = null"
by(simp add: OclANY_def false_def true_def)
text‹OclForall›
lemma OclForall_invalid[simp,code_unfold]:"invalid->forAll⇩S⇩e⇩t(a| P a) = invalid"
by(simp add: bot_fun_def invalid_def OclForall_def defined_def valid_def false_def true_def)
lemma OclForall_null[simp,code_unfold]:"null->forAll⇩S⇩e⇩t(a | P a) = invalid"
by(simp add: bot_fun_def invalid_def OclForall_def defined_def valid_def false_def true_def)
text‹OclExists›
lemma OclExists_invalid[simp,code_unfold]:"invalid->exists⇩S⇩e⇩t(a| P a) = invalid"
by(simp add: OclExists_def)
lemma OclExists_null[simp,code_unfold]:"null->exists⇩S⇩e⇩t(a | P a) = invalid"
by(simp add: OclExists_def)
text‹OclIterate›
lemma OclIterate_invalid[simp,code_unfold]:"invalid->iterate⇩S⇩e⇩t(a; x = A | P a x) = invalid"
by(simp add: bot_fun_def invalid_def OclIterate_def defined_def valid_def false_def true_def)
lemma OclIterate_null[simp,code_unfold]:"null->iterate⇩S⇩e⇩t(a; x = A | P a x) = invalid"
by(simp add: bot_fun_def invalid_def OclIterate_def defined_def valid_def false_def true_def)
lemma OclIterate_invalid_args[simp,code_unfold]:"S->iterate⇩S⇩e⇩t(a; x = invalid | P a x) = invalid"
by(simp add: bot_fun_def invalid_def OclIterate_def defined_def valid_def false_def true_def)
text‹An open question is this ...›
lemma "S->iterate⇩S⇩e⇩t(a; x = null | P a x) = invalid"
oops
lemma OclIterate_infinite:
assumes non_finite: "τ ⊨ not(δ(S->size⇩S⇩e⇩t()))"
shows "(OclIterate S A F) τ = invalid τ"
apply(insert non_finite [THEN OclSize_infinite])
apply(subst (asm) foundation9, simp)
by(metis OclIterate_def OclValid_def invalid_def)
text‹OclSelect›
lemma OclSelect_invalid[simp,code_unfold]:"invalid->select⇩S⇩e⇩t(a | P a) = invalid"
by(simp add: bot_fun_def invalid_def OclSelect_def defined_def valid_def false_def true_def)
lemma OclSelect_null[simp,code_unfold]:"null->select⇩S⇩e⇩t(a | P a) = invalid"
by(simp add: bot_fun_def invalid_def OclSelect_def defined_def valid_def false_def true_def)
text‹OclReject›
lemma OclReject_invalid[simp,code_unfold]:"invalid->reject⇩S⇩e⇩t(a | P a) = invalid"
by(simp add: OclReject_def)
lemma OclReject_null[simp,code_unfold]:"null->reject⇩S⇩e⇩t(a | P a) = invalid"
by(simp add: OclReject_def)
text_raw‹\isatagafp›
subsubsection‹Context Passing›
lemma cp_OclIncludes1:
"(X->includes⇩S⇩e⇩t(x)) τ = (X->includes⇩S⇩e⇩t(λ _. x τ)) τ"
by(auto simp: OclIncludes_def StrongEq_def invalid_def
cp_defined[symmetric] cp_valid[symmetric])
lemma cp_OclSize: "X->size⇩S⇩e⇩t() τ = ((λ_. X τ)->size⇩S⇩e⇩t()) τ"
by(simp add: OclSize_def cp_defined[symmetric])
lemma cp_OclIsEmpty: "X->isEmpty⇩S⇩e⇩t() τ = ((λ_. X τ)->isEmpty⇩S⇩e⇩t()) τ"
apply(simp only: OclIsEmpty_def)
apply(subst (2) cp_OclOr,
subst cp_OclAnd,
subst cp_OclNot,
subst StrictRefEq⇩I⇩n⇩t⇩e⇩g⇩e⇩r.cp0)
by(simp add: cp_defined[symmetric] cp_valid[symmetric] StrictRefEq⇩I⇩n⇩t⇩e⇩g⇩e⇩r.cp0[symmetric]
cp_OclSize[symmetric] cp_OclNot[symmetric] cp_OclAnd[symmetric] cp_OclOr[symmetric])
lemma cp_OclNotEmpty: "X->notEmpty⇩S⇩e⇩t() τ = ((λ_. X τ)->notEmpty⇩S⇩e⇩t()) τ"
apply(simp only: OclNotEmpty_def)
apply(subst (2) cp_OclNot)
by(simp add: cp_OclNot[symmetric] cp_OclIsEmpty[symmetric])
lemma cp_OclANY: "X->any⇩S⇩e⇩t() τ = ((λ_. X τ)->any⇩S⇩e⇩t()) τ"
apply(simp only: OclANY_def)
apply(subst (2) cp_OclAnd)
by(simp only: cp_OclAnd[symmetric] cp_defined[symmetric] cp_valid[symmetric]
cp_OclNotEmpty[symmetric])
lemma cp_OclForall:
"(S->forAll⇩S⇩e⇩t(x | P x)) τ = ((λ _. S τ)->forAll⇩S⇩e⇩t(x | P (λ _. x τ))) τ"
by(simp add: OclForall_def cp_defined[symmetric])
lemma cp_OclForall1 [simp,intro!]:
"cp S ⟹ cp (λX. ((S X)->forAll⇩S⇩e⇩t(x | P x)))"
apply(simp add: cp_def)
apply(erule exE, rule exI, intro allI)
apply(erule_tac x=X in allE)
by(subst cp_OclForall, simp)
lemma
"cp (λX St x. P (λτ. x) X St) ⟹ cp S ⟹ cp (λX. (S X)->forAll⇩S⇩e⇩t(x|P x X)) "
apply(simp only: cp_def)
oops
lemma
"cp S ⟹
(⋀ x. cp(P x)) ⟹
cp(λX. ((S X)->forAll⇩S⇩e⇩t(x | P x X)))"
oops
lemma cp_OclExists:
"(S->exists⇩S⇩e⇩t(x | P x)) τ = ((λ _. S τ)->exists⇩S⇩e⇩t(x | P (λ _. x τ))) τ"
by(simp add: OclExists_def OclNot_def, subst cp_OclForall, simp)
lemma cp_OclExists1 [simp,intro!]:
"cp S ⟹ cp (λX. ((S X)->exists⇩S⇩e⇩t(x | P x)))"
apply(simp add: cp_def)
apply(erule exE, rule exI, intro allI)
apply(erule_tac x=X in allE)
by(subst cp_OclExists,simp)
lemma cp_OclIterate:
"(X->iterate⇩S⇩e⇩t(a; x = A | P a x)) τ =
((λ _. X τ)->iterate⇩S⇩e⇩t(a; x = A | P a x)) τ"
by(simp add: OclIterate_def cp_defined[symmetric])
lemma cp_OclSelect: "(X->select⇩S⇩e⇩t(a | P a)) τ =
((λ _. X τ)->select⇩S⇩e⇩t(a | P a)) τ"
by(simp add: OclSelect_def cp_defined[symmetric])
lemma cp_OclReject: "(X->reject⇩S⇩e⇩t(a | P a)) τ = ((λ _. X τ)->reject⇩S⇩e⇩t(a | P a)) τ"
by(simp add: OclReject_def, subst cp_OclSelect, simp)
lemmas cp_intro''⇩S⇩e⇩t[intro!,simp,code_unfold] =
cp_OclSize [THEN allI[THEN allI[THEN cpI1], of "OclSize"]]
cp_OclIsEmpty [THEN allI[THEN allI[THEN cpI1], of "OclIsEmpty"]]
cp_OclNotEmpty [THEN allI[THEN allI[THEN cpI1], of "OclNotEmpty"]]
cp_OclANY [THEN allI[THEN allI[THEN cpI1], of "OclANY"]]
subsubsection‹Const›
lemma const_OclIncluding[simp,code_unfold] :
assumes const_x : "const x"
and const_S : "const S"
shows "const (S->including⇩S⇩e⇩t(x))"
proof -
have A:"⋀τ τ'. ¬ (τ ⊨ υ x) ⟹ (S->including⇩S⇩e⇩t(x) τ) = (S->including⇩S⇩e⇩t(x) τ')"
apply(simp add: foundation18)
apply(erule const_subst[OF const_x const_invalid],simp_all)
by(rule const_charn[OF const_invalid])
have B: "⋀ τ τ'. ¬ (τ ⊨ δ S) ⟹ (S->including⇩S⇩e⇩t(x) τ) = (S->including⇩S⇩e⇩t(x) τ')"
apply(simp add: foundation16', elim disjE)
apply(erule const_subst[OF const_S const_invalid],simp_all)
apply(rule const_charn[OF const_invalid])
apply(erule const_subst[OF const_S const_null],simp_all)
by(rule const_charn[OF const_invalid])
show ?thesis
apply(simp only: const_def,intro allI, rename_tac τ τ')
apply(case_tac "¬ (τ ⊨ υ x)", simp add: A)
apply(case_tac "¬ (τ ⊨ δ S)", simp_all add: B)
apply(frule_tac τ'1= τ' in const_OclValid2[OF const_x, THEN iffD1])
apply(frule_tac τ'1= τ' in const_OclValid1[OF const_S, THEN iffD1])
apply(simp add: OclIncluding_def OclValid_def)
apply(subst const_charn[OF const_x])
apply(subst const_charn[OF const_S])
by simp
qed
text_raw‹\endisatagafp›
subsection‹General Algebraic Execution Rules›
subsubsection‹Execution Rules on Including›
lemma OclIncluding_finite_rep_set :
assumes X_def : "τ ⊨ δ X"
and x_val : "τ ⊨ υ x"
shows "finite ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X->including⇩S⇩e⇩t(x) τ)⌉⌉ = finite ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X τ)⌉⌉"
proof -
have C : "⌊⌊insert (x τ) ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X τ)⌉⌉⌋⌋ ∈ {X. X = bot ∨ X = null ∨ (∀x∈⌈⌈X⌉⌉. x ≠ bot)}"
by(insert X_def x_val, frule Set_inv_lemma, simp add: foundation18 invalid_def)
show "?thesis"
by(insert X_def x_val,
auto simp: OclIncluding_def Abs_Set⇩b⇩a⇩s⇩e_inverse[OF C]
dest: foundation13[THEN iffD2, THEN foundation22[THEN iffD1]])
qed
lemma OclIncluding_rep_set:
assumes S_def: "τ ⊨ δ S"
shows "⌈⌈Rep_Set⇩b⇩a⇩s⇩e (S->including⇩S⇩e⇩t(λ_. ⌊⌊x⌋⌋) τ)⌉⌉ = insert ⌊⌊x⌋⌋ ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (S τ)⌉⌉"
apply(simp add: OclIncluding_def S_def[simplified OclValid_def])
apply(subst Abs_Set⇩b⇩a⇩s⇩e_inverse, simp add: bot_option_def null_option_def)
apply(insert Set_inv_lemma[OF S_def], metis bot_option_def not_Some_eq)
by(simp)
lemma OclIncluding_notempty_rep_set:
assumes X_def: "τ ⊨ δ X"
and a_val: "τ ⊨ υ a"
shows "⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X->including⇩S⇩e⇩t(a) τ)⌉⌉ ≠ {}"
apply(simp add: OclIncluding_def X_def[simplified OclValid_def] a_val[simplified OclValid_def])
apply(subst Abs_Set⇩b⇩a⇩s⇩e_inverse, simp add: bot_option_def null_option_def)
apply(insert Set_inv_lemma[OF X_def], metis a_val foundation18')
by(simp)
lemma OclIncluding_includes0:
assumes "τ ⊨ X->includes⇩S⇩e⇩t(x)"
shows "X->including⇩S⇩e⇩t(x) τ = X τ"
proof -
have includes_def: "τ ⊨ X->includes⇩S⇩e⇩t(x) ⟹ τ ⊨ δ X"
by (metis bot_fun_def OclIncludes_def OclValid_def defined3 foundation16)
have includes_val: "τ ⊨ X->includes⇩S⇩e⇩t(x) ⟹ τ ⊨ υ x"
using foundation5 foundation6 by fastforce
show ?thesis
apply(insert includes_def[OF assms] includes_val[OF assms] assms,
simp add: OclIncluding_def OclIncludes_def OclValid_def true_def)
apply(drule insert_absorb, simp, subst abs_rep_simp')
by(simp_all add: OclValid_def true_def)
qed
lemma OclIncluding_includes:
assumes "τ ⊨ X->includes⇩S⇩e⇩t(x)"
shows "τ ⊨ X->including⇩S⇩e⇩t(x) ≜ X"
by(simp add: StrongEq_def OclValid_def true_def OclIncluding_includes0[OF assms])
lemma OclIncluding_commute0 :
assumes S_def : "τ ⊨ δ S"
and i_val : "τ ⊨ υ i"
and j_val : "τ ⊨ υ j"
shows "τ ⊨ ((S :: ('𝔄, 'a::null) Set)->including⇩S⇩e⇩t(i)->including⇩S⇩e⇩t(j) ≜ (S->including⇩S⇩e⇩t(j)->including⇩S⇩e⇩t(i)))"
proof -
have A : "⌊⌊insert (i τ) ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (S τ)⌉⌉⌋⌋ ∈ {X. X = bot ∨ X = null ∨ (∀x∈⌈⌈X⌉⌉. x ≠ bot)}"
by(insert S_def i_val, frule Set_inv_lemma, simp add: foundation18 invalid_def)
have B : "⌊⌊insert (j τ) ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (S τ)⌉⌉⌋⌋ ∈ {X. X = bot ∨ X = null ∨ (∀x∈⌈⌈X⌉⌉. x ≠ bot)}"
by(insert S_def j_val, frule Set_inv_lemma, simp add: foundation18 invalid_def)
have G1 : "Abs_Set⇩b⇩a⇩s⇩e ⌊⌊insert (i τ) ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (S τ)⌉⌉⌋⌋ ≠ Abs_Set⇩b⇩a⇩s⇩e None"
by(insert A, simp add: Abs_Set⇩b⇩a⇩s⇩e_inject bot_option_def null_option_def)
have G2 : "Abs_Set⇩b⇩a⇩s⇩e ⌊⌊insert (i τ) ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (S τ)⌉⌉⌋⌋ ≠ Abs_Set⇩b⇩a⇩s⇩e ⌊None⌋"
by(insert A, simp add: Abs_Set⇩b⇩a⇩s⇩e_inject bot_option_def null_option_def)
have G3 : "Abs_Set⇩b⇩a⇩s⇩e ⌊⌊insert (j τ) ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (S τ)⌉⌉⌋⌋ ≠ Abs_Set⇩b⇩a⇩s⇩e None"
by(insert B, simp add: Abs_Set⇩b⇩a⇩s⇩e_inject bot_option_def null_option_def)
have G4 : "Abs_Set⇩b⇩a⇩s⇩e ⌊⌊insert (j τ) ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (S τ)⌉⌉⌋⌋ ≠ Abs_Set⇩b⇩a⇩s⇩e ⌊None⌋"
by(insert B, simp add: Abs_Set⇩b⇩a⇩s⇩e_inject bot_option_def null_option_def)
have * : "(δ (λ_. Abs_Set⇩b⇩a⇩s⇩e ⌊⌊insert (i τ) ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (S τ)⌉⌉⌋⌋)) τ = ⌊⌊True⌋⌋"
by(auto simp: OclValid_def false_def defined_def null_fun_def true_def
bot_fun_def bot_Set⇩b⇩a⇩s⇩e_def null_Set⇩b⇩a⇩s⇩e_def S_def i_val G1 G2)
have ** : "(δ (λ_. Abs_Set⇩b⇩a⇩s⇩e ⌊⌊insert (j τ) ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (S τ)⌉⌉⌋⌋)) τ = ⌊⌊True⌋⌋"
by(auto simp: OclValid_def false_def defined_def null_fun_def true_def
bot_fun_def bot_Set⇩b⇩a⇩s⇩e_def null_Set⇩b⇩a⇩s⇩e_def S_def i_val G3 G4)
have *** : "Abs_Set⇩b⇩a⇩s⇩e ⌊⌊insert(j τ)⌈⌈Rep_Set⇩b⇩a⇩s⇩e(Abs_Set⇩b⇩a⇩s⇩e⌊⌊insert(i τ)⌈⌈Rep_Set⇩b⇩a⇩s⇩e(S τ)⌉⌉⌋⌋)⌉⌉⌋⌋ =
Abs_Set⇩b⇩a⇩s⇩e ⌊⌊insert(i τ)⌈⌈Rep_Set⇩b⇩a⇩s⇩e(Abs_Set⇩b⇩a⇩s⇩e⌊⌊insert(j τ)⌈⌈Rep_Set⇩b⇩a⇩s⇩e(S τ)⌉⌉⌋⌋)⌉⌉⌋⌋"
by(simp add: Abs_Set⇩b⇩a⇩s⇩e_inverse[OF A] Abs_Set⇩b⇩a⇩s⇩e_inverse[OF B] Set.insert_commute)
show ?thesis
apply(simp add: OclIncluding_def S_def[simplified OclValid_def]
i_val[simplified OclValid_def] j_val[simplified OclValid_def]
true_def OclValid_def StrongEq_def)
apply(subst cp_defined,
simp add: S_def[simplified OclValid_def]
i_val[simplified OclValid_def] j_val[simplified OclValid_def] true_def *)
apply(subst cp_defined,
simp add: S_def[simplified OclValid_def]
i_val[simplified OclValid_def] j_val[simplified OclValid_def] true_def ** ***)
apply(subst cp_defined,
simp add: S_def[simplified OclValid_def]
i_val[simplified OclValid_def] j_val[simplified OclValid_def] true_def *)
apply(subst cp_defined,
simp add: S_def[simplified OclValid_def]
i_val[simplified OclValid_def] j_val[simplified OclValid_def] true_def * )
apply(subst cp_defined,
simp add: S_def[simplified OclValid_def]
i_val[simplified OclValid_def] j_val[simplified OclValid_def] true_def * **)
done
qed
lemma OclIncluding_commute[simp,code_unfold]:
"((S :: ('𝔄, 'a::null) Set)->including⇩S⇩e⇩t(i)->including⇩S⇩e⇩t(j) = (S->including⇩S⇩e⇩t(j)->including⇩S⇩e⇩t(i)))"
proof -
have A: "⋀ τ. τ ⊨ (i ≜ invalid) ⟹ (S->including⇩S⇩e⇩t(i)->including⇩S⇩e⇩t(j)) τ = invalid τ"
apply(rule foundation22[THEN iffD1])
by(erule StrongEq_L_subst2_rev, simp,simp)
have A': "⋀ τ. τ ⊨ (i ≜ invalid) ⟹ (S->including⇩S⇩e⇩t(j)->including⇩S⇩e⇩t(i)) τ = invalid τ"
apply(rule foundation22[THEN iffD1])
by(erule StrongEq_L_subst2_rev, simp,simp)
have B:"⋀ τ. τ ⊨ (j ≜ invalid) ⟹ (S->including⇩S⇩e⇩t(i)->including⇩S⇩e⇩t(j)) τ = invalid τ"
apply(rule foundation22[THEN iffD1])
by(erule StrongEq_L_subst2_rev, simp,simp)
have B':"⋀ τ. τ ⊨ (j ≜ invalid) ⟹ (S->including⇩S⇩e⇩t(j)->including⇩S⇩e⇩t(i)) τ = invalid τ"
apply(rule foundation22[THEN iffD1])
by(erule StrongEq_L_subst2_rev, simp,simp)
have C: "⋀ τ. τ ⊨ (S ≜ invalid) ⟹ (S->including⇩S⇩e⇩t(i)->including⇩S⇩e⇩t(j)) τ = invalid τ"
apply(rule foundation22[THEN iffD1])
by(erule StrongEq_L_subst2_rev, simp,simp)
have C': "⋀ τ. τ ⊨ (S ≜ invalid) ⟹ (S->including⇩S⇩e⇩t(j)->including⇩S⇩e⇩t(i)) τ = invalid τ"
apply(rule foundation22[THEN iffD1])
by(erule StrongEq_L_subst2_rev, simp,simp)
have D: "⋀ τ. τ ⊨ (S ≜ null) ⟹ (S->including⇩S⇩e⇩t(i)->including⇩S⇩e⇩t(j)) τ = invalid τ"
apply(rule foundation22[THEN iffD1])
by(erule StrongEq_L_subst2_rev, simp,simp)
have D': "⋀ τ. τ ⊨ (S ≜ null) ⟹ (S->including⇩S⇩e⇩t(j)->including⇩S⇩e⇩t(i)) τ = invalid τ"
apply(rule foundation22[THEN iffD1])
by(erule StrongEq_L_subst2_rev, simp,simp)
show ?thesis
apply(rule ext, rename_tac τ)
apply(case_tac "τ ⊨ (υ i)")
apply(case_tac "τ ⊨ (υ j)")
apply(case_tac "τ ⊨ (δ S)")
apply(simp only: OclIncluding_commute0[THEN foundation22[THEN iffD1]])
apply(simp add: foundation16', elim disjE)
apply(simp add: C[OF foundation22[THEN iffD2]] C'[OF foundation22[THEN iffD2]])
apply(simp add: D[OF foundation22[THEN iffD2]] D'[OF foundation22[THEN iffD2]])
apply(simp add:foundation18 B[OF foundation22[THEN iffD2]] B'[OF foundation22[THEN iffD2]])
apply(simp add:foundation18 A[OF foundation22[THEN iffD2]] A'[OF foundation22[THEN iffD2]])
done
qed
subsubsection‹Execution Rules on Excluding›
lemma OclExcluding_finite_rep_set :
assumes X_def : "τ ⊨ δ X"
and x_val : "τ ⊨ υ x"
shows "finite ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X->excluding⇩S⇩e⇩t(x) τ)⌉⌉ = finite ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X τ)⌉⌉"
proof -
have C : "⌊⌊⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X τ)⌉⌉ - {x τ}⌋⌋ ∈ {X. X = bot ∨ X = null ∨ (∀x∈⌈⌈X⌉⌉. x ≠ bot)}"
apply(insert X_def x_val, frule Set_inv_lemma)
apply(simp add: foundation18 invalid_def)
done
show "?thesis"
by(insert X_def x_val,
auto simp: OclExcluding_def Abs_Set⇩b⇩a⇩s⇩e_inverse[OF C]
dest: foundation13[THEN iffD2, THEN foundation22[THEN iffD1]])
qed
lemma OclExcluding_rep_set:
assumes S_def: "τ ⊨ δ S"
shows "⌈⌈Rep_Set⇩b⇩a⇩s⇩e (S->excluding⇩S⇩e⇩t(λ_. ⌊⌊x⌋⌋) τ)⌉⌉ = ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (S τ)⌉⌉ - {⌊⌊x⌋⌋}"
apply(simp add: OclExcluding_def S_def[simplified OclValid_def])
apply(subst Abs_Set⇩b⇩a⇩s⇩e_inverse, simp add: bot_option_def null_option_def)
apply(insert Set_inv_lemma[OF S_def], metis Diff_iff bot_option_def not_None_eq)
by(simp)
lemma OclExcluding_excludes0:
assumes "τ ⊨ X->excludes⇩S⇩e⇩t(x)"
shows "X->excluding⇩S⇩e⇩t(x) τ = X τ"
proof -
have excludes_def: "τ