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