--- a/src/HOL/MicroJava/JVM/JVMState.thy Wed Oct 23 16:10:02 2002 +0200
+++ b/src/HOL/MicroJava/JVM/JVMState.thy Wed Oct 23 16:10:42 2002 +0200
@@ -33,45 +33,15 @@
section {* Exceptions *}
constdefs
raise_system_xcpt :: "bool \<Rightarrow> xcpt \<Rightarrow> val option"
- "raise_system_xcpt b x \<equiv> if b then Some (Addr (XcptRef x)) else None"
-
- -- "redefines State.new\\_Addr:"
- new_Addr :: "aheap \<Rightarrow> loc \<times> val option"
- "new_Addr h \<equiv> let (a, x) = State.new_Addr h
- in (a, raise_system_xcpt (x ~= None) OutOfMemory)"
-
+ "raise_system_xcpt b x \<equiv> raise_if b x None"
section {* Runtime State *}
types
jvm_state = "val option \<times> aheap \<times> frame list" -- "exception flag, heap, frames"
-text {* a new, blank object with default values in all fields: *}
-constdefs
- blank :: "'c prog \<Rightarrow> cname \<Rightarrow> obj"
- "blank G C \<equiv> (C,init_vars (fields(G,C)))"
-
- start_heap :: "'c prog \<Rightarrow> aheap"
- "start_heap G \<equiv> empty (XcptRef NullPointer \<mapsto> blank G (Xcpt NullPointer))
- (XcptRef ClassCast \<mapsto> blank G (Xcpt ClassCast))
- (XcptRef OutOfMemory \<mapsto> blank G (Xcpt OutOfMemory))"
-
section {* Lemmas *}
-lemma new_AddrD:
- assumes new: "new_Addr hp = (ref, xcp)"
- shows "hp ref = None \<and> xcp = None \<or> xcp = Some (Addr (XcptRef OutOfMemory))"
-proof -
- from new obtain xcpT where old: "State.new_Addr hp = (ref,xcpT)"
- by (cases "State.new_Addr hp") (simp add: new_Addr_def)
- from this [symmetric]
- have "hp ref = None \<and> xcpT = None \<or> xcpT = Some OutOfMemory"
- by (rule State.new_AddrD)
- with new old show ?thesis
- by (auto simp add: new_Addr_def raise_system_xcpt_def)
-qed
-
-
lemma new_Addr_OutOfMemory:
"snd (new_Addr hp) = Some xcp \<Longrightarrow> xcp = Addr (XcptRef OutOfMemory)"
proof -
@@ -82,4 +52,4 @@
show ?thesis by (auto dest: new_AddrD)
qed
-end
\ No newline at end of file
+end