# Theory Errorable

(*  Title:       Safe OCL
Author:      Denis Nikiforov, March 2019
Maintainer:  Denis Nikiforov <denis.nikif at gmail.com>
*)
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>
*)
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>
*)
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>
*)
(* 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>
*)
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 end⇩1 ⟹
association_ends' classes associations 𝒞 from role end⇩2 ⟹
end⇩1 ≠ end⇩2 ⟹
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 end⇩1 ⟹
association_ends' classes associations 𝒞 from role end⇩2 ⟹ end⇩1 = end⇩2"
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 end⇩1 ⟹
association_end 𝒞 from role 𝒟⇩2 end⇩2 ⟹ 𝒟⇩1 = 𝒟⇩2 ∧ end⇩1 = end⇩2"
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 end⇩1 ⟹
association_class_end 𝒜 role end⇩2 ⟹ end⇩1 = end⇩2"
by (meson association_class_end_not_unique.intros unique_association_class_end.cases)

lemma (in object_model) operation_det:
"operation τ name π oper⇩1 ⟹
operation τ name π oper⇩2 ⟹ oper⇩1 = oper⇩2"
by (meson operation_not_unique.intros unique_operation.cases)

lemma (in object_model) static_operation_det:
"static_operation τ name π oper⇩1 ⟹
static_operation τ name π oper⇩2 ⟹ oper⇩1 = oper⇩2"
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>
*)
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>
*)
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;
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 = y─z ≡ 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>
*)
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>
*)
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 end⇩1 ⟹
association_ends' classes associations 𝒞 from role end⇩2 ⟹ end⇩1 = end⇩2"
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>
*)
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

(*** 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])"}

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>
*)
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:
"Γ ⊢ init⇩1 ⇛ init⇩2 ⟹
Γ(v ↦⇩f τ) ⊢ body⇩1 ⇛ body⇩2 ⟹
Γ ⊢ Let v (Some τ) init⇩1 body⇩1 ⇛ Let v (Some τ) init⇩2 body⇩2"
|ImplicitlyTypedLetN:
"Γ ⊢ init⇩1 ⇛ init⇩2 ⟹
Γ ⊢⇩E init⇩2 : τ ⟹
Γ(v ↦⇩f τ) ⊢ body⇩1 ⇛ body⇩2 ⟹
Γ ⊢ Let v None init⇩1 body⇩1 ⇛ Let v (Some τ) init⇩2 body⇩2"
|VarN:
"Γ ⊢ Var v ⇛ Var v"
|IfN:
"Γ ⊢ a⇩1 ⇛ a⇩2 ⟹
Γ ⊢ b⇩1 ⇛ b⇩2 ⟹
Γ ⊢ c⇩1 ⇛ c⇩2 ⟹
Γ ⊢ If a⇩1 b⇩1 c⇩1 ⇛ If a⇩2 b⇩2 c⇩2"

|MetaOperationCallN:
"Γ ⊢ MetaOperationCall τ op ⇛ MetaOperationCall τ op"
|StaticOperationCallN:
"Γ ⊢⇩L params⇩1 ⇛ params⇩2 ⟹