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