Theory OCL_Types

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

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

section ‹Definition›

text ‹
  Types are parameterized over classes.›

type_synonym telem = String.literal

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

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

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

definition "OclInvalid :: 'a type⊥ ≡ ⊥"

instantiation type :: (type) size
begin

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

instance ..

end

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

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

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

declare subtype.intros [intro!]

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

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

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

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

section ‹Constructors Bijectivity on Transitive Closures›

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

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

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

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

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

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

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

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

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

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

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

section ‹Partial Order of Types›

instantiation type :: (order) order
begin

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

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

subsection ‹Strict Introduction Rules›

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

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

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

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

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

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

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

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

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

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

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

subsection ‹Strict Elimination Rules›

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

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

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

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

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

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

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

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

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

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

subsection ‹Properties›

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

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

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

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

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

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

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

end

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

subsection ‹Non-Strict Introduction Rules›

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

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

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

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

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

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

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

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

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

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

subsection ‹Non-Strict Elimination Rules›

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

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

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

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

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

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

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

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

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

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

subsection ‹Simplification Rules›

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

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

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

section ‹Upper Semilattice of Types›

instantiation type :: (semilattice_sup) semilattice_sup
begin

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

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

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

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

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

end

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

section ‹Helper Relations›

abbreviation between (‹_/ = _─_›  [51, 51, 51] 50) where
  "x = 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