author  haftmann 
Tue, 23 Feb 2010 10:11:12 +0100  
changeset 35315  fbdc860d87a3 
parent 35069  09154b995ed8 
child 35431  8758fe1fc9f8 
permissions  rwrr 
12857  1 
(* Title: HOL/Bali/Name.thy 
12854  2 
Author: David von Oheimb 
3 
*) 

4 
header {* Java names *} 

5 

16417  6 
theory Name imports Basis begin 
12854  7 

8 
(* cf. 6.5 *) 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24783
diff
changeset

9 
typedecl tnam {* ordinary type name, i.e. class or interface name *} 
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 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

11 
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

12 
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

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

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

15 
datatype ename {* expression name *} 
12854  16 
= 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

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

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

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

35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

22 
abbreviation VName :: "vname \<Rightarrow> lname" 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

23 
where "VName n == EName (VNam n)" 
12854  24 

35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

25 
abbreviation Result :: lname 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

26 
where "Result == EName Res" 
12854  27 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24783
diff
changeset

28 
datatype xname {* names of standard exceptions *} 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24783
diff
changeset

29 
= Throwable 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24783
diff
changeset

30 
 NullPointer  OutOfMemory  ClassCast 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24783
diff
changeset

31 
 NegArrSize  IndOutBound  ArrStore 
12854  32 

33 
lemma xn_cases: 

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

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

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

37 
apply (induct xn) 

38 
apply auto 

39 
done 

40 

41 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24783
diff
changeset

42 
datatype tname {* type names for standard classes and other type names *} 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24783
diff
changeset

43 
= Object' 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24783
diff
changeset

44 
 SXcpt' xname 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24783
diff
changeset

45 
 TName tnam 
12854  46 

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

47 
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

48 
pid :: pname 
12854  49 
tid :: tname 
50 

35315  51 
class has_pname = 
52 
fixes pname :: "'a \<Rightarrow> pname" 

12854  53 

35315  54 
instantiation pname :: has_pname 
55 
begin 

12854  56 

35315  57 
definition 
58 
pname_pname_def: "pname (p::pname) \<equiv> p" 

12854  59 

35315  60 
instance .. 
61 

62 
end 

12854  63 

35315  64 
class has_tname = 
65 
fixes tname :: "'a \<Rightarrow> tname" 

12854  66 

35315  67 
instantiation tname :: has_tname 
68 
begin 

12854  69 

35315  70 
definition 
71 
tname_tname_def: "tname (t::tname) \<equiv> t" 

72 

73 
instance .. 

12854  74 

35315  75 
end 
12854  76 

35315  77 
definition 
78 
qtname_qtname_def: "qtname (q::'a qtname_ext_type) \<equiv> q" 

12854  79 

80 
translations 

81 
"mname" <= "Name.mname" 

82 
"xname" <= "Name.xname" 

83 
"tname" <= "Name.tname" 

84 
"ename" <= "Name.ename" 

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

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

87 

88 

19726  89 
axiomatization java_lang::pname {* package java.lang *} 
12854  90 

91 
consts 

92 
Object :: qtname 

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

94 
defs 

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

12854  97 

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

99 
by (simp add: Object_def SXcpt_def) 

100 

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

102 
by (simp add: SXcpt_def) 

103 
end 