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