Theory Type

(*  Title:      Jinja/Common/Type.thy
    ID:         $Id: Type.html 1910 2004-05-19 04:46:04Z kleing $
    Author:     David von Oheimb, Tobias Nipkow
    Copyright   1999 Technische Universitaet Muenchen
*)

header {* \isaheader{Jinja types} *}

theory Type = Aux:

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

constdefs
  Object :: cname
  "Object ≡ ''Object''"
  this :: vname
  "this ≡ ''this''"

-- "types"
datatype ty
  = Void          -- "type of statements"
  | Boolean
  | Integer
  | NT            -- "null type"
  | Class cname   -- "class type"

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 ==> P; !!C. T = Class C ==> P |] ==> P"
(*<*)by (auto simp add: is_refT_def)(*>*)

lemma not_refTE:
  "[| ¬is_refT T; T = Void ∨ T = Boolean ∨ T = Integer ==> P |] ==> P"
(*<*)by (cases T, auto simp add: is_refT_def)(*>*)

end