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"

datatype 'addr val
  = Unit          ― ‹dummy result value of void expressions›
  | Null          ― ‹null reference›
  | Bool bool     ― ‹Boolean value›
  | Intg word32   ― ‹integer value› 
  | Addr 'addr    ― ‹addresses of objects, arrays and threads in the heap›

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"

lemma default_val_not_Addr: "default_val T ≠ Addr a"
by(cases T)(simp_all)

lemma Addr_not_default_val: "Addr a ≠ default_val T"
by(cases T)(simp_all)

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

primrec the_Addr :: "'addr val ⇒ 'addr"
where
  "the_Addr (Addr a) = a"

fun is_Addr :: "'addr val ⇒ bool"
where
  "is_Addr (Addr a) = True"
| "is_Addr _        = False"

lemma is_AddrE [elim!]:
  "⟦ 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"

lemma undefined_value_not_Addr: 
  "undefined_value ≠ Addr a" "Addr a ≠ undefined_value"
by(simp_all add: undefined_value_def)

class addr =
  fixes hash_addr :: "'a ⇒ int"
  and monitor_finfun_to_list :: "('a ⇒f nat) ⇒ 'a list"
  assumes "set (monitor_finfun_to_list f) = Collect (($) (finfun_dom f))"

locale addr_base =
  fixes addr2thread_id :: "'addr ⇒ 'thread_id"
  and thread_id2addr :: "'thread_id ⇒ 'addr"

end