|
(* Title: HOL/Bali/Name.thy
Author: David von Oheimb
*)
subsection \<open>Java names\<close>
theory Name imports Basis begin
(* cf. 6.5 *)
typedecl tnam \<comment> \<open>ordinary type name, i.e. class or interface name\<close>
typedecl pname \<comment> \<open>package name\<close>
typedecl mname \<comment> \<open>method name\<close>
typedecl vname \<comment> \<open>variable or field name\<close>
typedecl label \<comment> \<open>label as destination of break or continue\<close>
datatype ename \<comment> \<open>expression name\<close>
= VNam vname
| Res \<comment> \<open>special name to model the return value of methods\<close>
datatype lname \<comment> \<open>names for local variables and the This pointer\<close>
= EName ename
| This
abbreviation VName :: "vname \ lname"
where "VName n == EName (VNam n)"
abbreviation Result :: lname
where "Result == EName Res"
datatype xname \<comment> \<open>names of standard exceptions\<close>
= Throwable
| NullPointer | OutOfMemory | ClassCast
| NegArrSize | IndOutBound | ArrStore
lemma xn_cases:
"xn = Throwable \ xn = NullPointer \
xn = OutOfMemory \<or> xn = ClassCast \<or>
xn = NegArrSize \<or> xn = IndOutBound \<or> xn = ArrStore"
apply (induct xn)
apply auto
done
datatype tname \<comment> \<open>type names for standard classes and other type names\<close>
= Object'
| SXcpt' xname
| TName tnam
record qtname = \<comment> \<open>qualified tname cf. 6.5.3, 6.5.4\<close>
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 \<comment> \<open>package java.lang\<close>
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
¤ Dauer der Verarbeitung: 0.19 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
