src/HOL/Bali/Value.thy
author berghofe
Mon Sep 30 16:14:02 2002 +0200 (2002-09-30)
changeset 13601 fd3e3d6b37b2
parent 12858 6214f03d6d27
child 13688 a0b16d42d489
permissions -rw-r--r--
Adapted to new simplifier.
wenzelm@12857
     1
(*  Title:      HOL/Bali/Value.thy
schirmer@12854
     2
    ID:         $Id$
schirmer@12854
     3
    Author:     David von Oheimb
wenzelm@12858
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
schirmer@12854
     5
*)
schirmer@12854
     6
header {* Java values *}
schirmer@12854
     7
schirmer@12854
     8
schirmer@12854
     9
schirmer@12854
    10
theory Value = Type:
schirmer@12854
    11
schirmer@12854
    12
typedecl loc            (* locations, i.e. abstract references on objects *)
schirmer@12854
    13
arities	 loc :: "type"
schirmer@12854
    14
schirmer@12854
    15
datatype val
schirmer@12854
    16
	= Unit          (* dummy result value of void methods *)
schirmer@12854
    17
	| Bool bool     (* Boolean value *)
schirmer@12854
    18
	| Intg int      (* integer value *)
schirmer@12854
    19
	| Null          (* null reference *)
schirmer@12854
    20
	| Addr loc      (* addresses, i.e. locations of objects *)
schirmer@12854
    21
schirmer@12854
    22
schirmer@12854
    23
translations "val" <= (type) "Term.val"
schirmer@12854
    24
             "loc" <= (type) "Term.loc"
schirmer@12854
    25
schirmer@12854
    26
consts   the_Bool   :: "val \<Rightarrow> bool"  
schirmer@12854
    27
primrec "the_Bool (Bool b) = b"
schirmer@12854
    28
consts   the_Intg   :: "val \<Rightarrow> int"
schirmer@12854
    29
primrec "the_Intg (Intg i) = i"
schirmer@12854
    30
consts   the_Addr   :: "val \<Rightarrow> loc"
schirmer@12854
    31
primrec "the_Addr (Addr a) = a"
schirmer@12854
    32
schirmer@12854
    33
types	dyn_ty      = "loc \<Rightarrow> ty option"
schirmer@12854
    34
consts
schirmer@12854
    35
  typeof        :: "dyn_ty \<Rightarrow> val \<Rightarrow> ty option"
schirmer@12854
    36
  defpval       :: "prim_ty \<Rightarrow> val"      (* default value for primitive types *)
schirmer@12854
    37
  default_val   :: "     ty \<Rightarrow> val"      (* default value for all types *)
schirmer@12854
    38
schirmer@12854
    39
primrec "typeof dt  Unit    = Some (PrimT Void)"
schirmer@12854
    40
	"typeof dt (Bool b) = Some (PrimT Boolean)"
schirmer@12854
    41
	"typeof dt (Intg i) = Some (PrimT Integer)"
schirmer@12854
    42
	"typeof dt  Null    = Some NT"
schirmer@12854
    43
	"typeof dt (Addr a) = dt a"
schirmer@12854
    44
schirmer@12854
    45
primrec	"defpval Void    = Unit"
schirmer@12854
    46
	"defpval Boolean = Bool False"
schirmer@12854
    47
	"defpval Integer = Intg 0"
schirmer@12854
    48
primrec	"default_val (PrimT pt) = defpval pt"
schirmer@12854
    49
	"default_val (RefT  r ) = Null"
schirmer@12854
    50
schirmer@12854
    51
end