--- a/src/HOL/MicroJava/JVM/JVMExceptions.thy Wed Oct 23 16:10:02 2002 +0200
+++ b/src/HOL/MicroJava/JVM/JVMExceptions.thy Wed Oct 23 16:10:42 2002 +0200
@@ -24,13 +24,9 @@
then Some (fst (snd (snd e)))
else match_exception_table G cn pc es)"
-
consts
- cname_of :: "aheap \<Rightarrow> val \<Rightarrow> cname"
ex_table_of :: "jvm_method \<Rightarrow> exception_table"
-
translations
- "cname_of hp v" == "fst (the (hp (the_Addr v)))"
"ex_table_of m" == "snd (snd (snd m))"
@@ -52,40 +48,6 @@
text {*
System exceptions are allocated in all heaps:
*}
-constdefs
- preallocated :: "aheap \<Rightarrow> bool"
- "preallocated hp \<equiv> \<forall>x. \<exists>fs. hp (XcptRef x) = Some (Xcpt x, fs)"
-
-lemma preallocatedD:
- "preallocated hp \<Longrightarrow> \<exists>fs. hp (XcptRef x) = Some (Xcpt x, fs)"
- by (unfold preallocated_def) fast
-
-lemma preallocatedE [elim?]:
- "preallocated hp \<Longrightarrow> (\<And>fs. hp (XcptRef x) = Some (Xcpt x, fs) \<Longrightarrow> P hp) \<Longrightarrow> P hp"
- by (fast dest: preallocatedD)
-
-lemma cname_of_xcp:
- "raise_system_xcpt b x = Some xcp \<Longrightarrow> preallocated hp
- \<Longrightarrow> cname_of (hp::aheap) xcp = Xcpt x"
-proof -
- assume "raise_system_xcpt b x = Some xcp"
- hence "xcp = Addr (XcptRef x)"
- by (simp add: raise_system_xcpt_def split: split_if_asm)
- moreover
- assume "preallocated hp"
- then obtain fs where "hp (XcptRef x) = Some (Xcpt x, fs)" ..
- ultimately
- show ?thesis by simp
-qed
-
-lemma preallocated_start:
- "preallocated (start_heap G)"
- apply (unfold preallocated_def)
- apply (unfold start_heap_def)
- apply (rule allI)
- apply (case_tac x)
- apply (auto simp add: blank_def)
- done
text {*
--- a/src/HOL/MicroJava/JVM/JVMInstructions.thy Wed Oct 23 16:10:02 2002 +0200
+++ b/src/HOL/MicroJava/JVM/JVMInstructions.thy Wed Oct 23 16:10:42 2002 +0200
@@ -36,6 +36,7 @@
-- "start-pc, end-pc, handler-pc, exception type"
exception_table = "exception_entry list"
jvm_method = "nat \<times> nat \<times> bytecode \<times> exception_table"
+ -- "max stacksize, length of local var array, \<dots>"
jvm_prog = "jvm_method prog"
end
--- 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