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