wenzelm@12857: (*  Title:      HOL/Bali/Name.thy
schirmer@12854:     Author:     David von Oheimb
schirmer@12854: *)
schirmer@12854: header {* Java names *}
schirmer@12854: 
haftmann@16417: theory Name imports Basis begin
schirmer@12854: 
schirmer@12854: (* cf. 6.5 *) 
wenzelm@32960: typedecl tnam   --{* ordinary type name, i.e. class or interface name *}
schirmer@13688: typedecl pname  --{* package name *}
schirmer@13688: typedecl mname  --{* method name *}
schirmer@13688: typedecl vname  --{* variable or field name *}
schirmer@13688: typedecl label  --{* label as destination of break or continue *}
schirmer@12854: 
schirmer@13688: datatype ename        --{* expression name *} 
schirmer@12854:         = VNam vname 
schirmer@13688:         | Res         --{* special name to model the return value of methods *}
schirmer@12854: 
schirmer@13688: datatype lname        --{* names for local variables and the This pointer *}
schirmer@12854:         = EName ename 
schirmer@12854:         | This
wenzelm@35067: abbreviation VName   :: "vname \<Rightarrow> lname"
wenzelm@35067:       where "VName n == EName (VNam n)"
schirmer@12854: 
wenzelm@35067: abbreviation Result :: lname
wenzelm@35067:       where "Result == EName Res"
schirmer@12854: 
wenzelm@32960: datatype xname          --{* names of standard exceptions *}
wenzelm@32960:         = Throwable
wenzelm@32960:         | NullPointer | OutOfMemory | ClassCast   
wenzelm@32960:         | NegArrSize  | IndOutBound | ArrStore
schirmer@12854: 
schirmer@12854: lemma xn_cases: 
schirmer@12854:   "xn = Throwable   \<or> xn = NullPointer \<or>  
schirmer@12854:          xn = OutOfMemory \<or> xn = ClassCast \<or> 
schirmer@12854:          xn = NegArrSize  \<or> xn = IndOutBound \<or> xn = ArrStore"
schirmer@12854: apply (induct xn)
schirmer@12854: apply auto
schirmer@12854: done
schirmer@12854: 
schirmer@12854: 
wenzelm@32960: datatype tname  --{* type names for standard classes and other type names *}
wenzelm@32960:         = Object'
wenzelm@32960:         | SXcpt'   xname
wenzelm@32960:         | TName   tnam
schirmer@12854: 
schirmer@13688: record   qtname = --{* qualified tname cf. 6.5.3, 6.5.4*}
schirmer@13688:           pid :: pname  
schirmer@12854:           tid :: tname
schirmer@12854: 
haftmann@35315: class has_pname =
haftmann@35315:   fixes pname :: "'a \<Rightarrow> pname"
schirmer@12854: 
haftmann@35315: instantiation pname :: has_pname
haftmann@35315: begin
schirmer@12854: 
haftmann@35315: definition
haftmann@35315:   pname_pname_def: "pname (p::pname) \<equiv> p"
schirmer@12854: 
haftmann@35315: instance ..
haftmann@35315: 
haftmann@35315: end
schirmer@12854: 
haftmann@35315: class has_tname =
haftmann@35315:   fixes tname :: "'a \<Rightarrow> tname"
schirmer@12854: 
haftmann@35315: instantiation tname :: has_tname
haftmann@35315: begin
schirmer@12854: 
haftmann@35315: definition
haftmann@35315:   tname_tname_def: "tname (t::tname) \<equiv> t"
haftmann@35315: 
haftmann@35315: instance ..
schirmer@12854: 
haftmann@35315: end
schirmer@12854: 
haftmann@35315: definition
haftmann@35315:   qtname_qtname_def: "qtname (q::'a qtname_ext_type) \<equiv> q"
schirmer@12854: 
schirmer@12854: translations
wenzelm@35431:   (type) "qtname" <= (type) "\<lparr>pid::pname,tid::tname\<rparr>"
schirmer@12854:   (type) "'a qtname_scheme" <= (type) "\<lparr>pid::pname,tid::tname,\<dots>::'a\<rparr>"
schirmer@12854: 
schirmer@12854: 
wenzelm@19726: axiomatization java_lang::pname --{* package java.lang *}
schirmer@12854: 
schirmer@12854: consts 
schirmer@12854:   Object :: qtname
schirmer@12854:   SXcpt  :: "xname \<Rightarrow> qtname"
schirmer@12854: defs
wenzelm@24783:   Object_def: "Object  \<equiv> \<lparr>pid = java_lang, tid = Object'\<rparr>"
wenzelm@24783:   SXcpt_def:  "SXcpt   \<equiv> \<lambda>x.  \<lparr>pid = java_lang, tid = SXcpt' x\<rparr>"
schirmer@12854: 
schirmer@12854: lemma Object_neq_SXcpt [simp]: "Object \<noteq> SXcpt xn"
schirmer@12854: by (simp add: Object_def SXcpt_def)
schirmer@12854: 
schirmer@12854: lemma SXcpt_inject [simp]: "(SXcpt xn = SXcpt xm) = (xn = xm)"
schirmer@12854: by (simp add: SXcpt_def)
schirmer@12854: end