Theory OCL_Basic_Types

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

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

section ‹Definition›

text ‹
  Basic types are parameterized over classes.›

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

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

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

| "UnlimitedNatural ⊏B Integer"
| "Integer ⊏B Real"
| "𝒞 < 𝒟 ⟹ ⟨𝒞⟩𝒯 ⊏B ⟨𝒟⟩𝒯"

| "Boolean ⊏B OclAny"
| "Real ⊏B OclAny"
| "String ⊏B OclAny"
| "⟨𝒞⟩𝒯 ⊏B OclAny"
| "Enum ℰ ⊏B OclAny"

declare basic_subtype.intros [intro!]

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

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

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

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

section ‹Partial Order of Basic Types›

instantiation basic_type :: (order) order
begin

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

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

subsection ‹Strict Introduction Rules›

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

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

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

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

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

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

subsection ‹Strict Elimination Rules›

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

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

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

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

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

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

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

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

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

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

subsection ‹Properties›

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

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

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

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

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

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

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

end

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

subsection ‹Non-Strict Introduction Rules›

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

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

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

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

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

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

subsection ‹Non-Strict Elimination Rules›

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

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

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

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

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

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

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

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

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

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

subsection ‹Simplification Rules›

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

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

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

section ‹Upper Semilattice of Basic Types›

notation sup (infixl "⊔" 65)

instantiation basic_type :: (semilattice_sup) semilattice_sup
begin

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

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

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

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

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

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

end

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

section ‹Code Setup›

code_pred basic_subtype .

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

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

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

end