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 |
|
|
19 |
datatype prim_ty (* primitive type, cf. 4.2 *)
|
|
20 |
= Void (* 'result type' of void methods *)
|
|
21 |
| Boolean
|
|
22 |
| Integer
|
|
23 |
|
|
24 |
|
|
25 |
datatype ref_ty (* reference type, cf. 4.3 *)
|
|
26 |
= NullT (* null type, cf. 4.1 *)
|
|
27 |
| IfaceT qtname (* interface type *)
|
|
28 |
| ClassT qtname (* class type *)
|
|
29 |
| ArrayT ty (* array type *)
|
|
30 |
|
|
31 |
and ty (* any type, cf. 4.1 *)
|
|
32 |
= PrimT prim_ty (* primitive type *)
|
|
33 |
| RefT ref_ty (* reference type *)
|
|
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"
|
|
54 |
"the_Class T \<equiv> \<epsilon>C. T = Class C" (** primrec not possible here **)
|
|
55 |
|
|
56 |
lemma the_Class_eq [simp]: "the_Class (Class C)= C"
|
|
57 |
by (auto simp add: the_Class_def)
|
|
58 |
|
|
59 |
end
|