src/HOL/Bali/Value.thy
author hoelzl
Fri Feb 19 13:40:50 2016 +0100 (2016-02-19)
changeset 62378 85ed00c1fe7c
parent 62042 6c6ccf573479
child 67443 3abf6a722518
permissions -rw-r--r--
generalize more theorems to support enat and ennreal
wenzelm@12857
     1
(*  Title:      HOL/Bali/Value.thy
schirmer@12854
     2
    Author:     David von Oheimb
schirmer@12854
     3
*)
wenzelm@62042
     4
subsection \<open>Java values\<close>
schirmer@12854
     5
schirmer@12854
     6
schirmer@12854
     7
haftmann@16417
     8
theory Value imports Type begin
schirmer@12854
     9
wenzelm@62042
    10
typedecl loc            \<comment>\<open>locations, i.e. abstract references on objects\<close>
schirmer@12854
    11
blanchet@58310
    12
datatype val
wenzelm@62042
    13
        = Unit          \<comment>\<open>dummy result value of void methods\<close>
wenzelm@62042
    14
        | Bool bool     \<comment>\<open>Boolean value\<close>
wenzelm@62042
    15
        | Intg int      \<comment>\<open>integer value\<close>
wenzelm@62042
    16
        | Null          \<comment>\<open>null reference\<close>
wenzelm@62042
    17
        | Addr loc      \<comment>\<open>addresses, i.e. locations of objects\<close>
schirmer@12854
    18
schirmer@12854
    19
wenzelm@37956
    20
primrec the_Bool :: "val \<Rightarrow> bool"
wenzelm@37956
    21
  where "the_Bool (Bool b) = b"
wenzelm@37956
    22
wenzelm@37956
    23
primrec the_Intg :: "val \<Rightarrow> int"
wenzelm@37956
    24
  where "the_Intg (Intg i) = i"
wenzelm@37956
    25
wenzelm@37956
    26
primrec the_Addr :: "val \<Rightarrow> loc"
wenzelm@37956
    27
  where "the_Addr (Addr a) = a"
schirmer@12854
    28
wenzelm@41778
    29
type_synonym dyn_ty = "loc \<Rightarrow> ty option"
wenzelm@37956
    30
wenzelm@37956
    31
primrec typeof :: "dyn_ty \<Rightarrow> val \<Rightarrow> ty option"
wenzelm@37956
    32
where
wenzelm@37956
    33
  "typeof dt  Unit = Some (PrimT Void)"
wenzelm@37956
    34
| "typeof dt (Bool b) = Some (PrimT Boolean)"
wenzelm@37956
    35
| "typeof dt (Intg i) = Some (PrimT Integer)"
wenzelm@37956
    36
| "typeof dt  Null = Some NT"
wenzelm@37956
    37
| "typeof dt (Addr a) = dt a"
schirmer@12854
    38
wenzelm@62042
    39
primrec defpval :: "prim_ty \<Rightarrow> val"  \<comment>\<open>default value for primitive types\<close>
wenzelm@37956
    40
where
wenzelm@37956
    41
  "defpval Void = Unit"
wenzelm@37956
    42
| "defpval Boolean = Bool False"
wenzelm@37956
    43
| "defpval Integer = Intg 0"
schirmer@12854
    44
wenzelm@62042
    45
primrec default_val :: "ty \<Rightarrow> val"  \<comment>\<open>default value for all types\<close>
wenzelm@37956
    46
where
wenzelm@37956
    47
  "default_val (PrimT pt) = defpval pt"
wenzelm@37956
    48
| "default_val (RefT  r ) = Null"
schirmer@12854
    49
schirmer@12854
    50
end