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