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