diff -r 521f2da133be -r a955fe2879ba src/HOL/MicroJava/JVM/JVMState.thy
--- a/src/HOL/MicroJava/JVM/JVMState.thy	Sun Dec 16 00:18:44 2001 +0100
+++ b/src/HOL/MicroJava/JVM/JVMState.thy	Sun Dec 16 00:19:08 2001 +0100
@@ -1,43 +1,70 @@
 (*  Title:      HOL/MicroJava/JVM/JVMState.thy
     ID:         $Id$
-    Author:     Cornelia Pusch
+    Author:     Cornelia Pusch, Gerwin Klein
     Copyright   1999 Technische Universitaet Muenchen
 *)
 
-
 header {* State of the JVM *}
 
-
 theory JVMState = Conform:
 
-
-text {* frame stack :*}
+section {* Frame Stack *}
 types
- opstack 	 = "val list"
- locvars 	 = "val list" 
- p_count 	 = nat
+ opstack   = "val list"
+ locvars   = "val list" 
+ p_count   = nat
 
- frame = "opstack \<times>			
-          locvars \<times>		
-          cname \<times>			
-          sig \<times>			
+ frame = "opstack \<times>     
+          locvars \<times>   
+          cname \<times>     
+          sig \<times>     
           p_count"
 
-	(* operand stack *)
-	(* local variables *)
-	(* name of def. class defined *)
-	(* meth name+param_desc *)
-	(* program counter within frame *)
+  -- "operand stack" 
+  -- "local variables (including this pointer and method parameters)"
+  -- "name of class where current method is defined"
+  -- "method name + parameter types"
+  -- "program counter within frame"
+
+
+section {* Exceptions *}
+constdefs
+  raise_system_xcpt :: "bool \<Rightarrow> xcpt \<Rightarrow> val option"
+  "raise_system_xcpt b x == if b then Some (Addr (XcptRef x)) else None"
+
+  -- "redefines State.new\\_Addr:"
+  new_Addr :: "aheap => loc \<times> val option"
+  "new_Addr h == SOME (a,x). (h a = None \<and>  x = None) |
+                             x = raise_system_xcpt True OutOfMemory"
+
+
+section {* Runtime State *}
+types
+  jvm_state = "val option \<times> aheap \<times> frame list"  -- "exception flag, heap, frames"
 
 
-text {* exceptions: *}
-constdefs
-  raise_xcpt :: "bool => xcpt => xcpt option"
-  "raise_xcpt c x == (if c then Some x else None)"
-
+section {* Lemmas *}
 
-text {* runtime state: *}
-types
-  jvm_state = "xcpt option \<times> aheap \<times> frame list"	
+lemma new_AddrD:
+  "new_Addr hp = (ref, xcp) \<Longrightarrow> hp ref = None \<and> xcp = None \<or> xcp = Some (Addr (XcptRef OutOfMemory))"
+  apply (drule sym)
+  apply (unfold new_Addr_def)
+  apply (simp add: raise_system_xcpt_def)
+  apply (simp add: Pair_fst_snd_eq Eps_split)
+  apply (rule someI)
+  apply (rule disjI2)
+  apply (rule_tac "r" = "snd (?a,Some (Addr (XcptRef OutOfMemory)))" in trans)
+  apply auto
+  done
 
-end
+lemma new_Addr_OutOfMemory:
+  "snd (new_Addr hp) = Some xcp \<Longrightarrow> xcp = Addr (XcptRef OutOfMemory)"
+proof - 
+  obtain ref xp where "new_Addr hp = (ref, xp)" by (cases "new_Addr hp")
+  moreover
+  assume "snd (new_Addr hp) = Some xcp" 
+  ultimately
+  show ?thesis by (auto dest: new_AddrD)
+qed  
+
+end
\ No newline at end of file