12854

1 
header {* Advanced concepts on Java declarations like overriding, inheritance,


2 
dynamic method lookup*}


3 


4 
theory DeclConcepts = TypeRel:


5 


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


7 


8 
constdefs


9 
is_public :: "prog \<Rightarrow> qtname \<Rightarrow> bool"


10 
"is_public G qn \<equiv> (case class G qn of


11 
None \<Rightarrow> (case iface G qn of


12 
None \<Rightarrow> False


13 
 Some iface \<Rightarrow> access iface = Public)


14 
 Some class \<Rightarrow> access class = Public)"


15 


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


17 
text {*


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


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


20 
its element type is accessible *}


21 


22 
consts accessible_in :: "prog \<Rightarrow> ty \<Rightarrow> pname \<Rightarrow> bool"


23 
("_ \<turnstile> _ accessible'_in _" [61,61,61] 60)


24 
rt_accessible_in:: "prog \<Rightarrow> ref_ty \<Rightarrow> pname \<Rightarrow> bool"


25 
("_ \<turnstile> _ accessible'_in' _" [61,61,61] 60)


26 
primrec


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


28 
accessible_in_RefT_simp:


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


30 


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


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


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


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


35 


36 
declare accessible_in_RefT_simp [simp del]


37 


38 
constdefs


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


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


41 
is_acc_iface :: "prog \<Rightarrow> pname \<Rightarrow> qtname \<Rightarrow> bool"


42 
"is_acc_iface G P I \<equiv> is_iface G I \<and> G\<turnstile>(Iface I) accessible_in P"


43 
is_acc_type :: "prog \<Rightarrow> pname \<Rightarrow> ty \<Rightarrow> bool"


44 
"is_acc_type G P T \<equiv> is_type G T \<and> G\<turnstile>T accessible_in P"


45 
is_acc_reftype :: "prog \<Rightarrow> pname \<Rightarrow> ref_ty \<Rightarrow> bool"


46 
"is_acc_reftype G P T \<equiv> isrtype G T \<and> G\<turnstile>T accessible_in' P"


47 


48 
lemma is_acc_classD:


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


50 
by (simp add: is_acc_class_def)


51 


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


53 
by (auto simp add: is_acc_class_def)


54 


55 
lemma is_acc_ifaceD:


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


57 
by (simp add: is_acc_iface_def)


58 


59 
lemma is_acc_typeD:


60 
"is_acc_type G P T \<equiv> is_type G T \<and> G\<turnstile>T accessible_in P"


61 
by (simp add: is_acc_type_def)


62 


63 
lemma is_acc_reftypeD:


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


65 
by (simp add: is_acc_reftype_def)


66 


67 
subsection "accessibility of members"


68 
text {*


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


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


71 
accessibility during inheritance, overriding and ordinary member access


72 
*}


73 


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


75 


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


77 
out of various HOL types *}


78 


79 
axclass has_accmodi < "type"


80 
consts accmodi:: "'a::has_accmodi \<Rightarrow> acc_modi"


81 


82 
instance acc_modi::has_accmodi


83 
by (intro_classes)


84 


85 
defs (overloaded)


86 
acc_modi_accmodi_def: "accmodi (a::acc_modi) \<equiv> a"


87 


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


89 
by (simp add: acc_modi_accmodi_def)


90 


91 
instance access_field_type:: ("type","type") has_accmodi


92 
by (intro_classes)


93 


94 
defs (overloaded)


95 
decl_acc_modi_def: "accmodi (d::('a:: type) decl_scheme) \<equiv> access d"


96 


97 


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


99 
by (simp add: decl_acc_modi_def)


100 


101 
instance * :: ("type",has_accmodi) has_accmodi


102 
by (intro_classes)


103 


104 
defs (overloaded)


105 
pair_acc_modi_def: "accmodi p \<equiv> (accmodi (snd p))"


106 


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


108 
by (simp add: pair_acc_modi_def)


109 


110 
instance memberdecl :: has_accmodi


111 
by (intro_classes)


112 


113 
defs (overloaded)


114 
memberdecl_acc_modi_def: "accmodi m \<equiv> (case m of


115 
fdecl f \<Rightarrow> accmodi f


116 
 mdecl m \<Rightarrow> accmodi m)"


117 


118 
lemma memberdecl_fdecl_acc_modi_simp[simp]:


119 
"accmodi (fdecl m) = accmodi m"


120 
by (simp add: memberdecl_acc_modi_def)


121 


122 
lemma memberdecl_mdecl_acc_modi_simp[simp]:


123 
"accmodi (mdecl m) = accmodi m"


124 
by (simp add: memberdecl_acc_modi_def)


125 


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


127 
out of various HOL types *}


128 


129 
axclass has_declclass < "type"


130 
consts declclass:: "'a::has_declclass \<Rightarrow> qtname"


131 


132 
instance pid_field_type::("type","type") has_declclass


133 
by (intro_classes)


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 


141 
instance * :: ("has_declclass","type") has_declclass


142 
by (intro_classes)


143 


144 
defs (overloaded)


145 
pair_declclass_def: "declclass p \<equiv> declclass (fst p)"


146 


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


148 
by (simp add: pair_declclass_def)


149 


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


151 
out of various HOL types *}


152 


153 


154 
axclass has_static < "type"


155 
consts is_static :: "'a::has_static \<Rightarrow> bool"


156 


157 
(*


158 
consts is_static :: "'a \<Rightarrow> bool"


159 
*)


160 


161 
instance access_field_type :: ("type","has_static") has_static


162 
by (intro_classes)


163 


164 
defs (overloaded)


165 
decl_is_static_def:


166 
"is_static (m::('a::has_static) decl_scheme) \<equiv> is_static (Decl.decl.more m)"


167 


168 
instance static_field_type :: ("type","type") has_static


169 
by (intro_classes)


170 


171 
defs (overloaded)


172 
static_field_type_is_static_def:


173 
"is_static (m::(bool,'b::type) static_field_type) \<equiv> static_val m"


174 


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


176 
apply (cases m)


177 
apply (simp add: static_field_type_is_static_def


178 
decl_is_static_def Decl.member.dest_convs)


179 
done


180 


181 
instance * :: ("type","has_static") has_static


182 
by (intro_classes)


183 


184 
defs (overloaded)


185 
pair_is_static_def: "is_static p \<equiv> is_static (snd p)"


186 


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


188 
by (simp add: pair_is_static_def)


189 


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


191 
by (simp add: pair_is_static_def)


192 


193 
instance memberdecl:: has_static


194 
by (intro_classes)


195 


196 
defs (overloaded)


197 
memberdecl_is_static_def:


198 
"is_static m \<equiv> (case m of


199 
fdecl f \<Rightarrow> is_static f


200 
 mdecl m \<Rightarrow> is_static m)"


201 


202 
lemma memberdecl_is_static_fdecl_simp[simp]:


203 
"is_static (fdecl f) = is_static f"


204 
by (simp add: memberdecl_is_static_def)


205 


206 
lemma memberdecl_is_static_mdecl_simp[simp]:


207 
"is_static (mdecl m) = is_static m"


208 
by (simp add: memberdecl_is_static_def)


209 


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


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


212 


213 
constdefs (* some mnemotic selectors for (qtname \<times> ('a::more) decl_scheme)


214 
* the first component is a class or interface name


215 
* the second component is a method, field or method head *)


216 
(* "declclass":: "(qtname \<times> ('a::more) decl_scheme) \<Rightarrow> qtname"*)


217 
(* "declclass \<equiv> fst" *) (* get the class component *)


218 


219 
"decliface":: "(qtname \<times> ('a::type) decl_scheme) \<Rightarrow> qtname"


220 
"decliface \<equiv> fst" (* get the interface component *)


221 


222 
(*


223 
"member":: "(qtname \<times> ('a::type) decl_scheme) \<Rightarrow> ('a::type) decl_scheme"


224 
*)


225 
"mbr":: "(qtname \<times> memberdecl) \<Rightarrow> memberdecl"


226 
"mbr \<equiv> snd" (* get the memberdecl component *)


227 


228 
"mthd":: "('b \<times> 'a) \<Rightarrow> 'a"


229 
(* also used for mdecl,mhead *)


230 
"mthd \<equiv> snd" (* get the method component *)


231 


232 
"fld":: "('b \<times> ('a::type) decl_scheme) \<Rightarrow> ('a::type) decl_scheme"


233 
(* also used for ((vname \<times> qtname)\<times> field) *)


234 
"fld \<equiv> snd" (* get the field component *)


235 


236 
(* "accmodi" :: "('b \<times> ('a::type) decl_scheme) \<Rightarrow> acc_modi"*)


237 
(* also used for mdecl *)


238 
(* "accmodi \<equiv> access \<circ> snd"*) (* get the access modifier *)


239 
(*


240 
"is_static" ::"('b \<times> ('a::type) member_scheme) \<Rightarrow> bool" *)


241 
(* also defined for emhead cf. WellType *)


242 
(*"is_static \<equiv> static \<circ> snd"*) (* get the static modifier *)


243 


244 
constdefs (* some mnemotic selectors for (vname \<times> qtname) *)


245 
fname:: "(vname \<times> 'a) \<Rightarrow> vname" (* also used for fdecl *)


246 
"fname \<equiv> fst"


247 


248 
declclassf:: "(vname \<times> qtname) \<Rightarrow> qtname"


249 
"declclassf \<equiv> snd"


250 


251 
(*


252 
lemma declclass_simp[simp]: "declclass (C,m) = C"


253 
by (simp add: declclass_def)


254 
*)


255 


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


257 
by (simp add: decliface_def)


258 


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


260 
by (simp add: mbr_def)


261 


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


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


264 


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


266 
by (simp add: mthd_def)


267 


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


269 
by (simp add: fld_def)


270 


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


272 
by (simp )


273 


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


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


276 


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


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


279 


280 
(*


281 
lemma is_static_simp[simp]: "is_static (C,m) = static m"


282 
by (simp add: is_static_def)


283 
*)


284 


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


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


287 


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


289 
by (cases m) simp


290 


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


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


293 


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


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


296 


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


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


299 


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


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


302 


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


304 
by (simp add: fname_def)


305 


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


307 
by (simp add: declclassf_def)


308 


309 
constdefs (* some mnemotic selectors for (vname \<times> qtname) *)


310 
"fldname" :: "(vname \<times> qtname) \<Rightarrow> vname"


311 
"fldname \<equiv> fst"


312 


313 
"fldclass" :: "(vname \<times> qtname) \<Rightarrow> qtname"


314 
"fldclass \<equiv> snd"


315 


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


317 
by (simp add: fldname_def)


318 


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


320 
by (simp add: fldclass_def)


321 


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


323 
by (simp add: fldname_def fldclass_def)


324 


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


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


327 


328 
constdefs


329 
methdMembr :: "(qtname \<times> mdecl) \<Rightarrow> (qtname \<times> memberdecl)"


330 
"methdMembr m \<equiv> (fst m,mdecl (snd m))"


331 


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


333 
by (simp add: methdMembr_def)


334 


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


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


337 


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


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


340 


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


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


343 


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


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


346 


347 
constdefs


348 
method :: "sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> memberdecl)"


349 
"method sig m \<equiv> (declclass m, mdecl (sig, mthd m))"


350 


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


352 
by (simp add: method_def)


353 


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


355 
by (simp add: method_def)


356 


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


358 
by (simp add: method_def)


359 


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


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


362 


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


364 
by (simp add: mbr_def method_def)


365 


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


367 
by (simp add: method_def)


368 


369 
constdefs


370 
fieldm :: "vname \<Rightarrow> (qtname \<times> field) \<Rightarrow> (qtname \<times> memberdecl)"


371 
"fieldm n f \<equiv> (declclass f, fdecl (n, fld f))"


372 


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


374 
by (simp add: fieldm_def)


375 


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


377 
by (simp add: fieldm_def)


378 


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


380 
by (simp add: fieldm_def)


381 


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


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


384 


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


386 
by (simp add: mbr_def fieldm_def)


387 


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


389 
by (simp add: fieldm_def)


390 


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


392 
@{text msig} *}


393 


394 
constdefs msig:: "(qtname \<times> mdecl) \<Rightarrow> sig"


395 
"msig m \<equiv> fst (snd m)"


396 


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


398 
by (simp add: msig_def)


399 


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


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


402 


403 
constdefs qmdecl :: "sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> mdecl)"


404 
"qmdecl sig m \<equiv> (declclass m, (sig,mthd m))"


405 


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


407 
by (simp add: qmdecl_def)


408 


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


410 
by (simp add: qmdecl_def)


411 


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


413 
by (simp add: qmdecl_def)


414 


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


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


417 


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


419 
by (simp add: qmdecl_def)


420 


421 
lemma mdecl_qmdecl_simp[simp]:


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


423 
by (simp add: qmdecl_def)


424 


425 
lemma methdMembr_qmdecl_simp [simp]:


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


427 
by (simp add: methdMembr_def qmdecl_def method_def)


428 


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


430 
out of various HOL types *}


431 


432 
axclass has_resTy < "type"


433 
consts resTy:: "'a::has_resTy \<Rightarrow> ty"


434 


435 
instance access_field_type :: ("type","has_resTy") has_resTy


436 
by (intro_classes)


437 


438 
defs (overloaded)


439 
decl_resTy_def:


440 
"resTy (m::('a::has_resTy) decl_scheme) \<equiv> resTy (Decl.decl.more m)"


441 


442 
instance static_field_type :: ("type","has_resTy") has_resTy


443 
by (intro_classes)


444 


445 
defs (overloaded)


446 
static_field_type_resTy_def:


447 
"resTy (m::(bool,'b::has_resTy) static_field_type)


448 
\<equiv> resTy (static_more m)"


449 


450 
instance pars_field_type :: ("type","has_resTy") has_resTy


451 
by (intro_classes)


452 


453 
defs (overloaded)


454 
pars_field_type_resTy_def:


455 
"resTy (m::(vname list,'b::has_resTy) pars_field_type)


456 
\<equiv> resTy (pars_more m)"


457 


458 
instance resT_field_type :: ("type","type") has_resTy


459 
by (intro_classes)


460 


461 
defs (overloaded)


462 
resT_field_type_resTy_def:


463 
"resTy (m::(ty,'b::type) resT_field_type)


464 
\<equiv> resT_val m"


465 


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


467 
apply (cases m)


468 
apply (simp add: decl_resTy_def static_field_type_resTy_def


469 
pars_field_type_resTy_def resT_field_type_resTy_def


470 
member.dest_convs mhead.dest_convs)


471 
done


472 


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


474 
by (simp add: mhead_def mhead_resTy_simp)


475 


476 
instance * :: ("type","has_resTy") has_resTy


477 
by (intro_classes)


478 


479 
defs (overloaded)


480 
pair_resTy_def: "resTy p \<equiv> resTy (snd p)"


481 


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


483 
by (simp add: pair_resTy_def)


484 


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


486 
by (cases m) (simp)


487 


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


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


490 


491 
subsubsection "inheritablein"


492 
text {*


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


494 
classes in package P if:


495 
\begin{itemize}


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


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


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


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


500 
it is not accessible for inheritance at all.


501 
\end{itemize}


502 
*}


503 
constdefs


504 
inheritable_in::


505 
"prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> pname \<Rightarrow> bool"


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


507 
"G\<turnstile>membr inheritable_in pack


508 
\<equiv> (case (accmodi membr) of


509 
Private \<Rightarrow> False


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


511 
 Protected \<Rightarrow> True


512 
 Public \<Rightarrow> True)"


513 


514 
syntax


515 
Method_inheritable_in::


516 
"prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> pname \<Rightarrow> bool"


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


518 


519 
translations


520 
"G\<turnstile>Method m inheritable_in p" == "G\<turnstile>methdMembr m inheritable_in p"


521 


522 
syntax


523 
Methd_inheritable_in::


524 
"prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> pname \<Rightarrow> bool"


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


526 


527 
translations


528 
"G\<turnstile>Methd s m inheritable_in p" == "G\<turnstile>(method s m) inheritable_in p"


529 


530 
subsubsection "declaredin/undeclaredin"


531 


532 
constdefs cdeclaredmethd:: "prog \<Rightarrow> qtname \<Rightarrow> (sig,methd) table"


533 
"cdeclaredmethd G C


534 
\<equiv> (case class G C of


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


536 
 Some c \<Rightarrow> table_of (methods c)


537 
)"


538 


539 
constdefs


540 
cdeclaredfield:: "prog \<Rightarrow> qtname \<Rightarrow> (vname,field) table"


541 
"cdeclaredfield G C


542 
\<equiv> (case class G C of


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


544 
 Some c \<Rightarrow> table_of (cfields c)


545 
)"


546 


547 


548 
constdefs


549 
declared_in:: "prog \<Rightarrow> memberdecl \<Rightarrow> qtname \<Rightarrow> bool"


550 
("_\<turnstile> _ declared'_in _" [61,61,61] 60)


551 
"G\<turnstile>m declared_in C \<equiv> (case m of


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


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


554 


555 
syntax


556 
method_declared_in:: "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> qtname \<Rightarrow> bool"


557 
("_\<turnstile>Method _ declared'_in _" [61,61,61] 60)


558 
translations


559 
"G\<turnstile>Method m declared_in C" == "G\<turnstile>mdecl (mthd m) declared_in C"


560 


561 
syntax


562 
methd_declared_in:: "prog \<Rightarrow> sig \<Rightarrow>(qtname \<times> methd) \<Rightarrow> qtname \<Rightarrow> bool"


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


564 
translations


565 
"G\<turnstile>Methd s m declared_in C" == "G\<turnstile>mdecl (s,mthd m) declared_in C"


566 


567 
lemma declared_in_classD:


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


569 
by (cases m)


570 
(auto simp add: declared_in_def cdeclaredmethd_def cdeclaredfield_def)


571 


572 
constdefs


573 
undeclared_in:: "prog \<Rightarrow> memberid \<Rightarrow> qtname \<Rightarrow> bool"


574 
("_\<turnstile> _ undeclared'_in _" [61,61,61] 60)


575 


576 
"G\<turnstile>m undeclared_in C \<equiv> (case m of


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


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


579 


580 
lemma method_declared_inI:


581 
"\<lbrakk>class G C = Some c; table_of (methods c) sig = Some m\<rbrakk>


582 
\<Longrightarrow> G\<turnstile>mdecl (sig,m) declared_in C"


583 
by (auto simp add: declared_in_def cdeclaredmethd_def)


584 


585 


586 
subsubsection "members"


587 


588 
consts


589 
members:: "prog \<Rightarrow> (qtname \<times> (qtname \<times> memberdecl)) set"


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


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


592 
below


593 
*)


594 


595 
syntax


596 
member_of:: "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> bool"


597 
("_ \<turnstile> _ member'_of _" [61,61,61] 60)


598 


599 
translations


600 
"G\<turnstile>m member_of C" \<rightleftharpoons> "(C,m) \<in> members G"


601 


602 
inductive "members G" intros


603 


604 
Immediate: "\<lbrakk>G\<turnstile>mbr m declared_in C;declclass m = C\<rbrakk> \<Longrightarrow> G\<turnstile>m member_of C"


605 
Inherited: "\<lbrakk>G\<turnstile>m inheritable_in (pid C); G\<turnstile>memberid m undeclared_in C;


606 
G\<turnstile>C \<prec>\<^sub>C\<^sub>1 S; G\<turnstile>(Class S) accessible_in (pid C);G\<turnstile>m member_of S


607 
\<rbrakk> \<Longrightarrow> G\<turnstile>m member_of C"


608 
text {* Note that in the case of an inherited member only the members of the


609 
direct superclass are concerned. If a member of a superclass of the direct


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


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


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


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


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


615 
package as A or not.*}


616 


617 
syntax


618 
method_member_of:: "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> qtname \<Rightarrow> bool"


619 
("_ \<turnstile>Method _ member'_of _" [61,61,61] 60)


620 


621 
translations


622 
"G\<turnstile>Method m member_of C" \<rightleftharpoons> "G\<turnstile>(methdMembr m) member_of C"


623 


624 
syntax


625 
methd_member_of:: "prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> qtname \<Rightarrow> bool"


626 
("_ \<turnstile>Methd _ _ member'_of _" [61,61,61,61] 60)


627 


628 
translations


629 
"G\<turnstile>Methd s m member_of C" \<rightleftharpoons> "G\<turnstile>(method s m) member_of C"


630 


631 
syntax


632 
fieldm_member_of:: "prog \<Rightarrow> vname \<Rightarrow> (qtname \<times> field) \<Rightarrow> qtname \<Rightarrow> bool"


633 
("_ \<turnstile>Field _ _ member'_of _" [61,61,61] 60)


634 


635 
translations


636 
"G\<turnstile>Field n f member_of C" \<rightleftharpoons> "G\<turnstile>fieldm n f member_of C"


637 


638 
constdefs


639 
inherits:: "prog \<Rightarrow> qtname \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> bool"


640 
("_ \<turnstile> _ inherits _" [61,61,61] 60)


641 
"G\<turnstile>C inherits m


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


643 
(\<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)"


644 


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


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


647 


648 


649 
constdefs member_in::"prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> bool"


650 
("_ \<turnstile> _ member'_in _" [61,61,61] 60)


651 
"G\<turnstile>m member_in C \<equiv> \<exists> provC. G\<turnstile> C \<preceq>\<^sub>C provC \<and> G \<turnstile> m member_of provC"


652 
text {* A member is in a class if it is member of the class or a superclass.


653 
If a member is in a class we can select this member. This additional notion


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


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


656 


657 
syntax


658 
method_member_in:: "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> qtname \<Rightarrow> bool"


659 
("_ \<turnstile>Method _ member'_in _" [61,61,61] 60)


660 


661 
translations


662 
"G\<turnstile>Method m member_in C" \<rightleftharpoons> "G\<turnstile>(methdMembr m) member_in C"


663 


664 
syntax


665 
methd_member_in:: "prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> qtname \<Rightarrow> bool"


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


667 


668 
translations


669 
"G\<turnstile>Methd s m member_in C" \<rightleftharpoons> "G\<turnstile>(method s m) member_in C"


670 


671 
consts stat_overridesR::


672 
"prog \<Rightarrow> ((qtname \<times> mdecl) \<times> (qtname \<times> mdecl)) set"


673 


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


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


676 
by (auto simp add: member_in_def)


677 


678 
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"


679 
by (auto simp add: member_in_def)


680 


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


682 
by (auto intro: member_inI)


683 


684 


685 
subsubsection "overriding"


686 


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


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


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


690 
*}


691 


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


693 
syntax


694 
stat_overrides:: "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> bool"


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


696 
translations


697 
"G\<turnstile>new overrides\<^sub>S old" == "(new,old) \<in> stat_overridesR G "


698 


699 
inductive "stat_overridesR G" intros


700 


701 
Direct: "\<lbrakk>\<not> is_static new; msig new = msig old;


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


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


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


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


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


707 
G \<turnstile>Method old member_of superNew


708 
\<rbrakk> \<Longrightarrow> G\<turnstile>new overrides\<^sub>S old"


709 


710 
Indirect: "\<lbrakk>G\<turnstile>new overrides\<^sub>S inter; G\<turnstile>inter overrides\<^sub>S old\<rbrakk>


711 
\<Longrightarrow> G\<turnstile>new overrides\<^sub>S old"


712 


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


714 
consts overridesR::


715 
"prog \<Rightarrow> ((qtname \<times> mdecl) \<times> (qtname \<times> mdecl)) set"


716 


717 


718 
overrides:: "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> bool"


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


720 
translations


721 
"G\<turnstile>new overrides old" == "(new,old) \<in> overridesR G "


722 


723 
inductive "overridesR G" intros


724 


725 
Direct: "\<lbrakk>\<not> is_static new; \<not> is_static old; accmodi new \<noteq> Private;


726 
msig new = msig old;


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


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


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


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


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


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


733 


734 
Indirect: "\<lbrakk>G\<turnstile>new overrides inter; G\<turnstile>inter overrides old\<rbrakk>


735 
\<Longrightarrow> G\<turnstile>new overrides old"


736 


737 
syntax


738 
sig_stat_overrides::


739 
"prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> methd) \<Rightarrow> bool"


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


741 
translations


742 
"G,s\<turnstile>new overrides\<^sub>S old" \<rightharpoonup> "G\<turnstile>(qmdecl s new) overrides\<^sub>S (qmdecl s old)"


743 


744 
syntax


745 
sig_overrides:: "prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> methd) \<Rightarrow> bool"


746 
("_,_\<turnstile> _ overrides _" [61,61,61,61] 60)


747 
translations


748 
"G,s\<turnstile>new overrides old" \<rightharpoonup> "G\<turnstile>(qmdecl s new) overrides (qmdecl s old)"


749 


750 
subsubsection "Hiding"


751 


752 
constdefs hides::


753 
"prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> bool"


754 
("_\<turnstile> _ hides _" [61,61,61] 60)


755 
"G\<turnstile>new hides old


756 
\<equiv> is_static new \<and> msig new = msig old \<and>


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


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


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


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


761 


762 
syntax


763 
sig_hides:: "prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> bool"


764 
("_,_\<turnstile> _ hides _" [61,61,61,61] 60)


765 
translations


766 
"G,s\<turnstile>new hides old" \<rightharpoonup> "G\<turnstile>(qmdecl s new) hides (qmdecl s old)"


767 


768 
lemma hidesI:


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


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


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


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


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


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


775 
by (auto simp add: hides_def)


776 


777 
lemma hidesD:


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


779 
declclass new \<noteq> Object \<and> is_static new \<and> 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 (auto simp add: hides_def)


784 


785 
lemma overrides_commonD:


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


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


788 
accmodi new \<noteq> Private \<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)


794 


795 
lemma ws_overrides_commonD:


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


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


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


799 
msig new = msig old \<and>


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


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


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


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


804 


805 
lemma stat_overrides_commonD:


806 
"\<lbrakk>G\<turnstile>new overrides\<^sub>S old\<rbrakk> \<Longrightarrow>


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


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


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


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


811 
by (induct set: stat_overridesR) (auto intro: trancl_trans)


812 


813 
lemma overrides_eq_sigD:


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


815 
by (auto dest: overrides_commonD)


816 


817 
lemma hides_eq_sigD:


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


819 
by (auto simp add: hides_def)


820 


821 
subsubsection "permits access"


822 
constdefs


823 
permits_acc::


824 
"prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"


825 
("_ \<turnstile> _ in _ permits'_acc'_to _" [61,61,61,61] 60)


826 


827 
"G\<turnstile>membr in class permits_acc_to accclass


828 
\<equiv> (case (accmodi membr) of


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


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


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


832 
\<or>


833 
(G\<turnstile>accclass \<prec>\<^sub>C declclass membr \<and> G\<turnstile>class \<preceq>\<^sub>C accclass)


834 
 Public \<Rightarrow> True)"


835 
text {*


836 
The subcondition of the @{term "Protected"} case:


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


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


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


840 
holds anyway.


841 
*}


842 


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


844 
of members is not uniform.


845 
\begin{itemize}


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


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


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


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


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


851 
the access to accessible subclasses during runtime.


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


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


854 
\end{itemize}


855 
*}


856 


857 


858 
consts


859 
accessible_fromR::


860 
"prog \<Rightarrow> qtname \<Rightarrow> ((qtname \<times> memberdecl) \<times> qtname) set"


861 


862 
syntax


863 
accessible_from::


864 
"prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"


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


866 


867 
translations


868 
"G\<turnstile>membr of cls accessible_from accclass"


869 
\<rightleftharpoons> "(membr,cls) \<in> accessible_fromR G accclass"


870 


871 
syntax


872 
method_accessible_from::


873 
"prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"


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


875 


876 
translations


877 
"G\<turnstile>Method m of cls accessible_from accclass"


878 
\<rightleftharpoons> "G\<turnstile>methdMembr m of cls accessible_from accclass"


879 


880 
syntax


881 
methd_accessible_from::


882 
"prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"


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


884 


885 
translations


886 
"G\<turnstile>Methd s m of cls accessible_from accclass"


887 
\<rightleftharpoons> "G\<turnstile>(method s m) of cls accessible_from accclass"


888 


889 
syntax


890 
field_accessible_from::


891 
"prog \<Rightarrow> vname \<Rightarrow> (qtname \<times> field) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"


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


893 


894 
translations


895 
"G\<turnstile>Field fn f of C accessible_from accclass"


896 
\<rightleftharpoons> "G\<turnstile>(fieldm fn f) of C accessible_from accclass"


897 


898 
inductive "accessible_fromR G accclass" intros


899 
immediate: "\<lbrakk>G\<turnstile>membr member_of class;


900 
G\<turnstile>(Class class) accessible_in (pid accclass);


901 
G\<turnstile>membr in class permits_acc_to accclass


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


903 


904 
overriding: "\<lbrakk>G\<turnstile>membr member_of class;


905 
G\<turnstile>(Class class) accessible_in (pid accclass);


906 
membr=(C,mdecl new);


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


908 
G\<turnstile>class \<prec>\<^sub>C sup;


909 
G\<turnstile>Method old of sup accessible_from accclass


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


911 


912 
consts


913 
dyn_accessible_fromR::


914 
"prog \<Rightarrow> qtname \<Rightarrow> ((qtname \<times> memberdecl) \<times> qtname) set"


915 


916 
syntax


917 
dyn_accessible_from::


918 
"prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"


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


920 


921 
translations


922 
"G\<turnstile>membr in C dyn_accessible_from accC"


923 
\<rightleftharpoons> "(membr,C) \<in> dyn_accessible_fromR G accC"


924 


925 
syntax


926 
method_dyn_accessible_from::


927 
"prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"


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


929 


930 
translations


931 
"G\<turnstile>Method m in C dyn_accessible_from accC"


932 
\<rightleftharpoons> "G\<turnstile>methdMembr m in C dyn_accessible_from accC"


933 


934 
syntax


935 
methd_dyn_accessible_from::


936 
"prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"


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


938 


939 
translations


940 
"G\<turnstile>Methd s m in C dyn_accessible_from accC"


941 
\<rightleftharpoons> "G\<turnstile>(method s m) in C dyn_accessible_from accC"


942 


943 
syntax


944 
field_dyn_accessible_from::


945 
"prog \<Rightarrow> vname \<Rightarrow> (qtname \<times> field) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"


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


947 


948 
translations


949 
"G\<turnstile>Field fn f in dynC dyn_accessible_from accC"


950 
\<rightleftharpoons> "G\<turnstile>(fieldm fn f) in dynC dyn_accessible_from accC"


951 


952 
(* #### Testet JVM noch über den Bytecodeverifier hinaus ob der


953 
statische Typ accessible ist bevor es den Zugriff erlaubt


954 
\<longrightarrow> Test mit Reflektion\<dots>


955 
*)


956 
inductive "dyn_accessible_fromR G accclass" intros


957 
immediate: "\<lbrakk>G\<turnstile>membr member_in class;


958 
G\<turnstile>membr in class permits_acc_to accclass


959 
\<rbrakk> \<Longrightarrow> G\<turnstile>membr in class dyn_accessible_from accclass"


960 


961 
overriding: "\<lbrakk>G\<turnstile>membr member_in class;


962 
membr=(C,mdecl new);


963 
G\<turnstile>(C,new) overrides old;


964 
G\<turnstile>class \<prec>\<^sub>C sup;


965 
G\<turnstile>Method old in sup dyn_accessible_from accclass


966 
\<rbrakk>\<Longrightarrow> G\<turnstile>membr in class dyn_accessible_from accclass"


967 


968 


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


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


971 
by (auto elim: accessible_fromR.induct)


972 


973 
lemma declared_not_undeclared:


974 
"G\<turnstile>m declared_in C \<Longrightarrow> \<not> G\<turnstile> memberid m undeclared_in C"


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


976 


977 
lemma not_undeclared_declared:


978 
"\<not> G\<turnstile> membr_id undeclared_in C \<Longrightarrow> (\<exists> m. G\<turnstile>m declared_in C \<and>


979 
membr_id = memberid m)"


980 
proof 


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


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


983 
proof (cases membr_id)


984 
case (fid vname)


985 
with not_undecl


986 
obtain fld where


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


988 
by (auto simp add: undeclared_in_def declared_in_def


989 
cdeclaredfield_def)


990 
with fid show ?thesis


991 
by auto


992 
next


993 
case (mid sig)


994 
with not_undecl


995 
obtain mthd where


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


997 
by (auto simp add: undeclared_in_def declared_in_def


998 
cdeclaredmethd_def)


999 
with mid show ?thesis


1000 
by auto


1001 
qed


1002 
qed


1003 


1004 
lemma unique_declared_in:


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


1006 
\<Longrightarrow> m = n"


1007 
by (auto simp add: declared_in_def cdeclaredmethd_def cdeclaredfield_def


1008 
split: memberdecl.splits)


1009 


1010 
lemma unique_member_of:


1011 
(assumes n: "G\<turnstile>n member_of C" and


1012 
m: "G\<turnstile>m member_of C" and


1013 
eqid: "memberid n = memberid m"


1014 
) "n=m"


1015 
proof 


1016 
from n m eqid


1017 
show "n=m"


1018 
proof (induct)


1019 
case (Immediate C n)


1020 
assume member_n: "G\<turnstile> mbr n declared_in C" "declclass n = C"


1021 
assume eqid: "memberid n = memberid m"


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


1023 
then show "n=m"


1024 
proof (cases)


1025 
case (Immediate _ m')


1026 
with eqid


1027 
have "m=m'"


1028 
"memberid n = memberid m"


1029 
"G\<turnstile> mbr m declared_in C"


1030 
"declclass m = C"


1031 
by auto


1032 
with member_n


1033 
show ?thesis


1034 
by (cases n, cases m)


1035 
(auto simp add: declared_in_def


1036 
cdeclaredmethd_def cdeclaredfield_def


1037 
split: memberdecl.splits)


1038 
next


1039 
case (Inherited _ _ m')


1040 
then have "G\<turnstile> memberid m undeclared_in C"


1041 
by simp


1042 
with eqid member_n


1043 
show ?thesis


1044 
by (cases n) (auto dest: declared_not_undeclared)


1045 
qed


1046 
next


1047 
case (Inherited C S n)


1048 
assume undecl: "G\<turnstile> memberid n undeclared_in C"


1049 
assume super: "G\<turnstile>C\<prec>\<^sub>C\<^sub>1S"


1050 
assume hyp: "\<lbrakk>G \<turnstile> m member_of S; memberid n = memberid m\<rbrakk> \<Longrightarrow> n = m"


1051 
assume eqid: "memberid n = memberid m"


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


1053 
then show "n=m"


1054 
proof (cases)


1055 
case Immediate


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


1057 
with eqid undecl


1058 
show ?thesis


1059 
by (cases m) (auto dest: declared_not_undeclared)


1060 
next


1061 
case Inherited


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


1063 
by (auto dest!: subcls1D)


1064 
with eqid hyp


1065 
show ?thesis


1066 
by blast


1067 
qed


1068 
qed


1069 
qed


1070 


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


1072 
proof (induct set: members)


1073 
case (Immediate C m)


1074 
assume "G\<turnstile> mbr m declared_in C"


1075 
then show "is_class G C"


1076 
by (cases "mbr m")


1077 
(auto simp add: declared_in_def cdeclaredmethd_def cdeclaredfield_def)


1078 
next


1079 
case (Inherited C S m)


1080 
assume "G\<turnstile>C\<prec>\<^sub>C\<^sub>1S" and "is_class G S"


1081 
then show "is_class G C"


1082 
by  (rule subcls_is_class2,auto)


1083 
qed


1084 


1085 
lemma member_of_declC:


1086 
"G\<turnstile>m member_of C


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


1088 
by (induct set: members) auto


1089 


1090 
lemma member_of_member_of_declC:


1091 
"G\<turnstile>m member_of C


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


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


1094 


1095 
lemma member_of_class_relation:


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


1097 
proof (induct set: members)


1098 
case (Immediate C m)


1099 
then show "G\<turnstile>C \<preceq>\<^sub>C declclass m" by simp


1100 
next


1101 
case (Inherited C S m)


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


1103 
by (auto dest: r_into_rtrancl intro: rtrancl_trans)


1104 
qed


1105 


1106 
lemma member_in_class_relation:


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


1108 
by (auto dest: member_inD member_of_class_relation


1109 
intro: rtrancl_trans)


1110 


1111 
lemma member_of_Package:


1112 
"\<lbrakk>G\<turnstile>m member_of C; accmodi m = Package\<rbrakk>


1113 
\<Longrightarrow> pid (declclass m) = pid C"


1114 
proof 


1115 
assume member: "G\<turnstile>m member_of C"


1116 
then show " accmodi m = Package \<Longrightarrow> ?thesis" (is "PROP ?P m C")


1117 
proof (induct rule: members.induct)


1118 
fix C m


1119 
assume C: "declclass m = C"


1120 
then show "pid (declclass m) = pid C"


1121 
by simp


1122 
next


1123 
fix C S m


1124 
assume inheritable: "G \<turnstile> m inheritable_in pid C"


1125 
assume hyp: "PROP ?P m S" and


1126 
package_acc: "accmodi m = Package"


1127 
with inheritable package_acc hyp


1128 
show "pid (declclass m) = pid C"


1129 
by (auto simp add: inheritable_in_def)


1130 
qed


1131 
qed


1132 


1133 
lemma dyn_accessible_from_commonD: "G\<turnstile>m in C dyn_accessible_from S


1134 
\<Longrightarrow> G\<turnstile>m member_in C"


1135 
by (auto elim: dyn_accessible_fromR.induct)


1136 


1137 
(* ### Gilt nicht für wf_progs!dynmaisches Override,


1138 
da die accmodi Bedingung nur für stat override gilt! *)


1139 
(*


1140 
lemma override_Package:


1141 
"\<lbrakk>G\<turnstile>new overrides old;


1142 
\<And> new old. G\<turnstile>new overrides old \<Longrightarrow> accmodi old \<le> accmodi new;


1143 
accmodi old = Package; accmodi new = Package\<rbrakk>


1144 
\<Longrightarrow> pid (declclass old) = pid (declclass new)"


1145 
proof 


1146 
assume wf: "\<And> new old. G\<turnstile>new overrides old \<Longrightarrow> accmodi old \<le> accmodi new"


1147 
assume ovverride: "G\<turnstile>new overrides old"


1148 
then show "\<lbrakk>accmodi old = Package;accmodi new = Package\<rbrakk> \<Longrightarrow> ?thesis"


1149 
(is "?Pack old \<Longrightarrow> ?Pack new \<Longrightarrow> ?EqPid old new")


1150 
proof (induct rule: overridesR.induct)


1151 
case Direct


1152 
fix new old


1153 
assume "accmodi old = Package"


1154 
"G \<turnstile> methdMembr old inheritable_in pid (declclass new)"


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


1156 
by (auto simp add: inheritable_in_def)


1157 
next


1158 
case (Indirect inter new old)


1159 
assume accmodi_old: "accmodi old = Package" and


1160 
accmodi_new: "accmodi new = Package"


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


1162 
with wf have le_inter_new: "accmodi inter \<le> accmodi new"


1163 
by blast


1164 
assume "G \<turnstile> inter overrides old"


1165 
with wf have le_old_inter: "accmodi old \<le> accmodi inter"


1166 
by blast


1167 
from accmodi_old accmodi_new le_inter_new le_old_inter


1168 
have "accmodi inter = Package"


1169 
by(auto simp add: le_acc_def less_acc_def)


1170 
with Indirect accmodi_old accmodi_new


1171 
show "?EqPid old new"


1172 
by auto


1173 
qed


1174 
qed


1175 


1176 
lemma stat_override_Package:


1177 
"\<lbrakk>G\<turnstile>new overrides\<^sub>S old;


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


1179 
accmodi old = Package; accmodi new = Package\<rbrakk>


1180 
\<Longrightarrow> pid (declclass old) = pid (declclass new)"


1181 
proof 


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


1183 
assume ovverride: "G\<turnstile>new overrides\<^sub>S old"


1184 
then show "\<lbrakk>accmodi old = Package;accmodi new = Package\<rbrakk> \<Longrightarrow> ?thesis"


1185 
(is "?Pack old \<Longrightarrow> ?Pack new \<Longrightarrow> ?EqPid old new")


1186 
proof (induct rule: stat_overridesR.induct)


1187 
case Direct


1188 
fix new old


1189 
assume "accmodi old = Package"


1190 
"G \<turnstile> methdMembr old inheritable_in pid (declclass new)"


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


1192 
by (auto simp add: inheritable_in_def)


1193 
next


1194 
case (Indirect inter new old)


1195 
assume accmodi_old: "accmodi old = Package" and


1196 
accmodi_new: "accmodi new = Package"


1197 
assume "G \<turnstile> new overrides\<^sub>S inter"


1198 
with wf have le_inter_new: "accmodi inter \<le> accmodi new"


1199 
by blast


1200 
assume "G \<turnstile> inter overrides\<^sub>S old"


1201 
with wf have le_old_inter: "accmodi old \<le> accmodi inter"


1202 
by blast


1203 
from accmodi_old accmodi_new le_inter_new le_old_inter


1204 
have "accmodi inter = Package"


1205 
by(auto simp add: le_acc_def less_acc_def)


1206 
with Indirect accmodi_old accmodi_new


1207 
show "?EqPid old new"


1208 
by auto


1209 
qed


1210 
qed


1211 


1212 
*)


1213 
lemma no_Private_stat_override:


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


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


1216 


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


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


1219 


1220 
lemma permits_acc_inheritance:


1221 
"\<lbrakk>G\<turnstile>m in statC permits_acc_to accC; G\<turnstile>dynC \<preceq>\<^sub>C statC


1222 
\<rbrakk> \<Longrightarrow> G\<turnstile>m in dynC permits_acc_to accC"


1223 
by (cases "accmodi m")


1224 
(auto simp add: permits_acc_def


1225 
intro: subclseq_trans)


1226 


1227 
lemma field_accessible_fromD:


1228 
"\<lbrakk>G\<turnstile>membr of C accessible_from accC;is_field membr\<rbrakk>


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


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


1231 
G\<turnstile>membr in C permits_acc_to accC"


1232 
by (cases set: accessible_fromR)


1233 
(auto simp add: is_field_def split: memberdecl.splits)


1234 


1235 
lemma field_accessible_from_permits_acc_inheritance:


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


1237 
\<Longrightarrow> G\<turnstile>membr in dynC permits_acc_to accC"


1238 
by (auto dest: field_accessible_fromD intro: permits_acc_inheritance)


1239 


1240 


1241 
(*


1242 
lemma accessible_Package:


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


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


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


1246 
proof 


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


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


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


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


1251 
proof (induct rule: accessible_fromR.induct)


1252 
fix C m


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


1254 
"G \<turnstile> m in C permits_acc_to S"


1255 
"accmodi m = Package"


1256 
then show "?P C m"


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


1258 
next


1259 
fix declC C new newm old Sup


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


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


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


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


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


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


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


1267 
accmodi_new: "accmodi new = Package"


1268 
from override wf


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


1270 
by (cases old,cases newm) auto


1271 
from override new


1272 
have "accmodi old \<noteq> Private"


1273 
by (simp add: no_Private_stat_override)


1274 
with accmodi_weaken accmodi_new new


1275 
have accmodi_old: "accmodi old = Package"


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


1277 
with hyp


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


1279 
by (simp)


1280 
from wf override new accmodi_old accmodi_new


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


1282 
by (auto dest: stat_override_Package)


1283 
from member_new accmodi_new


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


1285 
by (auto dest: member_of_Package)


1286 
with eq_pid_new_old P_sup show "?P C new"


1287 
by auto


1288 
qed


1289 
qed


1290 
*)


1291 
lemma accessible_fieldD:


1292 
"\<lbrakk>G\<turnstile>membr of C accessible_from accC; is_field membr\<rbrakk>


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


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


1295 
G\<turnstile>membr in C permits_acc_to accC"


1296 
by (induct rule: accessible_fromR.induct) (auto dest: is_fieldD)


1297 


1298 
(* lemmata:


1299 
Wegen G\<turnstile>Super accessible_in (pid C) folgt:


1300 
G\<turnstile>m declared_in C; G\<turnstile>m member_of D; accmodi m = Package (G\<turnstile>D \<preceq>\<^sub>C C)


1301 
\<Longrightarrow> pid C = pid D


1302 


1303 
C package


1304 
m public in C


1305 
für alle anderen D: G\<turnstile>m undeclared_in C


1306 
m wird in alle subklassen vererbt, auch aus dem Package heraus!


1307 


1308 
G\<turnstile>m member_of C \<Longrightarrow> \<exists> D. G\<turnstile>C \<preceq>\<^sub>C D \<and> G\<turnstile>m declared_in D


1309 
*)


1310 


1311 
(* Begriff (C,m) overrides (D,m)


1312 
3 Fälle: Direkt,


1313 
Indirekt über eine Zwischenklasse (ohne weiteres override)


1314 
Indirekt über override


1315 
*)


1316 


1317 
(*


1318 
"G\<turnstile>m member_of C \<equiv>


1319 
constdefs declares_method:: "prog \<Rightarrow> sig \<Rightarrow> qtname \<Rightarrow> methd \<Rightarrow> bool"


1320 
("_,_\<turnstile> _ declares'_method _" [61,61,61,61] 60)


1321 
"G,sig\<turnstile>C declares_method m \<equiv> cdeclaredmethd G C sig = Some m"


1322 


1323 
constdefs is_declared:: "prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> bool"


1324 
"is_declared G sig em \<equiv> G,sig\<turnstile>declclass em declares_method mthd em"


1325 
*)


1326 


1327 
lemma member_of_Private:


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


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


1330 


1331 
lemma member_of_subclseq_declC:


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


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


1334 


1335 
lemma member_of_inheritance:


1336 
(assumes m: "G\<turnstile>m member_of D" and


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


1338 
subclseq_C_m: "G\<turnstile>C \<preceq>\<^sub>C declclass m" and


1339 
ws: "ws_prog G"


1340 
) "G\<turnstile>m member_of C"


1341 
proof 


1342 
from m subclseq_D_C subclseq_C_m


1343 
show ?thesis


1344 
proof (induct)


1345 
case (Immediate D m)


1346 
assume "declclass m = D" and


1347 
"G\<turnstile>D\<preceq>\<^sub>C C" and "G\<turnstile>C\<preceq>\<^sub>C declclass m"


1348 
with ws have "D=C"


1349 
by (auto intro: subclseq_acyclic)


1350 
with Immediate


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


1352 
by (auto intro: members.Immediate)


1353 
next


1354 
case (Inherited D S m)


1355 
assume member_of_D_props:


1356 
"G \<turnstile> m inheritable_in pid D"


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


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


1359 
"G \<turnstile> m member_of S"


1360 
assume super: "G\<turnstile>D\<prec>\<^sub>C\<^sub>1S"


1361 
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"


1362 
assume subclseq_C_m: "G\<turnstile>C\<preceq>\<^sub>C declclass m"


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


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


1365 
proof (cases rule: subclseq_cases)


1366 
case Eq


1367 
assume "D=C"


1368 
with super member_of_D_props


1369 
show ?thesis


1370 
by (auto intro: members.Inherited)


1371 
next


1372 
case Subcls


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


1374 
with super


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


1376 
by (auto dest: subcls1D subcls_superD)


1377 
with subclseq_C_m hyp show ?thesis


1378 
by blast


1379 
qed


1380 
qed


1381 
qed


1382 


1383 
lemma member_of_subcls:


1384 
(assumes old: "G\<turnstile>old member_of C" and


1385 
new: "G\<turnstile>new member_of D" and


1386 
eqid: "memberid new = memberid old" and


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


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


1389 
ws: "ws_prog G"


1390 
) "G\<turnstile>D \<prec>\<^sub>C C"


1391 
proof 


1392 
from old


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


1394 
by (auto dest: member_of_subclseq_declC)


1395 
from new


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


1397 
by (auto dest: member_of_subclseq_declC)


1398 
from subcls_new_old ws


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


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


1401 
from subclseq_D_new subclseq_D_C


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


1403 
by (rule subcls_compareable)


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


1405 
proof


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


1407 
next


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


1409 
with new subclseq_D_C ws


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


1411 
by (blast intro: member_of_inheritance)


1412 
with eqid old


1413 
have "new=old"


1414 
by (blast intro: unique_member_of)


1415 
with neq_new_old


1416 
show ?thesis


1417 
by contradiction


1418 
qed


1419 
then show ?thesis


1420 
proof (cases rule: subclseq_cases)


1421 
case Eq


1422 
assume "declclass new = C"


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


1424 
by (auto dest: member_of_member_of_declC)


1425 
with eqid old


1426 
have "new=old"


1427 
by (blast intro: unique_member_of)


1428 
with neq_new_old


1429 
show ?thesis


1430 
by contradiction


1431 
next


1432 
case Subcls


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


1434 
with subclseq_D_new


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


1436 
by (rule rtrancl_trancl_trancl)


1437 
qed


1438 
qed


1439 


1440 
corollary member_of_overrides_subcls:


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


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


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


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


1445 


1446 
corollary member_of_stat_overrides_subcls:


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


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


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


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


1451 


1452 


1453 


1454 
lemma inherited_field_access:


1455 
(assumes stat_acc: "G\<turnstile>membr of statC accessible_from accC" and


1456 
is_field: "is_field membr" and


1457 
subclseq: "G \<turnstile> dynC \<preceq>\<^sub>C statC"


1458 
) "G\<turnstile>membr in dynC dyn_accessible_from accC"


1459 
proof 


1460 
from stat_acc is_field subclseq


1461 
show ?thesis


1462 
by (auto dest: accessible_fieldD


1463 
intro: dyn_accessible_fromR.immediate


1464 
member_inI


1465 
permits_acc_inheritance)


1466 
qed


1467 


1468 
lemma accessible_inheritance:


1469 
(assumes stat_acc: "G\<turnstile>m of statC accessible_from accC" and


1470 
subclseq: "G\<turnstile>dynC \<preceq>\<^sub>C statC" and


1471 
member_dynC: "G\<turnstile>m member_of dynC" and

