| author | wenzelm |
| Fri, 21 May 2004 21:14:52 +0200 | |
| changeset 14766 | c0401da7726d |
| parent 14171 | 0cab06e3bbd0 |
| child 14981 | e73f8140af78 |
| 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" |
|
| 14766 | 54 |
"the_Class T \<equiv> SOME 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 |