author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 38540  8c08631cb4b6 
child 58249  180f1b3508ed 
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 
37956  71 
tname_tname_def: "tname (t::tname) = t" 
35315  72 

73 
instance .. 

12854  74 

35315  75 
end 
12854  76 

35315  77 
definition 
38540
8c08631cb4b6
adjusted to changed naming convention of logical record types
haftmann
parents:
37956
diff
changeset

78 
qtname_qtname_def: "qtname (q::'a qtname_scheme) = q" 
12854  79 

80 
translations 

35431  81 
(type) "qtname" <= (type) "\<lparr>pid::pname,tid::tname\<rparr>" 
12854  82 
(type) "'a qtname_scheme" <= (type) "\<lparr>pid::pname,tid::tname,\<dots>::'a\<rparr>" 
83 

84 

19726  85 
axiomatization java_lang::pname {* package java.lang *} 
12854  86 

37956  87 
definition 
12854  88 
Object :: qtname 
37956  89 
where "Object = \<lparr>pid = java_lang, tid = Object'\<rparr>" 
90 

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

92 
where "SXcpt = (\<lambda>x. \<lparr>pid = java_lang, tid = SXcpt' x\<rparr>)" 

12854  93 

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

95 
by (simp add: Object_def SXcpt_def) 

96 

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

98 
by (simp add: SXcpt_def) 

37956  99 

12854  100 
end 