author | skalberg |
Thu, 28 Aug 2003 01:56:40 +0200 | |
changeset 14171 | 0cab06e3bbd0 |
parent 13688 | a0b16d42d489 |
child 14766 | c0401da7726d |
permissions | -rw-r--r-- |
12857 | 1 |
(* Title: HOL/Bali/Type.thy |
12854 | 2 |
ID: $Id$ |
3 |
Author: David von Oheimb |
|
12858 | 4 |
License: GPL (GNU GENERAL PUBLIC LICENSE) |
12854 | 5 |
*) |
6 |
||
7 |
header {* Java types *} |
|
8 |
||
9 |
theory Type = Name: |
|
10 |
||
11 |
text {* |
|
12 |
simplifications: |
|
13 |
\begin{itemize} |
|
14 |
\item only the most important primitive types |
|
15 |
\item the null type is regarded as reference type |
|
16 |
\end{itemize} |
|
17 |
*} |
|
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:
12858
diff
changeset
|
19 |
datatype prim_ty --{* primitive type, cf. 4.2 *} |
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:
12858
diff
changeset
|
20 |
= Void --{* result type of void methods *} |
12854 | 21 |
| Boolean |
22 |
| Integer |
|
23 |
||
24 |
||
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:
12858
diff
changeset
|
25 |
datatype ref_ty --{* reference type, cf. 4.3 *} |
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:
12858
diff
changeset
|
26 |
= NullT --{* null type, cf. 4.1 *} |
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:
12858
diff
changeset
|
27 |
| IfaceT qtname --{* interface type *} |
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:
12858
diff
changeset
|
28 |
| ClassT qtname --{* class type *} |
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:
12858
diff
changeset
|
29 |
| ArrayT ty --{* array type *} |
12854 | 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:
12858
diff
changeset
|
31 |
and ty --{* any type, cf. 4.1 *} |
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:
12858
diff
changeset
|
32 |
= PrimT prim_ty --{* primitive type *} |
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:
12858
diff
changeset
|
33 |
| RefT ref_ty --{* reference type *} |
12854 | 34 |
|
35 |
translations |
|
36 |
"prim_ty" <= (type) "Type.prim_ty" |
|
37 |
"ref_ty" <= (type) "Type.ref_ty" |
|
38 |
"ty" <= (type) "Type.ty" |
|
39 |
||
40 |
syntax |
|
41 |
NT :: " \<spacespace> ty" |
|
42 |
Iface :: "qtname \<Rightarrow> ty" |
|
43 |
Class :: "qtname \<Rightarrow> ty" |
|
44 |
Array :: "ty \<Rightarrow> ty" ("_.[]" [90] 90) |
|
45 |
||
46 |
translations |
|
47 |
"NT" == "RefT NullT" |
|
48 |
"Iface I" == "RefT (IfaceT I)" |
|
49 |
"Class C" == "RefT (ClassT C)" |
|
50 |
"T.[]" == "RefT (ArrayT T)" |
|
51 |
||
52 |
constdefs |
|
53 |
the_Class :: "ty \<Rightarrow> qtname" |
|
14171
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
13688
diff
changeset
|
54 |
"the_Class T \<equiv> \<epsilon> C. T = Class C" (** primrec not possible here **) |
12854 | 55 |
|
56 |
lemma the_Class_eq [simp]: "the_Class (Class C)= C" |
|
57 |
by (auto simp add: the_Class_def) |
|
58 |
||
59 |
end |