src/HOL/Bali/DeclConcepts.thy
author wenzelm
Wed Nov 01 20:46:23 2017 +0100 (22 months ago)
changeset 66983 df83b66f1d94
parent 62042 6c6ccf573479
child 67443 3abf6a722518
permissions -rw-r--r--
proper merge (amending fb46c031c841);
     1 (*  Title:      HOL/Bali/DeclConcepts.thy
     2     Author:     Norbert Schirmer
     3 *)
     4 subsection \<open>Advanced concepts on Java declarations like overriding, inheritance,
     5 dynamic method lookup\<close>
     6 
     7 theory DeclConcepts imports TypeRel begin
     8 
     9 subsubsection "access control (cf. 6.6), overriding and hiding (cf. 8.4.6.1)"
    10 
    11 definition 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 
    18 subsection "accessibility of types (cf. 6.6.1)"
    19 text \<open>
    20 Primitive types are always accessible, interfaces and classes are accessible
    21 in their package or if they are defined public, an array type is accessible if
    22 its element type is accessible\<close>
    23  
    24 primrec
    25   accessible_in :: "prog \<Rightarrow> ty \<Rightarrow> pname \<Rightarrow> bool"  ("_ \<turnstile> _ accessible'_in _" [61,61,61] 60) and
    26   rt_accessible_in :: "prog \<Rightarrow> ref_ty \<Rightarrow> pname \<Rightarrow> bool"  ("_ \<turnstile> _ accessible'_in' _" [61,61,61] 60)
    27 where
    28   "G\<turnstile>(PrimT p) accessible_in pack = True"
    29 | accessible_in_RefT_simp:
    30   "G\<turnstile>(RefT  r) accessible_in pack = G\<turnstile>r accessible_in' pack"
    31 | "G\<turnstile>(NullT) accessible_in' pack = True"
    32 | "G\<turnstile>(IfaceT I) accessible_in' pack = ((pid I = pack) \<or> is_public G I)"
    33 | "G\<turnstile>(ClassT C) accessible_in' pack = ((pid C = pack) \<or> is_public G C)"
    34 | "G\<turnstile>(ArrayT ty) accessible_in' pack = G\<turnstile>ty accessible_in pack"
    35 
    36 declare accessible_in_RefT_simp [simp del]
    37 
    38 definition
    39   is_acc_class :: "prog \<Rightarrow> pname \<Rightarrow> qtname \<Rightarrow> bool"
    40   where "is_acc_class G P C = (is_class G C \<and> G\<turnstile>(Class C) accessible_in P)"
    41 
    42 definition
    43   is_acc_iface :: "prog \<Rightarrow> pname \<Rightarrow> qtname \<Rightarrow> bool"
    44   where "is_acc_iface G P I = (is_iface G I \<and> G\<turnstile>(Iface I) accessible_in P)"
    45 
    46 definition
    47   is_acc_type :: "prog \<Rightarrow> pname \<Rightarrow> ty \<Rightarrow> bool"
    48   where "is_acc_type  G P T = (is_type G T  \<and> G\<turnstile>T accessible_in P)"
    49 
    50 definition
    51   is_acc_reftype  :: "prog \<Rightarrow> pname \<Rightarrow> ref_ty \<Rightarrow> bool"
    52   where "is_acc_reftype G P T = (isrtype G T  \<and> G\<turnstile>T accessible_in' P)"
    53 
    54 lemma is_acc_classD:
    55  "is_acc_class G P C \<Longrightarrow>  is_class G C \<and> G\<turnstile>(Class C) accessible_in P"
    56 by (simp add: is_acc_class_def)
    57 
    58 lemma is_acc_class_is_class: "is_acc_class G P C \<Longrightarrow> is_class G C"
    59 by (auto simp add: is_acc_class_def)
    60 
    61 lemma is_acc_ifaceD:
    62   "is_acc_iface G P I \<Longrightarrow> is_iface G I \<and> G\<turnstile>(Iface I) accessible_in P"
    63 by (simp add: is_acc_iface_def)
    64 
    65 lemma is_acc_typeD:
    66  "is_acc_type  G P T \<Longrightarrow> is_type G T  \<and> G\<turnstile>T accessible_in P"
    67 by (simp add: is_acc_type_def)
    68 
    69 lemma is_acc_reftypeD:
    70 "is_acc_reftype  G P T \<Longrightarrow> isrtype G T  \<and> G\<turnstile>T accessible_in' P"
    71 by (simp add: is_acc_reftype_def)
    72 
    73 subsection "accessibility of members"
    74 text \<open>
    75 The accessibility of members is more involved as the accessibility of types.
    76 We have to distinguish several cases to model the different effects of 
    77 accessibility during inheritance, overriding and ordinary member access 
    78 \<close>
    79 
    80 subsubsection \<open>Various technical conversion and selection functions\<close>
    81 
    82 text \<open>overloaded selector \<open>accmodi\<close> to select the access modifier 
    83 out of various HOL types\<close>
    84 
    85 class has_accmodi =
    86   fixes accmodi:: "'a \<Rightarrow> acc_modi"
    87 
    88 instantiation acc_modi :: has_accmodi
    89 begin
    90 
    91 definition
    92   acc_modi_accmodi_def: "accmodi (a::acc_modi) = a"
    93 
    94 instance ..
    95 
    96 end
    97 
    98 lemma acc_modi_accmodi_simp[simp]: "accmodi (a::acc_modi) = a"
    99 by (simp add: acc_modi_accmodi_def)
   100 
   101 instantiation decl_ext :: (type) has_accmodi
   102 begin
   103 
   104 definition
   105   decl_acc_modi_def: "accmodi (d::('a:: type) decl_scheme) = access d"
   106 
   107 instance ..
   108 
   109 end
   110 
   111 lemma decl_acc_modi_simp[simp]: "accmodi (d::('a::type) decl_scheme) = access d"
   112 by (simp add: decl_acc_modi_def)
   113 
   114 instantiation prod :: (type, has_accmodi) has_accmodi
   115 begin
   116 
   117 definition
   118   pair_acc_modi_def: "accmodi p = accmodi (snd p)"
   119 
   120 instance ..
   121 
   122 end
   123 
   124 lemma pair_acc_modi_simp[simp]: "accmodi (x,a) = (accmodi a)"
   125 by (simp add: pair_acc_modi_def)
   126 
   127 instantiation memberdecl :: has_accmodi
   128 begin
   129 
   130 definition
   131   memberdecl_acc_modi_def: "accmodi m = (case m of
   132                                           fdecl f \<Rightarrow> accmodi f
   133                                         | mdecl m \<Rightarrow> accmodi m)"
   134 
   135 instance ..
   136 
   137 end
   138 
   139 lemma memberdecl_fdecl_acc_modi_simp[simp]:
   140  "accmodi (fdecl m) = accmodi m"
   141 by (simp add: memberdecl_acc_modi_def)
   142 
   143 lemma memberdecl_mdecl_acc_modi_simp[simp]:
   144  "accmodi (mdecl m) = accmodi m"
   145 by (simp add: memberdecl_acc_modi_def)
   146 
   147 text \<open>overloaded selector \<open>declclass\<close> to select the declaring class 
   148 out of various HOL types\<close>
   149 
   150 class has_declclass =
   151   fixes declclass:: "'a \<Rightarrow> qtname"
   152 
   153 instantiation qtname_ext :: (type) has_declclass
   154 begin
   155 
   156 definition
   157   "declclass q = \<lparr> pid = pid q, tid = tid q \<rparr>"
   158 
   159 instance ..
   160 
   161 end
   162 
   163 lemma qtname_declclass_def:
   164   "declclass q \<equiv> (q::qtname)"
   165   by (induct q) (simp add: declclass_qtname_ext_def)
   166 
   167 lemma qtname_declclass_simp[simp]: "declclass (q::qtname) = q"
   168 by (simp add: qtname_declclass_def)
   169 
   170 instantiation prod :: (has_declclass, type) has_declclass
   171 begin
   172 
   173 definition
   174   pair_declclass_def: "declclass p = declclass (fst p)"
   175 
   176 instance ..
   177 
   178 end
   179 
   180 lemma pair_declclass_simp[simp]: "declclass (c,x) = declclass c" 
   181 by (simp add: pair_declclass_def)
   182 
   183 text \<open>overloaded selector \<open>is_static\<close> to select the static modifier 
   184 out of various HOL types\<close>
   185 
   186 class has_static =
   187   fixes is_static :: "'a \<Rightarrow> bool"
   188 
   189 instantiation decl_ext :: (has_static) has_static
   190 begin
   191 
   192 instance ..
   193 
   194 end
   195 
   196 instantiation member_ext :: (type) has_static
   197 begin
   198 
   199 instance ..
   200 
   201 end
   202 
   203 axiomatization where
   204   static_field_type_is_static_def: "is_static (m::('a member_scheme)) \<equiv> static m"
   205 
   206 lemma member_is_static_simp: "is_static (m::'a member_scheme) = static m"
   207 by (simp add: static_field_type_is_static_def)
   208 
   209 instantiation prod :: (type, has_static) has_static
   210 begin
   211 
   212 definition
   213   pair_is_static_def: "is_static p = is_static (snd p)"
   214 
   215 instance ..
   216 
   217 end
   218 
   219 lemma pair_is_static_simp [simp]: "is_static (x,s) = is_static s"
   220 by (simp add: pair_is_static_def)
   221 
   222 lemma pair_is_static_simp1: "is_static p = is_static (snd p)"
   223 by (simp add: pair_is_static_def)
   224 
   225 instantiation memberdecl :: has_static
   226 begin
   227 
   228 definition
   229 memberdecl_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 
   234 instance ..
   235 
   236 end
   237 
   238 lemma memberdecl_is_static_fdecl_simp[simp]:
   239  "is_static (fdecl f) = is_static f"
   240 by (simp add: memberdecl_is_static_def)
   241 
   242 lemma memberdecl_is_static_mdecl_simp[simp]:
   243  "is_static (mdecl m) = is_static m"
   244 by (simp add: memberdecl_is_static_def)
   245 
   246 lemma mhead_static_simp [simp]: "is_static (mhead m) = is_static m"
   247 by (cases m) (simp add: mhead_def member_is_static_simp)
   248 
   249 \<comment> \<open>some mnemotic selectors for various pairs\<close> 
   250 
   251 definition
   252   decliface :: "qtname \<times> 'a decl_scheme \<Rightarrow> qtname" where
   253   "decliface = fst"          \<comment>\<open>get the interface component\<close>
   254 
   255 definition
   256   mbr :: "qtname \<times> memberdecl \<Rightarrow> memberdecl" where
   257   "mbr = snd"            \<comment>\<open>get the memberdecl component\<close>
   258 
   259 definition
   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 
   264 definition
   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 
   271 definition
   272   fname:: "vname \<times> 'a \<Rightarrow> vname"
   273   where "fname = fst"
   274     \<comment>\<open>also used for fdecl\<close>
   275 
   276 definition
   277   declclassf:: "(vname \<times> qtname) \<Rightarrow> qtname"
   278   where "declclassf = snd"
   279 
   280 
   281 lemma decliface_simp[simp]: "decliface (I,m) = I"
   282 by (simp add: decliface_def) 
   283 
   284 lemma mbr_simp[simp]: "mbr (C,m) = m"
   285 by (simp add: mbr_def)
   286 
   287 lemma access_mbr_simp [simp]: "(accmodi (mbr m)) = accmodi m"
   288 by (cases m) (simp add:  mbr_def) 
   289 
   290 lemma mthd_simp[simp]: "mthd (C,m) = m"
   291 by (simp add: mthd_def)
   292 
   293 lemma fld_simp[simp]: "fld (C,f) = f"
   294 by (simp add: fld_def)
   295 
   296 lemma accmodi_simp[simp]: "accmodi (C,m) = access m"
   297 by (simp )
   298 
   299 lemma access_mthd_simp [simp]: "(access (mthd m)) = accmodi m"
   300 by (cases m) (simp add: mthd_def) 
   301 
   302 lemma access_fld_simp [simp]: "(access (fld f)) = accmodi f"
   303 by (cases f) (simp add:  fld_def) 
   304 
   305 lemma static_mthd_simp[simp]: "static (mthd m) = is_static m"
   306 by (cases m) (simp add:  mthd_def member_is_static_simp)
   307 
   308 lemma mthd_is_static_simp [simp]: "is_static (mthd m) = is_static m"
   309 by (cases m) simp
   310 
   311 lemma static_fld_simp[simp]: "static (fld f) = is_static f"
   312 by (cases f) (simp add:  fld_def member_is_static_simp)
   313 
   314 lemma ext_field_simp [simp]: "(declclass f,fld f) = f"
   315 by (cases f) (simp add:  fld_def)
   316 
   317 lemma ext_method_simp [simp]: "(declclass m,mthd m) = m"
   318 by (cases m) (simp add:  mthd_def)
   319 
   320 lemma ext_mbr_simp [simp]: "(declclass m,mbr m) = m"
   321 by (cases m) (simp add: mbr_def)
   322 
   323 lemma fname_simp[simp]:"fname (n,c) = n"
   324 by (simp add: fname_def)
   325 
   326 lemma declclassf_simp[simp]:"declclassf (n,c) = c"
   327 by (simp add: declclassf_def)
   328 
   329   \<comment>\<open>some mnemotic selectors for \<open>(vname \<times> qtname)\<close>\<close>
   330 
   331 definition
   332   fldname :: "vname \<times> qtname \<Rightarrow> vname"
   333   where "fldname = fst"
   334 
   335 definition
   336   fldclass :: "vname \<times> qtname \<Rightarrow> qtname"
   337   where "fldclass = snd"
   338 
   339 lemma fldname_simp[simp]: "fldname (n,c) = n"
   340 by (simp add: fldname_def)
   341 
   342 lemma fldclass_simp[simp]: "fldclass (n,c) = c"
   343 by (simp add: fldclass_def)
   344 
   345 lemma ext_fieldname_simp[simp]: "(fldname f,fldclass f) = f"
   346 by (simp add: fldname_def fldclass_def)
   347 
   348 text \<open>Convert a qualified method declaration (qualified with its declaring 
   349 class) to a qualified member declaration:  \<open>methdMembr\<close>\<close>
   350 
   351 definition
   352   methdMembr :: "qtname \<times> mdecl \<Rightarrow> qtname \<times> memberdecl"
   353   where "methdMembr m = (fst m, mdecl (snd m))"
   354 
   355 lemma methdMembr_simp[simp]: "methdMembr (c,m) = (c,mdecl m)"
   356 by (simp add: methdMembr_def)
   357 
   358 lemma accmodi_methdMembr_simp[simp]: "accmodi (methdMembr m) = accmodi m"
   359 by (cases m) (simp add: methdMembr_def)
   360 
   361 lemma is_static_methdMembr_simp[simp]: "is_static (methdMembr m) = is_static m"
   362 by (cases m) (simp add: methdMembr_def)
   363 
   364 lemma declclass_methdMembr_simp[simp]: "declclass (methdMembr m) = declclass m"
   365 by (cases m) (simp add: methdMembr_def)
   366 
   367 text \<open>Convert a qualified method (qualified with its declaring 
   368 class) to a qualified member declaration:  \<open>method\<close>\<close>
   369 
   370 definition
   371   "method" :: "sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> memberdecl)"
   372   where "method sig m = (declclass m, mdecl (sig, mthd m))"
   373 
   374 lemma method_simp[simp]: "method sig (C,m) = (C,mdecl (sig,m))"
   375 by (simp add: method_def)
   376 
   377 lemma accmodi_method_simp[simp]: "accmodi (method sig m) = accmodi m"
   378 by (simp add: method_def)
   379 
   380 lemma declclass_method_simp[simp]: "declclass (method sig m) = declclass m"
   381 by (simp add: method_def)
   382 
   383 lemma is_static_method_simp[simp]: "is_static (method sig m) = is_static m"
   384 by (cases m) (simp add: method_def)
   385 
   386 lemma mbr_method_simp[simp]: "mbr (method sig m) = mdecl (sig,mthd m)"
   387 by (simp add: mbr_def method_def)
   388 
   389 lemma memberid_method_simp[simp]:  "memberid (method sig m) = mid sig"
   390   by (simp add: method_def) 
   391 
   392 definition
   393   fieldm :: "vname \<Rightarrow> (qtname \<times> field) \<Rightarrow> (qtname \<times> memberdecl)"
   394   where "fieldm n f = (declclass f, fdecl (n, fld f))"
   395 
   396 lemma fieldm_simp[simp]: "fieldm n (C,f) = (C,fdecl (n,f))"
   397 by (simp add: fieldm_def)
   398 
   399 lemma accmodi_fieldm_simp[simp]: "accmodi (fieldm n f) = accmodi f"
   400 by (simp add: fieldm_def)
   401 
   402 lemma declclass_fieldm_simp[simp]: "declclass (fieldm n f) = declclass f"
   403 by (simp add: fieldm_def)
   404 
   405 lemma is_static_fieldm_simp[simp]: "is_static (fieldm n f) = is_static f"
   406 by (cases f) (simp add: fieldm_def)
   407 
   408 lemma mbr_fieldm_simp[simp]: "mbr (fieldm n f) = fdecl (n,fld f)"
   409 by (simp add: mbr_def fieldm_def)
   410 
   411 lemma memberid_fieldm_simp[simp]:  "memberid (fieldm n f) = fid n"
   412 by (simp add: fieldm_def) 
   413 
   414 text \<open>Select the signature out of a qualified method declaration:
   415  \<open>msig\<close>\<close>
   416 
   417 definition
   418   msig :: "(qtname \<times> mdecl) \<Rightarrow> sig"
   419   where "msig m = fst (snd m)"
   420 
   421 lemma msig_simp[simp]: "msig (c,(s,m)) = s"
   422 by (simp add: msig_def)
   423 
   424 text \<open>Convert a qualified method (qualified with its declaring 
   425 class) to a qualified method declaration:  \<open>qmdecl\<close>\<close>
   426 
   427 definition
   428   qmdecl :: "sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> mdecl)"
   429   where "qmdecl sig m = (declclass m, (sig,mthd m))"
   430 
   431 lemma qmdecl_simp[simp]: "qmdecl sig (C,m) = (C,(sig,m))"
   432 by (simp add: qmdecl_def)
   433 
   434 lemma declclass_qmdecl_simp[simp]: "declclass (qmdecl sig m) = declclass m"
   435 by (simp add: qmdecl_def)
   436 
   437 lemma accmodi_qmdecl_simp[simp]: "accmodi (qmdecl sig m) = accmodi m"
   438 by (simp add: qmdecl_def)
   439 
   440 lemma is_static_qmdecl_simp[simp]: "is_static (qmdecl sig m) = is_static m"
   441 by (cases m) (simp add: qmdecl_def)
   442 
   443 lemma msig_qmdecl_simp[simp]: "msig (qmdecl sig m) = sig"
   444 by (simp add: qmdecl_def)
   445 
   446 lemma mdecl_qmdecl_simp[simp]:  
   447  "mdecl (mthd (qmdecl sig new)) = mdecl (sig, mthd new)" 
   448 by (simp add: qmdecl_def) 
   449 
   450 lemma methdMembr_qmdecl_simp [simp]: 
   451  "methdMembr (qmdecl sig old) = method sig old"
   452 by (simp add: methdMembr_def qmdecl_def method_def)
   453 
   454 text \<open>overloaded selector \<open>resTy\<close> to select the result type 
   455 out of various HOL types\<close>
   456 
   457 class has_resTy =
   458   fixes resTy:: "'a \<Rightarrow> ty"
   459 
   460 instantiation decl_ext :: (has_resTy) has_resTy
   461 begin
   462 
   463 instance ..
   464 
   465 end
   466 
   467 instantiation member_ext :: (has_resTy) has_resTy
   468 begin
   469 
   470 instance ..
   471 
   472 end
   473 
   474 instantiation mhead_ext :: (type) has_resTy
   475 begin
   476 
   477 instance ..
   478 
   479 end
   480 
   481 axiomatization where
   482   mhead_ext_type_resTy_def: "resTy (m::('b mhead_scheme)) \<equiv> resT m"
   483 
   484 lemma mhead_resTy_simp: "resTy (m::'a mhead_scheme) = resT m"
   485 by (simp add: mhead_ext_type_resTy_def)
   486 
   487 lemma resTy_mhead [simp]:"resTy (mhead m) = resTy m"
   488 by (simp add: mhead_def mhead_resTy_simp)
   489 
   490 instantiation prod :: (type, has_resTy) has_resTy
   491 begin
   492 
   493 definition
   494   pair_resTy_def: "resTy p = resTy (snd p)"
   495 
   496 instance ..
   497 
   498 end
   499 
   500 lemma pair_resTy_simp[simp]: "resTy (x,m) = resTy m"
   501 by (simp add: pair_resTy_def)
   502 
   503 lemma qmdecl_resTy_simp [simp]: "resTy (qmdecl sig m) = resTy m"
   504 by (cases m) (simp)
   505 
   506 lemma resTy_mthd [simp]:"resTy (mthd m) = resTy m"
   507 by (cases m) (simp add: mthd_def )
   508 
   509 subsubsection "inheritable-in"
   510 text \<open>
   511 \<open>G\<turnstile>m inheritable_in P\<close>: m can be inherited by
   512 classes in package P if:
   513 \begin{itemize} 
   514 \item the declaration class of m is accessible in P and
   515 \item the member m is declared with protected or public access or if it is
   516       declared with default (package) access, the package of the declaration 
   517       class of m is also P. If the member m is declared with private access
   518       it is not accessible for inheritance at all.
   519 \end{itemize}
   520 \<close>
   521 definition
   522   inheritable_in :: "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> pname \<Rightarrow> bool" ("_ \<turnstile> _ inheritable'_in _" [61,61,61] 60)
   523 where
   524 "G\<turnstile>membr inheritable_in pack =
   525   (case (accmodi membr) of
   526      Private   \<Rightarrow> False
   527    | Package   \<Rightarrow> (pid (declclass membr)) = pack
   528    | Protected \<Rightarrow> True
   529    | Public    \<Rightarrow> True)"
   530 
   531 abbreviation
   532 Method_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 
   537 abbreviation
   538 Methd_inheritable_in::
   539  "prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> pname \<Rightarrow> bool"
   540                 ("_ \<turnstile>Methd _ _ inheritable'_in _ " [61,61,61,61] 60)
   541  where "G\<turnstile>Methd s m inheritable_in p == G\<turnstile>(method s m) inheritable_in p"
   542 
   543 subsubsection "declared-in/undeclared-in"
   544 
   545 definition
   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 
   552 definition
   553   cdeclaredfield :: "prog \<Rightarrow> qtname \<Rightarrow> (vname,field) table" where
   554   "cdeclaredfield G C =
   555     (case class G C of
   556       None \<Rightarrow> \<lambda> sig. None
   557     | Some c \<Rightarrow> table_of (cfields c))"
   558 
   559 definition
   560   declared_in :: "prog  \<Rightarrow> memberdecl \<Rightarrow> qtname \<Rightarrow> bool" ("_\<turnstile> _ declared'_in _" [61,61,61] 60)
   561 where
   562   "G\<turnstile>m declared_in C = (case m of
   563                           fdecl (fn,f ) \<Rightarrow> cdeclaredfield G C fn  = Some f
   564                         | mdecl (sig,m) \<Rightarrow> cdeclaredmethd G C sig = Some m)"
   565 
   566 abbreviation
   567 method_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 
   571 abbreviation
   572 methd_declared_in:: "prog  \<Rightarrow> sig  \<Rightarrow>(qtname \<times> methd) \<Rightarrow> qtname \<Rightarrow> bool"
   573                                ("_\<turnstile>Methd _  _ declared'_in _" [61,61,61,61] 60)
   574  where "G\<turnstile>Methd s m declared_in C == G\<turnstile>mdecl (s,mthd m) declared_in C"
   575 
   576 lemma declared_in_classD:
   577  "G\<turnstile>m declared_in C \<Longrightarrow> is_class G C"
   578 by (cases m) 
   579    (auto simp add: declared_in_def cdeclaredmethd_def cdeclaredfield_def)
   580 
   581 definition
   582   undeclared_in :: "prog  \<Rightarrow> memberid \<Rightarrow> qtname \<Rightarrow> bool" ("_\<turnstile> _ undeclared'_in _" [61,61,61] 60)
   583 where
   584   "G\<turnstile>m undeclared_in C = (case m of
   585                            fid fn  \<Rightarrow> cdeclaredfield G C fn  = None
   586                          | mid sig \<Rightarrow> cdeclaredmethd G C sig = None)"
   587 
   588 
   589 subsubsection "members"
   590 
   591 (* Can't just take a function: prog \<Rightarrow> qtname \<Rightarrow> memberdecl set because
   592    the class qtname changes to the superclass in the inductive definition
   593    below
   594 *)
   595 
   596 inductive
   597   members :: "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> bool"
   598     ("_ \<turnstile> _ member'_of _" [61,61,61] 60)
   599   for G :: prog
   600 where
   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"
   606 text \<open>Note that in the case of an inherited member only the members of the
   607 direct superclass are concerned. If a member of a superclass of the direct
   608 superclass isn't inherited in the direct superclass (not member of the
   609 direct superclass) than it can't be a member of the class. E.g. If a
   610 member of a class A is defined with package access it isn't member of a 
   611 subclass S if S isn't in the same package as A. Any further subclasses 
   612 of S will not inherit the member, regardless if they are in the same
   613 package as A or not.\<close>
   614 
   615 abbreviation
   616 method_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 
   620 abbreviation
   621 methd_member_of:: "prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> qtname \<Rightarrow> bool"
   622                            ("_ \<turnstile>Methd _ _ member'_of _" [61,61,61,61] 60)
   623  where "G\<turnstile>Methd s m member_of C == G\<turnstile>(method s m) member_of C" 
   624 
   625 abbreviation
   626 fieldm_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 
   630 definition
   631   inherits :: "prog \<Rightarrow> qtname \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> bool" ("_ \<turnstile> _ inherits _" [61,61,61] 60)
   632 where
   633   "G\<turnstile>C inherits m =
   634     (G\<turnstile>m inheritable_in (pid C) \<and> G\<turnstile>memberid m undeclared_in C \<and> 
   635       (\<exists>S. G\<turnstile>C \<prec>\<^sub>C1 S \<and> G\<turnstile>(Class S) accessible_in (pid C) \<and> G\<turnstile>m member_of S))"
   636 
   637 lemma inherits_member: "G\<turnstile>C inherits m \<Longrightarrow> G\<turnstile>m member_of C"
   638 by (auto simp add: inherits_def intro: members.Inherited)
   639 
   640 
   641 definition
   642   member_in :: "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> bool" ("_ \<turnstile> _ member'_in _" [61,61,61] 60)
   643   where "G\<turnstile>m member_in C = (\<exists> provC. G\<turnstile> C \<preceq>\<^sub>C provC \<and> G \<turnstile> m member_of provC)"
   644 text \<open>A member is in a class if it is member of the class or a superclass.
   645 If a member is in a class we can select this member. This additional notion
   646 is necessary since not all members are inherited to subclasses. So such
   647 members are not member-of the subclass but member-in the subclass.\<close>
   648 
   649 abbreviation
   650 method_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 
   654 abbreviation
   655 methd_member_in:: "prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> qtname \<Rightarrow> bool"
   656                            ("_ \<turnstile>Methd _ _ member'_in _" [61,61,61,61] 60)
   657  where "G\<turnstile>Methd s m member_in C == G\<turnstile>(method s m) member_in C"
   658 
   659 lemma member_inD: "G\<turnstile>m member_in C 
   660  \<Longrightarrow> \<exists> provC. G\<turnstile> C \<preceq>\<^sub>C provC \<and> G \<turnstile> m member_of provC"
   661 by (auto simp add: member_in_def)
   662 
   663 lemma member_inI: "\<lbrakk>G \<turnstile> m member_of provC;G\<turnstile> C \<preceq>\<^sub>C provC\<rbrakk> \<Longrightarrow>  G\<turnstile>m member_in C"
   664 by (auto simp add: member_in_def)
   665 
   666 lemma member_of_to_member_in: "G \<turnstile> m member_of C \<Longrightarrow> G \<turnstile>m member_in C"
   667 by (auto intro: member_inI)
   668 
   669 
   670 subsubsection "overriding"
   671 
   672 text \<open>Unfortunately the static notion of overriding (used during the
   673 typecheck of the compiler) and the dynamic notion of overriding (used during
   674 execution in the JVM) are not exactly the same. 
   675 \<close>
   676 
   677 text \<open>Static overriding (used during the typecheck of the compiler)\<close>
   678 
   679 inductive
   680   stat_overridesR :: "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> bool"
   681     ("_ \<turnstile> _ overrides\<^sub>S _" [61,61,61] 60)
   682   for G :: prog
   683 where
   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 
   696 text \<open>Dynamic overriding (used during the typecheck of the compiler)\<close>
   697 
   698 inductive
   699   overridesR :: "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> bool"
   700     ("_ \<turnstile> _ overrides _" [61,61,61] 60)
   701   for G :: prog
   702 where
   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 
   716 abbreviation (input)
   717 sig_stat_overrides:: 
   718  "prog  \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> methd) \<Rightarrow> bool" 
   719                                   ("_,_\<turnstile> _ overrides\<^sub>S _" [61,61,61,61] 60)
   720  where "G,s\<turnstile>new overrides\<^sub>S old == G\<turnstile>(qmdecl s new) overrides\<^sub>S (qmdecl s old)" 
   721 
   722 abbreviation (input)
   723 sig_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 
   727 subsubsection "Hiding"
   728 
   729 definition
   730   hides :: "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> bool" ("_\<turnstile> _ hides _" [61,61,61] 60)
   731 where 
   732   "G\<turnstile>new hides old =
   733     (is_static new \<and> msig new = msig old \<and>
   734       G\<turnstile>(declclass new) \<prec>\<^sub>C (declclass old) \<and>
   735       G\<turnstile>Method new declared_in (declclass new) \<and>
   736       G\<turnstile>Method old declared_in (declclass old) \<and> 
   737       G\<turnstile>Method old inheritable_in pid (declclass new))"
   738 
   739 abbreviation
   740 sig_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 
   744 lemma hidesI:
   745 "\<lbrakk>is_static new; msig new = msig old;
   746   G\<turnstile>(declclass new) \<prec>\<^sub>C (declclass old);
   747   G\<turnstile>Method new declared_in (declclass new);
   748   G\<turnstile>Method old declared_in (declclass old);
   749   G\<turnstile>Method old inheritable_in pid (declclass new)
   750  \<rbrakk> \<Longrightarrow> G\<turnstile>new hides old"
   751 by (auto simp add: hides_def)
   752 
   753 lemma hidesD:
   754 "\<lbrakk>G\<turnstile>new hides old\<rbrakk> \<Longrightarrow>  
   755   declclass new \<noteq> Object \<and> is_static new \<and> msig new = msig old \<and> 
   756   G\<turnstile>(declclass new) \<prec>\<^sub>C (declclass old) \<and>
   757   G\<turnstile>Method new declared_in (declclass new) \<and>   
   758   G\<turnstile>Method old declared_in (declclass old)"
   759 by (auto simp add: hides_def)
   760 
   761 lemma overrides_commonD:
   762 "\<lbrakk>G\<turnstile>new overrides old\<rbrakk> \<Longrightarrow>  
   763   declclass new \<noteq> Object \<and> \<not> is_static new \<and> \<not> is_static old \<and>
   764   accmodi new \<noteq> Private \<and> 
   765   msig new = msig old  \<and>
   766   G\<turnstile>(declclass new) \<prec>\<^sub>C (declclass old) \<and>
   767   G\<turnstile>Method new declared_in (declclass new) \<and>   
   768   G\<turnstile>Method old declared_in (declclass old)"
   769 by (induct set: overridesR) (auto intro: trancl_trans)
   770 
   771 lemma ws_overrides_commonD:
   772 "\<lbrakk>G\<turnstile>new overrides old;ws_prog G\<rbrakk> \<Longrightarrow>  
   773   declclass new \<noteq> Object \<and> \<not> is_static new \<and> \<not> is_static old \<and>
   774   accmodi new \<noteq> Private \<and> G\<turnstile>resTy new \<preceq> resTy old \<and>
   775   msig new = msig old  \<and>
   776   G\<turnstile>(declclass new) \<prec>\<^sub>C (declclass old) \<and>
   777   G\<turnstile>Method new declared_in (declclass new) \<and>   
   778   G\<turnstile>Method old declared_in (declclass old)"
   779 by (induct set: overridesR) (auto intro: trancl_trans ws_widen_trans)
   780 
   781 lemma overrides_eq_sigD: 
   782  "\<lbrakk>G\<turnstile>new overrides old\<rbrakk> \<Longrightarrow> msig old=msig new"
   783 by (auto dest: overrides_commonD)
   784 
   785 lemma hides_eq_sigD: 
   786  "\<lbrakk>G\<turnstile>new hides old\<rbrakk> \<Longrightarrow> msig old=msig new"
   787 by (auto simp add: hides_def)
   788 
   789 subsubsection "permits access" 
   790 definition
   791   permits_acc :: "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool" ("_ \<turnstile> _ in _ permits'_acc'_from _" [61,61,61,61] 60)
   792 where
   793   "G\<turnstile>membr in cls permits_acc_from accclass =
   794     (case (accmodi membr) of
   795       Private   \<Rightarrow> (declclass membr = accclass)
   796     | Package   \<Rightarrow> (pid (declclass membr) = pid accclass)
   797     | Protected \<Rightarrow> (pid (declclass membr) = pid accclass)
   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)"
   802 text \<open>
   803 The subcondition of the @{term "Protected"} case: 
   804 @{term "G\<turnstile>accclass \<prec>\<^sub>C declclass membr"} could also be relaxed to:
   805 @{term "G\<turnstile>accclass \<preceq>\<^sub>C declclass membr"} since in case both classes are the
   806 same the other condition @{term "(pid (declclass membr) = pid accclass)"}
   807 holds anyway.
   808 \<close> 
   809 
   810 text \<open>Like in case of overriding, the static and dynamic accessibility 
   811 of members is not uniform.
   812 \begin{itemize}
   813 \item Statically the class/interface of the member must be accessible for the
   814       member to be accessible. During runtime this is not necessary. For
   815       Example, if a class is accessible and we are allowed to access a member
   816       of this class (statically) we expect that we can access this member in 
   817       an arbitrary subclass (during runtime). It's not intended to restrict
   818       the access to accessible subclasses during runtime.
   819 \item Statically the member we want to access must be "member of" the class.
   820       Dynamically it must only be "member in" the class.
   821 \end{itemize} 
   822 \<close> 
   823 
   824 inductive
   825   accessible_fromR :: "prog \<Rightarrow> qtname \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> bool"
   826   and accessible_from :: "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
   827     ("_ \<turnstile> _ of _ accessible'_from _" [61,61,61,61] 60)
   828   and method_accessible_from :: "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
   829     ("_ \<turnstile>Method _ of _ accessible'_from _" [61,61,61,61] 60)
   830   for G :: prog and accclass :: qtname
   831 where
   832   "G\<turnstile>membr of cls accessible_from accclass \<equiv> accessible_fromR G accclass membr cls"
   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 
   851 abbreviation
   852 methd_accessible_from:: 
   853  "prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
   854                  ("_ \<turnstile>Methd _ _ of _ accessible'_from _" [61,61,61,61,61] 60)
   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 
   859 abbreviation
   860 field_accessible_from:: 
   861  "prog \<Rightarrow> vname \<Rightarrow> (qtname \<times> field) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
   862                  ("_ \<turnstile>Field _  _ of _ accessible'_from _" [61,61,61,61,61] 60)
   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 
   867 inductive
   868   dyn_accessible_fromR :: "prog \<Rightarrow> qtname \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> bool"
   869   and dyn_accessible_from' ::  "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
   870     ("_ \<turnstile> _ in _ dyn'_accessible'_from _" [61,61,61,61] 60)
   871   and method_dyn_accessible_from :: "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
   872     ("_ \<turnstile>Method _ in _ dyn'_accessible'_from _" [61,61,61,61] 60)
   873   for G :: prog and accclass :: qtname
   874 where
   875   "G\<turnstile>membr in C dyn_accessible_from accC \<equiv> dyn_accessible_fromR G accC membr C"
   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 
   890 abbreviation
   891 methd_dyn_accessible_from:: 
   892  "prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
   893              ("_ \<turnstile>Methd _ _ in _ dyn'_accessible'_from _" [61,61,61,61,61] 60)
   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 
   898 abbreviation
   899 field_dyn_accessible_from:: 
   900  "prog \<Rightarrow> vname \<Rightarrow> (qtname \<times> field) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
   901          ("_ \<turnstile>Field _ _ in _ dyn'_accessible'_from _" [61,61,61,61,61] 60)
   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 
   907 lemma accessible_from_commonD: "G\<turnstile>m of C accessible_from S
   908  \<Longrightarrow> G\<turnstile>m member_of C \<and> G\<turnstile>(Class C) accessible_in (pid S)"
   909 by (auto elim: accessible_fromR.induct)
   910 
   911 lemma 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"
   914 apply (cases m)
   915 apply (cases n,
   916         auto simp add: declared_in_def cdeclaredmethd_def cdeclaredfield_def)+
   917 done
   918 
   919 lemma declared_not_undeclared:
   920   "G\<turnstile>m declared_in C \<Longrightarrow> \<not> G\<turnstile> memberid m undeclared_in C"
   921 by (cases m) (auto simp add: declared_in_def undeclared_in_def)
   922 
   923 lemma undeclared_not_declared:
   924  "G\<turnstile> memberid m undeclared_in C \<Longrightarrow> \<not> G\<turnstile> m declared_in C" 
   925 by (cases m) (auto simp add: declared_in_def undeclared_in_def)
   926 
   927 lemma not_undeclared_declared:
   928   "\<not> G\<turnstile> membr_id undeclared_in C \<Longrightarrow> (\<exists> m. G\<turnstile>m declared_in C \<and> 
   929                                            membr_id = memberid m)"
   930 proof -
   931   assume not_undecl:"\<not> G\<turnstile> membr_id undeclared_in C"
   932   show ?thesis (is "?P membr_id")
   933   proof (cases membr_id)
   934     case (fid vname)
   935     with not_undecl
   936     obtain fld where
   937       "G\<turnstile>fdecl (vname,fld) declared_in C" 
   938       by (auto simp add: undeclared_in_def declared_in_def
   939                          cdeclaredfield_def)
   940     with fid show ?thesis 
   941       by auto
   942   next
   943     case (mid sig)
   944     with not_undecl
   945     obtain mthd where
   946       "G\<turnstile>mdecl (sig,mthd) declared_in C" 
   947       by (auto simp add: undeclared_in_def declared_in_def
   948                          cdeclaredmethd_def)
   949     with mid show ?thesis 
   950       by auto
   951   qed
   952 qed
   953 
   954 lemma unique_declared_in:
   955  "\<lbrakk>G\<turnstile>m declared_in C; G\<turnstile>n declared_in C; memberid m = memberid n\<rbrakk>
   956  \<Longrightarrow> m = n"
   957 by (auto simp add: declared_in_def cdeclaredmethd_def cdeclaredfield_def
   958             split: memberdecl.splits)
   959 
   960 lemma unique_member_of: 
   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"
   965 proof -
   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
  1011 qed
  1012 
  1013 lemma member_of_is_classD: "G\<turnstile>m member_of C \<Longrightarrow> is_class G C"
  1014 proof (induct set: members)
  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)
  1020 next
  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)
  1025 qed
  1026 
  1027 lemma member_of_declC: 
  1028  "G\<turnstile>m member_of C 
  1029   \<Longrightarrow> G\<turnstile>mbr m declared_in (declclass m)"
  1030 by (induct set: members) auto
  1031 
  1032 lemma member_of_member_of_declC:
  1033  "G\<turnstile>m member_of C 
  1034   \<Longrightarrow> G\<turnstile>m member_of (declclass m)"
  1035 by (auto dest: member_of_declC intro: members.Immediate)
  1036 
  1037 lemma member_of_class_relation:
  1038   "G\<turnstile>m member_of C \<Longrightarrow> G\<turnstile>C \<preceq>\<^sub>C declclass m"
  1039 proof (induct set: members)
  1040   case (Immediate m C)
  1041   then show "G\<turnstile>C \<preceq>\<^sub>C declclass m" by simp
  1042 next
  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)
  1046 qed
  1047 
  1048 lemma member_in_class_relation:
  1049   "G\<turnstile>m member_in C \<Longrightarrow> G\<turnstile>C \<preceq>\<^sub>C declclass m"
  1050 by (auto dest: member_inD member_of_class_relation
  1051         intro: rtrancl_trans)
  1052 
  1053 lemma 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)"
  1056 apply (rule trancl_rtrancl_trancl)
  1057 apply (erule r_into_trancl)
  1058 apply (cases old)
  1059 apply (auto dest: member_of_class_relation)
  1060 done
  1061 
  1062 lemma 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)"
  1068 apply (induct set: stat_overridesR) 
  1069 apply (frule (1) stat_override_declclasses_relation) 
  1070 apply (auto intro: trancl_trans)
  1071 done
  1072 
  1073 lemma 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
  1078 proof induct
  1079   case Immediate
  1080   then show ?case by simp
  1081 next
  1082   case Inherited
  1083   then show ?case by (auto simp add: inheritable_in_def)
  1084 qed
  1085 
  1086 lemma member_in_declC: "G\<turnstile>m member_in C\<Longrightarrow> G\<turnstile>m member_in (declclass m)"
  1087 proof -
  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)
  1104 qed
  1105 
  1106 lemma dyn_accessible_from_commonD: "G\<turnstile>m in C dyn_accessible_from S
  1107  \<Longrightarrow> G\<turnstile>m member_in C"
  1108 by (auto elim: dyn_accessible_fromR.induct)
  1109 
  1110 lemma no_Private_stat_override: 
  1111  "\<lbrakk>G\<turnstile>new overrides\<^sub>S old\<rbrakk> \<Longrightarrow> accmodi old \<noteq> Private"
  1112 by (induct set:  stat_overridesR) (auto simp add: inheritable_in_def)
  1113 
  1114 lemma no_Private_override: "\<lbrakk>G\<turnstile>new overrides old\<rbrakk> \<Longrightarrow> accmodi old \<noteq> Private"
  1115 by (induct set: overridesR) (auto simp add: inheritable_in_def)
  1116 
  1117 lemma permits_acc_inheritance:
  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"
  1120 by (cases "accmodi m")
  1121    (auto simp add: permits_acc_def
  1122             intro: subclseq_trans) 
  1123 
  1124 lemma 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"
  1127 by (cases "accmodi m") (auto simp add: permits_acc_def)
  1128 
  1129 lemma 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"
  1133 proof -
  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
  1150 qed
  1151 
  1152 lemma field_accessible_fromD:
  1153  "\<lbrakk>G\<turnstile>membr of C accessible_from accC;is_field membr\<rbrakk> 
  1154   \<Longrightarrow> G\<turnstile>membr member_of C \<and>
  1155       G\<turnstile>(Class C) accessible_in (pid accC) \<and>
  1156       G\<turnstile>membr in C permits_acc_from accC"
  1157 by (cases set: accessible_fromR)
  1158    (auto simp add: is_field_def split: memberdecl.splits) 
  1159 
  1160 lemma field_accessible_from_permits_acc_inheritance:
  1161 "\<lbrakk>G\<turnstile>membr of statC accessible_from accC; is_field membr; G \<turnstile> dynC \<preceq>\<^sub>C statC\<rbrakk>
  1162 \<Longrightarrow> G\<turnstile>membr in dynC permits_acc_from accC"
  1163 by (auto dest: field_accessible_fromD intro: permits_acc_inheritance)
  1164 
  1165 
  1166 (*
  1167 lemma accessible_Package:
  1168  "\<lbrakk>G \<turnstile> m of C accessible_from S;accmodi m = Package;
  1169    \<And> new old. G\<turnstile>new overrides\<^sub>S old \<Longrightarrow> accmodi old \<le> accmodi new\<rbrakk>
  1170   \<Longrightarrow> pid S = pid C \<and> pid C = pid (declclass m)"
  1171 proof -
  1172   assume wf: "\<And> new old. G\<turnstile>new overrides\<^sub>S old \<Longrightarrow> accmodi old \<le> accmodi new"
  1173   assume "G \<turnstile> m of C accessible_from S"
  1174   then show "accmodi m = Package \<Longrightarrow> pid S = pid C \<and> pid C = pid (declclass m)"
  1175     (is "?Pack m \<Longrightarrow> ?P C m")
  1176   proof (induct rule: accessible_fromR.induct)
  1177     fix C m
  1178     assume "G\<turnstile>m member_of C"
  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
  1214 qed
  1215 *)
  1216 
  1217 lemma accessible_fieldD: 
  1218  "\<lbrakk>G\<turnstile>membr of C accessible_from accC; is_field membr\<rbrakk>
  1219  \<Longrightarrow> G\<turnstile>membr member_of C \<and>
  1220      G\<turnstile>(Class C) accessible_in (pid accC) \<and>
  1221      G\<turnstile>membr in C permits_acc_from accC"
  1222 by (induct rule: accessible_fromR.induct) (auto dest: is_fieldD)
  1223       
  1224 
  1225 
  1226 lemma member_of_Private:
  1227 "\<lbrakk>G\<turnstile>m member_of C; accmodi m = Private\<rbrakk> \<Longrightarrow> declclass m = C"
  1228 by (induct set: members) (auto simp add: inheritable_in_def)
  1229 
  1230 lemma member_of_subclseq_declC:
  1231   "G\<turnstile>m member_of C \<Longrightarrow> G\<turnstile>C \<preceq>\<^sub>C declclass m"
  1232 by (induct set: members) (auto dest: r_into_rtrancl intro: rtrancl_trans)
  1233 
  1234 lemma member_of_inheritance:
  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"
  1240 proof -
  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
  1280 qed
  1281 
  1282 lemma 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"
  1290 proof -
  1291   from old 
  1292   have subclseq_C_old: "G\<turnstile>C \<preceq>\<^sub>C declclass old"
  1293     by (auto dest: member_of_subclseq_declC)
  1294   from new 
  1295   have subclseq_D_new: "G\<turnstile>D \<preceq>\<^sub>C declclass new"
  1296     by (auto dest: member_of_subclseq_declC)
  1297   from subcls_new_old ws
  1298   have neq_new_old: "new\<noteq>old"
  1299     by (cases new,cases old) (auto dest: subcls_irrefl)
  1300   from subclseq_D_new subclseq_D_C
  1301   have "G\<turnstile>(declclass new) \<preceq>\<^sub>C C \<or> G\<turnstile>C \<preceq>\<^sub>C (declclass new)" 
  1302     by (rule subcls_compareable)
  1303   then have "G\<turnstile>(declclass new) \<preceq>\<^sub>C C"
  1304   proof
  1305     assume "G\<turnstile>declclass new\<preceq>\<^sub>C C" then show ?thesis .
  1306   next
  1307     assume "G\<turnstile>C \<preceq>\<^sub>C (declclass new)"
  1308     with new subclseq_D_C ws 
  1309     have "G\<turnstile>new member_of C"
  1310       by (blast intro: member_of_inheritance)
  1311     with eqid old 
  1312     have "new=old"
  1313       by (blast intro: unique_member_of)
  1314     with neq_new_old 
  1315     show ?thesis
  1316       by contradiction
  1317   qed
  1318   then show ?thesis
  1319   proof (cases rule: subclseq_cases)
  1320     case Eq
  1321     assume "declclass new = C"
  1322     with new have "G\<turnstile>new member_of C"
  1323       by (auto dest: member_of_member_of_declC)
  1324     with eqid old 
  1325     have "new=old"
  1326       by (blast intro: unique_member_of)
  1327     with neq_new_old 
  1328     show ?thesis
  1329       by contradiction
  1330   next
  1331     case Subcls
  1332     assume "G\<turnstile>declclass new\<prec>\<^sub>C C"
  1333     with subclseq_D_new
  1334     show "G\<turnstile>D\<prec>\<^sub>C C"
  1335       by (rule rtrancl_trancl_trancl)
  1336   qed
  1337 qed
  1338 
  1339 corollary member_of_overrides_subcls:
  1340  "\<lbrakk>G\<turnstile>Methd sig old member_of C; G\<turnstile>Methd sig new member_of D;G\<turnstile>D \<preceq>\<^sub>C C;
  1341    G,sig\<turnstile>new overrides old; ws_prog G\<rbrakk>
  1342  \<Longrightarrow> G\<turnstile>D \<prec>\<^sub>C C"
  1343 by (drule overrides_commonD) (auto intro: member_of_subcls)    
  1344 
  1345 corollary member_of_stat_overrides_subcls:
  1346  "\<lbrakk>G\<turnstile>Methd sig old member_of C; G\<turnstile>Methd sig new member_of D;G\<turnstile>D \<preceq>\<^sub>C C;
  1347    G,sig\<turnstile>new overrides\<^sub>S old; ws_prog G\<rbrakk>
  1348  \<Longrightarrow> G\<turnstile>D \<prec>\<^sub>C C"
  1349 by (drule stat_overrides_commonD) (auto intro: member_of_subcls)    
  1350 
  1351 
  1352 
  1353 lemma inherited_field_access: 
  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"
  1358 proof -
  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)
  1365 qed
  1366 
  1367 lemma 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"
  1373 proof -
  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
  1390 qed
  1391 
  1392 subsubsection "fields and methods"
  1393 
  1394 
  1395 type_synonym
  1396   fspec = "vname \<times> qtname"
  1397 
  1398 translations 
  1399   (type) "fspec" <= (type) "vname \<times> qtname" 
  1400 
  1401 definition
  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))))"
  1406 text \<open>methods of an interface, with overriding and inheritance, cf. 9.2\<close>
  1407 
  1408 definition
  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. {}))"
  1414 text \<open>only returns imethds if the interface is accessible\<close>
  1415 
  1416 definition
  1417   methd :: "prog \<Rightarrow> qtname  \<Rightarrow> (sig,qtname \<times> methd) table" where
  1418   "methd G C =
  1419     class_rec G C 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)))"
  1425 text \<open>@{term "methd G C"}: 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 
  1431 definition
  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)"
  1435 text \<open>@{term "accmethd G S C"}: only those methods of @{term "methd G C"}, 
  1436         accessible from S\<close>
  1437 
  1438 text \<open>Note the class component in the accessibility filter. The class where
  1439     method @{term m} is declared (@{term declC}) isn't necessarily accessible 
  1440     from the current scope @{term S}. The method can be made accessible 
  1441     through inheritance, too.
  1442     So we must test accessibility of method @{term m} of class @{term C} 
  1443     (not @{term "declclass m"})\<close>
  1444 
  1445 definition
  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 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 
  1464 text \<open>@{term "dynmethd G statC dynC"}: dynamic method lookup of a reference 
  1465         with dynamic class @{term dynC} and static class @{term statC}\<close>
  1466 text \<open>Note some kind of duality between @{term methd} and @{term dynmethd} 
  1467         in the @{term class_rec} arguments. Whereas @{term methd} filters the 
  1468         subclass methods (to get only the inherited ones), @{term dynmethd} 
  1469         filters the new methods (to get only those methods which actually
  1470         override the methods of the static class)\<close>
  1471 
  1472 definition
  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)"
  1478 text \<open>@{term "dynimethd G I dynC"}: dynamic method lookup of a reference with 
  1479         dynamic class dynC and static interface type I\<close>
  1480 text \<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 methd}). 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 
  1492 definition
  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> 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)"
  1500 text \<open>@{term "dynlookup G statT dynC"}: 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 
  1505 definition
  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)"
  1509 text \<open>@{term "fields G C"} 
  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 
  1514 definition
  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)"
  1520 text  \<open>@{term "accfield G C S"}: fields of a class @{term C} which are 
  1521          accessible from scope of class
  1522          @{term S} with inheritance and hiding, cf. 8.3\<close>
  1523 text \<open>note the class component in the accessibility filter (see also 
  1524         @{term methd}).
  1525    The class declaring field @{term f} (@{term declC}) isn't necessarily 
  1526    accessible from scope @{term S}. The field can be made visible through 
  1527    inheritance, too. So we must test accessibility of field @{term f} of class 
  1528    @{term C} (not @{term "declclass f"})\<close> 
  1529 
  1530 definition
  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 
  1534 definition
  1535   efname :: "((vname \<times> qtname) \<times> field) \<Rightarrow> (vname \<times> qtname)"
  1536   where "efname = fst"
  1537 
  1538 lemma efname_simp[simp]:"efname (n,f) = n"
  1539 by (simp add: efname_def) 
  1540 
  1541 
  1542 subsection "imethds"
  1543 
  1544 lemma 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)))"
  1547 apply (unfold imethds_def)
  1548 apply (rule iface_rec [THEN trans])
  1549 apply auto
  1550 done
  1551 
  1552 
  1553 (* local lemma *)
  1554 lemma 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"
  1557 apply (subst imethds_rec)
  1558 apply assumption+
  1559 apply (rule iffD2)
  1560 apply (rule overrides_t_Some_iff)
  1561 apply (rule disjI1)
  1562 apply (auto elim: table_of_map_SomeI)
  1563 done
  1564 
  1565 lemma 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)^* \<and> m \<in> imethds G (decliface m) sig"
  1569 apply (erule rev_mp)
  1570 apply (rule ws_subint1_induct, assumption, assumption)
  1571 apply (subst imethds_rec, erule conjunct1, assumption)
  1572 apply (force elim: imethds_norec intro: rtrancl_into_rtrancl2)
  1573 done
  1574 
  1575 lemma 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"
  1581 using assms by (auto simp add: imethds_rec)
  1582 
  1583 
  1584 subsection "accimethd"
  1585 
  1586 lemma accimethds_simp [simp]: 
  1587 "G\<turnstile>Iface I accessible_in pack \<Longrightarrow> accimethds G pack I = imethds G I"
  1588 by (simp add: accimethds_def)
  1589 
  1590 lemma 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"
  1593 by (auto simp add: accimethds_def)
  1594 
  1595 lemma 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"
  1598 by simp
  1599 
  1600 subsection "methd"
  1601 
  1602 lemma methd_rec: "\<lbrakk>class G C = Some c; ws_prog G\<rbrakk> \<Longrightarrow>  
  1603   methd G C 
  1604     = (if C = Object 
  1605           then 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))"
  1609 apply (unfold methd_def)
  1610 apply (erule class_rec [THEN trans], assumption)
  1611 apply (simp)
  1612 done
  1613 
  1614 (* local lemma *)
  1615 lemma 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)"
  1618 apply (simp only: methd_rec)
  1619 apply (rule disjI1 [THEN map_add_Some_iff [THEN iffD2]])
  1620 apply (auto elim: table_of_map_SomeI)
  1621 done
  1622 
  1623 
  1624 lemma 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"   
  1628 apply (erule rev_mp)
  1629 apply (rule ws_subcls1_induct, assumption, assumption)
  1630 apply (subst methd_rec, assumption)
  1631 apply (case_tac "Ca=Object")
  1632 apply   (force elim: methd_norec )
  1633 
  1634 apply   simp
  1635 apply   (case_tac "table_of (map (\<lambda>(s, m). (s, Ca, m)) (methods c)) sig")
  1636 apply     (force intro: rtrancl_into_rtrancl2)
  1637 
  1638 apply     (auto intro: methd_norec)
  1639 done
  1640 
  1641 lemma 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)"
  1644 by (auto simp add: methd_rec)
  1645 
  1646 lemma 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"
  1650 by (auto simp add: methd_rec)
  1651 
  1652 lemma 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"
  1655 by (auto simp add: cdeclaredmethd_def declared_in_def)
  1656 
  1657 lemma 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)"
  1660 by (auto dest: methd_declC method_declared_inI)
  1661 
  1662 lemma 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"
  1666 proof -
  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
  1720 qed
  1721 
  1722 (*unused*)
  1723 lemma finite_methd:"ws_prog G \<Longrightarrow> finite {methd G C sig |sig C. is_class G C}"
  1724 apply (rule finite_is_class [THEN finite_SetCompr2])
  1725 apply (intro strip)
  1726 apply (erule_tac ws_subcls1_induct, assumption)
  1727 apply (subst methd_rec)
  1728 apply (assumption)
  1729 apply (auto intro!: finite_range_map_of finite_range_filter_tab finite_range_map_of_map_add)
  1730 done
  1731 
  1732 lemma finite_dom_methd:
  1733  "\<lbrakk>ws_prog G; is_class G C\<rbrakk> \<Longrightarrow> finite (dom (methd G C))"
  1734 apply (erule_tac ws_subcls1_induct)
  1735 apply assumption
  1736 apply (subst methd_rec)
  1737 apply (assumption)
  1738 apply (auto intro!: finite_dom_map_of finite_dom_filter_tab)
  1739 done
  1740 
  1741 
  1742 subsection "accmethd"
  1743 
  1744 lemma 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"
  1747 by (auto simp add: accmethd_def)
  1748 
  1749 lemma 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"
  1752 by (auto simp add: accmethd_def intro: filter_tab_SomeI)
  1753 
  1754 lemma 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"
  1760 by (auto dest: accmethd_SomeD methd_declC accmethd_SomeI)
  1761 
  1762 
  1763 lemma finite_dom_accmethd:
  1764  "\<lbrakk>ws_prog G; is_class G C\<rbrakk> \<Longrightarrow> finite (dom (accmethd G S C))"
  1765 by (auto simp add: accmethd_def intro: finite_dom_filter_tab finite_dom_methd)
  1766 
  1767 
  1768 subsection "dynmethd"
  1769 
  1770 lemma 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") 
  1786 proof -
  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 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
  1901 qed
  1902                
  1903 lemma dynmethd_C_C:"\<lbrakk>is_class G C; ws_prog G\<rbrakk> 
  1904 \<Longrightarrow> dynmethd G C C sig = methd G C sig"          
  1905 apply (auto simp add: dynmethd_rec)
  1906 done
  1907  
  1908 lemma 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)"
  1911 by (auto simp add: dynmethd_rec)
  1912  
  1913 lemma 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"
  1922 proof -
  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
  1936 qed
  1937 
  1938 lemma 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"
  1945 proof -
  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
  1959 qed
  1960 
  1961 
  1962 lemma 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"
  1971 proof -
  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])
  1976 qed
  1977 
  1978 lemma 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"
  1984 proof - 
  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
  2032 qed
  2033 
  2034 lemma 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")
  2041 proof -
  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
  2078 qed
  2079 
  2080 lemma 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"
  2088 proof -
  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
  2106 qed
  2107 
  2108 lemma 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"
  2116 proof - 
  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
  2130 qed
  2131 
  2132 subsection "dynlookup"
  2133 
  2134 lemma dynlookup_cases:
  2135   assumes "dynlookup G statT dynC sig = x"
  2136   obtains (NullT) "statT = NullT" and "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"
  2140 using assms by (cases statT) (auto simp add: dynlookup_def)
  2141 
  2142 subsection "fields"
  2143 
  2144 lemma 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))"
  2147 apply (simp only: fields_def)
  2148 apply (erule class_rec [THEN trans])
  2149 apply assumption
  2150 apply clarsimp
  2151 done
  2152 
  2153 (* local lemma *)
  2154 lemma 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"
  2157 apply (subst fields_rec)
  2158 apply assumption+
  2159 apply (subst map_of_append)
  2160 apply (rule disjI1 [THEN map_add_Some_iff [THEN iffD2]])
  2161 apply (auto elim: table_of_map2_SomeI)
  2162 done
  2163 
  2164 (* local lemma *)
  2165 lemma 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"
  2168 apply (case_tac "efn")
  2169 by auto
  2170 
  2171 lemma 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"
  2176 apply (erule rev_mp)
  2177 apply (rule ws_subcls1_induct, assumption, assumption)
  2178 apply (subst fields_rec, assumption)
  2179 apply clarify
  2180 apply (simp only: map_of_append)
  2181 apply (case_tac "table_of (map (case_prod (\<lambda>fn. Pair (fn, Ca))) (cfields c)) efn") 
  2182 apply   (force intro:rtrancl_into_rtrancl2 simp add: map_add_def)
  2183 
  2184 apply   (frule_tac fd="Ca" in fields_norec)
  2185 apply     assumption
  2186 apply     blast
  2187 apply   (frule table_of_fieldsD)  
  2188 apply   (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)
  2191 apply   (case_tac "efn")
  2192 apply   (simp)
  2193 done
  2194 
  2195 lemma 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 = []"
  2198 apply (subst fields_rec)
  2199 apply assumption
  2200 apply auto
  2201 done
  2202 
  2203 (* easier than with table_of *)
  2204 lemma 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)"
  2207 apply (erule rev_mp)
  2208 apply (erule converse_rtrancl_induct)
  2209 apply  fast
  2210 apply (drule subcls1D)
  2211 apply clarsimp
  2212 apply (subst fields_rec)
  2213 apply   auto
  2214 done
  2215 
  2216 
  2217 lemma 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"
  2221 apply (frule_tac ws_prog_cdeclD [THEN conjunct2], assumption, assumption)
  2222 apply (drule_tac weak_map_of_SomeI)
  2223 apply (frule_tac subcls1I [THEN subcls1_irrefl], assumption, assumption)
  2224 apply (auto dest: fields_declC [THEN conjunct2 [THEN conjunct1[THEN rtranclD]]])
  2225 done
  2226 
  2227 lemma 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)" 
  2230 apply (rule ws_subcls1_induct, assumption, assumption)
  2231 apply (subst fields_rec, assumption)            
  2232 apply (auto intro!: unique_map_inj inj_onI 
  2233             elim!: unique_append ws_unique_fields_lemma fields_norec)
  2234 done
  2235 
  2236 
  2237 subsection "accfield"
  2238 
  2239 lemma accfield_fields: 
  2240  "accfield G S C fn = Some f 
  2241   \<Longrightarrow> table_of (fields G C) (fn, declclass f) = Some (fld f)"
  2242 apply (simp only: accfield_def Let_def)
  2243 apply (rule table_of_remap_SomeD)
  2244 apply auto
  2245 done
  2246 
  2247 
  2248 lemma 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"
  2251 apply (drule accfield_fields)
  2252 apply (drule fields_declC [THEN conjunct1], assumption)
  2253 apply auto
  2254 done
  2255 
  2256 lemma accfield_accessibleD: 
  2257   "accfield G S C fn = Some f \<Longrightarrow> G\<turnstile>Field fn f of C accessible_from S"
  2258 by (auto simp add: accfield_def Let_def)
  2259 
  2260 subsection "is methd"
  2261 
  2262 lemma is_methdI: 
  2263 "\<lbrakk>class G C = Some y; methd G C sig = Some b\<rbrakk> \<Longrightarrow> is_methd G C sig"
  2264 apply (unfold is_methd_def)
  2265 apply auto
  2266 done
  2267 
  2268 lemma is_methdD: 
  2269 "is_methd G C sig \<Longrightarrow> class G C \<noteq> None \<and> methd G C sig \<noteq> None"
  2270 apply (unfold is_methd_def)
  2271 apply auto
  2272 done
  2273 
  2274 lemma finite_is_methd: 
  2275  "ws_prog G \<Longrightarrow> finite (Collect (case_prod (is_methd G)))"
  2276 apply (unfold is_methd_def)
  2277 apply (subst Collect_case_prod_Sigma)
  2278 apply (rule finite_is_class [THEN finite_SigmaI])
  2279 apply (simp only: mem_Collect_eq)
  2280 apply (fold dom_def)
  2281 apply (erule finite_dom_methd)
  2282 apply assumption
  2283 done
  2284 
  2285 subsubsection "calculation of the superclasses of a class"
  2286 
  2287 definition
  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    
  2294 lemma 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)))"
  2299 apply (unfold superclasses_def)
  2300 apply (erule class_rec [THEN trans], assumption)
  2301 apply (simp)
  2302 done
  2303 
  2304 lemma 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
  2312 proof (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)
  2317 next
  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)
  2328 qed
  2329 
  2330 lemma 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
  2337 proof (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)
  2341 next
  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 )
  2346 qed
  2347 
  2348 end