author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 46714  a7ca72710dfe 
child 55518  1ddb2edf5ceb 
permissions  rwrr 
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

1 
(* Title: HOL/Bali/DeclConcepts.thy 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

2 
Author: Norbert Schirmer 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

3 
*) 
12854  4 
header {* Advanced concepts on Java declarations like overriding, inheritance, 
5 
dynamic method lookup*} 

6 

16417  7 
theory DeclConcepts imports TypeRel begin 
12854  8 

9 
section "access control (cf. 6.6), overriding and hiding (cf. 8.4.6.1)" 

10 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35315
diff
changeset

11 
definition is_public :: "prog \<Rightarrow> qtname \<Rightarrow> bool" where 
37956  12 
"is_public G qn = (case class G qn of 
12854  13 
None \<Rightarrow> (case iface G qn of 
14 
None \<Rightarrow> False 

35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
34990
diff
changeset

15 
 Some i \<Rightarrow> access i = Public) 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
34990
diff
changeset

16 
 Some c \<Rightarrow> access c = Public)" 
12854  17 

18 
subsection "accessibility of types (cf. 6.6.1)" 

19 
text {* 

20 
Primitive types are always accessible, interfaces and classes are accessible 

21 
in their package or if they are defined public, an array type is accessible if 

22 
its element type is accessible *} 

23 

24 
primrec 

37956  25 
accessible_in :: "prog \<Rightarrow> ty \<Rightarrow> pname \<Rightarrow> bool" ("_ \<turnstile> _ accessible'_in _" [61,61,61] 60) and 
26 
rt_accessible_in :: "prog \<Rightarrow> ref_ty \<Rightarrow> pname \<Rightarrow> bool" ("_ \<turnstile> _ accessible'_in' _" [61,61,61] 60) 

27 
where 

28 
"G\<turnstile>(PrimT p) accessible_in pack = True" 

29 
 accessible_in_RefT_simp: 

30 
"G\<turnstile>(RefT r) accessible_in pack = G\<turnstile>r accessible_in' pack" 

31 
 "G\<turnstile>(NullT) accessible_in' pack = True" 

32 
 "G\<turnstile>(IfaceT I) accessible_in' pack = ((pid I = pack) \<or> is_public G I)" 

33 
 "G\<turnstile>(ClassT C) accessible_in' pack = ((pid C = pack) \<or> is_public G C)" 

34 
 "G\<turnstile>(ArrayT ty) accessible_in' pack = G\<turnstile>ty accessible_in pack" 

12854  35 

36 
declare accessible_in_RefT_simp [simp del] 

37 

37956  38 
definition 
39 
is_acc_class :: "prog \<Rightarrow> pname \<Rightarrow> qtname \<Rightarrow> bool" 

40 
where "is_acc_class G P C = (is_class G C \<and> G\<turnstile>(Class C) accessible_in P)" 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35315
diff
changeset

41 

37956  42 
definition 
43 
is_acc_iface :: "prog \<Rightarrow> pname \<Rightarrow> qtname \<Rightarrow> bool" 

44 
where "is_acc_iface G P I = (is_iface G I \<and> G\<turnstile>(Iface I) accessible_in P)" 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35315
diff
changeset

45 

37956  46 
definition 
47 
is_acc_type :: "prog \<Rightarrow> pname \<Rightarrow> ty \<Rightarrow> bool" 

48 
where "is_acc_type G P T = (is_type G T \<and> G\<turnstile>T accessible_in P)" 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35315
diff
changeset

49 

37956  50 
definition 
51 
is_acc_reftype :: "prog \<Rightarrow> pname \<Rightarrow> ref_ty \<Rightarrow> bool" 

52 
where "is_acc_reftype G P T = (isrtype G T \<and> G\<turnstile>T accessible_in' P)" 

12854  53 

54 
lemma is_acc_classD: 

55 
"is_acc_class G P C \<Longrightarrow> is_class G C \<and> G\<turnstile>(Class C) accessible_in P" 

56 
by (simp add: is_acc_class_def) 

57 

58 
lemma is_acc_class_is_class: "is_acc_class G P C \<Longrightarrow> is_class G C" 

59 
by (auto simp add: is_acc_class_def) 

60 

61 
lemma is_acc_ifaceD: 

62 
"is_acc_iface G P I \<Longrightarrow> is_iface G I \<and> G\<turnstile>(Iface I) accessible_in P" 

63 
by (simp add: is_acc_iface_def) 

64 

65 
lemma is_acc_typeD: 

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

66 
"is_acc_type G P T \<Longrightarrow> is_type G T \<and> G\<turnstile>T accessible_in P" 
12854  67 
by (simp add: is_acc_type_def) 
68 

69 
lemma is_acc_reftypeD: 

70 
"is_acc_reftype G P T \<Longrightarrow> isrtype G T \<and> G\<turnstile>T accessible_in' P" 

71 
by (simp add: is_acc_reftype_def) 

72 

73 
subsection "accessibility of members" 

74 
text {* 

75 
The accessibility of members is more involved as the accessibility of types. 

76 
We have to distinguish several cases to model the different effects of 

77 
accessibility during inheritance, overriding and ordinary member access 

78 
*} 

79 

80 
subsubsection {* Various technical conversion and selection functions *} 

81 

82 
text {* overloaded selector @{text accmodi} to select the access modifier 

83 
out of various HOL types *} 

84 

35315  85 
class has_accmodi = 
86 
fixes accmodi:: "'a \<Rightarrow> acc_modi" 

87 

88 
instantiation acc_modi :: has_accmodi 

89 
begin 

12854  90 

35315  91 
definition 
37956  92 
acc_modi_accmodi_def: "accmodi (a::acc_modi) = a" 
12854  93 

35315  94 
instance .. 
95 

96 
end 

12854  97 

98 
lemma acc_modi_accmodi_simp[simp]: "accmodi (a::acc_modi) = a" 

99 
by (simp add: acc_modi_accmodi_def) 

100 

38540
8c08631cb4b6
adjusted to changed naming convention of logical record types
haftmann
parents:
37956
diff
changeset

101 
instantiation decl_ext :: (type) has_accmodi 
35315  102 
begin 
12854  103 

35315  104 
definition 
37956  105 
decl_acc_modi_def: "accmodi (d::('a:: type) decl_scheme) = access d" 
12854  106 

35315  107 
instance .. 
108 

109 
end 

12854  110 

111 
lemma decl_acc_modi_simp[simp]: "accmodi (d::('a::type) decl_scheme) = access d" 

112 
by (simp add: decl_acc_modi_def) 

113 

37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
37406
diff
changeset

114 
instantiation prod :: (type, has_accmodi) has_accmodi 
35315  115 
begin 
12854  116 

35315  117 
definition 
37956  118 
pair_acc_modi_def: "accmodi p = accmodi (snd p)" 
35315  119 

120 
instance .. 

121 

122 
end 

12854  123 

124 
lemma pair_acc_modi_simp[simp]: "accmodi (x,a) = (accmodi a)" 

125 
by (simp add: pair_acc_modi_def) 

126 

35315  127 
instantiation memberdecl :: has_accmodi 
128 
begin 

12854  129 

35315  130 
definition 
37956  131 
memberdecl_acc_modi_def: "accmodi m = (case m of 
12854  132 
fdecl f \<Rightarrow> accmodi f 
133 
 mdecl m \<Rightarrow> accmodi m)" 

134 

35315  135 
instance .. 
136 

137 
end 

138 

12854  139 
lemma memberdecl_fdecl_acc_modi_simp[simp]: 
140 
"accmodi (fdecl m) = accmodi m" 

141 
by (simp add: memberdecl_acc_modi_def) 

142 

143 
lemma memberdecl_mdecl_acc_modi_simp[simp]: 

144 
"accmodi (mdecl m) = accmodi m" 

145 
by (simp add: memberdecl_acc_modi_def) 

146 

147 
text {* overloaded selector @{text declclass} to select the declaring class 

148 
out of various HOL types *} 

149 

35315  150 
class has_declclass = 
151 
fixes declclass:: "'a \<Rightarrow> qtname" 

152 

38540
8c08631cb4b6
adjusted to changed naming convention of logical record types
haftmann
parents:
37956
diff
changeset

153 
instantiation qtname_ext :: (type) has_declclass 
35315  154 
begin 
12854  155 

35315  156 
definition 
37956  157 
"declclass q = \<lparr> pid = pid q, tid = tid q \<rparr>" 
35315  158 

159 
instance .. 

12854  160 

35315  161 
end 
162 

163 
lemma qtname_declclass_def: 

164 
"declclass q \<equiv> (q::qtname)" 

38540
8c08631cb4b6
adjusted to changed naming convention of logical record types
haftmann
parents:
37956
diff
changeset

165 
by (induct q) (simp add: declclass_qtname_ext_def) 
12854  166 

167 
lemma qtname_declclass_simp[simp]: "declclass (q::qtname) = q" 

168 
by (simp add: qtname_declclass_def) 

169 

37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
37406
diff
changeset

170 
instantiation prod :: (has_declclass, type) has_declclass 
35315  171 
begin 
12854  172 

35315  173 
definition 
37956  174 
pair_declclass_def: "declclass p = declclass (fst p)" 
35315  175 

176 
instance .. 

177 

178 
end 

12854  179 

180 
lemma pair_declclass_simp[simp]: "declclass (c,x) = declclass c" 

181 
by (simp add: pair_declclass_def) 

182 

183 
text {* overloaded selector @{text is_static} to select the static modifier 

184 
out of various HOL types *} 

185 

35315  186 
class has_static = 
187 
fixes is_static :: "'a \<Rightarrow> bool" 

12854  188 

38540
8c08631cb4b6
adjusted to changed naming convention of logical record types
haftmann
parents:
37956
diff
changeset

189 
instantiation decl_ext :: (has_static) has_static 
35315  190 
begin 
12854  191 

35315  192 
instance .. 
193 

194 
end 

12854  195 

38540
8c08631cb4b6
adjusted to changed naming convention of logical record types
haftmann
parents:
37956
diff
changeset

196 
instantiation member_ext :: (type) has_static 
35315  197 
begin 
198 

199 
instance .. 

12854  200 

35315  201 
end 
202 

203 
axiomatization where 

204 
static_field_type_is_static_def: "is_static (m::('a member_scheme)) \<equiv> static m" 

12854  205 

206 
lemma member_is_static_simp: "is_static (m::'a member_scheme) = static m" 

32754
4e0256f7d219
Avoid recordinner constants in polymorphic definitions in Bali
Thomas Sewell <tsewell@nicta.com.au>
parents:
32134
diff
changeset

207 
by (simp add: static_field_type_is_static_def) 
12854  208 

37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
37406
diff
changeset

209 
instantiation prod :: (type, has_static) has_static 
35315  210 
begin 
12854  211 

35315  212 
definition 
37956  213 
pair_is_static_def: "is_static p = is_static (snd p)" 
35315  214 

215 
instance .. 

216 

217 
end 

12854  218 

219 
lemma pair_is_static_simp [simp]: "is_static (x,s) = is_static s" 

220 
by (simp add: pair_is_static_def) 

221 

222 
lemma pair_is_static_simp1: "is_static p = is_static (snd p)" 

223 
by (simp add: pair_is_static_def) 

224 

35315  225 
instantiation memberdecl :: has_static 
226 
begin 

12854  227 

35315  228 
definition 
12854  229 
memberdecl_is_static_def: 
37956  230 
"is_static m = (case m of 
12854  231 
fdecl f \<Rightarrow> is_static f 
232 
 mdecl m \<Rightarrow> is_static m)" 

233 

35315  234 
instance .. 
235 

236 
end 

237 

12854  238 
lemma memberdecl_is_static_fdecl_simp[simp]: 
239 
"is_static (fdecl f) = is_static f" 

240 
by (simp add: memberdecl_is_static_def) 

241 

242 
lemma memberdecl_is_static_mdecl_simp[simp]: 

243 
"is_static (mdecl m) = is_static m" 

244 
by (simp add: memberdecl_is_static_def) 

245 

246 
lemma mhead_static_simp [simp]: "is_static (mhead m) = is_static m" 

247 
by (cases m) (simp add: mhead_def member_is_static_simp) 

248 

37406  249 
 {* some mnemotic selectors for various pairs *} 
250 

37956  251 
definition 
252 
decliface :: "qtname \<times> 'a decl_scheme \<Rightarrow> qtname" where 

37406  253 
"decliface = fst" {* get the interface component *} 
12854  254 

37956  255 
definition 
256 
mbr :: "qtname \<times> memberdecl \<Rightarrow> memberdecl" where 

37406  257 
"mbr = snd" {* get the memberdecl component *} 
12854  258 

37956  259 
definition 
260 
mthd :: "'b \<times> 'a \<Rightarrow> 'a" where 

37406  261 
"mthd = snd" {* get the method component *} 
262 
{* also used for mdecl, mhead *} 

12854  263 

37956  264 
definition 
265 
fld :: "'b \<times> 'a decl_scheme \<Rightarrow> 'a decl_scheme" where 

37406  266 
"fld = snd" {* get the field component *} 
267 
{* also used for @{text "((vname \<times> qtname)\<times> field)"} *} 

12854  268 

37406  269 
 {* some mnemotic selectors for @{text "(vname \<times> qtname)"} *} 
12854  270 

37956  271 
definition 
272 
fname:: "vname \<times> 'a \<Rightarrow> vname" 

273 
where "fname = fst" 

37406  274 
{* also used for fdecl *} 
12854  275 

37956  276 
definition 
277 
declclassf:: "(vname \<times> qtname) \<Rightarrow> qtname" 

278 
where "declclassf = snd" 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

279 

12854  280 

281 
lemma decliface_simp[simp]: "decliface (I,m) = I" 

282 
by (simp add: decliface_def) 

283 

284 
lemma mbr_simp[simp]: "mbr (C,m) = m" 

285 
by (simp add: mbr_def) 

286 

287 
lemma access_mbr_simp [simp]: "(accmodi (mbr m)) = accmodi m" 

288 
by (cases m) (simp add: mbr_def) 

289 

290 
lemma mthd_simp[simp]: "mthd (C,m) = m" 

291 
by (simp add: mthd_def) 

292 

293 
lemma fld_simp[simp]: "fld (C,f) = f" 

294 
by (simp add: fld_def) 

295 

296 
lemma accmodi_simp[simp]: "accmodi (C,m) = access m" 

297 
by (simp ) 

298 

299 
lemma access_mthd_simp [simp]: "(access (mthd m)) = accmodi m" 

300 
by (cases m) (simp add: mthd_def) 

301 

302 
lemma access_fld_simp [simp]: "(access (fld f)) = accmodi f" 

303 
by (cases f) (simp add: fld_def) 

304 

305 
lemma static_mthd_simp[simp]: "static (mthd m) = is_static m" 

306 
by (cases m) (simp add: mthd_def member_is_static_simp) 

307 

308 
lemma mthd_is_static_simp [simp]: "is_static (mthd m) = is_static m" 

309 
by (cases m) simp 

310 

311 
lemma static_fld_simp[simp]: "static (fld f) = is_static f" 

312 
by (cases f) (simp add: fld_def member_is_static_simp) 

313 

314 
lemma ext_field_simp [simp]: "(declclass f,fld f) = f" 

315 
by (cases f) (simp add: fld_def) 

316 

317 
lemma ext_method_simp [simp]: "(declclass m,mthd m) = m" 

318 
by (cases m) (simp add: mthd_def) 

319 

320 
lemma ext_mbr_simp [simp]: "(declclass m,mbr m) = m" 

321 
by (cases m) (simp add: mbr_def) 

322 

323 
lemma fname_simp[simp]:"fname (n,c) = n" 

324 
by (simp add: fname_def) 

325 

326 
lemma declclassf_simp[simp]:"declclassf (n,c) = c" 

327 
by (simp add: declclassf_def) 

328 

37406  329 
{* some mnemotic selectors for @{text "(vname \<times> qtname)"} *} 
12854  330 

37956  331 
definition 
332 
fldname :: "vname \<times> qtname \<Rightarrow> vname" 

333 
where "fldname = fst" 

37406  334 

37956  335 
definition 
336 
fldclass :: "vname \<times> qtname \<Rightarrow> qtname" 

337 
where "fldclass = snd" 

12854  338 

339 
lemma fldname_simp[simp]: "fldname (n,c) = n" 

340 
by (simp add: fldname_def) 

341 

342 
lemma fldclass_simp[simp]: "fldclass (n,c) = c" 

343 
by (simp add: fldclass_def) 

344 

345 
lemma ext_fieldname_simp[simp]: "(fldname f,fldclass f) = f" 

346 
by (simp add: fldname_def fldclass_def) 

347 

348 
text {* Convert a qualified method declaration (qualified with its declaring 

349 
class) to a qualified member declaration: @{text methdMembr} *} 

350 

37956  351 
definition 
352 
methdMembr :: "qtname \<times> mdecl \<Rightarrow> qtname \<times> memberdecl" 

353 
where "methdMembr m = (fst m, mdecl (snd m))" 

12854  354 

355 
lemma methdMembr_simp[simp]: "methdMembr (c,m) = (c,mdecl m)" 

356 
by (simp add: methdMembr_def) 

357 

358 
lemma accmodi_methdMembr_simp[simp]: "accmodi (methdMembr m) = accmodi m" 

359 
by (cases m) (simp add: methdMembr_def) 

360 

361 
lemma is_static_methdMembr_simp[simp]: "is_static (methdMembr m) = is_static m" 

362 
by (cases m) (simp add: methdMembr_def) 

363 

364 
lemma declclass_methdMembr_simp[simp]: "declclass (methdMembr m) = declclass m" 

365 
by (cases m) (simp add: methdMembr_def) 

366 

367 
text {* Convert a qualified method (qualified with its declaring 

368 
class) to a qualified member declaration: @{text method} *} 

369 

37956  370 
definition 
371 
method :: "sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> memberdecl)" 

372 
where "method sig m = (declclass m, mdecl (sig, mthd m))" 

12854  373 

374 
lemma method_simp[simp]: "method sig (C,m) = (C,mdecl (sig,m))" 

375 
by (simp add: method_def) 

376 

377 
lemma accmodi_method_simp[simp]: "accmodi (method sig m) = accmodi m" 

378 
by (simp add: method_def) 

379 

380 
lemma declclass_method_simp[simp]: "declclass (method sig m) = declclass m" 

381 
by (simp add: method_def) 

382 

383 
lemma is_static_method_simp[simp]: "is_static (method sig m) = is_static m" 

384 
by (cases m) (simp add: method_def) 

385 

386 
lemma mbr_method_simp[simp]: "mbr (method sig m) = mdecl (sig,mthd m)" 

387 
by (simp add: mbr_def method_def) 

388 

389 
lemma memberid_method_simp[simp]: "memberid (method sig m) = mid sig" 

390 
by (simp add: method_def) 

391 

37956  392 
definition 
393 
fieldm :: "vname \<Rightarrow> (qtname \<times> field) \<Rightarrow> (qtname \<times> memberdecl)" 

394 
where "fieldm n f = (declclass f, fdecl (n, fld f))" 

12854  395 

396 
lemma fieldm_simp[simp]: "fieldm n (C,f) = (C,fdecl (n,f))" 

397 
by (simp add: fieldm_def) 

398 

399 
lemma accmodi_fieldm_simp[simp]: "accmodi (fieldm n f) = accmodi f" 

400 
by (simp add: fieldm_def) 

401 

402 
lemma declclass_fieldm_simp[simp]: "declclass (fieldm n f) = declclass f" 

403 
by (simp add: fieldm_def) 

404 

405 
lemma is_static_fieldm_simp[simp]: "is_static (fieldm n f) = is_static f" 

406 
by (cases f) (simp add: fieldm_def) 

407 

408 
lemma mbr_fieldm_simp[simp]: "mbr (fieldm n f) = fdecl (n,fld f)" 

409 
by (simp add: mbr_def fieldm_def) 

410 

411 
lemma memberid_fieldm_simp[simp]: "memberid (fieldm n f) = fid n" 

412 
by (simp add: fieldm_def) 

413 

414 
text {* Select the signature out of a qualified method declaration: 

415 
@{text msig} *} 

416 

37956  417 
definition 
418 
msig :: "(qtname \<times> mdecl) \<Rightarrow> sig" 

419 
where "msig m = fst (snd m)" 

12854  420 

421 
lemma msig_simp[simp]: "msig (c,(s,m)) = s" 

422 
by (simp add: msig_def) 

423 

424 
text {* Convert a qualified method (qualified with its declaring 

425 
class) to a qualified method declaration: @{text qmdecl} *} 

426 

37956  427 
definition 
428 
qmdecl :: "sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> mdecl)" 

429 
where "qmdecl sig m = (declclass m, (sig,mthd m))" 

12854  430 

431 
lemma qmdecl_simp[simp]: "qmdecl sig (C,m) = (C,(sig,m))" 

432 
by (simp add: qmdecl_def) 

433 

434 
lemma declclass_qmdecl_simp[simp]: "declclass (qmdecl sig m) = declclass m" 

435 
by (simp add: qmdecl_def) 

436 

437 
lemma accmodi_qmdecl_simp[simp]: "accmodi (qmdecl sig m) = accmodi m" 

438 
by (simp add: qmdecl_def) 

439 

440 
lemma is_static_qmdecl_simp[simp]: "is_static (qmdecl sig m) = is_static m" 

441 
by (cases m) (simp add: qmdecl_def) 

442 

443 
lemma msig_qmdecl_simp[simp]: "msig (qmdecl sig m) = sig" 

444 
by (simp add: qmdecl_def) 

445 

446 
lemma mdecl_qmdecl_simp[simp]: 

447 
"mdecl (mthd (qmdecl sig new)) = mdecl (sig, mthd new)" 

448 
by (simp add: qmdecl_def) 

449 

450 
lemma methdMembr_qmdecl_simp [simp]: 

451 
"methdMembr (qmdecl sig old) = method sig old" 

452 
by (simp add: methdMembr_def qmdecl_def method_def) 

453 

454 
text {* overloaded selector @{text resTy} to select the result type 

455 
out of various HOL types *} 

456 

35315  457 
class has_resTy = 
458 
fixes resTy:: "'a \<Rightarrow> ty" 

459 

38540
8c08631cb4b6
adjusted to changed naming convention of logical record types
haftmann
parents:
37956
diff
changeset

460 
instantiation decl_ext :: (has_resTy) has_resTy 
35315  461 
begin 
12854  462 

35315  463 
instance .. 
464 

465 
end 

466 

38540
8c08631cb4b6
adjusted to changed naming convention of logical record types
haftmann
parents:
37956
diff
changeset

467 
instantiation member_ext :: (has_resTy) has_resTy 
35315  468 
begin 
12854  469 

35315  470 
instance .. 
12854  471 

35315  472 
end 
473 

38540
8c08631cb4b6
adjusted to changed naming convention of logical record types
haftmann
parents:
37956
diff
changeset

474 
instantiation mhead_ext :: (type) has_resTy 
35315  475 
begin 
12854  476 

35315  477 
instance .. 
478 

479 
end 

480 

481 
axiomatization where 

482 
mhead_ext_type_resTy_def: "resTy (m::('b mhead_scheme)) \<equiv> resT m" 

12854  483 

484 
lemma mhead_resTy_simp: "resTy (m::'a mhead_scheme) = resT m" 

32754
4e0256f7d219
Avoid recordinner constants in polymorphic definitions in Bali
Thomas Sewell <tsewell@nicta.com.au>
parents:
32134
diff
changeset

485 
by (simp add: mhead_ext_type_resTy_def) 
12854  486 

487 
lemma resTy_mhead [simp]:"resTy (mhead m) = resTy m" 

488 
by (simp add: mhead_def mhead_resTy_simp) 

489 

38540
8c08631cb4b6
adjusted to changed naming convention of logical record types
haftmann
parents:
37956
diff
changeset

490 
instantiation prod :: (type, has_resTy) has_resTy 
35315  491 
begin 
12854  492 

35315  493 
definition 
37956  494 
pair_resTy_def: "resTy p = resTy (snd p)" 
35315  495 

496 
instance .. 

497 

498 
end 

12854  499 

500 
lemma pair_resTy_simp[simp]: "resTy (x,m) = resTy m" 

501 
by (simp add: pair_resTy_def) 

502 

503 
lemma qmdecl_resTy_simp [simp]: "resTy (qmdecl sig m) = resTy m" 

504 
by (cases m) (simp) 

505 

506 
lemma resTy_mthd [simp]:"resTy (mthd m) = resTy m" 

507 
by (cases m) (simp add: mthd_def ) 

508 

509 
subsubsection "inheritablein" 

510 
text {* 

511 
@{text "G\<turnstile>m inheritable_in P"}: m can be inherited by 

512 
classes in package P if: 

513 
\begin{itemize} 

514 
\item the declaration class of m is accessible in P and 

515 
\item the member m is declared with protected or public access or if it is 

516 
declared with default (package) access, the package of the declaration 

517 
class of m is also P. If the member m is declared with private access 

518 
it is not accessible for inheritance at all. 

519 
\end{itemize} 

520 
*} 

37956  521 
definition 
522 
inheritable_in :: "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> pname \<Rightarrow> bool" ("_ \<turnstile> _ inheritable'_in _" [61,61,61] 60) 

523 
where 

524 
"G\<turnstile>membr inheritable_in pack = 

525 
(case (accmodi membr) of 

526 
Private \<Rightarrow> False 

527 
 Package \<Rightarrow> (pid (declclass membr)) = pack 

528 
 Protected \<Rightarrow> True 

529 
 Public \<Rightarrow> True)" 

12854  530 

35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
34990
diff
changeset

531 
abbreviation 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
34990
diff
changeset

532 
Method_inheritable_in_syntax:: 
12854  533 
"prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> pname \<Rightarrow> bool" 
534 
("_ \<turnstile>Method _ inheritable'_in _ " [61,61,61] 60) 

35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
34990
diff
changeset

535 
where "G\<turnstile>Method m inheritable_in p == G\<turnstile>methdMembr m inheritable_in p" 
12854  536 

35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
34990
diff
changeset

537 
abbreviation 
12854  538 
Methd_inheritable_in:: 
539 
"prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> pname \<Rightarrow> bool" 

540 
("_ \<turnstile>Methd _ _ inheritable'_in _ " [61,61,61,61] 60) 

35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
34990
diff
changeset

541 
where "G\<turnstile>Methd s m inheritable_in p == G\<turnstile>(method s m) inheritable_in p" 
12854  542 

543 
subsubsection "declaredin/undeclaredin" 

544 

37956  545 
definition 
546 
cdeclaredmethd :: "prog \<Rightarrow> qtname \<Rightarrow> (sig,methd) table" where 

547 
"cdeclaredmethd G C = 

548 
(case class G C of 

12854  549 
None \<Rightarrow> \<lambda> sig. None 
37956  550 
 Some c \<Rightarrow> table_of (methods c))" 
12854  551 

37956  552 
definition 
553 
cdeclaredfield :: "prog \<Rightarrow> qtname \<Rightarrow> (vname,field) table" where 

554 
"cdeclaredfield G C = 

555 
(case class G C of 

556 
None \<Rightarrow> \<lambda> sig. None 

557 
 Some c \<Rightarrow> table_of (cfields c))" 

12854  558 

37956  559 
definition 
560 
declared_in :: "prog \<Rightarrow> memberdecl \<Rightarrow> qtname \<Rightarrow> bool" ("_\<turnstile> _ declared'_in _" [61,61,61] 60) 

561 
where 

562 
"G\<turnstile>m declared_in C = (case m of 

563 
fdecl (fn,f ) \<Rightarrow> cdeclaredfield G C fn = Some f 

564 
 mdecl (sig,m) \<Rightarrow> cdeclaredmethd G C sig = Some m)" 

12854  565 

35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
34990
diff
changeset

566 
abbreviation 
12854  567 
method_declared_in:: "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> qtname \<Rightarrow> bool" 
568 
("_\<turnstile>Method _ declared'_in _" [61,61,61] 60) 

35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
34990
diff
changeset

569 
where "G\<turnstile>Method m declared_in C == G\<turnstile>mdecl (mthd m) declared_in C" 
12854  570 

35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
34990
diff
changeset

571 
abbreviation 
12854  572 
methd_declared_in:: "prog \<Rightarrow> sig \<Rightarrow>(qtname \<times> methd) \<Rightarrow> qtname \<Rightarrow> bool" 
573 
("_\<turnstile>Methd _ _ declared'_in _" [61,61,61,61] 60) 

35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
34990
diff
changeset

574 
where "G\<turnstile>Methd s m declared_in C == G\<turnstile>mdecl (s,mthd m) declared_in C" 
12854  575 

576 
lemma declared_in_classD: 

577 
"G\<turnstile>m declared_in C \<Longrightarrow> is_class G C" 

578 
by (cases m) 

579 
(auto simp add: declared_in_def cdeclaredmethd_def cdeclaredfield_def) 

580 

37956  581 
definition 
582 
undeclared_in :: "prog \<Rightarrow> memberid \<Rightarrow> qtname \<Rightarrow> bool" ("_\<turnstile> _ undeclared'_in _" [61,61,61] 60) 

583 
where 

584 
"G\<turnstile>m undeclared_in C = (case m of 

585 
fid fn \<Rightarrow> cdeclaredfield G C fn = None 

586 
 mid sig \<Rightarrow> cdeclaredmethd G C sig = None)" 

12854  587 

588 

589 
subsubsection "members" 

590 

591 
(* Can't just take a function: prog \<Rightarrow> qtname \<Rightarrow> memberdecl set because 

592 
the class qtname changes to the superclass in the inductive definition 

593 
below 

594 
*) 

595 

23747  596 
inductive 
21765  597 
members :: "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> bool" 
598 
("_ \<turnstile> _ member'_of _" [61,61,61] 60) 

599 
for G :: prog 

600 
where 

12854  601 

21765  602 
Immediate: "\<lbrakk>G\<turnstile>mbr m declared_in C;declclass m = C\<rbrakk> \<Longrightarrow> G\<turnstile>m member_of C" 
603 
 Inherited: "\<lbrakk>G\<turnstile>m inheritable_in (pid C); G\<turnstile>memberid m undeclared_in C; 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35315
diff
changeset

604 
G\<turnstile>C \<prec>\<^sub>C1 S; G\<turnstile>(Class S) accessible_in (pid C);G\<turnstile>m member_of S 
21765  605 
\<rbrakk> \<Longrightarrow> G\<turnstile>m member_of C" 
12854  606 
text {* Note that in the case of an inherited member only the members of the 
607 
direct superclass are concerned. If a member of a superclass of the direct 

608 
superclass isn't inherited in the direct superclass (not member of the 

609 
direct superclass) than it can't be a member of the class. E.g. If a 

610 
member of a class A is defined with package access it isn't member of a 

611 
subclass S if S isn't in the same package as A. Any further subclasses 

612 
of S will not inherit the member, regardless if they are in the same 

613 
package as A or not.*} 

614 

35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
34990
diff
changeset

615 
abbreviation 
12854  616 
method_member_of:: "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> qtname \<Rightarrow> bool" 
617 
("_ \<turnstile>Method _ member'_of _" [61,61,61] 60) 

35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
34990
diff
changeset

618 
where "G\<turnstile>Method m member_of C == G\<turnstile>(methdMembr m) member_of C" 
12854  619 

35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
34990
diff
changeset

620 
abbreviation 
12854  621 
methd_member_of:: "prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> qtname \<Rightarrow> bool" 
622 
("_ \<turnstile>Methd _ _ member'_of _" [61,61,61,61] 60) 

35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
34990
diff
changeset

623 
where "G\<turnstile>Methd s m member_of C == G\<turnstile>(method s m) member_of C" 
12854  624 

35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
34990
diff
changeset

625 
abbreviation 
12854  626 
fieldm_member_of:: "prog \<Rightarrow> vname \<Rightarrow> (qtname \<times> field) \<Rightarrow> qtname \<Rightarrow> bool" 
627 
("_ \<turnstile>Field _ _ member'_of _" [61,61,61] 60) 

35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
34990
diff
changeset

628 
where "G\<turnstile>Field n f member_of C == G\<turnstile>fieldm n f member_of C" 
12854  629 

37956  630 
definition 
631 
inherits :: "prog \<Rightarrow> qtname \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> bool" ("_ \<turnstile> _ inherits _" [61,61,61] 60) 

632 
where 

633 
"G\<turnstile>C inherits m = 

634 
(G\<turnstile>m inheritable_in (pid C) \<and> G\<turnstile>memberid m undeclared_in C \<and> 

635 
(\<exists>S. G\<turnstile>C \<prec>\<^sub>C1 S \<and> G\<turnstile>(Class S) accessible_in (pid C) \<and> G\<turnstile>m member_of S))" 

12854  636 

637 
lemma inherits_member: "G\<turnstile>C inherits m \<Longrightarrow> G\<turnstile>m member_of C" 

638 
by (auto simp add: inherits_def intro: members.Inherited) 

639 

640 

37956  641 
definition 
642 
member_in :: "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> bool" ("_ \<turnstile> _ member'_in _" [61,61,61] 60) 

643 
where "G\<turnstile>m member_in C = (\<exists> provC. G\<turnstile> C \<preceq>\<^sub>C provC \<and> G \<turnstile> m member_of provC)" 

12854  644 
text {* A member is in a class if it is member of the class or a superclass. 
645 
If a member is in a class we can select this member. This additional notion 

646 
is necessary since not all members are inherited to subclasses. So such 

647 
members are not memberof the subclass but memberin the subclass.*} 

648 

35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
34990
diff
changeset

649 
abbreviation 
12854  650 
method_member_in:: "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> qtname \<Rightarrow> bool" 
651 
("_ \<turnstile>Method _ member'_in _" [61,61,61] 60) 

35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
34990
diff
changeset

652 
where "G\<turnstile>Method m member_in C == G\<turnstile>(methdMembr m) member_in C" 
12854  653 

35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
34990
diff
changeset

654 
abbreviation 
12854  655 
methd_member_in:: "prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> qtname \<Rightarrow> bool" 
656 
("_ \<turnstile>Methd _ _ member'_in _" [61,61,61,61] 60) 

35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
34990
diff
changeset

657 
where "G\<turnstile>Methd s m member_in C == G\<turnstile>(method s m) member_in C" 
12854  658 

659 
lemma member_inD: "G\<turnstile>m member_in C 

660 
\<Longrightarrow> \<exists> provC. G\<turnstile> C \<preceq>\<^sub>C provC \<and> G \<turnstile> m member_of provC" 

661 
by (auto simp add: member_in_def) 

662 

663 
lemma member_inI: "\<lbrakk>G \<turnstile> m member_of provC;G\<turnstile> C \<preceq>\<^sub>C provC\<rbrakk> \<Longrightarrow> G\<turnstile>m member_in C" 

664 
by (auto simp add: member_in_def) 

665 

666 
lemma member_of_to_member_in: "G \<turnstile> m member_of C \<Longrightarrow> G \<turnstile>m member_in C" 

667 
by (auto intro: member_inI) 

668 

669 

670 
subsubsection "overriding" 

671 

672 
text {* Unfortunately the static notion of overriding (used during the 

673 
typecheck of the compiler) and the dynamic notion of overriding (used during 

674 
execution in the JVM) are not exactly the same. 

675 
*} 

676 

677 
text {* Static overriding (used during the typecheck of the compiler) *} 

678 

23747  679 
inductive 
21765  680 
stat_overridesR :: "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> bool" 
681 
("_ \<turnstile> _ overrides\<^sub>S _" [61,61,61] 60) 

682 
for G :: prog 

683 
where 

12854  684 

21765  685 
Direct: "\<lbrakk>\<not> is_static new; msig new = msig old; 
686 
G\<turnstile>Method new declared_in (declclass new); 

687 
G\<turnstile>Method old declared_in (declclass old); 

688 
G\<turnstile>Method old inheritable_in pid (declclass new); 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35315
diff
changeset

689 
G\<turnstile>(declclass new) \<prec>\<^sub>C1 superNew; 
21765  690 
G \<turnstile>Method old member_of superNew 
691 
\<rbrakk> \<Longrightarrow> G\<turnstile>new overrides\<^sub>S old" 

12854  692 

32134
ee143615019c
set intersection and union now named inter and union
haftmann
parents:
30235
diff
changeset

693 
 Indirect: "\<lbrakk>G\<turnstile>new overrides\<^sub>S intr; G\<turnstile>intr overrides\<^sub>S old\<rbrakk> 
21765  694 
\<Longrightarrow> G\<turnstile>new overrides\<^sub>S old" 
12854  695 

696 
text {* Dynamic overriding (used during the typecheck of the compiler) *} 

697 

23747  698 
inductive 
21765  699 
overridesR :: "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> bool" 
700 
("_ \<turnstile> _ overrides _" [61,61,61] 60) 

701 
for G :: prog 

702 
where 

12854  703 

21765  704 
Direct: "\<lbrakk>\<not> is_static new; \<not> is_static old; accmodi new \<noteq> Private; 
705 
msig new = msig old; 

706 
G\<turnstile>(declclass new) \<prec>\<^sub>C (declclass old); 

707 
G\<turnstile>Method new declared_in (declclass new); 

708 
G\<turnstile>Method old declared_in (declclass old); 

709 
G\<turnstile>Method old inheritable_in pid (declclass new); 

710 
G\<turnstile>resTy new \<preceq> resTy old 

711 
\<rbrakk> \<Longrightarrow> G\<turnstile>new overrides old" 

12854  712 

32134
ee143615019c
set intersection and union now named inter and union
haftmann
parents:
30235
diff
changeset

713 
 Indirect: "\<lbrakk>G\<turnstile>new overrides intr; G\<turnstile>intr overrides old\<rbrakk> 
21765  714 
\<Longrightarrow> G\<turnstile>new overrides old" 
12854  715 

35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
34990
diff
changeset

716 
abbreviation (input) 
12854  717 
sig_stat_overrides:: 
718 
"prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> methd) \<Rightarrow> bool" 

719 
("_,_\<turnstile> _ overrides\<^sub>S _" [61,61,61,61] 60) 

35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
34990
diff
changeset

720 
where "G,s\<turnstile>new overrides\<^sub>S old == G\<turnstile>(qmdecl s new) overrides\<^sub>S (qmdecl s old)" 
12854  721 

35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
34990
diff
changeset

722 
abbreviation (input) 
12854  723 
sig_overrides:: "prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> methd) \<Rightarrow> bool" 
724 
("_,_\<turnstile> _ overrides _" [61,61,61,61] 60) 

35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
34990
diff
changeset

725 
where "G,s\<turnstile>new overrides old == G\<turnstile>(qmdecl s new) overrides (qmdecl s old)" 
12854  726 

727 
subsubsection "Hiding" 

728 

37956  729 
definition 
730 
hides :: "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> bool" ("_\<turnstile> _ hides _" [61,61,61] 60) 

731 
where 

732 
"G\<turnstile>new hides old = 

733 
(is_static new \<and> msig new = msig old \<and> 

734 
G\<turnstile>(declclass new) \<prec>\<^sub>C (declclass old) \<and> 

735 
G\<turnstile>Method new declared_in (declclass new) \<and> 

736 
G\<turnstile>Method old declared_in (declclass old) \<and> 

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

12854  738 

35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
34990
diff
changeset

739 
abbreviation 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
34990
diff
changeset

740 
sig_hides:: "prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> methd) \<Rightarrow> bool" 
12854  741 
("_,_\<turnstile> _ hides _" [61,61,61,61] 60) 
35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
34990
diff
changeset

742 
where "G,s\<turnstile>new hides old == G\<turnstile>(qmdecl s new) hides (qmdecl s old)" 
12854  743 

744 
lemma hidesI: 

745 
"\<lbrakk>is_static new; msig new = msig old; 

746 
G\<turnstile>(declclass new) \<prec>\<^sub>C (declclass old); 

747 
G\<turnstile>Method new declared_in (declclass new); 

748 
G\<turnstile>Method old declared_in (declclass old); 

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

750 
\<rbrakk> \<Longrightarrow> G\<turnstile>new hides old" 

751 
by (auto simp add: hides_def) 

752 

753 
lemma hidesD: 

754 
"\<lbrakk>G\<turnstile>new hides old\<rbrakk> \<Longrightarrow> 

755 
declclass new \<noteq> Object \<and> is_static new \<and> msig new = msig old \<and> 

756 
G\<turnstile>(declclass new) \<prec>\<^sub>C (declclass old) \<and> 

757 
G\<turnstile>Method new declared_in (declclass new) \<and> 

758 
G\<turnstile>Method old declared_in (declclass old)" 

759 
by (auto simp add: hides_def) 

760 

761 
lemma overrides_commonD: 

762 
"\<lbrakk>G\<turnstile>new overrides old\<rbrakk> \<Longrightarrow> 

763 
declclass new \<noteq> Object \<and> \<not> is_static new \<and> \<not> is_static old \<and> 

764 
accmodi new \<noteq> Private \<and> 

765 
msig new = msig old \<and> 

766 
G\<turnstile>(declclass new) \<prec>\<^sub>C (declclass old) \<and> 

767 
G\<turnstile>Method new declared_in (declclass new) \<and> 

768 
G\<turnstile>Method old declared_in (declclass old)" 

769 
by (induct set: overridesR) (auto intro: trancl_trans) 

770 

771 
lemma ws_overrides_commonD: 

772 
"\<lbrakk>G\<turnstile>new overrides old;ws_prog G\<rbrakk> \<Longrightarrow> 

773 
declclass new \<noteq> Object \<and> \<not> is_static new \<and> \<not> is_static old \<and> 

774 
accmodi new \<noteq> Private \<and> G\<turnstile>resTy new \<preceq> resTy old \<and> 

775 
msig new = msig old \<and> 

776 
G\<turnstile>(declclass new) \<prec>\<^sub>C (declclass old) \<and> 

777 
G\<turnstile>Method new declared_in (declclass new) \<and> 

778 
G\<turnstile>Method old declared_in (declclass old)" 

779 
by (induct set: overridesR) (auto intro: trancl_trans ws_widen_trans) 

780 

781 
lemma overrides_eq_sigD: 

782 
"\<lbrakk>G\<turnstile>new overrides old\<rbrakk> \<Longrightarrow> msig old=msig new" 

783 
by (auto dest: overrides_commonD) 

784 

785 
lemma hides_eq_sigD: 

786 
"\<lbrakk>G\<turnstile>new hides old\<rbrakk> \<Longrightarrow> msig old=msig new" 

787 
by (auto simp add: hides_def) 

788 

789 
subsubsection "permits access" 

37956  790 
definition 
791 
permits_acc :: "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool" ("_ \<turnstile> _ in _ permits'_acc'_from _" [61,61,61,61] 60) 

792 
where 

793 
"G\<turnstile>membr in cls permits_acc_from accclass = 

794 
(case (accmodi membr) of 

795 
Private \<Rightarrow> (declclass membr = accclass) 

796 
 Package \<Rightarrow> (pid (declclass membr) = pid accclass) 

797 
 Protected \<Rightarrow> (pid (declclass membr) = pid accclass) 

12854  798 
\<or> 
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

799 
(G\<turnstile>accclass \<prec>\<^sub>C declclass membr 
35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
34990
diff
changeset

800 
\<and> (G\<turnstile>cls \<preceq>\<^sub>C accclass \<or> is_static membr)) 
37956  801 
 Public \<Rightarrow> True)" 
12854  802 
text {* 
803 
The subcondition of the @{term "Protected"} case: 

804 
@{term "G\<turnstile>accclass \<prec>\<^sub>C declclass membr"} could also be relaxed to: 

805 
@{term "G\<turnstile>accclass \<preceq>\<^sub>C declclass membr"} since in case both classes are the 

806 
same the other condition @{term "(pid (declclass membr) = pid accclass)"} 

807 
holds anyway. 

808 
*} 

809 

810 
text {* Like in case of overriding, the static and dynamic accessibility 

811 
of members is not uniform. 

812 
\begin{itemize} 

813 
\item Statically the class/interface of the member must be accessible for the 

814 
member to be accessible. During runtime this is not necessary. For 

815 
Example, if a class is accessible and we are allowed to access a member 

816 
of this class (statically) we expect that we can access this member in 

817 
an arbitrary subclass (during runtime). It's not intended to restrict 

818 
the access to accessible subclasses during runtime. 

819 
\item Statically the member we want to access must be "member of" the class. 

820 
Dynamically it must only be "member in" the class. 

821 
\end{itemize} 

822 
*} 

823 

23747  824 
inductive 
21765  825 
accessible_fromR :: "prog \<Rightarrow> qtname \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> bool" 
826 
and accessible_from :: "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool" 

827 
("_ \<turnstile> _ of _ accessible'_from _" [61,61,61,61] 60) 

828 
and method_accessible_from :: "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool" 

829 
("_ \<turnstile>Method _ of _ accessible'_from _" [61,61,61,61] 60) 

830 
for G :: prog and accclass :: qtname 

831 
where 

832 
"G\<turnstile>membr of cls accessible_from accclass \<equiv> accessible_fromR G accclass membr cls" 

12854  833 

25143
2a1acc88a180
abbrevs within inductive definitions may no longer depend on each other (reflects in internal organization, particularly for output);
wenzelm
parents:
24038
diff
changeset

834 
 "G\<turnstile>Method m of cls accessible_from accclass \<equiv> accessible_fromR G accclass (methdMembr m) cls" 
12854  835 

35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
34990
diff
changeset

836 
 Immediate: "!!membr class. 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
34990
diff
changeset

837 
\<lbrakk>G\<turnstile>membr member_of class; 
21765  838 
G\<turnstile>(Class class) accessible_in (pid accclass); 
839 
G\<turnstile>membr in class permits_acc_from accclass 

840 
\<rbrakk> \<Longrightarrow> G\<turnstile>membr of class accessible_from accclass" 

12854  841 

35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
34990
diff
changeset

842 
 Overriding: "!!membr class C new old supr. 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
34990
diff
changeset

843 
\<lbrakk>G\<turnstile>membr member_of class; 
21765  844 
G\<turnstile>(Class class) accessible_in (pid accclass); 
845 
membr=(C,mdecl new); 

846 
G\<turnstile>(C,new) overrides\<^sub>S old; 

22426  847 
G\<turnstile>class \<prec>\<^sub>C supr; 
848 
G\<turnstile>Method old of supr accessible_from accclass 

21765  849 
\<rbrakk>\<Longrightarrow> G\<turnstile>membr of class accessible_from accclass" 
12854  850 

35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
34990
diff
changeset

851 
abbreviation 
12854  852 
methd_accessible_from:: 
853 
"prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool" 

854 
("_ \<turnstile>Methd _ _ of _ accessible'_from _" [61,61,61,61,61] 60) 

35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
34990
diff
changeset

855 
where 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
34990
diff
changeset

856 
"G\<turnstile>Methd s m of cls accessible_from accclass == 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
34990
diff
changeset

857 
G\<turnstile>(method s m) of cls accessible_from accclass" 
12854  858 

35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
34990
diff
changeset

859 
abbreviation 
12854  860 
field_accessible_from:: 
861 
"prog \<Rightarrow> vname \<Rightarrow> (qtname \<times> field) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool" 

862 
("_ \<turnstile>Field _ _ of _ accessible'_from _" [61,61,61,61,61] 60) 

35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
34990
diff
changeset

863 
where 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
34990
diff
changeset

864 
"G\<turnstile>Field fn f of C accessible_from accclass == 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
34990
diff
changeset

865 
G\<turnstile>(fieldm fn f) of C accessible_from accclass" 
12854  866 

23747  867 
inductive 
21765  868 
dyn_accessible_fromR :: "prog \<Rightarrow> qtname \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> bool" 
869 
and dyn_accessible_from' :: "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool" 

870 
("_ \<turnstile> _ in _ dyn'_accessible'_from _" [61,61,61,61] 60) 

871 
and method_dyn_accessible_from :: "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool" 

872 
("_ \<turnstile>Method _ in _ dyn'_accessible'_from _" [61,61,61,61] 60) 

873 
for G :: prog and accclass :: qtname 

874 
where 

875 
"G\<turnstile>membr in C dyn_accessible_from accC \<equiv> dyn_accessible_fromR G accC membr C" 

12854  876 

25143
2a1acc88a180
abbrevs within inductive definitions may no longer depend on each other (reflects in internal organization, particularly for output);
wenzelm
parents:
24038
diff
changeset

877 
 "G\<turnstile>Method m in C dyn_accessible_from accC \<equiv> dyn_accessible_fromR G accC (methdMembr m) C" 
12854  878 

35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
34990
diff
changeset

879 
 Immediate: "!!class. \<lbrakk>G\<turnstile>membr member_in class; 
21765  880 
G\<turnstile>membr in class permits_acc_from accclass 
881 
\<rbrakk> \<Longrightarrow> G\<turnstile>membr in class dyn_accessible_from accclass" 

12854  882 

35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
34990
diff
changeset

883 
 Overriding: "!!class. \<lbrakk>G\<turnstile>membr member_in class; 
21765  884 
membr=(C,mdecl new); 
885 
G\<turnstile>(C,new) overrides old; 

22426  886 
G\<turnstile>class \<prec>\<^sub>C supr; 
887 
G\<turnstile>Method old in supr dyn_accessible_from accclass 

21765  888 
\<rbrakk>\<Longrightarrow> G\<turnstile>membr in class dyn_accessible_from accclass" 
12854  889 

35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
34990
diff
changeset

890 
abbreviation 
12854  891 
methd_dyn_accessible_from:: 
892 
"prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool" 

893 
("_ \<turnstile>Methd _ _ in _ dyn'_accessible'_from _" [61,61,61,61,61] 60) 

35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
34990
diff
changeset

894 
where 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
34990
diff
changeset

895 
"G\<turnstile>Methd s m in C dyn_accessible_from accC == 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
34990
diff
changeset

896 
G\<turnstile>(method s m) in C dyn_accessible_from accC" 
12854  897 

35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
34990
diff
changeset

898 
abbreviation 
12854  899 
field_dyn_accessible_from:: 
900 
"prog \<Rightarrow> vname \<Rightarrow> (qtname \<times> field) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool" 

901 
("_ \<turnstile>Field _ _ in _ dyn'_accessible'_from _" [61,61,61,61,61] 60) 

35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
34990
diff
changeset

902 
where 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
34990
diff
changeset

903 
"G\<turnstile>Field fn f in dynC dyn_accessible_from accC == 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
34990
diff
changeset

904 
G\<turnstile>(fieldm fn f) in dynC dyn_accessible_from accC" 
12854  905 

906 

907 
lemma accessible_from_commonD: "G\<turnstile>m of C accessible_from S 

908 
\<Longrightarrow> G\<turnstile>m member_of C \<and> G\<turnstile>(Class C) accessible_in (pid S)" 

909 
by (auto elim: accessible_fromR.induct) 

910 

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

911 
lemma unique_declaration: 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

912 
"\<lbrakk>G\<turnstile>m declared_in C; G\<turnstile>n declared_in C; memberid m = memberid n \<rbrakk> 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

913 
\<Longrightarrow> m = n" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

914 
apply (cases m) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

915 
apply (cases n, 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

916 
auto simp add: declared_in_def cdeclaredmethd_def cdeclaredfield_def)+ 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

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

918 

12854  919 
lemma declared_not_undeclared: 
920 
"G\<turnstile>m declared_in C \<Longrightarrow> \<not> G\<turnstile> memberid m undeclared_in C" 

921 
by (cases m) (auto simp add: declared_in_def undeclared_in_def) 

922 

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

923 
lemma undeclared_not_declared: 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

924 
"G\<turnstile> memberid m undeclared_in C \<Longrightarrow> \<not> G\<turnstile> m declared_in C" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

925 
by (cases m) (auto simp add: declared_in_def undeclared_in_def) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

926 

12854  927 
lemma not_undeclared_declared: 
928 
"\<not> G\<turnstile> membr_id undeclared_in C \<Longrightarrow> (\<exists> m. G\<turnstile>m declared_in C \<and> 

929 
membr_id = memberid m)" 

930 
proof  

931 
assume not_undecl:"\<not> G\<turnstile> membr_id undeclared_in C" 

932 
show ?thesis (is "?P membr_id") 

933 
proof (cases membr_id) 

934 
case (fid vname) 

935 
with not_undecl 

936 
obtain fld where 

937 
"G\<turnstile>fdecl (vname,fld) declared_in C" 

938 
by (auto simp add: undeclared_in_def declared_in_def 

939 
cdeclaredfield_def) 

940 
with fid show ?thesis 

941 
by auto 

942 
next 

943 
case (mid sig) 

944 
with not_undecl 

945 
obtain mthd where 

946 
"G\<turnstile>mdecl (sig,mthd) declared_in C" 

947 
by (auto simp add: undeclared_in_def declared_in_def 

948 
cdeclaredmethd_def) 

949 
with mid show ?thesis 

950 
by auto 

951 
qed 

952 
qed 

953 

954 
lemma unique_declared_in: 

955 
"\<lbrakk>G\<turnstile>m declared_in C; G\<turnstile>n declared_in C; memberid m = memberid n\<rbrakk> 

956 
\<Longrightarrow> m = n" 

957 
by (auto simp add: declared_in_def cdeclaredmethd_def cdeclaredfield_def 

958 
split: memberdecl.splits) 

959 

960 
lemma unique_member_of: 

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

961 
assumes n: "G\<turnstile>n member_of C" and 
12854  962 
m: "G\<turnstile>m member_of C" and 
963 
eqid: "memberid n = memberid m" 

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

964 
shows "n=m" 
12854  965 
proof  
966 
from n m eqid 

967 
show "n=m" 

968 
proof (induct) 

21765  969 
case (Immediate n C) 
12854  970 
assume member_n: "G\<turnstile> mbr n declared_in C" "declclass n = C" 
971 
assume eqid: "memberid n = memberid m" 

972 
assume "G \<turnstile> m member_of C" 

973 
then show "n=m" 

974 
proof (cases) 

34990  975 
case Immediate 
976 
with eqid member_n 

12854  977 
show ?thesis 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32754
diff
changeset

978 
by (cases n, cases m) 
12854  979 
(auto simp add: declared_in_def 
980 
cdeclaredmethd_def cdeclaredfield_def 

981 
split: memberdecl.splits) 

982 
next 

34990  983 
case Inherited 
12854  984 
with eqid member_n 
985 
show ?thesis 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32754
diff
changeset

986 
by (cases n) (auto dest: declared_not_undeclared) 
12854  987 
qed 
988 
next 

21765  989 
case (Inherited n C S) 
12854  990 
assume undecl: "G\<turnstile> memberid n undeclared_in C" 
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35315
diff
changeset

991 
assume super: "G\<turnstile>C\<prec>\<^sub>C1S" 
12854  992 
assume hyp: "\<lbrakk>G \<turnstile> m member_of S; memberid n = memberid m\<rbrakk> \<Longrightarrow> n = m" 
993 
assume eqid: "memberid n = memberid m" 

994 
assume "G \<turnstile> m member_of C" 

995 
then show "n=m" 

996 
proof (cases) 

997 
case Immediate 

998 
then have "G\<turnstile> mbr m declared_in C" by simp 

999 
with eqid undecl 

1000 
show ?thesis 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32754
diff
changeset

1001 
by (cases m) (auto dest: declared_not_undeclared) 
12854  1002 
next 
1003 
case Inherited 

1004 
with super have "G \<turnstile> m member_of S" 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32754
diff
changeset

1005 
by (auto dest!: subcls1D) 
12854  1006 
with eqid hyp 
1007 
show ?thesis 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32754
diff
changeset

1008 
by blast 
12854  1009 
qed 
1010 
qed 

1011 
qed 

1012 

1013 
lemma member_of_is_classD: "G\<turnstile>m member_of C \<Longrightarrow> is_class G C" 

1014 
proof (induct set: members) 

21765  1015 
case (Immediate m C) 
12854  1016 
assume "G\<turnstile> mbr m declared_in C" 
1017 
then show "is_class G C" 

1018 
by (cases "mbr m") 

1019 
(auto simp add: declared_in_def cdeclaredmethd_def cdeclaredfield_def) 

1020 
next 

21765  1021 
case (Inherited m C S) 
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35315
diff
changeset

1022 
assume "G\<turnstile>C\<prec>\<^sub>C1S" and "is_class G S" 
12854  1023 
then show "is_class G C" 
1024 
by  (rule subcls_is_class2,auto) 

1025 
qed 

1026 

1027 
lemma member_of_declC: 

1028 
"G\<turnstile>m member_of C 

1029 
\<Longrightarrow> G\<turnstile>mbr m declared_in (declclass m)" 

1030 
by (induct set: members) auto 

1031 

1032 
lemma member_of_member_of_declC: 

1033 
"G\<turnstile>m member_of C 

1034 
\<Longrightarrow> G\<turnstile>m member_of (declclass m)" 

1035 
by (auto dest: member_of_declC intro: members.Immediate) 

1036 

1037 
lemma member_of_class_relation: 

1038 
"G\<turnstile>m member_of C \<Longrightarrow> G\<turnstile>C \<preceq>\<^sub>C declclass m" 

1039 
proof (induct set: members) 

21765  1040 
case (Immediate m C) 
12854  1041 
then show "G\<turnstile>C \<preceq>\<^sub>C declclass m" by simp 
1042 
next 

21765  1043 
case (Inherited m C S) 
12854  1044 
then show "G\<turnstile>C \<preceq>\<^sub>C declclass m" 
1045 
by (auto dest: r_into_rtrancl intro: rtrancl_trans) 

1046 
qed 

1047 

1048 
lemma member_in_class_relation: 

1049 
"G\<turnstile>m member_in C \<Longrightarrow> G\<turnstile>C \<preceq>\<^sub>C declclass m" 

1050 
by (auto dest: member_inD member_of_class_relation 

1051 
intro: rtrancl_trans) 

1052 

12962
a24ffe84a06a
Cleaning up the definition of static overriding.
schirmer
parents:
12937
diff
changeset

1053 
lemma stat_override_declclasses_relation: 
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35315
diff
changeset

1054 
"\<lbrakk>G\<turnstile>(declclass new) \<prec>\<^sub>C1 superNew; G \<turnstile>Method old member_of superNew \<rbrakk> 
12962
a24ffe84a06a
Cleaning up the definition of static overriding.
schirmer
parents:
12937
diff
changeset

1055 
\<Longrightarrow> G\<turnstile>(declclass new) \<prec>\<^sub>C (declclass old)" 
a24ffe84a06a
Cleaning up the definition of static overriding.
schirmer
parents:
12937
diff
changeset

1056 
apply (rule trancl_rtrancl_trancl) 
a24ffe84a06a
Cleaning up the definition of static overriding.
schirmer
parents:
12937
diff
changeset

1057 
apply (erule r_into_trancl) 
a24ffe84a06a
Cleaning up the definition of static overriding.
schirmer
parents:
12937
diff
changeset

1058 
apply (cases old) 
a24ffe84a06a
Cleaning up the definition of static overriding.
schirmer
parents:
12937
diff
changeset

1059 
apply (auto dest: member_of_class_relation) 
a24ffe84a06a
Cleaning up the definition of static overriding.
schirmer
parents:
12937
diff
changeset

1060 
done 
a24ffe84a06a
Cleaning up the definition of static overriding.
schirmer
parents:
12937
diff
changeset

1061 

a24ffe84a06a
Cleaning up the definition of static overriding.
schirmer
parents:
12937
diff
changeset

1062 
lemma stat_overrides_commonD: 
a24ffe84a06a
Cleaning up the definition of static overriding.
schirmer
parents:
12937
diff
changeset

1063 
"\<lbrakk>G\<turnstile>new overrides\<^sub>S old\<rbrakk> \<Longrightarrow> 
a24ffe84a06a
Cleaning up the definition of static overriding.
schirmer
parents:
12937
diff
changeset

1064 
declclass new \<noteq> Object \<and> \<not> is_static new \<and> msig new = msig old \<and> 
a24ffe84a06a
Cleaning up the definition of static overriding.
schirmer
parents:
12937
diff
changeset

1065 
G\<turnstile>(declclass new) \<prec>\<^sub>C (declclass old) \<and> 
a24ffe84a06a
Cleaning up the definition of static overriding.
schirmer
parents:
12937
diff
changeset

1066 
G\<turnstile>Method new declared_in (declclass new) \<and> 
a24ffe84a06a
Cleaning up the definition of static overriding.
schirmer
parents:
12937
diff
changeset

1067 
G\<turnstile>Method old declared_in (declclass old)" 
a24ffe84a06a
Cleaning up the definition of static overriding.
schirmer
parents:
12937
diff
changeset

1068 
apply (induct set: stat_overridesR) 
a24ffe84a06a
Cleaning up the definition of static overriding.
schirmer
parents:
12937
diff
changeset

1069 
apply (frule (1) stat_override_declclasses_relation) 
a24ffe84a06a
Cleaning up the definition of static overriding.
schirmer
parents:
12937
diff
changeset

1070 
apply (auto intro: trancl_trans) 
a24ffe84a06a
Cleaning up the definition of static overriding.
schirmer
parents:
12937
diff
changeset

1071 
done 
a24ffe84a06a
Cleaning up the definition of static overriding.
schirmer
parents:
12937
diff
changeset

1072 

12854  1073 
lemma member_of_Package: 
45471  1074 
assumes "G\<turnstile>m member_of C" 
1075 
and "accmodi m = Package" 

1076 
shows "pid (declclass m) = pid C" 

1077 
using assms 

1078 
proof induct 

1079 
case Immediate 

1080 
then show ?case by simp 

1081 
next 

1082 
case Inherited 

1083 
then show ?case by (auto simp add: inheritable_in_def) 

12854  1084 
qed 
1085 

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

1086 
lemma member_in_declC: "G\<turnstile>m member_in C\<Longrightarrow> G\<turnstile>m member_in (declclass m)" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

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

1088 
assume member_in_C: "G\<turnstile>m member_in C" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

1089 
from member_in_C 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

1090 
obtain provC where 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

1091 
subclseq_C_provC: "G\<turnstile> C \<preceq>\<^sub>C provC" and 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

1092 
member_of_provC: "G \<turnstile> m member_of provC" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

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

1094 
from member_of_provC 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

1095 
have "G \<turnstile> m member_of declclass m" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

1096 
by (rule member_of_member_of_declC) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

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

1098 
from member_in_C 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

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

1100 
by (rule member_in_class_relation) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

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

1102 
show ?thesis 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

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

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

1105 

12854  1106 
lemma dyn_accessible_from_commonD: "G\<turnstile>m in C dyn_accessible_from S 
1107 
\<Longrightarrow> G\<turnstile>m member_in C" 

1108 
by (auto elim: dyn_accessible_fromR.induct) 

1109 

1110 
lemma no_Private_stat_override: 

1111 
"\<lbrakk>G\<turnstile>new overrides\<^sub>S old\<rbrakk> \<Longrightarrow> accmodi old \<noteq> Private" 

1112 
by (induct set: stat_overridesR) (auto simp add: inheritable_in_def) 

1113 

1114 
lemma no_Private_override: "\<lbrakk>G\<turnstile>new overrides old\<rbrakk> \<Longrightarrow> accmodi old \<noteq> Private" 

1115 
by (induct set: overridesR) (auto simp add: inheritable_in_def) 

1116 

1117 
lemma permits_acc_inheritance: 

14030  1118 
"\<lbrakk>G\<turnstile>m in statC permits_acc_from accC; G\<turnstile>dynC \<preceq>\<^sub>C statC 
1119 
\<rbrakk> \<Longrightarrow> G\<turnstile>m in dynC permits_acc_from accC" 

12854  1120 
by (cases "accmodi m") 
1121 
(auto simp add: permits_acc_def 

1122 
intro: subclseq_trans) 

1123 

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

1124 
lemma permits_acc_static_declC: 
14030  1125 
"\<lbrakk>G\<turnstile>m in C permits_acc_from accC; G\<turnstile>m member_in C; is_static m 
1126 
\<rbrakk> \<Longrightarrow> G\<turnstile>m in (declclass m) permits_acc_from accC" 

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

1127 
by (cases "accmodi m") (auto simp add: permits_acc_def) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

1128 

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

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

1130 
assumes acc_C: "G\<turnstile>m in C dyn_accessible_from accC" and 
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

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

1132 
shows "G\<turnstile>m in (declclass m) dyn_accessible_from accC" 
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

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

1134 
from acc_C static 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

1135 
show "G\<turnstile>m in (declclass m) dyn_accessible_from accC" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

1136 
proof (induct) 
21765  1137 
case (Immediate m C) 
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

1138 
then show ?case 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

1139 
by (auto intro!: dyn_accessible_fromR.Immediate 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

1140 
dest: member_in_declC permits_acc_static_declC) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

1141 
next 
21765  1142 
case (Overriding m C declCNew new old sup) 
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

1143 
then have "\<not> is_static m" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

1144 
by (auto dest: overrides_commonD) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

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

1146 
assume "is_static m" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

1147 
ultimately show ?case 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

1148 
by contradiction 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

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

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

1151 

12854  1152 
lemma field_accessible_fromD: 
1153 
"\<lbrakk>G\<turnstile>membr of C accessible_from accC;is_field membr\<rbrakk> 

1154 
\<Longrightarrow> G\<turnstile>membr member_of C \<and> 

1155 
G\<turnstile>(Class C) accessible_in (pid accC) \<and> 

14030  1156 
G\<turnstile>membr in C permits_acc_from accC" 
12854  1157 
by (cases set: accessible_fromR) 
1158 
(auto simp add: is_field_def split: memberdecl.splits) 

1159 

1160 
lemma field_accessible_from_permits_acc_inheritance: 

1161 
"\<lbrakk>G\<turnstile>membr of statC accessible_from accC; is_field membr; G \<turnstile> dynC \<preceq>\<^sub>C statC\<rbrakk> 

14030  1162 
\<Longrightarrow> G\<turnstile>membr in dynC permits_acc_from accC" 
12854  1163 
by (auto dest: field_accessible_fromD intro: permits_acc_inheritance) 
1164 

1165 

1166 
(* 

1167 
lemma accessible_Package: 

1168 
"\<lbrakk>G \<turnstile> m of C accessible_from S;accmodi m = Package; 

1169 
\<And> new old. G\<turnstile>new overrides\<^sub>S old \<Longrightarrow> accmodi old \<le> accmodi new\<rbrakk> 

1170 
\<Longrightarrow> pid S = pid C \<and> pid C = pid (declclass m)" 

1171 
proof  

1172 
assume wf: "\<And> new old. G\<turnstile>new overrides\<^sub>S old \<Longrightarrow> accmodi old \<le> accmodi new" 

1173 
assume "G \<turnstile> m of C accessible_from S" 

1174 
then show "accmodi m = Package \<Longrightarrow> pid S = pid C \<and> pid C = pid (declclass m)" 

1175 
(is "?Pack m \<Longrightarrow> ?P C m") 

1176 
proof (induct rule: accessible_fromR.induct) 

1177 
fix C m 

1178 
assume "G\<turnstile>m member_of C" 

14030  1179 
"G \<turnstile> m in C permits_acc_from S" 
12854  1180 
"accmodi m = Package" 
1181 
then show "?P C m" 

1182 
by (auto dest: member_of_Package simp add: permits_acc_def) 

1183 
next 

1184 
fix declC C new newm old Sup 

1185 
assume member_new: "G \<turnstile> new member_of C" and 

1186 
acc_C: "G \<turnstile> Class C accessible_in pid S" and 

1187 
new: "new = (declC, mdecl newm)" and 

1188 
override: "G \<turnstile> (declC, newm) overrides\<^sub>S old" and 

1189 
subcls_C_Sup: "G\<turnstile>C \<prec>\<^sub>C Sup" and 

1190 
acc_old: "G \<turnstile> methdMembr old of Sup accessible_from S" and 

1191 
hyp: "?Pack (methdMembr old) \<Longrightarrow> ?P Sup (methdMembr old)" and 

1192 
accmodi_new: "accmodi new = Package" 

1193 
from override wf 

1194 
have accmodi_weaken: "accmodi old \<le> accmodi newm" 

1195 
by (cases old,cases newm) auto 

1196 
from override new 

1197 
have "accmodi old \<noteq> Private" 

1198 
by (simp add: no_Private_stat_override) 

1199 
with accmodi_weaken accmodi_new new 

1200 
have accmodi_old: "accmodi old = Package" 

1201 
by (cases "accmodi old") (auto simp add: le_acc_def less_acc_def) 

1202 
with hyp 

1203 
have P_sup: "?P Sup (methdMembr old)" 

1204 
by (simp) 

1205 
from wf override new accmodi_old accmodi_new 

1206 
have eq_pid_new_old: "pid (declclass new) = pid (declclass old)" 

1207 
by (auto dest: stat_override_Package) 

1208 
from member_new accmodi_new 

1209 
have "pid (declclass new) = pid C" 

1210 
by (auto dest: member_of_Package) 

1211 
with eq_pid_new_old P_sup show "?P C new" 

1212 
by auto 

1213 
qed 

1214 
qed 

1215 
*) 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13585
diff
changeset

1216 

12854  1217 
lemma accessible_fieldD: 
1218 
"\<lbrakk>G\<turnstile>membr of C accessible_from accC; is_field membr\<rbrakk> 

1219 
\<Longrightarrow> G\<turnstile>membr member_of C \<and> 

1220 
G\<turnstile>(Class C) accessible_in (pid accC) \<and> 

14030  1221 
G\<turnstile>membr in C permits_acc_from accC" 
12854  1222 
by (induct rule: accessible_fromR.induct) (auto dest: is_fieldD) 
1223 

1224 

1225 

1226 
lemma member_of_Private: 

1227 
"\<lbrakk>G\<turnstile>m member_of C; accmodi m = Private\<rbrakk> \<Longrightarrow> declclass m = C" 

1228 
by (induct set: members) (auto simp add: inheritable_in_def) 

1229 

1230 
lemma member_of_subclseq_declC: 

1231 
"G\<turnstile>m member_of C \<Longrightarrow> G\<turnstile>C \<preceq>\<^sub>C declclass m" 

1232 
by (induct set: members) (auto dest: r_into_rtrancl intro: rtrancl_trans) 

1233 

1234 
lemma member_of_inheritance: 

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

1235 
assumes m: "G\<turnstile>m member_of D" and 
12854  1236 
subclseq_D_C: "G\<turnstile>D \<preceq>\<^sub>C C" and 
1237 
subclseq_C_m: "G\<turnstile>C \<preceq>\<^sub>C declclass m" and 

1238 
ws: "ws_prog G" 

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

1239 
shows "G\<turnstile>m member_of C" 
12854  1240 
proof  
1241 
from m subclseq_D_C subclseq_C_m 

1242 
show ?thesis 

1243 
proof (induct) 

21765  1244 
case (Immediate m D) 
12854  1245 
assume "declclass m = D" and 
1246 
"G\<turnstile>D\<preceq>\<^sub>C C" and "G\<turnstile>C\<preceq>\<^sub>C declclass m" 

1247 
with ws have "D=C" 

1248 
by (auto intro: subclseq_acyclic) 

1249 
with Immediate 

1250 
show "G\<turnstile>m member_of C" 

1251 
by (auto intro: members.Immediate) 

1252 
next 

21765  1253 
case (Inherited m D S) 
12854  1254 
assume member_of_D_props: 
1255 
"G \<turnstile> m inheritable_in pid D" 

1256 
"G\<turnstile> memberid m undeclared_in D" 

1257 
"G \<turnstile> Class S accessible_in pid D" 

1258 
"G \<turnstile> m member_of S" 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35315
diff
changeset

1259 
assume super: "G\<turnstile>D\<prec>\<^sub>C1S" 
12854  1260 
assume hyp: "\<lbrakk>G\<turnstile>S\<preceq>\<^sub>C C; G\<turnstile>C\<preceq>\<^sub>C declclass m\<rbrakk> \<Longrightarrow> G \<turnstile> m member_of C" 
1261 
assume subclseq_C_m: "G\<turnstile>C\<preceq>\<^sub>C declclass m" 

1262 
assume "G\<turnstile>D\<preceq>\<^sub>C C" 

1263 
then show "G\<turnstile>m member_of C" 

1264 
proof (cases rule: subclseq_cases) 

1265 
case Eq 

1266 
assume "D=C" 

1267 
with super member_of_D_props 

1268 
show ?thesis 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32754
diff
changeset

1269 
by (auto intro: members.Inherited) 
12854  1270 
next 
1271 
case Subcls 

1272 
assume "G\<turnstile>D\<prec>\<^sub>C C" 

1273 
with super 

1274 
have "G\<turnstile>S\<preceq>\<^sub>C C" 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32754
diff
changeset

1275 
by (auto dest: subcls1D subcls_superD) 
12854  1276 
with subclseq_C_m hyp show ?thesis 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32754
diff
changeset

1277 
by blast 
12854  1278 
qed 
1279 
qed 

1280 
qed 

1281 

1282 
lemma member_of_subcls: 

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

1283 
assumes old: "G\<turnstile>old member_of C" and 
12854  1284 
new: "G\<turnstile>new member_of D" and 
1285 
eqid: "memberid new = memberid old" and 

1286 
subclseq_D_C: "G\<turnstile>D \<preceq>\<^sub>C C" and 

1287 
subcls_new_old: "G\<turnstile>declclass new \<prec>\<^sub>C declclass old" and 

1288 
ws: "ws_prog G" 

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

1289 
shows "G\<turnstile>D \<prec>\<^sub>C C" 
12854  1290 
proof  
1291 
from old 

1292 
have subclseq_C_old: "G\<turnstile>C \<preceq>\<^sub>C declclass old" 

1293 
by (auto dest: member_of_subclseq_declC) 

1294 
from new 

1295 
have subclseq_D_new: "G\<turnstile>D \<preceq>\<^sub>C declclass new" 

1296 
by (auto dest: member_of_subclseq_declC) 

1297 
from subcls_new_old ws 

1298 
have neq_new_old: "new\<noteq>old" 

1299 
by (cases new,cases old) (auto dest: subcls_irrefl) 

1300 
from subclseq_D_new subclseq_D_C 

1301 
have "G\<turnstile>(declclass new) \<preceq>\<^sub>C C \<or> G\<turnstile>C \<preceq>\<^sub>C (declclass new)" 

1302 
by (rule subcls_compareable) 

1303 
then have "G\<turnstile>(declclass new) \<preceq>\<^sub>C C" 

1304 
proof 

1305 
assume "G\<turnstile>declclass new\<preceq>\<^sub>C C" then show ?thesis . 

1306 
next 

1307 
assume "G\<turnstile>C \<preceq>\<^sub>C (declclass new)" 

1308 
with new subclseq_D_C ws 

1309 
have "G\<turnstile>new member_of C" 

1310 
by (blast intro: member_of_inheritance) 

1311 
with eqid old 

1312 
have "new=old" 

1313 
by (blast intro: unique_member_of) 

1314 
with neq_new_old 

1315 
show ?thesis 

1316 
by contradiction 

1317 
qed 

1318 
then show ?thesis 

1319 
proof (cases rule: subclseq_cases) 

1320 
case Eq 

1321 
assume "declclass new = C" 

1322 
with new have "G\<turnstile>new member_of C" 

1323 
by (auto dest: member_of_member_of_declC) 

1324 
with eqid old 

1325 
have "new=old" 

1326 
by (blast intro: unique_member_of) 

1327 
with neq_new_old 

1328 
show ?thesis 

1329 
by contradiction 

1330 
next 

1331 
case Subcls 

1332 
assume "G\<turnstile>declclass new\<prec>\<^sub>C C" 

1333 
with subclseq_D_new 

1334 
show "G\<turnstile>D\<prec>\<^sub>C C" 

1335 
by (rule rtrancl_trancl_trancl) 

1336 
qed 

1337 
qed 

1338 

1339 
corollary member_of_overrides_subcls: 

1340 
"\<lbrakk>G\<turnstile>Methd sig old member_of C; G\<turnstile>Methd sig new member_of D;G\<turnstile>D \<preceq>\<^sub>C C; 

1341 
G,sig\<turnstile>new overrides old; ws_prog G\<rbrakk> 

1342 
\<Longrightarrow> G\<turnstile>D \<prec>\<^sub>C C" 

1343 
by (drule overrides_commonD) (auto intro: member_of_subcls) 

1344 

1345 
corollary member_of_stat_overrides_subcls: 

1346 
"\<lbrakk>G\<turnstile>Methd sig old member_of C; G\<turnstile>Methd sig new member_of D;G\<turnstile>D \<preceq>\<^sub>C C; 

1347 
G,sig\<turnstile>new overrides\<^sub>S old; ws_prog G\<rbrakk> 

1348 
\<Longrightarrow> G\<turnstile>D \<prec>\<^sub>C C" 

1349 
by (drule stat_overrides_commonD) (auto intro: member_of_subcls) 

1350 

1351 

1352 

1353 
lemma inherited_field_access: 

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

1354 
assumes stat_acc: "G\<turnstile>membr of statC accessible_from accC" and 
12854  1355 
is_field: "is_field membr" and 
1356 
subclseq: "G \<turnstile> dynC \<preceq>\<^sub>C statC" 

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

1357 
shows "G\<turnstile>membr in dynC dyn_accessible_from accC" 
12854  1358 
proof  
1359 