# Theory Value

```(*  Title:      JinjaThreads/Common/Value.thy
Author:     David von Oheimb, Tobias Nipkow, Andreas Lochbihler

Based on the Jinja theory Common/Value.thy by David von Oheimb and Tobias Nipkow
*)

section ‹Jinja Values›

theory Value
imports
TypeRel
"HOL-Library.Word"
begin

no_notation floor ("⌊_⌋")

type_synonym word32 = "32 word"

= Unit          ― ‹dummy result value of void expressions›
| Null          ― ‹null reference›
| Bool bool     ― ‹Boolean value›
| Intg word32   ― ‹integer value›

primrec default_val :: "ty ⇒ 'addr val"   ― ‹default value for all types›
where
"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"

by(cases T)(simp_all)

by(cases T)(simp_all)

primrec the_Intg :: "'addr val ⇒ word32"
where
"the_Intg (Intg i) = i"

where

where

"⟦ is_Addr v; ⋀a. v = Addr a ⟹ thesis ⟧ ⟹ thesis"
by(cases v, auto)

fun is_Intg :: "'addr val ⇒ bool"
where
"is_Intg (Intg i) = True"
| "is_Intg _        = False"

lemma is_IntgE [elim!]:
"⟦ is_Intg v; ⋀i. v = Intg i ⟹ thesis ⟧ ⟹ thesis"
by(cases v, auto)

fun is_Bool :: "'addr val ⇒ bool"
where
"is_Bool (Bool b) = True"
| "is_Bool _        = False"

lemma is_BoolE [elim!]:
"⟦ is_Bool v; ⋀a. v = Bool a ⟹ thesis ⟧ ⟹ thesis"
by(cases v, auto)

definition is_Ref :: "'addr val ⇒ bool"
where "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)

definition undefined_value :: "'addr val" where "undefined_value = Unit"