Theory Objects

(*  Title:      HOL/MicroJava/J/State.thy

    Author:     David von Oheimb
    Copyright   1999 Technische Universitaet Muenchen

section ‹Objects and the Heap›

theory Objects imports TypeRel Value begin


  fields = "vname × cname  val"  ― ‹field name, defining class, value›
  obj = "cname × fields"    ― ‹class instance with class name and fields›

definition obj_ty  :: "obj  ty"
  "obj_ty obj    Class (fst obj)"

definition init_fields :: "((vname × cname) × ty) list  fields"
  "init_fields    map_of  map (λ(F,T). (F,default_val T))"
  ― ‹a new, blank object with default values in all fields:›
definition blank :: "'m prog  cname  obj"
  "blank P C    (C,init_fields (fields P C))" 

lemma [simp]: "obj_ty (C,fs) = Class C"
(*<*)by (simp add: obj_ty_def)(*>*)


type_synonym heap  = "addr  obj"

  cname_of :: "heap  addr  cname" where
  "cname_of hp a == fst (the (hp a))"

definition new_Addr  :: "heap  addr option"
  "new_Addr h    if a. h a = None then Some(LEAST a. h a = None) else None"

definition cast_ok :: "'m prog  cname  heap  val  bool"
  "cast_ok P C h v    v = Null  P  cname_of h (the_Addr v) * C"

definition hext :: "heap  heap  bool" ("_  _" [51,51] 50)
  "h  h'    a C fs. h a = Some(C,fs)  (fs'. h' a = Some(C,fs'))"

primrec typeof_h :: "heap  val  ty option"  ("typeof⇘_")
  "typeof⇘hUnit    = Some Void"
| "typeof⇘hNull    = Some NT"
| "typeof⇘h(Bool b) = Some Boolean"
| "typeof⇘h(Intg i) = Some Integer"
| "typeof⇘h(Addr a) = (case h a of None  None | Some(C,fs)  Some(Class C))"

lemma new_Addr_SomeD:
  "new_Addr h = Some a  h a = None"
 (*<*)by(fastforce simp add:new_Addr_def split:if_splits intro:LeastI)(*>*)

lemma [simp]: "(typeof⇘hv = Some Boolean) = (b. v = Bool b)"
 (*<*)by(induct v) auto(*>*)

lemma [simp]: "(typeof⇘hv = Some Integer) = (i. v = Intg i)"
(*<*)by(cases v) auto(*>*)

lemma [simp]: "(typeof⇘hv = Some NT) = (v = Null)"
 (*<*)by(cases v) auto(*>*)

lemma [simp]: "(typeof⇘hv = Some(Class C)) = (a fs. v = Addr a  h a = Some(C,fs))"
 (*<*)by(cases v) auto(*>*)

lemma [simp]: "h a = Some(C,fs)  typeof⇘(h(a(C,fs')))v = typeof⇘hv"
 (*<*)by(induct v) (auto simp:fun_upd_apply)(*>*)

text‹For literal values the first parameter of @{term typeof} can be
set to @{term Map.empty} because they do not contain addresses:›

  typeof :: "val  ty option" where
  "typeof v == typeof_h Map.empty v"

lemma typeof_lit_typeof:
  "typeof v = Some T  typeof⇘hv = Some T"
 (*<*)by(cases v) auto(*>*)

lemma typeof_lit_is_type: 
  "typeof v = Some T  is_type P T"
 (*<*)by (induct v) (auto simp:is_type_def)(*>*)

subsection ‹Heap extension ⊴›

lemma hextI: "a C fs. h a = Some(C,fs)  (fs'. h' a = Some(C,fs'))  h  h'"
(*<*)by(auto simp: hext_def)(*>*)

lemma hext_objD: " h  h'; h a = Some(C,fs)   fs'. h' a = Some(C,fs')"
(*<*)by(auto simp: hext_def)(*>*)

lemma hext_refl [iff]: "h  h"
(*<*)by (rule hextI) fast(*>*)

lemma hext_new [simp]: "h a = None  h  h(ax)"
(*<*)by (rule hextI) (auto simp:fun_upd_apply)(*>*)

lemma hext_trans: " h  h'; h'  h''   h  h''"
(*<*)by (rule hextI) (fast dest: hext_objD)(*>*)

lemma hext_upd_obj: "h a = Some (C,fs)  h  h(a(C,fs'))"
(*<*)by (rule hextI) (auto simp:fun_upd_apply)(*>*)

lemma hext_typeof_mono: " h  h'; typeof⇘hv = Some T   typeof⇘h'v = Some T"
proof(cases v)
  case Addr assume "h  h'" and "typeof⇘hv = T"
  then show ?thesis using Addr by(fastforce simp:hext_def)
qed simp_all

text ‹Code generator setup for @{term "new_Addr"}

definition gen_new_Addr :: "heap  addr  addr option"
where "gen_new_Addr h n  if a. a  n  h a = None then Some(LEAST a. a  n  h a = None) else None"

lemma new_Addr_code_code [code]:
  "new_Addr h = gen_new_Addr h 0"
by(simp add: new_Addr_def gen_new_Addr_def split del: if_split cong: if_cong)

lemma gen_new_Addr_code [code]:
  "gen_new_Addr h n = (if h n = None then Some n else gen_new_Addr h (Suc n))"
apply(simp add: gen_new_Addr_def)
apply(rule impI)
apply(rule conjI)
 apply safe[1]
  apply(fastforce intro: Least_equality)
 apply(rule arg_cong[where f=Least])
 apply(rule ext)
 apply(case_tac "n = ac")
  apply simp
apply clarify
apply(subgoal_tac "a = n")
 apply simp
 apply(rule Least_equality)
 apply auto[2]
apply(rule ccontr)
apply(erule_tac x="a" in allE)
apply simp