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