Theory UML_Sequence
theory UML_Sequence
imports "../basic_types/UML_Boolean"
"../basic_types/UML_Integer"
begin
no_notation None (‹⊥›)
section‹Collection Type Sequence: Operations›
subsection‹Basic Properties of the Sequence Type›
text‹Every element in a defined sequence is valid.›
lemma Sequence_inv_lemma: "τ ⊨ (δ X) ⟹ ∀x∈set ⌈⌈Rep_Sequence⇩b⇩a⇩s⇩e (X τ)⌉⌉. x ≠ bot"
apply(insert Rep_Sequence⇩b⇩a⇩s⇩e [of "X τ"], simp)
apply(auto simp: OclValid_def defined_def false_def true_def cp_def
bot_fun_def bot_Sequence⇩b⇩a⇩s⇩e_def null_Sequence⇩b⇩a⇩s⇩e_def null_fun_def
split:if_split_asm)
apply(erule contrapos_pp [of "Rep_Sequence⇩b⇩a⇩s⇩e (X τ) = bot"])
apply(subst Abs_Sequence⇩b⇩a⇩s⇩e_inject[symmetric], rule Rep_Sequence⇩b⇩a⇩s⇩e, simp)
apply(simp add: Rep_Sequence⇩b⇩a⇩s⇩e_inverse bot_Sequence⇩b⇩a⇩s⇩e_def bot_option_def)
apply(erule contrapos_pp [of "Rep_Sequence⇩b⇩a⇩s⇩e (X τ) = null"])
apply(subst Abs_Sequence⇩b⇩a⇩s⇩e_inject[symmetric], rule Rep_Sequence⇩b⇩a⇩s⇩e, simp)
apply(simp add: Rep_Sequence⇩b⇩a⇩s⇩e_inverse null_option_def)
by (simp add: bot_option_def)
subsection‹Definition: Strict Equality \label{sec:seq-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)Sequence,('𝔄,'α::null)Sequence] ⇒ ('𝔄)Boolean"
begin
definition StrictRefEq⇩S⇩e⇩q :
"((x::('𝔄,'α::null)Sequence) ≐ y) ≡ (λ τ. if (υ x) τ = true τ ∧ (υ y) τ = true τ
then (x ≜ y)τ
else invalid τ)"
end
text_raw‹\isatagafp›
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 sequences in the sense above---coincides.›
text_raw‹\endisatagafp›
text‹Property proof in terms of @{term "profile_bin⇩S⇩t⇩r⇩o⇩n⇩g⇩E⇩q_⇩v_⇩v"}›
interpretation StrictRefEq⇩S⇩e⇩q : profile_bin⇩S⇩t⇩r⇩o⇩n⇩g⇩E⇩q_⇩v_⇩v "λ x y. (x::('𝔄,'α::null)Sequence) ≐ y"
by unfold_locales (auto simp: StrictRefEq⇩S⇩e⇩q)
subsection‹Constants: mtSequence›
definition mtSequence ::"('𝔄,'α::null) Sequence" (‹Sequence{}›)
where "Sequence{} ≡ (λ τ. Abs_Sequence⇩b⇩a⇩s⇩e ⌊⌊[]::'α list⌋⌋ )"
lemma mtSequence_defined[simp,code_unfold]:"δ(Sequence{}) = true"
apply(rule ext, auto simp: mtSequence_def defined_def null_Sequence⇩b⇩a⇩s⇩e_def
bot_Sequence⇩b⇩a⇩s⇩e_def bot_fun_def null_fun_def)
by(simp_all add: Abs_Sequence⇩b⇩a⇩s⇩e_inject bot_option_def null_option_def)
lemma mtSequence_valid[simp,code_unfold]:"υ(Sequence{}) = true"
apply(rule ext,auto simp: mtSequence_def valid_def null_Sequence⇩b⇩a⇩s⇩e_def
bot_Sequence⇩b⇩a⇩s⇩e_def bot_fun_def null_fun_def)
by(simp_all add: Abs_Sequence⇩b⇩a⇩s⇩e_inject bot_option_def null_option_def)
lemma mtSequence_rep_set: "⌈⌈Rep_Sequence⇩b⇩a⇩s⇩e (Sequence{} τ)⌉⌉ = []"
apply(simp add: mtSequence_def, subst Abs_Sequence⇩b⇩a⇩s⇩e_inverse)
by(simp add: bot_option_def)+
text_raw‹\isatagafp›
lemma [simp,code_unfold]: "const Sequence{}"
by(simp add: const_def mtSequence_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: Prepend›
definition OclPrepend :: "[('𝔄,'α::null) Sequence,('𝔄,'α) val] ⇒ ('𝔄,'α) Sequence"
where "OclPrepend x y = (λ τ. if (δ x) τ = true τ ∧ (υ y) τ = true τ
then Abs_Sequence⇩b⇩a⇩s⇩e ⌊⌊ (y τ)#⌈⌈Rep_Sequence⇩b⇩a⇩s⇩e (x τ)⌉⌉ ⌋⌋
else invalid τ )"
notation OclPrepend (‹_->prepend⇩S⇩e⇩q'(_')›)
interpretation OclPrepend:profile_bin⇩d_⇩v OclPrepend "λx y. Abs_Sequence⇩b⇩a⇩s⇩e⌊⌊y#⌈⌈Rep_Sequence⇩b⇩a⇩s⇩e x⌉⌉⌋⌋"
proof -
have A : "⋀x y. x ≠ bot ⟹ x ≠ null ⟹ y ≠ bot ⟹
⌊⌊y#⌈⌈Rep_Sequence⇩b⇩a⇩s⇩e x⌉⌉⌋⌋ ∈ {X. X = bot ∨ X = null ∨ (∀x∈set ⌈⌈X⌉⌉. x ≠ bot)}"
by(auto intro!:Sequence_inv_lemma[simplified OclValid_def
defined_def false_def true_def null_fun_def bot_fun_def])
show "profile_bin⇩d_⇩v OclPrepend (λx y. Abs_Sequence⇩b⇩a⇩s⇩e ⌊⌊y#⌈⌈Rep_Sequence⇩b⇩a⇩s⇩e x⌉⌉⌋⌋)"
apply unfold_locales
apply(auto simp:OclPrepend_def bot_option_def null_option_def null_Sequence⇩b⇩a⇩s⇩e_def
bot_Sequence⇩b⇩a⇩s⇩e_def)
apply(erule_tac Q="Abs_Sequence⇩b⇩a⇩s⇩e ⌊⌊y#⌈⌈Rep_Sequence⇩b⇩a⇩s⇩e x⌉⌉⌋⌋ = Abs_Sequence⇩b⇩a⇩s⇩e None"
in contrapos_pp)
apply(subst Abs_Sequence⇩b⇩a⇩s⇩e_inject [OF A])
apply(simp_all add: null_Sequence⇩b⇩a⇩s⇩e_def bot_Sequence⇩b⇩a⇩s⇩e_def bot_option_def)
apply(erule_tac Q="Abs_Sequence⇩b⇩a⇩s⇩e⌊⌊y#⌈⌈Rep_Sequence⇩b⇩a⇩s⇩e x⌉⌉⌋⌋ = Abs_Sequence⇩b⇩a⇩s⇩e ⌊None⌋"
in contrapos_pp)
apply(subst Abs_Sequence⇩b⇩a⇩s⇩e_inject[OF A])
apply(simp_all add: null_Sequence⇩b⇩a⇩s⇩e_def bot_Sequence⇩b⇩a⇩s⇩e_def
bot_option_def null_option_def)
done
qed
syntax
"_OclFinsequence" :: "args => ('𝔄,'a::null) Sequence" (‹Sequence{(_)}›)
syntax_consts
"_OclFinsequence" == OclPrepend
translations
"Sequence{x, xs}" == "CONST OclPrepend (Sequence{xs}) x"
"Sequence{x}" == "CONST OclPrepend (Sequence{}) x "
subsection‹Definition: Including›
definition OclIncluding :: "[('𝔄,'α::null) Sequence,('𝔄,'α) val] ⇒ ('𝔄,'α) Sequence"
where "OclIncluding x y = (λ τ. if (δ x) τ = true τ ∧ (υ y) τ = true τ
then Abs_Sequence⇩b⇩a⇩s⇩e ⌊⌊ ⌈⌈Rep_Sequence⇩b⇩a⇩s⇩e (x τ)⌉⌉ @ [y τ] ⌋⌋
else invalid τ )"
notation OclIncluding (‹_->including⇩S⇩e⇩q'(_')›)
interpretation OclIncluding :
profile_bin⇩d_⇩v OclIncluding "λx y. Abs_Sequence⇩b⇩a⇩s⇩e⌊⌊⌈⌈Rep_Sequence⇩b⇩a⇩s⇩e x⌉⌉ @ [y]⌋⌋"
proof -
have A : "⋀x y. x ≠ bot ⟹ x ≠ null ⟹ y ≠ bot ⟹
⌊⌊⌈⌈Rep_Sequence⇩b⇩a⇩s⇩e x⌉⌉ @ [y]⌋⌋ ∈ {X. X = bot ∨ X = null ∨ (∀x∈set ⌈⌈X⌉⌉. x ≠ bot)}"
by(auto intro!:Sequence_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_Sequence⇩b⇩a⇩s⇩e ⌊⌊⌈⌈Rep_Sequence⇩b⇩a⇩s⇩e x⌉⌉ @ [y]⌋⌋)"
apply unfold_locales
apply(auto simp:OclIncluding_def bot_option_def null_option_def null_Sequence⇩b⇩a⇩s⇩e_def
bot_Sequence⇩b⇩a⇩s⇩e_def)
apply(erule_tac Q="Abs_Sequence⇩b⇩a⇩s⇩e ⌊⌊⌈⌈Rep_Sequence⇩b⇩a⇩s⇩e x⌉⌉ @ [y]⌋⌋ = Abs_Sequence⇩b⇩a⇩s⇩e None"
in contrapos_pp)
apply(subst Abs_Sequence⇩b⇩a⇩s⇩e_inject [OF A])
apply(simp_all add: null_Sequence⇩b⇩a⇩s⇩e_def bot_Sequence⇩b⇩a⇩s⇩e_def bot_option_def)
apply(erule_tac Q="Abs_Sequence⇩b⇩a⇩s⇩e⌊⌊⌈⌈Rep_Sequence⇩b⇩a⇩s⇩e x⌉⌉ @ [y]⌋⌋ = Abs_Sequence⇩b⇩a⇩s⇩e ⌊None⌋"
in contrapos_pp)
apply(subst Abs_Sequence⇩b⇩a⇩s⇩e_inject[OF A])
apply(simp_all add: null_Sequence⇩b⇩a⇩s⇩e_def bot_Sequence⇩b⇩a⇩s⇩e_def bot_option_def null_option_def)
done
qed
lemma [simp,code_unfold] : "(Sequence{}->including⇩S⇩e⇩q(a)) = (Sequence{}->prepend⇩S⇩e⇩q(a))"
apply(simp add: OclIncluding_def OclPrepend_def mtSequence_def)
apply(subst (1 2) Abs_Sequence⇩b⇩a⇩s⇩e_inverse, simp)
by(metis drop.simps append_Nil)
lemma [simp,code_unfold] : "((S->prepend⇩S⇩e⇩q(a))->including⇩S⇩e⇩q(b)) = ((S->including⇩S⇩e⇩q(b))->prepend⇩S⇩e⇩q(a))"
proof -
have A: "⋀S b τ. S ≠ ⊥ ⟹ S ≠ null ⟹ b ≠ ⊥ ⟹
⌊⌊⌈⌈Rep_Sequence⇩b⇩a⇩s⇩e S⌉⌉ @ [b]⌋⌋ ∈ {X. X = bot ∨ X = null ∨ (∀x∈set ⌈⌈X⌉⌉. x ≠ ⊥)}"
by(auto intro!:Sequence_inv_lemma[simplified OclValid_def
defined_def false_def true_def null_fun_def bot_fun_def])
have B: "⋀S a τ. S ≠ ⊥ ⟹ S ≠ null ⟹ a ≠ ⊥ ⟹
⌊⌊a # ⌈⌈Rep_Sequence⇩b⇩a⇩s⇩e S⌉⌉⌋⌋ ∈ {X. X = bot ∨ X = null ∨ (∀x∈set ⌈⌈X⌉⌉. x ≠ ⊥)}"
by(auto intro!:Sequence_inv_lemma[simplified OclValid_def
defined_def false_def true_def null_fun_def bot_fun_def])
show ?thesis
apply(simp add: OclIncluding_def OclPrepend_def mtSequence_def, rule ext)
apply(subst (2 5) cp_defined, simp split:)
apply(intro conjI impI)
apply(subst Abs_Sequence⇩b⇩a⇩s⇩e_inverse[OF B],
(simp add: foundation16[simplified OclValid_def] foundation18'[simplified OclValid_def])+)
apply(subst Abs_Sequence⇩b⇩a⇩s⇩e_inverse[OF A],
(simp add: foundation16[simplified OclValid_def] foundation18'[simplified OclValid_def])+)
apply(simp add: OclIncluding.def_body)
apply (metis OclValid_def foundation16 invalid_def)
apply (metis (no_types) OclPrepend.def_body' OclValid_def foundation16)
by (metis OclValid_def foundation16 invalid_def)+
qed
subsection‹Definition: Excluding›
definition OclExcluding :: "[('𝔄,'α::null) Sequence,('𝔄,'α) val] ⇒ ('𝔄,'α) Sequence"
where "OclExcluding x y = (λ τ. if (δ x) τ = true τ ∧ (υ y) τ = true τ
then Abs_Sequence⇩b⇩a⇩s⇩e ⌊⌊ filter (λx. x = y τ)
⌈⌈Rep_Sequence⇩b⇩a⇩s⇩e (x τ)⌉⌉⌋⌋
else invalid τ )"
notation OclExcluding (‹_->excluding⇩S⇩e⇩q'(_')›)
interpretation OclExcluding:profile_bin⇩d_⇩v OclExcluding
"λx y. Abs_Sequence⇩b⇩a⇩s⇩e ⌊⌊ filter (λx. x = y) ⌈⌈Rep_Sequence⇩b⇩a⇩s⇩e (x)⌉⌉⌋⌋"
proof -
show "profile_bin⇩d_⇩v OclExcluding (λx y. Abs_Sequence⇩b⇩a⇩s⇩e ⌊⌊[x←⌈⌈Rep_Sequence⇩b⇩a⇩s⇩e x⌉⌉ . x = y]⌋⌋)"
apply unfold_locales
apply(auto simp:OclExcluding_def bot_option_def null_option_def
null_Sequence⇩b⇩a⇩s⇩e_def bot_Sequence⇩b⇩a⇩s⇩e_def)
apply(subst (asm) Abs_Sequence⇩b⇩a⇩s⇩e_inject,
simp_all add: null_Sequence⇩b⇩a⇩s⇩e_def bot_Sequence⇩b⇩a⇩s⇩e_def bot_option_def null_option_def)+
done
qed
subsection‹Definition: Append›
text‹Identical to OclIncluding.›
definition OclAppend :: "[('𝔄,'α::null) Sequence,('𝔄,'α) val] ⇒ ('𝔄,'α) Sequence"
where "OclAppend = OclIncluding"
notation OclAppend (‹_->append⇩S⇩e⇩q'(_')›)
interpretation OclAppend :
profile_bin⇩d_⇩v OclAppend "λx y. Abs_Sequence⇩b⇩a⇩s⇩e⌊⌊⌈⌈Rep_Sequence⇩b⇩a⇩s⇩e x⌉⌉ @ [y]⌋⌋"
apply unfold_locales
by(auto simp: OclAppend_def bin_def bin'_def
OclIncluding.def_scheme OclIncluding.def_body)
subsection‹Definition: Union›
definition OclUnion :: "[('𝔄,'α::null) Sequence,('𝔄,'α) Sequence] ⇒ ('𝔄,'α) Sequence"
where "OclUnion x y = (λ τ. if (δ x) τ = true τ ∧ (δ y) τ = true τ
then Abs_Sequence⇩b⇩a⇩s⇩e ⌊⌊ ⌈⌈Rep_Sequence⇩b⇩a⇩s⇩e (x τ)⌉⌉ @
⌈⌈Rep_Sequence⇩b⇩a⇩s⇩e (y τ)⌉⌉⌋⌋
else invalid τ )"
notation OclUnion (‹_->union⇩S⇩e⇩q'(_')›)
interpretation OclUnion :
profile_bin⇩d_⇩d OclUnion "λx y. Abs_Sequence⇩b⇩a⇩s⇩e⌊⌊⌈⌈Rep_Sequence⇩b⇩a⇩s⇩e x⌉⌉ @ ⌈⌈Rep_Sequence⇩b⇩a⇩s⇩e y⌉⌉⌋⌋"
proof -
have A : "⋀x y. x ≠ ⊥ ⟹ x ≠ null ⟹ ∀x∈set ⌈⌈Rep_Sequence⇩b⇩a⇩s⇩e x⌉⌉. x ≠ ⊥ "
apply(rule Sequence_inv_lemma[of τ])
by(simp add: defined_def OclValid_def bot_fun_def null_fun_def false_def true_def)
show "profile_bin⇩d_⇩d OclUnion (λx y. Abs_Sequence⇩b⇩a⇩s⇩e⌊⌊⌈⌈Rep_Sequence⇩b⇩a⇩s⇩e x⌉⌉@⌈⌈Rep_Sequence⇩b⇩a⇩s⇩e y⌉⌉⌋⌋)"
apply unfold_locales
apply(auto simp:OclUnion_def bot_option_def null_option_def
null_Sequence⇩b⇩a⇩s⇩e_def bot_Sequence⇩b⇩a⇩s⇩e_def)
by(subst (asm) Abs_Sequence⇩b⇩a⇩s⇩e_inject,
simp_all add: bot_option_def null_option_def Set.ball_Un A null_Sequence⇩b⇩a⇩s⇩e_def bot_Sequence⇩b⇩a⇩s⇩e_def)+
qed
subsection‹Definition: At›
definition OclAt :: "[('𝔄,'α::null) Sequence,('𝔄) Integer] ⇒ ('𝔄,'α) val"
where "OclAt x y = (λ τ. if (δ x) τ = true τ ∧ (δ y) τ = true τ
then if 1 ≤ ⌈⌈y τ⌉⌉ ∧ ⌈⌈y τ⌉⌉ ≤ length⌈⌈Rep_Sequence⇩b⇩a⇩s⇩e (x τ)⌉⌉
then ⌈⌈Rep_Sequence⇩b⇩a⇩s⇩e (x τ)⌉⌉ ! (nat ⌈⌈y τ⌉⌉ - 1)
else invalid τ
else invalid τ )"
notation OclAt (‹_->at⇩S⇩e⇩q'(_')›)
subsection‹Definition: First›
definition OclFirst :: "[('𝔄,'α::null) Sequence] ⇒ ('𝔄,'α) val"
where "OclFirst x = (λ τ. if (δ x) τ = true τ then
case ⌈⌈Rep_Sequence⇩b⇩a⇩s⇩e (x τ)⌉⌉ of [] ⇒ invalid τ
| x # _ ⇒ x
else invalid τ )"
notation OclFirst (‹_->first⇩S⇩e⇩q'(_')›)
subsection‹Definition: Last›
definition OclLast :: "[('𝔄,'α::null) Sequence] ⇒ ('𝔄,'α) val"
where "OclLast x = (λ τ. if (δ x) τ = true τ then
if ⌈⌈Rep_Sequence⇩b⇩a⇩s⇩e (x τ)⌉⌉ = [] then
invalid τ
else
last ⌈⌈Rep_Sequence⇩b⇩a⇩s⇩e (x τ)⌉⌉
else invalid τ )"
notation OclLast (‹_->last⇩S⇩e⇩q'(_')›)
subsection‹Definition: Iterate›
definition OclIterate :: "[('𝔄,'α::null) Sequence,('𝔄,'β::null)val,
('𝔄,'α)val⇒('𝔄,'β)val⇒('𝔄,'β)val] ⇒ ('𝔄,'β)val"
where "OclIterate S A F = (λ τ. if (δ S) τ = true τ ∧ (υ A) τ = true τ
then (foldr (F) (map (λa τ. a) ⌈⌈Rep_Sequence⇩b⇩a⇩s⇩e (S τ)⌉⌉))(A)τ
else ⊥)"
syntax
"_OclIterateSeq" :: "[('𝔄,'α::null) Sequence, idt, idt, 'α, 'β] => ('𝔄,'γ)val"
(‹_ ->iterate⇩S⇩e⇩q'(_;_=_ | _')› )
syntax_consts
"_OclIterateSeq" == OclIterate
translations
"X->iterate⇩S⇩e⇩q(a; x = A | P)" == "CONST OclIterate X A (%a. (% x. P))"
subsection‹Definition: Forall›
definition OclForall :: "[('𝔄,'α::null) Sequence,('𝔄,'α)val⇒('𝔄)Boolean] ⇒ '𝔄 Boolean"
where "OclForall S P = (S->iterate⇩S⇩e⇩q(b; x = true | x and (P b)))"
syntax
"_OclForallSeq" :: "[('𝔄,'α::null) Sequence,id,('𝔄)Boolean] ⇒ '𝔄 Boolean" (‹(_)->forAll⇩S⇩e⇩q'(_|_')›)
syntax_consts
"_OclForallSeq" == UML_Sequence.OclForall
translations
"X->forAll⇩S⇩e⇩q(x | P)" == "CONST UML_Sequence.OclForall X (%x. P)"
subsection‹Definition: Exists›
definition OclExists :: "[('𝔄,'α::null) Sequence,('𝔄,'α)val⇒('𝔄)Boolean] ⇒ '𝔄 Boolean"
where "OclExists S P = (S->iterate⇩S⇩e⇩q(b; x = false | x or (P b)))"
syntax
"_OclExistSeq" :: "[('𝔄,'α::null) Sequence,id,('𝔄)Boolean] ⇒ '𝔄 Boolean" (‹(_)->exists⇩S⇩e⇩q'(_|_')›)
syntax_consts
"_OclExistSeq" == OclExists
translations
"X->exists⇩S⇩e⇩q(x | P)" == "CONST OclExists X (%x. P)"
subsection‹Definition: Collect›
definition OclCollect :: "[('𝔄,'α::null)Sequence,('𝔄,'α)val⇒('𝔄,'β)val]⇒('𝔄,'β::null)Sequence"
where "OclCollect S P = (S->iterate⇩S⇩e⇩q(b; x = Sequence{} | x->prepend⇩S⇩e⇩q(P b)))"
syntax
"_OclCollectSeq" :: "[('𝔄,'α::null) Sequence,id,('𝔄)Boolean] ⇒ '𝔄 Boolean" (‹(_)->collect⇩S⇩e⇩q'(_|_')›)
syntax_consts
"_OclCollectSeq" == OclCollect
translations
"X->collect⇩S⇩e⇩q(x | P)" == "CONST OclCollect X (%x. P)"
subsection‹Definition: Select›
definition OclSelect :: "[('𝔄,'α::null)Sequence,('𝔄,'α)val⇒('𝔄)Boolean]⇒('𝔄,'α::null)Sequence"
where "OclSelect S P =
(S->iterate⇩S⇩e⇩q(b; x = Sequence{} | if P b then x->prepend⇩S⇩e⇩q(b) else x endif))"
syntax
"_OclSelectSeq" :: "[('𝔄,'α::null) Sequence,id,('𝔄)Boolean] ⇒ '𝔄 Boolean" (‹(_)->select⇩S⇩e⇩q'(_|_')›)
syntax_consts
"_OclSelectSeq" == UML_Sequence.OclSelect
translations
"X->select⇩S⇩e⇩q(x | P)" == "CONST UML_Sequence.OclSelect X (%x. P)"
subsection‹Definition: Size›
definition OclSize :: "[('𝔄,'α::null)Sequence]⇒('𝔄)Integer" (‹(_)->size⇩S⇩e⇩q'(')›)
where "OclSize S = (S->iterate⇩S⇩e⇩q(b; x = 𝟬 | x +⇩i⇩n⇩t 𝟭 ))"
subsection‹Definition: IsEmpty›
definition OclIsEmpty :: "('𝔄,'α::null) Sequence ⇒ '𝔄 Boolean"
where "OclIsEmpty x = ((υ x and not (δ x)) or ((OclSize x) ≐ 𝟬))"
notation OclIsEmpty (‹_->isEmpty⇩S⇩e⇩q'(')› )
subsection‹Definition: NotEmpty›
definition OclNotEmpty :: "('𝔄,'α::null) Sequence ⇒ '𝔄 Boolean"
where "OclNotEmpty x = not(OclIsEmpty x)"
notation OclNotEmpty (‹_->notEmpty⇩S⇩e⇩q'(')› )
subsection‹Definition: Any›
definition "OclANY x = (λ τ.
if x τ = invalid τ then
⊥
else
case drop (drop (Rep_Sequence⇩b⇩a⇩s⇩e (x τ))) of [] ⇒ ⊥
| l ⇒ hd l)"
notation OclANY (‹_->any⇩S⇩e⇩q'(')›)
subsection‹Definition (future operators)›
consts
OclCount :: "[('𝔄,'α::null) Sequence,('𝔄,'α) Sequence] ⇒ '𝔄 Integer"
OclSum :: " ('𝔄,'α::null) Sequence ⇒ '𝔄 Integer"
notation OclCount (‹_->count⇩S⇩e⇩q'(_')› )
notation OclSum (‹_->sum⇩S⇩e⇩q'(')› )
subsection‹Logical Properties›
subsection‹Execution Laws with Invalid or Null as Argument›
text‹OclIterate›
lemma OclIterate_invalid[simp,code_unfold]:"invalid->iterate⇩S⇩e⇩q(a; x = A | P a x) = invalid"
by(simp add: OclIterate_def false_def true_def, simp add: invalid_def)
lemma OclIterate_null[simp,code_unfold]:"null->iterate⇩S⇩e⇩q(a; x = A | P a x) = invalid"
by(simp add: OclIterate_def false_def true_def, simp add: invalid_def)
lemma OclIterate_invalid_args[simp,code_unfold]:"S->iterate⇩S⇩e⇩q(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_raw‹\isatagafp›
subsubsection‹Context Passing›
lemma cp_OclIncluding:
"(X->including⇩S⇩e⇩q(x)) τ = ((λ _. X τ)->including⇩S⇩e⇩q(λ _. x τ)) τ"
by(auto simp: OclIncluding_def StrongEq_def invalid_def
cp_defined[symmetric] cp_valid[symmetric])
lemma cp_OclIterate:
"(X->iterate⇩S⇩e⇩q(a; x = A | P a x)) τ =
((λ _. X τ)->iterate⇩S⇩e⇩q(a; x = A | P a x)) τ"
by(simp add: OclIterate_def cp_defined[symmetric])
lemmas cp_intro''⇩S⇩e⇩q[intro!,simp,code_unfold] =
cp_OclIncluding [THEN allI[THEN allI[THEN allI[THEN cpI2]], of "OclIncluding"]]
subsubsection‹Const›
text_raw‹\endisatagafp›
subsection‹General Algebraic Execution Rules›
subsubsection‹Execution Rules on Iterate›
lemma OclIterate_empty[simp,code_unfold]:"Sequence{}->iterate⇩S⇩e⇩q(a; x = A | P a x) = A"
apply(simp add: OclIterate_def foundation22[symmetric] foundation13,
rule ext, rename_tac "τ")
apply(case_tac "τ ⊨ υ A", simp_all add: foundation18')
apply(simp add: mtSequence_def)
apply(subst Abs_Sequence⇩b⇩a⇩s⇩e_inverse) by auto
text‹In particular, this does hold for A = null.›
lemma OclIterate_including[simp,code_unfold]:
assumes strict1 : "⋀X. P invalid X = invalid"
and P_valid_arg: "⋀ τ. (υ A) τ = (υ (P a A)) τ"
and P_cp : "⋀ x y τ. P x y τ = P (λ _. x τ) y τ"
and P_cp' : "⋀ x y τ. P x y τ = P x (λ _. y τ) τ"
shows "(S->including⇩S⇩e⇩q(a))->iterate⇩S⇩e⇩q(b; x = A | P b x) = S->iterate⇩S⇩e⇩q(b; x = P a A| P b x)"
apply(rule ext)
proof -
have A: "⋀S b τ. S ≠ ⊥ ⟹ S ≠ null ⟹ b ≠ ⊥ ⟹
⌊⌊⌈⌈Rep_Sequence⇩b⇩a⇩s⇩e S⌉⌉ @ [b]⌋⌋ ∈ {X. X = bot ∨ X = null ∨ (∀x∈set ⌈⌈X⌉⌉. x ≠ ⊥)}"
by(auto intro!:Sequence_inv_lemma[simplified OclValid_def
defined_def false_def true_def null_fun_def bot_fun_def])
have P: "⋀l A A' τ. A τ = A' τ ⟹ foldr P l A τ = foldr P l A' τ"
apply(rule list.induct, simp, simp)
by(subst (1 2) P_cp', simp)
fix τ
show "OclIterate (S->including⇩S⇩e⇩q(a)) A P τ = OclIterate S (P a A) P τ"
apply(subst cp_OclIterate, subst OclIncluding_def, simp split:)
apply(intro conjI impI)
apply(simp add: OclIterate_def)
apply(intro conjI impI)
apply(subst Abs_Sequence⇩b⇩a⇩s⇩e_inverse[OF A],
(simp add: foundation16[simplified OclValid_def] foundation18'[simplified OclValid_def])+)
apply(rule P, metis P_cp)
apply (metis P_valid_arg)
apply(simp add: P_valid_arg[symmetric])
apply (metis (lifting, no_types) OclIncluding.def_body' OclValid_def foundation16)
apply(simp add: OclIterate_def defined_def invalid_def bot_option_def bot_fun_def false_def true_def)
apply(intro impI, simp add: false_def true_def P_valid_arg)
by (metis P_cp P_valid_arg UML_Types.bot_fun_def cp_valid invalid_def strict1 true_def valid1 valid_def)
qed
lemma OclIterate_prepend[simp,code_unfold]:
assumes strict1 : "⋀X. P invalid X = invalid"
and strict2 : "⋀X. P X invalid = invalid"
and P_cp : "⋀ x y τ. P x y τ = P (λ _. x τ) y τ"
and P_cp' : "⋀ x y τ. P x y τ = P x (λ _. y τ) τ"
shows "(S->prepend⇩S⇩e⇩q(a))->iterate⇩S⇩e⇩q(b; x = A | P b x) = P a (S->iterate⇩S⇩e⇩q(b; x = A| P b x))"
apply(rule ext)
proof -
have B: "⋀S a τ. S ≠ ⊥ ⟹ S ≠ null ⟹ a ≠ ⊥ ⟹
⌊⌊a # ⌈⌈Rep_Sequence⇩b⇩a⇩s⇩e S⌉⌉⌋⌋ ∈ {X. X = bot ∨ X = null ∨ (∀x∈set ⌈⌈X⌉⌉. x ≠ ⊥)}"
by(auto intro!:Sequence_inv_lemma[simplified OclValid_def
defined_def false_def true_def null_fun_def bot_fun_def])
fix τ
show "OclIterate (S->prepend⇩S⇩e⇩q(a)) A P τ = P a (OclIterate S A P) τ"
apply(subst cp_OclIterate, subst OclPrepend_def, simp split:)
apply(intro conjI impI)
apply(subst P_cp')
apply(simp add: OclIterate_def)
apply(intro conjI impI)
apply(subst Abs_Sequence⇩b⇩a⇩s⇩e_inverse[OF B],
(simp add: foundation16[simplified OclValid_def] foundation18'[simplified OclValid_def])+)
apply(simp add: P_cp'[symmetric])
apply(subst P_cp, simp add: P_cp[symmetric])
apply (metis (no_types) OclPrepend.def_body' OclValid_def foundation16)
apply (metis P_cp' invalid_def strict2 valid_def)
apply(subst P_cp',
simp add: OclIterate_def defined_def invalid_def bot_option_def bot_fun_def false_def true_def,
intro conjI impI)
apply (metis P_cp' invalid_def strict2 valid_def)
apply (metis P_cp' invalid_def strict2 valid_def)
apply (metis (no_types) P_cp invalid_def strict1 true_def valid1 valid_def)
apply (metis P_cp' invalid_def strict2 valid_def)
done
qed
subsection‹Test Statements›
instantiation Sequence⇩b⇩a⇩s⇩e :: (equal)equal
begin
definition "HOL.equal k l ⟷ (k::('a::equal)Sequence⇩b⇩a⇩s⇩e) = l"
instance by standard (rule equal_Sequence⇩b⇩a⇩s⇩e_def)
end
lemma equal_Sequence⇩b⇩a⇩s⇩e_code [code]:
"HOL.equal k (l::('a::{equal,null})Sequence⇩b⇩a⇩s⇩e) ⟷ Rep_Sequence⇩b⇩a⇩s⇩e k = Rep_Sequence⇩b⇩a⇩s⇩e l"
by (auto simp add: equal Sequence⇩b⇩a⇩s⇩e.Rep_Sequence⇩b⇩a⇩s⇩e_inject)
Assert "τ ⊨ (Sequence{} ≐ Sequence{})"
Assert "τ ⊨ (Sequence{𝟭,𝟮} ≜ Sequence{}->prepend⇩S⇩e⇩q(𝟮)->prepend⇩S⇩e⇩q(𝟭))"
Assert "τ ⊨ (Sequence{𝟭,invalid,𝟮} ≜ invalid)"
Assert "τ ⊨ (Sequence{𝟭,𝟮}->prepend⇩S⇩e⇩q(null) ≜ Sequence{null,𝟭,𝟮})"
Assert "τ ⊨ (Sequence{𝟭,𝟮}->including⇩S⇩e⇩q(null) ≜ Sequence{𝟭,𝟮,null})"
end