Theory JinjaDCI.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
where
  "Object ≡ ''Object''"

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