Theory UML_Void

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

section‹Basic Type Void: Operations›

(* For technical reasons, the type does not contain to the null-class yet. *)
text ‹This \emph{minimal} OCL type contains only two elements:
@{term "invalid"} and @{term "null"}.
@{term "Void"} could initially be defined as @{typ "unit option option"},
however the cardinal of this type is more than two, so it would have the cost to consider
 ‹Some None› and ‹Some (Some ())› seemingly everywhere.›
 
subsection‹Fundamental Properties on Voids: Strict Equality›

subsubsection‹Definition›

instantiation   Voidbase  :: bot
begin
   definition bot_Void_def: "(bot_class.bot :: Voidbase) ≡ Abs_Voidbase None"

   instance proof show "∃x:: Voidbase. x ≠ bot"
                  apply(rule_tac x="Abs_Voidbase ⌊None⌋" in exI)
                  apply(simp add:bot_Void_def, subst Abs_Voidbase_inject)
                  apply(simp_all add: null_option_def bot_option_def)
                  done
            qed
end

instantiation   Voidbase :: null
begin
   definition null_Void_def: "(null::Voidbase) ≡ Abs_Voidbase ⌊ None ⌋"

   instance proof show "(null:: Voidbase) ≠ bot"
                  apply(simp add:null_Void_def bot_Void_def, subst Abs_Voidbase_inject)
                  apply(simp_all add: null_option_def bot_option_def)
                  done
            qed
end


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 "('𝔄)Void"}-case as strict extension of the strong equality:›
overloading StrictRefEq ≡ "StrictRefEq :: [('𝔄)Void,('𝔄)Void] ⇒ ('𝔄)Boolean"
begin
  definition StrictRefEqVoid[code_unfold] :
    "(x::('𝔄)Void) ≐ y ≡ λ τ. if (υ x) τ = true τ ∧ (υ y) τ = true τ
                               then (x ≜ y) τ
                               else invalid τ"
end

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


subsection‹Validity and Definedness Properties›

lemma  "δ(null::('𝔄)Void) = false" by simp
lemma  "υ(null::('𝔄)Void) = true"  by simp

lemma [simp,code_unfold]: "δ (λ_. Abs_Voidbase None) = false"
apply(simp add:defined_def true_def
               bot_fun_def bot_option_def)
apply(rule ext, simp split:, intro conjI impI)
by(simp add: bot_Void_def)

lemma [simp,code_unfold]: "υ (λ_. Abs_Voidbase None) = false"
apply(simp add:valid_def true_def
               bot_fun_def bot_option_def)
apply(rule ext, simp split:, intro conjI impI)
by(simp add: bot_Void_def)

lemma [simp,code_unfold]: "δ (λ_. Abs_Voidbase ⌊None⌋) = false"
apply(simp add:defined_def true_def
               bot_fun_def bot_option_def null_fun_def null_option_def)
apply(rule ext, simp split:, intro conjI impI)
by(simp add: null_Void_def)

lemma [simp,code_unfold]: "υ (λ_. Abs_Voidbase ⌊None⌋) = true"
apply(simp add:valid_def true_def
               bot_fun_def bot_option_def)
apply(rule ext, simp split:, intro conjI impI)
by(metis null_Void_def null_is_valid, simp add: true_def)


subsection‹Test Statements›

Assert "τ ⊨ ((null::('𝔄)Void)  ≐ null)"


end