src/HOL/Bali/Name.thy
author wenzelm
Sun Aug 28 16:04:44 2005 +0200 (2005-08-28)
changeset 17160 fb65eda72fc7
parent 16417 9bc16273c2d4
child 19726 df95778b4c2f
permissions -rw-r--r--
removed obsolete arities;
     1 (*  Title:      HOL/Bali/Name.thy
     2     ID:         $Id$
     3     Author:     David von Oheimb
     4 *)
     5 header {* Java names *}
     6 
     7 theory Name imports Basis begin
     8 
     9 (* cf. 6.5 *) 
    10 typedecl tnam	--{* ordinary type name, i.e. class or interface name *}
    11 typedecl pname  --{* package name *}
    12 typedecl mname  --{* method name *}
    13 typedecl vname  --{* variable or field name *}
    14 typedecl label  --{* label as destination of break or continue *}
    15 
    16 datatype ename        --{* expression name *} 
    17         = VNam vname 
    18         | Res         --{* special name to model the return value of methods *}
    19 
    20 datatype lname        --{* names for local variables and the This pointer *}
    21         = EName ename 
    22         | This
    23 syntax   
    24   VName  :: "vname \<Rightarrow> lname"
    25   Result :: lname
    26 
    27 translations
    28   "VName n" == "EName (VNam n)"
    29   "Result"  == "EName Res"
    30 
    31 datatype xname		--{* names of standard exceptions *}
    32 	= Throwable
    33 	| NullPointer | OutOfMemory | ClassCast   
    34 	| NegArrSize  | IndOutBound | ArrStore
    35 
    36 lemma xn_cases: 
    37   "xn = Throwable   \<or> xn = NullPointer \<or>  
    38          xn = OutOfMemory \<or> xn = ClassCast \<or> 
    39          xn = NegArrSize  \<or> xn = IndOutBound \<or> xn = ArrStore"
    40 apply (induct xn)
    41 apply auto
    42 done
    43 
    44 
    45 datatype tname	--{* type names for standard classes and other type names *}
    46 	= Object_
    47 	| SXcpt_   xname
    48 	| TName   tnam
    49 
    50 record   qtname = --{* qualified tname cf. 6.5.3, 6.5.4*}
    51           pid :: pname  
    52           tid :: tname
    53 
    54 axclass has_pname < "type"
    55 consts pname::"'a::has_pname \<Rightarrow> pname"
    56 
    57 instance pname::has_pname ..
    58 
    59 defs (overloaded)
    60 pname_pname_def: "pname (p::pname) \<equiv> p"
    61 
    62 axclass has_tname < "type"
    63 consts tname::"'a::has_tname \<Rightarrow> tname"
    64 
    65 instance tname::has_tname ..
    66 
    67 defs (overloaded)
    68 tname_tname_def: "tname (t::tname) \<equiv> t"
    69 
    70 axclass has_qtname < type
    71 consts qtname:: "'a::has_qtname \<Rightarrow> qtname"
    72 
    73 instance qtname_ext_type :: (type) has_qtname ..
    74 
    75 defs (overloaded)
    76 qtname_qtname_def: "qtname (q::qtname) \<equiv> q"
    77 
    78 translations
    79   "mname"  <= "Name.mname"
    80   "xname"  <= "Name.xname"
    81   "tname"  <= "Name.tname"
    82   "ename"  <= "Name.ename"
    83   "qtname" <= (type) "\<lparr>pid::pname,tid::tname\<rparr>"
    84   (type) "'a qtname_scheme" <= (type) "\<lparr>pid::pname,tid::tname,\<dots>::'a\<rparr>"
    85 
    86 
    87 consts java_lang::pname --{* package java.lang *}
    88 
    89 consts 
    90   Object :: qtname
    91   SXcpt  :: "xname \<Rightarrow> qtname"
    92 defs
    93   Object_def: "Object  \<equiv> \<lparr>pid = java_lang, tid = Object_\<rparr>"
    94   SXcpt_def:  "SXcpt   \<equiv> \<lambda>x.  \<lparr>pid = java_lang, tid = SXcpt_ x\<rparr>"
    95 
    96 lemma Object_neq_SXcpt [simp]: "Object \<noteq> SXcpt xn"
    97 by (simp add: Object_def SXcpt_def)
    98 
    99 lemma SXcpt_inject [simp]: "(SXcpt xn = SXcpt xm) = (xn = xm)"
   100 by (simp add: SXcpt_def)
   101 end