src/HOL/Bali/Type.thy

clarified treatment of properties;
tuned messages;

(*  Title:      HOL/Bali/Type.thy
    Author:     David von Oheimb
*)

subsection \<open>Java types\<close>

theory Type imports Name begin

text \<open>
simplifications:
\begin{itemize}
\item only the most important primitive types
\item the null type is regarded as reference type
\end{itemize}
\<close>

datatype prim_ty        \<comment>\<open>primitive type, cf. 4.2\<close>
        = Void          \<comment>\<open>result type of void methods\<close>
        | Boolean
        | Integer


datatype ref_ty         \<comment>\<open>reference type, cf. 4.3\<close>
        = NullT         \<comment>\<open>null type, cf. 4.1\<close>
        | IfaceT qtname \<comment>\<open>interface type\<close>
        | ClassT qtname \<comment>\<open>class type\<close>
        | ArrayT ty     \<comment>\<open>array type\<close>

and ty                  \<comment>\<open>any type, cf. 4.1\<close>
        = PrimT prim_ty \<comment>\<open>primitive type\<close>
        | RefT  ref_ty  \<comment>\<open>reference type\<close>

abbreviation "NT == RefT NullT"
abbreviation "Iface I == RefT (IfaceT I)"
abbreviation "Class C == RefT (ClassT C)"
abbreviation Array :: "ty \<Rightarrow> ty"  ("_.[]" [90] 90)
  where "T.[] == RefT (ArrayT T)"

definition
  the_Class :: "ty \<Rightarrow> qtname"
  where "the_Class T = (SOME C. T = Class C)" (** primrec not possible here **)
 
lemma the_Class_eq [simp]: "the_Class (Class C)= C"
by (auto simp add: the_Class_def)

end