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_monod = 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_monod
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 dx dy X Y =
                       (f X Y = (λ τ. if (dx X) τ = true τ  (dy 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 dx:: "('𝔄,'a::null)val  '𝔄 Boolean"
   fixes dy:: "('𝔄,'b::null)val  '𝔄 Boolean"
   fixes f::"('𝔄,'a::null)val  ('𝔄,'b::null)val  ('𝔄,'c::null)val"
   fixes g
   assumes dx' : "profile_single dx"
   assumes dy' : "profile_single dy"
   assumes dx_dy_homo[simp,code_unfold]: "cp (f X)  
                          cp (λx. f x Y)  
                          f X invalid = invalid 
                          f invalid Y = invalid 
                          (¬ (τ  dx X)  ¬ (τ  dy Y)) 
                          τ  (δ f X Y  (dx X and dy Y))"
   assumes def_scheme''[simplified]: "bin f g dx dy X Y"
   assumes 1: "τ  dx X  τ  dy Y  τ  δ f X Y"
begin
      interpretation dx : profile_single dx by (rule dx')
      interpretation dy : profile_single dy by (rule dy')

      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'' dx.d_cp0[symmetric] dy.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) = (dx x and dy y)"
         apply(rule ext, rename_tac "τ",subst foundation22[symmetric])
         apply(case_tac "¬(τ  dx x)", simp)
         apply(case_tac "¬(τ  dy y)", simp)
         apply(simp)
         apply(rule foundation13[THEN iffD2,THEN StrongEq_L_subst2_rev, where y ="dx x"])
           apply(simp_all)
         apply(rule foundation13[THEN iffD2,THEN StrongEq_L_subst2_rev, where y ="dy 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)) = ((τ  dx x)  (τ  dy 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 dy:: "('𝔄,'b::null)val  '𝔄 Boolean"
   fixes f::"('𝔄,'a::null)val  ('𝔄,'b::null)val  ('𝔄,'c::null)val"
   fixes g
   assumes dy : "profile_single dy"
   assumes dy_homo[simp,code_unfold]: "cp (f X)  
                          f X invalid = invalid 
                          ¬ τ  dy Y 
                          τ  δ f X Y  (δ X and dy Y)"
   assumes def_scheme'[simplified]: "bin f g defined dy X Y"
   assumes def_body':  " x y τ. xbot  xnull  (dy 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 dy : profile_single dy by (rule dy)
 show "profile_bin_scheme defined dy 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_bind_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. xbot  xnull  ybot  ynull 
                               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_bind_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_bind_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. xbot  xnull  ybot  g x y  bot  g x y  null"

sublocale profile_bind_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_binStrongEq_v_v =
   fixes f :: "('𝔄,::null)val  ('𝔄,::null)val  ('𝔄) Boolean"
   assumes def_scheme[simplified]: "bin' f StrongEq valid valid X Y"

sublocale profile_binStrongEq_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_binStrongEq_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_binv_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. xbot  ybot  g x y  bot  g x y  null"

sublocale profile_binv_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