src/HOL/Bali/Type.thy
author blanchet
Thu Sep 11 19:32:36 2014 +0200 (2014-09-11)
changeset 58310 91ea607a34d8
parent 58249 180f1b3508ed
child 58887 38db8ddc0f57
permissions -rw-r--r--
updated news
     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
    40   the_Class :: "ty \<Rightarrow> qtname"
    41   where "the_Class T = (SOME C. T = Class C)" (** primrec not possible here **)
    42  
    43 lemma the_Class_eq [simp]: "the_Class (Class C)= C"
    44 by (auto simp add: the_Class_def)
    45 
    46 end