12857

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

12854

2 
ID: $Id$


3 
Author: David von Oheimb


4 
Copyright 1997 Technische Universitaet Muenchen


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 


74 
instance pname::has_pname


75 
by (intro_classes)


76 


77 
defs (overloaded)


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


79 


80 
axclass has_tname < "type"


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


82 


83 
instance tname::has_tname


84 
by (intro_classes)


85 


86 
defs (overloaded)


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


88 


89 
axclass has_qtname < "type"


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


91 


92 
(* Declare qtname as instance of has_qtname *)


93 
instance pid_field_type::(has_pname,"type") has_qtname


94 
by intro_classes


95 


96 
defs (overloaded)


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


98 


99 
translations


100 
"mname" <= "Name.mname"


101 
"xname" <= "Name.xname"


102 
"tname" <= "Name.tname"


103 
"ename" <= "Name.ename"


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


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


106 


107 


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


109 


110 
consts


111 
Object :: qtname


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


113 
defs


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


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


116 


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


118 
by (simp add: Object_def SXcpt_def)


119 


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


121 
by (simp add: SXcpt_def)


122 
end


123 
