1(*  Title:      HOL/Bali/Type.thy
2    Author:     David von Oheimb
3*)
4
5subsection \<open>Java types\<close>
6
7theory Type imports Name begin
8
9text \<open>
10simplifications:
11\begin{itemize}
12\item only the most important primitive types
13\item the null type is regarded as reference type
14\end{itemize}
15\<close>
16
17datatype prim_ty        \<comment> \<open>primitive type, cf. 4.2\<close>
18        = Void          \<comment> \<open>result type of void methods\<close>
19        | Boolean
20        | Integer
21
22
23datatype ref_ty         \<comment> \<open>reference type, cf. 4.3\<close>
24        = NullT         \<comment> \<open>null type, cf. 4.1\<close>
25        | IfaceT qtname \<comment> \<open>interface type\<close>
26        | ClassT qtname \<comment> \<open>class type\<close>
27        | ArrayT ty     \<comment> \<open>array type\<close>
28
29and ty                  \<comment> \<open>any type, cf. 4.1\<close>
30        = PrimT prim_ty \<comment> \<open>primitive type\<close>
31        | RefT  ref_ty  \<comment> \<open>reference type\<close>
32
33abbreviation "NT == RefT NullT"
34abbreviation "Iface I == RefT (IfaceT I)"
35abbreviation "Class C == RefT (ClassT C)"
36abbreviation Array :: "ty \<Rightarrow> ty"  ("_.[]" [90] 90)
37  where "T.[] == RefT (ArrayT T)"
38
39definition
40  the_Class :: "ty \<Rightarrow> qtname"
41  where "the_Class T = (SOME C. T = Class C)" (** primrec not possible here **)
42 
43lemma the_Class_eq [simp]: "the_Class (Class C)= C"
44by (auto simp add: the_Class_def)
45
46end
47