author | wenzelm |
Wed, 10 Feb 2010 00:45:16 +0100 | |
changeset 35067 | af4c18c30593 |
parent 32960 | 69916a850301 |
child 35069 | 09154b995ed8 |
permissions | -rw-r--r-- |
12857 | 1 |
(* Title: HOL/Bali/Type.thy |
12854 | 2 |
ID: $Id$ |
3 |
Author: David von Oheimb |
|
4 |
*) |
|
5 |
||
6 |
header {* Java types *} |
|
7 |
||
16417 | 8 |
theory Type imports Name begin |
12854 | 9 |
|
10 |
text {* |
|
11 |
simplifications: |
|
12 |
\begin{itemize} |
|
13 |
\item only the most important primitive types |
|
14 |
\item the null type is regarded as reference type |
|
15 |
\end{itemize} |
|
16 |
*} |
|
17 |
||
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
18 |
datatype prim_ty --{* primitive type, cf. 4.2 *} |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
19 |
= Void --{* result type of void methods *} |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
20 |
| Boolean |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
21 |
| Integer |
12854 | 22 |
|
23 |
||
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
24 |
datatype ref_ty --{* reference type, cf. 4.3 *} |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
25 |
= NullT --{* null type, cf. 4.1 *} |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
26 |
| IfaceT qtname --{* interface type *} |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
27 |
| ClassT qtname --{* class type *} |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
28 |
| ArrayT ty --{* array type *} |
12854 | 29 |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
30 |
and ty --{* any type, cf. 4.1 *} |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
31 |
= PrimT prim_ty --{* primitive type *} |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
32 |
| RefT ref_ty --{* reference type *} |
12854 | 33 |
|
34 |
translations |
|
35 |
"prim_ty" <= (type) "Type.prim_ty" |
|
36 |
"ref_ty" <= (type) "Type.ref_ty" |
|
37 |
"ty" <= (type) "Type.ty" |
|
38 |
||
35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset
|
39 |
abbreviation "NT == RefT NullT" |
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset
|
40 |
abbreviation "Iface I == RefT (IfaceT I)" |
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset
|
41 |
abbreviation "Class C == RefT (ClassT C)" |
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset
|
42 |
abbreviation Array :: "ty \<Rightarrow> ty" ("_.[]" [90] 90) |
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset
|
43 |
where "T.[] == RefT (ArrayT T)" |
12854 | 44 |
|
45 |
constdefs |
|
46 |
the_Class :: "ty \<Rightarrow> qtname" |
|
14766 | 47 |
"the_Class T \<equiv> SOME C. T = Class C" (** primrec not possible here **) |
12854 | 48 |
|
49 |
lemma the_Class_eq [simp]: "the_Class (Class C)= C" |
|
50 |
by (auto simp add: the_Class_def) |
|
51 |
||
52 |
end |