subsection ‹Java names›
theory Name imports Basis begin
typedecl tnam ―‹ordinary type name, i.e. class or interface name›
typedecl pname ―‹package name›
typedecl mname ―‹method name›
typedecl vname ―‹variable or field name›
typedecl label ―‹label as destination of break or continue›
datatype ename ―‹expression name›
= VNam vname
| Res ―‹special name to model the return value of methods›
datatype lname ―‹names for local variables and the This pointer›
= EName ename
| This
abbreviation VName :: "vname ⇒ lname"
where "VName n == EName (VNam n)"
abbreviation Result :: lname
where "Result == EName Res"
datatype xname ―‹names of standard exceptions›
= Throwable
| NullPointer | OutOfMemory | ClassCast
| NegArrSize | IndOutBound | ArrStore
lemma xn_cases:
"xn = Throwable ∨ xn = NullPointer ∨
xn = OutOfMemory ∨ xn = ClassCast ∨
xn = NegArrSize ∨ xn = IndOutBound ∨ xn = ArrStore"
apply (induct xn)
apply auto
done
datatype tname ―‹type names for standard classes and other type names›
= Object'
| SXcpt' xname
| TName tnam
record qtname = ―‹qualified tname cf. 6.5.3, 6.5.4›
pid :: pname
tid :: tname
class has_pname =
fixes pname :: "'a ⇒ pname"
instantiation pname :: has_pname
begin
definition
pname_pname_def: "pname (p::pname) ≡ p"
instance ..
end
class has_tname =
fixes tname :: "'a ⇒ tname"
instantiation tname :: has_tname
begin
definition
tname_tname_def: "tname (t::tname) = t"
instance ..
end
definition
qtname_qtname_def: "qtname (q::'a qtname_scheme) = q"
translations
(type) "qtname" <= (type) "⦇pid::pname,tid::tname⦈"
(type) "'a qtname_scheme" <= (type) "⦇pid::pname,tid::tname,…::'a⦈"
axiomatization java_lang::pname ―‹package java.lang›
definition
Object :: qtname
where "Object = ⦇pid = java_lang, tid = Object'⦈"
definition SXcpt :: "xname ⇒ qtname"
where "SXcpt = (λx. ⦇pid = java_lang, tid = SXcpt' x⦈)"
lemma Object_neq_SXcpt [simp]: "Object ≠ SXcpt xn"
by (simp add: Object_def SXcpt_def)
lemma SXcpt_inject [simp]: "(SXcpt xn = SXcpt xm) = (xn = xm)"
by (simp add: SXcpt_def)
end