src/HOL/Bali/Value.thy

"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.

(*  Title:      HOL/Bali/Value.thy
    ID:         $Id$
    Author:     David von Oheimb
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
*)
header {* Java values *}



theory Value = Type:

typedecl loc            --{* locations, i.e. abstract references on objects *}
arities	 loc :: "type"

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