# HG changeset patch
# User streckem
# Date 1035382242 -7200
# Node ID f4c64597fb023023899c62e9f4faed90eca98794
# Parent  2950128b820698a3b92ad51acfac5f4b06b856a4
*** empty log message ***

diff -r 2950128b8206 -r f4c64597fb02 src/HOL/MicroJava/JVM/JVMExceptions.thy
--- 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 {*
diff -r 2950128b8206 -r f4c64597fb02 src/HOL/MicroJava/JVM/JVMInstructions.thy
--- 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
diff -r 2950128b8206 -r f4c64597fb02 src/HOL/MicroJava/JVM/JVMState.thy
--- 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