# HG changeset patch
# User kleing
# Date 1016711911 -3600
# Node ID b1789117a1c634d5dca36801c1a695443e1bc763
# Parent  4b1edf2f6bd261690bf40db60f0520299efb6143
new_Addr defined in terms of J/State.new_Addr (for compiler)

diff -r 4b1edf2f6bd2 -r b1789117a1c6 src/HOL/MicroJava/JVM/JVMState.thy
--- a/src/HOL/MicroJava/JVM/JVMState.thy	Wed Mar 20 13:21:07 2002 +0100
+++ b/src/HOL/MicroJava/JVM/JVMState.thy	Thu Mar 21 12:58:31 2002 +0100
@@ -33,12 +33,12 @@
 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"
+  "raise_system_xcpt b x \<equiv> 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"
+  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)"
 
 
 section {* Runtime State *}
@@ -53,22 +53,24 @@
 
   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))"
+                        (XcptRef ClassCast \<mapsto> blank G (Xcpt ClassCast))
+                        (XcptRef OutOfMemory \<mapsto> blank G (Xcpt OutOfMemory))"
 
 section {* Lemmas *}
 
 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
+  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)"