--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Tue Dec 18 18:37:56 2001 +0100
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Tue Dec 18 21:28:01 2001 +0100
@@ -247,16 +247,16 @@
==> \<exists>adr T. xcp = Addr adr \<and> hp adr = Some T"
(is "[| ?xcpt; ?wt; ?correct |] ==> ?thesis")
proof -
- note [simp] = system_xcpt_allocated split_beta raise_system_xcpt_def
+ note [simp] = split_beta raise_system_xcpt_def
note [split] = split_if_asm option.split_asm
assume wt: ?wt ?correct
+ hence pre: "preallocated hp" by (simp add: correct_state_def)
- assume xcpt: ?xcpt
- thus ?thesis
+ assume xcpt: ?xcpt with pre show ?thesis
proof (cases "ins!pc")
- case New with xcpt
- show ?thesis by (auto dest: new_Addr_OutOfMemory)
+ case New with xcpt pre
+ show ?thesis by (auto dest: new_Addr_OutOfMemory)
next
case Throw with xcpt wt
show ?thesis
@@ -311,6 +311,7 @@
from correct meth
obtain ST LT where
hp_ok: "G \<turnstile>h hp \<surd>" and
+ prehp: "preallocated hp" and
class: "is_class G C" and
phi_pc: "phi C sig ! pc = Some (ST, LT)" and
frame: "correct_frame G hp (ST, LT) maxl ins (stk, loc, C, sig, pc)" and
@@ -349,8 +350,7 @@
with some_handler xp'
have xcp: "xcp = Addr (XcptRef OutOfMemory)"
by (simp add: raise_system_xcpt_def split_beta new_Addr_OutOfMemory)
- hence "cname_of hp xcp = Xcpt OutOfMemory"
- by (simp add: system_xcpt_allocated)
+ with prehp have "cname_of hp xcp = Xcpt OutOfMemory" by simp
with New some_handler phi_pc eff
obtain ST' LT' where
phi': "phi C sig ! handler = Some (ST', LT')" and
@@ -359,9 +359,9 @@
by (simp add: xcpt_eff_def) blast
note phi'
moreover
- { from xcp
+ { from xcp prehp
have "G,hp \<turnstile> xcp ::\<preceq> Class (Xcpt OutOfMemory)"
- by (simp add: conf_def obj_ty_def system_xcpt_allocated)
+ by (simp add: conf_def obj_ty_def)
moreover
from wf less loc
have "approx_loc G hp loc LT'"
@@ -380,8 +380,7 @@
with some_handler xp'
have xcp: "xcp = Addr (XcptRef NullPointer)"
by (simp add: raise_system_xcpt_def split_beta split: split_if_asm)
- hence "cname_of hp xcp = Xcpt NullPointer"
- by (simp add: system_xcpt_allocated)
+ with prehp have "cname_of hp xcp = Xcpt NullPointer" by simp
with Getfield some_handler phi_pc eff
obtain ST' LT' where
phi': "phi C sig ! handler = Some (ST', LT')" and
@@ -390,9 +389,9 @@
by (simp add: xcpt_eff_def) blast
note phi'
moreover
- { from xcp
+ { from xcp prehp
have "G,hp \<turnstile> xcp ::\<preceq> Class (Xcpt NullPointer)"
- by (simp add: conf_def obj_ty_def system_xcpt_allocated)
+ by (simp add: conf_def obj_ty_def)
moreover
from wf less loc
have "approx_loc G hp loc LT'"
@@ -411,8 +410,7 @@
with some_handler xp'
have xcp: "xcp = Addr (XcptRef NullPointer)"
by (simp add: raise_system_xcpt_def split_beta split: split_if_asm)
- hence "cname_of hp xcp = Xcpt NullPointer"
- by (simp add: system_xcpt_allocated)
+ with prehp have "cname_of hp xcp = Xcpt NullPointer" by simp
with Putfield some_handler phi_pc eff
obtain ST' LT' where
phi': "phi C sig ! handler = Some (ST', LT')" and
@@ -421,9 +419,9 @@
by (simp add: xcpt_eff_def) blast
note phi'
moreover
- { from xcp
+ { from xcp prehp
have "G,hp \<turnstile> xcp ::\<preceq> Class (Xcpt NullPointer)"
- by (simp add: conf_def obj_ty_def system_xcpt_allocated)
+ by (simp add: conf_def obj_ty_def)
moreover
from wf less loc
have "approx_loc G hp loc LT'"
@@ -442,8 +440,7 @@
with some_handler xp'
have xcp: "xcp = Addr (XcptRef ClassCast)"
by (simp add: raise_system_xcpt_def split_beta split: split_if_asm)
- hence "cname_of hp xcp = Xcpt ClassCast"
- by (simp add: system_xcpt_allocated)
+ with prehp have "cname_of hp xcp = Xcpt ClassCast" by simp
with Checkcast some_handler phi_pc eff
obtain ST' LT' where
phi': "phi C sig ! handler = Some (ST', LT')" and
@@ -452,9 +449,9 @@
by (simp add: xcpt_eff_def) blast
note phi'
moreover
- { from xcp
+ { from xcp prehp
have "G,hp \<turnstile> xcp ::\<preceq> Class (Xcpt ClassCast)"
- by (simp add: conf_def obj_ty_def system_xcpt_allocated)
+ by (simp add: conf_def obj_ty_def)
moreover
from wf less loc
have "approx_loc G hp loc LT'"
@@ -702,6 +699,7 @@
hext_upd_obj approx_stk_sup_heap
approx_loc_sup_heap
hconf_field_update
+ preallocated_field_update
correct_frames_field_update conf_widen
dest:
widen_cfs_fields)
@@ -729,6 +727,7 @@
from ins conf meth
obtain ST LT where
heap_ok: "G\<turnstile>h hp\<surd>" and
+ prealloc: "preallocated hp" 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
@@ -775,6 +774,8 @@
have "correct_frames G ?hp' phi rT sig frs"
by - (rule correct_frames_newref,
auto simp add: oconf_def dest: fields_is_type)
+ moreover
+ from hp prealloc have "preallocated ?hp'" by (rule preallocated_newref)
ultimately
show ?thesis
by (simp add: is_class_C meth phi_suc correct_state_def del: not_None_eq)
@@ -809,6 +810,7 @@
from ins method approx
obtain s where
heap_ok: "G\<turnstile>h hp\<surd>" and
+ prealloc:"preallocated hp" and
phi_pc: "phi C sig!pc = Some s" and
is_class_C: "is_class G C" and
frame: "correct_frame G hp s maxl ins (stk, loc, C, sig, pc)" and
@@ -955,7 +957,7 @@
qed
from state'_val heap_ok mD'' ins method phi_pc s X' l mX
- frames s' LT0 c_f is_class_C stk' oX_Addr frame
+ frames s' LT0 c_f is_class_C stk' oX_Addr frame prealloc
show ?thesis by (simp add: correct_state_def) (intro exI conjI, blast)
qed
@@ -1002,6 +1004,7 @@
from correct meth
obtain ST LT where
hp_ok: "G \<turnstile>h hp \<surd>" and
+ alloc: "preallocated hp" and
phi_pc: "phi C sig ! pc = Some (ST, LT)" 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"
@@ -1077,7 +1080,7 @@
show ?thesis by (simp add: correct_frame_def)
qed
- with state' frs' f meth hp_ok hd_stk phi_suc frames' meth' phi' class'
+ with state' frs' f meth hp_ok hd_stk phi_suc frames' meth' phi' class' alloc
have ?thesis by (simp add: correct_state_def)
}
ultimately
@@ -1285,7 +1288,7 @@
apply (auto intro: BV_correct_1)
done
-theorem BV_correct_initial:
+theorem BV_correct_implies_approx:
"[| wt_jvm_prog G phi;
G \<turnstile> s0 -jvm-> (None,hp,(stk,loc,C,sig,pc)#frs); G,phi \<turnstile>JVM s0 \<surd>|]
==> approx_stk G hp stk (fst (the (phi C sig ! pc))) \<and>
--- a/src/HOL/MicroJava/BV/Correct.thy Tue Dec 18 18:37:56 2001 +0100
+++ b/src/HOL/MicroJava/BV/Correct.thy Tue Dec 18 21:28:01 2001 +0100
@@ -1,3 +1,4 @@
+
(* Title: HOL/MicroJava/BV/Correct.thy
ID: $Id$
Author: Cornelia Pusch, Gerwin Klein
@@ -55,7 +56,7 @@
case xp of
None => (case frs of
[] => True
- | (f#fs) => G\<turnstile>h hp\<surd> \<and>
+ | (f#fs) => G\<turnstile>h hp\<surd> \<and> preallocated hp \<and>
(let (stk,loc,C,sig,pc) = f
in
\<exists>rT maxs maxl ins et s.
@@ -262,6 +263,27 @@
simp add: obj_ty_def)
done
+section {* preallocated *}
+
+lemma preallocated_field_update:
+ "\<lbrakk> map_of (fields (G, oT)) X = Some T; hp a = Some(oT,fs);
+ G\<turnstile>h hp\<surd>; preallocated hp \<rbrakk>
+ \<Longrightarrow> preallocated (hp(a \<mapsto> (oT, fs(X\<mapsto>v))))"
+ apply (unfold preallocated_def)
+ apply (rule allI)
+ apply (erule_tac x=x in allE)
+ apply simp
+ apply (rule ccontr)
+ apply (unfold hconf_def)
+ apply (erule allE, erule allE, erule impE, assumption)
+ apply (unfold oconf_def lconf_def)
+ apply (simp del: split_paired_All)
+ done
+
+lemma preallocated_newref:
+ "\<lbrakk> hp oref = None; preallocated hp \<rbrakk> \<Longrightarrow> preallocated (hp(oref\<mapsto>obj))"
+ by (unfold preallocated_def) auto
+
section {* correct-frames *}
lemmas [simp del] = fun_upd_apply
--- a/src/HOL/MicroJava/J/State.thy Tue Dec 18 18:37:56 2001 +0100
+++ b/src/HOL/MicroJava/J/State.thy Tue Dec 18 21:28:01 2001 +0100
@@ -27,14 +27,6 @@
state = "aheap \<times> locals" -- "heap, local parameter including This"
xstate = "xcpt option \<times> state" -- "state including exception information"
-
-text {*
- System exceptions are allocated in all heaps,
- and they don't carry any information other than their type: *}
-axioms
- system_xcpt_allocated: "(hp::aheap) (XcptRef x) = Some (Xcpt x, empty)"
-
-
syntax
heap :: "state => aheap"
locals :: "state => locals"
--- a/src/HOL/MicroJava/JVM/JVMExceptions.thy Tue Dec 18 18:37:56 2001 +0100
+++ b/src/HOL/MicroJava/JVM/JVMExceptions.thy Tue Dec 18 21:28:01 2001 +0100
@@ -49,16 +49,28 @@
| Some handler_pc \<Rightarrow> (None, hp, ([xc], loc, C, sig, handler_pc)#frs)))"
+text {*
+ System exceptions are allocated in all heaps,
+ and they don't carry any information other than their type:
+*}
+constdefs
+ preallocated :: "aheap \<Rightarrow> bool"
+ "preallocated hp \<equiv> \<forall>x. hp (XcptRef x) = Some (Xcpt x, empty)"
+
+lemma preallocated_iff [iff]:
+ "preallocated hp \<Longrightarrow> hp (XcptRef x) = Some (Xcpt x, empty)"
+ by (unfold preallocated_def) fast
lemma cname_of_xcp:
- "raise_system_xcpt b x = Some xcp \<Longrightarrow> cname_of (hp::aheap) xcp = Xcpt x"
+ "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
- have "hp (XcptRef x) = Some (Xcpt x, empty)"
- by (rule system_xcpt_allocated)
+ assume "preallocated hp"
+ hence "hp (XcptRef x) = Some (Xcpt x, empty)" ..
ultimately
show ?thesis by simp
qed