src/HOL/Bali/Type.thy
author wenzelm
Sat Oct 17 14:43:18 2009 +0200 (2009-10-17)
changeset 32960 69916a850301
parent 16417 9bc16273c2d4
child 35067 af4c18c30593
permissions -rw-r--r--
eliminated hard tabulators, guessing at each author's individual tab-width;
tuned headers;
wenzelm@12857
     1
(*  Title:      HOL/Bali/Type.thy
schirmer@12854
     2
    ID:         $Id$
schirmer@12854
     3
    Author:     David von Oheimb
schirmer@12854
     4
*)
schirmer@12854
     5
schirmer@12854
     6
header {* Java types *}
schirmer@12854
     7
haftmann@16417
     8
theory Type imports Name begin
schirmer@12854
     9
schirmer@12854
    10
text {*
schirmer@12854
    11
simplifications:
schirmer@12854
    12
\begin{itemize}
schirmer@12854
    13
\item only the most important primitive types
schirmer@12854
    14
\item the null type is regarded as reference type
schirmer@12854
    15
\end{itemize}
schirmer@12854
    16
*}
schirmer@12854
    17
wenzelm@32960
    18
datatype prim_ty        --{* primitive type, cf. 4.2 *}
wenzelm@32960
    19
        = Void          --{* result type of void methods *}
wenzelm@32960
    20
        | Boolean
wenzelm@32960
    21
        | Integer
schirmer@12854
    22
schirmer@12854
    23
wenzelm@32960
    24
datatype ref_ty         --{* reference type, cf. 4.3 *}
wenzelm@32960
    25
        = NullT         --{* null type, cf. 4.1 *}
wenzelm@32960
    26
        | IfaceT qtname --{* interface type *}
wenzelm@32960
    27
        | ClassT qtname --{* class type *}
wenzelm@32960
    28
        | ArrayT ty     --{* array type *}
schirmer@12854
    29
wenzelm@32960
    30
and ty                  --{* any type, cf. 4.1 *}
wenzelm@32960
    31
        = PrimT prim_ty --{* primitive type *}
wenzelm@32960
    32
        | RefT  ref_ty  --{* reference type *}
schirmer@12854
    33
schirmer@12854
    34
translations
schirmer@12854
    35
  "prim_ty" <= (type) "Type.prim_ty"
schirmer@12854
    36
  "ref_ty"  <= (type) "Type.ref_ty"
schirmer@12854
    37
  "ty"      <= (type) "Type.ty"
schirmer@12854
    38
schirmer@12854
    39
syntax
wenzelm@32960
    40
         NT     :: "       \<spacespace> ty"
wenzelm@32960
    41
         Iface  :: "qtname  \<Rightarrow> ty"
wenzelm@32960
    42
         Class  :: "qtname  \<Rightarrow> ty"
wenzelm@32960
    43
         Array  :: "ty     \<Rightarrow> ty"    ("_.[]" [90] 90)
schirmer@12854
    44
schirmer@12854
    45
translations
wenzelm@32960
    46
        "NT"      == "RefT   NullT"
wenzelm@32960
    47
        "Iface I" == "RefT (IfaceT I)"
wenzelm@32960
    48
        "Class C" == "RefT (ClassT C)"
wenzelm@32960
    49
        "T.[]"    == "RefT (ArrayT T)"
schirmer@12854
    50
schirmer@12854
    51
constdefs
schirmer@12854
    52
  the_Class :: "ty \<Rightarrow> qtname"
wenzelm@14766
    53
 "the_Class T \<equiv> SOME C. T = Class C" (** primrec not possible here **)
schirmer@12854
    54
 
schirmer@12854
    55
lemma the_Class_eq [simp]: "the_Class (Class C)= C"
schirmer@12854
    56
by (auto simp add: the_Class_def)
schirmer@12854
    57
schirmer@12854
    58
end