src/HOL/Bali/Name.thy
author schirmer
Thu Oct 31 18:27:10 2002 +0100 (2002-10-31)
changeset 13688 a0b16d42d489
parent 12859 f63315dfffd4
child 14700 2f885b7e5ba7
permissions -rw-r--r--
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
wenzelm@12857
     1
(*  Title:      HOL/Bali/Name.thy
schirmer@12854
     2
    ID:         $Id$
schirmer@12854
     3
    Author:     David von Oheimb
wenzelm@12858
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
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@13688
    11
typedecl tnam	--{* ordinary type name, i.e. class or interface name *}
schirmer@13688
    12
typedecl pname  --{* package name *}
schirmer@13688
    13
typedecl mname  --{* method name *}
schirmer@13688
    14
typedecl vname  --{* variable or field name *}
schirmer@13688
    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@13688
    25
datatype ename        --{* expression name *} 
schirmer@12854
    26
        = VNam vname 
schirmer@13688
    27
        | Res         --{* special name to model the return value of methods *}
schirmer@12854
    28
schirmer@13688
    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@13688
    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
schirmer@13688
    54
datatype tname	--{* type names for standard classes and other type names *}
schirmer@12854
    55
	= Object_
schirmer@12854
    56
	| SXcpt_   xname
schirmer@12854
    57
	| TName   tnam
schirmer@12854
    58
schirmer@13688
    59
record   qtname = --{* qualified tname cf. 6.5.3, 6.5.4*}
schirmer@13688
    60
          pid :: pname  
schirmer@12854
    61
          tid :: tname
schirmer@12854
    62
schirmer@12854
    63
axclass has_pname < "type"
schirmer@12854
    64
consts pname::"'a::has_pname \<Rightarrow> pname"
schirmer@12854
    65
wenzelm@12859
    66
instance pname::has_pname ..
schirmer@12854
    67
schirmer@12854
    68
defs (overloaded)
schirmer@12854
    69
pname_pname_def: "pname (p::pname) \<equiv> p"
schirmer@12854
    70
schirmer@12854
    71
axclass has_tname < "type"
schirmer@12854
    72
consts tname::"'a::has_tname \<Rightarrow> tname"
schirmer@12854
    73
wenzelm@12859
    74
instance tname::has_tname ..
schirmer@12854
    75
schirmer@12854
    76
defs (overloaded)
schirmer@12854
    77
tname_tname_def: "tname (t::tname) \<equiv> t"
schirmer@12854
    78
schirmer@12854
    79
axclass has_qtname < "type"
schirmer@12854
    80
consts qtname:: "'a::has_qtname \<Rightarrow> qtname"
schirmer@12854
    81
schirmer@12854
    82
(* Declare qtname as instance of has_qtname *)
wenzelm@12859
    83
instance pid_field_type::(has_pname,"type") has_qtname ..
schirmer@12854
    84
schirmer@12854
    85
defs (overloaded)
schirmer@12854
    86
qtname_qtname_def: "qtname (q::qtname) \<equiv> q"
schirmer@12854
    87
schirmer@12854
    88
translations
schirmer@12854
    89
  "mname"  <= "Name.mname"
schirmer@12854
    90
  "xname"  <= "Name.xname"
schirmer@12854
    91
  "tname"  <= "Name.tname"
schirmer@12854
    92
  "ename"  <= "Name.ename"
schirmer@12854
    93
  "qtname" <= (type) "\<lparr>pid::pname,tid::tname\<rparr>"
schirmer@12854
    94
  (type) "'a qtname_scheme" <= (type) "\<lparr>pid::pname,tid::tname,\<dots>::'a\<rparr>"
schirmer@12854
    95
schirmer@12854
    96
schirmer@13688
    97
consts java_lang::pname --{* package java.lang *}
schirmer@12854
    98
schirmer@12854
    99
consts 
schirmer@12854
   100
  Object :: qtname
schirmer@12854
   101
  SXcpt  :: "xname \<Rightarrow> qtname"
schirmer@12854
   102
defs
schirmer@12854
   103
  Object_def: "Object  \<equiv> \<lparr>pid = java_lang, tid = Object_\<rparr>"
schirmer@12854
   104
  SXcpt_def:  "SXcpt   \<equiv> \<lambda>x.  \<lparr>pid = java_lang, tid = SXcpt_ x\<rparr>"
schirmer@12854
   105
schirmer@12854
   106
lemma Object_neq_SXcpt [simp]: "Object \<noteq> SXcpt xn"
schirmer@12854
   107
by (simp add: Object_def SXcpt_def)
schirmer@12854
   108
schirmer@12854
   109
lemma SXcpt_inject [simp]: "(SXcpt xn = SXcpt xm) = (xn = xm)"
schirmer@12854
   110
by (simp add: SXcpt_def)
schirmer@12854
   111
end
schirmer@12854
   112