wenzelm@12857: (*  Title:      HOL/Bali/Type.thy
schirmer@12854:     Author:     David von Oheimb
schirmer@12854: *)
schirmer@12854: 
schirmer@12854: header {* Java types *}
schirmer@12854: 
haftmann@16417: theory Type imports Name begin
schirmer@12854: 
schirmer@12854: text {*
schirmer@12854: simplifications:
schirmer@12854: \begin{itemize}
schirmer@12854: \item only the most important primitive types
schirmer@12854: \item the null type is regarded as reference type
schirmer@12854: \end{itemize}
schirmer@12854: *}
schirmer@12854: 
wenzelm@32960: datatype prim_ty        --{* primitive type, cf. 4.2 *}
wenzelm@32960:         = Void          --{* result type of void methods *}
wenzelm@32960:         | Boolean
wenzelm@32960:         | Integer
schirmer@12854: 
schirmer@12854: 
wenzelm@32960: datatype ref_ty         --{* reference type, cf. 4.3 *}
wenzelm@32960:         = NullT         --{* null type, cf. 4.1 *}
wenzelm@32960:         | IfaceT qtname --{* interface type *}
wenzelm@32960:         | ClassT qtname --{* class type *}
wenzelm@32960:         | ArrayT ty     --{* array type *}
schirmer@12854: 
wenzelm@32960: and ty                  --{* any type, cf. 4.1 *}
wenzelm@32960:         = PrimT prim_ty --{* primitive type *}
wenzelm@32960:         | RefT  ref_ty  --{* reference type *}
schirmer@12854: 
schirmer@12854: translations
schirmer@12854:   "prim_ty" <= (type) "Type.prim_ty"
schirmer@12854:   "ref_ty"  <= (type) "Type.ref_ty"
schirmer@12854:   "ty"      <= (type) "Type.ty"
schirmer@12854: 
wenzelm@35067: abbreviation "NT == RefT NullT"
wenzelm@35067: abbreviation "Iface I == RefT (IfaceT I)"
wenzelm@35067: abbreviation "Class C == RefT (ClassT C)"
wenzelm@35067: abbreviation Array :: "ty \<Rightarrow> ty"  ("_.[]" [90] 90)
wenzelm@35067:   where "T.[] == RefT (ArrayT T)"
schirmer@12854: 
haftmann@35416: definition the_Class :: "ty \<Rightarrow> qtname" where
wenzelm@14766:  "the_Class T \<equiv> SOME C. T = Class C" (** primrec not possible here **)
schirmer@12854:  
schirmer@12854: lemma the_Class_eq [simp]: "the_Class (Class C)= C"
schirmer@12854: by (auto simp add: the_Class_def)
schirmer@12854: 
schirmer@12854: end