author  kleing 
Sun, 27 Oct 2002 23:34:02 +0100  
changeset 13681  06cce9be31a4 
parent 13052  3bf41c474a88 
child 16417  9bc16273c2d4 
permissions  rwrr 
12545
7319d384d0d3
removed preallocated heaps axiom (now in type safety invariant)
kleing
parents:
12516
diff
changeset

1 

8011  2 
(* Title: HOL/MicroJava/BV/Correct.thy 
3 
ID: $Id$ 

12516  4 
Author: Cornelia Pusch, Gerwin Klein 
8011  5 
Copyright 1999 Technische Universitaet Muenchen 
6 

7 
The invariant for the type safety proof. 

8 
*) 

9 

12911  10 
header {* \isaheader{BV Type Safety Invariant} *} 
9757
1024a2d80ac0
functional LBV style, dead code, type safety > Isar
kleing
parents:
9549
diff
changeset

11 

12774  12 
theory Correct = BVSpec + JVMExec: 
8011  13 

14 
constdefs 

13006  15 
approx_val :: "[jvm_prog,aheap,val,ty err] \<Rightarrow> bool" 
16 
"approx_val G h v any == case any of Err \<Rightarrow> True  OK T \<Rightarrow> G,h\<turnstile>v::\<preceq>T" 

8011  17 

13006  18 
approx_loc :: "[jvm_prog,aheap,val list,locvars_type] \<Rightarrow> bool" 
10056  19 
"approx_loc G hp loc LT == list_all2 (approx_val G hp) loc LT" 
20 

13006  21 
approx_stk :: "[jvm_prog,aheap,opstack,opstack_type] \<Rightarrow> bool" 
10496  22 
"approx_stk G hp stk ST == approx_loc G hp stk (map OK ST)" 
9757
1024a2d80ac0
functional LBV style, dead code, type safety > Isar
kleing
parents:
9549
diff
changeset

23 

13006  24 
correct_frame :: "[jvm_prog,aheap,state_type,nat,bytecode] \<Rightarrow> frame \<Rightarrow> bool" 
10056  25 
"correct_frame G hp == \<lambda>(ST,LT) maxl ins (stk,loc,C,sig,pc). 
26 
approx_stk G hp stk ST \<and> approx_loc G hp loc LT \<and> 

27 
pc < length ins \<and> length loc=length(snd sig)+maxl+1" 

8011  28 

29 

30 
consts 

13006  31 
correct_frames :: "[jvm_prog,aheap,prog_type,ty,sig,frame list] \<Rightarrow> bool" 
8011  32 
primrec 
8045
816f566c414f
Fixed a problem with returning from the last frame.
nipkow
parents:
8034
diff
changeset

33 
"correct_frames G hp phi rT0 sig0 [] = True" 
8011  34 

8045
816f566c414f
Fixed a problem with returning from the last frame.
nipkow
parents:
8034
diff
changeset

35 
"correct_frames G hp phi rT0 sig0 (f#frs) = 
11252  36 
(let (stk,loc,C,sig,pc) = f in 
12516  37 
(\<exists>ST LT rT maxs maxl ins et. 
10625
022c6b2bcd6b
strengthened invariant: current class must be defined
kleing
parents:
10612
diff
changeset

38 
phi C sig ! pc = Some (ST,LT) \<and> is_class G C \<and> 
12516  39 
method (G,C) sig = Some(C,rT,(maxs,maxl,ins,et)) \<and> 
40 
(\<exists>C' mn pTs. ins!pc = (Invoke C' mn pTs) \<and> 

9757
1024a2d80ac0
functional LBV style, dead code, type safety > Isar
kleing
parents:
9549
diff
changeset

41 
(mn,pTs) = sig0 \<and> 
1024a2d80ac0
functional LBV style, dead code, type safety > Isar
kleing
parents:
9549
diff
changeset

42 
(\<exists>apTs D ST' LT'. 
12516  43 
(phi C sig)!pc = Some ((rev apTs) @ (Class D) # ST', LT') \<and> 
9757
1024a2d80ac0
functional LBV style, dead code, type safety > Isar
kleing
parents:
9549
diff
changeset

44 
length apTs = length pTs \<and> 
12516  45 
(\<exists>D' rT' maxs' maxl' ins' et'. 
46 
method (G,D) sig0 = Some(D',rT',(maxs',maxl',ins',et')) \<and> 

9757
1024a2d80ac0
functional LBV style, dead code, type safety > Isar
kleing
parents:
9549
diff
changeset

47 
G \<turnstile> rT0 \<preceq> rT') \<and> 
12516  48 
correct_frame G hp (ST, LT) maxl ins f \<and> 
49 
correct_frames G hp phi rT sig frs))))" 

8011  50 

51 

52 
constdefs 

13006  53 
correct_state :: "[jvm_prog,prog_type,jvm_state] \<Rightarrow> bool" 
11372  54 
("_,_ JVM _ [ok]" [51,51] 50) 
10042  55 
"correct_state G phi == \<lambda>(xp,hp,frs). 
8011  56 
case xp of 
13006  57 
None \<Rightarrow> (case frs of 
58 
[] \<Rightarrow> True 

59 
 (f#fs) \<Rightarrow> G\<turnstile>h hp\<surd> \<and> preallocated hp \<and> 

12516  60 
(let (stk,loc,C,sig,pc) = f 
61 
in 

62 
\<exists>rT maxs maxl ins et s. 

10625
022c6b2bcd6b
strengthened invariant: current class must be defined
kleing
parents:
10612
diff
changeset

63 
is_class G C \<and> 
12516  64 
method (G,C) sig = Some(C,rT,(maxs,maxl,ins,et)) \<and> 
9757
1024a2d80ac0
functional LBV style, dead code, type safety > Isar
kleing
parents:
9549
diff
changeset

65 
phi C sig ! pc = Some s \<and> 
12516  66 
correct_frame G hp s maxl ins f \<and> 
67 
correct_frames G hp phi rT sig fs)) 

13006  68 
 Some x \<Rightarrow> frs = []" 
9757
1024a2d80ac0
functional LBV style, dead code, type safety > Isar
kleing
parents:
9549
diff
changeset

69 

1024a2d80ac0
functional LBV style, dead code, type safety > Isar
kleing
parents:
9549
diff
changeset

70 

11372  71 
syntax (xsymbols) 
13006  72 
correct_state :: "[jvm_prog,prog_type,jvm_state] \<Rightarrow> bool" 
11372  73 
("_,_ \<turnstile>JVM _ \<surd>" [51,51] 50) 
10060  74 

11252  75 

76 
lemma sup_ty_opt_OK: 

77 
"(G \<turnstile> X <=o (OK T')) = (\<exists>T. X = OK T \<and> G \<turnstile> T \<preceq> T')" 

78 
apply (cases X) 

79 
apply auto 

80 
done 

81 

82 

11085  83 
section {* approxval *} 
9757
1024a2d80ac0
functional LBV style, dead code, type safety > Isar
kleing
parents:
9549
diff
changeset

84 

11252  85 
lemma approx_val_Err [simp,intro!]: 
9757
1024a2d80ac0
functional LBV style, dead code, type safety > Isar
kleing
parents:
9549
diff
changeset

86 
"approx_val G hp x Err" 
11252  87 
by (simp add: approx_val_def) 
9757
1024a2d80ac0
functional LBV style, dead code, type safety > Isar
kleing
parents:
9549
diff
changeset

88 

11252  89 
lemma approx_val_OK [iff]: 
90 
"approx_val G hp x (OK T) = (G,hp \<turnstile> x ::\<preceq> T)" 

91 
by (simp add: approx_val_def) 

9757
1024a2d80ac0
functional LBV style, dead code, type safety > Isar
kleing
parents:
9549
diff
changeset

92 

11252  93 
lemma approx_val_Null [simp,intro!]: 
94 
"approx_val G hp Null (OK (RefT x))" 

95 
by (auto simp add: approx_val_def) 

9757
1024a2d80ac0
functional LBV style, dead code, type safety > Isar
kleing
parents:
9549
diff
changeset

96 

11252  97 
lemma approx_val_sup_heap: 
98 
"\<lbrakk> approx_val G hp v T; hp \<le> hp' \<rbrakk> \<Longrightarrow> approx_val G hp' v T" 

99 
by (cases T) (blast intro: conf_hext)+ 

9757
1024a2d80ac0
functional LBV style, dead code, type safety > Isar
kleing
parents:
9549
diff
changeset

100 

11252  101 
lemma approx_val_heap_update: 
13006  102 
"\<lbrakk> hp a = Some obj'; G,hp\<turnstile> v::\<preceq>T; obj_ty obj = obj_ty obj'\<rbrakk> 
103 
\<Longrightarrow> G,hp(a\<mapsto>obj)\<turnstile> v::\<preceq>T" 

11252  104 
by (cases v, auto simp add: obj_ty_def conf_def) 
9757
1024a2d80ac0
functional LBV style, dead code, type safety > Isar
kleing
parents:
9549
diff
changeset

105 

11252  106 
lemma approx_val_widen: 
107 
"\<lbrakk> approx_val G hp v T; G \<turnstile> T <=o T'; wf_prog wt G \<rbrakk> 

108 
\<Longrightarrow> approx_val G hp v T'" 

109 
by (cases T', auto simp add: sup_ty_opt_OK intro: conf_widen) 

9757
1024a2d80ac0
functional LBV style, dead code, type safety > Isar
kleing
parents:
9549
diff
changeset

110 

11085  111 
section {* approxloc *} 
9757
1024a2d80ac0
functional LBV style, dead code, type safety > Isar
kleing
parents:
9549
diff
changeset

112 

11252  113 
lemma approx_loc_Nil [simp,intro!]: 
114 
"approx_loc G hp [] []" 

115 
by (simp add: approx_loc_def) 

116 

9757
1024a2d80ac0
functional LBV style, dead code, type safety > Isar
kleing
parents:
9549
diff
changeset

117 
lemma approx_loc_Cons [iff]: 
11252  118 
"approx_loc G hp (l#ls) (L#LT) = 
119 
(approx_val G hp l L \<and> approx_loc G hp ls LT)" 

9757
1024a2d80ac0
functional LBV style, dead code, type safety > Isar
kleing
parents:
9549
diff
changeset

120 
by (simp add: approx_loc_def) 
1024a2d80ac0
functional LBV style, dead code, type safety > Isar
kleing
parents:
9549
diff
changeset

121 

11252  122 
lemma approx_loc_nth: 
123 
"\<lbrakk> approx_loc G hp loc LT; n < length LT \<rbrakk> 

124 
\<Longrightarrow> approx_val G hp (loc!n) (LT!n)" 

125 
by (simp add: approx_loc_def list_all2_conv_all_nth) 

126 

127 
lemma approx_loc_imp_approx_val_sup: 

128 
"\<lbrakk>approx_loc G hp loc LT; n < length LT; LT ! n = OK T; G \<turnstile> T \<preceq> T'; wf_prog wt G\<rbrakk> 

129 
\<Longrightarrow> G,hp \<turnstile> (loc!n) ::\<preceq> T'" 

130 
apply (drule approx_loc_nth, assumption) 

131 
apply simp 

132 
apply (erule conf_widen, assumption+) 

133 
done 

134 

135 
lemma approx_loc_conv_all_nth: 

136 
"approx_loc G hp loc LT = 

137 
(length loc = length LT \<and> (\<forall>n < length loc. approx_val G hp (loc!n) (LT!n)))" 

138 
by (simp add: approx_loc_def list_all2_conv_all_nth) 

139 

140 
lemma approx_loc_sup_heap: 

141 
"\<lbrakk> approx_loc G hp loc LT; hp \<le> hp' \<rbrakk> 

142 
\<Longrightarrow> approx_loc G hp' loc LT" 

143 
apply (clarsimp simp add: approx_loc_conv_all_nth) 

144 
apply (blast intro: approx_val_sup_heap) 

145 
done 

146 

147 
lemma approx_loc_widen: 

148 
"\<lbrakk> approx_loc G hp loc LT; G \<turnstile> LT <=l LT'; wf_prog wt G \<rbrakk> 

149 
\<Longrightarrow> approx_loc G hp loc LT'" 

150 
apply (unfold Listn.le_def lesub_def sup_loc_def) 

151 
apply (simp (no_asm_use) only: list_all2_conv_all_nth approx_loc_conv_all_nth) 

152 
apply (simp (no_asm_simp)) 

153 
apply clarify 

154 
apply (erule allE, erule impE) 

155 
apply simp 

156 
apply (erule approx_val_widen) 

157 
apply simp 

158 
apply assumption 

10056  159 
done 
9757
1024a2d80ac0
functional LBV style, dead code, type safety > Isar
kleing
parents:
9549
diff
changeset

160 

13052  161 
lemma loc_widen_Err [dest]: 
162 
"\<And>XT. G \<turnstile> replicate n Err <=l XT \<Longrightarrow> XT = replicate n Err" 

163 
by (induct n) auto 

164 

165 
lemma approx_loc_Err [iff]: 

166 
"approx_loc G hp (replicate n v) (replicate n Err)" 

167 
by (induct n) auto 

168 

11252  169 
lemma approx_loc_subst: 
170 
"\<lbrakk> approx_loc G hp loc LT; approx_val G hp x X \<rbrakk> 

171 
\<Longrightarrow> approx_loc G hp (loc[idx:=x]) (LT[idx:=X])" 

9757
1024a2d80ac0
functional LBV style, dead code, type safety > Isar
kleing
parents:
9549
diff
changeset

172 
apply (unfold approx_loc_def list_all2_def) 
1024a2d80ac0
functional LBV style, dead code, type safety > Isar
kleing
parents:
9549
diff
changeset

173 
apply (auto dest: subsetD [OF set_update_subset_insert] simp add: zip_update) 
10056  174 
done 
9757
1024a2d80ac0
functional LBV style, dead code, type safety > Isar
kleing
parents:
9549
diff
changeset

175 

11252  176 
lemma approx_loc_append: 
177 
"length l1=length L1 \<Longrightarrow> 

10056  178 
approx_loc G hp (l1@l2) (L1@L2) = 
179 
(approx_loc G hp l1 L1 \<and> approx_loc G hp l2 L2)" 

11252  180 
apply (unfold approx_loc_def list_all2_def) 
181 
apply (simp cong: conj_cong) 

182 
apply blast 

183 
done 

9757
1024a2d80ac0
functional LBV style, dead code, type safety > Isar
kleing
parents:
9549
diff
changeset

184 

11085  185 
section {* approxstk *} 
9757
1024a2d80ac0
functional LBV style, dead code, type safety > Isar
kleing
parents:
9549
diff
changeset

186 

1024a2d80ac0
functional LBV style, dead code, type safety > Isar
kleing
parents:
9549
diff
changeset

187 
lemma approx_stk_rev_lem: 
1024a2d80ac0
functional LBV style, dead code, type safety > Isar
kleing
parents:
9549
diff
changeset

188 
"approx_stk G hp (rev s) (rev t) = approx_stk G hp s t" 
11252  189 
apply (unfold approx_stk_def approx_loc_def) 
190 
apply (simp add: rev_map [THEN sym]) 

191 
done 

9757
1024a2d80ac0
functional LBV style, dead code, type safety > Isar
kleing
parents:
9549
diff
changeset

192 

1024a2d80ac0
functional LBV style, dead code, type safety > Isar
kleing
parents:
9549
diff
changeset

193 
lemma approx_stk_rev: 
1024a2d80ac0
functional LBV style, dead code, type safety > Isar
kleing
parents:
9549
diff
changeset

194 
"approx_stk G hp (rev s) t = approx_stk G hp s (rev t)" 
11252  195 
by (auto intro: subst [OF approx_stk_rev_lem]) 
9757
1024a2d80ac0
functional LBV style, dead code, type safety > Isar
kleing
parents:
9549
diff
changeset

196 

11252  197 
lemma approx_stk_sup_heap: 
198 
"\<lbrakk> approx_stk G hp stk ST; hp \<le> hp' \<rbrakk> \<Longrightarrow> approx_stk G hp' stk ST" 

199 
by (auto intro: approx_loc_sup_heap simp add: approx_stk_def) 

9757
1024a2d80ac0
functional LBV style, dead code, type safety > Isar
kleing
parents:
9549
diff
changeset

200 

11252  201 
lemma approx_stk_widen: 
202 
"\<lbrakk> approx_stk G hp stk ST; G \<turnstile> map OK ST <=l map OK ST'; wf_prog wt G \<rbrakk> 

203 
\<Longrightarrow> approx_stk G hp stk ST'" 

204 
by (auto elim: approx_loc_widen simp add: approx_stk_def) 

9757
1024a2d80ac0
functional LBV style, dead code, type safety > Isar
kleing
parents:
9549
diff
changeset

205 

1024a2d80ac0
functional LBV style, dead code, type safety > Isar
kleing
parents:
9549
diff
changeset

206 
lemma approx_stk_Nil [iff]: 
1024a2d80ac0
functional LBV style, dead code, type safety > Isar
kleing
parents:
9549
diff
changeset

207 
"approx_stk G hp [] []" 
11252  208 
by (simp add: approx_stk_def) 
9757
1024a2d80ac0
functional LBV style, dead code, type safety > Isar
kleing
parents:
9549
diff
changeset

209 

1024a2d80ac0
functional LBV style, dead code, type safety > Isar
kleing
parents:
9549
diff
changeset

210 
lemma approx_stk_Cons [iff]: 
11252  211 
"approx_stk G hp (x#stk) (S#ST) = 
212 
(approx_val G hp x (OK S) \<and> approx_stk G hp stk ST)" 

213 
by (simp add: approx_stk_def) 

9757
1024a2d80ac0
functional LBV style, dead code, type safety > Isar
kleing
parents:
9549
diff
changeset

214 

1024a2d80ac0
functional LBV style, dead code, type safety > Isar
kleing
parents:
9549
diff
changeset

215 
lemma approx_stk_Cons_lemma [iff]: 
1024a2d80ac0
functional LBV style, dead code, type safety > Isar
kleing
parents:
9549
diff
changeset

216 
"approx_stk G hp stk (S#ST') = 
10496  217 
(\<exists>s stk'. stk = s#stk' \<and> approx_val G hp s (OK S) \<and> approx_stk G hp stk' ST')" 
11252  218 
by (simp add: list_all2_Cons2 approx_stk_def approx_loc_def) 
219 

220 
lemma approx_stk_append: 

221 
"approx_stk G hp stk (S@S') \<Longrightarrow> 

222 
(\<exists>s stk'. stk = s@stk' \<and> length s = length S \<and> length stk' = length S' \<and> 

223 
approx_stk G hp s S \<and> approx_stk G hp stk' S')" 

224 
by (simp add: list_all2_append2 approx_stk_def approx_loc_def) 

9757
1024a2d80ac0
functional LBV style, dead code, type safety > Isar
kleing
parents:
9549
diff
changeset

225 

11252  226 
lemma approx_stk_all_widen: 
227 
"\<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> 

228 
\<Longrightarrow> approx_stk G hp stk ST'" 

229 
apply (unfold approx_stk_def) 

230 
apply (clarsimp simp add: approx_loc_conv_all_nth all_set_conv_all_nth) 

231 
apply (erule allE, erule impE, assumption) 

232 
apply (erule allE, erule impE, assumption) 

233 
apply (erule conf_widen, assumption+) 

234 
done 

9757
1024a2d80ac0
functional LBV style, dead code, type safety > Isar
kleing
parents:
9549
diff
changeset

235 

11085  236 
section {* oconf *} 
9757
1024a2d80ac0
functional LBV style, dead code, type safety > Isar
kleing
parents:
9549
diff
changeset

237 

11252  238 
lemma oconf_field_update: 
13006  239 
"\<lbrakk>map_of (fields (G, oT)) FD = Some T; G,hp\<turnstile>v::\<preceq>T; G,hp\<turnstile>(oT,fs)\<surd> \<rbrakk> 
240 
\<Longrightarrow> G,hp\<turnstile>(oT, fs(FD\<mapsto>v))\<surd>" 

11252  241 
by (simp add: oconf_def lconf_def) 
9757
1024a2d80ac0
functional LBV style, dead code, type safety > Isar
kleing
parents:
9549
diff
changeset

242 

11252  243 
lemma oconf_newref: 
244 
"\<lbrakk>hp oref = None; G,hp \<turnstile> obj \<surd>; G,hp \<turnstile> obj' \<surd>\<rbrakk> \<Longrightarrow> G,hp(oref\<mapsto>obj') \<turnstile> obj \<surd>" 

245 
apply (unfold oconf_def lconf_def) 

246 
apply simp 

247 
apply (blast intro: conf_hext hext_new) 

248 
done 

9757
1024a2d80ac0
functional LBV style, dead code, type safety > Isar
kleing
parents:
9549
diff
changeset

249 

11252  250 
lemma oconf_heap_update: 
251 
"\<lbrakk> hp a = Some obj'; obj_ty obj' = obj_ty obj''; G,hp\<turnstile>obj\<surd> \<rbrakk> 

252 
\<Longrightarrow> G,hp(a\<mapsto>obj'')\<turnstile>obj\<surd>" 

253 
apply (unfold oconf_def lconf_def) 

254 
apply (fastsimp intro: approx_val_heap_update) 

255 
done 

9757
1024a2d80ac0
functional LBV style, dead code, type safety > Isar
kleing
parents:
9549
diff
changeset

256 

11085  257 
section {* hconf *} 
9757
1024a2d80ac0
functional LBV style, dead code, type safety > Isar
kleing
parents:
9549
diff
changeset

258 

11252  259 
lemma hconf_newref: 
260 
"\<lbrakk> hp oref = None; G\<turnstile>h hp\<surd>; G,hp\<turnstile>obj\<surd> \<rbrakk> \<Longrightarrow> G\<turnstile>h hp(oref\<mapsto>obj)\<surd>" 

261 
apply (simp add: hconf_def) 

262 
apply (fast intro: oconf_newref) 

263 
done 

9757
1024a2d80ac0
functional LBV style, dead code, type safety > Isar
kleing
parents:
9549
diff
changeset

264 

11252  265 
lemma hconf_field_update: 
266 
"\<lbrakk> map_of (fields (G, oT)) X = Some T; hp a = Some(oT,fs); 

267 
G,hp\<turnstile>v::\<preceq>T; G\<turnstile>h hp\<surd> \<rbrakk> 

268 
\<Longrightarrow> G\<turnstile>h hp(a \<mapsto> (oT, fs(X\<mapsto>v)))\<surd>" 

269 
apply (simp add: hconf_def) 

270 
apply (fastsimp intro: oconf_heap_update oconf_field_update 

271 
simp add: obj_ty_def) 

272 
done 

9757
1024a2d80ac0
functional LBV style, dead code, type safety > Isar
kleing
parents:
9549
diff
changeset

273 

12545
7319d384d0d3
removed preallocated heaps axiom (now in type safety invariant)
kleing
parents:
12516
diff
changeset

274 
section {* preallocated *} 
7319d384d0d3
removed preallocated heaps axiom (now in type safety invariant)
kleing
parents:
12516
diff
changeset

275 

7319d384d0d3
removed preallocated heaps axiom (now in type safety invariant)
kleing
parents:
12516
diff
changeset

276 
lemma preallocated_field_update: 
7319d384d0d3
removed preallocated heaps axiom (now in type safety invariant)
kleing
parents:
12516
diff
changeset

277 
"\<lbrakk> map_of (fields (G, oT)) X = Some T; hp a = Some(oT,fs); 
7319d384d0d3
removed preallocated heaps axiom (now in type safety invariant)
kleing
parents:
12516
diff
changeset

278 
G\<turnstile>h hp\<surd>; preallocated hp \<rbrakk> 
7319d384d0d3
removed preallocated heaps axiom (now in type safety invariant)
kleing
parents:
12516
diff
changeset

279 
\<Longrightarrow> preallocated (hp(a \<mapsto> (oT, fs(X\<mapsto>v))))" 
7319d384d0d3
removed preallocated heaps axiom (now in type safety invariant)
kleing
parents:
12516
diff
changeset

280 
apply (unfold preallocated_def) 
7319d384d0d3
removed preallocated heaps axiom (now in type safety invariant)
kleing
parents:
12516
diff
changeset

281 
apply (rule allI) 
7319d384d0d3
removed preallocated heaps axiom (now in type safety invariant)
kleing
parents:
12516
diff
changeset

282 
apply (erule_tac x=x in allE) 
7319d384d0d3
removed preallocated heaps axiom (now in type safety invariant)
kleing
parents:
12516
diff
changeset

283 
apply simp 
7319d384d0d3
removed preallocated heaps axiom (now in type safety invariant)
kleing
parents:
12516
diff
changeset

284 
apply (rule ccontr) 
7319d384d0d3
removed preallocated heaps axiom (now in type safety invariant)
kleing
parents:
12516
diff
changeset

285 
apply (unfold hconf_def) 
7319d384d0d3
removed preallocated heaps axiom (now in type safety invariant)
kleing
parents:
12516
diff
changeset

286 
apply (erule allE, erule allE, erule impE, assumption) 
7319d384d0d3
removed preallocated heaps axiom (now in type safety invariant)
kleing
parents:
12516
diff
changeset

287 
apply (unfold oconf_def lconf_def) 
7319d384d0d3
removed preallocated heaps axiom (now in type safety invariant)
kleing
parents:
12516
diff
changeset

288 
apply (simp del: split_paired_All) 
7319d384d0d3
removed preallocated heaps axiom (now in type safety invariant)
kleing
parents:
12516
diff
changeset

289 
done 
7319d384d0d3
removed preallocated heaps axiom (now in type safety invariant)
kleing
parents:
12516
diff
changeset

290 

7319d384d0d3
removed preallocated heaps axiom (now in type safety invariant)
kleing
parents:
12516
diff
changeset

291 

13052  292 
lemma 
293 
assumes none: "hp oref = None" and alloc: "preallocated hp" 

294 
shows preallocated_newref: "preallocated (hp(oref\<mapsto>obj))" 

295 
proof (cases oref) 

296 
case (XcptRef x) 

297 
with none alloc have "False" by (auto elim: preallocatedE [of _ x]) 

298 
thus ?thesis .. 

299 
next 

300 
case (Loc l) 

301 
with alloc show ?thesis by (simp add: preallocated_def) 

302 
qed 

303 

11085  304 
section {* correctframes *} 
9757
1024a2d80ac0
functional LBV style, dead code, type safety > Isar
kleing
parents:
9549
diff
changeset

305 

1024a2d80ac0
functional LBV style, dead code, type safety > Isar
kleing
parents:
9549
diff
changeset

306 
lemmas [simp del] = fun_upd_apply 
1024a2d80ac0
functional LBV style, dead code, type safety > Isar
kleing
parents:
9549
diff
changeset

307 

11252  308 
lemma correct_frames_field_update [rule_format]: 
309 
"\<forall>rT C sig. 

13006  310 
correct_frames G hp phi rT sig frs \<longrightarrow> 
311 
hp a = Some (C,fs) \<longrightarrow> 

312 
map_of (fields (G, C)) fl = Some fd \<longrightarrow> 

10042  313 
G,hp\<turnstile>v::\<preceq>fd 
13006  314 
\<longrightarrow> correct_frames G (hp(a \<mapsto> (C, fs(fl\<mapsto>v)))) phi rT sig frs"; 
9757
1024a2d80ac0
functional LBV style, dead code, type safety > Isar
kleing
parents:
9549
diff
changeset

315 
apply (induct frs) 
1024a2d80ac0
functional LBV style, dead code, type safety > Isar
kleing
parents:
9549
diff
changeset

316 
apply simp 
10920  317 
apply clarify 
11252  318 
apply (simp (no_asm_use)) 
10920  319 
apply clarify 
320 
apply (unfold correct_frame_def) 

321 
apply (simp (no_asm_use)) 

11252  322 
apply clarify 
9757
1024a2d80ac0
functional LBV style, dead code, type safety > Isar
kleing
parents:
9549
diff
changeset

323 
apply (intro exI conjI) 
11252  324 
apply assumption+ 
325 
apply (erule approx_stk_sup_heap) 

326 
apply (erule hext_upd_obj) 

327 
apply (erule approx_loc_sup_heap) 

328 
apply (erule hext_upd_obj) 

329 
apply assumption+ 

330 
apply blast 

10056  331 
done 
9757
1024a2d80ac0
functional LBV style, dead code, type safety > Isar
kleing
parents:
9549
diff
changeset

332 

11252  333 
lemma correct_frames_newref [rule_format]: 
334 
"\<forall>rT C sig. 

335 
hp x = None \<longrightarrow> 

336 
correct_frames G hp phi rT sig frs \<longrightarrow> 

13681  337 
correct_frames G (hp(x \<mapsto> obj)) phi rT sig frs" 
9757
1024a2d80ac0
functional LBV style, dead code, type safety > Isar
kleing
parents:
9549
diff
changeset

338 
apply (induct frs) 
1024a2d80ac0
functional LBV style, dead code, type safety > Isar
kleing
parents:
9549
diff
changeset

339 
apply simp 
11252  340 
apply clarify 
341 
apply (simp (no_asm_use)) 

342 
apply clarify 

343 
apply (unfold correct_frame_def) 

344 
apply (simp (no_asm_use)) 

345 
apply clarify 

9757
1024a2d80ac0
functional LBV style, dead code, type safety > Isar
kleing
parents:
9549
diff
changeset

346 
apply (intro exI conjI) 
11252  347 
apply assumption+ 
348 
apply (erule approx_stk_sup_heap) 

349 
apply (erule hext_new) 

350 
apply (erule approx_loc_sup_heap) 

351 
apply (erule hext_new) 

352 
apply assumption+ 

353 
apply blast 

10056  354 
done 
8011  355 

356 
end 