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