--- a/src/HOL/MicroJava/J/State.thy Sun Dec 16 00:17:44 2001 +0100
+++ b/src/HOL/MicroJava/J/State.thy Sun Dec 16 00:18:17 2001 +0100
@@ -8,58 +8,57 @@
theory State = TypeRel + Value:
-types fields_
- = "(vname \<times> cname \<leadsto> val)" (* field name, defining class, value *)
+types
+ fields_ = "(vname \<times> cname \<leadsto> val)" -- "field name, defining class, value"
- obj = "cname \<times> fields_" (* class instance with class name and fields *)
+ obj = "cname \<times> fields_" -- "class instance with class name and fields"
constdefs
- obj_ty :: "obj => ty"
+ obj_ty :: "obj => ty"
"obj_ty obj == Class (fst obj)"
- init_vars :: "('a \<times> ty) list => ('a \<leadsto> val)"
- "init_vars == map_of o map (\<lambda>(n,T). (n,default_val T))"
+ init_vars :: "('a \<times> ty) list => ('a \<leadsto> val)"
+ "init_vars == map_of o map (\<lambda>(n,T). (n,default_val T))"
-datatype xcpt (* exceptions *)
- = NullPointer
- | ClassCast
- | OutOfMemory
+
+types aheap = "loc \<leadsto> obj" -- {* "@{text heap}" used in a translation below *}
+ locals = "vname \<leadsto> val" -- "simple state, i.e. variable contents"
-types aheap = "loc \<leadsto> obj" (** "heap" used in a translation below **)
- locals = "vname \<leadsto> val"
+ state = "aheap \<times> locals" -- "heap, local parameter including This"
+ xstate = "xcpt option \<times> state" -- "state including exception information"
+
- state (* simple state, i.e. variable contents *)
- = "aheap \<times> locals"
- (* heap, local parameter including This *)
+text {*
+ System exceptions are allocated in all heaps,
+ and they don't carry any information other than their type: *}
+axioms
+ system_xcpt_allocated: "(hp::aheap) (XcptRef x) = Some (Xcpt x, empty)"
- xstate (* state including exception information *)
- = "xcpt option \<times> state"
syntax
- heap :: "state => aheap"
- locals :: "state => locals"
- Norm :: "state => xstate"
+ heap :: "state => aheap"
+ locals :: "state => locals"
+ Norm :: "state => xstate"
translations
"heap" => "fst"
"locals" => "snd"
- "Norm s" == "(None,s)"
+ "Norm s" == "(None,s)"
constdefs
-
- new_Addr :: "aheap => loc \<times> xcpt option"
+ new_Addr :: "aheap => loc \<times> 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 :: "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 :: "val => xcpt option => xcpt option"
"np v == raise_if (v = Null) NullPointer"
- c_hupd :: "aheap => xstate => xstate"
+ 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 :: "'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"
@@ -93,7 +92,8 @@
apply auto
done
-lemma raise_if_Some2 [simp]: "raise_if c z (if x = None then Some y else x) \<noteq> None"
+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
@@ -105,12 +105,14 @@
apply auto
done
-lemma raise_if_NoneD [rule_format (no_asm)]: "raise_if c x y = None --> \<not> c \<and> y = None"
+lemma raise_if_NoneD [rule_format (no_asm)]:
+ "raise_if c x y = None --> \<not> 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"
+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