Theory UML_Set

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

no_notation None ("⊥")
section‹Collection Type Set: Operations \label{formal-set}›

subsection‹As a Motivation for the (infinite) Type Construction: Type-Extensions as Sets 
             \label{sec:type-extensions}›

text‹Our notion of typed set goes beyond the usual notion of a finite executable set and
is powerful enough to capture \emph{the extension of a type} in UML and OCL. This means
we can have in Featherweight OCL Sets containing all possible elements of a type, not only
those (finite) ones representable in a state. This holds for base types as well as class types,
although the notion for class-types --- involving object id's not occurring in a state ---
requires some care.

In a world with @{term invalid} and @{term null}, there are two notions extensions possible:
\begin{enumerate}
\item the set of all \emph{defined} values of a type @{term T}
      (for which we will introduce the constant  @{term T})
\item the set of all \emph{valid} values of a type @{term T}, so including @{term null}
      (for which we will introduce the constant  @{term T⇩n⇩u⇩l⇩l}).
\end{enumerate}
›

text‹We define the set extensions for the base type @{term Integer} as follows:›
definition Integer :: "('𝔄,Integer⇩b⇩a⇩s⇩e) Set"
where     "Integer ≡ (λ τ. (Abs_Set⇩b⇩a⇩s⇩e o Some o Some)  ((Some o Some) ` (UNIV::int set)))"

definition Integer⇩n⇩u⇩l⇩l :: "('𝔄,Integer⇩b⇩a⇩s⇩e) Set"
where     "Integer⇩n⇩u⇩l⇩l ≡ (λ τ. (Abs_Set⇩b⇩a⇩s⇩e o Some o Some)  (Some ` (UNIV::int option set)))"

lemma Integer_defined : "δ Integer = true"
apply(rule ext, auto simp: Integer_def defined_def false_def true_def
                           bot_fun_def null_fun_def null_option_def)
by(simp_all add: Abs_Set⇩b⇩a⇩s⇩e_inject bot_option_def bot_Set⇩b⇩a⇩s⇩e_def null_Set⇩b⇩a⇩s⇩e_def null_option_def)

lemma Integer⇩n⇩u⇩l⇩l_defined : "δ Integer⇩n⇩u⇩l⇩l = true"
apply(rule ext, auto simp: Integer⇩n⇩u⇩l⇩l_def defined_def false_def true_def
                           bot_fun_def null_fun_def null_option_def)
by(simp_all add: Abs_Set⇩b⇩a⇩s⇩e_inject bot_option_def bot_Set⇩b⇩a⇩s⇩e_def null_Set⇩b⇩a⇩s⇩e_def null_option_def)

text‹This allows the theorems:

      ‹τ ⊨ δ x  ⟹ τ ⊨ (Integer->includes⇩S⇩e⇩t(x))›
      ‹τ ⊨ δ x  ⟹ τ ⊨ Integer  ≜ (Integer->including⇩S⇩e⇩t(x))›

and

      ‹τ ⊨ υ x  ⟹ τ ⊨ (Integer⇩n⇩u⇩l⇩l->includes⇩S⇩e⇩t(x))›
      ‹τ ⊨ υ x  ⟹ τ ⊨ Integer⇩n⇩u⇩l⇩l  ≜ (Integer⇩n⇩u⇩l⇩l->including⇩S⇩e⇩t(x))›

which characterize the infiniteness of these sets by a recursive property on these sets.
›

text‹In the same spirit, we proceed similarly for the remaining base types:›

definition Void⇩n⇩u⇩l⇩l :: "('𝔄,Void⇩b⇩a⇩s⇩e) Set"
where     "Void⇩n⇩u⇩l⇩l ≡ (λ τ. (Abs_Set⇩b⇩a⇩s⇩e o Some o Some) {Abs_Void⇩b⇩a⇩s⇩e (Some None)})"

definition Void⇩e⇩m⇩p⇩t⇩y :: "('𝔄,Void⇩b⇩a⇩s⇩e) Set"
where     "Void⇩e⇩m⇩p⇩t⇩y ≡ (λ τ. (Abs_Set⇩b⇩a⇩s⇩e o Some o Some) {})"

lemma Void⇩n⇩u⇩l⇩l_defined : "δ Void⇩n⇩u⇩l⇩l = true"
apply(rule ext, auto simp: Void⇩n⇩u⇩l⇩l_def defined_def false_def true_def
                           bot_fun_def null_fun_def null_option_def
                           bot_Set⇩b⇩a⇩s⇩e_def null_Set⇩b⇩a⇩s⇩e_def)
by((subst (asm) Abs_Set⇩b⇩a⇩s⇩e_inject, auto simp add: bot_option_def null_option_def bot_Void_def),
   (subst (asm) Abs_Void⇩b⇩a⇩s⇩e_inject, auto simp add: bot_option_def null_option_def))+

lemma Void⇩e⇩m⇩p⇩t⇩y_defined : "δ Void⇩e⇩m⇩p⇩t⇩y = true"
apply(rule ext, auto simp: Void⇩e⇩m⇩p⇩t⇩y_def defined_def false_def true_def
                           bot_fun_def null_fun_def null_option_def
                           bot_Set⇩b⇩a⇩s⇩e_def null_Set⇩b⇩a⇩s⇩e_def)
by((subst (asm) Abs_Set⇩b⇩a⇩s⇩e_inject, auto simp add: bot_option_def null_option_def bot_Void_def))+

lemma assumes "τ ⊨ δ (V :: ('𝔄,Void⇩b⇩a⇩s⇩e) Set)"
      shows   "τ ⊨ V ≜ Void⇩n⇩u⇩l⇩l ∨ τ ⊨ V ≜ Void⇩e⇩m⇩p⇩t⇩y"
proof -
  have A:"⋀x y. x ≠ {} ⟹ ∃y. y∈ x"
  by (metis all_not_in_conv)
show "?thesis"
  apply(case_tac "V τ")
  proof - fix y show "V τ = Abs_Set⇩b⇩a⇩s⇩e y ⟹
                      y ∈ {X. X = ⊥ ∨ X = null ∨ (∀x∈⌈⌈X⌉⌉. x ≠ ⊥)} ⟹
                      τ ⊨ V ≜ Void⇩n⇩u⇩l⇩l ∨ τ ⊨ V ≜ Void⇩e⇩m⇩p⇩t⇩y"
  apply(insert assms, case_tac y, simp add: bot_option_def, simp add: bot_Set⇩b⇩a⇩s⇩e_def foundation16)
  apply(simp add: bot_option_def null_option_def)
  apply(erule disjE, metis OclValid_def defined_def foundation2 null_Set⇩b⇩a⇩s⇩e_def null_fun_def true_def)
  proof - fix a show "V τ = Abs_Set⇩b⇩a⇩s⇩e ⌊a⌋ ⟹ ∀x∈⌈a⌉. x ≠ ⊥ ⟹ τ ⊨ V ≜ Void⇩n⇩u⇩l⇩l ∨ τ ⊨ V ≜ Void⇩e⇩m⇩p⇩t⇩y"
  apply(case_tac a, simp, insert assms, metis OclValid_def foundation16 null_Set⇩b⇩a⇩s⇩e_def true_def)
  apply(simp)
  proof - fix aa show " V τ = Abs_Set⇩b⇩a⇩s⇩e ⌊⌊aa⌋⌋ ⟹ ∀x∈aa. x ≠ ⊥ ⟹ τ ⊨ V ≜ Void⇩n⇩u⇩l⇩l ∨ τ ⊨ V ≜ Void⇩e⇩m⇩p⇩t⇩y"
  apply(case_tac "aa = {}",
        rule disjI2,
        insert assms,
        simp add: Void⇩e⇩m⇩p⇩t⇩y_def OclValid_def StrongEq_def true_def,
        rule disjI1)
  apply(subgoal_tac "aa = {Abs_Void⇩b⇩a⇩s⇩e ⌊None⌋}", simp add: StrongEq_def OclValid_def true_def Void⇩n⇩u⇩l⇩l_def)
  apply(drule A, erule exE)
  proof - fix y show "V τ = Abs_Set⇩b⇩a⇩s⇩e ⌊⌊aa⌋⌋ ⟹
                      ∀x∈aa. x ≠ ⊥ ⟹
                      τ ⊨ δ V ⟹
                      y ∈ aa ⟹
                      aa = {Abs_Void⇩b⇩a⇩s⇩e ⌊None⌋}"  
  apply(rule equalityI, rule subsetI, simp)
    proof - fix x show " V τ = Abs_Set⇩b⇩a⇩s⇩e ⌊⌊aa⌋⌋ ⟹
             ∀x∈aa. x ≠ ⊥ ⟹ τ ⊨ δ V ⟹ y ∈ aa ⟹ x ∈ aa ⟹ x = Abs_Void⇩b⇩a⇩s⇩e ⌊None⌋"
    apply(case_tac x, simp)
    by (metis bot_Void_def bot_option_def null_option_def)
  apply_end(simp_all)
  
  apply_end(erule ballE[where x = y], simp_all)
  apply_end(case_tac y,
            simp add: bot_option_def null_option_def OclValid_def defined_def split: if_split_asm,
            simp add: false_def true_def)
  qed (erule disjE, simp add: bot_Void_def, simp)
qed qed qed qed qed

definition Boolean :: "('𝔄,Boolean⇩b⇩a⇩s⇩e) Set"
where     "Boolean ≡ (λ τ. (Abs_Set⇩b⇩a⇩s⇩e o Some o Some)  ((Some o Some) ` (UNIV::bool set)))"

definition Boolean⇩n⇩u⇩l⇩l :: "('𝔄,Boolean⇩b⇩a⇩s⇩e) Set"
where     "Boolean⇩n⇩u⇩l⇩l ≡ (λ τ. (Abs_Set⇩b⇩a⇩s⇩e o Some o Some)  (Some ` (UNIV::bool option set)))"

lemma Boolean_defined : "δ Boolean = true"
apply(rule ext, auto simp: Boolean_def defined_def false_def true_def
                           bot_fun_def null_fun_def null_option_def)
by(simp_all add: Abs_Set⇩b⇩a⇩s⇩e_inject bot_option_def bot_Set⇩b⇩a⇩s⇩e_def null_Set⇩b⇩a⇩s⇩e_def null_option_def)

lemma Boolean⇩n⇩u⇩l⇩l_defined : "δ Boolean⇩n⇩u⇩l⇩l = true"
apply(rule ext, auto simp: Boolean⇩n⇩u⇩l⇩l_def defined_def false_def true_def
                           bot_fun_def null_fun_def null_option_def)
by(simp_all add: Abs_Set⇩b⇩a⇩s⇩e_inject bot_option_def bot_Set⇩b⇩a⇩s⇩e_def null_Set⇩b⇩a⇩s⇩e_def null_option_def)

definition String :: "('𝔄,String⇩b⇩a⇩s⇩e) Set"
where     "String ≡ (λ τ. (Abs_Set⇩b⇩a⇩s⇩e o Some o Some)  ((Some o Some) ` (UNIV::string set)))"

definition String⇩n⇩u⇩l⇩l :: "('𝔄,String⇩b⇩a⇩s⇩e) Set"
where     "String⇩n⇩u⇩l⇩l ≡ (λ τ. (Abs_Set⇩b⇩a⇩s⇩e o Some o Some)  (Some ` (UNIV::string option set)))"

lemma String_defined : "δ String = true"
apply(rule ext, auto simp: String_def defined_def false_def true_def
                           bot_fun_def null_fun_def null_option_def)
by(simp_all add: Abs_Set⇩b⇩a⇩s⇩e_inject bot_option_def bot_Set⇩b⇩a⇩s⇩e_def null_Set⇩b⇩a⇩s⇩e_def null_option_def)

lemma String⇩n⇩u⇩l⇩l_defined : "δ String⇩n⇩u⇩l⇩l = true"
apply(rule ext, auto simp: String⇩n⇩u⇩l⇩l_def defined_def false_def true_def
                           bot_fun_def null_fun_def null_option_def)
by(simp_all add: Abs_Set⇩b⇩a⇩s⇩e_inject bot_option_def bot_Set⇩b⇩a⇩s⇩e_def null_Set⇩b⇩a⇩s⇩e_def null_option_def)

definition Real :: "('𝔄,Real⇩b⇩a⇩s⇩e) Set"
where     "Real ≡ (λ τ. (Abs_Set⇩b⇩a⇩s⇩e o Some o Some)  ((Some o Some) ` (UNIV::real set)))"

definition Real⇩n⇩u⇩l⇩l :: "('𝔄,Real⇩b⇩a⇩s⇩e) Set"
where     "Real⇩n⇩u⇩l⇩l ≡ (λ τ. (Abs_Set⇩b⇩a⇩s⇩e o Some o Some)  (Some ` (UNIV::real option set)))"

lemma Real_defined : "δ Real = true"
apply(rule ext, auto simp: Real_def defined_def false_def true_def
                           bot_fun_def null_fun_def null_option_def)
by(simp_all add: Abs_Set⇩b⇩a⇩s⇩e_inject bot_option_def bot_Set⇩b⇩a⇩s⇩e_def null_Set⇩b⇩a⇩s⇩e_def null_option_def)

lemma Real⇩n⇩u⇩l⇩l_defined : "δ Real⇩n⇩u⇩l⇩l = true"
apply(rule ext, auto simp: Real⇩n⇩u⇩l⇩l_def defined_def false_def true_def
                           bot_fun_def null_fun_def null_option_def)
by(simp_all add: Abs_Set⇩b⇩a⇩s⇩e_inject bot_option_def bot_Set⇩b⇩a⇩s⇩e_def null_Set⇩b⇩a⇩s⇩e_def null_option_def)

subsection‹Basic Properties of the Set Type›

text‹Every element in a defined set is valid.›

lemma Set_inv_lemma: "τ ⊨ (δ X) ⟹ ∀x∈⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X τ)⌉⌉. x ≠ bot"
apply(insert Rep_Set⇩b⇩a⇩s⇩e [of "X τ"], simp)
apply(auto simp: OclValid_def defined_def false_def true_def cp_def
                 bot_fun_def bot_Set⇩b⇩a⇩s⇩e_def null_Set⇩b⇩a⇩s⇩e_def null_fun_def
           split:if_split_asm)
 apply(erule contrapos_pp [of "Rep_Set⇩b⇩a⇩s⇩e (X τ) = bot"])
 apply(subst Abs_Set⇩b⇩a⇩s⇩e_inject[symmetric], rule Rep_Set⇩b⇩a⇩s⇩e, simp)
 apply(simp add: Rep_Set⇩b⇩a⇩s⇩e_inverse bot_Set⇩b⇩a⇩s⇩e_def bot_option_def)
apply(erule contrapos_pp [of "Rep_Set⇩b⇩a⇩s⇩e (X τ) = null"])
apply(subst Abs_Set⇩b⇩a⇩s⇩e_inject[symmetric], rule Rep_Set⇩b⇩a⇩s⇩e, simp)
apply(simp add: Rep_Set⇩b⇩a⇩s⇩e_inverse  null_option_def)
by (simp add: bot_option_def)

lemma Set_inv_lemma' :
 assumes x_def : "τ ⊨ δ X"
     and e_mem : "e ∈ ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X τ)⌉⌉"
   shows "τ ⊨ υ (λ_. e)"
 apply(rule Set_inv_lemma[OF x_def, THEN ballE[where x = e]])
  apply(simp add: foundation18')
by(simp add: e_mem)

lemma abs_rep_simp' :
 assumes S_all_def : "τ ⊨ δ S"
   shows "Abs_Set⇩b⇩a⇩s⇩e ⌊⌊⌈⌈Rep_Set⇩b⇩a⇩s⇩e (S τ)⌉⌉⌋⌋ = S τ"
proof -
 have discr_eq_false_true : "⋀τ. (false τ = true τ) = False" by(simp add: false_def true_def)
 show ?thesis
  apply(insert S_all_def, simp add: OclValid_def defined_def)
  apply(rule mp[OF Abs_Set⇩b⇩a⇩s⇩e_induct[where P = "λS. (if S = ⊥ τ ∨ S = null τ
                                                    then false τ else true τ) = true τ ⟶
                                                   Abs_Set⇩b⇩a⇩s⇩e ⌊⌊⌈⌈Rep_Set⇩b⇩a⇩s⇩e S⌉⌉⌋⌋ = S"]],
        rename_tac S')
   apply(simp add: Abs_Set⇩b⇩a⇩s⇩e_inverse discr_eq_false_true)
   apply(case_tac S') apply(simp add: bot_fun_def bot_Set⇩b⇩a⇩s⇩e_def)+
   apply(rename_tac S'', case_tac S'') apply(simp add: null_fun_def null_Set⇩b⇩a⇩s⇩e_def)+
 done
qed

lemma S_lift' :
 assumes S_all_def : "(τ :: '𝔄 st) ⊨ δ S"
   shows "∃S'. (λa (_::'𝔄 st). a) ` ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (S τ)⌉⌉ = (λa (_::'𝔄 st). ⌊a⌋) ` S'"
  apply(rule_tac x = "(λa. ⌈a⌉) ` ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (S τ)⌉⌉" in exI)
  apply(simp only: image_comp)
  apply(simp add: comp_def)
  apply(rule image_cong, fast)
  (* *)
  apply(drule Set_inv_lemma'[OF S_all_def])
by(case_tac x, (simp add: bot_option_def foundation18')+)

lemma invalid_set_OclNot_defined [simp,code_unfold]:"δ(invalid::('𝔄,'α::null) Set) = false" by simp
lemma null_set_OclNot_defined [simp,code_unfold]:"δ(null::('𝔄,'α::null) Set) = false"
by(simp add: defined_def null_fun_def)
lemma invalid_set_valid [simp,code_unfold]:"υ(invalid::('𝔄,'α::null) Set) = false"
by simp
lemma null_set_valid [simp,code_unfold]:"υ(null::('𝔄,'α::null) Set) = true"
apply(simp add: valid_def null_fun_def bot_fun_def bot_Set⇩b⇩a⇩s⇩e_def null_Set⇩b⇩a⇩s⇩e_def)
apply(subst Abs_Set⇩b⇩a⇩s⇩e_inject,simp_all add: null_option_def bot_option_def)
done

text‹... which means that we can have a type ‹('𝔄,('𝔄,('𝔄) Integer) Set) Set›
corresponding exactly to Set(Set(Integer)) in OCL notation. Note that the parameter
‹'𝔄› still refers to the object universe; making the OCL semantics entirely parametric
in the object universe makes it possible to study (and prove) its properties
independently from a concrete class diagram.›

subsection‹Definition: Strict Equality \label{sec:set-strict-equality}›

text‹After the part of foundational operations on sets, we detail here equality on sets.
Strong equality is inherited from the OCL core, but we have to consider
the case of the strict equality. We decide to overload strict equality in the
same way we do for other value's in OCL:›

overloading
  StrictRefEq ≡ "StrictRefEq :: [('𝔄,'α::null)Set,('𝔄,'α::null)Set] ⇒ ('𝔄)Boolean"
begin
  definition StrictRefEq⇩S⇩e⇩t :
    "(x::('𝔄,'α::null)Set) ≐ y ≡ λ τ. if (υ x) τ = true τ ∧ (υ y) τ = true τ
                                       then (x ≜ y)τ
                                       else invalid τ"
end

text‹One might object here that for the case of objects, this is an empty definition.
The answer is no, we will restrain later on states and objects such that any object
has its oid stored inside the object (so the ref, under which an object can be referenced
in the store will represented in the object itself). For such well-formed stores that satisfy
this invariant (the WFF-invariant), the referential equality and the
strong equality---and therefore the strict equality on sets in the sense above---coincides.›

text‹Property proof in terms of @{term "profile_bin⇩S⇩t⇩r⇩o⇩n⇩g⇩E⇩q_⇩v_⇩v"}›
interpretation  StrictRefEq⇩S⇩e⇩t : profile_bin⇩S⇩t⇩r⇩o⇩n⇩g⇩E⇩q_⇩v_⇩v "λ x y. (x::('𝔄,'α::null)Set) ≐ y" 
         by unfold_locales (auto simp:  StrictRefEq⇩S⇩e⇩t)



subsection‹Constants: mtSet›
definition mtSet::"('𝔄,'α::null) Set"  ("Set{}")
where     "Set{} ≡ (λ τ.  Abs_Set⇩b⇩a⇩s⇩e ⌊⌊{}::'α set⌋⌋ )"


lemma mtSet_defined[simp,code_unfold]:"δ(Set{}) = true"
apply(rule ext, auto simp: mtSet_def defined_def null_Set⇩b⇩a⇩s⇩e_def
                           bot_Set⇩b⇩a⇩s⇩e_def bot_fun_def null_fun_def)
by(simp_all add: Abs_Set⇩b⇩a⇩s⇩e_inject bot_option_def null_Set⇩b⇩a⇩s⇩e_def null_option_def)

lemma mtSet_valid[simp,code_unfold]:"υ(Set{}) = true"
apply(rule ext,auto simp: mtSet_def valid_def null_Set⇩b⇩a⇩s⇩e_def
                          bot_Set⇩b⇩a⇩s⇩e_def bot_fun_def null_fun_def)
by(simp_all add: Abs_Set⇩b⇩a⇩s⇩e_inject bot_option_def null_Set⇩b⇩a⇩s⇩e_def null_option_def)

lemma mtSet_rep_set: "⌈⌈Rep_Set⇩b⇩a⇩s⇩e (Set{} τ)⌉⌉ = {}"
 apply(simp add: mtSet_def, subst Abs_Set⇩b⇩a⇩s⇩e_inverse)
by(simp add: bot_option_def)+

lemma [simp,code_unfold]: "const Set{}"
by(simp add: const_def mtSet_def)


text‹Note that the collection types in OCL allow for null to be included;
  however, there is the null-collection into which inclusion yields invalid.›

subsection‹Definition: Including›

definition OclIncluding   :: "[('𝔄,'α::null) Set,('𝔄,'α) val] ⇒ ('𝔄,'α) Set"
where     "OclIncluding x y = (λ τ. if (δ x) τ = true τ ∧ (υ y) τ = true τ
                                    then Abs_Set⇩b⇩a⇩s⇩e ⌊⌊ ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (x τ)⌉⌉  ∪ {y τ} ⌋⌋
                                    else invalid τ )"
notation   OclIncluding   ("_->including⇩S⇩e⇩t'(_')")

interpretation OclIncluding : profile_bin⇩d_⇩v OclIncluding "λx y. Abs_Set⇩b⇩a⇩s⇩e⌊⌊⌈⌈Rep_Set⇩b⇩a⇩s⇩e x⌉⌉ ∪ {y}⌋⌋"
proof -  
 have A : "None ∈ {X. X = bot ∨ X = null ∨ (∀x∈⌈⌈X⌉⌉. x ≠ bot)}" by(simp add: bot_option_def)
 have B : "⌊None⌋ ∈ {X. X = bot ∨ X = null ∨ (∀x∈⌈⌈X⌉⌉. x ≠ bot)}" 
          by(simp add: null_option_def bot_option_def)
 have C : "⋀x y. x ≠ ⊥ ⟹ x ≠ null ⟹  y ≠ ⊥  ⟹
           ⌊⌊insert y ⌈⌈Rep_Set⇩b⇩a⇩s⇩e x⌉⌉⌋⌋ ∈ {X. X = bot ∨ X = null ∨ (∀x∈⌈⌈X⌉⌉. x ≠ bot)}"
           by(auto intro!:Set_inv_lemma[simplified OclValid_def 
                                        defined_def false_def true_def null_fun_def bot_fun_def])          
         show "profile_bin⇩d_⇩v OclIncluding (λx y. Abs_Set⇩b⇩a⇩s⇩e⌊⌊⌈⌈Rep_Set⇩b⇩a⇩s⇩e x⌉⌉ ∪ {y}⌋⌋)"
         apply unfold_locales  
          apply(auto simp:OclIncluding_def bot_option_def null_option_def null_Set⇩b⇩a⇩s⇩e_def bot_Set⇩b⇩a⇩s⇩e_def)
          apply(erule_tac Q="Abs_Set⇩b⇩a⇩s⇩e⌊⌊insert y ⌈⌈Rep_Set⇩b⇩a⇩s⇩e x⌉⌉⌋⌋ = Abs_Set⇩b⇩a⇩s⇩e None" in contrapos_pp)
          apply(subst Abs_Set⇩b⇩a⇩s⇩e_inject[OF C A])
             apply(simp_all add:  null_Set⇩b⇩a⇩s⇩e_def bot_Set⇩b⇩a⇩s⇩e_def bot_option_def)
         apply(erule_tac Q="Abs_Set⇩b⇩a⇩s⇩e⌊⌊insert y ⌈⌈Rep_Set⇩b⇩a⇩s⇩e x⌉⌉⌋⌋ = Abs_Set⇩b⇩a⇩s⇩e ⌊None⌋" in contrapos_pp)
         apply(subst Abs_Set⇩b⇩a⇩s⇩e_inject[OF C B])
            apply(simp_all add:  null_Set⇩b⇩a⇩s⇩e_def bot_Set⇩b⇩a⇩s⇩e_def bot_option_def)
         done
qed

syntax
  "_OclFinset" :: "args => ('𝔄,'a::null) Set"    ("Set{(_)}")
translations
  "Set{x, xs}" == "CONST OclIncluding (Set{xs}) x"
  "Set{x}"     == "CONST OclIncluding (Set{}) x "


subsection‹Definition: Excluding›

definition OclExcluding   :: "[('𝔄,'α::null) Set,('𝔄,'α) val] ⇒ ('𝔄,'α) Set"
where     "OclExcluding x y = (λ τ.  if (δ x) τ = true τ ∧ (υ y) τ = true τ
                                     then Abs_Set⇩b⇩a⇩s⇩e ⌊⌊ ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (x τ)⌉⌉ - {y τ} ⌋⌋
                                     else ⊥ )"
notation   OclExcluding   ("_->excluding⇩S⇩e⇩t'(_')")


lemma OclExcluding_inv: "(x:: Set('b::{null})) ≠ ⊥ ⟹ x ≠ null ⟹  y ≠ ⊥  ⟹
           ⌊⌊⌈⌈Rep_Set⇩b⇩a⇩s⇩e x⌉⌉ - {y}⌋⌋ ∈ {X. X = bot ∨ X = null ∨ (∀x∈⌈⌈X⌉⌉. x ≠ bot)}"
  proof - fix X :: "'a state × 'a state ⇒ Set('b)" fix τ
          show "x ≠ ⊥ ⟹ x ≠ null ⟹ y ≠ ⊥ ⟹ ?thesis"
            when "x = X τ"
  by(simp add: that Set_inv_lemma[simplified OclValid_def 
                                          defined_def null_fun_def bot_fun_def, of X τ])
qed simp_all

interpretation OclExcluding : profile_bin⇩d_⇩v OclExcluding "λx y. Abs_Set⇩b⇩a⇩s⇩e⌊⌊⌈⌈Rep_Set⇩b⇩a⇩s⇩e x⌉⌉ - {y}⌋⌋"
proof -  
 have A : "None ∈ {X. X = bot ∨ X = null ∨ (∀x∈⌈⌈X⌉⌉. x ≠ bot)}" by(simp add: bot_option_def)
 have B : "⌊None⌋ ∈ {X. X = bot ∨ X = null ∨ (∀x∈⌈⌈X⌉⌉. x ≠ bot)}" 
          by(simp add: null_option_def bot_option_def)
         show "profile_bin⇩d_⇩v OclExcluding (λx y. Abs_Set⇩b⇩a⇩s⇩e⌊⌊⌈⌈Rep_Set⇩b⇩a⇩s⇩e (x:: Set('b))⌉⌉ - {y}⌋⌋)"
         apply unfold_locales  
          apply(auto simp:OclExcluding_def bot_option_def null_option_def null_Set⇩b⇩a⇩s⇩e_def bot_Set⇩b⇩a⇩s⇩e_def invalid_def)
          apply(erule_tac Q="Abs_Set⇩b⇩a⇩s⇩e⌊⌊⌈⌈Rep_Set⇩b⇩a⇩s⇩e x⌉⌉ - {y}⌋⌋ = Abs_Set⇩b⇩a⇩s⇩e None" in contrapos_pp)
          apply(subst Abs_Set⇩b⇩a⇩s⇩e_inject[OF OclExcluding_inv A])
             apply(simp_all add:  null_Set⇩b⇩a⇩s⇩e_def bot_Set⇩b⇩a⇩s⇩e_def bot_option_def)
         apply(erule_tac Q="Abs_Set⇩b⇩a⇩s⇩e⌊⌊⌈⌈Rep_Set⇩b⇩a⇩s⇩e x⌉⌉ - {y}⌋⌋ = Abs_Set⇩b⇩a⇩s⇩e ⌊None⌋" in contrapos_pp)
         apply(subst Abs_Set⇩b⇩a⇩s⇩e_inject[OF OclExcluding_inv B])
            apply(simp_all add:  null_Set⇩b⇩a⇩s⇩e_def bot_Set⇩b⇩a⇩s⇩e_def bot_option_def)
         done
qed


subsection‹Definition: Includes›

definition OclIncludes   :: "[('𝔄,'α::null) Set,('𝔄,'α) val] ⇒ '𝔄 Boolean"
where     "OclIncludes x y = (λ τ.   if (δ x) τ = true τ ∧ (υ y) τ = true τ
                                     then ⌊⌊(y τ) ∈ ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (x τ)⌉⌉ ⌋⌋
                                     else ⊥  )"
notation   OclIncludes    ("_->includes⇩S⇩e⇩t'(_')" (*[66,65]65*))

interpretation OclIncludes : profile_bin⇩d_⇩v OclIncludes "λx y. ⌊⌊y ∈ ⌈⌈Rep_Set⇩b⇩a⇩s⇩e x⌉⌉⌋⌋"
by(unfold_locales, auto simp:OclIncludes_def bot_option_def null_option_def invalid_def)


subsection‹Definition: Excludes›

definition OclExcludes   :: "[('𝔄,'α::null) Set,('𝔄,'α) val] ⇒ '𝔄 Boolean"
where     "OclExcludes x y = (not(OclIncludes x y))"
notation   OclExcludes    ("_->excludes⇩S⇩e⇩t'(_')" (*[66,65]65*))

text‹The case of the size definition is somewhat special, we admit
explicitly in Featherweight OCL the possibility of infinite sets. For
the size definition, this requires an extra condition that assures
that the cardinality of the set is actually a defined integer.›

interpretation OclExcludes : profile_bin⇩d_⇩v OclExcludes "λx y. ⌊⌊y ∉ ⌈⌈Rep_Set⇩b⇩a⇩s⇩e x⌉⌉⌋⌋"
by(unfold_locales, auto simp:OclExcludes_def OclIncludes_def OclNot_def bot_option_def null_option_def invalid_def)

subsection‹Definition: Size›

definition OclSize     :: "('𝔄,'α::null)Set ⇒ '𝔄 Integer"
where     "OclSize x = (λ τ. if (δ x) τ = true τ ∧ finite(⌈⌈Rep_Set⇩b⇩a⇩s⇩e (x τ)⌉⌉)
                             then ⌊⌊ int(card ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (x τ)⌉⌉) ⌋⌋
                             else ⊥ )"
notation  (* standard ascii syntax *)
           OclSize        ("_->size⇩S⇩e⇩t'(')" (*[66]*))

text‹The following definition follows the requirement of the
standard to treat null as neutral element of sets. It is
a well-documented exception from the general strictness
rule and the rule that the distinguished argument self should
be non-null.›

(*TODO Locale - Equivalent*)  


subsection‹Definition: IsEmpty›

definition OclIsEmpty   :: "('𝔄,'α::null) Set ⇒ '𝔄 Boolean"
where     "OclIsEmpty x =  ((υ x and not (δ x)) or ((OclSize x) ≐ 𝟬))"
notation   OclIsEmpty     ("_->isEmpty⇩S⇩e⇩t'(')" (*[66]*))

(*TODO Locale - Equivalent*)  


subsection‹Definition: NotEmpty›

definition OclNotEmpty   :: "('𝔄,'α::null) Set ⇒ '𝔄 Boolean"
where     "OclNotEmpty x =  not(OclIsEmpty x)"
notation   OclNotEmpty    ("_->notEmpty⇩S⇩e⇩t'(')" (*[66]*))

(*TODO Locale - Equivalent*)  

subsection‹Definition: Any›

(* Slight breach of naming convention in order to avoid naming conflict on constant.*)
definition OclANY   :: "[('𝔄,'α::null) Set] ⇒ ('𝔄,'α) val"
where     "OclANY x = (λ τ. if (υ x) τ = true τ
                            then if (δ x and OclNotEmpty x) τ = true τ
                                 then SOME y. y ∈ ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (x τ)⌉⌉
                                 else null τ
                            else ⊥ )"
notation   OclANY   ("_->any⇩S⇩e⇩t'(')")

(*TODO Locale - Equivalent*)  

(* actually, this definition covers only: X->any⇩S⇩e⇩t(true) of the standard, which foresees
a (totally correct) high-level definition
source->any⇩S⇩e⇩t(iterator | body) =
source->select(iterator | body)->asSequence()->first(). Since we don't have sequences,
we have to go for a direct---restricted---definition. *)



subsection‹Definition: Forall›

text‹The definition of OclForall mimics the one of @{term "OclAnd"}:
OclForall is not a strict operation.›
definition OclForall     :: "[('𝔄,'α::null)Set,('𝔄,'α)val⇒('𝔄)Boolean] ⇒ '𝔄 Boolean"
where     "OclForall S P = (λ τ. if (δ S) τ = true τ
                                 then if (∃x∈⌈⌈Rep_Set⇩b⇩a⇩s⇩e (S τ)⌉⌉. P(λ _. x) τ = false τ)
                                      then false τ
                                      else if (∃x∈⌈⌈Rep_Set⇩b⇩a⇩s⇩e (S τ)⌉⌉. P(λ _. x) τ = invalid τ)
                                           then invalid τ
                                           else if (∃x∈⌈⌈Rep_Set⇩b⇩a⇩s⇩e (S τ)⌉⌉. P(λ _. x) τ = null τ)
                                                then null τ
                                                else true τ
                                 else ⊥)"
syntax
  "_OclForallSet" :: "[('𝔄,'α::null) Set,id,('𝔄)Boolean] ⇒ '𝔄 Boolean"    ("(_)->forAll⇩S⇩e⇩t'(_|_')")
translations
  "X->forAll⇩S⇩e⇩t(x | P)" == "CONST UML_Set.OclForall X (%x. P)"

(*TODO Locale - Equivalent*)  

subsection‹Definition: Exists›
  
text‹Like OclForall, OclExists is also not strict.›
definition OclExists     :: "[('𝔄,'α::null) Set,('𝔄,'α)val⇒('𝔄)Boolean] ⇒ '𝔄 Boolean"
where     "OclExists S P = not(UML_Set.OclForall S (λ X. not (P X)))"

syntax
  "_OclExistSet" :: "[('𝔄,'α::null) Set,id,('𝔄)Boolean] ⇒ '𝔄 Boolean"    ("(_)->exists⇩S⇩e⇩t'(_|_')")
translations
  "X->exists⇩S⇩e⇩t(x | P)" == "CONST UML_Set.OclExists X (%x. P)"

(*TODO Locale - Equivalent*)  
  
subsection‹Definition: Iterate›

definition OclIterate :: "[('𝔄,'α::null) Set,('𝔄,'β::null)val,
                             ('𝔄,'α)val⇒('𝔄,'β)val⇒('𝔄,'β)val] ⇒ ('𝔄,'β)val"
where "OclIterate S A F = (λ τ. if (δ S) τ = true τ ∧ (υ A) τ = true τ ∧ finite⌈⌈Rep_Set⇩b⇩a⇩s⇩e (S τ)⌉⌉
                                  then (Finite_Set.fold (F) (A) ((λa τ. a) ` ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (S τ)⌉⌉))τ
                                  else ⊥)"
syntax
  "_OclIterateSet"  :: "[('𝔄,'α::null) Set, idt, idt, 'α, 'β] => ('𝔄,'γ)val"
                        ("_ ->iterate⇩S⇩e⇩t'(_;_=_ | _')" (*[71,100,70]50*))
translations
  "X->iterate⇩S⇩e⇩t(a; x = A | P)" == "CONST OclIterate X A (%a. (% x. P))"

(*TODO Locale - Equivalent*)  
  
subsection‹Definition: Select›

definition OclSelect :: "[('𝔄,'α::null)Set,('𝔄,'α)val⇒('𝔄)Boolean] ⇒ ('𝔄,'α)Set"
where "OclSelect S P = (λτ. if (δ S) τ = true τ
                              then if (∃x∈⌈⌈Rep_Set⇩b⇩a⇩s⇩e (S τ)⌉⌉. P(λ _. x) τ = invalid τ)
                                   then invalid τ
                                   else Abs_Set⇩b⇩a⇩s⇩e ⌊⌊{x∈⌈⌈ Rep_Set⇩b⇩a⇩s⇩e (S τ)⌉⌉. P (λ_. x) τ ≠ false τ}⌋⌋
                              else invalid τ)"
syntax
  "_OclSelectSet" :: "[('𝔄,'α::null) Set,id,('𝔄)Boolean] ⇒ '𝔄 Boolean"    ("(_)->select⇩S⇩e⇩t'(_|_')")
translations
  "X->select⇩S⇩e⇩t(x | P)" == "CONST OclSelect X (% x. P)"

(*TODO Locale - Equivalent*)  

subsection‹Definition: Reject›

definition OclReject :: "[('𝔄,'α::null)Set,('𝔄,'α)val⇒('𝔄)Boolean] ⇒ ('𝔄,'α::null)Set"
where "OclReject S P = OclSelect S (not o P)"
syntax
  "_OclRejectSet" :: "[('𝔄,'α::null) Set,id,('𝔄)Boolean] ⇒ '𝔄 Boolean"    ("(_)->reject⇩S⇩e⇩t'(_|_')")
translations
  "X->reject⇩S⇩e⇩t(x | P)" == "CONST OclReject X (% x. P)"

(*TODO Locale - Equivalent*)  

subsection‹Definition: IncludesAll›

definition OclIncludesAll   :: "[('𝔄,'α::null) Set,('𝔄,'α) Set] ⇒ '𝔄 Boolean"
where     "OclIncludesAll x y = (λ τ.   if (δ x) τ = true τ ∧ (δ y) τ = true τ
                                        then ⌊⌊⌈⌈Rep_Set⇩b⇩a⇩s⇩e (y τ)⌉⌉ ⊆ ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (x τ)⌉⌉ ⌋⌋
                                        else ⊥  )"
notation   OclIncludesAll ("_->includesAll⇩S⇩e⇩t'(_')" (*[66,65]65*))

interpretation OclIncludesAll : profile_bin⇩d_⇩d OclIncludesAll "λx y. ⌊⌊⌈⌈Rep_Set⇩b⇩a⇩s⇩e y⌉⌉ ⊆ ⌈⌈Rep_Set⇩b⇩a⇩s⇩e x⌉⌉⌋⌋"
by(unfold_locales, auto simp:OclIncludesAll_def bot_option_def null_option_def invalid_def)

subsection‹Definition: ExcludesAll›

definition OclExcludesAll   :: "[('𝔄,'α::null) Set,('𝔄,'α) Set] ⇒ '𝔄 Boolean"
where     "OclExcludesAll x y = (λ τ.   if (δ x) τ = true τ ∧ (δ y) τ = true τ
                                        then ⌊⌊⌈⌈Rep_Set⇩b⇩a⇩s⇩e (y τ)⌉⌉ ∩ ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (x τ)⌉⌉ = {} ⌋⌋
                                        else ⊥  )"
notation  OclExcludesAll ("_->excludesAll⇩S⇩e⇩t'(_')" (*[66,65]65*))

interpretation OclExcludesAll : profile_bin⇩d_⇩d OclExcludesAll "λx y. ⌊⌊⌈⌈Rep_Set⇩b⇩a⇩s⇩e y⌉⌉ ∩ ⌈⌈Rep_Set⇩b⇩a⇩s⇩e x⌉⌉ = {}⌋⌋"
by(unfold_locales, auto simp:OclExcludesAll_def bot_option_def null_option_def invalid_def)

subsection‹Definition: Union›

definition OclUnion   :: "[('𝔄,'α::null) Set,('𝔄,'α) Set] ⇒ ('𝔄,'α) Set"
where     "OclUnion x y = (λ τ.   if (δ x) τ = true τ ∧ (δ y) τ = true τ
                                        then Abs_Set⇩b⇩a⇩s⇩e⌊⌊⌈⌈Rep_Set⇩b⇩a⇩s⇩e (y τ)⌉⌉ ∪ ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (x τ)⌉⌉ ⌋⌋
                                        else ⊥  )"
notation   OclUnion       ("_->union⇩S⇩e⇩t'(_')"          (*[66,65]65*))

lemma OclUnion_inv: "(x:: Set('b::{null})) ≠ ⊥ ⟹ x ≠ null ⟹  y ≠ ⊥  ⟹ y ≠ null ⟹
           ⌊⌊⌈⌈Rep_Set⇩b⇩a⇩s⇩e y⌉⌉ ∪ ⌈⌈Rep_Set⇩b⇩a⇩s⇩e x⌉⌉⌋⌋ ∈ {X. X = bot ∨ X = null ∨ (∀x∈⌈⌈X⌉⌉. x ≠ bot)}"
  proof - fix X Y :: "'a state × 'a state ⇒ Set('b)" fix τ
          show "x ≠ ⊥ ⟹ x ≠ null ⟹ y ≠ ⊥ ⟹ y ≠ null ⟹ ?thesis"
            when "x = X τ" "y = Y τ"
  by(auto simp: that,
     insert
       Set_inv_lemma[simplified OclValid_def 
                                          defined_def null_fun_def bot_fun_def, of Y τ]
       Set_inv_lemma[simplified OclValid_def 
                                          defined_def null_fun_def bot_fun_def, of X τ],
     auto)
qed simp_all

interpretation OclUnion : profile_bin⇩d_⇩d OclUnion "λx y. Abs_Set⇩b⇩a⇩s⇩e⌊⌊⌈⌈Rep_Set⇩b⇩a⇩s⇩e y⌉⌉ ∪ ⌈⌈Rep_Set⇩b⇩a⇩s⇩e x⌉⌉⌋⌋"
proof -  
 have A : "None ∈ {X. X = bot ∨ X = null ∨ (∀x∈⌈⌈X⌉⌉. x ≠ bot)}" by(simp add: bot_option_def)
 have B : "⌊None⌋ ∈ {X. X = bot ∨ X = null ∨ (∀x∈⌈⌈X⌉⌉. x ≠ bot)}" 
          by(simp add: null_option_def bot_option_def)
         show "profile_bin⇩d_⇩d OclUnion (λx y. Abs_Set⇩b⇩a⇩s⇩e⌊⌊⌈⌈Rep_Set⇩b⇩a⇩s⇩e y⌉⌉ ∪ ⌈⌈Rep_Set⇩b⇩a⇩s⇩e x⌉⌉⌋⌋)"
         apply unfold_locales  
          apply(auto simp:OclUnion_def bot_option_def null_option_def null_Set⇩b⇩a⇩s⇩e_def bot_Set⇩b⇩a⇩s⇩e_def invalid_def)
          apply(erule_tac Q="Abs_Set⇩b⇩a⇩s⇩e⌊⌊⌈⌈Rep_Set⇩b⇩a⇩s⇩e y⌉⌉ ∪ ⌈⌈Rep_Set⇩b⇩a⇩s⇩e x⌉⌉⌋⌋ = Abs_Set⇩b⇩a⇩s⇩e None" in contrapos_pp)
          apply(subst Abs_Set⇩b⇩a⇩s⇩e_inject[OF OclUnion_inv A])
             apply(simp_all add:  null_Set⇩b⇩a⇩s⇩e_def bot_Set⇩b⇩a⇩s⇩e_def bot_option_def)
         apply(erule_tac Q="Abs_Set⇩b⇩a⇩s⇩e⌊⌊⌈⌈Rep_Set⇩b⇩a⇩s⇩e y⌉⌉ ∪ ⌈⌈Rep_Set⇩b⇩a⇩s⇩e x⌉⌉⌋⌋ = Abs_Set⇩b⇩a⇩s⇩e ⌊None⌋" in contrapos_pp)
         apply(subst Abs_Set⇩b⇩a⇩s⇩e_inject[OF OclUnion_inv B])
            apply(simp_all add:  null_Set⇩b⇩a⇩s⇩e_def bot_Set⇩b⇩a⇩s⇩e_def bot_option_def)
         done
qed

subsection‹Definition: Intersection›

definition OclIntersection   :: "[('𝔄,'α::null) Set,('𝔄,'α) Set] ⇒ ('𝔄,'α) Set"
where     "OclIntersection x y = (λ τ.  if (δ x) τ = true τ ∧ (δ y) τ = true τ
                                        then Abs_Set⇩b⇩a⇩s⇩e⌊⌊⌈⌈Rep_Set⇩b⇩a⇩s⇩e (y τ)⌉⌉ 
                                                         ∩ ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (x τ)⌉⌉⌋⌋
                                        else ⊥  )"
notation   OclIntersection("_->intersection⇩S⇩e⇩t'(_')"   (*[71,70]70*))

lemma OclIntersection_inv: "(x:: Set('b::{null})) ≠ ⊥ ⟹ x ≠ null ⟹  y ≠ ⊥  ⟹ y ≠ null ⟹
           ⌊⌊⌈⌈Rep_Set⇩b⇩a⇩s⇩e y⌉⌉ ∩ ⌈⌈Rep_Set⇩b⇩a⇩s⇩e x⌉⌉⌋⌋ ∈ {X. X = bot ∨ X = null ∨ (∀x∈⌈⌈X⌉⌉. x ≠ bot)}"
  proof - fix X Y :: "'a state × 'a state ⇒ Set('b)" fix τ
          show "x ≠ ⊥ ⟹ x ≠ null ⟹ y ≠ ⊥ ⟹ y ≠ null ⟹ ?thesis"
            when "x = X τ" "y = Y τ"
  by(auto simp: that,
     insert
       Set_inv_lemma[simplified OclValid_def 
                                          defined_def null_fun_def bot_fun_def, of Y τ]
       Set_inv_lemma[simplified OclValid_def 
                                          defined_def null_fun_def bot_fun_def, of X τ],
     auto)
qed simp_all

interpretation OclIntersection : profile_bin⇩d_⇩d OclIntersection "λx y. Abs_Set⇩b⇩a⇩s⇩e⌊⌊⌈⌈Rep_Set⇩b⇩a⇩s⇩e y⌉⌉ ∩ ⌈⌈Rep_Set⇩b⇩a⇩s⇩e x⌉⌉⌋⌋"
proof -  
 have A : "None ∈ {X. X = bot ∨ X = null ∨ (∀x∈⌈⌈X⌉⌉. x ≠ bot)}" by(simp add: bot_option_def)
 have B : "⌊None⌋ ∈ {X. X = bot ∨ X = null ∨ (∀x∈⌈⌈X⌉⌉. x ≠ bot)}" 
          by(simp add: null_option_def bot_option_def)
         show "profile_bin⇩d_⇩d OclIntersection (λx y. Abs_Set⇩b⇩a⇩s⇩e⌊⌊⌈⌈Rep_Set⇩b⇩a⇩s⇩e y⌉⌉ ∩ ⌈⌈Rep_Set⇩b⇩a⇩s⇩e x⌉⌉⌋⌋)"
         apply unfold_locales  
          apply(auto simp:OclIntersection_def bot_option_def null_option_def null_Set⇩b⇩a⇩s⇩e_def bot_Set⇩b⇩a⇩s⇩e_def invalid_def)
          apply(erule_tac Q="Abs_Set⇩b⇩a⇩s⇩e⌊⌊⌈⌈Rep_Set⇩b⇩a⇩s⇩e y⌉⌉ ∩ ⌈⌈Rep_Set⇩b⇩a⇩s⇩e x⌉⌉⌋⌋ = Abs_Set⇩b⇩a⇩s⇩e None" in contrapos_pp)
          apply(subst Abs_Set⇩b⇩a⇩s⇩e_inject[OF OclIntersection_inv A])
             apply(simp_all add:  null_Set⇩b⇩a⇩s⇩e_def bot_Set⇩b⇩a⇩s⇩e_def bot_option_def)
         apply(erule_tac Q="Abs_Set⇩b⇩a⇩s⇩e⌊⌊⌈⌈Rep_Set⇩b⇩a⇩s⇩e y⌉⌉ ∩ ⌈⌈Rep_Set⇩b⇩a⇩s⇩e x⌉⌉⌋⌋ = Abs_Set⇩b⇩a⇩s⇩e ⌊None⌋" in contrapos_pp)
         apply(subst Abs_Set⇩b⇩a⇩s⇩e_inject[OF OclIntersection_inv B])
            apply(simp_all add:  null_Set⇩b⇩a⇩s⇩e_def bot_Set⇩b⇩a⇩s⇩e_def bot_option_def)
         done
qed

subsection‹Definition (future operators)›

consts (* abstract set collection operations *)
    OclCount       :: "[('𝔄,'α::null) Set,('𝔄,'α) Set] ⇒ '𝔄 Integer"
    OclSum         :: " ('𝔄,'α::null) Set ⇒ '𝔄 Integer"
  
notation  OclCount       ("_->count⇩S⇩e⇩t'(_')" (*[66,65]65*))
notation  OclSum         ("_->sum⇩S⇩e⇩t'(')" (*[66]*))

subsection‹Logical Properties›

text‹OclIncluding›

lemma OclIncluding_valid_args_valid:
"(τ ⊨ υ(X->including⇩S⇩e⇩t(x))) = ((τ ⊨(δ X)) ∧ (τ ⊨(υ x)))"
by (metis (opaque_lifting, no_types) OclIncluding.def_valid_then_def OclIncluding.defined_args_valid)

lemma OclIncluding_valid_args_valid''[simp,code_unfold]:
"υ(X->including⇩S⇩e⇩t(x)) = ((δ X) and (υ x))"
by (simp add: OclIncluding.def_valid_then_def)

text‹etc. etc.›
text_raw‹\isatagafp› 

text‹OclExcluding›

lemma OclExcluding_valid_args_valid:
"(τ ⊨ υ(X->excluding⇩S⇩e⇩t(x))) = ((τ ⊨(δ X)) ∧ (τ ⊨(υ x)))"
by (metis OclExcluding.def_valid_then_def OclExcluding.defined_args_valid)

lemma OclExcluding_valid_args_valid''[simp,code_unfold]:
"υ(X->excluding⇩S⇩e⇩t(x)) = ((δ X) and (υ x))"
by (simp add: OclExcluding.def_valid_then_def)

text‹OclIncludes›

lemma OclIncludes_valid_args_valid:
"(τ ⊨ υ(X->includes⇩S⇩e⇩t(x))) = ((τ ⊨(δ X)) ∧ (τ ⊨(υ x)))"
by (simp add: OclIncludes.def_valid_then_def foundation10')

lemma OclIncludes_valid_args_valid''[simp,code_unfold]:
"υ(X->includes⇩S⇩e⇩t(x)) = ((δ X) and (υ x))"
by (simp add: OclIncludes.def_valid_then_def)

text‹OclExcludes›

lemma OclExcludes_valid_args_valid:
"(τ ⊨ υ(X->excludes⇩S⇩e⇩t(x))) = ((τ ⊨(δ X)) ∧ (τ ⊨(υ x)))"
by (simp add: OclExcludes.def_valid_then_def foundation10')

lemma OclExcludes_valid_args_valid''[simp,code_unfold]:
"υ(X->excludes⇩S⇩e⇩t(x)) = ((δ X) and (υ x))"
by (simp add: OclExcludes.def_valid_then_def)

text‹OclSize›

lemma OclSize_defined_args_valid: "τ ⊨ δ (X->size⇩S⇩e⇩t()) ⟹ τ ⊨ δ X"
by(auto simp: OclSize_def OclValid_def true_def valid_def false_def StrongEq_def
              defined_def invalid_def bot_fun_def null_fun_def
        split: bool.split_asm HOL.if_split_asm option.split)

lemma OclSize_infinite:
assumes non_finite:"τ ⊨ not(δ(S->size⇩S⇩e⇩t()))"
shows   "(τ ⊨ not(δ(S))) ∨ ¬ finite ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (S τ)⌉⌉"
apply(insert non_finite, simp)
apply(rule impI)
apply(simp add: OclSize_def OclValid_def defined_def)
apply(case_tac "finite ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (S τ)⌉⌉",
      simp_all add:null_fun_def null_option_def bot_fun_def bot_option_def)
done

lemma "τ ⊨ δ X ⟹ ¬ finite ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X τ)⌉⌉ ⟹ ¬ τ ⊨ δ (X->size⇩S⇩e⇩t())"
by(simp add: OclSize_def OclValid_def defined_def bot_fun_def false_def true_def)

lemma size_defined:
 assumes X_finite: "⋀τ. finite ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X τ)⌉⌉"
 shows "δ (X->size⇩S⇩e⇩t()) = δ X"
 apply(rule ext, simp add: cp_defined[of "X->size⇩S⇩e⇩t()"] OclSize_def)
 apply(simp add: defined_def bot_option_def bot_fun_def null_option_def null_fun_def X_finite)
done

lemma size_defined':
 assumes X_finite: "finite ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X τ)⌉⌉"
 shows "(τ ⊨ δ (X->size⇩S⇩e⇩t())) = (τ ⊨ δ X)"
 apply(simp add: cp_defined[of "X->size⇩S⇩e⇩t()"] OclSize_def OclValid_def)
 apply(simp add: defined_def bot_option_def bot_fun_def null_option_def null_fun_def X_finite)
done

text‹OclIsEmpty›

lemma OclIsEmpty_defined_args_valid:"τ ⊨ δ (X->isEmpty⇩S⇩e⇩t()) ⟹ τ ⊨ υ X"
  apply(auto simp: OclIsEmpty_def OclValid_def defined_def valid_def false_def true_def
                   bot_fun_def null_fun_def OclAnd_def OclOr_def OclNot_def
             split: if_split_asm)
  apply(case_tac "(X->size⇩S⇩e⇩t() ≐ 𝟬) τ", simp add: bot_option_def, simp, rename_tac x)
  apply(case_tac x, simp add: null_option_def bot_option_def, simp)
  apply(simp add: OclSize_def StrictRefEq⇩I⇩n⇩t⇩e⇩g⇩e⇩r valid_def)
by (metis (opaque_lifting, no_types)
           bot_fun_def OclValid_def defined_def foundation2 invalid_def)

lemma "τ ⊨ δ (null->isEmpty⇩S⇩e⇩t())"
by(auto simp: OclIsEmpty_def OclValid_def defined_def valid_def false_def true_def
              bot_fun_def null_fun_def OclAnd_def OclOr_def OclNot_def null_is_valid
        split: if_split_asm)

lemma OclIsEmpty_infinite: "τ ⊨ δ X ⟹ ¬ finite ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X τ)⌉⌉ ⟹ ¬ τ ⊨ δ (X->isEmpty⇩S⇩e⇩t())"
  apply(auto simp: OclIsEmpty_def OclValid_def defined_def valid_def false_def true_def
                   bot_fun_def null_fun_def OclAnd_def OclOr_def OclNot_def
             split: if_split_asm)
  apply(case_tac "(X->size⇩S⇩e⇩t() ≐ 𝟬) τ", simp add: bot_option_def, simp, rename_tac x)
  apply(case_tac x, simp add: null_option_def bot_option_def, simp)
by(simp add: OclSize_def StrictRefEq⇩I⇩n⇩t⇩e⇩g⇩e⇩r valid_def bot_fun_def false_def true_def invalid_def)

text‹OclNotEmpty›

lemma OclNotEmpty_defined_args_valid:"τ ⊨ δ (X->notEmpty⇩S⇩e⇩t()) ⟹ τ ⊨ υ X"
by (metis (opaque_lifting, no_types) OclNotEmpty_def OclNot_defargs OclNot_not foundation6 foundation9
                                OclIsEmpty_defined_args_valid)

lemma "τ ⊨ δ (null->notEmpty⇩S⇩e⇩t())"
by (metis (opaque_lifting, no_types) OclNotEmpty_def OclAnd_false1 OclAnd_idem OclIsEmpty_def
                                OclNot3 OclNot4 OclOr_def defined2 defined4 transform1 valid2)

lemma OclNotEmpty_infinite: "τ ⊨ δ X ⟹ ¬ finite ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X τ)⌉⌉ ⟹ ¬ τ ⊨ δ (X->notEmpty⇩S⇩e⇩t())"
 apply(simp add: OclNotEmpty_def)
 apply(drule OclIsEmpty_infinite, simp)
by (metis OclNot_defargs OclNot_not foundation6 foundation9)

lemma OclNotEmpty_has_elt : "τ ⊨ δ X ⟹
                          τ ⊨ X->notEmpty⇩S⇩e⇩t() ⟹
                          ∃e. e ∈ ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X τ)⌉⌉"
 apply(simp add: OclNotEmpty_def OclIsEmpty_def deMorgan1 deMorgan2, drule foundation5)
 apply(subst (asm) (2) OclNot_def,
       simp add: OclValid_def StrictRefEq⇩I⇩n⇩t⇩e⇩g⇩e⇩r StrongEq_def
            split: if_split_asm)
  prefer 2
  apply(simp add: invalid_def bot_option_def true_def)
 apply(simp add: OclSize_def valid_def split: if_split_asm,
       simp_all add: false_def true_def bot_option_def bot_fun_def OclInt0_def)
by (metis equals0I)

text‹OclANY›

lemma OclANY_defined_args_valid: "τ ⊨ δ (X->any⇩S⇩e⇩t()) ⟹ τ ⊨ δ X"
by(auto simp: OclANY_def OclValid_def true_def valid_def false_def StrongEq_def
              defined_def invalid_def bot_fun_def null_fun_def OclAnd_def
        split: bool.split_asm HOL.if_split_asm option.split)

lemma "τ ⊨ δ X ⟹ τ ⊨ X->isEmpty⇩S⇩e⇩t() ⟹ ¬ τ ⊨ δ (X->any⇩S⇩e⇩t())"
 apply(simp add: OclANY_def OclValid_def)
 apply(subst cp_defined, subst cp_OclAnd, simp add: OclNotEmpty_def, subst (1 2) cp_OclNot,
       simp add: cp_OclNot[symmetric] cp_OclAnd[symmetric] cp_defined[symmetric],
       simp add: false_def true_def)
by(drule foundation20[simplified OclValid_def true_def], simp)

lemma OclANY_valid_args_valid:
"(τ ⊨ υ(X->any⇩S⇩e⇩t())) = (τ ⊨ υ X)"
proof -
 have A: "(τ ⊨ υ(X->any⇩S⇩e⇩t())) ⟹ ((τ ⊨(υ X)))"
          by(auto simp: OclANY_def OclValid_def true_def valid_def false_def StrongEq_def
                        defined_def invalid_def bot_fun_def null_fun_def
                  split: bool.split_asm HOL.if_split_asm option.split)
 have B: "(τ ⊨(υ X)) ⟹ (τ ⊨ υ(X->any⇩S⇩e⇩t()))"
           apply(auto simp: OclANY_def OclValid_def true_def false_def StrongEq_def
                            defined_def invalid_def valid_def bot_fun_def null_fun_def
                            bot_option_def null_option_def null_is_valid
                            OclAnd_def
                      split: bool.split_asm HOL.if_split_asm option.split)
           apply(frule Set_inv_lemma[OF foundation16[THEN iffD2], OF conjI], simp)
           apply(subgoal_tac "(δ X) τ = true τ")
            prefer 2
            apply (metis (opaque_lifting, no_types) OclValid_def foundation16)
           apply(simp add: true_def,
                 drule OclNotEmpty_has_elt[simplified OclValid_def true_def], simp)
          by(erule exE,
             insert someI2[where Q = "λx. x ≠ ⊥" and P = "λy. y ∈ ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X τ)⌉⌉"],
             simp)
 show ?thesis by(auto dest:A intro:B)
qed

lemma OclANY_valid_args_valid''[simp,code_unfold]:
"υ(X->any⇩S⇩e⇩t()) = (υ X)"
by(auto intro!: OclANY_valid_args_valid transform2_rev)

(* and higher order ones : forall, exists, iterate, select, reject... *)
text_raw‹\endisatagafp› 

subsection‹Execution Laws with Invalid or Null or Infinite Set as Argument›

text‹OclIncluding› (* properties already generated by the corresponding locale *)

text‹OclExcluding› (* properties already generated by the corresponding locale *)

text‹OclIncludes› (* properties already generated by the corresponding locale *)

text‹OclExcludes› (* properties already generated by the corresponding locale *)

text‹OclSize›

lemma OclSize_invalid[simp,code_unfold]:"(invalid->size⇩S⇩e⇩t()) = invalid"
by(simp add: bot_fun_def OclSize_def invalid_def defined_def valid_def false_def true_def)

lemma OclSize_null[simp,code_unfold]:"(null->size⇩S⇩e⇩t()) = invalid"
by(rule ext,
   simp add: bot_fun_def null_fun_def null_is_valid OclSize_def
             invalid_def defined_def valid_def false_def true_def)

text‹OclIsEmpty›

lemma OclIsEmpty_invalid[simp,code_unfold]:"(invalid->isEmpty⇩S⇩e⇩t()) = invalid"
by(simp add: OclIsEmpty_def)

lemma OclIsEmpty_null[simp,code_unfold]:"(null->isEmpty⇩S⇩e⇩t()) = true"
by(simp add: OclIsEmpty_def)

text‹OclNotEmpty›

lemma OclNotEmpty_invalid[simp,code_unfold]:"(invalid->notEmpty⇩S⇩e⇩t()) = invalid"
by(simp add: OclNotEmpty_def)

lemma OclNotEmpty_null[simp,code_unfold]:"(null->notEmpty⇩S⇩e⇩t()) = false"
by(simp add: OclNotEmpty_def)

text‹OclANY›

lemma OclANY_invalid[simp,code_unfold]:"(invalid->any⇩S⇩e⇩t()) = invalid"
by(simp add: bot_fun_def OclANY_def invalid_def defined_def valid_def false_def true_def)

lemma OclANY_null[simp,code_unfold]:"(null->any⇩S⇩e⇩t()) = null"
by(simp add: OclANY_def false_def true_def)

text‹OclForall›

lemma OclForall_invalid[simp,code_unfold]:"invalid->forAll⇩S⇩e⇩t(a| P a) = invalid"
by(simp add: bot_fun_def invalid_def OclForall_def defined_def valid_def false_def true_def)

lemma OclForall_null[simp,code_unfold]:"null->forAll⇩S⇩e⇩t(a | P a) = invalid"
by(simp add: bot_fun_def invalid_def OclForall_def defined_def valid_def false_def true_def)

text‹OclExists›

lemma OclExists_invalid[simp,code_unfold]:"invalid->exists⇩S⇩e⇩t(a| P a) = invalid"
by(simp add: OclExists_def)

lemma OclExists_null[simp,code_unfold]:"null->exists⇩S⇩e⇩t(a | P a) = invalid"
by(simp add: OclExists_def)

text‹OclIterate›

lemma OclIterate_invalid[simp,code_unfold]:"invalid->iterate⇩S⇩e⇩t(a; x = A | P a x) = invalid"
by(simp add: bot_fun_def invalid_def OclIterate_def defined_def valid_def false_def true_def)

lemma OclIterate_null[simp,code_unfold]:"null->iterate⇩S⇩e⇩t(a; x = A | P a x) = invalid"
by(simp add: bot_fun_def invalid_def OclIterate_def defined_def valid_def false_def true_def)


lemma OclIterate_invalid_args[simp,code_unfold]:"S->iterate⇩S⇩e⇩t(a; x = invalid | P a x) = invalid"
by(simp add: bot_fun_def invalid_def OclIterate_def defined_def valid_def false_def true_def)

text‹An open question is this ...›
lemma (*OclIterate_null_args[simp,code_unfold]:*) "S->iterate⇩S⇩e⇩t(a; x = null | P a x) = invalid"
oops
(* In the definition above, this does not hold in general.
       And I believe, this is how it should be ... *)

lemma OclIterate_infinite:
assumes non_finite: "τ ⊨ not(δ(S->size⇩S⇩e⇩t()))"
shows "(OclIterate S A F) τ = invalid τ"
apply(insert non_finite [THEN OclSize_infinite])
apply(subst (asm) foundation9, simp)
by(metis OclIterate_def OclValid_def invalid_def)

text‹OclSelect›

lemma OclSelect_invalid[simp,code_unfold]:"invalid->select⇩S⇩e⇩t(a | P a) = invalid"
by(simp add: bot_fun_def invalid_def OclSelect_def defined_def valid_def false_def true_def)

lemma OclSelect_null[simp,code_unfold]:"null->select⇩S⇩e⇩t(a | P a) = invalid"
by(simp add: bot_fun_def invalid_def OclSelect_def defined_def valid_def false_def true_def)

text‹OclReject›

lemma OclReject_invalid[simp,code_unfold]:"invalid->reject⇩S⇩e⇩t(a | P a) = invalid"
by(simp add: OclReject_def)

lemma OclReject_null[simp,code_unfold]:"null->reject⇩S⇩e⇩t(a | P a) = invalid"
by(simp add: OclReject_def)

text_raw‹\isatagafp›

subsubsection‹Context Passing›

lemma cp_OclIncludes1:
"(X->includes⇩S⇩e⇩t(x)) τ = (X->includes⇩S⇩e⇩t(λ _. x τ)) τ"
by(auto simp: OclIncludes_def StrongEq_def invalid_def
                 cp_defined[symmetric] cp_valid[symmetric])

lemma cp_OclSize: "X->size⇩S⇩e⇩t() τ = ((λ_. X τ)->size⇩S⇩e⇩t()) τ"
by(simp add: OclSize_def cp_defined[symmetric])

lemma cp_OclIsEmpty: "X->isEmpty⇩S⇩e⇩t() τ = ((λ_. X τ)->isEmpty⇩S⇩e⇩t()) τ"
 apply(simp only: OclIsEmpty_def)
 apply(subst (2) cp_OclOr,
       subst cp_OclAnd,
       subst cp_OclNot,
       subst StrictRefEq⇩I⇩n⇩t⇩e⇩g⇩e⇩r.cp0)
by(simp add: cp_defined[symmetric] cp_valid[symmetric] StrictRefEq⇩I⇩n⇩t⇩e⇩g⇩e⇩r.cp0[symmetric]
             cp_OclSize[symmetric] cp_OclNot[symmetric] cp_OclAnd[symmetric] cp_OclOr[symmetric])

lemma cp_OclNotEmpty: "X->notEmpty⇩S⇩e⇩t() τ = ((λ_. X τ)->notEmpty⇩S⇩e⇩t()) τ"
 apply(simp only: OclNotEmpty_def)
 apply(subst (2) cp_OclNot)
by(simp add: cp_OclNot[symmetric] cp_OclIsEmpty[symmetric])

lemma cp_OclANY: "X->any⇩S⇩e⇩t() τ = ((λ_. X τ)->any⇩S⇩e⇩t()) τ"
 apply(simp only: OclANY_def)
 apply(subst (2) cp_OclAnd)
by(simp only: cp_OclAnd[symmetric] cp_defined[symmetric] cp_valid[symmetric]
              cp_OclNotEmpty[symmetric])

lemma cp_OclForall:
"(S->forAll⇩S⇩e⇩t(x | P x)) τ = ((λ _. S τ)->forAll⇩S⇩e⇩t(x | P (λ _. x τ))) τ"
by(simp add: OclForall_def cp_defined[symmetric])

(* first-order version !*)
lemma cp_OclForall1 [simp,intro!]:
"cp S ⟹ cp (λX. ((S X)->forAll⇩S⇩e⇩t(x | P x)))"
apply(simp add: cp_def)
apply(erule exE, rule exI, intro allI)
apply(erule_tac x=X in allE)
by(subst cp_OclForall, simp)

lemma (*cp_OclForall2 [simp,intro!]:*)
"cp (λX St x. P (λτ. x) X St) ⟹ cp S ⟹ cp (λX. (S X)->forAll⇩S⇩e⇩t(x|P x X)) "
apply(simp only: cp_def)
oops

lemma (*cp_OclForall:*)
"cp S ⟹
 (⋀ x. cp(P x)) ⟹
 cp(λX. ((S X)->forAll⇩S⇩e⇩t(x | P x X)))"
oops

lemma cp_OclExists:
"(S->exists⇩S⇩e⇩t(x | P x)) τ = ((λ _. S τ)->exists⇩S⇩e⇩t(x | P (λ _. x τ))) τ"
by(simp add: OclExists_def OclNot_def, subst cp_OclForall, simp)

(* first-order version !*)
lemma cp_OclExists1 [simp,intro!]:
"cp S ⟹ cp (λX. ((S X)->exists⇩S⇩e⇩t(x | P x)))"
apply(simp add: cp_def)
apply(erule exE, rule exI, intro allI)
apply(erule_tac x=X in allE)
by(subst cp_OclExists,simp)

lemma cp_OclIterate: 
     "(X->iterate⇩S⇩e⇩t(a; x = A | P a x)) τ =
                ((λ _. X τ)->iterate⇩S⇩e⇩t(a; x = A | P a x)) τ"
by(simp add: OclIterate_def cp_defined[symmetric])

lemma cp_OclSelect: "(X->select⇩S⇩e⇩t(a | P a)) τ =
                ((λ _. X τ)->select⇩S⇩e⇩t(a | P a)) τ"
by(simp add: OclSelect_def cp_defined[symmetric])

lemma cp_OclReject: "(X->reject⇩S⇩e⇩t(a | P a)) τ = ((λ _. X τ)->reject⇩S⇩e⇩t(a | P a)) τ"
by(simp add: OclReject_def, subst cp_OclSelect, simp)

lemmas cp_intro''⇩S⇩e⇩t[intro!,simp,code_unfold] =
       cp_OclSize      [THEN allI[THEN allI[THEN cpI1], of "OclSize"]]
       cp_OclIsEmpty   [THEN allI[THEN allI[THEN cpI1], of "OclIsEmpty"]]
       cp_OclNotEmpty  [THEN allI[THEN allI[THEN cpI1], of "OclNotEmpty"]]
       cp_OclANY       [THEN allI[THEN allI[THEN cpI1], of "OclANY"]]

subsubsection‹Const›

lemma const_OclIncluding[simp,code_unfold] :
 assumes const_x : "const x"
     and const_S : "const S"
   shows  "const (S->including⇩S⇩e⇩t(x))"
   proof -
     have A:"⋀τ τ'. ¬ (τ ⊨ υ x) ⟹ (S->including⇩S⇩e⇩t(x) τ) = (S->including⇩S⇩e⇩t(x) τ')"
            apply(simp add: foundation18)
            apply(erule const_subst[OF const_x const_invalid],simp_all)
            by(rule const_charn[OF const_invalid])
     have B: "⋀ τ τ'. ¬ (τ ⊨ δ S) ⟹ (S->including⇩S⇩e⇩t(x) τ) = (S->including⇩S⇩e⇩t(x) τ')"
            apply(simp add: foundation16', elim disjE)
            apply(erule const_subst[OF const_S const_invalid],simp_all)
            apply(rule const_charn[OF const_invalid])
            apply(erule const_subst[OF const_S const_null],simp_all)
            by(rule const_charn[OF const_invalid])
     show ?thesis
       apply(simp only: const_def,intro allI, rename_tac τ τ')
       apply(case_tac "¬ (τ ⊨ υ x)", simp add: A)
       apply(case_tac "¬ (τ ⊨ δ S)", simp_all add: B)
       apply(frule_tac τ'1= τ' in  const_OclValid2[OF const_x, THEN iffD1])
       apply(frule_tac τ'1= τ' in  const_OclValid1[OF const_S, THEN iffD1])
       apply(simp add: OclIncluding_def OclValid_def)
       apply(subst const_charn[OF const_x])
       apply(subst const_charn[OF const_S])
       by simp
qed
text_raw‹\endisatagafp›

subsection‹General Algebraic Execution Rules›
subsubsection‹Execution Rules on Including›

lemma OclIncluding_finite_rep_set :
  assumes X_def : "τ ⊨ δ X"
      and x_val : "τ ⊨ υ x"
    shows "finite ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X->including⇩S⇩e⇩t(x) τ)⌉⌉ = finite ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X τ)⌉⌉"
 proof -
  have C : "⌊⌊insert (x τ) ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X τ)⌉⌉⌋⌋ ∈ {X. X = bot ∨ X = null ∨ (∀x∈⌈⌈X⌉⌉. x ≠ bot)}"
          by(insert X_def x_val, frule Set_inv_lemma, simp add: foundation18 invalid_def)
 show "?thesis"
  by(insert X_def x_val,
     auto simp: OclIncluding_def Abs_Set⇩b⇩a⇩s⇩e_inverse[OF C]
          dest: foundation13[THEN iffD2, THEN foundation22[THEN iffD1]])
qed

lemma OclIncluding_rep_set:
 assumes S_def: "τ ⊨ δ S"
   shows "⌈⌈Rep_Set⇩b⇩a⇩s⇩e (S->including⇩S⇩e⇩t(λ_. ⌊⌊x⌋⌋) τ)⌉⌉ = insert ⌊⌊x⌋⌋ ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (S τ)⌉⌉"
 apply(simp add: OclIncluding_def S_def[simplified OclValid_def])
 apply(subst Abs_Set⇩b⇩a⇩s⇩e_inverse, simp add: bot_option_def null_option_def)
 apply(insert Set_inv_lemma[OF S_def], metis bot_option_def not_Some_eq)
 by(simp)

lemma OclIncluding_notempty_rep_set:
 assumes X_def: "τ ⊨ δ X"
     and a_val: "τ ⊨ υ a"
  shows "⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X->including⇩S⇩e⇩t(a) τ)⌉⌉ ≠ {}"
 apply(simp add: OclIncluding_def X_def[simplified OclValid_def] a_val[simplified OclValid_def])
 apply(subst Abs_Set⇩b⇩a⇩s⇩e_inverse, simp add: bot_option_def null_option_def)
 apply(insert Set_inv_lemma[OF X_def], metis a_val foundation18')
 by(simp)

lemma OclIncluding_includes0:
 assumes "τ ⊨ X->includes⇩S⇩e⇩t(x)"
   shows "X->including⇩S⇩e⇩t(x) τ = X τ"
proof -
 have includes_def: "τ ⊨ X->includes⇩S⇩e⇩t(x) ⟹ τ ⊨ δ X"
 by (metis bot_fun_def OclIncludes_def OclValid_def defined3 foundation16)

 have includes_val: "τ ⊨ X->includes⇩S⇩e⇩t(x) ⟹ τ ⊨ υ x"
 using foundation5 foundation6 by fastforce

 show ?thesis
  apply(insert includes_def[OF assms] includes_val[OF assms] assms,
        simp add: OclIncluding_def OclIncludes_def OclValid_def true_def)
  apply(drule insert_absorb, simp, subst abs_rep_simp')
 by(simp_all add: OclValid_def true_def)
qed

lemma OclIncluding_includes:
 assumes "τ ⊨ X->includes⇩S⇩e⇩t(x)"
   shows "τ ⊨ X->including⇩S⇩e⇩t(x) ≜ X"
by(simp add: StrongEq_def OclValid_def true_def OclIncluding_includes0[OF assms])

lemma OclIncluding_commute0 :
 assumes S_def : "τ ⊨ δ S"
     and i_val : "τ ⊨ υ i"
     and j_val : "τ ⊨ υ j"
   shows "τ ⊨ ((S :: ('𝔄, 'a::null) Set)->including⇩S⇩e⇩t(i)->including⇩S⇩e⇩t(j) ≜ (S->including⇩S⇩e⇩t(j)->including⇩S⇩e⇩t(i)))"
proof -
  have A : "⌊⌊insert (i τ) ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (S τ)⌉⌉⌋⌋ ∈ {X. X = bot ∨ X = null ∨ (∀x∈⌈⌈X⌉⌉. x ≠ bot)}"
           by(insert S_def i_val, frule Set_inv_lemma, simp add: foundation18 invalid_def)
  have B : "⌊⌊insert (j τ) ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (S τ)⌉⌉⌋⌋ ∈ {X. X = bot ∨ X = null ∨ (∀x∈⌈⌈X⌉⌉. x ≠ bot)}"
           by(insert S_def j_val, frule Set_inv_lemma, simp add: foundation18 invalid_def)

  have G1 : "Abs_Set⇩b⇩a⇩s⇩e ⌊⌊insert (i τ) ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (S τ)⌉⌉⌋⌋ ≠ Abs_Set⇩b⇩a⇩s⇩e None"
           by(insert A, simp add: Abs_Set⇩b⇩a⇩s⇩e_inject bot_option_def null_option_def)
  have G2 : "Abs_Set⇩b⇩a⇩s⇩e ⌊⌊insert (i τ) ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (S τ)⌉⌉⌋⌋ ≠ Abs_Set⇩b⇩a⇩s⇩e ⌊None⌋"
           by(insert A, simp add: Abs_Set⇩b⇩a⇩s⇩e_inject bot_option_def null_option_def)
  have G3 : "Abs_Set⇩b⇩a⇩s⇩e ⌊⌊insert (j τ) ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (S τ)⌉⌉⌋⌋ ≠ Abs_Set⇩b⇩a⇩s⇩e None"
           by(insert B, simp add: Abs_Set⇩b⇩a⇩s⇩e_inject bot_option_def null_option_def)
  have G4 : "Abs_Set⇩b⇩a⇩s⇩e ⌊⌊insert (j τ) ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (S τ)⌉⌉⌋⌋ ≠ Abs_Set⇩b⇩a⇩s⇩e ⌊None⌋"
           by(insert B, simp add: Abs_Set⇩b⇩a⇩s⇩e_inject bot_option_def null_option_def)

  have *   : "(δ (λ_. Abs_Set⇩b⇩a⇩s⇩e ⌊⌊insert (i τ) ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (S τ)⌉⌉⌋⌋)) τ = ⌊⌊True⌋⌋"
             by(auto simp: OclValid_def false_def  defined_def null_fun_def  true_def
                              bot_fun_def bot_Set⇩b⇩a⇩s⇩e_def  null_Set⇩b⇩a⇩s⇩e_def S_def i_val G1 G2)

  have **  : "(δ (λ_. Abs_Set⇩b⇩a⇩s⇩e ⌊⌊insert (j τ) ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (S τ)⌉⌉⌋⌋)) τ = ⌊⌊True⌋⌋"
             by(auto simp: OclValid_def false_def  defined_def null_fun_def  true_def
                              bot_fun_def bot_Set⇩b⇩a⇩s⇩e_def  null_Set⇩b⇩a⇩s⇩e_def S_def i_val G3 G4)

  have *** : "Abs_Set⇩b⇩a⇩s⇩e ⌊⌊insert(j τ)⌈⌈Rep_Set⇩b⇩a⇩s⇩e(Abs_Set⇩b⇩a⇩s⇩e⌊⌊insert(i τ)⌈⌈Rep_Set⇩b⇩a⇩s⇩e(S τ)⌉⌉⌋⌋)⌉⌉⌋⌋ =
              Abs_Set⇩b⇩a⇩s⇩e ⌊⌊insert(i τ)⌈⌈Rep_Set⇩b⇩a⇩s⇩e(Abs_Set⇩b⇩a⇩s⇩e⌊⌊insert(j τ)⌈⌈Rep_Set⇩b⇩a⇩s⇩e(S τ)⌉⌉⌋⌋)⌉⌉⌋⌋"
              by(simp add: Abs_Set⇩b⇩a⇩s⇩e_inverse[OF A] Abs_Set⇩b⇩a⇩s⇩e_inverse[OF B] Set.insert_commute)
  show ?thesis
     apply(simp add: OclIncluding_def S_def[simplified OclValid_def]
                  i_val[simplified OclValid_def] j_val[simplified OclValid_def]
                  true_def OclValid_def StrongEq_def)
     apply(subst cp_defined,
           simp add: S_def[simplified OclValid_def]
                     i_val[simplified OclValid_def] j_val[simplified OclValid_def] true_def *)
     apply(subst cp_defined,
           simp add: S_def[simplified OclValid_def]
                     i_val[simplified OclValid_def] j_val[simplified OclValid_def] true_def ** ***)
     apply(subst cp_defined,
           simp add: S_def[simplified OclValid_def]
                     i_val[simplified OclValid_def] j_val[simplified OclValid_def] true_def *)
     apply(subst cp_defined,
           simp add: S_def[simplified OclValid_def]
                     i_val[simplified OclValid_def] j_val[simplified OclValid_def] true_def * )
     apply(subst cp_defined,
           simp add: S_def[simplified OclValid_def]
                     i_val[simplified OclValid_def] j_val[simplified OclValid_def] true_def * **)
     done
qed


lemma OclIncluding_commute[simp,code_unfold]:
"((S :: ('𝔄, 'a::null) Set)->including⇩S⇩e⇩t(i)->including⇩S⇩e⇩t(j) = (S->including⇩S⇩e⇩t(j)->including⇩S⇩e⇩t(i)))"
proof -
  have A: "⋀ τ.   τ ⊨ (i ≜ invalid)   ⟹ (S->including⇩S⇩e⇩t(i)->including⇩S⇩e⇩t(j)) τ = invalid τ"
            apply(rule foundation22[THEN iffD1])
            by(erule StrongEq_L_subst2_rev, simp,simp)
  have A': "⋀ τ.   τ ⊨ (i ≜ invalid)   ⟹ (S->including⇩S⇩e⇩t(j)->including⇩S⇩e⇩t(i)) τ = invalid τ"
            apply(rule foundation22[THEN iffD1])
            by(erule StrongEq_L_subst2_rev, simp,simp)
  have B:"⋀ τ.   τ ⊨ (j ≜ invalid)   ⟹ (S->including⇩S⇩e⇩t(i)->including⇩S⇩e⇩t(j)) τ = invalid τ"
            apply(rule foundation22[THEN iffD1])
            by(erule StrongEq_L_subst2_rev, simp,simp)
  have B':"⋀ τ.   τ ⊨ (j ≜ invalid)   ⟹ (S->including⇩S⇩e⇩t(j)->including⇩S⇩e⇩t(i)) τ = invalid τ"
            apply(rule foundation22[THEN iffD1])
            by(erule StrongEq_L_subst2_rev, simp,simp)
  have C: "⋀ τ.   τ ⊨ (S ≜ invalid)   ⟹ (S->including⇩S⇩e⇩t(i)->including⇩S⇩e⇩t(j)) τ = invalid τ"
            apply(rule foundation22[THEN iffD1])
            by(erule StrongEq_L_subst2_rev, simp,simp)
  have C': "⋀ τ.  τ ⊨ (S ≜ invalid)   ⟹ (S->including⇩S⇩e⇩t(j)->including⇩S⇩e⇩t(i)) τ = invalid τ"
            apply(rule foundation22[THEN iffD1])
            by(erule StrongEq_L_subst2_rev, simp,simp)
  have D: "⋀ τ.   τ ⊨ (S ≜ null)   ⟹ (S->including⇩S⇩e⇩t(i)->including⇩S⇩e⇩t(j)) τ = invalid τ"
            apply(rule foundation22[THEN iffD1])
            by(erule StrongEq_L_subst2_rev, simp,simp)
  have D': "⋀ τ.  τ ⊨ (S ≜ null)   ⟹ (S->including⇩S⇩e⇩t(j)->including⇩S⇩e⇩t(i)) τ = invalid τ"
            apply(rule foundation22[THEN iffD1])
            by(erule StrongEq_L_subst2_rev, simp,simp)
  show ?thesis
    apply(rule ext, rename_tac τ)
    apply(case_tac "τ ⊨ (υ i)")
     apply(case_tac "τ ⊨ (υ j)")
      apply(case_tac "τ ⊨ (δ S)")
       apply(simp only: OclIncluding_commute0[THEN foundation22[THEN iffD1]])
      apply(simp add: foundation16', elim disjE)
     apply(simp add: C[OF foundation22[THEN iffD2]] C'[OF foundation22[THEN iffD2]])
    apply(simp add: D[OF foundation22[THEN iffD2]] D'[OF foundation22[THEN iffD2]])
   apply(simp add:foundation18 B[OF foundation22[THEN iffD2]] B'[OF foundation22[THEN iffD2]])
  apply(simp add:foundation18 A[OF foundation22[THEN iffD2]] A'[OF foundation22[THEN iffD2]])
 done
qed


subsubsection‹Execution Rules on Excluding›

lemma OclExcluding_finite_rep_set :
  assumes X_def : "τ ⊨ δ X"
      and x_val : "τ ⊨ υ x"
    shows "finite ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X->excluding⇩S⇩e⇩t(x) τ)⌉⌉ = finite ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X τ)⌉⌉"
 proof -
  have C : "⌊⌊⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X τ)⌉⌉ - {x τ}⌋⌋ ∈ {X. X = bot ∨ X = null ∨ (∀x∈⌈⌈X⌉⌉. x ≠ bot)}"
          apply(insert X_def x_val, frule Set_inv_lemma)
          apply(simp add: foundation18 invalid_def)
          done
 show "?thesis"
  by(insert X_def x_val,
     auto simp: OclExcluding_def Abs_Set⇩b⇩a⇩s⇩e_inverse[OF C]
          dest: foundation13[THEN iffD2, THEN foundation22[THEN iffD1]])
qed

lemma OclExcluding_rep_set:
 assumes S_def: "τ ⊨ δ S"
   shows "⌈⌈Rep_Set⇩b⇩a⇩s⇩e (S->excluding⇩S⇩e⇩t(λ_. ⌊⌊x⌋⌋) τ)⌉⌉ = ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (S τ)⌉⌉ - {⌊⌊x⌋⌋}"
 apply(simp add: OclExcluding_def S_def[simplified OclValid_def])
 apply(subst Abs_Set⇩b⇩a⇩s⇩e_inverse, simp add: bot_option_def null_option_def)
  apply(insert Set_inv_lemma[OF S_def], metis Diff_iff bot_option_def not_None_eq)
by(simp)

lemma OclExcluding_excludes0:
 assumes "τ ⊨ X->excludes⇩S⇩e⇩t(x)"
   shows "X->excluding⇩S⇩e⇩t(x) τ = X τ"
proof -
 have excludes_def: "τ ⊨ X->excludes⇩S⇩e⇩t(x) ⟹ τ ⊨ δ X"
 by (metis OclExcludes.def_valid_then_def OclExcludes_valid_args_valid'' foundation10' foundation6)

 have excludes_val: "τ ⊨ X->excludes⇩S⇩e⇩t(x) ⟹ τ ⊨ υ x"
 by (metis OclExcludes.def_valid_then_def OclExcludes_valid_args_valid'' foundation10' foundation6)

 show ?thesis
  apply(insert excludes_def[OF assms] excludes_val[OF assms] assms,
        simp add: OclExcluding_def OclExcludes_def OclIncludes_def OclNot_def OclValid_def true_def)
 by (metis (opaque_lifting, no_types) abs_rep_simp' assms excludes_def)
qed

lemma OclExcluding_excludes:
 assumes "τ ⊨ X->excludes⇩S⇩e⇩t(x)"
   shows "τ ⊨ X->excluding⇩S⇩e⇩t(x) ≜ X"
by(simp add: StrongEq_def OclValid_def true_def OclExcluding_excludes0[OF assms])

lemma OclExcluding_charn0[simp]:
assumes val_x:"τ ⊨ (υ x)"
shows         "τ ⊨ ((Set{}->excluding⇩S⇩e⇩t(x))  ≜  Set{})"
proof -
  have A : "⌊None⌋ ∈ {X. X = bot ∨ X = null ∨ (∀x∈⌈⌈X⌉⌉. x ≠ bot)}"
  by(simp add: null_option_def bot_option_def)
  have B : "⌊⌊{}⌋⌋ ∈ {X. X = bot ∨ X = null ∨ (∀x∈⌈⌈X⌉⌉. x ≠ bot)}" by(simp add: mtSet_def)

  show ?thesis using val_x
    apply(auto simp: OclValid_def OclIncludes_def OclNot_def false_def true_def StrongEq_def
                     OclExcluding_def mtSet_def defined_def bot_fun_def null_fun_def null_Set⇩b⇩a⇩s⇩e_def)
     apply(auto simp: mtSet_def Set⇩b⇩a⇩s⇩e.Abs_Set⇩b⇩a⇩s⇩e_inverse
                      Set⇩b⇩a⇩s⇩e.Abs_Set⇩b⇩a⇩s⇩e_inject[OF B A])
  done
qed

lemma OclExcluding_commute0 :
 assumes S_def : "τ ⊨ δ S"
     and i_val : "τ ⊨ υ i"
     and j_val : "τ ⊨ υ j"
   shows "τ ⊨ ((S :: ('𝔄, 'a::null) Set)->excluding⇩S⇩e⇩t(i)->excluding⇩S⇩e⇩t(j) ≜ (S->excluding⇩S⇩e⇩t(j)->excluding⇩S⇩e⇩t(i)))"
proof -
  have A : "⌊⌊⌈⌈Rep_Set⇩b⇩a⇩s⇩e (S τ)⌉⌉ - {i τ}⌋⌋ ∈ {X. X = bot ∨ X = null ∨ (∀x∈⌈⌈X⌉⌉. x ≠ bot)}"
           by(insert S_def i_val, frule Set_inv_lemma, simp add: foundation18 invalid_def)
  have B : "⌊⌊⌈⌈Rep_Set⇩b⇩a⇩s⇩e (S τ)⌉⌉ - {j τ}⌋⌋ ∈ {X. X = bot ∨ X = null ∨ (∀x∈⌈⌈X⌉⌉. x ≠ bot)}"
           by(insert S_def j_val, frule Set_inv_lemma, simp add: foundation18 invalid_def)

  have G1 : "Abs_Set⇩b⇩a⇩s⇩e ⌊⌊⌈⌈Rep_Set⇩b⇩a⇩s⇩e (S τ)⌉⌉ - {i τ}⌋⌋ ≠ Abs_Set⇩b⇩a⇩s⇩e None"
           by(insert A, simp add: Abs_Set⇩b⇩a⇩s⇩e_inject bot_option_def null_option_def)
  have G2 : "Abs_Set⇩b⇩a⇩s⇩e ⌊⌊⌈⌈Rep_Set⇩b⇩a⇩s⇩e (S τ)⌉⌉ - {i τ}⌋⌋ ≠ Abs_Set⇩b⇩a⇩s⇩e ⌊None⌋"
           by(insert A, simp add: Abs_Set⇩b⇩a⇩s⇩e_inject bot_option_def null_option_def)
  have G3 : "Abs_Set⇩b⇩a⇩s⇩e ⌊⌊⌈⌈Rep_Set⇩b⇩a⇩s⇩e (S τ)⌉⌉ - {j τ}⌋⌋ ≠ Abs_Set⇩b⇩a⇩s⇩e None"
           by(insert B, simp add: Abs_Set⇩b⇩a⇩s⇩e_inject bot_option_def null_option_def)
  have G4 : "Abs_Set⇩b⇩a⇩s⇩e ⌊⌊⌈⌈Rep_Set⇩b⇩a⇩s⇩e (S τ)⌉⌉ - {j τ}⌋⌋ ≠ Abs_Set⇩b⇩a⇩s⇩e ⌊None⌋"
           by(insert B, simp add: Abs_Set⇩b⇩a⇩s⇩e_inject bot_option_def null_option_def)

  have *   : "(δ (λ_. Abs_Set⇩b⇩a⇩s⇩e ⌊⌊⌈⌈Rep_Set⇩b⇩a⇩s⇩e (S τ)⌉⌉ - {i τ}⌋⌋)) τ = ⌊⌊True⌋⌋"
             by(auto simp: OclValid_def false_def  defined_def null_fun_def  true_def
                              bot_fun_def bot_Set⇩b⇩a⇩s⇩e_def  null_Set⇩b⇩a⇩s⇩e_def S_def i_val G1 G2)

  have **  : "(δ (λ_. Abs_Set⇩b⇩a⇩s⇩e ⌊⌊⌈⌈Rep_Set⇩b⇩a⇩s⇩e (S τ)⌉⌉ - {j τ}⌋⌋)) τ = ⌊⌊True⌋⌋"
             by(auto simp: OclValid_def false_def  defined_def null_fun_def  true_def
                              bot_fun_def bot_Set⇩b⇩a⇩s⇩e_def  null_Set⇩b⇩a⇩s⇩e_def S_def i_val G3 G4)

  have *** : "Abs_Set⇩b⇩a⇩s⇩e ⌊⌊⌈⌈Rep_Set⇩b⇩a⇩s⇩e(Abs_Set⇩b⇩a⇩s⇩e⌊⌊⌈⌈Rep_Set⇩b⇩a⇩s⇩e(S τ)⌉⌉-{i τ}⌋⌋)⌉⌉-{j τ}⌋⌋ =
              Abs_Set⇩b⇩a⇩s⇩e ⌊⌊⌈⌈Rep_Set⇩b⇩a⇩s⇩e(Abs_Set⇩b⇩a⇩s⇩e⌊⌊⌈⌈Rep_Set⇩b⇩a⇩s⇩e(S τ)⌉⌉-{j τ}⌋⌋)⌉⌉-{i τ}⌋⌋"
              apply(simp add: Abs_Set⇩b⇩a⇩s⇩e_inverse[OF A] Abs_Set⇩b⇩a⇩s⇩e_inverse[OF B])
             by (metis Diff_insert2 insert_commute)
  show ?thesis
     apply(simp add: OclExcluding_def S_def[simplified OclValid_def]
                  i_val[simplified OclValid_def] j_val[simplified OclValid_def]
                  true_def OclValid_def StrongEq_def)
     apply(subst cp_defined,
           simp add: S_def[simplified OclValid_def]
                     i_val[simplified OclValid_def] j_val[simplified OclValid_def] true_def *)
     apply(subst cp_defined,
           simp add: S_def[simplified OclValid_def]
                     i_val[simplified OclValid_def] j_val[simplified OclValid_def] true_def ** ***)
     apply(subst cp_defined,
           simp add: S_def[simplified OclValid_def]
                     i_val[simplified OclValid_def] j_val[simplified OclValid_def] true_def *)
     apply(subst cp_defined,
           simp add: S_def[simplified OclValid_def]
                     i_val[simplified OclValid_def] j_val[simplified OclValid_def] true_def * )
     apply(subst cp_defined,
           simp add: S_def[simplified OclValid_def]
                     i_val[simplified OclValid_def] j_val[simplified OclValid_def] true_def * **)
     done
qed


lemma OclExcluding_commute[simp,code_unfold]:
"((S :: ('𝔄, 'a::null) Set)->excluding⇩S⇩e⇩t(i)->excluding⇩S⇩e⇩t(j) = (S->excluding⇩S⇩e⇩t(j)->excluding⇩S⇩e⇩t(i)))"
proof -
  have A: "⋀ τ.   τ ⊨ i ≜ invalid   ⟹ (S->excluding⇩S⇩e⇩t(i)->excluding⇩S⇩e⇩t(j)) τ = invalid τ"
            apply(rule foundation22[THEN iffD1])
            by(erule StrongEq_L_subst2_rev, simp,simp)
  have A': "⋀ τ.   τ ⊨ i ≜ invalid   ⟹ (S->excluding⇩S⇩e⇩t(j)->excluding⇩S⇩e⇩t(i)) τ = invalid τ"
            apply(rule foundation22[THEN iffD1])
            by(erule StrongEq_L_subst2_rev, simp,simp)
  have B:"⋀ τ.   τ ⊨ j ≜ invalid   ⟹ (S->excluding⇩S⇩e⇩t(i)->excluding⇩S⇩e⇩t(j)) τ = invalid τ"
            apply(rule foundation22[THEN iffD1])
            by(erule StrongEq_L_subst2_rev, simp,simp)
  have B':"⋀ τ.   τ ⊨ j ≜ invalid   ⟹ (S->excluding⇩S⇩e⇩t(j)->excluding⇩S⇩e⇩t(i)) τ = invalid τ"
            apply(rule foundation22[THEN iffD1])
            by(erule StrongEq_L_subst2_rev, simp,simp)
  have C: "⋀ τ.   τ ⊨ S ≜ invalid   ⟹ (S->excluding⇩S⇩e⇩t(i)->excluding⇩S⇩e⇩t(j)) τ = invalid τ"
            apply(rule foundation22[THEN iffD1])
            by(erule StrongEq_L_subst2_rev, simp,simp)
  have C': "⋀ τ.  τ ⊨ S ≜ invalid   ⟹ (S->excluding⇩S⇩e⇩t(j)->excluding⇩S⇩e⇩t(i)) τ = invalid τ"
            apply(rule foundation22[THEN iffD1])
            by(erule StrongEq_L_subst2_rev, simp,simp)
  have D: "⋀ τ.   τ ⊨ S ≜ null   ⟹ (S->excluding⇩S⇩e⇩t(i)->excluding⇩S⇩e⇩t(j)) τ = invalid τ"
            apply(rule foundation22[THEN iffD1])
            by(erule StrongEq_L_subst2_rev, simp,simp)
  have D': "⋀ τ.  τ ⊨ S ≜ null   ⟹ (S->excluding⇩S⇩e⇩t(j)->excluding⇩S⇩e⇩t(i)) τ = invalid τ"
            apply(rule foundation22[THEN iffD1])
            by(erule StrongEq_L_subst2_rev, simp,simp)
  show ?thesis
    apply(rule ext, rename_tac τ)
    apply(case_tac "τ ⊨ (υ i)")
     apply(case_tac "τ ⊨ (υ j)")
      apply(case_tac "τ ⊨ (δ S)")
       apply(simp only: OclExcluding_commute0[THEN foundation22[THEN iffD1]])
      apply(simp add: foundation16', elim disjE)
     apply(simp add: C[OF foundation22[THEN iffD2]] C'[OF foundation22[THEN iffD2]])
    apply(simp add: D[OF foundation22[THEN iffD2]] D'[OF foundation22[THEN iffD2]])
   apply(simp add:foundation18 B[OF foundation22[THEN iffD2]] B'[OF foundation22[THEN iffD2]])
  apply(simp add:foundation18 A[OF foundation22[THEN iffD2]] A'[OF foundation22[THEN iffD2]])
 done
qed


lemma OclExcluding_charn0_exec[simp,code_unfold]:
"(Set{}->excluding⇩S⇩e⇩t(x)) = (if (υ x) then Set{} else invalid endif)"
proof -
  have A: "⋀ τ. (Set{}->excluding⇩S⇩e⇩t(invalid)) τ = (if (υ invalid) then Set{} else invalid endif) τ"
          by simp
  have B: "⋀ τ x. τ ⊨ (υ x) ⟹
                 (Set{}->excluding⇩S⇩e⇩t(x)) τ = (if (υ x) then Set{} else invalid endif) τ"
          by(simp add: OclExcluding_charn0[THEN foundation22[THEN iffD1]])
  show ?thesis
    apply(rule ext, rename_tac τ)
    apply(case_tac "τ ⊨ (υ x)")
     apply(simp add: B)
    apply(simp add: foundation18)
    apply(subst OclExcluding.cp0, simp)
    apply(simp add: cp_OclIf[symmetric] OclExcluding.cp0[symmetric] cp_valid[symmetric] A)
   done
qed

lemma OclExcluding_charn1:
assumes def_X:"τ ⊨ (δ X)"
and     val_x:"τ ⊨ (υ x)"
and     val_y:"τ ⊨ (υ y)"
and     neq  :"τ ⊨ not(x ≜ y)"
shows         "τ ⊨ ((X->including⇩S⇩e⇩t(x))->excluding⇩S⇩e⇩t(y)) ≜ ((X->excluding⇩S⇩e⇩t(y))->including⇩S⇩e⇩t(x))"
proof -
 have C : "⌊⌊insert (x τ) ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X τ)⌉⌉⌋⌋ ∈ {X. X = bot ∨ X = null ∨ (∀x∈⌈⌈X⌉⌉. x ≠ bot)}"
          by(insert def_X val_x, frule Set_inv_lemma, simp add: foundation18 invalid_def)
 have D : "⌊⌊⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X τ)⌉⌉ - {y τ}⌋⌋ ∈ {X. X = bot ∨ X = null ∨ (∀x∈⌈⌈X⌉⌉. x ≠ bot)}"
          by(insert def_X val_x, frule Set_inv_lemma, simp add: foundation18 invalid_def)
 have E : "x τ ≠ y τ"
          by(insert neq,
             auto simp: OclValid_def bot_fun_def OclIncluding_def OclIncludes_def
                        false_def true_def defined_def valid_def bot_Set⇩b⇩a⇩s⇩e_def
                        null_fun_def null_Set⇩b⇩a⇩s⇩e_def StrongEq_def OclNot_def)

 have G1 : "Abs_Set⇩b⇩a⇩s⇩e ⌊⌊insert (x τ) ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X τ)⌉⌉⌋⌋ ≠ Abs_Set⇩b⇩a⇩s⇩e None"
          by(insert C, simp add: Abs_Set⇩b⇩a⇩s⇩e_inject bot_option_def null_option_def)
 have G2 : "Abs_Set⇩b⇩a⇩s⇩e ⌊⌊insert (x τ) ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X τ)⌉⌉⌋⌋ ≠ Abs_Set⇩b⇩a⇩s⇩e ⌊None⌋"
          by(insert C, simp add: Abs_Set⇩b⇩a⇩s⇩e_inject bot_option_def null_option_def)
 have G : "(δ (λ_. Abs_Set⇩b⇩a⇩s⇩e ⌊⌊insert (x τ) ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X τ)⌉⌉⌋⌋)) τ = true τ"
          by(auto simp: OclValid_def false_def true_def defined_def
                        bot_fun_def bot_Set⇩b⇩a⇩s⇩e_def null_fun_def null_Set⇩b⇩a⇩s⇩e_def G1 G2)

 have H1 : "Abs_Set⇩b⇩a⇩s⇩e ⌊⌊⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X τ)⌉⌉ - {y τ}⌋⌋ ≠ Abs_Set⇩b⇩a⇩s⇩e None"
          by(insert D, simp add: Abs_Set⇩b⇩a⇩s⇩e_inject bot_option_def null_option_def)
 have H2 : "Abs_Set⇩b⇩a⇩s⇩e ⌊⌊⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X τ)⌉⌉ - {y τ}⌋⌋ ≠ Abs_Set⇩b⇩a⇩s⇩e ⌊None⌋"
          by(insert D, simp add: Abs_Set⇩b⇩a⇩s⇩e_inject bot_option_def null_option_def)
 have H : "(δ (λ_. Abs_Set⇩b⇩a⇩s⇩e ⌊⌊⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X τ)⌉⌉ - {y τ}⌋⌋)) τ = true τ"
          by(auto simp: OclValid_def false_def true_def defined_def
                           bot_fun_def bot_Set⇩b⇩a⇩s⇩e_def null_fun_def null_Set⇩b⇩a⇩s⇩e_def H1 H2)

 have Z : "insert (x τ) ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X τ)⌉⌉ - {y τ} = insert (x τ) (⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X τ)⌉⌉ - {y τ})"
          by(auto simp: E)
 show ?thesis
  apply(insert def_X[THEN  foundation13[THEN iffD2]] val_x[THEN  foundation13[THEN iffD2]]
               val_y[THEN  foundation13[THEN iffD2]])
  apply(simp add: foundation22 OclIncluding_def OclExcluding_def def_X[THEN foundation16[THEN iffD1]])
  apply(subst cp_defined, simp)+
  apply(simp add: G H Abs_Set⇩b⇩a⇩s⇩e_inverse[OF C] Abs_Set⇩b⇩a⇩s⇩e_inverse[OF D] Z)
  done
qed



lemma OclExcluding_charn2:
assumes def_X:"τ ⊨ (δ X)"
and     val_x:"τ ⊨ (υ x)"
shows         "τ ⊨ (((X->including⇩S⇩e⇩t(x))->excluding⇩S⇩e⇩t(x)) ≜ (X->excluding⇩S⇩e⇩t(x)))"
proof -
 have C : "⌊⌊insert (x τ) ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X τ)⌉⌉⌋⌋ ∈ {X. X = bot ∨ X = null ∨ (∀x∈⌈⌈X⌉⌉. x ≠ bot)}"
          by(insert def_X val_x, frule Set_inv_lemma, simp add: foundation18 invalid_def)
 have G1 : "Abs_Set⇩b⇩a⇩s⇩e ⌊⌊insert (x τ) ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X τ)⌉⌉⌋⌋ ≠ Abs_Set⇩b⇩a⇩s⇩e None"
          by(insert C, simp add: Abs_Set⇩b⇩a⇩s⇩e_inject bot_option_def null_option_def)
 have G2 : "Abs_Set⇩b⇩a⇩s⇩e ⌊⌊insert (x τ) ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X τ)⌉⌉⌋⌋ ≠ Abs_Set⇩b⇩a⇩s⇩e ⌊None⌋"
          by(insert C, simp add: Abs_Set⇩b⇩a⇩s⇩e_inject bot_option_def null_option_def)
 show ?thesis
   apply(insert def_X[THEN foundation16[THEN iffD1]]
                val_x[THEN foundation18[THEN iffD1]])
   apply(auto simp: OclValid_def bot_fun_def OclIncluding_def OclIncludes_def false_def true_def
                    invalid_def defined_def valid_def bot_Set⇩b⇩a⇩s⇩e_def null_fun_def null_Set⇩b⇩a⇩s⇩e_def
                    StrongEq_def)
   apply(subst OclExcluding.cp0)
   apply(auto simp:OclExcluding_def)
            apply(simp add: Abs_Set⇩b⇩a⇩s⇩e_inverse[OF C])
           apply(simp_all add: false_def true_def defined_def valid_def
                               null_fun_def bot_fun_def null_Set⇩b⇩a⇩s⇩e_def bot_Set⇩b⇩a⇩s⇩e_def
                          split: bool.split_asm HOL.if_split_asm option.split)
   apply(auto simp: G1 G2)
  done
qed




theorem OclExcluding_charn3:  "((X->including⇩S⇩e⇩t(x))->excluding⇩S⇩e⇩t(x)) = (X->excluding⇩S⇩e⇩t(x))"
proof -
 have A1 : "⋀τ. τ ⊨ (X ≜ invalid) ⟹ (X->including⇩S⇩e⇩t(x)->excluding⇩S⇩e⇩t(x)) τ = invalid τ"
            apply(rule foundation22[THEN iffD1])
            by(erule StrongEq_L_subst2_rev, simp,simp)
 have A1': "⋀τ. τ ⊨ (X ≜ invalid) ⟹ (X->excluding⇩S⇩e⇩t(x)) τ = invalid τ"
            apply(rule foundation22[THEN iffD1])
            by(erule StrongEq_L_subst2_rev, simp,simp)
 have A2 : "⋀τ. τ ⊨ (X ≜ null) ⟹ (X->including⇩S⇩e⇩t(x)->excluding⇩S⇩e⇩t(x)) τ = invalid τ"
            apply(rule foundation22[THEN iffD1])
            by(erule StrongEq_L_subst2_rev, simp,simp)
 have A2': "⋀τ. τ ⊨ (X ≜ null) ⟹ (X->excluding⇩S⇩e⇩t(x)) τ = invalid τ"
            apply(rule foundation22[THEN iffD1])
            by(erule StrongEq_L_subst2_rev, simp,simp)
 have A3 : "⋀τ. τ ⊨ (x ≜ invalid) ⟹ (X->including⇩S⇩e⇩t(x)->excluding⇩S⇩e⇩t(x)) τ = invalid τ"
            apply(rule foundation22[THEN iffD1])
            by(erule StrongEq_L_subst2_rev, simp,simp)
 have A3': "⋀τ. τ ⊨ (x ≜ invalid) ⟹ (X->excluding⇩S⇩e⇩t(x)) τ = invalid τ"
            apply(rule foundation22[THEN iffD1])
            by(erule StrongEq_L_subst2_rev, simp,simp)

 show ?thesis
 apply(rule ext, rename_tac "τ")
 apply(case_tac "τ ⊨ (υ x)")
  apply(case_tac "τ ⊨ (δ X)")
   apply(simp only: OclExcluding_charn2[THEN foundation22[THEN iffD1]])
   apply(simp add: foundation16', elim disjE)
   apply(simp add: A1[OF foundation22[THEN iffD2]] A1'[OF foundation22[THEN iffD2]])
  apply(simp add: A2[OF foundation22[THEN iffD2]] A2'[OF foundation22[THEN iffD2]])
 apply(simp add:foundation18 A3[OF foundation22[THEN iffD2]] A3'[OF foundation22[THEN iffD2]])
 done
qed


text‹One would like a generic theorem of the form:
\begin{isar}[mathescape]
lemma OclExcluding_charn_exec:
       "(X->including$_{Set}$(x::('$\mathfrak{A}$,'a::null)val)->excluding$_{Set}$(y)) =
        (if δ X then if x ≐ y
                     then X->excluding$_{Set}$(y)
                     else X->excluding$_{Set}$(y)->including$_{Set}$(x)
                     endif
                else invalid endif)"
\end{isar}
Unfortunately, this does not hold in general, since referential equality is
an overloaded concept and has to be defined for each type individually.
Consequently, it is only valid for concrete  type instances for Boolean,
Integer, and Sets thereof...
›


text‹The computational law \emph{OclExcluding-charn-exec} becomes generic since it
uses strict equality which in itself is generic. It is possible to prove
the following generic theorem and instantiate it later (using properties
that link the polymorphic logical strong equality with the concrete instance
of strict quality).›
lemma OclExcluding_charn_exec:
 assumes strict1: "(invalid ≐ y) = invalid"
 and     strict2: "(x ≐ invalid) = invalid"
 and     StrictRefEq_valid_args_valid: "⋀ (x::('𝔄,'a::null)val) y τ.
                                     (τ ⊨ δ (x ≐ y)) = ((τ ⊨ (υ x)) ∧ (τ ⊨ υ y))"
 and     cp_StrictRefEq: "⋀ (X::('𝔄,'a::null)val) Y τ. (X ≐ Y) τ = ((λ_. X τ) ≐ (λ_. Y τ)) τ"
 and     StrictRefEq_vs_StrongEq: "⋀ (x::('𝔄,'a::null)val) y τ.
                                      τ ⊨ υ x ⟹ τ ⊨ υ y ⟹ (τ ⊨ ((x ≐ y) ≜ (x ≜ y)))"
 shows "(X->including⇩S⇩e⇩t(x::('𝔄,'a::null)val)->excluding⇩S⇩e⇩t(y)) =
        (if δ X then if x ≐ y
                     then X->excluding⇩S⇩e⇩t(y)
                     else X->excluding⇩S⇩e⇩t(y)->including⇩S⇩e⇩t(x)
                     endif
                else invalid endif)"
proof -
 (* Lifting theorems, largely analogous OclIncludes_execute_generic,
         with the same problems wrt. strict equality. *)
 have A1: "⋀τ. τ ⊨ (X ≜ invalid) ⟹
            (X->including⇩S⇩e⇩t(x)->includes⇩S⇩e⇩t(y)) τ = invalid τ"
            apply(rule foundation22[THEN iffD1])
            by(erule StrongEq_L_subst2_rev, simp,simp)

 have B1: "⋀τ. τ ⊨ (X ≜ null) ⟹
            (X->including⇩S⇩e⇩t(x)->includes⇩S⇩e⇩t(y)) τ = invalid  τ"
            apply(rule foundation22[THEN iffD1])
            by(erule StrongEq_L_subst2_rev, simp,simp)

 have A2: "⋀τ. τ ⊨ (X ≜ invalid) ⟹ X->including⇩S⇩e⇩t(x)->excluding⇩S⇩e⇩t(y) τ = invalid τ"
            apply(rule foundation22[THEN iffD1])
            by(erule StrongEq_L_subst2_rev, simp,simp)

 have B2: "⋀τ. τ ⊨ (X ≜ null) ⟹ X->including⇩S⇩e⇩t(x)->excluding⇩S⇩e⇩t(y) τ = invalid τ"
            apply(rule foundation22[THEN iffD1])
            by(erule StrongEq_L_subst2_rev, simp,simp)

 note [simp] = cp_StrictRefEq [THEN allI[THEN allI[THEN allI[THEN cpI2]], of "StrictRefEq"]]

 have C: "⋀τ. τ ⊨ (x ≜ invalid) ⟹
           (X->including⇩S⇩e⇩t(x)->excluding⇩S⇩e⇩t(y)) τ =
           (if x ≐ y then X->excluding⇩S⇩e⇩t(y) else X->excluding⇩S⇩e⇩t(y)->including⇩S⇩e⇩t(x) endif) τ"
            apply(rule foundation22[THEN iffD1])
            apply(erule StrongEq_L_subst2_rev,simp,simp)
            by(simp add: strict1)

 have D: "⋀τ. τ ⊨ (y ≜ invalid) ⟹
           (X->including⇩S⇩e⇩t(x)->excluding⇩S⇩e⇩t(y)) τ =
           (if x ≐ y then X->excluding⇩S⇩e⇩t(y) else X->excluding⇩S⇩e⇩t(y)->including⇩S⇩e⇩t(x) endif) τ"
            apply(rule foundation22[THEN iffD1])
            apply(erule StrongEq_L_subst2_rev,simp,simp)
            by (simp add: strict2)

 have E: "⋀τ. τ ⊨ υ x ⟹ τ ⊨ υ y ⟹
              (if x ≐ y then X->excluding⇩S⇩e⇩t(y) else X->excluding⇩S⇩e⇩t(y)->including⇩S⇩e⇩t(x) endif) τ =
              (if x ≜ y then X->excluding⇩S⇩e⇩t(y) else X->excluding⇩S⇩e⇩t(y)->including⇩S⇩e⇩t(x) endif) τ"
           apply(subst cp_OclIf)
           apply(subst StrictRefEq_vs_StrongEq[THEN foundation22[THEN iffD1]])
           by(simp_all add: cp_OclIf[symmetric])

 have F: "⋀τ. τ ⊨ δ X ⟹ τ ⊨ υ x ⟹ τ ⊨ (x ≜ y) ⟹
           (X->including⇩S⇩e⇩t(x)->excluding⇩S⇩e⇩t(y) τ) = (X->excluding⇩S⇩e⇩t(y) τ)"
           apply(drule StrongEq_L_sym)
           apply(rule foundation22[THEN iffD1])
           apply(erule StrongEq_L_subst2_rev,simp)
           by(simp add: OclExcluding_charn2)

 show ?thesis
    apply(rule ext, rename_tac "τ")
    apply(case_tac "¬ (τ ⊨ (δ X))", simp add:defined_split,elim disjE A1 B1 A2 B2)
    apply(case_tac "¬ (τ ⊨ (υ x))",
          simp add:foundation18 foundation22[symmetric],
          drule StrongEq_L_sym)
     apply(simp add: foundation22 C)
    apply(case_tac "¬ (τ ⊨ (υ y))",
          simp add:foundation18 foundation22[symmetric],
          drule StrongEq_L_sym, simp add: foundation22 D, simp)
    apply(subst E,simp_all)
    apply(case_tac "τ ⊨ not (x ≜ y)")
     apply(simp add: OclExcluding_charn1[simplified foundation22]
                     OclExcluding_charn2[simplified foundation22])
    apply(simp add: foundation9 F)
 done
qed


(* Hack to work around OF-Bug *)
schematic_goal OclExcluding_charn_exec⇩I⇩n⇩t⇩e⇩g⇩e⇩r[simp,code_unfold]: "?X"
by(rule OclExcluding_charn_exec[OF StrictRefEq⇩I⇩n⇩t⇩e⇩g⇩e⇩r.strict1 StrictRefEq⇩I⇩n⇩t⇩e⇩g⇩e⇩r.strict2
                                StrictRefEq⇩I⇩n⇩t⇩e⇩g⇩e⇩r.defined_args_valid
                                StrictRefEq⇩I⇩n⇩t⇩e⇩g⇩e⇩r.cp0 StrictRefEq⇩I⇩n⇩t⇩e⇩g⇩e⇩r.StrictRefEq_vs_StrongEq], simp_all)

schematic_goal OclExcluding_charn_exec⇩B⇩o⇩o⇩l⇩e⇩a⇩n[simp,code_unfold]: "?X"
by(rule OclExcluding_charn_exec[OF StrictRefEq⇩B⇩o⇩o⇩l⇩e⇩a⇩n.strict1 StrictRefEq⇩B⇩o⇩o⇩l⇩e⇩a⇩n.strict2
                                StrictRefEq⇩B⇩o⇩o⇩l⇩e⇩a⇩n.defined_args_valid
                             StrictRefEq⇩B⇩o⇩o⇩l⇩e⇩a⇩n.cp0 StrictRefEq⇩B⇩o⇩o⇩l⇩e⇩a⇩n.StrictRefEq_vs_StrongEq], simp_all)


schematic_goal OclExcluding_charn_exec⇩S⇩e⇩t[simp,code_unfold]: "?X"
by(rule OclExcluding_charn_exec[OF StrictRefEq⇩S⇩e⇩t.strict1 StrictRefEq⇩S⇩e⇩t.strict2
                                StrictRefEq⇩S⇩e⇩t.defined_args_valid
                                StrictRefEq⇩S⇩e⇩t.cp0 StrictRefEq⇩S⇩e⇩t.StrictRefEq_vs_StrongEq], simp_all)


subsubsection‹Execution Rules on Includes›

lemma OclIncludes_charn0[simp]:
assumes val_x:"τ ⊨ (υ x)"
shows         "τ ⊨ not(Set{}->includes⇩S⇩e⇩t(x))"
using val_x
apply(auto simp: OclValid_def OclIncludes_def OclNot_def false_def true_def)
apply(auto simp: mtSet_def Set⇩b⇩a⇩s⇩e.Abs_Set⇩b⇩a⇩s⇩e_inverse)
done


lemma OclIncludes_charn0'[simp,code_unfold]:
"Set{}->includes⇩S⇩e⇩t(x) = (if υ x then false else invalid endif)"
proof -
  have A: "⋀ τ. (Set{}->includes⇩S⇩e⇩t(invalid)) τ = (if (υ invalid) then false else invalid endif) τ"
          by simp
  have B: "⋀ τ x. τ ⊨ (υ x) ⟹ (Set{}->includes⇩S⇩e⇩t(x)) τ = (if υ x then false else invalid endif) τ"
          apply(frule OclIncludes_charn0, simp add: OclValid_def)
          apply(rule foundation21[THEN fun_cong, simplified StrongEq_def,simplified,
                     THEN iffD1, of _ _ "false"])
          by simp
  show ?thesis
    apply(rule ext, rename_tac τ)
    apply(case_tac "τ ⊨ (υ x)")
     apply(simp_all add: B foundation18)
    apply(subst OclIncludes.cp0, simp add: OclIncludes.cp0[symmetric] A)
  done
qed

lemma OclIncludes_charn1:
assumes def_X:"τ ⊨ (δ X)"
assumes val_x:"τ ⊨ (υ x)"
shows         "τ ⊨ (X->including⇩S⇩e⇩t(x)->includes⇩S⇩e⇩t(x))"
proof -
 have C : "⌊⌊insert (x τ) ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X τ)⌉⌉⌋⌋ ∈ {X. X = bot ∨ X = null ∨ (∀x∈⌈⌈X⌉⌉. x ≠ bot)}"
          by(insert def_X val_x, frule Set_inv_lemma, simp add: foundation18 invalid_def)
 show ?thesis
  apply(subst OclIncludes_def, simp add: foundation10[simplified OclValid_def] OclValid_def
                                 def_X[simplified OclValid_def] val_x[simplified OclValid_def])
  apply(simp add: OclIncluding_def def_X[simplified OclValid_def] val_x[simplified OclValid_def]
                  Abs_Set⇩b⇩a⇩s⇩e_inverse[OF C] true_def)
 done
qed



lemma OclIncludes_charn2:
assumes def_X:"τ ⊨ (δ X)"
and     val_x:"τ ⊨ (υ x)"
and     val_y:"τ ⊨ (υ y)"
and     neq  :"τ ⊨ not(x ≜ y)"
shows         "τ ⊨ (X->including⇩S⇩e⇩t(x)->includes⇩S⇩e⇩t(y)) ≜ (X->includes⇩S⇩e⇩t(y))"
proof -
 have C : "⌊⌊insert (x τ) ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X τ)⌉⌉⌋⌋ ∈ {X. X = bot ∨ X = null ∨ (∀x∈⌈⌈X⌉⌉. x ≠ bot)}"
          by(insert def_X val_x, frule Set_inv_lemma, simp add: foundation18 invalid_def)
 show ?thesis
  apply(subst OclIncludes_def,
        simp add: def_X[simplified OclValid_def] val_x[simplified OclValid_def]
                  val_y[simplified OclValid_def] foundation10[simplified OclValid_def]
                  OclValid_def StrongEq_def)
  apply(simp add: OclIncluding_def OclIncludes_def def_X[simplified OclValid_def]
                  val_x[simplified OclValid_def] val_y[simplified OclValid_def]
                  Abs_Set⇩b⇩a⇩s⇩e_inverse[OF C] true_def)
 by(metis foundation22 foundation6 foundation9 neq)
qed

text‹Here is again a generic theorem similar as above.›

lemma OclIncludes_execute_generic:
assumes strict1: "(invalid ≐ y) = invalid"
and     strict2: "(x ≐ invalid) = invalid"
and     cp_StrictRefEq: "⋀ (X::('𝔄,'a::null)val) Y τ. (X ≐ Y) τ = ((λ_. X τ) ≐ (λ_. Y τ)) τ"
and     StrictRefEq_vs_StrongEq: "⋀ (x::('𝔄,'a::null)val) y τ.
                                      τ ⊨ υ x ⟹ τ ⊨ υ y ⟹ (τ ⊨ ((x ≐ y) ≜ (x ≜ y)))"
shows
      "(X->including⇩S⇩e⇩t(x::('𝔄,'a::null)val)->includes⇩S⇩e⇩t(y)) =
       (if δ X then if x ≐ y then true else X->includes⇩S⇩e⇩t(y) endif else invalid endif)"
proof -
  have A: "⋀τ. τ ⊨ (X ≜ invalid) ⟹
            (X->including⇩S⇩e⇩t(x)->includes⇩S⇩e⇩t(y)) τ = invalid τ"
            apply(rule foundation22[THEN iffD1])
            by(erule StrongEq_L_subst2_rev,simp,simp)
  have B: "⋀τ. τ ⊨ (X ≜ null) ⟹
            (X->including⇩S⇩e⇩t(x)->includes⇩S⇩e⇩t(y)) τ = invalid  τ"
            apply(rule foundation22[THEN iffD1])
            by(erule StrongEq_L_subst2_rev,simp,simp)

  note [simp] = cp_StrictRefEq [THEN allI[THEN allI[THEN allI[THEN cpI2]], of "StrictRefEq"]]

  have C: "⋀τ. τ ⊨ (x ≜ invalid) ⟹
           (X->including⇩S⇩e⇩t(x)->includes⇩S⇩e⇩t(y)) τ =
           (if x ≐ y then true else X->includes⇩S⇩e⇩t(y) endif) τ"
            apply(rule foundation22[THEN iffD1])
            apply(erule StrongEq_L_subst2_rev,simp,simp)
            by (simp add: strict1)
  have D:"⋀τ. τ ⊨ (y ≜ invalid) ⟹
           (X->including⇩S⇩e⇩t(x)->includes⇩S⇩e⇩t(y)) τ =
           (if x ≐ y then true else X->includes⇩S⇩e⇩t(y) endif) τ"
            apply(rule foundation22[THEN iffD1])
            apply(erule StrongEq_L_subst2_rev,simp,simp)
            by (simp add: strict2)
  have E: "⋀τ. τ ⊨ υ x ⟹ τ ⊨ υ y ⟹
              (if x ≐ y then true else X->includes⇩S⇩e⇩t(y) endif) τ =
              (if x ≜ y then true else X->includes⇩S⇩e⇩t(y) endif) τ"
           apply(subst cp_OclIf)
           apply(subst StrictRefEq_vs_StrongEq[THEN foundation22[THEN iffD1]])
           by(simp_all add: cp_OclIf[symmetric])
  have F: "⋀τ. τ ⊨ (x ≜ y) ⟹
               (X->including⇩S⇩e⇩t(x)->includes⇩S⇩e⇩t(y)) τ = (X->including⇩S⇩e⇩t(x)->includes⇩S⇩e⇩t(x)) τ"
           apply(rule foundation22[THEN iffD1])
           by(erule StrongEq_L_subst2_rev,simp, simp)
  show ?thesis
    apply(rule ext, rename_tac "τ")
    apply(case_tac "¬ (τ ⊨ (δ X))", simp add:defined_split,elim disjE A B)
    apply(case_tac "¬ (τ ⊨ (υ x))",
          simp add:foundation18 foundation22[symmetric],
          drule StrongEq_L_sym)
     apply(simp add: foundation22 C)
    apply(case_tac "¬ (τ ⊨ (υ y))",
          simp add:foundation18 foundation22[symmetric],
          drule StrongEq_L_sym, simp add: foundation22 D, simp)
    apply(subst E,simp_all)
    apply(case_tac "τ ⊨ not(x ≜ y)")
     apply(simp add: OclIncludes_charn2[simplified foundation22])
    apply(simp add: foundation9 F
                    OclIncludes_charn1[THEN foundation13[THEN iffD2],
                                     THEN foundation22[THEN iffD1]])
  done
qed


(* Hack to work around OF-Bug *)
schematic_goal OclIncludes_execute⇩I⇩n⇩t⇩e⇩g⇩e⇩r[simp,code_unfold]: "?X"
by(rule OclIncludes_execute_generic[OF StrictRefEq⇩I⇩n⇩t⇩e⇩g⇩e⇩r.strict1 StrictRefEq⇩I⇩n⇩t⇩e⇩g⇩e⇩r.strict2
                                    StrictRefEq⇩I⇩n⇩t⇩e⇩g⇩e⇩r.cp0
                                    StrictRefEq⇩I⇩n⇩t⇩e⇩g⇩e⇩r.StrictRefEq_vs_StrongEq], simp_all)


schematic_goal OclIncludes_execute⇩B⇩o⇩o⇩l⇩e⇩a⇩n[simp,code_unfold]: "?X"
by(rule OclIncludes_execute_generic[OF StrictRefEq⇩B⇩o⇩o⇩l⇩e⇩a⇩n.strict1 StrictRefEq⇩B⇩o⇩o⇩l⇩e⇩a⇩n.strict2
                                    StrictRefEq⇩B⇩o⇩o⇩l⇩e⇩a⇩n.cp0
                                    StrictRefEq⇩B⇩o⇩o⇩l⇩e⇩a⇩n.StrictRefEq_vs_StrongEq], simp_all)


schematic_goal OclIncludes_execute⇩S⇩e⇩t[simp,code_unfold]: "?X"
by(rule OclIncludes_execute_generic[OF StrictRefEq⇩S⇩e⇩t.strict1 StrictRefEq⇩S⇩e⇩t.strict2
                                    StrictRefEq⇩S⇩e⇩t.cp0
                                    StrictRefEq⇩S⇩e⇩t.StrictRefEq_vs_StrongEq], simp_all)

lemma OclIncludes_including_generic :
 assumes OclIncludes_execute_generic [simp] : "⋀X x y.
           (X->including⇩S⇩e⇩t(x::('𝔄,'a::null)val)->includes⇩S⇩e⇩t(y)) =
           (if δ X then if x ≐ y then true else X->includes⇩S⇩e⇩t(y) endif else invalid endif)"
     and StrictRefEq_strict'' : "⋀x y. δ ((x::('𝔄,'a::null)val) ≐ y) = (υ(x) and υ(y))"
     and a_val : "τ ⊨ υ a"
     and x_val : "τ ⊨ υ x"
     and S_incl : "τ ⊨ (S)->includes⇩S⇩e⇩t((x::('𝔄,'a::null)val))"
   shows "τ ⊨ S->including⇩S⇩e⇩t((a::('𝔄,'a::null)val))->includes⇩S⇩e⇩t(x)"
proof -
 have discr_eq_bot1_true : "⋀τ. (⊥ τ = true τ) = False"
 by (metis bot_fun_def foundation1 foundation18' valid3)
 have discr_eq_bot2_true : "⋀τ. (⊥ = true τ) = False"
 by (metis bot_fun_def discr_eq_bot1_true)
 have discr_neq_invalid_true : "⋀τ. (invalid τ ≠ true τ) = True"
 by (metis discr_eq_bot2_true invalid_def)
 have discr_eq_invalid_true : "⋀τ. (invalid τ = true τ) = False"
 by (metis bot_option_def invalid_def option.simps(2) true_def)
show ?thesis
  apply(simp)
  apply(subgoal_tac "τ ⊨ δ S")
   prefer 2
   apply(insert S_incl[simplified OclIncludes_def], simp add:  OclValid_def)
   apply(metis discr_eq_bot2_true)
  apply(simp add: cp_OclIf[of "δ S"] OclValid_def OclIf_def x_val[simplified OclValid_def]
                  discr_neq_invalid_true discr_eq_invalid_true)
 by (metis OclValid_def S_incl StrictRefEq_strict'' a_val foundation10 foundation6 x_val)
qed

lemmas OclIncludes_including⇩I⇩n⇩t⇩e⇩g⇩e⇩r =
       OclIncludes_including_generic[OF OclIncludes_execute⇩I⇩n⇩t⇩e⇩g⇩e⇩r StrictRefEq⇩I⇩n⇩t⇩e⇩g⇩e⇩r.def_homo]

subsubsection‹Execution Rules on Excludes›

lemma OclExcludes_charn1:
assumes def_X:"τ ⊨ (δ X)"
assumes val_x:"τ ⊨ (υ x)"
shows         "τ ⊨ (X->excluding⇩S⇩e⇩t(x)->excludes⇩S⇩e⇩t(x))"
proof -
 let ?OclSet = "λS. ⌊⌊S⌋⌋ ∈ {X. X = ⊥ ∨ X = null ∨ (∀x∈⌈⌈X⌉⌉. x ≠ ⊥)}"
 have diff_in_Set⇩b⇩a⇩s⇩e : "?OclSet (⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X τ)⌉⌉ - {x τ})"
  apply(simp, (rule disjI2)+)
 by (metis (opaque_lifting, no_types) Diff_iff Set_inv_lemma def_X)

 show ?thesis
  apply(subst OclExcludes_def, simp add: foundation10[simplified OclValid_def] OclValid_def
                                 def_X[simplified OclValid_def] val_x[simplified OclValid_def])
  apply(subst OclIncludes_def, simp add: OclNot_def)
  apply(simp add: OclExcluding_def def_X[simplified OclValid_def] val_x[simplified OclValid_def]
                  Abs_Set⇩b⇩a⇩s⇩e_inverse[OF diff_in_Set⇩b⇩a⇩s⇩e] true_def)
 by(simp add: OclAnd_def def_X[simplified OclValid_def] val_x[simplified OclValid_def] true_def)
qed

subsubsection‹Execution Rules on Size›

lemma [simp,code_unfold]: "Set{} ->size⇩S⇩e⇩t() = 𝟬"
 apply(rule ext)
 apply(simp add: defined_def mtSet_def OclSize_def
                 bot_Set⇩b⇩a⇩s⇩e_def bot_fun_def
                 null_Set⇩b⇩a⇩s⇩e_def null_fun_def)
 apply(subst Abs_Set⇩b⇩a⇩s⇩e_inject, simp_all add: bot_option_def null_option_def) +
by(simp add: Abs_Set⇩b⇩a⇩s⇩e_inverse bot_option_def null_option_def OclInt0_def)

lemma OclSize_including_exec[simp,code_unfold]:
 "((X ->including⇩S⇩e⇩t(x)) ->size⇩S⇩e⇩t()) = (if δ X and υ x then
                                     X ->size⇩S⇩e⇩t() +⇩i⇩n⇩t if X ->includes⇩S⇩e⇩t(x) then 𝟬 else 𝟭 endif
                                   else
                                     invalid
                                   endif)"
proof -

 have valid_inject_true : "⋀τ P. (υ P) τ ≠ true τ ⟹ (υ P) τ = false τ"
      apply(simp add: valid_def true_def false_def bot_fun_def bot_option_def
                      null_fun_def null_option_def)
      by (case_tac "P τ = ⊥", simp_all add: true_def)
 have defined_inject_true : "⋀τ P. (δ P) τ ≠ true τ ⟹ (δ P) τ = false τ"
      apply(simp add: defined_def true_def false_def bot_fun_def bot_option_def
                      null_fun_def null_option_def)
      by (case_tac " P τ = ⊥ ∨ P τ = null", simp_all add: true_def)

 show ?thesis
  apply(rule ext, rename_tac τ)
  proof -
  fix τ
  have includes_notin: "¬ τ ⊨ X->includes⇩S⇩e⇩t(x) ⟹ (δ X) τ = true τ ∧ (υ x) τ = true τ ⟹
                        x τ ∉ ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X τ)⌉⌉"
  by(simp add: OclIncludes_def OclValid_def true_def)

  have includes_def: "τ ⊨ X->includes⇩S⇩e⇩t(x) ⟹ τ ⊨ δ X"
  by (metis bot_fun_def OclIncludes_def OclValid_def defined3 foundation16)

  have includes_val: "τ ⊨ X->includes⇩S⇩e⇩t(x) ⟹ τ ⊨ υ x"
  using foundation5 foundation6 by fastforce

  have ins_in_Set⇩b⇩a⇩s⇩e: "τ ⊨ δ X ⟹ τ ⊨ υ x ⟹
    ⌊⌊insert (x τ) ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X τ)⌉⌉⌋⌋ ∈ {X. X = ⊥ ∨ X = null ∨ (∀x∈⌈⌈X⌉⌉. x ≠ ⊥)}"
   apply(simp add: bot_option_def null_option_def)
  by (metis (opaque_lifting, no_types) Set_inv_lemma foundation18' foundation5)

  have m : "⋀τ. (λ_. ⊥) = (λ_. invalid τ)" by(rule ext, simp add:invalid_def)
  
  show "X->including⇩S⇩e⇩t(x)->size⇩S⇩e⇩t() τ = (if δ X and υ x
                                     then X->size⇩S⇩e⇩t() +⇩i⇩n⇩t if X->includes⇩S⇩e⇩t(x) then 𝟬 else 𝟭 endif
                                     else invalid endif) τ"
   apply(case_tac "τ ⊨ δ X and υ x", simp)
    apply(subst OclAdd⇩I⇩n⇩t⇩e⇩g⇩e⇩r.cp0)
    apply(case_tac "τ ⊨ X->includes⇩S⇩e⇩t(x)", simp add: OclAdd⇩I⇩n⇩t⇩e⇩g⇩e⇩r.cp0[symmetric])
     apply(case_tac "τ ⊨ ((υ (X->size⇩S⇩e⇩t())) and not (δ (X->size⇩S⇩e⇩t())))", simp)
      apply(drule foundation5[where P = "υ X->size⇩S⇩e⇩t()"], erule conjE)
      apply(drule OclSize_infinite)
      apply(frule includes_def, drule includes_val, simp)
      apply(subst OclSize_def, subst OclIncluding_finite_rep_set, assumption+)
     apply (metis (opaque_lifting, no_types) invalid_def)

     apply(subst OclIf_false',
           metis (opaque_lifting, no_types) defined5 defined6 defined_and_I defined_not_I
                                       foundation1 foundation9)
    apply(subst cp_OclSize, simp add: OclIncluding_includes0 cp_OclSize[symmetric])
    (* *)
    apply(subst OclIf_false', subst foundation9, auto, simp add: OclSize_def)
    apply(drule foundation5)
    apply(subst (1 2) OclIncluding_finite_rep_set, fast+)
    apply(subst (1 2) cp_OclAnd, subst (1 2) OclAdd⇩I⇩n⇩t⇩e⇩g⇩e⇩r.cp0, simp)
    apply(rule conjI)
     apply(simp add: OclIncluding_def)
     apply(subst Abs_Set⇩b⇩a⇩s⇩e_inverse[OF ins_in_Set⇩b⇩a⇩s⇩e], fast+)
     apply(subst (asm) (2 3) OclValid_def, simp add: OclAdd⇩I⇩n⇩t⇩e⇩g⇩e⇩r_def OclInt1_def)
     apply(rule impI)
     apply(drule Finite_Set.card.insert[where x = "x τ"])
     apply(rule includes_notin, simp, simp)
     apply (metis Suc_eq_plus1 of_nat_1 of_nat_add)

    apply(subst (1 2) m[of τ], simp only:   OclAdd⇩I⇩n⇩t⇩e⇩g⇩e⇩r.cp0[symmetric],simp, simp add:invalid_def)
    apply(subst OclIncluding_finite_rep_set, fast+, simp add: OclValid_def)
   (* *)
   apply(subst OclIf_false', metis (opaque_lifting, no_types) defined6 foundation1 foundation9
                                                         OclExcluding_valid_args_valid'')
  by (metis cp_OclSize foundation18' OclIncluding_valid_args_valid'' invalid_def OclSize_invalid)
 qed
qed

subsubsection‹Execution Rules on IsEmpty›

lemma [simp,code_unfold]: "Set{}->isEmpty⇩S⇩e⇩t() = true"
by(simp add: OclIsEmpty_def)

lemma OclIsEmpty_including [simp]:
assumes X_def: "τ ⊨ δ X"
    and X_finite: "finite ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X τ)⌉⌉"
    and a_val: "τ ⊨ υ a"
shows "X->including⇩S⇩e⇩t(a)->isEmpty⇩S⇩e⇩t() τ = false τ"
proof -
 have A1 : "⋀τ X. X τ = true τ ∨ X τ = false τ ⟹ (X and not X) τ = false τ"
 by (metis (no_types) OclAnd_false1 OclAnd_idem OclImplies_def OclNot3 OclNot_not OclOr_false1
                      cp_OclAnd cp_OclNot deMorgan1 deMorgan2)

 have defined_inject_true : "⋀τ P. (δ P) τ ≠ true τ ⟹ (δ P) τ = false τ"
      apply(simp add: defined_def true_def false_def bot_fun_def bot_option_def
                      null_fun_def null_option_def)
      by (case_tac " P τ = ⊥ ∨ P τ = null", simp_all add: true_def)

 have B : "⋀X τ. τ ⊨ υ X ⟹ X τ ≠ 𝟬 τ ⟹ (X ≐ 𝟬) τ = false τ"
      apply(simp add: foundation22[symmetric] foundation14 foundation9)
      apply(erule StrongEq_L_subst4_rev[THEN iffD2, OF StrictRefEq⇩I⇩n⇩t⇩e⇩g⇩e⇩r.StrictRefEq_vs_StrongEq])
      by(simp_all)

 show ?thesis
  apply(simp add: OclIsEmpty_def del: OclSize_including_exec)
  apply(subst cp_OclOr, subst A1)
   apply (metis OclExcludes.def_homo defined_inject_true)
  apply(simp add: cp_OclOr[symmetric] del: OclSize_including_exec)
  apply(rule B,
        rule foundation20,
        metis OclIncluding.def_homo OclIncluding_finite_rep_set X_def X_finite a_val foundation10' size_defined')
  apply(simp add: OclSize_def OclIncluding_finite_rep_set[OF X_def a_val] X_finite OclInt0_def)
 by (metis OclValid_def X_def a_val foundation10 foundation6
           OclIncluding_notempty_rep_set[OF X_def a_val])
qed

subsubsection‹Execution Rules on NotEmpty›

lemma [simp,code_unfold]: "Set{}->notEmpty⇩S⇩e⇩t() = false"
by(simp add: OclNotEmpty_def)

lemma OclNotEmpty_including [simp,code_unfold]:
assumes X_def: "τ ⊨ δ X"
    and X_finite: "finite ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X τ)⌉⌉"
    and a_val: "τ ⊨ υ a"
shows "X->including⇩S⇩e⇩t(a)->notEmpty⇩S⇩e⇩t() τ = true τ"
 apply(simp add: OclNotEmpty_def)
 apply(subst cp_OclNot, subst OclIsEmpty_including, simp_all add: assms)
by (metis OclNot4 cp_OclNot)

subsubsection‹Execution Rules on Any›

lemma [simp,code_unfold]: "Set{}->any⇩S⇩e⇩t() = null"
by(rule ext, simp add: OclANY_def, simp add: false_def true_def)

lemma OclANY_singleton_exec[simp,code_unfold]:
      "(Set{}->including⇩S⇩e⇩t(a))->any⇩S⇩e⇩t() = a"
 apply(rule ext, rename_tac τ, simp add: mtSet_def OclANY_def)
 apply(case_tac "τ ⊨ υ a")
  apply(simp add: OclValid_def mtSet_defined[simplified mtSet_def]
                  mtSet_valid[simplified mtSet_def] mtSet_rep_set[simplified mtSet_def])
  apply(subst (1 2) cp_OclAnd,
        subst (1 2) OclNotEmpty_including[where X = "Set{}", simplified mtSet_def])
     apply(simp add: mtSet_defined[simplified mtSet_def])
    apply(metis (opaque_lifting, no_types) finite.emptyI mtSet_def mtSet_rep_set)
   apply(simp add: OclValid_def)
  apply(simp add: OclIncluding_def)
  apply(rule conjI)
   apply(subst (1 2) Abs_Set⇩b⇩a⇩s⇩e_inverse, simp add: bot_option_def null_option_def)
    apply(simp, metis OclValid_def foundation18')
   apply(simp)
 apply(simp add: mtSet_defined[simplified mtSet_def])
 (* *)
 apply(subgoal_tac "a τ = ⊥")
  prefer 2
  apply(simp add: OclValid_def valid_def bot_fun_def split: if_split_asm)
 apply(simp)
 apply(subst (1 2 3 4) cp_OclAnd,
       simp add: mtSet_defined[simplified mtSet_def] valid_def bot_fun_def)
by(simp add: cp_OclAnd[symmetric], rule impI, simp add: false_def true_def)

subsubsection‹Execution Rules on Forall›

lemma OclForall_mtSet_exec[simp,code_unfold] :"((Set{})->forAll⇩S⇩e⇩t(z| P(z))) = true"
apply(simp add: OclForall_def)
apply(subst mtSet_def)+
apply(subst Abs_Set⇩b⇩a⇩s⇩e_inverse, simp_all add: true_def)+
done


text‹The following rule is a main theorem of our approach: From a denotational definition
that assures consistency, but may be --- as in the case of the @{term "X->forAll⇩S⇩e⇩t(x | P x)"} ---
dauntingly complex, we derive operational rules that can serve as a gold-standard for operational
execution, since they may be evaluated in whatever situation and according to whatever strategy.
In the case of @{term "X->forAll⇩S⇩e⇩t(x | P x)"}, the operational rule gives immediately a way to
evaluation in any finite (in terms of conventional OCL: denotable) set, although the rule also
holds for the infinite case:

@{term "Integer⇩n⇩u⇩l⇩l ->forAll⇩S⇩e⇩t(x | (Integer⇩n⇩u⇩l⇩l ->forAll⇩S⇩e⇩t(y | x +⇩i⇩n⇩t y ≜ y +⇩i⇩n⇩t x)))"}

or even:

@{term "Integer ->forAll⇩S⇩e⇩t(x | (Integer ->forAll⇩S⇩e⇩t(y | x +⇩i⇩n⇩t y ≐ y +⇩i⇩n⇩t x)))"}

are valid OCL statements in any context $\tau$.
›

theorem OclForall_including_exec[simp,code_unfold] :
        assumes cp0 : "cp P"
        shows         "((S->including⇩S⇩e⇩t(x))->forAll⇩S⇩e⇩t(z | P(z))) = (if δ S and υ x
                                                                then P x and (S->forAll⇩S⇩e⇩t(z | P(z)))
                                                                else invalid
                                                                endif)"
proof -
   have cp: "⋀τ. P x τ = P (λ_. x τ) τ" by(insert cp0, auto simp: cp_def)

   have cp_eq : "⋀τ v. (P x τ = v) = (P (λ_. x τ) τ = v)" by(subst cp, simp)

   have cp_OclNot_eq : "⋀τ v. (P x τ ≠ v) = (P (λ_. x τ) τ ≠ v)" by(subst cp, simp)

   have insert_in_Set⇩b⇩a⇩s⇩e : "⋀τ. (τ ⊨(δ S)) ⟹ (τ ⊨(υ x)) ⟹
                               ⌊⌊insert (x τ) ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (S τ)⌉⌉⌋⌋ ∈
                                 {X. X = bot ∨ X = null ∨ (∀x∈⌈⌈X⌉⌉. x ≠ bot)}"
           by(frule Set_inv_lemma, simp add: foundation18 invalid_def)

   have forall_including_invert : "⋀τ f. (f x τ = f (λ _. x τ) τ) ⟹
                                          τ ⊨ (δ S and υ x) ⟹
                                          (∀x∈⌈⌈Rep_Set⇩b⇩a⇩s⇩e (S->including⇩S⇩e⇩t(x) τ)⌉⌉. f (λ_. x) τ) =
                                            (f x τ ∧ (∀x∈⌈⌈Rep_Set⇩b⇩a⇩s⇩e (S τ)⌉⌉. f (λ_. x) τ))"
           apply(drule foundation5, simp add: OclIncluding_def)
           apply(subst Abs_Set⇩b⇩a⇩s⇩e_inverse)
           apply(rule insert_in_Set⇩b⇩a⇩s⇩e, fast+)
           by(simp add: OclValid_def)

   have exists_including_invert : "⋀τ f. (f x τ = f (λ _. x τ) τ) ⟹
                                          τ ⊨ (δ S and υ x) ⟹
                                          (∃x∈⌈⌈Rep_Set⇩b⇩a⇩s⇩e (S->including⇩S⇩e⇩t(x) τ)⌉⌉. f (λ_. x) τ) =
                                            (f x τ ∨ (∃x∈⌈⌈Rep_Set⇩b⇩a⇩s⇩e (S τ)⌉⌉. f (λ_. x) τ))"
           apply(subst arg_cong[where f = "λx. ¬x",
                                OF forall_including_invert[where f = "λx τ. ¬ (f x τ)"],
                                simplified])
           by simp_all

   have contradict_Rep_Set⇩b⇩a⇩s⇩e: "⋀τ S f. ∃x∈⌈⌈Rep_Set⇩b⇩a⇩s⇩e S⌉⌉. f (λ_. x) τ ⟹
                                       (∀x∈⌈⌈Rep_Set⇩b⇩a⇩s⇩e S⌉⌉. ¬ (f (λ_. x) τ)) = False"
           by(case_tac "(∀x∈⌈⌈Rep_Set⇩b⇩a⇩s⇩e S⌉⌉. ¬ (f (λ_. x) τ)) = True", simp_all)

   have bot_invalid : "⊥ = invalid"  by(rule ext, simp add: invalid_def bot_fun_def)

   have bot_invalid2 : "⋀τ. ⊥ = invalid τ"  by(simp add: invalid_def)

   have C1 : "⋀τ. P x τ = false τ ∨ (∃x∈⌈⌈Rep_Set⇩b⇩a⇩s⇩e (S τ)⌉⌉. P (λ_. x) τ = false τ) ⟹
                  τ ⊨ (δ S and υ x) ⟹
                  false τ = (P x and OclForall S P) τ"
           apply(simp add: cp_OclAnd[of "P x"])
           apply(elim disjE, simp)
            apply(simp only: cp_OclAnd[symmetric], simp)
           apply(subgoal_tac "OclForall S P τ = false τ")
            apply(simp only: cp_OclAnd[symmetric], simp)
           apply(simp add: OclForall_def)
           apply(fold OclValid_def, simp add:  foundation10')
           done

   have C2 : "⋀τ. τ ⊨ (δ S and υ x) ⟹
                  P x τ = null τ ∨ (∃x∈⌈⌈Rep_Set⇩b⇩a⇩s⇩e (S τ)⌉⌉. P (λ_. x) τ = null τ) ⟹
                  P x τ = invalid τ ∨ (∃x∈⌈⌈Rep_Set⇩b⇩a⇩s⇩e (S τ)⌉⌉. P (λ_. x) τ = invalid τ) ⟹
                  ∀x∈⌈⌈Rep_Set⇩b⇩a⇩s⇩e (S->including⇩S⇩e⇩t(x) τ)⌉⌉. P (λ_. x) τ ≠ false τ ⟹
                  invalid τ = (P x and OclForall S P) τ"
           apply(subgoal_tac "(δ S)τ = true τ")
            prefer 2 apply(simp add: foundation10', simp add: OclValid_def)
           apply(drule forall_including_invert[of "λ x τ. P x τ ≠ false τ", OF cp_OclNot_eq, THEN iffD1])
            apply(assumption)
           apply(simp add: cp_OclAnd[of "P x"],elim disjE, simp_all)
              apply(simp add: invalid_def null_fun_def null_option_def bot_fun_def bot_option_def)
             apply(subgoal_tac "OclForall S P τ = invalid τ")
              apply(simp only:cp_OclAnd[symmetric],simp,simp add:invalid_def bot_fun_def)
             apply(unfold OclForall_def, simp add: invalid_def false_def bot_fun_def,simp)
            apply(simp add:cp_OclAnd[symmetric],simp)
           apply(erule conjE)
           apply(subgoal_tac "(P x τ = invalid τ) ∨ (P x τ = null τ) ∨ (P x τ = true τ) ∨ (P x τ = false τ)")
            prefer 2 apply(rule bool_split_0)
           apply(elim disjE, simp_all)
            apply(simp only:cp_OclAnd[symmetric],simp)+
           done

   have A : "⋀τ. τ ⊨ (δ S and υ x) ⟹
                 OclForall (S->including⇩S⇩e⇩t(x)) P τ = (P x and OclForall S P) τ"
         proof - fix τ
                 assume 0 : "τ ⊨ (δ S and υ x)"
                 let ?S = "λocl. P x τ ≠ ocl τ ∧ (∀x∈⌈⌈Rep_Set⇩b⇩a⇩s⇩e (S τ)⌉⌉. P (λ_. x) τ ≠ ocl τ)"
                 let ?S' = "λocl. ∀x∈⌈⌈Rep_Set⇩b⇩a⇩s⇩e (S->including⇩S⇩e⇩t(x) τ)⌉⌉. P (λ_. x) τ ≠ ocl τ"
                 let ?assms_1 = "?S' null"
                 let ?assms_2 = "?S' invalid"
                 let ?assms_3 = "?S' false"
                 have 4 : "?assms_3 ⟹ ?S false"
                     apply(subst  forall_including_invert[of "λ x τ. P x τ ≠ false τ",symmetric])
                     by(simp_all add: cp_OclNot_eq 0)
                 have 5 : "?assms_2 ⟹ ?S invalid"
                     apply(subst  forall_including_invert[of "λ x τ. P x τ ≠ invalid τ",symmetric])
                     by(simp_all add: cp_OclNot_eq 0)
                 have 6 : "?assms_1 ⟹ ?S null"
                     apply(subst forall_including_invert[of "λ x τ. P x τ ≠ null τ",symmetric])
                     by(simp_all add: cp_OclNot_eq 0)
                 have 7 : "(δ S) τ = true τ"
                     by(insert 0, simp add: foundation10', simp add: OclValid_def)
         show "?thesis τ"
           apply(subst OclForall_def)
           apply(simp add: cp_OclAnd[THEN sym] OclValid_def contradict_Rep_Set⇩b⇩a⇩s⇩e)
           apply(intro conjI impI,fold OclValid_def)
           apply(simp_all add: exists_including_invert[where f = "λ x τ. P x τ = null τ", OF cp_eq])
           apply(simp_all add: exists_including_invert[where f = "λ x τ. P x τ = invalid τ", OF cp_eq])
           apply(simp_all add: exists_including_invert[where f = "λ x τ. P x τ = false τ", OF cp_eq])
           proof -
              assume 1 : "P x τ = null τ ∨ (∃x∈⌈⌈Rep_Set⇩b⇩a⇩s⇩e (S τ)⌉⌉. P (λ_. x) τ = null τ)"
              and    2 : ?assms_2
              and    3 : ?assms_3
              show   "null τ = (P x and OclForall S P) τ"
              proof -
                 note 4 = 4[OF 3]
                 note 5 = 5[OF 2]
                 have 6 : "P x τ = null τ ∨ P x τ = true τ"
                     by(metis 4 5 bool_split_0)
                 show ?thesis
                 apply(insert 6, elim disjE)
                  apply(subst cp_OclAnd)
                  apply(simp add: OclForall_def 7 4[THEN conjunct2] 5[THEN conjunct2])
                  apply(simp_all add:cp_OclAnd[symmetric])
                 apply(subst cp_OclAnd, simp_all add:cp_OclAnd[symmetric] OclForall_def)
                 apply(simp add:4[THEN conjunct2] 5[THEN conjunct2] 0[simplified OclValid_def] 7)
                 apply(insert 1, elim disjE, auto)
                 done
              qed
           next
              assume 1 : ?assms_1
              and    2 : "P x τ = invalid τ ∨ (∃x∈⌈⌈Rep_Set⇩b⇩a⇩s⇩e (S τ)⌉⌉. P (λ_. x) τ = invalid τ)"
              and    3 : ?assms_3
              show   "invalid τ = (P x and OclForall S P) τ"
              proof -
                 note 4 = 4[OF 3]
                 note 6 = 6[OF 1]
                 have 5 : "P x τ = invalid τ ∨ P x τ = true τ"
                     by(metis 4 6 bool_split_0)
                 show ?thesis
                 apply(insert 5, elim disjE)
                  apply(subst cp_OclAnd)
                  apply(simp add: OclForall_def 4[THEN conjunct2] 6[THEN conjunct2] 7)
                  apply(simp_all add:cp_OclAnd[symmetric])
                 apply(subst cp_OclAnd, simp_all add:cp_OclAnd[symmetric] OclForall_def)
                 apply(insert 2, elim disjE, simp add: invalid_def true_def bot_option_def)
                 apply(simp add: 0[simplified OclValid_def] 4[THEN conjunct2] 6[THEN conjunct2] 7)
                 by(auto)
               qed
           next
              assume 1 : ?assms_1
              and    2 : ?assms_2
              and    3 : ?assms_3
              show   "true τ = (P x and OclForall S P) τ"
              proof -
                 note 4 = 4[OF 3]
                 note 5 = 5[OF 2]
                 note 6 = 6[OF 1]
                 have 8 : "P x τ = true τ"
                     by(metis 4 5 6 bool_split_0)
                 show ?thesis
                 apply(subst cp_OclAnd, simp add: 8 cp_OclAnd[symmetric])
                 by(simp add: OclForall_def 4 5 6 7)
              qed
           qed ( simp add: 0
               | rule C1, simp+
               | rule C2, simp add: 0 )+
        qed

   have B : "⋀τ. ¬ (τ ⊨ (δ S and υ x)) ⟹
                 OclForall (S->including⇩S⇩e⇩t(x)) P τ = invalid τ"
           apply(rule foundation22[THEN iffD1])
           apply(simp only: foundation10' de_Morgan_conj foundation18'', elim disjE)
            apply(simp add:  defined_split, elim disjE)
             apply(erule StrongEq_L_subst2_rev, simp+)+
           done

   show ?thesis
           apply(rule ext, rename_tac τ)
           apply(simp add: OclIf_def)
           apply(simp add: cp_defined[of "δ S and υ x"] cp_defined[THEN sym])
           apply(intro conjI impI)
           by(auto intro!: A B simp: OclValid_def)
qed




subsubsection‹Execution Rules on Exists›

lemma OclExists_mtSet_exec[simp,code_unfold] :
"((Set{})->exists⇩S⇩e⇩t(z | P(z))) = false"
by(simp add: OclExists_def)

lemma OclExists_including_exec[simp,code_unfold] :
 assumes cp: "cp P"
 shows "((S->including⇩S⇩e⇩t(x))->exists⇩S⇩e⇩t(z | P(z))) = (if δ S and υ x
                                                 then P x or (S->exists⇩S⇩e⇩t(z | P(z)))
                                                 else invalid
                                                 endif)"
 by(simp add: OclExists_def OclOr_def  cp OclNot_inject)


subsubsection‹Execution Rules on Iterate›

lemma OclIterate_empty[simp,code_unfold]: "((Set{})->iterate⇩S⇩e⇩t(a; x = A | P a x)) = A"
proof -
 have C : "⋀ τ. (δ (λτ. Abs_Set⇩b⇩a⇩s⇩e ⌊⌊{}⌋⌋)) τ = true τ"
 by (metis (no_types) defined_def mtSet_def mtSet_defined null_fun_def)
 show ?thesis
      apply(simp add: OclIterate_def mtSet_def Abs_Set⇩b⇩a⇩s⇩e_inverse valid_def C)
      apply(rule ext, rename_tac τ)
      apply(case_tac "A τ = ⊥ τ", simp_all, simp add:true_def false_def bot_fun_def)
      apply(simp add: Abs_Set⇩b⇩a⇩s⇩e_inverse)
 done
qed

text‹In particular, this does hold for A = null.›

lemma OclIterate_including:
assumes S_finite:    "τ ⊨ δ(S->size⇩S⇩e⇩t())"
and     F_valid_arg: "(υ A) τ = (υ (F a A)) τ"
and     F_commute:   "comp_fun_commute F"
and     F_cp:        "⋀ x y τ. F x y τ = F (λ _. x τ) y τ"
shows   "((S->including⇩S⇩e⇩t(a))->iterate⇩S⇩e⇩t(a; x =     A | F a x)) τ =
         ((S->excluding⇩S⇩e⇩t(a))->iterate⇩S⇩e⇩t(a; x = F a A | F a x)) τ"
proof -
 have insert_in_Set⇩b⇩a⇩s⇩e : "⋀τ. (τ ⊨(δ S)) ⟹ (τ ⊨(υ a)) ⟹
    ⌊⌊insert (a τ) ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (S τ)⌉⌉⌋⌋ ∈ {X. X = bot ∨ X = null ∨ (∀x∈⌈⌈X⌉⌉. x ≠ bot)}"
  by(frule Set_inv_lemma, simp add: foundation18 invalid_def)

 have insert_defined : "⋀τ. (τ ⊨(δ S)) ⟹ (τ ⊨(υ a)) ⟹
            (δ (λ_. Abs_Set⇩b⇩a⇩s⇩e ⌊⌊insert (a τ) ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (S τ)⌉⌉⌋⌋)) τ = true τ"
  apply(subst defined_def)
  apply(simp add: bot_Set⇩b⇩a⇩s⇩e_def bot_fun_def null_Set⇩b⇩a⇩s⇩e_def null_fun_def)
  by(subst Abs_Set⇩b⇩a⇩s⇩e_inject,
     rule insert_in_Set⇩b⇩a⇩s⇩e, simp_all add: null_option_def bot_option_def)+

 have remove_finite : "finite ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (S τ)⌉⌉ ⟹
                       finite ((λa τ. a) ` (⌈⌈Rep_Set⇩b⇩a⇩s⇩e (S τ)⌉⌉ - {a τ}))"
 by(simp)

 have remove_in_Set⇩b⇩a⇩s⇩e : "⋀τ. (τ ⊨(δ S)) ⟹ (τ ⊨(υ a)) ⟹
   ⌊⌊⌈⌈Rep_Set⇩b⇩a⇩s⇩e (S τ)⌉⌉ - {a τ}⌋⌋ ∈ {X. X = bot ∨ X = null ∨ (∀x∈⌈⌈X⌉⌉. x ≠ bot)}"
 by(frule Set_inv_lemma, simp add: foundation18 invalid_def)

 have remove_defined : "⋀τ. (τ ⊨(δ S)) ⟹ (τ ⊨(υ a)) ⟹
            (δ (λ_. Abs_Set⇩b⇩a⇩s⇩e ⌊⌊⌈⌈Rep_Set⇩b⇩a⇩s⇩e (S τ)⌉⌉ - {a τ}⌋⌋)) τ = true τ"
  apply(subst defined_def)
  apply(simp add: bot_Set⇩b⇩a⇩s⇩e_def bot_fun_def null_Set⇩b⇩a⇩s⇩e_def null_fun_def)
  by(subst Abs_Set⇩b⇩a⇩s⇩e_inject,
     rule remove_in_Set⇩b⇩a⇩s⇩e, simp_all add: null_option_def bot_option_def)+

 have abs_rep: "⋀x. ⌊⌊x⌋⌋ ∈ {X. X = bot ∨ X = null ∨ (∀x∈⌈⌈X⌉⌉. x ≠ bot)} ⟹
                    ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (Abs_Set⇩b⇩a⇩s⇩e ⌊⌊x⌋⌋)⌉⌉ = x"
 by(subst Abs_Set⇩b⇩a⇩s⇩e_inverse, simp_all)

 have inject : "inj (λa τ. a)"
 by(rule inj_fun, simp)

 interpret F_commute: comp_fun_commute "F"
   by (fact F_commute)
 show ?thesis
  apply(subst (1 2) cp_OclIterate, subst OclIncluding_def, subst OclExcluding_def)
  apply(case_tac "¬ ((δ S) τ = true τ ∧ (υ a) τ = true τ)", simp add: invalid_def)

   apply(subgoal_tac "OclIterate (λ_. ⊥) A F τ = OclIterate (λ_. ⊥) (F a A) F τ", simp)
    apply(rule conjI, blast+)
  apply(simp add: OclIterate_def defined_def bot_option_def bot_fun_def false_def true_def)

  apply(simp add: OclIterate_def)
  apply((subst abs_rep[OF insert_in_Set⇩b⇩a⇩s⇩e[simplified OclValid_def], of τ], simp_all)+,
        (subst abs_rep[OF remove_in_Set⇩b⇩a⇩s⇩e[simplified OclValid_def], of τ], simp_all)+,
        (subst insert_defined, simp_all add: OclValid_def)+,
        (subst remove_defined, simp_all add: OclValid_def)+)

  apply(case_tac "¬ ((υ A) τ = true τ)", (simp add: F_valid_arg)+)
  apply(rule impI,
        subst F_commute.fold_fun_left_comm[symmetric],
        rule remove_finite, simp)

  apply(subst image_set_diff[OF inject], simp)
  apply(subgoal_tac "Finite_Set.fold F A (insert (λτ'. a τ) ((λa τ. a) ` ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (S τ)⌉⌉)) τ =
      F (λτ'. a τ) (Finite_Set.fold F A ((λa τ. a) ` ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (S τ)⌉⌉ - {λτ'. a τ})) τ")
   apply(subst F_cp, simp)

 by(subst F_commute.fold_insert_remove, simp+)
qed

subsubsection‹Execution Rules on Select›

lemma OclSelect_mtSet_exec[simp,code_unfold]: "OclSelect mtSet P = mtSet"
 apply(rule ext, rename_tac τ)
 apply(simp add: OclSelect_def mtSet_def defined_def false_def true_def
                 bot_Set⇩b⇩a⇩s⇩e_def bot_fun_def null_Set⇩b⇩a⇩s⇩e_def null_fun_def)
by(( subst (1 2 3 4 5) Abs_Set⇩b⇩a⇩s⇩e_inverse
   | subst Abs_Set⇩b⇩a⇩s⇩e_inject), (simp add: null_option_def bot_option_def)+)+

definition "OclSelect_body :: _ ⇒ _ ⇒ _ ⇒ ('𝔄, 'a option option) Set
           ≡ (λP x acc. if P x ≐ false then acc else acc->including⇩S⇩e⇩t(x) endif)"

theorem OclSelect_including_exec[simp,code_unfold]:
 assumes P_cp : "cp P"
 shows "OclSelect (X->including⇩S⇩e⇩t(y)) P = OclSelect_body P y (OclSelect (X->excluding⇩S⇩e⇩t(y)) P)"
 (is "_ = ?select")
proof -
 have P_cp: "⋀x τ. P x τ = P (λ_. x τ) τ" by(insert P_cp, auto simp: cp_def)

 have ex_including : "⋀f X y τ. τ ⊨ δ X ⟹ τ ⊨ υ y ⟹
                                   (∃x∈⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X->including⇩S⇩e⇩t(y) τ)⌉⌉. f (P (λ_. x)) τ) =
                                   (f (P (λ_. y τ)) τ ∨ (∃x∈⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X τ)⌉⌉. f (P (λ_. x)) τ))"
      apply(simp add: OclIncluding_def OclValid_def)
       apply(subst Abs_Set⇩b⇩a⇩s⇩e_inverse, simp, (rule disjI2)+)
      by (metis (opaque_lifting, no_types) OclValid_def Set_inv_lemma foundation18',simp)

 have al_including : "⋀f X y τ. τ ⊨ δ X ⟹ τ ⊨ υ y ⟹
                                   (∀x∈⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X->including⇩S⇩e⇩t(y) τ)⌉⌉. f (P (λ_. x)) τ) =
                                   (f (P (λ_. y τ)) τ ∧ (∀x∈⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X τ)⌉⌉. f (P (λ_. x)) τ))"
      apply(simp add: OclIncluding_def OclValid_def)
       apply(subst Abs_Set⇩b⇩a⇩s⇩e_inverse, simp, (rule disjI2)+)
      by (metis (opaque_lifting, no_types) OclValid_def Set_inv_lemma foundation18', simp)

 have ex_excluding1 : "⋀f X y τ. τ ⊨ δ X ⟹ τ ⊨ υ y ⟹ ¬ (f (P (λ_. y τ)) τ) ⟹
                                   (∃x∈⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X τ)⌉⌉. f (P (λ_. x)) τ) =
                                   (∃x∈⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X->excluding⇩S⇩e⇩t(y) τ)⌉⌉. f (P (λ_. x)) τ)"
      apply(simp add: OclExcluding_def OclValid_def)
       apply(subst Abs_Set⇩b⇩a⇩s⇩e_inverse, simp, (rule disjI2)+)
      by (metis (no_types) Diff_iff OclValid_def Set_inv_lemma) auto

 have al_excluding1 : "⋀f X y τ. τ ⊨ δ X ⟹ τ ⊨ υ y ⟹ f (P (λ_. y τ)) τ ⟹
                                   (∀x∈⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X τ)⌉⌉. f (P (λ_. x)) τ) =
                                   (∀x∈⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X->excluding⇩S⇩e⇩t(y) τ)⌉⌉. f (P (λ_. x)) τ)"
      apply(simp add: OclExcluding_def OclValid_def)
      apply(subst Abs_Set⇩b⇩a⇩s⇩e_inverse, simp, (rule disjI2)+)
      by (metis (no_types) Diff_iff OclValid_def Set_inv_lemma) auto

 have in_including : "⋀f X y τ. τ ⊨ δ X ⟹ τ ⊨ υ y ⟹
                                  {x ∈ ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X->including⇩S⇩e⇩t(y) τ)⌉⌉. f (P (λ_. x) τ)} =
                                   (let s = {x ∈ ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X τ)⌉⌉. f (P (λ_. x) τ)} in
                                    if f (P (λ_. y τ) τ) then insert (y τ) s else s)"
      apply(simp add: OclIncluding_def OclValid_def)
      apply(subst Abs_Set⇩b⇩a⇩s⇩e_inverse, simp, (rule disjI2)+)
       apply (metis (opaque_lifting, no_types) OclValid_def Set_inv_lemma foundation18')
      by(simp add: Let_def, auto)

 let ?OclSet = "λS. ⌊⌊S⌋⌋ ∈ {X. X = ⊥ ∨ X = null ∨ (∀x∈⌈⌈X⌉⌉. x ≠ ⊥)}"

 have diff_in_Set⇩b⇩a⇩s⇩e : "⋀τ. (δ X) τ = true τ ⟹ ?OclSet (⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X τ)⌉⌉ - {y τ})"
      apply(simp, (rule disjI2)+)
      by (metis (mono_tags) Diff_iff OclValid_def Set_inv_lemma)

 have ins_in_Set⇩b⇩a⇩s⇩e : "⋀τ. (δ X) τ = true τ ⟹ (υ y) τ = true τ ⟹
                           ?OclSet (insert (y τ) {x ∈ ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X τ)⌉⌉. P (λ_. x) τ ≠ false τ})"
      apply(simp, (rule disjI2)+)
      by (metis (opaque_lifting, no_types) OclValid_def Set_inv_lemma foundation18')

 have ins_in_Set⇩b⇩a⇩s⇩e' : "⋀τ. (δ X) τ = true τ ⟹ (υ y) τ = true τ ⟹
        ?OclSet (insert (y τ) {x ∈ ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X τ)⌉⌉. x ≠ y τ ∧ P (λ_. x) τ ≠ false τ})"
      apply(simp, (rule disjI2)+)
      by (metis (opaque_lifting, no_types) OclValid_def Set_inv_lemma foundation18')

 have ins_in_Set⇩b⇩a⇩s⇩e'' : "⋀τ. (δ X) τ = true τ ⟹
        ?OclSet {x ∈ ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X τ)⌉⌉. P (λ_. x) τ ≠ false τ}"
      apply(simp, (rule disjI2)+)
      by (metis (opaque_lifting, no_types) OclValid_def Set_inv_lemma)

 have ins_in_Set⇩b⇩a⇩s⇩e''' : "⋀τ. (δ X) τ = true τ ⟹
        ?OclSet {x ∈ ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X τ)⌉⌉. x ≠ y τ ∧ P (λ_. x) τ ≠ false τ}"
      apply(simp, (rule disjI2)+)
      by(metis (opaque_lifting, no_types) OclValid_def Set_inv_lemma)

 have if_same : "⋀a b c d τ. τ ⊨ δ a ⟹ b τ = d τ ⟹ c τ = d τ ⟹
                             (if a then b else c endif) τ = d τ"
      by(simp add: OclIf_def OclValid_def)

 have invert_including : "⋀P y τ. P τ = ⊥ ⟹ P->including⇩S⇩e⇩t(y) τ = ⊥"
      by (metis (opaque_lifting, no_types) foundation16[THEN iffD1]
                foundation18' OclIncluding_valid_args_valid)

 have exclude_defined : "⋀τ. τ ⊨ δ X ⟹
           (δ(λ_. Abs_Set⇩b⇩a⇩s⇩e ⌊⌊{x∈⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X τ)⌉⌉. x ≠ y τ ∧ P (λ_. x) τ≠false τ}⌋⌋)) τ = true τ"
      apply(subst defined_def,
            simp add: false_def true_def bot_Set⇩b⇩a⇩s⇩e_def bot_fun_def null_Set⇩b⇩a⇩s⇩e_def null_fun_def)
      by(subst Abs_Set⇩b⇩a⇩s⇩e_inject[OF ins_in_Set⇩b⇩a⇩s⇩e'''[simplified false_def]],
         (simp add: OclValid_def bot_option_def null_option_def)+)+

 have if_eq : "⋀x A B τ. τ ⊨ υ x ⟹ τ ⊨ ((if x ≐ false then A else B endif) ≜
                                          (if x ≜ false then A else B endif))"
      apply(simp add: StrictRefEq⇩B⇩o⇩o⇩l⇩e⇩a⇩n OclValid_def)
      apply(subst (2) StrongEq_def)
      by(subst cp_OclIf, simp add: cp_OclIf[symmetric] true_def)

 have OclSelect_body_bot: "⋀τ. τ ⊨ δ X ⟹ τ ⊨ υ y ⟹ P y τ ≠ ⊥ ⟹
                               (∃x∈⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X τ)⌉⌉. P (λ_. x) τ = ⊥) ⟹ ⊥ = ?select τ"
      apply(drule ex_excluding1[where X2 = X and y2 = y and f2 = "λx τ. x τ = ⊥"],
            (simp add: P_cp[symmetric])+)
      apply(subgoal_tac "τ ⊨ (⊥ ≜ ?select)", simp add: OclValid_def StrongEq_def true_def bot_fun_def)
      apply(simp add: OclSelect_body_def)
      apply(subst StrongEq_L_subst3[OF _ if_eq], simp, metis foundation18')
      apply(simp add: OclValid_def, subst StrongEq_def, subst true_def, simp)
      apply(subgoal_tac "∃x∈⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X->excluding⇩S⇩e⇩t(y) τ)⌉⌉. P (λ_. x) τ = ⊥ τ")
       prefer 2 apply (metis bot_fun_def )
       apply(subst if_same[where d5 = "⊥"])
        apply (metis defined7 transform1)
       apply(simp add: OclSelect_def bot_option_def bot_fun_def invalid_def)
      apply(subst invert_including)
      by(simp add: OclSelect_def bot_option_def bot_fun_def invalid_def)+


 have d_and_v_inject : "⋀τ X y. (δ X and υ y) τ ≠ true τ ⟹ (δ X and υ y) τ = false τ"
      apply(fold OclValid_def, subst foundation22[symmetric])
      apply(auto simp:foundation10'  defined_split)
        apply(erule StrongEq_L_subst2_rev,simp,simp)
       apply(erule StrongEq_L_subst2_rev,simp,simp)
      by(erule foundation7'[THEN iffD2, THEN foundation15[THEN iffD2,
                                       THEN StrongEq_L_subst2_rev]],simp,simp)




 have OclSelect_body_bot': "⋀τ. (δ X and υ y) τ ≠ true τ ⟹ ⊥ = ?select τ"
      apply(drule d_and_v_inject)
      apply(simp add: OclSelect_def OclSelect_body_def)
      apply(subst cp_OclIf, subst OclIncluding.cp0, simp add: false_def true_def)
      apply(subst cp_OclIf[symmetric], subst OclIncluding.cp0[symmetric])
      by (metis (lifting, no_types) OclIf_def foundation18 foundation18' invert_including)

 have conj_split2 : "⋀a b c τ. ((a ≜ false) τ = false τ ⟶ b) ∧ ((a ≜ false) τ = true τ ⟶ c) ⟹
                               (a τ ≠ false τ ⟶ b) ∧ (a τ = false τ ⟶ c)"
      by (metis OclValid_def defined7 foundation14 foundation22 foundation9)

 have defined_inject_true : "⋀τ P. (δ P) τ ≠ true τ ⟹ (δ P) τ = false τ"
      apply(simp add: defined_def true_def false_def bot_fun_def bot_option_def
                      null_fun_def null_option_def)
      by (case_tac " P τ = ⊥ ∨ P τ = null", simp_all add: true_def)

 have cp_OclSelect_body : "⋀τ. ?select τ = OclSelect_body P y (λ_.(OclSelect (X->excluding⇩S⇩e⇩t(y))P)τ)τ"
      apply(simp add: OclSelect_body_def)
      by(subst (1 2) cp_OclIf, subst (1 2) OclIncluding.cp0, blast)

 have OclSelect_body_strict1 : "OclSelect_body P y invalid = invalid"
      by(rule ext, simp add: OclSelect_body_def OclIf_def)

 have bool_invalid: "⋀(x::('𝔄)Boolean) y τ. ¬ (τ ⊨ υ x) ⟹ τ ⊨ ((x ≐ y) ≜ invalid)"
      by(simp add: StrictRefEq⇩B⇩o⇩o⇩l⇩e⇩a⇩n OclValid_def StrongEq_def true_def)

 have conj_comm : "⋀p q r. (p ∧ q ∧ r) = ((p ∧ q) ∧ r)" by blast

 have inv_bot : "⋀τ. invalid τ = ⊥ τ" by (metis bot_fun_def invalid_def)
 have inv_bot' : "⋀τ. invalid τ = ⊥" by (simp add: invalid_def)

 show ?thesis
  apply(rule ext, rename_tac τ)
  apply(subst OclSelect_def)
  apply(case_tac "(δ (X->including⇩S⇩e⇩t(y))) τ = true τ", simp)
   apply(( subst ex_including | subst in_including),
         metis OclValid_def foundation5,
         metis OclValid_def foundation5)+
   apply(simp add: Let_def inv_bot)
   apply(subst (2 4 7 9) bot_fun_def)

   apply(subst (4) false_def, subst (4) bot_fun_def, simp add: bot_option_def P_cp[symmetric])
   (* *)
   apply(case_tac "¬ (τ ⊨ (υ P y))")
    apply(subgoal_tac "P y τ ≠ false τ")
     prefer 2
     apply (metis (opaque_lifting, no_types) foundation1 foundation18' valid4)
    apply(simp)
    (* *)
    apply(subst conj_comm, rule conjI)
     apply(drule_tac y11 = false in bool_invalid)
     apply(simp only: OclSelect_body_def,
           metis OclIf_def OclValid_def defined_def foundation2 foundation22
                 bot_fun_def invalid_def)
    (* *)
    apply(drule foundation5[simplified OclValid_def],
          subst al_including[simplified OclValid_def],
          simp,
          simp)
    apply(simp add: P_cp[symmetric])
    apply (metis bot_fun_def foundation18')

   apply(simp add: foundation18' bot_fun_def OclSelect_body_bot OclSelect_body_bot')
   (* *)
   apply(subst (1 2) al_including, metis OclValid_def foundation5, metis OclValid_def foundation5)
   apply(simp add: P_cp[symmetric], subst (4) false_def, subst (4) bot_option_def, simp)

   apply(simp add: OclSelect_def[simplified inv_bot'] OclSelect_body_def StrictRefEq⇩B⇩o⇩o⇩l⇩e⇩a⇩n)
   apply(subst (1 2 3 4) cp_OclIf,
         subst (1 2 3 4) foundation18'[THEN iffD2, simplified OclValid_def],
         simp,
         simp only: cp_OclIf[symmetric] refl if_True)
   apply(subst (1 2) OclIncluding.cp0, rule conj_split2, simp add: cp_OclIf[symmetric])
   apply(subst (1 2 3 4 5 6 7 8) cp_OclIf[symmetric], simp)
   apply(( subst ex_excluding1[symmetric]
         | subst al_excluding1[symmetric] ),
         metis OclValid_def foundation5,
         metis OclValid_def foundation5,
         simp add: P_cp[symmetric] bot_fun_def)+
   apply(simp add: bot_fun_def)
   apply(subst (1 2) invert_including, simp+)
   (* *)
   apply(rule conjI, blast)
   apply(intro impI conjI)
    apply(subst OclExcluding_def)
    apply(drule foundation5[simplified OclValid_def], simp)
    apply(subst Abs_Set⇩b⇩a⇩s⇩e_inverse[OF diff_in_Set⇩b⇩a⇩s⇩e], fast)
    apply(simp add: OclIncluding_def cp_valid[symmetric])
    apply((erule conjE)+, frule exclude_defined[simplified OclValid_def], simp)
    apply(subst Abs_Set⇩b⇩a⇩s⇩e_inverse[OF ins_in_Set⇩b⇩a⇩s⇩e'''], simp+)
    apply(subst Abs_Set⇩b⇩a⇩s⇩e_inject[OF ins_in_Set⇩b⇩a⇩s⇩e ins_in_Set⇩b⇩a⇩s⇩e'], fast+)
   (* *)
   apply(simp add: OclExcluding_def)
   apply(simp add: foundation10[simplified OclValid_def])
   apply(subst Abs_Set⇩b⇩a⇩s⇩e_inverse[OF diff_in_Set⇩b⇩a⇩s⇩e], simp+)
   apply(subst Abs_Set⇩b⇩a⇩s⇩e_inject[OF ins_in_Set⇩b⇩a⇩s⇩e'' ins_in_Set⇩b⇩a⇩s⇩e'''], simp+)
   apply(subgoal_tac "P (λ_. y τ) τ = false τ")
    prefer 2
    apply(subst P_cp[symmetric], metis OclValid_def foundation22)
   apply(rule equalityI)
    apply(rule subsetI, simp, metis)
   apply(rule subsetI, simp)
  (* *)
  apply(drule defined_inject_true)
  apply(subgoal_tac "¬ (τ ⊨ δ X) ∨ ¬ (τ ⊨ υ y)")
   prefer 2
   apply (metis OclIncluding.def_homo OclIncluding_valid_args_valid OclIncluding_valid_args_valid'' OclValid_def foundation18 valid1)
  apply(subst cp_OclSelect_body, subst cp_OclSelect, subst OclExcluding_def)
  apply(simp add: OclValid_def false_def true_def, rule conjI, blast)
  apply(simp add: OclSelect_invalid[simplified invalid_def]
                  OclSelect_body_strict1[simplified invalid_def]
                  inv_bot')
 done
qed

subsubsection‹Execution Rules on Reject›

lemma OclReject_mtSet_exec[simp,code_unfold]: "OclReject mtSet P = mtSet"
by(simp add: OclReject_def)

lemma OclReject_including_exec[simp,code_unfold]:
 assumes P_cp : "cp P"
 shows "OclReject (X->including⇩S⇩e⇩t(y)) P = OclSelect_body (not o P) y (OclReject (X->excluding⇩S⇩e⇩t(y)) P)"
 apply(simp add: OclReject_def comp_def, rule OclSelect_including_exec)
by (metis  assms cp_intro'(5))

subsubsection‹Execution Rules Combining Previous Operators›

text‹OclIncluding›

(* logical level : *)
lemma OclIncluding_idem0 :
 assumes "τ ⊨ δ S"
     and "τ ⊨ υ i"
   shows "τ ⊨ (S->including⇩S⇩e⇩t(i)->including⇩S⇩e⇩t(i) ≜ (S->including⇩S⇩e⇩t(i)))"
by(simp add: OclIncluding_includes OclIncludes_charn1 assms)

(* Pure algebraic level *)
theorem OclIncluding_idem[simp,code_unfold]: "((S :: ('𝔄,'a::null)Set)->including⇩S⇩e⇩t(i)->including⇩S⇩e⇩t(i) = (S->including⇩S⇩e⇩t(i)))"
proof -
  have A: "⋀ τ.   τ ⊨ (i ≜ invalid)   ⟹ (S->including⇩S⇩e⇩t(i)->including⇩S⇩e⇩t(i)) τ = invalid τ"
            apply(rule foundation22[THEN iffD1])
            by(erule StrongEq_L_subst2_rev, simp,simp)
  have A':"⋀ τ.   τ ⊨ (i ≜ invalid)   ⟹ (S->including⇩S⇩e⇩t(i)) τ = invalid τ"
            apply(rule foundation22[THEN iffD1])
            by(erule StrongEq_L_subst2_rev, simp,simp)
  have C: "⋀ τ.   τ ⊨ (S ≜ invalid)   ⟹ (S->including⇩S⇩e⇩t(i)->including⇩S⇩e⇩t(i)) τ = invalid τ"
            apply(rule foundation22[THEN iffD1])
            by(erule StrongEq_L_subst2_rev, simp,simp)
  have C': "⋀ τ.  τ ⊨ (S ≜ invalid)   ⟹ (S->including⇩S⇩e⇩t(i)) τ = invalid τ"
            apply(rule foundation22[THEN iffD1])
            by(erule StrongEq_L_subst2_rev, simp,simp)
  have D: "⋀ τ.   τ ⊨ (S ≜ null)   ⟹ (S->including⇩S⇩e⇩t(i)->including⇩S⇩e⇩t(i)) τ = invalid τ"
            apply(rule foundation22[THEN iffD1])
            by(erule StrongEq_L_subst2_rev, simp,simp)
  have D': "⋀ τ.  τ ⊨ (S ≜ null)   ⟹ (S->including⇩S⇩e⇩t(i)) τ = invalid τ"
            apply(rule foundation22[THEN iffD1])
            by(erule StrongEq_L_subst2_rev, simp,simp)
  show ?thesis
    apply(rule ext, rename_tac τ)
    apply(case_tac "τ ⊨ (υ i)")
     apply(case_tac "τ ⊨ (δ S)")
      apply(simp only: OclIncluding_idem0[THEN foundation22[THEN iffD1]])
      apply(simp add: foundation16', elim disjE)
      apply(simp add: C[OF foundation22[THEN iffD2]] C'[OF foundation22[THEN iffD2]])
     apply(simp add: D[OF foundation22[THEN iffD2]] D'[OF foundation22[THEN iffD2]])
   apply(simp add:foundation18 A[OF foundation22[THEN iffD2]] A'[OF foundation22[THEN iffD2]])
  done
qed

text‹OclExcluding›

(* logical level : *)
lemma OclExcluding_idem0 :
 assumes "τ ⊨ δ S"
     and "τ ⊨ υ i"
   shows "τ ⊨ (S->excluding⇩S⇩e⇩t(i)->excluding⇩S⇩e⇩t(i) ≜ (S->excluding⇩S⇩e⇩t(i)))"
by(simp add: OclExcluding_excludes OclExcludes_charn1 assms)

(* Pure algebraic level *)
theorem OclExcluding_idem[simp,code_unfold]: "((S->excluding⇩S⇩e⇩t(i))->excluding⇩S⇩e⇩t(i)) = (S->excluding⇩S⇩e⇩t(i))"
proof -
  have A: "⋀ τ.   τ ⊨ (i ≜ invalid)   ⟹ (S->excluding⇩S⇩e⇩t(i)->excluding⇩S⇩e⇩t(i)) τ = invalid τ"
            apply(rule foundation22[THEN iffD1])
            by(erule StrongEq_L_subst2_rev, simp,simp)
  have A':"⋀ τ.   τ ⊨ (i ≜ invalid)   ⟹ (S->excluding⇩S⇩e⇩t(i)) τ = invalid τ"
            apply(rule foundation22[THEN iffD1])
            by(erule StrongEq_L_subst2_rev, simp,simp)
  have C: "⋀ τ.   τ ⊨ (S ≜ invalid)   ⟹ (S->excluding⇩S⇩e⇩t(i)->excluding⇩S⇩e⇩t(i)) τ = invalid τ"
            apply(rule foundation22[THEN iffD1])
            by(erule StrongEq_L_subst2_rev, simp,simp)
  have C': "⋀ τ.  τ ⊨ (S ≜ invalid)   ⟹ (S->excluding⇩S⇩e⇩t(i)) τ = invalid τ"
            apply(rule foundation22[THEN iffD1])
            by(erule StrongEq_L_subst2_rev, simp,simp)
  have D: "⋀ τ.   τ ⊨ (S ≜ null)   ⟹ (S->excluding⇩S⇩e⇩t(i)->excluding⇩S⇩e⇩t(i)) τ = invalid τ"
            apply(rule foundation22[THEN iffD1])
            by(erule StrongEq_L_subst2_rev, simp,simp)
  have D': "⋀ τ.  τ ⊨ (S ≜ null)   ⟹ (S->excluding⇩S⇩e⇩t(i)) τ = invalid τ"
            apply(rule foundation22[THEN iffD1])
            by(erule StrongEq_L_subst2_rev, simp,simp)
  show ?thesis
    apply(rule ext, rename_tac τ)
    apply(case_tac "τ ⊨ (υ i)")
     apply(case_tac "τ ⊨ (δ S)")
      apply(simp only: OclExcluding_idem0[THEN foundation22[THEN iffD1]])
      apply(simp add: foundation16', elim disjE)
      apply(simp add: C[OF foundation22[THEN iffD2]] C'[OF foundation22[THEN iffD2]])
     apply(simp add: D[OF foundation22[THEN iffD2]] D'[OF foundation22[THEN iffD2]])
   apply(simp add:foundation18 A[OF foundation22[THEN iffD2]] A'[OF foundation22[THEN iffD2]])
  done
qed

text‹OclIncludes›


lemma OclIncludes_any[simp,code_unfold]:
      "X->includes⇩S⇩e⇩t(X->any⇩S⇩e⇩t()) = (if δ X then
                                  if δ (X->size⇩S⇩e⇩t()) then not(X->isEmpty⇩S⇩e⇩t())
                                  else X->includes⇩S⇩e⇩t(null) endif
                                else invalid endif)"
proof -
 have defined_inject_true : "⋀τ P. (δ P) τ ≠ true τ ⟹ (δ P) τ = false τ"
      apply(simp add: defined_def true_def false_def bot_fun_def bot_option_def
                      null_fun_def null_option_def)
      by (case_tac " P τ = ⊥ ∨ P τ = null", simp_all add: true_def)

 have valid_inject_true : "⋀τ P. (υ P) τ ≠ true τ ⟹ (υ P) τ = false τ"
      apply(simp add: valid_def true_def false_def bot_fun_def bot_option_def
                      null_fun_def null_option_def)
      by (case_tac "P τ = ⊥", simp_all add: true_def)



 have notempty': "⋀τ X. τ ⊨ δ X ⟹ finite ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X τ)⌉⌉ ⟹ not (X->isEmpty⇩S⇩e⇩t()) τ ≠ true τ ⟹
                        X τ = Set{} τ"
  apply(case_tac "X τ", rename_tac X', simp add: mtSet_def Abs_Set⇩b⇩a⇩s⇩e_inject)
  apply(erule disjE, metis (opaque_lifting, mono_tags) bot_Set⇩b⇩a⇩s⇩e_def bot_option_def foundation16)
  apply(erule disjE, metis (opaque_lifting, no_types) bot_option_def
                                                 null_Set⇩b⇩a⇩s⇩e_def null_option_def foundation16[THEN iffD1])
  apply(case_tac X', simp, metis (opaque_lifting, no_types) bot_Set⇩b⇩a⇩s⇩e_def foundation16[THEN iffD1])
  apply(rename_tac X'', case_tac X'', simp)
   apply (metis (opaque_lifting, no_types) foundation16[THEN iffD1] null_Set⇩b⇩a⇩s⇩e_def)
  apply(simp add: OclIsEmpty_def OclSize_def)
  apply(subst (asm) cp_OclNot, subst (asm) cp_OclOr, subst (asm) StrictRefEq⇩I⇩n⇩t⇩e⇩g⇩e⇩r.cp0,
        subst (asm) cp_OclAnd, subst (asm) cp_OclNot)
  apply(simp only: OclValid_def foundation20[simplified OclValid_def]
                   cp_OclNot[symmetric] cp_OclAnd[symmetric] cp_OclOr[symmetric])
  apply(simp add: Abs_Set⇩b⇩a⇩s⇩e_inverse split: if_split_asm)
 by(simp add: true_def OclInt0_def OclNot_def StrictRefEq⇩I⇩n⇩t⇩e⇩g⇩e⇩r StrongEq_def)

 have B: "⋀X τ. ¬ finite ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X τ)⌉⌉ ⟹ (δ (X->size⇩S⇩e⇩t())) τ = false τ"
  apply(subst cp_defined)
  apply(simp add: OclSize_def)
 by (metis bot_fun_def defined_def)

 show ?thesis
  apply(rule ext, rename_tac τ, simp only: OclIncludes_def OclANY_def)
  apply(subst cp_OclIf, subst (2) cp_valid)
  apply(case_tac "(δ X) τ = true τ",
        simp only: foundation20[simplified OclValid_def] cp_OclIf[symmetric], simp,
        subst (1 2) cp_OclAnd, simp add: cp_OclAnd[symmetric])
   apply(case_tac "finite ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X τ)⌉⌉")
    apply(frule size_defined'[THEN iffD2, simplified OclValid_def], assumption)
    apply(subst (1 2 3 4) cp_OclIf, simp)
    apply(subst (1 2 3 4) cp_OclIf[symmetric], simp)
    apply(case_tac "(X->notEmpty⇩S⇩e⇩t()) τ = true τ", simp)
     apply(frule OclNotEmpty_has_elt[simplified OclValid_def], simp)
     apply(simp add: OclNotEmpty_def cp_OclIf[symmetric])
     apply(subgoal_tac "(SOME y. y ∈ ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X τ)⌉⌉) ∈ ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X τ)⌉⌉", simp add: true_def)
      apply(metis OclValid_def Set_inv_lemma foundation18' null_option_def true_def)
     apply(rule someI_ex, simp)
    apply(simp add: OclNotEmpty_def cp_valid[symmetric])
    apply(subgoal_tac "¬ (null τ ∈ ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X τ)⌉⌉)", simp)
     apply(subst OclIsEmpty_def, simp add: OclSize_def)
     apply(subst cp_OclNot, subst cp_OclOr, subst StrictRefEq⇩I⇩n⇩t⇩e⇩g⇩e⇩r.cp0, subst cp_OclAnd,
           subst cp_OclNot, simp add: OclValid_def foundation20[simplified OclValid_def]
                                      cp_OclNot[symmetric] cp_OclAnd[symmetric] cp_OclOr[symmetric])
     apply(frule notempty'[simplified OclValid_def],
           (simp add: mtSet_def Abs_Set⇩b⇩a⇩s⇩e_inverse OclInt0_def false_def)+)
    apply(drule notempty'[simplified OclValid_def], simp, simp)
    apply (metis (opaque_lifting, no_types) empty_iff mtSet_rep_set)
   (* *)
   apply(frule B)
   apply(subst (1 2 3 4) cp_OclIf, simp)
   apply(subst (1 2 3 4) cp_OclIf[symmetric], simp)
   apply(case_tac "(X->notEmpty⇩S⇩e⇩t()) τ = true τ", simp)
    apply(frule OclNotEmpty_has_elt[simplified OclValid_def], simp)
    apply(simp add: OclNotEmpty_def OclIsEmpty_def)
    apply(subgoal_tac "X->size⇩S⇩e⇩t() τ = ⊥")
     prefer 2
     apply (metis (opaque_lifting, no_types) OclSize_def)
    apply(subst (asm) cp_OclNot, subst (asm) cp_OclOr, subst (asm) StrictRefEq⇩I⇩n⇩t⇩e⇩g⇩e⇩r.cp0,
          subst (asm) cp_OclAnd, subst (asm) cp_OclNot)
    apply(simp add: OclValid_def foundation20[simplified OclValid_def]
                    cp_OclNot[symmetric] cp_OclAnd[symmetric] cp_OclOr[symmetric])
    apply(simp add: OclNot_def StrongEq_def StrictRefEq⇩I⇩n⇩t⇩e⇩g⇩e⇩r valid_def false_def true_def
                    bot_option_def bot_fun_def invalid_def)

   apply (metis bot_fun_def null_fun_def null_is_valid valid_def)
 by(drule defined_inject_true,
    simp add: false_def true_def OclIf_false[simplified false_def] invalid_def)
qed

text‹OclSize›

lemma [simp,code_unfold]: "δ (Set{} ->size⇩S⇩e⇩t()) = true"
by simp


lemma [simp,code_unfold]: "δ ((X ->including⇩S⇩e⇩t(x)) ->size⇩S⇩e⇩t()) = (δ(X->size⇩S⇩e⇩t()) and υ(x))"
proof -
 have defined_inject_true : "⋀τ P. (δ P) τ ≠ true τ ⟹ (δ P) τ = false τ"
      apply(simp add: defined_def true_def false_def bot_fun_def bot_option_def
                      null_fun_def null_option_def)
      by (case_tac " P τ = ⊥ ∨ P τ = null", simp_all add: true_def)

 have valid_inject_true : "⋀τ P. (υ P) τ ≠ true τ ⟹ (υ P) τ = false τ"
      apply(simp add: valid_def true_def false_def bot_fun_def bot_option_def
                      null_fun_def null_option_def)
      by (case_tac "P τ = ⊥", simp_all add: true_def)

 have OclIncluding_finite_rep_set : "⋀τ. (δ X and υ x) τ = true τ ⟹
                 finite ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X->including⇩S⇩e⇩t(x) τ)⌉⌉ = finite ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X τ)⌉⌉"
  apply(rule OclIncluding_finite_rep_set)
 by(metis OclValid_def foundation5)+

 have card_including_exec : "⋀τ. (δ (λ_. ⌊⌊int (card ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X->including⇩S⇩e⇩t(x) τ)⌉⌉)⌋⌋)) τ =
                                 (δ (λ_. ⌊⌊int (card ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X τ)⌉⌉)⌋⌋)) τ"
 by(simp add: defined_def bot_fun_def bot_option_def null_fun_def null_option_def)

 show ?thesis
  apply(rule ext, rename_tac τ)
  apply(case_tac "(δ (X->including⇩S⇩e⇩t(x)->size⇩S⇩e⇩t())) τ = true τ", simp del: OclSize_including_exec)
   apply(subst cp_OclAnd, subst cp_defined, simp only: cp_defined[of "X->including⇩S⇩e⇩t(x)->size⇩S⇩e⇩t()"],
         simp add: OclSize_def)
   apply(case_tac "((δ X and υ x) τ = true τ ∧ finite ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X->including⇩S⇩e⇩t(x) τ)⌉⌉)", simp)
    apply(erule conjE,
          simp add: OclIncluding_finite_rep_set[simplified OclValid_def] card_including_exec
                    cp_OclAnd[of "δ X" "υ x"]
                    cp_OclAnd[of "true", THEN sym])
    apply(subgoal_tac "(δ X) τ = true τ ∧ (υ x) τ = true τ", simp)
    apply(rule foundation5[of _ "δ X" "υ x", simplified OclValid_def],
          simp only: cp_OclAnd[THEN sym])
   apply(simp, simp add: defined_def true_def false_def bot_fun_def bot_option_def)

  apply(drule defined_inject_true[of "X->including⇩S⇩e⇩t(x)->size⇩S⇩e⇩t()"],
        simp del: OclSize_including_exec,
        simp only: cp_OclAnd[of "δ (X->size⇩S⇩e⇩t())" "υ x"],
        simp add: cp_defined[of "X->including⇩S⇩e⇩t(x)->size⇩S⇩e⇩t()" ] cp_defined[of "X->size⇩S⇩e⇩t()" ]
             del: OclSize_including_exec,
        simp add: OclSize_def card_including_exec
             del: OclSize_including_exec)
  apply(case_tac "(δ X and υ x) τ = true τ ∧ finite ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X τ)⌉⌉",
        simp add: OclIncluding_finite_rep_set[simplified OclValid_def] card_including_exec,
        simp only: cp_OclAnd[THEN sym],
        simp add: defined_def bot_fun_def)

  apply(split if_split_asm)
   apply(simp add: OclIncluding_finite_rep_set[simplified OclValid_def] card_including_exec)+
  apply(simp only: cp_OclAnd[THEN sym], simp, rule impI, erule conjE)
  apply(case_tac "(υ x) τ = true τ", simp add: cp_OclAnd[of "δ X" "υ x"])
 by(drule valid_inject_true[of "x"], simp add: cp_OclAnd[of _ "υ x"])
qed

lemma [simp,code_unfold]: "δ ((X ->excluding⇩S⇩e⇩t(x)) ->size⇩S⇩e⇩t()) = (δ(X->size⇩S⇩e⇩t()) and υ(x))"
proof -
 have defined_inject_true : "⋀τ P. (δ P) τ ≠ true τ ⟹ (δ P) τ = false τ"
      apply(simp add: defined_def true_def false_def bot_fun_def bot_option_def
                      null_fun_def null_option_def)
      by (case_tac " P τ = ⊥ ∨ P τ = null", simp_all add: true_def)

 have valid_inject_true : "⋀τ P. (υ P) τ ≠ true τ ⟹ (υ P) τ = false τ"
      apply(simp add: valid_def true_def false_def bot_fun_def bot_option_def
                      null_fun_def null_option_def)
      by (case_tac "P τ = ⊥", simp_all add: true_def)

 have OclExcluding_finite_rep_set : "⋀τ. (δ X and υ x) τ = true τ ⟹
                                     finite ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X->excluding⇩S⇩e⇩t(x) τ)⌉⌉ =
                                     finite ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X τ)⌉⌉"
  apply(rule OclExcluding_finite_rep_set)
 by(metis OclValid_def foundation5)+

 have card_excluding_exec : "⋀τ. (δ (λ_. ⌊⌊int (card ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X->excluding⇩S⇩e⇩t(x) τ)⌉⌉)⌋⌋)) τ =
                                   (δ (λ_. ⌊⌊int (card ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X τ)⌉⌉)⌋⌋)) τ"
 by(simp add: defined_def bot_fun_def bot_option_def null_fun_def null_option_def)

 show ?thesis
  apply(rule ext, rename_tac τ)
  apply(case_tac "(δ (X->excluding⇩S⇩e⇩t(x)->size⇩S⇩e⇩t())) τ = true τ", simp)
   apply(subst cp_OclAnd, subst cp_defined, simp only: cp_defined[of "X->excluding⇩S⇩e⇩t(x)->size⇩S⇩e⇩t()"],
         simp add: OclSize_def)
   apply(case_tac "((δ X and υ x) τ = true τ ∧ finite ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X->excluding⇩S⇩e⇩t(x) τ)⌉⌉)", simp)
    apply(erule conjE,
          simp add: OclExcluding_finite_rep_set[simplified OclValid_def] card_excluding_exec
                    cp_OclAnd[of "δ X" "υ x"]
                    cp_OclAnd[of "true", THEN sym])
    apply(subgoal_tac "(δ X) τ = true τ ∧ (υ x) τ = true τ", simp)
    apply(rule foundation5[of _ "δ X" "υ x", simplified OclValid_def],
          simp only: cp_OclAnd[THEN sym])
   apply(simp, simp add: defined_def true_def false_def bot_fun_def bot_option_def)

  apply(drule defined_inject_true[of "X->excluding⇩S⇩e⇩t(x)->size⇩S⇩e⇩t()"],
        simp,
        simp only: cp_OclAnd[of "δ (X->size⇩S⇩e⇩t())" "υ x"],
        simp add: cp_defined[of "X->excluding⇩S⇩e⇩t(x)->size⇩S⇩e⇩t()" ] cp_defined[of "X->size⇩S⇩e⇩t()" ],
        simp add: OclSize_def card_excluding_exec)
  apply(case_tac "(δ X and υ x) τ = true τ ∧ finite ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X τ)⌉⌉",
        simp add: OclExcluding_finite_rep_set[simplified OclValid_def] card_excluding_exec,
        simp only: cp_OclAnd[THEN sym],
        simp add: defined_def bot_fun_def)

  apply(split if_split_asm)
   apply(simp add: OclExcluding_finite_rep_set[simplified OclValid_def] card_excluding_exec)+
  apply(simp only: cp_OclAnd[THEN sym], simp, rule impI, erule conjE)
  apply(case_tac "(υ x) τ = true τ", simp add: cp_OclAnd[of "δ X" "υ x"])
 by(drule valid_inject_true[of "x"], simp add: cp_OclAnd[of _ "υ x"])
qed

lemma [simp]:
 assumes X_finite: "⋀τ. finite ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X τ)⌉⌉"
 shows "δ ((X ->including⇩S⇩e⇩t(x)) ->size⇩S⇩e⇩t()) = (δ(X) and υ(x))"
by(simp add: size_defined[OF X_finite] del: OclSize_including_exec)


text‹OclForall›

lemma OclForall_rep_set_false:
 assumes "τ ⊨ δ X"
 shows "(OclForall X P τ = false τ) = (∃x ∈ ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X τ)⌉⌉. P (λτ. x) τ = false τ)"
by(insert assms, simp add: OclForall_def OclValid_def false_def true_def invalid_def
                           bot_fun_def bot_option_def null_fun_def null_option_def)

lemma OclForall_rep_set_true:
 assumes "τ ⊨ δ X"
 shows "(τ ⊨ OclForall X P) = (∀x ∈ ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X τ)⌉⌉. τ ⊨ P (λτ. x))"
proof -
 have destruct_ocl : "⋀x τ. x = true τ ∨ x = false τ ∨ x = null τ ∨ x = ⊥ τ"
  apply(case_tac x) apply (metis bot_Boolean_def)
  apply(rename_tac x', case_tac x') apply (metis null_Boolean_def)
  apply(rename_tac x'', case_tac x'') apply (metis (full_types) true_def)
 by (metis (full_types) false_def)

 have disjE4 : "⋀ P1 P2 P3 P4 R.
   (P1 ∨ P2 ∨ P3 ∨ P4) ⟹ (P1 ⟹ R) ⟹ (P2 ⟹ R) ⟹ (P3 ⟹ R) ⟹ (P4 ⟹ R) ⟹ R"
 by metis
 show ?thesis
  apply(simp add: OclForall_def OclValid_def true_def false_def invalid_def
                  bot_fun_def bot_option_def null_fun_def null_option_def split: if_split_asm)
  apply(rule conjI, rule impI) apply (metis drop.simps option.distinct(1) invalid_def)
  apply(rule impI, rule conjI, rule impI) apply (metis option.distinct(1))
  apply(rule impI, rule conjI, rule impI) apply (metis drop.simps)
  apply(intro conjI impI ballI)
   proof - fix x show "∀x∈⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X τ)⌉⌉. P (λ_. x) τ ≠ ⌊None⌋ ⟹
                       ∀x∈⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X τ)⌉⌉. ∃y. P (λ_. x) τ = ⌊y⌋ ⟹
                       ∀x∈⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X τ)⌉⌉. P (λ_. x) τ ≠ ⌊⌊False⌋⌋ ⟹
                       x ∈ ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X τ)⌉⌉ ⟹ P (λτ. x) τ = ⌊⌊True⌋⌋"
   apply(erule_tac x = x in ballE)+
   by(rule disjE4[OF destruct_ocl[of "P (λτ. x) τ"]],
      (simp add: true_def false_def null_fun_def null_option_def bot_fun_def bot_option_def)+)
 qed(simp add: assms[simplified OclValid_def true_def])+
qed

lemma OclForall_includes :
 assumes x_def : "τ ⊨ δ x"
     and y_def : "τ ⊨ δ y"
   shows "(τ ⊨ OclForall x (OclIncludes y)) = (⌈⌈Rep_Set⇩b⇩a⇩s⇩e (x τ)⌉⌉ ⊆ ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (y τ)⌉⌉)"
 apply(simp add: OclForall_rep_set_true[OF x_def],
       simp add: OclIncludes_def OclValid_def y_def[simplified OclValid_def])
 apply(insert Set_inv_lemma[OF x_def], simp add: valid_def false_def true_def bot_fun_def)
by(rule iffI, simp add: subsetI, simp add: subsetD)

lemma OclForall_not_includes :
 assumes x_def : "τ ⊨ δ x"
     and y_def : "τ ⊨ δ y"
   shows "(OclForall x (OclIncludes y) τ = false τ) = (¬ ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (x τ)⌉⌉ ⊆ ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (y τ)⌉⌉)"
 apply(simp add: OclForall_rep_set_false[OF x_def],
       simp add: OclIncludes_def OclValid_def y_def[simplified OclValid_def])
 apply(insert Set_inv_lemma[OF x_def], simp add: valid_def false_def true_def bot_fun_def)
by(rule iffI, metis rev_subsetD, metis subsetI)

lemma OclForall_iterate:
 assumes S_finite: "finite ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (S τ)⌉⌉"
   shows "S->forAll⇩S⇩e⇩t(x | P x) τ = (S->iterate⇩S⇩e⇩t(x; acc = true | acc and P x)) τ"
proof -
 interpret and_comm: comp_fun_commute "(λx acc. acc and P x)"
  apply(simp add: comp_fun_commute_def comp_def)
  by (metis OclAnd_assoc OclAnd_commute)

 have ex_insert : "⋀x F P. (∃x∈insert x F. P x) = (P x ∨ (∃x∈F. P x))"
 by (metis insert_iff)

 have destruct_ocl : "⋀x τ. x = true τ ∨ x = false τ ∨ x = null τ ∨ x = ⊥ τ"
  apply(case_tac x) apply (metis bot_Boolean_def)
  apply(rename_tac x', case_tac x') apply (metis null_Boolean_def)
  apply(rename_tac x'', case_tac x'') apply (metis (full_types) true_def)
 by (metis (full_types) false_def)

 have disjE4 : "⋀ P1 P2 P3 P4 R.
   (P1 ∨ P2 ∨ P3 ∨ P4) ⟹ (P1 ⟹ R) ⟹ (P2 ⟹ R) ⟹ (P3 ⟹ R) ⟹ (P4 ⟹ R) ⟹ R"
 by metis

 let ?P_eq = "λx b τ. P (λ_. x) τ = b τ"
 let ?P = "λset b τ. ∃x∈set. ?P_eq x b τ"
 let ?if = "λf b c. if f b τ then b τ else c"
 let ?forall = "λP. ?if P false (?if P invalid (?if P null (true τ)))"
 show ?thesis
  apply(simp only: OclForall_def OclIterate_def)
  apply(case_tac "τ ⊨ δ S", simp only: OclValid_def)
   apply(subgoal_tac "let set = ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (S τ)⌉⌉ in
                      ?forall (?P set) =
                      Finite_Set.fold (λx acc. acc and P x) true ((λa τ. a) ` set) τ",
         simp only: Let_def, simp add: S_finite, simp only: Let_def)
   apply(case_tac "⌈⌈Rep_Set⇩b⇩a⇩s⇩e (S τ)⌉⌉ = {}", simp)
   apply(rule finite_ne_induct[OF S_finite], simp)
    (* *)
    apply(simp only: image_insert)
    apply(subst and_comm.fold_insert, simp)
     apply (metis empty_iff image_empty)
    apply(simp add: invalid_def)
    apply (metis bot_fun_def destruct_ocl null_fun_def)
   (* *)
   apply(simp only: image_insert)
   apply(subst and_comm.fold_insert, simp)
    apply (metis (mono_tags) imageE)

   (* *)
   apply(subst cp_OclAnd) apply(drule sym, drule sym, simp only:, drule sym, simp only:)
   apply(simp only: ex_insert)
   apply(subgoal_tac "∃x. x∈F") prefer 2
    apply(metis all_not_in_conv)
   proof - fix x F show "(δ S) τ = true τ ⟹ ∃x. x ∈ F ⟹
            ?forall (λb τ. ?P_eq x b τ ∨ ?P F b τ) =
            ((λ_. ?forall (?P F)) and (λ_. P (λτ. x) τ)) τ"
    apply(rule disjE4[OF destruct_ocl[where x1 = "P (λτ. x) τ"]])
       apply(simp_all add: true_def false_def invalid_def OclAnd_def
                           null_fun_def null_option_def bot_fun_def bot_option_def)
   by (metis (lifting) option.distinct(1))+
 qed(simp add: OclValid_def)+
qed

lemma OclForall_cong:
 assumes "⋀x. x ∈ ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X τ)⌉⌉ ⟹ τ ⊨ P (λτ. x) ⟹ τ ⊨ Q (λτ. x)"
 assumes P: "τ ⊨ OclForall X P"
 shows "τ ⊨ OclForall X Q"
proof -
 have def_X: "τ ⊨ δ X"
 by(insert P, simp add: OclForall_def OclValid_def bot_option_def true_def split: if_split_asm)
 show ?thesis
  apply(insert P)
  apply(subst (asm) OclForall_rep_set_true[OF def_X], subst OclForall_rep_set_true[OF def_X])
 by (simp add: assms)
qed

lemma OclForall_cong':
 assumes "⋀x. x ∈ ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (X τ)⌉⌉ ⟹ τ ⊨ P (λτ. x) ⟹ τ ⊨ Q (λτ. x) ⟹ τ ⊨ R (λτ. x)"
 assumes P: "τ ⊨ OclForall X P"
 assumes Q: "τ ⊨ OclForall X Q"
 shows "τ ⊨ OclForall X R"
proof -
 have def_X: "τ ⊨ δ X"
 by(insert P, simp add: OclForall_def OclValid_def bot_option_def true_def split: if_split_asm)
 show ?thesis
  apply(insert P Q)
  apply(subst (asm) (1 2) OclForall_rep_set_true[OF def_X], subst OclForall_rep_set_true[OF def_X])
 by (simp add: assms)
qed

text‹Strict Equality›

lemma StrictRefEq⇩S⇩e⇩t_defined :
 assumes x_def: "τ ⊨ δ x"
 assumes y_def: "τ ⊨ δ y"
 shows "((x::('𝔄,'α::null)Set) ≐ y) τ =
                (x->forAll⇩S⇩e⇩t(z| y->includes⇩S⇩e⇩t(z)) and (y->forAll⇩S⇩e⇩t(z| x->includes⇩S⇩e⇩t(z)))) τ"
proof -
 have rep_set_inj : "⋀τ. (δ x) τ = true τ ⟹
                         (δ y) τ = true τ ⟹
                          x τ ≠ y τ ⟹
                          ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (y τ)⌉⌉ ≠ ⌈⌈Rep_Set⇩b⇩a⇩s⇩e (x τ)⌉⌉"
  apply(simp add: defined_def)
  apply(split if_split_asm, simp add: false_def true_def)+
  apply(simp add: null_fun_def null_Set⇩b⇩a⇩s⇩e_def bot_fun_def bot_Set⇩b⇩a⇩s⇩e_def)

  apply(case_tac "x τ", rename_tac x')
  apply(case_tac x', simp_all, rename_tac x'')
  apply(case_tac x'', simp_all)

  apply(case_tac "y τ", rename_tac y')
  apply(case_tac y', simp_all, rename_tac y'')
  apply(case_tac y'', simp_all)

  apply(simp add: Abs_Set⇩b⇩a⇩s⇩e_inverse)
 by(blast)

 show ?thesis
  apply(simp add: StrictRefEq⇩S⇩e⇩t StrongEq_def
    foundation20[OF x_def, simplified OclValid_def]
    foundation20[OF y_def, simplified OclValid_def])
  apply(subgoal_tac "⌊⌊x τ = y τ⌋⌋ = true τ ∨ ⌊⌊x τ = y τ⌋⌋ = false τ")
   prefer 2
   apply(simp add: false_def true_def)
  (* *)
  apply(erule disjE)
   apply(simp add: true_def)

   apply(subgoal_tac "(τ ⊨ OclForall x (OclIncludes y)) ∧ (τ ⊨ OclForall y (OclIncludes x))")
    apply(subst cp_OclAnd, simp add: true_def OclValid_def)
   apply(simp add: OclForall_includes[OF x_def y_def]
                   OclForall_includes[OF y_def x_def])

  (* *)
  apply(simp)

  apply(subgoal_tac "OclForall x (OclIncludes y) τ = false τ ∨
                     OclForall y (OclIncludes x) τ = false τ")
   apply(subst cp_OclAnd, metis OclAnd_false1 OclAnd_false2 cp_OclAnd)
  apply(simp only: OclForall_not_includes[OF x_def y_def, simplified OclValid_def]
                   OclForall_not_includes[OF y_def x_def, simplified OclValid_def],
        simp add: false_def)
 by (metis OclValid_def rep_set_inj subset_antisym x_def y_def)
qed

lemma StrictRefEq⇩S⇩e⇩t_exec[simp,code_unfold] :
"((x::('𝔄,'α::null)Set) ≐ y) =
  (if δ x then (if δ y
                then ((x->forAll⇩S⇩e⇩t(z| y->includes⇩S⇩e⇩t(z)) and (y->forAll⇩S⇩e⇩t(z| x->includes⇩S⇩e⇩t(z)))))
                else if υ y
                      then false ― ‹‹x'->includes = null››
                      else invalid
                      endif
                endif)
         else if υ x ― ‹‹null = ???››
              then if υ y then not(δ y) else invalid endif
              else invalid
              endif
         endif)"
proof -
 have defined_inject_true : "⋀τ P. (¬ (τ ⊨ δ P)) = ((δ P) τ = false τ)"
 by (metis bot_fun_def OclValid_def defined_def foundation16 null_fun_def)

 have valid_inject_true : "⋀τ P. (¬ (τ ⊨ υ P)) = ((υ P) τ = false τ)"
 by (metis bot_fun_def OclIf_true' OclIncludes_charn0 OclIncludes_charn0' OclValid_def valid_def
           foundation6 foundation9)
 show ?thesis
  apply(rule ext, rename_tac τ)
  (* *)
  apply(simp add: OclIf_def
                  defined_inject_true[simplified OclValid_def]
                  valid_inject_true[simplified OclValid_def],
        subst false_def, subst true_def, simp)
  apply(subst (1 2) cp_OclNot, simp, simp add: cp_OclNot[symmetric])
  apply(simp add: StrictRefEq⇩S⇩e⇩t_defined[simplified OclValid_def])
 by(simp add: StrictRefEq⇩S⇩e⇩t StrongEq_def false_def true_def valid_def defined_def)
qed

lemma StrictRefEq⇩S⇩e⇩t_L_subst1 : "cp P ⟹ τ ⊨ υ x ⟹ τ ⊨ υ y ⟹ τ ⊨ υ P x ⟹ τ ⊨ υ P y ⟹
    τ ⊨ (x::('𝔄,'α::null)Set) ≐ y ⟹ τ ⊨ (P x ::('𝔄,'α::null)Set) ≐ P y"
 apply(simp only: StrictRefEq⇩S⇩e⇩t OclValid_def)
 apply(split if_split_asm)
  apply(simp add: StrongEq_L_subst1[simplified OclValid_def])
by (simp add: invalid_def bot_option_def true_def)

lemma OclIncluding_cong' :
shows "τ ⊨ δ s ⟹ τ ⊨ δ t ⟹ τ ⊨ υ x ⟹
    τ ⊨ ((s::('𝔄,'a::null)Set) ≐ t) ⟹ τ ⊨ (s->including⇩S⇩e⇩t(x) ≐ (t->including⇩S⇩e⇩t(x)))"
proof -
 have cp: "cp (λs. (s->including⇩S⇩e⇩t(x)))"
  apply(simp add: cp_def, subst OclIncluding.cp0)
 by (rule_tac x = "(λxab ab. ((λ_. xab)->including⇩S⇩e⇩t(λ_. x ab)) ab)" in exI, simp)

 show "τ ⊨ δ s ⟹ τ ⊨ δ t ⟹ τ ⊨ υ x ⟹ τ ⊨ (s ≐ t) ⟹ ?thesis"
  apply(rule_tac P = "λs. (s->including⇩S⇩e⇩t(x))" in StrictRefEq⇩S⇩e⇩t_L_subst1)
       apply(rule cp)
      apply(simp add: foundation20) apply(simp add: foundation20)
    apply (simp add: foundation10 foundation6)+
 done
qed

lemma OclIncluding_cong : "⋀(s::('𝔄,'a::null)Set) t x y τ. τ ⊨ δ t ⟹ τ ⊨ υ y ⟹
                             τ ⊨ s ≐ t ⟹ x = y ⟹ τ ⊨ s->including⇩S⇩e⇩t(x) ≐ (t->including⇩S⇩e⇩t(y))"
 apply(simp only:)
 apply(rule OclIncluding_cong', simp_all only:)
by(auto simp: OclValid_def OclIf_def invalid_def bot_option_def OclNot_def split : if_split_asm)

(* < *)
lemma const_StrictRefEq⇩S⇩e⇩t_empty : "const X ⟹  const (X ≐ Set{})" 
 apply(rule StrictRefEq⇩S⇩e⇩t.const, assumption)
by(simp)

lemma const_StrictRefEq⇩S⇩e⇩t_including : 
 "const a ⟹ const S ⟹ const X ⟹  const (X ≐ S->including⇩S⇩e⇩t(a))"
 apply(rule StrictRefEq⇩S⇩e⇩t.const, assumption)
by(rule const_OclIncluding)

subsection‹Test Statements›

Assert   "(τ ⊨ (Set{λ_. ⌊⌊x⌋⌋} ≐ Set{λ_. ⌊⌊x⌋⌋}))"
Assert   "(τ ⊨ (Set{λ_. ⌊x⌋} ≐ Set{λ_. ⌊x⌋}))"

instantiation Set⇩b⇩a⇩s⇩e  :: (equal)equal
begin
  definition "HOL.equal k l ⟷  (k::('a::equal)Set⇩b⇩a⇩s⇩e) =  l"
  instance   by standard (rule equal_Set⇩b⇩a⇩s⇩e_def)
end

lemma equal_Set⇩b⇩a⇩s⇩e_code [code]:
  "HOL.equal k (l::('a::{equal,null})Set⇩b⇩a⇩s⇩e) ⟷ Rep_Set⇩b⇩a⇩s⇩e k = Rep_Set⇩b⇩a⇩s⇩e l"
  by (auto simp add: equal Set⇩b⇩a⇩s⇩e.Rep_Set⇩b⇩a⇩s⇩e_inject)

Assert   "τ ⊨ (Set{} ≐ Set{})" 
Assert   "τ ⊨ (Set{𝟭,𝟮} ≜ Set{}->including⇩S⇩e⇩t(𝟮)->including⇩S⇩e⇩t(𝟭))" 
Assert   "τ ⊨ (Set{𝟭,invalid,𝟮} ≜ invalid)"
Assert   "τ ⊨ (Set{𝟭,𝟮}->including⇩S⇩e⇩t(null) ≜ Set{null,𝟭,𝟮})"
Assert   "τ ⊨ (Set{𝟭,𝟮}->including⇩S⇩e⇩t(null) ≜ Set{𝟭,𝟮,null})"

(*
Assert   "¬ (τ ⊨ (Set{𝟭,𝟭,𝟮} ≐ Set{𝟭,𝟮}))"
Assert   "¬ (τ ⊨ (Set{𝟭,𝟮} ≐ Set{𝟮,𝟭}))"
*)

(* > *)

end