author | wenzelm |
Wed, 11 Nov 2009 14:15:11 +0100 | |
changeset 33615 | 261abc2e3155 |
parent 32960 | 69916a850301 |
child 35067 | af4c18c30593 |
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 |
||
39 |
syntax |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
40 |
NT :: " \<spacespace> ty" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
41 |
Iface :: "qtname \<Rightarrow> ty" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
42 |
Class :: "qtname \<Rightarrow> ty" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
43 |
Array :: "ty \<Rightarrow> ty" ("_.[]" [90] 90) |
12854 | 44 |
|
45 |
translations |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
46 |
"NT" == "RefT NullT" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
47 |
"Iface I" == "RefT (IfaceT I)" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
48 |
"Class C" == "RefT (ClassT C)" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
49 |
"T.[]" == "RefT (ArrayT T)" |
12854 | 50 |
|
51 |
constdefs |
|
52 |
the_Class :: "ty \<Rightarrow> qtname" |
|
14766 | 53 |
"the_Class T \<equiv> SOME C. T = Class C" (** primrec not possible here **) |
12854 | 54 |
|
55 |
lemma the_Class_eq [simp]: "the_Class (Class C)= C" |
|
56 |
by (auto simp add: the_Class_def) |
|
57 |
||
58 |
end |