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