| author | wenzelm |
| Fri, 05 Oct 2001 21:52:39 +0200 | |
| changeset 11701 | 3d51fbf81c17 |
| parent 11070 | cc421547e744 |
| child 11908 | 82f68fd05094 |
| permissions | -rw-r--r-- |
| oheimb@11026 | 1 |
(* Title: HOL/MicroJava/J/Value.thy |
| oheimb@9346 | 2 |
ID: $Id$ |
| oheimb@9346 | 3 |
Author: David von Oheimb |
| oheimb@9346 | 4 |
Copyright 1999 Technische Universitaet Muenchen |
| oheimb@11070 | 5 |
*) |
| oheimb@9346 | 6 |
|
| oheimb@11070 | 7 |
header "Java Values" |
| oheimb@9346 | 8 |
|
| oheimb@11026 | 9 |
theory Value = Type: |
| oheimb@9346 | 10 |
|
| oheimb@11026 | 11 |
typedecl loc (* locations, i.e. abstract references on objects *) |
| oheimb@11026 | 12 |
arities loc :: "term" |
| oheimb@9346 | 13 |
|
| oheimb@11026 | 14 |
datatype val |
| kleing@10061 | 15 |
= Unit (* dummy result value of void methods *) |
| kleing@10061 | 16 |
| Null (* null reference *) |
| kleing@10061 | 17 |
| Bool bool (* Boolean value *) |
| kleing@10061 | 18 |
| Intg int (* integer value, name Intg instead of Int because |
| kleing@10061 | 19 |
of clash with HOL/Set.thy *) |
| kleing@10061 | 20 |
| Addr loc (* addresses, i.e. locations of objects *) |
| kleing@10061 | 21 |
|
| oheimb@9346 | 22 |
consts |
| kleing@10061 | 23 |
the_Bool :: "val => bool" |
| kleing@10061 | 24 |
the_Intg :: "val => int" |
| kleing@10061 | 25 |
the_Addr :: "val => loc" |
| oheimb@9346 | 26 |
|
| oheimb@9346 | 27 |
primrec |
| kleing@10061 | 28 |
"the_Bool (Bool b) = b" |
| oheimb@9346 | 29 |
|
| oheimb@9346 | 30 |
primrec |
| kleing@10061 | 31 |
"the_Intg (Intg i) = i" |
| oheimb@9346 | 32 |
|
| oheimb@9346 | 33 |
primrec |
| kleing@10061 | 34 |
"the_Addr (Addr a) = a" |
| oheimb@9346 | 35 |
|
| oheimb@9346 | 36 |
consts |
| kleing@10061 | 37 |
defpval :: "prim_ty => val" (* default value for primitive types *) |
| kleing@10061 | 38 |
default_val :: "ty => val" (* default value for all types *) |
| oheimb@9346 | 39 |
|
| oheimb@9346 | 40 |
primrec |
| kleing@10061 | 41 |
"defpval Void = Unit" |
| kleing@10061 | 42 |
"defpval Boolean = Bool False" |
| wenzelm@11701 | 43 |
"defpval Integer = Intg (Numeral0)" |
| oheimb@9346 | 44 |
|
| oheimb@9346 | 45 |
primrec |
| kleing@10061 | 46 |
"default_val (PrimT pt) = defpval pt" |
| kleing@10061 | 47 |
"default_val (RefT r ) = Null" |
| oheimb@9346 | 48 |
|
| oheimb@9346 | 49 |
end |