author | kleing |
Mon, 21 Jun 2004 10:25:57 +0200 | |
changeset 14981 | e73f8140af78 |
parent 14700 | 2f885b7e5ba7 |
child 16417 | 9bc16273c2d4 |
permissions | -rw-r--r-- |
12857 | 1 |
(* Title: HOL/Bali/Name.thy |
12854 | 2 |
ID: $Id$ |
3 |
Author: David von Oheimb |
|
4 |
*) |
|
5 |
header {* Java names *} |
|
6 |
||
7 |
theory Name = Basis: |
|
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 |
|
16 |
arities |
|
17 |
tnam :: "type" |
|
18 |
pname :: "type" |
|
19 |
vname :: "type" |
|
20 |
mname :: "type" |
|
21 |
label :: "type" |
|
22 |
||
23 |
||
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
|
24 |
datatype ename --{* expression name *} |
12854 | 25 |
= 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
|
26 |
| Res --{* special name to model the return value of methods *} |
12854 | 27 |
|
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
|
28 |
datatype lname --{* names for local variables and the This pointer *} |
12854 | 29 |
= EName ename |
30 |
| This |
|
31 |
syntax |
|
32 |
VName :: "vname \<Rightarrow> lname" |
|
33 |
Result :: lname |
|
34 |
||
35 |
translations |
|
36 |
"VName n" == "EName (VNam n)" |
|
37 |
"Result" == "EName Res" |
|
38 |
||
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
|
39 |
datatype xname --{* names of standard exceptions *} |
12854 | 40 |
= Throwable |
41 |
| NullPointer | OutOfMemory | ClassCast |
|
42 |
| NegArrSize | IndOutBound | ArrStore |
|
43 |
||
44 |
lemma xn_cases: |
|
45 |
"xn = Throwable \<or> xn = NullPointer \<or> |
|
46 |
xn = OutOfMemory \<or> xn = ClassCast \<or> |
|
47 |
xn = NegArrSize \<or> xn = IndOutBound \<or> xn = ArrStore" |
|
48 |
apply (induct xn) |
|
49 |
apply auto |
|
50 |
done |
|
51 |
||
52 |
||
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
|
53 |
datatype tname --{* type names for standard classes and other type names *} |
12854 | 54 |
= Object_ |
55 |
| SXcpt_ xname |
|
56 |
| TName tnam |
|
57 |
||
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
|
58 |
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
|
59 |
pid :: pname |
12854 | 60 |
tid :: tname |
61 |
||
62 |
axclass has_pname < "type" |
|
63 |
consts pname::"'a::has_pname \<Rightarrow> pname" |
|
64 |
||
12859 | 65 |
instance pname::has_pname .. |
12854 | 66 |
|
67 |
defs (overloaded) |
|
68 |
pname_pname_def: "pname (p::pname) \<equiv> p" |
|
69 |
||
70 |
axclass has_tname < "type" |
|
71 |
consts tname::"'a::has_tname \<Rightarrow> tname" |
|
72 |
||
12859 | 73 |
instance tname::has_tname .. |
12854 | 74 |
|
75 |
defs (overloaded) |
|
76 |
tname_tname_def: "tname (t::tname) \<equiv> t" |
|
77 |
||
78 |
axclass has_qtname < "type" |
|
79 |
consts qtname:: "'a::has_qtname \<Rightarrow> qtname" |
|
80 |
||
81 |
(* Declare qtname as instance of has_qtname *) |
|
14700
2f885b7e5ba7
reimplementation of HOL records; only one type is created for
schirmer
parents:
13688
diff
changeset
|
82 |
instance qtname_ext_type::("type") has_qtname .. |
12854 | 83 |
|
84 |
defs (overloaded) |
|
85 |
qtname_qtname_def: "qtname (q::qtname) \<equiv> q" |
|
86 |
||
87 |
translations |
|
88 |
"mname" <= "Name.mname" |
|
89 |
"xname" <= "Name.xname" |
|
90 |
"tname" <= "Name.tname" |
|
91 |
"ename" <= "Name.ename" |
|
92 |
"qtname" <= (type) "\<lparr>pid::pname,tid::tname\<rparr>" |
|
93 |
(type) "'a qtname_scheme" <= (type) "\<lparr>pid::pname,tid::tname,\<dots>::'a\<rparr>" |
|
94 |
||
95 |
||
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
|
96 |
consts java_lang::pname --{* package java.lang *} |
12854 | 97 |
|
98 |
consts |
|
99 |
Object :: qtname |
|
100 |
SXcpt :: "xname \<Rightarrow> qtname" |
|
101 |
defs |
|
102 |
Object_def: "Object \<equiv> \<lparr>pid = java_lang, tid = Object_\<rparr>" |
|
103 |
SXcpt_def: "SXcpt \<equiv> \<lambda>x. \<lparr>pid = java_lang, tid = SXcpt_ x\<rparr>" |
|
104 |
||
105 |
lemma Object_neq_SXcpt [simp]: "Object \<noteq> SXcpt xn" |
|
106 |
by (simp add: Object_def SXcpt_def) |
|
107 |
||
108 |
lemma SXcpt_inject [simp]: "(SXcpt xn = SXcpt xm) = (xn = xm)" |
|
109 |
by (simp add: SXcpt_def) |
|
110 |
end |
|
111 |