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