Theory State

Up to index of Isabelle/HOL/exceptions

theory State = TypeRel + Value:
(*  Title:      HOL/MicroJava/J/State.thy
    ID:         $Id: State.html,v 1.1 2002/11/28 13:16:31 kleing Exp $
    Author:     David von Oheimb
    Copyright   1999 Technische Universitaet Muenchen
*)

header {* \isaheader{Program State} *}

theory State = TypeRel + Value:

types 
  fields_ = "(vname × cname \<leadsto> val)"  -- "field name, defining class, value"

  obj = "cname × fields_"    -- "class instance with class name and fields"

constdefs
  obj_ty  :: "obj => ty"
 "obj_ty obj  == Class (fst obj)"

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

types aheap  = "loc \<leadsto> obj"    -- {* "@{text heap}" used in a translation below *}
      locals = "vname \<leadsto> val"  -- "simple state, i.e. variable contents"

      state  = "aheap × locals"      -- "heap, local parameter including This"
      xstate = "val option × state" -- "state including exception information"

syntax
  heap    :: "state => aheap"
  locals  :: "state => locals"
  Norm    :: "state => xstate"
  abrupt  :: "xstate \<Rightarrow> val option"
  store   :: "xstate \<Rightarrow> state"
  lookup_obj   :: "state \<Rightarrow> val \<Rightarrow> obj"

translations
  "heap"   => "fst"
  "locals" => "snd"
  "Norm s" == "(None,s)"
  "abrupt"     => "fst"
  "store"      => "snd"
 "lookup_obj s a'"  == "the (heap s (the_Addr a'))"


constdefs
  raise_if :: "bool \<Rightarrow> xcpt \<Rightarrow> val option \<Rightarrow> val option"
  "raise_if b x xo \<equiv> if b \<and>  (xo = None) then Some (Addr (XcptRef x)) else xo"

  new_Addr  :: "aheap => loc × val option"
  "new_Addr h \<equiv> SOME (a,x). (h a = None \<and>  x = None) |  x = Some (Addr (XcptRef OutOfMemory))"

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

  c_hupd  :: "aheap => xstate => xstate"
 "c_hupd h'== \<lambda>(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 \<or> G\<turnstile>obj_ty (the (h (the_Addr v)))\<preceq> Class C"

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


lemma new_AddrD: "new_Addr hp = (ref, xcp) \<Longrightarrow>
  hp ref = None \<and> xcp = None \<or> xcp = Some (Addr (XcptRef OutOfMemory))"
apply (drule sym)
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 (Addr (XcptRef OutOfMemory)))" in trans)
apply auto
done

lemma raise_if_True [simp]: "raise_if True x y \<noteq> 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) \<noteq> 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) \<noteq> 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 \<longrightarrow> c \<and>  Some z = Some (Addr (XcptRef 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 \<and>  y = None"
apply (unfold raise_if_def)
apply auto
done

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

lemma np_None [rule_format (no_asm), simp]: "a' \<noteq> 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 (Addr (XcptRef 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 (Addr (XcptRef (if c then  xc else NullPointer)))"
apply (unfold raise_if_def)
apply (simp (no_asm))
done

end

lemma obj_ty_def2:

  obj_ty (C, fs) = Class C

lemma new_AddrD:

  new_Addr hp = (ref, xcp)
  ==> hp ref = None & xcp = None | xcp = Some (Addr (XcptRef OutOfMemory))

lemma raise_if_True:

  raise_if True x y ~= None

lemma raise_if_False:

  raise_if False x y = y

lemma raise_if_Some:

  raise_if c x (Some y) ~= None

lemma raise_if_Some2:

  raise_if c z (if x = None then Some y else x) ~= None

lemma raise_if_SomeD:

  raise_if c x y = Some z ==> c & Some z = Some (Addr (XcptRef x)) | y = Some z

lemma raise_if_NoneD:

  raise_if c x y = None ==> ¬ c & y = None

lemma np_NoneD:

  np a' x' = None ==> x' = None & a' ~= Null

lemma np_None:

  a' ~= Null ==> np a' x' = x'

lemma np_Some:

  np a' (Some xc) = Some xc

lemma np_Null:

  np Null None = Some (Addr (XcptRef NullPointer))

lemma np_Addr:

  np (Addr a) None = None

lemma np_raise_if:

  np Null (raise_if c xc None) =
  Some (Addr (XcptRef (if c then xc else NullPointer)))