Theory Value

Up to index of Isabelle/HOL/MicroJava

(*  Title:      HOL/MicroJava/J/Term.thy
    ID:         $Id: Value.thy,v 1.3 2000/09/22 14:28:56 kleing Exp $
    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 => bool"
  the_Intg :: "val => int"
  the_Addr :: "val => loc"

primrec
  "the_Bool (Bool b) = b"

primrec
  "the_Intg (Intg i) = i"

primrec
  "the_Addr (Addr a) = a"

consts
  defpval :: "prim_ty => val"  (* default value for primitive types *)
  default_val :: "ty => 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