header {* \isaheader{Jinja Values} *}
theory Value imports TypeRel begin
types addr = nat
types thread_id = addr
datatype val
= Unit -- "dummy result value of void expressions"
| Null -- "null reference"
| Bool bool -- "Boolean value"
| Intg int -- "integer value"
| Addr addr -- "addresses of objects, arrays and threads in the heap"
consts
default_val :: "ty => val" -- "default value for all types"
primrec
"default_val Void = Unit"
"default_val Boolean = Bool False"
"default_val Integer = Intg 0"
"default_val NT = Null"
"default_val (Class C) = Null"
"default_val (Array A) = Null"
consts
the_Intg :: "val => int"
the_Addr :: "val => addr"
primrec
"the_Intg (Intg i) = i"
primrec
"the_Addr (Addr a) = a"
fun is_Addr :: "val => bool"
where
"is_Addr (Addr a) = True"
| "is_Addr v = False"
lemma is_AddrE [elim!]:
"[| is_Addr v; !!a. v = Addr a ==> thesis |] ==> thesis"
by(cases v, auto)
fun is_Intg :: "val => bool"
where
"is_Intg (Intg i) = True"
| "is_Intg v = False"
lemma is_IntgE [elim!]:
"[| is_Intg v; !!i. v = Intg i ==> thesis |] ==> thesis"
by(cases v, auto)
fun is_Bool :: "val => bool"
where
"is_Bool (Bool b) = True"
| "is_Bool v = False"
lemma is_BoolE [elim!]:
"[| is_Bool v; !!a. v = Bool a ==> thesis |] ==> thesis"
by(cases v, auto)
constdefs
is_Ref :: "val => bool"
"is_Ref v ≡ v = Null ∨ is_Addr v"
lemma is_Ref_def2:
"is_Ref v = (v = Null ∨ (∃a. v = Addr a))"
by (cases v) (auto simp add: is_Ref_def)
lemma [iff]: "is_Ref Null" by (simp add: is_Ref_def2)
end