src/HOL/MicroJava/J/Value.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/J/Value.thy	Fri Jul 14 16:32:51 2000 +0200
@@ -0,0 +1,51 @@
+(*  Title:      HOL/MicroJava/J/Term.thy
+    ID:         $Id$
+    Author:     David von Oheimb
+    Copyright   1999 Technische Universitaet Muenchen
+
+Java values
+*)
+
+Value = Type +
+
+types   loc		(* locations, i.e. abstract references on objects *)
+arities loc :: term
+
+datatype val_		(* name non 'val' because of clash with ML token *)
+	= Unit		(* dummy result value of void methods *)
+	| Null		(* null reference *)
+	| Bool bool	(* Boolean value *)
+	| Intg int	(* integer value *) (* Name Intg instead of Int because
+					       of clash with HOL/Set.thy *)
+	| Addr loc	(* addresses, i.e. locations of objects *)
+types	val = val_
+translations "val" <= (type) "val_"
+
+consts
+  the_Bool	:: "val \\<Rightarrow> bool"
+  the_Intg	:: "val \\<Rightarrow> int"
+  the_Addr	:: "val \\<Rightarrow> loc"
+
+primrec
+ "the_Bool (Bool b) = b"
+
+primrec
+ "the_Intg (Intg i) = i"
+
+primrec
+ "the_Addr (Addr a) = a"
+
+consts
+  defpval	:: "prim_ty \\<Rightarrow> val"	(* default value for primitive types *)
+  default_val	:: "ty \\<Rightarrow> val"		(* default value for all types *)
+
+primrec
+	"defpval Void    = Unit"
+	"defpval Boolean = Bool False"
+	"defpval Integer = Intg (#0)"
+
+primrec
+	"default_val (PrimT pt) = defpval pt"
+	"default_val (RefT  r ) = Null"
+
+end