src/HOL/Bali/Type.thy
author kuncar
Fri Dec 09 18:07:04 2011 +0100 (2011-12-09)
changeset 45802 b16f976db515
parent 37956 ee939247b2fb
child 58249 180f1b3508ed
permissions -rw-r--r--
Quotient_Info stores only relation maps
     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