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