src/HOL/Bali/Type.thy
author haftmann
Mon Mar 01 13:40:23 2010 +0100 (2010-03-01)
changeset 35416 d8d7d1b785af
parent 35069 09154b995ed8
child 35431 8758fe1fc9f8
permissions -rw-r--r--
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
wenzelm@12857
     1
(*  Title:      HOL/Bali/Type.thy
schirmer@12854
     2
    Author:     David von Oheimb
schirmer@12854
     3
*)
schirmer@12854
     4
schirmer@12854
     5
header {* Java types *}
schirmer@12854
     6
haftmann@16417
     7
theory Type imports Name begin
schirmer@12854
     8
schirmer@12854
     9
text {*
schirmer@12854
    10
simplifications:
schirmer@12854
    11
\begin{itemize}
schirmer@12854
    12
\item only the most important primitive types
schirmer@12854
    13
\item the null type is regarded as reference type
schirmer@12854
    14
\end{itemize}
schirmer@12854
    15
*}
schirmer@12854
    16
wenzelm@32960
    17
datatype prim_ty        --{* primitive type, cf. 4.2 *}
wenzelm@32960
    18
        = Void          --{* result type of void methods *}
wenzelm@32960
    19
        | Boolean
wenzelm@32960
    20
        | Integer
schirmer@12854
    21
schirmer@12854
    22
wenzelm@32960
    23
datatype ref_ty         --{* reference type, cf. 4.3 *}
wenzelm@32960
    24
        = NullT         --{* null type, cf. 4.1 *}
wenzelm@32960
    25
        | IfaceT qtname --{* interface type *}
wenzelm@32960
    26
        | ClassT qtname --{* class type *}
wenzelm@32960
    27
        | ArrayT ty     --{* array type *}
schirmer@12854
    28
wenzelm@32960
    29
and ty                  --{* any type, cf. 4.1 *}
wenzelm@32960
    30
        = PrimT prim_ty --{* primitive type *}
wenzelm@32960
    31
        | RefT  ref_ty  --{* reference type *}
schirmer@12854
    32
schirmer@12854
    33
translations
schirmer@12854
    34
  "prim_ty" <= (type) "Type.prim_ty"
schirmer@12854
    35
  "ref_ty"  <= (type) "Type.ref_ty"
schirmer@12854
    36
  "ty"      <= (type) "Type.ty"
schirmer@12854
    37
wenzelm@35067
    38
abbreviation "NT == RefT NullT"
wenzelm@35067
    39
abbreviation "Iface I == RefT (IfaceT I)"
wenzelm@35067
    40
abbreviation "Class C == RefT (ClassT C)"
wenzelm@35067
    41
abbreviation Array :: "ty \<Rightarrow> ty"  ("_.[]" [90] 90)
wenzelm@35067
    42
  where "T.[] == RefT (ArrayT T)"
schirmer@12854
    43
haftmann@35416
    44
definition the_Class :: "ty \<Rightarrow> qtname" where
wenzelm@14766
    45
 "the_Class T \<equiv> SOME C. T = Class C" (** primrec not possible here **)
schirmer@12854
    46
 
schirmer@12854
    47
lemma the_Class_eq [simp]: "the_Class (Class C)= C"
schirmer@12854
    48
by (auto simp add: the_Class_def)
schirmer@12854
    49
schirmer@12854
    50
end