--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Thu Apr 12 12:45:05 2001 +0200
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Thu Apr 12 13:40:15 2001 +0200
@@ -2,7 +2,6 @@
ID: $Id$
Author: Cornelia Pusch
Copyright 1999 Technische Universitaet Muenchen
-
Proof that the specification of the bytecode verifier only admits type safe
programs.
*)
@@ -14,6 +13,8 @@
lemmas defs1 = sup_state_conv correct_state_def correct_frame_def
wt_instr_def step_def
+lemmas widen_rules[intro] = approx_val_widen approx_loc_widen approx_stk_widen
+
lemmas [simp del] = split_paired_All
lemma wt_jvm_prog_impl_wt_instr_cor:
@@ -38,11 +39,7 @@
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
==> G,phi \<turnstile>JVM state'\<surd>"
apply (clarsimp simp add: defs1 map_eq_Cons)
-apply (rule conjI)
- apply (rule approx_loc_imp_approx_val_sup)
- apply simp+
-apply (blast intro: approx_stk_imp_approx_stk_sup
- approx_loc_imp_approx_loc_sup)
+apply (blast intro: approx_loc_imp_approx_val_sup)
done
lemma Store_correct:
@@ -54,10 +51,7 @@
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
==> G,phi \<turnstile>JVM state'\<surd>"
apply (clarsimp simp add: defs1 map_eq_Cons)
-apply (rule conjI)
- apply (blast intro: approx_stk_imp_approx_stk_sup)
-apply (blast intro: approx_loc_imp_approx_loc_subst
- approx_loc_imp_approx_loc_sup)
+apply (blast intro: approx_loc_subst)
done
@@ -68,10 +62,9 @@
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: defs1 approx_val_def sup_PTS_eq map_eq_Cons)
-apply (blast dest: conf_litval intro: conf_widen approx_stk_imp_approx_stk_sup
- approx_loc_imp_approx_loc_sup)
+==> G,phi \<turnstile>JVM state'\<surd>"
+apply (clarsimp simp add: defs1 sup_PTS_eq map_eq_Cons)
+apply (blast dest: conf_litval intro: conf_widen)
done
@@ -81,7 +74,7 @@
==> G,h\<turnstile>v::\<preceq>T"
apply (unfold cast_ok_def)
apply (frule widen_Class)
-apply (elim exE disjE)
+apply (elim exE disjE)
apply (simp add: null)
apply (clarsimp simp add: conf_def obj_ty_def)
apply (cases v)
@@ -97,9 +90,8 @@
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: defs1 map_eq_Cons raise_xcpt_def approx_val_def)
-apply (blast intro: approx_stk_imp_approx_stk_sup
- approx_loc_imp_approx_loc_sup Cast_conf2)
+apply (clarsimp simp add: defs1 map_eq_Cons raise_xcpt_def)
+apply (blast intro: Cast_conf2)
done
@@ -111,18 +103,17 @@
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: defs1 raise_xcpt_def map_eq_Cons approx_val_def
+apply (clarsimp simp add: defs1 raise_xcpt_def map_eq_Cons
split: option.split)
apply (frule conf_widen)
apply assumption+
apply (drule conf_RefTD)
-apply (clarsimp simp add: defs1 approx_val_def)
+apply (clarsimp simp add: defs1)
apply (rule conjI)
apply (drule widen_cfs_fields)
apply assumption+
apply (force intro: conf_widen simp add: hconf_def oconf_def lconf_def)
-apply (blast intro: approx_stk_imp_approx_stk_sup
- approx_loc_imp_approx_loc_sup)
+apply blast
done
lemma Putfield_correct:
@@ -134,19 +125,18 @@
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
==> G,phi \<turnstile>JVM state'\<surd>"
apply (clarsimp simp add: defs1 raise_xcpt_def split: option.split List.split)
-apply (clarsimp simp add: approx_val_def)
apply (frule conf_widen)
prefer 2
-apply assumption
-apply assumption
+ apply assumption
+ apply assumption
apply (drule conf_RefTD)
apply clarsimp
apply (blast
intro:
- hext_upd_obj 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_field_update
- correct_frames_imp_correct_frames_field_update conf_widen
+ hext_upd_obj approx_stk_sup_heap
+ approx_loc_sup_heap
+ hconf_field_update
+ correct_frames_field_update conf_widen
dest:
widen_cfs_fields)
done
@@ -175,8 +165,8 @@
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
@@ -194,10 +184,8 @@
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)
+ 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"
@@ -210,7 +198,7 @@
moreover
from wf hp heap_ok is_class_X
have hp': "G \<turnstile>h ?hp' \<surd>"
- by - (rule hconf_imp_hconf_newref,
+ by - (rule hconf_newref,
auto simp add: oconf_def dest: fields_is_type)
moreover
from hp
@@ -219,15 +207,12 @@
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)
+ apply (blast intro: approx_stk_sup_heap approx_loc_sup_heap 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,
+ by - (rule correct_frames_newref,
auto simp add: oconf_def dest: fields_is_type)
ultimately
have ?thesis
@@ -237,7 +222,6 @@
show ?thesis by auto
qed
-
lemmas [simp del] = split_paired_Ex
lemma Invoke_correct:
@@ -272,13 +256,13 @@
from ins wti phi_pc
obtain apTs X ST LT D' rT body where
- s: "s = (rev apTs @ X # ST, LT)" and
- l: "length apTs = length pTs" and
is_class: "is_class G C'" and
- X: "G\<turnstile> X \<preceq> Class C'" and
- w: "\<forall>x\<in>set (zip apTs pTs). x \<in> widen G" and
- mC': "method (G, C') (mn, pTs) = Some (D', rT, body)" and
- pc: "Suc pc < length ins" and
+ s: "s = (rev apTs @ X # ST, LT)" and
+ l: "length apTs = length pTs" and
+ X: "G\<turnstile> X \<preceq> Class C'" and
+ w: "\<forall>x\<in>set (zip apTs pTs). x \<in> widen G" and
+ mC':"method (G, C') (mn, pTs) = Some (D', rT, body)" and
+ pc: "Suc pc < length ins" and
step: "G \<turnstile> step (Invoke C' mn pTs) G (Some s) <=' phi C sig!Suc pc"
by (simp add: wt_instr_def del: not_None_eq) (elim exE conjE, rule that)
@@ -307,7 +291,7 @@
stk': "stk = opTs @ oX # stk'" and
l_o: "length opTs = length apTs"
"length stk' = length ST"
- by - (drule approx_stk_append_lemma, simp, elim, simp)
+ by - (drule approx_stk_append, simp, elim, simp)
from oX
have "\<exists>T'. typeof (option_map obj_ty \<circ> hp) oX = Some T' \<and> G \<turnstile> T' \<preceq> X"
@@ -322,15 +306,13 @@
by (elim, simp)
from stk' l_o l
- have oX_pos: "last (take (Suc (length pTs)) stk) = oX"
- by simp
+ have oX_pos: "last (take (Suc (length pTs)) stk) = oX" by simp
with state' method ins
have Null_ok: "oX = Null ==> ?thesis"
by (simp add: correct_state_def raise_xcpt_def)
- { fix ref
- assume oX_Addr: "oX = Addr ref"
+ { fix ref assume oX_Addr: "oX = Addr ref"
with oX_Ref
obtain obj where
@@ -424,29 +406,20 @@
have a: "approx_val G hp (Addr ref) (OK (Class D''))"
by (simp add: approx_val_def conf_def)
- from w l
- have "\<forall>x\<in>set (zip (rev apTs) (rev pTs)). x \<in> widen G"
- by (auto simp add: zip_rev)
- with wfprog l l_o opTs
- have "approx_loc G hp opTs (map OK (rev pTs))"
- by (auto intro: assConv_approx_stk_imp_approx_loc)
- hence "approx_stk G hp opTs (rev pTs)"
- by (simp add: approx_stk_def)
- hence "approx_stk G hp (rev opTs) pTs"
- by (simp add: approx_stk_rev)
+ from opTs w l l_o wfprog
+ have "approx_stk G hp opTs (rev pTs)"
+ by (auto elim!: approx_stk_all_widen simp add: zip_rev)
+ hence "approx_stk G hp (rev opTs) pTs" by (subst approx_stk_rev)
with r a l_o l
have "approx_loc G hp (Addr ref # rev opTs @ replicate mxl' arbitrary) ?LT"
(is "approx_loc G hp ?lt ?LT")
by (auto simp add: approx_loc_append approx_stk_def)
- from wfprog this sup_loc
- have "approx_loc G hp ?lt LT0"
- by (rule approx_loc_imp_approx_loc_sup)
-
+ from this sup_loc wfprog
+ have "approx_loc G hp ?lt LT0" by (rule approx_loc_widen)
with start l_o l
- show ?thesis
- by (simp add: correct_frame_def)
+ show ?thesis by (simp add: correct_frame_def)
qed
have c_f': "correct_frame G hp (tl ST', LT') maxl ins ?f'"
@@ -456,28 +429,26 @@
by (simp add: step_def sup_state_conv)
with wfprog a_loc
have a: "approx_loc G hp loc LT'"
- by (rule approx_loc_imp_approx_loc_sup)
+ by - (rule approx_loc_widen)
moreover
from s s' mC' step l
have "G \<turnstile> map OK ST <=l map OK (tl ST')"
by (auto simp add: step_def sup_state_conv map_eq_Cons)
with wfprog a_stk'
have "approx_stk G hp stk' (tl ST')"
- by (rule approx_stk_imp_approx_stk_sup)
+ by - (rule approx_stk_widen)
ultimately
- show ?thesis
- by (simp add: correct_frame_def suc_l pc)
+ show ?thesis by (simp add: correct_frame_def suc_l pc)
qed
with state'_val heap_ok mD'' ins method phi_pc s X' l
frames s' LT0 c_f c_f' is_class_C
- have ?thesis
- by (simp add: correct_state_def) (intro exI conjI, force+)
+ have ?thesis
+ by (simp add: correct_state_def) (intro exI conjI, blast, assumption+)
}
with Null_ok oX_Ref
- show "G,phi \<turnstile>JVM state'\<surd>"
- by - (cases oX, auto)
+ show "G,phi \<turnstile>JVM state'\<surd>" by - (cases oX, auto)
qed
lemmas [simp del] = map_append
@@ -493,12 +464,14 @@
apply (clarsimp simp add: neq_Nil_conv defs1 split: split_if_asm iff del: not_None_eq)
apply (frule wt_jvm_prog_impl_wt_instr)
apply (assumption, assumption, erule Suc_lessD)
+apply (clarsimp simp add: map_eq_Cons append_eq_conv_conj defs1)
apply (unfold wt_jvm_prog_def)
-apply (fastsimp
- dest: subcls_widen_methd
- elim: widen_trans [COMP swap_prems_rl]
- intro: conf_widen
- simp: approx_val_def append_eq_conv_conj map_eq_Cons defs1)
+apply (frule subcls_widen_methd, assumption+)
+apply clarify
+apply simp
+apply (erule conf_widen, assumption)
+apply (erule widen_trans)+
+apply blast
done
lemmas [simp] = map_append
@@ -512,8 +485,7 @@
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
==> G,phi \<turnstile>JVM state'\<surd>"
apply (clarsimp simp add: defs1)
-apply (fast intro: approx_loc_imp_approx_loc_sup
- approx_stk_imp_approx_stk_sup)
+apply fast
done
@@ -526,8 +498,7 @@
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
==> G,phi \<turnstile>JVM state'\<surd>"
apply (clarsimp simp add: defs1)
-apply (fast intro: approx_loc_imp_approx_loc_sup
- approx_stk_imp_approx_stk_sup)
+apply fast
done
lemma Pop_correct:
@@ -539,8 +510,7 @@
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
==> G,phi \<turnstile>JVM state'\<surd>"
apply (clarsimp simp add: defs1)
-apply (fast intro: approx_loc_imp_approx_loc_sup
- approx_stk_imp_approx_stk_sup)
+apply fast
done
lemma Dup_correct:
@@ -552,10 +522,7 @@
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
==> G,phi \<turnstile>JVM state'\<surd>"
apply (clarsimp simp add: defs1 map_eq_Cons)
-apply (force intro: approx_stk_imp_approx_stk_sup
- approx_val_imp_approx_val_sup
- approx_loc_imp_approx_loc_sup
- simp add: defs1 map_eq_Cons)
+apply (blast intro: conf_widen)
done
lemma Dup_x1_correct:
@@ -567,10 +534,7 @@
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
==> G,phi \<turnstile>JVM state'\<surd>"
apply (clarsimp simp add: defs1 map_eq_Cons)
-apply (force intro: approx_stk_imp_approx_stk_sup
- approx_val_imp_approx_val_sup
- approx_loc_imp_approx_loc_sup
- simp add: defs1 map_eq_Cons)
+apply (blast intro: conf_widen)
done
lemma Dup_x2_correct:
@@ -582,10 +546,7 @@
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
==> G,phi \<turnstile>JVM state'\<surd>"
apply (clarsimp simp add: defs1 map_eq_Cons)
-apply (force intro: approx_stk_imp_approx_stk_sup
- approx_val_imp_approx_val_sup
- approx_loc_imp_approx_loc_sup
- simp add: defs1 map_eq_Cons)
+apply (blast intro: conf_widen)
done
lemma Swap_correct:
@@ -597,10 +558,7 @@
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
==> G,phi \<turnstile>JVM state'\<surd>"
apply (clarsimp simp add: defs1 map_eq_Cons)
-apply (force intro: approx_stk_imp_approx_stk_sup
- approx_val_imp_approx_val_sup
- approx_loc_imp_approx_loc_sup
- simp add: defs1 map_eq_Cons)
+apply (blast intro: conf_widen)
done
lemma IAdd_correct:
@@ -612,9 +570,7 @@
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
==> G,phi \<turnstile>JVM state'\<surd>"
apply (clarsimp simp add: defs1 map_eq_Cons approx_val_def conf_def)
-apply (blast intro: approx_stk_imp_approx_stk_sup
- approx_val_imp_approx_val_sup
- approx_loc_imp_approx_loc_sup)
+apply blast
done
@@ -650,7 +606,6 @@
apply (rule Ifcmpeq_correct, assumption+)
done
-
section {* Main *}
lemma correct_state_impl_Some_method:
--- a/src/HOL/MicroJava/BV/Correct.thy Thu Apr 12 12:45:05 2001 +0200
+++ b/src/HOL/MicroJava/BV/Correct.thy Thu Apr 12 13:40:15 2001 +0200
@@ -10,6 +10,12 @@
theory Correct = BVSpec:
+lemma list_all2_rev [simp]:
+ "list_all2 P (rev l) (rev l') = list_all2 P l l'"
+ apply (unfold list_all2_def)
+ apply (simp add: zip_rev cong: conj_cong)
+ done
+
constdefs
approx_val :: "[jvm_prog,aheap,val,ty err] => bool"
"approx_val G h v any == case any of Err => True | OK T => G,h\<turnstile>v::\<preceq>T"
@@ -32,7 +38,7 @@
"correct_frames G hp phi rT0 sig0 [] = True"
"correct_frames G hp phi rT0 sig0 (f#frs) =
- (let (stk,loc,C,sig,pc) = f in
+ (let (stk,loc,C,sig,pc) = f in
(\<exists>ST LT rT maxs maxl ins.
phi C sig ! pc = Some (ST,LT) \<and> is_class G C \<and>
method (G,C) sig = Some(C,rT,(maxs,maxl,ins)) \<and>
@@ -71,254 +77,248 @@
correct_state :: "[jvm_prog,prog_type,jvm_state] => bool"
("_,_ |-JVM _ [ok]" [51,51] 50)
+
+lemma sup_ty_opt_OK:
+ "(G \<turnstile> X <=o (OK T')) = (\<exists>T. X = OK T \<and> G \<turnstile> T \<preceq> T')"
+ apply (cases X)
+ apply auto
+ done
+
+
section {* approx-val *}
-lemma approx_val_Err:
+lemma approx_val_Err [simp,intro!]:
"approx_val G hp x Err"
-by (simp add: approx_val_def)
-
-lemma approx_val_Null:
- "approx_val G hp Null (OK (RefT x))"
-by (auto intro: null simp add: approx_val_def)
+ by (simp add: approx_val_def)
-lemma approx_val_imp_approx_val_assConvertible [rule_format]:
- "wf_prog wt G ==> approx_val G hp v (OK T) --> G\<turnstile> T\<preceq>T'
- --> approx_val G hp v (OK T')"
-by (cases T) (auto intro: conf_widen simp add: approx_val_def)
+lemma approx_val_OK [iff]:
+ "approx_val G hp x (OK T) = (G,hp \<turnstile> x ::\<preceq> T)"
+ by (simp add: approx_val_def)
-lemma approx_val_imp_approx_val_sup_heap [rule_format]:
- "approx_val G hp v at --> hp \<le>| hp' --> approx_val G hp' v at"
-apply (simp add: approx_val_def split: err.split)
-apply (blast intro: conf_hext)
-done
+lemma approx_val_Null [simp,intro!]:
+ "approx_val G hp Null (OK (RefT x))"
+ by (auto simp add: approx_val_def)
-lemma approx_val_imp_approx_val_heap_update:
- "[|hp a = Some obj'; G,hp\<turnstile> v::\<preceq>T; obj_ty obj = obj_ty obj'|]
- ==> G,hp(a\<mapsto>obj)\<turnstile> v::\<preceq>T"
-by (cases v, auto simp add: obj_ty_def conf_def)
+lemma approx_val_sup_heap:
+ "\<lbrakk> approx_val G hp v T; hp \<le>| hp' \<rbrakk> \<Longrightarrow> approx_val G hp' v T"
+ by (cases T) (blast intro: conf_hext)+
-lemma approx_val_imp_approx_val_sup [rule_format]:
- "wf_prog wt G ==> (approx_val G h v us) --> (G \<turnstile> us <=o us')
- --> (approx_val G h v us')"
-apply (simp add: sup_PTS_eq approx_val_def split: err.split)
-apply (blast intro: conf_widen)
-done
+lemma approx_val_heap_update:
+ "[| hp a = Some obj'; G,hp\<turnstile> v::\<preceq>T; obj_ty obj = obj_ty obj'|]
+ ==> G,hp(a\<mapsto>obj)\<turnstile> v::\<preceq>T"
+ by (cases v, auto simp add: obj_ty_def conf_def)
-lemma approx_loc_imp_approx_val_sup:
- "[| wf_prog wt G; approx_loc G hp loc LT; idx < length LT;
- v = loc!idx; G \<turnstile> LT!idx <=o at |]
- ==> approx_val G hp v at"
-apply (unfold approx_loc_def)
-apply (unfold list_all2_def)
-apply (auto intro: approx_val_imp_approx_val_sup
- simp add: split_def all_set_conv_all_nth)
-done
-
+lemma approx_val_widen:
+ "\<lbrakk> approx_val G hp v T; G \<turnstile> T <=o T'; wf_prog wt G \<rbrakk>
+ \<Longrightarrow> approx_val G hp v T'"
+ by (cases T', auto simp add: sup_ty_opt_OK intro: conf_widen)
section {* approx-loc *}
+lemma approx_loc_Nil [simp,intro!]:
+ "approx_loc G hp [] []"
+ by (simp add: approx_loc_def)
+
lemma approx_loc_Cons [iff]:
- "approx_loc G hp (s#xs) (l#ls) =
- (approx_val G hp s l \<and> approx_loc G hp xs ls)"
+ "approx_loc G hp (l#ls) (L#LT) =
+ (approx_val G hp l L \<and> approx_loc G hp ls LT)"
by (simp add: approx_loc_def)
-lemma assConv_approx_stk_imp_approx_loc [rule_format]:
- "wf_prog wt G ==> (\<forall>tt'\<in>set (zip tys_n ts). tt' \<in> widen G)
- --> length tys_n = length ts --> approx_stk G hp s tys_n -->
- approx_loc G hp s (map OK ts)"
-apply (unfold approx_stk_def approx_loc_def list_all2_def)
-apply (clarsimp simp add: all_set_conv_all_nth)
-apply (rule approx_val_imp_approx_val_assConvertible)
-apply auto
+lemma approx_loc_nth:
+ "\<lbrakk> approx_loc G hp loc LT; n < length LT \<rbrakk>
+ \<Longrightarrow> approx_val G hp (loc!n) (LT!n)"
+ by (simp add: approx_loc_def list_all2_conv_all_nth)
+
+lemma approx_loc_imp_approx_val_sup:
+ "\<lbrakk>approx_loc G hp loc LT; n < length LT; LT ! n = OK T; G \<turnstile> T \<preceq> T'; wf_prog wt G\<rbrakk>
+ \<Longrightarrow> G,hp \<turnstile> (loc!n) ::\<preceq> T'"
+ apply (drule approx_loc_nth, assumption)
+ apply simp
+ apply (erule conf_widen, assumption+)
+ done
+
+lemma approx_loc_conv_all_nth:
+ "approx_loc G hp loc LT =
+ (length loc = length LT \<and> (\<forall>n < length loc. approx_val G hp (loc!n) (LT!n)))"
+ by (simp add: approx_loc_def list_all2_conv_all_nth)
+
+lemma approx_loc_sup_heap:
+ "\<lbrakk> approx_loc G hp loc LT; hp \<le>| hp' \<rbrakk>
+ \<Longrightarrow> approx_loc G hp' loc LT"
+ apply (clarsimp simp add: approx_loc_conv_all_nth)
+ apply (blast intro: approx_val_sup_heap)
+ done
+
+lemma approx_loc_widen:
+ "\<lbrakk> approx_loc G hp loc LT; G \<turnstile> LT <=l LT'; wf_prog wt G \<rbrakk>
+ \<Longrightarrow> approx_loc G hp loc LT'"
+apply (unfold Listn.le_def lesub_def sup_loc_def)
+apply (simp (no_asm_use) only: list_all2_conv_all_nth approx_loc_conv_all_nth)
+apply (simp (no_asm_simp))
+apply clarify
+apply (erule allE, erule impE)
+ apply simp
+apply (erule approx_val_widen)
+ apply simp
+apply assumption
done
-
-lemma approx_loc_imp_approx_loc_sup_heap [rule_format]:
- "\<forall>lvars. approx_loc G hp lvars lt --> hp \<le>| hp'
- --> approx_loc G hp' lvars lt"
-apply (unfold approx_loc_def list_all2_def)
-apply (cases lt)
- apply simp
-apply clarsimp
-apply (rule approx_val_imp_approx_val_sup_heap)
-apply auto
-done
-
-lemma approx_loc_imp_approx_loc_sup [rule_format]:
- "wf_prog wt G ==> approx_loc G hp lvars lt --> G \<turnstile> lt <=l lt'
- --> approx_loc G hp lvars lt'"
-apply (unfold Listn.le_def lesub_def sup_loc_def approx_loc_def list_all2_def)
-apply (auto simp add: all_set_conv_all_nth)
-apply (auto elim: approx_val_imp_approx_val_sup)
-done
-
-
-lemma approx_loc_imp_approx_loc_subst [rule_format]:
- "\<forall>loc idx x X. (approx_loc G hp loc LT) --> (approx_val G hp x X)
- --> (approx_loc G hp (loc[idx:=x]) (LT[idx:=X]))"
+lemma approx_loc_subst:
+ "\<lbrakk> approx_loc G hp loc LT; approx_val G hp x X \<rbrakk>
+ \<Longrightarrow> approx_loc G hp (loc[idx:=x]) (LT[idx:=X])"
apply (unfold approx_loc_def list_all2_def)
apply (auto dest: subsetD [OF set_update_subset_insert] simp add: zip_update)
done
-
-lemmas [cong] = conj_cong
-
-lemma approx_loc_append [rule_format]:
- "\<forall>L1 l2 L2. length l1=length L1 -->
+lemma approx_loc_append:
+ "length l1=length L1 \<Longrightarrow>
approx_loc G hp (l1@l2) (L1@L2) =
(approx_loc G hp l1 L1 \<and> approx_loc G hp l2 L2)"
-apply (unfold approx_loc_def list_all2_def)
-apply simp
-apply blast
-done
-
-lemmas [cong del] = conj_cong
-
+ apply (unfold approx_loc_def list_all2_def)
+ apply (simp cong: conj_cong)
+ apply blast
+ done
section {* approx-stk *}
lemma approx_stk_rev_lem:
"approx_stk G hp (rev s) (rev t) = approx_stk G hp s t"
-apply (unfold approx_stk_def approx_loc_def list_all2_def)
-apply (auto simp add: zip_rev sym [OF rev_map])
-done
+ apply (unfold approx_stk_def approx_loc_def)
+ apply (simp add: rev_map [THEN sym])
+ done
lemma approx_stk_rev:
"approx_stk G hp (rev s) t = approx_stk G hp s (rev t)"
-by (auto intro: subst [OF approx_stk_rev_lem])
-
+ by (auto intro: subst [OF approx_stk_rev_lem])
-lemma approx_stk_imp_approx_stk_sup_heap [rule_format]:
- "\<forall>lvars. approx_stk G hp lvars lt --> hp \<le>| hp'
- --> approx_stk G hp' lvars lt"
-by (auto intro: approx_loc_imp_approx_loc_sup_heap simp add: approx_stk_def)
+lemma approx_stk_sup_heap:
+ "\<lbrakk> approx_stk G hp stk ST; hp \<le>| hp' \<rbrakk> \<Longrightarrow> approx_stk G hp' stk ST"
+ by (auto intro: approx_loc_sup_heap simp add: approx_stk_def)
-lemma approx_stk_imp_approx_stk_sup [rule_format]:
- "wf_prog wt G ==> approx_stk G hp lvars st --> (G \<turnstile> map OK st <=l (map OK st'))
- --> approx_stk G hp lvars st'"
-by (auto intro: approx_loc_imp_approx_loc_sup simp add: approx_stk_def)
+lemma approx_stk_widen:
+ "\<lbrakk> approx_stk G hp stk ST; G \<turnstile> map OK ST <=l map OK ST'; wf_prog wt G \<rbrakk>
+ \<Longrightarrow> approx_stk G hp stk ST'"
+ by (auto elim: approx_loc_widen simp add: approx_stk_def)
lemma approx_stk_Nil [iff]:
"approx_stk G hp [] []"
-by (simp add: approx_stk_def approx_loc_def)
+ by (simp add: approx_stk_def)
lemma approx_stk_Cons [iff]:
- "approx_stk G hp (x # stk) (S#ST) =
- (approx_val G hp x (OK S) \<and> approx_stk G hp stk ST)"
-by (simp add: approx_stk_def approx_loc_def)
+ "approx_stk G hp (x#stk) (S#ST) =
+ (approx_val G hp x (OK S) \<and> approx_stk G hp stk ST)"
+ by (simp add: approx_stk_def)
lemma approx_stk_Cons_lemma [iff]:
"approx_stk G hp stk (S#ST') =
(\<exists>s stk'. stk = s#stk' \<and> approx_val G hp s (OK S) \<and> approx_stk G hp stk' ST')"
-by (simp add: list_all2_Cons2 approx_stk_def approx_loc_def)
+ by (simp add: list_all2_Cons2 approx_stk_def approx_loc_def)
+
+lemma approx_stk_append:
+ "approx_stk G hp stk (S@S') \<Longrightarrow>
+ (\<exists>s stk'. stk = s@stk' \<and> length s = length S \<and> length stk' = length S' \<and>
+ approx_stk G hp s S \<and> approx_stk G hp stk' S')"
+ by (simp add: list_all2_append2 approx_stk_def approx_loc_def)
-lemma approx_stk_append_lemma:
- "approx_stk G hp stk (S@ST') ==>
- (\<exists>s stk'. stk = s@stk' \<and> length s = length S \<and> length stk' = length ST' \<and>
- approx_stk G hp s S \<and> approx_stk G hp stk' ST')"
-by (simp add: list_all2_append2 approx_stk_def approx_loc_def)
-
+lemma approx_stk_all_widen:
+ "\<lbrakk> approx_stk G hp stk ST; \<forall>x \<in> set (zip ST ST'). x \<in> widen G; length ST = length ST'; wf_prog wt G \<rbrakk>
+ \<Longrightarrow> approx_stk G hp stk ST'"
+apply (unfold approx_stk_def)
+apply (clarsimp simp add: approx_loc_conv_all_nth all_set_conv_all_nth)
+apply (erule allE, erule impE, assumption)
+apply (erule allE, erule impE, assumption)
+apply (erule conf_widen, assumption+)
+done
section {* oconf *}
-lemma correct_init_obj:
- "[|is_class G C; wf_prog wt G|] ==>
- G,h \<turnstile> (C, map_of (map (\<lambda>(f,fT).(f,default_val fT)) (fields(G,C)))) \<surd>"
-apply (unfold oconf_def lconf_def)
-apply (simp add: map_of_map)
-apply (force intro: defval_conf dest: map_of_SomeD fields_is_type)
-done
-
-
-lemma oconf_imp_oconf_field_update [rule_format]:
+lemma oconf_field_update:
"[|map_of (fields (G, oT)) FD = Some T; G,hp\<turnstile>v::\<preceq>T; G,hp\<turnstile>(oT,fs)\<surd> |]
==> 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 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 hext_new)
-done
+ by (simp add: oconf_def lconf_def)
-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>"
-apply (unfold oconf_def lconf_def)
-apply simp
-apply (force intro: approx_val_imp_approx_val_heap_update)
-done
+lemma oconf_newref:
+ "\<lbrakk>hp oref = None; G,hp \<turnstile> obj \<surd>; G,hp \<turnstile> obj' \<surd>\<rbrakk> \<Longrightarrow> G,hp(oref\<mapsto>obj') \<turnstile> obj \<surd>"
+ apply (unfold oconf_def lconf_def)
+ apply simp
+ apply (blast intro: conf_hext hext_new)
+ done
+lemma oconf_heap_update:
+ "\<lbrakk> hp a = Some obj'; obj_ty obj' = obj_ty obj''; G,hp\<turnstile>obj\<surd> \<rbrakk>
+ \<Longrightarrow> G,hp(a\<mapsto>obj'')\<turnstile>obj\<surd>"
+ apply (unfold oconf_def lconf_def)
+ apply (fastsimp intro: approx_val_heap_update)
+ done
section {* hconf *}
-lemma hconf_imp_hconf_newref [rule_format]:
- "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
+lemma hconf_newref:
+ "\<lbrakk> hp oref = None; G\<turnstile>h hp\<surd>; G,hp\<turnstile>obj\<surd> \<rbrakk> \<Longrightarrow> G\<turnstile>h hp(oref\<mapsto>obj)\<surd>"
+ apply (simp add: hconf_def)
+ apply (fast intro: oconf_newref)
+ done
-lemma hconf_imp_hconf_field_update [rule_format]:
- "map_of (fields (G, oT)) (F, D) = Some T \<and> hp oloc = Some(oT,fs) \<and>
- G,hp\<turnstile>v::\<preceq>T \<and> G\<turnstile>h hp\<surd> --> G\<turnstile>h hp(oloc \<mapsto> (oT, fs((F,D)\<mapsto>v)))\<surd>"
-apply (simp add: hconf_def)
-apply (force intro: oconf_imp_oconf_heap_update oconf_imp_oconf_field_update
- simp add: obj_ty_def)
-done
+lemma hconf_field_update:
+ "\<lbrakk> map_of (fields (G, oT)) X = Some T; hp a = Some(oT,fs);
+ G,hp\<turnstile>v::\<preceq>T; G\<turnstile>h hp\<surd> \<rbrakk>
+ \<Longrightarrow> G\<turnstile>h hp(a \<mapsto> (oT, fs(X\<mapsto>v)))\<surd>"
+ apply (simp add: hconf_def)
+ apply (fastsimp intro: oconf_heap_update oconf_field_update
+ simp add: obj_ty_def)
+ done
section {* correct-frames *}
lemmas [simp del] = fun_upd_apply
-lemma correct_frames_imp_correct_frames_field_update [rule_format]:
- "\<forall>rT C sig. correct_frames G hp phi rT sig frs -->
- hp a = Some (C,od) --> map_of (fields (G, C)) fl = Some fd -->
+lemma correct_frames_field_update [rule_format]:
+ "\<forall>rT C sig.
+ correct_frames G hp phi rT sig frs -->
+ hp a = Some (C,fs) -->
+ map_of (fields (G, C)) fl = Some fd -->
G,hp\<turnstile>v::\<preceq>fd
- --> correct_frames G (hp(a \<mapsto> (C, od(fl\<mapsto>v)))) phi rT sig frs";
+ --> correct_frames G (hp(a \<mapsto> (C, fs(fl\<mapsto>v)))) phi rT sig frs";
apply (induct frs)
apply simp
apply clarify
-apply simp
+apply (simp (no_asm_use))
apply clarify
apply (unfold correct_frame_def)
apply (simp (no_asm_use))
-apply clarsimp
+apply clarify
apply (intro exI conjI)
- apply simp
- apply simp
- apply force
- apply simp
- apply (rule approx_stk_imp_approx_stk_sup_heap)
- apply simp
- apply (rule hext_upd_obj)
- apply simp
-apply (rule approx_loc_imp_approx_loc_sup_heap)
- apply simp
-apply (rule hext_upd_obj)
-apply simp
+ apply assumption+
+ apply (erule approx_stk_sup_heap)
+ apply (erule hext_upd_obj)
+ apply (erule approx_loc_sup_heap)
+ apply (erule hext_upd_obj)
+ apply assumption+
+apply blast
done
-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(x \<mapsto> obj)) phi rT sig frs"
+lemma correct_frames_newref [rule_format]:
+ "\<forall>rT C sig.
+ hp x = None \<longrightarrow>
+ correct_frames G hp phi rT sig frs \<longrightarrow>
+ G,hp \<turnstile> obj \<surd>
+ \<longrightarrow> correct_frames G (hp(x \<mapsto> obj)) phi rT sig frs"
apply (induct frs)
apply simp
-apply (clarsimp simp add: correct_frame_def)
+apply clarify
+apply (simp (no_asm_use))
+apply clarify
+apply (unfold correct_frame_def)
+apply (simp (no_asm_use))
+apply clarify
apply (intro exI conjI)
- apply simp
- apply simp
- apply force
- apply simp
- apply (rule approx_stk_imp_approx_stk_sup_heap)
- apply simp
- apply (rule hext_new)
- apply simp
-apply (rule approx_loc_imp_approx_loc_sup_heap)
- apply simp
-apply (rule hext_new)
-apply simp
+ apply assumption+
+ apply (erule approx_stk_sup_heap)
+ apply (erule hext_new)
+ apply (erule approx_loc_sup_heap)
+ apply (erule hext_new)
+ apply assumption+
+apply blast
done
end
-