Theory Type

(*  Title:       CoreC++
    Author:      Daniel Wasserrab
    Maintainer:  Daniel Wasserrab <wasserra at>

    Based on the Jinja theory Common/Decl.thy by David von Oheimb and Tobias Nipkow 

section ‹CoreC++ types›

theory Type imports Auxiliary begin

type_synonym cname = string ― ‹class names›
type_synonym mname = string ― ‹method name›
type_synonym vname = string ― ‹names for local/field variables›
definition this :: vname where
  "this  ''this''"

― ‹types›
datatype ty
  = Void          ― ‹type of statements›
  | Boolean
  | Integer
  | NT            ― ‹null type›
  | Class cname   ― ‹class type›

datatype base  ― ‹superclass›
  = Repeats cname  ― ‹repeated (nonvirtual) inheritance›
  | Shares cname   ― ‹shared (virtual) inheritance›

primrec getbase :: "base  cname" where
  "getbase (Repeats C) = C"
| "getbase (Shares C)  = C"

primrec isRepBase :: "base  bool" where
  "isRepBase (Repeats C) = True"
| "isRepBase (Shares C) = False"

primrec isShBase :: "base  bool" where
  "isShBase(Repeats C) = False"
| "isShBase(Shares C) = True"

definition is_refT :: "ty  bool" where
  "is_refT T    T = NT  (C. T = Class C)"

lemma [iff]: "is_refT NT"
by(simp add:is_refT_def)

lemma [iff]: "is_refT(Class C)"
by(simp add:is_refT_def)

lemma refTE:
  "is_refT T; T = NT  Q; C. T = Class C  Q   Q"
by (auto simp add: is_refT_def)

lemma not_refTE:
  " ¬is_refT T; T = Void  T = Boolean  T = Integer  Q   Q"
by (cases T, auto simp add: is_refT_def)

  env  = "vname  ty"