src/HOL/Bali/Name.thy
author wenzelm
Mon Jan 28 18:50:23 2002 +0100 (2002-01-28)
changeset 12857 a4386cc9b1c3
parent 12854 00d4a435777f
child 12858 6214f03d6d27
permissions -rw-r--r--
tuned header;
wenzelm@12857
     1
(*  Title:      HOL/Bali/Name.thy
schirmer@12854
     2
    ID:         $Id$
schirmer@12854
     3
    Author:     David von Oheimb
schirmer@12854
     4
    Copyright   1997 Technische Universitaet Muenchen
schirmer@12854
     5
*)
schirmer@12854
     6
header {* Java names *}
schirmer@12854
     7
schirmer@12854
     8
theory Name = Basis:
schirmer@12854
     9
schirmer@12854
    10
(* cf. 6.5 *) 
schirmer@12854
    11
typedecl tnam		(* ordinary type name, i.e. class or interface name *)
schirmer@12854
    12
typedecl pname          (* package name *)
schirmer@12854
    13
typedecl mname		(* method name *)
schirmer@12854
    14
typedecl vname          (* variable or field name *)
schirmer@12854
    15
typedecl label          (* label as destination of break or continue *)
schirmer@12854
    16
schirmer@12854
    17
arities
schirmer@12854
    18
  tnam  :: "type"
schirmer@12854
    19
  pname :: "type"
schirmer@12854
    20
  vname :: "type"
schirmer@12854
    21
  mname :: "type"
schirmer@12854
    22
  label :: "type"
schirmer@12854
    23
schirmer@12854
    24
schirmer@12854
    25
datatype ename        (* expression name *) 
schirmer@12854
    26
        = VNam vname 
schirmer@12854
    27
        | Res         (* special name to model the return value of methods *)
schirmer@12854
    28
schirmer@12854
    29
datatype lname        (* names for local variables and the This pointer *)
schirmer@12854
    30
        = EName ename 
schirmer@12854
    31
        | This
schirmer@12854
    32
syntax   
schirmer@12854
    33
  VName  :: "vname \<Rightarrow> lname"
schirmer@12854
    34
  Result :: lname
schirmer@12854
    35
schirmer@12854
    36
translations
schirmer@12854
    37
  "VName n" == "EName (VNam n)"
schirmer@12854
    38
  "Result"  == "EName Res"
schirmer@12854
    39
schirmer@12854
    40
datatype xname		(* names of standard exceptions *)
schirmer@12854
    41
	= Throwable
schirmer@12854
    42
	| NullPointer | OutOfMemory | ClassCast   
schirmer@12854
    43
	| NegArrSize  | IndOutBound | ArrStore
schirmer@12854
    44
schirmer@12854
    45
lemma xn_cases: 
schirmer@12854
    46
  "xn = Throwable   \<or> xn = NullPointer \<or>  
schirmer@12854
    47
         xn = OutOfMemory \<or> xn = ClassCast \<or> 
schirmer@12854
    48
         xn = NegArrSize  \<or> xn = IndOutBound \<or> xn = ArrStore"
schirmer@12854
    49
apply (induct xn)
schirmer@12854
    50
apply auto
schirmer@12854
    51
done
schirmer@12854
    52
schirmer@12854
    53
lemma xn_cases_old:   (* FIXME cf. Example.thy *)
schirmer@12854
    54
  "ALL xn. xn = Throwable   \<or> xn = NullPointer \<or>  
schirmer@12854
    55
         xn = OutOfMemory \<or> xn = ClassCast \<or> 
schirmer@12854
    56
         xn = NegArrSize  \<or> xn = IndOutBound \<or> xn = ArrStore"
schirmer@12854
    57
apply (rule allI)
schirmer@12854
    58
apply (induct_tac xn)
schirmer@12854
    59
apply auto
schirmer@12854
    60
done
schirmer@12854
    61
schirmer@12854
    62
datatype tname	(* type names for standard classes and other type names *)
schirmer@12854
    63
	= Object_
schirmer@12854
    64
	| SXcpt_   xname
schirmer@12854
    65
	| TName   tnam
schirmer@12854
    66
schirmer@12854
    67
record   qtname = (* qualified tname cf. 6.5.3, 6.5.4*)
schirmer@12854
    68
          pid :: pname 
schirmer@12854
    69
          tid :: tname
schirmer@12854
    70
schirmer@12854
    71
axclass has_pname < "type"
schirmer@12854
    72
consts pname::"'a::has_pname \<Rightarrow> pname"
schirmer@12854
    73
schirmer@12854
    74
instance pname::has_pname
schirmer@12854
    75
by (intro_classes)
schirmer@12854
    76
schirmer@12854
    77
defs (overloaded)
schirmer@12854
    78
pname_pname_def: "pname (p::pname) \<equiv> p"
schirmer@12854
    79
schirmer@12854
    80
axclass has_tname < "type"
schirmer@12854
    81
consts tname::"'a::has_tname \<Rightarrow> tname"
schirmer@12854
    82
schirmer@12854
    83
instance tname::has_tname
schirmer@12854
    84
by (intro_classes)
schirmer@12854
    85
schirmer@12854
    86
defs (overloaded)
schirmer@12854
    87
tname_tname_def: "tname (t::tname) \<equiv> t"
schirmer@12854
    88
schirmer@12854
    89
axclass has_qtname < "type"
schirmer@12854
    90
consts qtname:: "'a::has_qtname \<Rightarrow> qtname"
schirmer@12854
    91
schirmer@12854
    92
(* Declare qtname as instance of has_qtname *)
schirmer@12854
    93
instance pid_field_type::(has_pname,"type") has_qtname
schirmer@12854
    94
by intro_classes 
schirmer@12854
    95
schirmer@12854
    96
defs (overloaded)
schirmer@12854
    97
qtname_qtname_def: "qtname (q::qtname) \<equiv> q"
schirmer@12854
    98
schirmer@12854
    99
translations
schirmer@12854
   100
  "mname"  <= "Name.mname"
schirmer@12854
   101
  "xname"  <= "Name.xname"
schirmer@12854
   102
  "tname"  <= "Name.tname"
schirmer@12854
   103
  "ename"  <= "Name.ename"
schirmer@12854
   104
  "qtname" <= (type) "\<lparr>pid::pname,tid::tname\<rparr>"
schirmer@12854
   105
  (type) "'a qtname_scheme" <= (type) "\<lparr>pid::pname,tid::tname,\<dots>::'a\<rparr>"
schirmer@12854
   106
schirmer@12854
   107
schirmer@12854
   108
consts java_lang::pname (* package java.lang *)
schirmer@12854
   109
schirmer@12854
   110
consts 
schirmer@12854
   111
  Object :: qtname
schirmer@12854
   112
  SXcpt  :: "xname \<Rightarrow> qtname"
schirmer@12854
   113
defs
schirmer@12854
   114
  Object_def: "Object  \<equiv> \<lparr>pid = java_lang, tid = Object_\<rparr>"
schirmer@12854
   115
  SXcpt_def:  "SXcpt   \<equiv> \<lambda>x.  \<lparr>pid = java_lang, tid = SXcpt_ x\<rparr>"
schirmer@12854
   116
schirmer@12854
   117
lemma Object_neq_SXcpt [simp]: "Object \<noteq> SXcpt xn"
schirmer@12854
   118
by (simp add: Object_def SXcpt_def)
schirmer@12854
   119
schirmer@12854
   120
lemma SXcpt_inject [simp]: "(SXcpt xn = SXcpt xm) = (xn = xm)"
schirmer@12854
   121
by (simp add: SXcpt_def)
schirmer@12854
   122
end
schirmer@12854
   123