src/HOL/Bali/Name.thy
author schirmer
Mon Jan 28 17:00:19 2002 +0100 (2002-01-28)
changeset 12854 00d4a435777f
child 12857 a4386cc9b1c3
permissions -rw-r--r--
Isabelle/Bali sources;
     1 (*  Title:      isabelle/Bali/Name.thy
     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