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