author | wenzelm |
Mon, 25 Feb 2002 20:48:14 +0100 | |
changeset 12937 | 0c4fd7529467 |
parent 12925 | 99131847fb93 |
child 12962 | a24ffe84a06a |
permissions | -rw-r--r-- |
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 |
ID: $Id$ |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
3 |
Author: Norbert Schirmer |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
4 |
License: GPL (GNU GENERAL PUBLIC LICENSE) |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
5 |
*) |
12854 | 6 |
header {* Advanced concepts on Java declarations like overriding, inheritance, |
7 |
dynamic method lookup*} |
|
8 |
||
9 |
theory DeclConcepts = TypeRel: |
|
10 |
||
11 |
section "access control (cf. 6.6), overriding and hiding (cf. 8.4.6.1)" |
|
12 |
||
13 |
constdefs |
|
14 |
is_public :: "prog \<Rightarrow> qtname \<Rightarrow> bool" |
|
15 |
"is_public G qn \<equiv> (case class G qn of |
|
16 |
None \<Rightarrow> (case iface G qn of |
|
17 |
None \<Rightarrow> False |
|
18 |
| Some iface \<Rightarrow> access iface = Public) |
|
19 |
| Some class \<Rightarrow> access class = Public)" |
|
20 |
||
21 |
subsection "accessibility of types (cf. 6.6.1)" |
|
22 |
text {* |
|
23 |
Primitive types are always accessible, interfaces and classes are accessible |
|
24 |
in their package or if they are defined public, an array type is accessible if |
|
25 |
its element type is accessible *} |
|
26 |
||
27 |
consts accessible_in :: "prog \<Rightarrow> ty \<Rightarrow> pname \<Rightarrow> bool" |
|
28 |
("_ \<turnstile> _ accessible'_in _" [61,61,61] 60) |
|
29 |
rt_accessible_in:: "prog \<Rightarrow> ref_ty \<Rightarrow> pname \<Rightarrow> bool" |
|
30 |
("_ \<turnstile> _ accessible'_in' _" [61,61,61] 60) |
|
31 |
primrec |
|
32 |
"G\<turnstile>(PrimT p) accessible_in pack = True" |
|
33 |
accessible_in_RefT_simp: |
|
34 |
"G\<turnstile>(RefT r) accessible_in pack = G\<turnstile>r accessible_in' pack" |
|
35 |
||
36 |
"G\<turnstile>(NullT) accessible_in' pack = True" |
|
37 |
"G\<turnstile>(IfaceT I) accessible_in' pack = ((pid I = pack) \<or> is_public G I)" |
|
38 |
"G\<turnstile>(ClassT C) accessible_in' pack = ((pid C = pack) \<or> is_public G C)" |
|
39 |
"G\<turnstile>(ArrayT ty) accessible_in' pack = G\<turnstile>ty accessible_in pack" |
|
40 |
||
41 |
declare accessible_in_RefT_simp [simp del] |
|
42 |
||
43 |
constdefs |
|
44 |
is_acc_class :: "prog \<Rightarrow> pname \<Rightarrow> qtname \<Rightarrow> bool" |
|
45 |
"is_acc_class G P C \<equiv> is_class G C \<and> G\<turnstile>(Class C) accessible_in P" |
|
46 |
is_acc_iface :: "prog \<Rightarrow> pname \<Rightarrow> qtname \<Rightarrow> bool" |
|
47 |
"is_acc_iface G P I \<equiv> is_iface G I \<and> G\<turnstile>(Iface I) accessible_in P" |
|
48 |
is_acc_type :: "prog \<Rightarrow> pname \<Rightarrow> ty \<Rightarrow> bool" |
|
49 |
"is_acc_type G P T \<equiv> is_type G T \<and> G\<turnstile>T accessible_in P" |
|
50 |
is_acc_reftype :: "prog \<Rightarrow> pname \<Rightarrow> ref_ty \<Rightarrow> bool" |
|
51 |
"is_acc_reftype G P T \<equiv> isrtype G T \<and> G\<turnstile>T accessible_in' P" |
|
52 |
||
53 |
lemma is_acc_classD: |
|
54 |
"is_acc_class G P C \<Longrightarrow> is_class G C \<and> G\<turnstile>(Class C) accessible_in P" |
|
55 |
by (simp add: is_acc_class_def) |
|
56 |
||
57 |
lemma is_acc_class_is_class: "is_acc_class G P C \<Longrightarrow> is_class G C" |
|
58 |
by (auto simp add: is_acc_class_def) |
|
59 |
||
60 |
lemma is_acc_ifaceD: |
|
61 |
"is_acc_iface G P I \<Longrightarrow> is_iface G I \<and> G\<turnstile>(Iface I) accessible_in P" |
|
62 |
by (simp add: is_acc_iface_def) |
|
63 |
||
64 |
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
|
65 |
"is_acc_type G P T \<Longrightarrow> is_type G T \<and> G\<turnstile>T accessible_in P" |
12854 | 66 |
by (simp add: is_acc_type_def) |
67 |
||
68 |
lemma is_acc_reftypeD: |
|
69 |
"is_acc_reftype G P T \<Longrightarrow> isrtype G T \<and> G\<turnstile>T accessible_in' P" |
|
70 |
by (simp add: is_acc_reftype_def) |
|
71 |
||
72 |
subsection "accessibility of members" |
|
73 |
text {* |
|
74 |
The accessibility of members is more involved as the accessibility of types. |
|
75 |
We have to distinguish several cases to model the different effects of |
|
76 |
accessibility during inheritance, overriding and ordinary member access |
|
77 |
*} |
|
78 |
||
79 |
subsubsection {* Various technical conversion and selection functions *} |
|
80 |
||
81 |
text {* overloaded selector @{text accmodi} to select the access modifier |
|
82 |
out of various HOL types *} |
|
83 |
||
84 |
axclass has_accmodi < "type" |
|
85 |
consts accmodi:: "'a::has_accmodi \<Rightarrow> acc_modi" |
|
86 |
||
12859 | 87 |
instance acc_modi::has_accmodi .. |
12854 | 88 |
|
89 |
defs (overloaded) |
|
90 |
acc_modi_accmodi_def: "accmodi (a::acc_modi) \<equiv> a" |
|
91 |
||
92 |
lemma acc_modi_accmodi_simp[simp]: "accmodi (a::acc_modi) = a" |
|
93 |
by (simp add: acc_modi_accmodi_def) |
|
94 |
||
12859 | 95 |
instance access_field_type:: ("type","type") has_accmodi .. |
12854 | 96 |
|
97 |
defs (overloaded) |
|
98 |
decl_acc_modi_def: "accmodi (d::('a:: type) decl_scheme) \<equiv> access d" |
|
99 |
||
100 |
||
101 |
lemma decl_acc_modi_simp[simp]: "accmodi (d::('a::type) decl_scheme) = access d" |
|
102 |
by (simp add: decl_acc_modi_def) |
|
103 |
||
12859 | 104 |
instance * :: ("type",has_accmodi) has_accmodi .. |
12854 | 105 |
|
106 |
defs (overloaded) |
|
107 |
pair_acc_modi_def: "accmodi p \<equiv> (accmodi (snd p))" |
|
108 |
||
109 |
lemma pair_acc_modi_simp[simp]: "accmodi (x,a) = (accmodi a)" |
|
110 |
by (simp add: pair_acc_modi_def) |
|
111 |
||
12859 | 112 |
instance memberdecl :: has_accmodi .. |
12854 | 113 |
|
114 |
defs (overloaded) |
|
115 |
memberdecl_acc_modi_def: "accmodi m \<equiv> (case m of |
|
116 |
fdecl f \<Rightarrow> accmodi f |
|
117 |
| mdecl m \<Rightarrow> accmodi m)" |
|
118 |
||
119 |
lemma memberdecl_fdecl_acc_modi_simp[simp]: |
|
120 |
"accmodi (fdecl m) = accmodi m" |
|
121 |
by (simp add: memberdecl_acc_modi_def) |
|
122 |
||
123 |
lemma memberdecl_mdecl_acc_modi_simp[simp]: |
|
124 |
"accmodi (mdecl m) = accmodi m" |
|
125 |
by (simp add: memberdecl_acc_modi_def) |
|
126 |
||
127 |
text {* overloaded selector @{text declclass} to select the declaring class |
|
128 |
out of various HOL types *} |
|
129 |
||
130 |
axclass has_declclass < "type" |
|
131 |
consts declclass:: "'a::has_declclass \<Rightarrow> qtname" |
|
132 |
||
12859 | 133 |
instance pid_field_type::("type","type") has_declclass .. |
12854 | 134 |
|
135 |
defs (overloaded) |
|
136 |
qtname_declclass_def: "declclass (q::qtname) \<equiv> q" |
|
137 |
||
138 |
lemma qtname_declclass_simp[simp]: "declclass (q::qtname) = q" |
|
139 |
by (simp add: qtname_declclass_def) |
|
140 |
||
12859 | 141 |
instance * :: ("has_declclass","type") has_declclass .. |
12854 | 142 |
|
143 |
defs (overloaded) |
|
144 |
pair_declclass_def: "declclass p \<equiv> declclass (fst p)" |
|
145 |
||
146 |
lemma pair_declclass_simp[simp]: "declclass (c,x) = declclass c" |
|
147 |
by (simp add: pair_declclass_def) |
|
148 |
||
149 |
text {* overloaded selector @{text is_static} to select the static modifier |
|
150 |
out of various HOL types *} |
|
151 |
||
152 |
||
153 |
axclass has_static < "type" |
|
154 |
consts is_static :: "'a::has_static \<Rightarrow> bool" |
|
155 |
||
156 |
(* |
|
157 |
consts is_static :: "'a \<Rightarrow> bool" |
|
158 |
*) |
|
159 |
||
12859 | 160 |
instance access_field_type :: ("type","has_static") has_static .. |
12854 | 161 |
|
162 |
defs (overloaded) |
|
163 |
decl_is_static_def: |
|
164 |
"is_static (m::('a::has_static) decl_scheme) \<equiv> is_static (Decl.decl.more m)" |
|
165 |
||
12859 | 166 |
instance static_field_type :: ("type","type") has_static .. |
12854 | 167 |
|
168 |
defs (overloaded) |
|
169 |
static_field_type_is_static_def: |
|
170 |
"is_static (m::(bool,'b::type) static_field_type) \<equiv> static_val m" |
|
171 |
||
172 |
lemma member_is_static_simp: "is_static (m::'a member_scheme) = static m" |
|
173 |
apply (cases m) |
|
174 |
apply (simp add: static_field_type_is_static_def |
|
175 |
decl_is_static_def Decl.member.dest_convs) |
|
176 |
done |
|
177 |
||
12859 | 178 |
instance * :: ("type","has_static") has_static .. |
12854 | 179 |
|
180 |
defs (overloaded) |
|
181 |
pair_is_static_def: "is_static p \<equiv> is_static (snd p)" |
|
182 |
||
183 |
lemma pair_is_static_simp [simp]: "is_static (x,s) = is_static s" |
|
184 |
by (simp add: pair_is_static_def) |
|
185 |
||
186 |
lemma pair_is_static_simp1: "is_static p = is_static (snd p)" |
|
187 |
by (simp add: pair_is_static_def) |
|
188 |
||
12859 | 189 |
instance memberdecl:: has_static .. |
12854 | 190 |
|
191 |
defs (overloaded) |
|
192 |
memberdecl_is_static_def: |
|
193 |
"is_static m \<equiv> (case m of |
|
194 |
fdecl f \<Rightarrow> is_static f |
|
195 |
| mdecl m \<Rightarrow> is_static m)" |
|
196 |
||
197 |
lemma memberdecl_is_static_fdecl_simp[simp]: |
|
198 |
"is_static (fdecl f) = is_static f" |
|
199 |
by (simp add: memberdecl_is_static_def) |
|
200 |
||
201 |
lemma memberdecl_is_static_mdecl_simp[simp]: |
|
202 |
"is_static (mdecl m) = is_static m" |
|
203 |
by (simp add: memberdecl_is_static_def) |
|
204 |
||
205 |
lemma mhead_static_simp [simp]: "is_static (mhead m) = is_static m" |
|
206 |
by (cases m) (simp add: mhead_def member_is_static_simp) |
|
207 |
||
208 |
constdefs (* some mnemotic selectors for (qtname \<times> ('a::more) decl_scheme) |
|
209 |
* the first component is a class or interface name |
|
210 |
* the second component is a method, field or method head *) |
|
211 |
(* "declclass":: "(qtname \<times> ('a::more) decl_scheme) \<Rightarrow> qtname"*) |
|
212 |
(* "declclass \<equiv> fst" *) (* get the class component *) |
|
213 |
||
214 |
"decliface":: "(qtname \<times> ('a::type) decl_scheme) \<Rightarrow> qtname" |
|
215 |
"decliface \<equiv> fst" (* get the interface component *) |
|
216 |
||
217 |
(* |
|
218 |
"member":: "(qtname \<times> ('a::type) decl_scheme) \<Rightarrow> ('a::type) decl_scheme" |
|
219 |
*) |
|
220 |
"mbr":: "(qtname \<times> memberdecl) \<Rightarrow> memberdecl" |
|
221 |
"mbr \<equiv> snd" (* get the memberdecl component *) |
|
222 |
||
223 |
"mthd":: "('b \<times> 'a) \<Rightarrow> 'a" |
|
224 |
(* also used for mdecl,mhead *) |
|
225 |
"mthd \<equiv> snd" (* get the method component *) |
|
226 |
||
227 |
"fld":: "('b \<times> ('a::type) decl_scheme) \<Rightarrow> ('a::type) decl_scheme" |
|
228 |
(* also used for ((vname \<times> qtname)\<times> field) *) |
|
229 |
"fld \<equiv> snd" (* get the field component *) |
|
230 |
||
231 |
(* "accmodi" :: "('b \<times> ('a::type) decl_scheme) \<Rightarrow> acc_modi"*) |
|
232 |
(* also used for mdecl *) |
|
233 |
(* "accmodi \<equiv> access \<circ> snd"*) (* get the access modifier *) |
|
234 |
(* |
|
235 |
"is_static" ::"('b \<times> ('a::type) member_scheme) \<Rightarrow> bool" *) |
|
236 |
(* also defined for emhead cf. WellType *) |
|
237 |
(*"is_static \<equiv> static \<circ> snd"*) (* get the static modifier *) |
|
238 |
||
239 |
constdefs (* some mnemotic selectors for (vname \<times> qtname) *) |
|
240 |
fname:: "(vname \<times> 'a) \<Rightarrow> vname" (* also used for fdecl *) |
|
241 |
"fname \<equiv> fst" |
|
242 |
||
243 |
declclassf:: "(vname \<times> qtname) \<Rightarrow> qtname" |
|
244 |
"declclassf \<equiv> snd" |
|
245 |
||
246 |
(* |
|
247 |
lemma declclass_simp[simp]: "declclass (C,m) = C" |
|
248 |
by (simp add: declclass_def) |
|
249 |
*) |
|
250 |
||
251 |
lemma decliface_simp[simp]: "decliface (I,m) = I" |
|
252 |
by (simp add: decliface_def) |
|
253 |
||
254 |
lemma mbr_simp[simp]: "mbr (C,m) = m" |
|
255 |
by (simp add: mbr_def) |
|
256 |
||
257 |
lemma access_mbr_simp [simp]: "(accmodi (mbr m)) = accmodi m" |
|
258 |
by (cases m) (simp add: mbr_def) |
|
259 |
||
260 |
lemma mthd_simp[simp]: "mthd (C,m) = m" |
|
261 |
by (simp add: mthd_def) |
|
262 |
||
263 |
lemma fld_simp[simp]: "fld (C,f) = f" |
|
264 |
by (simp add: fld_def) |
|
265 |
||
266 |
lemma accmodi_simp[simp]: "accmodi (C,m) = access m" |
|
267 |
by (simp ) |
|
268 |
||
269 |
lemma access_mthd_simp [simp]: "(access (mthd m)) = accmodi m" |
|
270 |
by (cases m) (simp add: mthd_def) |
|
271 |
||
272 |
lemma access_fld_simp [simp]: "(access (fld f)) = accmodi f" |
|
273 |
by (cases f) (simp add: fld_def) |
|
274 |
||
275 |
(* |
|
276 |
lemma is_static_simp[simp]: "is_static (C,m) = static m" |
|
277 |
by (simp add: is_static_def) |
|
278 |
*) |
|
279 |
||
280 |
lemma static_mthd_simp[simp]: "static (mthd m) = is_static m" |
|
281 |
by (cases m) (simp add: mthd_def member_is_static_simp) |
|
282 |
||
283 |
lemma mthd_is_static_simp [simp]: "is_static (mthd m) = is_static m" |
|
284 |
by (cases m) simp |
|
285 |
||
286 |
lemma static_fld_simp[simp]: "static (fld f) = is_static f" |
|
287 |
by (cases f) (simp add: fld_def member_is_static_simp) |
|
288 |
||
289 |
lemma ext_field_simp [simp]: "(declclass f,fld f) = f" |
|
290 |
by (cases f) (simp add: fld_def) |
|
291 |
||
292 |
lemma ext_method_simp [simp]: "(declclass m,mthd m) = m" |
|
293 |
by (cases m) (simp add: mthd_def) |
|
294 |
||
295 |
lemma ext_mbr_simp [simp]: "(declclass m,mbr m) = m" |
|
296 |
by (cases m) (simp add: mbr_def) |
|
297 |
||
298 |
lemma fname_simp[simp]:"fname (n,c) = n" |
|
299 |
by (simp add: fname_def) |
|
300 |
||
301 |
lemma declclassf_simp[simp]:"declclassf (n,c) = c" |
|
302 |
by (simp add: declclassf_def) |
|
303 |
||
304 |
constdefs (* some mnemotic selectors for (vname \<times> qtname) *) |
|
305 |
"fldname" :: "(vname \<times> qtname) \<Rightarrow> vname" |
|
306 |
"fldname \<equiv> fst" |
|
307 |
||
308 |
"fldclass" :: "(vname \<times> qtname) \<Rightarrow> qtname" |
|
309 |
"fldclass \<equiv> snd" |
|
310 |
||
311 |
lemma fldname_simp[simp]: "fldname (n,c) = n" |
|
312 |
by (simp add: fldname_def) |
|
313 |
||
314 |
lemma fldclass_simp[simp]: "fldclass (n,c) = c" |
|
315 |
by (simp add: fldclass_def) |
|
316 |
||
317 |
lemma ext_fieldname_simp[simp]: "(fldname f,fldclass f) = f" |
|
318 |
by (simp add: fldname_def fldclass_def) |
|
319 |
||
320 |
text {* Convert a qualified method declaration (qualified with its declaring |
|
321 |
class) to a qualified member declaration: @{text methdMembr} *} |
|
322 |
||
323 |
constdefs |
|
324 |
methdMembr :: "(qtname \<times> mdecl) \<Rightarrow> (qtname \<times> memberdecl)" |
|
325 |
"methdMembr m \<equiv> (fst m,mdecl (snd m))" |
|
326 |
||
327 |
lemma methdMembr_simp[simp]: "methdMembr (c,m) = (c,mdecl m)" |
|
328 |
by (simp add: methdMembr_def) |
|
329 |
||
330 |
lemma accmodi_methdMembr_simp[simp]: "accmodi (methdMembr m) = accmodi m" |
|
331 |
by (cases m) (simp add: methdMembr_def) |
|
332 |
||
333 |
lemma is_static_methdMembr_simp[simp]: "is_static (methdMembr m) = is_static m" |
|
334 |
by (cases m) (simp add: methdMembr_def) |
|
335 |
||
336 |
lemma declclass_methdMembr_simp[simp]: "declclass (methdMembr m) = declclass m" |
|
337 |
by (cases m) (simp add: methdMembr_def) |
|
338 |
||
339 |
text {* Convert a qualified method (qualified with its declaring |
|
340 |
class) to a qualified member declaration: @{text method} *} |
|
341 |
||
342 |
constdefs |
|
343 |
method :: "sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> memberdecl)" |
|
344 |
"method sig m \<equiv> (declclass m, mdecl (sig, mthd m))" |
|
345 |
||
346 |
lemma method_simp[simp]: "method sig (C,m) = (C,mdecl (sig,m))" |
|
347 |
by (simp add: method_def) |
|
348 |
||
349 |
lemma accmodi_method_simp[simp]: "accmodi (method sig m) = accmodi m" |
|
350 |
by (simp add: method_def) |
|
351 |
||
352 |
lemma declclass_method_simp[simp]: "declclass (method sig m) = declclass m" |
|
353 |
by (simp add: method_def) |
|
354 |
||
355 |
lemma is_static_method_simp[simp]: "is_static (method sig m) = is_static m" |
|
356 |
by (cases m) (simp add: method_def) |
|
357 |
||
358 |
lemma mbr_method_simp[simp]: "mbr (method sig m) = mdecl (sig,mthd m)" |
|
359 |
by (simp add: mbr_def method_def) |
|
360 |
||
361 |
lemma memberid_method_simp[simp]: "memberid (method sig m) = mid sig" |
|
362 |
by (simp add: method_def) |
|
363 |
||
364 |
constdefs |
|
365 |
fieldm :: "vname \<Rightarrow> (qtname \<times> field) \<Rightarrow> (qtname \<times> memberdecl)" |
|
366 |
"fieldm n f \<equiv> (declclass f, fdecl (n, fld f))" |
|
367 |
||
368 |
lemma fieldm_simp[simp]: "fieldm n (C,f) = (C,fdecl (n,f))" |
|
369 |
by (simp add: fieldm_def) |
|
370 |
||
371 |
lemma accmodi_fieldm_simp[simp]: "accmodi (fieldm n f) = accmodi f" |
|
372 |
by (simp add: fieldm_def) |
|
373 |
||
374 |
lemma declclass_fieldm_simp[simp]: "declclass (fieldm n f) = declclass f" |
|
375 |
by (simp add: fieldm_def) |
|
376 |
||
377 |
lemma is_static_fieldm_simp[simp]: "is_static (fieldm n f) = is_static f" |
|
378 |
by (cases f) (simp add: fieldm_def) |
|
379 |
||
380 |
lemma mbr_fieldm_simp[simp]: "mbr (fieldm n f) = fdecl (n,fld f)" |
|
381 |
by (simp add: mbr_def fieldm_def) |
|
382 |
||
383 |
lemma memberid_fieldm_simp[simp]: "memberid (fieldm n f) = fid n" |
|
384 |
by (simp add: fieldm_def) |
|
385 |
||
386 |
text {* Select the signature out of a qualified method declaration: |
|
387 |
@{text msig} *} |
|
388 |
||
389 |
constdefs msig:: "(qtname \<times> mdecl) \<Rightarrow> sig" |
|
390 |
"msig m \<equiv> fst (snd m)" |
|
391 |
||
392 |
lemma msig_simp[simp]: "msig (c,(s,m)) = s" |
|
393 |
by (simp add: msig_def) |
|
394 |
||
395 |
text {* Convert a qualified method (qualified with its declaring |
|
396 |
class) to a qualified method declaration: @{text qmdecl} *} |
|
397 |
||
398 |
constdefs qmdecl :: "sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> mdecl)" |
|
399 |
"qmdecl sig m \<equiv> (declclass m, (sig,mthd m))" |
|
400 |
||
401 |
lemma qmdecl_simp[simp]: "qmdecl sig (C,m) = (C,(sig,m))" |
|
402 |
by (simp add: qmdecl_def) |
|
403 |
||
404 |
lemma declclass_qmdecl_simp[simp]: "declclass (qmdecl sig m) = declclass m" |
|
405 |
by (simp add: qmdecl_def) |
|
406 |
||
407 |
lemma accmodi_qmdecl_simp[simp]: "accmodi (qmdecl sig m) = accmodi m" |
|
408 |
by (simp add: qmdecl_def) |
|
409 |
||
410 |
lemma is_static_qmdecl_simp[simp]: "is_static (qmdecl sig m) = is_static m" |
|
411 |
by (cases m) (simp add: qmdecl_def) |
|
412 |
||
413 |
lemma msig_qmdecl_simp[simp]: "msig (qmdecl sig m) = sig" |
|
414 |
by (simp add: qmdecl_def) |
|
415 |
||
416 |
lemma mdecl_qmdecl_simp[simp]: |
|
417 |
"mdecl (mthd (qmdecl sig new)) = mdecl (sig, mthd new)" |
|
418 |
by (simp add: qmdecl_def) |
|
419 |
||
420 |
lemma methdMembr_qmdecl_simp [simp]: |
|
421 |
"methdMembr (qmdecl sig old) = method sig old" |
|
422 |
by (simp add: methdMembr_def qmdecl_def method_def) |
|
423 |
||
424 |
text {* overloaded selector @{text resTy} to select the result type |
|
425 |
out of various HOL types *} |
|
426 |
||
427 |
axclass has_resTy < "type" |
|
428 |
consts resTy:: "'a::has_resTy \<Rightarrow> ty" |
|
429 |
||
12859 | 430 |
instance access_field_type :: ("type","has_resTy") has_resTy .. |
12854 | 431 |
|
432 |
defs (overloaded) |
|
433 |
decl_resTy_def: |
|
434 |
"resTy (m::('a::has_resTy) decl_scheme) \<equiv> resTy (Decl.decl.more m)" |
|
435 |
||
12859 | 436 |
instance static_field_type :: ("type","has_resTy") has_resTy .. |
12854 | 437 |
|
438 |
defs (overloaded) |
|
439 |
static_field_type_resTy_def: |
|
440 |
"resTy (m::(bool,'b::has_resTy) static_field_type) |
|
441 |
\<equiv> resTy (static_more m)" |
|
442 |
||
12859 | 443 |
instance pars_field_type :: ("type","has_resTy") has_resTy .. |
12854 | 444 |
|
445 |
defs (overloaded) |
|
446 |
pars_field_type_resTy_def: |
|
447 |
"resTy (m::(vname list,'b::has_resTy) pars_field_type) |
|
448 |
\<equiv> resTy (pars_more m)" |
|
449 |
||
12859 | 450 |
instance resT_field_type :: ("type","type") has_resTy .. |
12854 | 451 |
|
452 |
defs (overloaded) |
|
453 |
resT_field_type_resTy_def: |
|
454 |
"resTy (m::(ty,'b::type) resT_field_type) |
|
455 |
\<equiv> resT_val m" |
|
456 |
||
457 |
lemma mhead_resTy_simp: "resTy (m::'a mhead_scheme) = resT m" |
|
458 |
apply (cases m) |
|
459 |
apply (simp add: decl_resTy_def static_field_type_resTy_def |
|
460 |
pars_field_type_resTy_def resT_field_type_resTy_def |
|
461 |
member.dest_convs mhead.dest_convs) |
|
462 |
done |
|
463 |
||
464 |
lemma resTy_mhead [simp]:"resTy (mhead m) = resTy m" |
|
465 |
by (simp add: mhead_def mhead_resTy_simp) |
|
466 |
||
12859 | 467 |
instance * :: ("type","has_resTy") has_resTy .. |
12854 | 468 |
|
469 |
defs (overloaded) |
|
470 |
pair_resTy_def: "resTy p \<equiv> resTy (snd p)" |
|
471 |
||
472 |
lemma pair_resTy_simp[simp]: "resTy (x,m) = resTy m" |
|
473 |
by (simp add: pair_resTy_def) |
|
474 |
||
475 |
lemma qmdecl_resTy_simp [simp]: "resTy (qmdecl sig m) = resTy m" |
|
476 |
by (cases m) (simp) |
|
477 |
||
478 |
lemma resTy_mthd [simp]:"resTy (mthd m) = resTy m" |
|
479 |
by (cases m) (simp add: mthd_def ) |
|
480 |
||
481 |
subsubsection "inheritable-in" |
|
482 |
text {* |
|
483 |
@{text "G\<turnstile>m inheritable_in P"}: m can be inherited by |
|
484 |
classes in package P if: |
|
485 |
\begin{itemize} |
|
486 |
\item the declaration class of m is accessible in P and |
|
487 |
\item the member m is declared with protected or public access or if it is |
|
488 |
declared with default (package) access, the package of the declaration |
|
489 |
class of m is also P. If the member m is declared with private access |
|
490 |
it is not accessible for inheritance at all. |
|
491 |
\end{itemize} |
|
492 |
*} |
|
493 |
constdefs |
|
494 |
inheritable_in:: |
|
495 |
"prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> pname \<Rightarrow> bool" |
|
496 |
("_ \<turnstile> _ inheritable'_in _" [61,61,61] 60) |
|
497 |
"G\<turnstile>membr inheritable_in pack |
|
498 |
\<equiv> (case (accmodi membr) of |
|
499 |
Private \<Rightarrow> False |
|
500 |
| Package \<Rightarrow> (pid (declclass membr)) = pack |
|
501 |
| Protected \<Rightarrow> True |
|
502 |
| Public \<Rightarrow> True)" |
|
503 |
||
504 |
syntax |
|
505 |
Method_inheritable_in:: |
|
506 |
"prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> pname \<Rightarrow> bool" |
|
507 |
("_ \<turnstile>Method _ inheritable'_in _ " [61,61,61] 60) |
|
508 |
||
509 |
translations |
|
510 |
"G\<turnstile>Method m inheritable_in p" == "G\<turnstile>methdMembr m inheritable_in p" |
|
511 |
||
512 |
syntax |
|
513 |
Methd_inheritable_in:: |
|
514 |
"prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> pname \<Rightarrow> bool" |
|
515 |
("_ \<turnstile>Methd _ _ inheritable'_in _ " [61,61,61,61] 60) |
|
516 |
||
517 |
translations |
|
518 |
"G\<turnstile>Methd s m inheritable_in p" == "G\<turnstile>(method s m) inheritable_in p" |
|
519 |
||
520 |
subsubsection "declared-in/undeclared-in" |
|
521 |
||
522 |
constdefs cdeclaredmethd:: "prog \<Rightarrow> qtname \<Rightarrow> (sig,methd) table" |
|
523 |
"cdeclaredmethd G C |
|
524 |
\<equiv> (case class G C of |
|
525 |
None \<Rightarrow> \<lambda> sig. None |
|
526 |
| Some c \<Rightarrow> table_of (methods c) |
|
527 |
)" |
|
528 |
||
529 |
constdefs |
|
530 |
cdeclaredfield:: "prog \<Rightarrow> qtname \<Rightarrow> (vname,field) table" |
|
531 |
"cdeclaredfield G C |
|
532 |
\<equiv> (case class G C of |
|
533 |
None \<Rightarrow> \<lambda> sig. None |
|
534 |
| Some c \<Rightarrow> table_of (cfields c) |
|
535 |
)" |
|
536 |
||
537 |
||
538 |
constdefs |
|
539 |
declared_in:: "prog \<Rightarrow> memberdecl \<Rightarrow> qtname \<Rightarrow> bool" |
|
540 |
("_\<turnstile> _ declared'_in _" [61,61,61] 60) |
|
541 |
"G\<turnstile>m declared_in C \<equiv> (case m of |
|
542 |
fdecl (fn,f ) \<Rightarrow> cdeclaredfield G C fn = Some f |
|
543 |
| mdecl (sig,m) \<Rightarrow> cdeclaredmethd G C sig = Some m)" |
|
544 |
||
545 |
syntax |
|
546 |
method_declared_in:: "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> qtname \<Rightarrow> bool" |
|
547 |
("_\<turnstile>Method _ declared'_in _" [61,61,61] 60) |
|
548 |
translations |
|
549 |
"G\<turnstile>Method m declared_in C" == "G\<turnstile>mdecl (mthd m) declared_in C" |
|
550 |
||
551 |
syntax |
|
552 |
methd_declared_in:: "prog \<Rightarrow> sig \<Rightarrow>(qtname \<times> methd) \<Rightarrow> qtname \<Rightarrow> bool" |
|
553 |
("_\<turnstile>Methd _ _ declared'_in _" [61,61,61,61] 60) |
|
554 |
translations |
|
555 |
"G\<turnstile>Methd s m declared_in C" == "G\<turnstile>mdecl (s,mthd m) declared_in C" |
|
556 |
||
557 |
lemma declared_in_classD: |
|
558 |
"G\<turnstile>m declared_in C \<Longrightarrow> is_class G C" |
|
559 |
by (cases m) |
|
560 |
(auto simp add: declared_in_def cdeclaredmethd_def cdeclaredfield_def) |
|
561 |
||
562 |
constdefs |
|
563 |
undeclared_in:: "prog \<Rightarrow> memberid \<Rightarrow> qtname \<Rightarrow> bool" |
|
564 |
("_\<turnstile> _ undeclared'_in _" [61,61,61] 60) |
|
565 |
||
566 |
"G\<turnstile>m undeclared_in C \<equiv> (case m of |
|
567 |
fid fn \<Rightarrow> cdeclaredfield G C fn = None |
|
568 |
| mid sig \<Rightarrow> cdeclaredmethd G C sig = None)" |
|
569 |
||
570 |
lemma method_declared_inI: |
|
571 |
"\<lbrakk>class G C = Some c; table_of (methods c) sig = Some m\<rbrakk> |
|
572 |
\<Longrightarrow> G\<turnstile>mdecl (sig,m) declared_in C" |
|
573 |
by (auto simp add: declared_in_def cdeclaredmethd_def) |
|
574 |
||
575 |
||
576 |
subsubsection "members" |
|
577 |
||
578 |
consts |
|
579 |
members:: "prog \<Rightarrow> (qtname \<times> (qtname \<times> memberdecl)) set" |
|
580 |
(* Can't just take a function: prog \<Rightarrow> qtname \<Rightarrow> memberdecl set because |
|
581 |
the class qtname changes to the superclass in the inductive definition |
|
582 |
below |
|
583 |
*) |
|
584 |
||
585 |
syntax |
|
586 |
member_of:: "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> bool" |
|
587 |
("_ \<turnstile> _ member'_of _" [61,61,61] 60) |
|
588 |
||
589 |
translations |
|
590 |
"G\<turnstile>m member_of C" \<rightleftharpoons> "(C,m) \<in> members G" |
|
591 |
||
592 |
inductive "members G" intros |
|
593 |
||
594 |
Immediate: "\<lbrakk>G\<turnstile>mbr m declared_in C;declclass m = C\<rbrakk> \<Longrightarrow> G\<turnstile>m member_of C" |
|
595 |
Inherited: "\<lbrakk>G\<turnstile>m inheritable_in (pid C); G\<turnstile>memberid m undeclared_in C; |
|
596 |
G\<turnstile>C \<prec>\<^sub>C\<^sub>1 S; G\<turnstile>(Class S) accessible_in (pid C);G\<turnstile>m member_of S |
|
597 |
\<rbrakk> \<Longrightarrow> G\<turnstile>m member_of C" |
|
598 |
text {* Note that in the case of an inherited member only the members of the |
|
599 |
direct superclass are concerned. If a member of a superclass of the direct |
|
600 |
superclass isn't inherited in the direct superclass (not member of the |
|
601 |
direct superclass) than it can't be a member of the class. E.g. If a |
|
602 |
member of a class A is defined with package access it isn't member of a |
|
603 |
subclass S if S isn't in the same package as A. Any further subclasses |
|
604 |
of S will not inherit the member, regardless if they are in the same |
|
605 |
package as A or not.*} |
|
606 |
||
607 |
syntax |
|
608 |
method_member_of:: "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> qtname \<Rightarrow> bool" |
|
609 |
("_ \<turnstile>Method _ member'_of _" [61,61,61] 60) |
|
610 |
||
611 |
translations |
|
612 |
"G\<turnstile>Method m member_of C" \<rightleftharpoons> "G\<turnstile>(methdMembr m) member_of C" |
|
613 |
||
614 |
syntax |
|
615 |
methd_member_of:: "prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> qtname \<Rightarrow> bool" |
|
616 |
("_ \<turnstile>Methd _ _ member'_of _" [61,61,61,61] 60) |
|
617 |
||
618 |
translations |
|
619 |
"G\<turnstile>Methd s m member_of C" \<rightleftharpoons> "G\<turnstile>(method s m) member_of C" |
|
620 |
||
621 |
syntax |
|
622 |
fieldm_member_of:: "prog \<Rightarrow> vname \<Rightarrow> (qtname \<times> field) \<Rightarrow> qtname \<Rightarrow> bool" |
|
623 |
("_ \<turnstile>Field _ _ member'_of _" [61,61,61] 60) |
|
624 |
||
625 |
translations |
|
626 |
"G\<turnstile>Field n f member_of C" \<rightleftharpoons> "G\<turnstile>fieldm n f member_of C" |
|
627 |
||
628 |
constdefs |
|
629 |
inherits:: "prog \<Rightarrow> qtname \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> bool" |
|
630 |
("_ \<turnstile> _ inherits _" [61,61,61] 60) |
|
631 |
"G\<turnstile>C inherits m |
|
632 |
\<equiv> G\<turnstile>m inheritable_in (pid C) \<and> G\<turnstile>memberid m undeclared_in C \<and> |
|
633 |
(\<exists> S. G\<turnstile>C \<prec>\<^sub>C\<^sub>1 S \<and> G\<turnstile>(Class S) accessible_in (pid C) \<and> G\<turnstile>m member_of S)" |
|
634 |
||
635 |
lemma inherits_member: "G\<turnstile>C inherits m \<Longrightarrow> G\<turnstile>m member_of C" |
|
636 |
by (auto simp add: inherits_def intro: members.Inherited) |
|
637 |
||
638 |
||
639 |
constdefs member_in::"prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> bool" |
|
640 |
("_ \<turnstile> _ member'_in _" [61,61,61] 60) |
|
641 |
"G\<turnstile>m member_in C \<equiv> \<exists> provC. G\<turnstile> C \<preceq>\<^sub>C provC \<and> G \<turnstile> m member_of provC" |
|
642 |
text {* A member is in a class if it is member of the class or a superclass. |
|
643 |
If a member is in a class we can select this member. This additional notion |
|
644 |
is necessary since not all members are inherited to subclasses. So such |
|
645 |
members are not member-of the subclass but member-in the subclass.*} |
|
646 |
||
647 |
syntax |
|
648 |
method_member_in:: "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> qtname \<Rightarrow> bool" |
|
649 |
("_ \<turnstile>Method _ member'_in _" [61,61,61] 60) |
|
650 |
||
651 |
translations |
|
652 |
"G\<turnstile>Method m member_in C" \<rightleftharpoons> "G\<turnstile>(methdMembr m) member_in C" |
|
653 |
||
654 |
syntax |
|
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) |
|
657 |
||
658 |
translations |
|
659 |
"G\<turnstile>Methd s m member_in C" \<rightleftharpoons> "G\<turnstile>(method s m) member_in C" |
|
660 |
||
661 |
consts stat_overridesR:: |
|
662 |
"prog \<Rightarrow> ((qtname \<times> mdecl) \<times> (qtname \<times> mdecl)) set" |
|
663 |
||
664 |
lemma member_inD: "G\<turnstile>m member_in C |
|
665 |
\<Longrightarrow> \<exists> provC. G\<turnstile> C \<preceq>\<^sub>C provC \<and> G \<turnstile> m member_of provC" |
|
666 |
by (auto simp add: member_in_def) |
|
667 |
||
668 |
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" |
|
669 |
by (auto simp add: member_in_def) |
|
670 |
||
671 |
lemma member_of_to_member_in: "G \<turnstile> m member_of C \<Longrightarrow> G \<turnstile>m member_in C" |
|
672 |
by (auto intro: member_inI) |
|
673 |
||
674 |
||
675 |
subsubsection "overriding" |
|
676 |
||
677 |
text {* Unfortunately the static notion of overriding (used during the |
|
678 |
typecheck of the compiler) and the dynamic notion of overriding (used during |
|
679 |
execution in the JVM) are not exactly the same. |
|
680 |
*} |
|
681 |
||
682 |
text {* Static overriding (used during the typecheck of the compiler) *} |
|
683 |
syntax |
|
684 |
stat_overrides:: "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> bool" |
|
685 |
("_ \<turnstile> _ overrides\<^sub>S _" [61,61,61] 60) |
|
686 |
translations |
|
687 |
"G\<turnstile>new overrides\<^sub>S old" == "(new,old) \<in> stat_overridesR G " |
|
688 |
||
689 |
inductive "stat_overridesR G" intros |
|
690 |
||
691 |
Direct: "\<lbrakk>\<not> is_static new; msig new = msig old; |
|
692 |
G\<turnstile>(declclass new) \<prec>\<^sub>C (declclass old); |
|
693 |
G\<turnstile>Method new declared_in (declclass new); |
|
694 |
G\<turnstile>Method old declared_in (declclass old); |
|
695 |
G\<turnstile>Method old inheritable_in pid (declclass new); |
|
696 |
G\<turnstile>(declclass new) \<prec>\<^sub>C\<^sub>1 superNew; |
|
697 |
G \<turnstile>Method old member_of superNew |
|
698 |
\<rbrakk> \<Longrightarrow> G\<turnstile>new overrides\<^sub>S old" |
|
699 |
||
700 |
Indirect: "\<lbrakk>G\<turnstile>new overrides\<^sub>S inter; G\<turnstile>inter overrides\<^sub>S old\<rbrakk> |
|
701 |
\<Longrightarrow> G\<turnstile>new overrides\<^sub>S old" |
|
702 |
||
703 |
text {* Dynamic overriding (used during the typecheck of the compiler) *} |
|
704 |
consts overridesR:: |
|
705 |
"prog \<Rightarrow> ((qtname \<times> mdecl) \<times> (qtname \<times> mdecl)) set" |
|
706 |
||
707 |
||
708 |
overrides:: "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> bool" |
|
709 |
("_ \<turnstile> _ overrides _" [61,61,61] 60) |
|
710 |
translations |
|
711 |
"G\<turnstile>new overrides old" == "(new,old) \<in> overridesR G " |
|
712 |
||
713 |
inductive "overridesR G" intros |
|
714 |
||
715 |
Direct: "\<lbrakk>\<not> is_static new; \<not> is_static old; accmodi new \<noteq> Private; |
|
716 |
msig new = msig old; |
|
717 |
G\<turnstile>(declclass new) \<prec>\<^sub>C (declclass old); |
|
718 |
G\<turnstile>Method new declared_in (declclass new); |
|
719 |
G\<turnstile>Method old declared_in (declclass old); |
|
720 |
G\<turnstile>Method old inheritable_in pid (declclass new); |
|
721 |
G\<turnstile>resTy new \<preceq> resTy old |
|
722 |
\<rbrakk> \<Longrightarrow> G\<turnstile>new overrides old" |
|
723 |
||
724 |
Indirect: "\<lbrakk>G\<turnstile>new overrides inter; G\<turnstile>inter overrides old\<rbrakk> |
|
725 |
\<Longrightarrow> G\<turnstile>new overrides old" |
|
726 |
||
727 |
syntax |
|
728 |
sig_stat_overrides:: |
|
729 |
"prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> methd) \<Rightarrow> bool" |
|
730 |
("_,_\<turnstile> _ overrides\<^sub>S _" [61,61,61,61] 60) |
|
731 |
translations |
|
732 |
"G,s\<turnstile>new overrides\<^sub>S old" \<rightharpoonup> "G\<turnstile>(qmdecl s new) overrides\<^sub>S (qmdecl s old)" |
|
733 |
||
734 |
syntax |
|
735 |
sig_overrides:: "prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> methd) \<Rightarrow> bool" |
|
736 |
("_,_\<turnstile> _ overrides _" [61,61,61,61] 60) |
|
737 |
translations |
|
738 |
"G,s\<turnstile>new overrides old" \<rightharpoonup> "G\<turnstile>(qmdecl s new) overrides (qmdecl s old)" |
|
739 |
||
740 |
subsubsection "Hiding" |
|
741 |
||
742 |
constdefs hides:: |
|
743 |
"prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> bool" |
|
744 |
("_\<turnstile> _ hides _" [61,61,61] 60) |
|
745 |
"G\<turnstile>new hides old |
|
746 |
\<equiv> is_static new \<and> msig new = msig old \<and> |
|
747 |
G\<turnstile>(declclass new) \<prec>\<^sub>C (declclass old) \<and> |
|
748 |
G\<turnstile>Method new declared_in (declclass new) \<and> |
|
749 |
G\<turnstile>Method old declared_in (declclass old) \<and> |
|
750 |
G\<turnstile>Method old inheritable_in pid (declclass new)" |
|
751 |
||
752 |
syntax |
|
753 |
sig_hides:: "prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> bool" |
|
754 |
("_,_\<turnstile> _ hides _" [61,61,61,61] 60) |
|
755 |
translations |
|
756 |
"G,s\<turnstile>new hides old" \<rightharpoonup> "G\<turnstile>(qmdecl s new) hides (qmdecl s old)" |
|
757 |
||
758 |
lemma hidesI: |
|
759 |
"\<lbrakk>is_static new; msig new = msig old; |
|
760 |
G\<turnstile>(declclass new) \<prec>\<^sub>C (declclass old); |
|
761 |
G\<turnstile>Method new declared_in (declclass new); |
|
762 |
G\<turnstile>Method old declared_in (declclass old); |
|
763 |
G\<turnstile>Method old inheritable_in pid (declclass new) |
|
764 |
\<rbrakk> \<Longrightarrow> G\<turnstile>new hides old" |
|
765 |
by (auto simp add: hides_def) |
|
766 |
||
767 |
lemma hidesD: |
|
768 |
"\<lbrakk>G\<turnstile>new hides old\<rbrakk> \<Longrightarrow> |
|
769 |
declclass new \<noteq> Object \<and> is_static new \<and> msig new = msig old \<and> |
|
770 |
G\<turnstile>(declclass new) \<prec>\<^sub>C (declclass old) \<and> |
|
771 |
G\<turnstile>Method new declared_in (declclass new) \<and> |
|
772 |
G\<turnstile>Method old declared_in (declclass old)" |
|
773 |
by (auto simp add: hides_def) |
|
774 |
||
775 |
lemma overrides_commonD: |
|
776 |
"\<lbrakk>G\<turnstile>new overrides old\<rbrakk> \<Longrightarrow> |
|
777 |
declclass new \<noteq> Object \<and> \<not> is_static new \<and> \<not> is_static old \<and> |
|
778 |
accmodi new \<noteq> Private \<and> |
|
779 |
msig new = msig old \<and> |
|
780 |
G\<turnstile>(declclass new) \<prec>\<^sub>C (declclass old) \<and> |
|
781 |
G\<turnstile>Method new declared_in (declclass new) \<and> |
|
782 |
G\<turnstile>Method old declared_in (declclass old)" |
|
783 |
by (induct set: overridesR) (auto intro: trancl_trans) |
|
784 |
||
785 |
lemma ws_overrides_commonD: |
|
786 |
"\<lbrakk>G\<turnstile>new overrides old;ws_prog G\<rbrakk> \<Longrightarrow> |
|
787 |
declclass new \<noteq> Object \<and> \<not> is_static new \<and> \<not> is_static old \<and> |
|
788 |
accmodi new \<noteq> Private \<and> G\<turnstile>resTy new \<preceq> resTy old \<and> |
|
789 |
msig new = msig old \<and> |
|
790 |
G\<turnstile>(declclass new) \<prec>\<^sub>C (declclass old) \<and> |
|
791 |
G\<turnstile>Method new declared_in (declclass new) \<and> |
|
792 |
G\<turnstile>Method old declared_in (declclass old)" |
|
793 |
by (induct set: overridesR) (auto intro: trancl_trans ws_widen_trans) |
|
794 |
||
795 |
lemma stat_overrides_commonD: |
|
796 |
"\<lbrakk>G\<turnstile>new overrides\<^sub>S old\<rbrakk> \<Longrightarrow> |
|
797 |
declclass new \<noteq> Object \<and> \<not> is_static new \<and> msig new = msig old \<and> |
|
798 |
G\<turnstile>(declclass new) \<prec>\<^sub>C (declclass old) \<and> |
|
799 |
G\<turnstile>Method new declared_in (declclass new) \<and> |
|
800 |
G\<turnstile>Method old declared_in (declclass old)" |
|
801 |
by (induct set: stat_overridesR) (auto intro: trancl_trans) |
|
802 |
||
803 |
lemma overrides_eq_sigD: |
|
804 |
"\<lbrakk>G\<turnstile>new overrides old\<rbrakk> \<Longrightarrow> msig old=msig new" |
|
805 |
by (auto dest: overrides_commonD) |
|
806 |
||
807 |
lemma hides_eq_sigD: |
|
808 |
"\<lbrakk>G\<turnstile>new hides old\<rbrakk> \<Longrightarrow> msig old=msig new" |
|
809 |
by (auto simp add: hides_def) |
|
810 |
||
811 |
subsubsection "permits access" |
|
812 |
constdefs |
|
813 |
permits_acc:: |
|
814 |
"prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool" |
|
815 |
("_ \<turnstile> _ in _ permits'_acc'_to _" [61,61,61,61] 60) |
|
816 |
||
817 |
"G\<turnstile>membr in class permits_acc_to accclass |
|
818 |
\<equiv> (case (accmodi membr) of |
|
819 |
Private \<Rightarrow> (declclass membr = accclass) |
|
820 |
| Package \<Rightarrow> (pid (declclass membr) = pid accclass) |
|
821 |
| Protected \<Rightarrow> (pid (declclass membr) = pid accclass) |
|
822 |
\<or> |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
823 |
(G\<turnstile>accclass \<prec>\<^sub>C declclass membr |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
824 |
\<and> (G\<turnstile>class \<preceq>\<^sub>C accclass \<or> is_static membr)) |
12854 | 825 |
| Public \<Rightarrow> True)" |
826 |
text {* |
|
827 |
The subcondition of the @{term "Protected"} case: |
|
828 |
@{term "G\<turnstile>accclass \<prec>\<^sub>C declclass membr"} could also be relaxed to: |
|
829 |
@{term "G\<turnstile>accclass \<preceq>\<^sub>C declclass membr"} since in case both classes are the |
|
830 |
same the other condition @{term "(pid (declclass membr) = pid accclass)"} |
|
831 |
holds anyway. |
|
832 |
*} |
|
833 |
||
834 |
text {* Like in case of overriding, the static and dynamic accessibility |
|
835 |
of members is not uniform. |
|
836 |
\begin{itemize} |
|
837 |
\item Statically the class/interface of the member must be accessible for the |
|
838 |
member to be accessible. During runtime this is not necessary. For |
|
839 |
Example, if a class is accessible and we are allowed to access a member |
|
840 |
of this class (statically) we expect that we can access this member in |
|
841 |
an arbitrary subclass (during runtime). It's not intended to restrict |
|
842 |
the access to accessible subclasses during runtime. |
|
843 |
\item Statically the member we want to access must be "member of" the class. |
|
844 |
Dynamically it must only be "member in" the class. |
|
845 |
\end{itemize} |
|
846 |
*} |
|
847 |
||
848 |
||
849 |
consts |
|
850 |
accessible_fromR:: |
|
851 |
"prog \<Rightarrow> qtname \<Rightarrow> ((qtname \<times> memberdecl) \<times> qtname) set" |
|
852 |
||
853 |
syntax |
|
854 |
accessible_from:: |
|
855 |
"prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool" |
|
856 |
("_ \<turnstile> _ of _ accessible'_from _" [61,61,61,61] 60) |
|
857 |
||
858 |
translations |
|
859 |
"G\<turnstile>membr of cls accessible_from accclass" |
|
860 |
\<rightleftharpoons> "(membr,cls) \<in> accessible_fromR G accclass" |
|
861 |
||
862 |
syntax |
|
863 |
method_accessible_from:: |
|
864 |
"prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool" |
|
865 |
("_ \<turnstile>Method _ of _ accessible'_from _" [61,61,61,61] 60) |
|
866 |
||
867 |
translations |
|
868 |
"G\<turnstile>Method m of cls accessible_from accclass" |
|
869 |
\<rightleftharpoons> "G\<turnstile>methdMembr m of cls accessible_from accclass" |
|
870 |
||
871 |
syntax |
|
872 |
methd_accessible_from:: |
|
873 |
"prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool" |
|
874 |
("_ \<turnstile>Methd _ _ of _ accessible'_from _" [61,61,61,61,61] 60) |
|
875 |
||
876 |
translations |
|
877 |
"G\<turnstile>Methd s m of cls accessible_from accclass" |
|
878 |
\<rightleftharpoons> "G\<turnstile>(method s m) of cls accessible_from accclass" |
|
879 |
||
880 |
syntax |
|
881 |
field_accessible_from:: |
|
882 |
"prog \<Rightarrow> vname \<Rightarrow> (qtname \<times> field) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool" |
|
883 |
("_ \<turnstile>Field _ _ of _ accessible'_from _" [61,61,61,61,61] 60) |
|
884 |
||
885 |
translations |
|
886 |
"G\<turnstile>Field fn f of C accessible_from accclass" |
|
887 |
\<rightleftharpoons> "G\<turnstile>(fieldm fn f) of C accessible_from accclass" |
|
888 |
||
889 |
inductive "accessible_fromR G accclass" intros |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
890 |
Immediate: "\<lbrakk>G\<turnstile>membr member_of class; |
12854 | 891 |
G\<turnstile>(Class class) accessible_in (pid accclass); |
892 |
G\<turnstile>membr in class permits_acc_to accclass |
|
893 |
\<rbrakk> \<Longrightarrow> G\<turnstile>membr of class accessible_from accclass" |
|
894 |
||
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
895 |
Overriding: "\<lbrakk>G\<turnstile>membr member_of class; |
12854 | 896 |
G\<turnstile>(Class class) accessible_in (pid accclass); |
897 |
membr=(C,mdecl new); |
|
898 |
G\<turnstile>(C,new) overrides\<^sub>S old; |
|
899 |
G\<turnstile>class \<prec>\<^sub>C sup; |
|
900 |
G\<turnstile>Method old of sup accessible_from accclass |
|
901 |
\<rbrakk>\<Longrightarrow> G\<turnstile>membr of class accessible_from accclass" |
|
902 |
||
903 |
consts |
|
904 |
dyn_accessible_fromR:: |
|
905 |
"prog \<Rightarrow> qtname \<Rightarrow> ((qtname \<times> memberdecl) \<times> qtname) set" |
|
906 |
||
907 |
syntax |
|
908 |
dyn_accessible_from:: |
|
909 |
"prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool" |
|
910 |
("_ \<turnstile> _ in _ dyn'_accessible'_from _" [61,61,61,61] 60) |
|
911 |
||
912 |
translations |
|
913 |
"G\<turnstile>membr in C dyn_accessible_from accC" |
|
914 |
\<rightleftharpoons> "(membr,C) \<in> dyn_accessible_fromR G accC" |
|
915 |
||
916 |
syntax |
|
917 |
method_dyn_accessible_from:: |
|
918 |
"prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool" |
|
919 |
("_ \<turnstile>Method _ in _ dyn'_accessible'_from _" [61,61,61,61] 60) |
|
920 |
||
921 |
translations |
|
922 |
"G\<turnstile>Method m in C dyn_accessible_from accC" |
|
923 |
\<rightleftharpoons> "G\<turnstile>methdMembr m in C dyn_accessible_from accC" |
|
924 |
||
925 |
syntax |
|
926 |
methd_dyn_accessible_from:: |
|
927 |
"prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool" |
|
928 |
("_ \<turnstile>Methd _ _ in _ dyn'_accessible'_from _" [61,61,61,61,61] 60) |
|
929 |
||
930 |
translations |
|
931 |
"G\<turnstile>Methd s m in C dyn_accessible_from accC" |
|
932 |
\<rightleftharpoons> "G\<turnstile>(method s m) in C dyn_accessible_from accC" |
|
933 |
||
934 |
syntax |
|
935 |
field_dyn_accessible_from:: |
|
936 |
"prog \<Rightarrow> vname \<Rightarrow> (qtname \<times> field) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool" |
|
937 |
("_ \<turnstile>Field _ _ in _ dyn'_accessible'_from _" [61,61,61,61,61] 60) |
|
938 |
||
939 |
translations |
|
940 |
"G\<turnstile>Field fn f in dynC dyn_accessible_from accC" |
|
941 |
\<rightleftharpoons> "G\<turnstile>(fieldm fn f) in dynC dyn_accessible_from accC" |
|
942 |
||
943 |
inductive "dyn_accessible_fromR G accclass" intros |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
944 |
Immediate: "\<lbrakk>G\<turnstile>membr member_in class; |
12854 | 945 |
G\<turnstile>membr in class permits_acc_to accclass |
946 |
\<rbrakk> \<Longrightarrow> G\<turnstile>membr in class dyn_accessible_from accclass" |
|
947 |
||
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
948 |
Overriding: "\<lbrakk>G\<turnstile>membr member_in class; |
12854 | 949 |
membr=(C,mdecl new); |
950 |
G\<turnstile>(C,new) overrides old; |
|
951 |
G\<turnstile>class \<prec>\<^sub>C sup; |
|
952 |
G\<turnstile>Method old in sup dyn_accessible_from accclass |
|
953 |
\<rbrakk>\<Longrightarrow> G\<turnstile>membr in class dyn_accessible_from accclass" |
|
954 |
||
955 |
||
956 |
lemma accessible_from_commonD: "G\<turnstile>m of C accessible_from S |
|
957 |
\<Longrightarrow> G\<turnstile>m member_of C \<and> G\<turnstile>(Class C) accessible_in (pid S)" |
|
958 |
by (auto elim: accessible_fromR.induct) |
|
959 |
||
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
960 |
lemma unique_declaration: |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
961 |
"\<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
|
962 |
\<Longrightarrow> m = n" |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
963 |
apply (cases m) |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
964 |
apply (cases n, |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
965 |
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
|
966 |
done |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
967 |
|
12854 | 968 |
lemma declared_not_undeclared: |
969 |
"G\<turnstile>m declared_in C \<Longrightarrow> \<not> G\<turnstile> memberid m undeclared_in C" |
|
970 |
by (cases m) (auto simp add: declared_in_def undeclared_in_def) |
|
971 |
||
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
972 |
lemma undeclared_not_declared: |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
973 |
"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
|
974 |
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
|
975 |
|
12854 | 976 |
lemma not_undeclared_declared: |
977 |
"\<not> G\<turnstile> membr_id undeclared_in C \<Longrightarrow> (\<exists> m. G\<turnstile>m declared_in C \<and> |
|
978 |
membr_id = memberid m)" |
|
979 |
proof - |
|
980 |
assume not_undecl:"\<not> G\<turnstile> membr_id undeclared_in C" |
|
981 |
show ?thesis (is "?P membr_id") |
|
982 |
proof (cases membr_id) |
|
983 |
case (fid vname) |
|
984 |
with not_undecl |
|
985 |
obtain fld where |
|
986 |
"G\<turnstile>fdecl (vname,fld) declared_in C" |
|
987 |
by (auto simp add: undeclared_in_def declared_in_def |
|
988 |
cdeclaredfield_def) |
|
989 |
with fid show ?thesis |
|
990 |
by auto |
|
991 |
next |
|
992 |
case (mid sig) |
|
993 |
with not_undecl |
|
994 |
obtain mthd where |
|
995 |
"G\<turnstile>mdecl (sig,mthd) declared_in C" |
|
996 |
by (auto simp add: undeclared_in_def declared_in_def |
|
997 |
cdeclaredmethd_def) |
|
998 |
with mid show ?thesis |
|
999 |
by auto |
|
1000 |
qed |
|
1001 |
qed |
|
1002 |
||
1003 |
lemma unique_declared_in: |
|
1004 |
"\<lbrakk>G\<turnstile>m declared_in C; G\<turnstile>n declared_in C; memberid m = memberid n\<rbrakk> |
|
1005 |
\<Longrightarrow> m = n" |
|
1006 |
by (auto simp add: declared_in_def cdeclaredmethd_def cdeclaredfield_def |
|
1007 |
split: memberdecl.splits) |
|
1008 |
||
1009 |
lemma unique_member_of: |
|
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
1010 |
assumes n: "G\<turnstile>n member_of C" and |
12854 | 1011 |
m: "G\<turnstile>m member_of C" and |
1012 |
eqid: "memberid n = memberid m" |
|
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
1013 |
shows "n=m" |
12854 | 1014 |
proof - |
1015 |
from n m eqid |
|
1016 |
show "n=m" |
|
1017 |
proof (induct) |
|
1018 |
case (Immediate C n) |
|
1019 |
assume member_n: "G\<turnstile> mbr n declared_in C" "declclass n = C" |
|
1020 |
assume eqid: "memberid n = memberid m" |
|
1021 |
assume "G \<turnstile> m member_of C" |
|
1022 |
then show "n=m" |
|
1023 |
proof (cases) |
|
1024 |
case (Immediate _ m') |
|
1025 |
with eqid |
|
1026 |
have "m=m'" |
|
1027 |
"memberid n = memberid m" |
|
1028 |
"G\<turnstile> mbr m declared_in C" |
|
1029 |
"declclass m = C" |
|
1030 |
by auto |
|
1031 |
with member_n |
|
1032 |
show ?thesis |
|
1033 |
by (cases n, cases m) |
|
1034 |
(auto simp add: declared_in_def |
|
1035 |
cdeclaredmethd_def cdeclaredfield_def |
|
1036 |
split: memberdecl.splits) |
|
1037 |
next |
|
1038 |
case (Inherited _ _ m') |
|
1039 |
then have "G\<turnstile> memberid m undeclared_in C" |
|
1040 |
by simp |
|
1041 |
with eqid member_n |
|
1042 |
show ?thesis |
|
1043 |
by (cases n) (auto dest: declared_not_undeclared) |
|
1044 |
qed |
|
1045 |
next |
|
1046 |
case (Inherited C S n) |
|
1047 |
assume undecl: "G\<turnstile> memberid n undeclared_in C" |
|
1048 |
assume super: "G\<turnstile>C\<prec>\<^sub>C\<^sub>1S" |
|
1049 |
assume hyp: "\<lbrakk>G \<turnstile> m member_of S; memberid n = memberid m\<rbrakk> \<Longrightarrow> n = m" |
|
1050 |
assume eqid: "memberid n = memberid m" |
|
1051 |
assume "G \<turnstile> m member_of C" |
|
1052 |
then show "n=m" |
|
1053 |
proof (cases) |
|
1054 |
case Immediate |
|
1055 |
then have "G\<turnstile> mbr m declared_in C" by simp |
|
1056 |
with eqid undecl |
|
1057 |
show ?thesis |
|
1058 |
by (cases m) (auto dest: declared_not_undeclared) |
|
1059 |
next |
|
1060 |
case Inherited |
|
1061 |
with super have "G \<turnstile> m member_of S" |
|
1062 |
by (auto dest!: subcls1D) |
|
1063 |
with eqid hyp |
|
1064 |
show ?thesis |
|
1065 |
by blast |
|
1066 |
qed |
|
1067 |
qed |
|
1068 |
qed |
|
1069 |
||
1070 |
lemma member_of_is_classD: "G\<turnstile>m member_of C \<Longrightarrow> is_class G C" |
|
1071 |
proof (induct set: members) |
|
1072 |
case (Immediate C m) |
|
1073 |
assume "G\<turnstile> mbr m declared_in C" |
|
1074 |
then show "is_class G C" |
|
1075 |
by (cases "mbr m") |
|
1076 |
(auto simp add: declared_in_def cdeclaredmethd_def cdeclaredfield_def) |
|
1077 |
next |
|
1078 |
case (Inherited C S m) |
|
1079 |
assume "G\<turnstile>C\<prec>\<^sub>C\<^sub>1S" and "is_class G S" |
|
1080 |
then show "is_class G C" |
|
1081 |
by - (rule subcls_is_class2,auto) |
|
1082 |
qed |
|
1083 |
||
1084 |
lemma member_of_declC: |
|
1085 |
"G\<turnstile>m member_of C |
|
1086 |
\<Longrightarrow> G\<turnstile>mbr m declared_in (declclass m)" |
|
1087 |
by (induct set: members) auto |
|
1088 |
||
1089 |
lemma member_of_member_of_declC: |
|
1090 |
"G\<turnstile>m member_of C |
|
1091 |
\<Longrightarrow> G\<turnstile>m member_of (declclass m)" |
|
1092 |
by (auto dest: member_of_declC intro: members.Immediate) |
|
1093 |
||
1094 |
lemma member_of_class_relation: |
|
1095 |
"G\<turnstile>m member_of C \<Longrightarrow> G\<turnstile>C \<preceq>\<^sub>C declclass m" |
|
1096 |
proof (induct set: members) |
|
1097 |
case (Immediate C m) |
|
1098 |
then show "G\<turnstile>C \<preceq>\<^sub>C declclass m" by simp |
|
1099 |
next |
|
1100 |
case (Inherited C S m) |
|
1101 |
then show "G\<turnstile>C \<preceq>\<^sub>C declclass m" |
|
1102 |
by (auto dest: r_into_rtrancl intro: rtrancl_trans) |
|
1103 |
qed |
|
1104 |
||
1105 |
lemma member_in_class_relation: |
|
1106 |
"G\<turnstile>m member_in C \<Longrightarrow> G\<turnstile>C \<preceq>\<^sub>C declclass m" |
|
1107 |
by (auto dest: member_inD member_of_class_relation |
|
1108 |
intro: rtrancl_trans) |
|
1109 |
||
1110 |
lemma member_of_Package: |
|
1111 |
"\<lbrakk>G\<turnstile>m member_of C; accmodi m = Package\<rbrakk> |
|
1112 |
\<Longrightarrow> pid (declclass m) = pid C" |
|
1113 |
proof - |
|
1114 |
assume member: "G\<turnstile>m member_of C" |
|
1115 |
then show " accmodi m = Package \<Longrightarrow> ?thesis" (is "PROP ?P m C") |
|
1116 |
proof (induct rule: members.induct) |
|
1117 |
fix C m |
|
1118 |
assume C: "declclass m = C" |
|
1119 |
then show "pid (declclass m) = pid C" |
|
1120 |
by simp |
|
1121 |
next |
|
1122 |
fix C S m |
|
1123 |
assume inheritable: "G \<turnstile> m inheritable_in pid C" |
|
1124 |
assume hyp: "PROP ?P m S" and |
|
1125 |
package_acc: "accmodi m = Package" |
|
1126 |
with inheritable package_acc hyp |
|
1127 |
show "pid (declclass m) = pid C" |
|
1128 |
by (auto simp add: inheritable_in_def) |
|
1129 |
qed |
|
1130 |
qed |
|
1131 |
||
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
1132 |
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
|
1133 |
proof - |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
1134 |
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
|
1135 |
from member_in_C |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
1136 |
obtain provC where |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
1137 |
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
|
1138 |
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
|
1139 |
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
|
1140 |
from member_of_provC |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
1141 |
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
|
1142 |
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
|
1143 |
moreover |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
1144 |
from member_in_C |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
1145 |
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
|
1146 |
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
|
1147 |
ultimately |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
1148 |
show ?thesis |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
1149 |
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
|
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 dyn_accessible_from_commonD: "G\<turnstile>m in C dyn_accessible_from S |
1153 |
\<Longrightarrow> G\<turnstile>m member_in C" |
|
1154 |
by (auto elim: dyn_accessible_fromR.induct) |
|
1155 |
||
1156 |
lemma no_Private_stat_override: |
|
1157 |
"\<lbrakk>G\<turnstile>new overrides\<^sub>S old\<rbrakk> \<Longrightarrow> accmodi old \<noteq> Private" |
|
1158 |
by (induct set: stat_overridesR) (auto simp add: inheritable_in_def) |
|
1159 |
||
1160 |
lemma no_Private_override: "\<lbrakk>G\<turnstile>new overrides old\<rbrakk> \<Longrightarrow> accmodi old \<noteq> Private" |
|
1161 |
by (induct set: overridesR) (auto simp add: inheritable_in_def) |
|
1162 |
||
1163 |
lemma permits_acc_inheritance: |
|
1164 |
"\<lbrakk>G\<turnstile>m in statC permits_acc_to accC; G\<turnstile>dynC \<preceq>\<^sub>C statC |
|
1165 |
\<rbrakk> \<Longrightarrow> G\<turnstile>m in dynC permits_acc_to accC" |
|
1166 |
by (cases "accmodi m") |
|
1167 |
(auto simp add: permits_acc_def |
|
1168 |
intro: subclseq_trans) |
|
1169 |
||
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
1170 |
lemma permits_acc_static_declC: |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
1171 |
"\<lbrakk>G\<turnstile>m in C permits_acc_to accC; G\<turnstile>m member_in C; is_static m |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
1172 |
\<rbrakk> \<Longrightarrow> G\<turnstile>m in (declclass m) permits_acc_to accC" |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
1173 |
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
|
1174 |
|
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
1175 |
lemma dyn_accessible_from_static_declC: |
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
1176 |
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
|
1177 |
static: "is_static m" |
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
1178 |
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
|
1179 |
proof - |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
1180 |
from acc_C static |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
1181 |
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
|
1182 |
proof (induct) |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
1183 |
case (Immediate C m) |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
1184 |
then show ?case |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
1185 |
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
|
1186 |
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
|
1187 |
next |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
1188 |
case (Overriding declCNew C m new old sup) |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
1189 |
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
|
1190 |
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
|
1191 |
moreover |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
1192 |
assume "is_static m" |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
1193 |
ultimately show ?case |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
1194 |
by contradiction |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
1195 |
qed |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
1196 |
qed |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
1197 |
|
12854 | 1198 |
lemma field_accessible_fromD: |
1199 |
"\<lbrakk>G\<turnstile>membr of C accessible_from accC;is_field membr\<rbrakk> |
|
1200 |
\<Longrightarrow> G\<turnstile>membr member_of C \<and> |
|
1201 |
G\<turnstile>(Class C) accessible_in (pid accC) \<and> |
|
1202 |
G\<turnstile>membr in C permits_acc_to accC" |
|
1203 |
by (cases set: accessible_fromR) |
|
1204 |
(auto simp add: is_field_def split: memberdecl.splits) |
|
1205 |
||
1206 |
lemma field_accessible_from_permits_acc_inheritance: |
|
1207 |
"\<lbrakk>G\<turnstile>membr of statC accessible_from accC; is_field membr; G \<turnstile> dynC \<preceq>\<^sub>C statC\<rbrakk> |
|
1208 |
\<Longrightarrow> G\<turnstile>membr in dynC permits_acc_to accC" |
|
1209 |
by (auto dest: field_accessible_fromD intro: permits_acc_inheritance) |
|
1210 |
||
1211 |
||
1212 |
(* |
|
1213 |
lemma accessible_Package: |
|
1214 |
"\<lbrakk>G \<turnstile> m of C accessible_from S;accmodi m = Package; |
|
1215 |
\<And> new old. G\<turnstile>new overrides\<^sub>S old \<Longrightarrow> accmodi old \<le> accmodi new\<rbrakk> |
|
1216 |
\<Longrightarrow> pid S = pid C \<and> pid C = pid (declclass m)" |
|
1217 |
proof - |
|
1218 |
assume wf: "\<And> new old. G\<turnstile>new overrides\<^sub>S old \<Longrightarrow> accmodi old \<le> accmodi new" |
|
1219 |
assume "G \<turnstile> m of C accessible_from S" |
|
1220 |
then show "accmodi m = Package \<Longrightarrow> pid S = pid C \<and> pid C = pid (declclass m)" |
|
1221 |
(is "?Pack m \<Longrightarrow> ?P C m") |
|
1222 |
proof (induct rule: accessible_fromR.induct) |
|
1223 |
fix C m |
|
1224 |
assume "G\<turnstile>m member_of C" |
|
1225 |
"G \<turnstile> m in C permits_acc_to S" |
|
1226 |
"accmodi m = Package" |
|
1227 |
then show "?P C m" |
|
1228 |
by (auto dest: member_of_Package simp add: permits_acc_def) |
|
1229 |
next |
|
1230 |
fix declC C new newm old Sup |
|
1231 |
assume member_new: "G \<turnstile> new member_of C" and |
|
1232 |
acc_C: "G \<turnstile> Class C accessible_in pid S" and |
|
1233 |
new: "new = (declC, mdecl newm)" and |
|
1234 |
override: "G \<turnstile> (declC, newm) overrides\<^sub>S old" and |
|
1235 |
subcls_C_Sup: "G\<turnstile>C \<prec>\<^sub>C Sup" and |
|
1236 |
acc_old: "G \<turnstile> methdMembr old of Sup accessible_from S" and |
|
1237 |
hyp: "?Pack (methdMembr old) \<Longrightarrow> ?P Sup (methdMembr old)" and |
|
1238 |
accmodi_new: "accmodi new = Package" |
|
1239 |
from override wf |
|
1240 |
have accmodi_weaken: "accmodi old \<le> accmodi newm" |
|
1241 |
by (cases old,cases newm) auto |
|
1242 |
from override new |
|
1243 |
have "accmodi old \<noteq> Private" |
|
1244 |
by (simp add: no_Private_stat_override) |
|
1245 |
with accmodi_weaken accmodi_new new |
|
1246 |
have accmodi_old: "accmodi old = Package" |
|
1247 |
by (cases "accmodi old") (auto simp add: le_acc_def less_acc_def) |
|
1248 |
with hyp |
|
1249 |
have P_sup: "?P Sup (methdMembr old)" |
|
1250 |
by (simp) |
|
1251 |
from wf override new accmodi_old accmodi_new |
|
1252 |
have eq_pid_new_old: "pid (declclass new) = pid (declclass old)" |
|
1253 |
by (auto dest: stat_override_Package) |
|
1254 |
from member_new accmodi_new |
|
1255 |
have "pid (declclass new) = pid C" |
|
1256 |
by (auto dest: member_of_Package) |
|
1257 |
with eq_pid_new_old P_sup show "?P C new" |
|
1258 |
by auto |
|
1259 |
qed |
|
1260 |
qed |
|
1261 |
*) |
|
1262 |
lemma accessible_fieldD: |
|
1263 |
"\<lbrakk>G\<turnstile>membr of C accessible_from accC; is_field membr\<rbrakk> |
|
1264 |
\<Longrightarrow> G\<turnstile>membr member_of C \<and> |
|
1265 |
G\<turnstile>(Class C) accessible_in (pid accC) \<and> |
|
1266 |
G\<turnstile>membr in C permits_acc_to accC" |
|
1267 |
by (induct rule: accessible_fromR.induct) (auto dest: is_fieldD) |
|
1268 |
||
1269 |
(* lemmata: |
|
1270 |
Wegen G\<turnstile>Super accessible_in (pid C) folgt: |
|
1271 |
G\<turnstile>m declared_in C; G\<turnstile>m member_of D; accmodi m = Package (G\<turnstile>D \<preceq>\<^sub>C C) |
|
1272 |
\<Longrightarrow> pid C = pid D |
|
1273 |
||
1274 |
C package |
|
1275 |
m public in C |
|
1276 |
für alle anderen D: G\<turnstile>m undeclared_in C |
|
1277 |
m wird in alle subklassen vererbt, auch aus dem Package heraus! |
|
1278 |
||
1279 |
G\<turnstile>m member_of C \<Longrightarrow> \<exists> D. G\<turnstile>C \<preceq>\<^sub>C D \<and> G\<turnstile>m declared_in D |
|
1280 |
*) |
|
1281 |
||
1282 |
(* Begriff (C,m) overrides (D,m) |
|
1283 |
3 Fälle: Direkt, |
|
1284 |
Indirekt über eine Zwischenklasse (ohne weiteres override) |
|
1285 |
Indirekt über override |
|
1286 |
*) |
|
1287 |
||
1288 |
(* |
|
1289 |
"G\<turnstile>m member_of C \<equiv> |
|
1290 |
constdefs declares_method:: "prog \<Rightarrow> sig \<Rightarrow> qtname \<Rightarrow> methd \<Rightarrow> bool" |
|
1291 |
("_,_\<turnstile> _ declares'_method _" [61,61,61,61] 60) |
|
1292 |
"G,sig\<turnstile>C declares_method m \<equiv> cdeclaredmethd G C sig = Some m" |
|
1293 |
||
1294 |
constdefs is_declared:: "prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> bool" |
|
1295 |
"is_declared G sig em \<equiv> G,sig\<turnstile>declclass em declares_method mthd em" |
|
1296 |
*) |
|
1297 |
||
1298 |
lemma member_of_Private: |
|
1299 |
"\<lbrakk>G\<turnstile>m member_of C; accmodi m = Private\<rbrakk> \<Longrightarrow> declclass m = C" |
|
1300 |
by (induct set: members) (auto simp add: inheritable_in_def) |
|
1301 |
||
1302 |
lemma member_of_subclseq_declC: |
|
1303 |
"G\<turnstile>m member_of C \<Longrightarrow> G\<turnstile>C \<preceq>\<^sub>C declclass m" |
|
1304 |
by (induct set: members) (auto dest: r_into_rtrancl intro: rtrancl_trans) |
|
1305 |
||
1306 |
lemma member_of_inheritance: |
|
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
1307 |
assumes m: "G\<turnstile>m member_of D" and |
12854 | 1308 |
subclseq_D_C: "G\<turnstile>D \<preceq>\<^sub>C C" and |
1309 |
subclseq_C_m: "G\<turnstile>C \<preceq>\<^sub>C declclass m" and |
|
1310 |
ws: "ws_prog G" |
|
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
1311 |
shows "G\<turnstile>m member_of C" |
12854 | 1312 |
proof - |
1313 |
from m subclseq_D_C subclseq_C_m |
|
1314 |
show ?thesis |
|
1315 |
proof (induct) |
|
1316 |
case (Immediate D m) |
|
1317 |
assume "declclass m = D" and |
|
1318 |
"G\<turnstile>D\<preceq>\<^sub>C C" and "G\<turnstile>C\<preceq>\<^sub>C declclass m" |
|
1319 |
with ws have "D=C" |
|
1320 |
by (auto intro: subclseq_acyclic) |
|
1321 |
with Immediate |
|
1322 |
show "G\<turnstile>m member_of C" |
|
1323 |
by (auto intro: members.Immediate) |
|
1324 |
next |
|
1325 |
case (Inherited D S m) |
|
1326 |
assume member_of_D_props: |
|
1327 |
"G \<turnstile> m inheritable_in pid D" |
|
1328 |
"G\<turnstile> memberid m undeclared_in D" |
|
1329 |
"G \<turnstile> Class S accessible_in pid D" |
|
1330 |
"G \<turnstile> m member_of S" |
|
1331 |
assume super: "G\<turnstile>D\<prec>\<^sub>C\<^sub>1S" |
|
1332 |
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" |
|
1333 |
assume subclseq_C_m: "G\<turnstile>C\<preceq>\<^sub>C declclass m" |
|
1334 |
assume "G\<turnstile>D\<preceq>\<^sub>C C" |
|
1335 |
then show "G\<turnstile>m member_of C" |
|
1336 |
proof (cases rule: subclseq_cases) |
|
1337 |
case Eq |
|
1338 |
assume "D=C" |
|
1339 |
with super member_of_D_props |
|
1340 |
show ?thesis |
|
1341 |
by (auto intro: members.Inherited) |
|
1342 |
next |
|
1343 |
case Subcls |
|
1344 |
assume "G\<turnstile>D\<prec>\<^sub>C C" |
|
1345 |
with super |
|
1346 |
have "G\<turnstile>S\<preceq>\<^sub>C C" |
|
1347 |
by (auto dest: subcls1D subcls_superD) |
|
1348 |
with subclseq_C_m hyp show ?thesis |
|
1349 |
by blast |
|
1350 |
qed |
|
1351 |
qed |
|
1352 |
qed |
|
1353 |
||
1354 |
lemma member_of_subcls: |
|
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
1355 |
assumes old: "G\<turnstile>old member_of C" and |
12854 | 1356 |
new: "G\<turnstile>new member_of D" and |
1357 |
eqid: "memberid new = memberid old" and |
|
1358 |
subclseq_D_C: "G\<turnstile>D \<preceq>\<^sub>C C" and |
|
1359 |
subcls_new_old: "G\<turnstile>declclass new \<prec>\<^sub>C declclass old" and |
|
1360 |
ws: "ws_prog G" |
|
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
1361 |
shows "G\<turnstile>D \<prec>\<^sub>C C" |
12854 | 1362 |
proof - |
1363 |
from old |
|
1364 |
have subclseq_C_old: "G\<turnstile>C \<preceq>\<^sub>C declclass old" |
|
1365 |
by (auto dest: member_of_subclseq_declC) |
|
1366 |
from new |
|
1367 |
have subclseq_D_new: "G\<turnstile>D \<preceq>\<^sub>C declclass new" |
|
1368 |
by (auto dest: member_of_subclseq_declC) |
|
1369 |
from subcls_new_old ws |
|
1370 |
have neq_new_old: "new\<noteq>old" |
|
1371 |
by (cases new,cases old) (auto dest: subcls_irrefl) |
|
1372 |
from subclseq_D_new subclseq_D_C |
|
1373 |
have "G\<turnstile>(declclass new) \<preceq>\<^sub>C C \<or> G\<turnstile>C \<preceq>\<^sub>C (declclass new)" |
|
1374 |
by (rule subcls_compareable) |
|
1375 |
then have "G\<turnstile>(declclass new) \<preceq>\<^sub>C C" |
|
1376 |
proof |
|
1377 |
assume "G\<turnstile>declclass new\<preceq>\<^sub>C C" then show ?thesis . |
|
1378 |
next |
|
1379 |
assume "G\<turnstile>C \<preceq>\<^sub>C (declclass new)" |
|
1380 |
with new subclseq_D_C ws |
|
1381 |
have "G\<turnstile>new member_of C" |
|
1382 |
by (blast intro: member_of_inheritance) |
|
1383 |
with eqid old |
|
1384 |
have "new=old" |
|
1385 |
by (blast intro: unique_member_of) |
|
1386 |
with neq_new_old |
|
1387 |
show ?thesis |
|
1388 |
by contradiction |
|
1389 |
qed |
|
1390 |
then show ?thesis |
|
1391 |
proof (cases rule: subclseq_cases) |
|
1392 |
case Eq |
|
1393 |
assume "declclass new = C" |
|
1394 |
with new have "G\<turnstile>new member_of C" |
|
1395 |
by (auto dest: member_of_member_of_declC) |
|
1396 |
with eqid old |
|
1397 |
have "new=old" |
|
1398 |
by (blast intro: unique_member_of) |
|
1399 |
with neq_new_old |
|
1400 |
show ?thesis |
|
1401 |
by contradiction |
|
1402 |
next |
|
1403 |
case Subcls |
|
1404 |
assume "G\<turnstile>declclass new\<prec>\<^sub>C C" |
|
1405 |
with subclseq_D_new |
|
1406 |
show "G\<turnstile>D\<prec>\<^sub>C C" |
|
1407 |
by (rule rtrancl_trancl_trancl) |
|
1408 |
qed |
|
1409 |
qed |
|
1410 |
||
1411 |
corollary member_of_overrides_subcls: |
|
1412 |
"\<lbrakk>G\<turnstile>Methd sig old member_of C; G\<turnstile>Methd sig new member_of D;G\<turnstile>D \<preceq>\<^sub>C C; |
|
1413 |
G,sig\<turnstile>new overrides old; ws_prog G\<rbrakk> |
|
1414 |
\<Longrightarrow> G\<turnstile>D \<prec>\<^sub>C C" |
|
1415 |
by (drule overrides_commonD) (auto intro: member_of_subcls) |
|
1416 |
||
1417 |
corollary member_of_stat_overrides_subcls: |
|
1418 |
"\<lbrakk>G\<turnstile>Methd sig old member_of C; G\<turnstile>Methd sig new member_of D;G\<turnstile>D \<preceq>\<^sub>C C; |
|
1419 |
G,sig\<turnstile>new overrides\<^sub>S old; ws_prog G\<rbrakk> |
|
1420 |
\<Longrightarrow> G\<turnstile>D \<prec>\<^sub>C C" |
|
1421 |
by (drule stat_overrides_commonD) (auto intro: member_of_subcls) |
|
1422 |
||
1423 |
||
1424 |
||
1425 |
lemma inherited_field_access: |
|
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
1426 |
assumes stat_acc: "G\<turnstile>membr of statC accessible_from accC" and |
12854 | 1427 |
is_field: "is_field membr" and |
1428 |
subclseq: "G \<turnstile> dynC \<preceq>\<^sub>C statC" |
|
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
1429 |
shows "G\<turnstile>membr in dynC dyn_accessible_from accC" |
12854 | 1430 |
proof - |
1431 |
from stat_acc is_field subclseq |
|
1432 |
show ?thesis |
|
1433 |
by (auto dest: accessible_fieldD |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
1434 |
intro: dyn_accessible_fromR.Immediate |
12854 | 1435 |
member_inI |
1436 |
permits_acc_inheritance) |
|
1437 |
qed |
|
1438 |
||
1439 |
lemma accessible_inheritance: |
|
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
1440 |
assumes stat_acc: "G\<turnstile>m of statC accessible_from accC" and |
12854 | 1441 |
subclseq: "G\<turnstile>dynC \<preceq>\<^sub>C statC" and |
1442 |
member_dynC: "G\<turnstile>m member_of dynC" and |
|
1443 |
dynC_acc: "G\<turnstile>(Class dynC) accessible_in (pid accC)" |
|
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
1444 |
shows "G\<turnstile>m of dynC accessible_from accC" |
12854 | 1445 |
proof - |
1446 |
from stat_acc |
|
1447 |
have member_statC: "G\<turnstile>m member_of statC" |
|
1448 |
by (auto dest: accessible_from_commonD) |
|
1449 |
from stat_acc |
|
1450 |
show ?thesis |
|
1451 |
proof (cases) |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
1452 |
case Immediate |
12854 | 1453 |
with member_dynC member_statC subclseq dynC_acc |
1454 |
show ?thesis |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
1455 |
by (auto intro: accessible_fromR.Immediate permits_acc_inheritance) |
12854 | 1456 |
next |
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
1457 |
case Overriding |
12854 | 1458 |
with member_dynC subclseq dynC_acc |
1459 |
show ?thesis |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
1460 |
by (auto intro: accessible_fromR.Overriding rtrancl_trancl_trancl) |
12854 | 1461 |
qed |
1462 |
qed |
|
1463 |
||
1464 |
section "fields and methods" |
|
1465 |
||
1466 |
||
1467 |
types |
|
1468 |
fspec = "vname \<times> qtname" |
|
1469 |
||
1470 |
translations |
|
1471 |
"fspec" <= (type) "vname \<times> qtname" |
|
1472 |
||
1473 |
constdefs |
|
1474 |
imethds:: "prog \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> mhead) tables" |
|
1475 |
"imethds G I |
|
1476 |
\<equiv> iface_rec (G,I) |
|
1477 |
(\<lambda>I i ts. (Un_tables ts) \<oplus>\<oplus> |
|
1478 |
(o2s \<circ> table_of (map (\<lambda>(s,m). (s,I,m)) (imethods i))))" |
|
1479 |
text {* methods of an interface, with overriding and inheritance, cf. 9.2 *} |
|
1480 |
||
1481 |
constdefs |
|
1482 |
accimethds:: "prog \<Rightarrow> pname \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> mhead) tables" |
|
1483 |
"accimethds G pack I |
|
1484 |
\<equiv> if G\<turnstile>Iface I accessible_in pack |
|
1485 |
then imethds G I |
|
1486 |
else \<lambda> k. {}" |
|
1487 |
text {* only returns imethds if the interface is accessible *} |
|
1488 |
||
1489 |
constdefs |
|
1490 |
methd:: "prog \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> methd) table" |
|
1491 |
||
1492 |
"methd G C |
|
1493 |
\<equiv> class_rec (G,C) empty |
|
1494 |
(\<lambda>C c subcls_mthds. |
|
1495 |
filter_tab (\<lambda>sig m. G\<turnstile>C inherits method sig m) |
|
1496 |
subcls_mthds |
|
1497 |
++ |
|
1498 |
table_of (map (\<lambda>(s,m). (s,C,m)) (methods c)))" |
|
1499 |
text {* @{term "methd G C"}: methods of a class C (statically visible from C), |
|
1500 |
with inheritance and hiding cf. 8.4.6; |
|
1501 |
Overriding is captured by @{text dynmethd}. |
|
1502 |
Every new method with the same signature coalesces the |
|
1503 |
method of a superclass. *} |
|
1504 |
||
1505 |
constdefs |
|
1506 |
accmethd:: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> methd) table" |
|
1507 |
"accmethd G S C |
|
1508 |
\<equiv> filter_tab (\<lambda>sig m. G\<turnstile>method sig m of C accessible_from S) |
|
1509 |
(methd G C)" |
|
1510 |
text {* @{term "accmethd G S C"}: only those methods of @{term "methd G C"}, |
|
1511 |
accessible from S *} |
|
1512 |
||
1513 |
text {* Note the class component in the accessibility filter. The class where |
|
1514 |
method @{term m} is declared (@{term declC}) isn't necessarily accessible |
|
1515 |
from the current scope @{term S}. The method can be made accessible |
|
1516 |
through inheritance, too. |
|
1517 |
So we must test accessibility of method @{term m} of class @{term C} |
|
1518 |
(not @{term "declclass m"}) *} |
|
1519 |
||
1520 |
constdefs |
|
1521 |
dynmethd:: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> methd) table" |
|
1522 |
"dynmethd G statC dynC |
|
1523 |
\<equiv> \<lambda> sig. |
|
1524 |
(if G\<turnstile>dynC \<preceq>\<^sub>C statC |
|
1525 |
then (case methd G statC sig of |
|
1526 |
None \<Rightarrow> None |
|
1527 |
| Some statM |
|
1528 |
\<Rightarrow> (class_rec (G,dynC) empty |
|
1529 |
(\<lambda>C c subcls_mthds. |
|
1530 |
subcls_mthds |
|
1531 |
++ |
|
1532 |
(filter_tab |
|
1533 |
(\<lambda> _ dynM. G,sig\<turnstile>dynM overrides statM \<or> dynM=statM) |
|
1534 |
(methd G C) )) |
|
1535 |
) sig |
|
1536 |
) |
|
1537 |
else None)" |
|
1538 |
(* |
|
1539 |
"dynmethd G statC dynC |
|
1540 |
\<equiv> \<lambda> sig. |
|
1541 |
(if G\<turnstile>dynC \<preceq>\<^sub>C statC |
|
1542 |
then (case methd G statC sig of |
|
1543 |
None \<Rightarrow> None |
|
1544 |
| Some statM |
|
1545 |
\<Rightarrow> (class_rec (G,statC) empty |
|
1546 |
(\<lambda>C c subcls_mthds. |
|
1547 |
subcls_mthds |
|
1548 |
++ |
|
1549 |
(filter_tab |
|
1550 |
(\<lambda> _ dynM. G,sig\<turnstile>dynM overrides statM) |
|
1551 |
(table_of (map (\<lambda>(s,m). (s,C,m)) (methods c))))) |
|
1552 |
) sig |
|
1553 |
) |
|
1554 |
else None)"*) |
|
1555 |
text {* @{term "dynmethd G statC dynC"}: dynamic method lookup of a reference |
|
1556 |
with dynamic class @{term dynC} and static class @{term statC} *} |
|
1557 |
text {* Note some kind of duality between @{term methd} and @{term dynmethd} |
|
1558 |
in the @{term class_rec} arguments. Whereas @{term methd} filters the |
|
1559 |
subclass methods (to get only the inherited ones), @{term dynmethd} |
|
1560 |
filters the new methods (to get only those methods which actually |
|
1561 |
override the methods of the static class) *} |
|
1562 |
||
1563 |
constdefs |
|
1564 |
dynimethd:: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> methd) table" |
|
1565 |
"dynimethd G I dynC |
|
1566 |
\<equiv> \<lambda> sig. if imethds G I sig \<noteq> {} |
|
1567 |
then methd G dynC sig |
|
1568 |
else dynmethd G Object dynC sig" |
|
1569 |
text {* @{term "dynimethd G I dynC"}: dynamic method lookup of a reference with |
|
1570 |
dynamic class dynC and static interface type I *} |
|
1571 |
text {* |
|
1572 |
When calling an interface method, we must distinguish if the method signature |
|
1573 |
was defined in the interface or if it must be an Object method in the other |
|
1574 |
case. If it was an interface method we search the class hierarchy |
|
1575 |
starting at the dynamic class of the object up to Object to find the |
|
1576 |
first matching method (@{term methd}). Since all interface methods have |
|
1577 |
public access the method can't be coalesced due to some odd visibility |
|
1578 |
effects like in case of dynmethd. The method will be inherited or |
|
1579 |
overridden in all classes from the first class implementing the interface |
|
1580 |
down to the actual dynamic class. |
|
1581 |
*} |
|
1582 |
||
1583 |
constdefs |
|
1584 |
dynlookup::"prog \<Rightarrow> ref_ty \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> methd) table" |
|
1585 |
"dynlookup G statT dynC |
|
1586 |
\<equiv> (case statT of |
|
1587 |
NullT \<Rightarrow> empty |
|
1588 |
| IfaceT I \<Rightarrow> dynimethd G I dynC |
|
1589 |
| ClassT statC \<Rightarrow> dynmethd G statC dynC |
|
1590 |
| ArrayT ty \<Rightarrow> dynmethd G Object dynC)" |
|
1591 |
text {* @{term "dynlookup G statT dynC"}: dynamic lookup of a method within the |
|
1592 |
static reference type statT and the dynamic class dynC. |
|
1593 |
In a wellformd context statT will not be NullT and in case |
|
1594 |
statT is an array type, dynC=Object *} |
|
1595 |
||
1596 |
constdefs |
|
1597 |
fields:: "prog \<Rightarrow> qtname \<Rightarrow> ((vname \<times> qtname) \<times> field) list" |
|
1598 |
"fields G C |
|
1599 |
\<equiv> class_rec (G,C) [] (\<lambda>C c ts. map (\<lambda>(n,t). ((n,C),t)) (cfields c) @ ts)" |
|
1600 |
text {* @{term "fields G C"} |
|
1601 |
list of fields of a class, including all the fields of the superclasses |
|
1602 |
(private, inherited and hidden ones) not only the accessible ones |
|
1603 |
(an instance of a object allocates all these fields *} |
|
1604 |
||
1605 |
constdefs |
|
1606 |
accfield:: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> (vname, qtname \<times> field) table" |
|
1607 |
"accfield G S C |
|
1608 |
\<equiv> let field_tab = table_of((map (\<lambda>((n,d),f).(n,(d,f)))) (fields G C)) |
|
1609 |
in filter_tab (\<lambda>n (declC,f). G\<turnstile> (declC,fdecl (n,f)) of C accessible_from S) |
|
1610 |
field_tab" |
|
1611 |
text {* @{term "accfield G C S"}: fields of a class @{term C} which are |
|
1612 |
accessible from scope of class |
|
1613 |
@{term S} with inheritance and hiding, cf. 8.3 *} |
|
1614 |
text {* note the class component in the accessibility filter (see also |
|
1615 |
@{term methd}). |
|
1616 |
The class declaring field @{term f} (@{term declC}) isn't necessarily |
|
1617 |
accessible from scope @{term S}. The field can be made visible through |
|
1618 |
inheritance, too. So we must test accessibility of field @{term f} of class |
|
1619 |
@{term C} (not @{term "declclass f"}) *} |
|
1620 |
||
1621 |
constdefs |
|
1622 |
||
1623 |
is_methd :: "prog \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> bool" |
|
1624 |
"is_methd G \<equiv> \<lambda>C sig. is_class G C \<and> methd G C sig \<noteq> None" |
|
1625 |
||
1626 |
constdefs efname:: "((vname \<times> qtname) \<times> field) \<Rightarrow> (vname \<times> qtname)" |
|
1627 |
"efname \<equiv> fst" |
|
1628 |
||
1629 |
lemma efname_simp[simp]:"efname (n,f) = n" |
|
1630 |
by (simp add: efname_def) |
|
1631 |
||
1632 |
||
1633 |
subsection "imethds" |
|
1634 |
||
1635 |
lemma imethds_rec: "\<lbrakk>iface G I = Some i; ws_prog G\<rbrakk> \<Longrightarrow> |
|
1636 |
imethds G I = Un_tables ((\<lambda>J. imethds G J)`set (isuperIfs i)) \<oplus>\<oplus> |
|
1637 |
(o2s \<circ> table_of (map (\<lambda>(s,mh). (s,I,mh)) (imethods i)))" |
|
1638 |
apply (unfold imethds_def) |
|
1639 |
apply (rule iface_rec [THEN trans]) |
|
1640 |
apply auto |
|
1641 |
done |
|
1642 |
||
1643 |
||
1644 |
(* local lemma *) |
|
1645 |
lemma imethds_norec: |
|
1646 |
"\<lbrakk>iface G md = Some i; ws_prog G; table_of (imethods i) sig = Some mh\<rbrakk> \<Longrightarrow> |
|
1647 |
(md, mh) \<in> imethds G md sig" |
|
1648 |
apply (subst imethds_rec) |
|
1649 |
apply assumption+ |
|
1650 |
apply (rule iffD2) |
|
1651 |
apply (rule overrides_t_Some_iff) |
|
1652 |
apply (rule disjI1) |
|
1653 |
apply (auto elim: table_of_map_SomeI) |
|
1654 |
done |
|
1655 |
||
1656 |
lemma imethds_declI: "\<lbrakk>m \<in> imethds G I sig; ws_prog G; is_iface G I\<rbrakk> \<Longrightarrow> |
|
1657 |
(\<exists>i. iface G (decliface m) = Some i \<and> |
|
1658 |
table_of (imethods i) sig = Some (mthd m)) \<and> |
|
1659 |
(I,decliface m) \<in> (subint1 G)^* \<and> m \<in> imethds G (decliface m) sig" |
|
1660 |
apply (erule make_imp) |
|
1661 |
apply (rule ws_subint1_induct, assumption, assumption) |
|
1662 |
apply (subst imethds_rec, erule conjunct1, assumption) |
|
1663 |
apply (force elim: imethds_norec intro: rtrancl_into_rtrancl2) |
|
1664 |
done |
|
1665 |
||
1666 |
lemma imethds_cases [consumes 3, case_names NewMethod InheritedMethod]: |
|
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
1667 |
assumes im: "im \<in> imethds G I sig" and |
12854 | 1668 |
ifI: "iface G I = Some i" and |
1669 |
ws: "ws_prog G" and |
|
1670 |
hyp_new: "table_of (map (\<lambda>(s, mh). (s, I, mh)) (imethods i)) sig |
|
1671 |
= Some im \<Longrightarrow> P" and |
|
1672 |
hyp_inh: "\<And> J. \<lbrakk>J \<in> set (isuperIfs i); im \<in> imethds G J sig\<rbrakk> \<Longrightarrow> P" |
|
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
1673 |
shows P |
12854 | 1674 |
proof - |
1675 |
from ifI ws im hyp_new hyp_inh |
|
1676 |
show "P" |
|
1677 |
by (auto simp add: imethds_rec) |
|
1678 |
qed |
|
1679 |
||
1680 |
subsection "accimethd" |
|
1681 |
||
1682 |
lemma accimethds_simp [simp]: |
|
1683 |
"G\<turnstile>Iface I accessible_in pack \<Longrightarrow> accimethds G pack I = imethds G I" |
|
1684 |
by (simp add: accimethds_def) |
|
1685 |
||
1686 |
lemma accimethdsD: |
|
1687 |
"im \<in> accimethds G pack I sig |
|
1688 |
\<Longrightarrow> im \<in> imethds G I sig \<and> G\<turnstile>Iface I accessible_in pack" |
|
1689 |
by (auto simp add: accimethds_def) |
|
1690 |
||
1691 |
lemma accimethdsI: |
|
1692 |
"\<lbrakk>im \<in> imethds G I sig;G\<turnstile>Iface I accessible_in pack\<rbrakk> |
|
1693 |
\<Longrightarrow> im \<in> accimethds G pack I sig" |
|
1694 |
by simp |
|
1695 |
||
1696 |
subsection "methd" |
|
1697 |
||
1698 |
lemma methd_rec: "\<lbrakk>class G C = Some c; ws_prog G\<rbrakk> \<Longrightarrow> |
|
1699 |
methd G C |
|
1700 |
= (if C = Object |
|
1701 |
then empty |
|
1702 |
else filter_tab (\<lambda>sig m. G\<turnstile>C inherits method sig m) |
|
1703 |
(methd G (super c))) |
|
1704 |
++ table_of (map (\<lambda>(s,m). (s,C,m)) (methods c))" |
|
1705 |
apply (unfold methd_def) |
|
1706 |
apply (erule class_rec [THEN trans], assumption) |
|
1707 |
apply (simp) |
|
1708 |
done |
|
1709 |
||
1710 |
(* local lemma *) |
|
1711 |
lemma methd_norec: |
|
1712 |
"\<lbrakk>class G declC = Some c; ws_prog G;table_of (methods c) sig = Some m\<rbrakk> |
|
1713 |
\<Longrightarrow> methd G declC sig = Some (declC, m)" |
|
1714 |
apply (simp only: methd_rec) |
|
1715 |
apply (rule disjI1 [THEN override_Some_iff [THEN iffD2]]) |
|
1716 |
apply (auto elim: table_of_map_SomeI) |
|
1717 |
done |
|
1718 |
||
1719 |
||
1720 |
lemma methd_declC: |
|
1721 |
"\<lbrakk>methd G C sig = Some m; ws_prog G;is_class G C\<rbrakk> \<Longrightarrow> |
|
1722 |
(\<exists>d. class G (declclass m)=Some d \<and> table_of (methods d) sig=Some (mthd m)) \<and> |
|
1723 |
G\<turnstile>C \<preceq>\<^sub>C (declclass m) \<and> methd G (declclass m) sig = Some m" |
|
1724 |
apply (erule make_imp) |
|
1725 |
apply (rule ws_subcls1_induct, assumption, assumption) |
|
1726 |
apply (subst methd_rec, assumption) |
|
1727 |
apply (case_tac "Ca=Object") |
|
1728 |
apply (force elim: methd_norec ) |
|
1729 |
||
1730 |
apply simp |
|
1731 |
apply (case_tac "table_of (map (\<lambda>(s, m). (s, Ca, m)) (methods c)) sig") |
|
1732 |
apply (force intro: rtrancl_into_rtrancl2) |
|
1733 |
||
1734 |
apply (auto intro: methd_norec) |
|
1735 |
done |
|
1736 |
||
1737 |
lemma methd_inheritedD: |
|
1738 |
"\<lbrakk>class G C = Some c; ws_prog G;methd G C sig = Some m\<rbrakk> |
|
1739 |
\<Longrightarrow> (declclass m \<noteq> C \<longrightarrow> G \<turnstile>C inherits method sig m)" |
|
1740 |
by (auto simp add: methd_rec) |
|
1741 |
||
1742 |
lemma methd_diff_cls: |
|
1743 |
"\<lbrakk>ws_prog G; is_class G C; is_class G D; |
|
1744 |
methd G C sig = m; methd G D sig = n; m\<noteq>n |
|
1745 |
\<rbrakk> \<Longrightarrow> C\<noteq>D" |
|
1746 |
by (auto simp add: methd_rec) |
|
1747 |
||
1748 |
lemma method_declared_inI: |
|
1749 |
"\<lbrakk>table_of (methods c) sig = Some m; class G C = Some c\<rbrakk> |
|
1750 |
\<Longrightarrow> G\<turnstile>mdecl (sig,m) declared_in C" |
|
1751 |
by (auto simp add: cdeclaredmethd_def declared_in_def) |
|
1752 |
||
1753 |
lemma methd_declared_in_declclass: |
|
1754 |
"\<lbrakk>methd G C sig = Some m; ws_prog G;is_class G C\<rbrakk> |
|
1755 |
\<Longrightarrow> G\<turnstile>Methd sig m declared_in (declclass m)" |
|
1756 |
by (auto dest: methd_declC method_declared_inI) |
|
1757 |
||
1758 |
lemma member_methd: |
|
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
1759 |
assumes member_of: "G\<turnstile>Methd sig m member_of C" and |
12854 | 1760 |
ws: "ws_prog G" |
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
1761 |
shows "methd G C sig = Some m" |
12854 | 1762 |
proof - |
1763 |
from member_of |
|
1764 |
have iscls_C: "is_class G C" |
|
1765 |
by (rule member_of_is_classD) |
|
1766 |
from iscls_C ws member_of |
|
1767 |
show ?thesis (is "?Methd C") |
|
1768 |
proof (induct rule: ws_class_induct') |
|
1769 |
case (Object co) |
|
1770 |
assume "G \<turnstile>Methd sig m member_of Object" |
|
1771 |
then have "G\<turnstile>Methd sig m declared_in Object \<and> declclass m = Object" |
|
1772 |
by (cases set: members) (cases m, auto dest: subcls1D) |
|
1773 |
with ws Object |
|
1774 |
show "?Methd Object" |
|
1775 |
by (cases m) |
|
1776 |
(auto simp add: declared_in_def cdeclaredmethd_def methd_rec |
|
1777 |
intro: table_of_mapconst_SomeI) |
|
1778 |
next |
|
1779 |
case (Subcls C c) |
|
1780 |
assume clsC: "class G C = Some c" and |
|
1781 |
neq_C_Obj: "C \<noteq> Object" and |
|
1782 |
hyp: "G \<turnstile>Methd sig m member_of super c \<Longrightarrow> ?Methd (super c)" and |
|
1783 |
member_of: "G \<turnstile>Methd sig m member_of C" |
|
1784 |
from member_of |
|
1785 |
show "?Methd C" |
|
1786 |
proof (cases) |
|
1787 |
case (Immediate Ca membr) |
|
1788 |
then have "Ca=C" "membr = method sig m" and |
|
1789 |
"G\<turnstile>Methd sig m declared_in C" "declclass m = C" |
|
1790 |
by (cases m,auto) |
|
1791 |
with clsC |
|
1792 |
have "table_of (map (\<lambda>(s, m). (s, C, m)) (methods c)) sig = Some m" |
|
1793 |
by (cases m) |
|
1794 |
(auto simp add: declared_in_def cdeclaredmethd_def |
|
1795 |
intro: table_of_mapconst_SomeI) |
|
1796 |
with clsC neq_C_Obj ws |
|
1797 |
show ?thesis |
|
1798 |
by (simp add: methd_rec) |
|
1799 |
next |
|
1800 |
case (Inherited Ca S membr) |
|
1801 |
with clsC |
|
1802 |
have eq_Ca_C: "Ca=C" and |
|
1803 |
undecl: "G\<turnstile>mid sig undeclared_in C" and |
|
1804 |
super: "G \<turnstile>Methd sig m member_of (super c)" |
|
1805 |
by (auto dest: subcls1D) |
|
1806 |
from eq_Ca_C clsC undecl |
|
1807 |
have "table_of (map (\<lambda>(s, m). (s, C, m)) (methods c)) sig = None" |
|
1808 |
by (auto simp add: undeclared_in_def cdeclaredmethd_def |
|
1809 |
intro: table_of_mapconst_NoneI) |
|
1810 |
moreover |
|
1811 |
from Inherited have "G \<turnstile> C inherits (method sig m)" |
|
1812 |
by (auto simp add: inherits_def) |
|
1813 |
moreover |
|
1814 |
note clsC neq_C_Obj ws super hyp |
|
1815 |
ultimately |
|
1816 |
show ?thesis |
|
1817 |
by (auto simp add: methd_rec intro: filter_tab_SomeI) |
|
1818 |
qed |
|
1819 |
qed |
|
1820 |
qed |
|
1821 |
||
1822 |
(*unused*) |
|
1823 |
lemma finite_methd:"ws_prog G \<Longrightarrow> finite {methd G C sig |sig C. is_class G C}" |
|
1824 |
apply (rule finite_is_class [THEN finite_SetCompr2]) |
|
1825 |
apply (intro strip) |
|
1826 |
apply (erule_tac ws_subcls1_induct, assumption) |
|
1827 |
apply (subst methd_rec) |
|
1828 |
apply (assumption) |
|
1829 |
apply (auto intro!: finite_range_map_of finite_range_filter_tab finite_range_map_of_override) |
|
1830 |
done |
|
1831 |
||
1832 |
lemma finite_dom_methd: |
|
1833 |
"\<lbrakk>ws_prog G; is_class G C\<rbrakk> \<Longrightarrow> finite (dom (methd G C))" |
|
1834 |
apply (erule_tac ws_subcls1_induct) |
|
1835 |
apply assumption |
|
1836 |
apply (subst methd_rec) |
|
1837 |
apply (assumption) |
|
1838 |
apply (auto intro!: finite_dom_map_of finite_dom_filter_tab) |
|
1839 |
done |
|
1840 |
||
1841 |
||
1842 |
subsection "accmethd" |
|
1843 |
||
1844 |
lemma accmethd_SomeD: |
|
1845 |
"accmethd G S C sig = Some m |
|
1846 |
\<Longrightarrow> methd G C sig = Some m \<and> G\<turnstile>method sig m of C accessible_from S" |
|
1847 |
by (auto simp add: accmethd_def dest: filter_tab_SomeD) |
|
1848 |
||
1849 |
lemma accmethd_SomeI: |
|
1850 |
"\<lbrakk>methd G C sig = Some m; G\<turnstile>method sig m of C accessible_from S\<rbrakk> |
|
1851 |
\<Longrightarrow> accmethd G S C sig = Some m" |
|
1852 |
by (auto simp add: accmethd_def intro: filter_tab_SomeI) |
|
1853 |
||
1854 |
lemma accmethd_declC: |
|
1855 |
"\<lbrakk>accmethd G S C sig = Some m; ws_prog G; is_class G C\<rbrakk> \<Longrightarrow> |
|
1856 |
(\<exists>d. class G (declclass m)=Some d \<and> |
|
1857 |
table_of (methods d) sig=Some (mthd m)) \<and> |
|
1858 |
G\<turnstile>C \<preceq>\<^sub>C (declclass m) \<and> methd G (declclass m) sig = Some m \<and> |
|
1859 |
G\<turnstile>method sig m of C accessible_from S" |
|
1860 |
by (auto dest: accmethd_SomeD methd_declC accmethd_SomeI) |
|
1861 |
||
1862 |
||
1863 |
lemma finite_dom_accmethd: |
|
1864 |
"\<lbrakk>ws_prog G; is_class G C\<rbrakk> \<Longrightarrow> finite (dom (accmethd G S C))" |
|
1865 |
by (auto simp add: accmethd_def intro: finite_dom_filter_tab finite_dom_methd) |
|
1866 |
||
1867 |
||
1868 |
subsection "dynmethd" |
|
1869 |
||
1870 |
lemma dynmethd_rec: |
|
1871 |
"\<lbrakk>class G dynC = Some c; ws_prog G\<rbrakk> \<Longrightarrow> |
|
1872 |
dynmethd G statC dynC sig |
|
1873 |
= (if G\<turnstile>dynC \<preceq>\<^sub>C statC |
|
1874 |
then (case methd G statC sig of |
|
1875 |
None \<Rightarrow> None |
|
1876 |
| Some statM |
|
1877 |
\<Rightarrow> (case methd G dynC sig of |
|
1878 |
None \<Rightarrow> dynmethd G statC (super c) sig |
|
1879 |
| Some dynM \<Rightarrow> |
|
1880 |
(if G,sig\<turnstile> dynM overrides statM \<or> dynM = statM |
|
1881 |
then Some dynM |
|
1882 |
else (dynmethd G statC (super c) sig) |
|
1883 |
))) |
|
1884 |
else None)" |
|
1885 |
(is "_ \<Longrightarrow> _ \<Longrightarrow> ?Dynmethd_def dynC sig = ?Dynmethd_rec dynC c sig") |
|
1886 |
proof - |
|
1887 |
assume clsDynC: "class G dynC = Some c" and |
|
1888 |
ws: "ws_prog G" |
|
1889 |
then show "?Dynmethd_def dynC sig = ?Dynmethd_rec dynC c sig" |
|
1890 |
proof (induct rule: ws_class_induct'') |
|
1891 |
case (Object co) |
|
1892 |
show "?Dynmethd_def Object sig = ?Dynmethd_rec Object co sig" |
|
1893 |
proof (cases "G\<turnstile>Object \<preceq>\<^sub>C statC") |
|
1894 |
case False |
|
1895 |
then show ?thesis by (simp add: dynmethd_def) |
|
1896 |
next |
|
1897 |
case True |
|
1898 |
then have eq_statC_Obj: "statC = Object" .. |
|
1899 |
show ?thesis |
|
1900 |
proof (cases "methd G statC sig") |
|
1901 |
case None then show ?thesis by (simp add: dynmethd_def) |
|
1902 |
next |
|
1903 |
case Some |
|
1904 |
with True Object ws eq_statC_Obj |
|
1905 |
show ?thesis |
|
1906 |
by (auto simp add: dynmethd_def class_rec |
|
1907 |
intro: filter_tab_SomeI) |
|
1908 |
qed |
|
1909 |
qed |
|
1910 |
next |
|
1911 |
case (Subcls dynC c sc) |
|
1912 |
show "?Dynmethd_def dynC sig = ?Dynmethd_rec dynC c sig" |
|
1913 |
proof (cases "G\<turnstile>dynC \<preceq>\<^sub>C statC") |
|
1914 |
case False |
|
1915 |
then show ?thesis by (simp add: dynmethd_def) |
|
1916 |
next |
|
1917 |
case True |
|
1918 |
note subclseq_dynC_statC = True |
|
1919 |
show ?thesis |
|
1920 |
proof (cases "methd G statC sig") |
|
1921 |
case None then show ?thesis by (simp add: dynmethd_def) |
|
1922 |
next |
|
1923 |
case (Some statM) |
|
1924 |
note statM = Some |
|
1925 |
let "?filter C" = |
|
1926 |
"filter_tab |
|
1927 |
(\<lambda>_ dynM. G,sig \<turnstile> dynM overrides statM \<or> dynM = statM) |
|
1928 |
(methd G C)" |
|
1929 |
let "?class_rec C" = |
|
1930 |
"(class_rec (G, C) empty |
|
1931 |
(\<lambda>C c subcls_mthds. subcls_mthds ++ (?filter C)))" |
|
1932 |
from statM Subcls ws subclseq_dynC_statC |
|
1933 |
have dynmethd_dynC_def: |
|
1934 |
"?Dynmethd_def dynC sig = |
|
1935 |
((?class_rec (super c)) |
|
1936 |
++ |
|
1937 |
(?filter dynC)) sig" |
|
1938 |
by (simp (no_asm_simp) only: dynmethd_def class_rec) |
|
1939 |
auto |
|
1940 |
show ?thesis |
|
1941 |
proof (cases "dynC = statC") |
|
1942 |
case True |
|
1943 |
with subclseq_dynC_statC statM dynmethd_dynC_def |
|
1944 |
have "?Dynmethd_def dynC sig = Some statM" |
|
1945 |
by (auto intro: override_find_right filter_tab_SomeI) |
|
1946 |
with subclseq_dynC_statC True Some |
|
1947 |
show ?thesis |
|
1948 |
by auto |
|
1949 |
next |
|
1950 |
case False |
|
1951 |
with subclseq_dynC_statC Subcls |
|
1952 |
have subclseq_super_statC: "G\<turnstile>(super c) \<preceq>\<^sub>C statC" |
|
1953 |
by (blast dest: subclseq_superD) |
|
1954 |
show ?thesis |
|
1955 |
proof (cases "methd G dynC sig") |
|
1956 |
case None |
|
1957 |
then have "?filter dynC sig = None" |
|
1958 |
by (rule filter_tab_None) |
|
1959 |
then have "?Dynmethd_def dynC sig=?class_rec (super c) sig" |
|
1960 |
by (simp add: dynmethd_dynC_def) |
|
1961 |
with subclseq_super_statC statM None |
|
1962 |
have "?Dynmethd_def dynC sig = ?Dynmethd_def (super c) sig" |
|
1963 |
by (auto simp add: empty_def dynmethd_def) |
|
1964 |
with None subclseq_dynC_statC statM |
|
1965 |
show ?thesis |
|
1966 |
by simp |
|
1967 |
next |
|
1968 |
case (Some dynM) |
|
1969 |
note dynM = Some |
|
1970 |
let ?Termination = "G \<turnstile> qmdecl sig dynM overrides qmdecl sig statM \<or> |
|
1971 |
dynM = statM" |
|
1972 |
show ?thesis |
|
1973 |
proof (cases "?filter dynC sig") |
|
1974 |
case None |
|
1975 |
with dynM |
|
1976 |
have no_termination: "\<not> ?Termination" |
|
1977 |
by (simp add: filter_tab_def) |
|
1978 |
from None |
|
1979 |
have "?Dynmethd_def dynC sig=?class_rec (super c) sig" |
|
1980 |
by (simp add: dynmethd_dynC_def) |
|
1981 |
with subclseq_super_statC statM dynM no_termination |
|
1982 |
show ?thesis |
|
1983 |
by (auto simp add: empty_def dynmethd_def) |
|
1984 |
next |
|
1985 |
case Some |
|
1986 |
with dynM |
|
1987 |
have termination: "?Termination" |
|
1988 |
by (auto) |
|
1989 |
with Some dynM |
|
1990 |
have "?Dynmethd_def dynC sig=Some dynM" |
|
1991 |
by (auto simp add: dynmethd_dynC_def) |
|
1992 |
with subclseq_super_statC statM dynM termination |
|
1993 |
show ?thesis |
|
1994 |
by (auto simp add: dynmethd_def) |
|
1995 |
qed |
|
1996 |
qed |
|
1997 |
qed |
|
1998 |
qed |
|
1999 |
qed |
|
2000 |
qed |
|
2001 |
qed |
|
2002 |
||
2003 |
lemma dynmethd_C_C:"\<lbrakk>is_class G C; ws_prog G\<rbrakk> |
|
2004 |
\<Longrightarrow> dynmethd G C C sig = methd G C sig" |
|
2005 |
apply (auto simp add: dynmethd_rec) |
|
2006 |
done |
|
2007 |
||
2008 |
lemma dynmethdSomeD: |
|
2009 |
"\<lbrakk>dynmethd G statC dynC sig = Some dynM; is_class G dynC; ws_prog G\<rbrakk> |
|
2010 |
\<Longrightarrow> G\<turnstile>dynC \<preceq>\<^sub>C statC \<and> (\<exists> statM. methd G statC sig = Some statM)" |
|
2011 |
apply clarify |
|
2012 |
apply rotate_tac |
|
2013 |
by (auto simp add: dynmethd_rec) |
|
2014 |
||
2015 |
lemma dynmethd_Some_cases [consumes 3, case_names Static Overrides]: |
|
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
2016 |
assumes dynM: "dynmethd G statC dynC sig = Some dynM" and |
12854 | 2017 |
is_cls_dynC: "is_class G dynC" and |
2018 |
ws: "ws_prog G" and |
|
2019 |
hyp_static: "methd G statC sig = Some dynM \<Longrightarrow> P" and |
|
2020 |
hyp_override: "\<And> statM. \<lbrakk>methd G statC sig = Some statM;dynM\<noteq>statM; |
|
2021 |
G,sig\<turnstile>dynM overrides statM\<rbrakk> \<Longrightarrow> P" |
|
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
2022 |
shows P |
12854 | 2023 |
proof - |
2024 |
from is_cls_dynC obtain dc where clsDynC: "class G dynC = Some dc" by blast |
|
2025 |
from clsDynC ws dynM hyp_static hyp_override |
|
2026 |
show "P" |
|
2027 |
proof (induct rule: ws_class_induct) |
|
2028 |
case (Object co) |
|
2029 |
with ws have "statC = Object" |
|
2030 |
by (auto simp add: dynmethd_rec) |
|
2031 |
with ws Object show ?thesis by (auto simp add: dynmethd_C_C) |
|
2032 |
next |
|
2033 |
case (Subcls C c) |
|
2034 |
with ws show ?thesis |
|
2035 |
by (auto simp add: dynmethd_rec) |
|
2036 |
qed |
|
2037 |
qed |
|
2038 |
||
2039 |
lemma no_override_in_Object: |
|
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
2040 |
assumes dynM: "dynmethd G statC dynC sig = Some dynM" and |
12854 | 2041 |
is_cls_dynC: "is_class G dynC" and |
2042 |
ws: "ws_prog G" and |
|
2043 |
statM: "methd G statC sig = Some statM" and |
|
2044 |
neq_dynM_statM: "dynM\<noteq>statM" |
|
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
2045 |
shows "dynC \<noteq> Object" |
12854 | 2046 |
proof - |
2047 |
from is_cls_dynC obtain dc where clsDynC: "class G dynC = Some dc" by blast |
|
2048 |
from clsDynC ws dynM statM neq_dynM_statM |
|
2049 |
show ?thesis (is "?P dynC") |
|
2050 |
proof (induct rule: ws_class_induct) |
|
2051 |
case (Object co) |
|
2052 |
with ws have "statC = Object" |
|
2053 |
by (auto simp add: dynmethd_rec) |
|
2054 |
with ws Object show "?P Object" by (auto simp add: dynmethd_C_C) |
|
2055 |
next |
|
2056 |
case (Subcls dynC c) |
|
2057 |
with ws show "?P dynC" |
|
2058 |
by (auto simp add: dynmethd_rec) |
|
2059 |
qed |
|
2060 |
qed |
|
2061 |
||
2062 |
||
2063 |
lemma dynmethd_Some_rec_cases [consumes 3, |
|
2064 |
case_names Static Override Recursion]: |
|
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
2065 |
assumes dynM: "dynmethd G statC dynC sig = Some dynM" and |
12854 | 2066 |
clsDynC: "class G dynC = Some c" and |
2067 |
ws: "ws_prog G" and |
|
2068 |
hyp_static: "methd G statC sig = Some dynM \<Longrightarrow> P" and |
|
2069 |
hyp_override: "\<And> statM. \<lbrakk>methd G statC sig = Some statM; |
|
2070 |
methd G dynC sig = Some dynM; statM\<noteq>dynM; |
|
2071 |
G,sig\<turnstile> dynM overrides statM\<rbrakk> \<Longrightarrow> P" and |
|
2072 |
||
2073 |
hyp_recursion: "\<lbrakk>dynC\<noteq>Object; |
|
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
2074 |
dynmethd G statC (super c) sig = Some dynM\<rbrakk> \<Longrightarrow> P" |
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
2075 |
shows P |
12854 | 2076 |
proof - |
2077 |
from clsDynC have "is_class G dynC" by simp |
|
2078 |
note no_override_in_Object' = no_override_in_Object [OF dynM this ws] |
|
2079 |
from ws clsDynC dynM hyp_static hyp_override hyp_recursion |
|
2080 |
show ?thesis |
|
2081 |
by (auto simp add: dynmethd_rec dest: no_override_in_Object') |
|
2082 |
qed |
|
2083 |
||
2084 |
lemma dynmethd_declC: |
|
2085 |
"\<lbrakk>dynmethd G statC dynC sig = Some m; |
|
2086 |
is_class G statC;ws_prog G |
|
2087 |
\<rbrakk> \<Longrightarrow> |
|
2088 |
(\<exists>d. class G (declclass m)=Some d \<and> table_of (methods d) sig=Some (mthd m)) \<and> |
|
2089 |
G\<turnstile>dynC \<preceq>\<^sub>C (declclass m) \<and> methd G (declclass m) sig = Some m" |
|
2090 |
proof - |
|
2091 |
assume is_cls_statC: "is_class G statC" |
|
2092 |
assume ws: "ws_prog G" |
|
2093 |
assume m: "dynmethd G statC dynC sig = Some m" |
|
2094 |
from m |
|
2095 |
have "G\<turnstile>dynC \<preceq>\<^sub>C statC" by (auto simp add: dynmethd_def) |
|
2096 |
from this is_cls_statC |
|
2097 |
have is_cls_dynC: "is_class G dynC" by (rule subcls_is_class2) |
|
2098 |
from is_cls_dynC ws m |
|
2099 |
show ?thesis (is "?P dynC") |
|
2100 |
proof (induct rule: ws_class_induct') |
|
2101 |
case (Object co) |
|
2102 |
with ws have "statC=Object" by (auto simp add: dynmethd_rec) |
|
2103 |
with ws Object |
|
2104 |
show "?P Object" |
|
2105 |
by (auto simp add: dynmethd_C_C dest: methd_declC) |
|
2106 |
next |
|
2107 |
case (Subcls dynC c) |
|
2108 |
assume hyp: "dynmethd G statC (super c) sig = Some m \<Longrightarrow> ?P (super c)" and |
|
2109 |
clsDynC: "class G dynC = Some c" and |
|
2110 |
m': "dynmethd G statC dynC sig = Some m" and |
|
2111 |
neq_dynC_Obj: "dynC \<noteq> Object" |
|
2112 |
from ws this obtain statM where |
|
2113 |
subclseq_dynC_statC: "G\<turnstile>dynC \<preceq>\<^sub>C statC" and |
|
2114 |
statM: "methd G statC sig = Some statM" |
|
2115 |
by (blast dest: dynmethdSomeD) |
|
2116 |
from clsDynC neq_dynC_Obj |
|
2117 |
have subclseq_dynC_super: "G\<turnstile>dynC \<preceq>\<^sub>C (super c)" |
|
2118 |
by (auto intro: subcls1I) |
|
2119 |
from m' clsDynC ws |
|
2120 |
show "?P dynC" |
|
2121 |
proof (cases rule: dynmethd_Some_rec_cases) |
|
2122 |
case Static |
|
2123 |
with is_cls_statC ws subclseq_dynC_statC |
|
2124 |
show ?thesis |
|
2125 |
by (auto intro: rtrancl_trans dest: methd_declC) |
|
2126 |
next |
|
2127 |
case Override |
|
2128 |
with clsDynC ws |
|
2129 |
show ?thesis |
|
2130 |
by (auto dest: methd_declC) |
|
2131 |
next |
|
2132 |
case Recursion |
|
2133 |
with hyp subclseq_dynC_super |
|
2134 |
show ?thesis |
|
2135 |
by (auto intro: rtrancl_trans) |
|
2136 |
qed |
|
2137 |
qed |
|
2138 |
qed |
|
2139 |
||
2140 |
lemma methd_Some_dynmethd_Some: |
|
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
2141 |
assumes statM: "methd G statC sig = Some statM" and |
12854 | 2142 |
subclseq: "G\<turnstile>dynC \<preceq>\<^sub>C statC" and |
2143 |
is_cls_statC: "is_class G statC" and |
|
2144 |
ws: "ws_prog G" |
|
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
2145 |
shows "\<exists> dynM. dynmethd G statC dynC sig = Some dynM" |
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
2146 |
(is "?P dynC") |
12854 | 2147 |
proof - |
2148 |
from subclseq is_cls_statC |
|
2149 |
have is_cls_dynC: "is_class G dynC" by (rule subcls_is_class2) |
|
2150 |
then obtain dc where |
|
2151 |
clsDynC: "class G dynC = Some dc" by blast |
|
2152 |
from clsDynC ws subclseq |
|
2153 |
show "?thesis" |
|
2154 |
proof (induct rule: ws_class_induct) |
|
2155 |
case (Object co) |
|
2156 |
with ws have "statC = Object" |
|
2157 |
by (auto) |
|
2158 |
with ws Object statM |
|
2159 |
show "?P Object" |
|
2160 |
by (auto simp add: dynmethd_C_C) |
|
2161 |
next |
|
2162 |
case (Subcls dynC dc) |
|
2163 |
assume clsDynC': "class G dynC = Some dc" |
|
2164 |
assume neq_dynC_Obj: "dynC \<noteq> Object" |
|
2165 |
assume hyp: "G\<turnstile>super dc\<preceq>\<^sub>C statC \<Longrightarrow> ?P (super dc)" |
|
2166 |
assume subclseq': "G\<turnstile>dynC\<preceq>\<^sub>C statC" |
|
2167 |
then |
|
2168 |
show "?P dynC" |
|
2169 |
proof (cases rule: subclseq_cases) |
|
2170 |
case Eq |
|
2171 |
with ws statM clsDynC' |
|
2172 |
show ?thesis |
|
2173 |
by (auto simp add: dynmethd_rec) |
|
2174 |
next |
|
2175 |
case Subcls |
|
2176 |
assume "G\<turnstile>dynC\<prec>\<^sub>C statC" |
|
2177 |
from this clsDynC' |
|
2178 |
have "G\<turnstile>super dc\<preceq>\<^sub>C statC" by (rule subcls_superD) |
|
2179 |
with hyp ws clsDynC' subclseq' statM |
|
2180 |
show ?thesis |
|
2181 |
by (auto simp add: dynmethd_rec) |
|
2182 |
qed |
|
2183 |
qed |
|
2184 |
qed |
|
2185 |
||
2186 |
lemma dynmethd_cases [consumes 4, case_names Static Overrides]: |
|
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
2187 |
assumes statM: "methd G statC sig = Some statM" and |
12854 | 2188 |
subclseq: "G\<turnstile>dynC \<preceq>\<^sub>C statC" and |
2189 |
is_cls_statC: "is_class G statC" and |
|
2190 |
ws: "ws_prog G" and |
|
2191 |
hyp_static: "dynmethd G statC dynC sig = Some statM \<Longrightarrow> P" and |
|
2192 |
hyp_override: "\<And> dynM. \<lbrakk>dynmethd G statC dynC sig = Some dynM; |
|
2193 |
dynM\<noteq>statM; |
|
2194 |
G,sig\<turnstile>dynM overrides statM\<rbrakk> \<Longrightarrow> P" |
|
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
2195 |
shows P |
12854 | 2196 |
proof - |
2197 |
from subclseq is_cls_statC |
|
2198 |
have is_cls_dynC: "is_class G dynC" by (rule subcls_is_class2) |
|
2199 |
then obtain dc where |
|
2200 |
clsDynC: "class G dynC = Some dc" by blast |
|
2201 |
from statM subclseq is_cls_statC ws |
|
2202 |
obtain dynM |
|
2203 |
where dynM: "dynmethd G statC dynC sig = Some dynM" |
|
2204 |
by (blast dest: methd_Some_dynmethd_Some) |
|
2205 |
from dynM is_cls_dynC ws |
|
2206 |
show ?thesis |
|
2207 |
proof (cases rule: dynmethd_Some_cases) |
|
2208 |
case Static |
|
2209 |
with hyp_static dynM statM show ?thesis by simp |
|
2210 |
next |
|
2211 |
case Overrides |
|
2212 |
with hyp_override dynM statM show ?thesis by simp |
|
2213 |
qed |
|
2214 |
qed |
|
2215 |
||
2216 |
lemma ws_dynmethd: |
|
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
2217 |
assumes statM: "methd G statC sig = Some statM" and |
12854 | 2218 |
subclseq: "G\<turnstile>dynC \<preceq>\<^sub>C statC" and |
2219 |
is_cls_statC: "is_class G statC" and |
|
2220 |
ws: "ws_prog G" |
|
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
2221 |
shows |
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
2222 |
"\<exists> dynM. dynmethd G statC dynC sig = Some dynM \<and> |
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
2223 |
is_static dynM = is_static statM \<and> G\<turnstile>resTy dynM\<preceq>resTy statM" |
12854 | 2224 |
proof - |
2225 |
from statM subclseq is_cls_statC ws |
|
2226 |
show ?thesis |
|
2227 |
proof (cases rule: dynmethd_cases) |
|
2228 |
case Static |
|
2229 |
with statM |
|
2230 |
show ?thesis |
|
2231 |
by simp |
|
2232 |
next |
|
2233 |
case Overrides |
|
2234 |
with ws |
|
2235 |
show ?thesis |
|
2236 |
by (auto dest: ws_overrides_commonD) |
|
2237 |
qed |
|
2238 |
qed |
|
2239 |
||
2240 |
(* |
|
2241 |
lemma dom_dynmethd: |
|
2242 |
"dom (dynmethd G statC dynC) \<subseteq> dom (methd G statC) \<union> dom (methd G dynC)" |
|
2243 |
by (auto simp add: dynmethd_def dom_def) |
|
2244 |
||
2245 |
lemma finite_dom_dynmethd: |
|
2246 |
"\<lbrakk>ws_prog G; is_class G statC; is_class G dynC\<rbrakk> |
|
2247 |
\<Longrightarrow> finite (dom (dynmethd G statC dynC))" |
|
2248 |
apply (rule_tac B="dom (methd G statC) \<union> dom (methd G dynC)" in finite_subset) |
|
2249 |
apply (rule dom_dynmethd) |
|
2250 |
apply (rule finite_UnI) |
|
2251 |
apply (drule (2) finite_dom_methd)+ |
|
2252 |
done |
|
2253 |
*) |
|
2254 |
(* |
|
2255 |
lemma dynmethd_SomeD: |
|
2256 |
"\<lbrakk>ws_prog G; is_class G statC; is_class G dynC; |
|
2257 |
methd G statC sig = Some sm; dynmethd G statC dynC sig = Some dm; sm \<noteq> dm |
|
2258 |
\<rbrakk> \<Longrightarrow> G\<turnstile>dynC \<prec>\<^sub>C statC \<and> |
|
2259 |
(declclass dm \<noteq> dynC \<longrightarrow> G \<turnstile> dm accessible_through_inheritance_in dynC)" |
|
2260 |
by (auto simp add: dynmethd_def |
|
2261 |
dest: methd_inheritedD methd_diff_cls |
|
2262 |
intro: rtrancl_into_trancl3) |
|
2263 |
*) |
|
2264 |
||
2265 |
subsection "dynlookup" |
|
2266 |
||
2267 |
lemma dynlookup_cases [consumes 1, case_names NullT IfaceT ClassT ArrayT]: |
|
2268 |
"\<lbrakk>dynlookup G statT dynC sig = x; |
|
2269 |
\<lbrakk>statT = NullT ; empty sig = x \<rbrakk> \<Longrightarrow> P; |
|
2270 |
\<And> I. \<lbrakk>statT = IfaceT I ; dynimethd G I dynC sig = x\<rbrakk> \<Longrightarrow> P; |
|
2271 |
\<And> statC.\<lbrakk>statT = ClassT statC; dynmethd G statC dynC sig = x\<rbrakk> \<Longrightarrow> P; |
|
2272 |
\<And> ty. \<lbrakk>statT = ArrayT ty ; dynmethd G Object dynC sig = x\<rbrakk> \<Longrightarrow> P |
|
2273 |
\<rbrakk> \<Longrightarrow> P" |
|
2274 |
by (cases statT) (auto simp add: dynlookup_def) |
|
2275 |
||
2276 |
subsection "fields" |
|
2277 |
||
2278 |
lemma fields_rec: "\<lbrakk>class G C = Some c; ws_prog G\<rbrakk> \<Longrightarrow> |
|
2279 |
fields G C = map (\<lambda>(fn,ft). ((fn,C),ft)) (cfields c) @ |
|
2280 |
(if C = Object then [] else fields G (super c))" |
|
2281 |
apply (simp only: fields_def) |
|
2282 |
apply (erule class_rec [THEN trans]) |
|
2283 |
apply assumption |
|
2284 |
apply clarsimp |
|
2285 |
done |
|
2286 |
||
2287 |
(* local lemma *) |
|
2288 |
lemma fields_norec: |
|
2289 |
"\<lbrakk>class G fd = Some c; ws_prog G; table_of (cfields c) fn = Some f\<rbrakk> |
|
2290 |
\<Longrightarrow> table_of (fields G fd) (fn,fd) = Some f" |
|
2291 |
apply (subst fields_rec) |
|
2292 |
apply assumption+ |
|
2293 |
apply (subst map_of_override [symmetric]) |
|
2294 |
apply (rule disjI1 [THEN override_Some_iff [THEN iffD2]]) |
|
2295 |
apply (auto elim: table_of_map2_SomeI) |
|
2296 |
done |
|
2297 |
||
2298 |
(* local lemma *) |
|
2299 |
lemma table_of_fieldsD: |
|
2300 |
"table_of (map (\<lambda>(fn,ft). ((fn,C),ft)) (cfields c)) efn = Some f |
|
2301 |
\<Longrightarrow> (declclassf efn) = C \<and> table_of (cfields c) (fname efn) = Some f" |
|
2302 |
apply (case_tac "efn") |
|
2303 |
by auto |
|
2304 |
||
2305 |
lemma fields_declC: |
|
2306 |
"\<lbrakk>table_of (fields G C) efn = Some f; ws_prog G; is_class G C\<rbrakk> \<Longrightarrow> |
|
2307 |
(\<exists>d. class G (declclassf efn) = Some d \<and> |
|
2308 |
table_of (cfields d) (fname efn)=Some f) \<and> |
|
2309 |
G\<turnstile>C \<preceq>\<^sub>C (declclassf efn) \<and> table_of (fields G (declclassf efn)) efn = Some f" |
|
2310 |
apply (erule make_imp) |
|
2311 |
apply (rule ws_subcls1_induct, assumption, assumption) |
|
2312 |
apply (subst fields_rec, assumption) |
|
2313 |
apply clarify |
|
2314 |
apply (simp only: map_of_override [symmetric] del: map_of_override) |
|
2315 |
apply (case_tac "table_of (map (split (\<lambda>fn. Pair (fn, Ca))) (cfields c)) efn") |
|
2316 |
apply (force intro:rtrancl_into_rtrancl2 simp add: override_def) |
|
2317 |
||
2318 |
apply (frule_tac fd="Ca" in fields_norec) |
|
2319 |
apply assumption |
|
2320 |
apply blast |
|
2321 |
apply (frule table_of_fieldsD) |
|
2322 |
apply (frule_tac n="table_of (map (split (\<lambda>fn. Pair (fn, Ca))) (cfields c))" |
|
2323 |
and m="table_of (if Ca = Object then [] else fields G (super c))" |
|
2324 |
in override_find_right) |
|
2325 |
apply (case_tac "efn") |
|
2326 |
apply (simp) |
|
2327 |
done |
|
2328 |
||
2329 |
lemma fields_emptyI: "\<And>y. \<lbrakk>ws_prog G; class G C = Some c;cfields c = []; |
|
2330 |
C \<noteq> Object \<longrightarrow> class G (super c) = Some y \<and> fields G (super c) = []\<rbrakk> \<Longrightarrow> |
|
2331 |
fields G C = []" |
|
2332 |
apply (subst fields_rec) |
|
2333 |
apply assumption |
|
2334 |
apply auto |
|
2335 |
done |
|
2336 |
||
2337 |
(* easier than with table_of *) |
|
2338 |
lemma fields_mono_lemma: |
|
2339 |
"\<lbrakk>x \<in> set (fields G C); G\<turnstile>D \<preceq>\<^sub>C C; ws_prog G\<rbrakk> |
|
2340 |
\<Longrightarrow> x \<in> set (fields G D)" |
|
2341 |
apply (erule make_imp) |
|
2342 |
apply (erule converse_rtrancl_induct) |
|
2343 |
apply fast |
|
2344 |
apply (drule subcls1D) |
|
2345 |
apply clarsimp |
|
2346 |
apply (subst fields_rec) |
|
2347 |
apply auto |
|
2348 |
done |
|
2349 |
||
2350 |
||
2351 |
lemma ws_unique_fields_lemma: |
|
2352 |
"\<lbrakk>(efn,fd) \<in> set (fields G (super c)); fc \<in> set (cfields c); ws_prog G; |
|
2353 |
fname efn = fname fc; declclassf efn = C; |
|
2354 |
class G C = Some c; C \<noteq> Object; class G (super c) = Some d\<rbrakk> \<Longrightarrow> R" |
|
2355 |
apply (frule_tac ws_prog_cdeclD [THEN conjunct2], assumption, assumption) |
|
2356 |
apply (drule_tac weak_map_of_SomeI) |
|
2357 |
apply (frule_tac subcls1I [THEN subcls1_irrefl], assumption, assumption) |
|
2358 |
apply (auto dest: fields_declC [THEN conjunct2 [THEN conjunct1[THEN rtranclD]]]) |
|
2359 |
done |
|
2360 |
||
2361 |
lemma ws_unique_fields: "\<lbrakk>is_class G C; ws_prog G; |
|
2362 |
\<And>C c. \<lbrakk>class G C = Some c\<rbrakk> \<Longrightarrow> unique (cfields c) \<rbrakk> \<Longrightarrow> |
|
2363 |
unique (fields G C)" |
|
2364 |
apply (rule ws_subcls1_induct, assumption, assumption) |
|
2365 |
apply (subst fields_rec, assumption) |
|
2366 |
apply (auto intro!: unique_map_inj injI |
|
2367 |
elim!: unique_append ws_unique_fields_lemma fields_norec |
|
2368 |
) |
|
2369 |
done |
|
2370 |
||
2371 |
||
2372 |
subsection "accfield" |
|
2373 |
||
2374 |
lemma accfield_fields: |
|
2375 |
"accfield G S C fn = Some f |
|
2376 |
\<Longrightarrow> table_of (fields G C) (fn, declclass f) = Some (fld f)" |
|
2377 |
apply (simp only: accfield_def Let_def) |
|
2378 |
apply (rule table_of_remap_SomeD) |
|
2379 |
apply (auto dest: filter_tab_SomeD) |
|
2380 |
done |
|
2381 |
||
2382 |
||
2383 |
lemma accfield_declC_is_class: |
|
2384 |
"\<lbrakk>is_class G C; accfield G S C en = Some (fd, f); ws_prog G\<rbrakk> \<Longrightarrow> |
|
2385 |
is_class G fd" |
|
2386 |
apply (drule accfield_fields) |
|
2387 |
apply (drule fields_declC [THEN conjunct1], assumption) |
|
2388 |
apply auto |
|
2389 |
done |
|
2390 |
||
2391 |
lemma accfield_accessibleD: |
|
2392 |
"accfield G S C fn = Some f \<Longrightarrow> G\<turnstile>Field fn f of C accessible_from S" |
|
2393 |
by (auto simp add: accfield_def Let_def) |
|
2394 |
||
2395 |
subsection "is methd" |
|
2396 |
||
2397 |
lemma is_methdI: |
|
2398 |
"\<lbrakk>class G C = Some y; methd G C sig = Some b\<rbrakk> \<Longrightarrow> is_methd G C sig" |
|
2399 |
apply (unfold is_methd_def) |
|
2400 |
apply auto |
|
2401 |
done |
|
2402 |
||
2403 |
lemma is_methdD: |
|
2404 |
"is_methd G C sig \<Longrightarrow> class G C \<noteq> None \<and> methd G C sig \<noteq> None" |
|
2405 |
apply (unfold is_methd_def) |
|
2406 |
apply auto |
|
2407 |
done |
|
2408 |
||
2409 |
lemma finite_is_methd: |
|
2410 |
"ws_prog G \<Longrightarrow> finite (Collect (split (is_methd G)))" |
|
2411 |
apply (unfold is_methd_def) |
|
2412 |
apply (subst SetCompr_Sigma_eq) |
|
2413 |
apply (rule finite_is_class [THEN finite_SigmaI]) |
|
2414 |
apply (simp only: mem_Collect_eq) |
|
2415 |
apply (fold dom_def) |
|
2416 |
apply (erule finite_dom_methd) |
|
2417 |
apply assumption |
|
2418 |
done |
|
2419 |
||
2420 |
section "calculation of the superclasses of a class" |
|
2421 |
||
2422 |
constdefs |
|
2423 |
superclasses:: "prog \<Rightarrow> qtname \<Rightarrow> qtname set" |
|
2424 |
"superclasses G C \<equiv> class_rec (G,C) {} |
|
2425 |
(\<lambda> C c superclss. (if C=Object |
|
2426 |
then {} |
|
2427 |
else insert (super c) superclss))" |
|
2428 |
||
2429 |
lemma superclasses_rec: "\<lbrakk>class G C = Some c; ws_prog G\<rbrakk> \<Longrightarrow> |
|
2430 |
superclasses G C |
|
2431 |
= (if (C=Object) |
|
2432 |
then {} |
|
2433 |
else insert (super c) (superclasses G (super c)))" |
|
2434 |
apply (unfold superclasses_def) |
|
2435 |
apply (erule class_rec [THEN trans], assumption) |
|
2436 |
apply (simp) |
|
2437 |
done |
|
2438 |
||
2439 |
lemma superclasses_mono: |
|
2440 |
"\<lbrakk>G\<turnstile>C \<prec>\<^sub>C D;ws_prog G; class G C = Some c; |
|
2441 |
\<And> C c. \<lbrakk>class G C = Some c;C\<noteq>Object\<rbrakk> \<Longrightarrow> \<exists> sc. class G (super c) = Some sc; |
|
2442 |
x\<in>superclasses G D |
|
2443 |
\<rbrakk> \<Longrightarrow> x\<in>superclasses G C" |
|
2444 |
proof - |
|
2445 |
||
2446 |
assume ws: "ws_prog G" and |
|
2447 |
cls_C: "class G C = Some c" and |
|
2448 |
wf: "\<And>C c. \<lbrakk>class G C = Some c; C \<noteq> Object\<rbrakk> |
|
2449 |
\<Longrightarrow> \<exists>sc. class G (super c) = Some sc" |
|
2450 |
assume clsrel: "G\<turnstile>C\<prec>\<^sub>C D" |
|
2451 |
thus "\<And> c. \<lbrakk>class G C = Some c; x\<in>superclasses G D\<rbrakk>\<Longrightarrow> |
|
2452 |
x\<in>superclasses G C" (is "PROP ?P C" |
|
2453 |
is "\<And> c. ?CLS C c \<Longrightarrow> ?SUP D \<Longrightarrow> ?SUP C") |
|
2454 |
proof (induct ?P C rule: converse_trancl_induct) |
|
2455 |
fix C c |
|
2456 |
assume "G\<turnstile>C\<prec>\<^sub>C\<^sub>1D" "class G C = Some c" "x \<in> superclasses G D" |
|
2457 |
with wf ws show "?SUP C" |
|
2458 |
by (auto intro: no_subcls1_Object |
|
2459 |
simp add: superclasses_rec subcls1_def) |
|
2460 |
next |
|
2461 |
fix C S c |
|
2462 |
assume clsrel': "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 S" "G\<turnstile>S \<prec>\<^sub>C D" |
|
2463 |
and hyp : "\<And> s. \<lbrakk>class G S = Some s; x \<in> superclasses G D\<rbrakk> |
|
2464 |
\<Longrightarrow> x \<in> superclasses G S" |
|
2465 |
and cls_C': "class G C = Some c" |
|
2466 |
and x: "x \<in> superclasses G D" |
|
2467 |
moreover note wf ws |
|
2468 |
moreover from calculation |
|
2469 |
have "?SUP S" |
|
2470 |
by (force intro: no_subcls1_Object simp add: subcls1_def) |
|
2471 |
moreover from calculation |
|
2472 |
have "super c = S" |
|
2473 |
by (auto intro: no_subcls1_Object simp add: subcls1_def) |
|
2474 |
ultimately show "?SUP C" |
|
2475 |
by (auto intro: no_subcls1_Object simp add: superclasses_rec) |
|
2476 |
qed |
|
2477 |
qed |
|
2478 |
||
2479 |
lemma subclsEval: |
|
2480 |
"\<lbrakk>G\<turnstile>C \<prec>\<^sub>C D;ws_prog G; class G C = Some c; |
|
2481 |
\<And> C c. \<lbrakk>class G C = Some c;C\<noteq>Object\<rbrakk> \<Longrightarrow> \<exists> sc. class G (super c) = Some sc |
|
2482 |
\<rbrakk> \<Longrightarrow> D\<in>superclasses G C" |
|
2483 |
proof - |
|
2484 |
note converse_trancl_induct |
|
2485 |
= converse_trancl_induct [consumes 1,case_names Single Step] |
|
2486 |
assume |
|
2487 |
ws: "ws_prog G" and |
|
2488 |
cls_C: "class G C = Some c" and |
|
2489 |
wf: "\<And>C c. \<lbrakk>class G C = Some c; C \<noteq> Object\<rbrakk> |
|
2490 |
\<Longrightarrow> \<exists>sc. class G (super c) = Some sc" |
|
2491 |
assume clsrel: "G\<turnstile>C\<prec>\<^sub>C D" |
|
2492 |
thus "\<And> c. class G C = Some c\<Longrightarrow> D\<in>superclasses G C" |
|
2493 |
(is "PROP ?P C" is "\<And> c. ?CLS C c \<Longrightarrow> ?SUP C") |
|
2494 |
proof (induct ?P C rule: converse_trancl_induct) |
|
2495 |
fix C c |
|
2496 |
assume "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 D" "class G C = Some c" |
|
2497 |
with ws wf show "?SUP C" |
|
2498 |
by (auto intro: no_subcls1_Object simp add: superclasses_rec subcls1_def) |
|
2499 |
next |
|
2500 |
fix C S c |
|
2501 |
assume "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 S" "G\<turnstile>S\<prec>\<^sub>C D" |
|
2502 |
"\<And>s. class G S = Some s \<Longrightarrow> D \<in> superclasses G S" |
|
2503 |
"class G C = Some c" |
|
2504 |
with ws wf show "?SUP C" |
|
2505 |
by - (rule superclasses_mono, |
|
2506 |
auto dest: no_subcls1_Object simp add: subcls1_def ) |
|
2507 |
qed |
|
2508 |
qed |
|
2509 |
||
2510 |
end |