Theory UML_Real

(*****************************************************************************
 * Featherweight-OCL --- A Formal Semantics for UML-OCL Version OCL 2.5
 *                       for the OMG Standard.
 *                       http://www.brucker.ch/projects/hol-testgen/
 *
 * UML_Real.thy --- Library definitions.
 * This file is part of HOL-TestGen.
 *
 * Copyright (c) 2012-2015 Université Paris-Saclay, Univ. Paris-Sud, France
 *               2013-2015 IRT SystemX, France
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are
 * met:
 *
 *     * Redistributions of source code must retain the above copyright
 *       notice, this list of conditions and the following disclaimer.
 *
 *     * Redistributions in binary form must reproduce the above
 *       copyright notice, this list of conditions and the following
 *       disclaimer in the documentation and/or other materials provided
 *       with the distribution.
 *
 *     * Neither the name of the copyright holders nor the names of its
 *       contributors may be used to endorse or promote products derived
 *       from this software without specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
 * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
 * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
 * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
 * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
 * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
 * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
 * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
 * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 ******************************************************************************)

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)

(* ecclectic proofs to make examples executable *)
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 τ "
(* TODO: special locale setup.*)

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 τ "
(* TODO: special locale setup.*)


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)

(* TODO Basic proproperties for multiplication, division, modulus. *)



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))" (* Without typeconstraint not executable.*)
Assert "τ |≠ υ (invalid ≐ (invalid::('𝔄)Real))" (* Without typeconstraint not executable.*)
Assert "τ |≠ (invalid <> (invalid::('𝔄)Real))" (* Without typeconstraint not executable.*)
Assert "τ |≠ υ (invalid <> (invalid::('𝔄)Real))" (* Without typeconstraint not executable.*)
Assert "τ ⊨ (null ≐ (null::('𝔄)Real) )" (* Without typeconstraint not executable.*)
Assert "τ ⊨ (null ≐ (null::('𝔄)Real) )" (* Without typeconstraint not executable.*)
Assert "τ ⊨ (𝟰.𝟬 ≐ 𝟰.𝟬)"
Assert "τ |≠ (𝟰.𝟬 <> 𝟰.𝟬)"
Assert "τ |≠ (𝟰.𝟬 ≐ 𝟭𝟬.𝟬)"
Assert "τ ⊨ (𝟰.𝟬 <> 𝟭𝟬.𝟬)"
Assert "τ |≠ (𝟬.𝟬 <⇩r⇩e⇩a⇩l null)"
Assert "τ |≠ (δ (𝟬.𝟬 <⇩r⇩e⇩a⇩l null))"


end