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