Session Safe_OCL

Theory Errorable

(*  Title:       Safe OCL
    Author:      Denis Nikiforov, March 2019
    Maintainer:  Denis Nikiforov <denis.nikif at gmail.com>
    License:     LGPL
*)
chapter ‹Preliminaries›
section ‹Errorable›
theory Errorable
  imports Main
begin

notation bot ("")

typedef 'a errorable ("_" [21] 21) = "UNIV :: 'a option set" ..

definition errorable :: "'a  'a errorable" ("_" [1000] 1000) where
  "errorable x = Abs_errorable (Some x)"

instantiation errorable :: (type) bot
begin
definition "  Abs_errorable None"
instance ..
end

free_constructors case_errorable for
  errorable
| " :: 'a errorable"
  unfolding errorable_def bot_errorable_def
  apply (metis Abs_errorable_cases not_None_eq)
  apply (metis Abs_errorable_inverse UNIV_I option.inject)
  by (simp add: Abs_errorable_inject)

copy_bnf 'a errorable

end

Theory Transitive_Closure_Ext

(*  Title:       Safe OCL
    Author:      Denis Nikiforov, March 2019
    Maintainer:  Denis Nikiforov <denis.nikif at gmail.com>
    License:     LGPL
*)
section ‹Transitive Closures›
theory Transitive_Closure_Ext
  imports "HOL-Library.FuncSet"
begin

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

subsection ‹Basic Properties›

text @{text "R++"} is a transitive closure of a relation @{text R}.
  @{text "R**"} is a reflexive transitive closure of a relation @{text R}.›

text ‹
  A function @{text f} is surjective on @{text "R++"} iff for any
  two elements in the range of @{text f}, related through @{text "R++"},
  all their intermediate elements belong to the range of @{text f}.›

abbreviation "surj_on_trancl R f 
  (x y z. R++ (f x) y  R y (f z)  y  range f)"

text ‹
  A function @{text f} is bijective on @{text "R++"} iff
  it is injective and surjective on @{text "R++"}.›

abbreviation "bij_on_trancl R f  inj f  surj_on_trancl R f"

(*** Helper Lemmas **********************************************************)

subsection ‹Helper Lemmas›

lemma rtranclp_eq_rtranclp [iff]:
  "(λx y. P x y  x = y)** = P**"
proof (intro ext iffI)
  fix x y
  have "(λx y. P x y  x = y)** x y  P==** x y"
    by (rule mono_rtranclp) simp
  thus "(λx y. P x y  x = y)** x y  P** x y"
    by simp
  show "P** x y  (λx y. P x y  x = y)** x y"
    by (metis (no_types, lifting) mono_rtranclp)
qed

lemma tranclp_eq_rtranclp [iff]:
  "(λx y. P x y  x = y)++ = P**"
proof (intro ext iffI)
  fix x y
  have "(λx y. P x y  x = y)** x y  P==** x y"
    by (rule mono_rtranclp) simp
  thus "(λx y. P x y  x = y)++ x y  P** x y"
    using tranclp_into_rtranclp by force
  show "P** x y  (λx y. P x y  x = y)++ x y"
    by (metis (mono_tags, lifting) mono_rtranclp rtranclpD tranclp.r_into_trancl)
qed

lemma rtranclp_eq_rtranclp' [iff]:
  "(λx y. P x y  x  y)** = P**"
proof (intro ext iffI)
  fix x y
  show "(λx y. P x y  x  y)** x y  P** x y"
    by (metis (no_types, lifting) mono_rtranclp)
  assume "P** x y"
  hence "(inf P (≠))** x y"
    by (simp add: rtranclp_r_diff_Id)
  also have "(inf P (≠))** x y  (λx y. P x y  x  y)** x y"
    by (rule mono_rtranclp) simp
  finally show "P** x y  (λx y. P x y  x  y)** x y" by simp
qed

lemma tranclp_tranclp_to_tranclp_r:
  assumes "(x y z. R++ x y  R y z  P x  P z  P y)"
  assumes "R++ x y" and "R++ y z"
  assumes "P x" and "P z"
  shows "P y"
proof -
  have "(x y z. R++ x y  R y z  P x  P z  P y) 
         R++ y z  R++ x y  P x  P z  P y"
    by (erule tranclp_induct, auto) (meson tranclp_trans)
  thus ?thesis using assms by auto
qed

(*** Transitive Closure Preservation & Reflection ***************************)

subsection ‹Transitive Closure Preservation›

text ‹
  A function @{text f} preserves @{text "R++"} if it preserves @{text R}.›

text ‹
  The proof was derived from the accepted answer on the website
  Stack Overflow that is available at
  @{url "https://stackoverflow.com/a/52573551/632199"}
  and provided with the permission of the author of the answer.›

lemma preserve_tranclp:
  assumes "x y. R x y  S (f x) (f y)"
  assumes "R++ x y"
  shows "S++ (f x) (f y)"
proof -
  define P where P: "P = (λx y. S++ (f x) (f y))" 
  define r where r: "r = (λx y. S (f x) (f y))"
  have "r++ x y" by (insert assms r; erule tranclp_trans_induct; auto)
  moreover have "x y. r x y  P x y" unfolding P r by simp
  moreover have "x y z. r++ x y  P x y  r++ y z  P y z  P x z"
    unfolding P by auto
  ultimately have "P x y" by (rule tranclp_trans_induct)
  with P show ?thesis by simp
qed

text ‹
  A function @{text f} preserves @{text "R**"} if it preserves @{text R}.›

lemma preserve_rtranclp:
  "(x y. R x y  S (f x) (f y)) 
   R** x y  S** (f x) (f y)"
  unfolding Nitpick.rtranclp_unfold
  by (metis preserve_tranclp)

text ‹
  If one needs to prove that @{text "(f x)"} and @{text "(g y)"}
  are related through @{text "S**"} then one can use the previous
  lemma and add a one more step from @{text "(f y)"} to @{text "(g y)"}.›

lemma preserve_rtranclp':
  "(x y. R x y  S (f x) (f y)) 
   (y. S (f y) (g y)) 
   R** x y  S** (f x) (g y)"
  by (metis preserve_rtranclp rtranclp.rtrancl_into_rtrancl)

lemma preserve_rtranclp'':
  "(x y. R x y  S (f x) (f y)) 
   (y. S (f y) (g y)) 
   R** x y  S++ (f x) (g y)"
  apply (rule_tac ?b="f y" in rtranclp_into_tranclp1, auto)
  by (rule preserve_rtranclp, auto)

subsection ‹Transitive Closure Reflection›

text ‹
  A function @{text f} reflects @{text "S++"} if it reflects
  @{text S} and is bijective on @{text "S++"}.›

text ‹
  The proof was derived from the accepted answer on the website
  Stack Overflow that is available at
  @{url "https://stackoverflow.com/a/52573551/632199"}
  and provided with the permission of the author of the answer.›

lemma reflect_tranclp:
  assumes refl_f: "x y. S (f x) (f y)  R x y"
  assumes bij_f: "bij_on_trancl S f"
  assumes prem: "S++ (f x) (f y)"
  shows "R++ x y"
proof -
  define B where B: "B = range f"
  define g where g: "g = the_inv_into UNIV f"
  define gr where gr: "gr = restrict g B"
  define P where P: "P = (λx y. x  B  y  B  R++ (gr x) (gr y))"
  from prem have major: "S++ (f x) (f y)" by blast
  from refl_f bij_f have cases_1: "x y. S x y  P x y"
    unfolding B P g gr
    by (simp add: f_the_inv_into_f tranclp.r_into_trancl)
  from refl_f bij_f
  have "(x y z. S++ x y  S++ y z  x  B  z  B  y  B)"
    unfolding B
    by (rule_tac ?z="z" in tranclp_tranclp_to_tranclp_r, auto, blast)
  with P have cases_2:
    "x y z. S++ x y  P x y  S++ y z  P y z  P x z"
    unfolding B
    by auto
  from major cases_1 cases_2 have "P (f x) (f y)"
    by (rule tranclp_trans_induct)
  with bij_f show ?thesis unfolding P B g gr by (simp add: the_inv_f_f)
qed

text ‹
  A function @{text f} reflects @{text "S**"} if it reflects
  @{text S} and is bijective on @{text "S++"}.›

lemma reflect_rtranclp:
  "(x y. S (f x) (f y)  R x y) 
   bij_on_trancl S f 
   S** (f x) (f y)  R** x y"
  unfolding Nitpick.rtranclp_unfold
  by (metis (full_types) injD reflect_tranclp)

end

Theory Finite_Map_Ext

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

type_notation fmap ("(_ f /_)" [22, 21] 21)

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"

(*** Helper Lemmas **********************************************************)

subsection ‹Helper Lemmas›

lemma fmrel_on_fset_fmdom:
  "fmrel_on_fset (fmdom ym) f xm ym 
   k |∈| fmdom ym 
   k |∈| fmdom xm"
  by (metis fmdom_notD fmdom_notI fmrel_on_fsetD option.rel_sel)

(*** Finite Map Merge *******************************************************)

subsection ‹Merge Operation›

definition "fmmerge f xm ym 
  fmap_of_list (map
    (λk. (k, f (the (fmlookup xm k)) (the (fmlookup ym k))))
    (sorted_list_of_fset (fmdom xm |∩| fmdom ym)))"

lemma fmdom_fmmerge [simp]:
  "fmdom (fmmerge g xm ym) = fmdom xm |∩| fmdom ym"
  by (auto simp add: fmmerge_def fmdom_of_list)

lemma fmmerge_commut:
  assumes "x y. x  fmran' xm  f x y = f y x"
  shows "fmmerge f xm ym = fmmerge f ym xm"
proof -
  obtain zm where zm: "zm = sorted_list_of_fset (fmdom xm |∩| fmdom ym)"
    by auto
  with assms have
    "map (λk. (k, f (the (fmlookup xm k)) (the (fmlookup ym k)))) zm =
     map (λk. (k, f (the (fmlookup ym k)) (the (fmlookup xm k)))) zm"
    by (auto) (metis fmdom_notI fmran'I notin_fset option.collapse)
  thus ?thesis
    unfolding fmmerge_def zm
    by (metis (no_types, lifting) inf_commute)
qed

lemma fmrel_on_fset_fmmerge1 [intro]:
  assumes "x y z. z  fmran' zm  f x z  f y z  f (g x y) z"
  assumes "fmrel_on_fset (fmdom zm) f xm zm"
  assumes "fmrel_on_fset (fmdom zm) f ym zm"
  shows "fmrel_on_fset (fmdom zm) f (fmmerge g xm ym) zm"
proof -
  {
    fix x a b c
    assume "x |∈| fmdom zm"
    moreover hence "x |∈| fmdom xm |∩| fmdom ym"
      by (meson assms(2) assms(3) finterI fmrel_on_fset_fmdom)
    moreover assume "fmlookup xm x = Some a"
                and "fmlookup ym x = Some b"
                and "fmlookup zm x = Some c"
    moreover from assms calculation have "f (g a b) c"
      by (metis fmran'I fmrel_on_fsetD option.rel_inject(2))
    ultimately have
      "rel_option f (fmlookup (fmmerge g xm ym) x) (fmlookup zm x)"
      unfolding fmmerge_def fmlookup_of_list apply auto
      unfolding option_rel_Some2 apply (rule_tac ?x="g a b" in exI)
      unfolding map_of_map_restrict restrict_map_def
      by (auto simp: fmember.rep_eq)
  }
  with assms(2) assms(3) show ?thesis
    by (meson fmdomE fmrel_on_fsetI fmrel_on_fset_fmdom)
qed

lemma fmrel_on_fset_fmmerge2 [intro]:
  assumes "x y. x  fmran' xm  f x (g x y)"
  shows "fmrel_on_fset (fmdom ym) f xm (fmmerge g xm ym)"
proof -
  {
    fix x a b
    assume "x |∈| fmdom xm |∩| fmdom ym"
       and "fmlookup xm x = Some a"
       and "fmlookup ym x = Some b"
    hence "rel_option f (fmlookup xm x) (fmlookup (fmmerge g xm ym) x)"
      unfolding fmmerge_def fmlookup_of_list apply auto
      unfolding option_rel_Some1 apply (rule_tac ?x="g a b" in exI)
      by (auto simp add: map_of_map_restrict fmember.rep_eq assms fmran'I)
  }
  with assms show ?thesis
    apply auto
    apply (rule fmrel_on_fsetI)
    by (metis (full_types) finterD1 fmdomE fmdom_fmmerge fmdom_notD rel_option_None2)
qed

(*** Acyclicity *************************************************************)

subsection ‹Acyclicity›

abbreviation "acyclic_on xs r  (x. x  xs  (x, x)  r+)"

abbreviation "acyclicP_on xs r  acyclic_on xs {(x, y). r x y}"

lemma fmrel_acyclic:
  "acyclicP_on (fmran' xm) R 
   fmrel R++ xm ym 
   fmrel R ym xm 
   xm = ym"
  by (metis (full_types) fmap_ext fmran'I fmrel_cases option.sel
        tranclp.trancl_into_trancl tranclp_unfold)

lemma fmrel_acyclic':
  assumes "acyclicP_on (fmran' ym) R"
  assumes "fmrel R++ xm ym"
  assumes "fmrel R ym xm"
  shows "xm = ym"
proof -
  {
    fix x
    from assms(1) have
      "rel_option R++ (fmlookup xm x) (fmlookup ym x) 
       rel_option R (fmlookup ym x) (fmlookup xm x) 
       rel_option R (fmlookup xm x) (fmlookup ym x)"
      by (metis (full_types) fmdom'_notD fmlookup_dom'_iff
            fmran'I option.rel_sel option.sel
            tranclp_into_tranclp2 tranclp_unfold)
  }
  with assms show ?thesis
    unfolding fmrel_iff
    by (metis fmap.rel_mono_strong fmrelI fmrel_acyclic tranclp.simps)
qed

lemma fmrel_on_fset_acyclic:
  "acyclicP_on (fmran' xm) R 
   fmrel_on_fset (fmdom ym) R++ xm ym 
   fmrel_on_fset (fmdom xm) R ym xm 
   xm = ym"
  unfolding fmrel_on_fset_fmrel_restrict
  by (metis (no_types, lifting) fmdom_filter fmfilter_alt_defs(5)
        fmfilter_cong fmlookup_filter fmrel_acyclic fmrel_fmdom_eq
        fmrestrict_fset_dom option.simps(3))

lemma fmrel_on_fset_acyclic':
  "acyclicP_on (fmran' ym) R 
   fmrel_on_fset (fmdom ym) R++ xm ym 
   fmrel_on_fset (fmdom xm) R ym xm 
   xm = ym"
  unfolding fmrel_on_fset_fmrel_restrict
  by (metis (no_types, lifting) ffmember_filter fmdom_filter
        fmfilter_alt_defs(5) fmfilter_cong fmrel_acyclic'
        fmrel_fmdom_eq fmrestrict_fset_dom)

(*** Transitive Closures ****************************************************)

subsection ‹Transitive Closures›

lemma fmrel_trans:
  "(x y z. x  fmran' xm  P x y  Q y z  R x z) 
   fmrel P xm ym  fmrel Q ym zm  fmrel R xm zm"
  unfolding fmrel_iff
  by (metis fmdomE fmdom_notD fmran'I option.rel_inject(2) option.rel_sel)

lemma fmrel_on_fset_trans:
  "(x y z. x  fmran' xm  P x y  Q y z  R x z) 
   fmrel_on_fset (fmdom ym) P xm ym 
   fmrel_on_fset (fmdom zm) Q ym zm 
   fmrel_on_fset (fmdom zm) R xm zm"
  apply (rule fmrel_on_fsetI)
  unfolding option.rel_sel apply auto
  apply (meson fmdom_notI fmrel_on_fset_fmdom)
  by (metis fmdom_notI fmran'I fmrel_on_fsetD fmrel_on_fset_fmdom
            option.rel_sel option.sel)

lemma trancl_to_fmrel:
  "(fmrel f)++ xm ym  fmrel f++ xm ym"
  apply (induct rule: tranclp_induct)
  apply (simp add: fmap.rel_mono_strong)
  by (rule fmrel_trans; auto)

lemma fmrel_trancl_fmdom_eq:
  "(fmrel f)++ xm ym  fmdom xm = fmdom ym"
  by (induct rule: tranclp_induct; simp add: fmrel_fmdom_eq)

text ‹
  The proof was derived from the accepted answer on the website
  Stack Overflow that is available at
  @{url "https://stackoverflow.com/a/53585232/632199"}
  and provided with the permission of the author of the answer.›

lemma fmupd_fmdrop:
  "fmlookup xm k = Some x 
   xm = fmupd k x (fmdrop k xm)"
  apply (rule fmap_ext)
  unfolding fmlookup_drop fmupd_lookup
  by auto

lemma fmap_eqdom_Cons1:
  assumes "fmlookup xm i = None"
      and "fmdom (fmupd i x xm) = fmdom ym"
      and "fmrel R (fmupd i x xm) ym"
    shows "(z zm. fmlookup zm i = None  ym = (fmupd i z zm) 
                   R x z  fmrel R xm zm)"
proof -
  from assms(2) obtain y where "fmlookup ym i = Some y" by force
  then obtain z zm where z_zm: "ym = fmupd i z zm  fmlookup zm i = None"
    using fmupd_fmdrop by force
  {
    assume "¬ R x z"
    with z_zm have "¬ fmrel R (fmupd i x xm) ym"
      by (metis fmrel_iff fmupd_lookup option.simps(11))
  }
  with assms(3) moreover have "R x z" by auto
  {
    assume "¬ fmrel R xm zm"
    with assms(1) have "¬ fmrel R (fmupd i x xm) ym"
      by (metis fmrel_iff fmupd_lookup option.rel_sel z_zm)
  }
  with assms(3) moreover have "fmrel R xm zm" by auto
  ultimately show ?thesis using z_zm by blast
qed

text ‹
  The proof was derived from the accepted answer on the website
  Stack Overflow that is available at
  @{url "https://stackoverflow.com/a/53585232/632199"}
  and provided with the permission of the author of the answer.›

lemma fmap_eqdom_induct [consumes 2, case_names nil step]:
  assumes R: "fmrel R xm ym"
    and dom_eq: "fmdom xm = fmdom ym"
    and nil: "P (fmap_of_list []) (fmap_of_list [])"
    and step:
    "x xm y ym i.
    R x y; fmrel R xm ym; fmdom xm = fmdom ym; P xm ym 
    P (fmupd i x xm) (fmupd i y ym)"
  shows "P xm ym"
  using R dom_eq
proof (induct xm arbitrary: ym)
  case fmempty thus ?case
    by (metis fempty_iff fmdom_empty fmempty_of_list fmfilter_alt_defs(5)
              fmfilter_false fmrestrict_fset_dom local.nil)
next
  case (fmupd i x xm) show ?case
  proof -
    obtain y where "fmlookup ym i = Some y"
      by (metis fmupd.prems(1) fmrel_cases fmupd_lookup option.discI)
    from fmupd.hyps(2) fmupd.prems(1) fmupd.prems(2) obtain z zm where
      "fmlookup zm i = None" and
      ym_eq_z_zm: "ym = (fmupd i z zm)" and
      R_x_z: "R x z" and
      R_xm_zm: "fmrel R xm zm"
      using fmap_eqdom_Cons1 by metis
    hence dom_xm_eq_dom_zm: "fmdom xm = fmdom zm"
      using fmrel_fmdom_eq by blast
    with R_xm_zm fmupd.hyps(1) have "P xm zm" by blast
    with R_x_z R_xm_zm dom_xm_eq_dom_zm have
      "P (fmupd i x xm) (fmupd i z zm)"
      by (rule step)
    thus ?thesis by (simp add: ym_eq_z_zm)
  qed
qed

text ‹
  The proof was derived from the accepted answer on the website
  Stack Overflow that is available at
  @{url "https://stackoverflow.com/a/53585232/632199"}
  and provided with the permission of the author of the answer.›

lemma fmrel_to_rtrancl:
  assumes as_r: "reflp r"
      and rel_rpp_xm_ym: "fmrel r** xm ym"
    shows "(fmrel r)** xm ym"
proof -
  from rel_rpp_xm_ym have "fmdom xm = fmdom ym"
    using fmrel_fmdom_eq by blast
  with rel_rpp_xm_ym show "(fmrel r)** xm ym"
  proof (induct rule: fmap_eqdom_induct)
    case nil show ?case by auto
  next
    case (step x xm y ym i) show ?case
    proof -
      from step.hyps(1) have "(fmrel r)** (fmupd i x xm) (fmupd i y xm)"
      proof (induct rule: rtranclp_induct)
        case base show ?case by simp
      next
        case (step y z) show ?case
        proof -
          from as_r have "fmrel r xm xm"
            by (simp add: fmap.rel_reflp reflpD)
          with step.hyps(2) have "(fmrel r)** (fmupd i y xm) (fmupd i z xm)"
            by (simp add: fmrel_upd r_into_rtranclp)
          with step.hyps(3) show ?thesis by simp
        qed
      qed
      also from step.hyps(4) have "(fmrel r)** (fmupd i y xm) (fmupd i y ym)"
      proof (induct rule: rtranclp_induct)
        case base show ?case by simp
      next
        case (step ya za) show ?case
        proof -
          from step.hyps(2) as_r have "(fmrel r)** (fmupd i y ya) (fmupd i y za)"
            by (simp add: fmrel_upd r_into_rtranclp reflp_def)
          with step.hyps(3) show ?thesis by simp
        qed
      qed
      finally show ?thesis by simp
    qed
  qed
qed

text ‹
  The proof was derived from the accepted answer on the website
  Stack Overflow that is available at
  @{url "https://stackoverflow.com/a/53585232/632199"}
  and provided with the permission of the author of the answer.›

lemma fmrel_to_trancl:
  assumes "reflp r"
      and "fmrel r++ xm ym"
    shows "(fmrel r)++ xm ym"
proof -
  from assms(2) have "fmrel r** xm ym"
    by (drule_tac ?Ra="r**" in fmap.rel_mono_strong; auto)
  with assms(1) have "(fmrel r)** xm ym"
    by (simp add: fmrel_to_rtrancl)
  with assms(1) show ?thesis
    by (metis fmap.rel_reflp reflpD rtranclpD tranclp.r_into_trancl)
qed

lemma fmrel_tranclp_induct:
  "fmrel r++ a b 
   reflp r 
   (y. fmrel r a y  P y) 
   (y z. (fmrel r)++ a y  fmrel r y z  P y  P z)  P b"
  apply (drule fmrel_to_trancl, simp)
  by (erule tranclp_induct; simp)

lemma fmrel_converse_tranclp_induct:
  "fmrel r++ a b 
   reflp r 
   (y. fmrel r y b  P y) 
   (y z. fmrel r y z  fmrel r++ z b  P z  P y)  P a"
  apply (drule fmrel_to_trancl, simp)
  by (erule converse_tranclp_induct; simp add: trancl_to_fmrel)

lemma fmrel_tranclp_trans_induct:
  "fmrel r++ a b 
   reflp r 
   (x y. fmrel r x y  P x y) 
   (x y z. fmrel r++ x y  P x y  fmrel r++ y z  P y z  P x z) 
   P a b"
  apply (drule fmrel_to_trancl, simp)
  apply (erule tranclp_trans_induct, simp)
  using trancl_to_fmrel by blast

(*** Finite Map Size Calculation ********************************************)

subsection ‹Size Calculation›

text ‹
  The contents of the subsection was derived from the accepted answer
  on the website Stack Overflow that is available at
  @{url "https://stackoverflow.com/a/53244203/632199"}
  and provided with the permission of the author of the answer.›

abbreviation "tcf  (λ v::('a × nat). (λ r::nat. snd v + r))"

interpretation tcf: comp_fun_commute tcf
proof
  fix x y :: "'a × nat"
  show "tcf y  tcf x = tcf x  tcf y"
  proof -
    fix z
    have "(tcf y  tcf x) z = snd y + snd x + z" by auto
    also have "(tcf x  tcf y) z = snd y + snd x + z" by auto
    finally have "(tcf y  tcf x) z = (tcf x  tcf y) z" by auto
    thus "(tcf y  tcf x) = (tcf x  tcf y)" by auto
  qed
qed

lemma ffold_rec_exp:
  assumes "k |∈| fmdom x"
    and "ky = (k, the (fmlookup (fmmap f x) k))"
  shows "ffold tcf 0 (fset_of_fmap (fmmap f x)) =
        tcf ky (ffold tcf 0 ((fset_of_fmap (fmmap f x)) |-| {|ky|}))"
proof -
  have "ky |∈| (fset_of_fmap (fmmap f x))"
    using assms by auto
  thus ?thesis
    by (simp add: tcf.ffold_rec)
qed

lemma elem_le_ffold [intro]:
  "k |∈| fmdom x 
   f (the (fmlookup x k)) < Suc (ffold tcf 0 (fset_of_fmap (fmmap f x)))"
  by (subst ffold_rec_exp, auto)

lemma elem_le_ffold' [intro]:
  "z  fmran' x 
   f z < Suc (ffold tcf 0 (fset_of_fmap (fmmap f x)))"
  apply (erule fmran'E)
  apply (frule fmdomI)
  by (subst ffold_rec_exp, auto)

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

subsection ‹Code Setup›

abbreviation "fmmerge_fun f xm ym 
  fmap_of_list (map
    (λk. if k |∈| fmdom xm  k |∈| fmdom ym
         then (k, f (the (fmlookup xm k)) (the (fmlookup ym k)))
         else (k, undefined))
    (sorted_list_of_fset (fmdom xm |∩| fmdom ym)))"

lemma fmmerge_fun_simp [code_abbrev, simp]:
  "fmmerge_fun f xm ym = fmmerge f xm ym"
  unfolding fmmerge_def
  apply (rule_tac ?f="fmap_of_list" in HOL.arg_cong)
  by (simp add: notin_fset)

end

Theory Tuple

(*  Title:       Safe OCL
    Author:      Denis Nikiforov, March 2019
    Maintainer:  Denis Nikiforov <denis.nikif at gmail.com>
    License:     LGPL
*)
(* TODO: There are a lot of similar lemmas in the theory.
         They should be generalized *)
section ‹Tuples›
theory Tuple
  imports Finite_Map_Ext Transitive_Closure_Ext
begin

subsection ‹Definitions›

abbreviation "subtuple f xm ym  fmrel_on_fset (fmdom ym) f xm ym"

abbreviation "strict_subtuple f xm ym  subtuple f xm ym  xm  ym"

(*** Helper Lemmas **********************************************************)

subsection ‹Helper Lemmas›

lemma fmrel_to_subtuple:
  "fmrel r xm ym  subtuple r xm ym"
  unfolding fmrel_on_fset_fmrel_restrict by blast

lemma subtuple_eq_fmrel_fmrestrict_fset:
  "subtuple r xm ym = fmrel r (fmrestrict_fset (fmdom ym) xm) ym"
  by (simp add: fmrel_on_fset_fmrel_restrict)

lemma subtuple_fmdom:
  "subtuple f xm ym 
   subtuple g ym xm 
   fmdom xm = fmdom ym"
  by (meson fmrel_on_fset_fmdom fset_eqI)

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

subsection ‹Basic Properties›

lemma subtuple_refl:
  "reflp R  subtuple R xm xm"
  by (simp add: fmrel_on_fsetI option.rel_reflp reflpD)

lemma subtuple_mono [mono]:
  "(x y. x  fmran' xm  y  fmran' ym  f x y  g x y) 
   subtuple f xm ym  subtuple g xm ym"
  apply (auto)
  apply (rule fmrel_on_fsetI)
  apply (drule_tac ?P="f" and ?m="xm" and ?n="ym" in fmrel_on_fsetD, simp)
  apply (erule option.rel_cases, simp)
  by (auto simp add: option.rel_sel fmran'I)

lemma strict_subtuple_mono [mono]:
  "(x y. x  fmran' xm  y  fmran' ym  f x y  g x y) 
   strict_subtuple f xm ym  strict_subtuple g xm ym"
  using subtuple_mono by blast

lemma subtuple_antisym:
  assumes "subtuple (λx y. f x y  x = y) xm ym"
  assumes "subtuple (λx y. f x y  ¬ f y x  x = y) ym xm"
  shows "xm = ym"
proof (rule fmap_ext)
  fix x
  from assms have "fmdom xm = fmdom ym"
    using subtuple_fmdom by blast
  with assms have "fmrel (λx y. f x y  x = y) xm ym"
      and "fmrel (λx y. f x y  ¬ f y x  x = y) ym xm"
    by (metis (mono_tags, lifting) fmrel_code fmrel_on_fset_alt_def)+
  thus "fmlookup xm x = fmlookup ym x"
    apply (erule_tac ?x="x" in fmrel_cases)
    by (erule_tac ?x="x" in fmrel_cases, auto)+
qed

lemma strict_subtuple_antisym:
  "strict_subtuple (λx y. f x y  x = y) xm ym 
   strict_subtuple (λx y. f x y  ¬ f y x  x = y) ym xm  False"
  by (auto simp add: subtuple_antisym)

lemma subtuple_acyclic:
  assumes "acyclicP_on (fmran' xm) P"
  assumes "subtuple (λx y. P x y  x = y)++ xm ym"
  assumes "subtuple (λx y. P x y  x = y) ym xm"
  shows "xm = ym"
proof (rule fmap_ext)
  fix x
  from assms have fmdom_eq: "fmdom xm = fmdom ym"
    using subtuple_fmdom by blast
  have "x a b. acyclicP_on (fmran' xm) P 
     fmlookup xm x = Some a 
     fmlookup ym x = Some b 
    P** a b  P b a  a = b  a = b"
    by (meson Nitpick.tranclp_unfold fmran'I rtranclp_into_tranclp1)
  moreover from fmdom_eq assms(2) have "fmrel P** xm ym"
    unfolding fmrel_on_fset_fmrel_restrict apply auto
    by (metis fmrestrict_fset_dom)
  moreover from fmdom_eq assms(3) have "fmrel (λx y. P x y  x = y) ym xm"
    unfolding fmrel_on_fset_fmrel_restrict apply auto
    by (metis fmrestrict_fset_dom)
  ultimately show "fmlookup xm x = fmlookup ym x"
    apply (erule_tac ?x="x" in fmrel_cases)
    apply (erule_tac ?x="x" in fmrel_cases, simp_all)+
    using assms(1) by blast
qed

lemma subtuple_acyclic':
  assumes "acyclicP_on (fmran' ym) P"
  assumes "subtuple (λx y. P x y  x = y)++ xm ym"
  assumes "subtuple (λx y. P x y  x = y) ym xm"
  shows "xm = ym"
proof (rule fmap_ext)
  fix x
  from assms have fmdom_eq: "fmdom xm = fmdom ym"
    using subtuple_fmdom by blast
  have "x a b. acyclicP_on (fmran' ym) P 
     fmlookup xm x = Some a 
     fmlookup ym x = Some b 
    P** a b  P b a  a = b  a = b"
    by (meson Nitpick.tranclp_unfold fmran'I rtranclp_into_tranclp2)
  moreover from fmdom_eq assms(2) have "fmrel P** xm ym"
    unfolding fmrel_on_fset_fmrel_restrict apply auto
    by (metis fmrestrict_fset_dom)
  moreover from fmdom_eq assms(3) have "fmrel (λx y. P x y  x = y) ym xm"
    unfolding fmrel_on_fset_fmrel_restrict apply auto
    by (metis fmrestrict_fset_dom)
  ultimately show "fmlookup xm x = fmlookup ym x"
    apply (erule_tac ?x="x" in fmrel_cases)
    apply (erule_tac ?x="x" in fmrel_cases, simp_all)+
    using assms(1) by blast
qed

lemma subtuple_acyclic'':
  "acyclicP_on (fmran' ym) R 
   subtuple R** xm ym 
   subtuple R ym xm 
   xm = ym"
  by (metis (no_types, lifting) subtuple_acyclic' subtuple_mono tranclp_eq_rtranclp)

lemma strict_subtuple_trans:
  "acyclicP_on (fmran' xm) P 
   strict_subtuple (λx y. P x y  x = y)++ xm ym 
   strict_subtuple (λx y. P x y  x = y) ym zm 
   strict_subtuple (λx y. P x y  x = y)++ xm zm"
  apply auto
  apply (rule fmrel_on_fset_trans, auto)
  by (drule_tac ?ym="ym" in subtuple_acyclic; auto)

lemma strict_subtuple_trans':
  "acyclicP_on (fmran' zm) P 
   strict_subtuple (λx y. P x y  x = y) xm ym 
   strict_subtuple (λx y. P x y  x = y)++ ym zm 
   strict_subtuple (λx y. P x y  x = y)++ xm zm"
  apply auto
  apply (rule fmrel_on_fset_trans, auto)
  by (drule_tac ?xm="ym" in subtuple_acyclic'; auto)

lemma strict_subtuple_trans'':
  "acyclicP_on (fmran' zm) R 
   strict_subtuple R xm ym 
   strict_subtuple R** ym zm 
   strict_subtuple R** xm zm"
  apply auto
  apply (rule fmrel_on_fset_trans, auto)
  by (drule_tac ?xm="ym" in subtuple_acyclic''; auto)

lemma strict_subtuple_trans''':
  "acyclicP_on (fmran' zm) P 
   strict_subtuple (λx y. P x y  x = y) xm ym 
   strict_subtuple (λx y. P x y  x = y)** ym zm 
   strict_subtuple (λx y. P x y  x = y)** xm zm"
  apply auto
  apply (rule fmrel_on_fset_trans, auto)
  by (drule_tac ?xm="ym" in subtuple_acyclic'; auto)

lemma subtuple_fmmerge2 [intro]:
  "(x y. x  fmran' xm  f x (g x y)) 
   subtuple f xm (fmmerge g xm ym)"
  by (rule_tac ?S="fmdom ym" in fmrel_on_fsubset; auto)

(*** Transitive Closures ****************************************************)

subsection ‹Transitive Closures›

lemma trancl_to_subtuple:
  "(subtuple r)++ xm ym 
   subtuple r++ xm ym"
  apply (induct rule: tranclp_induct)
  apply (metis subtuple_mono tranclp.r_into_trancl)
  by (rule fmrel_on_fset_trans; auto)

lemma rtrancl_to_subtuple:
  "(subtuple r)** xm ym 
   subtuple r** xm ym"
  apply (induct rule: rtranclp_induct)
  apply (simp add: fmap.rel_refl_strong fmrel_to_subtuple)
  by (rule fmrel_on_fset_trans; auto)

lemma fmrel_to_subtuple_trancl:
  "reflp r 
   (fmrel r)++ (fmrestrict_fset (fmdom ym) xm) ym 
   (subtuple r)++ xm ym"
  apply (frule trancl_to_fmrel)
  apply (rule_tac ?r="r" in fmrel_tranclp_induct, auto)
  apply (metis (no_types, lifting) fmrel_fmdom_eq
          subtuple_eq_fmrel_fmrestrict_fset tranclp.r_into_trancl)
  by (meson fmrel_to_subtuple tranclp.simps)

lemma subtuple_to_trancl:
  "reflp r 
   subtuple r++ xm ym 
   (subtuple r)++ xm ym"
  apply (rule fmrel_to_subtuple_trancl)
  unfolding fmrel_on_fset_fmrel_restrict
  by (simp_all add: fmrel_to_trancl)

lemma trancl_to_strict_subtuple:
  "acyclicP_on (fmran' ym) R 
   (strict_subtuple R)++ xm ym 
   strict_subtuple R** xm ym"
  apply (erule converse_tranclp_induct)
  apply (metis r_into_rtranclp strict_subtuple_mono)
  using strict_subtuple_trans'' by blast

lemma trancl_to_strict_subtuple':
  "acyclicP_on (fmran' ym) R 
   (strict_subtuple (λx y. R x y  x = y))++ xm ym 
   strict_subtuple (λx y. R x y  x = y)** xm ym"
  apply (erule converse_tranclp_induct)
  apply (metis (no_types, lifting) r_into_rtranclp strict_subtuple_mono)
  using strict_subtuple_trans''' by blast

lemma subtuple_rtranclp_intro:
  assumes "xm ym. R (f xm) (f ym)  subtuple R xm ym"
      and "bij_on_trancl R f"
      and "R** (f xm) (f ym)"
    shows "subtuple R** xm ym"
proof -
  have "(λxm ym. R (f xm) (f ym))** xm ym"
    apply (insert assms(2) assms(3))
    by (rule reflect_rtranclp; auto)
  with assms(1) have "(subtuple R)** xm ym"
    by (metis (mono_tags, lifting) mono_rtranclp)
  hence "subtuple R** xm ym"
    by (rule rtrancl_to_subtuple)
  thus ?thesis by simp
qed

lemma strict_subtuple_rtranclp_intro:
  assumes "xm ym. R (f xm) (f ym) 
           strict_subtuple (λx y. R x y  x = y) xm ym"
      and "bij_on_trancl R f"
      and "acyclicP_on (fmran' ym) R"
      and "R++ (f xm) (f ym)"
    shows "strict_subtuple R** xm ym"
proof -
  have "(λxm ym. R (f xm) (f ym))++ xm ym"
    apply (insert assms(1) assms(2) assms(4))
    by (rule reflect_tranclp; auto)
  hence "(strict_subtuple (λx y. R x y  x = y))++ xm ym"
    by (rule tranclp_trans_induct;
        auto simp add: assms(1) tranclp.r_into_trancl)
  with assms(3) have "strict_subtuple (λx y. R x y  x = y)** xm ym"
    by (rule trancl_to_strict_subtuple')
  thus ?thesis by simp
qed

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

subsection ‹Code Setup›

abbreviation "subtuple_fun f xm ym 
  fBall (fmdom ym) (λx. rel_option f (fmlookup xm x) (fmlookup ym x))"

abbreviation "strict_subtuple_fun f xm ym 
  subtuple_fun f xm ym  xm  ym"

lemma subtuple_fun_simp [code_abbrev, simp]:
  "subtuple_fun f xm ym = subtuple f xm ym"
  by (simp add: fmrel_on_fset_alt_def)

lemma strict_subtuple_fun_simp [code_abbrev, simp]:
  "strict_subtuple_fun f xm ym = strict_subtuple f xm ym"
  by simp

end

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›

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)

code_pred unique_closest_attribute .

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' .

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 .

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

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' .

code_pred has_literal' .

end

Theory OCL_Basic_Types

(*  Title:       Safe OCL
    Author:      Denis Nikiforov, March 2019
    Maintainer:  Denis Nikiforov <denis.nikif at gmail.com>
    License:     LGPL
*)
chapter ‹Basic Types›
theory OCL_Basic_Types
  imports Main "HOL-Library.FSet" "HOL-Library.Phantom_Type"
begin

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

section ‹Definition›

text ‹
  Basic types are parameterized over classes.›

type_synonym 'a enum = "('a, String.literal) phantom"
type_synonym elit = String.literal

datatype ('a :: order) basic_type =
  OclAny
| OclVoid
| Boolean
| Real
| Integer
| UnlimitedNatural
| String
| ObjectType 'a ("_𝒯" [0] 1000)
| Enum "'a enum"

inductive basic_subtype (infix "B" 65) where
  "OclVoid B Boolean"
| "OclVoid B UnlimitedNatural"
| "OclVoid B String"
| "OclVoid B 𝒞𝒯"
| "OclVoid B Enum "

| "UnlimitedNatural B Integer"
| "Integer B Real"
| "𝒞 < 𝒟  𝒞𝒯 B 𝒟𝒯"

| "Boolean B OclAny"
| "Real B OclAny"
| "String B OclAny"
| "𝒞𝒯 B OclAny"
| "Enum  B OclAny"

declare basic_subtype.intros [intro!]

inductive_cases basic_subtype_x_OclAny [elim!]: "τ B OclAny"
inductive_cases basic_subtype_x_OclVoid [elim!]: "τ B OclVoid"
inductive_cases basic_subtype_x_Boolean [elim!]: "τ B Boolean"
inductive_cases basic_subtype_x_Real [elim!]: "τ B Real"
inductive_cases basic_subtype_x_Integer [elim!]: "τ B Integer"
inductive_cases basic_subtype_x_UnlimitedNatural [elim!]: "τ B UnlimitedNatural"
inductive_cases basic_subtype_x_String [elim!]: "τ B String"
inductive_cases basic_subtype_x_ObjectType [elim!]: "τ B 𝒞𝒯"
inductive_cases basic_subtype_x_Enum [elim!]: "τ B Enum "

inductive_cases basic_subtype_OclAny_x [elim!]: "OclAny B σ"
inductive_cases basic_subtype_ObjectType_x [elim!]: "𝒞𝒯 B σ"

lemma basic_subtype_asym:
  "τ B σ  σ B τ  False"
  by (induct rule: basic_subtype.induct, auto)

(*** Partial Order of Basic Types *******************************************)

section ‹Partial Order of Basic Types›

instantiation basic_type :: (order) order
begin

definition "(<)  basic_subtype++"
definition "(≤)  basic_subtype**"

(*** Strict Introduction Rules **********************************************)

subsection ‹Strict Introduction Rules›

lemma type_less_x_OclAny_intro [intro]:
  "τ  OclAny  τ < OclAny"
proof -
  have "basic_subtype++ OclVoid OclAny"
    by (rule_tac ?b="Boolean" in tranclp.trancl_into_trancl; auto)
  moreover have "basic_subtype++ Integer OclAny"
    by (rule_tac ?b="Real" in tranclp.trancl_into_trancl; auto)
  moreover hence "basic_subtype++ UnlimitedNatural OclAny"
    by (rule_tac ?b="Integer" in tranclp_into_tranclp2; auto)
  ultimately show "τ  OclAny  τ < OclAny"
    unfolding less_basic_type_def
    by (induct τ, auto)
qed

lemma type_less_OclVoid_x_intro [intro]:
  "τ  OclVoid  OclVoid < τ"
proof -
  have "basic_subtype++ OclVoid OclAny"
    by (rule_tac ?b="Boolean" in tranclp.trancl_into_trancl; auto)
  moreover have "basic_subtype++ OclVoid Integer"
    by (rule_tac ?b="UnlimitedNatural" in tranclp.trancl_into_trancl; auto)
  moreover hence "basic_subtype++ OclVoid Real"
    by (rule_tac ?b="Integer" in tranclp.trancl_into_trancl; auto)
  ultimately show "τ  OclVoid  OclVoid < τ"
    unfolding less_basic_type_def
    by (induct τ; auto)
qed

lemma type_less_x_Real_intro [intro]:
  "τ = UnlimitedNatural  τ < Real"
  "τ = Integer  τ < Real"
  unfolding less_basic_type_def
  by (rule rtranclp_into_tranclp2, auto)

lemma type_less_x_Integer_intro [intro]:
  "τ = UnlimitedNatural  τ < Integer"
  unfolding less_basic_type_def
  by (rule rtranclp_into_tranclp2, auto)

lemma type_less_x_ObjectType_intro [intro]:
  "τ = 𝒞𝒯  𝒞 < 𝒟  τ < 𝒟𝒯"
  unfolding less_basic_type_def
  using dual_order.order_iff_strict by blast

(*** Strict Elimination Rules ***********************************************)

subsection ‹Strict Elimination Rules›

lemma type_less_x_OclAny [elim!]:
  "τ < OclAny 
   (τ = OclVoid  P) 
   (τ = Boolean  P) 
   (τ = Integer  P) 
   (τ = UnlimitedNatural  P) 
   (τ = Real  P) 
   (τ = String  P) 
   (. τ = Enum   P)  
   (𝒞. τ = 𝒞𝒯  P)  P"
  unfolding less_basic_type_def
  by (induct rule: converse_tranclp_induct; auto)

lemma type_less_x_OclVoid [elim!]:
  "τ < OclVoid  P"
  unfolding less_basic_type_def
  by (induct rule: converse_tranclp_induct; auto)

lemma type_less_x_Boolean [elim!]:
  "τ < Boolean 
   (τ = OclVoid  P)  P"
  unfolding less_basic_type_def
  by (induct rule: converse_tranclp_induct; auto)

lemma type_less_x_Real [elim!]:
  "τ < Real 
   (τ = OclVoid  P) 
   (τ = UnlimitedNatural  P) 
   (τ = Integer  P)  P"
  unfolding less_basic_type_def
  by (induct rule: converse_tranclp_induct; auto)

lemma type_less_x_Integer [elim!]:
  "τ < Integer 
   (τ = OclVoid  P) 
   (τ = UnlimitedNatural  P)  P"
  unfolding less_basic_type_def
  by (induct rule: converse_tranclp_induct; auto)

lemma type_less_x_UnlimitedNatural [elim!]:
  "τ < UnlimitedNatural 
   (τ = OclVoid  P)  P"
  unfolding less_basic_type_def
  by (induct rule: converse_tranclp_induct; auto)

lemma type_less_x_String [elim!]:
  "τ < String 
   (τ = OclVoid  P)  P"
  unfolding less_basic_type_def
  by (induct rule: converse_tranclp_induct; auto)

lemma type_less_x_ObjectType [elim!]:
  "τ < 𝒟𝒯 
   (τ = OclVoid  P) 
   (𝒞. τ = 𝒞𝒯  𝒞 < 𝒟  P)  P"
  unfolding less_basic_type_def
  apply (induct rule: converse_tranclp_induct)
  apply auto[1]
  using less_trans by auto

lemma type_less_x_Enum [elim!]:
  "τ < Enum  
   (τ = OclVoid  P)  P"
  unfolding less_basic_type_def
  by (induct rule: converse_tranclp_induct; auto)

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

subsection ‹Properties›

lemma basic_subtype_irrefl:
  "τ < τ  False"
  for τ :: "'a basic_type"
  by (cases τ; auto)

lemma tranclp_less_basic_type:
  "(τ, σ)  {(τ, σ). τ B σ}+  τ < σ"
  by (simp add: tranclp_unfold less_basic_type_def)

lemma basic_subtype_acyclic:
  "acyclicP basic_subtype"
  apply (rule acyclicI)
  using OCL_Basic_Types.basic_subtype_irrefl
    OCL_Basic_Types.tranclp_less_basic_type by auto

lemma less_le_not_le_basic_type:
  "τ < σ  τ  σ  ¬ σ  τ"
  for τ σ :: "'a basic_type"
  unfolding less_basic_type_def less_eq_basic_type_def
  apply (rule iffI; auto)
  apply (metis (mono_tags) basic_subtype_irrefl
      less_basic_type_def tranclp_rtranclp_tranclp)
  by (drule rtranclpD; auto)

lemma antisym_basic_type:
  "τ  σ  σ  τ  τ = σ"
  for τ σ :: "'a basic_type"
  unfolding less_eq_basic_type_def less_basic_type_def
  by (metis (mono_tags, lifting) less_eq_basic_type_def
      less_le_not_le_basic_type less_basic_type_def rtranclpD)

lemma order_refl_basic_type [iff]:
  "τ  τ"
  for τ :: "'a basic_type"
  by (simp add: less_eq_basic_type_def)

instance
  by standard (auto simp add: less_eq_basic_type_def
        less_le_not_le_basic_type antisym_basic_type)

end

(*** Non-Strict Introduction Rules ******************************************)

subsection ‹Non-Strict Introduction Rules›

lemma type_less_eq_x_OclAny_intro [intro]:
  "τ  OclAny"
  using order.order_iff_strict by auto

lemma type_less_eq_OclVoid_x_intro [intro]:
  "OclVoid  τ"
  using order.order_iff_strict by auto

lemma type_less_eq_x_Real_intro [intro]:
  "τ = UnlimitedNatural  τ  Real"
  "τ = Integer  τ  Real"
  using order.order_iff_strict by auto

lemma type_less_eq_x_Integer_intro [intro]:
  "τ = UnlimitedNatural  τ  Integer"
  using order.order_iff_strict by auto

lemma type_less_eq_x_ObjectType_intro [intro]:
  "τ = 𝒞𝒯  𝒞  𝒟  τ  𝒟𝒯"
  using order.order_iff_strict by fastforce

(*** Non-Strict Elimination Rules *******************************************)

subsection ‹Non-Strict Elimination Rules›

lemma type_less_eq_x_OclAny [elim!]:
  "τ  OclAny 
   (τ = OclVoid  P) 
   (τ = OclAny  P) 
   (τ = Boolean  P) 
   (τ = Integer  P) 
   (τ = UnlimitedNatural  P) 
   (τ = Real  P) 
   (τ = String  P) 
   (. τ = Enum   P)  
   (𝒞. τ = 𝒞𝒯  P)  P"
  by (drule le_imp_less_or_eq; auto)

lemma type_less_eq_x_OclVoid [elim!]:
  "τ  OclVoid 
   (τ = OclVoid  P)  P"
  by (drule le_imp_less_or_eq; auto)

lemma type_less_eq_x_Boolean [elim!]:
  "τ  Boolean 
   (τ = OclVoid  P) 
   (τ = Boolean  P)  P"
  by (drule le_imp_less_or_eq; auto)

lemma type_less_eq_x_Real [elim!]:
  "τ  Real 
   (τ = OclVoid  P) 
   (τ = UnlimitedNatural  P) 
   (τ = Integer  P) 
   (τ = Real  P)  P"
  by (drule le_imp_less_or_eq; auto)

lemma type_less_eq_x_Integer [elim!]:
  "τ  Integer 
   (τ = OclVoid  P) 
   (τ = UnlimitedNatural  P) 
   (τ = Integer  P)  P"
  by (drule le_imp_less_or_eq; auto)

lemma type_less_eq_x_UnlimitedNatural [elim!]:
  "τ  UnlimitedNatural 
   (τ = OclVoid  P) 
   (τ = UnlimitedNatural  P)  P"
  by (drule le_imp_less_or_eq; auto)

lemma type_less_eq_x_String [elim!]:
  "τ  String 
   (τ = OclVoid  P) 
   (τ = String  P)  P"
  by (drule le_imp_less_or_eq; auto)

lemma type_less_eq_x_ObjectType [elim!]:
  "τ  𝒟𝒯 
   (τ = OclVoid  P) 
   (𝒞. τ = 𝒞𝒯  𝒞  𝒟  P)  P"
  by (drule le_imp_less_or_eq; auto)

lemma type_less_eq_x_Enum [elim!]:
  "τ  Enum  
   (τ = OclVoid  P) 
   (τ = Enum   P)  P"
  by (drule le_imp_less_or_eq; auto)

(*** Simplification Rules ***************************************************)

subsection ‹Simplification Rules›

lemma basic_type_less_left_simps [simp]:
  "OclAny < σ = False"
  "OclVoid < σ = (σ  OclVoid)"
  "Boolean < σ = (σ = OclAny)"
  "Real < σ = (σ = OclAny)"
  "Integer < σ = (σ = OclAny  σ = Real)"
  "UnlimitedNatural < σ = (σ = OclAny  σ = Real  σ = Integer)"
  "String < σ = (σ = OclAny)"
  "ObjectType 𝒞 < σ = (𝒟. σ = OclAny  σ = ObjectType 𝒟  𝒞 < 𝒟)"
  "Enum  < σ = (σ = OclAny)"
  by (induct σ, auto)

lemma basic_type_less_right_simps [simp]:
  "τ < OclAny = (τ  OclAny)"
  "τ < OclVoid = False"
  "τ < Boolean = (τ = OclVoid)"
  "τ < Real = (τ = Integer  τ = UnlimitedNatural  τ = OclVoid)"
  "τ < Integer = (τ = UnlimitedNatural  τ = OclVoid)"
  "τ < UnlimitedNatural = (τ = OclVoid)"
  "τ < String = (τ = OclVoid)"
  "τ < ObjectType 𝒟 = (𝒞. τ = ObjectType 𝒞  𝒞 < 𝒟  τ = OclVoid)"
  "τ < Enum  = (τ = OclVoid)"
  by auto

(*** Upper Semilattice of Basic Types ***************************************)

section ‹Upper Semilattice of Basic Types›

notation sup (infixl "" 65)

instantiation basic_type :: (semilattice_sup) semilattice_sup
begin

(* We use "case"-style because it works faster *)
fun sup_basic_type where
  "𝒞𝒯  σ = (case σ of OclVoid  𝒞𝒯 | 𝒟𝒯  𝒞  𝒟𝒯 | _  OclAny)"
| "τ  σ = (if τ  σ then σ else (if σ  τ then τ else OclAny))"

lemma sup_ge1_ObjectType:
  "𝒞𝒯  𝒞𝒯  σ"
  apply (induct σ; simp add: basic_subtype.simps
        less_eq_basic_type_def r_into_rtranclp)
  by (metis Nitpick.rtranclp_unfold basic_subtype.intros(8)
        le_imp_less_or_eq r_into_rtranclp sup_ge1)

lemma sup_ge1_basic_type:
  "τ  τ  σ"
  for τ σ :: "'a basic_type"
  apply (induct τ, auto)
  using sup_ge1_ObjectType by auto

lemma sup_commut_basic_type:
  "τ  σ = σ  τ"
  for τ σ :: "'a basic_type"
  by (induct τ; induct σ; auto simp add: sup.commute)

lemma sup_least_basic_type:
  "τ  ρ  σ  ρ  τ  σ  ρ"
  for τ σ ρ :: "'a basic_type"
  by (induct ρ; auto)

instance
  by standard (auto simp add: sup_ge1_basic_type
        sup_commut_basic_type sup_least_basic_type)

end

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

section ‹Code Setup›

code_pred basic_subtype .

fun basic_subtype_fun :: "'a::order basic_type  'a basic_type  bool" where
  "basic_subtype_fun OclAny σ = False"
| "basic_subtype_fun OclVoid σ = (σ  OclVoid)"
| "basic_subtype_fun Boolean σ = (σ = OclAny)"
| "basic_subtype_fun Real σ = (σ = OclAny)"
| "basic_subtype_fun Integer σ = (σ = Real  σ = OclAny)"
| "basic_subtype_fun UnlimitedNatural σ = (σ = Integer  σ = Real  σ = OclAny)"
| "basic_subtype_fun String σ = (σ = OclAny)"
| "basic_subtype_fun 𝒞𝒯 σ = (case σ
    of 𝒟𝒯  𝒞 < 𝒟
     | OclAny  True
     | _  False)"
| "basic_subtype_fun (Enum _) σ = (σ = OclAny)"

lemma less_basic_type_code [code]:
  "(<) = basic_subtype_fun"
proof (intro ext iffI)
  fix τ σ :: "'a basic_type"
  show "τ < σ  basic_subtype_fun τ σ"
    apply (cases σ; auto)
    using basic_subtype_fun.elims(3) by fastforce
  show "basic_subtype_fun τ σ  τ < σ"
    apply (erule basic_subtype_fun.elims, auto)
    by (cases σ, auto)
qed

lemma less_eq_basic_type_code [code]:
  "(≤) = (λx y. basic_subtype_fun x y  x = y)"
  unfolding dual_order.order_iff_strict less_basic_type_code
  by auto

end

Theory OCL_Types

(*  Title:       Safe OCL
    Author:      Denis Nikiforov, March 2019
    Maintainer:  Denis Nikiforov <denis.nikif at gmail.com>
    License:     LGPL
*)
chapter ‹Types›
theory OCL_Types
  imports OCL_Basic_Types Errorable Tuple
begin

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

section ‹Definition›

text ‹
  Types are parameterized over classes.›

type_synonym telem = String.literal

datatype (plugins del: size) 'a type =
  OclSuper
| Required "'a basic_type" ("_[1]" [1000] 1000)
| Optional "'a basic_type" ("_[?]" [1000] 1000)
| Collection "'a type"
| Set "'a type"
| OrderedSet "'a type"
| Bag "'a type"
| Sequence "'a type"
| Tuple "telem f 'a type"

text ‹
  We define the @{text OclInvalid} type separately, because we
  do not need types like @{text "Set(OclInvalid)"} in the theory.
  The @{text "OclVoid[1]"} type is not equal to @{text OclInvalid}.
  For example, @{text "Set(OclVoid[1])"} could theoretically be
  a valid type of the following expression:›

text ‹Set{null}->excluding(null)›

definition "OclInvalid :: 'a type  "

instantiation type :: (type) size
begin

primrec size_type :: "'a type  nat" where
  "size_type OclSuper = 0"
| "size_type (Required τ) = 0"
| "size_type (Optional τ) = 0"
| "size_type (Collection τ) = Suc (size_type τ)"
| "size_type (Set τ) = Suc (size_type τ)"
| "size_type (OrderedSet τ) = Suc (size_type τ)"
| "size_type (Bag τ) = Suc (size_type τ)"
| "size_type (Sequence τ) = Suc (size_type τ)"
| "size_type (Tuple π) = Suc (ffold tcf 0 (fset_of_fmap (fmmap size_type π)))"

instance ..

end

inductive subtype :: "'a::order type  'a type  bool" (infix "" 65) where
  "τ B σ  τ[1]  σ[1]"
| "τ B σ  τ[?]  σ[?]"
| "τ[1]  τ[?]"
| "OclAny[?]  OclSuper"

| "τ  σ  Collection τ  Collection σ"
| "τ  σ  Set τ  Set σ"
| "τ  σ  OrderedSet τ  OrderedSet σ"
| "τ  σ  Bag τ  Bag σ"
| "τ  σ  Sequence τ  Sequence σ"
| "Set τ  Collection τ"
| "OrderedSet τ  Collection τ"
| "Bag τ  Collection τ"
| "Sequence τ  Collection τ"
| "Collection OclSuper  OclSuper"

| "strict_subtuple (λτ σ. τ  σ  τ = σ) π ξ 
   Tuple π  Tuple ξ"
| "Tuple π  OclSuper"

declare subtype.intros [intro!]

inductive_cases subtype_x_OclSuper [elim!]: "τ  OclSuper"
inductive_cases subtype_x_Required [elim!]: "τ  σ[1]"
inductive_cases subtype_x_Optional [elim!]: "τ  σ[?]"
inductive_cases subtype_x_Collection [elim!]: "τ  Collection σ"
inductive_cases subtype_x_Set [elim!]: "τ  Set σ"
inductive_cases subtype_x_OrderedSet [elim!]: "τ  OrderedSet σ"
inductive_cases subtype_x_Bag [elim!]: "τ  Bag σ"
inductive_cases subtype_x_Sequence [elim!]: "τ  Sequence σ"
inductive_cases subtype_x_Tuple [elim!]: "τ  Tuple π"

inductive_cases subtype_OclSuper_x [elim!]: "OclSuper  σ"
inductive_cases subtype_Collection_x [elim!]: "Collection τ  σ"

lemma subtype_asym:
  "τ  σ  σ  τ  False"
  apply (induct rule: subtype.induct)
  using basic_subtype_asym apply auto
  using subtuple_antisym by fastforce

(*** Constructors Bijectivity on Transitive Closures ************************)

section ‹Constructors Bijectivity on Transitive Closures›

lemma Required_bij_on_trancl [simp]:
  "bij_on_trancl subtype Required"
  by (auto simp add: inj_def)

lemma not_subtype_Optional_Required:
  "subtype++ τ[?] σ  σ = ρ[1]  P"
  by (induct arbitrary: ρ rule: tranclp_induct; auto)

lemma Optional_bij_on_trancl [simp]:
  "bij_on_trancl subtype Optional"
  apply (auto simp add: inj_def)
  using not_subtype_Optional_Required by blast

lemma subtype_tranclp_Collection_x:
  "subtype++ (Collection τ) σ 
   (ρ. σ = Collection ρ  subtype++ τ ρ  P) 
   (σ = OclSuper  P)  P"
  apply (induct rule: tranclp_induct, auto)
  by (metis subtype_Collection_x subtype_OclSuper_x tranclp.trancl_into_trancl)

lemma Collection_bij_on_trancl [simp]:
  "bij_on_trancl subtype Collection"
  apply (auto simp add: inj_def)
  using subtype_tranclp_Collection_x by auto

lemma Set_bij_on_trancl [simp]:
  "bij_on_trancl subtype Set"
  by (auto simp add: inj_def)

lemma OrderedSet_bij_on_trancl [simp]:
  "bij_on_trancl subtype OrderedSet"
  by (auto simp add: inj_def)

lemma Bag_bij_on_trancl [simp]:
  "bij_on_trancl subtype Bag"
  by (auto simp add: inj_def)

lemma Sequence_bij_on_trancl [simp]:
  "bij_on_trancl subtype Sequence"
  by (auto simp add: inj_def)

lemma Tuple_bij_on_trancl [simp]:
  "bij_on_trancl subtype Tuple"
  by (auto simp add: inj_def)

(*** Partial Order of Types *************************************************)

section ‹Partial Order of Types›

instantiation type :: (order) order
begin

definition "(<)  subtype++"
definition "(≤)  subtype**"

(*** Strict Introduction Rules **********************************************)

subsection ‹Strict Introduction Rules›

lemma type_less_x_Required_intro [intro]:
  "τ = ρ[1]  ρ < σ  τ < σ[1]"
  unfolding less_type_def less_basic_type_def
  by simp (rule preserve_tranclp; auto)

lemma type_less_x_Optional_intro [intro]:
  "τ = ρ[1]  ρ  σ  τ < σ[?]"
  "τ = ρ[?]  ρ < σ  τ < σ[?]"
  unfolding less_type_def less_basic_type_def less_eq_basic_type_def
  apply simp_all
  apply (rule preserve_rtranclp''; auto)
  by (rule preserve_tranclp; auto)

lemma type_less_x_Collection_intro [intro]:
  "τ = Collection ρ  ρ < σ  τ < Collection σ"
  "τ = Set ρ  ρ  σ  τ < Collection σ"
  "τ = OrderedSet ρ  ρ  σ  τ < Collection σ"
  "τ = Bag ρ  ρ  σ  τ < Collection σ"
  "τ = Sequence ρ  ρ  σ  τ < Collection σ"
  unfolding less_type_def less_eq_type_def
  apply simp_all
  apply (rule_tac ?f="Collection" in preserve_tranclp; auto)
  apply (rule preserve_rtranclp''; auto)
  apply (rule preserve_rtranclp''; auto)
  apply (rule preserve_rtranclp''; auto)
  by (rule preserve_rtranclp''; auto)

lemma type_less_x_Set_intro [intro]:
  "τ = Set ρ  ρ < σ  τ < Set σ"
  unfolding less_type_def
  by simp (rule preserve_tranclp; auto)

lemma type_less_x_OrderedSet_intro [intro]:
  "τ = OrderedSet ρ  ρ < σ  τ < OrderedSet σ"
  unfolding less_type_def
  by simp (rule preserve_tranclp; auto)

lemma type_less_x_Bag_intro [intro]:
  "τ = Bag ρ  ρ < σ  τ < Bag σ"
  unfolding less_type_def
  by simp (rule preserve_tranclp; auto)

lemma type_less_x_Sequence_intro [intro]:
  "τ = Sequence ρ  ρ < σ  τ < Sequence σ"
  unfolding less_type_def
  by simp (rule preserve_tranclp; auto)

lemma fun_or_eq_refl [intro]:
  "reflp (λx y. f x y  x = y)"
  by (simp add: reflpI)

lemma type_less_x_Tuple_intro [intro]:
  assumes "τ = Tuple π"
      and "strict_subtuple (≤) π ξ"
    shows "τ < Tuple ξ"
proof -
  have "subtuple (λτ σ. τ  σ  τ = σ)** π ξ"
    using assms(2) less_eq_type_def by auto
  hence "(subtuple (λτ σ. τ  σ  τ = σ))++ π ξ"
    by simp (rule subtuple_to_trancl; auto)
  hence "(strict_subtuple (λτ σ. τ  σ  τ = σ))** π ξ"
    by (simp add: tranclp_into_rtranclp)
  hence "(strict_subtuple (λτ σ. τ  σ  τ = σ))++ π ξ"
    by (meson assms(2) rtranclpD)
  thus ?thesis
    unfolding less_type_def
    using assms(1) apply simp
    by (rule preserve_tranclp; auto)
qed

lemma type_less_x_OclSuper_intro [intro]:
  "τ  OclSuper  τ < OclSuper"
  unfolding less_type_def
proof (induct τ)
  case OclSuper thus ?case by auto
next
  case (Required τ)
  have "subtype** τ[1] OclAny[1]"
    apply (rule_tac ?f="Required" in preserve_rtranclp[of basic_subtype], auto)
    by (metis less_eq_basic_type_def type_less_eq_x_OclAny_intro)
  also have "subtype++ OclAny[1] OclAny[?]" by auto
  also have "subtype++ OclAny[?] OclSuper" by auto
  finally show ?case by auto
next
  case (Optional τ)
  have "subtype** τ[?] OclAny[?]"
    apply (rule_tac ?f="Optional" in preserve_rtranclp[of basic_subtype], auto)
    by (metis less_eq_basic_type_def type_less_eq_x_OclAny_intro)
  also have "subtype++ OclAny[?] OclSuper" by auto
  finally show ?case by auto
next
  case (Collection τ)
  have "subtype** (Collection τ) (Collection OclSuper)"
    apply (rule_tac ?f="Collection" in preserve_rtranclp[of subtype], auto)
    using Collection.hyps by force
  also have "subtype++ (Collection OclSuper) OclSuper" by auto
  finally show ?case by auto
next
  case (Set τ)
  have "subtype++ (Set τ) (Collection τ)" by auto
  also have "subtype** (Collection τ) (Collection OclSuper)"
    apply (rule_tac ?f="Collection" in preserve_rtranclp[of subtype], auto)
    using Set.hyps by force
  also have "subtype** (Collection OclSuper) OclSuper" by auto
  finally show ?case by auto
next
  case (OrderedSet τ)
  have "subtype++ (OrderedSet τ) (Collection τ)" by auto
  also have "subtype** (Collection τ) (Collection OclSuper)"
    apply (rule_tac ?f="Collection" in preserve_rtranclp[of subtype], auto)
    using OrderedSet.hyps by force
  also have "subtype** (Collection OclSuper) OclSuper" by auto
  finally show ?case by auto
next
  case (Bag τ)
  have "subtype++ (Bag τ) (Collection τ)" by auto
  also have "subtype** (Collection τ) (Collection OclSuper)"
    apply (rule_tac ?f="Collection" in preserve_rtranclp[of subtype], auto)
    using Bag.hyps by force
  also have "subtype** (Collection OclSuper) OclSuper" by auto
  finally show ?case by auto
next
  case (Sequence τ)
  have "subtype++ (Sequence τ) (Collection τ)" by auto
  also have "subtype** (Collection τ) (Collection OclSuper)"
    apply (rule_tac ?f="Collection" in preserve_rtranclp[of subtype], auto)
    using Sequence.hyps by force
  also have "subtype** (Collection OclSuper) OclSuper" by auto
  finally show ?case by auto
next
  case (Tuple x) thus ?case by auto
qed

(*** Strict Elimination Rules ***********************************************)

subsection ‹Strict Elimination Rules›

lemma type_less_x_Required [elim!]:
  assumes "τ < σ[1]"
      and "ρ. τ = ρ[1]  ρ < σ  P"
    shows "P"
proof -
  from assms(1) obtain ρ where "τ = ρ[1]"
    unfolding less_type_def
    by (induct rule: converse_tranclp_induct; auto)
  moreover have "τ σ. τ[1] < σ[1]  τ < σ"
    unfolding less_type_def less_basic_type_def
    by (rule reflect_tranclp; auto)
  ultimately show ?thesis
    using assms by auto
qed
(*
lemma type_less_x_Optional [elim!]:
  assumes "τ < σ[?]"
      and "τ = OclVoid ⟹ P"
      and "⋀ρ. τ = ρ[1] ⟹ ρ ≤ σ ⟹ P"
      and "⋀ρ. τ = ρ[?] ⟹ ρ < σ ⟹ P"
    shows "P"
proof -
  from assms(1) obtain ρ where
    "τ = OclVoid ∨ τ = ρ[1] ∨ τ = ρ[?]"
    unfolding less_type_def
    by (induct rule: converse_tranclp_induct; auto)
  moreover have "⋀τ σ. τ[1] < σ[?] ⟹ τ ≤ σ"
    unfolding less_type_def less_eq_basic_type_def
    apply (drule tranclpD, auto)
    apply (erule subtype.cases, auto)
  moreover have "⋀τ σ. τ[?] < σ[?] ⟹ τ < σ"
    unfolding less_type_def less_basic_type_def
    by (rule reflect_tranclp; auto)
  ultimately show ?thesis
    using assms by auto
qed
*)
lemma type_less_x_Optional [elim!]:
  "τ < σ[?] 
   (ρ. τ = ρ[1]  ρ  σ  P)  
   (ρ. τ = ρ[?]  ρ < σ  P)  P"
  unfolding less_type_def
  apply (induct rule: converse_tranclp_induct)
  apply (metis subtype_x_Optional eq_refl less_basic_type_def tranclp.r_into_trancl)
  apply (erule subtype.cases; auto)
  apply (simp add: converse_rtranclp_into_rtranclp less_eq_basic_type_def)
  by (simp add: less_basic_type_def tranclp_into_tranclp2)

lemma type_less_x_Collection [elim!]:
  "τ < Collection σ 
   (ρ. τ = Collection ρ  ρ < σ  P) 
   (ρ. τ = Set ρ  ρ  σ  P)  
   (ρ. τ = OrderedSet ρ  ρ  σ  P)  
   (ρ. τ = Bag ρ  ρ  σ  P)  
   (ρ. τ = Sequence ρ  ρ  σ  P)  P"
  unfolding less_type_def
  apply (induct rule: converse_tranclp_induct)
  apply (metis (mono_tags) Nitpick.rtranclp_unfold
          subtype_x_Collection less_eq_type_def tranclp.r_into_trancl)
  by (erule subtype.cases;
      auto simp add: converse_rtranclp_into_rtranclp less_eq_type_def
                     tranclp_into_tranclp2 tranclp_into_rtranclp)

lemma type_less_x_Set [elim!]:
  assumes "τ < Set σ"
      and "ρ. τ = Set ρ  ρ < σ  P"
    shows "P"
proof -
  from assms(1) obtain ρ where "τ = Set ρ"
    unfolding less_type_def
    by (induct rule: converse_tranclp_induct; auto)
  moreover have "τ σ. Set τ < Set σ  τ < σ"
    unfolding less_type_def
    by (rule reflect_tranclp; auto)
  ultimately show ?thesis
    using assms by auto
qed

lemma type_less_x_OrderedSet [elim!]:
  assumes "τ < OrderedSet σ"
      and "ρ. τ = OrderedSet ρ  ρ < σ  P"
    shows "P"
proof -
  from assms(1) obtain ρ where "τ = OrderedSet ρ"
    unfolding less_type_def
    by (induct rule: converse_tranclp_induct; auto)
  moreover have "τ σ. OrderedSet τ < OrderedSet σ  τ < σ"
    unfolding less_type_def
    by (rule reflect_tranclp; auto)
  ultimately show ?thesis
    using assms by auto
qed

lemma type_less_x_Bag [elim!]:
  assumes "τ < Bag σ"
      and "ρ. τ = Bag ρ  ρ < σ  P"
    shows "P"
proof -
  from assms(1) obtain ρ where "τ = Bag ρ"
    unfolding less_type_def
    by (induct rule: converse_tranclp_induct; auto)
  moreover have "τ σ. Bag τ < Bag σ  τ < σ"
    unfolding less_type_def
    by (rule reflect_tranclp; auto)
  ultimately show ?thesis
    using assms by auto
qed

lemma type_less_x_Sequence [elim!]:
  assumes "τ < Sequence σ"
      and "ρ. τ = Sequence ρ  ρ < σ  P"
    shows "P"
proof -
  from assms(1) obtain ρ where "τ = Sequence ρ"
    unfolding less_type_def
    by (induct rule: converse_tranclp_induct; auto)
  moreover have "τ σ. Sequence τ < Sequence σ  τ < σ"
    unfolding less_type_def
    by (rule reflect_tranclp; auto)
  ultimately show ?thesis
    using assms by auto
qed

text ‹
  We will be able to remove the acyclicity assumption only after
  we prove that the subtype relation is acyclic.›

lemma type_less_x_Tuple':
  assumes "τ < Tuple ξ"
      and "acyclicP_on (fmran' ξ) subtype"
      and "π. τ = Tuple π  strict_subtuple (≤) π ξ  P"
    shows "P"
proof -
  from assms(1) obtain π where "τ = Tuple π"
    unfolding less_type_def
    by (induct rule: converse_tranclp_induct; auto)
  moreover from assms(2) have
    "π. Tuple π < Tuple ξ  strict_subtuple (≤) π ξ"
    unfolding less_type_def less_eq_type_def
    by (rule_tac ?f="Tuple" in strict_subtuple_rtranclp_intro; auto)
  ultimately show ?thesis
    using assms by auto
qed

lemma type_less_x_OclSuper [elim!]:
  "τ < OclSuper  (τ  OclSuper  P)  P"
  unfolding less_type_def
  by (drule tranclpD, auto)

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

subsection ‹Properties›

lemma subtype_irrefl:
  "τ < τ  False"
  for τ :: "'a type"
  apply (induct τ, auto)
  apply (erule type_less_x_Tuple', auto)
  unfolding less_type_def tranclp_unfold
  by auto

lemma subtype_acyclic:
  "acyclicP subtype"
  apply (rule acyclicI)
  apply (simp add: trancl_def)
  by (metis (mono_tags) OCL_Types.less_type_def OCL_Types.subtype_irrefl)

lemma less_le_not_le_type:
  "τ < σ  τ  σ  ¬ σ  τ"
  for τ σ :: "'a type"
proof
  show "τ < σ  τ  σ  ¬ σ  τ"
    apply (auto simp add: less_type_def less_eq_type_def)
    by (metis (mono_tags) subtype_irrefl less_type_def tranclp_rtranclp_tranclp)
  show "τ  σ  ¬ σ  τ  τ < σ"
    apply (auto simp add: less_type_def less_eq_type_def)
    by (metis rtranclpD)
qed

lemma order_refl_type [iff]:
  "τ  τ"
  for τ :: "'a type"
  unfolding less_eq_type_def by simp

lemma order_trans_type:
  "τ  σ  σ  ρ  τ  ρ"
  for τ σ ρ :: "'a type"
  unfolding less_eq_type_def by simp

lemma antisym_type:
  "τ  σ  σ  τ  τ = σ"
  for τ σ :: "'a type"
  unfolding less_eq_type_def less_type_def
  by (metis (mono_tags, lifting) less_eq_type_def
      less_le_not_le_type less_type_def rtranclpD)

instance
  apply intro_classes
  apply (simp add: less_le_not_le_type)
  apply (simp)
  using order_trans_type apply blast
  by (simp add: antisym_type)

end

(*** Non-Strict Introduction Rules ******************************************)

subsection ‹Non-Strict Introduction Rules›

lemma type_less_eq_x_Required_intro [intro]:
  "τ = ρ[1]  ρ  σ  τ  σ[1]"
  unfolding dual_order.order_iff_strict by auto

lemma type_less_eq_x_Optional_intro [intro]:
  "τ = ρ[1]  ρ  σ  τ  σ[?]"
  "τ = ρ[?]  ρ  σ  τ  σ[?]"
  unfolding dual_order.order_iff_strict by auto

lemma type_less_eq_x_Collection_intro [intro]:
  "τ = Collection ρ  ρ  σ  τ  Collection σ"
  "τ = Set ρ  ρ  σ  τ  Collection σ"
  "τ = OrderedSet ρ  ρ  σ  τ  Collection σ"
  "τ = Bag ρ  ρ  σ  τ  Collection σ"
  "τ = Sequence ρ  ρ  σ  τ  Collection σ"
  unfolding dual_order.order_iff_strict by auto

lemma type_less_eq_x_Set_intro [intro]:
  "τ = Set ρ  ρ  σ  τ  Set σ"
  unfolding dual_order.order_iff_strict by auto

lemma type_less_eq_x_OrderedSet_intro [intro]:
  "τ = OrderedSet ρ  ρ  σ  τ  OrderedSet σ"
  unfolding dual_order.order_iff_strict by auto

lemma type_less_eq_x_Bag_intro [intro]:
  "τ = Bag ρ  ρ  σ  τ  Bag σ"
  unfolding dual_order.order_iff_strict by auto

lemma type_less_eq_x_Sequence_intro [intro]:
  "τ = Sequence ρ  ρ  σ  τ  Sequence σ"
  unfolding dual_order.order_iff_strict by auto

lemma type_less_eq_x_Tuple_intro [intro]:
  "τ = Tuple π  subtuple (≤) π ξ  τ  Tuple ξ"
  using dual_order.strict_iff_order by blast

lemma type_less_eq_x_OclSuper_intro [intro]:
  "τ  OclSuper"
  unfolding dual_order.order_iff_strict by auto

(*** Non-Strict Elimination Rules *******************************************)

subsection ‹Non-Strict Elimination Rules›

lemma type_less_eq_x_Required [elim!]:
  "τ  σ[1] 
   (ρ. τ = ρ[1]  ρ  σ  P)  P"
  by (drule le_imp_less_or_eq; auto)

lemma type_less_eq_x_Optional [elim!]:
  "τ  σ[?] 
   (ρ. τ = ρ[1]  ρ  σ  P)  
   (ρ. τ = ρ[?]  ρ  σ  P)  P"
  by (drule le_imp_less_or_eq, auto)

lemma type_less_eq_x_Collection [elim!]:
  "τ  Collection σ 
   (ρ. τ = Set ρ  ρ  σ  P)  
   (ρ. τ = OrderedSet ρ  ρ  σ  P)  
   (ρ. τ = Bag ρ  ρ  σ  P)  
   (ρ. τ = Sequence ρ  ρ  σ  P)  
   (ρ. τ = Collection ρ  ρ  σ  P)  P"
  by (drule le_imp_less_or_eq; auto)

lemma type_less_eq_x_Set [elim!]:
   "τ  Set σ 
    (ρ. τ = Set ρ  ρ  σ  P)  P"
  by (drule le_imp_less_or_eq; auto)

lemma type_less_eq_x_OrderedSet [elim!]:
   "τ  OrderedSet σ 
    (ρ. τ = OrderedSet ρ  ρ  σ  P)  P"
  by (drule le_imp_less_or_eq; auto)

lemma type_less_eq_x_Bag [elim!]:
   "τ  Bag σ 
    (ρ. τ = Bag ρ  ρ  σ  P)  P"
  by (drule le_imp_less_or_eq; auto)

lemma type_less_eq_x_Sequence [elim!]:
   "τ  Sequence σ 
    (ρ. τ = Sequence ρ  ρ  σ  P)  P"
  by (drule le_imp_less_or_eq; auto)

lemma type_less_x_Tuple [elim!]:
  "τ < Tuple ξ 
   (π. τ = Tuple π  strict_subtuple (≤) π ξ  P)  P"
  apply (erule type_less_x_Tuple')
  by (meson acyclic_def subtype_acyclic)

lemma type_less_eq_x_Tuple [elim!]:
  "τ  Tuple ξ 
   (π. τ = Tuple π  subtuple (≤) π ξ  P)  P"
  apply (drule le_imp_less_or_eq, auto)
  by (simp add: fmap.rel_refl fmrel_to_subtuple)

(*** Simplification Rules ***************************************************)

subsection ‹Simplification Rules›

lemma type_less_left_simps [simp]:
  "OclSuper < σ = False"
  "ρ[1] < σ = (υ.
      σ = OclSuper 
      σ = υ[1]  ρ < υ 
      σ = υ[?]  ρ  υ)"
  "ρ[?] < σ = (υ.
      σ = OclSuper 
      σ = υ[?]  ρ < υ)"
  "Collection τ < σ = (φ.
      σ = OclSuper 
      σ = Collection φ  τ < φ)"
  "Set τ < σ = (φ.
      σ = OclSuper 
      σ = Collection φ  τ  φ 
      σ = Set φ  τ < φ)"
  "OrderedSet τ < σ = (φ.
      σ = OclSuper 
      σ = Collection φ  τ  φ 
      σ = OrderedSet φ  τ < φ)"
  "Bag τ < σ = (φ.
      σ = OclSuper 
      σ = Collection φ  τ  φ 
      σ = Bag φ  τ < φ)"
  "Sequence τ < σ = (φ.
      σ = OclSuper 
      σ = Collection φ  τ  φ 
      σ = Sequence φ  τ < φ)"
  "Tuple π < σ = (ξ.
      σ = OclSuper 
      σ = Tuple ξ  strict_subtuple (≤) π ξ)"
  by (induct σ; auto)+

lemma type_less_right_simps [simp]:
  "τ < OclSuper = (τ  OclSuper)"
  "τ < υ[1] = (ρ. τ = ρ[1]  ρ < υ)"
  "τ < υ[?] = (ρ. τ = ρ[1]  ρ  υ  τ = ρ[?]  ρ < υ)"
  "τ < Collection σ = (φ.
      τ = Collection φ  φ < σ 
      τ = Set φ  φ  σ 
      τ = OrderedSet φ  φ  σ 
      τ = Bag φ  φ  σ 
      τ = Sequence φ  φ  σ)"
  "τ < Set σ = (φ. τ = Set φ  φ < σ)"
  "τ < OrderedSet σ = (φ. τ = OrderedSet φ  φ < σ)"
  "τ < Bag σ = (φ. τ = Bag φ  φ < σ)"
  "τ < Sequence σ = (φ. τ = Sequence φ  φ < σ)"
  "τ < Tuple ξ = (π. τ = Tuple π  strict_subtuple (≤) π ξ)"
  by auto

(*** Upper Semilattice of Types *********************************************)

section ‹Upper Semilattice of Types›

instantiation type :: (semilattice_sup) semilattice_sup
begin

fun sup_type where
  "OclSuper  σ = OclSuper"
| "Required τ  σ = (case σ
    of ρ[1]  (τ  ρ)[1]
     | ρ[?]  (τ  ρ)[?]
     | _  OclSuper)"
| "Optional τ  σ = (case σ
    of ρ[1]  (τ  ρ)[?]
     | ρ[?]  (τ  ρ)[?]
     | _  OclSuper)"
| "Collection τ  σ = (case σ
    of Collection ρ  Collection (τ  ρ)
     | Set ρ  Collection (τ  ρ)
     | OrderedSet ρ  Collection (τ  ρ)
     | Bag ρ  Collection (τ  ρ)
     | Sequence ρ  Collection (τ  ρ)
     | _  OclSuper)"
| "Set τ  σ = (case σ
    of Collection ρ  Collection (τ  ρ)
     | Set ρ  Set (τ  ρ)
     | OrderedSet ρ  Collection (τ  ρ)
     | Bag ρ  Collection (τ  ρ)
     | Sequence ρ  Collection (τ  ρ)
     | _  OclSuper)"
| "OrderedSet τ  σ = (case σ
    of Collection ρ  Collection (τ  ρ)
     | Set ρ  Collection (τ  ρ)
     | OrderedSet ρ  OrderedSet (τ  ρ)
     | Bag ρ  Collection (τ  ρ)
     | Sequence ρ  Collection (τ  ρ)
     | _  OclSuper)"
| "Bag τ  σ = (case σ
    of Collection ρ  Collection (τ  ρ)
     | Set ρ  Collection (τ  ρ)
     | OrderedSet ρ  Collection (τ  ρ)
     | Bag ρ  Bag (τ  ρ)
     | Sequence ρ  Collection (τ  ρ)
     | _  OclSuper)"
| "Sequence τ  σ = (case σ
    of Collection ρ  Collection (τ  ρ)
     | Set ρ  Collection (τ  ρ)
     | OrderedSet ρ  Collection (τ  ρ)
     | Bag ρ  Collection (τ  ρ)
     | Sequence ρ  Sequence (τ  ρ)
     | _  OclSuper)"
| "Tuple π  σ = (case σ
    of Tuple ξ  Tuple (fmmerge_fun (⊔) π ξ)
     | _  OclSuper)"

lemma sup_ge1_type:
  "τ  τ  σ"
  for τ σ :: "'a type"
proof (induct τ arbitrary: σ)
  case OclSuper show ?case by simp
  case (Required τ) show ?case by (induct σ; auto)
  case (Optional τ) show ?case by (induct σ; auto)
  case (Collection τ) thus ?case by (induct σ; auto)
  case (Set τ) thus ?case by (induct σ; auto)
  case (OrderedSet τ) thus ?case by (induct σ; auto)
  case (Bag τ) thus ?case by (induct σ; auto)
  case (Sequence τ) thus ?case by (induct σ; auto)
next
  case (Tuple π)
  moreover have Tuple_less_eq_sup:
    "(τ σ. τ  fmran' π  τ  τ  σ) 
     Tuple π  Tuple π  σ"
    by (cases σ, auto)
  ultimately show ?case by (cases σ, auto)
qed

lemma sup_commut_type:
  "τ  σ = σ  τ"
  for τ σ :: "'a type"
proof (induct τ arbitrary: σ)
  case OclSuper show ?case by (cases σ; simp add: less_eq_type_def)
  case (Required τ) show ?case by (cases σ; simp add: sup_commute)
  case (Optional τ) show ?case by (cases σ; simp add: sup_commute)
  case (Collection τ) thus ?case by (cases σ; simp)
  case (Set τ) thus ?case by (cases σ; simp)
  case (OrderedSet τ) thus ?case by (cases σ; simp)
  case (Bag τ) thus ?case by (cases σ; simp)
  case (Sequence τ) thus ?case by (cases σ; simp)
next
  case (Tuple π) thus ?case
    apply (cases σ; simp add: less_eq_type_def)
    using fmmerge_commut by blast
qed

lemma sup_least_type:
  "τ  ρ  σ  ρ  τ  σ  ρ"
  for τ σ ρ :: "'a type"
proof (induct ρ arbitrary: τ σ)
  case OclSuper show ?case using eq_refl by auto
next
  case (Required x) show ?case
    apply (insert Required)
    by (erule type_less_eq_x_Required; erule type_less_eq_x_Required; auto)
next
  case (Optional x) show ?case
    apply (insert Optional)
    by (erule type_less_eq_x_Optional; erule type_less_eq_x_Optional; auto)
next
  case (Collection ρ) show ?case
    apply (insert Collection)
    by (erule type_less_eq_x_Collection; erule type_less_eq_x_Collection; auto)
next
  case (Set ρ) show ?case
    apply (insert Set)
    by (erule type_less_eq_x_Set; erule type_less_eq_x_Set; auto)
next
  case (OrderedSet ρ) show ?case
    apply (insert OrderedSet)
    by (erule type_less_eq_x_OrderedSet; erule type_less_eq_x_OrderedSet; auto)
next
  case (Bag ρ) show ?case
    apply (insert Bag)
    by (erule type_less_eq_x_Bag; erule type_less_eq_x_Bag; auto)
next
  case (Sequence ρ) thus ?case
    apply (insert Sequence)
    by (erule type_less_eq_x_Sequence; erule type_less_eq_x_Sequence; auto)
next
  case (Tuple π) show ?case
    apply (insert Tuple)
    apply (erule type_less_eq_x_Tuple; erule type_less_eq_x_Tuple; auto)
    by (rule_tac ="(fmmerge (⊔) π' π'')" in type_less_eq_x_Tuple_intro;
        simp add: fmrel_on_fset_fmmerge1)
qed

instance
  apply intro_classes
  apply (simp add: sup_ge1_type)
  apply (simp add: sup_commut_type sup_ge1_type)
  by (simp add: sup_least_type)

end

(*** Helper Relations *******************************************************)

section ‹Helper Relations›

abbreviation between ("_/ = __"  [51, 51, 51] 50) where
  "x = yz  y  x  x  z"

inductive element_type where
  "element_type (Collection τ) τ"
| "element_type (Set τ) τ"
| "element_type (OrderedSet τ) τ"
| "element_type (Bag τ) τ"
| "element_type (Sequence τ) τ"

lemma element_type_alt_simps:
  "element_type τ σ = 
     (Collection σ = τ 
      Set σ = τ 
      OrderedSet σ = τ 
      Bag σ = τ 
      Sequence σ = τ)"
  by (auto simp add: element_type.simps)

inductive update_element_type where
  "update_element_type (Collection _) τ (Collection τ)"
| "update_element_type (Set _) τ (Set τ)"
| "update_element_type (OrderedSet _) τ (OrderedSet τ)"
| "update_element_type (Bag _) τ (Bag τ)"
| "update_element_type (Sequence _) τ (Sequence τ)"

inductive to_unique_collection where
  "to_unique_collection (Collection τ) (Set τ)"
| "to_unique_collection (Set τ) (Set τ)"
| "to_unique_collection (OrderedSet τ) (OrderedSet τ)"
| "to_unique_collection (Bag τ) (Set τ)"
| "to_unique_collection (Sequence τ) (OrderedSet τ)"

inductive to_nonunique_collection where
  "to_nonunique_collection (Collection τ) (Bag τ)"
| "to_nonunique_collection (Set τ) (Bag τ)"
| "to_nonunique_collection (OrderedSet τ) (Sequence τ)"
| "to_nonunique_collection (Bag τ) (Bag τ)"
| "to_nonunique_collection (Sequence τ) (Sequence τ)"

inductive to_ordered_collection where
  "to_ordered_collection (Collection τ) (Sequence τ)"
| "to_ordered_collection (Set τ) (OrderedSet τ)"
| "to_ordered_collection (OrderedSet τ) (OrderedSet τ)"
| "to_ordered_collection (Bag τ) (Sequence τ)"
| "to_ordered_collection (Sequence τ) (Sequence τ)"

fun to_single_type where
  "to_single_type OclSuper = OclSuper"
| "to_single_type τ[1] = τ[1]"
| "to_single_type τ[?] = τ[?]"
| "to_single_type (Collection τ) = to_single_type τ"
| "to_single_type (Set τ) = to_single_type τ"
| "to_single_type (OrderedSet τ) = to_single_type τ"
| "to_single_type (Bag τ) = to_single_type τ"
| "to_single_type (Sequence τ) = to_single_type τ"
| "to_single_type (Tuple π) = Tuple π"

fun to_required_type where
  "to_required_type τ[1] = τ[1]"
| "to_required_type τ[?] = τ[1]"
| "to_required_type τ = τ"

fun to_optional_type_nested where
  "to_optional_type_nested OclSuper = OclSuper"
| "to_optional_type_nested τ[1] = τ[?]"
| "to_optional_type_nested τ[?] = τ[?]"
| "to_optional_type_nested (Collection τ) = Collection (to_optional_type_nested τ)"
| "to_optional_type_nested (Set τ) = Set (to_optional_type_nested τ)"
| "to_optional_type_nested (OrderedSet τ) = OrderedSet (to_optional_type_nested τ)"
| "to_optional_type_nested (Bag τ) = Bag (to_optional_type_nested τ)"
| "to_optional_type_nested (Sequence τ) = Sequence (to_optional_type_nested τ)"
| "to_optional_type_nested (Tuple π) = Tuple (fmmap to_optional_type_nested π)"

(*** Determinism ************************************************************)

section ‹Determinism›

lemma element_type_det:
  "element_type τ σ1 
   element_type τ σ2  σ1 = σ2"
  by (induct rule: element_type.induct; simp add: element_type.simps)

lemma update_element_type_det:
  "update_element_type τ σ ρ1 
   update_element_type τ σ ρ2  ρ1 = ρ2"
  by (induct rule: update_element_type.induct; simp add: update_element_type.simps)

lemma to_unique_collection_det:
  "to_unique_collection τ σ1 
   to_unique_collection τ σ2  σ1 = σ2"
  by (induct rule: to_unique_collection.induct; simp add: to_unique_collection.simps)

lemma to_nonunique_collection_det:
  "to_nonunique_collection τ σ1 
   to_nonunique_collection τ σ2  σ1 = σ2"
  by (induct rule: to_nonunique_collection.induct; simp add: to_nonunique_collection.simps)

lemma to_ordered_collection_det:
  "to_ordered_collection τ σ1 
   to_ordered_collection τ σ2  σ1 = σ2"
  by (induct rule: to_ordered_collection.induct; simp add: to_ordered_collection.simps)

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

section ‹Code Setup›

code_pred subtype .

function subtype_fun :: "'a::order type  'a type  bool" where
  "subtype_fun OclSuper _ = False"
| "subtype_fun (Required τ) σ = (case σ
    of OclSuper  True
     | ρ[1]  basic_subtype_fun τ ρ
     | ρ[?]  basic_subtype_fun τ ρ  τ = ρ
     | _  False)"
| "subtype_fun (Optional τ) σ = (case σ
    of OclSuper  True
     | ρ[?]  basic_subtype_fun τ ρ
     | _  False)"
| "subtype_fun (Collection τ) σ = (case σ
    of OclSuper  True
     | Collection ρ  subtype_fun τ ρ
     | _  False)"
| "subtype_fun (Set τ) σ = (case σ
    of OclSuper  True
     | Collection ρ  subtype_fun τ ρ  τ = ρ
     | Set ρ  subtype_fun τ ρ
     | _  False)"
| "subtype_fun (OrderedSet τ) σ = (case σ
    of OclSuper  True
     | Collection ρ  subtype_fun τ ρ  τ = ρ
     | OrderedSet ρ  subtype_fun τ ρ
     | _  False)"
| "subtype_fun (Bag τ) σ = (case σ
    of OclSuper  True
     | Collection ρ  subtype_fun τ ρ  τ = ρ
     | Bag ρ  subtype_fun τ ρ
     | _  False)"
| "subtype_fun (Sequence τ) σ = (case σ
    of OclSuper  True
     | Collection ρ  subtype_fun τ ρ  τ = ρ
     | Sequence ρ  subtype_fun τ ρ
     | _  False)"
| "subtype_fun (Tuple π) σ = (case σ
    of OclSuper  True
     | Tuple ξ  strict_subtuple_fun (λτ σ. subtype_fun τ σ  τ = σ) π ξ
     | _  False)"
  by pat_completeness auto
termination
  by (relation "measure (λ(xs, ys). size ys)";
      auto simp add: elem_le_ffold' fmran'I)

lemma less_type_code [code]:
  "(<) = subtype_fun"
proof (intro ext iffI)
  fix τ σ :: "'a type"
  show "τ < σ  subtype_fun τ σ"
  proof (induct τ arbitrary: σ)
    case OclSuper thus ?case by (cases σ; auto)
  next
    case (Required τ) thus ?case
      by (cases σ; auto simp: less_basic_type_code less_eq_basic_type_code)
  next
    case (Optional τ) thus ?case
      by (cases σ; auto simp: less_basic_type_code less_eq_basic_type_code)
  next
    case (Collection τ) thus ?case by (cases σ; auto)
  next
    case (Set τ) thus ?case by (cases σ; auto)
  next
    case (OrderedSet τ) thus ?case by (cases σ; auto)
  next
    case (Bag τ) thus ?case by (cases σ; auto)
  next
    case (Sequence τ) thus ?case by (cases σ; auto)
  next
    case (Tuple π)
    have
      "ξ. subtuple (≤) π ξ 
       subtuple (λτ σ. subtype_fun τ σ  τ = σ) π ξ"
      by (rule subtuple_mono; auto simp add: Tuple.hyps)
    with Tuple.prems show ?case by (cases σ; auto)
  qed
  show "subtype_fun τ σ  τ < σ"
  proof (induct σ arbitrary: τ)
    case OclSuper thus ?case by (cases σ; auto)
  next
    case (Required σ) show ?case
      by (insert Required) (erule subtype_fun.elims;
          auto simp: less_basic_type_code less_eq_basic_type_code)
  next
    case (Optional σ) show ?case
      by (insert Optional) (erule subtype_fun.elims;
          auto simp: less_basic_type_code less_eq_basic_type_code)
  next
    case (Collection σ) show ?case
      apply (insert Collection)
      apply (erule subtype_fun.elims; auto)
      using order.strict_implies_order by auto
  next
    case (Set σ) show ?case
      by (insert Set) (erule subtype_fun.elims; auto)
  next
    case (OrderedSet σ) show ?case
      by (insert OrderedSet) (erule subtype_fun.elims; auto)
  next
    case (Bag σ) show ?case
      by (insert Bag) (erule subtype_fun.elims; auto)
  next
    case (Sequence σ) show ?case
      by (insert Sequence) (erule subtype_fun.elims; auto)
  next
    case (Tuple ξ)
    have subtuple_imp_simp:
      "π. subtuple (λτ σ. subtype_fun τ σ  τ = σ) π ξ 
       subtuple (≤) π ξ"
      by (rule subtuple_mono; auto simp add: Tuple.hyps less_imp_le)
    show ?case
      apply (insert Tuple)
      by (erule subtype_fun.elims; auto simp add: subtuple_imp_simp)
  qed
qed

lemma less_eq_type_code [code]:
  "(≤) = (λx y. subtype_fun x y  x = y)"
  unfolding dual_order.order_iff_strict less_type_code
  by auto

code_pred element_type .
code_pred update_element_type .
code_pred to_unique_collection .
code_pred to_nonunique_collection .
code_pred to_ordered_collection .

end

Theory OCL_Syntax

(*  Title:       Safe OCL
    Author:      Denis Nikiforov, March 2019
    Maintainer:  Denis Nikiforov <denis.nikif at gmail.com>
    License:     LGPL
*)
chapter ‹Abstract Syntax›
theory OCL_Syntax
  imports Complex_Main Object_Model OCL_Types
begin

section ‹Preliminaries›

type_synonym vname = "String.literal"
type_synonym 'a env = "vname f 'a"

text ‹
  In OCL @{text "1 + ∞ = ⊥"}. So we do not use @{typ enat} and
  define the new data type.›

typedef unat = "UNIV :: nat option set" ..

definition "unat x  Abs_unat (Some x)"

instantiation unat :: infinity
begin
definition "  Abs_unat None"
instance ..
end

free_constructors cases_unat for
  unat
| " :: unat"
  unfolding unat_def infinity_unat_def
  apply (metis Rep_unat_inverse option.collapse)
  apply (metis Abs_unat_inverse UNIV_I option.sel)
  by (simp add: Abs_unat_inject)

section ‹Standard Library Operations›

datatype metaop = AllInstancesOp

datatype typeop = OclAsTypeOp | OclIsTypeOfOp | OclIsKindOfOp
| SelectByKindOp | SelectByTypeOp

datatype super_binop = EqualOp | NotEqualOp

datatype any_unop = OclAsSetOp | OclIsNewOp
| OclIsUndefinedOp | OclIsInvalidOp | OclLocaleOp | ToStringOp

datatype boolean_unop = NotOp
datatype boolean_binop = AndOp | OrOp | XorOp | ImpliesOp

datatype numeric_unop = UMinusOp | AbsOp | FloorOp | RoundOp | ToIntegerOp
datatype numeric_binop = PlusOp | MinusOp | MultOp | DivideOp
| DivOp | ModOp | MaxOp | MinOp
| LessOp | LessEqOp | GreaterOp | GreaterEqOp

datatype string_unop = SizeOp | ToUpperCaseOp | ToLowerCaseOp | CharactersOp
| ToBooleanOp | ToIntegerOp | ToRealOp
datatype string_binop = ConcatOp | IndexOfOp | EqualsIgnoreCaseOp | AtOp
| LessOp | LessEqOp | GreaterOp | GreaterEqOp
datatype string_ternop = SubstringOp

datatype collection_unop = CollectionSizeOp | IsEmptyOp | NotEmptyOp
| CollectionMaxOp | CollectionMinOp | SumOp
| AsSetOp | AsOrderedSetOp | AsSequenceOp | AsBagOp | FlattenOp
| FirstOp | LastOp | ReverseOp
datatype collection_binop = IncludesOp | ExcludesOp
| CountOp| IncludesAllOp | ExcludesAllOp | ProductOp
| UnionOp | IntersectionOp | SetMinusOp | SymmetricDifferenceOp
| IncludingOp | ExcludingOp
| AppendOp | PrependOp | CollectionAtOp | CollectionIndexOfOp
datatype collection_ternop = InsertAtOp | SubOrderedSetOp | SubSequenceOp

type_synonym unop = "any_unop + boolean_unop + numeric_unop + string_unop + collection_unop"

declare [[coercion "Inl :: any_unop  unop"]]
declare [[coercion "Inr  Inl :: boolean_unop  unop"]]
declare [[coercion "Inr  Inr  Inl :: numeric_unop  unop"]]
declare [[coercion "Inr  Inr  Inr  Inl :: string_unop  unop"]]
declare [[coercion "Inr  Inr  Inr  Inr :: collection_unop  unop"]]

type_synonym binop = "super_binop + boolean_binop + numeric_binop + string_binop + collection_binop"

declare [[coercion "Inl :: super_binop  binop"]]
declare [[coercion "Inr  Inl :: boolean_binop  binop"]]
declare [[coercion "Inr  Inr  Inl :: numeric_binop  binop"]]
declare [[coercion "Inr  Inr  Inr  Inl :: string_binop  binop"]]
declare [[coercion "Inr  Inr  Inr  Inr :: collection_binop  binop"]]

type_synonym ternop = "string_ternop + collection_ternop"

declare [[coercion "Inl :: string_ternop  ternop"]]
declare [[coercion "Inr :: collection_ternop  ternop"]]

type_synonym op = "unop + binop + ternop + oper"

declare [[coercion "Inl  Inl :: any_unop  op"]]
declare [[coercion "Inl  Inr  Inl :: boolean_unop  op"]]
declare [[coercion "Inl  Inr  Inr  Inl :: numeric_unop  op"]]
declare [[coercion "Inl  Inr  Inr  Inr  Inl :: string_unop  op"]]
declare [[coercion "Inl  Inr  Inr  Inr  Inr :: collection_unop  op"]]

declare [[coercion "Inr  Inl  Inl :: super_binop  op"]]
declare [[coercion "Inr  Inl  Inr  Inl :: boolean_binop  op"]]
declare [[coercion "Inr  Inl  Inr  Inr  Inl :: numeric_binop  op"]]
declare [[coercion "Inr  Inl  Inr  Inr  Inr  Inl :: string_binop  op"]]
declare [[coercion "Inr  Inl  Inr  Inr  Inr  Inr :: collection_binop  op"]]

declare [[coercion "Inr  Inr  Inl  Inl :: string_ternop  op"]]
declare [[coercion "Inr  Inr  Inl  Inr :: collection_ternop  op"]]

declare [[coercion "Inr  Inr  Inr :: oper  op"]]

datatype iterator = AnyIter | ClosureIter | CollectIter | CollectNestedIter
| ExistsIter | ForAllIter | OneIter | IsUniqueIter
| SelectIter | RejectIter | SortedByIter

section ‹Expressions›

datatype collection_literal_kind =
  CollectionKind | SetKind | OrderedSetKind | BagKind | SequenceKind

text ‹
  A call kind could be defined as two boolean values (@{text "is_arrow_call"},
  @{text "is_safe_call"}). Also we could derive @{text "is_arrow_call"}
  value automatically based on an operation kind.
  However, it is much easier and more natural to use the following enumeration.›

datatype call_kind = DotCall | ArrowCall | SafeDotCall | SafeArrowCall

text ‹
  We do not define a @{text Classifier} type (a type of all types),
  because it will add unnecessary complications to the theory.
  So we have to define type operations as a pure syntactic constructs.
  We do not define @{text Type} expressions either.

  We do not define @{text InvalidLiteral}, because it allows us to
  exclude @{text OclInvalid} type from typing rules. It simplifies
  the types system.

  Please take a note that for @{text AssociationEnd} and
  @{text AssociationClass} call expressions one can specify an
  optional role of a source class (@{text from_role}).
  It differs from the OCL specification, which allows one to specify
  a role of a destination class. However, the latter one does not
  allow one to determine uniquely a set of linked objects, for example,
  in a ternary self relation.›

datatype 'a expr =
  Literal "'a literal_expr"
| Let (var : vname) (var_type : "'a type option") (init_expr : "'a expr")
    (body_expr : "'a expr")
| Var (var : vname)
| If (if_expr : "'a expr") (then_expr : "'a expr") (else_expr : "'a expr")
| MetaOperationCall (type : "'a type") metaop
| StaticOperationCall (type : "'a type") oper (args : "'a expr list")
| Call (source : "'a expr") (kind : call_kind) "'a call_expr"
and 'a literal_expr =
  NullLiteral
| BooleanLiteral (boolean_symbol : bool)
| RealLiteral (real_symbol : real)
| IntegerLiteral (integer_symbol : int)
| UnlimitedNaturalLiteral (unlimited_natural_symbol : unat)
| StringLiteral (string_symbol : string)
| EnumLiteral (enum_type : "'a enum") (enum_literal : elit)
| CollectionLiteral (kind : collection_literal_kind)
    (parts : "'a collection_literal_part_expr list")
| TupleLiteral (tuple_elements : "(telem × 'a type option × 'a expr) list")
and 'a collection_literal_part_expr =
  CollectionItem (item : "'a expr")
| CollectionRange (first : "'a expr") (last : "'a expr")
and 'a call_expr =
  TypeOperation typeop (type : "'a type")
| Attribute attr
| AssociationEnd (from_role : "role option") role
| AssociationClass (from_role : "role option") 'a
| AssociationClassEnd role
| Operation op (args : "'a expr list")
| TupleElement telem
| Iterate (iterators : "vname list") (iterators_type : "'a type option")
    (var : vname) (var_type : "'a type option") (init_expr : "'a expr")
    (body_expr : "'a expr")
| Iterator iterator (iterators : "vname list") (iterators_type : "'a type option")
    (body_expr : "'a expr")

definition "tuple_element_name  fst"
definition "tuple_element_type  fst  snd"
definition "tuple_element_expr  snd  snd"

declare [[coercion "Literal :: 'a literal_expr  'a expr"]]

abbreviation "TypeOperationCall src k op ty 
  Call src k (TypeOperation op ty)"
abbreviation "AttributeCall src k attr 
  Call src k (Attribute attr)"
abbreviation "AssociationEndCall src k from role 
  Call src k (AssociationEnd from role)"
abbreviation "AssociationClassCall src k from cls 
  Call src k (AssociationClass from cls)"
abbreviation "AssociationClassEndCall src k role 
  Call src k (AssociationClassEnd role)"
abbreviation "OperationCall src k op as 
  Call src k (Operation op as)"
abbreviation "TupleElementCall src k elem 
  Call src k (TupleElement elem)"
abbreviation "IterateCall src k its its_ty v ty init body 
  Call src k (Iterate its its_ty v ty init body)"
abbreviation "AnyIteratorCall src k its its_ty body 
  Call src k (Iterator AnyIter its its_ty body)"
abbreviation "ClosureIteratorCall src k its its_ty body 
  Call src k (Iterator ClosureIter its its_ty body)"
abbreviation "CollectIteratorCall src k its its_ty body 
  Call src k (Iterator CollectIter its its_ty body)"
abbreviation "CollectNestedIteratorCall src k its its_ty body 
  Call src k (Iterator CollectNestedIter its its_ty body)"
abbreviation "ExistsIteratorCall src k its its_ty body 
  Call src k (Iterator ExistsIter its its_ty body)"
abbreviation "ForAllIteratorCall src k its its_ty body 
  Call src k (Iterator ForAllIter its its_ty body)"
abbreviation "OneIteratorCall src k its its_ty body 
  Call src k (Iterator OneIter its its_ty body)"
abbreviation "IsUniqueIteratorCall src k its its_ty body 
  Call src k (Iterator IsUniqueIter its its_ty body)"
abbreviation "SelectIteratorCall src k its its_ty body 
  Call src k (Iterator SelectIter its its_ty body)"
abbreviation "RejectIteratorCall src k its its_ty body 
  Call src k (Iterator RejectIter its its_ty body)"
abbreviation "SortedByIteratorCall src k its its_ty body 
  Call src k (Iterator SortedByIter its its_ty body)"

end

Theory OCL_Object_Model

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

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.›

definition
  "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]
    else
      if assoc_end_unique end then
        if assoc_end_ordered end
        then OrderedSet 𝒞𝒯[1]
        else Set 𝒞𝒯[1]
      else
        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"
begin

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

end

end

Theory OCL_Typing

(*  Title:       Safe OCL
    Author:      Denis Nikiforov, March 2019
    Maintainer:  Denis Nikiforov <denis.nikif at gmail.com>
    License:     LGPL
*)
chapter ‹Typing›
theory OCL_Typing
  imports OCL_Object_Model "HOL-Library.Transitive_Closure_Table"
begin

text ‹
  The following rules are more restrictive than rules given in
  the OCL specification. This allows one to identify more errors
  in expressions. However, these restrictions may be revised if necessary.
  Perhaps some of them could be separated and should cause warnings
  instead of errors.›

(*** Operations Typing ******************************************************)

section ‹Operations Typing›

subsection ‹Metaclass Operations›

text ‹
  All basic types in the theory are either nullable or non-nullable.
  For example, instead of @{text Boolean} type we have two types:
  @{text "Boolean[1]"} and @{text "Boolean[?]"}.
  The @{text "allInstances()"} operation is extended accordingly:›

text ‹Boolean[1].allInstances() = Set{true, false}
Boolean[?].allInstances() = Set{true, false, null}›

inductive mataop_type where
  "mataop_type τ AllInstancesOp (Set τ)"

subsection ‹Type Operations›

text ‹
  At first we decided to allow casting only to subtypes.
  However sometimes it is necessary to cast expressions to supertypes,
  for example, to access overridden attributes of a supertype.
  So we allow casting to subtypes and supertypes.
  Casting to other types is meaningless.›

text ‹
  According to the Section 7.4.7 of the OCL specification
  @{text "oclAsType()"} can be applied to collections as well as
  to single values. I guess we can allow @{text "oclIsTypeOf()"}
  and @{text "oclIsKindOf()"} for collections too.›

text ‹
  Please take a note that the following expressions are prohibited,
  because they always return true or false:›

text ‹1.oclIsKindOf(OclAny[?])
1.oclIsKindOf(String[1])›

text ‹
  Please take a note that:›

text ‹Set{1,2,null,'abc'}->selectByKind(Integer[1]) = Set{1,2}
Set{1,2,null,'abc'}->selectByKind(Integer[?]) = Set{1,2,null}›

text ‹
  The following expressions are prohibited, because they always
  returns either the same or empty collections:›

text ‹Set{1,2,null,'abc'}->selectByKind(OclAny[?])
Set{1,2,null,'abc'}->selectByKind(Collection(Boolean[1]))›

inductive typeop_type where
  "σ < τ  τ < σ 
   typeop_type DotCall OclAsTypeOp τ σ σ"

| "σ < τ 
   typeop_type DotCall OclIsTypeOfOp τ σ Boolean[1]"
| "σ < τ 
   typeop_type DotCall OclIsKindOfOp τ σ Boolean[1]"

| "element_type τ ρ  σ < ρ 
   update_element_type τ σ υ 
   typeop_type ArrowCall SelectByKindOp τ σ υ"

| "element_type τ ρ  σ < ρ 
   update_element_type τ σ υ 
   typeop_type ArrowCall SelectByTypeOp τ σ υ"

subsection ‹OclSuper Operations›

text ‹
  It makes sense to compare values only with compatible types.›

(* We have to specify the predicate type explicitly to let
   a generated code work *)
inductive super_binop_type
    :: "super_binop  ('a :: order) type  'a type  'a type  bool" where
  "τ  σ  σ < τ 
   super_binop_type EqualOp τ σ Boolean[1]"
| "τ  σ  σ < τ 
   super_binop_type NotEqualOp τ σ Boolean[1]"

subsection ‹OclAny Operations›

text ‹
  The OCL specification defines @{text "toString()"} operation
  only for boolean and numeric types. However, I guess it is a good
  idea to define it once for all basic types. Maybe it should be defined
  for collections as well.›

inductive any_unop_type where
  "τ  OclAny[?] 
   any_unop_type OclAsSetOp τ (Set (to_required_type τ))"
| "τ  OclAny[?] 
   any_unop_type OclIsNewOp τ Boolean[1]"
| "τ  OclAny[?] 
   any_unop_type OclIsUndefinedOp τ Boolean[1]"
| "τ  OclAny[?] 
   any_unop_type OclIsInvalidOp τ Boolean[1]"
| "τ  OclAny[?] 
   any_unop_type OclLocaleOp τ String[1]"
| "τ  OclAny[?] 
   any_unop_type ToStringOp τ String[1]"

subsection ‹Boolean Operations›

text ‹
  Please take a note that:›

text ‹true or false : Boolean[1]
true and null : Boolean[?]
null and null : OclVoid[?]›

inductive boolean_unop_type where
  "τ  Boolean[?] 
   boolean_unop_type NotOp τ τ"

inductive boolean_binop_type where
  "τ  σ = ρ  ρ  Boolean[?] 
   boolean_binop_type AndOp τ σ ρ"
| "τ  σ = ρ  ρ  Boolean[?] 
   boolean_binop_type OrOp τ σ ρ"
| "τ  σ = ρ  ρ  Boolean[?] 
   boolean_binop_type XorOp τ σ ρ"
| "τ  σ = ρ  ρ  Boolean[?] 
   boolean_binop_type ImpliesOp τ σ ρ"

subsection ‹Numeric Operations›

text ‹
  The expression @{text "1 + null"} is not well-typed.
  Nullable numeric values should be converted to non-nullable ones.
  This is a significant difference from the OCL specification.›

text ‹
  Please take a note that many operations automatically casts
  unlimited naturals to integers.›

text ‹
  The difference between @{text "oclAsType(Integer)"} and
  @{text "toInteger()"} for unlimited naturals is unclear.›

inductive numeric_unop_type where
  "τ = Real[1] 
   numeric_unop_type UMinusOp τ Real[1]"
| "τ = UnlimitedNatural[1]Integer[1] 
   numeric_unop_type UMinusOp τ Integer[1]"

| "τ = Real[1] 
   numeric_unop_type AbsOp τ Real[1]"
| "τ = UnlimitedNatural[1]Integer[1] 
   numeric_unop_type AbsOp τ Integer[1]"

| "τ = UnlimitedNatural[1]Real[1] 
   numeric_unop_type FloorOp τ Integer[1]"
| "τ = UnlimitedNatural[1]Real[1] 
   numeric_unop_type RoundOp τ Integer[1]"

| "τ = UnlimitedNatural[1] 
   numeric_unop_type numeric_unop.ToIntegerOp τ Integer[1]"

inductive numeric_binop_type where
  "τ  σ = ρ  ρ = UnlimitedNatural[1]Real[1] 
   numeric_binop_type PlusOp τ σ ρ"

| "τ  σ = Real[1] 
   numeric_binop_type MinusOp τ σ Real[1]"
| "τ  σ = UnlimitedNatural[1]Integer[1] 
   numeric_binop_type MinusOp τ σ Integer[1]"

| "τ  σ = ρ  ρ = UnlimitedNatural[1]Real[1] 
   numeric_binop_type MultOp τ σ ρ"

| "τ = UnlimitedNatural[1]Real[1]  σ = UnlimitedNatural[1]Real[1] 
   numeric_binop_type DivideOp τ σ Real[1]"

| "τ  σ = ρ  ρ = UnlimitedNatural[1]Integer[1] 
   numeric_binop_type DivOp τ σ ρ"
| "τ  σ = ρ  ρ = UnlimitedNatural[1]Integer[1] 
   numeric_binop_type ModOp τ σ ρ"

| "τ  σ = ρ  ρ = UnlimitedNatural[1]Real[1] 
   numeric_binop_type MaxOp τ σ ρ"
| "τ  σ = ρ  ρ = UnlimitedNatural[1]Real[1] 
   numeric_binop_type MinOp τ σ ρ"

| "τ = UnlimitedNatural[1]Real[1]  σ = UnlimitedNatural[1]Real[1] 
   numeric_binop_type numeric_binop.LessOp τ σ Boolean[1]"
| "τ = UnlimitedNatural[1]Real[1]  σ = UnlimitedNatural[1]Real[1] 
   numeric_binop_type numeric_binop.LessEqOp τ σ Boolean[1]"
| "τ = UnlimitedNatural[1]Real[1]  σ = UnlimitedNatural[1]Real[1] 
   numeric_binop_type numeric_binop.GreaterOp τ σ Boolean[1]"
| "τ = UnlimitedNatural[1]Real[1]  σ = UnlimitedNatural[1]Real[1] 
   numeric_binop_type numeric_binop.GreaterEqOp τ σ Boolean[1]"

subsection ‹String Operations›

inductive string_unop_type where
  "string_unop_type SizeOp String[1] Integer[1]"
| "string_unop_type CharactersOp String[1] (Sequence String[1])"
| "string_unop_type ToUpperCaseOp String[1] String[1]"
| "string_unop_type ToLowerCaseOp String[1] String[1]"
| "string_unop_type ToBooleanOp String[1] Boolean[1]"
| "string_unop_type ToIntegerOp String[1] Integer[1]"
| "string_unop_type ToRealOp String[1] Real[1]"

inductive string_binop_type where
  "string_binop_type ConcatOp String[1] String[1] String[1]"
| "string_binop_type EqualsIgnoreCaseOp String[1] String[1] Boolean[1]"
| "string_binop_type LessOp String[1] String[1] Boolean[1]"
| "string_binop_type LessEqOp String[1] String[1] Boolean[1]"
| "string_binop_type GreaterOp String[1] String[1] Boolean[1]"
| "string_binop_type GreaterEqOp String[1] String[1] Boolean[1]"
| "string_binop_type IndexOfOp String[1] String[1] Integer[1]"
| "τ = UnlimitedNatural[1]Integer[1] 
   string_binop_type AtOp String[1] τ String[1]"

inductive string_ternop_type where
  "σ = UnlimitedNatural[1]Integer[1] 
   ρ = UnlimitedNatural[1]Integer[1] 
   string_ternop_type SubstringOp String[1] σ ρ String[1]"

subsection ‹Collection Operations›

text ‹
  Please take a note, that @{text "flatten()"} preserves a collection kind.›

inductive collection_unop_type where
  "element_type τ _ 
   collection_unop_type CollectionSizeOp τ Integer[1]"
| "element_type τ _ 
   collection_unop_type IsEmptyOp τ Boolean[1]"
| "element_type τ _ 
   collection_unop_type NotEmptyOp τ Boolean[1]"

| "element_type τ σ  σ = UnlimitedNatural[1]Real[1] 
   collection_unop_type CollectionMaxOp τ σ"
| "element_type τ σ  operation σ STR ''max'' [σ] oper 
   collection_unop_type CollectionMaxOp τ σ"

| "element_type τ σ  σ = UnlimitedNatural[1]Real[1] 
   collection_unop_type CollectionMinOp τ σ"
| "element_type τ σ  operation σ STR ''min'' [σ] oper 
   collection_unop_type CollectionMinOp τ σ"

| "element_type τ σ  σ = UnlimitedNatural[1]Real[1] 
   collection_unop_type SumOp τ σ"
| "element_type τ σ  operation σ STR ''+'' [σ] oper 
   collection_unop_type SumOp τ σ"

| "element_type τ σ 
   collection_unop_type AsSetOp τ (Set σ)"
| "element_type τ σ 
   collection_unop_type AsOrderedSetOp τ (OrderedSet σ)"
| "element_type τ σ 
   collection_unop_type AsBagOp τ (Bag σ)"
| "element_type τ σ 
   collection_unop_type AsSequenceOp τ (Sequence σ)"

| "update_element_type τ (to_single_type τ) σ 
   collection_unop_type FlattenOp τ σ"

| "collection_unop_type FirstOp (OrderedSet τ) τ"
| "collection_unop_type FirstOp (Sequence τ) τ"
| "collection_unop_type LastOp (OrderedSet τ) τ"
| "collection_unop_type LastOp (Sequence τ) τ"
| "collection_unop_type ReverseOp (OrderedSet τ) (OrderedSet τ)"
| "collection_unop_type ReverseOp (Sequence τ) (Sequence τ)"

text ‹
  Please take a note that if both arguments are collections,
  then an element type of the resulting collection is a super type
  of element types of orginal collections. However for single-valued
  operations (@{text "append()"}, @{text "insertAt()"}, ...)
  this behavior looks undesirable. So we restrict such arguments
  to have a subtype of the collection element type.›

text ‹
  Please take a note that we allow the following expressions:›

text ‹let nullable_value : Integer[?] = null in
Sequence{1..3}->inculdes(nullable_value) and
Sequence{1..3}->inculdes(null) and
Sequence{1..3}->inculdesAll(Set{1,null})›

text ‹
  The OCL specification defines @{text "including()"} and
  @{text "excluding()"} operations for the @{text Sequence} type
  but does not define them for the @{text OrderedSet} type.
  We define them for all collection types.

  It is a good idea to prohibit including of values that
  do not conform to a collection element type.
  However we do not restrict it.

  At first we defined the following typing rules for the
  @{text "excluding()"} operation:

{\isacharbar}\ {\isachardoublequoteopen}element{\isacharunderscore}type\ {\isasymtau}\ {\isasymrho}\ {\isasymLongrightarrow}\ {\isasymsigma}\ {\isasymle}\ {\isasymrho}\ {\isasymLongrightarrow}\ {\isasymsigma}\ {\isasymnoteq}\ OclVoid{\isacharbrackleft}{\isacharquery}{\isacharbrackright}\ {\isasymLongrightarrow}\isanewline
\ \ \ collection{\isacharunderscore}binop{\isacharunderscore}type\ ExcludingOp\ {\isasymtau}\ {\isasymsigma}\ {\isasymtau}{\isachardoublequoteclose}\isanewline
{\isacharbar}\ {\isachardoublequoteopen}element{\isacharunderscore}type\ {\isasymtau}\ {\isasymrho}\ {\isasymLongrightarrow}\ {\isasymsigma}\ {\isasymle}\ {\isasymrho}\ {\isasymLongrightarrow}\ {\isasymsigma}\ {\isacharequal}\ OclVoid{\isacharbrackleft}{\isacharquery}{\isacharbrackright}\ {\isasymLongrightarrow}\isanewline
\ \ \ update{\isacharunderscore}element{\isacharunderscore}type\ {\isasymtau}\ {\isacharparenleft}to{\isacharunderscore}required{\isacharunderscore}type\ {\isasymrho}{\isacharparenright}\ {\isasymupsilon}\ {\isasymLongrightarrow}\isanewline
\ \ \ collection{\isacharunderscore}binop{\isacharunderscore}type\ ExcludingOp\ {\isasymtau}\ {\isasymsigma}\ {\isasymupsilon}{\isachardoublequoteclose}\isanewline

  This operation could play a special role in a definition
  of safe navigation operations:›

text ‹Sequence{1,2,null}->exculding(null) : Integer[1]›

text ‹
  However it is more natural to use a @{text "selectByKind(T[1])"}
  operation instead.›

inductive collection_binop_type where
  "element_type τ ρ  σ  to_optional_type_nested ρ 
   collection_binop_type IncludesOp τ σ Boolean[1]"
| "element_type τ ρ  σ  to_optional_type_nested ρ 
   collection_binop_type ExcludesOp τ σ Boolean[1]"
| "element_type τ ρ  σ  to_optional_type_nested ρ 
   collection_binop_type CountOp τ σ Integer[1]"

| "element_type τ ρ  element_type σ υ  υ  to_optional_type_nested ρ 
   collection_binop_type IncludesAllOp τ σ Boolean[1]"
| "element_type τ ρ  element_type σ υ  υ  to_optional_type_nested ρ 
   collection_binop_type ExcludesAllOp τ σ Boolean[1]"

| "element_type τ ρ  element_type σ υ 
   collection_binop_type ProductOp τ σ
      (Set (Tuple (fmap_of_list [(STR ''first'', ρ), (STR ''second'', υ)])))"

| "collection_binop_type UnionOp (Set τ) (Set σ) (Set (τ  σ))"
| "collection_binop_type UnionOp (Set τ) (Bag σ) (Bag (τ  σ))"
| "collection_binop_type UnionOp (Bag τ) (Set σ) (Bag (τ  σ))"
| "collection_binop_type UnionOp (Bag τ) (Bag σ) (Bag (τ  σ))"

| "collection_binop_type IntersectionOp (Set τ) (Set σ) (Set (τ  σ))"
| "collection_binop_type IntersectionOp (Set τ) (Bag σ) (Set (τ  σ))"
| "collection_binop_type IntersectionOp (Bag τ) (Set σ) (Set (τ  σ))"
| "collection_binop_type IntersectionOp (Bag τ) (Bag σ) (Bag (τ  σ))"

| "collection_binop_type SetMinusOp (Set τ) (Set σ) (Set τ)"
| "collection_binop_type SymmetricDifferenceOp (Set τ) (Set σ) (Set (τ  σ))"

| "element_type τ ρ  update_element_type τ (ρ  σ) υ 
   collection_binop_type IncludingOp τ σ υ"
| "element_type τ ρ  σ  ρ 
   collection_binop_type ExcludingOp τ σ τ"

| "σ  τ 
   collection_binop_type AppendOp (OrderedSet τ) σ (OrderedSet τ)"
| "σ  τ 
   collection_binop_type AppendOp (Sequence τ) σ (Sequence τ)"
| "σ  τ 
   collection_binop_type PrependOp (OrderedSet τ) σ (OrderedSet τ)"
| "σ  τ 
   collection_binop_type PrependOp (Sequence τ) σ (Sequence τ)"

| "σ = UnlimitedNatural[1]Integer[1] 
   collection_binop_type CollectionAtOp (OrderedSet τ) σ τ"
| "σ = UnlimitedNatural[1]Integer[1] 
   collection_binop_type CollectionAtOp (Sequence τ) σ τ"

| "σ  τ 
   collection_binop_type CollectionIndexOfOp (OrderedSet τ) σ Integer[1]"
| "σ  τ 
   collection_binop_type CollectionIndexOfOp (Sequence τ) σ Integer[1]"

inductive collection_ternop_type where
  "σ = UnlimitedNatural[1]Integer[1]  ρ  τ 
   collection_ternop_type InsertAtOp (OrderedSet τ) σ ρ (OrderedSet τ)"
| "σ = UnlimitedNatural[1]Integer[1]  ρ  τ 
   collection_ternop_type InsertAtOp (Sequence τ) σ ρ (Sequence τ)"
| "σ = UnlimitedNatural[1]Integer[1] 
   ρ = UnlimitedNatural[1]Integer[1] 
   collection_ternop_type SubOrderedSetOp (OrderedSet τ) σ ρ (OrderedSet τ)"
| "σ = UnlimitedNatural[1]Integer[1] 
   ρ = UnlimitedNatural[1]Integer[1] 
   collection_ternop_type SubSequenceOp (Sequence τ) σ ρ (Sequence τ)"

subsection ‹Coercions›

inductive unop_type where
  "any_unop_type op τ σ 
   unop_type (Inl op) DotCall τ σ"
| "boolean_unop_type op τ σ 
   unop_type (Inr (Inl op)) DotCall τ σ"
| "numeric_unop_type op τ σ 
   unop_type (Inr (Inr (Inl op))) DotCall τ σ"
| "string_unop_type op τ σ 
   unop_type (Inr (Inr (Inr (Inl op)))) DotCall τ σ"
| "collection_unop_type op τ σ 
   unop_type (Inr (Inr (Inr (Inr op)))) ArrowCall τ σ"

inductive binop_type where
  "super_binop_type op τ σ ρ 
   binop_type (Inl op) DotCall τ σ ρ"
| "boolean_binop_type op τ σ ρ 
   binop_type (Inr (Inl op)) DotCall τ σ ρ"
| "numeric_binop_type op τ σ ρ 
   binop_type (Inr (Inr (Inl op))) DotCall τ σ ρ"
| "string_binop_type op τ σ ρ 
   binop_type (Inr (Inr (Inr (Inl op)))) DotCall τ σ ρ"
| "collection_binop_type op τ σ ρ 
   binop_type (Inr (Inr (Inr (Inr op)))) ArrowCall τ σ ρ"

inductive ternop_type where
  "string_ternop_type op τ σ ρ υ 
   ternop_type (Inl op) DotCall τ σ ρ υ"
| "collection_ternop_type op τ σ ρ υ 
   ternop_type (Inr op) ArrowCall τ σ ρ υ"

inductive op_type where
  "unop_type op k τ υ 
   op_type (Inl op) k τ [] υ"
| "binop_type op k τ σ υ 
   op_type (Inr (Inl op)) k τ [σ] υ"
| "ternop_type op k τ σ ρ υ 
   op_type (Inr (Inr (Inl op))) k τ [σ, ρ] υ"
| "operation τ op π oper 
   op_type (Inr (Inr (Inr op))) DotCall τ π (oper_type oper)"

(*** Simplification Rules ***************************************************)

subsection ‹Simplification Rules›

inductive_simps op_type_alt_simps:
"mataop_type τ op σ"
"typeop_type k op τ σ ρ"

"op_type op k τ π σ"
"unop_type op k τ σ"
"binop_type op k τ σ ρ"
"ternop_type op k τ σ ρ υ"

"any_unop_type op τ σ"
"boolean_unop_type op τ σ"
"numeric_unop_type op τ σ"
"string_unop_type op τ σ"
"collection_unop_type op τ σ"

"super_binop_type op τ σ ρ"
"boolean_binop_type op τ σ ρ"
"numeric_binop_type op τ σ ρ"
"string_binop_type op τ σ ρ"
"collection_binop_type op τ σ ρ"

"string_ternop_type op τ σ ρ υ"
"collection_ternop_type op τ σ ρ υ"

(*** Determinism ************************************************************)

subsection ‹Determinism›

lemma typeop_type_det:
  "typeop_type op k τ σ ρ1 
   typeop_type op k τ σ ρ2  ρ1 = ρ2"
  by (induct rule: typeop_type.induct;
      auto simp add: typeop_type.simps update_element_type_det)

lemma any_unop_type_det:
  "any_unop_type op τ σ1 
   any_unop_type op τ σ2  σ1 = σ2"
  by (induct rule: any_unop_type.induct; simp add: any_unop_type.simps)

lemma boolean_unop_type_det:
  "boolean_unop_type op τ σ1 
   boolean_unop_type op τ σ2  σ1 = σ2"
  by (induct rule: boolean_unop_type.induct; simp add: boolean_unop_type.simps)

lemma numeric_unop_type_det:
  "numeric_unop_type op τ σ1 
   numeric_unop_type op τ σ2  σ1 = σ2"
  by (induct rule: numeric_unop_type.induct; auto simp add: numeric_unop_type.simps)

lemma string_unop_type_det:
  "string_unop_type op τ σ1 
   string_unop_type op τ σ2  σ1 = σ2"
  by (induct rule: string_unop_type.induct; simp add: string_unop_type.simps)

lemma collection_unop_type_det:
  "collection_unop_type op τ σ1 
   collection_unop_type op τ σ2  σ1 = σ2"
  apply (induct rule: collection_unop_type.induct)
  by (erule collection_unop_type.cases;
      auto simp add: element_type_det update_element_type_det)+

lemma unop_type_det:
  "unop_type op k τ σ1 
   unop_type op k τ σ2  σ1 = σ2"
  by (induct rule: unop_type.induct;
      simp add: unop_type.simps any_unop_type_det
                boolean_unop_type_det numeric_unop_type_det
                string_unop_type_det collection_unop_type_det)

lemma super_binop_type_det:
  "super_binop_type op τ σ ρ1 
   super_binop_type op τ σ ρ2  ρ1 = ρ2"
  by (induct rule: super_binop_type.induct; auto simp add: super_binop_type.simps)

lemma boolean_binop_type_det:
  "boolean_binop_type op τ σ ρ1 
   boolean_binop_type op τ σ ρ2  ρ1 = ρ2"
  by (induct rule: boolean_binop_type.induct; simp add: boolean_binop_type.simps)

lemma numeric_binop_type_det:
  "numeric_binop_type op τ σ ρ1 
   numeric_binop_type op τ σ ρ2  ρ1 = ρ2"
  by (induct rule: numeric_binop_type.induct;
      auto simp add: numeric_binop_type.simps split: if_splits)

lemma string_binop_type_det:
  "string_binop_type op τ σ ρ1 
   string_binop_type op τ σ ρ2  ρ1 = ρ2"
  by (induct rule: string_binop_type.induct; simp add: string_binop_type.simps)

lemma collection_binop_type_det:
  "collection_binop_type op τ σ ρ1 
   collection_binop_type op τ σ ρ2  ρ1 = ρ2"
  apply (induct rule: collection_binop_type.induct; simp add: collection_binop_type.simps)
  using element_type_det update_element_type_det by blast+

lemma binop_type_det:
  "binop_type op k τ σ ρ1 
   binop_type op k τ σ ρ2  ρ1 = ρ2"
  by (induct rule: binop_type.induct;
      simp add: binop_type.simps super_binop_type_det
                boolean_binop_type_det numeric_binop_type_det
                string_binop_type_det collection_binop_type_det)

lemma string_ternop_type_det:
  "string_ternop_type op τ σ ρ υ1 
   string_ternop_type op τ σ ρ υ2  υ1 = υ2"
  by (induct rule: string_ternop_type.induct; simp add: string_ternop_type.simps)

lemma collection_ternop_type_det:
  "collection_ternop_type op τ σ ρ υ1 
   collection_ternop_type op τ σ ρ υ2  υ1 = υ2"
  by (induct rule: collection_ternop_type.induct; simp add: collection_ternop_type.simps)

lemma ternop_type_det:
  "ternop_type op k τ σ ρ υ1 
   ternop_type op k τ σ ρ υ2  υ1 = υ2"
  by (induct rule: ternop_type.induct;
      simp add: ternop_type.simps string_ternop_type_det collection_ternop_type_det)

lemma op_type_det:
  "op_type op k τ π σ 
   op_type op k τ π ρ  σ = ρ"
  apply (induct rule: op_type.induct)
  apply (erule op_type.cases; simp add: unop_type_det)
  apply (erule op_type.cases; simp add: binop_type_det)
  apply (erule op_type.cases; simp add: ternop_type_det)
  by (erule op_type.cases; simp; metis operation_det)

(*** Expressions Typing *****************************************************)

section ‹Expressions Typing›

text ‹
  The following typing rules are preliminary. The final rules are given at
  the end of the next chapter.›

inductive typing :: "('a :: ocl_object_model) type env  'a expr  'a type  bool"
       ("(1_/ E/ (_ :/ _))" [51,51,51] 50)
    and collection_parts_typing ("(1_/ C/ (_ :/ _))" [51,51,51] 50)
    and collection_part_typing ("(1_/ P/ (_ :/ _))" [51,51,51] 50)
    and iterator_typing ("(1_/ I/ (_ :/ _))" [51,51,51] 50)
    and expr_list_typing ("(1_/ L/ (_ :/ _))" [51,51,51] 50) where

― ‹Primitive Literals›

 NullLiteralT:
  "Γ E NullLiteral : OclVoid[?]"
|BooleanLiteralT:
  "Γ E BooleanLiteral c : Boolean[1]"
|RealLiteralT:
  "Γ E RealLiteral c : Real[1]"
|IntegerLiteralT:
  "Γ E IntegerLiteral c : Integer[1]"
|UnlimitedNaturalLiteralT:
  "Γ E UnlimitedNaturalLiteral c : UnlimitedNatural[1]"
|StringLiteralT:
  "Γ E StringLiteral c : String[1]"
|EnumLiteralT:
  "has_literal enum lit 
   Γ E EnumLiteral enum lit : (Enum enum)[1]"

― ‹Collection Literals›

|SetLiteralT:
  "Γ C prts : τ 
   Γ E CollectionLiteral SetKind prts : Set τ"
|OrderedSetLiteralT:
  "Γ C prts : τ 
   Γ E CollectionLiteral OrderedSetKind prts : OrderedSet τ"
|BagLiteralT:
  "Γ C prts : τ 
   Γ E CollectionLiteral BagKind prts : Bag τ"
|SequenceLiteralT:
  "Γ C prts : τ 
   Γ E CollectionLiteral SequenceKind prts : Sequence τ"

― ‹We prohibit empty collection literals, because their type is unclear.
  We could use @{text "OclVoid[1]"} element type for empty collections, but
  the typing rules will give wrong types for nested collections, because,
  for example, @{text "OclVoid[1] ⊔ Set(Integer[1]) = OclSuper"}

|CollectionPartsSingletonT:
  "Γ P x : τ 
   Γ C [x] : τ"
|CollectionPartsListT:
  "Γ P x : τ 
   Γ C y # xs : σ 
   Γ C x # y # xs : τ  σ"

|CollectionPartItemT:
  "Γ E a : τ 
   Γ P CollectionItem a : τ"
|CollectionPartRangeT:
  "Γ E a : τ 
   Γ E b : σ 
   τ = UnlimitedNatural[1]Integer[1] 
   σ = UnlimitedNatural[1]Integer[1] 
   Γ P CollectionRange a b : Integer[1]"

― ‹Tuple Literals›
― ‹We do not prohibit empty tuples, because it could be useful.
  @{text "Tuple()"} is a supertype of all other tuple types.›

|TupleLiteralNilT:
  "Γ E TupleLiteral [] : Tuple fmempty"
|TupleLiteralConsT:
  "Γ E TupleLiteral elems : Tuple ξ 
   Γ E tuple_element_expr el : τ 
   tuple_element_type el = Some σ 
   τ  σ 
   Γ E TupleLiteral (el # elems) : Tuple (ξ(tuple_element_name el f σ))"

― ‹Misc Expressions›

|LetT:
  "Γ E init : σ 
   σ  τ 
   Γ(v f τ) E body : ρ 
   Γ E Let v (Some τ) init body : ρ"
|VarT:
  "fmlookup Γ v = Some τ 
   Γ E Var v : τ"
|IfT:
  "Γ E a : Boolean[1] 
   Γ E b : σ 
   Γ E c : ρ 
   Γ E If a b c : σ  ρ"

― ‹Call Expressions›

|MetaOperationCallT:
  "mataop_type τ op σ 
   Γ E MetaOperationCall τ op : σ"
|StaticOperationCallT:
  "Γ L params : π 
   static_operation τ op π oper 
   Γ E StaticOperationCall τ op params : oper_type oper"

|TypeOperationCallT:
  "Γ E a : τ 
   typeop_type k op τ σ ρ 
   Γ E TypeOperationCall a k op σ : ρ"

|AttributeCallT:
  "Γ E src : 𝒞𝒯[1] 
   attribute 𝒞 prop 𝒟 τ 
   Γ E AttributeCall src DotCall prop : τ"
|AssociationEndCallT:
  "Γ E src : 𝒞𝒯[1] 
   association_end 𝒞 from role 𝒟 end 
   Γ E AssociationEndCall src DotCall from role : assoc_end_type end"
|AssociationClassCallT:
  "Γ E src : 𝒞𝒯[1] 
   referred_by_association_class 𝒞 from 𝒜 𝒟 
   Γ E AssociationClassCall src DotCall from 𝒜 : class_assoc_type 𝒜"
|AssociationClassEndCallT:
  "Γ E src : 𝒜𝒯[1] 
   association_class_end 𝒜 role end 
   Γ E AssociationClassEndCall src DotCall role : class_assoc_end_type end"
|OperationCallT:
  "Γ E src : τ 
   Γ L params : π 
   op_type op k τ π σ 
   Γ E OperationCall src k op params : σ"

|TupleElementCallT:
  "Γ E src : Tuple π 
   fmlookup π elem = Some τ 
   Γ E TupleElementCall src DotCall elem : τ"

― ‹Iterator Expressions›

|IteratorT:
  "Γ E src : τ 
   element_type τ σ 
   σ  its_ty 
   Γ ++f fmap_of_list (map (λit. (it, its_ty)) its) E body : ρ 
   Γ I (src, its, (Some its_ty), body) : (τ, σ, ρ)"

|IterateT:
  "Γ I (src, its, its_ty, Let res (Some res_t) res_init body) : (τ, σ, ρ) 
   ρ  res_t 
   Γ E IterateCall src ArrowCall its its_ty res (Some res_t) res_init body : ρ"

|AnyIteratorT:
  "Γ I (src, its, its_ty, body) : (τ, σ, ρ) 
   length its  1 
   ρ  Boolean[?] 
   Γ E AnyIteratorCall src ArrowCall its its_ty body : σ"
|ClosureIteratorT:
  "Γ I (src, its, its_ty, body) : (τ, σ, ρ) 
   length its  1 
   to_single_type ρ  σ 
   to_unique_collection τ υ 
   Γ E ClosureIteratorCall src ArrowCall its its_ty body : υ"
|CollectIteratorT:
  "Γ I (src, its, its_ty, body) : (τ, σ, ρ) 
   length its  1 
   to_nonunique_collection τ υ 
   update_element_type υ (to_single_type ρ) φ 
   Γ E CollectIteratorCall src ArrowCall its its_ty body : φ"
|CollectNestedIteratorT:
  "Γ I (src, its, its_ty, body) : (τ, σ, ρ) 
   length its  1 
   to_nonunique_collection τ υ 
   update_element_type υ ρ φ 
   Γ E CollectNestedIteratorCall src ArrowCall its its_ty body : φ"
|ExistsIteratorT:
  "Γ I (src, its, its_ty, body) : (τ, σ, ρ) 
   ρ  Boolean[?] 
   Γ E ExistsIteratorCall src ArrowCall its its_ty body : ρ"
|ForAllIteratorT:
  "Γ I (src, its, its_ty, body) : (τ, σ, ρ) 
   ρ  Boolean[?] 
   Γ E ForAllIteratorCall src ArrowCall its its_ty body : ρ"
|OneIteratorT:
  "Γ I (src, its, its_ty, body) : (τ, σ, ρ) 
   length its  1 
   ρ  Boolean[?] 
   Γ E OneIteratorCall src ArrowCall its its_ty body : Boolean[1]"
|IsUniqueIteratorT:
  "Γ I (src, its, its_ty, body) : (τ, σ, ρ) 
   length its  1 
   Γ E IsUniqueIteratorCall src ArrowCall its its_ty body : Boolean[1]"
|SelectIteratorT:
  "Γ I (src, its, its_ty, body) : (τ, σ, ρ) 
   length its  1 
   ρ  Boolean[?] 
   Γ E SelectIteratorCall src ArrowCall its its_ty body : τ"
|RejectIteratorT:
  "Γ I (src, its, its_ty, body) : (τ, σ, ρ) 
   length its  1 
   ρ  Boolean[?] 
   Γ E RejectIteratorCall src ArrowCall its its_ty body : τ"
|SortedByIteratorT:
  "Γ I (src, its, its_ty, body) : (τ, σ, ρ) 
   length its  1 
   to_ordered_collection τ υ 
   Γ E SortedByIteratorCall src ArrowCall its its_ty body : υ"

― ‹Expression Lists›

|ExprListNilT:
  "Γ L [] : []"
|ExprListConsT:
  "Γ E expr : τ 
   Γ L exprs : π 
   Γ L expr # exprs : τ # π"

(*** Elimination Rules ******************************************************)

section ‹Elimination Rules›

inductive_cases NullLiteralTE [elim]: "Γ E NullLiteral : τ"
inductive_cases BooleanLiteralTE [elim]: "Γ E BooleanLiteral c : τ"
inductive_cases RealLiteralTE [elim]: "Γ E RealLiteral c : τ"
inductive_cases IntegerLiteralTE [elim]: "Γ E IntegerLiteral c : τ"
inductive_cases UnlimitedNaturalLiteralTE [elim]: "Γ E UnlimitedNaturalLiteral c : τ"
inductive_cases StringLiteralTE [elim]: "Γ E StringLiteral c : τ"
inductive_cases EnumLiteralTE [elim]: "Γ E EnumLiteral enm lit : τ"
inductive_cases CollectionLiteralTE [elim]: "Γ E CollectionLiteral k prts : τ"
inductive_cases TupleLiteralTE [elim]: "Γ E TupleLiteral elems : τ"

inductive_cases LetTE [elim]: "Γ E Let v τ init body : σ"
inductive_cases VarTE [elim]: "Γ E Var v : τ"
inductive_cases IfTE [elim]: "Γ E If a b c : τ"

inductive_cases MetaOperationCallTE [elim]: "Γ E MetaOperationCall τ op : σ"
inductive_cases StaticOperationCallTE [elim]: "Γ E StaticOperationCall τ op as : σ"

inductive_cases TypeOperationCallTE [elim]: "Γ E TypeOperationCall a k op σ : τ"
inductive_cases AttributeCallTE [elim]: "Γ E AttributeCall src k prop : τ"
inductive_cases AssociationEndCallTE [elim]: "Γ E AssociationEndCall src k role from : τ"
inductive_cases AssociationClassCallTE [elim]: "Γ E AssociationClassCall src k a from : τ"
inductive_cases AssociationClassEndCallTE [elim]: "Γ E AssociationClassEndCall src k role : τ"
inductive_cases OperationCallTE [elim]: "Γ E OperationCall src k op params : τ"
inductive_cases TupleElementCallTE [elim]: "Γ E TupleElementCall src k elem : τ"

inductive_cases IteratorTE [elim]: "Γ I (src, its, body) : ys"
inductive_cases IterateTE [elim]: "Γ E IterateCall src k its its_ty res res_t res_init body : τ"
inductive_cases AnyIteratorTE [elim]: "Γ E AnyIteratorCall src k its its_ty body : τ"
inductive_cases ClosureIteratorTE [elim]: "Γ E ClosureIteratorCall src k its its_ty body : τ"
inductive_cases CollectIteratorTE [elim]: "Γ E CollectIteratorCall src k its its_ty body : τ"
inductive_cases CollectNestedIteratorTE [elim]: "Γ E CollectNestedIteratorCall src k its its_ty body : τ"
inductive_cases ExistsIteratorTE [elim]: "Γ E ExistsIteratorCall src k its its_ty body : τ"
inductive_cases ForAllIteratorTE [elim]: "Γ E ForAllIteratorCall src k its its_ty body : τ"
inductive_cases OneIteratorTE [elim]: "Γ E OneIteratorCall src k its its_ty body : τ"
inductive_cases IsUniqueIteratorTE [elim]: "Γ E IsUniqueIteratorCall src k its its_ty body : τ"
inductive_cases SelectIteratorTE [elim]: "Γ E SelectIteratorCall src k its its_ty body : τ"
inductive_cases RejectIteratorTE [elim]: "Γ E RejectIteratorCall src k its its_ty body : τ"
inductive_cases SortedByIteratorTE [elim]: "Γ E SortedByIteratorCall src k its its_ty body : τ"

inductive_cases CollectionPartsNilTE [elim]: "Γ C [x] : τ"
inductive_cases CollectionPartsItemTE [elim]: "Γ C x # y # xs : τ"

inductive_cases CollectionItemTE [elim]: "Γ P CollectionItem a : τ"
inductive_cases CollectionRangeTE [elim]: "Γ P CollectionRange a b : τ"

inductive_cases ExprListTE [elim]: "Γ L exprs : π"

(*** Simplification Rules ***************************************************)

section ‹Simplification Rules›

inductive_simps typing_alt_simps: 
"Γ E NullLiteral : τ"
"Γ E BooleanLiteral c : τ"
"Γ E RealLiteral c : τ"
"Γ E UnlimitedNaturalLiteral c : τ"
"Γ E IntegerLiteral c : τ"
"Γ E StringLiteral c : τ"
"Γ E EnumLiteral enm lit : τ"
"Γ E CollectionLiteral k prts : τ"
"Γ E TupleLiteral [] : τ"
"Γ E TupleLiteral (x # xs) : τ"

"Γ E Let v τ init body : σ"
"Γ E Var v : τ"
"Γ E If a b c : τ"

"Γ E MetaOperationCall τ op : σ"
"Γ E StaticOperationCall τ op as : σ"

"Γ E TypeOperationCall a k op σ : τ"
"Γ E AttributeCall src k prop : τ"
"Γ E AssociationEndCall src k role from : τ"
"Γ E AssociationClassCall src k a from : τ"
"Γ E AssociationClassEndCall src k role : τ"
"Γ E OperationCall src k op params : τ"
"Γ E TupleElementCall src k elem : τ"

"Γ I (src, its, body) : ys"
"Γ E IterateCall src k its its_ty res res_t res_init body : τ"
"Γ E AnyIteratorCall src k its its_ty body : τ"
"Γ E ClosureIteratorCall src k its its_ty body : τ"
"Γ E CollectIteratorCall src k its its_ty body : τ"
"Γ E CollectNestedIteratorCall src k its its_ty body : τ"
"Γ E ExistsIteratorCall src k its its_ty body : τ"
"Γ E ForAllIteratorCall src k its its_ty body : τ"
"Γ E OneIteratorCall src k its its_ty body : τ"
"Γ E IsUniqueIteratorCall src k its its_ty body : τ"
"Γ E SelectIteratorCall src k its its_ty body : τ"
"Γ E RejectIteratorCall src k its its_ty body : τ"
"Γ E SortedByIteratorCall src k its its_ty body : τ"

"Γ C [x] : τ"
"Γ C x # y # xs : τ"

"Γ P CollectionItem a : τ"
"Γ P CollectionRange a b : τ"

"Γ L [] : π"
"Γ L x # xs : π"

(*** Determinism ************************************************************)

section ‹Determinism›

lemma
  typing_det:
    "Γ E expr : τ 
     Γ E expr : σ  τ = σ" and
  collection_parts_typing_det:
    "Γ C prts : τ 
     Γ C prts : σ  τ = σ" and
  collection_part_typing_det:
    "Γ P prt : τ 
     Γ P prt : σ  τ = σ" and
  iterator_typing_det:
    "Γ I (src, its, body) : xs 
     Γ I (src, its, body) : ys  xs = ys" and
  expr_list_typing_det:
    "Γ L exprs : π 
     Γ L exprs : ξ  π = ξ"
proof (induct arbitrary: σ and σ and σ and ys and ξ
       rule: typing_collection_parts_typing_collection_part_typing_iterator_typing_expr_list_typing.inducts)
  case (NullLiteralT Γ) thus ?case by auto
next
  case (BooleanLiteralT Γ c) thus ?case by auto
next
  case (RealLiteralT Γ c) thus ?case by auto
next
  case (IntegerLiteralT Γ c) thus ?case by auto
next
  case (UnlimitedNaturalLiteralT Γ c) thus ?case by auto
next
  case (StringLiteralT Γ c) thus ?case by auto
next
  case (EnumLiteralT Γ τ lit) thus ?case by auto
next
  case (SetLiteralT Γ prts τ) thus ?case by blast
next
  case (OrderedSetLiteralT Γ prts τ) thus ?case by blast
next
  case (BagLiteralT Γ prts τ) thus ?case by blast
next
  case (SequenceLiteralT Γ prts τ) thus ?case by blast
next
  case (CollectionPartsSingletonT Γ x τ) thus ?case by blast
next
  case (CollectionPartsListT Γ x τ y xs σ) thus ?case by blast
next
  case (CollectionPartItemT Γ a τ) thus ?case by blast
next
  case (CollectionPartRangeT Γ a τ b σ) thus ?case by blast
next
  case (TupleLiteralNilT Γ) thus ?case by auto
next
  case (TupleLiteralConsT Γ elems ξ el τ) show ?case
    apply (insert TupleLiteralConsT.prems)
    apply (erule TupleLiteralTE, simp)
    using TupleLiteralConsT.hyps by auto
next
  case (LetT Γ  init σ τ v body ρ) thus ?case by blast
next
  case (VarT Γ v τ ) thus ?case by auto
next
  case (IfT Γ a τ b σ c ρ) thus ?case
    apply (insert IfT.prems)
    apply (erule IfTE)
    by (simp add: IfT.hyps)
next
  case (MetaOperationCallT τ op σ Γ) thus ?case
    by (metis MetaOperationCallTE mataop_type.cases)
next
  case (StaticOperationCallT τ op π oper Γ as) thus ?case
    apply (insert StaticOperationCallT.prems)
    apply (erule StaticOperationCallTE)
    using StaticOperationCallT.hyps static_operation_det by blast
next
  case (TypeOperationCallT Γ a τ op σ ρ) thus ?case
    by (metis TypeOperationCallTE typeop_type_det)
next
  case (AttributeCallT Γ src τ 𝒞 "prop" 𝒟 σ) show ?case
    apply (insert AttributeCallT.prems)
    apply (erule AttributeCallTE)
    using AttributeCallT.hyps attribute_det by blast
next
  case (AssociationEndCallT Γ src 𝒞 "from" role 𝒟 "end") show ?case
    apply (insert AssociationEndCallT.prems)
    apply (erule AssociationEndCallTE)
    using AssociationEndCallT.hyps association_end_det by blast
next
  case (AssociationClassCallT Γ src 𝒞 "from" 𝒜) thus ?case by blast
next
  case (AssociationClassEndCallT Γ src τ 𝒜 role "end") show ?case
    apply (insert AssociationClassEndCallT.prems)
    apply (erule AssociationClassEndCallTE)
    using AssociationClassEndCallT.hyps association_class_end_det by blast
next
  case (OperationCallT Γ src τ params π op k) show ?case
    apply (insert OperationCallT.prems)
    apply (erule OperationCallTE)
    using OperationCallT.hyps op_type_det by blast
next
  case (TupleElementCallT Γ src π elem τ) thus ?case 
    apply (insert TupleElementCallT.prems)
    apply (erule TupleElementCallTE)
    using TupleElementCallT.hyps by fastforce
next
  case (IteratorT Γ src τ σ its_ty its body ρ) show ?case
    apply (insert IteratorT.prems)
    apply (erule IteratorTE)
    using IteratorT.hyps element_type_det by blast
next
  case (IterateT Γ src its its_ty res res_t res_init body τ σ ρ) show ?case
    apply (insert IterateT.prems)
    using IterateT.hyps by blast
next
  case (AnyIteratorT Γ src its its_ty body τ σ ρ) thus ?case
    by (meson AnyIteratorTE Pair_inject)
next
  case (ClosureIteratorT Γ src its its_ty body τ σ ρ υ) show ?case
    apply (insert ClosureIteratorT.prems)
    apply (erule ClosureIteratorTE)
    using ClosureIteratorT.hyps to_unique_collection_det by blast
next
  case (CollectIteratorT Γ src its its_ty body τ σ ρ υ) show ?case
    apply (insert CollectIteratorT.prems)
    apply (erule CollectIteratorTE)
    using CollectIteratorT.hyps to_nonunique_collection_det
      update_element_type_det Pair_inject by metis
next
  case (CollectNestedIteratorT Γ src its its_ty body τ σ ρ υ) show ?case
    apply (insert CollectNestedIteratorT.prems)
    apply (erule CollectNestedIteratorTE)
    using CollectNestedIteratorT.hyps to_nonunique_collection_det
      update_element_type_det Pair_inject by metis
next
  case (ExistsIteratorT Γ src its its_ty body τ σ ρ) show ?case
    apply (insert ExistsIteratorT.prems)
    apply (erule ExistsIteratorTE)
    using ExistsIteratorT.hyps Pair_inject by metis
next
  case (ForAllIteratorT Γ  src its its_ty body τ σ ρ) show ?case
    apply (insert ForAllIteratorT.prems)
    apply (erule ForAllIteratorTE)
    using ForAllIteratorT.hyps Pair_inject by metis
next
  case (OneIteratorT Γ  src its its_ty body τ σ ρ) show ?case
    apply (insert OneIteratorT.prems)
    apply (erule OneIteratorTE)
    by simp
next
  case (IsUniqueIteratorT Γ  src its its_ty body τ σ ρ) show ?case
    apply (insert IsUniqueIteratorT.prems)
    apply (erule IsUniqueIteratorTE)
    by simp
next
  case (SelectIteratorT Γ  src its its_ty body τ σ ρ) show ?case
    apply (insert SelectIteratorT.prems)
    apply (erule SelectIteratorTE)
    using SelectIteratorT.hyps by blast
next
  case (RejectIteratorT Γ  src its its_ty body τ σ ρ) show ?case
    apply (insert RejectIteratorT.prems)
    apply (erule RejectIteratorTE)
    using RejectIteratorT.hyps by blast
next
  case (SortedByIteratorT Γ  src its its_ty body τ σ ρ υ) show ?case
    apply (insert SortedByIteratorT.prems)
    apply (erule SortedByIteratorTE)
    using SortedByIteratorT.hyps to_ordered_collection_det by blast
next
  case (ExprListNilT Γ) thus ?case
    using expr_list_typing.cases by auto
next
  case (ExprListConsT Γ expr τ exprs π) show ?case
    apply (insert ExprListConsT.prems)
    apply (erule ExprListTE)
    by (simp_all add: ExprListConsT.hyps)
qed

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

section ‹Code Setup›

code_pred op_type .
code_pred (modes:
    i ⇒ i ⇒ i ⇒ bool,
    i ⇒ i ⇒ o ⇒ bool) iterator_typing .

end

Theory OCL_Normalization

(*  Title:       Safe OCL
    Author:      Denis Nikiforov, March 2019
    Maintainer:  Denis Nikiforov <denis.nikif at gmail.com>
    License:     LGPL
*)
chapter ‹Normalization›
theory OCL_Normalization
  imports OCL_Typing
begin

(*** Normalization Rules ****************************************************)

section ‹Normalization Rules›

text ‹
  The following expression normalization rules includes two kinds of an
  abstract syntax tree transformations:
\begin{itemize}
\item determination of implicit types of variables, iterators, and
      tuple elements,
\item unfolding of navigation shorthands and safe navigation operators,
      described in \autoref{tab:norm_rules}.
\end{itemize}

  The following variables are used in the table:
\begin{itemize}
\item ‹x› is a non-nullable value,
\item ‹n› is a nullable value,
\item ‹xs› is a collection of non-nullable values,
\item ‹ns› is a collection of nullable values. 
\end{itemize}

\begin{table}[h!]
  \begin{center}
    \caption{Expression Normalization Rules}
    \label{tab:norm_rules}
    \begin{threeparttable}
    \begin{tabular}{c|c}
      \textbf{Orig. expr.} & \textbf{Normalized expression}\\
      \hline
      ‹x.op()› & ‹x.op()›\\
      ‹n.op()› & ‹n.op()›\tnote{*}\\
      ‹x?.op()› & ---\\
      ‹n?.op()› & ‹if n <> null then n.oclAsType(T[1]).op() else null endif›\tnote{**}\\
      ‹x->op()› & ‹x.oclAsSet()->op()›\\
      ‹n->op()› & ‹n.oclAsSet()->op()›\\
      ‹x?->op()› & ---\\
      ‹n?->op()› & ---\\
      \hline
      ‹xs.op()› & ‹xs->collect(x | x.op())›\\
      ‹ns.op()› & ‹ns->collect(n | n.op())›\tnote{*}\\
      ‹xs?.op()› & ---\\
      ‹ns?.op()› & ‹ns->selectByKind(T[1])->collect(x | x.op())›\\
      ‹xs->op()› & ‹xs->op()›\\
      ‹ns->op()› & ‹ns->op()›\\
      ‹xs?->op()› & ---\\
      ‹ns?->op()› & ‹ns->selectByKind(T[1])->op()›\\
    \end{tabular}
    \begin{tablenotes}
    \item[*] The resulting expression will be ill-typed if the operation is unsafe.
    An unsafe operation is an operation which is well-typed for
    a non-nullable source only.
    \item[**] It would be a good idea to prohibit such a transformation
    for safe operations. A safe operation is an operation which is well-typed
    for a nullable source. However, it is hard to define safe operations
    formally considering operations overloading, complex relations between
    operation parameters types (please see the typing rules for the equality
    operator), and user-defined operations.
    \end{tablenotes}
    \end{threeparttable}
  \end{center}
\end{table}

  Please take a note that name resolution of variables, types,
  attributes, and associations is out of scope of this section.
  It should be done on a previous phase during transformation
  of a concrete syntax tree to an abstract syntax tree.›

fun string_of_nat :: "nat  string" where
  "string_of_nat n = (if n < 10 then [char_of (48 + n)]
      else string_of_nat (n div 10) @ [char_of (48 + (n mod 10))])"

definition "new_vname  String.implode  string_of_nat  fcard  fmdom"

inductive normalize
    :: "('a :: ocl_object_model) type env  'a expr  'a expr  bool"
    ("_  _ / _" [51,51,51] 50) and
    normalize_call ("_ C _ / _" [51,51,51] 50) and
    normalize_expr_list ("_ L _ / _" [51,51,51] 50)
    where
 LiteralN:
  "Γ  Literal a  Literal a"
|ExplicitlyTypedLetN:
  "Γ  init1  init2 
   Γ(v f τ)  body1  body2 
   Γ  Let v (Some τ) init1 body1  Let v (Some τ) init2 body2"
|ImplicitlyTypedLetN:
  "Γ  init1  init2 
   Γ E init2 : τ 
   Γ(v f τ)  body1  body2 
   Γ  Let v None init1 body1  Let v (Some τ) init2 body2"
|VarN:
  "Γ  Var v  Var v"
|IfN:
  "Γ  a1  a2 
   Γ  b1  b2 
   Γ  c1  c2 
   Γ  If a1 b1 c1  If a2 b2 c2"

|MetaOperationCallN:
  "Γ  MetaOperationCall τ op  MetaOperationCall τ op"
|StaticOperationCallN:
  "Γ L params1  params2