--- 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 {*