Theory Type

(*  Title:      JinjaDCI/Common/Type.thy

    Author:     David von Oheimb, Tobias Nipkow, Susannah Mansky
    Copyright   1999 Technische Universitaet Muenchen, 2019-20 UIUC

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

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
  "Object  ''Object''"

definition this :: vname
  "this  ''this''"

definition clinit :: "string" where "clinit = ''<clinit>''"
definition init :: "string" where "init = ''<init>''"

definition start_m :: "string" where "start_m = ''<start>''"
definition Start :: "string" where "Start = ''<Start>''"

lemma start_m_neq_clinit [simp]: "start_m  clinit" by(simp add: start_m_def clinit_def)
lemma Object_neq_Start [simp]: "Object  Start" by(simp add: Object_def Start_def)
lemma Start_neq_Object [simp]: "Start  Object" by(simp add: Object_def Start_def)

― ‹field/method static flag›

datatype staticb = Static | NonStatic

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

definition 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)(*>*)