header {* \isaheader{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