Theory UML_Real
theory UML_Real
imports "../UML_PropertyProfiles"
begin
section‹Basic Type Real: Operations›
subsection‹Fundamental Predicates on Reals: Strict Equality \label{sec:real-strict-eq}›
text‹The last basic operation belonging to the fundamental infrastructure
of a value-type in OCL is the weak equality, which is defined similar
to the @{typ "('𝔄)Boolean"}-case as strict extension of the strong equality:›
overloading StrictRefEq ≡ "StrictRefEq :: [('𝔄)Real,('𝔄)Real] ⇒ ('𝔄)Boolean"
begin
definition StrictRefEq⇩R⇩e⇩a⇩l [code_unfold] :
"(x::('𝔄)Real) ≐ y ≡ λ τ. if (υ x) τ = true τ ∧ (υ y) τ = true τ
then (x ≜ y) τ
else invalid τ"
end
text‹Property proof in terms of @{term "profile_bin⇩S⇩t⇩r⇩o⇩n⇩g⇩E⇩q_⇩v_⇩v"}›
interpretation StrictRefEq⇩R⇩e⇩a⇩l : profile_bin⇩S⇩t⇩r⇩o⇩n⇩g⇩E⇩q_⇩v_⇩v "λ x y. (x::('𝔄)Real) ≐ y"
by unfold_locales (auto simp: StrictRefEq⇩R⇩e⇩a⇩l)
subsection‹Basic Real Constants›
text‹Although the remaining part of this library reasons about
reals abstractly, we provide here as example some convenient shortcuts.›
definition OclReal0 ::"('𝔄)Real" ("𝟬.𝟬") where "𝟬.𝟬 = (λ _ . ⌊⌊0::real⌋⌋)"
definition OclReal1 ::"('𝔄)Real" ("𝟭.𝟬") where "𝟭.𝟬 = (λ _ . ⌊⌊1::real⌋⌋)"
definition OclReal2 ::"('𝔄)Real" ("𝟮.𝟬") where "𝟮.𝟬 = (λ _ . ⌊⌊2::real⌋⌋)"
text‹Etc.›
text_raw‹\isatagafp›
definition OclReal3 ::"('𝔄)Real" ("𝟯.𝟬") where "𝟯.𝟬 = (λ _ . ⌊⌊3::real⌋⌋)"
definition OclReal4 ::"('𝔄)Real" ("𝟰.𝟬") where "𝟰.𝟬 = (λ _ . ⌊⌊4::real⌋⌋)"
definition OclReal5 ::"('𝔄)Real" ("𝟱.𝟬") where "𝟱.𝟬 = (λ _ . ⌊⌊5::real⌋⌋)"
definition OclReal6 ::"('𝔄)Real" ("𝟲.𝟬") where "𝟲.𝟬 = (λ _ . ⌊⌊6::real⌋⌋)"
definition OclReal7 ::"('𝔄)Real" ("𝟳.𝟬") where "𝟳.𝟬 = (λ _ . ⌊⌊7::real⌋⌋)"
definition OclReal8 ::"('𝔄)Real" ("𝟴.𝟬") where "𝟴.𝟬 = (λ _ . ⌊⌊8::real⌋⌋)"
definition OclReal9 ::"('𝔄)Real" ("𝟵.𝟬") where "𝟵.𝟬 = (λ _ . ⌊⌊9::real⌋⌋)"
definition OclReal10 ::"('𝔄)Real" ("𝟭𝟬.𝟬") where "𝟭𝟬.𝟬 = (λ _ . ⌊⌊10::real⌋⌋)"
definition OclRealpi ::"('𝔄)Real" ("π") where "π = (λ _ . ⌊⌊pi⌋⌋)"
subsection‹Validity and Definedness Properties›
lemma "δ(null::('𝔄)Real) = false" by simp
lemma "υ(null::('𝔄)Real) = true" by simp
lemma [simp,code_unfold]: "δ (λ_. ⌊⌊n⌋⌋) = true"
by(simp add:defined_def true_def
bot_fun_def bot_option_def null_fun_def null_option_def)
lemma [simp,code_unfold]: "υ (λ_. ⌊⌊n⌋⌋) = true"
by(simp add:valid_def true_def
bot_fun_def bot_option_def)
lemma [simp,code_unfold]: "δ 𝟬.𝟬 = true" by(simp add:OclReal0_def)
lemma [simp,code_unfold]: "υ 𝟬.𝟬 = true" by(simp add:OclReal0_def)
lemma [simp,code_unfold]: "δ 𝟭.𝟬 = true" by(simp add:OclReal1_def)
lemma [simp,code_unfold]: "υ 𝟭.𝟬 = true" by(simp add:OclReal1_def)
lemma [simp,code_unfold]: "δ 𝟮.𝟬 = true" by(simp add:OclReal2_def)
lemma [simp,code_unfold]: "υ 𝟮.𝟬 = true" by(simp add:OclReal2_def)
lemma [simp,code_unfold]: "δ 𝟲.𝟬 = true" by(simp add:OclReal6_def)
lemma [simp,code_unfold]: "υ 𝟲.𝟬 = true" by(simp add:OclReal6_def)
lemma [simp,code_unfold]: "δ 𝟴.𝟬 = true" by(simp add:OclReal8_def)
lemma [simp,code_unfold]: "υ 𝟴.𝟬 = true" by(simp add:OclReal8_def)
lemma [simp,code_unfold]: "δ 𝟵.𝟬 = true" by(simp add:OclReal9_def)
lemma [simp,code_unfold]: "υ 𝟵.𝟬 = true" by(simp add:OclReal9_def)
text_raw‹\endisatagafp›
subsection‹Arithmetical Operations›
subsubsection‹Definition›
text‹Here is a common case of a built-in operation on built-in types.
Note that the arguments must be both defined (non-null, non-bot).›
text‹Note that we can not follow the lexis of the OCL Standard for Isabelle
technical reasons; these operators are heavily overloaded in the HOL library
that a further overloading would lead to heavy technical buzz in this
document.
›
definition OclAdd⇩R⇩e⇩a⇩l ::"('𝔄)Real ⇒ ('𝔄)Real ⇒ ('𝔄)Real" (infix "+⇩r⇩e⇩a⇩l" 40)
where "x +⇩r⇩e⇩a⇩l y ≡ λ τ. if (δ x) τ = true τ ∧ (δ y) τ = true τ
then ⌊⌊⌈⌈x τ⌉⌉ + ⌈⌈y τ⌉⌉⌋⌋
else invalid τ "
interpretation OclAdd⇩R⇩e⇩a⇩l : profile_bin⇩d_⇩d "(+⇩r⇩e⇩a⇩l)" "λ x y. ⌊⌊⌈⌈x⌉⌉ + ⌈⌈y⌉⌉⌋⌋"
by unfold_locales (auto simp:OclAdd⇩R⇩e⇩a⇩l_def bot_option_def null_option_def)
definition OclMinus⇩R⇩e⇩a⇩l ::"('𝔄)Real ⇒ ('𝔄)Real ⇒ ('𝔄)Real" (infix "-⇩r⇩e⇩a⇩l" 41)
where "x -⇩r⇩e⇩a⇩l y ≡ λ τ. if (δ x) τ = true τ ∧ (δ y) τ = true τ
then ⌊⌊⌈⌈x τ⌉⌉ - ⌈⌈y τ⌉⌉⌋⌋
else invalid τ "
interpretation OclMinus⇩R⇩e⇩a⇩l : profile_bin⇩d_⇩d "(-⇩r⇩e⇩a⇩l)" "λ x y. ⌊⌊⌈⌈x⌉⌉ - ⌈⌈y⌉⌉⌋⌋"
by unfold_locales (auto simp:OclMinus⇩R⇩e⇩a⇩l_def bot_option_def null_option_def)
definition OclMult⇩R⇩e⇩a⇩l ::"('𝔄)Real ⇒ ('𝔄)Real ⇒ ('𝔄)Real" (infix "*⇩r⇩e⇩a⇩l" 45)
where "x *⇩r⇩e⇩a⇩l y ≡ λ τ. if (δ x) τ = true τ ∧ (δ y) τ = true τ
then ⌊⌊⌈⌈x τ⌉⌉ * ⌈⌈y τ⌉⌉⌋⌋
else invalid τ"
interpretation OclMult⇩R⇩e⇩a⇩l : profile_bin⇩d_⇩d "OclMult⇩R⇩e⇩a⇩l" "λ x y. ⌊⌊⌈⌈x⌉⌉ * ⌈⌈y⌉⌉⌋⌋"
by unfold_locales (auto simp:OclMult⇩R⇩e⇩a⇩l_def bot_option_def null_option_def)
text‹Here is the special case of division, which is defined as invalid for division
by zero.›
definition OclDivision⇩R⇩e⇩a⇩l ::"('𝔄)Real ⇒ ('𝔄)Real ⇒ ('𝔄)Real" (infix "div⇩r⇩e⇩a⇩l" 45)
where "x div⇩r⇩e⇩a⇩l y ≡ λ τ. if (δ x) τ = true τ ∧ (δ y) τ = true τ
then if y τ ≠ OclReal0 τ then ⌊⌊⌈⌈x τ⌉⌉ / ⌈⌈y τ⌉⌉⌋⌋ else invalid τ
else invalid τ "
definition "mod_float a b = a - real_of_int (floor (a / b)) * b"
definition OclModulus⇩R⇩e⇩a⇩l ::"('𝔄)Real ⇒ ('𝔄)Real ⇒ ('𝔄)Real" (infix "mod⇩r⇩e⇩a⇩l" 45)
where "x mod⇩r⇩e⇩a⇩l y ≡ λ τ. if (δ x) τ = true τ ∧ (δ y) τ = true τ
then if y τ ≠ OclReal0 τ then ⌊⌊mod_float ⌈⌈x τ⌉⌉ ⌈⌈y τ⌉⌉⌋⌋ else invalid τ
else invalid τ "
definition OclLess⇩R⇩e⇩a⇩l ::"('𝔄)Real ⇒ ('𝔄)Real ⇒ ('𝔄)Boolean" (infix "<⇩r⇩e⇩a⇩l" 35)
where "x <⇩r⇩e⇩a⇩l y ≡ λ τ. if (δ x) τ = true τ ∧ (δ y) τ = true τ
then ⌊⌊⌈⌈x τ⌉⌉ < ⌈⌈y τ⌉⌉⌋⌋
else invalid τ "
interpretation OclLess⇩R⇩e⇩a⇩l : profile_bin⇩d_⇩d "(<⇩r⇩e⇩a⇩l)" "λ x y. ⌊⌊⌈⌈x⌉⌉ < ⌈⌈y⌉⌉⌋⌋"
by unfold_locales (auto simp:OclLess⇩R⇩e⇩a⇩l_def bot_option_def null_option_def)
definition OclLe⇩R⇩e⇩a⇩l ::"('𝔄)Real ⇒ ('𝔄)Real ⇒ ('𝔄)Boolean" (infix "≤⇩r⇩e⇩a⇩l" 35)
where "x ≤⇩r⇩e⇩a⇩l y ≡ λ τ. if (δ x) τ = true τ ∧ (δ y) τ = true τ
then ⌊⌊⌈⌈x τ⌉⌉ ≤ ⌈⌈y τ⌉⌉⌋⌋
else invalid τ "
interpretation OclLe⇩R⇩e⇩a⇩l : profile_bin⇩d_⇩d "(≤⇩r⇩e⇩a⇩l)" "λ x y. ⌊⌊⌈⌈x⌉⌉ ≤ ⌈⌈y⌉⌉⌋⌋"
by unfold_locales (auto simp:OclLe⇩R⇩e⇩a⇩l_def bot_option_def null_option_def)
subsubsection‹Basic Properties›
lemma OclAdd⇩R⇩e⇩a⇩l_commute: "(X +⇩r⇩e⇩a⇩l Y) = (Y +⇩r⇩e⇩a⇩l X)"
by(rule ext,auto simp:true_def false_def OclAdd⇩R⇩e⇩a⇩l_def invalid_def
split: option.split option.split_asm
bool.split bool.split_asm)
subsubsection‹Execution with Invalid or Null or Zero as Argument›
lemma OclAdd⇩R⇩e⇩a⇩l_zero1[simp,code_unfold] :
"(x +⇩r⇩e⇩a⇩l 𝟬.𝟬) = (if υ x and not (δ x) then invalid else x endif)"
proof (rule ext, rename_tac τ, case_tac "(υ x and not (δ x)) τ = true τ")
fix τ show "(υ x and not (δ x)) τ = true τ ⟹
(x +⇩r⇩e⇩a⇩l 𝟬.𝟬) τ = (if υ x and not (δ x) then invalid else x endif) τ"
apply(subst OclIf_true', simp add: OclValid_def)
by (metis OclAdd⇩R⇩e⇩a⇩l_def OclNot_defargs OclValid_def foundation5 foundation9)
next fix τ
have A: "⋀τ. (τ ⊨ not (υ x and not (δ x))) = (x τ = invalid τ ∨ τ ⊨ δ x)"
by (metis OclNot_not OclOr_def defined5 defined6 defined_not_I foundation11 foundation18'
foundation6 foundation7 foundation9 invalid_def)
have B: "τ ⊨ δ x ⟹ ⌊⌊⌈⌈x τ⌉⌉⌋⌋ = x τ"
apply(cases "x τ", metis bot_option_def foundation16)
apply(rename_tac x', case_tac x', metis bot_option_def foundation16 null_option_def)
by(simp)
show "(x +⇩r⇩e⇩a⇩l 𝟬.𝟬) τ = (if υ x and not (δ x) then invalid else x endif) τ"
when "τ ⊨ not (υ x and not (δ x))"
apply(insert that, subst OclIf_false', simp, simp add: A, auto simp: OclAdd⇩R⇩e⇩a⇩l_def OclReal0_def)
apply(simp add: foundation16'[simplified OclValid_def])
apply(simp add: B)
by(simp add: OclValid_def)
qed(metis OclValid_def defined5 defined6 defined_and_I defined_not_I foundation9)
lemma OclAdd⇩R⇩e⇩a⇩l_zero2[simp,code_unfold] :
"(𝟬.𝟬 +⇩r⇩e⇩a⇩l x) = (if υ x and not (δ x) then invalid else x endif)"
by(subst OclAdd⇩R⇩e⇩a⇩l_commute, simp)
subsection‹Test Statements›
text‹Here follows a list of code-examples, that explain the meanings
of the above definitions by compilation to code and execution to @{term "True"}.›
Assert "τ ⊨ ( 𝟵.𝟬 ≤⇩r⇩e⇩a⇩l 𝟭𝟬.𝟬 )"
Assert "τ ⊨ (( 𝟰.𝟬 +⇩r⇩e⇩a⇩l 𝟰.𝟬 ) ≤⇩r⇩e⇩a⇩l 𝟭𝟬.𝟬 )"
Assert "τ |≠ (( 𝟰.𝟬 +⇩r⇩e⇩a⇩l ( 𝟰.𝟬 +⇩r⇩e⇩a⇩l 𝟰.𝟬 )) <⇩r⇩e⇩a⇩l 𝟭𝟬.𝟬 )"
Assert "τ ⊨ not (υ (null +⇩r⇩e⇩a⇩l 𝟭.𝟬)) "
Assert "τ ⊨ (((𝟵.𝟬 *⇩r⇩e⇩a⇩l 𝟰.𝟬) div⇩r⇩e⇩a⇩l 𝟭𝟬.𝟬) ≤⇩r⇩e⇩a⇩l 𝟰.𝟬) "
Assert "τ ⊨ not (δ (𝟭.𝟬 div⇩r⇩e⇩a⇩l 𝟬.𝟬)) "
Assert "τ ⊨ not (υ (𝟭.𝟬 div⇩r⇩e⇩a⇩l 𝟬.𝟬)) "
lemma real_non_null [simp]: "((λ_. ⌊⌊n⌋⌋) ≐ (null::('𝔄)Real)) = false"
by(rule ext,auto simp: StrictRefEq⇩R⇩e⇩a⇩l valid_def
bot_fun_def bot_option_def null_fun_def null_option_def StrongEq_def)
lemma null_non_real [simp]: "((null::('𝔄)Real) ≐ (λ_. ⌊⌊n⌋⌋)) = false"
by(rule ext,auto simp: StrictRefEq⇩R⇩e⇩a⇩l valid_def
bot_fun_def bot_option_def null_fun_def null_option_def StrongEq_def)
lemma OclReal0_non_null [simp,code_unfold]: "(𝟬.𝟬 ≐ null) = false" by(simp add: OclReal0_def)
lemma null_non_OclReal0 [simp,code_unfold]: "(null ≐ 𝟬.𝟬) = false" by(simp add: OclReal0_def)
lemma OclReal1_non_null [simp,code_unfold]: "(𝟭.𝟬 ≐ null) = false" by(simp add: OclReal1_def)
lemma null_non_OclReal1 [simp,code_unfold]: "(null ≐ 𝟭.𝟬) = false" by(simp add: OclReal1_def)
lemma OclReal2_non_null [simp,code_unfold]: "(𝟮.𝟬 ≐ null) = false" by(simp add: OclReal2_def)
lemma null_non_OclReal2 [simp,code_unfold]: "(null ≐ 𝟮.𝟬) = false" by(simp add: OclReal2_def)
lemma OclReal6_non_null [simp,code_unfold]: "(𝟲.𝟬 ≐ null) = false" by(simp add: OclReal6_def)
lemma null_non_OclReal6 [simp,code_unfold]: "(null ≐ 𝟲.𝟬) = false" by(simp add: OclReal6_def)
lemma OclReal8_non_null [simp,code_unfold]: "(𝟴.𝟬 ≐ null) = false" by(simp add: OclReal8_def)
lemma null_non_OclReal8 [simp,code_unfold]: "(null ≐ 𝟴.𝟬) = false" by(simp add: OclReal8_def)
lemma OclReal9_non_null [simp,code_unfold]: "(𝟵.𝟬 ≐ null) = false" by(simp add: OclReal9_def)
lemma null_non_OclReal9 [simp,code_unfold]: "(null ≐ 𝟵.𝟬) = false" by(simp add: OclReal9_def)
text‹Here follows a list of code-examples, that explain the meanings
of the above definitions by compilation to code and execution to @{term "True"}.›
text‹Elementary computations on Real›
Assert "τ ⊨ 𝟭.𝟬 <> 𝟮.𝟬"
Assert "τ ⊨ 𝟮.𝟬 <> 𝟭.𝟬"
Assert "τ ⊨ 𝟮.𝟬 ≐ 𝟮.𝟬"
Assert "τ ⊨ υ 𝟰.𝟬"
Assert "τ ⊨ δ 𝟰.𝟬"
Assert "τ ⊨ υ (null::('𝔄)Real)"
Assert "τ ⊨ (invalid ≜ invalid)"
Assert "τ ⊨ (null ≜ null)"
Assert "τ ⊨ (𝟰.𝟬 ≜ 𝟰.𝟬)"
Assert "τ |≠ (𝟵.𝟬 ≜ 𝟭𝟬.𝟬)"
Assert "τ |≠ (invalid ≜ 𝟭𝟬.𝟬)"
Assert "τ |≠ (null ≜ 𝟭𝟬.𝟬)"
Assert "τ |≠ (invalid ≐ (invalid::('𝔄)Real))"
Assert "τ |≠ υ (invalid ≐ (invalid::('𝔄)Real))"
Assert "τ |≠ (invalid <> (invalid::('𝔄)Real))"
Assert "τ |≠ υ (invalid <> (invalid::('𝔄)Real))"
Assert "τ ⊨ (null ≐ (null::('𝔄)Real) )"
Assert "τ ⊨ (null ≐ (null::('𝔄)Real) )"
Assert "τ ⊨ (𝟰.𝟬 ≐ 𝟰.𝟬)"
Assert "τ |≠ (𝟰.𝟬 <> 𝟰.𝟬)"
Assert "τ |≠ (𝟰.𝟬 ≐ 𝟭𝟬.𝟬)"
Assert "τ ⊨ (𝟰.𝟬 <> 𝟭𝟬.𝟬)"
Assert "τ |≠ (𝟬.𝟬 <⇩r⇩e⇩a⇩l null)"
Assert "τ |≠ (δ (𝟬.𝟬 <⇩r⇩e⇩a⇩l null))"
end