Theory OCL_Object_Model

(*  Title:       Safe OCL
    Author:      Denis Nikiforov, March 2019
    Maintainer:  Denis Nikiforov <denis.nikif at>
    License:     LGPL
chapter ‹Object Model›
theory OCL_Object_Model
  imports OCL_Syntax

text ‹
  I see no reason why objects should refer nulls using multi-valued
  associations. Therefore, multi-valued associations have collection
  types with non-nullable element types.›

  "assoc_end_type end 
    let 𝒞 = assoc_end_class end in
    if assoc_end_max end  (1 :: nat) then
      if assoc_end_min end = (0 :: nat)
      then 𝒞𝒯[?]
      else 𝒞𝒯[1]
      if assoc_end_unique end then
        if assoc_end_ordered end
        then OrderedSet 𝒞𝒯[1]
        else Set 𝒞𝒯[1]
        if assoc_end_ordered end
        then Sequence 𝒞𝒯[1]
        else Bag 𝒞𝒯[1]"

definition "class_assoc_type 𝒜  Set 𝒜𝒯[1]"

definition "class_assoc_end_type end  assoc_end_class end𝒯[1]"

definition "oper_type op 
  let params = oper_out_params op in
  if length params = 0
  then oper_result op
  else Tuple (fmap_of_list (map (λp. (param_name p, param_type p))
    (params @ [(STR ''result'', oper_result op, Out)])))"

class ocl_object_model =
  fixes classes :: "'a :: semilattice_sup fset"
    and attributes :: "'a f attr f 'a type"
    and associations :: "assoc f role f 'a assoc_end"
    and association_classes :: "'a f assoc"
    and operations :: "('a type, 'a expr) oper_spec list"
    and literals :: "'a enum f elit fset"
  assumes assoc_end_min_less_eq_max:
    "assoc |∈| fmdom associations 
     fmlookup associations assoc = Some ends 
     role |∈| fmdom ends  
     fmlookup ends role = Some end 
     assoc_end_min end  assoc_end_max end"
  assumes association_ends_unique:
    "association_ends' classes associations 𝒞 from role end1 
     association_ends' classes associations 𝒞 from role end2  end1 = end2"

interpretation base: object_model
  by standard (simp_all add: local.assoc_end_min_less_eq_max local.association_ends_unique)

abbreviation "owned_attribute  base.owned_attribute"
abbreviation "attribute  base.attribute"
abbreviation "association_ends  base.association_ends"
abbreviation "owned_association_end  base.owned_association_end"
abbreviation "association_end  base.association_end"
abbreviation "referred_by_association_class  base.referred_by_association_class"
abbreviation "association_class_end  base.association_class_end"
abbreviation "operation  base.operation"
abbreviation "operation_defined  base.operation_defined"
abbreviation "static_operation  base.static_operation"
abbreviation "static_operation_defined  base.static_operation_defined"
abbreviation "has_literal  base.has_literal"

lemmas attribute_det = base.attribute_det
lemmas attribute_self_or_inherited = base.attribute_self_or_inherited
lemmas attribute_closest = base.attribute_closest
lemmas association_end_det = base.association_end_det
lemmas association_end_self_or_inherited = base.association_end_self_or_inherited
lemmas association_end_closest = base.association_end_closest
lemmas association_class_end_det = base.association_class_end_det
lemmas operation_det = base.operation_det
lemmas static_operation_det = base.static_operation_det