12857

1 
(* Title: HOL/Bali/Name.thy

12854

2 
ID: $Id$


3 
Author: David von Oheimb

12858

4 
License: GPL (GNU GENERAL PUBLIC LICENSE)

12854

5 
*)


6 
header {* Java names *}


7 


8 
theory Name = Basis:


9 


10 
(* cf. 6.5 *)


11 
typedecl tnam (* ordinary type name, i.e. class or interface name *)


12 
typedecl pname (* package name *)


13 
typedecl mname (* method name *)


14 
typedecl vname (* variable or field name *)


15 
typedecl label (* label as destination of break or continue *)


16 


17 
arities


18 
tnam :: "type"


19 
pname :: "type"


20 
vname :: "type"


21 
mname :: "type"


22 
label :: "type"


23 


24 


25 
datatype ename (* expression name *)


26 
= VNam vname


27 
 Res (* special name to model the return value of methods *)


28 


29 
datatype lname (* names for local variables and the This pointer *)


30 
= EName ename


31 
 This


32 
syntax


33 
VName :: "vname \<Rightarrow> lname"


34 
Result :: lname


35 


36 
translations


37 
"VName n" == "EName (VNam n)"


38 
"Result" == "EName Res"


39 


40 
datatype xname (* names of standard exceptions *)


41 
= Throwable


42 
 NullPointer  OutOfMemory  ClassCast


43 
 NegArrSize  IndOutBound  ArrStore


44 


45 
lemma xn_cases:


46 
"xn = Throwable \<or> xn = NullPointer \<or>


47 
xn = OutOfMemory \<or> xn = ClassCast \<or>


48 
xn = NegArrSize \<or> xn = IndOutBound \<or> xn = ArrStore"


49 
apply (induct xn)


50 
apply auto


51 
done


52 


53 
lemma xn_cases_old: (* FIXME cf. Example.thy *)


54 
"ALL xn. xn = Throwable \<or> xn = NullPointer \<or>


55 
xn = OutOfMemory \<or> xn = ClassCast \<or>


56 
xn = NegArrSize \<or> xn = IndOutBound \<or> xn = ArrStore"


57 
apply (rule allI)


58 
apply (induct_tac xn)


59 
apply auto


60 
done


61 


62 
datatype tname (* type names for standard classes and other type names *)


63 
= Object_


64 
 SXcpt_ xname


65 
 TName tnam


66 


67 
record qtname = (* qualified tname cf. 6.5.3, 6.5.4*)


68 
pid :: pname


69 
tid :: tname


70 


71 
axclass has_pname < "type"


72 
consts pname::"'a::has_pname \<Rightarrow> pname"


73 

12859

74 
instance pname::has_pname ..

12854

75 


76 
defs (overloaded)


77 
pname_pname_def: "pname (p::pname) \<equiv> p"


78 


79 
axclass has_tname < "type"


80 
consts tname::"'a::has_tname \<Rightarrow> tname"


81 

12859

82 
instance tname::has_tname ..

12854

83 


84 
defs (overloaded)


85 
tname_tname_def: "tname (t::tname) \<equiv> t"


86 


87 
axclass has_qtname < "type"


88 
consts qtname:: "'a::has_qtname \<Rightarrow> qtname"


89 


90 
(* Declare qtname as instance of has_qtname *)

12859

91 
instance pid_field_type::(has_pname,"type") has_qtname ..

12854

92 


93 
defs (overloaded)


94 
qtname_qtname_def: "qtname (q::qtname) \<equiv> q"


95 


96 
translations


97 
"mname" <= "Name.mname"


98 
"xname" <= "Name.xname"


99 
"tname" <= "Name.tname"


100 
"ename" <= "Name.ename"


101 
"qtname" <= (type) "\<lparr>pid::pname,tid::tname\<rparr>"


102 
(type) "'a qtname_scheme" <= (type) "\<lparr>pid::pname,tid::tname,\<dots>::'a\<rparr>"


103 


104 


105 
consts java_lang::pname (* package java.lang *)


106 


107 
consts


108 
Object :: qtname


109 
SXcpt :: "xname \<Rightarrow> qtname"


110 
defs


111 
Object_def: "Object \<equiv> \<lparr>pid = java_lang, tid = Object_\<rparr>"


112 
SXcpt_def: "SXcpt \<equiv> \<lambda>x. \<lparr>pid = java_lang, tid = SXcpt_ x\<rparr>"


113 


114 
lemma Object_neq_SXcpt [simp]: "Object \<noteq> SXcpt xn"


115 
by (simp add: Object_def SXcpt_def)


116 


117 
lemma SXcpt_inject [simp]: "(SXcpt xn = SXcpt xm) = (xn = xm)"


118 
by (simp add: SXcpt_def)


119 
end


120 
