Theory Type

(*  Title:      Jinja/Common/Type.thy

    Author:     David von Oheimb, Tobias Nipkow
    Copyright   1999 Technische Universitaet Muenchen
*)

section ‹Jinja 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 Object :: cname
where
  "Object ≡ ''Object''"

definition this :: vname
where
  "this ≡ ''this''"

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

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 ⟹ 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