Theory State

(*  Title:      HOL/MicroJava/J/State.thy
    ID:         $Id: State.thy,v 1.19 2007/09/30 19:55:17 wenzelm Exp $
    Author:     David von Oheimb
    Copyright   1999 Technische Universitaet Muenchen
*)

header {* \isaheader{Program State} *}

theory State imports TypeRel Value  begin

types 
  fields_  = "(vname × cname \<rightharpoonup> val)"  -- "field name, defining class to value"
  entries_ = "nat \<rightharpoonup> val"              -- "array index to value"

datatype
  heap_entry = Obj cname fields_    -- "class instance with class name and fields"
             | Arr ty nat entries_  -- "array with component type, length, and entries"

constdefs
  obj_ty  :: "heap_entry => ty"
 "obj_ty entry ≡ case entry of Obj C fs => Class C | Arr T len entries => T.[]"

  init_vars :: "('a × ty) list => ('a \<rightharpoonup> val)"
 "init_vars ≡ map_of o map (λ(n,T). (n,default_val T))"

consts
  the_obj :: "heap_entry => cname × fields_"
  the_arr :: "heap_entry => ty × nat × entries_"

recdef the_obj "{}"
  "the_obj (Obj C fs) = (C,fs)"

recdef the_arr "{}"
  "the_arr (Arr T len entries) = (T,len,entries)"
  
types aheap  = "loc \<rightharpoonup> heap_entry"   -- {* "@{text heap}" used in a translation below *}
      locals = "vname \<rightharpoonup> val"        -- "simple state, i.e. variable contents"
      state  = "aheap × locals"      -- "heap, local parameter including This"
      xstate = "xcpt option × state" -- "state including exception information"

syntax
  heap    :: "state => aheap"
  locals  :: "state => locals"
  Norm    :: "state => xstate"

translations
  "heap"   => "fst"
  "locals" => "snd"
  "Norm s" == "(None,s)"

constdefs
  new_Addr  :: "aheap => loc × xcpt option"
 "new_Addr h == SOME (a,x). (h a = None ∧  x = None) |  x = Some OutOfMemory"

  raise_if  :: "bool => xcpt => xcpt option => xcpt option"
 "raise_if c x xo == if c ∧  (xo = None) then Some x else xo"

  np    :: "val => xcpt option => xcpt option"
 "np v == raise_if (v = Null) NullPointer"

  c_hupd  :: "aheap => xstate => xstate"
 "c_hupd h'== λ(xo,(h,l)). if xo = None then (None,(h',l)) else (xo,(h,l))"


  cast_ok :: "'c prog => cname => aheap => val => bool"
  "cast_ok G C h v == v = Null ∨ G\<turnstile>obj_ty (the (h (the_Addr v)))\<preceq> Class C"




(* LEMMAS *)

lemma obj_ty_def2 [simp]: "obj_ty (Obj C fs) = Class C"
apply (unfold obj_ty_def)
apply (simp (no_asm))
done

lemma obj_ty_def3 [simp]: "obj_ty (Arr T len entries) = T.[]"
  by (unfold obj_ty_def) simp


(*
lemma new_AddrD: 
"(a,x) = new_Addr h ==> h a = None ∧ x = None | x = Some OutOfMemory"
apply (unfold new_Addr_def)
apply(simp add: Pair_fst_snd_eq Eps_split)
apply(rule someI)
apply(rule disjI2)
apply(rule_tac "r" = "snd (?a,Some OutOfMemory)" in trans)
apply auto
done
*)

lemma raise_if_True [simp]: "raise_if True x y ≠ None"
apply (unfold raise_if_def)
apply auto
done

lemma raise_if_False [simp]: "raise_if False x y = y"
apply (unfold raise_if_def)
apply auto
done

lemma raise_if_Some [simp]: "raise_if c x (Some y) ≠ None"
apply (unfold raise_if_def)
apply auto
done

lemma raise_if_Some2 [simp]: 
  "raise_if c z (if x = None then Some y else x) ≠ None"
apply (unfold raise_if_def)
apply(induct_tac "x")
apply auto
done

lemma raise_if_SomeD [rule_format (no_asm)]: 
  "raise_if c x y = Some z --> c ∧  Some z = Some x |  y = Some z"
apply (unfold raise_if_def)
apply auto
done

lemma raise_if_NoneD [rule_format (no_asm)]: 
  "raise_if c x y = None --> ¬ c ∧  y = None"
apply (unfold raise_if_def)
apply auto
done

lemma np_NoneD [rule_format (no_asm)]: 
  "np a' x' = None --> x' = None ∧  a' ≠ Null"
apply (unfold np_def raise_if_def)
apply auto
done

lemma np_None [rule_format (no_asm), simp]: "a' ≠ Null --> np a' x' = x'"
apply (unfold np_def raise_if_def)
apply auto
done

lemma np_Some [simp]: "np a' (Some xc) = Some xc"
apply (unfold np_def raise_if_def)
apply auto
done

lemma np_Null [simp]: "np Null None = Some NullPointer"
apply (unfold np_def raise_if_def)
apply auto
done

lemma np_Addr [simp]: "np (Addr a) None = None"
apply (unfold np_def raise_if_def)
apply auto
done

lemma np_raise_if [simp]: "(np Null (raise_if c xc None)) =  
  Some (if c then xc else NullPointer)"
apply (unfold raise_if_def)
apply (simp (no_asm))
done

(* ADDED FROM COMFORM.thy *)



syntax (xsymbols)
  conf     :: "'c prog => aheap => val => ty => bool"
              ("_,_ \<turnstile> _ ::\<preceq> _" [51,51,51,51] 50)

end