src/HOL/Bali/Value.thy

1. Function package accepts a parameter (default "some_term"), which specifies the functions
behaviour outside its domain.
2. Bugfix: An exception occured when a function in a mutual definition
was declared but no equation was given.

(*  Title:      HOL/Bali/Value.thy
    ID:         $Id$
    Author:     David von Oheimb
*)
header {* Java values *}



theory Value imports Type begin

typedecl loc            --{* locations, i.e. abstract references on objects *}

datatype val
	= Unit          --{* dummy result value of void methods *}
	| Bool bool     --{* Boolean value *}
	| Intg int      --{* integer value *}
	| Null          --{* null reference *}
	| Addr loc      --{* addresses, i.e. locations of objects *}


translations "val" <= (type) "Term.val"
             "loc" <= (type) "Term.loc"

consts   the_Bool   :: "val \<Rightarrow> bool"  
primrec "the_Bool (Bool b) = b"
consts   the_Intg   :: "val \<Rightarrow> int"
primrec "the_Intg (Intg i) = i"
consts   the_Addr   :: "val \<Rightarrow> loc"
primrec "the_Addr (Addr a) = a"

types	dyn_ty      = "loc \<Rightarrow> ty option"
consts
  typeof        :: "dyn_ty \<Rightarrow> val \<Rightarrow> ty option"
  defpval       :: "prim_ty \<Rightarrow> val"  --{* default value for primitive types *}
  default_val   :: "     ty \<Rightarrow> val"  --{* default value for all types *}

primrec "typeof dt  Unit    = Some (PrimT Void)"
	"typeof dt (Bool b) = Some (PrimT Boolean)"
	"typeof dt (Intg i) = Some (PrimT Integer)"
	"typeof dt  Null    = Some NT"
	"typeof dt (Addr a) = dt a"

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