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