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