author  wenzelm 
Sun, 30 Sep 2007 21:55:15 +0200  
changeset 24783  5a3e336a2e37 
parent 19726  df95778b4c2f 
child 32960  69916a850301 
permissions  rwrr 
12857  1 
(* Title: HOL/Bali/Name.thy 
12854  2 
ID: $Id$ 
3 
Author: David von Oheimb 

4 
*) 

5 
header {* Java names *} 

6 

16417  7 
theory Name imports Basis begin 
12854  8 

9 
(* cf. 6.5 *) 

13688
a0b16d42d489
"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.
schirmer
parents:
12859
diff
changeset

10 
typedecl tnam {* ordinary type name, i.e. class or interface name *} 
a0b16d42d489
"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.
schirmer
parents:
12859
diff
changeset

11 
typedecl pname {* package name *} 
a0b16d42d489
"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.
schirmer
parents:
12859
diff
changeset

12 
typedecl mname {* method name *} 
a0b16d42d489
"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.
schirmer
parents:
12859
diff
changeset

13 
typedecl vname {* variable or field name *} 
a0b16d42d489
"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.
schirmer
parents:
12859
diff
changeset

14 
typedecl label {* label as destination of break or continue *} 
12854  15 

13688
a0b16d42d489
"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.
schirmer
parents:
12859
diff
changeset

16 
datatype ename {* expression name *} 
12854  17 
= VNam vname 
13688
a0b16d42d489
"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.
schirmer
parents:
12859
diff
changeset

18 
 Res {* special name to model the return value of methods *} 
12854  19 

13688
a0b16d42d489
"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.
schirmer
parents:
12859
diff
changeset

20 
datatype lname {* names for local variables and the This pointer *} 
12854  21 
= EName ename 
22 
 This 

23 
syntax 

24 
VName :: "vname \<Rightarrow> lname" 

25 
Result :: lname 

26 

27 
translations 

28 
"VName n" == "EName (VNam n)" 

29 
"Result" == "EName Res" 

30 

13688
a0b16d42d489
"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.
schirmer
parents:
12859
diff
changeset

31 
datatype xname {* names of standard exceptions *} 
12854  32 
= Throwable 
33 
 NullPointer  OutOfMemory  ClassCast 

34 
 NegArrSize  IndOutBound  ArrStore 

35 

36 
lemma xn_cases: 

37 
"xn = Throwable \<or> xn = NullPointer \<or> 

38 
xn = OutOfMemory \<or> xn = ClassCast \<or> 

39 
xn = NegArrSize \<or> xn = IndOutBound \<or> xn = ArrStore" 

40 
apply (induct xn) 

41 
apply auto 

42 
done 

43 

44 

13688
a0b16d42d489
"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.
schirmer
parents:
12859
diff
changeset

45 
datatype tname {* type names for standard classes and other type names *} 
24783  46 
= Object' 
47 
 SXcpt' xname 

12854  48 
 TName tnam 
49 

13688
a0b16d42d489
"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.
schirmer
parents:
12859
diff
changeset

50 
record qtname = {* qualified tname cf. 6.5.3, 6.5.4*} 
a0b16d42d489
"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.
schirmer
parents:
12859
diff
changeset

51 
pid :: pname 
12854  52 
tid :: tname 
53 

54 
axclass has_pname < "type" 

55 
consts pname::"'a::has_pname \<Rightarrow> pname" 

56 

12859  57 
instance pname::has_pname .. 
12854  58 

59 
defs (overloaded) 

60 
pname_pname_def: "pname (p::pname) \<equiv> p" 

61 

62 
axclass has_tname < "type" 

63 
consts tname::"'a::has_tname \<Rightarrow> tname" 

64 

12859  65 
instance tname::has_tname .. 
12854  66 

67 
defs (overloaded) 

68 
tname_tname_def: "tname (t::tname) \<equiv> t" 

69 

17160  70 
axclass has_qtname < type 
12854  71 
consts qtname:: "'a::has_qtname \<Rightarrow> qtname" 
72 

17160  73 
instance qtname_ext_type :: (type) has_qtname .. 
12854  74 

75 
defs (overloaded) 

76 
qtname_qtname_def: "qtname (q::qtname) \<equiv> q" 

77 

78 
translations 

79 
"mname" <= "Name.mname" 

80 
"xname" <= "Name.xname" 

81 
"tname" <= "Name.tname" 

82 
"ename" <= "Name.ename" 

83 
"qtname" <= (type) "\<lparr>pid::pname,tid::tname\<rparr>" 

84 
(type) "'a qtname_scheme" <= (type) "\<lparr>pid::pname,tid::tname,\<dots>::'a\<rparr>" 

85 

86 

19726  87 
axiomatization java_lang::pname {* package java.lang *} 
12854  88 

89 
consts 

90 
Object :: qtname 

91 
SXcpt :: "xname \<Rightarrow> qtname" 

92 
defs 

24783  93 
Object_def: "Object \<equiv> \<lparr>pid = java_lang, tid = Object'\<rparr>" 
94 
SXcpt_def: "SXcpt \<equiv> \<lambda>x. \<lparr>pid = java_lang, tid = SXcpt' x\<rparr>" 

12854  95 

96 
lemma Object_neq_SXcpt [simp]: "Object \<noteq> SXcpt xn" 

97 
by (simp add: Object_def SXcpt_def) 

98 

99 
lemma SXcpt_inject [simp]: "(SXcpt xn = SXcpt xm) = (xn = xm)" 

100 
by (simp add: SXcpt_def) 

101 
end 