Theory UML_Sequence

(*****************************************************************************
 * Featherweight-OCL --- A Formal Semantics for UML-OCL Version OCL 2.5
 *                       for the OMG Standard.
 *                       http://www.brucker.ch/projects/hol-testgen/
 *
 * UML_Sequence.thy --- Library definitions.
 * This file is part of HOL-TestGen.
 *
 * Copyright (c) 2012-2015 Université Paris-Saclay, Univ. Paris-Sud, France
 *               2013-2015 IRT SystemX, France
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are
 * met:
 *
 *     * Redistributions of source code must retain the above copyright
 *       notice, this list of conditions and the following disclaimer.
 *
 *     * Redistributions in binary form must reproduce the above
 *       copyright notice, this list of conditions and the following
 *       disclaimer in the documentation and/or other materials provided
 *       with the distribution.
 *
 *     * Neither the name of the copyright holders nor the names of its
 *       contributors may be used to endorse or promote products derived
 *       from this software without specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
 * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
 * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
 * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
 * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
 * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
 * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
 * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
 * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 ******************************************************************************)


theory  UML_Sequence
imports "../basic_types/UML_Boolean"
        "../basic_types/UML_Integer"
begin

no_notation None ("⊥")
section‹Collection Type Sequence: Operations›

subsection‹Basic Properties of the Sequence Type›

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

lemma Sequence_inv_lemma: "τ ⊨ (δ X) ⟹ ∀x∈set ⌈⌈Rep_Sequencebase (X τ)⌉⌉. x ≠ bot"
apply(insert Rep_Sequencebase [of "X τ"], simp)
apply(auto simp: OclValid_def defined_def false_def true_def cp_def
                 bot_fun_def bot_Sequencebase_def null_Sequencebase_def null_fun_def
           split:if_split_asm)
 apply(erule contrapos_pp [of "Rep_Sequencebase (X τ) = bot"])
 apply(subst Abs_Sequencebase_inject[symmetric], rule Rep_Sequencebase, simp)
 apply(simp add: Rep_Sequencebase_inverse bot_Sequencebase_def bot_option_def)
apply(erule contrapos_pp [of "Rep_Sequencebase (X τ) = null"])
apply(subst Abs_Sequencebase_inject[symmetric], rule Rep_Sequencebase, simp)
apply(simp add: Rep_Sequencebase_inverse  null_option_def)
by (simp add: bot_option_def)

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

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

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

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

text‹Property proof in terms of @{term "profile_binStrongEq_v_v"}›
interpretation  StrictRefEqSeq : profile_binStrongEq_v_v "λ x y. (x::('𝔄,'α::null)Sequence) ≐ y" 
                by unfold_locales (auto simp:  StrictRefEqSeq)



subsection‹Constants: mtSequence›
definition mtSequence ::"('𝔄,'α::null) Sequence"  ("Sequence{}")
where     "Sequence{} ≡ (λ τ.  Abs_Sequencebase ⌊⌊[]::'α list⌋⌋ )"


lemma mtSequence_defined[simp,code_unfold]:"δ(Sequence{}) = true"
apply(rule ext, auto simp: mtSequence_def defined_def null_Sequencebase_def
                           bot_Sequencebase_def bot_fun_def null_fun_def)
by(simp_all add: Abs_Sequencebase_inject bot_option_def null_option_def)

lemma mtSequence_valid[simp,code_unfold]:"υ(Sequence{}) = true"
apply(rule ext,auto simp: mtSequence_def valid_def null_Sequencebase_def
                          bot_Sequencebase_def bot_fun_def null_fun_def)
by(simp_all add: Abs_Sequencebase_inject bot_option_def null_option_def)

lemma mtSequence_rep_set: "⌈⌈Rep_Sequencebase (Sequence{} τ)⌉⌉ = []"
 apply(simp add: mtSequence_def, subst Abs_Sequencebase_inverse)
by(simp add: bot_option_def)+

text_raw‹\isatagafp›

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

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

text_raw‹\endisatagafp›


subsection‹Definition: Prepend›
definition OclPrepend   :: "[('𝔄,'α::null) Sequence,('𝔄,'α) val] ⇒ ('𝔄,'α) Sequence"
where     "OclPrepend x y = (λ τ. if (δ x) τ = true τ ∧ (υ y) τ = true τ
                                    then Abs_Sequencebase ⌊⌊ (y τ)#⌈⌈Rep_Sequencebase (x τ)⌉⌉ ⌋⌋
                                    else invalid τ )"
notation   OclPrepend   ("_->prependSeq'(_')")

interpretation OclPrepend:profile_bind_v OclPrepend "λx y. Abs_Sequencebase⌊⌊y#⌈⌈Rep_Sequencebase x⌉⌉⌋⌋"
proof -  
 have A : "⋀x y. x ≠ bot ⟹ x ≠ null ⟹  y ≠ bot  ⟹
           ⌊⌊y#⌈⌈Rep_Sequencebase x⌉⌉⌋⌋ ∈ {X. X = bot ∨ X = null ∨ (∀x∈set ⌈⌈X⌉⌉. x ≠ bot)}"
          by(auto intro!:Sequence_inv_lemma[simplified OclValid_def 
                         defined_def false_def true_def null_fun_def bot_fun_def])  
                                       
         show "profile_bind_v OclPrepend (λx y. Abs_Sequencebase ⌊⌊y#⌈⌈Rep_Sequencebase x⌉⌉⌋⌋)"
         apply unfold_locales  
          apply(auto simp:OclPrepend_def bot_option_def null_option_def null_Sequencebase_def 
               bot_Sequencebase_def)
          apply(erule_tac Q="Abs_Sequencebase ⌊⌊y#⌈⌈Rep_Sequencebase x⌉⌉⌋⌋ = Abs_Sequencebase None" 
                in contrapos_pp)
          apply(subst Abs_Sequencebase_inject [OF A])
             apply(simp_all add:  null_Sequencebase_def bot_Sequencebase_def bot_option_def)
         apply(erule_tac Q="Abs_Sequencebase⌊⌊y#⌈⌈Rep_Sequencebase x⌉⌉⌋⌋ = Abs_Sequencebase ⌊None⌋" 
               in contrapos_pp)
         apply(subst Abs_Sequencebase_inject[OF A])
            apply(simp_all add:  null_Sequencebase_def bot_Sequencebase_def 
                                 bot_option_def null_option_def)
         done
qed
                
syntax
  "_OclFinsequence" :: "args => ('𝔄,'a::null) Sequence"    ("Sequence{(_)}")
translations
  "Sequence{x, xs}" == "CONST OclPrepend (Sequence{xs}) x"
  "Sequence{x}"     == "CONST OclPrepend (Sequence{}) x "

subsection‹Definition: Including›

definition OclIncluding   :: "[('𝔄,'α::null) Sequence,('𝔄,'α) val] ⇒ ('𝔄,'α) Sequence"
where     "OclIncluding x y = (λ τ. if (δ x) τ = true τ ∧ (υ y) τ = true τ
                                    then Abs_Sequencebase ⌊⌊ ⌈⌈Rep_Sequencebase (x τ)⌉⌉  @ [y τ] ⌋⌋
                                    else invalid τ )"
notation   OclIncluding   ("_->includingSeq'(_')")

interpretation OclIncluding : 
               profile_bind_v OclIncluding "λx y. Abs_Sequencebase⌊⌊⌈⌈Rep_Sequencebase x⌉⌉ @ [y]⌋⌋"
proof -  
 have A : "⋀x y. x ≠ bot ⟹ x ≠ null ⟹  y ≠ bot  ⟹
           ⌊⌊⌈⌈Rep_Sequencebase x⌉⌉ @ [y]⌋⌋ ∈ {X. X = bot ∨ X = null ∨ (∀x∈set ⌈⌈X⌉⌉. x ≠ bot)}"
          by(auto intro!:Sequence_inv_lemma[simplified OclValid_def 
                         defined_def false_def true_def null_fun_def bot_fun_def])  
                                       
         show "profile_bind_v OclIncluding (λx y. Abs_Sequencebase ⌊⌊⌈⌈Rep_Sequencebase x⌉⌉ @ [y]⌋⌋)"
         apply unfold_locales  
          apply(auto simp:OclIncluding_def bot_option_def null_option_def null_Sequencebase_def 
               bot_Sequencebase_def)
          apply(erule_tac Q="Abs_Sequencebase ⌊⌊⌈⌈Rep_Sequencebase x⌉⌉ @ [y]⌋⌋ = Abs_Sequencebase None" 
                in contrapos_pp)
          apply(subst Abs_Sequencebase_inject [OF A])
             apply(simp_all add:  null_Sequencebase_def bot_Sequencebase_def bot_option_def)
         apply(erule_tac Q="Abs_Sequencebase⌊⌊⌈⌈Rep_Sequencebase x⌉⌉ @ [y]⌋⌋ = Abs_Sequencebase ⌊None⌋" 
               in contrapos_pp)
         apply(subst Abs_Sequencebase_inject[OF A])
            apply(simp_all add:  null_Sequencebase_def bot_Sequencebase_def bot_option_def null_option_def)
         done
qed

lemma [simp,code_unfold] : "(Sequence{}->includingSeq(a)) = (Sequence{}->prependSeq(a))"
  apply(simp add: OclIncluding_def OclPrepend_def mtSequence_def)
  apply(subst (1 2) Abs_Sequencebase_inverse, simp)
by(metis drop.simps append_Nil)

lemma [simp,code_unfold] : "((S->prependSeq(a))->includingSeq(b)) = ((S->includingSeq(b))->prependSeq(a))"
 proof -
  have A: "⋀S b τ. S ≠ ⊥ ⟹ S ≠ null ⟹ b ≠ ⊥  ⟹
                   ⌊⌊⌈⌈Rep_Sequencebase S⌉⌉ @ [b]⌋⌋ ∈ {X. X = bot ∨ X = null ∨ (∀x∈set ⌈⌈X⌉⌉. x ≠ ⊥)}"
           by(auto intro!:Sequence_inv_lemma[simplified OclValid_def 
                                        defined_def false_def true_def null_fun_def bot_fun_def])          
  have B: "⋀S a τ. S ≠ ⊥ ⟹ S ≠ null ⟹ a ≠ ⊥  ⟹
                   ⌊⌊a # ⌈⌈Rep_Sequencebase S⌉⌉⌋⌋ ∈ {X. X = bot ∨ X = null ∨ (∀x∈set ⌈⌈X⌉⌉. x ≠ ⊥)}"
           by(auto intro!:Sequence_inv_lemma[simplified OclValid_def 
                                        defined_def false_def true_def null_fun_def bot_fun_def])          
 show ?thesis
  apply(simp add: OclIncluding_def OclPrepend_def mtSequence_def, rule ext)
  apply(subst (2 5) cp_defined, simp split:)
  apply(intro conjI impI)
        apply(subst Abs_Sequencebase_inverse[OF B],
              (simp add: foundation16[simplified OclValid_def] foundation18'[simplified OclValid_def])+)
        apply(subst Abs_Sequencebase_inverse[OF A],
              (simp add: foundation16[simplified OclValid_def] foundation18'[simplified OclValid_def])+)
       apply(simp add: OclIncluding.def_body)
      apply (metis OclValid_def foundation16 invalid_def)
     apply (metis (no_types) OclPrepend.def_body' OclValid_def foundation16)
 by (metis OclValid_def foundation16 invalid_def)+
qed

subsection‹Definition: Excluding›
definition OclExcluding   :: "[('𝔄,'α::null) Sequence,('𝔄,'α) val] ⇒ ('𝔄,'α) Sequence"
where     "OclExcluding x y = (λ τ. if (δ x) τ = true τ ∧ (υ y) τ = true τ
                                    then Abs_Sequencebase ⌊⌊ filter (λx. x = y τ)
                                                                   ⌈⌈Rep_Sequencebase (x τ)⌉⌉⌋⌋
                                    else invalid τ )"
notation   OclExcluding   ("_->excludingSeq'(_')")

interpretation OclExcluding:profile_bind_v OclExcluding 
                          "λx y. Abs_Sequencebase ⌊⌊ filter (λx. x = y) ⌈⌈Rep_Sequencebase (x)⌉⌉⌋⌋"
proof -
    show "profile_bind_v OclExcluding (λx y. Abs_Sequencebase ⌊⌊[x←⌈⌈Rep_Sequencebase x⌉⌉ . x = y]⌋⌋)"
         apply unfold_locales  
         apply(auto simp:OclExcluding_def bot_option_def null_option_def  
                         null_Sequencebase_def bot_Sequencebase_def)
         apply(subst (asm) Abs_Sequencebase_inject,
               simp_all add: null_Sequencebase_def bot_Sequencebase_def bot_option_def null_option_def)+
   done
qed

subsection‹Definition: Append›
text‹Identical to OclIncluding.›
definition OclAppend   :: "[('𝔄,'α::null) Sequence,('𝔄,'α) val] ⇒ ('𝔄,'α) Sequence"
where     "OclAppend = OclIncluding"
notation   OclAppend   ("_->appendSeq'(_')")

interpretation OclAppend : 
               profile_bind_v OclAppend "λx y. Abs_Sequencebase⌊⌊⌈⌈Rep_Sequencebase x⌉⌉ @ [y]⌋⌋"
         apply unfold_locales
 by(auto simp: OclAppend_def bin_def bin'_def
               OclIncluding.def_scheme OclIncluding.def_body)

subsection‹Definition: Union›
definition OclUnion   :: "[('𝔄,'α::null) Sequence,('𝔄,'α) Sequence] ⇒ ('𝔄,'α) Sequence"
where     "OclUnion x y = (λ τ. if (δ x) τ = true τ ∧ (δ y) τ = true τ
                                then Abs_Sequencebase ⌊⌊ ⌈⌈Rep_Sequencebase (x τ)⌉⌉ @
                                                        ⌈⌈Rep_Sequencebase (y τ)⌉⌉⌋⌋
                                else invalid τ )"
notation   OclUnion   ("_->unionSeq'(_')")

interpretation OclUnion : 
               profile_bind_d OclUnion "λx y. Abs_Sequencebase⌊⌊⌈⌈Rep_Sequencebase x⌉⌉ @ ⌈⌈Rep_Sequencebase y⌉⌉⌋⌋"
proof -  
   have A : "⋀x y. x ≠ ⊥ ⟹  x ≠ null ⟹ ∀x∈set ⌈⌈Rep_Sequencebase x⌉⌉. x ≠ ⊥ " 
            apply(rule Sequence_inv_lemma[of τ])
            by(simp add: defined_def OclValid_def bot_fun_def null_fun_def false_def true_def)   
   show "profile_bind_d OclUnion (λx y. Abs_Sequencebase⌊⌊⌈⌈Rep_Sequencebase x⌉⌉@⌈⌈Rep_Sequencebase y⌉⌉⌋⌋)"
   apply unfold_locales 
   apply(auto simp:OclUnion_def bot_option_def null_option_def 
                   null_Sequencebase_def bot_Sequencebase_def)
   by(subst (asm) Abs_Sequencebase_inject,
      simp_all add: bot_option_def null_option_def  Set.ball_Un A null_Sequencebase_def bot_Sequencebase_def)+
qed

subsection‹Definition: At›
definition OclAt   :: "[('𝔄,'α::null) Sequence,('𝔄) Integer] ⇒ ('𝔄,'α) val"
where     "OclAt x y = (λ τ. if (δ x) τ = true τ ∧ (δ y) τ = true τ
                             then if  1 ≤ ⌈⌈y τ⌉⌉ ∧  ⌈⌈y τ⌉⌉ ≤ length⌈⌈Rep_Sequencebase (x τ)⌉⌉ 
                                  then ⌈⌈Rep_Sequencebase (x τ)⌉⌉ ! (nat ⌈⌈y τ⌉⌉ - 1) 
                                  else invalid τ
                             else invalid τ )"
notation   OclAt ("_->atSeq'(_')")
(*TODO Locale - Equivalent*)  


subsection‹Definition: First›
definition OclFirst   :: "[('𝔄,'α::null) Sequence] ⇒ ('𝔄,'α) val"
where     "OclFirst x = (λ τ. if (δ x) τ = true τ then
                                case ⌈⌈Rep_Sequencebase (x τ)⌉⌉ of [] ⇒ invalid τ
                                                               | x # _ ⇒ x
                              else invalid τ )"
notation   OclFirst   ("_->firstSeq'(_')")
(*TODO Locale - Equivalent*)  


subsection‹Definition: Last›
definition OclLast   :: "[('𝔄,'α::null) Sequence] ⇒ ('𝔄,'α) val"
where     "OclLast x = (λ τ. if (δ x) τ = true τ then
                               if ⌈⌈Rep_Sequencebase (x τ)⌉⌉ = [] then
                                 invalid τ
                               else
                                 last ⌈⌈Rep_Sequencebase (x τ)⌉⌉
                             else invalid τ )"
notation   OclLast   ("_->lastSeq'(_')")
(*TODO Locale - Equivalent*)  

subsection‹Definition: Iterate›

definition OclIterate :: "[('𝔄,'α::null) Sequence,('𝔄,'β::null)val,
                           ('𝔄,'α)val⇒('𝔄,'β)val⇒('𝔄,'β)val] ⇒ ('𝔄,'β)val"
where     "OclIterate S A F = (λ τ. if (δ S) τ = true τ ∧ (υ A) τ = true τ 
                                    then (foldr (F) (map (λa τ. a) ⌈⌈Rep_Sequencebase (S τ)⌉⌉))(A)τ
                                    else ⊥)"
syntax  
  "_OclIterateSeq"  :: "[('𝔄,'α::null) Sequence, idt, idt, 'α, 'β] => ('𝔄,'γ)val"
                        ("_ ->iterateSeq'(_;_=_ | _')" (*[71,100,70]50*))
translations
  "X->iterateSeq(a; x = A | P)" == "CONST OclIterate X A (%a. (% x. P))"

(*TODO Locale - Equivalent*)  

  
  
subsection‹Definition: Forall›
definition OclForall     :: "[('𝔄,'α::null) Sequence,('𝔄,'α)val⇒('𝔄)Boolean] ⇒ '𝔄 Boolean"
where     "OclForall S P = (S->iterateSeq(b; x = true | x and (P b)))"

syntax
  "_OclForallSeq" :: "[('𝔄,'α::null) Sequence,id,('𝔄)Boolean] ⇒ '𝔄 Boolean"    ("(_)->forAllSeq'(_|_')")
translations
  "X->forAllSeq(x | P)" == "CONST UML_Sequence.OclForall X (%x. P)"

(*TODO Locale - Equivalent*)  

subsection‹Definition: Exists›
definition OclExists     :: "[('𝔄,'α::null) Sequence,('𝔄,'α)val⇒('𝔄)Boolean] ⇒ '𝔄 Boolean"
where     "OclExists S P = (S->iterateSeq(b; x = false | x or (P b)))"

syntax
  "_OclExistSeq" :: "[('𝔄,'α::null) Sequence,id,('𝔄)Boolean] ⇒ '𝔄 Boolean"    ("(_)->existsSeq'(_|_')")
translations
  "X->existsSeq(x | P)" == "CONST OclExists X (%x. P)"

(*TODO Locale - Equivalent*)  

subsection‹Definition: Collect›
definition OclCollect     :: "[('𝔄,'α::null)Sequence,('𝔄,'α)val⇒('𝔄,'β)val]⇒('𝔄,'β::null)Sequence"
where     "OclCollect S P = (S->iterateSeq(b; x = Sequence{} | x->prependSeq(P b)))"

syntax
  "_OclCollectSeq" :: "[('𝔄,'α::null) Sequence,id,('𝔄)Boolean] ⇒ '𝔄 Boolean"    ("(_)->collectSeq'(_|_')")
translations
  "X->collectSeq(x | P)" == "CONST OclCollect X (%x. P)"

(*TODO Locale - Equivalent*)  

subsection‹Definition: Select›
definition OclSelect     :: "[('𝔄,'α::null)Sequence,('𝔄,'α)val⇒('𝔄)Boolean]⇒('𝔄,'α::null)Sequence"
where     "OclSelect S P = 
           (S->iterateSeq(b; x = Sequence{} | if P b then x->prependSeq(b) else x endif))"

syntax
  "_OclSelectSeq" :: "[('𝔄,'α::null) Sequence,id,('𝔄)Boolean] ⇒ '𝔄 Boolean"  ("(_)->selectSeq'(_|_')")
translations
  "X->selectSeq(x | P)" == "CONST UML_Sequence.OclSelect X (%x. P)"

(*TODO Locale - Equivalent*)  

subsection‹Definition: Size›
definition OclSize     :: "[('𝔄,'α::null)Sequence]⇒('𝔄)Integer" ("(_)->sizeSeq'(')")
where     "OclSize S = (S->iterateSeq(b; x = 𝟬 | x +int 𝟭 ))"

(*TODO Locale - Equivalent*)  

subsection‹Definition: IsEmpty›
definition OclIsEmpty   :: "('𝔄,'α::null) Sequence ⇒ '𝔄 Boolean"
where     "OclIsEmpty x =  ((υ x and not (δ x)) or ((OclSize x) ≐ 𝟬))"
notation   OclIsEmpty     ("_->isEmptySeq'(')" (*[66]*))

(*TODO Locale - Equivalent*)  

subsection‹Definition: NotEmpty›

definition OclNotEmpty   :: "('𝔄,'α::null) Sequence ⇒ '𝔄 Boolean"
where     "OclNotEmpty x =  not(OclIsEmpty x)"
notation   OclNotEmpty    ("_->notEmptySeq'(')" (*[66]*))

(*TODO Locale - Equivalent*)  

subsection‹Definition: Any›

definition "OclANY x = (λ τ.
  if x τ = invalid τ then
    ⊥
  else
    case drop (drop (Rep_Sequencebase (x τ))) of [] ⇒ ⊥
                                              | l ⇒ hd l)"
notation   OclANY   ("_->anySeq'(')")

(*TODO Locale - Equivalent*)  

subsection‹Definition (future operators)›

consts (* abstract set collection operations *)
    OclCount       :: "[('𝔄,'α::null) Sequence,('𝔄,'α) Sequence] ⇒ '𝔄 Integer"
  (*OclFlatten*)
  (*OclInsertAt*)
  (*OclSubSequence*)
  (*OclIndexOf*)
  (*OclReverse*)
    OclSum         :: " ('𝔄,'α::null) Sequence ⇒ '𝔄 Integer"
  
notation  OclCount       ("_->countSeq'(_')" (*[66,65]65*))
notation  OclSum         ("_->sumSeq'(')" (*[66]*))

subsection‹Logical Properties›

subsection‹Execution Laws with Invalid or Null as Argument›

text‹OclIterate›

lemma OclIterate_invalid[simp,code_unfold]:"invalid->iterateSeq(a; x = A | P a x) = invalid"  
by(simp add: OclIterate_def false_def true_def, simp add: invalid_def)

lemma OclIterate_null[simp,code_unfold]:"null->iterateSeq(a; x = A | P a x) = invalid"  
by(simp add: OclIterate_def false_def true_def, simp add: invalid_def)

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

text_raw‹\isatagafp›

subsubsection‹Context Passing›

lemma cp_OclIncluding:
"(X->includingSeq(x)) τ = ((λ _. X τ)->includingSeq(λ _. x τ)) τ"
by(auto simp: OclIncluding_def StrongEq_def invalid_def
                 cp_defined[symmetric] cp_valid[symmetric])

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

lemmas cp_intro''Seq[intro!,simp,code_unfold] = 
       cp_OclIncluding [THEN allI[THEN allI[THEN allI[THEN cpI2]], of "OclIncluding"]]

subsubsection‹Const›

text_raw‹\endisatagafp›

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

lemma OclIterate_empty[simp,code_unfold]:"Sequence{}->iterateSeq(a; x = A | P a x) = A"  
apply(simp add: OclIterate_def foundation22[symmetric] foundation13, 
      rule ext, rename_tac "τ")
apply(case_tac "τ ⊨ υ A", simp_all add: foundation18')
apply(simp add: mtSequence_def)
apply(subst Abs_Sequencebase_inverse) by auto

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

lemma OclIterate_including[simp,code_unfold]:
assumes strict1 : "⋀X. P invalid X = invalid"
and     P_valid_arg: "⋀ τ. (υ A) τ = (υ (P a A)) τ"
and     P_cp    : "⋀ x y τ. P x y τ = P (λ _. x τ) y τ"
and     P_cp'   : "⋀ x y τ. P x y τ = P x (λ _. y τ) τ"
shows  "(S->includingSeq(a))->iterateSeq(b; x = A | P b x) = S->iterateSeq(b; x = P a A| P b x)"
 apply(rule ext)
proof -
 have A: "⋀S b τ. S ≠ ⊥ ⟹ S ≠ null ⟹ b ≠ ⊥  ⟹
                  ⌊⌊⌈⌈Rep_Sequencebase S⌉⌉ @ [b]⌋⌋ ∈ {X. X = bot ∨ X = null ∨ (∀x∈set ⌈⌈X⌉⌉. x ≠ ⊥)}"
          by(auto intro!:Sequence_inv_lemma[simplified OclValid_def 
                                       defined_def false_def true_def null_fun_def bot_fun_def])          
 have P: "⋀l A A' τ. A τ = A' τ ⟹ foldr P l A τ = foldr P l A' τ"
  apply(rule list.induct, simp, simp)
 by(subst (1 2) P_cp', simp)

 fix τ
 show "OclIterate (S->includingSeq(a)) A P τ = OclIterate S (P a A) P τ"
  apply(subst cp_OclIterate, subst OclIncluding_def, simp split:)
  apply(intro conjI impI)

   apply(simp add: OclIterate_def)
   apply(intro conjI impI)
     apply(subst Abs_Sequencebase_inverse[OF A],
           (simp add: foundation16[simplified OclValid_def] foundation18'[simplified OclValid_def])+)
     apply(rule P, metis P_cp)
    apply (metis P_valid_arg)
   apply(simp add: P_valid_arg[symmetric])
   apply (metis (lifting, no_types) OclIncluding.def_body' OclValid_def foundation16)
  apply(simp add: OclIterate_def defined_def invalid_def bot_option_def bot_fun_def false_def true_def)
  apply(intro impI, simp add: false_def true_def P_valid_arg)
 by (metis P_cp P_valid_arg UML_Types.bot_fun_def cp_valid invalid_def strict1 true_def valid1 valid_def)
qed

lemma OclIterate_prepend[simp,code_unfold]:
assumes strict1 : "⋀X. P invalid X = invalid"
and     strict2 : "⋀X. P X invalid = invalid"
and     P_cp    : "⋀ x y τ. P x y τ = P (λ _. x τ) y τ"
and     P_cp'   : "⋀ x y τ. P x y τ = P x (λ _. y τ) τ"
shows  "(S->prependSeq(a))->iterateSeq(b; x = A | P b x) = P a (S->iterateSeq(b; x = A| P b x))"
 apply(rule ext)
proof -
 have B: "⋀S a τ. S ≠ ⊥ ⟹ S ≠ null ⟹ a ≠ ⊥  ⟹
                  ⌊⌊a # ⌈⌈Rep_Sequencebase S⌉⌉⌋⌋ ∈ {X. X = bot ∨ X = null ∨ (∀x∈set ⌈⌈X⌉⌉. x ≠ ⊥)}"
          by(auto intro!:Sequence_inv_lemma[simplified OclValid_def 
                                       defined_def false_def true_def null_fun_def bot_fun_def])          
 fix τ
 show "OclIterate (S->prependSeq(a)) A P τ = P a (OclIterate S A P) τ"
  apply(subst cp_OclIterate, subst OclPrepend_def, simp split:)
  apply(intro conjI impI)

   apply(subst P_cp')
   apply(simp add: OclIterate_def)
   apply(intro conjI impI)
     apply(subst Abs_Sequencebase_inverse[OF B],
           (simp add: foundation16[simplified OclValid_def] foundation18'[simplified OclValid_def])+)
     apply(simp add: P_cp'[symmetric])
     apply(subst P_cp, simp add: P_cp[symmetric])
    apply (metis (no_types) OclPrepend.def_body' OclValid_def foundation16)
   apply (metis P_cp' invalid_def strict2 valid_def)

  apply(subst P_cp',
        simp add: OclIterate_def defined_def invalid_def bot_option_def bot_fun_def false_def true_def,
        intro conjI impI)
     apply (metis P_cp' invalid_def strict2 valid_def)
    apply (metis P_cp' invalid_def strict2 valid_def)
   apply (metis (no_types) P_cp invalid_def strict1 true_def valid1 valid_def)
  apply (metis P_cp' invalid_def strict2 valid_def)
 done
qed


(* < *)

subsection‹Test Statements›
(*
Assert   "(τ ⊨ (Sequence{λ_. ⌊⌊x⌋⌋} ≐ Sequence{λ_. ⌊⌊x⌋⌋}))"
Assert   "(τ ⊨ (Sequence{λ_. ⌊x⌋} ≐ Sequence{λ_. ⌊x⌋}))"
*)

instantiation Sequencebase  :: (equal)equal
begin
  definition "HOL.equal k l ⟷  (k::('a::equal)Sequencebase) =  l"
  instance   by standard (rule equal_Sequencebase_def)
end

lemma equal_Sequencebase_code [code]:
  "HOL.equal k (l::('a::{equal,null})Sequencebase) ⟷ Rep_Sequencebase k = Rep_Sequencebase l"
  by (auto simp add: equal Sequencebase.Rep_Sequencebase_inject)
  
Assert   "τ ⊨ (Sequence{} ≐ Sequence{})" 
Assert   "τ ⊨ (Sequence{𝟭,𝟮} ≜ Sequence{}->prependSeq(𝟮)->prependSeq(𝟭))" 
Assert   "τ ⊨ (Sequence{𝟭,invalid,𝟮} ≜ invalid)"
Assert   "τ ⊨ (Sequence{𝟭,𝟮}->prependSeq(null) ≜ Sequence{null,𝟭,𝟮})"
Assert   "τ ⊨ (Sequence{𝟭,𝟮}->includingSeq(null) ≜ Sequence{𝟭,𝟮,null})"

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

(* > *)

end