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