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