author  wenzelm 
Mon, 25 Feb 2002 20:48:14 +0100  
changeset 12937  0c4fd7529467 
parent 12925  99131847fb93 
child 12962  a24ffe84a06a 
permissions  rwrr 
12857  1 
(* Title: HOL/Bali/WellForm.thy 
12854  2 
ID: $Id$ 
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset

3 
Author: David von Oheimb and Norbert Schirmer 
12858  4 
License: GPL (GNU GENERAL PUBLIC LICENSE) 
12854  5 
*) 
6 

7 
header {* Wellformedness of Java programs *} 

8 

9 
theory WellForm = WellType: 

10 

11 
text {* 

12 
For static checks on expressions and statements, see WellType.thy 

13 

14 
improvements over Java Specification 1.0 (cf. 8.4.6.3, 8.4.6.4, 9.4.1): 

15 
\begin{itemize} 

16 
\item a method implementing or overwriting another method may have a result 

17 
type that widens to the result type of the other method 

18 
(instead of identical type) 

19 
\item if a method hides another method (both methods have to be static!) 

20 
there are no restrictions to the result type 

21 
since the methods have to be static and there is no dynamic binding of 

22 
static methods 

23 
\item if an interface inherits more than one method with the same signature, the 

24 
methods need not have identical return types 

25 
\end{itemize} 

26 
simplifications: 

27 
\begin{itemize} 

28 
\item Object and standard exceptions are assumed to be declared like normal 

29 
classes 

30 
\end{itemize} 

31 
*} 

32 

33 
section "wellformed field declarations" 

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

34 
text {* wellformed field declaration (common part for classes and interfaces), 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset

35 
cf. 8.3 and (9.3) *} 
12854  36 

37 
constdefs 

38 
wf_fdecl :: "prog \<Rightarrow> pname \<Rightarrow> fdecl \<Rightarrow> bool" 

39 
"wf_fdecl G P \<equiv> \<lambda>(fn,f). is_acc_type G P (type f)" 

40 

41 
lemma wf_fdecl_def2: "\<And>fd. wf_fdecl G P fd = is_acc_type G P (type (snd fd))" 

42 
apply (unfold wf_fdecl_def) 

43 
apply simp 

44 
done 

45 

46 

47 

48 
section "wellformed method declarations" 

49 
(*wellformed method declaration,cf. 8.4, 8.4.1, 8.4.3, 8.4.5, 14.3.2, (9.4)*) 

50 
(* cf. 14.15, 15.7.2, for scope issues cf. 8.4.1 and 14.3.2 *) 

51 

52 
text {* 

53 
A method head is wellformed if: 

54 
\begin{itemize} 

55 
\item the signature and the method head agree in the number of parameters 

56 
\item all types of the parameters are visible 

57 
\item the result type is visible 

58 
\item the parameter names are unique 

59 
\end{itemize} 

60 
*} 

61 
constdefs 

62 
wf_mhead :: "prog \<Rightarrow> pname \<Rightarrow> sig \<Rightarrow> mhead \<Rightarrow> bool" 

63 
"wf_mhead G P \<equiv> \<lambda> sig mh. length (parTs sig) = length (pars mh) \<and> 

64 
\<spacespace> ( \<forall>T\<in>set (parTs sig). is_acc_type G P T) \<and> 

65 
is_acc_type G P (resTy mh) \<and> 

12893  66 
\<spacespace> distinct (pars mh)" 
12854  67 

68 

69 
text {* 

70 
A method declaration is wellformed if: 

71 
\begin{itemize} 

72 
\item the method head is wellformed 

73 
\item the names of the local variables are unique 

74 
\item the types of the local variables must be accessible 

75 
\item the local variables don't shadow the parameters 

76 
\item the class of the method is defined 

77 
\item the body statement is welltyped with respect to the 

78 
modified environment of local names, were the local variables, 

79 
the parameters the special result variable (Res) and This are assoziated 

80 
with there types. 

81 
\end{itemize} 

82 
*} 

83 

84 
constdefs 

85 
wf_mdecl :: "prog \<Rightarrow> qtname \<Rightarrow> mdecl \<Rightarrow> bool" 

86 
"wf_mdecl G C \<equiv> 

87 
\<lambda>(sig,m). 

88 
wf_mhead G (pid C) sig (mhead m) \<and> 

89 
unique (lcls (mbody m)) \<and> 

90 
(\<forall>(vn,T)\<in>set (lcls (mbody m)). is_acc_type G (pid C) T) \<and> 

91 
(\<forall>pn\<in>set (pars m). table_of (lcls (mbody m)) pn = None) \<and> 

92 
is_class G C \<and> 

93 
\<lparr>prg=G,cls=C, 

94 
lcl=\<lambda> k. 

95 
(case k of 

96 
EName e 

97 
\<Rightarrow> (case e of 

98 
VNam v 

99 
\<Rightarrow>(table_of (lcls (mbody m))((pars m)[\<mapsto>](parTs sig))) v 

100 
 Res \<Rightarrow> Some (resTy m)) 

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

101 
 This \<Rightarrow> if is_static m then None else Some (Class C)) 
12854  102 
\<rparr>\<turnstile>(stmt (mbody m))\<Colon>\<surd>" 
103 

104 
lemma wf_mheadI: 

105 
"\<lbrakk>length (parTs sig) = length (pars m); \<forall>T\<in>set (parTs sig). is_acc_type G P T; 

12893  106 
is_acc_type G P (resTy m); distinct (pars m)\<rbrakk> \<Longrightarrow> 
12854  107 
wf_mhead G P sig m" 
108 
apply (unfold wf_mhead_def) 

109 
apply (simp (no_asm_simp)) 

110 
done 

111 

112 
lemma wf_mdeclI: "\<lbrakk> 

113 
wf_mhead G (pid C) sig (mhead m); unique (lcls (mbody m)); 

114 
(\<forall>pn\<in>set (pars m). table_of (lcls (mbody m)) pn = None); 

115 
\<forall>(vn,T)\<in>set (lcls (mbody m)). is_acc_type G (pid C) T; 

116 
is_class G C; 

117 
\<lparr>prg=G,cls=C, 

118 
lcl=\<lambda> k. 

119 
(case k of 

120 
EName e 

121 
\<Rightarrow> (case e of 

122 
VNam v 

123 
\<Rightarrow> (table_of (lcls (mbody m))((pars m)[\<mapsto>](parTs sig))) v 

124 
 Res \<Rightarrow> Some (resTy m)) 

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

125 
 This \<Rightarrow> if is_static m then None else Some (Class C)) 
12854  126 
\<rparr>\<turnstile>(stmt (mbody m))\<Colon>\<surd> 
127 
\<rbrakk> \<Longrightarrow> 

128 
wf_mdecl G C (sig,m)" 

129 
apply (unfold wf_mdecl_def) 

130 
apply simp 

131 
done 

132 

133 

134 
lemma wf_mdeclD1: 

135 
"wf_mdecl G C (sig,m) \<Longrightarrow> 

136 
wf_mhead G (pid C) sig (mhead m) \<and> unique (lcls (mbody m)) \<and> 

137 
(\<forall>pn\<in>set (pars m). table_of (lcls (mbody m)) pn = None) \<and> 

138 
(\<forall>(vn,T)\<in>set (lcls (mbody m)). is_acc_type G (pid C) T)" 

139 
apply (unfold wf_mdecl_def) 

140 
apply auto 

141 
done 

142 

143 
lemma wf_mdecl_bodyD: 

144 
"wf_mdecl G C (sig,m) \<Longrightarrow> 

145 
(\<exists>T. \<lparr>prg=G,cls=C, 

146 
lcl = \<lambda> k. 

147 
(case k of 

148 
EName e 

149 
\<Rightarrow> (case e of 

150 
VNam v \<Rightarrow> (table_of (lcls (mbody m))((pars m)[\<mapsto>](parTs sig))) v 

151 
 Res \<Rightarrow> Some (resTy m)) 

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

152 
 This \<Rightarrow> if is_static m then None else Some (Class C)) 
12854  153 
\<rparr>\<turnstile>Body C (stmt (mbody m))\<Colon>T \<and> G\<turnstile>T\<preceq>(resTy m))" 
154 
apply (unfold wf_mdecl_def) 

155 
apply clarify 

156 
apply (rule_tac x="(resTy m)" in exI) 

157 
apply (unfold wf_mhead_def) 

158 
apply (auto simp add: wf_mhead_def is_acc_type_def intro: wt.Body ) 

159 
done 

160 

161 

162 
(* 

163 
lemma static_Object_methodsE [elim!]: 

164 
"\<lbrakk>wf_mdecl G Object (sig, m);static m\<rbrakk> \<Longrightarrow> R" 

165 
apply (unfold wf_mdecl_def) 

166 
apply auto 

167 
done 

168 
*) 

169 

170 
lemma rT_is_acc_type: 

171 
"wf_mhead G P sig m \<Longrightarrow> is_acc_type G P (resTy m)" 

172 
apply (unfold wf_mhead_def) 

173 
apply auto 

174 
done 

175 

176 
section "wellformed interface declarations" 

177 
(* wellformed interface declaration, cf. 9.1, 9.1.2.1, 9.1.3, 9.4 *) 

178 

179 
text {* 

180 
A interface declaration is wellformed if: 

181 
\begin{itemize} 

182 
\item the interface hierarchy is wellstructured 

183 
\item there is no class with the same name 

184 
\item the method heads are wellformed and not static and have Public access 

185 
\item the methods are uniquely named 

186 
\item all superinterfaces are accessible 

187 
\item the result type of a method overriding a method of Object widens to the 

188 
result type of the overridden method. 

189 
Shadowing static methods is forbidden. 

190 
\item the result type of a method overriding a set of methods defined in the 

191 
superinterfaces widens to each of the corresponding result types 

192 
\end{itemize} 

193 
*} 

194 
constdefs 

195 
wf_idecl :: "prog \<Rightarrow> idecl \<Rightarrow> bool" 

196 
"wf_idecl G \<equiv> 

197 
\<lambda>(I,i). 

198 
ws_idecl G I (isuperIfs i) \<and> 

199 
\<not>is_class G I \<and> 

200 
(\<forall>(sig,mh)\<in>set (imethods i). wf_mhead G (pid I) sig mh \<and> 

201 
\<not>is_static mh \<and> 

202 
accmodi mh = Public) \<and> 

203 
unique (imethods i) \<and> 

204 
(\<forall> J\<in>set (isuperIfs i). is_acc_iface G (pid I) J) \<and> 

205 
(table_of (imethods i) 

206 
hiding (methd G Object) 

207 
under (\<lambda> new old. accmodi old \<noteq> Private) 

208 
entails (\<lambda>new old. G\<turnstile>resTy new\<preceq>resTy old \<and> 

209 
is_static new = is_static old)) \<and> 

210 
(o2s \<circ> table_of (imethods i) 

211 
hidings Un_tables((\<lambda>J.(imethds G J))`set (isuperIfs i)) 

212 
entails (\<lambda>new old. G\<turnstile>resTy new\<preceq>resTy old))" 

213 

214 
lemma wf_idecl_mhead: "\<lbrakk>wf_idecl G (I,i); (sig,mh)\<in>set (imethods i)\<rbrakk> \<Longrightarrow> 

215 
wf_mhead G (pid I) sig mh \<and> \<not>is_static mh \<and> accmodi mh = Public" 

216 
apply (unfold wf_idecl_def) 

217 
apply auto 

218 
done 

219 

220 
lemma wf_idecl_hidings: 

221 
"wf_idecl G (I, i) \<Longrightarrow> 

222 
(\<lambda>s. o2s (table_of (imethods i) s)) 

223 
hidings Un_tables ((\<lambda>J. imethds G J) ` set (isuperIfs i)) 

224 
entails \<lambda>new old. G\<turnstile>resTy new\<preceq>resTy old" 

225 
apply (unfold wf_idecl_def o_def) 

226 
apply simp 

227 
done 

228 

229 
lemma wf_idecl_hiding: 

230 
"wf_idecl G (I, i) \<Longrightarrow> 

231 
(table_of (imethods i) 

232 
hiding (methd G Object) 

233 
under (\<lambda> new old. accmodi old \<noteq> Private) 

234 
entails (\<lambda>new old. G\<turnstile>resTy new\<preceq>resTy old \<and> 

235 
is_static new = is_static old))" 

236 
apply (unfold wf_idecl_def) 

237 
apply simp 

238 
done 

239 

240 
lemma wf_idecl_supD: 

241 
"\<lbrakk>wf_idecl G (I,i); J \<in> set (isuperIfs i)\<rbrakk> 

242 
\<Longrightarrow> is_acc_iface G (pid I) J \<and> (J, I) \<notin> (subint1 G)^+" 

243 
apply (unfold wf_idecl_def ws_idecl_def) 

244 
apply auto 

245 
done 

246 

247 
section "wellformed class declarations" 

248 
(* wellformed class declaration, cf. 8.1, 8.1.2.1, 8.1.2.2, 8.1.3, 8.1.4 and 

249 
class method declaration, cf. 8.4.3.3, 8.4.6.1, 8.4.6.2, 8.4.6.3, 8.4.6.4 *) 

250 

251 
text {* 

252 
A class declaration is wellformed if: 

253 
\begin{itemize} 

254 
\item there is no interface with the same name 

255 
\item all superinterfaces are accessible and for all methods implementing 

256 
an interface method the result type widens to the result type of 

257 
the interface method, the method is not static and offers at least 

258 
as much access 

259 
(this actually means that the method has Public access, since all 

260 
interface methods have public access) 

261 
\item all field declarations are wellformed and the field names are unique 

262 
\item all method declarations are wellformed and the method names are unique 

263 
\item the initialization statement is welltyped 

264 
\item the classhierarchy is wellstructured 

265 
\item Unless the class is Object: 

266 
\begin{itemize} 

267 
\item the superclass is accessible 

268 
\item for all methods overriding another method (of a superclass )the 

269 
result type widens to the result type of the overridden method, 

270 
the access modifier of the new method provides at least as much 

271 
access as the overwritten one. 

272 
\item for all methods hiding a method (of a superclass) the hidden 

273 
method must be static and offer at least as much access rights. 

274 
Remark: In contrast to the Java Language Specification we don't 

275 
restrict the result types of the method 

276 
(as in case of overriding), because there seems to be no reason, 

277 
since there is no dynamic binding of static methods. 

278 
(cf. 8.4.6.3 vs. 15.12.1). 

279 
Stricly speaking the restrictions on the access rights aren't 

280 
necessary to, since the static type and the access rights 

281 
together determine which method is to be called statically. 

282 
But if a class gains more then one static method with the 

283 
same signature due to inheritance, it is confusing when the 

284 
method selection depends on the access rights only: 

285 
e.g. 

286 
Class C declares static public method foo(). 

287 
Class D is subclass of C and declares static method foo() 

288 
with default package access. 

289 
D.foo() ? if this call is in the same package as D then 

290 
foo of class D is called, otherwise foo of class C. 

291 
\end{itemize} 

292 

293 
\end{itemize} 

294 
*} 

295 
(* to Table *) 

296 
constdefs entails:: "('a,'b) table \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> bool" 

297 
("_ entails _" 20) 

298 
"t entails P \<equiv> \<forall>k. \<forall> x \<in> t k: P x" 

299 

300 
lemma entailsD: 

301 
"\<lbrakk>t entails P; t k = Some x\<rbrakk> \<Longrightarrow> P x" 

302 
by (simp add: entails_def) 

303 

304 
lemma empty_entails[simp]: "empty entails P" 

305 
by (simp add: entails_def) 

306 

307 
constdefs 

308 
wf_cdecl :: "prog \<Rightarrow> cdecl \<Rightarrow> bool" 

309 
"wf_cdecl G \<equiv> 

310 
\<lambda>(C,c). 

311 
\<not>is_iface G C \<and> 

312 
(\<forall>I\<in>set (superIfs c). is_acc_iface G (pid C) I \<and> 

313 
(\<forall>s. \<forall> im \<in> imethds G I s. 

314 
(\<exists> cm \<in> methd G C s: G\<turnstile>resTy cm\<preceq>resTy im \<and> 

315 
\<not> is_static cm \<and> 

316 
accmodi im \<le> accmodi cm))) \<and> 

317 
(\<forall>f\<in>set (cfields c). wf_fdecl G (pid C) f) \<and> unique (cfields c) \<and> 

318 
(\<forall>m\<in>set (methods c). wf_mdecl G C m) \<and> unique (methods c) \<and> 

319 
\<lparr>prg=G,cls=C,lcl=empty\<rparr>\<turnstile>(init c)\<Colon>\<surd> \<and> ws_cdecl G C (super c) \<and> 

320 
(C \<noteq> Object \<longrightarrow> 

321 
(is_acc_class G (pid C) (super c) \<and> 

322 
(table_of (map (\<lambda> (s,m). (s,C,m)) (methods c)) 

323 
entails (\<lambda> new. \<forall> old sig. 

324 
(G,sig\<turnstile>new overrides\<^sub>S old 

325 
\<longrightarrow> (G\<turnstile>resTy new\<preceq>resTy old \<and> 

326 
accmodi old \<le> accmodi new \<and> 

327 
\<not>is_static old)) \<and> 

328 
(G,sig\<turnstile>new hides old 

329 
\<longrightarrow> (accmodi old \<le> accmodi new \<and> 

330 
is_static old)))) 

331 
))" 

332 

333 
(* 

334 
constdefs 

335 
wf_cdecl :: "prog \<Rightarrow> cdecl \<Rightarrow> bool" 

336 
"wf_cdecl G \<equiv> 

337 
\<lambda>(C,c). 

338 
\<not>is_iface G C \<and> 

339 
(\<forall>I\<in>set (superIfs c). is_acc_iface G (pid C) I \<and> 

340 
(\<forall>s. \<forall> im \<in> imethds G I s. 

341 
(\<exists> cm \<in> methd G C s: G\<turnstile>resTy (mthd cm)\<preceq>resTy (mthd im) \<and> 

342 
\<not> is_static cm \<and> 

343 
accmodi im \<le> accmodi cm))) \<and> 

344 
(\<forall>f\<in>set (cfields c). wf_fdecl G (pid C) f) \<and> unique (cfields c) \<and> 

345 
(\<forall>m\<in>set (methods c). wf_mdecl G C m) \<and> unique (methods c) \<and> 

346 
\<lparr>prg=G,cls=C,lcl=empty\<rparr>\<turnstile>(init c)\<Colon>\<surd> \<and> ws_cdecl G C (super c) \<and> 

347 
(C \<noteq> Object \<longrightarrow> 

348 
(is_acc_class G (pid C) (super c) \<and> 

349 
(table_of (map (\<lambda> (s,m). (s,C,m)) (methods c)) 

350 
hiding methd G (super c) 

351 
under (\<lambda> new old. G\<turnstile>new overrides old) 

352 
entails (\<lambda> new old. 

353 
(G\<turnstile>resTy (mthd new)\<preceq>resTy (mthd old) \<and> 

354 
accmodi old \<le> accmodi new \<and> 

355 
\<not> is_static old))) \<and> 

356 
(table_of (map (\<lambda> (s,m). (s,C,m)) (methods c)) 

357 
hiding methd G (super c) 

358 
under (\<lambda> new old. G\<turnstile>new hides old) 

359 
entails (\<lambda> new old. is_static old \<and> 

360 
accmodi old \<le> accmodi new)) \<and> 

361 
(table_of (cfields c) hiding accfield G C (super c) 

362 
entails (\<lambda> newF oldF. accmodi oldF \<le> access newF))))" 

363 
*) 

364 

365 
lemma wf_cdecl_unique: 

366 
"wf_cdecl G (C,c) \<Longrightarrow> unique (cfields c) \<and> unique (methods c)" 

367 
apply (unfold wf_cdecl_def) 

368 
apply auto 

369 
done 

370 

371 
lemma wf_cdecl_fdecl: 

372 
"\<lbrakk>wf_cdecl G (C,c); f\<in>set (cfields c)\<rbrakk> \<Longrightarrow> wf_fdecl G (pid C) f" 

373 
apply (unfold wf_cdecl_def) 

374 
apply auto 

375 
done 

376 

377 
lemma wf_cdecl_mdecl: 

378 
"\<lbrakk>wf_cdecl G (C,c); m\<in>set (methods c)\<rbrakk> \<Longrightarrow> wf_mdecl G C m" 

379 
apply (unfold wf_cdecl_def) 

380 
apply auto 

381 
done 

382 

383 
lemma wf_cdecl_impD: 

384 
"\<lbrakk>wf_cdecl G (C,c); I\<in>set (superIfs c)\<rbrakk> 

385 
\<Longrightarrow> is_acc_iface G (pid C) I \<and> 

386 
(\<forall>s. \<forall>im \<in> imethds G I s. 

387 
(\<exists>cm \<in> methd G C s: G\<turnstile>resTy cm\<preceq>resTy im \<and> \<not>is_static cm \<and> 

388 
accmodi im \<le> accmodi cm))" 

389 
apply (unfold wf_cdecl_def) 

390 
apply auto 

391 
done 

392 

393 
lemma wf_cdecl_supD: 

394 
"\<lbrakk>wf_cdecl G (C,c); C \<noteq> Object\<rbrakk> \<Longrightarrow> 

395 
is_acc_class G (pid C) (super c) \<and> (super c,C) \<notin> (subcls1 G)^+ \<and> 

396 
(table_of (map (\<lambda> (s,m). (s,C,m)) (methods c)) 

397 
entails (\<lambda> new. \<forall> old sig. 

398 
(G,sig\<turnstile>new overrides\<^sub>S old 

399 
\<longrightarrow> (G\<turnstile>resTy new\<preceq>resTy old \<and> 

400 
accmodi old \<le> accmodi new \<and> 

401 
\<not>is_static old)) \<and> 

402 
(G,sig\<turnstile>new hides old 

403 
\<longrightarrow> (accmodi old \<le> accmodi new \<and> 

404 
is_static old))))" 

405 
apply (unfold wf_cdecl_def ws_cdecl_def) 

406 
apply auto 

407 
done 

408 

409 

410 
lemma wf_cdecl_overrides_SomeD: 

411 
"\<lbrakk>wf_cdecl G (C,c); C \<noteq> Object; table_of (methods c) sig = Some newM; 

412 
G,sig\<turnstile>(C,newM) overrides\<^sub>S old 

413 
\<rbrakk> \<Longrightarrow> G\<turnstile>resTy newM\<preceq>resTy old \<and> 

414 
accmodi old \<le> accmodi newM \<and> 

415 
\<not> is_static old" 

416 
apply (drule (1) wf_cdecl_supD) 

417 
apply (clarify) 

418 
apply (drule entailsD) 

419 
apply (blast intro: table_of_map_SomeI) 

420 
apply (drule_tac x="old" in spec) 

421 
apply (auto dest: overrides_eq_sigD simp add: msig_def) 

422 
done 

423 

424 
lemma wf_cdecl_hides_SomeD: 

425 
"\<lbrakk>wf_cdecl G (C,c); C \<noteq> Object; table_of (methods c) sig = Some newM; 

426 
G,sig\<turnstile>(C,newM) hides old 

427 
\<rbrakk> \<Longrightarrow> accmodi old \<le> access newM \<and> 

428 
is_static old" 

429 
apply (drule (1) wf_cdecl_supD) 

430 
apply (clarify) 

431 
apply (drule entailsD) 

432 
apply (blast intro: table_of_map_SomeI) 

433 
apply (drule_tac x="old" in spec) 

434 
apply (auto dest: hides_eq_sigD simp add: msig_def) 

435 
done 

436 

437 
lemma wf_cdecl_wt_init: 

438 
"wf_cdecl G (C, c) \<Longrightarrow> \<lparr>prg=G,cls=C,lcl=empty\<rparr>\<turnstile>init c\<Colon>\<surd>" 

439 
apply (unfold wf_cdecl_def) 

440 
apply auto 

441 
done 

442 

443 

444 
section "wellformed programs" 

445 
(* wellformed program, cf. 8.1, 9.1 *) 

446 

447 
text {* 

448 
A program declaration is wellformed if: 

449 
\begin{itemize} 

450 
\item the class ObjectC of Object is defined 

451 
\item every method of has an access modifier distinct from Package. This is 

452 
necessary since every interface automatically inherits from Object. 

453 
We must know, that every time a Object method is "overriden" by an 

454 
interface method this is also overriden by the class implementing the 

455 
the interface (see @{text "implement_dynmethd and class_mheadsD"}) 

456 
\item all standard Exceptions are defined 

457 
\item all defined interfaces are wellformed 

458 
\item all defined classes are wellformed 

459 
\end{itemize} 

460 
*} 

461 
constdefs 

462 
wf_prog :: "prog \<Rightarrow> bool" 

463 
"wf_prog G \<equiv> let is = ifaces G; cs = classes G in 

464 
ObjectC \<in> set cs \<and> 

465 
(\<forall> m\<in>set Object_mdecls. accmodi m \<noteq> Package) \<and> 

466 
(\<forall>xn. SXcptC xn \<in> set cs) \<and> 

467 
(\<forall>i\<in>set is. wf_idecl G i) \<and> unique is \<and> 

468 
(\<forall>c\<in>set cs. wf_cdecl G c) \<and> unique cs" 

469 

470 
lemma wf_prog_idecl: "\<lbrakk>iface G I = Some i; wf_prog G\<rbrakk> \<Longrightarrow> wf_idecl G (I,i)" 

471 
apply (unfold wf_prog_def Let_def) 

472 
apply simp 

473 
apply (fast dest: map_of_SomeD) 

474 
done 

475 

476 
lemma wf_prog_cdecl: "\<lbrakk>class G C = Some c; wf_prog G\<rbrakk> \<Longrightarrow> wf_cdecl G (C,c)" 

477 
apply (unfold wf_prog_def Let_def) 

478 
apply simp 

479 
apply (fast dest: map_of_SomeD) 

480 
done 

481 

482 
lemma wf_prog_Object_mdecls: 

483 
"wf_prog G \<Longrightarrow> (\<forall> m\<in>set Object_mdecls. accmodi m \<noteq> Package)" 

484 
apply (unfold wf_prog_def Let_def) 

485 
apply simp 

486 
done 

487 

488 
lemma wf_prog_acc_superD: 

489 
"\<lbrakk>wf_prog G; class G C = Some c; C \<noteq> Object \<rbrakk> 

490 
\<Longrightarrow> is_acc_class G (pid C) (super c)" 

491 
by (auto dest: wf_prog_cdecl wf_cdecl_supD) 

492 

493 
lemma wf_ws_prog [elim!,simp]: "wf_prog G \<Longrightarrow> ws_prog G" 

494 
apply (unfold wf_prog_def Let_def) 

495 
apply (rule ws_progI) 

496 
apply (simp_all (no_asm)) 

497 
apply (auto simp add: is_acc_class_def is_acc_iface_def 

498 
dest!: wf_idecl_supD wf_cdecl_supD )+ 

499 
done 

500 

501 
lemma class_Object [simp]: 

502 
"wf_prog G \<Longrightarrow> 

503 
class G Object = Some \<lparr>access=Public,cfields=[],methods=Object_mdecls, 

504 
init=Skip,super=arbitrary,superIfs=[]\<rparr>" 

505 
apply (unfold wf_prog_def Let_def ObjectC_def) 

506 
apply (fast dest!: map_of_SomeI) 

507 
done 

508 

509 
lemma methd_Object[simp]: "wf_prog G \<Longrightarrow> methd G Object = 

510 
table_of (map (\<lambda>(s,m). (s, Object, m)) Object_mdecls)" 

511 
apply (subst methd_rec) 

512 
apply (auto simp add: Let_def) 

513 
done 

514 

515 
lemma wf_prog_Object_methd: 

516 
"\<lbrakk>wf_prog G; methd G Object sig = Some m\<rbrakk> \<Longrightarrow> accmodi m \<noteq> Package" 

517 
by (auto dest!: wf_prog_Object_mdecls) (auto dest!: map_of_SomeD) 

518 

519 
lemma wf_prog_Object_is_public[intro]: 

520 
"wf_prog G \<Longrightarrow> is_public G Object" 

521 
by (auto simp add: is_public_def dest: class_Object) 

522 

523 
lemma class_SXcpt [simp]: 

524 
"wf_prog G \<Longrightarrow> 

525 
class G (SXcpt xn) = Some \<lparr>access=Public,cfields=[],methods=SXcpt_mdecls, 

526 
init=Skip, 

527 
super=if xn = Throwable then Object 

528 
else SXcpt Throwable, 

529 
superIfs=[]\<rparr>" 

530 
apply (unfold wf_prog_def Let_def SXcptC_def) 

531 
apply (fast dest!: map_of_SomeI) 

532 
done 

533 

534 
lemma wf_ObjectC [simp]: 

535 
"wf_cdecl G ObjectC = (\<not>is_iface G Object \<and> Ball (set Object_mdecls) 

536 
(wf_mdecl G Object) \<and> unique Object_mdecls)" 

537 
apply (unfold wf_cdecl_def ws_cdecl_def ObjectC_def) 

538 
apply (simp (no_asm)) 

539 
done 

540 

541 
lemma Object_is_class [simp,elim!]: "wf_prog G \<Longrightarrow> is_class G Object" 

542 
apply (simp (no_asm_simp)) 

543 
done 

544 

545 
lemma Object_is_acc_class [simp,elim!]: "wf_prog G \<Longrightarrow> is_acc_class G S Object" 

546 
apply (simp (no_asm_simp) add: is_acc_class_def is_public_def 

547 
accessible_in_RefT_simp) 

548 
done 

549 

550 
lemma SXcpt_is_class [simp,elim!]: "wf_prog G \<Longrightarrow> is_class G (SXcpt xn)" 

551 
apply (simp (no_asm_simp)) 

552 
done 

553 

554 
lemma SXcpt_is_acc_class [simp,elim!]: 

555 
"wf_prog G \<Longrightarrow> is_acc_class G S (SXcpt xn)" 

556 
apply (simp (no_asm_simp) add: is_acc_class_def is_public_def 

557 
accessible_in_RefT_simp) 

558 
done 

559 

560 
lemma fields_Object [simp]: "wf_prog G \<Longrightarrow> DeclConcepts.fields G Object = []" 

561 
by (force intro: fields_emptyI) 

562 

563 
lemma accfield_Object [simp]: 

564 
"wf_prog G \<Longrightarrow> accfield G S Object = empty" 

565 
apply (unfold accfield_def) 

566 
apply (simp (no_asm_simp) add: Let_def) 

567 
done 

568 

569 
lemma fields_Throwable [simp]: 

570 
"wf_prog G \<Longrightarrow> DeclConcepts.fields G (SXcpt Throwable) = []" 

571 
by (force intro: fields_emptyI) 

572 

573 
lemma fields_SXcpt [simp]: "wf_prog G \<Longrightarrow> DeclConcepts.fields G (SXcpt xn) = []" 

574 
apply (case_tac "xn = Throwable") 

575 
apply (simp (no_asm_simp)) 

576 
by (force intro: fields_emptyI) 

577 

578 
lemmas widen_trans = ws_widen_trans [OF _ _ wf_ws_prog, elim] 

579 
lemma widen_trans2 [elim]: "\<lbrakk>G\<turnstile>U\<preceq>T; G\<turnstile>S\<preceq>U; wf_prog G\<rbrakk> \<Longrightarrow> G\<turnstile>S\<preceq>T" 

580 
apply (erule (2) widen_trans) 

581 
done 

582 

583 
lemma Xcpt_subcls_Throwable [simp]: 

584 
"wf_prog G \<Longrightarrow> G\<turnstile>SXcpt xn\<preceq>\<^sub>C SXcpt Throwable" 

585 
apply (rule SXcpt_subcls_Throwable_lemma) 

586 
apply auto 

587 
done 

588 

589 
lemma unique_fields: 

590 
"\<lbrakk>is_class G C; wf_prog G\<rbrakk> \<Longrightarrow> unique (DeclConcepts.fields G C)" 

591 
apply (erule ws_unique_fields) 

592 
apply (erule wf_ws_prog) 

593 
apply (erule (1) wf_prog_cdecl [THEN wf_cdecl_unique [THEN conjunct1]]) 

594 
done 

595 

596 
lemma fields_mono: 

597 
"\<lbrakk>table_of (DeclConcepts.fields G C) fn = Some f; G\<turnstile>D\<preceq>\<^sub>C C; 

598 
is_class G D; wf_prog G\<rbrakk> 

599 
\<Longrightarrow> table_of (DeclConcepts.fields G D) fn = Some f" 

600 
apply (rule map_of_SomeI) 

601 
apply (erule (1) unique_fields) 

602 
apply (erule (1) map_of_SomeD [THEN fields_mono_lemma]) 

603 
apply (erule wf_ws_prog) 

604 
done 

605 

606 

607 
lemma fields_is_type [elim]: 

608 
"\<lbrakk>table_of (DeclConcepts.fields G C) m = Some f; wf_prog G; is_class G C\<rbrakk> \<Longrightarrow> 

609 
is_type G (type f)" 

610 
apply (frule wf_ws_prog) 

611 
apply (force dest: fields_declC [THEN conjunct1] 

612 
wf_prog_cdecl [THEN wf_cdecl_fdecl] 

613 
simp add: wf_fdecl_def2 is_acc_type_def) 

614 
done 

615 

616 
lemma imethds_wf_mhead [rule_format (no_asm)]: 

617 
"\<lbrakk>m \<in> imethds G I sig; wf_prog G; is_iface G I\<rbrakk> \<Longrightarrow> 

618 
wf_mhead G (pid (decliface m)) sig (mthd m) \<and> 

619 
\<not> is_static m \<and> accmodi m = Public" 

620 
apply (frule wf_ws_prog) 

621 
apply (drule (2) imethds_declI [THEN conjunct1]) 

622 
apply clarify 

623 
apply (frule_tac I="(decliface m)" in wf_prog_idecl,assumption) 

624 
apply (drule wf_idecl_mhead) 

625 
apply (erule map_of_SomeD) 

626 
apply (cases m, simp) 

627 
done 

628 

629 
lemma methd_wf_mdecl: 

630 
"\<lbrakk>methd G C sig = Some m; wf_prog G; class G C = Some y\<rbrakk> \<Longrightarrow> 

631 
G\<turnstile>C\<preceq>\<^sub>C (declclass m) \<and> is_class G (declclass m) \<and> 

632 
wf_mdecl G (declclass m) (sig,(mthd m))" 

633 
apply (frule wf_ws_prog) 

634 
apply (drule (1) methd_declC) 

635 
apply fast 

636 
apply clarsimp 

637 
apply (frule (1) wf_prog_cdecl, erule wf_cdecl_mdecl, erule map_of_SomeD) 

638 
done 

639 

640 
(* 

641 
This lemma doesn't hold! 

642 
lemma methd_rT_is_acc_type: 

643 
"\<lbrakk>wf_prog G;methd G C C sig = Some (D,m); 

644 
class G C = Some y\<rbrakk> 

645 
\<Longrightarrow> is_acc_type G (pid C) (resTy m)" 

646 
The result Type is only visible in the scope of defining class D 

647 
"is_vis_type G (pid D) (resTy m)" but not necessarily in scope of class C! 

648 
(The same is true for the type of pramaters of a method) 

649 
*) 

650 

651 

652 
lemma methd_rT_is_type: 

653 
"\<lbrakk>wf_prog G;methd G C sig = Some m; 

654 
class G C = Some y\<rbrakk> 

655 
\<Longrightarrow> is_type G (resTy m)" 

656 
apply (drule (2) methd_wf_mdecl) 

657 
apply clarify 

658 
apply (drule wf_mdeclD1) 

659 
apply clarify 

660 
apply (drule rT_is_acc_type) 

661 
apply (cases m, simp add: is_acc_type_def) 

662 
done 

663 

664 
lemma accmethd_rT_is_type: 

665 
"\<lbrakk>wf_prog G;accmethd G S C sig = Some m; 

666 
class G C = Some y\<rbrakk> 

667 
\<Longrightarrow> is_type G (resTy m)" 

668 
by (auto simp add: accmethd_def 

669 
intro: methd_rT_is_type) 

670 

671 
lemma methd_Object_SomeD: 

672 
"\<lbrakk>wf_prog G;methd G Object sig = Some m\<rbrakk> 

673 
\<Longrightarrow> declclass m = Object" 

674 
by (auto dest: class_Object simp add: methd_rec ) 

675 

676 
lemma wf_imethdsD: 

677 
"\<lbrakk>im \<in> imethds G I sig;wf_prog G; is_iface G I\<rbrakk> 

678 
\<Longrightarrow> \<not>is_static im \<and> accmodi im = Public" 

679 
proof  

680 
assume asm: "wf_prog G" "is_iface G I" "im \<in> imethds G I sig" 

681 
have "wf_prog G \<longrightarrow> 

682 
(\<forall> i im. iface G I = Some i \<longrightarrow> im \<in> imethds G I sig 

683 
\<longrightarrow> \<not>is_static im \<and> accmodi im = Public)" (is "?P G I") 

684 
proof (rule iface_rec.induct,intro allI impI) 

685 
fix G I i im 

686 
assume hyp: "\<forall> J i. J \<in> set (isuperIfs i) \<and> ws_prog G \<and> iface G I = Some i 

687 
\<longrightarrow> ?P G J" 

688 
assume wf: "wf_prog G" and if_I: "iface G I = Some i" and 

689 
im: "im \<in> imethds G I sig" 

690 
show "\<not>is_static im \<and> accmodi im = Public" 

691 
proof  

692 
let ?inherited = "Un_tables (imethds G ` set (isuperIfs i))" 

693 
let ?new = "(o2s \<circ> table_of (map (\<lambda>(s, mh). (s, I, mh)) (imethods i)))" 

694 
from if_I wf im have imethds:"im \<in> (?inherited \<oplus>\<oplus> ?new) sig" 

695 
by (simp add: imethds_rec) 

696 
from wf if_I have 

697 
wf_supI: "\<forall> J. J \<in> set (isuperIfs i) \<longrightarrow> (\<exists> j. iface G J = Some j)" 

698 
by (blast dest: wf_prog_idecl wf_idecl_supD is_acc_ifaceD) 

699 
from wf if_I have 

700 
"\<forall> im \<in> set (imethods i). \<not> is_static im \<and> accmodi im = Public" 

701 
by (auto dest!: wf_prog_idecl wf_idecl_mhead) 

702 
then have new_ok: "\<forall> im. table_of (imethods i) sig = Some im 

703 
\<longrightarrow> \<not> is_static im \<and> accmodi im = Public" 

704 
by (auto dest!: table_of_Some_in_set) 

705 
show ?thesis 

706 
proof (cases "?new sig = {}") 

707 
case True 

708 
from True wf wf_supI if_I imethds hyp 

709 
show ?thesis by (auto simp del: split_paired_All) 

710 
next 

711 
case False 

712 
from False wf wf_supI if_I imethds new_ok hyp 

713 
show ?thesis by (auto dest: wf_idecl_hidings hidings_entailsD) 

714 
qed 

715 
qed 

716 
qed 

717 
with asm show ?thesis by (auto simp del: split_paired_All) 

718 
qed 

719 

720 
lemma wf_prog_hidesD: 

12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

721 
assumes hides: "G \<turnstile>new hides old" and wf: "wf_prog G" 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

722 
shows 
12854  723 
"accmodi old \<le> accmodi new \<and> 
724 
is_static old" 

725 
proof  

726 
from hides 

727 
obtain c where 

728 
clsNew: "class G (declclass new) = Some c" and 

729 
neqObj: "declclass new \<noteq> Object" 

730 
by (auto dest: hidesD declared_in_classD) 

731 
with hides obtain newM oldM where 

732 
newM: "table_of (methods c) (msig new) = Some newM" and 

733 
new: "new = (declclass new,(msig new),newM)" and 

734 
old: "old = (declclass old,(msig old),oldM)" and 

735 
"msig new = msig old" 

736 
by (cases new,cases old) 

737 
(auto dest: hidesD 

738 
simp add: cdeclaredmethd_def declared_in_def) 

739 
with hides 

740 
have hides': 

741 
"G,(msig new)\<turnstile>(declclass new,newM) hides (declclass old,oldM)" 

742 
by auto 

743 
from clsNew wf 

744 
have "wf_cdecl G (declclass new,c)" by (blast intro: wf_prog_cdecl) 

745 
note wf_cdecl_hides_SomeD [OF this neqObj newM hides'] 

746 
with new old 

747 
show ?thesis 

748 
by (cases new, cases old) auto 

749 
qed 

750 

751 
text {* Compare this lemma about static 

752 
overriding @{term "G \<turnstile>new overrides\<^sub>S old"} with the definition of 

753 
dynamic overriding @{term "G \<turnstile>new overrides old"}. 

754 
Conforming result types and restrictions on the access modifiers of the old 

755 
and the new method are not part of the predicate for static overriding. But 

756 
they are enshured in a wellfromed program. Dynamic overriding has 

757 
no restrictions on the access modifiers but enforces confrom result types 

758 
as precondition. But with some efford we can guarantee the access modifier 

759 
restriction for dynamic overriding, too. See lemma 

760 
@{text wf_prog_dyn_override_prop}. 

761 
*} 

762 
lemma wf_prog_stat_overridesD: 

12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

763 
assumes stat_override: "G \<turnstile>new overrides\<^sub>S old" and wf: "wf_prog G" 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

764 
shows 
12854  765 
"G\<turnstile>resTy new\<preceq>resTy old \<and> 
766 
accmodi old \<le> accmodi new \<and> 

767 
\<not> is_static old" 

768 
proof  

769 
from stat_override 

770 
obtain c where 

771 
clsNew: "class G (declclass new) = Some c" and 

772 
neqObj: "declclass new \<noteq> Object" 

773 
by (auto dest: stat_overrides_commonD declared_in_classD) 

774 
with stat_override obtain newM oldM where 

775 
newM: "table_of (methods c) (msig new) = Some newM" and 

776 
new: "new = (declclass new,(msig new),newM)" and 

777 
old: "old = (declclass old,(msig old),oldM)" and 

778 
"msig new = msig old" 

779 
by (cases new,cases old) 

780 
(auto dest: stat_overrides_commonD 

781 
simp add: cdeclaredmethd_def declared_in_def) 

782 
with stat_override 

783 
have stat_override': 

784 
"G,(msig new)\<turnstile>(declclass new,newM) overrides\<^sub>S (declclass old,oldM)" 

785 
by auto 

786 
from clsNew wf 

787 
have "wf_cdecl G (declclass new,c)" by (blast intro: wf_prog_cdecl) 

788 
note wf_cdecl_overrides_SomeD [OF this neqObj newM stat_override'] 

789 
with new old 

790 
show ?thesis 

791 
by (cases new, cases old) auto 

792 
qed 

793 

794 
lemma static_to_dynamic_overriding: 

12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

795 
assumes stat_override: "G\<turnstile>new overrides\<^sub>S old" and wf : "wf_prog G" 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

796 
shows "G\<turnstile>new overrides old" 
12854  797 
proof  
798 
from stat_override 

799 
show ?thesis (is "?Overrides new old") 

800 
proof (induct) 

801 
case (Direct new old superNew) 

802 
then have stat_override:"G\<turnstile>new overrides\<^sub>S old" 

803 
by (rule stat_overridesR.Direct) 

804 
from stat_override wf 

805 
have resTy_widen: "G\<turnstile>resTy new\<preceq>resTy old" and 

806 
not_static_old: "\<not> is_static old" 

807 
by (auto dest: wf_prog_stat_overridesD) 

808 
have not_private_new: "accmodi new \<noteq> Private" 

809 
proof  

810 
from stat_override 

811 
have "accmodi old \<noteq> Private" 

812 
by (rule no_Private_stat_override) 

813 
moreover 

814 
from stat_override wf 

815 
have "accmodi old \<le> accmodi new" 

816 
by (auto dest: wf_prog_stat_overridesD) 

817 
ultimately 

818 
show ?thesis 

819 
by (auto dest: acc_modi_bottom) 

820 
qed 

821 
with Direct resTy_widen not_static_old 

822 
show "?Overrides new old" 

823 
by (auto intro: overridesR.Direct) 

824 
next 

825 
case (Indirect inter new old) 

826 
then show "?Overrides new old" 

827 
by (blast intro: overridesR.Indirect) 

828 
qed 

829 
qed 

830 

831 
lemma non_Package_instance_method_inheritance: 

12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

832 
assumes old_inheritable: "G\<turnstile>Method old inheritable_in (pid C)" and 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

833 
accmodi_old: "accmodi old \<noteq> Package" and 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

834 
instance_method: "\<not> is_static old" and 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

835 
subcls: "G\<turnstile>C \<prec>\<^sub>C declclass old" and 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

836 
old_declared: "G\<turnstile>Method old declared_in (declclass old)" and 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

837 
wf: "wf_prog G" 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

838 
shows "G\<turnstile>Method old member_of C \<or> 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

839 
(\<exists> new. G\<turnstile> new overrides\<^sub>S old \<and> G\<turnstile>Method new member_of C)" 
12854  840 
proof  
841 
from wf have ws: "ws_prog G" by auto 

842 
from old_declared have iscls_declC_old: "is_class G (declclass old)" 

843 
by (auto simp add: declared_in_def cdeclaredmethd_def) 

844 
from subcls have iscls_C: "is_class G C" 

845 
by (blast dest: subcls_is_class) 

846 
from iscls_C ws old_inheritable subcls 

847 
show ?thesis (is "?P C old") 

848 
proof (induct rule: ws_class_induct') 

849 
case Object 

850 
assume "G\<turnstile>Object\<prec>\<^sub>C declclass old" 

851 
then show "?P Object old" 

852 
by blast 

853 
next 

854 
case (Subcls C c) 

855 
assume cls_C: "class G C = Some c" and 

856 
neq_C_Obj: "C \<noteq> Object" and 

857 
hyp: "\<lbrakk>G \<turnstile>Method old inheritable_in pid (super c); 

858 
G\<turnstile>super c\<prec>\<^sub>C declclass old\<rbrakk> \<Longrightarrow> ?P (super c) old" and 

859 
inheritable: "G \<turnstile>Method old inheritable_in pid C" and 

860 
subclsC: "G\<turnstile>C\<prec>\<^sub>C declclass old" 

861 
from cls_C neq_C_Obj 

862 
have super: "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 super c" 

863 
by (rule subcls1I) 

864 
from wf cls_C neq_C_Obj 

865 
have accessible_super: "G\<turnstile>(Class (super c)) accessible_in (pid C)" 

866 
by (auto dest: wf_prog_cdecl wf_cdecl_supD is_acc_classD) 

867 
{ 

868 
fix old 

869 
assume member_super: "G\<turnstile>Method old member_of (super c)" 

870 
assume inheritable: "G \<turnstile>Method old inheritable_in pid C" 

871 
assume instance_method: "\<not> is_static old" 

872 
from member_super 

873 
have old_declared: "G\<turnstile>Method old declared_in (declclass old)" 

874 
by (cases old) (auto dest: member_of_declC) 

875 
have "?P C old" 

876 
proof (cases "G\<turnstile>mid (msig old) undeclared_in C") 

877 
case True 

878 
with inheritable super accessible_super member_super 

879 
have "G\<turnstile>Method old member_of C" 

880 
by (cases old) (auto intro: members.Inherited) 

881 
then show ?thesis 

882 
by auto 

883 
next 

884 
case False 

885 
then obtain new_member where 

886 
"G\<turnstile>new_member declared_in C" and 

887 
"mid (msig old) = memberid new_member" 

888 
by (auto dest: not_undeclared_declared) 

889 
then obtain new where 

890 
new: "G\<turnstile>Method new declared_in C" and 

891 
eq_sig: "msig old = msig new" and 

892 
declC_new: "declclass new = C" 

893 
by (cases new_member) auto 

894 
then have member_new: "G\<turnstile>Method new member_of C" 

895 
by (cases new) (auto intro: members.Immediate) 

896 
from declC_new super member_super 

897 
have subcls_new_old: "G\<turnstile>declclass new \<prec>\<^sub>C declclass old" 

898 
by (auto dest!: member_of_subclseq_declC 

899 
dest: r_into_trancl intro: trancl_rtrancl_trancl) 

900 
show ?thesis 

901 
proof (cases "is_static new") 

902 
case False 

903 
with eq_sig declC_new new old_declared inheritable 

904 
super member_super subcls_new_old 

905 
have "G\<turnstile>new overrides\<^sub>S old" 

906 
by (auto intro!: stat_overridesR.Direct) 

907 
with member_new show ?thesis 

908 
by blast 

909 
next 

910 
case True 

911 
with eq_sig declC_new subcls_new_old new old_declared inheritable 

912 
have "G\<turnstile>new hides old" 

913 
by (auto intro: hidesI) 

914 
with wf 

915 
have "is_static old" 

916 
by (blast dest: wf_prog_hidesD) 

917 
with instance_method 

918 
show ?thesis 

919 
by (contradiction) 

920 
qed 

921 
qed 

922 
} note hyp_member_super = this 

923 
from subclsC cls_C 

924 
have "G\<turnstile>(super c)\<preceq>\<^sub>C declclass old" 

925 
by (rule subcls_superD) 

926 
then 

927 
show "?P C old" 

928 
proof (cases rule: subclseq_cases) 

929 
case Eq 

930 
assume "super c = declclass old" 

931 
with old_declared 

932 
have "G\<turnstile>Method old member_of (super c)" 

933 
by (cases old) (auto intro: members.Immediate) 

934 
with inheritable instance_method 

935 
show ?thesis 

936 
by (blast dest: hyp_member_super) 

937 
next 

938 
case Subcls 

939 
assume "G\<turnstile>super c\<prec>\<^sub>C declclass old" 

940 
moreover 

941 
from inheritable accmodi_old 

942 
have "G \<turnstile>Method old inheritable_in pid (super c)" 

943 
by (cases "accmodi old") (auto simp add: inheritable_in_def) 

944 
ultimately 

945 
have "?P (super c) old" 

946 
by (blast dest: hyp) 

947 
then show ?thesis 

948 
proof 

949 
assume "G \<turnstile>Method old member_of super c" 

950 
with inheritable instance_method 

951 
show ?thesis 

952 
by (blast dest: hyp_member_super) 

953 
next 

954 
assume "\<exists>new. G \<turnstile> new overrides\<^sub>S old \<and> G \<turnstile>Method new member_of super c" 

955 
then obtain super_new where 

956 
super_new_override: "G \<turnstile> super_new overrides\<^sub>S old" and 

957 
super_new_member: "G \<turnstile>Method super_new member_of super c" 

958 
by blast 

959 
from super_new_override wf 

960 
have "accmodi old \<le> accmodi super_new" 

961 
by (auto dest: wf_prog_stat_overridesD) 

962 
with inheritable accmodi_old 

963 
have "G \<turnstile>Method super_new inheritable_in pid C" 

964 
by (auto simp add: inheritable_in_def 

965 
split: acc_modi.splits 

966 
dest: acc_modi_le_Dests) 

967 
moreover 

968 
from super_new_override 

969 
have "\<not> is_static super_new" 

970 
by (auto dest: stat_overrides_commonD) 

971 
moreover 

972 
note super_new_member 

973 
ultimately have "?P C super_new" 

974 
by (auto dest: hyp_member_super) 

975 
then show ?thesis 

976 
proof 

977 
assume "G \<turnstile>Method super_new member_of C" 

978 
with super_new_override 

979 
show ?thesis 

980 
by blast 

981 
next 

982 
assume "\<exists>new. G \<turnstile> new overrides\<^sub>S super_new \<and> 

983 
G \<turnstile>Method new member_of C" 

984 
with super_new_override show ?thesis 

985 
by (blast intro: stat_overridesR.Indirect) 

986 
qed 

987 
qed 

988 
qed 

989 
qed 

990 
qed 

991 

992 
lemma non_Package_instance_method_inheritance_cases [consumes 6, 

993 
case_names Inheritance Overriding]: 

12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

994 
assumes old_inheritable: "G\<turnstile>Method old inheritable_in (pid C)" and 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

995 
accmodi_old: "accmodi old \<noteq> Package" and 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

996 
instance_method: "\<not> is_static old" and 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

997 
subcls: "G\<turnstile>C \<prec>\<^sub>C declclass old" and 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

998 
old_declared: "G\<turnstile>Method old declared_in (declclass old)" and 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

999 
wf: "wf_prog G" and 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

1000 
inheritance: "G\<turnstile>Method old member_of C \<Longrightarrow> P" and 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

1001 
overriding: "\<And> new. 
12854  1002 
\<lbrakk>G\<turnstile> new overrides\<^sub>S old;G\<turnstile>Method new member_of C\<rbrakk> 
1003 
\<Longrightarrow> P" 

12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

1004 
shows P 
12854  1005 
proof  
1006 
from old_inheritable accmodi_old instance_method subcls old_declared wf 

1007 
inheritance overriding 

1008 
show ?thesis 

1009 
by (auto dest: non_Package_instance_method_inheritance) 

1010 
qed 

1011 

1012 
lemma dynamic_to_static_overriding: 

12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

1013 
assumes dyn_override: "G\<turnstile> new overrides old" and 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

1014 
accmodi_old: "accmodi old \<noteq> Package" and 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

1015 
wf: "wf_prog G" 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

1016 
shows "G\<turnstile> new overrides\<^sub>S old" 
12854  1017 
proof  
1018 
from dyn_override accmodi_old 

1019 
show ?thesis (is "?Overrides new old") 

1020 
proof (induct rule: overridesR.induct) 

1021 
case (Direct new old) 

1022 
assume new_declared: "G\<turnstile>Method new declared_in declclass new" 

1023 
assume eq_sig_new_old: "msig new = msig old" 

1024 
assume subcls_new_old: "G\<turnstile>declclass new \<prec>\<^sub>C declclass old" 

1025 
assume "G \<turnstile>Method old inheritable_in pid (declclass new)" and 

1026 
"accmodi old \<noteq> Package" and 

1027 
"\<not> is_static old" and 

1028 
"G\<turnstile>declclass new\<prec>\<^sub>C declclass old" and 

1029 
"G\<turnstile>Method old declared_in declclass old" 

1030 
from this wf 

1031 
show "?Overrides new old" 

1032 
proof (cases rule: non_Package_instance_method_inheritance_cases) 

1033 
case Inheritance 

1034 
assume "G \<turnstile>Method old member_of declclass new" 

1035 
then have "G\<turnstile>mid (msig old) undeclared_in declclass new" 

1036 
proof cases 

1037 
case Immediate 

1038 
with subcls_new_old wf show ?thesis 

1039 
by (auto dest: subcls_irrefl) 

1040 
next 

1041 
case Inherited 

1042 
then show ?thesis 

1043 
by (cases old) auto 

1044 
qed 

1045 
with eq_sig_new_old new_declared 

1046 
show ?thesis 

1047 
by (cases old,cases new) (auto dest!: declared_not_undeclared) 

1048 
next 

1049 
case (Overriding new') 

1050 
assume stat_override_new': "G \<turnstile> new' overrides\<^sub>S old" 

1051 
then have "msig new' = msig old" 

1052 
by (auto dest: stat_overrides_commonD) 

1053 
with eq_sig_new_old have eq_sig_new_new': "msig new=msig new'" 

1054 
by simp 

1055 
assume "G \<turnstile>Method new' member_of declclass new" 

1056 
then show ?thesis 

1057 
proof (cases) 

1058 
case Immediate 

1059 
then have declC_new: "declclass new' = declclass new" 

1060 
by auto 

1061 
from Immediate 

1062 
have "G\<turnstile>Method new' declared_in declclass new" 

1063 
by (cases new') auto 

1064 
with new_declared eq_sig_new_new' declC_new 

1065 
have "new=new'" 

1066 
by (cases new, cases new') (auto dest: unique_declared_in) 

1067 
with stat_override_new' 

1068 
show ?thesis 

1069 
by simp 

1070 
next 

1071 
case Inherited 

1072 
then have "G\<turnstile>mid (msig new') undeclared_in declclass new" 

1073 
by (cases new') (auto) 

1074 
with eq_sig_new_new' new_declared 

1075 
show ?thesis 

1076 
by (cases new,cases new') (auto dest!: declared_not_undeclared) 

1077 
qed 

1078 
qed 

1079 
next 

1080 
case (Indirect inter new old) 

1081 
assume accmodi_old: "accmodi old \<noteq> Package" 

1082 
assume "accmodi old \<noteq> Package \<Longrightarrow> G \<turnstile> inter overrides\<^sub>S old" 

1083 
with accmodi_old 

1084 
have stat_override_inter_old: "G \<turnstile> inter overrides\<^sub>S old" 

1085 
by blast 

1086 
moreover 

1087 
assume hyp_inter: "accmodi inter \<noteq> Package \<Longrightarrow> G \<turnstile> new overrides\<^sub>S inter" 

1088 
moreover 

1089 
have "accmodi inter \<noteq> Package" 

1090 
proof  

1091 
from stat_override_inter_old wf 

1092 
have "accmodi old \<le> accmodi inter" 

1093 
by (auto dest: wf_prog_stat_overridesD) 

1094 
with stat_override_inter_old accmodi_old 

1095 
show ?thesis 

1096 
by (auto dest!: no_Private_stat_override 

1097 
split: acc_modi.splits 

1098 
dest: acc_modi_le_Dests) 

1099 
qed 

1100 
ultimately show "?Overrides new old" 

1101 
by (blast intro: stat_overridesR.Indirect) 

1102 
qed 

1103 
qed 

1104 

1105 
lemma wf_prog_dyn_override_prop: 

12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

1106 
assumes dyn_override: "G \<turnstile> new overrides old" and 
12854  1107 
wf: "wf_prog G" 
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

1108 
shows "accmodi old \<le> accmodi new" 
12854  1109 
proof (cases "accmodi old = Package") 
1110 
case True 

1111 
note old_Package = this 

1112 
show ?thesis 

1113 
proof (cases "accmodi old \<le> accmodi new") 

1114 
case True then show ?thesis . 

1115 
next 

1116 
case False 

1117 
with old_Package 

1118 
have "accmodi new = Private" 

1119 
by (cases "accmodi new") (auto simp add: le_acc_def less_acc_def) 

1120 
with dyn_override 

1121 
show ?thesis 

1122 
by (auto dest: overrides_commonD) 

1123 
qed 

1124 
next 

1125 
case False 

1126 
with dyn_override wf 

1127 
have "G \<turnstile> new overrides\<^sub>S old" 

1128 
by (blast intro: dynamic_to_static_overriding) 

1129 
with wf 

1130 
show ?thesis 

1131 
by (blast dest: wf_prog_stat_overridesD) 

1132 
qed 

1133 

1134 
lemma overrides_Package_old: 

12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

1135 
assumes dyn_override: "G \<turnstile> new overrides old" and 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

1136 
accmodi_new: "accmodi new = Package" and 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

1137 
wf: "wf_prog G " 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

1138 
shows "accmodi old = Package" 
12854  1139 
proof (cases "accmodi old") 
1140 
case Private 

1141 
with dyn_override show ?thesis 

1142 
by (simp add: no_Private_override) 

1143 
next 

1144 
case Package 

1145 
then show ?thesis . 

1146 
next 

1147 
case Protected 

1148 
with dyn_override wf 

1149 
have "G \<turnstile> new overrides\<^sub>S old" 

1150 
by (auto intro: dynamic_to_static_overriding) 

1151 
with wf 

1152 
have "accmodi old \<le> accmodi new" 

1153 
by (auto dest: wf_prog_stat_overridesD) 

1154 
with Protected accmodi_new 

1155 
show ?thesis 

1156 
by (simp add: less_acc_def le_acc_def) 

1157 
next 

1158 
case Public 

1159 
with dyn_override wf 

1160 
have "G \<turnstile> new overrides\<^sub>S old" 

1161 
by (auto intro: dynamic_to_static_overriding) 

1162 
with wf 

1163 
have "accmodi old \<le> accmodi new" 

1164 
by (auto dest: wf_prog_stat_overridesD) 

1165 
with Public accmodi_new 

1166 
show ?thesis 

1167 
by (simp add: less_acc_def le_acc_def) 

1168 
qed 

1169 

1170 
lemma dyn_override_Package: 

12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

1171 
assumes dyn_override: "G \<turnstile> new overrides old" and 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

1172 
accmodi_old: "accmodi old = Package" and 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

1173 
accmodi_new: "accmodi new = Package" and 
12854  1174 
wf: "wf_prog G" 
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

1175 
shows "pid (declclass old) = pid (declclass new)" 
12854  1176 
proof  
1177 
from dyn_override accmodi_old accmodi_new 

1178 
show ?thesis (is "?EqPid old new") 

1179 
proof (induct rule: overridesR.induct) 

1180 
case (Direct new old) 

1181 
assume "accmodi old = Package" 

1182 
"G \<turnstile>Method old inheritable_in pid (declclass new)" 

1183 
then show "pid (declclass old) = pid (declclass new)" 

1184 
by (auto simp add: inheritable_in_def) 

1185 
next 

1186 
case (Indirect inter new old) 

1187 
assume accmodi_old: "accmodi old = Package" and 

1188 
accmodi_new: "accmodi new = Package" 

1189 
assume "G \<turnstile> new overrides inter" 

1190 
with accmodi_new wf 

1191 
have "accmodi inter = Package" 

1192 
by (auto intro: overrides_Package_old) 

1193 
with Indirect 

1194 
show "pid (declclass old) = pid (declclass new)" 

1195 
by auto 

1196 
qed 

1197 
qed 

1198 

1199 
lemma dyn_override_Package_escape: 

12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

1200 
assumes dyn_override: "G \<turnstile> new overrides old" and 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

1201 
accmodi_old: "accmodi old = Package" and 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

1202 
outside_pack: "pid (declclass old) \<noteq> pid (declclass new)" and 
12854  1203 
wf: "wf_prog G" 
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

1204 
shows "\<exists> inter. G \<turnstile> new overrides inter \<and> G \<turnstile> inter overrides old \<and> 
12854  1205 
pid (declclass old) = pid (declclass inter) \<and> 
1206 
Protected \<le> accmodi inter" 

1207 
proof  

1208 
from dyn_override accmodi_old outside_pack 

1209 
show ?thesis (is "?P new old") 

1210 
proof (induct rule: overridesR.induct) 

1211 
case (Direct new old) 

1212 
assume accmodi_old: "accmodi old = Package" 

1213 
assume outside_pack: "pid (declclass old) \<noteq> pid (declclass new)" 

1214 
assume "G \<turnstile>Method old inheritable_in pid (declclass new)" 

1215 
with accmodi_old 

1216 
have "pid (declclass old) = pid (declclass new)" 

1217 
by (simp add: inheritable_in_def) 

1218 
with outside_pack 

1219 
show "?P new old" 

1220 
by (contradiction) 

1221 
next 

1222 
case (Indirect inter new old) 

1223 
assume accmodi_old: "accmodi old = Package" 

1224 
assume outside_pack: "pid (declclass old) \<noteq> pid (declclass new)" 

1225 
assume override_new_inter: "G \<turnstile> new overrides inter" 

1226 
assume override_inter_old: "G \<turnstile> inter overrides old" 

1227 
assume hyp_new_inter: "\<lbrakk>accmodi inter = Package; 

1228 
pid (declclass inter) \<noteq> pid (declclass new)\<rbrakk> 

1229 
\<Longrightarrow> ?P new inter" 

1230 
assume hyp_inter_old: "\<lbrakk>accmodi old = Package; 

1231 
pid (declclass old) \<noteq> pid (declclass inter)\<rbrakk> 

1232 
\<Longrightarrow> ?P inter old" 

1233 
show "?P new old" 

1234 
proof (cases "pid (declclass old) = pid (declclass inter)") 

1235 
case True 

1236 
note same_pack_old_inter = this 

1237 
show ?thesis 

1238 
proof (cases "pid (declclass inter) = pid (declclass new)") 

1239 
case True 

1240 
with same_pack_old_inter outside_pack 

1241 
show ?thesis 

1242 
by auto 

1243 
next 

1244 
case False 

1245 
note diff_pack_inter_new = this 

1246 
show ?thesis 

1247 
proof (cases "accmodi inter = Package") 

1248 
case True 

1249 
with diff_pack_inter_new hyp_new_inter 

1250 
obtain newinter where 

1251 
over_new_newinter: "G \<turnstile> new overrides newinter" and 

1252 
over_newinter_inter: "G \<turnstile> newinter overrides inter" and 

1253 
eq_pid: "pid (declclass inter) = pid (declclass newinter)" and 

1254 
accmodi_newinter: "Protected \<le> accmodi newinter" 

1255 
by auto 

1256 
from over_newinter_inter override_inter_old 

1257 
have "G\<turnstile>newinter overrides old" 

1258 
by (rule overridesR.Indirect) 

1259 
moreover 

1260 
from eq_pid same_pack_old_inter 

1261 
have "pid (declclass old) = pid (declclass newinter)" 

1262 
by simp 

1263 
moreover 

1264 
note over_new_newinter accmodi_newinter 

1265 
ultimately show ?thesis 

1266 
by blast 

1267 
next 

1268 
case False 

1269 
with override_new_inter 

1270 
have "Protected \<le> accmodi inter" 

1271 
by (cases "accmodi inter") (auto dest: no_Private_override) 

1272 
with override_new_inter override_inter_old same_pack_old_inter 

1273 
show ?thesis 

1274 
by blast 

1275 
qed 

1276 
qed 

1277 
next 

1278 
case False 

1279 
with accmodi_old hyp_inter_old 

1280 
obtain newinter where 

1281 
over_inter_newinter: "G \<turnstile> inter overrides newinter" and 

1282 
over_newinter_old: "G \<turnstile> newinter overrides old" and 

1283 
eq_pid: "pid (declclass old) = pid (declclass newinter)" and 

1284 
accmodi_newinter: "Protected \<le> accmodi newinter" 

1285 
by auto 

1286 
from override_new_inter over_inter_newinter 

1287 
have "G \<turnstile> new overrides newinter" 

1288 
by (rule overridesR.Indirect) 

1289 
with eq_pid over_newinter_old accmodi_newinter 

1290 
show ?thesis 

1291 
by blast 

1292 
qed 

1293 
qed 

1294 
qed 

1295 

1296 
lemma declclass_widen[rule_format]: 

1297 
"wf_prog G 

1298 
\<longrightarrow> (\<forall>c m. class G C = Some c \<longrightarrow> methd G C sig = Some m 

1299 
\<longrightarrow> G\<turnstile>C \<preceq>\<^sub>C declclass m)" (is "?P G C") 

1300 
proof (rule class_rec.induct,intro allI impI) 

1301 
fix G C c m 

1302 
assume Hyp: "\<forall>c. C \<noteq> Object \<and> ws_prog G \<and> class G C = Some c 

1303 
\<longrightarrow> ?P G (super c)" 

1304 
assume wf: "wf_prog G" and cls_C: "class G C = Some c" and 

1305 
m: "methd G C sig = Some m" 

1306 
show "G\<turnstile>C\<preceq>\<^sub>C declclass m" 

1307 
proof (cases "C=Object") 

1308 
case True 

1309 
with wf m show ?thesis by (simp add: methd_Object_SomeD) 

1310 
next 

1311 
let ?filter="filter_tab (\<lambda>sig m. G\<turnstile>C inherits method sig m)" 

1312 
let ?table = "table_of (map (\<lambda>(s, m). (s, C, m)) (methods c))" 

1313 
case False 

1314 
with cls_C wf m 

1315 
have methd_C: "(?filter (methd G (super c)) ++ ?table) sig = Some m " 

1316 
by (simp add: methd_rec) 

1317 
show ?thesis 

1318 
proof (cases "?table sig") 

1319 
case None 

1320 
from this methd_C have "?filter (methd G (super c)) sig = Some m" 

1321 
by simp 

1322 
moreover 

1323 
from wf cls_C False obtain sup where "class G (super c) = Some sup" 

1324 
by (blast dest: wf_prog_cdecl wf_cdecl_supD is_acc_class_is_class) 

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

1325 
moreover note wf False cls_C 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset

1326 
ultimately have "G\<turnstile>super c \<preceq>\<^sub>C declclass m" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset

1327 
by (auto intro: Hyp [rule_format]) 
12854  1328 
moreover from cls_C False have "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 super c" by (rule subcls1I) 
1329 
ultimately show ?thesis by  (rule rtrancl_into_rtrancl2) 

1330 
next 

1331 
case Some 

1332 
from this wf False cls_C methd_C show ?thesis by auto 

1333 
qed 

1334 
qed 

1335 
qed 

1336 

1337 
lemma declclass_methd_Object: 

1338 
"\<lbrakk>wf_prog G; methd G Object sig = Some m\<rbrakk> \<Longrightarrow> declclass m = Object" 

1339 
by auto 

1340 

1341 
lemma methd_declaredD: 

1342 
"\<lbrakk>wf_prog G; is_class G C;methd G C sig = Some m\<rbrakk> 

1343 
\<Longrightarrow> G\<turnstile>(mdecl (sig,mthd m)) declared_in (declclass m)" 

1344 
proof  

1345 
assume wf: "wf_prog G" 

1346 
then have ws: "ws_prog G" .. 

1347 
assume clsC: "is_class G C" 

1348 
from clsC ws 

1349 
show "methd G C sig = Some m 

1350 
\<Longrightarrow> G\<turnstile>(mdecl (sig,mthd m)) declared_in (declclass m)" 

1351 
(is "PROP ?P C") 

1352 
proof (induct ?P C rule: ws_class_induct') 

1353 
case Object 

1354 
assume "methd G Object sig = Some m" 

1355 
with wf show ?thesis 

1356 
by  (rule method_declared_inI, auto) 

1357 
next 

1358 
case Subcls 

1359 
fix C c 

1360 
assume clsC: "class G C = Some c" 

1361 
and m: "methd G C sig = Some m" 

1362 
and hyp: "methd G (super c) sig = Some m \<Longrightarrow> ?thesis" 

1363 
let ?newMethods = "table_of (map (\<lambda>(s, m). (s, C, m)) (methods c))" 

1364 
show ?thesis 

1365 
proof (cases "?newMethods sig") 

1366 
case None 

1367 
from None ws clsC m hyp 

1368 
show ?thesis by (auto intro: method_declared_inI simp add: methd_rec) 

1369 
next 

1370 
case Some 

1371 
from Some ws clsC m 

1372 
show ?thesis by (auto intro: method_declared_inI simp add: methd_rec) 

1373 
qed 

1374 
qed 

1375 
qed 

1376 

1377 
lemma methd_rec_Some_cases [consumes 4, case_names NewMethod InheritedMethod]: 

12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

1378 
assumes methd_C: "methd G C sig = Some m" and 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

1379 
ws: "ws_prog G" and 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

1380 
clsC: "class G C = Some c" and 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

1381 
neq_C_Obj: "C\<noteq>Object" 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

1382 
shows 
12854  1383 
"\<lbrakk>table_of (map (\<lambda>(s, m). (s, C, m)) (methods c)) sig = Some m \<Longrightarrow> P; 
1384 
\<lbrakk>G\<turnstile>C inherits (method sig m); methd G (super c) sig = Some m\<rbrakk> \<Longrightarrow> P 

1385 
\<rbrakk> \<Longrightarrow> P" 

1386 
proof  

1387 
let ?inherited = "filter_tab (\<lambda>sig m. G\<turnstile>C inherits method sig m) 

1388 
(methd G (super c))" 

1389 
let ?new = "table_of (map (\<lambda>(s, m). (s, C, m)) (methods c))" 

1390 
from ws clsC neq_C_Obj methd_C 

1391 
have methd_unfold: "(?inherited ++ ?new) sig = Some m" 

1392 
by (simp add: methd_rec) 

1393 
assume NewMethod: "?new sig = Some m \<Longrightarrow> P" 

1394 
assume InheritedMethod: "\<lbrakk>G\<turnstile>C inherits (method sig m); 

1395 
methd G (super c) sig = Some m\<rbrakk> \<Longrightarrow> P" 

1396 
show P 

1397 
proof (cases "?new sig") 

1398 
case None 

1399 
with methd_unfold have "?inherited sig = Some m" 

1400 
by (auto) 

1401 
with InheritedMethod show P by blast 

1402 
next 

1403 
case Some 

1404 
with methd_unfold have "?new sig = Some m" 

1405 
by auto 

1406 
with NewMethod show P by blast 

1407 
qed 

1408 
qed 

1409 

1410 

1411 
lemma methd_member_of: 

12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

1412 
assumes wf: "wf_prog G" 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

1413 
shows 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

1414 
"\<lbrakk>is_class G C; methd G C sig = Some m\<rbrakk> \<Longrightarrow> G\<turnstile>Methd sig m member_of C" 
12854  1415 
(is "?Class C \<Longrightarrow> ?Method C \<Longrightarrow> ?MemberOf C") 
1416 
proof  

1417 
from wf have ws: "ws_prog G" .. 

1418 
assume defC: "is_class G C" 

1419 
from defC ws 

1420 
show "?Class C \<Longrightarrow> ?Method C \<Longrightarrow> ?MemberOf C" 

1421 
proof (induct rule: ws_class_induct') 

1422 
case Object 

1423 
with wf have declC: "declclass m = Object" 

1424 
by (blast intro: declclass_methd_Object) 

1425 
with Object wf have "G\<turnstile>Methd sig m declared_in Object" 

1426 
by (auto dest: methd_declaredD simp del: methd_Object) 

1427 
with declC 

1428 
show "?MemberOf Object" 

1429 
by (auto intro!: members.Immediate 

1430 
simp del: methd_Object) 

1431 
next 

1432 
case (Subcls C c) 

1433 
assume clsC: "class G C = Some c" and 

1434 
neq_C_Obj: "C \<noteq> Object" 

1435 
assume methd: "?Method C" 

1436 
from methd ws clsC neq_C_Obj 

1437 
show "?MemberOf C" 

1438 
proof (cases rule: methd_rec_Some_cases) 

1439 
case NewMethod 

1440 
with clsC show ?thesis 

1441 
by (auto dest: method_declared_inI intro!: members.Immediate) 

1442 
next 

1443 
case InheritedMethod 

1444 
then show "?thesis" 

1445 
by (blast dest: inherits_member) 

1446 
qed 

1447 
qed 

1448 
qed 

1449 

1450 
lemma current_methd: 

1451 
"\<lbrakk>table_of (methods c) sig = Some new; 

1452 
ws_prog G; class G C = Some c; C \<noteq> Object; 

1453 
methd G (super c) sig = Some old\<rbrakk> 

1454 
\<Longrightarrow> methd G C sig = Some (C,new)" 

1455 
by (auto simp add: methd_rec 

1456 
intro: filter_tab_SomeI override_find_right table_of_map_SomeI) 

1457 

1458 
lemma wf_prog_staticD: 

12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

1459 
assumes wf: "wf_prog G" and 
12854  1460 
clsC: "class G C = Some c" and 
1461 
neq_C_Obj: "C \<noteq> Object" and 

1462 
old: "methd G (super c) sig = Some old" and 

1463 
accmodi_old: "Protected \<le> accmodi old" and 

1464 
new: "table_of (methods c) sig = Some new" 

12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

1465 
shows "is_static new = is_static old" 
12854  1466 
proof  
1467 
from clsC wf 

1468 
have wf_cdecl: "wf_cdecl G (C,c)" by (rule wf_prog_cdecl) 

1469 
from wf clsC neq_C_Obj 

1470 
have is_cls_super: "is_class G (super c)" 

1471 
by (blast dest: wf_prog_acc_superD is_acc_classD) 

1472 
from wf is_cls_super old 

1473 
have old_member_of: "G\<turnstile>Methd sig old member_of (super c)" 

1474 
by (rule methd_member_of) 

1475 
from old wf is_cls_super 

1476 
have old_declared: "G\<turnstile>Methd sig old declared_in (declclass old)" 

1477 
by (auto dest: methd_declared_in_declclass) 

1478 
from new clsC 

1479 
have new_declared: "G\<turnstile>Methd sig (C,new) declared_in C" 

1480 
by (auto intro: method_declared_inI) 

1481 
note trancl_rtrancl_tranc = trancl_rtrancl_trancl [trans] (* ### in Basis *) 

1482 
from clsC neq_C_Obj 

1483 
have subcls1_C_super: "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 super c" 

1484 
by (rule subcls1I) 

1485 
then have "G\<turnstile>C \<prec>\<^sub>C super c" .. 

1486 
also from old wf is_cls_super 

1487 
have "G\<turnstile>super c \<preceq>\<^sub>C (declclass old)" by (auto dest: methd_declC) 

1488 
finally have subcls_C_old: "G\<turnstile>C \<prec>\<^sub>C (declclass old)" . 

1489 
from accmodi_old 

1490 
have inheritable: "G\<turnstile>Methd sig old inheritable_in pid C" 

1491 
by (auto simp add: inheritable_in_def 

1492 
dest: acc_modi_le_Dests) 

1493 
show ?thesis 

1494 
proof (cases "is_static new") 

1495 