I defined a very simple object-oriented model. The model defines a set of classes and a set of associations.
nonterminal fmaplets and fmaplet
syntax
"_fmaplet" :: "['a, 'a] ⇒ fmaplet" ("_ /↦⇩f/ _")
"_fmaplets" :: "['a, 'a] ⇒ fmaplet" ("_ /[↦⇩f]/ _")
"" :: "fmaplet ⇒ fmaplets" ("_")
"_FMaplets" :: "[fmaplet, fmaplets] ⇒ fmaplets" ("_,/ _")
"_FMapUpd" :: "['a ⇀ 'b, fmaplets] ⇒ 'a ⇀ 'b" ("_/'(_')" [900, 0] 900)
"_FMap" :: "fmaplets ⇒ 'a ⇀ 'b" ("(1[_])")
syntax (ASCII)
"_fmaplet" :: "['a, 'a] ⇒ fmaplet" ("_ /|->f/ _")
"_fmaplets" :: "['a, 'a] ⇒ fmaplet" ("_ /[|->f]/ _")
translations
"_FMapUpd m (_FMaplets xy ms)" ⇌ "_FMapUpd (_FMapUpd m xy) ms"
"_FMapUpd m (_fmaplet x y)" ⇌ "CONST fmupd x y m"
"_FMap ms" ⇌ "_FMapUpd (CONST fmempty) ms"
"_FMap (_FMaplets ms1 ms2)" ↽ "_FMapUpd (_FMap ms1) ms2"
"_FMaplets ms1 (_FMaplets ms2 ms3)" ↽ "_FMaplets (_FMaplets ms1 ms2) ms3"
datatype classes1 =
Object | Person | Employee | Customer | Project | Task | Sprint
abbreviation "associations ≡ [
STR ''ProjectManager'' ↦⇩f [
STR ''projects'' ↦⇩f (Project, 0::nat, 100::nat),
STR ''manager'' ↦⇩f (Employee, 1, 1)],
STR ''ProjectMember'' ↦⇩f [
STR ''member_of'' ↦⇩f (Project, 0, 100),
STR ''members'' ↦⇩f (Employee, 1, 20)],
STR ''ManagerEmployee'' ↦⇩f [
STR ''line_manager'' ↦⇩f (Employee, 0, 1),
STR ''project_manager'' ↦⇩f (Employee, 0, 100),
STR ''employees'' ↦⇩f (Employee, 3, 7)],
STR ''ProjectCustomer'' ↦⇩f [
STR ''projects'' ↦⇩f (Project, 0, 100),
STR ''customer'' ↦⇩f (Customer, 1, 1)],
STR ''ProjectTask'' ↦⇩f [
STR ''project'' ↦⇩f (Project, 1, 1),
STR ''tasks'' ↦⇩f (Task, 0, 100)],
STR ''SprintTaskAssignee'' ↦⇩f [
STR ''sprint'' ↦⇩f (Sprint, 0, 10),
STR ''tasks'' ↦⇩f (Task, 0, 5),
STR ''assignee'' ↦⇩f (Employee, 0, 1)]]"
I defined also a class_roles predicate which relates a class to a set of association ends navigable from this class:
lemma fmember_code_predI [code_pred_intro]:
"x |∈| xs" if "Predicate_Compile.contains (fset xs) x"
using that by (simp add: Predicate_Compile.contains_def fmember.rep_eq)
code_pred fmember
by (simp add: Predicate_Compile.contains_def fmember.rep_eq)
definition "assoc_end_class ≡ fst"
inductive assoc_refer_class where
"role |∈| fmdom ends ⟹
fmlookup ends role = Some end ⟹
assoc_end_class end =
