Up to index of Isabelle/HOL/arrays
theory State = TypeRel + Value:(* Title: HOL/MicroJava/J/State.thy
ID: $Id: State.html,v 1.1 2002/11/28 16:11:18 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 to value"
entries_ = "nat \<leadsto> 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 \<Rightarrow> ty"
"obj_ty entry \<equiv> case entry of Obj C fs \<Rightarrow> Class C | Arr T len entries \<Rightarrow> T.[]"
init_vars :: "('a × ty) list => ('a \<leadsto> val)"
"init_vars \<equiv> map_of \<circ> map (\<lambda>(n,T). (n,default_val T))"
consts
the_obj :: "heap_entry \<Rightarrow> cname × fields_"
the_arr :: "heap_entry \<Rightarrow> 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 \<leadsto> heap_entry" -- {* "@{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 = "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 \<and> x = None) | x = Some OutOfMemory"
raise_if :: "bool => xcpt => xcpt option => xcpt option"
"raise_if c x xo == if c \<and> (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'== \<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 (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 \<Longrightarrow> h a = None \<and> 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 \<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 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 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
end
lemma obj_ty_def2:
obj_ty (Obj C fs) = Class C
lemma obj_ty_def3:
obj_ty (Arr T len entries) = T.[]
lemma new_AddrD:
(a, x) = new_Addr h ==> h a = None & x = None | x = Some 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 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 NullPointer
lemma np_Addr:
np (Addr a) None = None
lemma np_raise_if:
np Null (raise_if c xc None) = Some (if c then xc else NullPointer)