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