# HG changeset patch
# User kleing
# Date 979656994 -3600
# Node ID 9b74eceea2d29b5bccd7433a01055278c7a7dfd8
# Parent  144ede948e58a4fb0664e318a686795141770300
newref -> new_Addr

diff -r 144ede948e58 -r 9b74eceea2d2 src/HOL/MicroJava/BV/BVSpecTypeSafe.thy
--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Tue Jan 16 12:20:52 2001 +0100
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Tue Jan 16 15:56:34 2001 +0100
@@ -85,7 +85,7 @@
   note l = this
 
   show ?thesis 
-    by (force intro: null dest: l)
+    by (force dest: l)
 qed
 
 
@@ -169,30 +169,93 @@
   "(\<forall>x y. P(x,y)) = (\<forall>z. P z)"
   by fast
 
+
 lemma New_correct:
 "[| wf_prog wt G;
   method (G,C) sig = Some (C,rT,maxs,maxl,ins); 
-  ins!pc = New cl_idx; 
+  ins!pc = New X; 
   wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; 
   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
 ==> G,phi \<turnstile>JVM state'\<surd>"
-apply (clarsimp simp add: NT_subtype_conv approx_val_def conf_def defs1
-		   fun_upd_apply map_eq_Cons raise_xcpt_def init_vars_def 
-       split: option.split)
-apply (force dest!: iffD1 [OF collapse_paired_All]
-       intro: sup_heap_newref approx_stk_imp_approx_stk_sup_heap 
-              approx_stk_imp_approx_stk_sup 
-              approx_loc_imp_approx_loc_sup_heap 
-              approx_loc_imp_approx_loc_sup
-              hconf_imp_hconf_newref correct_frames_imp_correct_frames_newref
-              correct_init_obj 
-       simp add: NT_subtype_conv approx_val_def conf_def defs1
-         fun_upd_apply map_eq_Cons raise_xcpt_def init_vars_def 
-       split: option.split)
-done
+proof -
+  assume wf:   "wf_prog wt G"
+  assume meth: "method (G,C) sig = Some (C,rT,maxs,maxl,ins)"
+  assume ins:  "ins!pc = New X"
+  assume wt:   "wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc"
+  assume exec: "Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs)"
+  assume conf: "G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>"
+
+  from ins conf meth
+  obtain ST LT where
+    heap_ok:    "G\<turnstile>h hp\<surd>" and
+    phi_pc:     "phi C sig!pc = Some (ST,LT)" and
+    is_class_C: "is_class G C" and
+    frame:      "correct_frame G hp (ST,LT) maxl ins (stk, loc, C, sig, pc)" and
+    frames:     "correct_frames G hp phi rT sig frs"
+    by (auto simp add: correct_state_def iff del: not_None_eq)
+  from phi_pc ins wt
 
-
+  obtain ST' LT' where
+    is_class_X: "is_class G X" and
+    maxs:       "maxs < length ST" and
+    suc_pc:     "Suc pc < length ins" and
+    phi_suc:    "phi C sig ! Suc pc = Some (ST', LT')" and
+    less:       "G \<turnstile> (Class X # ST, LT) <=s (ST', LT')"
+    by (unfold wt_instr_def step_def) auto
+ 
+  obtain oref xp' where
+    new_Addr: "(oref,xp') = new_Addr hp"
+    by (cases "new_Addr hp") auto  
+  hence cases: 
+    "hp oref = None \<and> xp' = None \<or> xp' = Some OutOfMemory"
+    by (blast dest: new_AddrD)
+  moreover
+  { assume "xp' = Some OutOfMemory"
+    with exec ins meth new_Addr [symmetric]
+    have "state' = (Some OutOfMemory, hp, (stk, loc, C, sig, Suc pc) # frs)"
+      by simp
+    hence ?thesis
+      by (simp add: correct_state_def)
+  }
+  moreover
+  { assume hp: "hp oref = None" and "xp' = None"
+    with exec ins meth new_Addr [symmetric]
+    have state':
+      "state' = Norm (hp(oref\<mapsto>(X, init_vars (fields (G, X)))), 
+                      (Addr oref # stk, loc, C, sig, Suc pc) # frs)" 
+      (is "state' = Norm (?hp', ?f # frs)")
+      by simp    
+    moreover
+    from wf hp heap_ok is_class_X
+    have hp': "G \<turnstile>h ?hp' \<surd>"
+      by - (rule hconf_imp_hconf_newref, 
+            auto simp add: oconf_def dest: fields_is_type)
+    moreover
+    from hp
+    have sup: "hp \<le>| ?hp'" by (rule sup_heap_newref)
+    from hp frame less suc_pc wf
+    have "correct_frame G ?hp' (ST', LT') maxl ins ?f"
+      apply (unfold correct_frame_def sup_state_conv)
+      apply (clarsimp simp add: map_eq_Cons conf_def fun_upd_apply approx_val_def)
+      apply (blast intro: approx_stk_imp_approx_stk_sup_heap 
+                          approx_stk_imp_approx_stk_sup
+                          approx_loc_imp_approx_loc_sup_heap 
+                          approx_loc_imp_approx_loc_sup sup)
+      done      
+    moreover
+    from hp frames wf heap_ok is_class_X
+    have "correct_frames G ?hp' phi rT sig frs"
+      by - (rule correct_frames_imp_correct_frames_newref,
+            auto simp add: oconf_def dest: fields_is_type)
+    ultimately
+    have ?thesis
+      by (simp add: is_class_C meth phi_suc correct_state_def del: not_None_eq)
+  }
+  ultimately
+  show ?thesis by auto
+qed
+  
 (****** Method Invocation ******)
 
 lemmas [simp del] = split_paired_Ex
diff -r 144ede948e58 -r 9b74eceea2d2 src/HOL/MicroJava/BV/Correct.thy
--- a/src/HOL/MicroJava/BV/Correct.thy	Tue Jan 16 12:20:52 2001 +0100
+++ b/src/HOL/MicroJava/BV/Correct.thy	Tue Jan 16 15:56:34 2001 +0100
@@ -76,14 +76,16 @@
  correct_state :: "[jvm_prog,prog_type,jvm_state] => bool"
                   ("_,_ |-JVM _ [ok]"  [51,51] 50)
 
-
 lemma sup_heap_newref:
-  "hp x = None ==> hp \<le>| hp(newref hp \<mapsto> obj)"
-apply (unfold hext_def)
-apply clarsimp
-apply (drule newref_None 1) back
-apply simp
-done
+  "hp oref = None ==> hp \<le>| hp(oref \<mapsto> obj)"
+proof (unfold hext_def, intro strip)
+  fix a C fs  
+  assume "hp oref = None" and hp: "hp a = Some (C, fs)"
+  hence "a \<noteq> oref" by auto 
+  hence "(hp (oref\<mapsto>obj)) a = hp a" by (rule fun_upd_other)
+  with hp
+  show "\<exists>fs'. (hp(oref\<mapsto>obj)) a = Some (C, fs')" by auto
+qed
 
 lemma sup_heap_update_value:
   "hp a = Some (C,od') ==> hp \<le>| hp (a \<mapsto> (C,od))"
@@ -254,15 +256,13 @@
   ==> G,hp\<turnstile>(oT, fs(FD\<mapsto>v))\<surd>"
 by (simp add: oconf_def lconf_def)
 
-
 lemma oconf_imp_oconf_heap_newref [rule_format]:
-"hp x = None --> G,hp\<turnstile>obj\<surd> --> G,hp\<turnstile>obj'\<surd> --> G,(hp(newref hp\<mapsto>obj'))\<turnstile>obj\<surd>"
+"hp oref = None --> G,hp\<turnstile>obj\<surd> --> G,hp\<turnstile>obj'\<surd> --> G,(hp(oref\<mapsto>obj'))\<turnstile>obj\<surd>"
 apply (unfold oconf_def lconf_def)
 apply simp
 apply (fast intro: conf_hext sup_heap_newref)
 done
 
-
 lemma oconf_imp_oconf_heap_update [rule_format]:
   "hp a = Some obj' --> obj_ty obj' = obj_ty obj'' --> G,hp\<turnstile>obj\<surd> 
   --> G,hp(a\<mapsto>obj'')\<turnstile>obj\<surd>"
@@ -274,9 +274,8 @@
 
 (** hconf **)
 
-
 lemma hconf_imp_hconf_newref [rule_format]:
-  "hp x = None --> G\<turnstile>h hp\<surd> --> G,hp\<turnstile>obj\<surd> --> G\<turnstile>h hp(newref hp\<mapsto>obj)\<surd>"
+  "hp oref = None --> G\<turnstile>h hp\<surd> --> G,hp\<turnstile>obj\<surd> --> G\<turnstile>h hp(oref\<mapsto>obj)\<surd>"
 apply (simp add: hconf_def)
 apply (fast intro: oconf_imp_oconf_heap_newref)
 done
@@ -300,7 +299,12 @@
   --> correct_frames G (hp(a \<mapsto> (C, od(fl\<mapsto>v)))) phi rT sig frs";
 apply (induct frs)
  apply simp
-apply (clarsimp simp add: correct_frame_def) (*takes long*)
+apply clarify
+apply simp
+apply clarify
+apply (unfold correct_frame_def)
+apply (simp (no_asm_use))
+apply clarsimp
 apply (intro exI conjI)
      apply simp
     apply simp
@@ -318,7 +322,7 @@
 
 lemma correct_frames_imp_correct_frames_newref [rule_format]:
   "\<forall>rT C sig. hp x = None --> correct_frames G hp phi rT sig frs \<and> oconf G hp obj 
-  --> correct_frames G (hp(newref hp \<mapsto> obj)) phi rT sig frs"
+  --> correct_frames G (hp(x \<mapsto> obj)) phi rT sig frs"
 apply (induct frs)
  apply simp
 apply (clarsimp simp add: correct_frame_def)
diff -r 144ede948e58 -r 9b74eceea2d2 src/HOL/MicroJava/JVM/JVMExecInstr.thy
--- a/src/HOL/MicroJava/JVM/JVMExecInstr.thy	Tue Jan 16 12:20:52 2001 +0100
+++ b/src/HOL/MicroJava/JVM/JVMExecInstr.thy	Tue Jan 16 15:56:34 2001 +0100
@@ -25,8 +25,7 @@
       (None, hp, (v # stk, vars, Cl, sig, pc+1)#frs)"
 
  "exec_instr (New C) G hp stk vars Cl sig pc frs = 
-	(let xp'	= raise_xcpt (\<forall>x. hp x \<noteq> None) OutOfMemory;
-	     oref	= newref hp;
+	(let (oref,xp')	= new_Addr hp;
        fs		= init_vars (fields(G,C));
 	     hp'	= if xp'=None then hp(oref \<mapsto> (C,fs)) else hp;
 	     stk'	= if xp'=None then (Addr oref)#stk else stk