Theory UML_String

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

section‹Basic Type String: Operations›

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

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

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

definition OclStringa ::"('𝔄)String" (‹𝖺›)    where      "𝖺 = (λ _ . ⌊⌊''a''⌋⌋)"
definition OclStringb ::"('𝔄)String" (‹𝖻›)    where      "𝖻 = (λ _ . ⌊⌊''b''⌋⌋)"
definition OclStringc ::"('𝔄)String" (‹𝖼›)    where      "𝖼 = (λ _ . ⌊⌊''c''⌋⌋)"
text‹Etc.›
text_raw‹\isatagafp›

subsection‹Validity and Definedness Properties›

lemma  "δ(null::('𝔄)String) = false" by simp
lemma  "υ(null::('𝔄)String) = 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:OclStringa_def)
lemma [simp,code_unfold]: "υ 𝖺 = true" by(simp add:OclStringa_def)
text_raw‹\endisatagafp›

subsection‹String 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 OclAddString ::"('𝔄)String ⇒ ('𝔄)String ⇒ ('𝔄)String" (infix ‹+string› 40)
where "x +string y ≡ λ τ. if (δ x) τ = true τ ∧ (δ y) τ = true τ
                       then ⌊⌊concat [⌈⌈x τ⌉⌉, ⌈⌈y τ⌉⌉]⌋⌋
                       else invalid τ "
interpretation OclAddString : profile_bind_d "(+string)" "λ x y. ⌊⌊concat [⌈⌈x⌉⌉, ⌈⌈y⌉⌉]⌋⌋"
         by unfold_locales (auto simp:OclAddString_def bot_option_def null_option_def)
         
(* TODO : size(), concat, substring(s:string) toInteger, toReal, at(i:Integer), characters() etc. *)


subsubsection‹Basic Properties›

lemma OclAddString_not_commute: "∃X Y. (X +string Y) ≠ (Y +string X)"
  apply(rule_tac x = "λ_. ⌊⌊''b''⌋⌋" in exI)
  apply(rule_tac x = "λ_. ⌊⌊''a''⌋⌋" in exI)
  apply(simp_all add:OclAddString_def)
  by(auto, drule fun_cong, auto)


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 "τ ⊨ ( 𝟵 ≤string 𝟭𝟬 )"
Assert "τ ⊨ (( 𝟰 +string 𝟰 ) ≤string 𝟭𝟬 )"
Assert "τ |≠ (( 𝟰 +string ( 𝟰 +string 𝟰 )) <string 𝟭𝟬 )"
Assert "τ ⊨ not (υ (null +string 𝟭)) "
*)

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 String›

Assert "τ ⊨ 𝖺 <> 𝖻"
Assert "τ ⊨ 𝖻 <> 𝖺"
Assert "τ ⊨ 𝖻 ≐ 𝖻"

Assert "τ ⊨ υ 𝖺"
Assert "τ ⊨ δ 𝖺"
Assert "τ ⊨ υ (null::('𝔄)String)"
Assert "τ ⊨ (invalid ≜ invalid)"
Assert "τ ⊨ (null ≜ null)"
Assert "τ ⊨ (𝖺 ≜ 𝖺)"
Assert "τ |≠ (𝖺 ≜ 𝖻)"
Assert "τ |≠ (invalid ≜ 𝖻)"
Assert "τ |≠ (null ≜ 𝖻)"
Assert "τ |≠ (invalid ≐ (invalid::('𝔄)String))" (* Without typeconstraint not executable.*)
Assert "τ |≠ υ (invalid ≐ (invalid::('𝔄)String))" (* Without typeconstraint not executable.*)
Assert "τ |≠ (invalid <> (invalid::('𝔄)String))" (* Without typeconstraint not executable.*)
Assert "τ |≠ υ (invalid <> (invalid::('𝔄)String))" (* Without typeconstraint not executable.*)
Assert "τ ⊨ (null ≐ (null::('𝔄)String) )" (* Without typeconstraint not executable.*)
Assert "τ ⊨ (null ≐ (null::('𝔄)String) )" (* Without typeconstraint not executable.*)
Assert "τ ⊨ (𝖻 ≐ 𝖻)"
Assert "τ |≠ (𝖻 <> 𝖻)"
Assert "τ |≠ (𝖻 ≐ 𝖼)"
Assert "τ ⊨ (𝖻 <> 𝖼)"
(*Assert "τ |≠ (𝟬 <string null)"
Assert "τ |≠ (δ (𝟬 <string null))"
*)

end