Theory UML_Logic

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

chapter‹Formalization II: OCL Terms and Library Operations›

theory  UML_Logic 
imports UML_Types 
begin

section‹The Operations of the Boolean Type and the OCL Logic›

subsection‹Basic Constants›

lemma bot_Boolean_def : "(bot::('𝔄)Boolean) = (λ τ. )"
by(simp add: bot_fun_def bot_option_def)

lemma null_Boolean_def : "(null::('𝔄)Boolean) = (λ τ. )"
by(simp add: null_fun_def null_option_def bot_option_def)

definition true :: "('𝔄)Boolean"
where     "true  λ τ. True"


definition false :: "('𝔄)Boolean"
where     "false   λ τ. False"

lemma bool_split_0: "X τ = invalid τ  X τ = null τ 
                   X τ = true τ     X τ = false τ"
apply(simp add: invalid_def null_def true_def false_def)
apply(case_tac "X τ",simp_all add: null_fun_def null_option_def bot_option_def)
apply(case_tac "a",simp)
apply(case_tac "aa",simp)
apply auto
done



lemma [simp]: "false (a, b) = False"
by(simp add:false_def)

lemma [simp]: "true (a, b) = True"
by(simp add:true_def)

lemma textbook_true: "I⟦true τ = True"
by(simp add: Sem_def true_def)

lemma textbook_false: "I⟦false τ = False"
by(simp add: Sem_def false_def)

text ‹
\begin{table}[htbp]
   \centering
   \begin{tabu}{lX[,c,]}
      \toprule
      Name & Theorem \\
      \midrule
      @{thm [source] textbook_invalid}  & @{thm  [display=false] textbook_invalid} \\
      @{thm [source] textbook_null_fun}  & @{thm [display=false] textbook_null_fun} \\
      @{thm [source] textbook_true}   & @{thm  [display=false] textbook_true} \\
      @{thm [source] textbook_false} & @{thm [display=false] textbook_false} \\
      \bottomrule
   \end{tabu}
   \caption{Basic semantic constant definitions of the logic}
   \label{tab:sem_basic_constants}
\end{table}
›

subsection‹Validity and Definedness›

text‹However, this has also the consequence that core concepts like definedness,
validity and even cp have to be redefined on this type class:›

definition valid :: "('𝔄,'a::null)val  ('𝔄)Boolean" ("υ _" [100]100)
where   "υ X   λ τ . if X τ = bot τ then false τ else true τ"

lemma valid1[simp]: "υ invalid = false"
  by(rule ext,simp add: valid_def bot_fun_def bot_option_def
                        invalid_def true_def false_def)
lemma valid2[simp]: "υ null = true"
  by(rule ext,simp add: valid_def bot_fun_def bot_option_def null_is_valid
                        null_fun_def invalid_def true_def false_def)
lemma valid3[simp]: "υ true = true"
  by(rule ext,simp add: valid_def bot_fun_def bot_option_def null_is_valid
                        null_fun_def invalid_def true_def false_def)
lemma valid4[simp]: "υ false = true"
  by(rule ext,simp add: valid_def bot_fun_def bot_option_def null_is_valid
                        null_fun_def invalid_def true_def false_def)
text_raw‹\isatagafp›
lemma cp_valid: "(υ X) τ = (υ (λ _. X τ)) τ"
by(simp add: valid_def)
text_raw‹\endisatagafp›

definition defined :: "('𝔄,'a::null)val  ('𝔄)Boolean" ("δ _" [100]100)
where   "δ X   λ τ . if X τ = bot τ   X τ = null τ then false τ else true τ"

text‹The generalized definitions of invalid and definedness have the same
properties as the old ones :›
lemma defined1[simp]: "δ invalid = false"
  by(rule ext,simp add: defined_def bot_fun_def bot_option_def
                        null_def invalid_def true_def false_def)
lemma defined2[simp]: "δ null = false"
  by(rule ext,simp add: defined_def bot_fun_def bot_option_def
                        null_def null_option_def null_fun_def invalid_def true_def false_def)
lemma defined3[simp]: "δ true = true"
  by(rule ext,simp add: defined_def bot_fun_def bot_option_def null_is_valid null_option_def
                        null_fun_def invalid_def true_def false_def)
lemma defined4[simp]: "δ false = true"
  by(rule ext,simp add: defined_def bot_fun_def bot_option_def null_is_valid null_option_def
                        null_fun_def invalid_def true_def false_def)
lemma defined5[simp]: "δ δ X = true"
  by(rule ext,
     auto simp:           defined_def true_def false_def
                bot_fun_def bot_option_def null_option_def null_fun_def)
lemma defined6[simp]: "δ υ X = true"
  by(rule ext,
     auto simp: valid_def defined_def true_def false_def
                bot_fun_def bot_option_def null_option_def null_fun_def)
lemma valid5[simp]: "υ υ X = true"
  by(rule ext,
     auto simp: valid_def             true_def false_def
                bot_fun_def bot_option_def null_option_def null_fun_def)
lemma valid6[simp]: "υ δ X = true"
  by(rule ext,
     auto simp: valid_def defined_def true_def false_def
                bot_fun_def bot_option_def null_option_def null_fun_def)
text_raw‹\isatagafp›
lemma cp_defined:"(δ X)τ = (δ (λ _. X τ)) τ"
by(simp add: defined_def)
text_raw‹\endisatagafp›

text‹The definitions above for the constants @{const defined} and @{const valid}
can be rewritten into the conventional semantic "textbook" format  as follows:›

lemma textbook_defined: "I⟦δ(X) τ = (if I⟦X τ = I⟦bot τ   I⟦X τ = I⟦null τ
                                     then I⟦false τ
                                     else I⟦true τ)"
by(simp add: Sem_def defined_def)

lemma textbook_valid: "I⟦υ(X) τ = (if I⟦X τ = I⟦bot τ
                                   then I⟦false τ
                                   else I⟦true τ)"
by(simp add: Sem_def valid_def)


text ‹
\autoref{tab:sem_definedness} and \autoref{tab:alglaws_definedness}
summarize the results of this section.
\begin{table}[htbp]
   \centering
   \begin{tabu}{lX[,c,]}
      \toprule
      Name & Theorem \\
      \midrule
      @{thm [source] textbook_defined}  & @{thm [show_question_marks=false,display=false,margin=45] textbook_defined} \\
      @{thm [source] textbook_valid}   & @{thm [show_question_marks=false,display=false,margin=45] textbook_valid} \\
      \bottomrule
   \end{tabu}
   \caption{Basic predicate definitions of the logic.}
   \label{tab:sem_definedness}
\end{table}
\begin{table}[htbp]
   \centering
   \begin{tabu}{lX[,c,]}
      \toprule
      Name & Theorem \\
      \midrule
      @{thm [source] defined1}  & @{thm  defined1} \\
      @{thm [source] defined2}   & @{thm [display=false,margin=35] defined2} \\
      @{thm [source] defined3}   & @{thm [display=false,margin=35] defined3} \\
      @{thm [source] defined4}   & @{thm [display=false,margin=35] defined4} \\
      @{thm [source] defined5}   & @{thm [display=false,margin=35] defined5} \\
      @{thm [source] defined6}   & @{thm [display=false,margin=35] defined6} \\
      \bottomrule
   \end{tabu}
   \caption{Laws of the basic predicates of the logic.}
   \label{tab:alglaws_definedness}
\end{table}
›

subsection‹The Equalities of OCL \label{sec:equality}›
text‹
  The OCL contains a particular version of equality, written in
  Standard documents \inlineocl+_ = _+ and \inlineocl+_ <> _+ for its
  negation, which is referred as \emph{weak referential equality}
  hereafter and for which we use the symbol \inlineisar+_ ≐ _+
  throughout the formal part of this document. Its semantics is
  motivated by the desire of fast execution, and similarity to
  languages like Java and C, but does not satisfy the needs of logical
  reasoning over OCL expressions and specifications. We therefore
  introduce a second equality, referred as \emph{strong equality} or
  \emph{logical equality} and written \inlineisar+_ ≜ _+
  which is not present in the current standard but was discussed in
  prior texts on OCL like the Amsterdam
  Manifesto~cite"cook.ea::amsterdam:2002" and was identified as
  desirable extension of OCL in the Aachen
  Meeting~cite"brucker.ea:summary-aachen:2013" in the future 2.5 OCL
  Standard. The purpose of strong equality is to define and reason
  over OCL. It is therefore a natural task in Featherweight OCL to
  formally investigate the somewhat quite complex relationship between
  these two.› text‹Strong equality has two motivations: a
  pragmatic one and a fundamental one.
  \begin{enumerate}
  \item The pragmatic reason is fairly simple: users of object-oriented languages want
    something like a ``shallow object value equality''.
    You will want to say
    \inlineisar+ a.boss ≜  b.boss@pre +
    instead of
\begin{isar}
  a.boss ≐ b.boss@pre and  (* just the pointers are equal! *)
  a.boss.name ≐ b.boss@pre.name@pre and
  a.boss.age ≐ b.boss@pre.age@pre
\end{isar}
      Breaking a shallow-object equality down to referential equality
      of attributes is cumbersome, error-prone, and makes
      specifications difficult to extend (add for example an attribute
      sex to your class, and check in your OCL specification
      everywhere that you did it right with your simulation of strong
      equality).  Therefore, languages like Java offer facilities
      to handle two different equalities, and it is problematic even
      in an execution oriented specification language to ignore
      shallow object equality because it is so common in the code.
    \item The fundamental reason goes as follows: whatever you do to
      reason consistently over a language, you need the concept of
      equality: you need to know what expressions can be replaced by
      others because they \emph{mean the same thing.}  People call
      this also ``Leibniz Equality'' because this philosopher brought
      this principle first explicitly to paper and shed some light
      over it. It is the theoretic foundation of what you do in an
      optimizing compiler: you replace expressions by \emph{equal}
      ones, which you hope are easier to evaluate. In a typed
      language, strong equality exists uniformly over all types, it is
      ``polymorphic'' $\_ = \_ :: \alpha * \alpha \rightarrow
      bool$---this is the way that equality is defined in HOL itself.
      We can express Leibniz principle as one logical rule of
      surprising simplicity and beauty:
    \begin{gather}
        s = t \Longrightarrow P(s) = P(t)
    \end{gather}
    ``Whenever we know, that $s$ is equal to $t$, we can replace the
    sub-expression $s$ in a term $P$ by $t$ and we have that the
    replacement is equal to the original.''
\end{enumerate}
›
text‹
  While weak referential equality is defined to be strict in the OCL
  standard, we will define strong equality as non-strict.  It is quite
  nasty (but not impossible) to define the logical equality in a
  strict way (the substitutivity rule above would look more complex),
  however, whenever references were used, strong equality is needed
  since references refer to particular states (pre or post), and that
  they mean the same thing can therefore not be taken for granted.
›

subsubsection‹Definition›
text‹
  The strict equality on basic types (actually on all types) must be
  exceptionally defined on @{term "null"}---otherwise the entire
  concept of null in the language does not make much sense. This is an
  important exception from the general rule that null
  arguments---especially if passed as ``self''-argument---lead to
  invalid results.
›


text‹
  We define strong equality extremely generic, even for types that
  contain a null› or ⊥› element. Strong
  equality is simply polymorphic in Featherweight OCL, \ie, is
  defined identical for all types in OCL and HOL.
›
definition StrongEq::"['𝔄 st  ,'𝔄 st  ]  ('𝔄)Boolean"  (infixl "" 30)
where     "X  Y   λ τ. X τ = Y τ "

text‹
  From this follow already elementary properties like:
›
lemma [simp,code_unfold]: "(true  false) = false"
by(rule ext, auto simp: StrongEq_def)

lemma [simp,code_unfold]: "(false  true) = false"
by(rule ext, auto simp: StrongEq_def)


subsubsection‹Fundamental Predicates on Strong Equality›

text‹Equality reasoning in OCL is not humpty dumpty. While strong equality
is clearly an equivalence:›
lemma StrongEq_refl [simp]: "(X  X) = true"
by(rule ext, simp add: null_def invalid_def true_def false_def StrongEq_def)

lemma StrongEq_sym: "(X  Y) = (Y  X)"
by(rule ext, simp add: eq_sym_conv invalid_def true_def false_def StrongEq_def)

lemma StrongEq_trans_strong [simp]:
  assumes A: "(X  Y) = true"
  and     B: "(Y  Z) = true"
  shows   "(X  Z) = true"
  apply(insert A B) apply(rule ext)
  apply(simp add: null_def invalid_def true_def false_def StrongEq_def)
  apply(drule_tac x=x in fun_cong)+
  by auto

text‹
    it is only in a limited sense a congruence, at least from the
    point of view of this semantic theory. The point is that it is
    only a congruence on OCL expressions, not arbitrary HOL
    expressions (with which we can mix Featherweight OCL expressions). A
    semantic---not syntactic---characterization of OCL expressions is
    that they are \emph{context-passing} or \emph{context-invariant},
    \ie, the context of an entire OCL expression, \ie the pre and
    post state it referes to, is passed constantly and unmodified to
    the sub-expressions, \ie, all sub-expressions inside an OCL
    expression refer to the same context. Expressed formally, this
    boils down to:
›
lemma StrongEq_subst :
  assumes cp: "X. P(X)τ = P(λ _. X τ)τ"
  and     eq: "(X  Y)τ = true τ"
  shows   "(P X  P Y)τ = true τ"
  apply(insert cp eq)
  apply(simp add: null_def invalid_def true_def false_def StrongEq_def)
  apply(subst cp[of X])
  apply(subst cp[of Y])
  by simp

lemma defined7[simp]: "δ (X  Y) = true"
  by(rule ext,
     auto simp: defined_def           true_def false_def StrongEq_def
                bot_fun_def bot_option_def null_option_def null_fun_def)

lemma valid7[simp]: "υ (X  Y) = true"
  by(rule ext,
     auto simp: valid_def true_def false_def StrongEq_def
                bot_fun_def bot_option_def null_option_def null_fun_def)

lemma cp_StrongEq: "(X  Y) τ = ((λ _. X τ)  (λ _. Y τ)) τ"
by(simp add: StrongEq_def)

subsection‹Logical Connectives and their Universal Properties›
text‹
  It is a design goal to give OCL a semantics that is as closely as
  possible to a ``logical system'' in a known sense; a specification
  logic where the logical connectives can not be understood other that
  having the truth-table aside when reading fails its purpose in our
  view.

  Practically, this means that we want to give a definition to the
  core operations to be as close as possible to the lattice laws; this
  makes also powerful symbolic normalization of OCL specifications
  possible as a pre-requisite for automated theorem provers. For
  example, it is still possible to compute without any definedness
  and validity reasoning the DNF of an OCL specification; be it for
  test-case generations or for a smooth transition to a two-valued
  representation of the specification amenable to fast standard
  SMT-solvers, for example.

  Thus, our representation of the OCL is merely a 4-valued
  Kleene-Logics with @{term "invalid"} as least, @{term "null"} as
  middle and @{term "true"} resp.  @{term "false"} as unrelated
  top-elements.
›


definition OclNot :: "('𝔄)Boolean  ('𝔄)Boolean" ("not")
where     "not X   λ τ . case X τ of
                                     
                           |         
                           |  x     ¬ x "



lemma cp_OclNot: "(not X)τ = (not (λ _. X τ)) τ"
by(simp add: OclNot_def)

lemma OclNot1[simp]: "not invalid = invalid"
  by(rule ext,simp add: OclNot_def null_def invalid_def true_def false_def bot_option_def)

lemma OclNot2[simp]: "not null = null"
  by(rule ext,simp add: OclNot_def null_def invalid_def true_def false_def
                        bot_option_def null_fun_def null_option_def )

lemma OclNot3[simp]: "not true = false"
  by(rule ext,simp add: OclNot_def null_def invalid_def true_def false_def)

lemma OclNot4[simp]: "not false = true"
  by(rule ext,simp add: OclNot_def null_def invalid_def true_def false_def)


lemma OclNot_not[simp]: "not (not X) = X"
  apply(rule ext,simp add: OclNot_def null_def invalid_def true_def false_def)
  apply(case_tac "X x", simp_all)
  apply(case_tac "a", simp_all)
  done

lemma OclNot_inject: " x y. not x = not y  x = y"
  by(subst OclNot_not[THEN sym], simp)

definition OclAnd :: "[('𝔄)Boolean, ('𝔄)Boolean]  ('𝔄)Boolean" (infixl "and" 30)
where     "X and Y   (λ τ . case X τ of
                          False                False
                        |          (case Y τ of
                                        False  False
                                      | _         )
                        |        (case Y τ of
                                        False  False
                                      |          
                                      | _         )
                        | True                 Y τ)"


text‹
  Note that @{term "not"} is \emph{not} defined as a strict function;
  proximity to lattice laws implies that we \emph{need} a definition
  of @{term "not"} that satisfies not(not(x))=x›.
›

text‹
  In textbook notation, the logical core constructs @{const
    "OclNot"} and @{const "OclAnd"} were represented as follows:
›
lemma textbook_OclNot:
     "I⟦not(X) τ =  (case I⟦X τ of       
                                 |        
                                 |  x    ¬ x )"
by(simp add: Sem_def OclNot_def)

lemma textbook_OclAnd:
     "I⟦X and Y τ = (case I⟦X τ of
                               (case I⟦Y τ of
                                                
                                          |   
                                          | True   
                                          | False   False)
                        |     (case I⟦Y τ of
                                                
                                          |   
                                          | True  
                                          | False   False)
                        | True  (case I⟦Y τ of
                                                
                                          |   
                                          | y   y)
                        | False    False )"
by(simp add: OclAnd_def Sem_def split: option.split bool.split)

definition OclOr :: "[('𝔄)Boolean, ('𝔄)Boolean]  ('𝔄)Boolean"            (infixl "or" 25)
where    "X or Y  not(not X and not Y)"

definition OclImplies :: "[('𝔄)Boolean, ('𝔄)Boolean]  ('𝔄)Boolean"       (infixl "implies" 25)
where    "X implies Y  not X or Y"

lemma cp_OclAnd:"(X and Y) τ = ((λ _. X τ) and (λ _. Y τ)) τ"
by(simp add: OclAnd_def)

lemma cp_OclOr:"((X::('𝔄)Boolean) or Y) τ = ((λ _. X τ) or (λ _. Y τ)) τ"
apply(simp add: OclOr_def)
apply(subst cp_OclNot[of "not (λ_. X τ) and not (λ_. Y τ)"])
apply(subst cp_OclAnd[of "not (λ_. X τ)" "not (λ_. Y τ)"])
by(simp add: cp_OclNot[symmetric] cp_OclAnd[symmetric] )


lemma cp_OclImplies:"(X implies Y) τ = ((λ _. X τ) implies (λ _. Y τ)) τ"
apply(simp add: OclImplies_def)
apply(subst cp_OclOr[of "not (λ_. X τ)" "(λ_. Y τ)"])
by(simp add: cp_OclNot[symmetric] cp_OclOr[symmetric] )

lemma OclAnd1[simp]: "(invalid and true) = invalid"
  by(rule ext,simp add: OclAnd_def null_def invalid_def true_def false_def bot_option_def)
lemma OclAnd2[simp]: "(invalid and false) = false"
  by(rule ext,simp add: OclAnd_def null_def invalid_def true_def false_def bot_option_def)
lemma OclAnd3[simp]: "(invalid and null) = invalid"
  by(rule ext,simp add: OclAnd_def null_def invalid_def true_def false_def bot_option_def
                        null_fun_def null_option_def)
lemma OclAnd4[simp]: "(invalid and invalid) = invalid"
  by(rule ext,simp add: OclAnd_def null_def invalid_def true_def false_def bot_option_def)

lemma OclAnd5[simp]: "(null and true) = null"
  by(rule ext,simp add: OclAnd_def null_def invalid_def true_def false_def bot_option_def
                        null_fun_def null_option_def)
lemma OclAnd6[simp]: "(null and false) = false"
  by(rule ext,simp add: OclAnd_def null_def invalid_def true_def false_def bot_option_def
                        null_fun_def null_option_def)
lemma OclAnd7[simp]: "(null and null) = null"
  by(rule ext,simp add: OclAnd_def null_def invalid_def true_def false_def bot_option_def
                        null_fun_def null_option_def)
lemma OclAnd8[simp]: "(null and invalid) = invalid"
  by(rule ext,simp add: OclAnd_def null_def invalid_def true_def false_def bot_option_def
                        null_fun_def null_option_def)

lemma OclAnd9[simp]: "(false and true) = false"
  by(rule ext,simp add: OclAnd_def null_def invalid_def true_def false_def)
lemma OclAnd10[simp]: "(false and false) = false"
  by(rule ext,simp add: OclAnd_def null_def invalid_def true_def false_def)
lemma OclAnd11[simp]: "(false and null) = false"
  by(rule ext,simp add: OclAnd_def null_def invalid_def true_def false_def)
lemma OclAnd12[simp]: "(false and invalid) = false"
  by(rule ext,simp add: OclAnd_def null_def invalid_def true_def false_def)

lemma OclAnd13[simp]: "(true and true) = true"
  by(rule ext,simp add: OclAnd_def null_def invalid_def true_def false_def)
lemma OclAnd14[simp]: "(true and false) = false"
  by(rule ext,simp add: OclAnd_def null_def invalid_def true_def false_def)
lemma OclAnd15[simp]: "(true and null) = null"
  by(rule ext,simp add: OclAnd_def null_def invalid_def true_def false_def bot_option_def
                        null_fun_def null_option_def)
lemma OclAnd16[simp]: "(true and invalid) = invalid"
  by(rule ext,simp add: OclAnd_def null_def invalid_def true_def false_def bot_option_def
                        null_fun_def null_option_def)

lemma OclAnd_idem[simp]: "(X and X) = X"
  apply(rule ext,simp add: OclAnd_def null_def invalid_def true_def false_def)
  apply(case_tac "X x", simp_all)
  apply(case_tac "a", simp_all)
  apply(case_tac "aa", simp_all)
  done

lemma OclAnd_commute: "(X and Y) = (Y and X)"
  by(rule ext,auto simp:true_def false_def OclAnd_def invalid_def
                   split: option.split option.split_asm
                          bool.split bool.split_asm)


lemma OclAnd_false1[simp]: "(false and X) = false"
  apply(rule ext, simp add: OclAnd_def)
  apply(auto simp:true_def false_def invalid_def
             split: option.split option.split_asm)
  done

lemma OclAnd_false2[simp]: "(X and false) = false"
  by(simp add: OclAnd_commute)


lemma OclAnd_true1[simp]: "(true and X) = X"
  apply(rule ext, simp add: OclAnd_def)
  apply(auto simp:true_def false_def invalid_def
             split: option.split option.split_asm)
  done

lemma OclAnd_true2[simp]: "(X and true) = X"
  by(simp add: OclAnd_commute)

lemma OclAnd_bot1[simp]: "τ. X τ  false τ  (bot and X) τ = bot τ"
  apply(simp add: OclAnd_def)
  apply(auto simp:true_def false_def bot_fun_def bot_option_def
             split: option.split option.split_asm)
done

lemma OclAnd_bot2[simp]: "τ. X τ  false τ  (X and bot) τ = bot τ"
  by(simp add: OclAnd_commute)

lemma OclAnd_null1[simp]: "τ. X τ  false τ  X τ  bot τ  (null and X) τ = null τ"
  apply(simp add: OclAnd_def)
  apply(auto simp:true_def false_def bot_fun_def bot_option_def null_fun_def null_option_def
             split: option.split option.split_asm)
done

lemma OclAnd_null2[simp]: "τ. X τ  false τ  X τ  bot τ  (X and null) τ = null τ"
  by(simp add: OclAnd_commute)

lemma OclAnd_assoc: "(X and (Y and Z)) = (X and Y and Z)"
  apply(rule ext, simp add: OclAnd_def)
  apply(auto simp:true_def false_def null_def invalid_def
             split: option.split option.split_asm
                    bool.split bool.split_asm)
done


lemma OclOr1[simp]: "(invalid or true) = true"
by(rule ext, simp add: OclOr_def OclNot_def OclAnd_def null_def invalid_def true_def false_def
                       bot_option_def)
lemma OclOr2[simp]: "(invalid or false) = invalid"
by(rule ext, simp add: OclOr_def OclNot_def OclAnd_def null_def invalid_def true_def false_def
                       bot_option_def)
lemma OclOr3[simp]: "(invalid or null) = invalid"
by(rule ext, simp add: OclOr_def OclNot_def OclAnd_def null_def invalid_def true_def false_def
                       bot_option_def null_fun_def null_option_def)
lemma OclOr4[simp]: "(invalid or invalid) = invalid"
by(rule ext, simp add: OclOr_def OclNot_def OclAnd_def null_def invalid_def true_def false_def
                       bot_option_def)

lemma OclOr5[simp]: "(null or true) = true"
by(rule ext, simp add: OclOr_def OclNot_def OclAnd_def null_def invalid_def true_def false_def
                       bot_option_def null_fun_def null_option_def)
lemma OclOr6[simp]: "(null or false) = null"
by(rule ext, simp add: OclOr_def OclNot_def OclAnd_def null_def invalid_def true_def false_def
                       bot_option_def null_fun_def null_option_def)
lemma OclOr7[simp]: "(null or null) = null"
by(rule ext, simp add: OclOr_def OclNot_def OclAnd_def null_def invalid_def true_def false_def
                       bot_option_def null_fun_def null_option_def)
lemma OclOr8[simp]: "(null or invalid) = invalid"
by(rule ext, simp add: OclOr_def OclNot_def OclAnd_def null_def invalid_def true_def false_def
                       bot_option_def null_fun_def null_option_def)

lemma OclOr_idem[simp]: "(X or X) = X"
  by(simp add: OclOr_def)

lemma OclOr_commute: "(X or Y) = (Y or X)"
  by(simp add: OclOr_def OclAnd_commute)

lemma OclOr_false1[simp]: "(false or Y) = Y"
  by(simp add: OclOr_def)

lemma OclOr_false2[simp]: "(Y or false) = Y"
  by(simp add: OclOr_def)

lemma OclOr_true1[simp]: "(true or Y) = true"
  by(simp add: OclOr_def)

lemma OclOr_true2: "(Y or true) = true"
  by(simp add: OclOr_def)

lemma OclOr_bot1[simp]: "τ. X τ  true τ  (bot or X) τ = bot τ"
  apply(simp add: OclOr_def OclAnd_def OclNot_def)
  apply(auto simp:true_def false_def bot_fun_def bot_option_def
             split: option.split option.split_asm)
done

lemma OclOr_bot2[simp]: "τ. X τ  true τ  (X or bot) τ = bot τ"
  by(simp add: OclOr_commute)

lemma OclOr_null1[simp]: "τ. X τ  true τ  X τ  bot τ  (null or X) τ = null τ"
  apply(simp add: OclOr_def OclAnd_def OclNot_def)
  apply(auto simp:true_def false_def bot_fun_def bot_option_def null_fun_def null_option_def
             split: option.split option.split_asm)
  apply (metis (full_types) bool.simps(3) bot_option_def null_is_valid null_option_def)
by (metis (full_types) bool.simps(3) option.distinct(1) option.sel)

lemma OclOr_null2[simp]: "τ. X τ  true τ  X τ  bot τ  (X or null) τ = null τ"
  by(simp add: OclOr_commute)

lemma OclOr_assoc: "(X or (Y or Z)) = (X or Y or Z)"
  by(simp add: OclOr_def OclAnd_assoc)

lemma deMorgan1: "not(X and Y) = ((not X) or (not Y))"
  by(simp add: OclOr_def)

lemma deMorgan2: "not(X or Y) = ((not X) and (not Y))"
  by(simp add: OclOr_def)

lemma OclImplies_true1[simp]:"(true implies X) = X"
  by(simp add: OclImplies_def)

lemma OclImplies_true2[simp]: "(X implies true) = true"
  by(simp add: OclImplies_def OclOr_true2)

lemma OclImplies_false1[simp]:"(false implies X) = true"
  by(simp add: OclImplies_def)

subsection‹A Standard Logical Calculus for OCL›

definition OclValid  :: "[('𝔄)st, ('𝔄)Boolean]  bool" ("(1(_)/  (_))" 50)
where     "τ  P  ((P τ) = true τ)"

syntax OclNonValid  :: "[('𝔄)st, ('𝔄)Boolean]  bool" ("(1(_)/ |≠ (_))" 50)

translations "τ |≠ P" == "¬(τ  P)" 

subsubsection‹Global vs. Local Judgements›
lemma transform1: "P = true  τ  P"
by(simp add: OclValid_def)


lemma transform1_rev: " τ. τ  P  P = true"
by(rule ext, auto simp: OclValid_def true_def)

lemma transform2: "(P = Q)  ((τ  P) = (τ  Q))"
by(auto simp: OclValid_def)

lemma transform2_rev: " τ. (τ  δ P)  (τ  δ Q)  (τ  P) = (τ  Q)  P = Q"
apply(rule ext,auto simp: OclValid_def true_def defined_def)
apply(erule_tac x=a in allE)
apply(erule_tac x=b in allE)
apply(auto simp: false_def true_def defined_def bot_Boolean_def null_Boolean_def
                 split: option.split_asm HOL.if_split_asm)
done

text‹However, certain properties (like transitivity) can not
       be \emph{transformed} from the global level to the local one,
       they have to be re-proven on the local level.›

lemma (*transform3:*)
assumes H : "P = true  Q = true"
shows "τ  P  τ  Q"
apply(simp add: OclValid_def)
apply(rule H[THEN fun_cong])
apply(rule ext)
oops

subsubsection‹Local Validity and Meta-logic›
text‹\label{sec:localVal}›

lemma foundation1[simp]: "τ  true"
by(auto simp: OclValid_def)

lemma foundation2[simp]: "¬(τ  false)"
by(auto simp: OclValid_def true_def false_def)

lemma foundation3[simp]: "¬(τ  invalid)"
by(auto simp: OclValid_def true_def false_def invalid_def bot_option_def)

lemma foundation4[simp]: "¬(τ  null)"
by(auto simp: OclValid_def true_def false_def null_def null_fun_def null_option_def bot_option_def)

lemma bool_split[simp]:
"(τ  (x  invalid))  (τ  (x  null))  (τ  (x  true))  (τ  (x  false))"
apply(insert bool_split_0[of x τ], auto)
apply(simp_all add: OclValid_def StrongEq_def true_def null_def invalid_def)
done

lemma defined_split:
"(τ  δ x) = ((¬(τ  (x  invalid)))  (¬ (τ  (x  null))))"
by(simp add:defined_def true_def false_def invalid_def null_def
               StrongEq_def OclValid_def bot_fun_def null_fun_def)

lemma valid_bool_split: "(τ  υ A) = ((τ  A  null)  (τ  A)   (τ  not A)) "
by(auto simp:valid_def true_def false_def invalid_def null_def OclNot_def
             StrongEq_def OclValid_def bot_fun_def bot_option_def null_option_def null_fun_def)

lemma defined_bool_split: "(τ  δ A) = ((τ  A)  (τ  not A))"
by(auto simp:defined_def true_def false_def invalid_def null_def OclNot_def
             StrongEq_def OclValid_def bot_fun_def bot_option_def null_option_def null_fun_def)



lemma foundation5:
"τ  (P and Q)  (τ  P)  (τ  Q)"
by(simp add: OclAnd_def OclValid_def true_def false_def defined_def
             split: option.split option.split_asm bool.split bool.split_asm)

lemma foundation6:
"τ  P  τ  δ P"
by(simp add: OclNot_def OclValid_def true_def false_def defined_def
                null_option_def null_fun_def bot_option_def bot_fun_def
             split: option.split option.split_asm)


lemma foundation7[simp]:
"(τ  not (δ x)) = (¬ (τ  δ x))"
by(simp add: OclNot_def OclValid_def true_def false_def defined_def
             split: option.split option.split_asm)

lemma foundation7'[simp]:
"(τ  not (υ x)) = (¬ (τ  υ x))"
by(simp add: OclNot_def OclValid_def true_def false_def valid_def
             split: option.split option.split_asm)


text‹
  Key theorem for the $\delta$-closure: either an expression is
  defined, or it can be replaced (substituted via StrongEq_L_subst2›;
  see below) by invalid› or null›. Strictness-reduction rules will
  usually reduce these substituted terms drastically.
›


lemma foundation8:
"(τ  δ x)  (τ  (x  invalid))  (τ  (x  null))"
proof -
  have 1 : "(τ  δ x)  (¬(τ  δ x))" by auto
  have 2 : "(¬(τ  δ x)) = ((τ  (x  invalid))  (τ  (x  null)))"
           by(simp only: defined_split, simp)
  show ?thesis by(insert 1, simp add:2)
qed


lemma foundation9:
"τ  δ x  (τ  not x) = (¬ (τ  x))"
apply(simp add: defined_split )
by(auto simp: OclNot_def null_fun_def null_option_def bot_option_def
                 OclValid_def invalid_def true_def null_def StrongEq_def)

lemma foundation9':
"τ  not x  ¬ (τ  x)"
by(auto simp: foundation6 foundation9)

lemma foundation9'':
"            τ  not x  τ  δ x"
by(metis OclNot3 OclNot_not OclValid_def cp_OclNot cp_defined defined4)

lemma foundation10:
"τ  δ x  τ  δ y  (τ  (x and y)) = ( (τ  x)  (τ  y))"
apply(simp add: defined_split)
by(auto simp: OclAnd_def OclValid_def invalid_def
              true_def null_def StrongEq_def null_fun_def null_option_def bot_option_def
        split:bool.split_asm)

lemma foundation10': "(τ  (A and B)) = ((τ  A)  (τ  B))" (* stronger than foundation !*)
by(auto dest:foundation5 simp:foundation6 foundation10)

lemma foundation11:
"τ  δ x   τ  δ y  (τ  (x or y)) = ( (τ  x)  (τ  y))"
apply(simp add: defined_split)
by(auto simp: OclNot_def OclOr_def OclAnd_def OclValid_def invalid_def
              true_def null_def StrongEq_def null_fun_def null_option_def bot_option_def
        split:bool.split_asm bool.split)



lemma foundation12:
"τ  δ x  (τ  (x implies y)) = ( (τ  x)  (τ  y))"
apply(simp add: defined_split)
by(auto simp: OclNot_def OclOr_def OclAnd_def OclImplies_def bot_option_def
              OclValid_def invalid_def true_def null_def StrongEq_def null_fun_def null_option_def
        split:bool.split_asm bool.split option.split_asm)

lemma foundation13:"(τ  A  true)    = (τ  A)"
by(auto simp: OclNot_def  OclValid_def invalid_def true_def null_def StrongEq_def
              split:bool.split_asm bool.split)

lemma foundation14:"(τ  A  false)   = (τ  not A)"
by(auto simp: OclNot_def  OclValid_def invalid_def false_def true_def null_def StrongEq_def
        split:bool.split_asm bool.split option.split)

lemma foundation15:"(τ  A  invalid) = (τ  not(υ A))"
by(auto simp: OclNot_def OclValid_def valid_def invalid_def false_def true_def null_def
              StrongEq_def bot_option_def null_fun_def null_option_def bot_option_def bot_fun_def
        split:bool.split_asm bool.split option.split)


(* ... and the usual rules on strictness, definedness propoagation, and cp ... *)
lemma foundation16: "τ  (δ X) = (X τ  bot  X τ  null)"
by(auto simp: OclValid_def defined_def false_def true_def  bot_fun_def null_fun_def
        split:if_split_asm)

lemma foundation16'': "¬(τ  (δ X)) = ((τ  (X  invalid))  (τ  (X  null)))"
apply(simp add: foundation16)
by(auto simp:defined_def false_def true_def  bot_fun_def null_fun_def OclValid_def StrongEq_def invalid_def)

(* correcter rule; the previous is deprecated *)
lemma foundation16': "(τ  (δ X)) = (X τ  invalid τ  X τ  null τ)"
apply(simp add:invalid_def null_def null_fun_def)
by(auto simp: OclValid_def defined_def false_def true_def  bot_fun_def null_fun_def
        split:if_split_asm)



lemma foundation18: "(τ  (υ X)) = (X τ  invalid τ)"
by(auto simp: OclValid_def valid_def false_def true_def bot_fun_def invalid_def
        split:if_split_asm)

(*legacy*)
lemma foundation18': "(τ  (υ X)) = (X τ  bot)"
by(auto simp: OclValid_def valid_def false_def true_def bot_fun_def
        split:if_split_asm)

lemma foundation18'': "(τ  (υ X) )=  (¬(τ  (X  invalid)))"
by(auto simp:foundation15)


lemma foundation20 : "τ  (δ X)  τ  υ X"
by(simp add: foundation18 foundation16 invalid_def)

lemma foundation21: "(not A  not B) = (A  B)"
by(rule ext, auto simp: OclNot_def StrongEq_def
                     split: bool.split_asm HOL.if_split_asm option.split)

lemma foundation22: "(τ  (X  Y)) = (X τ = Y τ)"
by(auto simp: StrongEq_def OclValid_def true_def)

lemma foundation23: "(τ  P) = (τ  (λ _ . P τ))"
by(auto simp: OclValid_def true_def)



lemma foundation24:"(τ  not(X  Y)) = (X τ  Y τ)"
by(simp add: StrongEq_def  OclValid_def OclNot_def true_def)

lemma foundation25: "τ  P  τ  (P or Q)"
by(simp add: OclOr_def OclNot_def OclAnd_def OclValid_def true_def)

lemma foundation25': "τ  Q  τ  (P or Q)"
by(subst OclOr_commute, simp add: foundation25)


lemma foundation26:
assumes defP: "τ  δ P"
assumes defQ: "τ  δ Q"
assumes H: "τ  (P or Q)"
assumes P: "τ  P  R"
assumes Q: "τ  Q  R"
shows "R"
by(insert H, subst (asm) foundation11[OF defP defQ], erule disjE, simp_all add: P Q)

lemma foundation27: "τ  A  (τ  A implies B) = (τ  B)" 
by (simp add: foundation12 foundation6)

lemma defined_not_I : "τ  δ (x)  τ  δ (not x)"
  by(auto simp: OclNot_def null_def invalid_def defined_def valid_def OclValid_def
                  true_def false_def bot_option_def null_option_def null_fun_def bot_fun_def
             split: option.split_asm HOL.if_split_asm)

lemma valid_not_I : "τ  υ (x)  τ  υ (not x)"
  by(auto simp: OclNot_def null_def invalid_def defined_def valid_def OclValid_def
                  true_def false_def bot_option_def null_option_def null_fun_def bot_fun_def
          split: option.split_asm option.split HOL.if_split_asm)

lemma defined_and_I : "τ  δ (x)   τ  δ (y)  τ  δ (x and y)"
  apply(simp add: OclAnd_def null_def invalid_def defined_def valid_def OclValid_def
                  true_def false_def bot_option_def null_option_def null_fun_def bot_fun_def
             split: option.split_asm HOL.if_split_asm)
  apply(auto simp: null_option_def split: bool.split)
  by(case_tac "ya",simp_all)

lemma valid_and_I :   "τ  υ (x)   τ  υ (y)  τ  υ (x and y)"
  apply(simp add: OclAnd_def null_def invalid_def defined_def valid_def OclValid_def
                  true_def false_def bot_option_def null_option_def null_fun_def bot_fun_def
             split: option.split_asm HOL.if_split_asm)
  by(auto simp: null_option_def split: option.split bool.split)

lemma defined_or_I : "τ  δ (x)   τ  δ (y)  τ  δ (x or y)"
by(simp add: OclOr_def defined_and_I defined_not_I)

lemma valid_or_I :   "τ  υ (x)   τ  υ (y)  τ  υ (x or y)"
by(simp add: OclOr_def valid_and_I valid_not_I)

subsubsection‹Local Judgements and Strong Equality›

lemma StrongEq_L_refl: "τ  (x  x)"
by(simp add: OclValid_def StrongEq_def)


lemma StrongEq_L_sym: "τ  (x  y)  τ  (y  x)"
by(simp add: StrongEq_sym)

lemma StrongEq_L_trans: "τ  (x  y)  τ  (y  z)  τ  (x  z)"
by(simp add: OclValid_def StrongEq_def true_def)



text‹In order to establish substitutivity (which does not
hold in general HOL formulas) we introduce the following
predicate that allows for a calculus of the necessary side-conditions.›
definition cp   :: "(('𝔄,) val  ('𝔄,) val)  bool"
where     "cp P  ( f.  X τ. P X τ = f (X τ) τ)"


text‹The rule of substitutivity in Featherweight OCL holds only
for context-passing expressions, \ie those that pass
the context τ› without changing it. Fortunately, all
operators of the OCL language satisfy this property
(but not all HOL operators).›

lemma StrongEq_L_subst1: " τ. cp P  τ  (x  y)  τ  (P x  P y)"
by(auto simp: OclValid_def StrongEq_def true_def cp_def)

lemma StrongEq_L_subst2:
" τ.  cp P  τ  (x  y)  τ  (P x)  τ  (P y)"
by(auto simp: OclValid_def StrongEq_def true_def cp_def)

lemma StrongEq_L_subst2_rev: "τ  y  x  cp P  τ  P x  τ  P y"
apply(erule StrongEq_L_subst2)
apply(erule StrongEq_L_sym)  
by assumption

lemma  StrongEq_L_subst3:
assumes cp: "cp P"
and     eq: "τ  (x  y)"
shows       "(τ  P x) = (τ  P y)"
apply(rule iffI)
apply(rule StrongEq_L_subst2[OF cp,OF eq],simp)
apply(rule StrongEq_L_subst2[OF cp,OF eq[THEN StrongEq_L_sym]],simp)
done

lemma  StrongEq_L_subst3_rev:
assumes eq: "τ  (x  y)" 
and     cp: "cp P"
shows       "(τ  P x) = (τ  P y)"
by(insert cp, erule StrongEq_L_subst3, rule eq)

lemma  StrongEq_L_subst4_rev:
assumes eq: "τ  (x  y)" 
and     cp: "cp P"
shows       "(¬(τ  P x)) = (¬(τ  P y))"
thm arg_cong[of _ _ "Not"]
apply(rule arg_cong[of _ _ "Not"])
by(insert cp, erule StrongEq_L_subst3, rule eq)

lemma cpI1:
"( X τ. f X τ = f(λ_. X τ) τ)  cp P  cp(λX. f (P X))"
apply(auto simp: true_def cp_def)
apply(rule exI, (rule allI)+)
by(erule_tac x="P X" in allE, auto)

lemma cpI2:
"( X Y τ. f X Y τ = f(λ_. X τ)(λ_. Y τ) τ) 
 cp P  cp Q  cp(λX. f (P X) (Q X))"
apply(auto simp: true_def cp_def)
apply(rule exI, (rule allI)+)
by(erule_tac x="P X" in allE, auto)

lemma cpI3:
"( X Y Z τ. f X Y Z τ = f(λ_. X τ)(λ_. Y τ)(λ_. Z τ) τ) 
 cp P  cp Q  cp R  cp(λX. f (P X) (Q X) (R X))"
apply(auto simp: cp_def)
apply(rule exI, (rule allI)+)
by(erule_tac x="P X" in allE, auto)

lemma cpI4:
"( W X Y Z τ. f W X Y Z τ = f(λ_. W τ)(λ_. X τ)(λ_. Y τ)(λ_. Z τ) τ) 
 cp P  cp Q  cp R  cp S  cp(λX. f (P X) (Q X) (R X) (S X))"
apply(auto simp: cp_def)
apply(rule exI, (rule allI)+)
by(erule_tac x="P X" in allE, auto)

lemma cpI5:
"( V W X Y Z τ. f V W X Y Z τ = f(λ_. V τ) (λ_. W τ)(λ_. X τ)(λ_. Y τ)(λ_. Z τ) τ) 
 cp N  cp P  cp Q  cp R  cp S  cp(λX. f (N X) (P X) (Q X) (R X) (S X))"
apply(auto simp: cp_def)
apply(rule exI, (rule allI)+)
by(erule_tac x="N X" in allE, auto)


lemma cp_const : "cp(λ_. c)"
  by (simp add: cp_def, fast)

lemma cp_id :     "cp(λX. X)"
  by (simp add: cp_def, fast)

text_raw‹\isatagafp›
 
lemmas cp_intro[intro!,simp,code_unfold] =
       cp_const
       cp_id
       cp_defined[THEN allI[THEN allI[THEN cpI1], of defined]]
       cp_valid[THEN allI[THEN allI[THEN cpI1], of valid]]
       cp_OclNot[THEN allI[THEN allI[THEN cpI1], of not]]
       cp_OclAnd[THEN allI[THEN allI[THEN allI[THEN cpI2]], of "(and)"]]
       cp_OclOr[THEN allI[THEN allI[THEN allI[THEN cpI2]], of "(or)"]]
       cp_OclImplies[THEN allI[THEN allI[THEN allI[THEN cpI2]], of "(implies)"]]
       cp_StrongEq[THEN allI[THEN allI[THEN allI[THEN cpI2]],
                   of "StrongEq"]]

text_raw‹\endisatagafp›
       
       
subsection‹OCL's if then else endif›

definition OclIf :: "[('𝔄)Boolean , ('𝔄,::null) val, ('𝔄,) val]  ('𝔄,) val"
                     ("if (_) then (_) else (_) endif" [10,10,10]50)
where "(if C then B1 else B2 endif) = (λ τ. if (δ C) τ = true τ
                                           then (if (C τ) = true τ
                                                then B1 τ
                                                else B2 τ)
                                           else invalid τ)"


lemma cp_OclIf:"((if C then B1 else B2 endif) τ =
                  (if (λ _. C τ) then (λ _. B1 τ) else (λ _. B2 τ) endif) τ)"
by(simp only: OclIf_def, subst cp_defined, rule refl)
text_raw‹\isatagafp›

lemmas cp_intro'[intro!,simp,code_unfold] =
       cp_intro
       cp_OclIf[THEN allI[THEN allI[THEN allI[THEN allI[THEN cpI3]]], of "OclIf"]]
text_raw‹\endisatagafp›

lemma OclIf_invalid [simp]: "(if invalid then B1 else B2 endif) = invalid"
by(rule ext, auto simp: OclIf_def)

lemma OclIf_null [simp]: "(if null then B1 else B2 endif) = invalid"
by(rule ext, auto simp: OclIf_def)

lemma OclIf_true [simp]: "(if true then B1 else B2 endif) = B1"
by(rule ext, auto simp: OclIf_def)

lemma OclIf_true' [simp]: "τ  P  (if P then B1 else B2 endif)τ = B1 τ"
apply(subst cp_OclIf,auto simp: OclValid_def)
by(simp add:cp_OclIf[symmetric])

lemma OclIf_true'' [simp]: "τ  P  τ  (if P then B1 else B2 endif)  B1"
by(subst OclValid_def, simp add: StrongEq_def true_def)

lemma OclIf_false [simp]: "(if false then B1 else B2 endif) = B2"
by(rule ext, auto simp: OclIf_def)

lemma OclIf_false' [simp]: "τ  not P  (if P then B1 else B2 endif)τ = B2 τ"
apply(subst cp_OclIf)
apply(auto simp: foundation14[symmetric] foundation22)
by(auto simp: cp_OclIf[symmetric])


lemma OclIf_idem1[simp]:"(if δ X then A else A endif) = A"
by(rule ext, auto simp: OclIf_def)

lemma OclIf_idem2[simp]:"(if υ X then A else A endif) = A"
by(rule ext, auto simp: OclIf_def)

lemma OclNot_if[simp]:
"not(if P then C else E endif) = (if P then not C else not E endif)"
  (* non-trivial but elementary *)
  apply(rule OclNot_inject, simp)
  apply(rule ext)
  apply(subst cp_OclNot, simp add: OclIf_def)
  apply(subst cp_OclNot[symmetric])+
by simp


       
subsection‹Fundamental Predicates on Basic Types: Strict (Referential) Equality›

text‹
  In contrast to logical equality, the OCL standard defines an equality operation
  which we call ``strict referential equality''. It behaves differently for all
  types---on value types, it is basically a strict version of strong equality, 
  for defined values it behaves identical. But on object types it will compare 
  their references within the store. We  introduce strict referential equality 
  as an \emph{overloaded} concept and will handle it for
  each type instance individually.
›
consts StrictRefEq :: "[('𝔄,'a)val,('𝔄,'a)val]  ('𝔄)Boolean" (infixl "" 30)

text‹with {term "not"} we can express the notation:›

syntax
  "notequal"        :: "('𝔄)Boolean  ('𝔄)Boolean  ('𝔄)Boolean"   (infix "<>" 40)
translations
  "a <> b" == "CONST OclNot(a  b)"
       
text‹We will define instances of this equality in a case-by-case basis.›       
       
subsection‹Laws to Establish Definedness (\texorpdfstring{$\delta$}{d}-closure)›

text‹For the logical connectives, we have --- beyond
@{thm foundation6} --- the following facts:›
lemma OclNot_defargs:
"τ  (not P)  τ  δ P"
by(auto simp: OclNot_def OclValid_def true_def invalid_def defined_def false_def
                 bot_fun_def bot_option_def null_fun_def null_option_def
        split: bool.split_asm HOL.if_split_asm option.split option.split_asm)


lemma OclNot_contrapos_nn:
 assumes A: "τ  δ A"
 assumes B: "τ  not B"
 assumes C: "τ  A  τ  B"
 shows      "τ  not A"
proof -
 have D : "τ  δ B" by(rule B[THEN OclNot_defargs])
 show ?thesis 
    apply(insert B,simp add: A D foundation9)
    by(erule contrapos_nn, auto intro: C)
qed


subsection‹A Side-calculus for Constant Terms›

definition "const X   τ τ'. X τ = X τ'"

lemma const_charn: "const X  X τ = X τ'"
by(auto simp: const_def)

lemma const_subst:
 assumes const_X: "const X"
     and const_Y: "const Y"
     and eq :     "X τ = Y τ"
     and cp_P:    "cp P"
     and pp :     "P Y τ = P Y τ'"
   shows "P X τ = P X τ'"
proof -
   have A: "Y. P Y τ = P (λ_. Y τ) τ"
      apply(insert cp_P, unfold cp_def)
      apply(elim exE, erule_tac x=Y in allE', erule_tac x=τ in allE)
      apply(erule_tac x="(λ_. Y τ)" in allE, erule_tac x=τ in allE)
      by simp
   have B: "Y. P Y τ' = P (λ_. Y τ') τ'"
      apply(insert cp_P, unfold cp_def)
      apply(elim exE, erule_tac x=Y in allE', erule_tac x=τ' in allE)
      apply(erule_tac x="(λ_. Y τ')" in allE, erule_tac x=τ' in allE)
      by simp
   have C: "X τ' = Y τ'"
      apply(rule trans, subst const_charn[OF const_X],rule eq)
      by(rule const_charn[OF const_Y])
   show ?thesis
      apply(subst A, subst B, simp add: eq C)
      apply(subst A[symmetric],subst B[symmetric])
      by(simp add:pp)
qed


lemma const_imply2 :
 assumes "τ τ'. P τ = P τ'  Q τ = Q τ'"
 shows "const P  const Q"
by(simp add: const_def, insert assms, blast)

lemma const_imply3 :
 assumes "τ τ'. P τ = P τ'  Q τ = Q τ'  R τ = R τ'"
 shows "const P  const Q  const R"
by(simp add: const_def, insert assms, blast)

lemma const_imply4 :
 assumes "τ τ'. P τ = P τ'  Q τ = Q τ'  R τ = R τ'  S τ = S τ'"
 shows "const P  const Q  const R  const S"
by(simp add: const_def, insert assms, blast)

lemma const_lam : "const (λ_. e)"
by(simp add: const_def)


lemma const_true[simp] : "const true"
by(simp add: const_def true_def)

lemma const_false[simp] : "const false"
by(simp add: const_def false_def)

lemma const_null[simp] : "const null"
by(simp add: const_def null_fun_def)

lemma const_invalid [simp]: "const invalid"
by(simp add: const_def invalid_def)

lemma const_bot[simp] : "const bot"
by(simp add: const_def bot_fun_def)



lemma const_defined :
 assumes "const X"
 shows   "const (δ X)"
by(rule const_imply2[OF _ assms],
   simp add: defined_def false_def true_def bot_fun_def bot_option_def null_fun_def null_option_def)

lemma const_valid :
 assumes "const X"
 shows   "const (υ X)"
by(rule const_imply2[OF _ assms],
   simp add: valid_def false_def true_def bot_fun_def null_fun_def assms)


lemma const_OclAnd :
  assumes "const X"
  assumes "const X'"
  shows   "const (X and X')"
by(rule const_imply3[OF _ assms], subst (1 2) cp_OclAnd, simp add: assms OclAnd_def)


lemma const_OclNot :
    assumes "const X"
    shows   "const (not X)"
by(rule const_imply2[OF _ assms],subst cp_OclNot,simp add: assms OclNot_def)

lemma const_OclOr :
  assumes "const X"
  assumes "const X'"
  shows   "const (X or X')"
by(simp add: assms OclOr_def const_OclNot const_OclAnd)

lemma const_OclImplies :
  assumes "const X"
  assumes "const X'"
  shows   "const (X implies X')"
by(simp add: assms OclImplies_def const_OclNot const_OclOr)

lemma const_StrongEq:
  assumes "const X"
  assumes "const X'"
  shows   "const(X  X')"
  apply(simp only: StrongEq_def const_def, intro allI)
  apply(subst assms(1)[THEN const_charn])
  apply(subst assms(2)[THEN const_charn])
  by simp
  
  
lemma const_OclIf :
  assumes "const B"
      and "const C1"
      and "const C2"
    shows "const (if B then C1 else C2 endif)"
 apply(rule const_imply4[OF _ assms],
       subst (1 2) cp_OclIf, simp only: OclIf_def cp_defined[symmetric])
 apply(simp add: const_defined[OF assms(1), simplified const_def, THEN spec, THEN spec]
                 const_true[simplified const_def, THEN spec, THEN spec]
                 assms[simplified const_def, THEN spec, THEN spec]
                 const_invalid[simplified const_def, THEN spec, THEN spec])
by (metis (no_types) bot_fun_def OclValid_def const_def const_true defined_def 
                 foundation16[THEN iffD1]  null_fun_def)

       

lemma const_OclValid1:
 assumes "const x"
 shows   "(τ  δ x) = (τ'  δ x)"
 apply(simp add: OclValid_def)
 apply(subst const_defined[OF assms, THEN const_charn])
 by(simp add: true_def)

lemma const_OclValid2:
 assumes "const x"
 shows   "(τ  υ x) = (τ'  υ x)"
 apply(simp add: OclValid_def)
 apply(subst const_valid[OF assms, THEN const_charn])
 by(simp add: true_def)


lemma const_HOL_if : "const C  const D  const F  const (λτ. if C τ then D τ else F τ)"
      by(auto simp: const_def)
lemma const_HOL_and: "const C  const D  const (λτ. C τ  D τ)"
      by(auto simp: const_def)
lemma const_HOL_eq : "const C  const D  const (λτ. C τ = D τ)" 
      apply(auto simp: const_def)
      apply(erule_tac x=τ in allE)
      apply(erule_tac x=τ in allE)
      apply(erule_tac x=τ' in allE)
      apply(erule_tac x=τ' in allE)
      apply simp
      apply(erule_tac x=τ in allE)
      apply(erule_tac x=τ in allE)
      apply(erule_tac x=τ' in allE)
      apply(erule_tac x=τ' in allE)
      by simp


lemmas const_ss = const_bot const_null  const_invalid  const_false  const_true  const_lam
                  const_defined const_valid const_StrongEq const_OclNot const_OclAnd
                  const_OclOr const_OclImplies const_OclIf
                  const_HOL_if const_HOL_and const_HOL_eq
               

text‹Miscellaneous: Overloading the syntax of ``bottom''›

notation bot ("")

end