Theory UML_Integer

(*****************************************************************************
 * Featherweight-OCL --- A Formal Semantics for UML-OCL Version OCL 2.5
 *                       for the OMG Standard.
 *                       http://www.brucker.ch/projects/hol-testgen/
 *
 * UML_Integer.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_Integer
imports "../UML_PropertyProfiles"
begin

section‹Basic Type Integer: Operations›

subsection‹Fundamental Predicates on Integers: Strict Equality \label{sec:integer-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 :: [('𝔄)Integer,('𝔄)Integer] ⇒ ('𝔄)Boolean"
begin
  definition StrictRefEqInteger[code_unfold] :
    "(x::('𝔄)Integer) ≐ y ≡ λ τ. if (υ x) τ = true τ ∧ (υ y) τ = true τ
                                  then (x ≜ y) τ
                                  else invalid τ"
end

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

subsection‹Basic Integer Constants›

text‹Although the remaining part of this library reasons about
integers abstractly, we provide here as example some convenient shortcuts.›

definition OclInt0 ::"('𝔄)Integer" ("𝟬")  where      "𝟬 = (λ _ . ⌊⌊0::int⌋⌋)"
definition OclInt1 ::"('𝔄)Integer" ("𝟭")  where      "𝟭 = (λ _ . ⌊⌊1::int⌋⌋)"
definition OclInt2 ::"('𝔄)Integer" ("𝟮")  where      "𝟮 = (λ _ . ⌊⌊2::int⌋⌋)"
text‹Etc.›
text_raw‹\isatagafp›
definition OclInt3 ::"('𝔄)Integer" ("𝟯")  where      "𝟯 = (λ _ . ⌊⌊3::int⌋⌋)"
definition OclInt4 ::"('𝔄)Integer" ("𝟰")  where      "𝟰 = (λ _ . ⌊⌊4::int⌋⌋)"
definition OclInt5 ::"('𝔄)Integer" ("𝟱")  where      "𝟱 = (λ _ . ⌊⌊5::int⌋⌋)"
definition OclInt6 ::"('𝔄)Integer" ("𝟲")  where      "𝟲 = (λ _ . ⌊⌊6::int⌋⌋)"
definition OclInt7 ::"('𝔄)Integer" ("𝟳")  where      "𝟳 = (λ _ . ⌊⌊7::int⌋⌋)"
definition OclInt8 ::"('𝔄)Integer" ("𝟴")  where      "𝟴 = (λ _ . ⌊⌊8::int⌋⌋)"
definition OclInt9 ::"('𝔄)Integer" ("𝟵")  where      "𝟵 = (λ _ . ⌊⌊9::int⌋⌋)"
definition OclInt10 ::"('𝔄)Integer" ("𝟭𝟬")where      "𝟭𝟬 = (λ _ . ⌊⌊10::int⌋⌋)"

subsection‹Validity and Definedness Properties›

lemma  "δ(null::('𝔄)Integer) = false" by simp
lemma  "υ(null::('𝔄)Integer) = 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:OclInt0_def)
lemma [simp,code_unfold]: "υ 𝟬 = true" by(simp add:OclInt0_def)
lemma [simp,code_unfold]: "δ 𝟭 = true" by(simp add:OclInt1_def)
lemma [simp,code_unfold]: "υ 𝟭 = true" by(simp add:OclInt1_def)
lemma [simp,code_unfold]: "δ 𝟮 = true" by(simp add:OclInt2_def)
lemma [simp,code_unfold]: "υ 𝟮 = true" by(simp add:OclInt2_def)
lemma [simp,code_unfold]: "δ 𝟲 = true" by(simp add:OclInt6_def)
lemma [simp,code_unfold]: "υ 𝟲 = true" by(simp add:OclInt6_def)
lemma [simp,code_unfold]: "δ 𝟴 = true" by(simp add:OclInt8_def)
lemma [simp,code_unfold]: "υ 𝟴 = true" by(simp add:OclInt8_def)
lemma [simp,code_unfold]: "δ 𝟵 = true" by(simp add:OclInt9_def)
lemma [simp,code_unfold]: "υ 𝟵 = true" by(simp add:OclInt9_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 OclAddInteger ::"('𝔄)Integer ⇒ ('𝔄)Integer ⇒ ('𝔄)Integer" (infix "+int" 40)
where "x +int y ≡ λ τ. if (δ x) τ = true τ ∧ (δ y) τ = true τ
                       then ⌊⌊⌈⌈x τ⌉⌉ + ⌈⌈y τ⌉⌉⌋⌋
                       else invalid τ "
interpretation OclAddInteger : profile_bind_d "(+int)" "λ x y. ⌊⌊⌈⌈x⌉⌉ + ⌈⌈y⌉⌉⌋⌋"
         by unfold_locales (auto simp:OclAddInteger_def bot_option_def null_option_def)

  
definition OclMinusInteger ::"('𝔄)Integer ⇒ ('𝔄)Integer ⇒ ('𝔄)Integer" (infix "-int" 41)
where "x -int y ≡ λ τ. if (δ x) τ = true τ ∧ (δ y) τ = true τ
                       then ⌊⌊⌈⌈x τ⌉⌉ - ⌈⌈y τ⌉⌉⌋⌋
                       else invalid τ "
interpretation OclMinusInteger : profile_bind_d "(-int)" "λ x y. ⌊⌊⌈⌈x⌉⌉ - ⌈⌈y⌉⌉⌋⌋"
         by   unfold_locales  (auto simp:OclMinusInteger_def bot_option_def null_option_def)

                       
definition OclMultInteger ::"('𝔄)Integer ⇒ ('𝔄)Integer ⇒ ('𝔄)Integer" (infix "*int" 45)
where "x *int y ≡ λ τ. if (δ x) τ = true τ ∧ (δ y) τ = true τ
                       then ⌊⌊⌈⌈x τ⌉⌉ * ⌈⌈y τ⌉⌉⌋⌋
                       else invalid τ"
interpretation OclMultInteger : profile_bind_d "OclMultInteger" "λ x y. ⌊⌊⌈⌈x⌉⌉ * ⌈⌈y⌉⌉⌋⌋"
         by   unfold_locales  (auto simp:OclMultInteger_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 OclDivisionInteger ::"('𝔄)Integer ⇒ ('𝔄)Integer ⇒ ('𝔄)Integer" (infix "divint" 45)
where "x divint y ≡ λ τ. if (δ x) τ = true τ ∧ (δ y) τ = true τ
                       then if y τ ≠ OclInt0 τ then ⌊⌊⌈⌈x τ⌉⌉ div ⌈⌈y τ⌉⌉⌋⌋ else invalid τ 
                       else invalid τ "
(* TODO: special locale setup.*)

definition OclModulusInteger ::"('𝔄)Integer ⇒ ('𝔄)Integer ⇒ ('𝔄)Integer" (infix "modint" 45)
where "x modint y ≡ λ τ. if (δ x) τ = true τ ∧ (δ y) τ = true τ
                       then if y τ ≠ OclInt0 τ then ⌊⌊⌈⌈x τ⌉⌉ mod ⌈⌈y τ⌉⌉⌋⌋ else invalid τ 
                       else invalid τ "
(* TODO: special locale setup.*)
                       
                       
definition OclLessInteger ::"('𝔄)Integer ⇒ ('𝔄)Integer ⇒ ('𝔄)Boolean" (infix "<int" 35)
where "x <int y ≡ λ τ. if (δ x) τ = true τ ∧ (δ y) τ = true τ
                       then ⌊⌊⌈⌈x τ⌉⌉ < ⌈⌈y τ⌉⌉⌋⌋
                       else invalid τ "
interpretation OclLessInteger : profile_bind_d "(<int)" "λ x y. ⌊⌊⌈⌈x⌉⌉ < ⌈⌈y⌉⌉⌋⌋"
         by   unfold_locales  (auto simp:OclLessInteger_def bot_option_def null_option_def)

definition OclLeInteger ::"('𝔄)Integer ⇒ ('𝔄)Integer ⇒ ('𝔄)Boolean" (infix "≤int" 35)
where "x ≤int y ≡ λ τ. if (δ x) τ = true τ ∧ (δ y) τ = true τ
                       then ⌊⌊⌈⌈x τ⌉⌉ ≤ ⌈⌈y τ⌉⌉⌋⌋
                       else invalid τ "
interpretation OclLeInteger : profile_bind_d "(≤int)" "λ x y. ⌊⌊⌈⌈x⌉⌉ ≤ ⌈⌈y⌉⌉⌋⌋"
         by   unfold_locales  (auto simp:OclLeInteger_def bot_option_def null_option_def)

subsubsection‹Basic Properties›

lemma OclAddInteger_commute: "(X +int Y) = (Y +int X)"
  by(rule ext,auto simp:true_def false_def OclAddInteger_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 OclAddInteger_zero1[simp,code_unfold] :
"(x +int 𝟬) = (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 +int 𝟬) τ = (if υ x and not (δ x) then invalid else x endif) τ"
   apply(subst OclIf_true', simp add: OclValid_def)
  by (metis OclAddInteger_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 +int 𝟬) τ = (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: OclAddInteger_def OclInt0_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 OclAddInteger_zero2[simp,code_unfold] :
"(𝟬 +int x) = (if υ x and not (δ x) then invalid else x endif)"
by(subst OclAddInteger_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 "τ ⊨ ( 𝟵 ≤int 𝟭𝟬 )"
Assert "τ ⊨ (( 𝟰 +int 𝟰 ) ≤int 𝟭𝟬 )"
Assert "τ |≠ (( 𝟰 +int ( 𝟰 +int 𝟰 )) <int 𝟭𝟬 )"
Assert "τ ⊨ not (υ (null +int 𝟭)) "
Assert "τ ⊨ (((𝟵 *int 𝟰) divint 𝟭𝟬) ≤int  𝟰) "
Assert "τ ⊨ not (δ (𝟭 divint 𝟬)) "
Assert "τ ⊨ not (υ (𝟭 divint 𝟬)) "



lemma integer_non_null [simp]: "((λ_. ⌊⌊n⌋⌋) ≐ (null::('𝔄)Integer)) = false"
by(rule ext,auto simp: StrictRefEqInteger valid_def
                         bot_fun_def bot_option_def null_fun_def null_option_def StrongEq_def)

lemma null_non_integer [simp]: "((null::('𝔄)Integer) ≐ (λ_. ⌊⌊n⌋⌋)) = false"
by(rule ext,auto simp: StrictRefEqInteger valid_def
                         bot_fun_def bot_option_def null_fun_def null_option_def StrongEq_def)

lemma OclInt0_non_null [simp,code_unfold]: "(𝟬 ≐ null) = false" by(simp add: OclInt0_def)
lemma null_non_OclInt0 [simp,code_unfold]: "(null ≐ 𝟬) = false" by(simp add: OclInt0_def)
lemma OclInt1_non_null [simp,code_unfold]: "(𝟭 ≐ null) = false" by(simp add: OclInt1_def)
lemma null_non_OclInt1 [simp,code_unfold]: "(null ≐ 𝟭) = false" by(simp add: OclInt1_def)
lemma OclInt2_non_null [simp,code_unfold]: "(𝟮 ≐ null) = false" by(simp add: OclInt2_def)
lemma null_non_OclInt2 [simp,code_unfold]: "(null ≐ 𝟮) = false" by(simp add: OclInt2_def)
lemma OclInt6_non_null [simp,code_unfold]: "(𝟲 ≐ null) = false" by(simp add: OclInt6_def)
lemma null_non_OclInt6 [simp,code_unfold]: "(null ≐ 𝟲) = false" by(simp add: OclInt6_def)
lemma OclInt8_non_null [simp,code_unfold]: "(𝟴 ≐ null) = false" by(simp add: OclInt8_def)
lemma null_non_OclInt8 [simp,code_unfold]: "(null ≐ 𝟴) = false" by(simp add: OclInt8_def)
lemma OclInt9_non_null [simp,code_unfold]: "(𝟵 ≐ null) = false" by(simp add: OclInt9_def)
lemma null_non_OclInt9 [simp,code_unfold]: "(null ≐ 𝟵) = false" by(simp add: OclInt9_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 Integer›

Assert "τ ⊨ ((𝟬 <int 𝟮) and (𝟬 <int 𝟭))"

Assert "τ ⊨ 𝟭 <> 𝟮"
Assert "τ ⊨ 𝟮 <> 𝟭"
Assert "τ ⊨ 𝟮 ≐ 𝟮"

Assert "τ ⊨ υ 𝟰"
Assert "τ ⊨ δ 𝟰"
Assert "τ ⊨ υ (null::('𝔄)Integer)"
Assert "τ ⊨ (invalid ≜ invalid)"
Assert "τ ⊨ (null ≜ null)"
Assert "τ ⊨ (𝟰 ≜ 𝟰)"
Assert "τ |≠ (𝟵 ≜ 𝟭𝟬)"
Assert "τ |≠ (invalid ≜ 𝟭𝟬)"
Assert "τ |≠ (null ≜ 𝟭𝟬)"
Assert "τ |≠ (invalid ≐ (invalid::('𝔄)Integer))"   (* Without typeconstraint not executable.*)
Assert "τ |≠ υ (invalid ≐ (invalid::('𝔄)Integer))" (* Without typeconstraint not executable.*)
Assert "τ |≠ (invalid <> (invalid::('𝔄)Integer))"   (* Without typeconstraint not executable.*)
Assert "τ |≠ υ (invalid <> (invalid::('𝔄)Integer))" (* Without typeconstraint not executable.*)
Assert "τ ⊨ (null ≐ (null::('𝔄)Integer) )" (* Without typeconstraint not executable.*)
Assert "τ ⊨ (null ≐ (null::('𝔄)Integer) )" (* Without typeconstraint not executable.*)
Assert "τ ⊨ (𝟰 ≐ 𝟰)"
Assert "τ |≠ (𝟰 <> 𝟰)"
Assert "τ |≠ (𝟰 ≐ 𝟭𝟬)"
Assert "τ ⊨ (𝟰 <> 𝟭𝟬)"
Assert "τ |≠ (𝟬 <int null)"
Assert "τ |≠ (δ (𝟬 <int null))"


end