Theory UML_Bag
theory UML_Bag
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 Bag: Operations›
definition "Rep_Bag_base' x = {(x0, y). y < ⌈⌈Rep_Bag⇩b⇩a⇩s⇩e x⌉⌉ x0 }"
definition "Rep_Bag_base x τ = {(x0, y). y < ⌈⌈Rep_Bag⇩b⇩a⇩s⇩e (x τ)⌉⌉ x0 }"
definition "Rep_Set_base x τ = fst ` {(x0, y). y < ⌈⌈Rep_Bag⇩b⇩a⇩s⇩e (x τ)⌉⌉ x0 }"
definition ApproxEq (infixl "≅" 30)
where "X ≅ Y ≡ λ τ. ⌊⌊Rep_Set_base X τ = Rep_Set_base Y τ ⌋⌋"
subsection‹As a Motivation for the (infinite) Type Construction: Type-Extensions as Bags
\label{sec:type-extensions}›
text‹Our notion of typed bag goes beyond the usual notion of a finite executable bag and
is powerful enough to capture \emph{the extension of a type} in UML and OCL. This means
we can have in Featherweight OCL Bags 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 bag of all \emph{defined} values of a type @{term T}
(for which we will introduce the constant @{term T})
\item the bag 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 bag extensions for the base type @{term Integer} as follows:›
definition Integer :: "('𝔄,Integer⇩b⇩a⇩s⇩e) Bag"
where "Integer ≡ (λ τ. (Abs_Bag⇩b⇩a⇩s⇩e o Some o Some) (λ None ⇒ 0 | Some None ⇒ 0 | _ ⇒ 1))"
definition Integer⇩n⇩u⇩l⇩l :: "('𝔄,Integer⇩b⇩a⇩s⇩e) Bag"
where "Integer⇩n⇩u⇩l⇩l ≡ (λ τ. (Abs_Bag⇩b⇩a⇩s⇩e o Some o Some) (λ None ⇒ 0 | _ ⇒ 1))"
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_Bag⇩b⇩a⇩s⇩e_inject bot_option_def bot_Bag⇩b⇩a⇩s⇩e_def null_Bag⇩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_Bag⇩b⇩a⇩s⇩e_inject bot_option_def bot_Bag⇩b⇩a⇩s⇩e_def null_Bag⇩b⇩a⇩s⇩e_def null_option_def)
text‹This allows the theorems:
‹τ ⊨ δ x ⟹ τ ⊨ (Integer->includes⇩B⇩a⇩g(x))›
‹τ ⊨ δ x ⟹ τ ⊨ Integer ≜ (Integer->including⇩B⇩a⇩g(x))›
and
‹τ ⊨ υ x ⟹ τ ⊨ (Integer⇩n⇩u⇩l⇩l->includes⇩B⇩a⇩g(x))›
‹τ ⊨ υ x ⟹ τ ⊨ Integer⇩n⇩u⇩l⇩l ≜ (Integer⇩n⇩u⇩l⇩l->including⇩B⇩a⇩g(x))›
which characterize the infiniteness of these bags by a recursive property on these bags.
›
text‹In the same spirit, we proceed similarly for the remaining base types:›
definition Void⇩n⇩u⇩l⇩l :: "('𝔄,Void⇩b⇩a⇩s⇩e) Bag"
where "Void⇩n⇩u⇩l⇩l ≡ (λ τ. (Abs_Bag⇩b⇩a⇩s⇩e o Some o Some) (λ x. if x = Abs_Void⇩b⇩a⇩s⇩e (Some None) then 1 else 0))"
definition Void⇩e⇩m⇩p⇩t⇩y :: "('𝔄,Void⇩b⇩a⇩s⇩e) Bag"
where "Void⇩e⇩m⇩p⇩t⇩y ≡ (λ τ. (Abs_Bag⇩b⇩a⇩s⇩e o Some o Some) (λ_. 0))"
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_Bag⇩b⇩a⇩s⇩e_def null_Bag⇩b⇩a⇩s⇩e_def)
by((subst (asm) Abs_Bag⇩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_Bag⇩b⇩a⇩s⇩e_def null_Bag⇩b⇩a⇩s⇩e_def)
by((subst (asm) Abs_Bag⇩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) Bag)"
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_Bag⇩b⇩a⇩s⇩e y ⟹
y ∈ {X. X = ⊥ ∨ X = null ∨ ⌈⌈X⌉⌉ ⊥ = 0} ⟹
τ ⊨ 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_Bag⇩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_Bag⇩b⇩a⇩s⇩e_def null_fun_def true_def)
proof - fix a show "V τ = Abs_Bag⇩b⇩a⇩s⇩e ⌊a⌋ ⟹ ⌈a⌉ ⊥ = 0 ⟹ τ ⊨ 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_Bag⇩b⇩a⇩s⇩e_def true_def)
apply(simp)
proof - fix aa show " V τ = Abs_Bag⇩b⇩a⇩s⇩e ⌊⌊aa⌋⌋ ⟹ aa ⊥ = 0 ⟹ τ ⊨ V ≅ Void⇩n⇩u⇩l⇩l ∨ τ ⊨ V ≅ Void⇩e⇩m⇩p⇩t⇩y"
apply(case_tac "aa (Abs_Void⇩b⇩a⇩s⇩e ⌊None⌋) = 0",
rule disjI2,
insert assms,
simp add: Void⇩e⇩m⇩p⇩t⇩y_def OclValid_def ApproxEq_def Rep_Set_base_def true_def Abs_Bag⇩b⇩a⇩s⇩e_inverse image_def)
apply(intro allI)
proof - fix x fix b show " V τ = Abs_Bag⇩b⇩a⇩s⇩e ⌊⌊aa⌋⌋ ⟹ aa ⊥ = 0 ⟹ aa (Abs_Void⇩b⇩a⇩s⇩e ⌊None⌋) = 0 ⟹ (δ V) τ = ⌊⌊True⌋⌋ ⟹ ¬ b < aa x"
apply (case_tac x, auto)
apply (simp add: bot_Void_def bot_option_def)
apply (simp add: bot_option_def null_option_def)
done
apply_end(simp+, rule disjI1)
show "V τ = Abs_Bag⇩b⇩a⇩s⇩e ⌊⌊aa⌋⌋ ⟹ aa ⊥ = 0 ⟹ 0 < aa (Abs_Void⇩b⇩a⇩s⇩e ⌊None⌋) ⟹ τ ⊨ δ V ⟹ τ ⊨ V ≅ Void⇩n⇩u⇩l⇩l"
apply(simp add: Void⇩n⇩u⇩l⇩l_def OclValid_def ApproxEq_def Rep_Set_base_def true_def Abs_Bag⇩b⇩a⇩s⇩e_inverse image_def,
subst Abs_Bag⇩b⇩a⇩s⇩e_inverse, simp)
using bot_Void_def apply auto[1]
apply(simp)
apply(rule equalityI, rule subsetI, simp)
proof - fix x show "V τ = Abs_Bag⇩b⇩a⇩s⇩e ⌊⌊aa⌋⌋ ⟹
aa ⊥ = 0 ⟹ 0 < aa (Abs_Void⇩b⇩a⇩s⇩e ⌊None⌋) ⟹ (δ V) τ = ⌊⌊True⌋⌋ ⟹ ∃b. b < aa x ⟹ x = Abs_Void⇩b⇩a⇩s⇩e ⌊None⌋"
apply( case_tac x, auto)
apply (simp add: bot_Void_def bot_option_def)
by (simp add: bot_option_def null_option_def)
qed ((simp add: bot_Void_def bot_option_def)+, blast)
qed qed qed qed qed
definition Boolean :: "('𝔄,Boolean⇩b⇩a⇩s⇩e) Bag"
where "Boolean ≡ (λ τ. (Abs_Bag⇩b⇩a⇩s⇩e o Some o Some) (λ None ⇒ 0 | Some None ⇒ 0 | _ ⇒ 1))"
definition Boolean⇩n⇩u⇩l⇩l :: "('𝔄,Boolean⇩b⇩a⇩s⇩e) Bag"
where "Boolean⇩n⇩u⇩l⇩l ≡ (λ τ. (Abs_Bag⇩b⇩a⇩s⇩e o Some o Some) (λ None ⇒ 0 | _ ⇒ 1))"
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_Bag⇩b⇩a⇩s⇩e_inject bot_option_def bot_Bag⇩b⇩a⇩s⇩e_def null_Bag⇩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_Bag⇩b⇩a⇩s⇩e_inject bot_option_def bot_Bag⇩b⇩a⇩s⇩e_def null_Bag⇩b⇩a⇩s⇩e_def null_option_def)
definition String :: "('𝔄,String⇩b⇩a⇩s⇩e) Bag"
where "String ≡ (λ τ. (Abs_Bag⇩b⇩a⇩s⇩e o Some o Some) (λ None ⇒ 0 | Some None ⇒ 0 | _ ⇒ 1))"
definition String⇩n⇩u⇩l⇩l :: "('𝔄,String⇩b⇩a⇩s⇩e) Bag"
where "String⇩n⇩u⇩l⇩l ≡ (λ τ. (Abs_Bag⇩b⇩a⇩s⇩e o Some o Some) (λ None ⇒ 0 | _ ⇒ 1))"
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_Bag⇩b⇩a⇩s⇩e_inject bot_option_def bot_Bag⇩b⇩a⇩s⇩e_def null_Bag⇩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_Bag⇩b⇩a⇩s⇩e_inject bot_option_def bot_Bag⇩b⇩a⇩s⇩e_def null_Bag⇩b⇩a⇩s⇩e_def null_option_def)
definition Real :: "('𝔄,Real⇩b⇩a⇩s⇩e) Bag"
where "Real ≡ (λ τ. (Abs_Bag⇩b⇩a⇩s⇩e o Some o Some) (λ None ⇒ 0 | Some None ⇒ 0 | _ ⇒ 1))"
definition Real⇩n⇩u⇩l⇩l :: "('𝔄,Real⇩b⇩a⇩s⇩e) Bag"
where "Real⇩n⇩u⇩l⇩l ≡ (λ τ. (Abs_Bag⇩b⇩a⇩s⇩e o Some o Some) (λ None ⇒ 0 | _ ⇒ 1))"
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_Bag⇩b⇩a⇩s⇩e_inject bot_option_def bot_Bag⇩b⇩a⇩s⇩e_def null_Bag⇩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_Bag⇩b⇩a⇩s⇩e_inject bot_option_def bot_Bag⇩b⇩a⇩s⇩e_def null_Bag⇩b⇩a⇩s⇩e_def null_option_def)
subsection‹Basic Properties of the Bag Type›
text‹Every element in a defined bag is valid.›
lemma Bag_inv_lemma: "τ ⊨ (δ X) ⟹ ⌈⌈Rep_Bag⇩b⇩a⇩s⇩e (X τ)⌉⌉ bot = 0"
apply(insert Rep_Bag⇩b⇩a⇩s⇩e [of "X τ"], simp)
apply(auto simp: OclValid_def defined_def false_def true_def cp_def
bot_fun_def bot_Bag⇩b⇩a⇩s⇩e_def null_Bag⇩b⇩a⇩s⇩e_def null_fun_def
split:if_split_asm)
apply(erule contrapos_pp [of "Rep_Bag⇩b⇩a⇩s⇩e (X τ) = bot"])
apply(subst Abs_Bag⇩b⇩a⇩s⇩e_inject[symmetric], rule Rep_Bag⇩b⇩a⇩s⇩e, simp)
apply(simp add: Rep_Bag⇩b⇩a⇩s⇩e_inverse bot_Bag⇩b⇩a⇩s⇩e_def bot_option_def)
apply(erule contrapos_pp [of "Rep_Bag⇩b⇩a⇩s⇩e (X τ) = null"])
apply(subst Abs_Bag⇩b⇩a⇩s⇩e_inject[symmetric], rule Rep_Bag⇩b⇩a⇩s⇩e, simp)
apply(simp add: Rep_Bag⇩b⇩a⇩s⇩e_inverse null_option_def)
by (simp add: bot_option_def)
lemma Bag_inv_lemma' :
assumes x_def : "τ ⊨ δ X"
and e_mem : "⌈⌈Rep_Bag⇩b⇩a⇩s⇩e (X τ)⌉⌉ e ≥ 1"
shows "τ ⊨ υ (λ_. e)"
apply(case_tac "e = bot", insert assms, drule Bag_inv_lemma, simp)
by (simp add: foundation18')
lemma abs_rep_simp' :
assumes S_all_def : "τ ⊨ δ S"
shows "Abs_Bag⇩b⇩a⇩s⇩e ⌊⌊⌈⌈Rep_Bag⇩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_Bag⇩b⇩a⇩s⇩e_induct[where P = "λS. (if S = ⊥ τ ∨ S = null τ
then false τ else true τ) = true τ ⟶
Abs_Bag⇩b⇩a⇩s⇩e ⌊⌊⌈⌈Rep_Bag⇩b⇩a⇩s⇩e S⌉⌉⌋⌋ = S"]],
rename_tac S')
apply(simp add: Abs_Bag⇩b⇩a⇩s⇩e_inverse discr_eq_false_true)
apply(case_tac S') apply(simp add: bot_fun_def bot_Bag⇩b⇩a⇩s⇩e_def)+
apply(rename_tac S'', case_tac S'') apply(simp add: null_fun_def null_Bag⇩b⇩a⇩s⇩e_def)+
done
qed
lemma invalid_bag_OclNot_defined [simp,code_unfold]:"δ(invalid::('𝔄,'α::null) Bag) = false" by simp
lemma null_bag_OclNot_defined [simp,code_unfold]:"δ(null::('𝔄,'α::null) Bag) = false"
by(simp add: defined_def null_fun_def)
lemma invalid_bag_valid [simp,code_unfold]:"υ(invalid::('𝔄,'α::null) Bag) = false"
by simp
lemma null_bag_valid [simp,code_unfold]:"υ(null::('𝔄,'α::null) Bag) = true"
apply(simp add: valid_def null_fun_def bot_fun_def bot_Bag⇩b⇩a⇩s⇩e_def null_Bag⇩b⇩a⇩s⇩e_def)
apply(subst Abs_Bag⇩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) Bag) Bag›
corresponding exactly to Bag(Bag(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:bag-strict-equality}›
text‹After the part of foundational operations on bags, we detail here equality on bags.
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)Bag,('𝔄,'α::null)Bag] ⇒ ('𝔄)Boolean"
begin
definition StrictRefEq⇩B⇩a⇩g :
"(x::('𝔄,'α::null)Bag) ≐ 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 bags 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⇩B⇩a⇩g : profile_bin⇩S⇩t⇩r⇩o⇩n⇩g⇩E⇩q_⇩v_⇩v "λ x y. (x::('𝔄,'α::null)Bag) ≐ y"
by unfold_locales (auto simp: StrictRefEq⇩B⇩a⇩g)
subsection‹Constants: mtBag›
definition mtBag::"('𝔄,'α::null) Bag" ("Bag{}")
where "Bag{} ≡ (λ τ. Abs_Bag⇩b⇩a⇩s⇩e ⌊⌊λ_. 0::nat⌋⌋ )"
lemma mtBag_defined[simp,code_unfold]:"δ(Bag{}) = true"
apply(rule ext, auto simp: mtBag_def defined_def null_Bag⇩b⇩a⇩s⇩e_def
bot_Bag⇩b⇩a⇩s⇩e_def bot_fun_def null_fun_def)
by(simp_all add: Abs_Bag⇩b⇩a⇩s⇩e_inject bot_option_def null_option_def)
lemma mtBag_valid[simp,code_unfold]:"υ(Bag{}) = true"
apply(rule ext,auto simp: mtBag_def valid_def
bot_Bag⇩b⇩a⇩s⇩e_def bot_fun_def null_fun_def)
by(simp_all add: Abs_Bag⇩b⇩a⇩s⇩e_inject bot_option_def null_option_def)
lemma mtBag_rep_bag: "⌈⌈Rep_Bag⇩b⇩a⇩s⇩e (Bag{} τ)⌉⌉ = (λ _. 0)"
apply(simp add: mtBag_def, subst Abs_Bag⇩b⇩a⇩s⇩e_inverse)
by(simp add: bot_option_def)+
text_raw‹\isatagafp›
lemma [simp,code_unfold]: "const Bag{}"
by(simp add: const_def mtBag_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.›
text_raw‹\endisatagafp›
subsection‹Definition: Including›
definition OclIncluding :: "[('𝔄,'α::null) Bag,('𝔄,'α) val] ⇒ ('𝔄,'α) Bag"
where "OclIncluding x y = (λ τ. if (δ x) τ = true τ ∧ (υ y) τ = true τ
then Abs_Bag⇩b⇩a⇩s⇩e ⌊⌊ ⌈⌈Rep_Bag⇩b⇩a⇩s⇩e(x τ)⌉⌉
((y τ):=⌈⌈Rep_Bag⇩b⇩a⇩s⇩e(x τ)⌉⌉(y τ)+1)
⌋⌋
else invalid τ )"
notation OclIncluding ("_->including⇩B⇩a⇩g'(_')")
interpretation OclIncluding : profile_bin⇩d_⇩v OclIncluding "λx y. Abs_Bag⇩b⇩a⇩s⇩e⌊⌊⌈⌈Rep_Bag⇩b⇩a⇩s⇩e x⌉⌉
(y := ⌈⌈Rep_Bag⇩b⇩a⇩s⇩e x⌉⌉ y + 1)⌋⌋"
proof -
let ?X = "λx y. ⌈⌈Rep_Bag⇩b⇩a⇩s⇩e(x)⌉⌉ ((y):=⌈⌈Rep_Bag⇩b⇩a⇩s⇩e(x)⌉⌉( y )+1)"
show "profile_bin⇩d_⇩v OclIncluding (λx y. Abs_Bag⇩b⇩a⇩s⇩e ⌊⌊ ?X x y ⌋⌋)"
apply unfold_locales
apply(auto simp:OclIncluding_def bot_option_def null_option_def
bot_Bag⇩b⇩a⇩s⇩e_def null_Bag⇩b⇩a⇩s⇩e_def)
by(subst (asm) Abs_Bag⇩b⇩a⇩s⇩e_inject, simp_all,
metis (mono_tags, lifting) Rep_Bag⇩b⇩a⇩s⇩e Rep_Bag⇩b⇩a⇩s⇩e_inverse bot_option_def mem_Collect_eq null_option_def,
simp add: bot_option_def null_option_def)+
qed
syntax
"_OclFinbag" :: "args => ('𝔄,'a::null) Bag" ("Bag{(_)}")
translations
"Bag{x, xs}" == "CONST OclIncluding (Bag{xs}) x"
"Bag{x}" == "CONST OclIncluding (Bag{}) x "
subsection‹Definition: Excluding›
definition OclExcluding :: "[('𝔄,'α::null) Bag,('𝔄,'α) val] ⇒ ('𝔄,'α) Bag"
where "OclExcluding x y = (λ τ. if (δ x) τ = true τ ∧ (υ y) τ = true τ
then Abs_Bag⇩b⇩a⇩s⇩e ⌊⌊ ⌈⌈Rep_Bag⇩b⇩a⇩s⇩e (x τ)⌉⌉ ((y τ):=0::nat) ⌋⌋
else invalid τ )"
notation OclExcluding ("_->excluding⇩B⇩a⇩g'(_')")
interpretation OclExcluding: profile_bin⇩d_⇩v OclExcluding
"λx y. Abs_Bag⇩b⇩a⇩s⇩e ⌊⌊⌈⌈Rep_Bag⇩b⇩a⇩s⇩e(x)⌉⌉(y:=0::nat)⌋⌋"
proof -
show "profile_bin⇩d_⇩v OclExcluding (λx y. Abs_Bag⇩b⇩a⇩s⇩e ⌊⌊⌈⌈Rep_Bag⇩b⇩a⇩s⇩e x⌉⌉(y := 0)⌋⌋)"
apply unfold_locales
apply(auto simp:OclExcluding_def bot_option_def null_option_def
null_Bag⇩b⇩a⇩s⇩e_def bot_Bag⇩b⇩a⇩s⇩e_def)
by(subst (asm) Abs_Bag⇩b⇩a⇩s⇩e_inject,
simp_all add: bot_option_def null_option_def,
metis (mono_tags, lifting) Rep_Bag⇩b⇩a⇩s⇩e Rep_Bag⇩b⇩a⇩s⇩e_inverse bot_option_def
mem_Collect_eq null_option_def)+
qed
subsection‹Definition: Includes›
definition OclIncludes :: "[('𝔄,'α::null) Bag,('𝔄,'α) val] ⇒ '𝔄 Boolean"
where "OclIncludes x y = (λ τ. if (δ x) τ = true τ ∧ (υ y) τ = true τ
then ⌊⌊ ⌈⌈Rep_Bag⇩b⇩a⇩s⇩e (x τ)⌉⌉ (y τ) > 0 ⌋⌋
else ⊥ )"
notation OclIncludes ("_->includes⇩B⇩a⇩g'(_')" )
interpretation OclIncludes : profile_bin⇩d_⇩v OclIncludes "λx y. ⌊⌊ ⌈⌈Rep_Bag⇩b⇩a⇩s⇩e x⌉⌉ y > 0 ⌋⌋"
by(unfold_locales, auto simp:OclIncludes_def bot_option_def null_option_def invalid_def)
subsection‹Definition: Excludes›
definition OclExcludes :: "[('𝔄,'α::null) Bag,('𝔄,'α) val] ⇒ '𝔄 Boolean"
where "OclExcludes x y = (not(OclIncludes x y))"
notation OclExcludes ("_->excludes⇩B⇩a⇩g'(_')" )
text‹The case of the size definition is somewhat special, we admit
explicitly in Featherweight OCL the possibility of infinite bags. For
the size definition, this requires an extra condition that assures
that the cardinality of the bag is actually a defined integer.›
interpretation OclExcludes : profile_bin⇩d_⇩v OclExcludes "λx y. ⌊⌊ ⌈⌈Rep_Bag⇩b⇩a⇩s⇩e x⌉⌉ y ≤ 0 ⌋⌋"
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)Bag ⇒ '𝔄 Integer"
where "OclSize x = (λ τ. if (δ x) τ = true τ ∧ finite (Rep_Bag_base x τ)
then ⌊⌊ int (card (Rep_Bag_base x τ)) ⌋⌋
else ⊥ )"
notation
OclSize ("_->size⇩B⇩a⇩g'(')" )
text‹The following definition follows the requirement of the
standard to treat null as neutral element of bags. 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) Bag ⇒ '𝔄 Boolean"
where "OclIsEmpty x = ((υ x and not (δ x)) or ((OclSize x) ≐ 𝟬))"
notation OclIsEmpty ("_->isEmpty⇩B⇩a⇩g'(')" )
subsection‹Definition: NotEmpty›
definition OclNotEmpty :: "('𝔄,'α::null) Bag ⇒ '𝔄 Boolean"
where "OclNotEmpty x = not(OclIsEmpty x)"
notation OclNotEmpty ("_->notEmpty⇩B⇩a⇩g'(')" )
subsection‹Definition: Any›
definition OclANY :: "[('𝔄,'α::null) Bag] ⇒ ('𝔄,'α) val"
where "OclANY x = (λ τ. if (υ x) τ = true τ
then if (δ x and OclNotEmpty x) τ = true τ
then SOME y. y ∈ (Rep_Set_base x τ)
else null τ
else ⊥ )"
notation OclANY ("_->any⇩B⇩a⇩g'(')")
subsection‹Definition: Forall›
text‹The definition of OclForall mimics the one of @{term "OclAnd"}:
OclForall is not a strict operation.›
definition OclForall :: "[('𝔄,'α::null)Bag,('𝔄,'α)val⇒('𝔄)Boolean] ⇒ '𝔄 Boolean"
where "OclForall S P = (λ τ. if (δ S) τ = true τ
then if (∃x∈Rep_Set_base S τ. P (λ_. x) τ = false τ)
then false τ
else if (∃x∈Rep_Set_base S τ. P (λ_. x) τ = invalid τ)
then invalid τ
else if (∃x∈Rep_Set_base S τ. P (λ_. x) τ = null τ)
then null τ
else true τ
else ⊥)"
syntax
"_OclForallBag" :: "[('𝔄,'α::null) Bag,id,('𝔄)Boolean] ⇒ '𝔄 Boolean" ("(_)->forAll⇩B⇩a⇩g'(_|_')")
translations
"X->forAll⇩B⇩a⇩g(x | P)" == "CONST UML_Bag.OclForall X (%x. P)"
subsection‹Definition: Exists›
text‹Like OclForall, OclExists is also not strict.›
definition OclExists :: "[('𝔄,'α::null) Bag,('𝔄,'α)val⇒('𝔄)Boolean] ⇒ '𝔄 Boolean"
where "OclExists S P = not(UML_Bag.OclForall S (λ X. not (P X)))"
syntax
"_OclExistBag" :: "[('𝔄,'α::null) Bag,id,('𝔄)Boolean] ⇒ '𝔄 Boolean" ("(_)->exists⇩B⇩a⇩g'(_|_')")
translations
"X->exists⇩B⇩a⇩g(x | P)" == "CONST UML_Bag.OclExists X (%x. P)"
subsection‹Definition: Iterate›
definition OclIterate :: "[('𝔄,'α::null) Bag,('𝔄,'β::null)val,
('𝔄,'α)val⇒('𝔄,'β)val⇒('𝔄,'β)val] ⇒ ('𝔄,'β)val"
where "OclIterate S A F = (λ τ. if (δ S) τ = true τ ∧ (υ A) τ = true τ ∧ finite (Rep_Bag_base S τ)
then Finite_Set.fold (F o (λa τ. a) o fst) A (Rep_Bag_base S τ) τ
else ⊥)"
syntax
"_OclIterateBag" :: "[('𝔄,'α::null) Bag, idt, idt, 'α, 'β] => ('𝔄,'γ)val"
("_ ->iterate⇩B⇩a⇩g'(_;_=_ | _')" )
translations
"X->iterate⇩B⇩a⇩g(a; x = A | P)" == "CONST OclIterate X A (%a. (% x. P))"
subsection‹Definition: Select›
definition OclSelect :: "[('𝔄,'α::null)Bag,('𝔄,'α)val⇒('𝔄)Boolean] ⇒ ('𝔄,'α)Bag"
where "OclSelect S P = (λτ. if (δ S) τ = true τ
then if (∃x∈Rep_Set_base S τ. P(λ _. x) τ = invalid τ)
then invalid τ
else Abs_Bag⇩b⇩a⇩s⇩e ⌊⌊λx.
let n = ⌈⌈ Rep_Bag⇩b⇩a⇩s⇩e (S τ) ⌉⌉ x in
if n = 0 | P (λ_. x) τ = false τ then
0
else
n⌋⌋
else invalid τ)"
syntax
"_OclSelectBag" :: "[('𝔄,'α::null) Bag,id,('𝔄)Boolean] ⇒ '𝔄 Boolean" ("(_)->select⇩B⇩a⇩g'(_|_')")
translations
"X->select⇩B⇩a⇩g(x | P)" == "CONST OclSelect X (% x. P)"
subsection‹Definition: Reject›
definition OclReject :: "[('𝔄,'α::null)Bag,('𝔄,'α)val⇒('𝔄)Boolean] ⇒ ('𝔄,'α::null)Bag"
where "OclReject S P = OclSelect S (not o P)"
syntax
"_OclRejectBag" :: "[('𝔄,'α::null) Bag,id,('𝔄)Boolean] ⇒ '𝔄 Boolean" ("(_)->reject⇩B⇩a⇩g'(_|_')")
translations
"X->reject⇩B⇩a⇩g(x | P)" == "CONST OclReject X (% x. P)"
subsection‹Definition: IncludesAll›
definition OclIncludesAll :: "[('𝔄,'α::null) Bag,('𝔄,'α) Bag] ⇒ '𝔄 Boolean"
where "OclIncludesAll x y = (λ τ. if (δ x) τ = true τ ∧ (δ y) τ = true τ
then ⌊⌊Rep_Bag_base y τ ⊆ Rep_Bag_base x τ ⌋⌋
else ⊥ )"
notation OclIncludesAll ("_->includesAll⇩B⇩a⇩g'(_')" )
interpretation OclIncludesAll : profile_bin⇩d_⇩d OclIncludesAll "λx y. ⌊⌊Rep_Bag_base' y ⊆ Rep_Bag_base' x ⌋⌋"
by(unfold_locales, auto simp:OclIncludesAll_def bot_option_def null_option_def invalid_def
Rep_Bag_base_def Rep_Bag_base'_def)
subsection‹Definition: ExcludesAll›
definition OclExcludesAll :: "[('𝔄,'α::null) Bag,('𝔄,'α) Bag] ⇒ '𝔄 Boolean"
where "OclExcludesAll x y = (λ τ. if (δ x) τ = true τ ∧ (δ y) τ = true τ
then ⌊⌊Rep_Bag_base y τ ∩ Rep_Bag_base x τ = {} ⌋⌋
else ⊥ )"
notation OclExcludesAll ("_->excludesAll⇩B⇩a⇩g'(_')" )
interpretation OclExcludesAll : profile_bin⇩d_⇩d OclExcludesAll "λx y. ⌊⌊Rep_Bag_base' y ∩ Rep_Bag_base' x = {} ⌋⌋"
by(unfold_locales, auto simp:OclExcludesAll_def bot_option_def null_option_def invalid_def
Rep_Bag_base_def Rep_Bag_base'_def)
subsection‹Definition: Union›
definition OclUnion :: "[('𝔄,'α::null) Bag,('𝔄,'α) Bag] ⇒ ('𝔄,'α) Bag"
where "OclUnion x y = (λ τ. if (δ x) τ = true τ ∧ (δ y) τ = true τ
then Abs_Bag⇩b⇩a⇩s⇩e ⌊⌊ λ X. ⌈⌈Rep_Bag⇩b⇩a⇩s⇩e (x τ)⌉⌉ X +
⌈⌈Rep_Bag⇩b⇩a⇩s⇩e (y τ)⌉⌉ X⌋⌋
else invalid τ )"
notation OclUnion ("_->union⇩B⇩a⇩g'(_')" )
interpretation OclUnion :
profile_bin⇩d_⇩d OclUnion "λx y. Abs_Bag⇩b⇩a⇩s⇩e ⌊⌊ λ X. ⌈⌈Rep_Bag⇩b⇩a⇩s⇩e x⌉⌉ X +
⌈⌈Rep_Bag⇩b⇩a⇩s⇩e y⌉⌉ X⌋⌋"
proof -
show "profile_bin⇩d_⇩d OclUnion (λx y. Abs_Bag⇩b⇩a⇩s⇩e ⌊⌊ λ X. ⌈⌈Rep_Bag⇩b⇩a⇩s⇩e x⌉⌉ X + ⌈⌈Rep_Bag⇩b⇩a⇩s⇩e y⌉⌉ X⌋⌋)"
apply unfold_locales
apply(auto simp:OclUnion_def bot_option_def null_option_def
null_Bag⇩b⇩a⇩s⇩e_def bot_Bag⇩b⇩a⇩s⇩e_def)
by(subst (asm) Abs_Bag⇩b⇩a⇩s⇩e_inject,
simp_all add: bot_option_def null_option_def,
metis (mono_tags, lifting) Rep_Bag⇩b⇩a⇩s⇩e Rep_Bag⇩b⇩a⇩s⇩e_inverse bot_option_def mem_Collect_eq
null_option_def)+
qed
subsection‹Definition: Intersection›
definition OclIntersection :: "[('𝔄,'α::null) Bag,('𝔄,'α) Bag] ⇒ ('𝔄,'α) Bag"
where "OclIntersection x y = (λ τ. if (δ x) τ = true τ ∧ (δ y) τ = true τ
then Abs_Bag⇩b⇩a⇩s⇩e⌊⌊ λ X. min (⌈⌈Rep_Bag⇩b⇩a⇩s⇩e (x τ)⌉⌉ X)
(⌈⌈Rep_Bag⇩b⇩a⇩s⇩e (y τ)⌉⌉ X)⌋⌋
else ⊥ )"
notation OclIntersection("_->intersection⇩B⇩a⇩g'(_')" )
interpretation OclIntersection :
profile_bin⇩d_⇩d OclIntersection "λx y. Abs_Bag⇩b⇩a⇩s⇩e ⌊⌊ λ X. min (⌈⌈Rep_Bag⇩b⇩a⇩s⇩e x⌉⌉ X)
(⌈⌈Rep_Bag⇩b⇩a⇩s⇩e y⌉⌉ X)⌋⌋"
proof -
show "profile_bin⇩d_⇩d OclIntersection (λx y. Abs_Bag⇩b⇩a⇩s⇩e ⌊⌊ λ X. min (⌈⌈Rep_Bag⇩b⇩a⇩s⇩e x⌉⌉ X)
(⌈⌈Rep_Bag⇩b⇩a⇩s⇩e y⌉⌉ X)⌋⌋)"
apply unfold_locales
apply(auto simp:OclIntersection_def bot_option_def null_option_def
null_Bag⇩b⇩a⇩s⇩e_def bot_Bag⇩b⇩a⇩s⇩e_def invalid_def)
by(subst (asm) Abs_Bag⇩b⇩a⇩s⇩e_inject,
simp_all add: bot_option_def null_option_def,
metis (mono_tags, lifting) Rep_Bag⇩b⇩a⇩s⇩e Rep_Bag⇩b⇩a⇩s⇩e_inverse bot_option_def mem_Collect_eq min_0R
null_option_def)+
qed
subsection‹Definition: Count›
definition OclCount :: "[('𝔄,'α::null) Bag,('𝔄,'α) val] ⇒ ('𝔄) Integer"
where "OclCount x y = (λ τ. if (δ x) τ = true τ ∧ (δ y) τ = true τ
then ⌊⌊int(⌈⌈Rep_Bag⇩b⇩a⇩s⇩e (x τ)⌉⌉ (y τ))⌋⌋
else invalid τ )"
notation OclCount ("_->count⇩B⇩a⇩g'(_')" )
interpretation OclCount : profile_bin⇩d_⇩d OclCount "λx y. ⌊⌊int(⌈⌈Rep_Bag⇩b⇩a⇩s⇩e x⌉⌉ y)⌋⌋"
by(unfold_locales, auto simp:OclCount_def bot_option_def null_option_def)
subsection‹Definition (future operators)›
consts
OclSum :: " ('𝔄,'α::null) Bag ⇒ '𝔄 Integer"
notation OclSum ("_->sum⇩B⇩a⇩g'(')" )
subsection‹Logical Properties›
text‹OclIncluding›
lemma OclIncluding_valid_args_valid:
"(τ ⊨ υ(X->including⇩B⇩a⇩g(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⇩B⇩a⇩g(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⇩B⇩a⇩g(x))) = ((τ ⊨(δ X)) ∧ (τ ⊨(υ x)))"
by (metis OclExcluding.def_valid_then_def OclExcluding.defined_args_valid)
lemma OclExcluding_valid_args_valid''[simp,code_unfold]:
"υ(X->excluding⇩B⇩a⇩g(x)) = ((δ X) and (υ x))"
by (simp add: OclExcluding.def_valid_then_def)
text‹OclIncludes›
lemma OclIncludes_valid_args_valid:
"(τ ⊨ υ(X->includes⇩B⇩a⇩g(x))) = ((τ ⊨(δ X)) ∧ (τ ⊨(υ x)))"
by (simp add: OclIncludes.def_valid_then_def foundation10')
lemma OclIncludes_valid_args_valid''[simp,code_unfold]:
"υ(X->includes⇩B⇩a⇩g(x)) = ((δ X) and (υ x))"
by (simp add: OclIncludes.def_valid_then_def)
text‹OclExcludes›
lemma OclExcludes_valid_args_valid:
"(τ ⊨ υ(X->excludes⇩B⇩a⇩g(x))) = ((τ ⊨(δ X)) ∧ (τ ⊨(υ x)))"
by (simp add: OclExcludes.def_valid_then_def foundation10')
lemma OclExcludes_valid_args_valid''[simp,code_unfold]:
"υ(X->excludes⇩B⇩a⇩g(x)) = ((δ X) and (υ x))"
by (simp add: OclExcludes.def_valid_then_def)
text‹OclSize›
lemma OclSize_defined_args_valid: "τ ⊨ δ (X->size⇩B⇩a⇩g()) ⟹ τ ⊨ δ 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⇩B⇩a⇩g()))"
shows "(τ ⊨ not(δ(S))) ∨ ¬ finite (Rep_Bag_base S τ)"
apply(insert non_finite, simp)
apply(rule impI)
apply(simp add: OclSize_def OclValid_def defined_def bot_fun_def null_fun_def bot_option_def null_option_def
split: if_split_asm)
done
lemma "τ ⊨ δ X ⟹ ¬ finite (Rep_Bag_base X τ) ⟹ ¬ τ ⊨ δ (X->size⇩B⇩a⇩g())"
by(simp add: OclSize_def OclValid_def defined_def bot_fun_def false_def true_def)
lemma size_defined:
assumes X_finite: "⋀τ. finite (Rep_Bag_base X τ)"
shows "δ (X->size⇩B⇩a⇩g()) = δ X"
apply(rule ext, simp add: cp_defined[of "X->size⇩B⇩a⇩g()"] 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_Bag_base X τ)"
shows "(τ ⊨ δ (X->size⇩B⇩a⇩g())) = (τ ⊨ δ X)"
apply(simp add: cp_defined[of "X->size⇩B⇩a⇩g()"] 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⇩B⇩a⇩g()) ⟹ τ ⊨ υ 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⇩B⇩a⇩g() ≐ 𝟬) τ", 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⇩B⇩a⇩g())"
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_Bag_base X τ) ⟹ ¬ τ ⊨ δ (X->isEmpty⇩B⇩a⇩g())"
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⇩B⇩a⇩g() ≐ 𝟬) τ", 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⇩B⇩a⇩g()) ⟹ τ ⊨ υ X"
by (metis (opaque_lifting, no_types) OclNotEmpty_def OclNot_defargs OclNot_not foundation6 foundation9
OclIsEmpty_defined_args_valid)
lemma "τ ⊨ δ (null->notEmpty⇩B⇩a⇩g())"
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_Bag_base X τ) ⟹ ¬ τ ⊨ δ (X->notEmpty⇩B⇩a⇩g())"
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⇩B⇩a⇩g() ⟹
∃e. e ∈ (Rep_Bag_base X τ)"
proof -
have s_non_empty: "⋀S. S ≠ {} ⟹ ∃x. x ∈ S"
by blast
show "τ ⊨ δ X ⟹
τ ⊨ X->notEmpty⇩B⇩a⇩g() ⟹
?thesis"
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)
apply(drule s_non_empty[of "Rep_Bag_base X τ"], erule exE, case_tac x)
by blast
qed
lemma OclNotEmpty_has_elt' : "τ ⊨ δ X ⟹
τ ⊨ X->notEmpty⇩B⇩a⇩g() ⟹
∃e. e ∈ (Rep_Set_base X τ)"
apply(drule OclNotEmpty_has_elt, simp)
by(simp add: Rep_Bag_base_def Rep_Set_base_def image_def)
text‹OclANY›
lemma OclANY_defined_args_valid: "τ ⊨ δ (X->any⇩B⇩a⇩g()) ⟹ τ ⊨ δ 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⇩B⇩a⇩g() ⟹ ¬ τ ⊨ δ (X->any⇩B⇩a⇩g())"
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⇩B⇩a⇩g())) = (τ ⊨ υ X)"
proof -
have A: "(τ ⊨ υ(X->any⇩B⇩a⇩g())) ⟹ ((τ ⊨(υ 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⇩B⇩a⇩g()))"
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 Bag_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)
apply(erule exE,
rule someI2[where Q = "λx. x ≠ ⊥" and P = "λy. y ∈ (Rep_Set_base X τ)",
simplified not_def, THEN mp], simp, auto)
by(simp add: Rep_Set_base_def image_def)
show ?thesis by(auto dest:A intro:B)
qed
lemma OclANY_valid_args_valid''[simp,code_unfold]:
"υ(X->any⇩B⇩a⇩g()) = (υ 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⇩B⇩a⇩g()) = 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⇩B⇩a⇩g()) = 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⇩B⇩a⇩g()) = invalid"
by(simp add: OclIsEmpty_def)
lemma OclIsEmpty_null[simp,code_unfold]:"(null->isEmpty⇩B⇩a⇩g()) = true"
by(simp add: OclIsEmpty_def)
text‹OclNotEmpty›
lemma OclNotEmpty_invalid[simp,code_unfold]:"(invalid->notEmpty⇩B⇩a⇩g()) = invalid"
by(simp add: OclNotEmpty_def)
lemma OclNotEmpty_null[simp,code_unfold]:"(null->notEmpty⇩B⇩a⇩g()) = false"
by(simp add: OclNotEmpty_def)
text‹OclANY›
lemma OclANY_invalid[simp,code_unfold]:"(invalid->any⇩B⇩a⇩g()) = 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⇩B⇩a⇩g()) = null"
by(simp add: OclANY_def false_def true_def)
text‹OclForall›
lemma OclForall_invalid[simp,code_unfold]:"invalid->forAll⇩B⇩a⇩g(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⇩B⇩a⇩g(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⇩B⇩a⇩g(a| P a) = invalid"
by(simp add: OclExists_def)
lemma OclExists_null[simp,code_unfold]:"null->exists⇩B⇩a⇩g(a | P a) = invalid"
by(simp add: OclExists_def)
text‹OclIterate›
lemma OclIterate_invalid[simp,code_unfold]:"invalid->iterate⇩B⇩a⇩g(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⇩B⇩a⇩g(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⇩B⇩a⇩g(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⇩B⇩a⇩g(a; x = null | P a x) = invalid"
oops
lemma OclIterate_infinite:
assumes non_finite: "τ ⊨ not(δ(S->size⇩B⇩a⇩g()))"
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⇩B⇩a⇩g(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⇩B⇩a⇩g(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⇩B⇩a⇩g(a | P a) = invalid"
by(simp add: OclReject_def)
lemma OclReject_null[simp,code_unfold]:"null->reject⇩B⇩a⇩g(a | P a) = invalid"
by(simp add: OclReject_def)
text_raw‹\isatagafp›
subsubsection‹Context Passing›
lemma cp_OclIncludes1:
"(X->includes⇩B⇩a⇩g(x)) τ = (X->includes⇩B⇩a⇩g(λ _. x τ)) τ"
by(auto simp: OclIncludes_def StrongEq_def invalid_def
cp_defined[symmetric] cp_valid[symmetric])
lemma cp_OclSize: "X->size⇩B⇩a⇩g() τ = ((λ_. X τ)->size⇩B⇩a⇩g()) τ"
by(simp add: OclSize_def cp_defined[symmetric] Rep_Bag_base_def)
lemma cp_OclIsEmpty: "X->isEmpty⇩B⇩a⇩g() τ = ((λ_. X τ)->isEmpty⇩B⇩a⇩g()) τ"
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⇩B⇩a⇩g() τ = ((λ_. X τ)->notEmpty⇩B⇩a⇩g()) τ"
apply(simp only: OclNotEmpty_def)
apply(subst (2) cp_OclNot)
by(simp add: cp_OclNot[symmetric] cp_OclIsEmpty[symmetric])
lemma cp_OclANY: "X->any⇩B⇩a⇩g() τ = ((λ_. X τ)->any⇩B⇩a⇩g()) τ"
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] Rep_Set_base_def)
lemma cp_OclForall:
"(S->forAll⇩B⇩a⇩g(x | P x)) τ = ((λ _. S τ)->forAll⇩B⇩a⇩g(x | P (λ _. x τ))) τ"
by(auto simp add: OclForall_def cp_defined[symmetric] Rep_Set_base_def)
lemma cp_OclForall1 [simp,intro!]:
"cp S ⟹ cp (λX. ((S X)->forAll⇩B⇩a⇩g(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⇩B⇩a⇩g(x|P x X)) "
apply(simp only: cp_def)
oops
lemma
"cp S ⟹
(⋀ x. cp(P x)) ⟹
cp(λX. ((S X)->forAll⇩B⇩a⇩g(x | P x X)))"
oops
lemma cp_OclExists:
"(S->exists⇩B⇩a⇩g(x | P x)) τ = ((λ _. S τ)->exists⇩B⇩a⇩g(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⇩B⇩a⇩g(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⇩B⇩a⇩g(a; x = A | P a x)) τ =
((λ _. X τ)->iterate⇩B⇩a⇩g(a; x = A | P a x)) τ"
by(simp add: OclIterate_def cp_defined[symmetric] Rep_Bag_base_def)
lemma cp_OclSelect: "(X->select⇩B⇩a⇩g(a | P a)) τ =
((λ _. X τ)->select⇩B⇩a⇩g(a | P a)) τ"
by(simp add: OclSelect_def cp_defined[symmetric] Rep_Set_base_def)
lemma cp_OclReject: "(X->reject⇩B⇩a⇩g(a | P a)) τ = ((λ _. X τ)->reject⇩B⇩a⇩g(a | P a)) τ"
by(simp add: OclReject_def, subst cp_OclSelect, simp)
lemmas cp_intro''⇩B⇩a⇩g[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⇩B⇩a⇩g(x))"
proof -
have A:"⋀τ τ'. ¬ (τ ⊨ υ x) ⟹ (S->including⇩B⇩a⇩g(x) τ) = (S->including⇩B⇩a⇩g(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⇩B⇩a⇩g(x) τ) = (S->including⇩B⇩a⇩g(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 (1 2) const_charn[OF const_x])
apply(subst (1 2) const_charn[OF const_S])
by simp
qed
text_raw‹\endisatagafp›
subsection‹Test Statements›
instantiation Bag⇩b⇩a⇩s⇩e :: (equal)equal
begin
definition "HOL.equal k l ⟷ (k::('a::equal)Bag⇩b⇩a⇩s⇩e) = l"
instance by standard (rule equal_Bag⇩b⇩a⇩s⇩e_def)
end
lemma equal_Bag⇩b⇩a⇩s⇩e_code [code]:
"HOL.equal k (l::('a::{equal,null})Bag⇩b⇩a⇩s⇩e) ⟷ Rep_Bag⇩b⇩a⇩s⇩e k = Rep_Bag⇩b⇩a⇩s⇩e l"
by (auto simp add: equal Bag⇩b⇩a⇩s⇩e.Rep_Bag⇩b⇩a⇩s⇩e_inject)
Assert "τ ⊨ (Bag{} ≐ Bag{})"
end