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