Theory UML_PropertyProfiles

(*****************************************************************************
 * Featherweight-OCL --- A Formal Semantics for UML-OCL Version OCL 2.5
 *                       for the OMG Standard.
 *                       http://www.brucker.ch/projects/hol-testgen/
 *
 * UML_PropertyProfiles.thy ---
 * This file is part of HOL-TestGen.
 *
 * Copyright (c) 2013-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_PropertyProfiles
imports  UML_Logic
begin

section‹Property Profiles for OCL Operators via Isabelle Locales›

text‹We use the Isabelle mechanism of a \emph{Locale} to generate the
common lemmas for each type and operator; Locales can be seen as a 
functor that takes a local theory and generates a number of theorems.
In our case, we will instantiate later these locales by the local theory 
of an operator definition and obtain the common rules for strictness, definedness
propagation, context-passingness and constance in a systematic way.
›

subsection‹Property Profiles for Monadic Operators›

locale profile_mono_scheme_defined =
   fixes f :: "('𝔄,'α::null)val ⇒ ('𝔄,'β::null)val"
   fixes g
   assumes def_scheme: "(f x) ≡ λ τ. if (δ x) τ = true τ then g (x τ) else invalid τ"
begin
   lemma strict[simp,code_unfold]: " f invalid = invalid"
   by(rule ext, simp add: def_scheme true_def false_def)
 
   lemma null_strict[simp,code_unfold]: " f null = invalid"
   by(rule ext, simp add: def_scheme true_def false_def)

   lemma cp0 : "f X τ = f (λ _. X τ) τ"
   by(simp add: def_scheme  cp_defined[symmetric])
      
   lemma cp[simp,code_unfold] : " cp P ⟹ cp (λX. f (P X) )"
   by(rule cpI1[of "f"], intro allI, rule cp0, simp_all)
    
end

locale profile_mono_schemeV =
   fixes f :: "('𝔄,'α::null)val ⇒ ('𝔄,'β::null)val"
   fixes g
   assumes def_scheme: "(f x) ≡ λ τ. if (υ x) τ = true τ then g (x τ) else invalid τ"
begin
   lemma strict[simp,code_unfold]: " f invalid = invalid"
   by(rule ext, simp add: def_scheme true_def false_def)
 
   lemma cp0 : "f X τ = f (λ _. X τ) τ"
   by(simp add: def_scheme  cp_valid[symmetric])
      
   lemma cp[simp,code_unfold] : " cp P ⟹ cp (λX. f (P X) )"
   by(rule cpI1[of "f"], intro allI, rule cp0, simp_all)
    
end

locale profile_mono⇩d = profile_mono_scheme_defined +
   assumes "⋀ x. x ≠ bot ⟹ x ≠ null ⟹ g x ≠ bot"
begin
  
   lemma const[simp,code_unfold] : 
          assumes C1 :"const X"
          shows       "const(f X)"
      proof -
        have const_g : "const (λτ. g (X τ))"  by(insert C1, auto simp:const_def, metis)
        show ?thesis   by(simp_all add : def_scheme const_ss C1 const_g)
      qed  
end

locale profile_mono0 = profile_mono_scheme_defined +
   assumes def_body:  "⋀ x. x ≠ bot ⟹ x ≠ null ⟹ g x ≠ bot ∧ g x ≠ null"

sublocale profile_mono0 < profile_mono⇩d
by(unfold_locales, simp add: def_scheme, simp add: def_body)

context profile_mono0
begin
   lemma def_homo[simp,code_unfold]: "δ(f x) = (δ x)"
   apply(rule ext, rename_tac "τ",subst foundation22[symmetric])
   apply(case_tac "¬(τ ⊨ δ x)", simp add:defined_split, elim disjE)
     apply(erule StrongEq_L_subst2_rev, simp,simp)
    apply(erule StrongEq_L_subst2_rev, simp,simp)
   apply(simp)
   apply(rule foundation13[THEN iffD2,THEN StrongEq_L_subst2_rev, where y ="δ x"])
     apply(simp_all add:def_scheme)
   apply(simp add: OclValid_def)
   by(auto simp:foundation13 StrongEq_def false_def true_def defined_def bot_fun_def null_fun_def def_body
           split: if_split_asm)

   lemma def_valid_then_def: "υ(f x) = (δ(f x))"
   apply(rule ext, rename_tac "τ",subst foundation22[symmetric])
   apply(case_tac "¬(τ ⊨ δ x)", simp add:defined_split, elim disjE)
     apply(erule StrongEq_L_subst2_rev, simp,simp)
    apply(erule StrongEq_L_subst2_rev, simp,simp)
   apply simp
   apply(simp_all add:def_scheme)
   apply(simp add: OclValid_def valid_def, subst cp_StrongEq)
   apply(subst (2) cp_defined, simp, simp add: cp_defined[symmetric])
   by(auto simp:foundation13 StrongEq_def false_def true_def defined_def bot_fun_def null_fun_def def_body
           split: if_split_asm)
end

subsection‹Property Profiles for Single›

locale profile_single =
   fixes d:: "('𝔄,'a::null)val ⇒ '𝔄 Boolean"
   assumes d_strict[simp,code_unfold]: "d invalid = false"
   assumes d_cp0: "d X τ = d (λ _. X τ) τ"
   assumes d_const[simp,code_unfold]: "const X ⟹ const (d X)"

subsection‹Property Profiles for Binary Operators›

definition "bin' f g d⇩x d⇩y X Y =
                       (f X Y = (λ τ. if (d⇩x X) τ = true τ ∧ (d⇩y Y) τ = true τ
                                      then g X Y τ
                                      else invalid τ ))"
 
definition "bin f g = bin' f (λX Y τ. g (X τ) (Y τ))"

lemmas [simp,code_unfold] = bin'_def bin_def

locale profile_bin_scheme =
   fixes d⇩x:: "('𝔄,'a::null)val ⇒ '𝔄 Boolean"
   fixes d⇩y:: "('𝔄,'b::null)val ⇒ '𝔄 Boolean"
   fixes f::"('𝔄,'a::null)val ⇒ ('𝔄,'b::null)val ⇒ ('𝔄,'c::null)val"
   fixes g
   assumes d⇩x' : "profile_single d⇩x"
   assumes d⇩y' : "profile_single d⇩y"
   assumes d⇩x_d⇩y_homo[simp,code_unfold]: "cp (f X) ⟹ 
                          cp (λx. f x Y) ⟹ 
                          f X invalid = invalid ⟹
                          f invalid Y = invalid ⟹
                          (¬ (τ ⊨ d⇩x X) ∨ ¬ (τ ⊨ d⇩y Y)) ⟹
                          τ ⊨ (δ f X Y ≜ (d⇩x X and d⇩y Y))"
   assumes def_scheme''[simplified]: "bin f g d⇩x d⇩y X Y"
   assumes 1: "τ ⊨ d⇩x X ⟹ τ ⊨ d⇩y Y ⟹ τ ⊨ δ f X Y"
begin
      interpretation d⇩x : profile_single d⇩x by (rule d⇩x')
      interpretation d⇩y : profile_single d⇩y by (rule d⇩y')

      lemma strict1[simp,code_unfold]: " f invalid y = invalid"
      by(rule ext, simp add: def_scheme'' true_def false_def)

      lemma strict2[simp,code_unfold]: " f x invalid = invalid"
      by(rule ext, simp add: def_scheme'' true_def false_def)

      lemma cp0 : "f X Y τ = f (λ _. X τ) (λ _. Y τ) τ"
      by(simp add: def_scheme'' d⇩x.d_cp0[symmetric] d⇩y.d_cp0[symmetric] cp_defined[symmetric])
      
      lemma cp[simp,code_unfold] : " cp P ⟹ cp Q ⟹ cp (λX. f (P X) (Q X))"
      by(rule cpI2[of "f"], intro allI, rule cp0, simp_all)

      lemma def_homo[simp,code_unfold]: "δ(f x y) = (d⇩x x and d⇩y y)"
         apply(rule ext, rename_tac "τ",subst foundation22[symmetric])
         apply(case_tac "¬(τ ⊨ d⇩x x)", simp)
         apply(case_tac "¬(τ ⊨ d⇩y y)", simp)
         apply(simp)
         apply(rule foundation13[THEN iffD2,THEN StrongEq_L_subst2_rev, where y ="d⇩x x"])
           apply(simp_all)
         apply(rule foundation13[THEN iffD2,THEN StrongEq_L_subst2_rev, where y ="d⇩y y"])
           apply(simp_all add: 1 foundation13)
         done

      lemma def_valid_then_def: "υ(f x y) = (δ(f x y))" (* [simp,code_unfold] ? *)
         apply(rule ext, rename_tac "τ") 
         apply(simp_all add: valid_def defined_def def_scheme''
                             true_def false_def invalid_def 
                             null_def null_fun_def null_option_def bot_fun_def)
         by (metis "1" OclValid_def def_scheme'' foundation16 true_def)

      lemma defined_args_valid: "(τ ⊨ δ (f x y)) = ((τ ⊨ d⇩x x) ∧ (τ ⊨ d⇩y y))"
         by(simp add: foundation10')

      lemma const[simp,code_unfold] : 
          assumes C1 :"const X" and C2 : "const Y"
          shows       "const(f X Y)"
      proof -
          have const_g : "const (λτ. g (X τ) (Y τ))" 
                  by(insert C1 C2, auto simp:const_def, metis)
        show ?thesis
        by(simp_all add : def_scheme'' const_ss C1 C2 const_g)
      qed
end


text‹
In our context, we will use Locales as ``Property Profiles'' for OCL operators;
if an operator @{term "f"} is of profile @{term "profile_bin_scheme defined f g"} we know
that it satisfies a number of properties like ‹strict1› or ‹strict2›
\ie{} @{term "f invalid y = invalid"} and @{term "f null y = invalid"}.
Since some of the more advanced Locales come with 10 - 15 theorems, property profiles
represent a major structuring mechanism for the OCL library.
›


locale profile_bin_scheme_defined =
   fixes d⇩y:: "('𝔄,'b::null)val ⇒ '𝔄 Boolean"
   fixes f::"('𝔄,'a::null)val ⇒ ('𝔄,'b::null)val ⇒ ('𝔄,'c::null)val"
   fixes g
   assumes d⇩y : "profile_single d⇩y"
   assumes d⇩y_homo[simp,code_unfold]: "cp (f X) ⟹ 
                          f X invalid = invalid ⟹
                          ¬ τ ⊨ d⇩y Y ⟹
                          τ ⊨ δ f X Y ≜ (δ X and d⇩y Y)"
   assumes def_scheme'[simplified]: "bin f g defined d⇩y X Y"
   assumes def_body':  "⋀ x y τ. x≠bot ⟹ x≠null ⟹ (d⇩y y) τ = true τ ⟹ g x (y τ) ≠ bot ∧ g x (y τ) ≠ null "
begin
      lemma strict3[simp,code_unfold]: " f null y = invalid"
      by(rule ext, simp add: def_scheme' true_def false_def)
end

sublocale profile_bin_scheme_defined < profile_bin_scheme defined
proof - 
      interpret d⇩y : profile_single d⇩y by (rule d⇩y)
 show "profile_bin_scheme defined d⇩y f g"
 apply(unfold_locales)
      apply(simp)+
     apply(subst cp_defined, simp)
    apply(rule const_defined, simp)
   apply(simp add:defined_split, elim disjE)
     apply(erule StrongEq_L_subst2_rev, simp, simp)+
   apply(simp)
  apply(simp add: def_scheme')
 apply(simp add: defined_def OclValid_def false_def true_def 
              bot_fun_def null_fun_def def_scheme' split: if_split_asm, rule def_body')
 by(simp add: true_def)+
qed

locale profile_bin⇩d_⇩d =
   fixes f::"('𝔄,'a::null)val ⇒ ('𝔄,'b::null)val ⇒ ('𝔄,'c::null)val"
   fixes g
   assumes def_scheme[simplified]: "bin f g defined defined X Y"
   assumes def_body:  "⋀ x y. x≠bot ⟹ x≠null ⟹ y≠bot ⟹ y≠null ⟹
                               g x y ≠ bot ∧ g x y ≠ null "
begin
      lemma strict4[simp,code_unfold]: " f x null = invalid"
      by(rule ext, simp add: def_scheme true_def false_def)
end

sublocale profile_bin⇩d_⇩d < profile_bin_scheme_defined defined
 apply(unfold_locales)
      apply(simp)+
     apply(subst cp_defined, simp)+
    apply(rule const_defined, simp)+
   apply(simp add:defined_split, elim disjE)
    apply(erule StrongEq_L_subst2_rev, simp, simp)+
  apply(simp add: def_scheme)
 apply(simp add: defined_def OclValid_def false_def true_def bot_fun_def null_fun_def def_scheme)
 apply(rule def_body, simp_all add: true_def false_def split:if_split_asm)
done

locale profile_bin⇩d_⇩v =
   fixes f::"('𝔄,'a::null)val ⇒ ('𝔄,'b::null)val ⇒ ('𝔄,'c::null)val"
   fixes g
   assumes def_scheme[simplified]: "bin f g defined valid X Y"
   assumes def_body:  "⋀ x y. x≠bot ⟹ x≠null ⟹ y≠bot ⟹ g x y ≠ bot ∧ g x y ≠ null"

sublocale profile_bin⇩d_⇩v < profile_bin_scheme_defined valid
 apply(unfold_locales)
      apply(simp)
     apply(subst cp_valid, simp)
    apply(rule const_valid, simp)
   apply(simp add:foundation18'')
   apply(erule StrongEq_L_subst2_rev, simp, simp)
  apply(simp add: def_scheme)
 by (metis OclValid_def def_body foundation18')
 
locale profile_bin⇩S⇩t⇩r⇩o⇩n⇩g⇩E⇩q_⇩v_⇩v =
   fixes f :: "('𝔄,'α::null)val ⇒ ('𝔄,'α::null)val ⇒ ('𝔄) Boolean"
   assumes def_scheme[simplified]: "bin' f StrongEq valid valid X Y"

sublocale profile_bin⇩S⇩t⇩r⇩o⇩n⇩g⇩E⇩q_⇩v_⇩v < profile_bin_scheme valid valid f "λx y. ⌊⌊x = y⌋⌋"
 apply(unfold_locales)
      apply(simp)
     apply(subst cp_valid, simp)
    apply (simp add: const_valid)
   apply (metis (opaque_lifting, mono_tags) OclValid_def def_scheme defined5 defined6 defined_and_I foundation1 foundation10' foundation16' foundation18 foundation21 foundation22 foundation9)
  apply(simp add: def_scheme, subst StrongEq_def, simp)
 by (metis OclValid_def def_scheme defined7 foundation16)

context profile_bin⇩S⇩t⇩r⇩o⇩n⇩g⇩E⇩q_⇩v_⇩v
   begin
      lemma idem[simp,code_unfold]: " f null null = true"
      by(rule ext, simp add: def_scheme true_def false_def)

      (* definedness *)
      lemma defargs: "τ ⊨ f x y ⟹ (τ ⊨ υ x) ∧ (τ ⊨ υ y)"
         by(simp add: def_scheme OclValid_def true_def invalid_def valid_def bot_option_def
               split: bool.split_asm HOL.if_split_asm)

      lemma defined_args_valid' : "δ (f x y) = (υ x and υ y)"
      by(auto intro!: transform2_rev defined_and_I simp:foundation10 defined_args_valid)

      (* logic and algebraic properties *)
      lemma refl_ext[simp,code_unfold] : "(f x x) = (if (υ x) then true else invalid endif)"
         by(rule ext, simp add: def_scheme OclIf_def)
      
      lemma sym : "τ ⊨ (f x y) ⟹ τ ⊨ (f y x)"  
         apply(case_tac "τ ⊨ υ x")
          apply(auto simp: def_scheme OclValid_def)
         by(fold OclValid_def, erule StrongEq_L_sym)

      lemma symmetric : "(f x y) = (f y x)"  
         by(rule ext, rename_tac τ, auto simp: def_scheme StrongEq_sym)
      
      lemma trans : "τ ⊨ (f x y) ⟹ τ ⊨ (f y z) ⟹ τ ⊨ (f x z)"  
         apply(case_tac "τ ⊨ υ x")
          apply(case_tac "τ ⊨ υ y")
           apply(auto simp: def_scheme OclValid_def)
         by(fold OclValid_def, auto elim: StrongEq_L_trans)
         
      lemma StrictRefEq_vs_StrongEq: "τ ⊨(υ x) ⟹ τ ⊨(υ y) ⟹ (τ ⊨ ((f x y) ≜ (x ≜ y)))"
         apply(simp add: def_scheme OclValid_def)
         apply(subst cp_StrongEq[of _ "(x ≜ y)"])
         by simp
         
   end

   
locale profile_bin⇩v_⇩v =
   fixes f :: "('𝔄,'α::null)val ⇒ ('𝔄,'β::null)val ⇒ ('𝔄,'γ::null)val"
   fixes g
   assumes def_scheme[simplified]: "bin f g valid valid X Y"
   assumes def_body:  "⋀ x y. x≠bot ⟹ y≠bot ⟹ g x y ≠ bot ∧ g x y ≠ null"

sublocale profile_bin⇩v_⇩v < profile_bin_scheme valid valid
 apply(unfold_locales)
         apply(simp, subst cp_valid, simp, rule const_valid, simp)+
   apply (metis (opaque_lifting, mono_tags) OclValid_def def_scheme defined5 defined6 defined_and_I 
         foundation1 foundation10' foundation16' foundation18 foundation21 foundation22 foundation9)
  apply(simp add: def_scheme)
 apply(simp add: defined_def OclValid_def false_def true_def 
              bot_fun_def null_fun_def def_scheme split: if_split_asm, rule def_body)
 by (metis OclValid_def foundation18' true_def)+

end