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