(* Title: HOL/Bali/Value.thy 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 *} consts the_Bool :: "val \ bool" primrec "the_Bool (Bool b) = b" consts the_Intg :: "val \ int" primrec "the_Intg (Intg i) = i" consts the_Addr :: "val \ loc" primrec "the_Addr (Addr a) = a" types dyn_ty = "loc \ ty option" consts typeof :: "dyn_ty \ val \ ty option" defpval :: "prim_ty \ val" --{* default value for primitive types *} default_val :: " ty \ 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