src/HOL/Bali/Type.thy
author skalberg
Thu Aug 28 01:56:40 2003 +0200 (2003-08-28)
changeset 14171 0cab06e3bbd0
parent 13688 a0b16d42d489
child 14766 c0401da7726d
permissions -rw-r--r--
Extended the notion of letter and digit, such that now one may use greek,
gothic, euler, or calligraphic letters as normal letters.
wenzelm@12857
     1
(*  Title:      HOL/Bali/Type.thy
schirmer@12854
     2
    ID:         $Id$
schirmer@12854
     3
    Author:     David von Oheimb
wenzelm@12858
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
schirmer@12854
     5
*)
schirmer@12854
     6
schirmer@12854
     7
header {* Java types *}
schirmer@12854
     8
schirmer@12854
     9
theory Type = Name:
schirmer@12854
    10
schirmer@12854
    11
text {*
schirmer@12854
    12
simplifications:
schirmer@12854
    13
\begin{itemize}
schirmer@12854
    14
\item only the most important primitive types
schirmer@12854
    15
\item the null type is regarded as reference type
schirmer@12854
    16
\end{itemize}
schirmer@12854
    17
*}
schirmer@12854
    18
schirmer@13688
    19
datatype prim_ty       	--{* primitive type, cf. 4.2 *}
schirmer@13688
    20
	= Void    	--{* result type of void methods *}
schirmer@12854
    21
	| Boolean
schirmer@12854
    22
	| Integer
schirmer@12854
    23
schirmer@12854
    24
schirmer@13688
    25
datatype ref_ty		--{* reference type, cf. 4.3 *}
schirmer@13688
    26
	= NullT		--{* null type, cf. 4.1 *}
schirmer@13688
    27
	| IfaceT qtname	--{* interface type *}
schirmer@13688
    28
	| ClassT qtname	--{* class type *}
schirmer@13688
    29
	| ArrayT ty	--{* array type *}
schirmer@12854
    30
schirmer@13688
    31
and ty	    		--{* any type, cf. 4.1 *}
schirmer@13688
    32
	= PrimT prim_ty	--{* primitive type *}
schirmer@13688
    33
	| RefT  ref_ty	--{* reference type *}
schirmer@12854
    34
schirmer@12854
    35
translations
schirmer@12854
    36
  "prim_ty" <= (type) "Type.prim_ty"
schirmer@12854
    37
  "ref_ty"  <= (type) "Type.ref_ty"
schirmer@12854
    38
  "ty"      <= (type) "Type.ty"
schirmer@12854
    39
schirmer@12854
    40
syntax
schirmer@12854
    41
	 NT	:: "       \<spacespace> ty"
schirmer@12854
    42
	 Iface	:: "qtname  \<Rightarrow> ty"
schirmer@12854
    43
	 Class	:: "qtname  \<Rightarrow> ty"
schirmer@12854
    44
	 Array	:: "ty     \<Rightarrow> ty"	("_.[]" [90] 90)
schirmer@12854
    45
schirmer@12854
    46
translations
schirmer@12854
    47
	"NT"      == "RefT   NullT"
schirmer@12854
    48
	"Iface I" == "RefT (IfaceT I)"
schirmer@12854
    49
	"Class C" == "RefT (ClassT C)"
schirmer@12854
    50
	"T.[]"    == "RefT (ArrayT T)"
schirmer@12854
    51
schirmer@12854
    52
constdefs
schirmer@12854
    53
  the_Class :: "ty \<Rightarrow> qtname"
skalberg@14171
    54
 "the_Class T \<equiv> \<epsilon> C. T = Class C" (** primrec not possible here **)
schirmer@12854
    55
 
schirmer@12854
    56
lemma the_Class_eq [simp]: "the_Class (Class C)= C"
schirmer@12854
    57
by (auto simp add: the_Class_def)
schirmer@12854
    58
schirmer@12854
    59
end