Theory Type

(*  Title:       CoreC++
    ID:          $Id: Type.thy,v 1.6 2006-11-06 11:54:13 wasserra Exp $
    Author:      Daniel Wasserrab
    Maintainer:  Daniel Wasserrab <wasserra at fmi.uni-passau.de>

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


header {* \isaheader{CoreC++ types} *}

theory Type imports Aux begin


types
 cname = string -- "class names"
 mname = string -- "method name"
 vname = string -- "names for local/field variables"
 

constdefs
 this :: vname
"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"

consts 
  getbase :: "base => cname"
  isRepBase :: "base => bool"
  isShBase :: "base => bool"

primrec
  "getbase (Repeats C) = C"
  "getbase (Shares C)  = C"
primrec
  "isRepBase (Repeats C) = True"
  "isRepBase (Shares C) = False"
primrec
  "isShBase(Repeats C) = False"
  "isShBase(Shares C) = True"

constdefs
  is_refT :: "ty => bool"
  "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)

types 
  env  = "vname \<rightharpoonup> ty"

end