src/HOL/MicroJava/J/Value.thy
author nipkow
Wed Jan 04 19:22:53 2006 +0100 (2006-01-04)
changeset 18576 8d98b7711e47
parent 16417 9bc16273c2d4
child 24783 5a3e336a2e37
permissions -rw-r--r--
Reversed Larry's option/iff change.
     1 (*  Title:      HOL/MicroJava/J/Value.thy
     2     ID:         $Id$
     3     Author:     David von Oheimb
     4     Copyright   1999 Technische Universitaet Muenchen
     5 *)
     6 
     7 header {* \isaheader{Java Values} *}
     8 
     9 theory Value imports Type begin
    10 
    11 typedecl loc_ -- "locations, i.e. abstract references on objects" 
    12 
    13 datatype loc 
    14   = XcptRef xcpt -- "special locations for pre-allocated system exceptions"
    15   | Loc loc_     -- "usual locations (references on objects)"
    16 
    17 datatype val
    18   = Unit        -- "dummy result value of void methods"
    19   | Null        -- "null reference"
    20   | Bool bool   -- "Boolean value"
    21   | Intg int    -- "integer value, name Intg instead of Int because
    22                    of clash with HOL/Set.thy" 
    23   | Addr loc    -- "addresses, i.e. locations of objects "
    24 
    25 consts
    26   the_Bool :: "val => bool"
    27   the_Intg :: "val => int"
    28   the_Addr :: "val => loc"
    29 
    30 primrec
    31   "the_Bool (Bool b) = b"
    32 
    33 primrec
    34   "the_Intg (Intg i) = i"
    35 
    36 primrec
    37   "the_Addr (Addr a) = a"
    38 
    39 consts
    40   defpval :: "prim_ty => val"  -- "default value for primitive types"
    41   default_val :: "ty => val"   -- "default value for all types"
    42 
    43 primrec
    44   "defpval Void    = Unit"
    45   "defpval Boolean = Bool False"
    46   "defpval Integer = Intg 0"
    47 
    48 primrec
    49   "default_val (PrimT pt) = defpval pt"
    50   "default_val (RefT  r ) = Null"
    51 
    52 end