(*  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
  "C |∈| fmdom attributes ==>
   fmlookup attributes C = Some attrs_\<C> ==>
   fmlookup attrs_\<C> attr = Some τ ==>
   owned_attribute' attributes C attr τ"

inductive attribute_not_closest where
  "owned_attribute' attributes D' attr τ' ==>
   C ≤ D' ==>
   D' < D ==>
   attribute_not_closest attributes C attr D τ"

inductive closest_attribute where
  "owned_attribute' attributes D attr τ ==>
   C ≤ D ==>
   ¬ attribute_not_closest attributes C attr D τ ==>
   closest_attribute attributes C attr D τ"

inductive closest_attribute_not_unique where
  "closest_attribute attributes C attr D' τ' ==>
   D ≠ D' ∨ τ ≠ τ' ==>
   closest_attribute_not_unique attributes C attr D τ"

inductive unique_closest_attribute where
  "closest_attribute attributes C attr D τ ==>
   ¬ closest_attribute_not_unique attributes C attr D τ ==>
   unique_closest_attribute attributes C attr D τ"

subsection ‹Association Ends›

inductive role_refer_class where
  "role |∈| fmdom ends ==>
   fmlookup ends role = Some end ==>
   assoc_end_class end = C ==>
   role_refer_class ends C role"

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

inductive association_ends_not_unique' where
  "association_ends' classes associations C from role end₁ ==>
   association_ends' classes associations C from role end₂ ==>
   end₁ ≠ end₂ ==>
   association_ends_not_unique' classes associations"

inductive owned_association_end' where
  "association_ends' classes associations C from role end ==>
   owned_association_end' classes associations C None role end"
| "association_ends' classes associations C from role end ==>
   owned_association_end' classes associations C (Some from) role end"

inductive association_end_not_closest where
  "owned_association_end' classes associations D' from role end' ==>
   C ≤ D' ==>
   D' < D ==>
   association_end_not_closest classes associations C from role D end"

inductive closest_association_end where
  "owned_association_end' classes associations D from role end ==>
   C ≤ D ==>
   ¬ association_end_not_closest classes associations C from role D end ==>
   closest_association_end classes associations C from role D end"

inductive closest_association_end_not_unique where
  "closest_association_end classes associations C from role D' end' ==>
   D ≠ D' ∨ end ≠ end' ==>
   closest_association_end_not_unique classes associations C from role D end"

inductive unique_closest_association_end where
  "closest_association_end classes associations C from role D end ==>
   ¬ closest_association_end_not_unique classes associations C from role D end ==>
   unique_closest_association_end classes associations C from role D end"

subsection ‹Association Classes›

inductive referred_by_association_class'' where
  "fmlookup association_classes A = Some assoc ==>
   fmlookup associations assoc = Some ends ==>
   role_refer_class ends C from ==>
   referred_by_association_class'' association_classes associations C from A"

inductive referred_by_association_class' where
  "referred_by_association_class'' association_classes associations C from A ==>
   referred_by_association_class' association_classes associations C None A"
| "referred_by_association_class'' association_classes associations C from A ==>
   referred_by_association_class' association_classes associations C (Some from) A"

inductive association_class_not_closest where
  "referred_by_association_class' association_classes associations D' from A ==>
   C ≤ D' ==>
   D' < D ==>
   association_class_not_closest association_classes associations C from A D"

inductive closest_association_class where
  "referred_by_association_class' association_classes associations D from A ==>
   C ≤ D ==>
   ¬ association_class_not_closest association_classes associations C from A D ==>
   closest_association_class association_classes associations C from A D"

inductive closest_association_class_not_unique where
  "closest_association_class association_classes associations C from A D' ==>
   D ≠ D' ==>
   closest_association_class_not_unique
        association_classes associations C from A D"

inductive unique_closest_association_class where
  "closest_association_class association_classes associations C from A D ==>
   ¬ closest_association_class_not_unique
        association_classes associations C from A D ==>
   unique_closest_association_class association_classes associations C from A D"

subsection ‹Association Class Ends›

inductive association_class_end' where
  "fmlookup association_classes A = Some assoc ==>
   fmlookup associations assoc = Some ends ==>
   fmlookup ends role = Some end ==>
   association_class_end' association_classes associations A role end"

inductive association_class_end_not_unique where
  "association_class_end' association_classes associations A role end' ==>
   end ≠ end' ==>
   association_class_end_not_unique association_classes associations A role end"

inductive unique_association_class_end where
  "association_class_end' association_classes associations A role end ==>
   ¬ association_class_end_not_unique
        association_classes associations A role end ==>
   unique_association_class_end association_classes associations A 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 C from role end₁ ==>
     association_ends' classes associations C from role end₂ ==> end₁ = end₂"
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 C attr D₁ τ₁ ==>
   attribute C attr D₂ τ₂ ==> D₁ = D₂ ∧ τ₁ = τ₂"
  by (meson closest_attribute_not_unique.intros unique_closest_attribute.cases)

lemma (in object_model) attribute_self_or_inherited:
  "attribute C attr D τ ==> C ≤ D"
  by (meson closest_attribute.cases unique_closest_attribute.cases)

lemma (in object_model) attribute_closest:
  "attribute C attr D τ ==>
   owned_attribute D' attr τ ==>
   C ≤ D' ==> ¬ D' < D"
  by (meson attribute_not_closest.intros closest_attribute.cases
      unique_closest_attribute.cases)


lemma (in object_model) association_end_det:
  "association_end C from role D₁ end₁ ==>
   association_end C from role D₂ end₂ ==> D₁ = D₂ ∧ end₁ = end₂"
  by (meson closest_association_end_not_unique.intros
      unique_closest_association_end.cases)

lemma (in object_model) association_end_self_or_inherited:
  "association_end C from role D end ==> C ≤ D"
  by (meson closest_association_end.cases unique_closest_association_end.cases)

lemma (in object_model) association_end_closest:
  "association_end C from role D end ==>
   owned_association_end D' from role end ==>
   C ≤ D' ==> ¬ D' < D"
  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 A role end₁ ==>
   association_class_end A role end₂ ==> end₁ = end₂"
  by (meson association_class_end_not_unique.intros unique_association_class_end.cases)


lemma (in object_model) operation_det:
  "operation τ name π oper₁ ==>
   operation τ name π oper₂ ==> oper₁ = oper₂"
  by (meson operation_not_unique.intros unique_operation.cases)

lemma (in object_model) static_operation_det:
  "static_operation τ name π oper₁ ==>
   static_operation τ name π oper₂ ==> oper₁ = oper₂"
  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