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 StrictRefEqReal [code_unfold] :
    "(x::('𝔄)Real)  y  λ τ. if (υ x) τ = true τ  (υ y) τ = true τ
                                  then (x  y) τ
                                  else invalid τ"
end

text‹Property proof in terms of @{term "profile_binStrongEq_v_v"}
interpretation StrictRefEqReal : profile_binStrongEq_v_v "λ x y. (x::('𝔄)Real)  y" 
         by unfold_locales (auto simp: StrictRefEqReal)

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 OclAddReal ::"('𝔄)Real  ('𝔄)Real  ('𝔄)Real" (infix "+real" 40)
where "x +real y  λ τ. if (δ x) τ = true τ  (δ y) τ = true τ
                       then x τ + y τ
                       else invalid τ "
interpretation OclAddReal : profile_bind_d "(+real)" "λ x y. x + y"
         by unfold_locales (auto simp:OclAddReal_def bot_option_def null_option_def)


definition OclMinusReal ::"('𝔄)Real  ('𝔄)Real  ('𝔄)Real" (infix "-real" 41)
where "x -real y  λ τ. if (δ x) τ = true τ  (δ y) τ = true τ
                       then x τ - y τ
                       else invalid τ "
interpretation OclMinusReal : profile_bind_d "(-real)" "λ x y. x - y"
         by   unfold_locales  (auto simp:OclMinusReal_def bot_option_def null_option_def)


definition OclMultReal ::"('𝔄)Real  ('𝔄)Real  ('𝔄)Real" (infix "*real" 45)
where "x *real y  λ τ. if (δ x) τ = true τ  (δ y) τ = true τ
                       then x τ * y τ
                       else invalid τ"
interpretation OclMultReal : profile_bind_d "OclMultReal" "λ x y. x * y"
         by   unfold_locales  (auto simp:OclMultReal_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 OclDivisionReal ::"('𝔄)Real  ('𝔄)Real  ('𝔄)Real" (infix "divreal" 45)
where "x divreal 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 OclModulusReal ::"('𝔄)Real  ('𝔄)Real  ('𝔄)Real" (infix "modreal" 45)
where "x modreal y  λ τ. if (δ x) τ = true τ  (δ y) τ = true τ
                       then if y τ  OclReal0 τ then mod_float x τ y τ else invalid τ 
                       else invalid τ "
(* TODO: special locale setup.*)


definition OclLessReal ::"('𝔄)Real  ('𝔄)Real  ('𝔄)Boolean" (infix "<real" 35)
where "x <real y  λ τ. if (δ x) τ = true τ  (δ y) τ = true τ
                       then x τ < y τ
                       else invalid τ "
interpretation OclLessReal : profile_bind_d "(<real)" "λ x y. x < y"
         by   unfold_locales  (auto simp:OclLessReal_def bot_option_def null_option_def)

definition OclLeReal ::"('𝔄)Real  ('𝔄)Real  ('𝔄)Boolean" (infix "real" 35)
where "x real y  λ τ. if (δ x) τ = true τ  (δ y) τ = true τ
                       then x τ  y τ
                       else invalid τ "
interpretation OclLeReal : profile_bind_d "(≤real)" "λ x y. x  y"
         by   unfold_locales  (auto simp:OclLeReal_def bot_option_def null_option_def)

subsubsection‹Basic Properties›

lemma OclAddReal_commute: "(X +real Y) = (Y +real X)"
  by(rule ext,auto simp:true_def false_def OclAddReal_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 OclAddReal_zero1[simp,code_unfold] :
"(x +real 𝟬.𝟬) = (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 +real 𝟬.𝟬) τ = (if υ x and not (δ x) then invalid else x endif) τ"
   apply(subst OclIf_true', simp add: OclValid_def)
  by (metis OclAddReal_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 +real 𝟬.𝟬) τ = (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: OclAddReal_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 OclAddReal_zero2[simp,code_unfold] :
"(𝟬.𝟬 +real x) = (if υ x and not (δ x) then invalid else x endif)"
by(subst OclAddReal_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 "τ  ( 𝟵.𝟬 real 𝟭𝟬.𝟬 )"
Assert "τ  (( 𝟰.𝟬 +real 𝟰.𝟬 ) real 𝟭𝟬.𝟬 )"
Assert "τ |≠ (( 𝟰.𝟬 +real ( 𝟰.𝟬 +real 𝟰.𝟬 )) <real 𝟭𝟬.𝟬 )"
Assert "τ  not (υ (null +real 𝟭.𝟬)) "
Assert "τ  (((𝟵.𝟬 *real 𝟰.𝟬) divreal 𝟭𝟬.𝟬) real  𝟰.𝟬) "
Assert "τ  not (δ (𝟭.𝟬 divreal 𝟬.𝟬)) "
Assert "τ  not (υ (𝟭.𝟬 divreal 𝟬.𝟬)) "



lemma real_non_null [simp]: "((λ_. n)  (null::('𝔄)Real)) = false"
by(rule ext,auto simp: StrictRefEqReal 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: StrictRefEqReal 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 "τ |≠ (𝟬.𝟬 <real null)"
Assert "τ |≠ (δ (𝟬.𝟬 <real null))"


end