author  wenzelm 
Mon, 25 Feb 2002 20:48:14 +0100  
changeset 12937  0c4fd7529467 
parent 12925  99131847fb93 
child 13688  a0b16d42d489 
permissions  rwrr 
12857  1 
(* Title: HOL/Bali/Conform.thy 
12854  2 
ID: $Id$ 
3 
Author: David von Oheimb 

12858  4 
License: GPL (GNU GENERAL PUBLIC LICENSE) 
12854  5 
*) 
6 

7 
header {* Conformance notions for the type soundness proof for Java *} 

8 

9 
theory Conform = State: 

10 

11 
text {* 

12 
design issues: 

13 
\begin{itemize} 

14 
\item lconf allows for (arbitrary) inaccessible values 

15 
\item ''conforms'' does not directly imply that the dynamic types of all 

16 
objects on the heap are indeed existing classes. Yet this can be 

17 
inferred for all referenced objs. 

18 
\end{itemize} 

19 
*} 

20 

21 
types env_ = "prog \<times> (lname, ty) table" (* same as env of WellType.thy *) 

22 

23 

24 
section "extension of global store" 

25 

12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset

26 

12854  27 
constdefs 
28 

29 
gext :: "st \<Rightarrow> st \<Rightarrow> bool" ("_\<le>_" [71,71] 70) 

30 
"s\<le>s' \<equiv> \<forall>r. \<forall>obj\<in>globs s r: \<exists>obj'\<in>globs s' r: tag obj'= tag obj" 

31 

12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset

32 
text {* For the the proof of type soundness we will need the 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset

33 
property that during execution, objects are not lost and moreover retain the 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset

34 
values of their tags. So the object store grows conservatively. Note that if 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset

35 
we considered garbage collection, we would have to restrict this property to 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset

36 
accessible objects. 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset

37 
*} 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset

38 

12854  39 
lemma gext_objD: 
40 
"\<lbrakk>s\<le>s'; globs s r = Some obj\<rbrakk> 

41 
\<Longrightarrow> \<exists>obj'. globs s' r = Some obj' \<and> tag obj' = tag obj" 

42 
apply (simp only: gext_def) 

43 
by force 

44 

45 
lemma rev_gext_objD: 

46 
"\<lbrakk>globs s r = Some obj; s\<le>s'\<rbrakk> 

47 
\<Longrightarrow> \<exists>obj'. globs s' r = Some obj' \<and> tag obj' = tag obj" 

48 
by (auto elim: gext_objD) 

49 

50 
lemma init_class_obj_inited: 

51 
"init_class_obj G C s1\<le>s2 \<Longrightarrow> inited C (globs s2)" 

52 
apply (unfold inited_def init_obj_def) 

53 
apply (auto dest!: gext_objD) 

54 
done 

55 

56 
lemma gext_refl [intro!, simp]: "s\<le>s" 

57 
apply (unfold gext_def) 

58 
apply (fast del: fst_splitE) 

59 
done 

60 

61 
lemma gext_gupd [simp, elim!]: "\<And>s. globs s r = None \<Longrightarrow> s\<le>gupd(r\<mapsto>x)s" 

62 
by (auto simp: gext_def) 

63 

64 
lemma gext_new [simp, elim!]: "\<And>s. globs s r = None \<Longrightarrow> s\<le>init_obj G oi r s" 

65 
apply (simp only: init_obj_def) 

66 
apply (erule_tac gext_gupd) 

67 
done 

68 

69 
lemma gext_trans [elim]: "\<And>X. \<lbrakk>s\<le>s'; s'\<le>s''\<rbrakk> \<Longrightarrow> s\<le>s''" 

70 
by (force simp: gext_def) 

71 

72 
lemma gext_upd_gobj [intro!]: "s\<le>upd_gobj r n v s" 

73 
apply (simp only: gext_def) 

74 
apply auto 

75 
apply (case_tac "ra = r") 

76 
apply auto 

77 
apply (case_tac "globs s r = None") 

78 
apply auto 

79 
done 

80 

81 
lemma gext_cong1 [simp]: "set_locals l s1\<le>s2 = s1\<le>s2" 

82 
by (auto simp: gext_def) 

83 

84 
lemma gext_cong2 [simp]: "s1\<le>set_locals l s2 = s1\<le>s2" 

85 
by (auto simp: gext_def) 

86 

87 

88 
lemma gext_lupd1 [simp]: "lupd(vn\<mapsto>v)s1\<le>s2 = s1\<le>s2" 

89 
by (auto simp: gext_def) 

90 

91 
lemma gext_lupd2 [simp]: "s1\<le>lupd(vn\<mapsto>v)s2 = s1\<le>s2" 

92 
by (auto simp: gext_def) 

93 

94 

95 
lemma inited_gext: "\<lbrakk>inited C (globs s); s\<le>s'\<rbrakk> \<Longrightarrow> inited C (globs s')" 

96 
apply (unfold inited_def) 

97 
apply (auto dest: gext_objD) 

98 
done 

99 

100 

101 
section "value conformance" 

102 

103 
constdefs 

104 

105 
conf :: "prog \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ty \<Rightarrow> bool" ("_,_\<turnstile>_\<Colon>\<preceq>_" [71,71,71,71] 70) 

106 
"G,s\<turnstile>v\<Colon>\<preceq>T \<equiv> \<exists>T'\<in>typeof (\<lambda>a. option_map obj_ty (heap s a)) v:G\<turnstile>T'\<preceq>T" 

107 

108 
lemma conf_cong [simp]: "G,set_locals l s\<turnstile>v\<Colon>\<preceq>T = G,s\<turnstile>v\<Colon>\<preceq>T" 

109 
by (auto simp: conf_def) 

110 

111 
lemma conf_lupd [simp]: "G,lupd(vn\<mapsto>va)s\<turnstile>v\<Colon>\<preceq>T = G,s\<turnstile>v\<Colon>\<preceq>T" 

112 
by (auto simp: conf_def) 

113 

114 
lemma conf_PrimT [simp]: "\<forall>dt. typeof dt v = Some (PrimT t) \<Longrightarrow> G,s\<turnstile>v\<Colon>\<preceq>PrimT t" 

115 
apply (simp add: conf_def) 

116 
done 

117 

118 
lemma conf_litval [rule_format (no_asm)]: 

119 
"typeof (\<lambda>a. None) v = Some T \<longrightarrow> G,s\<turnstile>v\<Colon>\<preceq>T" 

120 
apply (unfold conf_def) 

121 
apply (rule val.induct) 

122 
apply auto 

123 
done 

124 

125 
lemma conf_Null [simp]: "G,s\<turnstile>Null\<Colon>\<preceq>T = G\<turnstile>NT\<preceq>T" 

126 
by (simp add: conf_def) 

127 

128 
lemma conf_Addr: 

129 
"G,s\<turnstile>Addr a\<Colon>\<preceq>T = (\<exists>obj. heap s a = Some obj \<and> G\<turnstile>obj_ty obj\<preceq>T)" 

130 
by (auto simp: conf_def) 

131 

132 
lemma conf_AddrI:"\<lbrakk>heap s a = Some obj; G\<turnstile>obj_ty obj\<preceq>T\<rbrakk> \<Longrightarrow> G,s\<turnstile>Addr a\<Colon>\<preceq>T" 

133 
apply (rule conf_Addr [THEN iffD2]) 

134 
by fast 

135 

136 
lemma defval_conf [rule_format (no_asm), elim]: 

137 
"is_type G T \<longrightarrow> G,s\<turnstile>default_val T\<Colon>\<preceq>T" 

138 
apply (unfold conf_def) 

139 
apply (induct "T") 

140 
apply (auto intro: prim_ty.induct) 

141 
done 

142 

143 
lemma conf_widen [rule_format (no_asm), elim]: 

144 
"G\<turnstile>T\<preceq>T' \<Longrightarrow> G,s\<turnstile>x\<Colon>\<preceq>T \<longrightarrow> ws_prog G \<longrightarrow> G,s\<turnstile>x\<Colon>\<preceq>T'" 

145 
apply (unfold conf_def) 

146 
apply (rule val.induct) 

147 
apply (auto elim: ws_widen_trans) 

148 
done 

149 

150 
lemma conf_gext [rule_format (no_asm), elim]: 

151 
"G,s\<turnstile>v\<Colon>\<preceq>T \<longrightarrow> s\<le>s' \<longrightarrow> G,s'\<turnstile>v\<Colon>\<preceq>T" 

152 
apply (unfold gext_def conf_def) 

153 
apply (rule val.induct) 

154 
apply force+ 

155 
done 

156 

157 

158 
lemma conf_list_widen [rule_format (no_asm)]: 

159 
"ws_prog G \<Longrightarrow> 

160 
\<forall>Ts Ts'. list_all2 (conf G s) vs Ts 

161 
\<longrightarrow> G\<turnstile>Ts[\<preceq>] Ts' \<longrightarrow> list_all2 (conf G s) vs Ts'" 

162 
apply (unfold widens_def) 

163 
apply (rule list_all2_trans) 

164 
apply auto 

165 
done 

166 

167 
lemma conf_RefTD [rule_format (no_asm)]: 

168 
"G,s\<turnstile>a'\<Colon>\<preceq>RefT T 

169 
\<longrightarrow> a' = Null \<or> (\<exists>a obj T'. a' = Addr a \<and> heap s a = Some obj \<and> 

170 
obj_ty obj = T' \<and> G\<turnstile>T'\<preceq>RefT T)" 

171 
apply (unfold conf_def) 

172 
apply (induct_tac "a'") 

173 
apply (auto dest: widen_PrimT) 

174 
done 

175 

176 

177 
section "value list conformance" 

178 

179 
constdefs 

180 

181 
lconf :: "prog \<Rightarrow> st \<Rightarrow> ('a, val) table \<Rightarrow> ('a, ty) table \<Rightarrow> bool" 

182 
("_,_\<turnstile>_[\<Colon>\<preceq>]_" [71,71,71,71] 70) 

183 
"G,s\<turnstile>vs[\<Colon>\<preceq>]Ts \<equiv> \<forall>n. \<forall>T\<in>Ts n: \<exists>v\<in>vs n: G,s\<turnstile>v\<Colon>\<preceq>T" 

184 

185 
lemma lconfD: "\<lbrakk>G,s\<turnstile>vs[\<Colon>\<preceq>]Ts; Ts n = Some T\<rbrakk> \<Longrightarrow> G,s\<turnstile>(the (vs n))\<Colon>\<preceq>T" 

186 
by (force simp: lconf_def) 

187 

188 

189 
lemma lconf_cong [simp]: "\<And>s. G,set_locals x s\<turnstile>l[\<Colon>\<preceq>]L = G,s\<turnstile>l[\<Colon>\<preceq>]L" 

190 
by (auto simp: lconf_def) 

191 

192 
lemma lconf_lupd [simp]: "G,lupd(vn\<mapsto>v)s\<turnstile>l[\<Colon>\<preceq>]L = G,s\<turnstile>l[\<Colon>\<preceq>]L" 

193 
by (auto simp: lconf_def) 

194 

195 
(* unused *) 

196 
lemma lconf_new: "\<lbrakk>L vn = None; G,s\<turnstile>l[\<Colon>\<preceq>]L\<rbrakk> \<Longrightarrow> G,s\<turnstile>l(vn\<mapsto>v)[\<Colon>\<preceq>]L" 

197 
by (auto simp: lconf_def) 

198 

199 
lemma lconf_upd: "\<lbrakk>G,s\<turnstile>l[\<Colon>\<preceq>]L; G,s\<turnstile>v\<Colon>\<preceq>T; L vn = Some T\<rbrakk> \<Longrightarrow> 

200 
G,s\<turnstile>l(vn\<mapsto>v)[\<Colon>\<preceq>]L" 

201 
by (auto simp: lconf_def) 

202 

203 
lemma lconf_ext: "\<lbrakk>G,s\<turnstile>l[\<Colon>\<preceq>]L; G,s\<turnstile>v\<Colon>\<preceq>T\<rbrakk> \<Longrightarrow> G,s\<turnstile>l(vn\<mapsto>v)[\<Colon>\<preceq>]L(vn\<mapsto>T)" 

204 
by (auto simp: lconf_def) 

205 

206 
lemma lconf_map_sum [simp]: 

207 
"G,s\<turnstile>l1 (+) l2[\<Colon>\<preceq>]L1 (+) L2 = (G,s\<turnstile>l1[\<Colon>\<preceq>]L1 \<and> G,s\<turnstile>l2[\<Colon>\<preceq>]L2)" 

208 
apply (unfold lconf_def) 

209 
apply safe 

210 
apply (case_tac [3] "n") 

211 
apply (force split add: sum.split)+ 

212 
done 

213 

214 
lemma lconf_ext_list [rule_format (no_asm)]: " 

215 
\<And>X. \<lbrakk>G,s\<turnstile>l[\<Colon>\<preceq>]L\<rbrakk> \<Longrightarrow> 

12893  216 
\<forall>vs Ts. distinct vns \<longrightarrow> length Ts = length vns 
12854  217 
\<longrightarrow> list_all2 (conf G s) vs Ts \<longrightarrow> G,s\<turnstile>l(vns[\<mapsto>]vs)[\<Colon>\<preceq>]L(vns[\<mapsto>]Ts)" 
218 
apply (unfold lconf_def) 

219 
apply (induct_tac "vns") 

220 
apply clarsimp 

221 
apply clarsimp 

222 
apply (frule list_all2_lengthD) 

223 
apply clarsimp 

224 
done 

225 

226 

227 
lemma lconf_deallocL: "\<lbrakk>G,s\<turnstile>l[\<Colon>\<preceq>]L(vn\<mapsto>T); L vn = None\<rbrakk> \<Longrightarrow> G,s\<turnstile>l[\<Colon>\<preceq>]L" 

228 
apply (simp only: lconf_def) 

229 
apply safe 

230 
apply (drule spec) 

231 
apply (drule ospec) 

232 
apply auto 

233 
done 

234 

235 

236 
lemma lconf_gext [elim]: "\<lbrakk>G,s\<turnstile>l[\<Colon>\<preceq>]L; s\<le>s'\<rbrakk> \<Longrightarrow> G,s'\<turnstile>l[\<Colon>\<preceq>]L" 

237 
apply (simp only: lconf_def) 

238 
apply fast 

239 
done 

240 

241 
lemma lconf_empty [simp, intro!]: "G,s\<turnstile>vs[\<Colon>\<preceq>]empty" 

242 
apply (unfold lconf_def) 

243 
apply force 

244 
done 

245 

246 
lemma lconf_init_vals [intro!]: 

247 
" \<forall>n. \<forall>T\<in>fs n:is_type G T \<Longrightarrow> G,s\<turnstile>init_vals fs[\<Colon>\<preceq>]fs" 

248 
apply (unfold lconf_def) 

249 
apply force 

250 
done 

251 

252 

253 
section "object conformance" 

254 

255 
constdefs 

256 

257 
oconf :: "prog \<Rightarrow> st \<Rightarrow> obj \<Rightarrow> oref \<Rightarrow> bool" ("_,_\<turnstile>_\<Colon>\<preceq>\<surd>_" [71,71,71,71] 70) 

258 
"G,s\<turnstile>obj\<Colon>\<preceq>\<surd>r \<equiv> G,s\<turnstile>values obj[\<Colon>\<preceq>]var_tys G (tag obj) r \<and> 

259 
(case r of 

260 
Heap a \<Rightarrow> is_type G (obj_ty obj) 

261 
 Stat C \<Rightarrow> True)" 

262 
(* 

263 
lemma oconf_def2: "G,s\<turnstile>\<lparr>tag=oi,values=fs\<rparr>\<Colon>\<preceq>\<surd>r = 

264 
(G,s\<turnstile>fs[\<Colon>\<preceq>]var_tys G oi r \<and> 

265 
(case r of Heap a \<Rightarrow> is_type G (obj_ty \<lparr>tag=oi,values=fs\<rparr>)  Stat C \<Rightarrow> True))" 

266 
by (simp add: oconf_def Let_def) 

267 
*) 

268 
(* 

269 
lemma oconf_def2: "G,s\<turnstile>obj\<Colon>\<preceq>\<surd>r = 

270 
(G,s\<turnstile>values obj[\<Colon>\<preceq>]var_tys G (tag obj) r \<and> 

271 
(case r of Heap a \<Rightarrow> is_type G (obj_ty obj)  Stat C \<Rightarrow> True))" 

272 
by (simp add: oconf_def Let_def) 

273 
*) 

274 
lemma oconf_is_type: "G,s\<turnstile>obj\<Colon>\<preceq>\<surd>Heap a \<Longrightarrow> is_type G (obj_ty obj)" 

275 
by (auto simp: oconf_def Let_def) 

276 

277 
lemma oconf_lconf: "G,s\<turnstile>obj\<Colon>\<preceq>\<surd>r \<Longrightarrow> G,s\<turnstile>values obj[\<Colon>\<preceq>]var_tys G (tag obj) r" 

278 
by (simp add: oconf_def) 

279 

280 
lemma oconf_cong [simp]: "G,set_locals l s\<turnstile>obj\<Colon>\<preceq>\<surd>r = G,s\<turnstile>obj\<Colon>\<preceq>\<surd>r" 

281 
by (auto simp: oconf_def Let_def) 

282 

283 
lemma oconf_init_obj_lemma: 

284 
"\<lbrakk>\<And>C c. class G C = Some c \<Longrightarrow> unique (DeclConcepts.fields G C); 

285 
\<And>C c f fld. \<lbrakk>class G C = Some c; 

286 
table_of (DeclConcepts.fields G C) f = Some fld \<rbrakk> 

287 
\<Longrightarrow> is_type G (type fld); 

288 
(case r of 

289 
Heap a \<Rightarrow> is_type G (obj_ty obj) 

290 
 Stat C \<Rightarrow> is_class G C) 

291 
\<rbrakk> \<Longrightarrow> G,s\<turnstile>obj \<lparr>values:=init_vals (var_tys G (tag obj) r)\<rparr>\<Colon>\<preceq>\<surd>r" 

292 
apply (auto simp add: oconf_def) 

293 
apply (drule_tac var_tys_Some_eq [THEN iffD1]) 

294 
defer 

295 
apply (subst obj_ty_cong) 

296 
apply(auto dest!: fields_table_SomeD obj_ty_CInst1 obj_ty_Arr1 

297 
split add: sum.split_asm obj_tag.split_asm) 

298 
done 

299 

300 
(* 

301 
lemma oconf_init_obj_lemma: 

302 
"\<lbrakk>\<And>C c. class G C = Some c \<Longrightarrow> unique (fields G C); 

303 
\<And>C c f fld. \<lbrakk>class G C = Some c; table_of (fields G C) f = Some fld \<rbrakk> 

304 
\<Longrightarrow> is_type G (type fld); 

305 
(case r of 

306 
Heap a \<Rightarrow> is_type G (obj_ty \<lparr>tag=oi,values=fs\<rparr>) 

307 
 Stat C \<Rightarrow> is_class G C) 

308 
\<rbrakk> \<Longrightarrow> G,s\<turnstile>\<lparr>tag=oi, values=init_vals (var_tys G oi r)\<rparr>\<Colon>\<preceq>\<surd>r" 

309 
apply (auto simp add: oconf_def) 

310 
apply (drule_tac var_tys_Some_eq [THEN iffD1]) 

311 
defer 

312 
apply (subst obj_ty_eq) 

313 
apply(auto dest!: fields_table_SomeD split add: sum.split_asm obj_tag.split_asm) 

314 
done 

315 
*) 

316 

317 

318 
section "state conformance" 

319 

320 
constdefs 

321 

322 
conforms :: "state \<Rightarrow> env_ \<Rightarrow> bool" ( "_\<Colon>\<preceq>_" [71,71] 70) 

323 
"xs\<Colon>\<preceq>E \<equiv> let (G, L) = E; s = snd xs; l = locals s in 

324 
(\<forall>r. \<forall>obj\<in>globs s r: G,s\<turnstile>obj \<Colon>\<preceq>\<surd>r) \<and> 

325 
\<spacespace> G,s\<turnstile>l [\<Colon>\<preceq>]L\<spacespace> \<and> 

326 
(\<forall>a. fst xs=Some(Xcpt (Loc a)) \<longrightarrow> G,s\<turnstile>Addr a\<Colon>\<preceq> Class (SXcpt Throwable))" 

327 

328 
section "conforms" 

329 

330 
lemma conforms_globsD: 

331 
"\<lbrakk>(x, s)\<Colon>\<preceq>(G, L); globs s r = Some obj\<rbrakk> \<Longrightarrow> G,s\<turnstile>obj\<Colon>\<preceq>\<surd>r" 

332 
by (auto simp: conforms_def Let_def) 

333 

334 
lemma conforms_localD: "(x, s)\<Colon>\<preceq>(G, L) \<Longrightarrow> G,s\<turnstile>locals s[\<Colon>\<preceq>]L" 

335 
by (auto simp: conforms_def Let_def) 

336 

337 
lemma conforms_XcptLocD: "\<lbrakk>(x, s)\<Colon>\<preceq>(G, L); x = Some (Xcpt (Loc a))\<rbrakk> \<Longrightarrow> 

338 
G,s\<turnstile>Addr a\<Colon>\<preceq> Class (SXcpt Throwable)" 

339 
by (auto simp: conforms_def Let_def) 

340 

341 
lemma conforms_RefTD: 

342 
"\<lbrakk>G,s\<turnstile>a'\<Colon>\<preceq>RefT t; a' \<noteq> Null; (x,s) \<Colon>\<preceq>(G, L)\<rbrakk> \<Longrightarrow> 

343 
\<exists>a obj. a' = Addr a \<and> globs s (Inl a) = Some obj \<and> 

344 
G\<turnstile>obj_ty obj\<preceq>RefT t \<and> is_type G (obj_ty obj)" 

345 
apply (drule_tac conf_RefTD) 

346 
apply clarsimp 

347 
apply (rule conforms_globsD [THEN oconf_is_type]) 

348 
apply auto 

349 
done 

350 

351 
lemma conforms_Jump [iff]: 

352 
"((Some (Jump j), s)\<Colon>\<preceq>(G, L)) = (Norm s\<Colon>\<preceq>(G, L))" 

353 
by (auto simp: conforms_def) 

354 

355 
lemma conforms_StdXcpt [iff]: 

356 
"((Some (Xcpt (Std xn)), s)\<Colon>\<preceq>(G, L)) = (Norm s\<Colon>\<preceq>(G, L))" 

357 
by (auto simp: conforms_def) 

358 

12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset

359 
lemma conforms_Err [iff]: 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset

360 
"((Some (Error e), s)\<Colon>\<preceq>(G, L)) = (Norm s\<Colon>\<preceq>(G, L))" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset

361 
by (auto simp: conforms_def) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset

362 

12854  363 
lemma conforms_raise_if [iff]: 
364 
"((raise_if c xn x, s)\<Colon>\<preceq>(G, L)) = ((x, s)\<Colon>\<preceq>(G, L))" 

365 
by (auto simp: abrupt_if_def) 

366 

12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset

367 
lemma conforms_error_if [iff]: 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset

368 
"((error_if c err x, s)\<Colon>\<preceq>(G, L)) = ((x, s)\<Colon>\<preceq>(G, L))" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset

369 
by (auto simp: abrupt_if_def split: split_if) 
12854  370 

371 
lemma conforms_NormI: "(x, s)\<Colon>\<preceq>(G, L) \<Longrightarrow> Norm s\<Colon>\<preceq>(G, L)" 

372 
by (auto simp: conforms_def Let_def) 

373 

374 
lemma conforms_absorb [rule_format]: 

375 
"(a, b)\<Colon>\<preceq>(G, L) \<longrightarrow> (absorb j a, b)\<Colon>\<preceq>(G, L)" 

376 
apply (rule impI) 

377 
apply ( case_tac a) 

378 
apply (case_tac "absorb j a") 

379 
apply auto 

380 
apply (case_tac "absorb j (Some a)",auto) 

381 
apply (erule conforms_NormI) 

382 
done 

383 

384 
lemma conformsI: "\<lbrakk>\<forall>r. \<forall>obj\<in>globs s r: G,s\<turnstile>obj\<Colon>\<preceq>\<surd>r; 

385 
G,s\<turnstile>locals s[\<Colon>\<preceq>]L; 

386 
\<forall>a. x = Some (Xcpt (Loc a)) \<longrightarrow> G,s\<turnstile>Addr a\<Colon>\<preceq> Class (SXcpt Throwable)\<rbrakk> \<Longrightarrow> 

387 
(x, s)\<Colon>\<preceq>(G, L)" 

388 
by (auto simp: conforms_def Let_def) 

389 

390 
lemma conforms_xconf: "\<lbrakk>(x, s)\<Colon>\<preceq>(G,L); 

391 
\<forall>a. x' = Some (Xcpt (Loc a)) \<longrightarrow> G,s\<turnstile>Addr a\<Colon>\<preceq> Class (SXcpt Throwable)\<rbrakk> \<Longrightarrow> 

392 
(x',s)\<Colon>\<preceq>(G,L)" 

393 
by (fast intro: conformsI elim: conforms_globsD conforms_localD) 

394 

395 
lemma conforms_lupd: 

396 
"\<lbrakk>(x, s)\<Colon>\<preceq>(G, L); L vn = Some T; G,s\<turnstile>v\<Colon>\<preceq>T\<rbrakk> \<Longrightarrow> (x, lupd(vn\<mapsto>v)s)\<Colon>\<preceq>(G, L)" 

397 
by (force intro: conformsI lconf_upd dest: conforms_globsD conforms_localD 

398 
conforms_XcptLocD simp: oconf_def) 

399 

400 

401 
lemmas conforms_allocL_aux = conforms_localD [THEN lconf_ext] 

402 

403 
lemma conforms_allocL: 

404 
"\<lbrakk>(x, s)\<Colon>\<preceq>(G, L); G,s\<turnstile>v\<Colon>\<preceq>T\<rbrakk> \<Longrightarrow> (x, lupd(vn\<mapsto>v)s)\<Colon>\<preceq>(G, L(vn\<mapsto>T))" 

405 
by (force intro: conformsI dest: conforms_globsD 

406 
elim: conforms_XcptLocD conforms_allocL_aux simp: oconf_def) 

407 

408 
lemmas conforms_deallocL_aux = conforms_localD [THEN lconf_deallocL] 

409 

410 
lemma conforms_deallocL: "\<And>s.\<lbrakk>s\<Colon>\<preceq>(G, L(vn\<mapsto>T)); L vn = None\<rbrakk> \<Longrightarrow> s\<Colon>\<preceq>(G,L)" 

411 
by (fast intro: conformsI dest: conforms_globsD 

412 
elim: conforms_XcptLocD conforms_deallocL_aux) 

413 

414 
lemma conforms_gext: "\<lbrakk>(x, s)\<Colon>\<preceq>(G,L); s\<le>s'; 

415 
\<forall>r. \<forall>obj\<in>globs s' r: G,s'\<turnstile>obj\<Colon>\<preceq>\<surd>r; 

416 
locals s'=locals s\<rbrakk> \<Longrightarrow> (x,s')\<Colon>\<preceq>(G,L)" 

417 
by (force intro!: conformsI dest: conforms_localD conforms_XcptLocD) 

418 

419 

420 
lemma conforms_xgext: 

421 
"\<lbrakk>(x ,s)\<Colon>\<preceq>(G,L); (x', s')\<Colon>\<preceq>(G, L); s'\<le>s\<rbrakk> \<Longrightarrow> (x',s)\<Colon>\<preceq>(G,L)" 

422 
apply (erule_tac conforms_xconf) 

423 
apply (fast dest: conforms_XcptLocD) 

424 
done 

425 

426 
lemma conforms_gupd: "\<And>obj. \<lbrakk>(x, s)\<Colon>\<preceq>(G, L); G,s\<turnstile>obj\<Colon>\<preceq>\<surd>r; s\<le>gupd(r\<mapsto>obj)s\<rbrakk> 

427 
\<Longrightarrow> (x, gupd(r\<mapsto>obj)s)\<Colon>\<preceq>(G, L)" 

428 
apply (rule conforms_gext) 

429 
apply auto 

430 
apply (force dest: conforms_globsD simp add: oconf_def)+ 

431 
done 

432 

433 
lemma conforms_upd_gobj: "\<lbrakk>(x,s)\<Colon>\<preceq>(G, L); globs s r = Some obj; 

434 
var_tys G (tag obj) r n = Some T; G,s\<turnstile>v\<Colon>\<preceq>T\<rbrakk> \<Longrightarrow> (x,upd_gobj r n v s)\<Colon>\<preceq>(G,L)" 

435 
apply (rule conforms_gext) 

436 
apply auto 

437 
apply (drule (1) conforms_globsD) 

438 
apply (simp add: oconf_def) 

439 
apply safe 

440 
apply (rule lconf_upd) 

441 
apply auto 

442 
apply (simp only: obj_ty_cong) 

443 
apply (force dest: conforms_globsD intro!: lconf_upd 

444 
simp add: oconf_def cong del: sum.weak_case_cong) 

445 
done 

446 

447 
lemma conforms_set_locals: 

448 
"\<lbrakk>(x,s)\<Colon>\<preceq>(G, L'); G,s\<turnstile>l[\<Colon>\<preceq>]L\<rbrakk> \<Longrightarrow> (x,set_locals l s)\<Colon>\<preceq>(G,L)" 

449 
apply (auto intro!: conformsI dest: conforms_globsD 

450 
elim!: conforms_XcptLocD simp add: oconf_def) 

451 
done 

452 

12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset

453 
lemma conforms_locals [rule_format]: 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset

454 
"(a,b)\<Colon>\<preceq>(G, L) \<longrightarrow> L x = Some T \<longrightarrow> G,b\<turnstile>the (locals b x)\<Colon>\<preceq>T" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset

455 
apply (force simp: conforms_def Let_def lconf_def) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset

456 
done 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset

457 

12854  458 
lemma conforms_return: "\<And>s'. \<lbrakk>(x,s)\<Colon>\<preceq>(G, L); (x',s')\<Colon>\<preceq>(G, L'); s\<le>s'\<rbrakk> \<Longrightarrow> 
459 
(x',set_locals (locals s) s')\<Colon>\<preceq>(G, L)" 

460 
apply (rule conforms_xconf) 

461 
prefer 2 apply (force dest: conforms_XcptLocD) 

462 
apply (erule conforms_gext) 

463 
apply (force dest: conforms_globsD)+ 

464 
done 

465 

12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset

466 

12854  467 
end 