Theory Value

Up to index of Isabelle/Bali5

(*  Title:      isabelle/Bali/Value.thy
    ID:         $Id: Value.thy,v 1.3 2000/07/14 14:48:59 oheimb Exp $
    Author:     David von Oheimb
    Copyright   1997 Technische Universitaet Muenchen

Java values
*)

Value = Type +

types   loc             (* locations, i.e. abstract references on objects *)
arities loc :: term

datatype val_ (** name not 'val' because of nasty clash with ML token '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 *)
types         val   =         val_
translations "val" <= (type) "val_"
             "val" <= (type) "Term.val_"
             "loc" <= (type) "Term.loc"

constdefs
  the_Bool   :: "val \<Rightarrow> bool"  "the_Bool v \<equiv>  \<epsilon>b. v = Bool b"
  the_Intg   :: "val \<Rightarrow> int"   "the_Intg v \<equiv>  \<epsilon>i. v = Intg i"
  the_Addr   :: "val \<Rightarrow> loc"   "the_Addr v \<equiv>  \<epsilon>a. v = Addr 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

theorem the_Addr_Addr:

  the_Addr (Addr a) = a

theorem the_Intg_Intg:

  the_Intg (Intg i) = i