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

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›
  "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"
  "the_Intg (Intg i) = i"

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

fun is_Addr :: "'addr val  bool"
  "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"
  "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"
  "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"