Theory UML_Library

(*****************************************************************************
 * Featherweight-OCL --- A Formal Semantics for UML-OCL Version OCL 2.5
 *                       for the OMG Standard.
 *                       http://www.brucker.ch/projects/hol-testgen/
 *
 * UML_Library.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_Library
imports (* Basic Type Operations *)
        "basic_types/UML_Boolean"
        "basic_types/UML_Void"
        "basic_types/UML_Integer"
        "basic_types/UML_Real"
        "basic_types/UML_String"
        
        (* Collection Type Operations *)
        "collection_types/UML_Pair"
        "collection_types/UML_Bag"
        "collection_types/UML_Set"
        "collection_types/UML_Sequence"
begin

section‹Miscellaneous Stuff›

subsection‹Definition: asBoolean›

definition OclAsBoolean⇩I⇩n⇩t  :: "('𝔄) Integer ⇒ ('𝔄) Boolean" (‹(_)->oclAsType⇩I⇩n⇩t'(Boolean')›)
where     "OclAsBoolean⇩I⇩n⇩t X = (λτ. if (δ X) τ = true τ 
                              then ⌊⌊⌈⌈X τ⌉⌉ ≠ 0⌋⌋
                              else invalid τ)"

interpretation OclAsBoolean⇩I⇩n⇩t : profile_mono⇩d OclAsBoolean⇩I⇩n⇩t "λx. ⌊⌊⌈⌈x⌉⌉ ≠ 0⌋⌋"
                                by unfold_locales (auto simp: OclAsBoolean⇩I⇩n⇩t_def bot_option_def)

definition OclAsBoolean⇩R⇩e⇩a⇩l  :: "('𝔄) Real ⇒ ('𝔄) Boolean" (‹(_)->oclAsType⇩R⇩e⇩a⇩l'(Boolean')›)
where     "OclAsBoolean⇩R⇩e⇩a⇩l X = (λτ. if (δ X) τ = true τ 
                              then ⌊⌊⌈⌈X τ⌉⌉ ≠ 0⌋⌋
                              else invalid τ)"

interpretation OclAsBoolean⇩R⇩e⇩a⇩l : profile_mono⇩d OclAsBoolean⇩R⇩e⇩a⇩l "λx. ⌊⌊⌈⌈x⌉⌉ ≠ 0⌋⌋"
                                 by unfold_locales (auto simp: OclAsBoolean⇩R⇩e⇩a⇩l_def bot_option_def)

subsection‹Definition: asInteger›

definition OclAsInteger⇩R⇩e⇩a⇩l  :: "('𝔄) Real ⇒ ('𝔄) Integer" (‹(_)->oclAsType⇩R⇩e⇩a⇩l'(Integer')›)
where     "OclAsInteger⇩R⇩e⇩a⇩l X = (λτ. if (δ X) τ = true τ 
                              then ⌊⌊floor ⌈⌈X τ⌉⌉⌋⌋
                              else invalid τ)"

interpretation OclAsInteger⇩R⇩e⇩a⇩l : profile_mono⇩d OclAsInteger⇩R⇩e⇩a⇩l "λx. ⌊⌊floor ⌈⌈x⌉⌉⌋⌋"
                                 by unfold_locales (auto simp: OclAsInteger⇩R⇩e⇩a⇩l_def bot_option_def)

subsection‹Definition: asReal›

definition OclAsReal⇩I⇩n⇩t  :: "('𝔄) Integer ⇒ ('𝔄) Real" (‹(_)->oclAsType⇩I⇩n⇩t'(Real')›)
where     "OclAsReal⇩I⇩n⇩t X = (λτ. if (δ X) τ = true τ 
                              then ⌊⌊real_of_int ⌈⌈X τ⌉⌉⌋⌋
                              else invalid τ)"

interpretation OclAsReal⇩I⇩n⇩t : profile_mono⇩d OclAsReal⇩I⇩n⇩t "λx. ⌊⌊real_of_int ⌈⌈x⌉⌉⌋⌋"
                             by unfold_locales (auto simp: OclAsReal⇩I⇩n⇩t_def bot_option_def)

lemma Integer_subtype_of_Real: 
  assumes "τ ⊨ δ X"
  shows   "τ ⊨ X ->oclAsType⇩I⇩n⇩t(Real) ->oclAsType⇩R⇩e⇩a⇩l(Integer) ≜ X"
  apply(insert assms,  simp add: OclAsInteger⇩R⇩e⇩a⇩l_def OclAsReal⇩I⇩n⇩t_def OclValid_def StrongEq_def)
  apply(subst (2 4) cp_defined, simp add: true_def)
  by (metis assms bot_option_def drop.elims foundation16 null_option_def)

subsection‹Definition: asPair›

definition OclAsPair⇩S⇩e⇩q   :: "[('𝔄,'α::null)Sequence]⇒('𝔄,'α::null,'α::null) Pair" (‹(_)->asPair⇩S⇩e⇩q'(')›)
where     "OclAsPair⇩S⇩e⇩q S = (if S->size⇩S⇩e⇩q() ≐ 𝟮
                            then Pair{S->at⇩S⇩e⇩q(𝟬),S->at⇩S⇩e⇩q(𝟭)}
                            else invalid
                            endif)"

definition OclAsPair⇩S⇩e⇩t   :: "[('𝔄,'α::null)Set]⇒('𝔄,'α::null,'α::null) Pair" (‹(_)->asPair⇩S⇩e⇩t'(')›)
where     "OclAsPair⇩S⇩e⇩t S = (if S->size⇩S⇩e⇩t() ≐ 𝟮
                            then let v = S->any⇩S⇩e⇩t() in
                                 Pair{v,S->excluding⇩S⇩e⇩t(v)->any⇩S⇩e⇩t()}
                            else invalid
                            endif)"

definition OclAsPair⇩B⇩a⇩g   :: "[('𝔄,'α::null)Bag]⇒('𝔄,'α::null,'α::null) Pair" (‹(_)->asPair⇩B⇩a⇩g'(')›)
where     "OclAsPair⇩B⇩a⇩g S = (if S->size⇩B⇩a⇩g() ≐ 𝟮
                            then let v = S->any⇩B⇩a⇩g() in
                                 Pair{v,S->excluding⇩B⇩a⇩g(v)->any⇩B⇩a⇩g()}
                            else invalid
                            endif)"

subsection‹Definition: asSet›

definition OclAsSet⇩S⇩e⇩q   :: "[('𝔄,'α::null)Sequence]⇒('𝔄,'α)Set" (‹(_)->asSet⇩S⇩e⇩q'(')›)
where     "OclAsSet⇩S⇩e⇩q S = (S->iterate⇩S⇩e⇩q(b; x = Set{} | x ->including⇩S⇩e⇩t(b)))"

definition OclAsSet⇩P⇩a⇩i⇩r   :: "[('𝔄,'α::null,'α::null) Pair]⇒('𝔄,'α)Set" (‹(_)->asSet⇩P⇩a⇩i⇩r'(')›)
where     "OclAsSet⇩P⇩a⇩i⇩r S = Set{S .First(), S .Second()}"

definition OclAsSet⇩B⇩a⇩g   :: "('𝔄,'α::null) Bag⇒('𝔄,'α)Set" (‹(_)->asSet⇩B⇩a⇩g'(')›)
where     "OclAsSet⇩B⇩a⇩g S =  (λ τ. if (δ S) τ = true τ 
                                 then Abs_Set⇩b⇩a⇩s⇩e⌊⌊ Rep_Set_base S τ ⌋⌋ 
                                 else if (υ S) τ = true τ then null τ 
                                                          else invalid τ)"

subsection‹Definition: asSequence›

definition OclAsSeq⇩S⇩e⇩t   :: "[('𝔄,'α::null)Set]⇒('𝔄,'α)Sequence" (‹(_)->asSequence⇩S⇩e⇩t'(')›)
where     "OclAsSeq⇩S⇩e⇩t S = (S->iterate⇩S⇩e⇩t(b; x = Sequence{} | x ->including⇩S⇩e⇩q(b)))"

definition OclAsSeq⇩B⇩a⇩g   :: "[('𝔄,'α::null)Bag]⇒('𝔄,'α)Sequence" (‹(_)->asSequence⇩B⇩a⇩g'(')›)
where     "OclAsSeq⇩B⇩a⇩g S = (S->iterate⇩B⇩a⇩g(b; x = Sequence{} | x ->including⇩S⇩e⇩q(b)))"

definition OclAsSeq⇩P⇩a⇩i⇩r   :: "[('𝔄,'α::null,'α::null) Pair]⇒('𝔄,'α)Sequence" (‹(_)->asSequence⇩P⇩a⇩i⇩r'(')›)
where     "OclAsSeq⇩P⇩a⇩i⇩r S = Sequence{S .First(), S .Second()}"

subsection‹Definition: asBag›

definition OclAsBag⇩S⇩e⇩q   :: "[('𝔄,'α::null)Sequence]⇒('𝔄,'α)Bag" (‹(_)->asBag⇩S⇩e⇩q'(')›)
where     "OclAsBag⇩S⇩e⇩q S = (λτ. Abs_Bag⇩b⇩a⇩s⇩e ⌊⌊λs. if list_ex ((=) s) ⌈⌈Rep_Sequence⇩b⇩a⇩s⇩e (S τ)⌉⌉ then 1 else 0⌋⌋)"

definition OclAsBag⇩S⇩e⇩t   :: "[('𝔄,'α::null)Set]⇒('𝔄,'α)Bag" (‹(_)->asBag⇩S⇩e⇩t'(')›)
where     "OclAsBag⇩S⇩e⇩t S = (λτ. Abs_Bag⇩b⇩a⇩s⇩e ⌊⌊λs. if s ∈ ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (S τ)⌉⌉ then 1 else 0⌋⌋)"

lemma assumes "τ ⊨ δ (S ->size⇩S⇩e⇩t())" (* S is finite *)
      shows "OclAsBag⇩S⇩e⇩t S = (S->iterate⇩S⇩e⇩t(b; x = Bag{} | x ->including⇩B⇩a⇩g(b)))"
oops

definition OclAsBag⇩P⇩a⇩i⇩r   :: "[('𝔄,'α::null,'α::null) Pair]⇒('𝔄,'α)Bag" (‹(_)->asBag⇩P⇩a⇩i⇩r'(')›)
where     "OclAsBag⇩P⇩a⇩i⇩r S = Bag{S .First(), S .Second()}"

text_raw‹\isatagafp›
subsection‹Collection Types›
lemmas cp_intro'' [intro!,simp,code_unfold] =
       cp_intro'
     (*  cp_intro''⇩P⇩a⇩i⇩r *)
       cp_intro''⇩S⇩e⇩t
       cp_intro''⇩S⇩e⇩q
text_raw‹\endisatagafp›

subsection‹Test Statements›

lemma syntax_test: "Set{𝟮,𝟭} = (Set{}->including⇩S⇩e⇩t(𝟭)->including⇩S⇩e⇩t(𝟮))"
by (rule refl)

text‹Here is an example of a nested collection.›
lemma semantic_test2:
assumes H:"(Set{𝟮} ≐ null) = (false::('𝔄)Boolean)"
shows   "(τ::('𝔄)st) ⊨ (Set{Set{𝟮},null}->includes⇩S⇩e⇩t(null))"
by(simp add: OclIncludes_execute⇩S⇩e⇩t H)



lemma short_cut'[simp,code_unfold]: "(𝟴 ≐ 𝟲) = false"
 apply(rule ext)
 apply(simp add: StrictRefEq⇩I⇩n⇩t⇩e⇩g⇩e⇩r StrongEq_def OclInt8_def OclInt6_def
                 true_def false_def invalid_def bot_option_def)
done

lemma short_cut''[simp,code_unfold]: "(𝟮 ≐ 𝟭) = false"
 apply(rule ext)
 apply(simp add: StrictRefEq⇩I⇩n⇩t⇩e⇩g⇩e⇩r StrongEq_def OclInt2_def OclInt1_def
                 true_def false_def invalid_def bot_option_def)
done
lemma short_cut'''[simp,code_unfold]: "(𝟭 ≐ 𝟮) = false"
 apply(rule ext)
 apply(simp add: StrictRefEq⇩I⇩n⇩t⇩e⇩g⇩e⇩r StrongEq_def OclInt2_def OclInt1_def
                 true_def false_def invalid_def bot_option_def)
done

Assert   "τ ⊨ (𝟬 <⇩i⇩n⇩t 𝟮) and (𝟬 <⇩i⇩n⇩t 𝟭) "


text‹Elementary computations on Sets.›

declare OclSelect_body_def [simp]

Assert "¬ (τ ⊨ υ(invalid::('𝔄,'α::null) Set))"
Assert    "τ ⊨ υ(null::('𝔄,'α::null) Set)"
Assert "¬ (τ ⊨ δ(null::('𝔄,'α::null) Set))"
Assert    "τ ⊨ υ(Set{})"
Assert    "τ ⊨ υ(Set{Set{𝟮},null})"
Assert    "τ ⊨ δ(Set{Set{𝟮},null})"
Assert    "τ ⊨ (Set{𝟮,𝟭}->includes⇩S⇩e⇩t(𝟭))"
Assert "¬ (τ ⊨ (Set{𝟮}->includes⇩S⇩e⇩t(𝟭)))"
Assert "¬ (τ ⊨ (Set{𝟮,𝟭}->includes⇩S⇩e⇩t(null)))"
Assert    "τ ⊨ (Set{𝟮,null}->includes⇩S⇩e⇩t(null))"
Assert    "τ ⊨ (Set{null,𝟮}->includes⇩S⇩e⇩t(null))"

Assert    "τ ⊨ ((Set{})->forAll⇩S⇩e⇩t(z | 𝟬 <⇩i⇩n⇩t z))"

Assert    "τ ⊨ ((Set{𝟮,𝟭})->forAll⇩S⇩e⇩t(z | 𝟬 <⇩i⇩n⇩t z))"
Assert "¬ (τ ⊨ ((Set{𝟮,𝟭})->exists⇩S⇩e⇩t(z | z <⇩i⇩n⇩t 𝟬 )))"
Assert "¬ (τ ⊨ (δ(Set{𝟮,null})->forAll⇩S⇩e⇩t(z | 𝟬 <⇩i⇩n⇩t z)))"
Assert "¬ (τ ⊨ ((Set{𝟮,null})->forAll⇩S⇩e⇩t(z | 𝟬 <⇩i⇩n⇩t z)))"
Assert    "τ ⊨ ((Set{𝟮,null})->exists⇩S⇩e⇩t(z | 𝟬 <⇩i⇩n⇩t z))"


Assert "¬ (τ ⊨ (Set{null::'a Boolean} ≐ Set{}))"
Assert "¬ (τ ⊨ (Set{null::'a Integer} ≐ Set{}))"

Assert "¬ (τ ⊨ (Set{true} ≐ Set{false}))"
Assert "¬ (τ ⊨ (Set{true,true} ≐ Set{false}))"
lemma "¬ (τ ⊨ (Set{𝟮} ≐ Set{𝟭}))"
  by simp
lemma "τ ⊨ (Set{𝟮,null,𝟮} ≐ Set{null,𝟮})"
  by simp
lemma "τ ⊨ (Set{𝟭,null,𝟮} <> Set{null,𝟮})"
  by simp
lemma "τ ⊨ (Set{Set{𝟮,null}} ≐ Set{Set{null,𝟮}})"
  by simp
lemma "τ ⊨ (Set{Set{𝟮,null}} <> Set{Set{null,𝟮},null})"
  by simp
lemma "τ ⊨ (Set{null}->select⇩S⇩e⇩t(x | not x) ≐ Set{null})"
  by simp
lemma "τ ⊨ (Set{null}->reject⇩S⇩e⇩t(x | not x) ≐ Set{null})"
  by simp

lemma     "const (Set{Set{𝟮,null}, invalid})" by(simp add: const_ss)


text‹Elementary computations on Sequences.›

Assert "¬ (τ ⊨ υ(invalid::('𝔄,'α::null) Sequence))"
Assert    "τ ⊨ υ(null::('𝔄,'α::null) Sequence)"
Assert "¬ (τ ⊨ δ(null::('𝔄,'α::null) Sequence))"
Assert    "τ ⊨ υ(Sequence{})"

lemma     "const (Sequence{Sequence{𝟮,null}, invalid})" by(simp add: const_ss)

end