Theory UML_State

(*****************************************************************************
 * Featherweight-OCL --- A Formal Semantics for UML-OCL Version OCL 2.5
 *                       for the OMG Standard.
 *                       http://www.brucker.ch/projects/hol-testgen/
 *
 * UML_State.thy --- State Operations and Objects.
 * 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.
 ******************************************************************************)

chapter‹Formalization III:  UML/OCL constructs: State Operations and Objects›

theory  UML_State
imports UML_Library
begin

no_notation None ("⊥")
section‹Introduction: States over Typed Object Universes›

text‹\label{sec:universe}
  In the following, we will refine the concepts of a user-defined
  data-model (implied by a class-diagram) as well as the notion of
  $\state{}$ used in the previous section to much more detail.
  Surprisingly, even without a concrete notion of an objects and a
  universe of object representation, the generic infrastructure of
  state-related operations is fairly rich.
›



subsection‹Fundamental Properties on Objects: Core Referential Equality›
subsubsection‹Definition›

text‹Generic referential equality - to be used for instantiations
 with concrete object types ...›
definition  StrictRefEqObject :: "('𝔄,'a::{object,null})val ⇒ ('𝔄,'a)val ⇒ ('𝔄)Boolean"
where      "StrictRefEqObject x y
            ≡ λ τ. if (υ x) τ = true τ ∧ (υ y) τ = true τ
                    then if x τ = null ∨ y τ = null
                         then ⌊⌊x τ = null ∧ y τ = null⌋⌋
                         else ⌊⌊(oid_of (x τ)) = (oid_of (y τ)) ⌋⌋
                    else invalid τ"

subsubsection‹Strictness and context passing›

lemma StrictRefEqObject_strict1[simp,code_unfold] :
"(StrictRefEqObject x invalid) = invalid"
by(rule ext, simp add: StrictRefEqObject_def true_def false_def)

lemma StrictRefEqObject_strict2[simp,code_unfold] :
"(StrictRefEqObject invalid x) = invalid"
by(rule ext, simp add: StrictRefEqObject_def true_def false_def)


lemma cp_StrictRefEqObject:
"(StrictRefEqObject x y τ) = (StrictRefEqObject (λ_. x τ) (λ_. y τ)) τ"
by(auto simp: StrictRefEqObject_def cp_valid[symmetric])

text_raw‹\isatagafp›
lemmas cp0_StrictRefEqObject= cp_StrictRefEqObject[THEN allI[THEN allI[THEN allI[THEN cpI2]],
             of "StrictRefEqObject"]]

lemmas cp_intro''[intro!,simp,code_unfold] =
       cp_intro''
       cp_StrictRefEqObject[THEN allI[THEN allI[THEN allI[THEN cpI2]],
             of "StrictRefEqObject"]]

text_raw‹\endisatagafp›

subsection‹Logic and Algebraic Layer on Object›
subsubsection‹Validity and Definedness Properties›

text‹We derive the usual laws on definedness for (generic) object equality:›
lemma StrictRefEqObject_defargs:
"τ ⊨ (StrictRefEqObject x (y::('𝔄,'a::{null,object})val))⟹ (τ ⊨(υ x)) ∧ (τ ⊨(υ y))"
by(simp add: StrictRefEqObject_def OclValid_def true_def invalid_def bot_option_def
        split: bool.split_asm HOL.if_split_asm)

lemma defined_StrictRefEqObject_I:
 assumes val_x : "τ ⊨ υ x"
 assumes val_x : "τ ⊨ υ y"
 shows "τ ⊨ δ (StrictRefEqObject x y)"
 apply(insert assms, simp add: StrictRefEqObject_def OclValid_def)
by(subst cp_defined, simp add: true_def)

lemma StrictRefEqObject_def_homo :
"δ(StrictRefEqObject x (y::('𝔄,'a::{null,object})val)) = ((υ x) and (υ y))"
oops (* sorry *)

subsubsection‹Symmetry›

lemma StrictRefEqObject_sym :
assumes x_val : "τ ⊨ υ x"
shows "τ ⊨ StrictRefEqObject x x"
by(simp add: StrictRefEqObject_def true_def OclValid_def
             x_val[simplified OclValid_def])


subsubsection‹Behavior vs StrongEq›

text‹It remains to clarify the role of the state invariant
$\inv_\sigma(\sigma)$ mentioned above that states the condition that
there is a ``one-to-one'' correspondence between object
representations and $\oid$'s: $\forall \mathit{oid} \in \dom\ap
\sigma\spot oid = \HolOclOidOf\ap \drop{\sigma(\mathit{oid})}$.  This
condition is also mentioned in~cite‹‹Annex A› in "omg:ocl:2012"› and goes
back to citet‹"richters:precise:2002"›; however, we state this
condition as an invariant on states rather than a global axiom. It
can, therefore, not be taken for granted that an $\oid$ makes sense
both in pre- and post-states of OCL expressions.
›

text‹We capture this invariant in the predicate WFF :›

definition WFF :: "('𝔄::object)st ⇒ bool"
where "WFF τ = ((∀ x ∈ ran(heap(fst τ)). ⌈heap(fst τ) (oid_of x)⌉ = x) ∧
                (∀ x ∈ ran(heap(snd τ)). ⌈heap(snd τ) (oid_of x)⌉ = x))"

text‹It turns out that WFF is a key-concept for linking strict referential equality to
logical equality: in well-formed states (i.e. those states where the self (oid-of) field contains
the pointer to which the object is associated to in the state), referential equality coincides
with logical equality.›


text‹We turn now to the generic definition of referential equality on objects:
Equality on objects in a state is reduced to equality on the
references to these objects. As in HOL-OCL~cite‹"brucker.ea:hol-ocl:2008" and "brucker.ea:hol-ocl-book:2006"›,
we will store the reference of an object inside the object in a (ghost) field.
By establishing certain invariants (``consistent state''), it can
be assured that there is a ``one-to-one-correspondence'' of objects
to their references---and therefore the definition below
behaves as we expect.›
text‹Generic Referential Equality enjoys the usual properties:
(quasi) reflexivity, symmetry, transitivity, substitutivity for
defined values. For type-technical reasons, for each concrete
object type, the equality ‹≐› is defined by generic referential
equality.›

theorem StrictRefEqObject_vs_StrongEq:
assumes WFF: "WFF τ"
and valid_x: "τ ⊨(υ x)"
and valid_y: "τ ⊨(υ y)"
and x_present_pre: "x τ ∈ ran (heap(fst τ))"
and y_present_pre: "y τ ∈ ran (heap(fst τ))"
and x_present_post:"x τ ∈ ran (heap(snd τ))"
and y_present_post:"y τ ∈ ran (heap(snd τ))"
 (* x and y must be object representations that exist in either the pre or post state *)
shows "(τ ⊨ (StrictRefEqObject x y)) = (τ ⊨ (x ≜ y))"
apply(insert WFF valid_x valid_y x_present_pre y_present_pre x_present_post y_present_post)
apply(auto simp: StrictRefEqObject_def OclValid_def WFF_def StrongEq_def true_def Ball_def)
apply(erule_tac x="x τ" in allE', simp_all)
done

theorem StrictRefEqObject_vs_StrongEq':
assumes WFF: "WFF τ"
and valid_x: "τ ⊨(υ (x :: ('𝔄::object,'α::{null,object})val))"
and valid_y: "τ ⊨(υ y)"
and oid_preserve: "⋀x. x ∈ ran (heap(fst τ)) ∨ x ∈ ran (heap(snd τ)) ⟹
                        H x ≠ ⊥ ⟹ oid_of (H x) = oid_of x"
and xy_together: "x τ ∈ H ` ran (heap(fst τ)) ∧ y τ ∈ H ` ran (heap(fst τ)) ∨
                  x τ ∈ H ` ran (heap(snd τ)) ∧ y τ ∈ H ` ran (heap(snd τ))"
 (* x and y must be object representations that exist in either the pre or post state *)
shows "(τ ⊨ (StrictRefEqObject x y)) = (τ ⊨ (x ≜ y))"
 apply(insert WFF valid_x valid_y xy_together)
 apply(simp add: WFF_def)
 apply(auto simp: StrictRefEqObject_def OclValid_def WFF_def StrongEq_def true_def Ball_def)
by (metis foundation18' oid_preserve valid_x valid_y)+

text‹So, if two object descriptions live in the same state (both pre or post), the referential
equality on objects implies in a WFF state the logical equality.›

section‹Operations on Object›
subsection‹Initial States (for testing and code generation)›

definition τ0 :: "('𝔄)st"
where     "τ0 ≡ (⦇heap=Map.empty, assocs = Map.empty⦈,
                 ⦇heap=Map.empty, assocs = Map.empty⦈)"

subsection‹OclAllInstances›

text‹To denote OCL types occurring in OCL expressions syntactically---as, for example,
as ``argument'' of \inlineocl{oclAllInstances()}---we use the inverses of the injection functions into the object
universes; we show that this is a sufficient ``characterization.''›

definition OclAllInstances_generic :: "(('𝔄::object) st ⇒ '𝔄 state) ⇒ ('𝔄::object ⇀ 'α) ⇒
                                       ('𝔄, 'α option option) Set"
where "OclAllInstances_generic fst_snd H =
                    (λτ. Abs_Setbase ⌊⌊ Some ` ((H ` ran (heap (fst_snd τ))) - { None }) ⌋⌋)"

lemma OclAllInstances_generic_defined: "τ ⊨ δ (OclAllInstances_generic pre_post H)"
 apply(simp add: defined_def OclValid_def OclAllInstances_generic_def false_def true_def
                 bot_fun_def bot_Setbase_def null_fun_def null_Setbase_def)
 apply(rule conjI)
 apply(rule notI, subst (asm) Abs_Setbase_inject, simp,
       (rule disjI2)+,
       metis bot_option_def option.distinct(1),
       (simp add: bot_option_def null_option_def)+)+
done

lemma OclAllInstances_generic_init_empty:
 assumes [simp]: "⋀x. pre_post (x, x) = x"
 shows "τ0 ⊨ OclAllInstances_generic pre_post H ≜ Set{}"
by(simp add: StrongEq_def OclAllInstances_generic_def OclValid_def τ0_def mtSet_def)

lemma represented_generic_objects_nonnull:
assumes A: "τ ⊨ ((OclAllInstances_generic pre_post (H::('𝔄::object ⇀ 'α))) ->includesSet(x))"
shows      "τ ⊨ not(x ≜ null)"
proof -
    have B: "τ ⊨ δ (OclAllInstances_generic pre_post H)"
         by (simp add: OclAllInstances_generic_defined)
    have C: "τ ⊨ υ x"
         by (metis OclIncludes.def_valid_then_def
                   OclIncludes_valid_args_valid A foundation6)
    show ?thesis
    apply(insert A)
    apply(simp add: StrongEq_def  OclValid_def
                    OclNot_def null_def true_def OclIncludes_def B[simplified OclValid_def]
                                                                 C[simplified OclValid_def])
    apply(simp add:OclAllInstances_generic_def)
    apply(erule contrapos_pn)
    apply(subst Setbase.Abs_Setbase_inverse,
          auto simp: null_fun_def null_option_def bot_option_def)
    done
qed


lemma represented_generic_objects_defined:
assumes A: "τ ⊨ ((OclAllInstances_generic pre_post (H::('𝔄::object ⇀ 'α))) ->includesSet(x))"
shows      "τ ⊨ δ (OclAllInstances_generic pre_post H) ∧ τ ⊨ δ x"
by (metis OclAllInstances_generic_defined
          A[THEN represented_generic_objects_nonnull] OclIncludes.defined_args_valid
          A foundation16' foundation18 foundation24 foundation6)


text‹One way to establish the actual presence of an object representation in a state is:›

definition "is_represented_in_state fst_snd x H τ = (x τ ∈ (Some o H) ` ran (heap (fst_snd τ)))"

lemma represented_generic_objects_in_state:
assumes A: "τ ⊨ (OclAllInstances_generic pre_post H)->includesSet(x)"
shows      "is_represented_in_state pre_post x H τ"
proof -
   have B: "(δ (OclAllInstances_generic pre_post H)) τ = true τ"
           by(simp add: OclValid_def[symmetric] OclAllInstances_generic_defined)
   have C: "(υ x) τ = true τ"
           by (metis OclValid_def UML_Set.OclIncludes_def assms bot_option_def option.distinct(1) true_def)
   have F: "Rep_Setbase (Abs_Setbase ⌊⌊Some ` (H ` ran (heap (pre_post τ)) - {None})⌋⌋) =
            ⌊⌊Some ` (H ` ran (heap (pre_post τ)) - {None})⌋⌋"
           by(subst Setbase.Abs_Setbase_inverse,simp_all add: bot_option_def)
   show ?thesis
    apply(insert A)
    apply(simp add: is_represented_in_state_def OclIncludes_def OclValid_def ran_def B C image_def true_def)
    apply(simp add: OclAllInstances_generic_def)
    apply(simp add: F)
    apply(simp add: ran_def)
   by(fastforce)
qed


lemma state_update_vs_allInstances_generic_empty:
assumes [simp]: "⋀a. pre_post (mk a) = a"
shows   "(mk ⦇heap=Map.empty, assocs=A⦈) ⊨ OclAllInstances_generic pre_post Type ≐ Set{}"
proof -
 have state_update_vs_allInstances_empty:
  "(OclAllInstances_generic pre_post Type) (mk ⦇heap=Map.empty, assocs=A⦈) =
   Set{} (mk ⦇heap=Map.empty, assocs=A⦈)"
 by(simp add: OclAllInstances_generic_def mtSet_def)
 show ?thesis
  apply(simp only: OclValid_def, subst StrictRefEqSet.cp0,
        simp only: state_update_vs_allInstances_empty StrictRefEqSet.refl_ext)
  apply(simp add: OclIf_def valid_def mtSet_def defined_def
                  bot_fun_def null_fun_def null_option_def bot_Setbase_def)
 by(subst Abs_Setbase_inject, (simp add: bot_option_def true_def)+)
qed

text‹Here comes a couple of operational rules that allow to infer the value
of \inlineisar+oclAllInstances+ from the context $\tau$. These rules are a special-case
in the sense that they are the only rules that relate statements with \emph{different}
$\tau$'s. For that reason, new concepts like ``constant contexts P'' are necessary
(for which we do not elaborate an own theory for reasons of space limitations;
 in examples, we will prove resulting constraints straight forward by hand).›


lemma state_update_vs_allInstances_generic_including':
assumes [simp]: "⋀a. pre_post (mk a) = a"
assumes "⋀x. σ' oid = Some x ⟹ x = Object"
    and "Type Object ≠ None"
  shows "(OclAllInstances_generic pre_post Type)
         (mk ⦇heap=σ'(oid↦Object), assocs=A⦈)
         =
         ((OclAllInstances_generic pre_post Type)->includingSet(λ _. ⌊⌊ drop (Type Object) ⌋⌋))
         (mk ⦇heap=σ',assocs=A⦈)"
proof -
 have drop_none : "⋀x. x ≠ None ⟹ ⌊⌈x⌉⌋ = x"
 by(case_tac x, simp+)

 have insert_diff : "⋀x S. insert ⌊x⌋ (S - {None}) = (insert ⌊x⌋ S) - {None}"
 by (metis insert_Diff_if option.distinct(1) singletonE)

 show ?thesis
  apply(simp add: UML_Set.OclIncluding_def OclAllInstances_generic_defined[simplified OclValid_def],
        simp add: OclAllInstances_generic_def)
  apply(subst Abs_Setbase_inverse, simp add: bot_option_def, simp add: comp_def,
        subst image_insert[symmetric],
        subst drop_none, simp add: assms)
  apply(case_tac "Type Object", simp add: assms, simp only:,
        subst insert_diff, drule sym, simp)
  apply(subgoal_tac "ran (σ'(oid ↦ Object)) = insert Object (ran σ')", simp)
  apply(case_tac "¬ (∃x. σ' oid = Some x)")
   apply(rule ran_map_upd, simp)
  apply(simp, erule exE, frule assms, simp)
  apply(subgoal_tac "Object ∈ ran σ'") prefer 2
   apply(rule ranI, simp)
 by(subst insert_absorb, simp, metis fun_upd_apply)

qed


lemma state_update_vs_allInstances_generic_including:
assumes [simp]: "⋀a. pre_post (mk a) = a"
assumes "⋀x. σ' oid = Some x ⟹ x = Object"
    and "Type Object ≠ None"
shows   "(OclAllInstances_generic pre_post Type)
         (mk ⦇heap=σ'(oid↦Object), assocs=A⦈)
         =
         ((λ_. (OclAllInstances_generic pre_post Type)
                 (mk ⦇heap=σ', assocs=A⦈))->includingSet(λ _. ⌊⌊ drop (Type Object) ⌋⌋))
         (mk ⦇heap=σ'(oid↦Object), assocs=A⦈)"
 apply(subst state_update_vs_allInstances_generic_including', (simp add: assms)+,
       subst UML_Set.OclIncluding.cp0,
       simp add: UML_Set.OclIncluding_def)
 apply(subst (1 3) cp_defined[symmetric],
       simp add: OclAllInstances_generic_defined[simplified OclValid_def])

 apply(simp add: defined_def OclValid_def OclAllInstances_generic_def invalid_def
                 bot_fun_def null_fun_def bot_Setbase_def null_Setbase_def)
 apply(subst (1 3) Abs_Setbase_inject)
by(simp add: bot_option_def null_option_def)+



lemma state_update_vs_allInstances_generic_noincluding':
assumes [simp]: "⋀a. pre_post (mk a) = a"
assumes "⋀x. σ' oid = Some x ⟹ x = Object"
    and "Type Object = None"
  shows "(OclAllInstances_generic pre_post Type)
         (mk ⦇heap=σ'(oid↦Object), assocs=A⦈)
         =
         (OclAllInstances_generic pre_post Type)
         (mk ⦇heap=σ', assocs=A⦈)"
proof -
 have drop_none : "⋀x. x ≠ None ⟹ ⌊⌈x⌉⌋ = x"
 by(case_tac x, simp+)

 have insert_diff : "⋀x S. insert ⌊x⌋ (S - {None}) = (insert ⌊x⌋ S) - {None}"
 by (metis insert_Diff_if option.distinct(1) singletonE)

 show ?thesis
  apply(simp add: OclIncluding_def OclAllInstances_generic_defined[simplified OclValid_def]
                  OclAllInstances_generic_def)
  apply(subgoal_tac "ran (σ'(oid ↦ Object)) = insert Object (ran σ')", simp add: assms)
  apply(case_tac "¬ (∃x. σ' oid = Some x)")
   apply(rule ran_map_upd, simp)
  apply(simp, erule exE, frule assms, simp)
  apply(subgoal_tac "Object ∈ ran σ'") prefer 2
   apply(rule ranI, simp)
  apply(subst insert_absorb, simp)
 by (metis fun_upd_apply)
qed

theorem state_update_vs_allInstances_generic_ntc:
assumes [simp]: "⋀a. pre_post (mk a) = a"
assumes oid_def:   "oid∉dom σ'"
and  non_type_conform: "Type Object = None "
and  cp_ctxt:      "cp P"
and  const_ctxt:   "⋀X. const X ⟹ const (P X)"
shows "(mk ⦇heap=σ'(oid↦Object),assocs=A⦈ ⊨ P (OclAllInstances_generic pre_post Type)) =
       (mk ⦇heap=σ', assocs=A⦈            ⊨ P (OclAllInstances_generic pre_post Type))"
      (is "(?τ ⊨ P ?φ) = (?τ' ⊨ P ?φ)")
proof -
 have P_cp  : "⋀x τ. P x τ = P (λ_. x τ) τ"
             by (metis (full_types) cp_ctxt cp_def)
 have A     : "const (P (λ_. ?φ ?τ))"
             by(simp add: const_ctxt const_ss)
 have       "(?τ ⊨ P ?φ) = (?τ ⊨ λ_. P ?φ ?τ)"
             by(subst foundation23, rule refl)
 also have  "... = (?τ ⊨ λ_. P (λ_. ?φ ?τ)  ?τ)"
             by(subst P_cp, rule refl)
 also have  "... = (?τ' ⊨ λ_. P (λ_. ?φ ?τ)  ?τ')"
             apply(simp add: OclValid_def)
             by(subst A[simplified const_def], subst const_true[simplified const_def], simp)
 finally have X: "(?τ ⊨ P ?φ) = (?τ' ⊨ λ_. P (λ_. ?φ ?τ)  ?τ')"
             by simp
 show ?thesis
 apply(subst X) apply(subst foundation23[symmetric])
 apply(rule StrongEq_L_subst3[OF cp_ctxt])
 apply(simp add: OclValid_def StrongEq_def true_def)
 apply(rule state_update_vs_allInstances_generic_noincluding')
 by(insert oid_def, auto simp: non_type_conform)
qed

theorem state_update_vs_allInstances_generic_tc:
assumes [simp]: "⋀a. pre_post (mk a) = a"
assumes oid_def:   "oid∉dom σ'"
and  type_conform: "Type Object ≠ None "
and  cp_ctxt:      "cp P"
and  const_ctxt:   "⋀X. const X ⟹ const (P X)"
shows "(mk ⦇heap=σ'(oid↦Object),assocs=A⦈ ⊨ P (OclAllInstances_generic pre_post Type)) =
       (mk ⦇heap=σ', assocs=A⦈            ⊨ P ((OclAllInstances_generic pre_post Type)
                                                                ->includingSet(λ _. ⌊(Type Object)⌋)))"
       (is "(?τ ⊨ P ?φ) = (?τ' ⊨ P ?φ')")
proof -
 have P_cp  : "⋀x τ. P x τ = P (λ_. x τ) τ"
             by (metis (full_types) cp_ctxt cp_def)
 have A     : "const (P (λ_. ?φ ?τ))"
             by(simp add: const_ctxt const_ss)
 have       "(?τ ⊨ P ?φ) = (?τ ⊨ λ_. P ?φ ?τ)"
             by(subst foundation23, rule refl)
 also have  "... = (?τ ⊨ λ_. P (λ_. ?φ ?τ)  ?τ)"
             by(subst P_cp, rule refl)
 also have  "... = (?τ' ⊨ λ_. P (λ_. ?φ ?τ)  ?τ')"
             apply(simp add: OclValid_def)
             by(subst A[simplified const_def], subst const_true[simplified const_def], simp)
 finally have X: "(?τ ⊨ P ?φ) = (?τ' ⊨ λ_. P (λ_. ?φ ?τ)  ?τ')"
             by simp
 let         ?allInstances = "OclAllInstances_generic pre_post Type"
 have        "?allInstances ?τ = λ_. ?allInstances ?τ'->includingSet(λ_.⌊⌊⌈Type Object⌉⌋⌋) ?τ"
             apply(rule state_update_vs_allInstances_generic_including)
             by(insert oid_def, auto simp: type_conform)
 also have   "... = ((λ_. ?allInstances ?τ')->includingSet(λ_. (λ_.⌊⌊⌈Type Object⌉⌋⌋) ?τ') ?τ')"
             by(subst const_OclIncluding[simplified const_def], simp+)
 also have   "... = (?allInstances->includingSet(λ _. ⌊Type Object⌋) ?τ')"
             apply(subst UML_Set.OclIncluding.cp0[symmetric])
             by(insert type_conform, auto)
 finally have Y : "?allInstances ?τ = (?allInstances->includingSet(λ _. ⌊Type Object⌋) ?τ')"
             by auto
 show ?thesis
      apply(subst X) apply(subst foundation23[symmetric])
      apply(rule StrongEq_L_subst3[OF cp_ctxt])
      apply(simp add: OclValid_def StrongEq_def Y true_def)
 done
qed

declare OclAllInstances_generic_def [simp]

subsubsection‹OclAllInstances (@post)›

definition OclAllInstances_at_post :: "('𝔄 :: object ⇀ 'α) ⇒ ('𝔄, 'α option option) Set"
                           ("_ .allInstances'(')")
where  "OclAllInstances_at_post =  OclAllInstances_generic snd"

lemma OclAllInstances_at_post_defined: "τ ⊨ δ (H .allInstances())"
unfolding OclAllInstances_at_post_def
by(rule OclAllInstances_generic_defined)

lemma "τ0 ⊨ H .allInstances() ≜ Set{}"
unfolding OclAllInstances_at_post_def
by(rule OclAllInstances_generic_init_empty, simp)


lemma represented_at_post_objects_nonnull:
assumes A: "τ ⊨ (((H::('𝔄::object ⇀ 'α)).allInstances()) ->includesSet(x))"
shows      "τ ⊨ not(x ≜ null)"
by(rule represented_generic_objects_nonnull[OF A[simplified OclAllInstances_at_post_def]])


lemma represented_at_post_objects_defined:
assumes A: "τ ⊨ (((H::('𝔄::object ⇀ 'α)).allInstances()) ->includesSet(x))"
shows      "τ ⊨ δ (H .allInstances()) ∧ τ ⊨ δ x"
unfolding OclAllInstances_at_post_def
by(rule represented_generic_objects_defined[OF A[simplified OclAllInstances_at_post_def]])


text‹One way to establish the actual presence of an object representation in a state is:›

lemma
assumes A: "τ ⊨ H .allInstances()->includesSet(x)"
shows      "is_represented_in_state snd x H τ"
by(rule represented_generic_objects_in_state[OF A[simplified OclAllInstances_at_post_def]])

lemma state_update_vs_allInstances_at_post_empty:
shows   "(σ, ⦇heap=Map.empty, assocs=A⦈) ⊨ Type .allInstances() ≐ Set{}"
unfolding OclAllInstances_at_post_def
by(rule state_update_vs_allInstances_generic_empty[OF snd_conv])

text‹Here comes a couple of operational rules that allow to infer the value
of \inlineisar+oclAllInstances+ from the context $\tau$. These rules are a special-case
in the sense that they are the only rules that relate statements with \emph{different}
$\tau$'s. For that reason, new concepts like ``constant contexts P'' are necessary
(for which we do not elaborate an own theory for reasons of space limitations;
 in examples, we will prove resulting constraints straight forward by hand).›


lemma state_update_vs_allInstances_at_post_including':
assumes "⋀x. σ' oid = Some x ⟹ x = Object"
    and "Type Object ≠ None"
  shows "(Type .allInstances())
         (σ, ⦇heap=σ'(oid↦Object), assocs=A⦈)
         =
         ((Type .allInstances())->includingSet(λ _. ⌊⌊ drop (Type Object) ⌋⌋))
         (σ, ⦇heap=σ',assocs=A⦈)"
unfolding OclAllInstances_at_post_def
by(rule state_update_vs_allInstances_generic_including'[OF snd_conv], insert assms)


lemma state_update_vs_allInstances_at_post_including:
assumes "⋀x. σ' oid = Some x ⟹ x = Object"
    and "Type Object ≠ None"
shows   "(Type .allInstances())
         (σ, ⦇heap=σ'(oid↦Object), assocs=A⦈)
         =
         ((λ_. (Type .allInstances())
                 (σ, ⦇heap=σ', assocs=A⦈))->includingSet(λ _. ⌊⌊ drop (Type Object) ⌋⌋))
         (σ, ⦇heap=σ'(oid↦Object), assocs=A⦈)"
unfolding OclAllInstances_at_post_def
by(rule state_update_vs_allInstances_generic_including[OF snd_conv], insert assms)



lemma state_update_vs_allInstances_at_post_noincluding':
assumes "⋀x. σ' oid = Some x ⟹ x = Object"
    and "Type Object = None"
  shows "(Type .allInstances())
         (σ, ⦇heap=σ'(oid↦Object), assocs=A⦈)
         =
         (Type .allInstances())
         (σ, ⦇heap=σ', assocs=A⦈)"
unfolding OclAllInstances_at_post_def
by(rule state_update_vs_allInstances_generic_noincluding'[OF snd_conv], insert assms)

theorem state_update_vs_allInstances_at_post_ntc:
assumes oid_def:   "oid∉dom σ'"
and  non_type_conform: "Type Object = None "
and  cp_ctxt:      "cp P"
and  const_ctxt:   "⋀X. const X ⟹ const (P X)"
shows   "((σ, ⦇heap=σ'(oid↦Object),assocs=A⦈) ⊨ (P(Type .allInstances()))) =
         ((σ, ⦇heap=σ', assocs=A⦈)            ⊨ (P(Type .allInstances())))"
unfolding OclAllInstances_at_post_def
by(rule state_update_vs_allInstances_generic_ntc[OF snd_conv], insert assms)

theorem state_update_vs_allInstances_at_post_tc:
assumes oid_def:   "oid∉dom σ'"
and  type_conform: "Type Object ≠ None "
and  cp_ctxt:      "cp P"
and  const_ctxt:   "⋀X. const X ⟹ const (P X)"
shows   "((σ, ⦇heap=σ'(oid↦Object),assocs=A⦈) ⊨ (P(Type .allInstances()))) =
         ((σ, ⦇heap=σ', assocs=A⦈)            ⊨ (P((Type .allInstances())
                                                               ->includingSet(λ _. ⌊(Type Object)⌋))))"
unfolding OclAllInstances_at_post_def
by(rule state_update_vs_allInstances_generic_tc[OF snd_conv], insert assms)

subsubsection‹OclAllInstances (@pre)›

definition OclAllInstances_at_pre :: "('𝔄 :: object ⇀ 'α) ⇒ ('𝔄, 'α option option) Set"
                           ("_ .allInstances@pre'(')")
where  "OclAllInstances_at_pre = OclAllInstances_generic fst"

lemma OclAllInstances_at_pre_defined: "τ ⊨ δ (H .allInstances@pre())"
unfolding OclAllInstances_at_pre_def
by(rule OclAllInstances_generic_defined)

lemma "τ0 ⊨ H .allInstances@pre() ≜ Set{}"
unfolding OclAllInstances_at_pre_def
by(rule OclAllInstances_generic_init_empty, simp)


lemma represented_at_pre_objects_nonnull:
assumes A: "τ ⊨ (((H::('𝔄::object ⇀ 'α)).allInstances@pre()) ->includesSet(x))"
shows      "τ ⊨ not(x ≜ null)"
by(rule represented_generic_objects_nonnull[OF A[simplified OclAllInstances_at_pre_def]])

lemma represented_at_pre_objects_defined:
assumes A: "τ ⊨ (((H::('𝔄::object ⇀ 'α)).allInstances@pre()) ->includesSet(x))"
shows      "τ ⊨ δ (H .allInstances@pre()) ∧ τ ⊨ δ x"
unfolding OclAllInstances_at_pre_def
by(rule represented_generic_objects_defined[OF A[simplified OclAllInstances_at_pre_def]])


text‹One way to establish the actual presence of an object representation in a state is:›

lemma
assumes A: "τ ⊨ H .allInstances@pre()->includesSet(x)"
shows      "is_represented_in_state fst x H τ"
by(rule represented_generic_objects_in_state[OF A[simplified OclAllInstances_at_pre_def]])


lemma state_update_vs_allInstances_at_pre_empty:
shows   "(⦇heap=Map.empty, assocs=A⦈, σ) ⊨ Type .allInstances@pre() ≐ Set{}"
unfolding OclAllInstances_at_pre_def
by(rule state_update_vs_allInstances_generic_empty[OF fst_conv])

text‹Here comes a couple of operational rules that allow to infer the value
of \inlineisar+oclAllInstances@pre+ from the context $\tau$. These rules are a special-case
in the sense that they are the only rules that relate statements with \emph{different}
$\tau$'s. For that reason, new concepts like ``constant contexts P'' are necessary
(for which we do not elaborate an own theory for reasons of space limitations;
 in examples, we will prove resulting constraints straight forward by hand).›


lemma state_update_vs_allInstances_at_pre_including':
assumes "⋀x. σ' oid = Some x ⟹ x = Object"
    and "Type Object ≠ None"
  shows "(Type .allInstances@pre())
         (⦇heap=σ'(oid↦Object), assocs=A⦈, σ)
         =
         ((Type .allInstances@pre())->includingSet(λ _. ⌊⌊ drop (Type Object) ⌋⌋))
         (⦇heap=σ',assocs=A⦈, σ)"
unfolding OclAllInstances_at_pre_def
by(rule state_update_vs_allInstances_generic_including'[OF fst_conv], insert assms)


lemma state_update_vs_allInstances_at_pre_including:
assumes "⋀x. σ' oid = Some x ⟹ x = Object"
    and "Type Object ≠ None"
shows   "(Type .allInstances@pre())
         (⦇heap=σ'(oid↦Object), assocs=A⦈, σ)
         =
         ((λ_. (Type .allInstances@pre())
                 (⦇heap=σ', assocs=A⦈, σ))->includingSet(λ _. ⌊⌊ drop (Type Object) ⌋⌋))
         (⦇heap=σ'(oid↦Object), assocs=A⦈, σ)"
unfolding OclAllInstances_at_pre_def
by(rule state_update_vs_allInstances_generic_including[OF fst_conv], insert assms)



lemma state_update_vs_allInstances_at_pre_noincluding':
assumes "⋀x. σ' oid = Some x ⟹ x = Object"
    and "Type Object = None"
  shows "(Type .allInstances@pre())
         (⦇heap=σ'(oid↦Object), assocs=A⦈, σ)
         =
         (Type .allInstances@pre())
         (⦇heap=σ', assocs=A⦈, σ)"
unfolding OclAllInstances_at_pre_def
by(rule state_update_vs_allInstances_generic_noincluding'[OF fst_conv], insert assms)

theorem state_update_vs_allInstances_at_pre_ntc:
assumes oid_def:   "oid∉dom σ'"
and  non_type_conform: "Type Object = None "
and  cp_ctxt:      "cp P"
and  const_ctxt:   "⋀X. const X ⟹ const (P X)"
shows   "((⦇heap=σ'(oid↦Object),assocs=A⦈, σ) ⊨ (P(Type .allInstances@pre()))) =
         ((⦇heap=σ', assocs=A⦈, σ)            ⊨ (P(Type .allInstances@pre())))"
unfolding OclAllInstances_at_pre_def
by(rule state_update_vs_allInstances_generic_ntc[OF fst_conv], insert assms)

theorem state_update_vs_allInstances_at_pre_tc:
assumes oid_def:   "oid∉dom σ'"
and  type_conform: "Type Object ≠ None "
and  cp_ctxt:      "cp P"
and  const_ctxt:   "⋀X. const X ⟹ const (P X)"
shows   "((⦇heap=σ'(oid↦Object),assocs=A⦈, σ) ⊨ (P(Type .allInstances@pre()))) =
         ((⦇heap=σ', assocs=A⦈, σ)            ⊨ (P((Type .allInstances@pre())
                                                               ->includingSet(λ _. ⌊(Type Object)⌋))))"
unfolding OclAllInstances_at_pre_def
by(rule state_update_vs_allInstances_generic_tc[OF fst_conv], insert assms)

subsubsection‹@post or @pre›

theorem StrictRefEqObject_vs_StrongEq'':
assumes WFF: "WFF τ"
and valid_x: "τ ⊨(υ (x :: ('𝔄::object,'α::object option option)val))"
and valid_y: "τ ⊨(υ y)"
and oid_preserve: "⋀x. x ∈ ran (heap(fst τ)) ∨ x ∈ ran (heap(snd τ)) ⟹
                        oid_of (H x) = oid_of x"
and xy_together: "τ ⊨ ((H .allInstances()->includesSet(x) and H .allInstances()->includesSet(y)) or
                       (H .allInstances@pre()->includesSet(x) and H .allInstances@pre()->includesSet(y)))"
 (* x and y must be object representations that exist in either the pre or post state *)
shows "(τ ⊨ (StrictRefEqObject x y)) = (τ ⊨ (x ≜ y))"
proof -
   have at_post_def : "⋀x. τ ⊨ υ x ⟹ τ ⊨ δ (H .allInstances()->includesSet(x))"
    apply(simp add: OclIncludes_def OclValid_def
                    OclAllInstances_at_post_defined[simplified OclValid_def])
   by(subst cp_defined, simp)
   have at_pre_def : "⋀x. τ ⊨ υ x ⟹ τ ⊨ δ (H .allInstances@pre()->includesSet(x))"
    apply(simp add: OclIncludes_def OclValid_def
                    OclAllInstances_at_pre_defined[simplified OclValid_def])
   by(subst cp_defined, simp)
   have F: "Rep_Setbase (Abs_Setbase ⌊⌊Some ` (H ` ran (heap (fst τ)) - {None})⌋⌋) =
            ⌊⌊Some ` (H ` ran (heap (fst τ)) - {None})⌋⌋"
           by(subst Setbase.Abs_Setbase_inverse,simp_all add: bot_option_def)
   have F': "Rep_Setbase (Abs_Setbase ⌊⌊Some ` (H ` ran (heap (snd τ)) - {None})⌋⌋) =
            ⌊⌊Some ` (H ` ran (heap (snd τ)) - {None})⌋⌋"
           by(subst Setbase.Abs_Setbase_inverse,simp_all add: bot_option_def)
 show ?thesis
  apply(rule StrictRefEqObject_vs_StrongEq'[OF WFF valid_x valid_y, where H = "Some o H"])
  apply(subst oid_preserve[symmetric], simp, simp add: oid_of_option_def)
  apply(insert xy_together,
        subst (asm) foundation11,
        metis at_post_def defined_and_I valid_x valid_y,
        metis at_pre_def defined_and_I valid_x valid_y)
  apply(erule disjE)
 by(drule foundation5,
    simp add: OclAllInstances_at_pre_def OclAllInstances_at_post_def
              OclValid_def OclIncludes_def true_def F F'
              valid_x[simplified OclValid_def] valid_y[simplified OclValid_def] bot_option_def
         split: if_split_asm,
    simp add: comp_def image_def, fastforce)+
qed

subsection‹OclIsNew, OclIsDeleted, OclIsMaintained, OclIsAbsent›

definition OclIsNew:: "('𝔄, 'α::{null,object})val ⇒ ('𝔄)Boolean"   ("(_).oclIsNew'(')")
where "X .oclIsNew() ≡ (λτ . if (δ X) τ = true τ
                              then ⌊⌊oid_of (X τ) ∉ dom(heap(fst τ)) ∧
                                     oid_of (X τ) ∈ dom(heap(snd τ))⌋⌋
                              else invalid τ)"

text‹The following predicates --- which are not part of the OCL standard descriptions ---
complete the goal of \inlineisar+oclIsNew+ by describing where an object belongs.
›

definition OclIsDeleted:: "('𝔄, 'α::{null,object})val ⇒ ('𝔄)Boolean"   ("(_).oclIsDeleted'(')")
where "X .oclIsDeleted() ≡ (λτ . if (δ X) τ = true τ
                              then ⌊⌊oid_of (X τ) ∈ dom(heap(fst τ)) ∧
                                     oid_of (X τ) ∉ dom(heap(snd τ))⌋⌋
                              else invalid τ)"

definition OclIsMaintained:: "('𝔄, 'α::{null,object})val ⇒ ('𝔄)Boolean"("(_).oclIsMaintained'(')")
where "X .oclIsMaintained() ≡ (λτ . if (δ X) τ = true τ
                              then ⌊⌊oid_of (X τ) ∈ dom(heap(fst τ)) ∧
                                     oid_of (X τ) ∈ dom(heap(snd τ))⌋⌋
                              else invalid τ)"

definition OclIsAbsent:: "('𝔄, 'α::{null,object})val ⇒ ('𝔄)Boolean"   ("(_).oclIsAbsent'(')")
where "X .oclIsAbsent() ≡ (λτ . if (δ X) τ = true τ
                              then ⌊⌊oid_of (X τ) ∉ dom(heap(fst τ)) ∧
                                     oid_of (X τ) ∉ dom(heap(snd τ))⌋⌋
                              else invalid τ)"

lemma state_split : "τ ⊨ δ X ⟹
                     τ ⊨ (X .oclIsNew()) ∨ τ ⊨ (X .oclIsDeleted()) ∨
                     τ ⊨ (X .oclIsMaintained()) ∨ τ ⊨ (X .oclIsAbsent())"
by(simp add: OclIsDeleted_def OclIsNew_def OclIsMaintained_def OclIsAbsent_def
             OclValid_def true_def, blast)

lemma notNew_vs_others : "τ ⊨ δ X ⟹
                         (¬ τ ⊨ (X .oclIsNew())) = (τ ⊨ (X .oclIsDeleted()) ∨
                          τ ⊨ (X .oclIsMaintained()) ∨ τ ⊨ (X .oclIsAbsent()))"
by(simp add: OclIsDeleted_def OclIsNew_def OclIsMaintained_def OclIsAbsent_def
                OclNot_def OclValid_def true_def, blast)

subsection‹OclIsModifiedOnly›
subsubsection‹Definition›

text‹The following predicate---which is not part of the OCL
standard---provides a simple, but powerful means to describe framing
conditions. For any formal approach, be it animation of OCL contracts,
test-case generation or die-hard theorem proving, the specification of
the part of a system transition that \emph{does not change} is of
primordial importance. The following operator establishes the equality
between old and new objects in the state (provided that they exist in
both states), with the exception of those objects.›

definition OclIsModifiedOnly ::"('𝔄::object,'α::{null,object})Set ⇒ '𝔄 Boolean"
                        ("_->oclIsModifiedOnly'(')")
where "X->oclIsModifiedOnly() ≡ (λ(σ,σ').
                           let X' = (oid_of ` ⌈⌈Rep_Setbase(X(σ,σ'))⌉⌉);
                               S = ((dom (heap σ) ∩ dom (heap σ')) - X')
                           in if (δ X) (σ,σ') = true (σ,σ') ∧ (∀x∈⌈⌈Rep_Setbase(X(σ,σ'))⌉⌉. x ≠ null)
                              then ⌊⌊∀ x ∈ S. (heap σ) x = (heap σ') x⌋⌋
                              else invalid (σ,σ'))"

subsubsection‹Execution with Invalid or Null or Null Element as Argument›

lemma "invalid->oclIsModifiedOnly() = invalid"
by(simp add: OclIsModifiedOnly_def)

lemma "null->oclIsModifiedOnly() = invalid"
by(simp add: OclIsModifiedOnly_def)

lemma
 assumes X_null : "τ ⊨ X->includesSet(null)"
 shows "τ ⊨ X->oclIsModifiedOnly() ≜ invalid"
 apply(insert X_null,
       simp add : OclIncludes_def OclIsModifiedOnly_def StrongEq_def OclValid_def true_def)
 apply(case_tac τ, simp)
 apply(simp split: if_split_asm)
by(simp add: null_fun_def, blast)

subsubsection‹Context Passing›

lemma cp_OclIsModifiedOnly : "X->oclIsModifiedOnly() τ = (λ_. X τ)->oclIsModifiedOnly() τ"
by(simp only: OclIsModifiedOnly_def, case_tac τ, simp only:, subst cp_defined, simp)

subsection‹OclSelf›

text‹The following predicate---which is not part of the OCL
standard---explicitly retrieves in the pre or post state the original OCL expression
given as argument.›

definition [simp]: "OclSelf x H fst_snd = (λτ . if (δ x) τ = true τ
                        then if oid_of (x τ) ∈ dom(heap(fst τ)) ∧ oid_of (x τ) ∈ dom(heap (snd τ))
                             then  H ⌈(heap(fst_snd τ))(oid_of (x τ))⌉
                             else invalid τ
                        else invalid τ)"

definition OclSelf_at_pre :: "('𝔄::object,'α::{null,object})val ⇒
                      ('𝔄 ⇒ 'α) ⇒
                      ('𝔄::object,'α::{null,object})val" ("(_)@pre(_)")
where "x @pre H = OclSelf x H fst"

definition OclSelf_at_post :: "('𝔄::object,'α::{null,object})val ⇒
                      ('𝔄 ⇒ 'α) ⇒
                      ('𝔄::object,'α::{null,object})val" ("(_)@post(_)")
where "x @post H = OclSelf x H snd"

subsection‹Framing Theorem›

lemma all_oid_diff:
 assumes def_x : "τ ⊨ δ x"
 assumes def_X : "τ ⊨ δ X"
 assumes def_X' : "⋀x. x ∈ ⌈⌈Rep_Setbase (X τ)⌉⌉ ⟹ x ≠ null"

 defines "P ≡ (λa. not (StrictRefEqObject x a))"
 shows "(τ ⊨ X->forAllSet(a| P a)) = (oid_of (x τ) ∉ oid_of ` ⌈⌈Rep_Setbase (X τ)⌉⌉)"
proof -
 have P_null_bot: "⋀b. b = null ∨ b = ⊥ ⟹
                        ¬ (∃x∈⌈⌈Rep_Setbase (X τ)⌉⌉. P (λ(_:: 'a state × 'a state). x) τ = b τ)"
  apply(erule disjE)
   apply(simp, rule ballI,
         simp add: P_def StrictRefEqObject_def, rename_tac x',
         subst cp_OclNot, simp,
         subgoal_tac "x τ ≠ null ∧ x' ≠ null", simp,
         simp add: OclNot_def null_fun_def null_option_def bot_option_def bot_fun_def invalid_def,
         ( metis def_X' def_x foundation16[THEN iffD1]
         | (metis bot_fun_def OclValid_def Set_inv_lemma def_X def_x defined_def valid_def,
            metis def_X' def_x foundation16[THEN iffD1])))+
 done


 have not_inj : "⋀x y. ((not x) τ = (not y) τ) = (x τ = y τ)"
 by (metis foundation21 foundation22)

 have P_false : "∃x∈⌈⌈Rep_Setbase (X τ)⌉⌉. P (λ_. x) τ = false τ ⟹
                 oid_of (x τ) ∈ oid_of ` ⌈⌈Rep_Setbase (X τ)⌉⌉"
  apply(erule bexE, rename_tac x')
  apply(simp add: P_def)
  apply(simp only: OclNot3[symmetric], simp only: not_inj)
  apply(simp add: StrictRefEqObject_def split: if_split_asm)
    apply(subgoal_tac "x τ ≠ null ∧ x' ≠ null", simp)
    apply (metis (mono_tags) drop.simps def_x foundation16[THEN iffD1] true_def)
 by(simp add: invalid_def bot_option_def true_def)+

 have P_true : "∀x∈⌈⌈Rep_Setbase (X τ)⌉⌉. P (λ_. x) τ = true τ ⟹
                oid_of (x τ) ∉ oid_of ` ⌈⌈Rep_Setbase (X τ)⌉⌉"
  apply(subgoal_tac "∀x'∈⌈⌈Rep_Setbase (X τ)⌉⌉. oid_of x' ≠ oid_of (x τ)")
   apply (metis imageE)
  apply(rule ballI, drule_tac x = "x'" in ballE) prefer 3 apply assumption
   apply(simp add: P_def)
   apply(simp only: OclNot4[symmetric], simp only: not_inj)
   apply(simp add: StrictRefEqObject_def false_def split: if_split_asm)
    apply(subgoal_tac "x τ ≠ null ∧ x' ≠ null", simp)
    apply (metis def_X' def_x  foundation16[THEN iffD1])
 by(simp add: invalid_def bot_option_def false_def)+

 have bool_split : "∀x∈⌈⌈Rep_Setbase (X τ)⌉⌉. P (λ_. x) τ ≠ null τ ⟹
                    ∀x∈⌈⌈Rep_Setbase (X τ)⌉⌉. P (λ_. x) τ ≠ ⊥ τ ⟹
                    ∀x∈⌈⌈Rep_Setbase (X τ)⌉⌉. P (λ_. x) τ ≠ false τ ⟹
                    ∀x∈⌈⌈Rep_Setbase (X τ)⌉⌉. P (λ_. x) τ = true τ"
  apply(rule ballI)
  apply(drule_tac x = x in ballE) prefer 3 apply assumption
   apply(drule_tac x = x in ballE) prefer 3 apply assumption
    apply(drule_tac x = x in ballE) prefer 3 apply assumption
     apply (metis (full_types) bot_fun_def OclNot4 OclValid_def foundation16
                               foundation9 not_inj null_fun_def)
 by(fast+)

 show ?thesis
  apply(subst OclForall_rep_set_true[OF def_X], simp add: OclValid_def)
  apply(rule iffI, simp add: P_true)
 by (metis P_false P_null_bot bool_split)
qed

theorem framing:
      assumes modifiesclause:"τ ⊨ (X->excludingSet(x))->oclIsModifiedOnly()"
      and oid_is_typerepr : "τ ⊨ X->forAllSet(a| not (StrictRefEqObject x a))"
      shows "τ ⊨ (x @pre P  ≜  (x @post P))"
 apply(case_tac "τ ⊨ δ x")
 proof - show "τ ⊨ δ x ⟹ ?thesis" proof - assume def_x : "τ ⊨ δ x" show ?thesis proof -

 have def_X : "τ ⊨ δ X"
  apply(insert oid_is_typerepr, simp add: UML_Set.OclForall_def OclValid_def split: if_split_asm)
 by(simp add: bot_option_def true_def)

 have def_X' : "⋀x. x ∈ ⌈⌈Rep_Setbase (X τ)⌉⌉ ⟹ x ≠ null"
  apply(insert modifiesclause, simp add: OclIsModifiedOnly_def OclValid_def split: if_split_asm)
  apply(case_tac τ, simp split: if_split_asm)
   apply(simp add: UML_Set.OclExcluding_def split: if_split_asm)
    apply(subst (asm) (2) Abs_Setbase_inverse)
     apply(simp, (rule disjI2)+)
     apply (metis (opaque_lifting, mono_tags) Diff_iff Set_inv_lemma def_X)
    apply(simp)
    apply(erule ballE[where P = "λx. x ≠ null"]) apply(assumption)
    apply(simp)
    apply (metis (opaque_lifting, no_types) def_x  foundation16[THEN iffD1])
   apply (metis (opaque_lifting, no_types) OclValid_def def_X def_x foundation20
                                      OclExcluding_valid_args_valid OclExcluding_valid_args_valid'')
 by(simp add: invalid_def bot_option_def)

 have oid_is_typerepr : "oid_of (x τ) ∉ oid_of ` ⌈⌈Rep_Setbase (X τ)⌉⌉"
 by(rule all_oid_diff[THEN iffD1, OF def_x def_X def_X' oid_is_typerepr])

 show ?thesis
  apply(simp add: StrongEq_def OclValid_def true_def OclSelf_at_pre_def OclSelf_at_post_def
                  def_x[simplified OclValid_def])
  apply(rule conjI, rule impI)
   apply(rule_tac f = "λx. P ⌈x⌉" in arg_cong)
   apply(insert modifiesclause[simplified OclIsModifiedOnly_def OclValid_def])
   apply(case_tac τ, rename_tac σ σ', simp split: if_split_asm)
    apply(subst (asm) (2) UML_Set.OclExcluding_def)
    apply(drule foundation5[simplified OclValid_def true_def], simp)
    apply(subst (asm) Abs_Setbase_inverse, simp)
     apply(rule disjI2)+
     apply (metis (opaque_lifting, no_types) DiffD1 OclValid_def Set_inv_lemma def_x
                                        foundation16 foundation18')
    apply(simp)
    apply(erule_tac x = "oid_of (x (σ, σ'))" in ballE) apply simp+
    apply (metis (opaque_lifting, no_types)
                 DiffD1 image_iff image_insert insert_Diff_single insert_absorb oid_is_typerepr)
   apply(simp add: invalid_def bot_option_def)+
 by blast
 qed qed
qed(simp add: OclSelf_at_post_def OclSelf_at_pre_def OclValid_def StrongEq_def true_def)+


text‹As corollary, the framing property can be expressed with only the strong equality
as comparison operator.›

theorem framing':
  assumes wff : "WFF τ"
  assumes modifiesclause:"τ ⊨ (X->excludingSet(x))->oclIsModifiedOnly()"
  and oid_is_typerepr : "τ ⊨ X->forAllSet(a| not (x ≜ a))"
  and oid_preserve: "⋀x. x ∈ ran (heap(fst τ)) ∨ x ∈ ran (heap(snd τ)) ⟹
                          oid_of (H x) = oid_of x"
  and xy_together:
  "τ ⊨ X->forAllSet(y | (H .allInstances()->includesSet(x) and H .allInstances()->includesSet(y)) or
                     (H .allInstances@pre()->includesSet(x) and H .allInstances@pre()->includesSet(y)))"
  shows "τ ⊨ (x @pre P  ≜  (x @post P))"
proof -
 have def_X : "τ ⊨ δ X"
  apply(insert oid_is_typerepr, simp add: UML_Set.OclForall_def OclValid_def split: if_split_asm)
 by(simp add: bot_option_def true_def)
 show ?thesis
  apply(case_tac "τ ⊨ δ x", drule foundation20)
   apply(rule framing[OF modifiesclause])
   apply(rule OclForall_cong'[OF _ oid_is_typerepr xy_together], rename_tac y)
   apply(cut_tac Set_inv_lemma'[OF def_X]) prefer 2 apply assumption
   apply(rule OclNot_contrapos_nn, simp add: StrictRefEqObject_def)
     apply(simp add: OclValid_def, subst cp_defined, simp,
           assumption)
   apply(rule StrictRefEqObject_vs_StrongEq''[THEN iffD1, OF wff _ _ oid_preserve], assumption+)
 by(simp add: OclSelf_at_post_def OclSelf_at_pre_def OclValid_def StrongEq_def true_def)+
qed

subsection‹Miscellaneous›

lemma pre_post_new: "τ ⊨ (x .oclIsNew()) ⟹ ¬ (τ ⊨ υ(x @pre H1)) ∧ ¬ (τ ⊨ υ(x @post H2))"
by(simp add: OclIsNew_def OclSelf_at_pre_def OclSelf_at_post_def
             OclValid_def StrongEq_def true_def false_def
             bot_option_def invalid_def bot_fun_def valid_def
      split: if_split_asm)

lemma pre_post_old: "τ ⊨ (x .oclIsDeleted()) ⟹ ¬ (τ ⊨ υ(x @pre H1)) ∧ ¬ (τ ⊨ υ(x @post H2))"
by(simp add: OclIsDeleted_def OclSelf_at_pre_def OclSelf_at_post_def
             OclValid_def StrongEq_def true_def false_def
             bot_option_def invalid_def bot_fun_def valid_def
      split: if_split_asm)

lemma pre_post_absent: "τ ⊨ (x .oclIsAbsent()) ⟹ ¬ (τ ⊨ υ(x @pre H1)) ∧ ¬ (τ ⊨ υ(x @post H2))"
by(simp add: OclIsAbsent_def OclSelf_at_pre_def OclSelf_at_post_def
             OclValid_def StrongEq_def true_def false_def
             bot_option_def invalid_def bot_fun_def valid_def
      split: if_split_asm)

lemma pre_post_maintained: "(τ ⊨ υ(x @pre H1) ∨ τ ⊨ υ(x @post H2)) ⟹ τ ⊨ (x .oclIsMaintained())"
by(simp add: OclIsMaintained_def OclSelf_at_pre_def OclSelf_at_post_def
             OclValid_def StrongEq_def true_def false_def
             bot_option_def invalid_def bot_fun_def valid_def
      split: if_split_asm)

lemma pre_post_maintained':
"τ ⊨ (x .oclIsMaintained()) ⟹ (τ ⊨ υ(x @pre (Some o H1)) ∧ τ ⊨ υ(x @post (Some o H2)))"
by(simp add: OclIsMaintained_def OclSelf_at_pre_def OclSelf_at_post_def
             OclValid_def StrongEq_def true_def false_def
             bot_option_def invalid_def bot_fun_def valid_def
      split: if_split_asm)

lemma framing_same_state: "(σ, σ) ⊨ (x @pre H  ≜  (x @post H))"
by(simp add: OclSelf_at_pre_def OclSelf_at_post_def OclValid_def StrongEq_def)

section‹Accessors on Object›
subsection‹Definition›

definition "select_object mt incl smash deref l = smash (foldl incl mt (map deref l))
 ― ‹smash returns null with ‹mt› in input (in this case, object contains null pointer)›"

text‹The continuation ‹f› is usually instantiated with a smashing
function which is either the identity @{term id} or, for \inlineocl{0..1} cardinalities
of associations, the @{term OclANY}-selector which also handles the
@{term null}-cases appropriately. A standard use-case for this combinator
is for example:›
term "(select_object mtSet UML_Set.OclIncluding UML_Set.OclANY f  l oid )::('𝔄, 'a::null)val"

definition "select_objectSet = select_object mtSet UML_Set.OclIncluding id"
definition "select_object_any0Set f s_set = UML_Set.OclANY (select_objectSet f s_set)"
definition "select_object_anySet f s_set = 
 (let s = select_objectSet f s_set in
  if s->sizeSet() ≜ 𝟭 then
    s->anySet()
  else
    ⊥
  endif)"
definition "select_objectSeq = select_object mtSequence UML_Sequence.OclIncluding id"
definition "select_object_anySeq f s_set = UML_Sequence.OclANY (select_objectSeq f s_set)"
definition "select_objectPair f1 f2 = (λ(a,b). OclPair (f1 a) (f2 b))"

subsection‹Validity and Definedness Properties›

lemma select_fold_execSeq:
 assumes "list_all (λf. (τ ⊨ υ f)) l"
 shows "⌈⌈Rep_Sequencebase (foldl UML_Sequence.OclIncluding Sequence{} l τ)⌉⌉ = List.map (λf. f τ) l"
proof -
 have def_fold: "⋀l. list_all (λf. τ ⊨ υ f) l ⟹
            τ ⊨ (δ foldl UML_Sequence.OclIncluding Sequence{} l)"
  apply(rule rev_induct[where P = "λl. list_all (λf. (τ ⊨ υ f)) l ⟶ τ ⊨ (δ foldl UML_Sequence.OclIncluding Sequence{} l)", THEN mp], simp)
 by(simp add: foundation10')
 show ?thesis
  apply(rule rev_induct[where P = "λl. list_all (λf. (τ ⊨ υ f)) l ⟶ ⌈⌈Rep_Sequencebase (foldl UML_Sequence.OclIncluding Sequence{} l τ)⌉⌉ = List.map (λf. f τ) l", THEN mp], simp)
    apply(simp add: mtSequence_def)
    apply(subst Abs_Sequencebase_inverse, (simp | intro impI)+)
   apply(simp add: UML_Sequence.OclIncluding_def, intro conjI impI)
    apply(subst Abs_Sequencebase_inverse, simp, (rule disjI2)+)
     apply(simp add: list_all_iff foundation18', simp)
   apply(subst (asm) def_fold[simplified (no_asm) OclValid_def], simp, simp add: OclValid_def)
 by (rule assms)
qed

lemma select_fold_execSet:
 assumes "list_all (λf. (τ ⊨ υ f)) l"
 shows "⌈⌈Rep_Setbase (foldl UML_Set.OclIncluding Set{} l τ)⌉⌉ = set (List.map (λf. f τ) l)"
proof -
 have def_fold: "⋀l. list_all (λf. τ ⊨ υ f) l ⟹
            τ ⊨ (δ foldl UML_Set.OclIncluding Set{} l)"
  apply(rule rev_induct[where P = "λl. list_all (λf. (τ ⊨ υ f)) l ⟶ τ ⊨ (δ foldl UML_Set.OclIncluding Set{} l)", THEN mp], simp)
 by(simp add: foundation10')
 show ?thesis
  apply(rule rev_induct[where P = "λl. list_all (λf. (τ ⊨ υ f)) l ⟶ ⌈⌈Rep_Setbase (foldl UML_Set.OclIncluding Set{} l τ)⌉⌉ = set (List.map (λf. f τ) l)", THEN mp], simp)
    apply(simp add: mtSet_def)
    apply(subst Abs_Setbase_inverse, (simp | intro impI)+)
   apply(simp add: UML_Set.OclIncluding_def, intro conjI impI)
    apply(subst Abs_Setbase_inverse, simp, (rule disjI2)+)
     apply(simp add: list_all_iff foundation18', simp)
   apply(subst (asm) def_fold[simplified (no_asm) OclValid_def], simp, simp add: OclValid_def)
 by (rule assms)
qed

lemma fold_val_elemSeq:
 assumes "τ ⊨ υ (foldl UML_Sequence.OclIncluding Sequence{} (List.map (f p) s_set))"
 shows "list_all (λx. (τ ⊨ υ (f p x))) s_set"
 apply(rule rev_induct[where P = "λs_set. τ ⊨ υ foldl UML_Sequence.OclIncluding Sequence{} (List.map (f p) s_set) ⟶ list_all (λx. τ ⊨ υ f p x) s_set", THEN mp])
   apply(simp, auto)
    apply (metis (opaque_lifting, mono_tags) UML_Sequence.OclIncluding.def_valid_then_def UML_Sequence.OclIncluding.defined_args_valid foundation20)+
by(simp add: assms)

lemma fold_val_elemSet:
 assumes "τ ⊨ υ (foldl UML_Set.OclIncluding Set{} (List.map (f p) s_set))"
 shows "list_all (λx. (τ ⊨ υ (f p x))) s_set"
 apply(rule rev_induct[where P = "λs_set. τ ⊨ υ foldl UML_Set.OclIncluding Set{} (List.map (f p) s_set) ⟶ list_all (λx. τ ⊨ υ f p x) s_set", THEN mp])
   apply(simp, auto)
    apply (metis (opaque_lifting, mono_tags) foundation10' foundation20)+
by(simp add: assms)

lemma select_object_any_definedSeq:
 assumes def_sel: "τ ⊨ δ (select_object_anySeq f s_set)"
 shows "s_set ≠ []"
 apply(insert def_sel, case_tac s_set)
  apply(simp add: select_object_anySeq_def UML_Sequence.OclANY_def select_objectSeq_def select_object_def
                  defined_def OclValid_def
                  false_def true_def bot_fun_def bot_option_def
             split: if_split_asm)
  apply(simp add: mtSequence_def, subst (asm) Abs_Sequencebase_inverse, simp, simp)
by(simp)

lemma (*select_object_any_definedSet:*)
 assumes def_sel: "τ ⊨ δ (select_object_any0Set f s_set)"
 shows "s_set ≠ []"
 apply(insert def_sel, case_tac s_set)
  apply(simp add: select_object_any0Set_def UML_Sequence.OclANY_def select_objectSet_def select_object_def
                  defined_def OclValid_def
                  false_def true_def bot_fun_def bot_option_def
             split: if_split_asm)
by(simp)

lemma select_object_any_definedSet:
 assumes def_sel: "τ ⊨ δ (select_object_anySet f s_set)"
 shows "s_set ≠ []"
 apply(insert def_sel, case_tac s_set)
  apply(simp add: select_object_anySet_def UML_Sequence.OclANY_def select_objectSet_def select_object_def
                  defined_def OclValid_def
                  false_def true_def bot_fun_def bot_option_def
                  OclInt0_def OclInt1_def StrongEq_def OclIf_def null_fun_def null_option_def
             split: if_split_asm)
by(simp)

lemma select_object_any_exec0Seq:
 assumes def_sel: "τ ⊨ δ (select_object_anySeq f s_set)"
 shows "τ ⊨ (select_object_anySeq f s_set ≜ f (hd s_set))"
  apply(insert def_sel[simplified foundation16],
        simp add: select_object_anySeq_def foundation22 UML_Sequence.OclANY_def split: if_split_asm)
  apply(case_tac "⌈⌈Rep_Sequencebase (select_objectSeq f s_set τ)⌉⌉", simp add: bot_option_def, simp)
  apply(simp add: select_objectSeq_def select_object_def)
  apply(subst (asm) select_fold_execSeq)
   apply(rule fold_val_elemSeq, simp add: foundation18' invalid_def)
  apply(simp)
by(drule arg_cong[where f = hd], subst (asm) hd_map, simp add: select_object_any_definedSeq[OF def_sel], simp)

lemma select_object_any_execSeq:
 assumes def_sel: "τ ⊨ δ (select_object_anySeq f s_set)"
 shows "∃e. List.member s_set e ∧ (τ ⊨ (select_object_anySeq f s_set ≜ f e))"
 apply(insert select_object_any_exec0Seq[OF def_sel])
 apply(rule exI[where x = "hd s_set"], simp)
 apply(case_tac s_set, simp add: select_object_any_definedSeq[OF def_sel])
by (metis list.sel member_rec(1))

lemma (*select_object_any_execSet:*)
 assumes def_sel: "τ ⊨ δ (select_object_any0Set f s_set)"
 shows "∃ e. List.member s_set e ∧ (τ ⊨ (select_object_any0Set f s_set ≜ f e))"
proof -
 have list_all_map: "⋀P f l. list_all P (List.map f l) = list_all (P o f) l"
 by(induct_tac l, simp_all)

 fix z
 show ?thesis
  when "⌈⌈Rep_Setbase (select_objectSet f s_set τ)⌉⌉ = z"
  apply(insert that def_sel[simplified foundation16],
        simp add: select_object_any0Set_def foundation22 UML_Set.OclANY_def null_fun_def split: if_split_asm)

  apply(simp add: select_objectSet_def select_object_def)
  apply(subst (asm) select_fold_execSet)
   apply(rule fold_val_elemSet, simp add: OclValid_def)
  apply(simp add: comp_def)

  apply(case_tac s_set, simp, simp add: false_def true_def, simp)

  proof - fix a l
  show "insert (f a τ) ((λx. f x τ) ` set l) = z ⟹
        ∃e. List.member (a # l) e ∧ (SOME y. y ∈ z) = f e τ"
   apply(rule list.induct[where P = "λl. ∀z a. insert (f a τ) ((λx. f x τ) ` set l) = z ⟶
        (∃e. List.member (a # l) e ∧ ((SOME y. y ∈ z) = f e τ))", THEN spec, THEN spec, THEN mp], intro allI impI)
     proof - fix x xa show "insert (f xa τ) ((λx. f x τ) ` set []) = x ⟹ ∃e. List.member [xa] e ∧ (SOME y. y ∈ x) = f e τ"
      apply(rule exI[where x = xa], simp add: List.member_def)
      apply(subst some_equality[where a = "f xa τ"])
        apply (metis (mono_tags) insertI1)
       apply (metis (mono_tags) empty_iff insert_iff)
     by(simp)
    apply_end(intro allI impI, simp)
    fix x list xa xb
    show " ∀x. ∃e. List.member (x # list) e ∧ (SOME y. y = f x τ ∨ y ∈ (λx. f x τ) ` set list) = f e τ ⟹
       insert (f xb τ) (insert (f x τ) ((λx. f x τ) ` set list)) = xa ⟹
       ∃e. List.member (xb # x # list) e ∧ (SOME y. y ∈ xa) = f e τ"
     apply(case_tac "x = xb", simp)
      apply(erule allE[where x = xb])
      apply(erule exE)
      proof - fix e show "insert (f xb τ) ((λx. f x τ) ` set list) = xa ⟹
         x = xb ⟹
         List.member (xb # list) e ∧ (SOME y. y = f xb τ ∨ y ∈ (λx. f x τ) ` set list) = f e τ ⟹
         ∃e. List.member (xb # xb # list) e ∧ (SOME y. y ∈ xa) = f e τ"
      apply(rule exI[where x = e], auto)
      by (metis member_rec(1))
     apply_end(case_tac "List.member list x")
      apply_end(erule allE[where x = xb])
      apply_end(erule exE)
      fix e
      let ?P = "λy. y = f xb τ ∨ y ∈ (λx. f x τ) ` set list"
      show "insert (f xb τ) (insert (f x τ) ((λx. f x τ) ` set list)) = xa ⟹
         x ≠ xb ⟹
         List.member list x ⟹
         List.member (xb # list) e ∧ (SOME y. y = f xb τ ∨ y ∈ (λx. f x τ) ` set list) = f e τ ⟹
         ∃e. List.member (xb # x # list) e ∧ (SOME y. y ∈ xa) = f e τ"
       apply(rule exI[where x = e], auto)
        apply (metis member_rec(1))

       apply(subgoal_tac "?P (f e τ)")
        prefer 2
        apply(case_tac "xb = e", simp)
        apply (metis (mono_tags) image_eqI in_set_member member_rec(1)) 

       apply(rule someI2[where a = "f e τ"])
        apply(erule disjE, simp)+
        apply(rule disjI2)+ apply(simp)
oops

lemma select_object_any_execSet:
 assumes def_sel: "τ ⊨ δ (select_object_anySet f s_set)"
 shows "∃ e. List.member s_set e ∧ (τ ⊨ (select_object_anySet f s_set ≜ f e))"
proof -
 have card_singl: "⋀A a. finite A ⟹ card (insert a A) = 1 ⟹ A ⊆ {a}"
 by (auto, metis Suc_inject card_Suc_eq card_eq_0_iff insert_absorb insert_not_empty singleton_iff)

 have list_same: "⋀f s_set z' x. f ` set s_set = {z'} ⟹ List.member s_set x ⟹ f x = z'"
 by (metis (full_types) empty_iff imageI in_set_member insert_iff)

 fix z
 show ?thesis
  when "⌈⌈Rep_Setbase (select_objectSet f s_set τ)⌉⌉ = z"
  apply(insert that def_sel[simplified foundation16],
        simp add: select_object_anySet_def foundation22
                  Let_def null_fun_def bot_fun_def OclIf_def
             split: if_split_asm)
  apply(simp add: StrongEq_def OclInt1_def true_def UML_Set.OclSize_def
                  bot_option_def UML_Set.OclANY_def null_fun_def
                  split: if_split_asm)
  apply(subgoal_tac "∃z'. z = {z'}")
   prefer 2
   apply(rule finite.cases[where a = z], simp, simp, simp)
   apply(rule card_singl, simp, simp)
  apply(erule exE, clarsimp)

  apply(simp add: select_objectSet_def select_object_def)
  apply(subst (asm) select_fold_execSet)
   apply(rule fold_val_elemSet, simp add: OclValid_def true_def)
  apply(simp add: comp_def)

  apply(case_tac s_set, simp)
  proof - fix z' a list show "(λx. f x τ) ` set s_set = {z'} ⟹ s_set = a # list ⟹ ∃e. List.member s_set e ∧ z' = f e τ"
    apply(drule list_same[where x1 = a])
     apply (metis member_rec(1))
   by (metis (opaque_lifting, mono_tags) ListMem_iff elem in_set_member)
  qed
qed blast+

end