src/HOL/Bali/Type.thy
author skalberg
Thu, 28 Aug 2003 01:56:40 +0200
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.

(*  Title:      HOL/Bali/Type.thy
    ID:         $Id$
    Author:     David von Oheimb
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
*)

header {* Java types *}

theory Type = Name:

text {*
simplifications:
\begin{itemize}
\item only the most important primitive types
\item the null type is regarded as reference type
\end{itemize}
*}

datatype prim_ty       	--{* primitive type, cf. 4.2 *}
	= Void    	--{* result type of void methods *}
	| Boolean
	| Integer


datatype ref_ty		--{* reference type, cf. 4.3 *}
	= NullT		--{* null type, cf. 4.1 *}
	| IfaceT qtname	--{* interface type *}
	| ClassT qtname	--{* class type *}
	| ArrayT ty	--{* array type *}

and ty	    		--{* any type, cf. 4.1 *}
	= PrimT prim_ty	--{* primitive type *}
	| RefT  ref_ty	--{* reference type *}

translations
  "prim_ty" <= (type) "Type.prim_ty"
  "ref_ty"  <= (type) "Type.ref_ty"
  "ty"      <= (type) "Type.ty"

syntax
	 NT	:: "       \<spacespace> ty"
	 Iface	:: "qtname  \<Rightarrow> ty"
	 Class	:: "qtname  \<Rightarrow> ty"
	 Array	:: "ty     \<Rightarrow> ty"	("_.[]" [90] 90)

translations
	"NT"      == "RefT   NullT"
	"Iface I" == "RefT (IfaceT I)"
	"Class C" == "RefT (ClassT C)"
	"T.[]"    == "RefT (ArrayT T)"

constdefs
  the_Class :: "ty \<Rightarrow> qtname"
 "the_Class T \<equiv> \<epsilon> C. T = Class C" (** primrec not possible here **)
 
lemma the_Class_eq [simp]: "the_Class (Class C)= C"
by (auto simp add: the_Class_def)

end