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