Theory Object_Model

(*  Title:       Safe OCL
    Author:      Denis Nikiforov, March 2019
    Maintainer:  Denis Nikiforov <denis.nikif at gmail.com>
    License:     LGPL
*)
section ‹Object Model›
theory Object_Model
  imports "HOL-Library.Extended_Nat" Finite_Map_Ext
begin

text ‹
  The section defines a generic object model.›

(*** Type Synonyms **********************************************************)

subsection ‹Type Synonyms›

type_synonym attr = String.literal
type_synonym assoc = String.literal
type_synonym role = String.literal
type_synonym oper = String.literal
type_synonym param = String.literal
type_synonym elit = String.literal

datatype param_dir = In | Out | InOut

type_synonym 'c assoc_end = "'c × nat × enat × bool × bool"
type_synonym 't param_spec = "param × 't × param_dir"
type_synonym ('t, 'e) oper_spec =
  "oper × 't × 't param_spec list × 't × bool × 'e option"

definition "assoc_end_class :: 'c assoc_end ⇒ 'c ≡ fst"
definition "assoc_end_min :: 'c assoc_end ⇒ nat ≡ fst ∘ snd"
definition "assoc_end_max :: 'c assoc_end ⇒ enat ≡ fst ∘ snd ∘ snd"
definition "assoc_end_ordered :: 'c assoc_end ⇒ bool ≡ fst ∘ snd ∘ snd ∘ snd"
definition "assoc_end_unique :: 'c assoc_end ⇒ bool ≡ snd ∘ snd ∘ snd ∘ snd"

definition "oper_name :: ('t, 'e) oper_spec ⇒ oper ≡ fst"
definition "oper_context :: ('t, 'e) oper_spec ⇒ 't ≡ fst ∘ snd"
definition "oper_params :: ('t, 'e) oper_spec ⇒ 't param_spec list ≡ fst ∘ snd ∘ snd"
definition "oper_result :: ('t, 'e) oper_spec ⇒ 't ≡ fst ∘ snd ∘ snd ∘ snd"
definition "oper_static :: ('t, 'e) oper_spec ⇒ bool ≡ fst ∘ snd ∘ snd ∘ snd ∘ snd"
definition "oper_body :: ('t, 'e) oper_spec ⇒ 'e option ≡ snd ∘ snd ∘ snd ∘ snd ∘ snd"

definition "param_name ::'t param_spec ⇒ param ≡ fst"
definition "param_type ::'t param_spec ⇒ 't ≡ fst ∘ snd"
definition "param_dir ::'t param_spec ⇒ param_dir ≡ snd ∘ snd"

definition "oper_in_params op ≡
  filter (λp. param_dir p = In ∨ param_dir p = InOut) (oper_params op)"

definition "oper_out_params op ≡
  filter (λp. param_dir p = Out ∨ param_dir p = InOut) (oper_params op)"

subsection ‹Attributes›

inductive owned_attribute' where
  "𝒞 |∈| fmdom attributes ⟹
   fmlookup attributes 𝒞 = Some attrs𝒞 ⟹
   fmlookup attrs𝒞 attr = Some τ ⟹
   owned_attribute' attributes 𝒞 attr τ"

inductive attribute_not_closest where
  "owned_attribute' attributes 𝒟' attr τ' ⟹
   𝒞 ≤ 𝒟' ⟹
   𝒟' < 𝒟 ⟹
   attribute_not_closest attributes 𝒞 attr 𝒟 τ"

inductive closest_attribute where
  "owned_attribute' attributes 𝒟 attr τ ⟹
   𝒞 ≤ 𝒟 ⟹
   ¬ attribute_not_closest attributes 𝒞 attr 𝒟 τ ⟹
   closest_attribute attributes 𝒞 attr 𝒟 τ"

inductive closest_attribute_not_unique where
  "closest_attribute attributes 𝒞 attr 𝒟' τ' ⟹
   𝒟 ≠ 𝒟' ∨ τ ≠ τ' ⟹
   closest_attribute_not_unique attributes 𝒞 attr 𝒟 τ"

inductive unique_closest_attribute where
  "closest_attribute attributes 𝒞 attr 𝒟 τ ⟹
   ¬ closest_attribute_not_unique attributes 𝒞 attr 𝒟 τ ⟹
   unique_closest_attribute attributes 𝒞 attr 𝒟 τ"

subsection ‹Association Ends›

inductive role_refer_class where
  "role |∈| fmdom ends ⟹
   fmlookup ends role = Some end ⟹
   assoc_end_class end = 𝒞 ⟹
   role_refer_class ends 𝒞 role"

inductive association_ends' where
  "𝒞 |∈| classes ⟹
   assoc |∈| fmdom associations ⟹
   fmlookup associations assoc = Some ends ⟹
   role_refer_class ends 𝒞 from ⟹
   role |∈| fmdom ends ⟹
   fmlookup ends role = Some end ⟹
   role ≠ from ⟹
   association_ends' classes associations 𝒞 from role end"

inductive association_ends_not_unique' where
  "association_ends' classes associations 𝒞 from role end1 ⟹
   association_ends' classes associations 𝒞 from role end2 ⟹
   end1 ≠ end2 ⟹
   association_ends_not_unique' classes associations"

inductive owned_association_end' where
  "association_ends' classes associations 𝒞 from role end ⟹
   owned_association_end' classes associations 𝒞 None role end"
| "association_ends' classes associations 𝒞 from role end ⟹
   owned_association_end' classes associations 𝒞 (Some from) role end"

inductive association_end_not_closest where
  "owned_association_end' classes associations 𝒟' from role end' ⟹
   𝒞 ≤ 𝒟' ⟹
   𝒟' < 𝒟 ⟹
   association_end_not_closest classes associations 𝒞 from role 𝒟 end"

inductive closest_association_end where
  "owned_association_end' classes associations 𝒟 from role end ⟹
   𝒞 ≤ 𝒟 ⟹
   ¬ association_end_not_closest classes associations 𝒞 from role 𝒟 end ⟹
   closest_association_end classes associations 𝒞 from role 𝒟 end"

inductive closest_association_end_not_unique where
  "closest_association_end classes associations 𝒞 from role 𝒟' end' ⟹
   𝒟 ≠ 𝒟' ∨ end ≠ end' ⟹
   closest_association_end_not_unique classes associations 𝒞 from role 𝒟 end"

inductive unique_closest_association_end where
  "closest_association_end classes associations 𝒞 from role 𝒟 end ⟹
   ¬ closest_association_end_not_unique classes associations 𝒞 from role 𝒟 end ⟹
   unique_closest_association_end classes associations 𝒞 from role 𝒟 end"

subsection ‹Association Classes›

inductive referred_by_association_class'' where
  "fmlookup association_classes 𝒜 = Some assoc ⟹
   fmlookup associations assoc = Some ends ⟹
   role_refer_class ends 𝒞 from ⟹
   referred_by_association_class'' association_classes associations 𝒞 from 𝒜"

inductive referred_by_association_class' where
  "referred_by_association_class'' association_classes associations 𝒞 from 𝒜 ⟹
   referred_by_association_class' association_classes associations 𝒞 None 𝒜"
| "referred_by_association_class'' association_classes associations 𝒞 from 𝒜 ⟹
   referred_by_association_class' association_classes associations 𝒞 (Some from) 𝒜"

inductive association_class_not_closest where
  "referred_by_association_class' association_classes associations 𝒟' from 𝒜 ⟹
   𝒞 ≤ 𝒟' ⟹
   𝒟' < 𝒟 ⟹
   association_class_not_closest association_classes associations 𝒞 from 𝒜 𝒟"

inductive closest_association_class where
  "referred_by_association_class' association_classes associations 𝒟 from 𝒜 ⟹
   𝒞 ≤ 𝒟 ⟹
   ¬ association_class_not_closest association_classes associations 𝒞 from 𝒜 𝒟 ⟹
   closest_association_class association_classes associations 𝒞 from 𝒜 𝒟"

inductive closest_association_class_not_unique where
  "closest_association_class association_classes associations 𝒞 from 𝒜 𝒟' ⟹
   𝒟 ≠ 𝒟' ⟹
   closest_association_class_not_unique
        association_classes associations 𝒞 from 𝒜 𝒟"

inductive unique_closest_association_class where
  "closest_association_class association_classes associations 𝒞 from 𝒜 𝒟 ⟹
   ¬ closest_association_class_not_unique
        association_classes associations 𝒞 from 𝒜 𝒟 ⟹
   unique_closest_association_class association_classes associations 𝒞 from 𝒜 𝒟"

subsection ‹Association Class Ends›

inductive association_class_end' where
  "fmlookup association_classes 𝒜 = Some assoc ⟹
   fmlookup associations assoc = Some ends ⟹
   fmlookup ends role = Some end ⟹
   association_class_end' association_classes associations 𝒜 role end"

inductive association_class_end_not_unique where
  "association_class_end' association_classes associations 𝒜 role end' ⟹
   end ≠ end' ⟹
   association_class_end_not_unique association_classes associations 𝒜 role end"

inductive unique_association_class_end where
  "association_class_end' association_classes associations 𝒜 role end ⟹
   ¬ association_class_end_not_unique
        association_classes associations 𝒜 role end ⟹
   unique_association_class_end association_classes associations 𝒜 role end"

subsection ‹Operations›

inductive any_operation' where
  "op |∈| fset_of_list operations ⟹
   oper_name op = name ⟹
   τ ≤ oper_context op ⟹
   list_all2 (λσ param. σ ≤ param_type param) π (oper_in_params op) ⟹
   any_operation' operations τ name π op"

inductive operation' where
  "any_operation' operations τ name π op ⟹
   ¬ oper_static op ⟹
   operation' operations τ name π op"

inductive operation_not_unique where
  "operation' operations τ name π oper' ⟹
   oper ≠ oper' ⟹
   operation_not_unique operations τ name π oper"

inductive unique_operation where
  "operation' operations τ name π oper ⟹
   ¬ operation_not_unique operations τ name π oper ⟹
   unique_operation operations τ name π oper"

inductive operation_defined' where
  "unique_operation operations τ name π oper ⟹
   operation_defined' operations τ name π"

inductive static_operation' where
  "any_operation' operations τ name π op ⟹
   oper_static op ⟹
   static_operation' operations τ name π op"

inductive static_operation_not_unique where
  "static_operation' operations τ name π oper' ⟹
   oper ≠ oper' ⟹
   static_operation_not_unique operations τ name π oper"

inductive unique_static_operation where
  "static_operation' operations τ name π oper ⟹
   ¬ static_operation_not_unique operations τ name π oper ⟹
   unique_static_operation operations τ name π oper"

inductive static_operation_defined' where
  "unique_static_operation operations τ name π oper ⟹
   static_operation_defined' operations τ name π"

subsection ‹Literals›

inductive has_literal' where
  "fmlookup literals e = Some lits ⟹
   lit |∈| lits ⟹
   has_literal' literals e lit"

(*** Definition *************************************************************)

subsection ‹Definition›

locale object_model =
  fixes classes :: "'a :: semilattice_sup fset"
    and attributes :: "'a ⇀f attr ⇀f 't :: order"
    and associations :: "assoc ⇀f role ⇀f 'a assoc_end"
    and association_classes :: "'a ⇀f assoc"
    and operations :: "('t, 'e) oper_spec list"
    and literals :: "'n ⇀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"
begin

abbreviation "owned_attribute ≡
  owned_attribute' attributes"

abbreviation "attribute ≡
  unique_closest_attribute attributes"

abbreviation "association_ends ≡
  association_ends' classes associations"

abbreviation "owned_association_end ≡
  owned_association_end' classes associations"

abbreviation "association_end ≡
  unique_closest_association_end classes associations"

abbreviation "referred_by_association_class ≡
  unique_closest_association_class association_classes associations"

abbreviation "association_class_end ≡
  unique_association_class_end association_classes associations"

abbreviation "operation ≡
  unique_operation operations"

abbreviation "operation_defined ≡
  operation_defined' operations"

abbreviation "static_operation ≡
  unique_static_operation operations"

abbreviation "static_operation_defined ≡
  static_operation_defined' operations"

abbreviation "has_literal ≡
  has_literal' literals"

end

declare operation_defined'.simps [simp]
declare static_operation_defined'.simps [simp]

declare has_literal'.simps [simp]

(*** Properties *************************************************************)

subsection ‹Properties›

lemma (in object_model) attribute_det:
  "attribute 𝒞 attr 𝒟1 τ1 ⟹
   attribute 𝒞 attr 𝒟2 τ2 ⟹ 𝒟1 = 𝒟2 ∧ τ1 = τ2"
  by (meson closest_attribute_not_unique.intros unique_closest_attribute.cases)

lemma (in object_model) attribute_self_or_inherited:
  "attribute 𝒞 attr 𝒟 τ ⟹ 𝒞 ≤ 𝒟"
  by (meson closest_attribute.cases unique_closest_attribute.cases)

lemma (in object_model) attribute_closest:
  "attribute 𝒞 attr 𝒟 τ ⟹
   owned_attribute 𝒟' attr τ ⟹
   𝒞 ≤ 𝒟' ⟹ ¬ 𝒟' < 𝒟"
  by (meson attribute_not_closest.intros closest_attribute.cases
      unique_closest_attribute.cases)


lemma (in object_model) association_end_det:
  "association_end 𝒞 from role 𝒟1 end1 ⟹
   association_end 𝒞 from role 𝒟2 end2 ⟹ 𝒟1 = 𝒟2 ∧ end1 = end2"
  by (meson closest_association_end_not_unique.intros
      unique_closest_association_end.cases)

lemma (in object_model) association_end_self_or_inherited:
  "association_end 𝒞 from role 𝒟 end ⟹ 𝒞 ≤ 𝒟"
  by (meson closest_association_end.cases unique_closest_association_end.cases)

lemma (in object_model) association_end_closest:
  "association_end 𝒞 from role 𝒟 end ⟹
   owned_association_end 𝒟' from role end ⟹
   𝒞 ≤ 𝒟' ⟹ ¬ 𝒟' < 𝒟"
  by (meson association_end_not_closest.intros closest_association_end.cases
      unique_closest_association_end.cases)


lemma (in object_model) association_class_end_det:
  "association_class_end 𝒜 role end1 ⟹
   association_class_end 𝒜 role end2 ⟹ end1 = end2"
  by (meson association_class_end_not_unique.intros unique_association_class_end.cases)


lemma (in object_model) operation_det:
  "operation τ name π oper1 ⟹
   operation τ name π oper2 ⟹ oper1 = oper2"
  by (meson operation_not_unique.intros unique_operation.cases)

lemma (in object_model) static_operation_det:
  "static_operation τ name π oper1 ⟹
   static_operation τ name π oper2 ⟹ oper1 = oper2"
  by (meson static_operation_not_unique.intros unique_static_operation.cases)

(*** Code Setup *************************************************************)

subsection ‹Code Setup›

declare owned_attribute'.intros[folded Predicate_Compile.contains_def, code_pred_intro]
code_pred (modes:
  i ⇒ i ⇒ i ⇒ i ⇒ bool,
  i ⇒ i ⇒ i ⇒ o ⇒ bool,
  i ⇒ o ⇒ i ⇒ i ⇒ bool,
  i ⇒ o ⇒ i ⇒ o ⇒ bool) owned_attribute'
  by (elim owned_attribute'.cases) (simp add: Predicate_Compile.contains_def)

code_pred unique_closest_attribute .

declare role_refer_class.intros[folded Predicate_Compile.contains_def, code_pred_intro]
code_pred (modes:
    i ⇒ i ⇒ i ⇒ bool,
    i ⇒ i ⇒ o ⇒ bool,
    i ⇒ o ⇒ i ⇒ bool,
    i ⇒ o ⇒ o ⇒ bool) role_refer_class
  by (elim role_refer_class.cases) (simp add: Predicate_Compile.contains_def)

declare association_ends'.intros[folded Predicate_Compile.contains_def, code_pred_intro]
code_pred (modes:
    i ⇒ i ⇒ i ⇒ i ⇒ i ⇒ i ⇒ bool,
    i ⇒ i ⇒ i ⇒ i ⇒ i ⇒ o ⇒ bool,
    i ⇒ i ⇒ i ⇒ i ⇒ o ⇒ i ⇒ bool,
    i ⇒ i ⇒ i ⇒ i ⇒ o ⇒ o ⇒ bool,
    i ⇒ i ⇒ i ⇒ o ⇒ i ⇒ i ⇒ bool,
    i ⇒ i ⇒ i ⇒ o ⇒ i ⇒ o ⇒ bool,
    i ⇒ i ⇒ i ⇒ o ⇒ o ⇒ i ⇒ bool,
    i ⇒ i ⇒ i ⇒ o ⇒ o ⇒ o ⇒ bool,
    i ⇒ i ⇒ o ⇒ i ⇒ i ⇒ i ⇒ bool,
    i ⇒ i ⇒ o ⇒ i ⇒ i ⇒ o ⇒ bool,
    i ⇒ i ⇒ o ⇒ i ⇒ o ⇒ i ⇒ bool,
    i ⇒ i ⇒ o ⇒ i ⇒ o ⇒ o ⇒ bool,
    i ⇒ i ⇒ o ⇒ o ⇒ i ⇒ i ⇒ bool,
    i ⇒ i ⇒ o ⇒ o ⇒ i ⇒ o ⇒ bool,
    i ⇒ i ⇒ o ⇒ o ⇒ o ⇒ i ⇒ bool,
    i ⇒ i ⇒ o ⇒ o ⇒ o ⇒ o ⇒ bool) association_ends'
  by (auto simp: Predicate_Compile.contains_def elim: association_ends'.cases)

code_pred association_ends_not_unique' .

code_pred (modes:
    i ⇒ i ⇒ i ⇒ i ⇒ i ⇒ i ⇒ bool,
    i ⇒ i ⇒ i ⇒ i ⇒ i ⇒ o ⇒ bool,
    i ⇒ i ⇒ i ⇒ i ⇒ o ⇒ i ⇒ bool,
    i ⇒ i ⇒ i ⇒ i ⇒ o ⇒ o ⇒ bool,
    i ⇒ i ⇒ i ⇒ o ⇒ i ⇒ i ⇒ bool,
    i ⇒ i ⇒ i ⇒ o ⇒ i ⇒ o ⇒ bool,
    i ⇒ i ⇒ i ⇒ o ⇒ o ⇒ i ⇒ bool,
    i ⇒ i ⇒ i ⇒ o ⇒ o ⇒ o ⇒ bool,
    i ⇒ i ⇒ o ⇒ i ⇒ i ⇒ i ⇒ bool,
    i ⇒ i ⇒ o ⇒ i ⇒ i ⇒ o ⇒ bool,
    i ⇒ i ⇒ o ⇒ i ⇒ o ⇒ i ⇒ bool,
    i ⇒ i ⇒ o ⇒ i ⇒ o ⇒ o ⇒ bool,
    i ⇒ i ⇒ o ⇒ o ⇒ i ⇒ i ⇒ bool,
    i ⇒ i ⇒ o ⇒ o ⇒ i ⇒ o ⇒ bool,
    i ⇒ i ⇒ o ⇒ o ⇒ o ⇒ i ⇒ bool,
    i ⇒ i ⇒ o ⇒ o ⇒ o ⇒ o ⇒ bool) owned_association_end' .

code_pred (modes:
    i ⇒ i ⇒ i ⇒ i ⇒ i ⇒ i ⇒ i ⇒ bool,
    i ⇒ i ⇒ i ⇒ i ⇒ i ⇒ i ⇒ o ⇒ bool,
    i ⇒ i ⇒ i ⇒ i ⇒ i ⇒ o ⇒ i ⇒ bool,
    i ⇒ i ⇒ i ⇒ i ⇒ i ⇒ o ⇒ o ⇒ bool,
    i ⇒ i ⇒ i ⇒ i ⇒ o ⇒ i ⇒ i ⇒ bool,
    i ⇒ i ⇒ i ⇒ i ⇒ o ⇒ i ⇒ o ⇒ bool,
    i ⇒ i ⇒ i ⇒ i ⇒ o ⇒ o ⇒ i ⇒ bool,
    i ⇒ i ⇒ i ⇒ i ⇒ o ⇒ o ⇒ o ⇒ bool,
    i ⇒ i ⇒ i ⇒ o ⇒ i ⇒ i ⇒ i ⇒ bool,
    i ⇒ i ⇒ i ⇒ o ⇒ i ⇒ i ⇒ o ⇒ bool,
    i ⇒ i ⇒ i ⇒ o ⇒ i ⇒ o ⇒ i ⇒ bool,
    i ⇒ i ⇒ i ⇒ o ⇒ i ⇒ o ⇒ o ⇒ bool,
    i ⇒ i ⇒ i ⇒ o ⇒ o ⇒ i ⇒ i ⇒ bool,
    i ⇒ i ⇒ i ⇒ o ⇒ o ⇒ i ⇒ o ⇒ bool,
    i ⇒ i ⇒ i ⇒ o ⇒ o ⇒ o ⇒ i ⇒ bool,
    i ⇒ i ⇒ i ⇒ o ⇒ o ⇒ o ⇒ o ⇒ bool) closest_association_end .

code_pred (modes:
    i ⇒ i ⇒ i ⇒ i ⇒ i ⇒ i ⇒ i ⇒ bool,
    i ⇒ i ⇒ i ⇒ i ⇒ o ⇒ i ⇒ i ⇒ bool,
    i ⇒ i ⇒ i ⇒ o ⇒ i ⇒ i ⇒ i ⇒ bool,
    i ⇒ i ⇒ i ⇒ o ⇒ o ⇒ i ⇒ i ⇒ bool ) closest_association_end_not_unique .

code_pred (modes:
    i ⇒ i ⇒ i ⇒ i ⇒ i ⇒ i ⇒ i ⇒ bool,
    i ⇒ i ⇒ i ⇒ i ⇒ i ⇒ i ⇒ o ⇒ bool,
    i ⇒ i ⇒ i ⇒ i ⇒ i ⇒ o ⇒ i ⇒ bool,
    i ⇒ i ⇒ i ⇒ i ⇒ i ⇒ o ⇒ o ⇒ bool) unique_closest_association_end .

code_pred unique_closest_association_class .

code_pred association_class_end' .

code_pred association_class_end_not_unique .

code_pred unique_association_class_end .

declare any_operation'.intros[folded Predicate_Compile.contains_def, code_pred_intro]
code_pred [show_modes] any_operation'
  by (elim any_operation'.cases) (simp add: Predicate_Compile.contains_def)

code_pred (modes:
    i ⇒ i ⇒ i ⇒ i ⇒ i ⇒ bool,
    i ⇒ i ⇒ i ⇒ i ⇒ o ⇒ bool) operation' .

code_pred (modes:
    i ⇒ i ⇒ i ⇒ i ⇒ i ⇒ bool) operation_not_unique .

code_pred (modes:
    i ⇒ i ⇒ i ⇒ i ⇒ i ⇒ bool,
    i ⇒ i ⇒ i ⇒ i ⇒ o ⇒ bool) unique_operation .

code_pred operation_defined' .

code_pred (modes:
    i ⇒ i ⇒ i ⇒ i ⇒ i ⇒ bool,
    i ⇒ i ⇒ i ⇒ i ⇒ o ⇒ bool) static_operation' .

code_pred (modes:
    i ⇒ i ⇒ i ⇒ i ⇒ i ⇒ bool) static_operation_not_unique .

code_pred (modes:
    i ⇒ i ⇒ i ⇒ i ⇒ i ⇒ bool,
    i ⇒ i ⇒ i ⇒ i ⇒ o ⇒ bool) unique_static_operation .

code_pred static_operation_defined' .

declare has_literal'.intros[folded Predicate_Compile.contains_def, code_pred_intro]
code_pred (modes:
  i ⇒ i ⇒ i ⇒ bool, i ⇒ i ⇒ o ⇒ bool) has_literal'
  by (elim has_literal'.cases) (simp add: Predicate_Compile.contains_def)

end