Theory UML_Boolean

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


subsection‹Fundamental Predicates on Basic Types: Strict (Referential) Equality›
text‹
  Here is a first instance of a definition of strict value equality---for
  the special case of the type @{typ "('𝔄)Boolean"}, it is just
  the strict extension of the logical
  equality:
›
overloading StrictRefEq ≡ "StrictRefEq :: [('𝔄)Boolean,('𝔄)Boolean] ⇒ ('𝔄)Boolean"
begin
  definition StrictRefEq⇩B⇩o⇩o⇩l⇩e⇩a⇩n[code_unfold] :
    "(x::('𝔄)Boolean) ≐ y ≡ λ τ. if (υ x) τ = true τ ∧ (υ y) τ = true τ
                                  then (x ≜ y)τ
                                  else invalid τ"
end

text‹which implies elementary properties like:›
lemma [simp,code_unfold] : "(true ≐ false) = false"
by(simp add:StrictRefEq⇩B⇩o⇩o⇩l⇩e⇩a⇩n)
lemma [simp,code_unfold] : "(false ≐ true) = false"
by(simp add:StrictRefEq⇩B⇩o⇩o⇩l⇩e⇩a⇩n)

lemma null_non_false [simp,code_unfold]:"(null ≐ false) = false"
 apply(rule ext, simp add: StrictRefEq⇩B⇩o⇩o⇩l⇩e⇩a⇩n StrongEq_def false_def)
 by (metis drop.simps cp_valid false_def is_none_code(2) Option.is_none_def valid4
           bot_option_def null_fun_def null_option_def)

lemma null_non_true [simp,code_unfold]:"(null ≐ true) = false"
 apply(rule ext, simp add: StrictRefEq⇩B⇩o⇩o⇩l⇩e⇩a⇩n StrongEq_def false_def)
 by(simp add: true_def bot_option_def null_fun_def null_option_def)

lemma false_non_null [simp,code_unfold]:"(false ≐ null) = false"
 apply(rule ext, simp add: StrictRefEq⇩B⇩o⇩o⇩l⇩e⇩a⇩n StrongEq_def false_def)
 by(metis drop.simps cp_valid false_def is_none_code(2) Option.is_none_def valid4
          bot_option_def null_fun_def null_option_def )

lemma true_non_null [simp,code_unfold]:"(true ≐ null) = false"
 apply(rule ext, simp add: StrictRefEq⇩B⇩o⇩o⇩l⇩e⇩a⇩n StrongEq_def false_def)
 by(simp add: true_def bot_option_def null_fun_def null_option_def)

text‹With respect to strictness properties and miscelleaneous side-calculi,
strict referential equality behaves on booleans as described in the
@{term "profile_bin⇩S⇩t⇩r⇩o⇩n⇩g⇩E⇩q_⇩v_⇩v"}:›
interpretation StrictRefEq⇩B⇩o⇩o⇩l⇩e⇩a⇩n : profile_bin⇩S⇩t⇩r⇩o⇩n⇩g⇩E⇩q_⇩v_⇩v "λ x y. (x::('𝔄)Boolean) ≐ y" 
         by unfold_locales (auto simp:StrictRefEq⇩B⇩o⇩o⇩l⇩e⇩a⇩n)
         
text‹In particular, it is strict, cp-preserving and const-preserving. In particular,
it generates the simplifier rules for terms like:›
lemma "(invalid ≐ false) = invalid" by(simp)
lemma "(invalid ≐ true) = invalid"  by(simp)
lemma "(false ≐ invalid) = invalid" by(simp)
lemma "(true ≐ invalid) = invalid"  by(simp)
lemma "((invalid::('𝔄)Boolean) ≐ invalid) = invalid" by(simp)
text‹Thus, the weak equality is \emph{not} reflexive.›



subsection‹Test Statements on Boolean Operations.›
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 Boolean›
Assert "τ ⊨ υ(true)"
Assert "τ ⊨ δ(false)"
Assert "τ |≠ δ(null)"
Assert "τ |≠ δ(invalid)"
Assert "τ ⊨ υ((null::('𝔄)Boolean))"
Assert "τ |≠ υ(invalid)"
Assert "τ ⊨ (true and true)"
Assert "τ ⊨ (true and true ≜ true)"
Assert "τ ⊨ ((null or null) ≜ null)"
Assert "τ ⊨ ((null or null) ≐ null)"
Assert "τ ⊨ ((true ≜ false) ≜ false)"
Assert "τ ⊨ ((invalid ≜ false) ≜ false)"
Assert "τ ⊨ ((invalid ≐ false) ≜ invalid)"
Assert "τ ⊨ (true <> false)"
Assert "τ ⊨ (false <> true)"


end